Theory Checks

theory Checks
  imports "Voblint_CFG.CFG_Def"
begin

section ‹Ordinary assertion checks: store-only, no ghost-domain or
  additional trace-projection dependency›

text ‹
  A check table relates program points to the boolean conditions placed
  there; several checks may share one point. ‹checks_proven› states that
  every concrete store the caller's reachable-store function admits at a
  checked point satisfies that point's condition. The reachable-store
  function is left abstract (‹pp ⇒ store set›) so an instance supplies
  whatever collecting semantics its own ‹analysis_contract› interpretation
  already proves sound: this theory adds no new soundness anchor, only the
  store-level check layer on top of an existing one.

  A compiled graph's table is read off its ‹EA_Check› edges: each edge
  contributes its source node and its condition.
›

type_synonym checks = "(pp × exp) set"

definition checks_proven :: "checks ⇒ (pp ⇒ store set) ⇒ bool" where
  "checks_proven ck reach ⟷ (∀v c. (v, c) ∈ ck ⟶ (∀s ∈ reach v. truthy (⟦c⟧⇩e s)))"

lemma checks_provenI [intro]:
  "(⋀v c s. (v, c) ∈ ck ⟹ s ∈ reach v ⟹ truthy (⟦c⟧⇩e s)) ⟹ checks_proven ck reach"
  unfolding checks_proven_def by blast

text ‹The one-step destruction dual of ‹checks_provenI›, so a caller with a
  ‹checks_proven› fact in hand reaches the store-level conclusion without
  unfolding the definition. It carries no soundness content of its own, and is
  named for what it is rather than ‹_sound›: the real soundness work happens
  where a caller establishes ‹checks_proven› for a concrete ‹reach›, by
  composing this theory with an existing ‹node_collect ≤ gamma_state(…)›-shaped
  corollary; this theory never states or proves that inclusion itself.›

lemma checks_provenD [dest]:
  assumes proven: "checks_proven ck reach"
    and at_v: "(v, c) ∈ ck"
    and mem: "s ∈ reach v"
  shows "truthy (⟦c⟧⇩e s)"
  using proven at_v mem unfolding checks_proven_def by blast

end