sp1_recursion_program/machine/
deferred.rs

1use std::{
2    array,
3    borrow::{Borrow, BorrowMut},
4    marker::PhantomData,
5};
6
7use p3_air::Air;
8use p3_baby_bear::BabyBear;
9use p3_commit::TwoAdicMultiplicativeCoset;
10use p3_field::{AbstractField, PrimeField32, TwoAdicField};
11use sp1_core_machine::riscv::RiscvAir;
12use sp1_primitives::{consts::WORD_SIZE, types::RecursionProgramType};
13use sp1_recursion_compiler::{
14    config::InnerConfig,
15    ir::{Array, Builder, Config, Felt, Var},
16    prelude::DslVariable,
17};
18use sp1_recursion_core::{
19    air::{RecursionPublicValues, RECURSIVE_PROOF_NUM_PV_ELTS},
20    runtime::{RecursionProgram, DIGEST_SIZE},
21};
22
23use sp1_recursion_compiler::prelude::*;
24use sp1_stark::{
25    air::{MachineAir, POSEIDON_NUM_WORDS, PV_DIGEST_NUM_WORDS},
26    baby_bear_poseidon2::BabyBearPoseidon2,
27    Com, ShardProof, StarkGenericConfig, StarkMachine, StarkVerifyingKey, Word,
28};
29
30use crate::{
31    challenger::{CanObserveVariable, DuplexChallengerVariable},
32    fri::TwoAdicFriPcsVariable,
33    hints::Hintable,
34    stark::{RecursiveVerifierConstraintFolder, StarkVerifier},
35    types::{ShardProofVariable, VerifyingKeyVariable},
36    utils::{const_fri_config, get_challenger_public_values, hash_vkey, var2felt},
37};
38
39use super::utils::{commit_public_values, verify_public_values_hash};
40
41#[derive(Debug, Clone, Copy)]
42pub struct SP1DeferredVerifier<C: Config, SC: StarkGenericConfig, A> {
43    _phantom: PhantomData<(C, SC, A)>,
44}
45
46/// Inputs that are hinted to the [SP1DeferredVerifier] program.
47pub struct SP1DeferredMemoryLayout<'a, SC: StarkGenericConfig, A: MachineAir<SC::Val>>
48where
49    SC::Val: PrimeField32,
50{
51    pub compress_vk: &'a StarkVerifyingKey<SC>,
52    pub machine: &'a StarkMachine<SC, A>,
53    pub proofs: Vec<ShardProof<SC>>,
54
55    pub start_reconstruct_deferred_digest: Vec<SC::Val>,
56
57    pub is_complete: bool,
58
59    pub sp1_vk: &'a StarkVerifyingKey<SC>,
60    pub sp1_machine: &'a StarkMachine<SC, RiscvAir<SC::Val>>,
61    pub committed_value_digest: Vec<Word<SC::Val>>,
62    pub deferred_proofs_digest: Vec<SC::Val>,
63    pub leaf_challenger: SC::Challenger,
64    pub end_pc: SC::Val,
65    pub end_shard: SC::Val,
66    pub end_execution_shard: SC::Val,
67    pub init_addr_bits: [SC::Val; 32],
68    pub finalize_addr_bits: [SC::Val; 32],
69}
70
71/// A variable version of the [SP1DeferredMemoryLayout] struct.
72#[derive(DslVariable, Clone)]
73pub struct SP1DeferredMemoryLayoutVariable<C: Config> {
74    pub compress_vk: VerifyingKeyVariable<C>,
75
76    pub proofs: Array<C, ShardProofVariable<C>>,
77
78    pub start_reconstruct_deferred_digest: Array<C, Felt<C::F>>,
79
80    pub is_complete: Var<C::N>,
81
82    pub sp1_vk: VerifyingKeyVariable<C>,
83    pub committed_value_digest: Array<C, Array<C, Felt<C::F>>>,
84    pub deferred_proofs_digest: Array<C, Felt<C::F>>,
85    pub leaf_challenger: DuplexChallengerVariable<C>,
86    pub end_pc: Felt<C::F>,
87    pub end_shard: Felt<C::F>,
88    pub end_execution_shard: Felt<C::F>,
89    pub init_addr_bits: Array<C, Felt<C::F>>,
90    pub finalize_addr_bits: Array<C, Felt<C::F>>,
91}
92
93impl<A> SP1DeferredVerifier<InnerConfig, BabyBearPoseidon2, A>
94where
95    A: MachineAir<BabyBear> + for<'a> Air<RecursiveVerifierConstraintFolder<'a, InnerConfig>>,
96{
97    /// Create a new instance of the program for the [BabyBearPoseidon2] config.
98    pub fn build(machine: &StarkMachine<BabyBearPoseidon2, A>) -> RecursionProgram<BabyBear> {
99        let mut builder = Builder::<InnerConfig>::new(RecursionProgramType::Deferred);
100        let input: SP1DeferredMemoryLayoutVariable<_> = builder.uninit();
101        SP1DeferredMemoryLayout::<BabyBearPoseidon2, A>::witness(&input, &mut builder);
102
103        let pcs = TwoAdicFriPcsVariable {
104            config: const_fri_config(&mut builder, machine.config().pcs().fri_config()),
105        };
106
107        SP1DeferredVerifier::verify(&mut builder, &pcs, machine, input);
108
109        builder.halt();
110
111        builder.compile_program()
112    }
113}
114
115impl<C: Config, SC, A> SP1DeferredVerifier<C, SC, A>
116where
117    C::F: PrimeField32 + TwoAdicField,
118    SC: StarkGenericConfig<
119        Val = C::F,
120        Challenge = C::EF,
121        Domain = TwoAdicMultiplicativeCoset<C::F>,
122    >,
123    A: MachineAir<C::F> + for<'a> Air<RecursiveVerifierConstraintFolder<'a, C>>,
124    Com<SC>: Into<[SC::Val; DIGEST_SIZE]>,
125{
126    /// Verify a batch of deferred proofs.
127    ///
128    /// Each deferred proof is a recursive proof representing some computation. Namely, every such
129    /// proof represents a recursively verified program.
130    /// verifier:
131    /// - Asserts that each of these proofs is valid as a `compress` proof.
132    /// - Asserts that each of these proofs is complete by checking the `is_complete` flag in the
133    ///  proof's public values.
134    /// - Aggregates the proof information into the accumulated deferred digest.
135    pub fn verify(
136        builder: &mut Builder<C>,
137        pcs: &TwoAdicFriPcsVariable<C>,
138        machine: &StarkMachine<SC, A>,
139        input: SP1DeferredMemoryLayoutVariable<C>,
140    ) {
141        // Read the inputs.
142        let SP1DeferredMemoryLayoutVariable {
143            compress_vk,
144            proofs,
145            start_reconstruct_deferred_digest,
146            is_complete,
147            sp1_vk,
148            committed_value_digest,
149            deferred_proofs_digest,
150            leaf_challenger,
151            end_pc,
152            end_shard,
153            end_execution_shard,
154            init_addr_bits,
155            finalize_addr_bits,
156        } = input;
157
158        // Initialize the values for the aggregated public output as all zeros.
159        let mut deferred_public_values_stream: Vec<Felt<_>> =
160            (0..RECURSIVE_PROOF_NUM_PV_ELTS).map(|_| builder.eval(C::F::zero())).collect();
161
162        let deferred_public_values: &mut RecursionPublicValues<_> =
163            deferred_public_values_stream.as_mut_slice().borrow_mut();
164
165        // Compute the digest of compress_vk and input the value to the public values.
166        let compress_vk_digest = hash_vkey(builder, &compress_vk);
167
168        deferred_public_values.compress_vk_digest =
169            array::from_fn(|i| builder.get(&compress_vk_digest, i));
170
171        // Initialize the start of deferred digests.
172        deferred_public_values.start_reconstruct_deferred_digest =
173            array::from_fn(|i| builder.get(&start_reconstruct_deferred_digest, i));
174
175        // Assert that there is at least one proof.
176        builder.assert_usize_ne(proofs.len(), 0);
177
178        // Initialize the consistency check variable.
179        let mut reconstruct_deferred_digest = builder.array(POSEIDON_NUM_WORDS);
180        for (i, first_digest) in
181            deferred_public_values.start_reconstruct_deferred_digest.iter().enumerate()
182        {
183            builder.set(&mut reconstruct_deferred_digest, i, *first_digest);
184        }
185
186        // Verify the proofs and connect the values.
187        builder.range(0, proofs.len()).for_each(|i, builder| {
188            // Load the proof.
189            let proof = builder.get(&proofs, i);
190
191            // Verify the shard proof.
192
193            // Prepare a challenger.
194            let mut challenger = DuplexChallengerVariable::new(builder);
195            // Observe the vk and start pc.
196            challenger.observe(builder, compress_vk.commitment.clone());
197            challenger.observe(builder, compress_vk.pc_start);
198            // Observe the main commitment and public values.
199            challenger.observe(builder, proof.commitment.main_commit.clone());
200            for j in 0..machine.num_pv_elts() {
201                let element = builder.get(&proof.public_values, j);
202                challenger.observe(builder, element);
203            }
204
205            // Verify the proof.
206            StarkVerifier::<C, SC>::verify_shard(
207                builder,
208                &compress_vk,
209                pcs,
210                machine,
211                &mut challenger,
212                &proof,
213                true,
214            );
215
216            // Load the public values from the proof.
217            let current_public_values_elements = (0..RECURSIVE_PROOF_NUM_PV_ELTS)
218                .map(|i| builder.get(&proof.public_values, i))
219                .collect::<Vec<Felt<_>>>();
220
221            let current_public_values: &RecursionPublicValues<Felt<C::F>> =
222                current_public_values_elements.as_slice().borrow();
223
224            // Check that the public values digest is correct.
225            verify_public_values_hash(builder, current_public_values);
226
227            // Assert that the proof is complete.
228            builder.assert_felt_eq(current_public_values.is_complete, C::F::one());
229
230            // Assert that the compress_vk digest is the same.
231            for (digest, current) in deferred_public_values
232                .compress_vk_digest
233                .iter()
234                .zip(current_public_values.compress_vk_digest.iter())
235            {
236                builder.assert_felt_eq(*digest, *current);
237            }
238
239            // Update deferred proof digest
240            // poseidon2( current_digest[..8] || pv.sp1_vk_digest[..8] ||
241            // pv.committed_value_digest[..32] )
242            let mut poseidon_inputs = builder.array(48);
243            for j in 0..DIGEST_SIZE {
244                let current_digest_element = builder.get(&reconstruct_deferred_digest, j);
245                builder.set(&mut poseidon_inputs, j, current_digest_element);
246            }
247
248            for j in 0..DIGEST_SIZE {
249                // let input_index: Var<_> = builder.constant(F::from_canonical_usize(j + 8));
250                builder.set(
251                    &mut poseidon_inputs,
252                    j + DIGEST_SIZE,
253                    current_public_values.sp1_vk_digest[j],
254                );
255            }
256            for j in 0..PV_DIGEST_NUM_WORDS {
257                for k in 0..WORD_SIZE {
258                    // let input_index: Var<_> =
259                    //     builder.eval(F::from_canonical_usize(j * WORD_SIZE + k + 16));
260                    let element = current_public_values.committed_value_digest[j][k];
261                    builder.set(&mut poseidon_inputs, j * WORD_SIZE + k + 16, element);
262                }
263            }
264            let new_digest = builder.poseidon2_hash(&poseidon_inputs);
265            for j in 0..DIGEST_SIZE {
266                let new_value = builder.get(&new_digest, j);
267                builder.set(&mut reconstruct_deferred_digest, j, new_value);
268            }
269        });
270
271        // Set the public values.
272
273        // Set initial_pc, end_pc, initial_shard, and end_shard to be the hitned values.
274        deferred_public_values.start_pc = end_pc;
275        deferred_public_values.next_pc = end_pc;
276        deferred_public_values.start_shard = end_shard;
277        deferred_public_values.next_shard = end_shard;
278        deferred_public_values.start_execution_shard = end_execution_shard;
279        deferred_public_values.next_execution_shard = end_execution_shard;
280        // Set the init and finalize address bits to be the hintred values.
281        let init_addr_bits = core::array::from_fn(|i| builder.get(&init_addr_bits, i));
282        deferred_public_values.previous_init_addr_bits = init_addr_bits;
283        deferred_public_values.last_init_addr_bits = init_addr_bits;
284        let finalize_addr_bits = core::array::from_fn(|i| builder.get(&finalize_addr_bits, i));
285        deferred_public_values.previous_finalize_addr_bits = finalize_addr_bits;
286        deferred_public_values.last_finalize_addr_bits = finalize_addr_bits;
287
288        // Set the sp1_vk_digest to be the hitned value.
289        let sp1_vk_digest = hash_vkey(builder, &sp1_vk);
290        deferred_public_values.sp1_vk_digest = array::from_fn(|i| builder.get(&sp1_vk_digest, i));
291
292        // Set the committed value digest to be the hitned value.
293        for (i, public_word) in deferred_public_values.committed_value_digest.iter_mut().enumerate()
294        {
295            let hinted_word = builder.get(&committed_value_digest, i);
296            public_word.0 = array::from_fn(|j| builder.get(&hinted_word, j));
297        }
298
299        // Set the deferred proof digest to be the hitned value.
300        deferred_public_values.deferred_proofs_digest =
301            core::array::from_fn(|i| builder.get(&deferred_proofs_digest, i));
302
303        // Set the initial, end, and leaf challenger to be the hitned values.
304        let values = get_challenger_public_values(builder, &leaf_challenger);
305        deferred_public_values.leaf_challenger = values;
306        deferred_public_values.start_reconstruct_challenger = values;
307        deferred_public_values.end_reconstruct_challenger = values;
308
309        // Assign the deffered proof digests.
310        deferred_public_values.end_reconstruct_deferred_digest =
311            array::from_fn(|i| builder.get(&reconstruct_deferred_digest, i));
312
313        // Set the is_complete flag.
314        deferred_public_values.is_complete = var2felt(builder, is_complete);
315
316        commit_public_values(builder, deferred_public_values);
317    }
318}
sp1_recursion_program/machine/deferred.rs

sp1_recursion_program/machine/
deferred.rs
