ark-r1cs-std/src/bits/boolean.rs
src/bits/boolean.rsRaw
1use ark_ff::{BitIteratorBE, Field, PrimeField};
2
3use crate::{fields::fp::FpVar, prelude::*, Assignment, ToConstraintFieldGadget, Vec};
4use ark_relations::r1cs::{
5 ConstraintSystemRef, LinearCombination, Namespace, SynthesisError, Variable,
6};
7use core::borrow::Borrow;
8
9/// Represents a variable in the constraint system which is guaranteed
10/// to be either zero or one.
11///
12/// In general, one should prefer using `Boolean` instead of `AllocatedBit`,
13/// as `Boolean` offers better support for constant values, and implements
14/// more traits.
15#[derive(Clone, Debug, Eq, PartialEq)]
16#[must_use]
17pub struct AllocatedBit<F: Field> {
18 variable: Variable,
19 cs: ConstraintSystemRef<F>,
20}
21
22pub(crate) fn bool_to_field<F: Field>(val: impl Borrow<bool>) -> F {
23 if *val.borrow() {
24 F::one()
25 } else {
26 F::zero()
27 }
28}
29
30impl<F: Field> AllocatedBit<F> {
31 /// Get the assigned value for `self`.
32 pub fn value(&self) -> Result<bool, SynthesisError> {
33 let value = self.cs.assigned_value(self.variable).get()?;
34 if value.is_zero() {
35 Ok(false)
36 } else if value.is_one() {
37 Ok(true)
38 } else {
39 unreachable!("Incorrect value assigned: {:?}", value);
40 }
41 }
42
43 /// Get the R1CS variable for `self`.
44 pub fn variable(&self) -> Variable {
45 self.variable
46 }
47
48 /// Allocate a witness variable without a booleanity check.
49 fn new_witness_without_booleanity_check<T: Borrow<bool>>(
50 cs: ConstraintSystemRef<F>,
51 f: impl FnOnce() -> Result<T, SynthesisError>,
52 ) -> Result<Self, SynthesisError> {
53 let variable = cs.new_witness_variable(|| f().map(bool_to_field))?;
54 Ok(Self { variable, cs })
55 }
56
57 /// Performs an XOR operation over the two operands, returning
58 /// an `AllocatedBit`.
59 #[tracing::instrument(target = "r1cs")]
60 pub fn xor(&self, b: &Self) -> Result<Self, SynthesisError> {
61 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
62 Ok(self.value()? ^ b.value()?)
63 })?;
64
65 // Constrain (a + a) * (b) = (a + b - c)
66 // Given that a and b are boolean constrained, if they
67 // are equal, the only solution for c is 0, and if they
68 // are different, the only solution for c is 1.
69 //
70 // ¬(a ∧ b) ∧ ¬(¬a ∧ ¬b) = c
71 // (1 - (a * b)) * (1 - ((1 - a) * (1 - b))) = c
72 // (1 - ab) * (1 - (1 - a - b + ab)) = c
73 // (1 - ab) * (a + b - ab) = c
74 // a + b - ab - (a^2)b - (b^2)a + (a^2)(b^2) = c
75 // a + b - ab - ab - ab + ab = c
76 // a + b - 2ab = c
77 // -2a * b = c - a - b
78 // 2a * b = a + b - c
79 // (a + a) * b = a + b - c
80 self.cs.enforce_constraint(
81 lc!() + self.variable + self.variable,
82 lc!() + b.variable,
83 lc!() + self.variable + b.variable - result.variable,
84 )?;
85
86 Ok(result)
87 }
88
89 /// Performs an AND operation over the two operands, returning
90 /// an `AllocatedBit`.
91 #[tracing::instrument(target = "r1cs")]
92 pub fn and(&self, b: &Self) -> Result<Self, SynthesisError> {
93 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
94 Ok(self.value()? & b.value()?)
95 })?;
96
97 // Constrain (a) * (b) = (c), ensuring c is 1 iff
98 // a AND b are both 1.
99 self.cs.enforce_constraint(
100 lc!() + self.variable,
101 lc!() + b.variable,
102 lc!() + result.variable,
103 )?;
104
105 Ok(result)
106 }
107
108 /// Performs an OR operation over the two operands, returning
109 /// an `AllocatedBit`.
110 #[tracing::instrument(target = "r1cs")]
111 pub fn or(&self, b: &Self) -> Result<Self, SynthesisError> {
112 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
113 Ok(self.value()? | b.value()?)
114 })?;
115
116 // Constrain (1 - a) * (1 - b) = (c), ensuring c is 1 iff
117 // a and b are both false, and otherwise c is 0.
118 self.cs.enforce_constraint(
119 lc!() + Variable::One - self.variable,
120 lc!() + Variable::One - b.variable,
121 lc!() + Variable::One - result.variable,
122 )?;
123
124 Ok(result)
125 }
126
127 /// Calculates `a AND (NOT b)`.
128 #[tracing::instrument(target = "r1cs")]
129 pub fn and_not(&self, b: &Self) -> Result<Self, SynthesisError> {
130 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
131 Ok(self.value()? & !b.value()?)
132 })?;
133
134 // Constrain (a) * (1 - b) = (c), ensuring c is 1 iff
135 // a is true and b is false, and otherwise c is 0.
136 self.cs.enforce_constraint(
137 lc!() + self.variable,
138 lc!() + Variable::One - b.variable,
139 lc!() + result.variable,
140 )?;
141
142 Ok(result)
143 }
144
145 /// Calculates `(NOT a) AND (NOT b)`.
146 #[tracing::instrument(target = "r1cs")]
147 pub fn nor(&self, b: &Self) -> Result<Self, SynthesisError> {
148 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
149 Ok(!(self.value()? | b.value()?))
150 })?;
151
152 // Constrain (1 - a) * (1 - b) = (c), ensuring c is 1 iff
153 // a and b are both false, and otherwise c is 0.
154 self.cs.enforce_constraint(
155 lc!() + Variable::One - self.variable,
156 lc!() + Variable::One - b.variable,
157 lc!() + result.variable,
158 )?;
159
160 Ok(result)
161 }
162}
163
164impl<F: Field> AllocVar<bool, F> for AllocatedBit<F> {
165 /// Produces a new variable of the appropriate kind
166 /// (instance or witness), with a booleanity check.
167 ///
168 /// N.B.: we could omit the booleanity check when allocating `self`
169 /// as a new public input, but that places an additional burden on
170 /// protocol designers. Better safe than sorry!
171 fn new_variable<T: Borrow<bool>>(
172 cs: impl Into<Namespace<F>>,
173 f: impl FnOnce() -> Result<T, SynthesisError>,
174 mode: AllocationMode,
175 ) -> Result<Self, SynthesisError> {
176 let ns = cs.into();
177 let cs = ns.cs();
178 if mode == AllocationMode::Constant {
179 let variable = if *f()?.borrow() {
180 Variable::One
181 } else {
182 Variable::Zero
183 };
184 Ok(Self { variable, cs })
185 } else {
186 let variable = if mode == AllocationMode::Input {
187 cs.new_input_variable(|| f().map(bool_to_field))?
188 } else {
189 cs.new_witness_variable(|| f().map(bool_to_field))?
190 };
191
192 // Constrain: (1 - a) * a = 0
193 // This constrains a to be either 0 or 1.
194
195 cs.enforce_constraint(lc!() + Variable::One - variable, lc!() + variable, lc!())?;
196
197 Ok(Self { variable, cs })
198 }
199 }
200}
201
202impl<F: Field> CondSelectGadget<F> for AllocatedBit<F> {
203 #[tracing::instrument(target = "r1cs")]
204 fn conditionally_select(
205 cond: &Boolean<F>,
206 true_val: &Self,
207 false_val: &Self,
208 ) -> Result<Self, SynthesisError> {
209 let res = Boolean::conditionally_select(
210 cond,
211 &true_val.clone().into(),
212 &false_val.clone().into(),
213 )?;
214 match res {
215 Boolean::Is(a) => Ok(a),
216 _ => unreachable!("Impossible"),
217 }
218 }
219}
220
221/// Represents a boolean value in the constraint system which is guaranteed
222/// to be either zero or one.
223#[derive(Clone, Debug, Eq, PartialEq)]
224#[must_use]
225pub enum Boolean<F: Field> {
226 /// Existential view of the boolean variable.
227 Is(AllocatedBit<F>),
228 /// Negated view of the boolean variable.
229 Not(AllocatedBit<F>),
230 /// Constant (not an allocated variable).
231 Constant(bool),
232}
233
234impl<F: Field> R1CSVar<F> for Boolean<F> {
235 type Value = bool;
236
237 fn cs(&self) -> ConstraintSystemRef<F> {
238 match self {
239 Self::Is(a) | Self::Not(a) => a.cs.clone(),
240 _ => ConstraintSystemRef::None,
241 }
242 }
243
244 fn value(&self) -> Result<Self::Value, SynthesisError> {
245 match self {
246 Boolean::Constant(c) => Ok(*c),
247 Boolean::Is(ref v) => v.value(),
248 Boolean::Not(ref v) => v.value().map(|b| !b),
249 }
250 }
251}
252
253impl<F: Field> Boolean<F> {
254 /// The constant `true`.
255 pub const TRUE: Self = Boolean::Constant(true);
256
257 /// The constant `false`.
258 pub const FALSE: Self = Boolean::Constant(false);
259
260 /// Constructs a `LinearCombination` from `Self`'s variables according
261 /// to the following map.
262 ///
263 /// * `Boolean::Constant(true) => lc!() + Variable::One`
264 /// * `Boolean::Constant(false) => lc!()`
265 /// * `Boolean::Is(v) => lc!() + v.variable()`
266 /// * `Boolean::Not(v) => lc!() + Variable::One - v.variable()`
267 pub fn lc(&self) -> LinearCombination<F> {
268 match self {
269 Boolean::Constant(false) => lc!(),
270 Boolean::Constant(true) => lc!() + Variable::One,
271 Boolean::Is(v) => v.variable().into(),
272 Boolean::Not(v) => lc!() + Variable::One - v.variable(),
273 }
274 }
275
276 /// Constructs a `Boolean` vector from a slice of constant `u8`.
277 /// The `u8`s are decomposed in little-endian manner.
278 ///
279 /// This *does not* create any new variables or constraints.
280 ///
281 /// ```
282 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
283 /// // We'll use the BLS12-381 scalar field for our constraints.
284 /// use ark_test_curves::bls12_381::Fr;
285 /// use ark_relations::r1cs::*;
286 /// use ark_r1cs_std::prelude::*;
287 ///
288 /// let cs = ConstraintSystem::<Fr>::new_ref();
289 /// let t = Boolean::<Fr>::TRUE;
290 /// let f = Boolean::<Fr>::FALSE;
291 ///
292 /// let bits = vec![f, t];
293 /// let generated_bits = Boolean::constant_vec_from_bytes(&[2]);
294 /// bits[..2].enforce_equal(&generated_bits[..2])?;
295 /// assert!(cs.is_satisfied().unwrap());
296 /// # Ok(())
297 /// # }
298 /// ```
299 pub fn constant_vec_from_bytes(values: &[u8]) -> Vec<Self> {
300 let mut bits = vec![];
301 for byte in values {
302 for i in 0..8 {
303 bits.push(Self::Constant(((byte >> i) & 1u8) == 1u8));
304 }
305 }
306 bits
307 }
308
309 /// Constructs a constant `Boolean` with value `b`.
310 ///
311 /// This *does not* create any new variables or constraints.
312 /// ```
313 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
314 /// // We'll use the BLS12-381 scalar field for our constraints.
315 /// use ark_test_curves::bls12_381::Fr;
316 /// use ark_r1cs_std::prelude::*;
317 ///
318 /// let true_var = Boolean::<Fr>::TRUE;
319 /// let false_var = Boolean::<Fr>::FALSE;
320 ///
321 /// true_var.enforce_equal(&Boolean::constant(true))?;
322 /// false_var.enforce_equal(&Boolean::constant(false))?;
323 /// # Ok(())
324 /// # }
325 /// ```
326 pub fn constant(b: bool) -> Self {
327 Boolean::Constant(b)
328 }
329
330 /// Negates `self`.
331 ///
332 /// This *does not* create any new variables or constraints.
333 /// ```
334 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
335 /// // We'll use the BLS12-381 scalar field for our constraints.
336 /// use ark_test_curves::bls12_381::Fr;
337 /// use ark_relations::r1cs::*;
338 /// use ark_r1cs_std::prelude::*;
339 ///
340 /// let cs = ConstraintSystem::<Fr>::new_ref();
341 ///
342 /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
343 /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
344 ///
345 /// a.not().enforce_equal(&b)?;
346 /// b.not().enforce_equal(&a)?;
347 ///
348 /// a.not().enforce_equal(&Boolean::FALSE)?;
349 /// b.not().enforce_equal(&Boolean::TRUE)?;
350 ///
351 /// assert!(cs.is_satisfied().unwrap());
352 /// # Ok(())
353 /// # }
354 /// ```
355 pub fn not(&self) -> Self {
356 match *self {
357 Boolean::Constant(c) => Boolean::Constant(!c),
358 Boolean::Is(ref v) => Boolean::Not(v.clone()),
359 Boolean::Not(ref v) => Boolean::Is(v.clone()),
360 }
361 }
362
363 /// Outputs `self ^ other`.
364 ///
365 /// If at least one of `self` and `other` are constants, then this method
366 /// *does not* create any constraints or variables.
367 ///
368 /// ```
369 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
370 /// // We'll use the BLS12-381 scalar field for our constraints.
371 /// use ark_test_curves::bls12_381::Fr;
372 /// use ark_relations::r1cs::*;
373 /// use ark_r1cs_std::prelude::*;
374 ///
375 /// let cs = ConstraintSystem::<Fr>::new_ref();
376 ///
377 /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
378 /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
379 ///
380 /// a.xor(&b)?.enforce_equal(&Boolean::TRUE)?;
381 /// b.xor(&a)?.enforce_equal(&Boolean::TRUE)?;
382 ///
383 /// a.xor(&a)?.enforce_equal(&Boolean::FALSE)?;
384 /// b.xor(&b)?.enforce_equal(&Boolean::FALSE)?;
385 ///
386 /// assert!(cs.is_satisfied().unwrap());
387 /// # Ok(())
388 /// # }
389 /// ```
390 #[tracing::instrument(target = "r1cs")]
391 pub fn xor<'a>(&'a self, other: &'a Self) -> Result<Self, SynthesisError> {
392 use Boolean::*;
393 match (self, other) {
394 (&Constant(false), x) | (x, &Constant(false)) => Ok(x.clone()),
395 (&Constant(true), x) | (x, &Constant(true)) => Ok(x.not()),
396 // a XOR (NOT b) = NOT(a XOR b)
397 (is @ &Is(_), not @ &Not(_)) | (not @ &Not(_), is @ &Is(_)) => {
398 Ok(is.xor(¬.not())?.not())
399 }
400 // a XOR b = (NOT a) XOR (NOT b)
401 (&Is(ref a), &Is(ref b)) | (&Not(ref a), &Not(ref b)) => Ok(Is(a.xor(b)?)),
402 }
403 }
404
405 /// Outputs `self | other`.
406 ///
407 /// If at least one of `self` and `other` are constants, then this method
408 /// *does not* create any constraints or variables.
409 ///
410 /// ```
411 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
412 /// // We'll use the BLS12-381 scalar field for our constraints.
413 /// use ark_test_curves::bls12_381::Fr;
414 /// use ark_relations::r1cs::*;
415 /// use ark_r1cs_std::prelude::*;
416 ///
417 /// let cs = ConstraintSystem::<Fr>::new_ref();
418 ///
419 /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
420 /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
421 ///
422 /// a.or(&b)?.enforce_equal(&Boolean::TRUE)?;
423 /// b.or(&a)?.enforce_equal(&Boolean::TRUE)?;
424 ///
425 /// a.or(&a)?.enforce_equal(&Boolean::TRUE)?;
426 /// b.or(&b)?.enforce_equal(&Boolean::FALSE)?;
427 ///
428 /// assert!(cs.is_satisfied().unwrap());
429 /// # Ok(())
430 /// # }
431 /// ```
432 #[tracing::instrument(target = "r1cs")]
433 pub fn or<'a>(&'a self, other: &'a Self) -> Result<Self, SynthesisError> {
434 use Boolean::*;
435 match (self, other) {
436 (&Constant(false), x) | (x, &Constant(false)) => Ok(x.clone()),
437 (&Constant(true), _) | (_, &Constant(true)) => Ok(Constant(true)),
438 // a OR b = NOT ((NOT a) AND b)
439 (a @ &Is(_), b @ &Not(_)) | (b @ &Not(_), a @ &Is(_)) | (b @ &Not(_), a @ &Not(_)) => {
440 Ok(a.not().and(&b.not())?.not())
441 }
442 (&Is(ref a), &Is(ref b)) => a.or(b).map(From::from),
443 }
444 }
445
446 /// Outputs `self & other`.
447 ///
448 /// If at least one of `self` and `other` are constants, then this method
449 /// *does not* create any constraints or variables.
450 ///
451 /// ```
452 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
453 /// // We'll use the BLS12-381 scalar field for our constraints.
454 /// use ark_test_curves::bls12_381::Fr;
455 /// use ark_relations::r1cs::*;
456 /// use ark_r1cs_std::prelude::*;
457 ///
458 /// let cs = ConstraintSystem::<Fr>::new_ref();
459 ///
460 /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
461 /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
462 ///
463 /// a.and(&a)?.enforce_equal(&Boolean::TRUE)?;
464 ///
465 /// a.and(&b)?.enforce_equal(&Boolean::FALSE)?;
466 /// b.and(&a)?.enforce_equal(&Boolean::FALSE)?;
467 /// b.and(&b)?.enforce_equal(&Boolean::FALSE)?;
468 ///
469 /// assert!(cs.is_satisfied().unwrap());
470 /// # Ok(())
471 /// # }
472 /// ```
473 #[tracing::instrument(target = "r1cs")]
474 pub fn and<'a>(&'a self, other: &'a Self) -> Result<Self, SynthesisError> {
475 use Boolean::*;
476 match (self, other) {
477 // false AND x is always false
478 (&Constant(false), _) | (_, &Constant(false)) => Ok(Constant(false)),
479 // true AND x is always x
480 (&Constant(true), x) | (x, &Constant(true)) => Ok(x.clone()),
481 // a AND (NOT b)
482 (&Is(ref is), &Not(ref not)) | (&Not(ref not), &Is(ref is)) => Ok(Is(is.and_not(not)?)),
483 // (NOT a) AND (NOT b) = a NOR b
484 (&Not(ref a), &Not(ref b)) => Ok(Is(a.nor(b)?)),
485 // a AND b
486 (&Is(ref a), &Is(ref b)) => Ok(Is(a.and(b)?)),
487 }
488 }
489
490 /// Outputs `bits[0] & bits[1] & ... & bits.last().unwrap()`.
491 ///
492 /// ```
493 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
494 /// // We'll use the BLS12-381 scalar field for our constraints.
495 /// use ark_test_curves::bls12_381::Fr;
496 /// use ark_relations::r1cs::*;
497 /// use ark_r1cs_std::prelude::*;
498 ///
499 /// let cs = ConstraintSystem::<Fr>::new_ref();
500 ///
501 /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
502 /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
503 /// let c = Boolean::new_witness(cs.clone(), || Ok(true))?;
504 ///
505 /// Boolean::kary_and(&[a.clone(), b.clone(), c.clone()])?.enforce_equal(&Boolean::FALSE)?;
506 /// Boolean::kary_and(&[a.clone(), c.clone()])?.enforce_equal(&Boolean::TRUE)?;
507 ///
508 /// assert!(cs.is_satisfied().unwrap());
509 /// # Ok(())
510 /// # }
511 /// ```
512 #[tracing::instrument(target = "r1cs")]
513 pub fn kary_and(bits: &[Self]) -> Result<Self, SynthesisError> {
514 assert!(!bits.is_empty());
515 let mut cur: Option<Self> = None;
516 for next in bits {
517 cur = if let Some(b) = cur {
518 Some(b.and(next)?)
519 } else {
520 Some(next.clone())
521 };
522 }
523
524 Ok(cur.expect("should not be 0"))
525 }
526
527 /// Outputs `bits[0] | bits[1] | ... | bits.last().unwrap()`.
528 ///
529 /// ```
530 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
531 /// // We'll use the BLS12-381 scalar field for our constraints.
532 /// use ark_test_curves::bls12_381::Fr;
533 /// use ark_relations::r1cs::*;
534 /// use ark_r1cs_std::prelude::*;
535 ///
536 /// let cs = ConstraintSystem::<Fr>::new_ref();
537 ///
538 /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
539 /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
540 /// let c = Boolean::new_witness(cs.clone(), || Ok(false))?;
541 ///
542 /// Boolean::kary_or(&[a.clone(), b.clone(), c.clone()])?.enforce_equal(&Boolean::TRUE)?;
543 /// Boolean::kary_or(&[a.clone(), c.clone()])?.enforce_equal(&Boolean::TRUE)?;
544 /// Boolean::kary_or(&[b.clone(), c.clone()])?.enforce_equal(&Boolean::FALSE)?;
545 ///
546 /// assert!(cs.is_satisfied().unwrap());
547 /// # Ok(())
548 /// # }
549 /// ```
550 #[tracing::instrument(target = "r1cs")]
551 pub fn kary_or(bits: &[Self]) -> Result<Self, SynthesisError> {
552 assert!(!bits.is_empty());
553 let mut cur: Option<Self> = None;
554 for next in bits {
555 cur = if let Some(b) = cur {
556 Some(b.or(next)?)
557 } else {
558 Some(next.clone())
559 };
560 }
561
562 Ok(cur.expect("should not be 0"))
563 }
564
565 /// Outputs `(bits[0] & bits[1] & ... & bits.last().unwrap()).not()`.
566 ///
567 /// ```
568 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
569 /// // We'll use the BLS12-381 scalar field for our constraints.
570 /// use ark_test_curves::bls12_381::Fr;
571 /// use ark_relations::r1cs::*;
572 /// use ark_r1cs_std::prelude::*;
573 ///
574 /// let cs = ConstraintSystem::<Fr>::new_ref();
575 ///
576 /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
577 /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
578 /// let c = Boolean::new_witness(cs.clone(), || Ok(true))?;
579 ///
580 /// Boolean::kary_nand(&[a.clone(), b.clone(), c.clone()])?.enforce_equal(&Boolean::TRUE)?;
581 /// Boolean::kary_nand(&[a.clone(), c.clone()])?.enforce_equal(&Boolean::FALSE)?;
582 /// Boolean::kary_nand(&[b.clone(), c.clone()])?.enforce_equal(&Boolean::TRUE)?;
583 ///
584 /// assert!(cs.is_satisfied().unwrap());
585 /// # Ok(())
586 /// # }
587 /// ```
588 #[tracing::instrument(target = "r1cs")]
589 pub fn kary_nand(bits: &[Self]) -> Result<Self, SynthesisError> {
590 Ok(Self::kary_and(bits)?.not())
591 }
592
593 /// Enforces that `Self::kary_nand(bits).is_eq(&Boolean::TRUE)`.
594 ///
595 /// Informally, this means that at least one element in `bits` must be
596 /// `false`.
597 #[tracing::instrument(target = "r1cs")]
598 fn enforce_kary_nand(bits: &[Self]) -> Result<(), SynthesisError> {
599 use Boolean::*;
600 let r = Self::kary_nand(bits)?;
601 match r {
602 Constant(true) => Ok(()),
603 Constant(false) => Err(SynthesisError::AssignmentMissing),
604 Is(_) | Not(_) => {
605 r.cs()
606 .enforce_constraint(r.lc(), lc!() + Variable::One, lc!() + Variable::One)
607 }
608 }
609 }
610
611 /// Enforces that `bits`, when interpreted as a integer, is less than
612 /// `F::characteristic()`, That is, interpret bits as a little-endian
613 /// integer, and enforce that this integer is "in the field Z_p", where
614 /// `p = F::characteristic()` .
615 #[tracing::instrument(target = "r1cs")]
616 pub fn enforce_in_field_le(bits: &[Self]) -> Result<(), SynthesisError> {
617 // `bits` < F::characteristic() <==> `bits` <= F::characteristic() -1
618 let mut b = F::characteristic().to_vec();
619 assert_eq!(b[0] % 2, 1);
620 b[0] -= 1; // This works, because the LSB is one, so there's no borrows.
621 let run = Self::enforce_smaller_or_equal_than_le(bits, b)?;
622
623 // We should always end in a "run" of zeros, because
624 // the characteristic is an odd prime. So, this should
625 // be empty.
626 assert!(run.is_empty());
627
628 Ok(())
629 }
630
631 /// Enforces that `bits` is less than or equal to `element`,
632 /// when both are interpreted as (little-endian) integers.
633 #[tracing::instrument(target = "r1cs", skip(element))]
634 pub fn enforce_smaller_or_equal_than_le<'a>(
635 bits: &[Self],
636 element: impl AsRef<[u64]>,
637 ) -> Result<Vec<Self>, SynthesisError> {
638 let b: &[u64] = element.as_ref();
639
640 let mut bits_iter = bits.iter().rev(); // Iterate in big-endian
641
642 // Runs of ones in r
643 let mut last_run = Boolean::constant(true);
644 let mut current_run = vec![];
645
646 let mut element_num_bits = 0;
647 for _ in BitIteratorBE::without_leading_zeros(b) {
648 element_num_bits += 1;
649 }
650
651 if bits.len() > element_num_bits {
652 let mut or_result = Boolean::constant(false);
653 for should_be_zero in &bits[element_num_bits..] {
654 or_result = or_result.or(should_be_zero)?;
655 let _ = bits_iter.next().unwrap();
656 }
657 or_result.enforce_equal(&Boolean::constant(false))?;
658 }
659
660 for (b, a) in BitIteratorBE::without_leading_zeros(b).zip(bits_iter.by_ref()) {
661 if b {
662 // This is part of a run of ones.
663 current_run.push(a.clone());
664 } else {
665 if !current_run.is_empty() {
666 // This is the start of a run of zeros, but we need
667 // to k-ary AND against `last_run` first.
668
669 current_run.push(last_run.clone());
670 last_run = Self::kary_and(¤t_run)?;
671 current_run.truncate(0);
672 }
673
674 // If `last_run` is true, `a` must be false, or it would
675 // not be in the field.
676 //
677 // If `last_run` is false, `a` can be true or false.
678 //
679 // Ergo, at least one of `last_run` and `a` must be false.
680 Self::enforce_kary_nand(&[last_run.clone(), a.clone()])?;
681 }
682 }
683 assert!(bits_iter.next().is_none());
684
685 Ok(current_run)
686 }
687
688 /// Conditionally selects one of `first` and `second` based on the value of
689 /// `self`:
690 ///
691 /// If `self.is_eq(&Boolean::TRUE)`, this outputs `first`; else, it outputs
692 /// `second`. ```
693 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
694 /// // We'll use the BLS12-381 scalar field for our constraints.
695 /// use ark_test_curves::bls12_381::Fr;
696 /// use ark_relations::r1cs::*;
697 /// use ark_r1cs_std::prelude::*;
698 ///
699 /// let cs = ConstraintSystem::<Fr>::new_ref();
700 ///
701 /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
702 /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
703 ///
704 /// let cond = Boolean::new_witness(cs.clone(), || Ok(true))?;
705 ///
706 /// cond.select(&a, &b)?.enforce_equal(&Boolean::TRUE)?;
707 /// cond.select(&b, &a)?.enforce_equal(&Boolean::FALSE)?;
708 ///
709 /// assert!(cs.is_satisfied().unwrap());
710 /// # Ok(())
711 /// # }
712 /// ```
713 #[tracing::instrument(target = "r1cs", skip(first, second))]
714 pub fn select<T: CondSelectGadget<F>>(
715 &self,
716 first: &T,
717 second: &T,
718 ) -> Result<T, SynthesisError> {
719 T::conditionally_select(&self, first, second)
720 }
721}
722
723impl<F: Field> From<AllocatedBit<F>> for Boolean<F> {
724 fn from(b: AllocatedBit<F>) -> Self {
725 Boolean::Is(b)
726 }
727}
728
729impl<F: Field> AllocVar<bool, F> for Boolean<F> {
730 fn new_variable<T: Borrow<bool>>(
731 cs: impl Into<Namespace<F>>,
732 f: impl FnOnce() -> Result<T, SynthesisError>,
733 mode: AllocationMode,
734 ) -> Result<Self, SynthesisError> {
735 if mode == AllocationMode::Constant {
736 Ok(Boolean::Constant(*f()?.borrow()))
737 } else {
738 AllocatedBit::new_variable(cs, f, mode).map(Boolean::from)
739 }
740 }
741}
742
743impl<F: Field> EqGadget<F> for Boolean<F> {
744 #[tracing::instrument(target = "r1cs")]
745 fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
746 // self | other | XNOR(self, other) | self == other
747 // -----|-------|-------------------|--------------
748 // 0 | 0 | 1 | 1
749 // 0 | 1 | 0 | 0
750 // 1 | 0 | 0 | 0
751 // 1 | 1 | 1 | 1
752 Ok(self.xor(other)?.not())
753 }
754
755 #[tracing::instrument(target = "r1cs")]
756 fn conditional_enforce_equal(
757 &self,
758 other: &Self,
759 condition: &Boolean<F>,
760 ) -> Result<(), SynthesisError> {
761 use Boolean::*;
762 let one = Variable::One;
763 let difference = match (self, other) {
764 // 1 == 1; 0 == 0
765 (Constant(true), Constant(true)) | (Constant(false), Constant(false)) => return Ok(()),
766 // false != true
767 (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
768 // 1 - a
769 (Constant(true), Is(a)) | (Is(a), Constant(true)) => lc!() + one - a.variable(),
770 // a - 0 = a
771 (Constant(false), Is(a)) | (Is(a), Constant(false)) => lc!() + a.variable(),
772 // 1 - !a = 1 - (1 - a) = a
773 (Constant(true), Not(a)) | (Not(a), Constant(true)) => lc!() + a.variable(),
774 // !a - 0 = !a = 1 - a
775 (Constant(false), Not(a)) | (Not(a), Constant(false)) => lc!() + one - a.variable(),
776 // b - a,
777 (Is(a), Is(b)) => lc!() + b.variable() - a.variable(),
778 // !b - a = (1 - b) - a
779 (Is(a), Not(b)) | (Not(b), Is(a)) => lc!() + one - b.variable() - a.variable(),
780 // !b - !a = (1 - b) - (1 - a) = a - b,
781 (Not(a), Not(b)) => lc!() + a.variable() - b.variable(),
782 };
783
784 if condition != &Constant(false) {
785 let cs = self.cs().or(other.cs()).or(condition.cs());
786 cs.enforce_constraint(lc!() + difference, condition.lc(), lc!())?;
787 }
788 Ok(())
789 }
790
791 #[tracing::instrument(target = "r1cs")]
792 fn conditional_enforce_not_equal(
793 &self,
794 other: &Self,
795 should_enforce: &Boolean<F>,
796 ) -> Result<(), SynthesisError> {
797 use Boolean::*;
798 let one = Variable::One;
799 let difference = match (self, other) {
800 // 1 != 0; 0 != 1
801 (Constant(true), Constant(false)) | (Constant(false), Constant(true)) => return Ok(()),
802 // false == false and true == true
803 (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
804 // 1 - a
805 (Constant(true), Is(a)) | (Is(a), Constant(true)) => lc!() + one - a.variable(),
806 // a - 0 = a
807 (Constant(false), Is(a)) | (Is(a), Constant(false)) => lc!() + a.variable(),
808 // 1 - !a = 1 - (1 - a) = a
809 (Constant(true), Not(a)) | (Not(a), Constant(true)) => lc!() + a.variable(),
810 // !a - 0 = !a = 1 - a
811 (Constant(false), Not(a)) | (Not(a), Constant(false)) => lc!() + one - a.variable(),
812 // b - a,
813 (Is(a), Is(b)) => lc!() + b.variable() - a.variable(),
814 // !b - a = (1 - b) - a
815 (Is(a), Not(b)) | (Not(b), Is(a)) => lc!() + one - b.variable() - a.variable(),
816 // !b - !a = (1 - b) - (1 - a) = a - b,
817 (Not(a), Not(b)) => lc!() + a.variable() - b.variable(),
818 };
819
820 if should_enforce != &Constant(false) {
821 let cs = self.cs().or(other.cs()).or(should_enforce.cs());
822 cs.enforce_constraint(difference, should_enforce.lc(), should_enforce.lc())?;
823 }
824 Ok(())
825 }
826}
827
828impl<F: Field> ToBytesGadget<F> for Boolean<F> {
829 /// Outputs `1u8` if `self` is true, and `0u8` otherwise.
830 #[tracing::instrument(target = "r1cs")]
831 fn to_bytes(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
832 let value = self.value().map(u8::from).ok();
833 let mut bits = [Boolean::FALSE; 8];
834 bits[0] = self.clone();
835 Ok(vec![UInt8 { bits, value }])
836 }
837}
838
839impl<F: PrimeField> ToConstraintFieldGadget<F> for Boolean<F> {
840 #[tracing::instrument(target = "r1cs")]
841 fn to_constraint_field(&self) -> Result<Vec<FpVar<F>>, SynthesisError> {
842 let var = From::from(self.clone());
843 Ok(vec![var])
844 }
845}
846
847impl<F: Field> CondSelectGadget<F> for Boolean<F> {
848 #[tracing::instrument(target = "r1cs")]
849 fn conditionally_select(
850 cond: &Boolean<F>,
851 true_val: &Self,
852 false_val: &Self,
853 ) -> Result<Self, SynthesisError> {
854 use Boolean::*;
855 match cond {
856 Constant(true) => Ok(true_val.clone()),
857 Constant(false) => Ok(false_val.clone()),
858 cond @ Not(_) => Self::conditionally_select(&cond.not(), false_val, true_val),
859 cond @ Is(_) => match (true_val, false_val) {
860 (x, &Constant(false)) => cond.and(x),
861 (&Constant(false), x) => cond.not().and(x),
862 (&Constant(true), x) => cond.or(x),
863 (x, &Constant(true)) => cond.not().or(x),
864 (a, b) => {
865 let cs = cond.cs();
866 let result: Boolean<F> =
867 AllocatedBit::new_witness_without_booleanity_check(cs.clone(), || {
868 let cond = cond.value()?;
869 Ok(if cond { a.value()? } else { b.value()? })
870 })?
871 .into();
872 // a = self; b = other; c = cond;
873 //
874 // r = c * a + (1 - c) * b
875 // r = b + c * (a - b)
876 // c * (a - b) = r - b
877 //
878 // If a, b, cond are all boolean, so is r.
879 //
880 // self | other | cond | result
881 // -----|-------|----------------
882 // 0 | 0 | 1 | 0
883 // 0 | 1 | 1 | 0
884 // 1 | 0 | 1 | 1
885 // 1 | 1 | 1 | 1
886 // 0 | 0 | 0 | 0
887 // 0 | 1 | 0 | 1
888 // 1 | 0 | 0 | 0
889 // 1 | 1 | 0 | 1
890 cs.enforce_constraint(
891 cond.lc(),
892 lc!() + a.lc() - b.lc(),
893 lc!() + result.lc() - b.lc(),
894 )?;
895
896 Ok(result)
897 }
898 },
899 }
900 }
901}
902
903#[cfg(test)]
904mod test {
905 use super::{AllocatedBit, Boolean};
906 use crate::prelude::*;
907 use ark_ff::{BitIteratorBE, BitIteratorLE, Field, One, PrimeField, UniformRand, Zero};
908 use ark_relations::r1cs::{ConstraintSystem, Namespace, SynthesisError};
909 use ark_test_curves::bls12_381::Fr;
910 use rand::SeedableRng;
911 use rand_xorshift::XorShiftRng;
912
913 #[test]
914 fn test_boolean_to_byte() -> Result<(), SynthesisError> {
915 for val in [true, false].iter() {
916 let cs = ConstraintSystem::<Fr>::new_ref();
917 let a = Boolean::new_witness(cs.clone(), || Ok(*val))?;
918 let bytes = a.to_bytes()?;
919 assert_eq!(bytes.len(), 1);
920 let byte = &bytes[0];
921 assert_eq!(byte.value()?, *val as u8);
922
923 for (i, bit) in byte.bits.iter().enumerate() {
924 assert_eq!(bit.value()?, (byte.value()? >> i) & 1 == 1);
925 }
926 }
927 Ok(())
928 }
929
930 #[test]
931 fn test_xor() -> Result<(), SynthesisError> {
932 for a_val in [false, true].iter().copied() {
933 for b_val in [false, true].iter().copied() {
934 let cs = ConstraintSystem::<Fr>::new_ref();
935 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
936 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
937 let c = AllocatedBit::xor(&a, &b)?;
938 assert_eq!(c.value()?, a_val ^ b_val);
939
940 assert!(cs.is_satisfied().unwrap());
941 assert_eq!(a.value()?, (a_val));
942 assert_eq!(b.value()?, (b_val));
943 assert_eq!(c.value()?, (a_val ^ b_val));
944 }
945 }
946 Ok(())
947 }
948
949 #[test]
950 fn test_or() -> Result<(), SynthesisError> {
951 for a_val in [false, true].iter().copied() {
952 for b_val in [false, true].iter().copied() {
953 let cs = ConstraintSystem::<Fr>::new_ref();
954 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
955 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
956 let c = AllocatedBit::or(&a, &b)?;
957 assert_eq!(c.value()?, a_val | b_val);
958
959 assert!(cs.is_satisfied().unwrap());
960 assert_eq!(a.value()?, (a_val));
961 assert_eq!(b.value()?, (b_val));
962 assert_eq!(c.value()?, (a_val | b_val));
963 }
964 }
965 Ok(())
966 }
967
968 #[test]
969 fn test_and() -> Result<(), SynthesisError> {
970 for a_val in [false, true].iter().copied() {
971 for b_val in [false, true].iter().copied() {
972 let cs = ConstraintSystem::<Fr>::new_ref();
973 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
974 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
975 let c = AllocatedBit::and(&a, &b)?;
976 assert_eq!(c.value()?, a_val & b_val);
977
978 assert!(cs.is_satisfied().unwrap());
979 assert_eq!(a.value()?, (a_val));
980 assert_eq!(b.value()?, (b_val));
981 assert_eq!(c.value()?, (a_val & b_val));
982 }
983 }
984 Ok(())
985 }
986
987 #[test]
988 fn test_and_not() -> Result<(), SynthesisError> {
989 for a_val in [false, true].iter().copied() {
990 for b_val in [false, true].iter().copied() {
991 let cs = ConstraintSystem::<Fr>::new_ref();
992 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
993 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
994 let c = AllocatedBit::and_not(&a, &b)?;
995 assert_eq!(c.value()?, a_val & !b_val);
996
997 assert!(cs.is_satisfied().unwrap());
998 assert_eq!(a.value()?, (a_val));
999 assert_eq!(b.value()?, (b_val));
1000 assert_eq!(c.value()?, (a_val & !b_val));
1001 }
1002 }
1003 Ok(())
1004 }
1005
1006 #[test]
1007 fn test_nor() -> Result<(), SynthesisError> {
1008 for a_val in [false, true].iter().copied() {
1009 for b_val in [false, true].iter().copied() {
1010 let cs = ConstraintSystem::<Fr>::new_ref();
1011 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
1012 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
1013 let c = AllocatedBit::nor(&a, &b)?;
1014 assert_eq!(c.value()?, !a_val & !b_val);
1015
1016 assert!(cs.is_satisfied().unwrap());
1017 assert_eq!(a.value()?, (a_val));
1018 assert_eq!(b.value()?, (b_val));
1019 assert_eq!(c.value()?, (!a_val & !b_val));
1020 }
1021 }
1022 Ok(())
1023 }
1024
1025 #[test]
1026 fn test_enforce_equal() -> Result<(), SynthesisError> {
1027 for a_bool in [false, true].iter().cloned() {
1028 for b_bool in [false, true].iter().cloned() {
1029 for a_neg in [false, true].iter().cloned() {
1030 for b_neg in [false, true].iter().cloned() {
1031 let cs = ConstraintSystem::<Fr>::new_ref();
1032
1033 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
1034 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
1035
1036 if a_neg {
1037 a = a.not();
1038 }
1039 if b_neg {
1040 b = b.not();
1041 }
1042
1043 a.enforce_equal(&b)?;
1044
1045 assert_eq!(
1046 cs.is_satisfied().unwrap(),
1047 (a_bool ^ a_neg) == (b_bool ^ b_neg)
1048 );
1049 }
1050 }
1051 }
1052 }
1053 Ok(())
1054 }
1055
1056 #[test]
1057 fn test_conditional_enforce_equal() -> Result<(), SynthesisError> {
1058 for a_bool in [false, true].iter().cloned() {
1059 for b_bool in [false, true].iter().cloned() {
1060 for a_neg in [false, true].iter().cloned() {
1061 for b_neg in [false, true].iter().cloned() {
1062 let cs = ConstraintSystem::<Fr>::new_ref();
1063
1064 // First test if constraint system is satisfied
1065 // when we do want to enforce the condition.
1066 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
1067 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
1068
1069 if a_neg {
1070 a = a.not();
1071 }
1072 if b_neg {
1073 b = b.not();
1074 }
1075
1076 a.conditional_enforce_equal(&b, &Boolean::constant(true))?;
1077
1078 assert_eq!(
1079 cs.is_satisfied().unwrap(),
1080 (a_bool ^ a_neg) == (b_bool ^ b_neg)
1081 );
1082
1083 // Now test if constraint system is satisfied even
1084 // when we don't want to enforce the condition.
1085 let cs = ConstraintSystem::<Fr>::new_ref();
1086
1087 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
1088 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
1089
1090 if a_neg {
1091 a = a.not();
1092 }
1093 if b_neg {
1094 b = b.not();
1095 }
1096
1097 let false_cond =
1098 Boolean::new_witness(ark_relations::ns!(cs, "cond"), || Ok(false))?;
1099 a.conditional_enforce_equal(&b, &false_cond)?;
1100
1101 assert!(cs.is_satisfied().unwrap());
1102 }
1103 }
1104 }
1105 }
1106 Ok(())
1107 }
1108
1109 #[test]
1110 fn test_boolean_negation() -> Result<(), SynthesisError> {
1111 let cs = ConstraintSystem::<Fr>::new_ref();
1112
1113 let mut b = Boolean::new_witness(cs.clone(), || Ok(true))?;
1114 assert!(matches!(b, Boolean::Is(_)));
1115
1116 b = b.not();
1117 assert!(matches!(b, Boolean::Not(_)));
1118
1119 b = b.not();
1120 assert!(matches!(b, Boolean::Is(_)));
1121
1122 b = Boolean::Constant(true);
1123 assert!(matches!(b, Boolean::Constant(true)));
1124
1125 b = b.not();
1126 assert!(matches!(b, Boolean::Constant(false)));
1127
1128 b = b.not();
1129 assert!(matches!(b, Boolean::Constant(true)));
1130 Ok(())
1131 }
1132
1133 #[derive(Eq, PartialEq, Copy, Clone, Debug)]
1134 enum OpType {
1135 True,
1136 False,
1137 AllocatedTrue,
1138 AllocatedFalse,
1139 NegatedAllocatedTrue,
1140 NegatedAllocatedFalse,
1141 }
1142
1143 const VARIANTS: [OpType; 6] = [
1144 OpType::True,
1145 OpType::False,
1146 OpType::AllocatedTrue,
1147 OpType::AllocatedFalse,
1148 OpType::NegatedAllocatedTrue,
1149 OpType::NegatedAllocatedFalse,
1150 ];
1151
1152 fn construct<F: Field>(
1153 ns: Namespace<F>,
1154 operand: OpType,
1155 ) -> Result<Boolean<F>, SynthesisError> {
1156 let cs = ns.cs();
1157
1158 let b = match operand {
1159 OpType::True => Boolean::constant(true),
1160 OpType::False => Boolean::constant(false),
1161 OpType::AllocatedTrue => Boolean::new_witness(cs, || Ok(true))?,
1162 OpType::AllocatedFalse => Boolean::new_witness(cs, || Ok(false))?,
1163 OpType::NegatedAllocatedTrue => Boolean::new_witness(cs, || Ok(true))?.not(),
1164 OpType::NegatedAllocatedFalse => Boolean::new_witness(cs, || Ok(false))?.not(),
1165 };
1166 Ok(b)
1167 }
1168
1169 #[test]
1170 fn test_boolean_xor() -> Result<(), SynthesisError> {
1171 for first_operand in VARIANTS.iter().cloned() {
1172 for second_operand in VARIANTS.iter().cloned() {
1173 let cs = ConstraintSystem::<Fr>::new_ref();
1174
1175 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1176 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1177 let c = Boolean::xor(&a, &b)?;
1178
1179 assert!(cs.is_satisfied().unwrap());
1180
1181 match (first_operand, second_operand, c) {
1182 (OpType::True, OpType::True, Boolean::Constant(false)) => (),
1183 (OpType::True, OpType::False, Boolean::Constant(true)) => (),
1184 (OpType::True, OpType::AllocatedTrue, Boolean::Not(_)) => (),
1185 (OpType::True, OpType::AllocatedFalse, Boolean::Not(_)) => (),
1186 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Is(_)) => (),
1187 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Is(_)) => (),
1188
1189 (OpType::False, OpType::True, Boolean::Constant(true)) => (),
1190 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1191 (OpType::False, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1192 (OpType::False, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1193 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1194 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1195
1196 (OpType::AllocatedTrue, OpType::True, Boolean::Not(_)) => (),
1197 (OpType::AllocatedTrue, OpType::False, Boolean::Is(_)) => (),
1198 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1199 assert_eq!(v.value(), Ok(false));
1200 }
1201 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1202 assert_eq!(v.value(), Ok(true));
1203 }
1204 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1205 assert_eq!(v.value(), Ok(false));
1206 }
1207 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Not(ref v)) => {
1208 assert_eq!(v.value(), Ok(true));
1209 }
1210 (OpType::AllocatedFalse, OpType::True, Boolean::Not(_)) => (),
1211 (OpType::AllocatedFalse, OpType::False, Boolean::Is(_)) => (),
1212 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1213 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1214 assert_eq!(v.value(), Ok(true));
1215 }
1216 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1217 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1218 assert_eq!(v.value(), Ok(false));
1219 }
1220 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1221 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1222 assert_eq!(v.value(), Ok(true));
1223 }
1224 (
1225 OpType::AllocatedFalse,
1226 OpType::NegatedAllocatedFalse,
1227 Boolean::Not(ref v),
1228 ) => {
1229 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1230 assert_eq!(v.value(), Ok(false));
1231 }
1232
1233 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Is(_)) => (),
1234 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Not(_)) => (),
1235 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1236 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1237 assert_eq!(v.value(), Ok(false));
1238 }
1239 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Not(ref v)) => {
1240 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1241 assert_eq!(v.value(), Ok(true));
1242 }
1243 (
1244 OpType::NegatedAllocatedTrue,
1245 OpType::NegatedAllocatedTrue,
1246 Boolean::Is(ref v),
1247 ) => {
1248 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1249 assert_eq!(v.value(), Ok(false));
1250 }
1251 (
1252 OpType::NegatedAllocatedTrue,
1253 OpType::NegatedAllocatedFalse,
1254 Boolean::Is(ref v),
1255 ) => {
1256 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1257 assert_eq!(v.value(), Ok(true));
1258 }
1259
1260 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Is(_)) => (),
1261 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Not(_)) => (),
1262 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1263 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1264 assert_eq!(v.value(), Ok(true));
1265 }
1266 (
1267 OpType::NegatedAllocatedFalse,
1268 OpType::AllocatedFalse,
1269 Boolean::Not(ref v),
1270 ) => {
1271 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1272 assert_eq!(v.value(), Ok(false));
1273 }
1274 (
1275 OpType::NegatedAllocatedFalse,
1276 OpType::NegatedAllocatedTrue,
1277 Boolean::Is(ref v),
1278 ) => {
1279 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1280 assert_eq!(v.value(), Ok(true));
1281 }
1282 (
1283 OpType::NegatedAllocatedFalse,
1284 OpType::NegatedAllocatedFalse,
1285 Boolean::Is(ref v),
1286 ) => {
1287 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1288 assert_eq!(v.value(), Ok(false));
1289 }
1290
1291 _ => unreachable!(),
1292 }
1293 }
1294 }
1295 Ok(())
1296 }
1297
1298 #[test]
1299 fn test_boolean_cond_select() -> Result<(), SynthesisError> {
1300 for condition in VARIANTS.iter().cloned() {
1301 for first_operand in VARIANTS.iter().cloned() {
1302 for second_operand in VARIANTS.iter().cloned() {
1303 let cs = ConstraintSystem::<Fr>::new_ref();
1304
1305 let cond = construct(ark_relations::ns!(cs, "cond"), condition)?;
1306 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1307 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1308 let c = cond.select(&a, &b)?;
1309
1310 assert!(
1311 cs.is_satisfied().unwrap(),
1312 "failed with operands: cond: {:?}, a: {:?}, b: {:?}",
1313 condition,
1314 first_operand,
1315 second_operand,
1316 );
1317 assert_eq!(
1318 c.value()?,
1319 if cond.value()? {
1320 a.value()?
1321 } else {
1322 b.value()?
1323 }
1324 );
1325 }
1326 }
1327 }
1328 Ok(())
1329 }
1330
1331 #[test]
1332 fn test_boolean_or() -> Result<(), SynthesisError> {
1333 for first_operand in VARIANTS.iter().cloned() {
1334 for second_operand in VARIANTS.iter().cloned() {
1335 let cs = ConstraintSystem::<Fr>::new_ref();
1336
1337 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1338 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1339 let c = a.or(&b)?;
1340
1341 assert!(cs.is_satisfied().unwrap());
1342
1343 match (first_operand, second_operand, c.clone()) {
1344 (OpType::True, OpType::True, Boolean::Constant(true)) => (),
1345 (OpType::True, OpType::False, Boolean::Constant(true)) => (),
1346 (OpType::True, OpType::AllocatedTrue, Boolean::Constant(true)) => (),
1347 (OpType::True, OpType::AllocatedFalse, Boolean::Constant(true)) => (),
1348 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Constant(true)) => (),
1349 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Constant(true)) => (),
1350
1351 (OpType::False, OpType::True, Boolean::Constant(true)) => (),
1352 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1353 (OpType::False, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1354 (OpType::False, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1355 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1356 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1357
1358 (OpType::AllocatedTrue, OpType::True, Boolean::Constant(true)) => (),
1359 (OpType::AllocatedTrue, OpType::False, Boolean::Is(_)) => (),
1360 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1361 assert_eq!(v.value(), Ok(true));
1362 }
1363 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1364 assert_eq!(v.value(), Ok(true));
1365 }
1366 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1367 assert_eq!(v.value(), Ok(false));
1368 }
1369 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Not(ref v)) => {
1370 assert_eq!(v.value(), Ok(false));
1371 }
1372
1373 (OpType::AllocatedFalse, OpType::True, Boolean::Constant(true)) => (),
1374 (OpType::AllocatedFalse, OpType::False, Boolean::Is(_)) => (),
1375 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1376 assert_eq!(v.value(), Ok(true));
1377 }
1378 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1379 assert_eq!(v.value(), Ok(false));
1380 }
1381 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1382 assert_eq!(v.value(), Ok(true));
1383 }
1384 (
1385 OpType::AllocatedFalse,
1386 OpType::NegatedAllocatedFalse,
1387 Boolean::Not(ref v),
1388 ) => {
1389 assert_eq!(v.value(), Ok(false));
1390 }
1391
1392 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Constant(true)) => (),
1393 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Not(_)) => (),
1394 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1395 assert_eq!(v.value(), Ok(false));
1396 }
1397 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Not(ref v)) => {
1398 assert_eq!(v.value(), Ok(true));
1399 }
1400 (
1401 OpType::NegatedAllocatedTrue,
1402 OpType::NegatedAllocatedTrue,
1403 Boolean::Not(ref v),
1404 ) => {
1405 assert_eq!(v.value(), Ok(true));
1406 }
1407 (
1408 OpType::NegatedAllocatedTrue,
1409 OpType::NegatedAllocatedFalse,
1410 Boolean::Not(ref v),
1411 ) => {
1412 assert_eq!(v.value(), Ok(false));
1413 }
1414
1415 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Constant(true)) => (),
1416 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Not(_)) => (),
1417 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1418 assert_eq!(v.value(), Ok(false));
1419 }
1420 (
1421 OpType::NegatedAllocatedFalse,
1422 OpType::AllocatedFalse,
1423 Boolean::Not(ref v),
1424 ) => {
1425 assert_eq!(v.value(), Ok(false));
1426 }
1427 (
1428 OpType::NegatedAllocatedFalse,
1429 OpType::NegatedAllocatedTrue,
1430 Boolean::Not(ref v),
1431 ) => {
1432 assert_eq!(v.value(), Ok(false));
1433 }
1434 (
1435 OpType::NegatedAllocatedFalse,
1436 OpType::NegatedAllocatedFalse,
1437 Boolean::Not(ref v),
1438 ) => {
1439 assert_eq!(v.value(), Ok(false));
1440 }
1441
1442 _ => panic!(
1443 "this should never be encountered, in case: (a = {:?}, b = {:?}, c = {:?})",
1444 a, b, c
1445 ),
1446 }
1447 }
1448 }
1449 Ok(())
1450 }
1451
1452 #[test]
1453 fn test_boolean_and() -> Result<(), SynthesisError> {
1454 for first_operand in VARIANTS.iter().cloned() {
1455 for second_operand in VARIANTS.iter().cloned() {
1456 let cs = ConstraintSystem::<Fr>::new_ref();
1457
1458 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1459 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1460 let c = a.and(&b)?;
1461
1462 assert!(cs.is_satisfied().unwrap());
1463
1464 match (first_operand, second_operand, c) {
1465 (OpType::True, OpType::True, Boolean::Constant(true)) => (),
1466 (OpType::True, OpType::False, Boolean::Constant(false)) => (),
1467 (OpType::True, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1468 (OpType::True, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1469 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1470 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1471
1472 (OpType::False, OpType::True, Boolean::Constant(false)) => (),
1473 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1474 (OpType::False, OpType::AllocatedTrue, Boolean::Constant(false)) => (),
1475 (OpType::False, OpType::AllocatedFalse, Boolean::Constant(false)) => (),
1476 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Constant(false)) => (),
1477 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Constant(false)) => (),
1478
1479 (OpType::AllocatedTrue, OpType::True, Boolean::Is(_)) => (),
1480 (OpType::AllocatedTrue, OpType::False, Boolean::Constant(false)) => (),
1481 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1482 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1483 assert_eq!(v.value(), Ok(true));
1484 }
1485 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1486 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1487 assert_eq!(v.value(), Ok(false));
1488 }
1489 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Is(ref v)) => {
1490 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1491 assert_eq!(v.value(), Ok(false));
1492 }
1493 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Is(ref v)) => {
1494 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1495 assert_eq!(v.value(), Ok(true));
1496 }
1497
1498 (OpType::AllocatedFalse, OpType::True, Boolean::Is(_)) => (),
1499 (OpType::AllocatedFalse, OpType::False, Boolean::Constant(false)) => (),
1500 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1501 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1502 assert_eq!(v.value(), Ok(false));
1503 }
1504 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1505 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1506 assert_eq!(v.value(), Ok(false));
1507 }
1508 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Is(ref v)) => {
1509 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1510 assert_eq!(v.value(), Ok(false));
1511 }
1512 (OpType::AllocatedFalse, OpType::NegatedAllocatedFalse, Boolean::Is(ref v)) => {
1513 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1514 assert_eq!(v.value(), Ok(false));
1515 }
1516
1517 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Not(_)) => (),
1518 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Constant(false)) => (),
1519 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1520 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1521 assert_eq!(v.value(), Ok(false));
1522 }
1523 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1524 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1525 assert_eq!(v.value(), Ok(false));
1526 }
1527 (
1528 OpType::NegatedAllocatedTrue,
1529 OpType::NegatedAllocatedTrue,
1530 Boolean::Is(ref v),
1531 ) => {
1532 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1533 assert_eq!(v.value(), Ok(false));
1534 }
1535 (
1536 OpType::NegatedAllocatedTrue,
1537 OpType::NegatedAllocatedFalse,
1538 Boolean::Is(ref v),
1539 ) => {
1540 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1541 assert_eq!(v.value(), Ok(false));
1542 }
1543
1544 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Not(_)) => (),
1545 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Constant(false)) => (),
1546 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1547 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1548 assert_eq!(v.value(), Ok(true));
1549 }
1550 (OpType::NegatedAllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1551 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1552 assert_eq!(v.value(), Ok(false));
1553 }
1554 (
1555 OpType::NegatedAllocatedFalse,
1556 OpType::NegatedAllocatedTrue,
1557 Boolean::Is(ref v),
1558 ) => {
1559 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1560 assert_eq!(v.value(), Ok(false));
1561 }
1562 (
1563 OpType::NegatedAllocatedFalse,
1564 OpType::NegatedAllocatedFalse,
1565 Boolean::Is(ref v),
1566 ) => {
1567 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1568 assert_eq!(v.value(), Ok(true));
1569 }
1570
1571 _ => {
1572 panic!(
1573 "unexpected behavior at {:?} AND {:?}",
1574 first_operand, second_operand
1575 );
1576 }
1577 }
1578 }
1579 }
1580 Ok(())
1581 }
1582
1583 #[test]
1584 fn test_smaller_than_or_equal_to() -> Result<(), SynthesisError> {
1585 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1586 for _ in 0..1000 {
1587 let mut r = Fr::rand(&mut rng);
1588 let mut s = Fr::rand(&mut rng);
1589 if r > s {
1590 core::mem::swap(&mut r, &mut s)
1591 }
1592
1593 let cs = ConstraintSystem::<Fr>::new_ref();
1594
1595 let native_bits: Vec<_> = BitIteratorLE::new(r.into_repr()).collect();
1596 let bits = Vec::new_witness(cs.clone(), || Ok(native_bits))?;
1597 Boolean::enforce_smaller_or_equal_than_le(&bits, s.into_repr())?;
1598
1599 assert!(cs.is_satisfied().unwrap());
1600 }
1601
1602 for _ in 0..1000 {
1603 let r = Fr::rand(&mut rng);
1604 if r == -Fr::one() {
1605 continue;
1606 }
1607 let s = r + Fr::one();
1608 let s2 = r.double();
1609 let cs = ConstraintSystem::<Fr>::new_ref();
1610
1611 let native_bits: Vec<_> = BitIteratorLE::new(r.into_repr()).collect();
1612 let bits = Vec::new_witness(cs.clone(), || Ok(native_bits))?;
1613 Boolean::enforce_smaller_or_equal_than_le(&bits, s.into_repr())?;
1614 if r < s2 {
1615 Boolean::enforce_smaller_or_equal_than_le(&bits, s2.into_repr())?;
1616 }
1617
1618 assert!(cs.is_satisfied().unwrap());
1619 }
1620 Ok(())
1621 }
1622
1623 #[test]
1624 fn test_enforce_in_field() -> Result<(), SynthesisError> {
1625 {
1626 let cs = ConstraintSystem::<Fr>::new_ref();
1627
1628 let mut bits = vec![];
1629 for b in BitIteratorBE::new(Fr::characteristic()).skip(1) {
1630 bits.push(Boolean::new_witness(cs.clone(), || Ok(b))?);
1631 }
1632 bits.reverse();
1633
1634 Boolean::enforce_in_field_le(&bits)?;
1635
1636 assert!(!cs.is_satisfied().unwrap());
1637 }
1638
1639 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1640
1641 for _ in 0..1000 {
1642 let r = Fr::rand(&mut rng);
1643 let cs = ConstraintSystem::<Fr>::new_ref();
1644
1645 let mut bits = vec![];
1646 for b in BitIteratorBE::new(r.into_repr()).skip(1) {
1647 bits.push(Boolean::new_witness(cs.clone(), || Ok(b))?);
1648 }
1649 bits.reverse();
1650
1651 Boolean::enforce_in_field_le(&bits)?;
1652
1653 assert!(cs.is_satisfied().unwrap());
1654 }
1655 Ok(())
1656 }
1657
1658 #[test]
1659 fn test_enforce_nand() -> Result<(), SynthesisError> {
1660 {
1661 let cs = ConstraintSystem::<Fr>::new_ref();
1662
1663 assert!(
1664 Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), false)?]).is_ok()
1665 );
1666 assert!(
1667 Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), true)?]).is_err()
1668 );
1669 }
1670
1671 for i in 1..5 {
1672 // with every possible assignment for them
1673 for mut b in 0..(1 << i) {
1674 // with every possible negation
1675 for mut n in 0..(1 << i) {
1676 let cs = ConstraintSystem::<Fr>::new_ref();
1677
1678 let mut expected = true;
1679
1680 let mut bits = vec![];
1681 for _ in 0..i {
1682 expected &= b & 1 == 1;
1683
1684 let bit = if n & 1 == 1 {
1685 Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?
1686 } else {
1687 Boolean::new_witness(cs.clone(), || Ok(b & 1 == 0))?.not()
1688 };
1689 bits.push(bit);
1690
1691 b >>= 1;
1692 n >>= 1;
1693 }
1694
1695 let expected = !expected;
1696
1697 Boolean::enforce_kary_nand(&bits)?;
1698
1699 if expected {
1700 assert!(cs.is_satisfied().unwrap());
1701 } else {
1702 assert!(!cs.is_satisfied().unwrap());
1703 }
1704 }
1705 }
1706 }
1707 Ok(())
1708 }
1709
1710 #[test]
1711 fn test_kary_and() -> Result<(), SynthesisError> {
1712 // test different numbers of operands
1713 for i in 1..15 {
1714 // with every possible assignment for them
1715 for mut b in 0..(1 << i) {
1716 let cs = ConstraintSystem::<Fr>::new_ref();
1717
1718 let mut expected = true;
1719
1720 let mut bits = vec![];
1721 for _ in 0..i {
1722 expected &= b & 1 == 1;
1723 bits.push(Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?);
1724 b >>= 1;
1725 }
1726
1727 let r = Boolean::kary_and(&bits)?;
1728
1729 assert!(cs.is_satisfied().unwrap());
1730
1731 if let Boolean::Is(ref r) = r {
1732 assert_eq!(r.value()?, expected);
1733 }
1734 }
1735 }
1736 Ok(())
1737 }
1738}