You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

1898 lines
68 KiB

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