Skip to main content

sp1_recursion_circuit/basefold/
mod.rs

1use crate::{
2    challenger::{CanObserveVariable, CanSampleBitsVariable, FieldChallengerVariable},
3    hash::FieldHasherVariable,
4    symbolic::IntoSymbolic,
5    CircuitConfig, SP1FieldConfigVariable,
6};
7use itertools::Itertools;
8use slop_algebra::{AbstractField, TwoAdicField};
9use slop_basefold::{FriConfig, BATCH_GRINDING_BITS};
10use slop_multilinear::{partial_lagrange_blocking, MleEval, Point};
11use sp1_recursion_compiler::{
12    circuit::CircuitV2Builder,
13    ir::{Builder, DslIr, Ext, Felt, SymbolicExt},
14};
15
16use sp1_primitives::{SP1ExtensionField, SP1Field};
17use sp1_recursion_executor::D;
18use std::{iter::once, marker::PhantomData};
19use tcs::{RecursiveMerkleTreeTcs, RecursiveTensorCsOpening};
20pub mod merkle_tree;
21pub mod stacked;
22pub mod tcs;
23mod whir;
24pub mod witness;
25
26pub struct RecursiveBasefoldConfigImpl<C, SC>(PhantomData<(C, SC)>);
27
28pub struct RecursiveBasefoldProof<C: CircuitConfig, SC: SP1FieldConfigVariable<C>> {
29    /// The univariate polynomials that are used in the sumcheck part of the BaseFold protocol.
30    pub univariate_messages: Vec<[Ext<SP1Field, SP1ExtensionField>; 2]>,
31    /// The FRI parts of the proof.
32    /// The commitments to the folded polynomials produced in the commit phase.
33    pub fri_commitments: Vec<<SC as FieldHasherVariable<C>>::DigestVariable>,
34    /// The query openings for the individual multilinear polynomials.
35    /// The vector is indexed by the batch number.
36    pub component_polynomials_query_openings_and_proofs:
37        Vec<RecursiveTensorCsOpening<<SC as FieldHasherVariable<C>>::DigestVariable>>,
38    /// The query openings and the FRI query proofs for the FRI query phase.
39    pub query_phase_openings_and_proofs:
40        Vec<RecursiveTensorCsOpening<<SC as FieldHasherVariable<C>>::DigestVariable>>,
41    /// The prover performs FRI until we reach a polynomial of degree 0, and return the constant
42    /// value of this polynomial.
43    pub final_poly: Ext<SP1Field, SP1ExtensionField>,
44    /// Proof-of-work witness.
45    pub pow_witness: Felt<SP1Field>,
46    /// Batch grinding witness.
47    pub batch_grinding_witness: Felt<SP1Field>,
48}
49
50#[derive(Clone)]
51pub struct RecursiveBasefoldVerifier<C: CircuitConfig, SC: SP1FieldConfigVariable<C>> {
52    pub fri_config: FriConfig<SP1Field>,
53    pub tcs: RecursiveMerkleTreeTcs<C, SC>,
54}
55
56pub trait RecursiveMultilinearPcsVerifier: Sized {
57    type Commitment;
58    type Proof;
59    type Circuit: CircuitConfig<Bit = Self::Bit>;
60    type Bit;
61    type Challenger: FieldChallengerVariable<Self::Circuit, Self::Bit>;
62
63    fn verify_trusted_evaluations(
64        &self,
65        builder: &mut Builder<Self::Circuit>,
66        commitments: &[Self::Commitment],
67        point: Point<Ext<SP1Field, SP1ExtensionField>>,
68        evaluation_claims: &[MleEval<Ext<SP1Field, SP1ExtensionField>>],
69        proof: &Self::Proof,
70        challenger: &mut Self::Challenger,
71    );
72
73    fn verify_untrusted_evaluations(
74        &self,
75        builder: &mut Builder<Self::Circuit>,
76        commitments: &[Self::Commitment],
77        point: Point<Ext<SP1Field, SP1ExtensionField>>,
78        evaluation_claims: &[MleEval<Ext<SP1Field, SP1ExtensionField>>],
79        proof: &Self::Proof,
80        challenger: &mut Self::Challenger,
81    ) {
82        for round in evaluation_claims.iter() {
83            for evaluation in round.iter() {
84                let evaluation_felts = Self::Circuit::ext2felt(builder, *evaluation);
85                evaluation_felts.iter().for_each(|felt| challenger.observe(builder, *felt));
86            }
87        }
88        self.verify_trusted_evaluations(
89            builder,
90            commitments,
91            point,
92            evaluation_claims,
93            proof,
94            challenger,
95        )
96    }
97}
98
99impl<C: CircuitConfig, SC: SP1FieldConfigVariable<C>> RecursiveMultilinearPcsVerifier
100    for RecursiveBasefoldVerifier<C, SC>
101{
102    type Commitment = SC::DigestVariable;
103    type Proof = RecursiveBasefoldProof<C, SC>;
104    type Circuit = C;
105    type Bit = C::Bit;
106    type Challenger = SC::FriChallengerVariable;
107
108    fn verify_trusted_evaluations(
109        &self,
110        builder: &mut Builder<Self::Circuit>,
111        commitments: &[Self::Commitment],
112        point: Point<Ext<SP1Field, SP1ExtensionField>>,
113        evaluation_claims: &[MleEval<Ext<SP1Field, SP1ExtensionField>>],
114        proof: &Self::Proof,
115        challenger: &mut Self::Challenger,
116    ) {
117        self.verify_mle_evaluations(
118            builder,
119            commitments,
120            point,
121            evaluation_claims,
122            proof,
123            challenger,
124        )
125    }
126}
127
128impl<C: CircuitConfig, SC: SP1FieldConfigVariable<C>> RecursiveBasefoldVerifier<C, SC> {
129    fn verify_mle_evaluations(
130        &self,
131        builder: &mut Builder<C>,
132        commitments: &[SC::DigestVariable],
133        mut point: Point<Ext<SP1Field, SP1ExtensionField>>,
134        evaluation_claims: &[MleEval<Ext<SP1Field, SP1ExtensionField>>],
135        proof: &RecursiveBasefoldProof<C, SC>,
136        challenger: &mut SC::FriChallengerVariable,
137    ) {
138        // Check batch grinding witness.
139        challenger.check_witness(builder, BATCH_GRINDING_BITS, proof.batch_grinding_witness);
140
141        // Sample batching coefficients via partial Lagrange basis.
142        let total_len = evaluation_claims
143            .iter()
144            .map(|batch_claims| batch_claims.num_polynomials())
145            .sum::<usize>();
146        let num_batching_variables = total_len.next_power_of_two().ilog2();
147        let batching_point: Point<Ext<SP1Field, SP1ExtensionField>> =
148            Point::from_iter((0..num_batching_variables).map(|_| challenger.sample_ext(builder)));
149        let batching_point_symbolic = IntoSymbolic::<C>::as_symbolic(&batching_point);
150        let batching_coefficients_symbolic =
151            partial_lagrange_blocking(&batching_point_symbolic).into_buffer().into_vec();
152
153        // Force modular reduction the batching coefficients since they are used repeatedly later on
154        // which would save redundant reductions in the later computations.
155        let batching_coefficients: Vec<Ext<SP1Field, SP1ExtensionField>> =
156            batching_coefficients_symbolic
157                .into_iter()
158                .map(|x| {
159                    let element = x.as_ext().expect("lagrange coefficient should be a variable");
160                    builder.reduce_e(element);
161                    element
162                })
163                .collect();
164
165        builder.cycle_tracker_v2_enter("compute eval_claim");
166        // Compute the batched evaluation claim.
167        let eval_claim = evaluation_claims
168            .iter()
169            .flat_map(|batch_claims| batch_claims.iter())
170            .zip(batching_coefficients.iter())
171            .map(|(eval, batch_power)| *eval * *batch_power)
172            .sum::<SymbolicExt<SP1Field, SP1ExtensionField>>();
173        builder.cycle_tracker_v2_exit();
174
175        // Assert correctness of shape.
176        assert_eq!(
177            proof.fri_commitments.len(),
178            proof.univariate_messages.len(),
179            "Sumcheck FRI Length Mismatch"
180        );
181
182        // The prover messages correspond to fixing the last coordinate first, so we reverse the
183        // underlying point for the verification.
184        point.reverse();
185
186        // Sample the challenges used for FRI folding and BaseFold random linear combinations.
187        let len_felt: Felt<_> =
188            builder.constant(SP1Field::from_canonical_usize(proof.fri_commitments.len()));
189        challenger.observe(builder, len_felt);
190        let betas = proof
191            .fri_commitments
192            .iter()
193            .zip(proof.univariate_messages.iter())
194            .map(|(commitment, poly)| {
195                poly.iter().copied().for_each(|x| {
196                    let x_felts = C::ext2felt(builder, x);
197                    x_felts.iter().for_each(|felt| challenger.observe(builder, *felt));
198                });
199                challenger.observe(builder, *commitment);
200                challenger.sample_ext(builder)
201            })
202            .collect::<Vec<_>>();
203
204        // Check the consistency of the first univariate message with the claimed evaluation. The
205        // first_poly is supposed to be `vals(X_0, X_1, ..., X_{d-1}, 0), vals(X_0, X_1, ...,
206        // X_{d-1}, 1)`. Given this, the claimed evaluation should be `(1 - X_d) *
207        // first_poly[0] + X_d * first_poly[1]`.
208        let first_poly = proof.univariate_messages[0];
209        let one: Ext<SP1Field, SP1ExtensionField> = builder.constant(SP1ExtensionField::one());
210
211        builder.assert_ext_eq(
212            eval_claim,
213            (one - *point[0]) * first_poly[0] + *point[0] * first_poly[1],
214        );
215
216        // Fold the two messages into a single evaluation claim for the next round, using the
217        // sampled randomness.
218        let mut expected_eval = first_poly[0] + betas[0] * first_poly[1];
219
220        // Check round-by-round consistency between the successive sumcheck univariate messages.
221        for (i, (poly, beta)) in
222            proof.univariate_messages[1..].iter().zip(betas[1..].iter()).enumerate()
223        {
224            // The check is similar to the one for `first_poly`.
225            let i = i + 1;
226            builder.assert_ext_eq(expected_eval, (one - *point[i]) * poly[0] + *point[i] * poly[1]);
227
228            // Fold the two pieces of the message.
229            expected_eval = poly[0] + *beta * poly[1];
230        }
231
232        let final_poly_felts = C::ext2felt(builder, proof.final_poly);
233        challenger.observe_slice(builder, final_poly_felts);
234
235        // Check proof of work (grinding to find a number that hashes to have
236        // `self.config.proof_of_work_bits` zeroes at the beginning).
237        challenger.check_witness(builder, self.fri_config.proof_of_work_bits, proof.pow_witness);
238
239        let log_len = proof.fri_commitments.len();
240
241        builder.cycle_tracker_v2_enter("sample query_indices");
242        // Sample query indices for the FRI query IOPP part of BaseFold. This part is very similar
243        // to the corresponding part in the univariate FRI verifier.
244        let query_indices = (0..self.fri_config.num_queries)
245            .map(|_| challenger.sample_bits(builder, log_len + self.fri_config.log_blowup()))
246            .collect::<Vec<_>>();
247        builder.cycle_tracker_v2_exit();
248
249        builder.cycle_tracker_v2_enter("compute batch_evals");
250
251        // Compute the batch evaluations from the openings of the component polynomials.
252        let zero = SymbolicExt::<SP1Field, SP1ExtensionField>::zero();
253        let mut batch_evals = vec![zero; query_indices.len()];
254        let mut batch_idx = 0;
255        for opening in proof.component_polynomials_query_openings_and_proofs.iter() {
256            let values = &opening.values;
257            let total_columns = values.get(0).unwrap().as_slice().len();
258            let round_coefficients = &batching_coefficients[batch_idx..batch_idx + total_columns];
259            for (batch_eval, values) in batch_evals.iter_mut().zip_eq(values.split()) {
260                for (value, coeff) in values.as_slice().iter().zip(round_coefficients.iter()) {
261                    *batch_eval += *coeff * *value;
262                }
263            }
264            batch_idx += total_columns;
265        }
266        let batch_evals: Vec<Ext<SP1Field, SP1ExtensionField>> =
267            batch_evals.into_iter().map(|x| builder.eval(x)).collect_vec();
268        builder.cycle_tracker_v2_exit();
269
270        builder.cycle_tracker_v2_enter("verify_tensor_openings");
271
272        // Verify the proof of the claimed values.
273        for (commit, opening) in
274            commitments.iter().zip_eq(proof.component_polynomials_query_openings_and_proofs.iter())
275        {
276            RecursiveMerkleTreeTcs::<C, SC>::verify_tensor_openings(
277                builder,
278                commit,
279                &query_indices,
280                opening,
281            );
282        }
283        builder.cycle_tracker_v2_exit();
284
285        builder.cycle_tracker_v2_enter("verify_queries");
286        // Check that the query openings are consistent as FRI messages.
287        self.verify_queries(
288            builder,
289            &proof.fri_commitments,
290            &query_indices,
291            proof.final_poly,
292            batch_evals,
293            &proof.query_phase_openings_and_proofs,
294            &betas,
295        );
296        builder.cycle_tracker_v2_exit();
297
298        // The final consistency check between the FRI messages and the partial evaluation messages.
299        builder.assert_ext_eq(
300            proof.final_poly,
301            proof.univariate_messages.last().unwrap()[0]
302                + *betas.last().unwrap() * proof.univariate_messages.last().unwrap()[1],
303        );
304    }
305
306    /// The FRI verifier for a single query. We modify this from Plonky3 to be compatible with
307    /// opening only a single vector.
308    #[allow(clippy::too_many_arguments)]
309    fn verify_queries(
310        &self,
311        builder: &mut Builder<C>,
312        commitments: &[SC::DigestVariable],
313        indices: &[Vec<C::Bit>],
314        final_poly: Ext<SP1Field, SP1ExtensionField>,
315        reduced_openings: Vec<Ext<SP1Field, SP1ExtensionField>>,
316        query_openings: &[RecursiveTensorCsOpening<SC::DigestVariable>],
317        betas: &[Ext<SP1Field, SP1ExtensionField>],
318    ) {
319        let log_max_height = commitments.len() + self.fri_config.log_blowup();
320
321        let mut folded_evals = reduced_openings;
322        builder.cycle_tracker_v2_enter("compute exp reverse bits");
323        let mut xis: Vec<Felt<SP1Field>> = indices
324            .iter()
325            .map(|index| {
326                let two_adic_generator: Felt<SP1Field> =
327                    builder.constant(SP1Field::two_adic_generator(log_max_height));
328                C::exp_reverse_bits(builder, two_adic_generator, index.to_vec())
329            })
330            .collect::<Vec<_>>();
331        builder.cycle_tracker_v2_exit();
332
333        let mut indices = indices.to_vec();
334
335        // Loop over the FRI queries.
336        for ((commitment, query_opening), beta) in
337            commitments.iter().zip_eq(query_openings.iter()).zip_eq(betas)
338        {
339            let openings = &query_opening.values;
340
341            for (((index, folded_eval), opening), x) in indices
342                .iter_mut()
343                .zip_eq(folded_evals.iter_mut())
344                .zip_eq(openings.split())
345                .zip_eq(xis.iter_mut())
346            {
347                let index_sibling_complement = index[0];
348                let index_pair = &index[1..];
349
350                builder.reduce_e(*folded_eval);
351
352                let evals: [Ext<SP1Field, SP1ExtensionField>; 2] = opening
353                    .as_slice()
354                    .chunks_exact(D)
355                    .map(|slice| {
356                        let reconstructed_ext: Ext<SP1Field, SP1ExtensionField> =
357                            C::felt2ext(builder, slice.try_into().unwrap());
358                        reconstructed_ext
359                    })
360                    .collect::<Vec<_>>()
361                    .try_into()
362                    .unwrap();
363
364                let eval_ordered = C::select_chain_ef(
365                    builder,
366                    index_sibling_complement,
367                    once(evals[0]),
368                    once(evals[1]),
369                );
370
371                // Check that the folded evaluation is consistent with the FRI query proof opening.
372                builder.assert_ext_eq(eval_ordered[0], *folded_eval);
373
374                let xs_new = builder.eval((*x) * SP1Field::two_adic_generator(1));
375                let xs =
376                    C::select_chain_f(builder, index_sibling_complement, once(*x), once(xs_new));
377
378                // interpolate and evaluate at beta
379                let temp_1: Felt<_> = builder.uninit();
380                builder.push_op(DslIr::SubF(temp_1, xs[1], xs[0]));
381
382                // let temp_2 = evals_ext[1] - evals_ext[0];
383                let temp_2: Ext<_, _> = builder.uninit();
384                builder.push_op(DslIr::SubE(temp_2, evals[1], evals[0]));
385
386                // let temp_3 = temp_2 / temp_1;
387                let temp_3: Ext<_, _> = builder.uninit();
388                builder.push_op(DslIr::DivEF(temp_3, temp_2, temp_1));
389
390                // let temp_4 = beta - xs[0];
391                let temp_4: Ext<_, _> = builder.uninit();
392                builder.push_op(DslIr::SubEF(temp_4, *beta, xs[0]));
393
394                // let temp_5 = temp_4 * temp_3;
395                let temp_5: Ext<_, _> = builder.uninit();
396                builder.push_op(DslIr::MulE(temp_5, temp_4, temp_3));
397
398                // let temp6 = evals_ext[0] + temp_5;
399                let temp_6: Ext<_, _> = builder.uninit();
400                builder.push_op(DslIr::AddE(temp_6, evals[0], temp_5));
401                *folded_eval = temp_6;
402
403                // let temp_7 = x * x;
404                let temp_7: Felt<_> = builder.uninit();
405                builder.push_op(DslIr::MulF(temp_7, *x, *x));
406                *x = temp_7;
407
408                *index = index_pair.to_vec();
409            }
410            // Check that the opening is consistent with the commitment.
411            RecursiveMerkleTreeTcs::<C, SC>::verify_tensor_openings(
412                builder,
413                commitment,
414                &indices,
415                query_opening,
416            );
417        }
418
419        for folded_eval in folded_evals {
420            builder.assert_ext_eq(folded_eval, final_poly);
421        }
422    }
423}
424
425#[cfg(test)]
426mod tests {
427    use rand::thread_rng;
428    use slop_commit::Message;
429    use sp1_recursion_compiler::{circuit::AsmConfig, config::InnerConfig};
430    use std::sync::Arc;
431
432    use slop_algebra::extension::BinomialExtensionField;
433    use slop_challenger::IopCtx;
434    use sp1_primitives::SP1DiffusionMatrix;
435
436    use crate::{challenger::DuplexChallengerVariable, witness::Witnessable};
437
438    use super::*;
439    use slop_basefold::BasefoldVerifier;
440    use slop_basefold_prover::BasefoldProver;
441    use slop_challenger::CanObserve;
442
443    use slop_commit::Rounds;
444
445    use slop_multilinear::{Evaluations, Mle};
446    use sp1_hypercube::inner_perm;
447    use sp1_primitives::{SP1Field, SP1GlobalContext};
448    use sp1_recursion_compiler::circuit::{AsmBuilder, AsmCompiler};
449    use sp1_recursion_executor::Executor;
450
451    type F = SP1Field;
452    type EF = BinomialExtensionField<SP1Field, 4>;
453
454    #[test]
455    fn test_basefold_proof() {
456        type C = InnerConfig;
457        type SC = SP1GlobalContext;
458
459        type Prover = BasefoldProver<SP1GlobalContext, sp1_hypercube::prover::SP1MerkleTreeProver>;
460
461        let num_variables = 16;
462        let round_widths = [vec![16, 10, 14], vec![20, 78, 34], vec![10, 10]];
463
464        let mut rng = thread_rng();
465        let round_mles = round_widths
466            .iter()
467            .map(|widths| {
468                widths
469                    .iter()
470                    .map(|&w| Mle::<SP1Field>::rand(&mut rng, w, num_variables))
471                    .collect::<Message<_>>()
472            })
473            .collect::<Rounds<_>>();
474
475        let verifier =
476            BasefoldVerifier::<_>::new(FriConfig::default_fri_config(), round_widths.len());
477        let recursive_verifier = RecursiveBasefoldVerifier::<C, SC> {
478            fri_config: verifier.fri_config,
479            tcs: RecursiveMerkleTreeTcs::<C, SC>(PhantomData),
480        };
481
482        let prover = Prover::new(&verifier);
483
484        let mut challenger = SC::default_challenger();
485        let mut commitments = vec![];
486        let mut prover_data = Rounds::new();
487        let mut eval_claims = Rounds::new();
488        let point = Point::<EF>::rand(&mut rng, num_variables);
489        for mles in round_mles.iter() {
490            let (commitment, data) = prover.commit_mles(mles.clone()).unwrap();
491            challenger.observe(commitment);
492            commitments.push(commitment);
493            prover_data.push(data);
494            let evaluations =
495                mles.iter().map(|mle| mle.eval_at(&point)).collect::<Evaluations<_>>();
496            eval_claims.push(evaluations);
497        }
498
499        let proof = prover
500            .prove_trusted_mle_evaluations(
501                point.clone(),
502                round_mles,
503                eval_claims.clone(),
504                prover_data,
505                &mut challenger,
506            )
507            .unwrap();
508
509        let mut builder = AsmBuilder::default();
510        let mut witness_stream = Vec::new();
511        let mut challenger_variable = DuplexChallengerVariable::new(&mut builder);
512        let eval_claims = eval_claims
513            .iter()
514            .map(|round| round.into_iter().flat_map(|x| x.into_iter()).collect::<MleEval<_>>())
515            .collect::<Rounds<_>>();
516
517        for commitment in commitments.iter() {
518            challenger.observe(*commitment);
519        }
520
521        Witnessable::<AsmConfig>::write(&commitments, &mut witness_stream);
522        let commitments = commitments.read(&mut builder);
523
524        for commitment in commitments.iter() {
525            challenger_variable.observe(&mut builder, *commitment);
526        }
527
528        Witnessable::<AsmConfig>::write(&point, &mut witness_stream);
529        let point = point.read(&mut builder);
530
531        Witnessable::<AsmConfig>::write(&eval_claims, &mut witness_stream);
532        let eval_claims = eval_claims.read(&mut builder);
533
534        Witnessable::<AsmConfig>::write(&proof, &mut witness_stream);
535        let proof = proof.read(&mut builder);
536
537        RecursiveBasefoldVerifier::<C, SC>::verify_mle_evaluations(
538            &recursive_verifier,
539            &mut builder,
540            &commitments,
541            point,
542            &eval_claims,
543            &proof,
544            &mut challenger_variable,
545        );
546        let block = builder.into_root_block();
547        let mut compiler = AsmCompiler::default();
548        let program = Arc::new(compiler.compile_inner(block).validate().unwrap());
549        let mut executor =
550            Executor::<F, EF, SP1DiffusionMatrix>::new(program.clone(), inner_perm());
551        executor.witness_stream = witness_stream.into();
552        executor.run().unwrap();
553    }
554
555    #[test]
556    fn test_invalid_basefold_proof() {
557        type C = InnerConfig;
558        type SC = SP1GlobalContext;
559        type Prover = BasefoldProver<SP1GlobalContext, sp1_hypercube::prover::SP1MerkleTreeProver>;
560
561        let num_variables = 16;
562        let round_widths = [vec![16, 10, 14], vec![20, 78, 34], vec![10, 10]];
563        let fri_config = FriConfig::default_fri_config();
564
565        let mut rng = thread_rng();
566        let round_mles = round_widths
567            .iter()
568            .map(|widths| {
569                widths
570                    .iter()
571                    .map(|&w| Mle::<SP1Field>::rand(&mut rng, w, num_variables))
572                    .collect::<Message<_>>()
573            })
574            .collect::<Rounds<_>>();
575
576        let verifier = BasefoldVerifier::<SC>::new(fri_config, round_widths.len());
577        let recursive_verifier = RecursiveBasefoldVerifier::<C, SC> {
578            fri_config: verifier.fri_config,
579            tcs: RecursiveMerkleTreeTcs::<C, SC>(PhantomData),
580        };
581
582        let prover = Prover::new(&verifier);
583
584        let mut challenger = SC::default_challenger();
585        let mut commitments = vec![];
586        let mut prover_data = Rounds::new();
587        let mut eval_claims = Rounds::new();
588        let point = Point::<EF>::rand(&mut rng, num_variables);
589        for mles in round_mles.iter() {
590            let (commitment, data) = prover.commit_mles(mles.clone()).unwrap();
591            challenger.observe(commitment);
592            commitments.push(commitment);
593            prover_data.push(data);
594            let evaluations =
595                mles.iter().map(|mle| mle.eval_at(&point)).collect::<Evaluations<_>>();
596            eval_claims.push(evaluations);
597        }
598
599        let proof = prover
600            .prove_trusted_mle_evaluations(
601                point.clone(),
602                round_mles,
603                eval_claims.clone(),
604                prover_data,
605                &mut challenger,
606            )
607            .unwrap();
608
609        // Make a new point that is different from the original point.
610        let point = Point::<EF>::rand(&mut rng, num_variables);
611
612        let mut builder = AsmBuilder::default();
613        let mut witness_stream = Vec::new();
614        let mut challenger_variable = DuplexChallengerVariable::new(&mut builder);
615
616        for commitment in commitments.iter() {
617            challenger.observe(*commitment);
618        }
619
620        Witnessable::<AsmConfig>::write(&commitments, &mut witness_stream);
621        let commitments = commitments.read(&mut builder);
622
623        for commitment in commitments.iter() {
624            challenger_variable.observe(&mut builder, *commitment);
625        }
626
627        Witnessable::<AsmConfig>::write(&point, &mut witness_stream);
628        let point = point.read(&mut builder);
629
630        Witnessable::<AsmConfig>::write(&eval_claims, &mut witness_stream);
631        let eval_claims = eval_claims.read(&mut builder);
632
633        Witnessable::<AsmConfig>::write(&proof, &mut witness_stream);
634        let proof = proof.read(&mut builder);
635
636        let eval_claims = eval_claims
637            .iter()
638            .map(|round| {
639                round.into_iter().flat_map(|x| x.into_iter()).copied().collect::<MleEval<_>>()
640            })
641            .collect::<Rounds<_>>();
642
643        RecursiveBasefoldVerifier::<C, SC>::verify_mle_evaluations(
644            &recursive_verifier,
645            &mut builder,
646            &commitments,
647            point,
648            &eval_claims,
649            &proof,
650            &mut challenger_variable,
651        );
652        let block = builder.into_root_block();
653        let mut compiler = AsmCompiler::default();
654        let program = Arc::new(compiler.compile_inner(block).validate().unwrap());
655        let mut executor =
656            Executor::<F, EF, SP1DiffusionMatrix>::new(program.clone(), inner_perm());
657        executor.witness_stream = witness_stream.into();
658        executor.run().expect_err("invalid proof should not be verified");
659    }
660}