sp1_recursion_program/machine/
utils.rs

1use std::mem::transmute;
2
3use itertools::Itertools;
4use p3_commit::TwoAdicMultiplicativeCoset;
5use p3_field::AbstractField;
6
7use sp1_recursion_compiler::ir::{Array, Builder, Config, Felt, Var};
8use sp1_recursion_core::{
9    air::{RecursionPublicValues, NUM_PV_ELMS_TO_HASH, RECURSIVE_PROOF_NUM_PV_ELTS},
10    runtime::DIGEST_SIZE,
11};
12use sp1_stark::{air::MachineAir, Com, StarkGenericConfig, StarkMachine, StarkVerifyingKey};
13
14use crate::{
15    challenger::DuplexChallengerVariable,
16    fri::TwoAdicMultiplicativeCosetVariable,
17    types::VerifyingKeyVariable,
18    utils::{assert_challenger_eq_pv, felt2var, get_preprocessed_data},
19};
20
21/// Assertions on the public values describing a complete recursive proof state.
22///
23/// See [SP1Prover::verify] for the verification algorithm of a complete SP1 proof.
24pub(crate) fn assert_complete<C: Config>(
25    builder: &mut Builder<C>,
26    public_values: &RecursionPublicValues<Felt<C::F>>,
27    end_reconstruct_challenger: &DuplexChallengerVariable<C>,
28) {
29    let RecursionPublicValues {
30        deferred_proofs_digest,
31        next_pc,
32        start_shard,
33        next_shard,
34        start_execution_shard,
35        next_execution_shard,
36        cumulative_sum,
37        start_reconstruct_deferred_digest,
38        end_reconstruct_deferred_digest,
39        leaf_challenger,
40        ..
41    } = public_values;
42
43    // Assert that `next_pc` is equal to zero (so program execution has completed)
44    builder.assert_felt_eq(*next_pc, C::F::zero());
45
46    // Assert that start shard is equal to 1.
47    builder.assert_felt_eq(*start_shard, C::F::one());
48
49    // Assert that the next shard is not equal to one. This guarantees that there is at least one
50    // shard.
51    builder.assert_felt_ne(*next_shard, C::F::one());
52
53    // Assert that the start execution shard is equal to 1.
54    builder.assert_felt_eq(*start_execution_shard, C::F::one());
55
56    // Assert that next shard is not equal to one. This guarantees that there is at least one shard
57    // with CPU.
58    builder.assert_felt_ne(*next_execution_shard, C::F::one());
59
60    // Assert that the end reconstruct challenger is equal to the leaf challenger.
61    assert_challenger_eq_pv(builder, end_reconstruct_challenger, *leaf_challenger);
62
63    // The start reconstruct deffered digest should be zero.
64    for start_digest_word in start_reconstruct_deferred_digest {
65        builder.assert_felt_eq(*start_digest_word, C::F::zero());
66    }
67
68    // The end reconstruct deffered digest should be equal to the deferred proofs digest.
69    for (end_digest_word, deferred_digest_word) in
70        end_reconstruct_deferred_digest.iter().zip_eq(deferred_proofs_digest.iter())
71    {
72        builder.assert_felt_eq(*end_digest_word, *deferred_digest_word);
73    }
74
75    // Assert that the cumulative sum is zero.
76    for b in cumulative_sum.iter() {
77        builder.assert_felt_eq(*b, C::F::zero());
78    }
79}
80
81pub(crate) fn proof_data_from_vk<C: Config, SC, A>(
82    builder: &mut Builder<C>,
83    vk: &StarkVerifyingKey<SC>,
84    machine: &StarkMachine<SC, A>,
85) -> VerifyingKeyVariable<C>
86where
87    SC: StarkGenericConfig<
88        Val = C::F,
89        Challenge = C::EF,
90        Domain = TwoAdicMultiplicativeCoset<C::F>,
91    >,
92    A: MachineAir<SC::Val>,
93    Com<SC>: Into<[SC::Val; DIGEST_SIZE]>,
94{
95    let mut commitment = builder.dyn_array(DIGEST_SIZE);
96    for (i, value) in vk.commit.clone().into().iter().enumerate() {
97        builder.set(&mut commitment, i, *value);
98    }
99    let pc_start: Felt<_> = builder.eval(vk.pc_start);
100
101    let (prep_sorted_indices_val, prep_domains_val) = get_preprocessed_data(machine, vk);
102
103    let mut prep_sorted_indices = builder.dyn_array::<Var<_>>(prep_sorted_indices_val.len());
104    let mut prep_domains =
105        builder.dyn_array::<TwoAdicMultiplicativeCosetVariable<_>>(prep_domains_val.len());
106
107    for (i, value) in prep_sorted_indices_val.iter().enumerate() {
108        builder.set(&mut prep_sorted_indices, i, C::N::from_canonical_usize(*value));
109    }
110
111    for (i, value) in prep_domains_val.iter().enumerate() {
112        let domain: TwoAdicMultiplicativeCosetVariable<_> = builder.constant(*value);
113        builder.set(&mut prep_domains, i, domain);
114    }
115
116    VerifyingKeyVariable {
117        commitment,
118        pc_start,
119        preprocessed_sorted_idxs: prep_sorted_indices,
120        prep_domains,
121    }
122}
123
124/// Calculates the digest of the recursion public values.
125fn calculate_public_values_digest<C: Config>(
126    builder: &mut Builder<C>,
127    public_values: &RecursionPublicValues<Felt<C::F>>,
128) -> Array<C, Felt<C::F>> {
129    let pv_elements: [Felt<_>; RECURSIVE_PROOF_NUM_PV_ELTS] = unsafe { transmute(*public_values) };
130    let mut poseidon_inputs = builder.array(NUM_PV_ELMS_TO_HASH);
131    for (i, elm) in pv_elements[0..NUM_PV_ELMS_TO_HASH].iter().enumerate() {
132        builder.set(&mut poseidon_inputs, i, *elm);
133    }
134    builder.poseidon2_hash(&poseidon_inputs)
135}
136
137/// Verifies the digest of a recursive public values struct.
138pub(crate) fn verify_public_values_hash<C: Config>(
139    builder: &mut Builder<C>,
140    public_values: &RecursionPublicValues<Felt<C::F>>,
141) {
142    let var_exit_code = felt2var(builder, public_values.exit_code);
143    // Check that the public values digest is correct if the exit_code is 0.
144    builder.if_eq(var_exit_code, C::N::zero()).then(|builder| {
145        let calculated_digest = calculate_public_values_digest(builder, public_values);
146
147        let expected_digest = public_values.digest;
148        for (i, expected_elm) in expected_digest.iter().enumerate() {
149            let calculated_elm = builder.get(&calculated_digest, i);
150            builder.assert_felt_eq(*expected_elm, calculated_elm);
151        }
152    });
153}
154
155/// Register and commits the recursion public values.
156pub fn commit_public_values<C: Config>(
157    builder: &mut Builder<C>,
158    public_values: &RecursionPublicValues<Felt<C::F>>,
159) {
160    let pv_elements: [Felt<_>; RECURSIVE_PROOF_NUM_PV_ELTS] = unsafe { transmute(*public_values) };
161    let pv_elms_no_digest = &pv_elements[0..NUM_PV_ELMS_TO_HASH];
162
163    for value in pv_elms_no_digest.iter() {
164        builder.register_public_value(*value);
165    }
166
167    // Hash the public values.
168    let pv_digest = calculate_public_values_digest(builder, public_values);
169    for i in 0..DIGEST_SIZE {
170        let digest_element = builder.get(&pv_digest, i);
171        builder.commit_public_value(digest_element);
172    }
173}