Theory CFG_Exec

theory CFG_Exec
  imports CFG_Transfer
begin

section ‹How a control-flow graph runs›

text ‹
  ‹cstep› executes an arbitrary CFG over a node, a store, and a stack of suspended
  activations.  Each ‹cframe› records where to resume, which variable receives the
  result, and the caller's store.  There are three rules, one per graph phenomenon:
  follow an ‹intra› edge and apply its transfer; follow a ‹calls› edge, enter the callee
  and push a frame; at a \<^term>‹FunctionResult›, pop the top frame and combine the
  callee's store into the caller's.

  A return follows no edge.  The stack supplies the continuation, so one
  \<^term>‹FunctionResult› node serves every caller of a procedure and recursion needs no
  duplicated nodes.  Nothing here mentions the compiler: this is the execution of any
  graph, just as ‹valid_activation_trace› is the activation-trace semantics of any graph.
›
type_synonym cframe = "cfg_node × vname option × store"
type_synonym cconf = "cfg_node × store × cframe list"

inductive cstep :: "(vname ⇒ bool) ⇒ cfg ⇒ cconf ⇒ cconf ⇒ bool"
    ("(_,_ ⊢/ _ →⇩c/ _)" [51, 51, 51, 51] 50) for 𝒢 and g where
  Intra [intro]:
    "(u, a, v) ∈ intra g ⟹ s' ∈ edge_step a s ⟹
     𝒢, g ⊢ (u, s, stk) →⇩c (v, s', stk)"
| Call [intro]:
    "(u, CallEdge dst pars actuals, FunctionEntry q, cont) ∈ calls g ⟹
     𝒢, g ⊢ (u, s, stk)
       →⇩c (FunctionEntry q, call_enter 𝒢 (CallEdge dst pars actuals) s, (cont, dst, s) # stk)"
| Return [intro]:
    "𝒢, g ⊢ (FunctionResult q, t, (cont, dst, caller) # stk)
       →⇩c (cont, combine_collect 𝒢 dst caller t, stk)"


abbreviation csteps :: "(vname ⇒ bool) ⇒ cfg ⇒ cconf ⇒ cconf ⇒ bool"
    ("(_,_ ⊢/ _ →⇩c⇧*/ _)" [51, 51, 51, 51] 50)
  where "csteps 𝒢 g x y ≡ star (cstep 𝒢 g) x y"

text ‹One inversion rule, because the three clauses are told apart by the edge taken rather
  than by the shape of the configuration.  It stays plain ‹[elim]› so the classical reasoner
  does not split every ‹cstep› hypothesis three ways before trying anything else.›
inductive_cases cstep_E [elim]: "𝒢, g ⊢ (u, s, stk) →⇩c y"

subsection ‹Single-step and small-step lemmas›

text ‹
  Introduction lemmas for the store-preserving edge actions the simulation steps
  through: body, assume and assume-not.
›

lemma cstep_body:
  assumes "(u, EA_Body p, v) ∈ intra g"
  shows "𝒢, g ⊢ (u, s, stk) →⇩c (v, s, stk)"
  by (rule cstep.Intra[OF assms]) simp

lemma cstep_assume:
  assumes "(u, EA_Assume b, v) ∈ intra g" and "truthy (⟦b⟧⇩e s)"
  shows "𝒢, g ⊢ (u, s, stk) →⇩c (v, s, stk)"
  by (rule cstep.Intra[OF assms(1)]) (use assms(2) in simp)

lemma cstep_assume_not:
  assumes "(u, EA_AssumeNot b, v) ∈ intra g" and "¬ truthy (⟦b⟧⇩e s)"
  shows "𝒢, g ⊢ (u, s, stk) →⇩c (v, s, stk)"
  by (rule cstep.Intra[OF assms(1)]) (use assms(2) in simp)

subsection ‹Intra-only paths as stack-preserving runs›

text ‹An \<^const>‹intra_path› is a ‹cstep› run at any stack: every \<^const>‹cfg_intra_step› is a
  ‹cstep.Intra›, which passes the stack through untouched.  Callers that only need to move
  along local edges can therefore reason on ‹(node, store)› pairs and lift the result here.›
lemma intra_path_imp_cstep_star:
  "intra_path g x y ⟹ 𝒢, g ⊢ (fst x, snd x, stk) →⇩c⇧* (fst y, snd y, stk)"
proof (induction rule: star.induct)
  case (refl a) show ?case by simp
next
  case (step a b c)
  obtain ua sa where a: "a = (ua, sa)" by (cases a)
  obtain ub sb where b: "b = (ub, sb)" by (cases b)
  from step.hyps(1) a b obtain e where "(ua, e, ub) ∈ intra g" "sb ∈ edge_step e sa" by auto
  hence "𝒢, g ⊢ (ua, sa, stk) →⇩c (ub, sb, stk)" by (rule cstep.Intra)
  with step.IH a b show ?case by (auto intro: star.step)
qed

subsection ‹Activation-stack matching›

text ‹Both stacks record procedure activations.  ‹act_frames› removes the CFG-only
  continuation component and retains the caller store and destination used by the source.›

fun act_frames :: "frame list ⇒ (store × vname option) list" where
  "act_frames [] = []"
| "act_frames (Frame s d # frs) = (s, d) # act_frames frs"

definition cframe_act :: "cframe ⇒ store × vname option" where
  "cframe_act cf = (case cf of (cont, d, s) ⇒ (s, d))"

text ‹‹frames_match› ties a source frame stack to a CFG activation stack: the activation
  frames agree, in order, on caller store and destination (the continuation node is the CFG's
  own bookkeeping and is not visible to the source).›
definition frames_match :: "frame list ⇒ cframe list ⇒ bool" where
  "frames_match frs stk = (act_frames frs = map cframe_act stk)"

lemma frames_match_Nil [simp]: "frames_match [] []"
  by (simp add: frames_match_def)

text ‹An activation frame matches the top CFG activation on caller store and destination.›
lemma frames_match_activation:
  "frames_match (Frame s d # frs) ((cont, d, s) # stk)
     = frames_match frs stk"
  by (simp add: frames_match_def cframe_act_def)

end