不變量測試

不變量測試斷言一些無論合約經歷什麼動作序列都必須成立的性質，接著向系統發射冗長、隨機的呼叫序列，並在每一步之後檢查該性質是否依然成立。不變量是協議永遠不該打破的規則，例如借貸池的資產永遠覆蓋它欠存款人的、或所有使用者餘額之和永遠等於代幣總供給。單元測試檢查一條路徑、參數模糊測試變動單一呼叫的輸入，而不變量測試則變動呼叫的整個順序與組合。

就機制而言，你定義不變量函式，讓框架（Foundry 的不變量測試或 Echidna）對這些合約產生隨機的呼叫序列，通常經由一個 handler 路由，後者把輸入限制在實際的範圍內、並追蹤 ghost 變數（真實合約不保存的額外記帳）。在每個序列的每次呼叫之後，框架重新檢查所有不變量；第一個違例會以一串具體、最小化的交易序列回報。由於它是有狀態的、且探索多步互動，它能抓到單次呼叫測試漏掉的跨函式與累積狀態漏洞。

其藝術在於選出既為真又緊的不變量。像「合約不回滾」這種弱不變量幾乎毫無用處；像「任何存入、提領與轉帳的序列都不會讓使用者移出多於其加入的價值」、或「總資產永遠大於或等於總負債」這種強不變量，直接編碼了償付能力與守恆，正是真實漏洞所違反的東西。好的不變量通常捕捉償付能力、價值守恆、單調記帳與存取約束，而寫出它們，會逼你精確理解協議所承諾的是什麼。