Skip to main content

kimchi/circuits/
gate.rs

1//! This module implements Plonk constraint gate primitive.
2
3use crate::{
4    circuits::{
5        argument::{Argument, ArgumentEnv},
6        berkeley_columns::BerkeleyChallenges,
7        constraints::ConstraintSystem,
8        polynomials::{
9            complete_add, endomul_scalar, endosclmul, foreign_field_add, foreign_field_mul,
10            poseidon, range_check, rot, turshi, varbasemul, xor,
11        },
12        wires::*,
13    },
14    curve::KimchiCurve,
15    prover_index::ProverIndex,
16};
17use ark_ff::PrimeField;
18use o1_utils::hasher::CryptoDigest;
19use serde::{Deserialize, Serialize};
20use serde_with::serde_as;
21use thiserror::Error;
22
23use super::{argument::ArgumentWitness, expr};
24
25/// A row accessible from a given row, corresponds to the fact that we open all polynomials
26/// at `zeta` **and** `omega * zeta`.
27#[repr(C)]
28#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize)]
29#[cfg_attr(
30    feature = "ocaml_types",
31    derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Enum)
32)]
33#[cfg_attr(feature = "wasm_types", wasm_bindgen::prelude::wasm_bindgen)]
34#[cfg_attr(test, derive(proptest_derive::Arbitrary))]
35pub enum CurrOrNext {
36    Curr,
37    Next,
38}
39
40impl CurrOrNext {
41    /// Compute the offset corresponding to the `CurrOrNext` value.
42    /// - `Curr.shift() == 0`
43    /// - `Next.shift() == 1`
44    pub fn shift(&self) -> usize {
45        match self {
46            CurrOrNext::Curr => 0,
47            CurrOrNext::Next => 1,
48        }
49    }
50}
51
52/// The different types of gates the system supports.
53/// Note that all the gates are mutually exclusive:
54/// they cannot be used at the same time on single row.
55/// If we were ever to support this feature, we would have to make sure
56/// not to re-use powers of alpha across constraints.
57#[repr(C)]
58#[derive(
59    Clone, Copy, Debug, Default, PartialEq, Serialize, Deserialize, Eq, Hash, PartialOrd, Ord,
60)]
61#[cfg_attr(
62    feature = "ocaml_types",
63    derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Enum)
64)]
65#[cfg_attr(feature = "wasm_types", wasm_bindgen::prelude::wasm_bindgen)]
66#[cfg_attr(test, derive(proptest_derive::Arbitrary))]
67pub enum GateType {
68    #[default]
69    /// Zero gate
70    Zero,
71    /// Generic arithmetic gate
72    Generic,
73    /// Poseidon permutation gate
74    Poseidon,
75    /// Complete EC addition in Affine form
76    CompleteAdd,
77    /// EC variable base scalar multiplication
78    VarBaseMul,
79    /// EC variable base scalar multiplication with group endomorphim optimization
80    EndoMul,
81    /// Gate for computing the scalar corresponding to an endoscaling
82    EndoMulScalar,
83    // Lookup
84    Lookup,
85    /// Cairo
86    CairoClaim,
87    CairoInstruction,
88    CairoFlags,
89    CairoTransition,
90    /// Range check
91    RangeCheck0,
92    RangeCheck1,
93    ForeignFieldAdd,
94    ForeignFieldMul,
95    // Gates for Keccak
96    Xor16,
97    Rot64,
98}
99
100/// Gate error
101#[derive(Error, Debug, Clone, Copy, PartialEq, Eq)]
102pub enum CircuitGateError {
103    /// Invalid constraint
104    #[error("Invalid {0:?} constraint")]
105    InvalidConstraint(GateType),
106    /// Invalid constraint with number
107    #[error("Invalid {0:?} constraint: {1}")]
108    Constraint(GateType, usize),
109    /// Invalid wire column
110    #[error("Invalid {0:?} wire column: {1}")]
111    WireColumn(GateType, usize),
112    /// Disconnected wires
113    #[error("Invalid {typ:?} copy constraint: {},{} -> {},{}", .src.row, .src.col, .dst.row, .dst.col)]
114    CopyConstraint { typ: GateType, src: Wire, dst: Wire },
115    /// Invalid lookup
116    #[error("Invalid {0:?} lookup constraint")]
117    InvalidLookupConstraint(GateType),
118    /// Failed to get witness for row
119    #[error("Failed to get {0:?} witness for row {1}")]
120    FailedToGetWitnessForRow(GateType, usize),
121}
122
123/// Gate result
124pub type CircuitGateResult<T> = core::result::Result<T, CircuitGateError>;
125
126#[serde_as]
127#[derive(Clone, Debug, Default, Serialize, Deserialize)]
128/// A single gate in a circuit.
129pub struct CircuitGate<F: PrimeField> {
130    /// type of the gate
131    pub typ: GateType,
132
133    /// gate wiring (for each cell, what cell it is wired to)
134    pub wires: GateWires,
135
136    /// public selector polynomials that can used as handy coefficients in gates
137    #[serde_as(as = "Vec<o1_utils::serialization::SerdeAs>")]
138    pub coeffs: Vec<F>,
139}
140
141impl<F> CircuitGate<F>
142where
143    F: PrimeField,
144{
145    pub fn new(typ: GateType, wires: GateWires, coeffs: Vec<F>) -> Self {
146        Self { typ, wires, coeffs }
147    }
148}
149
150impl<F: PrimeField> CircuitGate<F> {
151    /// this function creates "empty" circuit gate
152    pub fn zero(wires: GateWires) -> Self {
153        CircuitGate::new(GateType::Zero, wires, vec![])
154    }
155
156    /// This function verifies the consistency of the wire
157    /// assignments (witness) against the constraints
158    ///
159    /// # Errors
160    ///
161    /// Will give error if verify process returns error.
162    pub fn verify<
163        const FULL_ROUNDS: usize,
164        G: KimchiCurve<FULL_ROUNDS, ScalarField = F>,
165        Srs: poly_commitment::SRS<G>,
166    >(
167        &self,
168        row: usize,
169        witness: &[Vec<F>; COLUMNS],
170        index: &ProverIndex<FULL_ROUNDS, G, Srs>,
171        public: &[F],
172    ) -> Result<(), String> {
173        use GateType::*;
174        match self.typ {
175            Zero => Ok(()),
176            Generic => self.verify_generic(row, witness, public),
177            Poseidon => self.verify_poseidon::<FULL_ROUNDS, G>(row, witness),
178            CompleteAdd => self.verify_complete_add(row, witness),
179            VarBaseMul => self.verify_vbmul(row, witness),
180            EndoMul => self.verify_endomul::<FULL_ROUNDS, G>(row, witness, &index.cs),
181            EndoMulScalar => self.verify_endomul_scalar::<FULL_ROUNDS, G>(row, witness, &index.cs),
182            // TODO: implement the verification for the lookup gate
183            // See https://github.com/MinaProtocol/mina/issues/14011
184            Lookup => Ok(()),
185            CairoClaim | CairoInstruction | CairoFlags | CairoTransition => {
186                self.verify_cairo_gate::<FULL_ROUNDS, G>(row, witness, &index.cs)
187            }
188            RangeCheck0 | RangeCheck1 => self
189                .verify_witness::<FULL_ROUNDS, G>(row, witness, &index.cs, public)
190                .map_err(|e| e.to_string()),
191            ForeignFieldAdd => self
192                .verify_witness::<FULL_ROUNDS, G>(row, witness, &index.cs, public)
193                .map_err(|e| e.to_string()),
194            ForeignFieldMul => self
195                .verify_witness::<FULL_ROUNDS, G>(row, witness, &index.cs, public)
196                .map_err(|e| e.to_string()),
197            Xor16 => self
198                .verify_witness::<FULL_ROUNDS, G>(row, witness, &index.cs, public)
199                .map_err(|e| e.to_string()),
200            Rot64 => self
201                .verify_witness::<FULL_ROUNDS, G>(row, witness, &index.cs, public)
202                .map_err(|e| e.to_string()),
203        }
204    }
205
206    /// Verify the witness against the constraints
207    pub fn verify_witness<
208        const FULL_ROUNDS: usize,
209        G: KimchiCurve<FULL_ROUNDS, ScalarField = F>,
210    >(
211        &self,
212        row: usize,
213        witness: &[Vec<F>; COLUMNS],
214        cs: &ConstraintSystem<F>,
215        _public: &[F],
216    ) -> CircuitGateResult<()> {
217        // Grab the relevant part of the witness
218        let argument_witness = self.argument_witness(row, witness)?;
219        // Set up the constants.  Note that alpha, beta, gamma and joint_combiner
220        // are one because this function is not running the prover.
221        let constants = expr::Constants {
222            endo_coefficient: cs.endo,
223            mds: &G::sponge_params().mds,
224            zk_rows: cs.zk_rows,
225        };
226        //TODO : use generic challenges, since we do not need those here
227        let challenges = BerkeleyChallenges {
228            alpha: F::one(),
229            beta: F::one(),
230            gamma: F::one(),
231            joint_combiner: F::one(),
232        };
233        // Create the argument environment for the constraints over field elements
234        let env = ArgumentEnv::<F, F>::create(
235            argument_witness,
236            self.coeffs.clone(),
237            constants,
238            challenges,
239        );
240
241        // Check the wiring (i.e. copy constraints) for this gate
242        // Note: Gates can operated on row Curr or Curr and Next.
243        //       It could be nice for gates to know this and then
244        //       this code could be adapted to check Curr or Curr
245        //       and Next depending on the gate definition
246        for col in 0..PERMUTS {
247            let wire = self.wires[col];
248
249            if wire.col >= PERMUTS {
250                return Err(CircuitGateError::WireColumn(self.typ, col));
251            }
252
253            if witness[col][row] != witness[wire.col][wire.row] {
254                // Pinpoint failed copy constraint
255                return Err(CircuitGateError::CopyConstraint {
256                    typ: self.typ,
257                    src: Wire { row, col },
258                    dst: wire,
259                });
260            }
261        }
262
263        let mut cache = expr::Cache::default();
264
265        // Perform witness verification on each constraint for this gate
266        let results = match self.typ {
267            GateType::Zero => {
268                vec![]
269            }
270            GateType::Generic => {
271                // TODO: implement the verification for the generic gate
272                vec![]
273            }
274            GateType::Poseidon => poseidon::Poseidon::constraint_checks(&env, &mut cache),
275            GateType::CompleteAdd => complete_add::CompleteAdd::constraint_checks(&env, &mut cache),
276            GateType::VarBaseMul => varbasemul::VarbaseMul::constraint_checks(&env, &mut cache),
277            GateType::EndoMul => endosclmul::EndosclMul::constraint_checks(&env, &mut cache),
278            GateType::EndoMulScalar => {
279                endomul_scalar::EndomulScalar::constraint_checks(&env, &mut cache)
280            }
281            GateType::Lookup => {
282                // TODO: implement the verification for the lookup gate
283                // See https://github.com/MinaProtocol/mina/issues/14011
284                vec![]
285            }
286            GateType::CairoClaim => turshi::Claim::constraint_checks(&env, &mut cache),
287            GateType::CairoInstruction => turshi::Instruction::constraint_checks(&env, &mut cache),
288            GateType::CairoFlags => turshi::Flags::constraint_checks(&env, &mut cache),
289            GateType::CairoTransition => turshi::Transition::constraint_checks(&env, &mut cache),
290            GateType::RangeCheck0 => {
291                range_check::circuitgates::RangeCheck0::constraint_checks(&env, &mut cache)
292            }
293            GateType::RangeCheck1 => {
294                range_check::circuitgates::RangeCheck1::constraint_checks(&env, &mut cache)
295            }
296            GateType::ForeignFieldAdd => {
297                foreign_field_add::circuitgates::ForeignFieldAdd::constraint_checks(
298                    &env, &mut cache,
299                )
300            }
301            GateType::ForeignFieldMul => {
302                foreign_field_mul::circuitgates::ForeignFieldMul::constraint_checks(
303                    &env, &mut cache,
304                )
305            }
306            GateType::Xor16 => xor::Xor16::constraint_checks(&env, &mut cache),
307            GateType::Rot64 => rot::Rot64::constraint_checks(&env, &mut cache),
308        };
309
310        // Check for failed constraints
311        for (i, result) in results.iter().enumerate() {
312            if !result.is_zero() {
313                // Pinpoint failed constraint
314                return Err(CircuitGateError::Constraint(self.typ, i + 1));
315            }
316        }
317
318        // TODO: implement generic plookup witness verification
319
320        Ok(())
321    }
322
323    // Return the part of the witness relevant to this gate at the given row offset
324    fn argument_witness(
325        &self,
326        row: usize,
327        witness: &[Vec<F>; COLUMNS],
328    ) -> CircuitGateResult<ArgumentWitness<F>> {
329        // Get the part of the witness relevant to this gate
330        let witness_curr: [F; COLUMNS] = (0..witness.len())
331            .map(|col| witness[col][row])
332            .collect::<Vec<F>>()
333            .try_into()
334            .map_err(|_| CircuitGateError::FailedToGetWitnessForRow(self.typ, row))?;
335        let witness_next: [F; COLUMNS] = if witness[0].len() > row + 1 {
336            (0..witness.len())
337                .map(|col| witness[col][row + 1])
338                .collect::<Vec<F>>()
339                .try_into()
340                .map_err(|_| CircuitGateError::FailedToGetWitnessForRow(self.typ, row))?
341        } else {
342            [F::zero(); COLUMNS]
343        };
344
345        Ok(ArgumentWitness::<F> {
346            curr: witness_curr,
347            next: witness_next,
348        })
349    }
350}
351
352/// Trait to connect a pair of cells in a circuit
353pub trait Connect {
354    /// Connect the pair of cells specified by the cell1 and cell2 parameters
355    /// `cell_pre` --> `cell_new` && `cell_new` --> `wire_tmp`
356    ///
357    /// Note: This function assumes that the targeted cells are freshly instantiated
358    ///       with self-connections.  If the two cells are transitively already part
359    ///       of the same permutation then this would split it.
360    fn connect_cell_pair(&mut self, cell1: (usize, usize), cell2: (usize, usize));
361
362    /// Connects a generic gate cell with zeros to a given row for 64bit range check
363    fn connect_64bit(&mut self, zero_row: usize, start_row: usize);
364
365    /// Connects the wires of the range checks in a single foreign field addition
366    /// Inputs:
367    /// - `ffadd_row`: the row of the foreign field addition gate
368    /// - `left_rc`: the first row of the range check for the left input
369    /// - `right_rc`: the first row of the range check for the right input
370    /// - `out_rc`: the first row of the range check for the output of the addition
371    ///
372    /// Note:
373    ///   If run with `left_rc = None` and `right_rc = None` then it can be used for the bound check range check
374    fn connect_ffadd_range_checks(
375        &mut self,
376        ffadd_row: usize,
377        left_rc: Option<usize>,
378        right_rc: Option<usize>,
379        out_rc: usize,
380    );
381}
382
383impl<F: PrimeField> Connect for Vec<CircuitGate<F>> {
384    fn connect_cell_pair(&mut self, cell_pre: (usize, usize), cell_new: (usize, usize)) {
385        let wire_tmp = self[cell_pre.0].wires[cell_pre.1];
386        self[cell_pre.0].wires[cell_pre.1] = self[cell_new.0].wires[cell_new.1];
387        self[cell_new.0].wires[cell_new.1] = wire_tmp;
388    }
389
390    fn connect_64bit(&mut self, zero_row: usize, start_row: usize) {
391        // Connect the 64-bit cells from previous Generic gate with zeros in first 12 bits
392        self.connect_cell_pair((start_row, 1), (start_row, 2));
393        self.connect_cell_pair((start_row, 2), (zero_row, 0));
394        self.connect_cell_pair((zero_row, 0), (start_row, 1));
395    }
396
397    fn connect_ffadd_range_checks(
398        &mut self,
399        ffadd_row: usize,
400        left_rc: Option<usize>,
401        right_rc: Option<usize>,
402        out_rc: usize,
403    ) {
404        if let Some(left_rc) = left_rc {
405            // Copy left_input_lo -> Curr(0)
406            self.connect_cell_pair((left_rc, 0), (ffadd_row, 0));
407            // Copy left_input_mi -> Curr(1)
408            self.connect_cell_pair((left_rc + 1, 0), (ffadd_row, 1));
409            // Copy left_input_hi -> Curr(2)
410            self.connect_cell_pair((left_rc + 2, 0), (ffadd_row, 2));
411        }
412
413        if let Some(right_rc) = right_rc {
414            // Copy right_input_lo -> Curr(3)
415            self.connect_cell_pair((right_rc, 0), (ffadd_row, 3));
416            // Copy right_input_mi -> Curr(4)
417            self.connect_cell_pair((right_rc + 1, 0), (ffadd_row, 4));
418            // Copy right_input_hi -> Curr(5)
419            self.connect_cell_pair((right_rc + 2, 0), (ffadd_row, 5));
420        }
421
422        // Copy result_lo -> Next(0)
423        self.connect_cell_pair((out_rc, 0), (ffadd_row + 1, 0));
424        // Copy result_mi -> Next(1)
425        self.connect_cell_pair((out_rc + 1, 0), (ffadd_row + 1, 1));
426        // Copy result_hi -> Next(2)
427        self.connect_cell_pair((out_rc + 2, 0), (ffadd_row + 1, 2));
428    }
429}
430
431/// A circuit is specified as a public input size and a list of [`CircuitGate`].
432#[derive(Serialize)]
433#[serde(bound = "CircuitGate<F>: Serialize")]
434pub struct Circuit<'a, F: PrimeField> {
435    pub public_input_size: usize,
436    pub gates: &'a [CircuitGate<F>],
437}
438
439impl<'a, F> Circuit<'a, F>
440where
441    F: PrimeField,
442{
443    pub fn new(public_input_size: usize, gates: &'a [CircuitGate<F>]) -> Self {
444        Self {
445            public_input_size,
446            gates,
447        }
448    }
449}
450
451impl<'a, F: PrimeField> CryptoDigest for Circuit<'a, F> {
452    const PREFIX: &'static [u8; 15] = b"kimchi-circuit0";
453}
454
455impl<'a, F> From<&'a ConstraintSystem<F>> for Circuit<'a, F>
456where
457    F: PrimeField,
458{
459    fn from(cs: &'a ConstraintSystem<F>) -> Self {
460        Self {
461            public_input_size: cs.public,
462            gates: &cs.gates,
463        }
464    }
465}
466
467#[cfg(feature = "ocaml_types")]
468pub mod caml {
469    use super::*;
470    use crate::circuits::wires::caml::CamlWire;
471    use itertools::Itertools;
472
473    #[derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct)]
474    pub struct CamlCircuitGate<F> {
475        pub typ: GateType,
476        pub wires: (
477            CamlWire,
478            CamlWire,
479            CamlWire,
480            CamlWire,
481            CamlWire,
482            CamlWire,
483            CamlWire,
484        ),
485        pub coeffs: Vec<F>,
486    }
487
488    impl<F, CamlF> From<CircuitGate<F>> for CamlCircuitGate<CamlF>
489    where
490        CamlF: From<F>,
491        F: PrimeField,
492    {
493        fn from(cg: CircuitGate<F>) -> Self {
494            Self {
495                typ: cg.typ,
496                wires: array_to_tuple(cg.wires),
497                coeffs: cg.coeffs.into_iter().map(Into::into).collect(),
498            }
499        }
500    }
501
502    impl<F, CamlF> From<&CircuitGate<F>> for CamlCircuitGate<CamlF>
503    where
504        CamlF: From<F>,
505        F: PrimeField,
506    {
507        fn from(cg: &CircuitGate<F>) -> Self {
508            Self {
509                typ: cg.typ,
510                wires: array_to_tuple(cg.wires),
511                coeffs: cg.coeffs.clone().into_iter().map(Into::into).collect(),
512            }
513        }
514    }
515
516    impl<F, CamlF> From<CamlCircuitGate<CamlF>> for CircuitGate<F>
517    where
518        F: From<CamlF>,
519        F: PrimeField,
520    {
521        fn from(ccg: CamlCircuitGate<CamlF>) -> Self {
522            Self {
523                typ: ccg.typ,
524                wires: tuple_to_array(ccg.wires),
525                coeffs: ccg.coeffs.into_iter().map(Into::into).collect(),
526            }
527        }
528    }
529
530    /// helper to convert array to tuple (OCaml doesn't have fixed-size arrays)
531    fn array_to_tuple<T1, T2>(a: [T1; PERMUTS]) -> (T2, T2, T2, T2, T2, T2, T2)
532    where
533        T1: Clone,
534        T2: From<T1>,
535    {
536        a.into_iter()
537            .map(Into::into)
538            .next_tuple()
539            .expect("bug in array_to_tuple")
540    }
541
542    /// helper to convert tuple to array (OCaml doesn't have fixed-size arrays)
543    fn tuple_to_array<T1, T2>(a: (T1, T1, T1, T1, T1, T1, T1)) -> [T2; PERMUTS]
544    where
545        T2: From<T1>,
546    {
547        [
548            a.0.into(),
549            a.1.into(),
550            a.2.into(),
551            a.3.into(),
552            a.4.into(),
553            a.5.into(),
554            a.6.into(),
555        ]
556    }
557}
558
559//
560// Tests
561//
562
563#[cfg(test)]
564mod tests {
565    use super::*;
566    use ark_ff::UniformRand as _;
567    use mina_curves::pasta::Fp;
568    use proptest::prelude::*;
569    use rand::SeedableRng as _;
570
571    prop_compose! {
572        fn arb_fp_vec(max: usize)(seed: [u8; 32], num in 0..max) -> Vec<Fp> {
573            let rng = &mut rand::rngs::StdRng::from_seed(seed);
574            let mut v = vec![];
575            for _ in 0..num {
576                v.push(Fp::rand(rng))
577            }
578            v
579        }
580    }
581
582    prop_compose! {
583        fn arb_circuit_gate()(typ: GateType, wires: GateWires, coeffs in arb_fp_vec(25)) -> CircuitGate<Fp> {
584            CircuitGate::new(
585                typ,
586                wires,
587                coeffs,
588            )
589        }
590    }
591
592    proptest! {
593        #[test]
594        fn test_gate_serialization(cg in arb_circuit_gate()) {
595            let encoded = rmp_serde::to_vec(&cg).unwrap();
596            let decoded: CircuitGate<Fp> = rmp_serde::from_slice(&encoded).unwrap();
597            prop_assert_eq!(cg.typ, decoded.typ);
598            for i in 0..PERMUTS {
599                prop_assert_eq!(cg.wires[i], decoded.wires[i]);
600            }
601            prop_assert_eq!(cg.coeffs, decoded.coeffs);
602        }
603    }
604}