Commit | Line | Data |
---|---|---|
51e44864 JG |
1 | /** @file |
2 | ***************************************************************************** | |
3 | * @author This file is part of libsnark, developed by SCIPR Lab | |
4 | * and contributors (see AUTHORS). | |
5 | * @copyright MIT license (see LICENSE file) | |
6 | *****************************************************************************/ | |
7 | ||
8 | #ifndef BASIC_GADGETS_TCC_ | |
9 | #define BASIC_GADGETS_TCC_ | |
10 | ||
11 | #include "common/profiling.hpp" | |
12 | #include "common/utils.hpp" | |
13 | ||
14 | namespace libsnark { | |
15 | ||
16 | template<typename FieldT> | |
17 | void generate_boolean_r1cs_constraint(protoboard<FieldT> &pb, const pb_linear_combination<FieldT> &lc, const std::string &annotation_prefix) | |
18 | /* forces lc to take value 0 or 1 by adding constraint lc * (1-lc) = 0 */ | |
19 | { | |
20 | pb.add_r1cs_constraint(r1cs_constraint<FieldT>(lc, 1-lc, 0), | |
21 | FMT(annotation_prefix, " boolean_r1cs_constraint")); | |
22 | } | |
23 | ||
24 | template<typename FieldT> | |
25 | void generate_r1cs_equals_const_constraint(protoboard<FieldT> &pb, const pb_linear_combination<FieldT> &lc, const FieldT& c, const std::string &annotation_prefix) | |
26 | { | |
27 | pb.add_r1cs_constraint(r1cs_constraint<FieldT>(1, lc, c), | |
28 | FMT(annotation_prefix, " constness_constraint")); | |
29 | } | |
30 | ||
31 | template<typename FieldT> | |
32 | void packing_gadget<FieldT>::generate_r1cs_constraints(const bool enforce_bitness) | |
33 | /* adds constraint result = \sum bits[i] * 2^i */ | |
34 | { | |
35 | this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(1, pb_packing_sum<FieldT>(bits), packed), FMT(this->annotation_prefix, " packing_constraint")); | |
36 | ||
37 | if (enforce_bitness) | |
38 | { | |
39 | for (size_t i = 0; i < bits.size(); ++i) | |
40 | { | |
41 | generate_boolean_r1cs_constraint<FieldT>(this->pb, bits[i], FMT(this->annotation_prefix, " bitness_%zu", i)); | |
42 | } | |
43 | } | |
44 | } | |
45 | ||
46 | template<typename FieldT> | |
47 | void packing_gadget<FieldT>::generate_r1cs_witness_from_packed() | |
48 | { | |
49 | packed.evaluate(this->pb); | |
50 | assert(this->pb.lc_val(packed).as_bigint().num_bits() <= bits.size()); | |
51 | bits.fill_with_bits_of_field_element(this->pb, this->pb.lc_val(packed)); | |
52 | } | |
53 | ||
54 | template<typename FieldT> | |
55 | void packing_gadget<FieldT>::generate_r1cs_witness_from_bits() | |
56 | { | |
57 | bits.evaluate(this->pb); | |
58 | this->pb.lc_val(packed) = bits.get_field_element_from_bits(this->pb); | |
59 | } | |
60 | ||
61 | template<typename FieldT> | |
62 | multipacking_gadget<FieldT>::multipacking_gadget(protoboard<FieldT> &pb, | |
63 | const pb_linear_combination_array<FieldT> &bits, | |
64 | const pb_linear_combination_array<FieldT> &packed_vars, | |
65 | const size_t chunk_size, | |
66 | const std::string &annotation_prefix) : | |
67 | gadget<FieldT>(pb, annotation_prefix), bits(bits), packed_vars(packed_vars), | |
68 | chunk_size(chunk_size), | |
69 | num_chunks(div_ceil(bits.size(), chunk_size)) | |
70 | // last_chunk_size(bits.size() - (num_chunks-1) * chunk_size) | |
71 | { | |
72 | assert(packed_vars.size() == num_chunks); | |
73 | for (size_t i = 0; i < num_chunks; ++i) | |
74 | { | |
75 | packers.emplace_back(packing_gadget<FieldT>(this->pb, pb_linear_combination_array<FieldT>(bits.begin() + i * chunk_size, | |
76 | bits.begin() + std::min((i+1) * chunk_size, bits.size())), | |
77 | packed_vars[i], FMT(this->annotation_prefix, " packers_%zu", i))); | |
78 | } | |
79 | } | |
80 | ||
81 | template<typename FieldT> | |
82 | void multipacking_gadget<FieldT>::generate_r1cs_constraints(const bool enforce_bitness) | |
83 | { | |
84 | for (size_t i = 0; i < num_chunks; ++i) | |
85 | { | |
86 | packers[i].generate_r1cs_constraints(enforce_bitness); | |
87 | } | |
88 | } | |
89 | ||
90 | template<typename FieldT> | |
91 | void multipacking_gadget<FieldT>::generate_r1cs_witness_from_packed() | |
92 | { | |
93 | for (size_t i = 0; i < num_chunks; ++i) | |
94 | { | |
95 | packers[i].generate_r1cs_witness_from_packed(); | |
96 | } | |
97 | } | |
98 | ||
99 | template<typename FieldT> | |
100 | void multipacking_gadget<FieldT>::generate_r1cs_witness_from_bits() | |
101 | { | |
102 | for (size_t i = 0; i < num_chunks; ++i) | |
103 | { | |
104 | packers[i].generate_r1cs_witness_from_bits(); | |
105 | } | |
106 | } | |
107 | ||
108 | template<typename FieldT> | |
109 | size_t multipacking_num_chunks(const size_t num_bits) | |
110 | { | |
111 | return div_ceil(num_bits, FieldT::capacity()); | |
112 | } | |
113 | ||
114 | template<typename FieldT> | |
115 | field_vector_copy_gadget<FieldT>::field_vector_copy_gadget(protoboard<FieldT> &pb, | |
116 | const pb_variable_array<FieldT> &source, | |
117 | const pb_variable_array<FieldT> &target, | |
118 | const pb_linear_combination<FieldT> &do_copy, | |
119 | const std::string &annotation_prefix) : | |
120 | gadget<FieldT>(pb, annotation_prefix), source(source), target(target), do_copy(do_copy) | |
121 | { | |
122 | assert(source.size() == target.size()); | |
123 | } | |
124 | ||
125 | template<typename FieldT> | |
126 | void field_vector_copy_gadget<FieldT>::generate_r1cs_constraints() | |
127 | { | |
128 | for (size_t i = 0; i < source.size(); ++i) | |
129 | { | |
130 | this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(do_copy, source[i] - target[i], 0), | |
131 | FMT(this->annotation_prefix, " copying_check_%zu", i)); | |
132 | } | |
133 | } | |
134 | ||
135 | template<typename FieldT> | |
136 | void field_vector_copy_gadget<FieldT>::generate_r1cs_witness() | |
137 | { | |
138 | do_copy.evaluate(this->pb); | |
139 | assert(this->pb.lc_val(do_copy) == FieldT::one() || this->pb.lc_val(do_copy) == FieldT::zero()); | |
140 | if (this->pb.lc_val(do_copy) != FieldT::zero()) | |
141 | { | |
142 | for (size_t i = 0; i < source.size(); ++i) | |
143 | { | |
144 | this->pb.val(target[i]) = this->pb.val(source[i]); | |
145 | } | |
146 | } | |
147 | } | |
148 | ||
149 | template<typename FieldT> | |
150 | bit_vector_copy_gadget<FieldT>::bit_vector_copy_gadget(protoboard<FieldT> &pb, | |
151 | const pb_variable_array<FieldT> &source_bits, | |
152 | const pb_variable_array<FieldT> &target_bits, | |
153 | const pb_linear_combination<FieldT> &do_copy, | |
154 | const size_t chunk_size, | |
155 | const std::string &annotation_prefix) : | |
156 | gadget<FieldT>(pb, annotation_prefix), source_bits(source_bits), target_bits(target_bits), do_copy(do_copy), | |
157 | chunk_size(chunk_size), num_chunks(div_ceil(source_bits.size(), chunk_size)) | |
158 | { | |
159 | assert(source_bits.size() == target_bits.size()); | |
160 | ||
161 | packed_source.allocate(pb, num_chunks, FMT(annotation_prefix, " packed_source")); | |
162 | pack_source.reset(new multipacking_gadget<FieldT>(pb, source_bits, packed_source, chunk_size, FMT(annotation_prefix, " pack_source"))); | |
163 | ||
164 | packed_target.allocate(pb, num_chunks, FMT(annotation_prefix, " packed_target")); | |
165 | pack_target.reset(new multipacking_gadget<FieldT>(pb, target_bits, packed_target, chunk_size, FMT(annotation_prefix, " pack_target"))); | |
166 | ||
167 | copier.reset(new field_vector_copy_gadget<FieldT>(pb, packed_source, packed_target, do_copy, FMT(annotation_prefix, " copier"))); | |
168 | } | |
169 | ||
170 | template<typename FieldT> | |
171 | void bit_vector_copy_gadget<FieldT>::generate_r1cs_constraints(const bool enforce_source_bitness, const bool enforce_target_bitness) | |
172 | { | |
173 | pack_source->generate_r1cs_constraints(enforce_source_bitness); | |
174 | pack_target->generate_r1cs_constraints(enforce_target_bitness); | |
175 | ||
176 | copier->generate_r1cs_constraints(); | |
177 | } | |
178 | ||
179 | template<typename FieldT> | |
180 | void bit_vector_copy_gadget<FieldT>::generate_r1cs_witness() | |
181 | { | |
182 | do_copy.evaluate(this->pb); | |
183 | assert(this->pb.lc_val(do_copy) == FieldT::zero() || this->pb.lc_val(do_copy) == FieldT::one()); | |
184 | if (this->pb.lc_val(do_copy) == FieldT::one()) | |
185 | { | |
186 | for (size_t i = 0; i < source_bits.size(); ++i) | |
187 | { | |
188 | this->pb.val(target_bits[i]) = this->pb.val(source_bits[i]); | |
189 | } | |
190 | } | |
191 | ||
192 | pack_source->generate_r1cs_witness_from_bits(); | |
193 | pack_target->generate_r1cs_witness_from_bits(); | |
194 | } | |
195 | ||
196 | template<typename FieldT> | |
197 | void dual_variable_gadget<FieldT>::generate_r1cs_constraints(const bool enforce_bitness) | |
198 | { | |
199 | consistency_check->generate_r1cs_constraints(enforce_bitness); | |
200 | } | |
201 | ||
202 | template<typename FieldT> | |
203 | void dual_variable_gadget<FieldT>::generate_r1cs_witness_from_packed() | |
204 | { | |
205 | consistency_check->generate_r1cs_witness_from_packed(); | |
206 | } | |
207 | ||
208 | template<typename FieldT> | |
209 | void dual_variable_gadget<FieldT>::generate_r1cs_witness_from_bits() | |
210 | { | |
211 | consistency_check->generate_r1cs_witness_from_bits(); | |
212 | } | |
213 | ||
214 | template<typename FieldT> | |
215 | void disjunction_gadget<FieldT>::generate_r1cs_constraints() | |
216 | { | |
217 | /* inv * sum = output */ | |
218 | linear_combination<FieldT> a1, b1, c1; | |
219 | a1.add_term(inv); | |
220 | for (size_t i = 0; i < inputs.size(); ++i) | |
221 | { | |
222 | b1.add_term(inputs[i]); | |
223 | } | |
224 | c1.add_term(output); | |
225 | ||
226 | this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(a1, b1, c1), FMT(this->annotation_prefix, " inv*sum=output")); | |
227 | ||
228 | /* (1-output) * sum = 0 */ | |
229 | linear_combination<FieldT> a2, b2, c2; | |
230 | a2.add_term(ONE); | |
231 | a2.add_term(output, -1); | |
232 | for (size_t i = 0; i < inputs.size(); ++i) | |
233 | { | |
234 | b2.add_term(inputs[i]); | |
235 | } | |
236 | c2.add_term(ONE, 0); | |
237 | ||
238 | this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(a2, b2, c2), FMT(this->annotation_prefix, " (1-output)*sum=0")); | |
239 | } | |
240 | ||
241 | template<typename FieldT> | |
242 | void disjunction_gadget<FieldT>::generate_r1cs_witness() | |
243 | { | |
244 | FieldT sum = FieldT::zero(); | |
245 | ||
246 | for (size_t i = 0; i < inputs.size(); ++i) | |
247 | { | |
248 | sum += this->pb.val(inputs[i]); | |
249 | } | |
250 | ||
251 | if (sum.is_zero()) | |
252 | { | |
253 | this->pb.val(inv) = FieldT::zero(); | |
254 | this->pb.val(output) = FieldT::zero(); | |
255 | } | |
256 | else | |
257 | { | |
258 | this->pb.val(inv) = sum.inverse(); | |
259 | this->pb.val(output) = FieldT::one(); | |
260 | } | |
261 | } | |
262 | ||
263 | template<typename FieldT> | |
264 | void test_disjunction_gadget(const size_t n) | |
265 | { | |
266 | printf("testing disjunction_gadget on all %zu bit strings\n", n); | |
267 | ||
268 | protoboard<FieldT> pb; | |
269 | pb_variable_array<FieldT> inputs; | |
270 | inputs.allocate(pb, n, "inputs"); | |
271 | ||
272 | pb_variable<FieldT> output; | |
273 | output.allocate(pb, "output"); | |
274 | ||
275 | disjunction_gadget<FieldT> d(pb, inputs, output, "d"); | |
276 | d.generate_r1cs_constraints(); | |
277 | ||
5a83e4fc | 278 | for (size_t w = 0; w < UINT64_C(1)<<n; ++w) |
51e44864 JG |
279 | { |
280 | for (size_t j = 0; j < n; ++j) | |
281 | { | |
5a83e4fc | 282 | pb.val(inputs[j]) = FieldT((w & (UINT64_C(1)<<j)) ? 1 : 0); |
51e44864 JG |
283 | } |
284 | ||
285 | d.generate_r1cs_witness(); | |
286 | ||
287 | #ifdef DEBUG | |
288 | printf("positive test for %zu\n", w); | |
289 | #endif | |
290 | assert(pb.val(output) == (w ? FieldT::one() : FieldT::zero())); | |
291 | assert(pb.is_satisfied()); | |
292 | ||
293 | #ifdef DEBUG | |
294 | printf("negative test for %zu\n", w); | |
295 | #endif | |
296 | pb.val(output) = (w ? FieldT::zero() : FieldT::one()); | |
297 | assert(!pb.is_satisfied()); | |
298 | } | |
299 | ||
300 | print_time("disjunction tests successful"); | |
301 | } | |
302 | ||
303 | template<typename FieldT> | |
304 | void conjunction_gadget<FieldT>::generate_r1cs_constraints() | |
305 | { | |
306 | /* inv * (n-sum) = 1-output */ | |
307 | linear_combination<FieldT> a1, b1, c1; | |
308 | a1.add_term(inv); | |
309 | b1.add_term(ONE, inputs.size()); | |
310 | for (size_t i = 0; i < inputs.size(); ++i) | |
311 | { | |
312 | b1.add_term(inputs[i], -1); | |
313 | } | |
314 | c1.add_term(ONE); | |
315 | c1.add_term(output, -1); | |
316 | ||
317 | this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(a1, b1, c1), FMT(this->annotation_prefix, " inv*(n-sum)=(1-output)")); | |
318 | ||
319 | /* output * (n-sum) = 0 */ | |
320 | linear_combination<FieldT> a2, b2, c2; | |
321 | a2.add_term(output); | |
322 | b2.add_term(ONE, inputs.size()); | |
323 | for (size_t i = 0; i < inputs.size(); ++i) | |
324 | { | |
325 | b2.add_term(inputs[i], -1); | |
326 | } | |
327 | c2.add_term(ONE, 0); | |
328 | ||
329 | this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(a2, b2, c2), FMT(this->annotation_prefix, " output*(n-sum)=0")); | |
330 | } | |
331 | ||
332 | template<typename FieldT> | |
333 | void conjunction_gadget<FieldT>::generate_r1cs_witness() | |
334 | { | |
335 | FieldT sum = FieldT(inputs.size()); | |
336 | ||
337 | for (size_t i = 0; i < inputs.size(); ++i) | |
338 | { | |
339 | sum -= this->pb.val(inputs[i]); | |
340 | } | |
341 | ||
342 | if (sum.is_zero()) | |
343 | { | |
344 | this->pb.val(inv) = FieldT::zero(); | |
345 | this->pb.val(output) = FieldT::one(); | |
346 | } | |
347 | else | |
348 | { | |
349 | this->pb.val(inv) = sum.inverse(); | |
350 | this->pb.val(output) = FieldT::zero(); | |
351 | } | |
352 | } | |
353 | ||
354 | template<typename FieldT> | |
355 | void test_conjunction_gadget(const size_t n) | |
356 | { | |
357 | printf("testing conjunction_gadget on all %zu bit strings\n", n); | |
358 | ||
359 | protoboard<FieldT> pb; | |
360 | pb_variable_array<FieldT> inputs; | |
361 | inputs.allocate(pb, n, "inputs"); | |
362 | ||
363 | pb_variable<FieldT> output; | |
364 | output.allocate(pb, "output"); | |
365 | ||
366 | conjunction_gadget<FieldT> c(pb, inputs, output, "c"); | |
367 | c.generate_r1cs_constraints(); | |
368 | ||
5a83e4fc | 369 | for (size_t w = 0; w < UINT64_C(1)<<n; ++w) |
51e44864 JG |
370 | { |
371 | for (size_t j = 0; j < n; ++j) | |
372 | { | |
5a83e4fc | 373 | pb.val(inputs[j]) = (w & (UINT64_C(1)<<j)) ? FieldT::one() : FieldT::zero(); |
51e44864 JG |
374 | } |
375 | ||
376 | c.generate_r1cs_witness(); | |
377 | ||
378 | #ifdef DEBUG | |
379 | printf("positive test for %zu\n", w); | |
380 | #endif | |
5a83e4fc | 381 | assert(pb.val(output) == (w == (UINT64_C(1)<<n) - 1 ? FieldT::one() : FieldT::zero())); |
51e44864 JG |
382 | assert(pb.is_satisfied()); |
383 | ||
384 | #ifdef DEBUG | |
385 | printf("negative test for %zu\n", w); | |
386 | #endif | |
5a83e4fc | 387 | pb.val(output) = (w == (UINT64_C(1)<<n) - 1 ? FieldT::zero() : FieldT::one()); |
51e44864 JG |
388 | assert(!pb.is_satisfied()); |
389 | } | |
390 | ||
391 | print_time("conjunction tests successful"); | |
392 | } | |
393 | ||
394 | template<typename FieldT> | |
395 | void comparison_gadget<FieldT>::generate_r1cs_constraints() | |
396 | { | |
397 | /* | |
398 | packed(alpha) = 2^n + B - A | |
399 | ||
400 | not_all_zeros = \bigvee_{i=0}^{n-1} alpha_i | |
401 | ||
402 | if B - A > 0, then 2^n + B - A > 2^n, | |
403 | so alpha_n = 1 and not_all_zeros = 1 | |
404 | if B - A = 0, then 2^n + B - A = 2^n, | |
405 | so alpha_n = 1 and not_all_zeros = 0 | |
406 | if B - A < 0, then 2^n + B - A \in {0, 1, \ldots, 2^n-1}, | |
407 | so alpha_n = 0 | |
408 | ||
409 | therefore alpha_n = less_or_eq and alpha_n * not_all_zeros = less | |
410 | */ | |
411 | ||
412 | /* not_all_zeros to be Boolean, alpha_i are Boolean by packing gadget */ | |
413 | generate_boolean_r1cs_constraint<FieldT>(this->pb, not_all_zeros, | |
414 | FMT(this->annotation_prefix, " not_all_zeros")); | |
415 | ||
416 | /* constraints for packed(alpha) = 2^n + B - A */ | |
417 | pack_alpha->generate_r1cs_constraints(true); | |
418 | this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(1, (FieldT(2)^n) + B - A, alpha_packed), FMT(this->annotation_prefix, " main_constraint")); | |
419 | ||
420 | /* compute result */ | |
421 | all_zeros_test->generate_r1cs_constraints(); | |
422 | this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(less_or_eq, not_all_zeros, less), | |
423 | FMT(this->annotation_prefix, " less")); | |
424 | } | |
425 | ||
426 | template<typename FieldT> | |
427 | void comparison_gadget<FieldT>::generate_r1cs_witness() | |
428 | { | |
429 | A.evaluate(this->pb); | |
430 | B.evaluate(this->pb); | |
431 | ||
432 | /* unpack 2^n + B - A into alpha_packed */ | |
433 | this->pb.val(alpha_packed) = (FieldT(2)^n) + this->pb.lc_val(B) - this->pb.lc_val(A); | |
434 | pack_alpha->generate_r1cs_witness_from_packed(); | |
435 | ||
436 | /* compute result */ | |
437 | all_zeros_test->generate_r1cs_witness(); | |
438 | this->pb.val(less) = this->pb.val(less_or_eq) * this->pb.val(not_all_zeros); | |
439 | } | |
440 | ||
441 | template<typename FieldT> | |
442 | void test_comparison_gadget(const size_t n) | |
443 | { | |
444 | printf("testing comparison_gadget on all %zu bit inputs\n", n); | |
445 | ||
446 | protoboard<FieldT> pb; | |
447 | ||
448 | pb_variable<FieldT> A, B, less, less_or_eq; | |
449 | A.allocate(pb, "A"); | |
450 | B.allocate(pb, "B"); | |
451 | less.allocate(pb, "less"); | |
452 | less_or_eq.allocate(pb, "less_or_eq"); | |
453 | ||
454 | comparison_gadget<FieldT> cmp(pb, n, A, B, less, less_or_eq, "cmp"); | |
455 | cmp.generate_r1cs_constraints(); | |
456 | ||
5a83e4fc | 457 | for (size_t a = 0; a < UINT64_C(1)<<n; ++a) |
51e44864 | 458 | { |
5a83e4fc | 459 | for (size_t b = 0; b < UINT64_C(1)<<n; ++b) |
51e44864 JG |
460 | { |
461 | pb.val(A) = FieldT(a); | |
462 | pb.val(B) = FieldT(b); | |
463 | ||
464 | cmp.generate_r1cs_witness(); | |
465 | ||
466 | #ifdef DEBUG | |
467 | printf("positive test for %zu < %zu\n", a, b); | |
468 | #endif | |
469 | assert(pb.val(less) == (a < b ? FieldT::one() : FieldT::zero())); | |
470 | assert(pb.val(less_or_eq) == (a <= b ? FieldT::one() : FieldT::zero())); | |
471 | assert(pb.is_satisfied()); | |
472 | } | |
473 | } | |
474 | ||
475 | print_time("comparison tests successful"); | |
476 | } | |
477 | ||
478 | template<typename FieldT> | |
479 | void inner_product_gadget<FieldT>::generate_r1cs_constraints() | |
480 | { | |
481 | /* | |
482 | S_i = \sum_{k=0}^{i+1} A[i] * B[i] | |
483 | S[0] = A[0] * B[0] | |
484 | S[i+1] - S[i] = A[i] * B[i] | |
485 | */ | |
486 | for (size_t i = 0; i < A.size(); ++i) | |
487 | { | |
488 | this->pb.add_r1cs_constraint( | |
489 | r1cs_constraint<FieldT>(A[i], B[i], | |
490 | (i == A.size()-1 ? result : S[i]) + (i == 0 ? 0 * ONE : -S[i-1])), | |
491 | FMT(this->annotation_prefix, " S_%zu", i)); | |
492 | } | |
493 | } | |
494 | ||
495 | template<typename FieldT> | |
496 | void inner_product_gadget<FieldT>::generate_r1cs_witness() | |
497 | { | |
498 | FieldT total = FieldT::zero(); | |
499 | for (size_t i = 0; i < A.size(); ++i) | |
500 | { | |
501 | A[i].evaluate(this->pb); | |
502 | B[i].evaluate(this->pb); | |
503 | ||
504 | total += this->pb.lc_val(A[i]) * this->pb.lc_val(B[i]); | |
505 | this->pb.val(i == A.size()-1 ? result : S[i]) = total; | |
506 | } | |
507 | } | |
508 | ||
509 | template<typename FieldT> | |
510 | void test_inner_product_gadget(const size_t n) | |
511 | { | |
512 | printf("testing inner_product_gadget on all %zu bit strings\n", n); | |
513 | ||
514 | protoboard<FieldT> pb; | |
515 | pb_variable_array<FieldT> A; | |
516 | A.allocate(pb, n, "A"); | |
517 | pb_variable_array<FieldT> B; | |
518 | B.allocate(pb, n, "B"); | |
519 | ||
520 | pb_variable<FieldT> result; | |
521 | result.allocate(pb, "result"); | |
522 | ||
523 | inner_product_gadget<FieldT> g(pb, A, B, result, "g"); | |
524 | g.generate_r1cs_constraints(); | |
525 | ||
5a83e4fc | 526 | for (size_t i = 0; i < UINT64_C(1)<<n; ++i) |
51e44864 | 527 | { |
5a83e4fc | 528 | for (size_t j = 0; j < UINT64_C(1)<<n; ++j) |
51e44864 JG |
529 | { |
530 | size_t correct = 0; | |
531 | for (size_t k = 0; k < n; ++k) | |
532 | { | |
5a83e4fc D |
533 | pb.val(A[k]) = (i & (UINT64_C(1)<<k) ? FieldT::one() : FieldT::zero()); |
534 | pb.val(B[k]) = (j & (UINT64_C(1)<<k) ? FieldT::one() : FieldT::zero()); | |
535 | correct += ((i & (UINT64_C(1)<<k)) && (j & (UINT64_C(1)<<k)) ? 1 : 0); | |
51e44864 JG |
536 | } |
537 | ||
538 | g.generate_r1cs_witness(); | |
539 | #ifdef DEBUG | |
540 | printf("positive test for (%zu, %zu)\n", i, j); | |
541 | #endif | |
542 | assert(pb.val(result) == FieldT(correct)); | |
543 | assert(pb.is_satisfied()); | |
544 | ||
545 | #ifdef DEBUG | |
546 | printf("negative test for (%zu, %zu)\n", i, j); | |
547 | #endif | |
548 | pb.val(result) = FieldT(100*n+19); | |
549 | assert(!pb.is_satisfied()); | |
550 | } | |
551 | } | |
552 | ||
553 | print_time("inner_product_gadget tests successful"); | |
554 | } | |
555 | ||
556 | template<typename FieldT> | |
557 | void loose_multiplexing_gadget<FieldT>::generate_r1cs_constraints() | |
558 | { | |
559 | /* \alpha_i (index - i) = 0 */ | |
560 | for (size_t i = 0; i < arr.size(); ++i) | |
561 | { | |
562 | this->pb.add_r1cs_constraint( | |
563 | r1cs_constraint<FieldT>(alpha[i], index - i, 0), | |
564 | FMT(this->annotation_prefix, " alpha_%zu", i)); | |
565 | } | |
566 | ||
567 | /* 1 * (\sum \alpha_i) = success_flag */ | |
568 | linear_combination<FieldT> a, b, c; | |
569 | a.add_term(ONE); | |
570 | for (size_t i = 0; i < arr.size(); ++i) | |
571 | { | |
572 | b.add_term(alpha[i]); | |
573 | } | |
574 | c.add_term(success_flag); | |
575 | this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(a, b, c), FMT(this->annotation_prefix, " main_constraint")); | |
576 | ||
577 | /* now success_flag is constrained to either 0 (if index is out of | |
578 | range) or \alpha_i. constrain it and \alpha_i to zero */ | |
579 | generate_boolean_r1cs_constraint<FieldT>(this->pb, success_flag, FMT(this->annotation_prefix, " success_flag")); | |
580 | ||
581 | /* compute result */ | |
582 | compute_result->generate_r1cs_constraints(); | |
583 | } | |
584 | ||
585 | template<typename FieldT> | |
586 | void loose_multiplexing_gadget<FieldT>::generate_r1cs_witness() | |
587 | { | |
588 | /* assumes that idx can be fit in ulong; true for our purposes for now */ | |
589 | const bigint<FieldT::num_limbs> valint = this->pb.val(index).as_bigint(); | |
5a83e4fc | 590 | uint64_t idx = valint.as_ulong(); |
51e44864 JG |
591 | const bigint<FieldT::num_limbs> arrsize(arr.size()); |
592 | ||
593 | if (idx >= arr.size() || mpn_cmp(valint.data, arrsize.data, FieldT::num_limbs) >= 0) | |
594 | { | |
595 | for (size_t i = 0; i < arr.size(); ++i) | |
596 | { | |
597 | this->pb.val(alpha[i]) = FieldT::zero(); | |
598 | } | |
599 | ||
600 | this->pb.val(success_flag) = FieldT::zero(); | |
601 | } | |
602 | else | |
603 | { | |
604 | for (size_t i = 0; i < arr.size(); ++i) | |
605 | { | |
606 | this->pb.val(alpha[i]) = (i == idx ? FieldT::one() : FieldT::zero()); | |
607 | } | |
608 | ||
609 | this->pb.val(success_flag) = FieldT::one(); | |
610 | } | |
611 | ||
612 | compute_result->generate_r1cs_witness(); | |
613 | } | |
614 | ||
615 | template<typename FieldT> | |
616 | void test_loose_multiplexing_gadget(const size_t n) | |
617 | { | |
618 | printf("testing loose_multiplexing_gadget on 2**%zu pb_variable<FieldT> array inputs\n", n); | |
619 | protoboard<FieldT> pb; | |
620 | ||
621 | pb_variable_array<FieldT> arr; | |
5a83e4fc | 622 | arr.allocate(pb, UINT64_C(1)<<n, "arr"); |
51e44864 JG |
623 | pb_variable<FieldT> index, result, success_flag; |
624 | index.allocate(pb, "index"); | |
625 | result.allocate(pb, "result"); | |
626 | success_flag.allocate(pb, "success_flag"); | |
627 | ||
628 | loose_multiplexing_gadget<FieldT> g(pb, arr, index, result, success_flag, "g"); | |
629 | g.generate_r1cs_constraints(); | |
630 | ||
5a83e4fc | 631 | for (size_t i = 0; i < UINT64_C(1)<<n; ++i) |
51e44864 | 632 | { |
5a83e4fc | 633 | pb.val(arr[i]) = FieldT((19*i) % (UINT64_C(1)<<n)); |
51e44864 JG |
634 | } |
635 | ||
5a83e4fc | 636 | for (int idx = -1; idx <= (int)(UINT64_C(1)<<n); ++idx) |
51e44864 JG |
637 | { |
638 | pb.val(index) = FieldT(idx); | |
639 | g.generate_r1cs_witness(); | |
640 | ||
5a83e4fc | 641 | if (0 <= idx && idx <= (int)(UINT64_C(1)<<n) - 1) |
51e44864 JG |
642 | { |
643 | printf("demuxing element %d (in bounds)\n", idx); | |
5a83e4fc | 644 | assert(pb.val(result) == FieldT((19*idx) % (UINT64_C(1)<<n))); |
51e44864 JG |
645 | assert(pb.val(success_flag) == FieldT::one()); |
646 | assert(pb.is_satisfied()); | |
647 | pb.val(result) -= FieldT::one(); | |
648 | assert(!pb.is_satisfied()); | |
649 | } | |
650 | else | |
651 | { | |
652 | printf("demuxing element %d (out of bounds)\n", idx); | |
653 | assert(pb.val(success_flag) == FieldT::zero()); | |
654 | assert(pb.is_satisfied()); | |
655 | pb.val(success_flag) = FieldT::one(); | |
656 | assert(!pb.is_satisfied()); | |
657 | } | |
658 | } | |
659 | printf("loose_multiplexing_gadget tests successful\n"); | |
660 | } | |
661 | ||
662 | template<typename FieldT, typename VarT> | |
663 | void create_linear_combination_constraints(protoboard<FieldT> &pb, | |
664 | const std::vector<FieldT> &base, | |
665 | const std::vector<std::pair<VarT, FieldT> > &v, | |
666 | const VarT &target, | |
667 | const std::string &annotation_prefix) | |
668 | { | |
669 | for (size_t i = 0; i < base.size(); ++i) | |
670 | { | |
671 | linear_combination<FieldT> a, b, c; | |
672 | ||
673 | a.add_term(ONE); | |
674 | b.add_term(ONE, base[i]); | |
675 | ||
676 | for (auto &p : v) | |
677 | { | |
678 | b.add_term(p.first.all_vars[i], p.second); | |
679 | } | |
680 | ||
681 | c.add_term(target.all_vars[i]); | |
682 | ||
683 | pb.add_r1cs_constraint(r1cs_constraint<FieldT>(a, b, c), FMT(annotation_prefix, " linear_combination_%zu", i)); | |
684 | } | |
685 | } | |
686 | ||
687 | template<typename FieldT, typename VarT> | |
688 | void create_linear_combination_witness(protoboard<FieldT> &pb, | |
689 | const std::vector<FieldT> &base, | |
690 | const std::vector<std::pair<VarT, FieldT> > &v, | |
691 | const VarT &target) | |
692 | { | |
693 | for (size_t i = 0; i < base.size(); ++i) | |
694 | { | |
695 | pb.val(target.all_vars[i]) = base[i]; | |
696 | ||
697 | for (auto &p : v) | |
698 | { | |
699 | pb.val(target.all_vars[i]) += p.second * pb.val(p.first.all_vars[i]); | |
700 | } | |
701 | } | |
702 | } | |
703 | ||
704 | } // libsnark | |
705 | #endif // BASIC_GADGETS_TCC_ |