Generalize pickles and snarky utils over field variable type

src/lib/crypto/kimchi_backend/kimchi_backend.mli

@@ -164,6 +164,7 @@ module Pasta : sig
 
     val field_size : Pasta_bindings.BigInt256.t
 
+    module Cvar = Kimchi_pasta.Pallas_based_plonk.Cvar
     module Verification_key = Kimchi_pasta.Pallas_based_plonk.Verification_key
 
     module R1CS_constraint_system =
@@ -197,6 +198,7 @@ module Pasta : sig
 
     val field_size : Pasta_bindings.BigInt256.t
 
+    module Cvar = Kimchi_pasta.Vesta_based_plonk.Cvar
     module Verification_key = Kimchi_pasta.Vesta_based_plonk.Verification_key
     module R1CS_constraint_system =
       Kimchi_pasta.Vesta_based_plonk.R1CS_constraint_system

src/lib/crypto/kimchi_backend/pasta/kimchi_pasta.ml

@@ -7,6 +7,7 @@ module Pallas_based_plonk = struct
 
   let field_size = Pallas_based_plonk.field_size
 
+  module Cvar = Pallas_based_plonk.Cvar
   module Verification_key = Pallas_based_plonk.Verification_key
   module R1CS_constraint_system = Pallas_based_plonk.R1CS_constraint_system
   module Constraint = R1CS_constraint_system.Constraint
@@ -26,6 +27,7 @@ module Vesta_based_plonk = struct
 
   let field_size = Vesta_based_plonk.field_size
 
+  module Cvar = Vesta_based_plonk.Cvar
   module Verification_key = Vesta_based_plonk.Verification_key
   module R1CS_constraint_system = Vesta_based_plonk.R1CS_constraint_system
   module Constraint = R1CS_constraint_system.Constraint

src/lib/crypto/kimchi_backend/pasta/kimchi_pasta.mli

@@ -7,6 +7,7 @@ module Pallas_based_plonk : sig
 
   val field_size : Pasta_bindings.BigInt256.t
 
+  module Cvar = Pallas_based_plonk.Cvar
   module Verification_key = Pallas_based_plonk.Verification_key
   module R1CS_constraint_system = Pallas_based_plonk.R1CS_constraint_system
   module Constraint = R1CS_constraint_system.Constraint
@@ -26,6 +27,7 @@ module Vesta_based_plonk : sig
 
   val field_size : Pasta_bindings.BigInt256.t
 
+  module Cvar = Vesta_based_plonk.Cvar
   module Verification_key = Vesta_based_plonk.Verification_key
   module R1CS_constraint_system = Vesta_based_plonk.R1CS_constraint_system
   module Constraint = R1CS_constraint_system.Constraint

src/lib/crypto/kimchi_backend/pasta/pallas_based_plonk.ml

@@ -181,4 +181,6 @@ module Oracles = Plonk_dlog_oracles.Make (struct
   end
 end)
 
+module Cvar = Kimchi_pasta_snarky_backend.Pallas_based_plonk.Cvar
+
 module Run_state = Kimchi_pasta_snarky_backend.Pallas_based_plonk.Run_state

src/lib/crypto/kimchi_backend/pasta/vesta_based_plonk.ml

@@ -179,4 +179,6 @@ module Oracles = Plonk_dlog_oracles.Make (struct
   end
 end)
 
+module Cvar = Kimchi_pasta_snarky_backend.Vesta_based_plonk.Cvar
+
 module Run_state = Kimchi_pasta_snarky_backend.Vesta_based_plonk.Run_state

src/lib/crypto/kimchi_pasta_snarky_backend/kimchi_pasta_snarky_backend.ml

@@ -35,6 +35,8 @@ module Vesta_based_plonk = struct
 
   let field_size = Field.size
 
+  module Cvar = Snarky_backendless.Cvar.Make (Field)
+
   module R1CS_constraint_system =
     Plonk_constraint_system.Make
       (Field)
@@ -73,6 +75,8 @@ module Pallas_based_plonk = struct
 
   let field_size = Field.size
 
+  module Cvar = Snarky_backendless.Cvar.Make (Field)
+
   module R1CS_constraint_system =
     Plonk_constraint_system.Make
       (Field)

src/lib/crypto/kimchi_pasta_snarky_backend/plonk_constraint_system.ml

@@ -748,6 +748,7 @@ module type Snark_intf = sig
   include
     Snarky_backendless.Snark_intf.Run
       with type field := field
+       and type field_var = field Snarky_backendless.Cvar.t
        and type Constraint.t =
         (field Snarky_backendless.Cvar.t, field) Plonk_constraint.basic
 end

src/lib/pickles/common.ml

@@ -250,9 +250,11 @@ let ft_comm ~add:( + ) ~scale ~negate
   f_comm + chunked_t_comm
   + negate (scale chunked_t_comm plonk.zeta_to_domain_size)
 
-let combined_evaluation (type f)
-    (module Impl : Snarky_backendless.Snark_intf.Run with type field = f)
-    ~(xi : Impl.Field.t) (without_degree_bound : _ list) =
+let combined_evaluation (type f v)
+    (module Impl : Snarky_backendless.Snark_intf.Run
+      with type field = f
+       and type field_var = v ) ~(xi : Impl.Field.t)
+    (without_degree_bound : _ list) =
   let open Impl in
   let open Field in
   let mul_and_add ~(acc : Field.t) ~(xi : Field.t)

src/lib/pickles/common.mli

@@ -57,14 +57,12 @@ val dlog_pcs_batch :
   -> ('a, 'total, Pickles_types.Nat.z) Pickles_types.Pcs_batch.t
 
 val combined_evaluation :
-     (module Snarky_backendless.Snark_intf.Run with type field = 'f)
-  -> xi:'f Snarky_backendless.Cvar.t
-  -> ( 'f Snarky_backendless.Cvar.t
-     , 'f Snarky_backendless.Cvar.t Snarky_backendless.Snark_intf.Boolean0.t )
-     Pickles_types.Opt.t
-     array
-     list
-  -> 'f Snarky_backendless.Cvar.t
+     (module Snarky_backendless.Snark_intf.Run
+        with type field = 'f
+         and type field_var = 'v )
+  -> xi:'v
+  -> ('v, 'v Snarky_backendless.Boolean.t) Pickles_types.Opt.t array list
+  -> 'v
 
 module Max_degree : sig
   val wrap_log2 : int

src/lib/pickles/composition_types/composition_types.mli

@@ -814,7 +814,7 @@ module Wrap : sig
       (** A layout of the raw data in a statement, which is needed for
           representing it inside the circuit. *)
       val spec :
-           'a Spec.impl
+           ('a, 'v) Spec.impl
         -> ('challenge1, 'challenge2, 'field1, 'field2) Lookup_parameters.t
         -> Opt.Flag.t Plonk_types.Features.t
         -> ( ( 'field1
@@ -1190,13 +1190,10 @@ module Step : sig
       val typ :
            ('b, 'c) Step_impl.Typ.t
         -> assert_16_bits:(Step_impl.Field.t -> unit)
-        -> ( ( Step_impl.Field.Constant.t Limb_vector.Challenge.t
-             , Step_impl.Field.Constant.t Limb_vector.Challenge.t
-               Scalar_challenge.t
+        -> ( ( Step_impl.Field.t
+             , Step_impl.Field.t Scalar_challenge.t
              , 'b
-             , ( Step_impl.Field.Constant.t Limb_vector.Challenge.t
-                 Scalar_challenge.t
-                 Bulletproof_challenge.t
+             , ( Step_impl.Field.t Scalar_challenge.t Bulletproof_challenge.t
                , Backend.Tock.Rounds.n )
                Vector.t
              , Step_impl.Field.t
@@ -1237,13 +1234,10 @@ module Step : sig
          assert_16_bits:(Wrap_impl.Field.t -> unit)
       -> (Opt.Flag.t Plonk_types.Features.t, 'n) Vector.t
       -> ('b, 'a) Wrap_impl.Typ.t
-      -> ( ( ( ( Wrap_impl.Field.Constant.t Limb_vector.Challenge.t
-               , Wrap_impl.Field.Constant.t Limb_vector.Challenge.t
-                 Scalar_challenge.t
+      -> ( ( ( ( Wrap_impl.Field.t
+               , Wrap_impl.Field.t Scalar_challenge.t
                , 'b
-               , ( Wrap_impl.Field.Constant.t Limb_vector.Challenge.t
-                   Scalar_challenge.t
-                   Bulletproof_challenge.t
+               , ( Wrap_impl.Field.t Scalar_challenge.t Bulletproof_challenge.t
                  , Backend.Tock.Rounds.n )
                  Vector.t
                , Wrap_impl.Field.t

src/lib/pickles/composition_types/spec.ml

@@ -4,7 +4,10 @@ open Pickles_types
 open Hlist
 module Sc = Kimchi_backend_common.Scalar_challenge
 
-type 'f impl = (module Snarky_backendless.Snark_intf.Run with type field = 'f)
+type ('f, 'v) impl =
+  (module Snarky_backendless.Snark_intf.Run
+     with type field = 'f
+      and type field_var = 'v )
 
 module type Branch_data_checked = sig
   type field_var
@@ -199,8 +202,9 @@ struct
   end
 end
 
-let pack_basic (type field other_field other_field_var branch_data_var)
-    ((module Impl) : field impl)
+let pack_basic
+    (type field field_var other_field other_field_var branch_data_var)
+    ((module Impl) : (field, field_var) impl)
     ((module Branch_data_checked) : (branch_data_var, Impl.Field.t) branch_data)
     =
   let open Impl in
@@ -235,7 +239,7 @@ let pack_basic (type field other_field other_field_var branch_data_var)
   in
   { pack }
 
-let pack (type f) ((module Impl) as impl : f impl) branch_data t =
+let pack (type f v) ((module Impl) as impl : (f, v) impl) branch_data t =
   let open Impl in
   pack
     (pack_basic impl branch_data)
@@ -381,10 +385,7 @@ struct
             let (Typ typ) = typ t is_boolean spec in
             let constant_var =
               let fields, aux = typ.value_to_fields x in
-              let fields =
-                Array.map fields ~f:(fun x ->
-                    Snarky_backendless.Cvar.Constant x )
-              in
+              let fields = Array.map ~f:Impl.Field.constant fields in
               typ.var_of_fields (fields, aux)
             in
             let open Impl.Typ in
@@ -477,10 +478,7 @@ struct
             let (T (Typ typ, f, f')) = etyp e is_boolean spec in
             let constant_var =
               let fields, aux = typ.value_to_fields x in
-              let fields =
-                Array.map fields ~f:(fun x ->
-                    Snarky_backendless.Cvar.Constant x )
-              in
+              let fields = Array.map ~f:Impl.Field.constant fields in
               typ.var_of_fields (fields, aux)
             in
             (* We skip any constraints that would be added here, but we *do* use

src/lib/pickles/composition_types/spec.mli

@@ -1,4 +1,7 @@
-type 'f impl = (module Snarky_backendless.Snark_intf.Run with type field = 'f)
+type ('f, 'v) impl =
+  (module Snarky_backendless.Snark_intf.Run
+     with type field = 'f
+      and type field_var = 'v )
 
 module type Branch_data_checked = sig
   type field_var
@@ -101,11 +104,10 @@ val typ :
            Kimchi_backend_common.Scalar_challenge.t
            Bulletproof_challenge.t
        ; bulletproof_challenge2 :
-           Step_impl.Field.Constant.t Limb_vector.Challenge.t
-           Kimchi_backend_common.Scalar_challenge.t
+           Step_impl.Field.t Kimchi_backend_common.Scalar_challenge.t
            Bulletproof_challenge.t
        ; challenge1 : Limb_vector.Challenge.Constant.t
-       ; challenge2 : Step_impl.Field.Constant.t Limb_vector.Challenge.t
+       ; challenge2 : Step_impl.Field.t
        ; digest1 : Digest.Constant.t
        ; digest2 : Step_impl.Field.t
        ; field1 : 'c
@@ -128,11 +130,10 @@ val wrap_typ :
            Kimchi_backend_common.Scalar_challenge.t
            Bulletproof_challenge.t
        ; bulletproof_challenge2 :
-           Wrap_impl.Field.Constant.t Limb_vector.Challenge.t
-           Kimchi_backend_common.Scalar_challenge.t
+           Wrap_impl.Field.t Kimchi_backend_common.Scalar_challenge.t
            Bulletproof_challenge.t
        ; challenge1 : Limb_vector.Challenge.Constant.t
-       ; challenge2 : Wrap_impl.Field.Constant.t Limb_vector.Challenge.t
+       ; challenge2 : Wrap_impl.Field.t
        ; digest1 : Digest.Constant.t
        ; digest2 : Wrap_impl.Field.t
        ; field1 : 'c
@@ -209,29 +210,27 @@ val wrap_packed_typ :
   -> ('e, 'd) Wrap_etyp.t
 
 val pack :
-     'f impl
-  -> ('branch_data_checked, 'f Snarky_backendless.Cvar.t) branch_data
+     ('f, 'v) impl
+  -> ('branch_data_checked, 'v) branch_data
   -> ( 'a
      , 'b
      , < bool1 : bool
-       ; bool2 :
-           'f Snarky_backendless.Cvar.t Snarky_backendless.Snark_intf.Boolean0.t
+       ; bool2 : 'v Snarky_backendless.Boolean.t
        ; branch_data1 : Branch_data.t
        ; branch_data2 : 'branch_data_checked
        ; bulletproof_challenge1 :
            Limb_vector.Challenge.Constant.t
            Kimchi_backend_common.Scalar_challenge.t
            Bulletproof_challenge.t
        ; bulletproof_challenge2 :
-           'f Limb_vector.Challenge.t Kimchi_backend_common.Scalar_challenge.t
-           Bulletproof_challenge.t
+           'v Kimchi_backend_common.Scalar_challenge.t Bulletproof_challenge.t
        ; challenge1 : Limb_vector.Challenge.Constant.t
-       ; challenge2 : 'f Limb_vector.Challenge.t
+       ; challenge2 : 'v
        ; digest1 : Digest.Constant.t
-       ; digest2 : 'f Snarky_backendless.Cvar.t
+       ; digest2 : 'v
        ; field1 : 'c
        ; field2 : 'd
        ; .. > )
      T.t
   -> 'b
-  -> [ `Field of 'd | `Packed_bits of 'f Snarky_backendless.Cvar.t * int ] array
+  -> [ `Field of 'd | `Packed_bits of 'v * int ] array

src/lib/pickles/limb_vector/challenge.ml

@@ -1,15 +1,12 @@
 open Pickles_types
-
-type 'f t = 'f Snarky_backendless.Cvar.t
-
 module Constant = Constant.Make (Nat.N2)
 
 module type S = sig
   module Impl : Snarky_backendless.Snark_intf.Run
 
   open Impl
 
-  type nonrec t = field t
+  type nonrec t = Field.t
 
   module Constant : sig
     type t = Constant.t [@@deriving sexp_of]

src/lib/pickles/limb_vector/challenge.mli

@@ -1,11 +1,9 @@
-type 'f t = 'f Snarky_backendless.Cvar.t
-
 module Constant : module type of Constant.Make (Pickles_types.Nat.N2)
 
 module type S = sig
   module Impl : Snarky_backendless.Snark_intf.Run
 
-  type nonrec t = Impl.field t
+  type nonrec t = Impl.Field.t
 
   module Constant : sig
     type t = Constant.t [@@deriving sexp_of]

src/lib/pickles/plonk_checks/plonk_checks.ml

@@ -447,9 +447,11 @@ module Make (Shifted_value : Shifted_value.S) (Sc : Scalars.S) = struct
     but we deferred the arithmetic checks until here
     so that we have the efficiency of the native field.
   *)
-  let checked (type t)
-      (module Impl : Snarky_backendless.Snark_intf.Run with type field = t)
-      ~shift ~env (plonk : (_, _, _, _ Opt.t, _ Opt.t, _) In_circuit.t) evals =
+  let checked (type field field_var)
+      (module Impl : Snarky_backendless.Snark_intf.Run
+        with type field = field
+         and type field_var = field_var ) ~shift ~env
+      (plonk : (_, _, _, _ Opt.t, _ Opt.t, _) In_circuit.t) evals =
     let actual =
       derive_plonk ~with_label:Impl.with_label
         (module Impl.Field)

src/lib/pickles/plonk_checks/plonk_checks.mli

@@ -131,24 +131,22 @@ module Make (Shifted_value : Pickles_types.Shifted_value.S) (_ : Scalars.S) : si
        Composition_types.Wrap.Proof_state.Deferred_values.Plonk.In_circuit.t
 
   val checked :
-       (module Snarky_backendless.Snark_intf.Run with type field = 't)
-    -> shift:'t Snarky_backendless.Cvar.t Shifted_value.Shift.t
-    -> env:'t Snarky_backendless.Cvar.t Scalars.Env.t
-    -> ( 't Snarky_backendless.Cvar.t
-       , 't Snarky_backendless.Cvar.t
-       , 't Snarky_backendless.Cvar.t Shifted_value.t
-       , ( 't Snarky_backendless.Cvar.t Shifted_value.t
-         , 't Snarky_backendless.Cvar.t Snarky_backendless.Boolean.t )
+       (module Snarky_backendless.Snark_intf.Run
+          with type field = 'f
+           and type field_var = 'v )
+    -> shift:'v Shifted_value.Shift.t
+    -> env:'v Scalars.Env.t
+    -> ( 'v
+       , 'v
+       , 'v Shifted_value.t
+       , ( 'v Shifted_value.t
+         , 'v Snarky_backendless.Boolean.t )
          Pickles_types.Opt.t
-       , ( 't Snarky_backendless.Cvar.t
-         , 't Snarky_backendless.Cvar.t Snarky_backendless.Boolean.t )
-         Pickles_types.Opt.t
-       , 't Snarky_backendless.Cvar.t Snarky_backendless.Boolean.t )
+       , ('v, 'v Snarky_backendless.Boolean.t) Pickles_types.Opt.t
+       , 'v Snarky_backendless.Boolean.t )
        Composition_types.Wrap.Proof_state.Deferred_values.Plonk.In_circuit.t
-    -> ( 't Snarky_backendless.Cvar.t * 't Snarky_backendless.Cvar.t
-       , 'a )
-       Pickles_types.Plonk_types.Evals.In_circuit.t
-    -> 't Snarky_backendless.Cvar.t Snarky_backendless.Boolean.t
+    -> ('v * 'v, 'a) Pickles_types.Plonk_types.Evals.In_circuit.t
+    -> 'v Snarky_backendless.Boolean.t
 end
 
 (** [Domain] is re-exported from library Pickles_base *)

src/lib/pickles/pseudo/pseudo.ml

@@ -13,7 +13,7 @@ module Make (Impl : Snarky_backendless.Snark_intf.Run) = struct
     let open Impl in
     match Field.to_constant_and_terms x with
     | None, [ (x, i) ] when Field.Constant.(equal x one) ->
-        Snarky_backendless.Cvar.Var i
+        Field.Unsafe.of_index i
     | Some c, [] ->
         Field.constant c
     | _ ->

src/lib/pickles/step_verifier.ml

@@ -10,6 +10,7 @@ open Pickles_types
 module Make
     (Inputs : Intf.Step_main_inputs.S
                 with type Impl.field = Backend.Tick.Field.t
+                 and type Impl.field_var = Step_main_inputs.Impl.field_var
                  and type Impl.Bigint.t = Backend.Tick.Bigint.t
                  and type Impl.Constraint.t = Backend.Tick.Constraint.t
                  and type 'a Impl.Internal_Basic.Checked.t =