commit 45048d48985f85707bbe9c77f476fba2735a41eb Author: saymrwulf Date: Fri Jul 3 09:44:40 2026 +0200 Verifying Cryptography with Lean 4: complete 12-chapter curriculum - 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 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..7d56dc0 --- /dev/null +++ b/.gitignore @@ -0,0 +1,10 @@ +*.aux +build/ +build2.log +build.log +.lake/ +lake-manifest.json +*.log +*.olean +*.out +*.toc diff --git a/README.md b/README.md new file mode 100644 index 0000000..2d7cabc --- /dev/null +++ b/README.md @@ -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). diff --git a/chapters/ch01-why-verify.tex b/chapters/ch01-why-verify.tex new file mode 100644 index 0000000..9b9b895 --- /dev/null +++ b/chapters/ch01-why-verify.tex @@ -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} diff --git a/chapters/ch02-meet-lean.tex b/chapters/ch02-meet-lean.tex new file mode 100644 index 0000000..fc49c85 --- /dev/null +++ b/chapters/ch02-meet-lean.tex @@ -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} diff --git a/chapters/ch03-propositions-as-types.tex b/chapters/ch03-propositions-as-types.tex new file mode 100644 index 0000000..9a1f4fc --- /dev/null +++ b/chapters/ch03-propositions-as-types.tex @@ -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} diff --git a/chapters/ch04-tactics.tex b/chapters/ch04-tactics.tex new file mode 100644 index 0000000..257a4ec --- /dev/null +++ b/chapters/ch04-tactics.tex @@ -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} diff --git a/chapters/ch05-numbers-and-automation.tex b/chapters/ch05-numbers-and-automation.tex new file mode 100644 index 0000000..e2641c8 --- /dev/null +++ b/chapters/ch05-numbers-and-automation.tex @@ -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} diff --git a/chapters/ch06-modular-arithmetic.tex b/chapters/ch06-modular-arithmetic.tex new file mode 100644 index 0000000..9bd7abc --- /dev/null +++ b/chapters/ch06-modular-arithmetic.tex @@ -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} diff --git a/chapters/ch07-primality-certificates.tex b/chapters/ch07-primality-certificates.tex new file mode 100644 index 0000000..b879e06 --- /dev/null +++ b/chapters/ch07-primality-certificates.tex @@ -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} diff --git a/chapters/ch08-rust-to-lean.tex b/chapters/ch08-rust-to-lean.tex new file mode 100644 index 0000000..566cac2 --- /dev/null +++ b/chapters/ch08-rust-to-lean.tex @@ -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} diff --git a/chapters/ch09-denotation-bridge.tex b/chapters/ch09-denotation-bridge.tex new file mode 100644 index 0000000..31ffc83 --- /dev/null +++ b/chapters/ch09-denotation-bridge.tex @@ -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} diff --git a/chapters/ch10-verifying-a-field.tex b/chapters/ch10-verifying-a-field.tex new file mode 100644 index 0000000..8ec1a10 --- /dev/null +++ b/chapters/ch10-verifying-a-field.tex @@ -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} diff --git a/chapters/ch11-honesty-and-axioms.tex b/chapters/ch11-honesty-and-axioms.tex new file mode 100644 index 0000000..7fd5177 --- /dev/null +++ b/chapters/ch11-honesty-and-axioms.tex @@ -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} diff --git a/chapters/ch12-the-pyramid.tex b/chapters/ch12-the-pyramid.tex new file mode 100644 index 0000000..caf2e75 --- /dev/null +++ b/chapters/ch12-the-pyramid.tex @@ -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} diff --git a/exercises/Ch02.lean b/exercises/Ch02.lean new file mode 100644 index 0000000..fe8fc65 --- /dev/null +++ b/exercises/Ch02.lean @@ -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 diff --git a/exercises/Ch03.lean b/exercises/Ch03.lean new file mode 100644 index 0000000..9b31240 --- /dev/null +++ b/exercises/Ch03.lean @@ -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 diff --git a/exercises/Ch04.lean b/exercises/Ch04.lean new file mode 100644 index 0000000..3558032 --- /dev/null +++ b/exercises/Ch04.lean @@ -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 diff --git a/exercises/Ch05.lean b/exercises/Ch05.lean new file mode 100644 index 0000000..ae18ac6 --- /dev/null +++ b/exercises/Ch05.lean @@ -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 diff --git a/exercises/Ch06.lean b/exercises/Ch06.lean new file mode 100644 index 0000000..fda9e58 --- /dev/null +++ b/exercises/Ch06.lean @@ -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 diff --git a/exercises/Ch07.lean b/exercises/Ch07.lean new file mode 100644 index 0000000..957ae4f --- /dev/null +++ b/exercises/Ch07.lean @@ -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 diff --git a/exercises/Ch09.lean b/exercises/Ch09.lean new file mode 100644 index 0000000..00531bf --- /dev/null +++ b/exercises/Ch09.lean @@ -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 diff --git a/exercises/Ch12.lean b/exercises/Ch12.lean new file mode 100644 index 0000000..d334c3e --- /dev/null +++ b/exercises/Ch12.lean @@ -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 diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..658dfc6 --- /dev/null +++ b/lakefile.toml @@ -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"] diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..6c7e31f --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.30.0-rc2 diff --git a/main.pdf b/main.pdf new file mode 100644 index 0000000..0b59ed5 Binary files /dev/null and b/main.pdf differ diff --git a/main.tex b/main.tex new file mode 100644 index 0000000..df22bec --- /dev/null +++ b/main.tex @@ -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} diff --git a/preamble.tex b/preamble.tex new file mode 100644 index 0000000..064de6e --- /dev/null +++ b/preamble.tex @@ -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} diff --git a/solutions/Ch02.lean b/solutions/Ch02.lean new file mode 100644 index 0000000..b4fe9e6 --- /dev/null +++ b/solutions/Ch02.lean @@ -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 diff --git a/solutions/Ch03.lean b/solutions/Ch03.lean new file mode 100644 index 0000000..b746536 --- /dev/null +++ b/solutions/Ch03.lean @@ -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 diff --git a/solutions/Ch04.lean b/solutions/Ch04.lean new file mode 100644 index 0000000..363d909 --- /dev/null +++ b/solutions/Ch04.lean @@ -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 diff --git a/solutions/Ch05.lean b/solutions/Ch05.lean new file mode 100644 index 0000000..8ce991c --- /dev/null +++ b/solutions/Ch05.lean @@ -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 diff --git a/solutions/Ch06.lean b/solutions/Ch06.lean new file mode 100644 index 0000000..cfce60a --- /dev/null +++ b/solutions/Ch06.lean @@ -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 diff --git a/solutions/Ch07.lean b/solutions/Ch07.lean new file mode 100644 index 0000000..126d65e --- /dev/null +++ b/solutions/Ch07.lean @@ -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 diff --git a/solutions/Ch09.lean b/solutions/Ch09.lean new file mode 100644 index 0000000..20be599 --- /dev/null +++ b/solutions/Ch09.lean @@ -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 diff --git a/solutions/Ch12.lean b/solutions/Ch12.lean new file mode 100644 index 0000000..9b2cf2c --- /dev/null +++ b/solutions/Ch12.lean @@ -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