diff --git a/tools/append_only_owners.py b/tools/append_only_owners.py index 0d5e52c..a6f90a1 100644 --- a/tools/append_only_owners.py +++ b/tools/append_only_owners.py @@ -152,10 +152,16 @@ def report(res, out=sys.stdout): r["shape"], r["break_text"][:60]), file=out) print(" total: %d" % len(others), file=out) print("\n-- per committed party (folded) --", file=out) + # One pass over losses indexed by (author, vs_prev); the three former + # `sum(1 for r in losses if r["author"] == k and r["vs_prev"] == X)` scans + # differed only by the constant X, so they collapse to a single Counter + # build and O(1) lookups that return 0 for an unseen (author, verdict) pair + # -- exactly the 0 the old sums returned for no matches. + party_vs = Counter((r["author"], r["vs_prev"]) for r in losses) for k, v in Counter(r["author"] for r in losses).most_common(): - same = sum(1 for r in losses if r["author"] == k and r["vs_prev"] == "SAME_PARTY") - oth = sum(1 for r in losses if r["author"] == k and r["vs_prev"] == "OTHER_PARTY") - first = sum(1 for r in losses if r["author"] == k and r["vs_prev"] == "FIRST_CHANGE_ON_PATH") + same = party_vs.get((k, "SAME_PARTY"), 0) + oth = party_vs.get((k, "OTHER_PARTY"), 0) + first = party_vs.get((k, "FIRST_CHANGE_ON_PATH"), 0) print(" %-18s %3d (own-file %d, other-file %d, first-change %d)" % (k, v, same, oth, first), file=out) diff --git a/wizard-work/forge/APPEND_ONLY_OWNERS_DRY_REFACTOR_VERIFICATION.md b/wizard-work/forge/APPEND_ONLY_OWNERS_DRY_REFACTOR_VERIFICATION.md new file mode 100644 index 0000000..9124079 --- /dev/null +++ b/wizard-work/forge/APPEND_ONLY_OWNERS_DRY_REFACTOR_VERIFICATION.md @@ -0,0 +1,100 @@ +# APPEND_ONLY_OWNERS_DRY_REFACTOR_VERIFICATION + +Tool: `tools/append_only_owners.py` (forge lane: DRY, behavior-preserving) +Date: 2026-10-20 +Original: `git show HEAD~1:tools/append_only_owners.py` (volt, last touched by 6ee8fce) +Refactored: working tree (`tools/append_only_owners.py`) + +## The smell + +`report()`'s per-party census tallied three verdict categories -- SAME_PARTY, +OTHER_PARTY, FIRST_CHANGE_ON_PATH -- with three full `sum(1 for r in losses if +r["author"] == k and r["vs_prev"] == X)` scans. They differed only by the +constant verdict X; everything else about the predicate was identical. + +```python +for k, v in Counter(r["author"] for r in losses).most_common(): + same = sum(1 for r in losses if r["author"] == k and r["vs_prev"] == "SAME_PARTY") + oth = sum(1 for r in losses if r["author"] == k and r["vs_prev"] == "OTHER_PARTY") + first = sum(1 for r in losses if r["author"] == k and r["vs_prev"] == "FIRST_CHANGE_ON_PATH") + print(" %-18s %3d (own-file %d, other-file %d, first-change %d)" + % (k, v, same, oth, first), file=out) +``` + +Three O(n) passes per party, over the same list, varying only the constant. + +## The refactor + +One `Counter((r["author"], r["vs_prev"]) for r in losses)` build, then O(1) +`.get((k, X), 0)` lookups. The outer `Counter(r["author"] for r in losses).most_common()` +ordering -- which drives print order -- is untouched. + +```python +party_vs = Counter((r["author"], r["vs_prev"]) for r in losses) +for k, v in Counter(r["author"] for r in losses).most_common(): + same = party_vs.get((k, "SAME_PARTY"), 0) + oth = party_vs.get((k, "OTHER_PARTY"), 0) + first = party_vs.get((k, "FIRST_CHANGE_ON_PATH"), 0) + print(" %-18s %3d (own-file %d, other-file %d, first-change %d)" + % (k, v, same, oth, first), file=out) +``` + +`git diff` for the change: four hunks collapsed to one, 9 insertions / 3 deletions. + +### Equivalence argument + +The three values `(same, oth, first)` are the sole behavioral inputs to that +print line. `Counter.get((k, X), 0)` returns 0 for an unseen (author, verdict) +pair -- exactly the 0 that `sum(1 for r in losses if ...)` returned over an +empty match set. The print format string is byte-identical. The outer loop +ordering is unchanged. Therefore `report()` renders byte-identical output on +every input the old and new code both accept. + +## Evidence (measured) + +The proof lives in `wizard-work/forge/verify_append_only_owners_dry_refactor.py`. +It materializes the `HEAD~1` blob as `append_only_owners.py` in a temp dir and +compares it against the working-tree refactored copy across five verdicts. +Run output: + +``` +[1] micro census: old_tally == new_tally PASS +[2] micro selftest-row tally agree (4 losses) PASS +[3] report() stdout original=4718f6d87ff2fe78f55d47ad24ba0b2729c6ca095c3c9427db83ad18ed64a8a5 refactored=4718f6d87ff2fe78f55d47ad24ba0b2729c6ca095c3c9427db83ad18ed64a8a5 PASS +[4] --selftest drift guard rc=0 PASS +[5] redundancy (code lines) party_vs builds=1 old-sum scans=0 PASS + +VERDICT: ALL GREEN -- per-party DRY collapse behavior preserved +``` + +### Verdict breakdown + +- **[1] MICRO EQUIVALENCE.** On a synthetic census covering every vs_prev class, + including parties for which a class is ABSENT (the 0-default path), the old + three-scan tally and the new single-pass tally agree. alice has 0 FIRST_CHANGE + (absent), bob has 0 SAME and 0 OTHER (absent), carol has 0 OTHER (absent), + dave has 0 SAME and 0 FIRST (absent) -- each exercised the 0-default branch. + +- **[2] MICRO SELFTEST-FIXTURE TALLY.** The same old-vs-new tally on the + module's own adjudicated selftest rows agrees (4 losses). + +- **[3] REPORT() STDOUT DRIFT.** End-to-end: the HEAD~1 original (old sum scans) + and the working-tree refactored copy both `report()` the same census to + StringIO; stdout is byte-identical (sha256 match). + +- **[4] SELFTEST DRIFT GUARD.** `python3 tools/append_only_owners.py --selftest` + exits 0 on the refactored worktree (the tool's own 15-cell contract). + +- **[5] REDUNDANCY COLLAPSED.** The worktree carries ONE `party_vs = Counter(...)` + build and ZERO of the old `sum(1 for r in losses if r["author"] == k` scan on + code lines (the explanatory comment is excluded by the comment-line filter). + +## Verdict + +Behavior-preserving DRY consolidation: three redundant per-party row-list scans +collapsed to one `Counter` pass plus O(1) lookups. Both consumers proven +byte-identical to the original across a synthetic census, the module's own +selftest fixtures, and the tool's 15-cell selftest battery. + +VERDICT: PASS -- per-party DRY collapse is behavior-preserving; sha256-identical +report() stdout, --selftest 15/15, old-sum scans 0 in code. diff --git a/wizard-work/forge/verify_append_only_owners_dry_refactor.py b/wizard-work/forge/verify_append_only_owners_dry_refactor.py new file mode 100644 index 0000000..0f65071 --- /dev/null +++ b/wizard-work/forge/verify_append_only_owners_dry_refactor.py @@ -0,0 +1,251 @@ +#!/usr/bin/env python3 +"""verify_append_only_owners_dry_refactor.py + +Equivalence proof for the DRY collapse in tools/append_only_owners.py's +report(): three `sum(1 for r in losses if r["author"] == k and r["vs_prev"] == X)` +scans -- identical except for the constant verdict X -- collapsed into ONE +`Counter((author, vs_prev) ...)` pass plus O(1) `.get((k, X), 0)` lookups. + +Behavior-preserving iff report() renders byte-identical output on every input +the old and new code both accept. The old `sum` returns 0 for no matches; the new +`Counter.get(..., 0)` returns 0 for an unseen (author, verdict) key -- same 0. +The outer ordering (`Counter(r["author"]...).most_common()`) is untouched, so the +emit order is unchanged. Five verdicts, all must be green. + + 1. MICRO census -- old three-scan tally vs new single-pass tally on a synthetic + losses census covering every vs_prev class, including parties for which a + class is ABSENT (the 0-default path the old sum returned). + 2. MICRO selftest fixtures -- same old-vs-new tally on the module's own + adjudicated selftest rows (real data shape). + 3. END-TO-END report() DRIFT -- the ORIGINAL module (git HEAD~1, the + pre-refactor commit; non-vacuous after the refactor is committed) and the + REFACTORED working-tree module both render the SAME res to StringIO; stdout + is byte-identical (sha256 match). + 4. SELFTEST DRIFT GUARD -- `python3 tools/append_only_owners.py --selftest` + exits 0 on the refactored worktree (the tool's own 15-cell contract). + 5. REDUNDANCY COLLAPSED -- the worktree carries ONE `party_vs = Counter(...)` + build and ZERO of the old `sum(1 for r in losses if r["author"] == k` scan. + +Exit code is the verdict: 0 = all green, 1 = any mismatch. +""" +import hashlib +import importlib.util +import io +import os +import shutil +import subprocess +import sys +import tempfile +from collections import Counter + +REPO = "/root/troupe-standup" +DCC = os.path.join(REPO, "tools", "append_only_owners.py") +SAME, OTHER, FIRST = "SAME_PARTY", "OTHER_PARTY", "FIRST_CHANGE_ON_PATH" + + +def sha(text): + return hashlib.sha256(text.encode()).hexdigest() + + +# --------------------------------------------------------------------------- +# OLD per-party tally: the three inline sum scans, verbatim pre-refactor. +# --------------------------------------------------------------------------- +def old_tally(losses): + out = [] + for k, v in Counter(r["author"] for r in losses).most_common(): + same = sum(1 for r in losses if r["author"] == k and r["vs_prev"] == SAME) + oth = sum(1 for r in losses if r["author"] == k and r["vs_prev"] == OTHER) + first = sum(1 for r in losses if r["author"] == k and r["vs_prev"] == FIRST) + out.append((k, v, same, oth, first)) + return out + + +# --------------------------------------------------------------------------- +# NEW per-party tally: one Counter pass + O(1) lookups, verbatim refactored. +# --------------------------------------------------------------------------- +def new_tally(losses): + party_vs = Counter((r["author"], r["vs_prev"]) for r in losses) + out = [] + for k, v in Counter(r["author"] for r in losses).most_common(): + same = party_vs.get((k, SAME), 0) + oth = party_vs.get((k, OTHER), 0) + first = party_vs.get((k, FIRST), 0) + out.append((k, v, same, oth, first)) + return out + + +class Verdict(Exception): + pass + + +def materialize_original(): + """Write the PRE-refactor source (git HEAD~1) under its real name in a temp + dir and return the path. HEAD~1 is the parent of the refactor commit, so + this reads the original even after the refactor is committed + pushed.""" + res = subprocess.run( + ["git", "-C", REPO, "show", "HEAD~1:tools/append_only_owners.py"], + capture_output=True, text=True) + if not res.stdout: + raise Verdict("could not read HEAD~1:tools/append_only_owners.py: " + + res.stderr.strip()) + d = tempfile.mkdtemp(prefix="aoo_orig_") + p = os.path.join(d, "append_only_owners.py") + with open(p, "w", encoding="utf-8") as fh: + fh.write(res.stdout) + os.chmod(p, 0o755) + return p + + +def load_module(path, name): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +def census_loss(author, vs_prev): + """A loss row carrying every key report() reads on a loss row.""" + return { + "author": author, "vs_prev": vs_prev, "vs_creator": vs_prev, + "shape": "PROSE", "loss_kind": "REWRITE", + "commit": "c1", "date": "2026-01-02T00:00:00Z", + "path": "checkins/x.md", "raw_author": author, + "prev_toucher": "someone", "parent_bytes": 10, + "child_bytes": 20, "missing_parent_lines": 1, + "break_text": "a break text line", + } + + +def census(): + """Per-party census covering every vs_prev class + the 0-default path. + + alice: 2 SAME, 1 OTHER, 0 FIRST (FIRST absent) + bob : 0 SAME, 0 OTHER, 1 FIRST (SAME/OTHER absent) + carol: 1 SAME, 0 OTHER, 2 FIRST (OTHER absent) + dave : 0 SAME, 2 OTHER, 0 FIRST (SAME/FIRST absent) + """ + return [ + census_loss("alice", SAME), census_loss("alice", SAME), census_loss("alice", OTHER), + census_loss("bob", FIRST), + census_loss("carol", SAME), census_loss("carol", FIRST), census_loss("carol", FIRST), + census_loss("dave", OTHER), census_loss("dave", OTHER), + ] + + +def selftest_rows(mod): + """Reproduce selftest()'s hand-built rows via the module's own _row().""" + _r = mod._row + return [ + _r("README.md", "2026-01-01T00:00:00Z", "alice", line_class="NEW"), + _r("checkins/a.md", "2026-01-01T00:00:00Z", "Alice", line_class="NEW"), + _r("checkins/a.md", "2026-01-02T00:00:00Z", "alice", + break_text="**Status: OPEN -- a", commit="c2"), + _r("checkins/b.md", "2026-01-01T00:00:00Z", "Bob", line_class="NEW"), + _r("checkins/b.md", "2026-01-02T00:00:00Z", "bob", + break_text="| 1 | x |", commit="c4"), + _r("WORK-QUEUE.md", "2026-01-01T00:00:00Z", "alice", line_class="NEW"), + _r("WORK-QUEUE.md", "2026-01-02T00:00:00Z", "bob", + break_text="plain prose line here", commit="c6"), + _r("replies/x.md", "2026-01-03T00:00:00Z", "carol", + break_text="2026-01-03T00:00:00Z reading", commit="c7"), + _r("tools/t.py", "2026-01-04T00:00:00Z", "dave", + break_text="gone", commit="c8"), + _r("checkins/a.md", "2026-01-05T00:00:00Z", "alice", + line_class="SUBSEQUENCE", commit="c9"), + ] + + +def show_diff(a, b): + la, lb = a.splitlines(), b.splitlines() + for i in range(max(len(la), len(lb))): + ga = la[i] if i < len(la) else "" + gb = lb[i] if i < len(lb) else "" + if ga != gb: + print(" live diff at line %d:" % (i + 1)) + print(" original: %r" % ga) + print(" refactored: %r" % gb) + return + print(" (identical length; mismatch is in byte value only)") + + +def main(): + ok = True + orig_path = materialize_original() + try: + tm_orig = load_module(orig_path, "aoo_orig") + tm_ref = load_module(DCC, "aoo_ref") + + # [1] micro equivalence on the census (every class + 0-default). + rows = census() + o, n = old_tally(rows), new_tally(rows) + micro_ok = o == n + print("[1] micro census: old_tally == new_tally ", "PASS" if micro_ok else "FAIL") + if not micro_ok: + ok = False + print(" old=%r" % (o,)) + print(" new=%r" % (n,)) + + # [2] micro equivalence on the module's own selftest fixtures. + sweep = tm_ref.adjudicate(selftest_rows(tm_ref)) + sweep_losses = sweep.get("losses", []) + micro2_ok = old_tally(sweep_losses) == new_tally(sweep_losses) + print("[2] micro selftest-row tally agree (%d losses) " + % len(sweep_losses), "PASS" if micro2_ok else "FAIL") + if not micro2_ok: + ok = False + + # [3] end-to-end report() DRIFT -- original (HEAD~1) vs refactored (tree). + res = {"spellings": [], "folded": {}, "losses": census()} + a, b = io.StringIO(), io.StringIO() + tm_orig.report(res, out=a) + tm_ref.report(res, out=b) + oa, ob = a.getvalue(), b.getvalue() + if not oa or "per committed party" not in oa: + raise Verdict("report() failed to render a valid census output") + drift_ok = oa == ob + print("[3] report() stdout original=%s refactored=%s %s" + % (sha(oa), sha(ob), "PASS" if drift_ok else "FAIL")) + if not drift_ok: + ok = False + show_diff(oa, ob) + + # [4] drift guard -- the tool's own 15-cell selftest on the worktree. + rc = subprocess.run([sys.executable, DCC, "--selftest"], + capture_output=True, text=True) + guard_ok = rc.returncode == 0 + print("[4] --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 ")) + + # [5] redundancy collapsed -- one Counter build, zero old sum scans. + text = open(DCC, encoding="utf-8").read() + # Count on CODE lines only -- the refactor's explanatory comment mentions + # the old `sum(1 for r in losses ...)` idiom, so a raw string count would + # false-positive against the comment, not the code. + code = "\n".join(ln for ln in text.splitlines() + if not ln.lstrip().startswith("#")) + builds = code.count('party_vs = Counter((r["author"], r["vs_prev"])') + scans = code.count('sum(1 for r in losses if r["author"] == k') + red_ok = builds == 1 and scans == 0 + print("[5] redundancy (code lines) party_vs builds=%d old-sum scans=%d %s" + % (builds, scans, "PASS" if red_ok else "FAIL")) + if not red_ok: + ok = False + + finally: + shutil.rmtree(os.path.dirname(orig_path), ignore_errors=True) + + print("\nVERDICT:", + "ALL GREEN -- per-party DRY collapse behavior preserved" 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)