3MIKAN
仮想通貨直コン

Foundry invariant test入門:handler・ghost variable・counterexampleを試す

Foundryのstateful invariant testをunit・fuzzと比較し、handler、actor、target selector、ghost variable、ERC-20・AMM・vault・権限の性質、縮約counterexampleを再現します。

3MIKANのブランドキャラクターが分岐する木製経路へ試験球を流し、秤・二槽プール・鍵付きレバーを囲む安全柵が保たれるか観察するFoundry invariant testの記事画像

Foundryのinvariant testは、入力を何個も試すだけでなく、複数の操作を順番に実行しても守られる性質を探すtestです。1回のdepositが成功するかではなく、deposit、donate、redeemの順序やactorが変わっても会計が合うかを確認します。

この記事では、unit test、stateless fuzz、stateful invariantを同じ再現用プロジェクトで比較します。handler、actor、targetSelector、ghost variableを組み、ERC-20、AMM、vault、access controlの性質を4,096 callで検査します。最後に意図的なrevoke bugを発生させ、Foundryが30 callの失敗を3 callへ縮めたcounterexampleを回帰testへ戻します。

unit test、stateless fuzz test、stateful invariant testが探索する入力と操作列の違い

unit・fuzz・invariantはstateの扱いが違う

まずは3つを実行単位で分けます。

test 変えるもの stateの扱い 見つけやすい失敗
unit 既知の入力と手順 1 scenarioを固定 明確な正常系・異常系・回帰
stateless fuzz 1 functionの入力 各fuzz caseで初期stateへ戻す 境界値、overflow、入力依存の失敗
stateful invariant function、入力、actor、順序 1 run内でstateを引き継ぐ 操作順、複数actor、会計・権限のずれ

今回のstateless fuzzは、同じ初期reserveへ1回だけswapし、256入力で積が減らないことを確認します。invariant campaignは11種類のhandler操作から64 callを並べるrunを64回実行するため、合計は4,096 callです。

回数が多いだけでは同じtestになりません。fuzz testを1万回実行しても、各caseでstateを戻すなら「grantした後にrevokeし、その後で旧actorが操作する」という順序は作りません。

良いinvariantは自然言語の安全性主張から作る

invariantは「revertしない」「残高が正しい」のような広すぎる言葉から始めず、比較する左右を決めます。

種類 今回のproperty 左辺と右辺
保存則 ERC-20供給量が既知actor残高の合計と一致 totalSupply == sum(balanceOf(actor))
独立ledger mint合計からburn合計を引くと供給量になる totalSupply == ghostMinted - ghostBurned
単調性 fee付きAMMのreserve積が初期値を下回らない reserveX * reserveY >= initialProduct
state整合 vaultのassetとshareが操作履歴へ一致 observed stateとghost ledger
権限 ghost上で未承認のactorは特権操作に成功しない unauthorizedSuccesses == 0

「contractが安全」は一つのmachine-checkable propertyではありません。会計、権限、rounding、liveness、価格、外部callを分け、今回のmodelが観測できる値へ落とします。

handlerはprotocolへ入る操作窓口

handlerは、fuzzerのraw inputを現実的な操作へ直すwrapperです。今回のProtocolHandlerは4つの固定actorを持ち、mint、transfer、burn、swap、deposit、donate、redeem、role操作をprotocolへ渡します。

たとえばmintは次の順に処理します。

function tokenMint(uint256 actorSeed, uint256 rawAmount) external {
    address receiver = _actor(actorSeed);
    uint256 amount = bound(rawAmount, 1, 1e18);

    vm.prank(admin);
    token.mint(receiver, amount);

    ghostMinted += amount;
}

actorSeedをそのままaddressとして使わず、固定したactor setのindexへ変換します。mintが成功した後だけghostを増やすため、期待stateとobserved stateを別の経路で更新できます。

actorの操作をhandlerが整形し、protocol実行後にobserved stateとghost ledgerを比較して次の操作へ進む循環

actorを1人に固定しない

token transfer、vault share、roleはaccountごとにstateが違います。test contractだけをmsg.senderにすると、別actorへのtransferや、付与したroleを別actorが使うpathを探索できません。

一方、無制限なaddressを生成すると、balanceの合計対象や権限対象が追えなくなります。今回は4 addressだけをhandlerから利用し、tokenをactor set外へ送らないことで「既知actor残高の合計」を成立させました。この前提が変わるなら、pool、vault、fee recipient、burn addressも合計へ追加します。

target selectorで操作面を明示する

FoundryはtargetContractでhandlerを対象にできます。さらにtargetSelectorを使うと、campaignが呼ぶfunctionをallowlistにできます。

bytes4[] memory selectors = new bytes4[](11);
selectors[0] = ProtocolHandler.tokenMint.selector;
selectors[1] = ProtocolHandler.tokenTransfer.selector;
// swap、vault、role操作を続ける
selectors[10] = ProtocolHandler.attemptPrivilege.selector;

targetContract(address(handler));
targetSelector(FuzzSelector({
    addr: address(handler),
    selectors: selectors
}));

excludeSelectorは、contractを広くtargetにしつつdebug用functionなどを除くdenylistです。今回のように安全性へ関わる操作面が明確なら、allowlistで「呼ぶもの」をreviewしやすくします。

targetを絞るほど必ず良いわけではありません。production entrypointをselectorから落とせば、そのpathは何run増やしても探索されません。PRではselector数と各call countを見て、全11操作が337〜397回呼ばれたことを確認しました。

boundassumefail_on_revertを使い分ける

handlerへ入るuint256は、そのままでは残高やreserveより大きい値が大半です。今回のamountはboundで有効範囲へ写します。

uint256 amount = bound(rawAmount, 1, balance);

vm.assume(condition)はconditionを満たさないcase全体を捨てます。複数の厳しいassumeを重ねるとreject上限へ達したり、重要な境界値をほとんど実行できなかったりします。

使い分けの目安は次の通りです。

  • 数量を有効範囲へ入れる: bound
  • address同士が異なるなど、生成し直すべきglobal precondition: assume
  • 現在のbalanceが0など、操作列の途中で自然に起きるstate: handlerからreturnしてcall countへ残す
  • 権限不足など想定した失敗: low-level callで結果を観測し、成功・失敗をghostへ分類する

今回のfail_on_revertfalseです。これは「すべてのrevertを無視してよい」という意味ではありません。handlerが期待revertを意味のあるcounterへ変換し、今回の通過campaignでは4,096 call・revert 0になったことまで確認します。

unexpected revertも性質に含めたいprotocolでは、fail_on_revert=trueにするか、handlerの失敗countを0とするinvariantを追加します。設定だけでなく、revertが仕様上の拒否なのかbugなのかを先に分けてください。

ghost variableは期待stateの別帳簿

ghost variableは、protocolに保存されていない期待値をtest側で持つ変数です。tokenの例では、成功したmintとburnだけを集計します。

expected supply = ghostMinted - ghostBurned
observed supply = token.totalSupply()

ここでghostMinted = token.totalSupply()と毎回コピーすると、同じ値を左右で比較するだけです。入力、成功結果、以前のghostから期待値を更新し、protocol getterとは独立させます。

今回の検証コードでは次を別管理しました。

  • token: mint合計、burn合計
  • vault: deposit、donation、withdrawalのasset合計
  • access control: actorごとの期待role、承認済み成功、未承認成功、承認済み失敗
  • coverage: selectorごとのcall count

ERC-20は供給量を2方向から照合する

ERC-20totalSupplybalanceOfを定義します。OpenZeppelin Contracts 5.6.1のERC20を使った例では、次の2 propertyを同時に確認しました。

totalSupply == actor A〜D の balanceOf 合計
totalSupply == ghostMinted - ghostBurned

1つ目は残高配分、2つ目は発行・焼却履歴です。transfer時に供給量まで変えるbugなら両方がずれ、mint時に間違ったactorへ配るbugなら残高合計だけでは見逃してもactor別ghostを追加して追えます。

この例の合計は、handlerがtokenを4 actor以外へ送らない条件でのみ完全です。任意addressへtransferできるproduction tokenへ同じloopをコピーしないでください。

AMMはreserve積の単調性を小さく検査する

定積型AMMではx*y=kを基準にします。今回の小さなpoolは入力から0.3%を差し引く式を使い、swap後に次を確認します。

reserveX * reserveY >= initialProduct

64×64 campaignではX→YとY→Xの順序が混ざります。1方向を1回だけ試すstateless fuzzより、roundingが積み重なったstateを検査できます。

ただしこれは、簡略化したreserve会計だけのpropertyです。実際のAMMではtoken balanceとrecorded reserve、liquidity mint / burn、fee-on-transfer token、callback、oracle、protocol feeも別に検査します。定積式と数値例はインパーマネントロスとAMM式の解説、proxyを含む実行contextはERC-1967のslot・authority・layout確認へ分けています。

vaultはassetとshareを別々に追う

vaultではassetとshareを同じ数量だと決めつけません。今回の再現コードはdeposit、donation、redeemを持ち、次を確認します。

totalAssets == ghostDeposited + ghostDonated - ghostWithdrawn
totalShares == sum(sharesOf(known actors))

100 assetをdepositして100 shareを発行した後、25 assetをdonateするとtotalAssets=125totalShares=100です。donationでshareまで増える実装なら、2つ目のpropertyが壊れます。

ERC-4626ではassetとERC-20 shareを分け、depositやredeemの方向ごとにrounding要件があります。今回のShareVaultはその関係を学ぶ最小実装であり、ERC-4626の全interface、fee、slippage、inflation attack対策を実装したproduction vaultではありません。

access controlは期待roleと実際の成功を比べる

role handlerはadminとしてgrant / revokeし、actorとして特権functionを呼びます。ghost上で未承認なら、成功数は常に0でなければなりません。

ghostUnauthorizedSuccesses == 0
gate.privilegedCount == ghostAuthorizedSuccesses
ghostAuthorizedFailures == 0

権限はfunction単体より、付与、取消、再付与、実行の順序で壊れやすい領域です。OpenZeppelin AccessControlでもroleとrole adminを分けています。proxy upgradeでcodeと権限が変わる場合はERC-1967の記事、同じtransaction内の一時lockを操作列で検査する入口はtransient storageの記事も参照してください。

意図的なrevoke bugを3 callへ縮める

counterexample用のBuggyRoleGateは、grantでroleをtrueにしますが、revokeで実際のmappingをfalseへ戻しません。handlerのghostはfalseになるため、期待stateとobserved stateが分かれます。

固定seedのcampaignでは、Foundryが30 call目で失敗を見つけ、shrinkerが次の3 callへ縮めました。

grantActor()
revokeActor()
actAsActor()
step ghostAuthorized contract authorized privileged call
grant true true 未実行
revoke false true(bug) 未実行
act false true 成功してinvariant失敗

Forgeのraw outputにはfuzzerがhandlerを呼ぶsenderと、handler内部のvm.prankも出ます。最小再現へ落とすときは、sender表示をそのままcopyするのではなく、admin grant、admin revoke、actor actionという意味を読みます。

意図的な失敗例は通常の通過campaignと分離します。別profileを実行するverifierが「このinvariantは失敗する」「理由が一致する」「3 callがこの順で出る」ことを期待値として検査します。公開した再現データに環境、設定、通過property、失敗sequence、限界を固定しました。

修正後は最小sequenceをunit testへ戻す

shrunk sequenceは、そのまま高速な回帰testへ変えます。修正版RoleGate.revokeがmappingをfalseへ戻した後、旧actorの特権callが失敗し、counterが0のままか確認しました。

gate.grant(actor);
gate.revoke(actor);

vm.prank(actor);
(bool success,) = address(gate).call(
    abi.encodeCall(RoleGate.privilegedIncrement, ())
);

require(!success);
require(gate.privilegedCount() == 0);

unit regressionだけへ置き換えず、fixed contractのinvariant campaignも残します。unitは既知の再発をすぐ止め、invariantは別の操作列で同じ性質が壊れないか探す役割です。

今回の実行結果

環境はFoundry / Forge 1.8.0、Solidity 0.8.36、OpenZeppelin Contracts 5.6.1、Prague EVM、optimizer有効、runs 200です。2026年8月31日時点のFoundry stableには1.8.1がありますが、この記事では公開した検証環境と同じ1.8.0を使い、toolchain更新を混ぜていません。

campaign result
unit ERC-20、vault、revoke regressionの3件pass
stateless fuzz AMM 256 runs pass
fixed stateful invariant 7 properties、64 runs、4,096 calls、revert 0でpass
selector coverage 11 / 11操作を実行、各337〜397 calls
intentional bug 30 callsで検出し、3 callsへshrink
expected-failure verifier failure reasonとsequenceを公開JSONへ照合してpass

これらは同じseedと環境の観測結果です。実行時間やcall countの偏りはhardware、Foundry version、dictionary、worker設定、code変更で変わり得ます。

seed・runs・depth・workerを固定する

再現用foundry.tomlの主要値は次の通りです。

[fuzz]
runs = 256
seed = "0x6022602260226022602260226022602260226022602260226022602260226022"

[invariant]
runs = 64
depth = 64
workers = 1
fail_on_revert = false
check_interval = 1
shrink_run_limit = 5000
show_metrics = true
show_solidity = true

runsは操作列を作る回数、depthは1 runのcall数です。単純には探索call数がruns × depthになりますが、revert、discard、早期failure、check_intervalで実際の評価回数は変わります。

固定seedは失敗の再現に役立ちますが、同じpathだけを永久に試す理由にはしません。固定campaignを回帰基準にし、深いnightly campaignや複数seedを追加する場合は別profileへ分けます。

counterexampleを読む順番

失敗logが長い場合は、次の順に切り分けます。

  1. 失敗したinvariant名と比較式を確認する
  2. originalとshrunkのcall数を見る
  3. handler function、actor、bound後の入力を順に並べる
  4. 各call後のobserved stateとghost stateの最初の差を探す
  5. expected revertをunexpected successとして数えたのか確認する
  6. 最小sequenceをunit testで再現する
  7. 修正後にunitとstateful campaignを両方実行する

最後のcallだけを修正すると、差が生まれた以前のcallを見落とします。今回も失敗したのはactAsActorですが、原因は一つ前のrevokeActorでした。

invariant test導入チェックリスト

  • 自然言語の主張を左右の値があるpropertyへ変換した
  • unit、stateless fuzz、stateful invariantの役割を分けた
  • production entrypointに対応するhandler操作を列挙した
  • actor setとactor外addressの扱いを決めた
  • targetSelectorまたはexcludeSelectorの理由をreviewした
  • amountはboundし、過剰なassumeでcaseを捨てていない
  • expected revertとunexpected revertを分けた
  • ghostはprotocol getterからコピーせず独立更新した
  • donation、rounding、fee、role revokeなど順序依存pathを入れた
  • selector call countとrevert / discardを確認した
  • seed、runs、depth、worker、compiler、optimizerを固定した
  • counterexampleをshrinkし、最小unit regressionへ戻した
  • passを全状態の証明やaudit完了として扱っていない

今回の再現用プロジェクトは、外部RPC、mainnet fork、wallet、個人鍵、署名、transaction送信、資産を使いません。token、AMM、vault、role gateも学習用の小さな会計modelです。

invariant testで重要なのは、run数を大きく見せることではありません。守りたい性質、到達できる操作、actor、入力、ghost、revertの意味を明示し、見つかった最小sequenceを回帰testへ戻すことです。

この記事にスポンサー、affiliate、wallet接続、署名要求、transaction送信、資産操作のCTAはありません。将来testing platform、audit、developer educationの広告を置く場合も広告であることを明示し、再現コード、counterexample、test pass、security reviewから分離します。

確認した一次情報