Theory Voblint_Analysis_Parity.Parity_Special

theory Parity_Special
  imports Parity_Domain "Voblint_Nonrelational.Special_Ops"
begin

section ‹Parity: special-call semantics›

text ‹
  ‹parity_min›/‹parity_max› exist solely as the abstract implementation of the
  ‹Min›/‹Max› special calls; see the analogous note on Sign's ‹sign_min›/
  ‹sign_max›. Unlike Sign and Interval, parity's result is not simply "top
  unless we're being lazy": ‹min x y› and ‹max x y› both evaluate to exactly
  one of their two arguments, never a newly synthesized value, so when both
  arguments share a known parity the result provably shares it too --
  ‹parity_min PEven PEven = PEven›, not ‹PTop›. Only a parity mismatch (or an
  unknown operand) loses the information, because then either argument could
  be the one selected.
›

fun parity_min :: "parity => parity => parity" where
    "parity_min PBot _        = PBot"
  | "parity_min _    PBot     = PBot"
  | "parity_min PEven PEven   = PEven"
  | "parity_min POdd  POdd    = POdd"
  | "parity_min _    _        = PTop"

fun parity_max :: "parity => parity => parity" where
    "parity_max PBot _        = PBot"
  | "parity_max _    PBot     = PBot"
  | "parity_max PEven PEven   = PEven"
  | "parity_max POdd  POdd    = POdd"
  | "parity_max _    _        = PTop"

lemma parity_min_sound:
  assumes "i ∈ gamma_parity a" "j ∈ gamma_parity b"
  shows "min i j ∈ gamma_parity (parity_min a b)"
  using assms by (cases a; cases b; auto simp: min_def)

lemma parity_max_sound:
  assumes "i ∈ gamma_parity a" "j ∈ gamma_parity b"
  shows "max i j ∈ gamma_parity (parity_max a b)"
  using assms by (cases a; cases b; auto simp: max_def)

lemma parity_min_mono1:
  "a1 ≤ a2 ⟹ parity_min a1 b ≤ parity_min a2 (b::parity)"
  unfolding less_eq_parity_def
  by (cases a1; cases a2; cases b; simp)

lemma parity_min_mono2:
  "b1 ≤ b2 ⟹ parity_min a b1 ≤ parity_min a (b2::parity)"
  unfolding less_eq_parity_def
  by (cases a; cases b1; cases b2; simp)

lemma parity_min_combine_mono:
  "⟦a1 ≤ a2; b1 ≤ b2⟧ ⟹ parity_min a1 b1 ≤ parity_min a2 (b2::parity)"
  by (meson order.trans parity_min_mono1 parity_min_mono2)

lemma parity_max_mono1:
  "a1 ≤ a2 ⟹ parity_max a1 b ≤ parity_max a2 (b::parity)"
  unfolding less_eq_parity_def
  by (cases a1; cases a2; cases b; simp)

lemma parity_max_mono2:
  "b1 ≤ b2 ⟹ parity_max a b1 ≤ parity_max a (b2::parity)"
  unfolding less_eq_parity_def
  by (cases a; cases b1; cases b2; simp)

lemma parity_max_combine_mono:
  "⟦a1 ≤ a2; b1 ≤ b2⟧ ⟹ parity_max a1 b1 ≤ parity_max a2 (b2::parity)"
  by (meson order.trans parity_max_mono1 parity_max_mono2)

subsection ‹Special-call dispatch›

text ‹
  ‹special_parity› havocs on ‹Nondet_Int› and applies ‹parity_min›/‹parity_max›
  otherwise. ‹special_parity_eq_transfer› shows it equals the generic transfer of
  the ‹mono_minmax_ops› interpretation at ‹parity_special_ops›.
›

fun special_parity ::
    "special_call => vname => (vname => parity) => (vname => parity)"
where
  "special_parity Nondet_Int x d = d(x := PTop)"
| "special_parity (Min a b) x d = d(x := parity_min (aval_parity a d) (aval_parity b d))"
| "special_parity (Max a b) x d = d(x := parity_max (aval_parity a d) (aval_parity b d))"

definition parity_special_ops :: "parity special_ops" where
  "parity_special_ops = (| special_min = parity_min, special_max = parity_max |)"

interpretation parity_special: mono_minmax_ops parity_special_ops aval_parity
  by unfold_locales
     (auto simp: parity_special_ops_def gamma_parity_top
           intro: parity_min_sound parity_max_sound parity_min_combine_mono parity_max_combine_mono)

lemma parity_special_ops_min [simp]: "special_min parity_special_ops = parity_min"
  by (simp add: parity_special_ops_def)

lemma parity_special_ops_max [simp]: "special_max parity_special_ops = parity_max"
  by (simp add: parity_special_ops_def)

lemma special_parity_eq_transfer:
  "special_parity sc x d = parity_special.special_transfer sc x d"
  by (cases sc) (simp_all add: top_parity_def)

end