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 /// ```
694 /// # fn main() -> Result<(), ark_relations::r1cs::SynthesisError> {
695 /// // We'll use the BLS12-381 scalar field for our constraints.
696 /// use ark_test_curves::bls12_381::Fr;
697 /// use ark_relations::r1cs::*;
698 /// use ark_r1cs_std::prelude::*;
699 ///
700 /// let cs = ConstraintSystem::<Fr>::new_ref();
701 ///
702 /// let a = Boolean::new_witness(cs.clone(), || Ok(true))?;
703 /// let b = Boolean::new_witness(cs.clone(), || Ok(false))?;
704 ///
705 /// let cond = Boolean::new_witness(cs.clone(), || Ok(true))?;
706 ///
707 /// cond.select(&a, &b)?.enforce_equal(&Boolean::TRUE)?;
708 /// cond.select(&b, &a)?.enforce_equal(&Boolean::FALSE)?;
709 ///
710 /// assert!(cs.is_satisfied().unwrap());
711 /// # Ok(())
712 /// # }
713 /// ```
714 ///
715 #[tracing::instrument(target = "r1cs", skip(first, second))]
716 pub fn select<T: CondSelectGadget<F>>(
717 &self,
718 first: &T,
719 second: &T,
720 ) -> Result<T, SynthesisError> {
721 T::conditionally_select(&self, first, second)
722 }
723}
724
725impl<F: Field> From<AllocatedBit<F>> for Boolean<F> {
726 fn from(b: AllocatedBit<F>) -> Self {
727 Boolean::Is(b)
728 }
729}
730
731impl<F: Field> AllocVar<bool, F> for Boolean<F> {
732 fn new_variable<T: Borrow<bool>>(
733 cs: impl Into<Namespace<F>>,
734 f: impl FnOnce() -> Result<T, SynthesisError>,
735 mode: AllocationMode,
736 ) -> Result<Self, SynthesisError> {
737 if mode == AllocationMode::Constant {
738 Ok(Boolean::Constant(*f()?.borrow()))
739 } else {
740 AllocatedBit::new_variable(cs, f, mode).map(Boolean::from)
741 }
742 }
743}
744
745impl<F: Field> EqGadget<F> for Boolean<F> {
746 #[tracing::instrument(target = "r1cs")]
747 fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
748 // self | other | XNOR(self, other) | self == other
749 // -----|-------|-------------------|--------------
750 // 0 | 0 | 1 | 1
751 // 0 | 1 | 0 | 0
752 // 1 | 0 | 0 | 0
753 // 1 | 1 | 1 | 1
754 Ok(self.xor(other)?.not())
755 }
756
757 #[tracing::instrument(target = "r1cs")]
758 fn conditional_enforce_equal(
759 &self,
760 other: &Self,
761 condition: &Boolean<F>,
762 ) -> Result<(), SynthesisError> {
763 use Boolean::*;
764 let one = Variable::One;
765 let difference = match (self, other) {
766 // 1 == 1; 0 == 0
767 (Constant(true), Constant(true)) | (Constant(false), Constant(false)) => return Ok(()),
768 // false != true
769 (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
770 // 1 - a
771 (Constant(true), Is(a)) | (Is(a), Constant(true)) => lc!() + one - a.variable(),
772 // a - 0 = a
773 (Constant(false), Is(a)) | (Is(a), Constant(false)) => lc!() + a.variable(),
774 // 1 - !a = 1 - (1 - a) = a
775 (Constant(true), Not(a)) | (Not(a), Constant(true)) => lc!() + a.variable(),
776 // !a - 0 = !a = 1 - a
777 (Constant(false), Not(a)) | (Not(a), Constant(false)) => lc!() + one - a.variable(),
778 // b - a,
779 (Is(a), Is(b)) => lc!() + b.variable() - a.variable(),
780 // !b - a = (1 - b) - a
781 (Is(a), Not(b)) | (Not(b), Is(a)) => lc!() + one - b.variable() - a.variable(),
782 // !b - !a = (1 - b) - (1 - a) = a - b,
783 (Not(a), Not(b)) => lc!() + a.variable() - b.variable(),
784 };
785
786 if condition != &Constant(false) {
787 let cs = self.cs().or(other.cs()).or(condition.cs());
788 cs.enforce_constraint(lc!() + difference, condition.lc(), lc!())?;
789 }
790 Ok(())
791 }
792
793 #[tracing::instrument(target = "r1cs")]
794 fn conditional_enforce_not_equal(
795 &self,
796 other: &Self,
797 should_enforce: &Boolean<F>,
798 ) -> Result<(), SynthesisError> {
799 use Boolean::*;
800 let one = Variable::One;
801 let difference = match (self, other) {
802 // 1 != 0; 0 != 1
803 (Constant(true), Constant(false)) | (Constant(false), Constant(true)) => return Ok(()),
804 // false == false and true == true
805 (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
806 // 1 - a
807 (Constant(true), Is(a)) | (Is(a), Constant(true)) => lc!() + one - a.variable(),
808 // a - 0 = a
809 (Constant(false), Is(a)) | (Is(a), Constant(false)) => lc!() + a.variable(),
810 // 1 - !a = 1 - (1 - a) = a
811 (Constant(true), Not(a)) | (Not(a), Constant(true)) => lc!() + a.variable(),
812 // !a - 0 = !a = 1 - a
813 (Constant(false), Not(a)) | (Not(a), Constant(false)) => lc!() + one - a.variable(),
814 // b - a,
815 (Is(a), Is(b)) => lc!() + b.variable() - a.variable(),
816 // !b - a = (1 - b) - a
817 (Is(a), Not(b)) | (Not(b), Is(a)) => lc!() + one - b.variable() - a.variable(),
818 // !b - !a = (1 - b) - (1 - a) = a - b,
819 (Not(a), Not(b)) => lc!() + a.variable() - b.variable(),
820 };
821
822 if should_enforce != &Constant(false) {
823 let cs = self.cs().or(other.cs()).or(should_enforce.cs());
824 cs.enforce_constraint(difference, should_enforce.lc(), should_enforce.lc())?;
825 }
826 Ok(())
827 }
828}
829
830impl<F: Field> ToBytesGadget<F> for Boolean<F> {
831 /// Outputs `1u8` if `self` is true, and `0u8` otherwise.
832 #[tracing::instrument(target = "r1cs")]
833 fn to_bytes(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
834 let value = self.value().map(u8::from).ok();
835 let mut bits = [Boolean::FALSE; 8];
836 bits[0] = self.clone();
837 Ok(vec![UInt8 { bits, value }])
838 }
839}
840
841impl<F: PrimeField> ToConstraintFieldGadget<F> for Boolean<F> {
842 #[tracing::instrument(target = "r1cs")]
843 fn to_constraint_field(&self) -> Result<Vec<FpVar<F>>, SynthesisError> {
844 let var = From::from(self.clone());
845 Ok(vec![var])
846 }
847}
848
849impl<F: Field> CondSelectGadget<F> for Boolean<F> {
850 #[tracing::instrument(target = "r1cs")]
851 fn conditionally_select(
852 cond: &Boolean<F>,
853 true_val: &Self,
854 false_val: &Self,
855 ) -> Result<Self, SynthesisError> {
856 use Boolean::*;
857 match cond {
858 Constant(true) => Ok(true_val.clone()),
859 Constant(false) => Ok(false_val.clone()),
860 cond @ Not(_) => Self::conditionally_select(&cond.not(), false_val, true_val),
861 cond @ Is(_) => match (true_val, false_val) {
862 (x, &Constant(false)) => cond.and(x),
863 (&Constant(false), x) => cond.not().and(x),
864 (&Constant(true), x) => cond.or(x),
865 (x, &Constant(true)) => cond.not().or(x),
866 (a, b) => {
867 let cs = cond.cs();
868 let result: Boolean<F> =
869 AllocatedBit::new_witness_without_booleanity_check(cs.clone(), || {
870 let cond = cond.value()?;
871 Ok(if cond { a.value()? } else { b.value()? })
872 })?
873 .into();
874 // a = self; b = other; c = cond;
875 //
876 // r = c * a + (1 - c) * b
877 // r = b + c * (a - b)
878 // c * (a - b) = r - b
879 //
880 // If a, b, cond are all boolean, so is r.
881 //
882 // self | other | cond | result
883 // -----|-------|----------------
884 // 0 | 0 | 1 | 0
885 // 0 | 1 | 1 | 0
886 // 1 | 0 | 1 | 1
887 // 1 | 1 | 1 | 1
888 // 0 | 0 | 0 | 0
889 // 0 | 1 | 0 | 1
890 // 1 | 0 | 0 | 0
891 // 1 | 1 | 0 | 1
892 cs.enforce_constraint(
893 cond.lc(),
894 lc!() + a.lc() - b.lc(),
895 lc!() + result.lc() - b.lc(),
896 )?;
897
898 Ok(result)
899 }
900 },
901 }
902 }
903}
904
905#[cfg(test)]
906mod test {
907 use super::{AllocatedBit, Boolean};
908 use crate::prelude::*;
909 use ark_ff::{BitIteratorBE, BitIteratorLE, Field, One, PrimeField, UniformRand, Zero};
910 use ark_relations::r1cs::{ConstraintSystem, Namespace, SynthesisError};
911 use ark_test_curves::bls12_381::Fr;
912 use rand::SeedableRng;
913 use rand_xorshift::XorShiftRng;
914
915 #[test]
916 fn test_boolean_to_byte() -> Result<(), SynthesisError> {
917 for val in [true, false].iter() {
918 let cs = ConstraintSystem::<Fr>::new_ref();
919 let a = Boolean::new_witness(cs.clone(), || Ok(*val))?;
920 let bytes = a.to_bytes()?;
921 assert_eq!(bytes.len(), 1);
922 let byte = &bytes[0];
923 assert_eq!(byte.value()?, *val as u8);
924
925 for (i, bit) in byte.bits.iter().enumerate() {
926 assert_eq!(bit.value()?, (byte.value()? >> i) & 1 == 1);
927 }
928 }
929 Ok(())
930 }
931
932 #[test]
933 fn test_xor() -> Result<(), SynthesisError> {
934 for a_val in [false, true].iter().copied() {
935 for b_val in [false, true].iter().copied() {
936 let cs = ConstraintSystem::<Fr>::new_ref();
937 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
938 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
939 let c = AllocatedBit::xor(&a, &b)?;
940 assert_eq!(c.value()?, a_val ^ b_val);
941
942 assert!(cs.is_satisfied().unwrap());
943 assert_eq!(a.value()?, (a_val));
944 assert_eq!(b.value()?, (b_val));
945 assert_eq!(c.value()?, (a_val ^ b_val));
946 }
947 }
948 Ok(())
949 }
950
951 #[test]
952 fn test_or() -> Result<(), SynthesisError> {
953 for a_val in [false, true].iter().copied() {
954 for b_val in [false, true].iter().copied() {
955 let cs = ConstraintSystem::<Fr>::new_ref();
956 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
957 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
958 let c = AllocatedBit::or(&a, &b)?;
959 assert_eq!(c.value()?, a_val | b_val);
960
961 assert!(cs.is_satisfied().unwrap());
962 assert_eq!(a.value()?, (a_val));
963 assert_eq!(b.value()?, (b_val));
964 assert_eq!(c.value()?, (a_val | b_val));
965 }
966 }
967 Ok(())
968 }
969
970 #[test]
971 fn test_and() -> Result<(), SynthesisError> {
972 for a_val in [false, true].iter().copied() {
973 for b_val in [false, true].iter().copied() {
974 let cs = ConstraintSystem::<Fr>::new_ref();
975 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
976 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
977 let c = AllocatedBit::and(&a, &b)?;
978 assert_eq!(c.value()?, a_val & b_val);
979
980 assert!(cs.is_satisfied().unwrap());
981 assert_eq!(a.value()?, (a_val));
982 assert_eq!(b.value()?, (b_val));
983 assert_eq!(c.value()?, (a_val & b_val));
984 }
985 }
986 Ok(())
987 }
988
989 #[test]
990 fn test_and_not() -> Result<(), SynthesisError> {
991 for a_val in [false, true].iter().copied() {
992 for b_val in [false, true].iter().copied() {
993 let cs = ConstraintSystem::<Fr>::new_ref();
994 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
995 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
996 let c = AllocatedBit::and_not(&a, &b)?;
997 assert_eq!(c.value()?, a_val & !b_val);
998
999 assert!(cs.is_satisfied().unwrap());
1000 assert_eq!(a.value()?, (a_val));
1001 assert_eq!(b.value()?, (b_val));
1002 assert_eq!(c.value()?, (a_val & !b_val));
1003 }
1004 }
1005 Ok(())
1006 }
1007
1008 #[test]
1009 fn test_nor() -> Result<(), SynthesisError> {
1010 for a_val in [false, true].iter().copied() {
1011 for b_val in [false, true].iter().copied() {
1012 let cs = ConstraintSystem::<Fr>::new_ref();
1013 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
1014 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
1015 let c = AllocatedBit::nor(&a, &b)?;
1016 assert_eq!(c.value()?, !a_val & !b_val);
1017
1018 assert!(cs.is_satisfied().unwrap());
1019 assert_eq!(a.value()?, (a_val));
1020 assert_eq!(b.value()?, (b_val));
1021 assert_eq!(c.value()?, (!a_val & !b_val));
1022 }
1023 }
1024 Ok(())
1025 }
1026
1027 #[test]
1028 fn test_enforce_equal() -> Result<(), SynthesisError> {
1029 for a_bool in [false, true].iter().cloned() {
1030 for b_bool in [false, true].iter().cloned() {
1031 for a_neg in [false, true].iter().cloned() {
1032 for b_neg in [false, true].iter().cloned() {
1033 let cs = ConstraintSystem::<Fr>::new_ref();
1034
1035 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
1036 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
1037
1038 if a_neg {
1039 a = a.not();
1040 }
1041 if b_neg {
1042 b = b.not();
1043 }
1044
1045 a.enforce_equal(&b)?;
1046
1047 assert_eq!(
1048 cs.is_satisfied().unwrap(),
1049 (a_bool ^ a_neg) == (b_bool ^ b_neg)
1050 );
1051 }
1052 }
1053 }
1054 }
1055 Ok(())
1056 }
1057
1058 #[test]
1059 fn test_conditional_enforce_equal() -> Result<(), SynthesisError> {
1060 for a_bool in [false, true].iter().cloned() {
1061 for b_bool in [false, true].iter().cloned() {
1062 for a_neg in [false, true].iter().cloned() {
1063 for b_neg in [false, true].iter().cloned() {
1064 let cs = ConstraintSystem::<Fr>::new_ref();
1065
1066 // First test if constraint system is satisfied
1067 // when we do want to enforce the condition.
1068 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
1069 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
1070
1071 if a_neg {
1072 a = a.not();
1073 }
1074 if b_neg {
1075 b = b.not();
1076 }
1077
1078 a.conditional_enforce_equal(&b, &Boolean::constant(true))?;
1079
1080 assert_eq!(
1081 cs.is_satisfied().unwrap(),
1082 (a_bool ^ a_neg) == (b_bool ^ b_neg)
1083 );
1084
1085 // Now test if constraint system is satisfied even
1086 // when we don't want to enforce the condition.
1087 let cs = ConstraintSystem::<Fr>::new_ref();
1088
1089 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
1090 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
1091
1092 if a_neg {
1093 a = a.not();
1094 }
1095 if b_neg {
1096 b = b.not();
1097 }
1098
1099 let false_cond =
1100 Boolean::new_witness(ark_relations::ns!(cs, "cond"), || Ok(false))?;
1101 a.conditional_enforce_equal(&b, &false_cond)?;
1102
1103 assert!(cs.is_satisfied().unwrap());
1104 }
1105 }
1106 }
1107 }
1108 Ok(())
1109 }
1110
1111 #[test]
1112 fn test_boolean_negation() -> Result<(), SynthesisError> {
1113 let cs = ConstraintSystem::<Fr>::new_ref();
1114
1115 let mut b = Boolean::new_witness(cs.clone(), || Ok(true))?;
1116 assert!(matches!(b, Boolean::Is(_)));
1117
1118 b = b.not();
1119 assert!(matches!(b, Boolean::Not(_)));
1120
1121 b = b.not();
1122 assert!(matches!(b, Boolean::Is(_)));
1123
1124 b = Boolean::Constant(true);
1125 assert!(matches!(b, Boolean::Constant(true)));
1126
1127 b = b.not();
1128 assert!(matches!(b, Boolean::Constant(false)));
1129
1130 b = b.not();
1131 assert!(matches!(b, Boolean::Constant(true)));
1132 Ok(())
1133 }
1134
1135 #[derive(Eq, PartialEq, Copy, Clone, Debug)]
1136 enum OpType {
1137 True,
1138 False,
1139 AllocatedTrue,
1140 AllocatedFalse,
1141 NegatedAllocatedTrue,
1142 NegatedAllocatedFalse,
1143 }
1144
1145 const VARIANTS: [OpType; 6] = [
1146 OpType::True,
1147 OpType::False,
1148 OpType::AllocatedTrue,
1149 OpType::AllocatedFalse,
1150 OpType::NegatedAllocatedTrue,
1151 OpType::NegatedAllocatedFalse,
1152 ];
1153
1154 fn construct<F: Field>(
1155 ns: Namespace<F>,
1156 operand: OpType,
1157 ) -> Result<Boolean<F>, SynthesisError> {
1158 let cs = ns.cs();
1159
1160 let b = match operand {
1161 OpType::True => Boolean::constant(true),
1162 OpType::False => Boolean::constant(false),
1163 OpType::AllocatedTrue => Boolean::new_witness(cs, || Ok(true))?,
1164 OpType::AllocatedFalse => Boolean::new_witness(cs, || Ok(false))?,
1165 OpType::NegatedAllocatedTrue => Boolean::new_witness(cs, || Ok(true))?.not(),
1166 OpType::NegatedAllocatedFalse => Boolean::new_witness(cs, || Ok(false))?.not(),
1167 };
1168 Ok(b)
1169 }
1170
1171 #[test]
1172 fn test_boolean_xor() -> Result<(), SynthesisError> {
1173 for first_operand in VARIANTS.iter().cloned() {
1174 for second_operand in VARIANTS.iter().cloned() {
1175 let cs = ConstraintSystem::<Fr>::new_ref();
1176
1177 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1178 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1179 let c = Boolean::xor(&a, &b)?;
1180
1181 assert!(cs.is_satisfied().unwrap());
1182
1183 match (first_operand, second_operand, c) {
1184 (OpType::True, OpType::True, Boolean::Constant(false)) => (),
1185 (OpType::True, OpType::False, Boolean::Constant(true)) => (),
1186 (OpType::True, OpType::AllocatedTrue, Boolean::Not(_)) => (),
1187 (OpType::True, OpType::AllocatedFalse, Boolean::Not(_)) => (),
1188 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Is(_)) => (),
1189 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Is(_)) => (),
1190
1191 (OpType::False, OpType::True, Boolean::Constant(true)) => (),
1192 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1193 (OpType::False, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1194 (OpType::False, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1195 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1196 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1197
1198 (OpType::AllocatedTrue, OpType::True, Boolean::Not(_)) => (),
1199 (OpType::AllocatedTrue, OpType::False, Boolean::Is(_)) => (),
1200 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1201 assert_eq!(v.value(), Ok(false));
1202 }
1203 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1204 assert_eq!(v.value(), Ok(true));
1205 }
1206 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1207 assert_eq!(v.value(), Ok(false));
1208 }
1209 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Not(ref v)) => {
1210 assert_eq!(v.value(), Ok(true));
1211 }
1212 (OpType::AllocatedFalse, OpType::True, Boolean::Not(_)) => (),
1213 (OpType::AllocatedFalse, OpType::False, Boolean::Is(_)) => (),
1214 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1215 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1216 assert_eq!(v.value(), Ok(true));
1217 }
1218 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1219 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1220 assert_eq!(v.value(), Ok(false));
1221 }
1222 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1223 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1224 assert_eq!(v.value(), Ok(true));
1225 }
1226 (
1227 OpType::AllocatedFalse,
1228 OpType::NegatedAllocatedFalse,
1229 Boolean::Not(ref v),
1230 ) => {
1231 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1232 assert_eq!(v.value(), Ok(false));
1233 }
1234
1235 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Is(_)) => (),
1236 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Not(_)) => (),
1237 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1238 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1239 assert_eq!(v.value(), Ok(false));
1240 }
1241 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Not(ref v)) => {
1242 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1243 assert_eq!(v.value(), Ok(true));
1244 }
1245 (
1246 OpType::NegatedAllocatedTrue,
1247 OpType::NegatedAllocatedTrue,
1248 Boolean::Is(ref v),
1249 ) => {
1250 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1251 assert_eq!(v.value(), Ok(false));
1252 }
1253 (
1254 OpType::NegatedAllocatedTrue,
1255 OpType::NegatedAllocatedFalse,
1256 Boolean::Is(ref v),
1257 ) => {
1258 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1259 assert_eq!(v.value(), Ok(true));
1260 }
1261
1262 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Is(_)) => (),
1263 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Not(_)) => (),
1264 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1265 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1266 assert_eq!(v.value(), Ok(true));
1267 }
1268 (
1269 OpType::NegatedAllocatedFalse,
1270 OpType::AllocatedFalse,
1271 Boolean::Not(ref v),
1272 ) => {
1273 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1274 assert_eq!(v.value(), Ok(false));
1275 }
1276 (
1277 OpType::NegatedAllocatedFalse,
1278 OpType::NegatedAllocatedTrue,
1279 Boolean::Is(ref v),
1280 ) => {
1281 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1282 assert_eq!(v.value(), Ok(true));
1283 }
1284 (
1285 OpType::NegatedAllocatedFalse,
1286 OpType::NegatedAllocatedFalse,
1287 Boolean::Is(ref v),
1288 ) => {
1289 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1290 assert_eq!(v.value(), Ok(false));
1291 }
1292
1293 _ => unreachable!(),
1294 }
1295 }
1296 }
1297 Ok(())
1298 }
1299
1300 #[test]
1301 fn test_boolean_cond_select() -> Result<(), SynthesisError> {
1302 for condition in VARIANTS.iter().cloned() {
1303 for first_operand in VARIANTS.iter().cloned() {
1304 for second_operand in VARIANTS.iter().cloned() {
1305 let cs = ConstraintSystem::<Fr>::new_ref();
1306
1307 let cond = construct(ark_relations::ns!(cs, "cond"), condition)?;
1308 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1309 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1310 let c = cond.select(&a, &b)?;
1311
1312 assert!(
1313 cs.is_satisfied().unwrap(),
1314 "failed with operands: cond: {:?}, a: {:?}, b: {:?}",
1315 condition,
1316 first_operand,
1317 second_operand,
1318 );
1319 assert_eq!(
1320 c.value()?,
1321 if cond.value()? {
1322 a.value()?
1323 } else {
1324 b.value()?
1325 }
1326 );
1327 }
1328 }
1329 }
1330 Ok(())
1331 }
1332
1333 #[test]
1334 fn test_boolean_or() -> Result<(), SynthesisError> {
1335 for first_operand in VARIANTS.iter().cloned() {
1336 for second_operand in VARIANTS.iter().cloned() {
1337 let cs = ConstraintSystem::<Fr>::new_ref();
1338
1339 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1340 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1341 let c = a.or(&b)?;
1342
1343 assert!(cs.is_satisfied().unwrap());
1344
1345 match (first_operand, second_operand, c.clone()) {
1346 (OpType::True, OpType::True, Boolean::Constant(true)) => (),
1347 (OpType::True, OpType::False, Boolean::Constant(true)) => (),
1348 (OpType::True, OpType::AllocatedTrue, Boolean::Constant(true)) => (),
1349 (OpType::True, OpType::AllocatedFalse, Boolean::Constant(true)) => (),
1350 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Constant(true)) => (),
1351 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Constant(true)) => (),
1352
1353 (OpType::False, OpType::True, Boolean::Constant(true)) => (),
1354 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1355 (OpType::False, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1356 (OpType::False, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1357 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1358 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1359
1360 (OpType::AllocatedTrue, OpType::True, Boolean::Constant(true)) => (),
1361 (OpType::AllocatedTrue, OpType::False, Boolean::Is(_)) => (),
1362 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1363 assert_eq!(v.value(), Ok(true));
1364 }
1365 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1366 assert_eq!(v.value(), Ok(true));
1367 }
1368 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1369 assert_eq!(v.value(), Ok(false));
1370 }
1371 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Not(ref v)) => {
1372 assert_eq!(v.value(), Ok(false));
1373 }
1374
1375 (OpType::AllocatedFalse, OpType::True, Boolean::Constant(true)) => (),
1376 (OpType::AllocatedFalse, OpType::False, Boolean::Is(_)) => (),
1377 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1378 assert_eq!(v.value(), Ok(true));
1379 }
1380 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1381 assert_eq!(v.value(), Ok(false));
1382 }
1383 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1384 assert_eq!(v.value(), Ok(true));
1385 }
1386 (
1387 OpType::AllocatedFalse,
1388 OpType::NegatedAllocatedFalse,
1389 Boolean::Not(ref v),
1390 ) => {
1391 assert_eq!(v.value(), Ok(false));
1392 }
1393
1394 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Constant(true)) => (),
1395 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Not(_)) => (),
1396 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1397 assert_eq!(v.value(), Ok(false));
1398 }
1399 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Not(ref v)) => {
1400 assert_eq!(v.value(), Ok(true));
1401 }
1402 (
1403 OpType::NegatedAllocatedTrue,
1404 OpType::NegatedAllocatedTrue,
1405 Boolean::Not(ref v),
1406 ) => {
1407 assert_eq!(v.value(), Ok(true));
1408 }
1409 (
1410 OpType::NegatedAllocatedTrue,
1411 OpType::NegatedAllocatedFalse,
1412 Boolean::Not(ref v),
1413 ) => {
1414 assert_eq!(v.value(), Ok(false));
1415 }
1416
1417 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Constant(true)) => (),
1418 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Not(_)) => (),
1419 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1420 assert_eq!(v.value(), Ok(false));
1421 }
1422 (
1423 OpType::NegatedAllocatedFalse,
1424 OpType::AllocatedFalse,
1425 Boolean::Not(ref v),
1426 ) => {
1427 assert_eq!(v.value(), Ok(false));
1428 }
1429 (
1430 OpType::NegatedAllocatedFalse,
1431 OpType::NegatedAllocatedTrue,
1432 Boolean::Not(ref v),
1433 ) => {
1434 assert_eq!(v.value(), Ok(false));
1435 }
1436 (
1437 OpType::NegatedAllocatedFalse,
1438 OpType::NegatedAllocatedFalse,
1439 Boolean::Not(ref v),
1440 ) => {
1441 assert_eq!(v.value(), Ok(false));
1442 }
1443
1444 _ => panic!(
1445 "this should never be encountered, in case: (a = {:?}, b = {:?}, c = {:?})",
1446 a, b, c
1447 ),
1448 }
1449 }
1450 }
1451 Ok(())
1452 }
1453
1454 #[test]
1455 fn test_boolean_and() -> Result<(), SynthesisError> {
1456 for first_operand in VARIANTS.iter().cloned() {
1457 for second_operand in VARIANTS.iter().cloned() {
1458 let cs = ConstraintSystem::<Fr>::new_ref();
1459
1460 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1461 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1462 let c = a.and(&b)?;
1463
1464 assert!(cs.is_satisfied().unwrap());
1465
1466 match (first_operand, second_operand, c) {
1467 (OpType::True, OpType::True, Boolean::Constant(true)) => (),
1468 (OpType::True, OpType::False, Boolean::Constant(false)) => (),
1469 (OpType::True, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1470 (OpType::True, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1471 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1472 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1473
1474 (OpType::False, OpType::True, Boolean::Constant(false)) => (),
1475 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1476 (OpType::False, OpType::AllocatedTrue, Boolean::Constant(false)) => (),
1477 (OpType::False, OpType::AllocatedFalse, Boolean::Constant(false)) => (),
1478 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Constant(false)) => (),
1479 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Constant(false)) => (),
1480
1481 (OpType::AllocatedTrue, OpType::True, Boolean::Is(_)) => (),
1482 (OpType::AllocatedTrue, OpType::False, Boolean::Constant(false)) => (),
1483 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1484 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1485 assert_eq!(v.value(), Ok(true));
1486 }
1487 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1488 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1489 assert_eq!(v.value(), Ok(false));
1490 }
1491 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Is(ref v)) => {
1492 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1493 assert_eq!(v.value(), Ok(false));
1494 }
1495 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Is(ref v)) => {
1496 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1497 assert_eq!(v.value(), Ok(true));
1498 }
1499
1500 (OpType::AllocatedFalse, OpType::True, Boolean::Is(_)) => (),
1501 (OpType::AllocatedFalse, OpType::False, Boolean::Constant(false)) => (),
1502 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1503 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1504 assert_eq!(v.value(), Ok(false));
1505 }
1506 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1507 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1508 assert_eq!(v.value(), Ok(false));
1509 }
1510 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Is(ref v)) => {
1511 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1512 assert_eq!(v.value(), Ok(false));
1513 }
1514 (OpType::AllocatedFalse, OpType::NegatedAllocatedFalse, Boolean::Is(ref v)) => {
1515 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1516 assert_eq!(v.value(), Ok(false));
1517 }
1518
1519 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Not(_)) => (),
1520 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Constant(false)) => (),
1521 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1522 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1523 assert_eq!(v.value(), Ok(false));
1524 }
1525 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1526 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1527 assert_eq!(v.value(), Ok(false));
1528 }
1529 (
1530 OpType::NegatedAllocatedTrue,
1531 OpType::NegatedAllocatedTrue,
1532 Boolean::Is(ref v),
1533 ) => {
1534 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1535 assert_eq!(v.value(), Ok(false));
1536 }
1537 (
1538 OpType::NegatedAllocatedTrue,
1539 OpType::NegatedAllocatedFalse,
1540 Boolean::Is(ref v),
1541 ) => {
1542 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1543 assert_eq!(v.value(), Ok(false));
1544 }
1545
1546 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Not(_)) => (),
1547 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Constant(false)) => (),
1548 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1549 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1550 assert_eq!(v.value(), Ok(true));
1551 }
1552 (OpType::NegatedAllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1553 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1554 assert_eq!(v.value(), Ok(false));
1555 }
1556 (
1557 OpType::NegatedAllocatedFalse,
1558 OpType::NegatedAllocatedTrue,
1559 Boolean::Is(ref v),
1560 ) => {
1561 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1562 assert_eq!(v.value(), Ok(false));
1563 }
1564 (
1565 OpType::NegatedAllocatedFalse,
1566 OpType::NegatedAllocatedFalse,
1567 Boolean::Is(ref v),
1568 ) => {
1569 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1570 assert_eq!(v.value(), Ok(true));
1571 }
1572
1573 _ => {
1574 panic!(
1575 "unexpected behavior at {:?} AND {:?}",
1576 first_operand, second_operand
1577 );
1578 }
1579 }
1580 }
1581 }
1582 Ok(())
1583 }
1584
1585 #[test]
1586 fn test_smaller_than_or_equal_to() -> Result<(), SynthesisError> {
1587 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1588 for _ in 0..1000 {
1589 let mut r = Fr::rand(&mut rng);
1590 let mut s = Fr::rand(&mut rng);
1591 if r > s {
1592 core::mem::swap(&mut r, &mut s)
1593 }
1594
1595 let cs = ConstraintSystem::<Fr>::new_ref();
1596
1597 let native_bits: Vec<_> = BitIteratorLE::new(r.into_repr()).collect();
1598 let bits = Vec::new_witness(cs.clone(), || Ok(native_bits))?;
1599 Boolean::enforce_smaller_or_equal_than_le(&bits, s.into_repr())?;
1600
1601 assert!(cs.is_satisfied().unwrap());
1602 }
1603
1604 for _ in 0..1000 {
1605 let r = Fr::rand(&mut rng);
1606 if r == -Fr::one() {
1607 continue;
1608 }
1609 let s = r + Fr::one();
1610 let s2 = r.double();
1611 let cs = ConstraintSystem::<Fr>::new_ref();
1612
1613 let native_bits: Vec<_> = BitIteratorLE::new(r.into_repr()).collect();
1614 let bits = Vec::new_witness(cs.clone(), || Ok(native_bits))?;
1615 Boolean::enforce_smaller_or_equal_than_le(&bits, s.into_repr())?;
1616 if r < s2 {
1617 Boolean::enforce_smaller_or_equal_than_le(&bits, s2.into_repr())?;
1618 }
1619
1620 assert!(cs.is_satisfied().unwrap());
1621 }
1622 Ok(())
1623 }
1624
1625 #[test]
1626 fn test_enforce_in_field() -> Result<(), SynthesisError> {
1627 {
1628 let cs = ConstraintSystem::<Fr>::new_ref();
1629
1630 let mut bits = vec![];
1631 for b in BitIteratorBE::new(Fr::characteristic()).skip(1) {
1632 bits.push(Boolean::new_witness(cs.clone(), || Ok(b))?);
1633 }
1634 bits.reverse();
1635
1636 Boolean::enforce_in_field_le(&bits)?;
1637
1638 assert!(!cs.is_satisfied().unwrap());
1639 }
1640
1641 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1642
1643 for _ in 0..1000 {
1644 let r = Fr::rand(&mut rng);
1645 let cs = ConstraintSystem::<Fr>::new_ref();
1646
1647 let mut bits = vec![];
1648 for b in BitIteratorBE::new(r.into_repr()).skip(1) {
1649 bits.push(Boolean::new_witness(cs.clone(), || Ok(b))?);
1650 }
1651 bits.reverse();
1652
1653 Boolean::enforce_in_field_le(&bits)?;
1654
1655 assert!(cs.is_satisfied().unwrap());
1656 }
1657 Ok(())
1658 }
1659
1660 #[test]
1661 fn test_enforce_nand() -> Result<(), SynthesisError> {
1662 {
1663 let cs = ConstraintSystem::<Fr>::new_ref();
1664
1665 assert!(
1666 Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), false)?]).is_ok()
1667 );
1668 assert!(
1669 Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), true)?]).is_err()
1670 );
1671 }
1672
1673 for i in 1..5 {
1674 // with every possible assignment for them
1675 for mut b in 0..(1 << i) {
1676 // with every possible negation
1677 for mut n in 0..(1 << i) {
1678 let cs = ConstraintSystem::<Fr>::new_ref();
1679
1680 let mut expected = true;
1681
1682 let mut bits = vec![];
1683 for _ in 0..i {
1684 expected &= b & 1 == 1;
1685
1686 let bit = if n & 1 == 1 {
1687 Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?
1688 } else {
1689 Boolean::new_witness(cs.clone(), || Ok(b & 1 == 0))?.not()
1690 };
1691 bits.push(bit);
1692
1693 b >>= 1;
1694 n >>= 1;
1695 }
1696
1697 let expected = !expected;
1698
1699 Boolean::enforce_kary_nand(&bits)?;
1700
1701 if expected {
1702 assert!(cs.is_satisfied().unwrap());
1703 } else {
1704 assert!(!cs.is_satisfied().unwrap());
1705 }
1706 }
1707 }
1708 }
1709 Ok(())
1710 }
1711
1712 #[test]
1713 fn test_kary_and() -> Result<(), SynthesisError> {
1714 // test different numbers of operands
1715 for i in 1..15 {
1716 // with every possible assignment for them
1717 for mut b in 0..(1 << i) {
1718 let cs = ConstraintSystem::<Fr>::new_ref();
1719
1720 let mut expected = true;
1721
1722 let mut bits = vec![];
1723 for _ in 0..i {
1724 expected &= b & 1 == 1;
1725 bits.push(Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?);
1726 b >>= 1;
1727 }
1728
1729 let r = Boolean::kary_and(&bits)?;
1730
1731 assert!(cs.is_satisfied().unwrap());
1732
1733 if let Boolean::Is(ref r) = r {
1734 assert_eq!(r.value()?, expected);
1735 }
1736 }
1737 }
1738 Ok(())
1739 }
1740}