sp1_recursion_program/
types.rs

1use p3_air::BaseAir;
2use p3_field::{AbstractExtensionField, AbstractField};
3use sp1_primitives::consts::WORD_SIZE;
4use sp1_recursion_compiler::prelude::*;
5use sp1_stark::{
6    air::{MachineAir, PV_DIGEST_NUM_WORDS},
7    AirOpenedValues, Chip, ChipOpenedValues, Word,
8};
9
10use crate::fri::{
11    types::{DigestVariable, FriConfigVariable, TwoAdicPcsProofVariable},
12    TwoAdicMultiplicativeCosetVariable,
13};
14
15/// Reference: [sp1_core_machine::stark::ShardProof]
16#[derive(DslVariable, Clone)]
17pub struct ShardProofVariable<C: Config> {
18    pub commitment: ShardCommitmentVariable<C>,
19    pub opened_values: ShardOpenedValuesVariable<C>,
20    pub opening_proof: TwoAdicPcsProofVariable<C>,
21    pub public_values: Array<C, Felt<C::F>>,
22    pub quotient_data: Array<C, QuotientData<C>>,
23    pub sorted_idxs: Array<C, Var<C::N>>,
24}
25
26#[derive(DslVariable, Clone, Copy)]
27pub struct QuotientData<C: Config> {
28    pub log_quotient_degree: Var<C::N>,
29    pub quotient_size: Var<C::N>,
30}
31
32#[derive(Debug, Clone, Copy, PartialEq, Eq)]
33pub struct QuotientDataValues {
34    pub log_quotient_degree: usize,
35    pub quotient_size: usize,
36}
37
38/// Reference: [sp1_core_machine::stark::VerifyingKey]
39#[derive(DslVariable, Clone)]
40pub struct VerifyingKeyVariable<C: Config> {
41    pub commitment: DigestVariable<C>,
42    pub pc_start: Felt<C::F>,
43    pub preprocessed_sorted_idxs: Array<C, Var<C::N>>,
44    pub prep_domains: Array<C, TwoAdicMultiplicativeCosetVariable<C>>,
45}
46
47/// Reference: [sp1_core_machine::stark::ShardCommitment]
48#[derive(DslVariable, Clone)]
49pub struct ShardCommitmentVariable<C: Config> {
50    pub main_commit: DigestVariable<C>,
51    pub permutation_commit: DigestVariable<C>,
52    pub quotient_commit: DigestVariable<C>,
53}
54
55/// Reference: [sp1_core_machine::stark::ShardOpenedValues]
56#[derive(DslVariable, Debug, Clone)]
57pub struct ShardOpenedValuesVariable<C: Config> {
58    pub chips: Array<C, ChipOpenedValuesVariable<C>>,
59}
60
61/// Reference: [sp1_core_machine::stark::ChipOpenedValues]
62#[derive(Debug, Clone)]
63pub struct ChipOpening<C: Config> {
64    pub preprocessed: AirOpenedValues<Ext<C::F, C::EF>>,
65    pub main: AirOpenedValues<Ext<C::F, C::EF>>,
66    pub permutation: AirOpenedValues<Ext<C::F, C::EF>>,
67    pub quotient: Vec<Vec<Ext<C::F, C::EF>>>,
68    pub cumulative_sum: Ext<C::F, C::EF>,
69    pub log_degree: Var<C::N>,
70}
71
72/// Reference: [sp1_core_machine::stark::ChipOpenedValues]
73#[derive(DslVariable, Debug, Clone)]
74pub struct ChipOpenedValuesVariable<C: Config> {
75    pub preprocessed: AirOpenedValuesVariable<C>,
76    pub main: AirOpenedValuesVariable<C>,
77    pub permutation: AirOpenedValuesVariable<C>,
78    pub quotient: Array<C, Array<C, Ext<C::F, C::EF>>>,
79    pub cumulative_sum: Ext<C::F, C::EF>,
80    pub log_degree: Var<C::N>,
81}
82
83/// Reference: [sp1_core_machine::stark::AirOpenedValues]
84#[derive(DslVariable, Debug, Clone)]
85pub struct AirOpenedValuesVariable<C: Config> {
86    pub local: Array<C, Ext<C::F, C::EF>>,
87    pub next: Array<C, Ext<C::F, C::EF>>,
88}
89
90#[derive(DslVariable, Debug, Clone)]
91pub struct Sha256DigestVariable<C: Config> {
92    pub bytes: Array<C, Felt<C::F>>,
93}
94
95impl<C: Config> Sha256DigestVariable<C> {
96    pub fn from_words(builder: &mut Builder<C>, words: &[Word<Felt<C::F>>]) -> Self {
97        let mut bytes = builder.array(PV_DIGEST_NUM_WORDS * WORD_SIZE);
98        for (i, word) in words.iter().enumerate() {
99            for j in 0..WORD_SIZE {
100                let byte = word[j];
101                builder.set(&mut bytes, i * WORD_SIZE + j, byte);
102            }
103        }
104        Sha256DigestVariable { bytes }
105    }
106}
107
108impl<C: Config> ChipOpening<C> {
109    /// Collect opening values from a dynamic array into vectors.
110    ///
111    /// This method is used to convert a `ChipOpenedValuesVariable` into a `ChipOpenedValues`, which
112    /// are the same values but with each opening converted from a dynamic array into a Rust vector.
113    ///
114    /// *Safety*: This method also verifies that the legnth of the dynamic arrays match the expected
115    /// length of the vectors.
116    pub fn from_variable<A>(
117        builder: &mut Builder<C>,
118        chip: &Chip<C::F, A>,
119        opening: &ChipOpenedValuesVariable<C>,
120    ) -> Self
121    where
122        A: MachineAir<C::F>,
123    {
124        let mut preprocessed = AirOpenedValues { local: vec![], next: vec![] };
125        let preprocessed_width = chip.preprocessed_width();
126        // Assert that the length of the dynamic arrays match the expected length of the vectors.
127        builder.assert_usize_eq(preprocessed_width, opening.preprocessed.local.len());
128        builder.assert_usize_eq(preprocessed_width, opening.preprocessed.next.len());
129        // Collect the preprocessed values into vectors.
130        for i in 0..preprocessed_width {
131            preprocessed.local.push(builder.get(&opening.preprocessed.local, i));
132            preprocessed.next.push(builder.get(&opening.preprocessed.next, i));
133        }
134
135        let mut main = AirOpenedValues { local: vec![], next: vec![] };
136        let main_width = chip.width();
137        // Assert that the length of the dynamic arrays match the expected length of the vectors.
138        builder.assert_usize_eq(main_width, opening.main.local.len());
139        builder.assert_usize_eq(main_width, opening.main.next.len());
140        // Collect the main values into vectors.
141        for i in 0..main_width {
142            main.local.push(builder.get(&opening.main.local, i));
143            main.next.push(builder.get(&opening.main.next, i));
144        }
145
146        let mut permutation = AirOpenedValues { local: vec![], next: vec![] };
147        let permutation_width = C::EF::D * chip.permutation_width();
148        // Assert that the length of the dynamic arrays match the expected length of the vectors.
149        builder.assert_usize_eq(permutation_width, opening.permutation.local.len());
150        builder.assert_usize_eq(permutation_width, opening.permutation.next.len());
151        // Collect the permutation values into vectors.
152        for i in 0..permutation_width {
153            permutation.local.push(builder.get(&opening.permutation.local, i));
154            permutation.next.push(builder.get(&opening.permutation.next, i));
155        }
156
157        let num_quotient_chunks = 1 << chip.log_quotient_degree();
158        let mut quotient = vec![];
159        // Assert that the length of the quotient chunk arrays match the expected length.
160        builder.assert_usize_eq(num_quotient_chunks, opening.quotient.len());
161        // Collect the quotient values into vectors.
162        for i in 0..num_quotient_chunks {
163            let chunk = builder.get(&opening.quotient, i);
164            // Assert that the chunk length matches the expected length.
165            builder.assert_usize_eq(C::EF::D, chunk.len());
166            // Collect the quotient values into vectors.
167            let mut quotient_vals = vec![];
168            for j in 0..C::EF::D {
169                let value = builder.get(&chunk, j);
170                quotient_vals.push(value);
171            }
172            quotient.push(quotient_vals);
173        }
174
175        ChipOpening {
176            preprocessed,
177            main,
178            permutation,
179            quotient,
180            cumulative_sum: opening.cumulative_sum,
181            log_degree: opening.log_degree,
182        }
183    }
184}
185
186impl<C: Config> FromConstant<C> for AirOpenedValuesVariable<C> {
187    type Constant = AirOpenedValues<C::EF>;
188
189    fn constant(value: Self::Constant, builder: &mut Builder<C>) -> Self {
190        AirOpenedValuesVariable {
191            local: builder.constant(value.local),
192            next: builder.constant(value.next),
193        }
194    }
195}
196
197impl<C: Config> FromConstant<C> for ChipOpenedValuesVariable<C> {
198    type Constant = ChipOpenedValues<C::EF>;
199
200    fn constant(value: Self::Constant, builder: &mut Builder<C>) -> Self {
201        ChipOpenedValuesVariable {
202            preprocessed: builder.constant(value.preprocessed),
203            main: builder.constant(value.main),
204            permutation: builder.constant(value.permutation),
205            quotient: builder.constant(value.quotient),
206            cumulative_sum: builder.eval(value.cumulative_sum.cons()),
207            log_degree: builder.eval(C::N::from_canonical_usize(value.log_degree)),
208        }
209    }
210}
211
212impl<C: Config> FriConfigVariable<C> {
213    pub fn get_subgroup(
214        &self,
215        builder: &mut Builder<C>,
216        log_degree: impl Into<Usize<C::N>>,
217    ) -> TwoAdicMultiplicativeCosetVariable<C> {
218        builder.get(&self.subgroups, log_degree)
219    }
220
221    pub fn get_two_adic_generator(
222        &self,
223        builder: &mut Builder<C>,
224        bits: impl Into<Usize<C::N>>,
225    ) -> Felt<C::F> {
226        builder.get(&self.generators, bits)
227    }
228}
sp1_recursion_program/types.rs

sp1_recursion_program/
types.rs
