Theory Int_Warrowing

theory Int_Warrowing
  imports
    "Voblint_Domain.Int_Lattice"
    "Voblint_Analysis_Sign.Sign_Warrowing"
    "Voblint_Analysis_Parity.Parity_Warrowing"
    "Voblint_Analysis_Interval.Interval_Warrowing"
    "Voblint_Analysis_Congruence.Congruence_Warrowing"
begin

section ‹Composite widening and narrowing›

text ‹
  Purely componentwise, with no reduced-product refinement attached to
  either operation. Widening already matches Goblint's own ‹~norefine:true›
  choice for ‹join›/‹widen›. Narrowing is a deliberate divergence from
  Goblint's ‹IntDomTuple›, forced by the vendored TD solver's interface:

  ‹narrow_ge: b <= a ==> b <= a Δ b›
  ‹narrow_le: b <= a ==> a Δ b <= a›

  Suppose componentwise narrowing gives ‹b <= narrow_raw a b <= a› and
  refinement is then applied on top, Goblint-style:
  ‹refine mode (narrow_raw a b)›. Refinement is reductive
  (‹Int_Refinement_Control.refine_reductive›), so the result stays ‹<= narrow_raw a
  b <= a› and ‹narrow_le› survives -- but there is no general reason for
  ‹b <= refine mode (narrow_raw a b)› to hold. Refinement may push the
  result strictly below ‹b›.

  The tempting escape is a stability argument: if ‹b› were already
  refinement-stable (‹refine mode b = b›) and refinement is monotone, then
  ‹b = refine mode b <= refine mode (narrow_raw a b)› would follow from
  ‹b <= narrow_raw a b›. But that needs every value reaching narrowing to
  already be refinement-stable, and this carrier has no such invariant:
  ‹Int_Backward›'s own composite examples exercise values such as
  ‹STop × [-1,0] × PEven × top›, where ‹refine mode b ~= b›. Join and
  widening deliberately do not refine either (mirroring Goblint's
  ‹~norefine:true› for both), so a value reaching narrowing by way of a
  widened solver state is not guaranteed stable. Building narrowing on an
  invariant the type does not enforce would be unsound at the class
  instance, not merely imprecise.

  Composite widening and narrowing therefore run no refinement at all,
  matching every other component's own choice (‹Sign_Warrowing›,
  ‹Interval_Warrowing›, ‹Parity_Warrowing›, ‹Congruence_Warrowing›):
  each component widens/narrows on its own terms, and the composite record
  update runs no cross-component step afterward.
›

text ‹
  The lattice instance in ‹Int_Lattice› sits on the record scheme
  ‹'a int_dom_scheme›, so ‹widen›/‹narrow› follow the same route and need
  ‹warrowing› on the scheme's ‹more› field too. ‹unit›, the ‹more› type of
  the closed ‹int_dom›, gets the trivial instance.
›

instantiation unit :: warrowing
begin
definition widen_unit :: "unit => unit => unit" where "(a ∇ b) = ()"
definition narrow_unit :: "unit => unit => unit" where "(a Δ b) = ()"
instance by intro_classes simp_all
end

instantiation int_dom_ext :: ("{bounded_lattice, warrowing}") warrowing
begin

definition widen_int_dom_ext :: "'a int_dom_scheme => 'a int_dom_scheme => 'a int_dom_scheme" where
  "((a :: 'a int_dom_scheme) ∇ b) =
     int_dom.extend
       (int_dom.truncate
         (a⦇
           int_sign := (int_sign a ∇ int_sign b),
           int_ivl := (int_ivl a ∇ int_ivl b),
           int_parity := (int_parity a ∇ int_parity b),
           int_congruence := (int_congruence a ∇ int_congruence b)
         ⦈))
       (int_dom.more a ∇ int_dom.more b)"

definition narrow_int_dom_ext :: "'a int_dom_scheme => 'a int_dom_scheme => 'a int_dom_scheme" where
  "((a :: 'a int_dom_scheme) Δ b) =
     int_dom.extend
       (int_dom.truncate
         (a⦇
           int_sign := (int_sign a Δ (int_sign b)),
           int_ivl := (int_ivl a Δ (int_ivl b)),
           int_parity := (int_parity a Δ (int_parity b)),
           int_congruence := (int_congruence a Δ (int_congruence b))
         ⦈))
       (int_dom.more a Δ (int_dom.more b))"

lemma int_dom_extend_truncate_select [simp]:
  "int_sign (int_dom.extend (int_dom.truncate r) m) = int_sign r"
  "int_ivl (int_dom.extend (int_dom.truncate r) m) = int_ivl r"
  "int_parity (int_dom.extend (int_dom.truncate r) m) = int_parity r"
  "int_congruence (int_dom.extend (int_dom.truncate r) m) = int_congruence r"
  "int_dom.more (int_dom.extend (int_dom.truncate r) m) = m"
  by (simp_all add: int_dom.defs)

instance proof intro_classes
  fix a b :: "'a int_dom_scheme"
  assume ba: "b <= a"
  have hb: "int_sign b <= int_sign a" "int_ivl b <= int_ivl a"
           "int_parity b <= int_parity a" "int_congruence b <= int_congruence a"
           "int_dom.more b <= int_dom.more a"
    using ba by (simp_all add: less_eq_int_dom_ext_def)
  have s: "int_sign b <= (int_sign a Δ (int_sign b))"
    by (rule narrow_ge[OF hb(1)])
  have i: "int_ivl b <= (int_ivl a Δ (int_ivl b))"
    by (rule narrow_ge[OF hb(2)])
  have p: "int_parity b <= (int_parity a Δ (int_parity b))"
    by (rule narrow_ge[OF hb(3)])
  have c: "int_congruence b <= (int_congruence a Δ (int_congruence b))"
    by (rule narrow_ge[OF hb(4)])
  have m: "int_dom.more b <= (int_dom.more a Δ (int_dom.more b))"
    by (rule narrow_ge[OF hb(5)])
  show "b <= (a Δ b)"
    unfolding narrow_int_dom_ext_def less_eq_int_dom_ext_def
    using s i p c m by simp
next
  fix a b :: "'a int_dom_scheme"
  assume ba: "b <= a"
  have hb: "int_sign b <= int_sign a" "int_ivl b <= int_ivl a"
           "int_parity b <= int_parity a" "int_congruence b <= int_congruence a"
           "int_dom.more b <= int_dom.more a"
    using ba by (simp_all add: less_eq_int_dom_ext_def)
  have s: "(int_sign a Δ (int_sign b)) <= int_sign a"
    by (rule narrow_le[OF hb(1)])
  have i: "(int_ivl a Δ (int_ivl b)) <= int_ivl a"
    by (rule narrow_le[OF hb(2)])
  have p: "(int_parity a Δ (int_parity b)) <= int_parity a"
    by (rule narrow_le[OF hb(3)])
  have c: "(int_congruence a Δ (int_congruence b)) <= int_congruence a"
    by (rule narrow_le[OF hb(4)])
  have m: "(int_dom.more a Δ (int_dom.more b)) <= int_dom.more a"
    by (rule narrow_le[OF hb(5)])
  show "(a Δ b) <= a"
    unfolding narrow_int_dom_ext_def less_eq_int_dom_ext_def
    using s i p c m by simp
next
  fix a b :: "'a int_dom_scheme"
  have s: "int_sign a <= (int_sign a ∇ int_sign b)"
    by (rule widen_ge1)
  have i: "int_ivl a <= (int_ivl a ∇ int_ivl b)"
    by (rule widen_ge1)
  have p: "int_parity a <= (int_parity a ∇ int_parity b)"
    by (rule widen_ge1)
  have c: "int_congruence a <= (int_congruence a ∇ int_congruence b)"
    by (rule widen_ge1)
  have m: "int_dom.more a <= (int_dom.more a ∇ int_dom.more b)"
    by (rule widen_ge1)
  show "a <= (a ∇ b)"
    unfolding widen_int_dom_ext_def less_eq_int_dom_ext_def
    using s i p c m by simp
next
  fix a b :: "'a int_dom_scheme"
  have s: "int_sign b <= (int_sign a ∇ int_sign b)"
    by (rule widen_ge2)
  have i: "int_ivl b <= (int_ivl a ∇ int_ivl b)"
    by (rule widen_ge2)
  have p: "int_parity b <= (int_parity a ∇ int_parity b)"
    by (rule widen_ge2)
  have c: "int_congruence b <= (int_congruence a ∇ int_congruence b)"
    by (rule widen_ge2)
  have m: "int_dom.more b <= (int_dom.more a ∇ int_dom.more b)"
    by (rule widen_ge2)
  show "b <= (a ∇ b)"
    unfolding widen_int_dom_ext_def less_eq_int_dom_ext_def
    using s i p c m by simp
qed

end

section ‹Numeric domain instance›

text ‹‹numeric_domain› extends ‹executable_domain›, which includes the solver's
  ‹warrowing›, so the composite instance asks the same of the ‹more› field
  as the widening and narrowing above.›

instantiation int_dom_ext ::
  ("{bounded_lattice, warrowing}") numeric_domain
begin

definition gamma_abs_int_dom_ext [simp]:
  "numeric_domain_class.gamma (d :: 'a int_dom_scheme) = gamma_int_dom d"

definition is_empty_int_dom_ext [simp]:
  "is_empty (d :: 'a int_dom_scheme) = is_bottom_int_dom d"

definition to_string_int_dom_ext [simp]:
  "to_string (d :: 'a int_dom_scheme) = string_of_int_dom d"

instance
proof intro_classes
  show "numeric_domain_class.gamma (bot :: 'a int_dom_scheme) = {}"
    by (simp add: gamma_int_dom_def bot_int_dom_ext_def
          bot_sign_def bot_ivl_def bot_parity_def)
next
  show "numeric_domain_class.gamma (top :: 'a int_dom_scheme) = UNIV"
    by (simp add: gamma_int_dom_def top_int_dom_ext_def
          gamma_sign_top gamma_ivl_top top_ivl_def gamma_parity_top)
next
  fix a b :: "'a int_dom_scheme"
  show "a ≤ b ⟹ numeric_domain_class.gamma a ⊆ numeric_domain_class.gamma b"
    by (simp add: gamma_int_dom_mono)
next
  fix a :: "'a int_dom_scheme"
  show "is_empty a ⟷ numeric_domain_class.gamma a = {}"
    by (simp add: is_bottom_int_dom_correct)
qed

end

end