¿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

• y : la instrucción and ri rj A almacenarán los bits y resultados de [rj] y [A] en el registro ri. Además, si el resultado es 0^{W} , establezca el flag en 1 y, de lo contrario, configúrelo en 0.

  
  

• o instrucción or ri rj A almacenará los bits y resultados de [rj] y [A] en el registro ri. Además, si el resultado es 0^{W} , establezca el flag en 1 y, de lo contrario, configúrelo en 0.

  
  

• La instrucción xor xor ri rj A almacenará los bits y resultados de [rj] y [A] en el registro ri. Además, si el resultado es 0^{W} , establezca el flag en 1 y, de lo contrario, configúrelo en 0.

  
  

• not instrucción not ri A almacenará los bits y resultados de [rj] y [A] en el registro ri. Además, si el resultado es 0^{W} , establezca el flag en 1 y, de lo contrario, configúrelo en 0.

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 flag en 1 y, de lo contrario, configúrelo en 0.

En la siguiente parte, U_{W} representa una serie de enteros {0*,…,* $2^{W} -1 $}; Estos enteros están formados por cadenas de bits W. S_{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.

• add: instrucción add ri rj A 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 G = [rj]_u + [A]_u . Además, la flag se establecerá en G_{W} . G_{W} es el bit más significativo (MSB) de G.

  
  

• sub: la instrucción sub ri rj A 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 G = [rj]_u + 2^W − [A]_u . Además, la flag se establecerá en 1−G_{W} . G_{W} es el bit más significativo (MSB) de G.

  
  

• mull instrucción mull ri rj A 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 G=[rj]_u∗[A]_u . Además, la flag se establecerá en 1 si

  [rj]_u × [A] u ∉ U {W} , y de lo contrario establecerlo en 0.

  
  

• La instrucción umulh umulh ri rj A 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 G = [rj]_u ∗ [A]_u . Además, la flag se establecerá en 1 si [rj]_u × [A] u ∉ U {W} , y de lo contrario se establecerá en 0.

  
  

• La instrucción smulh smulh ri rj A almacenará la cadena de bits W a_{W−1}⋯a_{0} en el ri. a_{W−1} es el bit de signo de [rj] u ∗ [A]u, a {W−2}⋯a{0} es el W - 1 MSB de [rj]_u ∗ [A]_u . Además, el flag se establecerá en 1 si [rj]_u × [A] u ∉ S {W } y, de lo contrario, se establecerá en 0.

  
  

La instrucción udiv udiv ri rj A almacenará la cadena de bits W a_{W−1}⋯a_{0} en el ri.

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

Si [A] u∣ ≠ 0, a {W−1}⋯a_{0} es la única codificación binaria del entero Q, lo que hace que para algunos enteros R ∈ {0,…,[A]_u − 1} , la fórmula [rj]_u = [A]_u × Q + R es factible. Además, solo cuando [A]_u=0 , el flag se establecerá en 1.

La instrucción umod umod ri rj A almacenará la cadena de bits W a_{W−1}⋯a_{0} en el ri.

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

Si [A] u∣ ≠ 0, a {W−1}⋯a_{0} es la única codificación binaria del entero R, cuyo rango de valores es

{0,…,[A]_u−1} , haciendo que la fórmula [rj]_u = [A]_u × Q+R funcione para algunos valores de Q. Además, solo cuando [A]_u = 0 , el flag se establecerá en 1.

Operación relacionada con turnos

• La instrucción shl shl ri rj A 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].

  
  

• La instrucción shr shr ri rj A 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].

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 cmpe cmpe ri A establecerá el indicador en 1 si [ri] = [A], y de lo contrario lo establecerá en 0

  
  

• instrucción cmpa cmpa ri A establecerá el indicador en 1 si [ri]_u > [A]_u , y de lo contrario lo establecerá en 0

  
  

• cmpae instrucción cmpae ri A establecerá el indicador en 1 si [ri]_u ≥ [A]_u , y de lo contrario lo establecerá en 0

  
  

• instrucción cmpg cmpg ri A establecerá el indicador en 1 si [ri]_s > [A]_s , y de lo contrario lo establecerá en 0

  
  

• La instrucción cmpge cmpge ri A establecerá el indicador en 1 si [ri]_S ≥ [A]_S , y de lo contrario lo establecerá en 0

Operación relacionada con el movimiento

• La instrucción mov mov ri A almacenará [A] en el registro ri.

  
  

• instrucción cmov cmov ri A almacenará [A] en el registro ri si flag = 1 y, de lo contrario, el valor del registro ri no cambiará.

relacionado con el salto

Estas instrucciones de salto y salto condicional no modificarán el registro y la flag , pero modificarán el pc .

• La instrucción de salto jmp A almacenará [A] en pc.

  
  

• cjmp instrucción cjmp A almacenará [A] en pc cuando flag = 1, y de lo contrario incrementa pc en 1

  
  

• La instrucción cnjmp cnjmp A almacenará [A] en pc cuando flag = 0, y de lo contrario incrementa pc en 1

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 store.b store A ri almacenará el LSB de [ri] en la dirección de byte U-ésimo [A] en la memoria.

  
  

• La instrucción load.b load ri A 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).

  
  

• Instrucción store.w store.w A ri almacenará [ri] en la posición de palabra alineada con el byte [A]w-ésimo en la memoria.

  
  

• instrucción load.w load.w ri A ha almacenado la palabra en su memoria alineada con el byte [A]w en el registro ri.

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 lectura read ri A 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á flag = 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 flag = 1.

Dado que TinyRAM solo tiene dos cintas de entrada, todas cintas excepto que se supone que los dos primeros están vacíos.

Específicamente, si [A]u no es 0 o 1, entonces almacenamos 0^W en el ri y establecemos la flag =1.

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

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 S del valor del producto interno está de acuerdo con las restricciones R1CS A_i, B_i , C_i representa el vector fila en la matriz).

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

• y fórmula de restricción:

  
  

   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:

  
  

  1. La restricción del proceso de cálculo y el código son los siguientes:

     
     

      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. La restricción de codificación de resultados

     
     

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

  
  

  4. Restricción de bandera

     
     

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

  
  

• o fórmula de restricción:

  
  

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

  
  

  Los pasos de restricción específicos son los siguientes:

  
  

  1. La restricción del proceso de cálculo y el código son los siguientes:

     
     

   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. La restricción de codificación de resultados

     
     

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

     
     

  4. Restricción de bandera

     
     

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

  
  

  1. La restricción del proceso de cálculo y el código son los siguientes:

     
     

   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. La restricción de codificación de resultados

     
     

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

     
     

  4. Restricción de bandera

     
     

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

  
  

• no fórmula de restricción:

  
  

   1 * （1 - b） = c

  
  

  Los pasos de restricción específicos son los siguientes:

  
  

  1. 
     

      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. La restricción de codificación de resultados

     
     

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

     
     

  4. Restricción de bandera

     
     

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

Restricción de operación relacionada con enteros

• añadir: fórmula de restricción:

  
  

   1 * （a + b） = c

  
  

  Los pasos de restricción específicos son los siguientes:

  
  

  1. La restricción del proceso de cálculo, el código es el siguiente:

     
     

   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. La restricción de resultado de decodificación y la restricción booleana

     
     

  3. La restricción del resultado de la codificación

     
     

• sub: fórmula de restricción:

  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

  
  

  1. La restricción del proceso de cálculo:

      /* 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. La restricción de resultado de decodificación y la restricción booleana

     
     

  3. 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:

  
  

  1. Restricciones de calcular la multiplicación

     
     

  2. Restricciones de la codificación de resultados informáticos

     
     

  3. Marcar las restricciones del resultado del cálculo

  
  

• fórmula de restricción udiv y umod :

  
  

 B * q + r = A r <= B

'B' es el divisor, 'q' es el cociente y 'r' es el resto. El resto no debe exceder al divisor. Los códigos de restricción específicos son los siguientes:

 /* 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 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 flag . Las instrucciones de comparación incluyen cmpe , cmpa , cmpae . cmpg y cmpge , 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 comparison_gadget realizado de libsnark en su núcleo de proceso de restricción.

• 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<FieldT>( {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<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"));

  
  

  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 flag , 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:

  
  

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

Restricción de operación de salto

Estas instrucciones de salto y salto condicional no modificarán los registros y la flag , pero modificarán 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<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 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<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

  
  

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

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

• tienda.b y 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<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"));

  
  

• carga.b y 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<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"));

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:

1. Cuando se termina la cinta anterior y hay contenido para leer, no se permite leer la cinta siguiente.

   
   

2. Cuando finaliza la cinta anterior y hay contenido para leer, la flag se establece en 1

   
   

3. Si la instrucción de read se ejecuta ahora, entonces el contenido leído es consistente con el contenido de entrada de la cinta.

   
   

4. Leer contenido desde fuera del tipo 1, el flag se establece en 1

   
   

5. Si el result es 0 significa que la flag es 0

Código de restricción:

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

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 answer y el valor arg2 es 0.

El código de restricción es el siguiente:

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

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 tinyram review ppt , que muestra el consumo de tiempo requerido para que una transferencia ERC20 genere una prueba a través de TinyRAM.

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.