Module Types.Typ

module T : sig ... end
include module type of struct include T end
type ('var, 'value, 'aux, 'field, 'checked) typ' = ( 'var, 'value, 'aux, 'field, 'checked ) T.typ' = {
var_to_fields : 'var -> 'field Cvar.t array * 'aux;
var_of_fields : ('field 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 = ( 'var, 'value, 'field, 'checked ) T.typ =
| Typ : ( 'var, 'value, 'aux, 'field, 'checked ) typ' -> ( 'var, 'value, 'field, 'checked ) typ
type ('var, 'value, 'field, 'checked) t = ( 'var, 'value, 'field, 'checked ) typ