sp1_recursion_circuit/machine/
vkey_proof.rs

1use crate::{
2    machine::{InnerVal, SP1ShapedWitnessValues},
3    shard::RecursiveShardVerifier,
4};
5use std::marker::PhantomData;
6
7use super::{PublicValuesOutputDigest, SP1CompressVerifier, SP1ShapedWitnessVariable};
8use crate::{
9    basefold::merkle_tree::verify, hash::FieldHasher, zerocheck::RecursiveVerifierConstraintFolder,
10    CircuitConfig, FieldHasherVariable, SP1FieldConfigVariable,
11};
12use serde::{Deserialize, Serialize};
13use slop_air::Air;
14use slop_algebra::AbstractField;
15use sp1_hypercube::{air::MachineAir, MerkleProof};
16use sp1_primitives::{SP1Field, SP1GlobalContext};
17use sp1_recursion_compiler::ir::{Builder, Felt};
18use sp1_recursion_executor::DIGEST_SIZE;
19
20/// A program to verify a batch of recursive proofs and aggregate their public values.
21#[derive(Debug, Clone, Copy)]
22pub struct SP1MerkleProofVerifier<C, SC> {
23    _phantom: PhantomData<(C, SC)>,
24}
25
26#[derive(Clone)]
27pub struct MerkleProofVariable<C: CircuitConfig, HV: FieldHasherVariable<C>> {
28    pub index: Vec<C::Bit>,
29    pub path: Vec<HV::DigestVariable>,
30}
31
32/// Witness layout for the compress stage verifier.
33pub struct SP1MerkleProofWitnessVariable<
34    C: CircuitConfig,
35    SC: FieldHasherVariable<C> + SP1FieldConfigVariable<C>,
36> {
37    /// The shard proofs to verify.
38    pub vk_merkle_proofs: Vec<MerkleProofVariable<C, SC>>,
39    /// Hinted values to enable dummy digests.
40    pub values: Vec<SC::DigestVariable>,
41    /// The root of the merkle tree.
42    pub root: SC::DigestVariable,
43}
44
45/// An input layout for the reduce verifier.
46#[derive(Debug, Clone, Serialize, Deserialize)]
47#[serde(bound(serialize = "GC::Digest: Serialize"))]
48#[serde(bound(deserialize = "GC::Digest: Deserialize<'de>"))]
49pub struct SP1MerkleProofWitnessValues<GC: FieldHasher> {
50    pub vk_merkle_proofs: Vec<MerkleProof<GC>>,
51    pub values: Vec<GC::Digest>,
52    pub root: GC::Digest,
53}
54
55impl<C, SC> SP1MerkleProofVerifier<C, SC>
56where
57    SC: SP1FieldConfigVariable<C>,
58    C: CircuitConfig,
59{
60    /// Verify (via Merkle tree) that the vkey digests of a proof belong to a specified set
61    /// (encoded the Merkle tree proofs in input).
62    pub fn verify(
63        builder: &mut Builder<C>,
64        digests: Vec<SC::DigestVariable>,
65        input: SP1MerkleProofWitnessVariable<C, SC>,
66        value_assertions: bool,
67    ) {
68        let SP1MerkleProofWitnessVariable { vk_merkle_proofs, values, root } = input;
69        for ((proof, value), expected_value) in
70            vk_merkle_proofs.into_iter().zip(values).zip(digests)
71        {
72            verify::<C, SC>(builder, proof.path, proof.index, value, root);
73            if value_assertions {
74                SC::assert_digest_eq(builder, expected_value, value);
75            } else {
76                SC::assert_digest_eq(builder, value, value);
77            }
78        }
79    }
80}
81
82#[derive(Debug, Clone, Copy)]
83pub struct SP1CompressWithVKeyVerifier<C, SC, A> {
84    _phantom: PhantomData<(C, SC, A)>,
85}
86
87/// Witness layout for the verifier of the proof shape phase of the compress stage.
88pub struct SP1CompressWithVKeyWitnessVariable<C: CircuitConfig, GC: SP1FieldConfigVariable<C>> {
89    pub compress_var: SP1ShapedWitnessVariable<C, GC>,
90    pub merkle_var: SP1MerkleProofWitnessVariable<C, GC>,
91}
92
93/// An input layout for the verifier of the proof shape phase of the compress stage.
94#[derive(Serialize, Deserialize)]
95pub struct SP1CompressWithVKeyWitnessValues<Proof> {
96    pub compress_val: SP1ShapedWitnessValues<SP1GlobalContext, Proof>,
97    pub merkle_val: SP1MerkleProofWitnessValues<SP1GlobalContext>,
98}
99
100impl<C, SC, A> SP1CompressWithVKeyVerifier<C, SC, A>
101where
102    C: CircuitConfig<Bit = Felt<SP1Field>>,
103    A: MachineAir<InnerVal> + for<'a> Air<RecursiveVerifierConstraintFolder<'a>>,
104{
105    /// Verify the proof shape phase of the compress stage.
106    pub fn verify(
107        builder: &mut Builder<C>,
108        machine: &RecursiveShardVerifier<SP1GlobalContext, A, C>,
109        input: SP1CompressWithVKeyWitnessVariable<C, SP1GlobalContext>,
110        value_assertions: bool,
111        kind: PublicValuesOutputDigest,
112    ) {
113        let values = input
114            .compress_var
115            .vks_and_proofs
116            .iter()
117            .map(|(vk, _)| vk.hash(builder))
118            .collect::<Vec<_>>();
119        let vk_root = input.merkle_var.root.map(|x| builder.eval(x));
120        SP1MerkleProofVerifier::verify(builder, values, input.merkle_var, value_assertions);
121        SP1CompressVerifier::<C, SP1GlobalContext, _>::verify(
122            builder,
123            machine,
124            input.compress_var,
125            vk_root,
126            kind,
127        );
128    }
129}
130
131impl SP1MerkleProofWitnessValues<SP1GlobalContext> {
132    pub fn dummy(num_proofs: usize, height: usize) -> Self {
133        let dummy_digest = [SP1Field::zero(); DIGEST_SIZE];
134        let vk_merkle_proofs =
135            vec![MerkleProof { index: 0, path: vec![dummy_digest; height] }; num_proofs];
136        let values = vec![dummy_digest; num_proofs];
137
138        Self { vk_merkle_proofs, values, root: dummy_digest }
139    }
140}
sp1_recursion_circuit/machine/vkey_proof.rs

sp1_recursion_circuit/machine/
vkey_proof.rs
