Theory Nonrelational_State

theory Nonrelational_State
  imports State_Concretization
begin

section ‹What a store of one abstract value per variable denotes, and when it denotes nothing›

text ‹
  A non-relational abstract state, ‹'a abs_state›, pairs every program
  variable with one abstract value, independently of every other variable
  -- the "non-relational" in the name. ‹gamma_state› says what that
  pairing denotes: exactly the concrete stores where each variable's value
  lies in its own component's concretization, i.e. the product of the
  per-component concretizations. Because that product is a conjunction over
  every variable, one witness-bottom component -- one variable whose
  abstract value denotes no concrete value at all -- already makes the
  whole state denote nothing, regardless of what every other component
  holds. ‹is_empty_state› names that witness-bottom condition directly,
  so a generic transfer dispatcher can detect and canonicalize it without
  testing ‹gamma_state› against the empty set at run time.
›

type_synonym 'a abs_state = "vname => 'a"

(* HOL ships fun :: (type, bounded_lattice) bounded_lattice but not this
   weaker pointwise instance; abs_state needs it for TD_side part_post_solution. *)
instance "fun" :: (type, bounded_semilattice_sup_bot) bounded_semilattice_sup_bot ..

text ‹Pointwise join on abstract states is idempotent because the value-domain
  semilattice structure lifts pointwise.  Finite folds can therefore use the
  standard idempotent-join laws without a separate state-level assumption.›
subsection ‹State concretization›

definition gamma_state :: "('a::numeric_domain) abs_state ⇒ store set" where
  "gamma_state d = {s. ∀x. s x ∈ γ (d x)}"

adhoc_overloading gamma_S == gamma_state

lemma gamma_stateI [intro]:
  "(⋀x. s x ∈ γ (d x)) ⟹ s ∈ γ d"
  unfolding gamma_state_def by simp

(* Note: pointwise bot / sup on 'a abs_state come from HOL's
   fun :: bot and fun :: sup instances; no extra definitions needed. *)

subsection ‹State concretization laws›

text ‹Every value-level concretization law, lifted to states.  All of them fall out
  pointwise, which is exactly what makes a nonrelational state cheap: order, bottom and join
  are read one variable at a time, and no law here needs a relation between variables.›
lemma gamma_state_mono:
  "sigma1 ≤ sigma2 ⟹ γ sigma1 ⊆ γ sigma2"
  for sigma1 sigma2 :: "'a::numeric_domain abs_state"
  unfolding gamma_state_def le_fun_def
  using gamma_mono by blast

lemma gamma_state_bot [simp]:
  "γ (bot :: 'a::numeric_domain abs_state) = {}"
  unfolding gamma_state_def bot_fun_def using gamma_bot by auto

lemma gamma_state_sup_ub1 [intro]:
  "γ sigma1 ⊆ γ (sigma1 ⊔ sigma2)"
  for sigma1 sigma2 :: "'a::numeric_domain abs_state"
  unfolding gamma_state_def sup_fun_def
  using gamma_sup_ub1 by blast

lemma gamma_state_sup_ub2 [intro]:
  "γ sigma2 ⊆ γ (sigma1 ⊔ sigma2)"
  for sigma1 sigma2 :: "'a::numeric_domain abs_state"
  unfolding gamma_state_def sup_fun_def
  using gamma_sup_ub2 by blast

text ‹
  Membership counterparts of ‹gamma_state_sup_ub1›/‹gamma_state_sup_ub2›,
  for citing at a witness ‹s› directly (‹using subsetD[OF gamma_state_sup_ub1 h]›
  otherwise repeats the same ‹subsetD› wrapper at every call site).
  ‹[intro]›: their conclusion has the distinctive
  ‹s ∈ γ (sigma1 ⊔ sigma2)› shape a join-injection goal actually has, and a
  witness already in one side's concretization is exactly the natural way to
  discharge it.
›

lemma gamma_state_supI1 [intro]:
  "s ∈ γ sigma1 ⟹ s ∈ γ (sigma1 ⊔ sigma2)"
  for sigma1 sigma2 :: "'a::numeric_domain abs_state"
  using gamma_state_sup_ub1 by blast

lemma gamma_state_supI2 [intro]:
  "s ∈ γ sigma2 ⟹ s ∈ γ (sigma1 ⊔ sigma2)"
  for sigma1 sigma2 :: "'a::numeric_domain abs_state"
  using gamma_state_sup_ub2 by blast

text ‹
  Left bare rather than ‹[dest]›: ‹x› is unconstrained by the premise, so a
  global destruction rule here would let ‹auto› pick a schematic variable
  unrelated to the goal at hand (as with the ‹Voblint_Solver› session's
  ‹env_indep_depsD›). Cite it explicitly with the variable the goal needs.
›
lemma gamma_stateD:
  "s ∈ γ d ⟹ s x ∈ γ (d x)"
  for d :: "'a::numeric_domain abs_state"
  unfolding gamma_state_def by simp

subsection ‹Witness-bottom abstract states›

text ‹
  Witness-bottom is not "the state has exactly one empty component": any
  number of a state's components can independently denote the empty set of
  concrete integers at once, and ‹is_empty_state› does not distinguish those
  cases from each other or count them. It only asks whether at least one
  witness exists (‹∃x. is_empty (d x)›), because one witness already
  suffices -- ‹gamma_state›'s product structure means a single empty
  component collapses the whole state's concretization to the empty set of
  stores, so a second, third, or every remaining empty component would only
  reconfirm what the first already decided.

  ‹is_empty_state› is a logical characterization of that condition, not an
  executable test: ‹'a abs_state› is a raw function ‹vname ⇒ 'a›, and
  \<^typ>‹vname› is infinite, so ‹∃x. is_empty (d x)› has no code equation --
  there is no finite witness search for code generation to compile. The
  finite executable bottom test a real dispatcher runs is ‹default_st_is_bot_for›,
  defined downstream in the ‹Voblint_Exec› session, which scans only the
  state's finitely many stored locations and is proved to agree with
  ‹is_empty_state› on every such state.
›

definition is_empty_state :: "('a::executable_domain) abs_state ⇒ bool" where
  "is_empty_state d = (∃x. is_empty (d x))"

lemma is_empty_stateI [intro]:
  "is_empty (d x) ⟹ is_empty_state d"
  unfolding is_empty_state_def by (rule exI)

lemma is_empty_stateE [elim]:
  assumes "is_empty_state d"
  obtains x where "is_empty (d x)"
  using assms unfolding is_empty_state_def by blast

text ‹
  Overwriting one variable of a state that is not already empty can only make
  it empty through the written element.  This is what lets an incremental
  emptiness check inspect the freshly computed element alone instead of
  searching the infinite variable space again.
›

lemma is_empty_state_fun_upd_iff:
  assumes "¬ is_empty_state d"
  shows "is_empty_state (d(x := a)) ⟷ is_empty a"
proof
  assume "is_empty_state (d(x := a))"
  then obtain y where "is_empty ((d(x := a)) y)"
    by (rule is_empty_stateE)
  with assms show "is_empty a"
    by (cases "y = x") auto
next
  assume "is_empty a"
  then have "is_empty ((d(x := a)) x)" by simp
  then show "is_empty_state (d(x := a))"
    by (rule is_empty_stateI)
qed

lemma is_empty_state_gamma_state_empty:
  assumes "is_empty_state d"
  shows "γ d = {}"
proof -
  obtain x where "is_empty (d x)" using assms by (rule is_empty_stateE)
  then show ?thesis
    using gamma_stateD[of _ d x] unfolding is_empty_correct by fastforce
qed

lemma gamma_state_empty_is_empty_state:
  assumes "γ d = {}"
  shows "is_empty_state d"
proof (rule ccontr)
  assume "¬ is_empty_state d"
  then have nonempty: "⋀x. ∃v. v ∈ γ (d x)"
    unfolding is_empty_state_def using is_empty_correct by blast
  define s where "s = (λx. SOME v. v ∈ γ (d x))"
  have s_prop: "s x ∈ γ (d x)" for x
    unfolding s_def using nonempty[of x] by (rule someI_ex)
  then have "s ∈ γ d"
    unfolding gamma_state_def by simp
  with assms show False by simp
qed

lemma is_empty_state_iff_gamma_state_empty:
  "is_empty_state d ⟷ γ d = {}"
  using is_empty_state_gamma_state_empty gamma_state_empty_is_empty_state by blast

lemma exact_emptiness_is_empty_state:
  "exact_emptiness is_empty_state (gamma_state :: 'a::numeric_domain abs_state ⇒ store set)"
  by (rule exact_emptinessI) (rule is_empty_state_iff_gamma_state_empty)

lemma is_empty_state_bot [simp]:
  "is_empty_state (bot :: 'a::numeric_domain abs_state)"
  unfolding is_empty_state_def bot_fun_def
  using is_empty_correct gamma_bot by blast

lemma is_empty_state_antimono:
  "d1 ≤ d2 ⟹ is_empty_state d2 ⟹ is_empty_state d1"
  for d1 d2 :: "'a::numeric_domain abs_state"
  unfolding is_empty_state_def le_fun_def using is_empty_antimono by blast

end