From e8d79241138af49bf4e16032ec3dfe411ad93b16 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 30 Jul 2026 19:16:20 +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 d8a4281..23e2b9c 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -182,3 +182,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. + +13. **`--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 028a621..36dae64 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,6 +1,6 @@ 6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf check-scalar.sh -27b84e22853e381c31bb89ccf38ac333ec13ff1eadc5828eabf9c8f577e79a15 check.sh +a8f560f1d46560ee8b90f90ffeeb63b1eccf0afdf1d6652a37a2047786945434 check.sh afa13c814ba9757de8d59777524e496653351112a1a7037a56f1b0b436b28cf9 extract.sh 0ea20d74cd359da404ee3be116058374cbb9fd992ed170e5f6c64f8d7a6b2733 GEN-MODEL.sha256 e95982c15c7d754f0c9bcffef95d4c9d4c63589ac51ecdd40870133f377a005c inventory-allowlist-scalar.txt @@ -11,7 +11,8 @@ e95982c15c7d754f0c9bcffef95d4c9d4c63589ac51ecdd40870133f377a005c 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 24cd83c..bb6eb88 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 @@ -299,6 +334,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" @@ -331,6 +394,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 @@ -637,6 +701,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