forge: verify write_probe two-scan -> Counter DRY collapse (behavior-preserving)
This commit is contained in:
forge committed
1 parent
ff904ea56c
commit
8b23b7a913
3 files changed
+324
No files matched your search
@@ -0,0 +1,105 @@
|
||||
# WRITE_PROBE_DRY_REFACTOR_VERIFICATION
|
||||
|
||||
Tool: `tools/write_probe.py` (forge lane: Refactor)
|
||||
Original: `git show HEAD:tools/write_probe.py` (byte-identical at HEAD; the refactor is
|
||||
unstaged in the working tree)
|
||||
Refactored: working tree (`tools/write_probe.py`)
|
||||
|
||||
## The smell
|
||||
|
||||
`write_probe.py`'s write-axis summary counted its own rows with two list-comprehension
|
||||
scans that differ ONLY by the axis string constant:
|
||||
|
||||
```python
|
||||
n_json = len([r for r in rows if r.get("axis") == "json"])
|
||||
n_flag = len([r for r in rows if r.get("axis") == "flag"])
|
||||
```
|
||||
|
||||
Twelve tokens of structure spelled twice, differing in a single string literal. The
|
||||
stdlib already owns the shape: a single `Counter` pass over `r.get("axis")` buckets every
|
||||
row once, and `["json"]/["flag"]` read out exactly the two counts needed.
|
||||
|
||||
## The refactor
|
||||
|
||||
One hunk (`from collections import Counter`) and one hunk in `main()`:
|
||||
|
||||
```python
|
||||
axis_counts = Counter(r.get("axis") for r in rows)
|
||||
n_json = axis_counts["json"]
|
||||
n_flag = axis_counts["flag"]
|
||||
```
|
||||
|
||||
The only consumer of `n_json`/`n_flag` is the single `print("write axis: ... (json %d,
|
||||
flag %d)")` line and the `--json` payload's `axes` object -- both derived purely from the
|
||||
row list. No verdict, no probe, no row content is touched.
|
||||
|
||||
### Equivalence argument
|
||||
|
||||
For any row `r`:
|
||||
|
||||
- `axis == "json"` -> counted by scan 1, lands in `Counter`'s `"json"` bucket. Same.
|
||||
- `axis == "flag"` -> counted by scan 2, lands in `Counter`'s `"flag"` bucket. Same.
|
||||
- `axis` absent (or any other value) -> `r.get("axis")` is `None` -> NOT equal to `"json"`
|
||||
or `"flag"`, so it is in neither scan count; and `None` is not `"json"`/`"flag"`, so
|
||||
`axis_counts["json"]` / `axis_counts["flag"]` read `0` for it. Same.
|
||||
|
||||
The two forms are arithmetically identical for every input, so `axes` and the printed
|
||||
write-axis line are unchanged.
|
||||
|
||||
## Evidence (measured)
|
||||
|
||||
Proof in `wizard-work/forge/verify_write_probe_dry_refactor.py`. It materializes the
|
||||
`HEAD` blob as `write_probe.py` in a temp dir and runs the ORIGINAL and the REFACTORED
|
||||
module as subprocesses over the SAME repo (`/root/troupe-standup`) with a writable `--json`
|
||||
target, then compares the three legs:
|
||||
|
||||
```
|
||||
[1] end-to-end axes+sig drift rc_orig=0 rc_ref=0 axes_orig={'flag': 3, 'json': 21} axes_ref={'flag': 3, 'json': 21} rows=24 PASS
|
||||
[2] --selftest drift guard rc=0 PASS
|
||||
selftest: 15 cells, 15 passed, 0 failed
|
||||
[3] redundancy (code lines) two-scan: orig=2 ref=0 counter-use: orig=0 ref=1 PASS
|
||||
|
||||
VERDICT: ALL GREEN -- write_probe axes+row-signature byte-identical to original, --selftest 15/15, 2 two-scan scans -> 1 Counter pass
|
||||
EXIT=0
|
||||
```
|
||||
|
||||
(Full captured log: `write_probe_dry_refactor_run.log`.)
|
||||
|
||||
### Verdict breakdown
|
||||
|
||||
- **[1] END-TO-END axes+signature drift.** The original (`HEAD`) and refactored (working
|
||||
tree) `write_probe.py` both run over `/root/troupe-standup --json <writable> --timeout 60`.
|
||||
The refactor's only output is the `axes` object, and `axes_orig == axes_ref`
|
||||
(`{'json': 21, 'flag': 3}` on both); the non-detail row signature is identical
|
||||
(24 rows, rc 0 both). Per-row `detail`/`probe` are excluded from the signature because
|
||||
they embed each run's own throwaway temp-dir path (e.g.
|
||||
`.../write-probe-XXXX/no-such-dir/out.json`) -- a diff they would produce regardless of
|
||||
the refactor. Non-vacuous: axes.json==21, axes.flag==3, 24 rows, rc 0 on both; the
|
||||
fixture grades real probes (21 json-axis tools + 3 caller-path write flags), and the
|
||||
counter change is isolated to axes computation.
|
||||
- **[2] SELFTEST drift guard.** `python3 tools/write_probe.py --selftest` exits 0 on the
|
||||
refactored worktree -- the tool's own 15-cell contract (judge ordering, fault-block
|
||||
position, table coverage, fixture shape, both axes, the bare/guarded `--write` twins)
|
||||
holds 15/15.
|
||||
- **[3] REDUNDANCY collapsed.** Measured on code lines (comment/docstring lines stripped,
|
||||
matching the convention the other forge verifiers use -- the only residual two-scan
|
||||
reference in the worktree is inside a `#` comment):
|
||||
|
||||
| pattern (code lines) | original (HEAD) | refactored (tree) |
|
||||
|---------------------------------|-----------------|-------------------|
|
||||
| `len([r for r in rows ...` scan | 2 | 0 |
|
||||
| `Counter(r.get("axis") ...` use | 0 | 1 |
|
||||
|
||||
The smell removed from the worktree is still present in the original baseline (2 two-scan
|
||||
lines, 0 Counter), confirming the diff is non-trivial and the assertions are non-vacuous.
|
||||
|
||||
## Verdict
|
||||
|
||||
Behavior-preserving DRY collapse: the two axis-count scans in `write_probe.py` collapsed
|
||||
into a single `Counter` pass. `axes` (`json=21, flag=3`) and the row signature are
|
||||
identical between original (`HEAD`) and refactored on the full repo probe, the tool's own
|
||||
15-cell `--selftest` stays green, and the smell is gone from code lines while still present
|
||||
in the original.
|
||||
|
||||
VERDICT: PASS -- `write_probe.py` refactor is behavior-preserving; axes + row signature
|
||||
identical to original, --selftest 15/15, 2 two-scan scans -> 1 Counter pass.
|
||||
@@ -0,0 +1,212 @@
|
||||
#!/usr/bin/env python3
|
||||
"""verify_write_probe_dry_refactor.py
|
||||
|
||||
Equivalence proof for the behavior-preserving refactor in
|
||||
tools/write_probe.py (forge lane: Refactor).
|
||||
|
||||
A single DRY collapse was applied to the working tree: the two near-identical
|
||||
list-comprehension scans in main()'s write-axis summary,
|
||||
|
||||
n_json = len([r for r in rows if r.get("axis") == "json"])
|
||||
n_flag = len([r for r in rows if r.get("axis") == "flag"])
|
||||
|
||||
which differ ONLY by the axis string constant, were collapsed into one pass:
|
||||
|
||||
axis_counts = Counter(r.get("axis") for r in rows)
|
||||
n_json = axis_counts["json"]
|
||||
n_flag = axis_counts["flag"]
|
||||
|
||||
A row whose "axis" key is absent (or any other value) yields None under
|
||||
``.get("axis")``, which is neither "json" nor "flag" -- so it is absent from
|
||||
both counts in the two-scan form, and lands in the ``None`` bucket of the
|
||||
Counter, which ``["json"]/["flag"]`` never read. The two forms are therefore
|
||||
arithmetically identical for every input, which is exactly the three legs below
|
||||
prove.
|
||||
|
||||
Exit code is the verdict: 0 = all green, 1 = any mismatch.
|
||||
|
||||
LEGS
|
||||
[1] END-TO-END counter equivalence. The ORIGINAL (git HEAD) and the REFACTORED
|
||||
(working tree) write_probe.py are both run, as subprocesses, over the SAME
|
||||
repo (/root/troupe-standup) with a writable --json target. The payload's
|
||||
"axes" object -- {json, flag} -- is the refactor's ONLY output, so it must
|
||||
match. The per-row "detail"/"probe" fields are EXCLUDED from the row
|
||||
signature: they embed each run's own throwaway temp dir path (unrelated to
|
||||
the refactor) and would otherwise guarantee a diff. Every other row field is
|
||||
compared, order preserved. Non-vacuous: axes.json==21, axes.flag==3, 24 rows.
|
||||
|
||||
[2] SELFTEST drift guard. `write_probe.py --selftest` exits 0 on the
|
||||
refactored worktree (the tool's own 15-cell contract).
|
||||
|
||||
[3] REDUNDANCY collapsed. The original (git HEAD) carries BOTH two-scan lines
|
||||
on code lines (0 Counter usages); the refactored worktree carries ONE
|
||||
Counter usage and ZERO two-scan lines. Counted on code lines only.
|
||||
"""
|
||||
import hashlib
|
||||
import json
|
||||
import os
|
||||
import shutil
|
||||
import subprocess
|
||||
import sys
|
||||
import tempfile
|
||||
|
||||
REPO = "/root/troupe-standup"
|
||||
DCC = os.path.join(REPO, "tools", "write_probe.py")
|
||||
REAL_REPO = os.path.join(REPO, ".")
|
||||
TWO_SCAN = 'len([r for r in rows if r.get("axis")' # the collapsed scan-shape
|
||||
COUNTER_USE = 'Counter(r.get("axis")' # the single-pass replacement
|
||||
|
||||
|
||||
class Verdict(Exception):
|
||||
pass
|
||||
|
||||
|
||||
def sha(text):
|
||||
return hashlib.sha256(text.encode()).hexdigest()
|
||||
|
||||
|
||||
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 '\"\"\"'
|
||||
is skipped. The refactored write_probe mentions the old shape ONLY in a '#'
|
||||
comment, so it must be 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 materialize_original():
|
||||
"""Write git HEAD:tools/write_probe.py under its real name in a temp dir;
|
||||
return (dir, path). HEAD is the clean original: the two-scan smell is
|
||||
present, the Counter is absent, and write_probe.py is byte-identical at the
|
||||
tip of the commit lineage (the Counter change is unstaged in the worktree).
|
||||
So HEAD reads a genuine original both before the refactor lands and after it
|
||||
is committed -- the same guarantee the other forge verifiers rely on.
|
||||
"""
|
||||
res = subprocess.run(["git", "-C", REPO, "show", "HEAD:tools/write_probe.py"],
|
||||
capture_output=True, text=True)
|
||||
if not res.stdout:
|
||||
raise Verdict("could not read HEAD:tools/write_probe.py: " + res.stderr.strip())
|
||||
d = tempfile.mkdtemp(prefix="wp_orig_")
|
||||
p = os.path.join(d, "write_probe.py")
|
||||
with open(p, "w", encoding="utf-8") as fh:
|
||||
fh.write(res.stdout)
|
||||
return d, p
|
||||
|
||||
|
||||
def row_sig(rows):
|
||||
"""(tool, axis, verdict, rc, flag) per row, order preserved.
|
||||
|
||||
detail and probe are dropped: detail embeds the run's throwaway temp dir
|
||||
(e.g. ".../write-probe-XXXX/no-such-dir/out.json") and the flag axis's probe
|
||||
embeds the expanded --write target path -- both differ per run regardless of
|
||||
the refactor. Everything that survives is identical between original and
|
||||
refactored because they probe the same repo with the same judge.
|
||||
"""
|
||||
sig = []
|
||||
for r in rows:
|
||||
sig.append((r.get("tool"), r.get("axis"), r.get("verdict"),
|
||||
r.get("rc"), r.get("flag")))
|
||||
return sig
|
||||
|
||||
|
||||
def run_probe_json(path, repo, timeout=180):
|
||||
"""Run a write_probe.py with --json to a writable temp file; return the
|
||||
parsed payload (and rc)."""
|
||||
out_json = os.path.join(tempfile.mkdtemp(prefix="wp_out_"), "payload.json")
|
||||
p = subprocess.run([sys.executable, path, "--repo", repo,
|
||||
"--json", out_json, "--timeout", "60"],
|
||||
capture_output=True, text=True, timeout=timeout)
|
||||
if p.returncode not in (0, 1):
|
||||
raise Verdict("run %s failed rc=%d: %s"
|
||||
% (path, p.returncode, (p.stderr or p.stdout)[:300]))
|
||||
with open(out_json, encoding="utf-8") as fh:
|
||||
payload = json.load(fh)
|
||||
shutil.rmtree(os.path.dirname(out_json), ignore_errors=True)
|
||||
return payload, p.returncode
|
||||
|
||||
|
||||
def main():
|
||||
ok = True
|
||||
|
||||
orig_dir, orig_path = materialize_original()
|
||||
try:
|
||||
# ---- [1] END-TO-END counter equivalence ---------------------------
|
||||
payload_o, rc_o = run_probe_json(orig_path, REPO)
|
||||
payload_r, rc_r = run_probe_json(DCC, REPO)
|
||||
|
||||
axes_o = payload_o.get("axes")
|
||||
axes_r = payload_r.get("axes")
|
||||
sig_o = row_sig(payload_o.get("tools", []))
|
||||
sig_r = row_sig(payload_r.get("tools", []))
|
||||
|
||||
# Non-vacuity: the refactor's output is real and exercised.
|
||||
nonvac = (axes_r.get("json") == 21 and axes_r.get("flag") == 3
|
||||
and len(payload_r.get("tools", [])) == 24
|
||||
and len(payload_o.get("tools", [])) == 24)
|
||||
axes_ok = axes_o == axes_r
|
||||
sig_ok = sig_o == sig_r
|
||||
drift_ok = nonvac and axes_ok and sig_ok and rc_o == rc_r
|
||||
print("[1] end-to-end axes+sig drift rc_orig=%d rc_ref=%d "
|
||||
"axes_orig=%s axes_ref=%s rows=24 %s"
|
||||
% (rc_o, rc_r, axes_o, axes_r, "PASS" if drift_ok else "FAIL"))
|
||||
if not drift_ok:
|
||||
ok = False
|
||||
print(" non-vacuity (json==21, flag==3, rows==24): %s" % nonvac)
|
||||
print(" axes match (counter equivalence): %s" % axes_ok)
|
||||
print(" row signature match (detail/probe excluded): %s" % sig_ok)
|
||||
print(" rc match: %s (rc_o=%s rc_r=%s)" % (rc_o == rc_r, rc_o, rc_r))
|
||||
|
||||
# ---- [2] SELFTEST drift guard ------------------------------------
|
||||
rc = subprocess.run([sys.executable, DCC, "--selftest"],
|
||||
capture_output=True, text=True)
|
||||
guard_ok = rc.returncode == 0
|
||||
print("[2] --selftest drift guard rc=%d %s"
|
||||
% (rc.returncode, "PASS" if guard_ok else "FAIL"))
|
||||
if not guard_ok:
|
||||
ok = False
|
||||
print(" " + (rc.stdout + rc.stderr).strip()[:400].replace("\n", "\n "))
|
||||
else:
|
||||
last = [l for l in rc.stdout.splitlines() if l.strip()][-1]
|
||||
print(" " + last.strip())
|
||||
|
||||
# ---- [3] REDUNDANCY collapsed ------------------------------------
|
||||
text = open(DCC, encoding="utf-8").read()
|
||||
orig_text = open(orig_path, encoding="utf-8").read()
|
||||
code = code_lines(text)
|
||||
code_o = code_lines(orig_text)
|
||||
orig_scans = code_o.count(TWO_SCAN)
|
||||
ref_scans = code.count(TWO_SCAN)
|
||||
orig_counter = code_o.count(COUNTER_USE)
|
||||
ref_counter = code.count(COUNTER_USE)
|
||||
red_ok = (orig_scans == 2 and ref_scans == 0
|
||||
and orig_counter == 0 and ref_counter == 1)
|
||||
print("[3] redundancy (code lines) two-scan: orig=%d ref=%d "
|
||||
"counter-use: orig=%d ref=%d %s"
|
||||
% (orig_scans, ref_scans, orig_counter, ref_counter,
|
||||
"PASS" if red_ok else "FAIL"))
|
||||
if not red_ok:
|
||||
ok = False
|
||||
finally:
|
||||
shutil.rmtree(orig_dir, ignore_errors=True)
|
||||
|
||||
print("\nVERDICT:",
|
||||
"ALL GREEN -- write_probe axes+row-signature byte-identical to "
|
||||
"original, --selftest 15/15, 2 two-scan scans -> 1 Counter pass"
|
||||
if ok else "MISMATCH -- behavior NOT preserved")
|
||||
sys.exit(0 if ok else 1)
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
try:
|
||||
main()
|
||||
except Verdict as e:
|
||||
print("\nVERDICT: MISMATCH -- %s" % e)
|
||||
sys.exit(1)
|
||||
@@ -0,0 +1,7 @@
|
||||
[1] end-to-end axes+sig drift rc_orig=0 rc_ref=0 axes_orig={'flag': 3, 'json': 21} axes_ref={'flag': 3, 'json': 21} rows=24 PASS
|
||||
[2] --selftest drift guard rc=0 PASS
|
||||
selftest: 15 cells, 15 passed, 0 failed
|
||||
[3] redundancy (code lines) two-scan: orig=2 ref=0 counter-use: orig=0 ref=1 PASS
|
||||
|
||||
VERDICT: ALL GREEN -- write_probe axes+row-signature byte-identical to original, --selftest 15/15, 2 two-scan scans -> 1 Counter pass
|
||||
EXIT=0
|
||||
Reference in new issue
Block a user