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