From 362d62aed60559203b75e984907e37ec5161d9bb Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sun, 16 Aug 2026 18:32:38 +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-RUNBOOK.md | 2 +- README.md | 12 +++++++----- RESPONSE-TO-REVIEWERS.md | 6 ++++-- 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/ATTESTATION-RUNBOOK.md b/ATTESTATION-RUNBOOK.md index 706f3e5..05c496f 100644 --- a/ATTESTATION-RUNBOOK.md +++ b/ATTESTATION-RUNBOOK.md @@ -24,7 +24,7 @@ Agent Appendix at the end. Every step ends in a mechanical check. | **operator** | The human running the log service (owner of ltl.zkdefi.org and its keys). NOT warden (warden is a consumer). All Phase-B actions are operator actions. | | **corpus** | `ltl-accumulator-verified` at freeze commit `172a1d0` (round-5 freeze — the reviewed subject; supersedes the earlier `2da0a79`) — the kernel-checked mechanization of paper §6. | | **the button** | `verification/check.sh`. Green means: printed `=== ATTESTATION GREEN (Lean + fidelity) ===` AND `echo $?` printed `0`. BOTH. Never judge from scrolled output. | -| **the log** | Live service ltl.zkdefi.org + public mirror repo `lean-transparency-log`. At execution time: 12 leaves (indices 0–11), head root `bcd15f9d…`, frozen. NOW (post-execution): 13 leaves, head root `3488a2d0…`, entry 13 live. | +| **the log** | Live service ltl.zkdefi.org + public mirror repo `lean-transparency-log`. At execution time: 12 leaves (indices 0–11), head root `bcd15f9d…`, frozen. As of this record's date (2026-07-16, post-execution): 13 leaves, head root `3488a2d0…`, leaf 12 live. | | **entry 13** | The attestation of the corpus itself. APPENDED 2026-07-16 as leaf index 12 (leaf hash `8cb258d6…`); this runbook is the record of that execution. | | **kit round N** | The review package delivered to the external reviewers after freeze N. Round-1 kit = freeze `6e56414`; round 2 = `260ad64`; round 3 = `9972ab4`; round 4 = `2da0a79`; round 5 = `172a1d0`; round 6 = review of `172a1d0` + pacta producer (current). | diff --git a/README.md b/README.md index 2a03c11..af9cc6d 100644 --- a/README.md +++ b/README.md @@ -9,22 +9,24 @@ results in its §5 and carries this corpus as entry 13): the Merkle accumulator's own correctness and soundness theorems, kernel-checked, in the same discipline as the four `*-ed25519-verified` subject corpora. -## Status: **ATTESTED — LTL entry 13, live (2026-07-16)** +## Status: **ATTESTED — LTL leaf 12 (the log's thirteenth entry), 2026-07-16; hardened model re-attested as leaf 17 (2026-08-08)** This corpus is now itself a leaf of the log it describes. It was appended as **entry 13** of the Lean Transparency Log (freeze `172a1d0`), so the log carries kernel-checked proofs *about the accumulator model* underlying its own inclusion and consistency reasoning (a deployment we are unaware of a precedent for; scoped to the mechanized model, not the -deployed verifier — see below). Live head after the append: -tree size **13**, root +deployed verifier — see below). Head at the time of the append +(2026-07-16): tree size **13**, root `3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d`; this corpus is leaf index 12, hash `8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a`. The old 12-leaf head (`bcd15f9d…`) is a proven prefix; the 12→13 consistency transition is accepted by both the deployed verifier and the mechanized -model. Fetch and verify it at -[ltl.zkdefi.org/v1/sth](https://ltl.zkdefi.org/v1/sth). The leaf carries +model. The log has since grown (nineteen leaves, dual-signed heads); +the current head is at +[ltl.zkdefi.org/v1/sth](https://ltl.zkdefi.org/v1/sth), and this leaf's +inclusion still verifies under it. The leaf carries its own **scope** block: what is kernel-checked is the mechanized model (§6), and correspondence to the deployed verifier is scoped by KNOWN-GAPS 14/15 — the leaf does not claim the deployed verifier is diff --git a/RESPONSE-TO-REVIEWERS.md b/RESPONSE-TO-REVIEWERS.md index 50c9cd8..02402d1 100644 --- a/RESPONSE-TO-REVIEWERS.md +++ b/RESPONSE-TO-REVIEWERS.md @@ -84,7 +84,9 @@ qualification. Every Lean file, the allowlist, the gate, the self-test, the fidelity pins (230,271 / 230,016 / 73,573 / 3,867), the axiom boundary, the -live log (12 leaves, `bcd15f9d…`), deployed pacta. Attestation remains -gated on the ePrint decision, the operator's read (A2), the rehearsal +live log (12 leaves, `bcd15f9d…`), deployed pacta. [Historical record, +round 5, July 2026 — the gated attestation has since occurred: leaf 12, +2026-07-16; hardened model re-attested as leaf 17, 2026-08-08.] +Attestation at that time remained gated on the ePrint decision, the operator's read (A2), the rehearsal (A4), and an explicit operator order — with the B2 scope wording now part of the gate.