forge: verify path_claim_check DEFAULT_REPO wrong-tree refactor is behavior-preserving
This commit is contained in:
forge committed
1 parent
3552295428
commit
ec5579c68d
2 files changed
+314
No files matched your search
@@ -0,0 +1,103 @@
|
||||
# PATH CLAIM CHECK DRY REFACTOR VERIFICATION
|
||||
|
||||
Tool: `tools/path_claim_check.py` (forge lane: Refactor -- wrong-tree DEFAULT_REPO)
|
||||
Date: 2026-10-22
|
||||
Original: `git show HEAD~1:tools/path_claim_check.py` (commit 38bb774, the pre-refactor parent the refactor descends from)
|
||||
Refactored: working tree (`tools/path_claim_check.py`)
|
||||
|
||||
## The smell
|
||||
|
||||
`DEFAULT_REPO` was a host-literal constant:
|
||||
|
||||
```python
|
||||
DEFAULT_REPO = "/root/troupe-standup"
|
||||
```
|
||||
|
||||
The tool's own USAGE documents that paths are "resolved against --repo, not against
|
||||
the caller's cwd" -- but the DEFAULT violated that contract. A bare invocation from
|
||||
any other checkout, clone, or host graded `/root/troupe-standup` from here -- the
|
||||
wrong tree. `tool_map.py` calls this the "wrong-tree defect" at length: a tool that
|
||||
grades the tree it lives in, not the tree it names.
|
||||
|
||||
## The refactor
|
||||
|
||||
One line on the working tree, uncommitted at HEAD:
|
||||
|
||||
```python
|
||||
DEFAULT_REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
|
||||
```
|
||||
|
||||
`import os` was already present (line 123). The expression resolves to the parent of
|
||||
the `tools/` directory this file lives in -- i.e. the checkout root -- so a bare run
|
||||
grades the tree it is run out of. At `/root/troupe-standup` that still resolves to
|
||||
`/root/troupe-standup`, so the change is a **no-op in this checkout** and ONLY changes
|
||||
behavior in a clone / copy: exactly the point.
|
||||
|
||||
## Equivalence argument
|
||||
|
||||
- A bare run (`--repo` unspecified) is the ONLY path affected by the change.
|
||||
`DEFAULT_REPO` feeds only `argparse`'s `--repo default=`; every real work path
|
||||
(`Store`, `scan`, `resolve_baseline`, `load_baseline`) reads `a.repo`, which is
|
||||
`--repo` when given or `DEFAULT_REPO` when not.
|
||||
- With an explicit `--repo` the refactor is provably inert: it never touches
|
||||
`scan_text`, `scan`, `report`, `resolve_baseline`, or the selftest cells. The diff
|
||||
is one `str` literal -> one `__file__`-based `str`; no control-flow, no matcher,
|
||||
no fixture, no stat.
|
||||
- The portable expression `os.path.dirname(os.path.dirname(os.path.abspath(__file__)))`
|
||||
for `tools/path_claim_check.py` resolves to `os.path.dirname(".../tools/path_claim_check.py")`
|
||||
-> `".../tools"` -> `".../"` = the repo root, identical to the hardcoded literal when
|
||||
the checkout lives at `/root/troupe-standup`.
|
||||
|
||||
## Evidence (measured)
|
||||
|
||||
`wizard-work/forge/verify_path_claim_dry_refactor.py` materializes the original from
|
||||
`git show HEAD~1:tools/path_claim_check.py` (the pre-refactor commit the refactor
|
||||
descends from; HEAD~1 == the working-tree baseline here) and runs the refactored
|
||||
(working tree) end-to-end, comparing the bytes they emit:
|
||||
|
||||
```
|
||||
[ok ] selftest: original 27/27 rc 0
|
||||
[ok ] selftest: refactored 27/27 rc 0
|
||||
[ok ] selftest: identical stdout (byte-for-byte)
|
||||
[ok ] live scan: original ran rc 0
|
||||
[ok ] live scan: refactored ran rc 0
|
||||
[ok ] live scan: identical findings (paths + verdicts)
|
||||
[ok ] live scan: identical stats
|
||||
[ok ] live scan: non-vacuous (paths found > 0)
|
||||
[ok ] refactored DEFAULT_REPO is portable (__file__-based)
|
||||
[ok ] original DEFAULT_REPO is the host literal
|
||||
[ok ] portable DEFAULT_REPO resolves to /root/troupe-standup
|
||||
|
||||
verify: 11 checks, 11 passed, 0 failed
|
||||
```
|
||||
|
||||
- **[1-3] SELFTEST PARITY.** Both original and refactored pass 27/27 with
|
||||
byte-identical stdout (the 27 cells exercise `scan_text` incl. the fenced exclusion,
|
||||
the DOCREL second-base rule, the CLI contract on a fixture repo, the default-ledger
|
||||
pin, and the closed ledger-class set).
|
||||
- **[4] LIVE SCAN FINDINGS PARITY.** Running both versions with `--repo` over the
|
||||
repo's real `.md` corpus produces identical `paths` arrays (same paths, same
|
||||
verdicts).
|
||||
- **[5] LIVE SCAN STATS PARITY.** The `stats` dict is identical between original and
|
||||
refactored.
|
||||
- **[7] NON-VACUITY.** The census is non-empty -- real MISSING/EXISTS/DOCREL/EXTERNAL
|
||||
findings exist, so the equivalence comparison is meaningful, not a pair of empty
|
||||
results.
|
||||
- **[6] CODE-LEVEL PORTABILITY.** The refactored source carries the `__file__`-based
|
||||
expression on code lines and carries no host literal; the original carries only the
|
||||
host literal. The expression resolves to `/root/troupe-standup` in this checkout.
|
||||
|
||||
## Verdict
|
||||
|
||||
PASS -- the `DEFAULT_REPO` wrong-tree refactor is behavior-preserving: identical
|
||||
27/27 self-test contract, byte-identical selftest stdout, identical live-census
|
||||
findings and stats, with the portable expression resolving to the same root in this
|
||||
checkout. The refactor only changes behavior in a clone/copy -- which is the defect
|
||||
it exists to fix, and which the code-level check pins.
|
||||
|
||||
## CHECK (rerun the verifier)
|
||||
|
||||
```
|
||||
python3 /root/troupe-standup/wizard-work/forge/verify_path_claim_dry_refactor.py
|
||||
```
|
||||
exits 0 on full pass, 1 otherwise.
|
||||
@@ -0,0 +1,211 @@
|
||||
#!/usr/bin/env python3
|
||||
"""verify_path_claim_dry_refactor.py
|
||||
|
||||
Equivalence proof for the behavior-preserving refactor in
|
||||
tools/path_claim_check.py (forge lane: Refactor).
|
||||
|
||||
THE SMELL
|
||||
DEFAULT_REPO was a host-literal constant:
|
||||
DEFAULT_REPO = "/root/troupe-standup"
|
||||
The tool's own USAGE documents that paths are "resolved against --repo, not
|
||||
against the caller's cwd" -- but the DEFAULT violated that contract. A bare
|
||||
invocation from any other checkout, clone, or host graded /root/troupe-standup
|
||||
from here, i.e. the wrong tree. tool_map.py calls this the "wrong-tree defect".
|
||||
|
||||
THE REFACTOR (one line on the working tree, uncommitted at HEAD):
|
||||
DEFAULT_REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
|
||||
`import os` was already present. The expression resolves to the parent of the
|
||||
tools/ directory this file lives in -- i.e. the checkout root -- so a bare run
|
||||
grades the tree it is run out of. At /root/troupe-standup that still resolves to
|
||||
/root/troupe-standup, so the change is a no-op in THIS checkout and ONLY changes
|
||||
behavior in a clone / copy: exactly the point.
|
||||
|
||||
WHAT THIS VERIFIER PROVES
|
||||
The refactor is behavior-preserving: identical census, identical stats,
|
||||
identical selftest contract, on the same repo with an explicit --repo.
|
||||
|
||||
LEGS
|
||||
[1] selftest: original (git HEAD~1) passes 27/27, rc 0
|
||||
[2] selftest: refactored (working tree) passes 27/27, rc 0
|
||||
[3] selftest: stdout is byte-identical between original and refactored
|
||||
[4] live scan --json: findings (paths + verdicts) are identical
|
||||
[5] live scan --json: stats are identical
|
||||
[6] code-level: refactored DEFAULT_REPO is portable (__file__-based);
|
||||
original DEFAULT_REPO is the host literal
|
||||
[7] non-vacuity: the live census is non-empty (stats carry real findings)
|
||||
|
||||
Exit 0 iff all checks pass, else 1.
|
||||
"""
|
||||
import json
|
||||
import os
|
||||
import shutil
|
||||
import subprocess
|
||||
import sys
|
||||
import tempfile
|
||||
|
||||
REPO = "/root/troupe-standup"
|
||||
TOOL = "tools/path_claim_check.py"
|
||||
ORIG_SPEC = f"HEAD~1:{TOOL}"
|
||||
PORTABLE_EXPR = "os.path.dirname(os.path.dirname(os.path.abspath(__file__)))"
|
||||
HARD_CODED = '"/root/troupe-standup"'
|
||||
ORIG_SELFTTEST_SUMMARY = "selftest: 27 cells, 27 passed, 0 failed"
|
||||
REF_SELFTTEST_SUMMARY = "selftest: 27 cells, 27 passed, 0 failed"
|
||||
|
||||
|
||||
class Verdict(Exception):
|
||||
pass
|
||||
|
||||
|
||||
def materialize_original():
|
||||
"""Write the PRE-refactor module (git HEAD~1) under its real name in a
|
||||
temp dir; return (dir, path). HEAD~1 is the commit the refactor descends
|
||||
from: before the refactor lands it is the current HEAD's parent, and after
|
||||
the refactor is committed it remains the refactor's parent -- so this reads
|
||||
the genuine original both ways, the same guarantee the citation_resolve
|
||||
verifier relies on."""
|
||||
out = tempfile.NamedTemporaryFile(suffix=".py", delete=False, mode="wb")
|
||||
try:
|
||||
subprocess.run(["git", "-C", REPO, "show", ORIG_SPEC],
|
||||
check=True, stdout=out, timeout=30)
|
||||
except subprocess.CalledProcessError as exc:
|
||||
raise Verdict("could not read %s: %s" % (ORIG_SPEC, exc))
|
||||
finally:
|
||||
out.close()
|
||||
return os.path.dirname(out.name), out.name
|
||||
|
||||
|
||||
def run(path, args, cwd=REPO, timeout=180):
|
||||
proc = subprocess.run([sys.executable, path, *args],
|
||||
capture_output=True, text=True, cwd=cwd, timeout=timeout)
|
||||
return proc.returncode, proc.stdout, proc.stderr
|
||||
|
||||
|
||||
def run_json(path, out_path, repo=REPO, only="missing", timeout=180):
|
||||
"""Run path_claim_check.py --repo <repo> --json <out_path> --only <only>;
|
||||
return rc, stdout, stderr. The JSON is written to out_path."""
|
||||
proc = subprocess.run([sys.executable, path, "--repo", repo,
|
||||
"--only", only, "--json", out_path],
|
||||
capture_output=True, text=True, cwd=REPO, timeout=timeout)
|
||||
return proc.returncode, proc.stdout, proc.stderr
|
||||
|
||||
|
||||
def code_lines(text):
|
||||
"""Lines that are actual code (the smell lives in code, not prose).
|
||||
Matches the naive comment/docstring strip the other forge verifiers use so
|
||||
the metric is comparable: a line whose first non-space char is '#' or a
|
||||
triple-quote doc-opening is skipped. path_claim mentions the old shape only
|
||||
in a comment, so it is stripped or the count would read 1 instead of 0."""
|
||||
out = []
|
||||
for ln in text.splitlines():
|
||||
s = ln.lstrip()
|
||||
if s.startswith("#") or s.startswith('"""'):
|
||||
continue
|
||||
out.append(ln)
|
||||
return "\n".join(out)
|
||||
|
||||
|
||||
def main():
|
||||
cells, failed = [], 0
|
||||
|
||||
def check(label, ok, detail=""):
|
||||
cells.append((label, ok))
|
||||
nonlocal failed
|
||||
if not ok:
|
||||
failed += 1
|
||||
print(" [%s] %s%s"
|
||||
% ("ok " if ok else "FAIL", label,
|
||||
(f" [{detail}]" if detail and not ok else "")))
|
||||
|
||||
orig_dir, orig_path = materialize_original()
|
||||
ref_path = os.path.join(REPO, TOOL)
|
||||
tmpdir = tempfile.mkdtemp(prefix="pc_verify_", dir=os.environ.get("TMPDIR", "/tmp"))
|
||||
|
||||
try:
|
||||
# ---- [1-3] selftest parity -----------------------------------------
|
||||
rc_o, out_o, err_o = run(orig_path, ["--selftest"])
|
||||
rc_r, out_r, err_r = run(ref_path, ["--selftest"])
|
||||
check("selftest: original 27/27 rc 0",
|
||||
rc_o == 0 and ORIG_SELFTTEST_SUMMARY in out_o, f"rc={rc_o}")
|
||||
check("selftest: refactored 27/27 rc 0",
|
||||
rc_r == 0 and REF_SELFTTEST_SUMMARY in out_r, f"rc={rc_r}")
|
||||
check("selftest: identical stdout (byte-for-byte)",
|
||||
out_o == out_r,
|
||||
f"len_o={len(out_o)} len_r={len(out_r)}")
|
||||
|
||||
# ---- [4-5] live scan equivalence -------------------------------------
|
||||
oj_path = os.path.join(tmpdir, "orig.json")
|
||||
rj_path = os.path.join(tmpdir, "ref.json")
|
||||
rc_o, _, _ = run_json(orig_path, oj_path)
|
||||
rc_r, _, _ = run_json(ref_path, rj_path)
|
||||
check("live scan: original ran rc 0", rc_o == 0, f"rc={rc_o}")
|
||||
check("live scan: refactored ran rc 0", rc_r == 0, f"rc={rc_r}")
|
||||
|
||||
if os.path.exists(oj_path) and os.path.exists(rj_path):
|
||||
oj = json.load(open(oj_path))
|
||||
rj = json.load(open(rj_path))
|
||||
|
||||
# [4] findings: paths + verdicts identical
|
||||
paths_o = sorted(r["path"] for r in oj["paths"])
|
||||
paths_r = sorted(r["path"] for r in rj["paths"])
|
||||
verdicts_o = {r["path"]: r["verdict"] for r in oj["paths"]}
|
||||
verdicts_r = {r["path"]: r["verdict"] for r in rj["paths"]}
|
||||
findings_ok = paths_o == paths_r and verdicts_o == verdicts_r
|
||||
check("live scan: identical findings (paths + verdicts)",
|
||||
findings_ok,
|
||||
f"orig={len(paths_o)} ref={len(paths_r)}")
|
||||
|
||||
# [5] stats identical
|
||||
stats_ok = oj["stats"] == rj["stats"]
|
||||
check("live scan: identical stats",
|
||||
stats_ok,
|
||||
f"orig={dict(oj['stats'])} ref={dict(rj['stats'])}")
|
||||
|
||||
# [7] non-vacuity: the census actually found something
|
||||
nonvac = (len(oj["paths"]) > 0 and len(rj["paths"]) > 0
|
||||
and sum(oj["stats"].values()) > 0)
|
||||
check("live scan: non-vacuous (paths found > 0)",
|
||||
nonvac)
|
||||
else:
|
||||
check("live scan: JSON files produced by both", False)
|
||||
|
||||
# ---- [6] code-level: DEFAULT_REPO portability ----------------------
|
||||
ref_text = open(ref_path, encoding="utf-8").read()
|
||||
orig_text = open(orig_path, encoding="utf-8").read()
|
||||
ref_code = code_lines(ref_text)
|
||||
orig_code = code_lines(orig_text)
|
||||
|
||||
ref_has_portable = PORTABLE_EXPR in ref_code
|
||||
ref_has_hardcoded = HARD_CODED in ref_code
|
||||
orig_has_portable = PORTABLE_EXPR in orig_code
|
||||
orig_has_hardcoded = HARD_CODED in orig_code
|
||||
|
||||
check("refactored DEFAULT_REPO is portable (__file__-based)",
|
||||
ref_has_portable and not ref_has_hardcoded,
|
||||
f"portable={ref_has_portable} hardcoded={ref_has_hardcoded}")
|
||||
check("original DEFAULT_REPO is the host literal",
|
||||
orig_has_hardcoded and not orig_has_portable,
|
||||
f"hardcoded={orig_has_hardcoded} portable={orig_has_portable}")
|
||||
|
||||
# the portable expression resolves to /root/troupe-standup here
|
||||
resolved = subprocess.run(
|
||||
[sys.executable, "-c",
|
||||
f"import os; print(os.path.dirname(os.path.dirname(os.path.abspath('{ref_path}'))))"],
|
||||
capture_output=True, text=True).stdout.strip()
|
||||
check("portable DEFAULT_REPO resolves to /root/troupe-standup",
|
||||
resolved == REPO, f"got={resolved}")
|
||||
finally:
|
||||
shutil.rmtree(orig_dir, ignore_errors=True)
|
||||
shutil.rmtree(tmpdir, ignore_errors=True)
|
||||
|
||||
total = len(cells)
|
||||
passed = total - failed
|
||||
print(f"\nverify: {total} checks, {passed} passed, {failed} failed")
|
||||
return 1 if failed else 0
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
try:
|
||||
sys.exit(main())
|
||||
except Verdict as e:
|
||||
print(f"\nVERDICT: MISMATCH -- {e}")
|
||||
sys.exit(1)
|
||||
Reference in new issue
Block a user