Module 1-Impl.Typ

Mappings from OCaml types to R1CS variables and constraints.

type ('var, 'value) t = ( 'var, 'value, Field.Constant.t, unit Internal_Basic.Checked.t ) Types.Typ.t

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
val field : ( Field.t, Field.Constant.t ) 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, field, unit Internal_Basic.Checked.t ) Snark_intf.Typ0.Data_spec0.data_spec -> ( ( 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, field, unit Internal_Basic.Checked.t ) Snark_intf.Typ0.Data_spec0.data_spec -> 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.

module Internal : sig ... end

Typ.ts that make it easier to write a Typ.t for a mix of R1CS data and normal OCaml data.