Theory Activation_Trace_Def

theory Activation_Trace_Def
  imports CFG_Transfer
begin

section ‹Activation traces›

text ‹
  An ‹activation_trace› represents one procedure activation of a sequential run and its
  concrete ancestry.  Its own path contains ‹(cfg_node, store)› pairs; structural constructors record the
  suspended caller and, after resumption, the completed callee.  Activation contexts
  are projections of this structure rather than fields stored in the trace.

  Local flow follows ‹intra›, including ‹EA_Ret› into the matching
  ‹FunctionResult›.  A ‹calls› tuple supplies the call site, callee entry, and
  continuation.  The call rule builds the parameter-bound entered store with
  \<^const>‹call_enter›.  The resume rule combines caller locals, callee globals,
  and the return value with \<^const>‹combine_collect›.

  The shape is adapted from the local traces of Schwarz et al., ∗‹Improving Thread-Modular
  Abstract Interpretation› (SAS 2021), and Schwarz and Erhard, ∗‹Data Race Detection
  by Digest-Driven Abstract Interpretation› (arXiv:2511.11055, 2025).  Theirs is a
  multithreaded semantics: a local trace is one thread's view, in which operations of different
  threads are only partially ordered.  An activation trace is one activation of a sequential run,
  and a return composes the completed callee into its suspended caller.
›

subsection ‹The datatype›

text ‹
  ▪ ‹Root p› --- the main activation, with local path ‹p›.
  ▪ ‹Call caller p› --- a callee whose local path ‹p› starts at the entered store;
    ‹caller› is the exact suspended caller, frozen at the call node.
  ▪ ‹Resume current callee p› --- the activation continued past a completed call.
    ‹current› is that activation frozen at its call node (the value that spawned ‹callee›);
    ‹callee› is the retained completed callee subtree; ‹p› is the continued path.
›

text ‹An ‹activation_path› lists the nodes one activation passed and the store it held at
  each.  An activation trace carries the path of its own activation, with the surrounding activations beside it rather than on it.›

type_synonym activation_path = "(cfg_node × store) list"

datatype activation_trace =
    Root activation_path
  | Call (activation_trace_caller: activation_trace) activation_path
  | Resume (activation_trace_current: activation_trace) (activation_trace_callee: activation_trace)
    activation_path

subsection ‹Observers›

text ‹‹path_of› is the activation path.  ‹sink_node› and ‹sink_store›
  return its final program point and final store.›

fun path_of :: "activation_trace ⇒ activation_path" where
  "path_of (Root p)       = p"
| "path_of (Call _ p)     = p"
| "path_of (Resume _ _ p) = p"

definition entry_store :: "activation_trace ⇒ store" where
  "entry_store t = snd (hd (path_of t))"

definition sink_node :: "activation_trace ⇒ cfg_node" where
  "sink_node t = fst (last (path_of t))"

definition sink_store :: "activation_trace ⇒ store" where
  "sink_store t = snd (last (path_of t))"

text ‹‹caller_of› recovers the creating caller of an activation.  It descends the frozen
  ‹caller› field of a \<^const>‹Resume›, so it works uniformly for a returned callee of any
  constructor --- this is what makes nested and recursive returns compose.›

fun caller_of :: "activation_trace ⇒ activation_trace option" where
  "caller_of (Root _)             = None"
| "caller_of (Call caller _)      = Some caller"
| "caller_of (Resume current _ _) = caller_of current"

subsection ‹Extension and context projection›

text ‹‹extend› appends one step to the innermost local path; it never touches an outer
  constructor's caller/callee fields.›
fun extend :: "activation_trace ⇒ (cfg_node * store) ⇒ activation_trace" where
  "extend (Root p) x       = Root (p @ [x])"
| "extend (Call c p) x     = Call c (p @ [x])"
| "extend (Resume c d p) x = Resume c d (p @ [x])"

subsection ‹The closure relation›

text ‹
  ‹valid_activation_trace› is the least set closed under four concrete operations: an initial main
  activation at \<^const>‹cfg_entry›; an ‹intra› step; a call; and a return.  Each rule reads
  exactly the relation for its phenomenon.  ‹intra› carries no side condition --- calls are
  not ‹intra› members, so they are untraversable by typing.  ‹call› enters the callee named
  by the ‹calls› edge at the entered store \<^const>‹call_enter›.  ‹ret› matches the
  callee's ‹FunctionResult p› against the ‹FunctionEntry p› of a concrete ‹calls› edge
  leaving the caller's node, and resumes at the continuation stored in that same edge; the
  resumed state is \<^const>‹combine_collect›.  There is no ‹combines› lookup and no scan for a
  compatible context.
›

inductive_set valid_activation_trace ::
    "(vname ⇒ bool) ⇒ cfg ⇒ store set ⇒ activation_trace set"
    ("𝒯⇘_,_,_⇙")
  for 𝒢 and g and S where
  root:
    "s ∈ S
     ⟹ Root [(cfg_entry g, s)] ∈ 𝒯⇘𝒢,g,S⇙"
| intra:
    "t ∈ 𝒯⇘𝒢,g,S⇙
     ⟹ (sink_node t, a, v) ∈ intra g
     ⟹ s' ∈ edge_step a (sink_store t)
     ⟹ extend t (v, s') ∈ 𝒯⇘𝒢,g,S⇙"
| call:
    "caller ∈ 𝒯⇘𝒢,g,S⇙
     ⟹ (sink_node caller, CallEdge dst pars args, FunctionEntry p, cont)
           ∈ calls g
     ⟹ Call caller
           [(FunctionEntry p,
             call_enter 𝒢 (CallEdge dst pars args) (sink_store caller))]
         ∈ 𝒯⇘𝒢,g,S⇙"
| ret:
    "callee ∈ 𝒯⇘𝒢,g,S⇙
     ⟹ caller_of callee = Some caller
     ⟹ sink_node callee = FunctionResult p
     ⟹ (sink_node caller, CallEdge dst pars args, FunctionEntry p, cont)
           ∈ calls g
     ⟹ Resume caller callee
           (path_of caller
              @ [(cont, combine_collect 𝒢 dst
                          (sink_store caller) (sink_store callee))])
         ∈ 𝒯⇘𝒢,g,S⇙"

inductive_cases valid_activation_trace_RootE [elim]:
  "Root p ∈ 𝒯⇘𝒢,g,S⇙"

inductive_cases valid_activation_trace_CallE [elim]:
  "Call caller p ∈ 𝒯⇘𝒢,g,S⇙"

inductive_cases valid_activation_trace_ResumeE [elim]:
  "Resume caller callee p ∈ 𝒯⇘𝒢,g,S⇙"

subsection ‹Structural lemmas›

text ‹How the three trace shapes answer the projections every later proof reads them
  through -- path, sink, caller, entry store.  Kept as ‹simp› rules so an induction over
  ‹valid_activation_trace› never has to case on the constructor merely to look up a sink.›
lemma extend_simps [simp]:
  "path_of (extend t x) = path_of t @ [x]"
  "caller_of (extend t x) = caller_of t"
  "sink_node (extend t x) = fst x"
  "sink_store (extend t x) = snd x"
  by (cases t; auto simp: sink_node_def sink_store_def)+

lemma sink_single_simps [simp]:
  "sink_node (Root [(n, s)]) = n"
  "sink_store (Root [(n, s)]) = s"
  "sink_node (Call c [(n, s)]) = n"
  "sink_store (Call c [(n, s)]) = s"
  by (simp_all add: sink_node_def sink_store_def)

text ‹The lemmas up to the caller-chain closure all speak about the traces of one graph
  from one set of initial stores, so the block fixes ‹𝒢›, ‹g› and ‹S› and writes
  ‹𝒯› for ‹𝒯⇘𝒢,g,S⇙›.  Outside the block every lemma holds
  for arbitrary ‹𝒢›, ‹g› and ‹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 ("𝒯")

lemma valid_activation_trace_path_nonempty:
  "t ∈ 𝒯 ⟹ path_of t ≠ []"
  by (induction t rule: valid_activation_trace.induct) auto

lemma entry_store_extend [simp]:
  assumes "path_of t ≠ []"
  shows "entry_store (extend t x) = entry_store t"
  using assms by (simp add: entry_store_def)

subsection ‹Design invariants›

text ‹A valid \<^const>‹Call› activation has a valid caller, even after intra steps have
  extended its local path.›
lemma valid_activation_trace_Call_caller_valid:
  "u ∈ 𝒯 ⟹ u = Call cc q ⟹ cc ∈ 𝒯"
proof (induction arbitrary: cc q rule: valid_activation_trace.induct)
  case (intra t a v s')
  from intra.prems obtain q' where "t = Call cc q'"
    by (cases t) auto
  then show ?case using intra.IH by simp
qed auto

text ‹A valid \<^const>‹Resume› retains its callee as a valid activation trace, and its frozen caller is
  forced to be exactly ‹caller_of callee› --- a return cannot invent a caller.›
lemma valid_activation_trace_Resume_fields:
  "u ∈ 𝒯 ⟹ u = Resume cc dd q
   ⟹ dd ∈ 𝒯 ∧ caller_of dd = Some cc"
proof (induction arbitrary: cc dd q rule: valid_activation_trace.induct)
  case (intra t a v s')
  from intra.prems obtain q' where "t = Resume cc dd q'"
    by (cases t) auto
  then show ?case using intra.IH by simp
qed auto

text ‹Every caller recovered from a valid activation trace by \<^const>‹caller_of› is itself valid.›
lemma valid_activation_trace_caller_valid:
  "t ∈ 𝒯 ⟹ caller_of t = Some c ⟹ c ∈ 𝒯"
proof (induction t arbitrary: c)
  case (Root x)
  then show ?case by simp
next
  case (Call caller p)
  have "caller ∈ 𝒯"
    using valid_activation_trace_Call_caller_valid[OF Call.prems(1) refl] .
  with Call.prems(2) show ?case by simp
next
  case (Resume caller callee p)
  from valid_activation_trace_Resume_fields[OF Resume.prems(1) refl]
  have cd: "callee ∈ 𝒯" "caller_of callee = Some caller" by auto
  have cv: "caller ∈ 𝒯" using Resume.IH(2)[OF cd(1)] cd(2) by simp
  from Resume.prems(2) have "caller_of caller = Some c" by simp
  then show ?case using Resume.IH(1)[OF cv] by simp
qed

text ‹A \<^const>‹Root› activation starts at \<^const>‹cfg_entry›: ‹root› creates it there and
  ‹intra› only appends.›
lemma valid_activation_trace_Root_entry:
  "u ∈ 𝒯 ⟹ u = Root p ⟹ fst (hd p) = cfg_entry g"
proof (induction arbitrary: p rule: valid_activation_trace.induct)
  case (intra t a v s')
  from intra.prems obtain p' where t: "t = Root p'" and p: "p = p' @ [(v, s')]"
    by (cases t) auto
  have "fst (hd p') = cfg_entry g" using intra.IH[OF t] .
  moreover have "p' ≠ []" using valid_activation_trace_path_nonempty[OF intra.hyps(1)] t by simp
  ultimately show ?case using p by simp
qed auto

text ‹A \<^const>‹Resume› extends its caller's own local path, so both share a head node.›
lemma valid_activation_trace_Resume_path:
  "u ∈ 𝒯 ⟹ u = Resume cc dd q ⟹ ∃xs. q = path_of cc @ xs ∧ xs ≠ []"
proof (induction arbitrary: cc dd q rule: valid_activation_trace.induct)
  case (intra t a v s')
  from intra.prems obtain q' where t: "t = Resume cc dd q'" and q: "q = q' @ [(v, s')]"
    by (cases t) auto
  from intra.IH[OF t] obtain xs where "q' = path_of cc @ xs" by blast
  then show ?case using q by auto
qed auto

text ‹A callerless activation is the root one, and its local \<^const>‹path_of› starts at
  \<^const>‹cfg_entry›.  The \<^const>‹Resume› case needs the caller's own entry, which term
  induction supplies (the caller is a subterm) --- rule induction would only offer the callee.›
lemma valid_activation_trace_caller_None_entry:
  "t ∈ 𝒯 ⟹ caller_of t = None ⟹ fst (hd (path_of t)) = cfg_entry g"
proof (induction t)
  case (Root p)
  then show ?case using valid_activation_trace_Root_entry[OF Root.prems(1) refl] by simp
next
  case (Call caller p)
  then show ?case by simp
next
  case (Resume caller callee q)
  from valid_activation_trace_Resume_fields[OF Resume.prems(1) refl]
  have cd: "callee ∈ 𝒯" "caller_of callee = Some caller" by auto
  have cv: "caller ∈ 𝒯" using Resume.IH(2)[OF cd(1)] cd(2)
    using valid_activation_trace_caller_valid[OF cd(1) cd(2)] by simp
  from Resume.prems(2) have "caller_of caller = None" by simp
  with Resume.IH(1)[OF cv] have hcaller: "fst (hd (path_of caller)) = cfg_entry g" by simp
  from valid_activation_trace_Resume_path[OF Resume.prems(1) refl] obtain xs where
    q: "q = path_of caller @ xs" by blast
  show ?case using hcaller q valid_activation_trace_path_nonempty[OF cv] by simp
qed

subsection ‹Caller ancestry›

text ‹‹ancestors t› is the \<^const>‹caller_of› chain above ‹t›; ‹callers t› adds ‹t›
  itself and is the set a caller-chain invariant ranges over.›
fun ancestors :: "activation_trace ⇒ activation_trace set" where
  "ancestors (Root _) = {}"
| "ancestors (Call caller _) = insert caller (ancestors caller)"
| "ancestors (Resume current _ _) = ancestors current"

abbreviation callers :: "activation_trace ⇒ activation_trace set" where
  "callers t ≡ insert t (ancestors t)"

lemma ancestors_extend [simp]: "ancestors (extend t x) = ancestors t"
  by (cases t) simp_all

lemma callers_refl: "t ∈ callers t"
  by simp

lemma ancestors_caller: "caller_of t = Some c ⟹ callers c ⊆ ancestors t"
  by (induction t) auto

lemma callers_caller_subset: "caller_of t = Some c ⟹ callers c ⊆ callers t"
  using ancestors_caller by blast

subsection ‹Generic caller-chain closure›

text ‹
  A caller-chain-quantified predicate ‹P› holds along the whole \<^const>‹callers› chain of
  every valid activation trace once its four ‹valid_activation_trace› obligations are discharged.  Each obligation
  reads its own generating trace's induction hypothesis as the whole-chain fact
  ‹∀u ∈ callers _. P u›, not a single-node fact --- this is exactly what ‹ret› needs to
  recover its caller's own chain fact from the callee's.
›

lemma caller_chain_closure:
  fixes P :: "activation_trace ⇒ bool"
  assumes Root: "⋀s. s ∈ S ⟹ P (Root [(cfg_entry g, s)])"
    and Intra: "⋀t a v s'. t ∈ 𝒯 ⟹ (∀u ∈ callers t. P u)
        ⟹ (sink_node t, a, v) ∈ intra g ⟹ s' ∈ edge_step a (sink_store t)
        ⟹ P (extend t (v, s'))"
    and Call: "⋀caller dst pars args p cont. caller ∈ 𝒯
        ⟹ (∀u ∈ callers caller. P u)
        ⟹ (sink_node caller, CallEdge dst pars args, FunctionEntry p, cont)
           ∈ calls g
        ⟹ P (Call caller
                 [(FunctionEntry p, call_enter 𝒢 (CallEdge dst pars args) (sink_store caller))])"
    and Ret: "⋀callee caller p dst pars args cont. callee ∈ 𝒯
        ⟹ (∀u ∈ callers callee. P u)
        ⟹ caller_of callee = Some caller ⟹ sink_node callee = FunctionResult p
        ⟹ (sink_node caller, CallEdge dst pars args, FunctionEntry p, cont)
           ∈ calls g
        ⟹ P (Resume caller callee (path_of caller
                 @ [(cont, combine_collect 𝒢 dst (sink_store caller) (sink_store callee))]))"
  shows "t ∈ 𝒯 ⟹ ∀u ∈ callers t. P u"
proof (induction rule: valid_activation_trace.induct)
  case (root s)
  then show ?case using Root[OF root] by simp
next
  case (intra t a v s')
  then show ?case using Intra[OF intra.hyps(1) intra.IH intra.hyps(2,3)] by auto
next
  case (call caller dst pars args p cont)
  then show ?case using Call[OF call.hyps(1) call.IH call.hyps(2)] by auto
next
  case (ret callee caller p dst pars args cont)
  then show ?case
    using Ret[OF ret.hyps(1) ret.IH ret.hyps(2,3,4)] ancestors_caller[OF ret.hyps(2)] by auto
qed

end

subsection ‹Stable context entry invariant›

text ‹An activation's entry store is fixed once it starts: a call names the store the callee
  begins with, and resuming a caller keeps the caller's own first store rather than adopting
  the callee's.  Context policies that read the entry store rely on this -- otherwise the
  context a trace carries could change under it as the trace grows.›
definition call_enter_store :: "(vname ⇒ bool) ⇒ cfg ⇒ cfg_node ⇒ store ⇒ store ⇒ bool" where
  "call_enter_store 𝒢 g c s t ⟷
     (∃dst pars args p cont. (c, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
        ∧ t = call_enter 𝒢 (CallEdge dst pars args) s)"

lemma entry_store_Resume_caller:
  "path_of caller ≠ [] ⟹
     entry_store (Resume caller callee (path_of caller @ [x])) = entry_store caller"
  by (simp add: entry_store_def hd_append)

end