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 : a instrução armazenará os bits e resultados de [rj] e [A] no registrador ri. Da mesma forma, se o resultado for , defina o como 1 e, caso contrário, defina-o como 0. e and ri rj A 0^{W} flag instrução armazenará os bits e resultados de [rj] e [A] no registrador ri. Da mesma forma, se o resultado for , defina o como 1 e, caso contrário, defina-o como 0. ou or ri rj A 0^{W} flag A instrução armazenará os bits e resultados de [rj] e [A] no registrador ri. Da mesma forma, se o resultado for , defina o como 1 e, caso contrário, defina-o como 0. xor xor ri rj A 0^{W} flag A instrução armazenará os bits e resultados de [rj] e [A] no registrador ri. Da mesma forma, se o resultado for , defina o como 1 e, caso contrário, defina-o como 0. not not ri A 0^{W} flag 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 como 1 e, caso contrário, defina-o como 0. flag Na parte seguinte, representa uma série de inteiros {0*,…,* $2^{W} -1 $}; Esses inteiros são compostos de strings de W-bit. 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. U_{W} S_{W} a instrução 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 . Além disso, o será definido como . é o bit mais significativo (MSB) de G. add: add ri rj A G = [rj]_u + [A]_u flag G_{W} G_{W} instrução 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 . Além disso, o será definido como . é o bit mais significativo (MSB) de G. sub: a sub ri rj A G = [rj]_u + 2^W − [A]_u flag 1−G_{W} G_{W} instrução 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 . Além disso, o será definido como 1 se mull mull ri rj A G=[rj]_u∗[A]_u flag e, caso contrário, defina-o como 0. [rj]_u × [A] {W} u ∉ U instrução 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 . Além disso, o será definido como 1 se , caso contrário, será definido como 0. umulh umulh ri rj A G = [rj]_u ∗ [A]_u flag [rj]_u × [A] {W} u ∉ U A instrução armazenará a string de W-bit a_{W−1}⋯a_{0} no ri. a_{W−1} é o bit de sinal de é o W - 1 MSB de . Além disso, o será definido como 1 se } , caso contrário, será definido como 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 armazenará a string de W-bit a_{W−1}⋯a_{0} no ri. Instrução udiv udiv ri rj A Se . [A] {W−1}⋯a_{0} = 0^W u = 0, a Se é a única codificação binária do inteiro Q, fazendo com que para alguns inteiros , a fórmula é viável. Além disso, somente quando , o será definido como 1. [A] {W−1}⋯a_{0} u∣ ≠ 0, a R ∈ {0,…,[A]_u − 1} [rj]_u = [A]_u × Q + R [A]_u=0 flag instrução armazenará a string de W-bit a_{W−1}⋯a_{0} no ri. umod umod ri rj A Se . [A] {W−1}⋯a_{0} = 0^W u = 0, a Se cujo intervalo de valores é [A] {W−1}⋯a_{0} u∣ ≠ 0, a é a única codificação binária do inteiro R, , tornando a fórmula wokável para alguns valores Q. Além disso, somente quando , o será definido como 1. {0,…,[A]_u−1} [rj]_u = [A]_u × Q+R [A]_u = 0 flag Operação relacionada a turno A instrução 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]. shl shl ri rj A A instrução 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]. shr shr ri rj A 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 definirá o sinalizador como 1 se [ri] = [A] e, caso contrário, definirá como 0 cmpe cmpe ri A instrução definirá o sinalizador como 1 se e, caso contrário, definirá como 0 cmpa cmpa ri A [ri]_u > [A]_u instrução definirá o sinalizador como 1 se , caso contrário, definirá como 0 cmpae cmpae ri A [ri]_u ≥ [A]_u instrução definirá o sinalizador como 1 se e, caso contrário, definirá como 0 cmpg cmpg ri A [ri]_s > [A]_s instrução definirá o sinalizador como 1 se , caso contrário, definirá como 0 cmpge cmpge ri A [ri]_S ≥ [A]_S Operação relacionada ao movimento A instrução armazenará [A] no registrador ri. mov mov ri A instrução armazenará [A] no registrador ri se flag = 1 e, caso contrário, o valor do registrador ri não mudará. cmov cmov ri A Relacionado ao salto Essas instruções de salto e salto condicional não modificarão o registrador e o , mas modificarão o . flag pc instrução de armazenará [A] em pc. salto jmp A Instrução armazenará [A] em pc quando = 1 e, caso contrário, incrementará pc em 1 cjmp cjmp A flag Instrução armazenará [A] em pc quando = 0 e, caso contrário, incrementará pc em 1 cnjmp cnjmp A flag 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”). armazenará o LSB de [ri] no endereço de [A] U-ésimo byte na memória. store.b store A ri A instrução armazenará o conteúdo do [A] U-ésimo endereço de byte na memória no registrador ri (preenchendo com 0 nos bytes frontais). load.b load ri A irá armazenar [ri] na posição da palavra alinhada com o [A]w-ésimo byte na memória. store.w store.w A ri A instrução armazenou a palavra em sua memória alinhada com o byte [A]w no registrador ri. load.w load.w ri A 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 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 = 0; Caso contrário (se não houver palavras de entrada de descanso na fita [A]u), armazene 0^W em ri e defina = 1. leitura read ri A flag flag Como a TinyRAM tem apenas duas fitas de entrada, todas exceto que os dois primeiros são considerados vazios. fitas Especificamente, se [A]u não for 0 ou 1, então armazenamos 0^W no ri e definimos =1. flag 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 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. resposta answer A 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 do valor do produto interno está de acordo com as restrições R1CS representa o vetor linha na matriz). S A_i, B_i , C_i 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 fórmula de restrição: e 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 ( { 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 ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); fórmula de restrição: ou (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 ( { 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 ( { 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 ( { 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 ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); fórmula restrição: sem 1 * （1 - b） = c As etapas de restrição específicas são as seguintes: 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)); 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 ( { 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 fórmula de restrição: adicionar: 1 * （a + b） = c As etapas de restrição específicas são as seguintes: A restrição do processo de computação, o código é o seguinte: this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { this->arg1val.packed, this->arg2val.packed }, { this->addition_result }), FMT(this->annotation_prefix, " addition_result")); A restrição de resultado de decodificação e a restrição booleana A restrição de resultado de codificação fórmula de restrição: sub: 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 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")); 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: Restrições de multiplicação computacional Restrições de codificação de resultados de computação Restrições de sinalização do resultado do cálculo Fórmula de restrição : udiv e 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(); 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 . As instruções de comparação incluem , , . e , 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 em seu núcleo de processo de restrição. flag cmpe cmpa cmpae cmpg cmpge comparison_gadget 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 ( {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 ( {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")); 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á , portanto, a restrição precisa garantir que o valor do sinalizador não seja alterado. O código de restrição é o seguinte: 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")); 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 ( {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")); Restrição de operação de salto Essas instruções de salto e salto condicional não modificarão os registradores e o , mas modificarão o . flag 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 ( { 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 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 ( 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 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 ( 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")); 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”). e loja.b 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 (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")); e load.b 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 (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")); 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 é definido como 1 flag Se a instrução de for executada agora, então o conteúdo lido é consistente com o conteúdo de entrada da fita read Leia o conteúdo de fora do type1, é definido como 1 flag Se o for 0 significa que o é 0 result flag Código de restrição: 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")); 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 é e o valor arg2 é 0. answer O código de restrição é o seguinte: 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")); 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 , mostrando o consumo de tempo necessário para uma transferência ERC20 gerar uma prova via TinyRAM. tinyram review ppt 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.