Clearmatics Libsnark  0.1
C++ library for zkSNARK proofs
tinyram_cpu_checker.tcc
Go to the documentation of this file.
1 /** @file
2  *****************************************************************************
3 
4  Implementation of interfaces for the TinyRAM CPU checker gadget.
5 
6  See tinyram_cpu_checker.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 TINYRAM_CPU_CHECKER_TCC_
15 #define TINYRAM_CPU_CHECKER_TCC_
16 
17 #include <libff/algebra/fields/field_utils.hpp>
18 
19 namespace libsnark
20 {
21 
22 template<typename FieldT>
23 tinyram_cpu_checker<FieldT>::tinyram_cpu_checker(
24  tinyram_protoboard<FieldT> &pb,
25  pb_variable_array<FieldT> &prev_pc_addr,
26  pb_variable_array<FieldT> &prev_pc_val,
27  pb_variable_array<FieldT> &prev_state,
28  pb_variable_array<FieldT> &ls_addr,
29  pb_variable_array<FieldT> &ls_prev_val,
30  pb_variable_array<FieldT> &ls_next_val,
31  pb_variable_array<FieldT> &next_state,
32  pb_variable_array<FieldT> &next_pc_addr,
33  pb_variable<FieldT> &next_has_accepted,
34  const std::string &annotation_prefix)
35  : tinyram_standard_gadget<FieldT>(pb, annotation_prefix)
36  , prev_pc_addr(prev_pc_addr)
37  , prev_pc_val(prev_pc_val)
38  , prev_state(prev_state)
39  , ls_addr(ls_addr)
40  , ls_prev_val(ls_prev_val)
41  , ls_next_val(ls_next_val)
42  , next_state(next_state)
43  , next_pc_addr(next_pc_addr)
44  , next_has_accepted(next_has_accepted)
45 {
46  /* parse previous PC value as an instruction (note that we start
47  parsing from LSB of the instruction doubleword and go to the
48  MSB) */
49  auto pc_val_it = prev_pc_val.begin();
50 
51  arg2idx = pb_variable_array<FieldT>(
52  pc_val_it, pc_val_it + pb.ap.reg_arg_or_imm_width());
53  std::advance(pc_val_it, pb.ap.reg_arg_or_imm_width());
54  std::advance(pc_val_it, pb.ap.instruction_padding_width());
55  arg1idx =
56  pb_variable_array<FieldT>(pc_val_it, pc_val_it + pb.ap.reg_arg_width());
57  std::advance(pc_val_it, pb.ap.reg_arg_width());
58  desidx =
59  pb_variable_array<FieldT>(pc_val_it, pc_val_it + pb.ap.reg_arg_width());
60  std::advance(pc_val_it, pb.ap.reg_arg_width());
61  arg2_is_imm = *pc_val_it;
62  std::advance(pc_val_it, 1);
63  opcode =
64  pb_variable_array<FieldT>(pc_val_it, pc_val_it + pb.ap.opcode_width());
65  std::advance(pc_val_it, pb.ap.opcode_width());
66 
67  assert(pc_val_it == prev_pc_val.end());
68 
69  /* parse state as registers + flags */
70  pb_variable_array<FieldT> packed_prev_registers, packed_next_registers;
71  for (size_t i = 0; i < pb.ap.k; ++i) {
72  prev_registers.emplace_back(word_variable_gadget<FieldT>(
73  pb,
74  pb_variable_array<FieldT>(
75  prev_state.begin() + i * pb.ap.w,
76  prev_state.begin() + (i + 1) * pb.ap.w),
77  FMT(annotation_prefix, " prev_registers_%zu", i)));
78  next_registers.emplace_back(word_variable_gadget<FieldT>(
79  pb,
80  pb_variable_array<FieldT>(
81  next_state.begin() + i * pb.ap.w,
82  next_state.begin() + (i + 1) * pb.ap.w),
83  FMT(annotation_prefix, " next_registers_%zu", i)));
84 
85  packed_prev_registers.emplace_back(prev_registers[i].packed);
86  packed_next_registers.emplace_back(next_registers[i].packed);
87  }
88  prev_flag = *(++prev_state.rbegin());
89  next_flag = *(++next_state.rbegin());
90  prev_tape1_exhausted = *(prev_state.rbegin());
91  next_tape1_exhausted = *(next_state.rbegin());
92 
93  /* decode arguments */
94  prev_pc_addr_as_word_variable.reset(new word_variable_gadget<FieldT>(
95  pb,
96  prev_pc_addr,
97  FMT(annotation_prefix, " prev_pc_addr_as_word_variable")));
98  desval.reset(new word_variable_gadget<FieldT>(
99  pb, FMT(annotation_prefix, " desval")));
100  arg1val.reset(new word_variable_gadget<FieldT>(
101  pb, FMT(annotation_prefix, " arg1val")));
102  arg2val.reset(new word_variable_gadget<FieldT>(
103  pb, FMT(annotation_prefix, " arg2val")));
104 
105  decode_arguments.reset(new argument_decoder_gadget<FieldT>(
106  pb,
107  arg2_is_imm,
108  desidx,
109  arg1idx,
110  arg2idx,
111  packed_prev_registers,
112  desval->packed,
113  arg1val->packed,
114  arg2val->packed,
115  FMT(annotation_prefix, " decode_arguments")));
116 
117  /* create indicator variables for opcodes */
118  opcode_indicators.allocate(
119  pb,
120  1ul << pb.ap.opcode_width(),
121  FMT(annotation_prefix, " opcode_indicators"));
122 
123  /* perform the ALU operations */
124  instruction_results.allocate(
125  pb,
126  1ul << pb.ap.opcode_width(),
127  FMT(annotation_prefix, " instruction_results"));
128  instruction_flags.allocate(
129  pb,
130  1ul << pb.ap.opcode_width(),
131  FMT(annotation_prefix, " instruction_flags"));
132 
133  ALU.reset(new ALU_gadget<FieldT>(
134  pb,
135  opcode_indicators,
136  *prev_pc_addr_as_word_variable,
137  *desval,
138  *arg1val,
139  *arg2val,
140  prev_flag,
141  instruction_results,
142  instruction_flags,
143  FMT(annotation_prefix, " ALU")));
144 
145  /* check correctness of memory operations */
146  ls_prev_val_as_doubleword_variable.reset(
147  new doubleword_variable_gadget<FieldT>(
148  pb,
149  ls_prev_val,
150  FMT(annotation_prefix, " ls_prev_val_as_doubleword_variable")));
151  ls_next_val_as_doubleword_variable.reset(
152  new doubleword_variable_gadget<FieldT>(
153  pb,
154  ls_next_val,
155  FMT(annotation_prefix, " ls_next_val_as_doubleword_variable")));
156  memory_subaddress.reset(new dual_variable_gadget<FieldT>(
157  pb,
158  pb_variable_array<FieldT>(
159  arg2val->bits.begin(), arg2val->bits.begin() + pb.ap.subaddr_len()),
160  FMT(annotation_prefix, " memory_subaddress")));
161 
162  memory_subcontents.allocate(
163  pb, FMT(annotation_prefix, " memory_subcontents"));
164  memory_access_is_word.assign(
165  pb,
166  1 - (opcode_indicators[tinyram_opcode_LOADB] +
167  opcode_indicators[tinyram_opcode_STOREB]));
168  memory_access_is_byte.assign(
169  pb,
170  opcode_indicators[tinyram_opcode_LOADB] +
171  opcode_indicators[tinyram_opcode_STOREB]);
172 
173  check_memory.reset(new memory_masking_gadget<FieldT>(
174  pb,
175  *ls_prev_val_as_doubleword_variable,
176  *memory_subaddress,
177  memory_subcontents,
178  memory_access_is_word,
179  memory_access_is_byte,
180  *ls_next_val_as_doubleword_variable,
181  FMT(annotation_prefix, " check_memory")));
182 
183  /* handle reads */
184  read_not1.allocate(pb, FMT(annotation_prefix, " read_not1"));
185 
186  /* check consistency of the states according to the ALU results */
187  next_pc_addr_as_word_variable.reset(new word_variable_gadget<FieldT>(
188  pb,
189  next_pc_addr,
190  FMT(annotation_prefix, " next_pc_addr_as_word_variable")));
191 
192  consistency_enforcer.reset(new consistency_enforcer_gadget<FieldT>(
193  pb,
194  opcode_indicators,
195  instruction_results,
196  instruction_flags,
197  desidx,
198  prev_pc_addr_as_word_variable->packed,
199  packed_prev_registers,
200  desval->packed,
201  prev_flag,
202  next_pc_addr_as_word_variable->packed,
203  packed_next_registers,
204  next_flag,
205  FMT(annotation_prefix, " consistency_enforcer")));
206 }
207 
208 template<typename FieldT>
209 void tinyram_cpu_checker<FieldT>::generate_r1cs_constraints()
210 {
211  decode_arguments->generate_r1cs_constraints();
212 
213  /* generate indicator variables for opcode */
214  for (size_t i = 0; i < 1ul << this->pb.ap.opcode_width(); ++i) {
215  this->pb.add_r1cs_constraint(
216  r1cs_constraint<FieldT>(
217  opcode_indicators[i], pb_packing_sum<FieldT>(opcode) - i, 0),
218  FMT(this->annotation_prefix, " opcode_indicators_%zu", i));
219  }
220  this->pb.add_r1cs_constraint(
221  r1cs_constraint<FieldT>(1, pb_sum<FieldT>(opcode_indicators), 1),
222  FMT(this->annotation_prefix, " opcode_indicators_sum_to_1"));
223 
224  /* consistency checks for repacked variables */
225  for (size_t i = 0; i < this->pb.ap.k; ++i) {
226  prev_registers[i].generate_r1cs_constraints(true);
227  next_registers[i].generate_r1cs_constraints(true);
228  }
229  prev_pc_addr_as_word_variable->generate_r1cs_constraints(true);
230  next_pc_addr_as_word_variable->generate_r1cs_constraints(true);
231  ls_prev_val_as_doubleword_variable->generate_r1cs_constraints(true);
232  ls_next_val_as_doubleword_variable->generate_r1cs_constraints(true);
233 
234  /* main consistency checks */
235  decode_arguments->generate_r1cs_constraints();
236  ALU->generate_r1cs_constraints();
237  consistency_enforcer->generate_r1cs_constraints();
238 
239  /* check correct access to memory */
240  ls_prev_val_as_doubleword_variable->generate_r1cs_constraints(false);
241  ls_next_val_as_doubleword_variable->generate_r1cs_constraints(false);
242  memory_subaddress->generate_r1cs_constraints(false);
243  check_memory->generate_r1cs_constraints();
244 
245  this->pb.add_r1cs_constraint(
246  r1cs_constraint<FieldT>(
247  1,
248  pb_packing_sum<FieldT>(pb_variable_array<FieldT>(
249  arg2val->bits.begin() + this->pb.ap.subaddr_len(),
250  arg2val->bits.end())),
251  pb_packing_sum<FieldT>(ls_addr)),
252  FMT(this->annotation_prefix, " ls_addr_is_arg2val_minus_subaddress"));
253 
254  /* We require that if opcode is one of load.{b,w}, then
255  subcontents is appropriately stored in instruction_results. If
256  opcode is store.b we only take the necessary portion of arg1val
257  (i.e. last byte), and take entire arg1val for store.w.
258 
259  Note that ls_addr is *always* going to be arg2val. If the
260  instruction is a non-memory instruction, we will treat it as a
261  load from that memory location. */
262  this->pb.add_r1cs_constraint(
263  r1cs_constraint<FieldT>(
264  opcode_indicators[tinyram_opcode_LOADB],
265  memory_subcontents - instruction_results[tinyram_opcode_LOADB],
266  0),
267  FMT(this->annotation_prefix, " handle_loadb"));
268  this->pb.add_r1cs_constraint(
269  r1cs_constraint<FieldT>(
270  opcode_indicators[tinyram_opcode_LOADW],
271  memory_subcontents - instruction_results[tinyram_opcode_LOADW],
272  0),
273  FMT(this->annotation_prefix, " handle_loadw"));
274  this->pb.add_r1cs_constraint(
275  r1cs_constraint<FieldT>(
276  opcode_indicators[tinyram_opcode_STOREB],
277  memory_subcontents -
278  pb_packing_sum<FieldT>(pb_variable_array<FieldT>(
279  desval->bits.begin(), desval->bits.begin() + 8)),
280  0),
281  FMT(this->annotation_prefix, " handle_storeb"));
282  this->pb.add_r1cs_constraint(
283  r1cs_constraint<FieldT>(
284  opcode_indicators[tinyram_opcode_STOREW],
285  memory_subcontents - desval->packed,
286  0),
287  FMT(this->annotation_prefix, " handle_storew"));
288  this->pb.add_r1cs_constraint(
289  r1cs_constraint<FieldT>(
290  1 - (opcode_indicators[tinyram_opcode_STOREB] +
291  opcode_indicators[tinyram_opcode_STOREW]),
292  ls_prev_val_as_doubleword_variable->packed -
293  ls_next_val_as_doubleword_variable->packed,
294  0),
295  FMT(this->annotation_prefix,
296  " non_store_instructions_dont_change_memory"));
297 
298  /* specify that accepting state implies opcode = answer && arg2val == 0 */
299  this->pb.add_r1cs_constraint(
300  r1cs_constraint<FieldT>(
301  next_has_accepted, 1 - opcode_indicators[tinyram_opcode_ANSWER], 0),
302  FMT(this->annotation_prefix, " accepting_requires_answer"));
303  this->pb.add_r1cs_constraint(
304  r1cs_constraint<FieldT>(next_has_accepted, arg2val->packed, 0),
305  FMT(this->annotation_prefix, " accepting_requires_arg2val_equal_zero"));
306 
307  /*
308  handle tapes:
309 
310  we require that:
311  prev_tape1_exhausted implies next_tape1_exhausted,
312  prev_tape1_exhausted implies flag to be set
313  reads other than from tape 1 imply flag to be set
314  flag implies result to be 0
315  */
316  this->pb.add_r1cs_constraint(
317  r1cs_constraint<FieldT>(
318  prev_tape1_exhausted, 1 - next_tape1_exhausted, 0),
319  FMT(this->annotation_prefix,
320  " prev_tape1_exhausted_implies_next_tape1_exhausted"));
321  this->pb.add_r1cs_constraint(
322  r1cs_constraint<FieldT>(
323  prev_tape1_exhausted,
324  1 - instruction_flags[tinyram_opcode_READ],
325  0),
326  FMT(this->annotation_prefix, " prev_tape1_exhausted_implies_flag"));
327  this->pb.add_r1cs_constraint(
328  r1cs_constraint<FieldT>(
329  opcode_indicators[tinyram_opcode_READ],
330  1 - arg2val->packed,
331  read_not1),
332  FMT(this->annotation_prefix,
333  " read_not1")); /* will be nonzero for read X for X != 1 */
334  this->pb.add_r1cs_constraint(
335  r1cs_constraint<FieldT>(
336  read_not1, 1 - instruction_flags[tinyram_opcode_READ], 0),
337  FMT(this->annotation_prefix, " other_reads_imply_flag"));
338  this->pb.add_r1cs_constraint(
339  r1cs_constraint<FieldT>(
340  instruction_flags[tinyram_opcode_READ],
341  instruction_results[tinyram_opcode_READ],
342  0),
343  FMT(this->annotation_prefix, " read_flag_implies_result_0"));
344 }
345 
346 template<typename FieldT>
347 void tinyram_cpu_checker<FieldT>::generate_r1cs_witness_address()
348 {
349  /* decode instruction and arguments */
350  prev_pc_addr_as_word_variable->generate_r1cs_witness_from_bits();
351  for (size_t i = 0; i < this->pb.ap.k; ++i) {
352  prev_registers[i].generate_r1cs_witness_from_bits();
353  }
354 
355  decode_arguments->generate_r1cs_witness();
356 
357  desval->generate_r1cs_witness_from_packed();
358  arg1val->generate_r1cs_witness_from_packed();
359  arg2val->generate_r1cs_witness_from_packed();
360 
361  /* clear out ls_addr and fill with everything of arg2val except the
362  * subaddress */
363  ls_addr.fill_with_bits_of_field_element(
364  this->pb,
365  this->pb.val(arg2val->packed).as_ulong() >> this->pb.ap.subaddr_len());
366 }
367 
368 template<typename FieldT>
369 void tinyram_cpu_checker<FieldT>::generate_r1cs_witness_other(
370  tinyram_input_tape_iterator &aux_it,
371  const tinyram_input_tape_iterator &aux_end)
372 {
373  /* now ls_prev_val is filled with memory contents at ls_addr. we
374  now ensure consistency with its doubleword representation */
375  ls_prev_val_as_doubleword_variable->generate_r1cs_witness_from_bits();
376 
377  /* fill in the opcode indicators */
378  const size_t opcode_val =
379  opcode.get_field_element_from_bits(this->pb).as_ulong();
380  for (size_t i = 0; i < 1ul << this->pb.ap.opcode_width(); ++i) {
381  this->pb.val(opcode_indicators[i]) =
382  (i == opcode_val ? FieldT::one() : FieldT::zero());
383  }
384 
385  /* execute the ALU */
386  ALU->generate_r1cs_witness();
387 
388  /* fill memory_subaddress */
389  memory_subaddress->bits.fill_with_bits(
390  this->pb,
391  pb_variable_array<FieldT>(
392  arg2val->bits.begin(),
393  arg2val->bits.begin() + +this->pb.ap.subaddr_len())
394  .get_bits(this->pb));
395  memory_subaddress->generate_r1cs_witness_from_bits();
396 
397  /* we distinguish four cases for memory handling:
398  a) load.b
399  b) store.b
400  c) store.w
401  d) load.w or any non-memory instruction */
402  const size_t prev_doubleword =
403  this->pb.val(ls_prev_val_as_doubleword_variable->packed).as_ulong();
404  const size_t subaddress =
405  this->pb.val(memory_subaddress->packed).as_ulong();
406 
407  if (this->pb.val(opcode_indicators[tinyram_opcode_LOADB]) ==
408  FieldT::one()) {
409  const size_t loaded_byte = (prev_doubleword >> (8 * subaddress)) & 0xFF;
410  this->pb.val(instruction_results[tinyram_opcode_LOADB]) =
411  FieldT(loaded_byte);
412  this->pb.val(memory_subcontents) = FieldT(loaded_byte);
413  } else if (
414  this->pb.val(opcode_indicators[tinyram_opcode_STOREB]) ==
415  FieldT::one()) {
416  const size_t stored_byte =
417  (this->pb.val(desval->packed).as_ulong()) & 0xFF;
418  this->pb.val(memory_subcontents) = FieldT(stored_byte);
419  } else if (
420  this->pb.val(opcode_indicators[tinyram_opcode_STOREW]) ==
421  FieldT::one()) {
422  const size_t stored_word = (this->pb.val(desval->packed).as_ulong());
423  this->pb.val(memory_subcontents) = FieldT(stored_word);
424  } else {
425  const bool access_is_word0 =
426  (this->pb.val(*memory_subaddress->bits.rbegin()) == FieldT::zero());
427  const size_t loaded_word =
428  (prev_doubleword >> (access_is_word0 ? 0 : this->pb.ap.w)) &
429  ((1ul << this->pb.ap.w) - 1);
430  this->pb.val(instruction_results[tinyram_opcode_LOADW]) = FieldT(
431  loaded_word); /* does not hurt even for non-memory instructions */
432  this->pb.val(memory_subcontents) = FieldT(loaded_word);
433  }
434 
435  memory_access_is_word.evaluate(this->pb);
436  memory_access_is_byte.evaluate(this->pb);
437 
438  check_memory->generate_r1cs_witness();
439 
440  /* handle reads */
441  if (this->pb.val(prev_tape1_exhausted) == FieldT::one()) {
442  /* if tape was exhausted before, it will always be
443  exhausted. we also need to only handle reads from tape 1,
444  so we can safely set flag here */
445  this->pb.val(next_tape1_exhausted) = FieldT::one();
446  this->pb.val(instruction_flags[tinyram_opcode_READ]) = FieldT::one();
447  }
448 
449  this->pb.val(read_not1) =
450  this->pb.val(opcode_indicators[tinyram_opcode_READ]) *
451  (FieldT::one() - this->pb.val(arg2val->packed));
452  if (this->pb.val(read_not1) != FieldT::one()) {
453  /* reading from tape other than 0 raises the flag */
454  this->pb.val(instruction_flags[tinyram_opcode_READ]) = FieldT::one();
455  } else {
456  /* otherwise perform the actual read */
457  if (aux_it != aux_end) {
458  this->pb.val(instruction_results[tinyram_opcode_READ]) =
459  FieldT(*aux_it);
460  if (++aux_it == aux_end) {
461  /* tape has ended! */
462  this->pb.val(next_tape1_exhausted) = FieldT::one();
463  }
464  } else {
465  /* handled above, so nothing to do here */
466  }
467  }
468 
469  /* flag implies result zero */
470  if (this->pb.val(instruction_flags[tinyram_opcode_READ]) == FieldT::one()) {
471  this->pb.val(instruction_results[tinyram_opcode_READ]) = FieldT::zero();
472  }
473 
474  /* execute consistency enforcer */
475  consistency_enforcer->generate_r1cs_witness();
476  next_pc_addr_as_word_variable->generate_r1cs_witness_from_packed();
477 
478  for (size_t i = 0; i < this->pb.ap.k; ++i) {
479  next_registers[i].generate_r1cs_witness_from_packed();
480  }
481 
482  /* finally set has_accepted to 1 if both the opcode is ANSWER and arg2val is
483  * 0 */
484  this->pb.val(next_has_accepted) =
485  (this->pb.val(opcode_indicators[tinyram_opcode_ANSWER]) ==
486  FieldT::one() &&
487  this->pb.val(arg2val->packed) == FieldT::zero())
488  ? FieldT::one()
489  : FieldT::zero();
490 }
491 
492 template<typename FieldT> void tinyram_cpu_checker<FieldT>::dump() const
493 {
494  printf(
495  " pc = %lu, flag = %lu\n",
496  this->pb.val(prev_pc_addr_as_word_variable->packed).as_ulong(),
497  this->pb.val(prev_flag).as_ulong());
498  printf(" ");
499 
500  for (size_t j = 0; j < this->pb.ap.k; ++j) {
501  printf(
502  "r%zu = %2lu ",
503  j,
504  this->pb.val(prev_registers[j].packed).as_ulong());
505  }
506  printf("\n");
507 
508  const size_t opcode_val =
509  opcode.get_field_element_from_bits(this->pb).as_ulong();
510  printf(
511  " %s r%lu, r%lu, %s%lu\n",
512  tinyram_opcode_names[static_cast<tinyram_opcode>(opcode_val)].c_str(),
513  desidx.get_field_element_from_bits(this->pb).as_ulong(),
514  arg1idx.get_field_element_from_bits(this->pb).as_ulong(),
515  (this->pb.val(arg2_is_imm) == FieldT::one() ? "" : "r"),
516  arg2idx.get_field_element_from_bits(this->pb).as_ulong());
517 }
518 
519 } // namespace libsnark
520 
521 #endif // TINYRAM_CPU_CHECKER_TCC_
Generated on Wed Jan 25 2023 11:05:57 for Clearmatics Libsnark by   doxygen 1.8.17