Theory Simulation_Preservation

theory Simulation_Preservation
  imports Simulation_Relation Compile_Invariants
begin

section ‹Every source step is matched by the graph›

text ‹
  The result the session exists for: if ‹csim› holds and the source takes one step, the graph
  can follow and ‹csim› holds again (‹csim_step›); hence the same for a whole run
  (‹csim_star›).  A source redex is one of four things --- a call, a return initiation, a
  return already in progress, or an ordinary step inside the activation --- and there is one
  completion theorem per case, which ‹csim_step› dispatches to.

  ‹procs_embedded› is the static side condition every case but the returning phase
  needs: every declared procedure's body has been compiled into this graph, with its entry
  and exit wiring present.
  It is deliberately not part of ‹csim›, which says only how two configurations correspond,
  so that the returning phase can proceed without it.  ‹procs_embedded_compile_prog›
  discharges it for any graph \<^const>‹compile_prog› actually produced.
›

definition procs_embedded :: "'a ptable ⇒ cfg ⇒ bool" where
  "procs_embedded Π g ⟷
     (∀p decl. Π p = Some decl ⟶
        (∃k n n' en E K.
           compile Π p (body decl) k n = (n', en, E, K)
         ∧ E ⊆ intra g ∧ K ⊆ calls g
         ∧ (FunctionEntry p, EA_Body p, en) ∈ intra g
         ∧ (k, EA_Ret None p, FunctionResult p) ∈ intra g
         ∧ k = Statement (n + csize (body decl))
         ∧ source_com (body decl) ∧ special_table p = None))"

lemma procs_embedded_proc:
  assumes "procs_embedded Π g" and "Π p = Some decl"
  obtains k n n' en E K where
    "compile Π p (body decl) k n = (n', en, E, K)"
    "E ⊆ intra g" "K ⊆ calls g"
    "(FunctionEntry p, EA_Body p, en) ∈ intra g"
    "(k, EA_Ret None p, FunctionResult p) ∈ intra g"
    "k = Statement (n + csize (body decl))"
    "source_com (body decl)" "special_table p = None"
  using assms unfolding procs_embedded_def by blast

lemma procs_embedded_source_com:
  assumes "procs_embedded Π g" and "Π p = Some decl"
  shows "source_com (body decl)"
  using assms by (blast elim: procs_embedded_proc)

text ‹A declared procedure's name is never one \<^const>‹special_table› also classifies:
  ‹procs_embedded› bundles this disjointness alongside compiler-correctness so a declared call
  and a special call are always distinguishable without a separate well-formedness premise.›
lemma procs_embedded_special_table_none:
  assumes "procs_embedded Π g" and "Π p = Some decl"
  shows "special_table p = None"
  using assms by (blast elim: procs_embedded_proc)

text ‹Everything needed to start a fresh activation of ‹p›, in one step: the certificate its
  ‹csim› layer will carry, the initial location of its body, and the \<^term>‹EA_Body› edge from
  \<^term>‹FunctionEntry p› that reaches that location.  Call preservation is otherwise the same
  destructuring written out by hand.›
lemma procs_embedded_activation:
  assumes pc: "procs_embedded Π g" and decl: "Π p = Some decl"
  obtains k n en where
    "compiled_at Π g p (body decl) k n"
    "control_at Π p (body decl) k n (body decl) en"
    "(FunctionEntry p, EA_Body p, en) ∈ intra g"
    "source_com (body decl)"
proof -
  obtain k n n' en E K where
    cb: "compile Π p (body decl) k n = (n', en, E, K)"
      and Esub: "E ⊆ intra g" and Ksub: "K ⊆ calls g"
      and entry: "(FunctionEntry p, EA_Body p, en) ∈ intra g"
      and ex: "(k, EA_Ret None p, FunctionResult p) ∈ intra g"
      and kk: "k = Statement (n + csize (body decl))"
      and src: "source_com (body decl)"
      and "special_table p = None"
    by (rule procs_embedded_proc[OF pc decl])
  have entry': "(FunctionEntry p, EA_Body p, Statement n) ∈ intra g"
    using entry compile_entry[OF cb] by simp
  have cacc: "compiled_at Π g p (body decl) k n"
    by (rule compiled_atI[OF decl refl cb Esub Ksub ex entry' kk])
  have ctrl: "control_at Π p (body decl) k n (body decl) en"
    using control_at_initial[OF src, of Π p k n, folded compile_entry[OF cb]] .
  from cacc ctrl entry src show ?thesis by (rule that)
qed

section ‹Frame-stack plumbing›

text ‹A single \<^const>‹pstep› touches only the head region of the frame stack, so a bottom
  segment ‹extra› rides along unchanged when the active part ‹frs› is non-empty.  This
  bridges the ‹Nested› snoc (the inner step threads all frames) to the induction hypothesis
  (stated on the inner frames alone).›
lemma pstep_frame_restrict:
  "𝒢, Π ⊢ (c, s, fr) →⇩p (c', s', frs') ⟹ fr = frs @ extra ⟹ frs ≠ [] ⟹
   ∃frs''. frs' = frs'' @ extra ∧ 𝒢, Π ⊢ (c, s, frs) →⇩p (c', s', frs'')"
proof (induction "(c, s, fr)" "(c', s', frs')"
       arbitrary: c s fr frs c' s' frs' rule: pstep.induct)
  case (Seq2 c1 s1 f1 c1' s1' f1' c2 frs)
  from Seq2.hyps(2)[OF Seq2.prems] obtain frs'' where
    ih: "f1' = frs'' @ extra" "𝒢, Π ⊢ (c1, s1, frs) →⇩p (c1', s1', frs'')" by blast
  show ?case
    by (rule exI[of _ frs'']) (use ih in auto)
next
  case (Call i p decl actuals dst vals callee s1 frs0 frs)
  then show ?case by auto
next
  case (RestoreStep i s1 fr0 dst frs0 frs)
  from RestoreStep.prems obtain frs1 where "frs = Frame fr0 dst # frs1" "frs0 = frs1 @ extra"
    by (auto simp: Cons_eq_append_conv)
  then show ?case by auto
next
  case (UnwindAct i j s1 fr0 dst frs0 frs)
  from UnwindAct.prems obtain frs1 where "frs = Frame fr0 dst # frs1" "frs0 = frs1 @ extra"
    by (auto simp: Cons_eq_append_conv)
  then show ?case by auto
qed auto

text ‹Unlike ‹pstep_frame_restrict› this needs no non-empty active stack: a call-headed
  command never heads with \<^const>‹SKIP› / \<^const>‹Restore› / \<^const>‹Unwind›, so no pop can
  fire.›
lemma pstep_call_frame_restrict:
  "𝒢, Π ⊢ (c, s, fr) →⇩p (c', s', frs') ⟹ head_call c ⟹ fr = frs @ extra ⟹
   ∃frs''. frs' = frs'' @ extra ∧ 𝒢, Π ⊢ (c, s, frs) →⇩p (c', s', frs'')"
proof (induction "(c, s, fr)" "(c', s', frs')"
       arbitrary: c s fr frs c' s' frs' rule: pstep.induct)
  case (Seq2 c1 s1 f1 c1' s1' f1' c2 frs)
  from Seq2.prems(1) have "head_call c1" by simp
  from Seq2.hyps(2)[OF this Seq2.prems(2)] obtain frs'' where
    ih: "f1' = frs'' @ extra" "𝒢, Π ⊢ (c1, s1, frs) →⇩p (c1', s1', frs'')" by blast
  show ?case by (rule exI[of _ frs'']) (use ih in auto)
next
  case (Call i p decl actuals dst vals callee s1 frs0 frs)
  then show ?case by auto
qed auto

text ‹The CFG dual: a \<^const>‹cstep› also touches only the head of the stack, so an extra
  bottom segment rides along --- with no non-emptiness needed, since the return step already
  requires a non-empty stack.›
lemma cstep_frame_extend:
  "𝒢, g ⊢ (u, s, stk) →⇩c (u', s', stk') ⟹
   𝒢, g ⊢ (u, s, stk @ E) →⇩c (u', s', stk' @ E)"
  by (erule cstep.cases) auto

lemma cstep_star_frame_extend:
  assumes "𝒢, g ⊢ c →⇩c⇧* c'"
  shows "𝒢, g ⊢ (fst c, fst (snd c), snd (snd c) @ E)
                        →⇩c⇧* (fst c', fst (snd c'), snd (snd c') @ E)"
  using assms
proof (induction rule: star.induct)
  case (refl a) show ?case by simp
next
  case (step a b c)
  obtain ua sa stka where a: "a = (ua, sa, stka)" by (cases a)
  obtain ub sb stkb where b: "b = (ub, sb, stkb)" by (cases b)
  from step.hyps(1) a b have "𝒢, g ⊢ (ua, sa, stka) →⇩c (ub, sb, stkb)" by simp
  hence "𝒢, g ⊢ (ua, sa, stka @ E) →⇩c (ub, sb, stkb @ E)" by (rule cstep_frame_extend)
  with step.IH a b show ?case by (auto intro: star.step)
qed

text ‹The ‹Nested› step-inversion rule: stepping a wrapped activation
  \<^term>‹Seq inner (Restore i)› is stepping ‹inner›, provided ‹inner› has neither completed nor
  begun to unwind (either of which would relocate rather than step).›
lemma pstep_seq_after_seq_restore:
  assumes step: "𝒢, Π ⊢ (seq_after (Seq inner (Restore i)) afters, s, frs) →⇩p src'"
      and nsk: "¬ is_SKIP inner" and nunw: "⋀j. inner ≠ Unwind j"
  obtains inner' s' fz where
    "src' = (seq_after (Seq inner' (Restore i)) afters, s', fz)"
    "𝒢, Π ⊢ (inner, s, frs) →⇩p (inner', s', fz)"
proof -
  obtain h' s' fz where
    src': "src' = (seq_after h' afters, s', fz)"
      and hstep: "𝒢, Π ⊢ (Seq inner (Restore i), s, frs) →⇩p (h', s', fz)"
    by (rule pstep_seq_after_headE[OF step]) auto
  from hstep nsk obtain inner' where
    "h' = Seq inner' (Restore i)" "𝒢, Π ⊢ (inner, s, frs) →⇩p (inner', s', fz)"
    by (auto simp: nunw)
  with src' show ?thesis using that by blast
qed

text ‹The ‹Nested› step shared by every completion theorem: the inner activation's run lifts
  under the caller frame and its relation re-wraps as ‹Nested›.  ‹csim› pins the graph store
  to the source store, so the lifted run ends at the source store.›
lemma csim_Nested_lift:
  assumes run: "∃cfg'. 𝒢, g ⊢ (v0, s0, stk0) →⇩c⇧* cfg' ∧ Π, g, q ⊢ (inner', s', fz') ≈ cfg'"
      and loc: "control_at Π pc body_pc kc nc (seq_after (SKIP i) afters) cont"
      and cloc: "control_at Π pc body_pc kc nc (seq_after (Call i dst q args) afters) site"
      and cacc: "compiled_at Π g pc body_pc kc nc"
  shows "∃cfg'. 𝒢, g ⊢ (v0, s0, stk0 @ [(cont, dst, caller)]) →⇩c⇧* cfg'
              ∧ Π, g, pc ⊢ (seq_after (Seq inner' (Restore i)) afters, s', fz' @ [Frame caller dst]) ≈ cfg'"
proof -
  from run obtain v' t' stk' where
    inner: "𝒢, g ⊢ (v0, s0, stk0) →⇩c⇧* (v', t', stk')"
      and sim: "Π, g, q ⊢ (inner', s', fz') ≈ (v', t', stk')" by auto
  have teq: "t' = s'" using csim_store_eq[OF sim] by simp
  have "𝒢, g ⊢ (v0, s0, stk0 @ [(cont, dst, caller)])
                         →⇩c⇧* (v', s', stk' @ [(cont, dst, caller)])"
    using cstep_star_frame_extend[OF inner, of "[(cont, dst, caller)]"] teq by simp
  moreover have "Π, g, pc ⊢ (seq_after (Seq inner' (Restore i)) afters, s', fz' @ [Frame caller dst]) ≈ (v', s', stk' @ [(cont, dst, caller)])"
    by (rule csim.Nested[OF sim[unfolded teq] loc cloc cacc])
  ultimately show ?thesis by blast
qed

section ‹Call preservation›

text ‹
  A source \<^const>‹Call› at the head of the active residual is matched by two \<^const>‹cstep›s
  --- the call edge to \<^term>‹FunctionEntry q› and the \<^term>‹EA_Body› edge to the callee body
  --- and adds exactly one ‹Nested› layer: the callee body becomes a fresh ‹Base› activation
  of ‹q›, and the caller resumes at \<^term>‹seq_after (SKIP i) afters›.  Everything the callee
  needs comes from the single \<^const>‹procs_embedded› certificate.
›
lemma csim_call_base:
  assumes pc: "procs_embedded Π g"
      and loc: "control_at Π p body_p kk n (seq_after (Call i dst q actuals) afters) v"
      and cacc: "compiled_at Π g p body_p kk n"
      and decl: "Π q = Some decl"
  shows "∃cfg'. 𝒢, g ⊢ (v, s, []) →⇩c⇧* cfg'
              ∧ Π, g, p ⊢ (seq_after (Seq (body decl) (Restore i)) afters,
                          bind_formals (formals decl) (map (λe. ⟦e⟧⇩e s) actuals)
                            (enter_state 𝒢 s),
                          [Frame s dst]) ≈ cfg'"
proof -
  let ?callee =
    "bind_formals (formals decl) (map (λe. ⟦e⟧⇩e s) actuals) (enter_state 𝒢 s)"
  have spNone: "special_table q = None" by (rule procs_embedded_special_table_none[OF pc decl])
  from cacc obtain n' en E K where comp: "compile Π p body_p kk n = (n', en, E, K)"
      and Ksub: "K ⊆ calls g" by blast
  from control_at_seq_after_call_edge[OF loc refl comp spNone] obtain j w where
    vk: "v = Statement j"
    and edgeK: "(Statement j, CallEdge dst (call_formals Π q) actuals,
                 FunctionEntry q, w) ∈ K"
    and callerSKIP: "control_at Π p body_p kk n (seq_after (SKIP i) afters) w" by blast
  have edge: "(Statement j, CallEdge dst (formals decl) actuals, FunctionEntry q, w)
                ∈ calls g" using edgeK Ksub by (auto simp: decl)
  have cstep1: "𝒢, g ⊢ (Statement j, s, [])
           →⇩c (FunctionEntry q, call_enter 𝒢 (CallEdge dst (formals decl) actuals) s,
            [(w, dst, s)])" by (rule cstep.Call[OF edge])
  have ce: "call_enter 𝒢 (CallEdge dst (formals decl) actuals) s = ?callee"
    by (rule call_enter_CallEdge)
  obtain kq m en_q where
    caccq: "compiled_at Π g q (body decl) kq m"
      and ctrlq: "control_at Π q (body decl) kq m (body decl) en_q"
      and entry: "(FunctionEntry q, EA_Body q, en_q) ∈ intra g"
    by (rule procs_embedded_activation[OF pc decl])
  have cstep2: "𝒢, g ⊢ (FunctionEntry q, ?callee, [(w, dst, s)])
                        →⇩c (en_q, ?callee, [(w, dst, s)])"
    using cstep_body[OF entry] .
  have star: "𝒢, g ⊢ (v, s, []) →⇩c⇧* (en_q, ?callee, [(w, dst, s)])"
    using cstep1[unfolded ce] cstep2 vk by (simp add: star.step)
  have baseCallee: "Π, g, q ⊢ (body decl, ?callee, []) ≈ (en_q, ?callee, [])"
    by (rule csim.Base[OF ctrlq caccq])
  have "Π, g, p ⊢ (seq_after (Seq (body decl) (Restore i)) afters, ?callee, [] @ [Frame s dst]) ≈ (en_q, ?callee, [] @ [(w, dst, s)])"
    by (rule csim.Nested[OF baseCallee callerSKIP loc cacc])
  then have "Π, g, p ⊢ (seq_after (Seq (body decl) (Restore i)) afters, ?callee, [Frame s dst]) ≈ (en_q, ?callee, [(w, dst, s)])"
    by simp
  with star show ?thesis by blast
qed

theorem csim_call_completion:
  "Π, g, ρ ⊢ (c, s, frs) ≈ (v, t, stk) ⟹ procs_embedded Π g ⟹ head_call c ⟹
   𝒢, Π ⊢ (c, s, frs) →⇩p src' ⟹
   ∃cfg'. 𝒢, g ⊢ (v, t, stk) →⇩c⇧* cfg' ∧ Π, g, ρ ⊢ src' ≈ cfg'"
proof (induction "(c, s, frs)" "(v, t, stk)" arbitrary: c s frs v t stk src' rule: csim.induct)
  case (Base p body_p kk n cc vv ss)
  from head_call_seq_after_form[OF Base.prems(2)] obtain i dst q actuals afters where
    ceq: "cc = seq_after (Call i dst q actuals) afters" and spNone: "special_table q = None"
    by blast
  have step: "𝒢, Π ⊢ (seq_after (Call i dst q actuals) afters, ss, []) →⇩p src'"
    using Base.prems(3) ceq by simp
  have w1: "¬ is_SKIP (Call i dst q actuals)" by simp
  have w2: "⋀j. Call i dst q actuals ≠ Unwind j" by simp
  obtain h' s' fz where
    src': "src' = (seq_after h' afters, s', fz)"
      and pcall: "𝒢, Π ⊢ (Call i dst q actuals, ss, []) →⇩p (h', s', fz)"
    by (rule pstep_seq_after_headE[OF step w1 w2])
  from pcall spNone obtain decl where
    qdecl: "Π q = Some decl"
      and heq: "h' = Seq (body decl) (Restore i)"
      and seq: "s' = bind_formals (formals decl) (map (λe. ⟦e⟧⇩e ss) actuals)
                        (enter_state 𝒢 ss)"
      and fzeq: "fz = [Frame ss dst]"
    by auto
  have loc': "control_at Π p body_p kk n (seq_after (Call i dst q actuals) afters) vv"
    using Base.hyps(1) ceq by simp
  from csim_call_base[OF Base.prems(1) loc' Base.hyps(2) qdecl, where s = ss]
  obtain cfg' where
    cstar: "𝒢, g ⊢ (vv, ss, []) →⇩c⇧* cfg'"
      and csimr: "Π, g, p ⊢ (seq_after (Seq (body decl) (Restore i)) afters,
               bind_formals (formals decl) (map (λe. ⟦e⟧⇩e ss) actuals)
                 (enter_state 𝒢 ss),
               [Frame ss dst]) ≈ cfg'" by blast
  from csimr have "Π, g, p ⊢ src' ≈ cfg'" by (simp add: src' heq seq fzeq)
  with cstar show ?case by (intro exI conjI)
next
  case (Returning w i pc body_pc kc nc afters cont dst p args site callee caller)
  from Returning.prems(2) have "head_call w" by simp
  with pop_ready_not_head_call[OF Returning.hyps(1)] show ?case by simp
next
  case (Nested q inner s0 frs0 v0 stk0 pc body_pc kc nc i afters cont dst args site caller)
  have headinner: "head_call inner" using Nested.prems(2) by simp
  have nsk: "¬ is_SKIP inner" using headinner by (rule head_call_not_SKIP)
  have nunw: "⋀j. inner ≠ Unwind j" using headinner by (rule head_call_not_Unwind)
  obtain inner' s' fz where
    src': "src' = (seq_after (Seq inner' (Restore i)) afters, s', fz)"
      and stepin: "𝒢, Π ⊢ (inner, s0, frs0 @ [Frame caller dst]) →⇩p (inner', s', fz)"
    by (rule pstep_seq_after_seq_restore[OF Nested.prems(3) nsk nunw])
  from pstep_call_frame_restrict[OF stepin headinner refl] obtain fz' where
    fz: "fz = fz' @ [Frame caller dst]"
      and stepin': "𝒢, Π ⊢ (inner, s0, frs0) →⇩p (inner', s', fz')" by blast
  from csim_Nested_lift[OF Nested.hyps(2)[OF Nested.prems(1) headinner stepin'] Nested.hyps(3,4,5)]
  show ?case by (simp add: src' fz)
qed

section ‹Intra-procedural preservation and callee fall-through›

text ‹The bulk of the simulation: a step that stays inside one activation.  Either the callee
  body still has work, in which case the step happens under the enclosing ‹Restore› and the
  stack is untouched, or the body is finished and control falls through to that ‹Restore› --
  the only place a callee reaches its own exit without a return statement.›
lemma intra_step_seq_after_seq_restore:
  "intra_step Π (seq_after (Seq inner (Restore i)) afters, s, frs) src' ⟹
   (is_SKIP inner ∧ src' = (seq_after (Restore i) afters, s, frs))
   ∨ (∃inner' s'. src' = (seq_after (Seq inner' (Restore i)) afters, s', frs)
        ∧ intra_step Π (inner, s, frs) (inner', s', frs))"
proof (induction afters arbitrary: src' rule: rev_induct)
  case Nil
  obtain c' s' frs' where sc: "src' = (c', s', frs')" by (cases src')
  from Nil.prems sc have "intra_step Π (Seq inner (Restore i), s, frs) (c', s', frs')" by simp
  from intra_Seq_cases[OF this] show ?case by (auto simp: sc)
next
  case (snoc a xs)
  obtain c' s' frs' where sc: "src' = (c', s', frs')" by (cases src')
  from snoc.prems sc
  have "intra_step Π (Seq (seq_after (Seq inner (Restore i)) xs) a, s, frs) (c', s', frs')"
    by (simp add: seq_after_snoc)
  from intra_Seq_cases[OF this] obtain B' where
    A: "c' = Seq B' a" "frs' = frs"
      and B: "intra_step Π (seq_after (Seq inner (Restore i)) xs, s, frs) (B', s', frs)"
    by auto
  from snoc.IH[OF B] show ?case
  proof (rule disjE)
    assume "is_SKIP inner ∧ (B', s', frs) = (seq_after (Restore i) xs, s, frs)"
    then show ?case using A sc by (auto simp: seq_after_snoc)
  next
    assume "∃inner' s''. (B', s', frs) = (seq_after (Seq inner' (Restore i)) xs, s'', frs)
              ∧ intra_step Π (inner, s, frs) (inner', s'', frs)"
    then show ?case using A sc by (auto simp: seq_after_snoc)
  qed
qed

text ‹
  A ‹Nested› callee that ∗‹completes› (‹inner = SKIP›) exposes \<^const>‹Restore› through the
  ‹ISeq1› fall-through; the CFG runs the completed callee to its exit
  (‹control_at_skip_to_exit›) and takes the \<^term>‹EA_Ret None p› edge into
  \<^term>‹FunctionResult p› (‹compiled_at_exit›), landing in a ‹Returning› activation.
›
theorem csim_intra_completion:
  "Π, g, ρ ⊢ (c, s, frs) ≈ (v, t, stk) ⟹ procs_embedded Π g ⟹
   intra_step Π (c, s, frs) src' ⟹
   ∃cfg'. 𝒢, g ⊢ (v, t, stk) →⇩c⇧* cfg' ∧ Π, g, ρ ⊢ src' ≈ cfg'"
proof (induction "(c, s, frs)" "(v, t, stk)" arbitrary: c s frs v t stk src' rule: csim.induct)
  case (Base p body_p kk n cc vv ss)
  obtain c' s' frs' where sc: "src' = (c', s', frs')" by (cases src')
  from Base.prems(2) sc have istep: "intra_step Π (cc, ss, []) (c', s', frs')" by simp
  from Base.hyps(2) obtain decl where "Π p = Some decl" "body_p = body decl"
    by (rule compiled_at_decl)
  have srcbody: "source_com body_p"
    using procs_embedded_source_com[OF Base.prems(1) ‹Π p = Some decl›] ‹body_p = body decl›
    by simp
  from Base.hyps(2) obtain n' en E K where comp: "compile Π p body_p kk n = (n', en, E, K)"
      and Esub: "E ⊆ intra g" by blast
  from intra_step_simulation[OF Base.hyps(1) istep comp Esub srcbody, where stk = "[]"]
  obtain v' where feq: "frs' = []" and loc': "control_at Π p body_p kk n c' v'"
      and cstar: "𝒢, g ⊢ (vv, ss, []) →⇩c⇧* (v', s', [])" by blast
  have "Π, g, p ⊢ (c', s', []) ≈ (v', s', [])" by (rule csim.Base[OF loc' Base.hyps(2)])
  with cstar show ?case using sc feq by auto
next
  case (Returning w i pc body_pc kc nc afters cont dst p args site callee caller)
  from Returning.prems(2) have "¬ is_returning (seq_after w afters)"
    by (cases src') (auto dest: intra_step_not_returning)
  with Returning.hyps(1) show ?case by (simp add: pop_ready_is_returning)
next
  case (Nested q inner s0 frs0 v0 stk0 pc body_pc kc nc i afters cont dst args site caller)
  from Nested.prems(2)
  have "intra_step Π (seq_after (Seq inner (Restore i)) afters, s0, frs0 @ [Frame caller dst]) src'"
    .
  from intra_step_seq_after_seq_restore[OF this] show ?case
  proof (rule disjE)
    assume fall:
      "is_SKIP inner ∧ src' = (seq_after (Restore i) afters, s0, frs0 @ [Frame caller dst])"
    then have innerSKIP: "is_SKIP inner"
      and src': "src' = (seq_after (Restore i) afters, s0, frs0 @ [Frame caller dst])" by auto
    from innerSKIP obtain j where ij: "inner = SKIP j" by auto
    have baseInner: "Π, g, q ⊢ (SKIP j, s0, frs0) ≈ (v0, s0, stk0)"
      using Nested.hyps(1) ij by simp
    from baseInner obtain c0in kin nin where
      ctrl: "control_at Π q c0in kin nin (SKIP j) v0" and cacc: "compiled_at Π g q c0in kin nin"
        and frs0nil: "frs0 = []" and stk0nil: "stk0 = []"
    proof (cases rule: csim.cases)
      case (Base body_p2 k2 n2) with that show ?thesis by auto
    qed simp_all
    from cacc obtain n' en E K where comp: "compile Π q c0in kin nin = (n', en, E, K)"
      and Esub: "E ⊆ intra g"
      and exitedge: "(kin, EA_Ret None q, FunctionResult q) ∈ intra g"
      by blast
    have star1: "𝒢, g ⊢ (v0, s0, [(cont, dst, caller)])
                   →⇩c⇧* (kin, s0, [(cont, dst, caller)])"
      by (rule control_at_skip_to_exit[OF ctrl _ comp Esub]) simp
    have "𝒢, g ⊢ (kin, s0, [(cont, dst, caller)])
            →⇩c (FunctionResult q, s0, [(cont, dst, caller)])"
      using cstep.Intra[OF exitedge edge_step_EA_Ret_ret_store_mem] by simp
    with star1 have star: "𝒢, g ⊢ (v0, s0, [(cont, dst, caller)])
                             →⇩c⇧* (FunctionResult q, s0, [(cont, dst, caller)])"
      by (rule star_trans[OF _ star_step1])
    have "Π, g, pc ⊢ (seq_after (Restore i) afters, s0, [Frame caller dst]) ≈ (FunctionResult q, s0, [(cont, dst, caller)])"
      by (rule csim.Returning[OF _ _ Nested.hyps(3) Nested.hyps(4) Nested.hyps(5)]) simp_all
    then have "Π, g, pc ⊢ src' ≈ (FunctionResult q, s0, [(cont, dst, caller)])"
      using src' frs0nil by simp
    with star show ?case using stk0nil by auto
  next
    assume "∃inner' s'.
              src' = (seq_after (Seq inner' (Restore i)) afters, s', frs0 @ [Frame caller dst])
              ∧ intra_step Π (inner, s0, frs0 @ [Frame caller dst])
                   (inner', s', frs0 @ [Frame caller dst])"
    then obtain inner' s' where
      src': "src' = (seq_after (Seq inner' (Restore i)) afters, s', frs0 @ [Frame caller dst])"
        and stepin: "intra_step Π (inner, s0, frs0 @ [Frame caller dst])
                       (inner', s', frs0 @ [Frame caller dst])"
      by blast
    from intra_step_any_frame[OF stepin]
    have stepin': "intra_step Π (inner, s0, frs0) (inner', s', frs0)" .
    from csim_Nested_lift[OF Nested.hyps(2)[OF Nested.prems(1) stepin'] Nested.hyps(3,4,5)]
    show ?case by (simp add: src')
  qed
qed

section ‹Return initiation›

text ‹
  A source \<^const>‹Return› in head position fires ‹Return e --> Unwind›, turning the innermost
  callee activation into its returning phase, while the CFG takes the \<^term>‹EA_Ret e p› edge
  to \<^term>‹FunctionResult p›.  The enclosing ‹Nested› wrapper becomes ‹Returning›: its body
  \<^term>‹Seq (seq_after (Unwind j) cafters) (Restore i)› is \<^const>‹pop_ready› because the callee's
  pending continuations ‹cafters› --- source residuals of a \<^const>‹control_at› location ---
  carry no \<^const>‹Restore›.  The ‹frs ≠ []› premise excludes the ill-formed base
  \<^const>‹Return› (a stuck top-level return); ‹csim_step› discharges it from \<^const>‹return_safe›.
›
theorem csim_return_init_completion:
  "Π, g, ρ ⊢ (c, s, frs) ≈ (v, t, stk) ⟹ procs_embedded Π g ⟹ frs ≠ [] ⟹
   head_return c ⟹ 𝒢, Π ⊢ (c, s, frs) →⇩p src' ⟹
   ∃cfg'. 𝒢, g ⊢ (v, t, stk) →⇩c⇧* cfg' ∧ Π, g, ρ ⊢ src' ≈ cfg'"
proof (induction "(c, s, frs)" "(v, t, stk)" arbitrary: c s frs v t stk src' rule: csim.induct)
  case (Base p body_p kk n cc vv ss)
  from Base.prems(2) show ?case by simp
next
  case (Returning w i pc body_pc kc nc afters cont dst p args site callee caller)
  from Returning.prems(3) pop_ready_not_head_return[OF Returning.hyps(1)]
  show ?case by simp
next
  case (Nested q inner s0 frs0 v0 stk0 pc body_pc kc nc i afters cont dst args site caller)
  have hr_inner: "head_return inner" using Nested.prems(3) by simp
  have nsk: "¬ is_SKIP inner" using hr_inner by (rule head_return_not_SKIP)
  have nunw: "inner ≠ Unwind j" for j using hr_inner by auto
  obtain inner' s' fz where
    src': "src' = (seq_after (Seq inner' (Restore i)) afters, s', fz)"
      and stepin: "𝒢, Π ⊢ (inner, s0, frs0 @ [Frame caller dst]) →⇩p (inner', s', fz)"
    by (rule pstep_seq_after_seq_restore[OF Nested.prems(4) nsk nunw])
  show ?case
  proof (cases "frs0 = []")
    case True
    have baseInner: "Π, g, q ⊢ (inner, s0, []) ≈ (v0, s0, stk0)" using Nested.hyps(1) True by simp
    obtain c0in kin nin where
      stk0nil: "stk0 = []"
        and ctrl: "control_at Π q c0in kin nin inner v0"
        and cacc: "compiled_at Π g q c0in kin nin"
      using baseInner by blast
    from cacc obtain decl where "Π q = Some decl" "c0in = body decl"
      by (rule compiled_at_decl)
    have srcc0: "source_com c0in"
      using procs_embedded_source_com[OF Nested.prems(1) ‹Π q = Some decl›]
            ‹c0in = body decl›
      by simp
    obtain ir e cafters where innerform: "inner = seq_after (Return ir e) cafters"
      using head_return_seq_after_form[OF hr_inner] by blast
    ― ‹the head step is @{text ‹Return e --> Unwind›}, leaving the continuations ‹cafters››
    have stepin1: "𝒢, Π ⊢ (seq_after (Return ir e) cafters, s0, [Frame caller dst])
                     →⇩p (inner', s', fz)"
      using stepin True innerform by simp
    obtain h' where inner'form: "inner' = seq_after h' cafters"
        and hstep: "𝒢, Π ⊢ (Return ir e, s0, [Frame caller dst]) →⇩p (h', s', fz)"
      by (rule pstep_seq_after_headE[OF stepin1]) auto
    have hUnw: "h' = Unwind ir" and s'eq: "s' = ret_store e s0" and fzeq: "fz = [Frame caller dst]"
      using hstep by (cases e; auto simp: ret_store_def)+
    ― ‹the callee continuations carry no ‹Restore›, so the ‹Unwind› spine is ‹pop_ready››
    have noRest: "∀a ∈ set cafters. ¬ is_Restore a"
      by (rule control_at_head_return_afters_no_Restore[OF ctrl[unfolded innerform] srcc0])
    have popready: "pop_ready (Seq (seq_after (Unwind ir) cafters) (Restore i))"
      using unwinding_seq_after_Unwind[OF noRest] by simp
    ― ‹CFG: one ‹Intra› step along the return edge to @{term ‹FunctionResult q›}›
    from cacc obtain n' en E K where comp: "compile Π q c0in kin nin = (n', en, E, K)"
        and Esub: "E ⊆ intra g" by blast
    obtain j where vk: "v0 = Statement j"
        and edge: "(Statement j, EA_Ret e q, FunctionResult q) ∈ E"
      using control_at_seq_after_return_edge[OF ctrl[unfolded innerform] refl comp] by blast
    have edgeg: "(Statement j, EA_Ret e q, FunctionResult q) ∈ intra g"
      using edge Esub by blast
    have cstep1: "𝒢, g ⊢ (Statement j, s0, [(cont, dst, caller)])
                          →⇩c (FunctionResult q, ret_store e s0, [(cont, dst, caller)])"
      using cstep.Intra[OF edgeg edge_step_EA_Ret_ret_store_mem] .
    ― ‹the enclosing wrapper becomes @{text Returning}›
    have rel: "Π, g, pc ⊢ (seq_after (Seq (seq_after (Unwind ir) cafters) (Restore i)) afters, ret_store e s0,
         [Frame caller dst]) ≈ (FunctionResult q, ret_store e s0, [(cont, dst, caller)])"
      by (rule csim.Returning[OF popready _ Nested.hyps(3) Nested.hyps(4) Nested.hyps(5)]) simp
    have srcshape: "src' = (seq_after (Seq (seq_after (Unwind ir) cafters) (Restore i)) afters,
                            ret_store e s0, [Frame caller dst])"
      using src' inner'form hUnw s'eq fzeq by simp
    have "𝒢, g ⊢ (v0, s0, stk0 @ [(cont, dst, caller)])
                         →⇩c⇧* (FunctionResult q, ret_store e s0, [(cont, dst, caller)])"
      using cstep1 vk stk0nil by auto
    with rel srcshape show ?thesis by auto
  next
    case False
    from pstep_frame_restrict[OF stepin refl False] obtain fz' where
      fz: "fz = fz' @ [Frame caller dst]"
        and stepin': "𝒢, Π ⊢ (inner, s0, frs0) →⇩p (inner', s', fz')" by blast
    from csim_Nested_lift[OF Nested.hyps(2)[OF Nested.prems(1) False hr_inner stepin']
                             Nested.hyps(3,4,5)]
    show ?thesis by (simp add: src' fz)
  qed
qed

section ‹Return propagation and the frame pop›

text ‹The half of the simulation where the two sides advance at different rates.  A source
  return walks out of the nested residual one dead layer at a time while the graph stays at
  the callee result node, and only the final pop takes a graph step -- so the correspondence
  is a star, not a step-for-step match.›
lemma csim_returning_frames_nonempty:
  "Π, g, ρ ⊢ (c, s, frs) ≈ (v, t, stk) ⟹ is_returning c ⟹ frs ≠ [] ∧ stk ≠ []"
  by (erule csim.cases) (auto dest: control_at_not_returning)

lemma csim_not_unwind:
  "Π, g, ρ ⊢ (Unwind i, s, frs) ≈ cfg' ⟹ False"
  by (erule csim.cases) (auto dest: control_at_not_unwind pop_ready_not_Unwind)

text ‹
  One \<^const>‹pstep› of a base returning activation \<^term>‹seq_after w afters›
  (\<^term>‹pop_ready w›, framed by the single caller frame, CFG at \<^term>‹FunctionResult p›)
  either ∗‹pops›: the source resumes at \<^term>‹seq_after (SKIP i) afters› with the combined store
  and the CFG performs exactly one return \<^const>‹cstep› to ‹cont›, rebuilt as a ‹Base›
  activation; or ∗‹propagates›: an \<^const>‹Unwind› advances one dead-code layer and the CFG
  stays at \<^term>‹FunctionResult p› with ∗‹zero› \<^const>‹cstep›, rebuilt as a ‹Returning›
  activation.
›
lemma csim_returning_base_completion:
  assumes pr: "pop_ready w" and ann: "pop_ann w = Some i"
      and loc: "control_at Π pc body_pc kc nc (seq_after (SKIP i) afters) cont"
      and cloc: "control_at Π pc body_pc kc nc (seq_after (Call i dst q args) afters) site"
      and cacc: "compiled_at Π g pc body_pc kc nc"
      and step: "𝒢, Π ⊢ (seq_after w afters, callee, [Frame caller dst]) →⇩p src'"
  shows "∃cfg'. 𝒢, g ⊢ (FunctionResult q, callee, [(cont, dst, caller)]) →⇩c⇧* cfg'
              ∧ Π, g, pc ⊢ src' ≈ cfg'"
proof -
  have wsk: "¬ is_SKIP w" using pr by (rule pop_ready_not_SKIP)
  have wunw: "w ≠ Unwind j" for j using pr by (rule pop_ready_not_Unwind)
  obtain h' s' frs' where
    src': "src' = (seq_after h' afters, s', frs')"
      and hstep: "𝒢, Π ⊢ (w, callee, [Frame caller dst]) →⇩p (h', s', frs')"
    by (rule pstep_seq_after_headE[OF step wsk wunw])
  let ?rs = "combine_collect 𝒢 dst caller callee"
  from pstep_pop_ready_head[OF pr ann hstep] show ?thesis
  proof (rule disjE)
    assume "(h', s', frs') =
              (SKIP i, combine_assign dst (callee ret_var) (combine_env 𝒢 caller callee), [])"
    hence h': "h' = SKIP i" "s' = ?rs" "frs' = []" by (auto simp: combine_collect_def)
    have "𝒢, g ⊢ (FunctionResult q, callee, [(cont, dst, caller)]) →⇩c (cont, ?rs, [])"
      by (rule cstep.Return)
    moreover have "Π, g, pc ⊢ (seq_after (SKIP i) afters, ?rs, []) ≈ (cont, ?rs, [])"
      by (rule csim.Base[OF loc cacc])
    ultimately show ?thesis using src' h' by auto
  next
    assume "∃w'. (h', s', frs') = (w', callee, [Frame caller dst])
                 ∧ pop_ready w' ∧ pop_ann w' = Some i"
    then obtain w' where h': "h' = w'" "s' = callee" "frs' = [Frame caller dst]"
        and pr': "pop_ready w'" and ann': "pop_ann w' = Some i" by auto
    have "Π, g, pc ⊢ (seq_after w' afters, callee, [Frame caller dst]) ≈ (FunctionResult q, callee, [(cont, dst, caller)])"
      by (rule csim.Returning[OF pr' ann' loc cloc cacc])
    with src' h' show ?thesis by auto
  qed
qed

text ‹Deep return completion: the base case above, threaded out through any number of
  ‹Nested› wrappers.  No \<^const>‹procs_embedded› is needed --- the returning phase runs on the
  certificates ‹csim› already carries.›
theorem csim_returning_completion:
  "Π, g, ρ ⊢ (c, s, frs) ≈ (v, t, stk) ⟹ is_returning c ⟹
   𝒢, Π ⊢ (c, s, frs) →⇩p src' ⟹
   ∃cfg'. 𝒢, g ⊢ (v, t, stk) →⇩c⇧* cfg' ∧ Π, g, ρ ⊢ src' ≈ cfg'"
proof (induction "(c, s, frs)" "(v, t, stk)" arbitrary: c s frs v t stk src' rule: csim.induct)
  case (Base p body_p kk n cc vv ss)
  from control_at_not_returning[OF Base.hyps(1)] Base.prems(1) show ?case by simp
next
  case (Returning w i pc body_pc kc nc ao cont dst p args site callee caller)
  from csim_returning_base_completion[OF Returning.hyps(1) Returning.hyps(2) Returning.hyps(3)
                                         Returning.hyps(4) Returning.hyps(5) Returning.prems(2)]
  show ?case .
next
  case (Nested q inner s0 frs0 v0 stk0 pc body_pc kc nc i afters cont dst args site caller)
  have retinner: "is_returning inner" using Nested.prems(1) by simp
  have nsk: "¬ is_SKIP inner" using retinner by auto
  have nunw: "inner ≠ Unwind j" for j
  proof
    assume "inner = Unwind j"
    with Nested.hyps(1) show False by (blast dest: csim_not_unwind)
  qed
  have frsne: "frs0 ≠ []"
    using csim_returning_frames_nonempty[OF Nested.hyps(1) retinner] by simp
  obtain inner' s' fz where
    src': "src' = (seq_after (Seq inner' (Restore i)) afters, s', fz)"
      and stepin: "𝒢, Π ⊢ (inner, s0, frs0 @ [Frame caller dst]) →⇩p (inner', s', fz)"
    by (rule pstep_seq_after_seq_restore[OF Nested.prems(2) nsk nunw])
  from pstep_frame_restrict[OF stepin refl frsne] obtain fz' where
    fz: "fz = fz' @ [Frame caller dst]"
      and stepin': "𝒢, Π ⊢ (inner, s0, frs0) →⇩p (inner', s', fz')" by blast
  from csim_Nested_lift[OF Nested.hyps(2)[OF retinner stepin'] Nested.hyps(3,4,5)]
  show ?case by (simp add: src' fz)
qed

section ‹Single-step and finite-execution forward simulation›

text ‹Only a ‹Base› activation has an empty stack, and its located residual is a source
  command, so \<^const>‹return_safe› forbids it from heading with \<^const>‹Return›.  This is where
  \<^const>‹return_safe› discharges the nonempty-frame premise of
  ‹csim_return_init_completion›.›
lemma csim_head_return_frames:
  assumes SIM: "Π, g, ρ ⊢ (c, s, frs) ≈ (v, t, stk)"
      and PC: "procs_embedded Π g"
      and WF: "return_safe c"
      and RET: "head_return c"
  shows "frs ≠ []"
proof (rule ccontr)
  assume "¬ frs ≠ []"
  hence base: "Π, g, ρ ⊢ (c, s, []) ≈ (v, t, stk)" using SIM by simp
  obtain p body_p kk n where
    ctrl: "control_at Π p body_p kk n c v" and cacc: "compiled_at Π g p body_p kk n"
    using base by blast
  from cacc obtain decl where "Π p = Some decl" "body_p = body decl"
    by (rule compiled_at_decl)
  have "source_com body_p"
    using procs_embedded_source_com[OF PC ‹Π p = Some decl›] ‹body_p = body decl› by simp
  hence "source_com c" using control_at_source_com[OF ctrl] by simp
  from return_safe_not_head_return[OF WF this] RET show False by simp
qed

text ‹
  One-step forward simulation: the four-way redex classification (‹head_call› /
  ‹head_return› / ‹is_returning› / otherwise-intra) dispatched to the four completion
  theorems above.  \<^const>‹return_safe› is used only to supply the nonempty frame for the
  return-initiation branch; the statement exposes none of the internal classifiers, compile
  tuples, offsets, or frame conditions.
›
theorem csim_step:
  assumes SIM: "Π, g, ρ ⊢ (c, s, frs) ≈ (v, t, stk)"
      and PC: "procs_embedded Π g"
      and WF: "return_safe c"
      and STEP: "𝒢, Π ⊢ (c, s, frs) →⇩p src'"
  shows "∃cfg'. 𝒢, g ⊢ (v, t, stk) →⇩c⇧* cfg' ∧ Π, g, ρ ⊢ src' ≈ cfg'"
proof -
  consider (call) "head_call c" | (ret) "head_return c" | (returning) "is_returning c"
    | (intra) "¬ head_call c" "¬ head_return c" "¬ is_returning c" by blast
  then show ?thesis
  proof cases
    case call
    from csim_call_completion[OF SIM PC call STEP] show ?thesis .
  next
    case ret
    from csim_head_return_frames[OF SIM PC WF ret]
    have "frs ≠ []" .
    from csim_return_init_completion[OF SIM PC this ret STEP] show ?thesis .
  next
    case returning
    from csim_returning_completion[OF SIM returning STEP] show ?thesis .
  next
    case intra
    obtain c' s' frs' where sc: "src' = (c', s', frs')" by (cases src')
    have "intra_step Π (c, s, frs) (c', s', frs')"
      by (rule pstep_intra_classify[OF procs_embedded_special_table_none[OF PC]
            STEP[unfolded sc] intra(1) intra(2) intra(3)])
    from csim_intra_completion[OF SIM PC this] show ?thesis by (simp add: sc)
  qed
qed

lemma csim_run:
  assumes PC: "procs_embedded Π g"
      and RUN: "𝒢, Π ⊢ sc →⇩p⇧* sc'"
      and SIM: "Π, g, ρ ⊢ sc ≈ dg"
      and WF: "return_safe (fst sc)"
  shows "∃dg'. 𝒢, g ⊢ dg →⇩c⇧* dg' ∧ Π, g, ρ ⊢ sc' ≈ dg'"
  using RUN SIM WF
proof (induction arbitrary: dg rule: star.induct)
  case (refl a)
  obtain v0 t0 k0 where "dg = (v0, t0, k0)" by (cases dg)
  with refl show ?case by auto
next
  case (step a b cc)
  obtain c0 s0 f0 where a: "a = (c0, s0, f0)" by (cases a)
  obtain c1 s1 f1 where b: "b = (c1, s1, f1)" by (cases b)
  obtain v0 t0 k0 where dgd: "dg = (v0, t0, k0)" by (cases dg)
  have SIMa: "Π, g, ρ ⊢ (c0, s0, f0) ≈ (v0, t0, k0)" using step.prems(1) a dgd by simp
  have WFa: "return_safe c0" using step.prems(2) a by simp
  have STEP: "𝒢, Π ⊢ (c0, s0, f0) →⇩p (c1, s1, f1)" using step.hyps(1) a b by simp
  from csim_step[OF SIMa PC WFa STEP] obtain dg1 where
    both: "𝒢, g ⊢ (v0, t0, k0) →⇩c⇧* dg1 ∧ Π, g, ρ ⊢ (c1, s1, f1) ≈ dg1" ..
  from both have run1: "𝒢, g ⊢ (v0, t0, k0) →⇩c⇧* dg1" by (rule conjunct1)
  from both have sim1: "Π, g, ρ ⊢ (c1, s1, f1) ≈ dg1" by (rule conjunct2)
  have bodies: "⋀p decl. Π p = Some decl ⟹ source_com (body decl)"
    using procs_embedded_source_com[OF PC] .
  have WFb: "return_safe (fst b)" using return_safe_pstep[OF bodies STEP WFa] b by simp
  have sim1b: "Π, g, ρ ⊢ b ≈ dg1" using sim1 b by simp
  from step.IH[OF sim1b WFb] obtain dg' where
    run2: "𝒢, g ⊢ dg1 →⇩c⇧* dg'" and sim2: "Π, g, ρ ⊢ cc ≈ dg'" by blast
  from run1 run2 have "𝒢, g ⊢ (v0, t0, k0) →⇩c⇧* dg'" by (rule star_trans)
  with sim2 show ?case using dgd by blast
qed

theorem csim_star:
  assumes SIM: "Π, g, ρ ⊢ (c, s, frs) ≈ (v, t, stk)"
      and PC: "procs_embedded Π g"
      and WF: "return_safe c"
      and RUN: "𝒢, Π ⊢ (c, s, frs) →⇩p⇧* src'"
  shows "∃cfg'. 𝒢, g ⊢ (v, t, stk) →⇩c⇧* cfg' ∧ Π, g, ρ ⊢ src' ≈ cfg'"
  using csim_run[OF PC RUN SIM] WF by simp

section ‹The static certificate for a whole compiled program›

text ‹The static source contract establishes the runtime return guard for the root activation.›
lemma wf_compile_input_return_safe:
  assumes "wf_compile_input 𝒢 Π ps"
  shows "return_safe (main_body Π)"
  using wf_compile_inputD(8)[OF assms] wf_compile_inputD(4)[OF assms]
  by (rule return_safe_if_no_return)

text ‹
  \<^const>‹procs_embedded› is the static certificate \<^const>‹csim› reads: every procedure declared
  in ‹Π› has its body fragment, entry ‹EA_Body› wiring and ‹EA_Ret None› exit wiring in the
  target graph.  It covers the entry procedure too, since
  ‹Π prog_main_name = Some ⦇formals = [], body = main_body Π⦈› makes
  \<^term>‹FunctionEntry prog_main_name› an ordinary
  activation.  Discharging it from actual \<^const>‹compile_prog› output, rather than assuming it
  forever, is what closes the static side of the simulation.
›
theorem procs_embedded_compile_prog:
  assumes wf: "wf_compile_input 𝒢 Π ps"
  shows "procs_embedded Π (compile_prog Π ps)"
  unfolding procs_embedded_def
proof (intro allI impI)
  fix p decl assume pd: "Π p = Some decl"
  let ?g = "compile_prog Π ps"
  obtain n1 Eprocs Kprocs n2 Emain Kmain where
      procs: "compile_procs Π ps 0 = (n1, Eprocs, Kprocs)"
    and mainc: "compile_proc Π prog_main_name ⦇formals = [], body = main_body Π⦈ n1
                  = (n2, Emain, Kmain)"
    and intra_g: "intra ?g = Eprocs ∪ Emain" and calls_g: "calls ?g = Kprocs ∪ Kmain"
    by (rule compile_prog_intra_split)
  have srccom: "source_com (body decl)"
    using wf_compile_inputD(7)[OF wf] pd unfolding source_pi_def by blast
  have "∃m m' Ef Kf. compile_proc Π p decl m = (m', Ef, Kf)
          ∧ Ef ⊆ intra ?g ∧ Kf ⊆ calls ?g"
  proof (cases "p = prog_main_name")
    case True
    with pd wf_compile_inputD(2)[OF wf]
    have "decl = ⦇formals = [], body = main_body Π⦈" by simp
    then show ?thesis using mainc True intra_g calls_g by blast
  next
    case False
    with pd wf_compile_inputD(10)[OF wf] have "p ∈ set ps" by auto
    from compile_procs_member[OF procs this pd] obtain m m' Ef Kf where
      cp: "compile_proc Π p decl m = (m', Ef, Kf)" and "Ef ⊆ Eprocs" "Kf ⊆ Kprocs"
      by blast
    then have "Ef ⊆ intra ?g" "Kf ⊆ calls ?g" using intra_g calls_g by auto
    with cp show ?thesis by blast
  qed
  then obtain m m' Ef Kf where cp: "compile_proc Π p decl m = (m', Ef, Kf)"
    and Esub: "Ef ⊆ intra ?g" and Ksub: "Kf ⊆ calls ?g" by blast
  from cp obtain Eb where
    cb: "compile Π p (body decl) (Statement (m + csize (body decl))) m
           = (m + csize (body decl), Statement m, Eb, Kf)"
    and Edef: "Ef = insert (FunctionEntry p, EA_Body p, Statement m)
                 (insert (Statement (m + csize (body decl)), EA_Ret None p, FunctionResult p) Eb)"
    by (rule compile_procE)
  have Ebsub: "Eb ⊆ intra ?g" using Edef Esub by auto
  have ent: "(FunctionEntry p, EA_Body p, Statement m) ∈ intra ?g" using Edef Esub by auto
  have ext: "(Statement (m + csize (body decl)), EA_Ret None p, FunctionResult p) ∈ intra ?g"
    using Edef Esub by auto
  show "∃k n n' en E K. compile Π p (body decl) k n = (n', en, E, K)
          ∧ E ⊆ intra ?g ∧ K ⊆ calls ?g
          ∧ (FunctionEntry p, EA_Body p, en) ∈ intra ?g
          ∧ (k, EA_Ret None p, FunctionResult p) ∈ intra ?g
          ∧ k = Statement (n + csize (body decl))
          ∧ source_com (body decl) ∧ special_table p = None"
    using cb Ebsub Ksub ent ext srccom wf_compile_inputD(6)[OF wf pd] by blast
qed

section ‹The certificate is inhabited›

text ‹
  Everything above is stated under \<^const>‹procs_embedded›, and ‹csim› relates configurations
  only where that certificate holds; a reader is owed one graph that satisfies it, or the
  theorems could all be vacuous.  The smallest program --- ‹main› with an empty body and no
  callees --- is that witness, and it carries through to a ‹csim› relating a real source
  configuration to a real node of a real compiled graph.
›

definition witness_pi :: proc_table where
  "witness_pi p = (if p = STR ''main'' then Some ⦇formals = [], body = SKIP ()⦈ else None)"

abbreviation witness_cfg :: cfg where
  "witness_cfg ≡ compile_prog witness_pi []"

lemma main_body_witness [simp]: "main_body witness_pi = SKIP ()"
  by (simp add: main_body_def witness_pi_def prog_main_name_def)

lemma witness_wf: "wf_compile_input (λ_. False) witness_pi []"
  by (auto simp: wf_compile_input_def wf_source_program_def witness_pi_def
        main_body_def prog_main_name_def
        wf_proc_decl_def reserved_ret_var_def ret_var_def
        special_table_def special_pname_nondet_int_def
        special_pname_min_def special_pname_max_def)

theorem procs_embedded_witness: "procs_embedded witness_pi witness_cfg"
  by (rule procs_embedded_compile_prog[OF witness_wf])

theorem csim_witness:
  obtains v where "witness_pi, witness_cfg, STR ''main'' ⊢ (SKIP (), s, []) ≈ (v, s, [])"
proof -
  have decl: "witness_pi (STR ''main'') = Some ⦇formals = [], body = SKIP ()⦈"
    by (simp add: witness_pi_def)
  obtain k n en where
    cacc: "compiled_at witness_pi witness_cfg (STR ''main'')
             (body ⦇formals = [], body = SKIP ()⦈) k n"
      and ctrl: "control_at witness_pi (STR ''main'')
             (body ⦇formals = [], body = SKIP ()⦈) k n (body ⦇formals = [], body = SKIP ()⦈) en"
    by (rule procs_embedded_activation[OF procs_embedded_witness decl])
  have "witness_pi, witness_cfg, STR ''main'' ⊢ (SKIP (), s, []) ≈ (en, s, [])"
    by (rule csim.Base[OF ctrl[simplified] cacc[simplified]])
  then show ?thesis ..
qed

end