Theory Abstract_Domain

theory Abstract_Domain
  imports "TD.Warrowing"
begin

unbundle lattice_syntax

section ‹Abstract value domains›

text ‹
  An executable domain supplies the required lattice operations, the widening
  and narrowing the solver applies (the vendored ‹warrowing› class), and an
  exact emptiness test. Sound domains add a concretization into integers.
  Abstract states and control-flow reachability are separate modules.
›

subsection ‹Exact and sound emptiness›

text ‹
  An emptiness test is ∗‹exact› for a concretization when it holds of exactly the
  values that describe nothing, and ∗‹sound› when every value it holds of describes
  nothing, with no converse. Each layer states which of the two its test is: a single
  domain's and a single state's test are exact, the combined state's only sound,
  because two analyses can each describe some value while their intersection is
  empty.
›

definition sound_emptiness :: "('s ⇒ bool) ⇒ ('s ⇒ 'c set) ⇒ bool" where
  "sound_emptiness e γ' ⟷ (∀x. e x ⟶ γ' x = {})"

definition exact_emptiness :: "('s ⇒ bool) ⇒ ('s ⇒ 'c set) ⇒ bool" where
  "exact_emptiness e γ' ⟷ (∀x. e x ⟷ γ' x = {})"

lemma sound_emptinessI [intro]: "(⋀x. e x ⟹ γ' x = {}) ⟹ sound_emptiness e γ'"
  unfolding sound_emptiness_def by blast

lemma sound_emptinessD [dest]: "sound_emptiness e γ' ⟹ e x ⟹ γ' x = {}"
  unfolding sound_emptiness_def by blast

lemma exact_emptinessI [intro]: "(⋀x. e x ⟷ γ' x = {}) ⟹ exact_emptiness e γ'"
  unfolding exact_emptiness_def by blast

lemma exact_emptinessD: "exact_emptiness e γ' ⟹ e x ⟷ γ' x = {}"
  unfolding exact_emptiness_def by blast

lemma exact_emptiness_sound: "exact_emptiness e γ' ⟹ sound_emptiness e γ'"
  unfolding exact_emptiness_def sound_emptiness_def by blast

subsection ‹Executable and sound domains›

text ‹
  The vendored ‹widening› and ‹narrowing› classes constrain their type
  parameter (‹'a::order›) instead of naming ‹order› as a superclass, so a class
  extending them starts from ‹order› and would reject ‹⊥› and ‹⊤› in its
  axioms. The lattice classes therefore enter the same way, through the sort of
  the first parameter, and ‹numeric_domain› repeats that sort.
›

class executable_domain = warrowing +
  fixes is_empty :: "'a::{bounded_semilattice_sup_bot, order_top} ⇒ bool"
  fixes to_string :: "'a ⇒ String.literal"

text ‹
  A numeric domain adds a concretization ‹gamma› to an executable domain:
  bottom denotes no integer, top every integer, the order is sound for
  ‹gamma›, and ‹is_empty› decides emptiness exactly.
›

class numeric_domain = executable_domain +
  fixes gamma :: "'a::{bounded_semilattice_sup_bot, order_top} ⇒ int set" ("γ")
  assumes gamma_bot[simp]: "γ ⊥ = {}"
  assumes gamma_top[simp]: "γ ⊤ = UNIV"
  assumes gamma_mono: "a ≤ b ⟹ γ a ⊆ γ b"
  assumes is_empty_correct: "is_empty a ⟷ γ a = {}"

lemma exact_emptiness_is_empty: "exact_emptiness is_empty (γ :: 'a::numeric_domain ⇒ int set)"
  by (rule exact_emptinessI) (rule is_empty_correct)

text ‹
  ‹executable_domain› carries exactly the executable per-element operations a
  concrete domain's runtime representation needs: the lattice structure, the
  solver's ‹widen› and ‹narrow›, ‹is_empty› (a finite decision procedure on every real instance
  -- Interval's bound comparison, Sign's constructor match, ...), and
  ‹to_string› for reporting a solved value back to a caller. ‹numeric_domain›
  extends it with ‹gamma›, which is not executable in general (an infinite
  \<^typ>‹int set›) and exists purely to state and prove soundness. Splitting the
  class this way keeps ‹gamma› out of the type-class dictionary that code
  generation must materialize for any constant that only needs ‹is_empty›
  (the finite witness-bottom tests over a ‹default_st›, in
  particular): requesting ‹'a::executable_domain› there never drags \<^const>‹gamma›'s
  code equation into the dependency closure, even though every
  \<^class>‹numeric_domain› instance is automatically a \<^class>‹executable_domain›
  instance too.
›

text ‹
  ‹is_empty› is a semantic classifier, not a structural equality
  test against ‹bot›: it mirrors Goblint's own ‹Lattice.Bot›
  signature (@{url "https://github.com/goblint/analyzer/blob/master/src/domain/lattice.ml"}):
  ‹val is_bot: t -> bool› is a per-domain operation there too, not a
  generic derived test. Goblint's own default implementation (‹IntDomain0.Std›
  in
  @{url "https://github.com/goblint/analyzer/blob/master/src/cdomain/value/cdomains/intDomain0.ml"})
  in fact defines it as structural equality against one canonical ‹bot_of›
  value, since most of its domains keep a single bottom representation
  (Interval's ‹bot () = None›, normalized on every operation). Voblint
  cannot take that shortcut: some Voblint domains admit representations with
  more than one empty-denoting value that are never normalized away
  (Interval's inverted bound pairs, e.g. \<^term>‹Ivl (Fin 5) (Fin (-1))›, none
  of them favored over ‹bot› itself), so ‹a = bot› would silently miss some
  of them. Fixing ‹is_empty› as its own class operation, correct against
  \<^const>‹gamma› rather than against \<^const>‹bot›, makes every
  \<^class>‹numeric_domain› instance responsible for its own exact emptiness
  test, the same obligation every domain already carries for
  \<^const>‹gamma› itself. The lattice constant ‹bot› stays the canonical
  representative; ‹is_empty› answers a different question (what a
  value denotes), and a proof that genuinely needs the canonical element
  still writes ‹a = bot› directly.
›

subsection ‹Concretization bounds›

lemma gamma_sup_ub1[intro]: "γ a ⊆ γ (a ⊔ b)" for a b :: "'a::numeric_domain"
  by (rule gamma_mono[OF sup_ge1])

lemma gamma_sup_ub2[intro]: "γ b ⊆ γ (a ⊔ b)" for a b :: "'a::numeric_domain"
  by (rule gamma_mono[OF sup_ge2])

text ‹
  Emptiness is downward closed under the abstract order: it follows from
  ‹gamma_mono› alone, with no per-domain fact needed. This is what lets the
  generic transfer dispatcher's short-circuit stay monotone: a smaller input
  can only be witness-empty ∗‹more› often than a larger one, never less.
›
lemma is_empty_antimono:
  "a ≤ b ⟹ is_empty b ⟹ is_empty a" for a b :: "'a::numeric_domain"
  using gamma_mono unfolding is_empty_correct by blast

subsection ‹Domains with widening›

text ‹
  ‹warrow› is deliberately not join-like: it takes the narrowing branch
  whenever ‹b ≤ a›, and narrowing moves the result down toward ‹b›, not up
  past ‹a›, so no ‹a ≤ a ∇Δ b› counterpart to ‹warrowing_properties› holds
  in general. What does hold unconditionally in that regime is the matching
  upper bound on the ‹a› side, ‹warrow_le_when_le›, together with
  ‹warrowing_properties›' ‹b ≤ a ∇Δ b› that gives the full sandwich
  ‹b ≤ a ∇Δ b ≤ a›. ‹warrow_idem› is the fixpoint case of that sandwich.
›

subsection ‹Printing values›

text ‹
  How a solved value is shown, following Goblint's notation (‹1+3ℤ›, ‹⊤›,
  ‹⊥›). Nothing is proved about it: it is not part of any soundness claim.

  A \<^typ>‹String.literal› holds ASCII only, so a mathematical symbol is written
  as its Isabelle symbol name without the backslash --- ‹<int>› for ‹ℤ› --- and
  the CLI decodes these tokens into Unicode before rendering. No variable name,
  numeral or bracket a printer emits contains ‹<›, so the tokens are unambiguous.
›

abbreviation (input) sym_bottom :: String.literal where "sym_bottom ≡ STR ''<bottom>''"
abbreviation (input) sym_top :: String.literal where "sym_top ≡ STR ''<top>''"
abbreviation (input) sym_int :: String.literal where "sym_int ≡ STR ''<int>''"
abbreviation (input) sym_infinity :: String.literal where "sym_infinity ≡ STR ''<infinity>''"
abbreviation (input) sym_le :: String.literal where "sym_le ≡ STR ''<le>''"
abbreviation (input) sym_ge :: String.literal where "sym_ge ≡ STR ''<ge>''"
abbreviation (input) sym_and :: String.literal where "sym_and ≡ STR ''<and>''"

fun string_of_nat :: "nat ⇒ String.literal" where
  "string_of_nat n =
     (if n < 10 then String.implode [char_of (n + 48)]
      else string_of_nat (n div 10) + String.implode [char_of (n mod 10 + 48)])"

definition string_of_int :: "int ⇒ String.literal" where
  "string_of_int i =
     (if i < 0 then STR ''-'' + string_of_nat (nat (- i))
      else string_of_nat (nat i))"

end