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