Theory Voblint_Analysis_Sign.Sign_Numeric_Queries

theory Sign_Numeric_Queries
  imports Sign_Backward
begin

section ‹Sign interpretation of the generic numeric-query interface›

text ‹
  ‹sound_numeric_queries› (\<^theory>‹Voblint_Domain.Numeric_Queries›) is
  the reusable interface; this theory supplies its Sign instance. None of the
  four query functions is a hand-built table: all four are Sign's instance of
  the generic derivations in \<^locale>‹sound_inverse_ops›'s own context ---
  ‹sign_less_true›/‹sign_less_false› read off ‹inv_less_sign›, ‹sign_eq_true›
  reads off ‹sign_less_false› in both directions, and ‹sign_eq_false› reads off
  ‹(⊓)› collapsing to ‹SBot› --- so their soundness is \<^locale>‹sound_inverse_ops›'s,
  instantiated by @{thm [source] sign_backward_domain}.
›

text ‹
  ‹sign_less_true_eq›/‹sign_less_false_eq›/‹sign_eq_true_eq›/‹sign_eq_false_eq›
  below restate each derived predicate as an explicit truth table over
  ‹inv_less_sign›/‹(⊓)›. They are the code equations of the four predicates, and
  they guard precision: a future change to
  ‹inv_less_sign›/‹inv_eq_sign›/‹(⊓)› that silently narrows or widens
  what these four predicates classify breaks one of these four proofs, at the
  seven-element lattice, rather than surfacing only as a precision regression
  in a downstream analysis.
›

subsection ‹Comparison judgments›

text ‹
  ‹sign_less_true a b› holds when every concrete pair ‹i ∈ gamma_sign a›,
  ‹j ∈ gamma_sign b› satisfies ‹i < j›; ‹sign_less_false a b› when every such
  pair satisfies ‹¬ i < j›. The two are not complements of each other:
  overlapping abstractions (e.g. ‹SNonPos› against ‹SNonNeg›) make both false,
  meaning unknown. ‹SBot› on either side makes both vacuously true.
›

definition sign_less_true :: "sign ⇒ sign ⇒ bool" where
  "sign_less_true = sound_inverse_ops.less_true inv_less_sign"

lemma sign_less_true_sound:
  assumes "sign_less_true a b" and "i ∈ gamma_sign a" and "j ∈ gamma_sign b"
  shows "i < j"
  using assms sound_inverse_ops.less_true_sound[OF
      sign_backward_domain[THEN mono_refinement.axioms(1), THEN sound_refinement.axioms(4)],
      of a b i j]
  by (simp add: sign_less_true_def)

definition sign_less_false :: "sign ⇒ sign ⇒ bool" where
  "sign_less_false = sound_inverse_ops.less_false inv_less_sign"

lemma sign_less_false_sound:
  assumes "sign_less_false a b" and "i ∈ gamma_sign a" and "j ∈ gamma_sign b"
  shows "¬ i < j"
  using assms sound_inverse_ops.less_false_sound[OF
      sign_backward_domain[THEN mono_refinement.axioms(1), THEN sound_refinement.axioms(4)],
      of a b i j]
  by (simp add: sign_less_false_def)

lemma sign_less_true_eq [code]: "sign_less_true a b ⟷
  (fst (inv_less_sign False a b) = SBot ∨ snd (inv_less_sign False a b) = SBot)"
  by (cases a; cases b;
      simp add: sign_less_true_def sound_inverse_ops.less_true_def[OF
        sign_backward_domain[THEN mono_refinement.axioms(1), THEN sound_refinement.axioms(4)]]
                bot_sign_def is_bottom_sign_def)

lemma sign_less_false_eq [code]: "sign_less_false a b ⟷
  (fst (inv_less_sign True a b) = SBot ∨ snd (inv_less_sign True a b) = SBot)"
  by (cases a; cases b;
      simp add: sign_less_false_def sound_inverse_ops.less_false_def[OF
        sign_backward_domain[THEN mono_refinement.axioms(1), THEN sound_refinement.axioms(4)]]
                bot_sign_def is_bottom_sign_def)

subsection ‹Equality judgments›

text ‹Only ‹SZero› concretizes to a singleton, so equality is provable exactly
  there; two abstractions are provably unequal exactly when their
  concretizations are disjoint. Neither table is hand-built: ‹sign_eq_true›
  is Sign's instance of the ‹eq_true› derivation off ‹less_false› in both
  directions (integer trichotomy), and ‹sign_eq_false› is Sign's instance of
  the ‹eq_false› derivation off ‹(⊓)› collapsing to ‹SBot› (disjoint
  concretizations).›

definition sign_eq_true :: "sign ⇒ sign ⇒ bool" where
  "sign_eq_true = sound_inverse_ops.eq_true inv_less_sign"

text ‹The derived definition unfolds through ‹less_false›'s global constant, so
  the code equation is stated over the Sign-level name directly.›

lemma sign_eq_true_eq [code]:
  "sign_eq_true a b ⟷ (sign_less_false a b ∧ sign_less_false b a)"
  by (simp add: sign_eq_true_def sign_less_false_def
    sound_inverse_ops.eq_true_def[OF
        sign_backward_domain[THEN mono_refinement.axioms(1), THEN sound_refinement.axioms(4)]])

lemma sign_eq_true_sound:
  assumes "sign_eq_true a b" and "i ∈ gamma_sign a" and "j ∈ gamma_sign b"
  shows "i = j"
  using assms sound_inverse_ops.eq_true_sound[OF
      sign_backward_domain[THEN mono_refinement.axioms(1), THEN sound_refinement.axioms(4)],
      of a b i j]
  by (simp add: sign_eq_true_def)

definition sign_eq_false :: "sign ⇒ sign ⇒ bool" where
  "sign_eq_false = sound_inverse_ops.eq_false inf"

lemma sign_eq_false_eq [code]: "sign_eq_false a b ⟷ a ⊓ b = SBot"
  by (cases a; cases b;
      simp add: sign_eq_false_def bot_sign_def sound_inverse_ops.eq_false_def[OF
        sign_backward_domain[THEN mono_refinement.axioms(1), THEN sound_refinement.axioms(4)]]
        is_bottom_sign_def)

lemma sign_eq_false_sound:
  assumes "sign_eq_false a b" and "i ∈ gamma_sign a" and "j ∈ gamma_sign b"
  shows "i ≠ j"
  using assms sound_inverse_ops.eq_false_sound[OF
      sign_backward_domain[THEN mono_refinement.axioms(1), THEN sound_refinement.axioms(4)],
      of a b i j]
  by (simp add: sign_eq_false_def)


subsection ‹Goblint-style optional-Boolean queries›

text ‹
  ‹sign_less›/‹sign_eq› are the generic packaging of the four judgments
  above, so one interpretation both introduces them and discharges the query
  interface. The ⬚‹defines› clause is what keeps them ordinary
  top-level constants, with the code equation the check layer needs.
›

global_interpretation sign_numeric_queries:
  numeric_query_judgments sign_less_true sign_less_false sign_eq_true sign_eq_false
  defines sign_less = sign_numeric_queries.query_less
    and sign_eq = sign_numeric_queries.query_eq
  by unfold_locales
     (auto intro: sign_less_true_sound sign_eq_true_sound
            dest: sign_less_false_sound sign_eq_false_sound)


end