From b243a1fa64c47bf624d5139924c2f90f95a32b66 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Thu, 2 Jan 2025 17:09:38 +0000
Subject: [PATCH 01/13] Remove redundant functor

---
 src/base/as_prover0.ml |  9 ---------
 src/base/snark0.ml     | 14 +-------------
 2 files changed, 1 insertion(+), 22 deletions(-)

diff --git a/src/base/as_prover0.ml b/src/base/as_prover0.ml
index f6a821cef..f5d47da95 100644
--- a/src/base/as_prover0.ml
+++ b/src/base/as_prover0.ml
@@ -80,12 +80,3 @@ struct
      fun _ -> Option.value_exn t.value
   end
 end
-
-module Make_extended (Env : sig
-  type field
-end)
-(As_prover : As_prover_intf.Basic with type field := Env.field) =
-struct
-  include Env
-  include As_prover
-end
diff --git a/src/base/snark0.ml b/src/base/snark0.ml
index aa4898943..5748eec22 100644
--- a/src/base/snark0.ml
+++ b/src/base/snark0.ml
@@ -659,18 +659,6 @@ module Make (Backend : Backend_intf.S) = struct
   module Checked1 =
     Checked.Make (Backend_extended) (Types) (Checked_runner) (As_prover1)
 
-  module Field_T = struct
-    type field = Backend_extended.Field.t
-  end
-
-  module As_prover_ext =
-    As_prover0.Make_extended
-      (Field_T)
-      (struct
-        module Types = Types
-        include As_prover1
-      end)
-
   module Checked_for_basic = struct
     include (
       Checked1 :
@@ -689,7 +677,7 @@ module Make (Backend : Backend_intf.S) = struct
   end
 
   module Basic =
-    Make_basic (Backend_extended) (Types) (Checked_for_basic) (As_prover_ext)
+    Make_basic (Backend_extended) (Types) (Checked_for_basic) (As_prover1)
       (Runner0)
   include Basic
   module Number = Number.Make (Basic)

From 9151622f3e95ba0c7bd9a04ebe91d69577eb7679 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Thu, 2 Jan 2025 17:25:30 +0000
Subject: [PATCH 02/13] Use field and field_var from Types module

---
 src/base/as_prover_intf.ml |  9 +++--
 src/base/checked.ml        | 12 +++----
 src/base/checked_intf.ml   | 11 +++---
 src/base/checked_runner.ml | 25 ++++----------
 src/base/runners.ml        | 11 ++----
 src/base/snark0.ml         | 17 +++------
 src/base/utils.ml          | 14 +++-----
 src/base/utils.mli         | 70 +++++++++++++++-----------------------
 8 files changed, 58 insertions(+), 111 deletions(-)

diff --git a/src/base/as_prover_intf.ml b/src/base/as_prover_intf.ml
index eeabefcee..b05a53fb7 100644
--- a/src/base/as_prover_intf.ml
+++ b/src/base/as_prover_intf.ml
@@ -1,24 +1,23 @@
 module type Basic = sig
   module Types : Types.Types
 
-  type field
-
   type 'a t = 'a Types.As_prover.t
 
   include Monad_let.S with type 'a t := 'a t
 
-  val run : 'a t -> (field Cvar.t -> field) -> 'a
+  val run : 'a t -> (Types.field_var -> Types.field) -> 'a
 
   val map2 : 'a t -> 'b t -> f:('a -> 'b -> 'c) -> 'c t
 
-  val read_var : field Cvar.t -> field t
+  val read_var : Types.field_var -> Types.field t
 
   val read : ('var, 'value) Types.Typ.t -> 'var -> 'value t
 
   module Provider : sig
     type 'a t
 
-    val run : 'a t -> (field Cvar.t -> field) -> Request.Handler.t -> 'a option
+    val run :
+      'a t -> (Types.field_var -> Types.field) -> Request.Handler.t -> 'a option
   end
 
   module Handle : sig
diff --git a/src/base/checked.ml b/src/base/checked.ml
index 24a262721..cafc87d8a 100644
--- a/src/base/checked.ml
+++ b/src/base/checked.ml
@@ -2,18 +2,14 @@ open Core_kernel
 
 module Make
     (Backend : Backend_extended.S)
-    (Types : Types.Types)
+    (Types : Types.Types with type field_var = Backend.Cvar.t)
     (Basic : Checked_intf.Basic
-               with type field = Backend.Field.t
-                and type constraint_ = Backend.Constraint.t
+               with type constraint_ = Backend.Constraint.t
                with module Types := Types)
-    (As_prover : As_prover_intf.Basic
-                   with type field := Basic.field
-                   with module Types := Types) :
+    (As_prover : As_prover_intf.Basic with module Types := Types) :
   Checked_intf.S
     with module Types := Types
-    with type field = Backend.Field.t
-     and type run_state = Basic.run_state
+    with type run_state = Basic.run_state
      and type constraint_ = Basic.constraint_ = struct
   include Basic
 
diff --git a/src/base/checked_intf.ml b/src/base/checked_intf.ml
index 92ec9b398..e7a79d8d7 100644
--- a/src/base/checked_intf.ml
+++ b/src/base/checked_intf.ml
@@ -1,8 +1,6 @@
 module type Basic = sig
   module Types : Types.Types
 
-  type field
-
   type constraint_
 
   type 'a t = 'a Types.Checked.t
@@ -40,8 +38,6 @@ end
 module type S = sig
   module Types : Types.Types
 
-  type field
-
   type constraint_
 
   type run_state
@@ -95,13 +91,14 @@ module type S = sig
 
   val assert_ : constraint_ -> unit t
 
-  val assert_r1cs : field Cvar.t -> field Cvar.t -> field Cvar.t -> unit t
+  val assert_r1cs :
+    Types.field_var -> Types.field_var -> Types.field_var -> unit t
 
-  val assert_square : field Cvar.t -> field Cvar.t -> unit t
+  val assert_square : Types.field_var -> Types.field_var -> unit t
 
   val assert_all : constraint_ list -> unit t
 
-  val assert_equal : field Cvar.t -> field Cvar.t -> unit t
+  val assert_equal : Types.field_var -> Types.field_var -> unit t
 
   val direct : (run_state -> run_state * 'a) -> 'a t
 
diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml
index f9e15dabd..b78048431 100644
--- a/src/base/checked_runner.ml
+++ b/src/base/checked_runner.ml
@@ -26,16 +26,14 @@ module Make_checked
     (Backend : Backend_extended.S)
     (Types : Types.Types
                with type field = Backend.Field.t
-                and type field_var = Backend.Field.t Cvar.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) 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) =
+    (As_prover : As_prover_intf.Basic with module Types := Types) =
 struct
   type run_state = Backend.Run_state.t
 
@@ -265,15 +263,11 @@ struct
 end
 
 module type Run_extras = sig
-  type field
-
-  type cvar
-
   type run_state
 
   module Types : Types.Types
 
-  val get_value : run_state -> cvar -> field
+  val get_value : run_state -> Types.field_var -> Types.field
 
   val run_as_prover :
     'a Types.As_prover.t option -> run_state -> run_state * 'a option
@@ -318,15 +312,10 @@ struct
         include
           Checked_intf.Basic
             with module Types := Types
-            with type field := Checked_runner.field
-             and type run_state := run_state
+            with type run_state := run_state
 
         include
-          Run_extras
-            with module Types := Types
-            with type field := Backend.Field.t
-             and type cvar := Backend.Cvar.t
-             and type run_state := run_state
+          Run_extras with module Types := Types with type run_state := run_state
       end )
 
   let run = Checked_runner.eval
@@ -392,9 +381,9 @@ module type S = sig
   module State : sig
     val make :
          num_inputs:int
-      -> input:field Run_state_intf.Vector.t
+      -> input:Types.field Run_state_intf.Vector.t
       -> next_auxiliary:int ref
-      -> aux:field Run_state_intf.Vector.t
+      -> aux:Types.field Run_state_intf.Vector.t
       -> ?system:r1cs
       -> ?eval_constraints:bool
       -> ?handler:Request.Handler.t
diff --git a/src/base/runners.ml b/src/base/runners.ml
index 5cd2a104f..010d39eba 100644
--- a/src/base/runners.ml
+++ b/src/base/runners.ml
@@ -7,17 +7,12 @@ module Make
                 and type field_var = Backend.Cvar.t)
     (Checked : Checked_intf.Extended
                  with module Types := Types
-                 with type field = Backend.Field.t
-                  and type run_state = Backend.Run_state.t
+                 with type run_state = Backend.Run_state.t
                   and type constraint_ = Backend.Constraint.t)
-    (As_prover : As_prover_intf.Basic
-                   with type field := Backend.Field.t
-                   with module Types := Types)
+    (As_prover : As_prover_intf.Basic with module Types := Types)
     (Runner : Checked_runner.S
                 with module Types := Types
-                with type field := Backend.Field.t
-                 and type cvar := Backend.Cvar.t
-                 and type constr := Backend.Constraint.t option
+                with type constr := Backend.Constraint.t option
                  and type r1cs := Backend.R1CS_constraint_system.t
                  and type run_state = Backend.Run_state.t) =
 struct
diff --git a/src/base/snark0.ml b/src/base/snark0.ml
index 5748eec22..256e72d71 100644
--- a/src/base/snark0.ml
+++ b/src/base/snark0.ml
@@ -15,17 +15,12 @@ module Make_basic
                 and type field_var = Backend.Cvar.t)
     (Checked : Checked_intf.Extended
                  with module Types := Types
-                 with type field = Backend.Field.t
-                  and type run_state = Backend.Run_state.t
+                 with type run_state = Backend.Run_state.t
                   and type constraint_ = Backend.Constraint.t)
-    (As_prover : As_prover_intf.Basic
-                   with type field := Backend.Field.t
-                   with module Types := Types)
+    (As_prover : As_prover_intf.Basic with module Types := Types)
     (Runner : Runner.S
                 with module Types := Types
-                with type field := Backend.Field.t
-                 and type cvar := Backend.Cvar.t
-                 and type constr := Backend.Constraint.t option
+                with type constr := Backend.Constraint.t option
                  and type r1cs := Backend.R1CS_constraint_system.t
                  and type run_state = Backend.Run_state.t) =
 struct
@@ -77,8 +72,7 @@ struct
       Checked :
         Checked_intf.Extended
           with module Types := Types
-          with type field := field
-           and type run_state = Backend.Run_state.t
+          with type run_state = Backend.Run_state.t
            and type constraint_ = Backend.Constraint.t )
 
     let perform req = request_witness Typ.unit req
@@ -665,12 +659,9 @@ module Make (Backend : Backend_intf.S) = struct
         Checked_intf.S
           with module Types := Types
           with type 'a t := 'a Checked1.t
-           and type field := Backend_extended.Field.t
            and type run_state = Backend.Run_state.t
            and type constraint_ = Backend_extended.Constraint.t )
 
-    type field = Backend_extended.Field.t
-
     type 'a t = 'a Types.Checked.t
 
     let run = Runner0.run
diff --git a/src/base/utils.ml b/src/base/utils.ml
index 0587f7deb..1e4ab67e3 100644
--- a/src/base/utils.ml
+++ b/src/base/utils.ml
@@ -11,12 +11,9 @@ module Make
                 and type field_var = Backend.Cvar.t)
     (Checked : Checked_intf.Extended
                  with module Types := Types
-                 with type field = Backend.Field.t
-                  and type run_state = Backend.Run_state.t
+                 with type run_state = Backend.Run_state.t
                   and type constraint_ = Backend.Constraint.t)
-    (As_prover : As_prover_intf.Basic
-                   with type field := Backend.Field.t
-                   with module Types := Types)
+    (As_prover : As_prover_intf.Basic with module Types := Types)
     (Typ : Snark_intf.Typ_intf
              with type field := Backend.Field.t
               and type field_var := Backend.Cvar.t
@@ -26,9 +23,7 @@ module Make
               and type ('var, 'value) typ := ('var, 'value) Types.Typ.typ)
     (Runner : Runner.S
                 with module Types := Types
-                with type field := Backend.Field.t
-                 and type cvar := Backend.Cvar.t
-                 and type constr := Backend.Constraint.t option
+                with type constr := Backend.Constraint.t option
                  and type r1cs := Backend.R1CS_constraint_system.t
                  and type run_state = Backend.Run_state.t) =
 struct
@@ -40,8 +35,7 @@ struct
     Checked :
       Checked_intf.Extended
         with module Types := Types
-        with type field := field
-         and type constraint_ := Constraint.t )
+        with type constraint_ := Constraint.t )
 
   (* [equal_constraints z z_inv r] asserts that
      if z = 0 then r = 1, or
diff --git a/src/base/utils.mli b/src/base/utils.mli
index 9caf9cf54..8707683e8 100644
--- a/src/base/utils.mli
+++ b/src/base/utils.mli
@@ -1,4 +1,3 @@
-module Cvar0 = Cvar
 module Runner = Checked_runner
 
 val set_eval_constraints : bool -> unit
@@ -10,12 +9,9 @@ module Make : functor
               and type field_var = Backend.Cvar.t)
   (Checked : Checked_intf.Extended
                with module Types := Types
-               with type field = Backend.Field.t
-                and type run_state = Backend.Run_state.t
-                and type constraint_ = Backend.Constraint.t)
-  (As_prover : As_prover_intf.Basic
-                 with type field := Backend.Field.t
-                 with module Types := Types)
+               with type run_state = Backend.Run_state.t
+               with type constraint_ = Backend.Constraint.t)
+  (As_prover : As_prover_intf.Basic with module Types := Types)
   (Typ : Snark_intf.Typ_intf
            with type field := Backend.Field.t
             and type field_var := Backend.Cvar.t
@@ -25,25 +21,21 @@ module Make : functor
             and type ('var, 'value) typ := ('var, 'value) Types.Typ.typ)
   (Runner : Runner.S
               with module Types := Types
-              with type field := Backend.Field.t
-               and type cvar := Backend.Cvar.t
-               and type constr := Backend.Constraint.t option
+              with type constr := Backend.Constraint.t option
                and type r1cs := Backend.R1CS_constraint_system.t
                and type run_state = Backend.Run_state.t)
   -> sig
   val equal :
-       Checked.field Cvar0.t
-    -> Checked.field Cvar0.t
-    -> Checked.field Cvar0.t Boolean.t Checked.t
+    Types.field_var -> Types.field_var -> Types.field_var Boolean.t Checked.t
 
   val if_ :
-       Checked.field Cvar0.t Boolean.t
-    -> then_:Checked.field Cvar0.t
-    -> else_:Checked.field Cvar0.t
-    -> Checked.field Cvar0.t Types.Checked.t
+       Types.field_var Boolean.t
+    -> then_:Types.field_var
+    -> else_:Types.field_var
+    -> Types.field_var Types.Checked.t
 
   module Boolean : sig
-    type var = Checked.field Cvar0.t Boolean.t
+    type var = Types.field_var Boolean.t
 
     type value = bool
 
@@ -54,13 +46,13 @@ module Make : functor
     val not : var -> var
 
     val if_ :
-         Checked.field Cvar0.t Boolean.t
+         Types.field_var Boolean.t
       -> then_:var
       -> else_:var
-      -> Checked.field Cvar0.t Boolean.t Types.Checked.t
+      -> Types.field_var Boolean.t Types.Checked.t
 
     val _and_for_square_constraint_systems :
-      var -> var -> Checked.field Cvar0.t Boolean.t Types.Checked.t
+      var -> var -> Types.field_var Boolean.t Types.Checked.t
 
     val ( && ) : var -> var -> var Checked.t
 
@@ -85,7 +77,7 @@ module Make : functor
     val ( lxor ) : var -> var -> var Types.Checked.t
 
     module Array : sig
-      val num_true : var array -> Checked.field Cvar0.t
+      val num_true : var array -> Types.field_var
 
       val any : var array -> var Types.Checked.t
 
@@ -103,7 +95,7 @@ module Make : functor
     val of_field : Backend.Cvar.t -> Backend.Cvar.t Boolean.t Types.Checked.t
 
     module Unsafe : sig
-      val of_cvar : Checked.field Cvar0.t -> var
+      val of_cvar : Types.field_var -> var
     end
 
     module Assert : sig
@@ -145,34 +137,28 @@ module Make : functor
 
   val mul :
        ?label:string
-    -> Checked.field Cvar0.t
-    -> Checked.field Cvar0.t
-    -> Checked.field Cvar0.t Types.Checked.t
+    -> Types.field_var
+    -> Types.field_var
+    -> Types.field_var Types.Checked.t
 
   val square :
-       ?label:string
-    -> Checked.field Cvar0.t
-    -> Checked.field Cvar0.t Types.Checked.t
+    ?label:string -> Types.field_var -> Types.field_var Types.Checked.t
 
   val div :
        ?label:string
-    -> Checked.field Cvar0.t
-    -> Checked.field Cvar0.t
-    -> Checked.field Cvar0.t Types.Checked.t
+    -> Types.field_var
+    -> Types.field_var
+    -> Types.field_var Types.Checked.t
 
-  val inv :
-       ?label:string
-    -> Checked.field Cvar0.t
-    -> Checked.field Cvar0.t Types.Checked.t
+  val inv : ?label:string -> Types.field_var -> Types.field_var Types.Checked.t
 
-  val assert_non_zero : Checked.field Cvar0.t -> unit Types.Checked.t
+  val assert_non_zero : Types.field_var -> unit Types.Checked.t
 
-  val equal_vars :
-    Checked.field Cvar0.t -> (Checked.field * Checked.field) As_prover.t
+  val equal_vars : Types.field_var -> (Types.field * Types.field) As_prover.t
 
   val equal_constraints :
-       Checked.field Cvar0.t
-    -> Checked.field Cvar0.t
-    -> Checked.field Cvar0.t
+       Types.field_var
+    -> Types.field_var
+    -> Types.field_var
     -> unit Types.Checked.t
 end

From 4f954e9d69dfaf69db990f0f12836e3b8189b7df Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Thu, 2 Jan 2025 17:36:22 +0000
Subject: [PATCH 03/13] Remove use of Cvar.t constructors

---
 src/base/checked.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/base/checked.ml b/src/base/checked.ml
index cafc87d8a..a0a15f929 100644
--- a/src/base/checked.ml
+++ b/src/base/checked.ml
@@ -77,8 +77,8 @@ module Make
         bind acc ~f:(fun () -> add_constraint c) )
 
   let assert_equal x y =
-    match (x, y) with
-    | Cvar.Constant x, Cvar.Constant y ->
+    match (Backend.Cvar.to_constant x, Backend.Cvar.to_constant y) with
+    | Some x, Some y ->
         if Backend.Field.equal x y then return ()
         else
           failwithf

From 2d40946738b4df00dde4aeab455a859d52eddcff Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Mon, 6 Jan 2025 13:49:56 +0000
Subject: [PATCH 04/13] Hoist generalized functions

---
 src/base/backend_extended.ml | 10 ----------
 src/base/cvar.ml             | 10 ++++++++++
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml
index c8ec3918c..ef54e046c 100644
--- a/src/base/backend_extended.ml
+++ b/src/base/backend_extended.ml
@@ -197,16 +197,6 @@ module Make (Backend : Backend_intf.S) :
 
   module Cvar = struct
     include Cvar.Make (Field)
-
-    let var_indices t =
-      let _, terms = to_constant_and_terms t in
-      List.map ~f:(fun (_, v) -> v) terms
-
-    let to_constant : t -> Field.t option = function
-      | Constant x ->
-          Some x
-      | _ ->
-          None
   end
 
   module Constraint = Constraint
diff --git a/src/base/cvar.ml b/src/base/cvar.ml
index 7c47f04a5..08c7a400c 100644
--- a/src/base/cvar.ml
+++ b/src/base/cvar.ml
@@ -144,4 +144,14 @@ module Make (Field : Snarky_intf.Field.Extended) = struct
       (List.filter_map (Map.to_alist map) ~f:(fun (i, f) ->
            if Field.(equal f zero) then None
            else Some (Int.to_string i, `String (Field.to_string f)) ) )
+
+  let var_indices t =
+    let _, terms = to_constant_and_terms t in
+    List.map ~f:(fun (_, v) -> v) terms
+
+  let to_constant : t -> Field.t option = function
+    | Constant x ->
+        Some x
+    | _ ->
+        None
 end

From 5676db4941469b20c8f835a1e5cbb95e8615ae50 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Mon, 6 Jan 2025 13:51:25 +0000
Subject: [PATCH 05/13] Hoist Cvar_intf

---
 src/base/backend_extended.ml | 42 ++++--------------------------------
 src/base/backend_intf.ml     | 40 ++++++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+), 38 deletions(-)

diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml
index ef54e046c..e415fe195 100644
--- a/src/base/backend_extended.ml
+++ b/src/base/backend_extended.ml
@@ -20,44 +20,10 @@ module type S = sig
     val to_bignum_bigint : t -> Bignum_bigint.t
   end
 
-  module Cvar : sig
-    type t = Field.t Cvar.t [@@deriving sexp]
-
-    val length : t -> int
-
-    module Unsafe : sig
-      val of_index : int -> t
-    end
-
-    val eval :
-      [ `Return_values_will_be_mutated of int -> Field.t ] -> t -> Field.t
-
-    val constant : Field.t -> t
-
-    val to_constant_and_terms : t -> Field.t option * (Field.t * int) list
-
-    val add : t -> t -> t
-
-    val negate : t -> t
-
-    val scale : t -> Field.t -> t
-
-    val sub : t -> t -> t
-
-    val linear_combination : (Field.t * t) list -> t
-
-    val sum : t list -> t
-
-    val ( + ) : t -> t -> t
-
-    val ( - ) : t -> t -> t
-
-    val ( * ) : Field.t -> t -> t
-
-    val var_indices : t -> int list
-
-    val to_constant : t -> Field.t option
-  end
+  module Cvar :
+    Backend_intf.Cvar_intf
+      with type field := Field.t
+       and type t = Field.t Cvar.t
 
   module Constraint : sig
     type t [@@deriving sexp]
diff --git a/src/base/backend_intf.ml b/src/base/backend_intf.ml
index be47d71b9..6de0de046 100644
--- a/src/base/backend_intf.ml
+++ b/src/base/backend_intf.ml
@@ -1,3 +1,43 @@
+module type Cvar_intf = sig
+  type field
+
+  type t [@@deriving sexp]
+
+  val length : t -> int
+
+  module Unsafe : sig
+    val of_index : int -> t
+  end
+
+  val eval : [ `Return_values_will_be_mutated of int -> field ] -> t -> field
+
+  val constant : field -> t
+
+  val to_constant_and_terms : t -> field option * (field * int) list
+
+  val add : t -> t -> t
+
+  val negate : t -> t
+
+  val scale : t -> field -> t
+
+  val sub : t -> t -> t
+
+  val linear_combination : (field * t) list -> t
+
+  val sum : t list -> t
+
+  val ( + ) : t -> t -> t
+
+  val ( - ) : t -> t -> t
+
+  val ( * ) : field -> t -> t
+
+  val var_indices : t -> int list
+
+  val to_constant : t -> field option
+end
+
 module type S = sig
   module Field : Snarky_intf.Field.S
 

From b1997ff17c091eb2fe31643f5f392737e4d7fbfa Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Mon, 6 Jan 2025 14:11:23 +0000
Subject: [PATCH 06/13] Include Cvar in Backend_intf

---
 src/base/backend_extended.ml |  6 ++----
 src/base/backend_intf.ml     | 14 ++++++++------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/base/backend_extended.ml b/src/base/backend_extended.ml
index e415fe195..38907d0ef 100644
--- a/src/base/backend_extended.ml
+++ b/src/base/backend_extended.ml
@@ -57,6 +57,7 @@ module Make (Backend : Backend_intf.S) :
     with type Field.t = Backend.Field.t
      and type Field.Vector.t = Backend.Field.Vector.t
      and type Bigint.t = Backend.Bigint.t
+     and type Cvar.t = Backend.Cvar.t
      and type R1CS_constraint_system.t = Backend.R1CS_constraint_system.t
      and type Run_state.t = Backend.Run_state.t
      and type Constraint.t = Backend.Constraint.t = struct
@@ -161,10 +162,7 @@ module Make (Backend : Backend_intf.S) :
     let ( / ) = div
   end
 
-  module Cvar = struct
-    include Cvar.Make (Field)
-  end
-
+  module Cvar = Cvar
   module Constraint = Constraint
   module R1CS_constraint_system = R1CS_constraint_system
   module Run_state = Run_state
diff --git a/src/base/backend_intf.ml b/src/base/backend_intf.ml
index 6de0de046..8dfcfccb3 100644
--- a/src/base/backend_intf.ml
+++ b/src/base/backend_intf.ml
@@ -45,20 +45,22 @@ module type S = sig
 
   val field_size : Bigint.t
 
+  module Cvar : Cvar_intf with type field := Field.t and type t = Field.t Cvar.t
+
   module Constraint : sig
     type t [@@deriving sexp]
 
-    val boolean : Field.t Cvar.t -> t
+    val boolean : Cvar.t -> t
 
-    val equal : Field.t Cvar.t -> Field.t Cvar.t -> t
+    val equal : Cvar.t -> Cvar.t -> t
 
-    val r1cs : Field.t Cvar.t -> Field.t Cvar.t -> Field.t Cvar.t -> t
+    val r1cs : Cvar.t -> Cvar.t -> Cvar.t -> t
 
-    val square : Field.t Cvar.t -> Field.t Cvar.t -> t
+    val square : Cvar.t -> Cvar.t -> t
 
-    val eval : t -> (Field.t Cvar.t -> Field.t) -> bool
+    val eval : t -> (Cvar.t -> Field.t) -> bool
 
-    val log_constraint : t -> (Field.t Cvar.t -> Field.t) -> string
+    val log_constraint : t -> (Cvar.t -> Field.t) -> string
   end
 
   module R1CS_constraint_system :

From 4a7dff5cddfea17530aaf784a089a75dc7c272f1 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Mon, 6 Jan 2025 14:27:26 +0000
Subject: [PATCH 07/13] Explicitly use Cvar.t for field_var alias

---
 src/base/checked_runner.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml
index b78048431..1a9f27aac 100644
--- a/src/base/checked_runner.ml
+++ b/src/base/checked_runner.ml
@@ -15,7 +15,7 @@ end
 module Simple_types (Backend : Backend_extended.S) = Types.Make_types (struct
   type field = Backend.Field.t
 
-  type field_var = field Cvar.t
+  type field_var = Backend.Cvar.t
 
   type 'a checked = 'a T(Backend).t
 

From 918ed8a55b68edf162b5a710b02169ff6118d317 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Mon, 6 Jan 2025 14:35:35 +0000
Subject: [PATCH 08/13] Relax As_prover0 interface

---
 src/base/as_prover0.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/base/as_prover0.ml b/src/base/as_prover0.ml
index f5d47da95..553631d93 100644
--- a/src/base/as_prover0.ml
+++ b/src/base/as_prover0.ml
@@ -4,12 +4,15 @@ module Make (Backend : sig
   module Field : sig
     type t
   end
+
+  module Cvar : sig
+    type t
+  end
 end)
 (Types : Types.Types
            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) =
+            and type field_var = Backend.Cvar.t
+            and type 'a As_prover.t = (Backend.Cvar.t -> Backend.Field.t) -> 'a) =
 struct
   type 'a t = 'a Types.As_prover.t
 

From 573a7b3e284b824161ebd1282c73ca4c0f577396 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Mon, 6 Jan 2025 14:40:30 +0000
Subject: [PATCH 09/13] Use Backend.Cvar methods in Utils

---
 src/base/utils.ml | 35 +++++++++++++++++------------------
 1 file changed, 17 insertions(+), 18 deletions(-)

diff --git a/src/base/utils.ml b/src/base/utils.ml
index 1e4ab67e3..08ccb879a 100644
--- a/src/base/utils.ml
+++ b/src/base/utils.ml
@@ -1,5 +1,4 @@
 open Core_kernel
-module Cvar0 = Cvar
 module Runner = Checked_runner
 
 let set_eval_constraints b = Runner.eval_constraints := b
@@ -60,12 +59,12 @@ struct
 
   let constant (Typ typ : _ Typ.t) x =
     let fields, aux = typ.value_to_fields x in
-    let field_vars = Array.map fields ~f:(fun x -> Cvar0.Constant x) in
+    let field_vars = Array.map fields ~f:(fun x -> Cvar.constant x) in
     typ.var_of_fields (field_vars, aux)
 
   let equal (x : Cvar.t) (y : Cvar.t) : Cvar.t Boolean.t Checked.t =
-    match (x, y) with
-    | Constant x, Constant y ->
+    match (Cvar.to_constant x, Cvar.to_constant y) with
+    | Some x, Some y ->
         Checked.return
           (Boolean.Unsafe.create
              (Cvar.constant
@@ -79,12 +78,12 @@ struct
         Boolean.Unsafe.create r
 
   let mul ?(label = "Checked.mul") (x : Cvar.t) (y : Cvar.t) =
-    match (x, y) with
-    | Constant x, Constant y ->
+    match (Cvar.to_constant x, Cvar.to_constant y) with
+    | Some x, Some y ->
         return (Cvar.constant (Field.mul x y))
-    | Constant x, _ ->
+    | Some x, _ ->
         return (Cvar.scale y x)
-    | _, Constant y ->
+    | _, Some y ->
         return (Cvar.scale x y)
     | _, _ ->
         with_label label (fun () ->
@@ -97,8 +96,8 @@ struct
             z )
 
   let square ?(label = "Checked.square") (x : Cvar.t) =
-    match x with
-    | Constant x ->
+    match Cvar.to_constant x with
+    | Some x ->
         return (Cvar.constant (Field.square x))
     | _ ->
         with_label label (fun () ->
@@ -114,8 +113,8 @@ struct
      put a bogus value for the inverse to make the constraint system unsat if
      x is zero. *)
   let inv ?(label = "Checked.inv") (x : Cvar.t) =
-    match x with
-    | Constant x ->
+    match Cvar.to_constant x with
+    | Some x ->
         return (Cvar.constant (Field.inv x))
     | _ ->
         with_label label (fun () ->
@@ -132,8 +131,8 @@ struct
             x_inv )
 
   let div ?(label = "Checked.div") (x : Cvar.t) (y : Cvar.t) =
-    match (x, y) with
-    | Constant x, Constant y ->
+    match (Cvar.to_constant x, Cvar.to_constant y) with
+    | Some x, Some y ->
         return (Cvar.constant (Field.( / ) x y))
     | _ ->
         with_label label (fun () ->
@@ -148,12 +147,12 @@ struct
        r - e = b (t - e)
     *)
     let b = (b :> Cvar.t) in
-    match b with
-    | Constant b ->
+    match Cvar.to_constant b with
+    | Some b ->
         if Field.(equal b one) then return then_ else return else_
     | _ -> (
-        match (then_, else_) with
-        | Constant t, Constant e ->
+        match (Cvar.to_constant then_, Cvar.to_constant else_) with
+        | Some t, Some e ->
             return Cvar.((t * b) + (e * (constant Field0.one - b)))
         | _, _ ->
             let%bind r =

From 53232ba074d3636f85e1a5300a1353dc701ca063 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Mon, 6 Jan 2025 14:47:11 +0000
Subject: [PATCH 10/13] Use Cvar helper functions instead of constructors in
 Snark0

---
 src/base/snark0.ml | 27 +++++++++++++--------------
 1 file changed, 13 insertions(+), 14 deletions(-)

diff --git a/src/base/snark0.ml b/src/base/snark0.ml
index 256e72d71..4a36ef448 100644
--- a/src/base/snark0.ml
+++ b/src/base/snark0.ml
@@ -1,5 +1,4 @@
 open Core_kernel
-module Cvar0 = Cvar
 module Bignum_bigint = Bigint
 
 exception Runtime_error of string list * exn * string
@@ -50,7 +49,7 @@ struct
 
   let constant (Typ typ : _ Typ.t) x =
     let fields, aux = typ.value_to_fields x in
-    let field_vars = Array.map fields ~f:(fun x -> Cvar0.Constant x) in
+    let field_vars = Array.map fields ~f:(fun x -> Cvar.constant x) in
     typ.var_of_fields (field_vars, aux)
 
   module As_prover = struct
@@ -153,11 +152,11 @@ struct
           | [] ->
               res
           | v :: vs ->
-              go Cvar0.(Add (v, Scale (two, res))) vs
+              go Cvar.(add v (Cvar.scale res two)) vs
         in
         match List.rev (vars :> Cvar.t list) with
         | [] ->
-            Cvar0.Constant Field.zero
+            Cvar.constant Field.zero
         | v :: vs ->
             go v vs
 
@@ -221,8 +220,8 @@ struct
       let inv x = Checked.inv ~label:"Field.Checked.inv" x
 
       let sqrt (x : Cvar.t) : Cvar.t Checked.t =
-        match x with
-        | Constant x ->
+        match Cvar.to_constant x with
+        | Some x ->
             Checked.return (Cvar.constant (Field.sqrt x))
         | _ ->
             let open Checked in
@@ -353,8 +352,8 @@ struct
 
       module Assert = struct
         let lt ~bit_length (x : Cvar.t) (y : Cvar.t) =
-          match (x, y) with
-          | Constant x, Constant y ->
+          match (Cvar.to_constant x, Cvar.to_constant y) with
+          | Some x, Some y ->
               assert (Field.compare x y < 0) ;
               Checked.return ()
           | _ ->
@@ -364,8 +363,8 @@ struct
               Boolean.Assert.is_true less
 
         let lte ~bit_length (x : Cvar.t) (y : Cvar.t) =
-          match (x, y) with
-          | Constant x, Constant y ->
+          match (Cvar.to_constant x, Cvar.to_constant y) with
+          | Some x, Some y ->
               assert (Field.compare x y <= 0) ;
               Checked.return ()
           | _ ->
@@ -379,8 +378,8 @@ struct
         let gte ~bit_length x y = lte ~bit_length y x
 
         let non_zero (v : Cvar.t) =
-          match v with
-          | Constant v ->
+          match Cvar.to_constant v with
+          | Some v ->
               if Field.(equal zero v) then
                 failwithf "assert_non_zero: failed on constant %s"
                   (Field.to_string v) () ;
@@ -391,8 +390,8 @@ struct
         let equal x y = Checked.assert_equal x y
 
         let not_equal (x : t) (y : t) =
-          match (x, y) with
-          | Constant x, Constant y ->
+          match (Cvar.to_constant x, Cvar.to_constant y) with
+          | Some x, Some y ->
               if Field.(equal x y) then
                 failwithf "not_equal: failed on constants %s and %s"
                   (Field.to_string x) (Field.to_string y) () ;

From c3b1c46b2cd74572c672aed07e3a8960cc46faaa Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Mon, 6 Jan 2025 14:53:00 +0000
Subject: [PATCH 11/13] Move misplaced comment

---
 src/base/snark_intf.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml
index 68bd90de8..46ebf01cf 100644
--- a/src/base/snark_intf.ml
+++ b/src/base/snark_intf.ml
@@ -298,9 +298,9 @@ end
 module type Field_var_intf = sig
   type field
 
+  (** The type that stores booleans as R1CS variables. *)
   type boolean_var
 
-  (** The type that stores booleans as R1CS variables. *)
   type t = field Cvar.t
 
   (** For debug purposes *)

From b9f1a2cb36285c6581756075ee28df2ca6a30b97 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Mon, 6 Jan 2025 15:25:20 +0000
Subject: [PATCH 12/13] Introduce field_var in Snark_intf

---
 src/base/snark0.ml     |  4 ++++
 src/base/snark_intf.ml | 41 +++++++++++++++++++++++++----------------
 2 files changed, 29 insertions(+), 16 deletions(-)

diff --git a/src/base/snark0.ml b/src/base/snark0.ml
index 4a36ef448..ad357a0da 100644
--- a/src/base/snark0.ml
+++ b/src/base/snark0.ml
@@ -25,6 +25,8 @@ module Make_basic
 struct
   open Backend
 
+  type field_var = Cvar.t
+
   module Typ = struct
     include Types.Typ
     module T = Typ.Make (Types) (Checked)
@@ -749,6 +751,8 @@ module Run = struct
 
     type field = Snark.field
 
+    type field_var = Snark.field_var
+
     module Bigint = Snark.Bigint
     module Constraint = Snark.Constraint
 
diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml
index 46ebf01cf..895d39190 100644
--- a/src/base/snark_intf.ml
+++ b/src/base/snark_intf.ml
@@ -301,7 +301,7 @@ module type Field_var_intf = sig
   (** The type that stores booleans as R1CS variables. *)
   type boolean_var
 
-  type t = field Cvar.t
+  type t
 
   (** For debug purposes *)
   val length : t -> int
@@ -545,6 +545,9 @@ module type Basic = sig
   (** The finite field over which the R1CS operates. *)
   type field
 
+  (** The variable type over which the R1CS operates. *)
+  type field_var = field Cvar.t
+
   (** The rank-1 constraint system used by this instance. See
       {!module:Backend_intf.S.R1CS_constraint_system}. *)
   module R1CS_constraint_system : sig
@@ -563,9 +566,7 @@ module type Basic = sig
 
   (** Rank-1 constraints over {!type:Var.t}s. *)
   module rec Constraint :
-    (Constraint_intf
-      with type field := Field.t
-       and type field_var := Field.Var.t)
+    (Constraint_intf with type field := field and type field_var := field_var)
 
   (** The data specification for checked computations. *)
 
@@ -573,8 +574,8 @@ module type Basic = sig
   and Typ : sig
     include
       Typ_intf
-        with type field := Field.t
-         and type field_var := Field.Var.t
+        with type field := field
+         and type field_var := field_var
          and type _ checked_unit := unit Checked.t
   end
 
@@ -586,7 +587,7 @@ module type Basic = sig
   and Boolean :
     (Boolean_intf
       with type var = Field.Var.t Boolean0.t
-       and type field_var := Field.Var.t
+       and type field_var := field_var
        and type 'a checked := 'a Checked.t
        and type ('var, 'value) typ := ('var, 'value) Typ.t)
 
@@ -676,11 +677,12 @@ let multiply3 (x : Field.Var.t) (y : Field.Var.t) (z : Field.Var.t)
       Field_var_intf
         with type field := field
          and type boolean_var := Boolean.var
+         and type t = field_var
 
     module Checked :
       Field_checked_intf
         with type field := field
-         and type field_var := Var.t
+         and type field_var := field_var
          and type scale_field := field
         (* TODO: harmonise this *)
          and type 'a checked := 'a Checked.t
@@ -1054,7 +1056,7 @@ module type S = sig
     Number_intf.S
       with type 'a checked := 'a Checked.t
        and type field := field
-       and type field_var := Field.Var.t
+       and type field_var := field_var
        and type bool_var := Boolean.var
 
   module Enumerable (M : sig
@@ -1087,6 +1089,9 @@ module type Run_basic = sig
   (** The finite field over which the R1CS operates. *)
   type field
 
+  (** The variable type over which the R1CS operates. *)
+  type field_var = field Cvar.t
+
   module Bigint : sig
     include Snarky_intf.Bigint_intf.Extended with type field := field
 
@@ -1099,13 +1104,13 @@ module type Run_basic = sig
   module rec Constraint :
     (Constraint_intf
       with type field := Field.Constant.t
-       and type field_var := Field.t)
+       and type field_var := field_var)
 
   (** Mappings from OCaml types to R1CS variables and constraints. *)
   and Typ :
     (Typ_intf
       with type field := Internal_Basic.field
-       and type field_var := Internal_Basic.Field.Var.t
+       and type field_var := Internal_Basic.field_var
        and type _ checked_unit := unit Internal_Basic.Checked.t
        and type ('var, 'value, 'aux) typ' =
         ('var, 'value, 'aux) Internal_Basic.Typ.typ'
@@ -1120,7 +1125,7 @@ module type Run_basic = sig
   and Boolean :
     (Boolean_intf
       with type var = Field.t Boolean0.t
-       and type field_var := Field.t
+       and type field_var := field_var
        and type 'a checked := 'a
        and type ('var, 'value) typ := ('var, 'value) Typ.t)
 
@@ -1153,11 +1158,12 @@ module type Run_basic = sig
       Field_var_intf
         with type field := field
          and type boolean_var := Boolean.var
+         and type t = field_var
 
     include
       Field_checked_intf
         with type field := field
-         and type field_var := t
+         and type field_var := field_var
          and type scale_field := t
         (* TODO: harmonise this *)
          and type 'a checked := 'a
@@ -1211,7 +1217,10 @@ module type Run_basic = sig
   end
 
   and Internal_Basic :
-    (Basic with type field = field and type Constraint.t = Constraint.t)
+    (Basic
+      with type field = field
+       and type field_var = field_var
+       and type Constraint.t = Constraint.t)
 
   module Bitstring_checked : sig
     type t = Boolean.var list
@@ -1419,7 +1428,7 @@ module type Run = sig
   module Number :
     Number_intf.Run
       with type field := field
-       and type field_var := Field.t
+       and type field_var := field_var
        and type bool_var := Boolean.var
 
   module Enumerable (M : sig
@@ -1428,6 +1437,6 @@ module type Run = sig
     Enumerable_intf.Run
       with type ('a, 'b) typ := ('a, 'b) Typ.t
        and type bool_var := Boolean.var
-       and type var = Field.t
+       and type var = field_var
        and type t := M.t
 end

From a608ed9e5375f130a4c786f8e00b00b7ab7fd90f Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
Date: Tue, 7 Jan 2025 14:11:37 +0000
Subject: [PATCH 13/13] Generalize over field_var type

---
 snarky_integer/integer.ml  | 53 +++++++++++++++-----------------
 snarky_integer/integer.mli | 63 ++++++++++++++++++++++----------------
 snarky_integer/util.ml     |  4 +--
 src/base/snark0.ml         |  7 +++--
 src/base/snark0.mli        | 11 +++++--
 src/base/snark_intf.ml     |  4 +--
 6 files changed, 79 insertions(+), 63 deletions(-)

diff --git a/snarky_integer/integer.ml b/snarky_integer/integer.ml
index 97519ebb0..a5323849b 100644
--- a/snarky_integer/integer.ml
+++ b/snarky_integer/integer.ml
@@ -12,7 +12,7 @@ module Interval = struct
 
   let iter t ~f = match t with Constant x -> f x | Less_than x -> f x
 
-  let check (type f) ~m:((module M) : f m) t =
+  let check (type f v) ~m:((module M) : (f, v) m) t =
     iter t ~f:(fun x -> assert (B.(x < M.Field.size))) ;
     t
 
@@ -113,18 +113,15 @@ module Interval = struct
 end
 
 (* TODO: Use <= instead of < for the upper bound *)
-type 'f t =
-  { value : 'f Cvar.t
-  ; interval : Interval.t
-  ; mutable bits : 'f Cvar.t Boolean.t list option
-  }
+type ('f, 'v) t =
+  { value : 'v; interval : Interval.t; mutable bits : 'v Boolean.t list option }
 
 let create ~value ~upper_bound =
   { value; interval = Less_than upper_bound; bits = None }
 
 let to_field t = t.value
 
-let constant (type f) ?length ~m:((module M) as m : f m) x =
+let constant (type f v) ?length ~m:((module M) as m : (f, v) m) x =
   let open M in
   assert (B.( < ) x Field.size) ;
   let upper_bound = B.(one + x) in
@@ -145,7 +142,7 @@ let constant (type f) ?length ~m:((module M) as m : f m) x =
              constant Boolean.typ B.(shift_right x i land one = one) ) )
   }
 
-let shift_left (type f) ~m:((module M) as m : f m) t k =
+let shift_left (type f v) ~m:((module M) as m : (f, v) m) t k =
   let open M in
   let two_to_k = B.(one lsl k) in
   { value = Field.(constant (bigint_to_field ~m two_to_k) * t.value)
@@ -155,7 +152,7 @@ let shift_left (type f) ~m:((module M) as m : f m) t k =
           List.init k ~f:(fun _ -> Boolean.false_) @ bs )
   }
 
-let of_bits (type f) ~m:((module M) : f m) bs =
+let of_bits (type f v) ~m:((module M) : (f, v) m) bs =
   let bs = Bitstring.Lsb_first.to_list bs in
   { value = M.Field.project bs
   ; interval = Less_than B.(one lsl List.length bs)
@@ -167,7 +164,7 @@ let of_bits (type f) ~m:((module M) : f m) bs =
     a = q * b + r
     r < b
 *)
-let div_mod (type f) ~m:((module M) as m : f m) a b =
+let div_mod (type f v) ~m:((module M) as m : (f, v) m) a b =
   let open M in
   (* Guess (q, r) *)
   let q, r =
@@ -198,7 +195,7 @@ let div_mod (type f) ~m:((module M) as m : f m) a b =
     }
   , { value = r; interval = b.interval; bits = Some r_bits } )
 
-let subtract_unpacking (type f) ~m:((module M) : f m) a b =
+let subtract_unpacking (type f v) ~m:((module M) : (f, v) m) a b =
   M.with_label "Integer.subtract_unpacking" (fun () ->
       assert (Interval.gte a.interval b.interval) ;
       let value = M.Field.(sub a.value b.value) in
@@ -207,15 +204,15 @@ let subtract_unpacking (type f) ~m:((module M) : f m) a b =
       let bits = M.Field.unpack value ~length in
       { value; interval = a.interval; bits = Some bits } )
 
-let add (type f) ~m:((module M) as m : f m) a b =
+let add (type f v) ~m:((module M) as m : (f, v) m) a b =
   let interval = Interval.(add ~m a.interval b.interval) in
   { value = M.Field.(a.value + b.value); interval; bits = None }
 
-let mul (type f) ~m:((module M) as m : f m) a b =
+let mul (type f v) ~m:((module M) as m : (f, v) m) a b =
   let interval = Interval.(mul ~m a.interval b.interval) in
   { value = M.Field.(a.value * b.value); interval; bits = None }
 
-let to_bits ?length (type f) ~m:((module M) : f m) t =
+let to_bits ?length (type f v) ~m:((module M) : (f, v) m) t =
   match t.bits with
   | Some bs -> (
       let bs = Bitstring.Lsb_first.of_list bs in
@@ -239,7 +236,7 @@ let to_bits_exn t = Bitstring.Lsb_first.of_list (Option.value_exn t.bits)
 
 let to_bits_opt t = Option.map ~f:Bitstring.Lsb_first.of_list t.bits
 
-let min (type f) ~m:((module M) : f m) (a : f t) (b : f t) =
+let min (type f v) ~m:((module M) : (f, v) m) (a : (f, v) t) (b : (f, v) t) =
   let open M in
   let bit_length =
     Int.max (Interval.bits_needed a.interval) (Interval.bits_needed b.interval)
@@ -250,48 +247,48 @@ let min (type f) ~m:((module M) : f m) (a : f t) (b : f t) =
   ; bits = None
   }
 
-let if_ (type f) ~m:((module M) : f m) cond ~then_ ~else_ =
+let if_ (type f v) ~m:((module M) : (f, v) m) cond ~then_ ~else_ =
   { value = M.Field.if_ cond ~then_:then_.value ~else_:else_.value
   ; interval = Interval.lub then_.interval else_.interval
   ; bits = None
   }
 
-let succ_if (type f) ~m:((module M) as m : f m) t (cond : f Cvar.t Boolean.t) =
+let succ_if (type f v) ~m:((module M) as m : (f, v) m) t (cond : v Boolean.t) =
   let open M in
   { value = Field.(add (cond :> t) t.value)
   ; interval = Interval.(lub t.interval (succ ~m t.interval))
   ; bits = None
   }
 
-let succ (type f) ~m:((module M) as m : f m) t =
+let succ (type f v) ~m:((module M) as m : (f, v) m) t =
   let open M in
   { value = Field.(add one t.value)
   ; interval = Interval.succ ~m t.interval
   ; bits = None
   }
 
-let equal (type f) ~m:((module M) : f m) a b = M.Field.equal a.value b.value
+let equal (type f v) ~m:((module M) : (f, v) m) a b =
+  M.Field.equal a.value b.value
 
 let max_bits a b =
   Int.max (Interval.bits_needed a.interval) (Interval.bits_needed b.interval)
 
-let lt (type f) ~m:((module M) : f m) a b =
+let lt (type f v) ~m:((module M) : (f, v) m) a b =
   (M.Field.compare ~bit_length:(max_bits a b) a.value b.value).less
 
-let lte (type f) ~m:((module M) : f m) a b =
+let lte (type f v) ~m:((module M) : (f, v) m) a b =
   (M.Field.compare ~bit_length:(max_bits a b) a.value b.value).less_or_equal
 
-let gte (type f) ~m:((module M) as m : f m) a b = M.Boolean.not (lt ~m a b)
+let gte (type f v) ~m:((module M) as m : (f, v) m) a b =
+  M.Boolean.not (lt ~m a b)
 
-let gt (type f) ~m:((module M) as m : f m) a b = M.Boolean.not (lte ~m a b)
+let gt (type f v) ~m:((module M) as m : (f, v) m) a b =
+  M.Boolean.not (lte ~m a b)
 
-let subtract_unpacking_or_zero (type f) ~m:((module M) as m : f m) a b =
+let subtract_unpacking_or_zero (type f v) ~m:((module M) as m : (f, v) m) a b =
   let flag = lt ~m a b in
   ( `Underflow flag
-  , { value =
-        M.Field.mul
-          (M.Field.sub a.value b.value)
-          (M.Boolean.not flag :> f Cvar.t)
+  , { value = M.Field.mul (M.Field.sub a.value b.value) (M.Boolean.not flag :> v)
     ; interval = a.interval
     ; bits = None
     } )
diff --git a/snarky_integer/integer.mli b/snarky_integer/integer.mli
index 58b6c49f4..4414f18b6 100644
--- a/snarky_integer/integer.mli
+++ b/snarky_integer/integer.mli
@@ -18,31 +18,28 @@ module Interval : sig
   type t = Constant of B.t | Less_than of B.t
 end
 
-type 'f t =
-  { value : 'f Cvar.t
-  ; interval : Interval.t
-  ; mutable bits : 'f Cvar.t Boolean.t list option
-  }
+type ('f, 'v) t =
+  { value : 'v; interval : Interval.t; mutable bits : 'v Boolean.t list option }
 
 (** Create an value representing the given constant value.
 
     The bit representation of the constant is cached, and is padded to [length]
     when given.
 *)
-val constant : ?length:int -> m:'f m -> Bigint.t -> 'f t
+val constant : ?length:int -> m:('f, 'v) m -> Bigint.t -> ('f, 'v) t
 
 (** [shift_left ~m x k] is equivalent to multiplying [x] by [2^k].
 
     The result has a cached bit representation whenever the given [x] had a
     cached bit representation.
 *)
-val shift_left : m:'f m -> 'f t -> int -> 'f t
+val shift_left : m:('f, 'v) m -> ('f, 'v) t -> int -> ('f, 'v) t
 
 (** Create a value from the given bit string.
 
     The given bit representation is cached.
 *)
-val of_bits : m:'f m -> 'f Cvar.t Boolean.t Bitstring.Lsb_first.t -> 'f t
+val of_bits : m:('f, 'v) m -> 'v Boolean.t Bitstring.Lsb_first.t -> ('f, 'v) t
 
 (** Compute the bit representation of the given integer.
 
@@ -51,17 +48,20 @@ val of_bits : m:'f m -> 'f Cvar.t Boolean.t Bitstring.Lsb_first.t -> 'f t
     value is updated to include the cache.
 *)
 val to_bits :
-  ?length:int -> m:'f m -> 'f t -> 'f Cvar.t Boolean.t Bitstring.Lsb_first.t
+     ?length:int
+  -> m:('f, 'v) m
+  -> ('f, 'v) t
+  -> 'v Boolean.t Bitstring.Lsb_first.t
 
 (** Return the cached bit representation, or raise an exception if the bit
     representation has not been cached.
 *)
-val to_bits_exn : 'f t -> 'f Cvar.t Boolean.t Bitstring.Lsb_first.t
+val to_bits_exn : ('f, 'v) t -> 'v Boolean.t Bitstring.Lsb_first.t
 
 (** Returns [Some bs] for [bs] the cached bit representation, or [None] if the
     bit representation has not been cached.
 *)
-val to_bits_opt : 'f t -> 'f Cvar.t Boolean.t Bitstring.Lsb_first.t option
+val to_bits_opt : ('f, 'v) t -> 'v Boolean.t Bitstring.Lsb_first.t option
 
 (** [div_mod ~m a b = (q, r)] such that [a = q * b + r] and [r < b].
 
@@ -69,54 +69,60 @@ val to_bits_opt : 'f t -> 'f Cvar.t Boolean.t Bitstring.Lsb_first.t option
 
     NOTE: This uses approximately [log2(a) + 2 * log2(b)] constraints.
 *)
-val div_mod : m:'f m -> 'f t -> 'f t -> 'f t * 'f t
+val div_mod :
+  m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t -> ('f, 'v) t * ('f, 'v) t
 
-val to_field : 'f t -> 'f Cvar.t
+val to_field : ('f, 'v) t -> 'v
 
-val create : value:'f Cvar.t -> upper_bound:Bigint.t -> 'f t
+val create : value:'v -> upper_bound:Bigint.t -> ('f, 'v) t
 
 (** [min ~m x y] returns a value equal the lesser of [x] and [y].
 
     The result does not carry a cached bit representation.
 *)
-val min : m:'f m -> 'f t -> 'f t -> 'f t
+val min : m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t -> ('f, 'v) t
 
-val if_ : m:'f m -> 'f Cvar.t Boolean.t -> then_:'f t -> else_:'f t -> 'f t
+val if_ :
+     m:('f, 'v) m
+  -> 'v Boolean.t
+  -> then_:('f, 'v) t
+  -> else_:('f, 'v) t
+  -> ('f, 'v) t
 
 (** [succ ~m x] computes the successor [x+1] of [x].
 
     The result does not carry a cached bit representation.
 *)
-val succ : m:'f m -> 'f t -> 'f t
+val succ : m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t
 
 (** [succ_if ~m x b] computes the integer [x+1] if [b] is [true], or [x]
     otherwise.
 
     The result does not carry a cached bit representation.
 *)
-val succ_if : m:'f m -> 'f t -> 'f Cvar.t Boolean.t -> 'f t
+val succ_if : m:('f, 'v) m -> ('f, 'v) t -> 'v Boolean.t -> ('f, 'v) t
 
-val equal : m:'f m -> 'f t -> 'f t -> 'f Cvar.t Boolean.t
+val equal : m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t -> 'v Boolean.t
 
-val lt : m:'f m -> 'f t -> 'f t -> 'f Cvar.t Boolean.t
+val lt : m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t -> 'v Boolean.t
 
-val lte : m:'f m -> 'f t -> 'f t -> 'f Cvar.t Boolean.t
+val lte : m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t -> 'v Boolean.t
 
-val gt : m:'f m -> 'f t -> 'f t -> 'f Cvar.t Boolean.t
+val gt : m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t -> 'v Boolean.t
 
-val gte : m:'f m -> 'f t -> 'f t -> 'f Cvar.t Boolean.t
+val gte : m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t -> 'v Boolean.t
 
 (** [add ~m x y] computes [x + y].
 
     The result does not carry a cached bit representation.
 *)
-val add : m:'f m -> 'f t -> 'f t -> 'f t
+val add : m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t -> ('f, 'v) t
 
 (** [mul ~m x y] computes [x * y].
 
     The result does not carry a cached bit representation.
 *)
-val mul : m:'f m -> 'f t -> 'f t -> 'f t
+val mul : m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t -> ('f, 'v) t
 
 (** [subtract_unpacking ~m x y] computes [x - y].
 
@@ -125,7 +131,7 @@ val mul : m:'f m -> 'f t -> 'f t -> 'f t
 
     NOTE: This uses approximately [log2(x)] constraints.
 *)
-val subtract_unpacking : m:'f m -> 'f t -> 'f t -> 'f t
+val subtract_unpacking : m:('f, 'v) m -> ('f, 'v) t -> ('f, 'v) t -> ('f, 'v) t
 
 (** [subtract_unpacking_or_zero ~m x y] computes [x - y].
 
@@ -139,4 +145,7 @@ val subtract_unpacking : m:'f m -> 'f t -> 'f t -> 'f t
     NOTE: This uses approximately [log2(x)] constraints.
 *)
 val subtract_unpacking_or_zero :
-  m:'f m -> 'f t -> 'f t -> [ `Underflow of 'f Cvar.t Boolean.t ] * 'f t
+     m:('f, 'v) m
+  -> ('f, 'v) t
+  -> ('f, 'v) t
+  -> [ `Underflow of 'v Boolean.t ] * ('f, 'v) t
diff --git a/snarky_integer/util.ml b/snarky_integer/util.ml
index 99d641288..64725e7ff 100644
--- a/snarky_integer/util.ml
+++ b/snarky_integer/util.ml
@@ -3,10 +3,10 @@ open Snarky_backendless
 open Snark
 module B = Bigint
 
-let bigint_to_field (type f) ~m:((module M) : f m) =
+let bigint_to_field (type f v) ~m:((module M) : (f, v) m) =
   let open M in
   Fn.compose Bigint.to_field Bigint.of_bignum_bigint
 
-let bigint_of_field (type f) ~m:((module M) : f m) =
+let bigint_of_field (type f v) ~m:((module M) : (f, v) m) =
   let open M in
   Fn.compose Bigint.to_bignum_bigint Bigint.of_field
diff --git a/src/base/snark0.ml b/src/base/snark0.ml
index ad357a0da..6f64ccb1c 100644
--- a/src/base/snark0.ml
+++ b/src/base/snark0.ml
@@ -1566,8 +1566,11 @@ module Run = struct
   end
 end
 
-type 'field m = (module Snark_intf.Run with type field = 'field)
+type ('field, 'field_var) m =
+  (module Snark_intf.Run
+     with type field = 'field
+      and type field_var = 'field_var )
 
 let make (type field) (module Backend : Backend_intf.S with type Field.t = field)
-    : field m =
+    : (field, field Cvar.t) m =
   (module Run.Make (Backend))
diff --git a/src/base/snark0.mli b/src/base/snark0.mli
index 60ef0d937..0ab33b86e 100644
--- a/src/base/snark0.mli
+++ b/src/base/snark0.mli
@@ -22,6 +22,7 @@ exception Runtime_error of string list * exn * string
 module Make (Backend : Backend_intf.S) :
   Snark_intf.S
     with type field = Backend.Field.t
+     and type field_var = Backend.Cvar.t
      and type Bigint.t = Backend.Bigint.t
      and type R1CS_constraint_system.t = Backend.R1CS_constraint_system.t
      and type Field.Vector.t = Backend.Field.Vector.t
@@ -31,12 +32,18 @@ module Run : sig
   module Make (Backend : Backend_intf.S) :
     Snark_intf.Run
       with type field = Backend.Field.t
+       and type field_var = Backend.Cvar.t
        and type Bigint.t = Backend.Bigint.t
        and type R1CS_constraint_system.t = Backend.R1CS_constraint_system.t
        and type Field.Constant.Vector.t = Backend.Field.Vector.t
        and type Constraint.t = Backend.Constraint.t
 end
 
-type 'field m = (module Snark_intf.Run with type field = 'field)
+type ('field, 'field_var) m =
+  (module Snark_intf.Run
+     with type field = 'field
+      and type field_var = 'field_var )
 
-val make : (module Backend_intf.S with type Field.t = 'field) -> 'field m
+val make :
+     (module Backend_intf.S with type Field.t = 'field)
+  -> ('field, 'field Cvar.t) m
diff --git a/src/base/snark_intf.ml b/src/base/snark_intf.ml
index 895d39190..ab212ba90 100644
--- a/src/base/snark_intf.ml
+++ b/src/base/snark_intf.ml
@@ -546,7 +546,7 @@ module type Basic = sig
   type field
 
   (** The variable type over which the R1CS operates. *)
-  type field_var = field Cvar.t
+  type field_var
 
   (** The rank-1 constraint system used by this instance. See
       {!module:Backend_intf.S.R1CS_constraint_system}. *)
@@ -1090,7 +1090,7 @@ module type Run_basic = sig
   type field
 
   (** The variable type over which the R1CS operates. *)
-  type field_var = field Cvar.t
+  type field_var
 
   module Bigint : sig
     include Snarky_intf.Bigint_intf.Extended with type field := field