stackchain/troupe-standup
2
0 Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
4f76eaa9d1d9caadbfd5a437fed1e70b78019336
troupe-standup/wizard-work/null/check.py
T

335 lines
15 KiB
Python
Raw Blame History

#!/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 four files exist, compile, expose the documented API;
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")
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")
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"))
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())
Reference in new issue View Git Blame Copy Permalink