Theory VIMP_Globals

theory VIMP_Globals
  imports VIMP_Syntax
begin

section ‹Locals and globals over the scalar store›

text ‹
  The store is one ‹vname ⇒ int› function; the locals/globals split is a
  classifier ‹𝒢 :: vname ⇒ bool› on top of it. A call needs both halves of
  that split: ‹enter_state› keeps the globals and resets the locals on entry,
  ‹combine_env caller callee› restores the caller's locals and keeps the
  callee's globals on exit.

  ‹combine_env› is the single pointwise selector, generic in both key and
  codomain. ‹enter_frame› specializes it with a constant reset map. The
  concrete semantics uses these operations at ‹store = vname ⇒ int›, while
  abstract states reuse them at their own codomain.
›

type_synonym pname = String.literal

definition combine_env ::
    "('k ⇒ bool) ⇒ ('k ⇒ 'a) ⇒ ('k ⇒ 'a) ⇒ ('k ⇒ 'a)" where
  "combine_env 𝒢 s t = (λn. if 𝒢 n then t n else s n)"

definition enter_frame :: "('k ⇒ bool) ⇒ 'a ⇒ ('k ⇒ 'a) ⇒ ('k ⇒ 'a)" where
  "enter_frame 𝒢 reset_val s = combine_env 𝒢 (λ_. reset_val) s"

definition enter_state :: "(vname ⇒ bool) ⇒ store ⇒ store" where
  "enter_state 𝒢 s = enter_frame 𝒢 0 s"

lemma combine_query [simp]:
  "combine_env 𝒢 s t n = (if 𝒢 n then t n else s n)"
  unfolding combine_env_def by simp

lemma enter_frame_apply [simp]:
  "enter_frame 𝒢 reset_val s n = (if 𝒢 n then s n else reset_val)"
  unfolding enter_frame_def by simp

lemma enter_state_apply [simp]:
  "enter_state 𝒢 s n = (if 𝒢 n then s n else 0)"
  unfolding enter_state_def by simp

lemma combine_collapse [simp]:
  "combine_env 𝒢 s s = s"
  by (rule ext) simp

lemma combine_nest_left [simp]:
  "combine_env 𝒢 (combine_env 𝒢 s t) u = combine_env 𝒢 s u"
  by (rule ext) simp

lemma combine_nest_right [simp]:
  "combine_env 𝒢 s (combine_env 𝒢 t u) = combine_env 𝒢 s u"
  by (rule ext) simp

section ‹C-faithful initial store set›

text ‹
  VIMP approximates C startup by initializing every global with no explicit
  initializer to 0 and leaving every other name of the initial store
  unconstrained. ‹cinit_stores› is the corresponding set of concrete stores:
  those where every global is 0, so ‹main›'s locals may hold any integer. It
  constrains only the initial store. A callee's locals do not come from it:
  ‹enter_state› resets them to 0 on every entry, which defines what C leaves
  indeterminate, as ‹c_div› defines division by zero. Neither convention is a
  model of C's indeterminate-value or undefined-behaviour rules, and VIMP has no
  global initializer syntax for a declaration such as ‹int x = 42;› to diverge
  from.
›

definition cinit_stores :: "(vname ⇒ bool) ⇒ store set" where
  "cinit_stores 𝒢 = {s. ∀x. 𝒢 x ⟶ s x = 0}"

end