Merge pull request #856 from o1-labs/feature/abstract-over-cvar

Remove type parameters from `Typ.t`

src/base/as_prover0.ml

@@ -6,7 +6,9 @@ module Make (Backend : sig
   end
 end)
 (Types : Types.Types
-           with type 'a As_prover.t =
+           with type field = Backend.Field.t
+            and type field_var = Backend.Field.t Cvar.t
+            and type 'a As_prover.t =
              (Backend.Field.t Cvar.t -> Backend.Field.t) -> 'a) =
 struct
   type 'a t = 'a Types.As_prover.t
@@ -37,8 +39,8 @@ struct
   let read_var (v : 'var) : 'field t = fun tbl -> tbl v
 
   let read
-      (Typ { var_to_fields; value_of_fields; _ } :
-        ('var, 'value, 'field) Types.Typ.t ) (var : 'var) : 'value t =
+      (Typ { var_to_fields; value_of_fields; _ } : ('var, 'value) Types.Typ.t)
+      (var : 'var) : 'value t =
    fun tbl ->
     let field_vars, aux = var_to_fields var in
     let fields = Array.map ~f:tbl field_vars in

src/base/as_prover_intf.ml

@@ -13,7 +13,7 @@ module type Basic = sig
 
   val read_var : field Cvar.t -> field t
 
-  val read : ('var, 'value, field) Types.Typ.t -> 'var -> 'value t
+  val read : ('var, 'value) Types.Typ.t -> 'var -> 'value t
 
   module Provider : sig
     type 'a t

src/base/checked.ml

@@ -13,7 +13,7 @@ end)
   Checked_intf.S with module Types := Types with type field = Field.t = struct
   include Basic
 
-  let request_witness (typ : ('var, 'value, field) Types.Typ.t)
+  let request_witness (typ : ('var, 'value) Types.Typ.t)
       (r : 'value Request.t As_prover.t) =
     let%map h = exists typ (Request r) in
     Handle.var h

src/base/checked_intf.ml

@@ -18,7 +18,7 @@ module type Basic = sig
   val with_handler : Request.Handler.single -> (unit -> 'a t) -> 'a t
 
   val exists :
-       ('var, 'value, field) Types.Typ.t
+       ('var, 'value) Types.Typ.t
     -> 'value Types.Provider.t
     -> ('var, 'value) Handle.t t
 
@@ -47,26 +47,24 @@ module type S = sig
   val mk_lazy : (unit -> 'a t) -> 'a Lazy.t t
 
   val request_witness :
-       ('var, 'value, field) Types.Typ.t
-    -> 'value Request.t Types.As_prover.t
-    -> 'var t
+    ('var, 'value) Types.Typ.t -> 'value Request.t Types.As_prover.t -> 'var t
 
   val request :
        ?such_that:('var -> unit t)
-    -> ('var, 'value, field) Types.Typ.t
+    -> ('var, 'value) Types.Typ.t
     -> 'value Request.t
     -> 'var t
 
   val exists_handle :
        ?request:'value Request.t Types.As_prover.t
     -> ?compute:'value Types.As_prover.t
-    -> ('var, 'value, field) Types.Typ.t
+    -> ('var, 'value) Types.Typ.t
     -> ('var, 'value) Handle.t t
 
   val exists :
        ?request:'value Request.t Types.As_prover.t
     -> ?compute:'value Types.As_prover.t
-    -> ('var, 'value, field) Types.Typ.t
+    -> ('var, 'value) Types.Typ.t
     -> 'var t
 
   type response = Request.response

src/base/checked_runner.ml

@@ -12,9 +12,13 @@ type ('a, 'f) t =
   | Function of ('f Run_state.t -> 'f Run_state.t * 'a)
 
 module Simple_types (Backend : Backend_extended.S) = Types.Make_types (struct
-  type 'a checked = ('a, Backend.Field.t) t
+  type field = Backend.Field.t
+
+  type field_var = field Cvar.t
+
+  type 'a checked = ('a, field) t
 
-  type 'a as_prover = (Backend.Field.t Cvar.t -> Backend.Field.t) -> 'a
+  type 'a as_prover = (field_var -> field) -> 'a
 end)
 
 module Simple = struct
@@ -53,17 +57,14 @@ end
 module Make_checked
     (Backend : Backend_extended.S)
     (Types : Types.Types
-               with type 'a Checked.t = 'a Simple_types(Backend).Checked.t
+               with type field = Backend.Field.t
+                and type field_var = Backend.Field.t Cvar.t
+                and type 'a Checked.t = 'a Simple_types(Backend).Checked.t
                 and type 'a As_prover.t = 'a Simple_types(Backend).As_prover.t
-                and type ('var, 'value, 'aux, 'field, 'checked) Typ.typ' =
-                 ( 'var
-                 , 'value
-                 , 'aux
-                 , 'field
-                 , 'checked )
-                 Simple_types(Backend).Typ.typ'
-                and type ('var, 'value, 'field, 'checked) Typ.typ =
-                 ('var, 'value, 'field, 'checked) Simple_types(Backend).Typ.typ)
+                and type ('var, 'value, 'aux) Typ.typ' =
+                 ('var, 'value, 'aux) Simple_types(Backend).Typ.typ'
+                and type ('var, 'value) Typ.typ =
+                 ('var, 'value) Simple_types(Backend).Typ.typ)
     (As_prover : As_prover_intf.Basic
                    with type field := Backend.Field.t
                    with module Types := Types) =
@@ -228,7 +229,7 @@ struct
          ; constraint_system_auxiliary
          ; _
          } :
-        (_, _, _, _ t) Types.Typ.typ ) p : _ t =
+        (_, _) Types.Typ.typ ) p : _ t =
     Function
       (fun s ->
         if Run_state.has_witness s then (
@@ -318,17 +319,14 @@ end
 module Make
     (Backend : Backend_extended.S)
     (Types : Types.Types
-               with type 'a Checked.t = 'a Simple_types(Backend).Checked.t
+               with type field = Backend.Field.t
+                and type field_var = Backend.Cvar.t
+                and type 'a Checked.t = 'a Simple_types(Backend).Checked.t
                 and type 'a As_prover.t = 'a Simple_types(Backend).As_prover.t
-                and type ('var, 'value, 'aux, 'field, 'checked) Typ.typ' =
-                 ( 'var
-                 , 'value
-                 , 'aux
-                 , 'field
-                 , 'checked )
-                 Simple_types(Backend).Typ.typ'
-                and type ('var, 'value, 'field, 'checked) Typ.typ =
-                 ('var, 'value, 'field, 'checked) Simple_types(Backend).Typ.typ
+                and type ('var, 'value, 'aux) Typ.typ' =
+                 ('var, 'value, 'aux) Simple_types(Backend).Typ.typ'
+                and type ('var, 'value) Typ.typ =
+                 ('var, 'value) Simple_types(Backend).Typ.typ
                 and type ('request, 'compute) Provider.provider =
                  ('request, 'compute) Simple_types(Backend).Provider.provider) =
 struct

src/base/runners.ml

@@ -2,7 +2,9 @@ open Core_kernel
 
 module Make
     (Backend : Backend_extended.S)
-    (Types : Types.Types)
+    (Types : Types.Types
+               with type field = Backend.Field.t
+                and type field_var = Backend.Cvar.t)
     (Checked : Checked_intf.Extended
                  with type field = Backend.Field.t
                  with module Types := Types)
@@ -159,26 +161,15 @@ struct
         }
 
       val build :
-           input_typ:
-             ( 'input_var
-             , 'input_value
-             , field
-             , unit Types.Checked.t )
-             Types.Typ.typ
-        -> return_typ:
-             ('retvar, 'retval, field, unit Types.Checked.t) Types.Typ.typ
+           input_typ:('input_var, 'input_value) Types.Typ.typ
+        -> return_typ:('retvar, 'retval) Types.Typ.typ
         -> ('input_var, 'retvar, field, 'checked) t
     end = struct
       let allocate_public_inputs :
           type input_var input_value output_var output_value.
              int ref
-          -> input_typ:
-               ( input_var
-               , input_value
-               , field
-               , unit Types.Checked.t )
-               Types.Typ.typ
-          -> return_typ:(output_var, output_value, field) Types.Typ.t
+          -> input_typ:(input_var, input_value) Types.Typ.typ
+          -> return_typ:(output_var, output_value) Types.Typ.t
           -> input_var * output_var =
        fun next_input ~input_typ:(Typ input_typ) ~return_typ:(Typ return_typ) ->
         (* allocate variables for the public input and the public output *)
@@ -205,13 +196,8 @@ struct
 
       let build :
           type checked input_var input_value retvar retval.
-             input_typ:
-               ( input_var
-               , input_value
-               , field
-               , unit Types.Checked.t )
-               Types.Typ.typ
-          -> return_typ:(retvar, retval, _) Types.Typ.t
+             input_typ:(input_var, input_value) Types.Typ.typ
+          -> return_typ:(retvar, retval) Types.Typ.t
           -> (input_var, retvar, field, checked) t =
        fun ~input_typ ~return_typ ->
         let next_input = ref 0 in
@@ -259,7 +245,7 @@ struct
 
     let constraint_system (type a checked input_var) :
            run:(a, checked) Runner.run
-        -> input_typ:(input_var, _, _, _) Types.Typ.typ
+        -> input_typ:(input_var, _) Types.Typ.typ
         -> return_typ:_
         -> (input_var -> checked)
         -> R1CS_constraint_system.t =
@@ -271,7 +257,7 @@ struct
       builder.finish_computation (state, res)
 
     let generate_public_input :
-           ('input_var, 'input_value, _, _) Types.Typ.typ
+           ('input_var, 'input_value) Types.Typ.typ
         -> 'input_value
         -> Field.Vector.t =
      fun (Typ { value_to_fields; _ }) value ->
@@ -291,7 +277,7 @@ struct
         }
 
       let receive_public_input :
-             ('input_var, 'input_value, _) Types.Typ.t
+             ('input_var, 'input_value) Types.Typ.t
           -> _ Types.Typ.t
           -> 'input_value
           -> _ =
@@ -382,7 +368,7 @@ struct
     let conv :
         type r_var r_value.
            (int -> _ -> r_var -> Field.Vector.t -> r_value)
-        -> ('input_var, 'input_value, _) Types.Typ.t
+        -> ('input_var, 'input_value) Types.Typ.t
         -> _ Types.Typ.t
         -> (unit -> 'input_var -> r_var)
         -> 'input_value
@@ -396,7 +382,7 @@ struct
     let generate_auxiliary_input :
            run:('a, 'checked) Runner.run
         -> input_typ:_ Types.Typ.t
-        -> return_typ:(_, _, _) Types.Typ.t
+        -> return_typ:(_, _) Types.Typ.t
         -> ?handlers:Handler.t list
         -> 'k_var
         -> 'k_value =

src/base/snark0.ml

@@ -10,7 +10,9 @@ let set_eval_constraints b = Runner.eval_constraints := b
 
 module Make_basic
     (Backend : Backend_extended.S)
-    (Types : Types.Types)
+    (Types : Types.Types
+               with type field = Backend.Field.t
+                and type field_var = Backend.Cvar.t)
     (Checked : Checked_intf.Extended
                  with type field = Backend.Field.t
                  with module Types := Types)
@@ -31,7 +33,7 @@ struct
     module T = Typ.Make (Types) (Checked)
     include T.T
 
-    type ('var, 'value) t = ('var, 'value, Field.t) T.t
+    type ('var, 'value) t = ('var, 'value) T.t
 
     let unit : (unit, unit) t = unit ()
 

src/base/snark_intf.ml

@@ -128,32 +128,27 @@ module type Typ_intf = sig
 
   type field_var
 
-  type _ checked
-
   type 'field checked_unit
 
-  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
+  type ('var, 'value, 'aux) typ' =
+    { var_to_fields : 'var -> field_var array * 'aux
+    ; var_of_fields : field_var 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
+    ; check : 'var -> field checked_unit
     }
 
-  type ('var, 'value, 'field, 'checked) typ =
-    | Typ :
-        ('var, 'value, 'aux, 'field, 'checked) typ'
-        -> ('var, 'value, 'field, 'checked) typ
+  type ('var, 'value) typ =
+    | Typ : ('var, 'value, 'aux) typ' -> ('var, 'value) typ
 
   module Data_spec : sig
-    type ('r_var, 'r_value, 'k_var, 'k_value, 'field) t =
+    type ('r_var, 'r_value, 'k_var, 'k_value) t =
       | ( :: ) :
-          ('var, 'value, 'field, '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
+          ('var, 'value) typ * ('r_var, 'r_value, 'k_var, 'k_value) t
+          -> ('r_var, 'r_value, 'var -> 'k_var, 'value -> 'k_value) t
+      | [] : ('r_var, 'r_value, 'r_var, 'r_value) t
   end
 
   (** The type [('var, 'value) t] describes a mapping from the OCaml type
@@ -169,7 +164,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, field checked_unit) typ
+  type ('var, 'value) t = ('var, 'value) typ
 
   (** Basic instances: *)
 
@@ -223,7 +218,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, field) Data_spec.t
+       (unit, unit, 'k_var, 'k_value) Data_spec.t
     -> ((unit, 'k_var) H_list.t, (unit, 'k_value) H_list.t) t
 
   (** Convert relationships over
@@ -246,7 +241,7 @@ module type Typ_intf = sig
         {!type:Data_spec.t}.
     *)
   val of_hlistable :
-       (unit, unit, 'k_var, 'k_value, field) Data_spec.t
+       (unit, unit, 'k_var, 'k_value) 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,7 +579,6 @@ module type Basic = sig
         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
   end
 
   (** Representation of booleans within a field.
@@ -1122,10 +1116,13 @@ module type Run_basic = sig
   (** Mappings from OCaml types to R1CS variables and constraints. *)
   and Typ :
     (Typ_intf
-      with type field := Field.Constant.t
-       and type field_var := Field.t
+      with type field := Internal_Basic.field
+       and type field_var := Internal_Basic.Field.Var.t
        and type _ checked_unit := unit Internal_Basic.Checked.t
-       and type _ checked := unit)
+       and type ('var, 'value, 'aux) typ' =
+        ('var, 'value, 'aux) Internal_Basic.Typ.typ'
+       and type ('var, 'value) typ = ('var, 'value) Internal_Basic.Typ.typ
+       and type 'a prover_value = 'a Internal_Basic.Typ.prover_value)
 
   (** Representation of booleans within a field.
 
@@ -1228,12 +1225,7 @@ module type Run_basic = sig
   and Internal_Basic :
     (Basic
       with type field = field
-       and type 'a Checked.t = ('a, field) Checked_runner.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
-       and type 'a Typ.prover_value = 'a Typ.prover_value)
+       and type 'a Checked.t = ('a, field) Checked_runner.t)
 
   module Bitstring_checked : sig
     type t = Boolean.var list