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