From e896ccfb9bd8990e9dfbccc22b97b70590b3b490 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Fri, 7 Aug 2026 16:00:53 +0200 Subject: [PATCH] docs: estate-wide consistency pass (workflow audit, 36 findings, all verified before fixing) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Nine parallel readers audited every doc against measured ground truth; every finding was re-verified against the file before any edit, and the sweep fixed by PROPERTY, not by flag — wording the readers caught in one repo was hunted in all siblings (the two-button README sentence existed in all four forks, not the three flagged; likewise the cone-overclaim in TRUSTED-BASE item 1). This repo: see the diff. Records were not rewritten; clarifications are dated. Doc-only except where noted in the estate summary; every gated doc change was followed by a green button run. Co-Authored-By: Claude Opus 4.8 --- README.md | 8 +++++--- TRUSTED-BASE.md | 13 +++++++++---- 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index aa44b64..ab653c1 100644 --- a/README.md +++ b/README.md @@ -18,8 +18,10 @@ coherent proof pyramid in Lean 4 via the Charon/Aeneas transpilation pipeline: Every layer states its theorems about the **actual Aeneas-transpiled Rust code** (never about a hand-written re-model), and every claim in the status table below is backed by a compiled proof plus an axiom audit of the named -certificate. Files that do not compile under `verification/check.sh` are not -in this repository. +certificate. Files that compile under neither `verification/check.sh` nor +`verification/check-scalar.sh` are not in this repository — each shipped +proof source belongs to exactly one button's manifest, and the seam gate +fails the build otherwise. ## Layer status @@ -110,7 +112,7 @@ cones deviates from the boundary above. source ~/aeneas-toolchain/env.sh cd verification ./extract.sh # Rust → LLBC → Lean (regenerates gen/) -./check.sh # compiles EVERY shipped file + axiom-audits EVERY certificate +./check.sh # compiles + audits everything the MAIN manifest owns (scalar layer: its own button below) ``` The gen model is ONE merged universe (`gen/CurveField`: field + curve + diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 6bcd6b4..dbc14a0 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -4,8 +4,11 @@ What you must believe for the theorems in this repository to transfer to the running Rust code. Everything else is machine-checked. 1. **Lean 4 kernel** (v4.30.0-rc2) and its three foundational axioms - `[propext, Classical.choice, Quot.sound]`. Every certificate is - `#print axioms`-audited against exactly this list. + `[propext, Classical.choice, Quot.sound]`. Every arithmetic and scalar + certificate is `#print axioms`-audited against exactly this list; the four + apex-tier certificates are audited against this list plus their documented + boundary axioms (the signature-apex item below), both enforced exactly — + nothing more, nothing less — by the button. 2. **mathlib** (prebuilt oleans fetched by `lake exe cache get`). 3. **Charon + Aeneas** (pinned `9dd7f23c` / `bf13c42e`): the translation from Rust MIR to the Lean model is assumed faithful. The generated @@ -175,8 +178,10 @@ running Rust code. Everything else is machine-checked. cross-check, its corpus being mathlib-free. · *The scalar layer is outside this phase.* Thirteen `Proofs/Scalar*` - modules belong to `check-scalar.sh` and are inventoried by nothing. That - is the two-button seam, still open. Phase 2c prints every uncovered + modules belong to `check-scalar.sh` and sit outside `check.sh`'s + Phase 2c specifically — they are inventoried by `check-scalar.sh`'s own + Phase 2c against `inventory-allowlist-scalar.txt`, both directions. The + two-button seam itself closed 2026-07-30 (see the two-button item below). Phase 2c prints every uncovered module by name on every run, so the omission is visible rather than inferred.