From ec5579c68d9932402668657ca3ff62d576bd2392 Mon Sep 17 00:00:00 2001 From: forge Date: Thu, 22 Oct 2026 19:35:23 +0000 Subject: [PATCH] forge: verify path_claim_check DEFAULT_REPO wrong-tree refactor is behavior-preserving --- .../PATH_CLAIM_DRY_REFACTOR_VERIFICATION.md | 103 +++++++++ .../forge/verify_path_claim_dry_refactor.py | 211 ++++++++++++++++++ 2 files changed, 314 insertions(+) create mode 100644 wizard-work/forge/PATH_CLAIM_DRY_REFACTOR_VERIFICATION.md create mode 100644 wizard-work/forge/verify_path_claim_dry_refactor.py diff --git a/wizard-work/forge/PATH_CLAIM_DRY_REFACTOR_VERIFICATION.md b/wizard-work/forge/PATH_CLAIM_DRY_REFACTOR_VERIFICATION.md new file mode 100644 index 0000000..c8a96bb --- /dev/null +++ b/wizard-work/forge/PATH_CLAIM_DRY_REFACTOR_VERIFICATION.md @@ -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. diff --git a/wizard-work/forge/verify_path_claim_dry_refactor.py b/wizard-work/forge/verify_path_claim_dry_refactor.py new file mode 100644 index 0000000..62aeba9 --- /dev/null +++ b/wizard-work/forge/verify_path_claim_dry_refactor.py @@ -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 --json --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)