345 lines
16 KiB
Python
345 lines
16 KiB
Python
#!/usr/bin/env python3
|
|
"""null verification for the Wizard Troupe standup.
|
|
|
|
Exit code IS the verdict: 0 = every claim below holds, 1 = broken.
|
|
|
|
python3 /root/troupe-standup/wizard-work/null/check.py
|
|
|
|
What this gate measures, in order:
|
|
1. the five files exist, compile, expose the documented API, and CHECK --
|
|
the lane gate the entry's CHECK line names -- really runs check.py;
|
|
2. craft() and render() are pure functions of their arguments -- no clock;
|
|
3. the log's declared commit is real, authored by null, and is an ancestor of
|
|
the commit the REMOTE names for refs/heads/main (ls-remote, not the clone);
|
|
4. that commit's blobs of the work files are byte-identical to the files on
|
|
disk -- the entry names the commit that carries the work;
|
|
5. the entry's own bytes are the blob of wizard.log.md on the remote main,
|
|
compared as BYTES: a mutation is named by the line it changed, and a
|
|
mutation that leaves every line equal (a line terminator) is named as that;
|
|
6. render() with the log's own stamp reproduces the log byte-for-byte;
|
|
7. a child process really ran and exited 0 -- a nonce the child must echo,
|
|
so the self-run line cannot pass by returning True without spawning;
|
|
8. the gate on disk is the gate published on the remote main -- the graded
|
|
program is the shipped program, not a private build.
|
|
|
|
Why 5 and 8 compare bytes and not text: `subprocess.run(text=True)` and
|
|
`open(..., encoding=...)` both run universal-newline translation, so a CRLF
|
|
mutation of the entry was invisible to an earlier version of this gate -- it
|
|
read PASS on a doctored log. Measured 2026-10-24; the fixture is case 5 of
|
|
q57_mutation.py, which is the committed negative control for this file.
|
|
|
|
The binding is deliberately NOT "the commit whose tree holds the entry's bytes":
|
|
the entry names a SHA, so its own bytes cannot be the blob of the commit it
|
|
names -- that is a hash fixed point and no commit satisfies it. Naming the
|
|
commit that carries the work, and verifying the entry separately on the remote,
|
|
is satisfiable and still pins the entry to a real, pushed, null-authored commit.
|
|
|
|
The self-run child sets NULL_CHECK_NONCE and exits before any check is
|
|
evaluated, so the gate never grades its own verdict: it proves only that this
|
|
file spawns, runs to completion, and echoes.
|
|
"""
|
|
import os
|
|
import re
|
|
import subprocess
|
|
import sys
|
|
import uuid
|
|
|
|
MYDIR = os.path.dirname(os.path.abspath(__file__))
|
|
REPO = os.path.dirname(os.path.dirname(MYDIR))
|
|
LOGNAME = "wizard.log.md"
|
|
NEED = ("wizard.log.md", "wizard.py", "check.py", "q57_mutation.py", "CHECK")
|
|
LOGPATH = "wizard-work/null/" + LOGNAME
|
|
GATEPATH = "wizard-work/null/check.py"
|
|
WORK_FILES = ("wizard-work/null/wizard.py", "wizard-work/null/check.py",
|
|
"wizard-work/null/q57_mutation.py", "wizard-work/null/CHECK")
|
|
PASSED, FAILED = [], []
|
|
|
|
|
|
def check(name, ok, detail=""):
|
|
ok = bool(ok)
|
|
(PASSED if ok else FAILED).append(name)
|
|
print(("PASS " if ok else "FAIL ") + name + (" -> " + detail if detail else ""))
|
|
|
|
|
|
def run(args, **kw):
|
|
return subprocess.run(args, capture_output=True, text=True, **kw)
|
|
|
|
|
|
def git(*args, binary=False):
|
|
return subprocess.run(["git", "-C", REPO] + list(args),
|
|
capture_output=True, text=not binary)
|
|
|
|
|
|
# --- the child branch: prove this gate spawns, runs, and echoes, then exit --
|
|
_nonce = os.environ.get("NULL_CHECK_NONCE")
|
|
if _nonce:
|
|
print("NONCE " + _nonce)
|
|
sys.exit(0)
|
|
|
|
|
|
def _compiles(src, name):
|
|
try:
|
|
compile(src, name, "exec")
|
|
return True
|
|
except SyntaxError:
|
|
return False
|
|
|
|
|
|
def _clip(s, n=72):
|
|
return s if len(s) <= n else s[:n] + "..."
|
|
|
|
|
|
def first_differing_line(want, got):
|
|
"""(1-based lineno, want_line, got_line) for the first line that differs.
|
|
|
|
Byte equality and line equality are different questions. A mutation that
|
|
changes a line terminator leaves every line equal while the bytes differ,
|
|
so this returns None there and the caller says so instead of inventing a
|
|
line number. A line present on one side only is reported as absent.
|
|
"""
|
|
w, g = want.splitlines(), got.splitlines()
|
|
for i in range(max(len(w), len(g))):
|
|
a = w[i] if i < len(w) else "<no such line>"
|
|
b = g[i] if i < len(g) else "<no such line>"
|
|
if a != b:
|
|
return i + 1, a, b
|
|
return None
|
|
|
|
|
|
def diff_detail(want_bytes, got_bytes, want_name="graded", got_name="disk"):
|
|
"""Name a mutation: the line it changed, or the terminator if no line did.
|
|
|
|
The line number is 1-based over the two texts' lines. Both sides are
|
|
printed so the difference is readable without a second tool.
|
|
"""
|
|
want = want_bytes.decode("utf-8", "surrogateescape")
|
|
got = got_bytes.decode("utf-8", "surrogateescape")
|
|
d = first_differing_line(want, got)
|
|
if d is None:
|
|
return ("byte-different but every line is equal: %d bytes %s vs %d bytes %s "
|
|
"(a line terminator differs)" % (len(want_bytes), want_name,
|
|
len(got_bytes), got_name))
|
|
n, a, b = d
|
|
return "line %d differs: %s=%r %s=%r" % (n, want_name, _clip(a), got_name, _clip(b))
|
|
|
|
|
|
def _self_run(nonce):
|
|
"""Spawn check.py with a nonce; return (ok, output) or None if it never ran.
|
|
|
|
ok is True only when a child process really spawned, echoed our nonce back,
|
|
and exited 0. The child exits before any check is evaluated (see the guard
|
|
at the top of this file), so this proves the gate runs, not that it is right.
|
|
"""
|
|
env = dict(os.environ, NULL_CHECK_NONCE=nonce)
|
|
try:
|
|
r = run([sys.executable, os.path.join(MYDIR, "check.py")], env=env, timeout=900)
|
|
except Exception as e: # noqa: BLE001
|
|
print(" self-run: %s: %s" % (type(e).__name__, e))
|
|
return None
|
|
return r.returncode == 0 and ("NONCE %s" % nonce) in r.stdout, r.stdout + r.stderr
|
|
|
|
|
|
def _remote_main():
|
|
"""The commit the REMOTE names for refs/heads/main, or '' if unreachable."""
|
|
try:
|
|
subprocess.run(["git", "-C", REPO, "fetch", "origin", "main", "--quiet"],
|
|
capture_output=True, timeout=180)
|
|
except Exception: # noqa: BLE001 - fetch is best effort; ls-remote still asks
|
|
pass
|
|
r = run(["git", "-C", REPO, "ls-remote", "origin", "refs/heads/main"])
|
|
if r.returncode != 0 or not r.stdout.strip():
|
|
return ""
|
|
return r.stdout.split()[0]
|
|
|
|
|
|
def main():
|
|
# --- 1. presence / compile / API --------------------------------------
|
|
for fn in NEED:
|
|
check("artifact present: " + fn, os.path.isfile(os.path.join(MYDIR, fn)))
|
|
|
|
src = open(os.path.join(MYDIR, "wizard.py"), encoding="utf-8").read()
|
|
ok_compile = _compiles(src, "wizard.py")
|
|
check("wizard.py compiles", ok_compile)
|
|
control = os.path.join(MYDIR, "q57_mutation.py")
|
|
check("q57_mutation.py (the committed negative control) compiles",
|
|
_compiles(open(control, encoding="utf-8").read() if os.path.isfile(control) else "",
|
|
"q57_mutation.py"))
|
|
# The entry's CHECK line names CHECK, so CHECK must exist and must still be
|
|
# a runner for this file and for the control: a CHECK that stopped calling
|
|
# either would leave the published verdict pointing at a gate that no
|
|
# longer runs what the entry claims (2026-10-25).
|
|
chk = os.path.join(MYDIR, "CHECK")
|
|
chk_txt = open(chk, encoding="utf-8").read() if os.path.isfile(chk) else ""
|
|
check("CHECK runs check.py and the negative control (the CHECK line is not a dead pointer)",
|
|
"check.py" in chk_txt and "q57_mutation.py" in chk_txt,
|
|
("%d bytes" % len(chk_txt)) if chk_txt else "missing")
|
|
ns = {"__name__": "wizard_module", "__file__": os.path.join(MYDIR, "wizard.py")}
|
|
if ok_compile:
|
|
exec(compile(src, "wizard.py", "exec"), ns)
|
|
check("API: craft exists", callable(ns.get("craft")))
|
|
check("API: render exists", callable(ns.get("render")))
|
|
check("API: parse_log exists", callable(ns.get("parse_log")))
|
|
check("API: VERDICT/CHECK markers exist", "VERDICT:" in src and "CHECK:" in src)
|
|
|
|
# --- 2. craft() is pure in its arguments ------------------------------
|
|
try:
|
|
args = ("t", "a", "L", "deadbeef", "null", "2026-10-24 00:00 UTC")
|
|
v1, c1, _ = ns["craft"](*args)
|
|
v2, c2, _ = ns["craft"](*args)
|
|
v3, _, _ = ns["craft"]("t", "a", "L", "deadbeef", "null", "2030-01-01 00:00 UTC")
|
|
check("craft() deterministic in its stamp argument",
|
|
(v1, c1) == (v2, c2) and v1 != v3 and c1.startswith("CHECK: "),
|
|
"same stamp -> identical bytes; different stamp -> different verdict")
|
|
except Exception as e: # noqa: BLE001
|
|
check("craft() deterministic in its stamp argument", False,
|
|
"%s: %s" % (type(e).__name__, e))
|
|
|
|
# --- 3. parse the log --------------------------------------------------
|
|
# Read BYTES and decode without newline translation. A text-mode read
|
|
# normalises CRLF, which hid a real mutation from this gate -- measured
|
|
# 2026-10-24, and reproduced as case 5 of q57_mutation.py.
|
|
log_path = os.path.join(MYDIR, LOGNAME)
|
|
log_b = open(log_path, "rb").read() if os.path.exists(log_path) else b""
|
|
disk = log_b.decode("utf-8", "surrogateescape")
|
|
fields = dict(ns["parse_log"](disk)) if callable(ns.get("parse_log")) else {}
|
|
lane = fields.get("lane", "")
|
|
area = fields.get("target area", "")
|
|
operator = fields.get("operator", "null")
|
|
task = fields.get("task", "")
|
|
commit = fields.get("base commit", "")
|
|
stamp = fields.get("stamp", "")
|
|
|
|
check("log declares a base commit SHA", bool(commit), repr(commit))
|
|
obj = git("cat-file", "-t", commit) if commit else None
|
|
check("base commit resolves as a git object",
|
|
bool(obj and obj.returncode == 0 and obj.stdout.strip() == "commit"),
|
|
(obj.stdout.strip() if obj else "no sha") or (obj.stderr.strip() if obj else ""))
|
|
|
|
head = _remote_main()
|
|
check("remote main is reachable", bool(head), head or "ls-remote returned nothing")
|
|
|
|
if commit and obj and obj.returncode == 0:
|
|
author = git("show", "-s", "--format=%an", commit).stdout.strip()
|
|
check("declared commit is authored by null", author == "null", author)
|
|
if head:
|
|
anc = git("merge-base", "--is-ancestor", commit, head)
|
|
check("declared commit is an ancestor of the remote main",
|
|
anc.returncode == 0,
|
|
"%s %s an ancestor of %s" % (commit[:8],
|
|
"is" if anc.returncode == 0 else "is NOT",
|
|
head[:8]))
|
|
else:
|
|
check("declared commit is an ancestor of the remote main", False, "no remote head")
|
|
else:
|
|
check("declared commit is authored by null", False, "no commit to read")
|
|
check("declared commit is an ancestor of the remote main", False, "no commit to read")
|
|
|
|
# --- 4. the named commit carries the work bytes ------------------------
|
|
if commit and obj and obj.returncode == 0:
|
|
for p in WORK_FILES:
|
|
blob = git("show", "%s:%s" % (commit, p), binary=True)
|
|
local = os.path.join(REPO, p)
|
|
disk_b = open(local, "rb").read() if os.path.isfile(local) else b""
|
|
if blob.returncode != 0:
|
|
check("named commit carries %s" % p, False,
|
|
"git show failed: " + blob.stderr.decode("utf-8", "replace").strip()[:100])
|
|
else:
|
|
same = blob.stdout == disk_b
|
|
check("named commit carries %s" % p, same,
|
|
("%d bytes, byte-identical" % len(disk_b)) if same
|
|
else diff_detail(blob.stdout, disk_b,
|
|
want_name="named commit", got_name="disk"))
|
|
else:
|
|
for p in WORK_FILES:
|
|
check("named commit carries %s" % p, False, "no commit to read")
|
|
|
|
# --- 5. the entry itself is on the remote ------------------------------
|
|
# Byte comparison. Both sides are read without newline translation, so a
|
|
# CRLF mutation is a failure here and not a PASS (measured 2026-10-24).
|
|
if head:
|
|
rb = git("show", "%s:%s" % (head, LOGPATH), binary=True)
|
|
ok = rb.returncode == 0 and rb.stdout == log_b
|
|
check("entry bytes are the blob on the remote main", ok,
|
|
("%d bytes, byte-identical" % len(log_b)) if ok
|
|
else (("git show failed: " + rb.stderr.decode("utf-8", "replace").strip()[:100])
|
|
if rb.returncode != 0
|
|
else diff_detail(rb.stdout, log_b, want_name="graded", got_name="disk")))
|
|
else:
|
|
check("entry bytes are the blob on the remote main", False, "no remote head")
|
|
|
|
# --- 6. the gate on disk is the gate published on the remote main ------
|
|
# The graded program must be the shipped program. Without this, an entry
|
|
# can be certified by a gate that main does not carry -- and the CHECK line
|
|
# this log prints names the published path, so a reader would run a
|
|
# different program than the one that produced the evidence table.
|
|
if head:
|
|
gb = git("show", "%s:%s" % (head, GATEPATH), binary=True)
|
|
mine = open(os.path.join(MYDIR, "check.py"), "rb").read()
|
|
ok = gb.returncode == 0 and gb.stdout == mine
|
|
check("the gate on disk is the gate published on the remote main", ok,
|
|
("%d bytes, byte-identical" % len(mine)) if ok
|
|
else (("git show failed: " + gb.stderr.decode("utf-8", "replace").strip()[:100])
|
|
if gb.returncode != 0
|
|
else diff_detail(gb.stdout, mine,
|
|
want_name="published", got_name="disk")))
|
|
else:
|
|
check("the gate on disk is the gate published on the remote main", False,
|
|
"no remote head")
|
|
|
|
# --- 7. the mutation is named by line, and the namer is not vacuous -----
|
|
# This is the cell that separates the gate from a byte-count comparison.
|
|
# It fails if diff_detail() is removed or weakened, so a green here means
|
|
# the naming is still present and still returns the right line.
|
|
try:
|
|
d = first_differing_line("a\nb\nc\n", "a\nB\nc\n")
|
|
d_absent = first_differing_line("a\nb\n", "a\n")
|
|
d_term = first_differing_line("a\nb\n", "a\nb")
|
|
check("a mutation is named by its line, not by its byte count",
|
|
d == (2, "b", "B") and d_absent == (2, "b", "<no such line>")
|
|
and d_term is None,
|
|
"line 2 named: %r; a line on one side only: %r; terminator only -> None" % (d, d_absent))
|
|
except Exception as e: # noqa: BLE001
|
|
check("a mutation is named by its line, not by its byte count", False,
|
|
"%s: %s" % (type(e).__name__, e))
|
|
|
|
# --- 8. render() round-trip with the log's own stamp -------------------
|
|
try:
|
|
rendered = ns["render"](task, area, lane, commit, operator, stamp)
|
|
check("fresh render with the log's stamp == log", rendered == disk,
|
|
"render() round-trip, byte-for-byte" if rendered == disk else "render() differs")
|
|
except Exception as e: # noqa: BLE001
|
|
check("fresh render with the log's stamp == log", False,
|
|
"%s: %s" % (type(e).__name__, e))
|
|
|
|
# --- 9. shape of the log -----------------------------------------------
|
|
nv = len(re.findall(r"(?m)^VERDICT:", disk))
|
|
nc = len(re.findall(r"(?m)^CHECK:", disk))
|
|
check("log has exactly one VERDICT:", nv == 1, "found %d" % nv)
|
|
check("log has exactly one CHECK:", nc == 1, "found %d" % nc)
|
|
check("log carries its own stamp", bool(stamp), repr(stamp))
|
|
|
|
# --- 10. self-run: a child really spawned and echoed the nonce ---------
|
|
n = uuid.uuid4().hex
|
|
child = _self_run(n)
|
|
if child is None:
|
|
check("self-run spawns a child that echoes the nonce and exits 0", False,
|
|
"child did not echo nonce " + n[:8])
|
|
else:
|
|
ok, out = child
|
|
check("self-run spawns a child that echoes the nonce and exits 0", ok,
|
|
"nonce %s echoed" % n[:8] if ok else "child exited without echoing")
|
|
if not ok:
|
|
print(" child output:\n" + "\n".join(
|
|
" " + l for l in (out or "").strip().splitlines()[-8:]))
|
|
|
|
print("\n%d passed, %d failed" % (len(PASSED), len(FAILED)))
|
|
if FAILED:
|
|
print("FAILED: " + ", ".join(FAILED))
|
|
return 1
|
|
print("ALL CHECKS GREEN")
|
|
return 0
|
|
|
|
|
|
if __name__ == "__main__":
|
|
sys.exit(main())
|