Skip to main content

mina_tree/proofs/
field.rs

1use ark_ec::{short_weierstrass::Projective, AffineRepr, CurveGroup};
2use ark_ff::{BigInteger256, FftField, Field, PrimeField};
3use kimchi::curve::KimchiCurve;
4use mina_curves::pasta::{
5    fields::fft::FpParameters as _, Fp, Fq, PallasParameters, ProjectivePallas, ProjectiveVesta,
6    VestaParameters,
7};
8use mina_poseidon::{
9    constants::PlonkSpongeConstantsKimchi, pasta::FULL_ROUNDS, sponge::DefaultFqSponge,
10};
11
12use poseidon::SpongeParamsForField;
13
14use crate::proofs;
15
16use super::{
17    public_input::plonk_checks::{self, ShiftedValue},
18    to_field_elements::ToFieldElements,
19    transaction::Check,
20    witness::Witness,
21    BACKEND_TICK_ROUNDS_N, BACKEND_TOCK_ROUNDS_N,
22};
23
24pub type GroupAffine<F> = ark_ec::short_weierstrass::Affine<<F as FieldWitness>::Parameters>;
25
26/// All the generics we need during witness generation
27pub trait FieldWitness
28where
29    Self: Field
30        + Send
31        + Sync
32        + Into<BigInteger256>
33        + From<BigInteger256>
34        + Into<mina_p2p_messages::bigint::BigInt>
35        + From<i64>
36        + From<i32>
37        + ToFieldElements<Self>
38        + Check<Self>
39        + FromFpFq
40        + PrimeField
41        + FftField
42        + SpongeParamsForField<Self>
43        + std::fmt::Debug
44        + 'static,
45{
46    type Scalar: FieldWitness<Scalar = Self>;
47    type Affine: AffineRepr<
48            Group = Self::Projective,
49            BaseField = Self,
50            ScalarField = <Self as proofs::field::FieldWitness>::Scalar,
51        > + Into<GroupAffine<Self>>
52        + KimchiCurve<FULL_ROUNDS>
53        + std::fmt::Debug;
54    type Projective: CurveGroup<
55            Affine = Self::Affine,
56            BaseField = Self,
57            ScalarField = <Self as proofs::field::FieldWitness>::Scalar,
58        > + From<Projective<Self::Parameters>>
59        + std::fmt::Debug;
60    type Parameters: ark_ec::short_weierstrass::SWCurveConfig<
61            BaseField = Self,
62            ScalarField = <Self as proofs::field::FieldWitness>::Scalar,
63        > + Clone
64        + std::fmt::Debug;
65    type Shifting: plonk_checks::ShiftingValue<Self> + Clone + std::fmt::Debug;
66    type OtherCurve: KimchiCurve<
67        FULL_ROUNDS,
68        ScalarField = Self,
69        BaseField = <Self as proofs::field::FieldWitness>::Scalar,
70    >;
71    type FqSponge: Clone
72        + mina_poseidon::FqSponge<
73            <Self as proofs::field::FieldWitness>::Scalar,
74            Self::OtherCurve,
75            Self,
76            FULL_ROUNDS,
77        >;
78
79    const PARAMS: Params<Self>;
80    const SIZE: BigInteger256;
81    const NROUNDS: usize;
82    const SRS_DEPTH: usize;
83}
84
85pub struct Params<F> {
86    pub a: F,
87    pub b: F,
88}
89
90impl FieldWitness for Fp {
91    type Scalar = Fq;
92    type Parameters = PallasParameters;
93    type Affine = GroupAffine<Self>;
94    type Projective = ProjectivePallas;
95    type Shifting = ShiftedValue<Fp>;
96    type OtherCurve = GroupAffine<Fq>;
97    type FqSponge = DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi, FULL_ROUNDS>;
98
99    /// <https://github.com/openmina/mina/blob/46b6403cb7f158b66a60fc472da2db043ace2910/src/lib/crypto/kimchi_backend/pasta/basic/kimchi_pasta_basic.ml#L107>
100    const PARAMS: Params<Self> = Params::<Self> {
101        a: ark_ff::MontFp!("0"),
102        b: ark_ff::MontFp!("5"),
103    };
104    const SIZE: BigInteger256 = mina_curves::pasta::fields::FpParameters::MODULUS;
105    const NROUNDS: usize = BACKEND_TICK_ROUNDS_N;
106    const SRS_DEPTH: usize = 32768;
107}
108
109impl FieldWitness for Fq {
110    type Scalar = Fp;
111    type Parameters = VestaParameters;
112    type Affine = GroupAffine<Self>;
113    type Projective = ProjectiveVesta;
114    type Shifting = ShiftedValue<Fq>;
115    type OtherCurve = GroupAffine<Fp>;
116    type FqSponge = DefaultFqSponge<PallasParameters, PlonkSpongeConstantsKimchi, FULL_ROUNDS>;
117
118    /// <https://github.com/openmina/mina/blob/46b6403cb7f158b66a60fc472da2db043ace2910/src/lib/crypto/kimchi_backend/pasta/basic/kimchi_pasta_basic.ml#L95>
119    const PARAMS: Params<Self> = Params::<Self> {
120        a: ark_ff::MontFp!("0"),
121        b: ark_ff::MontFp!("5"),
122    };
123    const SIZE: BigInteger256 = mina_curves::pasta::fields::FqParameters::MODULUS;
124    const NROUNDS: usize = BACKEND_TOCK_ROUNDS_N;
125    const SRS_DEPTH: usize = 65536;
126}
127
128/// Trait helping converting generics into concrete types
129pub trait FromFpFq {
130    fn from_fp(fp: Fp) -> Self;
131    fn from_fq(fp: Fq) -> Self;
132}
133
134impl FromFpFq for Fp {
135    fn from_fp(fp: Fp) -> Self {
136        fp
137    }
138    fn from_fq(_fq: Fq) -> Self {
139        // `Fq` cannot be converted into `Fp`.
140        // Caller must first split `Fq` into 2 parts (high & low bits)
141        // See `impl<F: FieldWitness> ToFieldElements<F> for Fq`
142        panic!("Attempt to convert a `Fq` into `Fp`")
143    }
144}
145
146impl FromFpFq for Fq {
147    fn from_fp(fp: Fp) -> Self {
148        // `Fp` is smaller than `Fq`, so the conversion is fine
149        let bigint: BigInteger256 = fp.into();
150        Self::from(bigint)
151    }
152    fn from_fq(fq: Fq) -> Self {
153        fq
154    }
155}
156
157/// Trait helping converting concrete types into generics
158pub trait IntoGeneric<F: FieldWitness> {
159    fn into_gen(self) -> F;
160}
161
162impl<F: FieldWitness> IntoGeneric<F> for Fp {
163    fn into_gen(self) -> F {
164        F::from_fp(self)
165    }
166}
167
168impl<F: FieldWitness> IntoGeneric<F> for Fq {
169    fn into_gen(self) -> F {
170        F::from_fq(self)
171    }
172}
173
174#[allow(clippy::module_inception)]
175pub mod field {
176    use crate::proofs::transaction::field_to_bits2;
177
178    use super::*;
179
180    // <https://github.com/o1-labs/snarky/blob/7edf13628872081fd7cad154de257dad8b9ba621/src/base/utils.ml#L99>
181    pub fn square<F>(field: F, w: &mut Witness<F>) -> F
182    where
183        F: FieldWitness,
184    {
185        w.exists(field.square())
186        // TODO: Rest of the function doesn't modify witness
187    }
188
189    pub fn mul<F>(x: F, y: F, w: &mut Witness<F>) -> F
190    where
191        F: FieldWitness,
192    {
193        w.exists(x * y)
194    }
195
196    pub fn const_mul<F>(x: F, y: F) -> F
197    where
198        F: FieldWitness,
199    {
200        x * y
201    }
202
203    pub fn muls<F>(xs: &[F], w: &mut Witness<F>) -> F
204    where
205        F: FieldWitness,
206    {
207        xs.iter()
208            .copied()
209            .reduce(|acc, v| w.exists(acc * v))
210            .expect("invalid param")
211    }
212
213    pub fn div<F>(x: F, y: F, w: &mut Witness<F>) -> F
214    where
215        F: FieldWitness,
216    {
217        w.exists(x / y)
218    }
219
220    // TODO: Do we need `div` above ?
221    pub fn div_by_inv<F>(x: F, y: F, w: &mut Witness<F>) -> F
222    where
223        F: FieldWitness,
224    {
225        let y_inv = w.exists(y.inverse().unwrap_or_else(F::zero));
226        mul(x, y_inv, w)
227    }
228
229    pub fn sub<F>(x: F, y: F, w: &mut Witness<F>) -> F
230    where
231        F: FieldWitness,
232    {
233        w.exists(x - y)
234    }
235
236    pub fn add<F>(x: F, y: F, w: &mut Witness<F>) -> F
237    where
238        F: FieldWitness,
239    {
240        w.exists(x + y)
241    }
242
243    pub fn const_add<F>(x: F, y: F) -> F
244    where
245        F: FieldWitness,
246    {
247        x + y
248    }
249
250    pub fn equal<F: FieldWitness>(x: F, y: F, w: &mut Witness<F>) -> Boolean {
251        let z = x - y;
252
253        let (boolean, r, inv) = if x == y {
254            (Boolean::True, F::one(), F::zero())
255        } else {
256            (Boolean::False, F::zero(), z.inverse().unwrap())
257        };
258        w.exists([r, inv]);
259
260        boolean
261    }
262
263    pub fn compare<F: FieldWitness>(
264        bit_length: u64,
265        a: F,
266        b: F,
267        w: &mut Witness<F>,
268    ) -> (Boolean, Boolean) {
269        let two_to_the = |n: usize| (0..n).fold(F::one(), |acc, _| acc.double());
270
271        let bit_length = bit_length as usize;
272        let alpha_packed = { two_to_the(bit_length) + b - a };
273        let alpha = w.exists(field_to_bits2(alpha_packed, bit_length + 1));
274        let (less_or_equal, prefix) = alpha.split_last().unwrap();
275
276        let less_or_equal = less_or_equal.to_boolean();
277        let prefix = prefix.iter().map(|b| b.to_boolean()).collect::<Vec<_>>();
278
279        let not_all_zeros = Boolean::any(&prefix, w);
280        let less = less_or_equal.and(&not_all_zeros, w);
281
282        (less, less_or_equal)
283    }
284
285    pub fn assert_lt<F: FieldWitness>(bit_length: u64, x: F, y: F, w: &mut Witness<F>) {
286        compare(bit_length, x, y, w);
287    }
288}
289
290pub trait ToBoolean {
291    fn to_boolean(&self) -> Boolean;
292}
293
294impl ToBoolean for bool {
295    fn to_boolean(&self) -> Boolean {
296        if *self {
297            Boolean::True
298        } else {
299            Boolean::False
300        }
301    }
302}
303
304#[derive(Clone, Copy, Debug, PartialEq, Eq)]
305pub enum Boolean {
306    True = 1,
307    False = 0,
308}
309
310impl Boolean {
311    pub fn of_field<F: FieldWitness>(field: F) -> Self {
312        if field.is_zero() {
313            Self::False
314        } else {
315            Self::True
316        }
317    }
318
319    pub fn as_bool(&self) -> bool {
320        match self {
321            Boolean::True => true,
322            Boolean::False => false,
323        }
324    }
325
326    pub fn neg(&self) -> Self {
327        match self {
328            Boolean::False => Boolean::True,
329            Boolean::True => Boolean::False,
330        }
331    }
332
333    pub fn to_field<F: FieldWitness>(self) -> F {
334        F::from(self.as_bool())
335    }
336
337    fn mul<F: FieldWitness>(&self, other: &Self, w: &mut Witness<F>) -> Self {
338        let result: F = self.to_field::<F>() * other.to_field::<F>();
339        w.exists(result);
340        if result.is_zero() {
341            Self::False
342        } else {
343            assert_eq!(result, F::one());
344            Self::True
345        }
346    }
347
348    pub fn and<F: FieldWitness>(&self, other: &Self, w: &mut Witness<F>) -> Self {
349        self.mul(other, w)
350    }
351
352    /// Same as `Self::and` but doesn't push values to the witness
353    pub fn const_and(&self, other: &Self) -> Self {
354        (self.as_bool() && other.as_bool()).to_boolean()
355    }
356
357    pub fn or<F: FieldWitness>(&self, other: &Self, w: &mut Witness<F>) -> Self {
358        let both_false = self.neg().and(&other.neg(), w);
359        both_false.neg()
360    }
361
362    /// Same as `Self::or` but doesn't push values to the witness
363    pub fn const_or(&self, other: &Self) -> Self {
364        (self.as_bool() || other.as_bool()).to_boolean()
365    }
366
367    pub fn all<F: FieldWitness>(x: &[Self], w: &mut Witness<F>) -> Self {
368        match x {
369            [] => Self::True,
370            [b1] => *b1,
371            [b1, b2] => b1.and(b2, w),
372            bs => {
373                let len = F::from(bs.len() as u64);
374                let sum = bs.iter().fold(0u64, |acc, b| {
375                    acc + match b {
376                        Boolean::True => 1,
377                        Boolean::False => 0,
378                    }
379                });
380                field::equal(len, F::from(sum), w)
381            }
382        }
383    }
384
385    pub fn const_all<F: FieldWitness>(x: &[Self]) -> Self {
386        match x {
387            [] => Self::True,
388            [b1] => *b1,
389            [b1, b2] => b1.const_and(b2),
390            bs => {
391                let len = F::from(bs.len() as u64);
392                let sum = bs.iter().fold(0u64, |acc, b| {
393                    acc + match b {
394                        Boolean::True => 1,
395                        Boolean::False => 0,
396                    }
397                });
398                (len == F::from(sum)).to_boolean()
399            }
400        }
401    }
402
403    // For non-constant
404    pub fn lxor<F: FieldWitness>(&self, other: &Self, w: &mut Witness<F>) -> Self {
405        let result = (self.as_bool() ^ other.as_bool()).to_boolean();
406        w.exists(result.to_field::<F>());
407        result
408    }
409
410    pub fn const_lxor(&self, other: &Self) -> Self {
411        (self.as_bool() ^ other.as_bool()).to_boolean()
412    }
413
414    pub fn equal<F: FieldWitness>(&self, other: &Self, w: &mut Witness<F>) -> Self {
415        self.lxor(other, w).neg()
416    }
417
418    pub fn const_equal(&self, other: &Self) -> Self {
419        (self.as_bool() == other.as_bool()).to_boolean()
420    }
421
422    pub fn const_any<F: FieldWitness>(x: &[Self]) -> Self {
423        match x {
424            [] => Self::False,
425            [b1] => *b1,
426            [b1, b2] => b1.const_or(b2),
427            bs => {
428                let sum = bs.iter().fold(0u64, |acc, b| {
429                    acc + match b {
430                        Boolean::True => 1,
431                        Boolean::False => 0,
432                    }
433                });
434                (F::from(sum) == F::zero()).to_boolean().neg()
435            }
436        }
437    }
438
439    pub fn any<F: FieldWitness>(x: &[Self], w: &mut Witness<F>) -> Self {
440        match x {
441            [] => Self::False,
442            [b1] => *b1,
443            [b1, b2] => b1.or(b2, w),
444            bs => {
445                let sum = bs.iter().fold(0u64, |acc, b| {
446                    acc + match b {
447                        Boolean::True => 1,
448                        Boolean::False => 0,
449                    }
450                });
451                field::equal(F::from(sum), F::zero(), w).neg()
452            }
453        }
454    }
455
456    // Part of utils.inv
457    pub fn assert_non_zero<F: FieldWitness>(v: F, w: &mut Witness<F>) {
458        if v.is_zero() {
459            w.exists(v);
460        } else {
461            w.exists(v.inverse().unwrap());
462        }
463    }
464
465    pub fn assert_any<F: FieldWitness>(bs: &[Self], w: &mut Witness<F>) {
466        let num_true = bs.iter().fold(0u64, |acc, b| {
467            acc + match b {
468                Boolean::True => 1,
469                Boolean::False => 0,
470            }
471        });
472        Self::assert_non_zero::<F>(F::from(num_true), w)
473    }
474
475    pub fn var(&self) -> CircuitVar<Boolean> {
476        CircuitVar::Var(*self)
477    }
478
479    pub fn constant(&self) -> CircuitVar<Boolean> {
480        CircuitVar::Constant(*self)
481    }
482}
483
484impl<F: FieldWitness> Check<F> for Boolean {
485    fn check(&self, _w: &mut Witness<F>) {
486        // Does not modify the witness
487    }
488}
489
490impl<F: FieldWitness> Check<F> for CircuitVar<Boolean> {
491    fn check(&self, _w: &mut Witness<F>) {
492        // Does not modify the witness
493    }
494}
495
496/// Our implementation of cvars (compare to OCaml) is incomplete, but sufficient
497/// for now (for witness generation).
498/// It's also sometimes not used correctly (`CircuitVar<GroupAffine<F>>` should be
499/// `GroupAffine<CircuitVar<F>>` instead)
500///
501/// Note that our implementation of `CircuitVar<Boolean>` is complete.
502#[derive(Clone, Copy, Debug)]
503pub enum CircuitVar<F> {
504    Var(F),
505    Constant(F),
506}
507
508impl<F: FieldWitness> CircuitVar<F> {
509    pub fn as_field(&self) -> F {
510        match self {
511            CircuitVar::Var(f) => *f,
512            CircuitVar::Constant(f) => *f,
513        }
514    }
515
516    fn scale(x: CircuitVar<F>, s: F) -> CircuitVar<F> {
517        use CircuitVar::*;
518
519        if s.is_zero() {
520            Constant(F::zero())
521        } else if s.is_one() {
522            x
523        } else {
524            match x {
525                Constant(x) => Constant(x * s),
526                Var(x) => Var(x * s),
527            }
528        }
529    }
530
531    fn mul(&self, other: &Self, w: &mut Witness<F>) -> CircuitVar<F> {
532        use CircuitVar::*;
533
534        let (x, y) = (*self, *other);
535        match (x, y) {
536            (Constant(x), Constant(y)) => Constant(x * y),
537            (Constant(x), _) => Self::scale(y, x),
538            (_, Constant(y)) => Self::scale(x, y),
539            (Var(x), Var(y)) => Var(w.exists(x * y)),
540        }
541    }
542
543    fn equal(x: &Self, y: &Self, w: &mut Witness<F>) -> CircuitVar<Boolean> {
544        match (x, y) {
545            (CircuitVar::Constant(x), CircuitVar::Constant(y)) => {
546                let eq = if x == y {
547                    Boolean::True
548                } else {
549                    Boolean::False
550                };
551                CircuitVar::Constant(eq)
552            }
553            _ => {
554                let x = x.as_field();
555                let y = y.as_field();
556                CircuitVar::Var(field::equal(x, y, w))
557            }
558        }
559    }
560}
561
562impl<T> CircuitVar<T> {
563    pub fn is_const(&self) -> bool {
564        match self {
565            CircuitVar::Var(_) => false,
566            CircuitVar::Constant(_) => true,
567        }
568    }
569
570    pub fn value(&self) -> &T {
571        match self {
572            CircuitVar::Var(v) => v,
573            CircuitVar::Constant(v) => v,
574        }
575    }
576
577    pub fn map<Fun, V>(&self, fun: Fun) -> CircuitVar<V>
578    where
579        Fun: Fn(&T) -> V,
580    {
581        match self {
582            CircuitVar::Var(v) => CircuitVar::Var(fun(v)),
583            CircuitVar::Constant(v) => CircuitVar::Constant(fun(v)),
584        }
585    }
586}
587
588impl CircuitVar<Boolean> {
589    pub fn as_boolean(&self) -> Boolean {
590        match self {
591            CircuitVar::Var(b) => *b,
592            CircuitVar::Constant(b) => *b,
593        }
594    }
595
596    fn as_cvar<F: FieldWitness>(&self) -> CircuitVar<F> {
597        self.map(|b| b.to_field::<F>())
598    }
599
600    pub fn of_cvar<F: FieldWitness>(cvar: CircuitVar<F>) -> Self {
601        cvar.map(|b| {
602            // TODO: Should we check for `is_one` or `is_zero` here ? To match OCaml behavior
603            if b.is_one() {
604                Boolean::True
605            } else {
606                Boolean::False
607            }
608        })
609    }
610
611    pub fn and<F: FieldWitness>(&self, other: &Self, w: &mut Witness<F>) -> Self {
612        self.as_cvar().mul(&other.as_cvar(), w).map(|v| {
613            // TODO: Should we check for `is_one` or `is_zero` here ? To match OCaml behavior
614            if v.is_one() {
615                Boolean::True
616            } else {
617                Boolean::False
618            }
619        })
620    }
621
622    fn boolean_sum<F: FieldWitness>(x: &[Self]) -> CircuitVar<F> {
623        let sum = x.iter().fold(0u64, |acc, b| {
624            acc + match b.as_boolean() {
625                Boolean::True => 1,
626                Boolean::False => 0,
627            }
628        });
629        if x.iter().all(|x| matches!(x, CircuitVar::Constant(_))) {
630            CircuitVar::Constant(F::from(sum))
631        } else {
632            CircuitVar::Var(F::from(sum))
633        }
634    }
635
636    pub fn any<F: FieldWitness>(x: &[Self], w: &mut Witness<F>) -> CircuitVar<Boolean> {
637        match x {
638            [] => CircuitVar::Constant(Boolean::False),
639            [b1] => *b1,
640            [b1, b2] => b1.or(b2, w),
641            bs => {
642                let sum = Self::boolean_sum(bs);
643                CircuitVar::equal(&sum, &CircuitVar::Constant(F::zero()), w).map(Boolean::neg)
644            }
645        }
646    }
647
648    pub fn all<F: FieldWitness>(x: &[Self], w: &mut Witness<F>) -> CircuitVar<Boolean> {
649        match x {
650            [] => CircuitVar::Constant(Boolean::True),
651            [b1] => *b1,
652            [b1, b2] => b1.and(b2, w),
653            bs => {
654                let sum = Self::boolean_sum(bs);
655                let len = F::from(bs.len() as u64);
656                CircuitVar::equal(&CircuitVar::Constant(len), &sum, w)
657            }
658        }
659    }
660
661    pub fn neg(&self) -> Self {
662        self.map(Boolean::neg)
663    }
664
665    pub fn or<F: FieldWitness>(&self, other: &Self, w: &mut Witness<F>) -> Self {
666        let both_false = self.neg().and(&other.neg(), w);
667        both_false.neg()
668    }
669
670    pub fn lxor<F: FieldWitness>(&self, other: &Self, w: &mut Witness<F>) -> Self {
671        match (self, other) {
672            (CircuitVar::Var(a), CircuitVar::Var(b)) => CircuitVar::Var(a.lxor(b, w)),
673            (CircuitVar::Constant(a), CircuitVar::Constant(b)) => {
674                CircuitVar::Constant(a.const_lxor(b))
675            }
676            (a, b) => CircuitVar::Var(a.as_boolean().const_lxor(&b.as_boolean())),
677        }
678    }
679
680    pub fn equal_bool<F: FieldWitness>(&self, other: &Self, w: &mut Witness<F>) -> Self {
681        self.lxor(other, w).neg()
682    }
683
684    pub fn assert_any<F: FieldWitness>(bs: &[Self], w: &mut Witness<F>) {
685        let num_true = bs.iter().fold(0u64, |acc, b| {
686            acc + match b.as_boolean() {
687                Boolean::True => 1,
688                Boolean::False => 0,
689            }
690        });
691        Boolean::assert_non_zero::<F>(F::from(num_true), w)
692    }
693}