Hệ thống bằng chứng rõ ràng của Miden

Sin7y

特邀专栏作者

2022-10-11 08:38

Bài viết này có khoảng 2722 từ, đọc toàn bộ bài viết mất khoảng 4 phút

Bài báo này xây dựng kiến trúc hệ thống bằng chứng miden một cách chi tiết.

tiêu đề cấp đầu tiên

Kiến trúc hệ thống bằng chứng Miden

miden là một triển khai zkvm dựa trên công nghệ strak. Lớp dưới cùng của nó dựa trên thư viện zkp của winterfell để tạo bằng chứng rõ ràng và xác minh bằng chứng. Đường chấm chấm trong Hình 1 bên dưới là chức năng chính do Miden thực hiện. Có thể thấy rằng chủ yếu có ba thành phần.

1. Bộ trình biên dịch ngữ pháp từ vựng, trình phân tích từ vựng và trình phân tích cú pháp trong Hình 1 dưới đây. Họ có thể lập trình các lệnh hợp ngữ được xác định bởi miden thành opcode và giá trị op chứa trong codeblock và block.

3. Một tập hợp AIR (Biểu diễn trung gian đại số) đáp ứng các yêu cầu chứng minh rõ ràng, AIR trong Hình 1 bên dưới. Nó được sử dụng để hạn chế quá trình thực thi của máy ảo của miden.

tiêu đề cấp đầu tiên

thiết kế cấu trúc AIR

Các ràng buộc của AIR được chia thành hai phần: ngăn xếp và bộ giải mã:

Hình 3 cho thấy các ràng buộc của bộ giải mã. Trong số đó, op_count, op_sponge, cf_op_bits, ld_op_bits, hd_op_bits là những cột có độ dài cố định. Trong số đó, op_sponge được sử dụng để hạn chế thứ tự và tính đúng đắn của việc thực hiện các lệnh. cf_op_bits ràng buộc 3bit flow_ops. ld_op_bits, hd_op_bits lần lượt hạn chế 5 bit thấp và 2 bit cao của user_ops. Sự kết hợp của ld_op_bits và hd_op_bits tạo thành một user_op được thực thi và cũng được sử dụng làm bộ chọn cho từng ràng buộc trạng thái bước của ngăn xếp.

tiêu đề cấp đầu tiên

Phiên bản quy trình thực thi Miden VM

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

Đoạn mã 1 dưới đây là đoạn mã sẽ được thực thi:

Logic mà nó thực thi là đẩy 3 và 5 vào ngăn xếp. Sau đó đọc cờ từ băng. Xác định xem cờ là 1 hay 0. Nếu là 1, hãy chạy nhánh if.true để lấy ra hai số 3 và 5 đã được đẩy vào ngăn xếp, cộng chúng lại với nhau để được 8 và đẩy lại vào ngăn xếp. Nếu nó là 0, hãy chạy nhánh khác để lấy ra hai số 3 và 5 đã được đẩy vào ngăn xếp và nhân chúng để có 15, sau đó đẩy 15 trở lại ngăn xếp.

Đoạn mã lệnh cuối cùng sau khi đoạn mã được phân tích cú pháp bởi bộ phân tích từ vựng và ngữ pháp của miden như sau Đoạn mã 2:

Hình 4 dưới đây cho thấy quá trình vm chạy đoạn mã 2. Ở giữa là lưu đồ của bộ thực thi thực thi opcode. Đường chấm chấm bên trái chỉ dấu vết bộ giải mã được tạo bởi quá trình thực thi mã và đường chấm chấm bên phải chỉ đến dấu vết ngăn xếp được tạo bởi quá trình thực thi mã.

Trong số đó, bộ thực thi được thực hiện từng cái một theo khối mã. Trong ví dụ này, khối span được thực hiện trước. Sau đó thực hiện cấu trúc if-else-end ở bước 32 để vào khối swtich và đẩy hàm băm miếng bọt biển được tạo bởi bước cuối cùng của khối span trước đó vào ctx_stack và sau khi khối swtich được thực thi, ở bước 49, hãy bật vào bọt biển.

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 dự án miden. Hiện tại, nhánh tiếp theo của miden đã thiết kế lại rất nhiều hướng dẫn và AIR chỉ thực hiện một phần nhỏ của các ràng buộc.

ràng buộc ngăn xếp

hướng dẫn có điều kiện

Choose

Constrain:

chữ

add

Constrain:

mul

Constrain:

inv

Constrain:

neg

Constrain:

chỉ thị boolean

not

Constrain:

and

Constrain:

lệnh băm

RESCR

chữ

Chiếm 6 thanh ghi

Constrain:

hướng dẫn so sánh

Constrain:

cmp

chữ

A: [0,1,0,1]

B: [0,0,1,1]

Cần so sánh 4 lần

Constrain:

chữ

dup.n

Constrain:

swap

Constrain:

ROLL4

Constrain:

tiêu đề cấp đầu tiên

ràng buộc bộ giải mã

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

op_bits

chữ

Các ràng buộc đối với cf_op_bits, ld_op_bits, 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_count không phải là 0, ld_ops và hd_ops không được đồng thời là 0.

Ràng buộc 3: Khi cf_op_bits bị hacc. Trạng thái op_counter sẽ được tăng thêm 1.

Ràng buộc 4: Các lệnh BEGIN, LOOP, BREAK và WRAP yêu cầu 16 căn chỉnh

Ràng buộc 6: Lệnh PUSH yêu cầu căn chỉnh 8

hacc

hacc được sử dụng làm flowOps, mỗi lần thực hiện lệnh này sẽ khiến trạng thái của miếng bọt biển thay đổi, trạng thái này cần được hạn chế

bản án có điều kiện

t_end

chữ

Ràng buộc là phần cuối của nhánh thực của if được chia thành hai phần:

Ràng buộc 1: Ràng buộc của trạng thái miếng bọt biển, giá trị ở đầu ngăn xếp bật lên bằng new_sponge_0. Miếng bọt biển sau khi thực hiện bước cuối cùng của nhánh thực của if bằng new_sponge_1. new_sponge_3 bằng 0.

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

f_end

chữ

Là ràng buộc ở cuối nhánh sai của if, nó được chia thành hai phần:

Sin7y được thành lập vào năm 2021 và bao gồm các nhà phát triển chuỗi khối hàng đầu. Chúng tôi vừa là vườn ươm dự án vừa là nhóm nghiên cứu công nghệ chuỗi khối, khám phá các công nghệ tiên tiến và quan trọng nhất như EVM, Layer2, chuỗi chéo, điện toán bảo mật và các giải pháp thanh toán tự động.