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.untrusted_config.enable_untrusted_programs);
152        #[cfg(feature = "mprotect")]
153        {
154            challenger.observe(builder, vk.untrusted_config.enable_trap_handler);
155            challenger.observe_slice(builder, vk.untrusted_config.trap_context);
156            challenger.observe_slice(builder, vk.untrusted_config.untrusted_memory);
157        }
158        // Observe the padding.
159        let zero: Felt<_> = builder.eval(SP1Field::zero());
160        for _ in 0..6 {
161            challenger.observe(builder, zero);
162        }
163
164        // Verify the shard proof.
165        tracing::debug_span!("verify shard")
166            .in_scope(|| machine.verify_shard(builder, &vk, shard_proof, &mut challenger));
167
168        // Assert that the `is_untrusted_programs_enabled` is equal to the vkey one.
169        builder.assert_felt_eq(
170            public_values.is_untrusted_programs_enabled,
171            vk.untrusted_config.enable_untrusted_programs,
172        );
173
174        #[cfg(feature = "mprotect")]
175        {
176            // Assert that the `trap_context` is equal to the vkey one.
177            for (pv_addr, vk_addr) in
178                (public_values.trap_context.iter()).zip_eq(vk.untrusted_config.trap_context.iter())
179            {
180                for idx in 0..3 {
181                    builder.assert_felt_eq(pv_addr[idx], vk_addr[idx]);
182                }
183            }
184
185            // Assert that the `untrusted_memory` is equal to the vkey one.
186            for (pv_addr, vk_addr) in (public_values.untrusted_memory.iter())
187                .zip_eq(vk.untrusted_config.untrusted_memory.iter())
188            {
189                for idx in 0..3 {
190                    builder.assert_felt_eq(pv_addr[idx], vk_addr[idx]);
191                }
192            }
193
194            // Assert that the `enable_trap_handler` is equal to the vkey one.
195            builder.assert_felt_eq(
196                public_values.enable_trap_handler,
197                vk.untrusted_config.enable_trap_handler,
198            );
199        }
200
201        // We add the global cumulative sum of the shard.
202        global_cumulative_sums.push(public_values.global_cumulative_sum);
203
204        // We sum the digests in `global_cumulative_sums` to get the overall global cumulative sum.
205        let global_cumulative_sum = builder.sum_digest_v2(global_cumulative_sums);
206
207        // Write all values to the public values struct and commit to them.
208        {
209            // Compute the vk digest.
210            let vk_digest = vk.hash(builder);
211
212            // Initialize the public values we will commit to.
213            let zero: Felt<_> = builder.eval(SP1Field::zero());
214            let mut recursion_public_values_stream = [zero; RECURSIVE_PROOF_NUM_PV_ELTS];
215            let recursion_public_values: &mut RecursionPublicValues<_> =
216                recursion_public_values_stream.as_mut_slice().borrow_mut();
217            recursion_public_values.prev_committed_value_digest =
218                public_values.prev_committed_value_digest;
219            recursion_public_values.committed_value_digest = public_values.committed_value_digest;
220            recursion_public_values.prev_deferred_proofs_digest =
221                public_values.prev_deferred_proofs_digest;
222            recursion_public_values.deferred_proofs_digest = public_values.deferred_proofs_digest;
223            recursion_public_values.prev_deferred_proof = num_deferred_proofs;
224            recursion_public_values.deferred_proof = num_deferred_proofs;
225            recursion_public_values.pc_start = public_values.pc_start;
226            recursion_public_values.next_pc = public_values.next_pc;
227            recursion_public_values.initial_timestamp = public_values.initial_timestamp;
228            recursion_public_values.last_timestamp = public_values.last_timestamp;
229            recursion_public_values.previous_init_addr = public_values.previous_init_addr;
230            recursion_public_values.last_init_addr = public_values.last_init_addr;
231            recursion_public_values.previous_finalize_addr = public_values.previous_finalize_addr;
232            recursion_public_values.last_finalize_addr = public_values.last_finalize_addr;
233            recursion_public_values.previous_init_page_idx = public_values.previous_init_page_idx;
234            recursion_public_values.last_init_page_idx = public_values.last_init_page_idx;
235            recursion_public_values.previous_finalize_page_idx =
236                public_values.previous_finalize_page_idx;
237            recursion_public_values.last_finalize_page_idx = public_values.last_finalize_page_idx;
238            recursion_public_values.start_reconstruct_deferred_digest = reconstruct_deferred_digest;
239            recursion_public_values.end_reconstruct_deferred_digest = reconstruct_deferred_digest;
240            recursion_public_values.sp1_vk_digest = vk_digest;
241            recursion_public_values.vk_root = vk_root;
242            recursion_public_values.global_cumulative_sum = global_cumulative_sum;
243            recursion_public_values.contains_first_shard = public_values.is_first_execution_shard;
244            recursion_public_values.num_included_shard = builder.eval(SP1Field::one());
245            recursion_public_values.is_complete = is_complete;
246            recursion_public_values.prev_exit_code = public_values.prev_exit_code;
247            recursion_public_values.exit_code = public_values.exit_code;
248            recursion_public_values.prev_commit_syscall = public_values.prev_commit_syscall;
249            recursion_public_values.commit_syscall = public_values.commit_syscall;
250            recursion_public_values.prev_commit_deferred_syscall =
251                public_values.prev_commit_deferred_syscall;
252            recursion_public_values.commit_deferred_syscall = public_values.commit_deferred_syscall;
253            recursion_public_values.proof_nonce = public_values.proof_nonce;
254
255            // Calculate the digest and set it in the public values.
256            recursion_public_values.digest = recursion_public_values_digest::<C, SP1GlobalContext>(
257                builder,
258                recursion_public_values,
259            );
260
261            assert_complete(builder, recursion_public_values, is_complete);
262
263            SP1GlobalContext::commit_recursion_public_values(builder, *recursion_public_values);
264        }
265    }
266}
sp1_recursion_circuit/machine/core.rs

sp1_recursion_circuit/machine/
core.rs
