Bounding Rounding Errors in Integer Maths
三句話摘要
智能合約中整數除法的舍入誤差分析，以及如何用 Z3 SMT 求解器嚴格證明誤差上界。 EVM 整數舍入誤差可導致結果與真實值相差近 2 倍，用 Z3 求解器寫 10 行 Python 即可嚴格證明公式的誤差上界，是智能合約數學審計的必備工具。 除法後乘法會放大誤差：Solidity 中 `a/b` 的誤差最多為 1，但若再乘以 c，誤差上限就變成 c。因此運算順序至關重要，應優先乘後除以避免精度損失。
重點整理
重點- 1
除法後乘法會放大誤差：Solidity 中 `a/b` 的誤差最多為 1，但若再乘以 c，誤差上限就變成 c。因此運算順序至關重要，應優先乘後除以避免精度損失。
- 2
巢狀除法的誤差超出直覺：`(a/b * c) / d` 看起來因乘以小於 1 的 `c/d` 應不放大誤差，但實際可能產生 2 的絕對誤差，原因是有兩個不同的截斷機會同時疊加。
- 3
ERC-4626 公式可能向上偏差：OpenZeppelin 的 vault 兌換公式並非總是向下取整，在特定參數下（如 a=189, b=1, c=20）結果為 18，而真實值僅 9.45，幾乎是 2 倍，完全違反「向下取整」的直覺假設。
- 4
Z3 可形式化證明誤差邊界：透過 Python 呼叫 Z3 定義整數變數與不等式，可以自動驗證「是否存在使誤差超過上界 c 的 a/b/c 組合」，UNSAT 表示不存在，SAT 並給出反例；用 0.999c 做 sanity check 即可確認腳本正確性。
實用技巧與重點
乾貨- 工具：Z3 SMT Solver（Python 介面），用於自動搜尋反例或證明不存在反例
- 講者：Jianis，Chain Security 安全工程師
- 公式類型分析：
- `a / b`：最大誤差 = 1
- `(a / b) * c`：最大誤差 = c
- `(a / b * c) / d`（c < d）：直覺猜 1，實際最大誤差 = 2
- `(a / b * c) / d`（c > d）：最大誤差 = `floor(c/d) + 1`
- ERC-4626 反例：a=189, b=1, c=20 → 真實值 9.45，OpenZeppelin 公式輸出 18（約 1.99 倍）
- 另一反例：a=512, b=3, c=1 → 真實值 1536，公式輸出 0.024，絕對誤差達 512
- 極端案例：a=1, b=1, c=4 → 真實值 0.25，公式輸出 0，相對誤差 100%
- Z3 判定結果：ERC-4626 公式可達真實值的 1.99999 倍，但無法達到 2 倍（UNSAT）
- Z3 程式碼流程：import z3 → 定義整數變數 → 設定邊界條件 → 轉換為實數計算真實值 → 計算絕對誤差 → 加入「誤差 ≥ 上界」作為求解條件 → 呼叫 `check()`
結論
結論“EVM 整數舍入誤差可導致結果與真實值相差近 2 倍，用 Z3 求解器寫 10 行 Python 即可嚴格證明公式的誤差上界，是智能合約數學審計的必備工具。”
完整解析
詳細智能合約在 EVM 上執行時只有整數運算，所有除法都會無條件向下截斷小數部分。這個事實看似簡單，但在複雜公式中，誤差的累積方式往往違反開發者的直覺，且現有靜態分析工具和 AI 助手對此類問題的偵測能力都相當有限。Chain Security 安全工程師 Jianis 在演講中系統性地分析了這個問題，並提出了一套可形式化驗證的解法。
從最基礎的 `a/b` 開始，截斷誤差最多為 1（因為只有小數部分被丟棄）。但一旦在除法後接乘法，如 `(a/b) * c`，那個 1 的誤差就會被 c 放大，最終與真實值的差距最多達到 c 個單位。更反直覺的情況出現在 `(a/b * c) / d` 且 c < d 的場景：多數人會猜測，由於後面乘以了小於 1 的係數，誤差應被縮小，最終不超過 1。然而實際上，由於存在兩個截斷機會，誤差可以達到 2。Jianis 以 a=5, b=3, c=2, d=3 為例，真實值為 1.111，而整數運算結果為 0，誤差超過 1，驗證了這個反直覺的結論。
接著 Jianis 聚焦於 ERC-4626 vault 的 OpenZeppelin 實作。這個公式用來將股份（shares）換算為資產（assets），本質是帶有加 1 修正的 `a * b / c` 形式。許多人假設這類公式永遠向下取整，但實際並非如此。以 a=189, b=1, c=20 為例，真實值為 9.45，但鏈上計算結果卻是 18，幾乎是真實值的兩倍。相反方向同樣嚴重：a=1, b=1, c=4 時，真實值 0.25 在鏈上計算為 0，相對誤差達 100%。這意味著小額操作可能被完全歸零，而某些操作則可能讓使用者獲得遠超預期的資產。
為了嚴格證明誤差邊界，Jianis 展示了用 Python 呼叫 Z3 SMT Solver 的做法。只需定義整數變數、設定合理邊界、寫出兩種計算版本（鏈上整數版 vs 實數真實值版），然後讓求解器嘗試找出「誤差超過上界 c」的反例。若結果為 UNSAT，即確認不存在這樣的反例，誤差上界成立。針對 ERC-4626 公式，Z3 證明了結果不可能達到真實值的 2 倍（UNSAT），但可以找到達到 1.99999 倍的反例（SAT），從而精確劃定了舍入誤差的理論極限。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
