Explore Cairo: una arquitectura de CPU compatible con STARK completa, práctica y eficiente

Cairo es una arquitectura de CPU compatible con STARK completa y prácticamente eficiente de Turing. En este artículo, presentamos la arquitectura de CPU de Cairo en términos de estructura de instrucción y transición de estado, y brindamos algunos ejemplos de instrucción. Estructura de instrucciones La palabra soportada de forma nativa por Cairo CPU es un elemento de campo, donde el campo es un campo finito fijo de característica . P>2^63 Cada instrucción ocupará 1 o 2 palabras. Si un valor inmediato ([ap] = “12345678”) sigue a la instrucción, la instrucción ocupará 2 palabras y el valor se almacenará en la segunda palabra. La primera palabra de cada instrucción consta de los siguientes elementos: _dst[ bit0…15]: desplazamiento de la dirección de destino, valor representativo off -2^{15} + ∑_{i = 0}^{15} b_i . 2^i ∈ [-2^{15}, 2^{15}); [bit16…31]: compensación de dirección op0, valor representativo off_op0 -2^{15} + ∑_{i = 0}^{15} b_i . 2^i ∈ [-2^{15}, 2^{15}); [bit32…47]: compensación de dirección op1, valor representativo off_op1 -2^{15} + ∑_{i = 0}^{15} b_i . 2^i ∈ [-2^{15}, 2^{15}); [bit48]: registro base de desplazamiento de la dirección de destino, ap o fp; dst reg [bit49]: Registro base del desplazamiento de dirección op0, ap o fp; op0 reg [bit50…52]: dirección de op1, op1_src Caso: 000 op1=m(op0+off_op1) Caso: 001 op1=m(pc+off_op1) Caso: 010 op1=m(fp+off_op1) Caja: 100 op1=m(ap+off_op1) bit53…54]: lógica computacional res_logic Caso: 00 res = op1 Caso: 01 res = op0 + op1 Caso: 10 res = op0 ∗ op1 [bit55…57]: la lógica de actualización de pc pc_update Caso: 000 // común next_pc = pc + instrucción_tamaño Caso: 001 // salto absoluto siguiente_pc = res Caso: 010 // salto relativo next_pc = pc + res Caso: 100 // salto relativo condicional siguiente_pc = pc + op1 (o tamaño_instrucción si dst = 0) [bit58…59]: la lógica de actualización de ap ap_update Caso: 00 next_ap = ap (o ap+2 si opcode = 1) Caso: 01 next_ap = ap + res Caso: 10 next_ap = ap + 1 de operación [bit60…62]: tipos de código de operación código Caso: 000 // jmp Caso: 001 // llamar Caso: 010 // ret Caso: 100 // afirmar Comentario de transición de estado La función de transición de estado representa una unidad de transición de estado general (porque contiene la lógica de procesamiento de todos los tipos de instrucciones), y un cálculo generalmente se descompone en múltiples instrucciones ejecutadas continuamente. Por lo tanto, necesitamos: asegurar el contenido de la instrucción y la validez de los estados antes y después de que se ejecute la instrucción (p. ej., pasar una cierta verificación de rango y verificación de consistencia de estado) y asegurarse de que la instrucción ejecutada es válida. Comentario de lógica de transición Si el estado antes y después de la ejecución de la instrucción es consistente, la actualización del estado debe ejecutarse de acuerdo con la siguiente lógica: #Context: m(.). #Input state: (pc, ap, and fp). #Output state: (next_pc, next_ap, and next_fp). #Compute op0. If op0_reg == 0: // Judge the basic register of op0 according to the flag value, 0 is ap,1 is fp, and obtain the value of op0. op0 = m(ap + off_{op0}) else: op0 = m(fp + off_{op0}) #Compute op1 and instruction_size. switch op1_src: // Obtain the value of op1 case 0: instruction_size = 1 // op1 = m[[ap/fp + off_op0] +off_op1], with two-level imbedding at most. op1 = m(op0 + off_{op1}) case 1: instruction_size = 2 // There exist(s) immediate number(s). The instruction size is 2 words. op1 = m(pc + off_{op1})// #If off_{op1} = 1, we have op1 = immediate_value. // For example, [ap] = "12345678", op1 = "12345678" case 2: instruction_size = 1 // op1 = [fp + off_op1] op1 = m(fp + off_{op1}) case 4: instruction_size = 1 // op1 = [ap +off_op1] op1 = m(ap + off_{op1}) default: Undefined Behavior #Compute res. if pc_update == 4: // jnz if res_logic == 0 && opcode == 0 && ap_update != 1: // Assign && jump && advanced ap res = Unused // Under conditional jump, the values of res_logic, opcode and ap_update flags can only be as shown above.The res variable will not be used on this occasion. else: Undefined Behavior else if pc_update = 0, 1 or 2: switch res_logic: // The computational logic of res is: case 0: res = op1 case 1: res = op0 + op1 case 2: res = op0 * op1 default: Undefined Behavior else: Undefined Behavior # Compute dst. if dst_reg == 0: dst = m(ap + offdst) else: dst = m(fp + offdst) # Compute the new value of pc. switch pc_update: case 0: # The common case: [ap] = 1 next_pc = pc + instruction_size case 1: # Absolute jump: jmp abs 123 next_pc = res case 2: # Relative jump: jmp rel [ap - 1] next_pc = pc + res case 4: # Conditional relative jump (jnz): jmp rel [ap - 1] if [fp - 7] = 0 next_pc = if dst == 0: pc + instruction_size // If dst = 0, then pc conducts ordinary updates; otherwise, it is similar to Case 2. else: pc + op1 // Under this circumstance, res is Unused, so pc directly conducts + op1, instead of + res. default: Undefined Behavior # Compute new value of ap and fp based on the opcode. if opcode == 1: # "Call" instruction. assert op0 == pc + instruction_size assert dst == fp # Update fp. next_fp = ap + 2 // [ap] saves the current fp value, [ap + 1] saves the pc after the call instruction; when the ret instruction is executed, it is convenient to reset fp to [ap], and then continue to execute subsequent instructions. # Update ap. switch ap_update: case 0: next_ap = ap + 2 // [ap] saves the value of fp, and [ap+1] saves the instruction address after the call instruction; thus, ap increases by 2. default: Undefined Behavior else if opcode is one of 0, 2, 4: # Update ap. switch ap_update: case 0: next_ap = ap // [fp + 1] = 5 case 1: next_ap = ap + res // advanced ap [ap] += 123 case 2: next_ap = ap + 1 // normal [fp + 1] = [ap]; ap++ default: Undefined Behavior switch opcode: // Within the same function, the fp value remains unchanged. case 0: next_fp = fp case 2: # "ret" instruction. next_fp = dst // The ret instruction goes with the call instruction, and assert dst == fp. case 4: # "assert equal" instruction. assert res = dst next_fp = fp else: Undefined Behavior Verificación de instrucciones Como se muestra en la Figura 1, una instrucción consta de los siguientes elementos: structure instruction := (off_dst : bitvec 16) (off_op0 : bitvec 16) (off_op1 : bitvec 16) (flags : bitvec 15) Dónde: [bit0…15], [bit16…31], [bit32…47] están dentro del rango off_dst off_op0 off_op1 -2^{15} + ∑_{i = 0}^{15} b_i . 2^i ∈ [-2^{15}, 2^{15}) Pero en AIR, los convertimos en la siguiente forma: ˜apagado∗ = apagado∗ + 2^15 (Donde * representa uno de dst, op0 y op1) Así que el rango de valores de debería ser [0,2^16) ˜off∗ Por lo tanto, para la codificación de una instrucción, tenemos: En lugar de asignar 15 columnas virtuales con una longitud de NN a los indicadores de 15 bits de la instrucción, usamos una columna virtual. Nota: =∑_{j=i}^{14} 2j−i⋅fj ˜f_i Con una longitud de 16N, que cumple con los siguientes requisitos: ˜f_0 = ∑_{j=0}^{14} 2^{j-0}⋅f_j es un valor de 15 bits ˜f_15 = 0 ˜f_i −2˜f_{i+1} = ∑_{j=i}^{14} (2^{j−i}⋅f_j) − 2⋅∑_{j=i+1}^{14} (2^{j−i−1}⋅fj) =∑_{j=1}^{14}(2j−i⋅fj) − ∑{j=i+1}^{14}(2j−i⋅ fj)=fi Por lo tanto, la ecuación (1) se puede escribir como: （2） inst = ˜off_dst + 2^16⋅˜off_op0 + 2^32⋅˜off_op1 + 2^48⋅˜f0 ∈ [0,263) Debido a que la característica del campo finito, una instrucción solo puede corresponder a un elemento de campo válido. P > 2^63 Por lo tanto, para la instrucción en sí, se deben cumplir las siguientes restricciones: Instrucción： inst= ˜off_dst + 2^16⋅˜off_op0 + 2^32⋅˜off_op1 + 2^48⋅ f0 ˜ Bit： (˜f_i−2˜f_i +1)(˜f_i−2˜f_i+1 −1)=0 para todo i ∈ [0,15) El último valor es cero: ˜f_15=0 El columna virtual ∈ [0,2^16), entonces ∈ [2^−15, 2^15) desplazamiento está dentro del rango: ˜off∗ off∗ Ejemplos de instrucciones Afirmar igual La instrucción afirmar igualdad se puede expresar con la siguiente sintaxis: = Asegura que ambos lados de la fórmula sean iguales; de lo contrario, se rechazará la ejecución del programa. El lado izquierdo de la ecuación a menudo proviene de [ ] o [ ], y el lado derecho tiene algunas formas posibles (reg_0 y reg_1 pueden ser o , ∘ puede ser suma o multiplicación, e imm puede ser cualquier elemento de campo fijo): fp+off_dst ap+off_dst fp ap immm [reg1+offop1][reg1+offop1] [reg0+offop0]∘[reg1+offop1][reg0+offop0]∘[reg1+offop1] [reg0+offop0]∘imm[reg0+offop0]∘imm [[reg0+offop0+offop1][[reg0+offop0+offop1] división y la resta se pueden expresar como multiplicación y suma con diferentes órdenes de operandos, respectivamente. Nota 2: La Una instrucción de se puede considerar como una instrucción de asignación, en la que se conoce el valor de un lado y se desconoce el otro lado. afirmación Por ejemplo, [ap]=4[ap]=4 puede considerarse como una afirmación de que el valor de [ap] es 4, o como una asignación que establece [ap] en 4, según el contexto. La figura 4 muestra algunos ejemplos de instrucciones de "afirmación igual" y los valores de bandera para cada instrucción: instrucción [fp + 1] = 5: Interpretar afirmar instrucción => código de operación = 4 next_ap = ap => ap_update = 00 = 0 next_pc = pc + instrucción_tamaño => pc_update = 000 = 0 Para op0 y op1, no hay add o mul => res_logic(res) = 00 = 0 Existe un valor inmediato => op1_src(op1) = 001 = 1 La dirección de valor inmediato indica que las direcciones son adyacentes => off_op1 = 1 El lado izquierdo de la ecuación [fp + 1] => dst_reg(dst) = 1 El lado izquierdo de la ecuación [fp + 1] => off_dst = 1 op0_reg/ off_op0 => valor inicial (1/-1) //Debido a que estos indicadores no se usan en esta instrucción, se completa el valor predeterminado. Comentario de salto condicional e incondicional La instrucción permite cambiar el valor del contador de programa . jmp pc Cairo admite el salto relativo (su operando representa el desplazamiento del pcpc actual) y el salto absoluto, representado por las palabras clave y respectivamente. rel abs La instrucción puede ser condicional. Por ejemplo, cuando el valor de una unidad de memoria no es 0, se activará la instrucción . jmp jmp La sintaxis de la instrucción es la siguiente: #Unconditional jumps. jmp abs jmp rel #Conditional jumps. jmp rel if ! La figura 5 muestra algunos ejemplos de las instrucciones y los valores de bandera correspondientes de cada instrucción: jmp instrucción jmp rel [ap +1] + [fp - 7]: Interpretar instrucción jmp => código de operación = 0 next_ap = ap => ap_update = b00 = 0 next_pc = pc + res=> pc_update = b010 = 2 res = op0 + op1 => res_logic(res) = b01 = 1 op1: [fp - 7] => op1_src(op1) = b010 = 2 op1: [fp - 7] => off_op1 = -7 op0: [ap + 1] => op0_src(op0) = 0 op0: [ap + 1] => off_op0 = 1 dst_reg/ off_dst => valor inicial (1/-1) /// Debido a que estos indicadores no se usan en esta instrucción, se completa el valor predeterminado. y llamar retirar Las instrucciones y permiten la implementación de la pila de funciones. La instrucción de actualiza los registros del contador de programa ( ) y del puntero de trama ( ). call ret llamada pc fp La actualización del contador del programa es similar a la instrucción . El valor anterior de se escribe en [ ], para permitir que la instrucción restablezca el valor de al valor anterior a la llamada; De manera similar, el pcpc devuelto (la dirección de la instrucción después de la instrucción de llamada) se escribe en [ ], para permitir que la instrucción retroceda y continúe con la ejecución del código después de la instrucción de llamada. jmp fp ap ret fp ap+1 ret Como se escribieron dos unidades de memoria, avanzó en 2 y se establece en la nueva . ap fp ap La sintaxis de las instrucciones es la siguiente: call abs call rel ret La figura 6 muestra algunos ejemplos de instrucciones y y valores de bandera correspondientes a cada instrucción: call ret llamada de instrucción abs [fp + 4]: Interpretar instrucción de llamada => código de operación = 0 next_ap = ap => ap_update = b00 = 0 next_pc = res => actualización_pc = b001 = 1 res = op1 => res_logic(res) = b00 = 0 op1: [fp + 4] => op1_src(op1) = b010 = 2 op1: [fp + 4] => off_op1 = 4 op0_reg/ off_op0 => valor inicial (0/1) /// Debido a que estos indicadores no se usan en esta instrucción, se completa el valor predeterminado. dst_reg/ off_dst => valor inicial (0/0) /// Debido a que estos indicadores no se usan en esta instrucción, se completa el valor predeterminado. Avanzando ap La instrucción incrementa el valor de por el operando dado. ap += ap Comentario La Figura 7 muestra algunos ejemplos de las instrucciones de avance y los valores de bandera correspondientes de cada instrucción: ap instrucción ap += 123: Interpretar avanzando la instrucción ap => código de operación = 0 next_ap = ap + res => ap_update = b01 = 1 next_pc = pc + instrucción_tamaño => pc_update = b000 = 0 res = op1 => res_logic(res) = b00 = 0 op1 = 123 => op1_src(op1) = b001 = 1 op1 = 123 => off_op1 = 1 op0_reg/ off_op0 => valor inicial (1/-1) /// Debido a que estos indicadores no se usan en esta instrucción, se completa el valor predeterminado. dst_reg/ off_dst => valor inicial (1/-1) /// Debido a que estos indicadores no se usan en esta instrucción, se completa el valor predeterminado.