arrabbiata/
constraint.rs

1use super::{column::Column, interpreter::InterpreterEnv};
2use crate::{
3    column::{Gadget, E},
4    curve::{ArrabbiataCurve, PlonkSpongeConstants},
5    interpreter::{self, Instruction, Side},
6    MAX_DEGREE, NUMBER_OF_COLUMNS,
7};
8
9use ark_ff::PrimeField;
10use kimchi::circuits::{
11    expr::{ConstantTerm::Literal, Expr, ExprInner, Operations, Variable},
12    gate::CurrOrNext,
13};
14use log::debug;
15use mina_poseidon::constants::SpongeConstants;
16use num_bigint::BigInt;
17use o1_utils::FieldHelpers;
18use std::collections::HashMap;
19
20#[derive(Clone, Debug)]
21pub struct Env<C: ArrabbiataCurve>
22where
23    C::BaseField: PrimeField,
24{
25    /// The parameter a is the coefficients of the elliptic curve in affine
26    /// coordinates.
27    pub a: BigInt,
28    pub idx_var: usize,
29    pub idx_var_next_row: usize,
30    pub constraints: Vec<E<C::ScalarField>>,
31}
32
33impl<C: ArrabbiataCurve> Env<C>
34where
35    C::BaseField: PrimeField,
36{
37    pub fn new() -> Self {
38        // This check might not be useful
39        let a: C::BaseField = C::get_curve_params().0;
40        let a: BigInt = a.to_biguint().into();
41        assert!(
42            a < C::ScalarField::modulus_biguint().into(),
43            "a is too large"
44        );
45        Self {
46            a,
47            idx_var: 0,
48            idx_var_next_row: 0,
49            constraints: Vec::new(),
50        }
51    }
52}
53
54/// An environment to build constraints.
55/// The constraint environment is mostly useful when we want to perform a Nova
56/// proof.
57/// The constraint environment must be instantiated only once, at the last step
58/// of the computation.
59impl<C: ArrabbiataCurve> InterpreterEnv for Env<C>
60where
61    C::BaseField: PrimeField,
62{
63    type Position = (Column, CurrOrNext);
64
65    type Variable = E<C::ScalarField>;
66
67    fn allocate(&mut self) -> Self::Position {
68        assert!(self.idx_var < NUMBER_OF_COLUMNS, "Maximum number of columns reached ({NUMBER_OF_COLUMNS}), increase the number of columns");
69        let pos = Column::X(self.idx_var);
70        self.idx_var += 1;
71        (pos, CurrOrNext::Curr)
72    }
73
74    fn allocate_next_row(&mut self) -> Self::Position {
75        assert!(self.idx_var_next_row < NUMBER_OF_COLUMNS, "Maximum number of columns reached ({NUMBER_OF_COLUMNS}), increase the number of columns");
76        let pos = Column::X(self.idx_var_next_row);
77        self.idx_var_next_row += 1;
78        (pos, CurrOrNext::Next)
79    }
80
81    fn read_position(&self, pos: Self::Position) -> Self::Variable {
82        let (col, row) = pos;
83        Expr::Atom(ExprInner::Cell(Variable { col, row }))
84    }
85
86    fn constant(&self, value: BigInt) -> Self::Variable {
87        let v = value.to_biguint().unwrap();
88        let v = C::ScalarField::from_biguint(&v).unwrap();
89        let v_inner = Operations::from(Literal(v));
90        Self::Variable::constant(v_inner)
91    }
92
93    /// Return the corresponding expression regarding the selected column
94    fn write_column(&mut self, pos: Self::Position, v: Self::Variable) -> Self::Variable {
95        let (col, row) = pos;
96        let res = Expr::Atom(ExprInner::Cell(Variable { col, row }));
97        self.assert_equal(res.clone(), v);
98        res
99    }
100
101    fn add_constraint(&mut self, constraint: Self::Variable) {
102        let degree = constraint.degree(1, 0);
103        debug!("Adding constraint of degree {degree}: {:}", constraint);
104        assert!(degree <= MAX_DEGREE.try_into().unwrap(), "degree is too high: {}. The folding scheme used currently allows constraint up to degree {}", degree, MAX_DEGREE);
105        self.constraints.push(constraint);
106    }
107
108    fn constrain_boolean(&mut self, x: Self::Variable) {
109        let one = self.one();
110        let c = x.clone() * (x.clone() - one);
111        self.constraints.push(c)
112    }
113    fn assert_zero(&mut self, x: Self::Variable) {
114        self.add_constraint(x);
115    }
116
117    fn assert_equal(&mut self, x: Self::Variable, y: Self::Variable) {
118        self.add_constraint(x - y);
119    }
120
121    unsafe fn bitmask_be(
122        &mut self,
123        _x: &Self::Variable,
124        _highest_bit: u32,
125        _lowest_bit: u32,
126        pos: Self::Position,
127    ) -> Self::Variable {
128        self.read_position(pos)
129    }
130
131    fn square(&mut self, pos: Self::Position, x: Self::Variable) -> Self::Variable {
132        let v = self.read_position(pos);
133        let x = x.square();
134        self.add_constraint(x - v.clone());
135        v
136    }
137
138    // This is witness-only. We simply return the corresponding expression to
139    // use later in constraints
140    fn fetch_input(&mut self, pos: Self::Position) -> Self::Variable {
141        self.read_position(pos)
142    }
143
144    fn reset(&mut self) {
145        self.idx_var = 0;
146        self.idx_var_next_row = 0;
147        self.constraints.clear();
148    }
149
150    fn coin_folding_combiner(&mut self, pos: Self::Position) -> Self::Variable {
151        self.read_position(pos)
152    }
153
154    fn load_poseidon_state(&mut self, pos: Self::Position, _i: usize) -> Self::Variable {
155        self.read_position(pos)
156    }
157
158    // Witness-only
159    unsafe fn save_poseidon_state(&mut self, _x: Self::Variable, _i: usize) {}
160
161    fn get_poseidon_round_constant(&self, round: usize, i: usize) -> Self::Variable {
162        let cst = C::sponge_params().round_constants[round][i];
163        let cst_inner = Operations::from(Literal(cst));
164        Self::Variable::constant(cst_inner)
165    }
166
167    fn get_poseidon_mds_matrix(&mut self, i: usize, j: usize) -> Self::Variable {
168        let v = C::sponge_params().mds[i][j];
169        let v_inner = Operations::from(Literal(v));
170        Self::Variable::constant(v_inner)
171    }
172
173    unsafe fn fetch_value_to_absorb(&mut self, pos: Self::Position) -> Self::Variable {
174        self.read_position(pos)
175    }
176
177    unsafe fn load_temporary_accumulators(
178        &mut self,
179        pos_x: Self::Position,
180        pos_y: Self::Position,
181        _side: Side,
182    ) -> (Self::Variable, Self::Variable) {
183        let x = self.read_position(pos_x);
184        let y = self.read_position(pos_y);
185        (x, y)
186    }
187
188    // witness only
189    unsafe fn save_temporary_accumulators(
190        &mut self,
191        _x: Self::Variable,
192        _y: Self::Variable,
193        _side: Side,
194    ) {
195    }
196
197    /// Inverse of a variable
198    ///
199    /// # Safety
200    ///
201    /// Zero is not allowed as an input.
202    unsafe fn inverse(&mut self, pos: Self::Position, x: Self::Variable) -> Self::Variable {
203        let v = self.read_position(pos);
204        let res = v.clone() * x.clone();
205        self.assert_equal(res.clone(), self.one());
206        v
207    }
208
209    unsafe fn is_same_ec_point(
210        &mut self,
211        pos: Self::Position,
212        _x1: Self::Variable,
213        _y1: Self::Variable,
214        _x2: Self::Variable,
215        _y2: Self::Variable,
216    ) -> Self::Variable {
217        self.read_position(pos)
218    }
219
220    fn zero(&self) -> Self::Variable {
221        self.constant(BigInt::from(0_usize))
222    }
223
224    fn one(&self) -> Self::Variable {
225        self.constant(BigInt::from(1_usize))
226    }
227
228    /// Double the elliptic curve point given by the affine coordinates
229    /// `(x1, y1)` and save the result in the registers `pos_x` and `pos_y`.
230    fn double_ec_point(
231        &mut self,
232        pos_x: Self::Position,
233        pos_y: Self::Position,
234        x1: Self::Variable,
235        y1: Self::Variable,
236    ) -> (Self::Variable, Self::Variable) {
237        let lambda = {
238            let pos = self.allocate();
239            self.read_position(pos)
240        };
241        let x3 = self.read_position(pos_x);
242        let y3 = self.read_position(pos_y);
243
244        // λ 2y1 = 3x1^2 + a
245        let x1_square = x1.clone() * x1.clone();
246        let two_x1_square = x1_square.clone() + x1_square.clone();
247        let three_x1_square = two_x1_square.clone() + x1_square.clone();
248        let two_y1 = y1.clone() + y1.clone();
249        let res = lambda.clone() * two_y1 - (three_x1_square + self.constant(self.a.clone()));
250        self.assert_zero(res);
251        // x3 = λ^2 - 2 x1
252        self.assert_equal(
253            x3.clone(),
254            lambda.clone() * lambda.clone() - x1.clone() - x1.clone(),
255        );
256        // y3 = λ(x1 - x3) - y1
257        self.assert_equal(
258            y3.clone(),
259            lambda.clone() * (x1.clone() - x3.clone()) - y1.clone(),
260        );
261        (x3, y3.clone())
262    }
263
264    fn compute_lambda(
265        &mut self,
266        pos: Self::Position,
267        is_same_point: Self::Variable,
268        x1: Self::Variable,
269        y1: Self::Variable,
270        x2: Self::Variable,
271        y2: Self::Variable,
272    ) -> Self::Variable {
273        let lambda = self.read_position(pos);
274        let lhs = lambda.clone() * (x1.clone() - x2.clone()) - (y1.clone() - y2.clone());
275        let rhs = {
276            let x1_square = x1.clone() * x1.clone();
277            let two_x1_square = x1_square.clone() + x1_square.clone();
278            let three_x1_square = two_x1_square.clone() + x1_square.clone();
279            let two_y1 = y1.clone() + y1.clone();
280            lambda.clone() * two_y1 - (three_x1_square + self.constant(self.a.clone()))
281        };
282        let res = is_same_point.clone() * lhs + (self.one() - is_same_point.clone()) * rhs;
283        self.assert_zero(res);
284        lambda
285    }
286}
287
288impl<C: ArrabbiataCurve> Env<C>
289where
290    C::BaseField: PrimeField,
291{
292    /// Get all the constraints for the verifier circuit, only.
293    ///
294    /// The following gadgets are used in the verifier circuit:
295    /// - [Instruction::PoseidonFullRound] and
296    ///   [Instruction::PoseidonSpongeAbsorb] to verify the challenges and the
297    ///   public IO.
298    /// - [Instruction::EllipticCurveScaling] and
299    ///   [Instruction::EllipticCurveAddition] to accumulate the commitments
300    // FIXME: the verifier circuit might not be complete, yet. For instance, we might
301    // need to accumulate the challenges and add a row to verify the output of
302    // the computation of the challenges.
303    // FIXME: add a test checking that whatever the value given in parameter of
304    // the gadget, the constraints are the same
305    pub fn get_all_constraints_for_verifier(&self) -> Vec<E<C::ScalarField>> {
306        // Copying the instance we got in parameter, and making it mutable to
307        // avoid modifying the original instance.
308        let mut env = self.clone();
309        // Resetting before running anything
310        env.reset();
311
312        let mut constraints = vec![];
313
314        // Poseidon constraints
315        (0..PlonkSpongeConstants::PERM_ROUNDS_FULL / 12).for_each(|i| {
316            interpreter::run_ivc(&mut env, Instruction::PoseidonFullRound(5 * i));
317            constraints.extend(env.constraints.clone());
318            env.reset();
319        });
320
321        interpreter::run_ivc(&mut env, Instruction::PoseidonSpongeAbsorb);
322        constraints.extend(env.constraints.clone());
323        env.reset();
324
325        // EC scaling
326        // The constraints are the same whatever the value given in parameter,
327        // therefore picking 0, 0
328        interpreter::run_ivc(&mut env, Instruction::EllipticCurveScaling(0, 0));
329        constraints.extend(env.constraints.clone());
330        env.reset();
331
332        // EC addition
333        // The constraints are the same whatever the value given in parameter,
334        // therefore picking 0
335        interpreter::run_ivc(&mut env, Instruction::EllipticCurveAddition(0));
336        constraints.extend(env.constraints.clone());
337        env.reset();
338
339        constraints
340    }
341
342    /// Get all the constraints for the verifier circuit and the application.
343    // FIXME: the application should be given as an argument to handle Rust
344    // zkApp. It is only for the PoC.
345    // FIXME: the selectors are not added for now.
346    pub fn get_all_constraints(&self) -> Vec<E<C::ScalarField>> {
347        let mut constraints = self.get_all_constraints_for_verifier();
348
349        // Copying the instance we got in parameter, and making it mutable to
350        // avoid modifying the original instance.
351        let mut env = self.clone();
352        // Resetting before running anything
353        env.reset();
354
355        // Get the constraints for the application
356        interpreter::run_app(&mut env);
357        constraints.extend(env.constraints.clone());
358
359        constraints
360    }
361
362    pub fn get_all_constraints_indexed_by_gadget(&self) -> HashMap<Gadget, Vec<E<C::ScalarField>>> {
363        let mut hashmap = HashMap::new();
364        let mut env = self.clone();
365
366        // Poseidon constraints
367        (0..PlonkSpongeConstants::PERM_ROUNDS_FULL / 12).for_each(|i| {
368            interpreter::run_ivc(&mut env, Instruction::PoseidonFullRound(5 * i));
369            hashmap.insert(Gadget::PoseidonFullRound(5 * i), env.constraints.clone());
370            env.reset();
371        });
372
373        interpreter::run_ivc(&mut env, Instruction::PoseidonSpongeAbsorb);
374        hashmap.insert(Gadget::PoseidonSpongeAbsorb, env.constraints.clone());
375        env.reset();
376
377        // EC scaling
378        // The constraints are the same whatever the value given in parameter,
379        // therefore picking 0, 0
380        interpreter::run_ivc(&mut env, Instruction::EllipticCurveScaling(0, 0));
381        hashmap.insert(Gadget::EllipticCurveScaling, env.constraints.clone());
382        env.reset();
383
384        // EC addition
385        // The constraints are the same whatever the value given in parameter,
386        // therefore picking 0
387        interpreter::run_ivc(&mut env, Instruction::EllipticCurveAddition(0));
388        hashmap.insert(Gadget::EllipticCurveAddition, env.constraints.clone());
389        env.reset();
390
391        interpreter::run_app(&mut env);
392        hashmap.insert(Gadget::App, env.constraints.clone());
393        env.reset();
394
395        hashmap
396    }
397}
398
399impl<C: ArrabbiataCurve> Default for Env<C>
400where
401    C::BaseField: PrimeField,
402{
403    fn default() -> Self {
404        Self::new()
405    }
406}
arrabbiata/constraint.rs

arrabbiata/
constraint.rs
