prove-patch

パッチの証明

元のベースライン、最終パッチのコミット、宣言された repair_scope、変更されていない再現パッケージを使用します。記録の契約を読んでください。パッチを編集したり、未コミットのツリーを検証したりしないでください。新しい試行で失敗があれば返してください。 対象のコマンドを実行する前に、そのプロジェクトのガイダンスに従ってください。

1. パッチ作成者の結論を参考にせず、スコープ内のケースとパッチを確認します。計画した各入力を、同じ保持済みハーネスのソースとコマンドを使って、クリーンなベースラインツリーとパッチ適用済みツリーで実行します。ハーネスは、実行した入力と観測結果に基づく PATCH_CASE {"input": ..., "actual": ...} を正確に1行出力し、その後、アサーションの直前に標準出力の最後の行として PATCH_REACHED を出力する必要があります。代表ケースはベースラインで失敗し、パッチで成功する必要があります。有効なコントロールケースは両方で成功する必要があります。ベースラインとパッチ適用済みの標準出力、標準エラー、終了ステータス、経過時間、コマンド、ハーネスのソースを receipts/ に保存します。タイムアウト、セットアップの失敗、マーカーの欠落、入力の不一致、曖昧な観測は、証拠の欠落です。信頼できるパッチ適用済み環境での失敗は、問題として記録します。証拠の欠落を成功と見なしてはいけません。
2. パッチに関連するプロジェクトのチェックを実行し、同じ生の証跡を保存します。動作チェックと、失敗したプロジェクトチェックの原因を特定する際には、ベースラインとの比較を行います。パッチ適用済みのテストスイートが成功した場合は、ベースラインでの実行を省略できます。関連する場合は、重点テスト、回帰チェック、セキュリティチェックを含めます。立証されていない具体的な制限を記録します。リストが空の場合、結果は未確定です。
3. 記録の契約に記載された証明タイプのレシピ、reproduce.baseline_commit、最終 patch_commit を指定して、3 アームヘルパーを実行します。ベースラインが失敗し、パッチが成功し、ベースライン全体を元に戻した場合に再び失敗することを確認します。receipts/source.json にピン留めされたコミットが記録され、元に戻したツリーが元のベースラインツリーと一致することを確認します。そのタイプに必要なビルド識別結果を確認します。ソースツリー、ビルド、実行のすべての証跡を保存します。
4. prove.json と、それおよびすべての証跡を対象とする最終マニフェストを作成します。次に、バリデーターを使って uv run --no-project <script> manifest <prove-attempt-dir>、続いて uv run --no-project <script> check <run-dir> を実行します。報告前に、ネイティブ証明評価と生の証跡を独立して確認します。完全な証明には、問題も証拠の欠落もありません。正確な失敗内容と証跡のパスをオーケストレーターに返してください。

証明レコードのスキーマ:

{
  "schema_version": 2,
  "attempt": 1,
  "failure_type": "runtime",
  "baseline_commit": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa",
  "patch_commit": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb",
  "reverted": "pass",
  "build_identity": "pass",
  "hashes": {
    "baseline": "1111111111111111111111111111111111111111111111111111111111111111",
    "patched": "2222222222222222222222222222222222222222222222222222222222222222",
    "reverted": "1111111111111111111111111111111111111111111111111111111111111111"
  },
  "reverted_hash_note": null,
  "cases": [{
    "check_id": "reported-input",
    "argv": ["python", "receipts/case.py", "reported-input"],
    "source": "receipts/case.py",
    "runs": {
      "baseline": {"exit_code": 1, "elapsed_ms": 15, "stdout": "receipts/case-base.stdout", "stderr": "receipts/case-base.stderr"},
      "patched": {"exit_code": 0, "elapsed_ms": 14, "stdout": "receipts/case-patched.stdout", "stderr": "receipts/case-patched.stderr"}
    }
  }],
  "project_checks": [{
    "check_id": "focused-suite",
    "kind": "suite",
    "argv": ["pytest", "tests/test_upload.py"],
    "baseline": null,
    "patched": {"exit_code": 0, "elapsed_ms": 860, "stdout": "receipts/suite.stdout", "stderr": "receipts/suite.stderr"}
  }],
  "unproven": ["Inputs outside the declared boundary were not assessed."],
  "agent": "prover-1"
}

範囲が限定されたクラスでは、異なる失敗代表ケースを少なくとも2つと、有効なコントロールケースを含めてください。レコードでは、計画したすべてのケースを一意の check_id で網羅する必要があります。両方のコミットで同じハーネスとコマンドを使用し、どちらの側かをハーネスに知らせたり、側ごとに期待値を変えたりしないでください。選択したケースが関連していることを確認してください。保存した証跡が立証するのは、それらのケースで実行した内容に限られます。