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