ark-r1cs-std/src/boolean/eq.rs
src/boolean/eq.rsRaw
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(¬_a)?;
174 a.enforce_not_equal(¬_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}