verifying-crypto-with-lean/chapters/ch01-why-verify.tex

\chapter{Why Verify? The Bug That Testing Cannot Find}
\label{ch:why}

\section{A story about one carry bit}

Here is the entire bug that this book exists because of:

\begin{lstlisting}
  h[4] += carry;              // propagate the top limb's overflow
- // (missing: one more conditional subtraction of p)
+ 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
test happens to catch the bug. Every unit test passes. Every integration test
passes. Fuzzers shrug. The code ships.

\begin{pitfall}
``It passed all the tests'' means: it worked on the inputs we tried. For a
32-bit function there are four billion inputs and exhaustive testing is
feasible. A field element in Ed25519 is $255$ bits. The number of input
\emph{pairs} to a two-argument field operation is about $10^{153}$ --- more
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}
One hit per $2^{64}$ trials, and $2^{64} \approx 1.8 \times 10^{19}$. At a
billion tests a second that is $1.8 \times 10^{10}$ seconds to expect a
single failure --- about \textbf{580 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 that is the \emph{optimistic} case: carry bugs cluster in exactly the
corners uniform sampling underweights, so in practice you wait longer than
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
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.)
\end{worked}

Why does cryptographic code have bugs of exactly this shape? Because of how it
must be written. To be fast and resistant to timing attacks, real
implementations represent a 255-bit number in several machine-word
\emph{limbs} (we will spend happy hours with limbs in
Chapter~\ref{ch:denotation}) and postpone expensive carry propagation as long
as possible. The rare inputs where a deferred carry finally overflows are
precisely the inputs no test generator stumbles on. The bug lives in the gap
between ``the arithmetic we meant'' and ``the arithmetic we wrote,'' and that
gap is only visible on a set of inputs of measure nearly zero.

\begin{worked}{where exactly the danger zone sits --- the headroom budget}
You can locate the habitat of every delayed-carry bug with one line of
arithmetic, using the real Ed25519 parameters. The implementation stores a
field element as five limbs, each meant to carry $51$ bits of payload, in
$64$-bit machine words. The slack between payload and word is the
\emph{headroom}:
\[
64 - 51 = 13 \text{ bits of headroom per limb.}
\]
Adding two elements limb-wise adds their limbs, so a freshly reduced limb
(value $< 2^{51}$) can absorb additions --- but each addition can roughly
double the limb, i.e.\ spend up to one bit of headroom. How many lazy
additions before a limb can reach the $64$-bit cliff? We need
\[
k \cdot (2^{51}-1) \;<\; 2^{64}
\qquad\Longleftrightarrow\qquad
k \;\le\; \frac{2^{64}}{2^{51}} = 2^{13} = 8192 .
\]
So the code may skip carry propagation for thousands of additions --- a huge
performance win --- \emph{provided someone, somewhere, is counting}. The
2014-species bug is precisely a miscount: a code path where the running
total of spent headroom exceeds the budget on inputs shaped just so. Notice
what kind of fact the budget is: a \emph{quantified arithmetic invariant}
(``for all reachable values, limb $< 2^{51+j}$ after $j$ additions'') ---
exactly the kind of statement a test cannot establish and a proof assistant
eats for breakfast. When Chapter~\ref{ch:field} makes ``bounds clauses''
feel bureaucratic, remember this box: the bounds clause \emph{is} the
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 the private key itself: published
attacks in the ``invalid-curve'' and fault-injection families turn a
\emph{single} faulty group operation into full key recovery --- the attacker
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}

What if, instead of sampling inputs, we could make a statement about
\emph{all} of them --- and have a machine check that statement with the same
rigor a compiler checks syntax?

\begin{bigidea}
A \textbf{formal proof of correctness} is a mathematical argument, written in
a language precise enough for a computer to verify, that a program satisfies
its specification on \emph{every} input. Not sampled. Not probabilistic.
Every input, forever, or the proof does not check.
\end{bigidea}

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.\footnote{You may have heard of Rocq
(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,
powerful automation, beautiful notation --- is scaffolding whose only job is
to produce a proof object the kernel accepts. The kernel is a few thousand
lines of code that does one thing: check that each step of a proof follows
from the previous ones by a fixed set of rules. If the kernel accepts, the
theorem holds. If it does not, no amount of confidence, seniority, or good
intentions makes the program correct.

\begin{aha}
Here is the emotional core of formal verification, and it is worth
internalizing early: \textbf{the proof assistant is not your examiner, it is
your collaborator}. It never gets tired, never skips a case, never says
``obviously.'' Every hour you spend arguing with it is an hour a bug did not
survive. People who love proof assistants love them the way climbers love a
good belayer.
\end{aha}

\section{What we will actually verify}

This book is not a tour of toy examples. It is the curriculum companion to a
set of real verification projects in which the arithmetic core of
\textbf{Ed25519} --- the elliptic-curve signature scheme used by SSH, Signal,
TLS, and most cryptocurrency systems --- was machine-checked in Lean~4,
starting from the actual Rust source code of the
\code{curve25519-dalek} library and several of its production forks.

The proofs are organized as a pyramid. Each layer states the correctness of
one abstraction level and rests on the layer beneath it:

\begin{center}
\begin{tikzpicture}[
  lay/.style={draw=ink2,thick,rounded corners=2pt,align=center,minimum height=0.95cm},
  note/.style={font=\small\color{ink2},align=left,anchor=west}
]
  \node[lay,fill=accentsoft,minimum width=2.8cm]  (sig) at (0,3.45) {\textbf{Signature}\\[-2pt]\small EdDSA verify};
  \node[lay,fill=warnsoft,minimum width=5.2cm]    (sca) at (0,2.3)  {\textbf{Scalar arithmetic mod $\boldsymbol{\ell}$}};
  \node[lay,fill=provensoft,minimum width=7.6cm]  (grp) at (0,1.15) {\textbf{Group law} \small (twisted Edwards points)};
  \node[lay,fill=codebg,minimum width=10cm]       (fld) at (0,0)    {\textbf{Field arithmetic in $\Fp$}, \small $p = 2^{255}-19$};
  \node[note] at (5.6,0)    {limbs, carries, multiplication};
  \node[note] at (5.6,1.15) {point addition is complete \& correct};
  \node[note] at (5.6,2.3)  {the group order $\ell$, reduction};
  \node[note] at (5.6,3.45) {the equation $sB = R + kA$,\\ checked from the raw bytes};
\end{tikzpicture}
\end{center}

\begin{tryit}
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 twelve
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}

By the end of this book you will be able to read --- and extend --- the real
proofs at every layer of this pyramid. To make that concrete, here is what
you will personally be able to \emph{do}, and roughly when: by Chapter~7 you
will have handed a paranoid kernel a certificate that a 77-digit number is
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.

\begin{bigidea}
\textbf{The ratchet rule of this book.} Every load-bearing idea is worked
at least twice: once at \emph{napkin scale} (a modulus like $13$, numbers
you can invert by scanning), and once at \emph{real scale} --- the actual
77-digit constants of Ed25519, printed in full, with no digits hidden and
no artificial zeros. The napkin run teaches the moves; the real-size run
proves the moves are the whole story, because they are \emph{identical} ---
only the digits get longer, and wherever raw size genuinely exceeds paper
(a 77-digit square root, say) the book says so explicitly and shows you
how to audit the machine's work instead (witnesses, small clocks,
certificates). If a step ever feels like a leap, back up one worked
example: the missing rung is there, at the smaller size.
\end{bigidea}

\section{Proofs versus tests: the honest comparison}

Formal verification is not magic, and this book will never pretend otherwise.
It is worth being precise, right now, about what a machine-checked proof does
and does not give you.

\begin{center}
\begin{tabular}{@{}p{0.44\linewidth}p{0.48\linewidth}@{}}
\toprule
\textbf{Testing} & \textbf{Proving} \\
\midrule
Checks sampled inputs & Checks \emph{all} inputs \\
Cheap to start, cheap to run & Expensive to write, cheap to re-check \\
Finds bugs & Establishes their absence (w.r.t.\ the spec) \\
Trusts nothing & Trusts the spec, the model, the kernel \\
Silent about \emph{why} code is right & The proof \emph{is} the why \\
\bottomrule
\end{tabular}
\end{center}

That word \emph{spec} in the right column is the fine print, and it matters
enormously. A proof shows that code satisfies a specification. If the
specification says the wrong thing --- or says nothing, or is accidentally
trivial --- the proof is worthless no matter how green the checkmark. A
recurring theme of this book (it gets its own chapter,
Chapter~\ref{ch:honesty}) is how to read a verification claim skeptically:
What exactly was proven? Against which model of the code? Resting on which
axioms?

\begin{aha}
The most dangerous artifact in formal methods is not a wrong proof --- the
kernel prevents those. It is a \emph{correct proof of the wrong statement}.
Learning to smell those is as important as learning to write proofs at all.
\end{aha}

\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 --- and each one is an advantage
\emph{you} inherit the moment you start:

\begin{enumerate}[leftmargin=1.6em]
\item \textbf{You start on a million lines of proved mathematics.} Lean~4
  ships with \emph{Mathlib} --- finite fields, elliptic curves, number theory,
  already formalized and checked. You do not build the tower from bare axioms;
  you walk onto a finished floor and add one room.
\item \textbf{You verify the code that ships, not a story about it.} Tools
  called \emph{Charon} and \emph{Aeneas} mechanically translate real Rust into
  Lean, so what you reason about is \emph{derived} from the deployed source
  rather than hand-copied by someone who might have copied it wrong
  (Chapter~\ref{ch:rust}). This is the difference between verifying software
  and verifying an essay about software.
\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
\emph{possible for a well-prepared person in finite time} --- and preparing
you is exactly what this book is for.

\begin{tryit}
You do not need anything installed yet, but if you want to run code from
Chapter~2 onward, install Lean now. One command:
\begin{lstlisting}
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
\end{lstlisting}
Then open the \code{exercises/} folder of this repository in VS~Code with the
\emph{Lean 4} extension. The orange progress bar you will see is the proof
checker working through the file --- your new collaborator saying hello.
\end{tryit}

\section*{Exercises}

\exercise{A function takes two 255-bit inputs and is buggy on exactly one
input pair. Assume you can test $10^{9}$ random pairs per second. Estimate the
expected time to find the bug by random testing, in multiples of the age of
the universe ($\approx 4\times10^{17}$ seconds). You may approximate freely;
the point is the order of magnitude.}

\exercise{Give an example, from your own programming experience, of a bug that
survived a test suite. What property would a specification have needed to
state in order to exclude it?}

\exercise{(Discussion) A colleague says: ``Our crypto library is audited by
three firms every year; formal verification is redundant.'' Name one class of
defect audits are better at than proofs, and one class where proofs are
strictly stronger.}

\exercise{Redo the headroom budget for a hypothetical radix-$26$
representation on $32$-bit words (ten limbs of $26$ bits for a 255-bit
value, a real design used on small CPUs). How many bits of headroom per
limb? How many lazy additions fit in the budget? Compare with the
radix-51/64-bit numbers and state which design must reduce more often.}

\section*{Solutions and pathways}
\solutionsintro

\solhead{1.1}
\pathway The only inputs that reveal the bug form a set of size $1$ inside
a set of size $2^{510}$, so a uniformly random test hits it with
probability $2^{-510}$; expected number of trials is $2^{510}$ (waiting
time of a geometric distribution). Then it is the Chapter-1 conversion
drill: powers of two $\to$ powers of ten $\to$ seconds $\to$ universes.
\answer Expected trials $2^{510} \approx 10^{153.5}$. At $10^9$ per second:
$10^{153.5 - 9} = 10^{144.5}$ seconds. Divide by the age of the universe,
$4 \times 10^{17}$ s:
\[
\frac{10^{144.5}}{4 \times 10^{17}} \approx 10^{126.9}
\quad\text{--- about } 10^{127} \text{ universe-ages.}
\]
Any answer within a few orders of magnitude is ``correct'': the lesson is
that no engineering factor (faster farms, smarter fuzzing schedules) dents
a number with $127$ digits of margin.

\solhead{1.2}
\pathway Pick a bug whose trigger was a \emph{property of the input}, not a
coding typo --- those are the ones a spec excludes. Then ask: what is the
universally quantified sentence that is false in the buggy program?
\answer (Model answer.) A JSON parser that crashed on deeply nested arrays
survived a big test suite: no test nested past depth $50$. The
specification that excludes it must \emph{quantify over all inputs}:
``for every input string, the parser terminates and returns either a value
or a well-formed error'' --- termination-for-all is exactly what the tests
never said. The general shape to remember: test suites assert
$P(x_1), \dots, P(x_n)$; specifications assert $\forall x,\, P(x)$; bugs
live in the gap.

\solhead{1.3}
\pathway Sort defect classes by \emph{whether their badness is expressible
as a violated formal property of the code}. Audits see things that are not
properties of the code; proofs cover input space no human can.
\answer Audits win at: flaws in the \emph{specification itself} and its
surroundings --- wrong protocol choice, misuse-prone APIs, side channels
outside the model, deployment and key-handling practice. A proof of the
wrong spec passes; a good auditor smells that the spec is wrong. Proofs are
strictly stronger at: input-space coverage for the stated property ---
carry bugs, overflow corners, algebraic edge cases on a measure-zero slice.
The honest synthesis: audits examine the \emph{claim}, proofs guarantee the
\emph{claim's body}. A serious system wants both, aimed at their targets.

\solhead{1.4}
\pathway Same two lines as the worked example, new constants: headroom
$= \text{word} - \text{radix}$; budget $= 2^{\text{headroom}}$.
\answer Headroom $32 - 26 = 6$ bits, so at most $2^{32}/2^{26} = 2^{6} =
64$ lazy additions --- against $8192$ for radix-51/64-bit, a budget $128$
times tighter. The radix-26 design must interleave reductions far more
often, and its correctness argument has $128$ times less slack for
miscounting --- one concrete reason ports of crypto code to small targets
are disproportionately bug-prone, and why per-fork verification
(Chapter~\ref{ch:field}) is not paranoia.

\begin{checkpoint}
Before moving on, you should be able to explain to a friend:
(1) why testing fundamentally cannot establish correctness of a 255-bit
arithmetic function; (2) what a proof assistant's kernel is and why its small
size matters; (3) what a proof of correctness actually promises --- and the
role the specification plays in that promise.
\end{checkpoint}