イーサリアムアカウント状態：最小限のトークンのためのQAパイプライン

QAダッシュボードによるスマートコントラクト状態の監視

前回の記事では、エンドツーエンドの実装を説明しました。最小限のトークンコントラクト、オフチェーン状態の再構築、Reactフロントエンド—`mint()`からMetaMaskまでのすべて。この記事では、その続きから始めます。このようなものをどのようにQAするのでしょうか?

私は(まだ)ブロックチェーンエンジニアではありませんが、QAパターンはドメイン間でうまく移植でき、他の場所ですでに機能しているものを借用することが、私が最も速く学ぶ方法です。

コントラクトは3つのことしか行いません:`mint`、`transfer`、`burn`ですが、それでも完全なQAツールチェーンを実践するには十分です:静的解析、ミューテーションテスト、ガスプロファイリング、形式検証。

コードは`egpivo/ethereum-account-state`にあります。

ブロックチェーンQAピラミッド:ベースの静的解析から最上位の形式検証まで

最初の状態

新しいものを追加する前に、プロジェクトにはすでに以下がありました:

• 21のFoundryユニットテスト 各状態遷移をカバー(成功、不正な入力でのリバート、イベント発行)
• 3つの不変テスト `TokenHandler`経由で10のアクター上でランダムな`mint`/`transfer`/`burn`のシーケンスを実行(各128k回の呼び出し)
• ファズテスト ランダムな量で`sum(balances) == totalSupply`をチェック
• TypeScriptドメインテスト (Vitest) オンチェーン状態マシンをミラーリング
• CI: コンパイル、テスト、リント(Prettier + solhint)

すべてのテストが合格しました。カバレッジも問題なく見えました。では、なぜさらに手間をかけるのでしょうか?

「すべてのテストが合格」は「すべてのバグが捕捉された」を意味しないからです。100%の行カバレッジでも、正しいことをチェックするアサーションがなければ、実際のバグを見逃す可能性があります。

フェーズ1: スマートコントラクトの静的解析とカバレッジ

Slither

Slither(Trail of Bits)は、テストでは見えない問題を捕捉します:リエントランシー、チェックされていない戻り値、インターフェースの不一致。

./scripts/run-qa.sh slither

結果: 1つの中程度の発見: `erc20-interface`: `transfer()`が`bool`を返さない。

これは予想されることです。コントラクトは意図的に完全なERC20ではありません:教育用の状態マシンです。しかし、この発見は学術的なものではありません:

後で誰かがこのトークンをERC20を期待するプロトコルにインポートした場合、インターフェースの不一致は静かに失敗します。Slitherは今それをフラグするので、決定は意識的です。

カバレッジ

./scripts/run-qa.sh coverageカバレッジ結果。

カバーされていない関数が1つ:`BalanceLib.gt()`。これについては後で戻ります。

forge coverageの出力: 24テスト合格、Token.solカバレッジテーブル

ガススナップショット

./scripts/run-qa.sh gas

3つの操作のベースラインガスコスト:

操作ごとのガス

その後の実行では、`forge snapshot — diff`がベースラインと比較します。`transfer()`の20%のガス退行は、すべてのユーザーにとって実際のコストです—マージ前にそれを捕捉することは安価です。

フェーズ2: ミューテーションテストと形式検証

ミューテーションテスト (Gambit)

ここで事態は興味深くなりました。Gambit(Certora)はミュータントを生成します: 小さな意図的なバグを持つ`Token.sol`のコピー(`+=`を`-=`に、`>=`を`>`に、条件を否定)。パイプラインは各ミュータントに対して完全なテストスイートを実行します。ミュータントが生き残った場合(すべてのテストがまだ合格)、それは具体的なテストギャップです。

./scripts/run-qa.sh mutation

結果: 97.0%のミューテーションスコア — 33のミュータントのうち32が死滅、1が生存。

Gambitの出力ログは各ミュータントとその変更を示します。いくつかの例:

Generated mutant #7: BinaryOpMutation — Token.sol:168
totalSupply = totalSupply.add(amountBalance) → totalSupply = totalSupply.sub(amountBalance)
KILLED by test_Mint_Success
Generated mutant #19: RelationalOpMutation — Token.sol:196
if (!fromBalance.gte(amountBalance)) → if (fromBalance.gte(amountBalance))
KILLED by test_Transfer_Success
Generated mutant #28: SwapArgumentsMutation — Token.sol:81
return Balance.unwrap(a) > Balance.unwrap(b) → return Balance.unwrap(b) > Balance.unwrap(a)
SURVIVED ← テストがこれを捕捉しませんでしたGambitミューテーションテスト: 32死滅、1生存、ミューテーションスコア97.0%

生き残ったミュータントは、`BalanceLib.gt()`内の`a > b`を`b > a`に入れ替えました。テストがそれを捕捉しなかったのは、`gt()`がデッドコードだからです。`Token.sol`のどこでも呼び出されることはありません。

カバレッジは91.67%の関数にフラグを立てましたが、ギャップを説明できませんでした。ミューテーションテストはそれを行いました:`gt()`はデッドコードで、何も呼び出さず、間違っていても誰も気付きません。

スマートコントラクト内のデッドコードまたは保護されていないコードには実際の前例があります。

この関数は呼び出し可能であることを意図していませんでしたが、誰もその仮定をテストしませんでした。私たちの`gt()`は比較すると無害ですが、パターンは同じです:存在するが実行されないコードは、誰も監視していないコードです。

形式検証 (Halmos)

Halmos(a16z)はすべての可能な入力について記号的に推論します。ファズテストがランダムな値をサンプリングしてエッジケースにヒットすることを期待する一方で、Halmosはプロパティを徹底的に証明します。

./scripts/run-qa.sh halmos

結果: 9/9の記号テスト合格 — すべての入力に対してすべてのプロパティが証明されました。

検証されたプロパティ:

検証されたプロパティ

1つの実用的な注意:Halmos 0.3.3は`vm.expectRevert()`をサポートしていないため、通常のFoundry方式でリバートテストを書くことができませんでした。回避策はtry/catchパターンです—リバートすべき時に呼び出しが成功した場合、`assert(false)`が証明を失敗させます:

function check_mint_reverts_on_zero_address(uint256 amount) public {
vm.assume(amount > 0);
try token.mint(address(0), amount) {
assert(false); // ここに到達すべきではありません
} catch {
// 予想されるリバート - Halmosはこのパスが常に取られることを証明します
}
}

最も美しいものではありませんが、機能します—Halmosはすべての入力に対してプロパティを証明します。これは、実際にツールを実行することによってのみわかる種類のものです。

形式検証が重要な理由の文脈:

脆弱性はコード内にあり、誰でも確認できましたが、デプロイ前にそれを捕捉したツールやテストはありませんでした。Halmosのような記号証明器は、まさにそのギャップを埋めるために存在します—それらはサンプリングしません;入力空間を使い果たします。

Halmosの出力: 9テスト合格、0失敗、記号テスト結果

テストファイルは`contracts/test/Token.halmos.t.sol`です。

フェーズ3: クロスレイヤープロパティテスト

最初の記事のアーキテクチャには、オンチェーン状態マシンをミラーリングするTypeScriptドメインレイヤーがあります。このフェーズでは、2つが実際に一致するかどうかをテストします。

fast-checkを使用したプロパティベースのテスト

TypeScriptドメインレイヤー用のfast-checkプロパティテストを追加し、FoundryのファザーがSolidityに対して行うことをミラーリングしました:

npm test - tests/unit/property.test.ts

結果: 実際のバグを修正した後、9/9のプロパティテストが合格しました。

テストされたプロパティ:

• `Balance`: 可換性、結合性、恒等性、逆元、比較の一貫性
• `Token`: ランダムな操作シーケンス下での不変条件`sum(balances) == totalSupply`(200回実行、各50操作)
• `Token`: ランダムなシーケンス後の`totalSupply`非負
• `mint`は有効な入力に対して常に成功
• `transfer`は`totalSupply`を保持

fast-checkが見つけたバグ

fast-checkは`Token.ts`の`transfer()`で実際のクロスレイヤー整合性バグを見つけました。縮小された反例はすぐに明らかでした:

Property failed after 3 tests
Shrunk 2 time(s)
Counterexample: transfer(from=0xaaa…, to=0xaaa…, amount=1n)
→ from == to (自己転送)
→ verifyInvariant() returned false

自己転送(`from == to`)は`sum(balances) == totalSupply`の不変条件を破りました。`toBalance`は`fromBalance`が更新される前に読み取られたため、`from == to`の場合、古い値が控除を上書きしました:

// Before (バグあり)
const fromBalance = this.getBalance(from);
const toBalance = this.getBalance(to); // ← from == toの時に古い
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
this.accounts.set(to.getValue(), toBalance.add(amount)); // ← 減算を上書き

修正:`fromBalance`を書き込んだ後に`toBalance`を読み取り、Solidityのストレージセマンティクスに一致させます:

// After (修正済み)
const fromBalance = this.getBalance(from);
this.accounts.set(from.getValue(), fromBalance.subtract(amount));
const toBalance = this.getBalance(to); // ← 今は更新された値を読み取ります
this.accounts.set(to.getValue(), toBalance.add(amount));

Solidityコントラクトは影響を受けませんでした:各書き込み後にストレージを再読み取りします。しかし、TypeScriptミラーには、既存のユニットテストがカバーしていない微妙な順序依存性がありました。

より大規模なクロスレイヤーの不一致は壊滅的でした。

私たちの自己転送バグは誰もお金を失わせることはありませんでしたが、障害モードは構造的に同じです:一致するはずの2つのレイヤーが一致しません。

途中で遭遇した落とし穴

既存のプロジェクトでQAツールを実行することは、決して「インストールして実行」だけではありません。いくつかのことが機能する前に壊れました:

• `foundry.toml`にテストパスがなかったため0%カバレッジ:最初の`forge coverage`実行は全面的に0%を返しました。`foundry.toml`が`test = "contracts/test"`または`script = "contracts/script"`を指定していなかったため、Forgeがテストを発見していなかったことがわかりました。カバレッジコマンドは静かに成功しました—カバーするものが何もなかっただけです。これは最も誤解を招く失敗でした:有用な出力のないグリーンラン。
• forge-std v1.14.0で`InvariantTest`インポートが消えた:`Invariant.t.sol`は`forge-std`から`InvariantTest`をインポートしていましたが、これは最近のリリースで削除されました。コンパイルは不透明な「シンボルが見つかりません」エラーで失敗しました。修正はインポートを削除することでした—`Test`だけでFoundryの不変テストには十分です。
• `uint256(token.totalSupply())` vs `Balance.unwrap()`:テストは、ユーザー定義の`Balance`型から基礎となる`uint256`を抽出するために明示的なキャストを使用していました。コンパイルされましたが、それは間違ったイディオムです—`Balance.unwrap(token.totalSupply())`がUDVTシステムが設計されたものです。`Token.t.sol`、`Invariant.t.sol`、`DeploySepolia.s.sol`全体に適用されました。

パイプライン設計

すべては2つのスクリプトを通じて実行されます:

• scripts/setup-qa-tools.sh`: Slither、Halmos、Gambitをインストール(べき等)
• `scripts/run-qa.sh`: チェックを実行し、タイムスタンプ付きの結果を`qa-results/`に保存

./scripts/run-qa.sh slither gas # 静的解析 + ガスのみ
./scripts/run-qa.sh mutation # ミューテーションテストのみ
./scripts/run-qa.sh all # すべて

すべてのチェックが速いわけではありません。Slitherとカバレッジはすべてのコミットで実行されます。ミューテーションテストとHalmosは遅いです—週次またはプレリリース実行により適しています。

まとめ

ブロックチェーンQAツールチェーン:各レイヤーが捕捉するもの—静的解析からクロスレイヤープロパティテストまで

5つのQAレイヤー、それぞれが異なるクラスの問題を捕捉します。

レイヤーの説明

GambitとFast-checkがこのラウンドで最も実用的な結果を提供しました。

CIパイプライン

QAチェックは現在、6段階のパイプラインとしてGitHub Actionsに配線されています:

CIパイプライン: Build & Lintがすべての下流ステージに展開—Test、Coverage、Gas、Slither、Auditステージ

GitHub Actionsパイプライン: Build & Lintがすべての下流ステージをゲートします。

ステージの説明

参考文献

• Ethereum Account Stateソース: [github.com/egpivo/ethereum-account-state](https://github.com/egpivo/ethereum-account-state)
• 前回の記事: Ethereum Account State
• Slither: github.com/crytic/slither
• Gambit: github.com/Certora/gambit
• Halmos: github.com/a16z/halmos
• fast-check: github.com/dubzzz/fast-check
• Foundry: getfoundry.sh

備考

• この記事は私のオリジナルのブログ記事から改編されています。

---

Ethereum Account State: QA Pipeline for a Minimal TokenはもともとMediumのCoinmonksで公開され、人々はこのストーリーをハイライトして返信することで会話を続けています。