backprop — bug → spec

Plan-then-execute はコードを修正して終わり。 SDD はコードを修正し、さらにスペックを編集して再発を不可能にする。 その編集が backprop だ。

いつ BACKPROP するか

• /build 検証でテストが失敗した。
• ユーザーがバグを報告した。
• 本番環境インシデント後のポストモーテム。
• /check が根本原因を特定した VIOLATE を指摘した。

6 つのステップ

1. TRACE

失敗出力 / バグレポートを読む。 誤った動作の正確なファイル:行番号を特定する。 根本原因をシンプルな1文で命名する。

2. ANALYZE

3つの質問を自問する:

• 新しい §V invariant がこのクラスのバグを捕捉するか? (最も多いケース: はい)
• §I が間違っているか — スペックが要求する形状をコードが提供できないか? (時々)
• §T が間違っているか — 実装する必要のない機能を作ったか? (稀だが実在)

3. PROPOSE

スペック変更案を作成する。§B を絶対に飛ばさない; §V/§I/§T はケースバイケース。

テンプレート:

§B row: B<next>|<date>|<root cause>|V<N>
§V line: V<next>: <testable rule that would have caught it>

例:

§B row: B3|2026-04-20|refund job ran twice on retry|V7
§V line: V7: ∀ refund → idempotency key check before charge reversal

4. GENERATE TEST

新しい invariant をテストなしで追加 = ウソ。先に失敗テストを追加する。 テストの名前を invariant に対応させて付ける: TestV7_RefundIdempotent。

5. VERIFY

コードを修正する。テストを実行する。パスしなければならない。フルスイートを実行する。リグレッションがないこと。

6. LOG

スペック編集 + テスト + コード修正をまとめて1つのコミットにする。 コミットメッセージ: backprop §B.<n> + §V.<N>: <one-line cause>。

よい invariant とは

• コードで検証可能 (grep 可能または assert 可能)。
• ファイル単位ではなく、振る舞い単位で範囲化されている。
• 可能な限り肯定形で述べる (⊥ forbid より ! hold)。
• §I の適用先サーフェスを参照する。

悪い例: V8: コードは正しくあるべき。 良い例: V8: ∀ pg_query ! params interpolated via driver, ⊥ string concat.

いつ §V を追加しないか

• バグが純粋な機械的タイプミスで、クラスがない (i++ vs i-- 使い捨てコード内)。
• 修正が一度限りのマイグレーション。
• 根本原因が外部依存 (代わりに deps をアップグレード、§C に記す)。

それでも §B エントリは追加すること — この失敗モードが検討されたことを記録する。同じ匂いを持つ将来のバグ → §B 検索が先例を示す。

出力形式

すべての backprop 実行は以下を生成する:

1. §B エントリ (常に)。
2. §V エントリ (通常)。
3. テストファイル (§V を追加した場合)。
4. コード修正。
5. 1つのコミット。

ダッシュボードなし。ログファイルなし。SPEC.md + git が完全な履歴。