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