Theory Abstract_Arithmetic

theory Abstract_Arithmetic
  imports
    "Voblint_Domain.Three_Valued" "Voblint_Domain.Forward_Domain"
    "Voblint_Domain.Numeric_Queries"
    "Voblint_Domain.Nonrelational_State"
begin

section ‹Generic expression soundness›

text ‹
  Sign, Interval, Parity, and Congruence each prove an ‹aval_<dom>_sound› lemma with the
  identical shape and proof script: structural induction on ‹exp›, discharged
  by the same per-operator soundness facts. Arithmetic
  (‹plus_sound›/‹minus_sound›/‹times_sound›) and comparison/truthiness
  (‹lt›/‹eqb›/‹tobool›) are genuinely domain-specific -- each domain's own
  case-split proof over its own representation -- so this locale does not try
  to share those. What it shares is the one induction that combines them,
  mirroring Goblint's ‹base.ml› expression evaluator: ‹Base› only ever calls
  ‹ID.add›/‹ID.lt›/‹ID.to_bool› and never recomputes a comparison's
  precision itself, so ‹ev› here only ever calls ‹lt›/‹eqb›/‹tobool› and
  never recomputes what a domain already knows about its own relation.

  ‹ev›, ‹lit›, ‹lt›, ‹eqb›, and ‹tobool› are locale parameters, not derived:
  interpreting this locale at a domain's own ‹aval_<dom>›, literal-embedding
  function, and comparison/truthiness queries keeps every existing call site
  of ‹aval_<dom>› untouched -- the shared ‹aval_dom_sound› lemma below is
  stated over the same externally-fixed functions, not a locale-internal
  reconstruction of them.
›

text ‹
  A comparison or logical result is always the concrete C truthiness value
  ‹0›/‹1›. Goblint's integer domains move between the two readings with
  ‹of_bool› and ‹to_bool›; here the three-valued answer of a query is read back
  as a value by ‹of_bool_option›: ‹Some True› is ‹lit 1›, ‹Some False›
  is ‹lit 0›, and an unknown answer joins both --- exactly Goblint's
  ‹id_binary_pred›/‹id_unary_log›/‹id_binary_log› pattern. A negated relation
  negates the query answer, and ‹And›/‹Or› combine their operands' truthiness
  with \<^const>‹and_opt›/\<^const>‹or_opt›, which settle on one definite annihilating
  operand, mirroring ‹id_binary_log›'s own short-circuit.

  Each operand is queried through ‹lt›/‹eqb›/‹tobool› only when it is not
  itself ‹is_empty›: an ‹is_empty› operand denotes an unreachable value (its
  concretization is empty), so the whole comparison collapses to ‹bot› rather
  than querying a value with no witness to reason about. This guard is not
  optional bookkeeping -- ‹bot› is every domain's own least element, so a
  comparison against it can widen to conflicting query answers as the
  ∗‹other› operand widens; routing it through ‹bot› directly, before ‹lt›/
  ‹eqb›/‹tobool› ever see it, is what keeps ‹aval_dom_mono› provable without
  demanding an impossible monotonicity obligation from those queries at their
  own domain's bottom.
›

fun of_bool_option :: "(int ⇒ 'a::sup) ⇒ bool option ⇒ 'a" where
  "of_bool_option lit (Some b) = lit (if b then 1 else 0)"
| "of_bool_option lit None = lit 0 ⊔ lit 1"

text ‹
  ‹sound_arith_ops› pins an evaluator ‹ev› down by its equations: arithmetic
  through the supplied operations, comparisons through ‹lt›/‹eqb› and
  ‹of_bool_option› behind the emptiness guard. Given sound operations and queries,
  the locale proves the evaluator sound.
›

locale sound_arith_ops =
  sound_truth_test tobool + sound_numeric_queries lt eqb
  for ev :: "exp ⇒ (vname ⇒ 'a::numeric_domain) ⇒ 'a" ("⟦_⟧⇧♯")
    and lit :: "int ⇒ 'a"
    and pls :: "'a ⇒ 'a ⇒ 'a"
    and mns :: "'a ⇒ 'a ⇒ 'a"
    and tms :: "'a ⇒ 'a ⇒ 'a"
    and dvs :: "'a ⇒ 'a ⇒ 'a"
    and rem :: "'a ⇒ 'a ⇒ 'a"
    and lt :: "'a ⇒ 'a ⇒ bool option"
    and eqb :: "'a ⇒ 'a ⇒ bool option"
    and tobool :: "'a ⇒ bool option" +
  assumes ev_N[simp]: "⟦N n⟧⇧♯ sigma = lit n"
    and ev_V[simp]: "⟦V x⟧⇧♯ sigma = sigma x"
    and ev_Plus[simp]: "⟦Plus e1 e2⟧⇧♯ sigma = pls (⟦e1⟧⇧♯ sigma) (⟦e2⟧⇧♯ sigma)"
    and ev_Minus[simp]: "⟦Minus e1 e2⟧⇧♯ sigma = mns (⟦e1⟧⇧♯ sigma) (⟦e2⟧⇧♯ sigma)"
    and ev_Times[simp]: "⟦Times e1 e2⟧⇧♯ sigma = tms (⟦e1⟧⇧♯ sigma) (⟦e2⟧⇧♯ sigma)"
    and ev_Div[simp]: "⟦Div e1 e2⟧⇧♯ sigma = dvs (⟦e1⟧⇧♯ sigma) (⟦e2⟧⇧♯ sigma)"
    and ev_Mod[simp]: "⟦Mod e1 e2⟧⇧♯ sigma = rem (⟦e1⟧⇧♯ sigma) (⟦e2⟧⇧♯ sigma)"
    and ev_Less[simp]: "⟦Less e1 e2⟧⇧♯ sigma =
         (if is_empty (⟦e1⟧⇧♯ sigma) ∨ is_empty (⟦e2⟧⇧♯ sigma) then bot
          else of_bool_option lit (lt (⟦e1⟧⇧♯ sigma) (⟦e2⟧⇧♯ sigma)))"
    and ev_LessEq[simp]: "⟦LessEq e1 e2⟧⇧♯ sigma =
         (if is_empty (⟦e1⟧⇧♯ sigma) ∨ is_empty (⟦e2⟧⇧♯ sigma) then bot
          else of_bool_option lit (map_option HOL.Not (lt (⟦e2⟧⇧♯ sigma) (⟦e1⟧⇧♯ sigma))))"
    and ev_Greater[simp]: "⟦Greater e1 e2⟧⇧♯ sigma =
         (if is_empty (⟦e1⟧⇧♯ sigma) ∨ is_empty (⟦e2⟧⇧♯ sigma) then bot
          else of_bool_option lit (lt (⟦e2⟧⇧♯ sigma) (⟦e1⟧⇧♯ sigma)))"
    and ev_GreaterEq[simp]: "⟦GreaterEq e1 e2⟧⇧♯ sigma =
         (if is_empty (⟦e1⟧⇧♯ sigma) ∨ is_empty (⟦e2⟧⇧♯ sigma) then bot
          else of_bool_option lit (map_option HOL.Not (lt (⟦e1⟧⇧♯ sigma) (⟦e2⟧⇧♯ sigma))))"
    and ev_NotEq[simp]: "⟦NotEq e1 e2⟧⇧♯ sigma =
         (if is_empty (⟦e1⟧⇧♯ sigma) ∨ is_empty (⟦e2⟧⇧♯ sigma) then bot
          else of_bool_option lit (map_option HOL.Not (eqb (⟦e1⟧⇧♯ sigma) (⟦e2⟧⇧♯ sigma))))"
    and ev_Eq[simp]: "⟦exp.Eq e1 e2⟧⇧♯ sigma =
         (if is_empty (⟦e1⟧⇧♯ sigma) ∨ is_empty (⟦e2⟧⇧♯ sigma) then bot
          else of_bool_option lit (eqb (⟦e1⟧⇧♯ sigma) (⟦e2⟧⇧♯ sigma)))"
    and ev_Not[simp]: "⟦exp.Not e⟧⇧♯ sigma =
         (if is_empty (⟦e⟧⇧♯ sigma) then bot
          else of_bool_option lit (map_option HOL.Not (tobool (⟦e⟧⇧♯ sigma))))"
    and ev_And[simp]: "⟦And e1 e2⟧⇧♯ sigma =
         (if is_empty (⟦e1⟧⇧♯ sigma) ∨ is_empty (⟦e2⟧⇧♯ sigma) then bot
          else of_bool_option lit (and_opt (tobool (⟦e1⟧⇧♯ sigma)) (tobool (⟦e2⟧⇧♯ sigma))))"
    and ev_Or[simp]: "⟦Or e1 e2⟧⇧♯ sigma =
         (if is_empty (⟦e1⟧⇧♯ sigma) ∨ is_empty (⟦e2⟧⇧♯ sigma) then bot
          else of_bool_option lit (or_opt (tobool (⟦e1⟧⇧♯ sigma)) (tobool (⟦e2⟧⇧♯ sigma))))"
    and lit_sound[simp]: "n ∈ γ (lit n)"
    and plus_sound[intro]:
      "i ∈ γ (p::'a) ⟹ j ∈ γ q ⟹ i + j ∈ γ (pls p q)"
    and minus_sound[intro]:
      "i ∈ γ (p::'a) ⟹ j ∈ γ q ⟹ i - j ∈ γ (mns p q)"
    and times_sound[intro]:
      "i ∈ γ (p::'a) ⟹ j ∈ γ q ⟹ i * j ∈ γ (tms p q)"
    and div_sound[intro]:
      "i ∈ γ (p::'a) ⟹ j ∈ γ q ⟹ c_div i j ∈ γ (dvs p q)"
    and mod_sound[intro]:
      "i ∈ γ (p::'a) ⟹ j ∈ γ q ⟹ c_mod i j ∈ γ (rem p q)"
begin

text ‹
  Every comparison and connective reads its query answer back through
  \<^const>‹of_bool_option› behind the same emptiness guard. ‹of_bool_option_sound›
  and ‹of_bool_option_mono› discharge that shape once, so each induction case
  supplies only its own query facts.
›

lemma of_bool_option_sound:
  assumes "¬ E" and "⋀b. r = Some b ⟹ v = (if b then 1 else 0)" and "v ∈ {0, 1}"
  shows "v ∈ γ (if E then bot else of_bool_option lit r)"
  using assms
  by (cases r) (auto intro: gamma_sup_ub1[THEN subsetD] gamma_sup_ub2[THEN subsetD])

lemma aval_dom_sound:
  "s ∈ γ sigma ⟹ ⟦a⟧⇩e s ∈ γ (⟦a⟧⇧♯ sigma)"
proof (induction a arbitrary: s sigma)
  case (Less e1 e2)
  have h1: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ sigma)" and h2: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ sigma)"
    using Less by simp_all
  show ?case unfolding ev_Less aval.simps
    by (rule of_bool_option_sound) (use h1 h2 is_empty_correct less_sound[OF _ h1 h2] in auto)
next
  case (LessEq e1 e2)
  have h1: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ sigma)" and h2: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ sigma)"
    using LessEq by simp_all
  show ?case unfolding ev_LessEq aval.simps
    by (rule of_bool_option_sound) (use h1 h2 is_empty_correct less_sound[OF _ h2 h1] in auto)
next
  case (Greater e1 e2)
  have h1: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ sigma)" and h2: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ sigma)"
    using Greater by simp_all
  show ?case unfolding ev_Greater aval.simps
    by (rule of_bool_option_sound) (use h1 h2 is_empty_correct less_sound[OF _ h2 h1] in auto)
next
  case (GreaterEq e1 e2)
  have h1: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ sigma)" and h2: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ sigma)"
    using GreaterEq by simp_all
  show ?case unfolding ev_GreaterEq aval.simps
    by (rule of_bool_option_sound) (use h1 h2 is_empty_correct less_sound[OF _ h1 h2] in auto)
next
  case (NotEq e1 e2)
  have h1: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ sigma)" and h2: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ sigma)"
    using NotEq by simp_all
  show ?case unfolding ev_NotEq aval.simps
    by (rule of_bool_option_sound) (use h1 h2 is_empty_correct eq_sound[OF _ h1 h2] in auto)
next
  case (Eq e1 e2)
  have h1: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ sigma)" and h2: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ sigma)"
    using Eq by simp_all
  show ?case unfolding ev_Eq aval.simps
    by (rule of_bool_option_sound) (use h1 h2 is_empty_correct eq_sound[OF _ h1 h2] in auto)
next
  case (Not e)
  have h: "⟦e⟧⇩e s ∈ γ (⟦e⟧⇧♯ sigma)" using Not by simp
  show ?case unfolding ev_Not aval.simps
    by (rule of_bool_option_sound) (use h is_empty_correct tobool_sound[OF _ h] in auto)
next
  case (And e1 e2)
  have h1: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ sigma)" and h2: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ sigma)"
    using And by simp_all
  show ?case unfolding ev_And aval.simps
    by (rule of_bool_option_sound)
       (use h1 h2 is_empty_correct
          and_opt_sound[OF _ tobool_sound[OF _ h1] tobool_sound[OF _ h2]] in auto)
next
  case (Or e1 e2)
  have h1: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ sigma)" and h2: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ sigma)"
    using Or by simp_all
  show ?case unfolding ev_Or aval.simps
    by (rule of_bool_option_sound)
       (use h1 h2 is_empty_correct
          or_opt_sound[OF _ tobool_sound[OF _ h1] tobool_sound[OF _ h2]] in auto)
qed (auto dest: gamma_stateD)

end

text ‹
  The expression domain extends the truth test and the numeric queries, whose laws it
  assumes, and derives its evaluator's soundness by induction.  An interpretation of
  \<^locale>‹sound_arith_ops› therefore registers the whole forward interface
  once, and a later ‹sound_refinement›, ‹sound_minmax_ops› or check-layer
  interpretation over the same operations does not ask for these laws again.
›

sublocale sound_arith_ops ⊆ sound_evaluator gamma_state ev
  by unfold_locales (rule aval_dom_sound)

text ‹
  Monotonicity needs strictly more than soundness does, and one domain can
  supply the first without the second: the composite integer domain's
  arithmetic is monotone only away from ‹Refine_Fixpoint›, while its soundness
  holds at every refinement mode. Splitting the two apart is what lets that
  domain interpret the shared induction twice --- unconditionally for
  ‹aval_dom_sound›, under its mode side condition for ‹aval_dom_mono› --- rather
  than repeat both proofs by hand.
›

locale mono_arith_ops = sound_arith_ops + mono_truth_test tobool +
  assumes plus_mono[intro]:
      "p1 ≤ p2 ⟹ q1 ≤ q2 ⟹ pls p1 q1 ≤ pls p2 q2"
    and minus_mono[intro]:
      "p1 ≤ p2 ⟹ q1 ≤ q2 ⟹ mns p1 q1 ≤ mns p2 q2"
    and times_mono[intro]:
      "p1 ≤ p2 ⟹ q1 ≤ q2 ⟹ tms p1 q1 ≤ tms p2 q2"
    and div_mono[intro]:
      "p1 ≤ p2 ⟹ q1 ≤ q2 ⟹ dvs p1 q1 ≤ dvs p2 q2"
    and mod_mono[intro]:
      "p1 ≤ p2 ⟹ q1 ≤ q2 ⟹ rem p1 q1 ≤ rem p2 q2"
    and lt_mono:
      "¬ is_empty p1 ⟹ ¬ is_empty q1 ⟹ p1 ≤ p2 ⟹ q1 ≤ q2 ⟹
       lt p2 q2 = Some b ⟹ lt p1 q1 = Some b"
    and eqb_mono:
      "¬ is_empty p1 ⟹ ¬ is_empty q1 ⟹ p1 ≤ p2 ⟹ q1 ≤ q2 ⟹
       eqb p2 q2 = Some b ⟹ eqb p1 q1 = Some b"
begin

lemma of_bool_option_mono:
  assumes "E2 ⟹ E1" and "⋀b. ¬ E1 ⟹ r2 = Some b ⟹ r1 = Some b"
  shows "(if E1 then bot else of_bool_option lit r1) ≤ (if E2 then bot else of_bool_option lit r2)"
  using assms by (cases r1; cases r2) auto

lemma aval_dom_mono:
  "sigma1 ≤ sigma2 ⟹ ⟦a⟧⇧♯ sigma1 ≤ ⟦a⟧⇧♯ sigma2"
proof (induction a arbitrary: sigma1 sigma2)
  case (Less e1 e2)
  have p: "⟦e1⟧⇧♯ sigma1 ≤ ⟦e1⟧⇧♯ sigma2" and q: "⟦e2⟧⇧♯ sigma1 ≤ ⟦e2⟧⇧♯ sigma2"
    using Less by simp_all
  show ?case unfolding ev_Less
    by (rule of_bool_option_mono)
       (use is_empty_antimono[OF p] is_empty_antimono[OF q] lt_mono[OF _ _ p q] in auto)
next
  case (LessEq e1 e2)
  have p: "⟦e1⟧⇧♯ sigma1 ≤ ⟦e1⟧⇧♯ sigma2" and q: "⟦e2⟧⇧♯ sigma1 ≤ ⟦e2⟧⇧♯ sigma2"
    using LessEq by simp_all
  show ?case unfolding ev_LessEq
    by (rule of_bool_option_mono)
       (use is_empty_antimono[OF p] is_empty_antimono[OF q] lt_mono[OF _ _ q p] in auto)
next
  case (Greater e1 e2)
  have p: "⟦e1⟧⇧♯ sigma1 ≤ ⟦e1⟧⇧♯ sigma2" and q: "⟦e2⟧⇧♯ sigma1 ≤ ⟦e2⟧⇧♯ sigma2"
    using Greater by simp_all
  show ?case unfolding ev_Greater
    by (rule of_bool_option_mono)
       (use is_empty_antimono[OF p] is_empty_antimono[OF q] lt_mono[OF _ _ q p] in auto)
next
  case (GreaterEq e1 e2)
  have p: "⟦e1⟧⇧♯ sigma1 ≤ ⟦e1⟧⇧♯ sigma2" and q: "⟦e2⟧⇧♯ sigma1 ≤ ⟦e2⟧⇧♯ sigma2"
    using GreaterEq by simp_all
  show ?case unfolding ev_GreaterEq
    by (rule of_bool_option_mono)
       (use is_empty_antimono[OF p] is_empty_antimono[OF q] lt_mono[OF _ _ p q] in auto)
next
  case (NotEq e1 e2)
  have p: "⟦e1⟧⇧♯ sigma1 ≤ ⟦e1⟧⇧♯ sigma2" and q: "⟦e2⟧⇧♯ sigma1 ≤ ⟦e2⟧⇧♯ sigma2"
    using NotEq by simp_all
  show ?case unfolding ev_NotEq
    by (rule of_bool_option_mono)
       (use is_empty_antimono[OF p] is_empty_antimono[OF q] eqb_mono[OF _ _ p q] in auto)
next
  case (Eq e1 e2)
  have p: "⟦e1⟧⇧♯ sigma1 ≤ ⟦e1⟧⇧♯ sigma2" and q: "⟦e2⟧⇧♯ sigma1 ≤ ⟦e2⟧⇧♯ sigma2"
    using Eq by simp_all
  show ?case unfolding ev_Eq
    by (rule of_bool_option_mono)
       (use is_empty_antimono[OF p] is_empty_antimono[OF q] eqb_mono[OF _ _ p q] in auto)
next
  case (Not e)
  have p: "⟦e⟧⇧♯ sigma1 ≤ ⟦e⟧⇧♯ sigma2" using Not by simp
  show ?case unfolding ev_Not
    by (rule of_bool_option_mono) (use is_empty_antimono[OF p] tobool_mono[OF _ p] in auto)
next
  case (And e1 e2)
  have p: "⟦e1⟧⇧♯ sigma1 ≤ ⟦e1⟧⇧♯ sigma2" and q: "⟦e2⟧⇧♯ sigma1 ≤ ⟦e2⟧⇧♯ sigma2"
    using And by simp_all
  show ?case unfolding ev_And
    by (rule of_bool_option_mono)
       (use is_empty_antimono[OF p] is_empty_antimono[OF q]
          and_opt_mono[OF tobool_mono[OF _ p] tobool_mono[OF _ q]] in auto)
next
  case (Or e1 e2)
  have p: "⟦e1⟧⇧♯ sigma1 ≤ ⟦e1⟧⇧♯ sigma2" and q: "⟦e2⟧⇧♯ sigma1 ≤ ⟦e2⟧⇧♯ sigma2"
    using Or by simp_all
  show ?case unfolding ev_Or
    by (rule of_bool_option_mono)
       (use is_empty_antimono[OF p] is_empty_antimono[OF q]
          or_opt_mono[OF tobool_mono[OF _ p] tobool_mono[OF _ q]] in auto)
qed (auto simp add: le_funD)

end

sublocale mono_arith_ops ⊆ mono_evaluator gamma_state ev
  by unfold_locales (rule aval_dom_mono)

end