Theory Voblint_Analysis_Sign.Sign_Arithmetic

theory Sign_Arithmetic
  imports Sign_Warrowing "Voblint_Nonrelational.Abstract_Arithmetic"
begin

section ‹What arithmetic does to a known sign›

text ‹
  Every operation here works on the seven-element lattice a variable's sign can
  take, from ‹SBot› (no value at all) through ‹SNeg›, ‹SNonPos›, ‹SZero›,
  ‹SNonNeg› and ‹SPos› to ‹STop› (any value). Addition and multiplication are
  given as complete tables over those seven cases; a combination the lattice
  cannot pin down --- a negative plus a positive, say --- lands on ‹STop›.

  On top of the tables sit three queries that answer about the numbers a sign
  denotes rather than about the sign itself: ‹sign_lt›, ‹sign_eqb› and
  ‹sign_tobool› return ‹Some b› when every pair of concrete values agrees on
  ‹b› and ‹None› when they do not. Each operation and query is proved sound and
  monotone, which is exactly what the shared ‹sound_arith_ops› locale
  needs; interpreting it at the end yields ‹sign_arith.aval_dom_sound› and
  ‹sign_arith.aval_dom_mono› for whole expressions.
›

instantiation sign :: plus begin
fun plus_sign :: "sign => sign => sign" where
    "plus_sign SBot    _       = SBot"
  | "plus_sign _       SBot    = SBot"
  | "plus_sign SNeg    SNeg    = SNeg"
  | "plus_sign SNeg    SNonPos = SNeg"
  | "plus_sign SNonPos SNeg    = SNeg"
  | "plus_sign SNonPos SNonPos = SNonPos"
  | "plus_sign SPos    SPos    = SPos"
  | "plus_sign SPos    SNonNeg = SPos"
  | "plus_sign SNonNeg SPos    = SPos"
  | "plus_sign SNonNeg SNonNeg = SNonNeg"
  | "plus_sign SZero   b       = b"
  | "plus_sign a       SZero   = a"
  | "plus_sign _       _       = STop"
instance ..
end

instantiation sign :: minus begin
fun minus_sign :: "sign => sign => sign" where
    "minus_sign SBot    _       = SBot"
  | "minus_sign _       SBot    = SBot"
  | "minus_sign SNeg    SPos    = SNeg"
  | "minus_sign SNeg    SNonNeg = SNeg"
  | "minus_sign SPos    SNeg    = SPos"
  | "minus_sign SPos    SNonPos = SPos"
  | "minus_sign SNeg    SZero   = SNeg"
  | "minus_sign SPos    SZero   = SPos"
  | "minus_sign SZero   SZero   = SZero"
  | "minus_sign SZero   SNeg    = SPos"
  | "minus_sign SZero   SPos    = SNeg"
  | "minus_sign SZero   SNonNeg = SNonPos"
  | "minus_sign SZero   SNonPos = SNonNeg"
  | "minus_sign SNonNeg SZero   = SNonNeg"
  | "minus_sign SNonNeg SNeg    = SPos"
  | "minus_sign SNonNeg SNonPos = SNonNeg"
  | "minus_sign SNonPos SZero   = SNonPos"
  | "minus_sign SNonPos SPos    = SNeg"
  | "minus_sign SNonPos SNonNeg = SNonPos"
  | "minus_sign _       _       = STop"
instance ..
end

instantiation sign :: times begin
fun times_sign :: "sign => sign => sign" where
    "times_sign SBot    _       = SBot"
  | "times_sign _       SBot    = SBot"
  | "times_sign SZero   _       = SZero"
  | "times_sign _       SZero   = SZero"
  | "times_sign SNeg    SNeg    = SPos"
  | "times_sign SPos    SPos    = SPos"
  | "times_sign SNeg    SPos    = SNeg"
  | "times_sign SPos    SNeg    = SNeg"
  | "times_sign SNeg    SNonPos = SNonNeg"
  | "times_sign SNonPos SNeg    = SNonNeg"
  | "times_sign SNeg    SNonNeg = SNonPos"
  | "times_sign SNonNeg SNeg    = SNonPos"
  | "times_sign SPos    SNonNeg = SNonNeg"
  | "times_sign SNonNeg SPos    = SNonNeg"
  | "times_sign SPos    SNonPos = SNonPos"
  | "times_sign SNonPos SPos    = SNonPos"
  | "times_sign SNonNeg SNonNeg = SNonNeg"
  | "times_sign SNonNeg SNonPos = SNonPos"
  | "times_sign SNonPos SNonNeg = SNonPos"
  | "times_sign SNonPos SNonPos = SNonNeg"
  | "times_sign _       _       = STop"
instance ..
end


definition sign_div :: "sign ⇒ sign ⇒ sign" where
  "sign_div a b = (if a = SBot ∨ b = SBot then SBot else (a * b) ⊔ SZero)"

definition sign_mod :: "sign ⇒ sign ⇒ sign" where
  "sign_mod a b =
    (if a = SBot ∨ b = SBot then SBot else if b = SZero then a else a ⊔ SZero)"

lemma sign_div_sound:
  assumes "i ∈ gamma_sign a" "j ∈ gamma_sign b"
  shows "c_div i j ∈ gamma_sign (sign_div a b)"
  using assms
  by (cases a; cases b; auto simp: sign_div_def sup_sign_def
      intro: c_div_nonneg c_div_nonpos)

lemma sign_mod_sound:
  assumes "i ∈ gamma_sign a" "j ∈ gamma_sign b"
  shows "c_mod i j ∈ gamma_sign (sign_mod a b)"
  using assms
  by (cases a; cases b; auto simp: sign_mod_def sup_sign_def
      intro: c_mod_nonneg c_mod_nonpos)

lemma sign_div_mono:
  "a1 ≤ a2 ⟹ b1 ≤ b2 ⟹ sign_div a1 b1 ≤ sign_div a2 b2"
  by (cases a1; cases a2; cases b1; cases b2;
      simp add: sign_div_def sup_sign_def less_eq_sign_def)

lemma sign_mod_mono:
  "a1 ≤ a2 ⟹ b1 ≤ b2 ⟹ sign_mod a1 b1 ≤ sign_mod a2 b2"
  by (cases a1; cases a2; cases b1; cases b2;
      simp add: sign_mod_def sup_sign_def less_eq_sign_def)

subsection ‹Comparison and truthiness queries›

text ‹
  ‹sign_lt›/‹sign_eqb›/‹sign_tobool› are Sign's three-valued ‹bool option›
  queries for ‹Voblint_Nonrelational.Abstract_Arithmetic›'s ‹sound_arith_ops›
  locale: ‹Some True›/‹Some False› when the two operands' sign bounds alone
  decide it, ‹None› otherwise. Every guard here is a ‹sign_le› test against a
  fixed threshold, so downward-closedness under ‹≤› (needed for
  ‹aval_dom_mono›) follows from ‹sign_le›'s own transitivity, not from any
  extra reasoning about ‹SBot›.
›

fun sign_lt :: "sign ⇒ sign ⇒ bool option" where
  "sign_lt a b =
     (if sign_le a SNeg ∧ sign_le b SNonNeg then Some True
      else if sign_le a SNonPos ∧ sign_le b SPos then Some True
      else if sign_le b SNonPos ∧ sign_le a SNonNeg then Some False
      else if sign_le b SNeg ∧ sign_le a SPos then Some False
      else None)"

fun sign_eqb :: "sign ⇒ sign ⇒ bool option" where
  "sign_eqb a b =
     (if a = SZero ∧ b = SZero then Some True
      else if (sign_le a SNeg ∧ sign_le b SNonNeg) ∨ (sign_le b SNeg ∧ sign_le a SNonNeg)
           ∨ (sign_le a SPos ∧ sign_le b SNonPos) ∨ (sign_le b SPos ∧ sign_le a SNonPos)
      then Some False
      else None)"

fun sign_tobool :: "sign ⇒ bool option" where
  "sign_tobool a =
     (if sign_le a SNeg ∨ sign_le a SPos then Some True
      else if sign_le a SZero then Some False
      else None)"

lemma sign_lt_sound:
  assumes "sign_lt a b = Some c" and "i ∈ gamma_sign a" and "j ∈ gamma_sign b"
  shows "(i < j) = c"
  using assms unfolding less_eq_sign_def[symmetric]
  by (cases a; cases b; auto split: if_splits)

lemma sign_eqb_sound:
  assumes "sign_eqb a b = Some c" and "i ∈ gamma_sign a" and "j ∈ gamma_sign b"
  shows "(i = j) = c"
  using assms unfolding less_eq_sign_def[symmetric]
  by (cases a; cases b; auto split: if_splits)

lemma sign_tobool_sound:
  assumes "sign_tobool a = Some c" and "i ∈ gamma_sign a"
  shows "(i ≠ 0) = c"
  using assms unfolding less_eq_sign_def[symmetric]
  by (cases a; auto split: if_splits)

lemma sign_le_trans_below:
  fixes a1 a2 :: sign
  assumes "sign_le a2 t" and "a1 ≤ a2"
  shows "sign_le a1 t"
  using assms sign_le_trans unfolding less_eq_sign_def
  by blast

lemma sign_lt_mono:
  assumes hp: "¬ is_empty (a1::sign)" and hq: "¬ is_empty b1"
      and hab: "a1 ≤ a2" and hbb: "b1 ≤ b2"
      and hwide: "sign_lt a2 b2 = Some c"
  shows "sign_lt a1 b1 = Some c"
proof (cases c)
  case True
  then have "sign_le a2 SNeg ∧ sign_le b2 SNonNeg ∨ sign_le a2 SNonPos ∧ sign_le b2 SPos"
    using hwide by (auto split: if_splits)
  then have "sign_le a1 SNeg ∧ sign_le b1 SNonNeg ∨ sign_le a1 SNonPos ∧ sign_le b1 SPos"
    using sign_le_trans_below[OF _ hab] sign_le_trans_below[OF _ hbb] by blast
  then show ?thesis using True by auto
next
  case False
  then have "sign_le b2 SNonPos ∧ sign_le a2 SNonNeg ∨ sign_le b2 SNeg ∧ sign_le a2 SPos"
    using hwide by (auto split: if_splits)
  then have hyp: "sign_le b1 SNonPos ∧ sign_le a1 SNonNeg ∨ sign_le b1 SNeg ∧ sign_le a1 SPos"
    using sign_le_trans_below[OF _ hab] sign_le_trans_below[OF _ hbb] by blast
  show ?thesis using hyp False hp hq unfolding is_empty_sign is_bottom_sign_def
    by (cases a1; cases b1; auto)
qed

lemma sign_eqb_mono:
  assumes hp: "¬ is_empty (a1::sign)" and hq: "¬ is_empty b1"
      and hab: "a1 ≤ a2" and hbb: "b1 ≤ b2"
      and hwide: "sign_eqb a2 b2 = Some c"
  shows "sign_eqb a1 b1 = Some c"
proof (cases c)
  case True
  then have "a2 = SZero ∧ b2 = SZero" using hwide by (auto split: if_splits)
  then have "sign_le a2 SZero" and "sign_le b2 SZero"
    unfolding less_eq_sign_def[symmetric] by simp_all
  then have hle1: "sign_le a1 SZero" and hle2: "sign_le b1 SZero"
    using sign_le_trans_below[OF _ hab] sign_le_trans_below[OF _ hbb] by blast+
  have ha1: "a1 = SBot ∨ a1 = SZero" using hle1 by (cases a1) auto
  have hb1: "b1 = SBot ∨ b1 = SZero" using hle2 by (cases b1) auto
  show ?thesis using True hp hq ha1 hb1 unfolding is_empty_sign is_bottom_sign_def by auto
next
next
  case False
  then have "sign_le a2 SNeg ∧ sign_le b2 SNonNeg ∨ sign_le b2 SNeg ∧ sign_le a2 SNonNeg
             ∨ sign_le a2 SPos ∧ sign_le b2 SNonPos ∨ sign_le b2 SPos ∧ sign_le a2 SNonPos"
    using hwide by (auto split: if_splits)
  then have "sign_le a1 SNeg ∧ sign_le b1 SNonNeg ∨ sign_le b1 SNeg ∧ sign_le a1 SNonNeg
             ∨ sign_le a1 SPos ∧ sign_le b1 SNonPos ∨ sign_le b1 SPos ∧ sign_le a1 SNonPos"
    using sign_le_trans_below[OF _ hab] sign_le_trans_below[OF _ hbb] by blast
  then show ?thesis using False by auto
qed

lemma sign_tobool_mono:
  assumes "¬ is_empty (a1::sign)" and "a1 ≤ a2" and "sign_tobool a2 = Some c"
  shows "sign_tobool a1 = Some c"
  using assms unfolding is_empty_sign is_bottom_sign_def
  by (cases a1; cases a2; auto simp: less_eq_sign_def split: if_splits)

subsection ‹Abstract expression evaluation›

text ‹
  ‹aval_sign› evaluates an expression bottom-up with the sign operations above.
  A comparison is ‹bot› when either operand is empty; otherwise it is the
  literal its three-valued query decides, or the join of ‹0› and ‹1› on
  ‹None›. These are the equations ‹sound_arith_ops› expects of an evaluator.
›

fun aval_sign :: "exp => (vname => sign) => sign" where
    "aval_sign (N n)        d = sign_of_int n"
  | "aval_sign (V x)        d = d x"
  | "aval_sign (Plus  a b)  d = aval_sign a d + aval_sign b d"
  | "aval_sign (Minus a b)  d = aval_sign a d - aval_sign b d"
  | "aval_sign (Times a b)  d = aval_sign a d * aval_sign b d"
  | "aval_sign (Div a b)  d = sign_div (aval_sign a d) (aval_sign b d)"
  | "aval_sign (Mod a b)  d = sign_mod (aval_sign a d) (aval_sign b d)"
  | "aval_sign (Less a b)   d =
       (if is_empty (aval_sign a d) ∨ is_empty (aval_sign b d) then bot
        else of_bool_option sign_of_int (sign_lt (aval_sign a d) (aval_sign b d)))"
  | "aval_sign (LessEq a b)   d =
       (if is_empty (aval_sign a d) ∨ is_empty (aval_sign b d) then bot
        else of_bool_option sign_of_int
               (map_option HOL.Not (sign_lt (aval_sign b d) (aval_sign a d))))"
  | "aval_sign (Greater a b)   d =
       (if is_empty (aval_sign a d) ∨ is_empty (aval_sign b d) then bot
        else of_bool_option sign_of_int (sign_lt (aval_sign b d) (aval_sign a d)))"
  | "aval_sign (GreaterEq a b)   d =
       (if is_empty (aval_sign a d) ∨ is_empty (aval_sign b d) then bot
        else of_bool_option sign_of_int
               (map_option HOL.Not (sign_lt (aval_sign a d) (aval_sign b d))))"
  | "aval_sign (NotEq a b) d =
       (if is_empty (aval_sign a d) ∨ is_empty (aval_sign b d) then bot
        else of_bool_option sign_of_int
               (map_option HOL.Not (sign_eqb (aval_sign a d) (aval_sign b d))))"
  | "aval_sign (exp.Eq a b) d =
       (if is_empty (aval_sign a d) ∨ is_empty (aval_sign b d) then bot
        else of_bool_option sign_of_int (sign_eqb (aval_sign a d) (aval_sign b d)))"
  | "aval_sign (exp.Not a)  d =
       (if is_empty (aval_sign a d) then bot
        else of_bool_option sign_of_int (map_option HOL.Not (sign_tobool (aval_sign a d))))"
  | "aval_sign (And a b)    d =
       (if is_empty (aval_sign a d) ∨ is_empty (aval_sign b d) then bot
        else of_bool_option sign_of_int
               (and_opt (sign_tobool (aval_sign a d)) (sign_tobool (aval_sign b d))))"
  | "aval_sign (Or a b)     d =
       (if is_empty (aval_sign a d) ∨ is_empty (aval_sign b d) then bot
        else of_bool_option sign_of_int
               (or_opt (sign_tobool (aval_sign a d)) (sign_tobool (aval_sign b d))))"

lemma sign_plus_sound:
  assumes "i ∈ gamma_sign a" "j ∈ gamma_sign b"
  shows "i + j ∈ gamma_sign (a + b)"
  using assms by (cases a; cases b; auto)

lemma sign_minus_sound:
  assumes "i ∈ gamma_sign a" "j ∈ gamma_sign b"
  shows "i - j ∈ gamma_sign (a - b)"
  using assms by (cases a; cases b; auto)

lemma sign_times_sound:
  assumes "i ∈ gamma_sign a" "j ∈ gamma_sign b"
  shows "i * j ∈ gamma_sign (a * b)"
  using assms by (cases a; cases b; auto simp: mult_neg_neg mult_neg_pos mult_pos_neg
                                                zero_le_mult_iff mult_le_0_iff)

lemma sign_plus_mono1:
  "a1 ≤ a2 ⟹ a1 + b ≤ a2 + (b::sign)"
  unfolding less_eq_sign_def
  by (cases a1; cases a2; cases b; simp)

lemma sign_plus_mono2:
  "b1 ≤ b2 ⟹ a + b1 ≤ a + (b2::sign)"
  unfolding less_eq_sign_def
  by (cases a; cases b1; cases b2; simp)

lemma sign_minus_mono1:
  "a1 ≤ a2 ⟹ a1 - b ≤ a2 - (b::sign)"
  unfolding less_eq_sign_def
  by (cases a1; cases a2; cases b; simp)

lemma sign_minus_mono2:
  "b1 ≤ b2 ⟹ a - b1 ≤ a - (b2::sign)"
  unfolding less_eq_sign_def
  by (cases a; cases b1; cases b2; simp)

lemma sign_times_mono1:
  "a1 ≤ a2 ⟹ a1 * b ≤ a2 * (b::sign)"
  unfolding less_eq_sign_def
  by (cases a1; cases a2; cases b; simp)

lemma sign_times_mono2:
  "b1 ≤ b2 ⟹ a * b1 ≤ a * (b2::sign)"
  unfolding less_eq_sign_def
  by (cases a; cases b1; cases b2; simp)

lemma sign_plus_combine_mono:
  "⟦a1 ≤ a2; b1 ≤ b2⟧ ⟹ a1 + b1 ≤ a2 + (b2::sign)"
  by (meson order.trans sign_plus_mono1 sign_plus_mono2)

lemma sign_minus_combine_mono:
  "⟦a1 ≤ a2; b1 ≤ b2⟧ ⟹ a1 - b1 ≤ a2 - (b2::sign)"
  by (meson order.trans sign_minus_mono1 sign_minus_mono2)

lemma sign_times_combine_mono:
  "⟦a1 ≤ a2; b1 ≤ b2⟧ ⟹ a1 * b1 ≤ a2 * (b2::sign)"
  by (meson order.trans sign_times_mono1 sign_times_mono2)

interpretation sign_arith: mono_arith_ops
    aval_sign sign_of_int "(+)" "(-)" "(*)" sign_div sign_mod sign_lt sign_eqb sign_tobool
  apply unfold_locales
  apply (simp_all add: sign_of_int_gamma sign_plus_sound sign_minus_sound sign_times_sound
    sign_div_sound sign_mod_sound
                        sign_plus_combine_mono sign_minus_combine_mono sign_times_combine_mono
                          sign_div_mono sign_mod_mono
                        sign_lt_sound sign_eqb_sound sign_tobool_sound[unfolded truthy_def]
                        sup_sign_def
                    del: sign_lt.simps sign_eqb.simps sign_tobool.simps)
  apply (blast intro: sign_lt_mono[unfolded is_empty_sign] sign_eqb_mono[unfolded is_empty_sign]
                      sign_tobool_mono[unfolded is_empty_sign])+
  done


end