Theory Solved_Table

theory Solved_Table
  imports "Voblint_Domain.Nonrelational_Reachability" "Voblint_CFG.CFG_Def"
begin

section ‹Solved analysis results›

text ‹
  The canonical, domain-generic shape of a finished analysis: a set of covered
  @{typ "pp × 'ctx"} keys together with a total lookup into a per-point
  abstract state. Checks, reports, and rendering are downstream consumers of
  this table, not siblings of it.

  The datatype constrains neither the key set nor the payloads. What the rest
  of this text describes --- finitely many keys, and canonical payloads --- is
  ‹wf_solved_table›, stated at the end of this theory. Its two halves are
  not established alike: an adapter canonicalizes every payload it publishes,
  so canonicality is unconditional, while finiteness holds only for those
  context policies whose whole context space is bounded in advance, and is
  carried as a hypothesis everywhere else.

  \<^const>‹Bot› means ``the solver's canonical result at this key is an
  outer \<^const>‹Bot›'', or the key is absent from ‹covered_keys› altogether;
  ‹Lifted a› means ``the canonical result is \<^const>‹Lifted›'', with the
  local unknown projected to the abstract state ‹a›. This is a structural
  reading, not a semantic-emptiness test: raw solver values are
  canonicalized -- a witness-bottom \<^const>‹Lifted› payload collapsed to
  \<^const>‹Bot› -- ∗‹before› they reach this boundary (every public result
  adapter routes through ‹canonicalize_lift›), so by the time a value
  reaches ‹lookup_table› here, \<^const>‹Bot› denotes no store. The converse
  does not hold: the emptiness test is sound and need not be complete, so a
  \<^const>‹Lifted› state may still denote no store (a product whose interval
  field says ‹x = 2› and whose parity field says ‹x› is odd stays
  \<^const>‹Lifted›).
›

subsection ‹Per-point reachability›

text ‹
  Per-point reachability is \<^typ>‹'a lifted› itself
  (\<^theory>‹Voblint_Domain.Reachability_Lift›), not a nominal copy of it: the
  reachability reading is fixed below rather than
  left to the caller, and stated directly in terms of \<^const>‹Bot›/
  \<^const>‹Lifted›. \<^const>‹map_lift› is the functorial map (payload
  rewriting that leaves reachability alone).
›

text ‹
  A point of an abstract-store table concretizes through the reachability
  lift: \<^const>‹Bot› to nothing, a \<^const>‹Lifted› store to its concretization.
  It is the lift at \<^const>‹gamma_state›, so a result generic in its published
  value reads back to exactly this at an abstract-store instance.
›

lemma gamma_state_of_reachable_env [simp]:
  "γ (case p of Bot ⇒ bot | Lifted st ⇒ st) = γ⇩⊥ p"
  for p :: "'a::numeric_domain abs_state lifted"
  by (cases p) simp_all

subsection ‹The result table›

text ‹
  ‹covered_keys› is the authoritative coverage surface --- the keys the
  solver actually reached --- while ‹table_at› is merely a total
  lookup function, defined everywhere but meaningful only on the key set.
  ‹lookup_table› keeps that distinction explicit rather than trusting
  ‹table_at› to answer sensibly off the key set.

  \<^typ>‹'ctx› carries no ordering or enumeration constraint: real context
  types include interval-vector and call-string contexts, which have
  neither.
›

datatype (plugins del: quickcheck_narrowing) ('ctx, 'a) solved_table =
  Solved_Table
    (covered_keys: "(pp × 'ctx) set")
    (table_at: "pp ⇒ 'ctx ⇒ 'a lifted")

definition table_contexts :: "('ctx, 'a) solved_table ⇒ pp ⇒ 'ctx set" where
  "table_contexts r v = snd ` Set.filter (λ(v', ctx). v' = v) (covered_keys r)"

definition lookup_table ::
  "('ctx, 'a) solved_table ⇒ pp ⇒ 'ctx ⇒ 'a lifted" where
  "lookup_table r v ctx =
     (if (v, ctx) ∈ covered_keys r then table_at r v ctx else Bot)"

lemma table_contexts_iff [simp]: "ctx ∈ table_contexts r v ⟷ (v, ctx) ∈ covered_keys r"
  unfolding table_contexts_def by force

lemma lookup_table_absent [simp]:
  "(v, ctx) ∉ covered_keys r ⟹ lookup_table r v ctx = Bot"
  unfolding lookup_table_def by simp

subsection ‹Telling ``analysed and dead'' from ``never analysed''›

text ‹
  \<^const>‹lookup_table› answers \<^const>‹Bot› for two unrelated reasons: the
  solver covered the key and stored \<^const>‹Bot› there, or it never covered the
  key at all. The first is a proved statement about the program; the second is
  the absence of one. A reader of the answer alone cannot tell which happened,
  so a claim about concrete unreachability must not be stated over it.
›

datatype (plugins del: quickcheck_narrowing) 'a context_result =
    Uncovered
  | Covered "'a lifted"

text ‹
  \<^typ>‹'a context_result› keeps the two apart at the lookup, rather than
  pushing the distinction into \<^typ>‹'a lifted›: making non-coverage a lattice
  element would put solver bookkeeping into the abstract domain and raise
  questions -- how it orders against \<^const>‹Bot›, what a join with it means --
  that have no semantic answer. Coverage is metadata about a solve; \<^const>‹Bot›
  is a statement about a program.
›

definition lookup_coverage ::
  "('ctx, 'a) solved_table ⇒ pp ⇒ 'ctx ⇒ 'a context_result" where
  "lookup_coverage r v ctx =
     (if (v, ctx) ∈ covered_keys r then Covered (table_at r v ctx) else Uncovered)"

lemma lookup_coverage_covered [simp]:
  "(v, ctx) ∈ covered_keys r ⟹
     lookup_coverage r v ctx = Covered (table_at r v ctx)"
  unfolding lookup_coverage_def by simp

lemma lookup_coverage_uncovered [simp]:
  "(v, ctx) ∉ covered_keys r ⟹ lookup_coverage r v ctx = Uncovered"
  unfolding lookup_coverage_def by simp

lemma lookup_coverage_eq_Uncovered_iff:
  "lookup_coverage r v ctx = Uncovered ⟷ (v, ctx) ∉ covered_keys r"
  unfolding lookup_coverage_def by simp

lemma lookup_coverage_eq_Covered_iff:
  "lookup_coverage r v ctx = Covered x ⟷
     (v, ctx) ∈ covered_keys r ∧ table_at r v ctx = x"
  unfolding lookup_coverage_def by auto

text ‹
  Where the information is lost, named so that losing it is a visible step.
  \<^const>‹lookup_table› is exactly this totalization, which is why it is safe
  to keep for callers that only ever read a covered key -- and why a soundness
  claim may not be stated over it directly.
›

fun context_result_or_bot :: "'a context_result ⇒ 'a lifted" where
  "context_result_or_bot Uncovered = Bot"
| "context_result_or_bot (Covered x) = x"

lemma lookup_table_eq_or_bot:
  "lookup_table r v ctx =
     context_result_or_bot (lookup_coverage r v ctx)"
  unfolding lookup_table_def lookup_coverage_def by simp

text ‹
  The logical core of every ``the reported point is unreachable'' claim, stated
  once here rather than per domain. It starts from \<^term>‹Covered Bot›, so an
  uncovered node cannot satisfy it however the caller obtained its inclusion.
›

lemma reported_covered_unreachable_empty:
  assumes lookup: "lookup_coverage r v ctx = Covered Bot"
    and sound: "C ⊆ gamma_lift gam (lookup_table r v ctx)"
  shows "C = {}"
  using sound unfolding lookup_table_eq_or_bot lookup by simp

text ‹
  The node-level reading, quantifying over the contexts at ‹v›. It asks only
  that every ∗‹stored› result there is \<^const>‹Bot›; an uncovered context is
  permitted rather than required to be absent, since whatever an uncovered
  context contributes is a question for the solve that produced the table, not
  for this predicate. A single \<^term>‹Covered (Lifted s)› at any context defeats
  it, which is the whole point: that context may still carry executions.

  Read the vacuous case before using this: a node with ∗‹no› stored context
  satisfies it, since there is nothing to be non-\<^const>‹Bot›. On its own that
  would be a hole --- ``never analysed'' passing as ``proved dead''. It is not
  one only where a caller separately knows that an unstored context contributes
  nothing, which is a property of the solve, not of this table. Do not lift this
  predicate out of a setting that establishes it.
›

definition result_node_is_bottom ::
  "('ctx, 'a) solved_table ⇒ pp ⇒ bool" where
  "result_node_is_bottom r v ⟷
     (∀ctx a. lookup_coverage r v ctx = Covered a ⟶ a = Bot)"

lemma result_node_is_bottomI:
  assumes "⋀ctx a. lookup_coverage r v ctx = Covered a ⟹ a = Bot"
  shows "result_node_is_bottom r v"
  unfolding result_node_is_bottom_def using assms by blast

lemma result_node_is_bottomD:
  assumes bot: "result_node_is_bottom r v"
    and covered: "(v, ctx) ∈ covered_keys r"
  shows "lookup_coverage r v ctx = Covered Bot"
proof -
  have eq: "lookup_coverage r v ctx = Covered (table_at r v ctx)"
    using covered by simp
  have "table_at r v ctx = Bot"
    using bot eq unfolding result_node_is_bottom_def by blast
  with eq show ?thesis by simp
qed

lemma lookup_table_LiftedD [dest]:
  "lookup_table r v ctx = Lifted st ⟹ ctx ∈ table_contexts r v"
  using lookup_table_absent by fastforce

subsection ‹Well-formed results›

text ‹
  \<^const>‹Solved_Table› is an ordinary constructor, so the two properties the
  opening text describes are not enforced by the type and have to be stated.

  Finiteness is the load-bearing one, and its failure is silent rather than
  loud: a per-node aggregate over \<^const>‹table_contexts› folds with
  \<^const>‹Finite_Set.fold›, which answers with its unit on an infinite carrier.
  The contextual check report's verdict aggregate is one such fold: over an
  infinite key set it reports a check dead whatever its contexts say.

  Canonicality is what licenses reading \<^const>‹Bot› as concrete emptiness
  rather than as the solver's own structural answer. \<^const>‹Lifted› gets no
  such reading: the supplied emptiness predicate is sound, not complete. It is stated against a supplied emptiness predicate, the
  same way the normalization operations upstream are, so this layer keeps its
  freedom from any class constraint on the payload.
›

definition finite_solved_table :: "('ctx, 'a) solved_table ⇒ bool" where
  "finite_solved_table r ⟷ finite (covered_keys r)"

definition wf_solved_table ::
  "('a ⇒ bool) ⇒ ('ctx, 'a) solved_table ⇒ bool" where
  "wf_solved_table empty_pred r ⟷
     finite_solved_table r
   ∧ (∀v ctx st. lookup_table r v ctx = Lifted st ⟶ ¬ empty_pred st)"

lemma wf_solved_table_finite [dest]:
  "wf_solved_table empty_pred r ⟹ finite_solved_table r"
  unfolding wf_solved_table_def by simp

lemma wf_solved_table_LiftedD [dest]:
  "⟦wf_solved_table empty_pred r; lookup_table r v ctx = Lifted st⟧
     ⟹ ¬ empty_pred st"
  unfolding wf_solved_table_def by blast

lemma finite_table_contexts:
  assumes "finite_solved_table r"
  shows "finite (table_contexts r v)"
  using assms unfolding finite_solved_table_def table_contexts_def by simp

text ‹What canonicality buys: on a well-formed result the structural
  reading and the concrete one coincide, provided the supplied predicate is
  the exact emptiness test its adapters use.›

lemma wf_solved_table_gamma_point_eq_empty_iff:
  fixes r :: "('ctx, 'a::numeric_domain abs_state) solved_table"
    and empty_pred :: "'a abs_state ⇒ bool"
  assumes wf: "wf_solved_table empty_pred r"
    and exact: "⋀st. empty_pred st ⟷ γ st = {}"
  shows "γ⇩⊥ (lookup_table r v ctx) = {} ⟷ lookup_table r v ctx = Bot"
proof (cases "lookup_table r v ctx")
  case Bot
  then show ?thesis by simp
next
  case (Lifted st)
  have "¬ empty_pred st" using wf Lifted by blast
  with exact Lifted show ?thesis by simp
qed

end