What is a TinyRAM Instruction Set?

Introduction TinyRAM is a simple Reduced Instruction Set Computer (RISC) with byte-level addressable random-access memory and input tapes. There are two variants of TinyRAM: one follows the Harvard (hv) architecture, and the other follows the von Neumann (vn) architecture (in this article, we mainly focus on the von Neumann architecture). The Succinct Computational Integrity and Privacy Research (SCIPR) project construct mechanisms for proving the correct execution of TinyRAM programs, and TinyRAM is designed for efficiency in this setting. It strikes a balance between two opposing requirements — “sufficient expressibility” and “small instruction set”: Sufficient expressibility to support short, efficient assembly code when compiled from high-level programming languages, Small instruction set to support simple verification via arithmetic circuits and efficient verification using SCIPR’s algorithms and cryptographic mechanisms. In this article, we will supplement the previous article rather than a repeating TinyRAM introduction, and then focus on the introduction of instructions and circuit constraints. For a basic introduction to TinyRAM, please refer to our previous article: tinyram简介-中文 TinyRAM Review-English TinyRAM Instruction Set TinyRAM supports 29 instructions, each specified by an opcode and up to 3 operands. The operand can be either a name of a register (i.e., integers from 0 to K-1) or an immediate value (i.e., W-bit strings). Unless otherwise specified, each instruction does not modify the flag separately and increments pc by i (i % 2^W) by default, i=2W/8 for the vnTinyRAM. In general, the first operand is the target register for instruction computation and the other operands specify the parameters required by the instructions. Finally, all instructions take one cycle of the machine to execute. Bit-related Operation : the instruction will store the bits and results of [rj] and [A] in the ri register. As well, if the result is , set to 1, and otherwise set it to 0. and and ri rj A 0^{W} flag instruction will store the bits and results of [rj] and [A] in the ri register. As well, if the result is , set to 1, and otherwise set it to 0. or or ri rj A 0^{W} flag instruction will store the bits and results of [rj] and [A] in the ri register. As well, if the result is , set to 1, and otherwise set it to 0. xor xor ri rj A 0^{W} flag instruction will store the bits and results of [rj] and [A] in the ri register. As well, if the result is , set to 1, and otherwise set it to 0. not not ri A 0^{W} flag Integer-related Operation These are variously unsigned and signed integer-related operations. In each setting, if an arithmetic overflow or error occurs (such as dividing by zero), set to 1 , and otherwise set it to 0. flag In the following part, represents a series of integers {0*,…,* $2^{W} -1 $}; These integers are made up of W-bit strings. represents a series of integers {−2^(W−1),… 0, 1, $2 ^ $} {} W - 1-1. These integers are also made up of W-bit strings. U_{W} S_{W} instruction will store the W-bit string a_{W−1}⋯a_{0} into the ri. a_{W−1}⋯a_{0} is the W least significant bit (LSB) of . In addition, will be set to . is the most significant bit (MSB) of G. add: add ri rj A G = [rj]_u + [A]_u flag G_{W} G_{W} instruction will store the W-bit string a_{W−1}⋯a_{0} into the ri. a_{W−1}⋯a_{0} is the W least significant bit (LSB) of . In addition, will be set to . is the most significant bit (MSB) of G. sub: sub ri rj A G = [rj]_u + 2^W − [A]_u flag 1−G_{W} G_{W} instruction will store the W-bit string a_{W−1}⋯a_{0} into the ri. a_{W−1}⋯a_{0} is the W least significant bit (LSB) of . In addition, will be set to 1 if mull mull ri rj A G=[rj]_u∗[A]_u flag , and otherwise set it to 0. [rj]_u × [A] {W} u ∉ U instruction will store the W-bit string a_{W−1}⋯a_{0} into the ri. a_{W−1}⋯a_{0} is the W most significant bit (MSB) of . In addition, will be set to 1 if , and otherwise set it to 0. umulh umulh ri rj A G = [rj]_u ∗ [A]_u flag [rj]_u × [A] {W} u ∉ U instruction will store the W-bit string a_{W−1}⋯a_{0} into the ri. a_{W−1} is the the sign bit of is the W - 1 MSB of . In addition, will be set to 1 if } , and otherwise set it to 0. smulh smulh ri rj A [rj] {W−2}⋯a{0} u ∗ [A]u, a [rj]_u ∗ [A]_u flag [rj]_u × [A] {W u ∉ S instuction will store the W-bit string a_{W−1}⋯a_{0} into the ri. udiv udiv ri rj A If . [A] {W−1}⋯a_{0} = 0^W u = 0, a If is the only binary encoding of the integer Q, making that for some integers , the formula is workable. In addition, only when , will be set to 1. [A] {W−1}⋯a_{0} u∣ ≠ 0, a R ∈ {0,…,[A]_u − 1} [rj]_u = [A]_u × Q + R [A]_u=0 flag instruction will store the W-bit string a_{W−1}⋯a_{0} into the ri. umod umod ri rj A If . [A] {W−1}⋯a_{0} = 0^W u = 0, a If whose value range is [A] {W−1}⋯a_{0} u∣ ≠ 0, a is the only binary encoding of the integer R, , making the formula wokable for some Q values. In addition, only when , will be set to 1. {0,…,[A]_u−1} [rj]_u = [A]_u × Q+R [A]_u = 0 flag Shift-related Operation instruction will store the W-bit string obtained by [rj] left shifting for [A] u bit in the ri register. The blank positions after shifting are filled with 0. In addition, flag is set to the MSB of [rj]. shl shl ri rj A instruction will store the W-bit string obtained by [rj] right shifting for [A] u bit in the ri register. The blank positions after shifting are filled with 0. In addition, flag is set to the LSB of [rj]. shr shr ri rj A Compare-related Operation Each instruction in the compare-related operation does not modify any registers; The comparison results will be stored in . flag instruction will set flag to 1 if [ri] = [A], and otherwise set it to 0 cmpe cmpe ri A instruction will set flag to 1 if , and otherwise set it to 0 cmpa cmpa ri A [ri]_u > [A]_u instruction will set flag to 1 if , and otherwise set it to 0 cmpae cmpae ri A [ri]_u ≥ [A]_u instruction will set flag to 1 if , and otherwise set it to 0 cmpg cmpg ri A [ri]_s > [A]_s instruction will set flag to 1 if , and otherwise set it to 0 cmpge cmpge ri A [ri]_S ≥ [A]_S Move-related Operation instruction will store [A] into the ri register. mov mov ri A instruction will store [A] into the ri register if flag = 1 and otherwise the value of the ri register will not change. cmov cmov ri A Jump-related These jump and conditional jump instructions will not modify the register and , but will modify the . flag pc instruction will store [A] into pc. jump jmp A instruction will store [A] into pc when = 1, and otherwise increments pc by 1 cjmp cjmp A flag instruction will store [A] into pc when = 0, and otherwise increments pc by 1 cnjmp cnjmp A flag Memory-related Operation These are simple memory load operations and store operations, where the address of memory is determined by the immediate number or the contents of the register. These are the only addressing methods in TinyRAM. (TinyRAM does not support the common “base+offset” addressing mode). instruction will store the LSB of [ri] at the [A] U-th byte address in memory. store.b store A ri instruction will store the contents of the [A] U-th byte address in memory into the ri register (filling with 0 in the front bytes). load.b load ri A instruction will store [ri] in word position aligned with the [A]w-th byte in memory. store.w store.w A ri instruction has stored the word in its memory aligned with the [A]w byte into the ri register. load.w load.w ri A Input-related Operation This instruction is the only one that can access either of the tapes. The 0th tape was used for primary input and the first tape for user auxiliary input. instruction will store the next W-bit word on the [A] U tape into the ri register. To be more precise, if the [A]u tape has any rest word, the next word will be consumed and stored in ri, and set = 0; Otherwise (if there are no rest input words on the [A]u tape), store 0^W into ri and set = 1. read read ri A flag flag Since TinyRAM only has two input tapes, all except the first two are assumed to be empty. tapes Specifically, if [A]u is not 0 or 1, then we store 0^W in the ri and set =1. flag Output-related Operation This instruction means that the program has finished its computation and no other operations are allowed. instruction will cause the state machine to be “stall”(with no pc increase) or “halt”(stop computing), and return to [A]u. The choice between stall or halt is not defined. The return value 0 is used to indicate acceptance. answer answer A Constraint of Instruction Set TinyRAM has used R1CS constraint to perform circuit constraints, and the specific form is as follows: (Ai ∗ S) ∗ (Bi ∗ S) − Ci ∗ S = 0 Now, if we want to prove that we know a solution of the original computation, we will need to prove that in matrices A, B and C, every row vector and solution vector of inner product value is accord with R1CS constraints represents the row vector in the matrix). S A_i, B_i, C_i Each R1CS constraint can be represented by linear_combination a, b, or c. Assignments of all variables in an R1CS system can be divided into two parts: primary input and auxiliary input. The Primary is what we often call a “statement” and the auxiliary is “witness”. Each R1CS constraint system contains multiple R1CS constraints. The vector length for each constraint is fixed (primary Input size + auxiliary Input size + 1). TinyRAM has used a lot of custom gadgtes in the libsnark code implementation to express vm constraints as well as opcode execution and memory constraints. The specific code is in the gadgetslib1/ Gadgets /cpu_checkers/tinyram folder. Bit-related Constraint constraint formula: and a * b = c The R1CS constraint of and verifies parameter 1 and parameter 2 and the computation results in bit-by-bit multiplication. The constraint steps are as follows: The computation process constraint, and the code is as follows: this->pb.add_r1cs_constraint( r1cs_constraint ( { this->arg1val.bits[i] }, { this->arg2val.bits[i] }, { this->res_word[i] }), FMT(this->annotation_prefix, " res_word_%zu", i)); The result coding constraint The computation results are not all zero constraints (consistent with the instruction definition, and the process is mainly to prepare the constraint flag) /* the gadgets below are Fp specific: I * X = R (1-R) * X = 0 if X = 0 then R = 0 if X != 0 then R = 1 and I = X^{-1} */ Flag constraint /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); constraint formula: or (1 - a) * (1 - b) = (1 - c) Specific constraint steps are as follows: The computation process constraint, and the code is as follows: this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE, this->arg1val.bits[i] * (-1) }, { ONE, this->arg2val.bits[i] * (-1) }, { ONE, this->res_word[i] * (-1) }), FMT(this->annotation_prefix, " res_word_%zu", i)); The result coding constraint The computation results are not all zero constraints (consistent with the instruction definition, and this process is mainly in preparation for the constraint flag) Flag constraint /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); constraint formula: xor c = a ^ b c = a + b - 2*a*b, (2*b)*a = a+b - c Specific constraint steps are as follows: The computation process constraint, and the code is as follows: this->pb.add_r1cs_constraint( r1cs_constraint ( { this->arg1val.bits[i] * 2}, { this->arg2val.bits[i] }, { this->arg1val.bits[i], this->arg2val.bits[i], this->res_word[i] * (-1) }), FMT(this->annotation_prefix, " res_word_%zu", i)); The result coding constraint The computation results are not all zero constraints (consistent with the instruction definition, and this process is mainly in preparation for the constraint flag) Flag constraint /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); constraint formula: not 1 * （1 - b） = c Specific constraint steps are as follows: this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->arg2val.bits[i] * (-1) }, { this->res_word[i] }), FMT(this->annotation_prefix, " res_word_%zu", i)); The result coding constraint The computation results are not all zero constraints (consistent with the instruction definition, and this process is mainly in preparation for the constraint flag) Flag constraint /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); Integer-related Operation Constraint constraint formula: add: 1 * （a + b） = c Specific constraint steps are as follows: The computation process constraint, the code is as follows: this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { this->arg1val.packed, this->arg2val.packed }, { this->addition_result }), FMT(this->annotation_prefix, " addition_result")); The decoding result constraint and boolean constraint The coding result constraint constraint formula: sub: The sub constraint is slightly more complex than that of add, with an intermediate variable representing the a-b result, and 2^ w added to ensure that the result is computed as a positive integer and a sign. The specific constraint steps are as follows: intermediate_result = 2^w + a -b The computation process constraint: /* intermediate_result = 2^w + (arg1val - arg2val) */ FieldT twoi = FieldT::one(); linear_combination a, b, c; a.add_term(0, 1); for (size_t i = 0; i pb.ap.w; ++i) { twoi = twoi + twoi; } b.add_term(0, twoi); b.add_term(this->arg1val.packed, 1); b.add_term(this->arg2val.packed, -1); c.add_term(intermediate_result, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a, b, c), FMT(this->annotation_prefix, " main_constraint")); The decoding result constraint and boolean constraint Sign bit constraint constraint formula: mull, umulh and smulh c = a * b Mull-related constraints all involve the following steps: Constraints of computing multiplication Constraints of computing results coding Flag constraints of computation result constraint formula: udiv and umod B * q + r = A r a1, b1, c1; a1.add_term(B_inv, 1); b1.add_term(this->arg2val.packed, 1); c1.add_term(B_nonzero, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a1, b1, c1), FMT(this->annotation_prefix, " B_inv*B=B_nonzero")); /* (1-B_nonzero) * B = 0 */ linear_combination a2, b2, c2; a2.add_term(ONE, 1); a2.add_term(B_nonzero, -1); b2.add_term(this->arg2val.packed, 1); c2.add_term(ONE, 0); this->pb.add_r1cs_constraint(r1cs_constraint (a2, b2, c2), FMT(this->annotation_prefix, " (1-B_nonzero)*B=0")); /* B * q + r = A_aux = A * B_nonzero */ linear_combination a3, b3, c3; a3.add_term(this->arg2val.packed, 1); b3.add_term(udiv_result, 1); c3.add_term(A_aux, 1); c3.add_term(umod_result, -; this->pb.add_r1cs_constraint(r1cs_constraint (a3, b3, c3), FMT(this->annotation_prefix, " B*q+r=A_aux")); linear_combination a4, b4, c4; a4.add_term(this->arg1val.packed, 1); b4.add_term(B_nonzero, 1); c4.add_term(A_aux, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a4, b4, c4), FMT(this->annotation_prefix, " A_aux=A*B_nonzero")); /* q * (1-B_nonzero) = 0 */ linear_combination a5, b5, c5; a5.add_term(udiv_result, 1); b5.add_term(ONE, 1); b5.add_term(B_nonzero, -1); c5.add_term(ONE, 0); this->pb.add_r1cs_constraint(r1cs_constraint (a5, b5, c5), FMT(this->annotation_prefix, " q*B_nonzero=0")); /* A (B, r, less=B_nonzero, leq=ONE) */ r_less_B->generate_r1cs_constraints(); Compare Operation Each instruction in the compare operations will not modify any register; The comparison results are stored in . Compare instructions include , , . and , which can be divided into two types: signed number comparison and unsigned number comparison, both of which use the realized of libsnark in their constraint process core. flag cmpe cmpa cmpae cmpg cmpge comparison_gadget Unsigned number comparison constraint formula: cmpe_flag = cmpae_flag * (1-cmpa_flag) cmp and constraint code is as follows: comparator.generate_r1cs_constraints(); this->pb.add_r1cs_constraint( r1cs_constraint ( {cmpae_result_flag}, {ONE, cmpa_result_flag * (-1)}, {cmpe_result_flag}), FMT(this->annotation_prefix, " cmpa_result_flag")); Signed number comparison constraint formula: The unsigned number constraint is more complex than the signed number comparison constraint because there is more sign bit constraint processing. The sign bit constraint is as follows: /* negate sign bits */ this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {ONE, this->arg1val.bits[this->pb.ap.w - 1] * (-1)}, {negated_arg1val_sign}), FMT(this->annotation_prefix, " negated_arg1val_sign")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {ONE, this->arg2val.bits[this->pb.ap.w - 1] * (-1)}, {negated_arg2val_sign}), FMT(this->annotation_prefix, " negated_arg2val_sign")); The rest steps are the same as the signed number comparison constraint. Move Operation Constraint constraint formula: mov The mov constraint is relatively simple because it only needs to ensure that [A] is stored in ri register. The mov operation will not modify , so the constraint needs to ensure that the flag value does not change. The constraint code is as follows: flag this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->arg2val.packed}, {this->result}), FMT(this->annotation_prefix, " mov_result")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->flag}, {this->result_flag}), FMT(this->annotation_prefix, " mov_result_flag")); constraint formula: cmov flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval The constraint condition of cmov is more complex than that of mov, because the mov behaviors are related to the change of flag value, and cmov will not modify flag, so the constraint needs to ensure that the value of flag does not change, and the code is as follows: /* flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval */ this->pb.add_r1cs_constraint( r1cs_constraint ( {this->flag}, {this->arg2val.packed, this->desval.packed * (-1)}, {this->result, this->desval.packed * (-1)}), FMT(this->annotation_prefix, " cmov_result")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->flag}, {this->result_flag}), FMT(this->annotation_prefix, " cmov_result_flag")); Jump Operation Constraint These jump and conditional jump instructions will not modify the registers and but will modify . flag pc jmp The pc value is consistent with the execution result of the instruction in Jmp operation constraint, and the specific constraint code is as follows: this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())) }, { this->result }), FMT(this->annotation_prefix, " jmp_result")); cjmp cjmp will jump according to the flag condition when flag = 1, and otherwise increments pc by 1. The constraint formula is as follows: flag1 * argval2 + (1-flag1) * (pc1 + 1) = cjmp_result flag1 * (argval2 - pc1 - 1) = cjmp_result - pc1 - 1 The constraint code is as follows: this->pb.add_r1cs_constraint( r1cs_constraint ( this->flag, pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())) - this->pc.packed - 1, this->result - this->pc.packed - 1), FMT(this->annotation_prefix, " cjmp_result")); cnjmp The cnjmp will jump according to flag conditions. If flag = 0, the PC jumps and otherwise, increments pc by 1. The constraint formula is as follows: flag1 * (pc1 + 1) + (1-flag1) * argval2 = cnjmp_result flag1 * (pc1 + 1 - argval2) = cnjmp_result - argval2 The constraint code is as follows: this->pb.add_r1cs_constraint( r1cs_constraint ( this->flag, this->pc.packed + 1 - pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())), this->result - pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end()))), FMT(this->annotation_prefix, " cnjmp_result")); Memory Operation Constraint These are simple memory load and store operations, where the address of memory is determined by the immediate number or the contents of a register. These are the only addressing methods in TinyRAM. (TinyRAM does not support the common “base+offset” addressing mode). and store.b store.w For store.w, take all values of arg1val , and for store.b opcodes, only take the necessary part of arg1val (e.g., the last byte), and the constraint code is as follows: this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_STOREW], memory_subcontents - desval->packed, 0), FMT(this->annotation_prefix, " handle_storew")); this->pb.add_r1cs_constraint(r1cs_constraint (1 - (opcode_indicators[tinyram_opcode_STOREB] + opcode_indicators[tinyram_opcode_STOREW]), ls_prev_val_as_doubleword_variable->packed - ls_next_val_as_doubleword_variable->packed, 0), FMT(this->annotation_prefix, " non_store_instructions_dont_change_memory")); and load.b load.w For these two instructions, we require that the contents loaded from the memory be stored in instruction_results, and the constraint code is as follows: this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_LOADB], memory_subcontents - instruction_results[tinyram_opcode_LOADB], 0), FMT(this->annotation_prefix, " handle_loadb")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_LOADW], memory_subcontents - instruction_results[tinyram_opcode_LOADW], 0), FMT(this->annotation_prefix, " handle_loadw")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_STOREB], memory_subcontents - pb_packing_sum ( pb_variable_array (desval->bits.begin(), desval->bits.begin() + 8)), 0), FMT(this->annotation_prefix, " handle_storeb")); Input Operation Constraint read The read operation is related to tape, and the specific constraints are as follows: When the previous tape is finished and there are contents to read, the next tape is not allowed to be read. When the previous tape is finished and there are contents to read, the is set to 1 flag If the instruction is exected now, then the content read catches is consistent with the input content of the tape read Read content from outside of type1, is set to 1 flag Whether the is 0 means the is 0 result flag Constraint code: this->pb.add_r1cs_constraint(r1cs_constraint (prev_tape1_exhausted, 1 - next_tape1_exhausted, 0), FMT(this->annotation_prefix, " prev_tape1_exhausted_implies_next_tape1_exhausted")); this->pb.add_r1cs_constraint(r1cs_constraint (prev_tape1_exhausted, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " prev_tape1_exhausted_implies_flag")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_READ], 1 - arg2val->packed, read_not1), FMT(this->annotation_prefix, " read_not1")); this->pb.add_r1cs_constraint(r1cs_constraint (read_not1, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " other_reads_imply_flag")); this->pb.add_r1cs_constraint(r1cs_constraint (instruction_flags[tinyram_opcode_READ], instruction_results[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " read_flag_implies_result_0")); Output Operation Constraints This instruction indicates that the program has completed its computation and therefore no further operations are allowed answer When the program’s output value is accepted, has_accepted is set to 1, and the program’s return value is accepted normally, meaning that the current instruction is and arg2 value is 0. answer Constraint code is as follows: this->pb.add_r1cs_constraint(r1cs_constraint (next_has_accepted, 1 - opcode_indicators[tinyram_opcode_ANSWER], 0), FMT(this->annotation_prefix, " accepting_requires_answer")); this->pb.add_r1cs_constraint(r1cs_constraint (next_has_accepted, arg2val->packed, 0), FMT(this->annotation_prefix, " accepting_requires_arg2val_equal_zero")); Other Of course, in addition to some of the instruction-related constraints mentioned above, TinyRAM also has some constraints on pc consistency, parameter codec, memory checking, etc. These constraints are combined through the R1CS system to form a completed TinyRAM constraint system. Therefore, this is the root cause why a large number of TinyRAM constraints are generated in the form of R1CS. Here we refer to a figure of , showing the time consumption required for an ERC20 transfer to generate a proof via TinyRAM. tinyram review ppt It can be concluded from the example above: it is not possible to verify all EVM operations with vnTinyRam + zk-SNARks and it is only suitable for computational verification of a small number of instructions. The vnTinyram can be used to verify opcode for partial computation types of EVM.