jf_relation/gadgets/
range.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//! Implementation of circuit lookup related gadgets
8
9use super::utils::next_multiple;
10use crate::{constants::GATE_WIDTH, BoolVar, Circuit, CircuitError, PlonkCircuit, Variable};
11use ark_ff::{BigInteger, PrimeField};
12use ark_std::{format, string::ToString, vec::Vec};
13
14impl<F: PrimeField> PlonkCircuit<F> {
15    /// Constrain a variable to be within the [0, 2^`bit_len`) range
16    /// Return error if the variable is invalid.
17    pub fn enforce_in_range(&mut self, a: Variable, bit_len: usize) -> Result<(), CircuitError> {
18        if self.support_lookup() {
19            self.range_gate_with_lookup(a, bit_len)?;
20        } else {
21            self.range_gate_internal(a, bit_len)?;
22        }
23        Ok(())
24    }
25
26    /// Return a boolean variable indicating whether variable `a` is in the
27    /// range [0, 2^`bit_len`). Return error if the variable is invalid.
28    /// TODO: optimize the gate for UltraPlonk.
29    pub fn is_in_range(&mut self, a: Variable, bit_len: usize) -> Result<BoolVar, CircuitError> {
30        let a_bit_le: Vec<BoolVar> = self.unpack(a, F::MODULUS_BIT_SIZE as usize)?;
31        let a_bit_le: Vec<Variable> = a_bit_le.into_iter().map(|b| b.into()).collect();
32        // a is in range if and only if the bits in `a_bit_le[bit_len..]` are all
33        // zeroes.
34        let higher_bit_sum = self.sum(&a_bit_le[bit_len..])?;
35        self.is_zero(higher_bit_sum)
36    }
37
38    /// Obtain the `bit_len`-long binary representation of variable `a`
39    /// Return a list of variables [b0, ..., b_`bit_len`] which is the binary
40    /// representation of `a`.
41    /// Return error if the `a` is not the range of [0, 2^`bit_len`).
42    pub fn unpack(&mut self, a: Variable, bit_len: usize) -> Result<Vec<BoolVar>, CircuitError> {
43        if bit_len < F::MODULUS_BIT_SIZE as usize
44            && self.witness(a)? >= F::from(2u32).pow([bit_len as u64])
45        {
46            return Err(CircuitError::ParameterError(
47                "Failed to unpack variable to a range of smaller than 2^bit_len".to_string(),
48            ));
49        }
50        self.range_gate_internal(a, bit_len)
51    }
52
53    /// a general decomposition gate (not necessarily binary decomposition)
54    /// where `a` are enforced to decomposed to `a_chunks_le` which consists
55    /// of chunks (multiple bits) in little-endian order and
56    /// each chunk \in [0, `range_size`)
57    pub(crate) fn decomposition_gate(
58        &mut self,
59        a_chunks_le: Vec<Variable>,
60        a: Variable,
61        range_size: F,
62    ) -> Result<(), CircuitError> {
63        // ensure (padded_len - 1) % 3 = 0
64        let mut padded = a_chunks_le;
65        let len = padded.len();
66        let rate = GATE_WIDTH - 1; // rate at which lc add each round
67        let padded_len = next_multiple(len - 1, rate)? + 1;
68        padded.resize(padded_len, self.zero());
69
70        let range_size_square = range_size.square();
71        let range_size_cube = range_size * range_size_square;
72        let coeffs = [range_size_cube, range_size_square, range_size, F::one()];
73        let mut accum = padded[padded_len - 1];
74        for i in 1..padded_len / rate {
75            accum = self.lc(
76                &[
77                    accum,
78                    padded[padded_len - 1 - rate * i + 2],
79                    padded[padded_len - 1 - rate * i + 1],
80                    padded[padded_len - 1 - rate * i],
81                ],
82                &coeffs,
83            )?;
84        }
85        // final round
86        let wires = [accum, padded[2], padded[1], padded[0], a];
87        self.lc_gate(&wires, &coeffs)?;
88
89        Ok(())
90    }
91}
92
93/// Private helper function for range gate
94impl<F: PrimeField> PlonkCircuit<F> {
95    // internal of a range check gate
96    pub(crate) fn range_gate_internal(
97        &mut self,
98        a: Variable,
99        bit_len: usize,
100    ) -> Result<Vec<BoolVar>, CircuitError> {
101        self.check_var_bound(a)?;
102        if bit_len == 0 {
103            return Err(CircuitError::ParameterError(
104                "Only allows positive bit length for range upper bound".to_string(),
105            ));
106        }
107
108        let a_bits_le: Vec<bool> = self.witness(a)?.into_bigint().to_bits_le();
109
110        if bit_len > a_bits_le.len() {
111            return Err(CircuitError::ParameterError(format!(
112                "Maximum field bit size: {}, requested range upper bound bit len: {}",
113                a_bits_le.len(),
114                bit_len
115            )));
116        }
117        // convert to variable in the circuit from the vector of boolean as binary
118        // representation
119        let a_bits_le: Vec<BoolVar> = a_bits_le
120            .iter()
121            .take(bit_len) // since little-endian, truncate would remove MSBs
122            .map(|&b| {
123                self.create_boolean_variable(b)
124            })
125            .collect::<Result<Vec<_>, CircuitError>>()?;
126
127        // edge case: when decomposing a field to exactly MODULUS_BIT_SIZE,
128        // and when MODULUS < 2^MODULUS_BIT_SIZE (e.g. p=17, log2(p) = 5), then we need
129        // to rule out non-canonical representation of field elements (e.g.
130        // avoid bit-wise 18 to represent 1 mod 17) by making sure its always < MODULUS
131        if bit_len == F::MODULUS_BIT_SIZE as usize {
132            self.binary_decomposition_gate_with_canonical_check(a_bits_le.clone(), a)?;
133        } else {
134            self.binary_decomposition_gate(a_bits_le.clone(), a)?;
135        }
136
137        Ok(a_bits_le)
138    }
139
140    fn binary_decomposition_gate_with_canonical_check(
141        &mut self,
142        a_bits_le: Vec<BoolVar>,
143        a: Variable,
144    ) -> Result<(), CircuitError> {
145        self.binary_decomposition_gate(a_bits_le.clone(), a)?;
146
147        // making sure a < modulus in binary format,
148        // namely it's in canonical representation
149        let modulus_bits_le = F::MODULUS.to_bits_le();
150        let is_lt_modulus = a_bits_le
151            .iter()
152            .chain(ark_std::iter::repeat(&self.false_var()))
153            .zip(modulus_bits_le.iter())
154            .try_fold(self.false_var(), |cur, (a_bit, p_bit)| {
155                let not_a = self.logic_neg(*a_bit)?;
156                if *p_bit {
157                    self.logic_or(cur, not_a)
158                } else {
159                    self.logic_and(cur, not_a)
160                }
161            })?;
162        self.enforce_constant(is_lt_modulus.0, F::one())?;
163        Ok(())
164    }
165
166    fn binary_decomposition_gate(
167        &mut self,
168        a_bits_le: Vec<BoolVar>,
169        a: Variable,
170    ) -> Result<(), CircuitError> {
171        let a_chunks_le: Vec<Variable> = a_bits_le.into_iter().map(|b| b.into()).collect();
172        self.decomposition_gate(a_chunks_le, a, 2u8.into())?;
173        Ok(())
174    }
175}
176
177#[cfg(test)]
178mod test {
179    use crate::{
180        gadgets::test_utils::test_variable_independence_for_circuit, BoolVar, Circuit,
181        CircuitError, PlonkCircuit, Variable,
182    };
183    use ark_bls12_377::Fq as Fq377;
184    use ark_ed_on_bls12_377::Fq as FqEd377;
185    use ark_ed_on_bls12_381::Fq as FqEd381;
186    use ark_ed_on_bn254::Fq as FqEd254;
187    use ark_ff::{
188        fields::{Fp64, MontBackend, MontConfig},
189        BigInt, BigInteger, PrimeField,
190    };
191    use ark_std::vec::Vec;
192    use core::mem::MaybeUninit;
193
194    #[test]
195    fn test_unpack() -> Result<(), CircuitError> {
196        test_unpack_helper::<FqEd254>()?;
197        test_unpack_helper::<FqEd377>()?;
198        test_unpack_helper::<FqEd381>()?;
199        test_unpack_helper::<Fq377>()
200    }
201
202    fn test_unpack_helper<F: PrimeField>() -> Result<(), CircuitError> {
203        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_turbo_plonk();
204        let a = circuit.create_variable(F::one())?;
205        let b = circuit.create_variable(F::from(1023u32))?;
206
207        circuit.enforce_in_range(a, 1)?;
208        let a_le = circuit.unpack(a, 3)?;
209        assert_eq!(a_le.len(), 3);
210        let b_le = circuit.unpack(b, 10)?;
211        assert_eq!(b_le.len(), 10);
212        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
213        assert!(circuit.unpack(b, 9).is_err());
214        Ok(())
215    }
216
217    #[test]
218    fn test_range_gate() -> Result<(), CircuitError> {
219        test_range_gate_helper::<FqEd254>()?;
220        test_range_gate_helper::<FqEd377>()?;
221        test_range_gate_helper::<FqEd381>()?;
222        test_range_gate_helper::<Fq377>()
223    }
224    fn test_range_gate_helper<F: PrimeField>() -> Result<(), CircuitError> {
225        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_turbo_plonk();
226        let a = circuit.create_variable(F::one())?;
227        let b = circuit.create_variable(F::from(1023u32))?;
228
229        circuit.enforce_in_range(a, 1)?;
230        circuit.enforce_in_range(a, 3)?;
231        circuit.enforce_in_range(b, 10)?;
232        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
233        circuit.enforce_in_range(b, 9)?;
234        assert!(circuit.enforce_in_range(a, 0).is_err());
235        // non-positive bit length is undefined, thus fail
236        assert!(circuit.enforce_in_range(a, 0).is_err());
237        // bit length bigger than that of a field element (bit length takes 256 or 381
238        // bits)
239        let bit_len = (F::MODULUS_BIT_SIZE as usize / 8 + 1) * 8;
240        assert!(circuit.enforce_in_range(a, bit_len + 1).is_err());
241        // if mess up the wire value, should fail
242        *circuit.witness_mut(b) = F::from(1024u32);
243        assert!(circuit.check_circuit_satisfiability(&[]).is_err());
244        // Check variable out of bound error.
245        assert!(circuit.enforce_in_range(circuit.num_vars(), 10).is_err());
246
247        // build two fixed circuits with different variable assignments, checking that
248        // the arithmetized extended permutation polynomial is variable
249        // independent
250        let circuit_1 = build_range_gate_circuit(F::from(314u32))?;
251        let circuit_2 = build_range_gate_circuit(F::from(489u32))?;
252        test_variable_independence_for_circuit(circuit_1, circuit_2)?;
253
254        Ok(())
255    }
256
257    fn build_range_gate_circuit<F: PrimeField>(a: F) -> Result<PlonkCircuit<F>, CircuitError> {
258        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_turbo_plonk();
259        let a_var = circuit.create_variable(a)?;
260        circuit.enforce_in_range(a_var, 10)?;
261        circuit.finalize_for_arithmetization()?;
262        Ok(circuit)
263    }
264
265    #[test]
266    fn test_check_in_range() -> Result<(), CircuitError> {
267        test_check_in_range_helper::<FqEd254>()?;
268        test_check_in_range_helper::<FqEd377>()?;
269        test_check_in_range_helper::<FqEd381>()?;
270        test_check_in_range_helper::<Fq377>()
271    }
272    fn test_check_in_range_helper<F: PrimeField>() -> Result<(), CircuitError> {
273        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_turbo_plonk();
274        let a = circuit.create_variable(F::from(1023u32))?;
275
276        let b1 = circuit.is_in_range(a, 5)?;
277        let b2 = circuit.is_in_range(a, 10)?;
278        let b3 = circuit.is_in_range(a, 0)?;
279        assert_eq!(circuit.witness(b1.into())?, F::zero());
280        assert_eq!(circuit.witness(b2.into())?, F::one());
281        assert_eq!(circuit.witness(b3.into())?, F::zero());
282        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
283
284        // if mess up the wire value, should fail
285        *circuit.witness_mut(a) = F::from(1024u32);
286        assert!(circuit.check_circuit_satisfiability(&[]).is_err());
287        // Check variable out of bound error.
288        assert!(circuit.is_in_range(circuit.num_vars(), 10).is_err());
289
290        // build two fixed circuits with different variable assignments, checking that
291        // the arithmetized extended permutation polynomial is variable
292        // independent
293        let circuit_1 = build_check_in_range_circuit(F::from(314u32))?;
294        let circuit_2 = build_check_in_range_circuit(F::from(1489u32))?;
295        test_variable_independence_for_circuit(circuit_1, circuit_2)?;
296
297        Ok(())
298    }
299
300    fn build_check_in_range_circuit<F: PrimeField>(a: F) -> Result<PlonkCircuit<F>, CircuitError> {
301        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_turbo_plonk();
302        let a_var = circuit.create_variable(a)?;
303        circuit.is_in_range(a_var, 10)?;
304        circuit.finalize_for_arithmetization()?;
305        Ok(circuit)
306    }
307
308    // A F17 finite field for test
309    #[derive(MontConfig)]
310    #[modulus = "17"]
311    #[generator = "3"]
312    pub struct F17Config;
313    pub type F17 = Fp64<MontBackend<F17Config, 1>>;
314
315    impl PlonkCircuit<F17> {
316        /// exactly the same gates as the old vulnerable `unpack()` except
317        /// when we create wire variables for the bit representation of `a`, we
318        /// directly take the raw representation of `a`, instead of
319        /// `.into_bigint(). to_bits_le()` which will canonicalize the
320        /// repr. So that if `a` is manipulated to be in non-canonical
321        /// form, the `a_bits_le` will also be in non-canonical form.
322        fn old_unpack(
323            &mut self,
324            a: Variable,
325            bit_len: usize,
326        ) -> Result<Vec<BoolVar>, CircuitError> {
327            self.check_var_bound(a)?;
328            // DIFF: this is only diff, directly accessing `.0` of Fp which avoid the
329            // canonicalization during `.into_bigint()`
330            let a_bits_le: Vec<bool> = self.witness(a)?.0.to_bits_le();
331            let a_bits_le: Vec<BoolVar> = a_bits_le
332                .iter()
333                .take(bit_len)
334                .map(|&b| self.create_boolean_variable(b))
335                .collect::<Result<Vec<_>, CircuitError>>()?;
336
337            self.binary_decomposition_gate(a_bits_le.clone(), a)?;
338            Ok(a_bits_le)
339        }
340
341        // fixing the vulnerable unpack by using a the gate `_with_canonical_check`
342        fn fixed_unpack(
343            &mut self,
344            a: Variable,
345            bit_len: usize,
346        ) -> Result<Vec<BoolVar>, CircuitError> {
347            self.check_var_bound(a)?;
348            let a_bits_le: Vec<bool> = self.witness(a)?.0.to_bits_le();
349            let a_bits_le: Vec<BoolVar> = a_bits_le
350                .iter()
351                .take(bit_len)
352                .map(|&b| self.create_boolean_variable(b))
353                .collect::<Result<Vec<_>, CircuitError>>()?;
354
355            self.binary_decomposition_gate_with_canonical_check(a_bits_le.clone(), a)?;
356            Ok(a_bits_le)
357        }
358    }
359
360    /// Credit: LeastAuthority responsibly reported a critical bug in v0.4.4 of
361    /// jf-relation (as of Aug 30, 2025).
362    #[test]
363    fn non_canonical_field() -> Result<(), CircuitError> {
364        // showcasing the vulnerability
365        let mut circuit = PlonkCircuit::<F17>::new_turbo_plonk();
366
367        // a mod p = 1, but non-canonical representation with actual integer value of 18
368        let a: F17 = unsafe {
369            let mut x = MaybeUninit::<F17>::uninit();
370            // directly write the BigInt [18] into the inner field storage
371            ark_std::ptr::write(&mut (*x.as_mut_ptr()).0, BigInt::new([18]));
372            x.assume_init()
373        };
374        let a_var = circuit.create_variable(a)?;
375        assert_eq!(circuit.witness(a_var)?.0, BigInt::new([18]));
376
377        let a_bits_le = circuit.old_unpack(a_var, F17::MODULUS_BIT_SIZE as usize)?;
378        let recomposed = a_bits_le.iter().enumerate().fold(0u64, |acc, (i, b_var)| {
379            acc | (circuit.witness(b_var.0).unwrap().0 .0[0] << i)
380        });
381
382        // non_canonical field repr would pass vulnerable `unpack()` gadget
383        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
384        assert!(recomposed > 17);
385
386        // verifying the fix
387        let mut circuit = PlonkCircuit::<F17>::new_turbo_plonk();
388        let a: F17 = unsafe {
389            let mut x = MaybeUninit::<F17>::uninit();
390            ark_std::ptr::write(&mut (*x.as_mut_ptr()).0, BigInt::new([18]));
391            x.assume_init()
392        };
393        let a_var = circuit.create_variable(a)?;
394        let _ = circuit.fixed_unpack(a_var, F17::MODULUS_BIT_SIZE as usize)?;
395        assert!(
396            circuit.check_circuit_satisfiability(&[]).is_err(),
397            "non_canonical field repr still fool fixed `unpack()` gadget"
398        );
399
400        Ok(())
401    }
402}