diff --git a/README.md b/README.md index d26ac8c..77db19e 100644 --- a/README.md +++ b/README.md @@ -5,18 +5,18 @@ 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 +which complete Ed25519 proof pyramids (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: +and three production forks — field, group law, scalars, and the signature +verifier itself) 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 | +| [dalek-ed25519-verified](https://github.com/saymrwulf/dalek-ed25519-verified) | the complete pyramid, upstream dalek: field 𝔽ₚ + Edwards group law + scalar arithmetic mod ℓ + the four-tier signature apex (accept ⇔ decompress(R) = [k](−A)+[s]B, hash opaque) | +| [anza-ed25519-verified](https://github.com/saymrwulf/anza-ed25519-verified) | the complete pyramid, Solana's fork, its own extraction | +| [risc0-ed25519-verified](https://github.com/saymrwulf/risc0-ed25519-verified) | the complete pyramid, RISC Zero's fork | +| [betrusted-ed25519-verified](https://github.com/saymrwulf/betrusted-ed25519-verified) | the complete pyramid, 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 | @@ -103,6 +103,11 @@ In the spirit of Chapter 11: - 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. + Re-audited 2026-07-06 after the signature apex reached its final + four-tier form (coherence pass 4): chapter 12's status diagram, apex + section, and audit-drill solution, chapter 11's boundary example, + chapter 8's extraction notes, the repo tour, and this table were + brought up to the proven state. - 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). - The three named solution certificates were kernel-audited diff --git a/chapters/appendix-repo-tour.tex b/chapters/appendix-repo-tour.tex index 407a425..e9bc302 100644 --- a/chapters/appendix-repo-tour.tex +++ b/chapters/appendix-repo-tour.tex @@ -20,9 +20,9 @@ where Montgomery form demands it. the honest-boundary statements of Chapter~\ref{ch:honesty} \\ \code{TRUSTED-BASE.md} & the ledger: every assumption, each with its reason --- read this \emph{before} being impressed by anything \\ -\code{verification/extract.sh} & extraction roots for the field layer -(Charon $\to$ LLBC $\to$ Aeneas); \code{extract-scalar.sh} likewise for -scalars \\ +\code{verification/extract.sh} & the extraction recipe (Charon $\to$ +LLBC $\to$ Aeneas): ONE merged universe per repo --- field, curve, +scalar, and the verify path --- plus the signature glue \\ \code{verification/gen/} & the extracted model. \textbf{Never hand-edited} (Chapter~\ref{ch:rust}); regenerated or left alone \\ \code{verification/Proofs/} & the human-written theorems --- @@ -58,10 +58,11 @@ you audited in Chapter~\ref{ch:field}'s worked example. (\code{fieldImplementation}) and its \lean{\#print axioms} line. This is the artifact all the marketing language ultimately refers to; note how unglamorous it looks. -\item \textbf{The frontier} --- the scalar layer's in-progress files, -clearly marked. Read one open lemma statement and recognize its shape -(it is 9.B with bigger constants). This is where -Chapter~\ref{ch:pyramid}'s invitation points. +\item \textbf{The apex} --- \code{verify\_accepts\_iff\_decompress} +in \code{Proofs/DecompressMain.lean}, the top of the four-tier stack, +and the check script's boundary phase that guards its axiom cone. Note +how short the capstone proof is: every hard fact was certified below it. +This is where Chapter~\ref{ch:pyramid}'s invitation points. \end{enumerate} \section{Running the machinery} @@ -91,7 +92,9 @@ mechanical half of the Chapter~\ref{ch:honesty} field guide, automated. unlike source text, cannot be hidden in comments. \emph{Phase 3 is the one-command audit}, run on every certificate, every time, so the axiom-clean property is continuously enforced rather than occasionally -asserted. +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. \section{The control repository} diff --git a/chapters/ch01-why-verify.tex b/chapters/ch01-why-verify.tex index 57196c0..316b7ba 100644 --- a/chapters/ch01-why-verify.tex +++ b/chapters/ch01-why-verify.tex @@ -167,7 +167,7 @@ one abstraction level and rests on the layer beneath it: \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$}; + \node[note] at (5.6,3.45) {the equation $sB = R + kA$,\\ checked from the raw bytes}; \end{tikzpicture} \end{center} diff --git a/chapters/ch08-rust-to-lean.tex b/chapters/ch08-rust-to-lean.tex index b679b5b..f6e88b2 100644 --- a/chapters/ch08-rust-to-lean.tex +++ b/chapters/ch08-rust-to-lean.tex @@ -178,13 +178,15 @@ 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 + repo (\code{extract.sh}) name exactly the needed roots and get one + small, clean, merged model per repo --- dozens of definitions instead + of a thousand. +\item \textbf{Some code will not translate.} The dalek SIMD backends use + CPU-specific intrinsics no translator models. The boundary is then + \emph{engineered} rather than assumed: extraction pins the serial + backend --- real, translatable code the campaign proved like everything + else --- and the SIMD alternatives are scoped out of the verified + claim, the scoping documented in the ledger. 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 diff --git a/chapters/ch11-honesty-and-axioms.tex b/chapters/ch11-honesty-and-axioms.tex index aa8a104..7a9dfad 100644 --- a/chapters/ch11-honesty-and-axioms.tex +++ b/chapters/ch11-honesty-and-axioms.tex @@ -190,8 +190,13 @@ 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 +correct, GIVEN the declared oracles} --- with every \emph{given} +machine-visible. The companion repos push the posture one step further +than this example: their SHA-512 is opaque with \emph{no properties +assumed at all} --- not even ``behaves ideally''; the apex theorems hold +for whatever bytes it produces --- and the backend question was +\emph{eliminated} rather than assumed (extraction pins the serial path, +which is real translated code, proven like everything below it). 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. diff --git a/chapters/ch12-the-pyramid.tex b/chapters/ch12-the-pyramid.tex index 0a60a4f..7d58030 100644 --- a/chapters/ch12-the-pyramid.tex +++ b/chapters/ch12-the-pyramid.tex @@ -20,8 +20,8 @@ and the keys. \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}; + \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}; \end{tikzpicture} \end{center} @@ -167,35 +167,56 @@ $sB = R + kA$ is not. Three multiplications by $8$, bought by exactly the three-line computation above. \end{worked} -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. +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). -\section{The apex: what ``verified signature'' will say} +\section{The apex: what ``verified signature'' says} -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. +EdDSA verification accepts $(R, s)$ on message $m$ under key $A$ when the +verification equation holds --- and RFC~8032 admits two readings. The +\emph{cofactored} form $8sB = 8R + 8kA$ (with $k = H(R,A,m)$; the $8$s +absorb the torsion, as the exercises below explore) is what ZIP-215-style +verifiers check. The dalek lineage this campaign verified checks the +\emph{stricter, canonical} form: recompute $[k](-A) + [s]B$, encode it, +and demand the signature's $R$ match \emph{byte for byte}. The apex +certificates state, in four button-enforced tiers that climb from bytes +to points, that the extracted verifier accepts exactly when: -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. +\begin{itemize}[leftmargin=1.4em] +\item \textbf{byte apex}: $\code{compress}([s]B - [k]A) = R$ as bytes; +\item \textbf{half-lift}: $R$ \emph{is the canonical encoding} of + $[k](-A) + [s]B$; +\item \textbf{point equation}: any valid curve point canonically encoded + by $R$ \emph{equals} $[k](-A) + [s]B$ --- encodings are injective on + the curve, courtesy of $d$'s non-squareness doing a second job; +\item \textbf{full lift}: $R$ \emph{decompresses} to a valid on-curve + point equal to $[k](-A) + [s]B$ --- decompression itself proven, square + root, sign bit, and all. +\end{itemize} + +The trusted base is \emph{smaller} than the one you might have predicted. +SHA-512 enters as an opaque oracle with \textbf{no assumed properties at +all} --- not even ``behaves like an ideal hash''; the theorems hold for +whatever bytes it produces. The wire-format types stay opaque. And the +point-multiplication backends are \emph{not} in the trusted base: +extraction pins the serial path, which is real translated code, proven +like everything below it. Each repo's check script has a dedicated phase +that \lean{\#print axioms} all four tiers and fails the build if any +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. \section{What you now know, and where to take it} @@ -213,10 +234,13 @@ 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 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{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. @@ -300,8 +324,8 @@ prime and $> 8$? (c) Conclude what an attacker who adds a small-order point to a public key changes, and what they provably cannot change.} \exercise{(Audit drill) Write down, from memory, the complete list of -what the apex certificate will \emph{assume} (its trusted base) and what -it will \emph{establish}, then check yourself against this chapter's +what the apex certificates \emph{assume} (their trusted base) and what +they \emph{establish}, then check yourself against this chapter's apex section. Anything you forgot is the thing to reread before you audit a real system.} @@ -349,25 +373,32 @@ invertible on the $\Z_\ell$ part.'' (c) The attacker changes the point $X$ (so: byte-level equality checks, hashes of the key, uniqueness assumptions \emph{can} be affected --- real protocols have been bitten) but provably cannot change $8X$, hence cannot affect the truth value of -any cofactored verification equation. The formal apex certificate -inherits exactly this robustness, and the ``$8$'' in its statement is -this exercise, immortalized. +any cofactored verification equation. Note carefully which verifiers +inherit this robustness: the \emph{cofactored} (ZIP-215) lineage. The +verified dalek-lineage verifier deliberately checks the stricter +canonical byte-equality criterion instead --- knowing \emph{which} +equation a library actually checks is this exercise's real teeth, and +the anza repo's ledger pins exactly that distinction for Solana's +verifier. \solhead{12.3} \pathway Close the book. Write two columns: \emph{assumes} / \emph{establishes}. Then open the apex section and diff. \answer The list your memory should reproduce --- \emph{assumes}: -(1) SHA-512 behaves as an ideal hash (axiomatized by design, in the -trusted-base ledger); (2) the untranslatable SIMD point-multiplication -backends meet their stated specs (documented, per fork); (3) the three -standard Lean axioms; (4) the extraction pipeline preserves meaning -(one tool, pinned versions). \emph{Establishes}: for every input in the -bounds discipline, the extracted verification routine returns true -\emph{iff} $8sB = 8R + 8\,H(R,A,m)\,A$ in the curve group --- with -field arithmetic, group law, scalar arithmetic, and encoding each -carried by its own kernel-checked layer below. If your two columns -match this, you can audit a verification paper's abstract in ninety -seconds --- which was the promise on the book's cover, kept. +(1) SHA-512 as an opaque oracle, with \emph{no} properties assumed --- +not even ideality; the theorems hold for whatever bytes it produces; +(2) the opaque wire-format types (the signature struct and error type, +per fork); (3) the three standard Lean axioms; (4) the extraction +pipeline preserves meaning (one tool, pinned versions). Notably ABSENT: +any backend assumption --- the serial path is pinned at extraction and +proven as real code. \emph{Establishes}, in four tiers each pinned to +exactly that boundary by the check script: the extracted verifier +returns true \emph{iff} the signature's $R$ decompresses to a valid +on-curve point equal to $[k](-A) + [s]B$ --- with field arithmetic, +group law, scalar arithmetic, encoding, and decompression each carried +by its own kernel-checked layer below. If your two columns match this, +you can audit a verification paper's abstract in ninety seconds --- +which was the promise on the book's cover, kept. \begin{checkpoint} The book's ending is a beginning, so the final checkpoint is prospective: diff --git a/chapters/glossary.tex b/chapters/glossary.tex index db90113..5908995 100644 --- a/chapters/glossary.tex +++ b/chapters/glossary.tex @@ -31,7 +31,9 @@ translates LLBC into pure Lean definitions \gloss{Cofactor} The factor $8$ in the Ed25519 group order $8\ell$; multiplying by it annihilates the small-torsion component of any point, -which is why the verification equation reads $8sB = 8R + 8kA$ +which is why \emph{cofactored} verifiers (the ZIP-215 lineage) check +$8sB = 8R + 8kA$. The verified dalek-lineage path checks the stricter +\emph{canonical} uncofactored equation byte-exactly (Chapter~\ref{ch:pyramid}). \gloss{Commuting square} The diagram --- machine operation along the diff --git a/main.pdf b/main.pdf index 4112dfb..7338efb 100644 Binary files a/main.pdf and b/main.pdf differ