Theory Voblint
section ‹Voblint: a verified abstract interpreter for VIMP›
theory Voblint
imports
"Voblint_Examples_Sign.Exec_Sign_DG_Run"
Example_End_To_End_Certificate
"Voblint_Examples_Sign.Example_Sign_DG_CallString_K2"
"Voblint_Examples_Interval.Example_Interval_Source_Ctx"
"Voblint_Examples_Relational.Example_Relational_DG_Demo"
"Voblint_Examples_Parity.Example_Parity_DG_Flagship"
"Voblint_Examples_Congruence.Example_Congruence_DG_Run"
"Voblint_Examples_Int.Exec_Int_DG_Run"
"Voblint_Examples_Tooling.Example_Update_Rule_Steps"
"Voblint_Examples_Tooling.Example_Per_Origin_Widening_Precision"
begin
text ‹
▩‹
____ ____ ___. .__ .__ __
\ \ / /___\_ |__ | | |__| _____/ |_
\ Y / _ \| __ \| | | |/ \ __\
\ ( <_> ) \_\ \ |_| | | \ |
\___/ \____/|___ /____/__|___| /__|
\/ \/
›
›
section ‹Certified pipeline›
text ‹
❙‹What this development proves.› An end-to-end soundness proof for a Goblint-style abstract
interpreter for VIMP, machine-checked from the source operational semantics to the
∗‹computed› analysis result. The whole pipeline, each arrow a theorem:
▩‹
source execution
-> procedure-aware CFG execution
-> activation trace
-> collecting semantics
-> D/G equation system
-> verified side-effecting solver
-> abstract post-solution
-> source-level soundness
›
Each arrow is justified independently. Compiler simulation preserves source
behavior. Forgetful trace projections introduce no abstract states. Transfer,
join, routing, and widening occur only on the abstract side and are justified by
containment in the corresponding concretization.
❙‹Where the chain ends.› At the operation the CLI actually calls and code
generation actually exports, not at an internal solved system.
@{thm [source] run_voblint_source_sound}, in
\<^theory>‹Voblint_CLI.Analysis_Certified›, says: run the source program, stop
wherever you like, and ask any configuration --- a list of active analyses, a global
update rule, a context policy and a placement of program globals --- for a report.
There is a graph node and frame stack for where you stopped, some state the report
holds at that node describes your store, and every definite verdict the report gives
there holds of that store.
Under a context policy the report holds one state per point ∗‹and› context. A
store reaching a point then lies in the state filed under at least one context its
own call history is admitted at --- exactly one for a call string, possibly several
under entry-state routing; quantifying over every covered context would be false,
since another activation's state need not describe this store. Joining the states
of all contexts at the node gives one state that does describe it
(@{thm [source] run_voblint_source_sound_joined}), at the price of precision.
A caller owes nothing beyond the answer itself. \<^const>‹run_voblint› solves with the
executable solver, which answers only where the solve terminates, so an analysed
answer carries termination; coverage of the solve follows from the solve, and a
malformed program answers ‹Malformed_Program›. The context policy is read in one
function, \<^const>‹analysis_report_of›, and its soundness is proved by one case split.
\<^theory>‹Voblint_Examples.Example_End_To_End_Certificate› is that theorem
with nothing left to assume. It fixes one program at the product domain, a
call-string context of length one and always-join globals, evaluates
the answer, builds the source run step by step, and reads the listed
\<^const>‹Check_Proved› check off the conclusion.
›
section ‹Flagship theorems›
text ‹
Each theory cited here compiles a source program, generates its D/G equation system,
∗‹computes› a solution with the verified solver (‹by eval›), and proves a soundness
theorem about that computed result. The session READMEs carry each family's full witness
inventory; this index names only the headline results along three axes: which domain, which
context policy, and how far the product domain's components refine each other.
›
subsection ‹One domain, the whole pipeline, monovariant›
text ‹
One flagship per selectable domain, all on the same generator and vendored solver. Only
the lattice differs.
▪ @{thm [source] flagship_source_run_sound}
(\<^theory>‹Voblint_Examples_Interval.Example_Interval_DG_Flagship›) bounds actual source
runs of an interval counting loop.
▪ @{thm [source] dgEx_source_run_sound}
(\<^theory>‹Voblint_Examples_Sign.Exec_Sign_DG_Run›) is the same bound for Sign, solved
with the always-join update rule.
▪ @{thm [source] parity_source_run_sound}
(\<^theory>‹Voblint_Examples_Parity.Example_Parity_DG_Flagship›) is the Parity instance on
an even-step loop.
▪ \<^theory>‹Voblint_Examples_Congruence.Example_Congruence_DG_Run› computes exact residue
classes at the exit of a straight-line program.
▪ \<^theory>‹Voblint_Examples_Int.Exec_Int_DG_Run› runs the reduced product of Sign,
Interval, Parity and Congruence. @{thm [source] dgExI_never_ne_once} separates
\<^const>‹Refine_Never›, which narrows only the Parity and Congruence components, from
\<^const>‹Refine_Once›, whose one reduction round reaches the exact singleton. Refinement
is legal because \<^const>‹int_reduction_step› preserves the concretization while
descending the order.
›
subsection ‹Context sensitivity: three storage policies for one axis›
text ‹
All three are certified against the same activation-indexed semantics, bounding
\<^const>‹activation_collect› at every ‹(node, context)› pair. They differ only in what a
context ∗‹is›.
▪ ❙‹Monovariant.› @{thm [source] twice_source_run_sound} analyses ‹twice›, whose single
procedure is called from two sites with different arguments, under one shared entry state.
▪ ❙‹Entry state›, the entered abstract value of the callee's formals (Seidl et al.,
∗‹Mixed Flow-Sensitive Static Analysis›, FM 2026, Example 8).
@{thm [source] twice_activation_collect_sound} keeps the two calls of ‹twice› in the
distinct contexts ‹[3,3]› and ‹[10,10]›, where the monovariant baseline joins them;
\<^theory>‹Voblint_Examples_Interval.Example_Interval_Source_Ctx› lifts that bound to
source runs at each activation's own context.
▪ ❙‹Call string›, a bounded record of the call sites that led to the activation
(FM 2026, Example 7). @{thm [source] sign_nest_1_activation_collect_sound} and
@{thm [source] sign_nest_2_activation_collect_sound} run one ‹nest› program at
‹k = 1› and ‹k = 2›; on Sign, whose computed solution is exact,
@{thm [source] sign_k2_strictly_more_precise_than_k1_at_g} shows the longer string
strictly more precise at ‹g›'s entry.
›
subsection ‹Checks›
text ‹
A compiled ‹__voblint_check(...)› condition gets one verdict per report:
@{thm [source] run_voblint_proved} and @{thm [source] run_voblint_refuted} state what a
‹PROVED› and a ‹REFUTED› verdict guarantee at every reachable store. The regression
corpus pins the verdicts themselves, one proved, one refuted and one unknown check per
domain, e.g. ▩‹tests/regression/05-checks/precision/04-guarded_interval_trio.vimp›,
and a bound Interval proves while Sign cannot
(▩‹07-sign-precision/known-imprecision/03-guard_bound_needs_magnitude.vimp›).
›
subsection ‹Activation-trace concrete semantics›
text ‹
\<^const>‹valid_activation_trace› represents one procedure activation and its ancestry.
\<^const>‹Root› starts main, \<^const>‹Call› records an immediate caller, and
\<^const>‹Resume› continues that caller after its callee reaches the matching
result node. Structural caller links distinguish nested and recursive activations
without placing an unbounded stack in CFG nodes.
\<^const>‹node_collect› forgets the activation structure and collects stores by
node, while \<^const>‹activation_collect› keys the same collection by the
structural activation context. Both contain only stores from valid activation traces.
›
subsection ‹Procedure-aware source and CFG›
text ‹
Procedures receive fresh local state and inherited globals. A call frame stores
the caller state and optional destination. Explicit return enters unwinding,
which skips the remaining commands in that activation and resumes the immediate
caller. Main has no caller and accepted programs therefore require it to terminate
by ordinary fall-through.
CFGs use explicit \<^const>‹FunctionEntry› and \<^const>‹FunctionResult› nodes.
The \<^const>‹intra› relation carries local transfers and matching returns. The
\<^const>‹calls› relation carries call-site, callee-entry, and continuation data.
Compiler certificates expose the node ownership and range separation needed by
the source/CFG simulation.
›
subsection ‹Equations, D/G routing, and solver›
text ‹
Every node equation joins ordinary predecessor flow, callee-entry flow, and
caller/callee combination. Executable equations and their soundness proof use
the same contribution families.
The D/G interface separates local flow-sensitive facts from information published
through global side effects. Analyses choose the two carriers, routing operations,
and context keys. Every domain instance --- Sign, Interval, Parity, the ▩‹int_dom›
product, and the relational carrier --- shares the one verified side-effecting top-down
solver and the one collecting-soundness infrastructure.
›
subsection ‹Executable witnesses›
text ‹
The interval and Sign flagships compile source programs, generate their D/G
equations, execute the verified solver, and certify the computed post-solutions.
The ‹twice› program calls one procedure from two sites; its activation-sensitive
interval analysis keeps the two call contexts separate. Recursive examples test
structural activation nesting independently of that repeated-call witness.
The exported analyser returns its solved result as data; the text report, GraphViz
drawings and report pages are built from that data outside this development, so no
rendering is part of any soundness claim.
❙‹How the development is laid out.› One Isabelle session per architectural
layer, and the ROOT graph is what keeps the layering honest: a theory cannot reach
past its session's declared ancestors, so a boundary claimed in prose is also
enforced by the build. ▩‹Voblint_CFG› never sees the compiler, which is why every
D/G soundness endpoint below holds for an arbitrary CFG rather than only for a
compiled one; ▩‹Voblint_Solver› never sees a CFG; ▩‹Voblint_Framework› never sees a
concrete domain.
Two layers are families rather than single sessions. Every abstract domain has its
own analysis session over the shared ▩‹Analyses/Shared/› chain --- Sign, Interval,
Parity, Congruence, the ▩‹int_dom› product, and the relational carrier --- and its
own example session over that, so a domain's witnesses cannot quietly depend on a
sibling domain. ▩‹Voblint_CLI› is where they meet again, because the dispatcher has
to see all of them, and a downstream codegen session exports it. This theory is the
most downstream file in the development: it imports the CLI and every flagship, so
anything it names has actually been built.
The index below separates the proof spine from executable frontends and research
witnesses.
❙‹1. Language.› VIMP syntax, small-step semantics, and the procedural extension
(scopes, calls, restores).
▪ @{theory Voblint_VIMP.VIMP_Syntax} --- AST, variable names, countability.
▪ @{theory Voblint_VIMP.VIMP_Expr} --- expression evaluation and small-step semantics.
▪ @{theory Voblint_VIMP.VIMP_Globals} --- global variable names and initial store.
▪ @{theory Voblint_VIMP.VIMP_Proc} --- procedural extension: ▩‹Scope›, ▩‹Call›, ▩‹Restore›.
▪ @{theory Voblint_VIMP.VIMP_Notation} --- ▩‹γ (...)› quotation bracket for examples.
❙‹2. Control-flow graph and concrete semantics.› CFG construction, transfer primitives, and
the activation trace semantics it carries.
▪ @{theory Voblint_CFG.CFG_Def} --- CFG node and edge types,
predecessor enumeration, and finite code lists.
▪ @{theory Voblint_Compile.VIMP_Proc_to_CFG} ---
▩‹compile_prog›, from VIMP programs to
interprocedural CFGs.
▪ @{theory Voblint_CFG.CFG_Transfer} --- concrete store
transformers shared by the semantics:
▩‹edge_step›, ▩‹edge_collect›,
▩‹edges_collect›,
▩‹combine_collect›, and
▩‹call_enter_store›.
▪ @{theory Voblint_CFG.Activation_Trace_Def} --- the call-structured
activation trace \<^const>‹valid_activation_trace›
(▩‹Root›/▩‹Call›/
▩‹Resume›), the \<^const>‹node_collect› and
\<^const>‹activation_collect› projections, and the
\<^locale>‹activation_coverage› interface with
▩‹node_collect_semantic_postfix›.
▪ @{theory Voblint_CFG.CFG_Prune} --- interprocedural graph
reachability (\<^const>‹cfg_reaches›), which feeds the cone
guard. The graph itself is unchanged; the cone restriction belongs to the
abstract concretization.
❙‹3. Analysis spine.› Abstract domains, equation systems, and the ‹TD_side› solver bridge; every
generic endpoint concludes over the trace projections.
▪ @{theory Voblint_Domain.Abstract_Domain} ---
▩‹numeric_domain›, lifted state concretization, and
display support.
▪ @{theory Voblint_Framework.Transfer_Algebra} --- the pure
abstract-state algebra: call-entry frame reset, formal binding, structural
return combination, and their soundness against
▩‹gamma_state›.
▪ @{theory Voblint_Framework.DG_Local_State_Spec} --- the
▩‹sound_nonrelational_transfer› contract and two Base
constructions. Their edge and ▩‹EA_Check› soundness
facts discharge \<^theory>‹Voblint_Framework.DG_Spec_Sound›'s
▩‹step_sound› and
▩‹combine_sound› obligations.
▪ @{theory Voblint_Framework.State_Restriction} --- the
local/global restriction algebra used to reassemble routed states.
▪ @{theory Voblint_Framework.DG_Indexed_Generator} ---
▩‹routed_node_rhs_mono_eq›/
▩‹routed_node_rhs_mono_sides›/
▩‹routed_node_rhs_mono_deps› discharge the vendored
solver's ▩‹TD_side_mono› precondition once for an
arbitrary generator instance.
❙‹3b. Check discharge.› A domain-generic, sound (incomplete) decision
procedure for compiled ▩‹__voblint_check(...)› conditions, discharged
against the computed abstract solver environment at each check's own
node --- no store is forwarded between check nodes or to the procedure
exit.
▪ @{theory Voblint_Domain.Numeric_Queries} --- the generic
\<^locale>‹sound_numeric_queries› interface (entailment/refutation of
‹<›/‹=› over an abstract numeric value) and its derivation, defined
directly in any \<^locale>‹sound_refinement› instance's own context, from
that instance's own narrowing operators --- a sound default a concrete
domain may override with sharper, hand-tuned predicates.
▪ @{theory Voblint_Framework.Abstract_Checks} --- \<^locale>‹sound_check_query›: the single ▩‹check_query› decision
procedure into \<^typ>‹bool option› over \<^typ>‹exp›, the three-way
▩‹check_result› classification (▩‹Check_Proved›/▩‹Check_Refuted›/
▩‹Check_Unknown›), and the node-indexed bridge to
\<^const>‹checks_proven›.
▪ @{theory Voblint_Analysis_Sign.Sign_Classify} --- the Sign instance: derived
numeric queries (read off \<^const>‹inv_less_sign›/\<^const>‹inv_eq_sign›/
\<^const>‹inf›), no hand-built comparison tables.
▪ @{theory Voblint_Analysis_Interval.Interval_Classify} --- the Interval instance:
specialized bound-comparison queries (\<^const>‹interval_less_true› and
siblings, ‹Interval_Numeric_Queries›). The backward-domain default derives
equality refutation through \<^const>‹intersect_ivl›, whose canonical empty
result is independent of the raw lattice \<^const>‹inf›.
❙‹4. Concrete domains.› One analysis session per domain, all over the shared
▩‹Analyses/Shared/› chain, all reaching the same spine. Each pairs a lattice theory
(order, transfers, soundness, monotonicity) with one generated ▩‹_Analyses› theory
that registers it at the routed D/G spine at the unit context, for Sign
▩‹sign_rule›; Interval also registers keyed by entry state and by a bounded call
string. The CLI's combined state registers once per context policy:
▩‹mcp_rule›, ▩‹mcp_es_rule› and ▩‹mcp_cs_rule›. Every registration takes
the global update rule ‹r› as a parameter, and the call-string one also its bound
‹k›, so one registration per context policy serves every rule and every bound.
▪ @{theory Voblint_Analysis_Sign.Sign_Transfer} /
@{theory Voblint_Analysis_Sign.Sign_Analyses} --- the seven-element Sign
lattice. It is finite, so the plain-join solver needs no widening.
▪ @{theory Voblint_Analysis_Interval.Interval_Domain} /
@{theory Voblint_Analysis_Interval.Interval_Analyses} --- intervals over
the extended integers. Their infinite height requires widening and
narrowing, making solver choice relevant.
▪ @{theory Voblint_Analysis_Parity.Parity_Domain} --- even/odd.
Finite like Sign, and expressive about values neither Sign nor Interval
constrains: ▩‹y := x * 2› is even for every
▩‹x›.
▪ @{theory Voblint_Domain.Congruence_Lattice} ---
normalized residue classes. Congruence is selectable on its own and is
also the fourth component of ▩‹int_dom›.
▪ @{theory Voblint_Domain.Int_Lattice} /
@{theory Voblint_Analysis_Int.Int_Refinement} ---
▩‹int_dom›, the reduced product of the four scalar
domains, with exact reduction steps and three refinement modes.
▪ @{theory Voblint_Analysis_Relational.Rel_Order_Domain} --- an
order carrier that is ∗‹not› a pointwise abstract state,
showing that the generator and solver do not assume one.
❙‹4b. The D/G interface spine.› The native, carrier-opaque Goblint-▩‹Spec› interface
(independent flow-sensitive local domain ▩‹D› and flow-insensitive global domain ▩‹G›),
the canonical context-sensitive backbone.
▪ @{theory Voblint_Framework.DG_Spec} --- the
▩‹dg_spec› record, with one manager-native transfer
per edge action, plus the ▩‹dg_state› copy lattice and
seeded keyed generator in
@{theory Voblint_Framework.DG_Constraint_Programs}.
▪ @{theory Voblint_Framework.DG_Spec_Sound} --- native
heterogeneous soundness over opaque carriers
(▩‹analysis_contract›). The routed context locales in
@{theory Voblint_Framework.Routed_Context} feed those obligations into
\<^const>‹activation_collect›. The unit-context instance reaches
\<^const>‹node_collect› through
▩‹node_collect_eq_Union_activation_of_fun›
(@{theory Voblint_Framework.Routed_Context_Unit}).
▪ @{theory Voblint_Analysis_Sign.Sign_Analyses} and its four siblings --- each
domain as a \<^locale>‹dg_analysis_exec› instance at the unit context, and
Interval also at entry state and call string, so each reaches
\<^const>‹activation_collect›, and at the unit context \<^const>‹node_collect›,
through the locale's generic node-soundness bridge.
❙‹4c. Activation-trace certification.› The concrete object the context-sensitive soundness
rides: one trace per activation, with a stable call-only context.
▪ @{theory Voblint_Framework.Activation_Backbone} --- the generic
▩‹activation_collect_sound›. Over
\<^const>‹valid_activation_trace›, the five obligations
▩‹INIT›/▩‹INTRA›/
▩‹CALL›/▩‹RETURN›/
▩‹TOTAL› on a ▩‹cover› map bound
\<^const>‹activation_collect› at every
▩‹(node, context)›.
▪ @{theory Voblint_Framework.DG_Ctx_Activation} --- discharges
those five obligations from a
▩‹analysis_contract› post-solution, so a computed D/G
solution certifies the activation collecting semantics.
❙‹5. Executable frontend.› Finite-map state representation and certified execution.
▪ @{theory Voblint_Exec.Default_St_Base} --- executable abstract-state maps for code
generation, layered as representation, algebra
(@{theory Voblint_Exec.Default_St_Algebra}), refinement to variable-indexed states
(@{theory Voblint_Exec.Default_St_Transfer}) and dead-code detection
(@{theory Voblint_Exec.Default_St_Reachability}).
▪ @{theory Voblint_Exec.Default_St_Restriction_Refinement} ---
commutation from executable states to function states.
▪ @{theory Voblint_Routing.Compiled_Routed_Equations} --- the D/G
equation generator (\<^const>‹compiled_routed_eqs_for›) every analysis,
context-insensitive or not, is solved over; the verified solver ∗‹runs› on it.
▪ @{theory Voblint_Framework.DG_Reader_Transport} --- reads a
whole equation system through carrier-generic readers
(\<^const>‹map_dg_state›), letting the executable run answer
for the mathematical system.
▪ @{theory Voblint_Exec.DG_Local_State_Exec_Refinement} ---
\<^locale>‹dg_domain_exec› proves a registered domain's
D/G spec sound directly at the executable carrier, without a separate
abstract-carrier transport step.
▪ @{theory Voblint_Analysis_Sign.Sign_Exec} --- executable Sign transfer functions.
▪ @{theory Voblint_Analysis_Sign.Sign_Analyses} --- the routed
D/G runtime for Sign: each registration's equation system, solved table,
and termination hypothesis ▩‹sign_rule.terminates r›, stated once for every
update rule ‹r›.
▪ @{theory Voblint_Analysis_Interval.Interval_Analyses},
@{theory Voblint_Analysis_Parity.Parity_Analyses},
@{theory Voblint_Analysis_Congruence.Congruence_Analyses} and
@{theory Voblint_Analysis_Int.Int_Fixpoint_Analyses} --- the same runtime for the other
four domains, generated from the same template.
❙‹5b. Solved results and reports.› What a finished analysis ∗‹is›, before anyone
renders or dispatches it.
▪ @{theory Voblint_Framework.Solved_Table} --- the
domain-generic table: a covered key set of
\<^typ>‹pp × 'ctx› pairs plus a total lookup.
▩‹wf_solved_table› requires finitely many keys and
canonical payloads. Publishing adapters guarantee canonicality;
finiteness is unconditional only for context spaces bounded in advance.
▪ @{theory Voblint_Framework.Check_Report} and
@{theory Voblint_Framework.Contextual_Check_Report} --- the flat and
per-context readings of that table. A check can be
\<^const>‹Dead› in one context and decided in another, which a
flat \<^typ>‹check_result› cannot express. The contextual report
therefore has a separate type.
▪ @{theory Voblint_CLI.Analysis_Config} --- the selection surface:
\<^typ>‹analysis_domain›, \<^typ>‹globals_rule› and \<^typ>‹context_mode›, all
plain values. Every combination is analysed, so there is no legality table and no
default a caller inherits.
❙‹6. End-to-end theorems.› Headline soundness and the source bridge.
▪ @{theory Voblint_Result.Source_Activation_Sound} --- the
source-adequacy bridge. A reachable VIMP source configuration produces a
\<^const>‹valid_activation_trace› trace
(▩‹source_run_has_activation_trace›), bounded at its activation
context (▩‹source_activation_sound›) and monovariantly
(▩‹source_reaches_node_collect›).
▪ @{theory Voblint_Result.DG_Live_Unknowns} --- the endpoints of a routed
analysis whose route is a function of the call site, the unit context
among them; they are what every flagship and codegen entry point applies: one
▩‹solve_c ... ≠ None› fact in, source-level soundness out.
Solver correctness, executable-to-pure commutation, post-solution
transport, and D/G collecting soundness are discharged inside. It is
partial correctness: the caller supplies that the solver
∗‹returns›, typically ⬚‹by eval›.
▪ @{theory Voblint_CLI.Analysis_Certified} --- one soundness statement for
every configuration the dispatcher answers with a report
(@{thm [source] run_voblint_source_sound}), and the dead-check and
arithmetic-error guarantees at the same entry point
(@{thm [source] run_voblint_dead_check_unreached},
@{thm [source] run_voblint_arithmetic_refuted}).
▪ @{theory Voblint_Examples.Example_End_To_End_Certificate} --- that
statement instantiated at one program, with its answer evaluated.
❙‹7. Examples and witnesses.› Executable demos, precision
witnesses, and tooling. The five domain flagships
(‹Example_Interval_DG_Flagship›, ‹Exec_Sign_DG_Run›,
‹Example_Parity_DG_Flagship›, ‹Example_Congruence_DG_Run›,
and ‹Exec_Int_DG_Run›) are indexed above, together with the
context-sensitive ‹Example_Interval_DG_Ctx_Collect› and
‹Example_Interval_Source_Ctx›. Analysis results on concrete programs are pinned
by the VIMP regression corpus under ▩‹tests/regression›, which runs the
generated analyzer in seconds.
▪ @{theory Voblint_Analysis_Int.Int_Refinement_Control} closes with the
refinement witnesses: \<^const>‹Refine_Once› stops short of the fixpoint
(@{thm [source] refinement_once_not_fixpoint}), and refining after
‹narrow› would break the solver's bracket
(@{thm [source] post_narrow_refinement_would_violate_narrow_ge}).
▪ @{theory Voblint_Examples_Sign.Example_Sign_DG_CallString_K1} --- the Sign counterpart of the
‹nest› pair, computed by the plain-join solver (▩‹TD_side_always_join_Interp›) rather
than warrowing: Sign is finite, so no widening is needed and the computed solution is
exact. ▩‹sign_nest_1_activation_collect_sound› is the same soundness shape at a
1-call-string context, where ‹g›'s two activations (entered with ‹SPos› and ‹SNeg›)
collapse and join to ‹STop›.
▪ @{theory Voblint_Examples_Sign.Example_Sign_DG_CallString_K2} --- the 2-call-string sibling
(▩‹sign_nest_2_activation_collect_sound›), which keeps ‹g›'s two activations separate
at ‹SPos› and ‹SNeg›. Because Sign is a finite lattice with an exact computed solution,
this pair supports a genuine strict-precision witness:
▩‹sign_k2_strictly_more_precise_than_k1_at_g› proves
the 2-call-string value at ‹g›'s entry is strictly below the 1-call-string ‹STop› merge in
the Sign order, for both activations, ∗‹computed and compared› rather than argued
abstractly.
▪ @{theory Voblint_Examples_Relational.Example_Relational_DG_Demo} --- an execution
witness, not a soundness-certified result: a compiled full-program
`if (x < y) { z := 1 } else { z := 0 }` runs through the *same*
▩‹compiled_routed_eqs_for›/vendored-solver pipeline as Sign/Interval, this time
over ▩‹Voblint_Analysis_Relational.Rel_Order_Domain›'s non-▩‹abs_state›
relational carrier; the computed result is compared against
Interval's on the identical program and rendered, raw and
analysis-annotated, via GraphViz.
❙‹8. Tooling.› Theories outside the core proof spine.
▪ ❙‹Named global unknowns› --- a keyed global family is the routed D/G
context's own ‹buffer_key_at›, and \<^const>‹dep_aux› pins what a per-edge
program reads: @{thm dep_dg_edge_program_at} names the source address and the
one global slot, nothing else.
▪ ❙‹Rendering› --- the text report, DOT and HTML are produced by the OCaml
renderers from \<^const>‹run_voblint›'s structured result, outside any theory.
A rendering asserts nothing that a ▩‹writeln› could check, so the
fixtures under ▩‹tests/regression/› carry it instead --- ▩‹08-tooling› for
▩‹--dot›, ▩‹13-full-state-dot› for the per-node states, and
▩‹11-graph-snapshot› for golden cluster/node/edge snapshots including a
recursive procedure.
▪ ❙‹Update rules on their own terms:›
@{theory Voblint_Examples_Tooling.Example_Update_Rule_Steps} feeds one global the same
contributions under each rule, outside any solver run, and
@{theory Voblint_Examples_Tooling.Example_Per_Origin_Widening_Precision} shows the
precision warrowing per origin keeps that warrowing the joined slot loses.
❙‹9. The CLI: configuration and code generation.›
One public operation over every activation list, update rule and context policy,
running the active analyses as one component of the shared pipeline, and exported
to OCaml.
▪ @{theory Voblint_Solver.Globals_Rule} --- the rule that merges contributions to a
side-effected global, as a value: one solver interpretation serves all four, and
every domain registers each context policy once over it.
▪ @{theory Voblint_CLI.Analysis_Run} --- \<^const>‹run_voblint›, the one operation
code generation exports: a configuration of analyses, a global update rule and a
context policy, and a program. Every combination is analysed; the answer is a
report of semantic states, and its rendering (@{theory Voblint_CLI.Analysis_Render})
is a projection outside the theorems. ▩‹dispatch_demo_interval_precise› pins one
program's answer ▩‹by eval›, and a hand-written OCaml driver under
‹codegen/regression/› checks the generated module against the same values.
▪ @{theory Voblint_CLI.Analysis_Run_Sound} and
@{theory Voblint_CLI.Analysis_Run_Ctx_Sound} --- one soundness table per context
policy (@{thm [source] mcp_rule_table}, @{thm [source] mcp_es_rule_table},
@{thm [source] mcp_cs_rule_table}), each stated for an arbitrary activation list
and update rule, over the registrations of
\<^theory>‹Voblint_CLI.MCP_Analyses›.
@{theory Voblint_CLI.Analysis_Report} reads a report through ‹ℛ⇘res⇙ v› and
\<^const>‹verdict_stores› and proves, by one case split over the tables, that
every report \<^const>‹run_voblint› returns is sound
(@{thm [source] analysis_report_of_sound}).
@{theory Voblint_CLI.Analysis_Certified} states
@{thm [source] run_voblint_source_sound} and
@{thm [source] run_voblint_check_sound} once for every configuration.
❙‹What the proof attaches to.› ▩‹export_code› translates the executable
equations of \<^const>‹run_voblint› and everything it transitively calls, down to the
solver itself. It is not proving one function and exporting a different,
hand-written one: the generated operation is a translation of the same equations
@{thm [source] run_voblint_source_sound} is proved about. That theorem asks for no
termination premise: an analysed answer exists only where the executable solve
returned. It is partial correctness; nothing proves the solve returns on every
program. \<^theory>‹Voblint_Examples.Example_End_To_End_Certificate› evaluates
the answer for one program and applies the theorem to a concrete run.
›
text ‹
❙‹The D/G execution pipeline (headline).› The flagship threads a single chain,
every step machine-checked, from source to a soundness theorem over the
∗‹computed› analysis result:
▪ VIMP source ▩‹compile_prog› to a CFG;
▪ the generic D/G generator ▩‹compiled_routed_eqs_for› emits the equation system;
▪ the verified solver ∗‹computes› a solution (▩‹solve_c ... = Some sigma›, ▩‹by eval›);
▪ the endpoint ‹interval_rule.fun_route_source_sound›
(@{theory Voblint_Result.DG_Live_Unknowns}, the routed analysis at the unit
context) bundles solver correctness,
executable/pure commutation,
post-solution transport, and D/G collecting soundness into one
application, bounding ‹𝒞⇘𝒢,g,S⇙ v› at every program point.
❙‹Soundness spine.› The context-sensitive analyses converge on one native
interface, the carrier-opaque ▩‹analysis_contract›; every domain is one of its
instances, and context slicing is factored through
the relational activation spine and its per-context admitted slots --- the unit
and call-string routings stay functional (\<^const>‹context_policy_of_fun›), while
entry-state routing genuinely admits several contexts per call. There is one
such spine: every domain reaches \<^const>‹node_collect› through the routed
unit-context instance's ▩‹node_collect_eq_Union_activation_of_fun›, and the routed
instances through ▩‹activation_collect_sound› above it.
›
end