jakman85andClaude Opus 5
fa4deac877
One historical `-dirty` row reddened this gate permanently, even after a clean re-run of the same test. status.py already resolves duplicates latest-wins (latest_by_test), so a superseded row is not evidence of anything — but this check iterated every row, so the poisoned row from the git_sha bug (fixed in the parent commit) would have failed the audit forever. The dirty-tree assertion is now scoped to rows status.py would actually honour, by importing latest_by_test rather than reimplementing the rule, so the two cannot disagree about which rows are live claims. Structural assertions — provenance keys, sentinel, test-still-exists — still apply to EVERY row. Nothing is erased: the row stays in the ledger and runs/20260913T014437Z-19fc8bc/ run.log stays committed. It simply stops being read as a live claim. Verified the guard is intact afterwards — the check still REFUSES both forgeries it is built to catch (a self-skip presented as a pass, and a proven row from the root commit). A dirty-then-clean sequence is also the normal shape of noticing a dirty tree, fixing it, and re-running; that should not permanently fail an audit. Co-Authored-By: Claude Opus 5 <[email protected]>
455 lines
27 KiB
Bash
Executable File
455 lines
27 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# =============================================================================
|
|
# L0 static check (offline, no cluster) — auditability-proofs-producible
|
|
# Serves: R-SEC-03 ("All the above properties MUST be demonstrable/auditable (an operator can
|
|
# prove isolation, egress path, cert validity, and backup integrity)."
|
|
# — spec docs/00-vision-and-scope.md).
|
|
#
|
|
# The spec makes this meta-requirement concrete. docs/07-security-and-secrets.md
|
|
# §"Auditability requirements (R-SEC-03) — what an operator must be able to prove":
|
|
# - **Isolation**: "service X cannot reach service Y" — via Hubble flow logs + a
|
|
# denied-probe test.
|
|
# - **Egress path**: "service X's public IP is the VPN's" — via an egress IP check.
|
|
# - **Kill-switch**: "with VPN down, X leaks nothing" — via a fault-injection test.
|
|
# - **TLS**: "every endpoint serves a valid, non-self-signed, unexpired cert" — via cert
|
|
# status + external check.
|
|
# - **Backups**: "irreplaceable data is restorable" — via a DR drill.
|
|
# "These proofs are part of the platform acceptance suite, not one-time checks."
|
|
# and its acceptance gate: "The five auditability proofs above can be produced on demand."
|
|
#
|
|
# HOW A META-REQUIREMENT IS TESTED WITHOUT BECOMING A TAUTOLOGY
|
|
# ------------------------------------------------------------
|
|
# The trap is obvious and this check is built to avoid it: "a test exists for R-NET-01,
|
|
# therefore isolation is auditable" is true of any suite that compiles, proves nothing, and
|
|
# would keep passing while every proof rotted into a scaffold. Four separate failure modes
|
|
# have to be caught for "an operator can PROVE it" to mean anything, and each one is asserted
|
|
# by DRIVING the real machinery rather than by reading files:
|
|
#
|
|
# (a) THE PROOF EXISTS, AT THE RIGHT STRENGTH. Each of the five named proofs maps to a
|
|
# requirement that must have an EXECUTABLE verifying test — not a placeholder scaffold — and,
|
|
# where the spec's own words name fault injection ("with VPN down"; "a DR drill"), an
|
|
# executable L3 test specifically. Executable-vs-scaffold is not re-derived here: this
|
|
# check RUNS lib/status.py and reads its verdict, so it cannot disagree with the
|
|
# repository's own status report.
|
|
# (b) THE PROOF IS PRODUCIBLE ON DEMAND, BY THE DOCUMENTED COMMAND. `run.sh
|
|
# --requirements <the five IDs>` must resolve to a non-empty test set and must ASSERT
|
|
# their coverage (that flag is the merge gate's own path: it passes --require to
|
|
# coverage.py). This check drives run.sh itself, so if the resolver, the labels or the
|
|
# gate wiring break, R-SEC-03 fails.
|
|
# (c) THE PROOF IS CAPTURABLE. A test that passes but records nothing leaves an operator
|
|
# with a green terminal and no evidence. For each Chainsaw-layer proof, the test must
|
|
# declare a PASS SENTINEL that lib/record_run.py can actually attribute — computed with
|
|
# record_run.py's OWN parser, so deleting a test's sentinel makes this check fail
|
|
# instead of silently making the requirement unprovable.
|
|
# (d) THE EVIDENCE CANNOT BE FORGED, AND IS NOT HONOURED WHEN STALE. This is the clause
|
|
# that makes the check bite. Two INDEPENDENT forgery attempts are mounted against the
|
|
# real tools, in a throwaway directory:
|
|
# * a Chainsaw run in which the JUnit says a real proof test PASSED while the run log
|
|
# carries only that test's SKIP token — the exact shape of a self-skipping L2/L3
|
|
# test. record_run.py must refuse to call it `proven`.
|
|
# * a ledger row claiming `proven` at a commit that PREDATES the requirement's
|
|
# implementing code — status.py must degrade it to `stale-proof`, never green.
|
|
# Both tools' own built-in self-tests (`--selftest`) are also driven, because nothing
|
|
# in ci/ or run.sh runs them today: the guards that keep a skip from becoming a proof
|
|
# were themselves unexercised in the merge gate until this check.
|
|
#
|
|
# The FIVE PROOFS ARE NOT HAND-LISTED where the spec can be read: when the read-only spec
|
|
# repo is mounted, the bullet labels are parsed out of docs/07 and must match this check's
|
|
# mapping EXACTLY. Add a sixth proof to the spec and this check fails as unmapped rather
|
|
# than quietly ignoring it.
|
|
#
|
|
# WHY L0: every clause above is a property of the repository and its own tooling, provable
|
|
# offline, and it belongs in the merge gate — the point of an audit chain is that it is intact
|
|
# BEFORE anyone needs it. Nothing here needs a cluster, and nothing here would be more true
|
|
# with one.
|
|
#
|
|
# WHAT THIS DOES *NOT* PROVE (honest gaps — do not read this check as claiming them):
|
|
# - THAT THE FIVE PROOFS PASS. This asserts the proofs are present, strong, runnable by one
|
|
# documented command, capturable as evidence, and that the evidence chain refuses
|
|
# forgeries. Whether isolation actually holds today is R-NET-01's test; whether the DR
|
|
# restore works is R-STATE-03's. R-SEC-03 is about the operator's ABILITY to produce the
|
|
# proof, which is what is asserted.
|
|
# - HUBBLE. docs/07 names "Hubble flow logs" as part of the isolation proof. No test in this
|
|
# suite queries Hubble, and this check does not pretend otherwise: it asserts the
|
|
# denied-probe half, which is the half that is automated. The Hubble half remains an
|
|
# operator-interactive capability — a real, named gap in R-SEC-03's coverage.
|
|
# - THE OPERATOR-FACING NARRATIVE. That a human can find and read the evidence (the status
|
|
# report's prose, the ledger's provenance fields) is a usability property, not a testable
|
|
# one.
|
|
# - LEDGER COMPLETENESS OVER TIME. The ledger is append-only by convention and by review;
|
|
# nothing here can prove a row was never removed from it (that would need signed history).
|
|
# - THAT THE PROOFS COVER "ALL THE ABOVE PROPERTIES". R-SEC-03's own wording is broader than
|
|
# the five bullets docs/07 enumerates. The five are what the spec made concrete and are
|
|
# what is asserted; suite-wide coverage of every requirement is R-TEST-01/04's claim,
|
|
# tested by tests/meta/harness-selfcheck, and is deliberately NOT re-asserted here.
|
|
# =============================================================================
|
|
set -euo pipefail
|
|
DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
|
ROOT="$(cd "${DIR}/../../../.." && pwd)" # repo root
|
|
PYTHON="${PYTHON:-python3}"
|
|
: "${SPEC_REPO:=${ROOT}/../home-network-k3s}"
|
|
export SPEC_REPO
|
|
|
|
cd "${ROOT}"
|
|
"${PYTHON}" - "${ROOT}" <<'PY'
|
|
import json
|
|
import os
|
|
import re
|
|
import shutil
|
|
import subprocess
|
|
import sys
|
|
import tempfile
|
|
from pathlib import Path
|
|
|
|
ROOT = Path(sys.argv[1])
|
|
CONF = ROOT / "conformance"
|
|
LIB = CONF / "lib"
|
|
FAILURES: list[str] = []
|
|
NOTES: list[str] = []
|
|
CHECKS = 0
|
|
|
|
|
|
def check(cond, msg):
|
|
global CHECKS
|
|
CHECKS += 1
|
|
if not cond:
|
|
FAILURES.append(msg)
|
|
|
|
|
|
def note(msg):
|
|
NOTES.append(msg)
|
|
|
|
|
|
def die():
|
|
print(f"CHECK FAIL (auditability-proofs-producible): {len(FAILURES)} of {CHECKS} "
|
|
"assertions failed", file=sys.stderr)
|
|
for f in FAILURES:
|
|
print(f" - {f}", file=sys.stderr)
|
|
raise SystemExit(1)
|
|
|
|
|
|
def run(cmd, **kw) -> subprocess.CompletedProcess:
|
|
return subprocess.run(cmd, capture_output=True, text=True, cwd=kw.pop("cwd", CONF), **kw)
|
|
|
|
|
|
# ================================================= THE FIVE PROOFS docs/07 ENUMERATES
|
|
# key = the bullet label docs/07 uses (verified against the spec below when it is mounted)
|
|
# reqs = the requirement(s) whose verifying test IS that proof
|
|
# layer= the WEAKEST layer the spec's own words allow. Where docs/07 says "a fault-injection
|
|
# test" / "a DR drill", an L2 happy-path test does not discharge the proof.
|
|
PROOFS = {
|
|
"Isolation": {"reqs": ["R-NET-01"], "layers": {"L2", "L3"},
|
|
"why": '"service X cannot reach service Y" — via Hubble flow logs + a '
|
|
"denied-probe test"},
|
|
"Egress path": {"reqs": ["R-NET-05"], "layers": {"L2", "L3"},
|
|
"why": '"service X\'s public IP is the VPN\'s" — via an egress IP check'},
|
|
"Kill-switch": {"reqs": ["R-NET-06"], "layers": {"L3"},
|
|
"why": '"with VPN down, X leaks nothing" — via a fault-injection test'},
|
|
"TLS": {"reqs": ["R-TLS-01"], "layers": {"L2", "L3"},
|
|
"why": '"every endpoint serves a valid, non-self-signed, unexpired cert" '
|
|
"— via cert status + external check"},
|
|
"Backups": {"reqs": ["R-STATE-03"], "layers": {"L3"},
|
|
"why": '"irreplaceable data is restorable" — via a DR drill'},
|
|
}
|
|
PROOF_REQS = sorted({r for p in PROOFS.values() for r in p["reqs"]})
|
|
|
|
# ---- SELF-POLICING: the proof list must still be the SPEC's proof list ---------------
|
|
spec = Path(os.environ.get("SPEC_REPO", ""))
|
|
sec_doc = spec / "docs" / "07-security-and-secrets.md"
|
|
if sec_doc.is_file():
|
|
text = sec_doc.read_text()
|
|
m = re.search(r"^##\s+Auditability requirements \(R-SEC-03\).*?$(.*?)^##\s", text,
|
|
re.M | re.S)
|
|
check(m is not None,
|
|
"docs/07 no longer carries an '## Auditability requirements (R-SEC-03)' section — "
|
|
"the proof list this check is coupled to has moved or been removed, so the mapping "
|
|
"below can no longer be trusted (R-TEST-06: follow the spec, never the other way)")
|
|
if m:
|
|
labels = re.findall(r"^\s*-\s+\*\*([^*]+)\*\*:", m.group(1), re.M)
|
|
check(set(labels) == set(PROOFS),
|
|
f"docs/07 enumerates the auditability proofs {sorted(labels)} but this check "
|
|
f"maps {sorted(PROOFS)} — every proof the spec names must map to a verifying "
|
|
"test, and a proof this check does not know about would be silently unverified")
|
|
check(len(labels) == 5,
|
|
f"docs/07 enumerates {len(labels)} auditability proof(s); its own acceptance "
|
|
"gate says 'The five auditability proofs above can be produced on demand' — the "
|
|
"prose and the list have drifted apart")
|
|
else:
|
|
note(f"the read-only spec repo is not mounted at {spec} — the proof list could not be "
|
|
"re-derived from docs/07, so the mapping below was used as written. Every other "
|
|
"assertion still ran. (ci/l0.sh mounts the spec; a bare local run may not.)")
|
|
|
|
# ============================================ (a) EACH PROOF EXISTS, AT THE RIGHT STRENGTH
|
|
# Driven through lib/status.py so this check and the repository's own status report cannot
|
|
# disagree about what is executable and what is a scaffold.
|
|
tmp = Path(tempfile.mkdtemp(prefix="r-sec-03-"))
|
|
try:
|
|
out = tmp / "status"
|
|
st = run([sys.executable, str(LIB / "status.py"), "--repo", str(ROOT),
|
|
"--registry", str(CONF / "requirements" / "registry.yaml"),
|
|
"--tests", str(CONF / "tests"), "--out", str(out)])
|
|
check(st.returncode == 0,
|
|
f"lib/status.py exited {st.returncode} — the report an operator would use to find "
|
|
f"the audit evidence does not generate: {(st.stderr or st.stdout).strip()[:400]}")
|
|
status = {}
|
|
sj = out / "status.json"
|
|
if sj.is_file():
|
|
status = json.loads(sj.read_text())
|
|
check(bool(status.get("by_requirement")),
|
|
"lib/status.py produced no per-requirement report — the audit posture of each "
|
|
"requirement is not derivable, so R-SEC-03 cannot be assessed at all")
|
|
by_req = status.get("by_requirement", {})
|
|
|
|
for label, spec_proof in sorted(PROOFS.items()):
|
|
for rid in spec_proof["reqs"]:
|
|
rec = by_req.get(rid)
|
|
check(rec is not None,
|
|
f"proof '{label}' maps to {rid}, which the status report does not know — "
|
|
"either the registry lost the requirement or this mapping is stale")
|
|
if not rec:
|
|
continue
|
|
tests = (rec.get("verification") or {}).get("tests") or []
|
|
executable = [t for t in tests if t.get("state", "").startswith("executable")]
|
|
check(bool(executable),
|
|
f"proof '{label}' ({rid}) has no EXECUTABLE verifying test — its tests are "
|
|
f"{[t.get('name') + ':' + t.get('state', '?') for t in tests]}. docs/07: "
|
|
f"{spec_proof['why']}. A placeholder scaffold cannot be produced on demand, so the "
|
|
"operator cannot prove this property")
|
|
at_layer = [t for t in executable if t.get("layer") in spec_proof["layers"]]
|
|
check(bool(at_layer),
|
|
f"proof '{label}' ({rid}) has no executable test at layer(s) "
|
|
f"{sorted(spec_proof['layers'])} — it has "
|
|
f"{[t.get('name') + '@' + str(t.get('layer')) for t in executable]}. "
|
|
f"docs/07 requires this proof to be produced {spec_proof['why']}, and a "
|
|
"weaker layer does not discharge it (a rendering check is not a drill)")
|
|
|
|
# ==================================== (b) PRODUCIBLE ON DEMAND, BY THE DOCUMENTED COMMAND
|
|
# The resolver: --requirements must translate the five R-IDs into real test dirs.
|
|
resolver = run(["bash", "-c",
|
|
f'export CONF_ROOT="{CONF}"; . "{LIB}/common.sh"; '
|
|
f'conf_dirs_for_requirements "{" ".join(PROOF_REQS)}"'])
|
|
dirs = [l for l in resolver.stdout.splitlines() if l.strip()]
|
|
check(resolver.returncode == 0 and len(dirs) >= len(PROOF_REQS),
|
|
f"`run.sh --requirements {','.join(PROOF_REQS)}` resolves to {len(dirs)} test dir(s) "
|
|
f"for {len(PROOF_REQS)} proof requirement(s) — the single command docs/07's "
|
|
"acceptance gate depends on ('produced on demand') cannot select the proofs")
|
|
|
|
# The gate: the same flag ASSERTS coverage (run.sh passes --require to coverage.py), so a
|
|
# zero exit here is the repository's own statement that all five proofs are covered.
|
|
gate = run(["./run.sh", "--coverage-only", "--requirements", ",".join(PROOF_REQS)])
|
|
check(gate.returncode == 0,
|
|
f"`./run.sh --coverage-only --requirements {','.join(PROOF_REQS)}` exited "
|
|
f"{gate.returncode} — the merge gate's own coverage assertion rejects the audit "
|
|
f"proof set: {(gate.stderr or gate.stdout).strip()[:400]}")
|
|
|
|
# ================================================ (c) THE PROOF IS CAPTURABLE AS EVIDENCE
|
|
# Use record_run.py's OWN sentinel parser: a Chainsaw-layer proof with no declared pass
|
|
# token can pass forever and never be recorded as proof of anything.
|
|
sys.path.insert(0, str(LIB))
|
|
os.environ.setdefault("PYTHONDONTWRITEBYTECODE", "1")
|
|
sys.dont_write_bytecode = True
|
|
import record_run as rr # noqa: E402
|
|
|
|
# status.py owns the latest-wins rule; import it rather than reimplementing it, so the two
|
|
# cannot disagree about which rows are live evidence.
|
|
import status as _st # noqa: E402
|
|
rr_latest_by_test = _st.latest_by_test
|
|
|
|
smap = rr.sentinel_map(CONF / "tests")
|
|
check(len(smap) >= 10,
|
|
f"record_run.py's sentinel map contains {len(smap)} test(s) — the parser lost its "
|
|
"grip on the test tree, so the assertions below would assert nothing")
|
|
for label, spec_proof in sorted(PROOFS.items()):
|
|
for rid in spec_proof["reqs"]:
|
|
rec = by_req.get(rid) or {}
|
|
tests = (rec.get("verification") or {}).get("tests") or []
|
|
names = [t.get("name") for t in tests
|
|
if t.get("state", "").startswith("executable")
|
|
and t.get("layer") in spec_proof["layers"]]
|
|
for name in names:
|
|
ent = smap.get(name)
|
|
check(ent is not None,
|
|
f"proof '{label}': record_run.py does not know the test {name!r} — its "
|
|
"result could never be attributed to a ledger row")
|
|
if not ent:
|
|
continue
|
|
if ent.get("layer") in rr.SENTINEL_EXEMPT_LAYERS:
|
|
continue # offline layers are truthful by JUnit alone
|
|
check(bool(ent.get("pass")),
|
|
f"proof '{label}': the Chainsaw test {name!r} declares NO pass sentinel, "
|
|
"so lib/record_run.py can never record it as proven. It would go green "
|
|
"in the terminal and leave the operator with no evidence — exactly the "
|
|
"gap the ledger exists to close (docs/07: the proofs are 'part of the "
|
|
"platform acceptance suite, not one-time checks')")
|
|
check(bool(ent.get("terminal_pass")),
|
|
f"proof '{label}': the test {name!r} has no TERMINAL pass token, so "
|
|
"record_run.py cannot decide its verdict")
|
|
|
|
# =============================== (d) THE EVIDENCE CANNOT BE FORGED, NOR HONOURED WHEN STALE
|
|
# Both tools' own guards, which NOTHING in ci/ or run.sh drives today.
|
|
for tool in ("record_run.py", "status.py"):
|
|
r = run([sys.executable, str(LIB / tool), "--selftest"])
|
|
check(r.returncode == 0,
|
|
f"`lib/{tool} --selftest` exited {r.returncode} — the guards that keep a "
|
|
"self-skipped or stale run from being recorded as proof are broken, so nothing "
|
|
f"in the evidence chain can be trusted: {(r.stderr or r.stdout).strip()[:500]}")
|
|
|
|
# ---- FORGERY 1: a green JUnit for a REAL proof test whose log holds only a SKIP token.
|
|
# This is the precise shape of a self-skipping L2/L3 test, and it must NOT become proof.
|
|
forge_target, forge_skip = None, None
|
|
for label, spec_proof in sorted(PROOFS.items()):
|
|
for rid in spec_proof["reqs"]:
|
|
for name, ent in smap.items():
|
|
if rid in (ent.get("requirements") or []) and ent.get("skip") \
|
|
and ent.get("layer") not in rr.SENTINEL_EXEMPT_LAYERS:
|
|
forge_target, forge_skip = name, ent["skip"][0]
|
|
break
|
|
if forge_target:
|
|
break
|
|
if forge_target:
|
|
break
|
|
check(forge_target is not None,
|
|
"no Chainsaw-layer proof test declares a skip token, so the forgery attempt below "
|
|
"could not be mounted. That is not a pass: it means this check could not verify "
|
|
"that a self-skip is refused as proof, which is the whole point of the ledger")
|
|
if forge_target:
|
|
run_dir = tmp / "20260101T000000Z-forged"
|
|
run_dir.mkdir(parents=True)
|
|
(run_dir / "report.junit.xml").write_text(
|
|
'<?xml version="1.0" encoding="UTF-8"?>\n'
|
|
'<testsuites><testsuite name="chainsaw" tests="1" failures="0" errors="0">'
|
|
f'<testcase name="{forge_target}" classname="forged"/>'
|
|
"</testsuite></testsuites>\n")
|
|
(run_dir / "run.log").write_text(
|
|
f"=== RUN chainsaw/{forge_target}\n"
|
|
f" === STDOUT\n {forge_skip}\n")
|
|
forged = run([sys.executable, str(LIB / "record_run.py"), "--run-dir", str(run_dir),
|
|
"--dry-run", "--ledger", str(tmp / "never-written.jsonl"),
|
|
"--tests", str(CONF / "tests"), "--repo", str(ROOT)])
|
|
verdicts = re.findall(rf"^\[record\]\s+\S+\s+(\S+)\s+{re.escape(forge_target)}\b",
|
|
forged.stdout, re.M)
|
|
check(verdicts and all(v != "proven" for v in verdicts),
|
|
f"lib/record_run.py recorded a FORGED run as {verdicts!r} for {forge_target!r}: "
|
|
"a JUnit saying `passed` with nothing in the log but that test's own SKIP token "
|
|
f"({forge_skip}). A self-skip must never become proof — with this hole every "
|
|
"audit proof in docs/07 could be produced by a cluster that skipped it")
|
|
check(not (tmp / "never-written.jsonl").exists(),
|
|
"record_run.py --dry-run WROTE to the ledger — a tool that records while "
|
|
"claiming not to cannot be trusted to record only real runs")
|
|
|
|
# ---- FORGERY 2: a ledger row claiming `proven` at a commit that predates the code.
|
|
# status.py must degrade it to stale-proof (not green), or an old green run would keep
|
|
# vouching for code it never executed.
|
|
root_sha = run(["git", "-C", str(ROOT), "rev-list", "--max-parents=0", "HEAD"])
|
|
old_sha = (root_sha.stdout.strip().splitlines() or [""])[0]
|
|
check(len(old_sha) == 40,
|
|
"the repository's root commit could not be resolved, so the stale-proof guard could "
|
|
"not be exercised (that is a gap in this check, not a pass)")
|
|
if len(old_sha) == 40 and forge_target:
|
|
stale_ledger = tmp / "stale.jsonl"
|
|
rid = sorted(smap[forge_target].get("requirements") or ["R-NET-06"])[0]
|
|
stale_ledger.write_text(json.dumps({
|
|
"ts_utc": "2026-01-01T00:00:00Z", "git_sha": old_sha, "env": "dev",
|
|
"chainsaw_version": "v0.0.0", "kube_version": "unknown",
|
|
"layer": smap[forge_target].get("layer", "L3"), "test": forge_target,
|
|
"requirements": [rid], "junit_result": "passed",
|
|
"sentinel": (smap[forge_target].get("terminal_pass") or "X"),
|
|
"proof": "proven", "run_id": "20260101T000000Z-forged",
|
|
"note": "synthetic row written by the R-SEC-03 conformance check",
|
|
}) + "\n")
|
|
out2 = tmp / "status-stale"
|
|
st2 = run([sys.executable, str(LIB / "status.py"), "--repo", str(ROOT),
|
|
"--registry", str(CONF / "requirements" / "registry.yaml"),
|
|
"--tests", str(CONF / "tests"), "--out", str(out2),
|
|
"--ledger", str(stale_ledger)])
|
|
check(st2.returncode == 0,
|
|
f"lib/status.py failed against a synthetic ledger: "
|
|
f"{(st2.stderr or st2.stdout).strip()[:300]}")
|
|
s2 = json.loads((out2 / "status.json").read_text()) if (out2 / "status.json").is_file() else {}
|
|
rec2 = (s2.get("by_requirement") or {}).get(rid) or {}
|
|
per = {p.get("test"): p.get("state") for p in ((rec2.get("proof") or {}).get("per_test") or [])}
|
|
check(per.get(forge_target) == "stale-proof",
|
|
f"a ledger row claiming `proven` for {forge_target!r} at the repository's ROOT "
|
|
f"commit was reported as {per.get(forge_target)!r} instead of 'stale-proof'. A "
|
|
"proof from a run that predates the code it vouches for is not evidence, and "
|
|
"honouring it would let one old green run certify every later change")
|
|
check((rec2.get("proof") or {}).get("state") != "proven",
|
|
f"{rid} is reported PROVEN on the strength of a row from the root commit — the "
|
|
"freshness guard is not holding")
|
|
|
|
# ---- the ledger itself is machine-readable, and no row proves a test that is gone ----
|
|
ledger = CONF / "runs" / "ledger.jsonl"
|
|
if ledger.is_file():
|
|
rows, bad = [], []
|
|
for i, line in enumerate(ledger.read_text().splitlines(), 1):
|
|
if not line.strip():
|
|
continue
|
|
try:
|
|
rows.append(json.loads(line))
|
|
except json.JSONDecodeError:
|
|
bad.append(i)
|
|
check(not bad,
|
|
f"conformance/runs/ledger.jsonl has unparsable line(s) {bad} — the audit record "
|
|
"is not machine-readable, so no proof can be derived from it")
|
|
# Which rows are HONOURED: status.py resolves duplicates latest-wins (latest_by_test),
|
|
# so a superseded row is not evidence of anything. The dirty-tree assertion below is
|
|
# therefore scoped to honoured rows. Without that scoping, ONE historical dirty row reds
|
|
# this gate permanently even after a clean re-run of the same test — and a dirty-then-
|
|
# clean sequence is the normal shape of "noticed the tree was dirty, fixed it, re-ran".
|
|
# The row is still kept in the ledger and its run.log stays committed: nothing is erased,
|
|
# it simply stops being treated as a live claim. Structural assertions (provenance keys,
|
|
# sentinel, test-still-exists) still apply to EVERY row.
|
|
honoured_ids = {id(v) for v in rr_latest_by_test(rows).values()}
|
|
for r in rows:
|
|
for key in ("ts_utc", "git_sha", "test", "requirements", "junit_result", "proof",
|
|
"run_id"):
|
|
check(key in r,
|
|
f"a ledger row for {r.get('test', '?')!r} lacks {key!r} — a row without "
|
|
"provenance cannot be audited")
|
|
if r.get("proof") == "proven":
|
|
# L0/L1 rows are recorded proven WITHOUT a sentinel, deliberately, by
|
|
# record_run.py's own SENTINEL_EXEMPT_LAYERS: run_l1_offline.py renders skips as
|
|
# JUnit <skipped/>, so those layers have no pass token to attribute. This
|
|
# assertion had NO layer exemption, so the two halves of the harness contradicted
|
|
# each other — ANY `--record` run touching L0 or L1 wrote a row this gate then
|
|
# rejected, which meant a requirement whose verifier set includes an L1 check
|
|
# (R-NET-06 is one) could never be both PROVEN and L0-green. Honour the same
|
|
# constant rather than restating the policy here, so the two cannot drift apart.
|
|
if r.get("layer") not in rr.SENTINEL_EXEMPT_LAYERS:
|
|
check(bool(r.get("sentinel")),
|
|
f"a ledger row claims `proven` for {r.get('test')!r} with NO sentinel — "
|
|
"the sentinel is the only thing separating a real pass from a self-skip")
|
|
check(r.get("test") in smap,
|
|
f"a ledger row claims `proven` for {r.get('test')!r}, which is not a "
|
|
"test in the suite any more — a proof of something that no longer exists")
|
|
check(id(r) not in honoured_ids or "-dirty" not in str(r.get("git_sha", "")),
|
|
f"a ledger row claims `proven` for {r.get('test')!r} from a DIRTY tree "
|
|
f"({r.get('git_sha')}) — what ran is not what is committed")
|
|
else:
|
|
note("conformance/runs/ledger.jsonl does not exist yet — the ledger-shape assertions "
|
|
"were skipped; every other assertion ran, and the forgery probes above use "
|
|
"synthetic ledgers, not this file")
|
|
finally:
|
|
shutil.rmtree(tmp, ignore_errors=True)
|
|
|
|
# --------------------------------------------------------------------------- verdict
|
|
# NO-OP GUARD: a check that quietly asserts nothing is worse than no check.
|
|
check(CHECKS >= 30,
|
|
f"only {CHECKS} assertions ran — the check degenerated to a near-no-op and its pass "
|
|
"would be meaningless")
|
|
|
|
if FAILURES:
|
|
die()
|
|
for n in NOTES:
|
|
print(f" note: {n}")
|
|
print(f"check OK: auditability-proofs-producible — {CHECKS} assertions; the five docs/07 "
|
|
f"proofs ({', '.join(sorted(PROOFS))}) each map to an executable test at the layer the "
|
|
f"spec's own wording requires, `run.sh --requirements {','.join(PROOF_REQS)}` resolves "
|
|
"and asserts them, each Chainsaw-layer proof declares a sentinel record_run.py can "
|
|
"attribute, both evidence tools' self-tests pass, and two independent forgeries — a "
|
|
"self-skip presented as a pass, and a `proven` row from the root commit — were REFUSED. "
|
|
"R-SEC-03's producibility half only: whether each proof PASSES is its own "
|
|
"requirement's test, and the Hubble half of the isolation proof is automated nowhere "
|
|
"(see the header's gap list).")
|
|
PY
|