verifying-crypto-with-lean/main.tex

\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}

\subsection*{Working the pen-and-paper material}

The notebook-ruled \emph{Pen and paper} boxes are not optional
enrichment; they are half the course. Each one performs a computation
with the \emph{real} constants of the systems under study ---
$2^{255}-19$, radix $2^{51}$, the fold constant $19$, the actual
inversion chain --- because the numbers themselves carry the arguments:
a headroom margin of $17$ bits, a design constant that fails at $8$ and
works at $16$, a certificate that beats trial division by a factor of
$10^{34}$. Copy each one out by hand at least once --- transcription is
where the steps become yours. Every chapter's exercises are followed
immediately by \emph{Solutions and pathways}: the pathway (how a person
finds the answer) before the answer, because the pathway is the
transferable part. The honest protocol: attempt, struggle a little,
then read --- in that order.

\subsection*{For instructors}

The book is engineered for self-study, which makes it easy to teach
from: every exercise carries an immediate pathway-then-answer solution,
so contact hours can go to the parts that need a human --- discussing
the discussion exercises (each chapter has one; they are the seminar
seeds), pair-debugging the Lean files, and auditing real repositories
together (Appendix~\ref{app:tour} is a ready-made lab session). Grading
suggestion: collect the pen-and-paper worked examples \emph{reproduced
from memory} rather than problem sets --- the book's bet is that a
student who can re-derive the $16p$ audit or the certificate cost
ledger unprompted has the durable skill, and that bet is testable. The
Lean solution files compile against the pinned toolchain in the repo;
\code{lake build Solutions} is your answer key's answer key. Prerequisites
in practice: one programming course (any language) and comfort with
high-school algebra; no number theory, no logic, no Rust. The
thirteen-week plan below has been paced so the two hard climbs ---
Chapter~9 and the Interlude --- each get a full week with nothing else
competing.

\subsection*{A thirteen-week plan}

For self-study or a seminar, the book paces naturally as a semester:

\begin{center}
\small
\begin{tabular}{@{}lll@{}}
\toprule
\textbf{Weeks} & \textbf{Material} & \textbf{Deliverable} \\
\midrule
1     & Ch.~1 + toolkit Cards 1--2       & the two Ch.~1 audits, by hand \\
2--3  & Ch.~2--3 + \code{Ch02/Ch03.lean} & term-mode proof portfolio \\
4     & Ch.~4 + \code{Ch04.lean}         & the \code{zero\_add} board trace, from memory \\
5     & Ch.~5 + \code{Ch05.lean}         & ten goals, right tool each \\
6     & Ch.~6 + \code{Ch06.lean}         & the Euclid inversion, reproduced \\
7     & Ch.~7 + \code{Ch07.lean}         & hand-checked certificate for 97 \\
8     & Ch.~8 + repo reading (App.~C)    & annotated extract of \code{gen/} \\
9     & Ch.~9 + \code{Ch09.lean}         & the miniature bridge, proved \\
10    & Interlude                        & the complete by-hand verification \\
11    & Ch.~10--11                       & audit drill on a stranger's repo \\
12    & Ch.~12 + \code{Ch12.lean}        & graduation: spec--refusal--fix--certificate \\
13    & project                          & one open lemma or one solo bridge \\
\bottomrule
\end{tabular}
\end{center}

\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/interlude-by-hand}
\input{chapters/ch10-verifying-a-field}
\input{chapters/ch11-honesty-and-axioms}
\input{chapters/ch12-the-pyramid}

\appendix
\input{chapters/appendix-toolkit}
\input{chapters/appendix-walkthroughs}
\input{chapters/appendix-repo-tour}
\input{chapters/glossary}

\end{document}