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