探索 Cairo：实用且高效的图灵完备的 STARK 友好型 CPU 架构

Cairo 是一个实用的图灵完备的 STARK 友好型 CPU 架构。

在本文中，我们从指令结构和状态转换方面介绍了 Cairo 的 CPU 架构，并提供了一些指令示例。

指令结构

Cairo CPU 原生支持的词是字段元素，其中字段是特征P>2^63的某个固定有限字段。

每条指令将占用 1 或 2 个字。如果指令后面有一个立即数（[ap] = “12345678”），则该指令将占用 2 个字，该值将存储在第二个字中。每条指令的第一个字由以下元素组成：

• off _dst[bit0…15]：目的地址偏移量，代表值

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

  
  

• off_op0 [bit16…31]：op0地址偏移，代表值

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

• off_op1 [bit32…47]：op1地址偏移，代表值

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

  
  

• dst reg [bit48]：目的地址偏移的基址寄存器，ap或fp；

  
  

• op0 reg [bit49]：op0地址偏移的基址寄存器，ap或fp；

  
  

• op1_src [bit50…52]：op1的地址，

  
  

  • 案例：000
    op1=m(op0+off_op1)

    
    

  • 案例：001

    op1=m(pc+off_op1)

    
    

  • 案例：010
    op1=m(fp+off_op1)

    
    

  • 案例：100

    op1=m(ap+off_op1)

    
    

• res_logic bit53…54]：计算逻辑

  
  

  • 案例：00
    水库= op1

    
    

  • 案例：01
    res = op0 + op1

    
    

  • 案例：10
    res = op0 * op1

    
    

• pc_update [ bit55…57]：pc的更新逻辑

  
  

  • 案例：000 //常见
    next_pc = pc + 指令大小

    
    

  • case: 001 // 绝对跳转
    next_pc = res

    
    

  • case: 010 // 相对跳转
    next_pc = pc + res

    
    

  • case: 100 // 条件相对跳转
    next_pc = pc + op1（如果 dst = 0 则为指令大小）

    
    

• ap_update [ bit58…59]：ap 的更新逻辑

  
  

  • 案例：00
    next_ap = ap（如果操作码 = 1，则为 ap+2）

    
    

  • 案例：01
    next_ap = ap + res

    
    

  • 案例：10
    下一个_ap = ap + 1

    
    

• 操作码[bit60…62]：操作码类型

  
  

  • 案例：000 // jmp

    
    

  • 案例：001 //调用

    
    

  • 案例：010 // ret

    
    

  • 案例：100 //断言

状态转换注释

状态转移函数代表一个通用的状态转移单元（因为它包含了所有指令类型的处理逻辑），一个计算通常被分解成多个连续执行的指令。

因此，我们需要：

1. 确保指令的内容和指令执行前后状态的有效性（例如，通过一定的范围检查和状态一致性检查）和

   
   

2. 确保执行的指令有效。

转换逻辑注释

如果指令执行前后的状态一致，则状态的更新必须按照如下逻辑执行：

 #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

指令验证

如图 1 所示，一条指令由以下元素组成：

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

在哪里：

off_dst [ bit0…15]、 off_op0 [ bit16…31]、 off_op1 [ bit32…47] 在范围内

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

但在 AIR 中，我们将它们转换为以下形式：

～off∗ = off∗ + 2^15

（其中 * 代表 dst、op0 和 op1 之一）

所以∼off∗的取值范围应该是 [0,2^16)

因此，对于指令的编码，我们有：

注意：我们没有将长度为 NN 的 15 个虚拟列分配给指令的 15 位标志，而是使用一个虚拟列。

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

长度为16N，满足以下要求：

1. ∼f_0 = ∑_{j=0}^{14} 2^{j-0}⋅f_j 是一个 15 位的值

   
   

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

   
   

因此，等式（1）可以写成：

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

由于有限域的特性P > 2^63 ，一条指令只能对应一个有效域元素。

因此，对于指令本身，应满足以下约束：

指令： inst= ～off_dst + 2^16⋅～off_op0 + 2^32⋅～off_op1 + 2^48⋅ ～ f0

位： (~f_i−2~f_i +1)(~f_i−2~f_i+1 -1)=0 对于所有 i ∈ [0,15)

最后一个值为零： ~f_15=0

偏移量在范围内：虚拟列∼off∗ ∈ [0,2^16)，所以off∗ ∈ [2^−15, 2^15)

说明示例

断言相等

断言相等指令可以用以下语法表示：

<left_handle_op> = <right_handle_op>

保证公式两边相等；否则程序的执行将被拒绝。

等式左边常来自[ fp+off_dst ]或[ ap+off_dst ]，右边有一些可能的形式（reg_0和reg_1可以是fp或ap ，∘可以是加法或乘法，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]

  
  

注2：除法和减法可以分别表示为不同操作数顺序的乘法和加法。

断言指令可以看成是赋值指令，其中一侧的值是已知的，而另一侧的值是未知的。

例如，[ap]=4[ap]=4 可以被认为是断言 [ap] 的值为 4，或者根据上下文将 [ap] 设置为 4。

图 4 显示了“断言相等”指令的一些示例以及每条指令的标志值：

解释指令 [fp + 1] = 5：

• 断言指令 => 操作码 = 4

  
  

• next_ap = ap => ap_update = 00 = 0

  
  

• next_pc = pc + 指令大小 => pc_update = 000 = 0

  
  

• 对于 op0 和 op1，没有 add 或 mul => res_logic(res) = 00 = 0

  
  

• 存在一个立即数 => op1_src(op1) = 001 = 1

  
  

• 立即值地址指示地址相邻 => off_op1 = 1

  
  

• 等式左侧 [fp + 1] => dst_reg(dst) = 1

  
  

• 等式左侧 [fp + 1] => off_dst = 1

  
  

• op0_reg/ off_op0 => inital value(1/-1) //因为本指令没有用到这些标志，所以填写默认值。

有条件和无条件跳转注释

jmp指令允许更改程序计数器pc的值。

Cairo 支持相对跳转（其操作数表示与当前 pc 的偏移量）和绝对跳转 - 分别由关键字rel和abs表示。

jmp指令可能是有条件的。例如，当某个内存单元的值不为 0 时，就会触发jmp指令。

该指令的语法如下：

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

图 5 显示了jmp指令的一些示例以及每条指令的相应标志值：

解释指令 jmp rel [ap +1] + [fp - 7]：

• jmp 指令 => 操作码 = 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 => inital value(1/-1) ///因为本指令没有用到这些标志，所以填写默认值。

打电话和转

call和ret指令允许函数栈的实现。 call指令更新程序计数器 ( pc ) 和帧指针 ( fp ) 寄存器。

程序计数器的更新与jmp指令类似。将fp之前的值写入 [ ap ]，以允许ret指令将fp的值重置为调用之前的值；同样，返回的pcpc（call指令后的指令地址）写入[ ap+1 ]，让ret指令跳转回去继续执行call指令后的代码。

当写入两个内存单元时， ap提前 2 并且fp设置为新的ap 。

指令的语法如下：

 call abs <address> call rel <offset> ret

图 6 显示了一些call和ret指令的示例以及对应于每条指令的标志值：

解释指令调用 abs [fp + 4]：

• 调用指令 => 操作码 = 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 => inital value(0/1) ///因为本指令没有用到这些标志位，所以填写默认值。

  
  

• dst_reg/ off_dst => inital value(0/0) ///因为本指令没有用到这些标志，所以填写默认值。

推进应用

指令ap += <op>将ap的值增加给定的操作数。

评论

图 7 显示了一些推进ap指令的示例以及每条指令的相应标志值：

解释指令 ap += 123：

• 推进 ap 指令 => 操作码 = 0

  
  

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

  
  

• next_pc = pc + 指令大小 => 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 => inital value(1/-1) ///因为本指令没有用到这些标志，所以填写默认值。

  
  

• dst_reg/ off_dst => inital value(1/-1) ///因为本指令没有用到这些标志，所以填写默认值。