Xác minh chính thức của zk-SNARK: Phương pháp chứng minh bộ nhớ

Khi thực hiện xác minh chính thức cho hệ thống zk-SNARK, việc xử lý của hệ thống con bộ nhớ là một thách thức quan trọng. Khác với máy ảo truyền thống, zkVM sử dụng bảng thực thi và bảng phụ để biểu diễn trạng thái bộ nhớ, điều này cần những phương pháp xác minh đặc biệt.

Hệ thống bộ nhớ của zkWasm bao gồm bảng thực thi và bảng bộ nhớ. Bảng thực thi ghi lại quá trình thực hiện lệnh, trong khi bảng bộ nhớ lưu giữ tất cả lịch sử truy cập bộ nhớ. Để đơn giản hóa việc phát triển, zkWasm cung cấp một lớp trừu tượng, thông qua hai hàm alloc_memory_table_lookup_write_cell và alloc_memory_table_lookup_read_cell để thao tác bộ nhớ.

Trong quá trình xác minh, chúng tôi coi bảng bộ nhớ là một cấu trúc dữ liệu có thể thay đổi, thông qua hàm memory_at để xây dựng ánh xạ dữ liệu địa chỉ. Điều này cho phép chứng minh rằng các ràng buộc do hàm alloc tạo ra tương đương với các thao tác set và get trên ánh xạ, do đó làm cho việc xác minh lệnh trở nên đơn giản hơn với hình thức giống như trình thông dịch không ZK.

Để ngăn chặn kẻ tấn công thao túng bảng bộ nhớ, zkWasm áp dụng cơ chế đếm để theo dõi số lượng mục hợp lệ. Bảng thực thi và bảng bộ nhớ lần lượt duy trì bộ đếm, thông qua các ràng buộc để đảm bảo cả hai nhất quán. Điều này yêu cầu xác minh chính xác hơn, cần chứng minh rằng mỗi lệnh tương ứng với số lượng mục bảng bộ nhớ đúng.

Quá trình xác minh được thực hiện theo cách từ trên xuống dưới, bao gồm ba bước:

1. Số lượng mục dự kiến mà lệnh nên tạo
2. Số mục trong bảng chứng minh không nhiều hơn dự kiến
3. Chứng minh rằng cum_mops và instructions_mops luôn nhất quán trong bảng bằng cách sử dụng phương pháp quy nạp.

Phương pháp xác minh chi tiết này giúp phát hiện các lỗi tiềm ẩn, chẳng hạn như một vấn đề quan trọng trong cơ chế đếm bảng nhảy.

Để thực hiện xác minh mô-đun, chúng tôi chia hệ thống thành ba phần độc lập: xác minh mạch lệnh, xác minh bảng thực thi và triển khai bảng bộ nhớ. Cấu trúc này cho phép nhiều kỹ sư làm việc song song, nâng cao hiệu quả xác minh.

Tổng thể, mặc dù zkVM có sự khác biệt trong việc xử lý trạng thái động, nhưng thông qua việc khớp các lớp trừu tượng trong triển khai, có thể áp dụng phương pháp mô-đun tương tự như xác minh trình thông dịch truyền thống. Phương pháp này tối đa hóa việc giảm thiểu ảnh hưởng do sự khác biệt mang lại, cho phép mỗi lệnh được xác minh độc lập dựa trên giao diện get-set.