feat(avm): avm replace zeromorph pcs by shplemini

barretenberg/cpp/src/barretenberg/dsl/acir_format/avm_recursion_constraint.cpp

@@ -45,17 +45,15 @@ void create_dummy_vkey_and_proof(Builder& builder,
 
     // Relevant source for proof layout: AvmFlavor::Transcript::serialize_full_transcript()
     assert((proof_size - Flavor::NUM_WITNESS_ENTITIES * Flavor::NUM_FRS_COM -
-            Flavor::NUM_ALL_ENTITIES * Flavor::NUM_FRS_FR - 2 * Flavor::NUM_FRS_COM - Flavor::NUM_FRS_FR) %
-               (Flavor::NUM_FRS_COM + Flavor::NUM_FRS_FR * Flavor::BATCHED_RELATION_PARTIAL_LENGTH) ==
+            (Flavor::NUM_ALL_ENTITIES + 1) * Flavor::NUM_FRS_FR - Flavor::NUM_FRS_COM) %
+               (Flavor::NUM_FRS_COM + Flavor::NUM_FRS_FR * (Flavor::BATCHED_RELATION_PARTIAL_LENGTH + 1)) ==
            0);
 
     // Derivation of circuit size based on the proof
-    // Here, we should always get CONST_PROOF_SIZE_LOG_N which is not what is
-    // usually set for the AVM proof. As it is a dummy key/proof, it should not matter.
-    auto log_circuit_size =
-        (proof_size - Flavor::NUM_WITNESS_ENTITIES * Flavor::NUM_FRS_COM -
-         Flavor::NUM_ALL_ENTITIES * Flavor::NUM_FRS_FR - 2 * Flavor::NUM_FRS_COM - Flavor::NUM_FRS_FR) /
-        (Flavor::NUM_FRS_COM + Flavor::NUM_FRS_FR * Flavor::BATCHED_RELATION_PARTIAL_LENGTH);
+    // Here, we should always get CONST_PROOF_SIZE_LOG_N.
+    auto log_circuit_size = (proof_size - Flavor::NUM_WITNESS_ENTITIES * Flavor::NUM_FRS_COM -
+                             (Flavor::NUM_ALL_ENTITIES + 1) * Flavor::NUM_FRS_FR - Flavor::NUM_FRS_COM) /
+                            (Flavor::NUM_FRS_COM + Flavor::NUM_FRS_FR * (Flavor::BATCHED_RELATION_PARTIAL_LENGTH + 1));
 
     /***************************************************************************
      *                  Construct Dummy Verification Key
@@ -109,8 +107,8 @@ void create_dummy_vkey_and_proof(Builder& builder,
         offset++;
     }
 
-    // now the zeromorph commitments
-    for (size_t i = 0; i < CONST_PROOF_SIZE_LOG_N; i++) {
+    // now the gemini fold commitments which are CONST_PROOF_SIZE_LOG_N - 1
+    for (size_t i = 1; i < CONST_PROOF_SIZE_LOG_N; i++) {
         auto comm = curve::BN254::AffineElement::one() * fr::random_element();
         auto frs = field_conversion::convert_to_bn254_frs(comm);
         builder.assert_equal(builder.add_variable(frs[0]), proof_fields[offset].witness_index);
@@ -120,7 +118,13 @@ void create_dummy_vkey_and_proof(Builder& builder,
         offset += 4;
     }
 
-    // lastly the 2 commitments
+    // the gemini fold evaluations which are CONST_PROOF_SIZE_LOG_N
+    for (size_t i = 0; i < CONST_PROOF_SIZE_LOG_N; i++) {
+        builder.assert_equal(builder.add_variable(fr::random_element()), proof_fields[offset].witness_index);
+        offset++;
+    }
+
+    // lastly the shplonk batched quotient commitment and kzg quotient commitment
     for (size_t i = 0; i < 2; i++) {
         auto comm = curve::BN254::AffineElement::one() * fr::random_element();
         auto frs = field_conversion::convert_to_bn254_frs(comm);
@@ -163,14 +167,6 @@ AggregationObjectIndices create_avm_recursion_constraints(Builder& builder,
         key_fields.emplace_back(field);
     }
 
-    // TODO(JEANMON): Once we integrate with public inputs, we will have to decide whether we inject (see
-    // ProofSurgeon::create_indices_for_reconstructed_proof) them as part of proof_fields or through some separate
-    // argument like in the native verifier. The latter will be favored because the public inputs are not part of the
-    // transcript and the verifier code passes the proof to initialize the transcript.
-    // Create witness indices for the
-    // proof with public inputs reinserted std::vector<uint32_t> proof_indices =
-    //     ProofSurgeon::create_indices_for_reconstructed_proof(input.proof, input.public_inputs);
-
     auto fields_from_witnesses = [&](std::vector<uint32_t> const& input) {
         std::vector<field_ct> result;
         result.reserve(input.size());

barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.cpp

@@ -41,14 +41,14 @@ void create_dummy_vkey_and_proof(Builder& builder,
     size_t num_frs_comm = bb::field_conversion::calc_num_bn254_frs<Flavor::Commitment>();
     size_t num_frs_fr = bb::field_conversion::calc_num_bn254_frs<Flavor::FF>();
     assert((proof_size - HONK_RECURSION_PUBLIC_INPUT_OFFSET - Flavor::NUM_WITNESS_ENTITIES * num_frs_comm -
-            Flavor::NUM_ALL_ENTITIES * num_frs_fr - 2 * num_frs_comm) %
-               (num_frs_comm + num_frs_fr * Flavor::BATCHED_RELATION_PARTIAL_LENGTH) ==
+            Flavor::NUM_ALL_ENTITIES * num_frs_fr - num_frs_comm) %
+               (num_frs_comm + num_frs_fr * (Flavor::BATCHED_RELATION_PARTIAL_LENGTH + 1)) ==
            0);
     // Note: this computation should always result in log_circuit_size = CONST_PROOF_SIZE_LOG_N
     auto log_circuit_size =
         (proof_size - HONK_RECURSION_PUBLIC_INPUT_OFFSET - Flavor::NUM_WITNESS_ENTITIES * num_frs_comm -
-         Flavor::NUM_ALL_ENTITIES * num_frs_fr - 2 * num_frs_comm) /
-        (num_frs_comm + num_frs_fr * Flavor::BATCHED_RELATION_PARTIAL_LENGTH);
+         Flavor::NUM_ALL_ENTITIES * num_frs_fr - num_frs_comm) /
+        (num_frs_comm + num_frs_fr * (Flavor::BATCHED_RELATION_PARTIAL_LENGTH + 1));
     // First key field is circuit size
     builder.assert_equal(builder.add_variable(1 << log_circuit_size), key_fields[0].witness_index);
     // Second key field is number of public inputs

barretenberg/cpp/src/barretenberg/eccvm/eccvm_prover.cpp

@@ -107,8 +107,6 @@ void ECCVMProver::execute_relation_check_rounds()
  * @brief Produce a univariate opening claim for the sumcheck multivariate evalutions and a batched univariate claim
  * for the transcript polynomials (for the Translator consistency check). Reduce the two opening claims to a single one
  * via Shplonk and produce an opening proof with the univariate PCS of choice (IPA when operating on Grumpkin).
- * @details See https://hackmd.io/dlf9xEwhTQyE3hiGbq4FsA?view for a complete description of the unrolled ZeroMorph
- * protocol.
  *
  */
 void ECCVMProver::execute_pcs_rounds()

barretenberg/cpp/src/barretenberg/stdlib/translator_vm_verifier/translator_recursive_verifier.cpp

@@ -114,9 +114,6 @@ std::array<typename Flavor::GroupElement, 2> TranslatorRecursiveVerifier_<Flavor
     auto [multivariate_challenge, claimed_evaluations, sumcheck_verified] =
         sumcheck.verify(relation_parameters, alpha, gate_challenges);
 
-    // Execute ZeroMorph rounds followed by the univariate PCS. See https://hackmd.io/dlf9xEwhTQyE3hiGbq4FsA?view for a
-    // complete description of the unrolled protocol.
-
     const BatchOpeningClaim<Curve> opening_claim =
         Shplemini::compute_batch_opening_claim(circuit_size,
                                                commitments.get_unshifted_without_concatenated(),

barretenberg/cpp/src/barretenberg/sumcheck/sumcheck_output.hpp

@@ -9,7 +9,7 @@ namespace bb {
 /**
  * @brief Contains the evaluations of multilinear polynomials \f$ P_1, \ldots, P_N\f$ at the challenge point \f$\vec u
  * =(u_0,\ldots, u_{d-1})\f$. These are computed by \ref bb::SumcheckProver< Flavor > "Sumcheck Prover" and need to be
- * checked using Zeromorph.
+ * checked using Shplemini.
  */
 template <typename Flavor, typename = void> struct SumcheckOutput {
     using FF = typename Flavor::FF;

barretenberg/cpp/src/barretenberg/translator_vm/translator_flavor.hpp

@@ -279,7 +279,7 @@ class TranslatorFlavor {
                                OrderedRangeConstraints<DataType>::get_all());
         };
 
-        // everything but ConcatenatedRangeConstraints (used for ZeroMorph input since concatenated handled separately)
+        // everything but ConcatenatedRangeConstraints (used for Shplemini input since concatenated handled separately)
         // TODO(https://github.com/AztecProtocol/barretenberg/issues/810)
         auto get_unshifted_without_concatenated()
         {

barretenberg/cpp/src/barretenberg/translator_vm/translator_prover.cpp

@@ -162,11 +162,11 @@ void TranslatorProver::execute_relation_check_rounds()
 }
 
 /**
- * @brief Execute the ZeroMorph protocol to produce an opening claim for the multilinear evaluations produced by
- * Sumcheck and then produce an opening proof with a univariate PCS
- * @details See https://hackmd.io/dlf9xEwhTQyE3hiGbq4FsA?view for a complete description of the unrolled protocol.
+ * @brief Produce a univariate opening claim for the sumcheck multivariate evalutions and a batched univariate claim
+ * for the transcript polynomials (for the Translator consistency check). Reduce the two opening claims to a single one
+ * via Shplonk and produce an opening proof with the univariate PCS of choice (IPA when operating on Grumpkin).
  *
- * */
+ */
 void TranslatorProver::execute_pcs_rounds()
 {
     using Curve = typename Flavor::Curve;
@@ -210,7 +210,7 @@ HonkProof TranslatorProver::construct_proof()
     execute_relation_check_rounds();
 
     // Fiat-Shamir: rho, y, x, z
-    // Execute Zeromorph multilinear PCS
+    // Execute Shplemini PCS
     execute_pcs_rounds();
 
     return export_proof();

barretenberg/cpp/src/barretenberg/translator_vm/translator_verifier.cpp

@@ -110,9 +110,6 @@ bool TranslatorVerifier::verify_proof(const HonkProof& proof)
         return false;
     }
 
-    // Execute ZeroMorph rounds. See https://hackmd.io/dlf9xEwhTQyE3hiGbq4FsA?view for a complete description ofthe
-    // unrolled protocol.
-
     const BatchOpeningClaim<Curve> opening_claim =
         Shplemini::compute_batch_opening_claim(circuit_size,
                                                commitments.get_unshifted_without_concatenated(),

barretenberg/cpp/src/barretenberg/ultra_honk/decider_prover.cpp

@@ -41,11 +41,11 @@ template <IsUltraFlavor Flavor> void DeciderProver_<Flavor>::execute_relation_ch
 }
 
 /**
- * @brief Execute the ZeroMorph protocol to produce an opening claim for the multilinear evaluations produced by
- * Sumcheck and then produce an opening proof with a univariate PCS.
- * @details See https://hackmd.io/dlf9xEwhTQyE3hiGbq4FsA?view for a complete description of the unrolled protocol.
+ * @brief Produce a univariate opening claim for the sumcheck multivariate evalutions and a batched univariate claim
+ * for the transcript polynomials (for the Translator consistency check). Reduce the two opening claims to a single one
+ * via Shplonk and produce an opening proof with the univariate PCS of choice (IPA when operating on Grumpkin).
  *
- * */
+ */
 template <IsUltraFlavor Flavor> void DeciderProver_<Flavor>::execute_pcs_rounds()
 {
     if (proving_key->proving_key.commitment_key == nullptr) {
@@ -82,8 +82,8 @@ template <IsUltraFlavor Flavor> HonkProof DeciderProver_<Flavor>::construct_proo
     execute_relation_check_rounds();
 
     // Fiat-Shamir: rho, y, x, z
-    // Execute Zeromorph multilinear PCS
-    vinfo("executing pcd opening rounds...");
+    // Execute Shplemini PCS
+    vinfo("executing pcs opening rounds...");
     execute_pcs_rounds();
 
     return export_proof();

barretenberg/cpp/src/barretenberg/ultra_honk/decider_prover.hpp

@@ -1,6 +1,5 @@
 #pragma once
 #include "barretenberg/commitment_schemes/shplonk/shplemini.hpp"
-#include "barretenberg/commitment_schemes/zeromorph/zeromorph.hpp"
 #include "barretenberg/honk/proof_system/types/proof.hpp"
 #include "barretenberg/relations/relation_parameters.hpp"
 #include "barretenberg/stdlib_circuit_builders/mega_flavor.hpp"

barretenberg/cpp/src/barretenberg/ultra_honk/decider_verification_key.hpp

@@ -6,7 +6,7 @@
 namespace bb {
 /**
  * @brief The DeciderVerificationKey encapsulates all the necessary information for a Mega Honk Verifier to verify a
- * proof (sumcheck + Zeromorph). In the context of folding, this is returned by the Protogalaxy verifier with non-zero
+ * proof (sumcheck + Shplemini). In the context of folding, this is returned by the Protogalaxy verifier with non-zero
  * target sum and gate challenges.
  *
  * @details This is ϕ in the paper.

barretenberg/cpp/src/barretenberg/ultra_honk/decider_verifier.cpp

@@ -1,6 +1,5 @@
 #include "decider_verifier.hpp"
 #include "barretenberg/commitment_schemes/shplonk/shplemini.hpp"
-#include "barretenberg/commitment_schemes/zeromorph/zeromorph.hpp"
 #include "barretenberg/numeric/bitop/get_msb.hpp"
 #include "barretenberg/sumcheck/sumcheck.hpp"
 #include "barretenberg/transcript/transcript.hpp"

barretenberg/cpp/src/barretenberg/ultra_honk/ultra_prover.hpp

@@ -1,5 +1,4 @@
 #pragma once
-#include "barretenberg/commitment_schemes/zeromorph/zeromorph.hpp"
 #include "barretenberg/honk/proof_system/types/proof.hpp"
 #include "barretenberg/relations/relation_parameters.hpp"
 #include "barretenberg/stdlib_circuit_builders/mega_flavor.hpp"
@@ -24,7 +23,6 @@ template <IsUltraFlavor Flavor_> class UltraProver_ {
     using DeciderProvingKey = DeciderProvingKey_<Flavor>;
     using DeciderPK = DeciderProvingKey;
     using Transcript = typename Flavor::Transcript;
-    using ZeroMorph = ZeroMorphProver_<PCS>;
 
     std::shared_ptr<DeciderPK> proving_key;
 

barretenberg/cpp/src/barretenberg/ultra_honk/ultra_verifier.cpp

@@ -1,5 +1,4 @@
 #include "./ultra_verifier.hpp"
-#include "barretenberg/commitment_schemes/zeromorph/zeromorph.hpp"
 #include "barretenberg/numeric/bitop/get_msb.hpp"
 #include "barretenberg/transcript/transcript.hpp"
 #include "barretenberg/ultra_honk/oink_verifier.hpp"

barretenberg/cpp/src/barretenberg/vm/avm/generated/flavor.cpp

@@ -2321,53 +2321,63 @@ AvmFlavor::CommitmentLabels::CommitmentLabels()
     Base::incl_mem_tag_err_counts = "INCL_MEM_TAG_ERR_COUNTS";
 };
 
-// Note: current de-/serialization routines are not including the padded zero univariates which are added as part of
-// current sumcheck implementation. Namely, this algorithm is padding to reach CONST_PROOF_SIZE_LOG_N sumcheck rounds.
-// Similarly, zeromorph implementation performs same padding over some commitments (zm_cq_comms).
-// In code below, the loops are of size log(circuit_size) instead of CONST_PROOF_SIZE_LOG_N.
 void AvmFlavor::Transcript::deserialize_full_transcript()
 {
     size_t num_frs_read = 0;
     circuit_size = deserialize_from_buffer<uint32_t>(proof_data, num_frs_read);
-    size_t log_n = numeric::get_msb(circuit_size);
 
     for (auto& commitment : commitments) {
         commitment = deserialize_from_buffer<Commitment>(proof_data, num_frs_read);
     }
-    for (size_t i = 0; i < log_n; ++i) {
+
+    for (size_t i = 0; i < CONST_PROOF_SIZE_LOG_N; ++i) {
         sumcheck_univariates.emplace_back(deserialize_from_buffer<bb::Univariate<FF, BATCHED_RELATION_PARTIAL_LENGTH>>(
             Transcript::proof_data, num_frs_read));
     }
+
     sumcheck_evaluations =
         deserialize_from_buffer<std::array<FF, NUM_ALL_ENTITIES>>(Transcript::proof_data, num_frs_read);
-    for (size_t i = 0; i < log_n; ++i) {
-        zm_cq_comms.push_back(deserialize_from_buffer<Commitment>(proof_data, num_frs_read));
+
+    for (size_t i = 0; i < CONST_PROOF_SIZE_LOG_N - 1; ++i) {
+        gemini_fold_comms.push_back(deserialize_from_buffer<Commitment>(proof_data, num_frs_read));
     }
-    zm_cq_comm = deserialize_from_buffer<Commitment>(proof_data, num_frs_read);
-    zm_pi_comm = deserialize_from_buffer<Commitment>(proof_data, num_frs_read);
+
+    for (size_t i = 0; i < CONST_PROOF_SIZE_LOG_N; ++i) {
+        gemini_fold_evals.push_back(deserialize_from_buffer<FF>(proof_data, num_frs_read));
+    }
+
+    shplonk_q_comm = deserialize_from_buffer<Commitment>(proof_data, num_frs_read);
+
+    kzg_w_comm = deserialize_from_buffer<Commitment>(proof_data, num_frs_read);
 }
 
-// See note above AvmFlavor::Transcript::deserialize_full_transcript()
 void AvmFlavor::Transcript::serialize_full_transcript()
 {
     size_t old_proof_length = proof_data.size();
     Transcript::proof_data.clear();
-    size_t log_n = numeric::get_msb(circuit_size);
 
     serialize_to_buffer(circuit_size, Transcript::proof_data);
 
     for (const auto& commitment : commitments) {
         serialize_to_buffer(commitment, Transcript::proof_data);
     }
-    for (size_t i = 0; i < log_n; ++i) {
+
+    for (size_t i = 0; i < CONST_PROOF_SIZE_LOG_N; ++i) {
         serialize_to_buffer(sumcheck_univariates[i], Transcript::proof_data);
     }
+
     serialize_to_buffer(sumcheck_evaluations, Transcript::proof_data);
-    for (size_t i = 0; i < log_n; ++i) {
-        serialize_to_buffer(zm_cq_comms[i], proof_data);
+
+    for (size_t i = 0; i < CONST_PROOF_SIZE_LOG_N - 1; ++i) {
+        serialize_to_buffer(gemini_fold_comms[i], proof_data);
     }
-    serialize_to_buffer(zm_cq_comm, proof_data);
-    serialize_to_buffer(zm_pi_comm, proof_data);
+
+    for (size_t i = 0; i < CONST_PROOF_SIZE_LOG_N; ++i) {
+        serialize_to_buffer(gemini_fold_evals[i], proof_data);
+    }
+
+    serialize_to_buffer(shplonk_q_comm, proof_data);
+    serialize_to_buffer(kzg_w_comm, proof_data);
 
     // sanity check to make sure we generate the same length of proof as before.
     ASSERT(proof_data.size() == old_proof_length);

barretenberg/cpp/src/barretenberg/vm/avm/generated/flavor.hpp

@@ -240,8 +240,8 @@ class AvmFlavor {
     // After any circuit changes, hover `COMPUTED_AVM_PROOF_LENGTH_IN_FIELDS` in your IDE
     // to see its value and then update `AVM_PROOF_LENGTH_IN_FIELDS` in constants.nr.
     static constexpr size_t COMPUTED_AVM_PROOF_LENGTH_IN_FIELDS =
-        (NUM_WITNESS_ENTITIES + 2) * NUM_FRS_COM + (NUM_ALL_ENTITIES + 1) * NUM_FRS_FR +
-        CONST_PROOF_SIZE_LOG_N * (NUM_FRS_COM + NUM_FRS_FR * BATCHED_RELATION_PARTIAL_LENGTH);
+        (NUM_WITNESS_ENTITIES + 1) * NUM_FRS_COM + (NUM_ALL_ENTITIES + 1) * NUM_FRS_FR +
+        CONST_PROOF_SIZE_LOG_N * (NUM_FRS_COM + NUM_FRS_FR * (BATCHED_RELATION_PARTIAL_LENGTH + 1));
 
     static_assert(AVM_PROOF_LENGTH_IN_FIELDS == COMPUTED_AVM_PROOF_LENGTH_IN_FIELDS,
                   "\nUnexpected AVM proof length. This might be due to some changes in the\n"
@@ -499,9 +499,10 @@ class AvmFlavor {
 
         std::vector<bb::Univariate<FF, BATCHED_RELATION_PARTIAL_LENGTH>> sumcheck_univariates;
         std::array<FF, NUM_ALL_ENTITIES> sumcheck_evaluations;
-        std::vector<Commitment> zm_cq_comms;
-        Commitment zm_cq_comm;
-        Commitment zm_pi_comm;
+        std::vector<Commitment> gemini_fold_comms;
+        std::vector<FF> gemini_fold_evals;
+        Commitment shplonk_q_comm;
+        Commitment kzg_w_comm;
 
         Transcript() = default;
 

barretenberg/cpp/src/barretenberg/vm/avm/generated/prover.cpp

@@ -1,16 +1,15 @@
 // AUTOGENERATED FILE
 #include "barretenberg/vm/avm/generated/prover.hpp"
-
 #include "barretenberg/commitment_schemes/claim.hpp"
 #include "barretenberg/commitment_schemes/commitment_key.hpp"
+#include "barretenberg/commitment_schemes/shplonk/shplemini.hpp"
 #include "barretenberg/common/constexpr_utils.hpp"
 #include "barretenberg/common/thread.hpp"
 #include "barretenberg/honk/proof_system/logderivative_library.hpp"
 #include "barretenberg/honk/proof_system/permutation_library.hpp"
 #include "barretenberg/plonk_honk_shared/library/grand_product_library.hpp"
 #include "barretenberg/relations/permutation_relation.hpp"
 #include "barretenberg/sumcheck/sumcheck.hpp"
-
 #include "barretenberg/vm/stats.hpp"
 
 namespace bb {
@@ -109,20 +108,17 @@ void AvmProver::execute_relation_check_rounds()
     sumcheck_output = sumcheck.prove(prover_polynomials, relation_parameters, alpha, gate_challenges);
 }
 
-/**
- * @brief Execute the ZeroMorph protocol to prove the multilinear evaluations produced by Sumcheck
- * @details See https://hackmd.io/dlf9xEwhTQyE3hiGbq4FsA?view for a complete description of the unrolled protocol.
- */
 void AvmProver::execute_pcs_rounds()
 {
-    auto prover_opening_claim = ZeroMorph::prove(key->circuit_size,
-                                                 prover_polynomials.get_unshifted(),
-                                                 prover_polynomials.get_to_be_shifted(),
-                                                 sumcheck_output.claimed_evaluations.get_unshifted(),
-                                                 sumcheck_output.claimed_evaluations.get_shifted(),
-                                                 sumcheck_output.challenge,
-                                                 commitment_key,
-                                                 transcript);
+    using OpeningClaim = ProverOpeningClaim<Curve>;
+
+    const OpeningClaim prover_opening_claim = ShpleminiProver_<Curve>::prove(key->circuit_size,
+                                                                             prover_polynomials.get_unshifted(),
+                                                                             prover_polynomials.get_to_be_shifted(),
+                                                                             sumcheck_output.challenge,
+                                                                             commitment_key,
+                                                                             transcript);
+
     PCS::compute_opening_proof(commitment_key, prover_opening_claim, transcript);
 }
 
@@ -152,7 +148,7 @@ HonkProof AvmProver::construct_proof()
     AVM_TRACK_TIME("prove/execute_relation_check_rounds", execute_relation_check_rounds());
 
     // Fiat-Shamir: rho, y, x, z
-    // Execute Zeromorph multilinear PCS
+    // Execute Shplemini PCS
     AVM_TRACK_TIME("prove/execute_pcs_rounds", execute_pcs_rounds());
 
     return export_proof();