Theory Default_St_Base

theory Default_St_Base
  imports "Voblint_VIMP.VIMP_Syntax" "HOL-Library.AList"
begin

section ‹Finite default-map representation›

text ‹
  An abstract state has to be a finite thing before a solver can run on it. A
  ‹default_dict› is a finite dictionary that answers every name it does not
  list with a default. A ‹default_st_rep› is two of them, one per partition:
  a local dictionary and a global one. Reading a location consults the
  dictionary of its partition. Nothing forces a stored value to differ from
  its default.

  Two such pairs can describe the same reading, so the type is quotiented by
  agreement of all lookups. That identifies list order and redundant duplicate
  entries only where they do not affect the reading: \<^const>‹map_of› answers
  with the first match, so reordering entries that disagree on a key is a
  genuine change and the quotient keeps it.

  This theory settles the representation, that quotient, and the order,
  equality and point update defined on it. It does not decide which variable
  names are local and which are global -- a ‹location› records a
  classification this theory never makes. That classifier arrives only in
  ‹Default_St_Transfer›, which is built on this.
›

text ‹
  ❙‹Why two defaults, rather than a sparse map over a fixed ‹top›.›
  Nipkow's ‹Abs_State› stores only the variables it has heard of and reads
  every other one as ‹top›. That is the smaller representation, and it makes
  the order and the join shorter to state, so the extra pair of defaults here
  needs a reason. Three, in fact, and each is load-bearing on its own.

  ▪ ❙‹C zero-initialization.› Every domain's entry state gives globals a
    non-‹top› value and locals ‹top› --- ‹⟪(STop, []), (SZero, [])⟫› for
    Sign, and the parity, interval and product analyses match it. It
    over-approximates ‹cinit_stores 𝒢 = {s. ∀x. 𝒢 x ⟶ s x = 0}›, which
    quantifies over ∗‹all› names the classifier calls global, for an arbitrary
    classifier and with no finiteness hypothesis. A fixed-‹top› map can only
    express that by materializing every global, which makes the entry state a
    function of the program's declaration list and pushes that dependency into
    every soundness statement that mentions it.

  ▪ ❙‹The ownership split needs ‹bot› on the discarded side.› Publishing a
    state's global half to a shared unknown sends locals to ‹bot›, and ‹bot› is
    what makes that half a unit for the join that combines publications from
    every call site. ‹top› there would not be a unit. These half-states are not
    transient: they are stored in solver unknowns and compared against the
    solution.

  ▪ ❙‹The solver needs a least element on this type.› The ownership-split
    specification types both its local and global unknowns at this carrier and
    demands ‹bounded_semilattice_sup_bot› of it, so unknowns can start at
    ‹bot›. That element is the everywhere-‹bot› state, which a sparse map over a
    fixed ‹top› cannot represent at all.

  What the defaults cost is visible throughout this theory: the order has to
  compare them, extensional equality has to pin them, and the emptiness test in
  ‹Default_St_Reachability› has to reason about them. That cost is the price of the
  three points above, not an accident of the first representation tried.
›

subsection ‹Default dictionaries›

type_synonym 'a default_dict = "'a × (vname × 'a) list"

fun default_dict_get :: "'a default_dict => vname => 'a" where
  "default_dict_get (d, ps) x = (case map_of ps x of Some a => a | None => d)"

fun default_dict_set :: "'a default_dict => vname => 'a => 'a default_dict" where
  "default_dict_set (d, ps) x a = (d, (x, a) # AList.delete x ps)"

lemma map_of_resolved_delete:
  "map_of (AList.delete k ps) k' =
     (if k = k' then None else map_of ps k')"
  by (simp add: AList.delete_conv')

lemma map_of_resolved_none_iff:
  "map_of ps k = None ⟷ k ∉ set (map fst ps)"
  by (induction ps) auto

lemma default_dict_get_set [simp]:
  "default_dict_get (default_dict_set m x a) y =
     (if x = y then a else default_dict_get m y)"
  by (cases m) (simp add: map_of_resolved_delete)

text ‹
  A name escaping a finite list, drawn from any infinite supply. It is not
  listed, so a dictionary answers it with its default. Consumers instantiate
  the supply with all vnames, or with the ones a classifier leaves local.
›

lemma obtain_fresh_vname:
  assumes "infinite A"
  obtains x where "x ∈ A" and "x ∉ set xs"
proof -
  have "infinite (A - set xs)"
    by (rule Diff_infinite_finite[OF _ assms]) simp
  then obtain x where "x ∈ A - set xs"
    using infinite_imp_nonempty by blast
  then have "x ∈ A" "x ∉ set xs" by simp_all
  then show thesis by (rule that)
qed

text ‹
  The order on one dictionary compares the defaults and the finitely many
  listed names. An unlisted name reads the default on both sides, so this
  decides the pointwise order over all names.
›

fun le_default_dict :: "('a::order) default_dict => 'a default_dict => bool" where
  "le_default_dict (d, ps) (e, qs) ⟷
     d ≤ e ∧
     list_all (λx. default_dict_get (d, ps) x ≤ default_dict_get (e, qs) x)
       (map fst ps @ map fst qs)"

lemma le_default_dict_iff:
  "le_default_dict m n ⟷ (∀x. default_dict_get m x ≤ default_dict_get n x)"
proof -
  obtain d ps where m: "m = (d, ps)" by (cases m)
  obtain e qs where n: "n = (e, qs)" by (cases n)
  show ?thesis
  proof
    assume le: "le_default_dict m n"
    show "∀x. default_dict_get m x ≤ default_dict_get n x"
    proof
      fix x
      show "default_dict_get m x ≤ default_dict_get n x"
      proof (cases "x ∈ set (map fst ps @ map fst qs)")
        case True
        with le show ?thesis unfolding m n
          by (auto simp: list_all_iff simp del: default_dict_get.simps)
      next
        case False
        then have "map_of ps x = None" "map_of qs x = None"
          by (simp_all add: map_of_resolved_none_iff)
        with le show ?thesis unfolding m n by simp
      qed
    qed
  next
    assume le: "∀x. default_dict_get m x ≤ default_dict_get n x"
    obtain y :: vname where "y ∈ UNIV" and fresh: "y ∉ set (map fst ps @ map fst qs)"
      by (rule obtain_fresh_vname[OF infinite_literal])
    then have "map_of ps y = None" "map_of qs y = None"
      by (simp_all add: map_of_resolved_none_iff)
    with le[rule_format, of y] have "d ≤ e" unfolding m n by simp
    with le show "le_default_dict m n" unfolding m n by (simp add: list_all_iff)
  qed
qed

subsection ‹Locations and raw lookup›

text ‹
  A ‹location› names a local or a global variable, and a raw state is a
  pair of dictionaries read by ‹default_st_rep_get›.
›

datatype location =
  Local_Location (location_vname: vname)
| Global_Location (location_vname: vname)

lemma all_location_iff:
  "(∀loc. P loc) ⟷ (∀x. P (Local_Location x)) ∧ (∀x. P (Global_Location x))"
  by (metis location.exhaust)

text ‹The local dictionary comes first, the global one second.›

type_synonym 'a default_st_rep = "'a default_dict × 'a default_dict"

fun default_st_rep_get ::
  "('a::bot) default_st_rep => location => 'a" where
  "default_st_rep_get (l, g) (Local_Location x) = default_dict_get l x"
| "default_st_rep_get (l, g) (Global_Location x) = default_dict_get g x"

subsection ‹Extensional equality›

text ‹
  Two raw states are equal when they agree on every location's lookup, whatever
  their dictionaries look like; ‹eq_default_st_rep› is an equivalence.
›

definition eq_default_st_rep ::
  "('a::bot) default_st_rep => 'a default_st_rep => bool"
where
  "eq_default_st_rep s t ⟷
     default_st_rep_get s = default_st_rep_get t"

lemma equivp_eq_default_st_rep: "equivp eq_default_st_rep"
  unfolding eq_default_st_rep_def
  by (rule equivpI) (auto intro: reflpI sympI transpI)

text ‹
  The two rules every congruence proof below goes through: a raw operation
  respects \<^const>‹eq_default_st_rep› exactly when its lookup equation says the
  result depends on the arguments only through their lookups.  Stating that
  once keeps the individual congruence proofs down to their own lookup rules.
›

lemma eq_default_st_repI [intro]:
  assumes "⋀loc. default_st_rep_get s loc = default_st_rep_get t loc"
  shows "eq_default_st_rep s t"
  unfolding eq_default_st_rep_def fun_eq_iff using assms by blast

lemma eq_default_st_repD:
  assumes "eq_default_st_rep s t"
  shows "default_st_rep_get s loc = default_st_rep_get t loc"
  using assms unfolding eq_default_st_rep_def fun_eq_iff by blast

subsection ‹Executable pointwise order›

text ‹
  ‹le_default_st_rep_code› compares both dictionaries with
  ‹le_default_dict› and is shown equal to the pointwise order on lookups.
›

fun le_default_st_rep_code ::
  "('a::order_bot) default_st_rep => 'a default_st_rep => bool"
where
  "le_default_st_rep_code (l1, g1) (l2, g2) ⟷
     le_default_dict l1 l2 ∧ le_default_dict g1 g2"

text ‹
  The characterization avoids the pair pattern, so that quotient-level
  statements can be discharged by ‹transfer› alone instead of re-opening both
  representatives.
›

lemma le_default_st_rep_code_iff:
  "le_default_st_rep_code s t ⟷
    (∀loc. default_st_rep_get s loc ≤ default_st_rep_get t loc)"
  by (cases s; cases t) (simp add: all_location_iff le_default_dict_iff)


subsection ‹The extensional quotient, lookup and point update›

text ‹
  ‹default_st› is the quotient of raw states by extensional equality.
  Lookup and point update lift to it because both respect the equivalence.
›

quotient_type 'a default_st =
  "('a::bot) default_st_rep" / "eq_default_st_rep"
  morphisms rep_default_st Abs_default_st
  by (rule equivp_eq_default_st_rep)

lift_definition default_st_get ::
  "('a::bot) default_st => location => 'a"
  is default_st_rep_get
  by (simp add: eq_default_st_rep_def)

fun default_st_rep_set ::
  "('a::bot) default_st_rep => location => 'a => 'a default_st_rep" where
  "default_st_rep_set (l, g) (Local_Location x) a = (default_dict_set l x a, g)"
| "default_st_rep_set (l, g) (Global_Location x) a = (l, default_dict_set g x a)"

lemma default_st_rep_get_set [simp]:
  "default_st_rep_get (default_st_rep_set s loc a) loc' =
     (if loc = loc' then a else default_st_rep_get s loc')"
  by (cases s; cases loc; cases loc') simp_all

lemma eq_default_st_rep_set:
  assumes "eq_default_st_rep s t"
  shows "eq_default_st_rep (default_st_rep_set s loc a)
      (default_st_rep_set t loc a)"
  by (rule eq_default_st_repI) (simp add: eq_default_st_repD[OF assms])

lift_definition default_st_set ::
  "('a::bot) default_st => location => 'a => 'a default_st"
  is default_st_rep_set
  by (rule eq_default_st_rep_set)

text ‹
  Lookup is written ‹s⟨l⟩› and point update ‹s⟨l := a⟩›. The notation is a
  bundle: every theory that uses it opens it after ‹begin› and closes it with
  ‹unbundle no› before ‹end›, so it never reaches an importing theory and
  never changes a term.
  Both forms bind tighter than application, so ‹f s⟨l⟩› reads
  ‹f (s⟨l⟩)› and updates chain as ‹s⟨l := a⟩⟨l'⟩›.
  The state with local dictionary ‹(dl, ls)› and global dictionary
  ‹(dg, gs)› is written ‹⟪(dl, ls), (dg, gs)⟫›.
  Theories past ‹default_st_to_fun› open ‹default_st_syntax›,
  which adds the notation for the function a state represents to this bundle.
›

abbreviation default_st_mk ::
  "('a::bot) default_dict => 'a default_dict => 'a default_st" where
  "default_st_mk l g ≡ Abs_default_st (l, g)"

bundle default_st_carrier_syntax
begin
notation default_st_get ("_⟨_⟩" [1000, 0] 1000)
notation default_st_set ("_⟨_ :=/ _⟩" [1000, 0, 0] 1000)
notation default_st_mk ("⟪_,/ _⟫")
end

unbundle default_st_carrier_syntax

lemma default_st_get_Abs [simp]:
  "(Abs_default_st s)⟨loc⟩ = default_st_rep_get s loc"
  by transfer simp

lemma Abs_default_st_rep_default_st [simp]:
  "Abs_default_st (rep_default_st s) = s"
  by (fact Lifting.Quotient_abs_rep [OF Quotient_default_st])

lemma default_st_get_rep:
  "s⟨loc⟩ = default_st_rep_get (rep_default_st s) loc"
  by (simp add: default_st_get.rep_eq)

text ‹
  One lookup equation for the update, rather than a same/different pair: the
  conditional is what a caller has to reason about anyway, and the two special
  cases fall out of it by \<^term>‹simp›.
›

lemma default_st_get_set [simp]:
  "s⟨loc := a⟩⟨loc'⟩ = (if loc = loc' then a else s⟨loc'⟩)"
  by transfer simp

lemma default_st_eq_iff:
  "s = t ⟷
     default_st_get s = default_st_get t"
  by transfer (simp add: eq_default_st_rep_def)

text ‹
  The quotient-level counterpart of @{thm [source] eq_default_st_repI}: two
  quotient states are equal as soon as they look the same everywhere.  Left
  untagged -- as an ‹[intro]› rule it would attack every equation at this type
  by extensionality, which is rarely what a goal about a concrete state wants.
›

lemma default_st_eqI:
  assumes "⋀loc. s⟨loc⟩ = t⟨loc⟩"
  shows "s = t"
  using assms by (simp add: default_st_eq_iff fun_eq_iff)


subsection ‹Order, bottom and executable equality›

text ‹
  Bottom is the pair of empty dictionaries with bottom defaults; the order lifts
  ‹le_default_st_rep_code›, which also yields an executable equality.
›

instantiation default_st :: (bot) bot
begin
definition bot_default_st ::
  "('a::bot) default_st"
where
  "bot_default_st = ⟪(bot, []), (bot, [])⟫"
instance ..
end

instantiation default_st :: (order_bot) ord
begin
lift_definition less_eq_default_st ::
  "('a::order_bot) default_st =>
   'a default_st => bool"
  is le_default_st_rep_code
  by (auto simp: le_default_st_rep_code_iff eq_default_st_rep_def)

definition less_default_st ::
  "('a::order_bot) default_st =>
   'a default_st => bool"
where
  "less_default_st s t ⟷
     s ≤ t ∧ ¬ t ≤ s"

instance ..
end


lemma le_default_st_iff:
  fixes s t :: "('a::order_bot) default_st"
  shows "s ≤ t ⟷ (∀loc. s⟨loc⟩ ≤ t⟨loc⟩)"
  by transfer (rule le_default_st_rep_code_iff)


instance default_st :: (order_bot) order
proof intro_classes
  fix s t u :: "('a::order_bot) default_st"
  show "(s < t) ⟷ (s ≤ t ∧ ¬ t ≤ s)"
    by (simp add: less_default_st_def)

  show "s ≤ s"
    by (simp add: le_default_st_iff)
  show "s ≤ t ⟹ t ≤ u ⟹ s ≤ u"
    by (auto simp: le_default_st_iff intro: order_trans)
  show "s ≤ t ⟹ t ≤ s ⟹ s = t"
    by (auto simp: le_default_st_iff
      default_st_eq_iff fun_eq_iff intro: order_antisym)
qed

context
  includes lattice_syntax
begin

lemma default_st_get_bot [simp]:
  "(⊥ :: ('a::bot) default_st)⟨loc⟩ = ⊥"
  unfolding bot_default_st_def by (cases loc) simp_all

end


lemma bot_le_default_st:
  "(bot :: ('a::order_bot) default_st) ≤ s"
  by (simp add: le_default_st_iff)

instance default_st :: (order_bot) order_bot
  by standard (rule bot_le_default_st)
instantiation default_st :: ("{order_bot,equal}") equal
begin
definition equal_default_st ::
  "('a::{order_bot,equal}) default_st =>
   'a default_st => bool"
where
  "equal_default_st s t = (s ≤ t ∧ t ≤ s)"
instance
  by standard (auto simp: equal_default_st_def intro: order_antisym)
end

unbundle no default_st_carrier_syntax

end