print-quality pass: the book gets looked at, and the looking becomes a gate

The operator caught what no check had ever tested: nobody had LOOKED at
the rendered pages. A ten-inspector visual audit of all 129 pages (every
page opened as an image) found 40 defects, including didactic
correctness bugs invisible to the text layer:

BAD, fixed:
- ch03 printed WRONG Lean operators: \lean{P /\ Q} lost its backslash
  ('P / Q') and \lean{P \/ Q} lost the operator entirely ('P  Q') —
  TeX ate them inside the non-verbatim macro. Now the unicode ∧/∨ the
  book uses everywhere else.
- ch12: the doubling display overflowed its box border, slicing the
  math; stacked on two lines.
- toolkit Card 6: the headroom-audit display was clipped by the page
  edge; now an align* stack.

UGLY, fixed:
- title page: the 'pyramid motif' at 5% white opacity on near-black
  rendered as smudge artifacts, plus a clipped ∀ glyph in the corner
  — redrawn with solid mixed colors (no transparency), glyph removed;
  the footer's mid-word paragraph gap was a \vspace landing inside
  horizontal mode; fixed with \par
- ch06: both clock diagrams' wrap-around arrows ran counterclockwise,
  retracing over earlier arcs — target position expressed as 12 (one
  revolution) so the arc continues clockwise, landing on 0 (mod 12)
  and 1 (mod 11) correctly
- ch04: two_mul'' printed as two_mul" (quote ligature)
- one-line orphaned box fragments and stranded solution headings
  throughout: bigidea/tryit/pitfall/aha/checkpoint are now unbreakable
  (none exceeds half a page), worked boxes announce '(continued)' after
  a break, \solhead keeps four lines with \Needspace
- --all/--receipt flags printed as one merged dash: \ddash macro
- inline code no longer hyphen-breaks at underscores (codeguards)
- ch09's 2^{...} smudge, glossary margin overflow, ch08 orphaned
  listing line, ch13 command-line layout, three >10pt overfulls

THE STRUCTURAL LESSON, encoded: the two worst clipping bugs had been
announced as 80pt/73pt overfull warnings in every build log and ignored.
check-book.sh now FAILS on any overfull box past 10pt — the machine was
telling us; now it is allowed to stop us.

132 pages; publication-history and README counts synced; every fixed
page re-rendered and verified by eye. Button: ALL GREEN (96 checks).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

README.md

@@ -22,13 +22,12 @@ Lean 4 against models extracted from the actual Rust sources:
 
 ## The book
 
-**[`main.pdf`](main.pdf)** — thirteen chapters + interlude + three
+**[`main.pdf`](main.pdf)** — fourteen chapters + interlude + three
 appendices, full color, built with LaTeX/TikZ from the sources in this
-repo. **Honesty note:** the committed PDF (109 pages) was built 2026-07-06,
+repo (`./build.sh`, tectonic, no root needed). **Second edition,
-before chapter 13 was committed (2026-07-28) — rebuild with the command
+published August 8, 2026** (132 pages; the full publication history is
-below to get the current book; the committed PDF lags the committed
+printed in the book's front matter). No prior Lean or formal
-sources until the next rebuild on a LaTeX-equipped machine. No prior Lean or formal methods assumed; high-school algebra
+methods assumed; high-school algebra and a little programming suffice.
-and a little programming suffice.
 
 1. **Why Verify?** — the carry bug testing cannot find
 2. **Meet Lean** — programs, types, inductive data
@@ -43,11 +42,12 @@ and a little programming suffice.
 10. **Verifying a Field** — the full campaign, told honestly (including the crash)
 11. **Honesty and Axioms** — `#print axioms`, hollow certificates, trusted bases
 12. **The Pyramid** — group law, scalars, signatures, and where you come in
-13. **The Attestation Protocol** — what it takes to make "it is proven" checkable by a stranger
+13. **The Second Summit** — a hash-based pyramid for the quantum era: SLH-DSA (FIPS 205), Winternitz chains and the checksum see-saw, the virtual hypertree, the eleven certificates and their cone-growth table, and leaf 18 live
+14. **The Attestation Protocol** — what it takes to make "it is proven" checkable by a stranger; closes with *Go and touch the real thing*: a guided reading of the estate's **live transparency log** (ltl.zkdefi.org — 19 leaves, the four ed25519 pyramids at 44 certificates, the log's own Merkle proofs as leaf 17, and the first post-quantum leaf, SLH-DSA, as leaf 18), including the fifteen-minute verify-it-yourself exercise
 
 Appendices: **A** — the pen-and-paper toolkit (recipe cards with drills);
 **B** — guided walkthroughs of every exercise-file hole; **C** — a tour of
-the real repositories. Plus a glossary and a thirteen-week course plan.
+the real repositories. Plus a glossary and a fourteen-week course plan.
 
 The didactic machinery, deliberately heavy:
 
@@ -89,9 +89,40 @@ lake build Solutions   # compiles all solution files as a check
 Chapters 2–4 need no Mathlib at all — you can start them with any Lean 4
 install while the cache downloads.
 
+## The button
+
+Like every repository in this estate, the book has one command that earns
+its claims — and it is the only source of the words "ALL GREEN" here:
+
+```bash
+./check-book.sh
+```
+
+It rebuilds the PDF from the committed sources and then verifies ~90
+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
+(digest split, signature size, the 3,824-call worst case), the
+transparency log's 19 leaves and per-leaf certificate counts, leaf 18's
+axiom cones, the first dual-signed head at size 14, the extracted
+SLH-DSA-SHA2-128s parameter card, and chapter 7's 71-digit Q — digit for
+digit against `P25519.lean`. Numbers are parsed out of the prose and
+compared to measurements, so editing either side alone turns the button
+red. Cross-repo checks need the sibling estate repos checked out next to
+this one (`BOOK_LOCAL_ONLY=1` skips them, loudly, and never prints ALL
+GREEN). `./check-book.sh --selftest` mutates copies of the sources seven
+ways and proves each mutation is caught by its own check.
+
 ## Building the book
 
-Any TeX Live ≥ 2023 with `tikz`, `tcolorbox`, `listings`, `lmodern`:
+The repo's own recipe (tectonic, user-space, no root — installs itself on
+first run):
+
+```bash
+./build.sh
+```
+
+Or any TeX Live ≥ 2023 with `tikz`, `tcolorbox`, `listings`, `lmodern`:
 
 ```bash
 pdflatex main.tex && pdflatex main.tex   # twice for the TOC
@@ -122,12 +153,11 @@ In the spirit of Chapter 11:
   twice (mod-13 sign-bit walk, then the real compressed base point:
   byte-31 sign bit, and the full-size hand verification 5·y_B − 4 = 4·p,
   every digit printed), plus a new paper exercise (12.4). Every printed
-  constant was machine-verified before typesetting; the PDF (109 pages,
+  constant was machine-verified before typesetting.
-  2026-07-06 build — predates ch13) is rebuilt from these sources.
+- The PDF in the repo is built from the committed sources by `./build.sh`
-- The PDF in the repo is built from the committed sources by the command
+  and recommitted alongside source changes; rebuild it yourself if you
-  above — but the committed build currently predates chapter 13 (see the
+  don't trust binaries (good instinct), and you should get the same
-  honesty note at the top); rebuild it yourself if you don't trust binaries
+  fourteen-chapter book.
-  (good instinct), and you will get the thirteen-chapter book.
 - The three named solution certificates were kernel-audited
   (coherence pass 2, 2026-07-03): `Ch09.add_spec` depends on
   `[propext, Classical.choice, Quot.sound]`; `Ch09.mulVal_spec` and

build.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+# Build the book. No root, no TeX Live install: tectonic is a single
+# user-space binary that fetches packages on demand (first run is slow,
+# after that it's seconds). pdflatex also works (the preamble carries a
+# dual-engine unicode block); tectonic is what the repo's button uses.
+set -euo pipefail
+cd "$(dirname "$0")"
+TECTONIC="${TECTONIC:-$HOME/.local/bin/tectonic}"
+if [ ! -x "$TECTONIC" ] && command -v tectonic >/dev/null; then TECTONIC=tectonic; fi
+[ -x "$TECTONIC" ] || command -v "$TECTONIC" >/dev/null || {
+  echo "no tectonic. Install (no root):"
+  echo "  curl -sL https://github.com/tectonic-typesetting/tectonic/releases/download/tectonic%400.15.0/tectonic-0.15.0-x86_64-unknown-linux-musl.tar.gz | tar xz -C ~/.local/bin"
+  exit 1
+}
+"$TECTONIC" -X compile main.tex
+pdfinfo main.pdf 2>/dev/null | grep Pages || true

chapters/appendix-repo-tour.tex

@@ -2,8 +2,10 @@
 \label{app:tour}
 
 The companion projects are working code, laid out for auditors rather
-than tourists. This appendix is the tourist map: what lives where, what
+than tourists. This appendix is the tourist map, and it ends with three
-to read first, and how to run the machinery yourself. Everything below
+things done, not read: you will run the full verification yourself,
+\emph{sabotage a proof on purpose} and watch the machinery catch you,
+and finish at a stop that is not on your disk at all. Everything below
 names \code{dalek-ed25519-verified}; the other three ed25519 forks are
 structured identically, and \code{pasta-pallas-verified} differs only
 where Montgomery form demands it.
@@ -96,6 +98,22 @@ asserted. A fourth phase arrived with the signature layer: \emph{3b pins
 the apex tiers' cones to the documented hash/wire-format boundary
 EXACTLY} --- an unexpected addition \emph{or removal} fails the build.
 
+\begin{tryit}
+Now sabotage it. A green button proves nothing until you have seen it
+red for the right reason. In your local clone (nothing here leaves your
+machine, and \code{git} undoes it all): pick one digit of one constant
+in a \code{Proofs/} statement --- say, turn a $19$ into an $18$ in a
+bounds lemma --- and run \code{./verification/check.sh}. Watch which
+phase catches it and what the failure actually says. Then try to be
+sneakier: weaken a theorem's \emph{statement} instead of its proof, or
+plant an \lean{axiom} in a \code{Proofs/} file, and see the stub-audit
+phase refuse before the compiler even starts. Restore with
+\code{git checkout \ddash\ .} when done. Ten minutes of vandalism buys you
+something reading cannot: the difference between believing the button
+because it is green and believing it because you have personally failed
+to fool it.
+\end{tryit}
+
 \section{The control repository}
 
 \code{formal-verification-control} is the method distilled --- written
@@ -116,10 +134,26 @@ of these stories; the file has the rest, and reading failure maps
 before starting work is the cheapest experience money can't buy.
 \end{itemize}
 
+\section{The last stop is not on your disk}
+
+The repository you just toured does not only sit on your machine or on a
+code-hosting site; it is \emph{attested}. The public transparency log at
+\code{ltl.zkdefi.org} carries a leaf binding this repo's pinned commit to
+the certificate names, their statement fingerprints, and their observed
+axiom cones --- the very things your sabotage exercise just tried to
+fake locally, notarized globally. Find the leaf for
+\code{dalek-ed25519-verified}, and check that the commit it names is the
+one you have been reading. Chapter~\ref{ch:attestation} is the full
+protocol --- including the fifteen-minute exercise where a stranger (you)
+re-derives the log's Merkle root from nothing but published bytes. The
+tour ends here on purpose: floor plan, button, sabotage, control room,
+and finally the public record that makes the whole thing checkable by
+someone who has never met you.
+
 A closing observation to carry out of the tour: nothing in these
 repositories asks to be trusted. The claims are in the READMEs, the
 assumptions in the ledgers, the checks in a script anyone can run, the
-axioms in a one-command audit. That shape --- \emph{auditability as the
+axioms in a one-command audit, the whole ensemble in a public log. That
-default posture} --- is the real deliverable of the whole verification
+shape --- \emph{auditability as the default posture} --- is the real
-enterprise, and the standard this book hopes you now hold everything
+deliverable of the whole verification enterprise, and the standard this
-else to.
+book hopes you now hold everything else to.

chapters/appendix-toolkit.tex

@@ -1,11 +1,16 @@
 \chapter{The Pen-and-Paper Toolkit}
 \label{app:toolkit}
 
-Every worked example in this book leaned on a small set of hand-computation
+You are in a design review. A slide asserts that nine products of
-techniques. This appendix collects them as recipe cards --- the reference
+$31$-bit limbs accumulate in a $64$-bit word without overflow, the
-you will reach for when auditing numbers in the wild, where there is no
+presenter is already on the next slide, and everyone else is nodding.
-chapter telling you which trick applies. Each card ends with a
+You have perhaps forty seconds and no proof assistant. This appendix is
-thirty-second drill; answers close the appendix.
+for that room. Every worked example in this book leaned on a small set of
+hand-computation techniques; here they are as recipe cards --- the
+reference for auditing numbers in the wild, where no chapter title tells
+you which trick applies. Each card ends with a thirty-second drill;
+answers close the appendix. (The slide, by the way, is wrong --- Card~6
+and Drill~6 are the forty seconds that catch it.)
 
 \section{Card 1: powers of two into powers of ten}
 
@@ -86,12 +91,12 @@ which is itself a toolkit skill.
 \section{Card 6: the headroom audit}
 
 For any limb design, three lines locate the overflow cliff:
-\[
+\begin{align*}
-\text{headroom} = \text{word bits} - \text{radix bits}; \qquad
+\text{headroom} &= \text{word bits} - \text{radix bits};\\
-\text{add budget} = 2^{\text{headroom}}; \qquad
+\text{add budget} &= 2^{\text{headroom}};\\
-\text{mul check: } (\text{limb count}) \cdot 2^{2\cdot\text{bound bits}}
+\text{mul check: } &(\text{limb count}) \cdot 2^{2\cdot\text{bound bits}}
 \overset{?}{<} 2^{\text{wide word}} .
-\]
+\end{align*}
 Run all three whenever anyone shows you a limb representation ---
 Chapter~\ref{ch:why} (budget), Chapter~\ref{ch:automation} (mul check),
 and Chapter~\ref{ch:field}'s $16p$ audit are all instances.
@@ -126,6 +131,9 @@ $2^{255} \equiv 0 \pmod 4$, so $p \equiv -19 \equiv -3 \equiv
 \emph{Drill 7a.} Is $3$ a square mod $11$? ($3^5 \bmod 11$ by ladder;
 then find the root or trust the sign.)
 
+\emph{Drill 7b.} Is $-1$ a square mod $11$? No ladder allowed --- decide
+it by exponent parity alone, the way the card handled $p = 2^{255}-19$.
+
 \section{Card 8: the substitution test (specs)}
 
 Given a claimed specification: substitute the worst implementation of
@@ -178,9 +186,22 @@ lines of arithmetic as your citation.
 (ladder: $3^2 = 9$, $3^4 = 81 \equiv 4$, $3^5 = 4 \cdot 3 = 12 \equiv 1$)
 --- so $3$ \emph{is} a square mod $11$; indeed $5^2 = 25 \equiv 3$.
 
+\solhead{Drill 7b} $(-1)^{(11-1)/2} = (-1)^{5} = -1$: \emph{not} a
+square --- because $(11-1)/2 = 5$ is odd, i.e.\ $11 \equiv 3 \pmod 4$.
+Parity of one exponent, no arithmetic bigger than a division by two.
+
 \solhead{Drill 8} No. Substitute $\code{mul}_{c}(a,b) :=$ ``return the
 constant array $c$'': both sides become $\denote{c}$ --- the adversary
 passes. Commutativity-of-the-implementation is a \emph{symmetry} spec;
 symmetric garbage satisfies it. (Real correctness needs the other side
 of the square: $\denote{a} \cdot \denote{b}$, a quantity the
 implementation cannot influence.)
+
+\bigskip
+\noindent\emph{The street assignment.} These cards were built in a book,
+but they pay rent outside it. Sometime this week you will meet a number
+in the wild --- a README boasting ``$2^{128}$ operations to break,'' a
+blog post's limb bound, a slide with an accumulator width. Pick one and
+audit it with the cards, on paper, before you believe it. The first time
+you catch a real number being wrong in public, this appendix will have
+paid for the whole book.

chapters/appendix-walkthroughs.tex

@@ -1,13 +1,17 @@
 \chapter{Guided Walkthroughs of the Exercise Files}
 \label{app:walkthroughs}
 
-The \code{exercises/} folder contains eight Lean files with \lean{sorry}
+You are probably here because a hole has defeated you. Good --- this
-holes; \code{solutions/} contains their completed twins (every one
+appendix was written for exactly that moment, and it will not waste it
-compiled, with no \lean{sorry}, against the pinned toolchain). This
+by simply handing over answers. The \code{exercises/} folder contains
-appendix is the middle path between the two: for every hole, the
+the Lean files with \lean{sorry} holes; \code{solutions/} contains their
-\emph{pathway} --- what to look at, what to try, where you will
+completed twins, every one compiled, with no \lean{sorry}, against the
-probably get stuck and why --- and then the resolution. Use it when a
+pinned toolchain (\code{ls exercises/} is the authoritative roster ---
-hole has genuinely defeated you; the file order follows the book.
+trust the folder, not a number printed in a book). This appendix is the
+middle path between the two, at a fixed exchange rate of one hole, one
+paragraph: the \emph{pathway} --- what to look at, what to try, where
+you will probably get stuck and why --- and then the resolution. The
+file order follows the book.
 
 \section{Ch02.lean --- definitions by recursion}
 
@@ -38,7 +42,7 @@ constructor syntax \lean{⟨num, den⟩}; the type-level lesson (what
 \section{Ch03.lean --- term-mode logic}
 
 The file's discipline (no tactics) makes every hole a smallish program.
-The reliable procedure for all six: (1) unfold the connectives into
+The reliable procedure, for every hole in the file: (1) unfold the connectives into
 arrow/pair/tagged-union shape; (2) write \lean{fun} for every arrow in
 the goal; (3) inside, build the result with \lean{And.intro} /
 \lean{Or.inl} / \lean{Or.inr} / projections / application. Where people
@@ -136,8 +140,12 @@ addition must happen \emph{on the clock face}, not in \lean{Nat}).
 this proof on paper. Bounds clause: \lean{simp only [add]; omega}.
 Value clause --- the one genuine difficulty in the file --- state the
 exact integer identity with its correction term:
-\lean{have key : (add a b).1 + 4 * (add a b).2 + 15 * ((a.2 + b.2 +
+\begin{lstlisting}[language=Lean]
-(a.1 + b.1) / 4) / 4) = (a.1 + 4*a.2) + (b.1 + 4*b.2)}, discharge with
+have key : (add a b).1 + 4 * (add a b).2
+    + 15 * ((a.2 + b.2 + (a.1 + b.1) / 4) / 4)
+    = (a.1 + 4*a.2) + (b.1 + 4*b.2)
+\end{lstlisting}
+discharge it with
 \lean{simp only [add]; omega}, then cast
 (\lean{push_cast}), kill the modulus
 (\lean{rw [show (15 : ZMod 15) = 0 by decide]}), and close with
@@ -145,9 +153,9 @@ exact integer identity with its correction term:
 correction term is wrong --- recompute $c_2$ on paper (Interlude Step
 2); \lean{omega}'s refusal is, as always, a counterexample pointing at
 the boundary. \textbf{9.C \code{mulVal_spec}}: same cast-and-kill
-scaffold, but the integer identity is pure algebra ---
+scaffold, but the integer identity is pure algebra,
-\lean{mulVal a b + 15 * (a.2 * b.2) = (a.1 + 4*a.2) * (b.1 + 4*b.2)}
+\lean{mulVal a b + 15*(a.2*b.2) = (a.1 + 4*a.2)*(b.1 + 4*b.2)}
-by \lean{ring} --- and \emph{no bounds hypotheses are needed}, a fact
+by \lean{ring}, and \emph{no bounds hypotheses are needed} --- a fact
 worth noticing (denotation does not care about digit discipline; only
 machine words do).
 
@@ -174,6 +182,6 @@ actually wrote.
 all: the scalar layer that was open when this appendix was first written is
 now complete on all four companion forks (thirteen certificates each ---
 lemmas shaped exactly like 9.B, bigger constants, same bones). The open
-frontier today is the paused Pasta curve layer, and chapter 12's ``Extend
+frontier today is the paused Pasta curve layer, and chapter 12's ``Where
-the pyramid'' item points at it; the \code{CONTRIBUTING} notes there will
+you come in'' subsection points at it; the \code{CONTRIBUTING} notes there
-treat you as what you now are: someone who has done this before.
+will treat you as what you now are: someone who has done this before.

chapters/ch01-why-verify.tex

@@ -3,12 +3,23 @@
 
 \section{A story about one carry bit}
 
-In 2014, researchers examining widely deployed elliptic-curve code found
+Here is the entire bug that this book exists because of:
-arithmetic bugs of a very particular species: the code was correct on
+
-\emph{almost every} input. Not most inputs --- almost all of them, in a
+\begin{lstlisting}
-precise sense. One famous example, a carry-propagation flaw in an
+  h[4] += carry;              // propagate the top limb's overflow
-implementation of curve25519 arithmetic, produced a wrong answer with
+- // (missing: one more conditional subtraction of p)
-probability on the order of $2^{-64}$ per random input.
++ if (h[4] >= LIMB_CAP) h[4] -= LIMB_CAP, h[0] += 19;
+\end{lstlisting}
+
+\noindent One missing line. A field-arithmetic routine that forgets a single
+final carry is correct on \emph{almost every} input --- not most, almost
+\emph{all} of them, in a precise sense --- and silently wrong on the rare
+ones where that last carry would have fired. Bugs of exactly this species
+were found in deployed elliptic-curve code and became the motivating
+disaster behind a whole line of verification research (the Fiat-Cryptography
+project, Erbsen et al., IEEE S\&P 2019 --- a direct ancestor of the work this
+book teaches). A representative one produced a wrong answer with probability
+on the order of $2^{-64}$ per random input.
 
 Pause on that number. If you tested this function a billion times per second,
 around the clock, you should expect to wait \emph{centuries} before a random
@@ -24,41 +35,18 @@ than the square of the number of atoms in the observable universe. Testing
 samples a raindrop from that ocean.
 \end{pitfall}
 
-\begin{worked}{feel what $2^{-64}$ means, with the real numbers}
+\begin{worked}{feel what $2^{-64}$ means}
-Claims about astronomical improbability deserve to be checked by hand, so
+One hit per $2^{64}$ trials, and $2^{64} \approx 1.8 \times 10^{19}$. At a
-check this one. A failure probability of $2^{-64}$ per random input means
+billion tests a second that is $1.8 \times 10^{10}$ seconds to expect a
-you expect one hit per $2^{64}$ trials. First, get $2^{64}$ into scientific
+single failure --- about \textbf{580 years}. So a test farm hammering this
-notation the way you always can: $\log_{10} 2 \approx 0.30103$, so
+function a \emph{billion} times per second, started when Copernicus
-\[
+published, would be expected to see the bug for the first time about now.
-\log_{10} 2^{64} = 64 \times 0.30103 \approx 19.27
+And that is the \emph{optimistic} case: carry bugs cluster in exactly the
-\qquad\Longrightarrow\qquad
+corners uniform sampling underweights, so in practice you wait longer than
-2^{64} \approx 1.8 \times 10^{19}.
+the calendar of the universe. (The one-line $\log_{10}$ derivation behind
-\]
+``580 years,'' and the far more hopeless arithmetic for the full 510-bit
-At $10^9$ tests per second, the expected waiting time is
+space of input \emph{pairs}, are Exercise~1.1 --- worth doing, because the
-\[
+number that falls out has more digits than the universe has atoms.)
-\frac{1.8 \times 10^{19}}{10^{9}} = 1.8 \times 10^{10} \text{ seconds}.
-\]
-A year is $\approx 3.15 \times 10^{7}$ seconds (a number worth memorizing:
-``$\pi \times 10^7$ seconds per year'' is accidentally almost exact), so
-\[
-\frac{1.8 \times 10^{10}}{3.15 \times 10^{7}} \approx 580 \text{ years}.
-\]
-So: a test farm hammering this function a \emph{billion} times per second,
-started when Copernicus published, would be expected to see the bug for the
-first time about now. And this is the \emph{optimistic} case where failing
-inputs are hit by uniform sampling --- for carry bugs they are typically
-\emph{correlated}, clustered in corners uniform sampling underweights.
-
-Now the input space itself. A single \lean{FieldElement} is 255 bits; a
-pair is 510 bits, and
-\[
-\log_{10} 2^{510} = 510 \times 0.30103 \approx 153.5
-\qquad\Longrightarrow\qquad
-2^{510} \approx 10^{153}.
-\]
-For comparison, the number of atoms in the observable universe is around
-$10^{80}$. Testing all pairs is not ``hard''; it is not a thing that
-happens in this universe.
 \end{worked}
 
 Why does cryptographic code have bugs of exactly this shape? Because of how it
@@ -102,10 +90,12 @@ headroom count, and the headroom count is where the bodies were buried.
 \end{worked}
 
 And in cryptography, ``rare wrong answer'' does not mean ``rare small
-glitch.'' Wrong field arithmetic can leak private keys: several published
+glitch.'' Wrong field arithmetic can leak the private key itself: published
-attacks turn a single faulty group operation into full key recovery. The
+attacks in the ``invalid-curve'' and fault-injection families turn a
-stakes are not a corrupted pixel; they are every signature your machine has
+\emph{single} faulty group operation into full key recovery --- the attacker
-ever made.
+feeds inputs engineered to land in the buggy corner, and reads the secret
+off the wrong answers. The stakes are not a corrupted pixel; they are every
+signature your machine has ever made, and every one it ever will.
 
 \section{There is another way}
 
@@ -122,8 +112,10 @@ Every input, forever, or the proof does not check.
 
 The tool that checks such arguments is called a \emph{proof assistant}. This
 book uses \textbf{Lean~4}, a modern proof assistant that is also a
-full-fledged programming language. Others you may have heard of: Rocq
+full-fledged programming language.\footnote{You may have heard of Rocq
-(formerly Coq), Isabelle/HOL, Agda. The ideas transfer; the syntax differs.
+(formerly Coq), Isabelle/HOL, or Agda. The ideas in this book transfer to
+all of them; only the syntax differs. We pick Lean~4 for reasons that will
+be concrete by the end of this chapter.}
 
 A proof assistant is built around a small, paranoid core called the
 \emph{kernel}. Everything you will learn in this book --- clever tactics,
@@ -171,21 +163,33 @@ one abstraction level and rests on the layer beneath it:
 \end{tikzpicture}
 \end{center}
 
-By the end of this book you will be able to read --- and extend --- the real
+\begin{tryit}
-proofs at every layer of this pyramid. The journey looks like this:
+Before you read another word, go and touch the thing this book is about. Open
+\textbf{\code{ltl.zkdefi.org}} on any device. You are looking at a public,
+append-only log of machine-checked proofs --- 19 entries, each one a claim of
+the form ``this exact version of this software was verified, resting on
+exactly these assumptions.'' Entries 13--16 are the four Ed25519 libraries
+whose pyramid you see above. Entry~18 is the first \emph{post-quantum} entry
+in the log. You cannot read the proofs yet --- that is what the next thirteen
+chapters are for --- but you can already see that they are real, public, and
+checkable by a stranger with a stock laptop. That stranger is who you are
+becoming.
+\end{tryit}
 
-\begin{itemize}[leftmargin=1.4em]
+By the end of this book you will be able to read --- and extend --- the real
-\item \textbf{Chapters 2--5} teach Lean itself, from \code{\#eval 1+1} to
+proofs at every layer of this pyramid. To make that concrete, here is what
-  proofs by induction and the automation that dispatches arithmetic goals.
+you will personally be able to \emph{do}, and roughly when: by Chapter~7 you
-\item \textbf{Chapters 6--7} build the mathematics: modular arithmetic, finite
+will have handed a paranoid kernel a certificate that a 77-digit number is
-  fields, and how to convince a paranoid kernel that a 77-digit number is
+prime, and watched it agree; by Chapter~9 you will read real Rust translated
-  prime.
+into Lean and understand the one idea (the \emph{denotation function}) that
-\item \textbf{Chapters 8--9} cross the bridge from Rust to Lean: how real
+makes the translation trustworthy; by Chapter~12 you will stand on the apex
-  code is translated into a form we can reason about, and the single most
+and read the signature-verification theorem for the actual code in your SSH
-  important idea in the whole enterprise --- the \emph{denotation function}.
+client; by Chapter~13 you will climb a \emph{second} pyramid --- the
-\item \textbf{Chapters 10--12} assemble the pyramid: field correctness, the
+post-quantum entry you just saw in the log, built from hashes alone --- and
-  ethics of axioms and honest boundaries, and the layers above.
+by Chapter~14 you will verify the log itself, so that nothing in this story
-\end{itemize}
+asks for your trust. The chapters between here and there earn each of those,
+in order --- Lean itself first, then the mathematics, then the bridge from
+real code, then the climb.
 
 \begin{bigidea}
 \textbf{The ratchet rule of this book.} Every load-bearing idea is worked
@@ -239,20 +243,24 @@ Learning to smell those is as important as learning to write proofs at all.
 \section{Why Lean, and why now}
 
 Twenty years ago, verifying real cryptographic C or Rust code was a heroic,
-multi-year effort. Three things changed:
+multi-year effort. Three things changed --- and each one is an advantage
+\emph{you} inherit the moment you start:
 
 \begin{enumerate}[leftmargin=1.6em]
-\item \textbf{Proof assistants matured.} Lean~4 is fast, pleasant, and comes
+\item \textbf{You start on a million lines of proved mathematics.} Lean~4
-  with \emph{Mathlib}, a library of over a million lines of formalized
+  ships with \emph{Mathlib} --- finite fields, elliptic curves, number theory,
-  mathematics --- finite fields and elliptic-curve ingredients included, so we
+  already formalized and checked. You do not build the tower from bare axioms;
-  do not start from bare axioms.
+  you walk onto a finished floor and add one room.
-\item \textbf{Translation pipelines appeared.} Tools like \emph{Charon} and
+\item \textbf{You verify the code that ships, not a story about it.} Tools
-  \emph{Aeneas} mechanically translate real Rust code into Lean definitions,
+  called \emph{Charon} and \emph{Aeneas} mechanically translate real Rust into
-  so the thing we verify is derived from the code that ships, not a
+  Lean, so what you reason about is \emph{derived} from the deployed source
-  hand-transcribed approximation (Chapter~\ref{ch:rust}).
+  rather than hand-copied by someone who might have copied it wrong
-\item \textbf{Automation got serious.} Decision procedures like \lean{omega}
+  (Chapter~\ref{ch:rust}). This is the difference between verifying software
-  (linear integer arithmetic) and \lean{decide} discharge the boring 90\% of
+  and verifying an essay about software.
-  goals, leaving humans the interesting 10\%.
+\item \textbf{The machine does the boring 90\%.} Decision procedures like
+  \lean{omega} and \lean{decide} dispatch the routine arithmetic goals on
+  their own, so your attention goes to the 10\% that is actually interesting
+  --- the part where the real idea lives.
 \end{enumerate}
 
 None of this made verification \emph{easy}. It made verification

chapters/ch03-propositions-as-types.tex

@@ -35,8 +35,8 @@ Chapter~\ref{ch:lean} \emph{is} the proof checker.
 proposition $P$        & type            & \lean{P : Prop} \\
 proof of $P$           & value/program of that type & \lean{h : P} \\
 $P \to Q$ (implication)& function type   & \lean{P -> Q} \\
-$P \land Q$ (and)      & pair type       & \lean{P /\ Q} \\
+$P \land Q$ (and)      & pair type       & \lean{P ∧ Q} \\
-$P \lor Q$ (or)        & tagged union    & \lean{P \/ Q} \\
+$P \lor Q$ (or)        & tagged union    & \lean{P ∨ Q} \\
 $\lnot P$ (not)        & \lean{P -> False} & \lean{Not P} \\
 ``true''               & type with one trivial value & \lean{True} \\
 ``false''              & \emph{empty} type & \lean{False} \\
@@ -246,8 +246,9 @@ structure of $n$, induction (Chapter~\ref{ch:tactics}) is how a recipe
 consults structure.
 \end{worked}
 
-Dually, \lean{exists n, P n} is proved by handing over a concrete witness
+Dually, \lean{exists n, P n} is proved by handing over a concrete
-together with evidence: \lean{Exists.intro 4 pf}. And remember the
+witness together with the evidence for it: \lean{Exists.intro 4 pf}.
+And remember the
 \lean{Rational} exercise from last chapter --- the denominator you could not
 keep nonzero? Dependent types fix it by letting data carry proofs:
 
@@ -279,17 +280,17 @@ coffee.
 
 \begin{tryit}
 Open \code{exercises/Ch03.lean} and prove, as programs (no tactics yet!):
-\lean{P -> Q -> P}; \ \lean{(P /\ Q) -> (P \/ Q)}; \ and modus ponens
+\lean{P -> Q -> P}; \ \lean{(P ∧ Q) -> (P ∨ Q)}; \ and modus ponens
 \lean{P -> (P -> Q) -> Q}. Each is a one-liner. Feel free to be delighted
 when the pieces click together like typed Lego.
 \end{tryit}
 
 \section*{Exercises}
 
-\exercise{Prove \lean{and_assoc : (P /\ Q) /\ R -> P /\ (Q /\ R)} as a
+\exercise{Prove \lean{and_assoc : (P ∧ Q) ∧ R -> P ∧ (Q ∧ R)} as a
 term-mode program using \lean{h.1}, \lean{h.2}, and \lean{And.intro}.}
 
-\exercise{Prove \lean{or_swap : P \/ Q -> Q \/ P}. You will need case
+\exercise{Prove \lean{or_swap : P ∨ Q -> Q ∨ P}. You will need case
 analysis on which side holds: \lean{match h with | Or.inl p => ... | Or.inr q => ...}}
 
 \exercise{\lean{Not P} is \emph{defined} as \lean{P -> False}. Using only

chapters/ch04-tactics.tex

@@ -3,9 +3,11 @@
 
 \section{From programs to conversations}
 
-Writing proofs as raw programs, as in Chapter~\ref{ch:pat}, is honest work,
+Here is the problem with everything you learned in the last chapter: a real
-but it scales badly: a real correctness proof for field multiplication would
+correctness proof for field multiplication --- the theorem this book is
-be a program the size of a small compiler. Nobody writes those by hand.
+climbing toward --- would, written as a raw proof program, be a program the
+size of a small compiler. Nobody writes those by hand. (Chapter~\ref{ch:pat}'s
+handcrafted terms were honest work; honest work does not scale.)
 Instead, Lean offers \emph{tactic mode}: an interactive dialogue where you
 issue commands and Lean builds the proof program for you, step by step,
 showing you the remaining work after each move.
@@ -171,6 +173,13 @@ structure \emph{is} the induction. Data and proof principle are two views of
 the same declaration. This is Curry--Howard paying rent again.
 \end{aha}
 
+\section{When you get stuck --- and you will}
+
+No chapter on tactics is honest without this section. The steady march of
+examples above is what proving looks like \emph{afterwards}, cleaned up for
+print. What it looks like \emph{during} is the next box --- and the
+discipline it teaches is worth more than any tactic in the table.
+
 \begin{worked}{a debugging session, reconstructed honestly}
 Here is a stuck proof, exactly as it happens to everyone, worked
 through with the discipline this chapter preaches. Goal: every number
@@ -368,8 +377,9 @@ theorem two_mul' (n : Nat) : 2 * n = n + n := by
   | zero      => rfl
   | succ k ih => rw [Nat.mul_succ, ih, Nat.succ_add, Nat.add_succ]
 \end{lstlisting}
-Library: \lean{exact?} finds \lean{Nat.two_mul}, so
+Library: \lean{exact?} finds \lean{Nat.two_mul}, giving
-\lean{theorem two_mul'' (n : Nat) : 2 * n = n + n := Nat.two_mul n}. Both
+\lean{theorem two_mul\textquotesingle\textquotesingle\ (n : Nat) : 2 * n = n + n}
+proved by \lean{Nat.two_mul n}. Both
 are legitimate craft: the first when you are building the ecosystem, the
 second when you are using it. Mathlib has over 200{,}000 lemmas ---
 searching \emph{is} a proof technique, and \lean{exact?} is its tactic.
@@ -392,5 +402,9 @@ You should now be able to: read a goal state (context, turnstile, goal);
 drive the core tactics \lean{intro}, \lean{exact}, \lean{apply},
 \lean{cases}, \lean{rw}, \lean{induction}; structure a multi-step argument
 with \lean{have} and \lean{calc}; and --- most importantly --- when stuck,
-interrogate the \emph{statement} before blaming the proof.
+interrogate the \emph{statement} before blaming the proof. One goal from the
+exercises is deliberately still open: the bound
+$a \cdot 19 < 2^{56}$, which no tactic in this chapter's table owns. Carry it
+with you --- the next chapter opens by handing you the tactic that eats it in
+one line.
 \end{checkpoint}

chapters/ch06-modular-arithmetic.tex

@@ -3,10 +3,17 @@
 
 \section{Clock arithmetic, taken seriously}
 
-You already compute modulo twelve every day: four hours after ten o'clock is
+A dare, to open: before this chapter ends you will compute --- by hand, on
-two o'clock. Wrap-around arithmetic --- add, overflow the dial, keep the
+paper --- the exact multiplicative inverse of $19$ modulo a $77$-digit prime,
-remainder --- is the entire idea of \emph{modular arithmetic}. Cryptography's
+and no number you write down will be longer than two digits. Professional
-only twist is the size of the clock: Ed25519's dial has
+cryptographers do this calculation's industrial cousin billions of times a
+second; you will do it once, slowly, and own it.
+
+The number system that makes the dare possible is one you already use daily:
+four hours after ten o'clock is two o'clock. Wrap-around arithmetic --- add,
+overflow the dial, keep the remainder --- is the entire idea of
+\emph{modular arithmetic}. Cryptography's only twist is the size of the
+clock: Ed25519's dial has
 \[
 p = 2^{255} - 19
 \]
@@ -60,7 +67,7 @@ is the entry ticket to division.
   \begin{scope}
     \draw[ink2,thick] (0,0) circle (2.2);
     \foreach \i in {0,...,11} \node[color=ink] at ({90-\i*30}:1.8) {\i};
-    \foreach \s/\t in {0/4, 4/8, 8/0}
+    \foreach \s/\t in {0/4, 4/8, 8/12}
       \draw[-{Stealth},accent,thick] ({90-\s*30}:2.55) arc ({90-\s*30}:{90-\t*30+8}:2.55);
     \node[color=accent,align=center] at (0,-3.4) {$\Zmod{12}$: stepping by $4$\\ visits only $\{0,4,8\}$ --- never $1$};
   \end{scope}
@@ -68,7 +75,7 @@ is the entry ticket to division.
   \begin{scope}[xshift=9.5cm]
     \draw[ink2,thick] (0,0) circle (2.2);
     \foreach \i in {0,...,10} \node[color=ink] at ({90-\i*32.72}:1.8) {\i};
-    \foreach \s/\t in {0/4, 4/8, 8/1}
+    \foreach \s/\t in {0/4, 4/8, 8/12}
       \draw[-{Stealth},proven,thick] ({90-\s*32.72}:2.55) arc ({90-\s*32.72}:{90-\t*32.72+8}:2.55);
     \node[color=proven,align=center] at (0,-3.4) {$\Zmod{11}$: stepping by $4$\\ reaches $1$ in three steps: $4^{-1}=3$};
   \end{scope}
@@ -131,6 +138,18 @@ couple hundred multiplications of overhead for silence; you will meet
 this trade at every layer of the pyramid.
 \end{worked}
 
+\begin{tryit}
+That was the dare from the chapter's first paragraph, delivered. Now let a
+machine referee your paper. In a scratch Lean file:
+\begin{lstlisting}[language=Lean]
+def p : Nat := 2^255 - 19
+#eval (19 * (3 + 7 * ((p - 8) / 19))) % p   -- 1
+\end{lstlisting}
+If it prints \lean{1}, your five hand divisions just controlled a
+computation over 77-digit numbers. That feeling --- small paper steps,
+machine-confirmed at full scale --- is the entire working style of this book.
+\end{tryit}
+
 \section{\texorpdfstring{Why $2^{255}-19$?}{Why 2**255-19?} A prime chosen for machines}
 
 Any large prime makes a field. Why this one? Because arithmetic mod $p$ is
@@ -406,5 +425,10 @@ You should now be able to: compute in $\Zmod{n}$ and explain the notation;
 state exactly when division works and why primality guarantees it; give two
 independent reasons the constant $19$ appears throughout curve25519
 codebases; and prove small modular facts in Lean with \lean{decide},
-\lean{ring}, and a Mathlib lemma found by name.
+\lean{ring}, and a Mathlib lemma found by name. And you should be able to
+say, in one sentence, why real code pays $254$ squarings for an inverse that
+Euclid finds in five divisions: \emph{the expensive route runs in the same
+time for every input, and silence about secrets is worth two hundred
+multiplications}. That sentence is your first piece of cryptographic
+engineering judgment.
 \end{checkpoint}

chapters/ch07-primality-certificates.tex

@@ -52,8 +52,13 @@ Concretely for our hero: $p - 1 = 2^{255} - 20$ factors as
 \[
 p - 1 \;=\; 2^{2} \cdot 3 \cdot 65147 \cdot Q,
 \]
-where $Q$ is a 71-digit prime with its own (short) certificate, and
+where $Q$ is the 71-digit prime
-$65147$ recurses one more level: $65146 = 2 \cdot 32573$ with $32573$
+\[
+Q = 740582127325613583022312264370627886761\allowbreak 66966415465897661863160754340907,
+\]
+printed here in full --- no hidden digits, this is the exact value in the
+repository's \code{P25519.lean} --- carrying its own (short) certificate,
+and $65147$ recurses one more level: $65146 = 2 \cdot 32573$ with $32573$
 prime. The full certificate for $p$ is a small tree of witnesses and
 factorizations --- a few hundred bytes of data standing behind a 77-digit
 claim:

chapters/ch08-rust-to-lean.tex

@@ -103,11 +103,13 @@ returns a \lean{Result} that is an error unless the mathematical sum fits.
 So the innocent theorem ``add returns the right field element'' \emph{cannot
 even be stated} without first proving \emph{add returns at all}:
 
+\noindent\begin{minipage}{\linewidth}
 \begin{lstlisting}[language=Lean]
 theorem add_spec (a b : Array U64 5)
     (ha : LimbsBounded a) (hb : LimbsBounded b) :
     ∃ c, fieldElement51_add a b = .ok c ∧ LimbsBounded c ∧ ...
 \end{lstlisting}
+\end{minipage}
 
 That hypothesis \lean{LimbsBounded} --- each limb below $2^{54}$, say --- is
 the bounds invariant promised in Chapters~\ref{ch:pat}

chapters/ch09-denotation-bridge.tex

@@ -69,7 +69,7 @@ diagram, instantiated.
 \section{Why redundancy is freedom (and where bugs hide)}
 
 A subtlety with consequences: denotation is \textbf{many-to-one}. The limb
-arrays $(19, 0, 0, 0, 0)$ and $(p + 19 \bmod 2^{\cdots}, \dots)$ --- or more
+arrays $(19, 0, 0, 0, 0)$ and $(19 + (2^{51}-19),\; 2^{51}-1,\; \dots)$ --- i.e.\ $p$ itself added limb-wise --- --- or more
 mundanely, unreduced sums whose limbs exceed $2^{51}$ --- can denote the
 \emph{same} field element. The representation has slack, and the
 implementation \emph{exploits} it: the fast \code{add} from

chapters/ch10-verifying-a-field.tex

@@ -1,6 +1,14 @@
 \chapter{Verifying a Field: The Full Campaign}
 \label{ch:field}
 
+Partway through the campaign this chapter narrates, one proof step consumed
+twelve gigabytes of memory and took the machine down --- not a slow test, not
+a warning in a log: the computer proving these theorems crashed, mid-proof,
+because of how a proof was written. This chapter climbs toward that wall,
+hits it, quantifies exactly why it stands where it stands, and comes out the
+other side with the discipline the rest of the book runs on. The crash is
+the most instructive thing in the chapter. Keep it in view.
+
 \section{The summit statement}
 
 Every thread so far --- specs as types, tactics, automation, $\Fp$,
@@ -22,6 +30,11 @@ theorem fieldImplementation :
   ∧ ...                                       -- reduce, negate, encode
 \end{lstlisting}
 
+(Vocabulary re-armed, from Chapter~\ref{ch:denotation}: \lean{Bnd a} says
+$a$'s limbs sit inside their envelopes; each \lean{...Square} says one
+operation's commuting square closes --- run the extracted code, denote the
+result, and you get the same field element as doing the mathematics.)
+
 One theorem, kernel-checked, quantified over \emph{every} input the
 representation admits: the extracted dalek field arithmetic implements
 $\Fp$. This chapter is the story of the campaign that proves it --- told
@@ -98,6 +111,21 @@ is a patched CVE. Now you know how to tell which side of that line a
 codebase is on.
 \end{worked}
 
+\begin{tryit}
+Do not take the box's word for the margin of $151$ --- falsify the rejected
+design yourself:
+\begin{lstlisting}[language=Lean]
+#eval (8 * (2^51 - 19) : Int) - (2^54 - 1)    -- -151
+#eval (16 * (2^51 - 19) : Int) - (2^54 - 1)   -- 18014398509481681
+\end{lstlisting}
+The first line is the deficit a $k=8$ subtraction suffers when a limb of $b$
+sits within $151$ of its envelope's top: in unsigned words that negative
+number is a silent wrap-around --- and a random test hits the triggering
+region with probability about $151/2^{54}$, which is to say never. The
+second line is the shipped design's headroom. Two \lean{\#eval}s, one
+CVE-class distinction.
+\end{tryit}
+
 \begin{worked}{verifying the inversion chain's bookkeeping --- all 265 steps}
 Step 6 sounds heroic --- verify a hand-crafted chain of $254$ squarings
 and $11$ multiplications computes $a^{p-2}$ --- until you see that the
@@ -147,14 +175,15 @@ undergraduate audits over coffee.
 
 \section{Dispatches from the terrain}
 
-\textbf{The wall that was really there.} Partway up, one proof style hit a
+\textbf{The wall that was really there.} This is the crash from the
-genuine limit of the tool: correctness certificates for \code{mul}-scale
+chapter's first sentence, and here is exactly how it was earned: a
-goals, when handed to a general decision procedure in one monolithic call,
+\code{mul}-scale goal, handed to a general decision procedure in one
-generate internal certificates with coefficients on the order of $2^{256}$
+monolithic call --- the natural move, the move you would make ---
---- and checking them can exhaust the proof checker's memory. One such call,
+generates an internal certificate with coefficients on the order of
-during the development of the Pasta field proofs, consumed twelve gigabytes
+$2^{256}$, and checking it can exhaust the proof checker's memory. During
-and crashed the machine (Chapter~\ref{ch:automation} told you this story
+the development of the Pasta field proofs that one call ate twelve
-from the tactic side). The cure was never cleverness --- it was
+gigabytes and took the machine down (Chapter~\ref{ch:automation} told you
+this story from the tactic side). The cure was never cleverness --- it was
 \emph{decomposition}: isolate each carry step as its own small lemma with a
 tiny context, prove the value identity with \lean{linear_combination}
 (a tactic that checks a \emph{stated} linear certificate rather than
@@ -208,7 +237,8 @@ good fast code turn out to obey the same engineering aesthetics. This is not
 a coincidence; both are fighting combinatorial growth with structure.
 \end{aha}
 
-\textbf{Four forks, one method, real divergence.} The companion projects
+\Needspace{4\baselineskip}
+\noindent\textbf{Four forks, one method, real divergence.} The companion projects
 verify not just upstream \code{curve25519-dalek} but three production forks
 (Solana's, RISC~Zero's, Betrusted's) --- each against \emph{its own}
 extraction. Worth it? The audit found the forks implement the same
@@ -340,6 +370,14 @@ if the optimizer wrote a second path, the verifier owes a second
 theorem}. (This is also exactly why the four forks each got their own
 proofs: same math, four instruction streams.)
 
+One last thing, so the summit does not feel abstract: the certificate this
+chapter taught you to state is not a textbook artifact. It lives in four
+public repositories --- one per fork --- where \code{check.sh} rebuilds it
+from scratch on demand, and each of those repositories is attested as a
+leaf of the live transparency log at \code{ltl.zkdefi.org}. When you audit
+one with the four questions above, you are not doing an exercise; you are
+doing the thing.
+
 \begin{checkpoint}
 You should now be able to: state the field implementation certificate and
 every quantifier in it; recite the campaign order and justify why bounds

chapters/ch12-the-pyramid.tex

@@ -4,10 +4,11 @@
 \section{The view from the field layer}
 
 Chapter~\ref{ch:field} left us holding a verified field. A signature scheme
-is still three stories up. This closing chapter walks the remaining layers
+is still three stories up. This chapter climbs them --- what each layer
---- what each one \emph{states}, what makes each one \emph{hard}, and where
+\emph{states}, what makes each one \emph{hard}, and where the campaign
-the campaign stands as this book goes to press --- then hands you the map
+stands as this book goes to press --- then hands you the map and the keys.
-and the keys.
+The floors above the field enter this chapter as question marks; by the last
+section you will know precisely which of them are theorems.
 
 \begin{center}
 \begin{tikzpicture}[
@@ -19,9 +20,9 @@ and the keys.
   \node[lay,fill=provensoft,minimum width=7.8cm]  (grp) at (0,1.25) {\textbf{Group law}};
   \node[lay,fill=codebg,minimum width=10.2cm]     (fld) at (0,0)    {\textbf{Field $\Fp$}};
   \node[st] at (5.7,0)    {\textbf{done}: certificates in 4 repos, axiom-clean};
-  \node[st] at (5.7,1.25) {\textbf{done}: complete addition, all 4 forks};
+  \node[st] at (5.7,1.25) {\textbf{?} --- this chapter, second section};
-  \node[st] at (5.7,2.5)  {\textbf{done}: add, sub, Montgomery mul\\ certified, all 4 forks};
+  \node[st] at (5.7,2.5)  {\textbf{?} --- third section};
-  \node[st] at (5.7,3.75) {\textbf{done}: accept $\Leftrightarrow$ decompress$(R) = [k](-A){+}[s]B$;\\ hash an opaque oracle by design};
+  \node[st] at (5.7,3.75) {\textbf{?} --- the apex section};
 \end{tikzpicture}
 \end{center}
 
@@ -62,7 +63,8 @@ Then
 \[
 x_3 \;=\; \frac{2xy}{1 + 11} \;=\; \frac{16}{12} \;\equiv\; 3 \cdot 12^{-1}
 \;=\; 3\cdot 12 \;=\; 36 \;\equiv\; 10,
-\qquad
+\]
+\[
 y_3 \;=\; \frac{y^2\!+\!x^2}{1 - 11} \;=\; \frac{20}{3} \;\equiv\; 7\cdot 3^{-1}
 \;=\; 7 \cdot 9 \;=\; 63 \;\equiv\; 11
 \]
@@ -74,10 +76,10 @@ want it.
 
 \emph{Run 2 --- the real base point, full digits.} The same doubling, on
 Ed25519's base point $B = (x_1, y_1)$:
-\par\noindent{\footnotesize $x_1 \;=$}\\[-2pt]
+\par\noindent{\footnotesize $x_1 \;=$}\\[1pt]
 {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}15\,11222\,13495\,35400\,77250\,11514\,09588\,53151\,14540\\
 12693\,04185\,72060\,46113\,28394\,98477\,62202\end{tabular}}\par\smallskip
-\par\noindent{\footnotesize $y_1 \;=$}\\[-2pt]
+\par\noindent{\footnotesize $y_1 \;=$}\\[1pt]
 {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}46\,31683\,56949\,26478\,16942\,83940\,03475\,16314\,13079\\
 93866\,25622\,56157\,83033\,60316\,52518\,55960\end{tabular}}\par\smallskip
 The machine's first step is the product $u = x_1 y_1 \bmod p$. Nobody
@@ -87,10 +89,10 @@ remainder $u$ it claims, turning the step into one integer equation
 \[
 x_1 \cdot y_1 \;=\; q \cdot p + u ,
 \]
-\par\noindent{\footnotesize $q \;=$}\\[-2pt]
+\par\noindent{\footnotesize $q \;=$}\\[1pt]
 {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}12\,08977\,70796\,28320\,61800\,09211\,27670\,82520\,91632\\
 10154\,43348\,57648\,36890\,62715\,98782\,09761\end{tabular}}\par\smallskip
-\par\noindent{\footnotesize $u \;=$}\\[-2pt]
+\par\noindent{\footnotesize $u \;=$}\\[1pt]
 {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}46\,82740\,38508\,23179\,24507\,22166\,30277\,19756\,51442\\
 05554\,12565\,49766\,74165\,82953\,38171\,01731\end{tabular}}\par\smallskip
 which Chapter~\ref{ch:modular}'s shadow arithmetic audits on two
@@ -104,10 +106,10 @@ each is two careful minutes over the blocks printed above; that labor
 \emph{is} the pen-and-paper content at this size. Five more certified
 steps of exactly this shape (square, multiply by $d$, the two inversions
 via Fermat chains) complete the doubling, landing on
-\par\noindent{\footnotesize $x_{2B} =$}\\[-2pt]
+\par\noindent{\footnotesize $x_{2B} =$}\\[1pt]
 {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}24\,72741\,32351\,06541\,00255\,45745\,71675\,58883\,46227\\
 68167\,39763\,84567\,26423\,68252\,12336\,08206\end{tabular}}\par\smallskip
-\par\noindent{\footnotesize $y_{2B} =$}\\[-2pt]
+\par\noindent{\footnotesize $y_{2B} =$}\\[1pt]
 {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}15\,54967\,55802\,80190\,17635\,26687\,10449\,54225\,15495\\
 72066\,44506\,05805\,07079\,59306\,26430\,49417\end{tabular}}\par\smallskip
 --- the coordinates of $2B$ that every Ed25519 stack on earth agrees on.
@@ -182,7 +184,8 @@ $(X:Y:Z:T) \mapsto (X/Z, Y/Z)$, and its own commuting squares built on the
 field layer's specs. Same movie, one floor up: the verified group law in the
 companion repos is precisely the statement that projective point addition
 implements the rational formula above, all bounds included, for each fork's
-own extraction.
+own extraction. First question mark from the opening figure, resolved:
+\textbf{group law --- done, complete addition, all four forks.}
 
 \section{Scalars: a second field, and a frontier}
 
@@ -250,17 +253,25 @@ $sB = R + kA$ is not. Three multiplications by $8$, bought by exactly the
 three-line computation above.
 \end{worked}
 
-The engineering met a wall here, and this book has told you enough truth
+The engineering met a wall here, and you have earned the exact
-to locate it precisely --- and to appreciate how it fell. Scalar Montgomery
+coordinates. Picture the session: the Montgomery multiplication square is
-multiplication mixes $2^{256}$-scale coefficients into single certificate
+stated, the strategy that conquered the field layer is deployed, and the
-steps; this is the kernel-capacity wall of Chapter~\ref{ch:field}, and for
+checker simply --- does not come back. Not an error message; a machine
-a while it marked the campaign's working edge. It was crossed the way the
+grinding toward the memory ceiling of Chapter~\ref{ch:field}, because
-method file predicts: re-decompose until every heavy identity is an
+scalar Montgomery multiplication mixes $2^{256}$-scale coefficients into
-isolated, context-free lemma the kernel checks alone --- exact-division
+single certificate steps, and no amount of waiting fixes arithmetic that
-Montgomery rounds, a double round through $RR \equiv R^2$ --- and the
+does not fit. For a while this wall \emph{was} the campaign's working
-layer is now \emph{complete on all four forks}: add, sub, and Montgomery
+edge --- the honest label on the map read ``frontier,'' and it stayed
-multiplication certified (including the pleasing theorem that the code's
+there for weeks. It fell the way the method file predicts, not by a
-constant \code{L} \emph{is} $\ell$, digit for digit).
+bigger machine but by smaller lemmas: re-decompose until every heavy
+identity is an isolated, context-free lemma the kernel checks alone ---
+exact-division Montgomery rounds, a double round through
+$RR \equiv R^2$ --- and the layer is now \emph{complete on all four
+forks}: add, sub, and Montgomery multiplication certified (including the
+pleasing theorem that the code's constant \code{L} \emph{is} $\ell$,
+digit for digit). Second question mark, resolved: \textbf{scalars ---
+done, add, sub, Montgomery mul certified, all four forks.} One floor to
+go.
 
 \section{The apex: what ``verified signature'' says}
 
@@ -319,7 +330,7 @@ little-endian):
 bytes, nothing elided).
 Byte 31 is $\code{0x66} = 01100110_2$: its top bit is $0$, so the sign
 bit says ``$x$ even.'' The remaining 255 bits, read little-endian, are
-\par\noindent{\footnotesize $y_B \;=$}\\[-2pt]
+\par\noindent{\footnotesize $y_B \;=$}\\[1pt]
 {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}46\,31683\,56949\,26478\,16942\,83940\,03475\,16314\,13079\\
 93866\,25622\,56157\,83033\,60316\,52518\,55960\end{tabular}}\par\smallskip
 The design claim behind this constant: $y_B = 4/5$ in $\Fp$, i.e.\
@@ -330,10 +341,10 @@ $5\,y_B \equiv 4 \pmod p$. At full size that is one integer equation,
 and this one you can verify with \emph{no} shortcuts and \emph{no}
 witnesses: multiply $y_B$ by $5$ yourself (one right-to-left carry pass),
 multiply $p$ by $4$, subtract $4$, compare every digit:
-\par\noindent{\footnotesize $5\,y_B - 4 \;=$}\\[-2pt]
+\par\noindent{\footnotesize $5\,y_B - 4 \;=$}\\[1pt]
 {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}231\,58417\,84746\,32390\,84714\,19700\,17375\,81570\,65399\\
 69331\,28112\,80789\,15168\,01582\,62592\,79796\end{tabular}}\par\smallskip
-\par\noindent{\footnotesize $4\,p \;=\;\;\;\;\;\;\;$}\\[-2pt]
+\par\noindent{\footnotesize $4\,p \;=\;\;\;\;\;\;\;$}\\[1pt]
 {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}231\,58417\,84746\,32390\,84714\,19700\,17375\,81570\,65399\\
 69331\,28112\,80789\,15168\,01582\,62592\,79796\end{tabular}}\par\smallskip
 An honest fifteen minutes, and you have hand-checked a constant that
@@ -362,9 +373,12 @@ cone deviates from that documented boundary by a single axiom.
 Read that again with Chapter~\ref{ch:honesty} eyes: it is a
 \emph{smaller} claim than ``Ed25519 is verified!'' --- nothing about the
 hash, nothing about signing, nothing about side channels --- and that is
-exactly why you can believe it.
+exactly why you can believe it. And with that, the last question mark
+falls: \textbf{apex --- done, accept $\Leftrightarrow$
+decompress$(R) = [k](-A)+[s]B$, hash an opaque oracle by design.} The
+opening figure is now all theorems, floor to peak, on all four forks.
 
-\section{What you now know, and where to take it}
+\section{What you now know}
 
 Take inventory. You can read a goal state and drive a proof; you know which
 decision procedure owns which arithmetic fragment; you can build a
@@ -372,73 +386,23 @@ denotation bridge and state a two-clause spec; you can certify a prime with
 a witness tree; you can audit anyone's certificate in one command and four
 questions. That skill set is not Ed25519-specific --- it is the working
 method of machine-checked mathematics applied to systems, and elliptic
-curves were merely your first campaign.
+curves were merely your first campaign. The next chapter takes that claim
+literally: same method, a second summit, and not one line of algebra on it.
 
-Where to go from here, in increasing order of ambition:
+\subsection*{Where you come in}
 
-\begin{itemize}[leftmargin=1.4em]
+The chapter title made a promise, and here it is, kept without
-\item \textbf{Read a real proof end-to-end.} \code{FieldSpec.lean} in
+condescension: there is open, real work on this pyramid sized for the
-  \code{dalek-ed25519-verified}, top to bottom, with this book as the
+person who finished this book. The ed25519 pyramids are capped, but the
-  decoder ring. Budget an afternoon; expect the odd hour of humility.
+Pasta curve layer (the Pallas group law and scalar multiplication) is
-\item \textbf{Extend the pyramid.} The ed25519 pyramids are capped, but
+paused with its field foundations proven and the route mapped. The
-  the Pasta curve layer (Pallas group law and scalar multiplication) is
+terrain is known: the scalar layer's kernel-frontier crossing is the
-  paused with its field foundations proven and the route mapped --- the
+template for the hard part, and the control repo's
-  scalar layer's kernel-frontier crossing is the template, and the
+\code{METHOD.md}/\code{TIERS.md} state exactly what a finished brick
-  control repo's \code{METHOD.md}/\code{TIERS.md} state exactly what a
+looks like --- spec shape, axiom audit, check-script entry. Nobody is
-  finished brick looks like (spec shape, axiom audit, check-script
+saving this for an expert. Frontier work in machine-checked cryptography
-  entry). Frontier work, undergraduate-accessible.
+is, right now, undergraduate-accessible, and every chapter before this
-\item \textbf{Verify something of yours.} Pick a 200-line pure function you
+one was the access.
-  actually use --- a parser, a checksum, a data structure --- write its
-  denotation (what does it \emph{mean}?), state the square, prove it.
-  The first solo bridge is the moment this stops being a course.
-\item \textbf{Go deeper into the theory.} \emph{Theorem Proving in Lean 4}
-  (the official text), \emph{Mathematics in Lean} (Mathlib's course), and
-  the Lean Zulip --- an unusually welcoming expert community --- are the
-  standard next doors.
-\end{itemize}
-
-\subsection*{Further reading, annotated}
-
-\begin{itemize}[leftmargin=1.4em]
-\item \emph{Theorem Proving in Lean 4} (Avigad, de Moura, et al.; free
-online) --- the official text. Read it \emph{after} this book's
-Chapters 2--5 and it will feel like meeting the extended family of
-ideas you already know; its dependent-type chapters go far beyond our
-needs and are worth the trip.
-\item \emph{Mathematics in Lean} (the Mathlib community course) ---
-hands-on Mathlib fluency: naming conventions, search strategies, the
-algebra hierarchy. The fastest cure for ``I know the fact exists but
-not its name,'' which will be your main bottleneck after this book.
-\item \emph{The Lean Zulip} (\code{leanprover.zulipchat.com}) --- where
-the community lives. Unusually welcoming to beginners; search before
-asking, then ask well: a minimal example plus the goal state gets
-expert answers in hours.
-\item Bernstein \& Lange, \emph{Faster addition and doubling on
-elliptic curves} (2007) --- the completeness proof this chapter's
-worked example walked; readable with this book's preparation, and a
-model of what ``designed for implementers'' mathematics looks like.
-\item The RFC for EdDSA (RFC 8032) --- the signature scheme as
-deployed, cofactor-$8$s and encoding details included. Read the
-verification equation section against this chapter and notice how much
-sharper your questions have become.
-\item Project Everest / HACL$^{*}$ and Fiat Crypto --- the two other
-major verified-crypto lineages (F$^{*}$-based and Coq-based
-respectively), both shipping in real TLS stacks and browsers. Reading
-their claims with your Chapter~\ref{ch:honesty} toolkit is instructive
-in both directions: the methods differ, the honest-boundary discipline
-rhymes.
-\end{itemize}
-
-\begin{aha}
-One last reframe, the one this book was secretly about. ``Formal
-verification'' sounds like bureaucracy --- forms, stamps, compliance. What
-you actually practiced is closer to \emph{engineering's version of the
-scientific method}: make the claim precise enough to be falsifiable, then
-let an incorruptible referee try to falsify it, then publish the referee's
-report with the assumptions itemized. Cryptography needed that discipline
-first because its failures are silent and adversarial. It will not need it
-last.
-\end{aha}
 
 \begin{tryit}
 The graduation exercise. In the mini-system from
@@ -549,8 +513,8 @@ returns true \emph{iff} the signature's $R$ decompresses to a valid
 on-curve point equal to $[k](-A) + [s]B$ --- with field arithmetic,
 group law, scalar arithmetic, encoding, and decompression each carried
 by its own kernel-checked layer below. If your two columns match this,
-you can audit a verification paper's abstract in ninety seconds ---
+you can audit a verification paper's abstract in ninety seconds --- the
-which was the promise on the book's cover, kept.
+skill the last two chapters of this book will aim at a live public log.
 
 \solhead{12.4}
 \pathway Mirror the worked example's run 1 with $y = 10$.
@@ -565,11 +529,12 @@ put you on the curve at the WRONG point $(7,10) = -3P$ --- the sign bit
 is one bit of information doing real cryptographic work.
 
 \begin{checkpoint}
-The book's ending is a beginning, so the final checkpoint is prospective:
+You should be able to: (1) state what each pyramid layer claims and which
-you should be able to (1) state what each pyramid layer claims and which
 denotation it rides on; (2) explain to a security engineer why completeness
 of the Edwards law matters to \emph{code}; (3) locate the current frontier
-and say precisely why it is hard; and (4) name the next proof \emph{you}
+and say precisely why it is hard. The first pyramid is finished --- every
-intend to write. The authors of the companion repositories left the
+question mark from the opening figure resolved into a theorem. But its
-scaffolding up on purpose.
+entire security story rests on one algebraic assumption, and there is a
+kind of computer, not yet built, that erases it. The next chapter climbs
+the pyramid that was built for that day.
 \end{checkpoint}

chapters/ch13-second-summit.tex

@@ -0,0 +1,622 @@
+\chapter{The Second Summit: A Hash-Based Pyramid}
+\label{ch:secondsummit}
+
+\section{The theorem that survives, and the reason that doesn't}
+
+One leaf in the log does not belong to the pyramid you just climbed. Its
+subject kind says \code{slh\_dsa} where eighteen others say
+\code{ed25519} or \code{merkle\_accumulator}; it carries eleven
+certificates where its neighbors carry sixteen, forty-four, or sixty-one;
+and the scheme it attests contains no curve, no field, no scalar --- not
+one line of the algebra this book spent twelve chapters verifying. Leaf~18
+attests the log's first \emph{post-quantum signature scheme}, and this
+chapter is the climb that earns it.
+
+First, the honest reason such a thing exists. Every certificate in the
+Ed25519 pyramid will still be \emph{true} the day a large quantum computer
+boots --- whether that day is a decade out or never; what dies that day is
+the reason anyone cared. Read that carefully,
+because it separates two ideas this book has been keeping distinct all
+along. The certificates say the code \emph{computes the right function} ---
+that the extracted verifier accepts exactly the signatures the mathematics
+accepts. Whether accepting those signatures keeps anyone \emph{safe} rests
+on an assumption no proof in this book touches: that computing discrete
+logarithms on the curve is infeasible. Shor's algorithm, on a big enough
+quantum computer, computes them efficiently. Correctness certificate:
+intact. Scheme: forgeable. A correct implementation of a broken lock is
+still a broken lock.
+
+Hash functions are the part of the cryptographic toolbox that takes this
+future best. The strongest known quantum attack on preimage search is
+Grover's algorithm, a \emph{quadratic} speedup --- the kind of erosion you
+answer with modestly larger parameters, not the kind that dissolves the
+problem. So in August 2024, NIST standardized FIPS~205: \textbf{SLH-DSA},
+the \emph{stateless hash-based digital signature algorithm} (descended
+from SPHINCS\textsuperscript{+}) --- a signature scheme built from hash
+functions and \emph{nothing else}. No group. No field. Nothing for Shor
+to eat.
+
+\begin{bigidea}
+The second summit asks the question the first one could not: does the
+\emph{method} --- extract the real code, build a bridge, prove the
+certificates, audit the cones, attest the result --- transfer to terrain
+with entirely different mathematics? Signature chains and Merkle trees
+instead of limbs and group laws. If the method only worked on the terrain
+it was invented for, it was a trick. If it transfers, it is a discipline.
+This chapter is the experiment, run for real, on the parameter set
+\textbf{SLH-DSA-SHA2-128s}.
+\end{bigidea}
+
+The whole parameter set fits on an index card, and you should copy it out
+now, because every number in this chapter comes from it: hash output
+$n = 16$ bytes; total tree height $h = 63$, split into $d = 7$ layers of
+height $h' = 9$ (check the joint: $63 = 7 \cdot 9$); FORS forest of
+$k = 14$ trees of height $a = 12$; Winternitz parameter $w = 16$ (digits
+are hex nibbles, $\log_2 w = 4$), giving $\mathit{len} = 35$ chains
+($32$ message nibbles $+$ $3$ checksum digits; check: $35 = 2n + 3$ ---
+two nibbles per byte of the $n = 16$-byte value, plus three);
+message digest $m = 30$ bytes. In the verified repository these are not
+documentation --- they are the const-generic arguments baked into the one
+extracted entry point, \code{slh\_verify\_128s}, in
+\code{gen/SlhVerify/Funs.lean} (except $w$ and $\log_2 w$, which ride
+along as the crate constants \code{W} and \code{LGW} in the same file).
+
+\section{Signatures with nothing but a hash}
+
+Strip the idea to one bit. Pick a hash function $F$. Choose two secret
+random values $s_0, s_1$; publish $F(s_0)$ and $F(s_1)$ as your public
+key. To sign the bit $0$, reveal $s_0$; to sign $1$, reveal $s_1$. A
+verifier hashes what you revealed and compares against your public key.
+A forger must produce a preimage of a published hash --- the exact thing
+hash functions exist to prevent. That is Lamport's 1979 scheme, and it
+already contains the whole species: \emph{a signature is a controlled
+leak of preimages; verification is re-hashing the leak}.
+
+Two problems, and their fixes build the entire pyramid. First, one bit
+per key pair is absurd; the fix is \emph{chains}. Second, every key is
+one-time --- reveal twice and a forger can mix and match; the fix is
+\emph{trees}. Chains first.
+
+\textbf{Winternitz chains (WOTS\textsuperscript{+}).} Instead of two
+secrets per bit, keep one secret per hex \emph{nibble} and define a chain:
+$c_0 = \text{secret}$, $c_{i+1} = F(c_i)$, sixteen positions
+$c_0 \dots c_{15}$. Publish the chain \emph{end} $c_{15}$ (all
+thirty-five chain ends will later be compressed to one value; the
+compressor is the $T$ of the pricing box to come). To sign the nibble
+value $v \in \{0,\dots,15\}$, reveal $c_v$
+--- the chain value $v$ steps up. The verifier takes what you revealed
+and \emph{walks the remaining steps}: $15 - v$ more applications of $F$
+must land exactly on the published end.
+
+\begin{worked}{one chain, resumed --- and the checksum see-saw}
+Real parameters ($w = 16$), no napkin scaling needed. Say message nibble
+$v = 11$ ($\mathtt{0xB}$). The signature reveals $c_{11}$. The verifier
+computes $15 - 11 = 4$ applications of $F$ --- in the verified code the
+hash \emph{address} is set to $11, 12, 13, 14$ in turn, one per step ---
+and compares the result against the chain end. Four hashes; no secrets;
+done.
+
+Now attack it. $F$ is public, so anyone holding $c_{11}$ can compute
+$c_{12} = F(c_{11})$ --- a valid signature for the nibble $12$! Walking
+\emph{forward} is free; only walking \emph{backward} needs a preimage.
+Forging ``11 $\to$ 12'' costs nothing... for that one chain. The fix is
+bookkeeping, and you can run all of it by hand. Alongside the $32$
+message nibbles, WOTS signs a \textbf{checksum}:
+\[
+\mathit{csum} \;=\; \sum_{i=0}^{31} \,(15 - \mathit{msg}_i),
+\]
+the total of all \emph{remaining} steps. Take the extreme case, all
+nibbles zero: $\mathit{csum} = 32 \cdot 15 = 480 = \mathtt{0x1E0}$. The
+code shifts left by $4$, flush against the top of two bytes, because the
+digit extractor reads nibbles most-significant-first:
+$\mathtt{0x1E00}$, bytes $[\mathtt{1E}, \mathtt{00}]$, whose
+first three nibbles are the checksum digits $(1, 14, 0)$ --- signed with
+three more chains, walked $15{-}1$, $15{-}14$, $15{-}0$ steps by the
+verifier.
+
+Now run the see-saw, on these numbers. A forger bumps one message nibble
+$0 \to 1$ (walking that chain forward one step, free). The checksum
+follows: $\mathit{csum} = 479 = \mathtt{0x1DF}$, shifted
+$\mathtt{0x1DF0}$, digits $(1, 13, 15)$. Compare against $(1, 14, 0)$:
+the \emph{third} digit rose $0 \to 15$ --- forward walk, free --- but
+the \emph{second} fell $14 \to 13$, and the signature only revealed that
+chain's value at position $14$. The forger needs position $13$: one step
+\emph{earlier}. Walking backward. Inverting $F$. (In general: a strictly
+smaller checksum must have a strictly smaller digit at the most
+significant position where the two differ --- some chain always falls.)
+The thirty-five chains hold each other hostage, and the
+hostage-taking is pure arithmetic --- the kind a certificate can pin.
+\end{worked}
+
+In the verified repository that arithmetic \emph{is} pinned:
+\lean{fips205.wots\_csum\_loop\_eq} certifies that the extracted checksum
+loop computes exactly the fold
+$\mathit{csum} \leftarrow \mathit{csum} + (W{-}1 - \mathit{msg}_i)$ ---
+and its axiom cone is the bare kernel three, because summing nibbles
+needs no hash at all. Keep that observation; it becomes a pattern.
+
+\section{One virtual tree of $2^{63}$ keys}
+
+Chains sign one message per key pair. The tree fix: make $2^{63}$
+one-time WOTS key pairs, hash each down to a leaf, and build a Merkle
+tree; the public key is the single root. A signature then contains the
+one-time signature \emph{plus the authentication path} --- the $\log_2$
+chain of sibling hashes from that leaf to the root. The verifier
+recomputes the leaf from the WOTS signature, hashes its way up the path
+--- at each level the current bit of the leaf index says whether the
+running node is a left or right child, i.e.\ whether to compute
+$H(\text{node} \,\Vert\, \text{sibling})$ or
+$H(\text{sibling} \,\Vert\, \text{node})$ --- and compares the result to
+the published root. You met this exact structure in
+Chapter~\ref{ch:why}'s pyramid diagrams and will meet it once more in the
+final chapter, holding this book's own proofs; here it holds signature
+keys.
+
+Except nobody can build that tree. Count it: $2^{63}$ leaves, each
+requiring a full WOTS key generation ($35$ chains $\times$ $15$ steps
+$+$ compression), plus the internal hashes --- on the order of $10^{21}$
+hash evaluations --- roughly $5 \times 10^{21}$, about $2^{72}$ --- to
+materialize once. The resolution is two-fold:
+
+\begin{itemize}[leftmargin=1.4em]
+\item \textbf{Hypertree}: don't build one tree of height $63$; build
+  $7$ layers of trees of height $9$, where each tree's root is signed by
+  a WOTS key of the tree \emph{above} it --- so nobody, signer included,
+  ever materializes more than a height-$9$ tree at a time. A signature
+  carries $7$ small WOTS signatures, one per layer.
+\item \textbf{Virtuality}: secrets are generated pseudorandomly from a
+  seed, so any leaf can be \emph{recomputed on demand}. The full
+  structure exists only potentially. The signer touches one path of it
+  per signature; the verifier re-hashes exactly that path.
+\end{itemize}
+
+\begin{aha}
+The hypertree is never built. A structure of $2^{63}$ keys --- more
+one-time keys than there are seconds in two hundred billion years ---
+exists only as the \emph{promise} that any requested piece can be
+recomputed from a $16$-byte seed, and the root pins every piece of it at
+once. This is the find/check asymmetry of Chapter~\ref{ch:prime} scaled
+to its logical extreme: the object is astronomically too large to ever
+exist, and verifying one path through it costs a few thousand hashes on
+your laptop.
+\end{aha}
+
+One piece is missing: the hypertree's leaves are \emph{one-time} keys,
+and the signer is stateless --- it cannot remember which leaves it has
+used. The scheme picks the leaf pseudorandomly per message, and to
+survive the rare event that two messages draw the same leaf, it does not
+put the message directly under a WOTS key. Instead the message digest is
+signed by \textbf{FORS} (Forest Of Random Subsets): $k = 14$ little
+Merkle trees of height $a = 12$. Each tree hides $2^{12}$ secrets in its
+leaves; the message digest names one leaf per tree; signing reveals
+those $14$ secrets with their authentication paths, and the $14$
+recomputed roots are compressed into one value which the hypertree then
+certifies.
+
+\begin{worked}{FORS on a napkin --- two trees, height two}
+Shrink to $k = 2$, $a = 2$: two trees of four secrets each, eight
+secrets total, digest length $k \cdot a = 4$ bits. Say the digest is
+$\mathtt{1001}$. Split into $2$-bit indices: tree $0$ opens leaf
+$\mathtt{10} = 2$, tree $1$ opens leaf $\mathtt{01} = 1$. The signature
+reveals secret $2$ of tree $0$ with its two path siblings, and secret
+$1$ of tree $1$ with its two; the verifier hashes each secret to a leaf,
+climbs both paths, and compresses the two roots. Now reuse the key on a
+second digest, $\mathtt{0111}$: it opens leaves $1$ and $3$ --- two
+\emph{more} secrets leaked, four of eight now public. A forger wanting
+to sign digest $\mathtt{1011}$ needs leaves $2$ and $3$: both already
+leaked --- forgery! At napkin scale reuse is fatal in one collision. At
+real scale the same arithmetic is the defense: two signatures leak at
+most $28$ of $57{,}344$ secrets, and a target digest needs its
+\emph{fourteen} indices --- each $12$ bits --- to land entirely inside
+the leaked sliver: probability about $(28/57{,}344)^{14}$ per key, and
+the pseudorandom leaf choice means the attacker cannot steer which
+key pair collides. Graceful degradation is not a slogan; it is this
+exponent.
+\end{worked}
+
+That degradation arithmetic --- a \emph{few} secrets out of
+$14 \cdot 2^{12} = 57{,}344$, and fourteen simultaneous hits needed ---
+is the reason the scheme can afford statelessness.
+
+\begin{worked}{the digest split, to the bit --- and the price of everything}
+The verifier's first act is one call to the message-digest oracle
+$H_{\mathit{msg}}$, producing $m = 30$ bytes. Those $30$ bytes are then
+split three ways by live arithmetic you can audit on paper:
+\[
+\Big\lceil \tfrac{k \cdot a}{8} \Big\rceil
+= \Big\lceil \tfrac{14 \cdot 12}{8} \Big\rceil = 21 \text{ bytes}
+\qquad
+\Big\lceil \tfrac{h - h/d}{8} \Big\rceil
+= \Big\lceil \tfrac{63 - 9}{8} \Big\rceil = 7 \text{ bytes}
+\qquad
+\Big\lceil \tfrac{h}{8d} \Big\rceil
+= \Big\lceil \tfrac{63}{56} \Big\rceil = 2 \text{ bytes}
+\]
+--- and $21 + 7 + 2 = 30$ exactly, no slack byte anywhere. The first
+$21$ bytes are the $14 \times 12 = 168$ bits of FORS leaf indices; the
+next $7$ bytes, masked to $54$ bits, choose \emph{which} bottom-layer
+tree of the $2^{54}$ signs this message; the last $2$ bytes, masked to
+$9$ bits, choose the leaf within it. (The masks in the extracted code
+are $\mathtt{U64.MAX} \ggg (64{-}54)$ and $\mathtt{U64.MAX} \ggg
+(64{-}9)$, the shift amounts computed from $h$ and $d$ --- keep $54$,
+keep $9$. And the hypertree spends the $54$ tree-index bits like a
+meter: the bottom layer takes the $9$-bit leaf index directly, then each
+of the six upper layers peels
+$\mathit{idx\_leaf} = \mathit{idx\_tree} \bmod 2^9$ off the bottom and
+shifts right by $9$; after the sixth peel, $54 - 6 \cdot 9 = 0$ bits
+remain --- the budget is spent exactly at the top layer.)
+
+Now price the whole verification, from the parameter card. Five oracles
+do all the work --- $F$ steps chains and hashes leaves, $H$ hashes tree
+nodes, two compressors $T$ squeeze the $35$ WOTS chain ends and the $14$
+FORS roots down to single values, and $H_{\mathit{msg}}$ digests the
+message --- and every one of them is countable. Input-independent first:
+FORS paths $k \cdot a = 168$ calls to $H$, XMSS paths
+$d \cdot h' = 63$ more --- $231$ exactly; compressions, one $T$ per WOTS
+public key per layer ($7$) plus one for the FORS roots; the single
+$H_{\mathit{msg}}$; and the $14$ $F$-calls hashing the revealed FORS
+secrets to leaves: a fixed overhead of $254$ oracle calls. The chains
+add the input-dependent part, and here the see-saw earns its keep a
+second time: each chain walks at most $15$ steps, suggesting a cap of
+$35 \cdot 15 = 525$ per layer --- but that cap is \emph{unreachable},
+because message walks total exactly $\mathit{csum}$ while long message
+walks force short checksum digits and vice versa. Run the numbers over
+every possible checksum and the true per-layer maximum is $510$,
+achieved precisely at the all-zero message you worked above. So: at
+worst $7 \cdot 510 = 3{,}570$ chain steps, a grand total of $3{,}824$
+oracle calls --- just under four thousand, typically nearer $2{,}000$.
+Set the two numbers side by side: $\sim 2^{72}$ hash calls to
+materialize the structure, $\sim 2^{12}$ to check one path through it.
+The verifier touches a $2^{-60}$ sliver and trusts the rest to
+arithmetic.
+
+And the signature that steers those two thousand hashes? Its size is an
+exercise in reading types: $n \cdot \big(1 + k(1+a) + d(\mathit{len} +
+h')\big) = 16 \cdot (1 + 182 + 308) = \mathbf{7{,}856}$ bytes, against a
+$32$-byte public key. (An Ed25519 signature is $64$ bytes. Post-quantum
+insurance is not free; it is merely \emph{possible}.)
+\end{worked}
+
+\section{The same method, on alien terrain}
+
+Now the experiment this chapter exists to report. The repository
+\code{fips205-slhdsa-verified} runs the exact pipeline you learned in
+Chapters~\ref{ch:rust}--\ref{ch:field}: pin a Rust source (a pure-Rust,
+no-unsafe FIPS~205 implementation, pinned by commit), extract through
+Charon and Aeneas into Lean --- starting from the one entry point
+\code{slh\_verify\_128s}, with the five hash primitives marked
+\emph{opaque} at the extraction boundary --- and prove certificates
+about the extracted model under a memory-guarded button. Same tools,
+same discipline, same \code{check.sh} skeleton with the same fail-closed
+phases. What comes out the other side is \textbf{eleven certificates}:
+ten loop theorems and one apex.
+
+The ten are old friends wearing new clothes. Every one has the shape of
+Chapter~\ref{ch:denotation}'s bridge: on the left, the loop the
+extraction produced (chain walking, checksum accumulation, Merkle
+ascent, hypertree layering); on the right, a hand-written structural
+fold; between them, an equality theorem proved by unfolding one loop
+turn and inducting on the trip count. You have met every one of these
+folds already, as arithmetic. \lean{wots\_csum\_loop\_eq} pins the
+see-saw sum. \lean{chain\_free\_loop\_eq} pins the resume-the-chain
+walk, address sequence $v, v{+}1, \dots$ included.
+\lean{xmss\_loop\_eq} pins the even-bit/odd-bit sibling order of the
+Merkle ascent. And \lean{ht\_loop\_eq} pins the layer walk --- the
+peel-nine-bits-and-shift meter you just ran on the digest split, as a
+theorem.
+
+But this terrain withholds something the first pyramid gave freely, and
+the repository says so in bold type. In the field proofs, the right-hand
+side of the bridge was \emph{independent mathematics} --- $\Zmod{p}$,
+which Mathlib understands without ever seeing dalek's code --- so each
+commuting square landed in a second semantics and meant something on its
+own. The natural move here would be the same: restate SLH-DSA
+verification as free-standing mathematics and prove the code equal to
+\emph{that}. But what would the restatement be made of? Hash chains and
+Merkle nodes --- the same oracles, the same folds; there is no
+Mathlib theory of SLH-DSA waiting on the other side of the bridge the
+way $\Zmod{p}$ was waiting for dalek. So the reference folds are built
+from \emph{the same extracted hash oracles} the loops call, and each
+certificate buys visibility rather than independent meaning: the
+extracted chain loop is some forty lines of monadic, generated Lean; the
+fold standing beside it in \lean{chain\_free\_loop\_eq} is fourteen you
+can hold against the standard's algorithm over a coffee. That last
+reading --- fold against FIPS~205 --- is a human step, named as such in
+the trusted base. The repository's own phrase is the one to memorize:
+read each loop certificate as \emph{``visible,'' not ``correct.''}
+
+\begin{pitfall}
+Chapter~\ref{ch:honesty} trained you to ask what a certificate does
+\emph{not} say; this repository answers before you ask, and its ledger
+is worth reading twice. The five hash oracles are \emph{axioms} ---
+nothing relates them to FIPS~180-4's SHA-256, the same standing boundary
+as SHA-512 in the Ed25519 apex. One inner loop (\code{base\_2b}, the
+digit extractor that feeds both FORS indices and WOTS nibbles) is
+threaded opaquely with \emph{no certificate} --- a defect there would
+change the recomputed root while all eleven theorems held. The proved
+subject is a monomorphic facade; its bridge to the deployed generic
+verifier is a $137$-case differential test, \emph{evidence, not proof}.
+Signing and key generation were never extracted at all. And everything
+\emph{above} the extraction root is trusted base too --- the assembly of
+the domain-separated message $M'$, including the single separator byte
+that is all that distinguishes pure from prehash verification; get that
+byte wrong and you have a cross-variant forgery primitive that no
+certificate in the repository would notice. A trusted
+base is not a weakness; an \emph{unstated} one is.
+\end{pitfall}
+
+The apex closes the pyramid the same way the Ed25519 apex did --- as an
+acceptance characterization, lightly paraphrased:
+
+\begin{lstlisting}[language=Lean]
+theorem slh_verify_128s_accepts_iff (mprime sig pk) :
+    slh_verify_128s mprime sig pk
+      = do let root ← slhVerifyRoot mprime sig pk
+           ok (decide (root.val = pk.pk_root.val))
+\end{lstlisting}
+
+(The paraphrase elides only typography: the const-generic parameter
+decorations and the \lean{Result}-monad plumbing. The verbatim statement
+is theorem \lean{fips205.slh\_verify\_128s\_accepts\_iff} in
+\code{verification/Proofs/ApexSpec.lean} --- diff this prose against
+that source; the book taught you to distrust paraphrases, including its
+own.) For \emph{every} message digest, \emph{every} signature,
+\emph{every} public key at these parameters: the extracted verifier
+accepts exactly when the recomputed hypertree root byte-equals the
+public key's root. There is no other acceptance path --- no debug
+backdoor, no unchecked branch, no early \lean{true}. Both summits end in
+the same clean air: a quantified equation whose right-hand side a
+stranger can read.
+
+One more object from this repository deserves a place in your permanent
+toolkit: the audit table of axiom cones, which turns
+Chapter~\ref{ch:honesty}'s discipline into a picture of the pyramid
+itself.
+
+\begin{center}
+\small
+\begin{tabular}{@{}ll@{}}
+\toprule
+\textbf{Certificate layer} & \textbf{Cone beyond the kernel three} \\
+\midrule
+digit/byte plumbing (4 certs) & --- \emph{(pure arithmetic, no hash)} \\
+chain, WOTS recompute & $F$ \\
+XMSS ascent, FORS inner & $H$ \\
+FORS outer & $F, H$ \\
+hypertree walk & $F, H$, the WOTS compressor (axiom \code{t\_l}) \\
+apex & all five oracles \\
+\bottomrule
+\end{tabular}
+\end{center}
+
+The cone \emph{grows as you climb}: bit-shuffling needs no oracles at
+all; each layer adds exactly the hash primitives it touches; the apex
+carries all five. The audit enforces every row with exact equality ---
+one axiom extra or one missing fails the build --- so this table is not
+documentation, it is a \emph{theorem about the theorems}.
+
+And the table carries a war story, told here so you inherit the scar
+without the wound. During the audit, comparing what each compressor
+axiom was \emph{used as} against what it was \emph{named} turned up a
+mismatch: the axiom spelled \code{t\_l} is the one doing the standard's
+$T_{\mathit{len}}$ job (compressing WOTS chain ends), while the axiom
+spelled \code{t\_len} does the $T_k$ job (compressing FORS roots) ---
+the source's names are \emph{inverted} against FIPS~205. Worse, both
+axioms model what is a \emph{single} primitive in the Rust source. The
+repository's response was not to quietly ``fix'' the names --- renaming
+proves nothing --- but to document the inversion at the axiom
+declarations and keep the two axioms separate anyway, assuming
+\emph{less} (two possibly-different functions) rather than more. Had the
+auditor trusted spelling, the cone table above would read cleanly and
+lie. When you audit a stranger's certificate, judge every axiom by what
+it is used as, never by what it is named. Names are spelling; cones are
+property.
+
+The experiment the chapter opened with can now be called. The pipeline
+re-ran end to end on terrain its designers never saw: extraction, the
+loop-to-fold bridge shape, the exact-cone audit, the fail-closed button,
+the acceptance-characterization apex --- all of it transferred without a
+structural change. Discipline, not trick. With one honest asterisk the
+ledger already made you read: this terrain offered no second semantics,
+so the bridges here are thinner than the field layer's --- visibility,
+not independent meaning. A method that transfers \emph{and tells you
+exactly how much thinner its guarantees just got} is rarer than either
+half alone.
+
+\section{The leaf, live}
+
+The climb ends where the chapter began, but now you can read every field.
+Leaf~18 of the log --- \code{entries/000018.json} in the mirror,
+nineteenth and newest --- binds the repository at its pinned commit to
+the eleven certificate names you now know, each with \code{status}
+proven, each with its \emph{observed} axiom cone equal to its expected
+cone: kernel-3 for the four plumbing certificates, the oracle sets of
+the table above for the rest, all five for the apex. Its scope block
+recites the trusted base you just read --- oracles assumed, signing out
+of scope, \code{base\_2b} uncertified, differential bridge not a proof
+--- because an attestation that hides its boundary is advertising, and
+this log does not accept advertising.
+
+``Leaf~18 landed, so the log went post-quantum'' --- plausible, and
+wrong twice. First: leaf~18 is the first leaf \emph{about} a
+post-quantum signature scheme, but its own issuance signature --- the
+block inside \code{entries/000018.json}, like every leaf's --- is
+Ed25519 only. Second: the log's \emph{tree heads} did start carrying an
+additional SLH-DSA-SHA2-128s co-signature in the same publication batch
+--- but the first dual-signed head is the size-\emph{14} head (leaf~18
+arrives at size $19$, five appends later). Two separate facts, one lazy
+conflation avoided; append-only history keeps them distinguishable
+forever.
+
+And here the estate quietly eats its own cooking --- with the books kept
+scrupulously. The head's required Ed25519 signature is produced by the
+dalek library attested at leaf~13 --- forty-four certificates,
+self-inclusion verified inside the signature block itself: machinery
+attested \emph{in the log}, signing \emph{for the log}. The additional
+co-signature closes a different, looser loop: it uses parameter set
+SHA2-128s --- \emph{exactly} the parameter set whose verification path
+leaf~18 proves --- but the OpenSSL backend that actually produces and
+checks that co-signature carries no certificate anywhere; what is
+attested is the scheme's verification path in an independent, extracted
+implementation, not the tool on duty. And for the \emph{signing}
+operations, no loop closes at all --- no signing operation is proven for
+either scheme, and the log says so. Read the three clauses again in
+order: attested machinery, attested scheme, honest gap. Even the
+self-reference keeps its books honest.
+
+\begin{tryit}
+Touch the second summit yourself; it costs one command. Clone
+\code{github.com/saymrwulf/lean-transparency-log} and run:
+\begin{center}
+\code{python3 verify.py \ddash receipt receipts/fips205-slhdsa-verified.receipt.json}
+\end{center}
+The receipt binds
+leaf~18 by inclusion proof to the size-$19$ signed head. Then open
+\code{entries/000018.json} and find, with your own eyes: the eleven
+certificate names, the five oracle axioms in the apex's observed cone,
+and the exclusions block naming \code{base\_2b}. You have just audited a
+post-quantum verification claim --- boundary and all --- in the time it
+takes to pour a coffee.
+\end{tryit}
+
+\section*{Exercises}
+
+\exercise{(Paper) All thirty-two message nibbles equal $7$. Compute the
+checksum, the shift, the two bytes, and the three checksum digits, as
+the worked example did for the all-zero message. How many steps of $F$
+does the verifier walk on each of the three checksum chains?}
+
+\exercise{(Paper) Re-derive the digest split from the parameter card:
+show $\lceil 168/8 \rceil = 21$, $\lceil 54/8 \rceil = 7$,
+$\lceil 63/56 \rceil = 2$, and verify they exhaust $m = 30$. Then
+explain in one sentence why the second slice is masked to exactly $54$
+bits and what would go wrong with a $55$-bit mask.}
+
+\exercise{(Paper) Derive the signature size from the types: $n$ bytes of
+randomness, $k$ revealed FORS secrets plus $k$ auth paths of $a$ nodes,
+and $d$ XMSS signatures of $\mathit{len} + h'$ hashes each. Show the
+total is $16 \cdot 491 = 7{,}856$ and locate the single largest
+contributor.}
+
+\exercise{(Audit drill) State the see-saw precisely and prove it: if a
+forger changes the message so that some nibble strictly increases and
+none decreases, then the checksum strictly decreases, and at least one
+checksum digit's chain must be evaluated at a position \emph{earlier}
+than the one revealed. Why does ``earlier position'' mean ``invert
+$F$''?}
+
+\exercise{(Audit drill) The audit holds five oracle axioms but the Rust
+source has four hash primitives: \code{t\_l} and \code{t\_len} both
+delegate to one function. Explain why modeling one primitive as two
+independent axioms is the \emph{conservative} choice --- what could a
+proof using ``they are equal'' conclude that the current model cannot,
+and why is refusing that conclusion safer?}
+
+\exercise{(Discussion) The day a cryptographically relevant quantum
+computer exists, which statements in this book's estate become false?
+Work through: the four Ed25519 apex certificates; the Ed25519 signatures
+on the log's tree heads; leaf~18's certificates; the SLH-DSA
+co-signatures on the heads. Sort each into ``still true,'' ``true but no
+longer load-bearing,'' and ``broken'' --- and defend the sorting.}
+
+\section*{Solutions and pathways}
+\solutionsintro
+
+\solhead{13.1}
+\pathway Same three moves as the worked box: sum the remaining steps,
+align, extract nibbles.
+\answer $\mathit{csum} = 32 \cdot (15 - 7) = 256 = \mathtt{0x100}$.
+Shifted left $4$: $\mathtt{0x1000}$, bytes $[\mathtt{10}, \mathtt{00}]$,
+first three nibbles $(1, 0, 0)$. The verifier walks $15 - 1 = 14$,
+$15 - 0 = 15$, $15 - 0 = 15$ steps. (Sanity: middle-of-the-road message
+digits still force near-full walks on checksum chains --- the checksum
+digits are usually \emph{small}, so their remaining walks are long.)
+
+\solhead{13.2}
+\pathway The three ceilings are $\lceil ka/8\rceil$,
+$\lceil (h - h/d)/8 \rceil$, $\lceil h/(8d) \rceil$ with the card's
+values substituted.
+\answer $\lceil 14 \cdot 12 / 8 \rceil = \lceil 21 \rceil = 21$;
+$\lceil (63-9)/8 \rceil = \lceil 6.75 \rceil = 7$;
+$\lceil 63/56 \rceil = 2$; and $21 + 7 + 2 = 30 = m$. The tree index
+addresses one of $2^{h - h/d} = 2^{54}$ bottom-layer trees, so the mask
+keeps exactly $54$ bits; a $55$-bit mask could name a tree that does not
+exist --- the verifier would recompute a root of an out-of-range tree
+and reject a valid signature (or, worse in a sloppier implementation,
+wrap around silently). Ranges are part of correctness; that is why the
+extracted masks are certificate-adjacent code, not comments.
+
+\solhead{13.3}
+\pathway Transcribe the type structure into a sum, then factor out $n$.
+\answer $n\big(1 + k(1{+}a) + d(\mathit{len}{+}h')\big)
+= 16\,(1 + 14 \cdot 13 + 7 \cdot 44) = 16\,(1 + 182 + 308)
+= 16 \cdot 491 = 7856$. The hypertree's $308$ hash-values (seven WOTS
+signatures of $35$ plus seven auth paths of $9$) dominate: $4{,}928$ of
+the $7{,}856$ bytes --- the price of splitting one impossible tree into
+seven possible ones.
+
+\solhead{13.4}
+\pathway Write the checksum as a function of the digit vector and
+difference it.
+\answer $\mathit{csum} = \sum_i (15 - \mathit{msg}_i)$, so if some
+nibbles increase by a total of $\delta > 0$ and none decrease,
+$\mathit{csum}$ drops by exactly $\delta$. The checksum digits are the
+base-$16$ representation of the (aligned) checksum; a strictly smaller
+value must have at least one strictly smaller digit at some position
+(compare digits from the most significant end; the first difference is
+a decrease). The signature revealed the chain value at the \emph{old}
+digit's position; a forgery needs the value at a strictly earlier
+position of that chain --- but the chain runs forward by $F$, so an
+earlier value is a preimage of the revealed one under iterated $F$.
+Producing it is inverting the hash --- the assumption the whole scheme
+stands on.
+
+\solhead{13.5}
+\pathway Ask what each axiom is \emph{used for} in the proofs, then ask
+what merging them would license.
+\answer The model with two independent axioms proves everything the
+certificates claim while assuming only ``there exist two functions with
+these signatures.'' Adding \lean{t\_l = t\_len} would let a proof
+conclude that a WOTS compression can be replayed as a FORS compression
+(and vice versa) --- an interchangeability the standard does not grant
+(the two uses differ in domain separation via the address argument) and
+no certificate needs. Assuming less can only make the theorems
+\emph{harder} to prove, never falsely stronger; if the theorems still go
+through, the weaker assumption is strictly safer. The general habit:
+when in doubt, split the axiom --- and let the cones show exactly which
+theorem leaned on which half.
+
+\solhead{13.6}
+\pathway Separate ``the theorem is true'' from ``the assumption behind
+the scheme's security is true'' for each artifact.
+\answer The four Ed25519 apex certificates: \emph{still true} ---
+kernel-checked equations about extracted code do not cite discrete-log
+hardness anywhere. The Ed25519 head signatures: \emph{true but no longer
+load-bearing} --- the signatures still verify, but a quantum forger
+could now mint alternative heads, so their evidentiary weight collapses
+(the certificates about the \emph{verifier} remain true; the
+unforgeability of \emph{signing} was never proven and is now also not
+believed). Leaf~18's certificates: \emph{still true}, and still
+load-bearing --- nothing in their cones or their scheme depends on
+Shor-vulnerable structure. The SLH-DSA head co-signatures: the reason
+the slot exists --- \emph{load-bearing by design} on that day, resting
+on hash preimage resistance, eroded only quadratically by Grover.
+Moral, worth saying aloud: proofs of correctness are
+quantum-proof; \emph{schemes} are not; and a log that dual-signs its
+heads is planning for the difference.
+
+\begin{checkpoint}
+You should now be able to: explain why a correctness certificate
+survives a quantum computer while the scheme it certifies may not;
+run a WOTS chain-resume and the checksum see-saw by hand at $w = 16$;
+price an SLH-DSA-SHA2-128s verification ($254$ fixed oracle calls plus
+the chains, against $2^{72}$ to build what it checks); read the eleven
+certificates and the cone-growth table as one object; and recite what
+the second summit does \emph{not} claim --- oracles assumed,
+\code{base\_2b} uncertified, the $M'$ assembly above the extraction
+root, signing never in scope. Both pyramids now
+stand, and both end the same way: a script prints \texttt{ALL GREEN}
+and a leaf lands in a public log. Which leaves exactly one question in
+this book, and it is the deepest one: that script, and that log --- who
+checks \emph{them}? The final chapter has been waiting for you.
+\end{checkpoint}

chapters/ch14-attestation-protocol.tex

@@ -3,6 +3,8 @@
 
 \section{The second act nobody warns you about}
 
+The question the last checkpoint left you holding --- that script, that
+log, who checks \emph{them}? --- has a name, and a body count.
 Chapter~\ref{ch:honesty} taught you to interrogate a certificate: ask what it
 rests on, and refuse to be impressed by a file that merely compiles. That
 chapter had a blind spot, and this one exists because a sequence of external
@@ -201,7 +203,7 @@ people who eventually caught them were strangers.
 You will not build an eighteen-attack self-test for a homework exercise, and you
 should not. What you should take away is a habit of mind and a vocabulary.
 
-\begin{checkpoint}
+\begin{bigidea}
 When you next read the words ``formally verified'', ask two questions instead of
 one.
 
@@ -215,9 +217,167 @@ myself?
 If a project cannot answer the second set, it has done act one and called it
 finished --- which is exactly the mistake these chapters were rewritten to
 prevent.
-\end{checkpoint}
+\end{bigidea}
 
 And when it is your own project: invite someone to attack the button, early.
 Every one of the eighteen defects was found by a reviewer trying to break it.
 \emph{None} was found by the author reviewing their own work --- and the author
 looked, repeatedly, with the same care they had used to write the proofs.
+
+\section{Go and touch the real thing}
+\label{sec:live-log}
+
+Everything in this chapter runs in production, in public, right now. The
+companion estate operates a \emph{transparency log} of its own attestations:
+a Merkle accumulator whose leaves are signed statements of the form ``this
+repository, at this exact commit, was checked by its own button, and these
+are the certificates it proved, on exactly these axiom cones.'' The log is
+served at \texttt{ltl.zkdefi.org} and mirrored as an ordinary git repository
+(\texttt{github.com/saymrwulf/lean-transparency-log}) that you can clone and
+interrogate offline. It is act two, industrialized: every failure class this
+chapter catalogued has a gate in that pipeline because a reviewer once got
+past the spot where the gate now stands.
+
+\begin{tryit}
+The fifteen-minute exercise, and the best return on time in this book: clone
+the mirror and run the verifier.
+
+\begin{itemize}
+\item \code{python3 verify.py \ddash all} --- plain Python for the hashing, the
+  \code{openssl} binary for signatures, and it \emph{fails closed} without
+  them (this chapter taught you why ``couldn't check'' must
+  never print as a pass). It recomputes every leaf hash, every historical
+  tree head against its recomputed prefix root, every signature, and every
+  inclusion proof --- your machine, your verdict, nobody's word.
+\item Pin the trust anchors \emph{two independent ways}: the keys are served
+  by the site (\texttt{/log-public-key}, \texttt{/log-slhdsa-public-key})
+  and shipped in the mirror (\code{provider.ed25519.pub},
+  \code{provider.slhdsa.pub}). The copies must agree byte-for-byte. If they
+  ever disagree, you have caught something worth catching.
+\item Read one leaf in full --- \code{entries/000018.json} is a good choice
+  --- and find, inside it, every vocabulary item of this chapter: the pinned
+  commit, the certificate list, the \emph{observed} axiom cones, the machine
+  protection, and the stated exclusions.
+\end{itemize}
+\end{tryit}
+
+The log's nineteen leaves map onto this book. Leaves 13--16 attest the four
+ed25519 repositories whose pyramid you climbed in
+Chapters~\ref{ch:modular}--\ref{ch:pyramid}: forty-four certificates each ---
+twenty-seven on the main button, thirteen on the scalar button, and the four
+apex-tier theorems whose \emph{documented, boundary-exact} cones are
+Chapter~\ref{ch:honesty}'s lesson enforced in production. Leaf 17 is this
+chapter made literal: the log carries kernel-checked proofs of \emph{its own
+Merkle machinery} as one of its own entries --- ``who checks the checker?''
+answered by putting the checker's mathematics inside the thing it checks.
+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
+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
+of its own signature scheme.
+
+Two boundaries, so that you read the log the way this book taught you to
+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
+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.
+
+That is the whole arc of this book in one artifact: arithmetic became
+theorems (act one), theorems became certificates with named cones
+(Chapter~\ref{ch:honesty}), the method crossed to a second pyramid with
+different mathematics and held (Chapter~\ref{ch:secondsummit}),
+certificates became attestations a stranger can re-derive (this chapter)
+--- and the attestations went into a structure that remembers everything
+and lets anyone catch it lying. When you build your own, you now know what
+it costs, and where the bodies are buried.
+
+\begin{aha}
+One last reframe, the one this book was secretly about. ``Formal
+verification'' sounds like bureaucracy --- forms, stamps, compliance. What
+you actually practiced is closer to \emph{engineering's version of the
+scientific method}: make the claim precise enough to be falsifiable, then
+let an incorruptible referee try to falsify it, then publish the referee's
+report with the assumptions itemized. Cryptography needed that discipline
+first because its failures are silent and adversarial. It will not need it
+last.
+\end{aha}
+
+\section*{Where to go from here}
+
+In increasing order of ambition:
+
+\begin{itemize}[leftmargin=1.4em]
+\item \textbf{Read a real proof end-to-end.} \code{FieldSpec.lean} in
+  \code{dalek-ed25519-verified}, top to bottom, with this book as the
+  decoder ring. Budget an afternoon; expect the odd hour of humility.
+\item \textbf{Verify something of yours.} Pick a 200-line pure function you
+  actually use --- a parser, a checksum, a data structure --- write its
+  denotation (what does it \emph{mean}?), state the square, prove it.
+  The first solo bridge is the moment this stops being a course.
+\item \textbf{Extend the estate.} Chapter~\ref{ch:pyramid}'s ``Where you
+  come in'' names the open frontier --- the paused Pasta curve layer ---
+  and the control repository's method files say exactly what a finished
+  brick looks like. When yours is done, this chapter told you how to
+  attest it, and the log is where it goes.
+\item \textbf{Go deeper into the theory.} \emph{Theorem Proving in Lean 4}
+  (the official text), \emph{Mathematics in Lean} (Mathlib's course), and
+  the Lean Zulip --- an unusually welcoming expert community --- are the
+  standard next doors.
+\end{itemize}
+
+\subsection*{Further reading, annotated}
+
+\begin{itemize}[leftmargin=1.4em]
+\item \emph{Theorem Proving in Lean 4} (Avigad, de Moura, et al.; free
+online) --- the official text. Read it \emph{after} this book's
+Chapters~\ref{ch:lean}--\ref{ch:automation} and it will feel like
+meeting the extended family of
+ideas you already know; its dependent-type chapters go far beyond our
+needs and are worth the trip.
+\item \emph{Mathematics in Lean} (the Mathlib community course) ---
+hands-on Mathlib fluency: naming conventions, search strategies, the
+algebra hierarchy. The fastest cure for ``I know the fact exists but
+not its name,'' which will be your main bottleneck after this book.
+\item \emph{The Lean Zulip} (\code{leanprover.zulipchat.com}) --- where
+the community lives. Unusually welcoming to beginners; search before
+asking, then ask well: a minimal example plus the goal state gets
+expert answers in hours.
+\item Bernstein \& Lange, \emph{Faster addition and doubling on
+elliptic curves} (2007) --- the completeness proof
+Chapter~\ref{ch:pyramid}'s worked example walked; readable with this
+book's preparation, and a model of what ``designed for implementers''
+mathematics looks like.
+\item The RFC for EdDSA (RFC 8032) and FIPS 205 (SLH-DSA) --- the two
+signature schemes as deployed, cofactor-$8$s, encodings, and address
+words included. Read their verification sections against
+Chapters~\ref{ch:pyramid} and~\ref{ch:secondsummit} and notice how much
+sharper your questions have become.
+\item Project Everest / HACL$^{*}$ and Fiat Crypto --- the two other
+major verified-crypto lineages (F$^{*}$-based and Coq-based
+respectively), both shipping in real TLS stacks and browsers. Reading
+their claims with your Chapter~\ref{ch:honesty} toolkit is instructive
+in both directions: the methods differ, the honest-boundary discipline
+rhymes.
+\end{itemize}
+
+\begin{checkpoint}
+The book's ending is a beginning, so the final checkpoint is prospective:
+you should be able to (1) explain the two acts of verification and why
+the second one cannot be delegated to the first; (2) audit a stranger's
+attestation --- leaf, cones, exclusions, inclusion proof --- in fifteen
+minutes with your own machine's verdict; (3) name the frontier brick
+\emph{you} could lay, and what the control repository says a finished
+one looks like; and (4) name the next proof you intend to write. The
+authors of the companion repositories left the scaffolding up on
+purpose.
+\end{checkpoint}

chapters/glossary.tex

@@ -5,8 +5,8 @@
 \newcommand{\gloss}[1]{\par\smallskip\noindent{\bfseries #1.}\ }
 
 \gloss{Axiom-clean} Of a theorem: \lean{\#print axioms} reports exactly
-Lean's standard trio \lean{[propext, Classical.choice, Quot.sound]} and
+Lean's standard trio --- \lean{propext}, \lean{Classical.choice},
-nothing else. The gold standard for shipped certificates
+\lean{Quot.sound} --- and nothing else. The gold standard for shipped certificates
 (Chapter~\ref{ch:honesty}).
 
 \gloss{Bounds invariant} A predicate limiting how large limbs may grow
@@ -82,23 +82,40 @@ fact and the cost of verifying a certificate for it --- the engine of
 Pratt certificates, proof kernels, and (in disguise) the P-vs-NP
 question (Chapter~\ref{ch:prime}).
 
-\gloss{Hasse bound} An elliptic curve over $\Fp$ has $p + 1 - t$ points
-with $|t| \le 2\sqrt{p}$; the thirty-second sanity check for any
-claimed group order (Chapter~\ref{ch:pyramid}).
-
 \gloss{Fold} Reducing an overflow of the representation (weight
 $2^{255}$ and above) back into range using the modulus identity
 $2^{255} \equiv 19$; costs exactly one multiple of $p$ per unit folded
 (Chapter~\ref{ch:denotation}; Interlude).
 
+\gloss{FORS} Forest Of Random Subsets: SLH-DSA's few-time signature ---
+$k$ small Merkle trees, one secret revealed per tree, all recomputed
+roots compressed and certified by the hypertree; reuse degrades
+gracefully instead of breaking, which is what buys statelessness
+(Chapter~\ref{ch:secondsummit}).
+
 \gloss{Goal state} The proof assistant's board: hypotheses above the
 turnstile $\vdash$, obligation below. Reading it is the core tactic
 skill (Chapter~\ref{ch:tactics}).
 
+\gloss{Hash oracle} A hash function entering a proof as an \emph{axiom}
+with assumed functional behavior and no proven properties; the five
+SLH-DSA verify-path oracles are the standing example, and the audit's
+cone table shows exactly which certificate leans on which
+(Chapter~\ref{ch:secondsummit}).
+
+\gloss{Hasse bound} An elliptic curve over $\Fp$ has $p + 1 - t$ points
+with $|t| \le 2\sqrt{p}$; the thirty-second sanity check for any
+claimed group order (Chapter~\ref{ch:pyramid}).
+
 \gloss{Headroom} Bits of slack between a limb's payload (e.g.\ 51 bits)
 and its machine word (64 bits); the budget lazy carries spend
 (Chapter~\ref{ch:why}).
 
+\gloss{Hypertree} SLH-DSA's tower of $d$ Merkle-tree layers, each tree's
+root signed by a one-time key of the layer above --- a virtual structure
+of $2^h$ keys that is never materialized: any path can be recomputed
+from a seed, and one root pins it all (Chapter~\ref{ch:secondsummit}).
+
 \gloss{Inductive type} A type defined by listing its constructors
 exhaustively (\lean{Nat}: \lean{zero} and \lean{succ}). Grants both
 pattern matching and the induction principle (Chapters~\ref{ch:lean},
@@ -129,6 +146,12 @@ certifies $p$ prime, given certificates for the $q$'s
 \gloss{Radix} The base of a limb representation ($2^{51}$ for the
 dalek field, $4$ for this book's toy system).
 
+\gloss{SLH-DSA} The stateless hash-based digital signature algorithm of
+FIPS~205 (descended from SPHINCS\textsuperscript{+}): FORS under a
+hypertree of Winternitz chains, built from hash functions and nothing
+else --- no structure for Shor's algorithm to attack
+(Chapter~\ref{ch:secondsummit}).
+
 \gloss{Specification (spec)} The precise statement a program is proven
 to satisfy. The two-clause shape for arithmetic: bounds propagation
 plus value equation. A proof is only as good as its spec
@@ -157,3 +180,9 @@ documented, and machine-visible (Chapters~\ref{ch:rust},
 theorem: \emph{(1)} the operation succeeds and its output satisfies the
 (possibly widened) bounds invariant; \emph{(2)} the output's denotation
 equals the ideal result (Chapter~\ref{ch:denotation}; Interlude).
+
+\gloss{Winternitz chain (WOTS\textsuperscript{+})} A hash chain
+$c_0, F(c_0), F(F(c_0)), \dots$ signing one digit by revealing the
+chain value at the digit's position; the verifier walks the remaining
+steps to the published end. A checksum makes forward-walking forgeries
+self-defeating (Chapter~\ref{ch:secondsummit}).

check-book.py

@@ -0,0 +1,412 @@
+#!/usr/bin/env python3
+"""check-book.py — the measured half of the book's button (see check-book.sh).
+
+Every check compares a claim PRINTED IN THE BOOK against a value MEASURED
+from the sources, the built PDF, or the sibling repositories at the moment
+it runs. No expected value is carried in this file when it can be derived;
+where the book's prose states a number, the number is parsed OUT OF THE
+PROSE and compared against the measurement — so editing either side alone
+turns the button red.
+
+Populations are derived by property, never by glob or label (the log's
+entries/ directory contains convenience copies; leaves are the files whose
+names are six digits AND whose index field matches their position).
+
+Exit 0 only if every applicable check passed. A check that could not
+measure (missing sibling repo without BOOK_LOCAL_ONLY=1) is a FAILURE,
+not a skip: a gate that read nothing must not look like a clean gate.
+"""
+
+import json
+import os
+import re
+import subprocess
+import sys
+
+FAILS = []
+PASSES = []
+
+
+def ok(label, detail=""):
+    PASSES.append(label)
+    print(f"  ok    {label}" + (f"  [{detail}]" if detail else ""))
+
+
+def fail(label, detail=""):
+    FAILS.append(label)
+    print(f"  FAIL  {label}" + (f"  [{detail}]" if detail else ""))
+
+
+def check(cond, label, detail=""):
+    (ok if cond else fail)(label, detail)
+
+
+def read(path):
+    with open(path, "r", errors="replace") as fh:
+        return fh.read()
+
+
+WORDS = {
+    "one": 1, "two": 2, "three": 3, "four": 4, "five": 5, "six": 6,
+    "seven": 7, "eight": 8, "nine": 9, "ten": 10, "eleven": 11,
+    "twelve": 12, "thirteen": 13, "fourteen": 14, "fifteen": 15,
+    "sixteen": 16, "seventeen": 17, "eighteen": 18, "nineteen": 19,
+    "twenty": 20, "forty-four": 44, "sixty-one": 61,
+}
+
+
+def main():
+    book = os.path.abspath(sys.argv[1] if len(sys.argv) > 1 else ".")
+    no_pdf = os.environ.get("SKIP_BUILD") == "1"
+    local_only = os.environ.get("BOOK_LOCAL_ONLY") == "1"
+    estate = os.environ.get("ESTATE_ROOT", os.path.dirname(book))
+    ltl = os.environ.get("LTL_DIR", os.path.join(estate, "lean-transparency-log"))
+    fips = os.environ.get("FIPS205_DIR", os.path.join(estate, "fips205-slhdsa-verified"))
+    p25519 = os.environ.get("P25519_FILE", os.path.join(
+        estate, "dalek-ed25519-verified", "verification", "Proofs", "P25519.lean"))
+
+    main_tex = read(os.path.join(book, "main.tex"))
+    readme = read(os.path.join(book, "README.md"))
+    chdir = os.path.join(book, "chapters")
+
+    # the publication-history block: its CURRENT-edition line is bound to
+    # measurements below; its historical lines are frozen and exempt from
+    # the whole-book claim scans, so strip the span for scanning purposes
+    mhist = re.search(r"% BEGIN PUBHIST.*?% END PUBHIST", main_tex, re.S)
+    pubhist = mhist.group(0) if mhist else ""
+    main_scan = main_tex.replace(pubhist, "")
+
+    # ── Phase 0: source hygiene ────────────────────────────────────────────
+    print("=== Phase 0: source hygiene ===")
+
+    inputs = re.findall(r"\\input\{(chapters/[^}]+)\}", main_tex)
+    missing = [i for i in inputs if not os.path.exists(os.path.join(book, i + ".tex"))]
+    check(not missing, "every \\input'd chapter file exists",
+          ",".join(missing) or f"{len(inputs)} inputs")
+    on_disk = {f"chapters/{f[:-4]}" for f in os.listdir(chdir) if f.endswith(".tex")}
+    orphans = sorted(on_disk - set(inputs))
+    check(not orphans, "no orphan .tex under chapters/", ",".join(orphans) or "none")
+
+    chapter_files = [i for i in inputs if re.search(r"chapters/ch\d\d-", i)]
+    nums = [int(re.search(r"ch(\d\d)-", c).group(1)) for c in chapter_files]
+    n_ch = len(chapter_files)
+    check(nums == list(range(1, n_ch + 1)) and n_ch > 0,
+          "chapter files contiguous ch01..chNN in input order", f"N={n_ch}")
+
+    for cf in chapter_files + ["chapters/interlude-by-hand"]:
+        src = read(os.path.join(book, cf + ".tex"))
+        envs = re.findall(r"\\end\{([a-z]+)\}", src)
+        check(envs and envs[-1] == "checkpoint",
+              f"{cf.split('/')[-1]}: last environment is checkpoint",
+              envs[-1] if envs else "no environments")
+
+    for cf in chapter_files:
+        num = int(re.search(r"ch(\d\d)-", cf).group(1))
+        src = read(os.path.join(book, cf + ".tex"))
+        n_ex = len(re.findall(r"\\exercise\{", src))
+        sols = re.findall(r"\\solhead\{(\d+)\.(\d+)\}", src)
+        n_sol = len(sols)
+        label = f"ch{num:02d}: exercises == solutions"
+        if n_ex == 0 and n_sol == 0:
+            ok(label, "none (allowed)")
+            continue
+        good = (n_ex == n_sol
+                and all(int(a) == num for a, _ in sols)
+                and [int(b) for _, b in sols] == list(range(1, n_sol + 1)))
+        check(good, label, f"{n_ex} exercises, solheads {[a+'.'+b for a, b in sols]}")
+
+    isrc = read(os.path.join(book, "chapters/interlude-by-hand.tex"))
+    i_ex = len(re.findall(r"Exercise I\.\d", isrc))
+    i_sol = re.findall(r"\\solhead\{I\.(\d+)\}", isrc)
+    check(i_ex == len(i_sol) and [int(x) for x in i_sol] == list(range(1, len(i_sol) + 1)),
+          "interlude: exercises == solutions", f"{i_ex} vs {len(i_sol)}")
+
+    # ── Phase 1 leftovers: claims about the built PDF ──────────────────────
+    print("=== Phase 1b: built-PDF claims ===")
+    if no_pdf:
+        print("  (skipped: SKIP_BUILD=1 — build phase runs in check-book.sh)")
+    else:
+        pdf = os.path.join(book, "main.pdf")
+        info = subprocess.run(["pdfinfo", pdf], capture_output=True, text=True).stdout
+        pages = int(re.search(r"Pages:\s+(\d+)", info).group(1))
+        check(pages >= 100, "PDF built and non-trivial", f"{pages} pages")
+        txt = subprocess.run(["pdftotext", pdf, "-"],
+                             capture_output=True, text=True).stdout
+        bad = [l for l in txt.splitlines() if "??" in l]
+        check(not bad, "no unresolved references ('??') in rendered PDF",
+              bad[0][:60] if bad else "clean")
+        page_claims = re.findall(r"(\d{2,4}) pages", readme + main_scan)
+        if page_claims:
+            for pc in page_claims:
+                check(int(pc) == pages, f"page-count claim {pc} == built {pages}")
+        else:
+            ok("no page-count claim outside the history block (nothing to bind)")
+
+        # publication history: the current-edition line is a live claim
+        med = re.search(r"\\textbf\{(\w+) edition\} --- published "
+                        r"([A-Za-z]+ \d+, \d{4}): (\w+)\s*\n?chapters, "
+                        r"(\d+) pages", pubhist)
+        if not (pubhist and med):
+            fail("publication-history block with parseable current-edition line",
+                 "missing" if not pubhist else "line not parseable")
+        else:
+            check(WORDS.get(med.group(3)) == n_ch,
+                  "current edition's chapter count == measured",
+                  f"{med.group(3)} vs {n_ch}")
+            check(int(med.group(4)) == pages,
+                  "current edition's page count == built PDF",
+                  f"{med.group(4)} vs {pages}")
+            # committed PDF must carry the current-edition line: this is what
+            # a GitHub visitor downloads, and it must not lag the sources
+            if os.path.isdir(os.path.join(book, ".git")):
+                blob = subprocess.run(["git", "-C", book, "show", "HEAD:main.pdf"],
+                                      capture_output=True)
+                tmp = os.path.join(book, ".committed-main.pdf.tmp")
+                with open(tmp, "wb") as fh:
+                    fh.write(blob.stdout)
+                ctxt = subprocess.run(["pdftotext", tmp, "-"],
+                                      capture_output=True, text=True).stdout
+                os.unlink(tmp)
+                check(f"published {med.group(2)}" in ctxt,
+                      "COMMITTED main.pdf carries the current-edition line "
+                      "(the PDF a visitor downloads is not stale)",
+                      med.group(2))
+            else:
+                ok("committed-PDF binding skipped (no git repo here)")
+
+    # ── Phase 2: internal countable claims ─────────────────────────────────
+    print("=== Phase 2: internal countable claims ===")
+
+    m = re.search(r"(\w+(?:-\w+)?) chapters", readme)
+    check(m and WORDS.get(m.group(1)) == n_ch,
+          f"README chapter count == {n_ch}", m.group(0) if m else "no claim found")
+
+    ch01 = read(os.path.join(book, "chapters/ch01-why-verify.tex"))
+    m = re.search(r"the next (\w+)\s*\nchapters|the next (\w+) chapters", ch01)
+    word = (m.group(1) or m.group(2)) if m else None
+    check(word is not None and WORDS.get(word) == n_ch - 1,
+          f"ch01 'the next N chapters' == {n_ch - 1}", word or "claim not found")
+
+    # stale-total scan is scoped to the front matter, where whole-book totals
+    # live; inside a chapter, "N chapters" is a positional count checked next
+    for stale in ("twelve chapters", "thirteen chapters"):
+        hits = [name for name, txt in (("main.tex", main_scan), ("README.md", readme))
+                if stale in txt]
+        check(not hits, f"no stale '{stale}' in front matter (history block exempt)",
+              ",".join(hits) or "clean")
+    # any "spent N chapters" phrase inside chapter chNN counts its predecessors
+    for cf in chapter_files:
+        num = int(re.search(r"ch(\d\d)-", cf).group(1))
+        for word in re.findall(r"spent (\w+) chapters",
+                               read(os.path.join(book, cf + ".tex"))):
+            check(WORDS.get(word) == num - 1,
+                  f"ch{num:02d} 'spent {word} chapters' == its {num - 1} predecessors")
+
+    m = re.search(r"A (\w+)-week plan", main_tex)
+    plan_word = WORDS.get(m.group(1)) if m else None
+    weeks = [int(x) for x in re.findall(r"^(\d+)\s+&", main_tex, re.M)]
+    ranges = [int(b) for _, b in re.findall(r"^(\d+)--(\d+)\s+&", main_tex, re.M)]
+    max_week = max(weeks + ranges) if (weeks or ranges) else 0
+    check(plan_word == max_week and plan_word is not None,
+          "week-plan heading == max week row", f"{plan_word} vs {max_week}")
+    check(f"{m.group(1)}-week" in main_tex.replace("A " + m.group(1), "", 1),
+          "instructors paragraph agrees with plan heading")
+
+    m = re.search(r"Chapters ([\d, ]+ and \d+) carry one", main_tex)
+    if not m:
+        fail("discussion-exercise roster claim parseable", "pattern not found")
+    else:
+        claimed = set(int(x) for x in re.findall(r"\d+", m.group(1)))
+        measured = set()
+        for cf in chapter_files:
+            num = int(re.search(r"ch(\d\d)-", cf).group(1))
+            src = read(os.path.join(book, cf + ".tex"))
+            if re.search(r"\\exercise\{\(Discussion\)", src):
+                measured.add(num)
+        check(claimed == measured, "discussion-exercise roster == measured",
+              f"claimed {sorted(claimed)}, measured {sorted(measured)}")
+
+    ch13 = read(os.path.join(book, "chapters/ch13-second-summit.tex"))
+    n, h, d, hp, a, k, w, ln2, m_dig = 16, 63, 7, 9, 12, 14, 16, 3, 30
+    length = 2 * n + ln2
+    split = ((k * a + 7) // 8, (h - h // d + 7) // 8, (h + 8 * d - 1) // (8 * d))
+    check(sum(split) == m_dig and split == (21, 7, 2), "digest split recomputes",
+          str(split))
+    sig_bytes = n * (1 + k * (1 + a) + d * (length + hp))
+    check(sig_bytes == 7856, "signature size recomputes", str(sig_bytes))
+    fixed = k * a + d * hp + d + 1 + 1 + k          # H paths + T's + Hmsg + FORS leaves
+    best = 0
+    for csum in range(0, 32 * (w - 1) + 1):
+        sh = csum << 4
+        digs = [(sh >> 12) & 0xF, (sh >> 8) & 0xF, (sh >> 4) & 0xF]
+        best = max(best, csum + sum((w - 1) - x for x in digs))
+    worst = fixed + d * best
+    check(fixed == 254 and best == 510 and worst == 3824,
+          "oracle pricing recomputes (fixed/per-layer-max/worst)",
+          f"{fixed}/{best}/{worst}")
+
+    def see_saw(csum):
+        sh = csum << 4
+        return ((sh >> 12) & 0xF, (sh >> 8) & 0xF, (sh >> 4) & 0xF)
+    check(see_saw(480) == (1, 14, 0) and see_saw(479) == (1, 13, 15)
+          and see_saw(256) == (1, 0, 0), "checksum worked examples recompute")
+
+    for token, why in [("7{,}856", "signature size"), ("254", "fixed oracle calls"),
+                       ("510", "per-layer max"), ("3{,}824", "worst total"),
+                       ("(1, 14, 0)", "csum 480 digits"),
+                       ("(1, 13, 15)", "csum 479 digits"),
+                       ("57{,}344", "FORS forest"), ("231", "H count"),
+                       ("$21 + 7 + 2 = 30$", "digest split")]:
+        check(token in ch13, f"ch13 prints {why}", token)
+    check(len(str(2**255 - 19)) == 77, "'77-digit prime' recomputes")
+
+    # ── Phase 3: cross-repo congruence ─────────────────────────────────────
+    print("=== Phase 3: cross-repo congruence ===")
+    if local_only:
+        print("  (SKIPPED: BOOK_LOCAL_ONLY=1 — cross-repo claims NOT verified)")
+    else:
+        # the log: leaves by property, not by glob
+        entdir = os.path.join(ltl, "entries")
+        if not os.path.isdir(entdir):
+            fail("lean-transparency-log present", entdir)
+        else:
+            leaf_files = sorted(f for f in os.listdir(entdir)
+                                if re.fullmatch(r"\d{6}\.json", f))
+            leaves = [json.load(open(os.path.join(entdir, f))) for f in leaf_files]
+            idx_ok = all(lf["index"] == i for i, lf in enumerate(leaves))
+            n_leaves = len(leaves)
+            check(idx_ok, "leaf indexes contiguous and match filenames",
+                  f"{n_leaves} leaves")
+
+            for where, src, pat in [
+                    ("title page '19 entries'", main_tex, r"(\d+) entries and counting"),
+                    ("preface 'nineteen pieces'", main_tex, r"lists (\w+)\s*\npieces|lists (\w+) pieces"),
+                    ("ch01 tryit '19 entries'", ch01, r"(\d+) entries, each one"),
+                    ("ch14 'nineteen leaves'",
+                     read(os.path.join(book, "chapters/ch14-attestation-protocol.tex")),
+                     r"log's (\w+) leaves")]:
+                mm = re.search(pat, src)
+                val = None
+                if mm:
+                    g = next(g for g in mm.groups() if g)
+                    val = int(g) if g.isdigit() else WORDS.get(g)
+                check(val == n_leaves, f"{where} == measured {n_leaves}", str(val))
+
+            def certs(i):
+                return leaves[i]["leaf"]["attestation"]["certificates"]
+
+            def comp(i):
+                return leaves[i]["leaf"]["attestation"]["subject"]["component"]
+
+            ed = {"dalek-ed25519-verified", "anza-ed25519-verified",
+                  "risc0-ed25519-verified", "betrusted-ed25519-verified"}
+            check({comp(i) for i in (13, 14, 15, 16)} == ed,
+                  "leaves 13-16 subjects are the four ed25519 forks")
+            check(all(len(certs(i)) == 44 for i in (13, 14, 15, 16)),
+                  "'forty-four certificates each' == measured",
+                  str([len(certs(i)) for i in (13, 14, 15, 16)]))
+            check(27 + 13 + 4 == 44, "27 main + 13 scalar + 4 apex == 44")
+            check(comp(17) == "ltl-accumulator-verified"
+                  and len(certs(17)) == 61 and len(certs(12)) == 61,
+                  "'sixty-one' accumulator certificates == measured (leaves 12, 17)")
+            check(all(len(certs(i)) == 16 for i in range(0, 12)),
+                  "'sixteen' early-leaf certificates == measured (leaves 0-11)")
+
+            s18 = leaves[18]["leaf"]["attestation"]
+            check(s18["subject"]["component"] == "fips205-slhdsa-verified"
+                  and s18["subject"]["kind"] == "slh_dsa",
+                  "leaf 18 subject is fips205-slhdsa-verified / slh_dsa")
+            check(len(certs(18)) == 11 and "eleven certificates" in ch13,
+                  "'eleven certificates' == measured", str(len(certs(18))))
+            by_name = {c["name"]: c for c in certs(18)}
+            for want in ("fips205.chain_free_loop_eq", "fips205.xmss_loop_eq",
+                         "fips205.ht_loop_eq", "fips205.wots_csum_loop_eq",
+                         "fips205.slh_verify_128s_accepts_iff"):
+                check(want in by_name, f"leaf 18 carries {want}")
+            kernel3 = {"propext", "Classical.choice", "Quot.sound"}
+            apex = set(by_name["fips205.slh_verify_128s_accepts_iff"]["observed_axioms"])
+            oracles = {f"verify_mono.oracle.{x}"
+                       for x in ("f", "h", "h_msg", "t_l", "t_len")}
+            check(apex == kernel3 | oracles, "apex cone == kernel-3 + five oracles")
+            ht = set(by_name["fips205.ht_loop_eq"]["observed_axioms"])
+            check(ht == kernel3 | {"verify_mono.oracle.f", "verify_mono.oracle.h",
+                                   "verify_mono.oracle.t_l"},
+                  "ht cone is f,h,t_l (the book's table row, by property not name)")
+            plumb = sum(1 for c in certs(18) if set(c["observed_axioms"]) == kernel3)
+            check(plumb == 4, "four kernel-3-only plumbing certificates", str(plumb))
+            check(all(c["status"] == "proven" and c["axiom_status"] == "clean"
+                      and set(c["observed_axioms"]) == set(c["expected_axioms"])
+                      for c in certs(18)), "leaf 18: all proven, clean, cones exact")
+
+            heads = [json.loads(l) for l in
+                     open(os.path.join(ltl, "sth-history.jsonl")) if l.strip()]
+            dual = [hd["tree_size"] for hd in heads
+                    if hd["signatures"].get("slh_dsa", {}).get("status") == "signed"]
+            check(dual and min(dual) == 14,
+                  "'since tree 14' dual-signed heads == measured",
+                  f"first dual head size {min(dual) if dual else None}")
+            check(heads[-1]["tree_size"] == n_leaves,
+                  "final head size == leaf count")
+
+        # fips205 parameter card
+        funs = os.path.join(fips, "verification", "gen", "SlhVerify", "Funs.lean")
+        if not os.path.exists(funs):
+            fail("fips205-slhdsa-verified present", funs)
+        else:
+            fsrc = read(funs)
+            mm = re.search(
+                r"def verify_mono\.slh_verify_128s.*?types\.SlhDsaSig "
+                r"(\d+)#usize (\d+)#usize (\d+)#usize (\d+)#usize (\d+)#usize "
+                r"(\d+)#usize.*?slh_verify_internal_free (\d+)#usize (\d+)#usize",
+                fsrc, re.S)
+            if not mm:
+                fail("fips205 entry-point parameters parseable")
+            else:
+                A, D, HP, K, LEN, N = (int(mm.group(i)) for i in range(1, 7))
+                H, M = int(mm.group(7)), int(mm.group(8))
+                W = int(re.search(r"def W : Std\.U32 := (\d+)#u32", fsrc).group(1))
+                repo = {"a": A, "d": D, "h'": HP, "k": K, "len": LEN,
+                        "n": N, "h": H, "m": M, "w": W}
+                card = {"a": a, "d": d, "h'": hp, "k": k, "len": length,
+                        "n": n, "h": h, "m": m_dig, "w": w}
+                check(repo == card, "ch13 parameter card == extracted entry point",
+                      str(repo))
+                for sym, val in card.items():
+                    tok = f"{sym} = {val}"
+                    check(tok in ch13 or f"= {val}" in ch13,
+                          f"ch13 prints {sym} = {val}")
+
+        # the 71-digit Q, digit for digit
+        if not os.path.exists(p25519):
+            fail("P25519.lean present for Q comparison", p25519)
+        else:
+            psrc = read(p25519)
+            mq = re.search(r"theorem prime_(\d{60,})", psrc)
+            ch07 = read(os.path.join(book, "chapters/ch07-primality-certificates.tex"))
+            mb = re.search(r"Q = ([0-9\\a-z{} ]+?),\s*\n?\\\]", ch07, re.S)
+            q_repo = mq.group(1) if mq else None
+            q_book = re.sub(r"\D", "", mb.group(1)) if mb else None
+            check(q_repo is not None and q_book == q_repo,
+                  "ch07's printed Q == repository's Q, digit for digit",
+                  f"book {len(q_book or '')} digits, repo {len(q_repo or '')} digits")
+            check(q_repo is not None and len(q_repo) == 71 and "71-digit" in ch07,
+                  "'71-digit' claim recomputes")
+
+    # ── verdict ────────────────────────────────────────────────────────────
+    print()
+    total = len(PASSES) + len(FAILS)
+    if FAILS:
+        print(f"RED: {len(FAILS)} of {total} claims diverge from measured reality:")
+        for f in FAILS:
+            print(f"  - {f}")
+        sys.exit(1)
+    if local_only:
+        print(f"LOCAL CHECKS GREEN ({total} checks) — cross-repo claims NOT "
+              f"verified (BOOK_LOCAL_ONLY=1). This is not ALL GREEN.")
+        sys.exit(0)
+    print(f"ALL CLAIM CHECKS GREEN ({total} checks)")
+    sys.exit(0)
+
+
+if __name__ == "__main__":
+    main()

check-book.sh

@@ -0,0 +1,126 @@
+#!/usr/bin/env bash
+# check-book.sh — THE button for verifying-crypto-with-lean.
+#
+# This script is the only source of the words "ALL GREEN" for this
+# repository. It rebuilds the book from the committed sources and then
+# verifies that every countable claim printed in the book matches reality
+# measured at run time: chapter counts, the week plan, exercise/solution
+# pairing, the recomputed SLH-DSA arithmetic, the transparency log's leaf
+# and certificate counts, the first dual-signed head, the extracted
+# parameter card, and the 71-digit Q — digit for digit.
+#
+# Phases
+#   0   source hygiene        (check-book.py)
+#   1   build                 (tectonic via build.sh; fails on TeX errors)
+#   1b  built-PDF claims      (pages, unresolved refs, page-count claims)
+#   2   internal congruence   (counts and arithmetic inside the book)
+#   3   cross-repo congruence (log + fips205 + P25519 siblings)
+#
+# Environment
+#   BOOK_LOCAL_ONLY=1   skip phase 3; verdict is downgraded, never ALL GREEN
+#   ESTATE_ROOT         parent dir of the sibling repos (default: ../)
+#   LTL_DIR / FIPS205_DIR / P25519_FILE   override individual siblings
+#
+# Modes
+#   ./check-book.sh              full run
+#   ./check-book.sh --selftest   adversarial self-test: mutates copies of the
+#                                sources and asserts the button turns RED
+set -euo pipefail
+cd "$(dirname "$0")"
+HERE="$(pwd)"
+
+selftest() {
+  echo "=== SELFTEST: the button must go red for the right reasons ==="
+  command -v python3 >/dev/null || { echo "python3 required"; exit 1; }
+  # the mutated copy keeps the REAL sibling repos: only the book is mutated,
+  # so a red verdict proves the mutation was caught, not that a repo was lost
+  local ESTATE; ESTATE="${ESTATE_ROOT:-$(dirname "$HERE")}"
+  local tmp out pass=0 fail=0
+  run_copy() {
+    tmp="$(mktemp -d)"; mkdir -p "$tmp/chapters"
+    cp main.tex README.md "$tmp/"; cp chapters/*.tex "$tmp/chapters/"
+  }
+  run_mutated() { # $1 description, $2 mutation cmd, $3 expected FAIL substring
+    run_copy
+    ( cd "$tmp" && eval "$2" )
+    out="$(SKIP_BUILD=1 ESTATE_ROOT="$ESTATE" python3 "$HERE/check-book.py" "$tmp" 2>&1)" \
+      && { echo "  FAIL  mutation NOT caught: $1"; fail=$((fail+1)); rm -rf "$tmp"; return; }
+    if echo "$out" | grep -q "FAIL.*$3"; then
+      echo "  ok    caught for the right reason: $1"; pass=$((pass+1))
+    else
+      echo "  FAIL  red, but not on the expected check ('$3'): $1"; fail=$((fail+1))
+      echo "$out" | grep "  FAIL" | head -3
+    fi
+    rm -rf "$tmp"
+  }
+  # control: the unmutated copy must pass (proves the harness can go green)
+  run_copy
+  if SKIP_BUILD=1 ESTATE_ROOT="$ESTATE" python3 "$HERE/check-book.py" "$tmp" >/dev/null 2>&1; then
+    echo "  ok    control: unmutated copy passes"; pass=$((pass+1))
+  else
+    echo "  FAIL  control: unmutated copy should pass but is red"; fail=$((fail+1))
+    SKIP_BUILD=1 ESTATE_ROOT="$ESTATE" python3 "$HERE/check-book.py" "$tmp" | grep FAIL || true
+  fi
+  rm -rf "$tmp"
+
+  run_mutated "chapter-count claim drifts (fourteen -> thirteen)" \
+    "sed -i 's/fourteen chapters/thirteen chapters/' README.md" \
+    "README chapter count"
+  run_mutated "a solution deleted (ch13 solhead 13.6 dropped)" \
+    "sed -i 's/\\\\solhead{13.6}/% gone/' chapters/ch13-second-summit.tex" \
+    "ch13: exercises == solutions"
+  run_mutated "one digit of the 71-digit Q changed in ch07" \
+    "sed -i 's/740582127325613583022312264370627886761/740582127325613583022312264370627886762/' chapters/ch07-primality-certificates.tex" \
+    "printed Q == repository"
+  run_mutated "leaf-count claim drifts (nineteen leaves -> twenty)" \
+    "sed -i \"s/log's nineteen leaves/log's twenty leaves/\" chapters/ch14-attestation-protocol.tex" \
+    "ch14 'nineteen leaves'"
+  run_mutated "worst-case arithmetic drifts (3,824 -> 3,689)" \
+    "sed -i 's/3{,}824/3{,}689/' chapters/ch13-second-summit.tex" \
+    "ch13 prints worst total"
+  run_mutated "a chapter stops ending on its checkpoint" \
+    "printf '\n\\\\begin{aha}\nstray box after the checkpoint\n\\\\end{aha}\n' >> chapters/ch05-numbers-and-automation.tex" \
+    "ch05.*last environment is checkpoint"
+  run_mutated "week plan and heading diverge (heading says fifteen)" \
+    "sed -i 's/A fourteen-week plan/A fifteen-week plan/' main.tex" \
+    "week-plan heading"
+
+  echo
+  if [ "$fail" -gt 0 ]; then
+    echo "SELFTEST RED: $fail defect(s) in the button itself"; exit 1
+  fi
+  echo "SELFTEST GREEN: $pass/$pass (control + 7 mutations, each caught on its own check)"
+  exit 0
+}
+
+[ "${1:-}" = "--selftest" ] && selftest
+
+echo "=== Phase 1: build ==="
+BUILDLOG="$(mktemp)"
+./build.sh 2>&1 | tee "$BUILDLOG"
+command -v pdfinfo >/dev/null && command -v pdftotext >/dev/null || {
+  echo "FAIL: poppler-utils (pdfinfo/pdftotext) required"; exit 1; }
+
+# Print-quality gate: an overfull box past 10pt is text visibly leaving the
+# margin or a border slicing through content. The 2026-08-08 visual audit
+# found the two worst rendering defects in the book had been announced in
+# every build log as 80pt/73pt overfull warnings — and ignored. Never again.
+if grep -oE "Overfull \\\\hbox \([0-9]+\.[0-9]+pt" "$BUILDLOG" \
+   | grep -oE "[0-9]+\.[0-9]+" | awk '$1 > 10 {bad=1} END {exit bad}'; then
+  echo "  ok    no overfull box exceeds 10pt (print-quality gate)"
+else
+  echo "  FAIL  overfull boxes past 10pt — text is leaving the page:"
+  grep -E "Overfull \\\\hbox \([0-9]{2,}" "$BUILDLOG" | sort -u | head -5
+  rm -f "$BUILDLOG"; exit 1
+fi
+rm -f "$BUILDLOG"
+
+python3 "$HERE/check-book.py" "$HERE"
+
+echo
+if [ "${BOOK_LOCAL_ONLY:-0}" = "1" ]; then
+  echo "VERDICT: build green + local claims green; cross-repo NOT verified."
+else
+  echo "ALL GREEN — the book builds and every countable claim matches"
+  echo "measured reality (sources, PDF, transparency log, extracted code)."
+fi

main.tex

@@ -7,13 +7,13 @@
 \begin{titlepage}
 \pagecolor{ink}\color{paper}
 \begin{tikzpicture}[remember picture,overlay]
-  % faint pyramid motif — the proof pyramid the book builds toward
+  % the proof pyramid the book climbs — drawn in solid mixed colors, never
+  % transparency: low-opacity fills on a dark ground render as smudge and
+  % vary by viewer. Crisp thin outlines make it read as intentional.
   \foreach \i/\w in {0/5.4, 1/4.2, 2/3.0, 3/1.8}{
-    \fill[paper,opacity=0.05] ($(current page.center)+(-\w/2,{-2.2+\i*0.95})$)
+    \draw[paper!30!ink, line width=0.5pt, fill=paper!8!ink]
-      rectangle ++(\w,0.8);
+      ($(current page.center)+(-\w/2,{-3.0+\i*0.95})$) rectangle ++(\w,0.8);
   }
-  \node[anchor=south west,paper,opacity=0.06,scale=6,font=\ttfamily]
-    at ($(current page.south west)+(0.5,0.4)$) {$\forall$};
 \end{tikzpicture}
 \vspace*{3.2cm}
 {\fontsize{15}{18}\selectfont\scshape\color{accent} a hands-on course in\par}
@@ -21,24 +21,71 @@
 {\fontsize{40}{44}\selectfont\bfseries Verifying Cryptography\\[2pt] with Lean 4\par}
 \vspace{0.8cm}
 {\fontsize{15}{20}\selectfont\color{paper}
-From \code{1+1=2} to a machine-checked proof that\\ real elliptic-curve code is correct.\par}
+From {\ttfamily 1+1=2} to a machine-checked proof that\\ real elliptic-curve code is correct.\par}
 \vfill
 {\large\color{paper} A curriculum for the curious undergraduate ---\\
 no prior formal-verification or Lean experience assumed.\par}
 \vspace{0.8cm}
-{\color{ink2}\rule{\linewidth}{0.6pt}}
+{\color{paper!40!ink}\rule{\linewidth}{0.6pt}\par}
-\vspace{0.3cm}
+\vspace{0.15cm}
-{\small\color{paper} Companion to the \code{*-ed25519-verified} and \code{pasta-pallas-verified}
+{\small\color{paper}\raggedright
-proof projects. \\ Every code snippet in this book runs. Every claim it makes about a proof, a proof assistant has checked.\par}
+Companion to a public transparency log of machine-checked proofs ---
+\textbf{\code{ltl.zkdefi.org}}, 19 entries and counting, one of them
+post-quantum. Open it on your phone now; by the last chapter you will be
+able to verify every entry yourself.\par
+\smallskip
+Every code snippet in this book runs. Every claim it makes about a proof,
+a proof assistant has checked.\par}
 \end{titlepage}
 \restoregeometry
 \pagecolor{paper}\color{ink}
 
+% BEGIN PUBHIST ==================== publication history =====================
+% The current-edition line is machine-checked by check-book.sh: its chapter
+% count and page count must match the built book, and the committed PDF must
+% contain it. Historical lines are frozen and exempt from the claim checks.
+\thispagestyle{empty}
+\vspace*{2cm}
+{\small
+\noindent\textbf{Second edition} --- published August 8, 2026: fourteen
+chapters, 132 pages.
+
+\medskip
+\noindent\emph{Publication history}
+\begin{itemize}[leftmargin=1.4em]
+\item \textbf{First edition}, July 3, 2026 --- twelve chapters and the
+  Interlude; expanded the same day with the pen-and-paper program and
+  in-book solution pathways (53 to 106 pages).
+\item July 28, 2026 --- the Attestation Protocol added as a thirteenth
+  chapter.
+\item \textbf{Second edition}, August 8, 2026 --- full didactic overhaul
+  (seven moves, from a seven-reader audit); new Chapter~13, \emph{The
+  Second Summit} (SLH-DSA, post-quantum); the Attestation Protocol becomes
+  the fourteen-chapter book's single finale; \code{check-book.sh} added ---
+  the script that verifies every countable claim in this book, including
+  the line at the top of this page, against measured reality.
+\end{itemize}
+
+\medskip
+\noindent The complete revision record is the git history of
+\code{github.com/saymrwulf/verifying-crypto-with-lean}.
+}
+\clearpage
+% END PUBHIST ================================================================
+
 % ===================== HOW TO READ =====================
 \chapter*{How to read this book}
 \markboth{How to read this book}{}
 \addcontentsline{toc}{chapter}{How to read this book}
 
+There is a public web page --- \code{ltl.zkdefi.org} --- that lists nineteen
+pieces of software, each stamped with a machine-checked proof that it does what
+it claims. One of those stamps was earned two days before the writer of that
+proof could make anyone else believe it; another belongs to a signature scheme
+built to survive a quantum computer. This book is the road from not
+understanding a single word on that page to being able to verify every entry on
+it yourself, and to add your own.
+
 You are about to learn one of the most powerful ideas in computer science: how
 to make a computer \emph{prove} that a program is correct --- not test it on a
 few inputs and hope, but establish, with the certainty of mathematics, that it
@@ -48,16 +95,13 @@ key a system ever generates.
 
 This book assumes you can program a little and remember a little high-school
 algebra. It assumes \textbf{nothing} about formal methods, proof assistants, or
-Lean. We start from \code{1 + 1 = 2} and end at a real, published,
+Lean. We start from \code{1 + 1 = 2} and end three summits later: real,
-machine-checked proof that the field arithmetic behind Ed25519 --- the signature
+published, machine-checked theorems about Ed25519 --- the signature scheme in
-scheme in your SSH client, your phone, and half the internet --- is correct.
+your SSH client, your phone, and half the internet --- then about a hash-based
+scheme built for the quantum era, and finally about the public log that lets a
+stranger check all of it without trusting anyone.
 
 \begin{itemize}[leftmargin=1.4em]
-  \item \textbf{The colored boxes each mean one thing.} A coral
-  \emph{big idea} box holds the load-bearing concept of a section. A grey
-  \emph{try it} box is an invitation to run something yourself. An amber
-  \emph{pitfall} box is a trap with its warning sign. A green \emph{aha} box is
-  an intuition meant to click. A framed \emph{checkpoint} ends each chapter.
   \item \textbf{Do the exercises.} Reading a proof is like watching someone
   swim. You learn by getting in the water. Solutions are in the \code{solutions/}
   folder, but consult them only after a real attempt.
@@ -73,6 +117,13 @@ strict compiler for it. Once you see proofs as programs, the fear evaporates and
 the fun begins.
 \end{aha}
 
+\noindent\emph{(That green box you just read is an ``aha'' --- an intuition
+meant to click. You will also meet coral \emph{big idea} boxes for
+load-bearing concepts, grey \emph{try it} boxes that ask you to run something,
+amber \emph{pitfall} boxes marking traps, and a framed \emph{checkpoint} at
+each chapter's end. That is the whole legend; you have now seen one in the
+wild.)}
+
 \subsection*{Working the pen-and-paper material}
 
 The notebook-ruled \emph{Pen and paper} boxes are not optional
@@ -94,8 +145,8 @@ then read --- in that order.
 The book is engineered for self-study, which makes it easy to teach
 from: every exercise carries an immediate pathway-then-answer solution,
 so contact hours can go to the parts that need a human --- discussing
-the discussion exercises (each chapter has one; they are the seminar
+the discussion exercises (Chapters 1, 7, 10, 11, and 13 carry one; they
-seeds), pair-debugging the Lean files, and auditing real repositories
+are the seminar seeds), pair-debugging the Lean files, and auditing real repositories
 together (Appendix~\ref{app:tour} is a ready-made lab session). Grading
 suggestion: collect the pen-and-paper worked examples \emph{reproduced
 from memory} rather than problem sets --- the book's bet is that a
@@ -105,11 +156,11 @@ Lean solution files compile against the pinned toolchain in the repo;
 \code{lake build Solutions} is your answer key's answer key. Prerequisites
 in practice: one programming course (any language) and comfort with
 high-school algebra; no number theory, no logic, no Rust. The
-thirteen-week plan below has been paced so the two hard climbs ---
+fourteen-week plan below has been paced so the two hard climbs ---
 Chapter~9 and the Interlude --- each get a full week with nothing else
 competing.
 
-\subsection*{A thirteen-week plan}
+\subsection*{A fourteen-week plan}
 
 For self-study or a seminar, the book paces naturally as a semester:
 
@@ -130,7 +181,9 @@ For self-study or a seminar, the book paces naturally as a semester:
 10    & Interlude                        & the complete by-hand verification \\
 11    & Ch.~10--11                       & audit drill on a stranger's repo \\
 12    & Ch.~12 + \code{Ch12.lean}        & graduation: spec--refusal--fix--certificate \\
-13    & project                          & one open lemma or one solo bridge \\
+13    & Ch.~13                           & the checksum see-saw + the cone table, from memory \\
+14    & Ch.~14 + project                 & a fifteen-minute independent log verification;\\
+      &                                  & then one open lemma or one solo bridge \\
 \bottomrule
 \end{tabular}
 \end{center}
@@ -151,7 +204,8 @@ For self-study or a seminar, the book paces naturally as a semester:
 \input{chapters/ch10-verifying-a-field}
 \input{chapters/ch11-honesty-and-axioms}
 \input{chapters/ch12-the-pyramid}
-\input{chapters/ch13-attestation-protocol}
+\input{chapters/ch13-second-summit}
+\input{chapters/ch14-attestation-protocol}
 
 \appendix
 \input{chapters/appendix-toolkit}

preamble.tex

@@ -18,7 +18,8 @@
 \usepackage{fancyhdr}
 \usepackage{titlesec}
 \usepackage{booktabs}
-\usepackage[strings]{underscore} % plain _ works in text; math subscripts unaffected
+\usepackage[strings]{underscore}
+\usepackage{needspace} % plain _ works in text; math subscripts unaffected
 \usepackage{hyperref}
 
 % ---- palette -------------------------------------------------------------
@@ -105,67 +106,118 @@
 % Inline code: plain styled text (robust in tables/footnotes, unlike lstinline).
 % Also safe inside math mode (wraps itself in \text there).
 % Unicode symbols in inline code are handled by the declarations below.
-\newcommand{\inlinecode}[1]{\ifmmode\text{\ttfamily\small #1}\else{\ttfamily\small #1}\fi}
+% Inside code: never break at an underscore with a hyphen — a hyphen inside
+% a printed identifier is a lie in a book that teaches exact names.
+\newcommand{\codeguards}{\let\BreakableUnderscore\textunderscore\relax}
+% command-line double dash, kept visibly TWO hyphens in tt (they touch otherwise)
+\newcommand{\ddash}{-\kern0.10em-}
+\newcommand{\inlinecode}[1]{\ifmmode\text{\ttfamily\small\codeguards#1}\else{\ttfamily\small\codeguards#1}\fi}
 \newcommand{\lean}[1]{\inlinecode{#1}}
 \newcommand{\rust}[1]{\inlinecode{#1}}
 \newcommand{\code}[1]{\inlinecode{#1}}
-\DeclareUnicodeCharacter{2192}{\ensuremath{\to}}          % →
+% Unicode in Lean listings, both engines. pdfTeX maps code points via
-\DeclareUnicodeCharacter{2190}{\ensuremath{\leftarrow}}   % ←
+% inputenc; XeTeX/Tectonic is natively Unicode but the tt font lacks the
-\DeclareUnicodeCharacter{2194}{\ensuremath{\leftrightarrow}} % ↔
+% glyphs, so newunicodechar substitutes the same math forms. BOTH branches
-\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}}      % ∀
+% derive from one list — edit both or the engines diverge (the build button
-\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}      % ∃
+% compiles under tectonic, the Mac under pdflatex; both must stay green).
-\DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}}       % ∧
+\ifdefined\XeTeXversion
-\DeclareUnicodeCharacter{2228}{\ensuremath{\vee}}         % ∨
+  \usepackage{newunicodechar}
-\DeclareUnicodeCharacter{00AC}{\ensuremath{\neg}}         % ¬
+  \newunicodechar{→}{\ensuremath{\to}} % →
-\DeclareUnicodeCharacter{2260}{\ensuremath{\neq}}         % ≠
+  \newunicodechar{←}{\ensuremath{\leftarrow}} % ←
-\DeclareUnicodeCharacter{2264}{\ensuremath{\leq}}         % ≤
+  \newunicodechar{↔}{\ensuremath{\leftrightarrow}} % ↔
-\DeclareUnicodeCharacter{2265}{\ensuremath{\geq}}         % ≥
+  \newunicodechar{∀}{\ensuremath{\forall}} % ∀
-\DeclareUnicodeCharacter{22A2}{\ensuremath{\vdash}}       % ⊢
+  \newunicodechar{∃}{\ensuremath{\exists}} % ∃
-\DeclareUnicodeCharacter{00B7}{\ensuremath{\cdot}}        % ·
+  \newunicodechar{∧}{\ensuremath{\wedge}} % ∧
-\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}}   % ℕ
+  \newunicodechar{∨}{\ensuremath{\vee}} % ∨
-\DeclareUnicodeCharacter{2124}{\ensuremath{\mathbb{Z}}}   % ℤ
+  \newunicodechar{¬}{\ensuremath{\neg}} % ¬
-\DeclareUnicodeCharacter{2113}{\ensuremath{\ell}}         % ℓ
+  \newunicodechar{≠}{\ensuremath{\neq}} % ≠
-\DeclareUnicodeCharacter{00D7}{\ensuremath{\times}}       % ×
+  \newunicodechar{≤}{\ensuremath{\leq}} % ≤
-\DeclareUnicodeCharacter{2208}{\ensuremath{\in}}          % ∈
+  \newunicodechar{≥}{\ensuremath{\geq}} % ≥
-\DeclareUnicodeCharacter{2211}{\ensuremath{\Sigma}}       % ∑
+  \newunicodechar{⊢}{\ensuremath{\vdash}} % ⊢
-\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}}       % ≡
+  \newunicodechar{·}{\ensuremath{\cdot}} % ·
-\DeclareUnicodeCharacter{2223}{\ensuremath{\mid}}         % ∣
+  \newunicodechar{ℕ}{\ensuremath{\mathbb{N}}} % ℕ
-\DeclareUnicodeCharacter{27E8}{\ensuremath{\langle}}      % ⟨
+  \newunicodechar{ℤ}{\ensuremath{\mathbb{Z}}} % ℤ
-\DeclareUnicodeCharacter{27E9}{\ensuremath{\rangle}}      % ⟩
+  \newunicodechar{ℓ}{\ensuremath{\ell}} % ℓ
-\DeclareUnicodeCharacter{1D53D}{\ensuremath{\mathbb{F}}}  % 𝔽
+  \newunicodechar{×}{\ensuremath{\times}} % ×
-\DeclareUnicodeCharacter{2080}{\ensuremath{{}_0}}         % ₀
+  \newunicodechar{∈}{\ensuremath{\in}} % ∈
-\DeclareUnicodeCharacter{2081}{\ensuremath{{}_1}}         % ₁
+  \newunicodechar{∑}{\ensuremath{\Sigma}} % ∑
-\DeclareUnicodeCharacter{2082}{\ensuremath{{}_2}}         % ₂
+  \newunicodechar{≡}{\ensuremath{\equiv}} % ≡
-\DeclareUnicodeCharacter{00B2}{\ensuremath{{}^2}}         % ²
+  \newunicodechar{∣}{\ensuremath{\mid}} % ∣
-\DeclareUnicodeCharacter{2075}{\ensuremath{{}^5}}         % ⁵
+  \newunicodechar{⟨}{\ensuremath{\langle}} % ⟨
-\DeclareUnicodeCharacter{2713}{\ensuremath{\checkmark}}   % ✓
+  \newunicodechar{⟩}{\ensuremath{\rangle}} % ⟩
-\DeclareUnicodeCharacter{2717}{\ensuremath{\times}}       % ✗
+  \newunicodechar{𝔽}{\ensuremath{\mathbb{F}}} % 𝔽
-\DeclareUnicodeCharacter{207B}{\ensuremath{{}^{-}}}       % ⁻
+  \newunicodechar{₀}{\ensuremath{{}_0}} % ₀
-\DeclareUnicodeCharacter{00B9}{\ensuremath{{}^{1}}}       % ¹
+  \newunicodechar{₁}{\ensuremath{{}_1}} % ₁
-\DeclareUnicodeCharacter{00B3}{\ensuremath{{}^{3}}}       % ³
+  \newunicodechar{₂}{\ensuremath{{}_2}} % ₂
-\DeclareUnicodeCharacter{2070}{\ensuremath{{}^{0}}}       % ⁰
+  \newunicodechar{²}{\ensuremath{{}^2}} % ²
-\DeclareUnicodeCharacter{2074}{\ensuremath{{}^{4}}}       % ⁴
+  \newunicodechar{⁵}{\ensuremath{{}^5}} % ⁵
-\DeclareUnicodeCharacter{2076}{\ensuremath{{}^{6}}}       % ⁶
+  \newunicodechar{✓}{\ensuremath{\checkmark}} % ✓
+  \newunicodechar{✗}{\ensuremath{\times}} % ✗
+  \newunicodechar{⁻}{\ensuremath{{}^{-}}} % ⁻
+  \newunicodechar{¹}{\ensuremath{{}^{1}}} % ¹
+  \newunicodechar{³}{\ensuremath{{}^{3}}} % ³
+  \newunicodechar{⁰}{\ensuremath{{}^{0}}} % ⁰
+  \newunicodechar{⁴}{\ensuremath{{}^{4}}} % ⁴
+  \newunicodechar{⁶}{\ensuremath{{}^{6}}} % ⁶
+\else
+  \DeclareUnicodeCharacter{2192}{\ensuremath{\to}}          % →
+  \DeclareUnicodeCharacter{2190}{\ensuremath{\leftarrow}}   % ←
+  \DeclareUnicodeCharacter{2194}{\ensuremath{\leftrightarrow}} % ↔
+  \DeclareUnicodeCharacter{2200}{\ensuremath{\forall}}      % ∀
+  \DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}      % ∃
+  \DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}}       % ∧
+  \DeclareUnicodeCharacter{2228}{\ensuremath{\vee}}         % ∨
+  \DeclareUnicodeCharacter{00AC}{\ensuremath{\neg}}         % ¬
+  \DeclareUnicodeCharacter{2260}{\ensuremath{\neq}}         % ≠
+  \DeclareUnicodeCharacter{2264}{\ensuremath{\leq}}         % ≤
+  \DeclareUnicodeCharacter{2265}{\ensuremath{\geq}}         % ≥
+  \DeclareUnicodeCharacter{22A2}{\ensuremath{\vdash}}       % ⊢
+  \DeclareUnicodeCharacter{00B7}{\ensuremath{\cdot}}        % ·
+  \DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}}   % ℕ
+  \DeclareUnicodeCharacter{2124}{\ensuremath{\mathbb{Z}}}   % ℤ
+  \DeclareUnicodeCharacter{2113}{\ensuremath{\ell}}         % ℓ
+  \DeclareUnicodeCharacter{00D7}{\ensuremath{\times}}       % ×
+  \DeclareUnicodeCharacter{2208}{\ensuremath{\in}}          % ∈
+  \DeclareUnicodeCharacter{2211}{\ensuremath{\Sigma}}       % ∑
+  \DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}}       % ≡
+  \DeclareUnicodeCharacter{2223}{\ensuremath{\mid}}         % ∣
+  \DeclareUnicodeCharacter{27E8}{\ensuremath{\langle}}      % ⟨
+  \DeclareUnicodeCharacter{27E9}{\ensuremath{\rangle}}      % ⟩
+  \DeclareUnicodeCharacter{1D53D}{\ensuremath{\mathbb{F}}}  % 𝔽
+  \DeclareUnicodeCharacter{2080}{\ensuremath{{}_0}}         % ₀
+  \DeclareUnicodeCharacter{2081}{\ensuremath{{}_1}}         % ₁
+  \DeclareUnicodeCharacter{2082}{\ensuremath{{}_2}}         % ₂
+  \DeclareUnicodeCharacter{00B2}{\ensuremath{{}^2}}         % ²
+  \DeclareUnicodeCharacter{2075}{\ensuremath{{}^5}}         % ⁵
+  \DeclareUnicodeCharacter{2713}{\ensuremath{\checkmark}}   % ✓
+  \DeclareUnicodeCharacter{2717}{\ensuremath{\times}}       % ✗
+  \DeclareUnicodeCharacter{207B}{\ensuremath{{}^{-}}}       % ⁻
+  \DeclareUnicodeCharacter{00B9}{\ensuremath{{}^{1}}}       % ¹
+  \DeclareUnicodeCharacter{00B3}{\ensuremath{{}^{3}}}       % ³
+  \DeclareUnicodeCharacter{2070}{\ensuremath{{}^{0}}}       % ⁰
+  \DeclareUnicodeCharacter{2074}{\ensuremath{{}^{4}}}       % ⁴
+  \DeclareUnicodeCharacter{2076}{\ensuremath{{}^{6}}}       % ⁶
+\fi
 
 % ---- pedagogical boxes: each means ONE thing ----------------------------
 % BIG IDEA — the load-bearing concept of a section.
-\newtcolorbox{bigidea}[1][]{enhanced,breakable,colback=accentsoft,
+\newtcolorbox{bigidea}[1][]{enhanced,colback=accentsoft,
   colframe=accent,boxrule=0.4pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
   fonttitle=\bfseries\color{paper},coltitle=paper,title={\faLightbulb\ The big idea},#1}
 % TRY IT — a hands-on invitation to run something.
-\newtcolorbox{tryit}[1][]{enhanced,breakable,colback=codebg,colframe=ink2,
+\newtcolorbox{tryit}[1][]{enhanced,colback=codebg,colframe=ink2,
   boxrule=0.4pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
   fonttitle=\bfseries\color{paper},coltitle=paper,title={\faTerminal\ Try it yourself},#1}
 % PITFALL — a trap, with its tell.
-\newtcolorbox{pitfall}[1][]{enhanced,breakable,colback=warnsoft,colframe=warn,
+\newtcolorbox{pitfall}[1][]{enhanced,colback=warnsoft,colframe=warn,
   boxrule=0.4pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
   fonttitle=\bfseries\color{paper},coltitle=paper,title={\faExclamationTriangle\ Pitfall},#1}
 % AHA — an intuition that clicks.
-\newtcolorbox{aha}[1][]{enhanced,breakable,colback=provensoft,colframe=proven,
+\newtcolorbox{aha}[1][]{enhanced,colback=provensoft,colframe=proven,
   boxrule=0.4pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
   fonttitle=\bfseries\color{paper},coltitle=paper,title={\faStar\ Aha},#1}
 % CHECKPOINT — end-of-chapter self-check.
-\newtcolorbox{checkpoint}[1][]{enhanced,breakable,colback=white,colframe=ink,
+\newtcolorbox{checkpoint}[1][]{enhanced,colback=white,colframe=ink,
   boxrule=0.6pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
   fonttitle=\bfseries\color{paper},coltitle=paper,title={\faFlagCheckered\ Checkpoint},#1}
 
@@ -190,7 +242,8 @@
 \newtcolorbox{worked}[1]{enhanced,breakable,colback=white,colframe=ink2,
   boxrule=0.4pt,leftrule=2.6pt,arc=1pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
   colbacktitle=codebg,coltitle=ink,
-  fonttitle=\bfseries,title={\pennib\ Pen and paper: #1}}
+  fonttitle=\bfseries,title={\pennib\ Pen and paper: #1},
+  title after break={\pennib\ Pen and paper: #1 \emph{(continued)}}}
 \providecommand{\pennib}{\raisebox{-1pt}{\small$\angle$}}
 
 % exercises
@@ -200,7 +253,7 @@
 
 % solutions — immediately after each chapter's exercises.
 % Every solution leads with the PATHWAY (how to find it), then the answer.
-\newcommand{\solhead}[1]{\medskip\noindent%
+\newcommand{\solhead}[1]{\Needspace{4\baselineskip}\medskip\noindent%
   {\bfseries\color{proven}Solution #1.}\ }
 \newcommand{\pathway}{\par\smallskip\noindent{\itshape\color{ink2}Pathway.}\ }
 \newcommand{\answer}{\par\smallskip\noindent{\itshape\color{ink2}Answer.}\ }