From 049a6f65560861370a02b5db8bfd36335b6b57fc Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 30 Jul 2026 19:16:18 +0200 Subject: [PATCH] verification: --audit-only mode, and the guard that keeps it from becoming evidence (T1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Gate work dominates this estate's wall-clock: on 2026-07-29, 3.9 hours of a session went to Lean re-elaborating proofs nobody had edited while the audit phases themselves took about fifteen seconds. --audit-only runs every gate against the artifacts a previous full run left behind: ~60s against ~1280s. IT IS SAFE ONLY BECAUSE IT REFUSES. - It requires every shipped .lean to be BYTE-IDENTICAL to a basis recorded by a previous full run. Not mtimes: `touch` defeats those, and a stale-artifact check that fails open is worse than no shortcut at all, because a green button would then describe a corpus that is no longer on disk. - The basis is gitignored build state, so a fresh clone cannot inherit permission to skip compiling. - The closing banner differs and says in words that the run is not evidence. selftest-auditonly.sh exercises seven cases: no basis, an edited comment character, a deleted source, a new source, a missing artifact, a truncated basis, and — asserted as a PASS — every source's mtime touched with bytes unchanged, which pins the bytes-not-mtimes decision rather than leaving it implicit. Negative-tested: with the basis comparison disabled a changed source is wrongly accepted, exit 0 and zero refusals, so the guard is load-bearing. A PHASE TERMINATOR, because this broke twice. Every self-test lifts a phase from check.sh by scanning to the next phase marker. The last phase had no marker after it, so a lift ran to end-of-file and swallowed whatever was appended later — first Phase 2c into the axgate lift, then T1's tail into the binding lift, where it referenced $AUDIT_ONLY and died under `set -u`. Both surfaced as the BASELINE case failing: a self-test blaming a gate for its own extraction bug. The phases now end at an explicit sentinel and both lifters stop there, so nothing appended below can silently become part of the last phase from a lifter's point of view. TRUSTED-BASE.md records what an audit-only transcript does and does not establish, and — because it cost a confusing red run today — that lean-guard's memory clamp presents as `FAIL: Proofs/` while being a resource condition, not a broken proof. Verified green: 8 full button runs (four check.sh, four check-scalar.sh) and 20 self-tests across the four repositories, zero red. One earlier run failed on the memory clamp because the author ran a test suite concurrently; re-run on a quiet machine, green. Co-Authored-By: Claude Opus 4.8 --- .gitignore | 1 + TRUSTED-BASE.md | 30 ++++++++ verification/HARNESS.sha256 | 7 +- verification/check.sh | 80 ++++++++++++++++++++ verification/selftest-auditonly.sh | 112 ++++++++++++++++++++++++++++ verification/selftest-axgate.sh | 2 +- verification/selftest-statements.sh | 2 +- 7 files changed, 229 insertions(+), 5 deletions(-) create mode 100755 verification/selftest-auditonly.sh diff --git a/.gitignore b/.gitignore index 24f9b74..1e9659c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ *.olean .lake/ lake-manifest.json +.audit-basis diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 03d2b8b..017b1ed 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -177,3 +177,33 @@ running Rust code. Everything else is machine-checked. button's driver. All three now test membership in a manifest. This is the same family as the source-text axiom grep that began this campaign: reasoning about names instead of about the thing itself. + +12. **`--audit-only`, and why a green transcript from it is not evidence.** + `check.sh --audit-only` runs every gate but skips recompilation, against the + `.olean` files a previous full run left behind: about 60 seconds against + about 1280. It exists because gate work dominates this estate's wall-clock, + and it is safe only because it refuses. + + It refuses unless every shipped `.lean` is BYTE-IDENTICAL to a basis + recorded by a previous full run — not mtimes, which `touch` defeats, and a + stale-artifact check that fails open would be worse than no shortcut at all: + a green button would then describe a corpus that is no longer on disk. The + basis is gitignored build state, so a fresh clone cannot inherit permission + to skip compiling, and the closing banner says in words that the run is not + evidence. + + **The kernel re-elaborates nothing in such a run.** What it establishes is + that the gates accept artifacts produced earlier — useful while developing a + gate, worthless as a record. `formal-verification-control/tools/record-run.py` + enforces that: it refuses to archive any transcript bearing the audit-only + markers, and also any transcript without a terminal success banner, any + containing `error:`, and any repository whose tree is dirty at record time. + A banner is a request; that tool is the gate. + + Also worth knowing when reading a red run: `lean-guard` clamps Lean's memory + budget to what the machine can spare, and under load that clamp can be too + small to elaborate a large module. It surfaces as `FAIL: Proofs/`, + which reads exactly like a broken proof and is not one — it is a resource + condition, and the cap is what protects this machine from the global OOM + that killed a session on 2026-07-02. Check the transcript for a `clamping` + line before concluding anything about the mathematics. diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 5977013..c3a2a1e 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,6 +1,6 @@ 12dc724bffd590e6f706573d97bf07425b8f268a1be2d72a3bbd9aef48f9c277 AUDIT-MANIFEST.txt 6b25b7e261633f4fa703de0be1dfd3c263d043107e3b3225d4c5079a93b6a64d check-scalar.sh -7367ebcca2ee288df3ce13ad693cc2493b3aecc0e087e78b514fd87f09eb2335 check.sh +d1f6d4bfeca87f1ae21fff97cf726fb5a083007874c2f01e8055a1ec5689f77e check.sh 64602c31ef34e740a0a27431534fa2ca65b6cd90a99cb17e119915a82a38b474 extract.sh 52afbe130c5551686f45643a35065729fd5bb8166b5fa3db67b74c60ba3eff62 GEN-MODEL.sha256 6033c86eb08b4c2ea0bd7cdbd2cfb5748059179ece3efa9673270dc17a2e38b9 inventory-allowlist-scalar.txt @@ -12,7 +12,8 @@ b2c79ccf7005051946d49ee1fb0b51fbee58819c5909c6efb00965547b56fa5d inventory-allo 84bc670991fd7456d8c8569ff7b7c32410513a63d3cb7fe8877bb19a82d36a7d Proofs/InventoryCore.lean 4b1d7f5249a80375b4ef849a760ae8e4bbcecf103c3f8b9e8d0a5d5a9ae377fc Proofs/Inventory.lean 6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78 Proofs/InventoryScalar.lean -62da1de45d2e19abe588a75e32454548e8caa3067ff51a97d7ae155886dbe0c0 selftest-axgate.sh +bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh +eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171 selftest-axgate.sh 3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh 1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh -bf88da29034ae32fe6aef8677c8952adcc2b6903e7b2972ea70971f276be0f45 selftest-statements.sh +2c591fb2a0cc50cfdf76c3328e5d72d52b69c02f5b230ebc55c977d6570ecc0f selftest-statements.sh diff --git a/verification/check.sh b/verification/check.sh index 0c4adf6..73bf8ad 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -37,6 +37,41 @@ TIMEOUT="${LEAN_TIMEOUT:-300}" export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}" # 8192: ReduceSpec exceeds 6144 (coherence pass 2) CORES="${LEAN_MAX_CORES:-0-3}" +# ── Mode selection ────────────────────────────────────────────────────────── +# --audit-only runs every gate EXCEPT the compile, against the .olean files a +# previous full run left behind. It exists because gate work dominates this +# estate's wall-clock: on 2026-07-29, 3.9 hours of a session went to Lean +# re-elaborating proofs nobody had edited, while the audit phases themselves +# take about fifteen seconds. +# +# IT MUST BE IMPOSSIBLE TO MISUSE, so: +# · it refuses to run unless a previous FULL run recorded a basis of source +# hashes AND every source still matches it byte-for-byte. Not mtimes — +# `touch` defeats those, and a stale-artifact check that fails open is +# worse than no shortcut at all, because a green button would then +# describe a corpus that is no longer on disk; +# · the basis file is build state, never committed, so a fresh clone cannot +# inherit permission to skip compiling; +# · the final banner DIFFERS, and says in words that the run is not evidence. +# A transcript must never be mistakable for a full one. +AUDIT_ONLY=0 +for arg in "$@"; do + case "$arg" in + --audit-only) AUDIT_ONLY=1 ;; + --help|-h) echo "usage: check.sh [--audit-only]"; exit 0 ;; + *) echo "unknown argument: $arg (see --help)"; exit 1 ;; + esac +done +BASIS="$HERE/.audit-basis" # gitignored build state, written by full runs + +# Every .lean this repository ships, with its hash: the exact set whose +# recompilation --audit-only proposes to skip. +source_basis() { + { find "$HERE/Proofs" -name '*.lean' -type f -printf '%P\n' | sed 's|^|Proofs/|' + find "$HERE/gen" -name '*.lean' -type f -printf '%P\n' | sed 's|^|gen/|'; } \ + | LC_ALL=C sort | while read -r f; do printf '%s %s\n' "$(sha256sum "$HERE/$f" | cut -d' ' -f1)" "$f"; done +} + # Layer manifests (extended as the pyramid grows; ORDER = import order). GEN_MODULES=( CurveField/TypesExternal @@ -297,6 +332,34 @@ done <<<"$SCALAR_MANIFEST" [ "$SEAMFAIL" = 0 ] && echo " every proof source belongs to exactly one button ($(grep -c . <<<"$MAIN_MANIFEST") here, $(grep -c . <<<"$SCALAR_MANIFEST") scalar)" [ "$SEAMFAIL" = 0 ] || { echo "SEAM CHECK FAILED"; exit 1; } # ── Phase 2: compile everything shipped ───────────────────────────────────── +if [ "$AUDIT_ONLY" = 1 ]; then + echo "=== Phase 2: SKIPPED (--audit-only) ===" + if [ ! -s "$BASIS" ]; then + echo "REFUSING: no basis from a previous full run ($BASIS absent)." + echo " --audit-only may only follow a full green run in this working tree." + echo " Run ./check.sh with no arguments first." + exit 1 + fi + if ! diff -q <(source_basis) "$BASIS" >/dev/null 2>&1; then + echo "REFUSING: the sources no longer match the basis of the last full run." + echo " The .olean files on disk describe a corpus that has changed, so every" + echo " audit below would be judging artifacts that no source produces." + echo " Differences (< basis, > now):" + diff <(source_basis) "$BASIS" | head -20 | sed 's/^/ /' + echo " Run ./check.sh with no arguments." + exit 1 + fi + # Fail closed on absence too: a source with no artifact cannot be audited. + MISSING=0 + for m in "${PROOFS[@]}"; do + [ -f "$HERE/Proofs/$m.olean" ] || { echo " MISSING ARTIFACT: Proofs/$m.olean"; MISSING=1; } + done + for m in "${GEN_MODULES[@]}"; do + [ -f "$HERE/gen/$m.olean" ] || { echo " MISSING ARTIFACT: gen/$m.olean"; MISSING=1; } + done + [ "$MISSING" = 0 ] || { echo "REFUSING: run ./check.sh with no arguments."; exit 1; } + echo " sources byte-identical to the last full run's basis; $(grep -c . "$BASIS") files" +else echo "=== Phase 2: compile ===" LOG=$(mktemp /tmp/check-compile-XXXX.log) cd "$AENEAS_LEAN" @@ -329,6 +392,7 @@ lake env bash -c " if grep -q "uses 'sorry'" "$LOG"; then echo "STUB DETECTED: a compiled declaration uses 'sorry'"; exit 1; fi rm -f "$LOG" +fi # ── Phase 2b: kernel-side axiom-declaration gate ──────────────────────────── # WHY THIS EXISTS. Phase 1's anti-smuggling check reads SOURCE TEXT, and a @@ -635,6 +699,22 @@ fi grep -o 'statement audit PASSED:.*' <<<"$AUD_OUT" | sed 's/^/ /' echo " audit-manifest sha256 = $GOT_SHA (matches the committed block byte-for-byte)" +# ── Phases end ────────────────────────────────────────────────────────────── +# Sentinel. Self-tests lift a phase by scanning from its header to the NEXT +# marker; without this the final phase's lift ran to end-of-file and picked up +# everything appended afterwards. Do not remove: anything added below this line +# would otherwise silently become part of the last phase from a lifter's point +# of view. + echo "" +if [ "$AUDIT_ONLY" = 1 ]; then + echo "AUDIT-ONLY RUN — GATES PASSED, PROOFS NOT RECOMPILED." + echo "This is NOT evidence: the kernel did not re-elaborate a single proof in" + echo "this run. It says the gates accept the artifacts a previous full run" + echo "left behind. For a recorded result, run ./check.sh with no arguments." + exit 0 +fi +# Only a full run earns the right to let a later --audit-only skip compiling. +source_basis > "$BASIS" echo "ALL PROOFS PASS. ALL CERTIFICATES AXIOM-CLEAN. NO DEAD FILES." echo "STATEMENTS AND SPECIFICATIONS BOUND TO THE COMMITTED AUDIT MANIFEST." diff --git a/verification/selftest-auditonly.sh b/verification/selftest-auditonly.sh new file mode 100755 index 0000000..c2fd262 --- /dev/null +++ b/verification/selftest-auditonly.sh @@ -0,0 +1,112 @@ +#!/usr/bin/env bash +# ───────────────────────────────────────────────────────────────────────────── +# selftest-auditonly.sh — adversarial self-test for check.sh --audit-only. +# +# --audit-only skips recompilation, which makes it the most dangerous thing in +# this repository: if it ever accepted a tree whose sources had changed, a green +# transcript would describe a corpus that is not on disk. Its whole safety rests +# on refusing, so refusal is what this tests. +# +# Cases, each asserting a SPECIFIC diagnostic: +# 0 no basis recorded -> REFUSING, may only follow a full run +# 1 a proof source edited by one comment -> REFUSING, sources no longer match +# 2 a proof source DELETED -> REFUSING (the basis lists it) +# 3 a NEW proof source added -> ORPHAN, from the seam check, +# which runs BEFORE the mode gate and catches it first +# 4 an artifact deleted, sources intact -> MISSING ARTIFACT +# 5 the basis file truncated -> REFUSING (mismatch, not a pass) +# 6 mtimes touched but bytes unchanged -> PASSES, because bytes are the +# test and mtimes are not: `touch` must neither grant nor deny permission +# +# Requires a prior full green run in this tree (that is what writes the basis). +# No Lean runs here; the whole thing takes seconds. +# ───────────────────────────────────────────────────────────────────────────── +set -uo pipefail +HERE="$(cd "$(dirname "$0")" && pwd)" +FAILURES=0 +STASH="$(mktemp -d)" +BASIS="$HERE/.audit-basis" +VICTIM_SRC="Proofs/FeQ.lean" +VICTIM_ART="Proofs/FeQ.olean" +NEWSRC="$HERE/Proofs/ZZAuditOnlyProbe.lean" + +cleanup() { + [ -f "$STASH/basis" ] && cp "$STASH/basis" "$BASIS" + [ -f "$STASH/src" ] && cp "$STASH/src" "$HERE/$VICTIM_SRC" + [ -f "$STASH/art" ] && cp "$STASH/art" "$HERE/$VICTIM_ART" + rm -f "$NEWSRC" "${NEWSRC%.lean}.olean" + rm -rf "$STASH" +} +trap cleanup EXIT INT TERM + +if [ ! -s "$BASIS" ]; then + echo "FATAL: no basis in this tree. Run ./check.sh with no arguments first;" + echo "this self-test exercises --audit-only, which requires one." + exit 1 +fi +cp "$BASIS" "$STASH/basis" +cp "$HERE/$VICTIM_SRC" "$STASH/src" +cp "$HERE/$VICTIM_ART" "$STASH/art" + +expect() { # expect