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(_) => Self::conditionally_select(cs, &cond.not(), false_value, true_value),
840 cond @ Boolean::Is(_) => match (true_value, false_value) {
841 (x, &Boolean::Constant(false)) => Boolean::and(cs.ns(|| "and"), cond, x).into(),
842 (&Boolean::Constant(false), x) => Boolean::and(cs.ns(|| "and"), &cond.not(), x),
843 (&Boolean::Constant(true), x) => Boolean::or(cs.ns(|| "or"), cond, x).into(),
844 (x, &Boolean::Constant(true)) => Boolean::or(cs.ns(|| "or"), &cond.not(), x),
845 (a @ Boolean::Is(_), b @ Boolean::Is(_))
846 | (a @ Boolean::Not(_), b @ Boolean::Not(_))
847 | (a @ Boolean::Is(_), b @ Boolean::Not(_))
848 | (a @ Boolean::Not(_), b @ Boolean::Is(_)) => {
849 let a_lc = a.lc(CS::one(), ConstraintF::one());
850 let b_lc = b.lc(CS::one(), ConstraintF::one());
851 Ok(
852 cond_select_helper(cs, cond, (a.get_value(), a_lc), (b.get_value(), b_lc))?
853 .into(),
854 )
855 },
856 },
857 }
858 }
859
860 fn cost() -> usize {
861 1
862 }
863}
864
865#[cfg(test)]
866mod test {
867 use super::{AllocatedBit, Boolean};
868 use crate::{prelude::*, test_constraint_system::TestConstraintSystem};
869 use algebra::{bls12_381::Fr, BitIterator, Field, One, PrimeField, UniformRand, Zero};
870 use core::str::FromStr;
871 use r1cs_core::ConstraintSystem;
872 use rand::SeedableRng;
873 use rand_xorshift::XorShiftRng;
874
875 #[test]
876 fn test_boolean_to_byte() {
877 for val in [true, false].iter() {
878 let mut cs = TestConstraintSystem::<Fr>::new();
879 let a: Boolean = AllocatedBit::alloc(&mut cs, || Ok(*val)).unwrap().into();
880 let bytes = a.to_bytes(&mut cs.ns(|| "ToBytes")).unwrap();
881 assert_eq!(bytes.len(), 1);
882 let byte = &bytes[0];
883 assert_eq!(byte.value.unwrap(), *val as u8);
884
885 for (i, bit_gadget) in byte.bits.iter().enumerate() {
886 assert_eq!(
887 bit_gadget.get_value().unwrap(),
888 (byte.value.unwrap() >> i) & 1 == 1
889 );
890 }
891 }
892 }
893
894 #[test]
895 fn test_allocated_bit() {
896 let mut cs = TestConstraintSystem::<Fr>::new();
897
898 AllocatedBit::alloc(&mut cs, || Ok(true)).unwrap();
899 assert!(cs.get("boolean") == Fr::one());
900 assert!(cs.is_satisfied());
901 cs.set("boolean", Fr::zero());
902 assert!(cs.is_satisfied());
903 cs.set("boolean", Fr::from_str("2").unwrap());
904 assert!(!cs.is_satisfied());
905 assert!(cs.which_is_unsatisfied() == Some("boolean constraint"));
906 }
907
908 #[test]
909 fn test_xor() {
910 for a_val in [false, true].iter() {
911 for b_val in [false, true].iter() {
912 let mut cs = TestConstraintSystem::<Fr>::new();
913 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
914 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
915 let c = AllocatedBit::xor(&mut cs, &a, &b).unwrap();
916 assert_eq!(c.value.unwrap(), *a_val ^ *b_val);
917
918 assert!(cs.is_satisfied());
919 }
920 }
921 }
922
923 #[test]
924 fn test_or() {
925 for a_val in [false, true].iter() {
926 for b_val in [false, true].iter() {
927 let mut cs = TestConstraintSystem::<Fr>::new();
928 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
929 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
930 let c = AllocatedBit::or(&mut cs, &a, &b).unwrap();
931 assert_eq!(c.value.unwrap(), *a_val | *b_val);
932
933 assert!(cs.is_satisfied());
934 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
935 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
936 }
937 }
938 }
939
940 #[test]
941 fn test_and() {
942 for a_val in [false, true].iter() {
943 for b_val in [false, true].iter() {
944 let mut cs = TestConstraintSystem::<Fr>::new();
945 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
946 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
947 let c = AllocatedBit::and(&mut cs, &a, &b).unwrap();
948 assert_eq!(c.value.unwrap(), *a_val & *b_val);
949
950 assert!(cs.is_satisfied());
951 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
952 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
953 assert!(
954 cs.get("and result")
955 == if *a_val & *b_val {
956 Fr::one()
957 } else {
958 Fr::zero()
959 }
960 );
961
962 // Invert the result and check if the constraint system is still satisfied
963 cs.set(
964 "and result",
965 if *a_val & *b_val {
966 Fr::zero()
967 } else {
968 Fr::one()
969 },
970 );
971 assert!(!cs.is_satisfied());
972 }
973 }
974 }
975
976 #[test]
977 fn test_and_not() {
978 for a_val in [false, true].iter() {
979 for b_val in [false, true].iter() {
980 let mut cs = TestConstraintSystem::<Fr>::new();
981 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
982 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
983 let c = AllocatedBit::and_not(&mut cs, &a, &b).unwrap();
984 assert_eq!(c.value.unwrap(), *a_val & !*b_val);
985
986 assert!(cs.is_satisfied());
987 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
988 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
989 assert!(
990 cs.get("and not result")
991 == if *a_val & !*b_val {
992 Fr::one()
993 } else {
994 Fr::zero()
995 }
996 );
997
998 // Invert the result and check if the constraint system is still satisfied
999 cs.set(
1000 "and not result",
1001 if *a_val & !*b_val {
1002 Fr::zero()
1003 } else {
1004 Fr::one()
1005 },
1006 );
1007 assert!(!cs.is_satisfied());
1008 }
1009 }
1010 }
1011
1012 #[test]
1013 fn test_nor() {
1014 for a_val in [false, true].iter() {
1015 for b_val in [false, true].iter() {
1016 let mut cs = TestConstraintSystem::<Fr>::new();
1017 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
1018 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
1019 let c = AllocatedBit::nor(&mut cs, &a, &b).unwrap();
1020 assert_eq!(c.value.unwrap(), !*a_val & !*b_val);
1021
1022 assert!(cs.is_satisfied());
1023 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
1024 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
1025 assert!(
1026 cs.get("nor result")
1027 == if !*a_val & !*b_val {
1028 Fr::one()
1029 } else {
1030 Fr::zero()
1031 }
1032 );
1033
1034 // Invert the result and check if the constraint system is still satisfied
1035 cs.set(
1036 "nor result",
1037 if !*a_val & !*b_val {
1038 Fr::zero()
1039 } else {
1040 Fr::one()
1041 },
1042 );
1043 assert!(!cs.is_satisfied());
1044 }
1045 }
1046 }
1047
1048 #[test]
1049 fn test_enforce_equal() {
1050 for a_bool in [false, true].iter().cloned() {
1051 for b_bool in [false, true].iter().cloned() {
1052 for a_neg in [false, true].iter().cloned() {
1053 for b_neg in [false, true].iter().cloned() {
1054 let mut cs = TestConstraintSystem::<Fr>::new();
1055
1056 let mut a: Boolean = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(a_bool))
1057 .unwrap()
1058 .into();
1059 let mut b: Boolean = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(b_bool))
1060 .unwrap()
1061 .into();
1062
1063 if a_neg {
1064 a = a.not();
1065 }
1066 if b_neg {
1067 b = b.not();
1068 }
1069
1070 a.enforce_equal(&mut cs, &b).unwrap();
1071
1072 assert_eq!(cs.is_satisfied(), (a_bool ^ a_neg) == (b_bool ^ b_neg));
1073 }
1074 }
1075 }
1076 }
1077 }
1078
1079 #[test]
1080 fn test_conditional_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 // First test if constraint system is satisfied
1088 // when we do want to enforce the condition.
1089 let mut a: Boolean = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(a_bool))
1090 .unwrap()
1091 .into();
1092 let mut b: Boolean = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(b_bool))
1093 .unwrap()
1094 .into();
1095
1096 if a_neg {
1097 a = a.not();
1098 }
1099 if b_neg {
1100 b = b.not();
1101 }
1102
1103 a.conditional_enforce_equal(&mut cs, &b, &Boolean::constant(true))
1104 .unwrap();
1105
1106 assert_eq!(cs.is_satisfied(), (a_bool ^ a_neg) == (b_bool ^ b_neg));
1107
1108 // Now test if constraint system is satisfied even
1109 // when we don't want to enforce the condition.
1110 let mut cs = TestConstraintSystem::<Fr>::new();
1111
1112 let mut a: Boolean = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(a_bool))
1113 .unwrap()
1114 .into();
1115 let mut b: Boolean = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(b_bool))
1116 .unwrap()
1117 .into();
1118
1119 if a_neg {
1120 a = a.not();
1121 }
1122 if b_neg {
1123 b = b.not();
1124 }
1125
1126 let false_cond = AllocatedBit::alloc(cs.ns(|| "cond"), || Ok(false))
1127 .unwrap()
1128 .into();
1129 a.conditional_enforce_equal(&mut cs, &b, &false_cond)
1130 .unwrap();
1131
1132 assert!(cs.is_satisfied());
1133 }
1134 }
1135 }
1136 }
1137 }
1138
1139 #[test]
1140 fn test_boolean_negation() {
1141 let mut cs = TestConstraintSystem::<Fr>::new();
1142
1143 let mut b = Boolean::from(AllocatedBit::alloc(&mut cs, || Ok(true)).unwrap());
1144
1145 match b {
1146 Boolean::Is(_) => {},
1147 _ => panic!("unexpected value"),
1148 }
1149
1150 b = b.not();
1151
1152 match b {
1153 Boolean::Not(_) => {},
1154 _ => panic!("unexpected value"),
1155 }
1156
1157 b = b.not();
1158
1159 match b {
1160 Boolean::Is(_) => {},
1161 _ => panic!("unexpected value"),
1162 }
1163
1164 b = Boolean::constant(true);
1165
1166 match b {
1167 Boolean::Constant(true) => {},
1168 _ => panic!("unexpected value"),
1169 }
1170
1171 b = b.not();
1172
1173 match b {
1174 Boolean::Constant(false) => {},
1175 _ => panic!("unexpected value"),
1176 }
1177
1178 b = b.not();
1179
1180 match b {
1181 Boolean::Constant(true) => {},
1182 _ => panic!("unexpected value"),
1183 }
1184 }
1185
1186 #[derive(Copy, Clone, Debug)]
1187 enum OperandType {
1188 True,
1189 False,
1190 AllocatedTrue,
1191 AllocatedFalse,
1192 NegatedAllocatedTrue,
1193 NegatedAllocatedFalse,
1194 }
1195
1196 #[test]
1197 fn test_boolean_xor() {
1198 let variants = [
1199 OperandType::True,
1200 OperandType::False,
1201 OperandType::AllocatedTrue,
1202 OperandType::AllocatedFalse,
1203 OperandType::NegatedAllocatedTrue,
1204 OperandType::NegatedAllocatedFalse,
1205 ];
1206
1207 for first_operand in variants.iter().cloned() {
1208 for second_operand in variants.iter().cloned() {
1209 let mut cs = TestConstraintSystem::<Fr>::new();
1210
1211 let a;
1212 let b;
1213
1214 {
1215 let mut dyn_construct = |operand, name| {
1216 let cs = cs.ns(|| name);
1217
1218 match operand {
1219 OperandType::True => Boolean::constant(true),
1220 OperandType::False => Boolean::constant(false),
1221 OperandType::AllocatedTrue => {
1222 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1223 },
1224 OperandType::AllocatedFalse => {
1225 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1226 },
1227 OperandType::NegatedAllocatedTrue => {
1228 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap()).not()
1229 },
1230 OperandType::NegatedAllocatedFalse => {
1231 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap()).not()
1232 },
1233 }
1234 };
1235
1236 a = dyn_construct(first_operand, "a");
1237 b = dyn_construct(second_operand, "b");
1238 }
1239
1240 let c = Boolean::xor(&mut cs, &a, &b).unwrap();
1241
1242 assert!(cs.is_satisfied());
1243
1244 match (first_operand, second_operand, c) {
1245 (OperandType::True, OperandType::True, Boolean::Constant(false)) => {},
1246 (OperandType::True, OperandType::False, Boolean::Constant(true)) => {},
1247 (OperandType::True, OperandType::AllocatedTrue, Boolean::Not(_)) => {},
1248 (OperandType::True, OperandType::AllocatedFalse, Boolean::Not(_)) => {},
1249 (OperandType::True, OperandType::NegatedAllocatedTrue, Boolean::Is(_)) => {},
1250 (OperandType::True, OperandType::NegatedAllocatedFalse, Boolean::Is(_)) => {},
1251
1252 (OperandType::False, OperandType::True, Boolean::Constant(true)) => {},
1253 (OperandType::False, OperandType::False, Boolean::Constant(false)) => {},
1254 (OperandType::False, OperandType::AllocatedTrue, Boolean::Is(_)) => {},
1255 (OperandType::False, OperandType::AllocatedFalse, Boolean::Is(_)) => {},
1256 (OperandType::False, OperandType::NegatedAllocatedTrue, Boolean::Not(_)) => {},
1257 (OperandType::False, OperandType::NegatedAllocatedFalse, Boolean::Not(_)) => {},
1258
1259 (OperandType::AllocatedTrue, OperandType::True, Boolean::Not(_)) => {},
1260 (OperandType::AllocatedTrue, OperandType::False, Boolean::Is(_)) => {},
1261 (
1262 OperandType::AllocatedTrue,
1263 OperandType::AllocatedTrue,
1264 Boolean::Is(ref v),
1265 ) => {
1266 assert!(cs.get("xor result") == Fr::zero());
1267 assert_eq!(v.value, Some(false));
1268 },
1269 (
1270 OperandType::AllocatedTrue,
1271 OperandType::AllocatedFalse,
1272 Boolean::Is(ref v),
1273 ) => {
1274 assert!(cs.get("xor result") == Fr::one());
1275 assert_eq!(v.value, Some(true));
1276 },
1277 (
1278 OperandType::AllocatedTrue,
1279 OperandType::NegatedAllocatedTrue,
1280 Boolean::Not(ref v),
1281 ) => {
1282 assert!(cs.get("xor result") == Fr::zero());
1283 assert_eq!(v.value, Some(false));
1284 },
1285 (
1286 OperandType::AllocatedTrue,
1287 OperandType::NegatedAllocatedFalse,
1288 Boolean::Not(ref v),
1289 ) => {
1290 assert!(cs.get("xor result") == Fr::one());
1291 assert_eq!(v.value, Some(true));
1292 },
1293
1294 (OperandType::AllocatedFalse, OperandType::True, Boolean::Not(_)) => {},
1295 (OperandType::AllocatedFalse, OperandType::False, Boolean::Is(_)) => {},
1296 (
1297 OperandType::AllocatedFalse,
1298 OperandType::AllocatedTrue,
1299 Boolean::Is(ref v),
1300 ) => {
1301 assert!(cs.get("xor result") == Fr::one());
1302 assert_eq!(v.value, Some(true));
1303 },
1304 (
1305 OperandType::AllocatedFalse,
1306 OperandType::AllocatedFalse,
1307 Boolean::Is(ref v),
1308 ) => {
1309 assert!(cs.get("xor result") == Fr::zero());
1310 assert_eq!(v.value, Some(false));
1311 },
1312 (
1313 OperandType::AllocatedFalse,
1314 OperandType::NegatedAllocatedTrue,
1315 Boolean::Not(ref v),
1316 ) => {
1317 assert!(cs.get("xor result") == Fr::one());
1318 assert_eq!(v.value, Some(true));
1319 },
1320 (
1321 OperandType::AllocatedFalse,
1322 OperandType::NegatedAllocatedFalse,
1323 Boolean::Not(ref v),
1324 ) => {
1325 assert!(cs.get("xor result") == Fr::zero());
1326 assert_eq!(v.value, Some(false));
1327 },
1328
1329 (OperandType::NegatedAllocatedTrue, OperandType::True, Boolean::Is(_)) => {},
1330 (OperandType::NegatedAllocatedTrue, OperandType::False, Boolean::Not(_)) => {},
1331 (
1332 OperandType::NegatedAllocatedTrue,
1333 OperandType::AllocatedTrue,
1334 Boolean::Not(ref v),
1335 ) => {
1336 assert!(cs.get("xor result") == Fr::zero());
1337 assert_eq!(v.value, Some(false));
1338 },
1339 (
1340 OperandType::NegatedAllocatedTrue,
1341 OperandType::AllocatedFalse,
1342 Boolean::Not(ref v),
1343 ) => {
1344 assert!(cs.get("xor result") == Fr::one());
1345 assert_eq!(v.value, Some(true));
1346 },
1347 (
1348 OperandType::NegatedAllocatedTrue,
1349 OperandType::NegatedAllocatedTrue,
1350 Boolean::Is(ref v),
1351 ) => {
1352 assert!(cs.get("xor result") == Fr::zero());
1353 assert_eq!(v.value, Some(false));
1354 },
1355 (
1356 OperandType::NegatedAllocatedTrue,
1357 OperandType::NegatedAllocatedFalse,
1358 Boolean::Is(ref v),
1359 ) => {
1360 assert!(cs.get("xor result") == Fr::one());
1361 assert_eq!(v.value, Some(true));
1362 },
1363
1364 (OperandType::NegatedAllocatedFalse, OperandType::True, Boolean::Is(_)) => {},
1365 (OperandType::NegatedAllocatedFalse, OperandType::False, Boolean::Not(_)) => {},
1366 (
1367 OperandType::NegatedAllocatedFalse,
1368 OperandType::AllocatedTrue,
1369 Boolean::Not(ref v),
1370 ) => {
1371 assert!(cs.get("xor result") == Fr::one());
1372 assert_eq!(v.value, Some(true));
1373 },
1374 (
1375 OperandType::NegatedAllocatedFalse,
1376 OperandType::AllocatedFalse,
1377 Boolean::Not(ref v),
1378 ) => {
1379 assert!(cs.get("xor result") == Fr::zero());
1380 assert_eq!(v.value, Some(false));
1381 },
1382 (
1383 OperandType::NegatedAllocatedFalse,
1384 OperandType::NegatedAllocatedTrue,
1385 Boolean::Is(ref v),
1386 ) => {
1387 assert!(cs.get("xor result") == Fr::one());
1388 assert_eq!(v.value, Some(true));
1389 },
1390 (
1391 OperandType::NegatedAllocatedFalse,
1392 OperandType::NegatedAllocatedFalse,
1393 Boolean::Is(ref v),
1394 ) => {
1395 assert!(cs.get("xor result") == Fr::zero());
1396 assert_eq!(v.value, Some(false));
1397 },
1398
1399 _ => panic!("this should never be encountered"),
1400 }
1401 }
1402 }
1403 }
1404
1405 #[test]
1406 fn test_boolean_cond_select() {
1407 let variants = [
1408 OperandType::True,
1409 OperandType::False,
1410 OperandType::AllocatedTrue,
1411 OperandType::AllocatedFalse,
1412 OperandType::NegatedAllocatedTrue,
1413 OperandType::NegatedAllocatedFalse,
1414 ];
1415
1416 for condition in variants.iter().cloned() {
1417 for first_operand in variants.iter().cloned() {
1418 for second_operand in variants.iter().cloned() {
1419 let mut cs = TestConstraintSystem::<Fr>::new();
1420
1421 let cond;
1422 let a;
1423 let b;
1424
1425 {
1426 let mut dyn_construct = |operand, name| {
1427 let cs = cs.ns(|| name);
1428
1429 match operand {
1430 OperandType::True => Boolean::constant(true),
1431 OperandType::False => Boolean::constant(false),
1432 OperandType::AllocatedTrue => {
1433 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1434 },
1435 OperandType::AllocatedFalse => {
1436 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1437 },
1438 OperandType::NegatedAllocatedTrue => {
1439 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1440 .not()
1441 },
1442 OperandType::NegatedAllocatedFalse => {
1443 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1444 .not()
1445 },
1446 }
1447 };
1448
1449 cond = dyn_construct(condition, "cond");
1450 a = dyn_construct(first_operand, "a");
1451 b = dyn_construct(second_operand, "b");
1452 }
1453
1454 let before = cs.num_constraints();
1455 let c = Boolean::conditionally_select(&mut cs, &cond, &a, &b).unwrap();
1456 let after = cs.num_constraints();
1457
1458 assert!(
1459 cs.is_satisfied(),
1460 "failed with operands: cond: {:?}, a: {:?}, b: {:?}",
1461 condition,
1462 first_operand,
1463 second_operand,
1464 );
1465 assert_eq!(
1466 c.get_value(),
1467 if cond.get_value().unwrap() {
1468 a.get_value()
1469 } else {
1470 b.get_value()
1471 }
1472 );
1473 assert!(<Boolean as CondSelectGadget<Fr>>::cost() >= after - before);
1474 }
1475 }
1476 }
1477 }
1478
1479 #[test]
1480 fn test_boolean_or() {
1481 let variants = [
1482 OperandType::True,
1483 OperandType::False,
1484 OperandType::AllocatedTrue,
1485 OperandType::AllocatedFalse,
1486 OperandType::NegatedAllocatedTrue,
1487 OperandType::NegatedAllocatedFalse,
1488 ];
1489
1490 for first_operand in variants.iter().cloned() {
1491 for second_operand in variants.iter().cloned() {
1492 let mut cs = TestConstraintSystem::<Fr>::new();
1493
1494 let a;
1495 let b;
1496
1497 {
1498 let mut dyn_construct = |operand, name| {
1499 let cs = cs.ns(|| name);
1500
1501 match operand {
1502 OperandType::True => Boolean::constant(true),
1503 OperandType::False => Boolean::constant(false),
1504 OperandType::AllocatedTrue => {
1505 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1506 },
1507 OperandType::AllocatedFalse => {
1508 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1509 },
1510 OperandType::NegatedAllocatedTrue => {
1511 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap()).not()
1512 },
1513 OperandType::NegatedAllocatedFalse => {
1514 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap()).not()
1515 },
1516 }
1517 };
1518
1519 a = dyn_construct(first_operand, "a");
1520 b = dyn_construct(second_operand, "b");
1521 }
1522
1523 let c = Boolean::or(&mut cs, &a, &b).unwrap();
1524
1525 assert!(cs.is_satisfied());
1526
1527 match (first_operand, second_operand, c) {
1528 (OperandType::True, OperandType::True, Boolean::Constant(true)) => {},
1529 (OperandType::True, OperandType::False, Boolean::Constant(true)) => {},
1530 (OperandType::True, OperandType::AllocatedTrue, Boolean::Constant(true)) => {},
1531 (OperandType::True, OperandType::AllocatedFalse, Boolean::Constant(true)) => {},
1532 (
1533 OperandType::True,
1534 OperandType::NegatedAllocatedTrue,
1535 Boolean::Constant(true),
1536 ) => {},
1537 (
1538 OperandType::True,
1539 OperandType::NegatedAllocatedFalse,
1540 Boolean::Constant(true),
1541 ) => {},
1542
1543 (OperandType::False, OperandType::True, Boolean::Constant(true)) => {},
1544 (OperandType::False, OperandType::False, Boolean::Constant(false)) => {},
1545 (OperandType::False, OperandType::AllocatedTrue, Boolean::Is(_)) => {},
1546 (OperandType::False, OperandType::AllocatedFalse, Boolean::Is(_)) => {},
1547 (OperandType::False, OperandType::NegatedAllocatedTrue, Boolean::Not(_)) => {},
1548 (OperandType::False, OperandType::NegatedAllocatedFalse, Boolean::Not(_)) => {},
1549
1550 (OperandType::AllocatedTrue, OperandType::True, Boolean::Constant(true)) => {},
1551 (OperandType::AllocatedTrue, OperandType::False, Boolean::Is(_)) => {},
1552 (
1553 OperandType::AllocatedTrue,
1554 OperandType::AllocatedTrue,
1555 Boolean::Is(ref v),
1556 ) => {
1557 assert_eq!(v.value, Some(true));
1558 },
1559 (
1560 OperandType::AllocatedTrue,
1561 OperandType::AllocatedFalse,
1562 Boolean::Is(ref v),
1563 ) => {
1564 assert_eq!(v.value, Some(true));
1565 },
1566 (
1567 OperandType::AllocatedTrue,
1568 OperandType::NegatedAllocatedTrue,
1569 Boolean::Not(ref v),
1570 ) => {
1571 assert_eq!(v.value, Some(false));
1572 },
1573 (
1574 OperandType::AllocatedTrue,
1575 OperandType::NegatedAllocatedFalse,
1576 Boolean::Not(ref v),
1577 ) => {
1578 assert_eq!(v.value, Some(false));
1579 },
1580
1581 (OperandType::AllocatedFalse, OperandType::True, Boolean::Constant(true)) => {},
1582 (OperandType::AllocatedFalse, OperandType::False, Boolean::Is(_)) => {},
1583 (
1584 OperandType::AllocatedFalse,
1585 OperandType::AllocatedTrue,
1586 Boolean::Is(ref v),
1587 ) => {
1588 assert_eq!(v.value, Some(true));
1589 },
1590 (
1591 OperandType::AllocatedFalse,
1592 OperandType::AllocatedFalse,
1593 Boolean::Is(ref v),
1594 ) => {
1595 assert_eq!(v.value, Some(false));
1596 },
1597 (
1598 OperandType::AllocatedFalse,
1599 OperandType::NegatedAllocatedTrue,
1600 Boolean::Not(ref v),
1601 ) => {
1602 assert_eq!(v.value, Some(true));
1603 },
1604 (
1605 OperandType::AllocatedFalse,
1606 OperandType::NegatedAllocatedFalse,
1607 Boolean::Not(ref v),
1608 ) => {
1609 assert_eq!(v.value, Some(false));
1610 },
1611
1612 (
1613 OperandType::NegatedAllocatedTrue,
1614 OperandType::True,
1615 Boolean::Constant(true),
1616 ) => {},
1617 (OperandType::NegatedAllocatedTrue, OperandType::False, Boolean::Not(_)) => {},
1618 (
1619 OperandType::NegatedAllocatedTrue,
1620 OperandType::AllocatedTrue,
1621 Boolean::Not(ref v),
1622 ) => {
1623 assert_eq!(v.value, Some(false));
1624 },
1625 (
1626 OperandType::NegatedAllocatedTrue,
1627 OperandType::AllocatedFalse,
1628 Boolean::Not(ref v),
1629 ) => {
1630 assert_eq!(v.value, Some(true));
1631 },
1632 (
1633 OperandType::NegatedAllocatedTrue,
1634 OperandType::NegatedAllocatedTrue,
1635 Boolean::Not(ref v),
1636 ) => {
1637 assert_eq!(v.value, Some(true));
1638 },
1639 (
1640 OperandType::NegatedAllocatedTrue,
1641 OperandType::NegatedAllocatedFalse,
1642 Boolean::Not(ref v),
1643 ) => {
1644 assert_eq!(v.value, Some(false));
1645 },
1646
1647 (
1648 OperandType::NegatedAllocatedFalse,
1649 OperandType::True,
1650 Boolean::Constant(true),
1651 ) => {},
1652 (OperandType::NegatedAllocatedFalse, OperandType::False, Boolean::Not(_)) => {},
1653 (
1654 OperandType::NegatedAllocatedFalse,
1655 OperandType::AllocatedTrue,
1656 Boolean::Not(ref v),
1657 ) => {
1658 assert_eq!(v.value, Some(false));
1659 },
1660 (
1661 OperandType::NegatedAllocatedFalse,
1662 OperandType::AllocatedFalse,
1663 Boolean::Not(ref v),
1664 ) => {
1665 assert_eq!(v.value, Some(false));
1666 },
1667 (
1668 OperandType::NegatedAllocatedFalse,
1669 OperandType::NegatedAllocatedTrue,
1670 Boolean::Not(ref v),
1671 ) => {
1672 assert_eq!(v.value, Some(false));
1673 },
1674 (
1675 OperandType::NegatedAllocatedFalse,
1676 OperandType::NegatedAllocatedFalse,
1677 Boolean::Not(ref v),
1678 ) => {
1679 assert_eq!(v.value, Some(false));
1680 },
1681
1682 _ => panic!(
1683 "this should never be encountered, in case: (a = {:?}, b = {:?}, c = {:?})",
1684 a, b, c
1685 ),
1686 }
1687 }
1688 }
1689 }
1690
1691 #[test]
1692 fn test_boolean_and() {
1693 let variants = [
1694 OperandType::True,
1695 OperandType::False,
1696 OperandType::AllocatedTrue,
1697 OperandType::AllocatedFalse,
1698 OperandType::NegatedAllocatedTrue,
1699 OperandType::NegatedAllocatedFalse,
1700 ];
1701
1702 for first_operand in variants.iter().cloned() {
1703 for second_operand in variants.iter().cloned() {
1704 let mut cs = TestConstraintSystem::<Fr>::new();
1705
1706 let a;
1707 let b;
1708
1709 {
1710 let mut dyn_construct = |operand, name| {
1711 let cs = cs.ns(|| name);
1712
1713 match operand {
1714 OperandType::True => Boolean::constant(true),
1715 OperandType::False => Boolean::constant(false),
1716 OperandType::AllocatedTrue => {
1717 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1718 },
1719 OperandType::AllocatedFalse => {
1720 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1721 },
1722 OperandType::NegatedAllocatedTrue => {
1723 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap()).not()
1724 },
1725 OperandType::NegatedAllocatedFalse => {
1726 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap()).not()
1727 },
1728 }
1729 };
1730
1731 a = dyn_construct(first_operand, "a");
1732 b = dyn_construct(second_operand, "b");
1733 }
1734
1735 let c = Boolean::and(&mut cs, &a, &b).unwrap();
1736
1737 assert!(cs.is_satisfied());
1738
1739 match (first_operand, second_operand, c) {
1740 (OperandType::True, OperandType::True, Boolean::Constant(true)) => {},
1741 (OperandType::True, OperandType::False, Boolean::Constant(false)) => {},
1742 (OperandType::True, OperandType::AllocatedTrue, Boolean::Is(_)) => {},
1743 (OperandType::True, OperandType::AllocatedFalse, Boolean::Is(_)) => {},
1744 (OperandType::True, OperandType::NegatedAllocatedTrue, Boolean::Not(_)) => {},
1745 (OperandType::True, OperandType::NegatedAllocatedFalse, Boolean::Not(_)) => {},
1746
1747 (OperandType::False, OperandType::True, Boolean::Constant(false)) => {},
1748 (OperandType::False, OperandType::False, Boolean::Constant(false)) => {},
1749 (OperandType::False, OperandType::AllocatedTrue, Boolean::Constant(false)) => {
1750 },
1751 (OperandType::False, OperandType::AllocatedFalse, Boolean::Constant(false)) => {
1752 },
1753 (
1754 OperandType::False,
1755 OperandType::NegatedAllocatedTrue,
1756 Boolean::Constant(false),
1757 ) => {},
1758 (
1759 OperandType::False,
1760 OperandType::NegatedAllocatedFalse,
1761 Boolean::Constant(false),
1762 ) => {},
1763
1764 (OperandType::AllocatedTrue, OperandType::True, Boolean::Is(_)) => {},
1765 (OperandType::AllocatedTrue, OperandType::False, Boolean::Constant(false)) => {
1766 },
1767 (
1768 OperandType::AllocatedTrue,
1769 OperandType::AllocatedTrue,
1770 Boolean::Is(ref v),
1771 ) => {
1772 assert!(cs.get("and result") == Fr::one());
1773 assert_eq!(v.value, Some(true));
1774 },
1775 (
1776 OperandType::AllocatedTrue,
1777 OperandType::AllocatedFalse,
1778 Boolean::Is(ref v),
1779 ) => {
1780 assert!(cs.get("and result") == Fr::zero());
1781 assert_eq!(v.value, Some(false));
1782 },
1783 (
1784 OperandType::AllocatedTrue,
1785 OperandType::NegatedAllocatedTrue,
1786 Boolean::Is(ref v),
1787 ) => {
1788 assert!(cs.get("and not result") == Fr::zero());
1789 assert_eq!(v.value, Some(false));
1790 },
1791 (
1792 OperandType::AllocatedTrue,
1793 OperandType::NegatedAllocatedFalse,
1794 Boolean::Is(ref v),
1795 ) => {
1796 assert!(cs.get("and not result") == Fr::one());
1797 assert_eq!(v.value, Some(true));
1798 },
1799
1800 (OperandType::AllocatedFalse, OperandType::True, Boolean::Is(_)) => {},
1801 (OperandType::AllocatedFalse, OperandType::False, Boolean::Constant(false)) => {
1802 },
1803 (
1804 OperandType::AllocatedFalse,
1805 OperandType::AllocatedTrue,
1806 Boolean::Is(ref v),
1807 ) => {
1808 assert!(cs.get("and result") == Fr::zero());
1809 assert_eq!(v.value, Some(false));
1810 },
1811 (
1812 OperandType::AllocatedFalse,
1813 OperandType::AllocatedFalse,
1814 Boolean::Is(ref v),
1815 ) => {
1816 assert!(cs.get("and result") == Fr::zero());
1817 assert_eq!(v.value, Some(false));
1818 },
1819 (
1820 OperandType::AllocatedFalse,
1821 OperandType::NegatedAllocatedTrue,
1822 Boolean::Is(ref v),
1823 ) => {
1824 assert!(cs.get("and not result") == Fr::zero());
1825 assert_eq!(v.value, Some(false));
1826 },
1827 (
1828 OperandType::AllocatedFalse,
1829 OperandType::NegatedAllocatedFalse,
1830 Boolean::Is(ref v),
1831 ) => {
1832 assert!(cs.get("and not result") == Fr::zero());
1833 assert_eq!(v.value, Some(false));
1834 },
1835
1836 (OperandType::NegatedAllocatedTrue, OperandType::True, Boolean::Not(_)) => {},
1837 (
1838 OperandType::NegatedAllocatedTrue,
1839 OperandType::False,
1840 Boolean::Constant(false),
1841 ) => {},
1842 (
1843 OperandType::NegatedAllocatedTrue,
1844 OperandType::AllocatedTrue,
1845 Boolean::Is(ref v),
1846 ) => {
1847 assert!(cs.get("and not result") == Fr::zero());
1848 assert_eq!(v.value, Some(false));
1849 },
1850 (
1851 OperandType::NegatedAllocatedTrue,
1852 OperandType::AllocatedFalse,
1853 Boolean::Is(ref v),
1854 ) => {
1855 assert!(cs.get("and not result") == Fr::zero());
1856 assert_eq!(v.value, Some(false));
1857 },
1858 (
1859 OperandType::NegatedAllocatedTrue,
1860 OperandType::NegatedAllocatedTrue,
1861 Boolean::Is(ref v),
1862 ) => {
1863 assert!(cs.get("nor result") == Fr::zero());
1864 assert_eq!(v.value, Some(false));
1865 },
1866 (
1867 OperandType::NegatedAllocatedTrue,
1868 OperandType::NegatedAllocatedFalse,
1869 Boolean::Is(ref v),
1870 ) => {
1871 assert!(cs.get("nor result") == Fr::zero());
1872 assert_eq!(v.value, Some(false));
1873 },
1874
1875 (OperandType::NegatedAllocatedFalse, OperandType::True, Boolean::Not(_)) => {},
1876 (
1877 OperandType::NegatedAllocatedFalse,
1878 OperandType::False,
1879 Boolean::Constant(false),
1880 ) => {},
1881 (
1882 OperandType::NegatedAllocatedFalse,
1883 OperandType::AllocatedTrue,
1884 Boolean::Is(ref v),
1885 ) => {
1886 assert!(cs.get("and not result") == Fr::one());
1887 assert_eq!(v.value, Some(true));
1888 },
1889 (
1890 OperandType::NegatedAllocatedFalse,
1891 OperandType::AllocatedFalse,
1892 Boolean::Is(ref v),
1893 ) => {
1894 assert!(cs.get("and not result") == Fr::zero());
1895 assert_eq!(v.value, Some(false));
1896 },
1897 (
1898 OperandType::NegatedAllocatedFalse,
1899 OperandType::NegatedAllocatedTrue,
1900 Boolean::Is(ref v),
1901 ) => {
1902 assert!(cs.get("nor result") == Fr::zero());
1903 assert_eq!(v.value, Some(false));
1904 },
1905 (
1906 OperandType::NegatedAllocatedFalse,
1907 OperandType::NegatedAllocatedFalse,
1908 Boolean::Is(ref v),
1909 ) => {
1910 assert!(cs.get("nor result") == Fr::one());
1911 assert_eq!(v.value, Some(true));
1912 },
1913
1914 _ => {
1915 panic!(
1916 "unexpected behavior at {:?} AND {:?}",
1917 first_operand, second_operand
1918 );
1919 },
1920 }
1921 }
1922 }
1923 }
1924
1925 #[test]
1926 fn test_enforce_in_field() {
1927 {
1928 let mut cs = TestConstraintSystem::<Fr>::new();
1929
1930 let mut bits = vec![];
1931 for (i, b) in BitIterator::new(Fr::characteristic()).skip(1).enumerate() {
1932 bits.push(Boolean::from(
1933 AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}", i)), || Ok(b)).unwrap(),
1934 ));
1935 }
1936
1937 Boolean::enforce_in_field::<_, _, Fr>(&mut cs, &bits).unwrap();
1938
1939 assert!(!cs.is_satisfied());
1940 }
1941
1942 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1943
1944 for _ in 0..1000 {
1945 let r = Fr::rand(&mut rng);
1946 let mut cs = TestConstraintSystem::<Fr>::new();
1947
1948 let mut bits = vec![];
1949 for (i, b) in BitIterator::new(r.into_repr()).skip(1).enumerate() {
1950 bits.push(Boolean::from(
1951 AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}", i)), || Ok(b)).unwrap(),
1952 ));
1953 }
1954
1955 Boolean::enforce_in_field::<_, _, Fr>(&mut cs, &bits).unwrap();
1956
1957 assert!(cs.is_satisfied());
1958 }
1959
1960 // for _ in 0..1000 {
1961 // // Sample a random element not in the field
1962 // let r = loop {
1963 // let mut a = Fr::rand(&mut rng).into_repr();
1964 // let b = Fr::rand(&mut rng).into_repr();
1965
1966 // a.add_nocarry(&b);
1967 // // we're shaving off the high bit_gadget later
1968 // a.as_mut()[3] &= 0x7fffffffffffffff;
1969 // if Fr::from_repr(a).is_err() {
1970 // break a;
1971 // }
1972 // };
1973
1974 // let mut cs = TestConstraintSystem::<Fr>::new();
1975
1976 // let mut bits = vec![];
1977 // for (i, b) in BitIterator::new(r).skip(1).enumerate() {
1978 // bits.push(Boolean::from(
1979 // AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}",
1980 // i)), Some(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}