# Sin7Y Tech Review (26): TinyRAM instruction set and circuit constraints
## 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 Review-English](https://sin7y.org/tinyram-review-architecture-design-and-assembly-instructions-774c904dbaee)
## 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} \cdots a_{0}$ into the ri. $a_{W-1} \cdots a_{0}$ is the W least significant bit (LSB) of $G=[\mathrm{r} j]_{\mathrm{u}}+[A]_{\mathrm{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} \cdots a_{0}$ into the ri. $a_{W-1} \cdots a_{0}$ is the W least significant bit (LSB) of $G=[\mathrm{r} j]_{\mathrm{u}}+ {2^{W}}-[A]_{\mathrm{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} \cdots a_{0}$ into the ri. $a_{W-1} \cdots a_{0}$ is the W least significant bit (LSB) of $G=[\mathrm{r} j]_{\mathrm{u}} * [A]_{\mathrm{u}}$. In addition, ` flag` will be set to 1 if $[r j]_{\mathrm{u}} \times[A]_{\mathrm{u}} \notin U_{W}$, and otherwise set it to 0.
* **umulh** instruction `umulh ri rj A` will store the W-bit string $a_{W-1} \cdots a_{0}$ into the ri. $a_{W-1} \cdots a_{0}$ is the W most significant bit (MSB) of $G=[\mathrm{r} j]_{\mathrm{u}} * [A]_{\mathrm{u}}$ . In addition, ` flag` will be set to 1 if $[r j]_{\mathrm{u}} \times[A]_{\mathrm{u}} \notin U_{W}$ , and otherwise set it to 0.
* **smulh** instruction `smulh ri rj A ` will store the W-bit string $a_{W-1} \cdots a_{0}$ into the ri. $a_{W-1}$ is the the sign bit of $[\mathrm{r} j]_{\mathrm{u}} * [A]_{\mathrm{u}}$ , $a_{W-2} \cdots a_{0}$ is the W - 1 MSB of $[\mathrm{r} j]_{\mathrm{u}} * [A]_{\mathrm{u}}$. In addition, ` flag` will be set to 1 if $[r j]_{\mathrm{u}} \times[A]_{\mathrm{u}} \notin S_{W}$ , and otherwise set it to 0.
**udiv** instuction `udiv ri rj A ` will store the W-bit string $a_{W-1} \cdots a_{0}$ into the ri.
If $[A]_u = 0$ , $a_{W-1} \cdots a_{0}$ = $0^{W}$.
If $[A]_{\mathrm{u} \mid} \neq 0$, $a_{W-1} \cdots a_{0}$ is the only binary encoding of the integer Q, making that for some integers $R \in\left\{0, \ldots,[A]_{\mathrm{u}}-1\right\}$, the formula $[\mathrm{r} j]_{\mathrm{u}}=[A]_{\mathrm{u}} \times 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} \cdots a_{0}$ into the ri.
If $[A]_u = 0$ , $a_{W-1} \cdots a_{0}$ = $0^{W}$.
If $[A]_{\mathrm{u} \mid} \neq 0$, $a_{W-1} \cdots a_{0}$ *is the only binary encoding of the integer R,* whose value range is $\left\{0, \ldots,[A]_{\mathrm{u}}-1\right\}$, making the formula $[\mathrm{r} j]_{\mathrm{u}}=[A]_{\mathrm{u}} \times 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 $[\mathrm{r} i]_{\mathrm{u}}>[A]_{\mathrm{u}}$, and otherwise set it to 0
* **cmpae** instruction `cmpae ri A` will set flag to 1 if $[\mathrm{ri}]_{\mathrm{u}} \geq[A]_{\mathrm{u}}$, and otherwise set it to 0
* **cmpg** instruction `cmpg ri A` will set flag to 1 if $[\mathrm{r} i]_{\mathrm{s}}>[A]_{\mathrm{s}}$, and otherwise set it to 0
* **cmpge** instruction `cmpge ri A` will set flag to 1 if $[r i]_{\mathrm{S}} \geq[A]_{\mathrm{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 ontherwise cincrements 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 <u>tapes</u> 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:
$$
\left(A_{i} * S\right) *\left(B_{i} * S\right)-C_{i} * 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:
```c++
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:
1. The computation process constraint, and the code is as follows:
```c++
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));
```
2. The result coding constraint
3. 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}
*/
```
4. Flag constraint
```c++
/* 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:
```c++
(1 - a) * (1 - b) = (1 - c)
```
Specific constraint steps are as follows:
1. The computation process constraint, and the code is as follows:
```c++
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));
```
2. The result coding constraint
3. The computation results are not all zero constraints (consistent with the instruction definition, and this process is mainly in preparation for the constraint flag)
4. Flag constraint
```c++
/* 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++
c = a ^ b <=> c = a + b - 2*a*b, (2*b)*a = a+b - c
```
Specific constraint steps are as follows:
1. The computation process constraint, and the code is as follows:
```c++
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));
```
2. The result coding constraint
3. The computation results are not all zero constraints (consistent with the instruction definition, and this process is mainly in preparation for the constraint flag)
4. Flag constraint
```c++
/* 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:
```c++
1 * （1 - b） = c
```
Specific constraint steps are as follows:
1. ```c++
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));
```
2. The result coding constraint
3. The computation results are not all zero constraints (consistent with the instruction definition, and this process is mainly in preparation for the constraint flag)
4. Flag constraint
```c++
/* 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:
```c++
1 * （a + b） = c
```
Specific constraint steps are as follows:
1. The computation process constraint, the code is as follows:
```c++
this->pb.add_r1cs_constraint(
r1cs_constraint<FieldT>(
{ ONE },
{ this->arg1val.packed, this->arg2val.packed },
{ this->addition_result }),
FMT(this->annotation_prefix, " addition_result"));
```
2. The decoding result constraint and boolean constraint
3. 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
```
1. The computation process constraint:
```c++
/* 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"));
```
2. The decoding result constraint and boolean constraint
3. Sign bit constraint
* **mull, umulh and smulh** constraint formula:
```c++
c = a * b
```
Mull-related constraints all involve the following steps:
1. <u>Constraints of computing multiplication</u>
2. <u>Constraints of computing results coding</u>
3. <u>Flag constraints of computation result </u>
* **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:
```c++
/* 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:
```c++
/* 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:
```c++
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 <u>the code is as follows:</u>
```c++
/*
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:
```c++
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:
```c++
flag1 * argval2 + (1-flag1) * (pc1 + 1) = cjmp_result
flag1 * (argval2 - pc1 - 1) = cjmp_result - pc1 - 1
```
The constraint code is as follows:
```c++
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:
```c++
flag1 * (pc1 + 1) + (1-flag1) * argval2 = cnjmp_result
flag1 * (pc1 + 1 - argval2) = cnjmp_result - argval2
```
The constraint code is as follows:
```c++
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:
```c++
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:
```c++
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:
1. When the previous tape is finished and there are contents to read, the next tape is not allowed to be read.
2. When the previous tape is finished and there are contents to read, the `flag` is set to 1
3. If the `read` instruction is exected now, then the content read catches is consistent with the input content of the tape
4. Read content from outside of type1, `flag ` is set to 1
5. Whether the `result` is 0 means the `flag` is 0
constraint code:
```c++
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:
```c++
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](https://docs.google.com/presentation/d/1lbyLmXhCry61fxWm8LLxPKhCYV67RcZaK3WL20Hb-t8/edit#slide=id.g5b38da04a0_0_21), 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.
Sign in with Wallet
Connect another wallet