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