Explore Cairo: uma arquitetura de CPU compatível com STARK prática e eficiente

Cairo é uma arquitetura de CPU compatível com STARK praticamente eficiente e completa para Turing.

Neste artigo, apresentamos a arquitetura da CPU do Cairo em termos de estrutura de instrução e transição de estado e fornecemos alguns exemplos de instrução.

Estrutura de instruções

A palavra suportada nativamente pela CPU Cairo é um elemento de campo, onde o campo é algum campo finito fixo de característica P>2^63 .

Cada instrução ocupará 1 ou 2 palavras. Se um valor imediato（[ap] = “12345678”）seguir a instrução, a instrução ocupará 2 palavras e o valor será armazenado na segunda palavra. A primeira palavra de cada instrução consiste nos seguintes elementos:

• off _dst[ bit0…15]: deslocamento do endereço de destino, valor representativo

  -2^{15} + ∑_{i = 0}^{15} b_i . 2^i ∈ [-2^{15}, 2^{15});

  
  

• off_op0 [ bit16…31]: deslocamento de endereço op0, valor representativo

-2^{15} + ∑_{i = 0}^{15} b_i . 2^i ∈ [-2^{15}, 2^{15});

• off_op1 [bit32…47]: deslocamento do endereço op1, valor representativo

  -2^{15} + ∑_{i = 0}^{15} b_i . 2^i ∈ [-2^{15}, 2^{15});

  
  

• dst reg [ bit48]: Registro base do deslocamento do endereço de destino, ap ou fp;

  
  

• op0 reg [ bit49]: Registro base do deslocamento do endereço op0, ap ou fp;

  
  

• op1_src [ bit50…52]: endereço de op1,

  
  

  • Caso: 000
    op1=m(op0+off_op1)

    
    

  • Caso: 001

    op1=m(pc+off_op1)

    
    

  • Caso: 010
    op1=m(fp+off_op1)

    
    

  • Caso: 100

    op1=m(ap+off_op1)

    
    

• res_logic bit53…54]: lógica computacional

  
  

  • Caso: 00
    res = op1

    
    

  • Caso: 01
    res = op0 + op1

    
    

  • Caso: 10
    res = op0 ∗ op1

    
    

• pc_update [bit55…57]: a lógica de atualização do pc

  
  

  • Caso: 000 // comum
    next_pc = pc + tamanho_instrução

    
    

  • Caso: 001 // salto absoluto
    next_pc = res

    
    

  • Caso: 010 // salto relativo
    next_pc = pc + res

    
    

  • Caso: 100 // salto relativo condicional
    next_pc = pc + op1 (ou tamanho_da_instrução se dst = 0)

    
    

• ap_update [ bit58…59]: a lógica de atualização de ap

  
  

  • Caso: 00
    next_ap = ap (ou ap+2 se opcode = 1)

    
    

  • Caso: 01
    next_ap = ap + res

    
    

  • Caso: 10
    next_ap = ap + 1

    
    

• opcode [ bit60…62]: tipos de opcode

  
  

  • Caso: 000 // jmp

    
    

  • Caso: 001 // chama

    
    

  • Caso: 010 // ret

    
    

  • Caso: 100 // afirma

Comentário de Transição de Estado

A função de transição de estado representa uma unidade geral de transição de estado (porque contém a lógica de processamento de todos os tipos de instrução) e um cálculo geralmente é decomposto em várias instruções executadas continuamente.

Portanto, precisamos:

1. garantir o conteúdo da instrução e a validade dos estados antes e depois da execução da instrução (por exemplo, passar em uma determinada verificação de intervalo e verificação de consistência de estado) e

   
   

2. certifique-se de que a instrução executada é válida.

Comentário da Lógica de Transição

Se o estado antes e depois da execução da instrução for consistente, a atualização do estado deve ser executada de acordo com a seguinte 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

Verificação de Instrução

Conforme mostrado na Figura 1, uma instrução consiste nos seguintes elementos:

 structure instruction := (off_dst : bitvec 16) (off_op0 : bitvec 16) (off_op1 : bitvec 16) (flags : bitvec 15)

Onde:

off_dst [ bit0…15], off_op0 [ bit16…31], off_op1 [ bit32…47] estão dentro do intervalo

-2^{15} + ∑_{i = 0}^{15} b_i . 2^i ∈ [-2^{15}, 2^{15})

Mas no AIR, nós os convertemos na seguinte forma:

˜desligado∗ = desligado∗ + 2^15

(Onde * representa um dos dst, op0 e op1)

Portanto, o intervalo de valores de ˜off∗ deve ser [0,2^16)

Portanto, para a codificação de uma instrução, temos:

Observação: Em vez de alocar 15 colunas virtuais com comprimento NN para os sinalizadores de 15 bits da instrução, usamos uma coluna virtual.

˜f_i =∑_{j=i}^{14} 2j−i⋅fj

Com um comprimento de 16N, que cumpre os seguintes requisitos:

1. ˜f_0 = ∑_{j=0}^{14} 2^{j-0}⋅f_j é um valor de 15 bits

   
   

2. ˜f_15 = 0

   
   

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

   
   

Portanto, a equação (1) pode ser escrita como:

inst = ˜off_dst + 2^16⋅˜off_op0 + 2^32⋅˜off_op1 + 2^48⋅˜f0 ∈ [0,263) （2）

Como a característica do campo finito P > 2^63 , uma instrução só pode corresponder a um elemento de campo válido.

Portanto, para a instrução em si, as seguintes restrições devem ser atendidas:

Instrução: 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)

O último valor é zero: ˜f_15=0

O deslocamento está no intervalo: coluna virtual ˜off∗ ∈ [0,2^16), então off∗ ∈ [2^−15, 2^15)

Exemplos de instrução

Afirmar Igual

A instrução assert equal pode ser expressa na seguinte sintaxe:

<left_handle_op> = <right_handle_op>

Ele garante que ambos os lados da fórmula sejam iguais; caso contrário, a execução do programa será rejeitada.

O lado esquerdo da equação geralmente vem de [ fp+off_dst ] ou [ ap+off_dst ], e o lado direito tem algumas formas possíveis (reg_0 e reg_1 podem ser fp ou ap , ∘ pode ser adição ou multiplicação e imm pode ser qualquer elemento de campo fixo):

• imm

  
  

• [reg1+offop1][reg1+offop1]

  
  

• [reg0+offop0]∘[reg1+offop1][reg0+offop0]∘[reg1+offop1]

  
  

• [reg0+offop0]∘imm[reg0+offop0]∘imm

  
  

• [[reg0+offop0+offop1][[reg0+offop0+offop1]

  
  

Nota2: Divisão e subtração podem ser expressas como multiplicação e adição com diferentes ordens de operandos, respectivamente.

Uma instrução assert pode ser considerada como uma instrução de atribuição, na qual o valor de um lado é conhecido e o outro lado é desconhecido.

Por exemplo, [ap]=4[ap]=4 pode ser considerado como uma afirmação de que o valor de [ap] é 4, ou como uma definição de atribuição [ap] para 4, de acordo com o contexto.

A Figura 4 mostra alguns exemplos de instruções “assert equal” e os valores de flag para cada instrução:

Interprete a instrução [fp + 1] = 5:

• instrução assert => opcode = 4

  
  

• next_ap = ap => ap_update = 00 = 0

  
  

• next_pc = pc + instrução_size => pc_update = 000 = 0

  
  

• Para op0 e op1, não há add ou mul => res_logic(res) = 00 = 0

  
  

• Existe um valor imediato => op1_src(op1) = 001 = 1

  
  

• O endereço de valor imediato instrui que os endereços são adjacentes => off_op1 = 1

  
  

• O lado esquerdo da equação [fp + 1] => dst_reg(dst) = 1

  
  

• O lado esquerdo da equação [fp + 1] => off_dst = 1

  
  

• op0_reg/ off_op0 => valor inicial(1/-1) //Como esses sinalizadores não são usados nesta instrução, o valor padrão é preenchido.

Comentário de salto condicional e incondicional

A instrução jmp permite alterar o valor do contador de programa pc .

Cairo suporta salto relativo (seu operando representa o deslocamento do pcpc atual) e salto absoluto - representado pelas palavras-chave rel e abs respectivamente.

A instrução jmp pode ser condicional. Por exemplo, quando o valor de uma unidade de memória não for 0, a instrução jmp será acionada.

A sintaxe da instrução é a seguinte:

 #Unconditional jumps. jmp abs <address> jmp rel <offset> #Conditional jumps. jmp rel <offset> if <op> !

A Figura 5 mostra alguns exemplos das instruções jmp e os valores de flag correspondentes de cada instrução:

Interprete a instrução jmp rel [ap +1] + [fp - 7]:

• instrução jmp => opcode = 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) ///Como esses sinalizadores não são usados nesta instrução, o valor padrão é preenchido.

ligue e retorne

As instruções call e ret permitem a implementação da pilha de funções. A instrução de chamada atualiza os registradores do contador do programa ( pc ) e do ponteiro do quadro ( fp ).

A atualização do contador de programa é semelhante à instrução jmp . O valor anterior de fp é gravado em [ ap ], para permitir que a instrução ret redefina o valor de fp para o valor antes da chamada; da mesma forma, o pcpc retornado (o endereço da instrução após a instrução de chamada) é gravado em [ ap+1 ], para permitir que a instrução ret volte e continue a execução do código após a instrução de chamada.

Como duas unidades de memória foram gravadas, ap avança 2 e fp é definido como o novo ap .

A sintaxe das instruções é a seguinte:

 call abs <address> call rel <offset> ret

A Figura 6 mostra alguns exemplos de instruções call e ret e valores de flag correspondentes a cada instrução:

Interprete a chamada de instrução abs [fp + 4]:

• instrução de chamada => opcode = 0

  
  

• next_ap = ap => ap_update = b00 = 0

  
  

• next_pc = res => pc_update = 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) ///Como esses sinalizadores não são usados nesta instrução, o valor padrão é preenchido.

  
  

• dst_reg/ off_dst => valor inicial(0/0) ///Como esses sinalizadores não são usados nesta instrução, o valor padrão é preenchido.

Avançando ap

A instrução ap += <op> incrementa o valor de ap pelo operando dado.

Comente

A Figura 7 mostra alguns exemplos das instruções ap de avanço e os valores de flag correspondentes de cada instrução:

Interprete a instrução ap += 123:

• avançando instrução ap => opcode = 0

  
  

• next_ap = ap + res => ap_update = b01 = 1

  
  

• next_pc = pc + instrução_size => 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) ///Como esses sinalizadores não são usados nesta instrução, o valor padrão é preenchido.

  
  

• dst_reg/ off_dst => valor inicial(1/-1) ///Como esses sinalizadores não são usados nesta instrução, o valor padrão é preenchido.