sp1_recursion_circuit_v2/
constraints.rs

1use p3_air::{Air, BaseAir};
2use p3_baby_bear::BabyBear;
3use p3_commit::{LagrangeSelectors, Mmcs, PolynomialSpace, TwoAdicMultiplicativeCoset};
4use p3_field::{AbstractExtensionField, AbstractField, TwoAdicField};
5use p3_matrix::dense::RowMajorMatrix;
6
7use sp1_recursion_compiler::ir::{
8    Builder, Config, Ext, ExtensionOperand, Felt, SymbolicExt, SymbolicFelt,
9};
10use sp1_stark::{
11    air::MachineAir, AirOpenedValues, ChipOpenedValues, GenericVerifierConstraintFolder,
12    MachineChip, OpeningShapeError,
13};
14
15use crate::{
16    domain::PolynomialSpaceVariable, stark::StarkVerifier, BabyBearFriConfigVariable, CircuitConfig,
17};
18
19pub type RecursiveVerifierConstraintFolder<'a, C> = GenericVerifierConstraintFolder<
20    'a,
21    <C as Config>::F,
22    <C as Config>::EF,
23    Felt<<C as Config>::F>,
24    Ext<<C as Config>::F, <C as Config>::EF>,
25    SymbolicExt<<C as Config>::F, <C as Config>::EF>,
26>;
27
28impl<C, SC, A> StarkVerifier<C, SC, A>
29where
30    C::F: TwoAdicField,
31    SC: BabyBearFriConfigVariable<C>,
32    C: CircuitConfig<F = SC::Val>,
33    <SC::ValMmcs as Mmcs<BabyBear>>::ProverData<RowMajorMatrix<BabyBear>>: Clone,
34    A: MachineAir<C::F> + for<'a> Air<RecursiveVerifierConstraintFolder<'a, C>>,
35{
36    #[allow(clippy::too_many_arguments)]
37    pub fn verify_constraints(
38        builder: &mut Builder<C>,
39        chip: &MachineChip<SC, A>,
40        opening: &ChipOpenedValues<Ext<C::F, C::EF>>,
41        trace_domain: TwoAdicMultiplicativeCoset<C::F>,
42        qc_domains: Vec<TwoAdicMultiplicativeCoset<C::F>>,
43        zeta: Ext<C::F, C::EF>,
44        alpha: Ext<C::F, C::EF>,
45        permutation_challenges: &[Ext<C::F, C::EF>],
46        public_values: &[Felt<C::F>],
47    ) {
48        let sels = trace_domain.selectors_at_point_variable(builder, zeta);
49
50        // Recompute the quotient at zeta from the chunks.
51        let quotient = Self::recompute_quotient(builder, opening, &qc_domains, zeta);
52
53        // Calculate the evaluations of the constraints at zeta.
54        let folded_constraints = Self::eval_constraints(
55            builder,
56            chip,
57            opening,
58            &sels,
59            alpha,
60            permutation_challenges,
61            public_values,
62        );
63
64        // Assert that the quotient times the zerofier is equal to the folded constraints.
65        builder.assert_ext_eq(folded_constraints * sels.inv_zeroifier, quotient);
66    }
67
68    pub fn eval_constraints(
69        builder: &mut Builder<C>,
70        chip: &MachineChip<SC, A>,
71        opening: &ChipOpenedValues<Ext<C::F, C::EF>>,
72        selectors: &LagrangeSelectors<Ext<C::F, C::EF>>,
73        alpha: Ext<C::F, C::EF>,
74        permutation_challenges: &[Ext<C::F, C::EF>],
75        public_values: &[Felt<C::F>],
76    ) -> Ext<C::F, C::EF> {
77        let mut unflatten = |v: &[Ext<C::F, C::EF>]| {
78            v.chunks_exact(<SC::Challenge as AbstractExtensionField<C::F>>::D)
79                .map(|chunk| {
80                    builder.eval(
81                        chunk
82                            .iter()
83                            .enumerate()
84                            .map(
85                                |(e_i, x): (usize, &Ext<C::F, C::EF>)| -> SymbolicExt<C::F, C::EF> {
86                                    SymbolicExt::from(*x) * C::EF::monomial(e_i)
87                                },
88                            )
89                            .sum::<SymbolicExt<_, _>>(),
90                    )
91                })
92                .collect::<Vec<Ext<_, _>>>()
93        };
94        let perm_opening = AirOpenedValues {
95            local: unflatten(&opening.permutation.local),
96            next: unflatten(&opening.permutation.next),
97        };
98
99        let mut folder = RecursiveVerifierConstraintFolder::<C> {
100            preprocessed: opening.preprocessed.view(),
101            main: opening.main.view(),
102            perm: perm_opening.view(),
103            perm_challenges: permutation_challenges,
104            cumulative_sum: opening.cumulative_sum,
105            public_values,
106            is_first_row: selectors.is_first_row,
107            is_last_row: selectors.is_last_row,
108            is_transition: selectors.is_transition,
109            alpha,
110            accumulator: SymbolicExt::zero(),
111            _marker: std::marker::PhantomData,
112        };
113
114        chip.eval(&mut folder);
115        builder.eval(folder.accumulator)
116    }
117
118    pub fn recompute_quotient(
119        builder: &mut Builder<C>,
120        opening: &ChipOpenedValues<Ext<C::F, C::EF>>,
121        qc_domains: &[TwoAdicMultiplicativeCoset<C::F>],
122        zeta: Ext<C::F, C::EF>,
123    ) -> Ext<C::F, C::EF> {
124        let zps = qc_domains
125            .iter()
126            .enumerate()
127            .map(|(i, domain)| {
128                let (zs, zinvs) = qc_domains
129                    .iter()
130                    .enumerate()
131                    .filter(|(j, _)| *j != i)
132                    .map(|(_, other_domain)| {
133                        let first_point = builder.eval(domain.first_point());
134                        (
135                            other_domain
136                                .zp_at_point_variable(builder, zeta)
137                                .to_operand()
138                                .symbolic(),
139                            other_domain.zp_at_point_f(builder, first_point).inverse(),
140                        )
141                    })
142                    .unzip::<_, _, Vec<_>, Vec<_>>();
143                zs.into_iter().product::<SymbolicExt<_, _>>()
144                    * zinvs.into_iter().product::<SymbolicFelt<_>>()
145            })
146            .collect::<Vec<SymbolicExt<_, _>>>()
147            .into_iter()
148            .map(|x| builder.eval(x))
149            .collect::<Vec<Ext<_, _>>>();
150
151        builder.eval(
152            opening
153                .quotient
154                .iter()
155                .enumerate()
156                .map(|(ch_i, ch)| {
157                    assert_eq!(ch.len(), C::EF::D);
158                    ch.iter()
159                        .enumerate()
160                        .map(|(e_i, &c)| zps[ch_i] * C::EF::monomial(e_i) * c)
161                        .sum::<SymbolicExt<_, _>>()
162                })
163                .sum::<SymbolicExt<_, _>>(),
164        )
165    }
166
167    pub fn verify_opening_shape(
168        chip: &MachineChip<SC, A>,
169        opening: &ChipOpenedValues<Ext<C::F, C::EF>>,
170    ) -> Result<(), OpeningShapeError> {
171        // Verify that the preprocessed width matches the expected value for the chip.
172        if opening.preprocessed.local.len() != chip.preprocessed_width() {
173            return Err(OpeningShapeError::PreprocessedWidthMismatch(
174                chip.preprocessed_width(),
175                opening.preprocessed.local.len(),
176            ));
177        }
178        if opening.preprocessed.next.len() != chip.preprocessed_width() {
179            return Err(OpeningShapeError::PreprocessedWidthMismatch(
180                chip.preprocessed_width(),
181                opening.preprocessed.next.len(),
182            ));
183        }
184
185        // Verify that the main width matches the expected value for the chip.
186        if opening.main.local.len() != chip.width() {
187            return Err(OpeningShapeError::MainWidthMismatch(
188                chip.width(),
189                opening.main.local.len(),
190            ));
191        }
192        if opening.main.next.len() != chip.width() {
193            return Err(OpeningShapeError::MainWidthMismatch(
194                chip.width(),
195                opening.main.next.len(),
196            ));
197        }
198
199        // Verify that the permutation width matches the expected value for the chip.
200        if opening.permutation.local.len()
201            != chip.permutation_width() * <SC::Challenge as AbstractExtensionField<C::F>>::D
202        {
203            return Err(OpeningShapeError::PermutationWidthMismatch(
204                chip.permutation_width(),
205                opening.permutation.local.len(),
206            ));
207        }
208        if opening.permutation.next.len()
209            != chip.permutation_width() * <SC::Challenge as AbstractExtensionField<C::F>>::D
210        {
211            return Err(OpeningShapeError::PermutationWidthMismatch(
212                chip.permutation_width(),
213                opening.permutation.next.len(),
214            ));
215        }
216
217        // Verift that the number of quotient chunks matches the expected value for the chip.
218        if opening.quotient.len() != chip.quotient_width() {
219            return Err(OpeningShapeError::QuotientWidthMismatch(
220                chip.quotient_width(),
221                opening.quotient.len(),
222            ));
223        }
224        // For each quotient chunk, verify that the number of elements is equal to the degree of the
225        // challenge extension field over the value field.
226        for slice in &opening.quotient {
227            if slice.len() != <SC::Challenge as AbstractExtensionField<C::F>>::D {
228                return Err(OpeningShapeError::QuotientChunkSizeMismatch(
229                    <SC::Challenge as AbstractExtensionField<C::F>>::D,
230                    slice.len(),
231                ));
232            }
233        }
234
235        Ok(())
236    }
237}
sp1_recursion_circuit_v2/constraints.rs

sp1_recursion_circuit_v2/
constraints.rs
