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