[b-2] EL Lean に対する 01e チェックリストを作成する

[grandchildrice]

📖 前提知識(共通)

SPECA は「仕様書 → 形式的なセキュリティプロパティ → 実装コードの監査」を自動化するパイプライン。フェーズは 01a(仕様収集) → 01b(サブグラフ抽出) → 01e(プロパティ生成) → 02c(コード位置解決) → 03(証明ベース監査) → 04(誤検知フィルタ)。エントリポイントは scripts/run_phase.py。

M2 の全体像(#86)= 3トラック × 4フェーズ。トラックは「どの Lean を起点に 01e を作るか」で分ける:

• a = gasper(コンセンサス層仕様。Lean 形式化は完了済み)
• b = EL spec(Execution Layer 仕様起点)
• c = vuln-dataset(NyxFoundation/ethereum-vuln-dataset の critical/high 実バグ起点)

各トラック共通のフェーズ: ①Lean形式化 → ②01e作成 → ③全クライアント監査 → ④Kurtosis再現 → 統合レポート(2-C)。

関係リポジトリ:

repo	役割	言語/実行
NyxFoundation/speca	パイプライン本体	Python 3.11 / uv。worker は Claude Code CLI
NyxFoundation/speca-lean4-plugin	Lean 形式化 + 01e emit(Lean の実行場所)	Lean 4 / lake + Python driver
NyxFoundation/ethereum-vuln-dataset	11クライアントの過去実バグ集(STRIDE/CWEラベル付き)	CSV
NyxFoundation/kurtosis-harness	findings の devnet 再現	Kurtosis

セットアップ(NyxFoundation/speca): uv sync / npm i -g @anthropic-ai/claude-code / bash scripts/setup_mcp.sh。詳細は CLAUDE.md。

---

🎯 Goal

b-1(#144)で形式化した Lean 定理を背骨に、judge/improve ハーネスで EL の 01e チェックリストを作り、品質バーを通して凍結する。

📍 このタスクの位置づけ

トラック b / フェーズ②。手法は a-2(#143)と完全に同型。違うのは入力の Lean 定理だけ。

🛠 作業場所

• リポジトリ: NyxFoundation/speca-lean4-plugin
• 主なファイル: src/speca_lean4/judge.py(a-2 と同じハーネス)、theorem_map.json、data/solodit_checklist.csv(参照バー)、data/ethereum_vulns.csv(improve 教材)
• emit(NyxFoundation/speca 側): uv run python3 scripts/run_phase.py --phase 01e --property-provider lean

📋 手順

1. b-1([b-1] EL(Execution Layer)スペックの Lean を一つ形式化する #144)の定理 → CHK-* チェックリスト項目を生成。
2. improve ループで vuln dataset の該当クラスを教材に投入し研ぎ直す。
3. src/speca_lean4/judge.py の judge で solodit 参照バー到達を確認(a-2 で確立した別系統 judge の手順を踏襲)。
4. 01e として emit、b-3 へ。

📦 成果物

• 何を: judge バー到達済みの EL 01e チェックリスト
• どこに: emit-01e で NyxFoundation/speca の outputs/01e_PARTIAL_*.json、CHK-* は theorem_map.json が正本
• 形式: 01e スキーマ準拠

✅ 完了条件

• EL 01e が judge バー到達(a-2 と同じ品質基準・別系統込み)
• 01e を凍結し b-3 へ引き渡し可能

⚙️ 制約

• 締切: 2026-08-15
• 依存: b-1([b-1] EL(Execution Layer)スペックの Lean を一つ形式化する #144)の完了
• スコープ外: 監査実行(b-3)

🔗 参考

• 手法の原型: a-2([a-2] gasper spec の 01e チェックリストを作成・仕上げる #143)/ judge ハーネス: plugin#22

[grandchildrice]

https://github.com/NyxFoundation/speca-lean4-plugin/tree/main/outputs/20260812-ethtotal