Quy trình thực thi bằng chứng dựa trên STARK hoạt động như thế nào trên Miden V1?

Miden là một giải pháp triển khai ZKVM dựa trên công nghệ hoàn hảo.

Trong lớp cơ bản của nó, bằng chứng rõ ràng được tạo dựa trên thư viện ZKP và bằng chứng sẽ được xác minh. Phần chấm trong Hình 1 sau đây là chức năng chính được thực hiện bởi Miden. Nó chủ yếu bao gồm ba thành phần.

1. Một tập hợp các trình biên dịch cú pháp từ vựng, đó là trình phân tích từ vựng và phân tích cú pháp trong Hình 1. Chúng có thể lập trình các lệnh hợp ngữ được xác định bởi Miden thành khối mã hoặc giá trị opcode và op có trong khối.

2. Một tập hợp các trình thực thi lệnh, đó là trình thực thi trong Hình 1. Nó sẽ thực thi khối mã và giá trị opcode và op có trong khối theo các quy tắc đã xác định. Và kết quả được thực thi sẽ là dấu vết thực thi được sử dụng để tạo bằng chứng.

3. Một bộ AIR (Biểu diễn trung gian trừu tượng), đáp ứng các yêu cầu của bằng chứng rõ ràng, đó là AIR trong Hình 1. Nó tiến hành các ràng buộc đối với quá trình thực thi của Máy ảo Miden.

Hình 1. Các thành phần của dự án Miden

Bản vẽ thiết kế kết cấu AIR

Các ràng buộc của AIR chia thành ngăn xếp và bộ giải mã: Hình 2 cho thấy các ràng buộc của ngăn xếp, được phân phối với ngăn xếp có độ sâu đỉnh là 8 khi khởi tạo.

Max_depth được tăng lên khi cần thiết nếu phân phối ban đầu có thể bị vượt quá trong quá trình thực thi, tùy thuộc vào nhu cầu của chương trình, nhưng nó không được vượt quá độ sâu tối đa là 16, nếu không sẽ xảy ra lỗi.

Hình 2: Cột ràng buộc ngăn xếp

Như có thể thấy bên dưới, Hình 3 cho thấy các hạn chế của bộ giải mã. Trong số các ràng buộc này, op_counter, op_SPONGE, CF_OP_bits, LD_OP_BITS và hd_OP_bits là độ dài cột cố định.

Op_sponge được sử dụng để ràng buộc thứ tự và tính đúng đắn của các hướng dẫn. Cf_op_bits hạn chế luồng 3-bit. Các ld_op_bits và hd_op_bits hạn chế 5 bit thấp và 2 bit cao của user_ops tương ứng.

Các ld_op_bits và hd_op_bits kết hợp để tạo thành một user_op có thể thực thi được cũng được sử dụng như một bộ chọn cho mỗi bước của các ràng buộc trạng thái của ngăn xếp!

Hình 3: Cột Ràng buộc Bộ giải mã

Ví dụ về quy trình thực thi của Miden VM

Phần này hiển thị logic Miden đơn giản để minh họa quá trình thực thi của máy ảo và việc tạo ra dấu vết thực thi của stark.

Đoạn mã 1 sau đây là đoạn để thực thi: Logic thực thi của nó là đẩy 3 và 5 trên ngăn xếp. Sau đó đọc lá cờ từ băng.

Kiểm tra xem cờ là 1 hay 0. Nếu là 1, hãy chạy "logic if.true" để lấy hai số 3 và 5 được đẩy trên ngăn xếp, cộng chúng lại với nhau, tạo ra 8 và đẩy 8 trên cây rơm. Nếu nó là 0, hãy chạy "logic khác" để lấy các số 3 và 5 rồi nhân chúng với nhau dẫn đến 15, sau đó đẩy 15 lên ngăn xếp.

 begin push.3 push.5 read if.true add else mul end end

Phân đoạn mã 1

Mã lệnh cuối cùng được phân tích cú pháp và phân tích cú pháp của Miden được hiển thị trong đoạn mã 2 sau:

 begin noop noop noop noop noop noop noop push(3) noop noop noop noop noop noop noop push(5) read noop noop noop noop noop noop noop noop noop noop noop noop noop, if assert add noop noop noop noop noop noop noop noop noop noop noop noop noop else not assert mul noop noop noop noop noop noop noop noop noop noop noop noop end]

Phân đoạn mã 2

Hình 4 cho thấy quá trình máy ảo thực thi đoạn mã 2.

Phần giữa là lưu đồ của trình thực thi thực thi các opcodes. Các đường chấm bên trái đề cập đến dấu vết bộ giải mã được tạo ra trong quá trình thực thi mã. Các dòng dấu chấm-gạch ngang bên phải đề cập đến dấu vết ngăn xếp được tạo ra trong quá trình thực thi mã.

Trong hình, trình thực thi tiến hành thực thi từng khối theo khối mã. Trong ví dụ này, một khối span được thực thi đầu tiên.

Sau đó, cấu trúc if-else-end ở bước 32 được thực hiện để nhập khối chuyển đổi và nhấn hàm băm xốp được tạo ra bởi lần thực thi cuối cùng của khối nhịp trước đó vào ctx_stack. Sau khi khối chuyển đổi được thực thi, hãy đặt nó vào miếng bọt biển ở bước 49.

Hình 4: hình thay đổi trạng thái của máy ảo thực thi opcode

Lưu ý: Tài liệu này mô tả phiên bản mới nhất của nhánh chính cho các dự án Miden kể từ năm 2022-05-27. Cho đến nay chi nhánh tiếp theo của Miden đã thực hiện rất nhiều việc thiết kế lại các hướng dẫn và AIR chỉ thực hiện một số ràng buộc.

Điều kiện ràng buộc của ngăn xếp

Trong phần này, chúng tôi sẽ hiển thị các điều kiện ràng buộc của hướng dẫn thao tác Người dùng chính, trong đó, old_stack_x đề cập đến giá trị được lưu trữ tại vị trí x của ngăn xếp trước khi thực hiện lệnh, new_stack_x đề cập đến giá trị được lưu trữ tại vị trí x của ngăn xếp sau khi thực hiện lệnh, “->” đề cập đến bản sao của giá trị từ phía bên trái của ngăn xếp sang bên phải và “==” đề cập đến ràng buộc phương trình. Các ràng buộc của ngăn xếp tương đối đơn giản và không cần giải thích.

Hướng dẫn điều kiện

Chọn

Hạn chế:

 new_stack_0 == (condition * x) + ((1 - condition) * y) old_stack_0 == x old_stack_1 == y old_stack_2 == condition old_stack_3 --> new_stack_1 old_stack_n. --> new_stack_n-2 aux_0 == condition.is_binary == true

Nếu điều kiện là 1, x ở trên cùng của ngăn xếp. Nếu điều kiện là 0, y ở trên cùng của ngăn xếp.

Hướng dẫn số học

cộng

Hạn chế:

 old_stack_0 + old_stack_1 == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

mul

Hạn chế:

 old_stack_0 * old_stack_1 == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

inv

Hạn chế:

 old_stack_0 * new_stack_0 == 1 old_stack_1 --> new_stack_1 old_stack_n. --> new_stack_n

phủ định

Hạn chế:

 old_stack_0 + new_stack_0 == 0 old_stack_1 --> new_stack_1 old_stack_n. --> new_stack_n

Hướng dẫn Bool

không phải

Hạn chế:

 aux_0: make sure old_stack_0 is binary 1-old_stack_0 == new_stack_0 old_stack_1 --> new_stack_1 old_stack_n. --> new_stack_n

và

Hạn chế:

 aux_0: make sure old_stack_0 is binary aux_1: make sure old_stack_1 is binary old_stack_0 * old_stack_1 == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

hoặc

Hạn chế:

 aux_0: make sure old_stack_0 is binary aux_1: make sure old_stack_1 is binary 1- (1-old_stack_0) *(1- old_stack_1) == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

Hướng dẫn băm

RESCR

Giới hạn hàm băm thỏa mãn giao thức hàm băm
Chiếm 6 thanh ghi.

Hạn chế:

 hash(old_stack0，old_stack1， old_stack2， old_stack3， old_stack3， old_stack5) == （new_stack0，new_stack1， new_stack2， new_stack3， new_stack3， new_stack5） old_stack_6 --> new_stack_6 old_stack_n. --> new_stack_n

So sánh hướng dẫn

eq

Hạn chế:

 aux_0 == new_stack_0 * diff == 0 new_stack_0 == 1- (old_stack_1-old_stack_2)*old_stack_0 old_stack_0 == inv(old_stack_1-old_stack_2) old_stack_3 --> new_stack_1 old_stack_n. --> new_stack_n-2

cmp

So sánh theo chu kỳ độ dài bit của hai số được so sánh, chẳng hạn như:

A: [0,1,0,1]
B: [0,0,1,1]

Các hướng dẫn so sánh cần được thực hiện bốn lần.

Hạn chế:

 // layout of first 8 registers // [pow, bit_a, bit_b, not_set, gt, lt, acc_b, acc_a] // x and y bits are binary new_stack_1 == x_big_idx(lg lt flag) （type:binary) new_stack_2 == y_big_idx(lg lt flag) （type:binary) bit_gt = x_big_idx*(1-y_big_idx) bit_lt = y_big_idx*(1-x_big_idx) // comparison trackers were updated correctly new_stack_3 = not_set_idx new_stack_4(gt) == old_stack_4(gt_idx) + bit_gt * not_set_idx new_stack_5(lt) == old_stack_5(lt_idx) + bit_lt * not_set_idx // binary representation accumulators were updated correctly old_stack_0 = POW2_IDX old_stack_6 = Y_ACC_IDX old_stack_7 = X_ACC_IDX new_stack_6 == old_stack_6 + x_big_idx * old_stack_0(power_of_two); new_stack_7 == old_stack_7 + y_big_idx * old_stack_0(power_of_two); // when GT or LT register is set to 1, not_set flag is cleared not_set_check = (1-old_stack_5(lt_idx))*(1-old_stack_4(gt_idx)) not_set_check == new_stack_3(not_set_idx) // power of 2 register was updated correctly new_stack[POW2_IDX] * two == old_stack[POW2_IDX] old_stack_8 --> new_stack_8 old_stack_n --> new_stack_n

Hướng dẫn vận hành ngăn xếp

Dup.n

Hạn chế:

 new_stack_0 == old_stack_0 ... new_stack_n-1 == old_stack_n-1 old_stack_0 --> new_stack_n old_stack_k --> new_stack_n+k

tráo đổi

Hạn chế:

 new_stack_0 == old_stack_1 new_stack_1 == old_stack_0 old_stack_2 --> new_stack_2 old_stack_n --> new_stack_n

ROLL4

Hạn chế:

 new_stack_0 == old_stack_3 new_stack_1 == old_stack_0 new_stack_2 == old_stack_1 new_stack_3 == old_stack_2 old_stack_4 --> new_stack_4 old_stack_n --> new_stack_n

Điều kiện ràng buộc của nhận xét của người giải mã

Trong phần này, chúng tôi sẽ chỉ ra các điều kiện ràng buộc của lệnh hoạt động Luồng chính.

Thực thi mã người dùng

op_bits

Đối với các ràng buộc của cf_op_bits, ld_op_bits và hd_op_bits
Ràng buộc 1: mỗi bit chỉ có thể là 0 hoặc 1.
Ràng buộc 2: khi op_counter không phải là 0, ld_ops và hd_ops đều không được bằng 0.
Ràng buộc 3: khi cf_op_bits là hacc, trạng thái op_counter sẽ tăng 1.
Ràng buộc 4: Các lệnh BEGIN, LOOP, BREAK và WRAP cần được căn chỉnh theo 16.
Ràng buộc 5: Hướng dẫn TEND và FEND cần phải được căn chỉnh theo 16.
Ràng buộc 6: Lệnh PUSH cần được căn chỉnh theo 8.

Hạn chế:

 cf_op_bits == binary ld_op_bits == binary hd_op_bits == binary // ld_ops and hd_ops can be all 0s at the first step, but cannot be all 0s at any other step op_counter * binary_not(ld_bit_prod) * binary_not(hd_bit_prod) == 0 if op_counter != 0 (1-ld_bit_prod)*(1- hd_bit_prod) == 0 if is_hacc != true op_counter = current.op_counter // BEGIN, LOOP, BREAK, and WRAP are allowed only on one less than multiple of 16 // TEND and FEND is allowed only on multiples of 16 // PUSH is allowed only on multiples of 8

hacc Bình luận

Hacc, với tư cách là flowOps, sẽ luôn gây ra sự thay đổi trạng thái của miếng bọt biển khi thực hiện hướng dẫn này, và do đó nó cần thiết để thực hiện các ràng buộc.

Hạn chế:

 mds(sbox(old_sponge) + user_opcode(7bits) + op_value(push_flag=1)) == sbox(inv_mds(new_sponge))

Phán đoán điều kiện

có khuynh hướng

Là ràng buộc của nhánh thực sự kết thúc của if, nó được chia thành hai phần:
Ràng buộc 1: là ràng buộc của trạng thái bọt biển.

Giá trị ở đầu ngăn xếp bằng new_sponge_0. Miếng bọt biển sau lần thực thi cuối cùng của nhánh true của if bằng new_sponge_1. New_sponge_3 bằng 0.

Ràng buộc 2: là ràng buộc của ctx_stack. Giá trị ở đầu ngăn xếp bằng new_sponge_0. Bất kỳ phần tử nào khác trong ngăn xếp sẽ di chuyển theo một vị trí lên trên cùng của ngăn xếp.

Ràng buộc 3: là ràng buộc của loop_stack. Trạng thái của loop_stack là không thay đổi.

Hạn chế:

 parent_hash = current.ctx_stack()[0] block_hash = current.op_sponge()[0] new_sponge = next.op_sponge() parent_hash == new_sponge[0] block_hash == new_sponge[1] new_sponge[3] == 0 // make parent hash was popped from context stack ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 is for loop image constraint ctx_stack_end = ctx_stack_start + ctx_stack_current.len() ctx_result = &mut result[ctx_stack_start..ctx_stack_end] ctx_stack_current_0 = ctx_stack_next_1 ctx_stack_current_1 = ctx_stack_next_2 ... ctx_stack_current_n = ctx_stack_next_n+1 // loop_stack copy copy range: ctx_stack_end to. ctx_stack_end + loop_stack_current.len() loop_stack_current_0 = loop_stack_next_0 ... loop_stack_current_n = loop_stack_next_n

f_end

Là ràng buộc của nhánh false kết thúc của if, nó được chia thành hai phần:
Ràng buộc 1: là ràng buộc của trạng thái bọt biển. Giá trị ở đầu ngăn xếp bằng new_sponge_0.

Miếng bọt biển sau lần thực thi cuối cùng của nhánh true của if bằng new_sponge_2. new_sponge_3 bằng 0.

Ràng buộc 2: là ràng buộc của ctx_stack. Giá trị ở đầu ngăn xếp bằng new_sponge_0. Bất kỳ phần tử nào khác trong ngăn xếp sẽ di chuyển theo một vị trí lên trên cùng của ngăn xếp.

Ràng buộc 3: là ràng buộc của loop_stack. Trạng thái của loop_stack là không thay đổi.

Hạn chế:

 parent_hash = current.ctx_stack()[0] block_hash = current.op_sponge()[0] new_sponge = next.op_sponge() parent_hash == new_sponge[0] block_hash == new_sponge[2] new_sponge[3] == 0 // make parent hash was popped from context stack ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 is for loop image constraint ctx_stack_end = ctx_stack_start + ctx_stack_current.len() ctx_result = &mut result[ctx_stack_start..ctx_stack_end] ctx_stack_current_0 = ctx_stack_next_1 ctx_stack_current_1 = ctx_stack_next_2 ... ctx_stack_current_n = ctx_stack_next_n+1 // loop_stack copy copy range: ctx_stack_end to. ctx_stack_end + loop_stack_current.len() loop_stack_current_0 = loop_stack_next_0 ... loop_stack_current_n = loop_stack_next_n