Theory Voblint_Domain.Forward_Domain

theory Forward_Domain
  imports State_Concretization "Voblint_VIMP.VIMP_Expr"
begin

section ‹Forward evaluation over a numeric domain›

text ‹
  Every expression-level interface of a domain needs the same two operations: an
  evaluator of expressions over an abstract state and a truth test on abstract values.
  Guard refinement (‹sound_refinement›), the special calls of the transfer
  functions (‹sound_minmax_ops›), the arithmetic of an expression domain
  (‹sound_arith_ops›) and the check layer (‹sound_check_query›)
  all build on them.  Stating the operations and their laws once lets a domain prove
  them once: the first interpretation registers them, and every later interface over
  the same operations inherits them instead of asking again.

  The evaluator is stated over any state type ‹'d› together with the stores
  ‹γ⇩S d› a state describes.  The pointwise abstract states of the
  numeric domains are the instance at their pointwise ‹gamma_state›; the check layer keeps
  the state type open.
›

locale sound_evaluator =
  fixes γ⇩S :: "'d ⇒ store set"
    and aval_abs :: "exp ⇒ 'd ⇒ 'a::numeric_domain" ("⟦_⟧⇧♯")
  assumes aval_abs_sound[intro]:
    "s ∈ γ⇩S d ⟹ ⟦e⟧⇩e s ∈ γ (⟦e⟧⇧♯ d)"

text ‹
  A truth test answers ‹Some b› only when every integer the abstract value
  concretizes to has truthiness ‹b›; ‹None› means the value cannot decide.
›

locale sound_truth_test =
  fixes tobool :: "'a::numeric_domain ⇒ bool option"
  assumes tobool_sound:
    "tobool p = Some b ⟹ i ∈ γ p ⟹ truthy i = b"

text ‹
  Monotonicity is not needed for soundness.  The solver's least-solution theorem and
  the monotone transfer interfaces ask for it, so it is a separate layer.
  ‹tobool_mono› reads downward: a definite answer at a coarser value survives at a
  sharper non-empty one.
›

locale mono_evaluator = sound_evaluator γ⇩S aval_abs
  for γ⇩S :: "'d::order ⇒ store set"
    and aval_abs :: "exp ⇒ 'd ⇒ 'a::numeric_domain" ("⟦_⟧⇧♯") +
  assumes aval_abs_mono[intro]:
    "d1 ≤ d2 ⟹ ⟦e⟧⇧♯ d1 ≤ ⟦e⟧⇧♯ d2"

text ‹
  ‹mono_truth_test› adds ‹tobool_mono› on top of the sound truth test,
  the downward monotonicity described above for non-empty values.
›

locale mono_truth_test = sound_truth_test +
  assumes tobool_mono:
    "¬ is_empty p1 ⟹ p1 ≤ p2 ⟹ tobool p2 = Some bv ⟹ tobool p1 = Some bv"

end