¿Qué es un conjunto de instrucciones de TinyRAM?

Introducción TinyRAM es una computadora con conjunto de instrucciones reducido (RISC) simple con memoria de acceso aleatorio direccionable a nivel de byte y cintas de entrada. Hay dos variantes de TinyRAM: una sigue la arquitectura Harvard (hv) y la otra sigue la arquitectura von Neumann (vn) (en este artículo, nos centramos principalmente en la arquitectura von Neumann). El proyecto Succinct Computational Integrity and Privacy Research (SCIPR) construye mecanismos para probar la ejecución correcta de los programas TinyRAM, y TinyRAM está diseñado para ser eficiente en este entorno. Logra un equilibrio entre dos requisitos opuestos: "expresibilidad suficiente" y "pequeño conjunto de instrucciones": Expresibilidad suficiente para admitir código ensamblador corto y eficiente cuando se compila a partir de lenguajes de programación de alto nivel, Pequeño conjunto de instrucciones para admitir una verificación simple a través de circuitos aritméticos y una verificación eficiente utilizando los algoritmos y mecanismos criptográficos de SCIPR. En este artículo, complementaremos el artículo anterior en lugar de una introducción repetitiva de TinyRAM, y luego nos centraremos en la introducción de instrucciones y restricciones de circuitos. Para obtener una introducción básica a TinyRAM, consulte nuestro artículo anterior: tinyram简介-中文 Revisión de TinyRAM-Inglés Conjunto de instrucciones TinyRAM TinyRAM admite 29 instrucciones, cada una especificada por un código de operación y hasta 3 operandos. El operando puede ser el nombre de un registro (es decir, números enteros de 0 a K-1) o un valor inmediato (es decir, cadenas de bits W). A menos que se especifique lo contrario, cada instrucción no modifica el indicador por separado y aumenta pc en i (i % 2^W) de forma predeterminada, i=2W/8 para vnTinyRAM. En general, el primer operando es el registro de destino para el cálculo de instrucciones y los otros operandos especifican los parámetros requeridos por las instrucciones. Finalmente, todas las instrucciones toman un ciclo de la máquina para ejecutarse. Operación relacionada con bits : la instrucción almacenarán los bits y resultados de [rj] y [A] en el registro ri. Además, si el resultado es , establezca el en 1 y, de lo contrario, configúrelo en 0. y and ri rj A 0^{W} flag instrucción almacenará los bits y resultados de [rj] y [A] en el registro ri. Además, si el resultado es , establezca el en 1 y, de lo contrario, configúrelo en 0. o or ri rj A 0^{W} flag La instrucción almacenará los bits y resultados de [rj] y [A] en el registro ri. Además, si el resultado es , establezca el en 1 y, de lo contrario, configúrelo en 0. xor xor ri rj A 0^{W} flag instrucción almacenará los bits y resultados de [rj] y [A] en el registro ri. Además, si el resultado es , establezca el en 1 y, de lo contrario, configúrelo en 0. not not ri A 0^{W} flag Operación relacionada con enteros Estas son diversas operaciones relacionadas con enteros con y sin signo. En cada configuración, si se produce un desbordamiento aritmético o un error (como dividir por cero), establezca el en 1 y, de lo contrario, configúrelo en 0. flag En la siguiente parte, representa una serie de enteros {0*,…,* $2^{W} -1 $}; Estos enteros están formados por cadenas de bits W. representa una serie de números enteros {−2^(W−1),… 0, 1, $2 ^ $} {} W - 1-1. Estos enteros también se componen de cadenas de bits W. U_{W} S_{W} instrucción almacenará la cadena de bits W a_{W−1}⋯a_{0} en el ri. a_{W−1}⋯a_{0} es el bit menos significativo W (LSB) de . Además, la se establecerá en . es el bit más significativo (MSB) de G. add: add ri rj A G = [rj]_u + [A]_u flag G_{W} G_{W} la instrucción almacenará la cadena de bits W a_{W−1}⋯a_{0} en el ri. a_{W−1}⋯a_{0} es el bit menos significativo W (LSB) de . Además, la se establecerá en . es el bit más significativo (MSB) de G. sub: sub ri rj A G = [rj]_u + 2^W − [A]_u flag 1−G_{W} G_{W} instrucción almacenará la cadena de bits W a_{W−1}⋯a_{0} en el ri. a_{W−1}⋯a_{0} es el bit menos significativo W (LSB) de . Además, la se establecerá en 1 si mull mull ri rj A G=[rj]_u∗[A]_u flag , y de lo contrario establecerlo en 0. [rj]_u × [A] {W} u ∉ U La instrucción almacenará la cadena de bits W a_{W−1}⋯a_{0} en el ri. a_{W−1}⋯a_{0} es el bit W más significativo (MSB) de . Además, la se establecerá en 1 si , y de lo contrario se establecerá en 0. umulh umulh ri rj A G = [rj]_u ∗ [A]_u flag [rj]_u × [A] {W} u ∉ U La instrucción almacenará la cadena de bits W a_{W−1}⋯a_{0} en el ri. a_{W−1} es el bit de signo de es el W - 1 MSB de . Además, el se establecerá en 1 si } y, de lo contrario, se establecerá en 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 udiv almacenará la cadena de bits W a_{W−1}⋯a_{0} en el ri. La instrucción udiv ri rj A Si . [A] {W−1}⋯a_{0} = 0^W u = 0, a Si es la única codificación binaria del entero Q, lo que hace que para algunos enteros , la fórmula es factible. Además, solo cuando , el se establecerá en 1. [A] {W−1}⋯a_{0} u∣ ≠ 0, a R ∈ {0,…,[A]_u − 1} [rj]_u = [A]_u × Q + R [A]_u=0 flag La instrucción almacenará la cadena de bits W a_{W−1}⋯a_{0} en el ri. umod umod ri rj A Si . [A] {W−1}⋯a_{0} = 0^W u = 0, a Si cuyo rango de valores es [A] {W−1}⋯a_{0} u∣ ≠ 0, a es la única codificación binaria del entero R, , haciendo que la fórmula funcione para algunos valores de Q. Además, solo cuando , el se establecerá en 1. {0,…,[A]_u−1} [rj]_u = [A]_u × Q+R [A]_u = 0 flag Operación relacionada con turnos La instrucción almacenará la cadena de bits W obtenida por [rj] desplazamiento a la izquierda para [A] u bit en el registro ri. Las posiciones en blanco después del cambio se llenan con 0. Además, el indicador se establece en el MSB de [rj]. shl shl ri rj A La instrucción almacenará la cadena de bits W obtenida al desplazar [rj] a la derecha para [A] u bit en el registro ri. Las posiciones en blanco después del cambio se llenan con 0. Además, la bandera se establece en el LSB de [rj]. shr shr ri rj A Operación relacionada con la comparación Cada instrucción en la operación relacionada con la comparación no modifica ningún registro; Los resultados de la comparación se almacenarán en . flag instrucción establecerá el indicador en 1 si [ri] = [A], y de lo contrario lo establecerá en 0 cmpe cmpe ri A instrucción establecerá el indicador en 1 si , y de lo contrario lo establecerá en 0 cmpa cmpa ri A [ri]_u > [A]_u instrucción establecerá el indicador en 1 si , y de lo contrario lo establecerá en 0 cmpae cmpae ri A [ri]_u ≥ [A]_u instrucción establecerá el indicador en 1 si , y de lo contrario lo establecerá en 0 cmpg cmpg ri A [ri]_s > [A]_s La instrucción establecerá el indicador en 1 si , y de lo contrario lo establecerá en 0 cmpge cmpge ri A [ri]_S ≥ [A]_S Operación relacionada con el movimiento La instrucción almacenará [A] en el registro ri. mov mov ri A instrucción almacenará [A] en el registro ri si flag = 1 y, de lo contrario, el valor del registro ri no cambiará. cmov cmov ri A relacionado con el salto Estas instrucciones de salto y salto condicional no modificarán el registro y la , pero modificarán el . flag pc La instrucción de almacenará [A] en pc. salto jmp A instrucción almacenará [A] en pc cuando = 1, y de lo contrario incrementa pc en 1 cjmp cjmp A flag La instrucción almacenará [A] en pc cuando = 0, y de lo contrario incrementa pc en 1 cnjmp cnjmp A flag Operación relacionada con la memoria Estas son operaciones simples de carga de memoria y operaciones de almacenamiento, donde la dirección de la memoria está determinada por el número inmediato o el contenido del registro. Estos son los únicos métodos de direccionamiento en TinyRAM. (TinyRAM no es compatible con el modo de direccionamiento común "base+offset"). La instrucción almacenará el LSB de [ri] en la dirección de byte U-ésimo [A] en la memoria. store.b store A ri La instrucción almacenará el contenido de la dirección del byte U-ésimo [A] en la memoria en el registro ri (rellenando con 0 en los bytes delanteros). load.b load ri A Instrucción almacenará [ri] en la posición de palabra alineada con el byte [A]w-ésimo en la memoria. store.w store.w A ri instrucción ha almacenado la palabra en su memoria alineada con el byte [A]w en el registro ri. load.w load.w ri A Operación relacionada con la entrada Esta instrucción es la única que puede acceder a cualquiera de las cintas. La cinta 0 se usó para la entrada principal y la primera cinta para la entrada auxiliar del usuario. La instrucción de almacenará la siguiente palabra de bit W en la cinta [A] U en el registro ri. Para ser más precisos, si la cinta [A]u tiene alguna palabra en reposo, la siguiente palabra se consumirá y almacenará en ri, y establecerá = 0; De lo contrario (si no hay palabras de entrada en reposo en la cinta [A]u), almacene 0^W en ri y establezca la = 1. lectura read ri A flag flag Dado que TinyRAM solo tiene dos cintas de entrada, todas excepto que se supone que los dos primeros están vacíos. cintas Específicamente, si [A]u no es 0 o 1, entonces almacenamos 0^W en el ri y establecemos la =1. flag Operación relacionada con la salida Esta instrucción significa que el programa ha terminado su cálculo y no se permiten otras operaciones. la instrucción de hará que la máquina de estado se "detenga" (sin aumento de pc) o se "detenga" (detenga el cálculo) y regrese a [A]u. No se define la elección entre parar o parar. El valor de retorno 0 se utiliza para indicar aceptación. respuesta answer A Restricción del conjunto de instrucciones TinyRAM ha utilizado la restricción R1CS para realizar restricciones de circuito, y la forma específica es la siguiente: (Ai ∗ S) ∗ (Bi ∗ S) − Ci ∗ S = 0 Ahora, si queremos probar que conocemos una solución del cálculo original, necesitaremos probar que en las matrices A, B y C, cada vector fila y vector solución del valor del producto interno está de acuerdo con las restricciones R1CS representa el vector fila en la matriz). S A_i, B_i , C_i Cada restricción R1CS se puede representar mediante una combinación_lineal a, b o c. Las asignaciones de todas las variables en un sistema R1CS se pueden dividir en dos partes: entrada principal y entrada auxiliar. El Primario es lo que a menudo llamamos una "declaración" y el auxiliar es "testigo". Cada sistema de restricciones R1CS contiene múltiples restricciones R1CS. La longitud del vector para cada restricción es fija (tamaño de entrada principal + tamaño de entrada auxiliar + 1). TinyRAM ha utilizado una gran cantidad de dispositivos personalizados en la implementación del código libsnark para expresar las restricciones de VM, así como la ejecución del código de operación y las restricciones de memoria. El código específico está en la carpeta gadgetslib1/ Gadgets /cpu_checkers/tinyram. Restricción relacionada con bits fórmula de restricción: y a * b = c La restricción R1CS de y verifica el parámetro 1 y el parámetro 2 y el cálculo da como resultado una multiplicación bit por bit. Los pasos de restricción son los siguientes: La restricción del proceso de cálculo y el código son los siguientes: 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)); La restricción de codificación de resultados Los resultados del cálculo no son todos restricciones cero (de acuerdo con la definición de la instrucción, y el proceso consiste principalmente en preparar el indicador de restricción) /* 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} */ Restricción de bandera /* 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 restricción: o (1 - a) * (1 - b) = (1 - c) Los pasos de restricción específicos son los siguientes: La restricción del proceso de cálculo y el código son los siguientes: 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)); La restricción de codificación de resultados Los resultados del cálculo no son todos restricciones cero (de acuerdo con la definición de la instrucción, y este proceso es principalmente una preparación para el indicador de restricción) Restricción de bandera /* 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 restricción : xor c = a ^ b c = a + b - 2*a*b, (2*b)*a = a+b - c Los pasos de restricción específicos son los siguientes: La restricción del proceso de cálculo y el código son los siguientes: 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)); La restricción de codificación de resultados Los resultados del cálculo no son todos restricciones cero (de acuerdo con la definición de la instrucción, y este proceso es principalmente una preparación para el indicador de restricción) Restricción de bandera /* 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 restricción: no 1 * （1 - b） = c Los pasos de restricción específicos son los siguientes: 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)); La restricción de codificación de resultados Los resultados del cálculo no son todos restricciones cero (de acuerdo con la definición de la instrucción, y este proceso es principalmente una preparación para el indicador de restricción) Restricción de bandera /* 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")); Restricción de operación relacionada con enteros fórmula de restricción: añadir: 1 * （a + b） = c Los pasos de restricción específicos son los siguientes: La restricción del proceso de cálculo, el código es el siguiente: this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { this->arg1val.packed, this->arg2val.packed }, { this->addition_result }), FMT(this->annotation_prefix, " addition_result")); La restricción de resultado de decodificación y la restricción booleana La restricción del resultado de la codificación fórmula de restricción: sub: La restricción sub es un poco más compleja que la de suma, con una variable intermedia que representa el resultado ab y 2^ w agregada para garantizar que el resultado se calcule como un entero positivo y un signo. Los pasos de restricción específicos son los siguientes: intermediate_result = 2^w + a -b La restricción del proceso de cálculo: /* 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")); La restricción de resultado de decodificación y la restricción booleana Restricción de bit de signo fórmula de restricción : mull, umulh y smulh c = a * b Todas las restricciones relacionadas con mull implican los siguientes pasos: Restricciones de calcular la multiplicación Restricciones de la codificación de resultados informáticos Marcar las restricciones del resultado del cálculo fórmula de restricción : udiv y 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 operación Cada instrucción en las operaciones de comparación no modificará ningún registro; Los resultados de la comparación se almacenan en . Las instrucciones de comparación incluyen , , . y , que se pueden dividir en dos tipos: comparación de números con signo y comparación de números sin signo, los cuales utilizan el gadget de realizado de libsnark en su núcleo de proceso de restricción. flag cmpe cmpa cmpae cmpg cmpge comparison_gadget Fórmula de restricción de comparación de números sin signo: cmpe_flag = cmpae_flag * (1-cmpa_flag) cmp y el código de restricción es el siguiente: 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 restricción de comparación de números con signo: La restricción de número sin signo es más compleja que la restricción de comparación de número con signo porque hay más procesamiento de restricción de bit de signo. La restricción de bit de signo es la siguiente: /* 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")); Los demás pasos son los mismos que los de la restricción de comparación de números con signo. Restricción de operación de movimiento fórmula de restricción : mov La restricción mov es relativamente simple porque solo necesita garantizar que [A] se almacene en el registro ri. La operación mov no modificará la , por lo que la restricción debe garantizar que el valor de la bandera no cambie. El código de restricción es el siguiente: 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 restricción : cmov flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval La condición de restricción de cmov es más compleja que la de mov, porque los comportamientos de mov están relacionados con el cambio del valor de la bandera, y cmov no modificará la bandera, por lo que la restricción debe garantizar que el valor de la bandera no cambie, y El código es el siguiente: /* 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")); Restricción de operación de salto Estas instrucciones de salto y salto condicional no modificarán los registros y la , pero modificarán . flag pc jmp El valor pc es consistente con el resultado de ejecución de la instrucción en la restricción de operación Jmp, y el código de restricción específico es el siguiente: 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 acuerdo con la condición de la bandera cuando la bandera = 1 y, de lo contrario, incrementará pc en 1. La fórmula de restricción es la siguiente: flag1 * argval2 + (1-flag1) * (pc1 + 1) = cjmp_result flag1 * (argval2 - pc1 - 1) = cjmp_result - pc1 - 1 El código de restricción es el siguiente: 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 El cnjmp saltará según las condiciones de la bandera. Si flag = 0, el PC salta y, en caso contrario, incrementa pc en 1. La fórmula de restricción es la siguiente: flag1 * (pc1 + 1) + (1-flag1) * argval2 = cnjmp_result flag1 * (pc1 + 1 - argval2) = cnjmp_result - argval2 El código de restricción es el siguiente: 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")); Restricción de operación de memoria Estas son operaciones simples de carga y almacenamiento de memoria, donde la dirección de la memoria está determinada por el número inmediato o el contenido de un registro. Estos son los únicos métodos de direccionamiento en TinyRAM. (TinyRAM no es compatible con el modo de direccionamiento común "base+offset"). y tienda.b tienda.w Para store.w, tome todos los valores de arg1val y para los códigos de operación de store.b, solo tome la parte necesaria de arg1val (por ejemplo, el último byte), y el código de restricción es el siguiente: 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")); y carga.b carga.w Para estas dos instrucciones, requerimos que los contenidos cargados desde la memoria se almacenen en instrucción_resultados, y el código de restricción es el siguiente: 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")); Restricción de operación de entrada leer La operación de lectura está relacionada con la cinta y las restricciones específicas son las siguientes: Cuando se termina la cinta anterior y hay contenido para leer, no se permite leer la cinta siguiente. Cuando finaliza la cinta anterior y hay contenido para leer, la se establece en 1 flag Si la instrucción de se ejecuta ahora, entonces el contenido leído es consistente con el contenido de entrada de la cinta. read Leer contenido desde fuera del tipo 1, el se establece en 1 flag Si el es 0 significa que la es 0 result flag Código de restricción: 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")); Restricciones de la operación de salida Esta instrucción indica que el programa ha completado su cálculo y, por lo tanto, no se permiten más operaciones. responder Cuando se acepta el valor de salida del programa, has_accepted se establece en 1 y el valor de retorno del programa se acepta normalmente, lo que significa que la instrucción actual es y el valor arg2 es 0. answer El código de restricción es el siguiente: 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")); Otro Por supuesto, además de algunas de las restricciones relacionadas con las instrucciones mencionadas anteriormente, TinyRAM también tiene algunas restricciones sobre la consistencia de la PC, el códec de parámetros, la verificación de memoria, etc. Estas restricciones se combinan a través del sistema R1CS para formar un sistema completo de restricciones de TinyRAM. Por lo tanto, esta es la causa principal por la que se genera una gran cantidad de restricciones de TinyRAM en forma de R1CS. Aquí nos referimos a una figura de , que muestra el consumo de tiempo requerido para que una transferencia ERC20 genere una prueba a través de TinyRAM. tinyram review ppt Se puede concluir del ejemplo anterior: no es posible verificar todas las operaciones de EVM con vnTinyRam + zk-SNARks y solo es adecuado para la verificación computacional de una pequeña cantidad de instrucciones. El vnTinyram se puede usar para verificar el código de operación para tipos de cómputo parciales de EVM.