Theory Voblint_Nonrelational.Special_Ops

theory Special_Ops
  imports "Voblint_Framework.Transfer_Algebra" "Voblint_Domain.Forward_Domain"
begin

section ‹Generic special-call dispatch›

text ‹
  Every domain's ‹Nondet_Int›/‹Min›/‹Max› dispatch (‹special_sign›,
  ‹special_ivl›, ‹special_parity›, ...) has the same shape: havoc to ‹top› for
  ‹Nondet_Int›, or apply a two-argument primitive to the evaluated operands for
  ‹Min›/‹Max›. This theory proves that shape's soundness and monotonicity once,
  against an abstract pair of primitives (‹special_min›/‹special_max›) and an
  abstract expression evaluator, so each domain only has to supply its own
  minimum and maximum primitives and their soundness/monotonicity facts -- the
  case-split dispatch and its proof are not repeated per domain.

  ‹special_min›/‹special_max› are bundled as a record rather than as two bare
  locale parameters so a concrete instance (e.g. ‹sign_special_ops›) is a
  first-class value, not just a locale interpretation.
›

record 'a special_ops =
  special_min :: "'a => 'a => 'a"
  special_max :: "'a => 'a => 'a"

text ‹
  ‹sound_minmax_ops› asks for a sound evaluator and primitives whose results contain
  ‹min›/‹max› of any two described integers.
›

locale sound_minmax_ops = sound_evaluator gamma_state ev
  for ops :: "'a::numeric_domain special_ops"
    and ev  :: "exp => 'a abs_state => 'a" ("⟦_⟧⇧♯") +
  assumes special_min_sound[intro]:
    "i ∈ γ p ⟹ j ∈ γ q ⟹ min i j ∈ γ (special_min ops p q)"
  assumes special_max_sound[intro]:
    "i ∈ γ p ⟹ j ∈ γ q ⟹ max i j ∈ γ (special_max ops p q)"

text ‹
  Monotonicity is a separate layer, as for the evaluator and the backward
  operations: soundness of the special calls needs none of it.
›

locale mono_minmax_ops = sound_minmax_ops + mono_evaluator gamma_state ev +
  assumes special_min_mono[intro]:
    "p1 ≤ p2 ⟹ q1 ≤ q2 ⟹ special_min ops p1 q1 ≤ special_min ops p2 q2"
  assumes special_max_mono[intro]:
    "p1 ≤ p2 ⟹ q1 ≤ q2 ⟹ special_max ops p1 q1 ≤ special_max ops p2 q2"

context sound_minmax_ops
begin

definition special_transfer ::
    "special_call => vname => (vname => 'a) => (vname => 'a)"
where
  "special_transfer sc x d =
     d(x := (case sc of
                Nondet_Int => top
              | Min a b => special_min ops (⟦a⟧⇧♯ d) (⟦b⟧⇧♯ d)
              | Max a b => special_max ops (⟦a⟧⇧♯ d) (⟦b⟧⇧♯ d)))"

lemma special_transfer_Nondet_Int [simp]:
  "special_transfer Nondet_Int x d = d(x := top)"
  unfolding special_transfer_def by simp

lemma special_transfer_Min [simp]:
  "special_transfer (Min a b) x d = d(x := special_min ops (⟦a⟧⇧♯ d) (⟦b⟧⇧♯ d))"
  unfolding special_transfer_def by simp

lemma special_transfer_Max [simp]:
  "special_transfer (Max a b) x d = d(x := special_max ops (⟦a⟧⇧♯ d) (⟦b⟧⇧♯ d))"
  unfolding special_transfer_def by simp

text ‹
  Each dispatch case writes one variable, so the whole proof is
  \<^theory>‹Voblint_Framework.Transfer_Algebra›'s ‹gamma_state_upd› --- a sound state
  updated at ‹x› with a value sound for the new abstract element stays sound --- once
  the case supplies that the written value is in the concretization. Only the three
  ‹v ∈ gamma _› obligations are special-call specific; the per-variable reasoning is
  entirely ‹gamma_state_upd›'s.
›

lemma special_transfer_sound:
  assumes 𝒢: "s ∈ γ d" and sr: "special_result sc s v"
  shows "s(x := v) ∈ γ (special_transfer sc x d)"
proof -
  show ?thesis
  proof (cases sc)
    case Nondet_Int
    with sr 𝒢 show ?thesis by auto
  next
    case (Min a b)
    with sr have "v = min (⟦a⟧⇩e s) (⟦b⟧⇩e s)" by simp
    moreover from 𝒢 have "⟦a⟧⇩e s ∈ γ (⟦a⟧⇧♯ d)" and "⟦b⟧⇩e s ∈ γ (⟦b⟧⇧♯ d)"
      by (rule aval_abs_sound)+
    ultimately show ?thesis using Min 𝒢 by auto
  next
    case (Max a b)
    with sr have "v = max (⟦a⟧⇩e s) (⟦b⟧⇩e s)" by simp
    moreover from 𝒢 have "⟦a⟧⇩e s ∈ γ (⟦a⟧⇧♯ d)" and "⟦b⟧⇩e s ∈ γ (⟦b⟧⇧♯ d)"
      by (rule aval_abs_sound)+
    ultimately show ?thesis using Max 𝒢 by auto
  qed
qed

end

context mono_minmax_ops
begin

lemma special_transfer_mono:
  assumes le: "sigma1 ≤ sigma2"
  shows "special_transfer sc x sigma1 ≤ special_transfer sc x sigma2"
proof (cases sc)
  case Nondet_Int
  with le show ?thesis by (simp add: le_funD le_funI)
next
  case (Min a b)
  have "special_min ops (⟦a⟧⇧♯ sigma1) (⟦b⟧⇧♯ sigma1)
          ≤ special_min ops (⟦a⟧⇧♯ sigma2) (⟦b⟧⇧♯ sigma2)"
    using le by (intro special_min_mono aval_abs_mono)
  with le Min show ?thesis unfolding le_fun_def by auto
next
  case (Max a b)
  have "special_max ops (⟦a⟧⇧♯ sigma1) (⟦b⟧⇧♯ sigma1)
          ≤ special_max ops (⟦a⟧⇧♯ sigma2) (⟦b⟧⇧♯ sigma2)"
    using le by (intro special_max_mono aval_abs_mono)
  with le Max show ?thesis unfolding le_fun_def by auto
qed

end

end