Theory Routed_Analysis_Sound

theory Routed_Analysis_Sound
  imports DG_Analysis_Adapter Routed_Context_Unit
begin

section ‹Reading a solved routed system as an analysis result›

text ‹
  A routed analysis is assembled from two independent choices: which abstract
  domain it computes in, and which context policy it routes calls by. This
  theory is the composition step that does not depend on either. It takes a
  solved routed equation system and derives the analysis-level soundness
  statement, so a concrete analysis supplies its domain facts and its policy
  facts and interprets this once, rather than repeating the derivation per
  (domain, policy) pair.

  ‹solved_local_reader› is the one reader every instance uses: at a
  covered unknown it hands back the solution's local half, and elsewhere
  ‹bot›. Reading a global key gives ‹bot› too -- the routed seed keys carry
  entry contributions, not program-point values, and a result table never
  reads them.
›

definition solved_local_reader ::
  "(pp × 'c) set ⇒ (pp × 'c + 'k ⇒ ('D::bounded_semilattice_sup_bot, 'G) dg_state)
   ⇒ pp × 'c + 'k ⇒ 'D"
where
  "solved_local_reader vars sigma k =
     (case k of Inl vc ⇒ (if vc ∈ vars then dg_local (sigma (Inl vc)) else bot)
              | Inr _ ⇒ bot)"

lemma solved_local_reader_covered [simp]:
  "vc ∈ vars ⟹ solved_local_reader vars sigma (Inl vc) = dg_local (sigma (Inl vc))"
  by (simp add: solved_local_reader_def)

lemma solved_local_reader_uncovered [simp]:
  "vc ∉ vars ⟹ solved_local_reader vars sigma (Inl vc) = bot"
  by (simp add: solved_local_reader_def)

lemma solved_local_reader_global [simp]:
  "solved_local_reader vars sigma (Inr k) = bot"
  by (simp add: solved_local_reader_def)

text ‹
  The reader returns only the local half. The global half enters through the
  concretization the locale below pairs with it, which publishes each local
  value together with the solved global at ‹Inr buffer_key›. Under that
  pairing the two coverage obligations \<^locale>‹dg_context_activation› asks for
  hold by construction, given ‹gammaDG_rd› and that the publication map takes
  ‹bot› to \<^const>‹Bot›. Neither depends on the domain or the context policy,
  so no instance need prove them again.
›

subsection ‹The composition locale›

text ‹
  Everything a routed analysis needs above its solved system, in one place: the
  domain enters through ‹S› and ‹γ⇩D⇩G›, the context policy through ‹route›,
  ‹adm› and ‹seed›, and the solved system through ‹sigma›/‹vars›. The
  fixed reader is \<^const>‹solved_local_reader›, and its concretization reads
  the solved global at ‹Inr buffer_key› as the second argument of ‹rd›,
  so the two coverage obligations are the one-line lemmas above.

  An instance is then a single ⬚‹interpretation›, and the theorems below are
  what it gets: a published result table, its per-node soundness, and the
  check report's proved/refuted verdicts.
›

locale routed_analysis =
  dg_analysis_adapter S γ⇩D⇩G 𝒢 g buffer_key global_of route bot0 d⇩0 g⇩0 sigma vars x0
    "solved_local_reader vars sigma" seed is_bot
    "λd. gamma_lift γ⇩V (rd d (genv global_of sigma))"
    adm rd γ⇩V empty⇩V classify
  for S :: "(pp × 'c, 'k, 'n, 'D::bounded_semilattice_sup_bot,
              'G::bounded_semilattice_sup_bot) dg_spec"
    and γ⇩D⇩G :: "'D ⇒ ('n ⇒ 'G) ⇒ store set"
    and 𝒢 :: "vname ⇒ bool"
    and g buffer_key and global_of :: "'n ⇒ 'k"
    and route :: "pp ⇒ 'c ⇒ 'D ⇒ call_action ⇒ 'c"
    and bot0 d⇩0 :: 'D and g⇩0 :: 'G
    and sigma :: "pp × 'c + 'k ⇒ ('D, 'G) dg_state"
    and vars :: "(pp × 'c) set"
    and x0 :: "pp × 'c"
    and seed :: "pp ⇒ 'c ⇒ 'k"
    and is_bot :: "'D ⇒ bool"
    and adm :: "'c context_policy"
    and rd :: "'D ⇒ ('n ⇒ 'G) ⇒ 'v lifted"
    and γ⇩V :: "'v ⇒ store set"
    and empty⇩V :: "'v ⇒ bool"
    and classify :: "exp ⇒ 'v ⇒ check_result"

end