1,087 leituras

O que é um conjunto de instruções TinyRAM?

por Sin7Y2022/06/21

Muito longo; Para ler

TinyRAM é um computador com conjunto de instruções reduzido (RISC) simples com memória de acesso aleatório endereçável em nível de byte e fitas de entrada. Existem duas variantes do TinyRAM: uma segue a arquitetura Harvard (hv) e a outra segue a arquitetura von Neumann (vn). A TinyRAM suporta 29 instruções, cada uma especificada por um opcode e até 3 operandos.

Companies Mentioned

Coin Mentioned

featured image - O que é um conjunto de instruções TinyRAM?

Introdução

TinyRAM é um computador com conjunto de instruções reduzido (RISC) simples com memória de acesso aleatório endereçável em nível de byte e fitas de entrada.

Existem duas variantes do TinyRAM: uma segue a arquitetura Harvard (hv) e a outra segue a arquitetura von Neumann (vn) (neste artigo, focamos principalmente na arquitetura von Neumann).

O projeto Sucinct Computational Integrity and Privacy Research (SCIPR) constrói mecanismos para provar a execução correta dos programas TinyRAM, e o TinyRAM foi projetado para eficiência nesse cenário. Ele atinge um equilíbrio entre dois requisitos opostos – “expressibilidade suficiente” e “pequeno conjunto de instruções”:

Expressibilidade suficiente para suportar código assembly curto e eficiente quando compilado a partir de linguagens de programação de alto nível,
Pequeno conjunto de instruções para suportar verificação simples por meio de circuitos aritméticos e verificação eficiente usando algoritmos e mecanismos criptográficos do SCIPR.

Neste artigo, complementaremos o artigo anterior em vez de repetir a introdução do TinyRAM e, em seguida, focaremos na introdução de instruções e restrições de circuito.

Para uma introdução básica ao TinyRAM, consulte nosso artigo anterior: tinyram简介-中文 TinyRAM Review-English

Conjunto de instruções TinyRAM

TinyRAM suporta 29 instruções, cada uma especificada por um opcode e até 3 operandos. O operando pode ser o nome de um registrador (isto é, inteiros de 0 a K-1) ou um valor imediato (isto é, strings de W-bit).

A menos que especificado de outra forma, cada instrução não modifica o sinalizador separadamente e incrementa pc em i (i % 2^W) por padrão, i=2W/8 para vnTinyRAM.

Em geral, o primeiro operando é o registrador de destino para a computação da instrução e os outros operandos especificam os parâmetros exigidos pelas instruções. Por fim, todas as instruções levam um ciclo da máquina para serem executadas.

Operação relacionada a bits

e : a instrução and ri rj A armazenará os bits e resultados de [rj] e [A] no registrador ri. Da mesma forma, se o resultado for 0^{W} , defina o flag como 1 e, caso contrário, defina-o como 0.
ou instrução or ri rj A armazenará os bits e resultados de [rj] e [A] no registrador ri. Da mesma forma, se o resultado for 0^{W} , defina o flag como 1 e, caso contrário, defina-o como 0.
A instrução xor xor ri rj A armazenará os bits e resultados de [rj] e [A] no registrador ri. Da mesma forma, se o resultado for 0^{W} , defina o flag como 1 e, caso contrário, defina-o como 0.
A instrução not not ri A armazenará os bits e resultados de [rj] e [A] no registrador ri. Da mesma forma, se o resultado for 0^{W} , defina o flag como 1 e, caso contrário, defina-o como 0.

Operação relacionada a inteiros

Essas são várias operações relacionadas a números inteiros não assinados e assinados. Em cada configuração, se ocorrer um estouro ou erro aritmético (como divisão por zero), defina flag como 1 e, caso contrário, defina-o como 0.

Na parte seguinte, U_{W} representa uma série de inteiros {0*,…,* $2^{W} -1 $}; Esses inteiros são compostos de strings de W-bit. S_{W} representa uma série de inteiros {−2^(W−1),… 0, 1, $2 ^ $} {} W - 1-1. Esses inteiros também são compostos de strings de W-bit.

add: a instrução add ri rj A armazenará a string de W-bit a_{W−1}⋯a_{0} no ri. a_{W−1}⋯a_{0} é o W bit menos significativo (LSB) de G = [rj]_u + [A]_u . Além disso, o flag será definido como G_{W} . G_{W} é o bit mais significativo (MSB) de G.
sub: a instrução sub ri rj A armazenará a string de W bits a_{W−1}⋯a_{0} no ri. a_{W−1}⋯a_{0} é o W bit menos significativo (LSB) de G = [rj]_u + 2^W − [A]_u . Além disso, o flag será definido como 1−G_{W} . G_{W} é o bit mais significativo (MSB) de G.
instrução mull mull ri rj A armazenará a string de W-bit a_{W−1}⋯a_{0} no ri. a_{W−1}⋯a_{0} é o W bit menos significativo (LSB) de G=[rj]_u∗[A]_u . Além disso, o flag será definido como 1 se
[rj]_u × [A] u ∉ U {W} e, caso contrário, defina-o como 0.
instrução umulh umulh ri rj A armazenará a string de W-bit a_{W−1}⋯a_{0} no ri. a_{W−1}⋯a_{0} é o W bit mais significativo (MSB) de G = [rj]_u ∗ [A]_u . Além disso, o flag será definido como 1 se [rj]_u × [A] u ∉ U {W} , caso contrário, será definido como 0.
A instrução smulh smulh ri rj A armazenará a string de W-bit a_{W−1}⋯a_{0} no ri. a_{W−1} é o bit de sinal de [rj] u ∗ [A]u, a {W−2}⋯a{0} é o W - 1 MSB de [rj]_u ∗ [A]_u . Além disso, o flag será definido como 1 se [rj]_u × [A] u ∉ S {W } , caso contrário, será definido como 0.

Instrução udiv udiv ri rj A armazenará a string de W-bit a_{W−1}⋯a_{0} no ri.

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

Se [A] u∣ ≠ 0, a {W−1}⋯a_{0} é a única codificação binária do inteiro Q, fazendo com que para alguns inteiros R ∈ {0,…,[A]_u − 1} , a fórmula [rj]_u = [A]_u × Q + R é viável. Além disso, somente quando [A]_u=0 , o flag será definido como 1.

instrução umod umod ri rj A armazenará a string de W-bit a_{W−1}⋯a_{0} no ri.

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

Se [A] u∣ ≠ 0, a {W−1}⋯a_{0} é a única codificação binária do inteiro R, cujo intervalo de valores é

{0,…,[A]_u−1} , tornando a fórmula [rj]_u = [A]_u × Q+R wokável para alguns valores Q. Além disso, somente quando [A]_u = 0 , o flag será definido como 1.

Operação relacionada a turno

A instrução shl shl ri rj A armazenará a sequência de W bits obtida pelo deslocamento à esquerda [rj] para o bit u [A] no registrador ri. As posições em branco após o deslocamento são preenchidas com 0. Além disso, o sinalizador é definido para o MSB de [rj].
A instrução shr shr ri rj A armazenará a cadeia de bits W obtida pelo deslocamento à direita [rj] para o bit u [A] no registrador ri. As posições em branco após o deslocamento são preenchidas com 0. Além disso, o sinalizador é definido como o LSB de [rj].

Operação relacionada a comparação

Cada instrução na operação relacionada à comparação não modifica nenhum registrador; Os resultados da comparação serão armazenados no flag .

instrução cmpe cmpe ri A definirá o sinalizador como 1 se [ri] = [A] e, caso contrário, definirá como 0
instrução cmpa cmpa ri A definirá o sinalizador como 1 se [ri]_u > [A]_u e, caso contrário, definirá como 0
instrução cmpae cmpae ri A definirá o sinalizador como 1 se [ri]_u ≥ [A]_u , caso contrário, definirá como 0
instrução cmpg cmpg ri A definirá o sinalizador como 1 se [ri]_s > [A]_s e, caso contrário, definirá como 0
instrução cmpge cmpge ri A definirá o sinalizador como 1 se [ri]_S ≥ [A]_S , caso contrário, definirá como 0

Operação relacionada ao movimento

A instrução mov mov ri A armazenará [A] no registrador ri.
instrução cmov cmov ri A armazenará [A] no registrador ri se flag = 1 e, caso contrário, o valor do registrador ri não mudará.

Relacionado ao salto

Essas instruções de salto e salto condicional não modificarão o registrador e o flag , mas modificarão o pc .

instrução de salto jmp A armazenará [A] em pc.
Instrução cjmp cjmp A armazenará [A] em pc quando flag = 1 e, caso contrário, incrementará pc em 1
Instrução cnjmp cnjmp A armazenará [A] em pc quando flag = 0 e, caso contrário, incrementará pc em 1

Operação relacionada à memória

Estas são operações simples de carregamento de memória e operações de armazenamento, onde o endereço da memória é determinado pelo número imediato ou pelo conteúdo do registrador.

Esses são os únicos métodos de endereçamento no TinyRAM. (TinyRAM não suporta o modo de endereçamento comum “base+offset”).

store.b store A ri armazenará o LSB de [ri] no endereço de [A] U-ésimo byte na memória.
A instrução load.b load ri A armazenará o conteúdo do [A] U-ésimo endereço de byte na memória no registrador ri (preenchendo com 0 nos bytes frontais).
store.w store.w A ri irá armazenar [ri] na posição da palavra alinhada com o [A]w-ésimo byte na memória.
A instrução load.w load.w ri A armazenou a palavra em sua memória alinhada com o byte [A]w no registrador ri.

Operação relacionada à entrada

Esta instrução é a única que pode acessar qualquer uma das fitas. A 0ª fita foi usada para entrada primária e a primeira fita para entrada auxiliar do usuário.

instrução de leitura read ri A armazenará a próxima palavra do bit W na fita [A] U no registrador ri. Para ser mais preciso, se a fita [A]u tiver alguma rest word, a próxima word será consumida e armazenada em ri, e set flag = 0; Caso contrário (se não houver palavras de entrada de descanso na fita [A]u), armazene 0^W em ri e defina flag = 1.

Como a TinyRAM tem apenas duas fitas de entrada, todas fitas exceto que os dois primeiros são considerados vazios.

Especificamente, se [A]u não for 0 ou 1, então armazenamos 0^W no ri e definimos flag =1.

Operação relacionada à saída

Esta instrução significa que o programa terminou sua computação e nenhuma outra operação é permitida.

instrução de resposta answer A fará com que a máquina de estado seja “paralisada” (sem aumento de pc) ou “parada” (interrompa a computação) e retorne para [A]u. A escolha entre estol ou parada não é definida. O valor de retorno 0 é usado para indicar aceitação.

Restrição do conjunto de instruções

TinyRAM usou a restrição R1CS para executar restrições de circuito, e a forma específica é a seguinte:

(Ai ∗ S) ∗ (Bi ∗ S) − Ci ∗ S = 0

Agora, se quisermos provar que conhecemos uma solução do cálculo original, precisaremos provar que nas matrizes A, B e C, todo vetor linha e vetor solução S do valor do produto interno está de acordo com as restrições R1CS A_i, B_i , C_i representa o vetor linha na matriz).

Cada restrição R1CS pode ser representada por linear_combination a, b ou c. As atribuições de todas as variáveis em um sistema R1CS podem ser divididas em duas partes: entrada primária e entrada auxiliar. O Primário é o que costumamos chamar de “declaração” e o auxiliar é “testemunha”.

Cada sistema de restrição R1CS contém várias restrições R1CS. O comprimento do vetor para cada restrição é fixo (tamanho da entrada principal + tamanho da entrada auxiliar + 1).

O TinyRAM usou muitos gadgtes personalizados na implementação do código libsnark para expressar as restrições de VM, bem como a execução do opcode e as restrições de memória. O código específico está na pasta gadgetslib1/ Gadgets /cpu_checkers/tinyram.

Restrição relacionada a bits

e fórmula de restrição:

 a * b = c

A restrição R1CS de e verifica o parâmetro 1 e o parâmetro 2 e o cálculo resulta na multiplicação bit a bit. As etapas de restrição são as seguintes:

A restrição do processo de computação e o código são os seguintes:

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

A restrição de codificação de resultado
Os resultados da computação não são todos restrições zero (consistentes com a definição da instrução e o processo é principalmente para preparar o sinalizador de restrição)

 /* 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} */

Sinalizar restrição

 /* 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"));

ou fórmula de restrição:

 (1 - a) * (1 - b) = (1 - c)

As etapas de restrição específicas são as seguintes:

A restrição do processo de computação e o código são os seguintes:

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

A restrição de codificação de resultado
Os resultados da computação não são todos restrições zero (consistentes com a definição da instrução, e este processo é principalmente uma preparação para o sinalizador de restrição)
Sinalizar restrição

 /* 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"));

fórmula de restrição xor :

 c = a ^ b <=> c = a + b - 2*a*b, (2*b)*a = a+b - c

As etapas de restrição específicas são as seguintes:

A restrição do processo de computação e o código são os seguintes:

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

A restrição de codificação de resultado
Os resultados da computação não são todos restrições zero (consistentes com a definição da instrução, e este processo é principalmente uma preparação para o sinalizador de restrição)
Sinalizar restrição

 /* 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"));

fórmula sem restrição:

 1 * （1 - b） = c

As etapas de restrição específicas são as seguintes:

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

A restrição de codificação de resultado
Os resultados da computação não são todos restrições zero (consistentes com a definição da instrução, e este processo é principalmente uma preparação para o sinalizador de restrição)
Sinalizar restrição

 /* 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"));

Restrição de operação relacionada a inteiro

adicionar: fórmula de restrição:
```
 1 * （a + b） = c
```
As etapas de restrição específicas são as seguintes:
1. A restrição do processo de computação, o código é o seguinte:
```
 this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { ONE }, { this->arg1val.packed, this->arg2val.packed }, { this->addition_result }), FMT(this->annotation_prefix, " addition_result"));
```
1. A restrição de resultado de decodificação e a restrição booleana
2. A restrição de resultado de codificação

sub: fórmula de restrição:

A subrestrição é um pouco mais complexa que a de add, com uma variável intermediária representando o resultado ab e 2^ w adicionados para garantir que o resultado seja computado como um inteiro positivo e um sinal. As etapas de restrição específicas são as seguintes:

 intermediate_result = 2^w + a -b

A restrição do processo de computação:

 /* 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"));

A restrição de resultado de decodificação e a restrição booleana
Restrição de bit de sinal

fórmula de restrição mull, umulh e smulh :
```
 c = a * b
```
Todas as restrições relacionadas a Mull envolvem as seguintes etapas:
1. Restrições de multiplicação computacional
2. Restrições de codificação de resultados de computação
3. Restrições de sinalização do resultado do cálculo
Fórmula de restrição udiv e umod :

 B * q + r = A r <= B

'B' é o divisor, 'q' é o quociente e 'r' é o resto. O resto não deve exceder o divisor. Os códigos de restrição específicos são os seguintes:

 /* 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();

Comparar operação

Cada instrução nas operações de comparação não modificará nenhum registrador; Os resultados da comparação são armazenados no flag . As instruções de comparação incluem cmpe , cmpa , cmpae . cmpg e cmpge , que podem ser divididos em dois tipos: comparação de números assinados e comparação de números não assinados, ambos os quais usam o purchase_gadget realizado de comparison_gadget em seu núcleo de processo de restrição.

Fórmula de restrição de comparação de número sem sinal:

 cmpe_flag = cmpae_flag * (1-cmpa_flag)

cmp e o código de restrição é o seguinte:

 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"));

Fórmula de restrição de comparação de números assinados:

A restrição de número sem sinal é mais complexa do que a restrição de comparação de número com sinal porque há mais processamento de restrição de bit de sinal.

A restrição de bit de sinal é a seguinte:

 /* 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"));

As etapas restantes são as mesmas da restrição de comparação de número com sinal.

Mover Restrição de Operação

fórmula de restrição mov :

A restrição mov é relativamente simples porque só precisa garantir que [A] seja armazenado no registrador ri. A operação mov não modificará flag , portanto, a restrição precisa garantir que o valor do sinalizador não seja alterado. O código de restrição é o seguinte:
```
 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"));
```

fórmula de restrição cmov :

 flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval

A condição de restrição do cmov é mais complexa do que a do mov, porque os comportamentos do mov estão relacionados à alteração do valor do sinalizador e o cmov não modificará o sinalizador, portanto, a restrição precisa garantir que o valor do sinalizador não mude e o código é o seguinte:

 /* 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"));

Restrição de operação de salto

Essas instruções de salto e salto condicional não modificarão os registradores e o flag , mas modificarão o pc .

jmp

O valor de pc é consistente com o resultado da execução da instrução na restrição de operação Jmp e o código de restrição específico é o seguinte:

 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 saltará de acordo com a condição do sinalizador quando sinalizador = 1 e, caso contrário, incrementará pc em 1.

A fórmula da restrição é a seguinte:

 flag1 * argval2 + (1-flag1) * (pc1 + 1) = cjmp_result flag1 * (argval2 - pc1 - 1) = cjmp_result - pc1 - 1

O código de restrição é o seguinte:

 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

O cnjmp saltará de acordo com as condições do sinalizador. Se flag = 0, o PC pula e caso contrário, incrementa pc em 1.

A fórmula da restrição é a seguinte:

 flag1 * (pc1 + 1) + (1-flag1) * argval2 = cnjmp_result flag1 * (pc1 + 1 - argval2) = cnjmp_result - argval2

O código de restrição é o seguinte:

 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"));

Restrição de operação de memória

Estas são operações simples de carregamento e armazenamento de memória, onde o endereço da memória é determinado pelo número imediato ou pelo conteúdo de um registrador.

Esses são os únicos métodos de endereçamento no TinyRAM. (TinyRAM não suporta o modo de endereçamento comum “base+offset”).

loja.b e loja.w

Para store.w, pegue todos os valores de arg1val , e para store.b opcodes, pegue apenas a parte necessária de arg1val (por exemplo, o último byte), e o código de restrição é o seguinte:

 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 e load.w

Para essas duas instruções, exigimos que o conteúdo carregado da memória seja armazenado em resultados_instrução e o código de restrição seja o seguinte:

 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"));

Restrição de operação de entrada

ler
A operação de leitura está relacionada à fita e as restrições específicas são as seguintes:

Quando a fita anterior terminar e houver conteúdo para ler, a próxima fita não poderá ser lida.
Quando a fita anterior terminar e houver conteúdo para ler, o flag é definido como 1
Se a instrução de read for executada agora, então o conteúdo lido é consistente com o conteúdo de entrada da fita
Leia o conteúdo de fora do type1, flag é definido como 1
Se o result for 0 significa que o flag é 0

Código de restrição:

 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"));

Restrições de operação de saída

Esta instrução indica que o programa concluiu sua computação e, portanto, nenhuma outra operação é permitida

responda

Quando o valor de saída do programa é aceito, has_accepted é definido como 1 e o valor de retorno do programa é aceito normalmente, o que significa que a instrução atual é answer e o valor arg2 é 0.

O código de restrição é o seguinte:

 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"));

Outro

Claro, além de algumas das restrições relacionadas à instrução mencionadas acima, o TinyRAM também possui algumas restrições na consistência do PC, codec de parâmetro, verificação de memória, etc. Essas restrições são combinadas por meio do sistema R1CS para formar um sistema de restrição TinyRAM completo. Portanto, esta é a causa raiz pela qual um grande número de restrições TinyRAM é gerado na forma de R1CS.

Aqui nos referimos a uma figura do tinyram review ppt , mostrando o consumo de tempo necessário para uma transferência ERC20 gerar uma prova via TinyRAM.

Pode-se concluir do exemplo acima: não é possível verificar todas as operações EVM com vnTinyRam + zk-SNARks e é adequado apenas para verificação computacional de um pequeno número de instruções. O vnTinyram pode ser usado para verificar opcode para tipos de computação parcial de EVM.