Merge pull request #14870 from MinaProtocol/volhovm/refactoring-15-01…

…-2024

Cosmetics/Refactoring

nix/ocaml.nix

@@ -147,7 +147,7 @@ let
         MINA_COMMIT_DATE = "<unknown>";
         MINA_BRANCH = "<unknown>";
 
-        DUNE_PROFILE = "devnet";
+        DUNE_PROFILE = "dev";
 
         NIX_LDFLAGS =
           optionalString (pkgs.stdenv.isDarwin && pkgs.stdenv.isAarch64)
@@ -269,9 +269,9 @@ let
           mv _build/default/src/app/cli/src/mina.exe $out/bin/mina
         '';
       });
-        
+
       with-instrumentation = wrapMina self.with-instrumentation-dev { };
-      
+
       # Unit tests
       mina_tests = runMinaCheck {
         name = "tests";
@@ -314,4 +314,4 @@ let
 
       test_executive = wrapMina self.test_executive-dev { };
     };
-in scope.overrideScope' overlay
+in scope.overrideScope' overlay

src/lib/blockchain_snark/blockchain_snark_state.ml

@@ -238,7 +238,7 @@ let%snarkydef_ step ~(logger : Logger.t)
     in
     (t, is_base_case)
   in
-  let%bind txn_snark_should_verify, success =
+  let%bind txn_snark_must_verify, success =
     let%bind new_pending_coinbase_hash, deleted_stack, no_coinbases_popped =
       let coinbase_receiver =
         Consensus.Data.Consensus_state.coinbase_receiver_var consensus_state
@@ -348,14 +348,14 @@ let%snarkydef_ step ~(logger : Logger.t)
     in
     (transaction_snark_should_verifiy, result)
   in
-  let txn_snark_should_verify =
+  let txn_snark_must_verify =
     match proof_level with
     | Check | None ->
         Boolean.false_
     | Full ->
-        txn_snark_should_verify
+        txn_snark_must_verify
   in
-  let prev_should_verify =
+  let prev_must_verify =
     match proof_level with
     | Check | None ->
         Boolean.false_
@@ -374,11 +374,11 @@ let%snarkydef_ step ~(logger : Logger.t)
   ( { Pickles.Inductive_rule.Previous_proof_statement.public_input =
         previous_blockchain_proof_input
     ; proof = previous_blockchain_proof
-    ; proof_must_verify = prev_should_verify
+    ; proof_must_verify = prev_must_verify
     }
   , { Pickles.Inductive_rule.Previous_proof_statement.public_input = txn_snark
     ; proof = txn_snark_proof
-    ; proof_must_verify = txn_snark_should_verify
+    ; proof_must_verify = txn_snark_must_verify
     } )
 
 module Statement = struct

src/lib/crypto/kimchi_backend/common/plonk_dlog_proof.ml

@@ -503,7 +503,8 @@ module Make (Inputs : Inputs_intf) = struct
   let to_backend_with_public_evals chal_polys primary_input t =
     to_backend_with_public_evals' chal_polys (List.to_array primary_input) t
 
-  let create ?message pk ~primary ~auxiliary =
+  (* Extract challenges and commitments from the (optional) message *)
+  let extract_challenges_and_commitments ?message =
     let chal_polys =
       match (message : message option) with Some s -> s | None -> []
     in
@@ -517,29 +518,17 @@ module Make (Inputs : Inputs_intf) = struct
         ~f:(fun { Challenge_polynomial.commitment; _ } ->
           G.Affine.to_backend (Finite commitment) )
     in
-    let res =
-      Backend.create pk ~primary ~auxiliary ~prev_chals:challenges
-        ~prev_comms:commitments
-    in
+    (challenges, commitments)
+
+  let create ?message pk ~primary ~auxiliary =
+    let prev_chals, prev_comms = extract_challenges_and_commitments ?message in
+    let res = Backend.create pk ~primary ~auxiliary ~prev_chals ~prev_comms in
     of_backend_with_public_evals res
 
   let create_async ?message pk ~primary ~auxiliary =
-    let chal_polys =
-      match (message : message option) with Some s -> s | None -> []
-    in
-    let challenges =
-      List.map chal_polys ~f:(fun { Challenge_polynomial.challenges; _ } ->
-          challenges )
-      |> Array.concat
-    in
-    let commitments =
-      Array.of_list_map chal_polys
-        ~f:(fun { Challenge_polynomial.commitment; _ } ->
-          G.Affine.to_backend (Finite commitment) )
-    in
+    let prev_chals, prev_comms = extract_challenges_and_commitments ?message in
     let%map.Promise res =
-      Backend.create_async pk ~primary ~auxiliary ~prev_chals:challenges
-        ~prev_comms:commitments
+      Backend.create_async pk ~primary ~auxiliary ~prev_chals ~prev_comms
     in
     of_backend_with_public_evals res
 

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

@@ -87,8 +87,8 @@ module Proof = Plonk_dlog_proof.Make (struct
     let batch_verify vks ts =
       Promise.run_in_thread (fun () -> batch_verify vks ts)
 
-    let create_aux ~f:create (pk : Keypair.t) ~primary ~auxiliary ~prev_chals
-        ~prev_comms =
+    let create_aux ~f:backend_create (pk : Keypair.t) ~primary ~auxiliary
+        ~prev_chals ~prev_comms =
       (* external values contains [1, primary..., auxiliary ] *)
       let external_values i =
         let open Field.Vector in
@@ -111,17 +111,19 @@ module Proof = Plonk_dlog_proof.Make (struct
             done ;
             witness )
       in
-      create pk.index witness_cols runtime_tables prev_chals prev_comms
+      backend_create pk.index witness_cols runtime_tables prev_chals prev_comms
 
     let create_async (pk : Keypair.t) ~primary ~auxiliary ~prev_chals
         ~prev_comms =
       create_aux pk ~primary ~auxiliary ~prev_chals ~prev_comms
-        ~f:(fun pk auxiliary_input runtime_tables prev_challenges prev_sgs ->
+        ~f:(fun index witness runtime_tables prev_chals prev_sgs ->
           Promise.run_in_thread (fun () ->
-              create pk auxiliary_input runtime_tables prev_challenges prev_sgs ) )
+              Kimchi_bindings.Protocol.Proof.Fq.create index witness
+                runtime_tables prev_chals prev_sgs ) )
 
     let create (pk : Keypair.t) ~primary ~auxiliary ~prev_chals ~prev_comms =
-      create_aux pk ~primary ~auxiliary ~prev_chals ~prev_comms ~f:create
+      create_aux pk ~primary ~auxiliary ~prev_chals ~prev_comms
+        ~f:Kimchi_bindings.Protocol.Proof.Fq.create
   end
 
   module Verifier_index = Kimchi_bindings.Protocol.VerifierIndex.Fq

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

@@ -86,8 +86,8 @@ module Proof = Plonk_dlog_proof.Make (struct
     let batch_verify vks ts =
       Promise.run_in_thread (fun () -> batch_verify vks ts)
 
-    let create_aux ~f:create (pk : Keypair.t) primary auxiliary prev_chals
-        prev_comms =
+    let create_aux ~f:backend_create (pk : Keypair.t) primary auxiliary
+        prev_chals prev_comms =
       (* external values contains [1, primary..., auxiliary ] *)
       let external_values i =
         let open Field.Vector in
@@ -110,17 +110,19 @@ module Proof = Plonk_dlog_proof.Make (struct
             done ;
             witness )
       in
-      create pk.index witness_cols runtime_tables prev_chals prev_comms
+      backend_create pk.index witness_cols runtime_tables prev_chals prev_comms
 
     let create_async (pk : Keypair.t) ~primary ~auxiliary ~prev_chals
         ~prev_comms =
       create_aux pk primary auxiliary prev_chals prev_comms
-        ~f:(fun pk auxiliary_input runtime_tables prev_challenges prev_sgs ->
+        ~f:(fun index witness runtime_tables prev_chals prev_sgs ->
           Promise.run_in_thread (fun () ->
-              create pk auxiliary_input runtime_tables prev_challenges prev_sgs ) )
+              Kimchi_bindings.Protocol.Proof.Fp.create index witness
+                runtime_tables prev_chals prev_sgs ) )
 
     let create (pk : Keypair.t) ~primary ~auxiliary ~prev_chals ~prev_comms =
-      create_aux pk primary auxiliary prev_chals prev_comms ~f:create
+      create_aux pk primary auxiliary prev_chals prev_comms
+        ~f:Kimchi_bindings.Protocol.Proof.Fp.create
   end
 
   module Verifier_index = Kimchi_bindings.Protocol.VerifierIndex.Fp

src/lib/pickles/step_main.ml

@@ -2,7 +2,6 @@ open Pickles_types
 open Hlist
 open Import
 open Impls.Step
-open Step_verifier
 module B = Inductive_rule.B
 
 (* Converts from the one hot vector representation of a number
@@ -16,6 +15,7 @@ module B = Inductive_rule.B
 let _one_hot_vector_to_num (type n) (v : n Per_proof_witness.One_hot_vector.t) :
     Field.t =
   let n = Vector.length (v :> (Boolean.var, n) Vector.t) in
+  let open Step_verifier in
   Pseudo.choose (v, Vector.init n ~f:Field.of_int) ~f:Fn.id
 
 let verify_one ~srs
@@ -28,8 +28,8 @@ let verify_one ~srs
      } :
       _ Per_proof_witness.t ) (d : _ Types_map.For_step.t)
     (messages_for_next_wrap_proof : Digest.t) (unfinalized : Unfinalized.t)
-    (should_verify : B.t) : _ Vector.t * B.t =
-  Boolean.Assert.( = ) unfinalized.should_finalize should_verify ;
+    (must_verify : B.t) : _ Vector.t * B.t =
+  Boolean.Assert.( = ) unfinalized.should_finalize must_verify ;
   let deferred_values = proof_state.deferred_values in
   let finalized, chals =
     with_label __LOC__ (fun () ->
@@ -41,9 +41,9 @@ let verify_one ~srs
           sponge
         in
         (* TODO: Refactor args into an "unfinalized proof" struct *)
-        finalize_other_proof d.max_proofs_verified ~step_domains:d.step_domains
-          ~zk_rows:d.zk_rows ~sponge ~prev_challenges deferred_values
-          prev_proof_evals )
+        Step_verifier.finalize_other_proof d.max_proofs_verified
+          ~step_domains:d.step_domains ~zk_rows:d.zk_rows ~sponge
+          ~prev_challenges deferred_values prev_proof_evals )
   in
   let branch_data = deferred_values.branch_data in
   let sponge_after_index, hash_messages_for_next_step_proof =
@@ -53,7 +53,8 @@ let verify_one ~srs
     in
     let sponge_after_index, hash_messages_for_next_step_proof =
       (* TODO: Don't rehash when it's not necessary *)
-      hash_messages_for_next_step_proof_opt ~index:d.wrap_key to_field_elements
+      Step_verifier.hash_messages_for_next_step_proof_opt ~index:d.wrap_key
+        to_field_elements
     in
     (sponge_after_index, unstage hash_messages_for_next_step_proof)
   in
@@ -87,7 +88,7 @@ let verify_one ~srs
      statement *)
   let verified =
     with_label __LOC__ (fun () ->
-        verify ~srs
+        Step_verifier.verify ~srs
           ~feature_flags:(Plonk_types.Features.of_full d.feature_flags)
           ~lookup_parameters:
             { use = d.feature_flags.uses_lookups
@@ -104,22 +105,21 @@ let verify_one ~srs
                 }
             }
           ~proofs_verified:d.max_proofs_verified ~wrap_domain:d.wrap_domain
-          ~is_base_case:(Boolean.not should_verify)
-          ~sponge_after_index ~sg_old:prev_challenge_polynomial_commitments
-          ~proof:wrap_proof ~wrap_verification_key:d.wrap_key statement
-          unfinalized )
+          ~is_base_case:(Boolean.not must_verify) ~sponge_after_index
+          ~sg_old:prev_challenge_polynomial_commitments ~proof:wrap_proof
+          ~wrap_verification_key:d.wrap_key statement unfinalized )
   in
   if debug then
     as_prover
       As_prover.(
         fun () ->
           let finalized = read Boolean.typ finalized in
           let verified = read Boolean.typ verified in
-          let should_verify = read Boolean.typ should_verify in
+          let must_verify = read Boolean.typ must_verify in
           printf "finalized: %b\n%!" finalized ;
           printf "verified: %b\n%!" verified ;
-          printf "should_verify: %b\n\n%!" should_verify) ;
-  (chals, Boolean.(verified &&& finalized ||| not should_verify))
+          printf "must_verify: %b\n\n%!" must_verify) ;
+  (chals, Boolean.(verified &&& finalized ||| not must_verify))
 
 (* The SNARK function corresponding to the input inductive rule. *)
 let step_main :
@@ -349,7 +349,7 @@ let step_main :
           exists
             ~request:(fun () -> Req.Wrap_index)
             (Plonk_verification_key_evals.typ
-               (Typ.array ~length:num_chunks Inner_curve.typ) )
+               (Typ.array ~length:num_chunks Step_verifier.Inner_curve.typ) )
         and prevs =
           exists (Prev_typ.f prev_proof_typs) ~request:(fun () ->
               Req.Proof_with_datas )
@@ -369,7 +369,7 @@ let step_main :
             (Vector.typ (Typ.Internal.ref ()) (Length.to_nat proofs_verified))
             ~request:(fun () -> Req.Wrap_domain_indices)
         in
-        let prevs =
+        let proof_witnesses =
           (* Inject the app-state values into the per-proof witnesses. *)
           let rec go :
               type vars ns1 ns2.
@@ -402,10 +402,10 @@ let step_main :
                        , n )
                        Vector.t
                   -> (_, n) Vector.t * B.t list =
-               fun proofs datas messages_for_next_wrap_proofs unfinalizeds stmts
-                   pi ~actual_wrap_domains ->
+               fun proof_witnesses datas messages_for_next_wrap_proofs
+                   unfinalizeds stmts pi ~actual_wrap_domains ->
                 match
-                  ( proofs
+                  ( proof_witnesses
                   , datas
                   , messages_for_next_wrap_proofs
                   , unfinalizeds
@@ -415,12 +415,12 @@ let step_main :
                 with
                 | [], [], [], [], [], Z, [] ->
                     ([], [])
-                | ( p :: proofs
+                | ( pw :: proof_witnesses
                   , d :: datas
                   , messages_for_next_wrap_proof
                     :: messages_for_next_wrap_proofs
                   , unfinalized :: unfinalizeds
-                  , { proof_must_verify = should_verify; _ } :: stmts
+                  , { proof_must_verify = must_verify; _ } :: stmts
                   , S pi
                   , actual_wrap_domain :: actual_wrap_domains ) ->
                     let () =
@@ -456,12 +456,12 @@ let step_main :
                           ()
                     in
                     let chals, v =
-                      verify_one ~srs p d messages_for_next_wrap_proof
-                        unfinalized should_verify
+                      verify_one ~srs pw d messages_for_next_wrap_proof
+                        unfinalized must_verify
                     in
                     let chalss, vs =
-                      go proofs datas messages_for_next_wrap_proofs unfinalizeds
-                        stmts pi ~actual_wrap_domains
+                      go proof_witnesses datas messages_for_next_wrap_proofs
+                        unfinalizeds stmts pi ~actual_wrap_domains
                     in
                     (chals :: chalss, v :: vs)
               in
@@ -518,26 +518,28 @@ let step_main :
                   in
                   M.f rule.prevs
                 in
-                go prevs datas messages_for_next_wrap_proofs unfinalized_proofs
-                  previous_proof_statements proofs_verified ~actual_wrap_domains
+                go proof_witnesses datas messages_for_next_wrap_proofs
+                  unfinalized_proofs previous_proof_statements proofs_verified
+                  ~actual_wrap_domains
               in
               Boolean.Assert.all vs ; chalss )
         in
         [%log internal] "Step_compute_bulletproof_challenges_done" ;
         let messages_for_next_step_proof =
           let challenge_polynomial_commitments =
             let module M =
-              H3.Map (Per_proof_witness) (E03 (Inner_curve))
+              H3.Map (Per_proof_witness) (E03 (Step_verifier.Inner_curve))
                 (struct
                   let f :
-                      type a b c. (a, b, c) Per_proof_witness.t -> Inner_curve.t
-                      =
+                      type a b c.
+                         (a, b, c) Per_proof_witness.t
+                      -> Step_verifier.Inner_curve.t =
                    fun acc ->
                     acc.wrap_proof.opening.challenge_polynomial_commitment
                 end)
             in
-            let module V = H3.To_vector (Inner_curve) in
-            V.f proofs_verified (M.f prevs)
+            let module V = H3.To_vector (Step_verifier.Inner_curve) in
+            V.f proofs_verified (M.f proof_witnesses)
           in
           with_label "hash_messages_for_next_step_proof" (fun () ->
               let hash_messages_for_next_step_proof =
@@ -546,8 +548,8 @@ let step_main :
                   fun x -> fst (typ.var_to_fields x)
                 in
                 unstage
-                  (hash_messages_for_next_step_proof ~index:dlog_plonk_index
-                     to_field_elements )
+                  (Step_verifier.hash_messages_for_next_step_proof
+                     ~index:dlog_plonk_index to_field_elements )
               in
               let (app_state : var) =
                 match public_input with