verifying-crypto-with-lean/chapters/ch14-attestation-protocol.tex

\chapter{The Attestation Protocol: Who Checks the Checker?}
\label{ch:attestation}

\section{The second act nobody warns you about}

The question the last checkpoint left you holding --- that script, that
log, who checks \emph{them}? --- has a name, and a body count.
Chapter~\ref{ch:honesty} taught you to interrogate a certificate: ask what it
rests on, and refuse to be impressed by a file that merely compiles. That
chapter had a blind spot, and this one exists because a sequence of external
reviewers found it.

The blind spot is this. \lean{\#print axioms} tells \emph{you}, at \emph{your}
terminal, that a theorem's cone is clean. Then you write a script that runs it
across your project, the script prints \texttt{ALL GREEN}, and you publish that
green light as evidence. Between the kernel's verdict and the reader's belief
sits a piece of software you wrote --- and \emph{that software is not verified
by anything}.

\begin{bigidea}
Verification is \textbf{two acts}, not one.

\textbf{Act one --- proof.} The Lean kernel decides whether a term is a valid
derivation of its statement. This is mathematics. It is what everyone pictures
when they hear ``formally verified''.

\textbf{Act two --- attestation.} Establishing that what the kernel accepted is
what you \emph{claim}, resting only on what you \emph{say} it rests on, about
the artifact you \emph{say} it concerns --- and that a stranger who was not
present and does not trust you can check every part of that for themselves.

\medskip
\textbf{Lean decides whether a proof is valid. The Attestation Protocol decides
whether anyone else can know that.} A proof without an attestation protocol is
a private conviction, not public evidence.
\end{bigidea}

The companion projects learned this expensively. In one campaign, eleven
theorems about a hash-based signature verifier were proved in \textbf{two days}
and no reviewer ever disputed one of them. Making the green light over those
same eleven theorems mean something to a determined skeptic took \textbf{eight
rounds of review} and turned up \textbf{eighteen distinct defect classes} ---
none of them in the mathematics, all of them in act two.

\section{The shape of every failure}

Here is the finding that makes this chapter teachable. All eighteen defects had
\emph{one shape}:

\begin{aha}
\textbf{Something load-bearing sat outside the binding.}

The audit was always \emph{sound} about what it examined. The entire attack
surface was what it did \emph{not} examine.
\end{aha}

Read the greatest hits and watch the pattern repeat. Each of these was
demonstrated end-to-end against a button that was printing \texttt{ALL GREEN}
at the time:

\begin{itemize}
  \item \textbf{The certificate list was outside.} Delete one row from the list
        of audited theorems and that theorem silently leaves the audit. Nothing
        noticed.
  \item \textbf{Un-listed declarations were outside.} Add
        \lean{axiom cheat : ∀ (P : Prop), P} and
        \lean{theorem oops : False := cheat _} to a proof file. The audit
        checked the theorems on its list; this one was not on the list.
        \textbf{The repository proved \lean{False} and the button stayed
        green.}
  \item \textbf{Non-theorems were outside.} After that was fixed, the same
        payload as a \lean{def} rather than a \lean{theorem} passed --- the
        enumeration matched only theorems.
  \item \textbf{The auditor was outside itself.} After \emph{that} was fixed,
        the same payload placed \emph{inside the audit driver} passed, because
        the driver was exempt from its own enumeration.
  \item \textbf{Statements were outside.} Replace a theorem's statement with a
        tautology that happens to have the same axiom cone. Passes.
  \item \textbf{Specifications were outside.} This is the subtle one. Each
        certificate said ``the extracted loop equals this hand-written
        reference fold''. Redefine the fold to \emph{be} the extracted loop.
        The certificate now says \emph{the loop equals the loop} --- vacuous ---
        and the axiom cone, the statement hash, and the digest are all
        \textbf{byte-identical}.
  \item \textbf{The policy was outside.} The audit compared each cone against a
        list of permitted axioms. That list was not itself covered by the
        digest. Add one name to it and every protection re-opens, digest
        unchanged.
  \item \textbf{The subject was outside.} The proofs were about a generated
        model file. Hand-edit the model; every phase still passes.
  \item \textbf{The tools were outside.} Stub the compiler-wrapper script and
        the button printed \texttt{ALL GREEN} in \textbf{3.6 seconds} over
        deliberately destroyed proofs. Flip two characters in the audit
        driver's fail-closed guards and every check switched off with the
        digest byte-identical.
\end{itemize}

\begin{pitfall}
Notice what is \emph{not} on that list: a wrong proof, a wrong theorem, a bug in
Lean. The kernel did its job perfectly throughout. Every single failure was in
the apparatus built \emph{around} it --- by the same person who was reporting
the results.
\end{pitfall}

\section{Completeness of binding}

Because the failures all have one shape, the property to design for has one
name. It is not soundness --- soundness was never the problem.

\begin{bigidea}
\textbf{Completeness of binding.} Everything load-bearing is inside the binding:
the statements, the definitions those statements are stated \emph{against}, the
policy that decides what is permitted, the bytes of the artifact being reasoned
about, and the tools doing the checking.
\end{bigidea}

Four rules follow, and each one is the generalisation of a defect above.

\subsection{Derive the population; never keep a list}

A hand-maintained list of ``things that must be checked'' is one more thing that
can fall out of sync --- and did, twice. Derive membership instead:

\begin{itemize}
  \item from the \emph{environment}: every declaration in these modules, obtained
        by walking the environment, not by naming them;
  \item from the \emph{filesystem}: every \lean{.lean} file under the generated
        directory must appear in the hash map, so a new file fails closed;
  \item from the \emph{type system}: the transitive closure of constants a
        statement mentions, so a new reference definition cannot appear
        unnoticed;
  \item from a \emph{file attribute}: every executable file in the verification
        directory must be pinned --- so adding a script fails until you pin it.
\end{itemize}

\subsection{Fail closed on absence}

\begin{pitfall}
The most common bug in an audit script: \emph{nothing found} and \emph{nothing
wrong} share a code path.

A missing report, an empty cone, a truncated line, a renamed theorem, an absent
map key --- each of these must be a build failure. In the campaign above,
fail-open-on-absence was both the \emph{first} defect found and the
\emph{last}.
\end{pitfall}

\subsection{Exact, not subset}

Checking that a cone contains nothing forbidden is not enough. A certificate can
lie by resting on \emph{less} than you declared as well as more --- if your
theorem quietly stopped depending on the hash function, something is very wrong,
and a subset check will smile at you. Require set \emph{equality}.

\subsection{A stranger must be able to re-derive it}

The final rule is the one that separates evidence from assertion. Publish a
digest a reader can recompute; commit the input that digest is taken over, so a
mismatch can be \emph{diffed} rather than merely reported; and record who ran
the check, on what machine, at which commit.

\section{The meta-defect: assertions that pass for the wrong reason}

There is a second lesson, about \emph{tests} rather than about products, and it
is humbling enough to state plainly. Across the same eight rounds, \textbf{eight
separate assertions were found to be checking nothing} --- including two inside
fixes written to repair that very problem.

The purest specimen. A script transformed a data file by dropping one field, and
carried this line:

\begin{lstlisting}[language=Python]
kept = {k: v for k, v in record.items() if k not in DROP}
assert set(kept) == set(record) - DROP   # can never fail
\end{lstlisting}

\lean{kept} was built by the comprehension on the line above. The assertion is a
tautology. The first attempt to repair it compared \lean{kept[k]} against
\lean{record[k]} --- tautological for exactly the same reason.

\begin{aha}
\textbf{No check inside a transformer can detect a corrupted input, because the
transformer is what defines the output from that input.}

Faithfulness there is a property a \emph{reviewer reads}, not something the code
can test about itself. What can actually fail --- and therefore what must carry
the weight --- is the pin on the input, the presence and count guards, and an
independent re-derivation.
\end{aha}

\begin{tryit}
Take any test you have written that guards an important property. Now
\textbf{break the thing it guards} and run it.

If it does not go red --- or goes red with a message about something else ---
you have a decoration, not a test. Do this for every guard you own. In the
campaign described here, that exercise would have caught eight defects, and the
people who eventually caught them were strangers.
\end{tryit}

\section{What this means for you}

You will not build an eighteen-attack self-test for a homework exercise, and you
should not. What you should take away is a habit of mind and a vocabulary.

\begin{bigidea}
When you next read the words ``formally verified'', ask two questions instead of
one.

\textbf{Act one:} what statement did a kernel accept, and what does it rest on?
(Chapter~\ref{ch:honesty} taught you this.)

\textbf{Act two:} what binds that statement to the artifact I care about, who
checked, what did the checker \emph{not} look at, and can I re-derive any of it
myself?

If a project cannot answer the second set, it has done act one and called it
finished --- which is exactly the mistake these chapters were rewritten to
prevent.
\end{bigidea}

And when it is your own project: invite someone to attack the button, early.
Every one of the eighteen defects was found by a reviewer trying to break it.
\emph{None} was found by the author reviewing their own work --- and the author
looked, repeatedly, with the same care they had used to write the proofs.

\section{Go and touch the real thing}
\label{sec:live-log}

Everything in this chapter runs in production, in public, right now. The
companion estate operates a \emph{transparency log} of its own attestations:
a Merkle accumulator whose leaves are signed statements of the form ``this
repository, at this exact commit, was checked by its own button, and these
are the certificates it proved, on exactly these axiom cones.'' The log is
served at \texttt{ltl.zkdefi.org} and mirrored as an ordinary git repository
(\texttt{github.com/saymrwulf/lean-transparency-log}) that you can clone and
interrogate offline. It is act two, industrialized: every failure class this
chapter catalogued has a gate in that pipeline because a reviewer once got
past the spot where the gate now stands.

\begin{tryit}
The fifteen-minute exercise, and the best return on time in this book: clone
the mirror and run the verifier.

\begin{itemize}
\item \code{python3 verify.py --all} --- plain Python for the hashing, the
  \code{openssl} binary for signatures, and it \emph{fails closed} without
  them (this chapter taught you why ``couldn't check'' must
  never print as a pass). It recomputes every leaf hash, every historical
  tree head against its recomputed prefix root, every signature, and every
  inclusion proof --- your machine, your verdict, nobody's word.
\item Pin the trust anchors \emph{two independent ways}: the keys are served
  by the site (\texttt{/log-public-key}, \texttt{/log-slhdsa-public-key})
  and shipped in the mirror (\code{provider.ed25519.pub},
  \code{provider.slhdsa.pub}). The copies must agree byte-for-byte. If they
  ever disagree, you have caught something worth catching.
\item Read one leaf in full --- \code{entries/000018.json} is a good choice
  --- and find, inside it, every vocabulary item of this chapter: the pinned
  commit, the certificate list, the \emph{observed} axiom cones, the machine
  protection, and the stated exclusions.
\end{itemize}
\end{tryit}

The log's nineteen leaves map onto this book. Leaves 13--16 attest the four
ed25519 repositories whose pyramid you climbed in
Chapters~\ref{ch:modular}--\ref{ch:pyramid}: forty-four certificates each ---
twenty-seven on the main button, thirteen on the scalar button, and the four
apex-tier theorems whose \emph{documented, boundary-exact} cones are
Chapter~\ref{ch:honesty}'s lesson enforced in production. Leaf 17 is this
chapter made literal: the log carries kernel-checked proofs of \emph{its own
Merkle machinery} as one of its own entries --- ``who checks the checker?''
answered by putting the checker's mathematics inside the thing it checks.
And leaf 18 is the second summit you climbed in
Chapter~\ref{ch:secondsummit} --- the eleven SLH-DSA certificates, the
cone-growth table, the see-saw: you can now read every field of that leaf
against a chapter of your own experience.
Since tree 14 every head also carries an \emph{additive} deterministic
SLH-DSA signature beside the required Ed25519 one; heads published before
then have none, and the verifier reports them as \code{ABSENT} rather than
failing them --- an append-only log keeps its history, including the history
of its own signature scheme.

Two boundaries, so that you read the log the way this book taught you to
read everything. First: for both signature algorithms the estate has proved
\emph{verification} and nothing about \emph{signing} --- the heads are
signed by unproven code and checkable by proven code, and every leaf names
its trusted base; read a leaf's exclusions before believing anything beyond
them. Second: the estate's paper about this log is frozen under journal
review and describes the thirteen-leaf snapshot of July 2026. Nothing it
describes was altered --- the paper-era leaves and heads sit byte-identical
inside today's history, and \code{verify.py --all} checks both eras in one
run. A document that ages honestly inside a system that keeps moving is not
a defect; it is what append-only means.

That is the whole arc of this book in one artifact: arithmetic became
theorems (act one), theorems became certificates with named cones
(Chapter~\ref{ch:honesty}), the method crossed to a second pyramid with
different mathematics and held (Chapter~\ref{ch:secondsummit}),
certificates became attestations a stranger can re-derive (this chapter)
--- and the attestations went into a structure that remembers everything
and lets anyone catch it lying. When you build your own, you now know what
it costs, and where the bodies are buried.

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

\section*{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{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{Extend the estate.} Chapter~\ref{ch:pyramid}'s ``Where you
  come in'' names the open frontier --- the paused Pasta curve layer ---
  and the control repository's method files say exactly what a finished
  brick looks like. When yours is done, this chapter told you how to
  attest it, and the log is where it goes.
\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~\ref{ch:lean}--\ref{ch:automation} 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
Chapter~\ref{ch:pyramid}'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) and FIPS 205 (SLH-DSA) --- the two
signature schemes as deployed, cofactor-$8$s, encodings, and address
words included. Read their verification sections against
Chapters~\ref{ch:pyramid} and~\ref{ch:secondsummit} 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{checkpoint}
The book's ending is a beginning, so the final checkpoint is prospective:
you should be able to (1) explain the two acts of verification and why
the second one cannot be delegated to the first; (2) audit a stranger's
attestation --- leaf, cones, exclusions, inclusion proof --- in fifteen
minutes with your own machine's verdict; (3) name the frontier brick
\emph{you} could lay, and what the control repository says a finished
one looks like; and (4) name the next proof you intend to write. The
authors of the companion repositories left the scaffolding up on
purpose.
\end{checkpoint}