two_layer_avm_recursive_verifier.hpp

Go to the documentation of this file.

// === AUDIT STATUS ===
// internal:    { status: Completed, auditors: [Federico], commit: }
// external_1:  { status: not started, auditors: [], commit: }
// external_2:  { status: not started, auditors: [], commit: }
// =====================
#pragma once
 
#include "barretenberg/circuit_checker/circuit_checker.hpp"
#include "barretenberg/flavor/mega_avm_flavor.hpp"
#include "barretenberg/flavor/mega_avm_recursive_flavor.hpp"
#include "barretenberg/flavor/mega_flavor.hpp"
#include "barretenberg/flavor/mega_recursive_flavor.hpp"
#include "barretenberg/goblin_avm/goblin_avm.hpp"
#include "barretenberg/goblin_avm/goblin_avm_verifier.hpp"
#include "barretenberg/stdlib/hash/poseidon2/poseidon2.hpp"
#include "barretenberg/stdlib/special_public_inputs/special_public_inputs.hpp"
#include "barretenberg/ultra_honk/ultra_prover.hpp"
#include "barretenberg/ultra_honk/ultra_verifier.hpp"
#include "barretenberg/vm2/common/avm_io.hpp"
#include "barretenberg/vm2/constraining/recursion/recursive_flavor.hpp"
#include "barretenberg/vm2/constraining/recursion/recursive_verifier.hpp"
 
namespace bb::avm2 {
 
class TwoLayerAvmRecursiveVerifier {
  public:
    using MegaPairingPoints = bb::stdlib::recursion::PairingPoints<stdlib::bn254<MegaCircuitBuilder>>;
 
    using UltraFF = stdlib::field_t<UltraCircuitBuilder>;
    using MegaFF = stdlib::field_t<MegaCircuitBuilder>;
 
    // The output of the goblinized AVM2 recursive verifier
    using TwoLayerAvmRecursiveVerifierOutput =
        stdlib::recursion::honk::UltraRecursiveVerifierOutput<UltraCircuitBuilder>;
 
    // Output of prover for inner Mega-arithmetized AVM recursive verifier circuit; input to the outer verifier
    struct InnerProverOutput {
        HonkProof mega_proof;                                    // \pi_M
        GoblinAvmProof goblin_proof;                             // \pi_G
        std::shared_ptr<MegaAvmFlavor::VerificationKey> mega_vk; // VK_M
    };
 
  private:
    UltraCircuitBuilder* outer_builder;
 
  public:
    explicit TwoLayerAvmRecursiveVerifier(UltraCircuitBuilder& builder)
        : outer_builder(&builder) {};
    [[nodiscard("IPA claim and Pairing points should be accumulated")]] TwoLayerAvmRecursiveVerifierOutput verify_proof(
        const stdlib::Proof<UltraCircuitBuilder>& stdlib_proof,
        const std::vector<std::vector<UltraFF>>& public_inputs) const
    {
        // Construct and prove the inner Mega-arithmetized AVM recursive verifier circuit; proof is {\pi_M, \pi_G}
        InnerProverOutput inner_output =
            construct_and_prove_inner_recursive_verification_circuit(stdlib_proof, public_inputs);
 
        // Construct the outer Ultra-arithmetized Mega/Goblin recursive verifier circuit
        TwoLayerAvmRecursiveVerifierOutput result =
            construct_outer_recursive_verification_circuit(stdlib_proof, public_inputs, inner_output);
 
        // Return ipa proof, ipa claim and output aggregation object produced from verifying the Mega + Goblin proofs
        return result;
    }
 
    [[nodiscard("IPA claim and Pairing points should be accumulated")]] TwoLayerAvmRecursiveVerifierOutput
    construct_outer_recursive_verification_circuit(const stdlib::Proof<UltraCircuitBuilder>& stdlib_proof,
                                                   const std::vector<std::vector<UltraFF>>& public_inputs,
                                                   const InnerProverOutput& inner_output) const
    {
        // Types for MegaRecursiveVerifier specialized for the AVM
        using MegaAvmRecursiveFlavor = MegaAvmRecursiveFlavor_<UltraCircuitBuilder>;
        using MegaRecursiveVKAndHash = MegaAvmRecursiveFlavor::VKAndHash;
        using IO = stdlib::recursion::honk::GoblinAvmIO<UltraCircuitBuilder>;
        using MegaAvmRecursiveVerifier = UltraVerifier_<MegaAvmRecursiveFlavor, IO>;
 
        // Step 1: Recursively verify the Mega proof \pi_M
        auto transcript = std::make_shared<MegaAvmRecursiveFlavor::Transcript>(); // Single shared transcript
        auto mega_vk_and_hash = std::make_shared<MegaRecursiveVKAndHash>(*outer_builder, inner_output.mega_vk);
 
        // The vk of the inner Mega arithmetized AVM recursive verifier circuit must be fixed to ensure that the outer
        // circuit verifies the validity of the intended inner circuit.
        mega_vk_and_hash->vk->fix_witness();
        mega_vk_and_hash->hash.fix_witness();
 
        MegaAvmRecursiveVerifier mega_verifier(mega_vk_and_hash, transcript);
        stdlib::Proof<UltraCircuitBuilder> mega_proof(*outer_builder, inner_output.mega_proof);
        auto mega_verifier_output = mega_verifier.verify_proof(mega_proof);
 
        // Step 2: Recursively verify the goblin proof \pi_G
        GoblinAvmStdlibProof stdlib_goblin_proof(*outer_builder, inner_output.goblin_proof);
        GoblinAvmRecursiveVerifier goblin_verifier{ transcript, stdlib_goblin_proof, mega_verifier.get_ecc_op_wires() };
        auto goblin_verifier_output = goblin_verifier.reduce_to_pairing_check_and_ipa_opening();
 
        // Step 3: Aggregate pairing points coming from Mega verification and Goblin verification
        mega_verifier_output.points_accumulator.aggregate(goblin_verifier_output.translator_pairing_points);
 
        // Step 4: Validate the consistency of the AVM2 verifier inputs {\pi, pub_inputs}_{AVM2} between the inner
        // (Mega) circuit and the outer (Ultra) by asserting equality on the independently computed hashes
        const UltraFF computed_transcript_hash =
            AvmRecursiveFlavor::UltraTranscript::hash_avm_transcript(*outer_builder, stdlib_proof, public_inputs);
        mega_verifier_output.transcript_hash.assert_equal(computed_transcript_hash);
 
        // Return ipa proof, ipa claim and output aggregation object produced from verifying the Mega + Goblin
        // proofs
        TwoLayerAvmRecursiveVerifierOutput output;
        output.points_accumulator = std::move(mega_verifier_output.points_accumulator);
        output.ipa_claim = goblin_verifier_output.ipa_claim;
        output.ipa_proof = goblin_verifier_output.ipa_proof;
        return output;
    }
 
    static InnerProverOutput construct_and_prove_inner_recursive_verification_circuit(
        const stdlib::Proof<UltraCircuitBuilder>& stdlib_proof, const std::vector<std::vector<UltraFF>>& public_inputs)
    {
        using MegaAvmProverInstance = ProverInstance_<MegaAvmFlavor>;
        using MegaAvmVerificationKey = MegaAvmFlavor::VerificationKey;
        using MegaAvmProver = UltraProver_<MegaAvmFlavor>;
 
        // Instantiate Mega builder for the inner circuit (AVM2 proof recursive verifier)
        MegaCircuitBuilder inner_builder;
        GoblinAvm goblin(inner_builder);
 
        // Construct the inner recursive verification circuit
        construct_inner_recursive_verification_circuit(inner_builder, stdlib_proof, public_inputs);
 
        // Construct the Mega proof \pi_M of the AVM recursive verifier circuit
        auto transcript = std::make_shared<NativeTranscript>(); // Single shared transcript
        auto mega_proving_key = std::make_shared<MegaAvmProverInstance>(inner_builder);
        // Detect when MEGA_AVM_LOG_N needs to be bumped.
        BB_ASSERT_LTE(
            mega_proving_key->log_dyadic_size(),
            MEGA_AVM_LOG_N,
            "AVMRecursiveVerifier: circuit size exceeded current upper bound. If expected, bump MEGA_AVM_LOG_N");
        auto mega_vk = std::make_shared<MegaAvmVerificationKey>(mega_proving_key->get_precomputed());
        MegaAvmProver mega_prover(mega_proving_key, mega_vk, transcript);
        HonkProof mega_proof = mega_prover.construct_proof();
 
        // Construct the GoblinAvm proof \pi_G (includes ECCVM, IPA, and Translator proofs)
        goblin.transcript = transcript;
        GoblinAvmProof goblin_proof = goblin.prove();
 
        return {
            .mega_proof = mega_proof,
            .goblin_proof = goblin_proof,
            .mega_vk = mega_vk,
        };
    }
 
    static void construct_inner_recursive_verification_circuit(MegaCircuitBuilder& inner_builder,
                                                               const stdlib::Proof<UltraCircuitBuilder>& stdlib_proof,
                                                               const std::vector<std::vector<UltraFF>>& public_inputs)
    {
        using IO = stdlib::recursion::honk::GoblinAvmIO<MegaCircuitBuilder>;
 
        // Create free witnesses representing the AVM proof and public inputs in the inner circuit.
        // The honest prover sets these values to match the values of the proof and public inputs in the outer circuit.
        // Consistency between these witnesses and the ones in the outer circuit is enforced via a hash check.
        stdlib::Proof<MegaCircuitBuilder> inner_stdlib_proof(inner_builder, stdlib_proof.get_value());
        std::vector<std::vector<MegaFF>> inner_public_inputs;
        inner_public_inputs.reserve(AVM_NUM_PUBLIC_INPUT_COLUMNS);
        for (const auto& public_input_column : public_inputs) {
            std::vector<MegaFF> inner_public_input_column;
            inner_public_input_column.reserve(AVM_PUBLIC_INPUTS_COLUMNS_MAX_LENGTH);
            for (const auto& public_input : public_input_column) {
                inner_public_input_column.push_back(MegaFF::from_witness(&inner_builder, public_input.get_value()));
            }
            inner_public_inputs.push_back(std::move(inner_public_input_column));
        }
 
        // Construct a Mega-arithmetized AVM2 recursive verifier circuit
        // The constructor of AvmRecursiveVerifier hard-codes the VK and the VK hash of the AVM2 by copying the values
        // into the selectors.
        AvmRecursiveVerifier recursive_verifier{ inner_builder };
        MegaPairingPoints points_accumulator = recursive_verifier.verify_proof(inner_stdlib_proof, inner_public_inputs);
 
        // Append to the transcript the padding values of the proof (if any) and generate a challenge to record the
        // final state of the transcript of the AVM recursive verifier
        const MegaFF transcript_hash = recursive_verifier.hash_avm_transcript(inner_stdlib_proof);
 
        // Public inputs
        IO inputs;
        inputs.transcript_hash = transcript_hash;
        inputs.pairing_inputs = points_accumulator;
        inputs.set_public();
    }
};
 
} // namespace bb::avm2