Module 1-Impl.Typ

Mappings from OCaml types to R1CS variables and constraints.

include Snarky_backendless.Snark_intf.Typ_intf with type field := Field.t and type field_var := Field.Var.t and type checked_unit := unit Checked.t and type _ checked := unit Checked.t and type ('a, 'b, 'c, 'd) data_spec := ( 'a, 'b, 'c, 'd, field, unit Checked.t ) Snarky_backendless.Snark_intf.Typ0.Data_spec0.data_spec and type 'a prover_ref := 'a As_prover.Ref.t
type ('var, 'value) t = ( 'var, 'value, Field.t, unit Checked.t ) Snarky_backendless.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.Var.t, Field.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 Checked.t ) Snarky_backendless.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 Checked.t ) Snarky_backendless.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.

include module type of Snarky_backendless.Types.Typ.T
type ('var, 'value, 'aux, 'field, 'checked) typ' = {
var_to_fields : 'var -> 'field Snarky_backendless.Cvar.t array * 'aux;
var_of_fields : ('field Snarky_backendless.Cvar.t array * 'aux) -> 'var;
value_to_fields : 'value -> 'field array * 'aux;
value_of_fields : ('field array * 'aux) -> 'value;
size_in_field_elements : int;
constraint_system_auxiliary : unit -> 'aux;
check : 'var -> 'checked;
}

The type ('var, 'value, 'field, 'checked) t describes a mapping from OCaml types to the variables and constraints they represent:

  • 'value is the OCaml type
  • 'field is the type of the field elements
  • 'var is some other type that contains some R1CS variables
  • 'checked is the type of checked computation that verifies the stored contents as R1CS variables.

For convenience and readability, it is usually best to have the 'var type mirror the 'value type in structure, for example:

type t = {b1 : bool; b2 : bool} (* 'value *)

let or (x : t) = x.b1 || x.b2

module Checked = struct
  type t = {b1 : Snark.Boolean.var; b2 : Snark.Boolean.var} (* 'var *)

  let or (x : t) = Snark.Boolean.(x.b1 || x.b2)
end
type ('var, 'value, 'field, 'checked) typ =
| Typ : ( 'var, 'value, 'aux, 'field, 'checked ) typ' -> ( 'var, 'value, 'field, 'checked ) typ