|
|
|
|
@ -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}
|
|
|
|
|
|
|
|
|
|
@ -47,6 +47,79 @@ 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}{running the addition law by hand --- napkin curve, then the real one}
|
|
|
|
|
Two runs of the same formula: first on numbers that fit a napkin, then on
|
|
|
|
|
the real 77-digit constants with nothing hidden. \emph{The moves are
|
|
|
|
|
identical; only the digits get longer.}
|
|
|
|
|
|
|
|
|
|
\emph{Run 1 --- the napkin curve.} Work mod $13$ with $d = 2$ (a
|
|
|
|
|
non-square mod $13$: the squares are $\{1,3,4,9,10,12\}$ --- so this toy
|
|
|
|
|
inherits the real curve's completeness, as the worked example below
|
|
|
|
|
derives). The point $P = (2,4)$ is on the curve: $-4 + 16 = 12$ and
|
|
|
|
|
$1 + 2\cdot 4\cdot 16 = 129 \equiv 12$ \checkmark. Now double it. The
|
|
|
|
|
shared product first: $d\,x^2 y^2 = 2 \cdot 4 \cdot 16 = 128 \equiv 11$.
|
|
|
|
|
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
|
|
|
|
|
\]
|
|
|
|
|
(the inverses by scanning: $12\cdot 12 = 144 \equiv 1$, $3\cdot 9 = 27
|
|
|
|
|
\equiv 1$). So $2P = (10, 11)$ --- and recheck it is on the curve:
|
|
|
|
|
$-100+121 = 21 \equiv 8$; $1 + 2\cdot(100\cdot 121) \equiv 1 + 2\cdot(9
|
|
|
|
|
\cdot 4) = 73 \equiv 8$ \checkmark. Keep $(10,11)$; the apex section will
|
|
|
|
|
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]
|
|
|
|
|
{\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]
|
|
|
|
|
{\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
|
|
|
|
|
multiplies two 77-digit numbers by hand --- and nobody needs to, because
|
|
|
|
|
the machine can hand you its homework for auditing: the quotient $q$ and
|
|
|
|
|
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]
|
|
|
|
|
{\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]
|
|
|
|
|
{\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
|
|
|
|
|
independent small clocks. Digit sums (clock $9$): $x_1 \to 3$,
|
|
|
|
|
$y_1 \to 1$, $q \to 0$, $p \to 7$, $u \to 3$; left side $3\cdot 1 = 3$,
|
|
|
|
|
right side $0 \cdot 7 + 3 = 3$ \checkmark. Alternating digit sums (clock
|
|
|
|
|
$11$, signs from the units digit up): $x_1 \to 5$, $y_1 \to 9$,
|
|
|
|
|
$q \to 10$, $p \to 2$, $u \to 3$; left $5 \cdot 9 = 45 \equiv 1$, right
|
|
|
|
|
$10 \cdot 2 + 3 = 23 \equiv 1$ \checkmark. Do the digit sums yourself ---
|
|
|
|
|
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]
|
|
|
|
|
{\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]
|
|
|
|
|
{\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.
|
|
|
|
|
Two honest footnotes. A passing two-clock audit is strong evidence, not
|
|
|
|
|
proof (a wrong digit survives both clocks once in $99$ tries); the kernel
|
|
|
|
|
checks the exact equation --- the audit is \emph{your} hand on the
|
|
|
|
|
ladder, the kernel is the ratchet. And what you just did --- verify a
|
|
|
|
|
giant computation through small residues plus a supplied witness --- is
|
|
|
|
|
precisely the certificate method of Chapter~\ref{ch:prime} and the
|
|
|
|
|
denotation method of Chapter~\ref{ch:denotation}, meeting at the summit.
|
|
|
|
|
\end{worked}
|
|
|
|
|
|
|
|
|
|
\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
|
|
|
|
|
@ -121,6 +194,16 @@ limbs, Montgomery multiplication) and its own denotation bridge. Nothing
|
|
|
|
|
conceptually new --- which is itself the lesson: the method \emph{scales
|
|
|
|
|
sideways} without new ideas.
|
|
|
|
|
|
|
|
|
|
First feel the cycle on the napkin curve: the multiples of $P = (2,4)$
|
|
|
|
|
from the group-law worked example repeat with period $16$ ($16P$ is the
|
|
|
|
|
identity $(0,1)$ --- patient readers can verify with fourteen more
|
|
|
|
|
doublings-and-additions of the kind already performed). So computing
|
|
|
|
|
$21 \cdot P$ never takes $21$ additions: $21 \equiv 5 \pmod{16}$, hence
|
|
|
|
|
$21P = 5P$. \emph{All exponent bookkeeping happens mod the cycle
|
|
|
|
|
length.} For the real base point $B$ the cycle length is the prime
|
|
|
|
|
$\ell$ below, and ``bookkeeping mod $\ell$'' is an entire second
|
|
|
|
|
arithmetic world in the code --- this floor.
|
|
|
|
|
|
|
|
|
|
\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
|
|
|
|
|
@ -167,35 +250,119 @@ $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
|
|
|
|
|
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}
|
|
|
|
|
|
|
|
|
|
\begin{worked}{decompression, run twice --- napkin curve, then the real base point}
|
|
|
|
|
The four tiers stand on one mechanism: a point is stored as \emph{$y$
|
|
|
|
|
plus a single bit --- is $x$ odd or even?} Run it small, then real.
|
|
|
|
|
|
|
|
|
|
\emph{Run 1 --- the napkin curve} (mod $13$, $d = 2$, the curve of the
|
|
|
|
|
group-law worked example). Encode $2P = (10, 11)$: store $y = 11$ and the
|
|
|
|
|
bit ``$x$ even.'' Now decompress $(11, \text{even})$ from scratch. The
|
|
|
|
|
curve equation, solved for $x^2$:
|
|
|
|
|
\[
|
|
|
|
|
8 s B \;=\; 8 R + 8\,H(R, A, m)\,A
|
|
|
|
|
x^2 \;=\; \frac{y^2 - 1}{1 + d\,y^2}
|
|
|
|
|
\;=\; \frac{121 - 1}{1 + 2\cdot 121}
|
|
|
|
|
\;\equiv\; \frac{3}{9}
|
|
|
|
|
\;=\; 3 \cdot 9^{-1} \;=\; 3\cdot 3 \;=\; 9 \pmod{13}.
|
|
|
|
|
\]
|
|
|
|
|
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.
|
|
|
|
|
The square roots of $9$ mod $13$: $3$ and $10$ --- \emph{one odd, one
|
|
|
|
|
even}, and that is no accident: the two roots are $x$ and $13 - x$, and
|
|
|
|
|
$13$ is odd, so their parities always differ (unless $x = 0$, where both
|
|
|
|
|
roots coincide). The stored bit says ``even'': take $x = 10$. Recovered:
|
|
|
|
|
$(10, 11)$, exactly the point we encoded --- and no \emph{other} curve
|
|
|
|
|
point could have produced $(11, \text{even})$, which is the entire
|
|
|
|
|
content of tier 3.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
\emph{Run 2 --- the real thing.} The compressed base point of Ed25519 is
|
|
|
|
|
a 32-byte constant you can find in any implementation on earth (hex,
|
|
|
|
|
little-endian):
|
|
|
|
|
\begin{center}
|
|
|
|
|
\ttfamily 58 66 66 66 66 66 66 66 66 66 66 66 66 66 66 66\\
|
|
|
|
|
66 66 66 66 66 66 66 66 66 66 66 66 66 66 66 66
|
|
|
|
|
\end{center}
|
|
|
|
|
\noindent (one \code{58}, then thirty-one \code{66}s --- all thirty-two
|
|
|
|
|
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]
|
|
|
|
|
{\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.\
|
|
|
|
|
$5\,y_B \equiv 4 \pmod p$. At full size that is one integer equation,
|
|
|
|
|
\[
|
|
|
|
|
5 \cdot y_B - 4 \;=\; 4 \cdot p \quad\text{\emph{exactly}},
|
|
|
|
|
\]
|
|
|
|
|
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]
|
|
|
|
|
{\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]
|
|
|
|
|
{\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
|
|
|
|
|
every Ed25519 signature on the planet flows through. Then the sign bit
|
|
|
|
|
earns its keep exactly as on the napkin: the real
|
|
|
|
|
$x_B$ ends in $\ldots 202$ (even), and $p - x_B$ ends in $\ldots 747$
|
|
|
|
|
(odd --- check it from the last six digits alone: $819949 - 762202 =
|
|
|
|
|
57747$). One even root, one odd root; the bit picks $x_B$. The one thing
|
|
|
|
|
paper cannot do at this size is the square root itself: the machine
|
|
|
|
|
raises to the exponent $(p+3)/8$ --- about $252$ squarings of 77-digit
|
|
|
|
|
numbers --- and the certificate \code{sqrt\_ratio\_i\_sq\_spec} pins its
|
|
|
|
|
output with the same kind of witness-checked equation you audited in the
|
|
|
|
|
group-law example, the kernel playing the role of your two clocks.
|
|
|
|
|
\end{worked}
|
|
|
|
|
|
|
|
|
|
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 +380,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,11 +470,17 @@ 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.}
|
|
|
|
|
|
|
|
|
|
\exercise{(Paper) The point $3P = (6, 10)$ lives on the napkin curve
|
|
|
|
|
(mod $13$, $d = 2$). Encode it (which bit?), then decompress your own
|
|
|
|
|
encoding from scratch --- compute $x^2$ from $y$, find both square
|
|
|
|
|
roots by scanning, and let the bit choose. Confirm you recover $(6,10)$
|
|
|
|
|
and not the other root.}
|
|
|
|
|
|
|
|
|
|
\section*{Solutions and pathways}
|
|
|
|
|
\solutionsintro
|
|
|
|
|
|
|
|
|
|
@ -349,25 +525,44 @@ 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.
|
|
|
|
|
|
|
|
|
|
\solhead{12.4}
|
|
|
|
|
\pathway Mirror the worked example's run 1 with $y = 10$.
|
|
|
|
|
\answer Encode: $x = 6$ is even $\Rightarrow$ store $(10, \text{even})$.
|
|
|
|
|
Decompress: $y^2 = 100 \equiv 9$, so
|
|
|
|
|
$x^2 = (9-1)/(1 + 2\cdot 9) = 8/19 \equiv 8 \cdot 6^{-1}$; scanning gives
|
|
|
|
|
$6^{-1} = 11$ ($6 \cdot 11 = 66 \equiv 1$), so $x^2 = 88 \equiv 10$. The
|
|
|
|
|
roots of $10$: scan the squares --- $6^2 = 36 \equiv 10$ and
|
|
|
|
|
$7^2 = 49 \equiv 10$, so $\{6, 7\}$, one even, one odd (they sum to
|
|
|
|
|
$13$). The bit says even: $x = 6$ \checkmark. Choosing $7$ instead would
|
|
|
|
|
put you on the curve at the WRONG point $(7,10) = -3P$ --- the sign bit
|
|
|
|
|
is one bit of information doing real cryptographic work.
|
|
|
|
|
|
|
|
|
|
\begin{checkpoint}
|
|
|
|
|
The book's ending is a beginning, so the final checkpoint is prospective:
|
|
|
|
|
|
