Theory Call_String_Context
theory Call_String_Context
imports "Voblint_CFG.CFG_Def"
begin
section ‹A reusable bounded call-string context›
text ‹
The call-string route/enter-context pair: this theory owns only the call-string
∗‹data› and the one closed-term equality that makes ‹routed_context›'s
routing agreement trivial for any bound ‹k› --- it deliberately does not
import ‹Routed_Context› or ‹DG_Ctx_Activation›, and fixes no domain, no solver, and
no CFG. ‹cs_route›/‹cs_context› (defined below) plug into ‹routed_context›'s
‹route›/‹enterc› parameters at whatever concrete instantiation a caller chooses; nothing
here decides what that instantiation is.
›
subsection ‹The call-string type and its two projections›
text ‹Most recent call site first, unbounded as a type --- ‹k› only bounds the ∗‹values›
‹cs_route›/‹cs_context› produce, not the type itself. This mirrors Goblint's
‹C.t› being a value-level choice under a type-level bound only because OCaml forces the
bound to be a type; here ‹k› is ordinary \<^typ>‹nat› data.›
type_synonym call_string = "cfg_node list"
text ‹The equation-level route: push the call site, keep only the most recent ‹k›. Ignores
the entered abstract/executable value ‹d› entirely, so it is representation-independent
for ∗‹any› domain without a per-domain commute lemma (‹cs_route_indep_of_data› below).›
definition cs_route :: "nat ⇒ pp ⇒ call_string ⇒ 'd ⇒ call_action ⇒ call_string" where
"cs_route k u ctx d ca = take k (u # ctx)"
text ‹The trace-semantic context function whose graph, ‹context_policy_of_fun (cs_context k)›,
instantiates ‹routed_context›'s ‹adm›: same closed term as \<^const>‹cs_route›,
over the concrete \<^typ>‹store› the activation-trace semantics supplies instead of an
abstract/executable ‹'d›.›
definition cs_context :: "nat ⇒ cfg_node ⇒ call_string ⇒ store ⇒ call_string" where
"cs_context k u ctx s = take k (u # ctx)"
subsection ‹The two facts every instance needs›
text ‹Routing agreement, generically: since neither side reads ‹d›/‹s›, this holds for
∗‹any› ‹k›, ‹u›, ‹ctx›, ‹d›, ‹ca›, ‹s› with zero case analysis.›
lemma cs_route_context_agree: "cs_route k u ctx d ca = cs_context k u ctx s"
by (simp add: cs_route_def cs_context_def)
text ‹Representation independence: \<^const>‹cs_route› agrees with itself under ∗‹any›
substitution for its data argument, since ‹d› never appears on the right-hand side. A
caller needing ‹cs_route k u ctx (d::'exec) ca = cs_route k u ctx (repr d) ca› for a
specific representation map ‹repr› -- the map from an executable state to its function, say --
gets it as an instance of this lemma, or just as directly by unfolding
‹cs_route_def› at the call site --- both are one line.›
lemma cs_route_indep_of_data: "cs_route k u ctx d ca = cs_route k u ctx d' ca"
by (simp add: cs_route_def)
subsection ‹Bounded length›
text ‹The one fact that makes this context space finite: routing truncates, so no context a
‹k›-bounded run produces is longer than ‹k›. Over a graph with finitely many nodes that
bounds the whole space before any solve is attempted, rather than per run.›
lemma cs_route_length: "length (cs_route k u ctx d ca) ≤ k"
by (simp add: cs_route_def)
subsection ‹Truncation behaviour›
text ‹Below the bound, pushing a call site loses nothing --- a plain cons, not a
truncation. Needed for any future precision argument: contexts stay distinct as long as
the call histories being separated fit under ‹k›.›
lemma cs_route_below_bound:
"length ctx < k ⟹ cs_route k u ctx d ca = u # ctx"
by (simp add: cs_route_def)
lemma cs_context_below_bound:
"length ctx < k ⟹ cs_context k u ctx s = u # ctx"
by (simp add: cs_context_def)
text ‹The central algebraic property of a bounded call string: projecting a longer bound's
context down to a shorter one agrees with routing at the shorter bound directly. This is
the ‹take k1 ctx_k2 = ctx_k1› fact any future ‹k1 <= k2› refinement theorem needs to relate
the two analyses' unknown spaces.›
lemma cs_route_k_mono:
assumes "k1 ≤ k2"
shows "take k1 (cs_route k2 u ctx d ca) = cs_route k1 u ctx d ca"
using assms by (simp add: cs_route_def)
subsection ‹The call-string-keyed global-key type›
text ‹The global-key space a call-string-routed equation system publishes into: one
‹Global› slot for the real globals, plus one ‹Seed› slot per (procedure entry,
call-string) pair for the routed callee entry states. The ‹Seed› payload carries the
call string itself, so the key shape does not depend on the bound ‹k› --- only the
payload's length does. Still pure data: no domain, no solver, no CFG.›