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 /// Constructs a `LinearCombination` from `Self`'s variables.
258 ///
259 /// * `Boolean::Is(v) => lc!() + v.variable()`
260 /// * `Boolean::Not(v) => lc!() + Variable::One - v.variable()`
261 pub fn lc(&self) -> LinearCombination<F> {
262 match self {
263 Boolean::Constant(false) => lc!(),
264 Boolean::Constant(true) => lc!() + Variable::One,
265 Boolean::Is(v) => v.variable().into(),
266 Boolean::Not(v) => lc!() + Variable::One - v.variable(),
267 }
268 }
269
270 /// Constructs a `Boolean` vector from a slice of constant `u8`.
271 ///
272 /// This *does not* create any new variables.
273 pub fn constant_vec_from_bytes(values: &[u8]) -> Vec<Self> {
274 let mut input_bits = vec![];
275 for input_byte in values {
276 for bit_i in (0..8).rev() {
277 input_bits.push(Self::Constant(((input_byte >> bit_i) & 1u8) == 1u8));
278 }
279 }
280 input_bits
281 }
282
283 /// Constructs a constant `Boolean` with value `b`.
284 pub fn constant(b: bool) -> Self {
285 Boolean::Constant(b)
286 }
287
288 /// Negates `self`.
289 pub fn not(&self) -> Self {
290 match *self {
291 Boolean::Constant(c) => Boolean::Constant(!c),
292 Boolean::Is(ref v) => Boolean::Not(v.clone()),
293 Boolean::Not(ref v) => Boolean::Is(v.clone()),
294 }
295 }
296}
297
298impl<F: Field> Boolean<F> {
299 /// Outputs `self ^ other`.
300 ///
301 /// If at least one of `self` and `other` are constants, then this method
302 /// *does not* create any constraints or variables.
303 #[tracing::instrument(target = "r1cs")]
304 pub fn xor<'a>(&'a self, other: &'a Self) -> Result<Self, SynthesisError> {
305 use Boolean::*;
306 match (self, other) {
307 (&Constant(false), x) | (x, &Constant(false)) => Ok(x.clone()),
308 (&Constant(true), x) | (x, &Constant(true)) => Ok(x.not()),
309 // a XOR (NOT b) = NOT(a XOR b)
310 (is @ &Is(_), not @ &Not(_)) | (not @ &Not(_), is @ &Is(_)) => {
311 Ok(is.xor(¬.not())?.not())
312 }
313 // a XOR b = (NOT a) XOR (NOT b)
314 (&Is(ref a), &Is(ref b)) | (&Not(ref a), &Not(ref b)) => Ok(Is(a.xor(b)?)),
315 }
316 }
317
318 /// Outputs `self | other`.
319 ///
320 /// If at least one of `self` and `other` are constants, then this method
321 /// *does not* create any constraints or variables.
322 #[tracing::instrument(target = "r1cs")]
323 pub fn or<'a>(&'a self, other: &'a Self) -> Result<Self, SynthesisError> {
324 use Boolean::*;
325 match (self, other) {
326 (&Constant(false), x) | (x, &Constant(false)) => Ok(x.clone()),
327 (&Constant(true), _) | (_, &Constant(true)) => Ok(Constant(true)),
328 // a OR b = NOT ((NOT a) AND b)
329 (a @ &Is(_), b @ &Not(_)) | (b @ &Not(_), a @ &Is(_)) | (b @ &Not(_), a @ &Not(_)) => {
330 Ok(a.not().and(&b.not())?.not())
331 }
332 (&Is(ref a), &Is(ref b)) => a.or(b).map(From::from),
333 }
334 }
335
336 /// Outputs `self & other`.
337 ///
338 /// If at least one of `self` and `other` are constants, then this method
339 /// *does not* create any constraints or variables.
340 #[tracing::instrument(target = "r1cs")]
341 pub fn and<'a>(&'a self, other: &'a Self) -> Result<Self, SynthesisError> {
342 use Boolean::*;
343 match (self, other) {
344 // false AND x is always false
345 (&Constant(false), _) | (_, &Constant(false)) => Ok(Constant(false)),
346 // true AND x is always x
347 (&Constant(true), x) | (x, &Constant(true)) => Ok(x.clone()),
348 // a AND (NOT b)
349 (&Is(ref is), &Not(ref not)) | (&Not(ref not), &Is(ref is)) => Ok(Is(is.and_not(not)?)),
350 // (NOT a) AND (NOT b) = a NOR b
351 (&Not(ref a), &Not(ref b)) => Ok(Is(a.nor(b)?)),
352 // a AND b
353 (&Is(ref a), &Is(ref b)) => Ok(Is(a.and(b)?)),
354 }
355 }
356
357 /// Outputs `bits[0] & bits[1] & ... & bits.last().unwrap()`.
358 #[tracing::instrument(target = "r1cs")]
359 pub fn kary_and(bits: &[Self]) -> Result<Self, SynthesisError> {
360 assert!(!bits.is_empty());
361 let mut cur: Option<Self> = None;
362 for next in bits {
363 cur = if let Some(b) = cur {
364 Some(b.and(next)?)
365 } else {
366 Some(next.clone())
367 };
368 }
369
370 Ok(cur.expect("should not be 0"))
371 }
372
373 /// Outputs `bits[0] | bits[1] | ... | bits.last().unwrap()`.
374 #[tracing::instrument(target = "r1cs")]
375 pub fn kary_or(bits: &[Self]) -> Result<Self, SynthesisError> {
376 assert!(!bits.is_empty());
377 let mut cur: Option<Self> = None;
378 for next in bits {
379 cur = if let Some(b) = cur {
380 Some(b.or(next)?)
381 } else {
382 Some(next.clone())
383 };
384 }
385
386 Ok(cur.expect("should not be 0"))
387 }
388
389 /// Outputs `(bits[0] & bits[1] & ... & bits.last().unwrap()).not()`.
390 #[tracing::instrument(target = "r1cs")]
391 pub fn kary_nand(bits: &[Self]) -> Result<Self, SynthesisError> {
392 Ok(Self::kary_and(bits)?.not())
393 }
394
395 /// Enforces that `Self::kary_nand(bits).is_eq(&Boolean::TRUE)`.
396 ///
397 /// Informally, this means that at least one element in `bits` must be `false`.
398 #[tracing::instrument(target = "r1cs")]
399 fn enforce_kary_nand(bits: &[Self]) -> Result<(), SynthesisError> {
400 use Boolean::*;
401 let r = Self::kary_nand(bits)?;
402 match r {
403 Constant(true) => Ok(()),
404 Constant(false) => Err(SynthesisError::AssignmentMissing),
405 Is(_) | Not(_) => r.cs().unwrap().enforce_constraint(
406 r.lc(),
407 lc!() + Variable::One,
408 lc!() + Variable::One,
409 ),
410 }
411 }
412
413 /// Enforces that `bits`, when interpreted as a integer, is less than `F::characteristic()`,
414 /// That is, interpret bits as a little-endian integer, and enforce that this integer
415 /// is "in the field Z_p", where `p = F::characteristic()` .
416 #[tracing::instrument(target = "r1cs")]
417 pub fn enforce_in_field_le(bits: &[Self]) -> Result<(), SynthesisError> {
418 // `bits` < F::characteristic() <==> `bits` <= F::characteristic() -1
419 let mut b = F::characteristic().to_vec();
420 assert_eq!(b[0] % 2, 1);
421 b[0] -= 1; // This works, because the LSB is one, so there's no borrows.
422 let run = Self::enforce_smaller_or_equal_than_le(bits, b)?;
423
424 // We should always end in a "run" of zeros, because
425 // the characteristic is an odd prime. So, this should
426 // be empty.
427 assert!(run.is_empty());
428
429 Ok(())
430 }
431
432 /// Enforces that `bits` is less than or equal to `element`,
433 /// when both are interpreted as (little-endian) integers.
434 #[tracing::instrument(target = "r1cs", skip(element))]
435 pub fn enforce_smaller_or_equal_than_le<'a>(
436 bits: &[Self],
437 element: impl AsRef<[u64]>,
438 ) -> Result<Vec<Self>, SynthesisError> {
439 let b: &[u64] = element.as_ref();
440
441 let mut bits_iter = bits.iter().rev(); // Iterate in big-endian
442
443 // Runs of ones in r
444 let mut last_run = Boolean::constant(true);
445 let mut current_run = vec![];
446
447 let mut element_num_bits = 0;
448 for _ in BitIteratorBE::without_leading_zeros(b) {
449 element_num_bits += 1;
450 }
451
452 if bits.len() > element_num_bits {
453 let mut or_result = Boolean::constant(false);
454 for should_be_zero in &bits[element_num_bits..] {
455 or_result = or_result.or(should_be_zero)?;
456 let _ = bits_iter.next().unwrap();
457 }
458 or_result.enforce_equal(&Boolean::constant(false))?;
459 }
460
461 for (b, a) in BitIteratorBE::without_leading_zeros(b).zip(bits_iter.by_ref()) {
462 if b {
463 // This is part of a run of ones.
464 current_run.push(a.clone());
465 } else {
466 if !current_run.is_empty() {
467 // This is the start of a run of zeros, but we need
468 // to k-ary AND against `last_run` first.
469
470 current_run.push(last_run.clone());
471 last_run = Self::kary_and(¤t_run)?;
472 current_run.truncate(0);
473 }
474
475 // If `last_run` is true, `a` must be false, or it would
476 // not be in the field.
477 //
478 // If `last_run` is false, `a` can be true or false.
479 //
480 // Ergo, at least one of `last_run` and `a` must be false.
481 Self::enforce_kary_nand(&[last_run.clone(), a.clone()])?;
482 }
483 }
484 assert!(bits_iter.next().is_none());
485
486 Ok(current_run)
487 }
488
489 /// Conditionally selects one of `first` and `second` based on the value of `self`:
490 ///
491 /// If `self.is_eq(&Boolean::TRUE)`, this outputs `first`; else, it outputs `second`.
492 #[tracing::instrument(target = "r1cs", skip(first, second))]
493 pub fn select<T: CondSelectGadget<F>>(
494 &self,
495 first: &T,
496 second: &T,
497 ) -> Result<T, SynthesisError> {
498 T::conditionally_select(&self, first, second)
499 }
500}
501
502impl<F: Field> From<AllocatedBit<F>> for Boolean<F> {
503 fn from(b: AllocatedBit<F>) -> Self {
504 Boolean::Is(b)
505 }
506}
507
508impl<F: Field> AllocVar<bool, F> for Boolean<F> {
509 fn new_variable<T: Borrow<bool>>(
510 cs: impl Into<Namespace<F>>,
511 f: impl FnOnce() -> Result<T, SynthesisError>,
512 mode: AllocationMode,
513 ) -> Result<Self, SynthesisError> {
514 if mode == AllocationMode::Constant {
515 Ok(Boolean::Constant(*f()?.borrow()))
516 } else {
517 AllocatedBit::new_variable(cs, f, mode).map(Boolean::from)
518 }
519 }
520}
521
522impl<F: Field> EqGadget<F> for Boolean<F> {
523 #[tracing::instrument(target = "r1cs")]
524 fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
525 // self | other | XNOR(self, other) | self == other
526 // -----|-------|-------------------|--------------
527 // 0 | 0 | 1 | 1
528 // 0 | 1 | 0 | 0
529 // 1 | 0 | 0 | 0
530 // 1 | 1 | 1 | 1
531 Ok(self.xor(other)?.not())
532 }
533
534 #[tracing::instrument(target = "r1cs")]
535 fn conditional_enforce_equal(
536 &self,
537 other: &Self,
538 condition: &Boolean<F>,
539 ) -> Result<(), SynthesisError> {
540 use Boolean::*;
541 let one = Variable::One;
542 let difference = match (self, other) {
543 // 1 == 1; 0 == 0
544 (Constant(true), Constant(true)) | (Constant(false), Constant(false)) => return Ok(()),
545 // false != true
546 (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
547 // 1 - a
548 (Constant(true), Is(a)) | (Is(a), Constant(true)) => lc!() + one - a.variable(),
549 // a - 0 = a
550 (Constant(false), Is(a)) | (Is(a), Constant(false)) => lc!() + a.variable(),
551 // 1 - !a = 1 - (1 - a) = a
552 (Constant(true), Not(a)) | (Not(a), Constant(true)) => lc!() + a.variable(),
553 // !a - 0 = !a = 1 - a
554 (Constant(false), Not(a)) | (Not(a), Constant(false)) => lc!() + one - a.variable(),
555 // b - a,
556 (Is(a), Is(b)) => lc!() + b.variable() - a.variable(),
557 // !b - a = (1 - b) - a
558 (Is(a), Not(b)) | (Not(b), Is(a)) => lc!() + one - b.variable() - a.variable(),
559 // !b - !a = (1 - b) - (1 - a) = a - b,
560 (Not(a), Not(b)) => lc!() + a.variable() - b.variable(),
561 };
562
563 if condition != &Constant(false) {
564 let cs = self.cs().or(other.cs()).or(condition.cs()).unwrap();
565 cs.enforce_constraint(lc!() + difference, condition.lc(), lc!())?;
566 }
567 Ok(())
568 }
569
570 #[tracing::instrument(target = "r1cs")]
571 fn conditional_enforce_not_equal(
572 &self,
573 other: &Self,
574 should_enforce: &Boolean<F>,
575 ) -> Result<(), SynthesisError> {
576 use Boolean::*;
577 let one = Variable::One;
578 let difference = match (self, other) {
579 // 1 != 0; 0 != 1
580 (Constant(true), Constant(false)) | (Constant(false), Constant(true)) => return Ok(()),
581 // false == false and true == true
582 (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
583 // 1 - a
584 (Constant(true), Is(a)) | (Is(a), Constant(true)) => lc!() + one - a.variable(),
585 // a - 0 = a
586 (Constant(false), Is(a)) | (Is(a), Constant(false)) => lc!() + a.variable(),
587 // 1 - !a = 1 - (1 - a) = a
588 (Constant(true), Not(a)) | (Not(a), Constant(true)) => lc!() + a.variable(),
589 // !a - 0 = !a = 1 - a
590 (Constant(false), Not(a)) | (Not(a), Constant(false)) => lc!() + one - a.variable(),
591 // b - a,
592 (Is(a), Is(b)) => lc!() + b.variable() - a.variable(),
593 // !b - a = (1 - b) - a
594 (Is(a), Not(b)) | (Not(b), Is(a)) => lc!() + one - b.variable() - a.variable(),
595 // !b - !a = (1 - b) - (1 - a) = a - b,
596 (Not(a), Not(b)) => lc!() + a.variable() - b.variable(),
597 };
598
599 if should_enforce != &Constant(false) {
600 let cs = self
601 .cs()
602 .or(other.cs())
603 .or(should_enforce.cs())
604 .ok_or(SynthesisError::UnconstrainedVariable)?;
605 cs.enforce_constraint(difference, should_enforce.lc(), should_enforce.lc())?;
606 }
607 Ok(())
608 }
609}
610
611impl<F: Field> ToBytesGadget<F> for Boolean<F> {
612 /// Outputs `1u8` if `self` is true, and `0u8` otherwise.
613 #[tracing::instrument(target = "r1cs")]
614 fn to_bytes(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
615 let mut bits = vec![self.clone()];
616 bits.extend(vec![Boolean::constant(false); 7]);
617 let value = self.value().map(u8::from).ok();
618 let byte = UInt8 { bits, value };
619 Ok(vec![byte])
620 }
621}
622
623impl<F: PrimeField> ToConstraintFieldGadget<F> for Boolean<F> {
624 #[tracing::instrument(target = "r1cs")]
625 fn to_constraint_field(&self) -> Result<Vec<FpVar<F>>, SynthesisError> {
626 let var = From::from(self.clone());
627 Ok(vec![var])
628 }
629}
630
631impl<F: Field> CondSelectGadget<F> for Boolean<F> {
632 #[tracing::instrument(target = "r1cs")]
633 fn conditionally_select(
634 cond: &Boolean<F>,
635 true_val: &Self,
636 false_val: &Self,
637 ) -> Result<Self, SynthesisError> {
638 use Boolean::*;
639 match cond {
640 Constant(true) => Ok(true_val.clone()),
641 Constant(false) => Ok(false_val.clone()),
642 cond @ Not(_) => Self::conditionally_select(&cond.not(), false_val, true_val),
643 cond @ Is(_) => match (true_val, false_val) {
644 (x, &Constant(false)) => cond.and(x),
645 (&Constant(false), x) => cond.not().and(x),
646 (&Constant(true), x) => cond.or(x),
647 (x, &Constant(true)) => cond.not().or(x),
648 (a, b) => {
649 let cs = cond.cs().unwrap();
650 let result: Boolean<F> =
651 AllocatedBit::new_witness_without_booleanity_check(cs.clone(), || {
652 let cond = cond.value()?;
653 Ok(if cond { a.value()? } else { b.value()? })
654 })?
655 .into();
656 //
657 // a = self; b = other; c = cond;
658 //
659 // r = c * a + (1 - c) * b
660 // r = b + c * (a - b)
661 // c * (a - b) = r - b
662 //
663 // If a, b, cond are all boolean, so is r.
664 //
665 // self | other | cond | result
666 // -----|-------|----------------
667 // 0 | 0 | 1 | 0
668 // 0 | 1 | 1 | 0
669 // 1 | 0 | 1 | 1
670 // 1 | 1 | 1 | 1
671 // 0 | 0 | 0 | 0
672 // 0 | 1 | 0 | 1
673 // 1 | 0 | 0 | 0
674 // 1 | 1 | 0 | 1
675 cs.enforce_constraint(
676 cond.lc(),
677 lc!() + a.lc() - b.lc(),
678 lc!() + result.lc() - b.lc(),
679 )?;
680
681 Ok(result)
682 }
683 },
684 }
685 }
686}
687
688#[cfg(test)]
689mod test {
690 use super::{AllocatedBit, Boolean};
691 use crate::prelude::*;
692 use algebra::{
693 bls12_381::Fr, BitIteratorBE, BitIteratorLE, Field, One, PrimeField, UniformRand, Zero,
694 };
695 use r1cs_core::{ConstraintSystem, Namespace, SynthesisError};
696 use rand::SeedableRng;
697 use rand_xorshift::XorShiftRng;
698
699 #[test]
700 fn test_boolean_to_byte() -> Result<(), SynthesisError> {
701 for val in [true, false].iter() {
702 let cs = ConstraintSystem::<Fr>::new_ref();
703 let a = Boolean::new_witness(cs.clone(), || Ok(*val))?;
704 let bytes = a.to_bytes()?;
705 assert_eq!(bytes.len(), 1);
706 let byte = &bytes[0];
707 assert_eq!(byte.value()?, *val as u8);
708
709 for (i, bit) in byte.bits.iter().enumerate() {
710 assert_eq!(bit.value()?, (byte.value()? >> i) & 1 == 1);
711 }
712 }
713 Ok(())
714 }
715
716 #[test]
717 fn test_xor() -> Result<(), SynthesisError> {
718 for a_val in [false, true].iter().copied() {
719 for b_val in [false, true].iter().copied() {
720 let cs = ConstraintSystem::<Fr>::new_ref();
721 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
722 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
723 let c = AllocatedBit::xor(&a, &b)?;
724 assert_eq!(c.value()?, a_val ^ b_val);
725
726 assert!(cs.is_satisfied().unwrap());
727 assert_eq!(a.value()?, (a_val));
728 assert_eq!(b.value()?, (b_val));
729 assert_eq!(c.value()?, (a_val ^ b_val));
730 }
731 }
732 Ok(())
733 }
734
735 #[test]
736 fn test_or() -> Result<(), SynthesisError> {
737 for a_val in [false, true].iter().copied() {
738 for b_val in [false, true].iter().copied() {
739 let cs = ConstraintSystem::<Fr>::new_ref();
740 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
741 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
742 let c = AllocatedBit::or(&a, &b)?;
743 assert_eq!(c.value()?, a_val | b_val);
744
745 assert!(cs.is_satisfied().unwrap());
746 assert_eq!(a.value()?, (a_val));
747 assert_eq!(b.value()?, (b_val));
748 assert_eq!(c.value()?, (a_val | b_val));
749 }
750 }
751 Ok(())
752 }
753
754 #[test]
755 fn test_and() -> Result<(), SynthesisError> {
756 for a_val in [false, true].iter().copied() {
757 for b_val in [false, true].iter().copied() {
758 let cs = ConstraintSystem::<Fr>::new_ref();
759 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
760 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
761 let c = AllocatedBit::and(&a, &b)?;
762 assert_eq!(c.value()?, a_val & b_val);
763
764 assert!(cs.is_satisfied().unwrap());
765 assert_eq!(a.value()?, (a_val));
766 assert_eq!(b.value()?, (b_val));
767 assert_eq!(c.value()?, (a_val & b_val));
768 }
769 }
770 Ok(())
771 }
772
773 #[test]
774 fn test_and_not() -> Result<(), SynthesisError> {
775 for a_val in [false, true].iter().copied() {
776 for b_val in [false, true].iter().copied() {
777 let cs = ConstraintSystem::<Fr>::new_ref();
778 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
779 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
780 let c = AllocatedBit::and_not(&a, &b)?;
781 assert_eq!(c.value()?, a_val & !b_val);
782
783 assert!(cs.is_satisfied().unwrap());
784 assert_eq!(a.value()?, (a_val));
785 assert_eq!(b.value()?, (b_val));
786 assert_eq!(c.value()?, (a_val & !b_val));
787 }
788 }
789 Ok(())
790 }
791
792 #[test]
793 fn test_nor() -> Result<(), SynthesisError> {
794 for a_val in [false, true].iter().copied() {
795 for b_val in [false, true].iter().copied() {
796 let cs = ConstraintSystem::<Fr>::new_ref();
797 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
798 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
799 let c = AllocatedBit::nor(&a, &b)?;
800 assert_eq!(c.value()?, !a_val & !b_val);
801
802 assert!(cs.is_satisfied().unwrap());
803 assert_eq!(a.value()?, (a_val));
804 assert_eq!(b.value()?, (b_val));
805 assert_eq!(c.value()?, (!a_val & !b_val));
806 }
807 }
808 Ok(())
809 }
810
811 #[test]
812 fn test_enforce_equal() -> Result<(), SynthesisError> {
813 for a_bool in [false, true].iter().cloned() {
814 for b_bool in [false, true].iter().cloned() {
815 for a_neg in [false, true].iter().cloned() {
816 for b_neg in [false, true].iter().cloned() {
817 let cs = ConstraintSystem::<Fr>::new_ref();
818
819 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
820 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
821
822 if a_neg {
823 a = a.not();
824 }
825 if b_neg {
826 b = b.not();
827 }
828
829 a.enforce_equal(&b)?;
830
831 assert_eq!(
832 cs.is_satisfied().unwrap(),
833 (a_bool ^ a_neg) == (b_bool ^ b_neg)
834 );
835 }
836 }
837 }
838 }
839 Ok(())
840 }
841
842 #[test]
843 fn test_conditional_enforce_equal() -> Result<(), SynthesisError> {
844 for a_bool in [false, true].iter().cloned() {
845 for b_bool in [false, true].iter().cloned() {
846 for a_neg in [false, true].iter().cloned() {
847 for b_neg in [false, true].iter().cloned() {
848 let cs = ConstraintSystem::<Fr>::new_ref();
849
850 // First test if constraint system is satisfied
851 // when we do want to enforce the condition.
852 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
853 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
854
855 if a_neg {
856 a = a.not();
857 }
858 if b_neg {
859 b = b.not();
860 }
861
862 a.conditional_enforce_equal(&b, &Boolean::constant(true))?;
863
864 assert_eq!(
865 cs.is_satisfied().unwrap(),
866 (a_bool ^ a_neg) == (b_bool ^ b_neg)
867 );
868
869 // Now test if constraint system is satisfied even
870 // when we don't want to enforce the condition.
871 let cs = ConstraintSystem::<Fr>::new_ref();
872
873 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
874 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
875
876 if a_neg {
877 a = a.not();
878 }
879 if b_neg {
880 b = b.not();
881 }
882
883 let false_cond =
884 Boolean::new_witness(r1cs_core::ns!(cs, "cond"), || Ok(false))?;
885 a.conditional_enforce_equal(&b, &false_cond)?;
886
887 assert!(cs.is_satisfied().unwrap());
888 }
889 }
890 }
891 }
892 Ok(())
893 }
894
895 #[test]
896 fn test_boolean_negation() -> Result<(), SynthesisError> {
897 let cs = ConstraintSystem::<Fr>::new_ref();
898
899 let mut b = Boolean::new_witness(cs.clone(), || Ok(true))?;
900 assert!(matches!(b, Boolean::Is(_)));
901
902 b = b.not();
903 assert!(matches!(b, Boolean::Not(_)));
904
905 b = b.not();
906 assert!(matches!(b, Boolean::Is(_)));
907
908 b = Boolean::Constant(true);
909 assert!(matches!(b, Boolean::Constant(true)));
910
911 b = b.not();
912 assert!(matches!(b, Boolean::Constant(false)));
913
914 b = b.not();
915 assert!(matches!(b, Boolean::Constant(true)));
916 Ok(())
917 }
918
919 #[derive(Eq, PartialEq, Copy, Clone, Debug)]
920 enum OpType {
921 True,
922 False,
923 AllocatedTrue,
924 AllocatedFalse,
925 NegatedAllocatedTrue,
926 NegatedAllocatedFalse,
927 }
928
929 const VARIANTS: [OpType; 6] = [
930 OpType::True,
931 OpType::False,
932 OpType::AllocatedTrue,
933 OpType::AllocatedFalse,
934 OpType::NegatedAllocatedTrue,
935 OpType::NegatedAllocatedFalse,
936 ];
937
938 fn construct<F: Field>(
939 ns: Namespace<F>,
940 operand: OpType,
941 ) -> Result<Boolean<F>, SynthesisError> {
942 let cs = ns.cs();
943
944 let b = match operand {
945 OpType::True => Boolean::constant(true),
946 OpType::False => Boolean::constant(false),
947 OpType::AllocatedTrue => Boolean::new_witness(cs, || Ok(true))?,
948 OpType::AllocatedFalse => Boolean::new_witness(cs, || Ok(false))?,
949 OpType::NegatedAllocatedTrue => Boolean::new_witness(cs, || Ok(true))?.not(),
950 OpType::NegatedAllocatedFalse => Boolean::new_witness(cs, || Ok(false))?.not(),
951 };
952 Ok(b)
953 }
954
955 #[test]
956 fn test_boolean_xor() -> Result<(), SynthesisError> {
957 for first_operand in VARIANTS.iter().cloned() {
958 for second_operand in VARIANTS.iter().cloned() {
959 let cs = ConstraintSystem::<Fr>::new_ref();
960
961 let a = construct(r1cs_core::ns!(cs, "a"), first_operand)?;
962 let b = construct(r1cs_core::ns!(cs, "b"), second_operand)?;
963 let c = Boolean::xor(&a, &b)?;
964
965 assert!(cs.is_satisfied().unwrap());
966
967 match (first_operand, second_operand, c) {
968 (OpType::True, OpType::True, Boolean::Constant(false)) => (),
969 (OpType::True, OpType::False, Boolean::Constant(true)) => (),
970 (OpType::True, OpType::AllocatedTrue, Boolean::Not(_)) => (),
971 (OpType::True, OpType::AllocatedFalse, Boolean::Not(_)) => (),
972 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Is(_)) => (),
973 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Is(_)) => (),
974
975 (OpType::False, OpType::True, Boolean::Constant(true)) => (),
976 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
977 (OpType::False, OpType::AllocatedTrue, Boolean::Is(_)) => (),
978 (OpType::False, OpType::AllocatedFalse, Boolean::Is(_)) => (),
979 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
980 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
981
982 (OpType::AllocatedTrue, OpType::True, Boolean::Not(_)) => (),
983 (OpType::AllocatedTrue, OpType::False, Boolean::Is(_)) => (),
984 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
985 assert_eq!(v.value(), Ok(false));
986 }
987 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
988 assert_eq!(v.value(), Ok(true));
989 }
990 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
991 assert_eq!(v.value(), Ok(false));
992 }
993 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Not(ref v)) => {
994 assert_eq!(v.value(), Ok(true));
995 }
996 (OpType::AllocatedFalse, OpType::True, Boolean::Not(_)) => (),
997 (OpType::AllocatedFalse, OpType::False, Boolean::Is(_)) => (),
998 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
999 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1000 assert_eq!(v.value(), Ok(true));
1001 }
1002 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1003 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1004 assert_eq!(v.value(), Ok(false));
1005 }
1006 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1007 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1008 assert_eq!(v.value(), Ok(true));
1009 }
1010 (
1011 OpType::AllocatedFalse,
1012 OpType::NegatedAllocatedFalse,
1013 Boolean::Not(ref v),
1014 ) => {
1015 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1016 assert_eq!(v.value(), Ok(false));
1017 }
1018
1019 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Is(_)) => (),
1020 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Not(_)) => (),
1021 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1022 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1023 assert_eq!(v.value(), Ok(false));
1024 }
1025 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, 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::NegatedAllocatedTrue,
1031 OpType::NegatedAllocatedTrue,
1032 Boolean::Is(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::NegatedAllocatedTrue,
1039 OpType::NegatedAllocatedFalse,
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, OpType::True, Boolean::Is(_)) => (),
1047 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Not(_)) => (),
1048 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1049 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1050 assert_eq!(v.value(), Ok(true));
1051 }
1052 (
1053 OpType::NegatedAllocatedFalse,
1054 OpType::AllocatedFalse,
1055 Boolean::Not(ref v),
1056 ) => {
1057 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1058 assert_eq!(v.value(), Ok(false));
1059 }
1060 (
1061 OpType::NegatedAllocatedFalse,
1062 OpType::NegatedAllocatedTrue,
1063 Boolean::Is(ref v),
1064 ) => {
1065 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1066 assert_eq!(v.value(), Ok(true));
1067 }
1068 (
1069 OpType::NegatedAllocatedFalse,
1070 OpType::NegatedAllocatedFalse,
1071 Boolean::Is(ref v),
1072 ) => {
1073 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1074 assert_eq!(v.value(), Ok(false));
1075 }
1076
1077 _ => unreachable!(),
1078 }
1079 }
1080 }
1081 Ok(())
1082 }
1083
1084 #[test]
1085 fn test_boolean_cond_select() -> Result<(), SynthesisError> {
1086 for condition in VARIANTS.iter().cloned() {
1087 for first_operand in VARIANTS.iter().cloned() {
1088 for second_operand in VARIANTS.iter().cloned() {
1089 let cs = ConstraintSystem::<Fr>::new_ref();
1090
1091 let cond = construct(r1cs_core::ns!(cs, "cond"), condition)?;
1092 let a = construct(r1cs_core::ns!(cs, "a"), first_operand)?;
1093 let b = construct(r1cs_core::ns!(cs, "b"), second_operand)?;
1094 let c = cond.select(&a, &b)?;
1095
1096 assert!(
1097 cs.is_satisfied().unwrap(),
1098 "failed with operands: cond: {:?}, a: {:?}, b: {:?}",
1099 condition,
1100 first_operand,
1101 second_operand,
1102 );
1103 assert_eq!(
1104 c.value()?,
1105 if cond.value()? {
1106 a.value()?
1107 } else {
1108 b.value()?
1109 }
1110 );
1111 }
1112 }
1113 }
1114 Ok(())
1115 }
1116
1117 #[test]
1118 fn test_boolean_or() -> Result<(), SynthesisError> {
1119 for first_operand in VARIANTS.iter().cloned() {
1120 for second_operand in VARIANTS.iter().cloned() {
1121 let cs = ConstraintSystem::<Fr>::new_ref();
1122
1123 let a = construct(r1cs_core::ns!(cs, "a"), first_operand)?;
1124 let b = construct(r1cs_core::ns!(cs, "b"), second_operand)?;
1125 let c = a.or(&b)?;
1126
1127 assert!(cs.is_satisfied().unwrap());
1128
1129 match (first_operand, second_operand, c.clone()) {
1130 (OpType::True, OpType::True, Boolean::Constant(true)) => (),
1131 (OpType::True, OpType::False, Boolean::Constant(true)) => (),
1132 (OpType::True, OpType::AllocatedTrue, Boolean::Constant(true)) => (),
1133 (OpType::True, OpType::AllocatedFalse, Boolean::Constant(true)) => (),
1134 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Constant(true)) => (),
1135 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Constant(true)) => (),
1136
1137 (OpType::False, OpType::True, Boolean::Constant(true)) => (),
1138 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1139 (OpType::False, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1140 (OpType::False, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1141 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1142 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1143
1144 (OpType::AllocatedTrue, OpType::True, Boolean::Constant(true)) => (),
1145 (OpType::AllocatedTrue, OpType::False, Boolean::Is(_)) => (),
1146 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1147 assert_eq!(v.value(), Ok(true));
1148 }
1149 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1150 assert_eq!(v.value(), Ok(true));
1151 }
1152 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1153 assert_eq!(v.value(), Ok(false));
1154 }
1155 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Not(ref v)) => {
1156 assert_eq!(v.value(), Ok(false));
1157 }
1158
1159 (OpType::AllocatedFalse, OpType::True, Boolean::Constant(true)) => (),
1160 (OpType::AllocatedFalse, OpType::False, Boolean::Is(_)) => (),
1161 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1162 assert_eq!(v.value(), Ok(true));
1163 }
1164 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1165 assert_eq!(v.value(), Ok(false));
1166 }
1167 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1168 assert_eq!(v.value(), Ok(true));
1169 }
1170 (
1171 OpType::AllocatedFalse,
1172 OpType::NegatedAllocatedFalse,
1173 Boolean::Not(ref v),
1174 ) => {
1175 assert_eq!(v.value(), Ok(false));
1176 }
1177
1178 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Constant(true)) => (),
1179 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Not(_)) => (),
1180 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1181 assert_eq!(v.value(), Ok(false));
1182 }
1183 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Not(ref v)) => {
1184 assert_eq!(v.value(), Ok(true));
1185 }
1186 (
1187 OpType::NegatedAllocatedTrue,
1188 OpType::NegatedAllocatedTrue,
1189 Boolean::Not(ref v),
1190 ) => {
1191 assert_eq!(v.value(), Ok(true));
1192 }
1193 (
1194 OpType::NegatedAllocatedTrue,
1195 OpType::NegatedAllocatedFalse,
1196 Boolean::Not(ref v),
1197 ) => {
1198 assert_eq!(v.value(), Ok(false));
1199 }
1200
1201 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Constant(true)) => (),
1202 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Not(_)) => (),
1203 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1204 assert_eq!(v.value(), Ok(false));
1205 }
1206 (
1207 OpType::NegatedAllocatedFalse,
1208 OpType::AllocatedFalse,
1209 Boolean::Not(ref v),
1210 ) => {
1211 assert_eq!(v.value(), Ok(false));
1212 }
1213 (
1214 OpType::NegatedAllocatedFalse,
1215 OpType::NegatedAllocatedTrue,
1216 Boolean::Not(ref v),
1217 ) => {
1218 assert_eq!(v.value(), Ok(false));
1219 }
1220 (
1221 OpType::NegatedAllocatedFalse,
1222 OpType::NegatedAllocatedFalse,
1223 Boolean::Not(ref v),
1224 ) => {
1225 assert_eq!(v.value(), Ok(false));
1226 }
1227
1228 _ => panic!(
1229 "this should never be encountered, in case: (a = {:?}, b = {:?}, c = {:?})",
1230 a, b, c
1231 ),
1232 }
1233 }
1234 }
1235 Ok(())
1236 }
1237
1238 #[test]
1239 fn test_boolean_and() -> Result<(), SynthesisError> {
1240 for first_operand in VARIANTS.iter().cloned() {
1241 for second_operand in VARIANTS.iter().cloned() {
1242 let cs = ConstraintSystem::<Fr>::new_ref();
1243
1244 let a = construct(r1cs_core::ns!(cs, "a"), first_operand)?;
1245 let b = construct(r1cs_core::ns!(cs, "b"), second_operand)?;
1246 let c = a.and(&b)?;
1247
1248 assert!(cs.is_satisfied().unwrap());
1249
1250 match (first_operand, second_operand, c) {
1251 (OpType::True, OpType::True, Boolean::Constant(true)) => (),
1252 (OpType::True, OpType::False, Boolean::Constant(false)) => (),
1253 (OpType::True, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1254 (OpType::True, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1255 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1256 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1257
1258 (OpType::False, OpType::True, Boolean::Constant(false)) => (),
1259 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1260 (OpType::False, OpType::AllocatedTrue, Boolean::Constant(false)) => (),
1261 (OpType::False, OpType::AllocatedFalse, Boolean::Constant(false)) => (),
1262 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Constant(false)) => (),
1263 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Constant(false)) => (),
1264
1265 (OpType::AllocatedTrue, OpType::True, Boolean::Is(_)) => (),
1266 (OpType::AllocatedTrue, OpType::False, Boolean::Constant(false)) => (),
1267 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1268 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1269 assert_eq!(v.value(), Ok(true));
1270 }
1271 (OpType::AllocatedTrue, OpType::AllocatedFalse, 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::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Is(ref v)) => {
1276 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1277 assert_eq!(v.value(), Ok(false));
1278 }
1279 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Is(ref v)) => {
1280 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1281 assert_eq!(v.value(), Ok(true));
1282 }
1283
1284 (OpType::AllocatedFalse, OpType::True, Boolean::Is(_)) => (),
1285 (OpType::AllocatedFalse, OpType::False, Boolean::Constant(false)) => (),
1286 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1287 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1288 assert_eq!(v.value(), Ok(false));
1289 }
1290 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1291 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1292 assert_eq!(v.value(), Ok(false));
1293 }
1294 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Is(ref v)) => {
1295 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1296 assert_eq!(v.value(), Ok(false));
1297 }
1298 (OpType::AllocatedFalse, OpType::NegatedAllocatedFalse, Boolean::Is(ref v)) => {
1299 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1300 assert_eq!(v.value(), Ok(false));
1301 }
1302
1303 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Not(_)) => (),
1304 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Constant(false)) => (),
1305 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1306 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1307 assert_eq!(v.value(), Ok(false));
1308 }
1309 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1310 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1311 assert_eq!(v.value(), Ok(false));
1312 }
1313 (
1314 OpType::NegatedAllocatedTrue,
1315 OpType::NegatedAllocatedTrue,
1316 Boolean::Is(ref v),
1317 ) => {
1318 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1319 assert_eq!(v.value(), Ok(false));
1320 }
1321 (
1322 OpType::NegatedAllocatedTrue,
1323 OpType::NegatedAllocatedFalse,
1324 Boolean::Is(ref v),
1325 ) => {
1326 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1327 assert_eq!(v.value(), Ok(false));
1328 }
1329
1330 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Not(_)) => (),
1331 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Constant(false)) => (),
1332 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1333 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1334 assert_eq!(v.value(), Ok(true));
1335 }
1336 (OpType::NegatedAllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1337 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1338 assert_eq!(v.value(), Ok(false));
1339 }
1340 (
1341 OpType::NegatedAllocatedFalse,
1342 OpType::NegatedAllocatedTrue,
1343 Boolean::Is(ref v),
1344 ) => {
1345 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1346 assert_eq!(v.value(), Ok(false));
1347 }
1348 (
1349 OpType::NegatedAllocatedFalse,
1350 OpType::NegatedAllocatedFalse,
1351 Boolean::Is(ref v),
1352 ) => {
1353 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1354 assert_eq!(v.value(), Ok(true));
1355 }
1356
1357 _ => {
1358 panic!(
1359 "unexpected behavior at {:?} AND {:?}",
1360 first_operand, second_operand
1361 );
1362 }
1363 }
1364 }
1365 }
1366 Ok(())
1367 }
1368
1369 #[test]
1370 fn test_smaller_than_or_equal_to() -> Result<(), SynthesisError> {
1371 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1372 for _ in 0..1000 {
1373 let mut r = Fr::rand(&mut rng);
1374 let mut s = Fr::rand(&mut rng);
1375 if r > s {
1376 core::mem::swap(&mut r, &mut s)
1377 }
1378
1379 let cs = ConstraintSystem::<Fr>::new_ref();
1380
1381 let native_bits: Vec<_> = BitIteratorLE::new(r.into_repr()).collect();
1382 let bits = Vec::new_witness(cs.clone(), || Ok(native_bits))?;
1383 Boolean::enforce_smaller_or_equal_than_le(&bits, s.into_repr())?;
1384
1385 assert!(cs.is_satisfied().unwrap());
1386 }
1387
1388 for _ in 0..1000 {
1389 let r = Fr::rand(&mut rng);
1390 if r == -Fr::one() {
1391 continue;
1392 }
1393 let s = r + Fr::one();
1394 let s2 = r.double();
1395 let cs = ConstraintSystem::<Fr>::new_ref();
1396
1397 let native_bits: Vec<_> = BitIteratorLE::new(r.into_repr()).collect();
1398 let bits = Vec::new_witness(cs.clone(), || Ok(native_bits))?;
1399 Boolean::enforce_smaller_or_equal_than_le(&bits, s.into_repr())?;
1400 if r < s2 {
1401 Boolean::enforce_smaller_or_equal_than_le(&bits, s2.into_repr())?;
1402 }
1403
1404 assert!(cs.is_satisfied().unwrap());
1405 }
1406 Ok(())
1407 }
1408
1409 #[test]
1410 fn test_enforce_in_field() -> Result<(), SynthesisError> {
1411 {
1412 let cs = ConstraintSystem::<Fr>::new_ref();
1413
1414 let mut bits = vec![];
1415 for b in BitIteratorBE::new(Fr::characteristic()).skip(1) {
1416 bits.push(Boolean::new_witness(cs.clone(), || Ok(b))?);
1417 }
1418 bits.reverse();
1419
1420 Boolean::enforce_in_field_le(&bits)?;
1421
1422 assert!(!cs.is_satisfied().unwrap());
1423 }
1424
1425 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1426
1427 for _ in 0..1000 {
1428 let r = Fr::rand(&mut rng);
1429 let cs = ConstraintSystem::<Fr>::new_ref();
1430
1431 let mut bits = vec![];
1432 for b in BitIteratorBE::new(r.into_repr()).skip(1) {
1433 bits.push(Boolean::new_witness(cs.clone(), || Ok(b))?);
1434 }
1435 bits.reverse();
1436
1437 Boolean::enforce_in_field_le(&bits)?;
1438
1439 assert!(cs.is_satisfied().unwrap());
1440 }
1441 Ok(())
1442 }
1443
1444 #[test]
1445 fn test_enforce_nand() -> Result<(), SynthesisError> {
1446 {
1447 let cs = ConstraintSystem::<Fr>::new_ref();
1448
1449 assert!(
1450 Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), false)?]).is_ok()
1451 );
1452 assert!(
1453 Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), true)?]).is_err()
1454 );
1455 }
1456
1457 for i in 1..5 {
1458 // with every possible assignment for them
1459 for mut b in 0..(1 << i) {
1460 // with every possible negation
1461 for mut n in 0..(1 << i) {
1462 let cs = ConstraintSystem::<Fr>::new_ref();
1463
1464 let mut expected = true;
1465
1466 let mut bits = vec![];
1467 for _ in 0..i {
1468 expected &= b & 1 == 1;
1469
1470 let bit = if n & 1 == 1 {
1471 Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?
1472 } else {
1473 Boolean::new_witness(cs.clone(), || Ok(b & 1 == 0))?.not()
1474 };
1475 bits.push(bit);
1476
1477 b >>= 1;
1478 n >>= 1;
1479 }
1480
1481 let expected = !expected;
1482
1483 Boolean::enforce_kary_nand(&bits)?;
1484
1485 if expected {
1486 assert!(cs.is_satisfied().unwrap());
1487 } else {
1488 assert!(!cs.is_satisfied().unwrap());
1489 }
1490 }
1491 }
1492 }
1493 Ok(())
1494 }
1495
1496 #[test]
1497 fn test_kary_and() -> Result<(), SynthesisError> {
1498 // test different numbers of operands
1499 for i in 1..15 {
1500 // with every possible assignment for them
1501 for mut b in 0..(1 << i) {
1502 let cs = ConstraintSystem::<Fr>::new_ref();
1503
1504 let mut expected = true;
1505
1506 let mut bits = vec![];
1507 for _ in 0..i {
1508 expected &= b & 1 == 1;
1509 bits.push(Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?);
1510 b >>= 1;
1511 }
1512
1513 let r = Boolean::kary_and(&bits)?;
1514
1515 assert!(cs.is_satisfied().unwrap());
1516
1517 if let Boolean::Is(ref r) = r {
1518 assert_eq!(r.value()?, expected);
1519 }
1520 }
1521 }
1522 Ok(())
1523 }
1524}