Theory Voblint_Domain.Order_Lattice

theory Order_Lattice
  imports "Voblint_Domain.State_Concretization"
    "HOL-Library.Product_Lexorder"
begin

section ‹Order lattice›

text ‹
  ‹relc› tracks a finite set of known pairwise-ordered variables, ‹(x, y)›
  meaning ‹x ≤ y› at every store the value describes. No closure: two known
  facts ‹x ≤ y› and ‹y ≤ z› do not automatically yield ‹x ≤ z› in this
  carrier. This is deliberately the least amount of relational structure that
  is still relational (a pair of variables, not one) and not ‹abs_state›
  (no ‹vname ⇒ 'a› function type anywhere in the carrier). Its concretization is a
  set of stores, not of integers, so it is an \<^class>‹executable_domain› but not a
  \<^class>‹numeric_domain›.
›

subsection ‹Carrier and order›

datatype relc = RelBot | RelC (relc_pairs: "(vname × vname) set")

text ‹Order is reverse inclusion on the constraint set: more known pairs is
  more information, hence lower (more precise) in the abstract-interpretation
  order. ‹sup› keeps only the pairs both sides agree on.

  ‹RelBot› is a separate explicit constructor rather than ‹RelC UNIV› (the
  most-constrained set, "every pair known ordered"): representing ‹UNIV›
  forces the code generator to use the ‹Coset› branch of HOL's executable-set
  representation, and the stock library does not give every set operation
  (subset test among them) a code equation for every ‹Set›/‹Coset›
  combination over an infinite element type such as ‹vname› -- confirmed
  directly: ‹RelC UNIV› batch-checked and even unit-tested via ‹value›
  cleanly, but running it through the solver raised ‹exception Match› in
  the generated code the first time a genuine ‹Coset›/‹Coset› combination
  arose. Keeping ‹RelC›'s field always finite avoids the gap entirely: no
  value this theory ever constructs is a ‹Coset›.›

instantiation relc :: bounded_semilattice_sup_bot
begin

fun less_eq_relc :: "relc ⇒ relc ⇒ bool" where
  "less_eq_relc RelBot _ = True"
| "less_eq_relc (RelC _) RelBot = False"
| "less_eq_relc (RelC a) (RelC b) = (b ⊆ a)"

definition less_relc :: "relc ⇒ relc ⇒ bool" where
  "less_relc a b ⟷ a ≤ b ∧ ¬ b ≤ a"

fun sup_relc :: "relc ⇒ relc ⇒ relc" where
  "sup_relc RelBot b = b"
| "sup_relc a RelBot = a"
| "sup_relc (RelC a) (RelC b) = RelC (a ∩ b)"

definition bot_relc :: relc where
  "bot_relc = RelBot"

instance
proof intro_classes
  fix x y z :: relc
  show "x < y ⟷ x ≤ y ∧ ¬ y ≤ x" by (simp add: less_relc_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
  show "x ≤ x ⊔ y" by (cases x; cases y) auto
  show "y ≤ x ⊔ y" by (cases x; cases y) auto
  show "y ≤ x ⟹ z ≤ x ⟹ y ⊔ z ≤ x" by (cases x; cases y; cases z) auto
  show "bot ≤ x" by (cases x) (simp_all add: bot_relc_def)
qed

end

lemma bot_relc_eq [simp]: "(⊥ :: relc) = RelBot"
  by (simp add: bot_relc_def)

text ‹‹⊤› is the empty constraint set: vacuously true of every pair, so its
  concretization is ‹UNIV› (‹gamma_relc_top›).›

instantiation relc :: order_top
begin

definition top_relc :: relc where
  "top_relc = RelC {}"

instance by intro_classes (case_tac a; simp add: top_relc_def)

end

text ‹The vendored TD solver's ‹TD_side_upd_rule› locale fixes its equation
  value type at sort ‹{bounded_semilattice_sup_bot, warrowing}› uniformly --
  every update rule in the solver menu needs it, not only the ‹warrow›
  entry, even on a loop-free equation system where widening is never
  actually invoked. ‹widen = sup› reuses the join laws already proved
  above; ‹narrow a b = b› is the simplest sound choice ("accept the
  incoming value, refine nothing") -- consistent with this carrier's own
  no-closure, no-normalization scope.›

instantiation relc :: warrowing
begin

definition widen_relc :: "relc ⇒ relc ⇒ relc" where
  "widen_relc a b = a ⊔ b"

definition narrow_relc :: "relc ⇒ relc ⇒ relc" where
  "narrow_relc a b = b"

instance
proof intro_classes
  fix a b :: relc
  show "a ≤ a ∇ b" by (simp add: widen_relc_def)
  show "b ≤ a ∇ b" by (simp add: widen_relc_def)
  show "b ≤ a ⟹ b ≤ a Δ b" by (simp add: narrow_relc_def)
  show "b ≤ a ⟹ a Δ b ≤ a" by (simp add: narrow_relc_def)
qed

end

subsection ‹Concretization›

text ‹
  A set of pairs denotes the stores satisfying ‹s x <= s y› for each pair;
  ‹RelBot› denotes no store. Concretization is monotone in the order.
›

fun gamma_relc :: "relc ⇒ store set" where
  "gamma_relc RelBot = {}"
| "gamma_relc (RelC ps) = {s. ∀(x, y) ∈ ps. s x ≤ s y}"

adhoc_overloading gamma_S == gamma_relc

lemma gamma_relc_top [simp]: "γ (⊤ :: relc) = UNIV"
  unfolding top_relc_def by simp

lemma gamma_relc_mono:
  fixes d d' :: relc
  assumes "d ≤ d'"
  shows "γ d ⊆ γ d'"
  using assms by (cases d; cases d') auto

text ‹
  Executable membership reader. ‹RelBot› answers ‹True› for every pair: its
  concretization is empty, so every fact holds of it vacuously, and it never needs
  to materialize ‹UNIV›.
›

fun relc_has :: "vname ⇒ vname ⇒ relc ⇒ bool" where
  "relc_has x y RelBot = True"
| "relc_has x y (RelC ps) = ((x, y) ∈ ps)"

subsection ‹Forgetting a variable›

text ‹The one operation every imprecise fallback reuses.›

fun forget_relc :: "vname ⇒ relc ⇒ relc" where
  "forget_relc x RelBot = RelBot"
| "forget_relc x (RelC ps) = RelC {(a, b) ∈ ps. a ≠ x ∧ b ≠ x}"

lemma forget_relc_sound[intro]:
  assumes "s ∈ γ d"
  shows "s(x := v) ∈ γ (forget_relc x d)"
  using assms by (cases d) auto

subsection ‹Executable operations›

text ‹
  The notation follows Goblint's two-variable equality domain, which prints a
  conjunction ‹{x=y ∧ z=y}› and its extremes as ‹⊥› and ‹⊤›; here each conjunct is
  an ordering ‹x≤y›. ‹vname × vname› is ‹linorder› (‹Product_Lexorder›), so
  \<^const>‹sorted_list_of_set› gives a deterministic enumeration.
›

fun string_of_pairs :: "(vname × vname) list ⇒ String.literal" where
  "string_of_pairs [] = STR ''''"
| "string_of_pairs [(x, y)] = x + sym_le + y"
| "string_of_pairs ((x, y) # p # ps) =
      x + sym_le + y + STR '' '' + sym_and + STR '' '' + string_of_pairs (p # ps)"

instantiation relc :: executable_domain
begin

definition is_empty_relc :: "relc ⇒ bool" where
  "is_empty_relc d ⟷ d = RelBot"

definition to_string_relc :: "relc ⇒ String.literal" where
  "to_string_relc d =
     (case d of
        RelBot ⇒ sym_bottom
      | RelC ps ⇒
          (if ps = {} then sym_top
           else STR ''{'' + string_of_pairs (sorted_list_of_set ps) + STR ''}''))"

instance ..

end

lemma is_empty_relc_gamma: "is_empty d ⟷ γ d = {}" for d :: relc
proof (cases d)
  case (RelC ps)
  then have "(λ_. 0) ∈ γ d" by auto
  with RelC show ?thesis by (auto simp: is_empty_relc_def)
qed (simp add: is_empty_relc_def)

lemma exact_emptiness_relc: "exact_emptiness (is_empty :: relc ⇒ bool) gamma_relc"
  by (rule exact_emptinessI) (rule is_empty_relc_gamma)

end