Theory VIMP_Proc_to_CFG

theory VIMP_Proc_to_CFG
  imports "Voblint_CFG.CFG_Def"
begin

section ‹Procedure-aware CFG compilation for ‹com› programs›

text ‹
  Compile a ‹com› program directly into the two-relation procedure-aware CFG.  Nodes are
  ‹Statement n› (allocated from a counter), ‹FunctionEntry p›, and ‹FunctionResult p›.
  The compiler threads the enclosing procedure name ‹p›, so a source ‹Return› and the
  normal fall-through both reach ‹FunctionResult p› through an ‹EA_Ret› intra edge.

  Compilation is continuation passing: the node reached when a fragment falls through is an
  input, not a result.  A node therefore denotes a program point between transfer functions,
  and no fragment invents a node to hold a control flow that its own source construct does not
  have.

  Layout of one procedure ‹p› with body ‹b›:
    ▪ ‹FunctionEntry p --EA_Body p--> entry(b)›;
    ▪ the compiled body edges, with the epilogue node as the body's continuation;
    ▪ ‹epilogue --EA_Ret None p--> FunctionResult p› (normal fall-through returns without a
       value);
    ▪ each source ‹Return e› inside ‹b› compiles to ‹--EA_Ret e p--> FunctionResult p› and
       ignores its continuation, so an early return leaves no node behind.

  Control effects and their source counterparts:
    ▪ source ‹Return› becomes an explicit ‹EA_Ret› edge into ‹FunctionResult›, which also
      does the work the runtime ‹Unwind› does at source level;
    ▪ source activation handling (‹Restore› and the frame pop) becomes
      ‹FunctionResult› + the ‹calls›-edge continuation.

  Calls are emitted only into ‹calls›; a call never appears as an executable intra edge.
  ‹Restore› / ‹Unwind› are runtime-only (excluded by \<^const>‹source_com›); their compile
  clauses are trivial one-node stubs that never occur for a source program.
›
subsection ‹Static allocation size›

text ‹‹csize c› is the number of ‹Statement› indices the fragment of ‹c› allocates, fixed by
  the source syntax alone.  ‹compile› needs it before it recurses: ‹Seq› names the entry
  node of ‹c2› --- the continuation it hands to ‹c1› --- and that node is
  ‹Statement (n + csize c1)›.  ‹compile_next_id› below ties the two together, so the two
  definitions cannot drift apart silently.›
fun csize :: "'a acom ⇒ nat" where
  "csize (SKIP i) = 1"
| "csize (Assign i x a) = 1"
| "csize (Check i l c) = 1"
| "csize (Seq c1 c2) = csize c1 + csize c2"
| "csize (If i b c1 c2) = 1 + csize c1 + csize c2"
| "csize (While i b c) = 1 + csize c"
| "csize (Call i dst q actuals) = 1"
| "csize (Return i e) = 1"
| "csize (Restore i) = 1"
| "csize (Unwind i) = 1"

lemma csize_pos: "0 < csize c"
  by (induction c) auto


subsection ‹Command compilation›

text ‹‹compile Π p c k n› returns ‹(n', entry, intra_edges, call_edges)›, allocating
  ‹Statement› indices in the counter range ‹[n, n')›.  The continuation ‹k› is an
  ∗‹input›: it is the node normal execution reaches when the fragment falls through.  A
  fragment therefore never reports an exit, and a command that cannot fall through simply
  ignores ‹k›.

  Every fragment enters at ‹Statement n›, so the entry is determined by the counter and is
  reported only for convenience.  The procedure table ‹Π› is threaded so a
  \<^const>‹Call› can label its ‹CallEdge› with the callee's declared formals; every other
  clause ignores it.

  Consequences of handing the continuation down rather than reporting an exit:
    ▪ \<^const>‹Seq› needs no connecting ‹EA_Nop›: ‹c1›'s continuation ∗‹is› ‹c2›'s
      entry;
    ▪ \<^const>‹If› allocates no merge node: both branches receive the same ‹k›, and the join
      happens at ‹k›, which is the program point after the conditional;
    ▪ \<^const>‹While› needs no back-edge node: the body's continuation is the loop head;
    ▪ \<^const>‹Return› ignores ‹k› and emits only its ‹EA_Ret› edge, so no unreachable
      continuation node is invented;
    ▪ \<^const>‹Call› resumes at ‹k›, so the resume point is the following program point.
  \<^const>‹Restore› and \<^const>‹Unwind› are runtime-only (excluded by \<^const>‹source_com›),
  so their clauses are never exercised for a source program.  They stay transparent: one node
  and a ‹EA_Nop› to the continuation.  Making them dead ends instead would cost the
  unconditional form of ‹compile_prog_entry_cfg_reaches_exit› for no gain, since no
  source program reaches these clauses.›

text ‹
  A call edge into an undeclared procedure carries no formals: \<^const>‹Call› compiles
  against whatever \<^term>‹Π q› says at compile time, declared or not, so its formal
  list is this classifier rather than a lookup that could fail. Naming it lets lemma
  statements about compiled call edges cite ‹call_formals› instead of restating the
  case split; the ‹[simp]› tag keeps it transparent to existing automation.
›
definition call_formals :: "'a ptable ⇒ pname ⇒ vname list" where
  [simp]: "call_formals Π q =
    (case Π q of
       Some decl ⇒ formals decl
     | None ⇒ Code.abort (STR ''call_formals: call to an undeclared procedure'') (λ_. []))"

fun compile ::
  "'a ptable ⇒ pname ⇒ 'a acom ⇒ cfg_node ⇒ nat
   ⇒ nat × cfg_node
        × (cfg_node × edge_action × cfg_node) set
        × (cfg_node × call_action × cfg_node × cfg_node) set"
where
  "compile Π p (SKIP i) k n =
     (Suc n, Statement n, {(Statement n, EA_Nop, k)}, {})"
| "compile Π p (Assign i x a) k n =
     (Suc n, Statement n, {(Statement n, EA_Assign x a, k)}, {})"
| "compile Π p (Check i l c) k n =
     (Suc n, Statement n, {(Statement n, EA_Check l c, k)}, {})"
| "compile Π p (Seq c1 c2) k n =
     (let (n1, en1, E1, K1) = compile Π p c1 (Statement (n + csize c1)) n;
          (n2, en2, E2, K2) = compile Π p c2 k (n + csize c1)
      in (n2, en1, E1 ∪ E2, K1 ∪ K2))"
| "compile Π p (If i b c1 c2) k n =
     (let (n1, en1, E1, K1) = compile Π p c1 k (Suc n);
          (n2, en2, E2, K2) = compile Π p c2 k n1
      in (n2, Statement n,
          {(Statement n, EA_Assume b, if is_SKIP c1 then k else en1),
           (Statement n, EA_AssumeNot b, if is_SKIP c2 then k else en2)}
            ∪ (if is_SKIP c1 then {} else E1) ∪ (if is_SKIP c2 then {} else E2),
          K1 ∪ K2))"
| "compile Π p (While i b c) k n =
     (let (n1, en1, E1, K1) = compile Π p c (Statement n) (Suc n)
      in (n1, Statement n,
          {(Statement n, EA_Assume b, en1), (Statement n, EA_AssumeNot b, k)} ∪ E1,
          K1))"
| "compile Π p (Call i dst q actuals) k n =
     (case special_table q of
        Some desc ⇒
          (case classify_special desc actuals of
             None ⇒ (Suc n, Statement n, {(Statement n, EA_Nop, k)}, {})
           | Some sc ⇒
               (case dst of
                  Some x ⇒
                    (Suc n, Statement n, {(Statement n, EA_Special sc x, k)}, {})
                | None ⇒
                    (Suc n, Statement n, {(Statement n, EA_Nop, k)}, {})))
      | None ⇒
          (Suc n, Statement n, {},
           {(Statement n,
             CallEdge dst (call_formals Π q) actuals,
             FunctionEntry q, k)}))"
| "compile Π p (Return i e) k n =
     (Suc n, Statement n, {(Statement n, EA_Ret e p, FunctionResult p)}, {})"
| "compile Π p (Restore i) k n =
     (Suc n, Statement n, {(Statement n, EA_Nop, k)}, {})"
| "compile Π p (Unwind i) k n =
     (Suc n, Statement n, {(Statement n, EA_Nop, k)}, {})"

subsection ‹Procedure and program compilation›

text ‹A procedure wraps its body between ‹FunctionEntry p› and ‹FunctionResult p›.  The body
  is compiled with the ∗‹epilogue› node ‹Statement r› as its continuation, and the epilogue
  carries the implicit ‹EA_Ret None p›: normal fall-through returns without a value.  A value is
  published only by an explicit source ‹Return e›, which compiles to its own
  ‹EA_Ret (Some e) p› edge inside the body.

  The epilogue exists so that every edge into ‹FunctionResult p› is a return edge.  Passing
  ‹FunctionResult p› directly as the body continuation would let a trailing assignment target
  the result node.  It is allocated ∗‹after› the body, so statement indices stay in source
  order and ‹r› lies inside the procedure's own counter range --- which is what keeps edge
  locality a statement about one fragment.

  The epilogue edge is emitted for every body, also for one all of whose paths end in an
  explicit \<^const>‹Return›; there the epilogue is dead code.  Emitting it unconditionally
  makes every node of a procedure reach its result, which the solver's coverage argument
  relies on (‹prog_node_reaches›).›

definition compile_proc ::
  "'a ptable ⇒ pname ⇒ 'a gproc_decl ⇒ nat
   ⇒ nat × (cfg_node × edge_action × cfg_node) set
        × (cfg_node × call_action × cfg_node × cfg_node) set"
where
  "compile_proc Π p decl n =
     (let r = n + csize (body decl);
          (n', ben, E, K) = compile Π p (body decl) (Statement r) n
      in (Suc r,
          insert (FunctionEntry p, EA_Body p, ben)
            (insert (Statement r, EA_Ret None p, FunctionResult p) E),
          K))"

fun compile_procs ::
  "'a ptable ⇒ pname list ⇒ nat
   ⇒ nat × (cfg_node × edge_action × cfg_node) set
        × (cfg_node × call_action × cfg_node × cfg_node) set"
where
  "compile_procs Π [] n = (n, {}, {})"
| "compile_procs Π (p # ps) n =
     (case Π p of
        None ⇒ compile_procs Π ps n
      | Some decl ⇒
          (let (n1, E, K) = compile_proc Π p decl n;
               (n2, E', K') = compile_procs Π ps n1
           in (n2, E ∪ E', K ∪ K')))"

text ‹The whole program: every declared procedure, plus ‹main_body Π› compiled under
  ‹prog_main_name› (which the well-formedness predicate keeps disjoint from ‹ps›).  There is
  no global exit: whole-program completion is ‹FunctionResult prog_main_name›, and the entry is
  ‹FunctionEntry prog_main_name›.›

definition compile_prog ::
  "'a ptable ⇒ pname list ⇒ cfg"
where
  "compile_prog Π ps =
     (let (n1, Eprocs, Kprocs) = compile_procs Π ps 0;
          (n2, Emain, Kmain) =
            compile_proc Π prog_main_name ⦇formals = [], body = main_body Π⦈ n1
      in ⦇ intra = Eprocs ∪ Emain, calls = Kprocs ∪ Kmain,
           cfg_entry = FunctionEntry prog_main_name ⦈)"

text ‹Decomposition of a whole compiled program into the callee pass and the ‹main›
  fragment.›
lemma compile_prog_intra_split:
  obtains n1 Eprocs Kprocs n2 Emain Kmain where
    "compile_procs Π ps 0 = (n1, Eprocs, Kprocs)"
    "compile_proc Π prog_main_name ⦇formals = [], body = (main_body Π)⦈ n1 = (n2, Emain, Kmain)"
    "intra (compile_prog Π ps) = Eprocs ∪ Emain"
    "calls (compile_prog Π ps) = Kprocs ∪ Kmain"
proof -
  obtain n1 Eprocs Kprocs where procs: "compile_procs Π ps 0 = (n1, Eprocs, Kprocs)"
    by (rule prod_cases3)
  obtain n2 Emain Kmain
    where mainc: "compile_proc Π prog_main_name ⦇formals = [], body = (main_body Π)⦈ n1
                    = (n2, Emain, Kmain)"
    by (rule prod_cases3)
  show ?thesis
    by (rule that[OF procs mainc]) (simp_all add: compile_prog_def procs mainc Let_def)
qed

lemma cfg_entry_compile_prog [simp]:
  "cfg_entry (compile_prog Π ps) = FunctionEntry prog_main_name"
  by (simp add: compile_prog_def Let_def split: prod.splits)

lemma cfg_exit_compile_prog [simp]:
  "cfg_exit (compile_prog Π ps) = FunctionResult prog_main_name"
  by (simp add: cfg_exit_def)

subsection ‹Allocation arithmetic and statement ranges›

text ‹A fragment allocates exactly ‹csize c› indices.  This is the obligation the forward
  numbering rests on: ‹Seq› names ‹c2›'s entry before compiling ‹c1›, so a clause allocating
  more or fewer nodes than its \<^const>‹csize› claims would leave that continuation dangling.
  The equation subsumes the counter monotonicity used throughout the ownership lemmas.›

lemma compile_next_id:
  "compile Π p c k n = (n', en, E, K) ⟹ n' = n + csize c"
proof (induction c arbitrary: k n n' en E K rule: gcom.induct)
  case (Seq c1 c2)
  then obtain n1 en1 E1 K1 n2 en2 E2 K2 where
    c1: "compile Π p c1 (Statement (n + csize c1)) n = (n1, en1, E1, K1)"
    and c2: "compile Π p c2 k (n + csize c1) = (n2, en2, E2, K2)"
    and n': "n' = n2"
    by (auto simp: Let_def split: prod.splits)
  from Seq.IH(2)[OF c2] n' show ?case by simp
next
  case (If i b c1 c2)
  then obtain n1 en1 E1 K1 n2 en2 E2 K2 where
    c1: "compile Π p c1 k (Suc n) = (n1, en1, E1, K1)"
    and c2: "compile Π p c2 k n1 = (n2, en2, E2, K2)" and n': "n' = n2"
    by (auto split: prod.splits)
  from If.IH(1)[OF c1] If.IH(2)[OF c2] n' show ?case by simp
next
  case (While i b c)
  then obtain n1 en1 E1 K1 where
    c1: "compile Π p c (Statement n) (Suc n) = (n1, en1, E1, K1)" and n': "n' = n1"
    by (auto split: prod.splits)
  from While.IH[OF c1] n' show ?case by simp
qed (auto split: prod.splits option.splits)

text ‹Every fragment enters at its base counter.  Handing the continuation down does not
  change this, which is why \<^const>‹SKIP› keeps a node of its own instead of reporting the
  continuation as its entry.›

lemma compile_entry:
  "compile Π p c k n = (n', en, E, K) ⟹ en = Statement n"
  by (induction c arbitrary: k n n' en E K rule: gcom.induct)
     (auto simp: Let_def split: prod.splits option.splits)

subsection ‹Fragment decomposition›

text ‹The composite clauses, packaged as elimination rules.  Every consumer of \<^const>‹compile›
  needs the same destructuring --- sub-fragments, their base counters, and the edge split ---
  and \<^const>‹csize› makes the sub-counters explicit, so no auxiliary equation has to be
  carried along.›

lemma compile_SeqE [elim]:
  assumes "compile Π p (Seq c1 c2) k n = (n', en, E, K)"
  obtains n1 E1 K1 n2 E2 K2 where
    "compile Π p c1 (Statement (n + csize c1)) n = (n1, Statement n, E1, K1)"
    "compile Π p c2 k (n + csize c1) = (n2, Statement (n + csize c1), E2, K2)"
    "en = Statement n" "E = E1 ∪ E2" "K = K1 ∪ K2"
proof -
  obtain n1 en1 E1 K1 where
    c1: "compile Π p c1 (Statement (n + csize c1)) n = (n1, en1, E1, K1)"
    by (cases "compile Π p c1 (Statement (n + csize c1)) n") auto
  obtain n2 en2 E2 K2 where
    c2: "compile Π p c2 k (n + csize c1) = (n2, en2, E2, K2)"
    by (cases "compile Π p c2 k (n + csize c1)") auto
  have e1: "en1 = Statement n" using compile_entry[OF c1] .
  have e2: "en2 = Statement (n + csize c1)" using compile_entry[OF c2] .
  from assms c1 c2 have "en = Statement n" "E = E1 ∪ E2" "K = K1 ∪ K2"
    using e1 by (auto simp: Let_def)
  with c1 c2 e1 e2 show ?thesis by (auto intro: that)
qed

lemma compile_IfE [elim]:
  assumes "compile Π p (If i b c1 c2) k n = (n', en, E, K)"
  obtains n1 E1 K1 n2 E2 K2 where
    "compile Π p c1 k (Suc n) = (n1, Statement (Suc n), E1, K1)"
    "compile Π p c2 k (Suc n + csize c1) = (n2, Statement (Suc n + csize c1), E2, K2)"
    "en = Statement n"
    "E = {(Statement n, EA_Assume b, if is_SKIP c1 then k else Statement (Suc n)),
          (Statement n, EA_AssumeNot b, if is_SKIP c2 then k else Statement (Suc n + csize c1))} ∪ (if is_SKIP c1 then {} else E1) ∪ (if is_SKIP c2 then {} else E2)"
    "K = K1 ∪ K2"
proof -
  obtain n1 en1 E1 K1 where c1: "compile Π p c1 k (Suc n) = (n1, en1, E1, K1)"
    by (cases "compile Π p c1 k (Suc n)") auto
  have e1: "en1 = Statement (Suc n)" using compile_entry[OF c1] .
  have i1: "n1 = Suc n + csize c1" using compile_next_id[OF c1] by simp
  obtain n2 en2 E2 K2 where c2: "compile Π p c2 k n1 = (n2, en2, E2, K2)"
    by (cases "compile Π p c2 k n1") auto
  have e2: "en2 = Statement (Suc n + csize c1)" using compile_entry[OF c2] i1 by simp
  from assms c1 c2 e1 e2
  have "en = Statement n"
    "E = {(Statement n, EA_Assume b, if is_SKIP c1 then k else Statement (Suc n)),
          (Statement n, EA_AssumeNot b, if is_SKIP c2 then k else Statement (Suc n + csize c1))} ∪ (if is_SKIP c1 then {} else E1) ∪ (if is_SKIP c2 then {} else E2)"
    "K = K1 ∪ K2"
    by (auto simp: Let_def)
  with c1 c2 e1 e2 i1 show ?thesis by (auto intro: that)
qed

lemma compile_WhileE [elim]:
  assumes "compile Π p (While i b c) k n = (n', en, E, K)"
  obtains n1 E1 K1 where
    "compile Π p c (Statement n) (Suc n) = (n1, Statement (Suc n), E1, K1)"
    "en = Statement n"
    "E = {(Statement n, EA_Assume b, Statement (Suc n)),
          (Statement n, EA_AssumeNot b, k)} ∪ E1"
    "K = K1"
proof -
  obtain n1 en1 E1 K1 where c1: "compile Π p c (Statement n) (Suc n) = (n1, en1, E1, K1)"
    by (cases "compile Π p c (Statement n) (Suc n)") auto
  have e1: "en1 = Statement (Suc n)" using compile_entry[OF c1] .
  from assms c1 e1
  have "en = Statement n"
    "E = {(Statement n, EA_Assume b, Statement (Suc n)),
          (Statement n, EA_AssumeNot b, k)} ∪ E1"
    "K = K1"
    by (auto simp: Let_def)
  with c1 e1 show ?thesis by (auto intro: that)
qed

text ‹
  The sub-fragment projections.  Descending into one branch needs only that branch's compile
  tuple and the fact that its edges are among the enclosing fragment's; the full rules above
  additionally hand back the sibling's counter and edge sets, which such a proof binds and
  never uses --- leaving their types unconstrained --- and the exact ‹E = ...› equation, which
  it then has to weaken to a subset by hand.  These state the weaker fact directly.
›

lemma compile_Seq_leftE [elim]:
  assumes "compile Π p (Seq c1 c2) k n = (n', en, E, K)"
  obtains m F L where
    "compile Π p c1 (Statement (n + csize c1)) n = (m, Statement n, F, L)"
    "F ⊆ E" "L ⊆ K"
proof -
  from assms obtain n1 E1 K1 n2 E2 K2 where
    "compile Π p c1 (Statement (n + csize c1)) n = (n1, Statement n, E1, K1)"
    "compile Π p c2 k (n + csize c1) = (n2, Statement (n + csize c1), E2, K2)"
    "en = Statement n" "E = E1 ∪ E2" "K = K1 ∪ K2"
    by (rule compile_SeqE)
  then show ?thesis by (intro that) auto
qed

lemma compile_Seq_rightE [elim]:
  assumes "compile Π p (Seq c1 c2) k n = (n', en, E, K)"
  obtains m F L where
    "compile Π p c2 k (n + csize c1) = (m, Statement (n + csize c1), F, L)"
    "F ⊆ E" "L ⊆ K"
proof -
  from assms obtain n1 E1 K1 n2 E2 K2 where
    "compile Π p c1 (Statement (n + csize c1)) n = (n1, Statement n, E1, K1)"
    "compile Π p c2 k (n + csize c1) = (n2, Statement (n + csize c1), E2, K2)"
    "en = Statement n" "E = E1 ∪ E2" "K = K1 ∪ K2"
    by (rule compile_SeqE)
  then show ?thesis by (intro that) auto
qed

lemma compile_If_leftE [elim]:
  assumes "compile Π p (If i b c1 c2) k n = (n', en, E, K)"
      and "¬ is_SKIP c1"
  obtains m F L where
    "compile Π p c1 k (Suc n) = (m, Statement (Suc n), F, L)"
    "F ⊆ E" "L ⊆ K"
proof -
  from assms(1) obtain n1 E1 K1 n2 E2 K2 where
    "compile Π p c1 k (Suc n) = (n1, Statement (Suc n), E1, K1)"
    "compile Π p c2 k (Suc n + csize c1) = (n2, Statement (Suc n + csize c1), E2, K2)"
    "en = Statement n"
    "E = {(Statement n, EA_Assume b, if is_SKIP c1 then k else Statement (Suc n)),
          (Statement n, EA_AssumeNot b, if is_SKIP c2 then k else Statement (Suc n + csize c1))} ∪ (if is_SKIP c1 then {} else E1) ∪ (if is_SKIP c2 then {} else E2)"
    "K = K1 ∪ K2"
    by (rule compile_IfE)
  with assms(2) show ?thesis by (intro that) auto
qed

lemma compile_If_rightE [elim]:
  assumes "compile Π p (If i b c1 c2) k n = (n', en, E, K)"
      and "¬ is_SKIP c2"
  obtains m F L where
    "compile Π p c2 k (Suc n + csize c1) = (m, Statement (Suc n + csize c1), F, L)"
    "F ⊆ E" "L ⊆ K"
proof -
  from assms(1) obtain n1 E1 K1 n2 E2 K2 where
    "compile Π p c1 k (Suc n) = (n1, Statement (Suc n), E1, K1)"
    "compile Π p c2 k (Suc n + csize c1) = (n2, Statement (Suc n + csize c1), E2, K2)"
    "en = Statement n"
    "E = {(Statement n, EA_Assume b, if is_SKIP c1 then k else Statement (Suc n)),
          (Statement n, EA_AssumeNot b, if is_SKIP c2 then k else Statement (Suc n + csize c1))} ∪ (if is_SKIP c1 then {} else E1) ∪ (if is_SKIP c2 then {} else E2)"
    "K = K1 ∪ K2"
    by (rule compile_IfE)
  with assms(2) show ?thesis by (intro that) auto
qed

lemma compile_While_bodyE [elim]:
  assumes "compile Π p (While i b c) k n = (n', en, E, K)"
  obtains m F L where
    "compile Π p c (Statement n) (Suc n) = (m, Statement (Suc n), F, L)"
    "F ⊆ E" "L ⊆ K"
proof -
  from assms obtain n1 E1 K1 where
    "compile Π p c (Statement n) (Suc n) = (n1, Statement (Suc n), E1, K1)"
    "en = Statement n"
    "E = {(Statement n, EA_Assume b, Statement (Suc n)),
          (Statement n, EA_AssumeNot b, k)} ∪ E1"
    "K = K1"
    by (rule compile_WhileE)
  then show ?thesis by (intro that) auto
qed

text ‹A branching fragment's own two edges, for the callers that want them rather than a
  sub-fragment: the guard edges out of \<^term>‹Statement n›, which are all the fragment adds
  beyond its branches.›

lemma compile_If_assume_edges:
  assumes "compile Π p (If i b c1 c2) k n = (n', en, E, K)"
  shows "(Statement n, EA_Assume b, if is_SKIP c1 then k else Statement (Suc n)) ∈ E"
        "(Statement n, EA_AssumeNot b, if is_SKIP c2 then k else Statement (Suc n + csize c1)) ∈ E"
proof -
  from assms obtain n1 E1 K1 n2 E2 K2 where
    "compile Π p c1 k (Suc n) = (n1, Statement (Suc n), E1, K1)"
    "compile Π p c2 k (Suc n + csize c1) = (n2, Statement (Suc n + csize c1), E2, K2)"
    "en = Statement n"
    and E: "E = {(Statement n, EA_Assume b, if is_SKIP c1 then k else Statement (Suc n)),
                 (Statement n, EA_AssumeNot b, if is_SKIP c2 then k else Statement (Suc n + csize c1))} ∪ (if is_SKIP c1 then {} else E1) ∪ (if is_SKIP c2 then {} else E2)"
    "K = K1 ∪ K2"
    by (rule compile_IfE)
  show "(Statement n, EA_Assume b, if is_SKIP c1 then k else Statement (Suc n)) ∈ E" using E
    by blast
  show "(Statement n, EA_AssumeNot b, if is_SKIP c2 then k else Statement (Suc n + csize c1)) ∈ E"
    using E by blast
qed

lemma compile_While_assume_edges:
  assumes "compile Π p (While i b c) k n = (n', en, E, K)"
  shows "(Statement n, EA_Assume b, Statement (Suc n)) ∈ E"
        "(Statement n, EA_AssumeNot b, k) ∈ E"
proof -
  from assms obtain n1 E1 K1 where
    "compile Π p c (Statement n) (Suc n) = (n1, Statement (Suc n), E1, K1)"
    "en = Statement n"
    and E: "E = {(Statement n, EA_Assume b, Statement (Suc n)),
                 (Statement n, EA_AssumeNot b, k)} ∪ E1"
    "K = K1"
    by (rule compile_WhileE)
  show "(Statement n, EA_Assume b, Statement (Suc n)) ∈ E" using E by blast
  show "(Statement n, EA_AssumeNot b, k) ∈ E" using E by blast
qed

text ‹The procedure layout, packaged the same way: the body is compiled at ‹n› with the
  epilogue as its continuation, the entry bracket points at the body entry \<^term>‹Statement n›,
  and the epilogue \<^term>‹Statement (n + csize (body decl))› carries the implicit return.›
lemma compile_procE [elim]:
  assumes "compile_proc Π p decl n = (n', E, K)"
  obtains Eb where
    "compile Π p (body decl) (Statement (n + csize (body decl))) n
       = (n + csize (body decl), Statement n, Eb, K)"
    "E = insert (FunctionEntry p, EA_Body p, Statement n)
           (insert (Statement (n + csize (body decl)), EA_Ret None p, FunctionResult p) Eb)"
    "n' = Suc (n + csize (body decl))"
proof -
  define r where "r = n + csize (body decl)"
  obtain m ben Eb Kb where
    cb: "compile Π p (body decl) (Statement r) n = (m, ben, Eb, Kb)"
    by (rule prod_cases4)
  have e: "ben = Statement n" using compile_entry[OF cb] .
  have i: "m = r" using compile_next_id[OF cb] unfolding r_def by simp
  from assms cb e i
  have "E = insert (FunctionEntry p, EA_Body p, Statement n)
              (insert (Statement r, EA_Ret None p, FunctionResult p) Eb)"
    "K = Kb" "n' = Suc r"
    unfolding compile_proc_def r_def by (auto simp: Let_def)
  with cb e i show ?thesis unfolding r_def by (auto intro: that)
qed

end