ark-r1cs-std/src/boolean/and.rs
src/boolean/and.rsRaw
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}