sia.hackernoon.com

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

and: the instruction and ri rj A will store the bits and results of [rj] and [A] in the ri register. As well, if the result is 0^{W}, set flag to 1, and otherwise set it to 0.
or instruction or ri rj A will store the bits and results of [rj] and [A] in the ri register. As well, if the result is 0^{W}, set flag to 1, and otherwise set it to 0.
xor instruction xor ri rj A will store the bits and results of [rj] and [A] in the ri register. As well, if the result is 0^{W}, set flag to 1, and otherwise set it to 0.
not instruction not ri A will store the bits and results of [rj] and [A] in the ri register. As well, if the result is 0^{W}, set flag to 1, and otherwise set it to 0.

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 flag to 1 , and otherwise set it to 0.

In the following part, U_{W} represents a series of integers {0*,…,* $2^{W} -1 $}; These integers are made up of W-bit strings. S_{W} represents a series of integers {−2^(W−1),… 0, 1, $2 ^ $} {} W - 1-1. These integers are also made up of W-bit strings.

add: instruction add ri rj A 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 G = [rj]_u + [A]_u. In addition, flag will be set to G_{W}. G_{W} is the most significant bit (MSB) of G.
sub: instruction sub ri rj A 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 G = [rj]_u + 2^W − [A]_u. In addition, flag will be set to 1−G_{W}. G_{W} is the most significant bit (MSB) of G.
mull instruction mull ri rj A 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 G=[rj]_u∗[A]_u. In addition, flag will be set to 1 if

[rj]_u × [A]u ∉ U{W}, and otherwise set it to 0.
umulh instruction umulh ri rj A 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 G = [rj]_u ∗ [A]_u. In addition, flag will be set to 1 if [rj]_u × [A]u ∉ U{W}, and otherwise set it to 0.
smulh instruction smulh ri rj A will store the W-bit string a_{W−1}⋯a_{0} into the ri. a_{W−1} is the the sign bit of [rj]u ∗ [A]u, a{W−2}⋯a{0} is the W - 1 MSB of [rj]_u ∗ [A]_u. In addition, flag will be set to 1 if [rj]_u × [A]u ∉ S{W} , and otherwise set it to 0.

udiv instuction udiv ri rj A will store the W-bit string a_{W−1}⋯a_{0} into the ri.

If [A]u = 0, a{W−1}⋯a_{0} = 0^W.

If [A]u∣ ≠ 0, a{W−1}⋯a_{0} is the only binary encoding of the integer Q, making that for some integers R ∈ {0,…,[A]_u − 1}, the formula [rj]_u = [A]_u × Q + R is workable. In addition, only when [A]_u=0, flag will be set to 1.

umod instruction umod ri rj A will store the W-bit string a_{W−1}⋯a_{0} into the ri.

If [A]u = 0, a{W−1}⋯a_{0} = 0^W.

If [A]u∣ ≠ 0, a{W−1}⋯a_{0} is the only binary encoding of the integer R, whose value range is

{0,…,[A]_u−1}, making the formula [rj]_u = [A]_u × Q+R wokable for some Q values. In addition, only when [A]_u = 0, flag will be set to 1.

Shift-related Operation

shl instruction shl ri rj A 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].
shr instruction shr ri rj A 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].

Compare-related Operation

Each instruction in the compare-related operation does not modify any registers; The comparison results will be stored in flag.

cmpe instruction cmpe ri A will set flag to 1 if [ri] = [A], and otherwise set it to 0
cmpa instruction cmpa ri A will set flag to 1 if [ri]_u > [A]_u, and otherwise set it to 0
cmpae instruction cmpae ri A will set flag to 1 if [ri]_u ≥ [A]_u, and otherwise set it to 0
cmpg instruction cmpg ri A will set flag to 1 if [ri]_s > [A]_s, and otherwise set it to 0
cmpge instruction cmpge ri A will set flag to 1 if [ri]_S ≥ [A]_S, and otherwise set it to 0

Move-related Operation

mov instruction mov ri A will store [A] into the ri register.
cmov instruction cmov ri A will store [A] into the ri register if flag = 1 and otherwise the value of the ri register will not change.

Jump-related

These jump and conditional jump instructions will not modify the register and flag, but will modify the pc.

jump instruction jmp A will store [A] into pc.
cjmp instruction cjmp A will store [A] into pc when flag = 1, and otherwise increments pc by 1
cnjmp instruction cnjmp A will store [A] into pc when flag = 0, and otherwise increments pc by 1

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).

store.b instruction store A ri will store the LSB of [ri] at the [A] U-th byte address in memory.
load.b instruction load ri A will store the contents of the [A] U-th byte address in memory into the ri register (filling with 0 in the front bytes).
store.w instruction store.w A ri will store [ri] in word position aligned with the [A]w-th byte in memory.
load.w instruction load.w ri A has stored the word in its memory aligned with the [A]w byte into the ri register.

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.

read instruction read ri A 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 flag = 0; Otherwise (if there are no rest input words on the [A]u tape), store 0^W into ri and set flag = 1.

Since TinyRAM only has two input tapes, all tapes except the first two are assumed to be empty.

Specifically, if [A]u is not 0 or 1, then we store 0^W in the ri and set flag=1.

Output-related Operation

This instruction means that the program has finished its computation and no other operations are allowed.

answer instruction answer A 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.

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 S of inner product value is accord with R1CS constraints A_i, B_i, C_i represents the row vector in the matrix).

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

and constraint formula:

 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<FieldT>(
                { 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<FieldT>(
            { ONE },
            { ONE, this->not_all_zeros_result * (-1) },
            { this->result_flag }),
        FMT(this->annotation_prefix, " result_flag"));

or constraint formula:

 (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<FieldT>(
                  { 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<FieldT>(
            { ONE },
            { ONE, this->not_all_zeros_result * (-1) },
            { this->result_flag }),
        FMT(this->annotation_prefix, " result_flag"));

xor constraint formula:

  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<FieldT>(
                { 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<FieldT>(
            { ONE },
            { ONE, this->not_all_zeros_result * (-1) },
            { this->result_flag }),
        FMT(this->annotation_prefix, " result_flag"));

not constraint formula:

1 * （1 - b） = c

Specific constraint steps are as follows:

         this->pb.add_r1cs_constraint(
             r1cs_constraint<FieldT>(
                 { 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<FieldT>(
            { ONE },
            { ONE, this->not_all_zeros_result * (-1) },
            { this->result_flag }),
        FMT(this->annotation_prefix, " result_flag"));

Integer-related Operation Constraint

add: constraint formula:

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<FieldT>(
            { 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

sub: constraint formula:

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<FieldT> a, b, c;

a.add_term(0, 1);
for (size_t i = 0; i < this->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<FieldT>(a, b, c), FMT(this->annotation_prefix, " main_constraint"));

The decoding result constraint and boolean constraint
Sign bit constraint

mull, umulh and smulh constraint formula:
```
c = a * b
```
Mull-related constraints all involve the following steps:
1. Constraints of computing multiplication
2. Constraints of computing results coding
3. Flag constraints of computation result
udiv and umod constraint formula:

  B * q + r = A

  r <= B

‘B’ is the divisor, ‘q’ is the quotient, and ‘r’ is the remainder. The remainder must not exceed the divisor. The specific constraint codes are as follows:

  /* B_inv * B = B_nonzero */
        linear_combination<FieldT> 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<FieldT>(a1, b1, c1), FMT(this->annotation_prefix, " B_inv*B=B_nonzero"));

        /* (1-B_nonzero) * B = 0 */
        linear_combination<FieldT> 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<FieldT>(a2, b2, c2), FMT(this->annotation_prefix, " (1-B_nonzero)*B=0"));

        /* B * q + r = A_aux = A * B_nonzero */
        linear_combination<FieldT> 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<FieldT>(a3, b3, c3), FMT(this->annotation_prefix, " B*q+r=A_aux"));

        linear_combination<FieldT> 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<FieldT>(a4, b4, c4), FMT(this->annotation_prefix, " A_aux=A*B_nonzero"));

        /* q * (1-B_nonzero) = 0 */
        linear_combination<FieldT> 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<FieldT>(a5, b5, c5), FMT(this->annotation_prefix, " q*B_nonzero=0"));

        /* A<B_gadget<FieldT>(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 flag. Compare instructions include cmpe, cmpa, cmpae. cmpg and cmpge, which can be divided into two types: signed number comparison and unsigned number comparison, both of which use the realized comparison_gadget of libsnark in their constraint process core.

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<FieldT>(
                {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<FieldT>(
                {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<FieldT>(
                {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

mov constraint formula:

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 flag, so the constraint needs to ensure that the flag value does not change. The constraint code is as follows:

this->pb.add_r1cs_constraint(
  r1cs_constraint<FieldT>(
    {ONE},
    {this->arg2val.packed},
    {this->result}),
  FMT(this->annotation_prefix, " mov_result"));

this->pb.add_r1cs_constraint(
  r1cs_constraint<FieldT>(
    {ONE},
    {this->flag},
    {this->result_flag}),
  FMT(this->annotation_prefix, " mov_result_flag"));

cmov constraint formula:

 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<FieldT>(
                {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<FieldT>(
                {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 flag but will modify 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<FieldT>(
            { ONE },
            { pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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<FieldT>(
            this->flag,
            pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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<FieldT>(
            this->flag,
            this->pc.packed + 1 - pb_packing_sum<FieldT>(pb_variable_array<FieldT>(this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())),
            this->result - pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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).

store.b and 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<FieldT>(opcode_indicators[tinyram_opcode_STOREW],
                                memory_subcontents - desval->packed,
                                                         0),
                                 FMT(this->annotation_prefix, " handle_storew"));
    this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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"));

load.b and 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<FieldT>(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<FieldT>(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<FieldT>(opcode_indicators[tinyram_opcode_STOREB],
memory_subcontents - pb_packing_sum<FieldT>(
pb_variable_array<FieldT>(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 flag is set to 1
If the read instruction is exected now, then the content read catches is consistent with the input content of the tape
Read content from outside of type1, flag is set to 1
Whether the result is 0 means the flag is 0

Constraint code:

this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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<FieldT>(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<FieldT>(opcode_indicators[tinyram_opcode_READ],
                                                     1 - arg2val->packed,
                                                     read_not1),
                             FMT(this->annotation_prefix, " read_not1")); 
this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(read_not1,
                                                     1 - instruction_flags[tinyram_opcode_READ],
                                                     0),
                             FMT(this->annotation_prefix, " other_reads_imply_flag"));
this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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 answer and arg2 value is 0.

Constraint code is as follows:

    this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(next_has_accepted,
                                                         1 - opcode_indicators[tinyram_opcode_ANSWER],
                                                         0),
                                 FMT(this->annotation_prefix, " accepting_requires_answer"));
    this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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 tinyram review ppt, showing the time consumption required for an ERC20 transfer to generate a proof via TinyRAM.

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.

What is a TinyRAM Instruction Set?

Introduction

TinyRAM Instruction Set

Bit-related Operation

Integer-related Operation

Shift-related Operation

Compare-related Operation

Move-related Operation

Jump-related

Memory-related Operation

Input-related Operation

Output-related Operation

Constraint of Instruction Set

Bit-related Constraint

Integer-related Operation Constraint

Compare Operation

Move Operation Constraint

Jump Operation Constraint

Memory Operation Constraint

Input Operation Constraint

Output Operation Constraints

Other