feat(ethvuln): add ethereum-vuln-dataset track c-1 formalization — 66 statements, proofs deferred (speca#146)

[banr1]

speca#146（トラック c / フェーズ①）の成果。NyxFoundation/ethereum-vuln-dataset の critical/high 全 66 エントリ（CRITICAL 3 / HIGH 63、dataset ref c7c4ccbc46aaaeb8b4d3abf18a81f587d2ba017e）について、各バグが破っていた不変条件を Lean 4 の命題として形式化し、lean/SpecaExport/EthVuln/ に配置して 専用 map theorem_map_ethvuln.json に登録する（第 3 トラック。gasper の theorem_map.json は無変更）。

改訂メモ 2（レビュー対応、CHANGES_REQUESTED への応答）: @grandchildrice さんの 4 指摘（must-establish への前提混入 / ArithAgrees の wrapping 許容 / availability のトートロジー / 仕様アンカーと忠実性）にすべて対応した。詳細は下記「レビュー対応」と docs/ethvuln-track.md の該当セクション。この対応の副産物として、全 66 定理が証明済み（sorry なし） になった。あわせて main（EthTotal の audit packet 対応 27dc1d8 / 5c0755b）に rebase している。

レビュー対応（改訂 2 の内容）

1. 結論ガードの must-establish 混入（inline 1 + 本文） — exporter は型全体を forallTelescope で平坦化するため、∀ c k, k < len c → … 形の結論からガードが漏れ、must-establish 130 件中 29 件（約 22%）が入力・文脈条件だった。全定理の結論を Common の名前付き述語 1 適用（AccessesInBounds / SpecEquivOn / AcceptanceCarriesOver / AcceptsOnlyValid / OnAccept / PreservesInvOnTrace / GrantedOnlyVerified …）に畳み、加えて exporter の A2 ヒューリスティックに rule 4: 匿名（hygienic 名）Prop 束縛子 → context-precondition を追加した（ProjectConfig.contextualizeAnonymousGuards による opt-in、有効なのは ethvuln トラックのみ。gasper は該当 0 件、EthTotal は既存分類を維持 — 匿名ガード 17 件があるため、opt-in はメンテナ判断に委ねる）。結果: must-establish は 115 件・全件が名前付きの実装義務、context-precondition は 0 件（規約で畳み切ったため）。tests/test_ethvuln.py が両方を回帰ピンする。
2. 算術述語の分離（inline 2） — ArithAgrees は「数学的結果が幅に収まる場合のみ一致」を要求するため、脆弱な wrapping 実装自身が仮定と結論の両方を満たしてしまっていた（websocket / geth p2p / Juno の 3 件で、定理が対象のバグを排除できていなかった）。廃止し 2 系統に分離: AgreesModWidth（全定義域での mod-2^n 厳密一致。仕様自体が modulo 意味論を定める consensus uint64 / EVM ガスワード用）と CheckedArith / AcceptedExact（Option 値の checked 演算 — オーバーフローは必ず検出。wrapping 実装は some を返し続けるため満たせない）。重要な点として、AgreesModWidth 系の spec 側は自由パラメータにせず具体関数に固定した（uint64 加算は Nat.+、Besu CALL ガス 2 件は Common の evmCallGas = EIP-150 の 63/64 ルール + min のモデル）— spec を自由にすると縮小実装が spec を自分に合わせて選べてしまい、排除にならないため。EVM のシフト / MULMOD は仕様条項そのもの（ShiftSaturates / SarSaturates / MulModZeroTotal。シフトの閾値は仕様どおり 256 以上の全域とし、ビット 31 の値はその部分域として docstring に記録）を述べ、仕様モデル上で証明した。
3. availability のトートロジー解消（inline 3） — hTotal は NeverCrashes の言い換えだった（15 件中 11 件が実質 P → P）。実装が守る具体的な 2 条件 — RejectsMalformed（malformed 入力は状態を変えずに正常拒否 = パース/検証の全域性 + ロールバック）と TotalOnWellFormed（整形式入力の全域処理。リソース枯渇・内部エラーも状態を保存する定義済み拒否に落ちる）— に分解し、NeverCrashes は補題 neverCrashes_of_split で導出。詳細非公開エントリではこの段階分解がモデリング選択であり dataset の記載事実ではないことを各 docstring に明記した。
4. 仕様アンカーと忠実性（issue コメント） — 全 66 エントリに per-entry の x_spec_anchor を付与: protocol semantics に対応する 20 件は consensus-specs / execution-specs の section + x_spec_symbol（例: MULMOD → execution-specs:…/vm/instructions/arithmetic.py::mulmod、Lodestar AttesterSlashing → consensus-specs:specs/phase0/beacon-chain.md::process_attester_slashing）、仕様対象外の 46 件は 明示的な N/A — <category>: <reason>（dependency-library 19 / client-internal 9 / rpc-api 8 / networking-devp2p 6 / undisclosed 4）として実装安全性側に区分。キュレーションは data/ethvuln_spec_anchors.json に収載。ラベルテーブルにも beacon-chain:execution-payload 行を追加（beacon-chain:sync-committee は当該 1 件のラベル自体が dataset 側で誤りのため行を追加せず、per-entry アンカーで process_effective_balance_updates を指す — upstream 再キュレーション候補）。汎用形で覆ったエントリの docstring には entry 固有条件と抽象化部分を明記した。
5. EthTotal 形式の分離出力（本文） — 全エントリに 決定的 audit_packet（tools/ethvuln-build-packets.py、LLM 不使用・冪等）。指摘の三分割をキーとして明示した: guarantee = Lean の結論そのもの、obligations = 実装が確立すべき性質（must-establish 仮説の名前と正確な型）、preconditions = A2 クラスタグ付きの全仮説リスト（EthTotal 互換の表現）、supporting_facts = ルート結論の exact fact + 実装義務 1 件ごとの exact fact（FACT-OB*）。emit-01e で全 118 プロパティに載る。packet は proof status を持たない（status は従来どおり exporter のみ）。CI の lean ジョブに staleness ゲート（export した health + data/ethvuln_spec_anchors.json から packet/アンカーを再生成して git diff --exit-code theorem_map_ethvuln.json、EthTotal の gate と同形）を追加した。あわせて map の assertion 文 10 件（算術 9 + memory-safety 1）を新述語に一致するよう更新した。

正直な残余（先に自己申告しておく）:

• 非公開アドバイザリ 2 件（Grandine 2.0.4 / 2.0.5）は当初 SpecEquivOn → SpecEquivOn の恒等になっていたため、エントリ固有の観測（2.0.5 = エポック遷移後のレジストリ観測、2.0.4 = ヘッド選択）での一致 AgreeOnObservation を結論とする形に強化した。must-establish は仕様準拠 hConform のまま。
• eff1234（jsonparser OOB read）は「読み取り前の境界チェック」という修正が破られた不変条件そのものなので、含意は定義の展開である（docstring に明記。監査内容は must-establish 側）。
• 仕様条項 3 件（Besu シフト ×2・geth MULMOD）は must-establish を持たない。Lean の定理はモデル上の仕様条項を証明し、実装義務は emit されるプロパティの assertion（「クライアントの演算がこの条項を満たすこと」）として 02c で結び付ける。
• 結論が「名前付き述語 1 適用」でない例外は 2 件のみ: a528f48 の定数不等式 400 * 1024 ≤ implMaxProofSize と GHSA-7pg2 の連言 ShiftSaturates ∧ SarSaturates（いずれもガードなしの閉形式、docs に記載）。

変更内容

パス	内容
lean/SpecaExport/EthVuln/Common.lean	共有定義。算術 2 系統（AgreesModWidth / CheckedArith+AcceptedExact）、availability 分解（RejectsMalformed / TotalOnWellFormed）、resource 3 条件（UsageAccounted / AdmissionControlled / RejectFrees）、受理事後条件（OnAccept / AcceptsOnlyValid）、spec-equiv 系（Agree / AcceptanceCarriesOver / AgreeOnObservation / ProducesSpecValid / PreservesInvOn / PreservesInvOnTrace）、crypto 系（RejectsInvalid / GrantedOnlyVerified / EstablishedAreValid）と、それらの分解補題（証明付き）
lean/SpecaExport/EthVuln/Props/*.lean	66 定理を「名前付き実装義務 ⇒ 名前付き述語の結論」に統一し、全件証明（各 1 行〜数行、共有補題経由）
lean/SpecaExport/Basic.lean	A2 rule 4（匿名 Prop 束縛子 → context-precondition、contextualizeAnonymousGuards opt-in、ethvuln のみ有効）
lean/MainEthVuln.lean + lean/lakefile.lean	専用 exporter エントリ lake exe speca-export-ethvuln（前回どおり）
theorem_map_ethvuln.json	66 件 + per-entry x_spec_anchor / x_spec_symbol + audit_packet。proof status 用フィールドは引き続き持たない
data/ethvuln_spec_anchors.json	per-entry アンカーのキュレーション（N/A は category + reason 付き）
data/anchor_map.json	beacon-chain:execution-payload 行を追加（+14 行のみ）
tools/ethvuln-build-packets.py	packet + アンカーの決定的・冪等な再生成ツール（LLM 不使用）
src/speca_lean4/cli.py	_run_lean が map の lean_exe / x_src_roots を尊重（前回どおり）
src/speca_lean4/health.py	context_preconditions アクセサ
tests/test_ethvuln.py ほか	従来の honesty 不変条件 + 新規 3 テスト（義務は名前付きのみ / アンカーの存在と形式 / packet と health の厳密同期）
README.md, docs/ethvuln-track.md, docs/pipeline.md	レビュー対応の全記録

クラス別内訳（66 件、変更なし）: availability-robustness 15 / resource-bounds 14 / spec-equivalence 13 / arithmetic-safety 9 / memory-safety 4 / input-validation 4 / crypto-auth-integrity 4 / state-integrity 2 / serialization-fidelity 1。

proof status

全 66 定理が証明済み（sorry なし）になった。 ただし枠づけを正直に: この証明は設計上「浅い」。再定式化の目的が「監査内容を仮説側に、保証される不変条件を結論側に正しく配ること」であり、その帰結として含意が数行の補題適用になった、というのが実体である。proved が保証するのは (a) その含意、(b) Common の分解補題群（neverCrashes_of_split・boundedUsage_of_admission・リスト帰納法など、小さいが実内容のある部分）、(c) 命題群が整合的で空虚でないこと — であって、実クライアントが義務を満たすかどうかはまさに 02c の監査対象である（must-establish 分解された 115 プロパティがその作業項目）。**issue #146 の「proved」完了条件を字義上は満たすが、その実体は上記のとおりなので、完了判定は issue 側の判断に委ねたい。**map は引き続き proof status を一切持たず、status は exporter（health JSON）だけが決める。CI・テストは値ではなく pairing（proved ⇔ sorry_free）と「emit された status = exporter の status」を検証するので、sorry への退行も今日の proved と同じ正直さで報告される。なお一部の定理は分解補題経由で Classical.choice に依存する（choice_free=false 18 件、exporter が正直に表示）。

検証

(cd lean && lake build)                    # Build completed successfully — sorry 警告 0
(cd lean && lake exe speca-export-ethvuln --targets targets_ethvuln.txt --output health_ethvuln.json --src-root .)
                                           # 66/66 resolved, all proved / sorry_free=true
                                           # must-establish 115（全件名前付き）、context-precondition 0
python3 tools/ethvuln-build-packets.py --map theorem_map_ethvuln.json \
  --health tests/fixtures/theorem_health.ethvuln.sample.json \
  --anchors data/ethvuln_spec_anchors.json     # 冪等（再実行で diff 0）
speca-lean4 emit-01e --map theorem_map_ethvuln.json \
  --scope tests/fixtures/bug_bounty_scope.ethvuln.sample.json \
  --health-json tests/fixtures/theorem_health.ethvuln.sample.json --out 01e_ethvuln.json
                                           # 118 properties（115 must-establish 分解 + 3 仕様条項）、
                                           # 全件 proved、全件 audit_packet 付き
pytest -q                                  # 201 passed, 3 skipped

main の既存破損への対処: tests/test_frontier.py の 3 テストは未コミットの生成物 lean-ethtotal/health.json を要求し、main の CI 自体が 27dc1d8 以降 red（committed の health.mapped.json は Lemmata 層がトリミング済みで代替不可）。本 PR では成果物欠如時に理由付きで skip する最小修正を入れ、成果物がある環境では従来どおり実行される。別の直し方が良ければ従います。

ci.yml の lean / python / run-lean-e2e 各ジョブの ethvuln ステップはローカルでそのまま再生して exit 0 を確認（--run-lean 経路含む）。

レビューで見てほしい点（改訂 2）

1. A2 rule 4 の scope — context-precondition 分類は opt-in にし、gasper / EthTotal の既存 export をバイト安定に保った。EthTotal には匿名ガードが 17 件あるため、opt-in するかは EthTotal 側の判断として分離した。この整理で良いか
2. availability の段階分解 — RejectsMalformed + TotalOnWellFormed は提示いただいた malformed input / resource exhaustion / state rollback を仮説側（= B2 で 01e の監査項目になる側）に置く設計。conclusion 側は導出された NeverCrashes。この配置で意図に合っているか
3. upstream 再キュレーション候補 — 42783aef（Reth 1.0 リリースノート、脆弱性ではない）と GHSA-wm9c（ラベル beacon-chain:sync-committee だが実体は Electra effective-balance）は ethereum-vuln-dataset 側の再キュレーション候補として挙げたい

補足

• 生成元 banr1/eth-vuln-formal-props（private）には本改訂の Lean ソースと map 生成の追随を別途同期する
• LF 維持（変更ファイルすべて CR=0）
• self-merge しない

Refs NyxFoundation/speca#146

[grandchildrice]

SPECA 02c での実装／関数への紐づけはこの PR の範囲外として見ています。sorry も問題ありません。

ただし、01e に落としたときの obligation の意味付けは修正が必要です。must-establish に入力・初期状態の前提が混ざっており、算術系も wraparound を許す定義と overflow-safe な要求の区別がつきません。EthTotal のように、実装が保証すべき性質と precondition、さらに exact な監査 assertion を分けて出力できる形にしたいです。

[grandchildrice]

ここで k < len c まで 01e の must-establish に分解されますが、これはアクセス時の入力／文脈条件で、実装全体が保証する性質とは別です。hWindowChecked のような実装 obligation と分離して出力してください。

[banr1]

ご指摘のとおりで、exporter が型全体を forallTelescope で平坦化するため、結論の ∀/→ ガードが must-establish に漏れていました(この k < len c を含め 130 件中 29 件・約 22% が入力/文脈条件でした)。二段で修正しています。

1. statement 側: 全定理の結論を Common の名前付き述語 1 適用に畳みました。この定理の結論は AccessesInBounds size (fun c => (List.range (len c)).map (base c + ·)) になり、must-establish は実装 obligation の hWindowChecked だけです(ガードは述語の内側)。
2. exporter 側(再発防止): A2 に rule 4 を追加 — 匿名(hygienic 名)の Prop 束縛子は context-precondition に分類し、B1 は property 化せず、audit packet の preconditions に載せます(contextualizeAnonymousGuards による opt-in で、有効なのは ethvuln のみ。gasper は該当 0 件、EthTotal は既存分類を維持)。

tests/test_ethvuln.py::test_obligations_are_named_and_guards_are_folded が「must-establish は名前付き obligation のみ・context-precondition の残留ゼロ」を回帰ピンします。現在の must-establish は 115 件・全件名前付きです。

[grandchildrice]

ArithAgrees は結果が 2^n 未満の場合だけ exact equality を要求し、各 theorem の仮定は % 2^n です。この形だと、overflow-safe な property のつもりでも通常の wrapping 実装が仮定を満たします。EVM の modulo semantics 用と、narrowing／overflow を禁止する用で predicate を分けてください。

[banr1]

ご指摘のとおりです。特に overflow 系 3 件(gorilla/websocket・geth p2p・Juno)では、脆弱だった wrapping 実装自身が % 2^n の仮定と ArithAgrees の結論の両方を満たしてしまい、定理が対象のバグを排除できていませんでした。ArithAgrees(と未使用の SignedArithAgrees)は廃止し、提案どおり 2 系統に分離しました。

• AgreesModWidth(modulo semantics 用): 全定義域での mod-2^n 厳密一致。仕様自体が modulo 意味論を定める consensus uint64 / EVM ガスワード用で、Lodestar の IEEE-754 経由や Besu の 32bit 縮小が反例になります。
• CheckedArith / AcceptedExact(overflow 禁止用): Option 値の checked 演算で、オーバーフローは必ず検出(none)。wrapping 実装は常に some を返すため満たせません。結論 AcceptedExact は下流の上限チェックが依存する「受理値の厳密性」です。

1点補足すると、AgreesModWidth 系は spec 側を自由パラメータにせず具体関数に固定しています(uint64 加算は Nat.+、Besu CALL ガス 2 件は Common の evmCallGas = EIP-150 63/64 ルールのモデル)。spec を自由にしたままだと、縮小実装が「spec を自分に合わせて選ぶ」インスタンス化で仮定・結論を両方満たせてしまうためです。

EVM のシフト / MULMOD は破られた仕様条項そのもの(ShiftSaturates / SarSaturates / MulModZeroTotal。シフト閾値は仕様どおり 256 以上の全域)を述べ、仕様モデル上で証明済みです。これら 3 件は must-establish を持たず、実装義務は emit されるプロパティの assertion として 02c で結び付ける整理です。

[grandchildrice]

Outcome が ok / reject / crash の3値なので、この hTotal は NeverCrashes h とほぼ同じ内容です。01e に出る availability property が定義の再掲になります。malformed input、resource exhaustion、state rollback など、実装が守る具体的な条件を conclusion 側に出せる形にしたいです。

[banr1]

トートロジーでした(availability 15 件中 11 件が実質 P → P)。挙げていただいた malformed input / resource exhaustion / state rollback に沿って、実装が守る具体的な 2 条件に分解しました。

• RejectsMalformed h wellFormed: 整形式でない入力は状態を変えずに正常拒否(パース/検証の全域性 + rollback)
• TotalOnWellFormed h wellFormed: 整形式入力の全域処理。resource exhaustion や内部エラーも、状態を保存する定義済みの reject に落ちる

結論 NeverCrashes は補題 neverCrashes_of_split で導出します(証明済み)。B2 の lowering ではこの 2 条件がそれぞれ独立の must-establish プロパティ = 01e の監査項目になるので、「具体的な条件を 01e に出す」要件はこの配置で満たしている認識です(結論側を conjunction にする形が好ましければ調整します)。

正直な注記を2点: (1) wellFormed は自由パラメータで、監査時に対象コンポーネント自身の検証述語で具体化される想定です。したがってこの分解が NeverCrashes に対して形式的に上乗せする正味の内容は「拒否は状態を変えない(rollback 規律)」であり、残りは監査を malformed 経路 / well-formed 経路に分けて誘導する構造です。(2) 詳細非公開のエントリでは、この段階分解が標準的なクラッシュベクタに基づくモデリング選択であって dataset の記載事実ではないことを各 docstring に明記しました。

[grandchildrice]

追加で、01e の中身に関するレビュー観点として以下を確認したいです。

• 仕様アンカー: EthTotal では各 property に execution-specs のファイル／シンボルがあります。EthVuln も protocol semantics に対応する entry には consensus-specs / execution-specs の section または symbol を Lean の docstring か map に残してください。Log4j や依存ライブラリのように仕様対象外のものは N/A と明記し、実装安全性として別扱いにしてください。
• dataset との忠実性: 同じ汎用 theorem で複数 entry を覆う場合、docstring に「その entry で追加される条件」と「抽象化した部分」を明記してください。dependency/DoS と consensus divergence を同じ NeverCrashes / SpecEquiv に落とすだけでは、02c で具体的な監査項目にならないケースがあります。

01e の生成物を fixture / outputs/ に追加することは、この PR には求めません。

[banr1]

4つの指摘、すべてに対応しました。

• must-establish への前提混入: 結論を named 述語 1 適用に統一 + exporter の context-precondition 分類(ethvuln のみ opt-in)。must-establish 130→115 件、全件が名前付きの実装 obligation。
• 算術の分離: ArithAgrees 廃止 → AgreesModWidth(modulo semantics)/ CheckedArith+AcceptedExact(overflow 検出)。wrapping 実装は仮定を満たせなくなりました。
• EthTotal 形式の分離出力: 全エントリに決定的 audit_packet。ご指摘の三分割をキーとして明示しています — guarantee(Lean の結論そのもの)/ obligations(実装が確立すべき性質 = must-establish 仮説の名前と正確な型) / preconditions(A2 クラスタグ付き全仮説、EthTotal 互換表現)/ supporting_facts(ルート + 義務 1 件ごとの exact fact FACT-OB*)。tools/ethvuln-build-packets.py で health から冪等に再生成でき、LLM は使いません。emit された 118 プロパティ全件に載ります。
• 副産物: 再定式化の帰結として全 66 定理が証明済みになりました(sorry ゼロ。choice_free=false 18 件は exporter が正直に表示)。ただしこの証明は設計上「浅い」ものです — 監査内容を仮説側に正しく配った帰結であり、証明されたのは含意・分解補題・命題群の整合性です。#146 の「proved」完了条件を字義上満たしますが、実体は上記のとおりなので完了判定は issue 側に委ねます。 map は引き続き proof status を持たず、status は exporter のみが決めます。

以下、補足です:

• context-precondition 分類は opt-in にし、gasper / EthTotal の export をバイト安定に保ちました(EthTotal には匿名ガードが 17 件あり、opt-in はそちらのメンテナ判断に委ねるのが筋と考えたため)。なお ethvuln では statement 規約でガードを畳み切ったため、この分類は現状 0 件です — テストが「must-establish に匿名が混ざらない・context-precondition の残留ゼロ」を回帰契約としてピンする、という位置付けです。
• 非公開の Grandine 2 件は当初 SpecEquivOn → SpecEquivOn の恒等でした。エントリ固有の観測(レジストリ / ヘッド選択)での一致 AgreeOnObservation を結論に置く形へ強化しています。eff1234 は修正 = 不変条件そのもののため含意が定義の展開であること、仕様条項 3 件が must-establish を持たないことは docstring / docs に明記しました。
• CI に map の staleness ゲート(EthTotal と同形: health + data/ethvuln_spec_anchors.json から packet/アンカーを再生成して diff ゼロ)を追加しています。
• 無関係の既存問題 1 件: tests/test_frontier.py の 3 テストが未コミット生成物 lean-ethtotal/health.json を要求し main の CI 自体が 27dc1d8 以降 red だったため、成果物欠如時に理由付き skip する最小修正を同梱しました(別の直し方が良ければ従います)。

この整理で問題ないか見ていただきたいです！確認お願いします。

[banr1]

仕様アンカー / dataset 忠実性の観点(#issuecomment-5312990851)への返信です。

• 仕様アンカー: 全 66 エントリに per-entry の x_spec_anchor を map に付与しました。protocol semantics に対応する 20 件は consensus-specs / execution-specs の section + x_spec_symbol(例: MULMOD → execution-specs:…/vm/instructions/arithmetic.py::mulmod、Lodestar AttesterSlashing → consensus-specs:specs/phase0/beacon-chain.md::process_attester_slashing)。仕様対象外の 46 件は明示的な N/A — <category>: <reason>(dependency-library 19 / client-internal 9 / rpc-api 8 / networking-devp2p 6 / undisclosed 4)とし、実装安全性として区分しています(Log4j 2 件は dependency-library)。キュレーションは data/ethvuln_spec_anchors.json、検査は tests/test_ethvuln.py::test_every_entry_has_an_explicit_spec_anchor。ラベルテーブルには beacon-chain:execution-payload 行を追加し、label 由来の spec_reference も 01e に出ます。
• dataset との忠実性: 汎用形で覆ったエントリの docstring に「entry 固有の条件」「抽象化した部分」「(非公開アドバイザリでは)段階分解がモデリング選択であること」を明記しました。また dependency/DoS と consensus divergence は同じ述語には落ちません — 前者は RejectsMalformed/TotalOnWellFormed(+ resource 系 3 条件)、後者は SpecEquivOn/AcceptanceCarriesOver/AgreeOnObservation と、監査項目が分かれます。
• upstream 再キュレーション候補(ご相談): 42783aef(Reth 1.0 リリースノート — 脆弱性ではなく安定性の主張)と GHSA-wm9c(ラベルは beacon-chain:sync-committee だが実体は Electra の effective-balance 処理)は ethereum-vuln-dataset 側での再キュレーション候補として挙げたいです。後者は per-entry アンカーでは内容基準で process_effective_balance_updates を指しています。
• 01e 生成物の fixture / outputs/ への追加は、ご指示どおり本 PR では行っていません。