Module type Snark_intf.Run

include Run_basic
module R1CS_constraint_system : sig ... end

The rank-1 constraint system used by this instance. See Backend_intf.S.R1CS_constraint_system.

type field

The finite field over which the R1CS operates.

module Bigint : sig ... end

Rank-1 constraints over Field.ts.

module Typ : Typ_intf with type field := Field.Constant.t and type field_var := Field.t and type checked_unit := unit Internal_Basic.Checked.t and type _ checked := unit and type ('a, 'b, 'c, 'd) data_spec := ( 'a, 'b, 'c, 'd, field, unit Internal_Basic.Checked.t ) Typ0.Data_spec0.data_spec and type 'a prover_ref := 'a As_prover.Ref.t

Mappings from OCaml types to R1CS variables and constraints.

module Boolean : Boolean_intf with type var = Field.t Boolean0.t and type field_var := Field.t and type 'a checked := 'a and type ('var, 'value) typ := ( 'var, 'value ) Typ.t

Representation of booleans within a field.

module Field : sig ... end
module As_prover : sig ... end

The functions in this module may only be run as the prover; trying to run them outside of functions that refer to As_prover.t will result in a runtime error.

module Proof_inputs : sig ... end
module Internal_Basic : Basic with type field = field and type 'a Checked.t = ( 'a, field ) Checked_runner.Simple.t and type 'a As_prover.Ref.t = 'a As_prover.Ref.t
module Bitstring_checked : sig ... end
module Handle : sig ... end
type response = Request.response
val unhandled : response
type request = Request.request =
| With : {
request : 'a Request.t;
respond : 'a Request.Response.t -> response;
} -> request
module Handler : sig ... end
val assert_ : ?label:string -> Constraint.t -> unit
val assert_all : ?label:string -> Constraint.t list -> unit
val assert_r1cs : ?label:string -> Field.t -> Field.t -> Field.t -> unit
val assert_square : ?label:string -> Field.t -> Field.t -> unit
val as_prover : ( unit -> unit ) As_prover.t -> unit
val next_auxiliary : unit -> int
val request_witness : ( 'var, 'value ) Typ.t -> ( unit -> 'value Request.t ) As_prover.t -> 'var
val perform : ( unit -> unit Request.t ) As_prover.t -> unit
val request : ?such_that:( 'var -> unit ) -> ( 'var, 'value ) Typ.t -> 'value Request.t -> 'var

TODO: Come up with a better name for this in relation to the above

val exists : ?request:( unit -> 'value Request.t ) As_prover.t -> ?compute:( unit -> 'value ) As_prover.t -> ( 'var, 'value ) Typ.t -> 'var
val exists_handle : ?request:( unit -> 'value Request.t ) As_prover.t -> ?compute:( unit -> 'value ) As_prover.t -> ( 'var, 'value ) Typ.t -> ( 'var, 'value ) Handle.t
val handle : ( unit -> 'a ) -> Handler.t -> 'a
val handle_as_prover : ( unit -> 'a ) -> ( unit -> Handler.t As_prover.t ) -> 'a
val if_ : Boolean.var -> typ:( 'var, _ ) Typ.t -> then_:'var -> else_:'var -> 'var

if_ b ~then_ ~else_ returns then_ if b is true, or else_ otherwise.

WARNING: The Typ.t's read field must be able to construct values from a series of field zeros.

val with_label : string -> ( unit -> 'a ) -> 'a
val make_checked : ( unit -> 'a ) -> 'a Internal_Basic.Checked.t
val constraint_system : input_typ:( 'input_var, 'input_value ) Typ.t -> return_typ:( 'a, _ ) Typ.t -> ( 'input_var -> unit -> 'a ) -> R1CS_constraint_system.t
val generate_witness : input_typ:( 'input_var, 'input_value ) Typ.t -> return_typ:( 'a, _ ) Typ.t -> ( 'input_var -> unit -> 'a ) -> 'input_value -> Proof_inputs.t
val generate_public_input : ( 'input_var, 'input_value ) Typ.t -> 'input_value -> Field.Constant.Vector.t

Generate the public input vector for a given statement.

val generate_witness_conv : f:( Proof_inputs.t -> 'r_value -> 'out ) -> input_typ:( 'input_var, 'input_value ) Typ.t -> return_typ:( 'r_var, 'r_value ) Typ.t -> ( 'input_var -> unit -> 'r_var ) -> 'input_value -> 'out
val run_unchecked : ( unit -> 'a ) -> 'a
val run_and_check : ( unit -> ( unit -> 'a ) As_prover.t ) -> 'a Core_kernel.Or_error.t
module Run_and_check_deferred (M : sig ... end) : sig ... end
val check : ( unit -> 'a ) -> unit Core_kernel.Or_error.t
val constraint_count : ?weight:( Constraint.t -> int ) -> ?log:( ?start:bool -> string -> int -> unit ) -> ( unit -> 'a ) -> int
val set_constraint_logger : ( ?at_label_boundary:([ `Start | `End ] * string) -> Constraint.t option -> unit ) -> unit
val clear_constraint_logger : unit -> unit
val in_prover : unit -> bool
val in_checked_computation : unit -> bool
val constant : ( 'var, 'value ) Typ.t -> 'value -> 'var

Return a constraint system constant representing the given value.

val run_checked : 'a Internal_Basic.Checked.t -> 'a
module Number : Number_intf.Run with type field := field and type field_var := Field.t and type bool_var := Boolean.var
module Enumerable (M : sig ... end) : Enumerable_intf.Run with type ('a, 'b) typ := ( 'a, 'b ) Typ.t and type bool_var := Boolean.var and type var = Field.t and type t := M.t