Theory Voblint_Domain.Query_Lift

theory Query_Lift
  imports Main
begin

unbundle lattice_syntax

section ‹Lifting a domain with a fresh bottom and top›

text ‹
  Goblint answers ‹EvalInt› in ‹Lattice.Lift(IntDomTuple)›
  (‹valueDomainQueries.ml› at ‹0dc12d355›): the integer domain with a fresh
  ‹⊥› and ‹⊤› around it. The fresh top lets an analysis that does not
  understand a query decline it without knowing the value domain's own top,
  and the fresh bottom marks a query asked of an unreachable state. This is
  kept apart from the reachability lift of the solver's carrier: the two
  bottoms mean different things, and only this one has a fresh top.
›

datatype 'a query_lift = QBot | QLifted 'a | QTop

instantiation query_lift :: (ord) ord
begin

fun less_eq_query_lift :: "'a query_lift ⇒ 'a query_lift ⇒ bool" where
  "less_eq_query_lift QBot _ = True"
| "less_eq_query_lift _ QTop = True"
| "less_eq_query_lift (QLifted a) (QLifted b) = (a ≤ b)"
| "less_eq_query_lift _ _ = False"

definition less_query_lift :: "'a query_lift ⇒ 'a query_lift ⇒ bool" where
  "less_query_lift a b ⟷ a ≤ b ∧ ¬ b ≤ a"

instance ..

end

instance query_lift :: (order) order
proof
  fix x y z :: "'a query_lift"
  show "x < y ⟷ x ≤ y ∧ ¬ y ≤ x"
    by (simp add: less_query_lift_def)
  show "x ≤ x"
    by (cases x) simp_all
  show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
    by (cases x; cases y; cases z) auto
  show "x ≤ y ⟹ y ≤ x ⟹ x = y"
    by (cases x; cases y) auto
qed

instantiation query_lift :: (order) order_bot
begin
definition bot_query_lift :: "'a query_lift" where "bot_query_lift = QBot"
instance by standard (simp add: bot_query_lift_def)
end

instantiation query_lift :: (order) order_top
begin
definition top_query_lift :: "'a query_lift" where "top_query_lift = QTop"
instance
proof
  fix x :: "'a query_lift"
  show "x ≤ ⊤"
    by (cases x) (simp_all add: top_query_lift_def)
qed
end

text ‹
  ‹QTop› is the identity of the meet and ‹QBot› absorbs it; two lifted
  values meet in the underlying domain.
›

instantiation query_lift :: (inf) inf
begin

fun inf_query_lift :: "'a query_lift ⇒ 'a query_lift ⇒ 'a query_lift" where
  "inf_query_lift QBot _ = QBot"
| "inf_query_lift _ QBot = QBot"
| "inf_query_lift QTop b = b"
| "inf_query_lift a QTop = a"
| "inf_query_lift (QLifted a) (QLifted b) = QLifted (a ⊓ b)"

instance ..

end

instance query_lift :: (semilattice_inf) semilattice_inf
proof
  fix x y z :: "'a query_lift"
  show "x ⊓ y ≤ x"
    by (cases x; cases y) simp_all
  show "x ⊓ y ≤ y"
    by (cases x; cases y) simp_all
  show "x ≤ y ⟹ x ≤ z ⟹ x ≤ y ⊓ z"
    by (cases x; cases y; cases z) simp_all
qed

subsection ‹Concretization›

text ‹
  A lifted value denotes what the underlying domain says; the fresh bottom
  denotes nothing and the fresh top everything. An exact underlying meet
  stays exact after lifting.
›

fun gamma_query_lift :: "('a ⇒ 'b set) ⇒ 'a query_lift ⇒ 'b set" where
  "gamma_query_lift γ QBot = {}"
| "gamma_query_lift γ (QLifted a) = γ a"
| "gamma_query_lift γ QTop = UNIV"

lemma gamma_query_lift_top [simp]: "gamma_query_lift γ ⊤ = UNIV"
  by (simp add: top_query_lift_def)

lemma gamma_query_lift_bot [simp]: "gamma_query_lift γ ⊥ = {}"
  by (simp add: bot_query_lift_def)

lemma gamma_query_lift_inf:
  assumes "⋀a b. γ (a ⊓ b) = γ a ∩ γ b"
  shows "gamma_query_lift γ (x ⊓ y) = gamma_query_lift γ x ∩ gamma_query_lift γ y"
  using assms by (cases x; cases y) simp_all

end