Theory Default_St_Reachability

theory Default_St_Reachability
  imports Default_St_Transfer "Voblint_Domain.Nonrelational_Reachability"
begin

unbundle default_st_syntax

text ‹
  A lifted state reads back pointwise under the lift: \<^const>‹Bot› stays
  \<^const>‹Bot›, and a \<^const>‹Lifted› state becomes \<^const>‹Lifted› of the
  function it represents. This is how a solved local unknown, stored as an
  \<^typ>‹'a default_st lifted›, enters the result boundary. The readback
  performs no bottom test. \<^const>‹canonicalize_lift› collapses a
  witness-bottom payload to \<^const>‹Bot› before it, and coverage stays a
  property of the solve: a covered key whose value is \<^const>‹Bot› remains a
  key.
›

adhoc_overloading readback == "λ𝒢. map_lift (default_st_to_fun 𝒢)"

section ‹Executable dead-code detection›

text ‹
  A nonrelational state denotes the product of its variables' value sets, so a
  single bottom component makes the whole state denote nothing. Deciding that
  by inspecting every variable is not executable -- there are infinitely many
  names -- so this theory builds a finite test and proves it says exactly what
  the infinite one does.

  The finite test has three witness sources: the local default, which covers
  every name no entry mentions; an explicitly stored entry that is bottom in
  the dictionary the classifier selects for its name; and a scan of the
  program's declared globals, which covers the side where no fresh-name
  argument is available. The middle one needs the classifier, since an entry
  stored in the other dictionary says nothing about the function the state
  represents. Above that sits the lifted view, where a whole unreachable state
  collapses to \<^const>‹Bot› and an update that writes a bottom value collapses
  to it incrementally, without re-testing the rest of the state.
›

subsection ‹Raw witness test›

text ‹
  Bottom detection is the one carrier operation that consults ‹𝒢›, and the
  reason is the mismatch between two readings of the same state. The quotient
  \<^typ>‹'a default_st› identifies two states exactly when their lookups agree
  at ∗‹every› location, whereas \<^const>‹default_st_rep_to_fun› reads each
  name in the one dictionary ‹𝒢› selects for it. An entry for a name in the
  other dictionary is therefore visible to equality and invisible to the
  concretization, and a test that must agree with \<^const>‹is_empty_state› on the
  represented function has to skip it. Every other operation on the carrier --
  lookup, update, order, join, widening, narrowing -- treats all locations
  alike and needs no classifier.

  The test below is sufficient but not yet exact, and takes three disjuncts:
  the local default already bottom, which covers every name no entry mentions;
  or a local entry, for a name ‹𝒢› leaves local, that is bottom; or a global
  entry, for a name ‹𝒢› calls global, that is bottom. The global default is
  deliberately not checked. A real program's classifier calls only finitely
  many names global, so no argument independent of the entry list can produce a
  fresh global escaping it, the way a fresh local always exists. Only the entry
  branch can safely observe a global; the exact test in the next subsection
  closes that gap by enumerating the declared globals outright.
›

fun default_st_rep_is_bot ::
  "(vname => bool) => ('a::executable_domain) default_st_rep => bool" where
  "default_st_rep_is_bot 𝒢 ((dl, ls), (dg, gs)) ⟷
     is_empty dl ∨
     (∃x ∈ set (map fst ls). ¬ 𝒢 x ∧ is_empty (default_dict_get (dl, ls) x)) ∨
     (∃x ∈ set (map fst gs). 𝒢 x ∧ is_empty (default_dict_get (dg, gs) x))"

text ‹
  Soundness needs ‹𝒢› to leave infinitely many vnames local, so that some local
  witness always escapes any given (finite) entry list -- true for any
  @{term declared_global} of a real program, which only ever declares finitely
  many globals while @{typ vname} is infinite.
›
lemma default_st_rep_is_bot_sound:
  assumes bot: "default_st_rep_is_bot 𝒢 s"
    and infinite_local: "infinite {x. ¬ 𝒢 x}"
  shows "is_empty_state (default_st_rep_to_fun 𝒢 s)"
proof -
  obtain l g where s_eq: "s = (l, g)" by (cases s)
  obtain dl ls where l_eq: "l = (dl, ls)" by (cases l)
  obtain dg gs where g_eq: "g = (dg, gs)" by (cases g)
  have local_lookup: "default_st_rep_to_fun 𝒢 s x = default_dict_get l x"
    if "¬ 𝒢 x" for x
    using that unfolding default_st_rep_to_fun_def location_of_def s_eq by simp
  have global_lookup: "default_st_rep_to_fun 𝒢 s x = default_dict_get g x"
    if "𝒢 x" for x
    using that unfolding default_st_rep_to_fun_def location_of_def s_eq by simp
  from bot consider
      (local_default) "is_empty dl"
    | (local_entry) x where "¬ 𝒢 x" "is_empty (default_dict_get l x)"
    | (global_entry) x where "𝒢 x" "is_empty (default_dict_get g x)"
    unfolding s_eq l_eq g_eq by auto
  then show ?thesis
  proof cases
    case local_default
    from infinite_local obtain x :: vname
      where x_local: "x ∈ {x. ¬ 𝒢 x}"
        and fresh: "x ∉ set (map fst ls)"
      by (rule obtain_fresh_vname)
    from fresh have "map_of ls x = None"
      by (simp add: map_of_resolved_none_iff)
    then have "default_dict_get l x = dl"
      unfolding l_eq by simp
    with local_default x_local have "is_empty (default_st_rep_to_fun 𝒢 s x)"
      by (simp add: local_lookup)
    then show ?thesis by (rule is_empty_stateI)
  next
    case (local_entry x)
    then have "is_empty (default_st_rep_to_fun 𝒢 s x)"
      by (simp add: local_lookup)
    then show ?thesis by (rule is_empty_stateI)
  next
    case (global_entry x)
    then have "is_empty (default_st_rep_to_fun 𝒢 s x)"
      by (simp add: global_lookup)
    then show ?thesis by (rule is_empty_stateI)
  qed
qed

text ‹
  \<^const>‹default_st_rep_is_bot› deliberately leaves the global default unchecked
  because an opaque classifier gives no way to enumerate the (finite) globally
  classified vnames. A concrete program's classifier is always backed by an
  explicit finite list (@{term declared_global_vars}), and enumerating exactly
  that list closes the gap: every globally classified vname is checked
  directly, so the global branch needs no entry witness. This makes the
  combined check an exact (not merely sound) characterization of
  @{const is_empty_state}, with no side condition on ‹𝒢› beyond ‹globals›
  actually listing its true set -- unlike @{thm default_st_rep_is_bot_sound},
  which still needs infinitely many locals to exist.
›

subsection ‹Exact test for the declared globals›

text ‹
  In these names ‹rep› marks a test on representations and ‹for› a test exact for an
  explicit list of declared globals. The classifier-only test
  \<^const>‹default_st_rep_is_bot› has no quotient counterpart: it ignores the global
  default, so extensionally equal representatives can disagree on it.
›

definition default_st_rep_is_bot_for ::
  "vname list => (vname => bool) => ('a::executable_domain) default_st_rep => bool" where
  "default_st_rep_is_bot_for globals 𝒢 s =
     ((∃x ∈ set globals. is_empty (default_st_rep_get s (location_of 𝒢 x))) ∨
      default_st_rep_is_bot 𝒢 s)"

lemma default_st_rep_is_bot_for_iff:
  fixes s :: "'a::executable_domain default_st_rep"
  assumes globals: "⋀x. 𝒢 x = (x ∈ set globals)"
  shows "default_st_rep_is_bot_for globals 𝒢 s ⟷ is_empty_state (default_st_rep_to_fun 𝒢 s)"
proof -
  have infinite_local: "infinite {x::vname. ¬ 𝒢 x}"
  proof
    assume fin: "finite {x::vname. ¬ 𝒢 x}"
    have "finite (UNIV :: vname set)"
    proof -
      have univ: "(UNIV :: vname set) = {x. ¬ 𝒢 x} ∪ set globals"
        using globals by auto
      have "finite ({x. ¬ 𝒢 x} ∪ set globals)" using fin by simp
      then show ?thesis unfolding univ .
    qed
    then show False using infinite_literal by simp
  qed
  show ?thesis
  proof
    assume "default_st_rep_is_bot_for globals 𝒢 s"
    then show "is_empty_state (default_st_rep_to_fun 𝒢 s)"
      unfolding default_st_rep_is_bot_for_def
    proof (elim disjE)
      assume "∃x ∈ set globals. is_empty (default_st_rep_get s (location_of 𝒢 x))"
      then obtain x where "is_empty (default_st_rep_get s (location_of 𝒢 x))" by blast
      then have "is_empty (default_st_rep_to_fun 𝒢 s x)"
        unfolding default_st_rep_to_fun_def by simp
      then show ?thesis by (rule is_empty_stateI)
    next
      assume bot: "default_st_rep_is_bot 𝒢 s"
      show ?thesis by (rule default_st_rep_is_bot_sound[OF bot infinite_local])
    qed
  next
    assume "is_empty_state (default_st_rep_to_fun 𝒢 s)"
    then obtain x where x: "is_empty (default_st_rep_to_fun 𝒢 s x)" by (rule is_empty_stateE)
    show "default_st_rep_is_bot_for globals 𝒢 s"
    proof (cases "𝒢 x")
      case True
      then have "x ∈ set globals" using globals by simp
      moreover have "default_st_rep_to_fun 𝒢 s x = default_st_rep_get s (location_of 𝒢 x)"
        unfolding default_st_rep_to_fun_def by (rule refl)
      ultimately have "∃y ∈ set globals. is_empty (default_st_rep_get s (location_of 𝒢 y))"
        using x by auto
      then show ?thesis unfolding default_st_rep_is_bot_for_def by (rule disjI1)
    next
      case False
      note local_x = False
      obtain l g where s_eq: "s = (l, g)" by (cases s)
      obtain dl ls where l_eq: "l = (dl, ls)" by (cases l)
      obtain dg gs where g_eq: "g = (dg, gs)" by (cases g)
      have empty: "is_empty (default_dict_get l x)"
        using x local_x unfolding default_st_rep_to_fun_def location_of_def s_eq by simp
      have "default_st_rep_is_bot 𝒢 s"
      proof (cases "x ∈ set (map fst ls)")
        case True
        with empty local_x
        have "∃y ∈ set (map fst ls). ¬ 𝒢 y ∧ is_empty (default_dict_get (dl, ls) y)"
          unfolding l_eq by blast
        then show ?thesis unfolding s_eq l_eq g_eq by simp
      next
        case False
        then have "map_of ls x = None"
          by (simp add: map_of_resolved_none_iff)
        with empty have "is_empty dl" unfolding l_eq by simp
        then show ?thesis unfolding s_eq l_eq g_eq by simp
      qed
      then show ?thesis unfolding default_st_rep_is_bot_for_def by (rule disjI2)
    qed
  qed
qed


subsection ‹Lifting the exact test to the quotient›

text ‹
  \<^const>‹default_st_rep_is_bot_for› takes ‹𝒢› as a free parameter, which makes it
  \<^const>‹eq_default_st_rep›-respectful only when ‹𝒢› agrees with ‹globals›: a
  mismatched pair can pick out a witness through one representative's
  dictionary entries that another, extensionally equal, representative encodes
  via its defaults instead. Every real caller supplies the matching pair, so fixing
  ‹𝒢› to ‹λx. x ∈ set globals› internally loses nothing and restores
  unconditional respectfulness -- which is what makes
  ‹default_st_is_bot_for› below liftable to the quotient at all.

  With that pair fixed, respectfulness is a corollary of exactness rather than
  a separate argument: extensionally equal representatives project to the same
  state, and @{thm [source] default_st_rep_is_bot_for_iff} says the test is
  exactly \<^const>‹is_empty_state› of that projection.
›

lemma eq_default_st_rep_is_bot_for:
  assumes eq: "eq_default_st_rep s t"
  shows "default_st_rep_is_bot_for globals (λx. x ∈ set globals) s
       = default_st_rep_is_bot_for globals (λx. x ∈ set globals) t"
proof -
  have iff: "default_st_rep_is_bot_for globals (λx. x ∈ set globals) u
      = is_empty_state (default_st_rep_to_fun (λx. x ∈ set globals) u)"
    for u :: "'a default_st_rep"
    by (rule default_st_rep_is_bot_for_iff) simp
  have "default_st_rep_to_fun (λx. x ∈ set globals) s
          = default_st_rep_to_fun (λx. x ∈ set globals) t"
    unfolding default_st_rep_to_fun_def
    by (rule ext) (rule eq_default_st_repD[OF eq])
  then show ?thesis unfolding iff by simp
qed

text ‹
  The exact check transported to the quotient through \<^const>‹rep_default_st›.
  This is the predicate the executable side trees are built against: unlike
  \<^const>‹is_empty_state› composed with \<^const>‹default_st_to_fun›, it has
  a genuine ‹[code]› equation, because it never quantifies over all of
  \<^typ>‹vname›.

  It takes ‹globals› alone and rebuilds ‹𝒢› from it internally, rather than
  accepting a caller-supplied classifier. That is what makes
  @{thm [source] eq_default_st_rep_is_bot_for} apply unconditionally, and so what
  makes the definition liftable at all. Nothing is lost: every real caller
  already recomputes the same ‹𝒢› from the same list at the call site.
›

lift_definition default_st_is_bot_for ::
  "vname list => ('a::executable_domain) default_st => bool"
  is "λglobals s. default_st_rep_is_bot_for globals (λx. x ∈ set globals) s"
  by (rule eq_default_st_rep_is_bot_for)

lemma default_st_is_bot_for_iff:
  fixes s :: "'a::executable_domain default_st"
  assumes globals: "⋀x. 𝒢 x = (x ∈ set globals)"
  shows "default_st_is_bot_for globals s ⟷ is_empty_state (ρ⇘𝒢⇙ s)"
proof -
  have gs_eq: "(λx. x ∈ set globals) = 𝒢"
    using globals by (simp add: fun_eq_iff)
  show ?thesis
    unfolding default_st_is_bot_for.rep_eq gs_eq
    by (simp add: default_st_rep_is_bot_for_iff[OF globals]
      default_st_to_fun_rep)
qed

text ‹
  The same test read through the carrier's concretization: a state passes it
  exactly when it describes no store.
›

lemma default_st_is_bot_for_gamma_iff:
  fixes s :: "'a::numeric_domain default_st"
  assumes globals: "⋀x. 𝒢 x = (x ∈ set globals)"
  shows "default_st_is_bot_for globals s ⟷ default_st_gamma 𝒢 s = {}"
  by (simp add: default_st_is_bot_for_iff[OF globals] default_st_gamma_def
      is_empty_state_iff_gamma_state_empty)

lemma exact_emptiness_default_st_is_bot_for:
  assumes globals: "⋀x. 𝒢 x = (x ∈ set globals)"
  shows "exact_emptiness (default_st_is_bot_for globals)
           (default_st_gamma 𝒢 :: 'a::numeric_domain default_st ⇒ store set)"
  by (rule exact_emptinessI) (rule default_st_is_bot_for_gamma_iff[OF globals])

subsection ‹The stores a lifted carrier state describes›

text ‹
  Reachability adds no new concretization: a lifted carrier state is read
  through \<^const>‹gamma_lift› over \<^const>‹default_st_gamma›, as a lifted
  pointwise state is read through \<^const>‹gamma_lift› over
  \<^const>‹gamma_state›. The lemma below relates the two through the
  represented function.
›

lemma gamma_lift_default_st_gamma_to_fun:
  "gamma_lift (default_st_gamma 𝒢) = (λd. γ⇩⊥ (map_lift ρ⇘𝒢⇙ d))"
  by (rule ext) (simp add: gamma_lift_def default_st_gamma_def split: lifted.split)


subsection ‹Incremental dead-code tracking›

text ‹
  ‹live_default_st› states that no location of the readback is empty, the
  condition under which a transfer result counts as reachable.
›


definition live_default_st ::
  "(vname => bool) => ('a::executable_domain) default_st => bool"
where
  "live_default_st 𝒢 s = (~ is_empty_state (ρ⇘𝒢⇙ s))"

text ‹
  ‹is_empty_state› on ‹ρ⇘𝒢⇙ s› is an infinite existential over
  ‹vname›, not executable on a quotient value.  ‹default_st_set_lift› tracks it
  incrementally instead: given a @{const live_default_st} input and the single
  freshly computed element, the result is witness-bottom iff that element is
  ‹is_empty› -- every other location is provably unchanged
  (@{thm default_st_to_fun_set}), so it cannot newly become bottom.  This
  mirrors Goblint's per-analysis ‹Deadcode› raise while staying generic: it lives at
  the shared update primitive, not in each domain's own transfer code.
›

definition default_st_set_lift ::
  "('a::executable_domain) default_st lifted => location => 'a => 'a default_st lifted"
where
  "default_st_set_lift x loc a = do {
     s <- x;
     if is_empty a then Bot else Lifted s⟨loc := a⟩
   }"

lemma default_st_set_lift_Bot [simp]:
  "default_st_set_lift Bot loc a = Bot"
  unfolding default_st_set_lift_def by simp

lemma default_st_set_lift_Lifted:
  "default_st_set_lift (Lifted s) loc a =
     (if is_empty a then Bot else Lifted s⟨loc := a⟩)"
  unfolding default_st_set_lift_def by simp

text ‹
  The completeness theorem the location-scoped check relies on: from a live input,
  the lifted update exactly tracks the spec-level normalized result.  Only the
  freshly written variable's element needs checking -- every other variable's
  ‹abs_state› component provably survives unchanged
  (@{thm default_st_to_fun_set}), so it cannot be the source of a new
  witness-bottom.
›
lemma default_st_set_lift_correct:
  fixes s :: "'a::executable_domain default_st"
  assumes live: "live_default_st 𝒢 s"
  shows "map_lift ρ⇘𝒢⇙
           (default_st_set_lift (Lifted s) (location_of 𝒢 x) a) =
         normalize_lift is_empty_state ((ρ⇘𝒢⇙ s)(x := a))"
proof -
  from live have live': "¬ is_empty_state (ρ⇘𝒢⇙ s)"
    unfolding live_default_st_def by simp
  have upd: "is_empty_state ((ρ⇘𝒢⇙ s)(x := a)) = is_empty a"
    by (rule is_empty_state_fun_upd_iff[OF live'])
  show ?thesis
    by (cases "is_empty a")
      (simp_all add: default_st_set_lift_Lifted upd)
qed

unbundle no default_st_syntax

end