15
15
16
16
use super :: * ;
17
17
18
+ fn boolean_witness < E : Environment > ( first : & Boolean < E > , second : & Boolean < E > ) -> Boolean < E > {
19
+ Boolean (
20
+ E :: new_variable ( Mode :: Private , match first. eject_value ( ) ^ second. eject_value ( ) {
21
+ true => E :: BaseField :: one ( ) ,
22
+ false => E :: BaseField :: zero ( ) ,
23
+ } )
24
+ . into ( ) ,
25
+ )
26
+ }
27
+
18
28
impl < E : Environment > BitXor < Boolean < E > > for Boolean < E > {
19
29
type Output = Boolean < E > ;
20
30
@@ -39,13 +49,7 @@ impl<E: Environment> BitXor<Boolean<E>> for Boolean<E> {
39
49
// Declare a new variable with the expected output as witness.
40
50
// Note: The constraint below will ensure `output` is either 0 or 1,
41
51
// assuming `self` and `other` are well-formed (they are either 0 or 1).
42
- let output = Boolean (
43
- E :: new_variable ( Mode :: Private , match self . eject_value ( ) ^ other. eject_value ( ) {
44
- true => E :: BaseField :: one ( ) ,
45
- false => E :: BaseField :: zero ( ) ,
46
- } )
47
- . into ( ) ,
48
- ) ;
52
+ let output = boolean_witness ( & self , & other) ;
49
53
50
54
//
51
55
// Ensure (`self` + `self`) * (`other`) = (`self` + `other` - `output`)
@@ -77,55 +81,19 @@ impl<E: Environment> BitXor<Boolean<E>> for Boolean<E> {
77
81
impl < E : Environment > BitXor < Boolean < E > > for & Boolean < E > {
78
82
type Output = Boolean < E > ;
79
83
80
- /// Returns `(self != other)`.
81
84
fn bitxor ( self , other : Boolean < E > ) -> Self :: Output {
82
- // Constant `self`
83
85
if self . is_constant ( ) {
84
86
match self . eject_value ( ) {
85
87
true => !other,
86
88
false => other,
87
89
}
88
- }
89
- // Constant `other`
90
- else if other. is_constant ( ) {
90
+ } else if other. is_constant ( ) {
91
91
match other. eject_value ( ) {
92
92
true => !self . clone ( ) ,
93
93
false => self . clone ( ) ,
94
94
}
95
- }
96
- // Variable != Variable
97
- else {
98
- // Declare a new variable with the expected output as witness.
99
- // Note: The constraint below will ensure `output` is either 0 or 1,
100
- // assuming `self` and `other` are well-formed (they are either 0 or 1).
101
- let output = Boolean (
102
- E :: new_variable ( Mode :: Private , match self . eject_value ( ) ^ other. eject_value ( ) {
103
- true => E :: BaseField :: one ( ) ,
104
- false => E :: BaseField :: zero ( ) ,
105
- } )
106
- . into ( ) ,
107
- ) ;
108
-
109
- //
110
- // Ensure (`self` + `self`) * (`other`) = (`self` + `other` - `output`)
111
- // `output` is `1` iff `self` != `other`.
112
- //
113
- // As `self` and `other` are enforced to be `Boolean` types,
114
- // if they are equal, then the `output` is 0,
115
- // and if they are different, then `output` must be 1.
116
- //
117
- // ¬(a ∧ b) ∧ ¬(¬a ∧ ¬b) = c
118
- //
119
- // (1 - (a * b)) * (1 - ((1 - a) * (1 - b))) = c
120
- // (1 - ab) * (1 - (1 - a - b + ab)) = c
121
- // (1 - ab) * (a + b - ab) = c
122
- // a + b - ab - (a^2)b - (b^2)a + (a^2)(b^2) = c
123
- // a + b - ab - ab - ab + ab = c
124
- // a + b - 2ab = c
125
- // -2a * b = c - a - b
126
- // 2a * b = a + b - c
127
- // (a + a) * b = a + b - c
128
- //
95
+ } else {
96
+ let output = boolean_witness ( self , & other) ;
129
97
E :: enforce ( || ( ( & self . 0 + & self . 0 ) , & other, ( & self . 0 + & other. 0 - & output. 0 ) ) ) ;
130
98
131
99
output
@@ -136,55 +104,19 @@ impl<E: Environment> BitXor<Boolean<E>> for &Boolean<E> {
136
104
impl < E : Environment > BitXor < & Boolean < E > > for Boolean < E > {
137
105
type Output = Boolean < E > ;
138
106
139
- /// Returns `(self != other)`.
140
107
fn bitxor ( self , other : & Boolean < E > ) -> Self :: Output {
141
- // Constant `self`
142
108
if self . is_constant ( ) {
143
109
match self . eject_value ( ) {
144
110
true => !other. clone ( ) ,
145
111
false => other. clone ( ) ,
146
112
}
147
- }
148
- // Constant `other`
149
- else if other. is_constant ( ) {
113
+ } else if other. is_constant ( ) {
150
114
match other. eject_value ( ) {
151
115
true => !self ,
152
116
false => self ,
153
117
}
154
- }
155
- // Variable != Variable
156
- else {
157
- // Declare a new variable with the expected output as witness.
158
- // Note: The constraint below will ensure `output` is either 0 or 1,
159
- // assuming `self` and `other` are well-formed (they are either 0 or 1).
160
- let output = Boolean (
161
- E :: new_variable ( Mode :: Private , match self . eject_value ( ) ^ other. eject_value ( ) {
162
- true => E :: BaseField :: one ( ) ,
163
- false => E :: BaseField :: zero ( ) ,
164
- } )
165
- . into ( ) ,
166
- ) ;
167
-
168
- //
169
- // Ensure (`self` + `self`) * (`other`) = (`self` + `other` - `output`)
170
- // `output` is `1` iff `self` != `other`.
171
- //
172
- // As `self` and `other` are enforced to be `Boolean` types,
173
- // if they are equal, then the `output` is 0,
174
- // and if they are different, then `output` must be 1.
175
- //
176
- // ¬(a ∧ b) ∧ ¬(¬a ∧ ¬b) = c
177
- //
178
- // (1 - (a * b)) * (1 - ((1 - a) * (1 - b))) = c
179
- // (1 - ab) * (1 - (1 - a - b + ab)) = c
180
- // (1 - ab) * (a + b - ab) = c
181
- // a + b - ab - (a^2)b - (b^2)a + (a^2)(b^2) = c
182
- // a + b - ab - ab - ab + ab = c
183
- // a + b - 2ab = c
184
- // -2a * b = c - a - b
185
- // 2a * b = a + b - c
186
- // (a + a) * b = a + b - c
187
- //
118
+ } else {
119
+ let output = boolean_witness ( & self , other) ;
188
120
E :: enforce ( || ( ( & self . 0 + & self . 0 ) , other, ( self . 0 + & other. 0 - & output. 0 ) ) ) ;
189
121
190
122
output
@@ -195,55 +127,19 @@ impl<E: Environment> BitXor<&Boolean<E>> for Boolean<E> {
195
127
impl < E : Environment > BitXor < & Boolean < E > > for & Boolean < E > {
196
128
type Output = Boolean < E > ;
197
129
198
- /// Returns `(self != other)`.
199
130
fn bitxor ( self , other : & Boolean < E > ) -> Self :: Output {
200
- // Constant `self`
201
131
if self . is_constant ( ) {
202
132
match self . eject_value ( ) {
203
133
true => !other. clone ( ) ,
204
134
false => other. clone ( ) ,
205
135
}
206
- }
207
- // Constant `other`
208
- else if other. is_constant ( ) {
136
+ } else if other. is_constant ( ) {
209
137
match other. eject_value ( ) {
210
138
true => !self . clone ( ) ,
211
139
false => self . clone ( ) ,
212
140
}
213
- }
214
- // Variable != Variable
215
- else {
216
- // Declare a new variable with the expected output as witness.
217
- // Note: The constraint below will ensure `output` is either 0 or 1,
218
- // assuming `self` and `other` are well-formed (they are either 0 or 1).
219
- let output = Boolean (
220
- E :: new_variable ( Mode :: Private , match self . eject_value ( ) ^ other. eject_value ( ) {
221
- true => E :: BaseField :: one ( ) ,
222
- false => E :: BaseField :: zero ( ) ,
223
- } )
224
- . into ( ) ,
225
- ) ;
226
-
227
- //
228
- // Ensure (`self` + `self`) * (`other`) = (`self` + `other` - `output`)
229
- // `output` is `1` iff `self` != `other`.
230
- //
231
- // As `self` and `other` are enforced to be `Boolean` types,
232
- // if they are equal, then the `output` is 0,
233
- // and if they are different, then `output` must be 1.
234
- //
235
- // ¬(a ∧ b) ∧ ¬(¬a ∧ ¬b) = c
236
- //
237
- // (1 - (a * b)) * (1 - ((1 - a) * (1 - b))) = c
238
- // (1 - ab) * (1 - (1 - a - b + ab)) = c
239
- // (1 - ab) * (a + b - ab) = c
240
- // a + b - ab - (a^2)b - (b^2)a + (a^2)(b^2) = c
241
- // a + b - ab - ab - ab + ab = c
242
- // a + b - 2ab = c
243
- // -2a * b = c - a - b
244
- // 2a * b = a + b - c
245
- // (a + a) * b = a + b - c
246
- //
141
+ } else {
142
+ let output = boolean_witness ( self , other) ;
247
143
E :: enforce ( || ( ( & self . 0 + & self . 0 ) , other, ( & self . 0 + & other. 0 - & output. 0 ) ) ) ;
248
144
249
145
output
@@ -252,120 +148,44 @@ impl<E: Environment> BitXor<&Boolean<E>> for &Boolean<E> {
252
148
}
253
149
254
150
impl < E : Environment > BitXorAssign < Boolean < E > > for Boolean < E > {
255
- /// Sets `self` as `(self != other)`.
256
151
fn bitxor_assign ( & mut self , other : Boolean < E > ) {
257
- // Stores the bitwise XOR of `self` and `other` in `self`.
258
- * self =
259
- // Constant `self`
260
- if self . is_constant ( ) {
261
- match self . eject_value ( ) {
262
- true => !other,
263
- false => other,
264
- }
265
- }
266
- // Constant `other`
267
- else if other. is_constant ( ) {
268
- match other. eject_value ( ) {
269
- true => !self . clone ( ) ,
270
- false => self . clone ( ) ,
271
- }
152
+ * self = if self . is_constant ( ) {
153
+ match self . eject_value ( ) {
154
+ true => !other,
155
+ false => other,
272
156
}
273
- // Variable != Variable
274
- else {
275
- // Declare a new variable with the expected output as witness.
276
- // Note: The constraint below will ensure `output` is either 0 or 1,
277
- // assuming `self` and `other` are well-formed (they are either 0 or 1).
278
- let output = Boolean (
279
- E :: new_variable ( Mode :: Private , match self . eject_value ( ) ^ other. eject_value ( ) {
280
- true => E :: BaseField :: one ( ) ,
281
- false => E :: BaseField :: zero ( ) ,
282
- } )
283
- . into ( ) ,
284
- ) ;
285
-
286
- //
287
- // Ensure (`self` + `self`) * (`other`) = (`self` + `other` - `output`)
288
- // `output` is `1` iff `self` != `other`.
289
- //
290
- // As `self` and `other` are enforced to be `Boolean` types,
291
- // if they are equal, then the `output` is 0,
292
- // and if they are different, then `output` must be 1.
293
- //
294
- // ¬(a ∧ b) ∧ ¬(¬a ∧ ¬b) = c
295
- //
296
- // (1 - (a * b)) * (1 - ((1 - a) * (1 - b))) = c
297
- // (1 - ab) * (1 - (1 - a - b + ab)) = c
298
- // (1 - ab) * (a + b - ab) = c
299
- // a + b - ab - (a^2)b - (b^2)a + (a^2)(b^2) = c
300
- // a + b - ab - ab - ab + ab = c
301
- // a + b - 2ab = c
302
- // -2a * b = c - a - b
303
- // 2a * b = a + b - c
304
- // (a + a) * b = a + b - c
305
- //
306
- E :: enforce ( || ( ( & self . 0 + & self . 0 ) , & other, ( & self . 0 + & other. 0 - & output. 0 ) ) ) ;
307
-
308
- output
157
+ } else if other. is_constant ( ) {
158
+ match other. eject_value ( ) {
159
+ true => !self . clone ( ) ,
160
+ false => self . clone ( ) ,
309
161
}
162
+ } else {
163
+ let output = boolean_witness ( self , & other) ;
164
+ E :: enforce ( || ( ( & self . 0 + & self . 0 ) , & other, ( & self . 0 + & other. 0 - & output. 0 ) ) ) ;
165
+
166
+ output
167
+ }
310
168
}
311
169
}
312
170
313
171
impl < E : Environment > BitXorAssign < & Boolean < E > > for Boolean < E > {
314
- /// Sets `self` as `(self != other)`.
315
172
fn bitxor_assign ( & mut self , other : & Boolean < E > ) {
316
- // Stores the bitwise XOR of `self` and `other` in `self`.
317
- * self =
318
- // Constant `self`
319
- if self . is_constant ( ) {
320
- match self . eject_value ( ) {
321
- true => !other. clone ( ) ,
322
- false => other. clone ( ) ,
323
- }
324
- }
325
- // Constant `other`
326
- else if other. is_constant ( ) {
327
- match other. eject_value ( ) {
328
- true => !self . clone ( ) ,
329
- false => self . clone ( ) ,
330
- }
173
+ * self = if self . is_constant ( ) {
174
+ match self . eject_value ( ) {
175
+ true => !other. clone ( ) ,
176
+ false => other. clone ( ) ,
331
177
}
332
- // Variable != Variable
333
- else {
334
- // Declare a new variable with the expected output as witness.
335
- // Note: The constraint below will ensure `output` is either 0 or 1,
336
- // assuming `self` and `other` are well-formed (they are either 0 or 1).
337
- let output = Boolean (
338
- E :: new_variable ( Mode :: Private , match self . eject_value ( ) ^ other. eject_value ( ) {
339
- true => E :: BaseField :: one ( ) ,
340
- false => E :: BaseField :: zero ( ) ,
341
- } )
342
- . into ( ) ,
343
- ) ;
344
-
345
- //
346
- // Ensure (`self` + `self`) * (`other`) = (`self` + `other` - `output`)
347
- // `output` is `1` iff `self` != `other`.
348
- //
349
- // As `self` and `other` are enforced to be `Boolean` types,
350
- // if they are equal, then the `output` is 0,
351
- // and if they are different, then `output` must be 1.
352
- //
353
- // ¬(a ∧ b) ∧ ¬(¬a ∧ ¬b) = c
354
- //
355
- // (1 - (a * b)) * (1 - ((1 - a) * (1 - b))) = c
356
- // (1 - ab) * (1 - (1 - a - b + ab)) = c
357
- // (1 - ab) * (a + b - ab) = c
358
- // a + b - ab - (a^2)b - (b^2)a + (a^2)(b^2) = c
359
- // a + b - ab - ab - ab + ab = c
360
- // a + b - 2ab = c
361
- // -2a * b = c - a - b
362
- // 2a * b = a + b - c
363
- // (a + a) * b = a + b - c
364
- //
365
- E :: enforce ( || ( ( & self . 0 + & self . 0 ) , other, ( & self . 0 + & other. 0 - & output. 0 ) ) ) ;
366
-
367
- output
178
+ } else if other. is_constant ( ) {
179
+ match other. eject_value ( ) {
180
+ true => !self . clone ( ) ,
181
+ false => self . clone ( ) ,
368
182
}
183
+ } else {
184
+ let output = boolean_witness ( self , other) ;
185
+ E :: enforce ( || ( ( & self . 0 + & self . 0 ) , other, ( & self . 0 + & other. 0 - & output. 0 ) ) ) ;
186
+
187
+ output
188
+ }
369
189
}
370
190
}
371
191
0 commit comments