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