ark-r1cs-std/r1cs-std/src/bits/boolean.rs
r1cs-std/src/bits/boolean.rsRaw
1use algebra::{BitIteratorBE, Field};
2
3use crate::{prelude::*, Assignment, Vec};
4use core::borrow::Borrow;
5use r1cs_core::{lc, ConstraintSystemRef, LinearCombination, Namespace, SynthesisError, Variable};
6
7/// Represents a variable in the constraint system which is guaranteed
8/// to be either zero or one.
9#[derive(Clone, Debug, Eq, PartialEq)]
10pub struct AllocatedBit<F: Field> {
11 variable: Variable,
12 cs: ConstraintSystemRef<F>,
13}
14
15pub(crate) fn bool_to_field<F: Field>(val: impl Borrow<bool>) -> F {
16 if *val.borrow() {
17 F::one()
18 } else {
19 F::zero()
20 }
21}
22
23impl<F: Field> AllocatedBit<F> {
24 /// Get the assigned value for `self`.
25 pub fn value(&self) -> Result<bool, SynthesisError> {
26 let value = self.cs.assigned_value(self.variable).get()?;
27 if value.is_zero() {
28 Ok(false)
29 } else if value.is_one() {
30 Ok(true)
31 } else {
32 unreachable!("Incorrect value assigned: {:?}", value);
33 }
34 }
35
36 /// Get the R1CS variable for `self`.
37 pub fn variable(&self) -> Variable {
38 self.variable
39 }
40
41 /// Allocate a witness variable without a booleanity check.
42 fn new_witness_without_booleanity_check<T: Borrow<bool>>(
43 cs: ConstraintSystemRef<F>,
44 f: impl FnOnce() -> Result<T, SynthesisError>,
45 ) -> Result<Self, SynthesisError> {
46 let variable = cs.new_witness_variable(|| f().map(bool_to_field))?;
47 Ok(Self { variable, cs })
48 }
49
50 /// Performs an XOR operation over the two operands, returning
51 /// an `AllocatedBit`.
52 pub fn xor(&self, b: &Self) -> Result<Self, SynthesisError> {
53 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
54 Ok(self.value()? ^ b.value()?)
55 })?;
56
57 // Constrain (a + a) * (b) = (a + b - c)
58 // Given that a and b are boolean constrained, if they
59 // are equal, the only solution for c is 0, and if they
60 // are different, the only solution for c is 1.
61 //
62 // ¬(a ∧ b) ∧ ¬(¬a ∧ ¬b) = c
63 // (1 - (a * b)) * (1 - ((1 - a) * (1 - b))) = c
64 // (1 - ab) * (1 - (1 - a - b + ab)) = c
65 // (1 - ab) * (a + b - ab) = c
66 // a + b - ab - (a^2)b - (b^2)a + (a^2)(b^2) = c
67 // a + b - ab - ab - ab + ab = c
68 // a + b - 2ab = c
69 // -2a * b = c - a - b
70 // 2a * b = a + b - c
71 // (a + a) * b = a + b - c
72 self.cs.enforce_constraint(
73 lc!() + self.variable + self.variable,
74 lc!() + b.variable,
75 lc!() + self.variable + b.variable - result.variable,
76 )?;
77
78 Ok(result)
79 }
80
81 /// Performs an AND operation over the two operands, returning
82 /// an `AllocatedBit`.
83 pub fn and(&self, b: &Self) -> Result<Self, SynthesisError> {
84 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
85 Ok(self.value()? & b.value()?)
86 })?;
87
88 // Constrain (a) * (b) = (c), ensuring c is 1 iff
89 // a AND b are both 1.
90 self.cs.enforce_constraint(
91 lc!() + self.variable,
92 lc!() + b.variable,
93 lc!() + result.variable,
94 )?;
95
96 Ok(result)
97 }
98
99 /// Performs an OR operation over the two operands, returning
100 /// an `AllocatedBit`.
101 pub fn or(&self, b: &Self) -> Result<Self, SynthesisError> {
102 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
103 Ok(self.value()? | b.value()?)
104 })?;
105
106 // Constrain (1 - a) * (1 - b) = (c), ensuring c is 1 iff
107 // a and b are both false, and otherwise c is 0.
108 self.cs.enforce_constraint(
109 lc!() + Variable::One - self.variable,
110 lc!() + Variable::One - b.variable,
111 lc!() + Variable::One - result.variable,
112 )?;
113
114 Ok(result)
115 }
116
117 /// Calculates `a AND (NOT b)`.
118 pub fn and_not(&self, b: &Self) -> Result<Self, SynthesisError> {
119 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
120 Ok(self.value()? & !b.value()?)
121 })?;
122
123 // Constrain (a) * (1 - b) = (c), ensuring c is 1 iff
124 // a is true and b is false, and otherwise c is 0.
125 self.cs.enforce_constraint(
126 lc!() + self.variable,
127 lc!() + Variable::One - b.variable,
128 lc!() + result.variable,
129 )?;
130
131 Ok(result)
132 }
133
134 /// Calculates `(NOT a) AND (NOT b)`.
135 pub fn nor(&self, b: &Self) -> Result<Self, SynthesisError> {
136 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
137 Ok(!(self.value()? | b.value()?))
138 })?;
139
140 // Constrain (1 - a) * (1 - b) = (c), ensuring c is 1 iff
141 // a and b are both false, and otherwise c is 0.
142 self.cs.enforce_constraint(
143 lc!() + Variable::One - self.variable,
144 lc!() + Variable::One - b.variable,
145 lc!() + result.variable,
146 )?;
147
148 Ok(result)
149 }
150}
151
152impl<F: Field> AllocVar<bool, F> for AllocatedBit<F> {
153 /// If `self.mode` == `AllocationMode::Constant`, this method simply outputs
154 /// a `Boolean::Constant`.
155 ///
156 /// Otherwise, it produces a new variable of the appropriate type
157 /// (instance or witness), with a booleanity check.
158 ///
159 /// N.B.: we could omit the booleanity check when allocating `self`
160 /// as a new public input, but that places an additional burden on
161 /// protocol designers. Better safe than sorry!
162 fn new_variable<T: Borrow<bool>>(
163 cs: impl Into<Namespace<F>>,
164 f: impl FnOnce() -> Result<T, SynthesisError>,
165 mode: AllocationMode,
166 ) -> Result<Self, SynthesisError> {
167 let ns = cs.into();
168 let cs = ns.cs();
169 if mode == AllocationMode::Constant {
170 let variable = if *f()?.borrow() {
171 Variable::One
172 } else {
173 Variable::Zero
174 };
175 Ok(Self { variable, cs })
176 } else {
177 let variable = if mode == AllocationMode::Input {
178 cs.new_input_variable(|| f().map(bool_to_field))?
179 } else {
180 cs.new_witness_variable(|| f().map(bool_to_field))?
181 };
182
183 // Constrain: (1 - a) * a = 0
184 // This constrains a to be either 0 or 1.
185
186 cs.enforce_named_constraint(
187 "Booleanity check",
188 lc!() + Variable::One - variable,
189 lc!() + variable,
190 lc!(),
191 )?;
192
193 Ok(Self { variable, cs })
194 }
195 }
196}
197
198impl<F: Field> CondSelectGadget<F> for AllocatedBit<F> {
199 fn conditionally_select(
200 cond: &Boolean<F>,
201 true_val: &Self,
202 false_val: &Self,
203 ) -> Result<Self, SynthesisError> {
204 let res = Boolean::conditionally_select(
205 cond,
206 &true_val.clone().into(),
207 &false_val.clone().into(),
208 )?;
209 match res {
210 Boolean::Is(a) => Ok(a),
211 _ => unreachable!("Impossible"),
212 }
213 }
214}
215
216/// This is a boolean value which may be either a constant or
217/// an interpretation of an `AllocatedBit`.
218#[derive(Clone, Debug, Eq, PartialEq)]
219pub enum Boolean<F: Field> {
220 /// Existential view of the boolean variable
221 Is(AllocatedBit<F>),
222 /// Negated view of the boolean variable
223 Not(AllocatedBit<F>),
224 /// Constant (not an allocated variable)
225 Constant(bool),
226}
227
228impl<F: Field> R1CSVar<F> for Boolean<F> {
229 type Value = bool;
230
231 fn cs(&self) -> Option<ConstraintSystemRef<F>> {
232 match self {
233 Self::Is(a) | Self::Not(a) => Some(a.cs.clone()),
234 _ => None,
235 }
236 }
237
238 fn value(&self) -> Result<Self::Value, SynthesisError> {
239 match self {
240 Boolean::Constant(c) => Ok(*c),
241 Boolean::Is(ref v) => v.value(),
242 Boolean::Not(ref v) => v.value().map(|b| !b),
243 }
244 }
245}
246
247impl<F: Field> Boolean<F> {
248 pub fn lc(&self) -> LinearCombination<F> {
249 match self {
250 Boolean::Constant(false) => lc!(),
251 Boolean::Constant(true) => lc!() + Variable::One,
252 Boolean::Is(v) => v.variable().into(),
253 Boolean::Not(v) => lc!() + Variable::One - v.variable(),
254 }
255 }
256
257 /// Construct a boolean vector from a vector of u8
258 pub fn constant_vec_from_bytes(values: &[u8]) -> Vec<Self> {
259 let mut input_bits = vec![];
260 for input_byte in values {
261 for bit_i in (0..8).rev() {
262 input_bits.push(Self::Constant(((input_byte >> bit_i) & 1u8) == 1u8));
263 }
264 }
265 input_bits
266 }
267
268 /// Construct a boolean from a known constant
269 pub fn constant(b: bool) -> Self {
270 Boolean::Constant(b)
271 }
272
273 /// Return a negated interpretation of this boolean.
274 pub fn not(&self) -> Self {
275 match *self {
276 Boolean::Constant(c) => Boolean::Constant(!c),
277 Boolean::Is(ref v) => Boolean::Not(v.clone()),
278 Boolean::Not(ref v) => Boolean::Is(v.clone()),
279 }
280 }
281}
282impl<F: Field> Boolean<F> {
283 /// Perform XOR over two boolean operands
284 pub fn xor<'a>(&'a self, b: &'a Self) -> Result<Self, SynthesisError> {
285 use Boolean::*;
286 match (self, b) {
287 (&Constant(false), x) | (x, &Constant(false)) => Ok(x.clone()),
288 (&Constant(true), x) | (x, &Constant(true)) => Ok(x.not()),
289 // a XOR (NOT b) = NOT(a XOR b)
290 (is @ &Is(_), not @ &Not(_)) | (not @ &Not(_), is @ &Is(_)) => {
291 Ok(is.xor(¬.not())?.not())
292 }
293 // a XOR b = (NOT a) XOR (NOT b)
294 (&Is(ref a), &Is(ref b)) | (&Not(ref a), &Not(ref b)) => Ok(Is(a.xor(b)?)),
295 }
296 }
297
298 /// Perform OR over two boolean operands
299 pub fn or<'a>(&'a self, b: &'a Self) -> Result<Self, SynthesisError> {
300 use Boolean::*;
301 match (self, b) {
302 (&Constant(false), x) | (x, &Constant(false)) => Ok(x.clone()),
303 (&Constant(true), _) | (_, &Constant(true)) => Ok(Constant(true)),
304 // a OR b = NOT ((NOT a) AND b)
305 (a @ &Is(_), b @ &Not(_)) | (b @ &Not(_), a @ &Is(_)) | (b @ &Not(_), a @ &Not(_)) => {
306 Ok(a.not().and(&b.not())?.not())
307 }
308 (&Is(ref a), &Is(ref b)) => a.or(b).map(From::from),
309 }
310 }
311
312 /// Perform AND over two boolean operands
313 pub fn and<'a>(&'a self, b: &'a Self) -> Result<Self, SynthesisError> {
314 use Boolean::*;
315 match (self, b) {
316 // false AND x is always false
317 (&Constant(false), _) | (_, &Constant(false)) => Ok(Constant(false)),
318 // true AND x is always x
319 (&Constant(true), x) | (x, &Constant(true)) => Ok(x.clone()),
320 // a AND (NOT b)
321 (&Is(ref is), &Not(ref not)) | (&Not(ref not), &Is(ref is)) => Ok(Is(is.and_not(not)?)),
322 // (NOT a) AND (NOT b) = a NOR b
323 (&Not(ref a), &Not(ref b)) => Ok(Is(a.nor(b)?)),
324 // a AND b
325 (&Is(ref a), &Is(ref b)) => Ok(Is(a.and(b)?)),
326 }
327 }
328
329 pub fn kary_and(bits: &[Self]) -> Result<Self, SynthesisError> {
330 assert!(!bits.is_empty());
331 let mut cur: Option<Self> = None;
332 for next in bits {
333 cur = if let Some(b) = cur {
334 Some(b.and(next)?)
335 } else {
336 Some(next.clone())
337 };
338 }
339
340 Ok(cur.expect("should not be 0"))
341 }
342
343 pub fn kary_or(bits: &[Self]) -> Result<Self, SynthesisError> {
344 assert!(!bits.is_empty());
345 let mut cur: Option<Self> = None;
346 for next in bits {
347 cur = if let Some(b) = cur {
348 Some(b.or(next)?)
349 } else {
350 Some(next.clone())
351 };
352 }
353
354 Ok(cur.expect("should not be 0"))
355 }
356
357 pub fn kary_nand(bits: &[Self]) -> Result<Self, SynthesisError> {
358 Ok(Self::kary_and(bits)?.not())
359 }
360
361 /// Assert that at least one input is false.
362 fn enforce_kary_nand(bits: &[Self]) -> Result<(), SynthesisError> {
363 use Boolean::*;
364 let r = Self::kary_nand(bits)?;
365 match r {
366 Constant(true) => Ok(()),
367 Constant(false) => Err(SynthesisError::AssignmentMissing),
368 Is(_) | Not(_) => r.cs().unwrap().enforce_constraint(
369 r.lc(),
370 lc!() + Variable::One,
371 lc!() + Variable::One,
372 ),
373 }
374 }
375
376 /// Enforces that `bits`, when interpreted as a integer, is less than `F::characteristic()`,
377 /// That is, interpret bits as a little-endian integer, and enforce that this integer
378 /// is "in the field F".
379 pub fn enforce_in_field_le(bits: &[Self]) -> Result<(), SynthesisError> {
380 // `bits` < F::characteristic() <==> `bits` <= F::characteristic() -1
381 let mut b = F::characteristic().to_vec();
382 assert_eq!(b[0] % 2, 1);
383 b[0] -= 1; // This works, because the LSB is one, so there's no borrows.
384 let run = Self::enforce_smaller_or_equal_than_le(bits, b)?;
385
386 // We should always end in a "run" of zeros, because
387 // the characteristic is an odd prime. So, this should
388 // be empty.
389 assert!(run.is_empty());
390
391 Ok(())
392 }
393
394 /// Enforces that `bits` is less than or equal to `element`,
395 /// when both are interpreted as (little-endian) integers.
396 pub fn enforce_smaller_or_equal_than_le<'a>(
397 bits: &[Self],
398 element: impl AsRef<[u64]>,
399 ) -> Result<Vec<Self>, SynthesisError> {
400 let b: &[u64] = element.as_ref();
401
402 let mut bits_iter = bits.iter().rev(); // Iterate in big-endian
403
404 // Runs of ones in r
405 let mut last_run = Boolean::constant(true);
406 let mut current_run = vec![];
407
408 let mut element_num_bits = 0;
409 for _ in BitIteratorBE::without_leading_zeros(b) {
410 element_num_bits += 1;
411 }
412
413 if bits.len() > element_num_bits {
414 let mut or_result = Boolean::constant(false);
415 for should_be_zero in &bits[element_num_bits..] {
416 or_result = or_result.or(should_be_zero)?;
417 let _ = bits_iter.next().unwrap();
418 }
419 or_result.enforce_equal(&Boolean::constant(false))?;
420 }
421
422 for (b, a) in BitIteratorBE::without_leading_zeros(b).zip(bits_iter.by_ref()) {
423 if b {
424 // This is part of a run of ones.
425 current_run.push(a.clone());
426 } else {
427 if !current_run.is_empty() {
428 // This is the start of a run of zeros, but we need
429 // to k-ary AND against `last_run` first.
430
431 current_run.push(last_run.clone());
432 last_run = Self::kary_and(¤t_run)?;
433 current_run.truncate(0);
434 }
435
436 // If `last_run` is true, `a` must be false, or it would
437 // not be in the field.
438 //
439 // If `last_run` is false, `a` can be true or false.
440 //
441 // Ergo, at least one of `last_run` and `a` must be false.
442 Self::enforce_kary_nand(&[last_run.clone(), a.clone()])?;
443 }
444 }
445 assert!(bits_iter.next().is_none());
446
447 Ok(current_run)
448 }
449
450 pub fn select<T: CondSelectGadget<F>>(
451 &self,
452 first: &T,
453 second: &T,
454 ) -> Result<T, SynthesisError> {
455 T::conditionally_select(&self, first, second)
456 }
457}
458
459impl<F: Field> From<AllocatedBit<F>> for Boolean<F> {
460 fn from(b: AllocatedBit<F>) -> Self {
461 Boolean::Is(b)
462 }
463}
464
465impl<F: Field> AllocVar<bool, F> for Boolean<F> {
466 fn new_variable<T: Borrow<bool>>(
467 cs: impl Into<Namespace<F>>,
468 f: impl FnOnce() -> Result<T, SynthesisError>,
469 mode: AllocationMode,
470 ) -> Result<Self, SynthesisError> {
471 if mode == AllocationMode::Constant {
472 Ok(Boolean::Constant(*f()?.borrow()))
473 } else {
474 AllocatedBit::new_variable(cs, f, mode).map(Boolean::from)
475 }
476 }
477}
478
479impl<F: Field> EqGadget<F> for Boolean<F> {
480 fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
481 // self | other | XNOR(self, other) | self == other
482 // -----|-------|-------------------|--------------
483 // 0 | 0 | 1 | 1
484 // 0 | 1 | 0 | 0
485 // 1 | 0 | 0 | 0
486 // 1 | 1 | 1 | 1
487 Ok(self.xor(other)?.not())
488 }
489
490 fn conditional_enforce_equal(
491 &self,
492 other: &Self,
493 condition: &Boolean<F>,
494 ) -> Result<(), SynthesisError> {
495 use Boolean::*;
496 let one = Variable::One;
497 let difference = match (self, other) {
498 // 1 == 1; 0 == 0
499 (Constant(true), Constant(true)) | (Constant(false), Constant(false)) => return Ok(()),
500 // false != true
501 (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
502 // 1 - a
503 (Constant(true), Is(a)) | (Is(a), Constant(true)) => lc!() + one - a.variable(),
504 // a - 0 = a
505 (Constant(false), Is(a)) | (Is(a), Constant(false)) => lc!() + a.variable(),
506 // 1 - !a = 1 - (1 - a) = a
507 (Constant(true), Not(a)) | (Not(a), Constant(true)) => lc!() + a.variable(),
508 // !a - 0 = !a = 1 - a
509 (Constant(false), Not(a)) | (Not(a), Constant(false)) => lc!() + one - a.variable(),
510 // b - a,
511 (Is(a), Is(b)) => lc!() + b.variable() - a.variable(),
512 // !b - a = (1 - b) - a
513 (Is(a), Not(b)) | (Not(b), Is(a)) => lc!() + one - b.variable() - a.variable(),
514 // !b - !a = (1 - b) - (1 - a) = a - b,
515 (Not(a), Not(b)) => lc!() + a.variable() - b.variable(),
516 };
517
518 if condition != &Constant(false) {
519 let cs = self.cs().or(other.cs()).or(condition.cs()).unwrap();
520 cs.enforce_constraint(lc!() + difference, condition.lc(), lc!())?;
521 }
522 Ok(())
523 }
524
525 fn conditional_enforce_not_equal(
526 &self,
527 other: &Self,
528 should_enforce: &Boolean<F>,
529 ) -> Result<(), SynthesisError> {
530 use Boolean::*;
531 let one = Variable::One;
532 let difference = match (self, other) {
533 // 1 != 0; 0 != 1
534 (Constant(true), Constant(false)) | (Constant(false), Constant(true)) => return Ok(()),
535 // false == false and true == true
536 (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
537 // 1 - a
538 (Constant(true), Is(a)) | (Is(a), Constant(true)) => lc!() + one - a.variable(),
539 // a - 0 = a
540 (Constant(false), Is(a)) | (Is(a), Constant(false)) => lc!() + a.variable(),
541 // 1 - !a = 1 - (1 - a) = a
542 (Constant(true), Not(a)) | (Not(a), Constant(true)) => lc!() + a.variable(),
543 // !a - 0 = !a = 1 - a
544 (Constant(false), Not(a)) | (Not(a), Constant(false)) => lc!() + one - a.variable(),
545 // b - a,
546 (Is(a), Is(b)) => lc!() + b.variable() - a.variable(),
547 // !b - a = (1 - b) - a
548 (Is(a), Not(b)) | (Not(b), Is(a)) => lc!() + one - b.variable() - a.variable(),
549 // !b - !a = (1 - b) - (1 - a) = a - b,
550 (Not(a), Not(b)) => lc!() + a.variable() - b.variable(),
551 };
552
553 if should_enforce != &Constant(false) {
554 let cs = self
555 .cs()
556 .or(other.cs())
557 .or(should_enforce.cs())
558 .ok_or(SynthesisError::UnconstrainedVariable)?;
559 cs.enforce_constraint(difference, should_enforce.lc(), should_enforce.lc())?;
560 }
561 Ok(())
562 }
563}
564
565impl<F: Field> ToBytesGadget<F> for Boolean<F> {
566 /// Outputs `1u8` if `self` is true, and `0u8` otherwise.
567 fn to_bytes(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
568 let mut bits = vec![self.clone()];
569 bits.extend(vec![Boolean::constant(false); 7]);
570 let value = self.value().map(|val| val as u8).ok();
571 let byte = UInt8 { bits, value };
572 Ok(vec![byte])
573 }
574}
575
576impl<F: Field> CondSelectGadget<F> for Boolean<F> {
577 fn conditionally_select(
578 cond: &Boolean<F>,
579 true_val: &Self,
580 false_val: &Self,
581 ) -> Result<Self, SynthesisError> {
582 use Boolean::*;
583 match cond {
584 Constant(true) => Ok(true_val.clone()),
585 Constant(false) => Ok(false_val.clone()),
586 cond @ Not(_) => Self::conditionally_select(&cond.not(), false_val, true_val),
587 cond @ Is(_) => match (true_val, false_val) {
588 (x, &Constant(false)) => cond.and(x),
589 (&Constant(false), x) => cond.not().and(x),
590 (&Constant(true), x) => cond.or(x),
591 (x, &Constant(true)) => cond.not().or(x),
592 (a, b) => {
593 let cs = cond.cs().unwrap();
594 let result: Boolean<F> =
595 AllocatedBit::new_witness_without_booleanity_check(cs.clone(), || {
596 let cond = cond.value()?;
597 Ok(if cond { a.value()? } else { b.value()? })
598 })?
599 .into();
600 //
601 // a = self; b = other; c = cond;
602 //
603 // r = c * a + (1 - c) * b
604 // r = b + c * (a - b)
605 // c * (a - b) = r - b
606 //
607 // If a, b, cond are all boolean, so is r.
608 //
609 // self | other | cond | result
610 // -----|-------|----------------
611 // 0 | 0 | 1 | 0
612 // 0 | 1 | 1 | 0
613 // 1 | 0 | 1 | 1
614 // 1 | 1 | 1 | 1
615 // 0 | 0 | 0 | 0
616 // 0 | 1 | 0 | 1
617 // 1 | 0 | 0 | 0
618 // 1 | 1 | 0 | 1
619 cs.enforce_constraint(
620 cond.lc(),
621 lc!() + a.lc() - b.lc(),
622 lc!() + result.lc() - b.lc(),
623 )?;
624
625 Ok(result)
626 }
627 },
628 }
629 }
630}
631
632#[cfg(test)]
633mod test {
634 use super::{AllocatedBit, Boolean};
635 use crate::prelude::*;
636 use algebra::{
637 bls12_381::Fr, BitIteratorBE, BitIteratorLE, Field, One, PrimeField, UniformRand, Zero,
638 };
639 use r1cs_core::{ConstraintSystem, Namespace, SynthesisError};
640 use rand::SeedableRng;
641 use rand_xorshift::XorShiftRng;
642
643 #[test]
644 fn test_boolean_to_byte() -> Result<(), SynthesisError> {
645 for val in [true, false].iter() {
646 let cs = ConstraintSystem::<Fr>::new_ref();
647 let a = Boolean::new_witness(cs.clone(), || Ok(*val))?;
648 let bytes = a.to_bytes()?;
649 assert_eq!(bytes.len(), 1);
650 let byte = &bytes[0];
651 assert_eq!(byte.value()?, *val as u8);
652
653 for (i, bit) in byte.bits.iter().enumerate() {
654 assert_eq!(bit.value()?, (byte.value()? >> i) & 1 == 1);
655 }
656 }
657 Ok(())
658 }
659
660 #[test]
661 fn test_xor() -> Result<(), SynthesisError> {
662 for a_val in [false, true].iter().copied() {
663 for b_val in [false, true].iter().copied() {
664 let cs = ConstraintSystem::<Fr>::new_ref();
665 let a = AllocatedBit::new_witness(cs.ns("a"), || Ok(a_val))?;
666 let b = AllocatedBit::new_witness(cs.ns("b"), || Ok(b_val))?;
667 let c = AllocatedBit::xor(&a, &b)?;
668 assert_eq!(c.value()?, a_val ^ b_val);
669
670 assert!(cs.is_satisfied().unwrap());
671 assert_eq!(a.value()?, (a_val));
672 assert_eq!(b.value()?, (b_val));
673 assert_eq!(c.value()?, (a_val ^ b_val));
674 }
675 }
676 Ok(())
677 }
678
679 #[test]
680 fn test_or() -> Result<(), SynthesisError> {
681 for a_val in [false, true].iter().copied() {
682 for b_val in [false, true].iter().copied() {
683 let cs = ConstraintSystem::<Fr>::new_ref();
684 let a = AllocatedBit::new_witness(cs.ns("a"), || Ok(a_val))?;
685 let b = AllocatedBit::new_witness(cs.ns("b"), || Ok(b_val))?;
686 let c = AllocatedBit::or(&a, &b)?;
687 assert_eq!(c.value()?, a_val | b_val);
688
689 assert!(cs.is_satisfied().unwrap());
690 assert_eq!(a.value()?, (a_val));
691 assert_eq!(b.value()?, (b_val));
692 assert_eq!(c.value()?, (a_val | b_val));
693 }
694 }
695 Ok(())
696 }
697
698 #[test]
699 fn test_and() -> Result<(), SynthesisError> {
700 for a_val in [false, true].iter().copied() {
701 for b_val in [false, true].iter().copied() {
702 let cs = ConstraintSystem::<Fr>::new_ref();
703 let a = AllocatedBit::new_witness(cs.ns("a"), || Ok(a_val))?;
704 let b = AllocatedBit::new_witness(cs.ns("b"), || Ok(b_val))?;
705 let c = AllocatedBit::and(&a, &b)?;
706 assert_eq!(c.value()?, a_val & b_val);
707
708 assert!(cs.is_satisfied().unwrap());
709 assert_eq!(a.value()?, (a_val));
710 assert_eq!(b.value()?, (b_val));
711 assert_eq!(c.value()?, (a_val & b_val));
712 }
713 }
714 Ok(())
715 }
716
717 #[test]
718 fn test_and_not() -> Result<(), SynthesisError> {
719 for a_val in [false, true].iter().copied() {
720 for b_val in [false, true].iter().copied() {
721 let cs = ConstraintSystem::<Fr>::new_ref();
722 let a = AllocatedBit::new_witness(cs.ns("a"), || Ok(a_val))?;
723 let b = AllocatedBit::new_witness(cs.ns("b"), || Ok(b_val))?;
724 let c = AllocatedBit::and_not(&a, &b)?;
725 assert_eq!(c.value()?, a_val & !b_val);
726
727 assert!(cs.is_satisfied().unwrap());
728 assert_eq!(a.value()?, (a_val));
729 assert_eq!(b.value()?, (b_val));
730 assert_eq!(c.value()?, (a_val & !b_val));
731 }
732 }
733 Ok(())
734 }
735
736 #[test]
737 fn test_nor() -> Result<(), SynthesisError> {
738 for a_val in [false, true].iter().copied() {
739 for b_val in [false, true].iter().copied() {
740 let cs = ConstraintSystem::<Fr>::new_ref();
741 let a = AllocatedBit::new_witness(cs.ns("a"), || Ok(a_val))?;
742 let b = AllocatedBit::new_witness(cs.ns("b"), || Ok(b_val))?;
743 let c = AllocatedBit::nor(&a, &b)?;
744 assert_eq!(c.value()?, !a_val & !b_val);
745
746 assert!(cs.is_satisfied().unwrap());
747 assert_eq!(a.value()?, (a_val));
748 assert_eq!(b.value()?, (b_val));
749 assert_eq!(c.value()?, (!a_val & !b_val));
750 }
751 }
752 Ok(())
753 }
754
755 #[test]
756 fn test_enforce_equal() -> Result<(), SynthesisError> {
757 for a_bool in [false, true].iter().cloned() {
758 for b_bool in [false, true].iter().cloned() {
759 for a_neg in [false, true].iter().cloned() {
760 for b_neg in [false, true].iter().cloned() {
761 let cs = ConstraintSystem::<Fr>::new_ref();
762
763 let mut a = Boolean::new_witness(cs.ns("a"), || Ok(a_bool))?;
764 let mut b = Boolean::new_witness(cs.ns("b"), || Ok(b_bool))?;
765
766 if a_neg {
767 a = a.not();
768 }
769 if b_neg {
770 b = b.not();
771 }
772
773 a.enforce_equal(&b)?;
774
775 assert_eq!(
776 cs.is_satisfied().unwrap(),
777 (a_bool ^ a_neg) == (b_bool ^ b_neg)
778 );
779 }
780 }
781 }
782 }
783 Ok(())
784 }
785
786 #[test]
787 fn test_conditional_enforce_equal() -> Result<(), SynthesisError> {
788 for a_bool in [false, true].iter().cloned() {
789 for b_bool in [false, true].iter().cloned() {
790 for a_neg in [false, true].iter().cloned() {
791 for b_neg in [false, true].iter().cloned() {
792 let cs = ConstraintSystem::<Fr>::new_ref();
793
794 // First test if constraint system is satisfied
795 // when we do want to enforce the condition.
796 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
797 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
798
799 if a_neg {
800 a = a.not();
801 }
802 if b_neg {
803 b = b.not();
804 }
805
806 a.conditional_enforce_equal(&b, &Boolean::constant(true))?;
807
808 assert_eq!(
809 cs.is_satisfied().unwrap(),
810 (a_bool ^ a_neg) == (b_bool ^ b_neg)
811 );
812
813 // Now test if constraint system is satisfied even
814 // when we don't want to enforce the condition.
815 let cs = ConstraintSystem::<Fr>::new_ref();
816
817 let mut a = Boolean::new_witness(cs.ns("a"), || Ok(a_bool))?;
818 let mut b = Boolean::new_witness(cs.ns("b"), || Ok(b_bool))?;
819
820 if a_neg {
821 a = a.not();
822 }
823 if b_neg {
824 b = b.not();
825 }
826
827 let false_cond = Boolean::new_witness(cs.ns("cond"), || Ok(false))?;
828 a.conditional_enforce_equal(&b, &false_cond)?;
829
830 assert!(cs.is_satisfied().unwrap());
831 }
832 }
833 }
834 }
835 Ok(())
836 }
837
838 #[test]
839 fn test_boolean_negation() -> Result<(), SynthesisError> {
840 let cs = ConstraintSystem::<Fr>::new_ref();
841
842 let mut b = Boolean::new_witness(cs.clone(), || Ok(true))?;
843 assert!(matches!(b, Boolean::Is(_)));
844
845 b = b.not();
846 assert!(matches!(b, Boolean::Not(_)));
847
848 b = b.not();
849 assert!(matches!(b, Boolean::Is(_)));
850
851 b = Boolean::Constant(true);
852 assert!(matches!(b, Boolean::Constant(true)));
853
854 b = b.not();
855 assert!(matches!(b, Boolean::Constant(false)));
856
857 b = b.not();
858 assert!(matches!(b, Boolean::Constant(true)));
859 Ok(())
860 }
861
862 #[derive(Eq, PartialEq, Copy, Clone, Debug)]
863 enum OpType {
864 True,
865 False,
866 AllocatedTrue,
867 AllocatedFalse,
868 NegatedAllocatedTrue,
869 NegatedAllocatedFalse,
870 }
871
872 const VARIANTS: [OpType; 6] = [
873 OpType::True,
874 OpType::False,
875 OpType::AllocatedTrue,
876 OpType::AllocatedFalse,
877 OpType::NegatedAllocatedTrue,
878 OpType::NegatedAllocatedFalse,
879 ];
880
881 fn construct<F: Field>(
882 cs: impl Into<Namespace<F>>,
883 operand: OpType,
884 name: &'static str,
885 ) -> Result<Boolean<F>, SynthesisError> {
886 let ns = cs.into();
887 let cs = ns.cs().ns(name);
888
889 let b = match operand {
890 OpType::True => Boolean::constant(true),
891 OpType::False => Boolean::constant(false),
892 OpType::AllocatedTrue => Boolean::new_witness(cs, || Ok(true))?,
893 OpType::AllocatedFalse => Boolean::new_witness(cs, || Ok(false))?,
894 OpType::NegatedAllocatedTrue => Boolean::new_witness(cs, || Ok(true))?.not(),
895 OpType::NegatedAllocatedFalse => Boolean::new_witness(cs, || Ok(false))?.not(),
896 };
897 Ok(b)
898 }
899
900 #[test]
901 fn test_boolean_xor() -> Result<(), SynthesisError> {
902 for first_operand in VARIANTS.iter().cloned() {
903 for second_operand in VARIANTS.iter().cloned() {
904 let cs = ConstraintSystem::<Fr>::new_ref();
905
906 let a = construct(cs.clone(), first_operand, "a")?;
907 let b = construct(cs.clone(), second_operand, "b")?;
908 let c = Boolean::xor(&a, &b)?;
909
910 assert!(cs.is_satisfied().unwrap());
911
912 match (first_operand, second_operand, c) {
913 (OpType::True, OpType::True, Boolean::Constant(false)) => (),
914 (OpType::True, OpType::False, Boolean::Constant(true)) => (),
915 (OpType::True, OpType::AllocatedTrue, Boolean::Not(_)) => (),
916 (OpType::True, OpType::AllocatedFalse, Boolean::Not(_)) => (),
917 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Is(_)) => (),
918 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Is(_)) => (),
919
920 (OpType::False, OpType::True, Boolean::Constant(true)) => (),
921 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
922 (OpType::False, OpType::AllocatedTrue, Boolean::Is(_)) => (),
923 (OpType::False, OpType::AllocatedFalse, Boolean::Is(_)) => (),
924 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
925 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
926
927 (OpType::AllocatedTrue, OpType::True, Boolean::Not(_)) => (),
928 (OpType::AllocatedTrue, OpType::False, Boolean::Is(_)) => (),
929 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
930 assert_eq!(v.value(), Ok(false));
931 }
932 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
933 assert_eq!(v.value(), Ok(true));
934 }
935 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
936 assert_eq!(v.value(), Ok(false));
937 }
938 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Not(ref v)) => {
939 assert_eq!(v.value(), Ok(true));
940 }
941 (OpType::AllocatedFalse, OpType::True, Boolean::Not(_)) => (),
942 (OpType::AllocatedFalse, OpType::False, Boolean::Is(_)) => (),
943 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
944 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
945 assert_eq!(v.value(), Ok(true));
946 }
947 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
948 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
949 assert_eq!(v.value(), Ok(false));
950 }
951 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
952 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
953 assert_eq!(v.value(), Ok(true));
954 }
955 (
956 OpType::AllocatedFalse,
957 OpType::NegatedAllocatedFalse,
958 Boolean::Not(ref v),
959 ) => {
960 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
961 assert_eq!(v.value(), Ok(false));
962 }
963
964 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Is(_)) => (),
965 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Not(_)) => (),
966 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
967 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
968 assert_eq!(v.value(), Ok(false));
969 }
970 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Not(ref v)) => {
971 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
972 assert_eq!(v.value(), Ok(true));
973 }
974 (
975 OpType::NegatedAllocatedTrue,
976 OpType::NegatedAllocatedTrue,
977 Boolean::Is(ref v),
978 ) => {
979 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
980 assert_eq!(v.value(), Ok(false));
981 }
982 (
983 OpType::NegatedAllocatedTrue,
984 OpType::NegatedAllocatedFalse,
985 Boolean::Is(ref v),
986 ) => {
987 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
988 assert_eq!(v.value(), Ok(true));
989 }
990
991 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Is(_)) => (),
992 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Not(_)) => (),
993 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
994 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
995 assert_eq!(v.value(), Ok(true));
996 }
997 (
998 OpType::NegatedAllocatedFalse,
999 OpType::AllocatedFalse,
1000 Boolean::Not(ref v),
1001 ) => {
1002 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1003 assert_eq!(v.value(), Ok(false));
1004 }
1005 (
1006 OpType::NegatedAllocatedFalse,
1007 OpType::NegatedAllocatedTrue,
1008 Boolean::Is(ref v),
1009 ) => {
1010 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1011 assert_eq!(v.value(), Ok(true));
1012 }
1013 (
1014 OpType::NegatedAllocatedFalse,
1015 OpType::NegatedAllocatedFalse,
1016 Boolean::Is(ref v),
1017 ) => {
1018 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1019 assert_eq!(v.value(), Ok(false));
1020 }
1021
1022 _ => unreachable!(),
1023 }
1024 }
1025 }
1026 Ok(())
1027 }
1028
1029 #[test]
1030 fn test_boolean_cond_select() -> Result<(), SynthesisError> {
1031 for condition in VARIANTS.iter().cloned() {
1032 for first_operand in VARIANTS.iter().cloned() {
1033 for second_operand in VARIANTS.iter().cloned() {
1034 let cs = ConstraintSystem::<Fr>::new_ref();
1035
1036 let cond = construct(cs.clone(), condition, "cond")?;
1037 let a = construct(cs.clone(), first_operand, "a")?;
1038 let b = construct(cs.clone(), second_operand, "b")?;
1039 let c = cond.select(&a, &b)?;
1040
1041 assert!(
1042 cs.is_satisfied().unwrap(),
1043 "failed with operands: cond: {:?}, a: {:?}, b: {:?}",
1044 condition,
1045 first_operand,
1046 second_operand,
1047 );
1048 assert_eq!(
1049 c.value()?,
1050 if cond.value()? {
1051 a.value()?
1052 } else {
1053 b.value()?
1054 }
1055 );
1056 }
1057 }
1058 }
1059 Ok(())
1060 }
1061
1062 #[test]
1063 fn test_boolean_or() -> Result<(), SynthesisError> {
1064 for first_operand in VARIANTS.iter().cloned() {
1065 for second_operand in VARIANTS.iter().cloned() {
1066 let cs = ConstraintSystem::<Fr>::new_ref();
1067
1068 let a = construct(cs.clone(), first_operand, "a")?;
1069 let b = construct(cs.clone(), second_operand, "b")?;
1070 let c = a.or(&b)?;
1071
1072 assert!(cs.is_satisfied().unwrap());
1073
1074 match (first_operand, second_operand, c.clone()) {
1075 (OpType::True, OpType::True, Boolean::Constant(true)) => (),
1076 (OpType::True, OpType::False, Boolean::Constant(true)) => (),
1077 (OpType::True, OpType::AllocatedTrue, Boolean::Constant(true)) => (),
1078 (OpType::True, OpType::AllocatedFalse, Boolean::Constant(true)) => (),
1079 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Constant(true)) => (),
1080 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Constant(true)) => (),
1081
1082 (OpType::False, OpType::True, Boolean::Constant(true)) => (),
1083 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1084 (OpType::False, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1085 (OpType::False, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1086 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1087 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1088
1089 (OpType::AllocatedTrue, OpType::True, Boolean::Constant(true)) => (),
1090 (OpType::AllocatedTrue, OpType::False, Boolean::Is(_)) => (),
1091 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1092 assert_eq!(v.value(), Ok(true));
1093 }
1094 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1095 assert_eq!(v.value(), Ok(true));
1096 }
1097 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1098 assert_eq!(v.value(), Ok(false));
1099 }
1100 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Not(ref v)) => {
1101 assert_eq!(v.value(), Ok(false));
1102 }
1103
1104 (OpType::AllocatedFalse, OpType::True, Boolean::Constant(true)) => (),
1105 (OpType::AllocatedFalse, OpType::False, Boolean::Is(_)) => (),
1106 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1107 assert_eq!(v.value(), Ok(true));
1108 }
1109 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1110 assert_eq!(v.value(), Ok(false));
1111 }
1112 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1113 assert_eq!(v.value(), Ok(true));
1114 }
1115 (
1116 OpType::AllocatedFalse,
1117 OpType::NegatedAllocatedFalse,
1118 Boolean::Not(ref v),
1119 ) => {
1120 assert_eq!(v.value(), Ok(false));
1121 }
1122
1123 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Constant(true)) => (),
1124 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Not(_)) => (),
1125 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1126 assert_eq!(v.value(), Ok(false));
1127 }
1128 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Not(ref v)) => {
1129 assert_eq!(v.value(), Ok(true));
1130 }
1131 (
1132 OpType::NegatedAllocatedTrue,
1133 OpType::NegatedAllocatedTrue,
1134 Boolean::Not(ref v),
1135 ) => {
1136 assert_eq!(v.value(), Ok(true));
1137 }
1138 (
1139 OpType::NegatedAllocatedTrue,
1140 OpType::NegatedAllocatedFalse,
1141 Boolean::Not(ref v),
1142 ) => {
1143 assert_eq!(v.value(), Ok(false));
1144 }
1145
1146 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Constant(true)) => (),
1147 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Not(_)) => (),
1148 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1149 assert_eq!(v.value(), Ok(false));
1150 }
1151 (
1152 OpType::NegatedAllocatedFalse,
1153 OpType::AllocatedFalse,
1154 Boolean::Not(ref v),
1155 ) => {
1156 assert_eq!(v.value(), Ok(false));
1157 }
1158 (
1159 OpType::NegatedAllocatedFalse,
1160 OpType::NegatedAllocatedTrue,
1161 Boolean::Not(ref v),
1162 ) => {
1163 assert_eq!(v.value(), Ok(false));
1164 }
1165 (
1166 OpType::NegatedAllocatedFalse,
1167 OpType::NegatedAllocatedFalse,
1168 Boolean::Not(ref v),
1169 ) => {
1170 assert_eq!(v.value(), Ok(false));
1171 }
1172
1173 _ => panic!(
1174 "this should never be encountered, in case: (a = {:?}, b = {:?}, c = {:?})",
1175 a, b, c
1176 ),
1177 }
1178 }
1179 }
1180 Ok(())
1181 }
1182
1183 #[test]
1184 fn test_boolean_and() -> Result<(), SynthesisError> {
1185 for first_operand in VARIANTS.iter().cloned() {
1186 for second_operand in VARIANTS.iter().cloned() {
1187 let cs = ConstraintSystem::<Fr>::new_ref();
1188
1189 let a = construct(cs.clone(), first_operand, "a")?;
1190 let b = construct(cs.clone(), second_operand, "b")?;
1191 let c = a.and(&b)?;
1192
1193 assert!(cs.is_satisfied().unwrap());
1194
1195 match (first_operand, second_operand, c) {
1196 (OpType::True, OpType::True, Boolean::Constant(true)) => (),
1197 (OpType::True, OpType::False, Boolean::Constant(false)) => (),
1198 (OpType::True, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1199 (OpType::True, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1200 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1201 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1202
1203 (OpType::False, OpType::True, Boolean::Constant(false)) => (),
1204 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1205 (OpType::False, OpType::AllocatedTrue, Boolean::Constant(false)) => (),
1206 (OpType::False, OpType::AllocatedFalse, Boolean::Constant(false)) => (),
1207 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Constant(false)) => (),
1208 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Constant(false)) => (),
1209
1210 (OpType::AllocatedTrue, OpType::True, Boolean::Is(_)) => (),
1211 (OpType::AllocatedTrue, OpType::False, Boolean::Constant(false)) => (),
1212 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1213 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1214 assert_eq!(v.value(), Ok(true));
1215 }
1216 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1217 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1218 assert_eq!(v.value(), Ok(false));
1219 }
1220 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Is(ref v)) => {
1221 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1222 assert_eq!(v.value(), Ok(false));
1223 }
1224 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Is(ref v)) => {
1225 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1226 assert_eq!(v.value(), Ok(true));
1227 }
1228
1229 (OpType::AllocatedFalse, OpType::True, Boolean::Is(_)) => (),
1230 (OpType::AllocatedFalse, OpType::False, Boolean::Constant(false)) => (),
1231 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1232 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1233 assert_eq!(v.value(), Ok(false));
1234 }
1235 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1236 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1237 assert_eq!(v.value(), Ok(false));
1238 }
1239 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Is(ref v)) => {
1240 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1241 assert_eq!(v.value(), Ok(false));
1242 }
1243 (OpType::AllocatedFalse, OpType::NegatedAllocatedFalse, Boolean::Is(ref v)) => {
1244 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1245 assert_eq!(v.value(), Ok(false));
1246 }
1247
1248 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Not(_)) => (),
1249 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Constant(false)) => (),
1250 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1251 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1252 assert_eq!(v.value(), Ok(false));
1253 }
1254 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1255 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1256 assert_eq!(v.value(), Ok(false));
1257 }
1258 (
1259 OpType::NegatedAllocatedTrue,
1260 OpType::NegatedAllocatedTrue,
1261 Boolean::Is(ref v),
1262 ) => {
1263 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1264 assert_eq!(v.value(), Ok(false));
1265 }
1266 (
1267 OpType::NegatedAllocatedTrue,
1268 OpType::NegatedAllocatedFalse,
1269 Boolean::Is(ref v),
1270 ) => {
1271 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1272 assert_eq!(v.value(), Ok(false));
1273 }
1274
1275 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Not(_)) => (),
1276 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Constant(false)) => (),
1277 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1278 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1279 assert_eq!(v.value(), Ok(true));
1280 }
1281 (OpType::NegatedAllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1282 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1283 assert_eq!(v.value(), Ok(false));
1284 }
1285 (
1286 OpType::NegatedAllocatedFalse,
1287 OpType::NegatedAllocatedTrue,
1288 Boolean::Is(ref v),
1289 ) => {
1290 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1291 assert_eq!(v.value(), Ok(false));
1292 }
1293 (
1294 OpType::NegatedAllocatedFalse,
1295 OpType::NegatedAllocatedFalse,
1296 Boolean::Is(ref v),
1297 ) => {
1298 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1299 assert_eq!(v.value(), Ok(true));
1300 }
1301
1302 _ => {
1303 panic!(
1304 "unexpected behavior at {:?} AND {:?}",
1305 first_operand, second_operand
1306 );
1307 }
1308 }
1309 }
1310 }
1311 Ok(())
1312 }
1313
1314 #[test]
1315 fn test_smaller_than_or_equal_to() -> Result<(), SynthesisError> {
1316 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1317 for _ in 0..1000 {
1318 let mut r = Fr::rand(&mut rng);
1319 let mut s = Fr::rand(&mut rng);
1320 if r > s {
1321 core::mem::swap(&mut r, &mut s)
1322 }
1323
1324 let cs = ConstraintSystem::<Fr>::new_ref();
1325
1326 let native_bits: Vec<_> = BitIteratorLE::new(r.into_repr()).collect();
1327 let bits = Vec::new_witness(cs.clone(), || Ok(native_bits))?;
1328 Boolean::enforce_smaller_or_equal_than_le(&bits, s.into_repr())?;
1329
1330 assert!(cs.is_satisfied().unwrap());
1331 }
1332
1333 for _ in 0..1000 {
1334 let r = Fr::rand(&mut rng);
1335 if r == -Fr::one() {
1336 continue;
1337 }
1338 let s = r + Fr::one();
1339 let s2 = r.double();
1340 let cs = ConstraintSystem::<Fr>::new_ref();
1341
1342 let native_bits: Vec<_> = BitIteratorLE::new(r.into_repr()).collect();
1343 let bits = Vec::new_witness(cs.clone(), || Ok(native_bits))?;
1344 Boolean::enforce_smaller_or_equal_than_le(&bits, s.into_repr())?;
1345 if r < s2 {
1346 Boolean::enforce_smaller_or_equal_than_le(&bits, s2.into_repr())?;
1347 }
1348
1349 assert!(cs.is_satisfied().unwrap());
1350 }
1351 Ok(())
1352 }
1353
1354 #[test]
1355 fn test_enforce_in_field() -> Result<(), SynthesisError> {
1356 {
1357 let cs = ConstraintSystem::<Fr>::new_ref();
1358
1359 let mut bits = vec![];
1360 for b in BitIteratorBE::new(Fr::characteristic()).skip(1) {
1361 bits.push(Boolean::new_witness(cs.clone(), || Ok(b))?);
1362 }
1363 bits.reverse();
1364
1365 Boolean::enforce_in_field_le(&bits)?;
1366
1367 assert!(!cs.is_satisfied().unwrap());
1368 }
1369
1370 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1371
1372 for _ in 0..1000 {
1373 let r = Fr::rand(&mut rng);
1374 let cs = ConstraintSystem::<Fr>::new_ref();
1375
1376 let mut bits = vec![];
1377 for b in BitIteratorBE::new(r.into_repr()).skip(1) {
1378 bits.push(Boolean::new_witness(cs.clone(), || Ok(b))?);
1379 }
1380 bits.reverse();
1381
1382 Boolean::enforce_in_field_le(&bits)?;
1383
1384 assert!(cs.is_satisfied().unwrap());
1385 }
1386 Ok(())
1387 }
1388
1389 #[test]
1390 fn test_enforce_nand() -> Result<(), SynthesisError> {
1391 {
1392 let cs = ConstraintSystem::<Fr>::new_ref();
1393
1394 assert!(
1395 Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), false)?]).is_ok()
1396 );
1397 assert!(
1398 Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), true)?]).is_err()
1399 );
1400 }
1401
1402 for i in 1..5 {
1403 // with every possible assignment for them
1404 for mut b in 0..(1 << i) {
1405 // with every possible negation
1406 for mut n in 0..(1 << i) {
1407 let cs = ConstraintSystem::<Fr>::new_ref();
1408
1409 let mut expected = true;
1410
1411 let mut bits = vec![];
1412 for _ in 0..i {
1413 expected &= b & 1 == 1;
1414
1415 let bit = if n & 1 == 1 {
1416 Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?
1417 } else {
1418 Boolean::new_witness(cs.clone(), || Ok(b & 1 == 0))?.not()
1419 };
1420 bits.push(bit);
1421
1422 b >>= 1;
1423 n >>= 1;
1424 }
1425
1426 let expected = !expected;
1427
1428 Boolean::enforce_kary_nand(&bits)?;
1429
1430 if expected {
1431 assert!(cs.is_satisfied().unwrap());
1432 } else {
1433 assert!(!cs.is_satisfied().unwrap());
1434 }
1435 }
1436 }
1437 }
1438 Ok(())
1439 }
1440
1441 #[test]
1442 fn test_kary_and() -> Result<(), SynthesisError> {
1443 // test different numbers of operands
1444 for i in 1..15 {
1445 // with every possible assignment for them
1446 for mut b in 0..(1 << i) {
1447 let cs = ConstraintSystem::<Fr>::new_ref();
1448
1449 let mut expected = true;
1450
1451 let mut bits = vec![];
1452 for _ in 0..i {
1453 expected &= b & 1 == 1;
1454 bits.push(Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?);
1455 b >>= 1;
1456 }
1457
1458 let r = Boolean::kary_and(&bits)?;
1459
1460 assert!(cs.is_satisfied().unwrap());
1461
1462 if let Boolean::Is(ref r) = r {
1463 assert_eq!(r.value()?, expected);
1464 }
1465 }
1466 }
1467 Ok(())
1468 }
1469}