ark_r1cs_std/boolean/
and.rs

1use ark_ff::{Field, PrimeField};
2use ark_relations::r1cs::SynthesisError;
3use ark_std::{ops::BitAnd, ops::BitAndAssign};
4
5use crate::{fields::fp::FpVar, prelude::EqGadget};
6
7use super::Boolean;
8
9impl<F: Field> Boolean<F> {
10    fn _and(&self, other: &Self) -> Result<Self, SynthesisError> {
11        use Boolean::*;
12        match (self, other) {
13            // false AND x is always false
14            (&Constant(false), _) | (_, &Constant(false)) => Ok(Constant(false)),
15            // true AND x is always x
16            (&Constant(true), x) | (x, &Constant(true)) => Ok(x.clone()),
17            (Var(ref x), Var(ref y)) => Ok(Var(x.and(y)?)),
18        }
19    }
20
21    /// Outputs `!(self & other)`.
22    pub fn nand(&self, other: &Self) -> Result<Self, SynthesisError> {
23        self._and(other).map(|x| !x)
24    }
25}
26
27impl<F: PrimeField> Boolean<F> {
28    /// Outputs `bits[0] & bits[1] & ... & bits.last().unwrap()`.
29    ///
30    /// ```
31    /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
32    /// // We'll use the BLS12-381 scalar field for our constraints.
33    /// use ark_test_curves::bls12_381::Fr;
34    /// use ark_relations::r1cs::*;
35    /// use ark_r1cs_std::prelude::*;
36    ///
37    /// let cs = ConstraintSystem::<Fr>::new_ref();
38    ///
39    /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
40    /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
41    /// let c = Boolean::new_witness(cs.clone(), || Ok(true))?;
42    ///
43    /// Boolean::kary_and(&[a.clone(), b.clone(), c.clone()])?.enforce_equal(&Boolean::FALSE)?;
44    /// Boolean::kary_and(&[a.clone(), c.clone()])?.enforce_equal(&Boolean::TRUE)?;
45    ///
46    /// assert!(cs.is_satisfied().unwrap());
47    /// # Ok(())
48    /// # }
49    /// ```
50    #[tracing::instrument(target = "r1cs")]
51    pub fn kary_and(bits: &[Self]) -> Result<Self, SynthesisError> {
52        assert!(!bits.is_empty());
53        if bits.len() <= 3 {
54            let mut cur: Option<Self> = None;
55            for next in bits {
56                cur = if let Some(b) = cur {
57                    Some(b & next)
58                } else {
59                    Some(next.clone())
60                };
61            }
62
63            Ok(cur.expect("should not be 0"))
64        } else {
65            // b0 & b1 & ... & bN == 1 if and only if sum(b0, b1, ..., bN) == N
66            let sum_bits: FpVar<_> = bits.iter().map(|b| FpVar::from(b.clone())).sum();
67            let num_bits = FpVar::Constant(F::from(bits.len() as u64));
68            sum_bits.is_eq(&num_bits)
69        }
70    }
71
72    /// Outputs `!(bits[0] & bits[1] & ... & bits.last().unwrap())`.
73    ///
74    /// ```
75    /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
76    /// // We'll use the BLS12-381 scalar field for our constraints.
77    /// use ark_test_curves::bls12_381::Fr;
78    /// use ark_relations::r1cs::*;
79    /// use ark_r1cs_std::prelude::*;
80    ///
81    /// let cs = ConstraintSystem::<Fr>::new_ref();
82    ///
83    /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
84    /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
85    /// let c = Boolean::new_witness(cs.clone(), || Ok(true))?;
86    ///
87    /// Boolean::kary_nand(&[a.clone(), b.clone(), c.clone()])?.enforce_equal(&Boolean::TRUE)?;
88    /// Boolean::kary_nand(&[a.clone(), c.clone()])?.enforce_equal(&Boolean::FALSE)?;
89    /// Boolean::kary_nand(&[b.clone(), c.clone()])?.enforce_equal(&Boolean::TRUE)?;
90    ///
91    /// assert!(cs.is_satisfied().unwrap());
92    /// # Ok(())
93    /// # }
94    /// ```
95    #[tracing::instrument(target = "r1cs")]
96    pub fn kary_nand(bits: &[Self]) -> Result<Self, SynthesisError> {
97        Ok(!Self::kary_and(bits)?)
98    }
99
100    /// Enforces that `!(bits[0] & bits[1] & ... ) == Boolean::TRUE`.
101    ///
102    /// Informally, this means that at least one element in `bits` must be
103    /// `false`.
104    #[tracing::instrument(target = "r1cs")]
105    pub fn enforce_kary_nand(bits: &[Self]) -> Result<(), SynthesisError> {
106        Self::kary_and(bits)?.enforce_equal(&Boolean::FALSE)
107    }
108}
109
110impl<'a, F: Field> BitAnd<Self> for &'a Boolean<F> {
111    type Output = Boolean<F>;
112    /// Outputs `self & other`.
113    ///
114    /// If at least one of `self` and `other` are constants, then this method
115    /// *does not* create any constraints or variables.
116    ///
117    /// ```
118    /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
119    /// // We'll use the BLS12-381 scalar field for our constraints.
120    /// use ark_test_curves::bls12_381::Fr;
121    /// use ark_relations::r1cs::*;
122    /// use ark_r1cs_std::prelude::*;
123    ///
124    /// let cs = ConstraintSystem::<Fr>::new_ref();
125    ///
126    /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
127    /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
128    ///
129    /// (&a & &a).enforce_equal(&Boolean::TRUE)?;
130    ///
131    /// (&a & &b).enforce_equal(&Boolean::FALSE)?;
132    /// (&b & &a).enforce_equal(&Boolean::FALSE)?;
133    /// (&b & &b).enforce_equal(&Boolean::FALSE)?;
134    ///
135    /// assert!(cs.is_satisfied().unwrap());
136    /// # Ok(())
137    /// # }
138    /// ```
139    #[tracing::instrument(target = "r1cs", skip(self, other))]
140    fn bitand(self, other: Self) -> Self::Output {
141        self._and(other).unwrap()
142    }
143}
144
145impl<'a, F: Field> BitAnd<&'a Self> for Boolean<F> {
146    type Output = Boolean<F>;
147
148    #[tracing::instrument(target = "r1cs", skip(self, other))]
149    fn bitand(self, other: &Self) -> Self::Output {
150        self._and(&other).unwrap()
151    }
152}
153
154impl<'a, F: Field> BitAnd<Boolean<F>> for &'a Boolean<F> {
155    type Output = Boolean<F>;
156
157    #[tracing::instrument(target = "r1cs", skip(self, other))]
158    fn bitand(self, other: Boolean<F>) -> Self::Output {
159        self._and(&other).unwrap()
160    }
161}
162
163impl<F: Field> BitAnd<Self> for Boolean<F> {
164    type Output = Self;
165
166    #[tracing::instrument(target = "r1cs", skip(self, other))]
167    fn bitand(self, other: Self) -> Self::Output {
168        self._and(&other).unwrap()
169    }
170}
171
172impl<F: Field> BitAndAssign<Self> for Boolean<F> {
173    /// Sets `self = self & other`.
174    #[tracing::instrument(target = "r1cs", skip(self, other))]
175    fn bitand_assign(&mut self, other: Self) {
176        let result = self._and(&other).unwrap();
177        *self = result;
178    }
179}
180
181impl<'a, F: Field> BitAndAssign<&'a Self> for Boolean<F> {
182    /// Sets `self = self & other`.
183    #[tracing::instrument(target = "r1cs", skip(self, other))]
184    fn bitand_assign(&mut self, other: &'a Self) {
185        let result = self._and(other).unwrap();
186        *self = result;
187    }
188}
189
190#[cfg(test)]
191mod tests {
192    use super::*;
193    use crate::{
194        alloc::{AllocVar, AllocationMode},
195        boolean::test_utils::run_binary_exhaustive,
196        prelude::EqGadget,
197        R1CSVar,
198    };
199    use ark_relations::r1cs::ConstraintSystem;
200    use ark_test_curves::bls12_381::Fr;
201
202    #[test]
203    fn and() {
204        run_binary_exhaustive::<Fr>(|a, b| {
205            let cs = a.cs().or(b.cs());
206            let both_constant = a.is_constant() && b.is_constant();
207            let computed = &a & &b;
208            let expected_mode = if both_constant {
209                AllocationMode::Constant
210            } else {
211                AllocationMode::Witness
212            };
213            let expected =
214                Boolean::new_variable(cs.clone(), || Ok(a.value()? & b.value()?), expected_mode)?;
215            assert_eq!(expected.value(), computed.value());
216            expected.enforce_equal(&computed)?;
217            if !both_constant {
218                assert!(cs.is_satisfied().unwrap());
219            }
220            Ok(())
221        })
222        .unwrap()
223    }
224
225    #[test]
226    fn nand() {
227        run_binary_exhaustive::<Fr>(|a, b| {
228            let cs = a.cs().or(b.cs());
229            let both_constant = a.is_constant() && b.is_constant();
230            let computed = a.nand(&b)?;
231            let expected_mode = if both_constant {
232                AllocationMode::Constant
233            } else {
234                AllocationMode::Witness
235            };
236            let expected = Boolean::new_variable(
237                cs.clone(),
238                || Ok(!(a.value()? & b.value()?)),
239                expected_mode,
240            )?;
241            assert_eq!(expected.value(), computed.value());
242            expected.enforce_equal(&computed)?;
243            if !both_constant {
244                assert!(cs.is_satisfied().unwrap());
245            }
246            Ok(())
247        })
248        .unwrap()
249    }
250
251    #[test]
252    fn enforce_nand() -> Result<(), SynthesisError> {
253        {
254            let cs = ConstraintSystem::<Fr>::new_ref();
255
256            assert!(
257                Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), false)?]).is_ok()
258            );
259            assert!(
260                Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), true)?]).is_err()
261            );
262        }
263
264        for i in 1..5 {
265            // with every possible assignment for them
266            for mut b in 0..(1 << i) {
267                // with every possible negation
268                for mut n in 0..(1 << i) {
269                    let cs = ConstraintSystem::<Fr>::new_ref();
270
271                    let mut expected = true;
272
273                    let mut bits = vec![];
274                    for _ in 0..i {
275                        expected &= b & 1 == 1;
276
277                        let bit = if n & 1 == 1 {
278                            Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?
279                        } else {
280                            !Boolean::new_witness(cs.clone(), || Ok(b & 1 == 0))?
281                        };
282                        bits.push(bit);
283
284                        b >>= 1;
285                        n >>= 1;
286                    }
287
288                    let expected = !expected;
289
290                    Boolean::enforce_kary_nand(&bits)?;
291
292                    if expected {
293                        assert!(cs.is_satisfied().unwrap());
294                    } else {
295                        assert!(!cs.is_satisfied().unwrap());
296                    }
297                }
298            }
299        }
300        Ok(())
301    }
302
303    #[test]
304    fn kary_and() -> Result<(), SynthesisError> {
305        // test different numbers of operands
306        for i in 1..15 {
307            // with every possible assignment for them
308            for mut b in 0..(1 << i) {
309                let cs = ConstraintSystem::<Fr>::new_ref();
310
311                let mut expected = true;
312
313                let mut bits = vec![];
314                for _ in 0..i {
315                    expected &= b & 1 == 1;
316                    bits.push(Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?);
317                    b >>= 1;
318                }
319
320                let r = Boolean::kary_and(&bits)?;
321
322                assert!(cs.is_satisfied().unwrap());
323
324                if let Boolean::Var(ref r) = r {
325                    assert_eq!(r.value()?, expected);
326                }
327            }
328        }
329        Ok(())
330    }
331}
ark_r1cs_std/boolean/and.rs

ark_r1cs_std/boolean/
and.rs
