Skip to main content

sp1_recursion_circuit/machine/
deferred.rs

1use std::{
2    array,
3    borrow::{Borrow, BorrowMut},
4};
5
6use serde::{Deserialize, Serialize};
7use slop_challenger::IopCtx;
8
9use crate::machine::{
10    assert_recursion_public_values_valid, SP1MerkleProofVerifier, SP1MerkleProofWitnessValues,
11    SP1MerkleProofWitnessVariable, VkAndProof,
12};
13use slop_air::Air;
14use slop_algebra::{AbstractField, PrimeField32};
15use sp1_hypercube::{
16    air::{MachineAir, ShardRange, POSEIDON_NUM_WORDS, PROOF_NONCE_NUM_WORDS},
17    septic_curve::SepticCurve,
18    septic_digest::SepticDigest,
19    ShardProof,
20};
21use sp1_primitives::{SP1ExtensionField, SP1Field};
22use sp1_recursion_compiler::ir::{Builder, Felt};
23
24use sp1_recursion_executor::{
25    RecursionPublicValues, DIGEST_SIZE, PV_DIGEST_NUM_WORDS, RECURSIVE_PROOF_NUM_PV_ELTS,
26};
27
28use crate::{
29    challenger::{CanObserveVariable, DuplexChallengerVariable},
30    hash::{FieldHasher, FieldHasherVariable},
31    shard::{MachineVerifyingKeyVariable, RecursiveShardVerifier, ShardProofVariable},
32    zerocheck::RecursiveVerifierConstraintFolder,
33    CircuitConfig, SP1FieldConfigVariable,
34};
35
36use super::{assert_complete, recursion_public_values_digest};
37
38pub struct SP1DeferredVerifier<GC, C, A> {
39    _phantom: std::marker::PhantomData<(GC, C, A)>,
40}
41
42#[derive(Clone, Serialize, Deserialize)]
43#[serde(bound(
44    serialize = "GC::Challenger: Serialize, ShardProof<GC, Proof>: Serialize, [GC::F; DIGEST_SIZE]: Serialize"
45))]
46#[serde(bound(
47    deserialize = "GC::Challenger: Deserialize<'de>, ShardProof<GC, Proof>: Deserialize<'de>,  [GC::F; DIGEST_SIZE]: Deserialize<'de>"
48))]
49pub struct SP1DeferredWitnessValues<
50    GC: IopCtx<F = SP1Field, EF = SP1ExtensionField> + FieldHasher,
51    Proof,
52> {
53    pub vks_and_proofs: Vec<VkAndProof<GC, Proof>>,
54    pub vk_merkle_data: SP1MerkleProofWitnessValues<GC>,
55    pub start_reconstruct_deferred_digest: [GC::F; POSEIDON_NUM_WORDS],
56    pub sp1_vk_digest: [GC::F; DIGEST_SIZE],
57    pub end_pc: [GC::F; 3],
58    pub proof_nonce: [GC::F; PROOF_NONCE_NUM_WORDS],
59    pub deferred_proof_index: GC::F,
60}
61
62impl<GC: IopCtx<F = SP1Field, EF = SP1ExtensionField> + FieldHasher, Proof>
63    SP1DeferredWitnessValues<GC, Proof>
64{
65    /// The deferred proof range.
66    ///
67    /// The deferred proofs are put at the "start" and assigned initial and final timestamp equal to
68    /// `1`. The rest of the range values are set to zero.
69    pub fn range(&self) -> ShardRange {
70        let prev_deferred_proof = self.deferred_proof_index.as_canonical_u32() as u64;
71        let deferred_proof = prev_deferred_proof + self.vks_and_proofs.len() as u64;
72        ShardRange {
73            timestamp_range: (1, 1),
74            initialized_address_range: (0, 0),
75            finalized_address_range: (0, 0),
76            initialized_page_index_range: (0, 0),
77            finalized_page_index_range: (0, 0),
78            deferred_proof_range: (prev_deferred_proof, deferred_proof),
79        }
80    }
81}
82
83#[allow(clippy::type_complexity)]
84pub struct SP1DeferredWitnessVariable<
85    C: CircuitConfig,
86    SC: FieldHasherVariable<C> + SP1FieldConfigVariable<C>,
87> {
88    pub vks_and_proofs: Vec<(MachineVerifyingKeyVariable<C, SC>, ShardProofVariable<C, SC>)>,
89    pub vk_merkle_data: SP1MerkleProofWitnessVariable<C, SC>,
90    pub start_reconstruct_deferred_digest: [Felt<SP1Field>; POSEIDON_NUM_WORDS],
91    pub sp1_vk_digest: [Felt<SP1Field>; DIGEST_SIZE],
92    pub end_pc: [Felt<SP1Field>; 3],
93    pub proof_nonce: [Felt<SP1Field>; PROOF_NONCE_NUM_WORDS],
94    pub deferred_proof_index: Felt<SP1Field>,
95}
96
97impl<GC, C, A> SP1DeferredVerifier<GC, C, A>
98where
99    GC: IopCtx<F = SP1Field, EF = SP1ExtensionField>
100        + SP1FieldConfigVariable<
101            C,
102            FriChallengerVariable = DuplexChallengerVariable<C>,
103            DigestVariable = [Felt<SP1Field>; DIGEST_SIZE],
104        > + Send
105        + Sync,
106    C: CircuitConfig,
107    A: MachineAir<SP1Field> + for<'a> Air<RecursiveVerifierConstraintFolder<'a>>,
108{
109    /// Verify a batch of deferred proofs.
110    ///
111    /// Each deferred proof is a recursive proof representing some computation. Namely, every such
112    /// proof represents a recursively verified program.
113    /// verifier:
114    /// - Asserts that each of these proofs is valid as a `compress` proof.
115    /// - Asserts that each of these proofs is complete by checking the `is_complete` flag in the
116    ///   proof's public values.
117    /// - Aggregates the proof information into the accumulated deferred digest.
118    pub fn verify(
119        builder: &mut Builder<C>,
120        machine: &RecursiveShardVerifier<GC, A, C>,
121        input: SP1DeferredWitnessVariable<C, GC>,
122        value_assertions: bool,
123    ) {
124        let SP1DeferredWitnessVariable {
125            vks_and_proofs,
126            vk_merkle_data,
127            start_reconstruct_deferred_digest,
128            sp1_vk_digest,
129            end_pc,
130            proof_nonce,
131            deferred_proof_index,
132        } = input;
133
134        // First, verify the merkle tree proofs.
135        let vk_root = vk_merkle_data.root;
136        let values = vks_and_proofs.iter().map(|(vk, _)| vk.hash(builder)).collect::<Vec<_>>();
137        SP1MerkleProofVerifier::verify(builder, values, vk_merkle_data, value_assertions);
138
139        let mut deferred_public_values_stream: Vec<Felt<SP1Field>> =
140            (0..RECURSIVE_PROOF_NUM_PV_ELTS).map(|_| builder.uninit()).collect();
141        let deferred_public_values: &mut RecursionPublicValues<_> =
142            deferred_public_values_stream.as_mut_slice().borrow_mut();
143
144        // Initialize the start of deferred digests.
145        deferred_public_values.start_reconstruct_deferred_digest =
146            start_reconstruct_deferred_digest;
147
148        // Initialize the consistency check variable.
149        let mut reconstruct_deferred_digest: [Felt<SP1Field>; POSEIDON_NUM_WORDS] =
150            start_reconstruct_deferred_digest;
151
152        // Save the number of deferred proofs before consuming the vector.
153        let num_deferred_proofs = SP1Field::from_canonical_usize(vks_and_proofs.len());
154
155        for (vk, shard_proof) in vks_and_proofs {
156            // Prepare a challenger.
157            let mut challenger = GC::challenger_variable(builder);
158            // Observe the vk and start pc.
159            challenger.observe(builder, vk.preprocessed_commit);
160            challenger.observe_slice(builder, vk.pc_start);
161            challenger.observe_slice(builder, vk.initial_global_cumulative_sum.0.x.0);
162            challenger.observe_slice(builder, vk.initial_global_cumulative_sum.0.y.0);
163            challenger.observe(builder, vk.enable_untrusted_programs);
164            // Observe the padding.
165            let zero: Felt<_> = builder.eval(SP1Field::zero());
166            for _ in 0..6 {
167                challenger.observe(builder, zero);
168            }
169
170            machine.verify_shard(builder, &vk, &shard_proof, &mut challenger);
171
172            // Get the current public values.
173            let current_public_values: &RecursionPublicValues<Felt<SP1Field>> =
174                shard_proof.public_values.as_slice().borrow();
175            // Assert that the `vk_root` is the same as the witnessed one.
176            for (elem, expected) in current_public_values.vk_root.iter().zip(vk_root.iter()) {
177                builder.assert_felt_eq(*elem, *expected);
178            }
179            // Assert that the public values are valid.
180            assert_recursion_public_values_valid::<C, GC>(builder, current_public_values);
181
182            // Assert that the proof is complete.
183            builder.assert_felt_eq(current_public_values.is_complete, SP1Field::one());
184
185            // Update deferred proof digest
186            // poseidon2( current_digest[..8] || pv.sp1_vk_digest[..8] ||
187            // pv.committed_value_digest[..16] )
188            let mut inputs: [Felt<SP1Field>; 48] = array::from_fn(|_| builder.uninit());
189            inputs[0..DIGEST_SIZE].copy_from_slice(&reconstruct_deferred_digest);
190
191            inputs[DIGEST_SIZE..DIGEST_SIZE + DIGEST_SIZE]
192                .copy_from_slice(&current_public_values.sp1_vk_digest);
193
194            for j in 0..PV_DIGEST_NUM_WORDS {
195                for k in 0..4 {
196                    let element = current_public_values.committed_value_digest[j][k];
197                    inputs[j * 4 + k + 16] = element;
198                }
199            }
200            reconstruct_deferred_digest = GC::hash(builder, &inputs);
201        }
202
203        // Set the public values.
204
205        let zero = builder.eval(SP1Field::zero());
206        let one = builder.eval(SP1Field::one());
207
208        // Set initial_pc, end_pc, initial_shard, and end_shard to be the hinted values.
209        deferred_public_values.pc_start = end_pc;
210        deferred_public_values.next_pc = end_pc;
211        // Set the init and finalize addresss to be the hinted values.
212        deferred_public_values.previous_init_addr = core::array::from_fn(|_| zero);
213        deferred_public_values.last_init_addr = core::array::from_fn(|_| zero);
214        deferred_public_values.previous_finalize_addr = core::array::from_fn(|_| zero);
215        deferred_public_values.last_finalize_addr = core::array::from_fn(|_| zero);
216        // Set the init and finalize page index to be the hinted values.
217        deferred_public_values.previous_init_page_idx = core::array::from_fn(|_| zero);
218        deferred_public_values.last_init_page_idx = core::array::from_fn(|_| zero);
219        deferred_public_values.previous_finalize_page_idx = core::array::from_fn(|_| zero);
220        deferred_public_values.last_finalize_page_idx = core::array::from_fn(|_| zero);
221        deferred_public_values.initial_timestamp = [zero, zero, zero, one];
222        deferred_public_values.last_timestamp = [zero, zero, zero, one];
223
224        // Set the sp1_vk_digest to be the hitned value.
225        deferred_public_values.sp1_vk_digest = sp1_vk_digest;
226
227        // Set the committed value digest to be the hitned value.
228        deferred_public_values.prev_committed_value_digest =
229            core::array::from_fn(|_| [zero, zero, zero, zero]);
230        deferred_public_values.committed_value_digest =
231            core::array::from_fn(|_| [zero, zero, zero, zero]);
232        // Set the deferred proof digest to all zeroes.
233        deferred_public_values.prev_deferred_proofs_digest = core::array::from_fn(|_| zero);
234        deferred_public_values.deferred_proofs_digest = core::array::from_fn(|_| zero);
235
236        // Set the exit code to be zero for now.
237        deferred_public_values.prev_exit_code = zero;
238        deferred_public_values.exit_code = zero;
239        // Set the `commit_syscall` and `commit_deferred_syscall` flags to zero.
240        deferred_public_values.prev_commit_syscall = zero;
241        deferred_public_values.commit_syscall = zero;
242        deferred_public_values.prev_commit_deferred_syscall = zero;
243        deferred_public_values.commit_deferred_syscall = zero;
244        // Assign the deferred proof digests.
245        deferred_public_values.end_reconstruct_deferred_digest = reconstruct_deferred_digest;
246        // Set the deferred proof index.
247        deferred_public_values.prev_deferred_proof = deferred_proof_index;
248        deferred_public_values.deferred_proof =
249            builder.eval(deferred_proof_index + num_deferred_proofs);
250        // Set the is_complete flag.
251        deferred_public_values.is_complete = zero;
252        deferred_public_values.proof_nonce = proof_nonce;
253        // Set the cumulative sum to zero.
254        deferred_public_values.global_cumulative_sum =
255            SepticDigest(SepticCurve::convert(SepticDigest::<SP1Field>::zero().0, |value| {
256                builder.eval(value)
257            }));
258        // Set the first shard flag to zero.
259        deferred_public_values.contains_first_shard = zero;
260        // Set the number of included shards to zero.
261        deferred_public_values.num_included_shard = zero;
262        // Set the vk root from the witness.
263        deferred_public_values.vk_root = vk_root;
264        // Set the digest according to the previous values.
265        deferred_public_values.digest =
266            recursion_public_values_digest::<C, GC>(builder, deferred_public_values);
267
268        assert_complete(builder, deferred_public_values, deferred_public_values.is_complete);
269
270        GC::commit_recursion_public_values(builder, *deferred_public_values);
271    }
272}