1use std::rc::Rc;
2
3use crate::{
4 proofs::{
5 prover::make_padded_proof_from_p2p,
6 public_input::{
7 plonk_checks::ShiftingValue,
8 prepared_statement::{DeferredValues, PreparedStatement, ProofState},
9 },
10 unfinalized::dummy_ipa_step_challenges_computed,
11 util::proof_evaluation_to_absorption_sequence,
12 verifiers::wrap_domains,
13 wrap::{
14 create_oracle_with_public_input, dummy_ipa_wrap_sg, wrap_verifier, Domain,
15 COMMON_MAX_DEGREE_WRAP_LOG2,
16 },
17 },
18 verifier::{get_srs, get_srs_mut},
19};
20use anyhow::Context;
21use ark_ff::{fields::arithmetic::InvalidBigInt, BigInteger256, One, Zero};
22use ark_poly::{
23 univariate::DensePolynomial, EvaluationDomain, Radix2EvaluationDomain, UVPolynomial,
24};
25use kimchi::proof::{PointEvaluations, ProverCommitments, RecursionChallenge};
26use mina_curves::pasta::{Fp, Fq, Pallas};
27use mina_p2p_messages::v2;
28use poly_commitment::{commitment::b_poly_coefficients, evaluation_proof::OpeningProof};
29
30use crate::proofs::{
31 public_input::{
32 plonk_checks::{derive_plonk, InCircuit},
33 prepared_statement::Plonk,
34 },
35 transaction::endos,
36 util::{challenge_polynomial, four_u64_to_field},
37 verification::{make_scalars_env, prev_evals_from_p2p},
38 wrap::{
39 combined_inner_product, evals_of_split_evals, CombinedInnerProductParams,
40 COMMON_MAX_DEGREE_STEP_LOG2,
41 },
42 BACKEND_TICK_ROUNDS_N, BACKEND_TOCK_ROUNDS_N,
43};
44
45use super::{
46 constants::ProofConstants,
47 field::{Boolean, CircuitVar, FieldWitness, GroupAffine},
48 public_input::{messages::MessagesForNextWrapProof, plonk_checks::PlonkMinimal},
49 to_field_elements::{ToFieldElements, ToFieldElementsDebug},
50 transaction::{
51 create_proof, make_group, messages_for_next_wrap_proof_padding,
52 scalar_challenge::to_field_checked, Check, CircuitPlonkVerificationKeyEvals,
53 CreateProofParams, InnerCurve, MessagesForNextStepProof, PlonkVerificationKeyEvals,
54 ProofWithPublic, Prover, ReducedMessagesForNextStepProof, StepStatement,
55 },
56 unfinalized::{evals_from_p2p, AllEvals, EvalsWithPublicInput, Unfinalized},
57 util::{extract_bulletproof, two_u64_to_field},
58 witness::Witness,
59 wrap::Domains,
60 ProverProof, VerifierIndex,
61};
62
63#[derive(Clone)]
64pub struct PreviousProofStatement<'a> {
65 pub public_input: Rc<dyn ToFieldElementsDebug>,
66 pub proof: &'a v2::PicklesProofProofsVerified2ReprStableV2,
67 pub proof_must_verify: CircuitVar<Boolean>,
68}
69
70pub struct InductiveRule<'a, const N_PREVIOUS: usize> {
71 pub previous_proof_statements: [PreviousProofStatement<'a>; N_PREVIOUS],
72 pub public_output: (),
73 pub auxiliary_output: (),
74}
75
76impl InductiveRule<'_, 0> {
77 pub fn empty() -> Self {
78 Self {
79 previous_proof_statements: [],
80 public_output: (),
81 auxiliary_output: (),
82 }
83 }
84}
85
86#[derive(Clone, Copy, Debug)]
87pub enum OptFlag {
88 Yes,
89 No,
90 Maybe,
91}
92
93#[derive(Clone, Debug)]
94pub enum Opt<T> {
95 Some(T),
96 No,
97 Maybe(Boolean, T),
98}
99
100impl<T> Opt<T> {
101 fn map<V>(&self, fun: impl Fn(&T) -> V) -> Opt<V> {
102 match self {
103 Opt::Some(v) => Opt::Some(fun(v)),
104 Opt::No => Opt::No,
105 Opt::Maybe(b, v) => Opt::Maybe(*b, fun(v)),
106 }
107 }
108}
109
110#[derive(Clone, Debug)]
111pub struct FeatureFlags<Bool> {
112 pub range_check0: Bool,
113 pub range_check1: Bool,
114 pub foreign_field_add: Bool,
115 pub foreign_field_mul: Bool,
116 pub xor: Bool,
117 pub rot: Bool,
118 pub lookup: Bool,
119 pub runtime_tables: Bool,
120}
121
122impl FeatureFlags<Boolean> {
123 pub fn empty() -> Self {
124 Self {
125 range_check0: Boolean::False,
126 range_check1: Boolean::False,
127 foreign_field_add: Boolean::False,
128 foreign_field_mul: Boolean::False,
129 xor: Boolean::False,
130 rot: Boolean::False,
131 lookup: Boolean::False,
132 runtime_tables: Boolean::False,
133 }
134 }
135}
136
137impl<F: FieldWitness> ToFieldElements<F> for FeatureFlags<bool> {
138 fn to_field_elements(&self, fields: &mut Vec<F>) {
139 let Self {
140 range_check0,
141 range_check1,
142 foreign_field_add,
143 foreign_field_mul,
144 xor,
145 rot,
146 lookup,
147 runtime_tables,
148 } = self;
149
150 [
151 range_check0,
152 range_check1,
153 foreign_field_add,
154 foreign_field_mul,
155 xor,
156 rot,
157 lookup,
158 runtime_tables,
159 ]
160 .to_field_elements(fields);
161 }
162}
163
164impl FeatureFlags<bool> {
165 pub fn empty_bool() -> Self {
166 Self {
167 range_check0: false,
168 range_check1: false,
169 foreign_field_add: false,
170 foreign_field_mul: false,
171 xor: false,
172 rot: false,
173 lookup: false,
174 runtime_tables: false,
175 }
176 }
177
178 pub fn to_boolean(&self) -> FeatureFlags<Boolean> {
179 use super::field::ToBoolean;
180
181 let Self {
182 range_check0,
183 range_check1,
184 foreign_field_add,
185 foreign_field_mul,
186 xor,
187 rot,
188 lookup,
189 runtime_tables,
190 } = self;
191
192 FeatureFlags {
193 range_check0: range_check0.to_boolean(),
194 range_check1: range_check1.to_boolean(),
195 foreign_field_add: foreign_field_add.to_boolean(),
196 foreign_field_mul: foreign_field_mul.to_boolean(),
197 xor: xor.to_boolean(),
198 rot: rot.to_boolean(),
199 lookup: lookup.to_boolean(),
200 runtime_tables: runtime_tables.to_boolean(),
201 }
202 }
203}
204
205#[derive(Debug)]
206pub struct Basic {
207 pub proof_verifieds: Vec<u64>,
208 pub wrap_domain: Domains,
210 pub step_domains: Box<[Domains]>,
211 pub feature_flags: FeatureFlags<OptFlag>,
212}
213
214#[derive(Debug)]
215pub enum ForStepKind<T, T2 = ()> {
216 Known(T),
217 SideLoaded(T2),
218}
219
220#[derive(Debug)]
221pub struct ForStep {
222 pub branches: usize,
223 pub max_proofs_verified: usize,
224 pub proof_verifieds: ForStepKind<Vec<Fp>>,
225 pub public_input: (), pub wrap_key: CircuitPlonkVerificationKeyEvals<Fp>,
227 pub wrap_domain: ForStepKind<Domain, Box<[Boolean]>>,
228 pub step_domains: ForStepKind<Box<[Domains]>>,
229 pub feature_flags: FeatureFlags<OptFlag>,
230 pub num_chunks: u64,
231 pub zk_rows: u64,
232}
233
234pub enum Packed {
235 Field(CircuitVar<Fq>),
236 PackedBits(CircuitVar<Fq>, usize),
237}
238
239impl std::fmt::Debug for Packed {
240 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
241 match self {
242 Self::Field(x) => f.write_fmt(format_args!("Field({:?})", x)),
243 Self::PackedBits(a, b) => f.write_fmt(format_args!("PackedBits({:?}, {:?})", a, b)),
244 }
245 }
246}
247
248pub struct StatementDeferredValues {
249 pub plonk: PlonkMinimal<Fp, 2>,
250 pub bulletproof_challenges: [[u64; 2]; 16],
251 pub branch_data: v2::CompositionTypesBranchDataStableV1,
252}
253
254pub struct StatementProofState {
255 pub deferred_values: StatementDeferredValues,
256 pub sponge_digest_before_evaluations: [u64; 4],
257 pub messages_for_next_wrap_proof: MessagesForNextWrapProof,
258}
259
260impl TryFrom<&v2::PicklesProofProofsVerified2ReprStableV2StatementProofState>
261 for StatementProofState
262{
263 type Error = InvalidBigInt;
264
265 fn try_from(
266 value: &v2::PicklesProofProofsVerified2ReprStableV2StatementProofState,
267 ) -> Result<Self, Self::Error> {
268 let v2::PicklesProofProofsVerified2ReprStableV2StatementProofState {
269 deferred_values:
270 v2::PicklesProofProofsVerified2ReprStableV2StatementProofStateDeferredValues {
271 plonk,
272 bulletproof_challenges,
273 branch_data,
274 },
275 sponge_digest_before_evaluations,
276 messages_for_next_wrap_proof:
277 v2::PicklesProofProofsVerified2ReprStableV2MessagesForNextWrapProof {
278 challenge_polynomial_commitment: (c0, c1),
279 old_bulletproof_challenges,
280 },
281 } = value;
282
283 Ok(Self {
284 deferred_values: StatementDeferredValues {
285 plonk: plonk.try_into()?,
286 bulletproof_challenges: bulletproof_challenges
287 .each_ref()
288 .map(|challenge| challenge.prechallenge.inner.each_ref().map(|v| v.as_u64())),
289 branch_data: branch_data.clone(),
290 },
291 sponge_digest_before_evaluations: sponge_digest_before_evaluations
292 .each_ref()
293 .map(|v| v.as_u64()),
294 messages_for_next_wrap_proof: MessagesForNextWrapProof {
295 challenge_polynomial_commitment: InnerCurve::from((
296 c0.to_field::<Fq>()?,
297 c1.to_field()?,
298 )),
299 old_bulletproof_challenges: old_bulletproof_challenges
300 .iter()
301 .map(|old_bulletproof_challenge| {
302 old_bulletproof_challenge.each_ref().map(|chal| {
303 two_u64_to_field(
304 &chal.prechallenge.inner.each_ref().map(|v| v.as_u64()),
305 )
306 })
307 })
308 .collect(),
309 },
310 })
311 }
312}
313
314pub mod step_verifier {
315 use std::ops::Neg;
316
317 use super::*;
318 use crate::proofs::{
319 field::{field, ToBoolean},
320 opt_sponge::OptSponge,
321 public_input::plonk_checks::{self, ft_eval0_checked},
322 transaction::{poseidon::Sponge, scalar_challenge},
323 unfinalized,
324 util::{
325 challenge_polynomial_checked, proof_evaluation_to_list_opt, to_absorption_sequence_opt,
326 },
327 wrap::{
328 make_scalars_env_checked, one_hot_vector, ones_vector,
329 pcs_batch::PcsBatch,
330 pseudo::{self, PseudoDomain},
331 wrap_verifier::{
332 actual_evaluation, chunks_needed, lowest_128_bits, split_commitments::Point,
333 Advice, OPS_BITS_PER_CHUNK,
334 },
335 MakeScalarsEnvParams, PERMUTS_MINUS_1_ADD_N1,
336 },
337 };
338 use itertools::Itertools;
339 use kimchi::circuits::wires::PERMUTS;
340 use poly_commitment::{srs::SRS, PolyComm};
341
342 fn squeeze_challenge(s: &mut Sponge<Fp>, w: &mut Witness<Fp>) -> Fp {
343 lowest_128_bits(s.squeeze(w), true, w)
344 }
345
346 fn squeeze_scalar(s: &mut Sponge<Fp>, w: &mut Witness<Fp>) -> Fp {
347 lowest_128_bits(s.squeeze(w), false, w)
348 }
349
350 fn absorb_curve(c: &Pallas, sponge: &mut Sponge<Fp>, w: &mut Witness<Fp>) {
351 let GroupAffine::<Fp> { x, y, .. } = c;
352 sponge.absorb2(&[*x, *y], w);
353 }
354
355 pub trait PlonkDomain<F: FieldWitness> {
356 fn vanishing_polynomial(&self, x: F, w: &mut Witness<F>) -> F;
357 fn generator(&self) -> F;
358 fn shifts(&self) -> &[F; PERMUTS];
359 fn log2_size(&self) -> u64;
360 }
361
362 impl<F: FieldWitness> PlonkDomain<F> for PseudoDomain<F> {
363 fn vanishing_polynomial(&self, x: F, w: &mut Witness<F>) -> F {
364 self.vanishing_polynomial(x, w)
365 }
366 fn generator(&self) -> F {
367 self.domain.group_gen
368 }
369 fn shifts(&self) -> &[F; PERMUTS] {
370 &self.shifts
371 }
372 fn log2_size(&self) -> u64 {
373 todo!()
374 }
375 }
376
377 impl<F: FieldWitness> PlonkDomain<F> for SideloadedDomain<F> {
378 fn vanishing_polynomial(&self, x: F, w: &mut Witness<F>) -> F {
379 (self.vanishing_polynomial)(x, w)
380 }
381 fn generator(&self) -> F {
382 self.generator
383 }
384 fn shifts(&self) -> &[F; PERMUTS] {
385 &self.shifts
386 }
387 fn log2_size(&self) -> u64 {
388 self.log2_size
389 }
390 }
391
392 struct SideloadedDomain<F: FieldWitness> {
393 generator: F,
394 shifts: Box<[F; PERMUTS]>,
395 vanishing_polynomial: Box<dyn Fn(F, &mut Witness<F>) -> F>,
396 log2_size: u64,
397 }
398
399 fn domain_for_compiled(
400 domains: &[Domains],
401 branch_data: &v2::CompositionTypesBranchDataStableV1,
402 w: &mut Witness<Fp>,
403 ) -> PseudoDomain<Fp> {
404 let unique_domains = domains
405 .iter()
406 .map(|d| d.h)
407 .sorted()
408 .dedup()
409 .collect::<Vec<_>>();
410 let mut which_log2 = unique_domains
411 .iter()
412 .rev()
413 .map(|Domain::Pow2RootsOfUnity(d)| {
414 let d = Fp::from(*d);
415 let domain_log2 = Fp::from(branch_data.domain_log2.as_u8() as u64);
416 field::equal(d, domain_log2, w)
417 })
418 .collect::<Vec<_>>();
419
420 which_log2.reverse();
421
422 pseudo::to_domain::<Fp>(&which_log2, &unique_domains)
423 }
424
425 fn tick_shifts(log2_size: u64) -> Box<[Fp; PERMUTS]> {
426 use kimchi::circuits::polynomials::permutation::Shifts;
428
429 let num_coeff = 1 << log2_size;
430 let domain = Radix2EvaluationDomain::<Fp>::new(num_coeff).unwrap();
431 let shifts = Shifts::new(&domain);
432 Box::from(*shifts.shifts())
433 }
434
435 fn domain_generator(log2_size: u64) -> Fp {
436 let num_coeff = 1 << log2_size;
438 let domain = Radix2EvaluationDomain::<Fp>::new(num_coeff).unwrap();
439 domain.group_gen
440 }
441
442 fn side_loaded_domain(log2_size: u64, w: &mut Witness<Fp>) -> SideloadedDomain<Fp> {
443 let log2_size_field = Fp::from(log2_size);
444
445 let vanishing_polynomial = |mask: Vec<Boolean>| {
446 Box::new(move |x: Fp, w: &mut Witness<Fp>| {
447 let result = mask.iter().rev().fold(x, |acc, should_square| {
448 let squared = field::square(acc, w);
449 w.exists_no_check(match should_square {
450 Boolean::True => squared,
451 Boolean::False => acc,
452 })
453 });
454 result - Fp::one()
455 })
456 };
457
458 let mut domain = |max: u64| {
459 let max_n = max;
460 let mask = ones_vector(log2_size_field, max_n, w);
461
462 let s_max_n = max_n + 1;
463 let log2_sizes = (
464 one_hot_vector::of_index(log2_size_field, s_max_n, w),
465 (0..max_n).collect::<Vec<_>>(),
466 );
467 let shifts = pseudo::shifts(&log2_sizes, tick_shifts);
468 let generator = pseudo::generator(&log2_sizes, domain_generator);
469 let vanishing_polynomial = vanishing_polynomial(mask);
470
471 SideloadedDomain {
472 generator,
473 shifts,
474 vanishing_polynomial,
475 log2_size,
476 }
477 };
478
479 domain(Domains::max().h.log2_size())
480 }
481
482 pub(super) fn proof_verified_to_prefix(
483 p: &v2::PicklesBaseProofsVerifiedStableV1,
484 ) -> [Boolean; 2] {
485 use v2::PicklesBaseProofsVerifiedStableV1::*;
486
487 match p {
488 N0 => [Boolean::False, Boolean::False],
489 N1 => [Boolean::False, Boolean::True],
490 N2 => [Boolean::True, Boolean::True],
491 }
492 }
493
494 fn validate_feature_flags(hack_feature_flags: OptFlag, w: &mut Witness<Fp>) {
496 let no = CircuitVar::Var(Boolean::False);
497
498 let range_check0 = no;
499 let range_check1 = no;
500 let rot = no;
501 let xor = no;
502 let foreign_field_mul = no;
503 let lookup = no;
504
505 if let OptFlag::Maybe = hack_feature_flags {
506 let range_check_lookup = {
507 let first = range_check0.or(&range_check1, w);
508 first.or(&rot, w)
509 };
510 let lookups_per_row_4 = {
511 let first = xor.or(&range_check_lookup, w);
512 first.or(&foreign_field_mul, w)
513 };
514 let _lookups_per_row_3 = lookups_per_row_4.or(&lookup, w);
515 };
516 }
517
518 pub(super) struct FinalizeOtherProofParams<'a> {
519 pub(super) max_proof_verified: usize,
520 pub(super) feature_flags: &'a FeatureFlags<OptFlag>,
521 pub(super) step_domains: &'a ForStepKind<Box<[Domains]>>,
522 pub(super) sponge: Sponge<Fp>,
523 pub(super) prev_challenges: &'a [[Fp; Fp::NROUNDS]],
524 pub(super) deferred_values: &'a DeferredValues<Fp>,
525 pub(super) evals: &'a AllEvals<Fp>,
526 pub(super) hack_feature_flags: OptFlag,
527 pub(super) zk_rows: u64,
528 }
529
530 pub(super) fn finalize_other_proof(
531 params: FinalizeOtherProofParams,
532 w: &mut Witness<Fp>,
533 ) -> anyhow::Result<(Boolean, Vec<Fp>)> {
534 let FinalizeOtherProofParams {
535 max_proof_verified,
536 feature_flags: _,
537 step_domains,
538 mut sponge,
539 prev_challenges,
540 deferred_values,
541 evals,
542 hack_feature_flags,
543 zk_rows,
544 } = params;
545
546 let DeferredValues {
547 plonk,
548 combined_inner_product,
549 b,
550 xi,
551 bulletproof_challenges,
552 branch_data,
553 } = deferred_values;
554
555 validate_feature_flags(hack_feature_flags, w);
556
557 let AllEvals { ft_eval1, evals } = evals;
558
559 let actual_width_mask = &branch_data.proofs_verified;
560 let actual_width_mask = proof_verified_to_prefix(actual_width_mask);
561
562 let (_, endo) = endos::<Fq>();
563 let scalar = |b: &[u64; 2], w: &mut Witness<Fp>| -> Fp {
564 let scalar = two_u64_to_field(b);
565 to_field_checked::<Fp, 128>(scalar, endo, w)
566 };
567
568 let plonk = {
569 let Plonk {
570 alpha,
571 beta,
572 gamma,
573 zeta,
574 zeta_to_srs_length,
575 zeta_to_domain_size,
576 perm,
577 feature_flags,
578 lookup: _,
579 } = plonk;
580
581 let lookup = match hack_feature_flags {
584 OptFlag::No => None,
585 OptFlag::Maybe => {
586 Some(scalar(&[0, 0], w))
590 }
591 OptFlag::Yes => todo!(),
592 };
593 let zeta = scalar(zeta, w);
594 let alpha = scalar(alpha, w);
595
596 InCircuit {
597 alpha,
598 beta: two_u64_to_field(beta),
599 gamma: two_u64_to_field(gamma),
600 zeta,
601 zeta_to_domain_size: zeta_to_domain_size.clone(),
602 zeta_to_srs_length: zeta_to_srs_length.clone(),
603 perm: perm.clone(),
604 lookup,
605 feature_flags: feature_flags.clone(),
606 }
607 };
608
609 let domain: Rc<dyn PlonkDomain<Fp>> = match step_domains {
610 ForStepKind::Known(ds) => Rc::new(domain_for_compiled(ds, branch_data, w)),
611 ForStepKind::SideLoaded(()) => Rc::new(side_loaded_domain(
612 branch_data.domain_log2.as_u8() as u64,
613 w,
614 )),
615 };
616
617 let zetaw = field::mul(domain.generator(), plonk.zeta, w);
618
619 let sg_olds = prev_challenges
620 .iter()
621 .map(|chals| challenge_polynomial_checked(chals))
622 .collect::<Vec<_>>();
623
624 let (sg_evals1, sg_evals2) = {
625 let sg_evals = |pt: Fp, w: &mut Witness<Fp>| {
626 let ntrim_front = 2 - max_proof_verified;
627
628 let mut sg = sg_olds
629 .iter()
630 .zip(&actual_width_mask[ntrim_front..])
631 .rev()
632 .map(|(f, keep)| (*keep, f(pt, w)))
633 .collect::<Vec<_>>();
634 sg.reverse();
635 sg
636 };
637
638 let sg_evals2 = sg_evals(zetaw, w);
640 let sg_evals1 = sg_evals(plonk.zeta, w);
641 (sg_evals1, sg_evals2)
642 };
643
644 {
646 let challenge_digest = {
647 let ntrim_front = 2 - max_proof_verified;
648
649 let mut sponge = OptSponge::create();
650 prev_challenges
651 .iter()
652 .zip(&actual_width_mask[ntrim_front..])
653 .for_each(|(chals, keep)| {
654 let keep = CircuitVar::Var(*keep);
655 for chal in chals {
656 sponge.absorb((keep, *chal));
657 }
658 });
659 sponge.squeeze(w)
660 };
661
662 sponge.absorb2(&[challenge_digest], w);
663 sponge.absorb(&[*ft_eval1], w);
664 sponge.absorb(&evals.public_input.0, w);
665 sponge.absorb(&evals.public_input.1, w);
666
667 for eval in &to_absorption_sequence_opt(&evals.evals, hack_feature_flags) {
668 match eval {
669 Opt::No => {}
670 Opt::Some(PointEvaluations { zeta, zeta_omega }) => {
671 sponge.absorb(zeta, w);
672 sponge.absorb(zeta_omega, w);
673 }
674 Opt::Maybe(b, PointEvaluations { zeta, zeta_omega }) => {
675 let sponge_state_before = sponge.sponge_state.clone();
676 let state_before = sponge.state;
677
678 sponge.absorb(zeta, w);
679 sponge.absorb(zeta_omega, w);
680
681 use ::poseidon::SpongeState::{Absorbed, Squeezed};
683 match (sponge_state_before, &sponge.sponge_state) {
684 (Absorbed(x), Absorbed(y)) => assert_eq!(x, *y),
685 (Squeezed(x), Squeezed(y)) => assert_eq!(x, *y),
686 (Absorbed(_), Squeezed(_)) => panic!(),
687 (Squeezed(_), Absorbed(_)) => panic!(),
688 }
689
690 sponge
691 .state
692 .iter_mut()
693 .zip(state_before)
694 .for_each(|(then, else_)| {
695 *then = w.exists_no_check(match b {
696 Boolean::True => *then,
697 Boolean::False => else_,
698 })
699 });
700 }
701 }
702 }
703 };
704
705 let xi_actual = lowest_128_bits(sponge.squeeze(w), true, w);
706 let r_actual = lowest_128_bits(sponge.squeeze(w), true, w);
707
708 let xi_correct = field::equal(xi_actual, two_u64_to_field(xi), w);
709
710 let xi = scalar(xi, w);
711 let r = to_field_checked::<Fp, 128>(r_actual, endo, w);
712
713 let to_bytes = |f: Fp| {
714 let bigint: BigInteger256 = f.into();
715 bigint.to_64x4()
716 };
717
718 let plonk_mininal = PlonkMinimal::<Fp, 4> {
719 alpha: plonk.alpha,
720 beta: plonk.beta,
721 gamma: plonk.gamma,
722 zeta: plonk.zeta,
723 joint_combiner: None,
724 alpha_bytes: to_bytes(plonk.alpha),
725 beta_bytes: to_bytes(plonk.beta),
726 gamma_bytes: to_bytes(plonk.gamma),
727 zeta_bytes: to_bytes(plonk.zeta),
728 joint_combiner_bytes: None,
729 feature_flags: FeatureFlags::empty_bool(), };
731
732 let combined_evals = {
733 let mut pow2pow =
734 |f: Fp| (0..COMMON_MAX_DEGREE_STEP_LOG2).fold(f, |acc, _| field::square(acc, w));
735
736 let zeta_n = pow2pow(plonk.zeta);
737 let zetaw_n = pow2pow(zetaw);
738
739 evals
740 .evals
741 .map_ref(&|PointEvaluations { zeta, zeta_omega }| {
742 let zeta = actual_evaluation(zeta, zeta_n);
743 let zeta_omega = actual_evaluation(zeta_omega, zetaw_n);
744 PointEvaluations { zeta, zeta_omega }
745 })
746 };
747
748 let srs_length_log2 = COMMON_MAX_DEGREE_STEP_LOG2;
749 let env = make_scalars_env_checked(
750 MakeScalarsEnvParams {
751 minimal: &plonk_mininal,
752 domain,
753 srs_length_log2,
754 hack_feature_flags,
755 zk_rows,
756 },
757 w,
758 );
759 let combined_inner_product_correct = {
760 let p_eval0 = &evals.public_input.0;
761
762 let ft_eval0 = ft_eval0_checked(
763 &env,
764 &combined_evals,
765 &plonk_mininal,
766 plonk.lookup,
767 p_eval0,
768 w,
769 );
770 let a = proof_evaluation_to_list_opt(&evals.evals, hack_feature_flags)
771 .into_iter()
772 .filter_map(|v| match v {
773 Opt::No => None,
774 Opt::Some(PointEvaluations { zeta, zeta_omega }) => Some([
775 zeta.into_iter().map(Opt::Some).collect::<Vec<_>>(),
776 zeta_omega.into_iter().map(Opt::Some).collect::<Vec<_>>(),
777 ]),
778 Opt::Maybe(boolean, PointEvaluations { zeta, zeta_omega }) => Some([
779 zeta.into_iter()
780 .map(|a| Opt::Maybe(boolean, a))
781 .collect::<Vec<_>>(),
782 zeta_omega
783 .into_iter()
784 .map(|a| Opt::Maybe(boolean, a))
785 .collect::<Vec<_>>(),
786 ]),
787 })
788 .collect::<Vec<_>>();
789
790 let actual_combined_inner_product = {
791 enum WhichEval {
792 First,
793 Second,
794 }
795
796 let combine = |which_eval: WhichEval,
797 sg_evals: &[(Boolean, Fp)],
798 ft_eval: Fp,
799 x_hat: &[Fp],
800 w: &mut Witness<Fp>| {
801 let f = |[a, b]: &[Vec<Opt<Fp>>; 2]| match which_eval {
802 WhichEval::First => a.clone(),
803 WhichEval::Second => b.clone(),
804 };
805 let v = sg_evals
806 .iter()
807 .copied()
808 .map(|(b, v)| Opt::Maybe(b, v))
809 .chain(x_hat.iter().copied().map(Opt::Some).collect::<Vec<_>>())
810 .chain([Opt::Some(ft_eval)])
811 .chain(a.iter().flat_map(f))
812 .rev()
813 .collect::<Vec<_>>();
814 let (init, rest) = v.split_at(1);
815
816 let init = match init[0] {
817 Opt::Some(x) => x,
818 Opt::No => Fp::zero(),
819 Opt::Maybe(b, x) => field::mul(b.to_field(), x, w),
820 };
821 rest.iter().fold(init, |acc: Fp, fx: &Opt<Fp>| match fx {
822 Opt::No => acc,
823 Opt::Some(fx) => *fx + field::mul(xi, acc, w),
824 Opt::Maybe(b, fx) => {
825 let on_true = *fx + field::mul(xi, acc, w);
826 w.exists_no_check(match b {
827 Boolean::True => on_true,
828 Boolean::False => acc,
829 })
830 }
831 })
832 };
833
834 let b = combine(
836 WhichEval::Second,
837 &sg_evals2,
838 *ft_eval1,
839 &evals.public_input.1,
840 w,
841 );
842 let b = field::mul(b, r, w);
843 let a = combine(
844 WhichEval::First,
845 &sg_evals1,
846 ft_eval0,
847 &evals.public_input.0,
848 w,
849 );
850 a + b
851 };
852
853 let combined_inner_product =
854 ShiftingValue::<Fp>::shifted_to_field(combined_inner_product);
855 field::equal(combined_inner_product, actual_combined_inner_product, w)
856 };
857
858 let mut bulletproof_challenges = bulletproof_challenges
859 .iter()
860 .rev()
861 .map(|f| to_field_checked::<Fp, 128>(*f, endo, w))
862 .collect::<Vec<_>>();
863 bulletproof_challenges.reverse();
864
865 let b_correct = {
866 let challenge_poly = challenge_polynomial_checked(&bulletproof_challenges);
867
868 let r_zetaw = field::mul(r, challenge_poly(zetaw, w), w);
870 let b_actual = challenge_poly(plonk.zeta, w) + r_zetaw;
871
872 field::equal(b.shifted_to_field(), b_actual, w)
873 };
874
875 let plonk = wrap_verifier::PlonkWithField {
876 alpha: plonk.alpha,
877 beta: plonk.beta,
878 gamma: plonk.gamma,
879 zeta: plonk.zeta,
880 zeta_to_srs_length: plonk.zeta_to_srs_length,
881 zeta_to_domain_size: plonk.zeta_to_domain_size,
882 perm: plonk.perm,
883 lookup: (),
884 };
885 let plonk_checks_passed = plonk_checks::checked(&env, &combined_evals, &plonk, w);
886
887 let finalized = Boolean::all(
888 &[
889 xi_correct,
890 b_correct,
891 combined_inner_product_correct,
892 plonk_checks_passed,
893 ],
894 w,
895 );
896
897 Ok((finalized, bulletproof_challenges))
898 }
899
900 pub(super) fn sponge_after_index(
901 index: &PlonkVerificationKeyEvals<Fp>,
902 w: &mut Witness<Fp>,
903 ) -> Sponge<Fp> {
904 let mut sponge = Sponge::<Fp>::new();
905 let fields = index.to_field_elements_owned();
906 sponge.absorb2(&fields, w);
907 sponge
908 }
909
910 pub(super) fn hash_messages_for_next_step_proof_opt(
911 msg: ReducedMessagesForNextStepProof,
912 sponge: Sponge<Fp>,
913 _widths: &ForStepKind<Vec<Fp>>,
914 _max_width: usize,
915 proofs_verified_mask: &[Boolean],
916 w: &mut Witness<Fp>,
917 ) -> Fp {
918 enum MaybeOpt<T, T2> {
919 Opt(Boolean, T),
920 NotOpt(T2),
921 }
922
923 let ReducedMessagesForNextStepProof {
924 app_state,
925 challenge_polynomial_commitments,
926 old_bulletproof_challenges,
927 } = msg;
928
929 let old_bulletproof_challenges = proofs_verified_mask
930 .iter()
931 .zip(old_bulletproof_challenges)
932 .map(|(b, v)| {
933 let b = *b;
934 v.map(|v| MaybeOpt::Opt(b, v))
935 });
936
937 let challenge_polynomial_commitments = proofs_verified_mask
938 .iter()
939 .zip(challenge_polynomial_commitments)
940 .map(|(b, v)| {
941 let b = *b;
942 let GroupAffine::<Fp> { x, y, .. } = v.to_affine();
943 [MaybeOpt::Opt(b, x), MaybeOpt::Opt(b, y)]
944 });
945
946 let app_state = app_state
947 .to_field_elements_owned()
948 .into_iter()
949 .map(MaybeOpt::NotOpt);
950
951 let both = challenge_polynomial_commitments
952 .zip(old_bulletproof_challenges)
953 .flat_map(|(c, o)| c.into_iter().chain(o));
954
955 let sponge = Box::new(sponge);
956 let res = app_state
957 .chain(both)
958 .fold(MaybeOpt::NotOpt(sponge), |acc, v| match (acc, v) {
959 (MaybeOpt::NotOpt(mut sponge), MaybeOpt::NotOpt(v)) => {
960 sponge.absorb(&[v], w);
961 MaybeOpt::NotOpt(sponge)
962 }
963 (MaybeOpt::NotOpt(sponge), MaybeOpt::Opt(b, v)) => {
964 let mut sponge = Box::new(OptSponge::of_sponge(*sponge, w));
965 sponge.absorb((CircuitVar::Var(b), v));
966 MaybeOpt::Opt(Boolean::True, sponge)
967 }
968 (MaybeOpt::Opt(_, mut sponge), MaybeOpt::Opt(b, v)) => {
969 sponge.absorb((CircuitVar::Var(b), v));
970 MaybeOpt::Opt(Boolean::True, sponge)
971 }
972 (MaybeOpt::Opt(_, _), MaybeOpt::NotOpt(_)) => panic!(),
973 });
974
975 match res {
976 MaybeOpt::NotOpt(mut sponge) => sponge.squeeze(w),
977 MaybeOpt::Opt(_, mut sponge) => sponge.squeeze(w),
978 }
979 }
980
981 fn scale_fast2<F: FieldWitness>(
983 g: CircuitVar<GroupAffine<F>>,
984 (s_div_2, s_odd): (F, Boolean),
985 num_bits: usize,
986 w: &mut Witness<F>,
987 ) -> GroupAffine<F> {
988 use crate::proofs::transaction::plonk_curve_ops::scale_fast_unpack;
989 use wrap_verifier::*;
990
991 let s_div_2_bits = num_bits - 1;
992 let chunks_needed = chunks_needed(s_div_2_bits);
993 let actual_bits_used = chunks_needed * OPS_BITS_PER_CHUNK;
994
995 let g_value = *g.value();
996 let shifted = F::Shifting::of_raw(s_div_2);
997 let h = match actual_bits_used {
998 255 => scale_fast_unpack::<F, F, 255>(g_value, shifted, w).0,
999 130 => scale_fast_unpack::<F, F, 130>(g_value, shifted, w).0,
1000 10 => scale_fast_unpack::<F, F, 10>(g_value, shifted, w).0,
1001 n => todo!("{:?} param_num_bits={:?}", n, num_bits),
1002 };
1003
1004 let on_false = {
1005 let g_neg = g.value().neg();
1006 if let CircuitVar::Var(_) = g {
1007 w.exists(g_neg.y);
1008 } else {
1009 }
1011 w.add_fast(h, g_neg)
1012 };
1013
1014 w.exists_no_check(match s_odd {
1015 Boolean::True => h,
1016 Boolean::False => on_false,
1017 })
1018 }
1019
1020 fn scale_fast22<F: FieldWitness>(
1022 g: CircuitVar<GroupAffine<F>>,
1023 (s_div_2, s_odd): (F, Boolean),
1024 num_bits: usize,
1025 w: &mut Witness<F>,
1026 ) -> GroupAffine<F> {
1027 use crate::proofs::transaction::plonk_curve_ops::scale_fast_unpack;
1028 use wrap_verifier::*;
1029
1030 let s_div_2_bits = num_bits - 1;
1031 let chunks_needed = chunks_needed(s_div_2_bits);
1032 let actual_bits_used = chunks_needed * OPS_BITS_PER_CHUNK;
1033
1034 let g_value = *g.value();
1035 let shifted = F::Shifting::of_raw(s_div_2);
1036 let h = match actual_bits_used {
1037 255 => scale_fast_unpack::<F, F, 255>(g_value, shifted, w).0,
1038 130 => scale_fast_unpack::<F, F, 130>(g_value, shifted, w).0,
1039 10 => scale_fast_unpack::<F, F, 10>(g_value, shifted, w).0,
1040 n => todo!("{:?} param_num_bits={:?}", n, num_bits),
1041 };
1042
1043 let on_false = {
1044 let g_neg = w.exists_no_check(g.value().neg());
1045 w.add_fast(h, g_neg)
1046 };
1047
1048 w.exists_no_check(match s_odd {
1049 Boolean::True => h,
1050 Boolean::False => on_false,
1051 })
1052 }
1053
1054 pub(super) fn scale_fast2_prime<F: FieldWitness, F2: FieldWitness>(
1056 g: CircuitVar<GroupAffine<F>>,
1057 s: F2,
1058 num_bits: usize,
1059 w: &mut Witness<F>,
1060 ) -> GroupAffine<F> {
1061 let s_parts = w.exists({
1062 let bigint: BigInteger256 = s.into();
1064 let bigint = bigint.to_64x4();
1065 let s_odd = bigint[0] & 1 != 0;
1066 let v = if s_odd { s - F2::one() } else { s };
1067 let v: BigInteger256 = (v / F2::from(2u64)).into();
1069 (F::try_from(v).unwrap(), s_odd.to_boolean()) });
1071
1072 scale_fast2(g, s_parts, num_bits, w)
1073 }
1074
1075 pub(super) fn ft_comm<F: FieldWitness, Scale>(
1077 plonk: &Plonk<F::Scalar>,
1078 t_comm: &PolyComm<GroupAffine<F>>,
1079 verification_key: &CircuitPlonkVerificationKeyEvals<F>,
1080 scale: Scale,
1081 w: &mut Witness<F>,
1082 ) -> GroupAffine<F>
1083 where
1084 Scale: Fn(
1085 CircuitVar<GroupAffine<F>>,
1086 <F::Scalar as FieldWitness>::Shifting,
1087 &mut Witness<F>,
1088 ) -> GroupAffine<F>,
1089 {
1090 let m = verification_key;
1091 let [sigma_comm_last] = &m.sigma[PERMUTS_MINUS_1_ADD_N1..] else {
1092 panic!()
1093 };
1094
1095 let f_comm = [scale(*sigma_comm_last, plonk.perm.clone(), w)]
1097 .into_iter()
1098 .rev()
1099 .reduce(|acc, v| w.add_fast(acc, v))
1100 .unwrap();
1101
1102 let chunked_t_comm = t_comm
1103 .elems
1104 .iter()
1105 .rev()
1106 .copied()
1107 .reduce(|acc, v| {
1108 let scaled = scale(CircuitVar::Var(acc), plonk.zeta_to_srs_length.clone(), w);
1109 w.add_fast(v, scaled)
1110 })
1111 .unwrap();
1112
1113 let scaled = scale(
1115 CircuitVar::Var(chunked_t_comm),
1116 plonk.zeta_to_domain_size.clone(),
1117 w,
1118 )
1119 .neg();
1120 let v = w.add_fast(f_comm, chunked_t_comm);
1121
1122 w.exists_no_check(scaled.y);
1124
1125 w.add_fast(v, scaled)
1126 }
1127
1128 fn public_input_commitment_dynamic(
1129 which: &[Boolean],
1130 srs: &mut poly_commitment::srs::SRS<Pallas>,
1131 domains: Vec<Domains>,
1132 public_input: Vec<Packed>,
1133 w: &mut Witness<Fp>,
1134 ) -> GroupAffine<Fp> {
1135 let lagrange_commitment =
1136 |d: &Domains, i: usize, srs: &mut poly_commitment::srs::SRS<Pallas>| {
1137 let d = 2u64.pow(d.h.log2_size() as u32);
1138 let elems = wrap_verifier::lagrange_commitment::<Fp>(srs, d, i).elems;
1139 assert_eq!(elems.len(), 1);
1140 InnerCurve::<Fp>::of_affine(elems[0])
1141 };
1142
1143 fn select_curve_points(
1144 domains: &[Domains],
1145 which: &[Boolean],
1146 srs: &mut poly_commitment::srs::SRS<Pallas>,
1147 w: &mut Witness<Fp>,
1148 points_for_domain: impl Fn(
1149 &Domains,
1150 &mut poly_commitment::srs::SRS<Pallas>,
1151 ) -> Vec<InnerCurve<Fp>>,
1152 ) -> Vec<InnerCurve<Fp>> {
1153 let (d, ds) = domains.split_first().unwrap();
1154 if ds.iter().all(|d2| d2.h == d.h) {
1155 points_for_domain(d, srs)
1156 } else {
1157 let index = which.iter().position(|b| b.as_bool()).unwrap();
1158 let domain = &domains[index];
1159 let points = points_for_domain(domain, srs);
1160 for p in points.iter().rev() {
1161 let GroupAffine::<Fp> { x, y, .. } = p.to_affine();
1162 w.exists_no_check([y, x]);
1163 }
1164 points
1165 }
1166 }
1167
1168 let lagrange =
1169 |i: usize, srs: &mut poly_commitment::srs::SRS<Pallas>, w: &mut Witness<Fp>| {
1170 let vec = select_curve_points(&domains, which, srs, w, |d, srs| {
1171 vec![lagrange_commitment(d, i, srs)]
1172 });
1173 vec[0].clone()
1174 };
1175
1176 let pow2pow = |x: InnerCurve<Fp>, n: usize| (0..n).fold(x, |acc, _| acc.clone() + acc);
1177
1178 let lagrange_with_correction = |input_length: usize,
1179 i: usize,
1180 srs: &mut poly_commitment::srs::SRS<Pallas>,
1181 w: &mut Witness<Fp>|
1182 -> Vec<InnerCurve<Fp>> {
1183 let actual_shift = OPS_BITS_PER_CHUNK * chunks_needed(input_length);
1184
1185 select_curve_points(&domains, which, srs, w, |d, srs| {
1186 let g = lagrange_commitment(d, i, srs);
1187 let powed = pow2pow(g.clone(), actual_shift);
1188 let powed = powed.to_affine().neg();
1189 vec![g, InnerCurve::of_affine(powed)]
1190 })
1191 };
1192
1193 let x_hat = {
1194 let (constant_part, non_constant_part): (Vec<_>, Vec<_>) = public_input
1195 .into_iter()
1196 .enumerate()
1197 .partition_map(|(i, t)| {
1198 use itertools::Either::{Left, Right};
1199 use CircuitVar::Constant;
1200 use Packed::{Field, PackedBits};
1201
1202 match t {
1203 Field(Constant(c)) | PackedBits(Constant(c), _) => Left(if c.is_zero() {
1204 None
1205 } else if c.is_one() {
1206 Some(lagrange(i, srs, w))
1207 } else {
1208 todo!()
1209 }),
1210 Field(x) => Right((i, (x, 255))),
1211 PackedBits(x, n) => Right((i, (x, n))),
1212 }
1213 });
1214
1215 #[derive(Debug)]
1216 enum CondOrAdd {
1217 CondAdd(CircuitVar<Boolean>, InnerCurve<Fp>),
1218 AddWithCorrection((CircuitVar<Fq>, usize), Vec<InnerCurve<Fp>>),
1219 }
1220
1221 let terms = non_constant_part
1222 .into_iter()
1223 .map(|(i, x)| match x {
1224 (b, 1) => CondOrAdd::CondAdd(CircuitVar::of_cvar(b), lagrange(i, srs, w)),
1225 (x, n) => {
1226 CondOrAdd::AddWithCorrection((x, n), lagrange_with_correction(n, i, srs, w))
1227 }
1228 })
1229 .collect::<Vec<_>>();
1230
1231 let correction = terms
1232 .iter()
1233 .filter_map(|term| match term {
1234 CondOrAdd::CondAdd(_, _) => None,
1235 CondOrAdd::AddWithCorrection(_, v) => {
1236 let [_, corr] = v.as_slice() else { panic!() };
1237 Some(corr.to_affine())
1238 }
1239 })
1240 .reduce(|a, b| w.add_fast(a, b))
1241 .unwrap();
1242
1243 let init =
1244 constant_part
1245 .iter()
1246 .filter_map(|term| term.as_ref())
1247 .fold(correction, |acc, v| {
1248 let v = v.to_affine();
1249 w.add_fast(acc, v)
1250 });
1251
1252 let result = terms.iter().fold(init, |acc, term| match term {
1253 CondOrAdd::CondAdd(b, g) => {
1254 let on_true = w.add_fast(g.to_affine(), acc);
1255 w.exists_no_check(match b.value() {
1256 Boolean::True => on_true,
1257 Boolean::False => acc,
1258 })
1259 }
1260 CondOrAdd::AddWithCorrection((x, num_bits), slice) => {
1261 let g = &slice[0];
1262 let g = CircuitVar::Var(g.to_affine());
1263 let acc2 = scale_fast2_prime(g, *x.value(), *num_bits, w);
1264 w.add_fast(acc, acc2)
1265 }
1266 });
1267 result.neg()
1268 };
1269
1270 x_hat
1271 }
1272
1273 fn multiscale_known(ts: &[(&Packed, InnerCurve<Fp>)], w: &mut Witness<Fp>) -> GroupAffine<Fp> {
1274 let pow2pow = |x: InnerCurve<Fp>, n: usize| (0..n).fold(x, |acc, _| acc.clone() + acc);
1275
1276 let (constant_part, non_constant_part): (Vec<_>, Vec<_>) =
1277 ts.iter().partition_map(|(t, g)| {
1278 use itertools::Either::{Left, Right};
1279 use CircuitVar::Constant;
1280 use Packed::{Field, PackedBits};
1281
1282 match t {
1283 Field(Constant(c)) | PackedBits(Constant(c), _) => Left(if c.is_zero() {
1284 None
1285 } else if c.is_one() {
1286 Some(g)
1287 } else {
1288 todo!()
1289 }),
1290 Field(x) => Right((Field(*x), g)),
1291 PackedBits(x, n) => Right((PackedBits(*x, *n), g)),
1292 }
1293 });
1294
1295 let add_opt = |xo: Option<InnerCurve<Fp>>, y: &InnerCurve<Fp>| match xo {
1296 Some(x) => x + y.clone(),
1297 None => y.clone(),
1298 };
1299
1300 let constant_part = constant_part
1301 .iter()
1302 .filter_map(|c| c.as_ref())
1303 .fold(None, |acc, x| Some(add_opt(acc, x)));
1304
1305 let (correction, acc) = {
1306 non_constant_part
1307 .iter()
1308 .map(|(s, x)| {
1309 let (rr, n) = match s {
1310 Packed::PackedBits(s, n) => {
1311 let x = CircuitVar::Constant(x.to_affine());
1312 let c = scale_fast2_prime(x, s.as_field(), *n, w);
1313 (c, *n)
1314 }
1315 Packed::Field(s) => {
1316 let x = CircuitVar::Constant(x.to_affine());
1317 let c = scale_fast2_prime(x, s.as_field(), 255, w);
1318 (c, 255)
1319 }
1320 };
1321
1322 let n = wrap_verifier::OPS_BITS_PER_CHUNK * wrap_verifier::chunks_needed(n - 1);
1323 let cc = pow2pow((*x).clone(), n);
1324 (cc, rr)
1325 })
1326 .collect::<Vec<_>>() .into_iter()
1328 .reduce(|(a1, b1), (a2, b2)| ((a1 + a2), w.add_fast(b1, b2)))
1329 .unwrap()
1330 };
1331
1332 let correction = InnerCurve::of_affine(correction.to_affine().neg());
1333 w.add_fast(acc, add_opt(constant_part, &correction).to_affine())
1334 }
1335
1336 fn lagrange_commitment<F: FieldWitness>(
1337 srs: &mut SRS<GroupAffine<F>>,
1338 domain: &Domain,
1339 i: usize,
1340 ) -> InnerCurve<F> {
1341 let d = domain.size();
1342 let elems = wrap_verifier::lagrange_commitment::<F>(srs, d, i).elems;
1343
1344 assert_eq!(elems.len(), 1);
1345 InnerCurve::of_affine(elems[0])
1346 }
1347
1348 fn to_high_low(f: Fq) -> (Fp, Boolean) {
1349 fn of_bits<F: FieldWitness>(bs: &[bool; 254]) -> F {
1350 bs.iter().rev().fold(F::zero(), |acc, b| {
1351 let acc = acc + acc;
1352 if *b {
1353 acc + F::one()
1354 } else {
1355 acc
1356 }
1357 })
1358 }
1359 let to_high_low = |fq: Fq| {
1360 let [low, high @ ..] = crate::proofs::transaction::field_to_bits::<Fq, 255>(fq);
1361 (of_bits::<Fp>(&high), low.to_boolean())
1362 };
1363 to_high_low(f)
1364 }
1365
1366 fn scale_for_ft_comm(
1367 g: CircuitVar<GroupAffine<Fp>>,
1368 f: <Fq as FieldWitness>::Shifting,
1369 w: &mut Witness<Fp>,
1370 ) -> GroupAffine<Fp> {
1371 let scalar = to_high_low(f.shifted_raw());
1372 scale_fast2(g, scalar, 255, w)
1373 }
1374
1375 struct CheckBulletProofParams<'a> {
1376 pcs_batch: PcsBatch,
1377 sponge: Sponge<Fp>,
1378 xi: [u64; 2],
1379 advice: &'a Advice<Fp>,
1380 openings_proof: &'a OpeningProof<GroupAffine<Fp>>,
1381 srs: &'a SRS<GroupAffine<Fp>>,
1382 polynomials: (Vec<CircuitVar<GroupAffine<Fp>>>, Vec<()>),
1383 }
1384
1385 fn check_bulletproof(
1386 params: CheckBulletProofParams,
1387 w: &mut Witness<Fp>,
1388 ) -> anyhow::Result<(Boolean, Vec<Fp>)> {
1389 let CheckBulletProofParams {
1390 pcs_batch: _,
1391 mut sponge,
1392 xi,
1393 advice,
1394 openings_proof:
1395 OpeningProof {
1396 lr,
1397 delta,
1398 z1,
1399 z2,
1400 sg,
1401 },
1402 srs,
1403 polynomials,
1404 } = params;
1405
1406 let (without_degree_bound, _with_degree_bound) = polynomials;
1407
1408 let (high, low) = to_high_low(advice.combined_inner_product.shifted_raw());
1409 sponge.absorb2(&[high, low.to_field()], w);
1410
1411 let u = {
1412 let t = sponge.squeeze(w);
1413 wrap_verifier::group_map(t, w)
1414 };
1415
1416 let xi_field: Fq = two_u64_to_field(&xi);
1417
1418 let point: Point<Fp> = PcsBatch::combine_split_commitments::<Fp, _, _, _, _>(
1419 |p, _w| p.clone(),
1420 |acc, _xi, p, w| match acc {
1421 Point::MaybeFinite(acc_is_finite, acc) => match p {
1422 Point::MaybeFinite(p_is_finite, p) => {
1423 let is_finite = p_is_finite.or(&acc_is_finite, w);
1424 let xi_acc = scalar_challenge::endo_cvar::<Fp, _, 128>(acc, xi_field, w);
1425
1426 let on_true = CircuitVar::Var(w.add_fast(*p.value(), xi_acc));
1427
1428 let v = match acc_is_finite.as_boolean() {
1429 Boolean::True => on_true,
1430 Boolean::False => *p,
1431 };
1432 if let CircuitVar::Var(_) = acc_is_finite {
1433 w.exists_no_check(v.value());
1434 };
1435 Point::<Fp>::MaybeFinite(is_finite, v)
1436 }
1437 Point::Finite(p) => {
1438 let xi_acc = scalar_challenge::endo_cvar::<Fp, _, 128>(acc, xi_field, w);
1439 let on_true = CircuitVar::Var(w.add_fast(*p.value(), xi_acc));
1440
1441 let v = match acc_is_finite.as_boolean() {
1442 Boolean::True => on_true,
1443 Boolean::False => *p,
1444 };
1445 if let CircuitVar::Var(_) = acc_is_finite {
1446 w.exists_no_check(v.value());
1447 };
1448 Point::<Fp>::Finite(v)
1449 }
1450 },
1451 Point::Finite(acc) => {
1452 let xi_acc = scalar_challenge::endo_cvar::<Fp, _, 128>(acc, xi_field, w);
1453
1454 let v = match p {
1455 Point::Finite(p) => CircuitVar::Var(w.add_fast(*p.value(), xi_acc)),
1456 Point::MaybeFinite(p_is_finite, p) => {
1457 let p = *p;
1458 let on_true = CircuitVar::Var(w.add_fast(*p.value(), xi_acc));
1459
1460 let v = match p_is_finite.as_boolean() {
1461 Boolean::True => on_true,
1462 Boolean::False => CircuitVar::Var(xi_acc),
1463 };
1464 if let CircuitVar::Var(_) = p_is_finite {
1465 w.exists_no_check(v.value());
1466 };
1467 v
1468 }
1469 };
1470
1471 Point::Finite(v)
1472 }
1473 },
1474 xi,
1475 &without_degree_bound
1476 .into_iter()
1477 .map(Point::Finite)
1478 .collect::<Vec<_>>(),
1479 &[],
1480 w,
1481 );
1482
1483 let Point::Finite(combined_polynomial) = point else {
1484 panic!("invalid state");
1485 };
1486 let combined_polynomial = *combined_polynomial.value();
1487
1488 let (lr_prod, challenges) = wrap_verifier::bullet_reduce(&mut sponge, lr, w);
1489
1490 let p_prime = {
1491 w.exists_no_check(&u); let combined_inner_product = to_high_low(advice.combined_inner_product.shifted_raw());
1493 let uc = scale_fast22(CircuitVar::Var(u), combined_inner_product, 255, w);
1494 w.add_fast(combined_polynomial, uc)
1495 };
1496
1497 let q = w.add_fast(p_prime, lr_prod);
1498 absorb_curve(delta, &mut sponge, w);
1499 let c = squeeze_scalar(&mut sponge, w);
1500
1501 let lhs = {
1502 let cq = scalar_challenge::endo::<Fp, Fp, 128>(q, c, w);
1503 w.add_fast(cq, *delta)
1504 };
1505
1506 let rhs = {
1507 let b_u = {
1508 w.exists_no_check(&u); let b = to_high_low(advice.b.shifted_raw());
1510 scale_fast22(CircuitVar::Var(u), b, 255, w)
1511 };
1512
1513 let z_1_g_plus_b_u = {
1514 use plonk_checks::ShiftedValue;
1515
1516 let z1 = to_high_low(ShiftedValue::<Fq>::of_field(*z1).shifted);
1517 scale_fast2(CircuitVar::Var(w.add_fast(*sg, b_u)), z1, 255, w)
1518 };
1519
1520 let z2_h = {
1521 use plonk_checks::ShiftedValue;
1522
1523 let z2 = to_high_low(ShiftedValue::<Fq>::of_field(*z2).shifted);
1524 scale_fast2(CircuitVar::Constant(srs.h), z2, 255, w)
1525 };
1526
1527 w.add_fast(z_1_g_plus_b_u, z2_h)
1528 };
1529
1530 Ok((wrap_verifier::equal_g(lhs, rhs, w), challenges))
1531 }
1532
1533 struct IncrementallyVerifyProofParams<'a> {
1534 pub proofs_verified: usize,
1535 pub srs: &'a mut poly_commitment::srs::SRS<Pallas>,
1536 pub wrap_domain: &'a ForStepKind<Domain, Box<[Boolean]>>,
1537 pub sponge: Sponge<Fp>,
1538 pub sponge_after_index: Sponge<Fp>,
1539 pub wrap_verification_key: &'a CircuitPlonkVerificationKeyEvals<Fp>,
1540 pub xi: [u64; 2],
1541 pub public_input: Vec<Packed>,
1542 pub sg_old: &'a Vec<GroupAffine<Fp>>,
1543 pub advice: &'a Advice<Fp>,
1544 pub proof: &'a ProverProof<Fq>,
1545 pub plonk: &'a Plonk<Fq>,
1546 }
1547
1548 fn incrementally_verify_proof(
1549 params: IncrementallyVerifyProofParams,
1550 w: &mut Witness<Fp>,
1551 ) -> anyhow::Result<(Fp, (Boolean, Vec<Fp>))> {
1552 let IncrementallyVerifyProofParams {
1553 proofs_verified: _,
1554 srs,
1555 wrap_domain,
1556 mut sponge,
1557 sponge_after_index,
1558 wrap_verification_key,
1559 xi,
1560 public_input,
1561 sg_old,
1562 advice,
1563 proof,
1564 plonk,
1565 } = params;
1566
1567 let ProverProof::<Fq> {
1568 commitments: messages,
1569 proof: openings_proof,
1570 ..
1571 } = proof;
1575
1576 let sample = squeeze_challenge;
1577 let sample_scalar = squeeze_scalar;
1578
1579 let index_digest = {
1580 let mut index_sponge = sponge_after_index.clone();
1581 index_sponge.squeeze(w)
1582 };
1583
1584 sponge.absorb2(&[index_digest], w);
1585
1586 assert_eq!(sg_old.len(), 2);
1588 for v in sg_old {
1589 absorb_curve(v, &mut sponge, w);
1590 }
1591
1592 let x_hat = match wrap_domain {
1593 ForStepKind::Known(domain) => {
1594 let ts = public_input
1595 .iter()
1596 .enumerate()
1597 .map(|(i, x)| (x, lagrange_commitment::<Fp>(srs, domain, i)))
1598 .collect::<Vec<_>>();
1599 multiscale_known(&ts, w).neg()
1600 }
1601 ForStepKind::SideLoaded(which) => {
1602 let domains = [0, 1, 2].into_iter().map(wrap_domains).collect();
1603 public_input_commitment_dynamic(which, srs, domains, public_input, w)
1604 }
1605 };
1606
1607 let x_hat = {
1608 w.exists(x_hat.y); w.add_fast(x_hat, srs.h)
1610 };
1611
1612 absorb_curve(&x_hat, &mut sponge, w);
1613
1614 let w_comm = &messages.w_comm;
1615 for g in w_comm.iter().flat_map(|w| &w.elems) {
1616 absorb_curve(g, &mut sponge, w);
1617 }
1618
1619 let _beta = sample(&mut sponge, w);
1620 let _gamma = sample(&mut sponge, w);
1621
1622 let z_comm = &messages.z_comm;
1623 for z in z_comm.elems.iter() {
1624 absorb_curve(z, &mut sponge, w);
1625 }
1626
1627 let _alpha = sample_scalar(&mut sponge, w);
1628
1629 let t_comm = &messages.t_comm;
1630 for t in t_comm.elems.iter() {
1631 absorb_curve(t, &mut sponge, w);
1632 }
1633
1634 let _zeta = sample_scalar(&mut sponge, w);
1635
1636 let sponge_before_evaluations = sponge.clone();
1637 let sponge_digest_before_evaluations = sponge.squeeze(w);
1638
1639 let sigma_comm_init = &wrap_verification_key.sigma[..PERMUTS_MINUS_1_ADD_N1];
1640
1641 let ft_comm = ft_comm(plonk, t_comm, wrap_verification_key, scale_for_ft_comm, w);
1642
1643 let bulletproof_challenges = {
1644 const WRAP_HACK_PADDED_LENGTH: usize = 2;
1646 const NUM_COMMITMENTS_WITHOUT_DEGREE_BOUND: usize = 45;
1647
1648 let cvar = CircuitVar::Var;
1649
1650 let without_degree_bound = {
1651 let sg_old = sg_old.iter().copied().map(cvar);
1652 let rest = [cvar(x_hat), cvar(ft_comm)]
1653 .into_iter()
1654 .chain(z_comm.elems.iter().cloned().map(cvar))
1655 .chain([
1656 wrap_verification_key.generic,
1657 wrap_verification_key.psm,
1658 wrap_verification_key.complete_add,
1659 wrap_verification_key.mul,
1660 wrap_verification_key.emul,
1661 wrap_verification_key.endomul_scalar,
1662 ])
1663 .chain(
1664 w_comm
1665 .iter()
1666 .flat_map(|w| w.elems.iter().cloned().map(cvar)),
1667 )
1668 .chain(wrap_verification_key.coefficients)
1669 .chain(sigma_comm_init.iter().cloned());
1670 sg_old.chain(rest).collect::<Vec<_>>()
1671 };
1672
1673 check_bulletproof(
1674 CheckBulletProofParams {
1675 pcs_batch: PcsBatch::create(
1676 WRAP_HACK_PADDED_LENGTH + NUM_COMMITMENTS_WITHOUT_DEGREE_BOUND,
1677 ),
1678 sponge: sponge_before_evaluations,
1679 xi,
1680 advice,
1681 openings_proof,
1682 srs,
1683 polynomials: (without_degree_bound, vec![]),
1684 },
1685 w,
1686 )?
1687 };
1688
1689 Ok((sponge_digest_before_evaluations, bulletproof_challenges))
1690 }
1691
1692 pub(super) struct VerifyParams<'a> {
1693 pub(super) srs: &'a mut poly_commitment::srs::SRS<Pallas>,
1694 pub(super) feature_flags: &'a FeatureFlags<OptFlag>,
1695 pub(super) lookup_parameters: (),
1696 pub(super) proofs_verified: usize,
1697 pub(super) wrap_domain: &'a ForStepKind<Domain, Box<[Boolean]>>,
1698 pub(super) is_base_case: CircuitVar<Boolean>,
1699 pub(super) sponge_after_index: Sponge<Fp>,
1700 pub(super) sg_old: &'a Vec<GroupAffine<Fp>>,
1701 pub(super) proof: &'a ProverProof<Fq>,
1702 pub(super) wrap_verification_key: &'a CircuitPlonkVerificationKeyEvals<Fp>,
1703 pub(super) statement: &'a PreparedStatement,
1704 pub(super) hack_feature_flags: OptFlag,
1705 pub(super) unfinalized: &'a Unfinalized,
1706 }
1707
1708 pub(super) fn verify(params: VerifyParams, w: &mut Witness<Fp>) -> anyhow::Result<Boolean> {
1709 let VerifyParams {
1710 srs,
1711 feature_flags: _,
1712 lookup_parameters: _,
1713 proofs_verified,
1714 wrap_domain,
1715 is_base_case,
1716 sponge_after_index,
1717 sg_old,
1718 proof,
1719 wrap_verification_key,
1720 statement,
1721 hack_feature_flags,
1722 unfinalized,
1723 } = params;
1724
1725 let public_input = {
1726 let npublic_input = match hack_feature_flags {
1727 OptFlag::No => 39,
1728 OptFlag::Maybe => 40,
1729 OptFlag::Yes => todo!(),
1730 };
1731 statement.to_public_input_cvar(hack_feature_flags, npublic_input)?
1732 };
1733
1734 let unfinalized::DeferredValues {
1735 plonk,
1736 combined_inner_product,
1737 b,
1738 xi,
1739 bulletproof_challenges: _,
1740 } = &unfinalized.deferred_values;
1741
1742 let b = b.clone();
1743 let combined_inner_product = combined_inner_product.clone();
1744 let sponge = Sponge::new();
1745
1746 let (
1747 _sponge_digest_before_evaluations_actual,
1748 (bulletproof_success, bulletproof_challenges_actual),
1749 ) = incrementally_verify_proof(
1750 IncrementallyVerifyProofParams {
1751 proofs_verified,
1752 srs,
1753 wrap_domain,
1754 sponge,
1755 sponge_after_index,
1756 wrap_verification_key,
1757 xi: *xi,
1758 public_input,
1759 sg_old,
1760 advice: &Advice {
1761 b,
1762 combined_inner_product,
1763 },
1764 proof,
1765 plonk,
1766 },
1767 w,
1768 )?;
1769
1770 for (c1, c2) in unfinalized
1771 .deferred_values
1772 .bulletproof_challenges
1773 .iter()
1774 .zip(&bulletproof_challenges_actual)
1775 {
1776 let v = match is_base_case.value() {
1777 Boolean::True => two_u64_to_field(c1),
1778 Boolean::False => *c2,
1779 };
1780 if let CircuitVar::Var(_) = is_base_case {
1781 w.exists_no_check(v);
1782 };
1783 }
1784
1785 Ok(bulletproof_success)
1786 }
1787}
1788
1789struct VerifyOneParams<'a> {
1790 srs: &'a mut poly_commitment::srs::SRS<Pallas>,
1791 proof: &'a PerProofWitness,
1792 data: &'a ForStep,
1793 messages_for_next_wrap_proof: Fp,
1794 unfinalized: &'a Unfinalized,
1795 should_verify: CircuitVar<Boolean>,
1796}
1797
1798fn verify_one(params: VerifyOneParams, w: &mut Witness<Fp>) -> anyhow::Result<(Vec<Fp>, Boolean)> {
1799 let VerifyOneParams {
1800 srs,
1801 proof,
1802 data,
1803 messages_for_next_wrap_proof,
1804 unfinalized,
1805 should_verify,
1806 } = params;
1807
1808 let PerProofWitness {
1809 app_state,
1810 wrap_proof,
1811 proof_state,
1812 prev_proof_evals,
1813 prev_challenges,
1814 prev_challenge_polynomial_commitments,
1815 hack_feature_flags,
1816 } = proof;
1817
1818 let deferred_values = &proof_state.deferred_values;
1819
1820 let (finalized, chals) = {
1821 let sponge_digest = proof_state.sponge_digest_before_evaluations;
1822
1823 let sponge = {
1824 let mut sponge = crate::proofs::transaction::poseidon::Sponge::<Fp>::new();
1825 sponge.absorb2(&[four_u64_to_field(&sponge_digest)?], w);
1826 sponge
1827 };
1828
1829 step_verifier::finalize_other_proof(
1830 step_verifier::FinalizeOtherProofParams {
1831 max_proof_verified: data.max_proofs_verified,
1832 feature_flags: &data.feature_flags,
1833 step_domains: &data.step_domains,
1834 sponge,
1835 prev_challenges,
1836 deferred_values,
1837 evals: prev_proof_evals,
1838 hack_feature_flags: *hack_feature_flags,
1839 zk_rows: data.zk_rows,
1840 },
1841 w,
1842 )?
1843 };
1844
1845 let branch_data = &deferred_values.branch_data;
1846
1847 let sponge_after_index = step_verifier::sponge_after_index(&data.wrap_key.to_non_cvar(), w);
1848
1849 let statement = {
1850 let msg = ReducedMessagesForNextStepProof {
1851 app_state: app_state.clone().unwrap(),
1852 challenge_polynomial_commitments: prev_challenge_polynomial_commitments
1853 .iter()
1854 .map(|g| InnerCurve::of_affine(*g))
1855 .collect(),
1856 old_bulletproof_challenges: prev_challenges.clone(),
1857 };
1858
1859 let ntrim_front = 2 - prev_challenge_polynomial_commitments.len();
1860 let proofs_verified_mask = {
1861 let proofs_verified_mask = &branch_data.proofs_verified;
1862 step_verifier::proof_verified_to_prefix(proofs_verified_mask)
1863 };
1864 let proofs_verified_mask = &proofs_verified_mask[ntrim_front..];
1865
1866 let prev_messages_for_next_step_proof =
1867 step_verifier::hash_messages_for_next_step_proof_opt(
1868 msg,
1869 sponge_after_index.clone(),
1870 &data.proof_verifieds,
1871 data.max_proofs_verified,
1872 proofs_verified_mask,
1873 w,
1874 );
1875
1876 PreparedStatement {
1877 proof_state: ProofState {
1878 messages_for_next_wrap_proof: { to_bytes(messages_for_next_wrap_proof) },
1879 ..proof_state.clone()
1880 },
1881 messages_for_next_step_proof: { to_bytes(prev_messages_for_next_step_proof) },
1882 }
1883 };
1884
1885 let verified = step_verifier::verify(
1886 step_verifier::VerifyParams {
1887 srs,
1888 feature_flags: &data.feature_flags,
1889 lookup_parameters: (),
1890 proofs_verified: data.max_proofs_verified,
1891 wrap_domain: &data.wrap_domain,
1892 is_base_case: should_verify.neg(),
1893 sponge_after_index,
1894 sg_old: prev_challenge_polynomial_commitments,
1895 proof: wrap_proof,
1896 wrap_verification_key: &data.wrap_key,
1897 statement: &statement,
1898 hack_feature_flags: *hack_feature_flags,
1899 unfinalized,
1900 },
1901 w,
1902 )?;
1903
1904 let a = verified.and(&finalized, w);
1905 let b = CircuitVar::Var(a).or(&should_verify.neg(), w);
1906
1907 Ok((chals, b.as_boolean()))
1908}
1909
1910fn to_bytes(f: Fp) -> [u64; 4] {
1911 let bigint: BigInteger256 = f.into();
1912 bigint.to_64x4()
1913}
1914
1915fn to_4limbs(v: [u64; 2]) -> [u64; 4] {
1916 [v[0], v[1], 0, 0]
1917}
1918
1919pub struct ExpandDeferredParams<'a> {
1920 pub evals: &'a AllEvals<Fp>,
1921 pub old_bulletproof_challenges: &'a Vec<[Fp; 16]>,
1922 pub proof_state: &'a StatementProofState,
1923 pub zk_rows: u64,
1924}
1925
1926pub fn expand_deferred(params: ExpandDeferredParams) -> anyhow::Result<DeferredValues<Fp>> {
1927 let ExpandDeferredParams {
1928 evals,
1929 old_bulletproof_challenges,
1930 proof_state,
1931 zk_rows,
1932 } = params;
1933
1934 use super::public_input::scalar_challenge::ScalarChallenge;
1935
1936 let (_, endo) = endos::<Fq>();
1937
1938 let plonk0 = &proof_state.deferred_values.plonk;
1939
1940 let zeta = ScalarChallenge::limbs_to_field(&plonk0.zeta_bytes);
1941 let alpha = ScalarChallenge::limbs_to_field(&plonk0.alpha_bytes);
1942 let step_domain: u8 = proof_state.deferred_values.branch_data.domain_log2.as_u8();
1943
1944 let Some(num_coeffs) = 1u64.checked_shl(step_domain as u32) else {
1945 return Err(InvalidBigInt)?;
1946 };
1947
1948 let Some(domain) = Radix2EvaluationDomain::<Fp>::new(num_coeffs as usize) else {
1949 return Err(InvalidBigInt)?;
1950 };
1951
1952 let zetaw = zeta * domain.group_gen;
1953
1954 let plonk_minimal = PlonkMinimal::<Fp, 4> {
1955 alpha,
1956 beta: plonk0.beta,
1957 gamma: plonk0.gamma,
1958 zeta,
1959 joint_combiner: plonk0
1961 .joint_combiner_bytes
1962 .as_ref()
1963 .map(ScalarChallenge::limbs_to_field),
1964 alpha_bytes: to_bytes(alpha),
1965 beta_bytes: to_4limbs(plonk0.beta_bytes),
1966 gamma_bytes: to_4limbs(plonk0.gamma_bytes),
1967 zeta_bytes: to_bytes(zeta),
1968 joint_combiner_bytes: plonk0.joint_combiner_bytes.map(to_4limbs),
1969 feature_flags: plonk0.feature_flags.clone(),
1970 };
1971
1972 let combined_evals =
1973 evals_of_split_evals(zeta, zetaw, &evals.evals.evals, BACKEND_TICK_ROUNDS_N);
1974
1975 let srs_length_log2 = COMMON_MAX_DEGREE_STEP_LOG2;
1976 let env = make_scalars_env(&plonk_minimal, step_domain, srs_length_log2, zk_rows);
1977
1978 let plonk = {
1979 let InCircuit {
1980 alpha: _,
1981 beta: _,
1982 gamma: _,
1983 zeta: _,
1984 zeta_to_domain_size,
1985 zeta_to_srs_length,
1986 perm,
1987 lookup,
1988 feature_flags,
1989 } = derive_plonk(&env, &combined_evals, &plonk_minimal);
1990
1991 Plonk {
1992 alpha: plonk0.alpha_bytes,
1993 beta: plonk0.beta_bytes,
1994 gamma: plonk0.gamma_bytes,
1995 zeta: plonk0.zeta_bytes,
1996 zeta_to_srs_length,
1997 zeta_to_domain_size,
1998 perm,
1999 feature_flags,
2000 lookup: lookup.map(|_| plonk0.joint_combiner_bytes.unwrap()),
2001 }
2002 };
2003
2004 let xs = proof_evaluation_to_absorption_sequence(&evals.evals.evals);
2005 let (x1, x2) = &evals.evals.public_input;
2006
2007 let old_bulletproof_challenges: Vec<_> = old_bulletproof_challenges
2008 .iter()
2009 .map(ScalarChallenge::array_to_fields)
2010 .collect();
2011
2012 let challenges_digest = {
2013 let mut sponge = poseidon::Sponge::<Fp>::default();
2014 for old_bulletproof_challenges in &old_bulletproof_challenges {
2015 sponge.absorb(old_bulletproof_challenges);
2016 }
2017 sponge.squeeze()
2018 };
2019
2020 let mut sponge = poseidon::FqSponge::default();
2021 sponge.absorb_fq(&[four_u64_to_field(
2022 &proof_state.sponge_digest_before_evaluations,
2023 )?]);
2024 sponge.absorb_fq(&[challenges_digest]);
2025 sponge.absorb_fq(&[evals.ft_eval1]);
2026 sponge.absorb_fq(x1);
2027 sponge.absorb_fq(x2);
2028 xs.iter().for_each(|PointEvaluations { zeta, zeta_omega }| {
2029 sponge.absorb_fq(zeta);
2030 sponge.absorb_fq(zeta_omega);
2031 });
2032 let xi_chal: [u64; 2] = sponge.squeeze_limbs();
2033 let r_chal: [u64; 2] = sponge.squeeze_limbs();
2034
2035 let xi = ScalarChallenge::from(xi_chal).to_field(&endo);
2036 let r = ScalarChallenge::from(r_chal).to_field(&endo);
2037
2038 let public_input = &evals.evals.public_input;
2039
2040 let es = &evals.evals.evals;
2041 let tick_combined_evals = evals_of_split_evals(zeta, zetaw, es, super::BACKEND_TICK_ROUNDS_N);
2042 let public = PointEvaluations {
2043 zeta: public_input.0.clone(),
2044 zeta_omega: public_input.1.clone(),
2045 };
2046
2047 let combined_inner_product_actual =
2048 combined_inner_product(CombinedInnerProductParams::<_, { Fp::NROUNDS }, 4> {
2049 env: &env,
2050 evals: es,
2051 combined_evals: &tick_combined_evals,
2052 public: &public,
2053 minimal: &plonk_minimal,
2054 ft_eval1: evals.ft_eval1,
2055 r,
2056 old_bulletproof_challenges: &old_bulletproof_challenges,
2057 xi,
2058 zetaw,
2059 });
2060
2061 let bulletproof_challenges: Vec<_> = proof_state
2062 .deferred_values
2063 .bulletproof_challenges
2064 .iter()
2065 .map(ScalarChallenge::limbs_to_field)
2066 .collect();
2067
2068 let b_actual = {
2069 let challenge_polys = challenge_polynomial(&bulletproof_challenges);
2070 challenge_polys(zeta) + (r * challenge_polys(zetaw))
2071 };
2072
2073 let to_shifted = |f: Fp| <Fp as FieldWitness>::Shifting::of_field(f);
2074
2075 Ok(DeferredValues {
2076 plonk,
2077 combined_inner_product: to_shifted(combined_inner_product_actual),
2078 b: to_shifted(b_actual),
2079 xi: xi_chal,
2080 bulletproof_challenges,
2081 branch_data: proof_state.deferred_values.branch_data.clone(),
2082 })
2083}
2084
2085fn wrap_compute_sg(challenges: &[[u64; 2]]) -> GroupAffine<Fp> {
2087 use super::public_input::scalar_challenge::ScalarChallenge;
2088
2089 let challenges = challenges
2090 .iter()
2091 .map(ScalarChallenge::limbs_to_field)
2092 .collect::<Vec<_>>();
2093
2094 let coeffs = b_poly_coefficients(&challenges);
2095 let p = DensePolynomial::from_coefficients_vec(coeffs);
2096
2097 let comm = {
2098 use poly_commitment::SRS;
2099
2100 let srs = get_srs::<Fq>();
2101 srs.commit_non_hiding(&p, 1)
2102 };
2103 comm.elems[0]
2104}
2105
2106struct ExpandProofParams<'a> {
2107 dlog_vk: &'a VerifierIndex<Fq>,
2108 dlog_plonk_index: &'a CircuitPlonkVerificationKeyEvals<Fp>,
2109 app_state: &'a Rc<dyn ToFieldElementsDebug>,
2110 t: &'a v2::PicklesProofProofsVerified2ReprStableV2,
2111 public_input_length: usize,
2112 tag: (),
2113 must_verify: CircuitVar<Boolean>,
2114 hack_feature_flags: OptFlag,
2115 zk_rows: u64,
2116}
2117
2118fn expand_proof(params: ExpandProofParams) -> anyhow::Result<ExpandedProof> {
2119 let ExpandProofParams {
2120 dlog_vk,
2121 dlog_plonk_index,
2122 app_state,
2123 t,
2124 public_input_length,
2125 tag: _,
2126 must_verify,
2127 hack_feature_flags,
2128 zk_rows,
2129 } = params;
2130
2131 use super::public_input::scalar_challenge::ScalarChallenge;
2132
2133 let plonk0: PlonkMinimal<Fp> = (&t.statement.proof_state.deferred_values.plonk).try_into()?;
2134
2135 let plonk = {
2136 let domain: u8 = t
2137 .statement
2138 .proof_state
2139 .deferred_values
2140 .branch_data
2141 .domain_log2
2142 .as_u8();
2143
2144 let alpha = ScalarChallenge::limbs_to_field(&plonk0.alpha_bytes);
2145 let zeta = ScalarChallenge::limbs_to_field(&plonk0.zeta_bytes);
2146 let w: Fp = Radix2EvaluationDomain::new(1 << domain).unwrap().group_gen;
2147 let zetaw = zeta * w;
2148
2149 let es = prev_evals_from_p2p(&t.prev_evals.evals.evals)?;
2152 let combined_evals = evals_of_split_evals(zeta, zetaw, &es, BACKEND_TICK_ROUNDS_N);
2153
2154 let plonk_minimal = PlonkMinimal::<Fp, 4> {
2155 alpha,
2156 beta: plonk0.beta,
2157 gamma: plonk0.gamma,
2158 zeta,
2159 joint_combiner: plonk0.joint_combiner,
2160 alpha_bytes: to_bytes(alpha),
2162 beta_bytes: to_4limbs(plonk0.beta_bytes),
2163 gamma_bytes: to_4limbs(plonk0.gamma_bytes),
2164 zeta_bytes: to_bytes(zeta),
2165 joint_combiner_bytes: plonk0.joint_combiner_bytes.map(to_4limbs),
2166 feature_flags: plonk0.feature_flags.clone(),
2167 };
2168
2169 let srs_length_log2 = COMMON_MAX_DEGREE_STEP_LOG2;
2170 let env = make_scalars_env(&plonk_minimal, domain, srs_length_log2, zk_rows);
2171
2172 derive_plonk(&env, &combined_evals, &plonk_minimal)
2173 };
2174
2175 let statement = &t.statement;
2176
2177 let prev_challenges: Vec<[Fq; BACKEND_TOCK_ROUNDS_N]> = {
2178 let old_bulletproof_challenges = &statement
2179 .proof_state
2180 .messages_for_next_wrap_proof
2181 .old_bulletproof_challenges;
2182 extract_bulletproof(&[
2183 old_bulletproof_challenges.0[0].0.clone(),
2184 old_bulletproof_challenges.0[1].0.clone(),
2185 ])
2186 };
2187
2188 let old_bulletproof_challenges: Vec<[Fp; 16]> = statement
2189 .messages_for_next_step_proof
2190 .old_bulletproof_challenges
2191 .iter()
2192 .map(|v| {
2193 v.0.clone()
2194 .map(|v| two_u64_to_field(&v.prechallenge.inner.0.map(|v| v.as_u64())))
2195 })
2196 .collect();
2197
2198 let deferred_values_computed = {
2199 let evals: AllEvals<Fp> = (&t.prev_evals).try_into()?;
2200 let proof_state: StatementProofState = (&statement.proof_state).try_into()?;
2201
2202 expand_deferred(ExpandDeferredParams {
2203 evals: &evals,
2204 old_bulletproof_challenges: &old_bulletproof_challenges,
2205 proof_state: &proof_state,
2206 zk_rows,
2207 })?
2208 };
2209
2210 let old_bulletproof_challenges: Vec<_> = old_bulletproof_challenges
2211 .iter()
2212 .map(ScalarChallenge::array_to_fields)
2213 .collect();
2214
2215 let messages_for_next_step_proof = MessagesForNextStepProof {
2216 app_state: Rc::clone(app_state),
2217 dlog_plonk_index: &dlog_plonk_index.to_non_cvar(),
2218 challenge_polynomial_commitments: statement
2219 .messages_for_next_step_proof
2220 .challenge_polynomial_commitments
2221 .iter()
2222 .map(|(x, y)| {
2223 Ok(InnerCurve::of_affine(make_group(
2224 x.to_field::<Fp>()?,
2225 y.to_field()?,
2226 )))
2227 })
2228 .collect::<Result<_, InvalidBigInt>>()?,
2229 old_bulletproof_challenges: old_bulletproof_challenges.clone(),
2230 }
2231 .hash();
2232
2233 let deferred_values = deferred_values_computed;
2234 let prev_statement_with_hashes = PreparedStatement {
2235 proof_state: ProofState {
2236 deferred_values: DeferredValues {
2237 plonk: Plonk {
2238 alpha: plonk0.alpha_bytes,
2239 beta: plonk0.beta_bytes,
2240 gamma: plonk0.gamma_bytes,
2241 zeta: plonk0.zeta_bytes,
2242 zeta_to_srs_length: plonk.zeta_to_srs_length,
2243 zeta_to_domain_size: plonk.zeta_to_domain_size,
2244 perm: plonk.perm,
2245 lookup: match plonk.lookup {
2246 None => None,
2247 Some(_) => Some(plonk0.joint_combiner_bytes.unwrap()),
2248 },
2249 feature_flags: plonk.feature_flags,
2250 },
2251 combined_inner_product: deferred_values.combined_inner_product,
2252 b: deferred_values.b,
2253 xi: deferred_values.xi,
2254 bulletproof_challenges: statement
2255 .proof_state
2256 .deferred_values
2257 .bulletproof_challenges
2258 .iter()
2259 .map(|challenge| {
2260 two_u64_to_field(
2261 &challenge.prechallenge.inner.each_ref().map(|v| v.as_u64()),
2262 )
2263 })
2264 .collect(),
2265 branch_data: deferred_values.branch_data,
2266 },
2267 sponge_digest_before_evaluations: statement
2268 .proof_state
2269 .sponge_digest_before_evaluations
2270 .each_ref()
2271 .map(|v| v.as_u64()),
2272 messages_for_next_wrap_proof: MessagesForNextWrapProof {
2273 old_bulletproof_challenges: prev_challenges.clone(),
2274 challenge_polynomial_commitment: {
2275 let (x, y) = &statement
2276 .proof_state
2277 .messages_for_next_wrap_proof
2278 .challenge_polynomial_commitment;
2279 InnerCurve::from((x.to_field::<Fq>()?, y.to_field()?))
2280 },
2281 }
2282 .hash(),
2283 },
2284 messages_for_next_step_proof,
2285 };
2286
2287 let mut proof = make_padded_proof_from_p2p(t)?;
2288 let oracle = {
2289 let public_input = prev_statement_with_hashes.to_public_input(public_input_length)?;
2290 create_oracle_with_public_input(dlog_vk, &proof, &public_input)
2291 };
2292
2293 let x_hat = PointEvaluations {
2294 zeta: oracle.p_eval_1(),
2295 zeta_omega: oracle.p_eval_2(),
2296 };
2297
2298 let alpha = oracle.alpha();
2299 let beta = oracle.beta();
2300 let gamma = oracle.gamma();
2301 let zeta = oracle.zeta();
2302
2303 let to_bytes = |f: Fq| {
2304 let bigint: BigInteger256 = f.into();
2305 let [a, b, c, d] = bigint.to_64x4();
2306 assert_eq!([c, d], [0, 0]);
2307 [a, b]
2308 };
2309
2310 let plonk0 = PlonkMinimal {
2311 alpha,
2312 beta,
2313 gamma,
2314 zeta,
2315 joint_combiner: None,
2316 alpha_bytes: to_bytes(alpha),
2317 beta_bytes: to_bytes(beta),
2318 gamma_bytes: to_bytes(gamma),
2319 zeta_bytes: to_bytes(zeta),
2320 joint_combiner_bytes: None, feature_flags: FeatureFlags::empty_bool(),
2322 };
2323
2324 let xi = oracle.v();
2325 let r = oracle.u();
2326 let sponge_digest_before_evaluations = oracle.digest_before_evaluations;
2327
2328 let (_, endo) = endos::<Fp>();
2329 let to_field = |bytes: [u64; 2]| -> Fq { ScalarChallenge::from(bytes).to_field(&endo) };
2330
2331 let w = dlog_vk.domain.group_gen;
2332
2333 let zeta = to_field(plonk0.zeta_bytes);
2334 let zetaw = { zeta * w };
2335
2336 let (new_bulletproof_challenges, b) = {
2337 let chals = oracle
2338 .opening_prechallenges
2339 .iter()
2340 .map(|v| to_field(to_bytes(*v)))
2341 .collect::<Vec<_>>();
2342
2343 let r = to_field(to_bytes(r.0));
2344 let challenge_poly = challenge_polynomial(&chals);
2346 let b = challenge_poly(zeta) + (r * challenge_poly(zetaw));
2347
2348 let prechals = oracle
2349 .opening_prechallenges
2350 .iter()
2351 .copied()
2352 .map(to_bytes)
2353 .collect::<Vec<_>>();
2354
2355 (prechals, b)
2356 };
2357
2358 let challenge_polynomial_commitment = match must_verify.value() {
2359 Boolean::False => wrap_compute_sg(&new_bulletproof_challenges),
2360 Boolean::True => proof.proof.sg,
2361 };
2362
2363 let witness = PerProofWitness {
2364 app_state: None,
2365 proof_state: prev_statement_with_hashes.proof_state.clone(),
2366 prev_proof_evals: (&t.prev_evals).try_into()?,
2367 prev_challenge_polynomial_commitments: {
2368 let mut challenge_polynomial_commitments = t
2369 .statement
2370 .messages_for_next_step_proof
2371 .challenge_polynomial_commitments
2372 .iter()
2373 .map(|(x, y)| Ok(make_group::<Fp>(x.to_field()?, y.to_field()?)))
2374 .collect::<Result<Vec<_>, InvalidBigInt>>()?;
2375
2376 while challenge_polynomial_commitments.len() < 2 {
2377 challenge_polynomial_commitments.insert(0, dummy_ipa_wrap_sg());
2378 }
2379
2380 challenge_polynomial_commitments
2381 },
2382 prev_challenges: {
2383 let mut prev_challenges = old_bulletproof_challenges.clone();
2384 while prev_challenges.len() < 2 {
2385 prev_challenges.insert(0, dummy_ipa_step_challenges_computed())
2386 }
2387
2388 prev_challenges
2389 },
2390 wrap_proof: {
2391 proof.proof.sg = challenge_polynomial_commitment;
2392 proof.clone()
2393 },
2394 hack_feature_flags,
2395 };
2396
2397 let tock_combined_evals = {
2398 let zeta = to_field(plonk0.zeta_bytes);
2399 evals_of_split_evals(zeta, zetaw, &proof.evals, BACKEND_TOCK_ROUNDS_N)
2400 };
2401
2402 let tock_plonk_minimal = {
2403 let alpha = to_field(plonk0.alpha_bytes);
2404 let zeta = to_field(plonk0.zeta_bytes);
2405
2406 let to_bytes = |f: Fq| {
2407 let bigint: BigInteger256 = f.into();
2408 bigint.to_64x4()
2409 };
2410
2411 PlonkMinimal {
2412 alpha,
2413 beta,
2414 gamma,
2415 zeta,
2416 joint_combiner: None,
2417 alpha_bytes: to_bytes(alpha),
2418 beta_bytes: to_4limbs(plonk0.beta_bytes),
2419 gamma_bytes: to_4limbs(plonk0.gamma_bytes),
2420 zeta_bytes: to_bytes(alpha),
2421 joint_combiner_bytes: None, feature_flags: FeatureFlags::empty_bool(),
2423 }
2424 };
2425
2426 let domain_log2 = dlog_vk.domain.log_size_of_group;
2427 let srs_length_log2 = COMMON_MAX_DEGREE_WRAP_LOG2;
2428 let tock_env = make_scalars_env(
2429 &tock_plonk_minimal,
2430 domain_log2 as u8,
2431 srs_length_log2 as u64,
2432 zk_rows,
2433 );
2434
2435 let public = {
2436 let PointEvaluations { zeta, zeta_omega } = &x_hat;
2437 PointEvaluations {
2438 zeta: vec![*zeta],
2439 zeta_omega: vec![*zeta_omega],
2440 }
2441 };
2442
2443 let combined_inner_product = combined_inner_product(CombinedInnerProductParams {
2444 env: &tock_env,
2445 evals: &proof.evals,
2446 combined_evals: &tock_combined_evals,
2447 public: &public,
2448 minimal: &tock_plonk_minimal,
2449 ft_eval1: proof.ft_eval1,
2450 r: to_field(to_bytes(r.0)),
2451 old_bulletproof_challenges: &prev_challenges,
2452 xi: to_field(to_bytes(xi.0)),
2453 zetaw,
2454 });
2455
2456 let plonk = derive_plonk(&tock_env, &tock_combined_evals, &tock_plonk_minimal);
2457
2458 let shift = |f: Fq| <Fq as FieldWitness>::Shifting::of_field(f);
2459
2460 let unfinalized = Unfinalized {
2461 deferred_values: crate::proofs::unfinalized::DeferredValues {
2462 plonk: Plonk {
2463 alpha: to_bytes(plonk0.alpha),
2464 beta: to_bytes(plonk0.beta),
2465 gamma: to_bytes(plonk0.gamma),
2466 zeta: to_bytes(plonk0.zeta),
2467 zeta_to_srs_length: plonk.zeta_to_srs_length,
2468 zeta_to_domain_size: plonk.zeta_to_domain_size,
2469 perm: plonk.perm,
2470 lookup: None,
2471 feature_flags: plonk.feature_flags,
2472 },
2473 combined_inner_product: shift(combined_inner_product),
2474 b: shift(b),
2475 xi: to_bytes(xi.0),
2476 bulletproof_challenges: new_bulletproof_challenges,
2477 },
2478 should_finalize: must_verify.value().as_bool(),
2479 sponge_digest_before_evaluations: {
2480 let bigint: BigInteger256 = sponge_digest_before_evaluations.into();
2481 bigint.to_64x4()
2482 },
2483 };
2484
2485 Ok(ExpandedProof {
2486 sg: challenge_polynomial_commitment,
2487 unfinalized,
2488 prev_statement_with_hashes,
2489 x_hat,
2490 witness,
2491 actual_wrap_domain: dlog_vk.domain.log_size_of_group,
2492 })
2493}
2494
2495#[derive(Debug)]
2496struct ExpandedProof {
2497 sg: GroupAffine<Fp>,
2498 unfinalized: Unfinalized,
2499 prev_statement_with_hashes: PreparedStatement,
2500 x_hat: PointEvaluations<Fq>,
2501 witness: PerProofWitness,
2502 actual_wrap_domain: u32,
2503}
2504
2505#[derive(Clone, Debug)]
2506pub struct PerProofWitness {
2507 pub app_state: Option<Rc<dyn ToFieldElementsDebug>>,
2508 pub wrap_proof: ProverProof<Fq>,
2510 pub proof_state: ProofState,
2511 pub prev_proof_evals: AllEvals<Fp>,
2512 pub prev_challenges: Vec<[Fp; 16]>,
2513 pub prev_challenge_polynomial_commitments: Vec<GroupAffine<Fp>>,
2514 pub hack_feature_flags: OptFlag,
2518}
2519
2520impl PerProofWitness {
2521 pub fn with_app_state(self, app_state: Rc<dyn ToFieldElementsDebug>) -> PerProofWitness {
2522 let Self {
2523 app_state: old,
2524 wrap_proof,
2525 proof_state,
2526 prev_proof_evals,
2527 prev_challenges,
2528 prev_challenge_polynomial_commitments,
2529 hack_feature_flags,
2530 } = self;
2531 assert!(old.is_none());
2532
2533 PerProofWitness {
2534 app_state: Some(app_state),
2535 wrap_proof,
2536 proof_state,
2537 prev_proof_evals,
2538 prev_challenges,
2539 prev_challenge_polynomial_commitments,
2540 hack_feature_flags,
2541 }
2542 }
2543}
2544
2545impl Check<Fp> for PerProofWitness {
2546 fn check(&self, w: &mut Witness<Fp>) {
2547 let Self {
2548 app_state,
2549 wrap_proof,
2550 proof_state,
2551 prev_proof_evals: _,
2552 prev_challenges: _,
2553 prev_challenge_polynomial_commitments,
2554 hack_feature_flags: _,
2555 } = self;
2556
2557 assert!(app_state.is_none());
2558
2559 let ProverProof::<Fq> {
2560 commitments:
2561 ProverCommitments {
2562 w_comm,
2563 z_comm,
2564 t_comm,
2565 lookup: _,
2566 },
2567 proof:
2568 OpeningProof {
2569 lr,
2570 delta,
2571 z1,
2572 z2,
2573 sg,
2574 },
2575 evals: _,
2576 ft_eval1: _,
2577 prev_challenges: _,
2578 } = wrap_proof;
2579
2580 for poly in w_comm {
2581 poly.elems.check(w);
2582 }
2583 z_comm.elems.check(w);
2584 t_comm.elems.check(w);
2585 lr.check(w);
2586
2587 let shift = |f: Fq| <Fq as FieldWitness>::Shifting::of_field(f);
2588
2589 shift(*z1).check(w);
2590 shift(*z2).check(w);
2591
2592 delta.check(w);
2593 sg.check(w);
2594
2595 let ProofState {
2596 deferred_values:
2597 DeferredValues {
2598 plonk:
2599 Plonk {
2600 alpha: _,
2601 beta: _,
2602 gamma: _,
2603 zeta: _,
2604 zeta_to_srs_length,
2605 zeta_to_domain_size,
2606 perm,
2607 lookup: _,
2608 feature_flags: _,
2609 },
2610 combined_inner_product,
2611 b,
2612 xi,
2613 bulletproof_challenges,
2614 branch_data,
2615 },
2616 sponge_digest_before_evaluations: _,
2617 messages_for_next_wrap_proof: _,
2618 } = proof_state;
2619
2620 zeta_to_srs_length.check(w);
2621 zeta_to_domain_size.check(w);
2622 perm.check(w);
2623 combined_inner_product.check(w);
2624 b.check(w);
2625 two_u64_to_field::<Fp>(xi).check(w);
2626 bulletproof_challenges.check(w);
2627
2628 {
2629 let v2::CompositionTypesBranchDataStableV1 {
2630 proofs_verified: _,
2631 domain_log2,
2632 } = branch_data;
2633 let domain_log2: u64 = domain_log2.0.as_u8() as u64;
2634
2635 const NBITS: usize = 16;
2637 let (_, endo) = endos::<Fq>();
2638 to_field_checked::<Fp, NBITS>(Fp::from(domain_log2), endo, w);
2639 }
2640
2641 prev_challenge_polynomial_commitments.check(w);
2642 }
2643}
2644
2645pub fn extract_recursion_challenges<const N: usize>(
2646 proofs: &[&v2::PicklesProofProofsVerified2ReprStableV2; N],
2647) -> anyhow::Result<Vec<RecursionChallenge<GroupAffine<Fq>>>> {
2648 use poly_commitment::PolyComm;
2649
2650 let comms: [(Fq, Fq); N] =
2651 crate::try_array_into_with(proofs, |proof| -> Result<_, InvalidBigInt> {
2652 let (a, b) = &proof
2653 .statement
2654 .proof_state
2655 .messages_for_next_wrap_proof
2656 .challenge_polynomial_commitment;
2657 Ok((a.to_field::<Fq>()?, b.to_field::<Fq>()?))
2658 })?;
2659
2660 let challs = proofs
2661 .iter()
2662 .map(|p| {
2663 p.statement
2664 .proof_state
2665 .deferred_values
2666 .bulletproof_challenges
2667 .clone()
2668 })
2669 .collect::<Vec<_>>();
2670 let challs = extract_bulletproof(&challs);
2671
2672 Ok(challs
2673 .into_iter()
2674 .zip(comms)
2675 .map(|(chals, (x, y))| {
2676 let comm = PolyComm::<mina_curves::pasta::Vesta> {
2677 elems: vec![make_group(x, y)],
2678 };
2679 RecursionChallenge {
2680 chals: chals.to_vec(),
2681 comm,
2682 }
2683 })
2684 .collect())
2685}
2686
2687pub struct StepParams<'a, const N_PREVIOUS: usize> {
2692 pub app_state: Rc<dyn ToFieldElementsDebug>,
2693 pub rule: InductiveRule<'a, N_PREVIOUS>,
2694 pub for_step_datas: [&'a ForStep; N_PREVIOUS],
2695 pub indexes: [(
2696 &'a VerifierIndex<Fq>,
2697 &'a CircuitPlonkVerificationKeyEvals<Fp>,
2698 ); N_PREVIOUS],
2699 pub prev_challenge_polynomial_commitments: Vec<RecursionChallenge<GroupAffine<Fq>>>,
2700 pub hack_feature_flags: OptFlag,
2702 pub step_prover: &'a Prover<Fp>,
2703 pub wrap_prover: &'a Prover<Fq>,
2704 pub only_verify_constraints: bool,
2705}
2706
2707pub struct StepProof {
2708 pub statement: StepStatement,
2709 pub prev_evals: Vec<AllEvals<Fq>>,
2710 pub proof_with_public: ProofWithPublic<Fp>,
2711}
2712
2713pub fn step<C: ProofConstants, const N_PREVIOUS: usize>(
2714 params: StepParams<N_PREVIOUS>,
2715 w: &mut Witness<Fp>,
2716) -> anyhow::Result<StepProof> {
2717 let StepParams {
2718 app_state,
2719 rule,
2720 for_step_datas,
2721 indexes,
2722 prev_challenge_polynomial_commitments,
2723 hack_feature_flags,
2724 step_prover,
2725 wrap_prover,
2726 only_verify_constraints,
2727 } = params;
2728
2729 let dlog_plonk_index = w.exists(super::merge::dlog_plonk_index(wrap_prover));
2730
2731 let expanded_proofs: Box<[ExpandedProof; N_PREVIOUS]> = rule
2732 .previous_proof_statements
2733 .iter()
2734 .zip(indexes)
2735 .zip(for_step_datas)
2736 .map(|((statement, (verifier_index, dlog_plonk_index)), data)| {
2737 let PreviousProofStatement {
2738 public_input,
2739 proof,
2740 proof_must_verify,
2741 } = statement;
2742
2743 expand_proof(ExpandProofParams {
2744 dlog_vk: verifier_index,
2745 dlog_plonk_index,
2746 app_state: public_input,
2747 t: proof,
2748 public_input_length: 40,
2749 tag: (),
2750 must_verify: *proof_must_verify,
2751 hack_feature_flags,
2752 zk_rows: data.zk_rows,
2753 })
2754 })
2755 .collect::<Result<Vec<_>, _>>()
2756 .context("expand_proof")?
2757 .try_into()
2758 .unwrap();
2759
2760 let prevs: [&PerProofWitness; N_PREVIOUS] =
2761 w.exists(expanded_proofs.each_ref().map(|p| &p.witness));
2762 let unfinalized_proofs_unextended: [&Unfinalized; N_PREVIOUS] =
2763 w.exists(expanded_proofs.each_ref().map(|p| &p.unfinalized));
2764
2765 let messages_for_next_wrap_proof: [Fp; N_PREVIOUS] = {
2766 let f = four_u64_to_field::<Fp>;
2767
2768 crate::try_array_into_with(&expanded_proofs, |p| {
2769 f(&p.prev_statement_with_hashes
2770 .proof_state
2771 .messages_for_next_wrap_proof)
2772 })?
2773 };
2774
2775 let messages_for_next_wrap_proof_padded: [Fp; 2] = w.exists({
2776 let n_padding = 2 - expanded_proofs.len();
2777 std::array::from_fn(|i| {
2778 if i < n_padding {
2779 messages_for_next_wrap_proof_padding()
2780 } else {
2781 messages_for_next_wrap_proof[i - n_padding]
2782 }
2783 })
2784 });
2785
2786 let actual_wrap_domains: [usize; N_PREVIOUS] = {
2787 let all_possible_domains = wrap_verifier::all_possible_domains();
2788
2789 let actuals_wrap_domain: [u32; N_PREVIOUS] =
2790 expanded_proofs.each_ref().map(|p| p.actual_wrap_domain);
2791
2792 actuals_wrap_domain.map(|domain_size| {
2793 let domain_size = domain_size as u64;
2794 all_possible_domains
2795 .iter()
2796 .position(|Domain::Pow2RootsOfUnity(d)| *d == domain_size)
2797 .unwrap_or(0)
2798 })
2799 };
2800
2801 let prevs: [PerProofWitness; N_PREVIOUS] = rule
2802 .previous_proof_statements
2803 .iter()
2804 .zip(prevs)
2805 .map(|(stmt, proof)| proof.clone().with_app_state(stmt.public_input.clone()))
2806 .collect::<Vec<_>>()
2807 .try_into()
2808 .unwrap();
2809
2810 let srs = get_srs_mut::<Fq>();
2811 let mut srs = srs.lock().unwrap();
2812
2813 let bulletproof_challenges = prevs
2814 .iter()
2815 .zip(messages_for_next_wrap_proof)
2816 .zip(unfinalized_proofs_unextended)
2817 .zip(&rule.previous_proof_statements)
2818 .zip(actual_wrap_domains)
2819 .zip(for_step_datas)
2820 .map(
2821 |(
2822 ((((proof, msg_for_next_wrap_proof), unfinalized), stmt), actual_wrap_domain),
2823 data,
2824 )| {
2825 let PreviousProofStatement {
2826 proof_must_verify: should_verify,
2827 ..
2828 } = stmt;
2829
2830 match data.wrap_domain {
2831 ForStepKind::SideLoaded(_) => {} ForStepKind::Known(wrap_domain) => {
2833 let actual_wrap_domain = wrap_domains(actual_wrap_domain);
2834 assert_eq!(actual_wrap_domain.h, wrap_domain);
2835 }
2836 }
2837 let (chals, _verified) = verify_one(
2838 VerifyOneParams {
2839 srs: &mut srs,
2840 proof,
2841 data,
2842 messages_for_next_wrap_proof: msg_for_next_wrap_proof,
2843 unfinalized,
2844 should_verify: *should_verify,
2845 },
2846 w,
2847 )?;
2848 Ok(chals.try_into().unwrap()) },
2850 )
2851 .collect::<Result<Vec<[Fp; 16]>, anyhow::Error>>()
2852 .context("verify_one")?;
2853
2854 std::mem::drop(srs);
2855
2856 let messages_for_next_step_proof = {
2857 let msg = MessagesForNextStepProof {
2858 app_state: Rc::clone(&app_state),
2859 dlog_plonk_index: &dlog_plonk_index,
2860 challenge_polynomial_commitments: prevs
2861 .iter()
2862 .map(|v| InnerCurve::of_affine(v.wrap_proof.proof.sg))
2863 .collect(),
2864 old_bulletproof_challenges: bulletproof_challenges,
2865 };
2866 crate::proofs::transaction::checked_hash2(&msg.to_fields(), w)
2867 };
2868
2869 let unfinalized_proofs = {
2870 let mut unfinalized_proofs: Vec<_> =
2871 unfinalized_proofs_unextended.into_iter().cloned().collect();
2872 while unfinalized_proofs.len() < 2 {
2873 unfinalized_proofs.insert(0, Unfinalized::dummy());
2874 }
2875 unfinalized_proofs
2876 };
2877
2878 let statement = crate::proofs::transaction::StepMainStatement {
2879 proof_state: crate::proofs::transaction::StepMainProofState {
2880 unfinalized_proofs,
2881 messages_for_next_step_proof,
2882 },
2883 messages_for_next_wrap_proof: messages_for_next_wrap_proof_padded.to_vec(),
2884 };
2885
2886 w.primary = statement.to_field_elements_owned();
2887
2888 let proof = create_proof::<C, Fp>(
2889 CreateProofParams {
2890 prover: step_prover,
2891 prev_challenges: prev_challenge_polynomial_commitments,
2892 only_verify_constraints,
2893 },
2894 w,
2895 )
2896 .context("create_proof")?;
2897
2898 let proofs: [&v2::PicklesProofProofsVerified2ReprStableV2; N_PREVIOUS] = rule
2899 .previous_proof_statements
2900 .each_ref()
2901 .map(|stmt| stmt.proof);
2902
2903 let prev_evals = proofs
2904 .iter()
2905 .zip(&*expanded_proofs)
2906 .map(|(p, expanded)| {
2907 let evals = evals_from_p2p(&p.proof.evaluations)?;
2908 let ft_eval1 = p.proof.ft_eval1.to_field()?;
2909 let PointEvaluations { zeta, zeta_omega } = expanded.x_hat;
2910
2911 Ok(AllEvals {
2912 ft_eval1,
2913 evals: EvalsWithPublicInput {
2914 evals,
2915 public_input: (vec![zeta], vec![zeta_omega]),
2916 },
2917 })
2918 })
2919 .collect::<anyhow::Result<Vec<_>>>()
2920 .context("prev_evals")?;
2921
2922 let challenge_polynomial_commitments = expanded_proofs
2923 .iter()
2924 .map(|v| InnerCurve::of_affine(v.sg))
2925 .collect();
2926
2927 let (old_bulletproof_challenges, messages_for_next_wrap_proof): (Vec<_>, Vec<_>) = proofs
2928 .iter()
2929 .map(|v| {
2930 let StatementProofState {
2931 deferred_values,
2932 messages_for_next_wrap_proof,
2933 ..
2934 } = (&v.statement.proof_state).try_into()?;
2935 Ok((
2936 deferred_values.bulletproof_challenges,
2937 messages_for_next_wrap_proof,
2938 ))
2939 })
2940 .collect::<Result<Vec<_>, InvalidBigInt>>() .context("unzip proof state")?
2942 .into_iter()
2943 .unzip();
2944
2945 let old_bulletproof_challenges = old_bulletproof_challenges
2946 .into_iter()
2947 .map(|v: [[u64; 2]; 16]| v.each_ref().map(two_u64_to_field))
2948 .collect();
2949
2950 let step_statement = crate::proofs::transaction::StepStatement {
2951 proof_state: crate::proofs::transaction::StepProofState {
2952 unfinalized_proofs: statement.proof_state.unfinalized_proofs,
2953 messages_for_next_step_proof: ReducedMessagesForNextStepProof {
2954 app_state: Rc::clone(&app_state),
2955 challenge_polynomial_commitments,
2956 old_bulletproof_challenges,
2957 },
2958 },
2959 messages_for_next_wrap_proof,
2960 };
2961
2962 Ok(StepProof {
2963 statement: step_statement,
2964 prev_evals,
2965 proof_with_public: proof,
2966 })
2967}