ark_r1cs_std/boolean/
cmp.rs

1use crate::cmp::CmpGadget;
2
3use super::*;
4use ark_ff::PrimeField;
5
6impl<F: PrimeField> CmpGadget<F> for Boolean<F> {
7    fn is_ge(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
8        // a | b | (a | !b) | a >= b
9        // --|---|--------|--------
10        // 0 | 0 |    1     |   1
11        // 1 | 0 |    1     |   1
12        // 0 | 1 |    0     |   0
13        // 1 | 1 |    1     |   1
14        Ok(self | &(!other))
15    }
16}
17
18impl<F: PrimeField> Boolean<F> {
19    /// Enforces that `bits`, when interpreted as a integer, is less than
20    /// `F::characteristic()`, That is, interpret bits as a little-endian
21    /// integer, and enforce that this integer is "in the field Z_p", where
22    /// `p = F::characteristic()` .
23    #[tracing::instrument(target = "r1cs")]
24    pub fn enforce_in_field_le(bits: &[Self]) -> Result<(), SynthesisError> {
25        // `bits` < F::characteristic() <==> `bits` <= F::characteristic() -1
26        let mut b = F::characteristic().to_vec();
27        assert_eq!(b[0] % 2, 1);
28        b[0] -= 1; // This works, because the LSB is one, so there's no borrows.
29        let run = Self::enforce_smaller_or_equal_than_le(bits, b)?;
30
31        // We should always end in a "run" of zeros, because
32        // the characteristic is an odd prime. So, this should
33        // be empty.
34        assert!(run.is_empty());
35
36        Ok(())
37    }
38
39    /// Enforces that `bits` is less than or equal to `element`,
40    /// when both are interpreted as (little-endian) integers.
41    #[tracing::instrument(target = "r1cs", skip(element))]
42    pub fn enforce_smaller_or_equal_than_le(
43        bits: &[Self],
44        element: impl AsRef<[u64]>,
45    ) -> Result<Vec<Self>, SynthesisError> {
46        let b: &[u64] = element.as_ref();
47
48        let mut bits_iter = bits.iter().rev(); // Iterate in big-endian
49
50        // Runs of ones in r
51        let mut last_run = Boolean::TRUE;
52        let mut current_run = vec![];
53
54        let mut element_num_bits = 0;
55        for _ in BitIteratorBE::without_leading_zeros(b) {
56            element_num_bits += 1;
57        }
58
59        if bits.len() > element_num_bits {
60            let mut or_result = Boolean::FALSE;
61            for should_be_zero in &bits[element_num_bits..] {
62                or_result |= should_be_zero;
63                let _ = bits_iter.next().unwrap();
64            }
65            or_result.enforce_equal(&Boolean::FALSE)?;
66        }
67
68        for (b, a) in BitIteratorBE::without_leading_zeros(b).zip(bits_iter.by_ref()) {
69            if b {
70                // This is part of a run of ones.
71                current_run.push(a.clone());
72            } else {
73                if !current_run.is_empty() {
74                    // This is the start of a run of zeros, but we need
75                    // to k-ary AND against `last_run` first.
76
77                    current_run.push(last_run.clone());
78                    last_run = Self::kary_and(&current_run)?;
79                    current_run.truncate(0);
80                }
81
82                // If `last_run` is true, `a` must be false, or it would
83                // not be in the field.
84                //
85                // If `last_run` is false, `a` can be true or false.
86                //
87                // Ergo, at least one of `last_run` and `a` must be false.
88                Self::enforce_kary_nand(&[last_run.clone(), a.clone()])?;
89            }
90        }
91        assert!(bits_iter.next().is_none());
92
93        Ok(current_run)
94    }
95}
ark_r1cs_std/boolean/cmp.rs

ark_r1cs_std/boolean/
cmp.rs
