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 pub univariate_messages: Vec<[Ext<SP1Field, SP1ExtensionField>; 2]>,
31 pub fri_commitments: Vec<<SC as FieldHasherVariable<C>>::DigestVariable>,
34 pub component_polynomials_query_openings_and_proofs:
37 Vec<RecursiveTensorCsOpening<<SC as FieldHasherVariable<C>>::DigestVariable>>,
38 pub query_phase_openings_and_proofs:
40 Vec<RecursiveTensorCsOpening<<SC as FieldHasherVariable<C>>::DigestVariable>>,
41 pub final_poly: Ext<SP1Field, SP1ExtensionField>,
44 pub pow_witness: Felt<SP1Field>,
46 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 challenger.check_witness(builder, BATCH_GRINDING_BITS, proof.batch_grinding_witness);
140
141 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 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 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_eq!(
177 proof.fri_commitments.len(),
178 proof.univariate_messages.len(),
179 "Sumcheck FRI Length Mismatch"
180 );
181
182 point.reverse();
185
186 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 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 let mut expected_eval = first_poly[0] + betas[0] * first_poly[1];
219
220 for (i, (poly, beta)) in
222 proof.univariate_messages[1..].iter().zip(betas[1..].iter()).enumerate()
223 {
224 let i = i + 1;
226 builder.assert_ext_eq(expected_eval, (one - *point[i]) * poly[0] + *point[i] * poly[1]);
227
228 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 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 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 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 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 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 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 #[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 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 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 let temp_1: Felt<_> = builder.uninit();
380 builder.push_op(DslIr::SubF(temp_1, xs[1], xs[0]));
381
382 let temp_2: Ext<_, _> = builder.uninit();
384 builder.push_op(DslIr::SubE(temp_2, evals[1], evals[0]));
385
386 let temp_3: Ext<_, _> = builder.uninit();
388 builder.push_op(DslIr::DivEF(temp_3, temp_2, temp_1));
389
390 let temp_4: Ext<_, _> = builder.uninit();
392 builder.push_op(DslIr::SubEF(temp_4, *beta, xs[0]));
393
394 let temp_5: Ext<_, _> = builder.uninit();
396 builder.push_op(DslIr::MulE(temp_5, temp_4, temp_3));
397
398 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: 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 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 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}