Merge pull request #847 from o1-labs/feature/opaque-typ-again

Specialize `Typ.t` for each snarky instance

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
 

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

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)