Lean 核心健全性破口:一個不靠公理就能證出 False 的投影漏洞
Leo de Moura 個人部落格(Lean 作者本人事後報告) · 2026-08-01
2026 年 7 月 28 日,leanprover/lean4 收到 issue #14576:核心檢查器會接受「結構名稱與被投影值不匹配」的投影(projection),讓型別不正確的引數繞過驗證,最終能在完全不使用公理、sorry、unsafeCast 的情況下,靠標準的 addDecl 流程證出 False。回報者 kiranandcode 是在審查一份被簡化過的 Collatz 猜想「反證」時發現這個破口。受影響的 nightly 版本為 4.34.0-nightly-2026-07-27。
漏洞機制
Lean 的可信基礎建立在 de Bruijn criterion 上:核心檢查器只有約五千行 C++、只做一件事——判斷證明項是否具備宣稱的型別,無論上層 elaborator、tactic 或 Mathlib 的程式碼是否有錯,最終都要通過這一關。這次的破洞出在巢狀歸納型別(nested inductive type)的消去處理:當某個參數只用來構造巢狀出現、卻不出現在建構子欄位裡(所謂 phantom parameter)時,核心產生輔助型別的過程會讓這個參數從自動生成的型別中消失,因而完全跳過型別檢查。de Moura 在報告中強調這是「實作臭蟲,不是後設理論的破洞」,即 Lean 的邏輯基礎本身沒有問題,問題出在核心沒有正確驗證巢狀出現參數是否真的表現得像參數。
影響範圍
這個漏洞只能透過 metaprogramming 直接把宣告送進核心、繞過前端的引數檢查才能觸發,一般使用者以標準語法撰寫證明不會踩中。
- 攻擊路徑僅限直接呼叫
addDecl,略過前端型別檢查 - 偽造的證明會讓
#print axioms顯示零依賴,難以事後察覺 - 回報者把一份錯誤的 Collatz 猜想證明,化簡成一個最小可重現的
False證明
修補與緩解
PR #14577 在回報後一小時內合併,隨後 PR #14582 進一步強化了核心對巢狀出現參數的檢查。團隊藉此機會複查了相鄰程式碼,又抓出並修補了數個獨立的核心漏洞(PR #14607、#14608、#14609、#14613、#14615、#14616),並提交多個強化措施(PR #14621、#14631、#14632)。新的 patch release 已經釋出。
冪等金鑰不是 Stripe 發明的:回溯到 1984 年 Xerox PARC 的一次 RPC 呼叫
Hatchet 官方部落格 · 2026-08-01
Hatchet 工程團隊在部落格文章中把現代 API 常見的「冪等金鑰(idempotency key)」機制,一路回溯到 1984 年 Andrew Birrell 與 Bruce Jay Nelson 發表的論文《Implementing Remote Procedure Calls》,指出這個構想比 Stripe 2015 年公開的 Idempotency-Key HTTP 標頭早了超過三十年。在不可靠網路上重送請求時如何避免同一筆操作被重複執行,是分散式系統的老問題;冪等金鑰讓伺服端能辨識「這是同一次呼叫的重試」而非「新的一次呼叫」。
源流:從 call identifier 到 ClientToken
Birrell 與 Nelson 論文中設計的「call identifier」機制,其構想源自 Nelson 1981 年在 Xerox PARC 的博士論文《Remote Procedure Call》,原文寫道:「呼叫識別碼有兩個作用——讓呼叫端確認收到的結果封包確實對應本次呼叫,也讓被呼叫端能剔除重複的呼叫封包。」這是目前有記錄、最早在電子電腦系統中出現的同類機制。此後 Amazon EC2 在 RunInstances 之類的變更型 API 上採用 ClientToken 參數達到同樣效果;OASIS 由 Microsoft、IBM、BEA、TIBCO 共同提出的 WS-ReliableMessaging,則選擇在傳輸層而非應用層做訊息去重。
標準化的漫長路徑
2005 年 Mark Nottingham 提出 Internet-Draft《POST Once Exactly》,嘗試把這個概念正式標準化進 HTTP 語意(呼應 RFC 2616),但當年並未成案。這條路線最終演變成目前仍在制訂中的 draft-ietf-httpapi-idempotency-key-header-04,試圖把 Stripe 帶紅的業界慣例收斂成正式的 HTTP 標頭規格。
原始來源:Hatchet: The First Idempotency Key、Birrell & Nelson, 1984、IETF idempotency-key-header draft
把 GCC 逼到只剩 5 顆暫存器:spill 對效能的代價比想像中雜訊得多
rjp.io(spillbench 作者部落格) · 2026-08-02
rjp.io 的作者用自建基準套件 spillbench,在一台 Intel Xeon E-2236(3.40GHz)上,以 GCC 15.2.0 的 -ffixed-<reg> 旗標逐一鎖住暫存器,量測 9 個運算核心函式在通用暫存器從 15 顆一路砍到 5 顆時的靜態 spill 數與 wall-clock 執行時間。這篇文章直接挑戰「暫存器越少、spill 越多、效能必然等比例變差」的直覺假設。
規格細節
受測的 9 個核心函式分兩組,分別鎖通用暫存器(r15…r8)與 XMM 暫存器(xmm15…xmm4):
- 通用暫存器組:ChaCha20、SHA-256、SipHash-2-4、整數矩陣乘法、LZ77 壓縮、Quicksort
- XMM 暫存器組:double 矩陣乘法、FIR 濾波器、Mandelbrot
在暫存器被砍到最緊繃的預算下,FIR 濾波器的 spill 數從 8 次暴增到 43 次,執行時間慢了 76%;整數矩陣乘法從 60 次增加到 82 次,慢了 42%;SHA-256 從 8 次增加到 80 次,慢了 33%。但 SipHash-2-4 即使多了 23 次 spill,執行時間反而快了 2%。9 個核心函式的「新增 spill 數」與「變慢幅度」之間,Pearson 相關係數只有 0.55,顯示 spill 次數本身是個很弱的效能預測指標——FIR 濾波器每多一次 spill 約損失 2.18% 效能,SipHash-2-4 卻幾乎是 0%。
影響範圍
暫存器檔案之間會互相干擾:對以 GP 暫存器為主的 double 矩陣乘法鎖住 XMM 幾乎沒有影響,但鎖住 GP 卻讓它慢 34%;反過來對 SHA-256 鎖住 XMM,會因為 GCC 的自動向量化被打斷,導致堆疊 spill 暴增 8 倍、執行時間多花 5.6%。作者也用這組資料反推 32-bit x86 年代(當時僅有 6-7 顆可用通用暫存器)的效能代價,估計平均會慢 13%–18%,暫存器需求特別高的核心函式甚至可能慢 27%–42%——較高成本部分來自當年 64-bit 值須拆成暫存器對處理、in-order 管線缺乏重排序視窗,以及 write-through L1 快取與有限的 store-to-load forwarding。完整基準程式與量測數據已公開在 github.com/rjpower/spillbench。