src/snark patches for windows build
[VerusCoin.git] / src / snark / libsnark / gadgetlib1 / gadgets / basic_gadgets.tcc
CommitLineData
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
14namespace libsnark {
15
16template<typename FieldT>
17void 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
24template<typename FieldT>
25void 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
31template<typename FieldT>
32void 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
46template<typename FieldT>
47void 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
54template<typename FieldT>
55void 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
61template<typename FieldT>
62multipacking_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
81template<typename FieldT>
82void 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
90template<typename FieldT>
91void 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
99template<typename FieldT>
100void 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
108template<typename FieldT>
109size_t multipacking_num_chunks(const size_t num_bits)
110{
111 return div_ceil(num_bits, FieldT::capacity());
112}
113
114template<typename FieldT>
115field_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) :
120gadget<FieldT>(pb, annotation_prefix), source(source), target(target), do_copy(do_copy)
121{
122 assert(source.size() == target.size());
123}
124
125template<typename FieldT>
126void 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
135template<typename FieldT>
136void 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
149template<typename FieldT>
150bit_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
170template<typename FieldT>
171void 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
179template<typename FieldT>
180void 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
196template<typename FieldT>
197void dual_variable_gadget<FieldT>::generate_r1cs_constraints(const bool enforce_bitness)
198{
199 consistency_check->generate_r1cs_constraints(enforce_bitness);
200}
201
202template<typename FieldT>
203void dual_variable_gadget<FieldT>::generate_r1cs_witness_from_packed()
204{
205 consistency_check->generate_r1cs_witness_from_packed();
206}
207
208template<typename FieldT>
209void dual_variable_gadget<FieldT>::generate_r1cs_witness_from_bits()
210{
211 consistency_check->generate_r1cs_witness_from_bits();
212}
213
214template<typename FieldT>
215void 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
241template<typename FieldT>
242void 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
263template<typename FieldT>
264void 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
303template<typename FieldT>
304void 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
332template<typename FieldT>
333void 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
354template<typename FieldT>
355void 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
394template<typename FieldT>
395void 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
426template<typename FieldT>
427void 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
441template<typename FieldT>
442void 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
478template<typename FieldT>
479void 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
495template<typename FieldT>
496void 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
509template<typename FieldT>
510void 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
556template<typename FieldT>
557void 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
585template<typename FieldT>
586void 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
615template<typename FieldT>
616void 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
662template<typename FieldT, typename VarT>
663void 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
687template<typename FieldT, typename VarT>
688void 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_
This page took 0.141769 seconds and 4 git commands to generate.