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

Verifying Cryptography with Lean 4: complete 12-chapter curriculum

Browse source 
- 53-page LaTeX/TikZ book (main.pdf + full sources): from zero background
  to reading the real Ed25519/Pasta verification projects
- runnable exercises with sorry-holes + complete solutions for chapters
  2-7, 9, 12; every solution file compiles clean (zero errors, no sorry)
  against Lean v4.30.0-rc2 + Mathlib 5450b53e
- lake project pinned to the same toolchain/Mathlib the solutions were
  verified with; students fetch the Mathlib cache, never build it
- honesty ledger in README: what was machine-checked and how

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
saymrwulf 2026-07-03 09:44:40 +02:00
commit 45048d4898
35 changed files with 3483 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
.gitignore vendored Normal file
View file

@ -0,0 +1,10 @@
*.aux
build/
build2.log
build.log
.lake/
lake-manifest.json
*.log
*.olean
*.out
*.toc

88
README.md Normal file
View file

@ -0,0 +1,88 @@
# Verifying Cryptography with Lean 4
**A hands-on curriculum for undergraduates with zero formal-verification
background** — from `1 + 1 = 2` to reading (and extending) real,
machine-checked proofs that production elliptic-curve code is correct.
This is the educational companion to a family of verification projects in
which the arithmetic core of Ed25519 (from
[curve25519-dalek](https://github.com/dalek-cryptography/curve25519-dalek)
and three production forks) and the Pasta curves' field layer were
machine-checked in Lean 4 against models extracted from the actual Rust
sources:
| Companion project | What is verified there |
|---|---|
| [dalek-ed25519-verified](https://github.com/saymrwulf/dalek-ed25519-verified) | field 𝔽ₚ + Edwards group law + scalar foundations, upstream dalek |
| [anza-ed25519-verified](https://github.com/saymrwulf/anza-ed25519-verified) | same layers, Solana's fork, its own extraction |
| [risc0-ed25519-verified](https://github.com/saymrwulf/risc0-ed25519-verified) | same layers, RISC Zero's fork |
| [betrusted-ed25519-verified](https://github.com/saymrwulf/betrusted-ed25519-verified) | same layers, Betrusted's fork |
| [pasta-pallas-verified](https://github.com/saymrwulf/pasta-pallas-verified) | Pallas modulus primality (Lucas/Pratt), Montgomery foundations |
| [formal-verification-control](https://github.com/saymrwulf/formal-verification-control) | the method: invariants, terrain map, failure map, tooling |
## The book
**[`main.pdf`](main.pdf)** — twelve chapters, ~50 pages, full color, built
with LaTeX/TikZ from the sources in this repo. 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
3. **Propositions as Types** — Curry–Howard: proofs *are* programs
4. **Tactics** — proving as a dialogue with the goal state
5. **Numbers and Automation** — `omega`, `ring`, `norm_num`, `decide`, and the `simp` discipline
6. **Modular Arithmetic** — clock worlds, fields, why 2²⁵⁵ − 19
7. **Primality Certificates** — convincing a paranoid kernel a 77-digit number is prime
8. **From Rust to Lean** — the Charon/Aeneas extraction pipeline
9. **The Denotation Bridge** — the commuting square at the heart of it all
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
Each chapter ends in exercises; boxed **Big idea / Try it / Pitfall / Aha /
Checkpoint** elements carry the didactic load. Everything the book claims
about the companion projects reflects their actual, auditable state —
including open frontiers.
## The exercises (they run!)
`exercises/ChNN.lean` are working files with `sorry` holes;
`solutions/ChNN.lean` are complete. **Every solution file compiles with
zero errors** against the pinned toolchain (Lean `v4.30.0-rc2`, Mathlib
`5450b53e`); solutions to proof exercises contain no `sorry`.
Setup (one-time, ~5 min + Mathlib cache download):
```bash
# 1. install elan (Lean version manager) if you haven't:
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
# 2. fetch the Mathlib build cache (do NOT build Mathlib yourself):
cd verifying-crypto-with-lean
lake exe cache get
# 3. open the folder in VS Code with the "Lean 4" extension, or:
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.
## Building the book
Any TeX Live ≥ 2023 with `tikz`, `tcolorbox`, `listings`, `lmodern`:
```bash
pdflatex main.tex && pdflatex main.tex # twice for the TOC
```
## Honesty ledger
In the spirit of Chapter 11:
- All `solutions/*.lean` were compiled (and their `#eval` outputs checked
against their comments) at authoring time with the pinned versions above.
- Exercise templates compile with `sorry` warnings only.
- The book's claims about the companion projects (what is proven, what is
frontier) mirror those repos' own READMEs and TRUSTED-BASE ledgers at the
time of writing; the repos, not this book, are the source of truth.
- The PDF in the repo is built from the committed sources by the command
above; rebuild it yourself if you don't trust binaries (good instinct).

215
chapters/ch01-why-verify.tex Normal file
View file

@ -0,0 +1,215 @@
\chapter{Why Verify? The Bug That Testing Cannot Find}
\label{ch:why}
\section{A story about one carry bit}
In 2014, researchers examining widely deployed elliptic-curve code found
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
precise sense. One famous example, a carry-propagation flaw in an
implementation of curve25519 arithmetic, 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}
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.
And in cryptography, ``rare wrong answer'' does not mean ``rare small
glitch.'' Wrong field arithmetic can leak private keys: several published
attacks turn a single faulty group operation into full key recovery. The
stakes are not a corrupted pixel; they are every signature your machine has
ever made.
\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. Others you may have heard of: Rocq
(formerly Coq), Isabelle/HOL, Agda. The ideas transfer; the syntax differs.
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 $8sB = 8R + 8kA$};
\end{tikzpicture}
\end{center}
By the end of this book you will be able to read --- and extend --- the real
proofs at every layer of this pyramid. The journey looks like this:
\begin{itemize}[leftmargin=1.4em]
\item \textbf{Chapters 2--5} teach Lean itself, from \code{\#eval 1+1} to
proofs by induction and the automation that dispatches arithmetic goals.
\item \textbf{Chapters 6--7} build the mathematics: modular arithmetic, finite
fields, and how to convince a paranoid kernel that a 77-digit number is
prime.
\item \textbf{Chapters 8--9} cross the bridge from Rust to Lean: how real
code is translated into a form we can reason about, and the single most
important idea in the whole enterprise --- the \emph{denotation function}.
\item \textbf{Chapters 10--12} assemble the pyramid: field correctness, the
ethics of axioms and honest boundaries, and the layers above.
\end{itemize}
\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:
\begin{enumerate}[leftmargin=1.6em]
\item \textbf{Proof assistants matured.} Lean~4 is fast, pleasant, and comes
with \emph{Mathlib}, a library of over a million lines of formalized
mathematics --- finite fields and elliptic-curve ingredients included, so we
do not start from bare axioms.
\item \textbf{Translation pipelines appeared.} Tools like \emph{Charon} and
\emph{Aeneas} mechanically translate real Rust code into Lean definitions,
so the thing we verify is derived from the code that ships, not a
hand-transcribed approximation (Chapter~\ref{ch:rust}).
\item \textbf{Automation got serious.} Decision procedures like \lean{omega}
(linear integer arithmetic) and \lean{decide} discharge the boring 90\% of
goals, leaving humans the interesting 10\%.
\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.}
\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}

219
chapters/ch02-meet-lean.tex Normal file
View file

@ -0,0 +1,219 @@
\chapter{Meet Lean: A Language Where Programs and Proofs Live Together}
\label{ch:lean}
\section{First contact}
Lean~4 is two things wearing one syntax: a programming language (fast,
functional, compiled) and a proof assistant. You will learn both faces, but we
start with the friendlier one. Open a new file \code{Scratch.lean} and type:
\begin{lstlisting}[language=Lean]
#eval 1 + 1 -- 2
#eval 2 ^ 255 - 19 -- a 77-digit number, instantly
#eval "hello".length -- 5
\end{lstlisting}
\lean{\#eval} runs an expression and prints the result right in your editor.
Notice the second line: Lean's natural numbers are \emph{arbitrary precision}
by default. The number $2^{255}-19$ --- which will follow us through the whole
book --- is a perfectly ordinary value here, not an overflow.
\lean{\#check} asks a different question: not ``what is the value?'' but
``what is the \emph{type}?''
\begin{lstlisting}[language=Lean]
#check 1 + 1 -- 1 + 1 : Nat
#check "hello" -- "hello" : String
#check (1 : Int) - 5 -- Int
\end{lstlisting}
\begin{bigidea}
In Lean, \textbf{every expression has a type}, and the type checker verifies
every file before anything runs. This obsession with types is not
bureaucracy --- in Chapter~\ref{ch:pat} it will turn out to be the entire
mechanism by which proofs work. Learn to read \code{e : T} as ``$e$ is of
type $T$'' --- or, with a squint we will justify later, ``$e$ is
\emph{evidence} for $T$.''
\end{bigidea}
\section{Definitions and functions}
New names are introduced with \lean{def}:
\begin{lstlisting}[language=Lean]
def p : Nat := 2 ^ 255 - 19
def double (n : Nat) : Nat := 2 * n
def isEven (n : Nat) : Bool := n % 2 == 0
#eval double 21 -- 42
#eval isEven p -- false (p is odd, good: p is supposed to be prime!)
\end{lstlisting}
Three things to absorb from this snippet:
\begin{itemize}[leftmargin=1.4em]
\item Function application is written with a space: \lean{double 21}, not
\code{double(21)}. It looks strange for a week and then all other syntax
looks noisy forever after.
\item Every definition states its types: \lean{double} takes a \lean{Nat} and
returns a \lean{Nat}. Lean can often infer types, but in this book we write
them --- specifications are the whole game, and a type is a tiny
specification.
\item Definitions are \emph{immutable equations}, not instructions. There is
no ``assignment.'' \lean{p} \emph{is} $2^{255}-19$, forever.
\end{itemize}
Functions of several arguments simply take them in sequence, and functions
are values you can pass around:
\begin{lstlisting}[language=Lean]
def addMul (a b c : Nat) : Nat := a + b * c
def twice (f : Nat -> Nat) (x : Nat) : Nat := f (f x)
#eval twice double 10 -- 40
\end{lstlisting}
The type of \lean{twice} is worth staring at:
\lean{(Nat -> Nat) -> Nat -> Nat}. Arrows associate to the right, and a
multi-argument function is really a chain of single-argument ones --- this is
called \emph{currying}. Nothing about it needs memorizing now; it will become
muscle memory.
\section{Inductive types: building data from nothing}
Where do types like \lean{Nat} and \lean{Bool} come from? They are not
built-in magic. They are \emph{inductive types} --- data types defined by
listing every way to construct a value. Here is \lean{Bool}, exactly as the
core library defines it:
\begin{lstlisting}[language=Lean]
inductive Bool where
| false : Bool
| true : Bool
\end{lstlisting}
Read: ``a \lean{Bool} is either \lean{false} or \lean{true}, and there is no
other way to make one.'' That closed-world clause is what makes case analysis
--- and later, proofs by cases --- airtight.
Now the star of the show. The natural numbers, following Peano's 1889 idea:
\begin{lstlisting}[language=Lean]
inductive Nat where
| zero : Nat -- 0 exists
| succ (n : Nat) : Nat -- every number has a successor
\end{lstlisting}
Every natural number is \lean{zero} wrapped in finitely many \lean{succ}s:
the number 3 \emph{is} \lean{succ (succ (succ zero))}. (Lean stores big
numbers efficiently under the hood, but \emph{reasons} about them through
this two-case skeleton.) Functions on inductive types are defined by
\emph{pattern matching} --- one equation per constructor:
\begin{lstlisting}[language=Lean]
def add : Nat -> Nat -> Nat
| m, Nat.zero => m
| m, Nat.succ n => Nat.succ (add m n)
\end{lstlisting}
\begin{aha}
Look at what just happened. Addition --- the operation at the bottom of every
cryptosystem in this book --- is not an axiom or a CPU instruction here. It is
a \emph{two-line recursive program}, and every arithmetic fact we will ever
prove unwinds, ultimately, to these two equations. When Lean later claims
$a + b = b + a$ for \emph{all} numbers, it will be because the structure of
this definition forces it, not because anyone tested it.
\end{aha}
\begin{pitfall}
\lean{Nat} subtraction \emph{truncates}: \lean{\#eval (3 - 5 : Nat)} prints
\lean{0}, not $-2$, because natural numbers have nowhere to go below zero.
This single fact causes a large fraction of all beginner proof failures ---
an identity like $a - b + b = a$ is simply \emph{false} for \lean{Nat}. When
subtraction must mean subtraction, use \lean{Int}, or carry a hypothesis
$b \le a$. Real verification projects hit this constantly: machine arithmetic
wraps, truncates, and overflows, and the proofs must say so honestly.
\end{pitfall}
\section{Structures: records with guarantees}
The last data-building tool we need bundles several fields together:
\begin{lstlisting}[language=Lean]
structure Point where
x : Int
y : Int
def origin : Point := { x := 0, y := 0 }
#eval origin.x -- 0
\end{lstlisting}
A preview of why this matters to us: the Rust type
\rust{struct FieldElement51(pub [u64; 5])} --- five 64-bit limbs representing
one element of $\Fp$ --- will arrive in Lean (Chapter~\ref{ch:rust}) as
essentially a structure holding an array of five machine words. The
verification question of this entire book is: \emph{do operations on those
five words faithfully implement arithmetic in $\Fp$?} Structures are how the
data crosses the bridge.
\section{Namespaces, Mathlib, and reading error messages}
Real developments organize names in \lean{namespace} blocks
(\lean{Nat.add}, \lean{Point.x}) and import the mathematical library:
\begin{lstlisting}[language=Lean]
import Mathlib
open Nat
#check Nat.Prime -- the primality predicate, ready-made
#check ZMod -- integers mod n -- our Chapter 6 home
\end{lstlisting}
And a word of comfort about \emph{error messages}. You will see many. Lean's
are precise and honest, and the single most useful habit you can develop this
week is: \textbf{read the expected/actual types in the message, slowly}. A
message like
\begin{lstlisting}
type mismatch: argument has type Int but is expected to have type Nat
\end{lstlisting}
is not the compiler being difficult; it is a specification violation caught at
the cheapest possible moment. Verification is this same experience scaled up:
the machine holds the line, and the line is exactly where you drew it.
\begin{tryit}
Open \code{exercises/Ch02.lean}. It contains the definitions from this chapter
with a few holes marked \lean{sorry} (a placeholder Lean accepts with a loud
warning). Replace each with a working definition and watch the warnings
disappear. In particular: define \lean{mul : Nat -> Nat -> Nat} by recursion,
using \lean{add} --- the same bootstrapping order (add, then mul) the real
field proofs follow.
\end{tryit}
\section*{Exercises}
\exercise{Define \lean{pow : Nat -> Nat -> Nat} (by recursion on the
exponent) and check with \lean{\#eval} that \lean{pow 2 10 = 1024}.}
\exercise{Define \lean{fib : Nat -> Nat}. Then evaluate \lean{fib 32}. Notice
the pause --- naive recursion is exponential. (Lean's \lean{\#eval} is fast;
your algorithm is slow. The distinction matters when we later care about
\emph{what} is being computed versus \emph{how}.)}
\exercise{Write a structure \lean{Rational} with fields \lean{num : Int} and
\lean{den : Nat}, and a function \lean{Rational.add}. What property of
\lean{den} can your type \emph{not} enforce yet? (Keep your answer; Chapter~3
gives you the tool to fix it.)}
\begin{checkpoint}
You should now be able to: evaluate and type-check expressions with
\lean{\#eval}/\lean{\#check}; define functions, including recursive ones over
\lean{Nat}; explain what an inductive type is and recite the two constructors
of \lean{Nat}; and state from memory what \lean{Nat} subtraction does on
$3 - 5$, and why that will matter.
\end{checkpoint}

208
chapters/ch03-propositions-as-types.tex Normal file
View file

@ -0,0 +1,208 @@
\chapter{Propositions as Types: The Idea That Makes It All Work}
\label{ch:pat}
\section{A suspicious similarity}
Here are two things that look unrelated. First, a function that converts a
pair into something else:
\begin{lstlisting}[language=Lean]
def swap (pair : A x B) : B x A := (pair.2, pair.1)
\end{lstlisting}
Second, a fact of logic: \emph{if $A$ and $B$ both hold, then $B$ and $A$ both
hold.} To prove it, you would say: ``suppose I have evidence for $A$ and
evidence for $B$; then I can produce evidence for $B$ and evidence for $A$ ---
just present the same two pieces in the other order.''
That prose proof and that program are the \emph{same object}. The function
takes a pair of values and reorders it; the proof takes a pair of pieces of
evidence and reorders it. This is not an analogy or a teaching trick. It is a
theorem about logic and computation, discovered independently by logicians
(Curry, Howard) and now the load-bearing wall of Lean:
\begin{bigidea}
\textbf{The Curry--Howard correspondence.} A proposition can be read as a
type --- the type of its proofs. A proof is then simply a \emph{program} of
that type. Checking a proof is type-checking a program. There is no separate
``proof checker'' bolted onto Lean: the type checker you met in
Chapter~\ref{ch:lean} \emph{is} the proof checker.
\begin{center}
\begin{tabular}{@{}lll@{}}
\toprule
\textbf{Logic} & \textbf{Programming} & \textbf{In Lean} \\
\midrule
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 \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} \\
\bottomrule
\end{tabular}
\end{center}
\end{bigidea}
Take a minute with the last row: \lean{False} is a type with \emph{no
constructors} --- no way to build a value. To prove a false statement you
would have to produce an inhabitant of an empty type. That is why the system
is sound: lies have no evidence, so lies do not type-check.
\section{Proofs are programs: first proofs}
Let us write actual proofs as actual programs. Implication is a function
type, so proving ``$P$ implies $P$'' means writing the identity function:
\begin{lstlisting}[language=Lean]
theorem p_implies_p (P : Prop) : P -> P :=
fun h => h
\end{lstlisting}
Read \lean{fun h => h} aloud as a proof: ``assume $P$ holds --- call the
evidence $h$; then $P$ holds, by $h$.'' Every classical proof-writing phrase
has a program shape:
\begin{center}
\begin{tabular}{@{}ll@{}}
\toprule
\textbf{You say in prose} & \textbf{You write in Lean} \\
\midrule
``Assume $P$; call it $h$'' & \lean{fun h => ...} \\
``By hypothesis $h$'' & \lean{h} \\
``Apply lemma $f$ to fact $h$'' & \lean{f h} \\
``Both parts hold: ... and ...'' & \lean{And.intro pf1 pf2} \\
``From $h : P \land Q$, the first part'' & \lean{h.1} \\
\bottomrule
\end{tabular}
\end{center}
The pair-swapping example, now as an official theorem:
\begin{lstlisting}[language=Lean]
theorem and_swap (P Q : Prop) : P /\ Q -> Q /\ P :=
fun h => And.intro h.2 h.1
\end{lstlisting}
And transitivity of implication is exactly function composition:
\begin{lstlisting}[language=Lean]
theorem imp_trans (P Q R : Prop) : (P -> Q) -> (Q -> R) -> (P -> R) :=
fun pq qr => fun p => qr (pq p)
\end{lstlisting}
\begin{aha}
If you have ever composed two functions, you have already done everything
this proof does. The intimidating part of formal logic --- ``natural
deduction,'' ``inference rules'' --- turns out to be the part you knew from
programming all along. What logicians call \emph{modus ponens}, you call
\emph{calling a function}.
\end{aha}
\section{Equality and the proof that \texorpdfstring{$1+1=2$}{1+1=2}}
The proposition $a = b$ is also a type. Its only constructor is reflexivity
--- \lean{rfl} --- which proves \lean{a = a}. How can that ever prove
anything interesting? Because Lean \emph{computes} before comparing:
\begin{lstlisting}[language=Lean]
theorem one_plus_one : 1 + 1 = 2 := rfl
\end{lstlisting}
Lean unfolds \lean{1 + 1} using the two-line definition of addition from
Chapter~\ref{ch:lean}, arrives at \lean{2}, and sees that both sides are
\emph{literally the same value}. The equation holds by computation. This
mechanism --- \emph{definitional equality} --- is the engine that lets proofs
lean on programs, and later lets us prove facts about extracted Rust code by,
in part, just running it symbolically.
\begin{pitfall}
\lean{rfl} proves $2^{255} - 19$-sized computations happily, but it can only
prove what computation alone can see. \lean{n + 0 = n} is \lean{rfl} (the
definition's first equation matches), yet \lean{0 + n = n} is \emph{not} ---
recursion is on the \emph{second} argument, and \lean{n} is an opaque
variable, so nothing unfolds. The statement is still true; it just needs a
real proof (induction --- next chapter). The asymmetry feels unfair for about
a day. Then it becomes your sharpest mental model of what a computer can and
cannot know for free.
\end{pitfall}
\section{Universals, existentials, and dependent types}
Cryptographic specifications are universal statements: ``\emph{for all}
inputs, the output is correct.'' In Lean, $\forall$ is a function type whose
\emph{result type mentions the argument}:
\begin{lstlisting}[language=Lean]
theorem add_self_even : forall n : Nat, isEven (n + n) = true := ...
\end{lstlisting}
A proof of \lean{forall n, P n} is a function that eats any \lean{n} and
returns a proof of \lean{P n} --- one uniform recipe covering all the
infinitely many cases at once. This is precisely the thing testing could not
give us in Chapter~\ref{ch:why}: testing produces finitely many
\lean{P 3, P 17, P 42}; a proof produces the function.
Dually, \lean{exists n, P n} is proved by handing over a concrete witness
together with evidence: \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:
\begin{lstlisting}[language=Lean]
structure Rational where
num : Int
den : Nat
den_ne_zero : den ≠ 0 -- a PROOF, stored inside the value
\end{lstlisting}
No value of this type with a zero denominator can ever be constructed,
anywhere, by anyone. In the real Ed25519 development this exact pattern
appears as a \emph{bounds invariant}: a field element travels together with
the proof that its five limbs are small enough not to overflow the next
multiplication. The data structure makes the unsafe states unrepresentable.
\section{What about proof by contradiction?}
One more resident of the logical zoo. Lean's core logic is
\emph{constructive}: a proof of existence builds a witness. Classical
reasoning --- ``it's either true or false, and not false, hence true'' --- is
available the moment you want it (Mathlib imports it as \lean{Classical.choice},
and we will meet it again on the trust ledger in Chapter~\ref{ch:honesty}),
but it is an \emph{ingredient you can see}, not smuggled seasoning. When a
verification result says ``this proof uses only \lean{propext},
\lean{Classical.choice}, \lean{Quot.sound},'' that is a complete list of the
logical beliefs you are being asked to hold. Three. You can audit them over
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 -> (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
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
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
that, prove \lean{P -> Not (Not P)}. Write down in one sentence what program
you just wrote.}
\exercise{(Thought) Explain to a skeptical friend why a type with no
constructors is the right representation of falsehood --- and what would go
wrong with the whole edifice if someone added a constructor to it.}
\begin{checkpoint}
You should now be able to: translate each logical connective into its type
($\to$, $\land$, $\lor$, $\lnot$, $\forall$, $\exists$); write small proofs
as terms; explain why \lean{rfl} proves \lean{1 + 1 = 2} but not
\lean{0 + n = n}; and articulate the Curry--Howard slogan --- \emph{proofs
are programs, propositions are types, checking is type-checking} --- with a
straight face and genuine conviction.
\end{checkpoint}

194
chapters/ch04-tactics.tex Normal file
View file

@ -0,0 +1,194 @@
\chapter{Tactics: Proving as a Dialogue}
\label{ch:tactics}
\section{From programs to conversations}
Writing proofs as raw programs, as in Chapter~\ref{ch:pat}, is honest work,
but it scales badly: a real correctness proof for field multiplication would
be a program the size of a small compiler. Nobody writes those by hand.
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.
You enter the dialogue with the keyword \lean{by}:
\begin{lstlisting}[language=Lean]
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := by
intro h
constructor
· exact h.2
· exact h.1
\end{lstlisting}
Place your cursor after \lean{by} in the editor and Lean shows the
\textbf{goal state} --- the exact logical situation at that point:
\begin{lstlisting}
P Q : Prop
⊢ P ∧ Q → Q ∧ P
\end{lstlisting}
Everything above the turnstile \(\vdash\) is what you \emph{have} (the
context); the line after it is what you \emph{owe} (the goal). Every tactic
transforms this picture. After \lean{intro h}, the hypothesis moves above the
line; after \lean{constructor}, the goal splits in two. Proving becomes a
game whose board you can always see.
\begin{bigidea}
A tactic proof is a \textbf{recorded conversation with the goal state}. The
skill of proving is not memorizing tactic names --- it is learning to
\emph{read the goal state} and recognize which of a handful of moves makes it
simpler. Below is the core vocabulary; it covers the vast majority of every
proof in the real Ed25519 development.
\end{bigidea}
\begin{center}
\begin{tabular}{@{}lll@{}}
\toprule
\textbf{Tactic} & \textbf{When the goal looks like...} & \textbf{Effect} \\
\midrule
\lean{intro h} & \lean{P → Q}, \ \lean{∀ x, P x} & assume it; name the evidence \\
\lean{exact e} & anything & finish: \lean{e} is a proof of the goal \\
\lean{apply f} & \lean{Q}, given \lean{f : P → Q} & reduce the goal to \lean{P} \\
\lean{constructor} & \lean{P ∧ Q}, \lean{P ↔ Q}, ... & split into pieces \\
\lean{cases h} & have \lean{h : P ∨ Q} (or \(\wedge\), \lean{∃}) & case analysis on \lean{h} \\
\lean{rw [eq]} & contains a rewritable subterm & replace using equation \lean{eq} \\
\lean{simp} & simplifiable clutter & rewrite with a lemma database \\
\lean{induction n} & \lean{∀ n : Nat, ...} & base case + inductive step \\
\lean{rfl} & \lean{a = a} after computation & close by computation \\
\bottomrule
\end{tabular}
\end{center}
\section{Rewriting: equality as a tool}
The workhorse tactic of equational reasoning is \lean{rw} (rewrite). Given a
proven equation, it replaces one side by the other inside your goal:
\begin{lstlisting}[language=Lean]
example (a b : Nat) (h : a = b) : a + a = b + b := by
rw [h] -- goal becomes: b + b = b + b, closed by rfl automatically
\end{lstlisting}
Chains of rewrites read like the two-column proofs of school geometry,
except a machine checks every line. Here is commutativity-and-associativity
shuffling, Mathlib lemmas by name:
\begin{lstlisting}[language=Lean]
example (a b c : Nat) : a + b + c = c + b + a := by
rw [Nat.add_comm a b] -- b + a + c = c + b + a
rw [Nat.add_assoc] -- b + (a + c) = c + b + a
rw [Nat.add_comm a c] -- b + (c + a) = c + b + a
rw [← Nat.add_assoc] -- b + c + a = c + b + a
rw [Nat.add_comm b c] -- done
\end{lstlisting}
The arrow \(\leftarrow\) rewrites right-to-left. Nobody enjoys writing five-line
shuffles like this, which is exactly why Chapter~\ref{ch:automation}
introduces \lean{ring} --- but you must \emph{once} feel the manual version to
understand what the automation is doing on your behalf.
\section{Induction: the tactic that conquers infinity}
Remember the embarrassment of Chapter~\ref{ch:pat}: \lean{0 + n = n} does not
hold by computation. Now we can prove it --- by induction, the proof
technique that inductive types were born for:
\begin{lstlisting}[language=Lean]
theorem zero_add (n : Nat) : 0 + n = n := by
induction n with
| zero => rfl -- 0 + 0 = 0: computes
| succ k ih => rw [Nat.add_succ, ih]
\end{lstlisting}
The \lean{induction} tactic converts a statement about \emph{all} naturals
into two finite obligations: the statement for \lean{zero}, and the statement
for \lean{succ k} \emph{assuming it for} \lean{k} (the induction hypothesis
\lean{ih}). Because every natural number is built from those two
constructors, the two cases cover infinity.
\begin{aha}
Induction is not a new axiom to swallow --- it falls out of the inductive
definition of \lean{Nat} itself. ``Every \lean{Nat} is \lean{zero} or a
\lean{succ}'' \emph{is} the license to do case analysis; recursion on the
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}
\begin{pitfall}
When a proof gets stuck, resist the urge to try random tactics --- the
formal-methods equivalent of mashing buttons. The goal state is telling you
something. Three honest questions unstick most situations: (1)~Is the
statement actually true as written --- check a small example with
\lean{\#eval}! (2)~Am I missing a hypothesis --- is there an unstated bound or
nonzero condition? (3)~Is my induction on the right variable? In the real
projects behind this book, ``the proof is stuck'' was, more often than not,
the \emph{statement} being subtly wrong --- a truncated subtraction, a missing
bound. The proof assistant was the messenger.
\end{pitfall}
\section{Structuring real proofs: \texttt{have} and \texttt{calc}}
Big proofs are not flat lists of tactics; they are structured arguments with
named intermediate results. The \lean{have} tactic states and proves a
stepping stone; \lean{calc} lays out a chain of equalities or inequalities
the way you would on a whiteboard:
\begin{lstlisting}[language=Lean]
example (a b : Nat) (h : a = 2 * b) : a + a = 4 * b := by
have h2 : a + a = 2 * a := by rw [Nat.two_mul]
calc a + a = 2 * a := h2
_ = 2 * (2 * b) := by rw [h]
_ = 4 * b := by rw [← Nat.mul_assoc]
\end{lstlisting}
This style is not cosmetic. In the verified field arithmetic you will read
later, a single multiplication correctness proof is a \lean{calc} chain
tracking limb products through carries --- dozens of steps, each trivial,
whose \emph{composition} is the theorem. \lean{have} and \lean{calc} are how
proofs stay readable at that scale; they are also how they stay
\emph{maintainable}, because a broken step localizes the damage to one line.
There is one more structuring fact worth knowing early, because it saved the
real project from a crash-course (literally --- see
Chapter~\ref{ch:honesty}): breaking a proof into small named \lean{have}
steps also controls the proof assistant's \emph{memory appetite}. A monolithic
``figure it all out at once'' tactic call over a huge context can consume
gigabytes; ten targeted steps, pennies each, prove the same thing. Structure
is not just style --- it is engineering.
\begin{tryit}
Open \code{exercises/Ch04.lean}. It sets up each theorem with the goal state
drawn in a comment, then asks you to: prove \lean{and_swap} in tactic mode;
prove \lean{zero_add} \emph{without} peeking above; and repair a broken
\lean{calc} chain in which exactly one step is wrong. The third
exercise is secretly the most realistic job training in this book.
\end{tryit}
\section*{Exercises}
\exercise{Prove by induction: \lean{∀ n : Nat, n + 0 = n} and
\lean{∀ n m : Nat, n + succ m = succ (n + m)}. (These are the mirror images
of the definitional equations --- the ones computation gives you for free ---
and together they yield commutativity.)}
\exercise{Using the previous exercise, prove
\lean{∀ n m : Nat, n + m = m + n} by induction on \lean{m}. Write out, in
one prose sentence per case, what each branch of your proof says.}
\exercise{Prove \lean{∀ n : Nat, 2 * n = n + n} twice: once with
\lean{induction}, once with a single \lean{rw} using a Mathlib lemma you find
yourself (search hint: \lean{exact?} asks Lean to search for you).}
\exercise{(Reading) In the goal state
\lean{h : a < 2\textasciicircum{}51 ⊢ a * 19 < 2\textasciicircum{}56}, no induction is needed --- this is pure
arithmetic. Which tactic from the table would you \emph{guess} handles it?
(Answer next chapter; your guess is the point.)}
\begin{checkpoint}
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.
\end{checkpoint}

186
chapters/ch05-numbers-and-automation.tex Normal file
View file

@ -0,0 +1,186 @@
\chapter{Numbers and Automation: Making the Machine Do the Boring Parts}
\label{ch:automation}
\section{The 90/10 rule of verification}
Here is a trade secret: most of a real verification effort is not clever.
Opening the correctness proof of Ed25519 field multiplication, you will find
that the overwhelming majority of proof obligations are statements like
\[
a < 2^{51} \;\wedge\; b < 2^{51} \;\Longrightarrow\; a + b < 2^{52},
\qquad\qquad
(a + b) \cdot c = a\cdot c + b\cdot c,
\]
--- bookkeeping a patient undergraduate could verify by hand in a minute
each. There are \emph{thousands} of them. The craft of modern verification is
to hand exactly this 90\% to decision procedures --- tactics that implement a
complete algorithm for a well-defined logical fragment --- and save the human
for the 10\% that needs insight. This chapter is your tour of the arsenal.
\section{\texttt{omega}: linear arithmetic, decided}
The tactic you will use more than any other in this book's domain is
\lean{omega}. It completely decides \emph{linear arithmetic} over integers
and naturals: any goal built from variables, constants, $+$, $-$,
multiplication \emph{by constants}, $=$, $<$, $\le$, $\lnot$, $\wedge$,
$\vee$, including the hypotheses in context.
\begin{lstlisting}[language=Lean]
example (a b : Nat) (h1 : a < 2^51) (h2 : b < 2^51) :
a + b < 2^52 := by omega
example (a b : Nat) (h : a ≤ b) : a + (b - a) = b := by omega
-- note: truncated Nat subtraction handled CORRECTLY -- omega knows
\end{lstlisting}
That second example deserves a salute: \lean{omega} understands \lean{Nat}
truncation natively, defusing the Chapter~\ref{ch:lean} pitfall by algorithm
rather than by vigilance. When the goal is false, \lean{omega} \emph{fails} ---
it is a decision procedure, so failure on a linear goal means the goal (with
the hypotheses in view) is simply not true. That property turns \lean{omega}
into a \emph{statement-debugging} tool: if it refuses your ``obviously true''
bound, go find the counterexample; there is one.
\begin{pitfall}
\lean{omega} does not touch multiplication of two \emph{variables}
($a \cdot b$ is not linear), division in general, or bit-shifts by variables.
For a goal mixing $a \cdot b$ with bounds, you often first name the product
--- \lean{have hab : a * b ≤ 2\textasciicircum{}102 := ...} using a multiplication
monotonicity lemma --- and then let \lean{omega} finish with \lean{hab} as an
opaque atom. This two-step, \emph{bound the nonlinear part, then release the
linear solver}, is the single most-used proof pattern in verified field
arithmetic. You will write it dozens of times, and by Chapter~\ref{ch:field}
it will feel like breathing.
\end{pitfall}
\section{\texttt{decide}: when truth is a computation}
Some propositions can be checked by running an algorithm to completion:
``$97$ is prime,'' ``these two sorted lists are equal,'' ``$x^3 = x$ for all
$x$ in $\Zmod{6}$'' (six cases --- check them all). For any such
\emph{decidable} proposition, the \lean{decide} tactic runs the decision
algorithm inside Lean's kernel and turns the answer into a proof:
\begin{lstlisting}[language=Lean]
example : Nat.Prime 97 := by decide
example : ∀ x : ZMod 6, x^3 = x^3 := by decide -- finite: try all six
\end{lstlisting}
The magic and the limitation are the same fact: the \emph{kernel itself}
re-executes the computation. That makes \lean{decide} unimpeachable --- and
completely hopeless for our 77-digit prime $2^{255}-19$, where trial division
would outlast the universe. There is a variant, \lean{native_decide}, that
compiles the check to native code first --- fast enough! --- but it makes the
compiler part of your trusted base, an IOU we will scrutinize hard in
Chapters~\ref{ch:prime} and~\ref{ch:honesty}. For now, the rule of the house:
\textbf{\lean{decide} yes, \lean{native_decide} never in a final certificate.}
\section{\texttt{ring} and \texttt{norm\_num}: algebra on tap}
The five-line commutativity shuffle from Chapter~\ref{ch:tactics}? Here is
the grown-up version:
\begin{lstlisting}[language=Lean]
example (a b c : Nat) : a + b + c = c + b + a := by ring
example (a b : ZMod p) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring
example : (2:Int)^255 - 19 > 2^254 := by norm_num
\end{lstlisting}
\lean{ring} proves any identity that holds in every commutative ring ---
polynomial rearrangements, binomial expansions, distributivity avalanches ---
by normalizing both sides to a canonical polynomial form and comparing.
\lean{norm_num} evaluates concrete numeric facts, comfortable with numbers of
any size. Between \lean{omega}, \lean{ring}, and \lean{norm_num} you now hold
the three keys that open most arithmetic doors:
\begin{center}
\begin{tikzpicture}[
key/.style={draw=ink2,thick,rounded corners=3pt,fill=white,align=center,
minimum width=3.55cm,minimum height=1.5cm},
]
\node[key,fill=accentsoft] (o) at (0,0)
{\textbf{\code{omega}}\\[1pt]\small linear $+,-,<,\le$\\\small bounds \& carries};
\node[key,fill=provensoft] (r) at (4.1,0)
{\textbf{\code{ring}}\\[1pt]\small polynomial identities\\\small in any comm.\ ring};
\node[key,fill=warnsoft] (n) at (8.2,0)
{\textbf{\code{norm\_num}}\\[1pt]\small concrete numerals\\\small any size};
\node[font=\small\color{ink2},align=center] at (4.1,-1.55)
{the three keys of verified arithmetic --- learn what each fragment
\emph{excludes}\\ and you will always know which door you are standing in front of};
\end{tikzpicture}
\end{center}
\section{\texttt{simp}: the rewriting engine, and how to hold it}
\lean{simp} rewrites the goal to exhaustion using a curated database of
thousands of ``simplification'' lemmas ($x + 0 \rightsquigarrow x$,
\lean{List.length (a :: l)} $\rightsquigarrow$ \lean{l.length + 1}, ...). It
is the most powerful tactic in Lean and the easiest to misuse. Used well, it
clears brush so the real argument stands out. Used lazily ---
\lean{simp [*]} with every hypothesis thrown in, in a context of sixty
accumulated facts --- it becomes a search over an enormous rewrite space:
slow, fragile under library updates, and occasionally a memory monster.
This is not hypothetical. During the development this book accompanies, a
single over-broad \lean{simp}-style discharge in a fat context consumed
twelve gigabytes of RAM and took down the machine. The postmortem produced
house rules worth adopting from day one:
\begin{itemize}[leftmargin=1.4em]
\item Prefer \lean{simp only [lemma1, lemma2]} --- an explicit lemma list ---
in anything you intend to keep.
\item Let \lean{simp?} tell you the list: run it once interactively, then
paste the \lean{simp only [...]} it suggests into the file.
\item Keep contexts lean (pun intended): a proof with sixty hypotheses in
scope wants to be five \lean{have}-steps with twelve each.
\end{itemize}
\begin{bigidea}
Automation is a \emph{contract}, not a slot machine. Each tactic decides a
known fragment: \lean{omega} linear arithmetic, \lean{ring} ring identities,
\lean{decide} finite computation, \lean{simp only} a rewrite system you
chose. The professional habit is to know \emph{which} contract you are
invoking --- then failure is information (``this goal is not linear''; ``this
identity needs the modulus''), never mystery.
\end{bigidea}
\begin{tryit}
Open \code{exercises/Ch05.lean}: ten arithmetic goals, each solvable by
exactly one of \lean{omega} / \lean{ring} / \lean{norm_num} / \lean{decide}.
Your task is not just to close them but to close each with the \emph{right}
tool --- the file rejects overkill by design. Goal number ten is the
Chapter~\ref{ch:tactics} cliffhanger:
\lean{a < 2\textasciicircum{}51 → a * 19 < 2\textasciicircum{}56}. (It is not linear --- $19$ is a constant, so
it is! Think, then fire.)
\end{tryit}
\section*{Exercises}
\exercise{For each, name the tactic and predict success before running:
(a) \lean{(a+b)*(a-b) = a*a - b*b} over \lean{Int};
(b) \lean{a < 100 → b < 100 → a*b < 10000} over \lean{Nat};
(c) \lean{Nat.Prime 65537};
(d) \lean{2\textasciicircum{}51 + 2\textasciicircum{}51 = 2\textasciicircum{}52}.}
\exercise{Goal (b) above is nonlinear, yet \lean{omega} alone fails while the
two-step pattern (bound the product with
\lean{Nat.mul_lt_mul} machinery, then \lean{omega}) succeeds. Carry it out.
Time yourself; the pattern should take under five minutes by the second
attempt.}
\exercise{Find a true statement about \lean{Nat} that \emph{no} tactic in
this chapter proves in one shot, and sketch in prose how you would decompose
it. (Anything genuinely inductive works --- automation here decides
arithmetic fragments, not all of mathematics.)}
\begin{checkpoint}
You should now be able to: match a goal to its decision procedure by the
shape of its operators; execute the bound-then-omega pattern for nonlinear
bounds; explain why \lean{decide} is trustworthy and where it hits its
computational wall; and state the \lean{simp} discipline --- and the story of
why this book is unusually sincere about it.
\end{checkpoint}

183
chapters/ch06-modular-arithmetic.tex Normal file
View file

@ -0,0 +1,183 @@
\chapter{Modular Arithmetic: The Number System Cryptography Lives In}
\label{ch:modular}
\section{Clock arithmetic, taken seriously}
You already compute modulo twelve every day: 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
\]
hours on it --- a 77-digit prime. Everything else --- the wrap-around, the
remainder-taking, the algebra --- is the twelve-hour clock you already know.
Formally, we write $a \equiv b \pmod{n}$ when $n$ divides $a - b$, and we
collect all integers with the same remainder into one object: the world
$\Zmod{n}$ has exactly $n$ elements, $\{0, 1, \dots, n-1\}$, with addition
and multiplication that wrap. In Lean/Mathlib this world is a first-class
type, and computation in it is exactly what you would hope:
\begin{lstlisting}[language=Lean]
#eval (7 + 8 : ZMod 12) -- 3 (fifteen o'clock is three o'clock)
#eval (5 * 9 : ZMod 12) -- 9
#eval (3 - 7 : ZMod 12) -- 8 (subtraction wraps -- no truncation!)
def p : Nat := 2^255 - 19
#eval (2^255 : ZMod p) -- 19 (of course: 2^255 = p + 19)
\end{lstlisting}
Note the third line with relief: unlike \lean{Nat}, subtraction in
\lean{ZMod n} is a total, well-behaved inverse of addition. Every element has
a negative. In algebra terms, $\Zmod{n}$ is a \emph{commutative ring} --- and
Lean knows it, so the \lean{ring} tactic from Chapter~\ref{ch:automation}
works there natively.
\section{Division: where primes enter}
Rings give us $+$, $-$, $\times$. Cryptography also needs $\div$ --- and
division is where the modulus stops being a size parameter and starts being a
design decision. Dividing by $a$ means multiplying by some $a^{-1}$ with
$a \cdot a^{-1} = 1$. Does such an inverse exist? On the twelve-hour clock,
try to invert $4$: the multiples of $4$ are $4, 8, 0, 4, 8, 0, \dots$ ---
the value $1$ never appears. $4$ has no inverse mod $12$, because $4$ and
$12$ share the factor~$4$.
\begin{bigidea}
In $\Zmod{n}$, the element $a$ is invertible exactly when
$\gcd(a, n) = 1$. So if $n = p$ is \textbf{prime}, \emph{every} nonzero
element is invertible: you can divide freely, and $\Zmod{p}$ earns the title
of \textbf{field}, written $\Fp$. Fields are the arithmetic paradise where
linear algebra, polynomial factoring, and elliptic-curve geometry all work.
This --- and only this --- is why cryptographic moduli are prime: primality
is the entry ticket to division.
\end{bigidea}
\begin{center}
\begin{tikzpicture}[scale=0.62,every node/.style={font=\small}]
% Z/12 clock: multiples of 4 stuck in a cycle
\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}
\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}
% Z/11 clock: multiples of 4 reach 1
\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}
\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}
\end{tikzpicture}
\end{center}
How do you \emph{find} $a^{-1}$ mod $p$? Two classical answers, both of which
appear in real Ed25519 code: the extended Euclidean algorithm, and Fermat's
little theorem, which says $a^{p-1} \equiv 1 \pmod p$ for $a \not\equiv 0$
--- hence $a^{p-2}$ \emph{is} the inverse. The dalek library computes
inverses as $a^{p-2}$ with a hand-crafted chain of $254$ squarings and $11$
multiplications; one of the proofs you will meet in Chapter~\ref{ch:field}
verifies precisely that this chain computes what Fermat promises.
\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
computed by \emph{machines with 64-bit words}, and $p = 2^{255}-19$ is shaped
for them:
\begin{itemize}[leftmargin=1.4em]
\item \textbf{Reduction is a multiply-by-19.} Numbers at or beyond $2^{255}$
overflow the dial; but since $2^{255} \equiv 19 \pmod p$, any overflow bit
re-enters the sum carrying a factor of just $19$. Reducing mod $p$ costs
one small multiplication --- no long division, ever.
\item \textbf{255 bits split evenly into five limbs of 51.} A 64-bit word
holding a 51-bit limb leaves 13 bits of headroom for carries to accumulate
lazily --- the delayed-carry style from Chapter~\ref{ch:why}, now by design
rather than accident. The bound $a_i < 2^{51+\varepsilon}$ will follow us
through Chapters~\ref{ch:denotation} and~\ref{ch:field}.
\item \textbf{It sits just below a power of two}, so 255-bit values fit in 32
bytes with one bit to spare --- and Ed25519 spends that spare bit storing a
point's sign. Engineering all the way down.
\end{itemize}
The Pasta curves verified in the companion projects (Pallas/Vesta, used in
zero-knowledge proof systems) choose their $\approx 2^{254}$ primes by a
different criterion --- friendliness to fast Fourier transforms --- and
represent elements in \emph{Montgomery form}, a representation trick we will
touch in Chapter~\ref{ch:denotation}. Different shapes, same theory: pick a
prime whose field your machine can love.
\section{Modular arithmetic in Lean, hands on}
Statements about $\Fp$ are ordinary Lean theorems, and the automation you
already own applies:
\begin{lstlisting}[language=Lean]
-- ring identities hold verbatim in ZMod n:
example (x y : ZMod 12) : (x + y)^2 = x^2 + 2*x*y + y^2 := by ring
-- small finite worlds: check every case
example : ∀ x : ZMod 12, 4 * x ≠ 1 := by decide
-- inverses exist in prime fields (Mathlib knows ZMod 11 is a field):
example (a : ZMod 11) (h : a ≠ 0) : a * a⁻¹ = 1 :=
ZMod.mul_inv_cancel_of_ne_zero h
\end{lstlisting}
What about the crown fact, $2^{255} \equiv 19$? For \emph{concrete numeric}
statements at 77-digit scale, tactic choice suddenly matters: \lean{decide}
would ask the kernel to grind case analysis it cannot afford, while
\lean{norm_num} and reflexivity-by-computation on efficient numerals handle
it comfortably. Verifying real cryptography is partly a \emph{performance
engineering} discipline --- Chapter~\ref{ch:prime} turns this observation
into a principle when the question becomes primality itself.
\begin{pitfall}
In \lean{ZMod n}, the numeral \lean{57896044618658...} and the numeral
\lean{19} can be \emph{the same element}. Equality of elements is not
equality of the numerals you typed. When a surprising \lean{rfl} succeeds ---
or two ``different'' constants turn out equal --- remember you are on the
clock face, not the number line. This is a feature: the entire verification
story of Chapter~\ref{ch:denotation} consists of choosing, deliberately, when
to view a pile of bytes as an integer and when as a clock position.
\end{pitfall}
\begin{tryit}
Open \code{exercises/Ch06.lean}. You will: compute your first inverses with
\lean{\#eval}; expand $(x+y)^3$ in \lean{ZMod 7} with one tactic; show $4$
has no inverse in \lean{ZMod 12} by \lean{decide}; and prove the reduction
identity $2^{255} = 19$ in \lean{ZMod p}.
\end{tryit}
\section*{Exercises}
\exercise{Compute by hand (yes, hand): $3^{-1}$ in $\Zmod{7}$, and check that
stepping by $3$ on a 7-hour clock visits every position. Then confirm both
with \lean{\#eval}.}
\exercise{Prove in Lean: \lean{∀ x : ZMod 12, 4 * x ≠ 1}, then change $12$
to $13$ and watch the same tactic refuse --- find the witness it is
implicitly pointing at.}
\exercise{Fermat's little theorem is \lean{ZMod.pow_card_sub_one_eq_one} in
Mathlib. Use it to prove that in \lean{ZMod 11}, \lean{a\textasciicircum{}9 * a = 1} whenever
\lean{a ≠ 0}.}
\exercise{(Paper) The Ed25519 code reduces a 256-bit value $x$ by writing
$x = x_{\mathrm{low}} + 2^{255}\, x_{\mathrm{high}}$ and returning
$x_{\mathrm{low}} + 19\, x_{\mathrm{high}}$. Prove informally that this
preserves the value mod $p$, and bound how much smaller the result is. You
have just re-derived the reduction step you will verify formally in
Chapter~\ref{ch:field}.}
\begin{checkpoint}
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.
\end{checkpoint}

174
chapters/ch07-primality-certificates.tex Normal file
View file

@ -0,0 +1,174 @@
\chapter{Convincing a Paranoid Kernel That a 77-Digit Number Is Prime}
\label{ch:prime}
\section{The problem nobody warns you about}
Chapter~\ref{ch:modular} ended with a quiet dependency: everything ---
division, field structure, the whole elliptic curve --- rests on
$p = 2^{255}-19$ \emph{being prime}. In Lean, that is a proposition like any
other, and it must be \emph{proved}:
\begin{lstlisting}[language=Lean]
theorem p_prime : Nat.Prime (2^255 - 19) := ?
\end{lstlisting}
Your Chapter~\ref{ch:automation} instincts say \lean{decide}: primality is
decidable --- just try dividing. But trial division tests divisors up to
$\sqrt{p} \approx 2^{127}$. At a billion billion divisions per second, that
is about $10^{12}$ ages of the universe. The kernel, which happily
\emph{re-executes} every computation you feed it, cannot afford this one. And
mathematicians clearly believe this number is prime --- so how does
\emph{anyone} know?
\section{Certificates: the deep idea hiding here}
The answer reorganizes how you think about computation. \emph{Finding} a
fact and \emph{checking} a fact can have wildly different costs. What we need
is a \textbf{certificate}: a piece of data, possibly expensive to discover,
that makes the fact \emph{cheap to verify}.
You have met certificates before without the name. A composite number's
certificate is a factor: finding a factor of a 77-digit number may be hard,
but checking $n = a \cdot b$ is one multiplication. The beautiful surprise
--- Pratt's theorem, 1975 --- is that \emph{primality} has certificates too:
\begin{bigidea}
\textbf{Pratt certificate.} To certify that $p$ is prime, exhibit a
\emph{witness} $w$ such that
\[
w^{p-1} \equiv 1 \pmod p
\qquad\text{and}\qquad
w^{(p-1)/q} \not\equiv 1 \pmod p
\ \text{ for every prime factor } q \text{ of } p-1 .
\]
Such a $w$ generates all $p-1$ nonzero residues, which forces $\Zmod{p}$ to
have $p-1$ invertible elements --- something only a prime modulus allows.
Checking the certificate costs a handful of modular exponentiations
(milliseconds, by fast squaring), \emph{plus recursively certifying the
prime factors $q$} --- each much smaller, so the recursion collapses fast.
\end{bigidea}
Concretely for our hero: $p - 1 = 2^{255} - 20 = 2^2 \cdot 5 \cdot q_1 \cdot
q_2$ where $q_1$ (44 digits) and $q_2$ (33 digits) are themselves prime, with
their own small certificates. 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:
\begin{center}
\begin{tikzpicture}[
lvl/.style={draw=ink2,thick,rounded corners=2pt,fill=white,align=center,font=\small},
edge/.style={-{Stealth},ink2,thick}
]
\node[lvl,fill=accentsoft] (p) at (0,2.6)
{$p = 2^{255}-19$ \quad witness $w=2$\\ $p-1 = 2^2\cdot 5\cdot q_1\cdot q_2$};
\node[lvl] (two) at (-4.4,0.6) {$2$: prime\\ \footnotesize (immediate)};
\node[lvl] (five) at (-1.9,0.6) {$5$: prime\\ \footnotesize (immediate)};
\node[lvl,fill=provensoft] (q1) at (0.9,0.6) {$q_1$ (44 digits)\\ own witness + factors};
\node[lvl,fill=provensoft] (q2) at (4.3,0.6) {$q_2$ (33 digits)\\ own witness + factors};
\draw[edge] (p) -- (two); \draw[edge] (p) -- (five);
\draw[edge] (p) -- (q1); \draw[edge] (p) -- (q2);
\node[font=\small\color{ink2},align=center] at (0,-0.6)
{each node: milliseconds to check; the whole tree: a proof};
\end{tikzpicture}
\end{center}
\begin{aha}
This find/check asymmetry is one of the great ideas of computer science ---
it is the P versus NP distinction wearing work clothes, and it is the engine
of zero-knowledge proof systems (the very technology the Pasta curves serve).
Proof assistants run on it too: Lean's whole architecture --- clever tactics
\emph{finding}, dumb kernel \emph{checking} --- is the same asymmetry. A
proof \emph{is} a certificate.
\end{aha}
\section{The tempting shortcut, and why the house declines it}
Lean offers a faster \lean{decide}: the variant \lean{native_decide}
compiles the decision procedure to native machine code, runs it at full
speed, and asserts the result. With a good primality test behind it, it can
dispatch \lean{Nat.Prime p} in seconds. Case closed?
Look at what you would be trusting. Ordinary \lean{decide} produces a
computation the \emph{kernel} replays --- the ~few-thousand-line paranoid
core remains the only thing you trust. \lean{native_decide} instead makes
the theorem's truth depend on the Lean \emph{compiler}, the C toolchain
behind it, and the runtime --- hundreds of thousands of lines promoted into
your trusted base, in exchange for convenience on one theorem. Every proof
downstream of the field --- group law, scalars, signatures --- would inherit
that enlarged trust, visible forever in its axiom report
(Chapter~\ref{ch:honesty} shows you how to read those).
\begin{pitfall}
\lean{native_decide} is not ``cheating,'' and for exploratory work it is a
fine tool. The trap is \emph{silent trust inflation}: its use is invisible at
the theorem statement --- the cost appears only when someone audits the
axioms, which is exactly what most readers never do. House rule, adopted from
the projects this book accompanies: exploratory scaffolding may use it;
\textbf{no shipped certificate depends on it}. The final Pallas-modulus
primality proof in \code{pasta-pallas-verified} is a kernel-checked
Lucas/Pratt certificate for precisely this reason.
\end{pitfall}
\section{Certificates in practice: Mathlib's toolbox}
You will not hand-roll witness trees. Mathlib provides the machinery
(\lean{Nat.Prime} decision lemmas, \lean{lucas_lehmer}-style infrastructure,
and the \lean{norm_num} extension \lean{Nat.Prime} plugin) that constructs
and checks Pratt-style certificates behind a single tactic call --- while
keeping every step kernel-checked. The shape in real code:
\begin{lstlisting}[language=Lean]
theorem p_prime : Nat.Prime (2^255 - 19) := by
norm_num -- certificate-backed primality, kernel-checked, ~seconds
\end{lstlisting}
When the built-in route struggles (very large or awkward moduli), the
fallback is explicit: state the witness data as definitions, prove the two
Pratt conditions with \lean{norm_num}-driven modular exponentiation, and
assemble. That is exactly the structure of the Pallas certificate in the
companion repository --- worth reading now with fresh eyes:
\code{pasta-pallas-verified/verification/Proofs/Primality.lean}.
\begin{tryit}
Open \code{exercises/Ch07.lean}. Ladder: certify $97$, then $65537$ (a
Fermat prime beloved of RSA), then the ten-digit Mersenne prime $2^{31}-1$,
watching what each tool costs as the numbers grow. (Amusingly, the
find/check asymmetry bites the \emph{tactic} too: \lean{norm_num} must
\emph{find} the witness tree before the kernel checks it, and at $2^{61}-1$
the finding already takes minutes.) Finale: implement square-and-multiply
modular exponentiation yourself and check the top witness condition for
$p = 2^{255}-19$ with \lean{\#eval} --- your own hands on the certificate,
at 77 digits, in milliseconds.
\end{tryit}
\section*{Exercises}
\exercise{Verify by hand that $w = 2$ is a Pratt witness for $p = 13$:
compute $2^{12} \bmod 13$ and $2^{12/q} \bmod 13$ for each prime $q \mid 12$.
Write the full certificate tree for $13$, recursing into the factors of
$12$.}
\exercise{Why does the witness condition force primality? Sketch the
argument: if $w$ has order exactly $p-1$ in $\Zmod{p}$, then the
multiplicative structure has $p-1$ elements, which fails if $p = ab$ with
$1 < a,b < p$. (Full rigor optional; the shape is the point.)}
\exercise{Estimate, in modular multiplications, the cost of checking the
certificate for $2^{255}-19$: count squarings for one exponentiation at 255
bits, times the number of conditions in the tree above. Compare with the
$2^{127}$ divisions of trial division. Write both numbers down next to each
other. Smile.}
\exercise{(Discussion) Bitcoin miners \emph{find} block hashes; nodes
\emph{check} them. GPS receivers \emph{check} satellite signals they could
never \emph{find}. Name two more systems built on the find/check asymmetry,
and one system that would collapse without it.}
\begin{checkpoint}
You should now be able to: explain why \lean{decide} cannot prove
$2^{255}-19$ prime while a certificate can; reproduce the two Pratt witness
conditions and check them on a small prime; articulate exactly what
additional trust \lean{native_decide} would introduce and why shipped
certificates decline it; and recognize the find/check asymmetry as the
common engine of certificates, proof assistants, and the P-vs-NP question.
\end{checkpoint}

195
chapters/ch08-rust-to-lean.tex Normal file
View file

@ -0,0 +1,195 @@
\chapter{From Rust to Lean: Verifying the Code That Actually Ships}
\label{ch:rust}
\section{The transcription problem}
Everything so far proved facts about \emph{Lean} programs. But the Ed25519
that guards your SSH connection is written in \emph{Rust} (in our case,
\code{curve25519-dalek} and its forks). An obvious plan: read the Rust,
rewrite it in Lean by hand, verify the rewrite. The plan has a hole you could
drive a key-recovery attack through: \textbf{what if you transcribe it
wrong?} A hand-copy that silently fixes a bug --- or introduces one --- makes
the proof a beautiful statement about code nobody runs.
The projects behind this book close the hole with a mechanical translation
pipeline:
\begin{center}
\begin{tikzpicture}[
stage/.style={draw=ink2,thick,rounded corners=3pt,align=center,
minimum height=1.15cm,minimum width=2.5cm,font=\small},
arr/.style={-{Stealth},thick,ink2},
lbl/.style={font=\scriptsize\color{ink2},midway,above}
]
\node[stage,fill=codebg] (rust) at (0,0) {\textbf{Rust source}\\ \code{field.rs}};
\node[stage,fill=warnsoft] (llbc) at (4.0,0) {\textbf{LLBC}\\ intermediate form};
\node[stage,fill=provensoft] (model) at (8.0,0) {\textbf{Lean model}\\ \code{gen/Funs.lean}};
\node[stage,fill=accentsoft] (proof) at (12.0,0) {\textbf{Your proofs}\\ \code{Proofs/*.lean}};
\draw[arr] (rust) -- node[lbl]{Charon} (llbc);
\draw[arr] (llbc) -- node[lbl]{Aeneas} (model);
\draw[arr] (model) -- node[lbl]{you} (proof);
\node[font=\scriptsize\color{ink2},align=center] at (6.0,-1.15)
{machine-generated, never hand-edited \hspace{2.2cm} human-written, kernel-checked};
\end{tikzpicture}
\end{center}
\textbf{Charon} compiles the Rust crate into LLBC (``low-level borrow
calculus''), a simplified intermediate representation. \textbf{Aeneas}
translates LLBC into pure Lean functions. The generated Lean --- the
\emph{model} --- lands in a \code{gen/} directory with a strict house rule:
\emph{never edit it}. Regenerate it from source, or don't touch it. Your
proofs import the model and state theorems about it.
\begin{bigidea}
The object of verification is the \textbf{extracted model}, produced from
the shipping source by a deterministic tool --- not a human transcription.
The trust question shifts from ``did we copy the code right?'' (unauditable
squinting) to ``does the translator preserve meaning?'' (one tool, studied
once, shared by every project that uses it). You will hear this called
\emph{shrinking the trusted base}: swap many ad-hoc trusts for one
well-examined trust.
\end{bigidea}
\section{What extracted code looks like}
Here is real input and real output, lightly abridged. The Rust (from
\code{curve25519-dalek}, radix-51 field addition):
\begin{lstlisting}[language=RustL]
impl Add for FieldElement51 {
fn add(self, rhs: &FieldElement51) -> FieldElement51 {
let mut output = *self;
for i in 0..5 {
output.0[i] += rhs.0[i];
}
output
}
}
\end{lstlisting}
And the Lean model Aeneas produces for it (shape, not verbatim):
\begin{lstlisting}[language=Lean]
def fieldElement51_add (self rhs : Array U64 5) :
Result (Array U64 5) := do
let a0 <- Array.index_usize self 0
let b0 <- Array.index_usize rhs 0
let s0 <- a0 + b0 -- U64 addition: can FAIL on overflow
let out <- Array.update self 0 s0
... -- and so on for limbs 1..4
\end{lstlisting}
Three features deserve your full attention, because every proof in the next
two chapters engages them:
\begin{itemize}[leftmargin=1.4em]
\item \textbf{Machine integers are honest.} \lean{U64} is not $\N$; it is
64-bit words. Aeneas models arithmetic on them precisely, overflow
included.
\item \textbf{Everything returns \lean{Result}.} The \lean{do}/\lean{<-}
notation threads a computation that can \emph{fail} --- returning an error
value instead of a result --- exactly where the Rust could panic or
overflow. There is no pretending partial functions are total.
\item \textbf{It is ugly.} Five limbs times load-add-store, all sequenced.
Machine-generated code has no taste. The \emph{proofs} restore the
elegance; the model's job is fidelity.
\end{itemize}
\section{Overflow is a proof obligation, not a footnote}
In Rust, \rust{a + b} on \rust{u64} panics in debug mode and wraps in
release mode when it overflows. In the extracted model, \lean{a + b}
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}:
\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}
That hypothesis \lean{LimbsBounded} --- each limb below $2^{54}$, say --- is
the bounds invariant promised in Chapters~\ref{ch:pat}
and~\ref{ch:modular}: 51-bit payload plus headroom, so limb additions cannot
reach $2^{64}$. The specification exposes what the Rust comments only
whisper: this code is correct \emph{under a discipline of bounded inputs},
the discipline must be maintained by every caller, and now there is a
machine checking that it is.
\begin{aha}
Notice what just happened to ``ugly generated code with Results
everywhere'': it forced us to discover, state, and prove the \emph{implicit
operating envelope} of the optimized implementation. The dalek authors knew
this envelope; it lived in comments and code-review lore. Now it is a
theorem. Extraction does not merely enable verification --- it
\emph{interrogates} the code.
\end{aha}
\section{Practicalities: extraction as surgery}
Running Charon on a whole real-world crate drags in everything the crate
touches --- iterators, byte serialization, trait machinery, SIMD backends
--- much of it irrelevant to the arithmetic core and some of it beyond what
the translator supports. The working method, learned the honest way in the
companion projects:
\begin{itemize}[leftmargin=1.4em]
\item \textbf{Extract functions, not crates.} Charon accepts specific roots
(individual functions and impls); the extraction scripts in each companion
repo (\code{extract.sh}, \code{extract-scalar.sh}) name exactly the
arithmetic functions and get a small, clean model --- 28 definitions
instead of a thousand.
\item \textbf{Some code will not translate.} The dalek scalar-multiplication
backends use CPU-specific SIMD intrinsics no translator models. The
boundary is then \emph{documented}: those functions enter the trusted base,
stated as assumptions, visible in every audit. Honest boundaries beat
heroic fictions (Chapter~\ref{ch:honesty} dwells on this).
\item \textbf{Pin your tools.} The pipeline records exact versions of
Charon, Aeneas, and Lean. A model regenerated with a different translator
version is a \emph{different model}; reproducibility of the proofs starts
with reproducibility of the artifact under proof.
\end{itemize}
\begin{pitfall}
When an extraction fails or a model looks bizarre, the temptation is to
``fix'' the generated Lean by hand. Resist absolutely. A hand-edited model
is a hand-transcription with extra steps --- the exact hole this pipeline
exists to close. The fixes live in extraction scope (choose different
roots), in the source (rarely), or in documented assumptions (openly).
\end{pitfall}
\begin{tryit}
Open the companion repo \code{dalek-ed25519-verified}: read
\code{extract.sh} (the roots), skim \code{verification/gen/Funs.lean} for
\code{add}/\code{sub} (recognize the load-add-store pattern above), then
read the first twenty lines of \code{verification/Proofs/FieldSpec.lean}
and identify: the bounds invariant, the \lean{Result} handling, and the
statement of the theorem. You now recognize every structural element. The
mathematics inside is Chapters~\ref{ch:denotation} and~\ref{ch:field}.
\end{tryit}
\section*{Exercises}
\exercise{The Rust expression \rust{output.0[i] += rhs.0[i]} hides four
distinct failure/effect points that the Lean model makes explicit. Name
them. (Hint: two indexings, one arithmetic operation, one write.)}
\exercise{Suppose limbs are bounded by $2^{54}$. What is the largest value
\lean{a0 + b0} can take, and how many such additions can chain before a
\lean{U64} overflow becomes possible? Show the margin calculation --- this
is precisely why the invariant is $2^{54}$ and not $2^{63}$.}
\exercise{(Design) Your colleague proposes verifying a hand-written Lean
``reference implementation'' instead of the extracted model, because it is
prettier. List two failure modes this reintroduces, and one legitimate use a
reference implementation still has (hint: Chapter~\ref{ch:denotation} uses
one as the \emph{specification} side).}
\begin{checkpoint}
You should now be able to: draw the Rust $\to$ LLBC $\to$ Lean pipeline and
say what each stage preserves; explain why generated models are never
hand-edited; read a \lean{Result}-typed extracted function and point to
where overflow lives; and state why ``the proof needs a bounds hypothesis''
is a discovery about the \emph{code}, not a weakness of the method.
\end{checkpoint}

190
chapters/ch09-denotation-bridge.tex Normal file
View file

@ -0,0 +1,190 @@
\chapter{The Denotation Bridge: What Do Five Numbers \emph{Mean}?}
\label{ch:denotation}
\section{Two worlds, one bridge}
We now hold two very different objects. On one side, mathematics:
the field $\Fp$, where elements are abstract clock positions and $+$ means
ideal modular addition. On the other side, the extracted model: arrays of
five \lean{U64} words, shuffled by loads, adds, and stores. The entire
question of verified cryptography is how to say --- precisely --- that the
second \emph{implements} the first.
The answer is a single function, small enough to write on one line and
important enough to carry this whole book. Given limbs
$a = (a_0, a_1, a_2, a_3, a_4)$, define the \textbf{denotation}:
\[
\denote{a} \;=\; a_0 + 2^{51} a_1 + 2^{102} a_2 + 2^{153} a_3 + 2^{204} a_4
\;\in\; \Fp .
\]
Read $\denote{a}$ as ``the field element these limbs \emph{mean}.'' It is
positional notation, nothing more --- base $2^{51}$ instead of base 10, with
the result interpreted on the clock face of $\Fp$. In Lean:
\begin{lstlisting}[language=Lean]
def denote (a : Array U64 5) : ZMod p :=
a[0].val + 2^51 * a[1].val + 2^102 * a[2].val
+ 2^153 * a[3].val + 2^204 * a[4].val
\end{lstlisting}
With the bridge in hand, correctness of an operation becomes a
\emph{commuting square} --- one picture you should internalize until you see
it in your sleep:
\begin{center}
\begin{tikzpicture}[
world/.style={font=\small,align=center},
arr/.style={-{Stealth},thick,ink2},
lbl/.style={font=\small\color{ink2}}
]
\node[world] (tl) at (0,2.6) {$(a, b)$\\ \footnotesize limb arrays};
\node[world] (tr) at (7.2,2.6) {$\mathtt{add}(a,b)$\\ \footnotesize limb array};
\node[world] (bl) at (0,0) {$(\denote{a}, \denote{b})$\\ \footnotesize field elements};
\node[world] (br) at (7.2,0) {$\denote{a} + \denote{b}$\\ \footnotesize field element};
\draw[arr] (tl) -- node[lbl,above] {machine code} (tr);
\draw[arr] (bl) -- node[lbl,below] {ideal math} (br);
\draw[arr] (tl) -- node[lbl,left] {$\denote{\cdot}$} (bl);
\draw[arr] (tr) -- node[lbl,right] {$\denote{\cdot}$} (br);
\node[font=\small\color{accent},align=center] at (3.6,1.3)
{\textbf{the theorem:}\\ both routes agree};
\end{tikzpicture}
\end{center}
\begin{bigidea}
\textbf{The correctness of an implementation is the statement that
denotation commutes with every operation:}
\[
\denote{\mathtt{add}(a,b)} = \denote{a} + \denote{b},
\qquad
\denote{\mathtt{mul}(a,b)} = \denote{a} \cdot \denote{b},
\qquad\dots
\]
The left-hand side lives in the machine world (with its bounds hypotheses
and \lean{Result}s); the right-hand side is pure mathematics. One equation
per operation, and the ugly optimized code is pinned, forever, to the
textbook meaning. Every verified-crypto project you will ever read is this
diagram, instantiated.
\end{bigidea}
\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
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
Chapter~\ref{ch:rust} just adds limbs pairwise, letting values drift above
$2^{51}$, and nobody reduces until a cheaper moment. The commuting square
still closes because $\denote{\cdot}$ doesn't care how bloated the limbs are
--- positional value is positional value.
This is also exactly where the carry bugs of Chapter~\ref{ch:why} live: code
that is correct only while the drift stays within headroom, and wrong on the
rare inputs where it spills. In the verified development that danger becomes
a visible, machine-checked pair of clauses attached to every operation:
\begin{lstlisting}[language=Lean]
theorem add_spec (ha : Bnd54 a) (hb : Bnd54 b) :
∃ c, add a b = .ok c
∧ Bnd55 c -- (1) bounds: the envelope holds
∧ denote c = denote a + denote b -- (2) value: the meaning is right
\end{lstlisting}
Clause (2) is the commuting square. Clause (1) feeds the \emph{next}
operation's hypothesis --- correctness composes only because every theorem
hands the following one the envelope it requires. A chain of such specs is
the formal skeleton of ``this sequence of optimized operations computes the
formula we claim.''
\begin{aha}
The denotation idea is vastly older and bigger than cryptography. Compilers
prove ``optimized code means the same as naive code''; databases prove
``this query plan means the same query''; hardware verifies ``this pipelined
circuit means this instruction set.'' The pattern --- map both sides into a
mathematical meaning-space and prove the square commutes --- is called
\emph{denotational semantics}, and you have now used it for real. It is the
single most transferable idea in this book.
\end{aha}
\section{Multiplication: where the bridge earns its keep}
Addition's square closes in an afternoon. Multiplication is the boss fight,
and seeing \emph{why} teaches you what verified arithmetic is really like.
Schoolbook multiplication of two 5-limb numbers produces nine columns of
partial products $\sum_{i+j=k} a_i b_j$; each column then owes a
\emph{carry} to the next; and columns $k \ge 5$ --- weights $2^{255}$ and up
--- must be folded back using the Chapter~\ref{ch:modular} identity
$2^{255} \equiv 19$. The implementation interleaves all three concerns for
speed. The proof must un-interleave them:
\[
\denote{\mathtt{mul}(a,b)}
\;\overset{?}{=}\;
\Big(\textstyle\sum_{k=0}^{8} 2^{51k} \sum_{i+j=k} a_i b_j \Big) \bmod p
\;\overset{?}{=}\; \denote{a} \cdot \denote{b} .
\]
The right equality is algebra --- \lean{ring} territory. The left is a walk
through the extracted code: every intermediate \lean{U128} product bounded
(no overflow --- the $2^{54}$ headroom at work), every carry accounted,
every $\times 19$ fold placed. In the companion projects this is a long
\lean{calc}-and-\lean{have} museum: dozens of small steps, each dispatched
by \lean{omega} or a bound lemma, composed into one commuting square.
One more representational dialect, because you will meet it in the Pasta
repos: \textbf{Montgomery form} stores $x$ as $x \cdot R \bmod p$ (with
$R = 2^{256}$) because it makes reduction after multiplication cheap. The
bridge absorbs the twist without complaint --- define
$\denote{a}_{\mathrm{M}} = (\text{positional value of } a) \cdot R^{-1}$
and the same commuting squares govern everything. Denotation is a
\emph{policy about meaning}, and it bends to fit the representation, not
the other way around.
\begin{pitfall}
When a denotation proof refuses to close, the failure is information ---
read it like a detective, in order: (1) Is the \emph{bound} hypothesis
strong enough for the intermediate products? (Count bits, on paper.)
(2) Is the \emph{denotation} right for this representation --- radix, limb
count, Montgomery factor? (3) Only then suspect the code. In the companion
projects this checklist ran hundreds of times; its order reflects the actual
base rates of what was wrong.
\end{pitfall}
\begin{tryit}
Open \code{exercises/Ch09.lean}. It builds a miniature of the whole story
you can hold in your head: a \emph{2-limb, radix-4} representation of
$\Zmod{15}$ (limbs are values $0$--$3$, denotation $a_0 + 4a_1$, and
$16 \equiv 1$ makes the fold trivial). You will write \lean{denote}, prove
the commuting square for the provided \lean{add} with carry, then for
\lean{mul} with its fold --- every conceptual ingredient of the dalek proof,
at a scale where \lean{decide} can double-check your work.
\end{tryit}
\section*{Exercises}
\exercise{Compute by hand the denotation of the limb arrays $(19,0,0,0,0)$
and $(0,0,0,0,2^{51})$ in the radix-51 system, reducing mod $p = 2^{255}-19$.
Conclude that $\denote{\cdot}$ is not injective by exhibiting the collision.}
\exercise{In the mini-system of the Try It box, find two distinct limb pairs
denoting the same element of $\Zmod{15}$, and check that the provided
\lean{add} treats them interchangeably \emph{as far as denotation goes} ---
compute both sides.}
\exercise{Sketch the multiplication column sums $\sum_{i+j=k} a_i b_j$ for
the 2-limb system and carry out the fold $16 \equiv 1$ by hand for
$a = (3,2)$, $b = (1,3)$. Check against direct computation in $\Zmod{15}$.}
\exercise{(Paper, challenge) For the radix-51 system with limbs bounded by
$2^{54}$: bound one column $\sum_{i+j=4} a_i b_j$ of partial products and
confirm it fits a \lean{U128}. How much headroom remains? This number ---
not elegance --- is why the invariant chose $2^{54}$.}
\begin{checkpoint}
You should now be able to: write the radix-51 denotation from memory; draw
the commuting square and label which side owns bounds and \lean{Result}s;
explain why many-to-one representation is both the performance trick and
the bug habitat; and recognize the two-clause shape (bounds propagation +
value equation) as the universal skeleton of implementation-correctness
theorems.
\end{checkpoint}

161
chapters/ch10-verifying-a-field.tex Normal file
View file

@ -0,0 +1,161 @@
\chapter{Verifying a Field: The Full Campaign}
\label{ch:field}
\section{The summit statement}
Every thread so far --- specs as types, tactics, automation, $\Fp$,
primality, extraction, denotation --- was preparation for one theorem. In
the companion repositories it is called the \emph{field implementation
certificate}, and (lightly paraphrased) it says:
\begin{lstlisting}[language=Lean]
theorem fieldImplementation :
-- p is prime, so ZMod p is genuinely a field
Nat.Prime p
-- and for all bounded limb arrays, every operation's
-- commuting square closes:
∧ (∀ a b, Bnd a → Bnd b → AddSquare a b)
∧ (∀ a b, Bnd a → Bnd b → SubSquare a b)
∧ (∀ a b, Bnd a → Bnd b → MulSquare a b)
∧ (∀ a, Bnd a → SquareSquare a)
∧ (∀ a, Bnd a → InvertSquare a) -- Fermat chain: a^(p-2)
∧ ... -- reduce, negate, encode
\end{lstlisting}
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
honestly, including the two places where the terrain fought back, because
the failures teach more than the victories.
\section{Order of battle}
You do not prove such a conjunction by heroism; you prove it by sequencing.
The campaign order in the real projects, and the reason for each position:
\begin{enumerate}[leftmargin=1.6em]
\item \textbf{Bounds lemmas first} --- pure \lean{omega} facts about limb
sizes, no denotation at all. Cheap, and everything depends on them.
\item \textbf{Primality} (Chapter~\ref{ch:prime}) --- independent of the
code entirely; it dignifies \lean{ZMod p} into a field.
\item \textbf{add, sub, negate} --- linear operations; the commuting squares
close with \lean{omega} plus the denotation unfolds. Confidence builders.
\item \textbf{reduce} --- the $\times 19$ fold in isolation. Proving it
alone, before mul uses it, halves the hardest proof's size.
\item \textbf{mul, square} --- the boss fight of Chapter~\ref{ch:denotation}:
column sums, carries, folds. Squaring is mul with algebraic shortcuts ---
a separate code path in dalek, hence a separate theorem. No shortcuts
in the proof: the \emph{code's} shortcut is precisely what needs checking.
\item \textbf{invert} --- the 254-squaring Fermat chain, verified as a
\lean{calc} of exponent bookkeeping on top of \code{mul}/\code{square}
specs, ending at $a^{p-2}$; Fermat's little theorem (Mathlib's) closes
the square.
\end{enumerate}
Notice the shape: \emph{each layer consumes only the specs of the layer
below}, never reaching into implementations. By step 6 you are doing exponent
arithmetic, blissfully ignorant of carries. That is the compositionality that
Chapter~\ref{ch:denotation}'s two-clause specs (bounds + value) were designed
to buy.
\section{Dispatches from the terrain}
\textbf{The wall that was really there.} Partway up, one proof style hit a
genuine limit of the tool: correctness certificates for \code{mul}-scale
goals, when handed to a general decision procedure in one monolithic call,
generate internal certificates with coefficients on the order of $2^{256}$
--- and checking them can exhaust the proof checker's memory. One such call,
during the development of the Pasta field proofs, consumed twelve gigabytes
and crashed the machine (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
searching for one), and let the big theorem be an assembly of small
checked parts. The same discipline, plus hard memory caps on the checker
process, became house infrastructure.
\begin{aha}
There is a deep symmetry in that fix worth savoring: the \emph{proof} was
restructured exactly the way the \emph{code} was --- into small steps with
controlled intermediate size. Delayed carries in the implementation; small
lemmas in the verification. Bounded limbs; bounded contexts. Good proofs and
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
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
constant-time conditional selection three different ways (a \code{subtle}
crate trait, a volatile-read \code{black_box}, a hand-rolled arithmetic
mask), and one fork reorders instructions in point doubling. All correct ---
\emph{provably}, now --- but the divergence is exactly the kind of thing
that silently breaks when someone ``harmonizes'' code during a rebase.
Per-fork verification is not pedantry; it is how you notice that ``the same
library'' isn't.
\begin{pitfall}
A verified fork is verified \emph{at a commit}. Change one line of
arithmetic and the certificate is stale --- that is a feature (the proof
\emph{should} break when the code changes), but it means verification is a
\emph{process wired into maintenance}, not a trophy. The companion repos
ship \code{check.sh} scripts that re-extract and re-verify from scratch;
treat those as the project's pulse, not as CI decoration.
\end{pitfall}
\section{Reading a certificate like a professional}
Suppose a stranger hands you a repository claiming ``formally verified
field arithmetic.'' Chapter~\ref{ch:honesty} gives you the full audit
protocol, but the field-layer questions you can already ask are these:
\begin{itemize}[leftmargin=1.4em]
\item \textbf{What is denoted?} Find the denotation function. Does it map
the \emph{extracted} representation (good) or a hand-written lookalike
(Chapter~\ref{ch:rust}'s hole)?
\item \textbf{Is the square complete?} Value equation \emph{and} bounds
propagation \emph{and} the \lean{.ok} clause --- a spec that assumes
success proves nothing about overflow.
\item \textbf{Is the quantifier honest?} \lean{∀ a b} with bounds
hypotheses, or a handful of \lean{example}s on constants dressed up as
coverage?
\item \textbf{Does anything say \lean{sorry}?} One \lean{sorry} anywhere in
the dependency chain and the certificate is decorative. The checker will
tell you; ask it.
\end{itemize}
\begin{tryit}
Do the audit for real: open \code{dalek-ed25519-verified}, find the
denotation, pick the \code{sub} spec, and check the three clauses against
the list above. Then run the repo's \code{check.sh} and watch the whole
pyramid rebuild. Total time: one coffee. Skill acquired: permanent.
\end{tryit}
\section*{Exercises}
\exercise{Field subtraction in dalek computes $a - b$ as
$a + (16p - b)$ limb-wise (adding a multiple of $p$ keeps limbs positive ---
recall \lean{Nat} truncation!). State the commuting square for \code{sub}
including the exact multiple-of-$p$ fact you would need as a lemma, and
explain why $16p$ rather than $p$.}
\exercise{The Fermat inversion chain computes $a^{p-2}$ via 254 squarings
and 11 multiplications. Verify the exponent bookkeeping for the first three
steps of dalek's actual chain: $a^2$, $a^{9} = (a^2)^{2\cdot 2} \cdot a$,
$a^{11} = a^9 \cdot a^2$. (The full chain is exercise-by-induction: each
step's exponent is a sum of previous ones --- addition-chain arithmetic.)}
\exercise{(Discussion) Step 5 refuses to trust the squaring shortcut and
verifies \code{square} separately from \code{mul}. A colleague argues
``square is just \code{mul a a}, reuse the theorem.'' What, concretely,
would that argument miss about the code under verification?}
\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
and \code{reduce} come early; tell the memory-wall story and its
decomposition moral; and audit a stranger's field-layer claim with four
pointed questions.
\end{checkpoint}

167
chapters/ch11-honesty-and-axioms.tex Normal file
View file

@ -0,0 +1,167 @@
\chapter{Honesty, Axioms, and the Art of Trusting Proofs}
\label{ch:honesty}
\section{``Formally verified'' is a claim, not a spell}
The phrase \emph{formally verified} has marketing gravity, and marketing
gravity attracts abuse. This chapter arms you with the auditor's toolkit:
what a Lean certificate actually rests on, how to interrogate it in one
command, and the specific ways a verification claim can be hollow while
every file compiles. Nothing here is hypothetical --- each failure mode
appears in the wild, and the discipline below is the one the companion
projects hold themselves to.
\section{The trust ledger}
When the kernel accepts \lean{fieldImplementation}, what exactly are you
being asked to believe? Lean can tell you --- precisely:
\begin{lstlisting}[language=Lean]
#print axioms fieldImplementation
-- 'fieldImplementation' depends on axioms:
-- [propext, Classical.choice, Quot.sound]
\end{lstlisting}
\lean{\#print axioms} walks the \emph{entire} dependency tree of a theorem
--- every lemma, every lemma's lemmas, down to bedrock --- and reports every
assumption found there. The three names above are Lean's standard trio
(propositional extensionality, classical choice, quotient soundness):
ordinary classical mathematics, accepted by working mathematicians,
scrutinized by logicians for a century. A certificate reporting exactly
these three is called \textbf{axiom-clean}. Anything \emph{else} in that
list is a custom assumption someone added --- and the whole audit consists
of reading that list and asking whether you believe each entry.
\begin{bigidea}
A machine-checked theorem is a receipt with a complete list of its own
assumptions --- something prose mathematics has never had. But the receipt
only protects people who read it. \textbf{The one-command audit:} run
\lean{\#print axioms} on the headline theorem; anything beyond
\lean{[propext, Classical.choice, Quot.sound]} is where the bodies are
buried. Make this reflex, and no verification claim can hide from you.
\end{bigidea}
\section{A field guide to hollow certificates}
Compiling proofs can still be worthless. The four classic ways, in
increasing order of subtlety:
\textbf{1. The \lean{sorry}.} Lean's placeholder accepts any goal with a
warning. Fine for work in progress; fatal in a certificate, because
downstream theorems inherit the hole silently. Detection: the compiler
warns, and \lean{\#print axioms} shows \lean{sorryAx}. Trivial to catch ---
if you look.
\textbf{2. The smuggled axiom.} Stuck on a lemma? \lean{axiom} makes it
true. Sometimes legitimate (see the trusted-base section below); rotten when
undisclosed --- a proof ``of'' the group law that axiomatizes the hard
half of the group law is theater. Detection: \lean{\#print axioms}, always.
\textbf{3. The trivial specification.} The most instructive one. Consider:
\begin{lstlisting}[language=Lean]
theorem mul_correct : ∀ a b, ∃ c, mul a b = c := by
intro a b; exact ⟨_, rfl⟩ -- checks! and says NOTHING
\end{lstlisting}
Kernel-approved, axiom-clean, and utterly empty: ``mul returns whatever it
returns.'' No tool catches this, because nothing is wrong \emph{formally}
--- the defect is that the statement doesn't say what the reader assumes it
says. The only detector is a human reading the \emph{statement} (never mind
the proof) and asking: \emph{if the code were wrong, would this theorem
fail?} For the trivial spec, the answer is no --- a buggy \code{mul}
satisfies it identically.
\textbf{4. The wrong model.} The proof is real, the spec is strong --- but
the thing verified isn't the thing that ships: a hand-transcription
(Chapter~\ref{ch:rust}), a stale extraction, a simplified semantics.
Detection: trace the chain from artifact to source --- extraction scripts,
pinned tool versions, regeneration instructions. If the chain can't be
replayed, the claim is about an orphan.
\begin{pitfall}
Rank these by danger and notice the inversion: the crude failures
(\lean{sorry}, smuggled axioms) are machine-detectable in seconds, while
the subtle ones (trivial specs, wrong models) defeat every automated check
and yield only to a thoughtful reader. Verification does not eliminate the
need for human judgment; it \emph{concentrates} all of it into two small,
well-lit places --- the statement and the model. That concentration is the
gift; squandering it by not reading the statement is the sin.
\end{pitfall}
\section{Honest boundaries: the trusted base}
Real projects meet real limits: SHA-512's compression function, SIMD
backends no translator models, foreign function calls. The honest move is
not to pretend, but to \emph{declare}: state the unverified piece as an
explicit assumption, document it in a ledger (the companion repos call
theirs \code{TRUSTED-BASE.md}), and let \lean{\#print axioms} carry the
disclosure to every downstream theorem automatically.
\begin{lstlisting}[language=Lean]
-- Declared, documented, and visible in every audit forever:
axiom sha512_spec : ∀ msg, Sha512.hash msg = SHA512_ideal msg
\end{lstlisting}
A signature-layer certificate honestly reads: \emph{EdDSA verification is
correct, GIVEN the hash behaves ideally and GIVEN the documented backend
assumptions} --- with both \emph{given}s machine-visible. Compare the two
postures: ``everything verified!'' (and hope nobody checks) versus ``these
two assumptions, this ledger, audit me'' --- the second is both humbler and
\emph{stronger}, because its claim survives the audit.
The companion projects add one more layer of candor worth copying: a
\emph{failure map}. Their control repository documents the dead ends ---
tactic patterns that exhaust memory, extraction scopes that drag in the
world, proof styles that don't scale --- each with the tell that identifies
it early. Knowledge of where the cliffs are is part of the method, and
pretending the cliffs don't exist is how the next person walks off one.
\begin{aha}
Notice the running theme: at every level, the methodology converts
\emph{invisible} trust into \emph{visible} trust. Extraction made the
code-to-model step visible; two-clause specs made operating envelopes
visible; \lean{\#print axioms} makes logical debts visible; the trusted-base
ledger makes engineering limits visible. Formal verification's deepest
product is not certainty --- it is \textbf{legibility of exactly what
remains uncertain}.
\end{aha}
\begin{tryit}
Audit the real thing. In \code{dalek-ed25519-verified}, run
\lean{\#print axioms} on \code{fieldImplementation} and
\code{edwardsImplementation} --- confirm the clean trio. Then read
\code{TRUSTED-BASE.md} and match each entry to where it would surface in an
audit. Finally, write a deliberately trivial spec for \code{add}, prove it
in one line, and observe that every automated check passes. Keep that file
open for one full minute. That minute is the chapter.
\end{tryit}
\section*{Exercises}
\exercise{For each hollow-certificate species, name its detector: (a)
\lean{sorry}; (b) smuggled axiom; (c) trivial spec; (d) wrong model. Which
two can a CI pipeline catch mechanically, and what CI check would you write
for each?}
\exercise{Strengthen this spec until a buggy implementation would fail it:
\lean{theorem sub_ok : ∀ a b, ∃ c, sub a b = .ok c}. (List what's missing:
bounds hypotheses? bounds propagation? the value equation? Compare with
Chapter~\ref{ch:denotation}'s two-clause shape.)}
\exercise{A vendor's whitepaper says: ``Our signature library is formally
verified in Lean.'' Draft the five questions you would send them, in
priority order, and the answer you would require for each before relying on
the claim. (You now know all five.)}
\exercise{(Discussion) The trusted-base \lean{axiom} for SHA-512 and the
smuggled \lean{axiom} for a hard lemma are the \emph{same language feature}.
Articulate the difference in one sentence --- it is not technical.}
\begin{checkpoint}
You should now be able to: run and interpret the one-command audit; name
the standard three axioms and greet anything else with suspicion; explain
why trivial specs and wrong models defeat automation and what defeats
\emph{them}; and argue --- with conviction --- why a declared trusted base
is stronger, not weaker, than a claim of totality.
\end{checkpoint}

158
chapters/ch12-the-pyramid.tex Normal file
View file

@ -0,0 +1,158 @@
\chapter{The Pyramid: From Field to Signature, and Where You Come In}
\label{ch:pyramid}
\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
--- what each one \emph{states}, what makes each one \emph{hard}, and where
the campaign stands as this book goes to press --- then hands you the map
and the keys.
\begin{center}
\begin{tikzpicture}[
lay/.style={draw=ink2,thick,rounded corners=2pt,align=center,minimum height=1.0cm},
st/.style={font=\footnotesize\color{ink2},anchor=west,align=left}
]
\node[lay,fill=accentsoft,minimum width=3.0cm] (sig) at (0,3.75) {\textbf{Signature}};
\node[lay,fill=warnsoft,minimum width=5.4cm] (sca) at (0,2.5) {\textbf{Scalars mod $\boldsymbol{\ell}$}};
\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,2.5) {\textbf{in progress}: foundations proven,\\ mul at the kernel frontier};
\node[st] at (5.7,3.75) {\textbf{ahead}: awaits scalars;\\ hash axiomatized by design};
\end{tikzpicture}
\end{center}
\section{The group law: geometry becomes algebra}
An elliptic curve is a set of points $(x,y)$ satisfying an equation; for
Ed25519 it is the \emph{twisted Edwards} curve
$-x^2 + y^2 = 1 + d\,x^2 y^2$ over $\Fp$. The miracle: these points form a
\emph{group} under the addition law
\[
(x_1,y_1) + (x_2,y_2) \;=\;
\left(
\frac{x_1 y_2 + x_2 y_1}{1 + d\,x_1 x_2 y_1 y_2},\;
\frac{y_1 y_2 + x_1 x_2}{1 - d\,x_1 x_2 y_1 y_2}
\right).
\]
Two facts make this law a verifier's dream, and both carry Edwards-curve
signatures for exactly this reason. First, it is \textbf{complete}: for the
Ed25519 parameters those denominators are \emph{never zero} --- no special
cases for doubling, no branch for the identity, hence constant-time-friendly
code with no rarely-taken paths for bugs to hide in. (The proof, due to
Bernstein and Lange, is a jewel of quiet algebra: if a denominator vanished,
$d$ would have to be a square in $\Fp$ --- and it is not, which is a
\lean{decide}-scale fact away from primality.) Second, the implementation
represents points \emph{projectively} (extended coordinates $(X:Y:Z:T)$,
avoiding division entirely) --- so the layer has its own denotation,
$(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.
\section{Scalars: a second field, and a frontier}
The group of curve points has order $8\ell$ with
$\ell = 2^{252} + 27742\ldots$ prime. Signature arithmetic happens in
exponents --- multiples of points --- so it is arithmetic mod $\ell$: a
\emph{second} finite field, with its own Rust implementation (radix-52
limbs, Montgomery multiplication) and its own denotation bridge. Nothing
conceptually new --- which is itself the lesson: the method \emph{scales
sideways} without new ideas.
The engineering, however, has a frontier, and this book has told you enough
truth to locate it precisely. Scalar Montgomery multiplication mixes
$2^{256}$-scale coefficients into single certificate steps; this is the
kernel-capacity wall of Chapter~\ref{ch:field}, and it marks the current
working edge of the campaign: additions and the foundational constants are
certified (including the pleasing theorem that the code's constant
\code{L} \emph{is} $\ell$); the multiplication path is a construction site
with scaffolding --- decomposed lemmas, isolated carry steps ---
mid-assembly, honestly labeled in-repo.
\section{The apex: what ``verified signature'' will say}
EdDSA verification accepts $(R, s)$ on message $m$ under key $A$ iff
\[
8 s B \;=\; 8 R + 8\,H(R, A, m)\,A
\]
in the curve group ($B$ the base point, $H$ = SHA-512, the $8$s absorbing
the cofactor). The apex certificate will state: \emph{the extracted
verification routine returns true exactly when this equation holds} ---
given the two declared trusted-base entries you can already predict:
SHA-512 as an ideal hash (axiomatized by design --- hash function
correctness is a different mathematical universe), and the SIMD
point-multiplication backends (untranslatable, documented). Everything
between those declared boundaries and the field bedrock: kernel-checked,
axiom-clean, per fork.
Read that sentence again with Chapter~\ref{ch:honesty} eyes: it is a
\emph{smaller} claim than ``Ed25519 is verified!'' --- and that is exactly
why you can believe it.
\section{What you now know, and where to take it}
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
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{Extend the pyramid.} The scalar layer's open lemmas are
decomposed, labeled, and waiting; the repos' \code{CONTRIBUTING} notes
state exactly what a finished brick looks like (spec shape, axiom
audit, check-script entry). Frontier work, undergraduate-accessible.
\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}
\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
\emph{deliberate off-by-one carry bug} in a variant \lean{add'} --- of
exactly the species from Chapter~\ref{ch:why}: correct on all limb pairs
except a thin boundary slice. Your final tasks: (1) write the spec ---
watch it \emph{refuse to prove}; (2) extract the counterexample from the
stuck goal state; (3) confirm by \lean{\#eval}; (4) fix the code and finish
the proof. That arc --- spec, refusal, counterexample, fix, certificate ---
is the entire profession in miniature. Welcome to it.
\end{tryit}
\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
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.
\end{checkpoint}

57
exercises/Ch02.lean Normal file
View file

@ -0,0 +1,57 @@
/- Chapter 2 — Meet Lean: exercises.
Replace each `sorry` and watch the warnings disappear.
Check your work: every `#eval` line below a definition should print
the value promised in its comment. -/
namespace Ch02
-- The constant that follows us through the whole book.
def p : Nat := 2 ^ 255 - 19
def double (n : Nat) : Nat := 2 * n
/- Exercise A (from the Try It box): multiplication by recursion.
Define `mul` using `Nat.add` (or `+`), by recursion on the second
argument — the same bootstrapping order (add, then mul) the real
field proofs follow. Do NOT use `*`. -/
def mul : Nat → Nat → Nat
| _, Nat.zero => sorry
| m, Nat.succ n => sorry
-- uncomment when your definition is in place:
-- #eval mul 6 7 -- expected: 42
-- #eval mul 0 9 -- expected: 0
/- Exercise 2.1: exponentiation by recursion on the exponent.
Do NOT use `^`. You may use `*`. -/
def pow : Nat → Nat → Nat
| _, Nat.zero => sorry
| b, Nat.succ e => sorry
-- #eval pow 2 10 -- expected: 1024
/- Exercise 2.2: the Fibonacci numbers, naive recursion.
Then evaluate `fib 32` and notice the pause: your ALGORITHM is
exponential even though #eval itself is fast. -/
def fib : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => sorry
-- #eval fib 10 -- expected: 55
/- Exercise 2.3: a structure with a smuggled weakness.
Complete `Rational.add` (school formula: a/b + c/d = (ad+cb)/(bd)).
Then answer in a comment: what property of `den` can this type NOT
enforce yet? (Chapter 3 gives the tool to fix it.) -/
structure Rational where
num : Int
den : Nat
def Rational.add (x y : Rational) : Rational :=
sorry
-- #eval (Rational.add ⟨1, 2⟩ ⟨1, 3⟩).num -- expected: 5
-- #eval (Rational.add ⟨1, 2⟩ ⟨1, 3⟩).den -- expected: 6
end Ch02

43
exercises/Ch03.lean Normal file
View file

@ -0,0 +1,43 @@
/- Chapter 3 — Propositions as Types: exercises.
Rules of the game: TERM MODE ONLY — no `by`, no tactics.
Your toolkit: fun ... => ..., function application, And.intro,
h.1 / h.2, Or.inl / Or.inr, match ... with. -/
namespace Ch03
variable (P Q R : Prop)
-- Warm-ups from the Try It box ---------------------------------------------
/- W1: "if P then (Q implies P)". A constant function. -/
theorem const_imp : P → Q → P :=
sorry
/- W2: a conjunction gives a disjunction (pick a side). -/
theorem and_to_or : P ∧ Q → P ∨ Q :=
sorry
/- W3: modus ponens — "calling a function". -/
theorem modus_ponens : P → (P → Q) → Q :=
sorry
-- Numbered exercises --------------------------------------------------------
/- 3.1: reassociate evidence with h.1, h.2, And.intro. -/
theorem and_assoc' : (P ∧ Q) ∧ R → P ∧ (Q ∧ R) :=
sorry
/- 3.2: case analysis on which side holds.
Shape: fun h => match h with
| Or.inl p => ...
| Or.inr q => ... -/
theorem or_swap : P ∨ Q → Q ∨ P :=
sorry
/- 3.3: Not P is DEFINED as P → False. Unfold it in your head, and this
becomes a two-argument function. Afterwards, write in a comment the
one-sentence description of the program you wrote. -/
theorem not_not_intro : P → ¬¬P :=
sorry
end Ch03

52
exercises/Ch04.lean Normal file
View file

@ -0,0 +1,52 @@
/- Chapter 4 — Tactics: exercises.
Now the game flips: TACTIC MODE. Place your cursor after each `by`
and watch the goal state as you work.
We define our own addition so the standard library can't spoil the fun. -/
namespace Ch04
/-- Our own Nat addition, recursion on the SECOND argument —
so `n + 0 = n`-style facts about `myAdd m 0` need REAL proofs. -/
def myAdd : Nat → Nat → Nat
| m, Nat.zero => m
| m, Nat.succ n => Nat.succ (myAdd m n)
/- Warm-up (worked in the chapter): and_swap in tactic mode.
Tactics: intro, constructor, exact. Goal state drawn for you:
P Q : Prop
⊢ P ∧ Q → Q ∧ P -/
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := by
sorry
/- 4.1a: the definitional direction is free... but this one is not.
`myAdd 0 n = n` needs induction on n.
Cases will be: zero: ⊢ myAdd 0 0 = 0 (computes: rfl)
succ: ih : myAdd 0 k = k
⊢ myAdd 0 (k+1) = k+1 (unfold one step, use ih)
Useful: `simp only [myAdd]` unfolds one layer of the definition,
or `rw [myAdd]`; then `rw [ih]`. -/
theorem zero_myAdd (n : Nat) : myAdd 0 n = n := by
sorry
/- 4.1b: the mirror image of the second defining equation. -/
theorem succ_myAdd (m n : Nat) : myAdd (Nat.succ m) n = Nat.succ (myAdd m n) := by
sorry
/- 4.2: commutativity, by induction on n, using 4.1a and 4.1b.
Write ONE prose sentence per case in a comment when you're done. -/
theorem myAdd_comm (m n : Nat) : myAdd m n = myAdd n m := by
sorry
/- 4.3: repair the broken calc chain. Exactly ONE step below is wrong.
Find it (read the goal state where the error appears!), fix it, done.
This is the most realistic job training in this book.
theorem calc_repair (a b : Nat) (h : a = 2 * b) : a + a + b = 5 * b := by
calc a + a + b = 2 * a + b := by omega
_ = 2 * (2 * b) + b := by rw [h]
_ = 4 * b + b := by omega
_ = 6 * b := by omega -- ← suspicious…
-/
end Ch04

55
exercises/Ch05.lean Normal file
View file

@ -0,0 +1,55 @@
/- Chapter 5 — Numbers and Automation: exercises.
Ten goals; each is solved by exactly ONE of
omega / ring / norm_num / decide
in one shot. Your task is to close each with the RIGHT tool —
overkill is rejected by design (and by your conscience).
Requires Mathlib (see README for setup). -/
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum
import Mathlib.Data.Nat.Prime.Basic
namespace Ch05
-- G1: bounds bookkeeping — the everyday goal of verified arithmetic.
example (a b : Nat) (h1 : a < 2^51) (h2 : b < 2^51) : a + b < 2^52 := by
sorry
-- G2: truncated Nat subtraction, handled honestly.
example (a b : Nat) (h : a ≤ b) : a + (b - a) = b := by
sorry
-- G3: a polynomial identity in any commutative ring.
example (a b : Int) : (a + b) * (a - b) = a * a - b * b := by
sorry
-- G4: a concrete numeric fact with big numbers.
example : (2:Int)^255 - 19 > 2^254 := by
sorry
-- G5: a finite check.
example : Nat.Prime 97 := by
sorry
-- G6: linear again — with a twist of multiplication BY A CONSTANT.
example (x : Nat) (h : 3 * x + 7 ≤ 100) : x ≤ 31 := by
sorry
-- G7: pure numeral arithmetic.
example : 2^51 + 2^51 = 2^52 := by
sorry
-- G8: binomial cube.
example (x y : Int) : (x + y)^3 = x^3 + 3*x^2*y + 3*x*y^2 + y^3 := by
sorry
-- G9 (exercise 5.2, the two-step pattern): nonlinear, so omega alone
-- fails. First BOUND the product with mul-monotonicity, then release
-- the linear solver. Useful: Nat.mul_lt_mul'' or Nat.mul_le_mul.
example (a b : Nat) (ha : a < 100) (hb : b < 100) : a * b < 10000 := by
sorry
-- G10: the Chapter 4 cliffhanger. Multiplication by 19 is linear!
example (a : Nat) (h : a < 2^51) : a * 19 < 2^56 := by
sorry
end Ch05

47
exercises/Ch06.lean Normal file
View file

@ -0,0 +1,47 @@
/- Chapter 6 — Modular Arithmetic: exercises.
The clock worlds ZMod n, hands on. Requires Mathlib. -/
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum
import Mathlib.FieldTheory.Finite.Basic
namespace Ch06
-- First contact: run these and read the answers.
#eval (7 + 8 : ZMod 12) -- ?
#eval (3 - 7 : ZMod 12) -- ? (wraps — no truncation)
#eval (3⁻¹ : ZMod 7) -- 6.1: your first inverse. Check 3 * answer = 1!
#eval (4⁻¹ : ZMod 11) -- (the chapter's clock picture says 3)
#eval (4⁻¹ : ZMod 12) -- what does Lean do when NO inverse exists?
/- 6.A: a cube expansion in a tiny field — one tactic. -/
example (x y : ZMod 7) :
(x + y)^3 = x^3 + 3*x^2*y + 3*x*y^2 + y^3 := by
sorry
/- 6.B (exercise 6.2): four has no inverse on the twelve-hour clock —
twelve cases, and you know the tactic that tries them all. -/
example : ∀ x : ZMod 12, 4 * x ≠ 1 := by
sorry
/- 6.C: …then change the modulus to 13 and the SAME tactic must refuse:
the statement becomes false. Find the witness: what is 4⁻¹ mod 13?
(Answer with an #eval, then explain in one comment line.) -/
-- Mathlib's Fermat lemma needs to KNOW 11 is prime — as a typeclass
-- fact. This is how you register arithmetic facts for instance search:
instance : Fact (Nat.Prime 11) := ⟨by decide⟩
/- 6.D (exercise 6.3): Fermat's little theorem from the library.
`ZMod.pow_card_sub_one_eq_one` says a^(p-1) = 1 for a ≠ 0.
Use it (with `show`/`calc`/`rw` as you like) to prove: -/
example (a : ZMod 11) (h : a ≠ 0) : a^10 = 1 := by
sorry
/- 6.E: the crown fact of the chapter, stated in the real field. -/
def p : Nat := 2^255 - 19
example : (2^255 : ZMod p) = 19 := by
sorry
end Ch06

64
exercises/Ch07.lean Normal file
View file

@ -0,0 +1,64 @@
/- Chapter 7 — Primality certificates: exercises.
The ladder: certify ever-larger primes, watching what each tool costs.
Requires Mathlib. -/
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.NormNum.Prime
namespace Ch07
/- 7.A: rung one — a two-digit prime. `decide` grinds trial division
in the kernel; at this size that is instant. -/
example : Nat.Prime 97 := by
sorry
/- 7.B: rung two — the Fermat prime 65537 = 2^16 + 1 (of RSA fame).
Try `decide` first and FEEL the pause (kernel trial division is
quadratic pain). Then switch to `norm_num`, whose prime extension
builds a certificate instead. Keep whichever is honest AND fast. -/
example : Nat.Prime 65537 := by
sorry
/- 7.C: rung three — the Mersenne prime 2^31 - 1 (ten digits).
Kernel trial division is now out of the question; `norm_num`'s
certificate route answers in seconds. That difference IS the chapter.
(Curious how far certificates scale? 2^61 - 1 already needs minutes —
witness trees are cheap to CHECK but costly to FIND.)
Hint: norm_num's prime extension wants a LITERAL numeral; `show` can
convert the goal to a definitionally equal one first. -/
example : Nat.Prime (2^31 - 1) := by
sorry
/- 7.D: your own hands on a Pratt witness (paper + #eval).
For p = 13: verify that w = 2 satisfies both witness conditions:
w^(p-1) = 1 (mod p) and w^((p-1)/q) ≠ 1 (mod p)
for each prime q dividing p - 1 = 12 (namely q = 2 and q = 3).
Fill in the two missing #evals; check against hand computation. -/
#eval (2:ZMod 13)^12 -- must be 1
-- #eval ... -- w^(12/2): must NOT be 1
-- #eval ... -- w^(12/3): must NOT be 1
/- 7.E (the finale): the top node of the certificate for the real prime,
checked with your own modular exponentiation. First, implement fast
square-and-multiply: at each step, square the base, halve the
exponent, and fold the base into the accumulator when the exponent
bit is 1. (The `fuel` argument just guarantees termination; 300 > the
255 bits we need.) -/
def powModAux : Nat → Nat → Nat → Nat → Nat → Nat
| 0, _, _, _, acc => acc
| fuel+1, b, e, m, acc =>
sorry -- if e = 0 we are done; otherwise recurse as described above
def powMod (b e m : Nat) : Nat :=
if m ≤ 1 then 0 else powModAux 300 (b % m) e m 1
-- sanity checks for your powMod:
-- #eval powMod 2 12 13 -- expected: 1
-- #eval powMod 3 4 7 -- expected: 4 (81 = 11*7 + 4)
/- …then check the first witness condition for w = 2 at 77 digits.
Predict the output before you run it. Note the speed: THAT is why
certificate checking is cheap. -/
def p : Nat := 2^255 - 19
-- #eval powMod 2 (p - 1) p -- prediction: ?
end Ch07

65
exercises/Ch09.lean Normal file
View file

@ -0,0 +1,65 @@
/- Chapter 9 — The Denotation Bridge: exercises.
A complete miniature of the verified-field story, small enough to hold
in your head: TWO limbs, radix FOUR, modulus 15. Because 16 ≡ 1
(mod 15), the top carry folds back with weight 1 — a toy version of
2^255 ≡ 19 (mod p). Requires Mathlib. -/
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.LinearCombination
namespace Ch09
/-- Two limbs, each meant to hold a base-4 digit. -/
abbrev Limbs := Nat × Nat
/-- The bounds invariant: both limbs are genuine base-4 digits. -/
def Bnd (a : Limbs) : Prop := a.1 < 4 ∧ a.2 < 4
/- 9.A: write the denotation — "what field element do these limbs MEAN?"
Positional notation in base 4, read on the clock face of ZMod 15. -/
def denote (a : Limbs) : ZMod 15 :=
sorry
-- sanity: denote (3, 2) should be 11; denote (1, 0) should be 1
-- #eval denote (3, 2) -- expected: 11
/-- Addition with carry, machine-style: limb sums, then carry
propagation, then the TOP carry (weight 16 ≡ 1) folds into limb 0. -/
def add (a b : Limbs) : Limbs :=
let s0 := a.1 + b.1
let s1 := a.2 + b.2 + s0 / 4
(s0 % 4 + s1 / 4, s1 % 4)
/- 9.B: the commuting square for add — your first denotation proof!
Route (both clauses of the two-clause shape):
• bounds clause: `simp only [add]` then `omega`.
• value clause: first prove the NAT identity
(add a b).1 + 4 * (add a b).2 + 15 * junk = (a.1+4*a.2)+(b.1+4*b.2)
for the right `junk` (omega finds div/mod facts by itself once you
unfold), then cast to ZMod 15 with push_cast and use that 15 = 0
on the clock: (15 : ZMod 15) = 0 is `by decide`. -/
theorem add_spec (a b : Limbs) (ha : Bnd a) (hb : Bnd b) :
((add a b).1 < 5 ∧ (add a b).2 < 4)
∧ denote (add a b) = denote a + denote b := by
sorry
/-- Multiplication, fold already applied: the column of weight 16 —
a.2*b.2 — re-enters at weight 1 because 16 ≡ 1 (mod 15).
(We return the VALUE; re-limbing it is exercise 9.D.) -/
def mulVal (a b : Limbs) : Nat :=
a.1 * b.1 + a.2 * b.2 + 4 * (a.1 * b.2 + a.2 * b.1)
/- 9.C: the fold theorem — the essence of every mul proof in this book.
Hint: the Nat identity
mulVal a b + 15 * (a.2 * b.2) = (a.1 + 4*a.2) * (b.1 + 4*b.2)
is pure algebra: `ring` proves it. Then cast as in 9.B.
Notice: NO bounds hypotheses needed — denotation doesn't care! -/
theorem mulVal_spec (a b : Limbs) :
((mulVal a b : Nat) : ZMod 15) = denote a * denote b := by
sorry
/- 9.D (paper, from the chapter): find two DISTINCT limb pairs with the
same denotation, and check by #eval that add treats them
interchangeably as far as denotation goes. -/
end Ch09

54
exercises/Ch12.lean Normal file
View file

@ -0,0 +1,54 @@
/- Chapter 12 — Graduation: spec, refusal, counterexample, fix, certificate.
The mini-system from Ch09, but one of the definitions below contains a
DELIBERATE off-by-one carry bug — exactly the species from Chapter 1:
correct on most inputs, wrong on a thin boundary slice that casual
testing misses. Requires Mathlib. -/
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.LinearCombination
namespace Ch12
abbrev Limbs := Nat × Nat
def Bnd (a : Limbs) : Prop := a.1 < 4 ∧ a.2 < 4
def denote (a : Limbs) : ZMod 15 := (a.1 : ZMod 15) + 4 * (a.2 : ZMod 15)
/-- Addition with carry… or is it? Somewhere in here hides the bug. -/
def add' (a b : Limbs) : Limbs :=
let s0 := a.1 + b.1
let s1 := a.2 + b.2 + s0 / 5
(s0 % 4 + s1 / 4, s1 % 4)
/- A few casual tests — they all pass! (Run them.) -/
#eval decide (denote (add' (1, 2) (2, 1)) = denote (1, 2) + denote (2, 1)) -- true
#eval decide (denote (add' (3, 3) (3, 3)) = denote (3, 3) + denote (3, 3)) -- true
#eval decide (denote (add' (0, 1) (1, 0)) = denote (0, 1) + denote (1, 0)) -- true
/- Task 1: state and attempt the spec. The proof below WILL get stuck —
that is the point. Push the omega/Nat-identity route from Ch09 until
Lean shows you a goal it refuses to close. READ that goal: it is
pointing at the counterexample slice. -/
theorem add'_spec (a b : Limbs) (ha : Bnd a) (hb : Bnd b) :
denote (add' a b) = denote a + denote b := by
sorry -- your attempt here. Expected outcome: honest failure.
/- Task 2: extract the counterexample. From the stuck goal, find concrete
bounded limbs where add' is WRONG, and confirm by #eval: -/
-- #eval decide (denote (add' (?, ?) (?, ?)) = denote (?, ?) + denote (?, ?))
-- -- expected: false
/- Task 3: fix the code (one character!) and prove the spec for real.
You may import your Ch09 solution mentally — it is the same proof. -/
def addFixed (a b : Limbs) : Limbs :=
sorry
theorem addFixed_spec (a b : Limbs) (ha : Bnd a) (hb : Bnd b) :
denote (addFixed a b) = denote a + denote b := by
sorry
/- Task 4 (reflection, one paragraph in a comment): the casual tests
passed and the spec failed. Explain — using the words "boundary",
"quantifier", and "thin slice" — why the spec knew better, and what
this says about the 2^-64 carry bug of Chapter 1. -/
end Ch12

18
lakefile.toml Normal file
View file

@ -0,0 +1,18 @@
name = "verifying-crypto-with-lean"
version = "0.1.0"
defaultTargets = ["Exercises", "Solutions"]
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"
rev = "5450b53e5ddc75d46418fabb605edbf36bd0beb6"
[[lean_lib]]
name = "Exercises"
srcDir = "exercises"
globs = ["Ch02", "Ch03", "Ch04", "Ch05", "Ch06", "Ch07", "Ch09", "Ch12"]
[[lean_lib]]
name = "Solutions"
srcDir = "solutions"
globs = ["Ch02", "Ch03", "Ch04", "Ch05", "Ch06", "Ch07", "Ch09", "Ch12"]

1
lean-toolchain Normal file
View file

@ -0,0 +1 @@
leanprover/lean4:v4.30.0-rc2

BIN
main.pdf Normal file
View file

Binary file not shown.

92
main.tex Normal file
View file

@ -0,0 +1,92 @@
\documentclass[11pt]{report}
\input{preamble}
\begin{document}
% ===================== TITLE PAGE =====================
\begin{titlepage}
\pagecolor{ink}\color{paper}
\begin{tikzpicture}[remember picture,overlay]
% faint pyramid motif — the proof pyramid the book builds toward
\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})$)
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}
\vspace{0.5cm}
{\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}
\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}}
\vspace{0.3cm}
{\small\color{paper} Companion to the \code{*-ed25519-verified} and \code{pasta-pallas-verified}
proof projects. \\ 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}
% ===================== HOW TO READ =====================
\chapter*{How to read this book}
\markboth{How to read this book}{}
\addcontentsline{toc}{chapter}{How to read this book}
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
does the right thing on \emph{every} input. We will aim that power at
cryptography, where a single overlooked carry bit can quietly compromise every
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.
\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.
\item \textbf{Everything runs.} The \code{exercises/} folder has Lean files you
can open and check. When the book says ``Lean accepts this,'' you can watch it
happen.
\end{itemize}
\begin{aha}
The secret this book reveals: a proof is not a wall of Greek symbols meant to
intimidate. A proof is a \emph{program} --- and a proof assistant is a very
strict compiler for it. Once you see proofs as programs, the fear evaporates and
the fun begins.
\end{aha}
\tableofcontents
% ===================== CHAPTERS =====================
\input{chapters/ch01-why-verify}
\input{chapters/ch02-meet-lean}
\input{chapters/ch03-propositions-as-types}
\input{chapters/ch04-tactics}
\input{chapters/ch05-numbers-and-automation}
\input{chapters/ch06-modular-arithmetic}
\input{chapters/ch07-primality-certificates}
\input{chapters/ch08-rust-to-lean}
\input{chapters/ch09-denotation-bridge}
\input{chapters/ch10-verifying-a-field}
\input{chapters/ch11-honesty-and-axioms}
\input{chapters/ch12-the-pyramid}
\end{document}

181
preamble.tex Normal file
View file

@ -0,0 +1,181 @@
% ============================================================================
% preamble.tex — shared style for "Verifying Cryptography with Lean 4"
% A didactic identity: warm ink on soft paper, one confident accent, and a
% small family of pedagogical boxes that each mean exactly one thing.
% ============================================================================
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=2.4cm,headsep=0.6cm]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{xcolor}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning,shapes.geometric,calc,fit,backgrounds,decorations.pathreplacing,shapes.misc}
\usepackage[most]{tcolorbox}
\usepackage{listings}
\usepackage{microtype}
\usepackage{enumitem}
\usepackage{fancyhdr}
\usepackage{titlesec}
\usepackage{booktabs}
\usepackage[strings]{underscore} % plain _ works in text; math subscripts unaffected
\usepackage{hyperref}
% ---- palette -------------------------------------------------------------
% Ink is a deep blue-slate; the accent is a warm coral used sparingly; a
% calm teal marks "things that are true / proven". Neutrals carry a faint
% blue bias so nothing reads as unconsidered grey.
\definecolor{ink}{HTML}{1C2430}
\definecolor{ink2}{HTML}{51607A}
\definecolor{paper}{HTML}{FBFAF7}
\definecolor{accent}{HTML}{E4572E} % coral — the one bold colour
\definecolor{accentsoft}{HTML}{FBE7DF}
\definecolor{proven}{HTML}{1E7F5C} % teal-green — proven / correct
\definecolor{provensoft}{HTML}{E1F1EA}
\definecolor{warn}{HTML}{B4690E} % amber — pitfalls
\definecolor{warnsoft}{HTML}{FBEFD8}
\definecolor{codebg}{HTML}{F3F1EC}
\definecolor{rule}{HTML}{DDE2E9}
\definecolor{kw}{HTML}{2B6CB0}
\definecolor{ty}{HTML}{6B46C1}
\definecolor{cmt}{HTML}{718096}
\definecolor{str}{HTML}{2F855A}
\hypersetup{colorlinks=true,linkcolor=accent,urlcolor=kw,citecolor=proven,
pdftitle={Verifying Cryptography with Lean 4},pdfauthor={Fable 5}}
% ---- page furniture ------------------------------------------------------
\pagecolor{paper}
\color{ink}
\pagestyle{fancy}\fancyhf{}
\renewcommand{\headrulewidth}{0pt}
\fancyfoot[C]{\small\color{ink2}\thepage}
% single header element: chapter title only (no number prefix), no collisions
\renewcommand{\chaptermark}[1]{\markboth{#1}{}}
\fancyhead[R]{\small\color{ink2}\scshape\leftmark}
\titleformat{\section}{\Large\bfseries\color{ink}}{\color{accent}\thesection}{0.7em}{}
\titleformat{\subsection}{\large\bfseries\color{ink}}{\color{accent}\thesubsection}{0.6em}{}
\setlength{\parskip}{0.55em}\setlength{\parindent}{0pt}
% ---- listings: Lean 4 and Rust ------------------------------------------
\lstdefinelanguage{Lean}{
morekeywords={theorem,lemma,def,example,by,intro,intros,exact,apply,rw,simp,
omega,decide,ring,constructor,rfl,have,let,fun,match,with,end,namespace,
open,import,structure,inductive,instance,class,where,do,return,if,then,else,
sorry,cases,induction,unfold,calc,show,from,at,using,Prop,Type,Nat,Int,Bool,True,False},
sensitive=true,
morecomment=[l]{--},
morecomment=[s]{/-}{-/},
morestring=[b]",
}
\lstdefinelanguage{RustL}{
morekeywords={fn,let,mut,const,pub,struct,impl,for,in,if,else,match,return,
u8,u16,u32,u64,u128,usize,i32,bool,self,Self,use,mod,where,unsafe,as},
sensitive=true,
morecomment=[l]{//},
morecomment=[s]{/*}{*/},
morestring=[b]",
}
\lstset{
% render the Unicode symbols real Lean code uses
literate={≠}{{$\neq$}}1 {∀}{{$\forall$}}1 {∃}{{$\exists$}}1
{→}{{$\to$}}1 {↔}{{$\leftrightarrow$}}1 {∧}{{$\wedge$}}1
{∨}{{$\vee$}}1 {¬}{{$\neg$}}1 {≤}{{$\leq$}}1 {≥}{{$\geq$}}1
{ℕ}{{$\mathbb{N}$}}1 {ℤ}{{$\mathbb{Z}$}}1 {ℓ}{{$\ell$}}1
{×}{{$\times$}}1 {∈}{{$\in$}}1 {∑}{{$\Sigma$}}1
{α}{{$\alpha$}}1 {β}{{$\beta$}}1 {⟨}{{$\langle$}}1 {⟩}{{$\rangle$}}1
{↦}{{$\mapsto$}}1 {⊢}{{$\vdash$}}1 {𝔽}{{$\mathbb{F}$}}1
{₀}{{$_0$}}1 {₁}{{$_1$}}1 {₂}{{$_2$}}1 {²}{{$^2$}}1 {⁵}{{$^5$}}1
{·}{{$\cdot$}}1 {←}{{$\leftarrow$}}1 {⟦}{{$[\![$}}1 {⟧}{{$]\!]$}}1
{∘}{{$\circ$}}1 {≡}{{$\equiv$}}1 {∣}{{$\mid$}}1 {⁻¹}{{$^{-1}$}}1,
basicstyle=\ttfamily\small\color{ink},
keywordstyle=\color{kw}\bfseries,
commentstyle=\color{cmt}\itshape,
stringstyle=\color{str},
numberstyle=\ttfamily\scriptsize\color{ink2},
backgroundcolor=\color{codebg},
frame=single, framerule=0pt, framesep=8pt,
rulecolor=\color{codebg},
xleftmargin=10pt, xrightmargin=6pt,
breaklines=true, showstringspaces=false,
columns=fullflexible, keepspaces=true,
aboveskip=1em, belowskip=1em,
}
% Inline code: plain styled text (robust in tables/footnotes, unlike lstinline).
% Unicode symbols in inline code are handled by the declarations below.
\newcommand{\lean}[1]{{\ttfamily\small #1}}
\newcommand{\rust}[1]{{\ttfamily\small #1}}
\newcommand{\code}[1]{{\ttfamily\small #1}}
\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}} % ⁵
% ---- pedagogical boxes: each means ONE thing ----------------------------
% BIG IDEA — the load-bearing concept of a section.
\newtcolorbox{bigidea}[1][]{enhanced,breakable,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,
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,
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,
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,
boxrule=0.6pt,arc=3pt,left=10pt,right=10pt,top=8pt,bottom=8pt,
fonttitle=\bfseries\color{paper},coltitle=paper,title={\faFlagCheckered\ Checkpoint},#1}
% Poor-man's icons (fontawesome may be absent): draw tiny glyphs with text.
\providecommand{\faLightbulb}{\raisebox{-1pt}{\small$\ast$}}
\providecommand{\faTerminal}{\raisebox{-1pt}{\small\ttfamily>\_}}
\providecommand{\faExclamationTriangle}{\raisebox{-1pt}{\small$\triangle$}}
\providecommand{\faStar}{\raisebox{-1pt}{\small$\star$}}
\providecommand{\faFlagCheckered}{\raisebox{-1pt}{\small$\bowtie$}}
% ---- math shortcuts the whole book uses ---------------------------------
\newcommand{\F}{\mathbb{F}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Fp}{\mathbb{F}_p}
\newcommand{\Zmod}[1]{\mathbb{Z}/#1\mathbb{Z}}
% double-bracket "denotation" delimiters without stmaryrd
\newcommand{\denote}[1]{\ensuremath{[\mkern-3.3mu[ #1 ]\mkern-3.3mu]}}
% exercises
\newcounter{exc}[section]
\newcommand{\exercise}[1]{\refstepcounter{exc}\smallskip\noindent%
{\bfseries\color{accent}Exercise \thechapter.\theexc.}\ #1\smallskip}

45
solutions/Ch02.lean Normal file
View file

@ -0,0 +1,45 @@
/- Chapter 2 — solutions. Every definition compiles with no sorry. -/
namespace Ch02
def p : Nat := 2 ^ 255 - 19
def double (n : Nat) : Nat := 2 * n
-- Exercise A: multiplication bootstrapped from addition.
def mul : Nat → Nat → Nat
| _, Nat.zero => 0
| m, Nat.succ n => mul m n + m
#eval mul 6 7 -- 42
#eval mul 0 9 -- 0
-- Exercise 2.1
def pow : Nat → Nat → Nat
| _, Nat.zero => 1
| b, Nat.succ e => pow b e * b
#eval pow 2 10 -- 1024
-- Exercise 2.2
def fib : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => fib (n + 1) + fib n
#eval fib 10 -- 55
/- Exercise 2.3. The type cannot enforce `den ≠ 0`: a value ⟨1, 0⟩ is
perfectly constructible. Chapter 3's dependent structures fix this by
storing a proof `den ≠ 0` inside the value. -/
structure Rational where
num : Int
den : Nat
def Rational.add (x y : Rational) : Rational :=
⟨x.num * y.den + y.num * x.den, x.den * y.den⟩
#eval (Rational.add ⟨1, 2⟩ ⟨1, 3⟩).num -- 5
#eval (Rational.add ⟨1, 2⟩ ⟨1, 3⟩).den -- 6
end Ch02

29
solutions/Ch03.lean Normal file
View file

@ -0,0 +1,29 @@
/- Chapter 3 — solutions. Term mode only, as required. -/
namespace Ch03
variable (P Q R : Prop)
theorem const_imp : P → Q → P :=
fun p _ => p
theorem and_to_or : P ∧ Q → P ∨ Q :=
fun h => Or.inl h.1
theorem modus_ponens : P → (P → Q) → Q :=
fun p f => f p
theorem and_assoc' : (P ∧ Q) ∧ R → P ∧ (Q ∧ R) :=
fun h => And.intro h.1.1 (And.intro h.1.2 h.2)
theorem or_swap : P ∨ Q → Q ∨ P :=
fun h => match h with
| Or.inl p => Or.inr p
| Or.inr q => Or.inl q
/- The program: "given evidence p for P and a refuter f of P, feed p to f."
A proof of ¬¬P is a function that defeats any would-be refutation. -/
theorem not_not_intro : P → ¬¬P :=
fun p f => f p
end Ch03

46
solutions/Ch04.lean Normal file
View file

@ -0,0 +1,46 @@
/- Chapter 4 — solutions. -/
namespace Ch04
def myAdd : Nat → Nat → Nat
| m, Nat.zero => m
| m, Nat.succ n => Nat.succ (myAdd m n)
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := by
intro h
constructor
· exact h.2
· exact h.1
theorem zero_myAdd (n : Nat) : myAdd 0 n = n := by
induction n with
| zero => rfl
| succ k ih =>
simp only [myAdd]
rw [ih]
theorem succ_myAdd (m n : Nat) : myAdd (Nat.succ m) n = Nat.succ (myAdd m n) := by
induction n with
| zero => rfl
| succ k ih =>
simp only [myAdd]
rw [ih]
/- zero case: "m + 0 is m by definition, and 0 + m is m by 4.1a."
succ case: "both sides step to a successor — the left by definition,
the right by 4.1b — and the induction hypothesis matches the insides." -/
theorem myAdd_comm (m n : Nat) : myAdd m n = myAdd n m := by
induction n with
| zero => simp only [myAdd]; rw [zero_myAdd]
| succ k ih =>
simp only [myAdd]
rw [succ_myAdd, ih]
/- 4.3: the wrong step was the last one: 4*b + b is 5*b, not 6*b. -/
theorem calc_repair (a b : Nat) (h : a = 2 * b) : a + a + b = 5 * b := by
calc a + a + b = 2 * a + b := by omega
_ = 2 * (2 * b) + b := by rw [h]
_ = 4 * b + b := by omega
_ = 5 * b := by omega
end Ch04

49
solutions/Ch05.lean Normal file
View file

@ -0,0 +1,49 @@
/- Chapter 5 — solutions: each goal, its one right tool. -/
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum
import Mathlib.Data.Nat.Prime.Basic
namespace Ch05
-- G1: linear bounds → omega.
example (a b : Nat) (h1 : a < 2^51) (h2 : b < 2^51) : a + b < 2^52 := by
omega
-- G2: truncated subtraction → omega (it models Nat subtraction natively).
example (a b : Nat) (h : a ≤ b) : a + (b - a) = b := by
omega
-- G3: commutative-ring identity → ring.
example (a b : Int) : (a + b) * (a - b) = a * a - b * b := by
ring
-- G4: concrete numerals → norm_num.
example : (2:Int)^255 - 19 > 2^254 := by
norm_num
-- G5: small finite check → decide.
example : Nat.Prime 97 := by
decide
-- G6: linear (constant coefficient) → omega.
example (x : Nat) (h : 3 * x + 7 ≤ 100) : x ≤ 31 := by
omega
-- G7: numerals → norm_num.
example : 2^51 + 2^51 = 2^52 := by
norm_num
-- G8: ring.
example (x y : Int) : (x + y)^3 = x^3 + 3*x^2*y + 3*x*y^2 + y^3 := by
ring
-- G9: the two-step pattern — bound the nonlinear atom, then omega.
example (a b : Nat) (ha : a < 100) (hb : b < 100) : a * b < 10000 := by
have hab : a * b < 100 * 100 := Nat.mul_lt_mul'' ha hb
omega
-- G10: multiplication by the CONSTANT 19 is linear → omega.
example (a : Nat) (h : a < 2^51) : a * 19 < 2^56 := by
omega
end Ch05

50
solutions/Ch06.lean Normal file
View file

@ -0,0 +1,50 @@
/- Chapter 6 — solutions. -/
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum
import Mathlib.FieldTheory.Finite.Basic
namespace Ch06
#eval (7 + 8 : ZMod 12) -- 3
#eval (3 - 7 : ZMod 12) -- 8
#eval (3⁻¹ : ZMod 7) -- 5 (3 * 5 = 15 = 1 mod 7)
#eval (4⁻¹ : ZMod 11) -- 3
#eval (4⁻¹ : ZMod 12) -- 1 (!) no inverse exists, so Lean returns a
-- JUNK value (here 1 — and 4 * 1 ≠ 1, check!).
-- Junk from total functions is exactly why
-- theorems carry hypotheses.
-- 6.A: a ring identity — the modulus is irrelevant.
example (x y : ZMod 7) :
(x + y)^3 = x^3 + 3*x^2*y + 3*x*y^2 + y^3 := by
ring
-- 6.B: finite world, decide.
example : ∀ x : ZMod 12, 4 * x ≠ 1 := by
decide
/- 6.C: mod 13 the statement is false: 4 * 10 = 40 = 3*13 + 1, so 4⁻¹ = 10.
`decide` fails (correctly) because it finds the counterexample x = 10. -/
#eval (4⁻¹ : ZMod 13) -- 10
-- Mathlib's Fermat lemma needs to KNOW 11 is prime — as a typeclass
-- fact. This is how you register arithmetic facts for instance search:
instance : Fact (Nat.Prime 11) := ⟨by decide⟩
-- 6.D: Fermat's little theorem, instantiated at p = 11.
example (a : ZMod 11) (h : a ≠ 0) : a^10 = 1 := by
have := ZMod.pow_card_sub_one_eq_one h
simpa using this
-- 6.E: the reduction identity behind every curve25519 codebase.
def p : Nat := 2^255 - 19
example : (2^255 : ZMod p) = 19 := by
have h : ((p : Nat) : ZMod p) = 0 := ZMod.natCast_self p
have hp : (2^255 : ZMod p) = ((p : Nat) : ZMod p) + 19 := by
have : (p : Nat) + 19 = 2^255 := by norm_num [p]
norm_cast
rw [hp, h, zero_add]
end Ch06

50
solutions/Ch07.lean Normal file
View file

@ -0,0 +1,50 @@
/- Chapter 7 — solutions. -/
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.NormNum.Prime
namespace Ch07
-- 7.A: small enough for kernel trial division.
example : Nat.Prime 97 := by
decide
-- 7.B: norm_num's certificate route — instant where decide crawls.
example : Nat.Prime 65537 := by
norm_num
-- 7.C: certificate or nothing at ten digits. One wrinkle worth knowing:
-- norm_num's prime extension wants a LITERAL, so first change the goal to
-- the (definitionally equal) evaluated numeral with `show`.
example : Nat.Prime (2^31 - 1) := by
show Nat.Prime 2147483647
norm_num
/- 7.D: Pratt witness for p = 13, w = 2. Hand computation:
2^12 = 4096 = 315*13 + 1 → 1 ✓ (first condition)
2^6 = 64 = 4*13 + 12 → 12 ✓ (≠ 1, q = 2)
2^4 = 16 = 13 + 3 → 3 ✓ (≠ 1, q = 3) -/
#eval (2:ZMod 13)^12 -- 1
#eval (2:ZMod 13)^6 -- 12 (not 1)
#eval (2:ZMod 13)^4 -- 3 (not 1)
-- 7.E: square-and-multiply.
def powModAux : Nat → Nat → Nat → Nat → Nat → Nat
| 0, _, _, _, acc => acc
| fuel+1, b, e, m, acc =>
if e = 0 then acc
else powModAux fuel (b*b % m) (e/2) m (if e % 2 = 1 then acc*b % m else acc)
def powMod (b e m : Nat) : Nat :=
if m ≤ 1 then 0 else powModAux 300 (b % m) e m 1
#eval powMod 2 12 13 -- 1
#eval powMod 3 4 7 -- 4
/- Fermat's little theorem in action at 77 digits: the answer is 1, in
milliseconds — this is why certificate CHECKING is cheap. (One node of
the witness tree; the full kernel-checked certificate for the Pallas
modulus lives in pasta-pallas-verified.) -/
def p : Nat := 2^255 - 19
#eval powMod 2 (p - 1) p -- 1
end Ch07

68
solutions/Ch09.lean Normal file
View file

@ -0,0 +1,68 @@
/- Chapter 9 — solutions. -/
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.LinearCombination
namespace Ch09
abbrev Limbs := Nat × Nat
def Bnd (a : Limbs) : Prop := a.1 < 4 ∧ a.2 < 4
-- 9.A: positional notation, base 4, on the clock face of ZMod 15.
def denote (a : Limbs) : ZMod 15 := (a.1 : ZMod 15) + 4 * (a.2 : ZMod 15)
#eval denote (3, 2) -- 11
#eval denote (1, 0) -- 1
def add (a b : Limbs) : Limbs :=
let s0 := a.1 + b.1
let s1 := a.2 + b.2 + s0 / 4
(s0 % 4 + s1 / 4, s1 % 4)
-- 9.B: the commuting square for add.
theorem add_spec (a b : Limbs) (ha : Bnd a) (hb : Bnd b) :
((add a b).1 < 5 ∧ (add a b).2 < 4)
∧ denote (add a b) = denote a + denote b := by
obtain ⟨ha1, ha2⟩ := ha
obtain ⟨hb1, hb2⟩ := hb
constructor
· -- bounds clause: pure integer bookkeeping.
simp only [add]
omega
· -- value clause: Nat identity first, then cast to the clock face.
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) := by
simp only [add]
omega
have := congrArg (fun n : Nat => (n : ZMod 15)) key
push_cast at this
rw [show (15 : ZMod 15) = 0 by decide] at this
simp only [zero_mul, add_zero] at this
simp only [denote]
linear_combination this
def mulVal (a b : Limbs) : Nat :=
a.1 * b.1 + a.2 * b.2 + 4 * (a.1 * b.2 + a.2 * b.1)
-- 9.C: the fold theorem — no bounds hypotheses needed.
theorem mulVal_spec (a b : Limbs) :
((mulVal a b : Nat) : ZMod 15) = denote a * denote b := by
have key : mulVal a b + 15 * (a.2 * b.2)
= (a.1 + 4 * a.2) * (b.1 + 4 * b.2) := by
simp only [mulVal]
ring
have := congrArg (fun n : Nat => (n : ZMod 15)) key
push_cast at this
rw [show (15 : ZMod 15) = 0 by decide] at this
simp only [zero_mul, add_zero] at this
simp only [denote]
linear_combination this
/- 9.D: (19,…) has no meaning here, but e.g. denote (3, 3) = 3 + 12 = 15 = 0
and denote (0, 0) = 0 — a collision. Check interchangeability: -/
#eval denote (add (3, 3) (1, 2)) -- 9
#eval denote (add (0, 0) (1, 2)) -- 9 — same, as denotation demands
end Ch09

69
solutions/Ch12.lean Normal file
View file

@ -0,0 +1,69 @@
/- Chapter 12 — solutions: the full arc. -/
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.LinearCombination
namespace Ch12
abbrev Limbs := Nat × Nat
def Bnd (a : Limbs) : Prop := a.1 < 4 ∧ a.2 < 4
def denote (a : Limbs) : ZMod 15 := (a.1 : ZMod 15) + 4 * (a.2 : ZMod 15)
def add' (a b : Limbs) : Limbs :=
let s0 := a.1 + b.1
let s1 := a.2 + b.2 + s0 / 5 -- ← the bug: carry threshold 5, not 4
(s0 % 4 + s1 / 4, s1 % 4)
/- Task 1: the attempt gets stuck because the Nat identity that closed
Ch09's proof is FALSE for add': omega refuses
(add' a b).1 + 4*(add' a b).2 + 15*junk = (a.1+4*a.2)+(b.1+4*b.2)
and its failure is concentrated where s0/5 ≠ s0/4 — that is,
a.1 + b.1 = 4 exactly (within our bounds, s0 ≤ 6, and 4 is the only
value where the two divisions disagree: 4/4 = 1 but 4/5 = 0).
The carry is simply DROPPED on that slice. -/
/- Task 2: the counterexample the stuck goal points at. -/
#eval decide (denote (add' (2, 0) (2, 0)) = denote (2, 0) + denote (2, 0))
-- false: add' (2,0) (2,0) = (0,0) — the dropped carry lost the value 4.
#eval denote (add' (2, 0) (2, 0)) -- 0 (wrong)
#eval denote (2, 0) + denote (2, 0) -- 4 (truth)
/- Note how thin the slice is: of the 256 bounded input pairs, exactly
the ones with a.1 + b.1 = 4 misbehave — none of which appeared in the
casual tests. This is the 2^-64 carry bug of Chapter 1, at toy scale. -/
/- Task 3: the one-character fix, and the proof from Ch09 goes through
verbatim — the certificate exists again because the code is right. -/
def addFixed (a b : Limbs) : Limbs :=
let s0 := a.1 + b.1
let s1 := a.2 + b.2 + s0 / 4 -- carry threshold restored
(s0 % 4 + s1 / 4, s1 % 4)
theorem addFixed_spec (a b : Limbs) (ha : Bnd a) (hb : Bnd b) :
denote (addFixed a b) = denote a + denote b := by
obtain ⟨ha1, ha2⟩ := ha
obtain ⟨hb1, hb2⟩ := hb
have key : (addFixed a b).1 + 4 * (addFixed a b).2
+ 15 * ((a.2 + b.2 + (a.1 + b.1) / 4) / 4)
= (a.1 + 4 * a.2) + (b.1 + 4 * b.2) := by
simp only [addFixed]
omega
have := congrArg (fun n : Nat => (n : ZMod 15)) key
push_cast at this
rw [show (15 : ZMod 15) = 0 by decide] at this
simp only [zero_mul, add_zero] at this
simp only [denote]
linear_combination this
/- Task 4 (reflection): The casual tests sampled comfortable interior
points; the bug lives on the BOUNDARY of the carry condition — the
THIN SLICE where a.1 + b.1 equals exactly 4. A test suite touches
finitely many points and missed the slice entirely; the spec's
universal QUANTIFIER covers the slice by construction, so the proof
had to fail — and its failure pointed straight at the guilty inputs.
Chapter 1's 2^-64 carry bug is this same story with a slice so thin
that random testing would need centuries to land on it. The
quantifier does not get luckier or unluckier; it just covers
everything. That is the entire value proposition of this book. -/
end Ch12