Theory Example_Keyed_Global_Footprint

theory Example_Keyed_Global_Footprint
  imports
    "Voblint_Framework.DG_Keyed_Split_Spec"
begin

section ‹Keyed globals: an edge depends on what it reads and publishes what it writes›

text ‹
  Two declared globals ‹g› and ‹h›. Under the keyed lifter an edge's program
  depends on its source point and on the unknowns of the globals its expressions
  mention, and it publishes exactly at the unknowns of the globals it may assign.
  Updating ‹h› therefore cannot destabilize a point that reads only ‹g›: no
  equation reading ‹g› names ‹h›'s unknown.
›

definition gh :: "vname ⇒ bool" where "gh x ⟷ x ∈ {STR ''g'', STR ''h''}"

abbreviation read_g :: edge_action where
  "read_g ≡ EA_Assign (STR ''x'') (Plus (V (STR ''g'')) (N 1))"

abbreviation write_h :: edge_action where
  "write_h ≡ EA_Assign (STR ''h'') (N 1)"

lemma read_g_footprint:
  "edge_global_reads gh read_g = [STR ''g'']" "edge_global_writes gh read_g = []"
  by (simp_all add: gh_def edge_global_reads_def edge_global_writes_def edge_reads_def
      global_names_in_def)

lemma write_h_footprint:
  "edge_global_reads gh write_h = []" "edge_global_writes gh write_h = [STR ''h'']"
  by (simp_all add: gh_def edge_global_reads_def edge_global_writes_def edge_reads_def
      global_names_in_def)

text ‹The keyed program for ‹x := g + 1› depends on ‹g›'s unknown and nothing else global.›

lemma read_g_depends_on_g_only:
  "dep_program τ (transfer_program (keyed_transfer cmb rl rg free
      (edge_global_reads gh read_g) (edge_global_writes gh read_g) f) src key)
     = {src, Inr (key (STR ''g''))}"
  by (simp add: dep_keyed_transfer read_g_footprint)

text ‹The keyed program for ‹h := 1› publishes at ‹h›'s unknown and nowhere else.›

lemma write_h_publishes_h_only:
  "side_path τ (sp_compile (transfer_program (keyed_transfer cmb rl rg free
      (edge_global_reads gh write_h) (edge_global_writes gh write_h) f) src key))
     = [key (STR ''h'')]"
  by (simp add: side_path_keyed_transfer write_h_footprint)

end