Theory Voblint_Analysis_Congruence.Congruence_Special

theory Congruence_Special
  imports Congruence_Arithmetic "Voblint_Nonrelational.Special_Ops"
begin

section ‹What a Min or Max call tells you about a residue class›

text ‹
  ‹Min a b› and ‹Max a b› each return one of their two operands, never a
  newly computed integer, so whatever describes both operands describes the
  result. Congruence answers with the join of the two argument classes: sound
  for either selection, and the sharpest answer available without knowing
  which one is taken. ‹Nondet_Int› constrains nothing and lands at ‹top›.

  The reader needs ‹aval_congruence›, Congruence's expression evaluator, from
  \<^theory>‹Voblint_Analysis_Congruence.Congruence_Arithmetic›.
›

text ‹
  Two known-even operands stay even, exactly as Parity's ‹parity_min› keeps
  ‹PEven›; a mismatch of moduli falls back on their common coarsening rather
  than on ‹top›, which is where the join earns over a constant answer.
›

definition congruence_min :: "congruence => congruence => congruence" where
  "congruence_min a b = a ⊔ b"

definition congruence_max :: "congruence => congruence => congruence" where
  "congruence_max a b = a ⊔ b"

lemma gamma_congruence_sup_ub1: "gamma_congruence a ⊆ gamma_congruence (a ⊔ b)"
proof -
  have "γ (a::congruence) ⊆ γ (a ⊔ b)" by (rule gamma_mono[OF sup_ge1])
  then show ?thesis by simp
qed

lemma gamma_congruence_sup_ub2: "gamma_congruence b ⊆ gamma_congruence (a ⊔ b)"
proof -
  have "γ (b::congruence) ⊆ γ (a ⊔ b)" by (rule gamma_mono[OF sup_ge2])
  then show ?thesis by simp
qed

lemma congruence_min_sound:
  assumes "i ∈ gamma_congruence a" and "j ∈ gamma_congruence b"
  shows "min i j ∈ gamma_congruence (congruence_min a b)"
  using assms gamma_congruence_sup_ub1[of a b] gamma_congruence_sup_ub2[of b a]
  unfolding congruence_min_def min_def by auto

lemma congruence_max_sound:
  assumes "i ∈ gamma_congruence a" and "j ∈ gamma_congruence b"
  shows "max i j ∈ gamma_congruence (congruence_max a b)"
  using assms gamma_congruence_sup_ub1[of a b] gamma_congruence_sup_ub2[of b a]
  unfolding congruence_max_def max_def by auto

lemma congruence_min_mono:
  "a1 ≤ a2 ⟹ b1 ≤ b2 ⟹ congruence_min a1 b1 ≤ congruence_min a2 (b2::congruence)"
  unfolding congruence_min_def by (rule sup_mono)

lemma congruence_max_mono:
  "a1 ≤ a2 ⟹ b1 ≤ b2 ⟹ congruence_max a1 b1 ≤ congruence_max a2 (b2::congruence)"
  unfolding congruence_max_def by (rule sup_mono)

subsection ‹Special-call dispatch›

text ‹
  ‹congruence_special_ops› pairs ‹congruence_min› and ‹congruence_max›, both the
  join of their operands. Interpreting ‹mono_minmax_ops› at this pair makes the
  generic special-call transfer sound and monotone for congruences.
›

definition congruence_special_ops :: "congruence special_ops" where
  "congruence_special_ops = (| special_min = congruence_min, special_max = congruence_max |)"

lemma congruence_special_ops_min [simp]: "special_min congruence_special_ops = congruence_min"
  by (simp add: congruence_special_ops_def)

lemma congruence_special_ops_max [simp]: "special_max congruence_special_ops = congruence_max"
  by (simp add: congruence_special_ops_def)

interpretation congruence_special: mono_minmax_ops congruence_special_ops aval_congruence
proof unfold_locales
  fix i j :: int and p q :: congruence
  assume "i ∈ γ p" and "j ∈ γ q"
  then show "min i j ∈ γ (special_min congruence_special_ops p q)"
    using congruence_min_sound by simp
next
  fix i j :: int and p q :: congruence
  assume "i ∈ γ p" and "j ∈ γ q"
  then show "max i j ∈ γ (special_max congruence_special_ops p q)"
    using congruence_max_sound by simp
next
  fix p1 p2 q1 q2 :: congruence
  assume "p1 ≤ p2" and "q1 ≤ q2"
  then show "special_min congruence_special_ops p1 q1
               ≤ special_min congruence_special_ops p2 q2"
    by (simp add: congruence_min_mono)
next
  fix p1 p2 q1 q2 :: congruence
  assume "p1 ≤ p2" and "q1 ≤ q2"
  then show "special_max congruence_special_ops p1 q1
               ≤ special_max congruence_special_ops p2 q2"
    by (simp add: congruence_max_mono)
qed

fun special_congruence ::
    "special_call => vname => (vname => congruence) => (vname => congruence)"
where
  "special_congruence Nondet_Int x d = d(x := top)"
| "special_congruence (Min a b) x d =
     d(x := congruence_min (aval_congruence a d) (aval_congruence b d))"
| "special_congruence (Max a b) x d =
     d(x := congruence_max (aval_congruence a d) (aval_congruence b d))"

lemma special_congruence_eq_transfer:
  "special_congruence sc x d = congruence_special.special_transfer sc x d"
  by (cases sc) simp_all

end