From f13707254fe887a0b391f207aa1a9a66eaac220a Mon Sep 17 00:00:00 2001 From: mrwulf Date: Fri, 7 Aug 2026 16:00:54 +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 | 12 ++++++++---- TRUSTED-BASE.md | 7 +++++-- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index f73a0d6..ae606b8 100644 --- a/README.md +++ b/README.md @@ -16,10 +16,14 @@ Charon/Aeneas transpilation pipeline: ``` Every theorem is stated about the **actual Aeneas-transpiled Rust code** from -`src/fields/fp.rs` / `src/curves.rs`. There are **no bridge axioms**: the -correctness of add/sub/neg/mul/square/montgomery_reduce/invert is *proven*, -not assumed. (A previous attempt at this target axiomatized exactly those -statements; this repository exists to do it properly.) +`src/fields/fp.rs`. The rule is **no bridge axioms**: nothing is claimed +proven that is in fact assumed. Proven today: sub/neg, the adc/sbb/mac +helpers, the constants, primality, and the denotation layer; +add/mul/montgomery_reduce/square/invert are **in progress** (drafted in +`Proofs/drafts/`, blocked on kernel proof-checking memory — see Layer status +below). No curve extraction exists yet. (A previous attempt at this target +axiomatized exactly the statements this repository refuses to assume; it +exists to do them properly or not claim them.) ## Layer status diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index f6a6ebc..23c900c 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]`. Three representative + certificates (`P_prime`, `sub_spec`, `INV_spec`) are `#print axioms`-audited + against exactly this list; the remaining foundation theorems are protected + by the no-axiom-declaration grep over `Proofs/` only, which is weaker — + it does not audit their cones. 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