メインコンテンツまでスキップ

コンテキスト工学

SPECA で最も成果に響いた設計判断は、プロンプトを読んでも、オーケストレータのコードを見てもそれぞれ単独では見えません。各フェーズが次のフェーズのコンテキストウィンドウに何を入れ、何を意図的に入れていないか に表れます。本ページはその判断を 1 ヶ所に集約したものです。

1. Subgraph index — 仕様コンテキストをスケールさせる​

問題. Phase 02c はすべてのプロパティを仕様コンテキストに紐づけ直す必要があります (どの関数名が出るか、どの状態が関与するか)。これがないと tree-sitter のシンボル解決が地に足のつかない推測になります。Phase 02c がプロパティごとに 01b の partial を全部読み直すと、コンテキスト消費が項目あたり解決自体より高くなる規模に膨らみます。

解決. Phase 02c のロード時に、オーケストレータが一度だけ outputs/01b_SUBGRAPH_INDEX.json を構築します — 仕様要素 ID から関連フィールド (関数名・状態遷移・mermaid ファイルパス) への簡潔な逆引きインデックスです。ワーカープロンプトはこのインデックスをコンテキストの一部として受け取り、必要なエントリだけ参照します。

結果. Phase 02c の項目あたりコンテキストが「全 01b partial」から「subgraph index へのヒット 1 つ + プロパティ本体」へ縮みました。これが CLAUDE.md に書かれている Phase 03 トークン削減 40〜60% の主な貢献者です。

インデックスは Phase 02c ランごとに再構築されます。コミット対象でも、フェーズ間契約の一部でもなく、オーケストレータが所有する派生 artifact です。

2. 02c でのコード事前解決 — 1 度払って 03 で取り返す​

問題. Phase 03 (監査) が自力でプロパティに対応するコード位置を発見するなら、すべての監査が "search/read flailing" フェーズで始まります。経験的にこの flailing が初期 SPECA で最大のコスト項目でした。

解決. プロパティ生成と監査の間に Phase 02c というフェーズを 1 つ挟み、事前解決だけをやらせます:

  • 各プロパティに対し、主要なコードシンボル (function / struct / modifier) を見つける。
  • ファイルパス・行範囲・ロール (primary / caller / callee / state-management) を記録。
  • シンボルが解決できないプロパティを not_found / specification_only / out_of_scope でマーク → 03 が安価にスキップ。
  • ここで Informational プロパティをドロップ — 監査予算を割く価値がない。

結果. Phase 03 は code_scope フィールドが事前埋めされた状態でプロパティを受け取ります。プロンプトは事前解決の使用を要求し、それ以外を short-circuit するように書けます: 実環境の Phase 03 は今や大半が証明推論で、コード grep ではありません。

プロンプトの diff としては映えない判断ですが、ベンチマークラン全体での回収は莫大です。

3. Phase 04 の recall-safe なゲート順序​

問題. 3 ゲートフィルタの良し悪しは順序と却下基準で決まります。素朴な設計 — 「大半は in-scope なのでスコープを最初に見る」 — は速いですが、dead code finding が gate-3 予算を浪費します。

解決. ゲートは 正しい却下が最も安いものから 順に並べ、DISPUTED_FP で early exit します:

  1. Dead Code — 構造的判定。最も安く、最も厳しい "不当却下しない" 基準 (unreachable! / panic! / 到達しない return / 明示的 stub にしか発火しない)。
  2. Trust Boundary — 意味的判定。proof gap を横断する入力が攻撃者制御可能かを問う。広いが、却下の根拠が具体的 (特定入力が internal だと識別される)。
  3. Scope Check — ポリシー判定。proof gap の位置が BUG_BOUNTY_SCOPE.json の in_scope に当たるかを問う。意味的には最も安い (パスマッチ) が最後に置く — そうしないと、前 2 ゲートが有用な根拠を残せたはずの finding を食ってしまう。

Phase 03 vs 04 のチャート で recall がフィルタを通して 100% を維持しつつ precision が 56.9% → 66.7% に上がっているのが、ゲート順序と却下基準が正しく較正されている経験的証拠です。

なぜどのゲートも "soft-reject" できないのか. ゲートは DISPUTED_FP を宣言する (フィルタする) か、findings を変更せず通過させるかのいずれかです。ゲートレベルでの "downgrade" 判定はありません。Downgrade は別途、すべてのゲート通過後に行います。これが重要なのは recall 分析が成り立つからです: 真陽性が落ちたなら、どのゲートが落としたかが正確に判明します。

4. Partial ファイルがフェーズ間契約​

outputs/<phase>_PARTIAL_*.json はログのアーティファクトではなく、フェーズ間契約そのもの です。下流フェーズはすべて上流の partial を glob で消費します。

これが嬉しい性質を 3 つ持ちます:

  1. Resume はディレクトリスキャン。 ステート DB なし、ラン UUID なし、整合性合わせなし。クラッシュリカバリは「partial をリストし、その項目 ID をスキップ」だけ。
  2. Partial 出力は first-class。 80% の項目を完了したフェーズは partial の 80% を書き出し、次フェーズはその 80% をそのまま消費します。これが --budget 制約付きランを有用にします: 安価で不完全な出力でも反復できる。
  3. クロスフェーズ検証は glob 時に走る。 02c が 01e partial を読むとき、各ファイルを Phase 01e の Pydantic スキーマで検証します。フェーズ間スキーマがズレれば境界で大きな声で失敗 — 監査の途中で静かに腐ったりしません。

トレードオフはファイル数の多さ。代替 (SQLite など) は不透明で grep しづらく、ベンチマーク成果物として publish しづらいので、ディスク使用量を許容しています。

5. Slim な 01e スキーマ — covers は文字列​

Phase 01e の初期版では各プロパティに豊富なサブグラフコンテキストを付与していました: 状態リスト、遷移リスト、RFC 2119 全文引用。やがて気付きました — このコンテキストは Phase 02c でも 03 でも使われていない (02c は subgraph index を持ち、03 はコード事前解決を持つ)。豊富なコンテキストは 01e partial を太らせるだけのデッドウェイトでした。

今日の 01e_PARTIAL_*.json は意図的にスリムです:

  • covers は単一文字列 (主要な仕様要素 ID、例: "FN-001") — サブグラフ断片のリストではない。
  • reachability はちょうど 4 フィールド: classification, entry_points, attacker_controlled, bug_bounty_scope。

原則: 下流で消費されないものは上流で生み出さない。 "将来の拡張のために残しておく" は誘惑だが、実際には後段すべてを遅くするだけ。

6. 領域非依存な STRIDE + CWE Top 25 — Ethereum 固有の埋め込みなし​

Phase 01e はプロパティ生成の脳です。初期版には Ethereum 固有テンプレート ("コンセンサスプロトコルなら fork choice を問う") がありました。Ethereum 仕事には速いものの、それ以外の領域からはロックアウトされます。

現在の Phase 01e プロンプトは STRIDE を一般的な思考フレームワーク、CWE Top 25 (CWE-22 / 78 / 89 / 94 / 200 / 502 / 639 / 770 / 862) を具体的なパターン として使います。Ethereum 固有の知識はプロンプトではなく BUG_BOUNTY_SCOPE.json 経由で入ります。

これにより、同じ SPECA ビルドが RQ1 (Ethereum クライアント)、RQ2 (任意の C/C++ OSS)、探索的な RQ2b (プロトコルファジング) すべてを、プロンプトのフォークなしに走ります。

7. なぜオーケストレータはプロンプトを編集しないのか​

エージェントフレームワークによっては、フェーズ状態に応じて動的にプロンプトを構築・変異させるものがあります。SPECA はそうしません。各プロンプトは prompts/ 下の静的ファイルです。オーケストレータの仕事は、3 つのテンプレートフィールド (QUEUE_FILE, CONTEXT_FILE, OUTPUT_FILE) を埋めて claude --prompt-path に渡すだけです。

理由: 動的プロンプトはレビュー不可能。 監査パイプラインが実行時に自分の指示を変えるなら、もはや「ある finding に対してエージェントに何を指示したか」を 1 つの artifact で示せません。git に置いた静的プロンプトが、SPECA の証明試行手法をエンドツーエンドで監査可能に保っている仕組みです。

まとめ​

このページの判断が、SPECA の出力を「リポジトリにエージェントを放つ」だけのパイプラインから分けています:

  • Subgraph index — コンテキスト量を項目あたりコストから切り離す。
  • コード事前解決 — 02c で 1 度払い、03 の flailing をスキップ。
  • Recall-safe なゲート順序 — 安価な却下を先に、意味的判定を中、ポリシーを最後。soft-reject は無し。
  • Partial が契約 — Resume が無料、検証は境界で。
  • Slim な 01e — 消費されないものは生まれない。
  • 領域非依存な Phase 01e — 領域知識は BUG_BOUNTY_SCOPE.json から、プロンプトからは無し。
  • 静的プロンプト — すべての監査判断は単一のコミット済み artifact にトレースできる。