jf_relation/gadgets/ultraplonk/
mod_arith.rs

1// Copyright (c) 2022 Espresso Systems (espressosys.com)
2// This file is part of the Jellyfish library.
3
4// You should have received a copy of the MIT License
5// along with the Jellyfish library. If not, see <https://mit-license.org/>.
6
7//! Modular arithmetic gates
8use crate::{
9    constants::GATE_WIDTH,
10    gadgets::utils::next_multiple,
11    Circuit,
12    CircuitError::{self, ParameterError},
13    PlonkCircuit, Variable,
14};
15use ark_ff::PrimeField;
16use ark_std::{format, string::ToString, vec, vec::Vec};
17use num_bigint::BigUint;
18
19macro_rules! to_big_int {
20    ($x:expr) => {
21        ($x).into_bigint().into()
22    };
23}
24
25#[derive(Debug, Clone, Eq, PartialEq, Default, Copy)]
26/// A field element represented by:
27/// p = p.0 + 2^m * p.1.
28/// The struct is useful in modular multiplication
29/// as the multiplication of two components (e.g. p.0 * q.0)
30/// won't overflow the prime field.
31/// Warning: for performance reasons, when this struct is used,
32/// we will assume 2^m - two_power_m without checking.
33pub struct FpElem<F: PrimeField> {
34    p: (F, F),
35    m: usize,
36    two_power_m: F,
37}
38
39impl<F> FpElem<F>
40where
41    F: PrimeField,
42{
43    /// Create a FpElem struct from field element `p` and split parameter `m`,
44    /// where `m` <= F::MODULUS_BIT_SIZE / 2
45    pub fn new(p: &F, m: usize, two_power_m: Option<F>) -> Result<Self, CircuitError> {
46        if m > F::MODULUS_BIT_SIZE as usize / 2 {
47            return Err(ParameterError(format!(
48                "field split parameter ({}) larger than half of the field size ({}) in bits",
49                m,
50                F::MODULUS_BIT_SIZE / 2
51            )));
52        }
53        let two_power_m = match two_power_m {
54            Some(p) => p,
55            None => F::from(2u8).pow([m as u64]),
56        };
57        let (p1, p0) = div_rem(p, &two_power_m);
58        Ok(Self {
59            p: (p0, p1),
60            m,
61            two_power_m,
62        })
63    }
64
65    /// Convert into a single field element.
66    pub fn field_elem(&self) -> F {
67        self.p.0 + self.two_power_m * self.p.1
68    }
69
70    /// Expose the field element components
71    pub fn components(&self) -> (F, F) {
72        self.p
73    }
74
75    /// Expose the m parameter
76    pub fn param_m(&self) -> usize {
77        self.m
78    }
79
80    /// Expose 2^m parameter
81    pub fn two_power_m(&self) -> F {
82        self.two_power_m
83    }
84}
85
86#[derive(Debug, Clone, Eq, PartialEq, Default, Copy)]
87/// Represent variable of an Fp element:
88///   elem = witness[vars.0] + 2^m * witness[vars.1]
89/// Warning: for performance reasons, when this struct is used,
90/// we will assume 2^m - two_power_m without checking.
91pub struct FpElemVar<F: PrimeField> {
92    vars: (Variable, Variable),
93    m: usize,
94    two_power_m: F,
95}
96
97impl<F: PrimeField> FpElemVar<F> {
98    /// Create an FpElemVar from Fp element variable `var` and split parameter
99    /// `m`. Does not perform range checks on the resulting variables.
100    /// To create an `FpElemVar` from a field element, consider to
101    /// use `new_from_field_element` instead (which comes with
102    /// a range proof for the field element).
103    pub fn new_unchecked(
104        cs: &mut PlonkCircuit<F>,
105        var: Variable,
106        m: usize,
107        two_power_m: Option<F>,
108    ) -> Result<Self, CircuitError> {
109        let fp_elem = FpElem::new(&cs.witness(var)?, m, two_power_m)?;
110        let var0 = cs.create_variable(fp_elem.p.0)?;
111        let var1 = cs.create_variable(fp_elem.p.1)?;
112        cs.lc_gate(
113            &[var0, var1, cs.zero(), cs.zero(), var],
114            &[F::one(), fp_elem.two_power_m, F::zero(), F::zero()],
115        )?;
116
117        Ok(Self {
118            vars: (var0, var1),
119            m,
120            two_power_m: fp_elem.two_power_m,
121        })
122    }
123
124    /// Convert into a single variable with value `witness[vars.0] + 2^m *
125    /// witness[vars.1]`
126    pub fn convert_to_var(&self, cs: &mut PlonkCircuit<F>) -> Result<Variable, CircuitError> {
127        cs.lc(
128            &[self.vars.0, self.vars.1, cs.zero(), cs.zero()],
129            &[F::one(), self.two_power_m, F::zero(), F::zero()],
130        )
131    }
132
133    /// Create an FpElemVar from field element and split parameter `m`.
134    /// This function is built with range-check proofs.
135    /// requires lookup table.
136    pub fn new_from_field_element(
137        cs: &mut PlonkCircuit<F>,
138        f: &F,
139        m: usize,
140        two_power_m: Option<F>,
141    ) -> Result<Self, CircuitError> {
142        let fp_elem = FpElem::new(f, m, two_power_m)?;
143        Self::new_from_fp_elem(cs, &fp_elem, m, two_power_m)
144    }
145
146    /// Create an FpElemVar from FpElem form field element .
147    /// This function is built with range-check proofs.
148    /// requires lookup table.
149    pub fn new_from_fp_elem(
150        cs: &mut PlonkCircuit<F>,
151        fp_elem: &FpElem<F>,
152        m: usize,
153        two_power_m: Option<F>,
154    ) -> Result<Self, CircuitError> {
155        let var0 = cs.create_variable(fp_elem.p.0)?;
156        let var1 = cs.create_variable(fp_elem.p.1)?;
157
158        cs.range_gate_with_lookup(var0, m)?;
159        cs.range_gate_with_lookup(var1, m)?;
160
161        Ok(Self {
162            vars: (var0, var1),
163            m,
164            two_power_m: match two_power_m {
165                Some(p) => p,
166                None => F::from(2u8).pow([m as u64]),
167            },
168        })
169    }
170
171    /// Get the witness in FpElem form from the variables
172    pub fn witness_fp_elem(&self, cs: &PlonkCircuit<F>) -> Result<FpElem<F>, CircuitError> {
173        Ok(FpElem {
174            p: (cs.witness(self.vars.0)?, cs.witness(self.vars.1)?),
175            m: self.m,
176            two_power_m: self.two_power_m,
177        })
178    }
179
180    /// Get the witness from the variables
181    pub fn witness(&self, cs: &PlonkCircuit<F>) -> Result<F, CircuitError> {
182        Ok(cs.witness(self.vars.0)? + cs.witness(self.vars.1)? * self.two_power_m)
183    }
184
185    /// Expose the field element variables components
186    pub fn components(&self) -> (Variable, Variable) {
187        self.vars
188    }
189
190    /// Expose the m parameter
191    pub fn param_m(&self) -> usize {
192        self.m
193    }
194
195    /// Expose 2^m parameter
196    pub fn two_power_m(&self) -> F {
197        self.two_power_m
198    }
199
200    /// An FpElemVar that represents a 0
201    pub fn zero(cs: &PlonkCircuit<F>, m: usize, two_power_m: Option<F>) -> Self {
202        FpElemVar {
203            vars: (cs.zero(), cs.zero()),
204            m,
205            two_power_m: match two_power_m {
206                Some(p) => p,
207                None => F::from(2u8).pow([m as u64]),
208            },
209        }
210    }
211
212    /// An FpElemVar that represents a 1
213    pub fn one(cs: &PlonkCircuit<F>, m: usize, two_power_m: Option<F>) -> Self {
214        FpElemVar {
215            vars: (cs.one(), cs.zero()),
216            m,
217            two_power_m: match two_power_m {
218                Some(p) => p,
219                None => F::from(2u8).pow([m as u64]),
220            },
221        }
222    }
223
224    /// Enforce self == other.
225    pub fn enforce_equal(
226        &self,
227        circuit: &mut PlonkCircuit<F>,
228        other: &Self,
229    ) -> Result<(), CircuitError> {
230        if self.m != other.m || self.two_power_m != other.two_power_m {
231            return Err(CircuitError::ParameterError(
232                "m or two_power_m do not match".to_string(),
233            ));
234        }
235        circuit.enforce_equal(self.components().0, other.components().0)?;
236        circuit.enforce_equal(self.components().1, other.components().1)
237    }
238}
239
240impl<F: PrimeField> PlonkCircuit<F> {
241    /// Modular arithmetic gates
242    ///
243    /// Modular addition gate: compute y = var_1 + ... var_k mod p,
244    /// where k < range_size / 2, p << field_size / range_size.
245    /// Let l_p be the minimal integer such that range_size^l_p >= p,
246    /// witness[var_1], ..., witness[var_k] are guaranteed to be in [0,
247    /// range_size^l_p). Return error if any variables are invalid.
248    fn mod_add_internal(
249        &mut self,
250        vars: &[Variable],
251        p: F,
252        l_p: usize,
253    ) -> Result<Variable, CircuitError> {
254        let range_bit_len = self.range_bit_len()?;
255        let range_size = self.range_size()?;
256        let mut sum_x = F::zero();
257        for &var in vars.iter() {
258            sum_x += self.witness(var)?;
259        }
260        // perform integer division
261        let (z, y) = div_rem(&sum_x, &p);
262        let z_range = F::from(range_size as u32);
263        if z >= z_range {
264            return Err(ParameterError(format!(
265                "z = {z} is out of range, the sum of variable values = {sum_x} might be too large for modulus = {p}",
266            )));
267        }
268
269        // add range check gates
270        let z_var = self.create_variable(z)?;
271        // range check z \in [0, range_size)
272        self.range_gate_with_lookup(z_var, range_bit_len)?;
273        let y_var = self.create_variable(y)?;
274        // range check y \in [0, range_size^l_p)
275        self.range_gate_with_lookup(y_var, range_bit_len * l_p)?;
276
277        // add constraint: y = x_1 + ... + x_k - p * z
278        let mut padded = vec![z_var];
279        padded.extend(vars);
280        let rate = GATE_WIDTH - 1; // rate at which lc add each round
281        let padded_len = next_multiple(padded.len() - 1, rate)? + 1;
282        padded.resize(padded_len, self.zero());
283
284        let coeffs = [F::one(), F::one(), F::one(), F::one()];
285        let mut accum = padded[padded_len - 1];
286        for i in 1..padded_len / rate {
287            accum = self.lc(
288                &[
289                    accum,
290                    padded[padded_len - 1 - rate * i + 2],
291                    padded[padded_len - 1 - rate * i + 1],
292                    padded[padded_len - 1 - rate * i],
293                ],
294                &coeffs,
295            )?;
296        }
297        // final round
298        let coeffs = [F::one(), F::one(), F::one(), p.neg()];
299        let wires = [accum, padded[2], padded[1], padded[0], y_var];
300        self.lc_gate(&wires, &coeffs)?;
301
302        Ok(y_var)
303    }
304
305    /// Modular addition gate:
306    /// Given Fp elements x, y and modulus p, compute z = x + y mod p
307    pub fn mod_add(
308        &mut self,
309        x: &FpElemVar<F>,
310        y: &FpElemVar<F>,
311        p: &FpElem<F>,
312    ) -> Result<FpElemVar<F>, CircuitError> {
313        let range_bit_len = self.range_bit_len()?;
314        self.check_var_bound(x.vars.0)?;
315        self.check_var_bound(x.vars.1)?;
316        self.check_var_bound(y.vars.0)?;
317        self.check_var_bound(y.vars.1)?;
318
319        if x.m != p.m || y.m != p.m {
320            return Err(ParameterError(format!(
321                "field elements splitting parameters do not match: x.m = {}, y.m = {}, p.m = {}",
322                x.m, y.m, p.m
323            )));
324        }
325        if x.two_power_m != p.two_power_m || y.two_power_m != p.two_power_m {
326            return Err(ParameterError(format!(
327                "field elements splitting parameters do not match: x.2^m = {}, y.2^m = {}, p.2^m = {}",
328                x.two_power_m, y.two_power_m, p.two_power_m
329            ))
330            );
331        }
332        if p.m % range_bit_len != 0 {
333            return Err(ParameterError(format!(
334                "splitting parameter m = {} is not a multiple of range_bit_len",
335                p.m
336            )));
337        }
338
339        let x_var = x.convert_to_var(self)?;
340        let y_var = y.convert_to_var(self)?;
341
342        let num_range_blocks = self.num_range_blocks()?;
343        let res = self.mod_add_internal(&[x_var, y_var], p.field_elem(), num_range_blocks)?;
344
345        FpElemVar::new_unchecked(self, res, x.m, Some(p.two_power_m))
346    }
347
348    /// Modular addition gate:
349    /// Given input
350    ///  x: Fp element variable,
351    ///  y: Fp element, and
352    ///  modulus p: Fp element,
353    /// use y as a constant and
354    /// compute z = x + y mod p
355    pub fn mod_add_constant(
356        &mut self,
357        x: &FpElemVar<F>,
358        y: &FpElem<F>,
359        p: &FpElem<F>,
360    ) -> Result<FpElemVar<F>, CircuitError> {
361        let range_bit_len = self.range_bit_len()?;
362        let range_size = self.range_size()?;
363        self.check_var_bound(x.vars.0)?;
364        self.check_var_bound(x.vars.1)?;
365
366        if x.m != p.m || y.m != p.m {
367            return Err(ParameterError(format!(
368                "field elements splitting parameters do not match: x.m = {}, y.m = {}, p.m = {}",
369                x.m, y.m, p.m
370            )));
371        }
372        if x.two_power_m != p.two_power_m || y.two_power_m != p.two_power_m {
373            return Err(ParameterError(format!(
374                "field elements splitting parameters do not match: x.2^m = {}, y.2^m = {}, p.2^m = {}",
375                x.two_power_m, y.two_power_m, p.two_power_m
376            ))
377            );
378        }
379        if p.m % range_bit_len != 0 {
380            return Err(ParameterError(format!(
381                "splitting parameter m = {} is not a multiple of range_bit_len",
382                p.m
383            )));
384        }
385        // ==============================================
386        // prepare the variables and constants
387        // ==============================================
388        let x_var = x.convert_to_var(self)?;
389        let y_f = y.field_elem();
390        let p_f = p.field_elem();
391
392        // perform integer division
393        let sum = self.witness(x_var)? + y_f;
394        let (divisor, remainder) = div_rem(&sum, &p_f);
395
396        let divisor_range = F::from(range_size as u32);
397        if divisor >= divisor_range {
398            return Err(ParameterError(format!(
399              "divisor = {divisor} is out of range, the sum of variable values = {sum} might be too large for modulus = {p_f}",
400          ))
401          );
402        }
403
404        // ==============================================
405        // now we need to prove a quadratic equation
406        //   x + y - p * divisor = remainder
407        // with the following map
408        //  var1: x
409        //  var2: remainder
410        //  var3: p
411        //  var4: divisor
412        //  var_output: 0
413        //  constant: y
414        // ==============================================
415
416        // add range check gates
417        let divisor_var = self.create_variable(divisor)?;
418        // range check divisor \in [0, range_size)
419        self.range_gate_with_lookup(divisor_var, range_bit_len)?;
420
421        // range check remainder \in [0, range_size^l_p)
422        let remainder_var = self.create_variable(remainder)?;
423        let num_range_blocks = self.num_range_blocks()?;
424        self.range_gate_with_lookup(remainder_var, range_bit_len * num_range_blocks)?;
425
426        // add constraint: x - remainder - p * divisor  + y = 0
427        let wires = [x_var, remainder_var, divisor_var, self.zero(), self.zero()];
428        let q_lc = [F::one(), -F::one(), -p_f, F::zero()];
429        let q_mul = [F::zero(), F::zero()];
430        let q_o = F::zero();
431        let q_c = y_f;
432
433        self.quad_poly_gate(&wires, &q_lc, &q_mul, q_o, q_c)?;
434
435        FpElemVar::new_unchecked(self, remainder_var, x.m, Some(p.two_power_m))
436    }
437
438    /// Modular addition gate:
439    /// Given Fp elements &\[x\] and modulus p, compute z = \sum x mod p
440    pub fn mod_add_vec(
441        &mut self,
442        x: &[FpElemVar<F>],
443        p: &FpElem<F>,
444    ) -> Result<FpElemVar<F>, CircuitError> {
445        let range_bit_len = self.range_bit_len()?;
446        for e in x {
447            if e.m != p.m {
448                return Err(ParameterError(format!(
449                    "field elements splitting parameters do not match: x.m = {}, p.m = {}",
450                    e.m, p.m
451                )));
452            }
453
454            if e.two_power_m != p.two_power_m {
455                return Err(ParameterError(format!(
456                    "field elements splitting parameters do not match: x.2^m = {}, p.2^m = {}",
457                    e.two_power_m, p.two_power_m
458                )));
459            }
460        }
461
462        if p.m % range_bit_len != 0 {
463            return Err(ParameterError(format!(
464                "splitting parameter m = {} is not a multiple of range_bit_len",
465                p.m
466            )));
467        }
468
469        let x_vars: Vec<Variable> = x
470            .iter()
471            .map(|y| y.convert_to_var(self))
472            .collect::<Result<Vec<Variable>, _>>()?;
473
474        let num_range_blocks = self.num_range_blocks()?;
475        let res = self.mod_add_internal(x_vars.as_ref(), p.field_elem(), num_range_blocks)?;
476
477        FpElemVar::new_unchecked(self, res, p.m, Some(p.two_power_m))
478    }
479
480    /// Modular multiplication gate:
481    /// Given Fp elements x, y and modulus p, compute z = x * y mod p.
482    #[allow(clippy::many_single_char_names)]
483    pub fn mod_mul(
484        &mut self,
485        x: &FpElemVar<F>,
486        y: &FpElemVar<F>,
487        p: &FpElem<F>,
488    ) -> Result<FpElemVar<F>, CircuitError> {
489        let range_bit_len = self.range_bit_len()?;
490        if x.m != p.m || y.m != p.m {
491            return Err(ParameterError(format!(
492                "field elements splitting parameters do not match: x.m = {}, y.m = {}, p.m = {}",
493                x.m, y.m, p.m
494            )));
495        }
496        if x.two_power_m != p.two_power_m || y.two_power_m != p.two_power_m {
497            return Err(ParameterError(format!(
498                "field elements splitting parameters do not match: x.2^m = {}, y.2^m = {}, p.2^m = {}",
499                x.two_power_m, y.two_power_m, p.two_power_m
500            )));
501        }
502        if p.m % range_bit_len != 0 {
503            return Err(ParameterError(format!(
504                "splitting parameter m = {} is not a multiple of range_bit_len",
505                p.m
506            )));
507        }
508
509        // Witness computation
510        //
511        // compute integer values of x, y, and p
512        let two_power_m_int: BigUint = to_big_int!(p.two_power_m);
513        let x0_int: BigUint = to_big_int!(self.witness(x.vars.0)?);
514        let x1_int: BigUint = to_big_int!(self.witness(x.vars.1)?);
515        let y0_int: BigUint = to_big_int!(self.witness(y.vars.0)?);
516        let y1_int: BigUint = to_big_int!(self.witness(y.vars.1)?);
517        let p0_int: BigUint = to_big_int!(p.p.0);
518        let p1_int: BigUint = to_big_int!(p.p.1);
519        let x_int = &x0_int + &two_power_m_int * &x1_int;
520        let y_int = &y0_int + &two_power_m_int * &y1_int;
521        let p_int = &p0_int + &two_power_m_int * &p1_int;
522
523        // compute z = x * y mod p, and w s.t. z + w * p = x * y
524        let xy_int = &x_int * &y_int;
525        let w_int = &xy_int / &p_int;
526        let z_int = &xy_int - (&w_int * &p_int);
527        let w = FpElem::new(&F::from(w_int), p.m, Some(p.two_power_m))?;
528        let w0_int: BigUint = to_big_int!(w.p.0);
529        let w1_int: BigUint = to_big_int!(w.p.1);
530        let z = FpElem::new(&F::from(z_int), p.m, Some(p.two_power_m))?;
531        let z0_int = to_big_int!(z.p.0);
532        let z1_int = to_big_int!(z.p.1);
533
534        // now we have the following:
535        //      z + w * p = x * y
536        // which is
537        //             z0 + w0p0 - x0y0                     (0)
538        //   + 2^m  *( z1 + w0p1 + w1p0 - x0y1 - x1y0 )     (1)
539        //   + 2^2m *( w1p1 - x1y1 )                        (2)
540        //   = 0
541        //
542        // Eq.(0) will generate a carrier c0' that gets added to 2^m term
543        // Eq.(1) will generate a carrier c1' that gets added to 2^2m term
544
545        // compute carry values
546        //
547        // c0' := c0 - 2^m is the carrier for |  z0 + w0p0 - x0y0  |,
548        // we define variable c0 rather than c0' because c0 is guaranteed to be positive
549        let x0y0_int = &x0_int * &y0_int;
550        let z0_plus_p0w0_int = &z0_int + &p0_int * &w0_int;
551        let c0_int = if z0_plus_p0w0_int >= x0y0_int {
552            let carry0_int = (&z0_plus_p0w0_int - &x0y0_int) / &two_power_m_int;
553            &two_power_m_int + carry0_int
554        } else {
555            let carry0_int = (&x0y0_int - z0_plus_p0w0_int) / &two_power_m_int;
556            &two_power_m_int - carry0_int
557        };
558
559        // c1' := c1 - 2^{m+1} is the carrier for | z1 + w0p1 + w1p0 - x0y1 - x1y0 + c0|
560        // we define variable c1 rather than c1' because c1 is guaranteed to be positive
561        let a_int = &x0_int * &y1_int + &x1_int * &y0_int + &two_power_m_int;
562        let b_int = &z1_int + &p0_int * &w1_int + &p1_int * &w0_int + &c0_int;
563        let c1_int = if b_int >= a_int {
564            let carry1_int = (b_int - a_int) / &two_power_m_int;
565            &two_power_m_int + &two_power_m_int + carry1_int
566        } else {
567            let carry1_int = (a_int - b_int) / &two_power_m_int;
568            &two_power_m_int + &two_power_m_int - carry1_int
569        };
570
571        // with the carriers, we translate
572        //      z + w * p = x * y
573        // into
574        //             z0 + w0p0 - x0y0 - 2^m c0'                        (3)
575        //   + 2^m  *( z1 + w0p1 + w1p0 - x0y1 - x1y0 + c0' - 2^m c1' )  (4)
576        //   + 2^2m *( w1p1 - x1y1 + c1' )                               (5)
577        //   = 0
578        // and we are able to choose c0' \in [-2^m, 2^{m+1}], c1' \in [-2^{m+1},
579        // 2^{m+2}] so that formulas (3), (4), (5) equal zero respectively.
580
581        // create variables and add range_checks
582        let w0_var = self.create_variable(F::from(w0_int))?;
583        let w1_var = self.create_variable(F::from(w1_int))?;
584        let z0_var = self.create_variable(F::from(z0_int))?;
585        let z1_var = self.create_variable(F::from(z1_int))?;
586        let c0_var = self.create_variable(F::from(c0_int))?;
587        let c1_var = self.create_variable(F::from(c1_int))?;
588        self.range_gate_with_lookup(w0_var, p.m)?;
589        self.range_gate_with_lookup(w1_var, p.m)?;
590        self.range_gate_with_lookup(z0_var, p.m)?;
591        self.range_gate_with_lookup(z1_var, p.m)?;
592        self.range_gate_with_lookup(c0_var, p.m + range_bit_len)?;
593        self.range_gate_with_lookup(c1_var, p.m + range_bit_len)?;
594
595        // add remaining gates
596        //
597        // ==============================================
598        // Eq.(3): z0 + w0p0 - x0y0 - 2^m c0' = 0 where c0' := c0 - 2^m
599        // ==============================================
600        // x0y0 - p0w0 + 2^m * c0 - 2^{2m} = z0
601        let wires = [x.vars.0, y.vars.0, w0_var, c0_var, z0_var];
602        let q_lin = [F::zero(), F::zero(), -p.p.0, p.two_power_m];
603        let q_mul = [F::one(), F::zero()];
604        let q_o = F::one();
605        let q_c = -p.two_power_m.square();
606        self.quad_poly_gate(&wires, &q_lin, &q_mul, q_o, q_c)?;
607
608        // ==============================================
609        // Eq.(4): z1 + w0p1 + w1p0 - x0y1 - x1y0 + c0' - 2^m c1' = 0
610        // which is
611        //  t1 + 2^m * c1' = z1 + t2 + c0' (4.1)
612        // where
613        //  t1 = x0y1 + x1y0  (4.2)
614        //  t2 = p0w1 + p1w0  (4.3)
615        // ==============================================
616
617        // Eq.(4.2): x0y1 + x1y0 = t1
618        let wires_in = [x.vars.0, y.vars.1, x.vars.1, y.vars.0];
619        let q_mul = [F::one(), F::one()];
620        let t1_var = self.mul_add(&wires_in, &q_mul)?;
621
622        // Eq.(4.3): p0w1 + p1w0 = t2
623        let wires_in = [w1_var, w0_var, self.zero(), self.zero()];
624        let q_lc = [p.p.0, p.p.1, F::zero(), F::zero()];
625        let t2_var = self.lc(&wires_in, &q_lc)?;
626
627        // ===============================================
628        // Eq.(4.1): t1 + 2^m * c1' = z1 + t2 + c0',
629        // where c0' := c0 - 2^m and c1' := c1 - 2^{m+1}
630        // ===============================================
631        // t1 - t2 - c0 + 2^m * c1 - 2^{2m+1} + 2^m = z1
632        let wires = [t1_var, t2_var, c0_var, c1_var, z1_var];
633        let q_lin = [F::one(), -F::one(), -F::one(), p.two_power_m];
634        let q_mul = [F::zero(), F::zero()];
635        let q_o = F::one();
636        let q_c = p.two_power_m - p.two_power_m.square().double();
637        self.quad_poly_gate(&wires, &q_lin, &q_mul, q_o, q_c)?;
638
639        // ==============================================
640        // Eq.(5): w1p1 - x1y1 + c1' = 0 where c1' := c1 - 2^{m+1}
641        // ==============================================
642        // x1y1 - p1w1 + 2^{m+1} = c1
643        let wires = [x.vars.1, y.vars.1, w1_var, self.zero(), c1_var];
644        let q_lin = [F::zero(), F::zero(), -p.p.1, F::zero()];
645        let q_mul = [F::one(), F::zero()];
646        let q_o = F::one();
647        let q_c = p.two_power_m.double();
648        self.quad_poly_gate(&wires, &q_lin, &q_mul, q_o, q_c)?;
649
650        Ok(FpElemVar {
651            vars: (z0_var, z1_var),
652            m: p.m,
653            two_power_m: p.two_power_m,
654        })
655    }
656
657    /// Modular multiplication gate:
658    /// Given input
659    ///  x: Fp element variable,
660    ///  y: Fp element, and
661    ///  modulus p: Fp element,
662    /// use y as a constant
663    /// compute z = x * y mod p
664    #[allow(clippy::many_single_char_names)]
665    pub fn mod_mul_constant(
666        &mut self,
667        x: &FpElemVar<F>,
668        y: &FpElem<F>,
669        p: &FpElem<F>,
670    ) -> Result<FpElemVar<F>, CircuitError> {
671        let range_bit_len = self.range_bit_len()?;
672        if x.m != p.m || y.m != p.m {
673            return Err(ParameterError(format!(
674                "field elements splitting parameters do not match: x.m = {}, y.m = {}, p.m = {}",
675                x.m, y.m, p.m
676            )));
677        }
678        if x.two_power_m != p.two_power_m || y.two_power_m != p.two_power_m {
679            return Err(ParameterError(format!(
680                "field elements splitting parameters do not match: x.2^m = {}, y.2^m = {}, p.2^m = {}",
681                x.two_power_m, y.two_power_m, p.two_power_m
682            )));
683        }
684        if p.m % range_bit_len != 0 {
685            return Err(ParameterError(format!(
686                "splitting parameter m = {} is not a multiple of range_bit_len",
687                p.m
688            )));
689        }
690
691        // Witness computation
692        //
693        // compute integer values of x, y, and p
694        let two_power_m_int: BigUint = to_big_int!(p.two_power_m);
695        let x0_int: BigUint = to_big_int!(self.witness(x.vars.0)?);
696        let x1_int: BigUint = to_big_int!(self.witness(x.vars.1)?);
697        let y0_int: BigUint = to_big_int!(y.p.0);
698        let y1_int: BigUint = to_big_int!(y.p.1);
699        let p0_int: BigUint = to_big_int!(p.p.0);
700        let p1_int: BigUint = to_big_int!(p.p.1);
701        let x_int = &x0_int + &two_power_m_int * &x1_int;
702        let y_int = &y0_int + &two_power_m_int * &y1_int;
703        let p_int = &p0_int + &two_power_m_int * &p1_int;
704
705        // compute z = x * y mod p, and w s.t. z + w * p = x * y
706        let xy_int = &x_int * &y_int;
707        let w_int = &xy_int / &p_int;
708        let z_int = &xy_int - (&w_int * &p_int);
709        let w = FpElem::new(&F::from(w_int), p.m, Some(p.two_power_m))?;
710        let w0_int: BigUint = to_big_int!(w.p.0);
711        let w1_int: BigUint = to_big_int!(w.p.1);
712        let z = FpElem::new(&F::from(z_int), p.m, Some(p.two_power_m))?;
713        let z0_int = to_big_int!(z.p.0);
714        let z1_int = to_big_int!(z.p.1);
715
716        // now we have the following:
717        //      z + w * p = x * y
718        // which is
719        //             z0 + w0p0 - x0y0                     (0)
720        //   + 2^m  *( z1 + w0p1 + w1p0 - x0y1 - x1y0 )     (1)
721        //   + 2^2m *( w1p1 - x1y1 )                        (2)
722        //   = 0
723        //
724        // Eq.(0) will generate a carrier c0' that gets added to 2^m term
725        // Eq.(1) will generate a carrier c1' that gets added to 2^2m term
726
727        // compute carry values
728        //
729        // c0' := c0 - 2^m is the carrier for |  z0 + w0p0 - x0y0  |,
730        // we define variable c0 rather than c0' because c0 is guaranteed to be positive
731        let x0y0_int = &x0_int * &y0_int;
732        let z0_plus_p0w0_int = &z0_int + &p0_int * &w0_int;
733        let c0_int = if z0_plus_p0w0_int >= x0y0_int {
734            let carry0_int = (&z0_plus_p0w0_int - &x0y0_int) / &two_power_m_int;
735            &two_power_m_int + carry0_int
736        } else {
737            let carry0_int = (&x0y0_int - z0_plus_p0w0_int) / &two_power_m_int;
738            &two_power_m_int - carry0_int
739        };
740
741        // c1' := c1 - 2^{m+1} is the carrier for | z1 + w0p1 + w1p0 - x0y1 - x1y0 + c0|
742        // we define variable c1 rather than c1' because c1 is guaranteed to be positive
743        let a_int = &x0_int * &y1_int + &x1_int * &y0_int + &two_power_m_int;
744        let b_int = &z1_int + &p0_int * &w1_int + &p1_int * &w0_int + &c0_int;
745        let c1_int = if b_int >= a_int {
746            let carry1_int = (b_int - a_int) / &two_power_m_int;
747            &two_power_m_int + &two_power_m_int + carry1_int
748        } else {
749            let carry1_int = (a_int - b_int) / &two_power_m_int;
750            &two_power_m_int + &two_power_m_int - carry1_int
751        };
752
753        // with the carriers, we translate
754        //      z + w * p = x * y
755        // into
756        //             z0 + w0p0 - x0y0 - 2^m c0'                        (3)
757        //   + 2^m  *( z1 + w0p1 + w1p0 - x0y1 - x1y0 + c0' - 2^m c1' )  (4)
758        //   + 2^2m *( w1p1 - x1y1 + c1' )                               (5)
759        //   = 0
760        // and we are able to choose c0' \in [-2^m, 2^{m+1}], c1' \in [-2^{m+1},
761        // 2^{m+2}] so that formulas (3), (4), (5) equal zero respectively.
762
763        // create variables and add range_checks
764        let w0_var = self.create_variable(F::from(w0_int))?;
765        let w1_var = self.create_variable(F::from(w1_int))?;
766        let z0_var = self.create_variable(F::from(z0_int))?;
767        let z1_var = self.create_variable(F::from(z1_int))?;
768        let c0_var = self.create_variable(F::from(c0_int))?;
769        let c1_var = self.create_variable(F::from(c1_int))?;
770        self.range_gate_with_lookup(w0_var, p.m)?;
771        self.range_gate_with_lookup(w1_var, p.m)?;
772        self.range_gate_with_lookup(z0_var, p.m)?;
773        self.range_gate_with_lookup(z1_var, p.m)?;
774        self.range_gate_with_lookup(c0_var, p.m + range_bit_len)?;
775        self.range_gate_with_lookup(c1_var, p.m + range_bit_len)?;
776
777        // add remaining gates
778        //
779        // ==============================================
780        // Eq.(3): z0 + w0p0 - x0y0 - 2^m c0' = 0 where c0' := c0 - 2^m
781        // Note: this use same number of constraints as mul_mod
782        // ==============================================
783        // y0x0 - p0w0 + 2^m * c0 - z0 - 2^{2m} = 0
784        let wires = [x.vars.0, w0_var, c0_var, z0_var, self.zero()];
785        let q_lin = [y.p.0, -p.p.0, p.two_power_m, -F::one()];
786        let q_mul = [F::zero(), F::zero()];
787        let q_o = F::zero();
788        let q_c = -p.two_power_m.square();
789        self.quad_poly_gate(&wires, &q_lin, &q_mul, q_o, q_c)?;
790
791        // ==============================================
792        // Eq.(4): z1 + w0p1 + w1p0 - x0y1 - x1y0 + c0' - 2^m c1' = 0
793        // which is
794        //  t + 2^m * c1' = z1 + c0' (4.1)
795        // where
796        //  t = x0y1 + x1y0 -  p0w1 - p1w0 (4.2)
797        // Note: this use one less constraint than mul_mod
798        // ==============================================
799
800        // Eq.(4.2): t = x0y1 + x1y0 - p0w1 - p1w0
801        let wires_in = [x.vars.0, x.vars.1, w1_var, w0_var];
802        let coeffs = [y.p.1, y.p.0, -p.p.0, -p.p.1];
803        let t1_var = self.lc(&wires_in, &coeffs)?;
804
805        // ===============================================
806        // Eq.(4.1): t + 2^m * c1' = z1 + c0',
807        // where c0' := c0 - 2^m and c1' := c1 - 2^{m+1}
808        // ===============================================
809        // t - z1 - c0 + 2^m * c1 - 2^{2m+1} + 2^m = 0
810        let wires = [t1_var, z1_var, c0_var, c1_var, self.zero()];
811        let q_lin = [F::one(), -F::one(), -F::one(), p.two_power_m];
812        let q_mul = [F::zero(), F::zero()];
813        let q_o = F::zero();
814        let q_c = p.two_power_m - p.two_power_m.square().double();
815        self.quad_poly_gate(&wires, &q_lin, &q_mul, q_o, q_c)?;
816
817        // ==============================================
818        // Eq.(5): w1p1 - x1y1 + c1' = 0 where c1' := c1 - 2^{m+1}
819        // ==============================================
820        // x1y1 - p1w1 - c1 + 2^{m+1} = 0
821        let wires = [x.vars.1, w1_var, c1_var, self.zero(), self.zero()];
822        let q_lin = [y.p.1, -p.p.1, -F::one(), F::zero()];
823        let q_mul = [F::zero(), F::zero()];
824        let q_o = F::zero();
825        let q_c = p.two_power_m.double();
826        self.quad_poly_gate(&wires, &q_lin, &q_mul, q_o, q_c)?;
827
828        Ok(FpElemVar {
829            vars: (z0_var, z1_var),
830            m: p.m,
831            two_power_m: p.two_power_m,
832        })
833    }
834
835    /// Negate an FpElemVar mod p where p is a public variable which is
836    /// also the modulus for the FpElem element.
837    pub fn mod_negate(&mut self, x: &FpElemVar<F>, p: &F) -> Result<FpElemVar<F>, CircuitError> {
838        let range_bit_len = self.range_bit_len()?;
839        if x.m % range_bit_len != 0 {
840            return Err(ParameterError(format!(
841                "splitting parameter m = {} is not a multiple of range_bit_len",
842                x.m
843            )));
844        }
845        // Witness computation
846        let two_power_m_int: BigUint = to_big_int!(x.two_power_m);
847        let x0_int: BigUint = to_big_int!(self.witness(x.vars.0)?);
848        let x1_int: BigUint = to_big_int!(self.witness(x.vars.1)?);
849        let p_int: BigUint = to_big_int!(p);
850        let x_int = &x0_int + &two_power_m_int * &x1_int;
851        if x_int >= p_int {
852            return Err(CircuitError::FieldAlgebraError(
853                "non native field overflow".to_string(),
854            ));
855        }
856        let x_negate = F::from(p_int - x_int);
857
858        // variables
859        let x_var = x.convert_to_var(self)?;
860        let x_neg_var = self.create_variable(x_negate)?;
861
862        let wires = [x_var, x_neg_var, self.one(), self.zero(), self.zero()];
863        let coeffs = [F::one(), F::one(), -*p, F::zero()];
864
865        self.lc_gate(&wires, &coeffs)?;
866
867        FpElemVar::new_unchecked(self, x_neg_var, x.m, Some(x.two_power_m))
868    }
869}
870
871#[inline]
872// Integer division: c = a / b
873fn int_div<F: PrimeField>(a: &F, b: &F) -> F {
874    let c_big_int: BigUint = a.into_bigint().into() / b.into_bigint().into();
875    F::from(c_big_int)
876}
877
878#[inline]
879// Return (a / b, a % b)
880fn div_rem<F: PrimeField>(a: &F, b: &F) -> (F, F) {
881    let div = int_div(a, b);
882    let rem = *a - *b * div;
883    (div, rem)
884}
885
886#[cfg(test)]
887mod test {
888    use super::*;
889    use crate::gadgets::test_utils::test_variable_independence_for_circuit;
890    use ark_bls12_377::{Fq as Fq377, Fr as Fr377};
891    use ark_ed_on_bls12_377::{Fq as FqEd377, Fr as FrEd377};
892    use ark_ed_on_bls12_381::Fq as FqEd381;
893    use ark_ed_on_bn254::{Fq as FqEd254, Fr as FrEd254};
894    use ark_ff::BigInteger;
895    use ark_std::rand::Rng;
896    use jf_utils::{field_switching, test_rng};
897
898    const RANGE_BIT_LEN_FOR_TEST: usize = 16;
899    const RANGE_SIZE_FOR_TEST: usize = 65536;
900
901    #[test]
902    fn test_fp_elem() -> Result<(), CircuitError> {
903        test_fp_elem_helper::<FqEd254>()?;
904        test_fp_elem_helper::<FqEd377>()?;
905        test_fp_elem_helper::<FqEd381>()?;
906        test_fp_elem_helper::<Fq377>()
907    }
908    // Test FpElem creation and conversion
909    fn test_fp_elem_helper<F: PrimeField>() -> Result<(), CircuitError> {
910        let mut rng = test_rng();
911        let p = int_div(&F::rand(&mut rng), &F::from(4u8));
912
913        // case 1: m = len(|F|) / 2
914        let m = F::MODULUS_BIT_SIZE as usize / 2;
915        let two_power_m = F::from(2u8).pow([m as u64]);
916        let fp_elem = FpElem::new(&p, m, Some(two_power_m))?;
917        assert!(fp_elem.p.0 < two_power_m, "p0 larger than 2^m");
918        assert!(fp_elem.p.1 < two_power_m, "p1 larger than 2^m");
919        let q = fp_elem.field_elem();
920        assert_eq!(p, q, "FpElem conversion failure");
921
922        // case 2: m = 0
923        let fp_elem = FpElem::new(&p, 0, Some(two_power_m))?;
924        let q = fp_elem.field_elem();
925        assert_eq!(p, q, "FpElem conversion failure when m = 0");
926
927        // case 3: m > len(|F|) / 2
928        let m = F::MODULUS_BIT_SIZE as usize / 2 + 1;
929        assert!(FpElem::new(&p, m, Some(two_power_m)).is_err());
930
931        Ok(())
932    }
933
934    #[test]
935    fn test_fp_elem_var() -> Result<(), CircuitError> {
936        test_fp_elem_var_helper::<FqEd254>()?;
937        test_fp_elem_var_helper::<FqEd377>()?;
938        test_fp_elem_var_helper::<FqEd381>()?;
939        test_fp_elem_var_helper::<Fq377>()
940    }
941    // Test FpElemVar variables creation and conversion
942    fn test_fp_elem_var_helper<F: PrimeField>() -> Result<(), CircuitError> {
943        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
944        let m = F::MODULUS_BIT_SIZE as usize / 2;
945        let mut rng = test_rng();
946
947        // Good path
948        let p = F::rand(&mut rng);
949        let p_var = circuit.create_variable(p)?;
950        let fp_elem_var = FpElemVar::new_unchecked(&mut circuit, p_var, m, None)?;
951        let q_var = fp_elem_var.convert_to_var(&mut circuit)?;
952        circuit.enforce_equal(p_var, q_var)?;
953        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
954
955        // Error path
956        *circuit.witness_mut(p_var) = F::zero();
957        assert!(circuit.check_circuit_satisfiability(&[]).is_err());
958
959        // check that circuit config is independent of witness values
960        let p1 = F::rand(&mut rng);
961        let p2 = F::rand(&mut rng);
962        let circuit_1 = build_fp_elem_var_circuit(p1, m, fp_elem_var.two_power_m)?;
963        let circuit_2 = build_fp_elem_var_circuit(p2, m, fp_elem_var.two_power_m)?;
964        test_variable_independence_for_circuit::<F>(circuit_1, circuit_2)?;
965
966        Ok(())
967    }
968    fn build_fp_elem_var_circuit<F: PrimeField>(
969        p: F,
970        m: usize,
971        two_power_m: F,
972    ) -> Result<PlonkCircuit<F>, CircuitError> {
973        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(2);
974        let p_var = circuit.create_variable(p)?;
975        let fp_elem_var = FpElemVar::new_unchecked(&mut circuit, p_var, m, Some(two_power_m))?;
976        let _ = fp_elem_var.convert_to_var(&mut circuit)?;
977        circuit.finalize_for_arithmetization()?;
978        Ok(circuit)
979    }
980
981    // ========================================
982    //  mod add internal
983    // ========================================
984
985    #[test]
986    fn test_mod_add_internal() -> Result<(), CircuitError> {
987        test_mod_add_internal_helper::<FqEd254>()?;
988        test_mod_add_internal_helper::<FqEd377>()?;
989        test_mod_add_internal_helper::<FqEd381>()?;
990        test_mod_add_internal_helper::<Fq377>()
991    }
992    fn test_mod_add_internal_helper<F: PrimeField>() -> Result<(), CircuitError> {
993        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
994
995        // Good paths
996        //
997        // 1 + ... + 10 mod 17 = 4
998        let p = F::from(17u8);
999        let vars: Vec<Variable> = (1..=10)
1000            .map(|i| circuit.create_variable(F::from(i as u8)))
1001            .collect::<Result<Vec<_>, CircuitError>>()?;
1002        let y_var = circuit.mod_add_internal(&vars, p, 1)?;
1003        assert_eq!(circuit.witness(y_var)?, F::from(4u8));
1004        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
1005
1006        // larger modulus: l_p = 10, p = 2^{160}
1007        let p = F::from(RANGE_SIZE_FOR_TEST as u32).pow([10u64]);
1008        let mut rng = test_rng();
1009        let vars: Vec<Variable> = (0..12)
1010            .map(|_| {
1011                circuit.create_variable(
1012                    int_div(&p, &F::from(2u8)) + F::from(rng.gen_range(0..u64::MAX)),
1013                )
1014            })
1015            .collect::<Result<Vec<_>, CircuitError>>()?;
1016        let y_var = circuit.mod_add_internal(&vars, p, 10)?;
1017        // y = x1 + ... + x12 - 6 * p
1018        let mut expected_y = F::zero();
1019        for &var in vars.iter() {
1020            expected_y += circuit.witness(var)?;
1021        }
1022        expected_y -= F::from(6u8) * p;
1023        assert_eq!(circuit.witness(y_var)?, expected_y);
1024        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
1025
1026        // Error paths
1027        //
1028        // bad output witness
1029        *circuit.witness_mut(y_var) = F::zero();
1030        assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1031        *circuit.witness_mut(y_var) = p + F::one();
1032        assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1033
1034        *circuit.witness_mut(y_var) = expected_y;
1035        // input witnesses are larger than the modulus
1036        let range_size = F::from(RANGE_SIZE_FOR_TEST as u32);
1037        let bad_x_var = circuit.create_variable(range_size * p)?;
1038        assert!(circuit
1039            .mod_add_internal(&[bad_x_var, bad_x_var], p, 10)
1040            .is_err());
1041
1042        // check that circuit config is independent of witness values
1043        let elems1: Vec<F> = (0..3)
1044            .map(|_| int_div(&p, &F::from(3u8)) + F::from(rng.gen_range(0..u64::MAX)))
1045            .collect();
1046        let elems2: Vec<F> = (0..3)
1047            .map(|_| int_div(&p, &F::from(3u8)) + F::from(rng.gen_range(0..u64::MAX)))
1048            .collect();
1049        let circuit_1 = build_mod_add_internal_circuit(&elems1, p, 10)?;
1050        let circuit_2 = build_mod_add_internal_circuit(&elems2, p, 10)?;
1051        test_variable_independence_for_circuit::<F>(circuit_1, circuit_2)?;
1052
1053        Ok(())
1054    }
1055    fn build_mod_add_internal_circuit<F: PrimeField>(
1056        elems: &[F],
1057        p: F,
1058        l_p: usize,
1059    ) -> Result<PlonkCircuit<F>, CircuitError> {
1060        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(3);
1061        let vars: Vec<Variable> = elems
1062            .iter()
1063            .map(|&elem| circuit.create_variable(elem))
1064            .collect::<Result<Vec<_>, CircuitError>>()?;
1065        circuit.mod_add_internal(&vars, p, l_p)?;
1066        circuit.finalize_for_arithmetization()?;
1067        Ok(circuit)
1068    }
1069
1070    // ========================================
1071    //  mod mul
1072    // ========================================
1073    #[test]
1074    fn test_mod_mul() -> Result<(), CircuitError> {
1075        test_mod_mul_helper::<FqEd254>()?;
1076        test_mod_mul_helper::<FqEd377>()?;
1077        test_mod_mul_helper::<FqEd381>()?;
1078        test_mod_mul_helper::<Fq377>()
1079    }
1080    fn test_mod_mul_helper<F: PrimeField>() -> Result<(), CircuitError> {
1081        let p = F::from(RANGE_SIZE_FOR_TEST as u32).pow([10u64]);
1082        let m = 80;
1083        let p_split = FpElem::new(&p, m, None)?;
1084        let mut rng = test_rng();
1085        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
1086
1087        for _ in 0..10 {
1088            let x_var = circuit.create_variable(p - F::from(rng.gen_range(1..u128::MAX)))?;
1089            let x_split_vars =
1090                FpElemVar::new_unchecked(&mut circuit, x_var, m, Some(p_split.two_power_m))?;
1091            let y_var = circuit.create_variable(p - F::from(rng.gen_range(1..u128::MAX)))?;
1092            let y_split_vars =
1093                FpElemVar::new_unchecked(&mut circuit, y_var, m, Some(p_split.two_power_m))?;
1094            let z_split_vars = circuit.mod_mul(&x_split_vars, &y_split_vars, &p_split)?;
1095            assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
1096
1097            // bad witnesses
1098            *circuit.witness_mut(z_split_vars.vars.1) += F::one();
1099            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1100            *circuit.witness_mut(z_split_vars.vars.1) -= F::one();
1101            *circuit.witness_mut(z_split_vars.vars.1) += p_split.two_power_m;
1102            // range check should fail
1103            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1104            *circuit.witness_mut(z_split_vars.vars.1) -= p_split.two_power_m;
1105
1106            let z_var = z_split_vars.convert_to_var(&mut circuit)?;
1107            check_mod_mul(
1108                circuit.witness(z_var)?,
1109                circuit.witness(x_var)?,
1110                circuit.witness(y_var)?,
1111                &p,
1112            );
1113        }
1114
1115        // Other error paths
1116        //
1117        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
1118        // mismatched splitting parameters
1119        let zero_var = circuit.zero();
1120        let x_split_vars =
1121            FpElemVar::new_unchecked(&mut circuit, zero_var, m + 1, Some(p_split.two_power_m))?;
1122        let y_split_vars =
1123            FpElemVar::new_unchecked(&mut circuit, zero_var, m, Some(p_split.two_power_m))?;
1124        assert!(circuit
1125            .mod_mul(&x_split_vars, &y_split_vars, &p_split)
1126            .is_err());
1127        // p.m is not a multiple of RANGE_BIT_LEN_FOR_TEST
1128        let p_split_bad = FpElem::new(&p, m + 1, Some(p_split.two_power_m))?;
1129        let x_split_vars =
1130            FpElemVar::new_unchecked(&mut circuit, zero_var, m + 1, Some(p_split.two_power_m))?;
1131        let y_split_vars =
1132            FpElemVar::new_unchecked(&mut circuit, zero_var, m + 1, Some(p_split.two_power_m))?;
1133        assert!(circuit
1134            .mod_mul(&x_split_vars, &y_split_vars, &p_split_bad)
1135            .is_err());
1136
1137        // p.two_power_m is not  2^m
1138        let p_split_bad = FpElem::new(&p, m, Some(p_split.two_power_m + F::one()))?;
1139        let x_split_vars =
1140            FpElemVar::new_unchecked(&mut circuit, zero_var, m, Some(p_split.two_power_m))?;
1141        let y_split_vars =
1142            FpElemVar::new_unchecked(&mut circuit, zero_var, m, Some(p_split.two_power_m))?;
1143        assert!(circuit
1144            .mod_mul(&x_split_vars, &y_split_vars, &p_split_bad)
1145            .is_err());
1146
1147        // check that circuit config is independent of witness values
1148        let x1 = p - F::from(rng.gen_range(1..u128::MAX));
1149        let y1 = p - F::from(rng.gen_range(1..u128::MAX));
1150        let x2 = p - F::from(rng.gen_range(1..u128::MAX));
1151        let y2 = p - F::from(rng.gen_range(1..u128::MAX));
1152        let circuit_1 = build_mod_mul_circuit(&x1, &y1, &p_split)?;
1153        let circuit_2 = build_mod_mul_circuit(&x2, &y2, &p_split)?;
1154        test_variable_independence_for_circuit::<F>(circuit_1, circuit_2)?;
1155
1156        Ok(())
1157    }
1158    fn check_mod_mul<F: PrimeField>(z: F, x: F, y: F, p: &F) {
1159        let x_int: BigUint = to_big_int!(x);
1160        let y_int: BigUint = to_big_int!(y);
1161        let p_int: BigUint = to_big_int!(p);
1162        let xy_int = &x_int * &y_int;
1163        let w_int = &xy_int / &p_int;
1164        let z_int = &xy_int - (&w_int * &p_int);
1165        let expected_z = F::from(z_int);
1166        assert_eq!(z, expected_z);
1167    }
1168    fn build_mod_mul_circuit<F: PrimeField>(
1169        x: &F,
1170        y: &F,
1171        p: &FpElem<F>,
1172    ) -> Result<PlonkCircuit<F>, CircuitError> {
1173        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(5);
1174        let x_var = circuit.create_variable(*x)?;
1175        let x_split_vars = FpElemVar::new_unchecked(&mut circuit, x_var, p.m, Some(p.two_power_m))?;
1176        let y_var = circuit.create_variable(*y)?;
1177        let y_split_vars = FpElemVar::new_unchecked(&mut circuit, y_var, p.m, Some(p.two_power_m))?;
1178        circuit.mod_mul(&x_split_vars, &y_split_vars, p)?;
1179        circuit.finalize_for_arithmetization()?;
1180        Ok(circuit)
1181    }
1182
1183    // ========================================
1184    //  mod mul constant
1185    // ========================================
1186    #[test]
1187    fn test_mod_mul_constant() -> Result<(), CircuitError> {
1188        test_mod_mul_constant_helper::<FqEd254>()?;
1189        test_mod_mul_constant_helper::<FqEd377>()?;
1190        test_mod_mul_constant_helper::<FqEd381>()?;
1191        test_mod_mul_constant_helper::<Fq377>()
1192    }
1193    fn test_mod_mul_constant_helper<F: PrimeField>() -> Result<(), CircuitError> {
1194        let p = F::from(RANGE_SIZE_FOR_TEST as u32).pow([10u64]);
1195        let m = 80;
1196        let p_split = FpElem::new(&p, m, None)?;
1197        let mut rng = test_rng();
1198        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
1199
1200        for _ in 0..10 {
1201            let x_var = circuit.create_variable(p - F::from(rng.gen_range(1..u128::MAX)))?;
1202            let x_split_vars =
1203                FpElemVar::new_unchecked(&mut circuit, x_var, m, Some(p_split.two_power_m))?;
1204            let y = p - F::from(rng.gen_range(1..u128::MAX));
1205            let y_split = FpElem::new(&y, m, Some(p_split.two_power_m))?;
1206            let z_split_vars = circuit.mod_mul_constant(&x_split_vars, &y_split, &p_split)?;
1207            assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
1208
1209            // bad witnesses
1210            *circuit.witness_mut(z_split_vars.vars.1) += F::one();
1211            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1212            *circuit.witness_mut(z_split_vars.vars.1) -= F::one();
1213            *circuit.witness_mut(z_split_vars.vars.1) += p_split.two_power_m;
1214            // range check should fail
1215            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1216            *circuit.witness_mut(z_split_vars.vars.1) -= p_split.two_power_m;
1217
1218            let z_var = z_split_vars.convert_to_var(&mut circuit)?;
1219            check_mod_mul(circuit.witness(z_var)?, circuit.witness(x_var)?, y, &p);
1220        }
1221
1222        // Other error paths
1223        //
1224        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
1225        // mismatched splitting parameters
1226        let zero_var = circuit.zero();
1227        let x_split_vars =
1228            FpElemVar::new_unchecked(&mut circuit, zero_var, m + 1, Some(p_split.two_power_m))?;
1229        let y = p - F::from(rng.gen_range(1..u128::MAX));
1230        let y_split = FpElem::new(&y, m, Some(p_split.two_power_m))?;
1231        assert!(circuit
1232            .mod_mul_constant(&x_split_vars, &y_split, &p_split)
1233            .is_err());
1234        // p.m is not a multiple of RANGE_BIT_LEN_FOR_TEST
1235        let p_split_bad = FpElem::new(&p, m + 1, Some(p_split.two_power_m))?;
1236        let x_split_vars =
1237            FpElemVar::new_unchecked(&mut circuit, zero_var, m + 1, Some(p_split.two_power_m))?;
1238        let y = p - F::from(rng.gen_range(1..u128::MAX));
1239        let y_split = FpElem::new(&y, m + 1, Some(p_split.two_power_m))?;
1240        assert!(circuit
1241            .mod_mul_constant(&x_split_vars, &y_split, &p_split_bad)
1242            .is_err());
1243
1244        // p.two_power_m is not  2^m
1245        let p_split_bad = FpElem::new(&p, m, Some(p_split.two_power_m + F::one()))?;
1246        let x_split_vars =
1247            FpElemVar::new_unchecked(&mut circuit, zero_var, m, Some(p_split.two_power_m))?;
1248        let y = p - F::from(rng.gen_range(1..u128::MAX));
1249        let y_split = FpElem::new(&y, m, Some(p_split.two_power_m))?;
1250        assert!(circuit
1251            .mod_mul_constant(&x_split_vars, &y_split, &p_split_bad)
1252            .is_err());
1253
1254        // check that circuit config is independent of witness values
1255        let x1 = p - F::from(rng.gen_range(1..u128::MAX));
1256        let y1 = p - F::from(rng.gen_range(1..u128::MAX));
1257        let x2 = p - F::from(rng.gen_range(1..u128::MAX));
1258        let y2 = p - F::from(rng.gen_range(1..u128::MAX));
1259        let circuit_1 = build_mod_mul_constant_circuit(&x1, &y1, &p_split)?;
1260        let circuit_2 = build_mod_mul_constant_circuit(&x2, &y2, &p_split)?;
1261        test_variable_independence_for_circuit::<F>(circuit_1, circuit_2)?;
1262
1263        Ok(())
1264    }
1265    fn build_mod_mul_constant_circuit<F: PrimeField>(
1266        x: &F,
1267        y: &F,
1268        p: &FpElem<F>,
1269    ) -> Result<PlonkCircuit<F>, CircuitError> {
1270        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(5);
1271        let x_var = circuit.create_variable(*x)?;
1272        let x_split_vars = FpElemVar::new_unchecked(&mut circuit, x_var, p.m, Some(p.two_power_m))?;
1273        let y_split = FpElem::new(y, p.m, Some(p.two_power_m))?;
1274        circuit.mod_mul_constant(&x_split_vars, &y_split, p)?;
1275        circuit.finalize_for_arithmetization()?;
1276        Ok(circuit)
1277    }
1278
1279    // ========================================
1280    //  mod add
1281    // ========================================
1282    #[test]
1283    fn test_mod_add() -> Result<(), CircuitError> {
1284        test_mod_add_helper::<FqEd254>()?;
1285        test_mod_add_helper::<FqEd377>()?;
1286        test_mod_add_helper::<FqEd381>()?;
1287        test_mod_add_helper::<Fq377>()
1288    }
1289    fn test_mod_add_helper<F: PrimeField>() -> Result<(), CircuitError> {
1290        let p = F::from(RANGE_SIZE_FOR_TEST as u32).pow([10u64]);
1291        let m = 80;
1292        let p_split = FpElem::new(&p, m, None)?;
1293        let mut rng = test_rng();
1294        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
1295
1296        for _ in 0..10 {
1297            let x_var = circuit.create_variable(p - F::from(rng.gen_range(1..u128::MAX)))?;
1298            let x_split_vars =
1299                FpElemVar::new_unchecked(&mut circuit, x_var, m, Some(p_split.two_power_m))?;
1300            let y_var = circuit.create_variable(p - F::from(rng.gen_range(1..u128::MAX)))?;
1301            let y_split_vars =
1302                FpElemVar::new_unchecked(&mut circuit, y_var, m, Some(p_split.two_power_m))?;
1303            let z_split_vars = circuit.mod_add(&x_split_vars, &y_split_vars, &p_split)?;
1304            assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
1305
1306            // bad witnesses
1307            *circuit.witness_mut(z_split_vars.vars.1) += F::one();
1308            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1309            *circuit.witness_mut(z_split_vars.vars.1) -= F::one();
1310            *circuit.witness_mut(z_split_vars.vars.1) += p_split.two_power_m;
1311            // range check should fail
1312            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1313            *circuit.witness_mut(z_split_vars.vars.1) -= p_split.two_power_m;
1314
1315            let z_var = z_split_vars.convert_to_var(&mut circuit)?;
1316            check_mod_add(
1317                circuit.witness(z_var)?,
1318                circuit.witness(x_var)?,
1319                circuit.witness(y_var)?,
1320                &p,
1321            );
1322        }
1323
1324        // Other error paths
1325        //
1326        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
1327        // mismatched splitting parameters
1328        let zero_var = circuit.zero();
1329        let x_split_vars =
1330            FpElemVar::new_unchecked(&mut circuit, zero_var, m + 1, Some(p_split.two_power_m))?;
1331        let y_split_vars =
1332            FpElemVar::new_unchecked(&mut circuit, zero_var, m, Some(p_split.two_power_m))?;
1333        assert!(circuit
1334            .mod_add(&x_split_vars, &y_split_vars, &p_split)
1335            .is_err());
1336        // p.m is not a multiple of RANGE_BIT_LEN_FOR_TEST
1337        let p_split_bad = FpElem::new(&p, m + 1, Some(p_split.two_power_m))?;
1338        let x_split_vars =
1339            FpElemVar::new_unchecked(&mut circuit, zero_var, m + 1, Some(p_split.two_power_m))?;
1340        let y_split_vars =
1341            FpElemVar::new_unchecked(&mut circuit, zero_var, m + 1, Some(p_split.two_power_m))?;
1342        assert!(circuit
1343            .mod_add(&x_split_vars, &y_split_vars, &p_split_bad)
1344            .is_err());
1345        // p.two_power_m is not 2^m
1346        let p_split_bad = FpElem::new(&p, m, Some(p_split.two_power_m + F::one()))?;
1347        let x_split_vars =
1348            FpElemVar::new_unchecked(&mut circuit, zero_var, m, Some(p_split.two_power_m))?;
1349        let y_split_vars =
1350            FpElemVar::new_unchecked(&mut circuit, zero_var, m, Some(p_split.two_power_m))?;
1351        assert!(circuit
1352            .mod_add(&x_split_vars, &y_split_vars, &p_split_bad)
1353            .is_err());
1354
1355        // check that circuit config is independent of witness values
1356        let x1 = p - F::from(rng.gen_range(1..u128::MAX));
1357        let y1 = p - F::from(rng.gen_range(1..u128::MAX));
1358        let x2 = p - F::from(rng.gen_range(1..u128::MAX));
1359        let y2 = p - F::from(rng.gen_range(1..u128::MAX));
1360        let circuit_1 = build_mod_add_circuit(&x1, &y1, &p_split)?;
1361        let circuit_2 = build_mod_add_circuit(&x2, &y2, &p_split)?;
1362        test_variable_independence_for_circuit::<F>(circuit_1, circuit_2)?;
1363
1364        Ok(())
1365    }
1366    fn check_mod_add<F: PrimeField>(z: F, x: F, y: F, p: &F) {
1367        let x_int: BigUint = to_big_int!(x);
1368        let y_int: BigUint = to_big_int!(y);
1369        let p_int: BigUint = to_big_int!(p);
1370        let xy_int = &x_int + &y_int;
1371        let w_int = &xy_int / &p_int;
1372        let z_int = &xy_int - (&w_int * &p_int);
1373        let expected_z = F::from(z_int);
1374        assert_eq!(z, expected_z);
1375    }
1376    fn build_mod_add_circuit<F: PrimeField>(
1377        x: &F,
1378        y: &F,
1379        p: &FpElem<F>,
1380    ) -> Result<PlonkCircuit<F>, CircuitError> {
1381        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(5);
1382        let x_var = circuit.create_variable(*x)?;
1383        let x_split_vars = FpElemVar::new_unchecked(&mut circuit, x_var, p.m, Some(p.two_power_m))?;
1384        let y_var = circuit.create_variable(*y)?;
1385        let y_split_vars = FpElemVar::new_unchecked(&mut circuit, y_var, p.m, Some(p.two_power_m))?;
1386        circuit.mod_add(&x_split_vars, &y_split_vars, p)?;
1387        circuit.finalize_for_arithmetization()?;
1388        Ok(circuit)
1389    }
1390
1391    // ========================================
1392    //  mod add constant
1393    // ========================================
1394    #[test]
1395    fn test_mod_add_constant() -> Result<(), CircuitError> {
1396        test_mod_add_constant_helper::<FqEd254>()?;
1397        test_mod_add_constant_helper::<FqEd377>()?;
1398        test_mod_add_constant_helper::<FqEd381>()?;
1399        test_mod_add_constant_helper::<Fq377>()
1400    }
1401    fn test_mod_add_constant_helper<F: PrimeField>() -> Result<(), CircuitError> {
1402        let p = F::from(RANGE_SIZE_FOR_TEST as u32).pow([10u64]);
1403        let m = 80;
1404        let p_split = FpElem::new(&p, m, None)?;
1405        let mut rng = test_rng();
1406        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
1407
1408        // set up a test where a mod p will happen
1409        {
1410            let x = p - F::one();
1411            let y = F::from(2u8);
1412
1413            let x_var = circuit.create_variable(x)?;
1414            let x_split_vars =
1415                FpElemVar::new_unchecked(&mut circuit, x_var, m, Some(p_split.two_power_m))?;
1416            let y_split = FpElem::new(&y, m, Some(p_split.two_power_m))?;
1417
1418            let z_split_vars = circuit.mod_add_constant(&x_split_vars, &y_split, &p_split)?;
1419            assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
1420
1421            // bad witnesses
1422            *circuit.witness_mut(z_split_vars.vars.1) += F::one();
1423            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1424            *circuit.witness_mut(z_split_vars.vars.1) -= F::one();
1425            *circuit.witness_mut(z_split_vars.vars.1) += p_split.two_power_m;
1426            // range check should fail
1427            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1428            *circuit.witness_mut(z_split_vars.vars.1) -= p_split.two_power_m;
1429
1430            let z_var = z_split_vars.convert_to_var(&mut circuit)?;
1431
1432            check_mod_add_constant(circuit.witness(z_var)?, circuit.witness(x_var)?, y, &p);
1433        }
1434
1435        // random tests
1436        for _ in 0..10 {
1437            let x_var = circuit.create_variable(p - F::from(rng.gen_range(1..u128::MAX)))?;
1438            let x_split_vars =
1439                FpElemVar::new_unchecked(&mut circuit, x_var, m, Some(p_split.two_power_m))?;
1440            let y = p - F::from(rng.gen_range(1..u128::MAX));
1441            let y_split = FpElem::new(&y, m, Some(p_split.two_power_m))?;
1442
1443            let z_split_vars = circuit.mod_add_constant(&x_split_vars, &y_split, &p_split)?;
1444            assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
1445
1446            // bad witnesses
1447            *circuit.witness_mut(z_split_vars.vars.1) += F::one();
1448            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1449            *circuit.witness_mut(z_split_vars.vars.1) -= F::one();
1450            *circuit.witness_mut(z_split_vars.vars.1) += p_split.two_power_m;
1451            // range check should fail
1452            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1453            *circuit.witness_mut(z_split_vars.vars.1) -= p_split.two_power_m;
1454
1455            let z_var = z_split_vars.convert_to_var(&mut circuit)?;
1456            check_mod_add_constant(circuit.witness(z_var)?, circuit.witness(x_var)?, y, &p);
1457        }
1458
1459        // Other error paths
1460        //
1461        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(RANGE_BIT_LEN_FOR_TEST);
1462        // mismatched splitting parameters
1463        let zero_var = circuit.zero();
1464        let x_split_vars =
1465            FpElemVar::new_unchecked(&mut circuit, zero_var, m + 1, Some(p_split.two_power_m))?;
1466        let y_split = FpElem::new(
1467            &(p - F::from(rng.gen_range(1..u128::MAX))),
1468            m,
1469            Some(p_split.two_power_m),
1470        )?;
1471
1472        assert!(circuit
1473            .mod_add_constant(&x_split_vars, &y_split, &p_split)
1474            .is_err());
1475        // p.m is not a multiple of RANGE_BIT_LEN_FOR_TEST
1476        let p_split_bad = FpElem::new(&p, m + 1, Some(p_split.two_power_m))?;
1477        let x_split_vars =
1478            FpElemVar::new_unchecked(&mut circuit, zero_var, m + 1, Some(p_split.two_power_m))?;
1479        let y_split = FpElem::new(
1480            &(p - F::from(rng.gen_range(1..u128::MAX))),
1481            m + 1,
1482            Some(p_split.two_power_m),
1483        )?;
1484        assert!(circuit
1485            .mod_add_constant(&x_split_vars, &y_split, &p_split_bad)
1486            .is_err());
1487        // p.two_power_m is not 2^m
1488        let p_split_bad = FpElem::new(&p, m, Some(p_split.two_power_m + F::one()))?;
1489        let x_split_vars =
1490            FpElemVar::new_unchecked(&mut circuit, zero_var, m, Some(p_split.two_power_m))?;
1491        let y_split = FpElem::new(
1492            &(p - F::from(rng.gen_range(1..u128::MAX))),
1493            m,
1494            Some(p_split.two_power_m),
1495        )?;
1496        assert!(circuit
1497            .mod_add_constant(&x_split_vars, &y_split, &p_split_bad)
1498            .is_err());
1499
1500        // check that circuit config is independent of witness values
1501        let x1 = p - F::from(rng.gen_range(1..u128::MAX));
1502        let y1 = p - F::from(rng.gen_range(1..u128::MAX));
1503        let x2 = p - F::from(rng.gen_range(1..u128::MAX));
1504        let y2 = p - F::from(rng.gen_range(1..u128::MAX));
1505        let circuit_1 = build_mod_add_constant_circuit(&x1, &y1, &p_split)?;
1506        let circuit_2 = build_mod_add_constant_circuit(&x2, &y2, &p_split)?;
1507        test_variable_independence_for_circuit::<F>(circuit_1, circuit_2)?;
1508
1509        Ok(())
1510    }
1511    fn check_mod_add_constant<F: PrimeField>(z: F, x: F, y: F, p: &F) {
1512        let x_int: BigUint = to_big_int!(x);
1513        let y_int: BigUint = to_big_int!(y);
1514        let p_int: BigUint = to_big_int!(p);
1515        let xy_int = &x_int + &y_int;
1516        let w_int = &xy_int / &p_int;
1517        let z_int = &xy_int - (&w_int * &p_int);
1518        let expected_z = F::from(z_int);
1519        assert_eq!(z, expected_z);
1520    }
1521    fn build_mod_add_constant_circuit<F: PrimeField>(
1522        x: &F,
1523        y: &F,
1524        p: &FpElem<F>,
1525    ) -> Result<PlonkCircuit<F>, CircuitError> {
1526        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(5);
1527        let x_var = circuit.create_variable(*x)?;
1528        let x_split_vars = FpElemVar::new_unchecked(&mut circuit, x_var, p.m, Some(p.two_power_m))?;
1529        let y_split = FpElem::new(y, p.m, Some(p.two_power_m))?;
1530        circuit.mod_add_constant(&x_split_vars, &y_split, p)?;
1531        circuit.finalize_for_arithmetization()?;
1532        Ok(circuit)
1533    }
1534
1535    // ========================================
1536    //  mod negation
1537    // ========================================
1538    #[test]
1539    fn test_mod_negation() -> Result<(), CircuitError> {
1540        test_mod_negation_helper::<FqEd254, FrEd254>(126, 9)?;
1541        test_mod_negation_helper::<FqEd377, FrEd377>(126, 9)?;
1542        test_mod_negation_helper::<Fq377, Fr377>(128, 16)
1543
1544        // cannot test for the following set up since 127 is a prime
1545        // test_mod_negation_helper::<FqEd381, FrEd381>(127, xx)?;
1546    }
1547    fn test_mod_negation_helper<F: PrimeField, T: PrimeField>(
1548        m: usize,
1549        range_bit_len: usize,
1550    ) -> Result<(), CircuitError> {
1551        let p = F::from_le_bytes_mod_order(T::MODULUS.to_bytes_le().as_ref());
1552        let p_split = FpElem::new(&p, m, None)?;
1553        let mut rng = test_rng();
1554        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(range_bit_len);
1555
1556        for _ in 0..10 {
1557            let x = T::rand(&mut rng);
1558            let x_var = circuit.create_variable(field_switching(&x))?;
1559            let x_split_vars =
1560                FpElemVar::new_unchecked(&mut circuit, x_var, m, Some(p_split.two_power_m))?;
1561
1562            let y_split_vars = circuit.mod_negate(&x_split_vars, &p)?;
1563
1564            assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
1565
1566            // bad witnesses
1567            *circuit.witness_mut(y_split_vars.vars.1) += F::one();
1568            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1569            *circuit.witness_mut(y_split_vars.vars.1) -= F::one();
1570            *circuit.witness_mut(y_split_vars.vars.1) += p_split.two_power_m;
1571
1572            // range check should fail
1573            assert!(circuit.check_circuit_satisfiability(&[]).is_err());
1574            *circuit.witness_mut(y_split_vars.vars.1) -= p_split.two_power_m;
1575
1576            let y_var = y_split_vars.convert_to_var(&mut circuit)?;
1577            let y = circuit.witness(y_var)?;
1578            assert_eq!(T::zero(), x + field_switching::<_, T>(&y))
1579        }
1580
1581        Ok(())
1582    }
1583}