Theory Simulation_Relation

theory Simulation_Relation
  imports Residual_Edges
begin

section ‹What it means for a source state and a graph state to agree›

text ‹
  ‹csim› relates a source configuration \<^term>‹(c, s, frs)› to a CFG configuration
  \<^term>‹(v, s, stk)› holding the very same store.  The two represent suspended callers
  differently: the source nests each caller's continuation inside the single command ‹c›,
  as \<^term>‹Seq (Seq inner (Restore i)) after› wrappings, while the CFG keeps them as
  continuation nodes on its frame stack.  ‹csim› pairs the two off, one layer per
  suspended caller.

  Both nestings run outermost-first, so the top command layer pairs with the last frame.
  After ‹main› calls ‹f› calls ‹g› the source command is
  ‹Seq (Seq (Seq (Seq C Restore) B) Restore) A› --- ‹A› is main's continuation and ‹C› the
  running residual of ‹g› --- while the CFG sits at ‹g›'s node with continuation frames
  ‹[B's node, A's node]›.

  Three constructors, one per phase an activation can be in.  ‹Base› relates a single
  activation with nothing beneath it.  ‹Nested› peels one suspended caller.  ‹Returning›
  covers the skew just after a callee finishes: the CFG has already reached
  \<^term>‹FunctionResult p›, while the source is still propagating \<^const>‹Restore› or
  \<^const>‹Unwind› towards its frame-pop rule.  Proving that execution preserves ‹csim› is
  the next theory's business; this one defines the relation and the vocabulary it is
  stated in.
›

subsection ‹Return-store update›

text ‹The store published by a return, common to the source \<^const>‹Return› step and the
  compiled \<^term>‹EA_Ret› edge.›
definition ret_store :: "exp option ⇒ store ⇒ store" where
  "ret_store e s = s(ret_var := (case e of None ⇒ s ret_var | Some a ⇒ ⟦a⟧⇩e s))"

lemma ret_store_None [simp]: "ret_store None s = s"
  by (simp add: ret_store_def)

lemma ret_store_Some [simp]: "ret_store (Some e) s = s(ret_var := ⟦e⟧⇩e s)"
  by (simp add: ret_store_def)

lemma edge_step_EA_Ret_ret_store_mem [simp]: "ret_store e s ∈ edge_step (EA_Ret e p) s"
  by (simp add: ret_store_def)

subsection ‹Bare Unwind is stuck›

text ‹A lone \<^const>‹Unwind› has no source step: only the \<^const>‹Seq› rules propagate it, and
  the frame pop it is heading for fires on \<^term>‹Seq (Unwind j) (Restore i)›.›
lemma pstep_Unwind_stuck: "¬ 𝒢, Π ⊢ (Unwind i, s, frs) →⇩p x"
  by auto

text ‹
  Why a top-level ‹Return› must not reach the source: an empty frame stack has
  nowhere to unwind to, so a run that starts at ‹Unwind› or ‹Return› never completes.
›

lemma Unwind_not_pcompletes: "¬ pcompletes 𝒢 Π (Unwind ()) s t"
proof (rule notI)
  assume "𝒢, Π ⊢ (Unwind (), s, []) →⇩p⇧* (SKIP (), t, [])"
  then show False
    by (cases rule: star.cases) (auto simp: pstep_Unwind_stuck)
qed

lemma Return_empty_not_pcompletes: "¬ pcompletes 𝒢 Π (Return () e) s t"
proof (rule notI)
  assume "𝒢, Π ⊢ (Return () e, s, []) →⇩p⇧* (SKIP (), t, [])"
  then obtain y where step: "𝒢, Π ⊢ (Return () e, s, []) →⇩p y"
      and rest: "𝒢, Π ⊢ y →⇩p⇧* (SKIP (), t, [])"
    by (cases rule: star.cases) auto
  from step have "y = (Unwind (), ret_store e s, [])"
    by (cases e) (auto simp: ret_store_def)
  with rest have "𝒢, Π ⊢ (Unwind (), ret_store e s, []) →⇩p⇧* (SKIP (), t, [])" by simp
  then show False
    by (cases rule: star.cases) (auto simp: pstep_Unwind_stuck)
qed

subsection ‹The returning (frame-pop) source shapes›

text ‹
  Once a callee finishes, the CFG is already at \<^term>‹FunctionResult p› while the source
  propagates toward the frame-pop rule.  ‹unwinding› describes an \<^const>‹Unwind› travelling
  up through the callee's residual, dropping the dead code it skips (never the activation's
  own \<^const>‹Restore›); ‹pop_ready› describes the whole activation body in that phase ---
  either the normal fall-through \<^const>‹Restore› or an \<^const>‹Unwind› spine
  ‹Seq u Restore› from an explicit \<^const>‹Return›.  Both pop the single caller frame with one
  ‹cstep› return; ‹unwinding› propagation is matched by ∗‹no› CFG step, because the CFG
  waits at \<^term>‹FunctionResult p›.
›
fun unwinding :: "'a acom ⇒ bool" where
  "unwinding (Unwind i) = True"
| "unwinding (Seq u c2) = (unwinding u ∧ ¬ is_Restore c2)"
| "unwinding _ = False"

fun pop_ready :: "'a acom ⇒ bool" where
  "pop_ready (Restore i) = True"
| "pop_ready (Seq u (Restore i)) = unwinding u"
| "pop_ready _ = False"

text ‹The annotation of the \<^const>‹Restore› a returning activation pops: the call it
  came from, which is also the annotation of the \<^const>‹SKIP› the pop leaves behind.›
fun pop_ann :: "'a acom ⇒ 'a option" where
  "pop_ann (Restore i) = Some i"
| "pop_ann (Seq u (Restore i)) = Some i"
| "pop_ann _ = None"

lemma unwinding_not_SKIP: "unwinding u ⟹ ¬ is_SKIP u"
  by (cases u) auto

lemma pop_ready_not_SKIP: "pop_ready w ⟹ ¬ is_SKIP w"
  by (cases w rule: pop_ready.cases) auto

lemma pop_ready_not_Unwind: "pop_ready w ⟹ w ≠ Unwind i"
  by (cases w rule: pop_ready.cases) auto

subsection ‹Compile-into-‹g› evidence for an active fragment›

text ‹
  ‹compiled_at Π g p body_p k n› is an activation's certificate.  It says two things at once,
  because every activation needs both: ‹body_p› is genuinely procedure ‹p›'s body, and that body,
  compiled at the exact offset ‹n› with continuation ‹k›, is embedded in the target graph
  ‹g› --- its intra edges lie in \<^term>‹intra g› and its call edges in \<^term>‹calls g›.

  The offset matters because compilation is shift-parametric: neither ‹n› nor ‹k› is fixed by
  the syntax, so graph membership ∗‹at the chosen offset› is the missing fact and this
  predicate supplies it, at the same ‹k› and ‹n› that \<^const>‹control_at› uses.  The procedure
  identity matters because \<^const>‹control_at›'s fragment parameter is otherwise free, and
  fall-through preservation is false for a fragment that is not a whole body.

  A procedure body's continuation is its epilogue node, which is why the fall-through return
  edge is stated from ‹k›.  \<^const>‹compile_proc› emits that edge for every body.

  The offset itself is anchored to the graph: the body enters at the target of ‹p›'s
  \<^term>‹EA_Body› edge, and ‹k› is the epilogue right after the body.  Without the anchor the
  body's edges could be matched at a shifted offset, and the relation would locate a residual
  at a node no execution of ‹p› uses.
›
definition compiled_at ::
  "'a ptable ⇒ cfg ⇒ pname ⇒ 'a acom ⇒ cfg_node ⇒ nat ⇒ bool" where
  "compiled_at Π g p body_p k n ⟷
     (∃decl n' en E K. Π p = Some decl ∧ body_p = body decl
        ∧ compile Π p body_p k n = (n', en, E, K)
        ∧ E ⊆ intra g ∧ K ⊆ calls g
        ∧ (k, EA_Ret None p, FunctionResult p) ∈ intra g
        ∧ (FunctionEntry p, EA_Body p, Statement n) ∈ intra g
        ∧ k = Statement (n + csize body_p))"

lemma compiled_atI [intro]:
  "Π p = Some decl ⟹ body_p = body decl ⟹
   compile Π p body_p k n = (n', en, E, K) ⟹ E ⊆ intra g ⟹ K ⊆ calls g ⟹
   (k, EA_Ret None p, FunctionResult p) ∈ intra g ⟹
   (FunctionEntry p, EA_Body p, Statement n) ∈ intra g ⟹ k = Statement (n + csize body_p) ⟹
   compiled_at Π g p body_p k n"
  unfolding compiled_at_def by blast

lemma compiled_atE [elim]:
  assumes "compiled_at Π g p body_p k n"
  obtains decl n' en E K where
    "Π p = Some decl" "body_p = body decl"
    "compile Π p body_p k n = (n', en, E, K)" "E ⊆ intra g" "K ⊆ calls g"
    "(k, EA_Ret None p, FunctionResult p) ∈ intra g"
  using assms unfolding compiled_at_def by blast

text ‹The procedure-identity half on its own, for the many proofs that only need the
  declaration behind an activation.›
lemma compiled_at_decl:
  assumes "compiled_at Π g p body_p k n"
  obtains decl where "Π p = Some decl" "body_p = body decl"
  using assms unfolding compiled_at_def by blast

lemma compiled_at_exit:
  "compiled_at Π g p body_p k n ⟹ (k, EA_Ret None p, FunctionResult p) ∈ intra g"
  unfolding compiled_at_def by auto

subsection ‹The simulation relation›

text ‹What it means for a source configuration and a graph configuration to be at the same
  place.  Three shapes, one per stack situation: a single activation, a call in progress with
  the caller recorded on both stacks, and the moment between a return and the frame pop.  All
  three carry the same store, so the relation constrains position and stack only.

  The index ‹p› in ‹Π, g, p ⊢ cfg ≈ dg› is the procedure of the outermost activation of
  ‹cfg›, the one with no caller below it in the relation.  ‹Nested› and ‹Returning› record the
  call that suspended that activation, \<^term>‹Call i dst q args›: the activation inside
  \<^term>‹Seq inner (Restore i)› runs ‹q›, and a returning activation is at \<^term>‹FunctionResult q›
  of that same ‹q›.  Recursion is harmless because the index belongs to an activation, not to a
  body.›
inductive csim :: "'a ptable ⇒ cfg ⇒ pname ⇒ 'a acom × store × frame list
                    ⇒ cfg_node × store × cframe list ⇒ bool"
    ("(_,_,_ ⊢/ _ ≈/ _)" [51, 51, 51, 51, 51] 50) for Π g where
  Base:
    "control_at Π p body_p k n c v ⟹ compiled_at Π g p body_p k n ⟹
     Π, g, p ⊢ (c, s, []) ≈ (v, s, [])"
| Nested:
    "Π, g, q ⊢ (inner, s, frs) ≈ (v, s, stk) ⟹
     control_at Π pc body_pc kc nc (seq_after (SKIP i) afters) cont ⟹
     control_at Π pc body_pc kc nc (seq_after (Call i dst q args) afters) site ⟹
     compiled_at Π g pc body_pc kc nc ⟹
     Π, g, pc ⊢ (seq_after (Seq inner (Restore i)) afters, s, frs @ [Frame caller dst])
       ≈ (v, s, stk @ [(cont, dst, caller)])"
| Returning:
    "pop_ready w ⟹ pop_ann w = Some i ⟹
     control_at Π pc body_pc kc nc (seq_after (SKIP i) afters) cont ⟹
     control_at Π pc body_pc kc nc (seq_after (Call i dst q args) afters) site ⟹
     compiled_at Π g pc body_pc kc nc ⟹
     Π, g, pc ⊢ (seq_after w afters, callee, [Frame caller dst])
       ≈ (FunctionResult q, callee, [(cont, dst, caller)])"
text ‹
  On its own \<^const>‹csim› is a ∗‹structural› correspondence, not a reachability one.  For an
  unannotated program it is not functional either: a residual carries no record of which
  occurrence it came from, so two textually equal statements share every location.  A caller
  that needs the semantic node pairs it with membership in ‹node_collect› at the same node.
  Annotated programs whose annotations are the compiler's own locations are the case where the
  node is determined.
›

text ‹Inversion at an empty source frame stack.  Only ‹Base› can produce one --- ‹Nested› and
  ‹Returning› both append a caller frame --- so the CFG stack is empty too, the stores agree,
  and the whole activation certificate comes back.  ‹csim›'s introduction rules stay
  undeclared: choosing between ‹Base›, ‹Nested› and ‹Returning› is the step each preservation
  proof exists to make, and it belongs in the proof text rather than in a search.›
inductive_cases csim_empty_stackE [elim]: "Π, g, p ⊢ (c, s, []) ≈ (v, t, stk)"

text ‹‹Nested› and ‹Returning› both locate the ∗‹resumed caller› --- the ordinary residual
  \<^term>‹seq_after (SKIP i) afters› that the return will land in --- at the continuation node
  ‹cont›.  ‹Returning› carries exactly the one frame the return pops; outer callers are
  consumed by the ‹Nested› layers wrapping it, and after the pop the caller resumes as a
  ‹Base› activation with that wrapping untouched.›

lemma csim_store_eq:
  "Π, g, ρ ⊢ (c, s, frs) ≈ (v, t, stk) ⟹ s = t"
  by (induction "(c, s, frs)" "(v, t, stk)" arbitrary: c frs v stk rule: csim.induct) auto

subsection ‹Returning commands and the frame-pop phase›

text ‹‹is_returning c› holds when the leftmost-innermost of ‹c› is \<^const>‹Restore› or
  \<^const>‹Unwind›: the shape of every returning-phase command, ordinary or ‹Nested›-wrapped.›
fun is_returning :: "'a acom ⇒ bool" where
  "is_returning (Restore i) = True"
| "is_returning (Unwind i) = True"
| "is_returning (Seq c1 c2) = is_returning c1"
| "is_returning _ = False"

lemma is_returning_seq_after [simp]:
  "is_returning (seq_after c afters) = is_returning c"
  by (induction afters arbitrary: c) auto

subsection ‹The call-redex source shape›

text ‹‹head_call c› holds when the leftmost-innermost of ‹c› is a \<^const>‹Call› to a procedure
  \<^const>‹special_table› does not classify: the shape of an active residual whose next
  \<^const>‹pstep› pushes a frame.  A call \<^const>‹special_table› classifies resolves in place
  instead (\<^const>‹intra_step›'s ‹ISpecial›), so it is deliberately excluded here, mirroring
  \<^const>‹intra_step›'s own exclusion of \<^const>‹Call›.›
fun head_call :: "'a acom ⇒ bool" where
  "head_call (Call i dst q actuals) = (special_table q = None)"
| "head_call (Seq c1 c2) = head_call c1"
| "head_call _ = False"

lemma head_call_seq_after [simp]:
  "head_call (seq_after c afters) = head_call c"
  by (induction afters arbitrary: c) auto

lemma head_call_not_SKIP: "head_call c ⟹ ¬ is_SKIP c"
  by (cases c) auto

lemma head_call_not_Unwind: "head_call c ⟹ c ≠ Unwind i"
  by (cases c) auto

lemma head_call_seq_after_form:
  "head_call c ⟹ ∃i dst q actuals afters.
     c = seq_after (Call i dst q actuals) afters ∧ special_table q = None"
proof (induction c)
  case (Seq c1 c2)
  from Seq.prems have "head_call c1" by simp
  from Seq.IH(1)[OF this] obtain i dst q actuals afters where
    "c1 = seq_after (Call i dst q actuals) afters" "special_table q = None" by blast
  then have "Seq c1 c2 = seq_after (Call i dst q actuals) (afters @ [c2])"
             "special_table q = None"
    by (simp_all add: seq_after_snoc)
  then show ?case by blast
qed auto

lemma unwinding_not_head_call: "unwinding u ⟹ ¬ head_call u"
  by (induction u rule: unwinding.induct) auto

lemma pop_ready_not_head_call: "pop_ready w ⟹ ¬ head_call w"
  by (cases w rule: pop_ready.cases) (auto simp: unwinding_not_head_call)

subsection ‹The return-initiation source shape›

text ‹‹head_return c› holds when the leftmost-innermost of ‹c› is a source \<^const>‹Return›:
  the shape whose next \<^const>‹pstep› initiates a return.›
fun head_return :: "'a acom ⇒ bool" where
  "head_return (Return i e) = True"
| "head_return (Seq c1 c2) = head_return c1"
| "head_return _ = False"

lemma head_return_seq_after [simp]:
  "head_return (seq_after c afters) = head_return c"
  by (induction afters arbitrary: c) auto

lemma head_return_not_SKIP: "head_return c ⟹ ¬ is_SKIP c"
  by (cases c) auto

lemma head_return_seq_after_form:
  "head_return c ⟹ ∃i e afters. c = seq_after (Return i e) afters"
proof (induction c)
  case (Seq c1 c2)
  from Seq.prems have "head_return c1" by simp
  from Seq.IH(1)[OF this] obtain i e afters where "c1 = seq_after (Return i e) afters" by blast
  then have "Seq c1 c2 = seq_after (Return i e) (afters @ [c2])" by (simp add: seq_after_snoc)
  then show ?case by blast
qed auto

lemma unwinding_not_head_return: "unwinding u ⟹ ¬ head_return u"
  by (induction u rule: unwinding.induct) auto

lemma pop_ready_not_head_return: "pop_ready w ⟹ ¬ head_return w"
  by (cases w rule: pop_ready.cases) (auto simp: unwinding_not_head_return)

subsection ‹Source well-formedness: the base-activation return guard›

text ‹‹ret_guarded allow_return c› is the deep source-only well-formedness check: an explicit
  \<^const>‹Return› (or an in-flight \<^const>‹Unwind›) is admissible only where ‹allow_return›
  holds --- inside a called activation.  Permission is ∗‹granted by the activation tail›: the
  right child \<^const>‹Restore› of a \<^const>‹Seq› marks a callee body, so its left child is
  checked with ‹allow_return = True›, whereas ordinary continuations inherit the ambient
  permission.  A bare \<^const>‹Restore› (the transient tail after the callee body reduces to
  \<^const>‹SKIP›) is always admissible.  Crucially this looks ∗‹behind› \<^const>‹Restore›
  boundaries: a \<^const>‹Return› hidden in a base-activation continuation is rejected, which a
  head-only check misses --- exactly the configuration a frame pop would later surface at the
  base.›
fun ret_guarded :: "bool ⇒ 'a acom ⇒ bool" where
  "ret_guarded allow_return (SKIP i) = True"
| "ret_guarded allow_return (Assign i x a) = True"
| "ret_guarded allow_return (VIMP_Proc.gcom.Check i l b) = True"
| "ret_guarded allow_return (Seq c1 c2) =
     (if is_Restore c2 then ret_guarded True c1
      else ret_guarded allow_return c1 ∧ ret_guarded allow_return c2)"
| "ret_guarded allow_return (If i b c1 c2) =
     (ret_guarded allow_return c1 ∧ ret_guarded allow_return c2)"
| "ret_guarded allow_return (While i b c) = ret_guarded allow_return c"
| "ret_guarded allow_return (Call i dst p actuals) = True"
| "ret_guarded allow_return (Return i e) = allow_return"
| "ret_guarded allow_return (Restore i) = True"
| "ret_guarded allow_return (Unwind i) = allow_return"

lemma ret_guarded_True_source: "source_com c ⟹ ret_guarded True c"
  by (induction c) (auto split: if_splits)

lemma ret_guarded_False_source_not_head_return:
  "source_com c ⟹ ret_guarded False c ⟹ ¬ head_return c"
  by (induction c) (auto split: if_splits)

lemma ret_guarded_pstep:
  assumes bodies: "⋀p decl. Π p = Some decl ⟹ source_com (body decl)"
      and step: "𝒢, Π ⊢ (c, s, frs) →⇩p (c', s', frs')"
      and "ret_guarded allow_return c"
  shows "ret_guarded allow_return c'"
  using step assms(3)
proof (induction "(c, s, frs)" "(c', s', frs')"
       arbitrary: c s frs c' s' frs' allow_return rule: pstep.induct)
  case Call
  then show ?case using bodies ret_guarded_True_source by auto
next
  case (Seq2 c1 s1 f1 c1' s1' f1' c2)
  then show ?case by (auto split: if_splits)
qed (auto split: if_splits)

text ‹The runtime invariant ‹csim_step› asks for: the active command may not return until a
  call has opened an activation for it.  Only the command matters --- neither the store nor
  the frame stack --- and unlike a head-only guard this survives a \<^const>‹pstep›, because it
  already forbids the base-activation returns that a frame pop would expose.›
definition return_safe :: "'a acom ⇒ bool" where
  "return_safe c ⟷ ret_guarded False c"

lemma return_safe_if_no_return:
  assumes "source_com c" and "no_return c"
  shows "return_safe c"
  using assms
  unfolding return_safe_def
  by (induction c) (auto split: if_splits)

lemma return_safe_not_head_return:
  "return_safe c ⟹ source_com c ⟹ ¬ head_return c"
  by (auto simp: return_safe_def ret_guarded_False_source_not_head_return)

lemma return_safe_pstep:
  assumes bodies: "⋀p decl. Π p = Some decl ⟹ source_com (body decl)"
      and step: "𝒢, Π ⊢ (c, s, frs) →⇩p (c', s', frs')"
      and wf: "return_safe c"
  shows "return_safe c'"
  using ret_guarded_pstep[OF bodies step] wf by (simp add: return_safe_def)

lemma unwinding_seq_after_Unwind:
  "(∀a ∈ set afters. ¬ is_Restore a) ⟹ unwinding (seq_after (Unwind i) afters)"
  by (induction afters rule: rev_induct) (auto simp: seq_after_snoc)

subsection ‹Source-step classification›

text ‹Sorting a source step into the three cases the simulation treats separately: an
  ordinary intra step, a call, or a return in progress.  The classification is what lets each
  preservation proof assume it is in exactly one case rather than re-deriving the exclusions
  from \<^const>‹pstep› every time.›
lemma intra_step_not_returning:
  "intra_step Π (c, s, frs) (c', s', frs') ⟹ ¬ is_returning c"
  by (induction "(c, s, frs)" "(c', s', frs')" arbitrary: c s frs c' s' frs'
      rule: intra_step.induct) auto

text ‹A declared procedure's name is never one \<^const>‹special_table› also classifies: the
  same disjointness ‹procs_embedded› bundles in the next theory, supplied directly since this
  lemma sits upstream of that definition.  Without it the ‹pstep.Call› case cannot rule out
  ‹c› also matching ‹pstep.Special›, which \<^const>‹head_call› excludes.›
lemma pstep_intra_classify:
  assumes disj: "⋀p decl. Π p = Some decl ⟹ special_table p = None"
  shows "𝒢, Π ⊢ (c, s, frs) →⇩p (c', s', frs') ⟹ ¬ head_call c ⟹ ¬ head_return c ⟹
   ¬ is_returning c ⟹ intra_step Π (c, s, frs) (c', s', frs')"
proof (induction "(c, s, frs)" "(c', s', frs')"
       arbitrary: c s frs c' s' frs' rule: pstep.induct)
  case (Seq2 c1 s1 f1 c1' s1' f1' c2)
  from Seq2.prems have "¬ head_call c1" "¬ head_return c1" "¬ is_returning c1" by auto
  from Seq2.hyps(2)[OF this] have ih: "intra_step Π (c1, s1, f1) (c1', s1', f1')" .
  from intra_step_frame_eq[OF ih] ih show ?case by auto
next
  case (Call i p decl actuals dst vals callee s1 frs0)
  then show ?case using disj by simp
qed auto

lemma control_at_not_returning:
  "control_at Π p c0 k n r v ⟹ ¬ is_returning r"
  by (induction rule: control_at.induct) auto

lemma control_at_not_unwind:
  "control_at Π p c0 k n r v ⟹ r ≠ Unwind i"
  using control_at_not_returning by fastforce

text ‹‹is_returning› classifies the active head.  The ‹unwinding› and ‹pop_ready› predicates
  refine that class with the nested residual shape needed by frame-pop proofs; they
  deliberately overlap instead of forming a phase partition.›
lemma unwinding_is_returning: "unwinding u ⟹ is_returning u"
  by (induction u rule: unwinding.induct) auto

lemma pop_ready_is_returning: "pop_ready w ⟹ is_returning w"
  by (cases w rule: pop_ready.cases) (auto simp: unwinding_is_returning)

lemma is_returning_next_check: "is_returning c ⟹ next_check c = None"
  by (induction c) auto

text ‹A source configuration about to run a check is, under \<^const>‹csim›, at a node
  whose \<^const>‹EA_Check› edge carries that check.  Suspended callers only wrap the
  running residual, and the frame-pop phase runs no check.›
lemma csim_next_check_edge:
  assumes "Π, g, ρ ⊢ (c, s, frs) ≈ (v, t, stk)" and "next_check c = Some (l, e)"
  shows "∃w. (v, EA_Check l e, w) ∈ intra g"
  using assms
proof (induction "(c, s, frs)" "(v, t, stk)" arbitrary: c s frs v t stk rule: csim.induct)
  case (Base p body_p k n c v s)
  from Base.hyps(2) obtain n' en E K
    where "compile Π p body_p k n = (n', en, E, K)" and "E ⊆ intra g"
    by blast
  with control_at_next_check_edge [OF Base.hyps(1) Base.prems] show ?case by blast
next
  case (Returning w i pc body_pc kc nc afters cont callee caller dst p)
  then show ?case by (simp add: is_returning_next_check pop_ready_is_returning)
qed simp

subsection ‹Stepping the frame-pop phase›

text ‹How the phase between a return and its frame pop behaves: it neither changes the store
  nor touches the frames, and it stays in the phase until the pop.  That is what lets the
  simulation hold the graph side still while the source side unwinds.›
lemma pstep_unwinding:
  assumes "unwinding u" and "𝒢, Π ⊢ (u, s, frs) →⇩p (u', s', frs')"
  shows "s' = s ∧ frs' = frs ∧ unwinding u'"
  using assms
proof (induction u arbitrary: u' s' frs')
  case (Seq u1 c2)
  from Seq.prems(1) have u1w: "unwinding u1" and c2R: "¬ is_Restore c2" by auto
  from Seq.prems(2) consider
      (dead) j where "u' = Unwind j" "s' = s" "frs' = frs"
    | (step) c1' where "u' = Seq c1' c2" "𝒢, Π ⊢ (u1, s, frs) →⇩p (c1', s', frs')"
    using c2R unwinding_not_SKIP[OF u1w] by auto
  then show ?case
  proof cases
    case dead then show ?thesis by simp
  next
    case (step c1')
    from Seq.IH(1)[OF u1w step(2)] have "s' = s" "frs' = frs" "unwinding c1'" by simp_all
    then show ?thesis using step(1) c2R by simp
  qed
next
  case SKIP    from SKIP.prems(1)    show ?case by simp
next
  case Assign  from Assign.prems(1)  show ?case by simp
next
  case Check   from Check.prems(1)   show ?case by simp
next
  case If      from If.prems(1)      show ?case by simp
next
  case While   from While.prems(1)   show ?case by simp
next
  case Call    from Call.prems(1)    show ?case by simp
next
  case Return  from Return.prems(1)  show ?case by simp
next
  case Restore from Restore.prems(1) show ?case by simp
next
  case (Unwind i)
  from Unwind.prems(2) show ?case using pstep_Unwind_stuck by blast
qed

lemma pstep_pop_ready_head:
  assumes "pop_ready w" and "pop_ann w = Some i"
      and "𝒢, Π ⊢ (w, s, Frame fr dst # frs) →⇩p x"
  shows "x = (SKIP i, combine_assign dst (s ret_var) (combine_env 𝒢 fr s), frs)
       ∨ (∃w'. x = (w', s, Frame fr dst # frs) ∧ pop_ready w' ∧ pop_ann w' = Some i)"
  using assms
proof (cases w rule: pop_ready.cases)
  case 1
  with assms(2,3) show ?thesis by auto
next
  case (2 u)
  hence uw: "unwinding u" using assms(1) by simp
  from assms(3) show ?thesis
    unfolding 2 using assms(2) unfolding 2
    by (elim SeqSE) (auto dest: pstep_unwinding[OF uw] simp: unwinding_not_SKIP[OF uw])
qed (use assms(1) in auto)

subsection ‹Stepping through a ‹seq_after› spine›

text ‹A step of a \<^const>‹seq_after› spine is a step of its head, with the pending
  continuations carried along untouched.  \<^const>‹SKIP› and \<^const>‹Unwind› heads are excluded
  because those relocate into the spine instead of stepping in place.›
lemma pstep_seq_after_headE [elim]:
  assumes step: "𝒢, Π ⊢ (seq_after w afters, s, frs) →⇩p src'"
      and wsk: "¬ is_SKIP w" and wunw: "⋀i. w ≠ Unwind i"
  obtains h' s' fz where
    "src' = (seq_after h' afters, s', fz)"
    "𝒢, Π ⊢ (w, s, frs) →⇩p (h', s', fz)"
proof -
  have "∃h' s' fz. src' = (seq_after h' afters, s', fz)
          ∧ 𝒢, Π ⊢ (w, s, frs) →⇩p (h', s', fz)"
    using step
  proof (induction afters arbitrary: src' rule: rev_induct)
    case Nil
    then obtain h' s' fz where "src' = (h', s', fz)"
      "𝒢, Π ⊢ (w, s, frs) →⇩p (h', s', fz)"
      by (cases src') auto
    then show ?case by auto
  next
    case (snoc a xs)
    from snoc.prems have "𝒢, Π ⊢ (Seq (seq_after w xs) a, s, frs) →⇩p src'"
      by (simp add: seq_after_snoc)
    then obtain B' s' fz where
      A: "src' = (Seq B' a, s', fz)"
        and B: "𝒢, Π ⊢ (seq_after w xs, s, frs) →⇩p (B', s', fz)"
      using wsk wunw by auto
    from snoc.IH[OF B] obtain h' where
      "B' = seq_after h' xs" "𝒢, Π ⊢ (w, s, frs) →⇩p (h', s', fz)" by auto
    then show ?case using A by (auto simp: seq_after_snoc)
  qed
  then show ?thesis using that by blast
qed

end