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

Cairo 是一个实用的图灵完备的 STARK 友好型 CPU 架构。 在本文中，我们从指令结构和状态转换方面介绍了 Cairo 的 CPU 架构，并提供了一些指令示例。 指令结构 Cairo CPU 原生支持的词是字段元素，其中字段是特征 的某个固定有限字段。 P>2^63 每条指令将占用 1 或 2 个字。如果指令后面有一个立即数（[ap] = “12345678”），则该指令将占用 2 个字，该值将存储在第二个字中。每条指令的第一个字由以下元素组成： _dst[bit0…15]：目的地址偏移量，代表值 off -2^{15} + ∑_{i = 0}^{15} b_i 。 2^i ∈ [-2^{15}, 2^{15}); [bit16…31]：op0地址偏移，代表值 off_op0 -2^{15} + ∑_{i = 0}^{15} b_i 。 2^i ∈ [-2^{15}, 2^{15}); [bit32…47]：op1地址偏移，代表值 off_op1 -2^{15} + ∑_{i = 0}^{15} b_i 。 2^i ∈ [-2^{15}, 2^{15}); [bit48]：目的地址偏移的基址寄存器，ap或fp； dst reg [bit49]：op0地址偏移的基址寄存器，ap或fp； op0 reg [bit50…52]：op1的地址， op1_src 案例：000 op1=m(op0+off_op1) 案例：001 op1=m(pc+off_op1) 案例：010 op1=m(fp+off_op1) 案例：100 op1=m(ap+off_op1) bit53…54]：计算逻辑 res_logic 案例：00 水库= op1 案例：01 res = op0 + op1 案例：10 res = op0 * op1 [ bit55…57]：pc的更新逻辑 pc_update 案例：000 //常见 next_pc = pc + 指令大小 case: 001 // 绝对跳转 next_pc = res case: 010 // 相对跳转 next_pc = pc + res case: 100 // 条件相对跳转 next_pc = pc + op1（如果 dst = 0 则为指令大小） [ bit58…59]：ap 的更新逻辑 ap_update 案例：00 next_ap = ap（如果操作码 = 1，则为 ap+2） 案例：01 next_ap = ap + res 案例：10 下一个_ap = ap + 1 [bit60…62]：操作码类型 操作码 案例：000 // jmp 案例：001 //调用 案例：010 // ret 案例：100 //断言 状态转换注释 状态转移函数代表一个通用的状态转移单元（因为它包含了所有指令类型的处理逻辑），一个计算通常被分解成多个连续执行的指令。 因此，我们需要： 确保指令的内容和指令执行前后状态的有效性（例如，通过一定的范围检查和状态一致性检查）和 确保执行的指令有效。 转换逻辑注释 如果指令执行前后的状态一致，则状态的更新必须按照如下逻辑执行： #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) 在哪里： [ bit0…15]、 [ bit16…31]、 [ bit32…47] 在范围内 off_dst off_op0 off_op1 -2^{15} + ∑_{i = 0}^{15} b_i 。 2^i ∈ [-2^{15}, 2^{15}) 但在 AIR 中，我们将它们转换为以下形式： ～off∗ = off∗ + 2^15 （其中 * 代表 dst、op0 和 op1 之一） 所以 的取值范围应该是 [0,2^16) ∼off∗ 因此，对于指令的编码，我们有： 我们没有将长度为 NN 的 15 个虚拟列分配给指令的 15 位标志，而是使用一个虚拟列。 注意： =∑_{j=i}^{14} 2j−i⋅fj ∼f_i 长度为16N，满足以下要求： ∼f_0 = ∑_{j=0}^{14} 2^{j-0}⋅f_j 是一个 15 位的值 ～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 因此，等式（1）可以写成： （2） inst = ~off_dst + 2^16⋅~off_op0 + 2^32⋅~off_op1 + 2^48⋅~f0 ∈ [0,263) 由于有限域的特性 ，一条指令只能对应一个有效域元素。 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 虚拟列 ∈ [0,2^16)，所以 ∈ [2^−15, 2^15) 偏移量在范围内： ∼off∗ off∗ 说明示例 断言相等 断言相等指令可以用以下语法表示： = 保证公式两边相等；否则程序的执行将被拒绝。 等式左边常来自[ ]或[ ]，右边有一些可能的形式（reg_0和reg_1可以是 或 ，∘可以是加法或乘法，imm可以是任何固定字段元素）： fp+off_dst ap+off_dst fp ap 嗯 [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 指令可能是有条件的。例如，当某个内存单元的值不为 0 时，就会触发 指令。 jmp jmp 该指令的语法如下： #Unconditional jumps. jmp abs jmp rel #Conditional jumps. jmp rel if ! 图 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 程序计数器的更新与 指令类似。将 之前的值写入 [ ]，以允许 指令将 的值重置为调用之前的值；同样，返回的pcpc（call指令后的指令地址）写入[ ]，让 指令跳转回去继续执行call指令后的代码。 jmp fp ap ret fp ap+1 ret 当写入两个内存单元时， 提前 2 并且 设置为新的 。 ap fp ap 指令的语法如下： call abs call rel 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 += 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) ///因为本指令没有用到这些标志，所以填写默认值。

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

太長; 讀書

Company Mentioned

@sin7y

相關故事