Theory Activation_Backbone

theory Activation_Backbone
  imports "Voblint_Domain.Nonrelational_State" "Voblint_CFG.Activation_Trace_Abstract"
begin

section ‹What one activation of a procedure may observe›

text ‹
  Every concrete call creates one callee activation.  Each step of that activation carries
  the contexts its creating call admits, a nested call derives its callee's contexts from
  those, and a return resumes the caller at the caller's own.  const‹activation_context_rel› replays
  those choices along a trace, so a table indexed by ‹(node, context)› can be checked
  against concrete runs without carrying an auxiliary digest.  That indexing is many-to-one
  and one-to-many at once: activations reaching the same context are collected together,
  and one activation may be collected under several contexts.  The buckets of a node cover
  its stores; they need not partition them.

  ‹cover v c› is the set of stores that table admits at node ‹v› in context ‹c›.  Given the
  five local obligations of locale‹activation_coverage› on it --- ‹INIT› for the seed stores,
  ‹INTRA› per intra edge, ‹CALL› per call and admitted context, ‹RETURN› per return,
  ‹TOTAL› for at least one admitted context per covered call ---
  ‹activation_collect_sound› bounds const‹activation_collect›, the set
  of stores some valid activation trace can leave at one ‹(node, context)›.  It is the context-sensitive
  twin of ‹node_collect_semantic_postfix› and shares its proof shape: interpret
  locale‹activation_coverage› at the supplied ‹cover›, then read off ‹valid_activation_trace_covered_at›.

  ‹adm› says which contexts may describe a concrete call transition, and that is what indexes
  the collecting semantics.  It is handed both stores, so a policy may inspect them, but
  need not: a call-string policy ignores them, and an entry-state policy is induced by the
  analyzer's own routing decisions on the abstract entry alternatives that cover them.
  Proving that a particular policy's ‹route› induces an ‹adm› total on the solved table is
  the routed context locale's job downstream, not this theorem's.
›

theorem activation_collect_sound:
  assumes "activation_coverage g S cover adm c0 𝒢"
  shows "𝒜⇘𝒢,adm,c0,g,S⇙ v c ⊆ cover v c"
proof -
  interpret G: activation_coverage g S cover adm c0 𝒢 by (fact assms)
  show ?thesis
  proof (rule subsetI)
    fix st assume "st ∈ 𝒜⇘𝒢,adm,c0,g,S⇙ v c"
    then obtain t where t: "t ∈ 𝒯⇘𝒢,g,S⇙"
      and sn: "sink_node t = v" and kc: "activation_context_rel 𝒢 adm c0 g t c"
      and st: "sink_store t = st"
      by (rule activation_collect_E)
    have "sink_store t ∈ cover (sink_node t) c" using G.valid_activation_trace_covered_at[OF t kc]
      .
    then show "st ∈ cover v c" using sn st by simp
  qed
qed

end