Theory Nonrelational_Reachability

theory Nonrelational_Reachability
  imports Nonrelational_State Reachability_Lift
begin

section ‹Reachability for pointwise abstract stores›

text ‹
  Pointwise stores and structural reachability are independent domain
  constructions. This theory composes them: unreachable points denote no
  concrete store, and reachable payloads use \<^const>‹gamma_state›.
  The logical witness-empty predicate agrees with that composed
  concretization; a concrete executable state representation supplies a
  finite implementation of it (‹default_st_is_bot_for›, downstream in the
  ‹Voblint_Exec› session), since ‹is_empty_state_lift› below inherits
  \<^const>‹is_empty_state›'s non-executable quantifier over \<^typ>‹vname› on its
  ‹Lifted› case.
›

subsection ‹Composed concretization›

text ‹A lifted pointwise state is one more kind of state, so ‹γ d› covers it too.
  ‹γ⇩⊥ _› stays as input syntax that fixes the lifted type where nothing else does.›

abbreviation (input) gamma_state_lift ::
  "'a::numeric_domain abs_state lifted ⇒ store set" ("γ⇩⊥") where
  "gamma_state_lift ≡ gamma_lift gamma_state"

adhoc_overloading gamma_S == "gamma_lift gamma_state"

fun is_empty_state_lift ::
  "'a::executable_domain abs_state lifted ⇒ bool" where
  "is_empty_state_lift Bot = True"
| "is_empty_state_lift (Lifted d) = is_empty_state d"

lemma is_empty_state_lift_iff:
  "is_empty_state_lift s ⟷ γ⇩⊥ s = {}"
  by (cases s) (simp_all add: is_empty_state_iff_gamma_state_empty)

lemma exact_emptiness_is_empty_state_lift:
  "exact_emptiness is_empty_state_lift
     (gamma_lift gamma_state :: 'a::numeric_domain abs_state lifted ⇒ store set)"
  by (rule exact_emptinessI) (rule is_empty_state_lift_iff)

text ‹
  ‹Reachability_Lift›'s generic ‹gamma_normalize_lift›/‹normalize_lift_mono›/
  ‹normalized_lift_sup› specialized to ‹is_empty_state›: each generic side
  condition (concretization agreement, downward closure) is discharged by
  ‹is_empty_state_iff_gamma_state_empty›/‹is_empty_state_antimono›. The first
  is tagged ‹[simp]›, unlike the generic version, because its side condition
  is now a closed fact rather than a further proof obligation.
›

lemma gamma_state_normalize_lift [simp]:
  "γ⇩⊥ (normalize_lift is_empty_state d) = γ d"
  by (rule gamma_normalize_lift) (rule is_empty_state_iff_gamma_state_empty)

text ‹Collapsing a witness-bottom payload changes what a value says about
  itself, never what it represents. Every public result adapter routes its
  solved values through \<^const>‹canonicalize_lift› before publishing them, so
  this is what lets such an adapter's soundness argument ignore the collapse
  entirely.›

lemma gamma_state_canonicalize_lift [simp]:
  "γ⇩⊥ (canonicalize_lift is_empty_state d) = γ⇩⊥ d"
  by (cases d) simp_all

lemma normalize_state_lift_mono [intro]:
  fixes d1 d2 :: "'a::numeric_domain abs_state"
  assumes le: "d1 ≤ d2"
  shows "normalize_lift is_empty_state d1 ≤ normalize_lift is_empty_state d2"
  by (rule normalize_lift_mono[OF le]) (rule is_empty_state_antimono[OF le])

lemma normalized_state_lift_sup [intro]:
  fixes s1 s2 :: "'a::numeric_domain abs_state lifted"
  assumes n1: "normalized_lift is_empty_state s1" and n2: "normalized_lift is_empty_state s2"
  shows "normalized_lift is_empty_state (s1 ⊔ s2)"
  by (rule normalized_lift_sup[OF is_empty_state_antimono n1 n2])

subsection ‹The normalization invariant›

text ‹
  After normalization, structural and semantic deadness coincide: a
  ‹normalized_lift›-disciplined value can no longer disagree with its own
  ‹is_empty_state_lift› reading, because normalization is exactly what rules
  out a live-looking ‹Lifted› payload that is secretly witness-bottom.
›

lemma normalized_state_lift_bot_iff [simp]:
  "normalized_lift is_empty_state s ⟹ is_empty_state_lift s ⟷ s = Bot"
  by (cases s) simp_all

subsection ‹Join›

text ‹
  ‹gamma_state_supI1›/‹gamma_state_supI2› lifted through \<^const>‹gamma_state_lift›:
  a witness on one side of a lifted join survives it, whether the other side
  is \<^const>‹Bot› (the join's identity) or a competing \<^const>‹Lifted› payload.
›

lemma gamma_state_lift_supI1 [intro]:
  "s ∈ γ⇩⊥ x ⟹ s ∈ γ⇩⊥ (x ⊔ y)"
  for x y :: "'a::numeric_domain abs_state lifted"
  by (cases x; cases y) auto

lemma gamma_state_lift_supI2 [intro]:
  "s ∈ γ⇩⊥ y ⟹ s ∈ γ⇩⊥ (x ⊔ y)"
  for x y :: "'a::numeric_domain abs_state lifted"
  by (cases x; cases y) auto

subsection ‹Carrying a transfer's soundness through the lift›

text ‹
  A pure transfer's soundness fact carries over the \<^const>‹transfer_lift›
  wrapper by one case split: \<^const>‹Bot›'s concretization is empty, and a
  \<^const>‹normalize_lift› collapse to \<^const>‹Bot› only ever fires when
  ‹empty_pred› holds, whose concretization is empty by assumption. Three shapes
  cover every use --- a collecting inclusion, a membership, and a binary
  membership for a combine --- so no consumer repeats the bottom argument.
›

lemma transfer_lift_sound_collect:
  assumes step: "⋀d'. C (γ d') ⊆ γ (f d')"
    and Cempty: "C {} = {}"
    and empty_pred_sound: "⋀d'. empty_pred d' ⟹ γ d' = {}"
  shows "C (γ⇩⊥ d) ⊆ γ⇩⊥ (transfer_lift empty_pred f d)"
proof (cases d)
  case Bot
  then show ?thesis by (simp add: Cempty)
next
  case (Lifted d')
  have "C (γ d') ⊆ γ (f d')" by (rule step)
  then show ?thesis
    using Lifted empty_pred_sound[of "f d'"] by (auto simp: normalize_lift_def)
qed

lemma transfer_lift_sound_mem:
  assumes step: "⋀d'. s ∈ γ d' ⟹ h s ∈ γ (f d')"
    and empty_pred_sound: "⋀d'. empty_pred d' ⟹ γ d' = {}"
    and s: "s ∈ γ⇩⊥ d"
  shows "h s ∈ γ⇩⊥ (transfer_lift empty_pred f d)"
proof (cases d)
  case Bot
  then show ?thesis using s by simp
next
  case (Lifted d')
  with s have "s ∈ γ d'" by simp
  then have hs: "h s ∈ γ (f d')" by (rule step)
  then have "¬ empty_pred (f d')" using empty_pred_sound by auto
  with Lifted hs show ?thesis by simp
qed

lemma transfer_lift2_sound_mem:
  assumes step: "⋀d1' d2'. s ∈ γ d1' ⟹ t ∈ γ d2' ⟹ h s t ∈ γ (f d1' d2')"
    and empty_pred_sound: "⋀d'. empty_pred d' ⟹ γ d' = {}"
    and s: "s ∈ γ⇩⊥ d1"
    and t: "t ∈ γ⇩⊥ d2"
  shows "h s t ∈ γ⇩⊥ (transfer_lift2 empty_pred f d1 d2)"
proof (cases d1)
  case Bot
  then show ?thesis using s by simp
next
  case (Lifted d1')
  show ?thesis
  proof (cases d2)
    case Bot
    then show ?thesis using t by simp
  next
    case (Lifted d2')
    with ‹d1 = Lifted d1'› s t have "s ∈ γ d1'" "t ∈ γ d2'" by simp_all
    then have hst: "h s t ∈ γ (f d1' d2')" by (rule step)
    then have "¬ empty_pred (f d1' d2')" using empty_pred_sound by auto
    with ‹d1 = Lifted d1'› Lifted hst show ?thesis by simp
  qed
qed

end