\section{From Equations to a Cover}
\label{sec:equations}

The equations follow Goblint's \texttt{Spec} interface~\cite{vojdani16,seidl26}
and side-effecting constraint systems~\cite{seidl03,apinis12}. We show how
sound abstract operations, context routing, and the solver
certificate~\cite{tilscher26} establish the five coverage obligations.

\subsection{The analysis interface}

An analysis describes the stores at a node by an abstract state $d$. The
concretization $\conc(d, \rho)$ is the set of stores it represents,
parameterized by $\rho$, the solved values of the analysis's global unknowns.
We suppress $\rho$ when it plays no role. The
analysis supplies the record \isaname{dg_spec}, the counterpart of Goblint's
\texttt{Spec}: one transfer per kind of edge action, an enter operation, and
two combine operations. A transfer computes an abstract successor state. A call transfer retains the caller's state alongside
the callee's entry state. After the return, the
caller's locals come from before the call, while the globals and the result
come from the callee. Enter therefore returns a list of entry pairs $(q, d)$:
a resume state $q$ describing the caller's store and an entry state $d$
describing the store in which the callee starts. After the return,
\emph{combine\_env} merges the callee's exit state into $q$, taking the
callee's globals, and \emph{combine\_assign} then writes the return value to
the call's destination. Together they mirror the concrete
$\mathit{combine}_e$ of \cref{sec:traces}. A transfer may also publish
contributions, meaning abstract values that must be included in
the analysis's global unknowns. We interpret its output using the join of the
previous global values and these contributions.

The local soundness laws of transfers and combine form the locale
\isaname{analysis_contract}: the concretization is monotone, each transfer
covers every concrete successor store, and combine covers $\mathit{combine}_e(s, t)$
whenever $q$ covers $s$ and the exit state covers $t$. The routing conditions
below require enter to return a pair
covering the caller's store and the entered store
(\isaname{entry_pairs_cover}). Each context policy must satisfy these
conditions, which are separate from \isaname{analysis_contract}. A numeric
domain proves only its abstract operations sound. The framework derives the
transfers once for all domains, following Nipkow and Klein's generic
interpreter~\cite[Sect.~13.5]{nipkow14}. The implemented domains are Sign,
Interval, Parity, Congruence, and Int, a reduced product that combines all four
and propagates information between them.

\subsection{Context-indexed equations and routing}

Write $\sol(v,c)$ for the value assigned to local unknown $(v,c)$ by the
solved valuation. The unknown's right-hand side joins four sources (\isaname{routed_node_rhs_parts}):
\begin{itemize}
  \item the initial state at the program entry;
  \item the transfer along each intraprocedural edge into $v$, in the same
    context $c$;
  \item the combined result of each call returning to $v$;
  \item at a procedure entry, the entry states published to it.
\end{itemize}
At a call, a \emph{routing function} $\mathit{route}$ chooses the callee
context from the call site, the caller context, the entry state and the call.
Consider a call edge $(u, e, \ctor{FunctionEntry}\;p, k)$ in caller context
$c$. For each entry pair $(q, d)$ returned by enter for $\sol(u, c)$, the
continuation's right-hand side includes a contribution
(\isaname{routed_call_alternative_program}). If $d$ is bottom
($\bot$, representing no stores), the
contribution is $\mathit{combine}(q, \bot)$. Otherwise, let
$c' = \mathit{route}(u, c, d, e)$; the contribution is the program
\[
\text{publish } d \text{ to } \mathit{seed}(p, c');\quad
r \leftarrow \text{read } (\ctor{FunctionResult}\;p, c');\quad
\mathit{combine}(q, r).
\]
This program is a sequence of solver operations, not source-language code.
Here $\mathit{seed}(p,c')$ is a global unknown accumulating entry states for
$p$ in $c'$. The entry equation of $(\ctor{FunctionEntry}\;p, c')$ reads it.
In the running example, the call \texttt{bump(5)} in
$c_0$ publishes $n \in [5,5]$ to $\mathit{seed}(\texttt{bump}, [5,5])$, reads
the result of \texttt{bump} in $[5,5]$, and combines it with the resume state
of \texttt{main}. The same equation construction handles recursive calls,
which can introduce cyclic dependencies.

The locale \isaname{routed_context} connects abstract routing to the concrete
policy $\adm$ through adequacy and totality.
\begin{description}
  \item[Adequacy] (\isaname{routing_adequate}). If $\adm$ admits $c'$ for a call
    from a store that the caller's solved state describes, then enter produces
    a pair $(q, d)$ routed to $c'$. The pair's resume state covers the
    caller's store, and its entry state covers the entered store. The
    callee's entry unknown in $c'$ is solved.
  \item[Totality] (\isaname{routing_total}). $\adm$ admits at least one context
    for every call from a store that the caller's solved state describes.
\end{description}
For the unit policy and for call strings, $\adm$ admits exactly the context the
routing function computes from the call site and the caller context. Totality
is then immediate, and adequacy reduces to entry coverage and the routed entry
unknown being solved.

For entry-state contexts, the policy \isaname{routed_entry_context_rel} is
defined from the solved valuation $\sol$:
\[
\adm_{u,c}(e, s, s') \;=\; \{\, \mathit{route}(u, c, d, e) \mid
(q, d) \in \mathit{enter}_e(\sol(u, c)),\; s \in \conc(q),\; s' \in \conc(d) \,\}.
\]
In words, a context is admitted when an entry pair of the solved caller state
covers both concrete stores and is routed there. We first fix $\sol$ and
then define the policy. This policy determines which contexts contain each
store, while their union $\NodeColl$ remains unchanged. \Cref{sec:related} compares this with a posteriori
soundness~\cite{might09}. For entry-state contexts, $\ActColl(v, c)$
therefore depends on the analysis that produced $\sol$.

\begin{table}[t]
\centering
\footnotesize
\begin{tabular}{@{}lp{0.58\textwidth}@{}}
\toprule
Hypothesis & Reading \\
\midrule
\texttt{analysis\_contract} & transfers and combine are sound \\
\texttt{pp} (\texttt{post\_bounded}) & the query is in $W$, and at each unknown of $W$, $\sol$ bounds the right-hand side and every side effect it publishes \\
\texttt{sg\_cov}, \texttt{sg\_uncov} & the cover is $\conc(\sol(v,c), \rho)$ on $W$ and $\emptyset$ elsewhere \\
\texttt{fwd} & an intraprocedural edge from an unknown of $W$ with a non-empty state leads into $W$ \\
\texttt{comb\_fwd} & a call's continuation is in $W$ in the caller's context \\
\texttt{routing\_adequate}, & the policy agrees with the routing \\
\quad\texttt{routing\_total} & \\
\texttt{resolve\_sound} & callee resolution lists every procedure a covered store can call \\
\texttt{calls\_unique} & each call site has one call edge (\isaname{calls_source_unique}) \\
\texttt{is\_bot\_sound}, \texttt{is\_bot\_bot} & a state classified as bottom describes no store, and $\bot$ is classified as bottom \\
\texttt{cmb\_wf}, \texttt{extra\_wf} & the generated call and seed contributions are well-formed programs over unknowns \\
\texttt{finC}, \texttt{finE} & the graph has finitely many edges \\
seed keys & seed unknowns differ from all other global unknowns \\
\bottomrule
\end{tabular}
\caption{Hypotheses of \cref{thm:routed}, stated over a set $W$ of local
unknowns: all assumptions of the locales \isaname{routed_context} and
\isaname{dg_context_activation}. The theorem adds three premises: the program
entry is in $W$ in context $c_0$, the initial state describes the initial
stores under initial global values $\rho_0$, and $\rho_0 \leq \rho$.}
\label{tab:hypotheses}
\end{table}

\begin{theorem}[Routed collecting soundness, \isaname{activation_collect_dg_sound}]
\label{thm:routed}
Under the hypotheses of \cref{tab:hypotheses}, if $(\mathit{entry}_g, c_0) \in W$,
the initial state describes the initial stores under initial global values
$\rho_0$, and $\rho_0 \leq \rho$, then $\ActColl(v, c) \subseteq \cover(v, c)$
for all $v$ and $c$, where $\cover(v, c) = \conc(\sol(v, c), \rho)$ on $W$
and $\emptyset$ elsewhere.
\end{theorem}

The proof checks the five obligations of \cref{thm:contract} for this cover.
The initial state and $\rho_0 \leq \rho$ give \oblig{Init}. The edge
transfers and \texttt{fwd} give \oblig{Intra}. \oblig{Call} follows from adequacy and entry coverage.
\oblig{Return} follows from adequacy and combine soundness.
\oblig{Total} follows from totality. Both bounds of \texttt{pp} are needed because a
value reaches its target unknown as an answer or as a published side effect,
such as an entry state published to a seed.
Here \texttt{calls\_unique} identifies the admitted and returning call edges.

\subsection{The solver certificate}

\Cref{thm:routed} requires closure under execution steps. The verified
top-down solver~\cite{tilscher26} instead provides \isaname{part_post_solution}
for its query $x$, solved set $V$, and result $\sol$. This certificate states
that $x \in V$ and $V$ is closed under right-hand-side reads of local unknowns.
The result $\sol$ bounds the right-hand side and every side effect of each
solved unknown.

The solver works backward from its query, the result of
\texttt{main}, while \cref{thm:routed} follows executions forward from the
entry. The bridge takes $W$ to be the \emph{live} part of $V$: the unknowns $(u, c)$
such that $u$ belongs to a procedure $q$ whose result
$(\ctor{FunctionResult}\;q, c)$ is in $V$ (\isaname{live_unknowns}). The
compiler ends every body with a return edge, so every node of a procedure
reaches the procedure's result through intraprocedural edges and
call-to-continuation steps. The result's right-hand side reads its
predecessors, so closure under reads puts all nodes of a procedure into $V$
once its result is in $V$ in that context.

The same closure argument applies to callees. For a non-bottom routed entry state, $(k,c) \in V$ reads
$(\ctor{FunctionResult}\;p,c')$ (\isaname{sol_vars_callee_result}). The callee's nodes are therefore live in
$c'$, including its entry. If the entry state is bottom, no concrete store enters
the callee, so this case requires no callee coverage.
\isaname{live_unknowns_cover} proves, from a well-formed
program and a completed solver run, that the live set contains the program entry
and satisfies the closure hypotheses of \cref{tab:hypotheses}.

Structural reachability also holds for an activation that never returns, because the argument follows the equations, not executions.
\Cref{thm:routed} applies to the live subset $W$ of the solved unknowns $V$.
The report publishes the states associated with all unknowns in $V$, so it
can include more states than the proof requires. This preserves soundness
because the report only has to contain the cover.

The rest of the proof never inspects the solver. The analysis locale takes it
as a parameter with four assumptions (\isaname{certified_solver}). A run
satisfying its domain predicate, which identifies terminating inputs, yields
\isaname{part_post_solution} and a finite solved set. A returned executable
run lies in that domain and agrees with the logical solver. These facts are proved for the vendored solver under each of its five
update rules for global unknowns (\isaname{td_certified_solver}). An update
rule decides how contributions to a global unknown accumulate: by join, by
join per contributing right-hand side, or by \emph{warrowing}, which combines
widening and narrowing~\cite{tilscher26}. Any solver satisfying this
certificate can reuse the same semantic
soundness proof.