From 851e9764505f5b0fe21addc748a76e53f010d1c3 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 3 Aug 2026 17:53:31 +0200 Subject: [PATCH] =?UTF-8?q?docs:=20seven=20bindings,=20not=20six=20?= =?UTF-8?q?=E2=80=94=20the=20documents=20were=20a=20phase=20behind=20again?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit I wrote the README and TRUSTED-BASE to describe six bindings, then added Phase 3c an hour later and did not update them. That is exactly the drift GPT-5.6's round-8 review is about, committed by me immediately after fixing it. Recorded plainly rather than quietly corrected. README six -> seven, with Phase 3c stated in full: both allowlists, both directions (UNCLASSIFIED / STALE), why the instrument surface carries cones, and the accounting identity as set containment with its actual numbers — kernel 300 = corpus 265 + instrument 35, residual none check.sh header lists Phase 3c The failure mode is worth naming because it is cheap and recurring: a phase is added, the button is re-run, the button is green, and nothing anywhere fails because a document is stale. Nothing in this repository can catch it — the gates check the corpus, not the prose. Only reading the diff catches it, which is why the round-8 briefs asked for exactly that. Button re-run after the edits: green, accounting over 300 kernel constants. Co-Authored-By: Claude Opus 4.8 --- README.md | 19 +++++++++++++++++-- verification/check.sh | 4 ++++ 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 92dbb16..d41c5e7 100644 --- a/README.md +++ b/README.md @@ -8,9 +8,9 @@ four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`). ## STATUS: eleven certificates over the extracted verify model (external review rounds 1–6 applied) `verification/check.sh` is **green** (exit 0): the model compiles, the proofs -compile, and the audit passes. It binds **six** things, each added because an +compile, and the audit passes. It binds **seven** things, each added because an external reviewer *demonstrated* the button going green without it. Four are -checked **inside Lean** by `verification/Proofs/Audit.lean`; the last two are +checked **inside Lean** by `verification/Proofs/Audit.lean`; the last three are separate phases that deliberately do **not** rely on that file: - **axiom cones** — each certificate's cone is read from the kernel via @@ -47,6 +47,21 @@ separate phases that deliberately do **not** rely on that file: axiom" and is telling the truth about what it could see. Verified here by planting `axiom cheat : ∀ (P : Prop), P` after the audit command — Phase 3 passed it, Phase 3b rejected it. +- **which declarations exist** (Phase 3c) — the checks above prove each + certificate's cone is exact and that nothing in scope carries a disallowed + axiom. They do not pin WHICH declarations exist: a new one that happens to be + clean, and a silently vanished one, both pass. `inventory-allowlist.txt` (265 + rows) and `driver-allowlist.txt` (35 rows) pin the corpus and the audit + instrument's own surface as `module|name|kind|cone`, diffed in **both** + directions — UNCLASSIFIED for a declaration no row describes, STALE for a row + with no declaration behind it. The instrument surface carries cones because + enumeration is not audit: a claim planted in an instrument is counted and then + examined by nothing if its row has no cone and no allowlist covers it. + Finally the **accounting identity**, as set containment rather than + arithmetic: every constant the kernel holds must appear in one of the two + walks — `kernel 300 = corpus 265 + instrument 35`, residual none. A residual + that has to be explained is a fudge term waiting to absorb the next real + finding. What the button still does **not** bind is stated plainly in [TRUSTED-BASE.md](TRUSTED-BASE.md) item 11 — `check.sh` itself, the toolchain diff --git a/verification/check.sh b/verification/check.sh index ff02a4d..1586084 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -30,6 +30,10 @@ # declaration made after the command that performs the walk is in # the object file but not in the environment while the walk runs. # It runs after Phase 3 because Proofs/Audit.lean is compiled there. +# Phase 3c— declaration coverage + the accounting identity: both walks diffed +# against committed allowlists in BOTH directions, and every +# constant the kernel holds must be accounted for by one of them. +# Set containment, never arithmetic. # # What this button does NOT bind is stated in TRUSTED-BASE.md item 11: this # script itself, the toolchain env, $AENEAS_HOME, and the Lean toolchain.