S (snarky.Snarky_backendless.Snark

include Basic

type field

The finite field over which the R1CS operates.

module R1CS_constraint_system : sig ... end

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

module Bigint : sig ... end

module Constraint : 
  Constraint_intf with type field := Field.t and type field_var := Field.Var.t

Rank-1 constraints over Var.ts.

The data specification for checked computations.

module Typ : sig ... end

Mappings from OCaml types to R1CS variables and constraints.

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

Representation of booleans within a field.

module Checked : sig ... end

Checked computations.

module Field : sig ... end

module As_prover : sig ... end

Code that can be run by the prover only, using 'superpowers' like looking at the contents of R1CS variables and creating new variables from other OCaml values.

module Proof_inputs : sig ... end

The complete set of inputs needed to generate a zero-knowledge proof.

module Let_syntax : Monad_let.Syntax2 with type ('a, 's) t := 'a Checked.t

module Bitstring_checked : sig ... end

Utility functions for dealing with lists of bits in the R1CS.

module Handle : sig ... end

Representation of an R1CS value and an OCaml value (if running as the prover) together.

module Runner : sig ... end

Utility functions for calling single checked computations.

type response = Request.response

val unhandled : response

type request = Request.request =

| With : {

request : 'a Request.t;

respond : 'a Request.Response.t -> response;

} -> request

The argument type for request handlers.

type _ Request.t += My_request : 'a list -> 'a Request.t

let handled (c : ('a) Checked.t) : ('a) Checked.t =
  handle (fun (With {request; respond}) ->
    match request with
    | My_request l ->
      let x = (* Do something with l to create a single value. *) in
      respond (Provide x)
    | _ -> unhandled )

module Handler : sig ... end

The type of handlers.

val assert_ : ?label:string -> Constraint.t -> unit Checked.t

Add a constraint to the constraint system, optionally with the label given by label.

val assert_all : ?label:string -> Constraint.t list -> unit Checked.t

Add all of the constraints in the list to the constraint system, optionally with the label given by label.

val assert_r1cs : 
  ?label:string ->
  Field.Var.t ->
  Field.Var.t ->
  Field.Var.t ->
  unit Checked.t

Add a rank-1 constraint to the constraint system, optionally with the label given by label.

See Constraint.r1cs for more information on rank-1 constraints.

val assert_square : 
  ?label:string ->
  Field.Var.t ->
  Field.Var.t ->
  unit Checked.t

Add a 'square' constraint to the constraint system, optionally with the label given by label.

See Constraint.square for more information.

val as_prover : unit As_prover.t -> unit Checked.t

Run an As_prover block.

val mk_lazy : ( unit -> 'a Checked.t ) -> 'a Core_kernel.Lazy.t Checked.t

Lazily evaluate a checked computation.

Any constraints within the checked computation are not added to the constraint system unless the lazy value is forced.

val next_auxiliary : unit -> int Checked.t

Internal: read the value of the next unused auxiliary input index.

val request_witness : 
  ( 'var, 'value ) Typ.t ->
  'value Request.t As_prover.t ->
  'var Checked.t

request_witness typ create_request runs the create_request As_prover.t block to generate a Request.t.

This allows us to introduce values into the R1CS without passing them as public inputs.

If no handler for the request is attached by handle, this raises a Failure.

val perform : unit Request.t As_prover.t -> unit Checked.t

Like request_witness, but the request doesn't return any usable value.

val request : 
  ?such_that:( 'var -> unit Checked.t ) ->
  ( 'var, 'value ) Typ.t ->
  'value Request.t ->
  'var Checked.t

Like request_witness, but generates the request without using any As_prover 'superpowers'.

The argument such_that allows adding extra constraints on the returned value.

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

val exists : 
  ?request:'value Request.t As_prover.t ->
  ?compute:'value As_prover.t ->
  ( 'var, 'value ) Typ.t ->
  'var Checked.t

Introduce a value into the R1CS.

The request argument functions like request_witness, creating a request and returning the result.
If no request argument is given, or if the request isn't handled, then compute is run to create a value.

If compute is not given and request fails/is also not given, then this function raises a Failure.

val exists_handle : 
  ?request:'value Request.t As_prover.t ->
  ?compute:'value As_prover.t ->
  ( 'var, 'value ) Typ.t ->
  ( 'var, 'value ) Handle.t Checked.t

Like exists, but returns a Handle.t.

This persists the OCaml value of the result, which is stored unchanged in the Handle.t and can be recalled in later As_prover blocks using Handle.value.

val handle : ( unit -> 'a Checked.t ) -> Handler.t -> 'a Checked.t

Add a request handler to the checked computation, to be used by request_witness, perform, request or exists.

val handle_as_prover : 
  ( unit -> 'a Checked.t ) ->
  Handler.t As_prover.t ->
  'a Checked.t

Generate a handler using the As_prover 'superpowers', and use it for request_witness, perform, request or exists calls in the wrapped checked computation.

val if_ : 
  Boolean.var ->
  typ:( 'var, _ ) Typ.t ->
  then_:'var ->
  else_:'var ->
  'var Checked.t

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 Checked.t ) -> 'a Checked.t

Add a label to all of the constraints added in the checked computation. If a constraint is checked and isn't satisfied, this label will be shown in the error message.

val constraint_system : 
  input_typ:( 'input_var, 'input_value ) Typ.t ->
  return_typ:( 'a, _ ) Typ.t ->
  ( 'input_var -> 'a Checked.t ) ->
  R1CS_constraint_system.t

Generate the R1CS for the checked computation.

val conv : 
  ( 'r_var -> 'r_value ) ->
  ( 'input_var, 'input_value ) Typ.t ->
  ( _, _ ) Typ.t ->
  ( 'input_var -> 'r_var ) ->
  'input_value ->
  'r_value

Internal: supplies arguments to a checked computation by storing them according to the Data_spec.t and passing the R1CS versions.

val generate_public_input : 
  ( 'input_var, 'input_value ) Typ.t ->
  'input_value ->
  Field.Vector.t

Generate the public input vector for a given statement.

val generate_witness : 
  input_typ:( 'input_var, 'input_value ) Typ.t ->
  return_typ:( 'r_var, _ ) Typ.t ->
  ( 'input_var -> 'r_var Checked.t ) ->
  'input_value ->
  Proof_inputs.t

Generate a witness (auxiliary input) for the given public input.

Returns a record of field vectors {public_inputs; auxiliary_inputs}, corresponding to the given public input and generated auxiliary input.

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 -> 'r_var Checked.t ) ->
  'input_value ->
  'out

Generate a witness (auxiliary input) for the given public input and pass the result to a function.

Returns the result of applying f to the record of field vectors {public_inputs; auxiliary_inputs}, corresponding to the given public input and generated auxiliary input.

val run_unchecked : 'a Checked.t -> 'a

Run a checked computation as the prover, without checking the constraints.

val run_and_check : 'a As_prover.t Checked.t -> 'a Core_kernel.Or_error.t

Run a checked computation as the prover, checking the constraints.

val check : 'a Checked.t -> unit Core_kernel.Or_error.t

Run a checked computation as the prover, returning true if the constraints are all satisfied, or false otherwise.

val generate_auxiliary_input : 
  input_typ:( 'input_var, 'input_value ) Typ.t ->
  return_typ:( 'a, _ ) Typ.t ->
  ( 'input_var -> 'a Checked.t ) ->
  'input_value ->
  unit

Run the checked computation and generate the auxiliary input, but don't generate a proof.

Returns unit; this is for testing only.

val constraint_count : 
  ?weight:( Constraint.t -> int ) ->
  ?log:( ?start:bool -> string -> int -> unit ) ->
  ( unit -> _ Checked.t ) ->
  int

Returns the number of constraints in the constraint system.

The optional log argument is called at the start and end of each with_label, with the arguments log ?start label count, where:

start is Some true if it the start of the with_label, or None otherwise
label is the label added by with_label
count is the number of constraints at that point.

val constant : ( 'var, 'value ) Typ.t -> 'value -> 'var

Return a constraint system constant representing the given value.

module Test : sig ... end

val set_constraint_logger : 
  ( ?at_label_boundary:([ `Start | `End ] * string) ->
    Constraint.t option ->
    unit ) ->
  unit

val clear_constraint_logger : unit -> unit

module Number : 
  Number_intf.S
    with type 'a checked := 'a Checked.t
     and type field := field
     and type field_var := Field.Var.t
     and type bool_var := Boolean.var

module Enumerable
  (M : sig ... end) : 
  Enumerable_intf.S
    with type 'a checked := 'a Checked.t
     and type ('a, 'b) typ := ( 'a, 'b ) Typ.t
     and type bool_var := Boolean.var
     and type var = Field.Var.t
     and type t := M.t