\section{The End-to-End Theorem}
\label{sec:theorem}

The solved valuation bounds the context-indexed collecting semantics of the
CFG\@. A forward simulation connects source and graph executions, following
the CompCert methodology~\cite{leroy09}. Report construction then preserves
coverage and gives sound verdicts.

\subparagraph*{From source to graph.}
VIMP has a small-step semantics \isaname{pstep} over configurations
$(r, s, \mathit{frs})$ of a residual command (the code left to execute), a
store, and a frame stack. A
call pushes a frame holding the caller's store and destination and continues
with the callee's body followed by a $\mathit{Restore}$ marker; the marker pops
the frame and combines the stores as in \cref{sec:traces}
(\isaname{pstep}, rules \texttt{Call} and \texttt{RestoreStep}). A call whose
arity does not match, or whose callee is undeclared, is stuck; well-formedness
excludes such programs.

The compiler uses continuations to translate each procedure body into a
procedure-aware CFG\@. A forward simulation matches each source step with graph
steps that reach the same store (\isaname{csim_star}).

A source configuration does not determine a graph node. The residual command can occur in both branches of
\texttt{if (b) \{x = 1;\} else \{x = 1;\}}. The proof therefore annotates every
command of the program with its nodes. The relation
$p, s_0 \vdash (r, s, \mathit{frs}) \rhd v$ (\isaname{at_node}) holds when some
run of the annotated program from $s_0$ reaches an annotated configuration
that erases to $(r, s, \mathit{frs})$, names $v$, and is related to $v$ by the
simulation. In the example, the configuration after either branch is
observed at both branch nodes. The theorem quantifies over every node at which
a configuration is observed.

Combining the simulation with the result of \cref{sec:traces} shows that every
store reached by a finite source execution lies in $\NodeColl$ at a node
related to that execution (\isaname{source_reaches_node_collect}). For the
annotated program, this holds at every node where the execution is observed
(\isaname{csim_point_compile_prog}).

\subparagraph*{From valuation to report.}
The analyzer function \isaname{run_voblint} takes a configuration and a
program. The configuration selects the analyses, the update rule for global
unknowns, the context policy and call-string length, and the placement of
program globals. The function rejects an invalid
configuration or an ill-formed program, and otherwise runs the executable
solver and returns $\ctor{Analysed}~\mathit{res}$ when the solver returns a
result (\isaname{run_voblint}). At each node, the report lists the states
computed for its solved contexts and classifies each check as
\verdict{PROVED}, \verdict{REFUTED}, \verdict{UNKNOWN} (undetermined), or
\verdict{DEAD} (unreachable). The sets $\Report_{\mathit{res}}(v)$ and
$\Verd_{\mathit{res}}(v)$ interpret these states and verdicts as in
\cref{sec:overview}.

In the Isabelle statement below, \texttt{fixes} declares typed parameters,
\texttt{defines} introduces abbreviations, \texttt{assumes} lists premises,
and \texttt{shows} gives the conclusion. Here $\Pi$ is the procedure table of $p$, and
$\Glob, \Pi \vdash (c, s, \mathit{frs}) \rightarrow_p^* (c', s', \mathit{frs}')$
is a finite execution of \isaname{pstep} from residual command $c$, store $s$
and frame stack $\mathit{frs}$. $\NodeColl_{\Glob,g,S}\,v$ is the node
collecting semantics of the compiled graph $g$ from the initial stores $S$.

\begin{theorem}[End-to-end soundness, \isaname{run_voblint_source_sound}]
\label{thm:headline}
\end{theorem}
\vspace{-1.5ex}
\snippet{run_voblint_source_sound}

The theorem assumes an initial store with zero-valued globals and
unconstrained locals, a finite execution from the body of \texttt{main}, and a
returned analyzer report. This includes finite prefixes of nonterminating executions. The reached
configuration is observed at some node; at every such node, its store is
collected, covered by the report, and consistent with every definite verdict.
The proof combines contexts using $\NodeColl(v) = \bigcup_c \ActColl(v, c)$
and \cref{thm:routed}.

Under the configured policy, the report's states for $c$ at $v$ also cover
$\ActColl(v,c)$ (\isaname{run_voblint_context_covers}). The underlying
\isaname{run_voblint_contexts} theorem additionally ensures that every valid
activation trace has an admitted context.

A returned report entails solver termination, program well-formedness, and
coverage via \isaname{live_unknowns_cover}. No separate premises
restrict the accepted configurations.

\subparagraph*{Meaning of verdicts.}
\verdict{PROVED} states that whenever a covered execution reaches the check,
the condition holds; \verdict{REFUTED} that it fails
(\isaname{run_voblint_check_sound}). Neither asserts that the check is
reachable, and \verdict{REFUTED} is not a verified counterexample.
\verdict{DEAD} establishes that the check's node is unreachable (\isaname{run_voblint_dead_check_unreached}). Analogous theorems cover
arithmetic diagnostics. If a node has no diagnostic, divisors in its outgoing
edge expressions and call arguments are nonzero in every collected store
(\isaname{run_voblint_arithmetic_safe}). An error diagnostic establishes
that its divisor is zero in every collected store at that node
(\isaname{run_voblint_arithmetic_refuted}).

\subparagraph*{Trusted components.}
\Cref{fig:trust} separates what is proved from what is trusted. The theorem is
about the constant that Isabelle's code generator~\cite{haftmann10} exports to
OCaml and that the command-line tool calls. The lexer and parser, which
construct the program, and the handwritten OCaml that prints the report lie
outside the proof. The Isabelle kernel, the code generator, the OCaml
toolchain, and the arbitrary-precision integer library Zarith are trusted.
When tracing is requested, the command-line tool calls
\isaname{run_voblint_traced}, which is equal to \isaname{run_voblint} in
Isabelle (\isaname{run_voblint_traced_eq}). Its exported code maps
\isaname{trace_event}, whose logical result is the unit value $()$, to the
handwritten hook \texttt{Solver\_trace\_hook.emit}. The solver, routing
functions, and report construction call this hook. The traced executable
additionally trusts it to return without exceptions and leave the computed
results unchanged; untraced runs do not call it.

We must also justify that \isaname{pstep} models the intended language; the
soundness theorem does not establish this. Some of VIMP's choices differ
from C. Integers are unbounded. Division by zero
yields $0$ and the remainder by zero yields the dividend. Expressions are pure and
total, so operand evaluation order does not affect the values of
\texttt{\&\&} and \texttt{||}. A failed check does not stop
the execution, so a verdict for one check does not depend on an earlier one.
The locals of \texttt{main} start unconstrained, while a callee's locals start
at $0$. \texttt{min}, \texttt{max}, and the nondeterministic input are
built-in calls, and \texttt{main} has no explicit \texttt{return}. A verdict therefore does not always hold for a C program with the
same text.

\begin{figure}[t]
\centering
\begin{tikzpicture}[
  font=\footnotesize,
  part/.style={draw, rounded corners=1pt, align=center, inner sep=3pt},
  zone/.style={draw, rounded corners=3pt, inner sep=4pt},
  arr/.style={-{Stealth[length=1.6mm]}}]
  \node[part, dashed] (par) {lexer, parser};
  \node[part, dashed, above=5mm of par] (src) {source text};
  \node[part, right=8mm of par] (cmp) {compiler};
  \node[part, right=3mm of cmp] (eqs) {equations};
  \node[part, right=3mm of eqs] (slv) {solver};
  \node[part, right=3mm of slv] (rep) {report, verdicts};
  \node[part, dashed, right=8mm of rep] (out) {printing};
  \draw[arr] (src) -- (par); \draw[arr] (par) -- (cmp); \draw[arr] (cmp) -- (eqs);
  \draw[arr] (eqs) -- (slv); \draw[arr] (slv) -- (rep); \draw[arr] (rep) -- (out);
  \begin{scope}[on background layer]
    \node[zone, fill=green!8, fit=(cmp)(rep)] (pz) {};
    \node[zone, dashed, fit=(src)(par)] (uz) {};
    \node[zone, dashed, fit=(out)] (oz) {};
  \end{scope}
  \node[font=\scriptsize, above=1mm of pz.north west, anchor=south west]
    {proved in Isabelle/HOL};
  \node[font=\scriptsize, above=1mm of uz] {unverified};
  \node[font=\scriptsize, above=1mm of oz] {unverified};
  \node[part, dashed, above=11mm of slv, font=\scriptsize] (hook)
    {trace hook (traced runs)};
  \draw[dashed] (hook) -- (slv);
  \coordinate (baseleft) at ($(uz.south west)+(-1mm,0)$);
  \coordinate (baseright) at ($(oz.south east)+(1mm,0)$);
  \path let \p1=(baseleft), \p2=(baseright) in
    node[zone, fill=black!5, minimum width=\x2-\x1, minimum height=7mm,
         anchor=north west, inner sep=0pt] (base) at (baseleft) {};
  \node[font=\footnotesize] at (base.center)
    {trusted: Isabelle kernel $\cdot$ code generator $\cdot$ OCaml toolchain $\cdot$ Zarith};
\end{tikzpicture}
\caption{The trust boundary of the delivered analyzer, for programs for which the
solver terminates. Dashed boxes are handwritten code outside the proof. For traced runs, the solver, routing functions, and report construction
also call a trusted hook, which must return without exceptions and leave their
results unchanged.}
\label{fig:trust}
\end{figure}