diff --git a/src/base/snark0.ml b/src/base/snark0.ml index 11ffde363..6fcef9c5f 100644 --- a/src/base/snark0.ml +++ b/src/base/snark0.ml @@ -767,7 +767,9 @@ module Run = struct module Constraint = Snark.Constraint module Typ = struct + include Types.Typ.T open Snark.Typ + module Data_spec = Typ.Data_spec type nonrec ('var, 'value) t = ('var, 'value) t diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml index 465daf208..718a83782 100644 --- a/src/base/snark_intf.ml +++ b/src/base/snark_intf.ml @@ -133,10 +133,32 @@ module type Typ_intf = sig type checked_unit - type (_, _, _, _) data_spec - type _ prover_ref + type ('var, 'value, 'aux, 'field, 'checked) 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 + } + + type ('var, 'value, 'field, 'checked) typ = + | Typ : + ('var, 'value, 'aux, 'field, 'checked) typ' + -> ('var, 'value, 'field, 'checked) typ + + module Data_spec : sig + type ('r_var, 'r_value, 'k_var, 'k_value, 'field) t = + | ( :: ) : + ('var, 'value, 'field, checked_unit) typ + * ('r_var, 'r_value, 'k_var, 'k_value, 'field) t + -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value, 'field) t + | [] : ('r_var, 'r_value, 'r_var, 'r_value, 'field) t + end + (** The type [('var, 'value) t] describes a mapping from the OCaml type ['value] to a type representing the value using R1CS variables (['var]). @@ -150,7 +172,7 @@ module type Typ_intf = sig example, that a [Boolean.t] is either a {!val:Field.zero} or a {!val:Field.one}. *) - type ('var, 'value) t = ('var, 'value, field, checked_unit) Types.Typ.t + type ('var, 'value) t = ('var, 'value, field, checked_unit) typ (** Basic instances: *) @@ -204,7 +226,7 @@ module type Typ_intf = sig (** Unpack a {!type:Data_spec.t} list to a {!type:t}. The return value relates a polymorphic list of OCaml types to a polymorphic list of R1CS types. *) val hlist : - (unit, unit, 'k_var, 'k_value) data_spec + (unit, unit, 'k_var, 'k_value, field) Data_spec.t -> ((unit, 'k_var) H_list.t, (unit, 'k_value) H_list.t) t (** Convert relationships over @@ -227,7 +249,7 @@ module type Typ_intf = sig {!type:Data_spec.t}. *) val of_hlistable : - (unit, unit, 'k_var, 'k_value) data_spec + (unit, unit, 'k_var, 'k_value, field) 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) @@ -584,11 +606,7 @@ module type Basic = sig 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) Typ0.Data_spec0.data_spec and type 'a prover_ref := 'a As_prover_ref.t - - include module type of Types.Typ.T end (** Representation of booleans within a field. @@ -1143,14 +1161,6 @@ module type Run_basic = sig and type field_var := Field.t and type checked_unit := unit Internal_Basic.Checked.t and type _ checked := unit - and type ('a, 'b, 'c, 'd) data_spec := - ( 'a - , 'b - , 'c - , 'd - , field - , unit Internal_Basic.Checked.t ) - Typ0.Data_spec0.data_spec and type 'a prover_ref := 'a As_prover_ref.t) (** Representation of booleans within a field. @@ -1268,7 +1278,11 @@ module type Run_basic = sig (Basic with type field = field and type 'a Checked.t = ('a, field) Checked_runner.Simple.t - and type 'a As_prover.Ref.t = 'a As_prover_ref.t) + and type 'a As_prover.Ref.t = 'a As_prover_ref.t + and type ('var, 'value, 'aux, 'field, 'checked) Typ.typ' = + ('var, 'value, 'aux, 'field, 'checked) Typ.typ' + and type ('var, 'value, 'field, 'checked) Typ.typ = + ('var, 'value, 'field, 'checked) Typ.typ) module Bitstring_checked : sig type t = Boolean.var list diff --git a/src/base/typ.ml b/src/base/typ.ml index af16e2538..c98f0505a 100644 --- a/src/base/typ.ml +++ b/src/base/typ.ml @@ -100,27 +100,29 @@ module Make (Checked : Checked_monad) = struct and type field_var := field Cvar.t end - module Data_spec = struct - include Data_spec0 - - type ('r_var, 'r_value, 'k_var, 'k_value, 'f) t = - ('r_var, 'r_value, 'k_var, 'k_value, 'f, (unit, 'f) Checked.t) data_spec - - let size t = - let rec go : - type r_var r_value k_var k_value. - int -> (r_var, r_value, k_var, k_value, 'f) t -> int = - fun acc t -> - match t with - | [] -> - acc - | Typ { size_in_field_elements; _ } :: t' -> - go (acc + size_in_field_elements) t' - in - go 0 t - end - module T = struct + module Data_spec = struct + type ('r_var, 'r_value, 'k_var, 'k_value, 'field) t = + | ( :: ) : + ('var, 'value, 'field) typ + * ('r_var, 'r_value, 'k_var, 'k_value, 'field) t + -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value, 'field) t + | [] : ('r_var, 'r_value, 'r_var, 'r_value, 'field) t + + let size t = + let rec go : + type r_var r_value k_var k_value. + int -> (r_var, r_value, k_var, k_value, 'f) t -> int = + fun acc t -> + match t with + | [] -> + acc + | Typ { size_in_field_elements; _ } :: t' -> + go (acc + size_in_field_elements) t' + in + go 0 t + end + let unit () : (unit, unit, 'field) t = Typ { var_to_fields = (fun () -> ([||], ())) @@ -461,5 +463,3 @@ module Make (Checked : Checked_monad) = struct include T end - -include Make (Checked_runner.Simple)