verifying-crypto-with-lean/chapters/ch12-the-pyramid.tex

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

\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.)

\begin{worked}{the completeness argument, derived to its hinge}
The Bernstein--Lange proof rewards a full pen-and-paper walk --- symbols,
not toy numbers, because the argument \emph{is} the real one at every
size. We run it on the Edwards curve $x^2 + y^2 = 1 + d x^2 y^2$ with
$d$ a non-square (Ed25519's twisted form adds decorations; the skeleton
is identical, and the exercises hand you the twist). Suppose, for
contradiction, points $(x_1,y_1)$, $(x_2,y_2)$ on the curve make a
denominator vanish: $\varepsilon := d\,x_1 x_2 y_1 y_2 \in \{\pm 1\}$.
A product equal to $\pm 1$ has no zero factor, so all four coordinates
are nonzero. Three moves, each checkable by expansion:

\emph{Move 1 --- square the assumption.} From $\varepsilon^2 = 1$:
$d^2 x_1^2 x_2^2 y_1^2 y_2^2 = 1$, which rearranges to
\[
1 \;=\; d x_1^2 y_1^2 \cdot d x_2^2 y_2^2 .
\]

\emph{Move 2 --- expand a well-chosen square.} Using
$x_1^2 + y_1^2 = 1 + d x_1^2 y_1^2$ (the curve, point 1) and
$\varepsilon x_1 y_1 = d x_1^2 y_1^2\, x_2 y_2$ (multiply the definition
of $\varepsilon$ by $x_1 y_1$):
\[
(x_1 + \varepsilon y_1)^2
= x_1^2 + y_1^2 + 2\varepsilon x_1 y_1
= 1 + d x_1^2 y_1^2 + 2\, d x_1^2 y_1^2\, x_2 y_2 .
\]

\emph{Move 3 --- substitute Move 1's $1$ and factor.} Replace the
leading $1$ by $d x_1^2 y_1^2 \cdot d x_2^2 y_2^2$ and pull out
$d x_1^2 y_1^2$:
\[
(x_1 + \varepsilon y_1)^2
= d x_1^2 y_1^2 \big( d x_2^2 y_2^2 + 1 + 2 x_2 y_2 \big)
= d x_1^2 y_1^2 \big( x_2^2 + y_2^2 + 2 x_2 y_2 \big)
= d\,\big(x_1 y_1 (x_2 + y_2)\big)^2 ,
\]
where the middle equality used the curve equation for point 2 backwards
($1 + d x_2^2 y_2^2 = x_2^2 + y_2^2$). Now the hinge: if
$x_2 + y_2 \neq 0$, divide ---
\[
d = \left( \frac{x_1 + \varepsilon y_1}{x_1 y_1 (x_2 + y_2)} \right)^{2},
\]
\textbf{$d$ is a square}. And if $x_2 + y_2 = 0$, rerun Moves 2--3 with
$(x_1 - \varepsilon y_1)^2$ to get $d \cdot (x_1 y_1 (x_2 - y_2))^2$
instead --- $x_2 - y_2$ cannot \emph{also} vanish (both would force
$x_2 = y_2 = 0$). Either way $d$ is a square in $\Fp$. But Ed25519's $d$
is \emph{not} --- one Legendre-symbol computation,
$d^{(p-1)/2} \equiv -1 \pmod p$, checkable by exactly the
square-and-multiply ladder of Chapter~\ref{ch:prime}, established once
as a constant fact in the verified development. Contradiction; no
denominator ever vanishes. Savor the architecture: one quadratic-residue
bit about one constant buys the \emph{total absence of special cases}
from every point addition ever executed --- and thereby the absence of
the rarely-taken branches where Chapter~\ref{ch:why}'s bugs live. That
is what ``a curve chosen for verifiability'' means in practice.
\end{worked} 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.

\begin{worked}{sizing the group --- real constants, three-line audits}
The scalar layer's constants invite the same pen-and-paper audits as the
field's. The group order is $8\ell$ with
\[
\ell \;=\; 2^{252} + 27742317777372353535851937790883648493 ,
\]
that $38$-digit tail being an inseparable companion of anyone who works
on this layer. Three audits, each a few lines:

\emph{(1) Consistency with the curve.} A theorem of Hasse says an
elliptic curve over $\Fp$ has $p + 1 - t$ points with
$|t| \le 2\sqrt{p}$ --- so about $2^{255}$ points, within
$2^{128.5}$-ish. Check the claimed order:
$8\ell = 2^{3} \cdot 2^{252} + 8 \cdot (38\text{-digit}) =
2^{255} + (\text{a number} < 2^{129})$. Sits exactly in Hasse's window
around $p + 1 \approx 2^{255}$ ✓. The claimed structure is at least
arithmetically possible --- a thirty-second sanity check worth running on
\emph{any} curve parameter set someone hands you.

\emph{(2) The tail is not decoration.} Could a signature library
``round'' $\ell$ to $2^{252}$ --- who would notice? Anyone reducing a
$256$-bit hash output mod $\ell$: the reductions differ on roughly a
$2^{-124}$ slice of inputs (the interval lengths differ by the tail), and
the certified theorem \code{L\_val} in all four companion repos ---
\emph{the transpiled constant equals $\ell$, digit for digit} --- exists
precisely because ``a constant nobody can eyeball'' is where typos
retire. The proof is one \lean{decide}-scale comparison, and it has
teeth: change one digit of the Rust constant and \code{check-scalar.sh}
fails.

\emph{(3) Why the $8$s in the verification equation.} The full group has
order $8\ell = 2^3 \cdot \ell$, so (by the structure of finite abelian
groups) it decomposes as $\Z_8$-part $\times$ $\Z_\ell$-part: every point
splits as $X = T + Y$ with $T$ of order dividing $8$ (``torsion'') and
$Y$ of order dividing $\ell$. Multiply by $8$:
\[
8X \;=\; 8T + 8Y \;=\; \mathcal{O} + 8Y \;=\; 8Y
\]
--- the torsion component is annihilated, whoever chose it. An attacker
who tampers with a public key by adding a small-order point $T$ changes
$X$ but not $8X$; the cofactored equation $8sB = 8R + 8kA$ is therefore
immune to a whole class of malleability games that the uncofactored
$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).

\section{The apex: what ``verified signature'' says}

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:

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

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

\subsection*{Further reading, annotated}

\begin{itemize}[leftmargin=1.4em]
\item \emph{Theorem Proving in Lean 4} (Avigad, de Moura, et al.; free
online) --- the official text. Read it \emph{after} this book's
Chapters 2--5 and it will feel like meeting the extended family of
ideas you already know; its dependent-type chapters go far beyond our
needs and are worth the trip.
\item \emph{Mathematics in Lean} (the Mathlib community course) ---
hands-on Mathlib fluency: naming conventions, search strategies, the
algebra hierarchy. The fastest cure for ``I know the fact exists but
not its name,'' which will be your main bottleneck after this book.
\item \emph{The Lean Zulip} (\code{leanprover.zulipchat.com}) --- where
the community lives. Unusually welcoming to beginners; search before
asking, then ask well: a minimal example plus the goal state gets
expert answers in hours.
\item Bernstein \& Lange, \emph{Faster addition and doubling on
elliptic curves} (2007) --- the completeness proof this chapter's
worked example walked; readable with this book's preparation, and a
model of what ``designed for implementers'' mathematics looks like.
\item The RFC for EdDSA (RFC 8032) --- the signature scheme as
deployed, cofactor-$8$s and encoding details included. Read the
verification equation section against this chapter and notice how much
sharper your questions have become.
\item Project Everest / HACL$^{*}$ and Fiat Crypto --- the two other
major verified-crypto lineages (F$^{*}$-based and Coq-based
respectively), both shipping in real TLS stacks and browsers. Reading
their claims with your Chapter~\ref{ch:honesty} toolkit is instructive
in both directions: the methods differ, the honest-boundary discipline
rhymes.
\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}

\section*{Exercises}

\exercise{(Paper) Verify Move 2 and Move 3 of the completeness worked
example by full expansion --- every term written out, nothing skipped.
Then adapt the argument's \emph{first} move to the twisted curve
$-x^2 + y^2 = 1 + d x^2 y^2$: where does the $-1$ enter, and why does the
argument want $-1$ to be a \emph{square} mod $p$? (Hint: $p = 2^{255}-19
\equiv 1 \pmod 4$, and for such primes $-1$ is a quadratic residue ---
which is not an accident of the curve designers.)}

\exercise{(Paper) In the group decomposition $X = T + Y$ (torsion of
order dividing $8$ plus a $\Z_\ell$ component), verify: (a) $8X = 8Y$;
(b) $8Y \neq \mathcal{O}$ whenever $Y \neq \mathcal{O}$ --- why does this
need $\gcd(8, \ell) = 1$, and where does the argument use that $\ell$ is
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 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.}

\section*{Solutions and pathways}
\solutionsintro

\solhead{12.1}
\pathway For the expansion: Move 2 is the binomial square plus two
substitutions --- write $(x_1 + \varepsilon y_1)^2 = x_1^2 +
2\varepsilon x_1 y_1 + y_1^2$, then replace $x_1^2 + y_1^2$ via the curve
and $\varepsilon x_1 y_1$ via the definition. Move 3 is distributing
$d x_1^2 y_1^2$ and recognizing a perfect square. For the twist,
transport the curve equation and re-run Move 2.
\answer Move 2 fully expanded:
$(x_1+\varepsilon y_1)^2 = x_1^2 + 2\varepsilon x_1 y_1 + y_1^2$;
curve gives $x_1^2 + y_1^2 = 1 + dx_1^2y_1^2$; and
$\varepsilon x_1 y_1 = (d x_1 x_2 y_1 y_2)(x_1 y_1) = d x_1^2 y_1^2 x_2
y_2$ --- sum the three pieces to get the displayed line ✓. Move 3:
$d x_1^2 y_1^2 (d x_2^2 y_2^2 + 1 + 2 x_2 y_2)$; the curve for point 2
says $1 + d x_2^2 y_2^2 = x_2^2 + y_2^2$, so the bracket is
$x_2^2 + 2x_2y_2 + y_2^2 = (x_2+y_2)^2$, and
$d x_1^2 y_1^2 (x_2+y_2)^2 = d (x_1 y_1 (x_2+y_2))^2$ ✓. For the twisted
curve: $x_1^2 + y_1^2$ no longer appears --- the curve supplies
$y_1^2 - x_1^2$ --- so the well-chosen square must mix a factor
$\sqrt{-1}$ into the $x$'s (expand $(\sqrt{-1}\,x_1 + \varepsilon y_1)^2
= -x_1^2 + y_1^2 + 2\varepsilon\sqrt{-1}\,x_1 y_1$: the curve's
left-hand side appears exactly). That $\sqrt{-1}$ must \emph{exist} in
$\Fp$ for the argument to run --- hence the requirement that $-1$ be a
square, guaranteed by $p \equiv 1 \pmod 4$. The designers chose the
twist $a = -1$ \emph{because} it is a square mod this $p$: speed came
from the twist, completeness survived because of the residue class.
Parameters this well-matched are chosen, not lucky.

\solhead{12.2}
\pathway All three parts are order bookkeeping: $nZ = \mathcal{O}$
exactly when the order of $Z$ divides $n$.
\answer (a) $8X = 8T + 8Y$; the order of $T$ divides $8$, so
$8T = \mathcal{O}$, leaving $8Y$ ✓. (b) The order of $Y$ divides the
prime $\ell$, so it is $1$ or $\ell$. If $Y \neq \mathcal{O}$ the order
is $\ell$; then $8Y = \mathcal{O}$ would force $\ell \mid 8$ ---
impossible since $\ell > 8$ (it is $\approx 2^{252}$). This is where
both primality (order is $1$ or $\ell$, nothing between) and size come
in; $\gcd(8,\ell) = 1$ is the compact way to say ``multiplying by $8$ is
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. 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 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:
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}