360 lines
17 KiB
Python
360 lines
17 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 -- still too generous, because a basename
|
|
spelled in a docstring, a report string or a
|
|
git-show snapshot path is a mention, not a runner.
|
|
invoke-grep the same grep with every reference classified:
|
|
python3 X / runpy / import / ./X counts as
|
|
wiring, anything else is a mention, and a bare
|
|
basename only wires the file in its own directory
|
|
(`verify_archive.py` exists in four sphinx
|
|
archives). Result at `c033059`: 80 of 87 unwired,
|
|
7 with an invocation-shaped line, and `--why`
|
|
prints those seven lines so the figure is read
|
|
rather than trusted.
|
|
This scan grades the INVOKE 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"
|
|
# The measuring instruments name every file in the class; naming is not running.
|
|
INSTRUMENT_DIR = "wizard-work/volt/"
|
|
# INVOCATION, not mention. A code file that spells the basename in a git-show
|
|
# string, a docstring or a report wires nothing -- the first version of this
|
|
# scanner counted those as wired, and its own proof harness "wired" five files
|
|
# it only read from a blob. A reference counts only in a shape that runs it.
|
|
INVOKE_PATTERNS = [
|
|
r"(?:python3?|python|sys\.executable|\$PY)[^\n]*{base}", # python3 verify_x.py
|
|
r"(?:runpy|run_path|run_module|importlib)[^\n]*{base}", # runpy.run_path("verify_x.py")
|
|
r"(?:import\s+{stem}\b)", # import verify_x
|
|
r"(?:^|[;&|]\s*|\./|bash\s+|sh\s+){base}", # ./verify_x.py
|
|
]
|
|
|
|
|
|
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 wiring_refs(repo, rev, path, base, stem):
|
|
"""(invocations, mentions) for one basename at one revision.
|
|
|
|
git grep gives the lines; each line is classified. Two accuracy rules, both
|
|
paid for by measurement rather than assumed:
|
|
|
|
* a reference counts only in an INVOCATION shape (python3 X, runpy/import,
|
|
./X). A docstring, a report string or a git-show snapshot path is a
|
|
MENTION: it wires nothing, and counting it would hide a dead verifier.
|
|
* a bare basename is directory-local. `verify_archive.py` exists in four
|
|
sphinx archives; a reference from another archive's directory is a
|
|
reference to ITS sibling, not to this file. So a wiring reference must
|
|
either name this file's parent directory, or sit in the same directory.
|
|
"""
|
|
args = ["grep", "-F", "-n", "--", base]
|
|
if rev != "WORKTREE":
|
|
args.append(rev)
|
|
args += ["--", *CODE_PATHSPECS]
|
|
try:
|
|
lines = git(repo, *args).splitlines()
|
|
except RuntimeError:
|
|
return [], [] # git grep rc 1 == no match
|
|
inv, men = [], []
|
|
mydir = os.path.dirname(path)
|
|
for ln in lines:
|
|
# git grep output is REV:path:line:text at a rev, path:line:text on disk
|
|
rest = ln.split(":", 1)[1] if rev != "WORKTREE" else ln
|
|
where = rest.split(":", 2)[0]
|
|
if where == path:
|
|
continue # the file's own text is not a reference
|
|
if where.startswith(INSTRUMENT_DIR):
|
|
continue # the instruments that measure this class
|
|
hit = any(re.search(p.format(base=re.escape(base), stem=re.escape(stem)), rest)
|
|
for p in INVOKE_PATTERNS)
|
|
same_dir = os.path.dirname(where) == mydir
|
|
names_dir = mydir and (mydir + "/") in rest
|
|
if hit and (same_dir or names_dir):
|
|
inv.append(ln)
|
|
else:
|
|
men.append(ln)
|
|
return inv, men
|
|
|
|
|
|
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]
|
|
stem = base[:-3]
|
|
bare = len(ASSERT_RE.findall(src))
|
|
refs, mentions = wiring_refs(repo, rev, n, base, stem)
|
|
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,
|
|
"mention_refs": mentions,
|
|
"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 Q65 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("--why", action="store_true",
|
|
help="print the lines counted as wiring and as mention, per file")
|
|
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.why:
|
|
print("\nwiring detail (what the count is made of):")
|
|
for r in rows:
|
|
if not (r["wired_refs"] or r["mention_refs"]):
|
|
continue
|
|
print(f" {r['path']}")
|
|
for ln in r["wired_refs"]:
|
|
print(f" WIRED {ln[:150]}")
|
|
for ln in r["mention_refs"][:3]:
|
|
print(f" mention {ln[:150]}")
|
|
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())
|