From 65211a877569ffca56179550a33b48c7fd2a93af Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sun, 16 Aug 2026 18:32:40 +0200 Subject: [PATCH] =?UTF-8?q?docs:=20dated-record=20clarity=20for=20the=20pr?= =?UTF-8?q?e-Green=20scan=20=E2=80=94=20attestations=20that=20have=20since?= =?UTF-8?q?=20occurred=20say=20so;=20leaf-index=20numbering=20unified?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ATTESTATION-BASIS.md | 3 ++- README.md | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/ATTESTATION-BASIS.md b/ATTESTATION-BASIS.md index 8da93ec..f34894c 100644 --- a/ATTESTATION-BASIS.md +++ b/ATTESTATION-BASIS.md @@ -7,7 +7,8 @@ consumer never sees. Nothing in this file is a decision to attest. The signing-key halt and the paper-appeal gate are the operator's, and an attest verdict from a reviewer is a -technical input to that decision, not the decision. +technical input to that decision, not the decision. (The attestation has since +occurred: LTL leaf 18, 2026-08-08 — this file remains the conditions record.) --- diff --git a/README.md b/README.md index 4ccbf62..88cb4d2 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ path**, extracted from a pure-Rust implementation into Lean 4 via Charon/Aeneas — the same pipeline, discipline, and honesty rules as the four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`). -## STATUS: eleven certificates over the extracted verify model (external review rounds 1–9 applied) +## STATUS: eleven certificates over the extracted verify model (external review rounds 1–9 applied); attested in the Lean Transparency Log as leaf 18 (2026-08-08), the log's first post-quantum entry `verification/check.sh` is **green** (exit 0): the model compiles, the proofs compile, and the audit passes. It binds **seven** things, each added because an