Blame for code/notes/src/0307-aeneas-semantics.tex

\documentclass[11pt]{article}
\usepackage{common}
\begin{document}
\notehead{0307}{Aeneas semantics: what a proof of $\neg P$ about translated Rust certifies}{Formal-methods series (0301--0306). Rust (safe subset) $\to$ LLBC $\to$ pure Lean, the \texttt{Result} monad, and the exact logical content of a bug certificate. Companion notebook: \texttt{notebooks/0307-aeneas-semantics.ipynb} (abstract machine versus translation, exhaustive over \texttt{u8}; executed, 20 checks).}

\begin{problem}
\question{If a prover proves the negation of a property of the Lean function Aeneas produced from a Rust function, what has it shown about the Rust program?}
Note 0304 showed that a counterexample is a proof of $\neg S$ for a \emph{closed} statement $S$ about a Lean function. The bug-finding pipeline we want to evaluate applies this to Rust: translate with Charon and Aeneas, state an intended property, try to prove it, and on failure try to prove its negation (the Leanstral~1.5 funnel, vendor-reported, recorded in \cite{lit}). Three things sit between ``the kernel accepted $\neg S$'' and ``the Rust program has a bug'': (i) the translation must \emph{mean} what the Rust program means, including panics, overflow and divergence; (ii) the negation must be of the right closed proposition, because $\neg\forall x.\,(H\to P)$ and $\forall x.\,(H\to\neg P)$ are different claims; (iii) the witnessing input must be reachable from a caller that exists. The answers: a certificate is a proof about the \emph{translated model}; it becomes a bug report exactly modulo (i) the adequacy of the translation and its trusted base and (iii) reachability, and (ii) fixes which statement was proved.
\end{problem}
\stepcounter{section}% the problem box counts as section 1: keeps every \S and notebook cross-reference stable

\section{Notation}
\begin{center}
\begin{tabular}{@{}p{0.36\linewidth}p{0.60\linewidth}@{}}
\toprule
Symbol & Meaning \\ \midrule
$\mathcal M\sem{f}(x)$ & observable outcome of running Rust function $f$ on input $x$ in the abstract machine: $\mathsf{ret}\,v$, $\mathsf{panic}\,e$, or $\mathsf{diverge}$ \\
$\mathcal T(f)\,x$ & the Lean term Aeneas emits for $f$, of type \texttt{Result} $\alpha$ \\
$\mathsf{Result}\;\alpha$ & $\mathsf{ok}\,a\ |\ \mathsf{fail}\,e\ |\ \mathsf{div}$ (success, panic with an error tag, non-termination) \\
$H,\ P$ & precondition and postcondition predicates; $Q(x):=\exists r.\ \mathcal T(f)\,x=\mathsf{ok}\,r\wedge P(x,r)$ \\
$S_H$ & closed statement $\forall x.\ H(x)\to Q(x)$ \\
$W_H=\{x: H(x)\wedge\neg Q(x)\}$ & witness set of $\neg S_H$ \\
$\mathrm{Reach}(g)$ & inputs actually passed to $f$ by the rest of the program $g$ (public entry points) \\
$\mathrm{TCB}$ & what must be trusted besides the Lean kernel: Charon, Aeneas, the Rust semantics modelled, the property's formalisation \\ \bottomrule
\end{tabular}
\end{center}

\section{Derivation}
\subsection{The pipeline and what each stage removes}
Charon extracts from a Rust crate its MIR-derived, typed intermediate form LLBC; Aeneas translates LLBC to a \emph{pure} Lean 4 program and a types file \cite{ho22,rustlean}. Each Rust function becomes a Lean function returning \texttt{Result} $\alpha$ whose three constructors distinguish return, panic and non-termination \cite{rustlean}. Rust's ownership and borrow discipline is used as a \emph{semantic input}: Aeneas removes the heap and aliasing from the model by (a) passing and returning values instead of mutating places, and (b) for a function that returns a mutable borrow, also returning a \emph{backward function} that the caller invokes when the borrow ends to write the final value back to the owner \cite{ho22,scaling}. Loops become recursive functions; traits become structures. Unsafe code, raw pointers, interior mutability and concurrency are outside the supported subset and must be modelled by hand \cite{scaling}; so a certificate says nothing about code that the front end did not translate faithfully.

A worked instance (simplified from ML-KEM in \cite{scaling}): \texttt{fn reduce(x: \&mut u64) \{ let q = (*x * R) >> 32; *x = *x - q * Q; \}} becomes a function \texttt{reduce (x : U64) : Result U64} whose body is a chain of monadic binds, one for every fallible operation (\texttt{x*R}, the shift, \texttt{q*Q}, \texttt{x-z}); the mutable borrow is gone and the new value is returned. Overflow in any step is a \texttt{fail}.

\subsection{The Result monad and why panics must be in the type}
Define
\[
\mathsf{bind}(\mathsf{ok}\,a,f)=f\,a,\qquad \mathsf{bind}(\mathsf{fail}\,e,f)=\mathsf{fail}\,e,\qquad\mathsf{bind}(\mathsf{div},f)=\mathsf{div}.
\]
The monad laws (left identity, right identity, associativity) hold by case analysis on the first argument, so the translation is free to re-associate sequences of fallible steps. \ver{checked on all $256$ values plus three error tags and $\mathsf{div}$: left identity, right identity and associativity hold.}

\textbf{The naive translation fails.} Take the running example (the same one is used through the note)
\[
\texttt{fn avg(a: u8, b: u8) -> u8 \{ (a + b) / 2 \}}
\]
With overflow checks on, the machine panics iff $a+b>255$. A translation that reads $a,b$ as mathematical integers and returns $\mathsf{ok}\,((a+b)/2)$ is total and ``clean'', and it disagrees with the machine on exactly the panicking inputs: $\#\{(a,b):a+b\ge256\}=\sum_{a=1}^{255}a=\tfrac{255\cdot256}2=32640$ of the $65536$ pairs. The correct translation is $\mathcal T(\mathtt{avg})(a,b)=\mathsf{bind}(\mathrm{add}_{u8}(a,b),\ \lambda s.\ \mathsf{ok}(s/2))$ with $\mathrm{add}_{u8}(a,b)=\mathsf{ok}(a+b)$ if $a+b\le255$ else $\mathsf{fail}\ \mathsf{integerOverflow}$. \ver{the naive translation disagrees with the machine on $32640=255\cdot256/2$ inputs, the \texttt{Result} translation on $0$ of $65536$.}

\subsection{Borrow elimination as a commuting diagram}
For \texttt{fn bump(x: \&mut u8) \{ *x += 1 \}} the machine updates a store $\sigma(x)$; the translation is $\mathtt{bump}(x)=\mathrm{add}_{u8}(x,1)$ and the caller rebinds. The claim is the diagram: $\mathcal M$ run on $\sigma=\{x\mapsto v\}$ ends with $\sigma'(x)=v'$ iff $\mathcal T(\mathtt{bump})(v)=\mathsf{ok}\,v'$, and panics iff it is $\mathsf{fail}$ (with the same error tag; the store is unchanged because the write comes after the check). For a function returning a borrow into a vector, $\mathtt{get\_mut}(v,i)=\mathsf{ok}(v[i],\ \mathsf{back})$ with $\mathsf{back}:u8\to\mathrm{Vec}$ the update $v[i:=\cdot]$, or $\mathsf{fail}\ \mathsf{arrayOutOfBounds}$; a caller that does \texttt{*get\_mut(\&mut v,i) += k} translates to $\mathsf{bind}(\mathtt{get\_mut}\,v\,i,\ \lambda(a,\mathsf{back}).\ \mathsf{bind}(\mathrm{add}_{u8}(a,k),\ \lambda n.\ \mathsf{ok}(\mathsf{back}\,n)))$. The order of the binds fixes \emph{which} panic is reported first. \ver{bump: store and outcome equal the translation for all $256$ inputs; returned-borrow case: forward value, backward function and error tag agree with the machine on $1275/1275$ cases (vectors of length $\le3$ over $\{0,1,254,255\}$, $i\le4$, $k\le2$).}

\subsection{Loops and divergence}
A \texttt{while} loop becomes a recursive function; whether it terminates is not decided by the translation. The \texttt{div} constructor models the machine observation ``does not terminate'': for \texttt{while x != 0 \{\}} the machine returns normally iff $x=0$, and for every fuel bound $F$ the fuel-limited machine runs out of fuel iff the translation is $\mathsf{div}$ \ver{agreement on all $256$ inputs and $F\in\{1,10,1000\}$}. A loop with a checked accumulator, \texttt{sum\_to(n)}, panics first at $n=23$ ($22\cdot23/2=253\le255<276=23\cdot24/2$); the recursive translation and the machine agree for every \texttt{u8} input \ver{256 of 256; first panic at $n=23$}. A proof of a property about a possibly-diverging function must either prove termination or accept that $\mathsf{div}$ is not $\mathsf{ok}$: in $Q$ above $\mathsf{div}$ counts as a violation.

\subsection{What a proof of $\neg P$ proves}
\begin{definition}[Adequacy of the translation]
$\mathcal T$ is \emph{adequate} for $f$ if for every $x$: $\mathcal M\sem f(x)=\mathsf{ret}\,v\Rightarrow\mathcal T(f)\,x=\mathsf{ok}\,v$; $\mathcal M\sem f(x)=\mathsf{panic}\,e\Rightarrow\mathcal T(f)\,x=\mathsf{fail}\,e$; $\mathcal M\sem f(x)=\mathsf{diverge}\Rightarrow\mathcal T(f)\,x=\mathsf{div}$ (and conversely, so the three cases are exhaustive and exclusive).
\end{definition}
Adequacy is the content of the translation's correctness theorem; it is a property of the \emph{toolchain} (and of the Rust semantics it formalises), not something the Lean kernel checks for the individual program.

\begin{proposition}[Closed negation]
Let $S_H=\forall x.\,H(x)\to Q(x)$. (a) $\neg S_H\iff\exists x.\,H(x)\wedge\neg Q(x)$ (classically; constructively only the implication $\Leftarrow$, and a witness is extracted only if $H,Q$ are decidable). (b) $\forall x.\,H(x)\to\neg Q(x)$ is strictly stronger than $\neg S_H$ whenever $H$ is satisfiable, and when $H$ is \emph{un}satisfiable it is provable vacuously and carries no evidence. (c) Under adequacy, any $x\in W_H$ is an input on which the Rust function panics, diverges or returns a value violating $P$.
\end{proposition}
\emph{Proof.} (a) De Morgan for the quantifier and the implication. (b) Instantiating a witness of $H$ in $\forall x.H\to\neg Q$ gives $\neg Q$ there, hence $\neg S_H$; the converse fails when $H$ also holds at some $x$ with $Q(x)$ (take $H\equiv\top$ and any function with one good input). If $\neg\exists x.H(x)$ the universal statement is vacuous. (c) By adequacy $\mathcal T(f)\,x$ is $\mathsf{ok}\,r$ with $P(x,r)$ false or is $\mathsf{fail}/\mathsf{div}$ exactly when the machine outcome is the corresponding one. $\square$

\emph{Why the distinction matters here.} A statement ``$\neg P\ x$ for the $x$ in scope'' written under binders is a claim about \emph{every} $x$; a prover that is asked for it either fails (it is false at every good input) or ``succeeds'' vacuously. The right target for a bug search is the closed $\neg\forall$ form (equivalently, an $\exists$ with a witness). For \texttt{avg} with $H\equiv\top$ and $P=$ ``$\min(a,b)\le r\le\max(a,b)$'': $|W|=32640$, the closed statement $S$ is false (first witness $(1,255)$), and the under-binders form $\forall x.\neg Q(x)$ is also false since $Q(0,0)$ holds ($|\{Q\}|=32896$). With $H:=a+b\le255$, $S_H$ is true and no certificate exists. With the unsatisfiable $H:=a+b>255\wedge a+b<256$ the under-binders form holds vacuously and $W=\emptyset$; with the satisfiable $H:=a+b\ge256$ it holds for a real reason and implies $\neg S_H$. \ver{all six statements verified by exhaustion over the $65536$ inputs.}

\subsection{Reachability: a certificate about $f$ is not a bug in the program}
$W_H$ is a set of inputs to $f$ in isolation. The program has a bug only if some $x\in W_H$ can be produced by a public entry point: $W_H\cap\mathrm{Reach}\ne\emptyset$. Example: \texttt{fn mean\_pct(a,b) \{ avg(min(a,c), min(b,c)) \}}. The reachable inputs of \texttt{avg} are $[0,c]^2$ and
\[
|W\cap[0,c]^2|=\sum_{a=0}^{c}\max\{0,\ \min(c,255)-\max(0,256-a)+1\},
\]
which is $0$ for $c\le127$ and $1$ at $c=128$ (the pair $(128,128)$). So the same certificate is a false alarm for $c\le127$ and a real bug for $c\ge128$. \ver{closed form equals brute force at $c\in\{50,100,127,128,150,200,255\}$ ($0,0,0,1,1035,10585,32640$); running \texttt{mean\_pct} on all $65536$ raw input pairs gives $0$ panics for $c=127$, $16384=128^2$ for $c=128$, $29560$ for $c=200$.} The Leanstral report is recorded as attributing most of its false flags to properties that were ``too strong (for instance failing because of a state that was unreachable from the public interface) or malformed'' (my arithmetic from its counts: $11/47=23\%$ of flags genuine, $5/47\approx11\%$ per distinct bug); this section is the mechanism for the first class. A certificate gate therefore has to include a reachability or precondition check and a concrete replay of the witness through the \emph{Rust} program.

\subsection{Translation soundness fails in both directions}
Adequacy has two halves, and each failure gives a different wrong certificate.
\begin{enumerate}[nosep]
\item \emph{Too lax} (unbounded integers; a missed panic). $S$ is provable in the model although the program panics on $32640$ inputs. No certificate for the real bug exists, because the model has no such witness.
\item \emph{A different semantics} (wrapping, as release builds do by default). The witnesses for $P$ are the \emph{same} $32640$ inputs but now because the value is wrong, not because of a panic, and panic-freedom becomes \emph{provable}. ``The bug'' depends on which Rust semantics the translation models; Aeneas models checked arithmetic (failure on overflow) \cite{scaling}.
\item \emph{Too strict} (a spurious \texttt{fail}). For \texttt{((a as u16 + b as u16) / 2) as u8}, which never panics in Rust, a translation that checks the widened add at \texttt{u8} width produces $32640$ spurious witnesses: a ``proof of the negation'' of a true property of the real program.
\end{enumerate}
\ver{exhaustive: (1) $|W|=0$ in the model vs $32640$ in the machine; (2) same witness set, panic-free true under wrapping and false under checked semantics; (3) real program correct on all $65536$ inputs, strict translation fails on $32640$.} The notebook compares machine and translation on a finite domain, which is a \emph{test} of adequacy for these programs. It is not a proof of the toolchain's soundness theorem, and the kernel's acceptance of $\neg S$ says nothing about it.

\subsection{The trusted base of a bug certificate}
A certificate for ``the Rust program has a bug'' needs: the Lean kernel (small), the Lean statement faithfully formalising the intended $H,P$ (spec risk, 0305), Charon's extraction being faithful to rustc's MIR, Aeneas' translation being adequate for the features used (the ICFP paper presents the translation and its semantic justification \cite{ho22}; I have not re-verified a mechanised end-to-end proof for the current tool version, and I treat the toolchain as trusted code), the Rust semantics chosen (overflow, evaluation order of panics), and reachability. Only the first item is checked by the kernel; the rest is why the final step in 0304's protocol is a concrete replay of the witness against the original Rust.

\section{Boxed result}
\begin{result}
\begin{align*}
&\mathsf{Result}\,\alpha=\mathsf{ok}\,\alpha\,|\,\mathsf{fail}\,e\,|\,\mathsf{div};\quad \mathsf{bind}\text{ propagates }\mathsf{fail},\mathsf{div};\quad\&\mathsf{mut}\ \leadsto\ \text{returned value (+ backward fn).}\\
&\neg S_H\iff\exists x.\,H(x)\wedge\neg Q(x);\qquad \forall x.\,H\to\neg Q\ \text{is stronger (and vacuous if $H$ unsatisfiable)}.\\
&\text{real bug}\iff \underbrace{\vdash\neg S_H}_{\text{kernel}}\ \wedge\ \underbrace{\mathcal T\text{ adequate}}_{\text{toolchain}}\ \wedge\ \underbrace{W_H\cap\mathrm{Reach}\neq\emptyset}_{\text{program}}\ \wedge\ \underbrace{H,P\text{ the intended spec}}_{\text{0305}}.
\end{align*}
Running example: $|W|=32640$ of $65536$; $|W\cap[0,c]^2|=0$ for $c\le127$, $1$ at $c=128$.
\end{result}

\section{What breaks}
\begin{breaks}
\begin{tabular}{@{}p{0.27\linewidth}p{0.30\linewidth}p{0.37\linewidth}@{}}
\toprule
Failure & Assumption violated & Consequence \\ \midrule
Negation stated under binders & the proved statement is the closed $\neg\forall$ & unprovable, or vacuously provable when $H$ is unsatisfiable \\
Witness not reachable & $W\cap\mathrm{Reach}\ne\emptyset$ & false alarm: certificate about $f$, not about the program (the dominant flagged-but-not-genuine class in the funnel) \\
Translation too lax (missed overflow) & adequacy, panic half & $S$ provable in the model, real panic exists; the pipeline reports ``correct'' \\
Translation too strict & adequacy, converse half & spurious certificate of $\neg S$ for a correct program \\
Different arithmetic semantics & the machine modelled is the one deployed & wrong-value versus panic; release versus debug builds disagree \\
Unsupported features (unsafe, interior mutability, concurrency) & the function lies in the safe subset & model written by hand; the certificate is about the hand model \cite{scaling} \\
Divergence read as success & $\mathsf{div}\ne\mathsf{ok}$ & termination must be proved or the property must tolerate $\mathsf{div}$ \\
Property formalises the wrong intent & $H,P$ capture the spec & bug in the spec, not the code (0305) \\
Exhaustive agreement mistaken for adequacy & finite test $\ne$ theorem & only the programs and domains tested are covered \\ \bottomrule
\end{tabular}
\end{breaks}

\nextnote{0305 asks the converse question: when the proof of $S$ \emph{succeeds}, how do we know $S$ is the right statement? The same $(H,P)$ that makes a certificate meaningful here is what spec-risk analysis has to validate.}

\begin{thebibliography}{9}
\bibitem{ho22} S.~Ho, J.~Protzenko. Aeneas: Rust verification by functional translation. Proc.\ ACM Program.\ Lang.\ 6(ICFP):711--741, 2022 (as cited in \cite{rustlean}; not re-fetched here).
\bibitem{rustlean} A Rust-to-Lean verification pipeline with AI provers, arXiv:2605.30106, Sec.~2.1 (Charon $\to$ LLBC $\to$ Lean; \texttt{Result} with \texttt{ok}, \texttt{fail}, \texttt{div}; safe-Rust subset); vault note \texttt{a-rust-to-lean-verification-pipeline-with-ai-provers}.
\bibitem{scaling} Scaling verification of cryptographic software with Aeneas, Rust, and Lean, arXiv:2609.15648, Sec.~3 (the \texttt{reduce} example, monadic binds for overflow, backward functions for returned borrows, loops as recursion, unsupported features); vault note \texttt{scaling-verification-of-cryptographic-software-with-aeneas-rust-and-lean}.
\bibitem{lit} \texttt{docs/research/BUGFINDING\_LIT\_REVIEW.md}, Sec.~3.1 (Leanstral~1.5 funnel: 57 repositories, 47 flags, 11 genuine, 5 distinct bugs; vendor-reported, method for ``genuine'' not described).
\end{thebibliography}
\end{document}