ark-r1cs-std/r1cs-std/src/bits/boolean.rs
r1cs-std/src/bits/boolean.rsRaw
1use algebra::{BitIterator, Field, FpParameters, 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 first: &Self,
316 second: &Self,
317 ) -> Result<Self, SynthesisError> {
318 cond_select_helper(
319 cs,
320 cond,
321 (first.value, first.variable),
322 (second.value, second.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 mut cs: CS,
580 bits: &[Self],
581 ) -> Result<(), SynthesisError>
582 where
583 ConstraintF: Field,
584 CS: ConstraintSystem<ConstraintF>,
585 {
586 let mut bits_iter = bits.iter();
587
588 // b = char() - 1
589 let mut b = F::characteristic().to_vec();
590 assert_eq!(b[0] % 2, 1);
591 b[0] -= 1;
592
593 // Runs of ones in r
594 let mut last_run = Boolean::constant(true);
595 let mut current_run = vec![];
596
597 let mut found_one = false;
598 let mut run_i = 0;
599 let mut nand_i = 0;
600
601 let char_num_bits = <F as PrimeField>::Params::MODULUS_BITS as usize;
602 if bits.len() > char_num_bits {
603 let num_extra_bits = bits.len() - char_num_bits;
604 let mut or_result = Boolean::constant(false);
605 for (i, should_be_zero) in bits[0..num_extra_bits].iter().enumerate() {
606 or_result = Boolean::or(
607 &mut cs.ns(|| format!("Check {}-th or", i)),
608 &or_result,
609 should_be_zero,
610 )?;
611 let _ = bits_iter.next().unwrap();
612 }
613 or_result.enforce_equal(
614 &mut cs.ns(|| "Check that or of extra bits is zero"),
615 &Boolean::constant(false),
616 )?;
617 }
618
619 for b in BitIterator::new(b) {
620 // Skip over unset bits at the beginning
621 found_one |= b;
622 if !found_one {
623 continue;
624 }
625
626 let a = bits_iter.next().unwrap();
627
628 if b {
629 // This is part of a run of ones.
630 current_run.push(a.clone());
631 } else {
632 if !current_run.is_empty() {
633 // This is the start of a run of zeros, but we need
634 // to k-ary AND against `last_run` first.
635
636 current_run.push(last_run);
637 last_run = Self::kary_and(cs.ns(|| format!("run {}", run_i)), ¤t_run)?;
638 run_i += 1;
639 current_run.truncate(0);
640 }
641
642 // If `last_run` is true, `a` must be false, or it would
643 // not be in the field.
644 //
645 // If `last_run` is false, `a` can be true or false.
646 //
647 // Ergo, at least one of `last_run` and `a` must be false.
648 Self::enforce_nand(cs.ns(|| format!("nand {}", nand_i)), &[last_run, *a])?;
649 nand_i += 1;
650 }
651 }
652 assert!(bits_iter.next().is_none());
653
654 // We should always end in a "run" of zeros, because
655 // the characteristic is an odd prime. So, this should
656 // be empty.
657 assert!(current_run.is_empty());
658
659 Ok(())
660 }
661}
662
663impl PartialEq for Boolean {
664 fn eq(&self, other: &Self) -> bool {
665 use self::Boolean::*;
666
667 match (*self, *other) {
668 (Is(a), Is(b)) | (Not(a), Not(b)) => a == b,
669 (Is(a), Not(b)) | (Not(a), Is(b)) => a != b,
670 (Is(a), Constant(b)) | (Constant(b), Is(a)) => a.value.unwrap() == b,
671 (Not(a), Constant(b)) | (Constant(b), Not(a)) => a.value.unwrap() != b,
672 (Constant(a), Constant(b)) => a == b,
673 }
674 }
675}
676
677impl Eq for Boolean {}
678
679impl From<AllocatedBit> for Boolean {
680 fn from(b: AllocatedBit) -> Boolean {
681 Boolean::Is(b)
682 }
683}
684
685impl<ConstraintF: Field> AllocGadget<bool, ConstraintF> for Boolean {
686 fn alloc<F, T, CS: ConstraintSystem<ConstraintF>>(
687 cs: CS,
688 value_gen: F,
689 ) -> Result<Self, SynthesisError>
690 where
691 F: FnOnce() -> Result<T, SynthesisError>,
692 T: Borrow<bool>,
693 {
694 AllocatedBit::alloc(cs, value_gen).map(Boolean::from)
695 }
696
697 fn alloc_input<F, T, CS: ConstraintSystem<ConstraintF>>(
698 cs: CS,
699 value_gen: F,
700 ) -> Result<Self, SynthesisError>
701 where
702 F: FnOnce() -> Result<T, SynthesisError>,
703 T: Borrow<bool>,
704 {
705 AllocatedBit::alloc_input(cs, value_gen).map(Boolean::from)
706 }
707}
708
709impl<ConstraintF: Field> EqGadget<ConstraintF> for Boolean {}
710
711impl<ConstraintF: Field> ConditionalEqGadget<ConstraintF> for Boolean {
712 fn conditional_enforce_equal<CS>(
713 &self,
714 mut cs: CS,
715 other: &Self,
716 condition: &Boolean,
717 ) -> Result<(), SynthesisError>
718 where
719 CS: ConstraintSystem<ConstraintF>,
720 {
721 use self::Boolean::*;
722 let one = CS::one();
723 let difference: LinearCombination<ConstraintF> = match (self, other) {
724 // 1 - 1 = 0 - 0 = 0
725 (Constant(true), Constant(true)) | (Constant(false), Constant(false)) => return Ok(()),
726 // false != true
727 (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
728 // 1 - a
729 (Constant(true), Is(a)) | (Is(a), Constant(true)) => {
730 LinearCombination::zero() + one - a.get_variable()
731 },
732 // a - 0 = a
733 (Constant(false), Is(a)) | (Is(a), Constant(false)) => {
734 LinearCombination::zero() + a.get_variable()
735 },
736 // 1 - !a = 1 - (1 - a) = a
737 (Constant(true), Not(a)) | (Not(a), Constant(true)) => {
738 LinearCombination::zero() + a.get_variable()
739 },
740 // !a - 0 = !a = 1 - a
741 (Constant(false), Not(a)) | (Not(a), Constant(false)) => {
742 LinearCombination::zero() + one - a.get_variable()
743 },
744 // b - a,
745 (Is(a), Is(b)) => LinearCombination::zero() + b.get_variable() - a.get_variable(),
746 // !b - a = (1 - b) - a
747 (Is(a), Not(b)) | (Not(b), Is(a)) => {
748 LinearCombination::zero() + one - b.get_variable() - a.get_variable()
749 },
750 // !b - !a = (1 - b) - (1 - a) = a - b,
751 (Not(a), Not(b)) => LinearCombination::zero() + a.get_variable() - b.get_variable(),
752 };
753
754 if let Constant(false) = condition {
755 Ok(())
756 } else {
757 cs.enforce(
758 || "conditional_equals",
759 |lc| difference + &lc,
760 |lc| condition.lc(one, ConstraintF::one()) + &lc,
761 |lc| lc,
762 );
763 Ok(())
764 }
765 }
766
767 fn cost() -> usize {
768 1
769 }
770}
771
772impl<ConstraintF: Field> ToBytesGadget<ConstraintF> for Boolean {
773 fn to_bytes<CS: ConstraintSystem<ConstraintF>>(
774 &self,
775 _cs: CS,
776 ) -> Result<Vec<UInt8>, SynthesisError> {
777 let mut bits = vec![Boolean::constant(false); 7];
778 bits.push(*self);
779 bits.reverse();
780 let value = self.get_value().map(|val| val as u8);
781 let byte = UInt8 { bits, value };
782 Ok(vec![byte])
783 }
784
785 /// Additionally checks if the produced list of booleans is 'valid'.
786 fn to_bytes_strict<CS: ConstraintSystem<ConstraintF>>(
787 &self,
788 cs: CS,
789 ) -> Result<Vec<UInt8>, SynthesisError> {
790 self.to_bytes(cs)
791 }
792}
793
794impl<ConstraintF: PrimeField> CondSelectGadget<ConstraintF> for Boolean {
795 fn conditionally_select<CS>(
796 mut cs: CS,
797 cond: &Self,
798 first: &Self,
799 second: &Self,
800 ) -> Result<Self, SynthesisError>
801 where
802 CS: ConstraintSystem<ConstraintF>,
803 {
804 match cond {
805 Boolean::Constant(true) => Ok(first.clone()),
806 Boolean::Constant(false) => Ok(second.clone()),
807 cond @ Boolean::Not(_) => Self::conditionally_select(cs, &cond.not(), second, first),
808 cond @ Boolean::Is(_) => match (first, second) {
809 (x, &Boolean::Constant(false)) => Boolean::and(cs.ns(|| "and"), cond, x).into(),
810 (&Boolean::Constant(false), x) => Boolean::and(cs.ns(|| "and"), &cond.not(), x),
811 (&Boolean::Constant(true), x) => Boolean::or(cs.ns(|| "or"), cond, x).into(),
812 (x, &Boolean::Constant(true)) => Boolean::or(cs.ns(|| "or"), &cond.not(), x),
813 (a @ Boolean::Is(_), b @ Boolean::Is(_))
814 | (a @ Boolean::Not(_), b @ Boolean::Not(_))
815 | (a @ Boolean::Is(_), b @ Boolean::Not(_))
816 | (a @ Boolean::Not(_), b @ Boolean::Is(_)) => {
817 let a_lc = a.lc(CS::one(), ConstraintF::one());
818 let b_lc = b.lc(CS::one(), ConstraintF::one());
819 Ok(
820 cond_select_helper(cs, cond, (a.get_value(), a_lc), (b.get_value(), b_lc))?
821 .into(),
822 )
823 },
824 },
825 }
826 }
827
828 fn cost() -> usize {
829 1
830 }
831}
832
833#[cfg(test)]
834mod test {
835 use super::{AllocatedBit, Boolean};
836 use crate::{prelude::*, test_constraint_system::TestConstraintSystem};
837 use algebra::{fields::bls12_381::Fr, BitIterator, Field, One, PrimeField, UniformRand, Zero};
838 use core::str::FromStr;
839 use r1cs_core::ConstraintSystem;
840 use rand::SeedableRng;
841 use rand_xorshift::XorShiftRng;
842
843 #[test]
844 fn test_boolean_to_byte() {
845 for val in [true, false].iter() {
846 let mut cs = TestConstraintSystem::<Fr>::new();
847 let a: Boolean = AllocatedBit::alloc(&mut cs, || Ok(*val)).unwrap().into();
848 let bytes = a.to_bytes(&mut cs.ns(|| "ToBytes")).unwrap();
849 assert_eq!(bytes.len(), 1);
850 let byte = &bytes[0];
851 assert_eq!(byte.value.unwrap(), *val as u8);
852
853 for (i, bit_gadget) in byte.bits.iter().enumerate() {
854 assert_eq!(
855 bit_gadget.get_value().unwrap(),
856 (byte.value.unwrap() >> i) & 1 == 1
857 );
858 }
859 }
860 }
861
862 #[test]
863 fn test_allocated_bit() {
864 let mut cs = TestConstraintSystem::<Fr>::new();
865
866 AllocatedBit::alloc(&mut cs, || Ok(true)).unwrap();
867 assert!(cs.get("boolean") == Fr::one());
868 assert!(cs.is_satisfied());
869 cs.set("boolean", Fr::zero());
870 assert!(cs.is_satisfied());
871 cs.set("boolean", Fr::from_str("2").unwrap());
872 assert!(!cs.is_satisfied());
873 assert!(cs.which_is_unsatisfied() == Some("boolean constraint"));
874 }
875
876 #[test]
877 fn test_xor() {
878 for a_val in [false, true].iter() {
879 for b_val in [false, true].iter() {
880 let mut cs = TestConstraintSystem::<Fr>::new();
881 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
882 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
883 let c = AllocatedBit::xor(&mut cs, &a, &b).unwrap();
884 assert_eq!(c.value.unwrap(), *a_val ^ *b_val);
885
886 assert!(cs.is_satisfied());
887 }
888 }
889 }
890
891 #[test]
892 fn test_or() {
893 for a_val in [false, true].iter() {
894 for b_val in [false, true].iter() {
895 let mut cs = TestConstraintSystem::<Fr>::new();
896 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
897 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
898 let c = AllocatedBit::or(&mut cs, &a, &b).unwrap();
899 assert_eq!(c.value.unwrap(), *a_val | *b_val);
900
901 assert!(cs.is_satisfied());
902 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
903 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
904 }
905 }
906 }
907
908 #[test]
909 fn test_and() {
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::and(&mut cs, &a, &b).unwrap();
916 assert_eq!(c.value.unwrap(), *a_val & *b_val);
917
918 assert!(cs.is_satisfied());
919 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
920 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
921 assert!(
922 cs.get("and result")
923 == if *a_val & *b_val {
924 Fr::one()
925 } else {
926 Fr::zero()
927 }
928 );
929
930 // Invert the result and check if the constraint system is still satisfied
931 cs.set(
932 "and result",
933 if *a_val & *b_val {
934 Fr::zero()
935 } else {
936 Fr::one()
937 },
938 );
939 assert!(!cs.is_satisfied());
940 }
941 }
942 }
943
944 #[test]
945 fn test_and_not() {
946 for a_val in [false, true].iter() {
947 for b_val in [false, true].iter() {
948 let mut cs = TestConstraintSystem::<Fr>::new();
949 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
950 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
951 let c = AllocatedBit::and_not(&mut cs, &a, &b).unwrap();
952 assert_eq!(c.value.unwrap(), *a_val & !*b_val);
953
954 assert!(cs.is_satisfied());
955 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
956 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
957 assert!(
958 cs.get("and not result")
959 == if *a_val & !*b_val {
960 Fr::one()
961 } else {
962 Fr::zero()
963 }
964 );
965
966 // Invert the result and check if the constraint system is still satisfied
967 cs.set(
968 "and not result",
969 if *a_val & !*b_val {
970 Fr::zero()
971 } else {
972 Fr::one()
973 },
974 );
975 assert!(!cs.is_satisfied());
976 }
977 }
978 }
979
980 #[test]
981 fn test_nor() {
982 for a_val in [false, true].iter() {
983 for b_val in [false, true].iter() {
984 let mut cs = TestConstraintSystem::<Fr>::new();
985 let a = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(*a_val)).unwrap();
986 let b = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(*b_val)).unwrap();
987 let c = AllocatedBit::nor(&mut cs, &a, &b).unwrap();
988 assert_eq!(c.value.unwrap(), !*a_val & !*b_val);
989
990 assert!(cs.is_satisfied());
991 assert!(cs.get("a/boolean") == if *a_val { Fr::one() } else { Fr::zero() });
992 assert!(cs.get("b/boolean") == if *b_val { Fr::one() } else { Fr::zero() });
993 assert!(
994 cs.get("nor result")
995 == if !*a_val & !*b_val {
996 Fr::one()
997 } else {
998 Fr::zero()
999 }
1000 );
1001
1002 // Invert the result and check if the constraint system is still satisfied
1003 cs.set(
1004 "nor result",
1005 if !*a_val & !*b_val {
1006 Fr::zero()
1007 } else {
1008 Fr::one()
1009 },
1010 );
1011 assert!(!cs.is_satisfied());
1012 }
1013 }
1014 }
1015
1016 #[test]
1017 fn test_enforce_equal() {
1018 for a_bool in [false, true].iter().cloned() {
1019 for b_bool in [false, true].iter().cloned() {
1020 for a_neg in [false, true].iter().cloned() {
1021 for b_neg in [false, true].iter().cloned() {
1022 let mut cs = TestConstraintSystem::<Fr>::new();
1023
1024 let mut a: Boolean = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(a_bool))
1025 .unwrap()
1026 .into();
1027 let mut b: Boolean = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(b_bool))
1028 .unwrap()
1029 .into();
1030
1031 if a_neg {
1032 a = a.not();
1033 }
1034 if b_neg {
1035 b = b.not();
1036 }
1037
1038 a.enforce_equal(&mut cs, &b).unwrap();
1039
1040 assert_eq!(cs.is_satisfied(), (a_bool ^ a_neg) == (b_bool ^ b_neg));
1041 }
1042 }
1043 }
1044 }
1045 }
1046
1047 #[test]
1048 fn test_conditional_enforce_equal() {
1049 for a_bool in [false, true].iter().cloned() {
1050 for b_bool in [false, true].iter().cloned() {
1051 for a_neg in [false, true].iter().cloned() {
1052 for b_neg in [false, true].iter().cloned() {
1053 let mut cs = TestConstraintSystem::<Fr>::new();
1054
1055 // First test if constraint system is satisfied
1056 // when we do want to enforce the condition.
1057 let mut a: Boolean = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(a_bool))
1058 .unwrap()
1059 .into();
1060 let mut b: Boolean = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(b_bool))
1061 .unwrap()
1062 .into();
1063
1064 if a_neg {
1065 a = a.not();
1066 }
1067 if b_neg {
1068 b = b.not();
1069 }
1070
1071 a.conditional_enforce_equal(&mut cs, &b, &Boolean::constant(true))
1072 .unwrap();
1073
1074 assert_eq!(cs.is_satisfied(), (a_bool ^ a_neg) == (b_bool ^ b_neg));
1075
1076 // Now test if constraint system is satisfied even
1077 // when we don't want to enforce the condition.
1078 let mut cs = TestConstraintSystem::<Fr>::new();
1079
1080 let mut a: Boolean = AllocatedBit::alloc(cs.ns(|| "a"), || Ok(a_bool))
1081 .unwrap()
1082 .into();
1083 let mut b: Boolean = AllocatedBit::alloc(cs.ns(|| "b"), || Ok(b_bool))
1084 .unwrap()
1085 .into();
1086
1087 if a_neg {
1088 a = a.not();
1089 }
1090 if b_neg {
1091 b = b.not();
1092 }
1093
1094 let false_cond = AllocatedBit::alloc(cs.ns(|| "cond"), || Ok(false))
1095 .unwrap()
1096 .into();
1097 a.conditional_enforce_equal(&mut cs, &b, &false_cond)
1098 .unwrap();
1099
1100 assert!(cs.is_satisfied());
1101 }
1102 }
1103 }
1104 }
1105 }
1106
1107 #[test]
1108 fn test_boolean_negation() {
1109 let mut cs = TestConstraintSystem::<Fr>::new();
1110
1111 let mut b = Boolean::from(AllocatedBit::alloc(&mut cs, || Ok(true)).unwrap());
1112
1113 match b {
1114 Boolean::Is(_) => {},
1115 _ => panic!("unexpected value"),
1116 }
1117
1118 b = b.not();
1119
1120 match b {
1121 Boolean::Not(_) => {},
1122 _ => panic!("unexpected value"),
1123 }
1124
1125 b = b.not();
1126
1127 match b {
1128 Boolean::Is(_) => {},
1129 _ => panic!("unexpected value"),
1130 }
1131
1132 b = Boolean::constant(true);
1133
1134 match b {
1135 Boolean::Constant(true) => {},
1136 _ => panic!("unexpected value"),
1137 }
1138
1139 b = b.not();
1140
1141 match b {
1142 Boolean::Constant(false) => {},
1143 _ => panic!("unexpected value"),
1144 }
1145
1146 b = b.not();
1147
1148 match b {
1149 Boolean::Constant(true) => {},
1150 _ => panic!("unexpected value"),
1151 }
1152 }
1153
1154 #[derive(Copy, Clone, Debug)]
1155 enum OperandType {
1156 True,
1157 False,
1158 AllocatedTrue,
1159 AllocatedFalse,
1160 NegatedAllocatedTrue,
1161 NegatedAllocatedFalse,
1162 }
1163
1164 #[test]
1165 fn test_boolean_xor() {
1166 let variants = [
1167 OperandType::True,
1168 OperandType::False,
1169 OperandType::AllocatedTrue,
1170 OperandType::AllocatedFalse,
1171 OperandType::NegatedAllocatedTrue,
1172 OperandType::NegatedAllocatedFalse,
1173 ];
1174
1175 for first_operand in variants.iter().cloned() {
1176 for second_operand in variants.iter().cloned() {
1177 let mut cs = TestConstraintSystem::<Fr>::new();
1178
1179 let a;
1180 let b;
1181
1182 {
1183 let mut dyn_construct = |operand, name| {
1184 let cs = cs.ns(|| name);
1185
1186 match operand {
1187 OperandType::True => Boolean::constant(true),
1188 OperandType::False => Boolean::constant(false),
1189 OperandType::AllocatedTrue => {
1190 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1191 },
1192 OperandType::AllocatedFalse => {
1193 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1194 },
1195 OperandType::NegatedAllocatedTrue => {
1196 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap()).not()
1197 },
1198 OperandType::NegatedAllocatedFalse => {
1199 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap()).not()
1200 },
1201 }
1202 };
1203
1204 a = dyn_construct(first_operand, "a");
1205 b = dyn_construct(second_operand, "b");
1206 }
1207
1208 let c = Boolean::xor(&mut cs, &a, &b).unwrap();
1209
1210 assert!(cs.is_satisfied());
1211
1212 match (first_operand, second_operand, c) {
1213 (OperandType::True, OperandType::True, Boolean::Constant(false)) => {},
1214 (OperandType::True, OperandType::False, Boolean::Constant(true)) => {},
1215 (OperandType::True, OperandType::AllocatedTrue, Boolean::Not(_)) => {},
1216 (OperandType::True, OperandType::AllocatedFalse, Boolean::Not(_)) => {},
1217 (OperandType::True, OperandType::NegatedAllocatedTrue, Boolean::Is(_)) => {},
1218 (OperandType::True, OperandType::NegatedAllocatedFalse, Boolean::Is(_)) => {},
1219
1220 (OperandType::False, OperandType::True, Boolean::Constant(true)) => {},
1221 (OperandType::False, OperandType::False, Boolean::Constant(false)) => {},
1222 (OperandType::False, OperandType::AllocatedTrue, Boolean::Is(_)) => {},
1223 (OperandType::False, OperandType::AllocatedFalse, Boolean::Is(_)) => {},
1224 (OperandType::False, OperandType::NegatedAllocatedTrue, Boolean::Not(_)) => {},
1225 (OperandType::False, OperandType::NegatedAllocatedFalse, Boolean::Not(_)) => {},
1226
1227 (OperandType::AllocatedTrue, OperandType::True, Boolean::Not(_)) => {},
1228 (OperandType::AllocatedTrue, OperandType::False, Boolean::Is(_)) => {},
1229 (
1230 OperandType::AllocatedTrue,
1231 OperandType::AllocatedTrue,
1232 Boolean::Is(ref v),
1233 ) => {
1234 assert!(cs.get("xor result") == Fr::zero());
1235 assert_eq!(v.value, Some(false));
1236 },
1237 (
1238 OperandType::AllocatedTrue,
1239 OperandType::AllocatedFalse,
1240 Boolean::Is(ref v),
1241 ) => {
1242 assert!(cs.get("xor result") == Fr::one());
1243 assert_eq!(v.value, Some(true));
1244 },
1245 (
1246 OperandType::AllocatedTrue,
1247 OperandType::NegatedAllocatedTrue,
1248 Boolean::Not(ref v),
1249 ) => {
1250 assert!(cs.get("xor result") == Fr::zero());
1251 assert_eq!(v.value, Some(false));
1252 },
1253 (
1254 OperandType::AllocatedTrue,
1255 OperandType::NegatedAllocatedFalse,
1256 Boolean::Not(ref v),
1257 ) => {
1258 assert!(cs.get("xor result") == Fr::one());
1259 assert_eq!(v.value, Some(true));
1260 },
1261
1262 (OperandType::AllocatedFalse, OperandType::True, Boolean::Not(_)) => {},
1263 (OperandType::AllocatedFalse, OperandType::False, Boolean::Is(_)) => {},
1264 (
1265 OperandType::AllocatedFalse,
1266 OperandType::AllocatedTrue,
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::AllocatedFalse,
1274 OperandType::AllocatedFalse,
1275 Boolean::Is(ref v),
1276 ) => {
1277 assert!(cs.get("xor result") == Fr::zero());
1278 assert_eq!(v.value, Some(false));
1279 },
1280 (
1281 OperandType::AllocatedFalse,
1282 OperandType::NegatedAllocatedTrue,
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,
1290 OperandType::NegatedAllocatedFalse,
1291 Boolean::Not(ref v),
1292 ) => {
1293 assert!(cs.get("xor result") == Fr::zero());
1294 assert_eq!(v.value, Some(false));
1295 },
1296
1297 (OperandType::NegatedAllocatedTrue, OperandType::True, Boolean::Is(_)) => {},
1298 (OperandType::NegatedAllocatedTrue, OperandType::False, Boolean::Not(_)) => {},
1299 (
1300 OperandType::NegatedAllocatedTrue,
1301 OperandType::AllocatedTrue,
1302 Boolean::Not(ref v),
1303 ) => {
1304 assert!(cs.get("xor result") == Fr::zero());
1305 assert_eq!(v.value, Some(false));
1306 },
1307 (
1308 OperandType::NegatedAllocatedTrue,
1309 OperandType::AllocatedFalse,
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::NegatedAllocatedTrue,
1317 OperandType::NegatedAllocatedTrue,
1318 Boolean::Is(ref v),
1319 ) => {
1320 assert!(cs.get("xor result") == Fr::zero());
1321 assert_eq!(v.value, Some(false));
1322 },
1323 (
1324 OperandType::NegatedAllocatedTrue,
1325 OperandType::NegatedAllocatedFalse,
1326 Boolean::Is(ref v),
1327 ) => {
1328 assert!(cs.get("xor result") == Fr::one());
1329 assert_eq!(v.value, Some(true));
1330 },
1331
1332 (OperandType::NegatedAllocatedFalse, OperandType::True, Boolean::Is(_)) => {},
1333 (OperandType::NegatedAllocatedFalse, OperandType::False, Boolean::Not(_)) => {},
1334 (
1335 OperandType::NegatedAllocatedFalse,
1336 OperandType::AllocatedTrue,
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::NegatedAllocatedFalse,
1344 OperandType::AllocatedFalse,
1345 Boolean::Not(ref v),
1346 ) => {
1347 assert!(cs.get("xor result") == Fr::zero());
1348 assert_eq!(v.value, Some(false));
1349 },
1350 (
1351 OperandType::NegatedAllocatedFalse,
1352 OperandType::NegatedAllocatedTrue,
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,
1360 OperandType::NegatedAllocatedFalse,
1361 Boolean::Is(ref v),
1362 ) => {
1363 assert!(cs.get("xor result") == Fr::zero());
1364 assert_eq!(v.value, Some(false));
1365 },
1366
1367 _ => panic!("this should never be encountered"),
1368 }
1369 }
1370 }
1371 }
1372
1373 #[test]
1374 fn test_boolean_cond_select() {
1375 let variants = [
1376 OperandType::True,
1377 OperandType::False,
1378 OperandType::AllocatedTrue,
1379 OperandType::AllocatedFalse,
1380 OperandType::NegatedAllocatedTrue,
1381 OperandType::NegatedAllocatedFalse,
1382 ];
1383
1384 for condition in variants.iter().cloned() {
1385 for first_operand in variants.iter().cloned() {
1386 for second_operand in variants.iter().cloned() {
1387 let mut cs = TestConstraintSystem::<Fr>::new();
1388
1389 let cond;
1390 let a;
1391 let b;
1392
1393 {
1394 let mut dyn_construct = |operand, name| {
1395 let cs = cs.ns(|| name);
1396
1397 match operand {
1398 OperandType::True => Boolean::constant(true),
1399 OperandType::False => Boolean::constant(false),
1400 OperandType::AllocatedTrue => {
1401 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1402 },
1403 OperandType::AllocatedFalse => {
1404 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1405 },
1406 OperandType::NegatedAllocatedTrue => {
1407 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1408 .not()
1409 },
1410 OperandType::NegatedAllocatedFalse => {
1411 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1412 .not()
1413 },
1414 }
1415 };
1416
1417 cond = dyn_construct(condition, "cond");
1418 a = dyn_construct(first_operand, "a");
1419 b = dyn_construct(second_operand, "b");
1420 }
1421
1422 let before = cs.num_constraints();
1423 let c = Boolean::conditionally_select(&mut cs, &cond, &a, &b).unwrap();
1424 let after = cs.num_constraints();
1425
1426 assert!(
1427 cs.is_satisfied(),
1428 "failed with operands: cond: {:?}, a: {:?}, b: {:?}",
1429 condition,
1430 first_operand,
1431 second_operand,
1432 );
1433 assert_eq!(
1434 c.get_value(),
1435 if cond.get_value().unwrap() {
1436 a.get_value()
1437 } else {
1438 b.get_value()
1439 }
1440 );
1441 assert!(<Boolean as CondSelectGadget<Fr>>::cost() >= after - before);
1442 }
1443 }
1444 }
1445 }
1446
1447 #[test]
1448 fn test_boolean_or() {
1449 let variants = [
1450 OperandType::True,
1451 OperandType::False,
1452 OperandType::AllocatedTrue,
1453 OperandType::AllocatedFalse,
1454 OperandType::NegatedAllocatedTrue,
1455 OperandType::NegatedAllocatedFalse,
1456 ];
1457
1458 for first_operand in variants.iter().cloned() {
1459 for second_operand in variants.iter().cloned() {
1460 let mut cs = TestConstraintSystem::<Fr>::new();
1461
1462 let a;
1463 let b;
1464
1465 {
1466 let mut dyn_construct = |operand, name| {
1467 let cs = cs.ns(|| name);
1468
1469 match operand {
1470 OperandType::True => Boolean::constant(true),
1471 OperandType::False => Boolean::constant(false),
1472 OperandType::AllocatedTrue => {
1473 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1474 },
1475 OperandType::AllocatedFalse => {
1476 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1477 },
1478 OperandType::NegatedAllocatedTrue => {
1479 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap()).not()
1480 },
1481 OperandType::NegatedAllocatedFalse => {
1482 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap()).not()
1483 },
1484 }
1485 };
1486
1487 a = dyn_construct(first_operand, "a");
1488 b = dyn_construct(second_operand, "b");
1489 }
1490
1491 let c = Boolean::or(&mut cs, &a, &b).unwrap();
1492
1493 assert!(cs.is_satisfied());
1494
1495 match (first_operand, second_operand, c) {
1496 (OperandType::True, OperandType::True, Boolean::Constant(true)) => {},
1497 (OperandType::True, OperandType::False, Boolean::Constant(true)) => {},
1498 (OperandType::True, OperandType::AllocatedTrue, Boolean::Constant(true)) => {},
1499 (OperandType::True, OperandType::AllocatedFalse, Boolean::Constant(true)) => {},
1500 (
1501 OperandType::True,
1502 OperandType::NegatedAllocatedTrue,
1503 Boolean::Constant(true),
1504 ) => {},
1505 (
1506 OperandType::True,
1507 OperandType::NegatedAllocatedFalse,
1508 Boolean::Constant(true),
1509 ) => {},
1510
1511 (OperandType::False, OperandType::True, Boolean::Constant(true)) => {},
1512 (OperandType::False, OperandType::False, Boolean::Constant(false)) => {},
1513 (OperandType::False, OperandType::AllocatedTrue, Boolean::Is(_)) => {},
1514 (OperandType::False, OperandType::AllocatedFalse, Boolean::Is(_)) => {},
1515 (OperandType::False, OperandType::NegatedAllocatedTrue, Boolean::Not(_)) => {},
1516 (OperandType::False, OperandType::NegatedAllocatedFalse, Boolean::Not(_)) => {},
1517
1518 (OperandType::AllocatedTrue, OperandType::True, Boolean::Constant(true)) => {},
1519 (OperandType::AllocatedTrue, OperandType::False, Boolean::Is(_)) => {},
1520 (
1521 OperandType::AllocatedTrue,
1522 OperandType::AllocatedTrue,
1523 Boolean::Is(ref v),
1524 ) => {
1525 assert_eq!(v.value, Some(true));
1526 },
1527 (
1528 OperandType::AllocatedTrue,
1529 OperandType::AllocatedFalse,
1530 Boolean::Is(ref v),
1531 ) => {
1532 assert_eq!(v.value, Some(true));
1533 },
1534 (
1535 OperandType::AllocatedTrue,
1536 OperandType::NegatedAllocatedTrue,
1537 Boolean::Not(ref v),
1538 ) => {
1539 assert_eq!(v.value, Some(false));
1540 },
1541 (
1542 OperandType::AllocatedTrue,
1543 OperandType::NegatedAllocatedFalse,
1544 Boolean::Not(ref v),
1545 ) => {
1546 assert_eq!(v.value, Some(false));
1547 },
1548
1549 (OperandType::AllocatedFalse, OperandType::True, Boolean::Constant(true)) => {},
1550 (OperandType::AllocatedFalse, OperandType::False, Boolean::Is(_)) => {},
1551 (
1552 OperandType::AllocatedFalse,
1553 OperandType::AllocatedTrue,
1554 Boolean::Is(ref v),
1555 ) => {
1556 assert_eq!(v.value, Some(true));
1557 },
1558 (
1559 OperandType::AllocatedFalse,
1560 OperandType::AllocatedFalse,
1561 Boolean::Is(ref v),
1562 ) => {
1563 assert_eq!(v.value, Some(false));
1564 },
1565 (
1566 OperandType::AllocatedFalse,
1567 OperandType::NegatedAllocatedTrue,
1568 Boolean::Not(ref v),
1569 ) => {
1570 assert_eq!(v.value, Some(true));
1571 },
1572 (
1573 OperandType::AllocatedFalse,
1574 OperandType::NegatedAllocatedFalse,
1575 Boolean::Not(ref v),
1576 ) => {
1577 assert_eq!(v.value, Some(false));
1578 },
1579
1580 (
1581 OperandType::NegatedAllocatedTrue,
1582 OperandType::True,
1583 Boolean::Constant(true),
1584 ) => {},
1585 (OperandType::NegatedAllocatedTrue, OperandType::False, Boolean::Not(_)) => {},
1586 (
1587 OperandType::NegatedAllocatedTrue,
1588 OperandType::AllocatedTrue,
1589 Boolean::Not(ref v),
1590 ) => {
1591 assert_eq!(v.value, Some(false));
1592 },
1593 (
1594 OperandType::NegatedAllocatedTrue,
1595 OperandType::AllocatedFalse,
1596 Boolean::Not(ref v),
1597 ) => {
1598 assert_eq!(v.value, Some(true));
1599 },
1600 (
1601 OperandType::NegatedAllocatedTrue,
1602 OperandType::NegatedAllocatedTrue,
1603 Boolean::Not(ref v),
1604 ) => {
1605 assert_eq!(v.value, Some(true));
1606 },
1607 (
1608 OperandType::NegatedAllocatedTrue,
1609 OperandType::NegatedAllocatedFalse,
1610 Boolean::Not(ref v),
1611 ) => {
1612 assert_eq!(v.value, Some(false));
1613 },
1614
1615 (
1616 OperandType::NegatedAllocatedFalse,
1617 OperandType::True,
1618 Boolean::Constant(true),
1619 ) => {},
1620 (OperandType::NegatedAllocatedFalse, OperandType::False, Boolean::Not(_)) => {},
1621 (
1622 OperandType::NegatedAllocatedFalse,
1623 OperandType::AllocatedTrue,
1624 Boolean::Not(ref v),
1625 ) => {
1626 assert_eq!(v.value, Some(false));
1627 },
1628 (
1629 OperandType::NegatedAllocatedFalse,
1630 OperandType::AllocatedFalse,
1631 Boolean::Not(ref v),
1632 ) => {
1633 assert_eq!(v.value, Some(false));
1634 },
1635 (
1636 OperandType::NegatedAllocatedFalse,
1637 OperandType::NegatedAllocatedTrue,
1638 Boolean::Not(ref v),
1639 ) => {
1640 assert_eq!(v.value, Some(false));
1641 },
1642 (
1643 OperandType::NegatedAllocatedFalse,
1644 OperandType::NegatedAllocatedFalse,
1645 Boolean::Not(ref v),
1646 ) => {
1647 assert_eq!(v.value, Some(false));
1648 },
1649
1650 _ => panic!(
1651 "this should never be encountered, in case: (a = {:?}, b = {:?}, c = {:?})",
1652 a, b, c
1653 ),
1654 }
1655 }
1656 }
1657 }
1658
1659 #[test]
1660 fn test_boolean_and() {
1661 let variants = [
1662 OperandType::True,
1663 OperandType::False,
1664 OperandType::AllocatedTrue,
1665 OperandType::AllocatedFalse,
1666 OperandType::NegatedAllocatedTrue,
1667 OperandType::NegatedAllocatedFalse,
1668 ];
1669
1670 for first_operand in variants.iter().cloned() {
1671 for second_operand in variants.iter().cloned() {
1672 let mut cs = TestConstraintSystem::<Fr>::new();
1673
1674 let a;
1675 let b;
1676
1677 {
1678 let mut dyn_construct = |operand, name| {
1679 let cs = cs.ns(|| name);
1680
1681 match operand {
1682 OperandType::True => Boolean::constant(true),
1683 OperandType::False => Boolean::constant(false),
1684 OperandType::AllocatedTrue => {
1685 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap())
1686 },
1687 OperandType::AllocatedFalse => {
1688 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap())
1689 },
1690 OperandType::NegatedAllocatedTrue => {
1691 Boolean::from(AllocatedBit::alloc(cs, || Ok(true)).unwrap()).not()
1692 },
1693 OperandType::NegatedAllocatedFalse => {
1694 Boolean::from(AllocatedBit::alloc(cs, || Ok(false)).unwrap()).not()
1695 },
1696 }
1697 };
1698
1699 a = dyn_construct(first_operand, "a");
1700 b = dyn_construct(second_operand, "b");
1701 }
1702
1703 let c = Boolean::and(&mut cs, &a, &b).unwrap();
1704
1705 assert!(cs.is_satisfied());
1706
1707 match (first_operand, second_operand, c) {
1708 (OperandType::True, OperandType::True, Boolean::Constant(true)) => {},
1709 (OperandType::True, OperandType::False, Boolean::Constant(false)) => {},
1710 (OperandType::True, OperandType::AllocatedTrue, Boolean::Is(_)) => {},
1711 (OperandType::True, OperandType::AllocatedFalse, Boolean::Is(_)) => {},
1712 (OperandType::True, OperandType::NegatedAllocatedTrue, Boolean::Not(_)) => {},
1713 (OperandType::True, OperandType::NegatedAllocatedFalse, Boolean::Not(_)) => {},
1714
1715 (OperandType::False, OperandType::True, Boolean::Constant(false)) => {},
1716 (OperandType::False, OperandType::False, Boolean::Constant(false)) => {},
1717 (OperandType::False, OperandType::AllocatedTrue, Boolean::Constant(false)) => {
1718 },
1719 (OperandType::False, OperandType::AllocatedFalse, Boolean::Constant(false)) => {
1720 },
1721 (
1722 OperandType::False,
1723 OperandType::NegatedAllocatedTrue,
1724 Boolean::Constant(false),
1725 ) => {},
1726 (
1727 OperandType::False,
1728 OperandType::NegatedAllocatedFalse,
1729 Boolean::Constant(false),
1730 ) => {},
1731
1732 (OperandType::AllocatedTrue, OperandType::True, Boolean::Is(_)) => {},
1733 (OperandType::AllocatedTrue, OperandType::False, Boolean::Constant(false)) => {
1734 },
1735 (
1736 OperandType::AllocatedTrue,
1737 OperandType::AllocatedTrue,
1738 Boolean::Is(ref v),
1739 ) => {
1740 assert!(cs.get("and result") == Fr::one());
1741 assert_eq!(v.value, Some(true));
1742 },
1743 (
1744 OperandType::AllocatedTrue,
1745 OperandType::AllocatedFalse,
1746 Boolean::Is(ref v),
1747 ) => {
1748 assert!(cs.get("and result") == Fr::zero());
1749 assert_eq!(v.value, Some(false));
1750 },
1751 (
1752 OperandType::AllocatedTrue,
1753 OperandType::NegatedAllocatedTrue,
1754 Boolean::Is(ref v),
1755 ) => {
1756 assert!(cs.get("and not result") == Fr::zero());
1757 assert_eq!(v.value, Some(false));
1758 },
1759 (
1760 OperandType::AllocatedTrue,
1761 OperandType::NegatedAllocatedFalse,
1762 Boolean::Is(ref v),
1763 ) => {
1764 assert!(cs.get("and not result") == Fr::one());
1765 assert_eq!(v.value, Some(true));
1766 },
1767
1768 (OperandType::AllocatedFalse, OperandType::True, Boolean::Is(_)) => {},
1769 (OperandType::AllocatedFalse, OperandType::False, Boolean::Constant(false)) => {
1770 },
1771 (
1772 OperandType::AllocatedFalse,
1773 OperandType::AllocatedTrue,
1774 Boolean::Is(ref v),
1775 ) => {
1776 assert!(cs.get("and result") == Fr::zero());
1777 assert_eq!(v.value, Some(false));
1778 },
1779 (
1780 OperandType::AllocatedFalse,
1781 OperandType::AllocatedFalse,
1782 Boolean::Is(ref v),
1783 ) => {
1784 assert!(cs.get("and result") == Fr::zero());
1785 assert_eq!(v.value, Some(false));
1786 },
1787 (
1788 OperandType::AllocatedFalse,
1789 OperandType::NegatedAllocatedTrue,
1790 Boolean::Is(ref v),
1791 ) => {
1792 assert!(cs.get("and not result") == Fr::zero());
1793 assert_eq!(v.value, Some(false));
1794 },
1795 (
1796 OperandType::AllocatedFalse,
1797 OperandType::NegatedAllocatedFalse,
1798 Boolean::Is(ref v),
1799 ) => {
1800 assert!(cs.get("and not result") == Fr::zero());
1801 assert_eq!(v.value, Some(false));
1802 },
1803
1804 (OperandType::NegatedAllocatedTrue, OperandType::True, Boolean::Not(_)) => {},
1805 (
1806 OperandType::NegatedAllocatedTrue,
1807 OperandType::False,
1808 Boolean::Constant(false),
1809 ) => {},
1810 (
1811 OperandType::NegatedAllocatedTrue,
1812 OperandType::AllocatedTrue,
1813 Boolean::Is(ref v),
1814 ) => {
1815 assert!(cs.get("and not result") == Fr::zero());
1816 assert_eq!(v.value, Some(false));
1817 },
1818 (
1819 OperandType::NegatedAllocatedTrue,
1820 OperandType::AllocatedFalse,
1821 Boolean::Is(ref v),
1822 ) => {
1823 assert!(cs.get("and not result") == Fr::zero());
1824 assert_eq!(v.value, Some(false));
1825 },
1826 (
1827 OperandType::NegatedAllocatedTrue,
1828 OperandType::NegatedAllocatedTrue,
1829 Boolean::Is(ref v),
1830 ) => {
1831 assert!(cs.get("nor result") == Fr::zero());
1832 assert_eq!(v.value, Some(false));
1833 },
1834 (
1835 OperandType::NegatedAllocatedTrue,
1836 OperandType::NegatedAllocatedFalse,
1837 Boolean::Is(ref v),
1838 ) => {
1839 assert!(cs.get("nor result") == Fr::zero());
1840 assert_eq!(v.value, Some(false));
1841 },
1842
1843 (OperandType::NegatedAllocatedFalse, OperandType::True, Boolean::Not(_)) => {},
1844 (
1845 OperandType::NegatedAllocatedFalse,
1846 OperandType::False,
1847 Boolean::Constant(false),
1848 ) => {},
1849 (
1850 OperandType::NegatedAllocatedFalse,
1851 OperandType::AllocatedTrue,
1852 Boolean::Is(ref v),
1853 ) => {
1854 assert!(cs.get("and not result") == Fr::one());
1855 assert_eq!(v.value, Some(true));
1856 },
1857 (
1858 OperandType::NegatedAllocatedFalse,
1859 OperandType::AllocatedFalse,
1860 Boolean::Is(ref v),
1861 ) => {
1862 assert!(cs.get("and not result") == Fr::zero());
1863 assert_eq!(v.value, Some(false));
1864 },
1865 (
1866 OperandType::NegatedAllocatedFalse,
1867 OperandType::NegatedAllocatedTrue,
1868 Boolean::Is(ref v),
1869 ) => {
1870 assert!(cs.get("nor result") == Fr::zero());
1871 assert_eq!(v.value, Some(false));
1872 },
1873 (
1874 OperandType::NegatedAllocatedFalse,
1875 OperandType::NegatedAllocatedFalse,
1876 Boolean::Is(ref v),
1877 ) => {
1878 assert!(cs.get("nor result") == Fr::one());
1879 assert_eq!(v.value, Some(true));
1880 },
1881
1882 _ => {
1883 panic!(
1884 "unexpected behavior at {:?} AND {:?}",
1885 first_operand, second_operand
1886 );
1887 },
1888 }
1889 }
1890 }
1891 }
1892
1893 #[test]
1894 fn test_enforce_in_field() {
1895 {
1896 let mut cs = TestConstraintSystem::<Fr>::new();
1897
1898 let mut bits = vec![];
1899 for (i, b) in BitIterator::new(Fr::characteristic()).skip(1).enumerate() {
1900 bits.push(Boolean::from(
1901 AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}", i)), || Ok(b)).unwrap(),
1902 ));
1903 }
1904
1905 Boolean::enforce_in_field::<_, _, Fr>(&mut cs, &bits).unwrap();
1906
1907 assert!(!cs.is_satisfied());
1908 }
1909
1910 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1911
1912 for _ in 0..1000 {
1913 let r = Fr::rand(&mut rng);
1914 let mut cs = TestConstraintSystem::<Fr>::new();
1915
1916 let mut bits = vec![];
1917 for (i, b) in BitIterator::new(r.into_repr()).skip(1).enumerate() {
1918 bits.push(Boolean::from(
1919 AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}", i)), || Ok(b)).unwrap(),
1920 ));
1921 }
1922
1923 Boolean::enforce_in_field::<_, _, Fr>(&mut cs, &bits).unwrap();
1924
1925 assert!(cs.is_satisfied());
1926 }
1927
1928 // for _ in 0..1000 {
1929 // // Sample a random element not in the field
1930 // let r = loop {
1931 // let mut a = Fr::rand(&mut rng).into_repr();
1932 // let b = Fr::rand(&mut rng).into_repr();
1933
1934 // a.add_nocarry(&b);
1935 // // we're shaving off the high bit_gadget later
1936 // a.as_mut()[3] &= 0x7fffffffffffffff;
1937 // if Fr::from_repr(a).is_err() {
1938 // break a;
1939 // }
1940 // };
1941
1942 // let mut cs = TestConstraintSystem::<Fr>::new();
1943
1944 // let mut bits = vec![];
1945 // for (i, b) in BitIterator::new(r).skip(1).enumerate() {
1946 // bits.push(Boolean::from(
1947 // AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}",
1948 // i)), Some(b)) .unwrap(),
1949 // ));
1950 // }
1951
1952 // Boolean::enforce_in_field::<_, _, Fr>(&mut cs, &bits).unwrap();
1953
1954 // assert!(!cs.is_satisfied());
1955 // }
1956 }
1957
1958 #[test]
1959 fn test_enforce_nand() {
1960 {
1961 let mut cs = TestConstraintSystem::<Fr>::new();
1962
1963 assert!(Boolean::enforce_nand(&mut cs, &[Boolean::constant(false)]).is_ok());
1964 assert!(Boolean::enforce_nand(&mut cs, &[Boolean::constant(true)]).is_err());
1965 }
1966
1967 for i in 1..5 {
1968 // with every possible assignment for them
1969 for mut b in 0..(1 << i) {
1970 // with every possible negation
1971 for mut n in 0..(1 << i) {
1972 let mut cs = TestConstraintSystem::<Fr>::new();
1973
1974 let mut expected = true;
1975
1976 let mut bits = vec![];
1977 for j in 0..i {
1978 expected &= b & 1 == 1;
1979
1980 if n & 1 == 1 {
1981 bits.push(Boolean::from(
1982 AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}", j)), || {
1983 Ok(b & 1 == 1)
1984 })
1985 .unwrap(),
1986 ));
1987 } else {
1988 bits.push(
1989 Boolean::from(
1990 AllocatedBit::alloc(
1991 cs.ns(|| format!("bit_gadget {}", j)),
1992 || Ok(b & 1 == 0),
1993 )
1994 .unwrap(),
1995 )
1996 .not(),
1997 );
1998 }
1999
2000 b >>= 1;
2001 n >>= 1;
2002 }
2003
2004 let expected = !expected;
2005
2006 Boolean::enforce_nand(&mut cs, &bits).unwrap();
2007
2008 if expected {
2009 assert!(cs.is_satisfied());
2010 } else {
2011 assert!(!cs.is_satisfied());
2012 }
2013 }
2014 }
2015 }
2016 }
2017
2018 #[test]
2019 fn test_kary_and() {
2020 // test different numbers of operands
2021 for i in 1..15 {
2022 // with every possible assignment for them
2023 for mut b in 0..(1 << i) {
2024 let mut cs = TestConstraintSystem::<Fr>::new();
2025
2026 let mut expected = true;
2027
2028 let mut bits = vec![];
2029 for j in 0..i {
2030 expected &= b & 1 == 1;
2031
2032 bits.push(Boolean::from(
2033 AllocatedBit::alloc(cs.ns(|| format!("bit_gadget {}", j)), || {
2034 Ok(b & 1 == 1)
2035 })
2036 .unwrap(),
2037 ));
2038 b >>= 1;
2039 }
2040
2041 let r = Boolean::kary_and(&mut cs, &bits).unwrap();
2042
2043 assert!(cs.is_satisfied());
2044
2045 match r {
2046 Boolean::Is(ref r) => {
2047 assert_eq!(r.value.unwrap(), expected);
2048 },
2049 _ => unreachable!(),
2050 }
2051 }
2052 }
2053 }
2054}