ark_r1cs_std/boolean/
allocated.rs

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