mina_tree/proofs/
block.rs

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