diff --git a/chapters/appendix-repo-tour.tex b/chapters/appendix-repo-tour.tex index e9bc302..d2d2763 100644 --- a/chapters/appendix-repo-tour.tex +++ b/chapters/appendix-repo-tour.tex @@ -2,8 +2,10 @@ \label{app:tour} The companion projects are working code, laid out for auditors rather -than tourists. This appendix is the tourist map: what lives where, what -to read first, and how to run the machinery yourself. Everything below +than tourists. This appendix is the tourist map, and it ends with three +things done, not read: you will run the full verification yourself, +\emph{sabotage a proof on purpose} and watch the machinery catch you, +and finish at a stop that is not on your disk at all. Everything below names \code{dalek-ed25519-verified}; the other three ed25519 forks are structured identically, and \code{pasta-pallas-verified} differs only where Montgomery form demands it. @@ -96,6 +98,22 @@ asserted. A fourth phase arrived with the signature layer: \emph{3b pins the apex tiers' cones to the documented hash/wire-format boundary EXACTLY} --- an unexpected addition \emph{or removal} fails the build. +\begin{tryit} +Now sabotage it. A green button proves nothing until you have seen it +red for the right reason. In your local clone (nothing here leaves your +machine, and \code{git} undoes it all): pick one digit of one constant +in a \code{Proofs/} statement --- say, turn a $19$ into an $18$ in a +bounds lemma --- and run \code{./verification/check.sh}. Watch which +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 +something reading cannot: the difference between believing the button +because it is green and believing it because you have personally failed +to fool it. +\end{tryit} + \section{The control repository} \code{formal-verification-control} is the method distilled --- written @@ -116,10 +134,26 @@ of these stories; the file has the rest, and reading failure maps before starting work is the cheapest experience money can't buy. \end{itemize} +\section{The last stop is not on your disk} + +The repository you just toured does not only sit on your machine or on a +code-hosting site; it is \emph{attested}. The public transparency log at +\code{ltl.zkdefi.org} carries a leaf binding this repo's pinned commit to +the certificate names, their statement fingerprints, and their observed +axiom cones --- the very things your sabotage exercise just tried to +fake locally, notarized globally. Find the leaf for +\code{dalek-ed25519-verified}, and check that the commit it names is the +one you have been reading. Chapter~\ref{ch:attestation} is the full +protocol --- including the fifteen-minute exercise where a stranger (you) +re-derives the log's Merkle root from nothing but published bytes. The +tour ends here on purpose: floor plan, button, sabotage, control room, +and finally the public record that makes the whole thing checkable by +someone who has never met you. + A closing observation to carry out of the tour: nothing in these repositories asks to be trusted. The claims are in the READMEs, the assumptions in the ledgers, the checks in a script anyone can run, the -axioms in a one-command audit. That shape --- \emph{auditability as the -default posture} --- is the real deliverable of the whole verification -enterprise, and the standard this book hopes you now hold everything -else to. +axioms in a one-command audit, the whole ensemble in a public log. That +shape --- \emph{auditability as the default posture} --- is the real +deliverable of the whole verification enterprise, and the standard this +book hopes you now hold everything else to. diff --git a/chapters/appendix-toolkit.tex b/chapters/appendix-toolkit.tex index b2bbc48..aa8c265 100644 --- a/chapters/appendix-toolkit.tex +++ b/chapters/appendix-toolkit.tex @@ -1,11 +1,16 @@ \chapter{The Pen-and-Paper Toolkit} \label{app:toolkit} -Every worked example in this book leaned on a small set of hand-computation -techniques. This appendix collects them as recipe cards --- the reference -you will reach for when auditing numbers in the wild, where there is no -chapter telling you which trick applies. Each card ends with a -thirty-second drill; answers close the appendix. +You are in a design review. A slide asserts that nine products of +$31$-bit limbs accumulate in a $64$-bit word without overflow, the +presenter is already on the next slide, and everyone else is nodding. +You have perhaps forty seconds and no proof assistant. This appendix is +for that room. Every worked example in this book leaned on a small set of +hand-computation techniques; here they are as recipe cards --- the +reference for auditing numbers in the wild, where no chapter title tells +you which trick applies. Each card ends with a thirty-second drill; +answers close the appendix. (The slide, by the way, is wrong --- Card~6 +and Drill~6 are the forty seconds that catch it.) \section{Card 1: powers of two into powers of ten} @@ -126,6 +131,9 @@ $2^{255} \equiv 0 \pmod 4$, so $p \equiv -19 \equiv -3 \equiv \emph{Drill 7a.} Is $3$ a square mod $11$? ($3^5 \bmod 11$ by ladder; then find the root or trust the sign.) +\emph{Drill 7b.} Is $-1$ a square mod $11$? No ladder allowed --- decide +it by exponent parity alone, the way the card handled $p = 2^{255}-19$. + \section{Card 8: the substitution test (specs)} Given a claimed specification: substitute the worst implementation of @@ -178,9 +186,22 @@ lines of arithmetic as your citation. (ladder: $3^2 = 9$, $3^4 = 81 \equiv 4$, $3^5 = 4 \cdot 3 = 12 \equiv 1$) --- so $3$ \emph{is} a square mod $11$; indeed $5^2 = 25 \equiv 3$. +\solhead{Drill 7b} $(-1)^{(11-1)/2} = (-1)^{5} = -1$: \emph{not} a +square --- because $(11-1)/2 = 5$ is odd, i.e.\ $11 \equiv 3 \pmod 4$. +Parity of one exponent, no arithmetic bigger than a division by two. + \solhead{Drill 8} No. Substitute $\code{mul}_{c}(a,b) :=$ ``return the constant array $c$'': both sides become $\denote{c}$ --- the adversary passes. Commutativity-of-the-implementation is a \emph{symmetry} spec; symmetric garbage satisfies it. (Real correctness needs the other side of the square: $\denote{a} \cdot \denote{b}$, a quantity the implementation cannot influence.) + +\bigskip +\noindent\emph{The street assignment.} These cards were built in a book, +but they pay rent outside it. Sometime this week you will meet a number +in the wild --- a README boasting ``$2^{128}$ operations to break,'' a +blog post's limb bound, a slide with an accumulator width. Pick one and +audit it with the cards, on paper, before you believe it. The first time +you catch a real number being wrong in public, this appendix will have +paid for the whole book. diff --git a/chapters/appendix-walkthroughs.tex b/chapters/appendix-walkthroughs.tex index 2284727..be83912 100644 --- a/chapters/appendix-walkthroughs.tex +++ b/chapters/appendix-walkthroughs.tex @@ -1,13 +1,17 @@ \chapter{Guided Walkthroughs of the Exercise Files} \label{app:walkthroughs} -The \code{exercises/} folder contains eight Lean files with \lean{sorry} -holes; \code{solutions/} contains their completed twins (every one -compiled, with no \lean{sorry}, against the pinned toolchain). This -appendix is the middle path between the two: for every hole, the -\emph{pathway} --- what to look at, what to try, where you will -probably get stuck and why --- and then the resolution. Use it when a -hole has genuinely defeated you; the file order follows the book. +You are probably here because a hole has defeated you. Good --- this +appendix was written for exactly that moment, and it will not waste it +by simply handing over answers. The \code{exercises/} folder contains +the Lean files with \lean{sorry} holes; \code{solutions/} contains their +completed twins, every one compiled, with no \lean{sorry}, against the +pinned toolchain (\code{ls exercises/} is the authoritative roster --- +trust the folder, not a number printed in a book). This appendix is the +middle path between the two, at a fixed exchange rate of one hole, one +paragraph: the \emph{pathway} --- what to look at, what to try, where +you will probably get stuck and why --- and then the resolution. The +file order follows the book. \section{Ch02.lean --- definitions by recursion} @@ -38,7 +42,7 @@ constructor syntax \lean{⟨num, den⟩}; the type-level lesson (what \section{Ch03.lean --- term-mode logic} The file's discipline (no tactics) makes every hole a smallish program. -The reliable procedure for all six: (1) unfold the connectives into +The reliable procedure, for every hole in the file: (1) unfold the connectives into arrow/pair/tagged-union shape; (2) write \lean{fun} for every arrow in the goal; (3) inside, build the result with \lean{And.intro} / \lean{Or.inl} / \lean{Or.inr} / projections / application. Where people diff --git a/chapters/ch04-tactics.tex b/chapters/ch04-tactics.tex index c7db929..a6d5e7e 100644 --- a/chapters/ch04-tactics.tex +++ b/chapters/ch04-tactics.tex @@ -3,9 +3,11 @@ \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. +Here is the problem with everything you learned in the last chapter: a real +correctness proof for field multiplication --- the theorem this book is +climbing toward --- would, written as a raw proof program, be a program the +size of a small compiler. Nobody writes those by hand. (Chapter~\ref{ch:pat}'s +handcrafted terms were honest work; honest work does not scale.) 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. @@ -171,6 +173,13 @@ 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} +\section{When you get stuck --- and you will} + +No chapter on tactics is honest without this section. The steady march of +examples above is what proving looks like \emph{afterwards}, cleaned up for +print. What it looks like \emph{during} is the next box --- and the +discipline it teaches is worth more than any tactic in the table. + \begin{worked}{a debugging session, reconstructed honestly} Here is a stuck proof, exactly as it happens to everyone, worked through with the discipline this chapter preaches. Goal: every number @@ -392,5 +401,9 @@ 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. +interrogate the \emph{statement} before blaming the proof. One goal from the +exercises is deliberately still open: the bound +$a \cdot 19 < 2^{56}$, which no tactic in this chapter's table owns. Carry it +with you --- the next chapter opens by handing you the tactic that eats it in +one line. \end{checkpoint} diff --git a/chapters/ch06-modular-arithmetic.tex b/chapters/ch06-modular-arithmetic.tex index 024dbfe..95e6c3e 100644 --- a/chapters/ch06-modular-arithmetic.tex +++ b/chapters/ch06-modular-arithmetic.tex @@ -3,10 +3,17 @@ \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 +A dare, to open: before this chapter ends you will compute --- by hand, on +paper --- the exact multiplicative inverse of $19$ modulo a $77$-digit prime, +and no number you write down will be longer than two digits. Professional +cryptographers do this calculation's industrial cousin billions of times a +second; you will do it once, slowly, and own it. + +The number system that makes the dare possible is one you already use daily: +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 \] @@ -131,6 +138,18 @@ couple hundred multiplications of overhead for silence; you will meet this trade at every layer of the pyramid. \end{worked} +\begin{tryit} +That was the dare from the chapter's first paragraph, delivered. Now let a +machine referee your paper. In a scratch Lean file: +\begin{lstlisting}[language=Lean] +def p : Nat := 2^255 - 19 +#eval (19 * (3 + 7 * ((p - 8) / 19))) % p -- 1 +\end{lstlisting} +If it prints \lean{1}, your five hand divisions just controlled a +computation over 77-digit numbers. That feeling --- small paper steps, +machine-confirmed at full scale --- is the entire working style of this book. +\end{tryit} + \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 @@ -406,5 +425,10 @@ 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. +\lean{ring}, and a Mathlib lemma found by name. And you should be able to +say, in one sentence, why real code pays $254$ squarings for an inverse that +Euclid finds in five divisions: \emph{the expensive route runs in the same +time for every input, and silence about secrets is worth two hundred +multiplications}. That sentence is your first piece of cryptographic +engineering judgment. \end{checkpoint} diff --git a/chapters/ch10-verifying-a-field.tex b/chapters/ch10-verifying-a-field.tex index b8e0980..fe951a4 100644 --- a/chapters/ch10-verifying-a-field.tex +++ b/chapters/ch10-verifying-a-field.tex @@ -1,6 +1,14 @@ \chapter{Verifying a Field: The Full Campaign} \label{ch:field} +Partway through the campaign this chapter narrates, one proof step consumed +twelve gigabytes of memory and took the machine down --- not a slow test, not +a warning in a log: the computer proving these theorems crashed, mid-proof, +because of how a proof was written. This chapter climbs toward that wall, +hits it, quantifies exactly why it stands where it stands, and comes out the +other side with the discipline the rest of the book runs on. The crash is +the most instructive thing in the chapter. Keep it in view. + \section{The summit statement} Every thread so far --- specs as types, tactics, automation, $\Fp$, @@ -22,6 +30,11 @@ theorem fieldImplementation : ∧ ... -- reduce, negate, encode \end{lstlisting} +(Vocabulary re-armed, from Chapter~\ref{ch:denotation}: \lean{Bnd a} says +$a$'s limbs sit inside their envelopes; each \lean{...Square} says one +operation's commuting square closes --- run the extracted code, denote the +result, and you get the same field element as doing the mathematics.) + 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 @@ -98,6 +111,21 @@ is a patched CVE. Now you know how to tell which side of that line a codebase is on. \end{worked} +\begin{tryit} +Do not take the box's word for the margin of $151$ --- falsify the rejected +design yourself: +\begin{lstlisting}[language=Lean] +#eval (8 * (2^51 - 19) : Int) - (2^54 - 1) -- -151 +#eval (16 * (2^51 - 19) : Int) - (2^54 - 1) -- 18014398509481681 +\end{lstlisting} +The first line is the deficit a $k=8$ subtraction suffers when a limb of $b$ +sits within $151$ of its envelope's top: in unsigned words that negative +number is a silent wrap-around --- and a random test hits the triggering +region with probability about $151/2^{54}$, which is to say never. The +second line is the shipped design's headroom. Two \lean{\#eval}s, one +CVE-class distinction. +\end{tryit} + \begin{worked}{verifying the inversion chain's bookkeeping --- all 265 steps} Step 6 sounds heroic --- verify a hand-crafted chain of $254$ squarings and $11$ multiplications computes $a^{p-2}$ --- until you see that the @@ -147,14 +175,15 @@ undergraduate audits over coffee. \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 +\textbf{The wall that was really there.} This is the crash from the +chapter's first sentence, and here is exactly how it was earned: a +\code{mul}-scale goal, handed to a general decision procedure in one +monolithic call --- the natural move, the move you would make --- +generates an internal certificate with coefficients on the order of +$2^{256}$, and checking it can exhaust the proof checker's memory. During +the development of the Pasta field proofs that one call ate twelve +gigabytes and took the machine down (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 @@ -340,6 +369,14 @@ if the optimizer wrote a second path, the verifier owes a second theorem}. (This is also exactly why the four forks each got their own proofs: same math, four instruction streams.) +One last thing, so the summit does not feel abstract: the certificate this +chapter taught you to state is not a textbook artifact. It lives in four +public repositories --- one per fork --- where \code{check.sh} rebuilds it +from scratch on demand, and each of those repositories is attested as a +leaf of the live transparency log at \code{ltl.zkdefi.org}. When you audit +one with the four questions above, you are not doing an exercise; you are +doing the thing. + \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 diff --git a/chapters/ch12-the-pyramid.tex b/chapters/ch12-the-pyramid.tex index 19df1de..79439e3 100644 --- a/chapters/ch12-the-pyramid.tex +++ b/chapters/ch12-the-pyramid.tex @@ -4,10 +4,11 @@ \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. +is still three stories up. This chapter climbs them --- what each layer +\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. +The floors above the field enter this chapter as question marks; by the last +section you will know precisely which of them are theorems. \begin{center} \begin{tikzpicture}[ @@ -19,9 +20,9 @@ and the keys. \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{done}: add, sub, Montgomery mul\\ certified, all 4 forks}; - \node[st] at (5.7,3.75) {\textbf{done}: accept $\Leftrightarrow$ decompress$(R) = [k](-A){+}[s]B$;\\ hash an opaque oracle by design}; + \node[st] at (5.7,1.25) {\textbf{?} --- this chapter, second section}; + \node[st] at (5.7,2.5) {\textbf{?} --- third section}; + \node[st] at (5.7,3.75) {\textbf{?} --- the apex section}; \end{tikzpicture} \end{center} @@ -182,7 +183,8 @@ $(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. +own extraction. First question mark from the opening figure, resolved: +\textbf{group law --- done, complete addition, all four forks.} \section{Scalars: a second field, and a frontier} @@ -250,17 +252,25 @@ $sB = R + kA$ is not. Three multiplications by $8$, bought by exactly the three-line computation above. \end{worked} -The engineering met a wall here, and this book has told you enough truth -to locate it precisely --- and to appreciate how it fell. Scalar Montgomery -multiplication mixes $2^{256}$-scale coefficients into single certificate -steps; this is the kernel-capacity wall of Chapter~\ref{ch:field}, and for -a while it marked the campaign's working edge. It was crossed the way the -method file predicts: re-decompose until every heavy identity is an -isolated, context-free lemma the kernel checks alone --- exact-division -Montgomery rounds, a double round through $RR \equiv R^2$ --- and the -layer is now \emph{complete on all four forks}: add, sub, and Montgomery -multiplication certified (including the pleasing theorem that the code's -constant \code{L} \emph{is} $\ell$, digit for digit). +The engineering met a wall here, and you have earned the exact +coordinates. Picture the session: the Montgomery multiplication square is +stated, the strategy that conquered the field layer is deployed, and the +checker simply --- does not come back. Not an error message; a machine +grinding toward the memory ceiling of Chapter~\ref{ch:field}, because +scalar Montgomery multiplication mixes $2^{256}$-scale coefficients into +single certificate steps, and no amount of waiting fixes arithmetic that +does not fit. For a while this wall \emph{was} the campaign's working +edge --- the honest label on the map read ``frontier,'' and it stayed +there for weeks. It fell the way the method file predicts, not by a +bigger machine but by smaller lemmas: re-decompose until every heavy +identity is an isolated, context-free lemma the kernel checks alone --- +exact-division Montgomery rounds, a double round through +$RR \equiv R^2$ --- and the layer is now \emph{complete on all four +forks}: add, sub, and Montgomery multiplication certified (including the +pleasing theorem that the code's constant \code{L} \emph{is} $\ell$, +digit for digit). Second question mark, resolved: \textbf{scalars --- +done, add, sub, Montgomery mul certified, all four forks.} One floor to +go. \section{The apex: what ``verified signature'' says} @@ -362,7 +372,10 @@ cone deviates from that documented boundary by a single axiom. Read that again with Chapter~\ref{ch:honesty} eyes: it is a \emph{smaller} claim than ``Ed25519 is verified!'' --- nothing about the hash, nothing about signing, nothing about side channels --- and that is -exactly why you can believe it. +exactly why you can believe it. And with that, the last question mark +falls: \textbf{apex --- done, accept $\Leftrightarrow$ +decompress$(R) = [k](-A)+[s]B$, hash an opaque oracle by design.} The +opening figure is now all theorems, floor to peak, on all four forks. \section{What you now know, and where to take it} @@ -380,13 +393,6 @@ Where to go from here, in increasing order of ambition: \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 ed25519 pyramids are capped, but - the Pasta curve layer (Pallas group law and scalar multiplication) is - paused with its field foundations proven and the route mapped --- the - scalar layer's kernel-frontier crossing is the template, and the - control repo's \code{METHOD.md}/\code{TIERS.md} 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. @@ -397,6 +403,21 @@ Where to go from here, in increasing order of ambition: standard next doors. \end{itemize} +\subsection*{Where you come in} + +The chapter title made a promise, and here it is, kept without +condescension: there is open, real work on this pyramid sized for the +person who finished this book. The ed25519 pyramids are capped, but the +Pasta curve layer (the Pallas group law and scalar multiplication) is +paused with its field foundations proven and the route mapped. The +terrain is known: the scalar layer's kernel-frontier crossing is the +template for the hard part, and the control repo's +\code{METHOD.md}/\code{TIERS.md} state exactly what a finished brick +looks like --- spec shape, axiom audit, check-script entry. Nobody is +saving this for an expert. Frontier work in machine-checked cryptography +is, right now, undergraduate-accessible, and every chapter before this +one was the access. + \subsection*{Further reading, annotated} \begin{itemize}[leftmargin=1.4em] diff --git a/main.pdf b/main.pdf index c8520d8..66b5563 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.tex b/main.tex index c9ed2e2..1a8050e 100644 --- a/main.tex +++ b/main.tex @@ -63,11 +63,6 @@ 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. @@ -83,6 +78,13 @@ strict compiler for it. Once you see proofs as programs, the fear evaporates and the fun begins. \end{aha} +\noindent\emph{(That green box you just read is an ``aha'' --- an intuition +meant to click. You will also meet coral \emph{big idea} boxes for +load-bearing concepts, grey \emph{try it} boxes that ask you to run something, +amber \emph{pitfall} boxes marking traps, and a framed \emph{checkpoint} at +each chapter's end. That is the whole legend; you have now seen one in the +wild.)} + \subsection*{Working the pen-and-paper material} The notebook-ruled \emph{Pen and paper} boxes are not optional