Fixed Cell evaluation issue and field type generic issue§

src/lib/pickles/plonk_checks/dune

@@ -20,6 +20,8 @@
  pickles_base
  pickles.backend
  pickles.composition_types
+ kimchi_backend.pasta.basic
+ kimchi_backend.pasta
  kimchi_backend
  kimchi_types
  snarky.backendless

src/lib/pickles/plonk_checks/gen_scalars/gen_scalars.ml

@@ -14,8 +14,7 @@ let () =
 (* turn off fragile pattern-matching warning from sexp ppx *)
 [@@@warning "-4"]
 
-type curr_or_next = Curr | Next
-[@@deriving hash, eq, compare, sexp]
+type curr_or_next = Kimchi_types.curr_or_next = Curr | Next [@@deriving hash, eq, compare, sexp]
 
 module Gate_type = struct
  module T = struct
@@ -60,19 +59,19 @@ module Lookup_pattern = struct
 end
 
 module Column = struct
- open Core_kernel
-
  module T = struct
- type t =
+ type t = Kimchi_types.column =
  | Witness of int
- | Index of Gate_type.t
- | Coefficient of int
- | LookupTable
+ | Z
  | LookupSorted of int
  | LookupAggreg
+ | LookupTable
  | LookupKindIndex of Lookup_pattern.t
  | LookupRuntimeSelector
  | LookupRuntimeTable
+ | Index of Gate_type.t
+ | Coefficient of int
+ | Permutation of int
  [@@deriving hash, eq, compare, sexp]
  end
 

src/lib/pickles/plonk_checks/plonk_checks.ml

@@ -48,6 +48,14 @@ module type Field_intf = sig
  val inv : t -> t
 
  val negate : t -> t
+ (*
+ module Constant : sig
+ (** The finite field over which the R1CS operates. *)
+ type t = field [@@deriving bin_io, sexp, hash, compare]
+
+ (** Return a constraint system constant representing the given value. *)
+ val constant : ('var, 'value) Typ.t -> 'value -> 'var
+ end *)
 end
 
 module type Field_with_if_intf = sig
@@ -197,6 +205,10 @@ let scalars_env (type boolean t) (module B : Bool_intf with type t = boolean)
  i ()
  | Coefficient i ->
  get_eval coefficients.(i)
+ | Permutation _i ->
+ failwith "Not implemented"
+ | Z ->
+ failwith "Not implemented"
  | LookupTable ->
  get_eval (Opt.value_exn e.lookup_table)
  | LookupSorted i ->
@@ -339,20 +351,86 @@ let scalars_env (type boolean t) (module B : Bool_intf with type t = boolean)
 let perm_alpha0 : int = 21
 
 module Make (Shifted_value : Shifted_value.S) (Sc : Scalars.S) = struct
+ let evaluate_rpn (type t u) (module F : Field_intf with type t = t)
+ ~(* (module U : Field_intf with type t = u) *) (env : t Scalars.Env.t)
+ ~(gate_rpn : u Kimchi_types.polish_token array)
+ ~(* ~(gate_rpn : Kimchi_pasta_basic.Fp.t Kimchi_types.polish_token array) *)
+ map_constant =
+ (* ~(_evals : (_ * _, _) Plonk_types.Evals.In_circuit.t) *)
+ (* ~(gate_rpn : Kimchi_pasta_basic.Fp.t Kimchi_types.polish_token array) = *)
+ printf "HI\n" ;
+
+ let stack = Stack.create () in
+ Array.iteri gate_rpn ~f:(fun _idx token ->
+ Kimchi_types.(
+ match token with
+ | Alpha ->
+ Stack.push stack @@ env.alpha_pow 1
+ (* JES: CHECK: Where just plain alpha? *)
+ | Beta ->
+ Stack.push stack env.beta
+ | Gamma ->
+ Stack.push stack env.gamma
+ | JointCombiner ->
+ Stack.push stack env.joint_combiner
+ | EndoCoefficient ->
+ Stack.push stack env.endo_coefficient
+ | Mds mds ->
+ Stack.push stack @@ env.mds (mds.row, mds.col)
+ (* JES: CHECK: is this (row, col) format *)
+ | VanishesOnZeroKnowledgeAndPreviousRows ->
+ Stack.push stack env.vanishes_on_zero_knowledge_and_previous_rows
+ | UnnormalizedLagrangeBasis i ->
+ Stack.push stack
+ @@ env.unnormalized_lagrange_basis
+ (i.zk_rows, Int32.to_int_exn i.offset)
+ | Literal x ->
+ Stack.push stack @@ map_constant x
+ | Dup ->
+ Stack.(push stack @@ top_exn stack)
+ | Cell v ->
+ Stack.push stack @@ env.var (v.col, v.row)
+ | Pow n ->
+ Stack.(
+ push stack
+ @@ pow2pow (module F) (top_exn stack) (Int32.to_int_exn n))
+ (* JES: CHECK: Correct way to pow here? *)
+ | Add ->
+ Stack.(push stack @@ F.( + ) (pop_exn stack) (pop_exn stack))
+ | Mul ->
+ Stack.(push stack @@ F.( * ) (pop_exn stack) (pop_exn stack))
+ | Sub ->
+ Stack.(push stack @@ F.( - ) (pop_exn stack) (pop_exn stack))
+ | Store ->
+ failwith "Unsupported RPN token: Store"
+ | Load _ ->
+ failwith "Unsupported RPN token: Load"
+ | SkipIf _ ->
+ failwith "Unsupported RPN token: SkipIf"
+ | SkipIfNot _ ->
+ failwith "Unsupported RPN token: SkipIfNot") ) ;
+
+ Stack.pop_exn stack
+
  (** Computes the ft evaluation at zeta.
  (see https://o1-labs.github.io/mina-book/crypto/plonk/maller_15.html#the-evaluation-of-l)
  *)
- let ft_eval0 (type t) (module F : Field_intf with type t = t) ~domain
- ~(env : t Scalars.Env.t)
- ({ alpha = _
- ; beta
- ; gamma
- ; zeta
- ; joint_combiner = _
- ; feature_flags = _
- ; _
- } :
- _ Minimal.t ) (e : (_ * _, _) Plonk_types.Evals.In_circuit.t) p_eval0 =
+ let ft_eval0 (type t) (* (type u) *) (module F : Field_intf with type t = t)
+ ~(* (module U : Field_intf with type t = u) *) domain
+ ~(env : t Scalars.Env.t) ?custom_gate_type ?map_constant
+ (* ~(const_map : 'a -> 'b) *)
+ (* ~(custom_gate_type : Kimchi_pasta_basic.Fp.t Kimchi_types.polish_token array option) *)
+ (* ?custom_gate_type *)
+ ({ alpha = _
+ ; beta
+ ; gamma
+ ; zeta
+ ; joint_combiner = _
+ ; feature_flags = _
+ ; _
+ } :
+ _ Minimal.t ) (e : (_ * _, _) Plonk_types.Evals.In_circuit.t) p_eval0
+ =
  let open Plonk_types.Evals.In_circuit in
  let e0 field = fst (field e) in
  let e1 field = snd (field e) in
@@ -401,6 +479,21 @@ module Make (Shifted_value : Shifted_value.S) (Sc : Scalars.S) = struct
  (* (1) Create ScalarsMinus, without ffAdd *)
  let constant_term =
  Sc.constant_term env
+ +
+ match custom_gate_type with
+ | Some custom_gate_type -> (
+ match map_constant with
+ | Some map_constant ->
+ evaluate_rpn
+ (module F)
+ ~env ~gate_rpn:custom_gate_type ~map_constant
+ | None ->
+ failwith "Need constant mapping function"
+ (* evaluate_rpn
+ (module F)
+ ~env ~gate_rpn:custom_gate_type ~map_constant:Fn.id *) )
+ | None ->
+ F.zero
  (* (2) ~override_ffadd: optional... Sc.evaluate_custom_gate ~env ~polish_gate *)
  in
  ft_eval0 - constant_term
@@ -478,152 +571,4 @@ module Make (Shifted_value : Shifted_value.S) (Sc : Scalars.S) = struct
  ~f:(fun f -> Shifted_value.equal Field.equal (f plonk) (f actual))
  [ perm ] )
  |> Boolean.all )
-
- (* let evaluate_rpn (type t) (module F : Field_intf with type t = t) (* ~(_env : t Scalars.Env.t) *) ~(_rpn_gate : t Kimchi_types.polish_token array) =
- F.zero *)
-
- (* let evaluate_rpn (type t) (module F : Field_intf with type t = t) (* ~(_env : t Scalars.Env.t) *) ~(_rpn_gate : t Kimchi_types.polish_token array) =
- F.zero *)
-
- (* let evaluate_rpn (type t) (module F : Field_intf with type t = t) ~(_env : t Scalars.Env.t) ~(_rpn_gate : F.t Kimchi_types.polish_token array) =
- F.zero *)
-
- (* WORKING: let evaluate_rpn (type t) (module F: Field_intf with type t = t) (* ~(_env : t Scalars.Env.t) *) ~(_rpn_gate : t Kimchi_types.polish_token array) =
- F.zero *)
-
- let evaluate_rpn (type t) (module F : Field_intf with type t = t)
- ~(_env : t Scalars.Env.t)
- ~(_evals : (_ * _, _) Plonk_types.Evals.In_circuit.t)
- ~(gate_rpn : t Kimchi_types.polish_token array) =
- (* let rec evaluate ~stack ~(_rpn_gate : t Kimchi_types.polish_token array) idx : F.t =
- if Array.length rpn_gate = 0 then
- Stack.pop_exn stack
- else
- let elt = Array.get rpn_gate idx in
- match elt with
- | _ -> F.zero *)
- let evaluate_cell (evals : (_ * _, _) Plonk_types.Evals.In_circuit.t)
- (var : Kimchi_types.variable) =
- (* Kimchi_types.( *)
- let witness = Vector.to_array evals.w in
- let coefficients = Vector.to_array evals.coefficients in
- let permutation_column = Vector.to_array evals.s in
- let get_eval = match var.row with Curr -> fst | Next -> snd in
- match[@warning "-4"] var.col with
- | Witness i ->
- get_eval witness.(i)
- | Z ->
- get_eval evals.z
- | LookupSorted i ->
- get_eval
- (Opt.value_exn
- (Option.value_exn (Vector.nth evals.lookup_sorted i)) )
- | LookupAggreg ->
- get_eval (Opt.value_exn evals.lookup_aggregation)
- | LookupTable ->
- get_eval (Opt.value_exn evals.lookup_table)
- | LookupRuntimeTable ->
- get_eval (Opt.value_exn evals.runtime_lookup_table)
- | Index Poseidon ->
- get_eval evals.poseidon_selector
- | Index Generic ->
- get_eval evals.generic_selector
- | Index CompleteAdd ->
- get_eval evals.complete_add_selector
- | Index VarBaseMul ->
- get_eval evals.mul_selector
- | Index EndoMul ->
- get_eval evals.emul_selector
- | Index EndoMulScalar ->
- get_eval evals.endomul_scalar_selector
- | Index RangeCheck0 ->
- get_eval (Opt.value_exn evals.range_check0_selector)
- | Index RangeCheck1 ->
- get_eval (Opt.value_exn evals.range_check1_selector)
- | Index ForeignFieldAdd ->
- get_eval (Opt.value_exn evals.foreign_field_add_selector)
- | Index ForeignFieldMul ->
- get_eval (Opt.value_exn evals.foreign_field_mul_selector)
- | Index Xor16 ->
- get_eval (Opt.value_exn evals.xor_selector)
- | Index Rot64 ->
- get_eval (Opt.value_exn evals.rot_selector)
- | Index i ->
- failwithf
- !"Index %{sexp:Scalars.Gate_type.t}\n\
- %! should have been linearized away"
- i ()
- | Permutation i ->
- get_eval permutation_column.(i)
- | Coefficient i ->
- get_eval coefficients.(i)
- | LookupKindIndex Lookup ->
- get_eval (Opt.value_exn evals.lookup_gate_lookup_selector)
- | LookupKindIndex Xor ->
- get_eval (Opt.value_exn evals.xor_lookup_selector)
- | LookupKindIndex RangeCheck ->
- get_eval (Opt.value_exn evals.range_check_lookup_selector)
- | LookupKindIndex ForeignFieldMul ->
- get_eval (Opt.value_exn evals.foreign_field_mul_lookup_selector)
- | LookupRuntimeSelector ->
- get_eval (Opt.value_exn evals.runtime_lookup_table_selector)
- in
-
- let stack = Stack.create () in
- Array.iteri gate_rpn ~f:(fun _idx token ->
- Kimchi_types.(
- match token with
- | Alpha ->
- Stack.push stack @@ _env.alpha_pow 1
- (* JES: CHECK: Where just plain alpha? *)
- | Beta ->
- Stack.push stack _env.beta
- | Gamma ->
- Stack.push stack _env.gamma
- | JointCombiner ->
- Stack.push stack _env.joint_combiner
- | EndoCoefficient ->
- Stack.push stack _env.endo_coefficient
- | Mds mds ->
- Stack.push stack @@ _env.mds (mds.row, mds.col)
- (* JES: CHECK: is this (row, col) format *)
- | VanishesOnZeroKnowledgeAndPreviousRows ->
- Stack.push stack _env.vanishes_on_zero_knowledge_and_previous_rows
- | UnnormalizedLagrangeBasis i ->
- Stack.push stack
- @@ _env.unnormalized_lagrange_basis
- (i.zk_rows, Int32.to_int_exn i.offset)
- | Literal x ->
- Stack.push stack x
- | Dup ->
- Stack.(push stack @@ top_exn stack)
- | Cell v ->
- Stack.push stack @@ evaluate_cell _evals v
- (* JES: TODO: would be nice to instead somehow do
- Stack.push stack @@ _env.var (v.col, v.row) *)
- (* JES: CHECK: How to v.evaluate here? *)
- | Pow n ->
- Stack.(
- push stack
- @@ pow2pow (module F) (top_exn stack) (Int32.to_int_exn n))
- (* JES: CHECK: Correct way to pow here? *)
- | Add ->
- Stack.(push stack @@ F.( + ) (pop_exn stack) (pop_exn stack))
- | Mul ->
- Stack.(push stack @@ F.( * ) (pop_exn stack) (pop_exn stack))
- | Sub ->
- Stack.(push stack @@ F.( - ) (pop_exn stack) (pop_exn stack))
- | Store ->
- failwith "Unsupported RPN token: Store"
- | Load _ ->
- failwith "Unsupported RPN token: Load"
- | SkipIf _ ->
- failwith "Unsupported RPN token: SkipIf"
- | SkipIfNot _ ->
- failwith "Unsupported RPN token: SkipIfNot") ) ;
-
- Stack.pop_exn stack
-
- (* let evaluate_rpn (* ~(_env : Backend.Tick.Field.t Scalars.Env.t) *) ~(_rpn_gate : t Kimchi_types.polish_token array) =
- F.zero *)
 end

src/lib/pickles/plonk_checks/plonk_checks.mli

@@ -89,11 +89,27 @@ val scalars_env :
  -> 't Scalars.Env.t
 
 module Make (Shifted_value : Pickles_types.Shifted_value.S) (_ : Scalars.S) : sig
+ val evaluate_rpn :
+ (module Field_intf with type t = 't)
+ (* -> (module Field_intf with type t = 'u) *)
+ -> env:'t Scalars.Env.t
+ (* -> _evals:('t * 't, 'a) Pickles_types.Plonk_types.Evals.In_circuit.t *)
+ (* -> gate_rpn:Kimchi_pasta_basic.Fp.t Kimchi_types.polish_token array *)
+ -> gate_rpn:'u Kimchi_types.polish_token array
+ -> map_constant:('u -> 't)
+ -> (* -> map_constant:(Kimchi_pasta_basic.Fp.t -> 't) *)
+ 't
+
  val ft_eval0 :
- 't field
- -> domain:< shifts : 't array ; .. >
+ 't field (* -> 'u field *)
+ -> domain:< shifts : 't array ; .. > (* -> const_map:('a -> 'b) *)
  -> env:'t Scalars.Env.t
- -> ( 't
+ (* -> ?custom_gate_type:Kimchi_pasta_basic.Fp.t Kimchi_types.polish_token array *)
+ -> ?custom_gate_type:'u Kimchi_types.polish_token array
+ -> ?map_constant:('u -> 't)
+ -> (* -> ?map_constant:(Kimchi_pasta_basic.Fp.t -> 't) *)
+ (* -> ?custom_gate_type:Kimchi_pasta_basic.Fp.t Kimchi_types.polish_token array *)
+ ( 't
  , 't
  , 'b )
  Composition_types.Wrap.Proof_state.Deferred_values.Plonk.Minimal.t
@@ -138,16 +154,6 @@ module Make (Shifted_value : Pickles_types.Shifted_value.S) (_ : Scalars.S) : si
  , 'a )
  Pickles_types.Plonk_types.Evals.In_circuit.t
  -> 't Snarky_backendless.Cvar.t Snarky_backendless.Boolean.t
-
- val evaluate_rpn :
- (module Field_intf with type t = 't)
- (* 't field *)
- (* 't *)
- (* (module Internal_Basic.field with type t = 't) *)
- -> _env:'t Scalars.Env.t
- -> _evals:('t * 't, 'a) Pickles_types.Plonk_types.Evals.In_circuit.t
- -> gate_rpn:'t Kimchi_types.polish_token array
- -> 't
 end
 
 (** [Domain] is re-exported from library Pickles_base *)