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