diff --git a/README.md b/README.md index ab2c102..6b95de6 100644 --- a/README.md +++ b/README.md @@ -25,7 +25,7 @@ Lean 4 against models extracted from the actual Rust sources: **[`main.pdf`](main.pdf)** — fourteen chapters + interlude + three appendices, full color, built with LaTeX/TikZ from the sources in this repo (`./build.sh`, tectonic, no root needed). **Second edition, -published August 8, 2026** (129 pages; the full publication history is +published August 8, 2026** (132 pages; the full publication history is printed in the book's front matter). No prior Lean or formal methods assumed; high-school algebra and a little programming suffice. diff --git a/chapters/appendix-repo-tour.tex b/chapters/appendix-repo-tour.tex index d2d2763..1bb5457 100644 --- a/chapters/appendix-repo-tour.tex +++ b/chapters/appendix-repo-tour.tex @@ -108,7 +108,7 @@ phase catches it and what the failure actually says. Then try to be sneakier: weaken a theorem's \emph{statement} instead of its proof, or plant an \lean{axiom} in a \code{Proofs/} file, and see the stub-audit phase refuse before the compiler even starts. Restore with -\code{git checkout -- .} when done. Ten minutes of vandalism buys you +\code{git checkout \ddash\ .} when done. Ten minutes of vandalism buys you something reading cannot: the difference between believing the button because it is green and believing it because you have personally failed to fool it. diff --git a/chapters/appendix-toolkit.tex b/chapters/appendix-toolkit.tex index aa8c265..1b9eb50 100644 --- a/chapters/appendix-toolkit.tex +++ b/chapters/appendix-toolkit.tex @@ -91,12 +91,12 @@ which is itself a toolkit skill. \section{Card 6: the headroom audit} For any limb design, three lines locate the overflow cliff: -\[ -\text{headroom} = \text{word bits} - \text{radix bits}; \qquad -\text{add budget} = 2^{\text{headroom}}; \qquad -\text{mul check: } (\text{limb count}) \cdot 2^{2\cdot\text{bound bits}} +\begin{align*} +\text{headroom} &= \text{word bits} - \text{radix bits};\\ +\text{add budget} &= 2^{\text{headroom}};\\ +\text{mul check: } &(\text{limb count}) \cdot 2^{2\cdot\text{bound bits}} \overset{?}{<} 2^{\text{wide word}} . -\] +\end{align*} Run all three whenever anyone shows you a limb representation --- Chapter~\ref{ch:why} (budget), Chapter~\ref{ch:automation} (mul check), and Chapter~\ref{ch:field}'s $16p$ audit are all instances. diff --git a/chapters/appendix-walkthroughs.tex b/chapters/appendix-walkthroughs.tex index 4deeebf..66884fc 100644 --- a/chapters/appendix-walkthroughs.tex +++ b/chapters/appendix-walkthroughs.tex @@ -140,8 +140,12 @@ addition must happen \emph{on the clock face}, not in \lean{Nat}). this proof on paper. Bounds clause: \lean{simp only [add]; omega}. Value clause --- the one genuine difficulty in the file --- state the exact integer identity with its correction term: -\lean{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)}, discharge with +\begin{lstlisting}[language=Lean] +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) +\end{lstlisting} +discharge it with \lean{simp only [add]; omega}, then cast (\lean{push_cast}), kill the modulus (\lean{rw [show (15 : ZMod 15) = 0 by decide]}), and close with @@ -149,9 +153,9 @@ exact integer identity with its correction term: correction term is wrong --- recompute $c_2$ on paper (Interlude Step 2); \lean{omega}'s refusal is, as always, a counterexample pointing at the boundary. \textbf{9.C \code{mulVal_spec}}: same cast-and-kill -scaffold, but the integer identity is pure algebra --- -\lean{mulVal a b + 15 * (a.2 * b.2) = (a.1 + 4*a.2) * (b.1 + 4*b.2)} -by \lean{ring} --- and \emph{no bounds hypotheses are needed}, a fact +scaffold, but the integer identity is pure algebra, +\lean{mulVal a b + 15*(a.2*b.2) = (a.1 + 4*a.2)*(b.1 + 4*b.2)} +by \lean{ring}, and \emph{no bounds hypotheses are needed} --- a fact worth noticing (denotation does not care about digit discipline; only machine words do). diff --git a/chapters/ch03-propositions-as-types.tex b/chapters/ch03-propositions-as-types.tex index 0fe1fbb..23df06d 100644 --- a/chapters/ch03-propositions-as-types.tex +++ b/chapters/ch03-propositions-as-types.tex @@ -35,8 +35,8 @@ Chapter~\ref{ch:lean} \emph{is} the proof checker. 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} \\ +$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} \\ @@ -246,8 +246,9 @@ structure of $n$, induction (Chapter~\ref{ch:tactics}) is how a recipe consults structure. \end{worked} -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 +Dually, \lean{exists n, P n} is proved by handing over a concrete +witness together with the evidence for it: \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: @@ -279,17 +280,17 @@ 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 -> 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 +\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 +\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 diff --git a/chapters/ch04-tactics.tex b/chapters/ch04-tactics.tex index a6d5e7e..276cd50 100644 --- a/chapters/ch04-tactics.tex +++ b/chapters/ch04-tactics.tex @@ -377,8 +377,9 @@ theorem two_mul' (n : Nat) : 2 * n = n + n := by | zero => rfl | succ k ih => rw [Nat.mul_succ, ih, Nat.succ_add, Nat.add_succ] \end{lstlisting} -Library: \lean{exact?} finds \lean{Nat.two_mul}, so -\lean{theorem two_mul'' (n : Nat) : 2 * n = n + n := Nat.two_mul n}. Both +Library: \lean{exact?} finds \lean{Nat.two_mul}, giving +\lean{theorem two_mul\textquotesingle\textquotesingle\ (n : Nat) : 2 * n = n + n} +proved by \lean{Nat.two_mul n}. Both are legitimate craft: the first when you are building the ecosystem, the second when you are using it. Mathlib has over 200{,}000 lemmas --- searching \emph{is} a proof technique, and \lean{exact?} is its tactic. diff --git a/chapters/ch06-modular-arithmetic.tex b/chapters/ch06-modular-arithmetic.tex index 95e6c3e..7bf34d6 100644 --- a/chapters/ch06-modular-arithmetic.tex +++ b/chapters/ch06-modular-arithmetic.tex @@ -67,7 +67,7 @@ is the entry ticket to division. \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} + \foreach \s/\t in {0/4, 4/8, 8/12} \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} @@ -75,7 +75,7 @@ is the entry ticket to division. \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} + \foreach \s/\t in {0/4, 4/8, 8/12} \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} diff --git a/chapters/ch08-rust-to-lean.tex b/chapters/ch08-rust-to-lean.tex index f6e88b2..158fc31 100644 --- a/chapters/ch08-rust-to-lean.tex +++ b/chapters/ch08-rust-to-lean.tex @@ -103,11 +103,13 @@ 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}: +\noindent\begin{minipage}{\linewidth} \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} +\end{minipage} That hypothesis \lean{LimbsBounded} --- each limb below $2^{54}$, say --- is the bounds invariant promised in Chapters~\ref{ch:pat} diff --git a/chapters/ch09-denotation-bridge.tex b/chapters/ch09-denotation-bridge.tex index 71bd8a9..afeebf6 100644 --- a/chapters/ch09-denotation-bridge.tex +++ b/chapters/ch09-denotation-bridge.tex @@ -69,7 +69,7 @@ diagram, instantiated. \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 +arrays $(19, 0, 0, 0, 0)$ and $(19 + (2^{51}-19),\; 2^{51}-1,\; \dots)$ --- i.e.\ $p$ itself added limb-wise --- --- 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 diff --git a/chapters/ch10-verifying-a-field.tex b/chapters/ch10-verifying-a-field.tex index fe951a4..0dd7b8a 100644 --- a/chapters/ch10-verifying-a-field.tex +++ b/chapters/ch10-verifying-a-field.tex @@ -237,7 +237,8 @@ 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 +\Needspace{4\baselineskip} +\noindent\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 diff --git a/chapters/ch12-the-pyramid.tex b/chapters/ch12-the-pyramid.tex index 34a0002..2ac3bf9 100644 --- a/chapters/ch12-the-pyramid.tex +++ b/chapters/ch12-the-pyramid.tex @@ -63,7 +63,8 @@ Then \[ x_3 \;=\; \frac{2xy}{1 + 11} \;=\; \frac{16}{12} \;\equiv\; 3 \cdot 12^{-1} \;=\; 3\cdot 12 \;=\; 36 \;\equiv\; 10, -\qquad +\] +\[ y_3 \;=\; \frac{y^2\!+\!x^2}{1 - 11} \;=\; \frac{20}{3} \;\equiv\; 7\cdot 3^{-1} \;=\; 7 \cdot 9 \;=\; 63 \;\equiv\; 11 \] @@ -75,10 +76,10 @@ want it. \emph{Run 2 --- the real base point, full digits.} The same doubling, on Ed25519's base point $B = (x_1, y_1)$: -\par\noindent{\footnotesize $x_1 \;=$}\\[-2pt] +\par\noindent{\footnotesize $x_1 \;=$}\\[1pt] {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}15\,11222\,13495\,35400\,77250\,11514\,09588\,53151\,14540\\ 12693\,04185\,72060\,46113\,28394\,98477\,62202\end{tabular}}\par\smallskip -\par\noindent{\footnotesize $y_1 \;=$}\\[-2pt] +\par\noindent{\footnotesize $y_1 \;=$}\\[1pt] {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}46\,31683\,56949\,26478\,16942\,83940\,03475\,16314\,13079\\ 93866\,25622\,56157\,83033\,60316\,52518\,55960\end{tabular}}\par\smallskip The machine's first step is the product $u = x_1 y_1 \bmod p$. Nobody @@ -88,10 +89,10 @@ remainder $u$ it claims, turning the step into one integer equation \[ x_1 \cdot y_1 \;=\; q \cdot p + u , \] -\par\noindent{\footnotesize $q \;=$}\\[-2pt] +\par\noindent{\footnotesize $q \;=$}\\[1pt] {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}12\,08977\,70796\,28320\,61800\,09211\,27670\,82520\,91632\\ 10154\,43348\,57648\,36890\,62715\,98782\,09761\end{tabular}}\par\smallskip -\par\noindent{\footnotesize $u \;=$}\\[-2pt] +\par\noindent{\footnotesize $u \;=$}\\[1pt] {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}46\,82740\,38508\,23179\,24507\,22166\,30277\,19756\,51442\\ 05554\,12565\,49766\,74165\,82953\,38171\,01731\end{tabular}}\par\smallskip which Chapter~\ref{ch:modular}'s shadow arithmetic audits on two @@ -105,10 +106,10 @@ each is two careful minutes over the blocks printed above; that labor \emph{is} the pen-and-paper content at this size. Five more certified steps of exactly this shape (square, multiply by $d$, the two inversions via Fermat chains) complete the doubling, landing on -\par\noindent{\footnotesize $x_{2B} =$}\\[-2pt] +\par\noindent{\footnotesize $x_{2B} =$}\\[1pt] {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}24\,72741\,32351\,06541\,00255\,45745\,71675\,58883\,46227\\ 68167\,39763\,84567\,26423\,68252\,12336\,08206\end{tabular}}\par\smallskip -\par\noindent{\footnotesize $y_{2B} =$}\\[-2pt] +\par\noindent{\footnotesize $y_{2B} =$}\\[1pt] {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}15\,54967\,55802\,80190\,17635\,26687\,10449\,54225\,15495\\ 72066\,44506\,05805\,07079\,59306\,26430\,49417\end{tabular}}\par\smallskip --- the coordinates of $2B$ that every Ed25519 stack on earth agrees on. @@ -329,7 +330,7 @@ little-endian): bytes, nothing elided). Byte 31 is $\code{0x66} = 01100110_2$: its top bit is $0$, so the sign bit says ``$x$ even.'' The remaining 255 bits, read little-endian, are -\par\noindent{\footnotesize $y_B \;=$}\\[-2pt] +\par\noindent{\footnotesize $y_B \;=$}\\[1pt] {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}46\,31683\,56949\,26478\,16942\,83940\,03475\,16314\,13079\\ 93866\,25622\,56157\,83033\,60316\,52518\,55960\end{tabular}}\par\smallskip The design claim behind this constant: $y_B = 4/5$ in $\Fp$, i.e.\ @@ -340,10 +341,10 @@ $5\,y_B \equiv 4 \pmod p$. At full size that is one integer equation, and this one you can verify with \emph{no} shortcuts and \emph{no} witnesses: multiply $y_B$ by $5$ yourself (one right-to-left carry pass), multiply $p$ by $4$, subtract $4$, compare every digit: -\par\noindent{\footnotesize $5\,y_B - 4 \;=$}\\[-2pt] +\par\noindent{\footnotesize $5\,y_B - 4 \;=$}\\[1pt] {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}231\,58417\,84746\,32390\,84714\,19700\,17375\,81570\,65399\\ 69331\,28112\,80789\,15168\,01582\,62592\,79796\end{tabular}}\par\smallskip -\par\noindent{\footnotesize $4\,p \;=\;\;\;\;\;\;\;$}\\[-2pt] +\par\noindent{\footnotesize $4\,p \;=\;\;\;\;\;\;\;$}\\[1pt] {\footnotesize\ttfamily\begin{tabular}{@{}l@{}}231\,58417\,84746\,32390\,84714\,19700\,17375\,81570\,65399\\ 69331\,28112\,80789\,15168\,01582\,62592\,79796\end{tabular}}\par\smallskip An honest fifteen minutes, and you have hand-checked a constant that diff --git a/chapters/ch13-second-summit.tex b/chapters/ch13-second-summit.tex index c1e5039..27a8a8a 100644 --- a/chapters/ch13-second-summit.tex +++ b/chapters/ch13-second-summit.tex @@ -466,9 +466,11 @@ self-reference keeps its books honest. \begin{tryit} Touch the second summit yourself; it costs one command. Clone -\code{github.com/saymrwulf/lean-transparency-log} and run -\code{python3 verify.py --receipt -receipts/fips205-slhdsa-verified.receipt.json} --- the receipt binds +\code{github.com/saymrwulf/lean-transparency-log} and run: +\begin{center} +\code{python3 verify.py \ddash receipt receipts/fips205-slhdsa-verified.receipt.json} +\end{center} +The receipt binds leaf~18 by inclusion proof to the size-$19$ signed head. Then open \code{entries/000018.json} and find, with your own eyes: the eleven certificate names, the five oracle axioms in the apex's observed cone, diff --git a/chapters/ch14-attestation-protocol.tex b/chapters/ch14-attestation-protocol.tex index 8b9eeda..79bd79c 100644 --- a/chapters/ch14-attestation-protocol.tex +++ b/chapters/ch14-attestation-protocol.tex @@ -243,7 +243,7 @@ The fifteen-minute exercise, and the best return on time in this book: clone the mirror and run the verifier. \begin{itemize} -\item \code{python3 verify.py --all} --- plain Python for the hashing, the +\item \code{python3 verify.py \ddash all} --- plain Python for the hashing, the \code{openssl} binary for signatures, and it \emph{fails closed} without them (this chapter taught you why ``couldn't check'' must never print as a pass). It recomputes every leaf hash, every historical @@ -288,7 +288,7 @@ its trusted base; read a leaf's exclusions before believing anything beyond them. Second: the estate's paper about this log is frozen under journal review and describes the thirteen-leaf snapshot of July 2026. Nothing it describes was altered --- the paper-era leaves and heads sit byte-identical -inside today's history, and \code{verify.py --all} checks both eras in one +inside today's history, and \code{verify.py \ddash all} checks both eras in one run. A document that ages honestly inside a system that keeps moving is not a defect; it is what append-only means. diff --git a/chapters/glossary.tex b/chapters/glossary.tex index 4a3d087..98abf8c 100644 --- a/chapters/glossary.tex +++ b/chapters/glossary.tex @@ -5,8 +5,8 @@ \newcommand{\gloss}[1]{\par\smallskip\noindent{\bfseries #1.}\ } \gloss{Axiom-clean} Of a theorem: \lean{\#print axioms} reports exactly -Lean's standard trio \lean{[propext, Classical.choice, Quot.sound]} and -nothing else. The gold standard for shipped certificates +Lean's standard trio --- \lean{propext}, \lean{Classical.choice}, +\lean{Quot.sound} --- and nothing else. The gold standard for shipped certificates (Chapter~\ref{ch:honesty}). \gloss{Bounds invariant} A predicate limiting how large limbs may grow diff --git a/check-book.sh b/check-book.sh index 6c7de81..e5bf278 100755 --- a/check-book.sh +++ b/check-book.sh @@ -96,10 +96,25 @@ selftest() { [ "${1:-}" = "--selftest" ] && selftest echo "=== Phase 1: build ===" -./build.sh +BUILDLOG="$(mktemp)" +./build.sh 2>&1 | tee "$BUILDLOG" command -v pdfinfo >/dev/null && command -v pdftotext >/dev/null || { echo "FAIL: poppler-utils (pdfinfo/pdftotext) required"; exit 1; } +# Print-quality gate: an overfull box past 10pt is text visibly leaving the +# margin or a border slicing through content. The 2026-08-08 visual audit +# found the two worst rendering defects in the book had been announced in +# every build log as 80pt/73pt overfull warnings — and ignored. Never again. +if grep -oE "Overfull \\\\hbox \([0-9]+\.[0-9]+pt" "$BUILDLOG" \ + | grep -oE "[0-9]+\.[0-9]+" | awk '$1 > 10 {bad=1} END {exit bad}'; then + echo " ok no overfull box exceeds 10pt (print-quality gate)" +else + echo " FAIL overfull boxes past 10pt — text is leaving the page:" + grep -E "Overfull \\\\hbox \([0-9]{2,}" "$BUILDLOG" | sort -u | head -5 + rm -f "$BUILDLOG"; exit 1 +fi +rm -f "$BUILDLOG" + python3 "$HERE/check-book.py" "$HERE" echo diff --git a/main.pdf b/main.pdf index 498ca23..d77e9d1 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.tex b/main.tex index f927df2..0f2535b 100644 --- a/main.tex +++ b/main.tex @@ -7,13 +7,13 @@ \begin{titlepage} \pagecolor{ink}\color{paper} \begin{tikzpicture}[remember picture,overlay] - % faint pyramid motif — the proof pyramid the book builds toward + % the proof pyramid the book climbs — drawn in solid mixed colors, never + % transparency: low-opacity fills on a dark ground render as smudge and + % vary by viewer. Crisp thin outlines make it read as intentional. \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); + \draw[paper!30!ink, line width=0.5pt, fill=paper!8!ink] + ($(current page.center)+(-\w/2,{-3.0+\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} @@ -21,18 +21,21 @@ {\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} +From {\ttfamily 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 a public transparency log of machine-checked -proofs --- \textbf{\code{ltl.zkdefi.org}}, 19 entries and counting, one of them -post-quantum. Open it on your phone now; by the last chapter you will be able -to verify every entry yourself. \\ Every code snippet in this book runs. Every -claim it makes about a proof, a proof assistant has checked.\par} +{\color{paper!40!ink}\rule{\linewidth}{0.6pt}\par} +\vspace{0.15cm} +{\small\color{paper}\raggedright +Companion to a public transparency log of machine-checked proofs --- +\textbf{\code{ltl.zkdefi.org}}, 19 entries and counting, one of them +post-quantum. Open it on your phone now; by the last chapter you will be +able to verify every entry yourself.\par +\smallskip +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} @@ -45,7 +48,7 @@ claim it makes about a proof, a proof assistant has checked.\par} \vspace*{2cm} {\small \noindent\textbf{Second edition} --- published August 8, 2026: fourteen -chapters, 129 pages. +chapters, 132 pages. \medskip \noindent\emph{Publication history} diff --git a/preamble.tex b/preamble.tex index 3a70fd7..4e07966 100644 --- a/preamble.tex +++ b/preamble.tex @@ -18,7 +18,8 @@ \usepackage{fancyhdr} \usepackage{titlesec} \usepackage{booktabs} -\usepackage[strings]{underscore} % plain _ works in text; math subscripts unaffected +\usepackage[strings]{underscore} +\usepackage{needspace} % plain _ works in text; math subscripts unaffected \usepackage{hyperref} % ---- palette ------------------------------------------------------------- @@ -105,7 +106,12 @@ % Inline code: plain styled text (robust in tables/footnotes, unlike lstinline). % Also safe inside math mode (wraps itself in \text there). % Unicode symbols in inline code are handled by the declarations below. -\newcommand{\inlinecode}[1]{\ifmmode\text{\ttfamily\small #1}\else{\ttfamily\small #1}\fi} +% Inside code: never break at an underscore with a hyphen — a hyphen inside +% a printed identifier is a lie in a book that teaches exact names. +\newcommand{\codeguards}{\let\BreakableUnderscore\textunderscore\relax} +% command-line double dash, kept visibly TWO hyphens in tt (they touch otherwise) +\newcommand{\ddash}{-\kern0.10em-} +\newcommand{\inlinecode}[1]{\ifmmode\text{\ttfamily\small\codeguards#1}\else{\ttfamily\small\codeguards#1}\fi} \newcommand{\lean}[1]{\inlinecode{#1}} \newcommand{\rust}[1]{\inlinecode{#1}} \newcommand{\code}[1]{\inlinecode{#1}} @@ -195,23 +201,23 @@ % ---- pedagogical boxes: each means ONE thing ---------------------------- % BIG IDEA — the load-bearing concept of a section. -\newtcolorbox{bigidea}[1][]{enhanced,breakable,colback=accentsoft, +\newtcolorbox{bigidea}[1][]{enhanced,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, +\newtcolorbox{tryit}[1][]{enhanced,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, +\newtcolorbox{pitfall}[1][]{enhanced,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, +\newtcolorbox{aha}[1][]{enhanced,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, +\newtcolorbox{checkpoint}[1][]{enhanced,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} @@ -236,7 +242,8 @@ \newtcolorbox{worked}[1]{enhanced,breakable,colback=white,colframe=ink2, boxrule=0.4pt,leftrule=2.6pt,arc=1pt,left=10pt,right=10pt,top=8pt,bottom=8pt, colbacktitle=codebg,coltitle=ink, - fonttitle=\bfseries,title={\pennib\ Pen and paper: #1}} + fonttitle=\bfseries,title={\pennib\ Pen and paper: #1}, + title after break={\pennib\ Pen and paper: #1 \emph{(continued)}}} \providecommand{\pennib}{\raisebox{-1pt}{\small$\angle$}} % exercises @@ -246,7 +253,7 @@ % solutions — immediately after each chapter's exercises. % Every solution leads with the PATHWAY (how to find it), then the answer. -\newcommand{\solhead}[1]{\medskip\noindent% +\newcommand{\solhead}[1]{\Needspace{4\baselineskip}\medskip\noindent% {\bfseries\color{proven}Solution #1.}\ } \newcommand{\pathway}{\par\smallskip\noindent{\itshape\color{ink2}Pathway.}\ } \newcommand{\answer}{\par\smallskip\noindent{\itshape\color{ink2}Answer.}\ }