Theory Interval_Warrowing

theory Interval_Warrowing
  imports "Voblint_Domain.Interval_Lattice"
begin

section ‹Interval widening and narrowing›

text ‹
  The interval lattice has infinite ascending chains, so the solver needs widening
  to terminate and narrowing to recover precision afterwards. This theory defines
  both and instantiates intervals as a numeric domain.
›

subsection ‹Widening›

text ‹
  Standard interval widening: keep a bound if it did not move outward, otherwise
  push it to the infinite end.  Every widen-ascending chain therefore stabilises
  after at most two steps (each bound takes at most one outward jump).
›

fun widen_ivl_core :: "ivl => ivl => ivl" where
    "widen_ivl_core (Ivl l1 u1) (Ivl l2 u2) =
       Ivl (if l1 ≤ l2 then l1 else MinInf)
           (if u2 ≤ u1 then u1 else PlusInf)"

lemma a_le_widen_ivl_core: "(a :: ivl) ≤ widen_ivl_core a b"
proof (cases a; cases b)
  fix l1 u1 l2 u2 :: eint
  assume "a = Ivl l1 u1" "b = Ivl l2 u2"
  then show "a ≤ widen_ivl_core a b"
    unfolding less_eq_ivl_def by auto
qed

lemma b_le_widen_ivl_core: "(b :: ivl) ≤ widen_ivl_core a b"
proof (cases a; cases b)
  fix l1 u1 l2 u2 :: eint
  assume "a = Ivl l1 u1" "b = Ivl l2 u2"
  then show "b ≤ widen_ivl_core a b"
    unfolding less_eq_ivl_def
    using eint_le_linear[of l1 l2] eint_le_linear[of u2 u1]
    by auto
qed

text ‹
  Widening termination: every widen-ascending chain stabilises.  At each step
  each bound either stays or jumps to @{text MinInf} / @{text PlusInf}, and once
  a bound reaches the infinite end it remains there.  After at most two
  transitions the chain is constant.
›
lemma widen_ivl_core_terminates:
  assumes "∀i. widen_ivl_core (f i) (f (Suc i)) = f (Suc i)"
  shows "∃n. ∀j. n ≤ j ⟶ f j = f n"
proof -
  define lb where "lb i = ivl_lower (f i)" for i
  define ub where "ub i = ivl_upper (f i)" for i
  have f_eq: "f i = Ivl (lb i) (ub i)" for i
    unfolding lb_def ub_def by (cases "f i") simp
  have step:
    "lb (Suc i) = lb i ∨ lb (Suc i) = MinInf"
    "ub (Suc i) = ub i ∨ ub (Suc i) = PlusInf"
    for i
  proof -
    have "widen_ivl_core (Ivl (lb i) (ub i)) (Ivl (lb (Suc i)) (ub (Suc i))) =
          Ivl (lb (Suc i)) (ub (Suc i))"
      using assms[rule_format, of i] f_eq[of i] f_eq[of "Suc i"] by simp
    then have eqs:
      "lb (Suc i) = (if eint_le (lb i) (lb (Suc i)) then lb i else MinInf)"
      "ub (Suc i) = (if eint_le (ub (Suc i)) (ub i) then ub i else PlusInf)"
      by simp_all
    from eqs(1) show "lb (Suc i) = lb i ∨ lb (Suc i) = MinInf"
      by (auto split: if_splits)
    from eqs(2) show "ub (Suc i) = ub i ∨ ub (Suc i) = PlusInf"
      by (auto split: if_splits)
  qed
  have lb_stay: "lb i = MinInf ⟹ lb (Suc i) = MinInf" for i
    using step(1) by metis
  have ub_stay: "ub i = PlusInf ⟹ ub (Suc i) = PlusInf" for i
    using step(2) by metis
  have lb_stay_le: "lb i = MinInf ⟹ i ≤ j ⟹ lb j = MinInf" for i j
  proof (induct j)
    case 0 thus ?case by simp
  next
    case (Suc j) thus ?case using lb_stay le_SucE by metis
  qed
  have ub_stay_le: "ub i = PlusInf ⟹ i ≤ j ⟹ ub j = PlusInf" for i j
  proof (induct j)
    case 0 thus ?case by simp
  next
    case (Suc j) thus ?case using ub_stay le_SucE by metis
  qed
  have lb_const_if_no_MinInf:
    "(∀k. lb k ≠ MinInf) ⟹ lb j = lb 0" for j
  proof (induct j)
    case 0 thus ?case by simp
  next
    case (Suc j) thus ?case using step(1)[of j] by auto
  qed
  have ub_const_if_no_PlusInf:
    "(∀k. ub k ≠ PlusInf) ⟹ ub j = ub 0" for j
  proof (induct j)
    case 0 thus ?case by simp
  next
    case (Suc j) thus ?case using step(2)[of j] by auto
  qed
  obtain nl where nl: "∀j ≥ nl. lb j = lb nl"
  proof (cases "∃k. lb k = MinInf")
    case True
    then obtain k where "lb k = MinInf" by blast
    then have "∀j ≥ k. lb j = MinInf" using lb_stay_le by blast
    then have "∀j ≥ k. lb j = lb k" using ‹lb k = MinInf› by simp
    then show ?thesis by (rule that)
  next
    case False
    then have "∀k. lb k ≠ MinInf" by blast
    then have "∀j. lb j = lb 0" using lb_const_if_no_MinInf by blast
    then have "∀j ≥ 0. lb j = lb 0" by blast
    then show ?thesis by (rule that)
  qed
  obtain nu where nu: "∀j ≥ nu. ub j = ub nu"
  proof (cases "∃k. ub k = PlusInf")
    case True
    then obtain k where "ub k = PlusInf" by blast
    then have "∀j ≥ k. ub j = PlusInf" using ub_stay_le by blast
    then have "∀j ≥ k. ub j = ub k" using ‹ub k = PlusInf› by simp
    then show ?thesis by (rule that)
  next
    case False
    then have "∀k. ub k ≠ PlusInf" by blast
    then have "∀j. ub j = ub 0" using ub_const_if_no_PlusInf by blast
    then have "∀j ≥ 0. ub j = ub 0" by blast
    then show ?thesis by (rule that)
  qed
  let ?n = "max nl nu"
  have "∀j. ?n ≤ j ⟶ f j = f ?n"
  proof (intro allI impI)
    fix j assume jn: "?n ≤ j"
    have lb_eq: "lb j = lb ?n"
    proof -
      from jn have "nl ≤ j" "nl ≤ ?n" by auto
      then have "lb j = lb nl" "lb ?n = lb nl"
        using nl by blast+
      then show ?thesis by simp
    qed
    have ub_eq: "ub j = ub ?n"
    proof -
      from jn have "nu ≤ j" "nu ≤ ?n" by auto
      then have "ub j = ub nu" "ub ?n = ub nu"
        using nu by blast+
      then show ?thesis by simp
    qed
    show "f j = f ?n"
      using f_eq[of j] f_eq[of ?n] lb_eq ub_eq by simp
  qed
  then show ?thesis by blast
qed


subsection ‹Type-class widening for TD warrowing solver›

text ‹Standard interval narrowing: when the recomputed value ‹b› refines the widened value
  ‹a› (‹b ≤ a›), keep ‹a›'s finite bounds and only fill an infinite bound of ‹a› from ‹b›.
  A bound moves off an infinite endpoint at most once, so the narrowing descent is finite.  Combined with
  the backward guard filters this recovers loop bounds under ∗‹every› update rule (a bounded
  local counter reads ‹[0, 20]› under ‹join›, ‹per_origin› and ‹warrow› alike).  It does not
  help a ∗‹flow-insensitive global›: there the guard never bounds the value written back to
  the slot, so ‹[0, +inf]› is a genuine fixpoint and narrowing has nothing smaller to descend
  to.›
fun narrow_ivl_td :: "ivl ⇒ ivl ⇒ ivl" where
  "narrow_ivl_td (Ivl l1 u1) (Ivl l2 u2) =
     Ivl (if l1 = MinInf then l2 else l1) (if u1 = PlusInf then u2 else u1)"

instantiation ivl :: warrowing begin
  text ‹Widening carries the standard bot-law ‹bot ∇ x = x›, ‹x ∇ bot = x›: since
    \<^term>‹bot :: ivl› is the empty interval \<^term>‹Ivl PlusInf MinInf›, an unguarded
    \<^const>‹widen_ivl_core› from bot would jump straight to the top interval, topping any
    unknown on its first stabilisation.  The guard keeps the first contribution exact.›
  definition "((a :: ivl) ∇ b) =
     (if a = bot then b else if b = bot then a else widen_ivl_core a b)"
  definition "((a :: ivl) Δ b) = narrow_ivl_td a b"
instance proof intro_classes
  fix a b :: ivl
  show "a ≤ (a ∇ b)"
  proof (cases "a = bot")
    case True thus ?thesis by (simp add: widen_ivl_def)
  next
    case False thus ?thesis
      by (cases "b = bot") (simp_all add: widen_ivl_def a_le_widen_ivl_core)
  qed
  show "b ≤ (a ∇ b)"
  proof (cases "a = bot")
    case True thus ?thesis by (simp add: widen_ivl_def)
  next
    case False thus ?thesis
      by (cases "b = bot") (simp_all add: widen_ivl_def b_le_widen_ivl_core)
  qed
  show "b ≤ a ⟹ b ≤ (a Δ b)"
    unfolding narrow_ivl_def
    by (cases a; cases b) (auto simp: less_eq_ivl_def split: if_splits)
  show "b ≤ a ⟹ (a Δ b) ≤ a"
    unfolding narrow_ivl_def
    by (cases a; cases b) (auto simp: less_eq_ivl_def split: if_splits)
qed
end

subsection ‹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 ivl :: numeric_domain begin
definition gamma_abs_ivl [simp]: "numeric_domain_class.gamma (a :: ivl) = gamma_ivl a"
definition is_empty_ivl [simp]: "is_empty (a :: ivl) = is_bottom_ivl a"
definition to_string_ivl [simp]:
  "to_string (a :: ivl) = (if is_top_ivl a then sym_top else string_of_ivl a)"
instance proof intro_classes
  show "numeric_domain_class.gamma (bot :: ivl) = {}"
    by (simp add: gamma_ivl_bot)
next
  show "numeric_domain_class.gamma (top :: ivl) = UNIV"
    by (simp add: gamma_ivl_top top_ivl_def)
next
  fix a b :: ivl
  assume H: "a ≤ b"
  show "numeric_domain_class.gamma a ⊆ numeric_domain_class.gamma b"
  proof -
    have "gamma_ivl a ⊆ gamma_ivl b" using H by (rule gamma_ivl_mono)
    then show ?thesis by simp
  qed
next
  fix a :: ivl
  show "is_empty a ⟷ numeric_domain_class.gamma a = {}"
    by (simp add: is_bottom_ivl_correct)
qed
end

end