Clearmatics Libsnark  0.1
C++ library for zkSNARK proofs
consistency_enforcer_gadget.tcc
Go to the documentation of this file.
1 /** @file
2  *****************************************************************************
3 
4  Implementation of interfaces for the TinyRAM consistency enforcer gadget.
5 
6  See consistency_enforcer_gadget.hpp .
7 
8  *****************************************************************************
9  * @author This file is part of libsnark, developed by SCIPR Lab
10  * and contributors (see AUTHORS).
11  * @copyright MIT license (see LICENSE file)
12  *****************************************************************************/
13 
14 #ifndef CONSISTENCY_ENFORCER_GADGET_TCC_
15 #define CONSISTENCY_ENFORCER_GADGET_TCC_
16 
17 namespace libsnark
18 {
19 
20 template<typename FieldT>
21 consistency_enforcer_gadget<FieldT>::consistency_enforcer_gadget(
22  tinyram_protoboard<FieldT> &pb,
23  const pb_variable_array<FieldT> &opcode_indicators,
24  const pb_variable_array<FieldT> &instruction_results,
25  const pb_variable_array<FieldT> &instruction_flags,
26  const pb_variable_array<FieldT> &desidx,
27  const pb_variable<FieldT> &packed_incoming_pc,
28  const pb_variable_array<FieldT> &packed_incoming_registers,
29  const pb_variable<FieldT> &packed_incoming_desval,
30  const pb_variable<FieldT> &incoming_flag,
31  const pb_variable<FieldT> &packed_outgoing_pc,
32  const pb_variable_array<FieldT> &packed_outgoing_registers,
33  const pb_variable<FieldT> &outgoing_flag,
34  const std::string &annotation_prefix)
35  : tinyram_standard_gadget<FieldT>(pb, annotation_prefix)
36  , opcode_indicators(opcode_indicators)
37  , instruction_results(instruction_results)
38  , instruction_flags(instruction_flags)
39  , desidx(desidx)
40  , packed_incoming_pc(packed_incoming_pc)
41  , packed_incoming_registers(packed_incoming_registers)
42  , packed_incoming_desval(packed_incoming_desval)
43  , incoming_flag(incoming_flag)
44  , packed_outgoing_pc(packed_outgoing_pc)
45  , packed_outgoing_registers(packed_outgoing_registers)
46  , outgoing_flag(outgoing_flag)
47 {
48  assert(desidx.size() == pb.ap.reg_arg_width());
49 
50  packed_outgoing_desval.allocate(
51  pb, FMT(this->annotation_prefix, " packed_outgoing_desval"));
52  is_register_instruction.allocate(
53  pb, FMT(this->annotation_prefix, " is_register_instruction"));
54  is_control_flow_instruction.allocate(
55  pb, FMT(this->annotation_prefix, " is_control_flow_instruction"));
56  is_stall_instruction.allocate(
57  pb, FMT(this->annotation_prefix, " is_stall_instruction"));
58 
59  packed_desidx.allocate(pb, FMT(this->annotation_prefix, " packed_desidx"));
60  pack_desidx.reset(new packing_gadget<FieldT>(
61  pb,
62  desidx,
63  packed_desidx,
64  FMT(this->annotation_prefix, "pack_desidx")));
65 
66  computed_result.allocate(
67  pb, FMT(this->annotation_prefix, " computed_result"));
68  computed_flag.allocate(pb, FMT(this->annotation_prefix, " computed_flag"));
69 
70  compute_computed_result.reset(new inner_product_gadget<FieldT>(
71  pb,
72  opcode_indicators,
73  instruction_results,
74  computed_result,
75  FMT(this->annotation_prefix, " compute_computed_result")));
76  compute_computed_flag.reset(new inner_product_gadget<FieldT>(
77  pb,
78  opcode_indicators,
79  instruction_flags,
80  computed_flag,
81  FMT(this->annotation_prefix, " compute_computed_flag")));
82 
83  pc_from_cf_or_zero.allocate(
84  pb, FMT(this->annotation_prefix, " pc_from_cf_or_zero"));
85 
86  demux_packed_outgoing_desval.reset(new loose_multiplexing_gadget<FieldT>(
87  pb,
88  packed_outgoing_registers,
89  packed_desidx,
90  packed_outgoing_desval,
91  ONE,
92  FMT(this->annotation_prefix, " demux_packed_outgoing_desval")));
93 }
94 
95 template<typename FieldT>
96 void consistency_enforcer_gadget<FieldT>::generate_r1cs_constraints()
97 {
98  /* pack destination index */
99  pack_desidx->generate_r1cs_constraints(false);
100 
101  /* demux result register */
102  demux_packed_outgoing_desval->generate_r1cs_constraints();
103 
104  /* is_register_instruction */
105  linear_combination<FieldT> reg_a, reg_b, reg_c;
106  reg_a.add_term(ONE, 1);
107  for (size_t i = 0; i < ARRAY_SIZE(tinyram_opcodes_register); ++i) {
108  reg_b.add_term(opcode_indicators[tinyram_opcodes_register[i]], 1);
109  }
110  reg_c.add_term(is_register_instruction, 1);
111  this->pb.add_r1cs_constraint(
112  r1cs_constraint<FieldT>(reg_a, reg_b, reg_c),
113  FMT(this->annotation_prefix, " is_register_instruction"));
114 
115  /* is_control_flow_instruction */
116  linear_combination<FieldT> cf_a, cf_b, cf_c;
117  cf_a.add_term(ONE, 1);
118  for (size_t i = 0; i < ARRAY_SIZE(tinyram_opcodes_control_flow); ++i) {
119  cf_b.add_term(opcode_indicators[tinyram_opcodes_control_flow[i]], 1);
120  }
121  cf_c.add_term(is_control_flow_instruction, 1);
122  this->pb.add_r1cs_constraint(
123  r1cs_constraint<FieldT>(cf_a, cf_b, cf_c),
124  FMT(this->annotation_prefix, " is_control_flow_instruction"));
125 
126  /* is_stall_instruction */
127  linear_combination<FieldT> stall_a, stall_b, stall_c;
128  stall_a.add_term(ONE, 1);
129  for (size_t i = 0; i < ARRAY_SIZE(tinyram_opcodes_stall); ++i) {
130  stall_b.add_term(opcode_indicators[tinyram_opcodes_stall[i]], 1);
131  }
132  stall_c.add_term(is_stall_instruction, 1);
133  this->pb.add_r1cs_constraint(
134  r1cs_constraint<FieldT>(stall_a, stall_b, stall_c),
135  FMT(this->annotation_prefix, " is_stall_instruction"));
136 
137  /* compute actual result/actual flag */
138  compute_computed_result->generate_r1cs_constraints();
139  compute_computed_flag->generate_r1cs_constraints();
140 
141  /*
142  compute new PC address (in double words, not bytes!):
143 
144  PC' = computed_result * is_control_flow_instruction + PC *
145  is_stall_instruction + (PC+1) * (1-is_control_flow_instruction -
146  is_stall_instruction) PC' - pc_from_cf_or_zero -
147  (1-is_control_flow_instruction - is_stall_instruction) = PC * (1 -
148  is_control_flow_instruction)
149  */
150  this->pb.add_r1cs_constraint(
151  r1cs_constraint<FieldT>(
152  computed_result, is_control_flow_instruction, pc_from_cf_or_zero),
153  FMT(this->annotation_prefix, " pc_from_cf_or_zero"));
154 
155  this->pb.add_r1cs_constraint(
156  r1cs_constraint<FieldT>(
157  packed_incoming_pc,
158  1 - is_control_flow_instruction,
159  packed_outgoing_pc - pc_from_cf_or_zero -
160  (1 - is_control_flow_instruction - is_stall_instruction)),
161  FMT(this->annotation_prefix, " packed_outgoing_pc"));
162 
163  /*
164  enforce new flag:
165 
166  flag' = computed_flag * is_register_instruction + flag *
167  (1-is_register_instruction) flag' - flag = (computed_flag - flag) *
168  is_register_instruction
169  */
170  this->pb.add_r1cs_constraint(
171  r1cs_constraint<FieldT>(
172  {computed_flag, incoming_flag * (-1)},
173  {is_register_instruction},
174  {outgoing_flag, incoming_flag * (-1)}),
175  FMT(this->annotation_prefix, " outgoing_flag"));
176 
177  /*
178  force carryover of unchanged registers
179 
180  (1-indicator) * (new-old) = 0
181 
182  In order to save constraints we "borrow" indicator variables
183  from loose multiplexing gadget.
184  */
185  for (size_t i = 0; i < this->pb.ap.k; ++i) {
186  this->pb.add_r1cs_constraint(
187  r1cs_constraint<FieldT>(
188  {ONE, demux_packed_outgoing_desval->alpha[i] * (-1)},
189  {packed_outgoing_registers[i],
190  packed_incoming_registers[i] * (-1)},
191  {ONE * 0}),
192  FMT(this->annotation_prefix, " register_carryover_%zu", i));
193  }
194 
195  /*
196  enforce correct destination register value:
197 
198  next_desval = computed_result * is_register_instruction +
199  packed_incoming_desval * (1-is_register_instruction) next_desval -
200  packed_incoming_desval = (computed_result - packed_incoming_desval) *
201  is_register_instruction
202  */
203  this->pb.add_r1cs_constraint(
204  r1cs_constraint<FieldT>(
205  {computed_result, packed_incoming_desval * (-1)},
206  {is_register_instruction},
207  {packed_outgoing_desval, packed_incoming_desval * (-1)}),
208  FMT(this->annotation_prefix, " packed_outgoing_desval"));
209 }
210 
211 template<typename FieldT>
212 void consistency_enforcer_gadget<FieldT>::generate_r1cs_witness()
213 {
214  /* pack destination index */
215  pack_desidx->generate_r1cs_witness_from_bits();
216 
217  /* is_register_instruction */
218  this->pb.val(is_register_instruction) = FieldT::zero();
219 
220  for (size_t i = 0; i < ARRAY_SIZE(tinyram_opcodes_register); ++i) {
221  this->pb.val(is_register_instruction) +=
222  this->pb.val(opcode_indicators[tinyram_opcodes_register[i]]);
223  }
224 
225  /* is_control_flow_instruction */
226  this->pb.val(is_control_flow_instruction) = FieldT::zero();
227 
228  for (size_t i = 0; i < ARRAY_SIZE(tinyram_opcodes_control_flow); ++i) {
229  this->pb.val(is_control_flow_instruction) +=
230  this->pb.val(opcode_indicators[tinyram_opcodes_control_flow[i]]);
231  }
232 
233  /* is_stall_instruction */
234  this->pb.val(is_stall_instruction) = FieldT::zero();
235 
236  for (size_t i = 0; i < ARRAY_SIZE(tinyram_opcodes_stall); ++i) {
237  this->pb.val(is_stall_instruction) +=
238  this->pb.val(opcode_indicators[tinyram_opcodes_stall[i]]);
239  }
240 
241  /* compute actual result/actual flag */
242  compute_computed_result->generate_r1cs_witness();
243  compute_computed_flag->generate_r1cs_witness();
244 
245  /*
246  compute new PC address (in double words, not bytes!):
247 
248  PC' = computed_result * is_control_flow_instruction + PC *
249  is_stall_instruction + (PC+1) * (1-is_control_flow_instruction -
250  is_stall_instruction) PC' - pc_from_cf_or_zero -
251  (1-is_control_flow_instruction - is_stall_instruction) = PC * (1 -
252  is_control_flow_instruction)
253  */
254  this->pb.val(pc_from_cf_or_zero) =
255  this->pb.val(computed_result) *
256  this->pb.val(is_control_flow_instruction);
257  this->pb.val(packed_outgoing_pc) =
258  this->pb.val(pc_from_cf_or_zero) +
259  this->pb.val(packed_incoming_pc) * this->pb.val(is_stall_instruction) +
260  (this->pb.val(packed_incoming_pc) + FieldT::one()) *
261  (FieldT::one() - this->pb.val(is_control_flow_instruction) -
262  this->pb.val(is_stall_instruction));
263 
264  /*
265  enforce new flag:
266 
267  flag' = computed_flag * is_register_instruction + flag *
268  (1-is_register_instruction) flag' - flag = (computed_flag - flag) *
269  is_register_instruction
270  */
271  this->pb.val(outgoing_flag) =
272  this->pb.val(computed_flag) * this->pb.val(is_register_instruction) +
273  this->pb.val(incoming_flag) *
274  (FieldT::one() - this->pb.val(is_register_instruction));
275 
276  /*
277  update registers (changed and unchanged)
278 
279  next_desval = computed_result * is_register_instruction +
280  packed_incoming_desval * (1-is_register_instruction)
281  */
282  FieldT changed_register_contents =
283  this->pb.val(computed_result) * this->pb.val(is_register_instruction) +
284  this->pb.val(packed_incoming_desval) *
285  (FieldT::one() - this->pb.val(is_register_instruction));
286 
287  for (size_t i = 0; i < this->pb.ap.k; ++i) {
288  this->pb.val(packed_outgoing_registers[i]) =
289  (this->pb.val(packed_desidx).as_ulong() == i)
290  ? changed_register_contents
291  : this->pb.val(packed_incoming_registers[i]);
292  }
293 
294  /* demux result register (it is important to do witness generation
295  here after all registers have been set to the correct
296  values!) */
297  demux_packed_outgoing_desval->generate_r1cs_witness();
298 }
299 
300 #if 0
301 template<typename FieldT>
302 void test_arithmetic_consistency_enforcer_gadget()
303 {
304  libff::print_time("starting arithmetic_consistency_enforcer test");
305 
306  tinyram_architecture_params ap(16, 16);
307  tinyram_protoboard<FieldT> pb(ap);
308 
309  pb_variable_array<FieldT> opcode_indicators, instruction_results, instruction_flags;
310  opcode_indicators.allocate(pb, 1ul<<ap.opcode_width(), "opcode_indicators");
311  instruction_results.allocate(pb, 1ul<<ap.opcode_width(), "instruction_results");
312  instruction_flags.allocate(pb, 1ul<<ap.opcode_width(), "instruction_flags");
313 
314  dual_variable_gadget<FieldT> desidx(pb, ap.reg_arg_width(), "desidx");
315 
316  pb_variable<FieldT> incoming_pc;
317  incoming_pc.allocate(pb, "incoming_pc");
318 
319  pb_variable_array<FieldT> packed_incoming_registers;
320  packed_incoming_registers.allocate(pb, ap.k, "packed_incoming_registers");
321 
322  pb_variable<FieldT> incoming_load_flag;
323  incoming_load_flag.allocate(pb, "incoming_load_flag");
324 
325  pb_variable<FieldT> outgoing_pc, outgoing_flag;
326  outgoing_pc.allocate(pb, "outgoing_pc");
327  outgoing_flag.allocate(pb, "outgoing_flag");
328 
329  pb_variable_array<FieldT> packed_outgoing_registers;
330  packed_outgoing_registers.allocate(pb, ap.k, "packed_outgoing_registers");
331 
332  arithmetic_consistency_enforcer_gadget g(pb, opcode_indicators, instruction_results, instruction_flags,
333  desidx.bits, incoming_pc, packed_incoming_registers,
334  incoming_load_flag, outgoing_pc, packed_outgoing_registers, outgoing_flag, "g");
335  g.generate_r1cs_constraints();
336 
337  for (size_t i = 0; i < 1ul<<ap.opcode_width(); ++i)
338  {
339  this->pb.val(instruction_results[i]) = FieldT(std::rand());
340  this->pb.val(instruction_flags[i]) = FieldT(std::rand() % 2);
341  }
342 
343  this->pb.val(incoming_pc) = FieldT(12345);
344  this->pb.val(incoming_load_flag) = FieldT::zero();
345 
346  for (size_t i = 0; i < ap.k; ++i)
347  {
348  this->pb.val(packed_incoming_registers[i]) = FieldT(1000+i);
349  }
350 
351  for (size_t t = 0; t < 1ul<<ap.opcode_width(); ++t)
352  {
353  this->pb.val(opcode_indicators[t]) = FieldT::zero();
354  }
355 
356  this->pb.val(opcode_indicators[tinyram_opcode_AND]) = FieldT::one();
357 
358  for (size_t i = 0; i < ap.k; ++i)
359  {
360  this->pb.val(desidx.packed) = FieldT(i);
361  desidx.generate_r1cs_witness_from_packed();
362 
363  g.generate_r1cs_witness();
364 
365  assert(this->pb.val(outgoing_pc) == FieldT(12346));
366 
367  for (size_t j = 0; j < ap.k; ++j)
368  {
369  assert(this->pb.val(packed_outgoing_registers[j]) ==
370  this->pb.val(i == j ?
371  instruction_results[tinyram_opcode_AND] :
372  packed_incoming_registers[j]));
373  }
374 
375  assert(this->pb.val(outgoing_flag) == this->pb.val(instruction_flags[tinyram_opcode_AND]));
376  assert(pb.is_satisfied());
377  }
378 
379  printf("arithmetic test successful\n");
380  for (size_t t = 0; t < 1ul<<ap.opcode_width(); ++t)
381  {
382  this->pb.val(opcode_indicators[t]) = FieldT::zero();
383  }
384  this->pb.val(opcode_indicators[tinyram_opcode_LOAD]) = FieldT::one();
385  this->pb.val(incoming_load_flag) = FieldT::one();
386 
387  g.generate_r1cs_witness();
388 
389  this->pb.val(outgoing_pc) == FieldT(12345);
390  assert(pb.is_satisfied());
391 
392  this->pb.val(incoming_load_flag) = FieldT::zero();
393  printf("test that firstload doesn't increment PC successful\n");
394 
395  for (size_t t = 0; t < 1ul<<ap.opcode_width(); ++t)
396  {
397  this->pb.val(opcode_indicators[t]) = FieldT::zero();
398  }
399 
400  this->pb.val(opcode_indicators[tinyram_opcode_JMP]) = FieldT::one();
401 
402  for (size_t i = 0; i < ap.k; ++i)
403  {
404  this->pb.val(desidx.packed) = FieldT(i);
405  desidx.generate_r1cs_witness_from_packed();
406 
407  g.generate_r1cs_witness();
408 
409  for (size_t j = 0; j < ap.k; ++j)
410  {
411  assert(this->pb.val(packed_outgoing_registers[j]) == this->pb.val(packed_incoming_registers[j]));
412  }
413 
414  assert(pb.is_satisfied());
415  }
416 
417  printf("non-arithmetic test successful\n");
418 
419  libff::print_time("arithmetic_consistency_enforcer tests successful");
420 }
421 
422 template<typename FieldT>
423 void test_control_flow_consistency_enforcer_gadget()
424 {
425  libff::print_time("starting control_flow_consistency_enforcer test");
426 
427  tinyram_architecture_params ap(16, 16);
428  tinyram_protoboard<FieldT> pb(ap);
429 
430  pb_variable_array<FieldT> opcode_indicators, instruction_results;
431  opcode_indicators.allocate(pb, 1ul<<ap.opcode_width(), "opcode_indicators");
432  instruction_results.allocate(pb, 1ul<<ap.opcode_width(), "instruction_results");
433 
434  pb_variable<FieldT> incoming_pc, incoming_flag;
435  incoming_pc.allocate(pb, "incoming_pc");
436  incoming_flag.allocate(pb, "incoming_flag");
437 
438  pb_variable_array<FieldT> packed_incoming_registers;
439  packed_incoming_registers.allocate(pb, ap.k, "packed_incoming_registers");
440 
441  pb_variable<FieldT> outgoing_pc, outgoing_flag;
442  outgoing_pc.allocate(pb, "outgoing_pc");
443  outgoing_flag.allocate(pb, "outgoing_flag");
444 
445  pb_variable_array<FieldT> packed_outgoing_registers;
446  packed_outgoing_registers.allocate(pb, ap.k, "packed_outgoing_registers");
447 
448  control_flow_consistency_enforcer_gadget g(pb, opcode_indicators, instruction_results,
449  incoming_pc, packed_incoming_registers, incoming_flag,
450  outgoing_pc, packed_outgoing_registers, outgoing_flag, "g");
451  g.generate_r1cs_constraints();
452 
453  for (size_t i = 0; i < 1ul<<ap.opcode_width(); ++i)
454  {
455  this->pb.val(instruction_results[i]) = FieldT(std::rand());
456  }
457 
458  this->pb.val(incoming_pc) = FieldT(12345);
459 
460  for (size_t i = 0; i < ap.k; ++i)
461  {
462  this->pb.val(packed_incoming_registers[i]) = FieldT(1000+i);
463  }
464 
465  for (size_t t = 0; t < 1ul<<ap.opcode_width(); ++t)
466  {
467  this->pb.val(opcode_indicators[t]) = FieldT::zero();
468  }
469  this->pb.val(opcode_indicators[tinyram_opcode_JMP]) = FieldT::one();
470 
471  for (int flag = 0; flag <= 1; ++flag)
472  {
473  this->pb.val(incoming_flag) = FieldT(flag);
474 
475  g.generate_r1cs_witness();
476 
477  assert(this->pb.val(outgoing_pc) == this->pb.val(instruction_results[tinyram_opcode_JMP]));
478  assert(this->pb.val(outgoing_flag) == this->pb.val(incoming_flag));
479 
480  for (size_t j = 0; j < ap.k; ++j)
481  {
482  assert(this->pb.val(packed_outgoing_registers[j]) == this->pb.val(packed_incoming_registers[j]));
483  }
484  assert(pb.is_satisfied());
485  }
486 
487  libff::print_time("control_flow_consistency_enforcer tests successful");
488 }
489 
490 template<typename FieldT>
491 void test_special_consistency_enforcer_gadget()
492 {
493  libff::print_time("starting special_consistency_enforcer_gadget test");
494 
495  tinyram_architecture_params ap(16, 16);
496  tinyram_protoboard<FieldT> pb(ap);
497 
498  pb_variable_array<FieldT> opcode_indicators;
499  opcode_indicators.allocate(pb, 1ul<<ap.opcode_width(), "opcode_indicators");
500 
501  pb_variable<FieldT> incoming_pc, incoming_flag, incoming_load_flag;
502  incoming_pc.allocate(pb, "incoming_pc");
503  incoming_flag.allocate(pb, "incoming_flag");
504  incoming_load_flag.allocate(pb, "incoming_load_flag");
505 
506  pb_variable_array<FieldT> packed_incoming_registers;
507  packed_incoming_registers.allocate(pb, ap.k, "packed_incoming_registers");
508 
509  pb_variable<FieldT> outgoing_pc, outgoing_flag, outgoing_load_flag;
510  outgoing_pc.allocate(pb, "outgoing_pc");
511  outgoing_flag.allocate(pb, "outgoing_flag");
512  outgoing_load_flag.allocate(pb, "outgoing_load_flag");
513 
514  pb_variable_array<FieldT> packed_outgoing_registers;
515  packed_outgoing_registers.allocate(pb, ap.k, "packed_outgoing_registers");
516 
517  special_consistency_enforcer_gadget g(pb, opcode_indicators,
518  incoming_pc, packed_incoming_registers, incoming_flag, incoming_load_flag,
519  outgoing_pc, packed_outgoing_registers, outgoing_flag, outgoing_load_flag, "g");
520  g.generate_r1cs_constraints();
521 
522  this->pb.val(incoming_pc) = FieldT(12345);
523  for (size_t i = 0; i < ap.k; ++i)
524  {
525  this->pb.val(packed_incoming_registers[i]) = FieldT(1000+i);
526  }
527  this->pb.val(incoming_flag) = FieldT::zero();
528  this->pb.val(incoming_load_flag) = FieldT::zero();
529 
530  /* test that accept stalls */
531  printf("test that ACCEPT stalls\n");
532 
533  for (size_t t = 0; t < 1ul<<ap.opcode_width(); ++t)
534  {
535  this->pb.val(opcode_indicators[t]) = FieldT::zero();
536  }
537  this->pb.val(opcode_indicators[tinyram_opcode_ACCEPT]) = FieldT::one();
538 
539  g.generate_r1cs_witness();
540 
541  assert(this->pb.val(outgoing_flag) == this->pb.val(incoming_flag));
542  for (size_t j = 0; j < ap.k; ++j)
543  {
544  assert(this->pb.val(packed_outgoing_registers[j]) == this->pb.val(packed_incoming_registers[j]));
545  }
546 
547  assert(this->pb.val(outgoing_pc) == this->pb.val(incoming_pc));
548  assert(pb.is_satisfied());
549 
550  printf("test that ACCEPT preserves registers\n");
551  this->pb.val(packed_outgoing_registers[0]) = FieldT::zero();
552  assert(!pb.is_satisfied());
553 
554  /* test that other special instructions (e.g. STORE) don't and also preserve registers */
555  printf("test that others (e.g. STORE) don't stall\n");
556 
557  for (size_t t = 0; t < 1ul<<ap.opcode_width(); ++t)
558  {
559  this->pb.val(opcode_indicators[t]) = FieldT::zero();
560  }
561  this->pb.val(opcode_indicators[tinyram_opcode_STORE]) = FieldT::one();
562 
563  g.generate_r1cs_witness();
564 
565  assert(this->pb.val(outgoing_flag) == this->pb.val(incoming_flag));
566  for (size_t j = 0; j < ap.k; ++j)
567  {
568  assert(this->pb.val(packed_outgoing_registers[j]) == this->pb.val(packed_incoming_registers[j]));
569  }
570 
571  assert(this->pb.val(outgoing_pc) == this->pb.val(incoming_pc) + FieldT::one());
572  assert(pb.is_satisfied());
573 
574  printf("test that STORE preserves registers\n");
575  this->pb.val(packed_outgoing_registers[0]) = FieldT::zero();
576  assert(!pb.is_satisfied());
577 
578  printf("test that STORE can't have load_flag\n");
579  g.generate_r1cs_witness();
580  this->pb.val(incoming_load_flag) = FieldT::one();
581 
582  assert(!pb.is_satisfied());
583 
584  /* test that load can modify outgoing register and sets load_flag */
585  printf("test that LOAD sets load_flag\n");
586 
587  for (size_t t = 0; t < 1ul<<ap.opcode_width(); ++t)
588  {
589  this->pb.val(opcode_indicators[t]) = FieldT::zero();
590  }
591  this->pb.val(opcode_indicators[tinyram_opcode_LOAD]) = FieldT::one();
592  this->pb.val(incoming_load_flag) = FieldT::zero();
593 
594  g.generate_r1cs_witness();
595 
596  assert(this->pb.val(outgoing_load_flag) == FieldT::one());
597  assert(pb.is_satisfied());
598 
599  printf("test that LOAD can modify registers\n");
600  this->pb.val(packed_outgoing_registers[0]) = FieldT::zero();
601  assert(pb.is_satisfied());
602 
603  /* test that postload clears load_flag */
604  printf("test that postload clears load_flag\n");
605 
606  for (size_t t = 0; t < 1ul<<ap.opcode_width(); ++t)
607  {
608  this->pb.val(opcode_indicators[t]) = FieldT::zero();
609  }
610  this->pb.val(opcode_indicators[tinyram_opcode_LOAD]) = FieldT::one();
611  this->pb.val(incoming_load_flag) = FieldT::one();
612 
613  g.generate_r1cs_witness();
614 
615  assert(this->pb.val(outgoing_load_flag) == FieldT::zero());
616  assert(pb.is_satisfied());
617 
618  /* test non-special instructions */
619  printf("test non-special instructions\n");
620 
621  for (size_t t = 0; t < 1ul<<ap.opcode_width(); ++t)
622  {
623  this->pb.val(opcode_indicators[t]) = FieldT::zero();
624  }
625  this->pb.val(opcode_indicators[tinyram_opcode_JMP]) = FieldT::one();
626  this->pb.val(incoming_load_flag) = FieldT::zero();
627  g.generate_r1cs_witness();
628 
629  assert(pb.is_satisfied());
630 
631  printf("test that non-special can't have load_flag\n");
632  g.generate_r1cs_witness();
633  this->pb.val(incoming_load_flag) = FieldT::one();
634 
635  assert(!pb.is_satisfied());
636 
637  libff::print_time("special_consistency_enforcer_gadget tests successful");
638 }
639 #endif
640 
641 } // namespace libsnark
642 
643 #endif // CONSISTENCY_ENFORCER_GADGET_TCC_
Generated on Wed Jan 25 2023 11:05:57 for Clearmatics Libsnark by   doxygen 1.8.17