papers/zoo-gpu-evm/sections/05-formal-verification.tex

\section{Formal Verification}

\label{sec:formal}

All core properties are mechanically verified in Lean~4 (\texttt{GPU/EVMScaling.lean}).

\begin{theorem}[\texttt{linear\_scaling}]
\label{thm:formal-linear}
For independent set $I$ with $|I| = n$ and $p$ parallel units ($1 \leq p \leq n$):
\begin{equation}
\frac{\Theta(p)}{\Theta(1)} \geq \frac{p}{1 + (p-1) \cdot f}
\end{equation}
Proof by induction on $p$, showing each additional SM contributes positive marginal throughput for $f < 1$.
\end{theorem}

\begin{theorem}[\texttt{amdahl\_bound}]
\label{thm:formal-amdahl}
\begin{equation}
S(p) \leq \frac{1}{f} \quad \forall\, p \geq 1
\end{equation}
Proof constructs $\lim_{p \to \infty} S(p) = 1/f$ from Equation~\ref{eq:amdahl} and shows monotonicity.
\end{theorem}

\begin{theorem}[\texttt{deterministic\_reexecution}]
\label{thm:formal-deterministic}
For any two valid partitions $(I_1, C_1)$ and $(I_2, C_2)$ of $T$:
\begin{equation}
\sigma_{\text{post}}(I_1, C_1) = \sigma_{\text{post}}(I_2, C_2)
\end{equation}
Decomposed into three lemmas: \texttt{disjoint\_writes\_commute}, \texttt{sequential\_canonical}, and \texttt{merge\_equivalence}.
\end{theorem}

\begin{table}[h]
\centering
\begin{tabular}{lcc}
\toprule
\textbf{Theorem} & \textbf{Lines} & \textbf{Check Time} \\
\midrule
\texttt{linear\_scaling} & 142 & 3.2s \\
\texttt{amdahl\_bound} & 87 & 1.8s \\
\texttt{deterministic\_reexecution} & 231 & 5.7s \\
\texttt{disjoint\_writes\_commute} & 64 & 1.1s \\
\texttt{sequential\_canonical} & 48 & 0.9s \\
\texttt{merge\_equivalence} & 119 & 2.8s \\
\midrule
\textbf{Total} & \textbf{691} & \textbf{15.5s} \\
\bottomrule
\end{tabular}
\caption{Lean~4 proof statistics}
\label{tab:proofs}
\end{table}

%% ---------------------------------------------------------------------------