Theory Parity_Numeric_Queries

theory Parity_Numeric_Queries
  imports Parity_Domain
begin

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

text ‹
  Third-domain validation for ‹sound_numeric_queries›
  (\<^theory>‹Voblint_Domain.Numeric_Queries›), hand-tuned like
  ‹Voblint_Analysis_Interval.Interval_Numeric_Queries› rather than derived through
  ‹sound_refinement›: parity has no ‹inv_less› instance (guards do not
  refine parity), so there is nothing for
  the generic derivations to read off. Parity carries no order information at
  all, so ‹parity_less_true›/‹parity_less_false› are provable only in the
  vacuous case (one side ‹PBot›); every genuine pair is unknown. ‹PBot› is the
  lattice's unique empty representative (unlike Interval's raw ‹ivl› type,
  which has infinitely many non-canonical empty representations), so the
  vacuous case is a single clean equality test, as for Sign's ‹SBot›.
›

subsection ‹Comparison judgments: vacuous only›

text ‹
  ‹parity_less_true a b›/‹parity_less_false a b› both hold exactly when one
  side concretizes to nothing: neither judgment can ever be established from
  parity alone, since knowing a value's evenness says nothing about its order
  against another value's evenness. The two coincide definitionally --- both
  are the same vacuity test --- which is itself the content of the "usually
  unknown" fact about Parity's order queries.
›

definition parity_vacuous :: "parity ⇒ parity ⇒ bool" where
  "parity_vacuous a b ⟷ (a = PBot ∨ b = PBot)"

definition parity_less_true :: "parity ⇒ parity ⇒ bool" where
  "parity_less_true = parity_vacuous"

definition parity_less_false :: "parity ⇒ parity ⇒ bool" where
  "parity_less_false = parity_vacuous"

lemma parity_less_true_sound:
  assumes "parity_less_true a b" and "i ∈ gamma_parity a" and "j ∈ gamma_parity b"
  shows "i < j"
  using assms unfolding parity_less_true_def parity_vacuous_def by (cases a; cases b; auto)

lemma parity_less_false_sound:
  assumes "parity_less_false a b" and "i ∈ gamma_parity a" and "j ∈ gamma_parity b"
  shows "¬ i < j"
  using assms unfolding parity_less_false_def parity_vacuous_def by (cases a; cases b; auto)

subsection ‹Equality judgments›

text ‹
  ‹parity_eq_true› is vacuous-only for the same reason as the order queries:
  no parity class concretizes to a singleton (unlike Sign's ‹SZero› or an
  Interval point interval), so no non-vacuous pair is ever provably equal.
  ‹parity_eq_true a b› asks provable equality of every witness pair, so a
  reflexive-looking check such as ‹x == x› is ∗‹not› classified true by this
  interface either: ‹aval_abs› only ever hands both sides the same
  ∗‹abstract› value ‹PEven›/‹POdd›/‹PTop›, which still ranges over
  infinitely many concrete integers, so ‹eq_true› stays false there too ---
  correctly: this classification layer never assumes two occurrences of the
  same syntactic expression carry a hidden equality constraint.

  ‹parity_eq_true› is genuinely provable to be true for identical parity
  classes when combined at the check level with the compiler-independent
  evaluator; this file states it as it is, no more.
›

definition parity_eq_true :: "parity ⇒ parity ⇒ bool" where
  "parity_eq_true = parity_vacuous"

lemma parity_eq_true_sound:
  assumes "parity_eq_true a b" and "i ∈ gamma_parity a" and "j ∈ gamma_parity b"
  shows "i = j"
  using assms unfolding parity_eq_true_def parity_vacuous_def by (cases a; cases b; auto)

text ‹
  ‹parity_eq_false› is where parity earns its keep: two values of disjoint
  parity classes --- one ‹PEven›, the other ‹POdd› --- can never be equal,
  regardless of how imprecise Sign or Interval are about the same pair (both
  may see fully overlapping sign/range information). This is the one query
  Parity answers strictly better than a vacuity check.
›

fun parity_eq_false :: "parity ⇒ parity ⇒ bool" where
    "parity_eq_false PEven POdd = True"
  | "parity_eq_false POdd PEven = True"
  | "parity_eq_false a b = (a = PBot ∨ b = PBot)"

lemma parity_eq_false_sound:
  assumes "parity_eq_false a b" and "i ∈ gamma_parity a" and "j ∈ gamma_parity b"
  shows "i ≠ j"
  using assms by (cases a; cases b; auto)

subsection ‹Goblint-style optional-Boolean queries›

text ‹
  ‹parity_less›/‹parity_eq› are the generic packaging of the four judgments
  above, so one interpretation both introduces them and discharges the query
  interface. Nothing about that packaging is backward-specific: it asks only
  for four judgments and their soundness, which is why parity can reuse it
  while having no ‹inv_less› for the derivations beside it to read off. The
  ⬚‹defines› clause is what keeps the two queries ordinary
  top-level constants, with the code equation the check layer needs.
›

global_interpretation parity_numeric_queries:
  numeric_query_judgments
    parity_less_true parity_less_false parity_eq_true parity_eq_false
  defines parity_less = parity_numeric_queries.query_less
    and parity_eq = parity_numeric_queries.query_eq
  by unfold_locales
     (auto intro: parity_less_true_sound parity_eq_true_sound
            dest: parity_less_false_sound parity_eq_false_sound)


end