ark-r1cs-std/r1cs-std/src/bits/boolean.rs
r1cs-std/src/bits/boolean.rsRaw
1use algebra::{BitIterator, Field, PrimeField};
2
3use crate::{prelude::*, Assignment, Vec};
4use core::borrow::Borrow;
5use r1cs_core::{ConstraintSystem, ConstraintVar, LinearCombination, SynthesisError, Variable};
6
7/// Represents a variable in the constraint system which is guaranteed
8/// to be either zero or one.
9#[derive(Copy, Clone, Debug)]
10pub struct AllocatedBit {
11 variable: Variable,
12 value: Option<bool>,
13}
14
15impl AllocatedBit {
16 pub fn get_value(&self) -> Option<bool> {
17 self.value
18 }
19
20 pub fn get_variable(&self) -> Variable {
21 self.variable
22 }
23
24 /// Performs an XOR operation over the two operands, returning
25 /// an `AllocatedBit`.
26 pub fn xor<ConstraintF, CS>(mut cs: CS, a: &Self, b: &Self) -> Result<Self, SynthesisError>
27 where
28 ConstraintF: Field,
29 CS: ConstraintSystem<ConstraintF>,
30 {
31 let mut result_value = None;
32
33 let result_var = cs.alloc(
34 || "xor result",
35 || {
36 if a.value.get()? ^ b.value.get()? {
37 result_value = Some(true);
38
39 Ok(ConstraintF::one())
40 } else {
41 result_value = Some(false);
42
43 Ok(ConstraintF::zero())
44 }
45 },
46 )?;
47
48 // Constrain (a + a) * (b) = (a + b - c)
49 // Given that a and b are boolean constrained, if they
50 // are equal, the only solution for c is 0, and if they
51 // are different, the only solution for c is 1.
52 //
53 // ¬(a ∧ b) ∧ ¬(¬a ∧ ¬b) = c
54 // (1 - (a * b)) * (1 - ((1 - a) * (1 - b))) = c
55 // (1 - ab) * (1 - (1 - a - b + ab)) = c
56 // (1 - ab) * (a + b - ab) = c
57 // a + b - ab - (a^2)b - (b^2)a + (a^2)(b^2) = c
58 // a + b - ab - ab - ab + ab = c
59 // a + b - 2ab = c
60 // -2a * b = c - a - b
61 // 2a * b = a + b - c
62 // (a + a) * b = a + b - c
63 cs.enforce(
64 || "xor constraint",
65 |lc| lc + a.variable + a.variable,
66 |lc| lc + b.variable,
67 |lc| lc + a.variable + b.variable - result_var,
68 );
69
70 Ok(AllocatedBit {
71 variable: result_var,
72 value: result_value,
73 })
74 }
75
76 /// Performs an AND operation over the two operands, returning
77 /// an `AllocatedBit`.
78 pub fn and<ConstraintF, CS>(mut cs: CS, a: &Self, b: &Self) -> Result<Self, SynthesisError>
79 where
80 ConstraintF: Field,
81 CS: ConstraintSystem<ConstraintF>,
82 {
83 let mut result_value = None;
84
85 let result_var = cs.alloc(
86 || "and result",
87 || {
88 if a.value.get()? & b.value.get()? {
89 result_value = Some(true);
90
91 Ok(ConstraintF::one())
92 } else {
93 result_value = Some(false);
94
95 Ok(ConstraintF::zero())
96 }
97 },
98 )?;
99
100 // Constrain (a) * (b) = (c), ensuring c is 1 iff
101 // a AND b are both 1.
102 cs.enforce(
103 || "and constraint",
104 |lc| lc + a.variable,
105 |lc| lc + b.variable,
106 |lc| lc + result_var,
107 );
108
109 Ok(AllocatedBit {
110 variable: result_var,
111 value: result_value,
112 })
113 }
114
115 /// Performs an OR operation over the two operands, returning
116 /// an `AllocatedBit`.
117 pub fn or<ConstraintF, CS>(mut cs: CS, a: &Self, b: &Self) -> Result<Self, SynthesisError>
118 where
119 ConstraintF: Field,
120 CS: ConstraintSystem<ConstraintF>,
121 {
122 let mut result_value = None;
123
124 let result_var = cs.alloc(
125 || "or result",
126 || {
127 if a.value.get()? | b.value.get()? {
128 result_value = Some(true);
129 Ok(ConstraintF::one())
130 } else {
131 result_value = Some(false);
132 Ok(ConstraintF::zero())
133 }
134 },
135 )?;
136
137 // Constrain (1 - a) * (1 - b) = (c), ensuring c is 1 iff
138 // a and b are both false, and otherwise c is 0.
139 cs.enforce(
140 || "nor constraint",
141 |lc| lc + CS::one() - a.variable,
142 |lc| lc + CS::one() - b.variable,
143 |lc| lc + CS::one() - result_var,
144 );
145
146 Ok(AllocatedBit {
147 variable: result_var,
148 value: result_value,
149 })
150 }
151
152 /// Calculates `a AND (NOT b)`.
153 pub fn and_not<ConstraintF, CS>(mut cs: CS, a: &Self, b: &Self) -> Result<Self, SynthesisError>
154 where
155 ConstraintF: Field,
156 CS: ConstraintSystem<ConstraintF>,
157 {
158 let mut result_value = None;
159
160 let result_var = cs.alloc(
161 || "and not result",
162 || {
163 if a.value.get()? & !b.value.get()? {
164 result_value = Some(true);
165
166 Ok(ConstraintF::one())
167 } else {
168 result_value = Some(false);
169
170 Ok(ConstraintF::zero())
171 }
172 },
173 )?;
174
175 // Constrain (a) * (1 - b) = (c), ensuring c is 1 iff
176 // a is true and b is false, and otherwise c is 0.
177 cs.enforce(
178 || "and not constraint",
179 |lc| lc + a.variable,
180 |lc| lc + CS::one() - b.variable,
181 |lc| lc + result_var,
182 );
183
184 Ok(AllocatedBit {
185 variable: result_var,
186 value: result_value,
187 })
188 }
189
190 /// Calculates `(NOT a) AND (NOT b)`.
191 pub fn nor<ConstraintF, CS>(mut cs: CS, a: &Self, b: &Self) -> Result<Self, SynthesisError>
192 where
193 ConstraintF: Field,
194 CS: ConstraintSystem<ConstraintF>,
195 {
196 let mut result_value = None;
197
198 let result_var = cs.alloc(
199 || "nor result",
200 || {
201 if !a.value.get()? & !b.value.get()? {
202 result_value = Some(true);
203
204 Ok(ConstraintF::one())
205 } else {
206 result_value = Some(false);
207
208 Ok(ConstraintF::zero())
209 }
210 },
211 )?;
212
213 // Constrain (1 - a) * (1 - b) = (c), ensuring c is 1 iff
214 // a and b are both false, and otherwise c is 0.
215 cs.enforce(
216 || "nor constraint",
217 |lc| lc + CS::one() - a.variable,
218 |lc| lc + CS::one() - b.variable,
219 |lc| lc + result_var,
220 );
221
222 Ok(AllocatedBit {
223 variable: result_var,
224 value: result_value,
225 })
226 }
227}
228
229impl PartialEq for AllocatedBit {
230 fn eq(&self, other: &Self) -> bool {
231 self.value.is_some() && other.value.is_some() && self.value == other.value
232 }
233}
234
235impl Eq for AllocatedBit {}
236
237impl<ConstraintF: Field> AllocGadget<bool, ConstraintF> for AllocatedBit {
238 fn alloc_constant<T, CS: ConstraintSystem<ConstraintF>>(
239 _cs: CS,
240 _t: T,
241 ) -> Result<Self, SynthesisError>
242 where
243 T: Borrow<bool>,
244 {
245 unimplemented!();
246 }
247
248 fn alloc<F, T, CS: ConstraintSystem<ConstraintF>>(
249 mut cs: CS,
250 value_gen: F,
251 ) -> Result<Self, SynthesisError>
252 where
253 F: FnOnce() -> Result<T, SynthesisError>,
254 T: Borrow<bool>,
255 {
256 let mut value = None;
257 let var = cs.alloc(
258 || "boolean",
259 || {
260 value = Some(*value_gen()?.borrow());
261 if value.get()? {
262 Ok(ConstraintF::one())
263 } else {
264 Ok(ConstraintF::zero())
265 }
266 },
267 )?;
268
269 // Constrain: (1 - a) * a = 0
270 // This constrains a to be either 0 or 1.
271 cs.enforce(
272 || "boolean constraint",
273 |lc| lc + CS::one() - var,
274 |lc| lc + var,
275 |lc| lc,
276 );
277
278 Ok(AllocatedBit {
279 variable: var,
280 value,
281 })
282 }
283
284 fn alloc_input<F, T, CS: ConstraintSystem<ConstraintF>>(
285 mut cs: CS,
286 value_gen: F,
287 ) -> Result<Self, SynthesisError>
288 where
289 F: FnOnce() -> Result<T, SynthesisError>,
290 T: Borrow<bool>,
291 {
292 let mut value = None;
293 let var = cs.alloc_input(
294 || "boolean",
295 || {
296 value = Some(*value_gen()?.borrow());
297 if value.get()? {
298 Ok(ConstraintF::one())
299 } else {
300 Ok(ConstraintF::zero())
301 }
302 },
303 )?;
304
305 // Constrain: (1 - a) * a = 0
306 // This constrains a to be either 0 or 1.
307 cs.enforce(
308 || "boolean constraint",
309 |lc| lc + CS::one() - var,
310 |lc| lc + var,
311 |lc| lc,
312 );
313
314 Ok(AllocatedBit {
315 variable: var,
316 value,
317 })
318 }
319}
320
321impl<ConstraintF: PrimeField> CondSelectGadget<ConstraintF> for AllocatedBit {
322 fn conditionally_select<CS: ConstraintSystem<ConstraintF>>(
323 cs: CS,
324 cond: &Boolean,
325 true_value: &Self,
326 false_value: &Self,
327 ) -> Result<Self, SynthesisError> {
328 cond_select_helper(
329 cs,
330 cond,
331 (true_value.value, true_value.variable),
332 (false_value.value, false_value.variable),
333 )
334 }
335
336 fn cost() -> usize {
337 1
338 }
339}
340
341fn cond_select_helper<F: PrimeField, CS: ConstraintSystem<F>>(
342 mut cs: CS,
343 cond: &Boolean,
344 first: (Option<bool>, impl Into<ConstraintVar<F>>),
345 second: (Option<bool>, impl Into<ConstraintVar<F>>),
346) -> Result<AllocatedBit, SynthesisError> {
347 let mut result_val = None;
348 let result_var = cs.alloc(
349 || "cond_select_result",
350 || {
351 result_val = cond
352 .get_value()
353 .and_then(|c| if c { first.0 } else { second.0 });
354 result_val.get().map(|v| F::from(v as u8))
355 },
356 )?;
357
358 let first_var = first.1.into();
359 let second_var = second.1.into();
360
361 // a = self; b = other; c = cond;
362 //
363 // r = c * a + (1 - c) * b
364 // r = b + c * (a - b)
365 // c * (a - b) = r - b
366 let one = CS::one();
367 cs.enforce(
368 || "conditionally_select",
369 |_| cond.lc(one, F::one()),
370 |lc| (&first_var - &second_var) + lc,
371 |lc| ConstraintVar::from(result_var) - &second_var + lc,
372 );
373
374 Ok(AllocatedBit {
375 value: result_val,
376 variable: result_var,
377 })
378}
379
380/// This is a boolean value which may be either a constant or
381/// an interpretation of an `AllocatedBit`.
382#[derive(Copy, Clone, Debug)]
383pub enum Boolean {
384 /// Existential view of the boolean variable
385 Is(AllocatedBit),
386 /// Negated view of the boolean variable
387 Not(AllocatedBit),
388 /// Constant (not an allocated variable)
389 Constant(bool),
390}
391
392impl Boolean {
393 pub fn get_value(&self) -> Option<bool> {
394 match *self {
395 Boolean::Constant(c) => Some(c),
396 Boolean::Is(ref v) => v.get_value(),
397 Boolean::Not(ref v) => v.get_value().map(|b| !b),
398 }
399 }
400
401 pub fn lc<ConstraintF: Field>(
402 &self,
403 one: Variable,
404 coeff: ConstraintF,
405 ) -> LinearCombination<ConstraintF> {
406 match *self {
407 Boolean::Constant(c) => {
408 if c {
409 (coeff, one).into()
410 } else {
411 LinearCombination::<ConstraintF>::zero()
412 }
413 }
414 Boolean::Is(ref v) => (coeff, v.get_variable()).into(),
415 Boolean::Not(ref v) => {
416 LinearCombination::<ConstraintF>::zero() + (coeff, one) - (coeff, v.get_variable())
417 }
418 }
419 }
420
421 /// Construct a boolean vector from a vector of u8
422 pub fn constant_u8_vec<ConstraintF: Field, CS: ConstraintSystem<ConstraintF>>(
423 cs: &mut CS,
424 values: &[u8],
425 ) -> Vec<Self> {
426 let mut input_bits = vec![];
427 for (byte_i, input_byte) in values.iter().enumerate() {
428 for bit_i in (0..8).rev() {
429 let cs = cs.ns(|| format!("input_bit_gadget {} {}", byte_i, bit_i));
430 input_bits.push(
431 AllocatedBit::alloc(cs, || Ok((input_byte >> bit_i) & 1u8 == 1u8))
432 .unwrap()
433 .into(),
434 );
435 }
436 }
437 input_bits
438 }
439
440 /// Construct a boolean from a known constant
441 pub fn constant(b: bool) -> Self {
442 Boolean::Constant(b)
443 }
444
445 /// Return a negated interpretation of this boolean.
446 pub fn not(&self) -> Self {
447 match *self {
448 Boolean::Constant(c) => Boolean::Constant(!c),
449 Boolean::Is(ref v) => Boolean::Not(*v),
450 Boolean::Not(ref v) => Boolean::Is(*v),
451 }
452 }
453
454 /// Perform XOR over two boolean operands
455 pub fn xor<'a, ConstraintF, CS>(
456 cs: CS,
457 a: &'a Self,
458 b: &'a Self,
459 ) -> Result<Self, SynthesisError>
460 where
461 ConstraintF: Field,
462 CS: ConstraintSystem<ConstraintF>,
463 {
464 match (a, b) {
465 (&Boolean::Constant(false), x) | (x, &Boolean::Constant(false)) => Ok(*x),
466 (&Boolean::Constant(true), x) | (x, &Boolean::Constant(true)) => Ok(x.not()),
467 // a XOR (NOT b) = NOT(a XOR b)
468 (is @ &Boolean::Is(_), not @ &Boolean::Not(_))
469 | (not @ &Boolean::Not(_), is @ &Boolean::Is(_)) => {
470 Ok(Boolean::xor(cs, is, ¬.not())?.not())
471 }
472 // a XOR b = (NOT a) XOR (NOT b)
473 (&Boolean::Is(ref a), &Boolean::Is(ref b))
474 | (&Boolean::Not(ref a), &Boolean::Not(ref b)) => {
475 Ok(Boolean::Is(AllocatedBit::xor(cs, a, b)?))
476 }
477 }
478 }
479
480 /// Perform OR over two boolean operands
481 pub fn or<'a, ConstraintF, CS>(cs: CS, a: &'a Self, b: &'a Self) -> Result<Self, SynthesisError>
482 where
483 ConstraintF: Field,
484 CS: ConstraintSystem<ConstraintF>,
485 {
486 match (a, b) {
487 (&Boolean::Constant(false), x) | (x, &Boolean::Constant(false)) => Ok(*x),
488 (&Boolean::Constant(true), _) | (_, &Boolean::Constant(true)) => {
489 Ok(Boolean::Constant(true))
490 }
491 // a OR b = NOT ((NOT a) AND b)
492 (a @ &Boolean::Is(_), b @ &Boolean::Not(_))
493 | (b @ &Boolean::Not(_), a @ &Boolean::Is(_))
494 | (b @ &Boolean::Not(_), a @ &Boolean::Not(_)) => {
495 Ok(Boolean::and(cs, &a.not(), &b.not())?.not())
496 }
497 (&Boolean::Is(ref a), &Boolean::Is(ref b)) => {
498 AllocatedBit::or(cs, a, b).map(Boolean::from)
499 }
500 }
501 }
502
503 /// Perform AND over two boolean operands
504 pub fn and<'a, ConstraintF, CS>(
505 cs: CS,
506 a: &'a Self,
507 b: &'a Self,
508 ) -> Result<Self, SynthesisError>
509 where
510 ConstraintF: Field,
511 CS: ConstraintSystem<ConstraintF>,
512 {
513 match (a, b) {
514 // false AND x is always false
515 (&Boolean::Constant(false), _) | (_, &Boolean::Constant(false)) => {
516 Ok(Boolean::Constant(false))
517 }
518 // true AND x is always x
519 (&Boolean::Constant(true), x) | (x, &Boolean::Constant(true)) => Ok(*x),
520 // a AND (NOT b)
521 (&Boolean::Is(ref is), &Boolean::Not(ref not))
522 | (&Boolean::Not(ref not), &Boolean::Is(ref is)) => {
523 Ok(Boolean::Is(AllocatedBit::and_not(cs, is, not)?))
524 }
525 // (NOT a) AND (NOT b) = a NOR b
526 (&Boolean::Not(ref a), &Boolean::Not(ref b)) => {
527 Ok(Boolean::Is(AllocatedBit::nor(cs, a, b)?))
528 }
529 // a AND b
530 (&Boolean::Is(ref a), &Boolean::Is(ref b)) => {
531 Ok(Boolean::Is(AllocatedBit::and(cs, a, b)?))
532 }
533 }
534 }
535
536 pub fn kary_and<ConstraintF, CS>(mut cs: CS, bits: &[Self]) -> Result<Self, SynthesisError>
537 where
538 ConstraintF: Field,
539 CS: ConstraintSystem<ConstraintF>,
540 {
541 assert!(!bits.is_empty());
542 let mut bits = bits.iter();
543
544 let mut cur: Self = *bits.next().unwrap();
545 for (i, next) in bits.enumerate() {
546 cur = Boolean::and(cs.ns(|| format!("AND {}", i)), &cur, next)?;
547 }
548
549 Ok(cur)
550 }
551
552 pub fn kary_or<ConstraintF, CS>(mut cs: CS, bits: &[Self]) -> Result<Self, SynthesisError>
553 where
554 ConstraintF: Field,
555 CS: ConstraintSystem<ConstraintF>,
556 {
557 assert!(!bits.is_empty());
558 let mut bits = bits.iter();
559
560 let mut cur: Self = *bits.next().unwrap();
561 for (i, next) in bits.enumerate() {
562 cur = Boolean::or(cs.ns(|| format!("OR {}", i)), &cur, next)?;
563 }
564
565 Ok(cur)
566 }
567
568 /// Asserts that at least one operand is false.
569 pub fn enforce_nand<ConstraintF, CS>(mut cs: CS, bits: &[Self]) -> Result<(), SynthesisError>
570 where
571 ConstraintF: Field,
572 CS: ConstraintSystem<ConstraintF>,
573 {
574 let res = Self::kary_and(&mut cs, bits)?;
575
576 match res {
577 Boolean::Constant(false) => Ok(()),
578 Boolean::Constant(true) => Err(SynthesisError::AssignmentMissing),
579 Boolean::Is(ref res) => {
580 cs.enforce(
581 || "enforce nand",
582 |lc| lc,
583 |lc| lc,
584 |lc| lc + res.get_variable(),
585 );
586
587 Ok(())
588 }
589 Boolean::Not(ref res) => {
590 cs.enforce(
591 || "enforce nand",
592 |lc| lc,
593 |lc| lc,
594 |lc| lc + CS::one() - res.get_variable(),
595 );
596
597 Ok(())
598 }
599 }
600 }
601
602 /// Asserts that this bit_gadget representation is "in
603 /// the field" when interpreted in big endian.
604 pub fn enforce_in_field<ConstraintF, CS, F: PrimeField>(
605 cs: CS,
606 bits: &[Self],
607 ) -> Result<(), SynthesisError>
608 where
609 ConstraintF: Field,
610 CS: ConstraintSystem<ConstraintF>,
611 {
612 // b = char() - 1
613 let mut b = F::characteristic().to_vec();
614 assert_eq!(b[0] % 2, 1);
615 b[0] -= 1;
616 let run = Self::enforce_smaller_or_equal_than::<_, _, F, _>(cs, bits, b)?;
617
618 // We should always end in a "run" of zeros, because
619 // the characteristic is an odd prime. So, this should
620 // be empty.
621 assert!(run.is_empty());
622
623 Ok(())
624 }
625
626 /// Asserts that this bit_gadget representation is smaller
627 /// or equal than the provided element
628 pub fn enforce_smaller_or_equal_than<ConstraintF, CS, F: PrimeField, E: AsRef<[u64]>>(
629 mut cs: CS,
630 bits: &[Self],
631 element: E,
632 ) -> Result<Vec<Boolean>, SynthesisError>
633 where
634 ConstraintF: Field,
635 CS: ConstraintSystem<ConstraintF>,
636 {
637 let mut bits_iter = bits.iter();
638 let b: &[u64] = element.as_ref();
639
640 // Runs of ones in r
641 let mut last_run = Boolean::constant(true);
642 let mut current_run = vec![];
643
644 let mut found_one = false;
645 let mut run_i = 0;
646 let mut nand_i = 0;
647
648 let char_num_bits = {
649 let mut leading_zeros = 0;
650 let mut total_bits = 0;
651 let mut found_one = false;
652 for b in BitIterator::new(b.clone()) {
653 total_bits += 1;
654 if !b && !found_one {
655 leading_zeros += 1
656 }
657 if b {
658 found_one = true;
659 }
660 }
661
662 total_bits - leading_zeros
663 };
664
665 if bits.len() > char_num_bits {
666 let num_extra_bits = bits.len() - char_num_bits;
667 let mut or_result = Boolean::constant(false);
668 for (i, should_be_zero) in bits[0..num_extra_bits].iter().enumerate() {
669 or_result = Boolean::or(
670 &mut cs.ns(|| format!("Check {}-th or", i)),
671 &or_result,
672 should_be_zero,
673 )?;
674 let _ = bits_iter.next().unwrap();
675 }
676 or_result.enforce_equal(
677 &mut cs.ns(|| "Check that or of extra bits is zero"),
678 &Boolean::constant(false),
679 )?;
680 }
681
682 for b in BitIterator::new(b) {
683 // Skip over unset bits at the beginning
684 found_one |= b;
685 if !found_one {
686 continue;
687 }
688
689 let a = bits_iter.next().unwrap();
690
691 if b {
692 // This is part of a run of ones.
693 current_run.push(a.clone());
694 } else {
695 if !current_run.is_empty() {
696 // This is the start of a run of zeros, but we need
697 // to k-ary AND against `last_run` first.
698
699 current_run.push(last_run);
700 last_run = Self::kary_and(cs.ns(|| format!("run {}", run_i)), ¤t_run)?;
701 run_i += 1;
702 current_run.truncate(0);
703 }
704
705 // If `last_run` is true, `a` must be false, or it would
706 // not be in the field.
707 //
708 // If `last_run` is false, `a` can be true or false.
709 //
710 // Ergo, at least one of `last_run` and `a` must be false.
711 Self::enforce_nand(cs.ns(|| format!("nand {}", nand_i)), &[last_run, *a])?;
712 nand_i += 1;
713 }
714 }
715 assert!(bits_iter.next().is_none());
716
717 Ok(current_run)
718 }
719}
720
721impl PartialEq for Boolean {
722 fn eq(&self, other: &Self) -> bool {
723 use self::Boolean::*;
724
725 match (*self, *other) {
726 (Is(a), Is(b)) | (Not(a), Not(b)) => a == b,
727 (Is(a), Not(b)) | (Not(a), Is(b)) => a != b,
728 (Is(a), Constant(b)) | (Constant(b), Is(a)) => a.value.unwrap() == b,
729 (Not(a), Constant(b)) | (Constant(b), Not(a)) => a.value.unwrap() != b,
730 (Constant(a), Constant(b)) => a == b,
731 }
732 }
733}
734
735impl Eq for Boolean {}
736
737impl From<AllocatedBit> for Boolean {
738 fn from(b: AllocatedBit) -> Boolean {
739 Boolean::Is(b)
740 }
741}
742
743impl<ConstraintF: Field> AllocGadget<bool, ConstraintF> for Boolean {
744 fn alloc_constant<T, CS: ConstraintSystem<ConstraintF>>(
745 _cs: CS,
746 t: T,
747 ) -> Result<Self, SynthesisError>
748 where
749 T: Borrow<bool>,
750 {
751 Ok(Boolean::constant(*t.borrow()))
752 }
753
754 fn alloc<F, T, CS: ConstraintSystem<ConstraintF>>(
755 cs: CS,
756 value_gen: F,
757 ) -> Result<Self, SynthesisError>
758 where
759 F: FnOnce() -> Result<T, SynthesisError>,
760 T: Borrow<bool>,
761 {
762 AllocatedBit::alloc(cs, value_gen).map(Boolean::from)
763 }
764
765 fn alloc_input<F, T, CS: ConstraintSystem<ConstraintF>>(
766 cs: CS,
767 value_gen: F,
768 ) -> Result<Self, SynthesisError>
769 where
770 F: FnOnce() -> Result<T, SynthesisError>,
771 T: Borrow<bool>,
772 {
773 AllocatedBit::alloc_input(cs, value_gen).map(Boolean::from)
774 }
775}
776
777impl<ConstraintF: Field> EqGadget<ConstraintF> for Boolean {}
778
779impl<ConstraintF: Field> ConditionalEqGadget<ConstraintF> for Boolean {
780 fn conditional_enforce_equal<CS>(
781 &self,
782 mut cs: CS,
783 other: &Self,
784 condition: &Boolean,
785 ) -> Result<(), SynthesisError>
786 where
787 CS: ConstraintSystem<ConstraintF>,
788 {
789 use self::Boolean::*;
790 let one = CS::one();
791 let difference: LinearCombination<ConstraintF> = match (self, other) {
792 // 1 - 1 = 0 - 0 = 0
793 (Constant(true), Constant(true)) | (Constant(false), Constant(false)) => return Ok(()),
794 // false != true
795 (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
796 // 1 - a
797 (Constant(true), Is(a)) | (Is(a), Constant(true)) => {
798 LinearCombination::zero() + one - a.get_variable()
799 }
800 // a - 0 = a
801 (Constant(false), Is(a)) | (Is(a), Constant(false)) => {
802 LinearCombination::zero() + a.get_variable()
803 }
804 // 1 - !a = 1 - (1 - a) = a
805 (Constant(true), Not(a)) | (Not(a), Constant(true)) => {
806 LinearCombination::zero() + a.get_variable()
807 }
808 // !a - 0 = !a = 1 - a
809 (Constant(false), Not(a)) | (Not(a), Constant(false)) => {
810 LinearCombination::zero() + one - a.get_variable()
811 }
812 // b - a,
813 (Is(a), Is(b)) => LinearCombination::zero() + b.get_variable() - a.get_variable(),
814 // !b - a = (1 - b) - a
815 (Is(a), Not(b)) | (Not(b), Is(a)) => {
816 LinearCombination::zero() + one - b.get_variable() - a.get_variable()
817 }
818 // !b - !a = (1 - b) - (1 - a) = a - b,
819 (Not(a), Not(b)) => LinearCombination::zero() + a.get_variable() - b.get_variable(),
820 };
821
822 if let Constant(false) = condition {
823 Ok(())
824 } else {
825 cs.enforce(
826 || "conditional_equals",
827 |lc| difference + &lc,
828 |lc| condition.lc(one, ConstraintF::one()) + &lc,
829 |lc| lc,
830 );
831 Ok(())
832 }
833 }
834
835 fn cost() -> usize {
836 1
837 }
838}
839
840impl<ConstraintF: Field> ToBytesGadget<ConstraintF> for Boolean {
841 /// Outputs `1u8` if `self` is true, and `0u8` otherwise.
842 fn to_bytes<CS: ConstraintSystem<ConstraintF>>(
843 &self,
844 _cs: CS,
845 ) -> Result<Vec<UInt8>, SynthesisError> {
846 let mut bits = vec![Boolean::constant(false); 7];
847 bits.push(*self);
848 bits.reverse();
849 let value = self.get_value().map(|val| val as u8);
850 let byte = UInt8 { bits, value };
851 Ok(vec![byte])
852 }
853}
854
855impl<ConstraintF: PrimeField> CondSelectGadget<ConstraintF> for Boolean {
856 fn conditionally_select<CS>(
857 mut cs: CS,
858 cond: &Self,
859 true_value: &Self,
860 false_value: &Self,
861 ) -> Result<Self, SynthesisError>
862 where
863 CS: ConstraintSystem<ConstraintF>,
864 {
865 match cond {
866 Boolean::Constant(true) => Ok(true_value.clone()),
867 Boolean::Constant(false) => Ok(false_value.clone()),
868 cond @ Boolean::Not(_) => {
869 Self::conditionally_select(cs, &cond.not(), false_value, true_value)
870 }
871 cond @ Boolean::Is(_) => match (true_value, false_value) {
872 (x, &Boolean::Constant(false)) => Boolean::and(cs.ns(|| "and"), cond, x).into(),
873 (&Boolean::Constant(false), x) => Boolean::and(cs.ns(|| "and"), &cond.not(), x),
874 (&Boolean::Constant(true), x) => Boolean::or(cs.ns(|| "or"), cond, x).into(),
875 (x, &Boolean::Constant(true)) => Boolean::or(cs.ns(|| "or"), &cond.not(), x),
876 (a @ Boolean::Is(_), b @ Boolean::Is(_))
877 | (a @ Boolean::Not(_), b @ Boolean::Not(_))
878 | (a @ Boolean::Is(_), b @ Boolean::Not(_))
879 | (a @ Boolean::Not(_), b @ Boolean::Is(_)) => {
880 let a_lc = a.lc(CS::one(), ConstraintF::one());
881 let b_lc = b.lc(CS::one(), ConstraintF::one());
882 Ok(
883 cond_select_helper(cs, cond, (a.get_value(), a_lc), (b.get_value(), b_lc))?
884 .into(),
885 )
886 }
887 },
888 }
889 }
890
891 fn cost() -> usize {
892 1
893 }
894}
895
896#[cfg(test)]
897mod test {
898 use super::{AllocatedBit, Boolean};
899 use crate::{prelude::*, test_constraint_system::TestConstraintSystem};
900 use algebra::{bls12_381::Fr, BitIterator, Field, One, PrimeField, UniformRand, Zero};
901 use core::str::FromStr;
902 use r1cs_core::ConstraintSystem;
903 use rand::SeedableRng;
904 use rand_xorshift::XorShiftRng;
905
906 #[test]
907 fn test_boolean_to_byte() {
908 for val in [true, false].iter() {
909 let mut cs = TestConstraintSystem::<Fr>::new();
910 let a: Boolean = AllocatedBit::alloc(&mut cs, || Ok(*val)).unwrap().into();
911 let bytes = a.to_bytes(&mut cs.ns(|| "ToBytes")).unwrap();
912 assert_eq!(bytes.len(), 1);
913 let byte = &bytes[0];
914 assert_eq!(byte.value.unwrap(), *val as u8);
915
916 for (i, bit_gadget) in byte.bits.iter().enumerate() {
917 assert_eq!(
918 bit_gadget.get_value().unwrap(),
919 (byte.value.unwrap() >> i) & 1 == 1
920 );
921 }
922 }
923 }
924
925 #[test]
926 fn test_allocated_bit() {
927 let mut cs = TestConstraintSystem::<Fr>::new();
928
929 AllocatedBit::alloc(&mut cs, || Ok(true)).unwrap();
930 assert!(cs.get("boolean") == Fr::one());
931 assert!(cs.is_satisfied());
932 cs.set("boolean", Fr::zero());
933 assert!(cs.is_satisfied());
934 cs.set("boolean", Fr::from_str("2").unwrap());
935 assert!(!cs.is_satisfied());
936 assert!(cs.which_is_unsatisfied() == Some("boolean constraint"));
937 }
938
939 #[test]
940 fn test_xor() {
941 for a_val in [false, true].iter() {
942 for b_val in [false, true].iter() {
943 let mut cs = TestConstraintSystem::<Fr>::new();
944 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
945 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
946 let c = AllocatedBit::xor(&mut cs, &a, &b).unwrap();
947 assert_eq!(c.value.unwrap(), *a_val ^ *b_val);
948
949 assert!(cs.is_satisfied());
950 }
951 }
952 }
953
954 #[test]
955 fn test_or() {
956 for a_val in [false, true].iter() {
957 for b_val in [false, true].iter() {
958 let mut cs = TestConstraintSystem::<Fr>::new();
959 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
960 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
961 let c = AllocatedBit::or(&mut cs, &a, &b).unwrap();
962 assert_eq!(c.value.unwrap(), *a_val | *b_val);
963
964 assert!(cs.is_satisfied());
965 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
966 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
967 }
968 }
969 }
970
971 #[test]
972 fn test_and() {
973 for a_val in [false, true].iter() {
974 for b_val in [false, true].iter() {
975 let mut cs = TestConstraintSystem::<Fr>::new();
976 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
977 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
978 let c = AllocatedBit::and(&mut cs, &a, &b).unwrap();
979 assert_eq!(c.value.unwrap(), *a_val & *b_val);
980
981 assert!(cs.is_satisfied());
982 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
983 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
984 assert!(
985 cs.get("and result")
986 == if *a_val & *b_val {
987 Fr::one()
988 } else {
989 Fr::zero()
990 }
991 );
992
993 // Invert the result and check if the constraint system is still satisfied
994 cs.set(
995 "and result",
996 if *a_val & *b_val {
997 Fr::zero()
998 } else {
999 Fr::one()
1000 },
1001 );
1002 assert!(!cs.is_satisfied());
1003 }
1004 }
1005 }
1006
1007 #[test]
1008 fn test_and_not() {
1009 for a_val in [false, true].iter() {
1010 for b_val in [false, true].iter() {
1011 let mut cs = TestConstraintSystem::<Fr>::new();
1012 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
1013 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
1014 let c = AllocatedBit::and_not(&mut cs, &a, &b).unwrap();
1015 assert_eq!(c.value.unwrap(), *a_val & !*b_val);
1016
1017 assert!(cs.is_satisfied());
1018 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
1019 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
1020 assert!(
1021 cs.get("and not result")
1022 == if *a_val & !*b_val {
1023 Fr::one()
1024 } else {
1025 Fr::zero()
1026 }
1027 );
1028
1029 // Invert the result and check if the constraint system is still satisfied
1030 cs.set(
1031 "and not result",
1032 if *a_val & !*b_val {
1033 Fr::zero()
1034 } else {
1035 Fr::one()
1036 },
1037 );
1038 assert!(!cs.is_satisfied());
1039 }
1040 }
1041 }
1042
1043 #[test]
1044 fn test_nor() {
1045 for a_val in [false, true].iter() {
1046 for b_val in [false, true].iter() {
1047 let mut cs = TestConstraintSystem::<Fr>::new();
1048 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
1049 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
1050 let c = AllocatedBit::nor(&mut cs, &a, &b).unwrap();
1051 assert_eq!(c.value.unwrap(), !*a_val & !*b_val);
1052
1053 assert!(cs.is_satisfied());
1054 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
1055 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
1056 assert!(
1057 cs.get("nor result")
1058 == if !*a_val & !*b_val {
1059 Fr::one()
1060 } else {
1061 Fr::zero()
1062 }
1063 );
1064
1065 // Invert the result and check if the constraint system is still satisfied
1066 cs.set(
1067 "nor result",
1068 if !*a_val & !*b_val {
1069 Fr::zero()
1070 } else {
1071 Fr::one()
1072 },
1073 );
1074 assert!(!cs.is_satisfied());
1075 }
1076 }
1077 }
1078
1079 #[test]
1080 fn test_enforce_equal() {
1081 for a_bool in [false, true].iter().cloned() {
1082 for b_bool in [false, true].iter().cloned() {
1083 for a_neg in [false, true].iter().cloned() {
1084 for b_neg in [false, true].iter().cloned() {
1085 let mut cs = TestConstraintSystem::<Fr>::new();
1086
1087 let mut a: Boolean = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(a_bool))
1088 .unwrap()
1089 .into();
1090 let mut b: Boolean = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(b_bool))
1091 .unwrap()
1092 .into();
1093
1094 if a_neg {
1095 a = a.not();
1096 }
1097 if b_neg {
1098 b = b.not();
1099 }
1100
1101 a.enforce_equal(&mut cs, &b).unwrap();
1102
1103 assert_eq!(cs.is_satisfied(), (a_bool ^ a_neg) == (b_bool ^ b_neg));
1104 }
1105 }
1106 }
1107 }
1108 }
1109
1110 #[test]
1111 fn test_conditional_enforce_equal() {
1112 for a_bool in [false, true].iter().cloned() {
1113 for b_bool in [false, true].iter().cloned() {
1114 for a_neg in [false, true].iter().cloned() {
1115 for b_neg in [false, true].iter().cloned() {
1116 let mut cs = TestConstraintSystem::<Fr>::new();
1117
1118 // First test if constraint system is satisfied
1119 // when we do want to enforce the condition.
1120 let mut a: Boolean = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(a_bool))
1121 .unwrap()
1122 .into();
1123 let mut b: Boolean = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(b_bool))
1124 .unwrap()
1125 .into();
1126
1127 if a_neg {
1128 a = a.not();
1129 }
1130 if b_neg {
1131 b = b.not();
1132 }
1133
1134 a.conditional_enforce_equal(&mut cs, &b, &Boolean::constant(true))
1135 .unwrap();
1136
1137 assert_eq!(cs.is_satisfied(), (a_bool ^ a_neg) == (b_bool ^ b_neg));
1138
1139 // Now test if constraint system is satisfied even
1140 // when we don't want to enforce the condition.
1141 let mut cs = TestConstraintSystem::<Fr>::new();
1142
1143 let mut a: Boolean = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(a_bool))
1144 .unwrap()
1145 .into();
1146 let mut b: Boolean = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(b_bool))
1147 .unwrap()
1148 .into();
1149
1150 if a_neg {
1151 a = a.not();
1152 }
1153 if b_neg {
1154 b = b.not();
1155 }
1156
1157 let false_cond = AllocatedBit::alloc(cs.ns(|| "cond"), || Ok(false))
1158 .unwrap()
1159 .into();
1160 a.conditional_enforce_equal(&mut cs, &b, &false_cond)
1161 .unwrap();
1162
1163 assert!(cs.is_satisfied());
1164 }
1165 }
1166 }
1167 }
1168 }
1169
1170 #[test]
1171 fn test_boolean_negation() {
1172 let mut cs = TestConstraintSystem::<Fr>::new();
1173
1174 let mut b = Boolean::from(AllocatedBit::alloc(&mut cs, || Ok(true)).unwrap());
1175
1176 match b {
1177 Boolean::Is(_) => {}
1178 _ => panic!("unexpected value"),
1179 }
1180
1181 b = b.not();
1182
1183 match b {
1184 Boolean::Not(_) => {}
1185 _ => panic!("unexpected value"),
1186 }
1187
1188 b = b.not();
1189
1190 match b {
1191 Boolean::Is(_) => {}
1192 _ => panic!("unexpected value"),
1193 }
1194
1195 b = Boolean::constant(true);
1196
1197 match b {
1198 Boolean::Constant(true) => {}
1199 _ => panic!("unexpected value"),
1200 }
1201
1202 b = b.not();
1203
1204 match b {
1205 Boolean::Constant(false) => {}
1206 _ => panic!("unexpected value"),
1207 }
1208
1209 b = b.not();
1210
1211 match b {
1212 Boolean::Constant(true) => {}
1213 _ => panic!("unexpected value"),
1214 }
1215 }
1216
1217 #[derive(Copy, Clone, Debug)]
1218 enum OperandType {
1219 True,
1220 False,
1221 AllocatedTrue,
1222 AllocatedFalse,
1223 NegatedAllocatedTrue,
1224 NegatedAllocatedFalse,
1225 }
1226
1227 #[test]
1228 fn test_boolean_xor() {
1229 let variants = [
1230 OperandType::True,
1231 OperandType::False,
1232 OperandType::AllocatedTrue,
1233 OperandType::AllocatedFalse,
1234 OperandType::NegatedAllocatedTrue,
1235 OperandType::NegatedAllocatedFalse,
1236 ];
1237
1238 for first_operand in variants.iter().cloned() {
1239 for second_operand in variants.iter().cloned() {
1240 let mut cs = TestConstraintSystem::<Fr>::new();
1241
1242 let a;
1243 let b;
1244
1245 {
1246 let mut dyn_construct = |operand, name| {
1247 let cs = cs.ns(|| name);
1248
1249 match operand {
1250 OperandType::True => Boolean::constant(true),
1251 OperandType::False => Boolean::constant(false),
1252 OperandType::AllocatedTrue => {
1253 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1254 }
1255 OperandType::AllocatedFalse => {
1256 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1257 }
1258 OperandType::NegatedAllocatedTrue => {
1259 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap()).not()
1260 }
1261 OperandType::NegatedAllocatedFalse => {
1262 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap()).not()
1263 }
1264 }
1265 };
1266
1267 a = dyn_construct(first_operand, "a");
1268 b = dyn_construct(second_operand, "b");
1269 }
1270
1271 let c = Boolean::xor(&mut cs, &a, &b).unwrap();
1272
1273 assert!(cs.is_satisfied());
1274
1275 match (first_operand, second_operand, c) {
1276 (OperandType::True, OperandType::True, Boolean::Constant(false)) => {}
1277 (OperandType::True, OperandType::False, Boolean::Constant(true)) => {}
1278 (OperandType::True, OperandType::AllocatedTrue, Boolean::Not(_)) => {}
1279 (OperandType::True, OperandType::AllocatedFalse, Boolean::Not(_)) => {}
1280 (OperandType::True, OperandType::NegatedAllocatedTrue, Boolean::Is(_)) => {}
1281 (OperandType::True, OperandType::NegatedAllocatedFalse, Boolean::Is(_)) => {}
1282
1283 (OperandType::False, OperandType::True, Boolean::Constant(true)) => {}
1284 (OperandType::False, OperandType::False, Boolean::Constant(false)) => {}
1285 (OperandType::False, OperandType::AllocatedTrue, Boolean::Is(_)) => {}
1286 (OperandType::False, OperandType::AllocatedFalse, Boolean::Is(_)) => {}
1287 (OperandType::False, OperandType::NegatedAllocatedTrue, Boolean::Not(_)) => {}
1288 (OperandType::False, OperandType::NegatedAllocatedFalse, Boolean::Not(_)) => {}
1289
1290 (OperandType::AllocatedTrue, OperandType::True, Boolean::Not(_)) => {}
1291 (OperandType::AllocatedTrue, OperandType::False, Boolean::Is(_)) => {}
1292 (
1293 OperandType::AllocatedTrue,
1294 OperandType::AllocatedTrue,
1295 Boolean::Is(ref v),
1296 ) => {
1297 assert!(cs.get("xor result") == Fr::zero());
1298 assert_eq!(v.value, Some(false));
1299 }
1300 (
1301 OperandType::AllocatedTrue,
1302 OperandType::AllocatedFalse,
1303 Boolean::Is(ref v),
1304 ) => {
1305 assert!(cs.get("xor result") == Fr::one());
1306 assert_eq!(v.value, Some(true));
1307 }
1308 (
1309 OperandType::AllocatedTrue,
1310 OperandType::NegatedAllocatedTrue,
1311 Boolean::Not(ref v),
1312 ) => {
1313 assert!(cs.get("xor result") == Fr::zero());
1314 assert_eq!(v.value, Some(false));
1315 }
1316 (
1317 OperandType::AllocatedTrue,
1318 OperandType::NegatedAllocatedFalse,
1319 Boolean::Not(ref v),
1320 ) => {
1321 assert!(cs.get("xor result") == Fr::one());
1322 assert_eq!(v.value, Some(true));
1323 }
1324
1325 (OperandType::AllocatedFalse, OperandType::True, Boolean::Not(_)) => {}
1326 (OperandType::AllocatedFalse, OperandType::False, Boolean::Is(_)) => {}
1327 (
1328 OperandType::AllocatedFalse,
1329 OperandType::AllocatedTrue,
1330 Boolean::Is(ref v),
1331 ) => {
1332 assert!(cs.get("xor result") == Fr::one());
1333 assert_eq!(v.value, Some(true));
1334 }
1335 (
1336 OperandType::AllocatedFalse,
1337 OperandType::AllocatedFalse,
1338 Boolean::Is(ref v),
1339 ) => {
1340 assert!(cs.get("xor result") == Fr::zero());
1341 assert_eq!(v.value, Some(false));
1342 }
1343 (
1344 OperandType::AllocatedFalse,
1345 OperandType::NegatedAllocatedTrue,
1346 Boolean::Not(ref v),
1347 ) => {
1348 assert!(cs.get("xor result") == Fr::one());
1349 assert_eq!(v.value, Some(true));
1350 }
1351 (
1352 OperandType::AllocatedFalse,
1353 OperandType::NegatedAllocatedFalse,
1354 Boolean::Not(ref v),
1355 ) => {
1356 assert!(cs.get("xor result") == Fr::zero());
1357 assert_eq!(v.value, Some(false));
1358 }
1359
1360 (OperandType::NegatedAllocatedTrue, OperandType::True, Boolean::Is(_)) => {}
1361 (OperandType::NegatedAllocatedTrue, OperandType::False, Boolean::Not(_)) => {}
1362 (
1363 OperandType::NegatedAllocatedTrue,
1364 OperandType::AllocatedTrue,
1365 Boolean::Not(ref v),
1366 ) => {
1367 assert!(cs.get("xor result") == Fr::zero());
1368 assert_eq!(v.value, Some(false));
1369 }
1370 (
1371 OperandType::NegatedAllocatedTrue,
1372 OperandType::AllocatedFalse,
1373 Boolean::Not(ref v),
1374 ) => {
1375 assert!(cs.get("xor result") == Fr::one());
1376 assert_eq!(v.value, Some(true));
1377 }
1378 (
1379 OperandType::NegatedAllocatedTrue,
1380 OperandType::NegatedAllocatedTrue,
1381 Boolean::Is(ref v),
1382 ) => {
1383 assert!(cs.get("xor result") == Fr::zero());
1384 assert_eq!(v.value, Some(false));
1385 }
1386 (
1387 OperandType::NegatedAllocatedTrue,
1388 OperandType::NegatedAllocatedFalse,
1389 Boolean::Is(ref v),
1390 ) => {
1391 assert!(cs.get("xor result") == Fr::one());
1392 assert_eq!(v.value, Some(true));
1393 }
1394
1395 (OperandType::NegatedAllocatedFalse, OperandType::True, Boolean::Is(_)) => {}
1396 (OperandType::NegatedAllocatedFalse, OperandType::False, Boolean::Not(_)) => {}
1397 (
1398 OperandType::NegatedAllocatedFalse,
1399 OperandType::AllocatedTrue,
1400 Boolean::Not(ref v),
1401 ) => {
1402 assert!(cs.get("xor result") == Fr::one());
1403 assert_eq!(v.value, Some(true));
1404 }
1405 (
1406 OperandType::NegatedAllocatedFalse,
1407 OperandType::AllocatedFalse,
1408 Boolean::Not(ref v),
1409 ) => {
1410 assert!(cs.get("xor result") == Fr::zero());
1411 assert_eq!(v.value, Some(false));
1412 }
1413 (
1414 OperandType::NegatedAllocatedFalse,
1415 OperandType::NegatedAllocatedTrue,
1416 Boolean::Is(ref v),
1417 ) => {
1418 assert!(cs.get("xor result") == Fr::one());
1419 assert_eq!(v.value, Some(true));
1420 }
1421 (
1422 OperandType::NegatedAllocatedFalse,
1423 OperandType::NegatedAllocatedFalse,
1424 Boolean::Is(ref v),
1425 ) => {
1426 assert!(cs.get("xor result") == Fr::zero());
1427 assert_eq!(v.value, Some(false));
1428 }
1429
1430 _ => panic!("this should never be encountered"),
1431 }
1432 }
1433 }
1434 }
1435
1436 #[test]
1437 fn test_boolean_cond_select() {
1438 let variants = [
1439 OperandType::True,
1440 OperandType::False,
1441 OperandType::AllocatedTrue,
1442 OperandType::AllocatedFalse,
1443 OperandType::NegatedAllocatedTrue,
1444 OperandType::NegatedAllocatedFalse,
1445 ];
1446
1447 for condition in variants.iter().cloned() {
1448 for first_operand in variants.iter().cloned() {
1449 for second_operand in variants.iter().cloned() {
1450 let mut cs = TestConstraintSystem::<Fr>::new();
1451
1452 let cond;
1453 let a;
1454 let b;
1455
1456 {
1457 let mut dyn_construct = |operand, name| {
1458 let cs = cs.ns(|| name);
1459
1460 match operand {
1461 OperandType::True => Boolean::constant(true),
1462 OperandType::False => Boolean::constant(false),
1463 OperandType::AllocatedTrue => {
1464 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1465 }
1466 OperandType::AllocatedFalse => {
1467 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1468 }
1469 OperandType::NegatedAllocatedTrue => {
1470 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1471 .not()
1472 }
1473 OperandType::NegatedAllocatedFalse => {
1474 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1475 .not()
1476 }
1477 }
1478 };
1479
1480 cond = dyn_construct(condition, "cond");
1481 a = dyn_construct(first_operand, "a");
1482 b = dyn_construct(second_operand, "b");
1483 }
1484
1485 let before = cs.num_constraints();
1486 let c = Boolean::conditionally_select(&mut cs, &cond, &a, &b).unwrap();
1487 let after = cs.num_constraints();
1488
1489 assert!(
1490 cs.is_satisfied(),
1491 "failed with operands: cond: {:?}, a: {:?}, b: {:?}",
1492 condition,
1493 first_operand,
1494 second_operand,
1495 );
1496 assert_eq!(
1497 c.get_value(),
1498 if cond.get_value().unwrap() {
1499 a.get_value()
1500 } else {
1501 b.get_value()
1502 }
1503 );
1504 assert!(<Boolean as CondSelectGadget<Fr>>::cost() >= after - before);
1505 }
1506 }
1507 }
1508 }
1509
1510 #[test]
1511 fn test_boolean_or() {
1512 let variants = [
1513 OperandType::True,
1514 OperandType::False,
1515 OperandType::AllocatedTrue,
1516 OperandType::AllocatedFalse,
1517 OperandType::NegatedAllocatedTrue,
1518 OperandType::NegatedAllocatedFalse,
1519 ];
1520
1521 for first_operand in variants.iter().cloned() {
1522 for second_operand in variants.iter().cloned() {
1523 let mut cs = TestConstraintSystem::<Fr>::new();
1524
1525 let a;
1526 let b;
1527
1528 {
1529 let mut dyn_construct = |operand, name| {
1530 let cs = cs.ns(|| name);
1531
1532 match operand {
1533 OperandType::True => Boolean::constant(true),
1534 OperandType::False => Boolean::constant(false),
1535 OperandType::AllocatedTrue => {
1536 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1537 }
1538 OperandType::AllocatedFalse => {
1539 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1540 }
1541 OperandType::NegatedAllocatedTrue => {
1542 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap()).not()
1543 }
1544 OperandType::NegatedAllocatedFalse => {
1545 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap()).not()
1546 }
1547 }
1548 };
1549
1550 a = dyn_construct(first_operand, "a");
1551 b = dyn_construct(second_operand, "b");
1552 }
1553
1554 let c = Boolean::or(&mut cs, &a, &b).unwrap();
1555
1556 assert!(cs.is_satisfied());
1557
1558 match (first_operand, second_operand, c) {
1559 (OperandType::True, OperandType::True, Boolean::Constant(true)) => {}
1560 (OperandType::True, OperandType::False, Boolean::Constant(true)) => {}
1561 (OperandType::True, OperandType::AllocatedTrue, Boolean::Constant(true)) => {}
1562 (OperandType::True, OperandType::AllocatedFalse, Boolean::Constant(true)) => {}
1563 (
1564 OperandType::True,
1565 OperandType::NegatedAllocatedTrue,
1566 Boolean::Constant(true),
1567 ) => {}
1568 (
1569 OperandType::True,
1570 OperandType::NegatedAllocatedFalse,
1571 Boolean::Constant(true),
1572 ) => {}
1573
1574 (OperandType::False, OperandType::True, Boolean::Constant(true)) => {}
1575 (OperandType::False, OperandType::False, Boolean::Constant(false)) => {}
1576 (OperandType::False, OperandType::AllocatedTrue, Boolean::Is(_)) => {}
1577 (OperandType::False, OperandType::AllocatedFalse, Boolean::Is(_)) => {}
1578 (OperandType::False, OperandType::NegatedAllocatedTrue, Boolean::Not(_)) => {}
1579 (OperandType::False, OperandType::NegatedAllocatedFalse, Boolean::Not(_)) => {}
1580
1581 (OperandType::AllocatedTrue, OperandType::True, Boolean::Constant(true)) => {}
1582 (OperandType::AllocatedTrue, OperandType::False, Boolean::Is(_)) => {}
1583 (
1584 OperandType::AllocatedTrue,
1585 OperandType::AllocatedTrue,
1586 Boolean::Is(ref v),
1587 ) => {
1588 assert_eq!(v.value, Some(true));
1589 }
1590 (
1591 OperandType::AllocatedTrue,
1592 OperandType::AllocatedFalse,
1593 Boolean::Is(ref v),
1594 ) => {
1595 assert_eq!(v.value, Some(true));
1596 }
1597 (
1598 OperandType::AllocatedTrue,
1599 OperandType::NegatedAllocatedTrue,
1600 Boolean::Not(ref v),
1601 ) => {
1602 assert_eq!(v.value, Some(false));
1603 }
1604 (
1605 OperandType::AllocatedTrue,
1606 OperandType::NegatedAllocatedFalse,
1607 Boolean::Not(ref v),
1608 ) => {
1609 assert_eq!(v.value, Some(false));
1610 }
1611
1612 (OperandType::AllocatedFalse, OperandType::True, Boolean::Constant(true)) => {}
1613 (OperandType::AllocatedFalse, OperandType::False, Boolean::Is(_)) => {}
1614 (
1615 OperandType::AllocatedFalse,
1616 OperandType::AllocatedTrue,
1617 Boolean::Is(ref v),
1618 ) => {
1619 assert_eq!(v.value, Some(true));
1620 }
1621 (
1622 OperandType::AllocatedFalse,
1623 OperandType::AllocatedFalse,
1624 Boolean::Is(ref v),
1625 ) => {
1626 assert_eq!(v.value, Some(false));
1627 }
1628 (
1629 OperandType::AllocatedFalse,
1630 OperandType::NegatedAllocatedTrue,
1631 Boolean::Not(ref v),
1632 ) => {
1633 assert_eq!(v.value, Some(true));
1634 }
1635 (
1636 OperandType::AllocatedFalse,
1637 OperandType::NegatedAllocatedFalse,
1638 Boolean::Not(ref v),
1639 ) => {
1640 assert_eq!(v.value, Some(false));
1641 }
1642
1643 (
1644 OperandType::NegatedAllocatedTrue,
1645 OperandType::True,
1646 Boolean::Constant(true),
1647 ) => {}
1648 (OperandType::NegatedAllocatedTrue, OperandType::False, Boolean::Not(_)) => {}
1649 (
1650 OperandType::NegatedAllocatedTrue,
1651 OperandType::AllocatedTrue,
1652 Boolean::Not(ref v),
1653 ) => {
1654 assert_eq!(v.value, Some(false));
1655 }
1656 (
1657 OperandType::NegatedAllocatedTrue,
1658 OperandType::AllocatedFalse,
1659 Boolean::Not(ref v),
1660 ) => {
1661 assert_eq!(v.value, Some(true));
1662 }
1663 (
1664 OperandType::NegatedAllocatedTrue,
1665 OperandType::NegatedAllocatedTrue,
1666 Boolean::Not(ref v),
1667 ) => {
1668 assert_eq!(v.value, Some(true));
1669 }
1670 (
1671 OperandType::NegatedAllocatedTrue,
1672 OperandType::NegatedAllocatedFalse,
1673 Boolean::Not(ref v),
1674 ) => {
1675 assert_eq!(v.value, Some(false));
1676 }
1677
1678 (
1679 OperandType::NegatedAllocatedFalse,
1680 OperandType::True,
1681 Boolean::Constant(true),
1682 ) => {}
1683 (OperandType::NegatedAllocatedFalse, OperandType::False, Boolean::Not(_)) => {}
1684 (
1685 OperandType::NegatedAllocatedFalse,
1686 OperandType::AllocatedTrue,
1687 Boolean::Not(ref v),
1688 ) => {
1689 assert_eq!(v.value, Some(false));
1690 }
1691 (
1692 OperandType::NegatedAllocatedFalse,
1693 OperandType::AllocatedFalse,
1694 Boolean::Not(ref v),
1695 ) => {
1696 assert_eq!(v.value, Some(false));
1697 }
1698 (
1699 OperandType::NegatedAllocatedFalse,
1700 OperandType::NegatedAllocatedTrue,
1701 Boolean::Not(ref v),
1702 ) => {
1703 assert_eq!(v.value, Some(false));
1704 }
1705 (
1706 OperandType::NegatedAllocatedFalse,
1707 OperandType::NegatedAllocatedFalse,
1708 Boolean::Not(ref v),
1709 ) => {
1710 assert_eq!(v.value, Some(false));
1711 }
1712
1713 _ => panic!(
1714 "this should never be encountered, in case: (a = {:?}, b = {:?}, c = {:?})",
1715 a, b, c
1716 ),
1717 }
1718 }
1719 }
1720 }
1721
1722 #[test]
1723 fn test_boolean_and() {
1724 let variants = [
1725 OperandType::True,
1726 OperandType::False,
1727 OperandType::AllocatedTrue,
1728 OperandType::AllocatedFalse,
1729 OperandType::NegatedAllocatedTrue,
1730 OperandType::NegatedAllocatedFalse,
1731 ];
1732
1733 for first_operand in variants.iter().cloned() {
1734 for second_operand in variants.iter().cloned() {
1735 let mut cs = TestConstraintSystem::<Fr>::new();
1736
1737 let a;
1738 let b;
1739
1740 {
1741 let mut dyn_construct = |operand, name| {
1742 let cs = cs.ns(|| name);
1743
1744 match operand {
1745 OperandType::True => Boolean::constant(true),
1746 OperandType::False => Boolean::constant(false),
1747 OperandType::AllocatedTrue => {
1748 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1749 }
1750 OperandType::AllocatedFalse => {
1751 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1752 }
1753 OperandType::NegatedAllocatedTrue => {
1754 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap()).not()
1755 }
1756 OperandType::NegatedAllocatedFalse => {
1757 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap()).not()
1758 }
1759 }
1760 };
1761
1762 a = dyn_construct(first_operand, "a");
1763 b = dyn_construct(second_operand, "b");
1764 }
1765
1766 let c = Boolean::and(&mut cs, &a, &b).unwrap();
1767
1768 assert!(cs.is_satisfied());
1769
1770 match (first_operand, second_operand, c) {
1771 (OperandType::True, OperandType::True, Boolean::Constant(true)) => {}
1772 (OperandType::True, OperandType::False, Boolean::Constant(false)) => {}
1773 (OperandType::True, OperandType::AllocatedTrue, Boolean::Is(_)) => {}
1774 (OperandType::True, OperandType::AllocatedFalse, Boolean::Is(_)) => {}
1775 (OperandType::True, OperandType::NegatedAllocatedTrue, Boolean::Not(_)) => {}
1776 (OperandType::True, OperandType::NegatedAllocatedFalse, Boolean::Not(_)) => {}
1777
1778 (OperandType::False, OperandType::True, Boolean::Constant(false)) => {}
1779 (OperandType::False, OperandType::False, Boolean::Constant(false)) => {}
1780 (OperandType::False, OperandType::AllocatedTrue, Boolean::Constant(false)) => {}
1781 (OperandType::False, OperandType::AllocatedFalse, Boolean::Constant(false)) => {
1782 }
1783 (
1784 OperandType::False,
1785 OperandType::NegatedAllocatedTrue,
1786 Boolean::Constant(false),
1787 ) => {}
1788 (
1789 OperandType::False,
1790 OperandType::NegatedAllocatedFalse,
1791 Boolean::Constant(false),
1792 ) => {}
1793
1794 (OperandType::AllocatedTrue, OperandType::True, Boolean::Is(_)) => {}
1795 (OperandType::AllocatedTrue, OperandType::False, Boolean::Constant(false)) => {}
1796 (
1797 OperandType::AllocatedTrue,
1798 OperandType::AllocatedTrue,
1799 Boolean::Is(ref v),
1800 ) => {
1801 assert!(cs.get("and result") == Fr::one());
1802 assert_eq!(v.value, Some(true));
1803 }
1804 (
1805 OperandType::AllocatedTrue,
1806 OperandType::AllocatedFalse,
1807 Boolean::Is(ref v),
1808 ) => {
1809 assert!(cs.get("and result") == Fr::zero());
1810 assert_eq!(v.value, Some(false));
1811 }
1812 (
1813 OperandType::AllocatedTrue,
1814 OperandType::NegatedAllocatedTrue,
1815 Boolean::Is(ref v),
1816 ) => {
1817 assert!(cs.get("and not result") == Fr::zero());
1818 assert_eq!(v.value, Some(false));
1819 }
1820 (
1821 OperandType::AllocatedTrue,
1822 OperandType::NegatedAllocatedFalse,
1823 Boolean::Is(ref v),
1824 ) => {
1825 assert!(cs.get("and not result") == Fr::one());
1826 assert_eq!(v.value, Some(true));
1827 }
1828
1829 (OperandType::AllocatedFalse, OperandType::True, Boolean::Is(_)) => {}
1830 (OperandType::AllocatedFalse, OperandType::False, Boolean::Constant(false)) => {
1831 }
1832 (
1833 OperandType::AllocatedFalse,
1834 OperandType::AllocatedTrue,
1835 Boolean::Is(ref v),
1836 ) => {
1837 assert!(cs.get("and result") == Fr::zero());
1838 assert_eq!(v.value, Some(false));
1839 }
1840 (
1841 OperandType::AllocatedFalse,
1842 OperandType::AllocatedFalse,
1843 Boolean::Is(ref v),
1844 ) => {
1845 assert!(cs.get("and result") == Fr::zero());
1846 assert_eq!(v.value, Some(false));
1847 }
1848 (
1849 OperandType::AllocatedFalse,
1850 OperandType::NegatedAllocatedTrue,
1851 Boolean::Is(ref v),
1852 ) => {
1853 assert!(cs.get("and not result") == Fr::zero());
1854 assert_eq!(v.value, Some(false));
1855 }
1856 (
1857 OperandType::AllocatedFalse,
1858 OperandType::NegatedAllocatedFalse,
1859 Boolean::Is(ref v),
1860 ) => {
1861 assert!(cs.get("and not result") == Fr::zero());
1862 assert_eq!(v.value, Some(false));
1863 }
1864
1865 (OperandType::NegatedAllocatedTrue, OperandType::True, Boolean::Not(_)) => {}
1866 (
1867 OperandType::NegatedAllocatedTrue,
1868 OperandType::False,
1869 Boolean::Constant(false),
1870 ) => {}
1871 (
1872 OperandType::NegatedAllocatedTrue,
1873 OperandType::AllocatedTrue,
1874 Boolean::Is(ref v),
1875 ) => {
1876 assert!(cs.get("and not result") == Fr::zero());
1877 assert_eq!(v.value, Some(false));
1878 }
1879 (
1880 OperandType::NegatedAllocatedTrue,
1881 OperandType::AllocatedFalse,
1882 Boolean::Is(ref v),
1883 ) => {
1884 assert!(cs.get("and not result") == Fr::zero());
1885 assert_eq!(v.value, Some(false));
1886 }
1887 (
1888 OperandType::NegatedAllocatedTrue,
1889 OperandType::NegatedAllocatedTrue,
1890 Boolean::Is(ref v),
1891 ) => {
1892 assert!(cs.get("nor result") == Fr::zero());
1893 assert_eq!(v.value, Some(false));
1894 }
1895 (
1896 OperandType::NegatedAllocatedTrue,
1897 OperandType::NegatedAllocatedFalse,
1898 Boolean::Is(ref v),
1899 ) => {
1900 assert!(cs.get("nor result") == Fr::zero());
1901 assert_eq!(v.value, Some(false));
1902 }
1903
1904 (OperandType::NegatedAllocatedFalse, OperandType::True, Boolean::Not(_)) => {}
1905 (
1906 OperandType::NegatedAllocatedFalse,
1907 OperandType::False,
1908 Boolean::Constant(false),
1909 ) => {}
1910 (
1911 OperandType::NegatedAllocatedFalse,
1912 OperandType::AllocatedTrue,
1913 Boolean::Is(ref v),
1914 ) => {
1915 assert!(cs.get("and not result") == Fr::one());
1916 assert_eq!(v.value, Some(true));
1917 }
1918 (
1919 OperandType::NegatedAllocatedFalse,
1920 OperandType::AllocatedFalse,
1921 Boolean::Is(ref v),
1922 ) => {
1923 assert!(cs.get("and not result") == Fr::zero());
1924 assert_eq!(v.value, Some(false));
1925 }
1926 (
1927 OperandType::NegatedAllocatedFalse,
1928 OperandType::NegatedAllocatedTrue,
1929 Boolean::Is(ref v),
1930 ) => {
1931 assert!(cs.get("nor result") == Fr::zero());
1932 assert_eq!(v.value, Some(false));
1933 }
1934 (
1935 OperandType::NegatedAllocatedFalse,
1936 OperandType::NegatedAllocatedFalse,
1937 Boolean::Is(ref v),
1938 ) => {
1939 assert!(cs.get("nor result") == Fr::one());
1940 assert_eq!(v.value, Some(true));
1941 }
1942
1943 _ => {
1944 panic!(
1945 "unexpected behavior at {:?} AND {:?}",
1946 first_operand, second_operand
1947 );
1948 }
1949 }
1950 }
1951 }
1952 }
1953
1954 #[test]
1955 fn test_enforce_in_field() {
1956 {
1957 let mut cs = TestConstraintSystem::<Fr>::new();
1958
1959 let mut bits = vec![];
1960 for (i, b) in BitIterator::new(Fr::characteristic()).skip(1).enumerate() {
1961 bits.push(Boolean::from(
1962 AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}", i)), || Ok(b)).unwrap(),
1963 ));
1964 }
1965
1966 Boolean::enforce_in_field::<_, _, Fr>(&mut cs, &bits).unwrap();
1967
1968 assert!(!cs.is_satisfied());
1969 }
1970
1971 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1972
1973 for _ in 0..1000 {
1974 let r = Fr::rand(&mut rng);
1975 let mut cs = TestConstraintSystem::<Fr>::new();
1976
1977 let mut bits = vec![];
1978 for (i, b) in BitIterator::new(r.into_repr()).skip(1).enumerate() {
1979 bits.push(Boolean::from(
1980 AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}", i)), || Ok(b)).unwrap(),
1981 ));
1982 }
1983
1984 Boolean::enforce_in_field::<_, _, Fr>(&mut cs, &bits).unwrap();
1985
1986 assert!(cs.is_satisfied());
1987 }
1988 }
1989
1990 #[test]
1991 fn test_enforce_nand() {
1992 {
1993 let mut cs = TestConstraintSystem::<Fr>::new();
1994
1995 assert!(Boolean::enforce_nand(&mut cs, &[Boolean::constant(false)]).is_ok());
1996 assert!(Boolean::enforce_nand(&mut cs, &[Boolean::constant(true)]).is_err());
1997 }
1998
1999 for i in 1..5 {
2000 // with every possible assignment for them
2001 for mut b in 0..(1 << i) {
2002 // with every possible negation
2003 for mut n in 0..(1 << i) {
2004 let mut cs = TestConstraintSystem::<Fr>::new();
2005
2006 let mut expected = true;
2007
2008 let mut bits = vec![];
2009 for j in 0..i {
2010 expected &= b & 1 == 1;
2011
2012 if n & 1 == 1 {
2013 bits.push(Boolean::from(
2014 AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}", j)), || {
2015 Ok(b & 1 == 1)
2016 })
2017 .unwrap(),
2018 ));
2019 } else {
2020 bits.push(
2021 Boolean::from(
2022 AllocatedBit::alloc(
2023 cs.ns(|| format!("bit_gadget {}", j)),
2024 || Ok(b & 1 == 0),
2025 )
2026 .unwrap(),
2027 )
2028 .not(),
2029 );
2030 }
2031
2032 b >>= 1;
2033 n >>= 1;
2034 }
2035
2036 let expected = !expected;
2037
2038 Boolean::enforce_nand(&mut cs, &bits).unwrap();
2039
2040 if expected {
2041 assert!(cs.is_satisfied());
2042 } else {
2043 assert!(!cs.is_satisfied());
2044 }
2045 }
2046 }
2047 }
2048 }
2049
2050 #[test]
2051 fn test_kary_and() {
2052 // test different numbers of operands
2053 for i in 1..15 {
2054 // with every possible assignment for them
2055 for mut b in 0..(1 << i) {
2056 let mut cs = TestConstraintSystem::<Fr>::new();
2057
2058 let mut expected = true;
2059
2060 let mut bits = vec![];
2061 for j in 0..i {
2062 expected &= b & 1 == 1;
2063
2064 bits.push(Boolean::from(
2065 AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}", j)), || {
2066 Ok(b & 1 == 1)
2067 })
2068 .unwrap(),
2069 ));
2070 b >>= 1;
2071 }
2072
2073 let r = Boolean::kary_and(&mut cs, &bits).unwrap();
2074
2075 assert!(cs.is_satisfied());
2076
2077 match r {
2078 Boolean::Is(ref r) => {
2079 assert_eq!(r.value.unwrap(), expected);
2080 }
2081 _ => unreachable!(),
2082 }
2083 }
2084 }
2085 }
2086}