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