Khám phá Cairo: Kiến trúc CPU thân thiện với STARK Turing hoàn chỉnh và hiệu quả

Cairo là một kiến trúc CPU STARK thân thiện với Turing hoàn chỉnh thực tế.

Trong bài viết này, chúng tôi giới thiệu kiến trúc CPU của Cairo về cấu trúc lệnh và chuyển đổi trạng thái, đồng thời cung cấp một số ví dụ về lệnh.

Cấu trúc hướng dẫn

Từ nguyên bản được hỗ trợ bởi CPU Cairo là một phần tử trường, trong đó trường là một trường xác thực nào đó của đặc tính P> 2 ^ 63 .

Mỗi hướng dẫn sẽ chiếm 1 hoặc 2 từ. Nếu giá trị tức thời （[ap] = “12345678”） tuân theo lệnh, lệnh sẽ chiếm 2 từ và giá trị sẽ được lưu trữ trong từ thứ hai. Từ đầu tiên của mỗi lệnh bao gồm các yếu tố sau:

• off _dst [bit0… 15]: offset địa chỉ đích, giá trị đại diện

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

  
  

• off_op0 [bit16… 31]: độ lệch địa chỉ op0, giá trị đại diện

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

• off_op1 [bit32… 47]: độ lệch địa chỉ op1, giá trị đại diện

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

  
  

• dst reg [bit48]: Thanh ghi cơ sở của offset địa chỉ đích, ap hoặc fp;

  
  

• op0 reg [bit49]: Thanh ghi cơ sở của phần bù địa chỉ op0, ap hoặc fp;

  
  

• op1_src [bit50… 52]: địa chỉ của op1,

  
  

  • Trường hợp: 000
    op1 = m (op0 + off_op1)

    
    

  • Trường hợp: 001

    op1 = m (pc + off_op1)

    
    

  • Trường hợp: 010
    op1 = m (fp + off_op1)

    
    

  • Trường hợp: 100

    op1 = m (ap + off_op1)

    
    

• res_logic bit53… 54]: logic tính toán

  
  

  • Trường hợp: 00
    res = op1

    
    

  • Trường hợp: 01
    res = op0 + op1

    
    

  • Trường hợp: 10
    res = op0 ∗ op1

    
    

• pc_update [bit55… 57]: logic cập nhật của pc

  
  

  • Trường hợp: 000 // chung
    next_pc = pc + hướng dẫn_size

    
    

  • Trường hợp: 001 // bước nhảy tuyệt đối
    next_pc = res

    
    

  • Trường hợp: 010 // bước nhảy tương đối
    next_pc = pc + res

    
    

  • Trường hợp: 100 // bước nhảy tương đối có điều kiện
    next_pc = pc + op1 (hoặc hướng dẫn_size nếu dst = 0)

    
    

• ap_update [bit58… 59]: logic cập nhật của ap

  
  

  • Trường hợp: 00
    next_ap = ap (hoặc ap + 2 nếu opcode = 1)

    
    

  • Trường hợp: 01
    next_ap = ap + res

    
    

  • Trường hợp: 10
    next_ap = ap + 1

    
    

• opcode [bit60… 62]: các loại opcode

  
  

  • Trường hợp: 000 // jmp

    
    

  • Trường hợp: 001 // cuộc gọi

    
    

  • Trường hợp: 010 // ret

    
    

  • Trường hợp: 100 // khẳng định

Nhận xét về chuyển đổi trạng thái

Hàm chuyển trạng thái đại diện cho một đơn vị chuyển đổi trạng thái chung (vì nó chứa logic xử lý của tất cả các loại lệnh) và một phép tính thường được phân tách thành nhiều lệnh được thực thi liên tục.

Do đó, chúng ta cần:

1. đảm bảo nội dung của lệnh và tính hợp lệ của các trạng thái trước và sau khi lệnh được thực thi (ví dụ: vượt qua kiểm tra phạm vi nhất định và kiểm tra tính nhất quán của trạng thái) và

   
   

2. đảm bảo rằng lệnh được thực thi là hợp lệ.

Nhận xét logic chuyển đổi

Nếu trạng thái trước và sau khi thực hiện lệnh là nhất quán, thì việc cập nhật trạng thái phải được thực hiện theo logic sau:

 #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

Xác minh hướng dẫn

Như trong Hình 1, một lệnh bao gồm các phần tử sau:

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

Ở đâu:

off_dst [bit0… 15], off_op0 [bit16… 31], off_op1 [bit32… 47] nằm trong phạm vi

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

Nhưng trong AIR, chúng tôi chuyển đổi chúng thành dạng sau:

˜off ∗ = tắt ∗ + 2 ^ 15

(Trong đó * đại diện cho một trong các dst, op0 và op1)

Vì vậy, phạm vi giá trị của ˜off ∗ phải là [0,2 ^ 16)

Do đó, để mã hóa một lệnh, chúng ta có:

Lưu ý: Thay vì phân bổ 15 cột ảo có độ dài NN cho các cờ 15 bit của lệnh, thay vào đó, chúng ta sử dụng một cột ảo.

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

Với chiều dài 16N, đáp ứng các yêu cầu sau:

1. ˜f_0 = ∑_ {j = 0} ^ {14} 2 ^ {j-0} ⋅f_j là giá trị 15 bit

   
   

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

   
   

Do đó, phương trình (1) có thể được viết thành:

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

Vì đặc tính của trường hữu hạn P> 2 ^ 63 , một lệnh chỉ có thể tương ứng với một phần tử trường hợp lệ.

Do đó, đối với bản thân lệnh, cần đáp ứng các ràng buộc sau:

Hướng dẫ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 với mọi i ∈ [0,15)

Giá trị cuối cùng bằng 0: ˜f_15 = 0

Phần bù nằm trong phạm vi: cột ảo ˜ off ∗ ∈ [0,2 ^ 16), do đó tắt ∗ ∈ [2 ^ −15, 2 ^ 15)

Ví dụ hướng dẫn

Khẳng định bằng

Lệnh xác nhận bằng nhau có thể được diễn đạt theo cú pháp sau:

<left_handle_op> = <right_handle_op>

Nó đảm bảo rằng cả hai vế của công thức đều bằng nhau; nếu không việc thực thi chương trình sẽ bị từ chối.

Vế trái của phương trình thường đến từ [ fp + off_dst ] hoặc [ ap + off_dst ] và vế phải có một số dạng có thể có (reg_0 và reg_1 có thể là fp hoặc ap , ∘ có thể là phép cộng hoặc phép nhân, và Imm có thể là bất kỳ phần tử trường cố định nào):

• non nớt

  
  

• [reg1 + offop1] [reg1 + offop1]

  
  

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

  
  

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

  
  

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

  
  

Lưu ý 2: Phép chia và phép trừ có thể được biểu thị thành phép nhân và phép cộng với các thứ tự toán hạng khác nhau, tương ứng.

Một lệnh khẳng định có thể được coi là một lệnh gán, trong đó giá trị của một phía được biết và phía bên kia là không xác định.

Ví dụ: [ap] = 4 [ap] = 4 có thể được coi là một khẳng định rằng giá trị của [ap] là 4 hoặc như một cài đặt gán [ap] thành 4, tùy theo ngữ cảnh.

Hình 4 cho thấy một số ví dụ về các lệnh “xác nhận bằng nhau” và các giá trị cờ cho mỗi lệnh:

Giải thích hướng dẫn [fp + 1] = 5:

• khẳng định hướng dẫn => opcode = 4

  
  

• next_ap = ap => ap_update = 00 = 0

  
  

• next_pc = pc + guide_size => pc_update = 000 = 0

  
  

• Đối với op0 và op1, không có thêm hoặc đa => res_logic (res) = 00 = 0

  
  

• Tồn tại một giá trị tức thì => op1_src (op1) = 001 = 1

  
  

• Địa chỉ giá trị tức thì chỉ thị rằng các địa chỉ liền kề nhau => off_op1 = 1

  
  

• Vế trái của phương trình [fp + 1] => dst_reg (dst) = 1

  
  

• Vế trái của phương trình [fp + 1] => off_dst = 1

  
  

• op0_reg / off_op0 => inital value (1 / -1) // Bởi vì những cờ này không được sử dụng trong lệnh này, giá trị mặc định được điền vào.

Nhận xét nhảy có điều kiện và không có điều kiện

Lệnh jmp cho phép thay đổi giá trị của pc bộ đếm chương trình.

Cairo hỗ trợ bước nhảy tương đối (toán hạng của nó đại diện cho độ lệch từ pcpc） hiện tại và bước nhảy tuyệt đối - được đại diện bởi các từ khóa rel và abs tương ứng.

Lệnh jmp có thể có điều kiện. Ví dụ, khi giá trị của một đơn vị bộ nhớ không phải là 0, lệnh jmp sẽ được kích hoạt.

Cú pháp của lệnh như sau:

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

Hình 5 cho thấy một số ví dụ về các lệnh jmp và các giá trị cờ tương ứng của mỗi lệnh:

Giải thích hướng dẫn jmp rel [ap +1] + [fp - 7]:

• hướng dẫn 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 => inital value (1 / -1) /// Bởi vì những cờ này không được sử dụng trong lệnh này, giá trị mặc định được điền vào.

gọi và bắt đầu lại

Lệnh gọi và lệnh ret cho phép thực hiện ngăn xếp hàm. Lệnh gọi cập nhật thanh ghi bộ đếm chương trình ( pc ) và con trỏ khung ( fp ).

Việc cập nhật bộ đếm chương trình tương tự như lệnh jmp . Giá trị trước đó của fp được ghi vào [ ap ], để cho phép lệnh ret đặt lại giá trị của fp về giá trị trước khi gọi; tương tự, pcpc trả về (địa chỉ của lệnh sau lệnh gọi) được ghi vào [ ap + 1 ], để cho phép lệnh ret nhảy trở lại và tiếp tục thực thi mã sau lệnh gọi.

Khi hai đơn vị bộ nhớ được viết, ap nâng cao 2 và fp được đặt thành ap mới.

Cú pháp của hướng dẫn như sau:

 call abs <address> call rel <offset> ret

Hình 6 cho thấy một số ví dụ về lệnh gọi và lệnh ret và giá trị cờ tương ứng với mỗi lệnh:

Giải thích lệnh gọi abs [fp + 4]:

• lệnh gọi => 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 => inital value (0/1) /// Vì những cờ này không được sử dụng trong lệnh này nên giá trị mặc định sẽ được điền vào.

  
  

• dst_reg / off_dst => inital value (0/0) /// Vì những cờ này không được sử dụng trong lệnh này nên giá trị mặc định sẽ được điền vào.

Nâng cao ap

Lệnh ap + = <op> tăng giá trị của ap bằng toán hạng đã cho.

Bình luận

Hình 7 cho thấy một số ví dụ về các lệnh ap nâng cao và các giá trị cờ tương ứng của mỗi lệnh:

Giải thích lệnh ap + = 123:

• tiến trình hướng dẫn ap => opcode = 0

  
  

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

  
  

• next_pc = pc + hướng dẫn_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 => inital value (1 / -1) /// Bởi vì những cờ này không được sử dụng trong lệnh này, giá trị mặc định được điền vào.

  
  

• dst_reg / off_dst => inital value (1 / -1) /// Bởi vì những cờ này không được sử dụng trong lệnh này, giá trị mặc định được điền vào.