sp1_recursion_circuit/machine/
core.rs

1use std::{
2    borrow::{Borrow, BorrowMut},
3    marker::PhantomData,
4};
5
6use itertools::Itertools;
7use slop_air::Air;
8use slop_algebra::{AbstractField, PrimeField32};
9use slop_challenger::IopCtx;
10use sp1_primitives::{SP1Field, SP1GlobalContext};
11
12use serde::{Deserialize, Serialize};
13use sp1_core_machine::riscv::RiscvAir;
14
15use sp1_hypercube::air::{PublicValues, SP1CorePublicValues};
16
17use sp1_hypercube::{air::ShardRange, MachineVerifyingKey, ShardProof};
18
19use sp1_recursion_compiler::{
20    circuit::CircuitV2Builder,
21    ir::{Builder, Config, Felt},
22};
23
24use sp1_recursion_executor::{RecursionPublicValues, DIGEST_SIZE, RECURSIVE_PROOF_NUM_PV_ELTS};
25
26use crate::{
27    challenger::CanObserveVariable,
28    machine::{assert_complete, recursion_public_values_digest},
29    shard::{MachineVerifyingKeyVariable, RecursiveShardVerifier, ShardProofVariable},
30    zerocheck::RecursiveVerifierConstraintFolder,
31    CircuitConfig, SP1FieldConfigVariable,
32};
33
34pub struct SP1RecursionWitnessVariable<C: CircuitConfig, SC: SP1FieldConfigVariable<C>> {
35    pub vk: MachineVerifyingKeyVariable<C, SC>,
36    pub shard_proofs: Vec<ShardProofVariable<C, SC>>,
37    pub reconstruct_deferred_digest: [Felt<SP1Field>; DIGEST_SIZE],
38    pub num_deferred_proofs: Felt<SP1Field>,
39    pub is_complete: Felt<SP1Field>,
40    pub vk_root: [Felt<SP1Field>; DIGEST_SIZE],
41}
42
43#[derive(Clone, Serialize, Deserialize)]
44#[serde(bound(serialize = "ShardProof<GC,Proof>: Serialize"))]
45#[serde(bound(deserialize = "ShardProof<GC,Proof>: Deserialize<'de>"))]
46/// A struct to contain the inputs to the `normalize` program.
47pub struct SP1NormalizeWitnessValues<GC: IopCtx, Proof> {
48    pub vk: MachineVerifyingKey<GC>,
49    pub shard_proofs: Vec<ShardProof<GC, Proof>>,
50    pub is_complete: bool,
51    pub vk_root: [GC::F; DIGEST_SIZE],
52    pub reconstruct_deferred_digest: [GC::F; 8],
53    pub num_deferred_proofs: GC::F,
54}
55
56impl<GC: IopCtx, Proof> SP1NormalizeWitnessValues<GC, Proof> {
57    pub fn range(&self) -> ShardRange
58    where
59        GC::F: PrimeField32,
60    {
61        let start_pv: &SP1CorePublicValues<GC::F> =
62            self.shard_proofs[0].public_values.as_slice().borrow();
63        let end_pv: &SP1CorePublicValues<GC::F> =
64            self.shard_proofs[self.shard_proofs.len() - 1].public_values.as_slice().borrow();
65
66        let start = start_pv.range().start();
67        let end = end_pv.range().end();
68
69        let mut range: ShardRange = (start..end).into();
70        let num_deferred_proofs = self.num_deferred_proofs.as_canonical_u32() as u64;
71        range.deferred_proof_range = (num_deferred_proofs, num_deferred_proofs);
72        range
73    }
74}
75
76/// A program for recursively verifying a batch of SP1 proofs.
77#[derive(Debug, Clone, Copy)]
78pub struct SP1RecursiveVerifier<C: Config> {
79    _phantom: PhantomData<C>,
80}
81
82impl<C> SP1RecursiveVerifier<C>
83where
84    C: CircuitConfig<Bit = Felt<SP1Field>>,
85{
86    /// Verify a batch of SP1 shard proofs and aggregate their public values.
87    ///
88    /// This program represents a first recursive step in the verification of an SP1 proof
89    /// consisting of one or more shards. Each shard proof is verified and its public values are
90    /// turned into the recursion public values, which will be aggregated in compress.
91    ///
92    /// # Constraints
93    ///
94    /// ## Verifying the core shard proofs.
95    /// For each shard, the verifier asserts the correctness of the shard proof which is composed
96    /// of verifying the polynomial commitment's proof for openings and verifying the constraints.
97    ///
98    /// ## Verifing the first shard constraints.
99    /// The first shard has some additional constraints for initialization.
100    pub fn verify(
101        builder: &mut Builder<C>,
102        machine: &RecursiveShardVerifier<SP1GlobalContext, RiscvAir<SP1Field>, C>,
103        input: SP1RecursionWitnessVariable<C, SP1GlobalContext>,
104    ) where
105        RiscvAir<SP1Field>: for<'b> Air<RecursiveVerifierConstraintFolder<'b>>,
106    {
107        // Read input.
108        let SP1RecursionWitnessVariable {
109            vk,
110            shard_proofs,
111            is_complete,
112            vk_root,
113            reconstruct_deferred_digest,
114            num_deferred_proofs,
115        } = input;
116
117        // Assert that the number of proofs is one.
118        assert!(shard_proofs.len() == 1);
119        let shard_proof = &shard_proofs[0];
120
121        // Initialize the cumulative sum.
122        let mut global_cumulative_sums = Vec::new();
123
124        // Get the public values.
125        let public_values: &PublicValues<[Felt<_>; 4], [Felt<_>; 3], [Felt<_>; 4], Felt<_>> =
126            shard_proof.public_values.as_slice().borrow();
127
128        // If it's the first shard, then the `pc_start` should be vk.pc_start.
129        for (pc, vk_pc) in public_values.pc_start.iter().zip_eq(vk.pc_start.iter()) {
130            builder.assert_felt_eq(
131                public_values.is_first_execution_shard * (*pc - *vk_pc),
132                SP1Field::zero(),
133            );
134        }
135
136        // If it's the first shard, we add the vk's `initial_global_cumulative_sum` to the
137        // digest. If it's not the first shard, we add the zero digest to the digest.
138        global_cumulative_sums.push(builder.select_global_cumulative_sum(
139            public_values.is_first_execution_shard,
140            vk.initial_global_cumulative_sum,
141        ));
142
143        // Prepare a challenger.
144        let mut challenger = SP1GlobalContext::challenger_variable(builder);
145
146        // Observe the vk and start pc.
147        challenger.observe(builder, vk.preprocessed_commit);
148        challenger.observe_slice(builder, vk.pc_start);
149        challenger.observe_slice(builder, vk.initial_global_cumulative_sum.0.x.0);
150        challenger.observe_slice(builder, vk.initial_global_cumulative_sum.0.y.0);
151        challenger.observe(builder, vk.enable_untrusted_programs);
152        // Observe the padding.
153        let zero: Felt<_> = builder.eval(SP1Field::zero());
154        for _ in 0..6 {
155            challenger.observe(builder, zero);
156        }
157
158        // Verify the shard proof.
159        tracing::debug_span!("verify shard")
160            .in_scope(|| machine.verify_shard(builder, &vk, shard_proof, &mut challenger));
161
162        // Assert that the `is_untrusted_programs_enabled` is equal to the vkey one.
163        builder.assert_felt_eq(
164            public_values.is_untrusted_programs_enabled,
165            vk.enable_untrusted_programs,
166        );
167
168        // We add the global cumulative sum of the shard.
169        global_cumulative_sums.push(public_values.global_cumulative_sum);
170
171        // We sum the digests in `global_cumulative_sums` to get the overall global cumulative sum.
172        let global_cumulative_sum = builder.sum_digest_v2(global_cumulative_sums);
173
174        // Write all values to the public values struct and commit to them.
175        {
176            // Compute the vk digest.
177            let vk_digest = vk.hash(builder);
178
179            // Initialize the public values we will commit to.
180            let zero: Felt<_> = builder.eval(SP1Field::zero());
181            let mut recursion_public_values_stream = [zero; RECURSIVE_PROOF_NUM_PV_ELTS];
182            let recursion_public_values: &mut RecursionPublicValues<_> =
183                recursion_public_values_stream.as_mut_slice().borrow_mut();
184            recursion_public_values.prev_committed_value_digest =
185                public_values.prev_committed_value_digest;
186            recursion_public_values.committed_value_digest = public_values.committed_value_digest;
187            recursion_public_values.prev_deferred_proofs_digest =
188                public_values.prev_deferred_proofs_digest;
189            recursion_public_values.deferred_proofs_digest = public_values.deferred_proofs_digest;
190            recursion_public_values.prev_deferred_proof = num_deferred_proofs;
191            recursion_public_values.deferred_proof = num_deferred_proofs;
192            recursion_public_values.pc_start = public_values.pc_start;
193            recursion_public_values.next_pc = public_values.next_pc;
194            recursion_public_values.initial_timestamp = public_values.initial_timestamp;
195            recursion_public_values.last_timestamp = public_values.last_timestamp;
196            recursion_public_values.previous_init_addr = public_values.previous_init_addr;
197            recursion_public_values.last_init_addr = public_values.last_init_addr;
198            recursion_public_values.previous_finalize_addr = public_values.previous_finalize_addr;
199            recursion_public_values.last_finalize_addr = public_values.last_finalize_addr;
200            recursion_public_values.previous_init_page_idx = public_values.previous_init_page_idx;
201            recursion_public_values.last_init_page_idx = public_values.last_init_page_idx;
202            recursion_public_values.previous_finalize_page_idx =
203                public_values.previous_finalize_page_idx;
204            recursion_public_values.last_finalize_page_idx = public_values.last_finalize_page_idx;
205            recursion_public_values.start_reconstruct_deferred_digest = reconstruct_deferred_digest;
206            recursion_public_values.end_reconstruct_deferred_digest = reconstruct_deferred_digest;
207            recursion_public_values.sp1_vk_digest = vk_digest;
208            recursion_public_values.vk_root = vk_root;
209            recursion_public_values.global_cumulative_sum = global_cumulative_sum;
210            recursion_public_values.contains_first_shard = public_values.is_first_execution_shard;
211            recursion_public_values.num_included_shard = builder.eval(SP1Field::one());
212            recursion_public_values.is_complete = is_complete;
213            recursion_public_values.prev_exit_code = public_values.prev_exit_code;
214            recursion_public_values.exit_code = public_values.exit_code;
215            recursion_public_values.prev_commit_syscall = public_values.prev_commit_syscall;
216            recursion_public_values.commit_syscall = public_values.commit_syscall;
217            recursion_public_values.prev_commit_deferred_syscall =
218                public_values.prev_commit_deferred_syscall;
219            recursion_public_values.commit_deferred_syscall = public_values.commit_deferred_syscall;
220            recursion_public_values.proof_nonce = public_values.proof_nonce;
221
222            // Calculate the digest and set it in the public values.
223            recursion_public_values.digest = recursion_public_values_digest::<C, SP1GlobalContext>(
224                builder,
225                recursion_public_values,
226            );
227
228            assert_complete(builder, recursion_public_values, is_complete);
229
230            SP1GlobalContext::commit_recursion_public_values(builder, *recursion_public_values);
231        }
232    }
233}
sp1_recursion_circuit/machine/core.rs

sp1_recursion_circuit/machine/
core.rs
