From 5a9d4237dd7c1712fb1bf6a8cd00734f2afcb691 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 28 Jul 2026 21:18:50 +0200 Subject: [PATCH] TRUSTED-BASE: record the kernel-side axiom gate and its residue MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds one item naming what check.sh Phase 2b binds — every compiled Proofs/*.olean, kernel-side, membership self-derived, fail-closed on a missing module — and, more importantly, what it still does not bind: declarations, not statements. A theorem gutted to a tautology with the same axiom cone passes every phase. Reading the statements remains a human act, and this document is where that has to be said rather than left for a reviewer to discover. Verified green at this commit's parent across all eight buttons on 2026-07-28; see formal-verification-control/RECORDED-RUN-2026-07-28.md. Co-Authored-By: Claude Opus 4.8 --- TRUSTED-BASE.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 64f0058..3bac923 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -37,3 +37,19 @@ running Rust code. Everything else is machine-checked. 6. **Compilation of Rust to machine code** (rustc backend) is out of scope, as is side-channel behaviour (timing, speculation). The proofs are about functional correctness at the MIR/LLBC level. +7. **What the axiom gate binds, and what it does not.** `check.sh` Phase 2b + reads every compiled `Proofs/*.olean` and fails the build if any + declaration there is an axiom. It asks the kernel rather than parsing + source text, because the source-text check in Phase 1 is evadable four + ways — an indented `axiom`, `@[simp] axiom`, `unsafe axiom`, and `axiom` + with the name on the following line all compile and all miss its pattern. + Membership self-derives from the filesystem, so `Scalar*` and `AxiomCheck` + are covered as well, and the count of compiled modules must equal the + count of shipped sources, so a deleted `.olean` cannot make the scan pass + vacuously. `selftest-axgate.sh` attacks the shipping gate rather than a + copy of it, and was itself negative-tested by removing the gate's error. + **The residue you must still supply yourself:** this binds *declarations*, + not *statements*. Nothing in the button establishes that a certificate's + theorem says what its name — or this document — suggests it says. A + theorem gutted to a tautology with the same axiom cone would pass every + phase. Reading the statements remains a human act.