287 lines
13 KiB
Python
287 lines
13 KiB
Python
"""q63_verify_scan.py -- grade the two ways a committed verifier can be a
|
|
decoration rather than a check (Q63, volt lane, 2026-10-24).
|
|
|
|
WHY THIS EXISTS
|
|
Q62 covered one way a verifier can lie: an input that lives outside the repo.
|
|
Q63 opened two more, both measured on committed files:
|
|
|
|
STRIPPED-ASSERT a verifier whose only failure path is `assert`. `python3 -O`
|
|
(and PYTHONOPTIMIZE=1) compiles every `assert` away, so the
|
|
file prints its success line and exits 0 against a subject it
|
|
would fail in normal mode. Measured at `89cda97`:
|
|
beam/verify_toposort_none printed ALL VERIFIED (rc 0) under
|
|
-O against a broken toposort whose normal-mode run returned
|
|
rc 1. This population is CLOSED: 6 of 87 at `89cda97`, 0 of
|
|
87 at `c033059`, and this scanner is the reason it stays 0.
|
|
A file is exit-safe when it carries `_check(`, a `raise`, or
|
|
`sys.exit()`/`exit()` with an argument that is not a zero
|
|
literal. `exit(0)` at the end of a file whose only checks are
|
|
asserts is NOT an exit path -- it is the false-PASS print.
|
|
|
|
UNWIRED nothing committed runs it. There are two honest definitions
|
|
and they differ by an order of magnitude, which is the first
|
|
thing this scan had to fix:
|
|
prose-grep `git grep -F <basename>` over every committed
|
|
file: 8 of 87 unwired. This is what Q63's own
|
|
opening record quotes -- and the record's 8 went
|
|
to 0 at the next commit, because the record
|
|
itself names all eight basenames. Prose about a
|
|
defect is not wiring for it.
|
|
code-grep the same grep over code pathspecs only
|
|
('*.py' '*.sh' 'CHECK' '*.yml' '*.yaml'):
|
|
73 of 87 unwired at `c033059`. No gate, test or
|
|
CHECK invokes them; `unittest discover` matches
|
|
`test_*` and no CHECK globs `verify_*.py`.
|
|
This scan grades the CODE definition, and holds the result in
|
|
a tolerance ledger rather than a claim: `q63_unwired_baseline.tsv`
|
|
names every unwired file measured today with its class
|
|
(`declared-one-off` when the file says so in-file, `undeclared`
|
|
otherwise). A NEW unwired file the ledger does not name is
|
|
rc 1 the moment it lands -- the same rule checkin_baseline.tsv
|
|
and reply_baseline.tsv already use, where a row is a stated
|
|
tolerance and not an exemption.
|
|
|
|
WHAT IT PRINTS
|
|
per-file rows only with --verbose; always the two counts, the tolerated rows,
|
|
and the command behind each figure.
|
|
|
|
EXIT CODES
|
|
0 no stripped-assert verifier; no unwired verifier outside the ledger
|
|
1 a fault: new stripped-assert file, or a new unwired file the ledger omits
|
|
2 could not grade (bad rev, git failure) -- outranks 1
|
|
|
|
Usage:
|
|
python3 wizard-work/volt/q63_verify_scan.py --repo .
|
|
python3 wizard-work/volt/q63_verify_scan.py --repo . --rev 89cda97 --verbose
|
|
python3 wizard-work/volt/q63_verify_scan.py --repo . --emit-baseline
|
|
python3 wizard-work/volt/q63_verify_scan.py --selftest
|
|
"""
|
|
import argparse
|
|
import json
|
|
import os
|
|
import re
|
|
import subprocess
|
|
import sys
|
|
|
|
DEFAULT_BASELINE = os.path.join(os.path.dirname(os.path.abspath(__file__)),
|
|
"q63_unwired_baseline.tsv")
|
|
VERIFY_RE = re.compile(r"/verify_.*\.py$")
|
|
ASSERT_RE = re.compile(r"(?m)^[ \t]*assert[ \t(]")
|
|
SAFE_PATH_RE = re.compile(r"\b_check\(")
|
|
RAISE_RE = re.compile(r"(?m)^[ \t]*raise\b")
|
|
EXIT_RE = re.compile(r"\b(?:sys\.)?exit\(\s*([^)]*?)\s*\)")
|
|
CODE_PATHSPECS = ["*.py", "*.sh", "CHECK", "*.yml", "*.yaml"]
|
|
DECLARED_RE = re.compile(r"Q63", re.I)
|
|
DECLARED_PHRASE = "no committed gate invokes"
|
|
|
|
|
|
def git(repo, *args):
|
|
p = subprocess.run(["git", "-C", repo, *args], capture_output=True)
|
|
if p.returncode != 0:
|
|
raise RuntimeError(f"git {' '.join(args)} -> rc {p.returncode}: "
|
|
f"{p.stderr.decode('utf-8', 'replace').strip()[:200]}")
|
|
return p.stdout.decode("utf-8", "replace")
|
|
|
|
|
|
def exit_safe(src):
|
|
"""True when a failing check cannot be swallowed by -O."""
|
|
if SAFE_PATH_RE.search(src) or RAISE_RE.search(src):
|
|
return True
|
|
for arg in EXIT_RE.findall(src):
|
|
if arg.strip() in ("", "None", "0", '"0"', "'0'"):
|
|
continue # exit() / exit(0): a success path
|
|
return True
|
|
return False
|
|
|
|
|
|
def scan(repo, rev):
|
|
if rev == "WORKTREE":
|
|
names = [n for n in git(repo, "ls-files").splitlines() if VERIFY_RE.search(n)]
|
|
blobs = {}
|
|
for n in names:
|
|
p = os.path.join(repo, n)
|
|
blobs[n] = open(p, encoding="utf-8", errors="replace").read() if os.path.isfile(p) else ""
|
|
else:
|
|
names = [n for n in git(repo, "ls-tree", "-r", "--name-only", rev).splitlines()
|
|
if VERIFY_RE.search(n)]
|
|
blobs = {n: git(repo, "show", f"{rev}:{n}") for n in names}
|
|
rows = []
|
|
for n in sorted(names):
|
|
src = blobs[n]
|
|
base = n.rsplit("/", 1)[-1]
|
|
bare = len(ASSERT_RE.findall(src))
|
|
refs = []
|
|
try:
|
|
refs = [ln for ln in git(repo, "grep", "-F", "-l", "--", base, rev,
|
|
"--", *CODE_PATHSPECS).splitlines() if ln != f"{rev}:{n}"]
|
|
except RuntimeError:
|
|
refs = [] # git grep rc 1 == no match: unwired
|
|
declared = bool(DECLARED_RE.search(src)) and DECLARED_PHRASE in src
|
|
faults = []
|
|
if bare and not exit_safe(src):
|
|
faults.append("STRIPPED_ASSERT")
|
|
rows.append({"path": n, "lane": n.split("/")[1], "asserts": bare,
|
|
"exit_safe": exit_safe(src), "wired_refs": refs,
|
|
"declared_one_off": declared, "faults": faults})
|
|
return rows
|
|
|
|
|
|
def read_baseline(path):
|
|
led = {}
|
|
if not os.path.isfile(path):
|
|
return led
|
|
for ln in open(path, encoding="utf-8"):
|
|
if not ln.strip() or ln.lstrip().startswith("#"):
|
|
continue
|
|
parts = ln.rstrip("\n").split("\t")
|
|
if len(parts) >= 2:
|
|
led[parts[1]] = parts[0]
|
|
return led
|
|
|
|
|
|
def grade(rows, ledger):
|
|
stripped = [r for r in rows if "STRIPPED_ASSERT" in r["faults"]]
|
|
unwired = [r for r in rows if not r["wired_refs"]]
|
|
new_unwired = [r for r in unwired if r["path"] not in ledger]
|
|
stale = [p for p in ledger if p not in {r["path"] for r in rows}]
|
|
return stripped, unwired, new_unwired, stale
|
|
|
|
|
|
def report(rows, ledger, rev, verbose=False):
|
|
lanes = {}
|
|
for r in rows:
|
|
lanes[r["lane"]] = lanes.get(r["lane"], 0) + 1
|
|
print(f"q63_verify_scan -- rev {rev}")
|
|
print(" committed verify_*.py : %d (%s)"
|
|
% (len(rows), " ".join(f"{k} {v}" for k, v in sorted(lanes.items(), key=lambda kv: -kv[1]))))
|
|
if verbose:
|
|
for r in rows:
|
|
tag = ",".join(r["faults"]) or ("wired" if r["wired_refs"] else ledger.get(r["path"], "NEW-UNWIRED"))
|
|
print(f" {'FAULT ' if r['faults'] else 'ok '}{r['asserts']:2d} assert {tag:18s} {r['path']}")
|
|
stripped, unwired, new_unwired, stale = grade(rows, ledger)
|
|
print(" stripped-assert : %d of %d (no _check/raise/non-zero exit; -O compiles `assert` away)"
|
|
% (len(stripped), len(rows)))
|
|
for r in stripped:
|
|
print(f" STRIPPED_ASSERT {r['path']}")
|
|
print(" unwired (code-grep) : %d of %d (`git grep -F -l <basename> %s -- %s`)"
|
|
% (len(unwired), len(rows), rev, " ".join(CODE_PATHSPECS)))
|
|
print(" unwired, ledger-tolerated : %d (%s: %d declared one-off, %d undeclared)"
|
|
% (len(unwired) - len(new_unwired), os.path.basename(DEFAULT_BASELINE),
|
|
sum(1 for r in unwired if ledger.get(r["path"]) == "declared-one-off"),
|
|
sum(1 for r in unwired if ledger.get(r["path"]) == "undeclared")))
|
|
print(" unwired, NEW (fault) : %d" % len(new_unwired))
|
|
for r in new_unwired:
|
|
print(f" NEW_UNWIRED {r['path']}")
|
|
if stale:
|
|
print(" stale ledger rows : %d (advisory): %s" % (len(stale), ", ".join(stale[:5])))
|
|
faults = len(stripped) + len(new_unwired)
|
|
print(f"q63: {faults} fault(s)")
|
|
return faults
|
|
|
|
|
|
def emit_baseline(rows, path):
|
|
out = ["# Q63 unwired-verifier baseline -- the unwired population this archive",
|
|
"# already carried when the rule was written. One row per file: <class>\\t<path>.",
|
|
"# class declared-one-off = the file states in-file that no gate invokes it;",
|
|
"# class undeclared = measured unwired, no such statement (the Q64 residual).",
|
|
"# A row is a stated tolerance, not an exemption: an unwired file that is NOT",
|
|
"# listed makes q63_verify_scan.py rc 1, and a stripped-assert file always does.",
|
|
"# Regenerate: q63_verify_scan.py --repo . --emit-baseline"]
|
|
for r in sorted(rows, key=lambda r: r["path"]):
|
|
if r["wired_refs"]:
|
|
continue
|
|
cls = "declared-one-off" if r["declared_one_off"] else "undeclared"
|
|
out.append(f"{cls}\t{r['path']}")
|
|
open(path, "w", encoding="utf-8").write("\n".join(out) + "\n")
|
|
print(f"baseline written: {path} ({sum(1 for r in rows if not r['wired_refs'])} rows)")
|
|
|
|
|
|
def selftest():
|
|
"""Four cells on a throwaway repo: the two fault classes, and the ledger rule."""
|
|
import tempfile
|
|
d = tempfile.mkdtemp(prefix="q63-selftest-")
|
|
env = dict(os.environ, GIT_AUTHOR_NAME="t", GIT_AUTHOR_EMAIL="t@t",
|
|
GIT_COMMITTER_NAME="t", GIT_COMMITTER_EMAIL="t@t")
|
|
subprocess.run(["git", "init", "-q", d], check=True, env=env)
|
|
cells, ok = [], True
|
|
|
|
def put(rel, text):
|
|
p = os.path.join(d, rel)
|
|
os.makedirs(os.path.dirname(p), exist_ok=True)
|
|
open(p, "w").write(text)
|
|
return rel
|
|
|
|
def commit(msg):
|
|
subprocess.run(["git", "-C", d, "add", "-A"], check=True, env=env)
|
|
subprocess.run(["git", "-C", d, "commit", "-qm", msg], check=True, env=env)
|
|
|
|
# (1) exit-safe + wired by a CHECK -> clean
|
|
put("tools/t.py", "print('ok')\n")
|
|
put("wizard-work/x/verify_safe.py", "import sys\n_check = None\nif 1:\n raise SystemExit('nope')\n")
|
|
put("wizard-work/x/CHECK", "python3 verify_safe.py\n")
|
|
commit("c1")
|
|
rows = scan(d, "HEAD")
|
|
led = {r["path"]: "declared-one-off" for r in rows if not r["wired_refs"]}
|
|
cells.append(("exit-safe and wired is clean", grade(rows, led)[3] == [] and not grade(rows, led)[0]
|
|
and not grade(rows, led)[2]))
|
|
|
|
# (2) bare asserts, no exit path -> STRIPPED_ASSERT even though wired
|
|
put("wizard-work/x/verify_assert.py", "assert 1 == 1\nprint('PASS')\n")
|
|
put("wizard-work/x/CHECK", "python3 verify_safe.py\npython3 verify_assert.py\n")
|
|
commit("c2")
|
|
rows = scan(d, "HEAD")
|
|
led = {r["path"]: "declared-one-off" for r in rows}
|
|
cells.append(("bare assert without exit path is a fault", len(grade(rows, led)[0]) == 1))
|
|
|
|
# (3) unwired and not in the ledger -> NEW_UNWIRED
|
|
put("wizard-work/x/verify_orphan.py", "import sys\nsys.exit(1)\n")
|
|
commit("c3")
|
|
rows = scan(d, "HEAD")
|
|
led = {r["path"]: "declared-one-off" for r in rows if not r["wired_refs"]
|
|
and "orphan" not in r["path"]}
|
|
cells.append(("unwired file the ledger omits is a fault", len(grade(rows, led)[2]) == 1))
|
|
|
|
# (4) the same file listed in the ledger -> tolerated
|
|
led["wizard-work/x/verify_orphan.py"] = "undeclared"
|
|
cells.append(("unwired file the ledger names is tolerated", len(grade(rows, led)[2]) == 0))
|
|
|
|
for name, passed in cells:
|
|
print(f" {'PASS' if passed else 'FAIL'} {name}")
|
|
ok &= passed
|
|
print(f"selftest: {sum(1 for _, p in cells if p)}/{len(cells)}")
|
|
return 0 if ok else 1
|
|
|
|
|
|
def main():
|
|
ap = argparse.ArgumentParser()
|
|
ap.add_argument("--repo", default=".")
|
|
ap.add_argument("--rev", default="HEAD")
|
|
ap.add_argument("--baseline", default=DEFAULT_BASELINE)
|
|
ap.add_argument("--emit-baseline", action="store_true")
|
|
ap.add_argument("--json")
|
|
ap.add_argument("--verbose", action="store_true")
|
|
ap.add_argument("--selftest", action="store_true")
|
|
a = ap.parse_args()
|
|
if a.selftest:
|
|
return selftest()
|
|
try:
|
|
rows = scan(a.repo, a.rev)
|
|
except RuntimeError as e:
|
|
print(f"q63_verify_scan: cannot grade: {e}")
|
|
return 2
|
|
if a.emit_baseline:
|
|
emit_baseline(rows, a.baseline)
|
|
return 0
|
|
faults = report(rows, read_baseline(a.baseline), a.rev, a.verbose)
|
|
if a.json:
|
|
stripped, unwired, new_unwired, stale = grade(rows, read_baseline(a.baseline))
|
|
with open(a.json, "w", encoding="utf-8") as f:
|
|
json.dump({"rev": a.rev, "verifiers": len(rows), "rows": rows,
|
|
"stripped_assert": len(stripped), "unwired": len(unwired),
|
|
"new_unwired": len(new_unwired), "stale": stale}, f, indent=1)
|
|
return 0 if faults == 0 else 1
|
|
|
|
|
|
if __name__ == "__main__":
|
|
sys.exit(main())
|