Skip to main content

sp1_recursion_circuit/machine/
wrap.rs

1use std::marker::PhantomData;
2
3use super::SP1ShapedWitnessVariable;
4use crate::{
5    challenger::CanObserveVariable,
6    machine::{assert_complete, assert_root_public_values_valid, RootPublicValues},
7    shard::RecursiveShardVerifier,
8    zerocheck::RecursiveVerifierConstraintFolder,
9    CircuitConfig, SP1FieldConfigVariable,
10};
11use slop_air::Air;
12use slop_algebra::AbstractField;
13use slop_challenger::IopCtx;
14use sp1_hypercube::air::MachineAir;
15use sp1_primitives::{SP1ExtensionField, SP1Field};
16use sp1_recursion_compiler::ir::{Builder, Felt};
17use std::borrow::Borrow;
18
19/// A program to verify a single recursive proof representing a complete proof of program execution.
20///
21/// The root verifier is simply a `SP1CompressVerifier` with an assertion that the `is_complete`
22/// flag is set to true.
23#[derive(Debug, Clone, Copy)]
24pub struct SP1WrapVerifier<GC, C, A> {
25    _phantom: PhantomData<(GC, C, A)>,
26}
27
28impl<GC, C, A> SP1WrapVerifier<GC, C, A>
29where
30    GC: IopCtx<F = SP1Field, EF = SP1ExtensionField>
31        + Send
32        + Sync
33        + SP1FieldConfigVariable<C>
34        + Send
35        + Sync,
36    C: CircuitConfig,
37    A: MachineAir<SP1Field> + for<'a> Air<RecursiveVerifierConstraintFolder<'a>>,
38{
39    pub fn verify(
40        builder: &mut Builder<C>,
41        machine: &RecursiveShardVerifier<GC, A, C>,
42        input: SP1ShapedWitnessVariable<C, GC>,
43    ) {
44        // Assert the the proof is not malformed.
45        assert!(input.vks_and_proofs.len() == 1);
46        // Take the proof from the input.
47        let (vk, proof) = &input.vks_and_proofs[0];
48
49        // Assert that the program is complete.
50        builder.assert_felt_eq(input.is_complete, SP1Field::one());
51        let public_values: &RootPublicValues<Felt<SP1Field>> =
52            proof.public_values.as_slice().borrow();
53        assert_root_public_values_valid::<C, GC>(builder, public_values);
54
55        let mut challenger = <GC as SP1FieldConfigVariable<C>>::challenger_variable(builder);
56        challenger.observe(builder, vk.preprocessed_commit);
57        challenger.observe_slice(builder, vk.pc_start);
58        challenger.observe_slice(builder, vk.initial_global_cumulative_sum.0.x.0);
59        challenger.observe_slice(builder, vk.initial_global_cumulative_sum.0.y.0);
60        challenger.observe(builder, vk.enable_untrusted_programs);
61
62        // Observe the padding.
63        let zero: Felt<_> = builder.eval(SP1Field::zero());
64        for _ in 0..6 {
65            challenger.observe(builder, zero);
66        }
67        machine.verify_shard(builder, vk, proof, &mut challenger);
68
69        assert_complete(builder, &public_values.inner, input.is_complete);
70
71        GC::commit_recursion_public_values(builder, public_values.inner);
72    }
73}