mina_tree/proofs/numbers/
nat.rs

1use mina_curves::pasta::Fp;
2
3use crate::{
4    proofs::{
5        block::consensus::ConsensusConstantsChecked,
6        field::{field, Boolean, FieldWitness},
7        to_field_elements::ToFieldElements,
8        transaction::Check,
9        witness::Witness,
10    },
11    scan_state::currency::{
12        BlockTime, BlockTimeSpan, Index, Length, Magnitude, MinMax, Nonce, Slot, SlotSpan,
13        TxnVersion,
14    },
15    ToInputs,
16};
17
18use super::common::{range_check, range_check_flag, ForZkappCheck};
19
20pub trait CheckedNat<F: FieldWitness, const NBITS: usize>:
21    Sized + ToFieldElements<F> + Check<F> + Clone
22{
23    type Inner: MinMax + Magnitude;
24
25    fn to_field(&self) -> F;
26    fn from_field(field: F) -> Self;
27
28    fn zero() -> Self {
29        Self::from_field(F::zero())
30    }
31
32    fn one() -> Self {
33        Self::from_field(F::one())
34    }
35
36    fn to_inner(&self) -> Self::Inner {
37        Self::Inner::of_field(self.to_field())
38    }
39
40    fn from_inner(inner: Self::Inner) -> Self {
41        Self::from_field(inner.to_field())
42    }
43
44    /// >=
45    /// > greater than or equal
46    fn gte(&self, other: &Self, w: &mut Witness<F>) -> Boolean {
47        let (x, y) = (self.to_field(), other.to_field());
48
49        let xy = w.exists(x - y);
50        let yx = w.exists(xy.neg());
51
52        let x_gte_y = range_check_flag::<F, NBITS>(xy, w);
53        let y_gte_x = range_check_flag::<F, NBITS>(yx, w);
54
55        Boolean::assert_any(&[x_gte_y, y_gte_x], w);
56        x_gte_y
57    }
58
59    /// <=
60    /// less than or equal
61    fn lte(&self, other: &Self, w: &mut Witness<F>) -> Boolean {
62        other.gte(self, w)
63    }
64
65    /// <
66    /// less than
67    fn less_than(&self, other: &Self, w: &mut Witness<F>) -> Boolean {
68        let is_equal = field::equal(other.to_field(), self.to_field(), w);
69        other.gte(self, w).and(&is_equal.neg(), w)
70    }
71
72    /// TODO: Remove this
73    fn const_gte(&self, other: &Self, w: &mut Witness<F>) -> Boolean {
74        let (x, y) = (self.to_field(), other.to_field());
75
76        let xy = x - y;
77        let yx = w.exists(xy.neg());
78
79        let x_gte_y = range_check_flag::<F, NBITS>(xy, w);
80        let y_gte_x = range_check_flag::<F, NBITS>(yx, w);
81
82        Boolean::assert_any(&[x_gte_y, y_gte_x], w);
83        x_gte_y
84    }
85
86    fn const_less_than(&self, other: &Self, w: &mut Witness<F>) -> Boolean {
87        let is_equal = field::equal(other.to_field(), self.to_field(), w);
88        other.const_gte(self, w).and(&is_equal.neg(), w)
89    }
90
91    /// >
92    /// greater than
93    fn greater_than(&self, other: &Self, w: &mut Witness<F>) -> Boolean {
94        other.less_than(self, w)
95    }
96
97    fn const_greater_than(&self, other: &Self, w: &mut Witness<F>) -> Boolean {
98        other.const_less_than(self, w)
99    }
100
101    fn equal(&self, other: &Self, w: &mut Witness<F>) -> Boolean {
102        field::equal(self.to_field(), other.to_field(), w)
103    }
104
105    fn subtract_unpacking_or_zero(&self, y: &Self, w: &mut Witness<F>) -> (Boolean, Self) {
106        let x = self.to_field();
107        let y = y.to_field();
108
109        let res = w.exists(x - y);
110        let neg_res = w.exists(res.neg());
111
112        let x_gte_y = range_check_flag::<F, NBITS>(res, w);
113        let y_gte_x = range_check_flag::<F, NBITS>(neg_res, w);
114
115        Boolean::assert_any(&[x_gte_y, y_gte_x], w);
116
117        let is_equal = field::equal(x, y, w);
118        let underflow = y_gte_x.and(&is_equal.neg(), w);
119
120        let value = w.exists(match underflow {
121            Boolean::True => F::zero(),
122            Boolean::False => res,
123        });
124
125        (underflow, Self::from_field(value))
126    }
127
128    /// Returns (is_underflow, value)
129    fn sub_or_zero(&self, y: &Self, w: &mut Witness<F>) -> (Boolean, Self) {
130        self.subtract_unpacking_or_zero(y, w)
131    }
132
133    /// (div, remainder)
134    fn div_mod(&self, y: &Self, w: &mut Witness<F>) -> (Self, Self) {
135        let x = self.to_inner();
136        let y = y.to_inner();
137
138        let div = x.checked_div(&y).unwrap();
139        let rem = x.checked_rem(&y).unwrap();
140
141        w.exists((Self::from_inner(div), Self::from_inner(rem)))
142    }
143
144    fn add(&self, y: &Self, w: &mut Witness<F>) -> Self {
145        let res = field::add(self.to_field(), y.to_field(), w);
146        range_check::<F, NBITS>(res, w);
147        Self::from_field(res)
148    }
149
150    fn const_add(&self, y: &Self, w: &mut Witness<F>) -> Self {
151        let res = self.to_field() + y.to_field();
152        range_check::<F, NBITS>(res, w);
153        Self::from_field(res)
154    }
155
156    fn mul(&self, y: &Self, w: &mut Witness<F>) -> Self {
157        let res = field::mul(self.to_field(), y.to_field(), w);
158        range_check::<F, NBITS>(res, w);
159        Self::from_field(res)
160    }
161
162    fn const_mul(&self, y: &Self, w: &mut Witness<F>) -> Self {
163        let res = self.to_field() * y.to_field();
164        range_check::<F, NBITS>(res, w);
165        Self::from_field(res)
166    }
167
168    fn min(&self, b: &Self, w: &mut Witness<F>) -> Self {
169        let a_lte_b = self.lte(b, w);
170        w.exists_no_check(match a_lte_b {
171            Boolean::True => self.clone(),
172            Boolean::False => b.clone(),
173        })
174    }
175
176    fn succ(&self) -> Self {
177        let this = self.to_field();
178        Self::from_field(this + F::one())
179    }
180}
181
182impl<F: FieldWitness> CheckedSlot<F> {
183    pub fn diff_or_zero(&self, t2: &Self, w: &mut Witness<F>) -> (Boolean, CheckedSlotSpan<F>) {
184        let t1 = self;
185        let (is_underflow, diff) = Self::sub_or_zero(t1, t2, w);
186        (is_underflow, CheckedSlotSpan(diff.0))
187    }
188
189    pub fn diff(&self, t2: &Self, w: &mut Witness<F>) -> CheckedSlotSpan<F> {
190        let diff = field::sub(self.to_field(), t2.to_field(), w);
191        range_check::<F, 32>(diff, w);
192        CheckedSlotSpan::from_field(diff)
193    }
194
195    pub fn to_length(&self) -> CheckedLength<F> {
196        CheckedLength::from_field(self.to_field())
197    }
198}
199
200impl CheckedSlot<Fp> {
201    pub fn in_seed_update_range(
202        &self,
203        constants: &ConsensusConstantsChecked,
204        w: &mut Witness<Fp>,
205    ) -> Boolean {
206        // constant
207        let c = |n: u32| Length::from_u32(n).to_checked();
208        let third_epoch = {
209            let (q, _r) = constants.slots_per_epoch.div_mod(&c(3), w);
210            q
211        };
212        let ck_times_2 = third_epoch.const_mul(&c(2), w);
213        // let ck_times_2 = third_epoch.mul(&c(2), w);
214        self.to_length().less_than(&ck_times_2, w)
215    }
216}
217
218impl<F: FieldWitness> CheckedLength<F> {
219    pub fn to_slot(&self) -> CheckedSlot<F> {
220        CheckedSlot::from_field(self.to_field())
221    }
222
223    pub fn const_succ(&self) -> Self {
224        Self(self.0 + F::one())
225    }
226}
227
228macro_rules! impl_nat {
229    ($({$name:tt, $unchecked:tt}),*) => ($(
230
231        #[derive(Copy, Clone, Debug)]
232        pub struct $name<F: FieldWitness>(F);
233
234        impl<F: FieldWitness> CheckedNat<F, 32> for $name::<F> {
235            type Inner = $unchecked;
236            fn to_field(&self) -> F {
237                self.0
238            }
239            fn from_field(field: F) -> Self {
240                Self(field)
241            }
242        }
243
244        impl<F: FieldWitness> ToFieldElements<F> for $name::<F> {
245            fn to_field_elements(&self, fields: &mut Vec<F>) {
246                let Self(this) = self;
247                this.to_field_elements(fields)
248            }
249        }
250
251        impl<F: FieldWitness> Check<F> for $name::<F> {
252            fn check(&self, w: &mut Witness<F>) {
253                range_check::<F, { 32 }>(self.0, w);
254            }
255        }
256
257        impl<F: FieldWitness> ToInputs for $name<F> {
258            fn to_inputs(&self, inputs: &mut ::poseidon::hash::Inputs) {
259                self.to_inner().to_inputs(inputs)
260            }
261        }
262
263        impl $unchecked {
264            pub fn to_checked<F: FieldWitness>(&self) -> $name<F> {
265                $name::from_inner(*self)
266            }
267        }
268
269        impl<F: FieldWitness> ForZkappCheck<F> for $unchecked {
270            type CheckedType = $name<F>;
271            fn checked_from_field(field: F) -> Self::CheckedType {
272                Self::CheckedType::from_field(field)
273            }
274            fn lte(this: &Self::CheckedType, other: &Self::CheckedType, w: &mut Witness<F>) -> Boolean {
275                Self::CheckedType::lte(this, other, w)
276            }
277        }
278    )*)
279}
280
281impl_nat!(
282    {CheckedTxnVersion, TxnVersion},
283    {CheckedSlot, Slot},
284    {CheckedSlotSpan, SlotSpan},
285    {CheckedLength, Length},
286    {CheckedNonce, Nonce},
287    {CheckedIndex, Index},
288    {CheckedBlockTime, BlockTime},
289    {CheckedBlockTimeSpan, BlockTimeSpan}
290);
291
292/// A generic 64 bits checked number
293#[derive(Clone, Debug)]
294pub struct CheckedN<F: FieldWitness>(F);
295
296impl<F: FieldWitness> CheckedNat<F, 64> for CheckedN<F> {
297    type Inner = crate::scan_state::currency::N;
298    fn to_field(&self) -> F {
299        self.0
300    }
301    fn from_field(field: F) -> Self {
302        Self(field)
303    }
304}
305
306impl<F: FieldWitness> ToFieldElements<F> for CheckedN<F> {
307    fn to_field_elements(&self, fields: &mut Vec<F>) {
308        let Self(this) = self;
309        this.to_field_elements(fields)
310    }
311}
312
313impl<F: FieldWitness> Check<F> for CheckedN<F> {
314    fn check(&self, w: &mut Witness<F>) {
315        range_check::<F, 64>(self.0, w);
316    }
317}
318
319/// A generic 32 bits checked number
320#[derive(Clone, Debug)]
321pub struct CheckedN32<F: FieldWitness>(F);
322
323impl<F: FieldWitness> CheckedNat<F, 32> for CheckedN32<F> {
324    type Inner = crate::scan_state::currency::N;
325    fn to_field(&self) -> F {
326        self.0
327    }
328    fn from_field(field: F) -> Self {
329        Self(field)
330    }
331}
332
333impl<F: FieldWitness> ToFieldElements<F> for CheckedN32<F> {
334    fn to_field_elements(&self, fields: &mut Vec<F>) {
335        let Self(this) = self;
336        this.to_field_elements(fields)
337    }
338}
339
340impl<F: FieldWitness> Check<F> for CheckedN32<F> {
341    fn check(&self, w: &mut Witness<F>) {
342        range_check::<F, 32>(self.0, w);
343    }
344}
345
346impl<F: FieldWitness> CheckedN32<F> {
347    pub fn constant(n: usize) -> Self {
348        let n: u32 = n.try_into().unwrap();
349        Self::from_field(n.into())
350    }
351}
mina_tree/proofs/numbers/nat.rs

mina_tree/proofs/numbers/
nat.rs
