SV 1 — Abstractions from Proofs

原文：POPL 2004 · doi:10.1145/982962.964021 · 開啟原文 PDF ↗

這一份是同一篇論文的另一種編排。內容自成一體，讀這篇不需要看站上其他頁。

1 先自己試一次

下面這支程式是對的。lock() 和 unlock() 嚴格交替，沒有連續上兩次鎖，也沒有解一個沒上的鎖。

while (*) {
1:  if (p1) lock();
    if (p1) unlock();
2:  if (p2) lock();
    if (p2) unlock();
    ...
n:  if (pn) lock();
    if (pn) unlock();
}

但一個自動驗證器很容易在這裡誤報。它會說：「我找到一條路徑，lock() 之後沒有 unlock()。」

那條路徑是這樣走的：進入第一個 if（所以上了鎖），然後不進入第二個 if（所以沒解鎖）。從控制流程上看，這條路徑確實存在。

先停下來想一分鐘：驗證器要記住什麼事實，才會知道這條路徑走不通？

想好了再往下。

答案不難：它得記住 p1 的值。因為第一個 if 進去了就表示 p1 為真，而 p1 為真時第二個 if 也一定進得去。兩個 if 的條件是同一個。

好。那現在把問題放大：

這裡有 $n$ 個這樣的 if。 你要記住 $p_1$ 到 $p_n$ 全部嗎？如果每個都是一個布林事實，那狀態就有 $2^n$ 種組合。$n = 30$ 就是十億。

再看仔細一點：$p_1$ 這個事實，只在標籤 1 和標籤 2 之間有用。過了標籤 2，lock/unlock 那一對已經配好了，$p_1$ 再也用不到。

所以真正的問題不是「要記住哪些事實」，而是：

哪些事實，該在哪個程式位置記住？

這篇論文（POPL 2004）就是在回答這個問題。而它的答案有點出乎意料：不要用猜的，去讀「這條路走不通」的那份證明——答案已經寫在裡面了。

2 這個問題為什麼值得解

要看懂這篇的位置，得知道它掉在一段什麼樣的歷史裡。

1980 年代，model checking 在硬體驗證上非常成功。 電路的狀態是有限的，可以窮舉。但軟體不行——一個 32 位元的整數變數就有四十億種取值，再加上迴圈、遞迴、heap，狀態空間直接無限。

1997 年前後出現的關鍵想法是 predicate abstraction。 概念很直接：不要追蹤變數的確切數值，只追蹤一組是非問句的真假。

假設你選了三個 predicate $p_1, p_2, p_3$，那麼任何一個程式狀態都被壓縮成三個位元，例如 $(\text{真}, \text{假}, \text{真})$。原本無限多的狀態，變成最多 $2^3 = 8$ 種。有限了，就能窮舉。

代價是資訊流失：兩個不同的具體狀態可能壓成同一組位元。但這正是我們要的——抽象就是刻意丟掉不重要的細節。難的是決定哪些不重要。

接著的問題是：那組 predicate 從哪來？ 沒有人一開始就知道該選哪些。標準做法是一個叫 CEGAR（counterexample-guided abstraction refinement）的迴圈：

1. 先用很少的 predicate 做一個粗略的抽象
2. 在抽象上找通往 ERROR 的路徑
3. 找不到 → 程式安全，結束
4. 找到了 → 把這條路徑翻成一條數學公式，丟給求解器
5. 公式有解 → 這條路真的走得通，是真的 bug，回報
6. 公式無解 → 這是誤報。加入新的 predicate 讓抽象變細，回到第 2 步

這個迴圈本身不難懂。難的全部集中在第 6 步那幾個字：「加入新的 predicate」。

到 2000 年代初，這一套已經有實際戰果——微軟的 SLAM 專案用它驗證 Windows 驅動程式，找到真實的錯誤。工具跑得動，但第 6 步仍然是靠啟發式規則在猜：從錯誤路徑裡撈出現過的表達式，加進 predicate 集合。

猜出來的東西有兩個毛病，而那正是下一節的內容。

3 前人做到哪裡

要看懂「前人的毛病」，得先看懂第 4 步在做什麼——那裡有幾個記號，後面整篇都會用到。

3.1 把一條路徑翻成公式

第 4 步說「把路徑翻成公式」。規則只有兩條：

• 賦值 v = e 變成等式 v = e
• 條件成立（if (c) 走 true 分支）變成 c 本身

例如這條通往 ERROR 的路徑：

int x = 1;
int y = x + 1;
if (y < 0) { ERROR; }

翻譯後是 $x = 1 \;\wedge\; y = x + 1 \;\wedge\; y < 0$。

現在問題變成純數學的了：這三個條件能同時成立嗎？不能——前兩式逼出 $y = 2$，跟第三式牴觸。

「路徑走得通」等價於「公式有解」。 這個轉換是整個領域的地基。回答「有沒有解」的程式叫 SMT solver；你不需要知道它內部怎麼運作，只要知道它回答什麼：有解（satisfiable，這條路走得通）或無解（unsatisfiable，走不通、是誤報）。

3.2 為什麼變數要加下標

上面那個翻譯有個漏洞。看這兩行：

x = 1;
x = x + 1;

照規則會翻成 $x = 1 \wedge x = x + 1$。但 $x = x+1$ 在數學上永遠是假的——沒有任何數字等於自己加一。翻譯出錯了。

問題在於：程式裡的 x 是一個會變的盒子，數學裡的 $x$ 是一個固定的值。同一個名字被當成兩種東西用。

解法是給每次賦值後的值一個新名字：$x_1 = 1 \;\wedge\; x_2 = x_1 + 1$。現在它有解了（$x_1 = 1$、$x_2 = 2$），而且忠實反映程式行為。這種寫法叫 SSA（static single assignment）。

論文用的記號是尖括號 $\langle x, 1 \rangle$，代表某個變數在執行過程中某個時間點的值。下標不是指令編號，別這樣記——論文 p.234 的例子是「$\langle \mathit{ctr},1 \rangle$ 代表*前兩個指令執行後* $\mathit{ctr}$ 的值」，下標 1，卻是第 2 個指令之後。抓住「同一個變數在不同時間點有不同名字」就夠了。

3.3 前人的兩個毛病

現在可以講清楚問題出在哪了。回到第 1 節那個 locking 例子。

第一，數量爆炸。 要排除所有誤報，$p_1, \dots, p_n$ 全都得追蹤。$n$ 個布林 predicate 就是 $2^n$ 種組合，抽象狀態指數成長。

第二，位置放錯。 前人的做法是把找到的 predicate 靠啟發式撒出去，而且往往一視同仁地加到許多、甚至全部的程式位置。但 $p_1$ 只在標籤 1 和 2 之間有用，把它帶到程式的每個角落是純粹的浪費。

論文在 Abstract（p.232）用 parsimonious（精簡）形容理想的抽象：在每個控制位置，只指定當下變數之間的關係，而且只留證明正確性真正需要的那些。它同時點出前人的抽象為什麼不精簡——predicate 裡混進了變數的「舊值」，而且是靠啟發式規則撒到各處的。

這個觀察值多少？論文 §1（p.233）給了數字：一個 138,000 行的 C 驅動程式，總共需要 382 個 predicate 才能證明正確——但平均每個程式位置只需要約 8 個。

382 對 8。這就是「哪些 predicate 用在哪裡」值得單獨解一次的理由。

4 這篇的解法

4.1 證明裡面就有答案

論文 §1（p.233）的原話是：一條抽象路徑之所以走不通，理由已經簡潔地編碼在「它走不通」的證明裡了。

所以不要猜。solver 說「無解」的時候，它其實握有一份反駁證明（refutation）。把證明讀一遍，需要的事實就浮出來。而且成本很低——論文說 interpolant 可以用對證明做一次線性掃描得到，不需要額外的定理證明工作。

4.2 工具：只用共同語言說話

把一條走不通的路徑從中間切開，前半段叫 $\varphi^-$，後半段叫 $\varphi^+$。兩者合起來無解（因為路徑走不通）。

interpolant（插值式）是一個公式 $\psi$，滿足三個條件（論文 §2, p.234）：

1. $\varphi^- \Rightarrow \psi$ —— 前半段成立時，$\psi$ 一定成立
2. $\psi \wedge \varphi^+$ 無解 —— $\psi$ 已經足以跟後半段矛盾
3. $\psi$ 只用同時出現在 $\varphi^-$ 和 $\varphi^+$ 裡的符號

Craig interpolation theorem 保證：只要 $\varphi^- \wedge \varphi^+$ 無解，這樣的 $\psi$ 一定存在。這條定理不是這篇發明的，它是 1957 年就有的結果——論文自己的參考文獻 [9] 就是它：W. Craig, Linear reasoning, J. Symbolic Logic 22:250–268, 1957。

用個比喻。前半段講中文，後半段講日文，$\psi$ 只能用兩邊都寫得出來的漢字。條件 1 說「$\psi$ 是前半段的合理摘要」，條件 2 說「這份摘要已經足以拆穿後半段」，條件 3 說「摘要只能用共同詞彙」。

第 3 條就是我們要的東西。 切點兩側的共同符號，正是「執行到切點時各變數當下的值」——不多不少，剛好是那個程式位置需要記住的事實。回頭看第 3.3 節說的前人毛病：predicate 裡混進「舊值」，正好被條件 3 擋掉了。

4.3 真正的貢獻不是「用了 interpolation」

這點很容易被誤讀。Craig 的定理只保證 interpolant 存在，沒說怎麼把它算出來。

這篇發明的是一套可以機械執行的推導規則。 論文 §3 定義了兩層東西：

第一層，一個證明系統（Fig. 3, p.235）。四條規則 HYP、COMB、CONTRA、RES，用來對線性算術的子句集合產生反駁證明。

第二層，帶插值的推導規則。 把上面每條規則改寫成這個形式：

讀作：「在把公式切成 $\varphi^-$ 和 $\varphi^+$ 的前提下，推出了 $\Delta$，而目前累積的插值式是 $\psi$。」（論文的一般 sequent 寫成 $\Gamma \vdash \Delta$，$\Gamma$ 是左邊的前提、$\Delta$ 是右邊的結論；這裡看到的是右邊。）

方括號就是重點。 推導一路往下走，方括號裡的東西同步累積；推到矛盾（$\vdash \bot$）時，方括號裡剩下的就是 interpolant。

不用猜，不用事後驗證，照著規則走就會掉出來。論文用 Invariant 1 和 Invariant 2 證明這些規則是健全的——這樣算出來的東西保證滿足 4.2 的三個條件。

4.4 每個位置一份清單

第二個洞察在論文的 Locality 段（p.235）。注意它排在「3 Interpolants from Proofs」標題之前，屬於 §2 Overview 的收尾。

不要只在一個地方切開路徑。沿著路徑的每一個切點都切一次，每個切點各求一個 interpolant。

在第 $i$ 個切點求出的 interpolant，只會用到那個切點兩側的共同符號——也就是執行到那裡時各變數當下的值。把它翻譯回程式變數，就得到「第 $i$ 個位置需要知道的事實」。

於是我們不是得到一包全域 predicate，而是得到一張表：位置 1 需要這些、位置 2 需要那些。382 對 8 的差距就是這樣來的。

論文還指出一個附帶好處：這件事跟 lazy abstraction 搭配時，predicate 集合不再只增不減——沿著路徑走，用得上的 predicate 會換人。interpolation 因此順便給出了「什麼時候某個 predicate 已經沒用了」的判準。

5 案例：三個，由淺入深

論文裡有四個具體案例。這一節走前三個，由淺入深；第四個放在最後當延伸。

5.1 案例一：locking（不用算，先建立直覺）

回到第 1 節那支程式，這是論文的 Figure 1（p.233）。

我們已經知道答案是「記住 $p_1$」。現在用 4.4 的眼光重看一次：

那條誤報路徑是「進第一個 if、不進第二個 if」。翻成公式，前半段有 $p_1 \ne 0$（進去了），後半段有 $p_1 = 0$（沒進去）。兩邊的共同符號只有 $p_1$。

所以在標籤 1 和 2 之間那個切點，interpolant 只能是關於 $p_1$ 的東西——不可能是關於 $p_2, \dots, p_n$ 的，因為那些符號在切點的一側根本不出現。

條件 3 自動幫你做到了「只記必要的」。 這不是啟發式撈出來的結果，是規則的直接後果。

5.2 案例二：算出一個 interpolant（論文 Figure 2）

這是論文的主案例（p.234）。ctr 是計數器，m 是另一個變數：

1:  x := ctr;
2:  ctr := ctr + 1;
3:  y := ctr;
4:  assume(x = m);
5:  assume(y ≠ m + 1);

這條路徑走不通。 原因：$x$ 抄下舊的 ctr，然後 ctr 加一，$y$ 抄下新的 ctr，所以必然 $y = x + 1$。既然 $x = m$，就有 $y = m+1$，第 5 行的 $y \ne m+1$ 不可能成立。

照 3.2 的 SSA 規則翻成公式：

這五條的 conjunction 就是這條路徑的 trace formula，它無解。

原文這裡有個排版錯誤，順便學一課。 論文 Figure 2 第 5 列的約束印成 $\langle y,2 \rangle = \langle m,0 \rangle + 1$（等號），但那一行的指令是 assume(y ≠ m+1)，而且論文同一頁明說「the conjunction $\varphi$ of all constraints is unsatisfiable」。照等號讀，這五條其實有解（取 $\mathit{ctr}_0 = m_0 = 0$ 就成立），整個例子會垮掉。所以原意必然是 $\ne$，上表已經改正。 讀論文本來就會遇到這種事。算不出來的時候，先確認是不是自己錯了；真的對不上，原文也可能有 typo。

現在在第 2 行後面切一刀：$\varphi^-_2$ 是前兩條，$\varphi^+_2$ 是後三條。兩邊的共同符號是 $\langle x,1 \rangle$ 和 $\langle \mathit{ctr},1 \rangle$——正好就是「執行完前兩行之後，$x$ 和 ctr 當下的值」。

論文算出的 interpolant 是 $\psi_2 = (\langle x,1 \rangle = \langle \mathit{ctr},1 \rangle - 1)$，翻回程式變數就是 $\hat\psi_2 = (x = \mathit{ctr} - 1)$。

這就是位置 2 需要記住的唯一事實。 不是 ctr 的值，不是 x 的值，而是它們的差。

五行指令中間有四個切點，論文對每個各做一次：「If we partition the TF $\varphi$ in this way at each point $i = 1,\dots,4$ of the trace, then we obtain from $P$ four interpolants」（p.234）。這四個 interpolant 翻回程式變數，就是 Figure 2 最右欄那一整排 predicate。

5.3 案例三：自己用規則導一次（論文 Figure 4）

上面兩個案例都是看答案。但這篇的重點是不用猜——照著規則走，interpolant 會自己掉出來。

這一題你自己動手。三段：先建立對定義的直覺，再認識三條規則，最後用論文 Figure 4（p.237）的例子實際推導一次。答錯會告訴你錯在哪，答對才解鎖下一步。進度存著，關掉瀏覽器再回來不會歸零。

為了讓你專心在機制上，這裡只用線性算術的三條規則，不碰 resolution。

5.4 一個容易混淆的地方

做完上面那題，有個陷阱要先拆掉，很多人第一次會弄混。

問題一：推導過程中 $y$ 是在哪裡消失的？

在相加那一步。$0 \le y-x$ 和 $0 \le z-y$ 相加，$-y$ 和 $+y$ 抵銷，剩下 $0 \le z-x$。這是國中就會的代數消去，跟規則設計、跟 interpolation 理論都沒有關係。

問題二：那為什麼 interpolant 能『保證』只含共同變數？

這是另一回事。真正的保證來自整套規則共同維持的不變量（論文的 Invariant 1 與 Invariant 2）：每一條規則都被設計成不會把非共同符號漏進方括號，所以不論推導怎麼走、多長，結論都成立。

把這兩件事混為一談的後果：你會以為「代數消去 = 只含共同變數」。這在上面那個例子恰好看起來成立，但換到 resolution 那半套規則就完全對不上。

記住：消去是這個例子的計算過程，不變量才是通則的保證。

5.5 案例四（延伸）：resolution

論文 Fig. 5（p.237）示範了用 resolution 規則推導 interpolant，對應布林推理的部分（RES、RES-A、RES-B）。它需要先熟悉 CNF 與子句的概念，所以這裡不展開。想補齊的話，讀完 §3 前半再回頭看那張圖。

6 他們比了什麼、沒比什麼

這一節值得慢慢讀，因為論文的實驗結果有一個反直覺的地方，而論文自己誠實地寫出來了。

6.1 實驗設定

• 實作：BLAST，論文作者群的軟體模型檢查器。求 interpolant 用 VAMPYRE 這個能產生證明的定理證明器。
• 對象：數個 Windows NT 裝置驅動程式，驗證的性質是一個關於 I/O Request packet 處理的有限狀態自動機（22 個狀態）。
• 硬體：IBM ThinkPad T30，2.4 GHz Pentium，512MB RAM。
• 比較的三組設定（同一個工具、同一批程式、同一台機器）：

6.2 數字

Table 1（p.244）。Disc 是從空 predicate 集合開始的總驗證時間；Reach 是給定所有必要 predicate 後、只做可達性分析的時間；Preds 是需要的 predicate 總數；Avg/Max 是每個程式位置追蹤的 predicate 數的平均與最大值。- 表示六小時內沒跑完。

6.3 讀出反直覺的那一格

先看最亮眼的：舊版 BLAST 在 parport 和 parclass 上六小時跑不完，兩個新設定跑完了。最大那支 138,373 行、382 個 predicate、平均每個位置只要 7.2 個、最多 28 個——就是第 3.3 節那個「382 對 8」。

但接著看 Disc 那幾欄，會發現一件怪事：

Craig+Locality 的總時間反而比 Craig 慢，而且慢不少（floppy：25m20s vs 7m56s）。

如果只看這一欄，結論會變成「locality 沒有用，反而更貴」。論文自己解釋了原因：Craig+Locality 可能在不同的程式位置重新發現同一個 predicate，所以找 predicate 的過程變慢了。

那它贏在哪？看 Reach 欄——給定所有 predicate 之後，只做可達性分析：

• floppy：3m21s → 0m46s
• parclass：9m1s → 1m6s

差了將近九倍。 因為每個位置只帶 7 個 predicate，而不是全部 382 個，狀態空間小得多。論文還提到兩件表格上看不到的事：Craig+Locality 用的記憶體顯著較少，而且後續執行（例如驗證修改過的版本、或產生 proof-carrying code 的證明）更快、產生的證明樹更小。

所以「哪個比較好」的答案取決於你在測什麼。 一次性的驗證看 Disc，Craig 贏；要反覆驗證、或要輸出證明，看 Reach 和記憶體，Craig+Locality 大幅領先。

6.4 他們沒比什麼

這份實驗控制得相當乾淨——同一個工具、同一批 benchmark、同一台機器，三種設定只差在 predicate 怎麼來、放在哪。這是自我比較的優勢：變因少。

但也因此有幾件事它沒有告訴你：

• 沒有跟其他工具比。 表裡沒有 SLAM 或任何外部系統的數字，所以看不出這套方法相對於當時其他做法的位置。
• 記憶體只有文字描述，沒有數字。 「顯著較少」是論文的說法，表格裡沒有這一欄。
• 「後續執行更快」也沒有數字。 同樣只是文字宣稱。
• benchmark 全部是 Windows 裝置驅動程式，性質是同一個 22 狀態的自動機。換一種程式、換一種性質會怎樣，這份實驗答不了。
• 論文提到在 parclass 上找到數個違反規範的地方，表中數字是把含錯誤的 case 註解掉之後的版本——也就是說，表格量的是「驗證正確程式」的成本。

這不是在挑毛病。讀任何一篇實驗論文，都值得把「他們比了什麼、沒比什麼、變因控制到什麼程度」問過一遍，這是判斷一個數字能推廣到多遠的唯一方法。

7 怎麼讀原文

只有 13 頁（pp.232–244），但密度很高。

7.1 一組動作，不只是順序

讀這類論文時，專業讀者做的不是「從頭讀到尾」，而是一組固定的動作。拿這篇練習：

• 看到定義，先找反例。 讀到 interpolant 的三個條件，問「拿掉第 3 條會怎樣？」——答案是 $\varphi^-$ 自己就成了合法的 interpolant，等於什麼都沒壓縮。第 3 條是唯一逼迫壓縮發生的條件。
• 看到定理，先問它排除了什麼。 Craig 的定理保證存在性，那它沒有保證什麼？沒有保證好算、沒有保證唯一、沒有保證算出來的那個對驗證有用。這篇的貢獻正好落在它沒保證的那一格。
• 看到表格，先找沒有比較的那一格。 就是 6.4 做的事。
• 看到「我們的方法快 N 倍」，先問變因。 這篇沒有這個問題（它是自我比較），但這個習慣要帶著走。
• 讀不懂的段落，先確認是不是自己錯了；真的對不上，原文也可能有 typo。 5.2 那個等號就是。

7.2 各節導覽

下表的章節名與起始頁都逐頁對照過原文。

如果只有一小時：Abstract → §1 → §2（含 Locality）→ §3 的 Fig. 3 與 Fig. 4 → §7 的 Table 1。這條線涵蓋了問題、洞察、機制與證據，其餘都是把它做嚴謹的細節。

取得原文：本頁頂端有 DOI 與作者公開版 PDF 的連結，教材裡每個 p.NNN 也都直接連到原文那一頁。