Theory Exec_DG_State

theory Exec_DG_State
  imports Default_St_Restriction_Refinement "Voblint_Framework.DG_Constraint_Programs"
begin

section ‹The executable carrier and the functions it represents›

text ‹
  The verified solver uses the executable association-list carrier ‹'a default_st›, while
  soundness is stated over function-valued abstract states. This theory is the bottom of the
  bridge: the D/G product's lattice structure and ‹dg_state_to_fun›, which lifts
  \<^const>‹default_st_to_fun› to that product: the pair of functions a D/G state
  represents, parametric in the classifier. Everything here is carrier-level -- no specification, no transfer, no equation shape -- so a
  domain's executable mirror is related to its abstract state once, here, and the
  specification layers above never restate it.

  D/G lattice operations are componentwise, so the product inherits the order, join, bottom,
  equality, and widening operations the solver requires.
›


subsection ‹Classifier-parametric represented function›

text ‹
  The function a local or side state represents is \<^const>‹default_st_to_fun›,
  generic in the classifier: an executable state is written with a declaration-driven
  classifier, so its function needs the same classifier or it consults the wrong slot.
  ‹dg_state_to_fun› applies it to both components.
›

definition dg_state_to_fun ::
  "(vname => bool) =>
   (('a::bot) default_st, ('b::bot) default_st) dg_state => ('a abs_state, 'b abs_state) dg_state"
where
  "dg_state_to_fun 𝒢 d =
    DG (ρ⇘𝒢⇙ (dg_local d)) (ρ⇘𝒢⇙ (dg_global d))"

adhoc_overloading readback == dg_state_to_fun

lemma dg_state_to_fun_simps [simp]:
  "dg_local (ρ⇘𝒢⇙ d) = ρ⇘𝒢⇙ (dg_local d)"
  "dg_global (ρ⇘𝒢⇙ d) = ρ⇘𝒢⇙ (dg_global d)"
  "ρ⇘𝒢⇙ (DG a b) = DG (ρ⇘𝒢⇙ a) (ρ⇘𝒢⇙ b)"
  by (simp_all add: dg_state_to_fun_def)

lemma dg_state_to_fun_bot [simp]:
  "ρ⇘𝒢⇙ (bot :: ('a::bounded_semilattice_sup_bot default_st,
                         'b::bounded_semilattice_sup_bot default_st) dg_state) = bot"
  by (simp add: bot_dg_state_def)
end