Theory Routed_Context
theory Routed_Context
imports Routed_Call_Programs DG_Ctx_Activation DG_Local_State_Spec
Activation_Backbone
begin
section ‹One route, CALL and COMB discharged once›
text ‹
\<^locale>‹dg_context_activation› already discharges EDGE (‹dg_ctx_act_edge›) generically off the
post-solution, independent of ‹route›/‹cmb›/‹extra›: intra edges never route. COMB
cannot be discharged that generically, because ‹cmb› is an unconstrained parameter: a
context-sensitive analysis whose entry-seed publication and return combine are hand-written
has to rederive the routing argument itself. This
theory fixes ‹cmb› and ‹extra› to the one canonical shape ‹Routed_Call_Programs›
builds --- parametric only in a routing function ‹route› and a seed-key injection
‹seed› --- and discharges CALL and COMB as theorems of that shape: a k-call-string
or a partial-tabulation context becomes an interpretation of this locale, not a second
proof development.
›
subsection ‹The routed-context locale: D and G independently typed›
text ‹
‹routed_context› instantiates \<^locale>‹dg_context_activation› at
‹routed_call_program›/‹routed_entry_seed_programs›, so ‹S›'s own ‹'D›/‹'G› stay as
independent as that locale already keeps them: no ‹'D = 'G› constraint is threaded
in by this locale's ‹for› clause. \<^locale>‹dg_context_activation› itself carries
no routing-specific content: every fact it supplies (‹pp_eq_bound›,
‹pp_sides_bound›, ‹sides_fold_le_Gen›, ‹edge_bound_local›/‹_global›,
‹dg_ctx_act_edge›) is already generic in
‹cmb›/‹extra›, so instantiating it at ‹routed_call_program›/‹routed_entry_seed_programs›
reuses those proofs unchanged; only the seed-specific reasoning below, which
‹dg_context_activation› never has since seeding is ‹routed_call_program›'s own
addition, is carried out here.
Beyond \<^locale>‹dg_context_activation›'s parameters: ‹seed› injects a routed
‹(pp, 'c)› pair into the global-key space; ‹adm› is the trace-semantic context relation
keying the activation-trace collecting semantics; and two obligations about it cannot be
discharged generically. ‹routing_adequate› is adequacy: whenever ‹adm› admits a context
for a real call edge and a covered caller store, some alternative of the specification's
own entry run describes that call --- its continuation half containing the caller store,
its entry half containing the entered store, and its route being exactly the admitted
context. The three come from one alternative rather than three, which is what keeps a
multi-alternative entry from mixing one alternative's continuation with another's callee
frame. ‹routing_total› is existence: every covered call admits some context.
Restricting both to an edge of ‹g› (rather than quantifying over every value of the
‹call_action› type) matches how CALL and COMB below only ever invoke them at a matched
edge, and keeps the obligations provable for an abstract domain that is exact on edges
actually present in the program without being exact everywhere. These are per-instance
proof obligations, not locale theorems.
‹calls_unique› ties the edge a return reads to the edge its callee was entered through;
the collecting semantics itself never needs it, and compiled programs have it for free.
›
locale routed_context =
dg_context_activation S γ⇩D⇩G 𝒢 g buffer_key global_of route
"routed_call_program S global_of seed resolve is_bot"
"routed_entry_seed_programs seed"
bot0 d⇩0 g⇩0 sigma vars x0 sg γ⇩M
for S :: "(pp × 'c, 'k, 'v, 'D::bounded_semilattice_sup_bot,
'G::bounded_semilattice_sup_bot) dg_spec"
and γ⇩D⇩G :: "'D ⇒ ('v ⇒ 'G) ⇒ store set"
and 𝒢 :: "vname ⇒ bool"
and g buffer_key and global_of :: "'v ⇒ 'k"
and route ("context⇧♯")
and bot0 d⇩0 g⇩0 sigma vars x0 sg
and seed :: "pp ⇒ 'c ⇒ 'k"
and resolve :: "pp ⇒ pp ⇒ call_action ⇒ 'D ⇒ pname list"
and is_bot :: "'D ⇒ bool"
and γ⇩M :: "'M ⇒ store set" +
fixes adm :: "'c context_policy"
assumes finC: "finite (calls g)"
and calls_unique: "calls_source_unique g"
and seed_ne_buffer_key[simp]: "⋀p ctx. seed p ctx ≠ buffer_key"
and seed_ne_global_of[simp]: "⋀p ctx v. seed p ctx ≠ global_of v"
and is_bot_bot[simp]: "is_bot bot"
and is_bot_sound: "⋀d g. is_bot d ⟹ γ⇩D⇩G d g = {}"
and resolve_sound:
"⋀u ctx dst pars args p cont s.
(u, ctx) ∈ vars
⟹ (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
⟹ s ∈ γ⇩D⇩G (dg_local (sigma (Inl (u, ctx)))) (genv global_of sigma)
⟹ p ∈ set (resolve cont u (CallEdge dst pars args)
(dg_local (sigma (Inl (u, ctx)))))"
and routing_adequate:
"⋀u ctx dst pars args p cont s ctx'.
(u, ctx) ∈ vars
⟹ (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
⟹ s ∈ γ⇩D⇩G (dg_local (sigma (Inl (u, ctx)))) (genv global_of sigma)
⟹ ctx' ∈ adm u ctx (call_info_of (CallEdge dst pars args) p) s
(call_enter 𝒢 (CallEdge dst pars args) s)
⟹ ∃pairs pub deps cont' entry.
enter_runs (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(mk_dg_man (dg_local (sigma (Inl (u, ctx)))) global_of) sigma pairs pub
∧ enter_deps (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(mk_dg_man (dg_local (sigma (Inl (u, ctx)))) global_of) sigma pairs deps
∧ (cont', entry) ∈ set pairs
∧ s ∈ γ⇩D⇩G cont' (genv global_of sigma)
∧ call_enter 𝒢 (CallEdge dst pars args) s
∈ γ⇩D⇩G entry (genv global_of sigma)
∧ context⇧♯ u ctx entry (CallEdge dst pars args) = ctx'
∧ (FunctionEntry p, ctx') ∈ vars"
and routing_total:
"⋀u ctx dst pars args p cont s.
(u, ctx) ∈ vars
⟹ (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
⟹ s ∈ γ⇩D⇩G (dg_local (sigma (Inl (u, ctx)))) (genv global_of sigma)
⟹ adm u ctx (call_info_of (CallEdge dst pars args) p) s
(call_enter 𝒢 (CallEdge dst pars args) s) ≠ {}"
and comb_fwd:
"⋀cl c1 dst pars args p cont.
(cl, c1) ∈ vars ⟹ (cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
⟹ (cont, c1) ∈ vars"
begin
text ‹The reader's claim at a key, and the call contexts ‹adm› admits. Input-only, like
‹gamma_at›, so interpreted facts keep printing the explicit terms.›
abbreviation (input) cover :: "pp ⇒ 'c ⇒ store set" where
"cover v ctx ≡ γ⇩M (sg (Inl (v, ctx)))"
abbreviation (input) admits where
"admits ≡ admits_call_context 𝒢 g adm"
text ‹
One place unpacks the call's entry protocol. ‹routing_adequate› is a nest
of existentials over one entry run, and both CALL and COMB need the same
witnesses: unpacking it separately in each would let them drift onto
∗‹different› alternatives of the same call, which is precisely the
correlation the pair list exists to keep.
Invoke it with ‹obtain›; it is not an elimination rule for the classical
reasoner.
›
lemma routed_enter_witness:
assumes covV: "(u, ctx) ∈ vars"
and ce: "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ gamma_at u ctx"
and Rc: "ctx' ∈ adm u ctx (call_info_of (CallEdge dst pars args) p) s
(call_enter 𝒢 (CallEdge dst pars args) s)"
obtains pairs pub deps cont' entry
where "enter_runs (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(man_at u ctx) sigma pairs pub"
and "enter_deps (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(man_at u ctx) sigma pairs deps"
and "(cont', entry) ∈ set pairs"
and "s ∈ γ⇩D⇩G cont' (genv global_of sigma)"
and "call_enter 𝒢 (CallEdge dst pars args) s
∈ γ⇩D⇩G entry (genv global_of sigma)"
and "context⇧♯ u ctx entry (CallEdge dst pars args) = ctx'"
and "(FunctionEntry p, ctx') ∈ vars"
using routing_adequate[OF covV ce sin Rc] that by blast
text ‹
The alternative the eliminator hands over cannot be bottom, and no case
distinction is needed to see it: a bottom alternative concretizes to nothing,
while this one demonstrably contains the store the callee actually starts
from. A bottom alternative therefore never describes a real callee execution
--- it stays in the fold only because its combine stage may still have
effects.
›
lemma entry_cover_not_bot:
assumes "s' ∈ γ⇩D⇩G entry gv"
shows "¬ is_bot entry"
proof
assume "is_bot entry"
then have "γ⇩D⇩G entry gv = {}" by (rule is_bot_sound)
with assms show False by simp
qed
lemma le_dg_state_localD: "d ≤ d' ⟹ dg_local d ≤ dg_local d'"
by (simp add: less_eq_dg_state_def)
lemma le_dg_state_globalD: "d ≤ d' ⟹ dg_global d ≤ dg_global d'"
by (simp add: less_eq_dg_state_def)
subsection ‹Reaching a resolved callee's contribution›
text ‹
A call edge reaches the generated equation in two hops: the call site's own program is one
of the node's contribs, and the resolved callee's program is one summand of that site's fold.
The second hop needs a concrete store at the call site, since a resolver may drop a
target the abstract caller state rules out; where a store exists, the edge's own callee
survives resolution.
›
lemma resolved_site_mem:
assumes ce: "(cc, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
shows "routed_call_program S global_of seed resolve is_bot context⇧♯ ctx
(CallEdge dst pars args) cc cont
∈ set (contribs cont ctx)"
proof -
have "(cc, CallEdge dst pars args) ∈ set (call_site_list g cont)"
using ce by (auto simp: set_call_site_list[OF finC])
then show ?thesis by (rule routed_contribution_programs_combineI)
qed
lemma resolved_target_mem:
assumes covV: "(cc, ctx) ∈ vars"
and ce: "(cc, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ gamma_at cc ctx"
shows "routed_callee_call_program S global_of seed context⇧♯ is_bot ctx (CallEdge dst pars args) cc
(dg_local (sigma (Inl (cc, ctx)))) p
∈ set (map (routed_callee_call_program S global_of seed context⇧♯ is_bot ctx
(CallEdge dst pars args) cc
(dg_local (sigma (Inl (cc, ctx)))))
(resolve cont cc (CallEdge dst pars args)
(dg_local (sigma (Inl (cc, ctx))))))"
using resolve_sound[OF covV ce sin] by simp
lemma resolved_at_le_site_acc:
assumes covV: "(cc, ctx) ∈ vars"
and ce: "(cc, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ gamma_at cc ctx"
shows "dg_local (traverse_program
(routed_callee_call_program S global_of seed context⇧♯ is_bot ctx (CallEdge dst pars args) cc
(dg_local (sigma (Inl (cc, ctx)))) p) sigma)
≤ side_acc_dg (acc0 cont) sigma (contribs cont ctx)"
proof -
have "dg_local (traverse_program
(routed_callee_call_program S global_of seed context⇧♯ is_bot ctx (CallEdge dst pars args) cc
(dg_local (sigma (Inl (cc, ctx)))) p) sigma)
≤ dg_local (traverse_program
(routed_call_program S global_of seed resolve is_bot context⇧♯ ctx
(CallEdge dst pars args) cc cont)
sigma)"
using dg_local_traverse_le_side_acc_dg[OF resolved_target_mem[OF covV ce sin], where acc = bot]
by (simp add: routed_call_program_def sp_compile_bind sp_wf_observes
traverse_side_rhs_fold_dg[OF sp_wf_routed_callee_call_programs[OF spec_wf]])
also have "… ≤ side_acc_dg (acc0 cont) sigma (contribs cont ctx)"
by (rule dg_local_traverse_le_side_acc_dg[OF resolved_site_mem[OF ce]])
finally show ?thesis .
qed
lemma resolved_at_le_site_sides:
assumes covV: "(cc, ctx) ∈ vars"
and ce: "(cc, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ gamma_at cc ctx"
shows "sides_of_program
(routed_callee_call_program S global_of seed context⇧♯ is_bot ctx (CallEdge dst pars args) cc
(dg_local (sigma (Inl (cc, ctx)))) p) sigma z
≤ sides_of_program (side_rhs_fold_dg (acc0 cont) (contribs cont ctx)) sigma z"
proof -
have "sides_of_program
(routed_callee_call_program S global_of seed context⇧♯ is_bot ctx (CallEdge dst pars args) cc
(dg_local (sigma (Inl (cc, ctx)))) p) sigma z
≤ sides_of_program
(routed_call_program S global_of seed resolve is_bot context⇧♯ ctx
(CallEdge dst pars args) cc cont)
sigma z"
by (rule routed_call_program_sides_ge_at
[where resolve = resolve and v = cont and cc = cc and ctx = ctx and σ = sigma,
OF spec_wf resolve_sound[OF covV ce sin]])
also have "… ≤ sides_of_program (side_rhs_fold_dg (acc0 cont) (contribs cont ctx)) sigma z"
by (rule sides_le_side_rhs_fold_dg[OF contribs_wf resolved_site_mem[OF ce]])
finally show ?thesis .
qed
subsection ‹CALL: the routed callee entry›
text ‹The CALL obligation, ending in ‹routed_context_call›: the store a call hands the callee
is covered by the callee entry read at the routed context. The bound does not go there
directly. It goes through the seed unknown, which is the only place the caller's own program
and the callee's entry equation meet.›
lemma routed_seed_read_bound:
assumes covV: "(FunctionEntry p, ctx') ∈ vars"
shows "dg_local (sigma (Inr (seed (FunctionEntry p) ctx')))
≤ dg_local (sigma (Inl (FunctionEntry p, ctx')))"
proof -
let ?t = "do { s ← sp_read_global (seed (FunctionEntry p) ctx');
sp_return (DG (dg_local s) bot) }"
have mem: "?t ∈ set (contribs (FunctionEntry p) ctx')"
by (rule routed_contribution_programs_extraI) (simp add: routed_entry_seed_programs_def)
have "dg_local (sigma (Inr (seed (FunctionEntry p) ctx')))
= dg_local (traverse_program ?t sigma)"
by (simp add: sp_compile_def)
also have "… ≤ side_acc_dg (acc0 (FunctionEntry p)) sigma (contribs (FunctionEntry p) ctx')"
using dg_local_traverse_le_side_acc_dg[OF mem] .
also have "… = dg_local (eq Gen (FunctionEntry p, ctx') sigma)"
by (simp add: eq_routed_node_rhs[OF contribs_wf])
also have "… ≤ dg_local (sigma (Inl (FunctionEntry p, ctx')))"
using pp_eq_bound[OF covV] by (simp add: less_eq_dg_state_def)
finally show ?thesis .
qed
text ‹
The published callee-entry state is bounded by the seed unknown itself, and that
bound needs only the continuation's coverage: the seed is written by the combine
program living at the continuation, so nothing about the callee entry's own unknown
enters the argument. ‹routed_seed_publish_bound_local› adds the one further hop
from the seed to the callee-entry local, which is where the callee's own entry
equation reads it back, and that hop is what needs the callee entry covered.
›
lemma routed_seed_publish_bound_seed:
assumes covV: "(u, ctx) ∈ vars"
and ce: "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ gamma_at u ctx"
and covV_cont: "(cont, ctx) ∈ vars"
and R: "enter_runs (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(man_at u ctx) sigma pairs pub"
and mem: "(cont', entry) ∈ set pairs"
and nb: "¬ is_bot entry"
shows "entry
≤ dg_local (sigma (Inr (seed (FunctionEntry p)
(context⇧♯ u ctx entry (CallEdge dst pars args)))))"
proof -
let ?ctx' = "context⇧♯ u ctx entry (CallEdge dst pars args)"
let ?k = "Inr (seed (FunctionEntry p) ?ctx')"
let ?t = "routed_callee_call_program S global_of seed context⇧♯ is_bot ctx (CallEdge dst pars args) u
(dg_local (sigma (Inl (u, ctx)))) p"
have seedb: "DG entry bot ≤ sides_of_program ?t sigma ?k"
using spec_wf R mem nb by (rule routed_callee_call_program_sides_ge_seed)
have "entry ≤ dg_local (sides_of_program ?t sigma ?k)"
using le_dg_state_localD[OF seedb] by simp
also have "… ≤ dg_local (sides_of_program
(side_rhs_fold_dg (acc0 cont) (contribs cont ctx)) sigma ?k)"
by (rule le_dg_state_localD[OF resolved_at_le_site_sides[OF covV ce sin]])
also have "… ≤ dg_local (sides_of_rhs (Gen (cont, ctx)) sigma ?k)"
by (rule le_dg_state_localD[OF sides_fold_le_Gen])
also have "… ≤ dg_local (sigma ?k)"
using pp_sides_bound[OF covV_cont, THEN le_funD, of ?k]
by (rule le_dg_state_localD)
finally show ?thesis .
qed
lemma routed_seed_publish_bound_local:
assumes covV_call: "(u, ctx) ∈ vars"
and ce: "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ gamma_at u ctx"
and covV_cont: "(cont, ctx) ∈ vars"
and R: "enter_runs (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(man_at u ctx) sigma pairs pub"
and mem: "(cont', entry) ∈ set pairs"
and nb: "¬ is_bot entry"
and covV: "(FunctionEntry p, context⇧♯ u ctx entry (CallEdge dst pars args)) ∈ vars"
shows "entry
≤ dg_local (sigma (Inl (FunctionEntry p,
context⇧♯ u ctx entry (CallEdge dst pars args))))"
by (rule order_trans
[OF routed_seed_publish_bound_seed[OF covV_call ce sin covV_cont R mem nb]
routed_seed_read_bound[OF covV]])
theorem routed_context_call:
assumes ce: "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ cover u ctx"
and Rc: "ctx' ∈ adm u ctx (call_info_of (CallEdge dst pars args) p) s
(call_enter 𝒢 (CallEdge dst pars args) s)"
shows "call_enter 𝒢 (CallEdge dst pars args) s ∈ cover (FunctionEntry p) ctx'"
proof (cases "(u, ctx) ∈ vars")
case False
hence "cover u ctx = {}" by (rule sg_uncov)
thus ?thesis using sin by simp
next
case True
let ?g = "genv global_of sigma"
have covV_cont: "(cont, ctx) ∈ vars"
using comb_fwd[OF True ce] .
have sin': "s ∈ γ⇩D⇩G (dg_local (sigma (Inl (u, ctx)))) ?g"
using sin True by simp
obtain pairs pub deps cont' entry
where Rr: "enter_runs (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(man_at u ctx) sigma pairs pub"
and "enter_deps (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(man_at u ctx) sigma pairs deps"
and mem: "(cont', entry) ∈ set pairs"
and ecov: "call_enter 𝒢 (CallEdge dst pars args) s ∈ γ⇩D⇩G entry ?g"
and req: "context⇧♯ u ctx entry (CallEdge dst pars args) = ctx'"
and covV: "(FunctionEntry p, ctx') ∈ vars"
by (rule routed_enter_witness[OF True ce sin' Rc])
let ?ctx' = "context⇧♯ u ctx entry (CallEdge dst pars args)"
have nb: "¬ is_bot entry" using ecov by (rule entry_cover_not_bot)
have "γ⇩D⇩G entry ?g ⊆ γ⇩D⇩G (dg_local (sigma (Inl (FunctionEntry p, ?ctx')))) ?g"
by (rule gammaDG_mono
[OF routed_seed_publish_bound_local[OF True ce sin' covV_cont Rr mem nb covV[folded req]]
order_refl])
also have "… = cover (FunctionEntry p) ?ctx'"
using covV[folded req] by simp
finally show ?thesis using ecov req by auto
qed
subsection ‹COMB: the routed return combine›
text ‹The COMB obligation, ending in ‹routed_context_comb›: the state a return combines is
covered by the continuation read at the caller's own context. The return takes one
alternative among those the enter step produced, so the work is to bound that single
alternative -- once locally, once at the global key -- against what the continuation's
unknown already holds.›
lemma routed_comb_bound_local:
assumes covV: "(cl, c1) ∈ vars"
and ce: "(cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ gamma_at cl c1"
and covV_cont: "(cont, c1) ∈ vars"
and R: "enter_runs (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(man_at cl c1) sigma pairs pub"
and mem: "(cont', entry) ∈ set pairs"
shows "dg_local (traverse_program
(routed_call_alternative_program S global_of seed context⇧♯ is_bot c1
(CallEdge dst pars args) cl p (cont', entry)) sigma)
≤ dg_local (sigma (Inl (cont, c1)))"
proof -
have "dg_local (traverse_program
(routed_call_alternative_program S global_of seed context⇧♯ is_bot c1
(CallEdge dst pars args) cl p (cont', entry)) sigma)
≤ dg_local (traverse_program
(routed_callee_call_program S global_of seed context⇧♯ is_bot c1 (CallEdge dst pars args) cl
(dg_local (sigma (Inl (cl, c1)))) p) sigma)"
by (rule routed_callee_call_program_traverse_ge[OF spec_wf R mem])
also have "… ≤ side_acc_dg (acc0 cont) sigma (contribs cont c1)"
by (rule resolved_at_le_site_acc[OF covV ce sin])
also have "… = dg_local (eq Gen (cont, c1) sigma)"
by (simp add: eq_routed_node_rhs[OF contribs_wf])
also have "… ≤ dg_local (sigma (Inl (cont, c1)))"
using pp_eq_bound[OF covV_cont] by (simp add: less_eq_dg_state_def)
finally show ?thesis .
qed
lemma routed_comb_bound_global:
assumes covV: "(cl, c1) ∈ vars"
and ce: "(cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ gamma_at cl c1"
and covV_cont: "(cont, c1) ∈ vars"
and R: "enter_runs (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(man_at cl c1) sigma pairs pub"
and mem: "(cont', entry) ∈ set pairs"
shows "dg_global (sides_of_program
(routed_call_alternative_program S global_of seed context⇧♯ is_bot c1
(CallEdge dst pars args) cl p (cont', entry)) sigma (Inr k))
≤ dg_global (sigma (Inr k))"
proof -
have "dg_global (sides_of_program
(routed_call_alternative_program S global_of seed context⇧♯ is_bot c1
(CallEdge dst pars args) cl p (cont', entry)) sigma (Inr k))
≤ dg_global (sides_of_program
(routed_callee_call_program S global_of seed context⇧♯ is_bot c1 (CallEdge dst pars args) cl
(dg_local (sigma (Inl (cl, c1)))) p) sigma (Inr k))"
by (rule le_dg_state_globalD[OF routed_callee_call_program_sides_ge_combine[OF spec_wf R mem]])
also have "… ≤ dg_global (sides_of_program
(side_rhs_fold_dg (acc0 cont) (contribs cont c1)) sigma (Inr k))"
by (rule le_dg_state_globalD[OF resolved_at_le_site_sides[OF covV ce sin]])
also have "… ≤ dg_global (sides_of_rhs (Gen (cont, c1)) sigma (Inr k))"
by (rule le_dg_state_globalD[OF sides_fold_le_Gen])
also have "… ≤ dg_global (sigma (Inr k))"
using pp_sides_bound[OF covV_cont, THEN le_funD, of "Inr k"]
by (rule le_dg_state_globalD)
finally show ?thesis .
qed
lemma routed_comb_bound_genv:
assumes covV: "(cl, c1) ∈ vars"
and ce: "(cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ gamma_at cl c1"
and covV_cont: "(cont, c1) ∈ vars"
and R: "enter_runs (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
(man_at cl c1) sigma pairs pub"
and mem: "(cont', entry) ∈ set pairs"
shows "genv global_of (sides_of_program
(routed_call_alternative_program S global_of seed context⇧♯ is_bot c1
(CallEdge dst pars args) cl p (cont', entry)) sigma)
≤ genv global_of sigma"
unfolding le_fun_def genv_def
using routed_comb_bound_global[OF covV ce sin covV_cont R mem] by blast
theorem routed_context_comb:
assumes ce: "(cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and s: "s ∈ cover cl c1"
and adm: "admits cl c1 p' s es ctx'"
and t: "t ∈ cover (FunctionResult p) ctx'"
shows "combine_collect 𝒢 dst s t ∈ cover cont c1"
proof (cases "(cl, c1) ∈ vars")
case False
hence "cover cl c1 = {}" by (rule sg_uncov)
thus ?thesis using s by simp
next
case True
let ?g = "genv global_of sigma"
let ?ci = "call_info_of (CallEdge dst pars args) p"
have sin: "s ∈ γ⇩D⇩G (dg_local (sigma (Inl (cl, c1)))) ?g"
using s True by simp
from adm obtain dst2 pars2 args2 cont2
where e2: "(cl, CallEdge dst2 pars2 args2, FunctionEntry p', cont2) ∈ calls g"
and es_eq: "es = call_enter 𝒢 (CallEdge dst2 pars2 args2) s"
and Rc2: "ctx' ∈ adm cl c1 (call_info_of (CallEdge dst2 pars2 args2) p') s es"
by (rule admits_call_contextE)
have same: "CallEdge dst2 pars2 args2 = CallEdge dst pars args" and pp': "p' = p"
using calls_source_unique_edgesD(1,2)[OF calls_unique e2 ce] by simp_all
have Rc: "ctx' ∈ adm cl c1 ?ci s (call_enter 𝒢 (CallEdge dst pars args) s)"
using Rc2 unfolding es_eq same pp' .
obtain pairs pub deps cont' entry
where Rr: "enter_runs (enter⇧♯ S ?ci)
(man_at cl c1) sigma pairs pub"
and "enter_deps (enter⇧♯ S ?ci)
(man_at cl c1) sigma pairs deps"
and mem: "(cont', entry) ∈ set pairs"
and ccov: "s ∈ γ⇩D⇩G cont' ?g"
and ecov: "call_enter 𝒢 (CallEdge dst pars args) s ∈ γ⇩D⇩G entry ?g"
and req: "context⇧♯ cl c1 entry (CallEdge dst pars args) = ctx'"
by (rule routed_enter_witness[OF True ce sin Rc])
let ?ex_ctx = "context⇧♯ cl c1 entry (CallEdge dst pars args)"
let ?alt = "routed_call_alternative_program S global_of seed context⇧♯ is_bot c1
(CallEdge dst pars args) cl p (cont', entry)"
have nb: "¬ is_bot entry" using ecov by (rule entry_cover_not_bot)
show ?thesis
proof (cases "(FunctionResult p, ?ex_ctx) ∈ vars")
case False
hence "cover (FunctionResult p) ?ex_ctx = {}" by (rule sg_uncov)
with req have "cover (FunctionResult p) ctx' = {}" by simp
with t show ?thesis by simp
next
case True
have covV_cont: "(cont, c1) ∈ vars"
using comb_fwd[OF ‹(cl, c1) ∈ vars› ce] .
have tin: "t ∈ γ⇩D⇩G (dg_local (sigma (Inl (FunctionResult p, ?ex_ctx)))) ?g"
using t req True by simp
let ?sub = "sp_compile_with (λd. DG d bot)
(dg_spec_combine_transfer S ?ci (mk_dg_man cont' global_of)
(dg_local (sigma (Inl (FunctionResult p, ?ex_ctx)))))"
have tr: "traverse_program ?alt sigma = traverse_rhs ?sub sigma"
using nb by (simp add: sp_compile_def)
have sd:
"genv global_of (sides_of_program ?alt sigma) = genv global_of (sides_of_rhs ?sub sigma)"
proof (rule ext)
fix w
have knk: "(Inr (global_of w) :: (pp × 'c) + 'k) ≠ Inr (seed (FunctionEntry p) ?ex_ctx)"
by (rule not_sym) simp
show "genv global_of (sides_of_program ?alt sigma) w = genv global_of (sides_of_rhs ?sub sigma) w"
using nb
by (simp add: genv_def Let_def sp_compile_def fun_upd_other[OF knk] del: fun_upd_apply)
qed
have "combine_collect 𝒢 dst s t
∈ γ⇩D⇩G (dg_local (traverse_rhs ?sub sigma)) (?g ⊔ genv global_of (sides_of_rhs ?sub sigma))"
using combine_sound[where q = cont'
and r = "dg_local (sigma (Inl (FunctionResult p, ?ex_ctx)))"
and τ = sigma and key = global_of and ci = ?ci, OF ccov tin]
by simp
also have "… = γ⇩D⇩G (dg_local (traverse_program ?alt sigma))
(?g ⊔ genv global_of (sides_of_program ?alt sigma))"
by (simp only: tr sd)
also have "… ⊆ γ⇩D⇩G (dg_local (sigma (Inl (cont, c1)))) ?g"
by (rule gammaDG_mono[OF
routed_comb_bound_local[OF ‹(cl, c1) ∈ vars› ce sin covV_cont Rr mem]
sup_least[OF order_refl
routed_comb_bound_genv[OF ‹(cl, c1) ∈ vars› ce sin covV_cont Rr mem]]])
also have "… = cover cont c1"
using covV_cont by simp
finally show ?thesis .
qed
qed
subsection ‹Activation-collect soundness against the routed local unknown›
text ‹
Every activation-collected store at any ‹(v, ctx)› pair is concretized by the routed
local unknown's own ‹γ⇩M› reading. The five obligations of
\<^locale>‹activation_coverage› are this locale's own facts: the two entry bounds discharge
‹INIT› together, ‹dg_ctx_act_edge› is ‹INTRA›, the CALL and COMB theorems above are
‹CALL› and ‹RETURN›, and ‹routing_total› read through the reader is ‹TOTAL›. An
instance therefore gets its activation-indexed soundness theorem by interpretation alone.
›
lemma routed_call_context_total:
"call_context_total_on cover adm 𝒢 g"
unfolding call_context_total_on_def
proof (intro allI impI)
fix u dst pars args p cont ctx s
assume ce: "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sin: "s ∈ cover u ctx"
have covV: "(u, ctx) ∈ vars"
proof (rule ccontr)
assume "(u, ctx) ∉ vars"
then have "cover u ctx = {}" by (rule sg_uncov)
with sin show False by simp
qed
with sin have "s ∈ gamma_at u ctx" by simp
from routing_total[OF covV ce this]
show "adm u ctx (call_info_of (CallEdge dst pars args) p) s
(call_enter 𝒢 (CallEdge dst pars args) s) ≠ {}" .
qed
theorem activation_collect_dg_sound:
fixes S0 :: "store set" and c⇩0 :: 'c
assumes entry_cov: "(cfg_entry g, c⇩0) ∈ vars"
and init_sound: "S0 ⊆ γ⇩D⇩G d⇩0 e⇩0"
and init_env_le: "e⇩0 ≤ genv global_of sigma"
shows "𝒜⇘𝒢,adm,c⇩0,g,S0⇙ v c ⊆ cover v c"
proof (rule activation_collect_sound[where cover = "cover"], unfold_locales)
fix s0 assume s0mem: "s0 ∈ S0"
have le_local: "d⇩0 ≤ dg_local (sigma (Inl (cfg_entry g, c⇩0)))"
by (rule pp_entry_init_local_bound[OF entry_cov])
have "γ⇩D⇩G d⇩0 e⇩0
⊆ gamma_at (cfg_entry g) c⇩0"
by (rule gammaDG_mono[OF le_local init_env_le])
with s0mem init_sound have "s0 ∈ gamma_at (cfg_entry g) c⇩0" by blast
thus "s0 ∈ cover (cfg_entry g) c⇩0"
using entry_cov by simp
next
fix u a v' c' s' s''
assume "(u, a, v') ∈ intra g" "s' ∈ cover u c'" "s'' ∈ edge_step a s'"
thus "s'' ∈ cover v' c'" by (rule dg_ctx_act_edge)
next
fix u dst pars args p cont c' c'' s'
assume ce: "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sm: "s' ∈ cover u c'"
and Rc: "c'' ∈ adm u c' (call_info_of (CallEdge dst pars args) p) s'
(call_enter 𝒢 (CallEdge dst pars args) s')"
show "call_enter 𝒢 (CallEdge dst pars args) s' ∈ cover (FunctionEntry p) c''"
using routed_context_call[OF ce sm Rc] .
next
fix cl dst pars args p cont c1 c' p' s' t es
assume ce: "(cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sm: "s' ∈ cover cl c1"
and adm: "admits cl c1 p' s' es c'"
and tm: "t ∈ cover (FunctionResult p) c'"
show "combine_collect 𝒢 dst s' t ∈ cover cont c1"
using routed_context_comb[OF ce sm adm tm] .
next
show "call_context_total_on cover adm 𝒢 g"
by (rule routed_call_context_total)
qed
text ‹
Every valid activation trace of a covered program carries some context under this instance's own
‹adm›: the same four EDGE/CALL/COMB/TOTAL facts that bound the buckets above also make
‹activation_coverage› total here, so an example such as
‹Example_Interval_Source_Ctx› can discharge the ‹has_ctx› premise ‹source_sound_from_collecting_cap› asks for without restating the
interpretation itself.
›
lemma routed_valid_activation_trace_has_context:
fixes S0 :: "store set" and c⇩0 :: 'c
assumes entry_cov: "(cfg_entry g, c⇩0) ∈ vars"
and init_sound: "S0 ⊆ γ⇩D⇩G d⇩0 e⇩0"
and init_env_le: "e⇩0 ≤ genv global_of sigma"
and tv: "t ∈ 𝒯⇘𝒢,g,S0⇙"
shows "∃c. activation_context_rel 𝒢 adm c⇩0 g t c"
proof -
interpret G: activation_coverage g S0 cover adm c⇩0 𝒢
proof unfold_locales
fix s0 assume s0mem: "s0 ∈ S0"
have le_local: "d⇩0 ≤ dg_local (sigma (Inl (cfg_entry g, c⇩0)))"
by (rule pp_entry_init_local_bound[OF entry_cov])
have "γ⇩D⇩G d⇩0 e⇩0
⊆ gamma_at (cfg_entry g) c⇩0"
by (rule gammaDG_mono[OF le_local init_env_le])
with s0mem init_sound have "s0 ∈ gamma_at (cfg_entry g) c⇩0" by blast
thus "s0 ∈ cover (cfg_entry g) c⇩0"
using entry_cov by simp
next
fix u a v' c' s' s''
assume "(u, a, v') ∈ intra g" "s' ∈ cover u c'" "s'' ∈ edge_step a s'"
thus "s'' ∈ cover v' c'" by (rule dg_ctx_act_edge)
next
fix u dst pars args p cont c' c'' s'
assume ce: "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sm: "s' ∈ cover u c'"
and Rc: "c'' ∈ adm u c' (call_info_of (CallEdge dst pars args) p) s'
(call_enter 𝒢 (CallEdge dst pars args) s')"
show "call_enter 𝒢 (CallEdge dst pars args) s' ∈ cover (FunctionEntry p) c''"
using routed_context_call[OF ce sm Rc] .
next
fix cl dst pars args p cont c1 c' p' s' t es
assume ce: "(cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
and sm: "s' ∈ cover cl c1"
and adm: "admits cl c1 p' s' es c'"
and tm: "t ∈ cover (FunctionResult p) c'"
show "combine_collect 𝒢 dst s' t ∈ cover cont c1"
using routed_context_comb[OF ce sm adm tm] .
next
show "call_context_total_on cover adm 𝒢 g"
by (rule routed_call_context_total)
qed
show ?thesis using G.valid_activation_trace_has_context[OF tv] by blast
qed
end
subsection ‹The context relation a solved entry-state table induces›
text ‹
A state-dependent policy picks a context from an abstract entry state, and a pure entry
answers a list of them, so one concrete call may be routed to several contexts --- one
per alternative whose continuation covers the caller store and whose entry covers the
entered store. ‹routed_entry_context_rel alts› is exactly that set, for an entry
operation whose alternatives are the pure function ‹alts› of the call information and the
caller's solved local value: it admits ‹ctx'› whenever some alternative has those two
coverings and its ‹route› is ‹ctx'›. Stated as an equivalence, both routed obligations
come for free: adequacy is the definition read forwards, and totality is the alternatives
covering the concrete call at all, which is what \<^const>‹entry_pairs_cover› says. No
decoder of the concrete store is involved: the context is induced by the analyzer's own
decision, as Goblint's ‹context› applied to each ‹enter› alternative induces it.
The relation is stated over ‹alts› rather than over an arbitrary entry run because a run
does not determine its alternative list in general --- over a one-point carrier every
list traverses alike --- while a pure entry's list is the function's own answer.
›
definition routed_entry_context_rel ::
"(call_info ⇒ 'D ⇒ 'D enter_result list)
⇒ ('D ⇒ ('v ⇒ 'G) ⇒ store set) ⇒ (pp × 'c + 'k ⇒ ('D, 'G) dg_state) ⇒ ('v ⇒ 'k)
⇒ (pp ⇒ 'c ⇒ 'D ⇒ call_action ⇒ 'c) ⇒ 'c context_policy"
where
"routed_entry_context_rel alts γ⇩D⇩G sigma global_of route u ctx ci caller entered =
{ctx'. ∃cont entry.
(cont, entry) ∈ set (alts ci (dg_local (sigma (Inl (u, ctx)))))
∧ caller ∈ γ⇩D⇩G cont (genv global_of sigma)
∧ entered ∈ γ⇩D⇩G entry (genv global_of sigma)
∧ ctx' = route u ctx entry (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci))}"
lemma routed_entry_context_relI:
assumes "(cont, entry) ∈ set (alts ci (dg_local (sigma (Inl (u, ctx)))))"
and "caller ∈ γ⇩D⇩G cont (genv global_of sigma)"
and "entered ∈ γ⇩D⇩G entry (genv global_of sigma)"
shows "route u ctx entry (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci))
∈ routed_entry_context_rel alts γ⇩D⇩G sigma global_of route u ctx ci caller entered"
using assms unfolding routed_entry_context_rel_def by blast
text ‹Invoke with ‹obtain›: the alternative is a witness the classical reasoner should not
be left to guess.›
lemma routed_entry_context_relE:
assumes
"ctx' ∈ routed_entry_context_rel alts γ⇩D⇩G sigma global_of route u ctx ci caller entered"
obtains cont entry
where "(cont, entry) ∈ set (alts ci (dg_local (sigma (Inl (u, ctx)))))"
and "caller ∈ γ⇩D⇩G cont (genv global_of sigma)"
and "entered ∈ γ⇩D⇩G entry (genv global_of sigma)"
and "ctx' = route u ctx entry (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci))"
using assms unfolding routed_entry_context_rel_def by blast
text ‹Totality is the alternatives covering the concrete call: exactly the
\<^const>‹entry_pairs_cover› obligation every routed instance already carries.›
lemma routed_entry_context_rel_total:
assumes "entry_pairs_cover (λd. γ⇩D⇩G d (genv global_of sigma)) caller entered
(alts ci (dg_local (sigma (Inl (u, ctx)))))"
shows
"routed_entry_context_rel alts γ⇩D⇩G sigma global_of route u ctx ci caller entered ≠ {}"
using assms unfolding routed_entry_context_rel_def
by blast
subsection ‹Formal-entry contexts: routing on the callee's declared formals›
text ‹
A context type derived from the callee's declared formals rather than call-site
history: ‹'a list›, one abstract value per formal, in the order \<^const>‹CallEdge›
already carries them --- populated at compile time from the callee's own
declaration, so no separate procedure-table lookup is needed here.
‹formals_context› is the plain per-variable projection (\<^typ>‹'a abs_state› is
\<^typ>‹vname ⇒ 'a›, so this is just \<^const>‹map›), and the routing functions
below apply it to the state they are handed. That state is already the
∗‹entered› callee frame:
\<^const>‹routed_callee_call_program› runs the specification's own enter transfer first and
passes its answer to ‹route›, so a routing function must not enter again.
‹formals_context_sem› is the trace-semantic counterpart, decoding the concrete
entered store's formals the same way, given the point abstraction ‹decode› a
domain provides for a concrete value and the CFG needed to look up a call
site's own formal list. Neither definition mentions a domain-specific accessor
beyond ‹decode› itself, nor a specification, so any domain reusing
\<^locale>‹routed_context› instantiates this pair once instead of
hand-writing a per-formal projection.
›
definition formals_context :: "vname list ⇒ 'a abs_state ⇒ 'a list" where
"formals_context pars d = map d pars"
text ‹The formals of the call originating at ‹u›: at most one, by the compiler's
own invariant (‹Voblint_Compile.VIMP_Proc_to_CFG› emits a single \<^const>‹CallEdge›
per \<^const>‹Call›); ‹[]› if ‹u› has none.›
definition formals_at_call_site :: "cfg ⇒ pp ⇒ vname list" where
"formals_at_call_site g u =
(case filter (λ(c, ca, ce, k). c = u) (cfg_calls_list g) of
(_, CallEdge _ pars _, _, _) # _ ⇒ pars
| _ ⇒ [])"
definition formals_context_sem ::
"cfg ⇒ (int ⇒ 'a) ⇒ cfg_node ⇒ 'a list ⇒ store ⇒ 'a list"
where
"formals_context_sem g decode u ctx s = formals_context (formals_at_call_site g u) (decode ∘ s)"
text ‹
The whole matched \<^type>‹call_action› at a node, not only its formals: an
‹enterc› built purely from the caller's own solved abstract state (rather than
by decoding the concrete entered store, as \<^const>‹formals_context_sem› does) needs
the callee's actuals too, to recompute the same \<^const>‹dgs_enter› the route
itself already ran. Same convention as \<^const>‹formals_at_call_site›: the head
of the filtered call list, ‹CallEdge None [] []› if ‹u› has no outgoing call.
›
definition call_action_at_call_site :: "cfg ⇒ pp ⇒ call_action" where
"call_action_at_call_site g u =
(case filter (λ(c, ca, ce, k). c = u) (cfg_calls_list g) of
(_, ca, _, _) # _ ⇒ ca
| _ ⇒ CallEdge None [] [])"
text ‹
Not a locale theorem, same as routing agreement itself: whether a node has at
most one outgoing call is a per-instance fact about ‹g›, true for
‹compile_prog› output (‹Voblint_Compile.VIMP_Proc_to_CFG›'s
‹compile_prog_calls_source_unique›) but not for an arbitrary hand-built CFG.
›
lemma calls_filter_singleton:
assumes fin: "finite (calls g)"
and uniq: "⋀ca1 ce1 af1 ca2 ce2 af2.
(u, ca1, ce1, af1) ∈ calls g ⟹ (u, ca2, ce2, af2) ∈ calls g
⟹ ca1 = ca2 ∧ ce1 = ce2 ∧ af1 = af2"
and ce: "(u, ca, cf, af) ∈ calls g"
shows "filter (λ(c, ca, ce, k). c = u) (cfg_calls_list g) = [(u, ca, cf, af)]"
proof -
let ?P = "λ(c, ca, ce, k). c = u"
let ?L = "cfg_calls_list g"
have mem: "(u, ca, cf, af) ∈ set ?L" using ce fin by simp
have distinctL: "distinct ?L" unfolding cfg_calls_list_code by (rule distinct_sorted_list_of_set)
have "set (filter ?P ?L) = {(u, ca, cf, af)}"
proof (rule set_eqI, rule iffI)
fix x assume hx: "x ∈ set (filter ?P ?L)"
then have memx: "x ∈ set ?L" and px: "?P x" by auto
obtain c ca' ce' af' where x: "x = (c, ca', ce', af')" by (cases x) auto
from px x have cU: "c = u" by simp
from memx x cU fin have "(u, ca', ce', af') ∈ calls g" by simp
with uniq[OF ce] have "ca' = ca" "ce' = cf" "af' = af" by auto
thus "x ∈ {(u, ca, cf, af)}" using x cU by simp
next
fix x assume "x ∈ {(u, ca, cf, af)}"
thus "x ∈ set (filter ?P ?L)" using mem by simp
qed
moreover have "distinct (filter ?P ?L)" using distinctL by (rule distinct_filter)
ultimately show ?thesis
apply (cases "filter (λ(c, ca, ce, k). c = u) (cfg_calls_list g)")
using singleton_iff subset_singletonD by(fastforce)+
qed
lemma call_action_at_call_site_eq:
assumes fin: "finite (calls g)"
and uniq: "⋀ca1 ce1 af1 ca2 ce2 af2.
(u, ca1, ce1, af1) ∈ calls g ⟹ (u, ca2, ce2, af2) ∈ calls g
⟹ ca1 = ca2 ∧ ce1 = ce2 ∧ af1 = af2"
and ce: "(u, ca, cf, af) ∈ calls g"
shows "call_action_at_call_site g u = ca"
unfolding call_action_at_call_site_def
using calls_filter_singleton[OF fin uniq ce] by simp
subsection ‹Formal-entry contexts at the routed spine's lifted carrier›
text ‹
\<^const>‹formals_context› above operates on the unlifted
\<^typ>‹'a abs_state›, the shape an abstract-carrier \<^locale>‹routed_context› caller state
has. The routed executable spine (\<^locale>‹dg_context_activation›, every current
instance) instead carries \<^typ>‹'a abs_state lifted› throughout, to represent an
activation the solver has not yet covered. ‹formals_route_lifted›/
‹formals_route_lifted_gen› are the same formal-entry projection at that carrier:
a caller point that is \<^const>‹Bot› routes to the all-‹bot› formal context (the
entered callee frame is then \<^const>‹Bot› too), the same collapse an EntryState
routed instance needs for its own executable/abstract route. Like the
projection above, these read the state they are handed and never re-enter, so
neither mentions a specification.
›
definition formals_route_lifted ::
"'a::numeric_domain abs_state lifted ⇒ call_action ⇒ 'a list"
where
"formals_route_lifted d ca =
(case ca of CallEdge dst pars args ⇒
formals_context pars (case d of Bot ⇒ bot | Lifted d0 ⇒ d0))"
definition formals_route_lifted_gen ::
"pp ⇒ 'a list ⇒ 'a::numeric_domain abs_state lifted ⇒ call_action ⇒ 'a list"
where
"formals_route_lifted_gen u ctx d ca = formals_route_lifted d ca"
end