ark-r1cs-std/src/boolean/allocated.rs
src/boolean/allocated.rsRaw
1use core::borrow::{Borrow, BorrowMut};
2
3use ark_ff::{Field, PrimeField};
4use ark_relations::r1cs::{ConstraintSystemRef, Namespace, SynthesisError, Variable};
5
6use crate::{
7 alloc::{AllocVar, AllocationMode},
8 select::CondSelectGadget,
9};
10
11use super::Boolean;
12
13/// Represents a variable in the constraint system which is guaranteed
14/// to be either zero or one.
15///
16/// In general, one should prefer using `Boolean` instead of `AllocatedBool`,
17/// as `Boolean` offers better support for constant values, and implements
18/// more traits.
19#[derive(Clone, Debug, Eq, PartialEq)]
20#[must_use]
21pub struct AllocatedBool<F: Field> {
22 pub(super) variable: Variable,
23 pub(super) cs: ConstraintSystemRef<F>,
24 pub(super) enable_lc: bool,
25 pub(super) value: Option<bool>,
26}
27
28impl<F: Field> AllocatedBool<F> {
29 /// Get the assigned value for `self`.
30 pub fn value(&self) -> Result<bool, SynthesisError> {
31 self.value.ok_or(SynthesisError::AssignmentMissing)
32 }
33
34 /// Get the R1CS variable for `self`.
35 pub fn variable(&self) -> Variable {
36 self.variable
37 }
38
39 /// Allocate a witness variable without a booleanity check.
40 #[doc(hidden)]
41 pub fn new_witness_without_booleanity_check<T: Borrow<bool>>(
42 cs: ConstraintSystemRef<F>,
43 f: impl FnOnce() -> Result<T, SynthesisError>,
44 ) -> Result<Self, SynthesisError> {
45 let value = f().map(|b| *b.borrow());
46 Ok(Self {
47 variable: cs.new_witness_variable(|| value.map(F::from))?,
48 enable_lc: cs.should_construct_matrices(),
49 cs,
50 value: value.ok(),
51 })
52 }
53
54 /// Performs an XOR operation over the two operands, returning
55 /// an `AllocatedBool`.
56 #[tracing::instrument(target = "r1cs")]
57 pub fn not(&self) -> Result<Self, SynthesisError> {
58 let variable = self.cs.new_lc(if self.enable_lc {
59 lc!() + Variable::One - self.variable
60 } else {
61 lc!()
62 })?;
63 Ok(Self {
64 variable,
65 cs: self.cs.clone(),
66 value: self.value.map(|v| !v),
67 enable_lc: self.cs.should_construct_matrices()
68 })
69 }
70
71 /// Performs an XOR operation over the two operands, returning
72 /// an `AllocatedBool`.
73 #[tracing::instrument(target = "r1cs")]
74 pub fn xor(&self, b: &Self) -> Result<Self, SynthesisError> {
75 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
76 Ok(self.value()? ^ b.value()?)
77 })?;
78
79 // Constrain (a + a) * (b) = (a + b - c)
80 // Given that a and b are boolean constrained, if they
81 // are equal, the only solution for c is 0, and if they
82 // are different, the only solution for c is 1.
83 //
84 // ¬(a ∧ b) ∧ ¬(¬a ∧ ¬b) = c
85 // (1 - (a * b)) * (1 - ((1 - a) * (1 - b))) = c
86 // (1 - ab) * (1 - (1 - a - b + ab)) = c
87 // (1 - ab) * (a + b - ab) = c
88 // a + b - ab - (a^2)b - (b^2)a + (a^2)(b^2) = c
89 // a + b - ab - ab - ab + ab = c
90 // a + b - 2ab = c
91 // -2a * b = c - a - b
92 // 2a * b = a + b - c
93 // (a + a) * b = a + b - c
94 if self.enable_lc {
95 self.cs.enforce_constraint(
96 lc!() + self.variable + self.variable,
97 lc!() + b.variable,
98 lc!() + self.variable + b.variable - result.variable,
99 )?;
100 } else {
101 self.cs.borrow_mut().unwrap().num_constraints += 1;
102 }
103
104 Ok(result)
105 }
106
107 /// Performs an AND operation over the two operands, returning
108 /// an `AllocatedBool`.
109 #[tracing::instrument(target = "r1cs")]
110 pub fn and(&self, b: &Self) -> Result<Self, SynthesisError> {
111 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
112 Ok(self.value()? & b.value()?)
113 })?;
114
115 // Constrain (a) * (b) = (c), ensuring c is 1 iff
116 // a AND b are both 1.
117 if self.enable_lc {
118 self.cs.enforce_constraint(
119 lc!() + self.variable,
120 lc!() + b.variable,
121 lc!() + result.variable,
122 )?;
123 } else {
124 self.cs.borrow_mut().unwrap().num_constraints += 1;
125 }
126
127 Ok(result)
128 }
129
130 /// Performs an OR operation over the two operands, returning
131 /// an `AllocatedBool`.
132 #[tracing::instrument(target = "r1cs")]
133 pub fn or(&self, b: &Self) -> Result<Self, SynthesisError> {
134 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
135 Ok(self.value()? | b.value()?)
136 })?;
137
138 // Constrain (1 - a) * (1 - b) = (1 - c), ensuring c is 0 iff
139 // a and b are both false, and otherwise c is 1.
140 if self.enable_lc {
141 self.cs.enforce_constraint(
142 lc!() + Variable::One - self.variable,
143 lc!() + Variable::One - b.variable,
144 lc!() + Variable::One - result.variable,
145 )?;
146 } else {
147 self.cs.borrow_mut().unwrap().num_constraints += 1;
148 }
149
150 Ok(result)
151 }
152
153 /// Calculates `a AND (NOT b)`.
154 #[tracing::instrument(target = "r1cs")]
155 pub fn and_not(&self, b: &Self) -> Result<Self, SynthesisError> {
156 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
157 Ok(self.value()? & !b.value()?)
158 })?;
159
160 // Constrain (a) * (1 - b) = (c), ensuring c is 1 iff
161 // a is true and b is false, and otherwise c is 0.
162 if self.enable_lc {
163 self.cs.enforce_constraint(
164 lc!() + self.variable,
165 lc!() + Variable::One - b.variable,
166 lc!() + result.variable,
167 )?;
168 } else {
169 self.cs.borrow_mut().unwrap().num_constraints += 1;
170 }
171
172 Ok(result)
173 }
174
175 /// Calculates `(NOT a) AND (NOT b)`.
176 #[tracing::instrument(target = "r1cs")]
177 pub fn nor(&self, b: &Self) -> Result<Self, SynthesisError> {
178 let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
179 Ok(!(self.value()? | b.value()?))
180 })?;
181
182 // Constrain (1 - a) * (1 - b) = (c), ensuring c is 1 iff
183 // a and b are both false, and otherwise c is 0.
184 if self.enable_lc {
185 self.cs.enforce_constraint(
186 lc!() + Variable::One - self.variable,
187 lc!() + Variable::One - b.variable,
188 lc!() + result.variable,
189 )?;
190 } else {
191 self.cs.borrow_mut().unwrap().num_constraints += 1;
192 }
193
194 Ok(result)
195 }
196}
197
198impl<F: Field> AllocVar<bool, F> for AllocatedBool<F> {
199 /// Produces a new variable of the appropriate kind
200 /// (instance or witness), with a booleanity check.
201 ///
202 /// N.B.: we could omit the booleanity check when allocating `self`
203 /// as a new public input, but that places an additional burden on
204 /// protocol designers. Better safe than sorry!
205 fn new_variable<T: Borrow<bool>>(
206 cs: impl Into<Namespace<F>>,
207 f: impl FnOnce() -> Result<T, SynthesisError>,
208 mode: AllocationMode,
209 ) -> Result<Self, SynthesisError> {
210 let ns = cs.into();
211 let cs = ns.cs();
212 if mode == AllocationMode::Constant {
213 let value = *f()?.borrow();
214 Ok(Self {
215 variable: if value { Variable::One } else { Variable::Zero },
216 enable_lc: cs.should_construct_matrices(),
217 cs,
218 value: Some(value),
219 })
220 } else {
221 let value = f().map(|b| *b.borrow());
222 let variable = if mode == AllocationMode::Input {
223 cs.new_input_variable(|| value.map(F::from))?
224 } else {
225 cs.new_witness_variable(|| value.map(F::from))?
226 };
227
228 let enable_lc = cs.should_construct_matrices();
229
230 // Constrain: (1 - a) * a = 0
231 // This constrains a to be either 0 or 1.
232 if enable_lc {
233 cs.enforce_constraint(lc!() + Variable::One - variable, lc!() + variable, lc!())?;
234 } else {
235 cs.borrow_mut().unwrap().num_constraints += 1;
236 }
237
238 Ok(Self {
239 variable,
240 enable_lc,
241 cs,
242 value: value.ok(),
243 })
244 }
245 }
246}
247
248impl<F: PrimeField> CondSelectGadget<F> for AllocatedBool<F> {
249 #[tracing::instrument(target = "r1cs")]
250 fn conditionally_select(
251 cond: &Boolean<F>,
252 true_val: &Self,
253 false_val: &Self,
254 ) -> Result<Self, SynthesisError> {
255 let res = Boolean::conditionally_select(
256 cond,
257 &true_val.clone().into(),
258 &false_val.clone().into(),
259 )?;
260 match res {
261 Boolean::Var(a) => Ok(a),
262 _ => unreachable!("Impossible"),
263 }
264 }
265}
266
267#[cfg(test)]
268mod test {
269 use super::*;
270
271 use ark_relations::r1cs::ConstraintSystem;
272 use ark_test_curves::bls12_381::Fr;
273 #[test]
274 fn allocated_xor() -> Result<(), SynthesisError> {
275 for a_val in [false, true].iter().copied() {
276 for b_val in [false, true].iter().copied() {
277 let cs = ConstraintSystem::<Fr>::new_ref();
278 let a = AllocatedBool::new_witness(cs.clone(), || Ok(a_val))?;
279 let b = AllocatedBool::new_witness(cs.clone(), || Ok(b_val))?;
280 let c = AllocatedBool::xor(&a, &b)?;
281 assert_eq!(c.value()?, a_val ^ b_val);
282
283 assert!(cs.is_satisfied().unwrap());
284 assert_eq!(a.value()?, (a_val));
285 assert_eq!(b.value()?, (b_val));
286 assert_eq!(c.value()?, (a_val ^ b_val));
287 }
288 }
289 Ok(())
290 }
291
292 #[test]
293 fn allocated_or() -> Result<(), SynthesisError> {
294 for a_val in [false, true].iter().copied() {
295 for b_val in [false, true].iter().copied() {
296 let cs = ConstraintSystem::<Fr>::new_ref();
297 let a = AllocatedBool::new_witness(cs.clone(), || Ok(a_val))?;
298 let b = AllocatedBool::new_witness(cs.clone(), || Ok(b_val))?;
299 let c = AllocatedBool::or(&a, &b)?;
300 assert_eq!(c.value()?, a_val | b_val);
301
302 assert!(cs.is_satisfied().unwrap());
303 assert_eq!(a.value()?, (a_val));
304 assert_eq!(b.value()?, (b_val));
305 assert_eq!(c.value()?, (a_val | b_val));
306 }
307 }
308 Ok(())
309 }
310
311 #[test]
312 fn allocated_and() -> Result<(), SynthesisError> {
313 for a_val in [false, true].iter().copied() {
314 for b_val in [false, true].iter().copied() {
315 let cs = ConstraintSystem::<Fr>::new_ref();
316 let a = AllocatedBool::new_witness(cs.clone(), || Ok(a_val))?;
317 let b = AllocatedBool::new_witness(cs.clone(), || Ok(b_val))?;
318 let c = AllocatedBool::and(&a, &b)?;
319 assert_eq!(c.value()?, a_val & b_val);
320
321 assert!(cs.is_satisfied().unwrap());
322 assert_eq!(a.value()?, (a_val));
323 assert_eq!(b.value()?, (b_val));
324 assert_eq!(c.value()?, (a_val & b_val));
325 }
326 }
327 Ok(())
328 }
329
330 #[test]
331 fn allocated_and_not() -> Result<(), SynthesisError> {
332 for a_val in [false, true].iter().copied() {
333 for b_val in [false, true].iter().copied() {
334 let cs = ConstraintSystem::<Fr>::new_ref();
335 let a = AllocatedBool::new_witness(cs.clone(), || Ok(a_val))?;
336 let b = AllocatedBool::new_witness(cs.clone(), || Ok(b_val))?;
337 let c = AllocatedBool::and_not(&a, &b)?;
338 assert_eq!(c.value()?, a_val & !b_val);
339
340 assert!(cs.is_satisfied().unwrap());
341 assert_eq!(a.value()?, (a_val));
342 assert_eq!(b.value()?, (b_val));
343 assert_eq!(c.value()?, (a_val & !b_val));
344 }
345 }
346 Ok(())
347 }
348
349 #[test]
350 fn allocated_nor() -> Result<(), SynthesisError> {
351 for a_val in [false, true].iter().copied() {
352 for b_val in [false, true].iter().copied() {
353 let cs = ConstraintSystem::<Fr>::new_ref();
354 let a = AllocatedBool::new_witness(cs.clone(), || Ok(a_val))?;
355 let b = AllocatedBool::new_witness(cs.clone(), || Ok(b_val))?;
356 let c = AllocatedBool::nor(&a, &b)?;
357 assert_eq!(c.value()?, !a_val & !b_val);
358
359 assert!(cs.is_satisfied().unwrap());
360 assert_eq!(a.value()?, (a_val));
361 assert_eq!(b.value()?, (b_val));
362 assert_eq!(c.value()?, (!a_val & !b_val));
363 }
364 }
365 Ok(())
366 }
367}