From 146881185328dc78de82644d1f51e09e5ef32be4 Mon Sep 17 00:00:00 2001 From: forge Date: Fri, 23 Oct 2026 23:41:25 +0000 Subject: [PATCH] =?UTF-8?q?forge:=20append=5Fonly=5Faudit=20DRY=20collapse?= =?UTF-8?q?=20=E2=80=94=20extract=20=5Fsubseq=5Fmatch=5Fcount=20from=20dup?= =?UTF-8?q?licated=20subsequence=20scan=20in=20line=5Ftest=20+=20is=5Fline?= =?UTF-8?q?=5Fsubsequence?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- tools/append_only_audit.py | 27 +- .../verify_append_only_audit_dry_refactor.py | 317 ++++++++++++++++++ 2 files changed, 335 insertions(+), 9 deletions(-) create mode 100644 wizard-work/forge/verify_append_only_audit_dry_refactor.py diff --git a/tools/append_only_audit.py b/tools/append_only_audit.py index 67bfaa6..c20f89a 100644 --- a/tools/append_only_audit.py +++ b/tools/append_only_audit.py @@ -167,10 +167,7 @@ def line_test(parent_bytes, child_bytes): return "IDENTICAL", None, "", 0, 0 missing = sum((Counter(pl) - Counter(cl)).values()) added = sum((Counter(cl) - Counter(pl)).values()) - i = 0 - for ln in cl: - if i < len(pl) and ln == pl[i]: - i += 1 + i = _subseq_match_count(pl, cl) if i == len(pl): return "SUBSEQUENCE", None, "", 0, added return "LOSS", i + 1, pl[i].decode("utf-8", "replace")[:120], missing, added @@ -187,14 +184,26 @@ def escape_unescape(b): return ESCAPE_RE.sub(lambda m: chr(int(m.group(1), 16)).encode("utf-8"), b) +def _subseq_match_count(parent_lines, child_lines): + """Greedy count of parent_lines that match, in order, within child_lines. + + Returns the number of parent_lines consumed by the forward scan: + len(parent_lines) means the parent is a subsequence of the child; a + smaller value means the scan broke after that many matches, and + parent_lines[i] is the first parent line that did not match. + """ + i = 0 + for ln in child_lines: + if i < len(parent_lines) and ln == parent_lines[i]: + i += 1 + return i + + def is_line_subsequence(a_bytes, b_bytes): + """True iff a_bytes's lines are an order-preserving subsequence of b_bytes's.""" al = a_bytes.split(b"\n") bl = b_bytes.split(b"\n") - i = 0 - for ln in bl: - if i < len(al) and ln == al[i]: - i += 1 - return i == len(al) + return _subseq_match_count(al, bl) == len(al) def loss_kind(parent_bytes, child_bytes): diff --git a/wizard-work/forge/verify_append_only_audit_dry_refactor.py b/wizard-work/forge/verify_append_only_audit_dry_refactor.py new file mode 100644 index 0000000..6e2fe6a --- /dev/null +++ b/wizard-work/forge/verify_append_only_audit_dry_refactor.py @@ -0,0 +1,317 @@ +#!/usr/bin/env python3 +"""verify_append_only_audit_dry_refactor.py + +Equivalence proof for the DRY collapse in tools/append_only_audit.py +(forge lane: Refactor). + +THE SMELL + The greedy subsequence-walk loop was hand-duplicated, verbatim, in two + functions that do the same scan with different variable names: + + line_test() -- inlined in the audit engine: + i = 0 + for ln in cl: + if i < len(pl) and ln == pl[i]: + ^-- the inlined loop (4 lines) + + is_line_subsequence() -- the standalone predicate used by loss_kind(): + i = 0 + for ln in bl: + if i < len(al) and ln == al[i]: + ^-- the SAME loop, verbatim, only variable names differ + return i == len(al) + + Two copies of one 4-line statement is the canonical DRY smell; each edit to + the scan logic would have to touch both, and a third call site would be a + third freehand copy. + +THE REFACTOR + One module-level helper replaces both inlined loops: + + def _subseq_match_count(parent_lines, child_lines): + ... # the single greedy scan + return i # number of parent_lines consumed + + line_test(): i = _subseq_match_count(pl, cl) + is_line_subsequence(): return _subseq_match_count(al, bl) == len(al) + +WHAT THIS VERIFIER PROVES (post-commit: HEAD~1 = original, HEAD = refactored) + + [1] selftest: ORIGINAL (HEAD~1) 18/18 rc 0 + [2] selftest: REFACTORED (HEAD) 18/18 rc 0 + [3] selftest: stdout BYTE-IDENTICAL (original == refactored) + [4] code-level: refactored HAS _subseq_match_count; original has NONE + [5] code-level: refactored inlined-loops = 0; original inlined-loops >= 1 + [6] non-vacuity: live selftest produced a real 18-cell census + [7] line_test direct equivalence on 8 edge-case inputs + [8] is_line_subsequence direct equivalence on 6 inputs + [9] loss_kind direct equivalence on 4 inputs (calls is_line_subsequence) + [10] report() on a real synthetic audit: BYTE-IDENTICAL stdout + [11] verifier itself committed to HEAD + +Exit 0 iff all checks pass, else 1. +""" +import hashlib +import importlib.util +import io +import os +import shutil +import subprocess +import sys +import tempfile + +REPO = "/root/troupe-standup" +TOOL = "tools/append_only_audit.py" +VERIFIER_NAME = "verify_append_only_audit_dry_refactor.py" +VERIFIER_PATH = "wizard-work/forge/" + VERIFIER_NAME +SUMMARY = "selftest: 18 cells, 18 passed, 0 failed" +HELPER = "def _subseq_match_count(" +INLINED_CL = "for ln in cl:" +INLINED_BL = "for ln in bl:" +TMPDIR = os.environ.get("TMPDIR", tempfile.gettempdir()) + + +class Mismatch(Exception): + pass + + +def git_show(rev, path): + """Return the text of `path` at git revision `rev` in REPO.""" + proc = subprocess.run(["git", "-C", REPO, "show", f"{rev}:{path}"], + capture_output=True, text=True, timeout=60) + if proc.returncode != 0: + raise Mismatch(f"cannot read {rev}:{path}: {proc.stderr.strip()}") + return proc.stdout + + +def materialize_original(): + """Write the pre-refactor source (HEAD~1) to a temp file; return path.""" + src = git_show("HEAD~1", TOOL) + d = tempfile.mkdtemp(prefix="aoa_orig_") + p = os.path.join(d, "append_only_audit.py") + with open(p, "w", encoding="utf-8") as fh: + fh.write(src) + 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 run_script(source_text, args): + """Write source_text to an isolated temp file and run with args.""" + fd, path = tempfile.mkstemp(suffix=".py", dir=TMPDIR) + try: + with os.fdopen(fd, "w") as fh: + fh.write(source_text) + proc = subprocess.run([sys.executable, path] + list(args), + capture_output=True, text=True, timeout=120) + return proc.returncode, proc.stdout, proc.stderr + finally: + os.unlink(path) + + +def count_inlined_loops(text): + """Count bare `for ln in cl:` / `for ln in bl:` loop headers in code (not comments).""" + code_lines = [ln for ln in text.splitlines() + if not ln.lstrip().startswith("#")] + return sum(1 for ln in code_lines if ln.strip() in (INLINED_CL, INLINED_BL)) + + +def sha(text): + return hashlib.sha256(text.encode()).hexdigest() + + +# --------------------------------------------------------------------------- +# Direct equivalence cases: (parent_bytes, child_bytes, description) +# --------------------------------------------------------------------------- +EDGE_CASES_LINE_TEST = [ + (b"", b"hello\n", "NO_PARENT (empty parent)"), + (b"same\n", b"same\n", "IDENTICAL"), + (b"a\nb\n", b"a\nb\nc\n", "APPEND (byte prefix)"), + (b"a\nb\n", b"a\nX\nb\nc\n", "SUBSEQUENCE (mid insertion)"), + (b"a\nb\nc\n", b"a\nb\n", "LOSS (parent longer)"), + (b"\n\n\n", b"x\ny\nz\n", "LOSS (no match)"), + (b"dash \\u2014 here\nplain\n", b"dash \u2014 here\nplain\n", + "ESCAPE_NORMALISATION path"), + (b"alpha\nbeta\n", b"ALPHA\nbeta\n", "LOSS (case change)"), +] + +EDGE_CASES_SUBSEQ = [ + (b"a\nb\n", b"a\nb\nc\n", True, "a is subsequence of abc"), + (b"a\nb\n", b"a\nX\nb\nc\n", True, "a is subsequence of aXb"), + (b"a\nb\nc\n", b"a\nb\n", False, "abc is not subsequence of ab"), + (b"alpha\n", b"ALPHA\n", False, "alpha != ALPHA"), + (b"", b"anything\n", True, "empty parent is trivially subsequence"), + (b"x\ny\n", b"y\nx\n", False, "NOT order-preserving"), +] + +EDGE_CASES_LOSS_KIND = [ + (b"dash \\u2014 here\nplain\n", b"dash \u2014 here\nplain\n", + "ESCAPE_NORMALISATION", "escape rewrite"), + (b"alpha\nbeta\n", b"ALPHA\nbeta\n", + "REWRITE", "case change"), + (b"a\nb\nc\n", b"a\nb\nx\n", + "REWRITE", "last line changed"), + (b"foo\nbar\n", b"FOO\nbaz\n", + "REWRITE", "both lines changed"), +] + + +def make_fixture_repo(tmp): + """A synthetic git repo with append / mid-insertion / loss history.""" + repo = os.path.join(tmp, "repo") + os.makedirs(repo) + env = dict(os.environ, GIT_AUTHOR_NAME="t", GIT_AUTHOR_EMAIL="t@e", + GIT_COMMITTER_NAME="t", GIT_COMMITTER_EMAIL="t@e") + subprocess.run(["git", "init", "-q", "-b", "main", repo], check=True, env=env, + capture_output=True) + + def w(path, data): + p = os.path.join(repo, path) + os.makedirs(os.path.dirname(p), exist_ok=True) + with open(p, "w") as fh: + fh.write(data) + + def g(*a): + subprocess.run(["git", "-C", repo] + list(a), check=True, env=env, + capture_output=True) + + w("a.txt", "one\ntwo\n") + w("mid.txt", "head\nbody\ntail\n") + g("add", "-A") + g("commit", "-qm", "c1") + + p = os.path.join(repo, "a.txt") + with open(p, "a") as fh: + fh.write("three\n") + g("add", "-A"); g("commit", "-qm", "c2 append") + + p = os.path.join(repo, "mid.txt") + with open(p, "w") as fh: + fh.write("head\nINSERTED\nbody\ntail\n") + g("add", "-A"); g("commit", "-qm", "c3 mid insertion") + + p = os.path.join(repo, "mid.txt") + with open(p, "w") as fh: + fh.write("head\nINSERTED\ntail\n") + g("add", "-A"); g("commit", "-qm", "c4 loss") + return repo + + +def main(): + ok = True + cells, failed = [], [] + + def check(label, passed, detail=""): + cells.append(label) + status = "ok " if passed else "FAIL" + print(f" [{status}] {label}" + (f" [{detail}]" if detail and not passed else "")) + if not passed: + failed.append(f"{label}: {detail}" if detail else label) + nonlocal ok + ok = False + + orig_path = materialize_original() + try: + orig_src = git_show("HEAD~1", TOOL) + with open(os.path.join(REPO, TOOL), encoding="utf-8") as fh: + ref_src = fh.read() + + mod_o = load_module(orig_path, "aoa_orig") + mod_r = load_module(os.path.join(REPO, TOOL), "aoa_ref") + + # ---- [1-3] selftest equivalence --------------------------------------- + rc_o, out_o, _ = run_script(orig_src, ["--selftest"]) + rc_r, out_r, _ = run_script(ref_src, ["--selftest"]) + check("[1] selftest: ORIGINAL (HEAD~1) 18/18 rc 0", + rc_o == 0 and SUMMARY in out_o, f"rc={rc_o} {out_o[-120:]}") + check("[2] selftest: REFACTORED (HEAD) 18/18 rc 0", + rc_r == 0 and SUMMARY in out_r, f"rc={rc_r} {out_r[-120:]}") + check("[3] selftest: stdout BYTE-IDENTICAL (original == refactored)", + out_o == out_r, f"len_o={len(out_o)} len_r={len(out_r)}") + + # ---- [4-5] code-level: smell existed and was collapsed ---------------- + check("[4] refactored HAS _subseq_match_count; original NONE", + HELPER in ref_src and HELPER not in orig_src, + f"ref={HELPER in ref_src} orig={HELPER in orig_src}") + check("[5] refactored inlined-loops = 0; original >= 1", + count_inlined_loops(ref_src) == 0 and count_inlined_loops(orig_src) >= 1, + f"ref={count_inlined_loops(ref_src)} orig={count_inlined_loops(orig_src)}") + + # ---- [6] non-vacuity -------------------------------------------------- + check("[6] non-vacuity: live selftest produced a real 18-cell census", + "c01" in out_r and "PASS" in out_r and out_r.count("PASS") >= 17) + + # ---- [7-9] direct function equivalence -------------------------------- + mismatches = [] + for pb, cb, desc in EDGE_CASES_LINE_TEST: + o = mod_o.line_test(pb, cb) + r = mod_r.line_test(pb, cb) + if o != r: + mismatches.append(f"line_test {desc}: {o!r} != {r!r}") + check("[7] line_test direct equivalence (8 edge cases)", + not mismatches, "; ".join(mismatches)[:300]) + + subseq_mismatches = [] + for pb, cb, want, desc in EDGE_CASES_SUBSEQ: + o = mod_o.is_line_subsequence(pb, cb) + r = mod_r.is_line_subsequence(pb, cb) + if o != r or o != want: + subseq_mismatches.append(f"{desc}: orig={o} ref={r} want={want}") + check("[8] is_line_subsequence direct equivalence (6 inputs)", + not subseq_mismatches, "; ".join(subseq_mismatches)[:300]) + + lk_mismatches = [] + for pb, cb, want, desc in EDGE_CASES_LOSS_KIND: + o = mod_o.loss_kind(pb, cb) + r = mod_r.loss_kind(pb, cb) + if o != r or o != want: + lk_mismatches.append(f"{desc}: orig={o} ref={r} want={want}") + check("[9] loss_kind direct equivalence (4 inputs, via is_line_subsequence)", + not lk_mismatches, "; ".join(lk_mismatches)[:300]) + + # ---- [10] report() byte-identical on a real synthetic audit ----------- + with tempfile.TemporaryDirectory(prefix="aoa_report_") as td: + repo = make_fixture_repo(td) + res_o = mod_o.audit(repo) + res_r = mod_r.audit(repo) + check("[10a] audit() rows match structurally", + len(res_o["rows"]) == len(res_r["rows"]) + and all(r_o == r_r for r_o, r_r in zip(res_o["rows"], res_r["rows"])), + f"n_o={len(res_o['rows'])} n_r={len(res_r['rows'])}") + buf_o, buf_r = io.StringIO(), io.StringIO() + mod_o.report(res_o, out=buf_o) + mod_r.report(res_r, out=buf_r) + check("[10b] report() stdout BYTE-IDENTICAL", + buf_o.getvalue() == buf_r.getvalue(), + f"sha_o={sha(buf_o.getvalue()[:12])} sha_r={sha(buf_r.getvalue()[:12])}") + + # ---- [11] verifier committed to HEAD ---------------------------------- + rc_gc = subprocess.run( + ["git", "-C", REPO, "cat-file", "-e", f"HEAD:{VERIFIER_PATH}"], + capture_output=True).returncode + check("[11] verifier committed to HEAD", rc_gc == 0, f"cat-file rc={rc_gc}") + + finally: + shutil.rmtree(os.path.dirname(orig_path), ignore_errors=True) + + print(f"\nverify: {len(cells)} checks, {len(cells) - len(failed)} passed, {len(failed)} failed") + for f in failed: + print(f" FAIL {f}") + verdict = ("ALL GREEN -- append_only_audit DRY collapse behavior preserved" + if ok else "MISMATCH -- behavior NOT preserved") + print(f"\nVERDICT: {verdict}") + return 0 if ok else 1 + + +if __name__ == "__main__": + try: + sys.exit(main()) + except Mismatch as e: + print(f"\nVERDICT: MISMATCH -- {e}") + sys.exit(1)