prove-patch

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Prove Patch

证明补丁

Use the original baseline, final patch commit, declared

repair_scope

, and unchanged reproduction package. Read the record contract. Do not edit the patch or validate an uncommitted tree. Return failures for a new attempt. Before target commands, follow its project guidance.

Review the scoped cases and the patch without the patcher's conclusion. Execute each planned input on clean baseline and patched trees with the same retained harness source and command. The harness must print exactly one
```
PATCH_CASE {"input": ..., "actual": ...}
```
from the exercised input and observed result, then print
```
PATCH_REACHED
```
as its final stdout line immediately before the assertion. Representatives must fail on the baseline and pass on the patch. Valid controls must pass on both. Keep the baseline and patched stdout, stderr, exit status, elapsed time, command, and harness source under
```
receipts/
```
. A timeout, setup failure, missing marker, mismatched input, or ambiguous observation is an evidence gap. A trustworthy patched failure is a finding. Never relabel a gap as a pass.
Run relevant project checks on the patch and retain the same raw receipts. Use baseline comparison for behavior checks and to attribute failed project checks; a passing patched suite may omit a baseline run. Include focused tests, regression and security checks where relevant. Record specific unproven limits; an empty list leaves the result inconclusive.
Run the three-arm helper with the proof-type recipe in the record contract,
```
reproduce.baseline_commit
```
, and final
```
patch_commit
```
. Require the baseline to fail, patch to pass, and complete baseline revert to fail again. Require
```
receipts/source.json
```
to identify the pinned commits and the reverted tree to equal the original baseline tree. Require the type's build identity result. Retain all source-tree, build, and execution receipts.
Write
```
prove.json
```
and a final manifest covering it and every receipt. Run
```
uv run --no-project <script> manifest <prove-attempt-dir>
```
and then
```
uv run --no-project <script> check <run-dir>
```
with the validator. Independently inspect the native proof assessment and raw receipts before reporting a result. A complete proof has no findings or gaps. Return exact failures and receipt paths to the orchestrator.

Prove record schema:

json

{
  "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"
}

For a bounded class, include at least two distinct failing representatives and a valid control. The record must cover every planned case by unique

check_id

. Use the same harness and command on both commits; do not reveal the side to the harness or change expectations by side. Review the selected cases for relevance; retained receipts establish only what those cases exercised.

使用原始基线、最终补丁提交、声明的

repair_scope

和未经修改的复现包。阅读记录契约。不要编辑补丁，也不要验证未提交的代码树。新尝试应返回失败项。在执行目标命令前，遵循其项目指导。

审查限定范围内的各个用例和补丁时，不要参考 patcher 的结论。使用相同的留存 harness 源码和命令，在干净的基线代码树和已修补代码树上执行每个计划输入。harness 必须根据所执行的输入和观察到的结果恰好打印一条
```
PATCH_CASE {"input": ..., "actual": ...}
```
，然后在断言前将
```
PATCH_REACHED
```
作为最后一条 stdout 行打印出来。代表性用例必须在基线上失败、在补丁上通过。有效对照用例必须在两者上均通过。将基线和补丁版本的 stdout、stderr、退出状态、耗时、命令及 harness 源码保存在
```
receipts/
```
下。超时、设置失败、标记缺失、输入不匹配或观察结果含糊，均属于证据缺口。可信的补丁版本失败是一项发现。绝不能将缺口重新标记为通过。
在补丁上运行相关项目检查，并保留原始回执。行为检查应使用基线对比，并用于归因失败的项目检查；如果补丁版本的测试套件通过，可以省略基线运行。根据相关性纳入聚焦测试、回归检查和安全检查。记录具体尚未证明的边界；空列表意味着结果不确定。
使用记录契约中的证明类型配方、
```
reproduce.baseline_commit
```
和最终
```
patch_commit
```
运行三臂辅助工具。要求基线失败、补丁通过，并且在完整回退到基线后再次失败。要求
```
receipts/source.json
```
标识固定的提交，且回退后的代码树与原始基线代码树相同。要求取得该类型的构建标识结果。保留所有源代码树、构建和执行回执。
编写
```
prove.json
```
以及一份涵盖它和每份回执的最终 manifest。运行
```
uv run --no-project <script> manifest <prove-attempt-dir>
```
，然后使用验证器运行
```
uv run --no-project <script> check <run-dir>
```
。在报告结果前，独立检查原生证明评估和原始回执。完整的证明不得存在发现或缺口。将精确的失败项和回执路径返回给 orchestrator。

证明记录结构：

json

{
  "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"
}

对于有界类别，至少包含两个不同的失败代表性用例和一个有效对照用例。记录必须通过唯一的

check_id

覆盖每个计划用例。在两个提交上使用相同的 harness 和命令；不要向 harness 透露执行的是哪一侧，也不要根据执行侧改变预期。审查所选用例的相关性；留存回执只能证明这些用例实际覆盖的范围。