Module Impl.Typ

Mappings from OCaml types to R1CS variables and constraints.

type ('var, 'value, 'aux) typ' = ( 'var, 'value, 'aux ) Internal_Basic.Typ.typ' = {
var_to_fields : 'var -> Internal_Basic.field_var array * 'aux;
var_of_fields : (Internal_Basic.field_var array * 'aux) -> 'var;
value_to_fields : 'value -> Internal_Basic.field array * 'aux;
value_of_fields : (Internal_Basic.field array * 'aux) -> 'value;
size_in_field_elements : int;
constraint_system_auxiliary : unit -> 'aux;
check : 'var -> unit Internal_Basic.Checked.t;
}
type ('var, 'value) typ = ( 'var, 'value ) Internal_Basic.Typ.typ =
| 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.