verifying-crypto-with-lean/chapters/ch08-rust-to-lean.tex

\chapter{From Rust to Lean: Verifying the Code That Actually Ships}
\label{ch:rust}

\section{The transcription problem}

Everything so far proved facts about \emph{Lean} programs. But the Ed25519
that guards your SSH connection is written in \emph{Rust} (in our case,
\code{curve25519-dalek} and its forks). An obvious plan: read the Rust,
rewrite it in Lean by hand, verify the rewrite. The plan has a hole you could
drive a key-recovery attack through: \textbf{what if you transcribe it
wrong?} A hand-copy that silently fixes a bug --- or introduces one --- makes
the proof a beautiful statement about code nobody runs.

The projects behind this book close the hole with a mechanical translation
pipeline:

\begin{center}
\begin{tikzpicture}[
  stage/.style={draw=ink2,thick,rounded corners=3pt,align=center,
                minimum height=1.15cm,minimum width=2.5cm,font=\small},
  arr/.style={-{Stealth},thick,ink2},
  lbl/.style={font=\scriptsize\color{ink2},midway,above}
]
  \node[stage,fill=codebg]     (rust)  at (0,0)    {\textbf{Rust source}\\ \code{field.rs}};
  \node[stage,fill=warnsoft]   (llbc)  at (4.0,0)  {\textbf{LLBC}\\ intermediate form};
  \node[stage,fill=provensoft] (model) at (8.0,0)  {\textbf{Lean model}\\ \code{gen/Funs.lean}};
  \node[stage,fill=accentsoft] (proof) at (12.0,0) {\textbf{Your proofs}\\ \code{Proofs/*.lean}};
  \draw[arr] (rust)  -- node[lbl]{Charon}  (llbc);
  \draw[arr] (llbc)  -- node[lbl]{Aeneas}  (model);
  \draw[arr] (model) -- node[lbl]{you}     (proof);
  \node[font=\scriptsize\color{ink2},align=center] at (6.0,-1.15)
    {machine-generated, never hand-edited \hspace{2.2cm} human-written, kernel-checked};
\end{tikzpicture}
\end{center}

\textbf{Charon} compiles the Rust crate into LLBC (``low-level borrow
calculus''), a simplified intermediate representation. \textbf{Aeneas}
translates LLBC into pure Lean functions. The generated Lean --- the
\emph{model} --- lands in a \code{gen/} directory with a strict house rule:
\emph{never edit it}. Regenerate it from source, or don't touch it. Your
proofs import the model and state theorems about it.

\begin{bigidea}
The object of verification is the \textbf{extracted model}, produced from
the shipping source by a deterministic tool --- not a human transcription.
The trust question shifts from ``did we copy the code right?'' (unauditable
squinting) to ``does the translator preserve meaning?'' (one tool, studied
once, shared by every project that uses it). You will hear this called
\emph{shrinking the trusted base}: swap many ad-hoc trusts for one
well-examined trust.
\end{bigidea}

\section{What extracted code looks like}

Here is real input and real output, lightly abridged. The Rust (from
\code{curve25519-dalek}, radix-51 field addition):

\begin{lstlisting}[language=RustL]
impl Add for FieldElement51 {
    fn add(self, rhs: &FieldElement51) -> FieldElement51 {
        let mut output = *self;
        for i in 0..5 {
            output.0[i] += rhs.0[i];
        }
        output
    }
}
\end{lstlisting}

And the Lean model Aeneas produces for it (shape, not verbatim):

\begin{lstlisting}[language=Lean]
def fieldElement51_add (self rhs : Array U64 5) :
    Result (Array U64 5) := do
  let a0 <- Array.index_usize self 0
  let b0 <- Array.index_usize rhs 0
  let s0 <- a0 + b0            -- U64 addition: can FAIL on overflow
  let out <- Array.update self 0 s0
  ...                          -- and so on for limbs 1..4
\end{lstlisting}

Three features deserve your full attention, because every proof in the next
two chapters engages them:

\begin{itemize}[leftmargin=1.4em]
\item \textbf{Machine integers are honest.} \lean{U64} is not $\N$; it is
  64-bit words. Aeneas models arithmetic on them precisely, overflow
  included.
\item \textbf{Everything returns \lean{Result}.} The \lean{do}/\lean{<-}
  notation threads a computation that can \emph{fail} --- returning an error
  value instead of a result --- exactly where the Rust could panic or
  overflow. There is no pretending partial functions are total.
\item \textbf{It is ugly.} Five limbs times load-add-store, all sequenced.
  Machine-generated code has no taste. The \emph{proofs} restore the
  elegance; the model's job is fidelity.
\end{itemize}

\section{Overflow is a proof obligation, not a footnote}

In Rust, \rust{a + b} on \rust{u64} panics in debug mode and wraps in
release mode when it overflows. In the extracted model, \lean{a + b}
returns a \lean{Result} that is an error unless the mathematical sum fits.
So the innocent theorem ``add returns the right field element'' \emph{cannot
even be stated} without first proving \emph{add returns at all}:

\begin{lstlisting}[language=Lean]
theorem add_spec (a b : Array U64 5)
    (ha : LimbsBounded a) (hb : LimbsBounded b) :
    ∃ c, fieldElement51_add a b = .ok c ∧ LimbsBounded c ∧ ...
\end{lstlisting}

That hypothesis \lean{LimbsBounded} --- each limb below $2^{54}$, say --- is
the bounds invariant promised in Chapters~\ref{ch:pat}
and~\ref{ch:modular}: 51-bit payload plus headroom, so limb additions cannot
reach $2^{64}$. The specification exposes what the Rust comments only
whisper: this code is correct \emph{under a discipline of bounded inputs},
the discipline must be maintained by every caller, and now there is a
machine checking that it is.

\begin{worked}{running the extracted model by hand, at the envelope's edge}
Trace the extracted \lean{fieldElement51_add} on paper twice --- once
safely inside the operating envelope, once outside --- and watch the
\lean{Result} machinery earn its keep. The model threads every step
through \lean{Result}: a step either produces \lean{.ok v} and the
\lean{do}-block continues, or produces an error and everything after it
is skipped (short-circuit).

\emph{Run 1 --- the worst legal input.} Take both arguments at the very
edge of the bounds discipline: every limb of both inputs equal to
$2^{54} - 1$ (the maximum the invariant \lean{LimbsBounded} admits).
Limb $0$:
\[
s_0 = (2^{54}-1) + (2^{54}-1) = 2^{55} - 2 \;<\; 2^{64}. \quad
\text{\lean{.ok} --- continue.}
\]
Same for limbs $1$--$4$; the block reaches its end and returns
\lean{.ok} of the array with every limb $2^{55}-2$. Note the output
\emph{exceeds} $2^{54}$: addition legitimately leaves the input envelope,
which is why the spec's conclusion states the \emph{wider} bound
$< 2^{55}$ --- bounds flow through operations, and every theorem must say
where they land. Nothing is failing here; the envelope is simply moving.

\emph{Run 2 --- one step past the cliff.} Now feed limbs of $2^{63}$
(representable in a \lean{U64}, but far outside the invariant):
\[
s_0 = 2^{63} + 2^{63} = 2^{64}
\;\not<\; 2^{64}
\quad\Longrightarrow\quad \text{the addition returns an error.}
\]
The \lean{do}-block short-circuits: limbs $1$--$4$ never execute, and the
whole function returns the failure --- in Rust terms, this is the input on
which the release build would have \emph{silently wrapped} to $0$ and kept
going. The model turned undefined-ish behavior into a visible, provable
event. Now reread the spec with both runs in mind: the hypotheses
\lean{LimbsBounded a}/\lean{LimbsBounded b} are exactly the promise that
run 2 cannot happen, and the conclusion \lean{∃ c, ... = .ok c} is
exactly the payoff. One theorem, and the wrap-around is not ``probably
absent'' but \emph{impossible for every input the discipline admits}.
\end{worked}

\begin{aha}
Notice what just happened to ``ugly generated code with Results
everywhere'': it forced us to discover, state, and prove the \emph{implicit
operating envelope} of the optimized implementation. The dalek authors knew
this envelope; it lived in comments and code-review lore. Now it is a
theorem. Extraction does not merely enable verification --- it
\emph{interrogates} the code.
\end{aha}

\section{Practicalities: extraction as surgery}

Running Charon on a whole real-world crate drags in everything the crate
touches --- iterators, byte serialization, trait machinery, SIMD backends
--- much of it irrelevant to the arithmetic core and some of it beyond what
the translator supports. The working method, learned the honest way in the
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
  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
  version is a \emph{different model}; reproducibility of the proofs starts
  with reproducibility of the artifact under proof.
\end{itemize}

\begin{worked}{sizing an extraction --- the surgery, quantified}
``Extract functions, not crates'' sounds like taste; it is arithmetic,
and the numbers from the actual scalar-layer extraction of
\code{dalek-ed25519-verified} make it vivid. First attempt: point Charon
at the \code{Scalar} type wholesale. The dependency closure dragged in
the byte-serialization path (\rust{from_bytes}: shifts, masks, and a
\rust{wrapping_shr} on a signed type), the iterator machinery behind a
zip-reverse-fold (\code{IterMut}, \code{Chunks}, three trait
instantiations each), and the high-level wrapper's trait impls ---
roughly a \emph{thousand} generated definitions, several using features
at the translator's edge, every one of them something a proof might have
to step around. Second attempt: name exactly the arithmetic roots ---
\code{Scalar52::add}, \code{sub}, \code{mul_internal},
\code{montgomery_reduce}, and their constants --- and the generated
model is \emph{28 definitions}, every one arithmetic, every one
provable. Do the auditor's division: $28/1000$ --- the surgery cut
$97\%$ of the material a reader would otherwise have to trust-or-verify.
The lesson generalizes beyond this pipeline: \textbf{the size of the
thing you verify is a design variable}, and an hour spent narrowing
extraction roots buys weeks of not proving lemmas about iterator
adapters. (The one-sentence version for your future code reviews:
verification pressure flows backwards into interface design ---
arithmetic kernels with narrow waists get verified; grand unified
objects do not.)
\end{worked}

\begin{pitfall}
When an extraction fails or a model looks bizarre, the temptation is to
``fix'' the generated Lean by hand. Resist absolutely. A hand-edited model
is a hand-transcription with extra steps --- the exact hole this pipeline
exists to close. The fixes live in extraction scope (choose different
roots), in the source (rarely), or in documented assumptions (openly).
\end{pitfall}

\begin{tryit}
Open the companion repo \code{dalek-ed25519-verified}: read
\code{extract.sh} (the roots), skim \code{verification/gen/Funs.lean} for
\code{add}/\code{sub} (recognize the load-add-store pattern above), then
read the first twenty lines of \code{verification/Proofs/FieldSpec.lean}
and identify: the bounds invariant, the \lean{Result} handling, and the
statement of the theorem. You now recognize every structural element. The
mathematics inside is Chapters~\ref{ch:denotation} and~\ref{ch:field}.
\end{tryit}

\section*{Exercises}

\exercise{The Rust expression \rust{output.0[i] += rhs.0[i]} hides four
distinct failure/effect points that the Lean model makes explicit. Name
them. (Hint: two indexings, one arithmetic operation, one write.)}

\exercise{Suppose limbs are bounded by $2^{54}$. What is the largest value
\lean{a0 + b0} can take, and how many such additions can chain before a
\lean{U64} overflow becomes possible? Show the margin calculation --- this
is precisely why the invariant is $2^{54}$ and not $2^{63}$.}

\exercise{(Design) Your colleague proposes verifying a hand-written Lean
``reference implementation'' instead of the extracted model, because it is
prettier. List two failure modes this reintroduces, and one legitimate use a
reference implementation still has (hint: Chapter~\ref{ch:denotation} uses
one as the \emph{specification} side).}

\section*{Solutions and pathways}
\solutionsintro

\solhead{8.1}
\pathway Expand the sugared Rust into its elementary operations, in
evaluation order, and ask of each: can this one panic, wrap, or write?
\answer In order: (1) \emph{index read} \rust{rhs.0[i]} --- can panic if
$i$ is out of bounds (here the loop guarantees $i < 5$, and the model
makes even that guarantee a visible \lean{Result} on
\lean{Array.index_usize}); (2) \emph{index read} \rust{output.0[i]} ---
same; (3) \emph{the addition} --- can overflow the \lean{U64}: the
failure point the worked example walked off; (4) \emph{the write-back}
into \rust{output.0[i]} --- an effect the pure model represents as
\lean{Array.update}, producing a \emph{new} array value (functional
update). Four operations, three failure modes, one effect --- all hidden
inside \rust{+=} and all explicit in the extracted model, which is
precisely why the model is provable and the sugar is not.

\solhead{8.2}
\pathway Maximize under the hypothesis, then chain: after $k$ additions
without reduction, limbs can approach $k$ times the single-input bound;
find where that crosses $2^{64}$.
\answer Largest single sum: $s_0 = 2 \cdot (2^{54}-1) = 2^{55}-2$.
Chaining: adding $k$ inputs all bounded by $2^{54}$ yields limbs
$< k \cdot 2^{54}$; the \lean{U64} cliff sits where
$k \cdot 2^{54} \ge 2^{64}$, i.e.\ $k = 2^{10} = 1024$ chained additions.
The margin calculation behind ``$2^{54}$, not $2^{63}$'': the invariant
must survive \emph{multiplication}, whose column sums need
$5 \cdot (\text{bound})^2 < 2^{128}$ (the Chapter~\ref{ch:automation}
worked example: $5 \cdot 2^{108} < 2^{111}$, seventeen bits spare). A
$2^{63}$ bound would give $5 \cdot 2^{126} > 2^{128}$ --- overflow. So
the number $54$ is set by the \emph{quadratic} consumer of the bound, not
the linear one, and the addition headroom ($1024$ chained adds) is what
falls out, not what was aimed for. Real invariants are negotiated
between operations; the spec records the treaty.

\solhead{8.3}
\pathway For failure modes, ask what the mechanical pipeline was bought
to eliminate. For the legitimate use, ask what role \emph{wants} to be
clean and human-readable rather than faithful to machine details.
\answer Two reintroduced failure modes: (1) \emph{transcription drift} ---
the hand-model quietly fixes, or introduces, an off-by-one the Rust does
not have, and the proof certifies the wrong artifact (the exact hole the
pipeline closes); (2) \emph{staleness} --- the Rust moves on (a rebase,
an optimization), nobody re-syncs the hand-model, and the certificate
silently detaches from the shipping code; extraction fails loudly
instead. One legitimate use: as the \emph{specification} --- the clean,
obviously-correct definition (schoolbook arithmetic over $\Fp$, ideal
group law) that the ugly extracted model is proven \emph{equal to}. The
reference implementation's prettiness is a liability in the role of
``thing verified'' and an asset in the role of ``thing verified
against'' --- one sentence worth keeping for every verification design
review you ever attend.

\begin{checkpoint}
You should now be able to: draw the Rust $\to$ LLBC $\to$ Lean pipeline and
say what each stage preserves; explain why generated models are never
hand-edited; read a \lean{Result}-typed extracted function and point to
where overflow lives; and state why ``the proof needs a bounds hypothesis''
is a discovery about the \emph{code}, not a weakness of the method.
\end{checkpoint}