saymrwulf/verifying-crypto-with-lean
1
0
Fork 0
mirror of https://github.com/saymrwulf/verifying-crypto-with-lean.git synced 2026-09-04 20:03:41 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

coherence sweep wave 3 (book): the paper is published, not frozen

Browse source 
Findings 13-16,26: ch14's 'frozen under journal review / thirteen-leaf
snapshot' paragraph now states the published truth (v0.15, DOI, live
nineteen-leaf deployment; July measurements byte-identical in history);
'additive' aligned to 'second, deterministic SLH-DSA signature'; the
private control repo's 404 link row removed from the public README;
claim count corrected to the gate's measured 96; publication history
carries the companion paper's DOI.
This commit is contained in:
mrwulf 2026-08-22 18:42:29 +02:00
parent f1cd701730
commit 0355ff22f3
4 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
README.md
View file

@ -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 | | [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 | | [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 | | [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 ## The book
@ -98,7 +97,7 @@ its claims — and it is the only source of the words "ALL GREEN" here:
./check-book.sh ./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 countable claims printed in the book against reality measured at run
time: chapter and week-plan counts, exercise↔solution pairing per chapter, time: chapter and week-plan counts, exercise↔solution pairing per chapter,
every chapter ending on its checkpoint, the recomputed SLH-DSA arithmetic every chapter ending on its checkpoint, the recomputed SLH-DSA arithmetic

9
chapters/ch14-attestation-protocol.tex
View file

@ -274,7 +274,7 @@ And leaf 18 is the second summit you climbed in
Chapter~\ref{ch:secondsummit} --- the eleven SLH-DSA certificates, the 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 cone-growth table, the see-saw: you can now read every field of that leaf
against a chapter of your own experience. 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 SLH-DSA signature beside the required Ed25519 one; heads published before
then have none, and the verifier reports them as \code{ABSENT} rather than 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 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 \emph{verification} and nothing about \emph{signing} --- the heads are
signed by unproven code and checkable by proven code, and every leaf names 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 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 them. Second: the estate's paper about this log is published (v0.15, August
review and describes the thirteen-leaf snapshot of July 2026. Nothing it 2026, DOI 10.5281/zenodo.22057482) and, since its August revisions,
describes was altered --- the paper-era leaves and heads sit byte-identical 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 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 run. A document that ages honestly inside a system that keeps moving is not
a defect; it is what append-only means. a defect; it is what append-only means.

BIN
main.pdf
View file

Binary file not shown.

4
main.tex
View file

@ -57,6 +57,10 @@ a proof assistant has checked.\par}
\noindent\textbf{Second edition} --- published August 8, 2026: fourteen \noindent\textbf{Second edition} --- published August 8, 2026: fourteen
chapters, 132 pages. chapters, 132 pages.
\smallskip
\noindent The estate's companion paper: DOI
\href{https://doi.org/10.5281/zenodo.22057482}{10.5281/zenodo.22057482}.
\medskip \medskip
\noindent\emph{Publication history} \noindent\emph{Publication history}
\begin{itemize}[leftmargin=1.4em] \begin{itemize}[leftmargin=1.4em]