ark_r1cs_std/boolean/
eq.rs

1use ark_relations::r1cs::SynthesisError;
2
3use crate::boolean::Boolean;
4use crate::eq::EqGadget;
5
6use super::*;
7
8impl<F: Field> EqGadget<F> for Boolean<F> {
9    #[tracing::instrument(target = "r1cs")]
10    fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
11        // self | other | XNOR(self, other) | self == other
12        // -----|-------|-------------------|--------------
13        //   0  |   0   |         1         |      1
14        //   0  |   1   |         0         |      0
15        //   1  |   0   |         0         |      0
16        //   1  |   1   |         1         |      1
17        Ok(!(self ^ other))
18    }
19
20    #[tracing::instrument(target = "r1cs")]
21    fn conditional_enforce_equal(
22        &self,
23        other: &Self,
24        condition: &Boolean<F>,
25    ) -> Result<(), SynthesisError> {
26        use Boolean::*;
27        let one = Variable::One;
28        // We will use the following trick: a == b <=> a - b == 0
29        // This works because a - b == 0 if and only if a = 0 and b = 0, or a = 1 and b = 1,
30        // which is exactly the definition of a == b.
31        let difference = match (self, other) {
32            // 1 == 1; 0 == 0
33            (Constant(true), Constant(true)) | (Constant(false), Constant(false)) => return Ok(()),
34            // false != true
35            (Constant(_), Constant(_)) => return Err(SynthesisError::Unsatisfiable),
36            // 1 - a
37            (Constant(true), Var(a)) | (Var(a), Constant(true)) => lc!() + one - a.variable(),
38            // a - 0 = a
39            (Constant(false), Var(a)) | (Var(a), Constant(false)) => lc!() + a.variable(),
40            // b - a,
41            (Var(a), Var(b)) => lc!() + b.variable() - a.variable(),
42        };
43
44        if condition != &Constant(false) {
45            let cs = self.cs().or(other.cs()).or(condition.cs());
46            cs.enforce_constraint(lc!() + difference, condition.lc(), lc!())?;
47        }
48        Ok(())
49    }
50
51    #[tracing::instrument(target = "r1cs")]
52    fn conditional_enforce_not_equal(
53        &self,
54        other: &Self,
55        should_enforce: &Boolean<F>,
56    ) -> Result<(), SynthesisError> {
57        use Boolean::*;
58        let one = Variable::One;
59        // We will use the following trick: a != b <=> a + b == 1
60        // This works because a + b == 1 if and only if a = 0 and b = 1, or a = 1 and b = 0,
61        // which is exactly the definition of a != b.
62        let sum = match (self, other) {
63            // 1 != 0; 0 != 1
64            (Constant(true), Constant(false)) | (Constant(false), Constant(true)) => return Ok(()),
65            // false == false and true == true
66            (Constant(_), Constant(_)) => return Err(SynthesisError::Unsatisfiable),
67            // 1 + a
68            (Constant(true), Var(a)) | (Var(a), Constant(true)) => lc!() + one + a.variable(),
69            // a + 0 = a
70            (Constant(false), Var(a)) | (Var(a), Constant(false)) => lc!() + a.variable(),
71            // b + a,
72            (Var(a), Var(b)) => lc!() + b.variable() + a.variable(),
73        };
74
75        if should_enforce != &Constant(false) {
76            let cs = self.cs().or(other.cs()).or(should_enforce.cs());
77            cs.enforce_constraint(sum, should_enforce.lc(), lc!() + one)?;
78        }
79        Ok(())
80    }
81}
82
83#[cfg(test)]
84mod tests {
85    use super::*;
86    use crate::{
87        alloc::{AllocVar, AllocationMode},
88        boolean::test_utils::{run_binary_exhaustive, run_unary_exhaustive},
89        prelude::EqGadget,
90        R1CSVar,
91    };
92    use ark_test_curves::bls12_381::Fr;
93
94    #[test]
95    fn eq() {
96        run_binary_exhaustive::<Fr>(|a, b| {
97            let cs = a.cs().or(b.cs());
98            let both_constant = a.is_constant() && b.is_constant();
99            let computed = &a.is_eq(&b)?;
100            let expected_mode = if both_constant {
101                AllocationMode::Constant
102            } else {
103                AllocationMode::Witness
104            };
105            let expected =
106                Boolean::new_variable(cs.clone(), || Ok(a.value()? == b.value()?), expected_mode)?;
107            assert_eq!(expected.value(), computed.value());
108            expected.enforce_equal(&computed)?;
109            if !both_constant {
110                assert!(cs.is_satisfied().unwrap());
111            }
112            Ok(())
113        })
114        .unwrap()
115    }
116
117    #[test]
118    fn neq() {
119        run_binary_exhaustive::<Fr>(|a, b| {
120            let cs = a.cs().or(b.cs());
121            let both_constant = a.is_constant() && b.is_constant();
122            let computed = &a.is_neq(&b)?;
123            let expected_mode = if both_constant {
124                AllocationMode::Constant
125            } else {
126                AllocationMode::Witness
127            };
128            let expected =
129                Boolean::new_variable(cs.clone(), || Ok(a.value()? != b.value()?), expected_mode)?;
130            assert_eq!(expected.value(), computed.value());
131            expected.enforce_equal(&computed)?;
132            if !both_constant {
133                assert!(cs.is_satisfied().unwrap());
134            }
135            Ok(())
136        })
137        .unwrap()
138    }
139
140    #[test]
141    fn neq_and_eq_consistency() {
142        run_binary_exhaustive::<Fr>(|a, b| {
143            let cs = a.cs().or(b.cs());
144            let both_constant = a.is_constant() && b.is_constant();
145            let is_neq = &a.is_neq(&b)?;
146            let is_eq = &a.is_eq(&b)?;
147            let expected_mode = if both_constant {
148                AllocationMode::Constant
149            } else {
150                AllocationMode::Witness
151            };
152            let expected_is_neq =
153                Boolean::new_variable(cs.clone(), || Ok(a.value()? != b.value()?), expected_mode)?;
154            assert_eq!(expected_is_neq.value(), is_neq.value());
155            assert_ne!(expected_is_neq.value(), is_eq.value());
156            expected_is_neq.enforce_equal(is_neq)?;
157            expected_is_neq.enforce_equal(&!is_eq)?;
158            expected_is_neq.enforce_not_equal(is_eq)?;
159            if !both_constant {
160                assert!(cs.is_satisfied().unwrap());
161            }
162            Ok(())
163        })
164        .unwrap()
165    }
166
167    #[test]
168    fn enforce_eq_and_enforce_neq_consistency() {
169        run_unary_exhaustive::<Fr>(|a| {
170            let cs = a.cs();
171            let not_a = !&a;
172            a.enforce_equal(&a)?;
173            not_a.enforce_equal(&not_a)?;
174            a.enforce_not_equal(&not_a)?;
175            not_a.enforce_not_equal(&a)?;
176            if !a.is_constant() {
177                assert!(cs.is_satisfied().unwrap());
178            }
179            Ok(())
180        })
181        .unwrap()
182    }
183
184    #[test]
185    fn eq_soundness() {
186        run_binary_exhaustive::<Fr>(|a, b| {
187            let cs = a.cs().or(b.cs());
188            let both_constant = a.is_constant() && b.is_constant();
189            let computed = &a.is_eq(&b)?;
190            let expected_mode = if both_constant {
191                AllocationMode::Constant
192            } else {
193                AllocationMode::Witness
194            };
195            let expected =
196                Boolean::new_variable(cs.clone(), || Ok(a.value()? != b.value()?), expected_mode)?;
197            assert_ne!(expected.value(), computed.value());
198            expected.enforce_not_equal(&computed)?;
199            if !both_constant {
200                assert!(cs.is_satisfied().unwrap());
201            }
202            Ok(())
203        })
204        .unwrap()
205    }
206
207    #[test]
208    fn neq_soundness() {
209        run_binary_exhaustive::<Fr>(|a, b| {
210            let cs = a.cs().or(b.cs());
211            let both_constant = a.is_constant() && b.is_constant();
212            let computed = &a.is_neq(&b)?;
213            let expected_mode = if both_constant {
214                AllocationMode::Constant
215            } else {
216                AllocationMode::Witness
217            };
218            let expected =
219                Boolean::new_variable(cs.clone(), || Ok(a.value()? == b.value()?), expected_mode)?;
220            assert_ne!(expected.value(), computed.value());
221            expected.enforce_not_equal(&computed)?;
222            if !both_constant {
223                assert!(cs.is_satisfied().unwrap());
224            }
225            Ok(())
226        })
227        .unwrap()
228    }
229}
ark_r1cs_std/boolean/eq.rs

ark_r1cs_std/boolean/
eq.rs
