ark_r1cs_std/boolean/
cmp.rs

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

ark_r1cs_std/boolean/
cmp.rs
