goblin_avm_recursive_verifier.hpp

Go to the documentation of this file.

#pragma once
 
#include "barretenberg/circuit_checker/circuit_checker.hpp"
#include "barretenberg/flavor/mega_flavor.hpp"
#include "barretenberg/flavor/mega_recursive_flavor.hpp"
#include "barretenberg/goblin/goblin.hpp"
#include "barretenberg/stdlib/goblin_verifier/goblin_recursive_verifier.hpp"
#include "barretenberg/stdlib/hash/poseidon2/poseidon2.hpp"
#include "barretenberg/stdlib/honk_verifier/ultra_recursive_verifier.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/constraining/recursion/recursive_flavor.hpp"
#include "barretenberg/vm2/constraining/recursion/recursive_verifier.hpp"
 
namespace bb::avm2 {
 
class AvmGoblinRecursiveVerifier {
  public:
    using UltraBuilder = UltraCircuitBuilder;
    using MegaBuilder = MegaCircuitBuilder;
 
    using PairingPoints = bb::stdlib::recursion::PairingPoints<UltraBuilder>;
    using MegaPairingPoints = bb::stdlib::recursion::PairingPoints<MegaBuilder>;
 
    using UltraFF = stdlib::bn254<UltraBuilder>::ScalarField;
 
    // The structure of the final output of the goblinized AVM2 recursive verifier. The IPA data comes from recursive
    // verification of the ECCVM proof as part of Goblin recursive verification.
    using RecursiveAvmGoblinOutput = stdlib::recursion::honk::UltraRecursiveVerifierOutput<UltraBuilder>;
 
    // Output of prover for inner Mega-arithmetized AVM recursive verifier circuit; input to the outer verifier
    struct InnerProverOutput {
        HonkProof mega_proof;                                 // \pi_M
        GoblinProof goblin_proof;                             // \pi_G
        std::shared_ptr<MegaFlavor::VerificationKey> mega_vk; // VK_M
        Goblin::VerificationKey goblin_vk;                    // VK_G
    };
 
    UltraBuilder& ultra_builder;
    std::vector<UltraFF> outer_key_fields;
    UltraFF vk_hash; // this should be a constant witness
 
    explicit AvmGoblinRecursiveVerifier(UltraBuilder& builder, const std::vector<UltraFF>& outer_key_fields)
        : ultra_builder(builder)
        , outer_key_fields(outer_key_fields)
    {
        // TODO(#15892): Set this to be the actual vk hash when vk is fixed.
        vk_hash = UltraFF::from_witness(&builder, /* should be native hash of vk fields*/ 0);
        vk_hash.fix_witness();
    }
 
    [[nodiscard("IPA claim and Pairing points should be accumulated")]] RecursiveAvmGoblinOutput verify_proof(
        const stdlib::Proof<UltraBuilder>& 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
        RecursiveAvmGoblinOutput 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")]] RecursiveAvmGoblinOutput
    construct_outer_recursive_verification_circuit(const stdlib::Proof<UltraBuilder>& stdlib_proof,
                                                   const std::vector<std::vector<UltraFF>>& public_inputs,
                                                   const InnerProverOutput& inner_output) const
    {
        // Types for MegaHonk and Goblin recursive verifiers arithmetized with Ultra
        using MegaRecursiveFlavor = MegaRecursiveFlavor_<UltraBuilder>;
        using MegaRecursiveVKAndHash = MegaRecursiveFlavor::VKAndHash;
        using MegaRecursiveVerifier = stdlib::recursion::honk::UltraRecursiveVerifier_<MegaRecursiveFlavor>;
        using GoblinRecursiveVerifier = stdlib::recursion::honk::GoblinRecursiveVerifier;
        using GoblinRecursiveVerifierOutput = stdlib::recursion::honk::GoblinRecursiveVerifierOutput;
        using MergeCommitments = GoblinRecursiveVerifier::MergeVerifier::InputCommitments;
        using FF = MegaRecursiveFlavor::FF;
        using IO = stdlib::recursion::honk::GoblinAvmIO<UltraBuilder>;
 
        // Construct hash buffer containing the AVM proof, public inputs, and VK
        std::vector<FF> hash_buffer;
        hash_buffer.insert(hash_buffer.end(), stdlib_proof.begin(), stdlib_proof.end());
        for (const std::vector<FF>& input_vec : public_inputs) {
            hash_buffer.insert(hash_buffer.end(), input_vec.begin(), input_vec.end());
        }
        // TODO(#15892): Remove vk from hash buffer when vk/hash are fixed in circuit. Keep the vk_hash in the buffer
        hash_buffer.insert(hash_buffer.end(), outer_key_fields.begin(), outer_key_fields.end());
        hash_buffer.emplace_back(vk_hash);
 
        // Recursively verify the Mega proof \pi_M in the Ultra circuit
        // All verifier components share a single transcript
        auto transcript = std::make_shared<MegaRecursiveFlavor::Transcript>();
        auto mega_vk_and_hash = std::make_shared<MegaRecursiveVKAndHash>(ultra_builder, inner_output.mega_vk);
        // Fix the inner mega vk and vk hash to be constants in the outer circuit.
        mega_vk_and_hash->vk->fix_witness();
        mega_vk_and_hash->hash.fix_witness();
        // TODO(#16352): Figure out how not to add hashing gates to mega recursive verifier.
        MegaRecursiveVerifier mega_verifier(&ultra_builder, mega_vk_and_hash, transcript);
        stdlib::Proof<UltraBuilder> mega_proof(ultra_builder, inner_output.mega_proof);
        auto mega_verifier_output = mega_verifier.template verify_proof<IO>(mega_proof);
 
        // Recursively verify the goblin proof\pi_G in the Ultra circuit
        MergeCommitments merge_commitments{
            .t_commitments = mega_verifier.key->witness_commitments.get_ecc_op_wires().get_copy(),
            .T_prev_commitments = stdlib::recursion::honk::empty_ecc_op_tables(
                ultra_builder) // Empty ecc op tables because there is only one layer of Goblin
        };
        GoblinRecursiveVerifier goblin_verifier{ &ultra_builder, inner_output.goblin_vk, transcript };
        GoblinRecursiveVerifierOutput goblin_verifier_output =
            goblin_verifier.verify(inner_output.goblin_proof, merge_commitments);
        goblin_verifier_output.points_accumulator.aggregate(mega_verifier_output.points_accumulator);
 
        // Validate the consistency of the AVM2 verifier inputs {\pi, pub_inputs, VK}_{AVM2} between the inner (Mega)
        // circuit and the outer (Ultra) by asserting equality on the independently computed hashes of this data.
        const FF ultra_hash = stdlib::poseidon2<UltraBuilder>::hash(ultra_builder, hash_buffer);
        mega_verifier_output.mega_hash.assert_equal(ultra_hash);
 
        // Return ipa proof, ipa claim and output aggregation object produced from verifying the Mega + Goblin proofs
        RecursiveAvmGoblinOutput output;
        output.points_accumulator = goblin_verifier_output.points_accumulator;
        output.ipa_claim = goblin_verifier_output.opening_claim;
        output.ipa_proof = goblin_verifier_output.ipa_proof;
        return output;
    }
 
    InnerProverOutput construct_and_prove_inner_recursive_verification_circuit(
        const stdlib::Proof<UltraBuilder>& stdlib_proof, const std::vector<std::vector<UltraFF>>& public_inputs) const
    {
        using AvmRecursiveVerificationKey = AvmRecursiveFlavor::VerificationKey;
        using ECCVMVK = Goblin::ECCVMVerificationKey;
        using TranslatorVK = Goblin::TranslatorVerificationKey;
        using MegaVerificationKey = MegaFlavor::VerificationKey;
        using FF = AvmRecursiveFlavor::FF;
        using IO = stdlib::recursion::honk::GoblinAvmIO<MegaBuilder>;
 
        // Instantiate Mega builder for the inner circuit (AVM2 proof recursive verifier)
        Goblin goblin;
        MegaBuilder mega_builder(goblin.op_queue);
        mega_builder.queue_ecc_no_op();
 
        // lambda to convert from Ultra to Mega stdlib field buffer and add all elements to respective hash buffers
        std::vector<FF> mega_hash_buffer;
        auto convert_stdlib_ultra_to_stdlib_mega = [&](const std::vector<UltraFF>& ultra_object) {
            std::vector<FF> mega_object;
            for (const UltraFF& ultra_element : ultra_object) {
                FF mega_element = FF::from_witness(&mega_builder, ultra_element.get_value());
                mega_object.emplace_back(mega_element);
                mega_hash_buffer.emplace_back(mega_element);
            }
            return mega_object;
        };
 
        // Convert the AVM proof, public inputs, and VK to stdlib Mega representations and add them to the hash buffer.
        stdlib::Proof<MegaBuilder> mega_stdlib_proof = convert_stdlib_ultra_to_stdlib_mega(stdlib_proof);
        std::vector<std::vector<FF>> mega_public_inputs;
        mega_public_inputs.reserve(public_inputs.size());
        for (const std::vector<UltraFF>& input_vec : public_inputs) {
            mega_public_inputs.emplace_back(convert_stdlib_ultra_to_stdlib_mega(input_vec));
        }
        // TODO(#15892): Remove key_fields from hash buffer when vk/hash are fixed in circuit. Keep the vk_hash in the
        // buffer
        std::vector<FF> key_fields = convert_stdlib_ultra_to_stdlib_mega(outer_key_fields);
        FF mega_vk_hash = convert_stdlib_ultra_to_stdlib_mega({ vk_hash })[0];
        // TODO(#15892): We call fix_witness on the vk hash twice here because we hash it here and also for
        // fiat-shamiring.
        mega_vk_hash.fix_witness(); // fix witness because vk hash should be a circuit constant
 
        // Compute the hash and set it public
        const FF mega_hash = stdlib::poseidon2<MegaBuilder>::hash(mega_builder, mega_hash_buffer);
 
        // Construct a Mega-arithmetized AVM2 recursive verifier circuit
        auto stdlib_key = std::make_shared<AvmRecursiveVerificationKey>(mega_builder, std::span<FF>(key_fields));
        AvmRecursiveVerifier recursive_verifier{ mega_builder, stdlib_key };
        MegaPairingPoints points_accumulator = recursive_verifier.verify_proof(mega_stdlib_proof, mega_public_inputs);
 
        // Public inputs
        IO inputs;
        inputs.mega_hash = mega_hash;
        inputs.pairing_inputs = points_accumulator;
        inputs.set_public();
 
        // All prover components share a single transcript
        std::shared_ptr<Goblin::Transcript> transcript = std::make_shared<Goblin::Transcript>();
        // Construct Mega proof \pi_M of the AVM recursive verifier circuit
        auto mega_proving_key = std::make_shared<DeciderProvingKey_<MegaFlavor>>(mega_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<MegaVerificationKey>(mega_proving_key->get_precomputed());
        MegaProver mega_prover(mega_proving_key, mega_vk, transcript);
        HonkProof mega_proof = mega_prover.construct_proof();
        goblin.transcript = transcript;
 
        // Construct corresponding Goblin proof \pi_G (includes Merge, ECCVM, and Translator proofs)
        GoblinProof goblin_proof = goblin.prove();
 
        // Recursively verify the goblin proof in the Ultra circuit
        Goblin::VerificationKey goblin_vk{ std::make_shared<ECCVMVK>(), std::make_shared<TranslatorVK>() };
 
        return {
            .mega_proof = mega_proof,
            .goblin_proof = goblin_proof,
            .mega_vk = mega_vk,
            .goblin_vk = goblin_vk,
        };
    }
};
 
} // namespace bb::avm2