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