Theory Activation_Trace_Collect

theory Activation_Trace_Collect
  imports Activation_Trace_Context
begin

section ‹Which stores can occur at each node›

text ‹
  ‹𝒞⇘𝒢,g,S⇙ v› is the set of stores a run can actually have at node ‹v›: take
  every valid activation trace that ends there and keep its final store.  This is the concrete set an
  analysis has to over-approximate, so it is the target of every soundness statement
  downstream.

  \<^const>‹valid_activation_trace› has four clauses --- root, intra
  step, call, return --- each reading exactly the relation for its phenomenon: ‹intra› for
  local extension, ‹calls› for entering a callee and for recovering a continuation.  The
  return clause recovers the caller from the completed callee's own ancestry through
  \<^const>‹caller_of›, never by an independent choice.

  There is no global exit node: whole-program completion is collection at
  ‹FunctionResult main›, and a procedure result is an ordinary collected node rather than a
  separate summary mechanism.
›

subsection ‹Forgetful projections›

text ‹‹node_collect› is the concrete collecting view: the sink stores of valid activation traces
  reaching node ‹v›.  \<^const>‹activation_collect› is the context-indexed collector, keeping
  those whose trace may carry the queried context; the context type is not required
  finite, and a bucket is not claimed to be an exact activation identity.›

definition node_collect ::
    "(vname ⇒ bool) ⇒ cfg ⇒ store set ⇒ cfg_node ⇒ store set"
    ("𝒞⇘_,_,_⇙") where
  "𝒞⇘𝒢,g,S⇙ v =
     {sink_store t | t. t ∈ 𝒯⇘𝒢,g,S⇙ ∧ sink_node t = v}"

text ‹Up to the inhabitation witness, every lemma concerns one graph and one set of
  initial stores, so the block fixes ‹𝒢›, ‹g› and ‹S› and writes
  ‹𝒯› and ‹𝒞 v› for ‹𝒯⇘𝒢,g,S⇙› and
  ‹𝒞⇘𝒢,g,S⇙ v›.›

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

private abbreviation (input) traces :: "activation_trace set" where "traces ≡ 𝒯⇘𝒢,g,S⇙"
private abbreviation (input) collect :: "cfg_node ⇒ store set"
  where "collect ≡ 𝒞⇘𝒢,g,S⇙"
notation traces ("𝒯") and collect ("𝒞")

lemma node_collect_I [intro]:
  "t ∈ 𝒯 ⟹ sink_store t ∈ 𝒞 (sink_node t)"
  unfolding node_collect_def by blast

text ‹Every collected state has a valid activation trace witness.›
lemma node_collect_E [elim]:
  assumes "s ∈ 𝒞 v"
  obtains t where "t ∈ 𝒯" "sink_node t = v" "sink_store t = s"
  using assms unfolding node_collect_def by blast

text ‹
  \<^const>‹node_collect› is closed under intra flow: extending a witness trace by one
  \<^const>‹intra› edge is ‹valid_activation_trace.intra›.  Closure under ∗‹call› and ∗‹return›
  steps is deliberately absent here --- ‹valid_activation_trace.ret› requires the popped activation to be the
  witness trace's own caller, which a bare CFG step does not supply.
›

lemma node_collect_intra_step:
  assumes s: "s ∈ 𝒞 u"
    and e: "(u, a, v) ∈ intra g"
    and st: "s' ∈ edge_step a s"
  shows "s' ∈ 𝒞 v"
proof -
  from s obtain t where t: "t ∈ 𝒯" and n: "sink_node t = u" and w: "sink_store t = s"
    by (rule node_collect_E)
  have "extend t (v, s') ∈ 𝒯"
    by (rule valid_activation_trace.intra[OF t]) (use e st n w in simp_all)
  from node_collect_I[OF this] show ?thesis by simp
qed

text ‹
  The activation-preserving form.  Following an \<^const>‹intra_path› only ‹extend›s the trace, so
  the resulting witness is the ∗‹same› activation: same caller and same entry node.  Callers
  that must know ∗‹which› activation reached a node need this: the collection at a node
  merges every activation that reaches it.
›

lemma valid_activation_trace_intra_path_extend_pair:
  "intra_path g x y ⟹ t ∈ 𝒯 ⟹ sink_node t = fst x ⟹ sink_store t = snd x
   ⟹ ∃t'. t' ∈ 𝒯 ∧ sink_node t' = fst y ∧ sink_store t' = snd y
            ∧ caller_of t' = caller_of t ∧ fst (hd (path_of t')) = fst (hd (path_of t))"
proof (induction arbitrary: t rule: star.induct)
  case (refl x)
  then show ?case by blast
next
  case (step x y z)
  obtain u s where x: "x = (u, s)" by (cases x)
  obtain w s1 where y: "y = (w, s1)" by (cases y)
  from step.hyps(1) x y obtain a where
    e: "(u, a, w) ∈ intra g" and st: "s1 ∈ edge_step a s"
    by auto
  have ext: "extend t (w, s1) ∈ 𝒯"
    by (rule valid_activation_trace.intra[OF step.prems(1)])
       (use e st step.prems(2,3) x in simp_all)
  have hd_ext: "fst (hd (path_of (extend t (w, s1)))) = fst (hd (path_of t))"
    using valid_activation_trace_path_nonempty[OF step.prems(1)] by simp
  from step.IH[OF ext] y obtain t' where
    "t' ∈ 𝒯" "sink_node t' = fst z" "sink_store t' = snd z"
    "caller_of t' = caller_of (extend t (w, s1))"
    "fst (hd (path_of t')) = fst (hd (path_of (extend t (w, s1))))" by auto
  then show ?case using hd_ext by auto
qed

lemma valid_activation_trace_intra_path_extend:
  assumes p: "intra_path g (sink_node t, sink_store t) (v, s')"
    and t: "t ∈ 𝒯"
  obtains t' where "t' ∈ 𝒯" "sink_node t' = v" "sink_store t' = s'"
    "caller_of t' = caller_of t" "fst (hd (path_of t')) = fst (hd (path_of t))"
  using valid_activation_trace_intra_path_extend_pair[OF p t] by auto

text ‹
  A call and its matching return ∗‹do› compose, which is what makes the missing
  single-step closure above harmless in practice.  The callee trace is built from
  the caller's by ‹valid_activation_trace.call›, so ‹valid_activation_trace.ret›'s side condition --- that the
  activation being popped is this trace's own caller --- holds by construction,
  and running the callee to its \<^const>‹FunctionResult› along \<^const>‹intra_path›
  preserves it.  What a caller supplies is the call edge and an intra path through
  the callee; what it gets back is the continuation node with the combined store.
›

lemma node_collect_call_return_step:
  assumes s: "s ∈ 𝒞 u"
      and ce: "(u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls g"
      and body: "intra_path g (FunctionEntry q, call_enter 𝒢 (CallEdge dst pars args) s)
                   (FunctionResult q, t)"
  shows "combine_collect 𝒢 dst s t ∈ 𝒞 cont"
proof -
  from s obtain caller where cv: "caller ∈ 𝒯"
    and cn: "sink_node caller = u" and cs: "sink_store caller = s"
    by (rule node_collect_E)
  let ?entered = "Call caller [(FunctionEntry q, call_enter 𝒢 (CallEdge dst pars args) s)]"
  have ev: "?entered ∈ 𝒯"
    using valid_activation_trace.call [OF cv, where dst = dst and pars = pars and args = args
                            and p = q and cont = cont]
      ce cn cs by simp
  obtain callee where dv: "callee ∈ 𝒯"
    and dn: "sink_node callee = FunctionResult q" and ds: "sink_store callee = t"
    and dc: "caller_of callee = caller_of ?entered"
    by (rule valid_activation_trace_intra_path_extend [OF _ ev]) (use body in simp_all)
  have "Resume caller callee
          (path_of caller @ [(cont, combine_collect 𝒢 dst (sink_store caller) (sink_store callee))])
          ∈ 𝒯"
    by (rule valid_activation_trace.ret [OF dv _ dn]) (use dc ce cn in simp_all)
  from node_collect_I [OF this] show ?thesis
    using cs ds by (simp add: sink_node_def sink_store_def)
qed

subsection ‹Collecting equations›

text ‹(1) Initial stores are collected at \<^const>‹cfg_entry›.›
lemma node_collect_init:
  "s ∈ S ⟹ s ∈ 𝒞 (cfg_entry g)"
  using node_collect_I[OF valid_activation_trace.root] by simp

subsection ‹Context-sensitive / context-insensitive bridge›

text ‹Bridge (1): every context bucket, and so their union, is included in the
  context-insensitive collection.›
theorem activation_collect_le_node_collect:
  "𝒜⇘𝒢,adm,c⇩0,g,S⇙ v c ⊆ 𝒞 v"
  unfolding activation_collect_def node_collect_def by blast

theorem Union_activation_collect_le_node_collect:
  "(⋃c. 𝒜⇘𝒢,adm,c⇩0,g,S⇙ v c) ⊆ 𝒞 v"
  using activation_collect_le_node_collect by blast

text ‹Bridge (2): the converse needs every valid activation trace to carry some context.  That premise is
  the whole content of the direction -- a policy that leaves some trace uncontexted loses the
  stores on it, and the union then falls short.  A functional policy has it outright, since
  \<^const>‹activation_context_of› is total; a relational one earns it from conditional totality, which is
  ‹Activation_Trace_Abstract›'s business.  No finiteness assumption either way.›
theorem node_collect_eq_Union_activation_of_has_context:
  assumes has_ctx: "⋀t. t ∈ 𝒯 ⟹ ∃c. activation_context_rel 𝒢 adm c⇩0 g t c"
  shows "𝒞 v = (⋃c. 𝒜⇘𝒢,adm,c⇩0,g,S⇙ v c)"
proof
  show "𝒞 v ⊆ (⋃c. 𝒜⇘𝒢,adm,c⇩0,g,S⇙ v c)"
  proof
    fix x assume "x ∈ 𝒞 v"
    then obtain t where t: "t ∈ 𝒯" "sink_node t = v" "sink_store t = x"
      by (rule node_collect_E)
    from has_ctx [OF t(1)] obtain c where "activation_context_rel 𝒢 adm c⇩0 g t c" ..
    with t show "x ∈ (⋃c. 𝒜⇘𝒢,adm,c⇩0,g,S⇙ v c)"
      by blast
  qed
next
  show "(⋃c. 𝒜⇘𝒢,adm,c⇩0,g,S⇙ v c) ⊆ 𝒞 v"
    by (rule Union_activation_collect_le_node_collect)
qed

theorem node_collect_eq_Union_activation_of_fun:
  "𝒞 v
     = (⋃c. 𝒜⇘𝒢,context_policy_of_fun f,c⇩0,g,S⇙ v c)"
  by (rule node_collect_eq_Union_activation_of_has_context)
     (simp add: activation_context_rel_of_fun_iff)

end


section ‹The collecting semantics is inhabited›

text ‹
  \<^const>‹valid_activation_trace› and \<^const>‹node_collect› are defined over an arbitrary graph, and every
  soundness statement downstream is an over-approximation claim about them; if they were
  empty, all of it would hold vacuously.  A two-node graph with one assignment edge settles
  that inside this session, without borrowing a graph from the compiler: the initial store is
  collected at the entry, and the assigned store is collected one edge later.
›

definition activation_trace_witness_cfg :: cfg where
  "activation_trace_witness_cfg =
     ⦇ intra = {(Statement 0, EA_Assign (STR ''x'') (N 1), Statement 1)},
       calls = {},
       cfg_entry = Statement 0 ⦈"

lemma activation_trace_witness_entry [simp]: "cfg_entry activation_trace_witness_cfg = Statement 0"
  by (simp add: activation_trace_witness_cfg_def)

lemma activation_trace_witness_edge [simp]:
  "(Statement 0, EA_Assign (STR ''x'') (N 1), Statement 1) ∈ intra activation_trace_witness_cfg"
  by (simp add: activation_trace_witness_cfg_def)

lemma activation_trace_witness_root:
  "Root [(Statement 0, s)] ∈ 𝒯⇘𝒢,activation_trace_witness_cfg,{s}⇙"
proof -
  have "Root [(cfg_entry activation_trace_witness_cfg, s)] ∈ 𝒯⇘𝒢,activation_trace_witness_cfg,{s}⇙"
    by (rule valid_activation_trace.root) simp
  then show ?thesis by simp
qed

theorem node_collect_witness:
  "s ∈ 𝒞⇘𝒢,activation_trace_witness_cfg,{s}⇙ (Statement 0)"
  "s(STR ''x'' := 1) ∈ 𝒞⇘𝒢,activation_trace_witness_cfg,{s}⇙ (Statement 1)"
proof -
  have root: "Root [(Statement 0, s)] ∈ 𝒯⇘𝒢,activation_trace_witness_cfg,{s}⇙"
    by (rule activation_trace_witness_root)
  show "s ∈ 𝒞⇘𝒢,activation_trace_witness_cfg,{s}⇙ (Statement 0)"
    using node_collect_I[OF root] by (simp add: sink_node_def sink_store_def)
  have "extend (Root [(Statement 0, s)]) (Statement 1, s(STR ''x'' := 1))
          ∈ 𝒯⇘𝒢,activation_trace_witness_cfg,{s}⇙"
    by (rule valid_activation_trace.intra[OF root, where a = "EA_Assign (STR ''x'') (N 1)"
                                        and v = "Statement 1"])
       (simp_all add: activation_trace_witness_cfg_def sink_node_def sink_store_def)
  from node_collect_I[OF this]
  show "s(STR ''x'' := 1) ∈ 𝒞⇘𝒢,activation_trace_witness_cfg,{s}⇙ (Statement 1)"
    by (simp add: sink_node_def sink_store_def)
qed

end