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