Theory Activation_Trace_Context

theory Activation_Trace_Context
  imports Activation_Trace_Def
begin

section ‹Activation context selection and context-indexed collecting›

text ‹
  The activation context is computed from the concrete trace after the fact and is
  activation-stable: fixed when the activation is created and unchanged by the calls it
  later makes and returns from.  \<^const>‹Root› carries the seed; a \<^const>‹Call› routes the
  caller context on the call site and the entered store --- ‹sink_node parent› is
  exactly the call site, since \<^const>‹extend› only ever appends to the callee path and
  leaves ‹parent› frozen there; a \<^const>‹Resume› keeps the resumed caller's own context, so
  a completed call does not repartition the caller.  Exposing the call site to ‹enterc› is
  what makes a call-site-keyed context (a k-call-string) expressible as an instance rather
  than only as a generator-side hook.›
fun activation_context_of :: "(cfg_node ⇒ 'c ⇒ store ⇒ 'c) ⇒ 'c ⇒ activation_trace ⇒ 'c" where
  "activation_context_of enterc initial_ctx (Root _)                  = initial_ctx"
| "activation_context_of enterc initial_ctx (Call parent p)           =
     enterc (sink_node parent) (activation_context_of enterc initial_ctx parent) (snd (hd p))"
| "activation_context_of enterc initial_ctx (Resume current callee _) = activation_context_of enterc initial_ctx current"

text ‹‹activation_context_of› fixes one context per trace by decoding the entered store exactly: a
  \<^const>‹Call› activation's context is derived from its caller's OWN selected context,
  not re-derived from the concrete store independently at each node. This is what keeps a
  chosen context stable across a CALL/RETURN pair: the callee's context in \<^const>‹Resume›
  resumes through ‹current›, so a completed call cannot repartition the caller.

  ‹activation_context_of› is the deterministic special case: a total function from the entered store to a
  context, never a relation admitting several contexts for one concrete activation. The
  unit and call-site/k-call-string routing instances are exactly this shape, and the
  executable routed solver's own ‹route› is typed to return a single context, not a set.
  The entry-state instance is not: a call may answer several overlapping alternatives, each
  covering the same concrete activation and routing it to its own context, so its concrete
  semantics is stated directly over ‹activation_context_rel›/‹context_policy› rather than over
  ‹activation_context_of›. ‹activation_context_of› is therefore not the primary semantics; it is the deterministic
  compatibility witness for the functional case, connected to ‹activation_context_rel› via
  ‹context_policy_of_fun› and ‹activation_context_rel_of_fun_iff›.›


lemma activation_context_extend_nonempty:
  "path_of t ≠ [] ⟹ activation_context_of enterc initial_ctx (extend t x) = activation_context_of enterc initial_ctx t"
  by (cases t) (auto simp: hd_append)


subsection ‹Admissible callee contexts, as a set per call›

text ‹
  An analysis's entry operation answers a ∗‹list› of alternatives and its context
  selector is applied to each, so one concrete call may be admitted in several contexts.
  ‹context_policy› is the semantic shape of that whole-call protocol: given the call
  site, the caller's own context, the call's information, the caller store and the entered
  store, it returns the set of callee contexts that may describe this transition.  The set
  may be empty or have several elements; ‹call_context_total_on› below requires it to be
  non-empty for every covered call.  Both stores are
  arguments so an instance can tie the chosen context to one alternative whose continuation
  half covers the caller and whose entry half covers the entered store, never mixing two.

  A functional policy --- the unit context, a k-call-string --- returns a singleton,
  ‹context_policy_of_fun›.  The abstract selector an analysis actually runs stays a
  function of the abstract entry state; only the activation-trace semantics is set-valued.
›

type_synonym 'c context_policy =
  "cfg_node ⇒ 'c ⇒ call_info ⇒ store ⇒ store ⇒ 'c set"

definition context_policy_of_fun ::
  "(cfg_node ⇒ 'c ⇒ store ⇒ 'c) ⇒ 'c context_policy"
where
  "context_policy_of_fun f u ctx ci caller entered = {f u ctx entered}"

lemma context_policy_of_fun_iff [simp]:
  "ctx' ∈ context_policy_of_fun f u ctx ci caller entered ⟷ ctx' = f u ctx entered"
  by (simp add: context_policy_of_fun_def)

lemma context_policy_of_fun_nonempty [simp]:
  "context_policy_of_fun f u ctx ci caller entered ≠ {}"
  by (simp add: context_policy_of_fun_def)

text ‹
  ‹admits_call_context 𝒢 g adm u ctx p s es ctx'›: from node ‹u› in context ‹ctx› with store
  ‹s›, some ‹calls› edge of ‹g› enters ‹p› with exactly the store ‹es›, and ‹adm› admits
  ‹ctx'› for that edge.  It is \<^const>‹call_enter_store› with the callee and the admitted
  context made explicit.  Naming the edge by its effect rather than assuming it unique keeps
  the semantics honest on a graph with two call edges leaving one node, exactly as
  ‹valid_activation_trace.ret› does.
›

definition admits_call_context ::
  "(vname ⇒ bool) ⇒ cfg ⇒ 'c context_policy
     ⇒ cfg_node ⇒ 'c ⇒ pname ⇒ store ⇒ store ⇒ 'c ⇒ bool"
where
  "admits_call_context 𝒢 g adm u ctx p s es ctx' ⟷
     (∃dst pars args cont.
        (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
        ∧ es = call_enter 𝒢 (CallEdge dst pars args) s
        ∧ ctx' ∈ adm u ctx (call_info_of (CallEdge dst pars args) p) s es)"

lemma admits_call_contextI:
  assumes "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
    and "ctx' ∈ adm u ctx (call_info_of (CallEdge dst pars args) p) s
           (call_enter 𝒢 (CallEdge dst pars args) s)"
  shows "admits_call_context 𝒢 g adm u ctx p s (call_enter 𝒢 (CallEdge dst pars args) s) ctx'"
  using assms unfolding admits_call_context_def by blast

lemma admits_call_contextE:
  assumes "admits_call_context 𝒢 g adm u ctx p s es ctx'"
  obtains dst pars args cont
    where "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
      and "es = call_enter 𝒢 (CallEdge dst pars args) s"
      and "ctx' ∈ adm u ctx (call_info_of (CallEdge dst pars args) p) s es"
  using assms unfolding admits_call_context_def by blast

lemma admits_call_context_call_enter_storeD:
  "admits_call_context 𝒢 g adm u ctx p s es ctx' ⟹ call_enter_store 𝒢 g u s es"
  unfolding admits_call_context_def call_enter_store_def by blast

lemma admits_call_context_of_fun:
  "admits_call_context 𝒢 g (context_policy_of_fun f) u ctx p s es ctx'
     ⟷ (∃dst pars args cont.
           (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
           ∧ es = call_enter 𝒢 (CallEdge dst pars args) s)
       ∧ ctx' = f u ctx es"
  unfolding admits_call_context_def by auto

text ‹
  ‹activation_context_rel 𝒢 adm c⇩0 g t ctx›: the trace ‹t› may carry context ‹ctx›.  A root
  carries ‹c⇩0›; a call carries any context admitted for its creating transition,
  computed from the caller's own carried context; a resumed caller keeps what it carried.
›

inductive activation_context_rel ::
  "(vname ⇒ bool) ⇒ 'c context_policy ⇒ 'c ⇒ cfg ⇒ activation_trace ⇒ 'c ⇒ bool"
  for 𝒢 :: "vname ⇒ bool" and adm :: "'c context_policy" and c⇩0 :: 'c and g :: cfg
where
  Root [intro]: "activation_context_rel 𝒢 adm c⇩0 g (Root xs) c⇩0"
| Call [intro]:
    "activation_context_rel 𝒢 adm c⇩0 g caller c
     ⟹ admits_call_context 𝒢 g adm (sink_node caller) c p (sink_store caller) es c'
     ⟹ activation_context_rel 𝒢 adm c⇩0 g (Call caller ((FunctionEntry p, es) # xs)) c'"
| Resume [intro]:
    "activation_context_rel 𝒢 adm c⇩0 g current c
     ⟹ activation_context_rel 𝒢 adm c⇩0 g (Resume current callee xs) c"


inductive_cases activation_context_rel_RootE [elim!]:
  "activation_context_rel 𝒢 adm c⇩0 g (Root xs) ctx"

inductive_cases activation_context_rel_CallE [elim]:
  "activation_context_rel 𝒢 adm c⇩0 g (Call parent xs) ctx"

inductive_cases activation_context_rel_ResumeE [elim]:
  "activation_context_rel 𝒢 adm c⇩0 g (Resume current callee xs) ctx"

lemma activation_context_rel_Root_iff [simp]:
  "activation_context_rel 𝒢 adm c⇩0 g (Root xs) ctx ⟷ ctx = c⇩0"
  by blast

lemma activation_context_rel_Resume_iff [simp]:
  "activation_context_rel 𝒢 adm c⇩0 g (Resume current callee xs) ctx
     ⟷ activation_context_rel 𝒢 adm c⇩0 g current ctx"
  by blast

lemma activation_context_rel_Call_Nil [simp]:
  "¬ activation_context_rel 𝒢 adm c⇩0 g (Call parent []) ctx"
  by blast

text ‹The carried context of a called activation depends on its caller and its entry
  record only: the rest of the local path is irrelevant, which is what makes an intra step
  context-preserving.›
lemma activation_context_rel_Call_iff:
  "activation_context_rel 𝒢 adm c⇩0 g (Call parent ((n, es) # xs)) ctx'
     ⟷ (∃ctx p. n = FunctionEntry p
           ∧ activation_context_rel 𝒢 adm c⇩0 g parent ctx
           ∧ admits_call_context 𝒢 g adm (sink_node parent) ctx p (sink_store parent) es ctx')"
  by blast

lemma activation_context_rel_extend:
  assumes "path_of t ≠ []"
  shows "activation_context_rel 𝒢 adm c⇩0 g (extend t x) ctx
           ⟷ activation_context_rel 𝒢 adm c⇩0 g t ctx"
proof (cases t)
  case (Call parent xs)
  then obtain n es ys where "xs = (n, es) # ys" using assms by (cases xs) auto
  then show ?thesis using Call by (simp add: activation_context_rel_Call_iff)
qed simp_all

subsection ‹Context entry invariant›

text ‹The invariants below concern the traces of one graph from one set of initial stores,
  so the block fixes ‹𝒢›, ‹g› and ‹S› and writes ‹𝒯› for
  ‹𝒯⇘𝒢,g,S⇙›.›

context
  fixes 𝒢 :: "vname ⇒ bool" and g :: cfg and S :: "store set"
begin

private abbreviation (input) traces :: "activation_trace set" where "traces ≡ 𝒯⇘𝒢,g,S⇙"
notation traces ("𝒯")

text ‹A called activation carries exactly the contexts admitted for the transition from its
  immediate caller, each computed from a context the caller itself carries.  Stated as an
  equivalence: forwards, a RETURN argument recovers the caller's slot from the callee's;
  backwards, it re-enters the callee at a context derived from whichever slot the resumed
  caller is being placed in.›
lemma activation_context_rel_caller_entry:
  assumes "callee ∈ 𝒯"
  shows "∀u ∈ callers callee. ∀c. caller_of u = Some c
       ⟶ (∃p es. hd (path_of u) = (FunctionEntry p, es)
             ∧ (∀ctx'. activation_context_rel 𝒢 adm c⇩0 g u ctx'
                  ⟷ (∃ctx. activation_context_rel 𝒢 adm c⇩0 g c ctx
                        ∧ admits_call_context 𝒢 g adm (sink_node c) ctx p (sink_store c) es ctx')))"
proof -
  define P where "P u ⟷ (∀c. caller_of u = Some c
       ⟶ (∃p es. hd (path_of u) = (FunctionEntry p, es)
             ∧ (∀ctx'. activation_context_rel 𝒢 adm c⇩0 g u ctx'
                  ⟷ (∃ctx. activation_context_rel 𝒢 adm c⇩0 g c ctx
                        ∧ admits_call_context 𝒢 g adm (sink_node c) ctx p (sink_store c) es ctx'))))"
    for u
  have "∀u ∈ callers callee. P u"
  proof (rule caller_chain_closure[OF _ _ _ _ assms])
    fix s show "P (Root [(cfg_entry g, s)])" by (simp add: P_def)
  next
    fix t a v s' assume t: "t ∈ 𝒯" and IH: "∀u ∈ callers t. P u"
    have "path_of t ≠ []" using valid_activation_trace_path_nonempty[OF t] .
    with IH[THEN bspec, OF callers_refl] show "P (extend t (v, s'))"
      by (simp add: P_def activation_context_rel_extend hd_append)
  next
    fix caller dst pars args p cont
    show "P (Call caller
        [(FunctionEntry p, call_enter 𝒢 (CallEdge dst pars args) (sink_store caller))])"
      unfolding P_def by (auto simp: activation_context_rel_Call_iff)
  next
    fix callee caller p dst pars args cont
    assume cv: "callee ∈ 𝒯" and IH: "∀u ∈ callers callee. P u"
      and cof: "caller_of callee = Some caller"
    have "path_of caller ≠ []"
      using valid_activation_trace_path_nonempty[OF valid_activation_trace_caller_valid[OF cv cof]]
      .
    moreover have "P caller" using IH ancestors_caller[OF cof] by blast
    ultimately show "P (Resume caller callee
        (path_of caller @ [(cont, combine_collect 𝒢 dst (sink_store caller) (sink_store callee))]))"
      by (simp add: P_def hd_append)
  qed
  then show ?thesis unfolding P_def .
qed

lemma activation_context_rel_caller_entryE:
  assumes "callee ∈ 𝒯" and "caller_of callee = Some caller"
    and "activation_context_rel 𝒢 adm c⇩0 g callee ctx'"
  obtains ctx p where "hd (path_of callee) = (FunctionEntry p, entry_store callee)"
    and "activation_context_rel 𝒢 adm c⇩0 g caller ctx"
    and "admits_call_context 𝒢 g adm (sink_node caller) ctx p (sink_store caller)
           (entry_store callee) ctx'"
proof -
  from activation_context_rel_caller_entry[OF assms(1), THEN bspec, OF callers_refl,
      rule_format, OF assms(2)]
  obtain p es where hd: "hd (path_of callee) = (FunctionEntry p, es)"
    and iff: "∀ctx'. activation_context_rel 𝒢 adm c⇩0 g callee ctx'
         ⟷ (∃ctx. activation_context_rel 𝒢 adm c⇩0 g caller ctx
               ∧ admits_call_context 𝒢 g adm (sink_node caller) ctx p (sink_store caller) es ctx')"
    by force
  have "es = entry_store callee" using hd by (simp add: entry_store_def)
  with hd iff assms(3) show thesis using that by blast
qed

lemma activation_context_rel_caller_entryI:
  assumes "callee ∈ 𝒯" and "caller_of callee = Some caller"
    and "hd (path_of callee) = (FunctionEntry p, entry_store callee)"
    and "activation_context_rel 𝒢 adm c⇩0 g caller ctx"
    and "admits_call_context 𝒢 g adm (sink_node caller) ctx p (sink_store caller)
           (entry_store callee) ctx'"
  shows "activation_context_rel 𝒢 adm c⇩0 g callee ctx'"
proof -
  from activation_context_rel_caller_entry[OF assms(1), THEN bspec, OF callers_refl,
      rule_format, OF assms(2)]
  obtain p' es where hd: "hd (path_of callee) = (FunctionEntry p', es)"
    and iff: "∀ctx'. activation_context_rel 𝒢 adm c⇩0 g callee ctx'
         ⟷ (∃ctx. activation_context_rel 𝒢 adm c⇩0 g caller ctx
               ∧ admits_call_context 𝒢 g adm (sink_node caller) ctx p' (sink_store caller) es ctx')"
    by force
  have "p' = p" and "es = entry_store callee" using hd assms(3) by simp_all
  with iff assms(4,5) show ?thesis by blast
qed

text ‹A functional policy carries exactly \<^const>‹activation_context_of›'s context on every valid activation trace.  The
  restriction to valid activation traces is what supplies the call edge the relational clause names.›
lemma activation_context_rel_of_fun_iff:
  assumes "t ∈ 𝒯"
  shows "activation_context_rel 𝒢 (context_policy_of_fun f) c⇩0 g t ctx
           ⟷ activation_context_of f c⇩0 t = ctx"
proof -
  define P where "P u ⟷ (∀ctx. activation_context_rel 𝒢 (context_policy_of_fun f) c⇩0 g u ctx
                                ⟷ activation_context_of f c⇩0 u = ctx)" for u
  have "∀u ∈ callers t. P u"
  proof (rule caller_chain_closure[OF _ _ _ _ assms])
    fix s show "P (Root [(cfg_entry g, s)])" by (simp add: P_def eq_commute)
  next
    fix t a v s' assume t: "t ∈ 𝒯" and IH: "∀u ∈ callers t. P u"
    have "path_of t ≠ []" using valid_activation_trace_path_nonempty[OF t] .
    with IH[THEN bspec, OF callers_refl] show "P (extend t (v, s'))"
      by (simp add: P_def activation_context_extend_nonempty activation_context_rel_extend)
  next
    fix caller dst pars args p cont
    assume IH: "∀u ∈ callers caller. P u"
      and e: "(sink_node caller, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
    have Pc: "P caller" using IH callers_refl by blast
    show "P (Call caller
        [(FunctionEntry p, call_enter 𝒢 (CallEdge dst pars args) (sink_store caller))])"
      unfolding P_def activation_context_rel_Call_iff admits_call_context_of_fun
      using Pc[unfolded P_def] e by auto
  next
    fix callee caller p dst pars args cont
    assume IH: "∀u ∈ callers callee. P u" and cof: "caller_of callee = Some caller"
    have "P caller" using IH ancestors_caller[OF cof] by blast
    then show "P (Resume caller callee
        (path_of caller @ [(cont, combine_collect 𝒢 dst (sink_store caller) (sink_store callee))]))"
      by (simp add: P_def)
  qed
  then show ?thesis unfolding P_def using callers_refl by blast
qed

subsection ‹Functional context entry invariant›

text ‹Every ancestor of a valid activation trace is itself valid: ‹caller_chain_closure›'s own
  four cases are exactly \<^const>‹valid_activation_trace›'s four introduction rules, so the closure fact
  and validity coincide.›

lemma callers_valid:
  assumes "callee ∈ 𝒯" and "u ∈ callers callee"
  shows "u ∈ 𝒯"
proof -
  have "∀u ∈ callers callee. u ∈ 𝒯"
  proof (rule caller_chain_closure[OF _ _ _ _ assms(1)], goal_cases Root Intra Call Ret)
    case (Root s) then show ?case by (rule valid_activation_trace.root)
  next
    case (Intra t a v s') then show ?case by (blast intro: valid_activation_trace.intra)
  next
    case (Call caller dst pars args p cont) then show ?case
      by (blast intro: valid_activation_trace.call)
  next
    case (Ret callee caller p dst pars args cont) then show ?case
      by (blast intro: valid_activation_trace.ret)
  qed
  then show ?thesis using assms(2) by blast
qed

text ‹The context of an activation is exactly what ‹enterc› computes from its immediate
  caller's own context and the entered store.  This is what lets a RETURN argument
  construct the callee's context directly from the caller's chosen one, rather than
  rediscovering it after the fact. A special case of ‹activation_context_rel_caller_entry› at
  the functional policy \<^const>‹context_policy_of_fun›, where ‹activation_context_rel_of_fun_iff›
  pins both sides' witness context to \<^const>‹activation_context_of› and ‹admits_call_context_of_fun› reads off
  the ‹enterc›-equation and the call-edge witness in one step.›

lemma activation_context_entry_invariant:
  assumes "callee ∈ 𝒯"
  shows "∀u ∈ callers callee. ∀c. caller_of u = Some c ⟶
       activation_context_of enterc initial_ctx u = enterc (sink_node c) (activation_context_of enterc initial_ctx c) (entry_store u)
       ∧ call_enter_store 𝒢 g (sink_node c) (sink_store c) (entry_store u)"
proof (intro ballI allI impI)
  fix u c assume mem: "u ∈ callers callee" and cof: "caller_of u = Some c"
  have uv: "u ∈ 𝒯" using callers_valid[OF assms mem] .
  have cv: "c ∈ 𝒯" using valid_activation_trace_caller_valid[OF uv cof] .
  have tc_u: "activation_context_rel 𝒢 (context_policy_of_fun enterc) initial_ctx g u
                (activation_context_of enterc initial_ctx u)"
    by (simp only: activation_context_rel_of_fun_iff[OF uv])
  obtain p ctx where "hd (path_of u) = (FunctionEntry p, entry_store u)"
    and tc_c: "activation_context_rel 𝒢 (context_policy_of_fun enterc) initial_ctx g c ctx"
    and adm: "admits_call_context 𝒢 g (context_policy_of_fun enterc) (sink_node c) ctx p
                (sink_store c) (entry_store u) (activation_context_of enterc initial_ctx u)"
    by (rule activation_context_rel_caller_entryE[OF uv cof tc_u])
  have activation_context_c: "activation_context_of enterc initial_ctx c = ctx"
    using tc_c by (simp only: activation_context_rel_of_fun_iff[OF cv])
  have adm': "activation_context_of enterc initial_ctx u = enterc (sink_node c) ctx (entry_store u)"
    using adm unfolding admits_call_context_of_fun by simp
  have activation_context_eq: "activation_context_of enterc initial_ctx u
                  = enterc (sink_node c) (activation_context_of enterc initial_ctx c) (entry_store u)"
    unfolding activation_context_c using adm' .
  show "activation_context_of enterc initial_ctx u
          = enterc (sink_node c) (activation_context_of enterc initial_ctx c) (entry_store u)
        ∧ call_enter_store 𝒢 g (sink_node c) (sink_store c) (entry_store u)"
    using activation_context_eq admits_call_context_call_enter_storeD[OF adm] by (intro conjI)
qed

lemma key_entry_invariant_call_enterD [dest]:
  assumes "callee ∈ 𝒯" and "caller_of callee = Some caller"
  shows "call_enter_store 𝒢 g (sink_node caller) (sink_store caller) (entry_store callee)"
  using activation_context_entry_invariant[OF assms(1), THEN bspec, OF callers_refl, rule_format, OF
    assms(2)]
  by (rule conjunct2)

end

subsection ‹Conditional totality›

text ‹
  A policy may admit no context for a call.  The callee activation then carries no
  context and drops out of every bucket, but the resumed caller keeps its own, so the
  continuation is still collected.  CALL and RETURN hold vacuously at such a call, and a
  claim may leave the continuation uncovered although a valid activation trace reaches it there
  (‹total_dropped_unsound› in ‹Example_Non_Vacuity›).  ‹call_context_total_on cover adm 𝒢 g›
  rules that out exactly where it matters: at every call edge, every store the claimed
  ‹cover› admits at the call site has some admissible callee context.  A dead call site
  owes nothing.  The graph of a function is total outright.
›

definition call_context_total_on ::
  "(cfg_node ⇒ 'c ⇒ store set) ⇒ 'c context_policy ⇒ (vname ⇒ bool) ⇒ cfg ⇒ bool"
where
  "call_context_total_on cover adm 𝒢 g ⟷
     (∀u dst pars args p cont ctx s.
        (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
        ⟶ s ∈ cover u ctx
        ⟶ adm u ctx (call_info_of (CallEdge dst pars args) p) s
              (call_enter 𝒢 (CallEdge dst pars args) s) ≠ {})"

lemma call_context_total_onE:
  assumes "call_context_total_on cover adm 𝒢 g"
    and "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g"
    and "s ∈ cover u ctx"
  obtains ctx' where "admits_call_context 𝒢 g adm u ctx p s
                        (call_enter 𝒢 (CallEdge dst pars args) s) ctx'"
  using assms unfolding call_context_total_on_def
  by (blast intro: admits_call_contextI)

lemma call_context_total_on_of_fun [simp]:
  "call_context_total_on cover (context_policy_of_fun f) 𝒢 g"
  unfolding call_context_total_on_def context_policy_of_fun_def by blast

subsection ‹The activation-indexed context collecting›

text ‹The activation-sensitive collecting is the sink stores of valid activation traces reaching ‹v›
  that may carry the queried context ‹c›.  One trace may carry several contexts, so the
  buckets of one node cover its stores without partitioning them.›

definition activation_collect ::
  "(vname ⇒ bool) ⇒ 'c context_policy ⇒ 'c ⇒ cfg
     ⇒ store set ⇒ cfg_node ⇒ 'c ⇒ store set"
    ("𝒜⇘_,_,_,_,_⇙") where
  "𝒜⇘𝒢,adm,c⇩0,g,S⇙ v c =
     {sink_store t | t. t ∈ 𝒯⇘𝒢,g,S⇙ ∧ sink_node t = v
                        ∧ activation_context_rel 𝒢 adm c⇩0 g t c}"

lemma activation_collect_I [intro]:
  "t ∈ 𝒯⇘𝒢,g,S⇙ ⟹ sink_node t = v ⟹ activation_context_rel 𝒢 adm c⇩0 g t c
   ⟹ sink_store t ∈ 𝒜⇘𝒢,adm,c⇩0,g,S⇙ v c"
  unfolding activation_collect_def by blast

text ‹Every collected state has a valid activation trace witness carrying the queried ‹c›.›
lemma activation_collect_E [elim]:
  assumes "s ∈ 𝒜⇘𝒢,adm,c⇩0,g,S⇙ v c"
  obtains t where "t ∈ 𝒯⇘𝒢,g,S⇙" "sink_node t = v"
    "activation_context_rel 𝒢 adm c⇩0 g t c" "sink_store t = s"
  using assms unfolding activation_collect_def by blast

text ‹Under a functional policy the buckets are \<^const>‹activation_context_of›'s fibres.›
lemma activation_collect_of_fun:
  "𝒜⇘𝒢,context_policy_of_fun f,c⇩0,g,S⇙ v c =
     {sink_store t | t. t ∈ 𝒯⇘𝒢,g,S⇙ ∧ sink_node t = v ∧ activation_context_of f c⇩0 t = c}"
  unfolding activation_collect_def
  by (auto simp: activation_context_rel_of_fun_iff)


end