カイロを探る: 実用的で効率的な Turing 完全な STARK 対応 CPU アーキテクチャ

Cairo は、実質的に効率的な Turing 完全な STARK に適した CPU アーキテクチャです。

この記事では、Cairo の CPU アーキテクチャを命令構造と状態遷移の観点から紹介し、命令の例をいくつか示します。

命令構造

Cairo CPU でネイティブにサポートされている単語はフィールド要素であり、フィールドは特性P>2^63の固定有限フィールドです。

各命令は 1 または 2 ワードを占有します。命令の後に即値（[ap] = “12345678”）が続く場合、命令は2ワードを占有し、値は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
    res = op1

    
    

  • ケース: 01
    res = op0 + op1

    
    

  • ケース: 10
    res = op0 ∗ op1

    
    

• pc_update [bit55…57]: pc の更新ロジック

  
  

  • Case: 000 // 共通
    next_pc = pc + instruction_size

    
    

  • Case: 001 //絶対ジャンプ
    next_pc = res

    
    

  • Case: 010 // 相対ジャンプ
    next_pc = PC + res

    
    

  • Case: 100 // 条件付き相対ジャンプ
    next_pc = pc + op1 (または dst = 0 の場合は instruction_size)

    
    

• ap_update [bit58…59]: ap の更新ロジック

  
  

  • ケース: 00
    next_ap = ap (または、opcode = 1 の場合は ap+2)

    
    

  • ケース: 01
    next_ap = ap + res

    
    

  • ケース: 10
    next_ap = ap + 1

    
    

• opcode [bit60…62]: オペコードの種類

  
  

  • ケース: 000 // jmp

    
    

  • Case: 001 // 呼び出し

    
    

  • Case: 010 // ret

    
    

  • Case: 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 に示すように、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 では、それらを次の形式に変換します。

〜オフ* = オフ* + 2^15

(* は dst、op0、op1 のいずれかを表します)

したがって、 ~off*の値の範囲は [0,2^16) になります。

したがって、命令のコーディングについては、次のようになります。

注:長さ NN の 15 個の仮想列を命令の 15 ビット フラグに割り当てる代わりに、1 つの仮想列を使用します。

˜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であるため、1 つの命令は 1 つの有効な体要素にしか対応できません。

したがって、命令自体については、次の制約を満たす必要があります。

命令： 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 for all i ∈ [0,15)

最後の値はゼロです: ~f_15=0

オフセットは範囲内です:仮想列˜off∗ ∈ [0,2^16)、したがってoff∗ ∈ [2^−15, 2^15)

命令例

等しいことをアサート

assert equal 命令は、次の構文で表現できます。

<左ハンドル操作> = <右ハンドル操作>

式の両辺が等しいことが保証されます。そうしないと、プログラムの実行が拒否されます。

方程式の左辺は [ 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 は、「assert equal」命令と各命令のフラグ値の例を示しています。

命令の解釈[fp + 1] = 5:

• アサート命令 => オペコード = 4

  
  

• next_ap = ap => ap_update = 00 = 0

  
  

• next_pc = pc + instruction_size => 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 => 初期値(1/-1) //本命令ではこれらのフラグを使用しないため、デフォルト値が入ります。

条件付きおよび無条件のジャンプコメント

jmp命令を使用すると、プログラム カウンタpcの値を変更できます。

Cairo は相対ジャンプ (そのオペランドは現在の pcpc からのオフセットを表します) と絶対ジャンプをサポートします - それぞれキーワード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 => 初期値(1/-1) ///本命令ではこれらのフラグを使用しないため、デフォルト値が入ります。

コールアンドレッティング

callおよびret命令により、関数スタックの実装が可能になります。 call命令は、プログラム カウンター ( pc ) およびフレーム ポインター ( fp ) レジスターを更新します。

プログラムカウンタの更新はjmp命令と同様です。 fpの以前の値は [ ap ] に書き込まれ、 ret命令がfpの値を呼び出し前の値にリセットできるようにします。同様に、返された pcpc (call 命令の後の命令のアドレス) は [ ap+1 ] に書き込まれ、 ret命令がジャンプして call 命令の後のコードの実行を続行できるようにします。

2 つのメモリ ユニットが書き込まれたため、 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 => 初期値(0/1) ///本命令ではこれらのフラグを使用しないため、デフォルト値が入ります。

  
  

• dst_reg/ off_dst => 初期値(0/0) ///本命令ではこれらのフラグを使用しないため、デフォルト値が入ります。

アドバンシングap

命令ap += <op>は、指定されたオペランドによってapの値をインクリメントします。

コメント

図 7 は、 ap命令を進める例と、各命令の対応するフラグ値を示しています。

命令 ap += 123 の解釈:

• ap 命令を進める => オペコード = 0

  
  

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

  
  

• next_pc = pc + instruction_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 => 初期値(1/-1) ///本命令ではこれらのフラグを使用しないため、デフォルト値が入ります。

  
  

• dst_reg/ off_dst => 初期値(1/-1) ///本命令ではこれらのフラグを使用しないため、デフォルト値が入ります。