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