diff --git a/README.md b/README.md index 6b95de6..b53979e 100644 --- a/README.md +++ b/README.md @@ -18,7 +18,6 @@ Lean 4 against models extracted from the actual Rust sources: | [risc0-ed25519-verified](https://github.com/saymrwulf/risc0-ed25519-verified) | the complete pyramid, RISC Zero's fork | | [betrusted-ed25519-verified](https://github.com/saymrwulf/betrusted-ed25519-verified) | the complete pyramid, Betrusted's fork | | [pasta-pallas-verified](https://github.com/saymrwulf/pasta-pallas-verified) | Pallas modulus primality (Lucas/Pratt), Montgomery foundations | -| [formal-verification-control](https://github.com/saymrwulf/formal-verification-control) | the method: invariants, terrain map, failure map, tooling | ## The book @@ -98,7 +97,7 @@ its claims — and it is the only source of the words "ALL GREEN" here: ./check-book.sh ``` -It rebuilds the PDF from the committed sources and then verifies ~90 +It rebuilds the PDF from the committed sources and then verifies 96 countable claims printed in the book against reality measured at run time: chapter and week-plan counts, exercise↔solution pairing per chapter, every chapter ending on its checkpoint, the recomputed SLH-DSA arithmetic diff --git a/chapters/ch14-attestation-protocol.tex b/chapters/ch14-attestation-protocol.tex index 79bd79c..32beb6f 100644 --- a/chapters/ch14-attestation-protocol.tex +++ b/chapters/ch14-attestation-protocol.tex @@ -274,7 +274,7 @@ And leaf 18 is the second summit you climbed in Chapter~\ref{ch:secondsummit} --- the eleven SLH-DSA certificates, the cone-growth table, the see-saw: you can now read every field of that leaf against a chapter of your own experience. -Since tree 14 every head also carries an \emph{additive} deterministic +Since tree 14 every head also carries a second, deterministic SLH-DSA signature beside the required Ed25519 one; heads published before then have none, and the verifier reports them as \code{ABSENT} rather than failing them --- an append-only log keeps its history, including the history @@ -285,9 +285,10 @@ read everything. First: for both signature algorithms the estate has proved \emph{verification} and nothing about \emph{signing} --- the heads are signed by unproven code and checkable by proven code, and every leaf names its trusted base; read a leaf's exclusions before believing anything beyond -them. Second: the estate's paper about this log is frozen under journal -review and describes the thirteen-leaf snapshot of July 2026. Nothing it -describes was altered --- the paper-era leaves and heads sit byte-identical +them. Second: the estate's paper about this log is published (v0.15, August +2026, DOI 10.5281/zenodo.22057482) and, since its August revisions, +describes the live nineteen-leaf deployment. Its July-era measurements +were never altered --- the paper-era leaves and heads sit byte-identical inside today's history, and \code{verify.py \ddash all} checks both eras in one run. A document that ages honestly inside a system that keeps moving is not a defect; it is what append-only means. diff --git a/main.pdf b/main.pdf index 2834b40..76aeab7 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.tex b/main.tex index 7ffc858..8678eb5 100644 --- a/main.tex +++ b/main.tex @@ -57,6 +57,10 @@ a proof assistant has checked.\par} \noindent\textbf{Second edition} --- published August 8, 2026: fourteen chapters, 132 pages. +\smallskip +\noindent The estate's companion paper: DOI +\href{https://doi.org/10.5281/zenodo.22057482}{10.5281/zenodo.22057482}. + \medskip \noindent\emph{Publication history} \begin{itemize}[leftmargin=1.4em]