Theory DG_Ctx_Activation
theory DG_Ctx_Activation
imports DG_Spec_Sound DG_Indexed_Generator
"Voblint_Domain.Nonrelational_State"
begin
section ‹What a solved routed system says about one program point›
text ‹
A post-solution bounds a right-hand side by the value at its own unknown and
every published side effect by the value at its target key.
‹dg_context_activation› fixes such a solution over the routed generator, a
set ‹vars› of keys whose own equations it bounds, and a reader ‹sg› that
answers the empty set off ‹vars›. The set may contain every key the solver
visited or any subset. These facts derive the EDGE obligation the activation
backbone asks for; ‹Routed_Context› derives COMB for the routed call shape.
Entry and callee-seed coverage remain with the concrete analysis.
Both carriers are parameters: ‹γ⇩D⇩G› interprets a D/G pair, while
‹γ⇩M› interprets whatever ‹sg› returns. An analysis whose reader is not an
‹abs_state› therefore instantiates this locale directly. The generator
buffers its writes at ‹Inr buffer_key›; ‹global_of› names the key each global
name is read from, and ‹sg_cov› ties the reader at a covered key to
‹γ⇩D⇩G› of the local slot against the environment \<^term>‹genv global_of sigma›.
›
locale dg_context_activation = analysis_contract S γ⇩D⇩G 𝒢
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" +
fixes g :: cfg and buffer_key :: 'k and global_of :: "'v ⇒ 'k"
and route :: "pp ⇒ 'c ⇒ 'D ⇒ call_action ⇒ 'c"
and cmb :: "(pp ⇒ 'c ⇒ 'D ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ call_action ⇒ pp ⇒ pp
⇒ (pp × 'c, 'k, ('D, 'G) dg_state, ('D, 'G) dg_state) strategy_program"
and extra :: "(pp ⇒ 'c ⇒ 'D ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ pp
⇒ (pp × 'c, 'k, ('D, 'G) dg_state, ('D, 'G) dg_state) strategy_program list"
and bot0 d⇩0 :: 'D and g⇩0 :: 'G
and sigma :: "pp × 'c + 'k ⇒ ('D, 'G) dg_state"
and vars :: "(pp × 'c) set" and x0 :: "pp × 'c"
and sg :: "pp × 'c + 'k ⇒ 'M"
and γ⇩M :: "'M ⇒ store set"
assumes cmb_wf: "⋀c ca cc v. sp_wf (cmb route c ca cc v)"
and : "⋀c v q. q ∈ set (extra route c v) ⟹ sp_wf q"
and finE: "finite (intra g)"
and pp: "post_bounded
(routed_node_rhs intra_predecessor_addr_list call_site_list (λ_. buffer_key)
route (λc src a. dg_spec_edge_program S a src global_of) cmb extra g bot0 d⇩0 g⇩0)
x0 sigma vars"
and sg_cov[simp]: "⋀v c. (v, c) ∈ vars
⟹ γ⇩M (sg (Inl (v, c))) =
γ⇩D⇩G (dg_local (sigma (Inl (v, c)))) (genv global_of sigma)"
and sg_uncov[simp]: "⋀v c. (v, c) ∉ vars
⟹ γ⇩M (sg (Inl (v, c))) = {}"
and fwd: "⋀u a v c. (u, c) ∈ vars
⟹ γ⇩D⇩G (dg_local (sigma (Inl (u, c)))) (genv global_of sigma) ≠ {}
⟹ (u, a, v) ∈ intra g
⟹ (v, c) ∈ vars"
begin
abbreviation Gen :: "(pp × 'c, 'k, ('D, 'G) dg_state) eqsT" where
"Gen ≡ routed_node_rhs intra_predecessor_addr_list call_site_list (λ_. buffer_key)
route (λc src a. dg_spec_edge_program S a src global_of) cmb extra g bot0 d⇩0 g⇩0"
abbreviation acc0 :: "pp ⇒ 'D" where
"acc0 v ≡ (if v = cfg_entry g then bot0 ⊔ d⇩0 else bot0)"
abbreviation contribs :: "pp ⇒ 'c
⇒ (pp × 'c, 'k, ('D, 'G) dg_state, ('D, 'G) dg_state) strategy_program list" where
"contribs v ctx ≡
routed_contribution_programs intra_predecessor_addr_list call_site_list route
(λc src a. dg_spec_edge_program S a src global_of) cmb extra g ctx v"
text ‹The reader's claim at a covered point (‹sg_cov›) and the manager its call
programs run under. Input-only, so facts of theory-level interpretations keep printing
the explicit terms.›
abbreviation (input) gamma_at :: "pp ⇒ 'c ⇒ store set" where
"gamma_at v ctx ≡ γ⇩D⇩G (dg_local (sigma (Inl (v, ctx)))) (genv global_of sigma)"
abbreviation (input) man_at where
"man_at v ctx ≡ mk_dg_man (dg_local (sigma (Inl (v, ctx)))) global_of"
text ‹Every contribution the routed generator folds here runs its continuation
once: the edge hook is a compiled specification step, and the call and extra
hooks carry their own well-formedness as locale assumptions.›
lemma contribs_wf [simp]: "∀q ∈ set (contribs v ctx). sp_wf q"
by (rule routed_contribution_programs_wf)
(auto intro: sp_wf_dg_spec_edge_program[OF spec_wf] cmb_wf extra_wf)
subsection ‹Post-solution elimination›
text ‹The solver hypothesis, unpacked once into the two bounds every later proof uses: at a
covered unknown the generated right-hand side is below the stored local, and its side
writes are below the stored globals. Everything downstream cites these instead of
\<^const>‹part_post_solution›.›
lemma pp_eq_bound:
"(v, ctx) ∈ vars ⟹ eq Gen (v, ctx) sigma ≤ sigma (Inl (v, ctx))"
by (rule tree_covered_at_local[OF post_boundedD[OF pp]])
lemma pp_sides_bound:
"(v, ctx) ∈ vars ⟹ sides_of_rhs (Gen (v, ctx)) sigma ≤ sigma"
by (rule tree_covered_at_sides[OF post_boundedD[OF pp]])
lemma pp_entry_init_global_bound:
assumes cov: "(cfg_entry g, ctx) ∈ vars"
shows "g⇩0 ≤ dg_global (sigma (Inr buffer_key))"
proof -
have "g⇩0 ≤ dg_global (sides_of_rhs (Gen (cfg_entry g, ctx)) sigma (Inr buffer_key))"
unfolding routed_node_rhs_def Let_def
by (simp add: Let_def sup_dg_state_def)
also have "… ≤ dg_global (sigma (Inr buffer_key))"
using pp_sides_bound[OF cov, THEN le_funD, of "Inr buffer_key"]
by (simp add: less_eq_dg_state_def)
finally show ?thesis .
qed
text ‹The local-carrier twin, proved the same way: ‹Gen›'s entry accumulator starts at
‹bot0 ⊔ d⇩0›, ‹side_acc_dg_ge_acc› only grows it, and ‹pp_eq_bound› transports the
bound across a covered point's own equation.›
lemma pp_entry_init_local_bound:
assumes cov: "(cfg_entry g, ctx) ∈ vars"
shows "d⇩0 ≤ dg_local (sigma (Inl (cfg_entry g, ctx)))"
proof -
have "d⇩0 ≤ dg_local (eq Gen (cfg_entry g, ctx) sigma)"
by (simp add: eq_routed_node_rhs[OF contribs_wf])
(rule order_trans[OF _ side_acc_dg_ge_acc], simp add: le_supI2)
also have "… ≤ dg_local (sigma (Inl (cfg_entry g, ctx)))"
using pp_eq_bound[OF cov] by (simp add: less_eq_dg_state_def)
finally show ?thesis .
qed
subsection ‹The entry Side wrapper only grows the sides›
text ‹At the entry the generator wraps its fold in one extra ‹Side› carrying the seed
global, so a side read of the wrapped tree dominates the same read of the fold. Bounds
proved against the fold therefore transport to \<^const>‹routed_node_rhs› without a separate
entry case.›
lemma sides_fold_le_Gen:
"(sides_of_program (side_rhs_fold_dg (acc0 v) (contribs v ctx)) sigma) k
≤ sides_of_rhs (Gen (v, ctx)) sigma k"
unfolding routed_node_rhs_def Let_def
by (cases "v = cfg_entry g") (auto simp: Let_def intro: sup.cobounded1)
subsection ‹EDGE: the routed intra bounds and the guarded transport›
text ‹Every intra predecessor of ‹v› contributes its edge program to ‹v›'s own fold, so
both bounds below are the post-solution read off that one membership.›
lemma edge_program_mem_contribs:
assumes e: "(u, a, v) ∈ intra g"
shows "dg_spec_edge_program S a (Inl (u, ctx)) global_of ∈ set (contribs v ctx)"
proof -
have "(Inl (u, ctx), a) ∈ set (intra_predecessor_addr_list g v ctx)"
using e by (force simp: intra_predecessor_addr_list_def
set_intra_predecessor_list[OF finE] intra_predecessors_def)
thus ?thesis by (force simp: routed_contribution_programs_def)
qed
lemma edge_bound_local:
assumes cov_v: "(v, ctx) ∈ vars"
and e: "(u, a, v) ∈ intra g"
shows "edge_out S a (Inl (u, ctx)) global_of sigma ≤ dg_local (sigma (Inl (v, ctx)))"
proof -
have "edge_out S a (Inl (u, ctx)) global_of sigma
≤ side_acc_dg (acc0 v) sigma (contribs v ctx)"
using dg_local_traverse_le_side_acc_dg[OF edge_program_mem_contribs[OF e]] .
also have "… = dg_local (eq Gen (v, ctx) sigma)"
by (simp add: eq_routed_node_rhs[OF contribs_wf])
also have "… ≤ dg_local (sigma (Inl (v, ctx)))"
using pp_eq_bound[OF cov_v] by (simp add: less_eq_dg_state_def)
finally show ?thesis .
qed
lemma edge_bound_global:
assumes cov_v: "(v, ctx) ∈ vars"
and e: "(u, a, v) ∈ intra g"
shows "dg_global (sides_of_program (dg_spec_edge_program S a (Inl (u, ctx)) global_of) sigma (Inr k))
≤ dg_global (sigma (Inr k))"
proof -
have "dg_global (sides_of_program (dg_spec_edge_program S a (Inl (u, ctx)) global_of) sigma (Inr k))
≤ dg_global ((sides_of_program (side_rhs_fold_dg (acc0 v) (contribs v ctx)) sigma) (Inr k))"
using sides_le_side_rhs_fold_dg[OF contribs_wf edge_program_mem_contribs[OF e], where k =
"Inr k"]
by (simp add: less_eq_dg_state_def)
also have "… ≤ dg_global (sides_of_rhs (Gen (v, ctx)) sigma (Inr k))"
using sides_fold_le_Gen[where k = "Inr k"]
by (simp add: less_eq_dg_state_def)
also have "… ≤ dg_global (sigma (Inr k))"
using pp_sides_bound[OF cov_v, THEN le_funD, of "Inr k"]
by (simp add: less_eq_dg_state_def)
finally show ?thesis .
qed
lemma edge_bound_genv:
assumes cov_v: "(v, ctx) ∈ vars"
and e: "(u, a, v) ∈ intra g"
shows "edge_pub S a (Inl (u, ctx)) global_of sigma ≤ genv global_of sigma"
unfolding le_fun_def genv_def using edge_bound_global[OF cov_v e] by blast
theorem dg_ctx_act_edge:
assumes e: "(u, a, v) ∈ intra g"
and sin: "s ∈ γ⇩M (sg (Inl (u, ctx)))" and st: "s' ∈ edge_step a s"
shows "s' ∈ γ⇩M (sg (Inl (v, ctx)))"
proof (cases "(u, ctx) ∈ vars")
case False
hence "γ⇩M (sg (Inl (u, ctx))) = {}" by (rule sg_uncov)
thus ?thesis using sin by simp
next
case True
let ?d = "dg_local (sigma (Inl (u, ctx)))"
let ?g = "genv global_of sigma"
have sin': "s ∈ γ⇩D⇩G ?d ?g"
using sin True by simp
have cov_v: "(v, ctx) ∈ vars"
using True _ e by (rule fwd) (use sin' in blast)
have "{s} ⊆ γ⇩D⇩G ?d ?g" using sin' by simp
hence "edge_collect a {s} ⊆ edge_collect a (γ⇩D⇩G ?d ?g)" by (rule edge_collect_mono)
moreover have "s' ∈ edge_collect a {s}" using st by (simp add: edge_collect_single)
ultimately have "s' ∈ edge_collect a (γ⇩D⇩G ?d ?g)" by blast
hence "s' ∈ γ⇩D⇩G
(edge_out S a (Inl (u, ctx)) global_of sigma)
(?g ⊔ edge_pub S a (Inl (u, ctx)) global_of sigma)"
using step_sound[of a sigma "Inl (u, ctx)" global_of] by blast
also have "… ⊆ gamma_at v ctx"
by (rule gammaDG_mono[OF edge_bound_local[OF cov_v e]
sup_least[OF order_refl edge_bound_genv[OF cov_v e]]])
also have "… = γ⇩M (sg (Inl (v, ctx)))"
using cov_v by simp
finally show ?thesis .
qed
end
end