From a2cb720dc4535b2fab40e20c4ff93beaf029c75e Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 3 Aug 2026 16:35:12 +0200 Subject: [PATCH] docs: say what the button enforces today, and where each check stops MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round-8 estate review (GPT-5.6). Their central complaint across the estate was that documents promise more than code checks. Here the drift ran the other way as well: two phases were added this week and the documents described neither, so the repository was UNDER-claiming while its own header still listed four phases. check.sh header now lists Phase 0d and Phase 3b, each with the reason it exists rather than only what it does README "binds four things" -> six, and says plainly that four are checked inside Lean by Proofs/Audit.lean while the last two deliberately do NOT rely on that file. "four model files" -> five (the template is pinned now). The Phase 3b bullet carries its demonstration: axiom planted after the audit command, Phase 3 passed it, Phase 3b rejected it TRUSTED-BASE 3 extraction reproducibility split honestly in two. The committed .llbc means the LLBC -> Lean half re-runs on demand and did reproduce Types.lean and Funs.lean byte-identically. The Rust -> LLBC half still needs charon and still rests on the author alone. "Do not read the first half as evidence for the second." TRUSTED-BASE 3b NEW, and it is a limit rather than a capability: Phase 0d is TEXTUAL. It does not ask Lean how names resolve — the ed25519 repositories have a semantic phase for that and this one does not. All eleven externals here happen to be answered by the model itself, the narrow case where the textual and semantic answers coincide; that is a property of today's corpus, not a guarantee of the check. RECORDED-RUN.md is deliberately untouched again: its "all four model files" and its `797b4ef` pin describe the state at the run it records. A record edited to match today is not a corrected record. Button re-run after every edit: green, 11 externals, 298 declarations across 9 modules, none an axiom. Co-Authored-By: Claude Opus 4.8 --- README.md | 28 +++++++++++++++++++++++----- TRUSTED-BASE.md | 21 +++++++++++++++++++++ verification/check.sh | 13 +++++++++++++ 3 files changed, 57 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 0c571ec..92dbb16 100644 --- a/README.md +++ b/README.md @@ -8,9 +8,10 @@ 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. The audit runs **inside Lean** -(`verification/Proofs/Audit.lean`) and binds four things, each added because an -external reviewer *demonstrated* the button going green without it: +compile, and the audit passes. It binds **six** 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 +separate phases that deliberately do **not** rely on that file: - **axiom cones** — each certificate's cone is read from the kernel via `collectAxioms` and must equal its expected set EXACTLY, so an added axiom @@ -26,9 +27,26 @@ external reviewer *demonstrated* the button going green without it: *body*. Round 5 showed why the last part is essential: redefining a fold to *be* the extracted loop left every earlier fingerprint bit-identical while the certificate degenerated to "the loop equals the loop"; -- **bytes** — Phase 0 sha256-pins the four model files and the compiler harness +- **bytes** — Phase 0 sha256-pins the five model files and the compiler harness `lean-guard`, purges stale `.olean`s, and forbids stray `.lean` files, so the - verdict depends on committed bytes rather than build-directory state. + verdict depends on committed bytes rather than build-directory state; +- **correspondence** (Phase 0d) — byte pins say the model did not *change*; they + say nothing about whether it *answers the extraction*. Aeneas states what the + extracted Rust needs from outside in `FunsExternal_Template.lean`, and every + such name must be answered by the hand-written model or by a real definition + in the corpus. An **extra axiom** in the model — an assumption no template + asks for — fails the button rather than passing as a silent row. This + repository previously deleted the template on every run, which is exactly why + it shipped a Template/model pair with no correspondence check at all + (round-8 estate review, GPT-5.6); +- **the object files** (Phase 3b) — a second, independently implemented axiom + gate that reads the compiled `.olean`s via `readModuleData` instead of the + elaboration-time environment. Phase 3's view has a demonstrated blind spot: a + declaration made *after* the command that performs the walk sits in the object + file but not in the environment while the walk runs, so the walker reports "no + 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. 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/TRUSTED-BASE.md b/TRUSTED-BASE.md index 7cdee30..9fa7c49 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -20,6 +20,27 @@ proceeds and is part of every claim. toolchain) are trusted to preserve semantics from Rust (MIR) to the Lean model. Divergence between rustc's semantics and the extracted model is trusted base. + + **What is now reproducible, and what is not.** Extraction is two steps: + `Rust --charon--> SlhVerify.llbc --aeneas--> gen/SlhVerify/*.lean`. The + `.llbc` is committed, so the SECOND step can be re-run by anyone with the + pinned Aeneas and this repository, and on 2026-08-03 doing so reproduced + `Types.lean` and `Funs.lean` **byte-identically**. The FIRST step still + requires charon, which no reviewer has yet had available. So: the + LLBC → Lean half is reproducible on demand; the Rust → LLBC half rests on + the author's attestation alone, and continues to do so until a third party + runs it. Do not read the first half as evidence for the second. + +3b. **The correspondence check is textual, not a Lean query.** Phase 0d parses + `FunsExternal_Template.lean` and the hand-written model as SOURCE TEXT. It + establishes that every external the extraction names is answered by a + declaration of the right name in the pinned model, and that the model + declares no axiom the extraction never asked for. It does **not** ask Lean + how those names resolve at elaboration — the four ed25519 repositories have + a second, semantic phase for that; this one does not. All eleven externals + here are answered by the model itself (none by the proven corpus), which is + the narrow case where the textual answer and the semantic one coincide, but + that is a property of today's corpus and not a guarantee of the check. 4. **The Lean kernel and its three axioms** (`propext, Classical.choice, Quot.sound`). 5. **Build correspondence.** No reproducible-builds claim: the proof is diff --git a/verification/check.sh b/verification/check.sh index 708f23e..1057974 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -7,6 +7,11 @@ # depend on committed bytes, not untracked build state), forbid any # .lean outside gen/ and Proofs/, and sha256-pin the four model files # AND the compiler harness `lean-guard` to PROVENANCE.json. +# Phase 0d— template/model correspondence: every external Aeneas states the +# extracted Rust needs (FunsExternal_Template.lean, committed and +# pinned) must be answered by the hand-written model or by a real +# definition in the corpus. An EXTRA AXIOM in the model — an +# assumption no template asks for — is a failure, not a silent row. # Phase 1 — compile the extracted Lean model (gen/SlhVerify). # Phase 2 — compile the proof files (Proofs/). # Phase 3 — the in-Lean audit (Proofs/Audit.lean): per certificate, the cone @@ -17,6 +22,14 @@ # POLICY constants, every certificate STATEMENT, and every reachable # SPECIFICATION DEFINITION BODY. Any mismatch → non-zero exit → # fail-closed. No text parsing of axiom cones. +# Phase 3b— kernel-side axiom-declaration gate: reads the compiled OBJECT +# FILES (`readModuleData`) rather than the elaboration-time +# environment, and rejects any axiom declared under Proofs/. This is +# a SECOND, independently implemented gate on the same property, +# because Phase 3's view has a demonstrated blind spot: a +# 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. # # 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.