\section{Mechanization}
\label{sec:mechanization}

\Cref{tab:scale} lists the size of the development~\cite{voblint} by layer. The development reuses part of the verified
solver of Tilscher et al.~\cite{tilscher26}. The solver is vendored with four
changes made for this work and proposed upstream. They restore the build
under Isabelle2025-2, remove from the widening and narrowing classes the
stabilization assumptions, which require update sequences to stop changing
and are used only in termination proofs, rename clashing
names, and add facts such as \isaname{solve_dom_of_solve_c}. None changes the
algorithm.
Neither Voblint nor the imported solver theories contain \texttt{sorry} or
\texttt{oops}, commands that admit or abandon a proof. Code generation emits \stat{generated_ocaml} lines of OCaml. The handwritten
OCaml implementation contains \stat{handwritten_ocaml} lines for parsing,
report printing, and the trace hook.

\begin{table}[t]
\centering
\scriptsize
\input{generated/scale}
\caption{Size of the development by layer: lines of Isabelle/HOL including
comments, and proved statements, which are \texttt{lemma}, \texttt{theorem}
and \texttt{corollary} commands. The counts exclude one theory generated from
the grammar manifest (\texttt{VIMP\_Grammar\_Generated}).}
\label{tab:scale}
\end{table}

\subparagraph*{Design choices and their alternatives.}
Besides the relational context policy (\cref{sec:traces}) and the solver
as a parameter (\cref{sec:equations}), two choices shaped the proof.
\begin{itemize}
  \item \emph{Activation traces as the soundness target.} A first prototype
    used whole-program executions with calls inlined. The prototype's proof spliced
    a callee execution into the caller's run, which was hard to extend to
    recursion. An unimplemented alternative would annotate graph-semantics
    stack frames with ghost contexts and maintain an invariant over the stack.
    With activation traces, the invariant concerns the caller chain recovered
    by $\mathit{caller\_of}$; contexts remain a separate policy parameter.
  \item \emph{Two-default executable states.} Soundness is stated over total
    functions on variable names; the solver runs on a quotient
    type~\cite{huffman13} of a finite override list with separate defaults
    for locals and zero-initialized globals. The list stores exceptions to
    the defaults; the quotient identifies representations of the same function
    (\isaname{exec_local_spec_sound}). Separate defaults refine the single
    default of Concrete Semantics~\cite[§13.6]{nipkow14}.
\end{itemize}

\subparagraph*{Feedback on the proof assistant.}
Connecting the executable solver to its logical definition required a
separate proof. Functions in Isabelle/HOL are total, so the potentially
diverging solver has a domain predicate. For a terminating execution, we must
show that the logical solver is defined. The added lemma
\isaname{solve_dom_of_solve_c} establishes this implication.
Code generation also turns finite sets and maps into lists that every
lookup scans, and CPU profiles attribute most of the solving time to these scans.
Replacing these list representations through the Containers library is a
possible optimization that we have not evaluated.