Module Circuit.Typ

Mappings from OCaml types to R1CS variables and constraints.

type ('var, 'value, 'aux) typ' = ('var, 'value, 'aux) Internal_Basic.Typ.typ' = {
  1. var_to_fields : 'var -> Internal_Basic.field_var array * 'aux;
  2. var_of_fields : (Internal_Basic.field_var array * 'aux) -> 'var;
  3. value_to_fields : 'value -> Internal_Basic.field array * 'aux;
  4. value_of_fields : (Internal_Basic.field array * 'aux) -> 'value;
  5. size_in_field_elements : int;
  6. constraint_system_auxiliary : unit -> 'aux;
  7. check : 'var -> unit Internal_Basic.Checked.t;
}
type ('var, 'value) typ = ('var, 'value) Internal_Basic.Typ.typ =
  1. | Typ : ('var, 'value, 'aux) typ' -> ('var, 'value) typ
module Data_spec : sig ... end
type ('var, 'value) t = ('var, 'value) typ

The type ('var, 'value) t describes a mapping from the OCaml type 'value to a type representing the value using R1CS variables ('var). This description includes

  • a Store.t for storing 'values as 'vars
  • a Alloc.t for creating a 'var when we don't know what values it should contain yet
  • a Read.t for reading the contents of the 'var back out as a 'value in As_prover blocks
  • a Checked.t for asserting constraints on the 'var -- for example, that a Boolean.t is either a Field.zero or a Field.one.

Basic instances:

val unit : (unit, unit) t

Common constructors:

val tuple2 : ('var1, 'value1) t -> ('var2, 'value2) t -> ('var1 * 'var2, 'value1 * 'value2) t
val (*) : ('var1, 'value1) t -> ('var2, 'value2) t -> ('var1 * 'var2, 'value1 * 'value2) t

synonym for tuple2

val tuple3 : ('var1, 'value1) t -> ('var2, 'value2) t -> ('var3, 'value3) t -> ('var1 * 'var2 * 'var3, 'value1 * 'value2 * 'value3) t
val list : length:int -> ('var, 'value) t -> ('var list, 'value list) t

list ~length typ describes how to convert between a 'value list and a 'var list, given a description of how to convert between a 'value and a 'var.

length must be the length of the lists that are converted. This value must be constant for every use; otherwise the constraint system may use a different number of variables depending on the data given.

Passing a list of the wrong length throws an error.

val array : length:int -> ('var, 'value) t -> ('var array, 'value array) t

array ~length typ describes how to convert between a 'value array and a 'var array, given a description of how to convert between a 'value and a 'var.

length must be the length of the arrays that are converted. This value must be constant for every use; otherwise the constraint system may use a different number of variables depending on the data given.

Passing an array of the wrong length throws an error.

val hlist : (unit, unit, 'k_var, 'k_value) Data_spec.t -> ((unit, 'k_var) H_list.t, (unit, 'k_value) H_list.t) t

Unpack a Data_spec.t list to a t. The return value relates a polymorphic list of OCaml types to a polymorphic list of R1CS types.

Convert relationships over isomorphic types:

val transport : ('var, 'value1) t -> there:('value2 -> 'value1) -> back:('value1 -> 'value2) -> ('var, 'value2) t
val transport_var : ('var1, 'value) t -> there:('var2 -> 'var1) -> back:('var1 -> 'var2) -> ('var2, 'value) t
val of_hlistable : (unit, unit, 'k_var, 'k_value) Data_spec.t -> var_to_hlist:('var -> (unit, 'k_var) H_list.t) -> var_of_hlist:((unit, 'k_var) H_list.t -> 'var) -> value_to_hlist:('value -> (unit, 'k_value) H_list.t) -> value_of_hlist:((unit, 'k_value) H_list.t -> 'value) -> ('var, 'value) t

A specialised version of transport/transport_var that describes the relationship between 'var and 'value in terms of a Data_spec.t.

type 'a prover_value = 'a Internal_Basic.Typ.prover_value
val prover_value : unit -> ('a prover_value, 'a) t

A Typ.t for marshalling OCaml values generated in As_prover blocks, while keeping them opaque to the Checked world.

This is the dual of snarkless, which allows OCaml values from the Checked world to pass through As_prover blocks.