mina_tree/proofs/
block.rs

1use std::{rc::Rc, sync::Arc};
2
3use anyhow::Context;
4use consensus::ConsensusState;
5use mina_core::constants::{constraint_constants, ForkConstants};
6use mina_curves::pasta::{Fp, Fq};
7use mina_p2p_messages::{bigint::InvalidBigInt, v2};
8use poseidon::hash::{
9    params::{MINA_PROTO_STATE, MINA_PROTO_STATE_BODY},
10    Inputs,
11};
12
13use crate::{
14    dummy,
15    proofs::{
16        block::consensus::CheckedConsensusState,
17        constants::{
18            make_step_block_data, make_step_transaction_data, StepBlockProof, WrapBlockProof,
19        },
20        field::{Boolean, CircuitVar},
21        numbers::{
22            currency::CheckedSigned,
23            nat::{CheckedNat, CheckedSlot},
24        },
25        step::extract_recursion_challenges,
26        to_field_elements::ToFieldElementsDebug,
27        util::sha256_sum,
28        wrap::{wrap, WrapParams},
29    },
30    scan_state::{
31        currency,
32        fee_excess::{self, FeeExcess},
33        pending_coinbase::{PendingCoinbase, PendingCoinbaseWitness, Stack},
34        protocol_state::MinaHash,
35        scan_state::transaction_snark::{
36            validate_ledgers_at_merge_checked, Registers, SokDigest, Statement, StatementLedgers,
37        },
38        transaction_logic::protocol_state::{EpochLedger, ProtocolStateView},
39    },
40    staged_ledger::hash::StagedLedgerHash,
41    zkapps::intefaces::{SignedAmountBranchParam, SignedAmountInterface},
42    ToInputs,
43};
44
45use super::{
46    field::field,
47    numbers::{
48        currency::CheckedAmount,
49        nat::{CheckedBlockTime, CheckedBlockTimeSpan, CheckedLength},
50    },
51    step::{step, InductiveRule, OptFlag, PreviousProofStatement, StepParams, StepProof},
52    to_field_elements::ToFieldElements,
53    transaction::{transaction_snark::checked_hash, Check, Prover},
54    witness::Witness,
55    wrap::WrapProof,
56};
57
58#[derive(Debug, Clone)]
59pub struct BlockchainState {
60    pub staged_ledger_hash: StagedLedgerHash<Fp>,
61    pub genesis_ledger_hash: Fp,
62    pub ledger_proof_statement: Statement<()>,
63    pub timestamp: currency::BlockTime,
64    pub body_reference: v2::ConsensusBodyReferenceStableV1,
65}
66
67#[derive(Debug, Clone)]
68pub struct SnarkTransition {
69    pub blockchain_state: BlockchainState,
70    pub consensus_transition: currency::Slot,
71    pub pending_coinbase_update: crate::scan_state::pending_coinbase::update::Update,
72}
73
74impl TryFrom<&v2::MinaStateBlockchainStateValueStableV2> for BlockchainState {
75    type Error = InvalidBigInt;
76
77    fn try_from(value: &v2::MinaStateBlockchainStateValueStableV2) -> Result<Self, Self::Error> {
78        let v2::MinaStateBlockchainStateValueStableV2 {
79            staged_ledger_hash,
80            genesis_ledger_hash,
81            ledger_proof_statement,
82            timestamp,
83            body_reference,
84        } = value;
85
86        Ok(Self {
87            staged_ledger_hash: staged_ledger_hash.try_into()?,
88            genesis_ledger_hash: genesis_ledger_hash.to_field()?,
89            ledger_proof_statement: ledger_proof_statement.try_into()?,
90            timestamp: (*timestamp).into(),
91            body_reference: body_reference.clone(),
92        })
93    }
94}
95
96impl TryFrom<&v2::MinaStateSnarkTransitionValueStableV2> for SnarkTransition {
97    type Error = InvalidBigInt;
98
99    fn try_from(value: &v2::MinaStateSnarkTransitionValueStableV2) -> Result<Self, Self::Error> {
100        let v2::MinaStateSnarkTransitionValueStableV2 {
101            blockchain_state,
102            consensus_transition,
103            pending_coinbase_update,
104        } = value;
105
106        Ok(Self {
107            blockchain_state: blockchain_state.try_into()?,
108            consensus_transition: consensus_transition.into(),
109            pending_coinbase_update: pending_coinbase_update.into(),
110        })
111    }
112}
113
114impl ToFieldElements<Fp> for SnarkTransition {
115    fn to_field_elements(&self, fields: &mut Vec<Fp>) {
116        let Self {
117            blockchain_state,
118            consensus_transition,
119            pending_coinbase_update:
120                crate::scan_state::pending_coinbase::update::Update {
121                    action,
122                    coinbase_amount,
123                },
124        } = self;
125
126        blockchain_state.to_field_elements(fields);
127        fields.push(Fp::from(consensus_transition.as_u32()));
128
129        // <https://github.com/MinaProtocol/mina/blob/f6fb903bef974b191776f393a2f9a1e6360750fe/src/lib/mina_base/pending_coinbase.ml#L420>
130        use crate::scan_state::pending_coinbase::update::Action::*;
131        let bits = match action {
132            None => [Boolean::False, Boolean::False],
133            One => [Boolean::True, Boolean::False],
134            TwoCoinbaseInFirst => [Boolean::False, Boolean::True],
135            TwoCoinbaseInSecond => [Boolean::True, Boolean::True],
136        };
137        fields.extend(bits.into_iter().map(Boolean::to_field::<Fp>));
138        fields.push(Fp::from(coinbase_amount.as_u64()));
139    }
140}
141
142impl Check<Fp> for SnarkTransition {
143    fn check(&self, w: &mut Witness<Fp>) {
144        let Self {
145            blockchain_state,
146            consensus_transition,
147            pending_coinbase_update:
148                crate::scan_state::pending_coinbase::update::Update {
149                    action: _,
150                    coinbase_amount,
151                },
152        } = self;
153
154        blockchain_state.check(w);
155        consensus_transition.check(w);
156        coinbase_amount.check(w);
157    }
158}
159
160impl ToFieldElements<Fp> for EpochLedger<Fp> {
161    fn to_field_elements(&self, fields: &mut Vec<Fp>) {
162        let Self {
163            hash,
164            total_currency,
165        } = self;
166        hash.to_field_elements(fields);
167        total_currency.to_field_elements(fields);
168    }
169}
170
171impl ToFieldElements<Fp> for ProtocolState {
172    fn to_field_elements(&self, fields: &mut Vec<Fp>) {
173        let Self {
174            previous_state_hash,
175            body,
176        } = self;
177
178        previous_state_hash.to_field_elements(fields);
179        body.to_field_elements(fields);
180    }
181}
182
183impl Check<Fp> for ProtocolState {
184    fn check(&self, w: &mut Witness<Fp>) {
185        let Self {
186            previous_state_hash: _,
187            body,
188        } = self;
189
190        body.check(w);
191    }
192}
193
194fn ledger_proof_opt(
195    proof: Option<&v2::LedgerProofProdStableV2>,
196    next_state: &v2::MinaStateProtocolStateValueStableV2,
197) -> anyhow::Result<(Statement<SokDigest>, Arc<v2::TransactionSnarkProofStableV2>)> {
198    match proof {
199        Some(proof) => {
200            let statement: Statement<SokDigest> = (&proof.0.statement).try_into()?;
201            let p: &v2::TransactionSnarkProofStableV2 = &proof.0.proof;
202            // TODO: Don't clone the proof here
203            Ok((statement, Arc::new(p.clone())))
204        }
205        None => {
206            let statement: Statement<()> =
207                (&next_state.body.blockchain_state.ledger_proof_statement).try_into()?;
208            let statement = statement.with_digest(SokDigest::default());
209            let p = dummy::dummy_transaction_proof();
210            Ok((statement, p))
211        }
212    }
213}
214
215fn checked_hash_protocol_state(
216    state: &ProtocolState,
217    w: &mut Witness<Fp>,
218) -> anyhow::Result<(Fp, Fp)> {
219    let ProtocolState {
220        previous_state_hash,
221        body,
222    } = state;
223
224    let mut inputs = Inputs::new();
225    body.to_inputs(&mut inputs);
226    let body_hash = checked_hash(&MINA_PROTO_STATE_BODY, &inputs.to_fields(), w);
227
228    let mut inputs = Inputs::new();
229    inputs.append_field(*previous_state_hash);
230    inputs.append_field(body_hash);
231    let hash = checked_hash(&MINA_PROTO_STATE, &inputs.to_fields(), w);
232
233    Ok((hash, body_hash))
234}
235
236// Checked version
237fn checked_hash_protocol_state2(
238    state: &ProtocolState<CheckedConsensusState>,
239    w: &mut Witness<Fp>,
240) -> (Fp, Fp) {
241    let ProtocolState {
242        previous_state_hash,
243        body,
244    } = state;
245
246    let mut inputs = Inputs::new();
247    body.to_inputs(&mut inputs);
248    let body_hash = checked_hash(&MINA_PROTO_STATE_BODY, &inputs.to_fields(), w);
249
250    let mut inputs = Inputs::new();
251    inputs.append_field(*previous_state_hash);
252    inputs.append_field(body_hash);
253    let hash = checked_hash(&MINA_PROTO_STATE, &inputs.to_fields(), w);
254
255    (hash, body_hash)
256}
257
258fn non_pc_registers_equal_var(t1: &Registers, t2: &Registers, w: &mut Witness<Fp>) -> Boolean {
259    let alls = [
260        // t1.pending_coinbase_stack.equal_var(&t2.pending_coinbase_stack, w),
261        field::equal(t1.first_pass_ledger, t2.first_pass_ledger, w),
262        field::equal(t1.second_pass_ledger, t2.second_pass_ledger, w),
263    ]
264    .into_iter()
265    .chain(t1.local_state.checked_equal_prime(&t2.local_state, w))
266    .collect::<Vec<_>>();
267
268    Boolean::all(&alls, w)
269}
270
271fn txn_statement_ledger_hashes_equal(
272    s1: &Statement<()>,
273    s2: &Statement<()>,
274    w: &mut Witness<Fp>,
275) -> Boolean {
276    let source_eq = non_pc_registers_equal_var(&s1.source, &s2.source, w);
277    let target_eq = non_pc_registers_equal_var(&s1.target, &s2.target, w);
278    let left_ledger_eq = field::equal(s1.connecting_ledger_left, s2.connecting_ledger_left, w);
279    let right_ledger_eq = field::equal(s1.connecting_ledger_right, s2.connecting_ledger_right, w);
280    let supply_increase_eq = s1
281        .supply_increase
282        .to_checked()
283        .equal(&s2.supply_increase.to_checked(), w);
284
285    Boolean::all(
286        &[
287            source_eq,
288            target_eq,
289            left_ledger_eq,
290            right_ledger_eq,
291            supply_increase_eq,
292        ],
293        w,
294    )
295}
296
297mod floating_point {
298    use std::cmp::Ordering;
299
300    use ark_ff::BigInteger256;
301    use num_bigint::BigUint;
302
303    use crate::{
304        proofs::{
305            field::FieldWitness, to_field_elements::field_of_bits, transaction::field_to_bits2,
306        },
307        scan_state::currency::{Amount, Balance, Sgn},
308    };
309
310    use super::*;
311
312    pub enum CoeffIntegerPart {
313        Zero,
314        One,
315    }
316
317    const COEFFICIENTS: [(Sgn, BigInteger256); 11] = [
318        (Sgn::Pos, BigInteger256::new([405058, 0, 0, 0])),
319        (Sgn::Neg, BigInteger256::new([1007582, 0, 0, 0])),
320        (Sgn::Pos, BigInteger256::new([465602, 0, 0, 0])),
321        (Sgn::Neg, BigInteger256::new([161365, 0, 0, 0])),
322        (Sgn::Pos, BigInteger256::new([44739, 0, 0, 0])),
323        (Sgn::Neg, BigInteger256::new([10337, 0, 0, 0])),
324        (Sgn::Pos, BigInteger256::new([2047, 0, 0, 0])),
325        (Sgn::Neg, BigInteger256::new([354, 0, 0, 0])),
326        (Sgn::Pos, BigInteger256::new([54, 0, 0, 0])),
327        (Sgn::Neg, BigInteger256::new([7, 0, 0, 0])),
328        (Sgn::Pos, BigInteger256::new([0, 0, 0, 0])),
329    ];
330
331    pub struct Params {
332        pub total_precision: usize,
333        pub per_term_precision: usize,
334        pub terms_needed: usize,
335        pub coefficients: [(Sgn, BigInteger256); 11],
336        pub linear_term_integer_part: CoeffIntegerPart,
337    }
338
339    pub const PARAMS: Params = Params {
340        total_precision: 16,
341        per_term_precision: 20,
342        terms_needed: 11,
343        coefficients: COEFFICIENTS,
344        linear_term_integer_part: CoeffIntegerPart::One,
345    };
346
347    #[derive(Clone)]
348    pub enum Interval {
349        Constant(BigUint),
350        LessThan(BigUint),
351    }
352
353    fn bits_needed(v: BigUint) -> u64 {
354        v.bits().checked_sub(1).unwrap()
355    }
356
357    impl Interval {
358        fn scale(&self, x: BigUint) -> Self {
359            match self {
360                Interval::Constant(v) => Self::Constant(v * x),
361                Interval::LessThan(v) => Self::LessThan(v * x),
362            }
363        }
364
365        fn bits_needed(&self) -> u64 {
366            match self {
367                Interval::Constant(x) => bits_needed(x + BigUint::from(1u64)),
368                Interval::LessThan(x) => bits_needed(x.clone()),
369            }
370        }
371
372        fn quotient(&self, b: &Self) -> Self {
373            use Interval::*;
374
375            match (self, b) {
376                (Constant(a), Constant(b)) => Constant(a / b),
377                (LessThan(a), Constant(b)) => LessThan((a / b) + 1u64),
378                (Constant(a), LessThan(_)) => LessThan(a + 1u64),
379                (LessThan(a), LessThan(_)) => LessThan(a.clone()),
380            }
381        }
382    }
383
384    pub struct SnarkyInteger<F: FieldWitness> {
385        pub value: F,
386        pub interval: Interval,
387        pub bits: Option<Box<[bool]>>,
388    }
389
390    impl<F: FieldWitness> SnarkyInteger<F> {
391        pub fn create(value: F, upper_bound: BigUint) -> Self {
392            Self {
393                value,
394                interval: Interval::LessThan(upper_bound),
395                bits: None,
396            }
397        }
398
399        fn to_field(&self) -> F {
400            self.value
401        }
402
403        fn shift_left(&self, k: usize) -> Self {
404            let Self {
405                value,
406                interval,
407                bits,
408            } = self;
409
410            let two_to_k = BigUint::new(vec![1, 0, 0, 0]) << k;
411
412            Self {
413                value: *value * F::from(two_to_k.clone()),
414                interval: interval.scale(two_to_k),
415                bits: bits.as_ref().map(|_| todo!()),
416            }
417        }
418
419        fn div_mod(&self, b: &Self, w: &mut Witness<F>) -> (Self, Self) {
420            let (q, r) = w.exists({
421                let a: BigUint = self.value.into();
422                let b: BigUint = b.value.into();
423                (F::from(&a / &b), F::from(&a % &b))
424            });
425
426            let q_bit_length = self.interval.bits_needed();
427            let b_bit_length = b.interval.bits_needed();
428
429            let q_bits = w.exists(field_to_bits2(q, q_bit_length as usize));
430            let r_bits = w.exists(field_to_bits2(r, b_bit_length as usize));
431
432            field::assert_lt(b_bit_length, r, b.value, w);
433
434            (
435                Self {
436                    value: q,
437                    interval: self.interval.quotient(&b.interval),
438                    bits: Some(q_bits),
439                },
440                Self {
441                    value: r,
442                    interval: b.interval.clone(),
443                    bits: Some(r_bits),
444                },
445            )
446        }
447    }
448
449    pub fn balance_upper_bound() -> BigUint {
450        BigUint::new(vec![1, 0, 0, 0]) << Balance::NBITS as u32
451    }
452
453    pub fn amount_upper_bound() -> BigUint {
454        BigUint::new(vec![1, 0, 0, 0]) << Amount::NBITS as u32
455    }
456
457    #[derive(Clone, Debug)]
458    pub struct Point<F: FieldWitness> {
459        pub value: F,
460        pub precision: usize,
461    }
462
463    pub fn of_quotient<F: FieldWitness>(
464        precision: usize,
465        top: SnarkyInteger<F>,
466        bottom: SnarkyInteger<F>,
467        w: &mut Witness<F>,
468    ) -> Point<F> {
469        let (q, _r) = top.shift_left(precision).div_mod(&bottom, w);
470        Point {
471            value: q.to_field(),
472            precision,
473        }
474    }
475
476    impl<F: FieldWitness> Point<F> {
477        pub fn mul(&self, y: &Self, w: &mut Witness<F>) -> Self {
478            let new_precision = self.precision + y.precision;
479            Self {
480                value: field::mul(self.value, y.value, w),
481                precision: new_precision,
482            }
483        }
484
485        pub fn const_mul(&self, y: &Self) -> Self {
486            let new_precision = self.precision + y.precision;
487            Self {
488                value: self.value * y.value,
489                precision: new_precision,
490            }
491        }
492
493        pub fn powers(&self, n: usize, w: &mut Witness<F>) -> Vec<Self> {
494            let mut res = vec![self.clone(); n];
495            for i in 1..n {
496                res[i] = self.mul(&res[i - 1], w);
497            }
498            res
499        }
500
501        pub fn constant(value: &BigInteger256, precision: usize) -> anyhow::Result<Self> {
502            Ok(Self {
503                value: (*value).into(),
504                precision,
505            })
506        }
507
508        pub fn add_signed(&self, (sgn, t2): (Sgn, &Self)) -> Self {
509            let precision = self.precision.max(t2.precision);
510            let (t1, t2) = if self.precision < t2.precision {
511                (self, t2)
512            } else {
513                (t2, self)
514            };
515
516            let powed2 = (0..(t2.precision - t1.precision)).fold(F::one(), |acc, _| acc.double());
517
518            let value = match sgn {
519                Sgn::Pos => (powed2 * t1.value) + t2.value,
520                Sgn::Neg => (powed2 * t1.value) - t2.value,
521            };
522
523            Self { value, precision }
524        }
525
526        pub fn add(&self, t2: &Self) -> Self {
527            self.add_signed((Sgn::Pos, t2))
528        }
529
530        pub fn of_bits<const N: usize>(bits: &[bool; N], precision: usize) -> Self {
531            Self {
532                value: field_of_bits(bits),
533                precision,
534            }
535        }
536
537        pub fn le(&self, t2: &Self, w: &mut Witness<F>) -> Boolean {
538            let precision = self.precision.max(t2.precision);
539
540            let padding = {
541                let k = precision - self.precision.min(t2.precision);
542                (0..k).fold(F::one(), |acc, _| acc.double())
543            };
544
545            let (x1, x2) = {
546                let (x1, x2) = (self.value, t2.value);
547
548                match self.precision.cmp(&t2.precision) {
549                    Ordering::Less => (padding * x1, x2),
550                    Ordering::Greater => (x1, padding * x2),
551                    Ordering::Equal => (x1, x1),
552                }
553            };
554
555            field::compare(precision as u64, x1, x2, w).1
556        }
557    }
558}
559
560mod snarky_taylor {
561    use crate::{proofs::field::FieldWitness, scan_state::currency::Sgn};
562
563    use super::*;
564    use floating_point::*;
565
566    fn taylor_sum<F: FieldWitness>(
567        x_powers: Vec<Point<F>>,
568        coefficients: impl Iterator<Item = (Sgn, floating_point::Point<F>)>,
569        linear_term_integer_part: &CoeffIntegerPart,
570    ) -> Point<F> {
571        let acc = coefficients
572            .zip(&x_powers)
573            .fold(None, |sum, ((sgn, ci), xi)| {
574                let term = ci.const_mul(xi);
575                match sum {
576                    None => Some(term),
577                    Some(s) => Some(s.add_signed((sgn, &term))),
578                }
579            })
580            .unwrap();
581
582        match linear_term_integer_part {
583            CoeffIntegerPart::Zero => acc,
584            CoeffIntegerPart::One => acc.add(&x_powers[0]),
585        }
586    }
587
588    pub fn one_minus_exp<F: FieldWitness>(
589        params: &Params,
590        x: Point<F>,
591        w: &mut Witness<F>,
592    ) -> Point<F> {
593        let floating_point::Params {
594            total_precision: _,
595            per_term_precision,
596            terms_needed,
597            coefficients,
598            linear_term_integer_part,
599        } = params;
600
601        let powers = x.powers(*terms_needed, w);
602        let coefficients = coefficients
603            .iter()
604            .map(|(sgn, c)| (*sgn, Point::<F>::constant(c, *per_term_precision).unwrap())); // Never fail, coeffs are hardcoded
605        taylor_sum(powers, coefficients, linear_term_integer_part)
606    }
607}
608
609mod vrf {
610    use std::ops::Neg;
611
612    use mina_signer::{CompressedPubKey, PubKey};
613    use poseidon::hash::params::{MINA_VRF_MESSAGE, MINA_VRF_OUTPUT};
614
615    use crate::{
616        checked_verify_merkle_path,
617        proofs::{
618            field::GroupAffine,
619            transaction::{
620                decompress_var, field_to_bits, legacy_input::to_bits, scale_known,
621                scale_non_constant, InnerCurve,
622            },
623        },
624        scan_state::currency::{Amount, Balance},
625        sparse_ledger::SparseLedger,
626        AccountIndex, Address, AppendToInputs,
627    };
628
629    use super::*;
630
631    struct Message<'a> {
632        global_slot: &'a CheckedSlot<Fp>,
633        seed: Fp,
634        delegator: AccountIndex,
635        delegator_bits: [bool; 35],
636    }
637
638    impl ToInputs for Message<'_> {
639        fn to_inputs(&self, inputs: &mut Inputs) {
640            let Self {
641                global_slot,
642                seed,
643                delegator: _,
644                delegator_bits,
645            } = self;
646
647            inputs.append(seed);
648            inputs.append_u32(global_slot.to_inner().as_u32());
649            for b in delegator_bits {
650                inputs.append_bool(*b);
651            }
652        }
653    }
654
655    fn hash_to_group(m: &Message, w: &mut Witness<Fp>) -> GroupAffine<Fp> {
656        let inputs = m.to_inputs_owned().to_fields();
657        let hash = checked_hash(&MINA_VRF_MESSAGE, &inputs, w);
658        crate::proofs::group_map::to_group(hash, w)
659    }
660
661    fn scale_generator(
662        s: &[bool; 255],
663        init: &InnerCurve<Fp>,
664        w: &mut Witness<Fp>,
665    ) -> GroupAffine<Fp> {
666        scale_known(InnerCurve::<Fp>::one().to_affine(), s, init, w)
667    }
668
669    fn eval(
670        m: &InnerCurve<Fp>,
671        private_key: &[bool; 255],
672        message: &Message,
673        w: &mut Witness<Fp>,
674    ) -> Fp {
675        let h = hash_to_group(message, w);
676
677        let u = {
678            let _ = w.exists_no_check(h);
679            let u = scale_non_constant(h, private_key, m, w);
680
681            // unshift_nonzero
682            let neg = m.to_affine().neg();
683            w.exists(neg.y);
684            w.add_fast(neg, u)
685        };
686
687        let GroupAffine::<Fp> { x, y, .. } = u;
688
689        let mut inputs = message.to_inputs_owned();
690        inputs.append_field(x);
691        inputs.append_field(y);
692
693        checked_hash(&MINA_VRF_OUTPUT, &inputs.to_fields(), w)
694    }
695
696    fn eval_and_check_public_key(
697        m: &InnerCurve<Fp>,
698        private_key: &[bool; 255],
699        public_key: &PubKey,
700        message: Message,
701        w: &mut Witness<Fp>,
702    ) -> Fp {
703        let _ = {
704            let _public_key_shifted = w.add_fast(m.to_affine(), *public_key.point());
705            scale_generator(private_key, m, w)
706        };
707
708        eval(m, private_key, &message, w)
709    }
710
711    fn get_vrf_evaluation(
712        m: &InnerCurve<Fp>,
713        message: Message,
714        prover_state: &v2::ConsensusStakeProofStableV2,
715        w: &mut Witness<Fp>,
716    ) -> anyhow::Result<(Fp, Box<crate::Account>)> {
717        let private_key = prover_state.producer_private_key.to_field::<Fq>()?;
718        let private_key = w.exists(field_to_bits::<Fq, 255>(private_key));
719
720        let account = {
721            let mut ledger: SparseLedger = (&prover_state.ledger).try_into()?;
722
723            let staker_addr = message.delegator;
724            let staker_addr =
725                Address::from_index(staker_addr, constraint_constants().ledger_depth as usize);
726
727            let account = ledger.get_exn(&staker_addr);
728            let path = ledger.path_exn(staker_addr.clone());
729
730            let (account, path) = w.exists((account, path));
731            checked_verify_merkle_path(&account, &path, w);
732
733            account
734        };
735
736        let delegate = {
737            let delegate = account.delegate.as_ref().unwrap();
738            decompress_var(delegate, w)
739        };
740
741        let evaluation = eval_and_check_public_key(m, &private_key, &delegate, message, w);
742
743        Ok((evaluation, account))
744    }
745
746    fn is_satisfied(
747        my_stake: Balance,
748        total_stake: Amount,
749        vrf_output: &[bool; VRF_OUTPUT_NBITS],
750        w: &mut Witness<Fp>,
751    ) -> Boolean {
752        use floating_point::*;
753
754        let top = SnarkyInteger::create(my_stake.to_field::<Fp>(), balance_upper_bound());
755        let bottom = SnarkyInteger::create(total_stake.to_field::<Fp>(), amount_upper_bound());
756        let precision = PARAMS.per_term_precision;
757
758        let point = floating_point::of_quotient(precision, top, bottom, w);
759        let rhs = snarky_taylor::one_minus_exp(&PARAMS, point, w);
760
761        let lhs = vrf_output;
762        Point::of_bits(lhs, VRF_OUTPUT_NBITS).le(&rhs, w)
763    }
764
765    pub const VRF_OUTPUT_NBITS: usize = 253;
766
767    fn truncate_vrf_output(output: Fp, w: &mut Witness<Fp>) -> Box<[bool; VRF_OUTPUT_NBITS]> {
768        let output: [bool; 255] = w.exists(field_to_bits(output));
769        Box::new(std::array::from_fn(|i| output[i])) // 2 last bits are ignored
770    }
771
772    pub fn check(
773        m: &InnerCurve<Fp>,
774        epoch_ledger: &EpochLedger<Fp>,
775        global_slot: &CheckedSlot<Fp>,
776        _block_stake_winner: &CompressedPubKey,
777        _block_creator: &CompressedPubKey,
778        seed: Fp,
779        prover_state: &v2::ConsensusStakeProofStableV2,
780        w: &mut Witness<Fp>,
781    ) -> anyhow::Result<(
782        Boolean,
783        Fp,
784        Box<[bool; VRF_OUTPUT_NBITS]>,
785        Box<crate::Account>,
786    )> {
787        let (winner_addr, winner_addr_bits) = {
788            const LEDGER_DEPTH: usize = 35;
789            assert_eq!(constraint_constants().ledger_depth, LEDGER_DEPTH as u64);
790
791            let account_index = prover_state.delegator.as_u64();
792            let bits = w.exists(to_bits::<_, LEDGER_DEPTH>(account_index));
793            (AccountIndex(account_index), bits)
794        };
795
796        let (result, winner_account) = get_vrf_evaluation(
797            m,
798            Message {
799                global_slot,
800                seed,
801                delegator: winner_addr,
802                delegator_bits: winner_addr_bits,
803            },
804            prover_state,
805            w,
806        )?;
807
808        let my_stake = winner_account.balance;
809        let truncated_result = truncate_vrf_output(result, w);
810        let satisifed = is_satisfied(my_stake, epoch_ledger.total_currency, &truncated_result, w);
811
812        Ok((satisifed, result, truncated_result, winner_account))
813    }
814}
815
816pub mod consensus {
817    use ark_ff::Zero;
818    use mina_signer::CompressedPubKey;
819    use poseidon::hash::params::MINA_EPOCH_SEED;
820
821    use super::{vrf::VRF_OUTPUT_NBITS, *};
822    use crate::{
823        decompress_pk,
824        proofs::{
825            numbers::{
826                currency::CheckedCurrency,
827                nat::{CheckedN, CheckedN32, CheckedSlotSpan},
828            },
829            transaction::{compress_var, create_shifted_inner_curve, CompressedPubKeyVar},
830        },
831        scan_state::{
832            currency::{Amount, Length},
833            transaction_logic::protocol_state::EpochData,
834        },
835        Account,
836    };
837
838    pub struct ConsensusConstantsChecked {
839        pub k: CheckedLength<Fp>,
840        pub delta: CheckedLength<Fp>,
841        pub block_window_duration_ms: CheckedBlockTimeSpan<Fp>,
842        pub slots_per_sub_window: CheckedLength<Fp>,
843        pub slots_per_window: CheckedLength<Fp>,
844        pub sub_windows_per_window: CheckedLength<Fp>,
845        pub slots_per_epoch: CheckedLength<Fp>,
846        pub grace_period_slots: CheckedLength<Fp>,
847        pub grace_period_end: CheckedLength<Fp>,
848        pub slot_duration_ms: CheckedBlockTimeSpan<Fp>,
849        pub epoch_duration: CheckedBlockTimeSpan<Fp>,
850        pub checkpoint_window_slots_per_year: CheckedLength<Fp>,
851        pub checkpoint_window_size_in_slots: CheckedLength<Fp>,
852        pub delta_duration: CheckedBlockTimeSpan<Fp>,
853        pub genesis_state_timestamp: CheckedBlockTime<Fp>,
854    }
855
856    /// Number of millisecond per day
857    const N_MILLIS_PER_DAY: u64 = 86400000;
858
859    // Keep this in sync with the implementation of ConsensusConstants::create
860    // in ledger/src/transaction_pool.rs
861    fn create_constant_prime(
862        prev_state: &ProtocolState,
863        w: &mut Witness<Fp>,
864    ) -> ConsensusConstantsChecked {
865        let v2::MinaBaseProtocolConstantsCheckedValueStableV1 {
866            k,
867            slots_per_epoch,
868            slots_per_sub_window,
869            grace_period_slots,
870            delta,
871            genesis_state_timestamp,
872        } = &prev_state.body.constants;
873
874        let constraint_constants = constraint_constants();
875
876        let of_u64 = |n: u64| CheckedN::<Fp>::from_field(n.into());
877        let of_u32 = |n: u32| CheckedN::<Fp>::from_field(n.into());
878
879        let block_window_duration_ms = of_u64(constraint_constants.block_window_duration_ms);
880
881        let k = of_u32(k.as_u32());
882        let delta = of_u32(delta.as_u32());
883        let slots_per_sub_window = of_u32(slots_per_sub_window.as_u32());
884        let sub_windows_per_window = of_u64(constraint_constants.sub_windows_per_window);
885
886        let slots_per_window = slots_per_sub_window.const_mul(&sub_windows_per_window, w);
887
888        let slots_per_epoch = of_u32(slots_per_epoch.as_u32());
889
890        let slot_duration_ms = block_window_duration_ms.clone();
891
892        let epoch_duration = {
893            let size = &slots_per_epoch;
894            slot_duration_ms.const_mul(size, w)
895        };
896
897        let delta_duration = {
898            let delta_plus_one = delta.add(&CheckedN::one(), w);
899            slot_duration_ms.const_mul(&delta_plus_one, w)
900        };
901
902        let grace_period_slots = of_u32(grace_period_slots.as_u32());
903        let grace_period_end = { grace_period_slots.add(&slots_per_window, w) };
904
905        let to_length = |v: CheckedN<Fp>| CheckedLength::from_field(v.to_field());
906        let to_timespan = |v: CheckedN<Fp>| CheckedBlockTimeSpan::from_field(v.to_field());
907
908        ConsensusConstantsChecked {
909            k: to_length(k),
910            delta: to_length(delta),
911            block_window_duration_ms: to_timespan(block_window_duration_ms),
912            slots_per_sub_window: to_length(slots_per_sub_window),
913            slots_per_window: to_length(slots_per_window),
914            sub_windows_per_window: to_length(sub_windows_per_window),
915            slots_per_epoch: to_length(slots_per_epoch),
916            grace_period_slots: to_length(grace_period_slots),
917            grace_period_end: to_length(grace_period_end),
918            slot_duration_ms: to_timespan(slot_duration_ms),
919            epoch_duration: to_timespan(epoch_duration),
920            checkpoint_window_slots_per_year: CheckedLength::zero(),
921            checkpoint_window_size_in_slots: CheckedLength::zero(),
922            delta_duration: to_timespan(delta_duration),
923            genesis_state_timestamp: {
924                let v = of_u64(genesis_state_timestamp.as_u64());
925                CheckedBlockTime::from_field(v.to_field())
926            },
927        }
928    }
929
930    fn check_invariants(constants: &ConsensusConstantsChecked) {
931        let slots_per_epoch = constants.slots_per_epoch.to_inner().as_u32();
932        let slots_per_window = constants.slots_per_window.to_inner().as_u32();
933        let grace_period_end = constants.grace_period_end.to_inner().as_u32();
934
935        let grace_period_effective_end = grace_period_end - slots_per_window;
936
937        assert!(grace_period_effective_end < (slots_per_epoch / 3))
938    }
939
940    fn create_constant(
941        prev_state: &ProtocolState,
942        w: &mut Witness<Fp>,
943    ) -> ConsensusConstantsChecked {
944        let mut constants = create_constant_prime(prev_state, w);
945
946        let (checkpoint_window_slots_per_year, checkpoint_window_size_in_slots) = {
947            let of_u64 = |n: u64| CheckedN::<Fp>::from_field(n.into());
948            let of_field = |f: Fp| CheckedN::<Fp>::from_field(f);
949
950            let per_year = of_u64(12);
951            let slot_duration_ms = of_field(constants.slot_duration_ms.to_field());
952
953            let (slots_per_year, _) = {
954                let one_year_ms = of_u64(365 * N_MILLIS_PER_DAY);
955                one_year_ms.div_mod(&slot_duration_ms, w)
956            };
957
958            let size_in_slots = {
959                let (size_in_slots, _rem) = slots_per_year.div_mod(&per_year, w);
960                size_in_slots
961            };
962
963            let to_length = |v: CheckedN<Fp>| CheckedLength::from_field(v.to_field());
964            (to_length(slots_per_year), to_length(size_in_slots))
965        };
966
967        constants.checkpoint_window_slots_per_year = checkpoint_window_slots_per_year;
968        constants.checkpoint_window_size_in_slots = checkpoint_window_size_in_slots;
969
970        check_invariants(&constants);
971
972        constants
973    }
974
975    type CheckedEpoch = CheckedBlockTime<Fp>;
976
977    #[derive(Clone, Debug)]
978    pub struct GlobalSlot {
979        pub slot_number: CheckedSlot<Fp>,
980        pub slots_per_epoch: CheckedLength<Fp>,
981    }
982
983    impl From<&v2::ConsensusGlobalSlotStableV1> for GlobalSlot {
984        fn from(value: &v2::ConsensusGlobalSlotStableV1) -> Self {
985            let v2::ConsensusGlobalSlotStableV1 {
986                slot_number,
987                slots_per_epoch,
988            } = value;
989
990            Self {
991                slot_number: CheckedSlot::from_field(slot_number.as_u32().into()),
992                slots_per_epoch: CheckedLength::from_field(slots_per_epoch.as_u32().into()),
993            }
994        }
995    }
996
997    impl GlobalSlot {
998        fn of_slot_number(
999            constants: &ConsensusConstantsChecked,
1000            slot_number: CheckedSlot<Fp>,
1001        ) -> Self {
1002            Self {
1003                slot_number,
1004                slots_per_epoch: constants.slots_per_epoch,
1005            }
1006        }
1007
1008        fn diff_slots(&self, other: &Self, w: &mut Witness<Fp>) -> CheckedSlotSpan<Fp> {
1009            self.slot_number.diff(&other.slot_number, w)
1010        }
1011
1012        fn less_than(&self, other: &Self, w: &mut Witness<Fp>) -> Boolean {
1013            self.slot_number.less_than(&other.slot_number, w)
1014        }
1015
1016        fn to_epoch_and_slot(&self, w: &mut Witness<Fp>) -> (CheckedEpoch, CheckedSlot<Fp>) {
1017            let (epoch, slot) = self
1018                .slot_number
1019                .div_mod(&CheckedSlot::from_field(self.slots_per_epoch.to_field()), w);
1020
1021            (CheckedEpoch::from_field(epoch.to_field()), slot)
1022        }
1023    }
1024
1025    fn compute_supercharge_coinbase(
1026        winner_account: &Account,
1027        global_slot: &CheckedSlot<Fp>,
1028        w: &mut Witness<Fp>,
1029    ) -> Boolean {
1030        let winner_locked = winner_account.has_locked_tokens_checked(global_slot, w);
1031        winner_locked.neg()
1032    }
1033
1034    fn same_checkpoint_window(
1035        constants: &ConsensusConstantsChecked,
1036        prev: &GlobalSlot,
1037        next: &GlobalSlot,
1038        w: &mut Witness<Fp>,
1039    ) -> Boolean {
1040        let slot1 = prev;
1041        let slot2 = next;
1042
1043        let slot1 = &slot1.slot_number;
1044        let checkpoint_window_size_in_slots = &constants.checkpoint_window_size_in_slots;
1045
1046        let (_q1, r1) = slot1.div_mod(&checkpoint_window_size_in_slots.to_slot(), w);
1047
1048        let next_window_start =
1049            { slot1.to_field() - r1.to_field() + checkpoint_window_size_in_slots.to_field() };
1050
1051        slot2
1052            .slot_number
1053            .less_than(&CheckedSlot::from_field(next_window_start), w)
1054    }
1055
1056    struct GlobalSubWindow {
1057        inner: CheckedN32<Fp>,
1058    }
1059
1060    impl std::ops::Deref for GlobalSubWindow {
1061        type Target = CheckedN32<Fp>;
1062
1063        fn deref(&self) -> &Self::Target {
1064            &self.inner
1065        }
1066    }
1067
1068    impl GlobalSubWindow {
1069        fn of_global_slot(
1070            constants: &ConsensusConstantsChecked,
1071            s: &GlobalSlot,
1072            w: &mut Witness<Fp>,
1073        ) -> Self {
1074            let slot_as_field = s.slot_number.to_field();
1075            let slot_as_field = CheckedN32::from_field(slot_as_field);
1076
1077            let (q, _) = slot_as_field.div_mod(
1078                &CheckedN32::from_field(constants.slots_per_sub_window.to_field()),
1079                w,
1080            );
1081            Self { inner: q }
1082        }
1083
1084        fn sub_window(&self, constants: &ConsensusConstantsChecked, w: &mut Witness<Fp>) -> Self {
1085            let (_, shift) = self.inner.div_mod(
1086                &CheckedN32::from_field(constants.sub_windows_per_window.to_field()),
1087                w,
1088            );
1089            Self { inner: shift }
1090        }
1091
1092        fn equal(&self, other: &Self, w: &mut Witness<Fp>) -> Boolean {
1093            self.inner.equal(&other.inner, w)
1094        }
1095
1096        fn add(&self, b: &CheckedLength<Fp>, w: &mut Witness<Fp>) -> Self {
1097            let inner = self.inner.add(&CheckedN32::from_field(b.to_field()), w);
1098            Self { inner }
1099        }
1100
1101        fn gte(&self, other: &Self, w: &mut Witness<Fp>) -> Boolean {
1102            self.inner.gte(&other.inner, w)
1103        }
1104    }
1105
1106    type SubWindow = CheckedN32<Fp>;
1107
1108    struct UpdateMinWindowDensityParams<'a> {
1109        constants: &'a ConsensusConstantsChecked,
1110        prev_global_slot: &'a GlobalSlot,
1111        next_global_slot: &'a GlobalSlot,
1112        prev_sub_window_densities: Vec<u32>,
1113        prev_min_window_density: u32,
1114    }
1115
1116    fn update_min_window_density(
1117        params: UpdateMinWindowDensityParams,
1118        w: &mut Witness<Fp>,
1119    ) -> (CheckedLength<Fp>, Vec<CheckedLength<Fp>>) {
1120        let UpdateMinWindowDensityParams {
1121            constants: c,
1122            prev_global_slot,
1123            next_global_slot,
1124            prev_sub_window_densities,
1125            prev_min_window_density,
1126        } = params;
1127
1128        let prev_global_sub_window = GlobalSubWindow::of_global_slot(c, prev_global_slot, w);
1129        let next_global_sub_window = GlobalSubWindow::of_global_slot(c, next_global_slot, w);
1130
1131        let prev_relative_sub_window = prev_global_sub_window.sub_window(c, w);
1132        let next_relative_sub_window = next_global_sub_window.sub_window(c, w);
1133
1134        let same_sub_window = prev_global_sub_window.equal(&next_global_sub_window, w);
1135        let overlapping_window = {
1136            let x = prev_global_sub_window.add(&c.sub_windows_per_window, w);
1137            x.gte(&next_global_sub_window, w)
1138        };
1139
1140        let current_sub_window_densities = prev_sub_window_densities
1141            .iter()
1142            .enumerate()
1143            .map(|(i, density)| {
1144                let gt_prev_sub_window =
1145                    SubWindow::constant(i).greater_than(&prev_relative_sub_window, w);
1146
1147                // :(
1148                // This will be removed once we have cvar
1149                let lt_next_sub_window = if i == 0 {
1150                    SubWindow::constant(i).const_less_than(&next_relative_sub_window, w)
1151                } else {
1152                    SubWindow::constant(i).less_than(&next_relative_sub_window, w)
1153                };
1154
1155                let within_range = {
1156                    let cond = prev_relative_sub_window.less_than(&next_relative_sub_window, w);
1157                    let on_true = gt_prev_sub_window.and(&lt_next_sub_window, w);
1158                    let on_false = gt_prev_sub_window.or(&lt_next_sub_window, w);
1159
1160                    w.exists_no_check(match cond {
1161                        Boolean::True => on_true,
1162                        Boolean::False => on_false,
1163                    })
1164                };
1165
1166                let density = Length::from_u32(*density).to_checked::<Fp>();
1167
1168                let on_true = density;
1169                let on_false = {
1170                    let cond = overlapping_window.and(&within_range.neg(), w);
1171                    w.exists_no_check(match cond {
1172                        Boolean::True => density,
1173                        Boolean::False => CheckedLength::zero(),
1174                    })
1175                };
1176
1177                w.exists_no_check(match same_sub_window {
1178                    Boolean::True => on_true,
1179                    Boolean::False => on_false,
1180                })
1181            })
1182            .collect::<Vec<_>>();
1183
1184        let current_window_density = current_sub_window_densities.iter().enumerate().fold(
1185            CheckedLength::zero(),
1186            |acc, (i, v)| {
1187                // :(
1188                // This will be removed once we have cvar
1189                if i == 0 {
1190                    acc.const_add(v, w)
1191                } else {
1192                    acc.add(v, w)
1193                }
1194            },
1195        );
1196
1197        let min_window_density = {
1198            let in_grace_period = next_global_slot.less_than(
1199                &GlobalSlot::of_slot_number(c, c.grace_period_end.to_slot()),
1200                w,
1201            );
1202            let prev_min_window_density = Length::from_u32(prev_min_window_density).to_checked();
1203
1204            let cond = same_sub_window.or(&in_grace_period, w);
1205            let on_true = prev_min_window_density;
1206            let on_false = current_window_density.min(&prev_min_window_density, w);
1207
1208            w.exists_no_check(match cond {
1209                Boolean::True => on_true,
1210                Boolean::False => on_false,
1211            })
1212        };
1213
1214        let next_sub_window_densities = current_sub_window_densities
1215            .iter()
1216            .enumerate()
1217            .map(|(i, density)| {
1218                let is_next_sub_window = SubWindow::constant(i).equal(&next_relative_sub_window, w);
1219
1220                let on_true = {
1221                    w.exists_no_check(match same_sub_window {
1222                        Boolean::True => density.const_succ(),
1223                        Boolean::False => CheckedLength::zero().const_succ(),
1224                    })
1225                };
1226
1227                w.exists_no_check(match is_next_sub_window {
1228                    Boolean::True => on_true,
1229                    Boolean::False => *density,
1230                })
1231            })
1232            .collect::<Vec<_>>();
1233
1234        (min_window_density, next_sub_window_densities)
1235    }
1236
1237    #[derive(Debug, Clone)]
1238    pub struct ConsensusState {
1239        pub blockchain_length: currency::Length,
1240        pub epoch_count: currency::Length,
1241        pub min_window_density: currency::Length,
1242        pub sub_window_densities: Vec<currency::Length>,
1243        pub last_vrf_output: Box<[bool; VRF_OUTPUT_NBITS]>,
1244        pub curr_global_slot_since_hard_fork: GlobalSlot,
1245        pub global_slot_since_genesis: currency::Slot,
1246        pub total_currency: currency::Amount,
1247        pub staking_epoch_data: EpochData<Fp>,
1248        pub next_epoch_data: EpochData<Fp>,
1249        pub has_ancestor_in_same_checkpoint_window: bool,
1250        pub block_stake_winner: CompressedPubKey,
1251        pub block_creator: CompressedPubKey,
1252        pub coinbase_receiver: CompressedPubKey,
1253        pub supercharge_coinbase: bool,
1254    }
1255
1256    #[derive(Debug, Clone)]
1257    pub struct CheckedConsensusState {
1258        pub blockchain_length: CheckedLength<Fp>,
1259        pub epoch_count: CheckedLength<Fp>,
1260        pub min_window_density: CheckedLength<Fp>,
1261        pub sub_window_densities: Vec<CheckedLength<Fp>>,
1262        pub last_vrf_output: Box<[bool; VRF_OUTPUT_NBITS]>,
1263        pub curr_global_slot_since_hard_fork: GlobalSlot,
1264        pub global_slot_since_genesis: CheckedSlot<Fp>,
1265        pub total_currency: CheckedAmount<Fp>,
1266        pub staking_epoch_data: EpochData<Fp>,
1267        pub next_epoch_data: EpochData<Fp>,
1268        pub has_ancestor_in_same_checkpoint_window: Boolean,
1269        pub block_stake_winner: CompressedPubKey,
1270        pub block_creator: CompressedPubKey,
1271        pub coinbase_receiver: CompressedPubKey,
1272        pub supercharge_coinbase: Boolean,
1273    }
1274
1275    pub fn next_state_checked(
1276        prev_state: &ProtocolState,
1277        prev_state_hash: Fp,
1278        transition: &SnarkTransition,
1279        supply_increase: CheckedSigned<Fp, CheckedAmount<Fp>>,
1280        prover_state: &v2::ConsensusStakeProofStableV2,
1281        w: &mut Witness<Fp>,
1282    ) -> anyhow::Result<(Boolean, CheckedConsensusState)> {
1283        let previous_blockchain_state_ledger_hash = prev_state
1284            .body
1285            .blockchain_state
1286            .ledger_proof_statement
1287            .target
1288            .first_pass_ledger;
1289        let genesis_ledger_hash = prev_state.body.blockchain_state.genesis_ledger_hash;
1290        let consensus_transition =
1291            CheckedSlot::<Fp>::from_field(transition.consensus_transition.as_u32().into());
1292        let previous_state = &prev_state.body.consensus_state;
1293        // transiti
1294
1295        let constants = create_constant(prev_state, w);
1296
1297        let ConsensusState {
1298            curr_global_slot_since_hard_fork: prev_global_slot,
1299            ..
1300        } = &prev_state.body.consensus_state;
1301
1302        let next_global_slot = GlobalSlot::of_slot_number(&constants, consensus_transition);
1303
1304        let slot_diff = next_global_slot.diff_slots(prev_global_slot, w);
1305
1306        {
1307            let global_slot_increased = prev_global_slot.less_than(&next_global_slot, w);
1308            let is_genesis = field::equal(
1309                CheckedSlot::zero().to_field(),
1310                next_global_slot.slot_number.to_field(),
1311                w,
1312            );
1313
1314            Boolean::assert_any(&[global_slot_increased, is_genesis], w)
1315        };
1316
1317        let (next_epoch, next_slot) = next_global_slot.to_epoch_and_slot(w);
1318        let (prev_epoch, _prev_slot) = prev_global_slot.to_epoch_and_slot(w);
1319
1320        let global_slot_since_genesis =
1321            CheckedSlot::<Fp>::from_field(previous_state.global_slot_since_genesis.as_u32().into())
1322                .add(&CheckedSlot::<Fp>::from_field(slot_diff.to_field()), w);
1323
1324        let epoch_increased = prev_epoch.less_than(&next_epoch, w);
1325
1326        let staking_epoch_data = {
1327            let next_epoch_data: &EpochData<Fp> = &previous_state.next_epoch_data;
1328            let staking_epoch_data: &EpochData<Fp> = &previous_state.staking_epoch_data;
1329
1330            w.exists_no_check(match epoch_increased {
1331                Boolean::True => next_epoch_data,
1332                Boolean::False => staking_epoch_data,
1333            })
1334            .clone()
1335        };
1336
1337        let next_slot_number = next_global_slot.slot_number;
1338
1339        let block_stake_winner = {
1340            let delegator_pk: CompressedPubKey = (&prover_state.delegator_pk).try_into()?;
1341            w.exists(delegator_pk)
1342        };
1343
1344        let block_creator = {
1345            // TODO: See why `prover_state.producer_public_key` is compressed
1346            //       In OCaml it's uncompressed
1347            let producer_public_key: CompressedPubKey =
1348                (&prover_state.producer_public_key).try_into()?;
1349            let pk = decompress_pk(&producer_public_key).unwrap();
1350            w.exists_no_check(&pk);
1351            // TODO: Remove this
1352            let CompressedPubKeyVar { x, is_odd } = compress_var(pk.point(), w);
1353            CompressedPubKey { x, is_odd }
1354        };
1355
1356        let coinbase_receiver = {
1357            let pk: CompressedPubKey = (&prover_state.coinbase_receiver_pk).try_into()?;
1358            w.exists(pk)
1359        };
1360
1361        let (threshold_satisfied, vrf_result, truncated_vrf_result, winner_account) = {
1362            let m = create_shifted_inner_curve::<Fp>(w);
1363
1364            vrf::check(
1365                &m,
1366                &staking_epoch_data.ledger,
1367                &next_slot_number,
1368                &block_stake_winner,
1369                &block_creator,
1370                staking_epoch_data.seed,
1371                prover_state,
1372                w,
1373            )?
1374        };
1375
1376        let supercharge_coinbase =
1377            compute_supercharge_coinbase(&winner_account, &global_slot_since_genesis, w);
1378
1379        let (new_total_currency, _overflow) = {
1380            let total_currency: Amount = previous_state.total_currency;
1381            total_currency
1382                .to_checked()
1383                .add_signed_flagged(supply_increase, w)
1384        };
1385
1386        let has_ancestor_in_same_checkpoint_window =
1387            same_checkpoint_window(&constants, prev_global_slot, &next_global_slot, w);
1388
1389        let in_seed_update_range = next_slot.in_seed_update_range(&constants, w);
1390
1391        let update_next_epoch_ledger = {
1392            let snarked_ledger_is_still_genesis = field::equal(
1393                genesis_ledger_hash,
1394                previous_blockchain_state_ledger_hash,
1395                w,
1396            );
1397            epoch_increased.and(&snarked_ledger_is_still_genesis.neg(), w)
1398        };
1399
1400        fn epoch_seed_update_var(seed: Fp, vrf_result: Fp, w: &mut Witness<Fp>) -> Fp {
1401            checked_hash(&MINA_EPOCH_SEED, &[seed, vrf_result], w)
1402        }
1403
1404        let next_epoch_data = {
1405            let seed = {
1406                let base: Fp = previous_state.next_epoch_data.seed;
1407                let updated = epoch_seed_update_var(base, vrf_result, w);
1408                w.exists_no_check(match in_seed_update_range {
1409                    Boolean::True => updated,
1410                    Boolean::False => base,
1411                })
1412            };
1413
1414            let epoch_length = {
1415                let base = w.exists_no_check(match epoch_increased {
1416                    Boolean::True => CheckedLength::zero(),
1417                    Boolean::False => {
1418                        let length: &Length = &previous_state.next_epoch_data.epoch_length;
1419                        length.to_checked()
1420                    }
1421                });
1422                base.const_succ()
1423            };
1424
1425            let ledger = w.exists_no_check(match update_next_epoch_ledger {
1426                Boolean::True => EpochLedger {
1427                    hash: previous_blockchain_state_ledger_hash,
1428                    total_currency: new_total_currency.to_inner(), // TODO: Might overflow ?
1429                },
1430                Boolean::False => {
1431                    let ledger = &previous_state.next_epoch_data.ledger;
1432                    EpochLedger {
1433                        hash: ledger.hash,
1434                        total_currency: ledger.total_currency,
1435                    }
1436                }
1437            });
1438
1439            let start_checkpoint = w.exists_no_check(match epoch_increased {
1440                Boolean::True => prev_state_hash,
1441                Boolean::False => previous_state.next_epoch_data.start_checkpoint,
1442            });
1443
1444            let lock_checkpoint = {
1445                let base = w.exists_no_check(match epoch_increased {
1446                    Boolean::True => Fp::zero(),
1447                    Boolean::False => previous_state.next_epoch_data.lock_checkpoint,
1448                });
1449                w.exists_no_check(match in_seed_update_range {
1450                    Boolean::True => prev_state_hash,
1451                    Boolean::False => base,
1452                })
1453            };
1454
1455            EpochData {
1456                ledger,
1457                seed,
1458                start_checkpoint,
1459                lock_checkpoint,
1460                epoch_length: epoch_length.to_inner(), // TODO: Overflow ?
1461            }
1462        };
1463
1464        let blockchain_length = {
1465            let blockchain_length: &Length = &previous_state.blockchain_length;
1466            blockchain_length.to_checked::<Fp>().const_succ()
1467        };
1468
1469        let epoch_count = {
1470            let epoch_count: &Length = &previous_state.epoch_count;
1471            match epoch_increased {
1472                Boolean::True => epoch_count.to_checked::<Fp>().const_succ(),
1473                Boolean::False => epoch_count.to_checked(),
1474            }
1475        };
1476
1477        let (min_window_density, sub_window_densities) = update_min_window_density(
1478            UpdateMinWindowDensityParams {
1479                constants: &constants,
1480                prev_global_slot,
1481                next_global_slot: &next_global_slot,
1482                prev_sub_window_densities: previous_state
1483                    .sub_window_densities
1484                    .iter()
1485                    .map(|v| v.as_u32())
1486                    .collect(),
1487                prev_min_window_density: previous_state.min_window_density.as_u32(),
1488            },
1489            w,
1490        );
1491
1492        let state = CheckedConsensusState {
1493            blockchain_length,
1494            epoch_count,
1495            min_window_density,
1496            sub_window_densities,
1497            last_vrf_output: truncated_vrf_result,
1498            curr_global_slot_since_hard_fork: next_global_slot,
1499            global_slot_since_genesis,
1500            total_currency: new_total_currency,
1501            staking_epoch_data,
1502            next_epoch_data,
1503            has_ancestor_in_same_checkpoint_window,
1504            block_stake_winner,
1505            block_creator,
1506            coinbase_receiver,
1507            supercharge_coinbase,
1508        };
1509
1510        Ok((threshold_satisfied, state))
1511    }
1512}
1513
1514fn is_genesis_state_var(cs: &ConsensusState, w: &mut Witness<Fp>) -> Boolean {
1515    let consensus::GlobalSlot {
1516        slot_number,
1517        slots_per_epoch: _,
1518    } = cs.curr_global_slot_since_hard_fork;
1519
1520    CheckedSlot::zero().equal(&slot_number, w)
1521}
1522
1523fn is_genesis_state_var2(cs: &CheckedConsensusState, w: &mut Witness<Fp>) -> Boolean {
1524    let curr_global_slot = &cs.curr_global_slot_since_hard_fork;
1525    let slot_number = &curr_global_slot.slot_number;
1526
1527    CheckedSlot::zero().equal(slot_number, w)
1528}
1529
1530fn genesis_state_hash_checked(
1531    state_hash: Fp,
1532    state: &ProtocolState,
1533    w: &mut Witness<Fp>,
1534) -> anyhow::Result<Fp> {
1535    let is_genesis = is_genesis_state_var(&state.body.consensus_state, w);
1536
1537    Ok(w.exists_no_check(match is_genesis {
1538        Boolean::True => state_hash,
1539        Boolean::False => state.body.genesis_state_hash,
1540    }))
1541}
1542
1543#[derive(Debug, Clone)]
1544pub struct ProtocolStateBody<CS = ConsensusState> {
1545    pub genesis_state_hash: Fp,
1546    pub blockchain_state: BlockchainState,
1547    pub consensus_state: CS,
1548    pub constants: v2::MinaBaseProtocolConstantsCheckedValueStableV1,
1549}
1550
1551#[derive(Debug, Clone)]
1552pub struct ProtocolState<CS = ConsensusState> {
1553    pub previous_state_hash: Fp,
1554    pub body: ProtocolStateBody<CS>,
1555}
1556
1557impl ProtocolStateBody {
1558    pub fn view(&self) -> ProtocolStateView {
1559        let Self {
1560            genesis_state_hash: _,
1561            blockchain_state,
1562            consensus_state: cs,
1563            constants: _,
1564        } = self;
1565
1566        let sed = &cs.staking_epoch_data;
1567        let ned = &cs.next_epoch_data;
1568
1569        ProtocolStateView {
1570            // <https://github.com/MinaProtocol/mina/blob/436023ba41c43a50458a551b7ef7a9ae61670b25/src/lib/mina_state/blockchain_state.ml#L58>
1571            //
1572            snarked_ledger_hash: blockchain_state
1573                .ledger_proof_statement
1574                .target
1575                .first_pass_ledger,
1576            blockchain_length: cs.blockchain_length,
1577            min_window_density: cs.min_window_density,
1578            total_currency: cs.total_currency,
1579            global_slot_since_genesis: cs.global_slot_since_genesis,
1580            staking_epoch_data: sed.clone(),
1581            next_epoch_data: ned.clone(),
1582        }
1583    }
1584}
1585
1586fn protocol_create_var(
1587    previous_state_hash: Fp,
1588    genesis_state_hash: Fp,
1589    blockchain_state: &BlockchainState,
1590    consensus_state: &CheckedConsensusState,
1591    constants: &v2::MinaBaseProtocolConstantsCheckedValueStableV1,
1592) -> ProtocolState<CheckedConsensusState> {
1593    ProtocolState {
1594        previous_state_hash,
1595        body: ProtocolStateBody {
1596            genesis_state_hash,
1597            blockchain_state: blockchain_state.clone(),
1598            consensus_state: consensus_state.clone(),
1599            constants: constants.clone(),
1600        },
1601    }
1602}
1603
1604fn block_main<'a>(
1605    params: BlockMainParams<'a>,
1606    w: &mut Witness<Fp>,
1607) -> anyhow::Result<(Fp, [PreviousProofStatement<'a>; 2])> {
1608    let BlockMainParams {
1609        transition,
1610        prev_state,
1611        prev_state_proof,
1612        txn_snark,
1613        txn_snark_proof,
1614        next_state,
1615        prover_state,
1616        pending_coinbase,
1617    } = params;
1618
1619    let next_state: ProtocolState = next_state.try_into()?;
1620    let new_state_hash = w.exists(MinaHash::hash(&next_state));
1621    let transition: SnarkTransition = w.exists(transition.try_into()?);
1622    w.exists(txn_snark);
1623
1624    let prev_state: ProtocolState = w.exists(prev_state.try_into()?);
1625
1626    let (
1627        previous_state,
1628        previous_state_hash,
1629        previous_blockchain_proof_input, // TODO: Use hash here
1630        previous_state_body_hash,
1631    ) = {
1632        let (previous_state_hash, body) = checked_hash_protocol_state(&prev_state, w)?;
1633
1634        (&prev_state, previous_state_hash, &prev_state, body)
1635    };
1636
1637    let txn_stmt_ledger_hashes_didn_t_change = {
1638        let s1: &Statement<()> = &previous_state.body.blockchain_state.ledger_proof_statement;
1639        let s2: Statement<()> = txn_snark.clone().without_digest();
1640        txn_statement_ledger_hashes_equal(s1, &s2, w)
1641    };
1642
1643    let supply_increase = CheckedSigned::on_if(
1644        txn_stmt_ledger_hashes_didn_t_change.var(),
1645        SignedAmountBranchParam {
1646            on_true: &CheckedSigned::zero(),
1647            on_false: &txn_snark.supply_increase.to_checked(),
1648        },
1649        w,
1650    );
1651
1652    let (updated_consensus_state, consensus_state) = consensus::next_state_checked(
1653        previous_state,
1654        previous_state_hash,
1655        &transition,
1656        supply_increase,
1657        prover_state,
1658        w,
1659    )?;
1660
1661    let CheckedConsensusState {
1662        global_slot_since_genesis,
1663        coinbase_receiver,
1664        supercharge_coinbase,
1665        ..
1666    } = &consensus_state;
1667
1668    let prev_pending_coinbase_root = previous_state
1669        .body
1670        .blockchain_state
1671        .staged_ledger_hash
1672        .pending_coinbase_hash;
1673
1674    let genesis_state_hash = genesis_state_hash_checked(previous_state_hash, previous_state, w)?;
1675
1676    let (new_state, is_base_case) = {
1677        let mut t = protocol_create_var(
1678            previous_state_hash,
1679            genesis_state_hash,
1680            &transition.blockchain_state,
1681            &consensus_state,
1682            &previous_state.body.constants,
1683        );
1684        let is_base_case = CircuitVar::Var(is_genesis_state_var2(&t.body.consensus_state, w));
1685
1686        let previous_state_hash = match constraint_constants().fork.as_ref() {
1687            Some(ForkConstants {
1688                state_hash: fork_prev,
1689                ..
1690            }) => w.exists_no_check(match is_base_case.value() {
1691                Boolean::True => *fork_prev,
1692                Boolean::False => t.previous_state_hash,
1693            }),
1694            None => t.previous_state_hash,
1695        };
1696        t.previous_state_hash = previous_state_hash;
1697        checked_hash_protocol_state2(&t, w);
1698        (t, is_base_case)
1699    };
1700
1701    let (txn_snark_should_verify, success) = {
1702        let mut pending_coinbase = PendingCoinbaseWitness {
1703            is_new_stack: pending_coinbase.is_new_stack,
1704            pending_coinbase: (&pending_coinbase.pending_coinbases).try_into()?,
1705        };
1706
1707        let global_slot = global_slot_since_genesis;
1708
1709        let (new_pending_coinbase_hash, deleted_stack, no_coinbases_popped) = {
1710            let (root_after_delete, deleted_stack) = PendingCoinbase::pop_coinbases(
1711                txn_stmt_ledger_hashes_didn_t_change.neg(),
1712                &mut pending_coinbase,
1713                w,
1714            )?;
1715
1716            let no_coinbases_popped =
1717                field::equal(root_after_delete, prev_pending_coinbase_root, w);
1718
1719            let new_root = PendingCoinbase::add_coinbase_checked(
1720                &transition.pending_coinbase_update,
1721                coinbase_receiver,
1722                *supercharge_coinbase,
1723                previous_state_body_hash,
1724                global_slot,
1725                &mut pending_coinbase,
1726                w,
1727            )?;
1728
1729            (new_root, deleted_stack, no_coinbases_popped)
1730        };
1731
1732        let current_ledger_statement = &new_state.body.blockchain_state.ledger_proof_statement;
1733        let pending_coinbase_source_stack = Stack::var_create_with(&deleted_stack);
1734
1735        let txn_snark_input_correct = {
1736            fee_excess::assert_equal_checked(&FeeExcess::empty(), &txn_snark.fee_excess, w);
1737
1738            let previous_ledger_statement =
1739                &previous_state.body.blockchain_state.ledger_proof_statement;
1740
1741            let s1 = previous_ledger_statement;
1742            let s2 = current_ledger_statement;
1743
1744            let ledger_statement_valid = validate_ledgers_at_merge_checked(
1745                &StatementLedgers::of_statement(s1),
1746                &StatementLedgers::of_statement(s2),
1747                w,
1748            );
1749
1750            let a = txn_snark
1751                .source
1752                .pending_coinbase_stack
1753                .equal_var(&pending_coinbase_source_stack, w);
1754            let b = txn_snark
1755                .target
1756                .pending_coinbase_stack
1757                .equal_var(&deleted_stack, w);
1758
1759            Boolean::all(&[ledger_statement_valid, a, b], w)
1760        };
1761
1762        let nothing_changed = Boolean::all(
1763            &[txn_stmt_ledger_hashes_didn_t_change, no_coinbases_popped],
1764            w,
1765        );
1766
1767        let correct_coinbase_status = {
1768            let new_root = transition
1769                .blockchain_state
1770                .staged_ledger_hash
1771                .pending_coinbase_hash;
1772            field::equal(new_pending_coinbase_hash, new_root, w)
1773        };
1774
1775        Boolean::assert_any(&[txn_snark_input_correct, nothing_changed], w);
1776
1777        let transaction_snark_should_verifiy = CircuitVar::Var(nothing_changed.neg());
1778
1779        let result = Boolean::all(&[updated_consensus_state, correct_coinbase_status], w);
1780
1781        (transaction_snark_should_verifiy, result)
1782    };
1783
1784    let prev_should_verify = is_base_case.neg();
1785
1786    Boolean::assert_any(&[*is_base_case.value(), success], w);
1787
1788    let previous_proof_statements = [
1789        PreviousProofStatement {
1790            public_input: Rc::new(MinaHash::hash(previous_blockchain_proof_input)),
1791            proof: prev_state_proof,
1792            proof_must_verify: prev_should_verify,
1793        },
1794        PreviousProofStatement {
1795            public_input: Rc::new(txn_snark.clone()),
1796            proof: txn_snark_proof,
1797            proof_must_verify: txn_snark_should_verify,
1798        },
1799    ];
1800
1801    Ok((new_state_hash, previous_proof_statements))
1802}
1803
1804struct BlockMainParams<'a> {
1805    transition: &'a v2::MinaStateSnarkTransitionValueStableV2,
1806    prev_state: &'a v2::MinaStateProtocolStateValueStableV2,
1807    prev_state_proof: &'a v2::MinaBaseProofStableV2,
1808    txn_snark: &'a Statement<SokDigest>,
1809    txn_snark_proof: &'a v2::TransactionSnarkProofStableV2,
1810    next_state: &'a v2::MinaStateProtocolStateValueStableV2,
1811    prover_state: &'a v2::ConsensusStakeProofStableV2,
1812    pending_coinbase: &'a v2::MinaBasePendingCoinbaseWitnessStableV2,
1813}
1814
1815pub struct BlockParams<'a> {
1816    pub input: &'a v2::ProverExtendBlockchainInputStableV2,
1817    pub block_step_prover: &'a Prover<Fp>,
1818    pub block_wrap_prover: &'a Prover<Fq>,
1819    pub tx_wrap_prover: &'a Prover<Fq>,
1820    /// When set to `true`, `generate_block_proof` will not create a proof, but only
1821    /// verify constraints in the step witnesses
1822    pub only_verify_constraints: bool,
1823    /// For debugging only
1824    pub expected_step_proof: Option<&'static str>,
1825    /// For debugging only
1826    pub ocaml_wrap_witness: Option<Vec<Fq>>,
1827}
1828
1829const BLOCK_N_PREVIOUS_PROOFS: usize = 2;
1830
1831pub(super) fn generate_block_proof(
1832    params: BlockParams,
1833    w: &mut Witness<Fp>,
1834) -> anyhow::Result<WrapProof> {
1835    let BlockParams {
1836        input:
1837            v2::ProverExtendBlockchainInputStableV2 {
1838                chain,
1839                next_state,
1840                block,
1841                ledger_proof,
1842                prover_state,
1843                pending_coinbase,
1844            },
1845        block_step_prover,
1846        block_wrap_prover,
1847        tx_wrap_prover,
1848        only_verify_constraints,
1849        expected_step_proof,
1850        ocaml_wrap_witness,
1851    } = params;
1852
1853    let (txn_snark_statement, txn_snark_proof) =
1854        ledger_proof_opt(ledger_proof.as_deref(), next_state).context("ledger_proof_opt")?;
1855    let prev_state_proof = &chain.proof;
1856
1857    let (new_state_hash, previous_proof_statements) = block_main(
1858        BlockMainParams {
1859            transition: block,
1860            prev_state: &chain.state,
1861            prev_state_proof,
1862            txn_snark: &txn_snark_statement,
1863            txn_snark_proof: &txn_snark_proof,
1864            next_state,
1865            prover_state,
1866            pending_coinbase,
1867        },
1868        w,
1869    )
1870    .context("block_main")?;
1871
1872    let prev_challenge_polynomial_commitments =
1873        extract_recursion_challenges(&[prev_state_proof, &txn_snark_proof])
1874            .context("extract_recursion_challenges")?;
1875
1876    let rule = InductiveRule {
1877        previous_proof_statements,
1878        public_output: (),
1879        auxiliary_output: (),
1880    };
1881
1882    let dlog_plonk_index = super::merge::dlog_plonk_index(block_wrap_prover);
1883    let verifier_index = block_wrap_prover.index.verifier_index.as_ref().unwrap();
1884
1885    let tx_dlog_plonk_index = super::merge::dlog_plonk_index(tx_wrap_prover);
1886    let tx_verifier_index = tx_wrap_prover.index.verifier_index.as_ref().unwrap();
1887
1888    let dlog_plonk_index_cvar = dlog_plonk_index.to_cvar(CircuitVar::Var);
1889    let tx_dlog_plonk_index_cvar = tx_dlog_plonk_index.to_cvar(CircuitVar::Constant);
1890
1891    let indexes = [
1892        (verifier_index, &dlog_plonk_index_cvar),
1893        (tx_verifier_index, &tx_dlog_plonk_index_cvar),
1894    ];
1895
1896    let block_data = make_step_block_data(&dlog_plonk_index_cvar);
1897    let tx_data = make_step_transaction_data(&tx_dlog_plonk_index_cvar);
1898    let for_step_datas = [&block_data, &tx_data];
1899
1900    let app_state: Rc<dyn ToFieldElementsDebug> = Rc::new(new_state_hash);
1901
1902    let StepProof {
1903        statement,
1904        prev_evals,
1905        proof_with_public: proof,
1906    } = step::<StepBlockProof, BLOCK_N_PREVIOUS_PROOFS>(
1907        StepParams {
1908            app_state: Rc::clone(&app_state),
1909            rule,
1910            for_step_datas,
1911            indexes,
1912            prev_challenge_polynomial_commitments,
1913            hack_feature_flags: OptFlag::No,
1914            wrap_prover: block_wrap_prover,
1915            step_prover: block_step_prover,
1916            only_verify_constraints,
1917        },
1918        w,
1919    )
1920    .context("step")?;
1921
1922    if let Some(expected) = expected_step_proof {
1923        let proof_json = serde_json::to_vec(&proof.proof).unwrap();
1924        assert_eq!(sha256_sum(&proof_json), expected);
1925    };
1926
1927    let mut w = Witness::new::<WrapBlockProof>();
1928
1929    if let Some(ocaml_aux) = ocaml_wrap_witness {
1930        w.ocaml_aux = ocaml_aux;
1931    };
1932
1933    wrap::<WrapBlockProof>(
1934        WrapParams {
1935            app_state,
1936            proof_with_public: &proof,
1937            step_statement: statement,
1938            prev_evals: &prev_evals,
1939            dlog_plonk_index: &dlog_plonk_index,
1940            step_prover_index: &block_step_prover.index,
1941            wrap_prover: block_wrap_prover,
1942        },
1943        &mut w,
1944    )
1945    .context("wrap")
1946}