669 lines
32 KiB
Python
669 lines
32 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 ast
|
|
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")
|
|
# Q65: the runner ledger. A file this carries a GRADED row for was executed and
|
|
# its rc recorded -- see q65_runner.py. Class `gate-run` in the baseline below.
|
|
DEFAULT_GATE = os.path.join(os.path.dirname(os.path.abspath(__file__)),
|
|
"q65_runner_baseline.tsv")
|
|
GATE_RC = {"PASS": "0", "FAIL": "1", "REFUSED": "2"}
|
|
# Q150: the population is every committed basename verify_*.py, at any depth.
|
|
# This regex used to be r"/verify_.*\.py$" -- a SLASH was required, so a
|
|
# verifier committed at the repo root was invisible here while
|
|
# q65_runner.VERIFIER_RE (basename match, ^verify_[^/]*\.py$) counted it: two
|
|
# instruments, two populations, and the disagreement printed as an
|
|
# `UNCLASSED verify_wordcount.py` fault no census row could ever clear.
|
|
# Measured at fe23317: this scan said 196 committed verifiers, q65_runner's
|
|
# rev_files said 197, and the missing one is root verify_wordcount.py (ef83d3d).
|
|
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*\)")
|
|
# `CHECK` as a bare pathspec is a LITERAL path: it matches ./CHECK only, so the
|
|
# four nested `wizard-work/*/CHECK` files were outside the wiring grep until
|
|
# 2026-10-24. Measured at `2bc2662` with `:(glob)**/CHECK`: the same 7 files are
|
|
# wired, because no nested CHECK invokes a verify_*.py (they run
|
|
# `unittest discover -p 'test_*.py'`). The defect was latent, not academic:
|
|
# a nested CHECK that ran a verifier would have been read as not running it.
|
|
CODE_PATHSPECS = ["*.py", "*.sh", ":(glob)**/CHECK", ":(glob)**/CHECK.txt",
|
|
"*.yml", "*.yaml"]
|
|
# `CHECK.txt` was the second half of the same defect, measured 2026-10-25 at
|
|
# `30653c6`: sphinx's `archive-agentic-memory-5paper-dossier-2026-10-25/CHECK.txt`
|
|
# is one line, `python3 "$(dirname "$0")/verify_claims.py"`, and the file sat in
|
|
# the NEW_UNWIRED fault list while its own committed gate invoked it. Adding
|
|
# `:(glob)**/CHECK.txt` and holding every other argument fixed moves
|
|
# `wired by name (invoke)` 7 -> 8 and `unwired, NEW (fault)` 5 -> 4, with the
|
|
# one file that moves being exactly that verifier. A pathspec is a claim about
|
|
# where a runner may live; leaving a gate filename out of it files a false
|
|
# fault against the lane that wrote the gate.
|
|
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
|
|
|
|
|
|
# A basename that appears only inside a string literal is a MENTION unless the
|
|
# line also carries an exec-shaped call: a command quoted in a report string runs
|
|
# nothing, the same command passed to subprocess.run() is the invocation itself.
|
|
EXEC_RE = re.compile(r"\b(?:subprocess|Popen|runpy|run_path|run_module|"
|
|
r"check_call|check_output|os\.system|os\.exec\w*|executable)\b")
|
|
_KIND_CACHE = {}
|
|
|
|
|
|
def _docstring_rows(tree):
|
|
"""Rows covered by a module/class/function docstring -- never executed."""
|
|
rows = set()
|
|
for node in ast.walk(tree):
|
|
if not isinstance(node, (ast.Module, ast.ClassDef, ast.FunctionDef,
|
|
ast.AsyncFunctionDef)):
|
|
continue
|
|
body = getattr(node, "body", [])
|
|
if body and isinstance(body[0], ast.Expr) and \
|
|
isinstance(body[0].value, ast.Constant) and \
|
|
isinstance(body[0].value.value, str):
|
|
first = body[0].value
|
|
rows |= set(range(first.lineno, (first.end_lineno or first.lineno) + 1))
|
|
return rows
|
|
|
|
|
|
def py_line_kinds(src):
|
|
"""line number -> 'dead' | 'string', for the lines of one Python referrer.
|
|
|
|
'dead' the line is inside a docstring or is a comment: the interpreter
|
|
never runs it, so no shape on that line invokes anything.
|
|
'string' a string literal covers the line (a report line, a message) -- an
|
|
invocation is still possible there, but only if the line also
|
|
carries an exec-shaped call; the caller applies that second test.
|
|
|
|
Returns None when the source does not parse: the caller then falls back to
|
|
the grep shape rather than guessing, which is the old behaviour.
|
|
"""
|
|
import tokenize, io as _io
|
|
try:
|
|
tree = ast.parse(src)
|
|
except SyntaxError:
|
|
return None
|
|
kinds = {}
|
|
for row in _docstring_rows(tree):
|
|
kinds[row] = "dead"
|
|
for node in ast.walk(tree):
|
|
if isinstance(node, ast.Constant) and isinstance(node.value, str):
|
|
last = node.end_lineno or node.lineno
|
|
for row in range(node.lineno, last + 1):
|
|
kinds.setdefault(row, "string")
|
|
try:
|
|
for tok in tokenize.generate_tokens(_io.StringIO(src).readline):
|
|
if tok.type == tokenize.COMMENT:
|
|
row, col = tok.start
|
|
line = src.splitlines()[row - 1] if row <= len(src.splitlines()) else ""
|
|
if not line[:col].strip(): # comment-only line
|
|
kinds[row] = "dead"
|
|
except (tokenize.TokenError, IndentationError, SyntaxError):
|
|
pass
|
|
return kinds
|
|
|
|
|
|
def ref_kinds(repo, rev, where):
|
|
"""(kind map, error) for the referrer at `rev`; cached per path."""
|
|
key = (repo, rev, where)
|
|
if key in _KIND_CACHE:
|
|
return _KIND_CACHE[key]
|
|
try:
|
|
if rev == "WORKTREE":
|
|
src = open(os.path.join(repo, where), encoding="utf-8",
|
|
errors="replace").read()
|
|
else:
|
|
src = git(repo, "show", "%s:%s" % (rev, where))
|
|
except (OSError, RuntimeError):
|
|
_KIND_CACHE[key] = None
|
|
return None
|
|
if where.endswith(".py"):
|
|
kinds = py_line_kinds(src)
|
|
else:
|
|
kinds = {}
|
|
for n, line in enumerate(src.splitlines(), 1):
|
|
if line.lstrip().startswith("#"):
|
|
kinds[n] = "dead" # shell/yaml comment: never run
|
|
_KIND_CACHE[key] = kinds
|
|
return kinds
|
|
|
|
|
|
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. Three accuracy rules, all
|
|
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.
|
|
* THE SHAPE IS TESTED ON THE LINE TEXT, NEVER ON `<path>:<line>:`. The
|
|
first version tested `rest` -- the whole grep record -- so an interpreter
|
|
token could come from the REFERRER'S OWN FILENAME: the prose line
|
|
`- Verdict: the sibling verify_github_python_repos.py re-queries` was
|
|
read as `python ... verify_github_python_repos.py` and wired a verifier
|
|
nothing invokes, because the referring file is itself named
|
|
`extract_github_python_repos.py`. Measured at `b01ec0e`; the line was
|
|
WIRED before this rule and is a mention after it.
|
|
|
|
And a shape found inside unexecuted text is not a shape: `ref_kinds` marks
|
|
docstring and comment lines dead, and a string-only line is a mention unless
|
|
it also carries an exec-shaped call.
|
|
"""
|
|
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, _, tail = rest.partition(":")
|
|
num, _, text = tail.partition(":")
|
|
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)), text)
|
|
for p in INVOKE_PATTERNS)
|
|
same_dir = os.path.dirname(where) == mydir
|
|
names_dir = mydir and (mydir + "/") in text
|
|
kind = None
|
|
if hit:
|
|
kinds = ref_kinds(repo, rev, where)
|
|
if kinds is not None:
|
|
kind = kinds.get(int(num)) if num.isdigit() else None
|
|
if kind == "dead":
|
|
hit = False # docstring or comment: unexecuted
|
|
elif kind == "string" and not EXEC_RE.search(text):
|
|
hit = False # a command quoted in a report string
|
|
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] if "/" in n else "(root)",
|
|
"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 read_gate(path):
|
|
"""path -> verdict, for rows whose verdict and rc AGREE.
|
|
|
|
Assumes nothing about the ledger's writer. The rule that makes a row
|
|
evidence of a run is the one q65_runner.py grades itself with: the verdict
|
|
must match the rc recorded beside it. A row that says PASS with rc 1, or
|
|
TIMEOUT with no rc, is not a grade -- there is no rc to grade -- so the file
|
|
stays unwired here and the fault is the one Q65 opened, not a tolerated row.
|
|
"""
|
|
gate, ungraded = {}, {}
|
|
if not os.path.isfile(path):
|
|
return gate, ungraded
|
|
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) < 4:
|
|
continue
|
|
verdict, rc, p = parts[2], parts[3], parts[1]
|
|
if verdict in GATE_RC and rc == GATE_RC[verdict]:
|
|
gate[p] = verdict
|
|
elif verdict == "OTHER_RC" and rc.isdigit() and int(rc) > 2:
|
|
gate[p] = verdict
|
|
else:
|
|
ungraded[p] = verdict
|
|
return gate, ungraded
|
|
|
|
|
|
def grade(rows, ledger, gate=None):
|
|
gate = gate or {}
|
|
stripped = [r for r in rows if "STRIPPED_ASSERT" in r["faults"]]
|
|
unwired = [r for r in rows if not r["wired_refs"] and r["path"] not in gate]
|
|
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, gate=None, ungraded=None):
|
|
gate = gate or {}
|
|
ungraded = ungraded or {}
|
|
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, gate)
|
|
ran = [r for r in rows if r["path"] in gate and not r["wired_refs"]]
|
|
by_verdict = {}
|
|
for r in ran:
|
|
by_verdict[gate[r["path"]]] = by_verdict.get(gate[r["path"]], 0) + 1
|
|
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(" wired by name (invoke) : %d of %d" % (len(rows) - len([r for r in rows if not r['wired_refs']]), len(rows)))
|
|
print(" run by q65_runner : %d (%s)"
|
|
% (len(ran), ", ".join(f"{k} {v}" for k, v in sorted(by_verdict.items())) or "no graded row"))
|
|
for p, v in sorted(ungraded.items()):
|
|
print(f" NOT_GRADED {v:9s} {p} (ledger row without an rc to grade)")
|
|
print(" unwired (code-grep) : %d of %d (`git grep -F -l <basename> %s -- %s`)"
|
|
% (len(unwired), len(rows), rev, " ".join(CODE_PATHSPECS)))
|
|
tol = len(unwired) - len(new_unwired)
|
|
buckets = {}
|
|
for r in unwired:
|
|
k = ledger.get(r["path"], "NEW-UNWIRED")
|
|
buckets[k] = buckets.get(k, 0) + 1
|
|
print(" unwired, ledger-tolerated : %d (%s: %s)"
|
|
% (tol, os.path.basename(DEFAULT_BASELINE),
|
|
", ".join("%d %s" % (v, k) for k, v in sorted(buckets.items())) or "none"))
|
|
covered = sum(1 for r in rows if r["path"] in ledger)
|
|
no_census = [r["path"] for r in rows if r["path"] not in ledger]
|
|
unclassed = [p for p in no_census if p not in gate]
|
|
print(" census coverage : %d of %d committed verifier(s) carry a census row"
|
|
% (covered, len(rows)))
|
|
for p in no_census:
|
|
if p in gate:
|
|
print(" CENSUS_ROW_MISSING %s (no census row; a runner row (%s) still "
|
|
"classes it -- the coverage NUMBER drops, no fault)" % (p, gate[p]))
|
|
for p in unclassed:
|
|
print(" UNCLASSED %s (neither ledger names it)" % p)
|
|
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
|
|
|
|
|
|
BASELINE_HEAD = [
|
|
"# Q63 verifier census -- one row per COMMITTED verify_*.py at the rev the",
|
|
"# scan read, class plus the evidence the class rests on.",
|
|
"# row: <class> TAB <path> TAB <evidence> (three tab-separated columns)",
|
|
"# class gate-run = q65_runner.py executed it and recorded an rc (Q65);",
|
|
"# class wired-invoke = a committed line invokes it (the ref is the evidence);",
|
|
"# class declared-one-off = the file states in-file that no gate invokes it;",
|
|
"# class undeclared = unwired, no statement and no graded run (the Q65 residual).",
|
|
"# ARITHMETIC: the row count must equal the committed verifier count at that rev.",
|
|
"# This file used to list only the UNWIRED files, so a verifier that appeared in",
|
|
"# no row was invisible and both instruments still read clean -- 8 of 88 at",
|
|
"# `b01ec0e`. A census makes the omission itself the fault: q65_runner.py --check",
|
|
"# reports UNCLASSED for a committed verifier this file does not name.",
|
|
"# Regenerate: q63_verify_scan.py --repo . --emit-baseline"]
|
|
|
|
|
|
def _short(line, limit=96):
|
|
s = " ".join(line.split())
|
|
return s if len(s) <= limit else s[:limit - 3] + "..."
|
|
|
|
|
|
def emit_baseline(rows, path, gate=None, rev=None):
|
|
"""Write the census: one row per verifier the scan saw, with its evidence.
|
|
|
|
`rev` is written into the header as a short sha. A census is the class a
|
|
file held WHEN THE SCAN READ THE TREE; without the rev the same row set
|
|
reads as current forever, which is the one thing this archive does not
|
|
allow (Q63 reply: any closure must state its commit).
|
|
"""
|
|
gate = gate or {}
|
|
rev = rev or "unknown"
|
|
out = list(BASELINE_HEAD)
|
|
out.insert(2, "# rev: %s (the tree these classes were read at)" % rev)
|
|
for r in sorted(rows, key=lambda r: r["path"]):
|
|
if r["path"] in gate:
|
|
cls, ev = "gate-run", "q65:%s" % gate[r["path"]]
|
|
elif r["wired_refs"]:
|
|
cls, ev = "wired-invoke", _short(r["wired_refs"][0])
|
|
elif r["declared_one_off"]:
|
|
cls, ev = "declared-one-off", "in-file declaration"
|
|
else:
|
|
cls, ev = "undeclared", "no invocation, no declaration, no graded run"
|
|
out.append(chr(9).join((cls, r["path"], ev)))
|
|
open(path, "w", encoding="utf-8").write(chr(10).join(out) + chr(10))
|
|
tally = {}
|
|
for r in rows:
|
|
k = ("gate-run" if r["path"] in gate else "wired-invoke" if r["wired_refs"]
|
|
else "declared-one-off" if r["declared_one_off"] else "undeclared")
|
|
tally[k] = tally.get(k, 0) + 1
|
|
print("census written: %s (%d rows: %s)" % (
|
|
path, len(rows), ", ".join("%s %d" % (k, tally[k]) for k in
|
|
("gate-run", "wired-invoke", "declared-one-off",
|
|
"undeclared") if tally.get(k))))
|
|
return len(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))
|
|
|
|
# (5) Q65: a graded row in the runner ledger wires the file, no grep needed
|
|
gate = {"wizard-work/x/verify_orphan.py": "PASS"}
|
|
cells.append(("a graded gate-run row is not unwired",
|
|
len(grade(rows, led, gate)[1]) == 0))
|
|
# (6) a row whose verdict and rc disagree is not evidence of a run
|
|
with open(os.path.join(d, "gate.tsv"), "w") as fh:
|
|
fh.write("ungated\twizard-work/x/verify_orphan.py\tPASS\t1\t0.1\t\n")
|
|
parsed, ungraded = read_gate(os.path.join(d, "gate.tsv"))
|
|
cells.append(("PASS-with-rc-1 is not a graded row",
|
|
parsed == {} and "wizard-work/x/verify_orphan.py" in ungraded
|
|
and [r["path"] for r in grade(rows, led, parsed)[1]]
|
|
== ["wizard-work/x/verify_orphan.py"]))
|
|
|
|
# (7) prose is not an invocation. All four lines below are real shapes from
|
|
# the archive at `b01ec0e`, which the pre-fix scanner read as WIRED.
|
|
put("wizard-work/x/verify_prose.py", "import sys\nsys.exit(0)\n")
|
|
put("wizard-work/x/runner_docstring.py",
|
|
'"""Runner.\n\nRun as: python3 verify_prose.py\n"""\nprint("x")\n')
|
|
commit("c7")
|
|
rows = scan(d, "HEAD")
|
|
row = [r for r in rows if r["path"].endswith("verify_prose.py")][0]
|
|
cells.append(("a command quoted in a docstring wires nothing",
|
|
row["wired_refs"] == [] and row["mention_refs"] != []))
|
|
|
|
# (8) the same basename passed to subprocess.run() IS the invocation
|
|
put("wizard-work/x/verify_call.py", "import sys\nsys.exit(0)\n")
|
|
put("wizard-work/x/runner_call.py",
|
|
'import subprocess, sys\n'
|
|
'subprocess.run([sys.executable, "verify_call.py"], check=True)\n')
|
|
commit("c8")
|
|
rows = scan(d, "HEAD")
|
|
row = [r for r in rows if r["path"].endswith("verify_call.py")][0]
|
|
cells.append(("the basename passed to subprocess.run is an invocation",
|
|
len(row["wired_refs"]) == 1))
|
|
|
|
# (9) a report string in code, with no exec-shaped call on the line
|
|
put("wizard-work/x/verify_report.py", "import sys\nsys.exit(0)\n")
|
|
put("wizard-work/x/report_gen.py",
|
|
'A("`python3 verify_report.py .` runs 8 checks (A-H) and exits 0")\n')
|
|
commit("c9")
|
|
rows = scan(d, "HEAD")
|
|
row = [r for r in rows if r["path"].endswith("verify_report.py")][0]
|
|
cells.append(("a command quoted in a report string wires nothing",
|
|
row["wired_refs"] == []))
|
|
|
|
# (10) the interpreter token may not come from the REFERRER's filename:
|
|
# `extract_python_thing.py` + a prose mention read as "python ... X".
|
|
put("wizard-work/x/verify_pathtok.py", "import sys\nsys.exit(0)\n")
|
|
put("wizard-work/x/extract_python_thing.py",
|
|
'note = "the sibling verify_pathtok.py re-queries the API"\n')
|
|
commit("c10")
|
|
rows = scan(d, "HEAD")
|
|
row = [r for r in rows if r["path"].endswith("verify_pathtok.py")][0]
|
|
cells.append(("a token from the referrer's own path does not wire a file",
|
|
row["wired_refs"] == []))
|
|
|
|
# (11) Q150: a verifier committed at the repo ROOT is in the population.
|
|
# The regex required a slash, so this file was invisible to the scan
|
|
# while q65_runner counted it -- the disagreement read as an UNCLASSED
|
|
# fault no census row could clear. Both instruments now match on the
|
|
# basename, and the lane tally has a value for a path with no directory.
|
|
put("verify_root.py", "import sys\nsys.exit(1)\n")
|
|
commit("c11")
|
|
rows = scan(d, "HEAD")
|
|
roots = [r for r in rows if r["path"] == "verify_root.py"]
|
|
cells.append(("a repo-root verifier is in the population",
|
|
len(roots) == 1 and roots[0]["lane"] == "(root)"))
|
|
|
|
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("--gate", default=DEFAULT_GATE,
|
|
help="q65_runner ledger: rows with a graded rc count as run")
|
|
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:
|
|
gate, _ = read_gate(a.gate)
|
|
try:
|
|
sha = git(a.repo, "rev-parse", "--short", a.rev).strip() or a.rev
|
|
except RuntimeError:
|
|
sha = a.rev
|
|
emit_baseline(rows, a.baseline, gate, rev=sha)
|
|
return 0
|
|
gate, ungraded = read_gate(a.gate)
|
|
faults = report(rows, read_baseline(a.baseline), a.rev, a.verbose, gate, ungraded)
|
|
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())
|