diff --git a/README.md b/README.md index 2102e68..a97858e 100644 --- a/README.md +++ b/README.md @@ -22,13 +22,10 @@ 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, -before chapter 13 was committed (2026-07-28) — rebuild with the command -below to get the current book; the committed PDF lags the committed -sources until the next rebuild on a LaTeX-equipped machine. No prior Lean or formal methods assumed; high-school algebra -and a little programming suffice. +repo (`./build.sh`, tectonic, no root needed). No prior Lean or formal +methods assumed; high-school algebra and a little programming suffice. 1. **Why Verify?** — the carry bug testing cannot find 2. **Meet Lean** — programs, types, inductive data @@ -43,11 +40,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; 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 +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: @@ -91,7 +89,14 @@ install while the cache downloads. ## 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 +127,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, - 2026-07-06 build — predates ch13) is rebuilt from these sources. -- The PDF in the repo is built from the committed sources by the command - above — but the committed build currently predates chapter 13 (see the - honesty note at the top); rebuild it yourself if you don't trust binaries - (good instinct), and you will get the thirteen-chapter book. + constant was machine-verified before typesetting. +- The PDF in the repo is built from the committed sources by `./build.sh` + and recommitted alongside source changes; rebuild it yourself if you + don't trust binaries (good instinct), and you should get the same + fourteen-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 diff --git a/chapters/appendix-walkthroughs.tex b/chapters/appendix-walkthroughs.tex index be83912..4deeebf 100644 --- a/chapters/appendix-walkthroughs.tex +++ b/chapters/appendix-walkthroughs.tex @@ -178,6 +178,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 -the pyramid'' item points at it; the \code{CONTRIBUTING} notes there will -treat you as what you now are: someone who has done this before. +frontier today is the paused Pasta curve layer, and chapter 12's ``Where +you come in'' subsection points at it; the \code{CONTRIBUTING} notes there +will treat you as what you now are: someone who has done this before. diff --git a/chapters/ch01-why-verify.tex b/chapters/ch01-why-verify.tex index db202a2..c796c1e 100644 --- a/chapters/ch01-why-verify.tex +++ b/chapters/ch01-why-verify.tex @@ -170,7 +170,7 @@ 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 twelve +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. @@ -184,9 +184,12 @@ prime, and watched it agree; by Chapter~9 you will read real Rust translated into Lean and understand the one idea (the \emph{denotation function}) that makes the translation trustworthy; by Chapter~12 you will stand on the apex and read the signature-verification theorem for the actual code in your SSH -client. 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. +client; by Chapter~13 you will climb a \emph{second} pyramid --- the +post-quantum entry you just saw in the log, built from hashes alone --- and +by Chapter~14 you will verify the log itself, so that nothing in this story +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 diff --git a/chapters/ch12-the-pyramid.tex b/chapters/ch12-the-pyramid.tex index 79439e3..34a0002 100644 --- a/chapters/ch12-the-pyramid.tex +++ b/chapters/ch12-the-pyramid.tex @@ -377,7 +377,7 @@ 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 @@ -385,23 +385,8 @@ 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. - -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{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} +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. \subsection*{Where you come in} @@ -418,49 +403,6 @@ saving this for an expert. Frontier work in machine-checked cryptography is, right now, undergraduate-accessible, and every chapter before this one was the access. -\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 \code{exercises/Ch09.lean}, the file \code{exercises/Ch12.lean} plants a @@ -570,8 +512,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 --- -which was the promise on the book's cover, kept. +you can audit a verification paper's abstract in ninety seconds --- the +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$. @@ -586,11 +528,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} -intend to write. The authors of the companion repositories left the -scaffolding up on purpose. +and say precisely why it is hard. The first pyramid is finished --- every +question mark from the opening figure resolved into a theorem. But its +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} diff --git a/chapters/ch13-second-summit.tex b/chapters/ch13-second-summit.tex new file mode 100644 index 0000000..c1e5039 --- /dev/null +++ b/chapters/ch13-second-summit.tex @@ -0,0 +1,620 @@ +\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 +\code{python3 verify.py --receipt +receipts/fips205-slhdsa-verified.receipt.json} --- 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} diff --git a/chapters/ch13-attestation-protocol.tex b/chapters/ch14-attestation-protocol.tex similarity index 73% rename from chapters/ch13-attestation-protocol.tex rename to chapters/ch14-attestation-protocol.tex index d220a49..8b9eeda 100644 --- a/chapters/ch13-attestation-protocol.tex +++ b/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,7 +217,7 @@ 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. @@ -236,14 +238,14 @@ 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{checkpoint} +\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 --all} --- plain Python for the hashing, the \code{openssl} binary for signatures, and it \emph{fails closed} without - them (Section~\ref{ch:attestation} taught you why ``couldn't check'' must + 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. @@ -257,7 +259,7 @@ the mirror and run the verifier. commit, the certificate list, the \emph{observed} axiom cones, the machine protection, and the stated exclusions. \end{itemize} -\end{checkpoint} +\end{tryit} The log's nineteen leaves map onto this book. Leaves 13--16 attest the four ed25519 repositories whose pyramid you climbed in @@ -268,11 +270,10 @@ 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 estate's first post-quantum subject: eleven certificates -over the SLH-DSA-SHA2-128s \emph{verification} path (FIPS~205), whose apex -states that the extracted verifier accepts exactly when the recomputed -Merkle root matches --- tree recursions under a hash-oracle boundary, the -same proof shapes you met in the pyramid, on a hash-based signature scheme. +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 @@ -293,7 +294,90 @@ 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}), 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. +(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} diff --git a/chapters/glossary.tex b/chapters/glossary.tex index 5908995..4a3d087 100644 --- a/chapters/glossary.tex +++ b/chapters/glossary.tex @@ -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}). diff --git a/main.pdf b/main.pdf index 66b5563..3caae07 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.tex b/main.tex index 1a8050e..6d851b7 100644 --- a/main.tex +++ b/main.tex @@ -45,9 +45,10 @@ claim it makes about a proof, a proof assistant has checked.\par} 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 survived quantum-resistant -cryptography. 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. +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 @@ -58,9 +59,11 @@ 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, -machine-checked proof that the field arithmetic behind Ed25519 --- the signature -scheme in your SSH client, your phone, and half the internet --- is correct. +Lean. We start from \code{1 + 1 = 2} and end three summits later: real, +published, machine-checked theorems about Ed25519 --- the signature scheme in +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{Do the exercises.} Reading a proof is like watching someone @@ -106,8 +109,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 -seeds), pair-debugging the Lean files, and auditing real repositories +the discussion exercises (Chapters 1, 7, 10, 11, and 13 carry one; they +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 @@ -117,11 +120,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: @@ -142,7 +145,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} @@ -163,7 +168,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}