Theory Voblint_Analysis_Congruence.Congruence_Warrowing

theory Congruence_Warrowing
  imports "Voblint_Domain.Congruence_Lattice" "Voblint_Exec.Default_St_Reachability"
begin

section ‹Type-class warrowing for the TD warrowing solver›

text ‹
  Congruence follows Sign's and Parity's own choice
  (‹Sign_Lattice›, ‹Parity_Domain›): the vendored ‹widening›/
  ‹narrowing› classes require only the four upper/bracket laws below, not a
  termination proof, so a domain whose lattice is already well behaved gets
  a conservative instance rather than an invented acceleration mechanism.
  Widening is plain join; narrowing is the trivial left projection, which
  discharges ‹narrow_ge›/‹narrow_le› immediately from ‹b <= a› without
  needing anything about congruence's own structure.
›

definition narrow_congruence_td :: "congruence => congruence => congruence" where
  "narrow_congruence_td a b = a"

instantiation congruence :: warrowing
begin

definition widen_congruence :: "congruence => congruence => congruence" where
  "((a :: congruence) ∇ b) = join_congruence a b"

definition narrow_congruence :: "congruence => congruence => congruence" where
  "((a :: congruence) Δ b) = narrow_congruence_td a b"

instance proof intro_classes
  fix a b :: congruence
  show "a <= (a ∇ b)"
    unfolding widen_congruence_def by (rule join_congruence_ub1)
  show "b <= (a ∇ b)"
    unfolding widen_congruence_def by (rule join_congruence_ub2)
  show "b <= a ⟹ b <= (a Δ b)"
    unfolding narrow_congruence_def narrow_congruence_td_def by simp
  show "b <= a ⟹ (a Δ b) <= a"
    unfolding narrow_congruence_def narrow_congruence_td_def by simp
qed

end

section ‹Numeric domain instance›

text ‹‹numeric_domain› extends ‹executable_domain›, which includes the solver's
  ‹warrowing›, so the instance follows the widening and narrowing above.›

instantiation congruence :: numeric_domain
begin

definition gamma_abs_congruence [simp]:
  "numeric_domain_class.gamma (a :: congruence) = gamma_congruence a"

definition is_empty_congruence [simp]:
  "is_empty (a :: congruence) = is_bottom_congruence a"

definition to_string_congruence [simp]:
  "to_string (a :: congruence) =
     (if is_top_congruence a then sym_top else string_of_congruence a)"

instance
proof intro_classes
  show "numeric_domain_class.gamma (bot :: congruence) = {}"
    unfolding bot_congruence_def by simp
next
  show "numeric_domain_class.gamma (top :: congruence) = UNIV"
    by simp
next
  fix a b :: congruence
  assume "a <= b"
  then show "numeric_domain_class.gamma a ⊆ numeric_domain_class.gamma b"
    unfolding less_eq_congruence_iff_gamma
    by simp
next
  fix a :: congruence
  show "is_empty a ⟷ numeric_domain_class.gamma a = {}"
    by (simp add: is_bottom_congruence_correct)
qed

end

end