在關(guān)于零知識(shí)證明的先進(jìn)形式化驗(yàn)證的系列博客中，我們已經(jīng)討論了如何驗(yàn)證 ZK 指令以及對(duì)兩個(gè) ZK 漏洞的深度剖析。正如在公開(kāi)報(bào)告和代碼庫(kù)中所顯示的，通過(guò)形式化驗(yàn)證每一條 zkWasm 指令，我們找到并修復(fù)了每一個(gè)漏洞，從而能夠完全驗(yàn)證整個(gè) zkWasm 電路的技術(shù)安全性和正確性。
盡管我們已展示了驗(yàn)證一條 zkWasm 指令的過(guò)程，并介紹了相關(guān)的項(xiàng)目初步概念，但熟悉形式化驗(yàn)證讀者可能更想了解 zkVM 與其他較小的 ZK 系統(tǒng)、或其他類型的字節(jié)碼 VM 在驗(yàn)證上的獨(dú)特之處。在本文中，我們將深入討論在驗(yàn)證 zkWasm 內(nèi)存子系統(tǒng)時(shí)所遇到的一些技術(shù)要點(diǎn)。內(nèi)存是 zkVM 最為獨(dú)特的部分，處理好這一點(diǎn)對(duì)所有其他 zkVM 的驗(yàn)證都至關(guān)重要。
形式化驗(yàn)證：虛擬機(jī)（VM）對(duì) ZK 虛擬機(jī)（zkVM）
我們的最終目標(biāo)是驗(yàn)證 zkWasm 的正確性，其與普通的字節(jié)碼解釋器（VM，例如以太坊節(jié)點(diǎn)所使用的 EVM 解釋器）的正確性定理相似。亦即，解釋器的每一執(zhí)行步驟都與基于該語(yǔ)言操作語(yǔ)義的合法步驟相對(duì)應(yīng)。如下圖所示，如果字節(jié)碼解釋器的數(shù)據(jù)結(jié)構(gòu)當(dāng)前狀態(tài)為 SL，且該狀態(tài)在 Wasm 機(jī)器的高級(jí)規(guī)范中被標(biāo)記為狀態(tài) SH，那么當(dāng)解釋器步進(jìn)到狀態(tài) SL'時(shí)，必須存在一個(gè)對(duì)應(yīng)的合法高級(jí)狀態(tài) SH'，且 Wasm 規(guī)范中規(guī)定了 SH 必須步進(jìn)到 SH'。
同樣地，zkVM 也有一個(gè)類似的正確性定理：zkWasm 執(zhí)行表中新的每一行都與一個(gè)基于該語(yǔ)言操作語(yǔ)義的合法步驟相對(duì)應(yīng)。如下圖所示，如果執(zhí)行表中某行數(shù)據(jù)結(jié)構(gòu)的當(dāng)前狀態(tài)是 SR，且該狀態(tài)在 Wasm 機(jī)器的高級(jí)規(guī)范中表示為狀態(tài) SH，那么執(zhí)行表的下一行狀態(tài) SR'必須對(duì)應(yīng)一個(gè)高級(jí)狀態(tài) SH'，且 Wasm 規(guī)范中規(guī)定了 SH 必須步進(jìn)到 SH'。
由此可見(jiàn)，無(wú)論是在 VM 還是 zkVM 中，高級(jí)狀態(tài)和 Wasm 步驟的規(guī)范是一致的，因此可以借鑒先前對(duì)編程語(yǔ)言解釋器或編譯器的驗(yàn)證經(jīng)驗(yàn)。而 zkVM 驗(yàn)證的特殊之處在于其構(gòu)成系統(tǒng)低級(jí)狀態(tài)的數(shù)據(jù)結(jié)構(gòu)類型。
首先，如我們?cè)谥暗牟┛臀恼轮兴觯瑉k 證明器在本質(zhì)上是對(duì)大素?cái)?shù)取模的整數(shù)運(yùn)算，而 Wasm 規(guī)范和普通解釋器處理的是 32 位或 64 位整數(shù)。zkVM 實(shí)現(xiàn)的大部分內(nèi)容都涉及到此，因此，在驗(yàn)證中也需要做相應(yīng)的處理。然而，這是一個(gè)“本地局部”問(wèn)題：因?yàn)樾枰幚硭阈g(shù)運(yùn)算，每行代碼變得更復(fù)雜，但代碼和證明的整體結(jié)構(gòu)并沒(méi)有改變。
另一個(gè)主要的區(qū)別是如何處理動(dòng)態(tài)大小的數(shù)據(jù)結(jié)構(gòu)。在常規(guī)的字節(jié)碼解釋器中，內(nèi)存、數(shù)據(jù)棧和調(diào)用棧都被實(shí)現(xiàn)為可變數(shù)據(jù)結(jié)構(gòu)，同樣的，Wasm 規(guī)范將內(nèi)存表示為具有 get/set 方法的數(shù)據(jù)類型。例如，Geth 的 EVM 解釋器有一個(gè)`Memory`數(shù)據(jù)類型，它被實(shí)現(xiàn)為表示物理內(nèi)存的字節(jié)數(shù)組，并通過(guò)`Set 32 `和`GetPtr`方法寫入和讀取。為了實(shí)現(xiàn)一條內(nèi)存存儲(chǔ)指令，Geth 調(diào)用`Set 32 `來(lái)修改物理內(nèi)存。
func opMstore(pc *uint 64, interpreter *EVMInterpreter, scope *ScopeContext) ([]byte, error) {
// pop value of the stack
mStart, val := scope.Stack.pop(), scope.Stack.pop()
scope.Memory.Set 32(mStart.Uint 64(), &val)
return nil, nil
}
在上述解釋器的正確性證明中，我們?cè)趯?duì)解釋器中的具體內(nèi)存和在規(guī)范中的抽象內(nèi)存進(jìn)行賦值之后，證明其高級(jí)狀態(tài)和低級(jí)狀態(tài)相互匹配，這相對(duì)來(lái)說(shuō)是比較容易的。
然而，對(duì)于 zkVM 而言，情況將變得更加復(fù)雜。
zkWasm 的內(nèi)存表和內(nèi)存抽象層
在 zkVM 中，執(zhí)行表上有用于固定大小數(shù)據(jù)的列（類似于 CPU 中的寄存器），但它不能用來(lái)處理動(dòng)態(tài)大小的數(shù)據(jù)結(jié)構(gòu)，這些數(shù)據(jù)結(jié)構(gòu)要通過(guò)查找輔助表來(lái)實(shí)現(xiàn)。zkWasm 的執(zhí)行表有一個(gè) EID 列，該列的取值為 1、 2、 3 ……，并且有內(nèi)存表和跳轉(zhuǎn)表兩個(gè)輔助表，分別用于表示內(nèi)存數(shù)據(jù)和調(diào)用棧。
以下是一個(gè)提款程序的實(shí)現(xiàn)示例：
int balance, amount;
void main () {
balance = 100;
amount = 10;
balance -= amount; // withdraw
}
執(zhí)行表的內(nèi)容和結(jié)構(gòu)相當(dāng)簡(jiǎn)單。它有 6 個(gè)執(zhí)行步驟（EID 1 到 6），每個(gè)步驟都有一行列出其操作碼（opcode），如果該指令是內(nèi)存讀取或?qū)懭耄瑒t還會(huì)列出其地址和數(shù)據(jù)：
內(nèi)存表中的每一行都包含地址、數(shù)據(jù)、起始 EID 和終止 EID。起始 EID 是寫入該數(shù)據(jù)到該地址的執(zhí)行步驟的 EID，終止 EID 是下一個(gè)將會(huì)寫入該地址的執(zhí)行步驟的 EID。（它還包含一個(gè)計(jì)數(shù)，我們稍后詳細(xì)討論。）對(duì)于 Wasm 內(nèi)存讀取指令電路，其使用查找約束來(lái)確保表中存在一個(gè)合適的表項(xiàng)，使得讀取指令的 EID 在起始到終止的范圍內(nèi)。（類似地，跳轉(zhuǎn)表的每一行對(duì)應(yīng)于調(diào)用棧的一幀，每行均標(biāo)有創(chuàng)建它的調(diào)用指令步驟的 EID。）
這個(gè)內(nèi)存系統(tǒng)與常規(guī) VM 解釋器的區(qū)別很大：內(nèi)存表不是逐步更新的可變內(nèi)存，而是包含整個(gè)執(zhí)行軌跡中所有內(nèi)存訪問(wèn)的歷史記錄。為了簡(jiǎn)化程序員的工作，zkWasm 提供了一個(gè)抽象層，通過(guò)兩個(gè)便捷入口函數(shù)來(lái)實(shí)現(xiàn)。分別是：
alloc_memory_table_lookup_write_cell
和
Alloc_memory_table_lookup_read_cell
其參數(shù)如下：
例如，zkWasm 中實(shí)現(xiàn)內(nèi)存存儲(chǔ)指令的代碼包含了一次對(duì)’write alloc’函數(shù)的調(diào)用：
let memory_table_lookup_heap_write1 = allocator
.alloc_memory_table_lookup_write_cell_with_value(
"store write res 1",
constraint_builder,
eid,
move |____| constant_from!(LocationType::Heap as u 64),
move |meta| load_block_index.expr(meta), // address
move |____| constant_from!( 0), // is 32-bit
move |____| constant_from!( 1), // (always) enabled
);
let store_value_in_heap1 = memory_table_lookup_heap_write1.value_cell;
`alloc`函數(shù)負(fù)責(zé)處理表之間的查找約束以及將當(dāng)前`eid`與內(nèi)存表?xiàng)l目相關(guān)聯(lián)的算術(shù)約束。由此，程序員可以將這些表看作普通內(nèi)存，并且在代碼執(zhí)行之后 `store_value_in_heap1`的值已被賦給了 `load_block_index` 地址。
類似地，內(nèi)存讀取指令使用`read_alloc`函數(shù)實(shí)現(xiàn)。在上面的示例執(zhí)行序列中，每條加載指令有一個(gè)讀取約束，每條存儲(chǔ)指令有一個(gè)寫入約束，每個(gè)約束都由內(nèi)存表中的一個(gè)條目所滿足。
mtable_lookup_write(row 1.eid, row 1.store_addr, row 1.store_value)
? (row 1.eid= 1 ∧ row 1.store_addr=balance ∧ row 1.store_value= 100 ∧ ...)
mtable_lookup_write(row 2.eid, row 2.store_addr, row 2.store_value)
? (row 2.eid= 2 ∧ row 2.store_addr=amount ∧ row 2.store_value= 10 ∧ ...)
mtable_lookup_read(row 3.eid, row 3.load_addr, row 3.load_value)
? ( 2<row 3.eid≤ 6 ∧ row 3.load_addr=amount ∧ row 3.load_value= 100 ∧ ...)
mtable_lookup_read(row 4.eid, row 4.load_addr, row 4.load_value)
? ( 1<row 4.eid≤ 6 ∧ row 4.load_addr=balance ∧ row 4.load_value= 10 ∧ ...)
mtable_lookup_write(row 6.eid, row 6.store_addr, row 6.store_value)
? (row 6.eid= 6 ∧ row 6.store_addr=balance ∧ row 6.store_value= 90 ∧ ...)
形式化驗(yàn)證的結(jié)構(gòu)應(yīng)與被驗(yàn)證軟件中所使用的抽象相對(duì)應(yīng)，使得證明可以遵循與代碼相同的邏輯。對(duì)于 zkWasm，這意味著我們需要將內(nèi)存表電路和“alloc read/write cell”函數(shù)作為一個(gè)模塊來(lái)進(jìn)行驗(yàn)證，其接口則像可變內(nèi)存。給定這樣的接口后，每條指令電路的驗(yàn)證可以以類似于常規(guī)解釋器的方式進(jìn)行，而額外的 ZK 復(fù)雜性則被封裝在內(nèi)存子系統(tǒng)模塊中。
在驗(yàn)證中，我們具體實(shí)現(xiàn)了“內(nèi)存表其實(shí)可以被看作是一個(gè)可變數(shù)據(jù)結(jié)構(gòu)”這個(gè)想法。亦即，編寫函數(shù) `memory_at type`，其完整掃描內(nèi)存表、并構(gòu)建相應(yīng)的地址數(shù)據(jù)映射。（這里變量 `type` 的取值范圍為三種不同類型的 Wasm 內(nèi)存數(shù)據(jù)：堆、數(shù)據(jù)棧和全局變量。）而后，我們證明由 alloc 函數(shù)所生成的內(nèi)存約束等價(jià)于使用 set 和 get 函數(shù)對(duì)相應(yīng)地址數(shù)據(jù)映射所進(jìn)行的數(shù)據(jù)變更。我們可以證明：
對(duì)于每一 eid，如果以下約束成立
memory_table_lookup_read_cell eid type offset value
則
get (memory_at eid type) offset = Some value
并且，如果以下約束成立
memory_table_lookup_write_cell eid type offset value
則
memory_at (eid 1) type = set (memory_at eid type) offset value
在此之后，每條指令的驗(yàn)證可以建立在對(duì)地址數(shù)據(jù)映射的 get 和 set 操作之上，這與非 ZK 字節(jié)碼解釋器相類似。
zkWasm 的內(nèi)存寫入計(jì)數(shù)機(jī)制
不過(guò)，上述的簡(jiǎn)化描述并未揭示內(nèi)存表和跳轉(zhuǎn)表的全部?jī)?nèi)容。在 zkVM 的框架下，這些表可能會(huì)受到攻擊者的操控，攻擊者可以輕易地通過(guò)插入一行數(shù)據(jù)來(lái)操縱內(nèi)存加載指令，返回任意數(shù)值。
以提款程序?yàn)槔?，攻擊者有機(jī)會(huì)在提款操作前，通過(guò)偽造一個(gè)$ 110 的內(nèi)存寫入操作，將虛假數(shù)據(jù)注入到賬戶余額中。這一過(guò)程可以通過(guò)在內(nèi)存表中添加一行數(shù)據(jù)，并修改內(nèi)存表和執(zhí)行表中現(xiàn)有單元格的數(shù)值來(lái)實(shí)現(xiàn)。這將導(dǎo)致其可以進(jìn)行“免費(fèi)”的提款操作，因?yàn)橘~戶余額在操作后將仍然保持在$ 100 。
為確保內(nèi)存表（和跳轉(zhuǎn)表）僅包含由實(shí)際執(zhí)行的內(nèi)存寫入（和調(diào)用及返回）指令生成的有效條目，zkWasm 采用了一種特殊的計(jì)數(shù)機(jī)制來(lái)監(jiān)控條目數(shù)量。具體來(lái)說(shuō)，內(nèi)存表設(shè)有一個(gè)專門的列，用以持續(xù)追蹤內(nèi)存寫入條目的總數(shù)。同時(shí)，執(zhí)行表中也包含了一個(gè)計(jì)數(shù)器，用于統(tǒng)計(jì)每個(gè)指令預(yù)期進(jìn)行的內(nèi)存寫入操作的次數(shù)。通過(guò)設(shè)置一個(gè)相等約束，從而確保這兩個(gè)計(jì)數(shù)是一致的。這種方法的邏輯十分直觀：每當(dāng)內(nèi)存進(jìn)行寫入操作，就會(huì)被計(jì)數(shù)一次，而內(nèi)存表中相應(yīng)地也應(yīng)有一條記錄。因此，攻擊者無(wú)法在內(nèi)存表中插入任何額外的條目。
上面的邏輯陳述有點(diǎn)模糊，在機(jī)械化證明的過(guò)程中，需要使其更加精確。首先，我們需要修正前述內(nèi)存寫入引理的陳述。我們定義函數(shù)`mops_at eid type`，對(duì)具有給定`eid`和`type`的內(nèi)存表?xiàng)l目計(jì)數(shù)（大多數(shù)指令將在一個(gè) eid 處創(chuàng)建 0 或 1 個(gè)條目）。該定理的完整陳述有一個(gè)額外的前提條件，指出沒(méi)有虛假的內(nèi)存表?xiàng)l目：
如果以下約束成立
(memory_table_lookup_write_cell eid type offset value)
并且以下新增約束成立
(mops_at eid type) = 1
則
(memory_at(eid 1) type) = set (memory_at eid type) offset value
這要求我們的驗(yàn)證比前述情況更精確。 僅僅從相等約束條件中得出內(nèi)存表?xiàng)l目總數(shù)等于執(zhí)行中的總內(nèi)存寫入次數(shù)并不足以完成驗(yàn)證。為了證明指令的正確性，我們需要知道每條指令對(duì)應(yīng)了正確數(shù)目的內(nèi)存表?xiàng)l目。例如，我們需要排除攻擊者是否可能在執(zhí)行序列中略去某條指令的內(nèi)存表?xiàng)l目，并為另一條無(wú)關(guān)指令創(chuàng)建一個(gè)惡意的新內(nèi)存表?xiàng)l目。
為了證明這一點(diǎn)，我們采用了由上至下的方式，對(duì)給定指令對(duì)應(yīng)的內(nèi)存表?xiàng)l目數(shù)量進(jìn)行限制，這包括了三個(gè)步驟。首先，我們根據(jù)指令類型為執(zhí)行序列中的指令預(yù)估了所應(yīng)該創(chuàng)建的條目數(shù)量。我們稱從第 i 個(gè)步驟到執(zhí)行結(jié)束的預(yù)期寫入次數(shù)為`instructions_mops i`，并稱從第 i 條指令到執(zhí)行結(jié)束在內(nèi)存表中的相應(yīng)條目數(shù)為`cum_mops (eid i)`。通過(guò)分析每條指令的查找約束，我們可以證明其所創(chuàng)建的條目不少于預(yù)期，從而可以得出所跟蹤的每一段 [i... numRows] 所創(chuàng)建的條目不少于預(yù)期：
Lemma cum_mops_bound': forall n i,
0 ≤ i ->
i Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid 1) ≥ instructions_mops' i n.
其次，如果能證明表中的條目數(shù)不多于預(yù)期，那么它就恰好具有正確數(shù)量的條目，而這一點(diǎn)是顯而易見(jiàn)的。
Lemma cum_mops_equal' : forall n i,
0 ≤ i ->
i Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid 1) ≤ instructions_mops' i n ->
MTable.cum_mops (etable_values eid_cell i) (max_eid 1) = instructions_mops' i n.
現(xiàn)在進(jìn)行第三步。我們的正確性定理聲明：對(duì)于任意 n，cum_mops 和 instructions_mops 在表中從第 n 行到末尾的部分總是一致的：
Lemma 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) = instructions_mops (Z.of_nat n)
通過(guò)對(duì) n 進(jìn)行歸納總結(jié)來(lái)完成驗(yàn)證。表中的第一行是 zkWasm 的等式約束，表明內(nèi)存表中條目的總數(shù)是正確的，即 cum_mops 0 = instructions_mops 0 。對(duì)于接下來(lái)的行，歸納假設(shè)告訴我們：
cum_mops n = instructions_mops n
并且我們希望證明
cum_mops (n 1) = instructions_mops (n 1)
注意此處
cum_mops n = mop_at n cum_mops (n 1)
并且
instructions_mops n = instruction_mops n instructions_mops (n 1)
因此，我們可以得到
mops_at n cum_mops (n 1) = instruction_mops n instructions_mops (n 1)
此前，我們已經(jīng)證明了每條指令將創(chuàng)造不少于預(yù)期數(shù)量的條目，例如
mops_at n ≥ instruction_mops n.
所以可以得出
cum_mops (n 1) ≤ instructions_mops (n 1)
這里我們需要應(yīng)用上述第二個(gè)引理。
（用類似的引理對(duì)跳轉(zhuǎn)表進(jìn)行驗(yàn)證，可證得每條調(diào)用指令都能準(zhǔn)確地產(chǎn)生一個(gè)跳轉(zhuǎn)表?xiàng)l目，這個(gè)證明技術(shù)因此普遍適用。然而，我們?nèi)孕枰M(jìn)一步的驗(yàn)證工作來(lái)證明返回指令的正確性。返回的 eid 與創(chuàng)建調(diào)用幀的調(diào)用指令的 eid 是不同的，因此我們還需要一個(gè)附加的不變性質(zhì)，用來(lái)聲明 eid 數(shù)值在執(zhí)行序列中是單向遞增的。）
如此詳細(xì)地說(shuō)明證明過(guò)程，是形式化驗(yàn)證的典型特征，也是驗(yàn)證特定代碼片段通常比編寫它需要更長(zhǎng)時(shí)間的原因。然而這樣做是否值得？在這里的情況下是值得的，因?yàn)槲覀冊(cè)谧C明的過(guò)程中的確發(fā)現(xiàn)了一個(gè)跳轉(zhuǎn)表計(jì)數(shù)機(jī)制的關(guān)鍵錯(cuò)誤。之前的文章中已經(jīng)詳細(xì)描述了這個(gè)錯(cuò)誤——總結(jié)來(lái)說(shuō)，舊版本的代碼同時(shí)計(jì)入了調(diào)用和返回指令，而攻擊者可以通過(guò)在執(zhí)行序列中添加額外的返回指令，來(lái)為偽造的跳轉(zhuǎn)表?xiàng)l目騰出空間。盡管不正確的計(jì)數(shù)機(jī)制可以滿足對(duì)每條調(diào)用和返回指令都計(jì)數(shù)的直覺(jué)，但當(dāng)我們?cè)噲D將這種直覺(jué)細(xì)化為更精確的定理陳述時(shí)，問(wèn)題就會(huì)凸顯出來(lái)。
使證明過(guò)程模塊化
從上面的討論中，我們可以看到在關(guān)于每條指令電路的證明和關(guān)于執(zhí)行表的計(jì)數(shù)列的證明之間存在著一種循環(huán)依賴關(guān)系。要證明指令電路的正確性，我們需要對(duì)其中的內(nèi)存寫入進(jìn)行推理；即需要知道在特定 EID 處內(nèi)存表?xiàng)l目的數(shù)量、以及需要證明執(zhí)行表中的內(nèi)存寫入操作計(jì)數(shù)是正確的；而這又需要證明每條指令至少執(zhí)行了最少數(shù)量的內(nèi)存寫入操作。
此外，還有一個(gè)需要考慮的因素，zkWasm 項(xiàng)目相當(dāng)龐大，因此驗(yàn)證工作需要模塊化，以便多位驗(yàn)證工程師分工處理。因此，對(duì)計(jì)數(shù)機(jī)制的證明解構(gòu)時(shí)需要特別注意其復(fù)雜性。例如，對(duì)于 LocalGet 指令，有兩個(gè)定理如下：
Theorem opcode_mops_correct_local_get : forall i,
0 <= i ->
etable_values eid_cell i > 0 ->
opcode_mops_correct LocalGet i.
Theorem LocalGetOp_correct : forall i st y xs,
0 <= i ->
etable_values enabled_cell i = 1 ->
mops_at_correct i ->
etable_values (ops_cell LocalGet) i = 1 ->
state_rel i st ->
wasm_stack st = xs ->
(etable_values offset_cell i) > 1 ->
nth_error xs (Z.to_nat (etable_values offset_cell i - 1)) = Some y ->
state_rel (i 1) (update_stack (incr_iid st) (y :: xs)).
第一個(gè)定理聲明
opcode_mops_correct LocalGet i
展開(kāi)定義后，意味著該指令在第 i 行至少創(chuàng)建了一個(gè)內(nèi)存表?xiàng)l目（數(shù)字 1 是在 zkWasm 的 LocalGet 操作碼規(guī)范中指定的）。
第二個(gè)定理是該指令的完整正確性定理，它引用
mops_at_correct i
作為假設(shè)，這意味著該指令準(zhǔn)確地創(chuàng)建了一個(gè)內(nèi)存表?xiàng)l目。
驗(yàn)證工程師可以分別獨(dú)立地證明這兩個(gè)定理，然后將它們與關(guān)于執(zhí)行表的證明結(jié)合起來(lái)，從而證得整個(gè)系統(tǒng)的正確性。值得注意的是，所有針對(duì)單個(gè)指令的證明都可以在讀取/寫入約束的層面上進(jìn)行，而無(wú)須了解內(nèi)存表的具體實(shí)現(xiàn)。因此，項(xiàng)目分為三個(gè)可以獨(dú)立處理的部分。
總結(jié)
逐行驗(yàn)證 zkVM 的電路與驗(yàn)證其他領(lǐng)域的 ZK 應(yīng)用并沒(méi)有本質(zhì)區(qū)別，因?yàn)樗鼈兌夹枰獙?duì)算術(shù)約束進(jìn)行類似的推理。從高層來(lái)看，對(duì) zkVM 的驗(yàn)證需要用到許多運(yùn)用于編程語(yǔ)言解釋器和編譯器形式化驗(yàn)證的方法。這里主要的區(qū)別在于動(dòng)態(tài)大小的虛擬機(jī)狀態(tài)。然而，通過(guò)精心構(gòu)建驗(yàn)證結(jié)構(gòu)來(lái)匹配實(shí)現(xiàn)中所使用的抽象層，這些差異的影響可以被最小化，從而使得每條指令都可以像對(duì)常規(guī)解釋器那樣，基于 get-set 接口來(lái)進(jìn)行獨(dú)立的模塊化驗(yàn)證。
鄭重聲明：本文版權(quán)歸原作者所有，轉(zhuǎn)載文章僅為傳播更多信息之目的，如作者信息標(biāo)記有誤，請(qǐng)第一時(shí)間聯(lián)系我們修改或刪除，多謝。
