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 `AllocatedBit`,
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 AllocatedBit<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> AllocatedBit<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 `AllocatedBit`.
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 `AllocatedBit`.
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 `AllocatedBit`.
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 AllocatedBit<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 AllocatedBit<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(AllocatedBit<F>),
228 /// Negated view of the boolean variable.
229 Not(AllocatedBit<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<AllocatedBit<F>> for Boolean<F> {
776 fn from(b: AllocatedBit<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 AllocatedBit::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 AllocatedBit::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::{AllocatedBit, 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 use rand::SeedableRng;
963 use rand_xorshift::XorShiftRng;
964
965 #[test]
966 fn test_boolean_to_byte() -> Result<(), SynthesisError> {
967 for val in [true, false].iter() {
968 let cs = ConstraintSystem::<Fr>::new_ref();
969 let a = Boolean::new_witness(cs.clone(), || Ok(*val))?;
970 let bytes = a.to_bytes()?;
971 assert_eq!(bytes.len(), 1);
972 let byte = &bytes[0];
973 assert_eq!(byte.value()?, *val as u8);
974
975 for (i, bit) in byte.bits.iter().enumerate() {
976 assert_eq!(bit.value()?, (byte.value()? >> i) & 1 == 1);
977 }
978 }
979 Ok(())
980 }
981
982 #[test]
983 fn test_xor() -> Result<(), SynthesisError> {
984 for a_val in [false, true].iter().copied() {
985 for b_val in [false, true].iter().copied() {
986 let cs = ConstraintSystem::<Fr>::new_ref();
987 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
988 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
989 let c = AllocatedBit::xor(&a, &b)?;
990 assert_eq!(c.value()?, a_val ^ b_val);
991
992 assert!(cs.is_satisfied().unwrap());
993 assert_eq!(a.value()?, (a_val));
994 assert_eq!(b.value()?, (b_val));
995 assert_eq!(c.value()?, (a_val ^ b_val));
996 }
997 }
998 Ok(())
999 }
1000
1001 #[test]
1002 fn test_or() -> Result<(), SynthesisError> {
1003 for a_val in [false, true].iter().copied() {
1004 for b_val in [false, true].iter().copied() {
1005 let cs = ConstraintSystem::<Fr>::new_ref();
1006 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
1007 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
1008 let c = AllocatedBit::or(&a, &b)?;
1009 assert_eq!(c.value()?, a_val | b_val);
1010
1011 assert!(cs.is_satisfied().unwrap());
1012 assert_eq!(a.value()?, (a_val));
1013 assert_eq!(b.value()?, (b_val));
1014 assert_eq!(c.value()?, (a_val | b_val));
1015 }
1016 }
1017 Ok(())
1018 }
1019
1020 #[test]
1021 fn test_and() -> Result<(), SynthesisError> {
1022 for a_val in [false, true].iter().copied() {
1023 for b_val in [false, true].iter().copied() {
1024 let cs = ConstraintSystem::<Fr>::new_ref();
1025 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
1026 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
1027 let c = AllocatedBit::and(&a, &b)?;
1028 assert_eq!(c.value()?, a_val & b_val);
1029
1030 assert!(cs.is_satisfied().unwrap());
1031 assert_eq!(a.value()?, (a_val));
1032 assert_eq!(b.value()?, (b_val));
1033 assert_eq!(c.value()?, (a_val & b_val));
1034 }
1035 }
1036 Ok(())
1037 }
1038
1039 #[test]
1040 fn test_and_not() -> Result<(), SynthesisError> {
1041 for a_val in [false, true].iter().copied() {
1042 for b_val in [false, true].iter().copied() {
1043 let cs = ConstraintSystem::<Fr>::new_ref();
1044 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
1045 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
1046 let c = AllocatedBit::and_not(&a, &b)?;
1047 assert_eq!(c.value()?, a_val & !b_val);
1048
1049 assert!(cs.is_satisfied().unwrap());
1050 assert_eq!(a.value()?, (a_val));
1051 assert_eq!(b.value()?, (b_val));
1052 assert_eq!(c.value()?, (a_val & !b_val));
1053 }
1054 }
1055 Ok(())
1056 }
1057
1058 #[test]
1059 fn test_nor() -> Result<(), SynthesisError> {
1060 for a_val in [false, true].iter().copied() {
1061 for b_val in [false, true].iter().copied() {
1062 let cs = ConstraintSystem::<Fr>::new_ref();
1063 let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
1064 let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
1065 let c = AllocatedBit::nor(&a, &b)?;
1066 assert_eq!(c.value()?, !a_val & !b_val);
1067
1068 assert!(cs.is_satisfied().unwrap());
1069 assert_eq!(a.value()?, (a_val));
1070 assert_eq!(b.value()?, (b_val));
1071 assert_eq!(c.value()?, (!a_val & !b_val));
1072 }
1073 }
1074 Ok(())
1075 }
1076
1077 #[test]
1078 fn test_enforce_equal() -> Result<(), SynthesisError> {
1079 for a_bool in [false, true].iter().cloned() {
1080 for b_bool in [false, true].iter().cloned() {
1081 for a_neg in [false, true].iter().cloned() {
1082 for b_neg in [false, true].iter().cloned() {
1083 let cs = ConstraintSystem::<Fr>::new_ref();
1084
1085 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
1086 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
1087
1088 if a_neg {
1089 a = a.not();
1090 }
1091 if b_neg {
1092 b = b.not();
1093 }
1094
1095 a.enforce_equal(&b)?;
1096
1097 assert_eq!(
1098 cs.is_satisfied().unwrap(),
1099 (a_bool ^ a_neg) == (b_bool ^ b_neg)
1100 );
1101 }
1102 }
1103 }
1104 }
1105 Ok(())
1106 }
1107
1108 #[test]
1109 fn test_conditional_enforce_equal() -> Result<(), SynthesisError> {
1110 for a_bool in [false, true].iter().cloned() {
1111 for b_bool in [false, true].iter().cloned() {
1112 for a_neg in [false, true].iter().cloned() {
1113 for b_neg in [false, true].iter().cloned() {
1114 let cs = ConstraintSystem::<Fr>::new_ref();
1115
1116 // First test if constraint system is satisfied
1117 // when we do want to enforce the condition.
1118 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
1119 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
1120
1121 if a_neg {
1122 a = a.not();
1123 }
1124 if b_neg {
1125 b = b.not();
1126 }
1127
1128 a.conditional_enforce_equal(&b, &Boolean::constant(true))?;
1129
1130 assert_eq!(
1131 cs.is_satisfied().unwrap(),
1132 (a_bool ^ a_neg) == (b_bool ^ b_neg)
1133 );
1134
1135 // Now test if constraint system is satisfied even
1136 // when we don't want to enforce the condition.
1137 let cs = ConstraintSystem::<Fr>::new_ref();
1138
1139 let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
1140 let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
1141
1142 if a_neg {
1143 a = a.not();
1144 }
1145 if b_neg {
1146 b = b.not();
1147 }
1148
1149 let false_cond =
1150 Boolean::new_witness(ark_relations::ns!(cs, "cond"), || Ok(false))?;
1151 a.conditional_enforce_equal(&b, &false_cond)?;
1152
1153 assert!(cs.is_satisfied().unwrap());
1154 }
1155 }
1156 }
1157 }
1158 Ok(())
1159 }
1160
1161 #[test]
1162 fn test_boolean_negation() -> Result<(), SynthesisError> {
1163 let cs = ConstraintSystem::<Fr>::new_ref();
1164
1165 let mut b = Boolean::new_witness(cs.clone(), || Ok(true))?;
1166 assert!(matches!(b, Boolean::Is(_)));
1167
1168 b = b.not();
1169 assert!(matches!(b, Boolean::Not(_)));
1170
1171 b = b.not();
1172 assert!(matches!(b, Boolean::Is(_)));
1173
1174 b = Boolean::Constant(true);
1175 assert!(matches!(b, Boolean::Constant(true)));
1176
1177 b = b.not();
1178 assert!(matches!(b, Boolean::Constant(false)));
1179
1180 b = b.not();
1181 assert!(matches!(b, Boolean::Constant(true)));
1182 Ok(())
1183 }
1184
1185 #[derive(Eq, PartialEq, Copy, Clone, Debug)]
1186 enum OpType {
1187 True,
1188 False,
1189 AllocatedTrue,
1190 AllocatedFalse,
1191 NegatedAllocatedTrue,
1192 NegatedAllocatedFalse,
1193 }
1194
1195 const VARIANTS: [OpType; 6] = [
1196 OpType::True,
1197 OpType::False,
1198 OpType::AllocatedTrue,
1199 OpType::AllocatedFalse,
1200 OpType::NegatedAllocatedTrue,
1201 OpType::NegatedAllocatedFalse,
1202 ];
1203
1204 fn construct<F: Field>(
1205 ns: Namespace<F>,
1206 operand: OpType,
1207 ) -> Result<Boolean<F>, SynthesisError> {
1208 let cs = ns.cs();
1209
1210 let b = match operand {
1211 OpType::True => Boolean::constant(true),
1212 OpType::False => Boolean::constant(false),
1213 OpType::AllocatedTrue => Boolean::new_witness(cs, || Ok(true))?,
1214 OpType::AllocatedFalse => Boolean::new_witness(cs, || Ok(false))?,
1215 OpType::NegatedAllocatedTrue => Boolean::new_witness(cs, || Ok(true))?.not(),
1216 OpType::NegatedAllocatedFalse => Boolean::new_witness(cs, || Ok(false))?.not(),
1217 };
1218 Ok(b)
1219 }
1220
1221 #[test]
1222 fn test_boolean_xor() -> Result<(), SynthesisError> {
1223 for first_operand in VARIANTS.iter().cloned() {
1224 for second_operand in VARIANTS.iter().cloned() {
1225 let cs = ConstraintSystem::<Fr>::new_ref();
1226
1227 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1228 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1229 let c = Boolean::xor(&a, &b)?;
1230
1231 assert!(cs.is_satisfied().unwrap());
1232
1233 match (first_operand, second_operand, c) {
1234 (OpType::True, OpType::True, Boolean::Constant(false)) => (),
1235 (OpType::True, OpType::False, Boolean::Constant(true)) => (),
1236 (OpType::True, OpType::AllocatedTrue, Boolean::Not(_)) => (),
1237 (OpType::True, OpType::AllocatedFalse, Boolean::Not(_)) => (),
1238 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Is(_)) => (),
1239 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Is(_)) => (),
1240
1241 (OpType::False, OpType::True, Boolean::Constant(true)) => (),
1242 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1243 (OpType::False, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1244 (OpType::False, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1245 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1246 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1247
1248 (OpType::AllocatedTrue, OpType::True, Boolean::Not(_)) => (),
1249 (OpType::AllocatedTrue, OpType::False, Boolean::Is(_)) => (),
1250 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1251 assert_eq!(v.value(), Ok(false));
1252 }
1253 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1254 assert_eq!(v.value(), Ok(true));
1255 }
1256 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1257 assert_eq!(v.value(), Ok(false));
1258 }
1259 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Not(ref v)) => {
1260 assert_eq!(v.value(), Ok(true));
1261 }
1262 (OpType::AllocatedFalse, OpType::True, Boolean::Not(_)) => (),
1263 (OpType::AllocatedFalse, OpType::False, Boolean::Is(_)) => (),
1264 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1265 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1266 assert_eq!(v.value(), Ok(true));
1267 }
1268 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1269 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1270 assert_eq!(v.value(), Ok(false));
1271 }
1272 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1273 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1274 assert_eq!(v.value(), Ok(true));
1275 }
1276 (
1277 OpType::AllocatedFalse,
1278 OpType::NegatedAllocatedFalse,
1279 Boolean::Not(ref v),
1280 ) => {
1281 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1282 assert_eq!(v.value(), Ok(false));
1283 }
1284
1285 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Is(_)) => (),
1286 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Not(_)) => (),
1287 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1288 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1289 assert_eq!(v.value(), Ok(false));
1290 }
1291 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Not(ref v)) => {
1292 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1293 assert_eq!(v.value(), Ok(true));
1294 }
1295 (
1296 OpType::NegatedAllocatedTrue,
1297 OpType::NegatedAllocatedTrue,
1298 Boolean::Is(ref v),
1299 ) => {
1300 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1301 assert_eq!(v.value(), Ok(false));
1302 }
1303 (
1304 OpType::NegatedAllocatedTrue,
1305 OpType::NegatedAllocatedFalse,
1306 Boolean::Is(ref v),
1307 ) => {
1308 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1309 assert_eq!(v.value(), Ok(true));
1310 }
1311
1312 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Is(_)) => (),
1313 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Not(_)) => (),
1314 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1315 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1316 assert_eq!(v.value(), Ok(true));
1317 }
1318 (
1319 OpType::NegatedAllocatedFalse,
1320 OpType::AllocatedFalse,
1321 Boolean::Not(ref v),
1322 ) => {
1323 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1324 assert_eq!(v.value(), Ok(false));
1325 }
1326 (
1327 OpType::NegatedAllocatedFalse,
1328 OpType::NegatedAllocatedTrue,
1329 Boolean::Is(ref v),
1330 ) => {
1331 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1332 assert_eq!(v.value(), Ok(true));
1333 }
1334 (
1335 OpType::NegatedAllocatedFalse,
1336 OpType::NegatedAllocatedFalse,
1337 Boolean::Is(ref v),
1338 ) => {
1339 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1340 assert_eq!(v.value(), Ok(false));
1341 }
1342
1343 _ => unreachable!(),
1344 }
1345 }
1346 }
1347 Ok(())
1348 }
1349
1350 #[test]
1351 fn test_boolean_cond_select() -> Result<(), SynthesisError> {
1352 for condition in VARIANTS.iter().cloned() {
1353 for first_operand in VARIANTS.iter().cloned() {
1354 for second_operand in VARIANTS.iter().cloned() {
1355 let cs = ConstraintSystem::<Fr>::new_ref();
1356
1357 let cond = construct(ark_relations::ns!(cs, "cond"), condition)?;
1358 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1359 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1360 let c = cond.select(&a, &b)?;
1361
1362 assert!(
1363 cs.is_satisfied().unwrap(),
1364 "failed with operands: cond: {:?}, a: {:?}, b: {:?}",
1365 condition,
1366 first_operand,
1367 second_operand,
1368 );
1369 assert_eq!(
1370 c.value()?,
1371 if cond.value()? {
1372 a.value()?
1373 } else {
1374 b.value()?
1375 }
1376 );
1377 }
1378 }
1379 }
1380 Ok(())
1381 }
1382
1383 #[test]
1384 fn test_boolean_or() -> Result<(), SynthesisError> {
1385 for first_operand in VARIANTS.iter().cloned() {
1386 for second_operand in VARIANTS.iter().cloned() {
1387 let cs = ConstraintSystem::<Fr>::new_ref();
1388
1389 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1390 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1391 let c = a.or(&b)?;
1392
1393 assert!(cs.is_satisfied().unwrap());
1394
1395 match (first_operand, second_operand, c.clone()) {
1396 (OpType::True, OpType::True, Boolean::Constant(true)) => (),
1397 (OpType::True, OpType::False, Boolean::Constant(true)) => (),
1398 (OpType::True, OpType::AllocatedTrue, Boolean::Constant(true)) => (),
1399 (OpType::True, OpType::AllocatedFalse, Boolean::Constant(true)) => (),
1400 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Constant(true)) => (),
1401 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Constant(true)) => (),
1402
1403 (OpType::False, OpType::True, Boolean::Constant(true)) => (),
1404 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1405 (OpType::False, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1406 (OpType::False, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1407 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1408 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1409
1410 (OpType::AllocatedTrue, OpType::True, Boolean::Constant(true)) => (),
1411 (OpType::AllocatedTrue, OpType::False, Boolean::Is(_)) => (),
1412 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1413 assert_eq!(v.value(), Ok(true));
1414 }
1415 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1416 assert_eq!(v.value(), Ok(true));
1417 }
1418 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1419 assert_eq!(v.value(), Ok(false));
1420 }
1421 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Not(ref v)) => {
1422 assert_eq!(v.value(), Ok(false));
1423 }
1424
1425 (OpType::AllocatedFalse, OpType::True, Boolean::Constant(true)) => (),
1426 (OpType::AllocatedFalse, OpType::False, Boolean::Is(_)) => (),
1427 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1428 assert_eq!(v.value(), Ok(true));
1429 }
1430 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1431 assert_eq!(v.value(), Ok(false));
1432 }
1433 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Not(ref v)) => {
1434 assert_eq!(v.value(), Ok(true));
1435 }
1436 (
1437 OpType::AllocatedFalse,
1438 OpType::NegatedAllocatedFalse,
1439 Boolean::Not(ref v),
1440 ) => {
1441 assert_eq!(v.value(), Ok(false));
1442 }
1443
1444 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Constant(true)) => (),
1445 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Not(_)) => (),
1446 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1447 assert_eq!(v.value(), Ok(false));
1448 }
1449 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Not(ref v)) => {
1450 assert_eq!(v.value(), Ok(true));
1451 }
1452 (
1453 OpType::NegatedAllocatedTrue,
1454 OpType::NegatedAllocatedTrue,
1455 Boolean::Not(ref v),
1456 ) => {
1457 assert_eq!(v.value(), Ok(true));
1458 }
1459 (
1460 OpType::NegatedAllocatedTrue,
1461 OpType::NegatedAllocatedFalse,
1462 Boolean::Not(ref v),
1463 ) => {
1464 assert_eq!(v.value(), Ok(false));
1465 }
1466
1467 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Constant(true)) => (),
1468 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Not(_)) => (),
1469 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Not(ref v)) => {
1470 assert_eq!(v.value(), Ok(false));
1471 }
1472 (
1473 OpType::NegatedAllocatedFalse,
1474 OpType::AllocatedFalse,
1475 Boolean::Not(ref v),
1476 ) => {
1477 assert_eq!(v.value(), Ok(false));
1478 }
1479 (
1480 OpType::NegatedAllocatedFalse,
1481 OpType::NegatedAllocatedTrue,
1482 Boolean::Not(ref v),
1483 ) => {
1484 assert_eq!(v.value(), Ok(false));
1485 }
1486 (
1487 OpType::NegatedAllocatedFalse,
1488 OpType::NegatedAllocatedFalse,
1489 Boolean::Not(ref v),
1490 ) => {
1491 assert_eq!(v.value(), Ok(false));
1492 }
1493
1494 _ => panic!(
1495 "this should never be encountered, in case: (a = {:?}, b = {:?}, c = {:?})",
1496 a, b, c
1497 ),
1498 }
1499 }
1500 }
1501 Ok(())
1502 }
1503
1504 #[test]
1505 fn test_boolean_and() -> Result<(), SynthesisError> {
1506 for first_operand in VARIANTS.iter().cloned() {
1507 for second_operand in VARIANTS.iter().cloned() {
1508 let cs = ConstraintSystem::<Fr>::new_ref();
1509
1510 let a = construct(ark_relations::ns!(cs, "a"), first_operand)?;
1511 let b = construct(ark_relations::ns!(cs, "b"), second_operand)?;
1512 let c = a.and(&b)?;
1513
1514 assert!(cs.is_satisfied().unwrap());
1515
1516 match (first_operand, second_operand, c) {
1517 (OpType::True, OpType::True, Boolean::Constant(true)) => (),
1518 (OpType::True, OpType::False, Boolean::Constant(false)) => (),
1519 (OpType::True, OpType::AllocatedTrue, Boolean::Is(_)) => (),
1520 (OpType::True, OpType::AllocatedFalse, Boolean::Is(_)) => (),
1521 (OpType::True, OpType::NegatedAllocatedTrue, Boolean::Not(_)) => (),
1522 (OpType::True, OpType::NegatedAllocatedFalse, Boolean::Not(_)) => (),
1523
1524 (OpType::False, OpType::True, Boolean::Constant(false)) => (),
1525 (OpType::False, OpType::False, Boolean::Constant(false)) => (),
1526 (OpType::False, OpType::AllocatedTrue, Boolean::Constant(false)) => (),
1527 (OpType::False, OpType::AllocatedFalse, Boolean::Constant(false)) => (),
1528 (OpType::False, OpType::NegatedAllocatedTrue, Boolean::Constant(false)) => (),
1529 (OpType::False, OpType::NegatedAllocatedFalse, Boolean::Constant(false)) => (),
1530
1531 (OpType::AllocatedTrue, OpType::True, Boolean::Is(_)) => (),
1532 (OpType::AllocatedTrue, OpType::False, Boolean::Constant(false)) => (),
1533 (OpType::AllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1534 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1535 assert_eq!(v.value(), Ok(true));
1536 }
1537 (OpType::AllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1538 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1539 assert_eq!(v.value(), Ok(false));
1540 }
1541 (OpType::AllocatedTrue, OpType::NegatedAllocatedTrue, Boolean::Is(ref v)) => {
1542 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1543 assert_eq!(v.value(), Ok(false));
1544 }
1545 (OpType::AllocatedTrue, OpType::NegatedAllocatedFalse, Boolean::Is(ref v)) => {
1546 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1547 assert_eq!(v.value(), Ok(true));
1548 }
1549
1550 (OpType::AllocatedFalse, OpType::True, Boolean::Is(_)) => (),
1551 (OpType::AllocatedFalse, OpType::False, Boolean::Constant(false)) => (),
1552 (OpType::AllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1553 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1554 assert_eq!(v.value(), Ok(false));
1555 }
1556 (OpType::AllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1557 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1558 assert_eq!(v.value(), Ok(false));
1559 }
1560 (OpType::AllocatedFalse, OpType::NegatedAllocatedTrue, Boolean::Is(ref v)) => {
1561 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1562 assert_eq!(v.value(), Ok(false));
1563 }
1564 (OpType::AllocatedFalse, OpType::NegatedAllocatedFalse, Boolean::Is(ref v)) => {
1565 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1566 assert_eq!(v.value(), Ok(false));
1567 }
1568
1569 (OpType::NegatedAllocatedTrue, OpType::True, Boolean::Not(_)) => (),
1570 (OpType::NegatedAllocatedTrue, OpType::False, Boolean::Constant(false)) => (),
1571 (OpType::NegatedAllocatedTrue, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1572 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1573 assert_eq!(v.value(), Ok(false));
1574 }
1575 (OpType::NegatedAllocatedTrue, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1576 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1577 assert_eq!(v.value(), Ok(false));
1578 }
1579 (
1580 OpType::NegatedAllocatedTrue,
1581 OpType::NegatedAllocatedTrue,
1582 Boolean::Is(ref v),
1583 ) => {
1584 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1585 assert_eq!(v.value(), Ok(false));
1586 }
1587 (
1588 OpType::NegatedAllocatedTrue,
1589 OpType::NegatedAllocatedFalse,
1590 Boolean::Is(ref v),
1591 ) => {
1592 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1593 assert_eq!(v.value(), Ok(false));
1594 }
1595
1596 (OpType::NegatedAllocatedFalse, OpType::True, Boolean::Not(_)) => (),
1597 (OpType::NegatedAllocatedFalse, OpType::False, Boolean::Constant(false)) => (),
1598 (OpType::NegatedAllocatedFalse, OpType::AllocatedTrue, Boolean::Is(ref v)) => {
1599 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1600 assert_eq!(v.value(), Ok(true));
1601 }
1602 (OpType::NegatedAllocatedFalse, OpType::AllocatedFalse, Boolean::Is(ref v)) => {
1603 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1604 assert_eq!(v.value(), Ok(false));
1605 }
1606 (
1607 OpType::NegatedAllocatedFalse,
1608 OpType::NegatedAllocatedTrue,
1609 Boolean::Is(ref v),
1610 ) => {
1611 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::zero());
1612 assert_eq!(v.value(), Ok(false));
1613 }
1614 (
1615 OpType::NegatedAllocatedFalse,
1616 OpType::NegatedAllocatedFalse,
1617 Boolean::Is(ref v),
1618 ) => {
1619 assert_eq!(cs.assigned_value(v.variable()).unwrap(), Fr::one());
1620 assert_eq!(v.value(), Ok(true));
1621 }
1622
1623 _ => {
1624 panic!(
1625 "unexpected behavior at {:?} AND {:?}",
1626 first_operand, second_operand
1627 );
1628 }
1629 }
1630 }
1631 }
1632 Ok(())
1633 }
1634
1635 #[test]
1636 fn test_smaller_than_or_equal_to() -> Result<(), SynthesisError> {
1637 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1638 for _ in 0..1000 {
1639 let mut r = Fr::rand(&mut rng);
1640 let mut s = Fr::rand(&mut rng);
1641 if r > s {
1642 core::mem::swap(&mut r, &mut s)
1643 }
1644
1645 let cs = ConstraintSystem::<Fr>::new_ref();
1646
1647 let native_bits: Vec<_> = BitIteratorLE::new(r.into_repr()).collect();
1648 let bits = Vec::new_witness(cs.clone(), || Ok(native_bits))?;
1649 Boolean::enforce_smaller_or_equal_than_le(&bits, s.into_repr())?;
1650
1651 assert!(cs.is_satisfied().unwrap());
1652 }
1653
1654 for _ in 0..1000 {
1655 let r = Fr::rand(&mut rng);
1656 if r == -Fr::one() {
1657 continue;
1658 }
1659 let s = r + Fr::one();
1660 let s2 = r.double();
1661 let cs = ConstraintSystem::<Fr>::new_ref();
1662
1663 let native_bits: Vec<_> = BitIteratorLE::new(r.into_repr()).collect();
1664 let bits = Vec::new_witness(cs.clone(), || Ok(native_bits))?;
1665 Boolean::enforce_smaller_or_equal_than_le(&bits, s.into_repr())?;
1666 if r < s2 {
1667 Boolean::enforce_smaller_or_equal_than_le(&bits, s2.into_repr())?;
1668 }
1669
1670 assert!(cs.is_satisfied().unwrap());
1671 }
1672 Ok(())
1673 }
1674
1675 #[test]
1676 fn test_enforce_in_field() -> Result<(), SynthesisError> {
1677 {
1678 let cs = ConstraintSystem::<Fr>::new_ref();
1679
1680 let mut bits = vec![];
1681 for b in BitIteratorBE::new(Fr::characteristic()).skip(1) {
1682 bits.push(Boolean::new_witness(cs.clone(), || Ok(b))?);
1683 }
1684 bits.reverse();
1685
1686 Boolean::enforce_in_field_le(&bits)?;
1687
1688 assert!(!cs.is_satisfied().unwrap());
1689 }
1690
1691 let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
1692
1693 for _ in 0..1000 {
1694 let r = Fr::rand(&mut rng);
1695 let cs = ConstraintSystem::<Fr>::new_ref();
1696
1697 let mut bits = vec![];
1698 for b in BitIteratorBE::new(r.into_repr()).skip(1) {
1699 bits.push(Boolean::new_witness(cs.clone(), || Ok(b))?);
1700 }
1701 bits.reverse();
1702
1703 Boolean::enforce_in_field_le(&bits)?;
1704
1705 assert!(cs.is_satisfied().unwrap());
1706 }
1707 Ok(())
1708 }
1709
1710 #[test]
1711 fn test_enforce_nand() -> Result<(), SynthesisError> {
1712 {
1713 let cs = ConstraintSystem::<Fr>::new_ref();
1714
1715 assert!(
1716 Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), false)?]).is_ok()
1717 );
1718 assert!(
1719 Boolean::enforce_kary_nand(&[Boolean::new_constant(cs.clone(), true)?]).is_err()
1720 );
1721 }
1722
1723 for i in 1..5 {
1724 // with every possible assignment for them
1725 for mut b in 0..(1 << i) {
1726 // with every possible negation
1727 for mut n in 0..(1 << i) {
1728 let cs = ConstraintSystem::<Fr>::new_ref();
1729
1730 let mut expected = true;
1731
1732 let mut bits = vec![];
1733 for _ in 0..i {
1734 expected &= b & 1 == 1;
1735
1736 let bit = if n & 1 == 1 {
1737 Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?
1738 } else {
1739 Boolean::new_witness(cs.clone(), || Ok(b & 1 == 0))?.not()
1740 };
1741 bits.push(bit);
1742
1743 b >>= 1;
1744 n >>= 1;
1745 }
1746
1747 let expected = !expected;
1748
1749 Boolean::enforce_kary_nand(&bits)?;
1750
1751 if expected {
1752 assert!(cs.is_satisfied().unwrap());
1753 } else {
1754 assert!(!cs.is_satisfied().unwrap());
1755 }
1756 }
1757 }
1758 }
1759 Ok(())
1760 }
1761
1762 #[test]
1763 fn test_kary_and() -> Result<(), SynthesisError> {
1764 // test different numbers of operands
1765 for i in 1..15 {
1766 // with every possible assignment for them
1767 for mut b in 0..(1 << i) {
1768 let cs = ConstraintSystem::<Fr>::new_ref();
1769
1770 let mut expected = true;
1771
1772 let mut bits = vec![];
1773 for _ in 0..i {
1774 expected &= b & 1 == 1;
1775 bits.push(Boolean::new_witness(cs.clone(), || Ok(b & 1 == 1))?);
1776 b >>= 1;
1777 }
1778
1779 let r = Boolean::kary_and(&bits)?;
1780
1781 assert!(cs.is_satisfied().unwrap());
1782
1783 if let Boolean::Is(ref r) = r {
1784 assert_eq!(r.value()?, expected);
1785 }
1786 }
1787 }
1788 Ok(())
1789 }
1790
1791 #[test]
1792 fn test_bits_to_fp() -> Result<(), SynthesisError> {
1793 use AllocationMode::*;
1794 let rng = &mut ark_std::test_rng();
1795 let cs = ConstraintSystem::<Fr>::new_ref();
1796
1797 let modes = [Input, Witness, Constant];
1798 for &mode in modes.iter() {
1799 for _ in 0..1000 {
1800 let f = Fr::rand(rng);
1801 let bits = BitIteratorLE::new(f.into_repr()).collect::<Vec<_>>();
1802 let bits: Vec<_> =
1803 AllocVar::new_variable(cs.clone(), || Ok(bits.as_slice()), mode)?;
1804 let f = AllocVar::new_variable(cs.clone(), || Ok(f), mode)?;
1805 let claimed_f = Boolean::le_bits_to_fp_var(&bits)?;
1806 claimed_f.enforce_equal(&f)?;
1807 }
1808
1809 for _ in 0..1000 {
1810 let f = Fr::from(u64::rand(rng));
1811 let bits = BitIteratorLE::new(f.into_repr()).collect::<Vec<_>>();
1812 let bits: Vec<_> =
1813 AllocVar::new_variable(cs.clone(), || Ok(bits.as_slice()), mode)?;
1814 let f = AllocVar::new_variable(cs.clone(), || Ok(f), mode)?;
1815 let claimed_f = Boolean::le_bits_to_fp_var(&bits)?;
1816 claimed_f.enforce_equal(&f)?;
1817 }
1818 assert!(cs.is_satisfied().unwrap());
1819 }
1820
1821 Ok(())
1822 }
1823}