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