Theory Numeric_Queries

theory Numeric_Queries
  imports State_Concretization
begin

section ‹Numeric relational query interface›

text ‹
  Entailment/refutation of ‹<›/‹=› over an abstract numeric value is not
  check-specific: it is the same question a backward/guard domain answers,
  phrased as a query instead of a narrowing. ‹less›/‹eq› package that answer
  in Goblint's own shape -- ‹ID.lt›/‹ID.eq› -- a definite ‹Some True›, a
  definite ‹Some False›, or ‹None› when neither direction is provable, the
  same three-way shape ‹tobool› already gives a single abstract value's
  truthiness.

  ‹sound_numeric_queries› fixes that shape together with its soundness
  obligation, as ‹sound_truth_test› does for ‹tobool›. Kept in a session with
  no ‹exp›/‹store› concept at all, so a domain
  that only has these two operations could still interpret it: the
  ‹sound_refinement› locale refines an
  abstract value under an assumed truth value; ‹sound_numeric_queries›
  instead classifies an already-fixed pair of values as provably related,
  provably unrelated, or neither.

  ‹numeric_query_judgments›, below, is how every domain here builds such an
  instance: it packages four yes/no judgments into the two queries and proves
  the obligation once, so no domain restates that step. Where the four
  judgments come from is the domain's business. Every ‹sound_refinement›
  instance reads them off its own narrowing operators, in the
  ‹Backward_Numeric_Queries› theory, and gets an instance for free; a
  concrete domain may instead supply sharper, hand-tuned judgments when that
  derivation loses precision it cannot recover, or judgments unrelated to
  narrowing altogether.
›

text ‹The soundness obligation, stated so that a ‹Some› answer is exact rather than merely
  one-sided: every concrete pair drawn from the two values must relate the way the answer
  says.  ‹None› carries no obligation at all, which is what lets a domain answer it whenever
  it cannot decide.›
locale sound_numeric_queries =
  fixes less :: "'a::numeric_domain ⇒ 'a ⇒ bool option"
    and eq :: "'a ⇒ 'a ⇒ bool option"
  assumes less_sound[intro]:
      "less a b = Some r ⟹ i ∈ γ a ⟹ j ∈ γ b ⟹ (i < j) = r"
    and eq_sound[intro]:
      "eq a b = Some r ⟹ i ∈ γ a ⟹ j ∈ γ b ⟹ (i = j) = r"

subsection ‹Building an instance from four judgments›

text ‹
  A domain rarely decides ‹less›/‹eq› in one step. It decides four separate
  judgments -- every witness pair satisfies ‹<›, every witness pair refutes
  it, and the same two for ‹=› -- and the two queries are those four read in
  order: prefer the affirmative judgment, fall back to the refuting one,
  answer ‹None› when neither fires. ‹numeric_query_judgments› fixes the four
  and their soundness, and nothing else, so a domain interprets it whatever
  the judgments were read off: a narrowing operator, a comparison of bounds,
  a test that one side denotes nothing.

  The two queries are named ‹query_less›/‹query_eq› rather than
  ‹less›/‹eq›, which would share a base name with the order's \<^const>‹less›
  and the vendored solver's ‹eq›. Interpreting the locale introduces them as
  ordinary top-level constants through a ⬚‹defines› clause, and
  therefore with the code equation a constant living in a still-abstract locale
  context does not have.

  ‹less_true› and ‹less_false› (and ‹eq_true› and ‹eq_false›) can both hold
  at once only when an operand denotes nothing: a live witness pair on both
  sides would have to satisfy ‹i < j› and ‹¬ i < j› simultaneously. So on
  any pair of feasible operands the ‹if› choice between ‹Some True› and
  ‹Some False› below is never live.
›

locale numeric_query_judgments =
  fixes less_true :: "'a::numeric_domain ⇒ 'a ⇒ bool"
    and less_false :: "'a ⇒ 'a ⇒ bool"
    and eq_true :: "'a ⇒ 'a ⇒ bool"
    and eq_false :: "'a ⇒ 'a ⇒ bool"
  assumes less_true_sound:
      "less_true a b ⟹ i ∈ γ a ⟹ j ∈ γ b ⟹ i < j"
    and less_false_sound:
      "less_false a b ⟹ i ∈ γ a ⟹ j ∈ γ b ⟹ ¬ i < j"
    and eq_true_sound:
      "eq_true a b ⟹ i ∈ γ a ⟹ j ∈ γ b ⟹ i = j"
    and eq_false_sound:
      "eq_false a b ⟹ i ∈ γ a ⟹ j ∈ γ b ⟹ i ≠ j"
begin

definition query_less :: "'a ⇒ 'a ⇒ bool option" where
  "query_less a b = (if less_true a b then Some True else if less_false a b then Some False else None)"

definition query_eq :: "'a ⇒ 'a ⇒ bool option" where
  "query_eq a b = (if eq_true a b then Some True else if eq_false a b then Some False else None)"

lemma less_opt_sound:
  assumes "query_less a b = Some r" and "i ∈ γ a" and "j ∈ γ b"
  shows "(i < j) = r"
  using assms less_true_sound less_false_sound unfolding query_less_def by (auto split: if_splits)

lemma eq_opt_sound:
  assumes "query_eq a b = Some r" and "i ∈ γ a" and "j ∈ γ b"
  shows "(i = j) = r"
  using assms eq_true_sound eq_false_sound unfolding query_eq_def by (auto split: if_splits)

end

sublocale numeric_query_judgments ⊆ sound_numeric_queries query_less query_eq
proof
  fix a b r i j
  assume "query_less a b = Some r" and "i ∈ γ a" and "j ∈ γ b"
  then show "(i < j) = r" by (rule less_opt_sound)
next
  fix a b r i j
  assume "query_eq a b = Some r" and "i ∈ γ a" and "j ∈ γ b"
  then show "(i = j) = r" by (rule eq_opt_sound)
qed

end