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