CAPRI 這個名字最近出現(xiàn)在 Isabelle 交互式定理證明相關(guān)的討論里核心指向的方向是“契約感知的證明修復”。如果只看字母縮寫可能會誤以為它是一個自動補全證明的通用工具。實際上它解決的問題很具體當 Isabelle 理論里的函數(shù)、謂詞、定義或規(guī)范契約發(fā)生變化后舊依賴這些證明的記錄實現(xiàn)任務(wù)會大量失敗CAPRI 這類系統(tǒng)要做的就是讓失敗定位和重建過程具備對契約變化的感知而不是只知道“這一步過不去”。先給出我的總體判斷如果你正在維護一段長期演進的形式化驗證代碼里面有函數(shù)規(guī)格、接口契約和成片依賴的 lemma那么“契約感知的證明修復”會是一個非常值得關(guān)注的思路。它的價值不在于替你寫出一個新發(fā)明而是在你刪改一行定義導致二十處證明失敗后幫你更快找出哪些失敗是真需要改契約哪些失敗只是舊證明步驟在實現(xiàn)層不匹配。這篇文章我會從實際工程體驗出發(fā)拆解 CAPRI 術(shù)語背后的思想、Isabelle 證明失效的原因、本地復現(xiàn)實驗時該準備的前提條件以及你在引入這類方法前應(yīng)該關(guān)注的風險點。1. 先理解 CAPRI 與 contract-aware 的關(guān)系1.1 CAPRI 不是“萬能補證明器”不少人在 Isabelle 項目里遇到一堆 lemma 變紅時第一反應(yīng)是找個工具自動跑一遍看能不能把錯誤狀態(tài)消掉。這是把證明修復想得太簡單了。CAPRI 所屬的“proof repair”方向關(guān)注的是證明文本在某次理論變更后失去合法性時的自動化處理過程。它處理的不是某局部語法報錯而是結(jié)果失效。舊證明曾經(jīng)能被 Isabelle 完整檢查過現(xiàn)在因為環(huán)境變了導致原來的證明狀態(tài)在某一位置無法推進或某條引理無法滿足當前條件約束。CAPRI 的輸入通常是三樣東西變更前的舊理論、變更后的新理論、變更前后的契約對應(yīng)關(guān)系。它做的并不是把舊證明刪除然后跑到任意庫里去試探。它更愿意保留舊證明中仍然有效的結(jié)構(gòu)只把受契約變化波及的部分挑出來重新調(diào)整證明策略、中間狀態(tài)和前置假設(shè)。1.2 contract-aware 是“契約感知”不等于普通接口推斷很多關(guān)于自動修復的討論只關(guān)心接口簽名比如函數(shù)從兩個參數(shù)改成三個參數(shù)然后生成函數(shù)替換。契約感知比這個更深處一層。在 Isabelle/HOL 的形式化表達里契約可以表現(xiàn)為前置條件、后置條件、類型約束、歸納定義規(guī)則、函數(shù)終止規(guī)則、不變量、狀態(tài)轉(zhuǎn)換關(guān)系等。你在證明一個函數(shù)滿足某個性質(zhì)時經(jīng)常不是因為函數(shù)名的拼寫變了導致失敗而是函數(shù)所遵守的契約變化了。舉個例子一個step函數(shù)原本保證任何輸入都會前進一步經(jīng)某次重構(gòu)后它加入邊界控制大于等于某值的輸入不再變化。這時候原先證明x step x所依賴的簡單展開關(guān)系已經(jīng)不再成立真正需要修復的其實是證明前提要加一個閾值約束變成x threshold ? x step x。這就是讓 CAPRI 需要感知的內(nèi)容哪些性質(zhì)與契約中的前置條件綁定哪些只需要改變方法調(diào)用順序。如果系統(tǒng)不理解這種語義映射它只能機械地把舊 proof script 重播一遍最后告訴你在某一行失敗對維護的實際幫助非常有限。1.3 與手動修復和通用重寫的差別手動修復當然可行但對于大型理論庫來說成本很高。尤其當一次接口更新會牽動數(shù)百個依賴引理時純手工檢查每一個 apply 步驟的狀態(tài)幾乎不可維持。通用重寫工具的問題則相反它往往太“激進”不了解哪些舊證明結(jié)構(gòu)對新契約依然有意義。修正時可能生成一個能讓當前目標閉合的證明卻沒有保留證明的結(jié)構(gòu)語義或者為了過某個 lemma擅自弱化原命題最后產(chǎn)生的結(jié)論根本不是用戶本意想維護的性質(zhì)。CAPRI 這類契約感知方案提供的是中間態(tài)利用契約變化前后的對應(yīng)關(guān)系把失敗限制在特定的證明片段上再針對契約失效原因從知識庫、已有引理和可選擇性原語中構(gòu)建新的證明片段最終生成一個可審閱、可回放、可維護的成果。它解決的核心矛盾始終只有一個在驗證工程中代碼和契約在演進而手工同步所有證明的成本正在快速上升。2. 實際中哪些項目會被這類證明修復問題卡住2.1 長期演進項目最容易遇到“證明爛尾”Isabelle 并不只存在于學術(shù) demo。操作系統(tǒng)模型驗證、編譯器語義、并發(fā)算法、分布式協(xié)議形式化、程序邏輯和小型函數(shù)式語言的設(shè)計驗證都會把 Isabelle 作為長期驗證環(huán)境。這類項目往往需要數(shù)月甚至數(shù)年的迭代真正能撐到最后的團隊都知道一件事代碼結(jié)構(gòu)變化是常態(tài)證明跟著適應(yīng)才是復雜度最大的來源。我在本地方案中遇到過一種典型狀態(tài)定義更新之前某個理論文件還處于綠色狀態(tài)驗證耗時也就幾十秒。然而某次為了調(diào)整一個數(shù)據(jù)結(jié)構(gòu)字段改動后的契約不再支持原來的不變量結(jié)果并沒有集中在定義那一處而是順著引用網(wǎng)絡(luò)跑到了別的文件里。一個 lemma 失敗后后面所有依賴它的 theorem 也開始連片變紅滾動頁面時都不太容易看出最初的錯誤發(fā)生在哪里。CAPRI 所針對的場景正是這種。它關(guān)心“下游證明為什么會壞”并要求你提供契約變化前后的框架好讓工具在大量下游失敗中區(qū)分共同原因而不是逐個去修復表象。2.2 適合使用的前置條件不是所有 Isabelle 項目都適合跑契約感知修復。我建議先做三個檢查。第一項目里需要存在相對穩(wěn)定、命名清晰的契約結(jié)構(gòu)。如果全部是自由定義的輔助函數(shù)每個都沒什么語義約束那契約變化其實很難界定。第二你對歷史版本有版本管理。修復的前提是比較沒有變更前后快照很難區(qū)分某項證明失敗到底來自哪一次契約改動。第三理論文件的可構(gòu)建性要好。依賴關(guān)系混亂、互相循環(huán)導入、文件構(gòu)建順序不固定會讓自動修復系統(tǒng)接收到大量低質(zhì)量信號修復效果會明顯下降。這里至少有一個判斷底線如果一個項目連當天完整編譯一遍都要碰運氣那你最需要的其實不是自動修復而是先把項目構(gòu)建鏈理順。2.3 邊界情況不要過度硬套契約感知修復不擅長處理完全推翻重寫的理論。如果整個證明和契約領(lǐng)域已被替換很多舊證明片段保留不了有價值的信息再去做修復跟從零寫證明的差別不大。它也不適合用來掩蓋漏寫的證明。一臺自動修復系統(tǒng)為了把狀態(tài)閉合可能會給出一種沒經(jīng)過語義風險審查的證明看起來通過了 Isabelle 的類型檢查卻把原本要證明的邊界條件給回避了。這種情況下如果你缺少足夠的契約 review 環(huán)節(jié)自動修復帶來的風險比你手寫一個稍慢的證明還要更危險。更現(xiàn)實的應(yīng)用方式是“分路徑修復”對于改動十分局部的函數(shù)啟用自動修復讓系統(tǒng)補齊受影響的 lemma對于涉及核心安全性質(zhì)的主定理要求人工逐步審閱。等到自動修復結(jié)果在多條分支上都產(chǎn)生可復用的新模式再放開限制應(yīng)用到更大范圍。3. Isabelle 中舊證明為什么“集體爛掉”3.1 證明是疊積木式依賴鏈Isabelle 里每個 lemma、theorem、inductive case 都會形成一個被證明庫正式承認的事實。后來的證明可以使用前面的定理進行重寫、解算條件、觸發(fā)推理因此后續(xù)證明天然建立在一張依賴圖譜上。如果上層某個定義發(fā)生變化但舊定義的可簡化規(guī)則仍然保留部分低層證明可能還看不出問題。真正的問題通常出現(xiàn)在一個引理被某條件削弱后所有引用它作為輔助步驟的證明都會面臨觸發(fā)條件不匹配進而集體失敗。單純看某一行報錯很難定位到源頭是第 100 行的定義還是第 1300 行由匿名中間 lemma 添加的約束條件。自動修復系統(tǒng)要做的是順著這條依賴鏈反向檢查而不是停在首次報錯的位置。3.2 失敗狀態(tài)有幾種常見樣態(tài)契約變化后舊證明文件報錯狀態(tài)并不總是千篇一律。我通常會觀察以下特征作為判斷失敗來源的參考現(xiàn)象更可能的源頭某處simp或auto找不到重寫規(guī)則相關(guān)定義被調(diào)整可簡化性質(zhì)或原 rewrite lemma 不再是前提apply 步驟執(zhí)行后還有剩余子目標問題邏輯前提比舊契約多證明方法無法覆蓋新增分支by ...直接報“無法證明”引理結(jié)論在新契約下已經(jīng)不成立真正需要寫新性質(zhì)后面大量 lemma 因前置 lemma 失效而級聯(lián)失敗先回到依賴源頭逐層修好公共定理證明在induction分支上進展異常遞歸函數(shù)結(jié)構(gòu)或終止規(guī)則變化歸納假設(shè)不再匹配這五類情況并不互斥。CAPRI 做分析時往往會先看失敗目標中最先出現(xiàn)的現(xiàn)象因為越早失效的狀態(tài)通常意味著更靠近真實源頭等到后面出現(xiàn)的大量失敗是直接依賴關(guān)系被破壞后產(chǎn)生的傳播效應(yīng)。3.3 為什么“把 auto 重跑一遍”不夠受啟發(fā)有人寫過自動把失敗證明里的by smt替換成by auto的經(jīng)驗。問題是當契約真的變化了簡單地重跑 auto 并不能解決根源。auto、simp這類方法只會在當前上下文的已知定理和定義里自動搜索它們并不會去判斷你是不是需要新增一個前置假設(shè)。新舊契約在語義上不再是等價的關(guān)系映射重跑推理方法只會重復失敗區(qū)別只是失敗點或輸出消息更加不透明。而且自動重跑很容易制造假陽性信心。你可以看到一個 lemma 變成了綠色以為修復成功了操作權(quán)限卻沒有注意這個 lemma 的廣義相對性是否被暗中改變了。沒有契約感知的話這種自動“成功”并沒有把你帶向目標。更讓人擔心的是若干次自動重跑后代碼里累積了大量只針對當前版本可過的引用技巧再次演進時舊證明幾乎完全沒有參考價值。4. 本地實驗 CAPRI 前建議你準備的復現(xiàn)環(huán)境4.1 環(huán)境準備不復雜但要做三件事這里不談具體版本號只給通用順序因為你拿到的工具和 Isabelle 發(fā)行版未必完全匹配。落地時以你本地實際依賴為準。先安裝 Isabelle 本體并確認命令行里能調(diào)用到對應(yīng)可執(zhí)行文件。再建一個干凈的目錄當作試驗場把待修復理論、依賴腳本和日志目錄都放在同一層。最后用 git 或等價工具記錄一次“變更前”的 baseline。記錄 baseline 有個特別實際的好處你可以在壞掉之后快速跑出兩個清單。一個清單是舊版本里可以完整訓練的 lemma 數(shù)量另一個是改動后可以訓練的數(shù)量。兩邊做 diff幫助 CAPRI 這類工具縮小修復范圍。4.2 設(shè)計一個能復現(xiàn)的最小理論我會用一版最小可運行的 Isabelle/HOL 示意代碼來說明失敗機制。這里的邊界很關(guān)鍵不同版本 Isabelle 支持的語法細節(jié)不同建議你把它當成結(jié)構(gòu)示意不要直接復制到生產(chǎn)庫。theory ContractDemo imports Main begin (* 第一個契約版本step 對所有輸入都前進一步 *) fun step :: nat \Rightarrow nat where step x x 1 (* 舊證明任意輸入增加 *) lemma step_increase: x step x by simp (* 第二次契約調(diào)整加入邊界控制 *) fun step :: nat \Rightarrow nat where step x (if x 10 then x 1 else x) (* 舊證明繼續(xù)執(zhí)行會失敗 *) lemma step_increase: x step x by simp (* 契約感知修復后的思路 結(jié)論不再全稱成立需要把 x 10 拆成前置條件寫清楚 *) lemma step_increase_under_contract: x 10 \Longrightarrow x step x by auto end注意在同一理論里同名fun定義即使不允許重復上述代碼只是為了說明當函數(shù)契約從“無條件遞增”改成“閾值內(nèi)遞增再不變”時舊證明不能直接復用而修復不能只靠切換證明方法完成關(guān)鍵在于把新契約納入定理前置條件。如果你要測試的工具比手工改 lemma 更自動化輸入最好直接使用新舊兩個理論文件并且用 diff 生成契約變更位置列表讓系統(tǒng)先嘗試匹配哪些定義在舊版本里的證明結(jié)論仍然與新版本語義可對齊。4.3 驗證修復是否真成功用什么標準很多人只關(guān)心 Isabelle 是否回了個綠燈。但對一個維護任務(wù)來說驗證標準至少要包括五層。第一層是可復現(xiàn)。同一個修復命令再次執(zhí)行結(jié)果穩(wěn)定。第二層是范圍邊界。修復后的 lemma 數(shù)量、新增的假設(shè)數(shù)量、對輸入文件外部依賴的改變量都能被輸出出來。第三層是證明可理解性。你能否看出它到底用了哪條引理、哪個前置條件把目標推過去的。第四層是舊證明保留度。如果這次修復把所有 lemma 全部推倒重建雖然系統(tǒng)任務(wù)最終過了但維護上的價值很可能不高。理想的修復應(yīng)該盡量保留沒有涉及契約變化的舊證明路徑。第五層是回歸風險。修復之后舊版本代碼里原本依賴舊契約的證明是否受影響如果影響有沒有統(tǒng)一記錄。這五個標準也是評測 CAPRI 時比較關(guān)鍵的觀測點。若只看工具自身是否成功結(jié)束很容易錯過隱藏的語義漂移。5. 把自動修復機制拆成四個理解單元5.1 將“契約變化”與“證明失敗”對齊契約感知的第一步是做對齊。系統(tǒng)把舊版本中函數(shù)的定義、類型、前置條件和后置條件項作為舊契約把新版本中對應(yīng)的項作為新契約然后將舊證明中每一步所依賴的契約分量映射到新版本。這一步的復雜度在于 Isar 證明里往往存在大量匿名假設(shè)和中間態(tài)。系統(tǒng)要判斷某個問題的失敗是因為契約新增條件導致前提不可達還是因為契約的結(jié)論本身已經(jīng)變?nèi)趸蜃儚娨只蚴且粋€舊 proof 方法觸發(fā)了不同語義的重寫規(guī)則。這樣對齊完才能把修復對象縮小到某個子目標上。如果沒有這一步修復腳本只能在失敗位置嘗試一個動作列表無法理解哪些地方值得保留哪些地方必須重建。這也是許多“證明修復插件”看似集成方便、效果卻很有限的原因。5.2 在證明文本里定位斷裂點對齊后系統(tǒng)可以給出失效范圍圖譜。舊的 lemma 本來依賴 A、B、C 三條引理契約調(diào)整后 A 變了B 沒變C 只是被新版本的 A 間接影響。修復系統(tǒng)會識別出第一個真實斷裂點。有的斷裂發(fā)生在證明開頭比如 lemma 加入assumes后直接導致現(xiàn)有證明上下文發(fā)生變化。有的斷裂發(fā)生在中間某個apply (subst ...)步驟因為重寫引理被移除。還有的斷裂發(fā)生在終點by auto雖然把舊目標幾乎推完但新契約下多了個分支需要再補一步展開。斷裂點粒度非常重要。一個apply (auto simp: ...)可以接納二十個引理一旦失敗你很難只靠外層報錯判斷如何補。CAPRI 類機制會再次嘗試把該步驟展開為若干小步驟從失敗狀態(tài)中提取出沒有目標閉合的分支再交給下一階段去修復。5.3 為受影響的證明片段構(gòu)造新路徑定位完成后進入真正意義上的 proof repair。系統(tǒng)會嘗試在失敗子目標上匹配可用的定義擴張、simp 規(guī)則、已有定理、條件激活性、歸納結(jié)構(gòu)等信息。與純粹的sledgehammer使用不同CAPRI 不是把整條目標傳給外部求解器而是在保留舊證明路徑上下文的前提下對局部目標搭建一條新路徑。如果目標只是缺了一個前置條件系統(tǒng)會修改 lemma 的頭部把該條件寫入assumes如果目標來自函數(shù)的遞歸結(jié)構(gòu)變化系統(tǒng)會把證明風格從apply auto改成apply (induction ...)并在相應(yīng)分支補條件如果問題源于重寫規(guī)則缺失它可能生成一個新引理把新的定義展開式制作成 rewrite rule插在舊失敗點之前。從代碼庫維護者的角度這里最有價值的不是那些已經(jīng)能自動提示的 lemma 名稱而是系統(tǒng)建議修改的點。一個靠譜的修復成果應(yīng)該看起來像舊證明中 80% 的步驟不變只在新契約外增加少量步驟或前置條件并且在注釋里標明為什么要加。這比生成一大段復雜到人肉無法審閱的 Isar 腳本要實用得多。5.4 產(chǎn)出仍要經(jīng)過人工思考一道由于 CAPRI 來自定理證明研究的延伸當前不建議把它輸出的修復結(jié)果當成最終成果。至少在關(guān)鍵性質(zhì)上需要做一次人工 review。原因是證明修復的語義并不只是“讓所有目標收到done”。尤其在前置條件變化的情況下工具更容易配合全稱量詞變化、前置條件調(diào)整等整體上合法的修改。人工 review 可以分三步查看修復涉及的契約頭變更確認是否與期望的 API 演進方向一致只審閱工具新生成或新增改的證明片段跳過完全未改變的舊路徑最后跑一遍完整回歸觀察修復前后所有被引用文件的導出性質(zhì)。只要維護者能說清“這次輸入系統(tǒng)允許調(diào)整的是哪個契約項”修復過程就是可控的。這也正是 contract-aware 與暴力重寫相比的本質(zhì)區(qū)別。6. 我在實際評測和使用前會確認的清單6.1 先把版本和導入關(guān)系摸清楚帶 Isabelle 概念的設(shè)計很容易忽略依賴版本變化、理論導入結(jié)構(gòu)調(diào)整、外部庫更換這些也可能導致證明失敗。表面上你會看到 lemma 紅掉但根因其實不在你自己的契約改動上。因此測試 CAPRI 之前我會先跑一次環(huán)境基線。確認在當前 Isabelle 版本下不修改任何契約的代碼能否被完整驗證。如果能再引入契約變更。接著檢查導入關(guān)系避免修復工具在指定目錄外訪問到同名的舊理論。最后把自動生成的報告和 diff 日志保存下來。若失敗出現(xiàn)在某個文件里而該文件的契約其實沒變優(yōu)先修復它的上游依賴。6.2 不要只盯單條 lemma要看批量結(jié)果如果系統(tǒng)需要同時處理幾十個失敗證明建議給每次修復定義一個批量結(jié)果表檢查項說明可接受信號成功率新理論中需要修復的 lemma 總量里能被完整構(gòu)建的數(shù)量越高越好但要有失敗記錄變更幅度修復后與舊證明 diff 的行數(shù)和被改 lemma 數(shù)同一問題下變化越集中越正常新增假設(shè)數(shù)工具通過給 lemma 添加前置條件來繞開契約變化新增假設(shè)與契約調(diào)整目標一致外部依賴變化修復時是否改動被其他文件導入的公共定理對公共定理的改動需要重點 review人工審閱成本新生成證明片段的可讀性和注釋完整性約低越好不適合只丟一個巨型求解命令回歸穩(wěn)定性整個理論庫連續(xù)執(zhí)行兩次的結(jié)果輸出結(jié)果和耗時無明顯差異批量任務(wù)中最常踩的坑是并發(fā)跑多個修復時所有 lemma 同時使用同一個“以前可用的引理”而公共引理在修復過程中被自動改寫。這樣你會得到一片綠油油的結(jié)果但項目整體語義偏離很遠。所以修復順序也要保證依賴目錄沒有丟失。6.3 基于我踩過的一些坑給出幾條第一原則如果需要用一個句子反映什么值得用什么不值得我會這樣描述把 CAPRI 當成一個把失敗范圍收窄到可控修復對象的研究性工具而不是一鍵解決所有驗證工程問題的正式軟件依賴建議先從規(guī)模較小的契約邊界入手觀察它對簡單函數(shù)重構(gòu)的修復情況。之后每次升級盡量將“代碼變化”和“契約變化”分開提交。當 a 和契約同步改動時CAPRI 類工具的映射難度會急速上升。你可以在版本管理中先把契約名、類型表達式和引理頭記錄進說明文件的 metadata讓修復系統(tǒng)之后能更容易對齊。還有如果你不是理論證明維護者而只是一個臨時被征調(diào)來補證明的工程師我給你的建議是先不打 CAPRI。先去看對應(yīng)文件里契約當前承諾什么再判斷舊證明的失敗是環(huán)境升級造成的語法問題還是真實現(xiàn)的語義變化。后者的修復往往需要在斷言層面重新取舍自動工具只能幫你處理大量重復、耗時的機械旋轉(zhuǎn)部分。今天記錄這些主要是想讓人看到“契約感知證明修復”為什么值得理解。它的核心不是把apply auto換成另一個更強方法而是用一種能反映用戶意圖的方式維護長期驗證工程。我認為這條路代表著 Isabelle 等證明助手走向大規(guī)模實踐的必要方向。等這類工具真正支持普通理論庫規(guī)模的運行維護成本才可能真正被降下來。