Trong loạt blog này về xác minh chính thức nâng cao đối với bằng chứng không có kiến thức , chúng tôi đã thảo luận về cách xác minh hướng dẫn ZK và cung cấp cái nhìn sâu sắc về hai lỗ hổng ZK . Bằng cách xác minh chính thức mọi hướng dẫn zkWasm, chúng tôi đã tìm thấy và khắc phục mọi lỗ hổng, cho phép chúng tôi xác minh đầy đủ tính an toàn và chính xác về mặt kỹ thuật của toàn bộ mạch zkWasm, như được hiển thị trong các báo cáo công khai và cơ sở mã .
Mặc dù chúng tôi đã trình diễn quy trình xác minh hướng dẫn zkWasm và giới thiệu các khái niệm sơ bộ của dự án liên quan, nhưng những độc giả quen thuộc với xác minh chính thức có thể quan tâm hơn đến việc tìm hiểu xác minh zkVM với các hệ thống ZK nhỏ hơn khác hoặc các loại máy ảo mã byte khác. TRÊN. Trong bài viết này, chúng tôi sẽ thảo luận sâu về một số điểm kỹ thuật gặp phải khi xác thực hệ thống con bộ nhớ zkWasm. Bộ nhớ là phần độc đáo nhất của zkVM và việc xử lý phần này rất quan trọng đối với tất cả các xác thực zkVM khác.
Xác minh chính thức: máy ảo (VM) so với máy ảo ZK (zkVM)
Mục tiêu cuối cùng của chúng tôi là xác minh tính đúng đắn của zkWasm, tương tự như định lý về tính đúng đắn của các trình thông dịch mã byte thông thường (VM, chẳng hạn như trình thông dịch EVM được các nút Ethereum sử dụng). Nghĩa là, mỗi bước thực hiện của trình thông dịch tương ứng với một bước pháp lý dựa trên ngữ nghĩa hoạt động của ngôn ngữ. Như được hiển thị trong hình bên dưới, nếu trạng thái hiện tại của cấu trúc dữ liệu của trình thông dịch mã byte là SL và trạng thái này được đánh dấu là trạng thái SH trong đặc tả cấp cao của máy Wasm, thì khi trình thông dịch chuyển sang trạng thái SL, ở đó phải là trạng thái cấp cao hợp pháp tương ứng SH và đặc tả Wasm quy định SH phải bước tới SH.
Tương tự, zkVM có định lý về tính đúng đắn tương tự: mỗi hàng mới trong bảng thực thi zkWasm tương ứng với một bước pháp lý dựa trên ngữ nghĩa hoạt động của ngôn ngữ. Như được hiển thị trong hình bên dưới, nếu trạng thái hiện tại của một hàng cấu trúc dữ liệu trong bảng thực thi là SR và trạng thái này được biểu thị dưới dạng trạng thái SH trong đặc tả cấp cao của máy Wasm, thì trạng thái SR của hàng tiếp theo trong bảng thực thi phải tương ứng với trạng thái cấp cao SH và đặc tả Wasm quy định SH phải bước tới SH.
Theo đó, đặc điểm kỹ thuật của các trạng thái cấp cao và các bước Wasm nhất quán cho dù trong VM hay zkVM và do đó có thể rút ra kinh nghiệm xác minh trước đó với trình thông dịch hoặc trình biên dịch ngôn ngữ lập trình. Điều làm cho việc xác minh zkVM trở nên đặc biệt là loại cấu trúc dữ liệu tạo nên trạng thái cấp thấp của hệ thống.
Đầu tiên, như chúng tôi đã nêu trong bài đăng trên blog trước đó , bộ chứng minh zk về cơ bản là một phép toán số nguyên theo modulo các số nguyên tố lớn, trong khi đặc tả Wasm và trình thông dịch thông thường xử lý các số nguyên 32 bit hoặc 64 bit. Hầu hết việc triển khai zkVM đều liên quan đến điều này, vì vậy việc xử lý tương ứng cũng cần được thực hiện trong quá trình xác minh. Tuy nhiên, đây là vấn đề cục bộ: mỗi dòng mã trở nên phức tạp hơn do các phép toán số học cần xử lý, nhưng cấu trúc tổng thể của mã và cách chứng minh không thay đổi.
Một điểm khác biệt lớn nữa là cách xử lý cấu trúc dữ liệu có kích thước động. Trong trình thông dịch mã byte thông thường, bộ nhớ, ngăn xếp dữ liệu và ngăn xếp lệnh gọi đều được triển khai dưới dạng cấu trúc dữ liệu có thể thay đổi. Tương tự, đặc tả Wasm biểu thị bộ nhớ dưới dạng kiểu dữ liệu với các phương thức get/set. Ví dụ: trình thông dịch EVM của Geth có kiểu dữ liệu `Bộ nhớ`, được triển khai dưới dạng mảng byte biểu thị bộ nhớ vật lý và được ghi vào cũng như đọc qua các phương thức `Set 32` và `GetPtr`. Để thực hiện lệnh lưu trữ bộ nhớ , Geth gọi `Set 32` để sửa đổi bộ nhớ vật lý.
func opMstore(pc *uint 64, trình thông dịch *EVMInterpreter, phạm vi *ScopeContext) ([]byte, error) {
// giá trị pop của ngăn xếp
mStart, val := phạm vi.Stack.pop(), phạm vi.Stack.pop()
phạm vi.Memory.Set 32(mStart.Uint 64(), val)
trả về con số không, con số không
}
Trong bằng chứng về tính chính xác ở trên của trình thông dịch, chúng tôi đã chứng minh rằng trạng thái cấp cao và trạng thái cấp thấp của nó khớp với nhau sau khi gán giá trị cho bộ nhớ cụ thể trong trình thông dịch và bộ nhớ trừu tượng trong đặc tả. Điều này tương đối dễ dàng.
Tuy nhiên, với zkVM, mọi thứ trở nên phức tạp hơn.
Bảng bộ nhớ và lớp trừu tượng bộ nhớ của zkWasm
Trong zkVM, có các cột trên bảng thực thi dành cho dữ liệu có kích thước cố định (tương tự như các thanh ghi trong CPU), nhưng nó không thể được sử dụng để xử lý các cấu trúc dữ liệu có kích thước động, được triển khai bằng cách tra cứu các bảng phụ. Bảng thực thi của zkWasm có một cột EID, có các giá trị là 1, 2, 3... và có hai bảng phụ trợ là bảng bộ nhớ và bảng nhảy, được sử dụng để biểu thị dữ liệu bộ nhớ và ngăn xếp cuộc gọi tương ứng.
Sau đây là ví dụ về cách triển khai chương trình rút tiền:
số dư int, số tiền;
khoảng trống chính () {
số dư = 100;
số tiền = 10;
số dư -= số tiền; // rút
}
Nội dung và cấu trúc của bảng thực hiện khá đơn giản. Nó có 6 bước thực thi (EID từ 1 đến 6), mỗi bước có một dòng liệt kê mã hoạt động của nó và nếu lệnh là đọc hoặc ghi bộ nhớ thì địa chỉ và dữ liệu của nó:
Mỗi hàng trong bảng bộ nhớ chứa địa chỉ, dữ liệu, EID bắt đầu và EID kết thúc. EID bắt đầu là EID của bước thực hiện ghi dữ liệu này vào địa chỉ này và EID kết thúc là EID của bước thực hiện tiếp theo sẽ ghi địa chỉ này. (Nó cũng chứa một số đếm mà chúng ta sẽ thảo luận chi tiết sau.) Đối với mạch lệnh đọc bộ nhớ Wasm, nó sử dụng một ràng buộc tra cứu để đảm bảo rằng có một mục thích hợp trong bảng sao cho EID của lệnh đọc nằm trong phạm vi từ đầu đến cuối Bên trong. (Tương tự, mỗi hàng của bảng nhảy tương ứng với một khung của ngăn xếp cuộc gọi và mỗi hàng được gắn nhãn EID của bước hướng dẫn cuộc gọi đã tạo ra nó.)
Hệ thống bộ nhớ này khác biệt đáng kể so với trình thông dịch VM thông thường: thay vì bộ nhớ có thể thay đổi được cập nhật tăng dần, bảng bộ nhớ chứa lịch sử của tất cả các lần truy cập bộ nhớ trong suốt quá trình theo dõi thực thi. Để đơn giản hóa công việc của lập trình viên, zkWasm cung cấp một lớp trừu tượng được triển khai thông qua hai hàm nhập thuận tiện. Họ đang:
alloc_memory_table_lookup_write_cell
Và
Alloc_memory_table_lookup_read_cell
Các thông số của nó như sau:
Ví dụ: mã triển khai các hướng dẫn lưu trữ bộ nhớ trong zkWasm chứa lệnh gọi hàm write alloc:
hãy để bộ nhớ_table_lookup_heap_write1 = bộ cấp phát
.alloc_memory_table_lookup_write_cell_with_value(
lưu trữ ghi res 1,
hạn chế_builder,
eid,
di chuyển |____| constant_from!(LocationType::Heap as u 64),
di chuyển |meta| Load_block_index.expr(meta), // địa chỉ
di chuyển |____| hằng_from!(0), // là 32-bit
di chuyển |____| hằng_from!( 1), // (luôn luôn) bật
);
hãy store_value_in_heap1 = bộ nhớ_table_lookup_heap_write1.value_cell;
Hàm `alloc` chịu trách nhiệm xử lý các ràng buộc tra cứu giữa các bảng và các ràng buộc số học liên quan đến `eid` hiện tại với các mục trong bảng bộ nhớ. Từ đó, các lập trình viên có thể coi các bảng này như bộ nhớ thông thường và giá trị của `store_value_in_heap1` đã được gán cho địa chỉ `load_block_index` sau khi mã được thực thi.
Tương tự, hướng dẫn đọc bộ nhớ được triển khai bằng hàm `read_alloc`. Trong trình tự thực thi ví dụ ở trên, có một ràng buộc đọc cho mỗi lệnh tải và một ràng buộc ghi cho mỗi lệnh lưu trữ, và mỗi ràng buộc được thỏa mãn bởi một mục trong bảng bộ nhớ.
mtable_lookup_write(hàng 1.eid, hàng 1.store_addr, hàng 1.store_value)
⇐ (hàng 1.eid= 1 ∧ hàng 1.store_addr=balance ∧ hàng 1.store_value= 100 ∧ ...)
mtable_lookup_write(hàng 2.eid, hàng 2.store_addr, hàng 2.store_value)
⇐ (hàng 2.eid= 2 ∧ hàng 2.store_addr=số tiền ∧ hàng 2.store_value= 10 ∧ ...)
mtable_lookup_read(hàng 3.eid, hàng 3.load_addr, hàng 3.load_value)
⇐ ( 2<hàng 3.eid≤ 6 ∧ hàng 3.load_addr=số tiền ∧ hàng 3.load_value= 100 ∧ ...)
mtable_lookup_read(hàng 4.eid, hàng 4.load_addr, hàng 4.load_value)
⇐ ( 1<hàng 4.eid≤ 6 ∧ hàng 4.load_addr=balance ∧ hàng 4.load_value= 10 ∧ ...)
mtable_lookup_write(hàng 6.eid, hàng 6.store_addr, hàng 6.store_value)
⇐ (hàng 6.eid= 6 ∧ hàng 6.store_addr=balance ∧ hàng 6.store_value= 90 ∧ ...)
Cấu trúc của xác minh chính thức phải tương ứng với các khái niệm trừu tượng được sử dụng trong phần mềm đang được xác minh, để bằng chứng có thể tuân theo logic tương tự như mã. Đối với zkWasm, điều này có nghĩa là chúng ta cần xác minh mạch bảng bộ nhớ và các chức năng phân bổ ô đọc/ghi dưới dạng một mô-đun, có giao diện giống như một bộ nhớ biến đổi. Với giao diện như vậy, việc xác minh từng mạch lệnh có thể được thực hiện theo cách tương tự như trình thông dịch thông thường, trong khi độ phức tạp ZK bổ sung được gói gọn trong mô-đun hệ thống con bộ nhớ.
Trong quá trình xác minh, chúng tôi đã triển khai ý tưởng rằng bảng bộ nhớ thực sự có thể được coi là cấu trúc dữ liệu có thể thay đổi. Tức là viết hàm `memory_at type`, quét toàn bộ bảng bộ nhớ và xây dựng ánh xạ dữ liệu địa chỉ tương ứng. (Phạm vi giá trị của biến `type` ở đây là ba loại dữ liệu bộ nhớ Wasm khác nhau: heap, data stack và biến toàn cục.) Sau đó, chúng tôi chứng minh rằng các ràng buộc bộ nhớ do hàm cấp phát tạo ra tương đương với việc sử dụng set và get thay đổi dữ liệu được thực hiện bởi ánh xạ dữ liệu địa chỉ tương ứng. Chúng ta có thể chứng minh:
Đối với mỗi eid, nếu các ràng buộc sau được giữ nguyên
giá trị bù loại bộ nhớ_table_lookup_read_cell eid
Nhưng
get (memory_at eid type) offset = Một số giá trị
Và, nếu các ràng buộc sau giữ nguyên
giá trị bù loại bộ nhớ_table_lookup_write_cell eid
Nhưng
bộ nhớ_at (eid+ 1) loại = set (bộ nhớ_at loại eid) giá trị bù đắp
Sau đó, việc xác minh từng lệnh có thể dựa trên các thao tác nhận và đặt trên bản đồ dữ liệu địa chỉ, tương tự như các trình thông dịch mã byte không phải ZK.
Cơ chế đếm ghi vào bộ nhớ của zkWasm
Tuy nhiên, mô tả đơn giản ở trên không tiết lộ tất cả nội dung của bảng bộ nhớ và bảng nhảy. Trong khung zkVM, những bảng này có thể bị kẻ tấn công thao túng, những kẻ này có thể dễ dàng thao túng các hướng dẫn tải bộ nhớ để trả về các giá trị tùy ý bằng cách chèn một hàng dữ liệu.
Lấy chương trình rút tiền làm ví dụ, kẻ tấn công có cơ hội đưa dữ liệu sai vào số dư tài khoản bằng cách giả mạo hoạt động ghi bộ nhớ 110 USD trước hoạt động rút tiền. Quá trình này có thể đạt được bằng cách thêm một hàng dữ liệu vào bảng bộ nhớ và sửa đổi giá trị của các ô hiện có trong bảng bộ nhớ và bảng thực thi. Điều này sẽ dẫn đến việc rút tiền miễn phí vì số dư tài khoản sẽ vẫn ở mức 100 USD sau hoạt động.
Để đảm bảo rằng bảng bộ nhớ (và bảng nhảy) chỉ chứa các mục nhập hợp lệ được tạo bởi các lệnh ghi (gọi và trả về) bộ nhớ được thực thi thực sự, zkWasm sử dụng một cơ chế đếm đặc biệt để theo dõi số lượng mục nhập. Cụ thể, bảng bộ nhớ có một cột chuyên dụng để theo dõi tổng số mục được ghi vào bộ nhớ. Đồng thời, bảng thực thi còn chứa bộ đếm để đếm số thao tác ghi bộ nhớ dự kiến cho mỗi lệnh. Đảm bảo hai số đếm nhất quán bằng cách đặt ràng buộc đẳng thức. Logic của phương pháp này rất trực quan: mỗi khi thực hiện thao tác ghi vào bộ nhớ, nó sẽ được tính một lần và phải có một bản ghi tương ứng trong bảng bộ nhớ. Do đó, kẻ tấn công không thể chèn bất kỳ mục bổ sung nào vào bảng bộ nhớ.
Tuyên bố hợp lý ở trên hơi mơ hồ và trong quá trình chứng minh cơ giới hóa, nó cần phải được thực hiện chính xác hơn. Đầu tiên, chúng ta cần xem lại phát biểu của bổ đề ghi nhớ đã đề cập ở trên. Chúng tôi xác định hàm `mops_at eid type` để đếm các mục trong bảng bộ nhớ với `eid` và `type` nhất định (hầu hết các hướng dẫn sẽ tạo 0 hoặc 1 mục tại một eid`). Phát biểu đầy đủ của định lý có một điều kiện tiên quyết bổ sung nêu rõ rằng không có mục nào trong bảng bộ nhớ giả:
Nếu các ràng buộc sau giữ nguyên
(giá trị bù loại eid của bộ nhớ_table_lookup_write_cell)
Và những ràng buộc mới sau đây được thiết lập
(loại mops_at eid) = 1
Nhưng
(loại bộ nhớ_at(eid+ 1)) = đặt giá trị bù (loại bộ nhớ_at eid)
Điều này yêu cầu xác minh của chúng tôi phải chính xác hơn trường hợp trước. Chỉ xuất phát từ ràng buộc đẳng thức rằng tổng số mục trong bảng bộ nhớ bằng tổng số lần ghi bộ nhớ trong quá trình thực thi là không đủ để hoàn thành việc xác minh. Để chứng minh tính đúng đắn của một lệnh, chúng ta cần biết rằng mỗi lệnh tương ứng với đúng số mục trong bảng bộ nhớ. Ví dụ: chúng ta cần loại trừ liệu kẻ tấn công có thể bỏ qua một mục trong bảng bộ nhớ cho một lệnh trong chuỗi thực thi và tạo một mục trong bảng bộ nhớ mới độc hại cho một lệnh khác không liên quan hay không.
Để chứng minh điều này, chúng tôi sử dụng cách tiếp cận từ trên xuống để giới hạn số lượng mục trong bảng bộ nhớ tương ứng với một lệnh nhất định, bao gồm ba bước. Đầu tiên, chúng tôi ước tính số lượng mục cần được tạo cho các lệnh trong trình tự thực hiện dựa trên loại lệnh. Chúng tôi gọi số lần ghi dự kiến từ bước thứ i đến khi kết thúc thực thi là `guides_mops i` và số mục nhập tương ứng trong bảng bộ nhớ từ lệnh thứ i đến khi kết thúc thực thi là `cum_mops (eid i)`. Bằng cách phân tích các ràng buộc tìm kiếm của từng lệnh, chúng tôi có thể chứng minh rằng nó tạo ra không ít mục nhập hơn mong đợi và do đó chúng tôi có thể kết luận rằng mỗi phân đoạn [i... numRows] được theo dõi tạo ra không ít mục nhập hơn mong đợi:
Bổ đề cum_mops_bound: forall ni,
0 ≤ tôi ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≥guides_mops i n.
Thứ hai, nếu bạn có thể chỉ ra rằng bảng không có nhiều mục hơn dự kiến, thì nó có đúng số mục, đó là điều hiển nhiên.
Bổ đề cum_mops_equal : forall ni,
0 ≤ tôi ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) upguides_mops trong ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) =guides_mops i n.
Bây giờ tiến hành bước ba. Định lý về tính đúng đắn của chúng tôi phát biểu rằng với mọi n, cum_mops vàguides_mops luôn nhất quán từ hàng n đến cuối bảng:
Bổ đề cum_mops_equal : forall n,
0 <= Z.of_nat n < etable_numRow ->
MTable.cum_mops (etable_values eid_cell (Z.of_nat n)) (max_eid+ 1) =guides_mops (Z.of_nat n)
Việc xác minh được thực hiện bằng cách tóm tắt n. Hàng đầu tiên trong bảng là ràng buộc đẳng thức của zkWasm, cho biết tổng số mục trong bảng bộ nhớ là chính xác, tức là cum_mops 0 =guides_mops 0 . Đối với các dòng sau, giả thuyết quy nạp cho chúng ta biết:
cum_mops n = hướng dẫn_mops n
và chúng tôi hy vọng chứng minh được
cum_mops (n+ 1) = hướng dẫn_mops (n+ 1)
Hãy chú ý ở đây
cum_mops n = mop_at n + cum_mops (n+ 1)
Và
hướng dẫn_mops n = hướng dẫn_mops n + hướng dẫn_mops (n+ 1)
Vì vậy, chúng ta có thể nhận được
mops_at n + cum_mops (n+ 1) =guide_mops n +guide_mops (n+ 1)
Trước đây, chúng tôi đã chỉ ra rằng mỗi lệnh sẽ tạo ra không ít hơn số lượng mục nhập dự kiến, ví dụ:
mops_at n ≥ hướng dẫn_mops n.
Vậy có thể kết luận
cum_mops (n+ 1) struct_mops (n+ 1)
Ở đây chúng ta cần áp dụng bổ đề thứ hai ở trên.
(Sử dụng bổ đề tương tự để xác minh bảng nhảy, có thể chứng minh rằng mỗi lệnh gọi có thể tạo ra một mục nhập bảng nhảy một cách chính xác, vì vậy kỹ thuật chứng minh này thường có thể áp dụng được. Tuy nhiên, chúng tôi vẫn cần xác minh thêm để chứng minh rằng tính đúng đắn của kết quả trả về lệnh. Eid được trả về khác với eid của lệnh gọi đã tạo khung lệnh gọi, vì vậy chúng ta cũng cần một thuộc tính bất biến bổ sung để khai báo rằng giá trị eid được tăng theo một hướng trong suốt chuỗi thực thi.)
Việc mô tả quy trình chứng minh một cách chi tiết như vậy là điển hình của việc xác minh chính thức và là lý do tại sao việc xác minh một đoạn mã cụ thể thường mất nhiều thời gian hơn việc viết nó. Nhưng nó có đáng không? Trong trường hợp này, nó đáng giá vì chúng tôi đã tìm thấy một lỗi nghiêm trọng trong cơ chế đếm bảng nhảy trong quá trình chứng minh. Lỗi này đã được mô tả chi tiết trong bài viết trước - tóm lại, các phiên bản mã cũ hơn chiếm cả lệnh gọi và lệnh trả lại, và kẻ tấn công có thể tạo bước nhảy giả bằng cách thêm các lệnh trả về bổ sung vào trình tự thực thi. . Mặc dù cơ chế đếm không chính xác có thể thỏa mãn trực giác rằng mọi lệnh gọi và trả về đều được tính, nhưng vấn đề nảy sinh khi chúng ta cố gắng tinh chỉnh trực giác này thành một phát biểu định lý chính xác hơn.
Làm cho quá trình chứng minh trở thành mô-đun
Từ phần thảo luận ở trên, chúng ta có thể thấy rằng có một sự phụ thuộc vòng tròn giữa bằng chứng về mạch của mỗi lệnh và bằng chứng về cột đếm của bảng thực thi. Để chứng minh tính đúng đắn của mạch lệnh, chúng ta cần suy luận về bộ nhớ ghi trong đó; nghĩa là chúng ta cần biết số lượng mục trong bảng bộ nhớ tại một EID cụ thể và chúng ta cần chứng minh rằng thao tác ghi bộ nhớ được tính trong đó. bảng thực thi là chính xác; và điều này cũng cần phải chứng minh rằng mỗi lệnh thực hiện ít nhất một số lần ghi bộ nhớ tối thiểu.
Ngoài ra, còn một yếu tố khác cần xem xét. Dự án zkWasm khá lớn nên công việc xác minh cần phải được mô-đun hóa để nhiều kỹ sư xác minh có thể phân chia công việc. Vì vậy, cần đặc biệt chú ý đến độ phức tạp của nó khi giải cấu trúc chứng minh cơ chế đếm. Ví dụ: đối với lệnh LocalGet, có hai định lý như sau:
Định lý opcode_mops_Corr_local_get : cho tất cả tôi,
0 <= tôi ->
etable_values eid_cell i > 0 ->
opcode_mops_ Correct LocalGet i.
Định lý LocalGetOp_core : forall i s y xs,
0 <= tôi ->
etable_values enabled_cell i = 1 ->
mops_at_chính xác tôi ->
etable_values (ops_cell LocalGet) i = 1 ->
state_rel và st ->
wasm_stack st = xs ->
(etable_values offset_cell i) > 1 ->
nth_error xs (Z.to_nat (etable_values offset_cell i - 1)) = Một số y ->
state_rel (i+ 1) (update_stack (incr_iid st) (y::xs)).
Phát biểu định lý đầu tiên
opcode_mops_core LocalGet i
Khi được mở rộng, điều này có nghĩa là lệnh tạo ra ít nhất một mục nhập bảng bộ nhớ ở dòng i (số 1 được chỉ định trong đặc tả mã opcode LocalGet của zkWasm).
Định lý thứ hai là định lý về tính đúng đắn hoàn chỉnh cho lệnh, trong đó trích dẫn
giẻ lau_at_chính xác tôi
Theo giả thuyết, điều này có nghĩa là lệnh tạo chính xác một mục trong bảng bộ nhớ.
Kỹ sư xác minh có thể chứng minh hai định lý này một cách độc lập và sau đó kết hợp chúng với chứng minh về bảng thực thi để chứng minh tính đúng đắn của toàn bộ hệ thống. Điều đáng lưu ý là tất cả các bằng chứng cho các hướng dẫn riêng lẻ có thể được thực hiện ở mức độ ràng buộc đọc/ghi mà không cần biết cách triển khai cụ thể của bảng bộ nhớ. Do đó, dự án được chia thành ba phần có thể được xử lý độc lập.
Tóm tắt
Việc xác minh các mạch cho từng dòng zkVM về cơ bản không khác biệt so với việc xác minh các ứng dụng ZK trong các miền khác, vì cả hai đều yêu cầu lý luận tương tự về các ràng buộc số học. Ở cấp độ cao, việc xác minh zkVM yêu cầu nhiều phương pháp xác minh chính thức tương tự được sử dụng cho trình thông dịch và trình biên dịch ngôn ngữ lập trình. Sự khác biệt chính ở đây là trạng thái máy ảo có kích thước động. Tuy nhiên, tác động của những khác biệt này có thể được giảm thiểu bằng cách cấu trúc cấu trúc xác minh một cách cẩn thận để phù hợp với lớp trừu tượng được sử dụng trong quá trình triển khai, cho phép mỗi lệnh trở thành một mô-đun độc lập dựa trên giao diện get-set như đối với xác minh hóa học của trình thông dịch thông thường.
