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.
94pub struct SP1CompressWithVKeyWitnessValues<Proof> {
95    pub compress_val: SP1ShapedWitnessValues<SP1GlobalContext, Proof>,
96    pub merkle_val: SP1MerkleProofWitnessValues<SP1GlobalContext>,
97}
98
99impl<C, SC, A> SP1CompressWithVKeyVerifier<C, SC, A>
100where
101    C: CircuitConfig<Bit = Felt<SP1Field>>,
102    A: MachineAir<InnerVal> + for<'a> Air<RecursiveVerifierConstraintFolder<'a>>,
103{
104    /// Verify the proof shape phase of the compress stage.
105    pub fn verify(
106        builder: &mut Builder<C>,
107        machine: &RecursiveShardVerifier<SP1GlobalContext, A, C>,
108        input: SP1CompressWithVKeyWitnessVariable<C, SP1GlobalContext>,
109        value_assertions: bool,
110        kind: PublicValuesOutputDigest,
111    ) {
112        let values = input
113            .compress_var
114            .vks_and_proofs
115            .iter()
116            .map(|(vk, _)| vk.hash(builder))
117            .collect::<Vec<_>>();
118        let vk_root = input.merkle_var.root.map(|x| builder.eval(x));
119        SP1MerkleProofVerifier::verify(builder, values, input.merkle_var, value_assertions);
120        SP1CompressVerifier::<C, SP1GlobalContext, _>::verify(
121            builder,
122            machine,
123            input.compress_var,
124            vk_root,
125            kind,
126        );
127    }
128}
129
130impl SP1MerkleProofWitnessValues<SP1GlobalContext> {
131    pub fn dummy(num_proofs: usize, height: usize) -> Self {
132        let dummy_digest = [SP1Field::zero(); DIGEST_SIZE];
133        let vk_merkle_proofs =
134            vec![MerkleProof { index: 0, path: vec![dummy_digest; height] }; num_proofs];
135        let values = vec![dummy_digest; num_proofs];
136
137        Self { vk_merkle_proofs, values, root: dummy_digest }
138    }
139}
sp1_recursion_circuit/machine/vkey_proof.rs

sp1_recursion_circuit/machine/
vkey_proof.rs
