Pickles (pickles.Pickles)

module Scalar_challenge : sig ... end

module Endo : sig ... end

module Tick_field_sponge : sig ... end

module Util : sig ... end

module Step_main_inputs : sig ... end

module Backend = Backend

module Sponge_inputs : sig ... end

module Impls : sig ... end

module Tag : sig ... end

module Types_map : sig ... end

module Step_verifier : sig ... end

module Common : sig ... end

exception Return_digest of Core_kernel.Md5.t

module type Statement_intf = sig ... end

module type Statement_var_intf =
  Statement_intf with type field := Impls.Step.Field.t

module type Statement_value_intf =
  Statement_intf with type field := Impls.Step.field

module Verification_key : sig ... end

module type Proof_intf = sig ... end

module Proof : sig ... end

module Statement_with_proof : sig ... end

module Inductive_rule : sig ... end

val verify_promise : 
  (module Pickles_types.Nat.Intf with type n = 'n) ->
  (module Statement_value_intf with type t = 'a) ->
  Verification_key.t ->
  ('a * ( 'n, 'n ) Proof.t) list ->
  bool Promise.t

val verify : 
  (module Pickles_types.Nat.Intf with type n = 'n) ->
  (module Statement_value_intf with type t = 'a) ->
  Verification_key.t ->
  ('a * ( 'n, 'n ) Proof.t) list ->
  bool Async_kernel.Deferred.t

module Prover : sig ... end

module Provers : sig ... end

module Dirty : sig ... end

module Cache_handle : sig ... end

module Side_loaded : sig ... end

val compile_promise : 
  ?self:( 'var, 'value, 'max_proofs_verified, 'branches ) Tag.t ->
  ?cache:Key_cache.Spec.t list ->
  ?disk_keys:
    (( Core_kernel.Type_equal.Id.Uid.t
       * Snark_keys_header.t
       * int
       * Core_kernel.Md5.t,
       'branches )
       Pickles_types.Vector.t
     * (Core_kernel.Type_equal.Id.Uid.t
        * Snark_keys_header.t
        * Core_kernel.Md5.t)) ->
  ?return_early_digest_exception:bool ->
  ?override_wrap_domain:Pickles_base.Proofs_verified.t ->
  public_input:
    ( 'var, 'value, 'a_var, 'a_value, 'ret_var, 'ret_value )
      Inductive_rule.public_input ->
  auxiliary_typ:( 'auxiliary_var, 'auxiliary_value ) Impls.Step.Typ.t ->
  branches:(module Pickles_types.Nat.Intf with type n = 'branches) ->
  max_proofs_verified:
    (module Pickles_types.Nat.Add.Intf with type n = 'max_proofs_verified) ->
  name:string ->
  constraint_constants:Snark_keys_header.Constraint_constants.t ->
  choices:
    ( self:( 'var, 'value, 'max_proofs_verified, 'branches ) Tag.t ->
      ( 'prev_varss,
        'prev_valuess,
        'widthss,
        'heightss,
        'a_var,
        'a_value,
        'ret_var,
        'ret_value,
        'auxiliary_var,
        'auxiliary_value )
        Pickles_types.Hlist.H4_6.T(Inductive_rule).t ) ->
  unit ->
  ( 'var, 'value, 'max_proofs_verified, 'branches ) Tag.t
  * Cache_handle.t
  * (module Proof_intf
  with type statement = 'value
   and type t = ( 'max_proofs_verified, 'max_proofs_verified ) Proof.t)
  * ( 'prev_valuess,
      'widthss,
      'heightss,
      'a_value,
      ('ret_value
       * 'auxiliary_value
       * ( 'max_proofs_verified, 'max_proofs_verified ) Proof.t)
        Promise.t )
      Pickles_types.Hlist.H3_2.T(Prover).t

This compiles a series of inductive rules defining a set into a proof system for proving membership in that set, with a prover corresponding to each inductive rule.

val compile : 
  ?self:( 'var, 'value, 'max_proofs_verified, 'branches ) Tag.t ->
  ?cache:Key_cache.Spec.t list ->
  ?disk_keys:
    (( Core_kernel.Type_equal.Id.Uid.t
       * Snark_keys_header.t
       * int
       * Core_kernel.Md5.t,
       'branches )
       Pickles_types.Vector.t
     * (Core_kernel.Type_equal.Id.Uid.t
        * Snark_keys_header.t
        * Core_kernel.Md5.t)) ->
  ?override_wrap_domain:Pickles_base.Proofs_verified.t ->
  public_input:
    ( 'var, 'value, 'a_var, 'a_value, 'ret_var, 'ret_value )
      Inductive_rule.public_input ->
  auxiliary_typ:( 'auxiliary_var, 'auxiliary_value ) Impls.Step.Typ.t ->
  branches:(module Pickles_types.Nat.Intf with type n = 'branches) ->
  max_proofs_verified:
    (module Pickles_types.Nat.Add.Intf with type n = 'max_proofs_verified) ->
  name:string ->
  constraint_constants:Snark_keys_header.Constraint_constants.t ->
  choices:
    ( self:( 'var, 'value, 'max_proofs_verified, 'branches ) Tag.t ->
      ( 'prev_varss,
        'prev_valuess,
        'widthss,
        'heightss,
        'a_var,
        'a_value,
        'ret_var,
        'ret_value,
        'auxiliary_var,
        'auxiliary_value )
        Pickles_types.Hlist.H4_6.T(Inductive_rule).t ) ->
  unit ->
  ( 'var, 'value, 'max_proofs_verified, 'branches ) Tag.t
  * Cache_handle.t
  * (module Proof_intf
  with type statement = 'value
   and type t = ( 'max_proofs_verified, 'max_proofs_verified ) Proof.t)
  * ( 'prev_valuess,
      'widthss,
      'heightss,
      'a_value,
      ('ret_value
       * 'auxiliary_value
       * ( 'max_proofs_verified, 'max_proofs_verified ) Proof.t)
        Async_kernel.Deferred.t )
      Pickles_types.Hlist.H3_2.T(Prover).t

This compiles a series of inductive rules defining a set into a proof system for proving membership in that set, with a prover corresponding to each inductive rule.