kimchi/circuits/polynomials/foreign_field_add/
gadget.rs

1//! This module obtains the gates of a foreign field addition circuit.
2use alloc::{vec, vec::Vec};
3
4use ark_ff::PrimeField;
5use num_bigint::BigUint;
6
7use crate::circuits::{
8    gate::{CircuitGate, Connect, GateType},
9    polynomials::foreign_field_common::BigUintForeignFieldHelpers,
10    wires::Wire,
11};
12
13use super::witness::FFOps;
14
15impl<F: PrimeField> CircuitGate<F> {
16    /// Create foreign field addition gate chain without range checks (needs to wire the range check for result bound manually)
17    /// - Inputs
18    ///   - starting row
19    ///   - operations to perform
20    ///   - modulus of the foreign field
21    /// - Outputs tuple (next_row, circuit_gates) where
22    ///   - next_row      - next row after this gate
23    ///   - circuit_gates - vector of circuit gates comprising this gate
24    ///
25    /// Note that the final structure of the circuit is as follows:
26    /// circuit_gates = [
27    ///      {
28    ///        (i) ->      -> 1 ForeignFieldAdd row
29    ///      } * num times
30    ///      (n)           -> 1 ForeignFieldAdd row (this is where the final result goes)
31    ///      (n+1)         -> 1 Zero row for bound result
32    /// ]
33    ///
34    /// Warning:
35    /// - Wire the range check for result bound manually
36    /// - Connect to public input containing the 1 value for the overflow in the final bound check
37    /// - If the inputs of the addition come from public input, wire it as well
38    pub fn create_chain_ffadd(
39        start_row: usize,
40        opcodes: &[FFOps],
41        foreign_field_modulus: &BigUint,
42    ) -> (usize, Vec<Self>) {
43        if *foreign_field_modulus > BigUint::max_foreign_field_modulus::<F>() {
44            panic!(
45                "foreign_field_modulus exceeds maximum: {} > {}",
46                *foreign_field_modulus,
47                BigUint::max_foreign_field_modulus::<F>()
48            );
49        }
50
51        let next_row = start_row;
52        let foreign_field_modulus = foreign_field_modulus.to_field_limbs::<F>();
53        let mut circuit_gates = vec![];
54        let num = opcodes.len();
55        // ---------------------------
56        // Foreign field addition gates
57        // ---------------------------
58        // First the single-addition gates
59        for (i, opcode) in opcodes.iter().enumerate() {
60            let mut coeffs = foreign_field_modulus.to_vec();
61            coeffs.push(opcode.sign::<F>());
62            circuit_gates.append(&mut vec![CircuitGate {
63                typ: GateType::ForeignFieldAdd,
64                wires: Wire::for_row(next_row + i),
65                coeffs,
66            }]);
67        }
68        let mut final_coeffs = foreign_field_modulus.to_vec();
69        final_coeffs.push(FFOps::Add.sign::<F>());
70        // Then the final bound gate and the zero gate
71        circuit_gates.append(&mut vec![
72            CircuitGate {
73                typ: GateType::ForeignFieldAdd,
74                wires: Wire::for_row(next_row + num),
75                coeffs: final_coeffs,
76            },
77            CircuitGate {
78                typ: GateType::Zero,
79                wires: Wire::for_row(next_row + num + 1),
80                coeffs: vec![],
81            },
82        ]);
83        (start_row + circuit_gates.len(), circuit_gates)
84    }
85
86    /// Create a single foreign field addition gate. This is used for example in the final bound check.
87    /// - Inputs
88    ///   - starting row
89    ///   - operation to perform
90    ///   - modulus of the foreign field
91    /// - Outputs tuple (next_row, circuit_gates) where
92    ///   - next_row      - next row after this gate
93    ///   - circuit_gates - vector of circuit gates comprising this gate
94    pub fn create_single_ffadd(
95        start_row: usize,
96        operation: FFOps,
97        foreign_field_modulus: &BigUint,
98    ) -> (usize, Vec<Self>) {
99        if *foreign_field_modulus > BigUint::max_foreign_field_modulus::<F>() {
100            panic!(
101                "foreign_field_modulus exceeds maximum: {} > {}",
102                *foreign_field_modulus,
103                BigUint::max_foreign_field_modulus::<F>()
104            );
105        }
106
107        let foreign_field_modulus = foreign_field_modulus.to_field_limbs::<F>();
108        let mut coeffs = foreign_field_modulus.to_vec();
109        coeffs.push(operation.sign::<F>());
110        let circuit_gates = vec![
111            CircuitGate {
112                typ: GateType::ForeignFieldAdd,
113                wires: Wire::for_row(start_row),
114                coeffs,
115            },
116            CircuitGate {
117                typ: GateType::Zero,
118                wires: Wire::for_row(start_row + 1),
119                coeffs: vec![],
120            },
121        ];
122
123        (start_row + circuit_gates.len(), circuit_gates)
124    }
125
126    /// Extend a chain of foreign field addition gates. It already wires 1 value to the overflow cell.
127    /// - Inputs
128    ///   - gates: vector of gates to extend
129    ///   - pub_row: row of the public input
130    ///   - curr_row: mutable reference to the current row
131    ///   - opcodes: operations to perform
132    ///   - foreign_field_modulus: modulus of the foreign field
133    pub fn extend_chain_ffadd(
134        gates: &mut Vec<Self>,
135        pub_row: usize,
136        curr_row: &mut usize,
137        opcodes: &[FFOps],
138        foreign_field_modulus: &BigUint,
139    ) {
140        let (next_row, add_gates) =
141            Self::create_chain_ffadd(*curr_row, opcodes, foreign_field_modulus);
142        gates.extend_from_slice(&add_gates);
143        *curr_row = next_row;
144        // check overflow flag is one
145        gates.connect_cell_pair((pub_row, 0), (*curr_row - 2, 6));
146    }
147
148    /// Extend a single foreign field addition gate followed by a zero row containing the result
149    pub fn extend_single_ffadd(
150        gates: &mut Vec<Self>,
151        curr_row: &mut usize,
152        operation: FFOps,
153        foreign_field_modulus: &BigUint,
154    ) {
155        let (next_row, add_gates) =
156            Self::create_single_ffadd(*curr_row, operation, foreign_field_modulus);
157        *curr_row = next_row;
158        gates.extend_from_slice(&add_gates);
159    }
160}
kimchi/circuits/polynomials/foreign_field_add/gadget.rs

kimchi/circuits/polynomials/foreign_field_add/
gadget.rs
