Theory Compile_Wellformed

theory Compile_Wellformed
  imports VIMP_Proc_to_CFG
begin

section ‹What is true of the graph the compiler produces›

text ‹
  The compiler theory says how a program becomes nodes and edges; this one says what holds of
  the result.  Three facts leave the session.  A compiled ‹calls› set never has two edges out
  of one node, because each fragment claims fresh \<^const>‹Statement› indices for its call
  leaves (‹compile_prog_calls_source_unique›) --- the context-sensitive analyses need it to
  read a call site's callee off the graph.  A compiled graph is finite
  (‹compile_prog_finite›), which every solver instantiation requires.  And a compiled graph
  satisfies \<^const>‹wf_cfg› (‹compile_prog_wf›), the compiler-agnostic contract the D/G layer
  is stated against.

  ‹frag_stmts› is the local vocabulary: the set of \<^const>‹Statement› indices an edge set
  mentions, which is how a fragment's claim on the counter is expressed and how two
  procedures are shown not to overlap.
›

subsection ‹Call-source uniqueness›

text ‹
  Each compiled fragment allocates its ‹Call› leaves at distinct, freshly claimed
  ‹Statement› indices, so a compiled ‹calls› set never has two different edges out of
  the same source node.  This is a structural fact about the compiler, not about
  \<^const>‹wf_cfg› (which is deliberately compiler-agnostic) or about any particular
  program: a hand-built CFG whose source node has two distinct outgoing call edges can
  still violate it, but no \<^const>‹compile_prog› output can, and it is what lets a
  context-routing hook resolve the one call at a node from the source node alone.
›

lemma compile_calls_source_range:
  "compile Π p c k n = (n', en, E, K) ⟹ (u, act, ce, af) ∈ K
   ⟹ ∃j. u = Statement j ∧ n ≤ j ∧ j < n'"
proof (induction c arbitrary: k n n' en E K rule: gcom.induct)
  case (Seq c1 c2)
  from Seq.prems(1) 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" and K: "K = K1 ∪ K2"
    by (auto simp: Let_def split: prod.splits)
  have i1: "n1 = n + csize c1" using compile_next_id[OF c1] .
  have i2: "n2 = n + csize c1 + csize c2" using compile_next_id[OF c2] by simp
  from Seq.prems(2) K consider (L) "(u, act, ce, af) ∈ K1" | (R) "(u, act, ce, af) ∈ K2" by auto
  then show ?case
  proof cases
    case L with Seq.IH(1)[OF c1 L] i1 i2 show ?thesis unfolding n' by auto
  next
    case R with Seq.IH(2)[OF c2 R] i1 i2 show ?thesis unfolding n' by auto
  qed
next
  case (If i b c1 c2)
  from If.prems(1) 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" and K: "K = K1 ∪ K2"
    by (auto split: prod.splits)
  have i1: "n1 = Suc n + csize c1" using compile_next_id[OF c1] by simp
  have i2: "n2 = n1 + csize c2" using compile_next_id[OF c2] .
  from If.prems(2) K consider (L) "(u, act, ce, af) ∈ K1" | (R) "(u, act, ce, af) ∈ K2" by auto
  then show ?case
  proof cases
    case L with If.IH(1)[OF c1 L] i1 i2 show ?thesis unfolding n' by auto
  next
    case R with If.IH(2)[OF c2 R] i1 i2 show ?thesis unfolding n' by auto
  qed
next
  case (While i b c)
  from While.prems(1) obtain n1 en1 E1 K1 where
      c1: "compile Π p c (Statement n) (Suc n) = (n1, en1, E1, K1)"
    and n': "n' = n1" and K: "K = K1"
    by (auto split: prod.splits)
  from While.prems(2) K have "(u, act, ce, af) ∈ K1" by simp
  with While.IH[OF c1] show ?case unfolding n' by auto
qed (auto split: prod.splits option.splits)

text ‹Two call sets whose sources lie on either side of one counter value cannot share a
  source, so each being source-unique makes their union source-unique.  Both compound
  commands that split the counter, \<^const>‹Seq› and \<^const>‹If›, close
  their case with it.›
lemma calls_source_unique_Un:
  assumes u1: "(u, ca1, ce1, af1) ∈ K1 ⟹ (u, ca2, ce2, af2) ∈ K1
                 ⟹ ca1 = ca2 ∧ ce1 = ce2 ∧ af1 = af2"
    and u2: "(u, ca1, ce1, af1) ∈ K2 ⟹ (u, ca2, ce2, af2) ∈ K2
                 ⟹ ca1 = ca2 ∧ ce1 = ce2 ∧ af1 = af2"
    and lo: "⋀u ca ce af. (u, ca, ce, af) ∈ K1 ⟹ ∃j. u = Statement j ∧ j < m"
    and hi: "⋀u ca ce af. (u, ca, ce, af) ∈ K2 ⟹ ∃j. u = Statement j ∧ m ≤ j"
    and e1: "(u, ca1, ce1, af1) ∈ K1 ∪ K2" and e2: "(u, ca2, ce2, af2) ∈ K1 ∪ K2"
  shows "ca1 = ca2 ∧ ce1 = ce2 ∧ af1 = af2"
  using u1 u2 lo hi e1
  by (metis Un_iff cfg_node.inject(1) e2 leD)

lemma compile_calls_source_unique:
  "compile Π p c k n = (n', en, E, K) ⟹ (u, ca1, ce1, af1) ∈ K ⟹ (u, ca2, ce2, af2) ∈ K
   ⟹ ca1 = ca2 ∧ ce1 = ce2 ∧ af1 = af2"
proof (induction c arbitrary: k n n' en E K rule: gcom.induct)
  case (Seq c1 c2)
  from Seq.prems(1) obtain n1 en1 E1 K1 n2 en2 E2 K2 where
      cc1: "compile Π p c1 (Statement (n + csize c1)) n = (n1, en1, E1, K1)"
    and cc2: "compile Π p c2 k (n + csize c1) = (n2, en2, E2, K2)"
    and K: "K = K1 ∪ K2"
    by (auto simp: Let_def split: prod.splits)
  have i1: "n1 = n + csize c1" using compile_next_id[OF cc1] .
  show ?case
    by (rule calls_source_unique_Un[OF Seq.IH(1)[OF cc1] Seq.IH(2)[OF cc2], where m = n1])
       (use compile_calls_source_range[OF cc1] compile_calls_source_range[OF cc2] i1
            Seq.prems(2,3) K in ‹fastforce+›)
next
  case (If i b c1 c2)
  from If.prems(1) obtain n1 en1 E1 K1 n2 en2 E2 K2 where
      cc1: "compile Π p c1 k (Suc n) = (n1, en1, E1, K1)"
    and cc2: "compile Π p c2 k n1 = (n2, en2, E2, K2)"
    and K: "K = K1 ∪ K2"
    by (auto split: prod.splits)
  show ?case
    by (rule calls_source_unique_Un[OF If.IH(1)[OF cc1] If.IH(2)[OF cc2], where m = n1])
       (use compile_calls_source_range[OF cc1] compile_calls_source_range[OF cc2]
            If.prems(2,3) K in ‹fastforce+›)
next
  case (While i b c)
  from While.prems(1) obtain n1 en1 E1 K1 where
      cc1: "compile Π p c (Statement n) (Suc n) = (n1, en1, E1, K1)"
    and K: "K = K1"
    by (auto split: prod.splits)
  from While.prems(2) K have "(u, ca1, ce1, af1) ∈ K1" by simp
  moreover from While.prems(3) K have "(u, ca2, ce2, af2) ∈ K1" by simp
  ultimately show ?case using While.IH[OF cc1] by blast
qed (auto split: prod.splits option.splits)

lemma compile_proc_counter_mono:
  "compile_proc Π p decl n = (n', E, K) ⟹ n ≤ n'"
  by auto

lemma compile_proc_calls_source_range:
  assumes "compile_proc Π p decl n = (n', E, K)" and "(u, act, ce, af) ∈ K"
  shows "∃j. u = Statement j ∧ n ≤ j ∧ j < n'"
proof -
  from assms(1) obtain Eb where
      body: "compile Π p (body decl) (Statement (n + csize (body decl))) n
               = (n + csize (body decl), Statement n, Eb, K)"
    and n': "n' = Suc (n + csize (body decl))"
    by (rule compile_procE)
  from compile_calls_source_range[OF body assms(2)] show ?thesis unfolding n' by auto
qed

lemma compile_proc_calls_source_unique:
  assumes "compile_proc Π p decl n = (n', E, K)"
    and "(u, ca1, ce1, af1) ∈ K" and "(u, ca2, ce2, af2) ∈ K"
  shows "ca1 = ca2 ∧ ce1 = ce2 ∧ af1 = af2"
proof -
  from assms(1) obtain Eb where
    body: "compile Π p (body decl) (Statement (n + csize (body decl))) n
             = (n + csize (body decl), Statement n, Eb, K)"
    by (rule compile_procE)
  from compile_calls_source_unique[OF body assms(2,3)] show ?thesis .
qed

lemma compile_procs_counter_mono:
  "compile_procs Π ps n = (n', E, K) ⟹ n ≤ n'"
proof (induction ps arbitrary: n n' E K)
  case Nil then show ?case by simp
next
  case (Cons p ps)
  show ?case
  proof (cases "Π p")
    case None with Cons show ?thesis by simp
  next
    case (Some decl)
    with Cons.prems obtain n1 E0 K0 n2 E' K' where
        cp: "compile_proc Π p decl n = (n1, E0, K0)"
      and rest: "compile_procs Π ps n1 = (n2, E', K')" and n': "n' = n2"
      by (auto split: prod.splits)
    from compile_proc_counter_mono[OF cp] Cons.IH[OF rest] n' show ?thesis by simp
  qed
qed

text ‹Every edge of a \<^const>‹compile_procs› pass comes from one declared member's
  \<^const>‹compile_proc› fragment, compiled at some offset inside the pass's counter range;
  conversely every declared member contributes such a fragment.  The three facts below
  are what every structural property of a pass reduces to.›
lemma compile_procs_intra_origin:
  assumes "compile_procs Π ps n = (n', E, K)" and "e ∈ E"
  shows "∃p decl m m' Ep Kp. p ∈ set ps ∧ Π p = Some decl
           ∧ compile_proc Π p decl m = (m', Ep, Kp) ∧ n ≤ m ∧ m' ≤ n' ∧ e ∈ Ep"
  using assms
proof (induction ps arbitrary: n n' E K)
  case Nil then show ?case by simp
next
  case (Cons q qs)
  show ?case
  proof (cases "Π q")
    case None
    with Cons.prems have "compile_procs Π qs n = (n', E, K)" by simp
    from Cons.IH[OF this Cons.prems(2)] show ?thesis by (blast intro: list.set_intros(2))
  next
    case (Some declq)
    from Cons.prems(1) Some obtain n1 Eq Kq n2 E' K' where
        cq: "compile_proc Π q declq n = (n1, Eq, Kq)"
      and rest: "compile_procs Π qs n1 = (n2, E', K')"
      and eq: "n' = n2" "E = Eq ∪ E'"
      by (auto split: prod.splits)
    have mono: "n ≤ n1" "n1 ≤ n2"
      using compile_proc_counter_mono[OF cq] compile_procs_counter_mono[OF rest] .
    show ?thesis
    proof (cases "e ∈ Eq")
      case True
      have "q ∈ set (q # qs) ∧ Π q = Some declq ∧ compile_proc Π q declq n = (n1, Eq, Kq)
              ∧ n ≤ n ∧ n1 ≤ n' ∧ e ∈ Eq"
        using Some cq mono(2) eq(1) True by simp
      then show ?thesis by blast
    next
      case False
      with Cons.prems(2) eq(2) have "e ∈ E'" by simp
      from Cons.IH[OF rest this] obtain p decl m m' Ep Kp where
        "p ∈ set qs" "Π p = Some decl" "compile_proc Π p decl m = (m', Ep, Kp)"
        "n1 ≤ m" "m' ≤ n2" "e ∈ Ep" by blast
      with mono(1) eq(1)
      have "p ∈ set (q # qs) ∧ Π p = Some decl ∧ compile_proc Π p decl m = (m', Ep, Kp)
              ∧ n ≤ m ∧ m' ≤ n' ∧ e ∈ Ep"
        by (auto intro: le_trans)
      then show ?thesis by blast
    qed
  qed
qed

lemma compile_procs_calls_origin:
  assumes "compile_procs Π ps n = (n', E, K)" and "e ∈ K"
  shows "∃p decl m m' Ep Kp. p ∈ set ps ∧ Π p = Some decl
           ∧ compile_proc Π p decl m = (m', Ep, Kp) ∧ n ≤ m ∧ m' ≤ n' ∧ e ∈ Kp"
  using assms
proof (induction ps arbitrary: n n' E K)
  case Nil then show ?case by simp
next
  case (Cons q qs)
  show ?case
  proof (cases "Π q")
    case None
    with Cons.prems have "compile_procs Π qs n = (n', E, K)" by simp
    from Cons.IH[OF this Cons.prems(2)] show ?thesis by (blast intro: list.set_intros(2))
  next
    case (Some declq)
    from Cons.prems(1) Some obtain n1 Eq Kq n2 E' K' where
        cq: "compile_proc Π q declq n = (n1, Eq, Kq)"
      and rest: "compile_procs Π qs n1 = (n2, E', K')"
      and eq: "n' = n2" "K = Kq ∪ K'"
      by (auto split: prod.splits)
    have mono: "n ≤ n1" "n1 ≤ n2"
      using compile_proc_counter_mono[OF cq] compile_procs_counter_mono[OF rest] .
    show ?thesis
    proof (cases "e ∈ Kq")
      case True
      have "q ∈ set (q # qs) ∧ Π q = Some declq ∧ compile_proc Π q declq n = (n1, Eq, Kq)
              ∧ n ≤ n ∧ n1 ≤ n' ∧ e ∈ Kq"
        using Some cq mono(2) eq(1) True by simp
      then show ?thesis by blast
    next
      case False
      with Cons.prems(2) eq(2) have "e ∈ K'" by simp
      from Cons.IH[OF rest this] obtain p decl m m' Ep Kp where
        "p ∈ set qs" "Π p = Some decl" "compile_proc Π p decl m = (m', Ep, Kp)"
        "n1 ≤ m" "m' ≤ n2" "e ∈ Kp" by blast
      with mono(1) eq(1)
      have "p ∈ set (q # qs) ∧ Π p = Some decl ∧ compile_proc Π p decl m = (m', Ep, Kp)
              ∧ n ≤ m ∧ m' ≤ n' ∧ e ∈ Kp"
        by (auto intro: le_trans)
      then show ?thesis by blast
    qed
  qed
qed

lemma compile_procs_member:
  assumes "compile_procs Π ps n = (n', E, K)" and "p ∈ set ps" and "Π p = Some decl"
  shows "∃m m' Ep Kp. compile_proc Π p decl m = (m', Ep, Kp)
           ∧ n ≤ m ∧ m' ≤ n' ∧ Ep ⊆ E ∧ Kp ⊆ K"
  using assms
proof (induction ps arbitrary: n n' E K)
  case Nil then show ?case by simp
next
  case (Cons q qs)
  show ?case
  proof (cases "Π q")
    case None
    with Cons.prems have "compile_procs Π qs n = (n', E, K)" "p ∈ set qs" by auto
    then show ?thesis using Cons.IH Cons.prems(3) by blast
  next
    case (Some declq)
    from Cons.prems(1) Some obtain n1 Eq Kq n2 E' K' where
        cq: "compile_proc Π q declq n = (n1, Eq, Kq)"
      and rest: "compile_procs Π qs n1 = (n2, E', K')"
      and eq: "n' = n2" "E = Eq ∪ E'" "K = Kq ∪ K'"
      by (auto split: prod.splits)
    have mono: "n ≤ n1" "n1 ≤ n2"
      using compile_proc_counter_mono[OF cq] compile_procs_counter_mono[OF rest] .
    show ?thesis
    proof (cases "p = q")
      case True
      with Cons.prems(3) Some have "decl = declq" by simp
      with True cq mono(2) eq
      have "compile_proc Π p decl n = (n1, Eq, Kq) ∧ n ≤ n ∧ n1 ≤ n' ∧ Eq ⊆ E ∧ Kq ⊆ K"
        by simp
      then show ?thesis by blast
    next
      case False
      with Cons.prems(2) have "p ∈ set qs" by simp
      from Cons.IH[OF rest this Cons.prems(3)] obtain m m' Ep Kp where
        "compile_proc Π p decl m = (m', Ep, Kp)" "n1 ≤ m" "m' ≤ n2" "Ep ⊆ E'" "Kp ⊆ K'"
        by blast
      with mono(1) eq
      have "compile_proc Π p decl m = (m', Ep, Kp) ∧ n ≤ m ∧ m' ≤ n' ∧ Ep ⊆ E ∧ Kp ⊆ K"
        by (auto intro: le_trans)
      then show ?thesis by blast
    qed
  qed
qed

lemma compile_procs_calls_source_range:
  assumes "compile_procs Π ps n = (n', E, K)" and "(u, act, ce, af) ∈ K"
  shows "∃j. u = Statement j ∧ n ≤ j ∧ j < n'"
  using compile_procs_calls_origin[OF assms] compile_proc_calls_source_range by fastforce

lemma compile_procs_calls_source_unique:
  "compile_procs Π ps n = (n', E, K) ⟹ (u, ca1, ce1, af1) ∈ K ⟹ (u, ca2, ce2, af2) ∈ K
   ⟹ ca1 = ca2 ∧ ce1 = ce2 ∧ af1 = af2"
proof (induction ps arbitrary: n n' E K)
  case Nil then show ?case by simp
next
  case (Cons p ps)
  show ?case
  proof (cases "Π p")
    case None with Cons show ?thesis by simp
  next
    case (Some decl)
    with Cons.prems(1) obtain n1 E0 K0 n2 E' K' where
        cp: "compile_proc Π p decl n = (n1, E0, K0)"
      and rest: "compile_procs Π ps n1 = (n2, E', K')" and K: "K = K0 ∪ K'"
      by (auto split: prod.splits)
    have not_both: "⋀u' act1' ce1' af1' act2' ce2' af2'.
        (u', act1', ce1', af1') ∈ K0 ⟹ (u', act2', ce2', af2') ∈ K' ⟹ False"
      using compile_proc_calls_source_range[OF cp]
            compile_procs_calls_source_range[OF rest]
      by fastforce
    from Cons.prems(2) K have m1: "(u, ca1, ce1, af1) ∈ K0 ∨ (u, ca1, ce1, af1) ∈ K'" by auto
    from Cons.prems(3) K have m2: "(u, ca2, ce2, af2) ∈ K0 ∨ (u, ca2, ce2, af2) ∈ K'" by auto
    consider (LL) "(u, ca1, ce1, af1) ∈ K0" "(u, ca2, ce2, af2) ∈ K0"
           | (RR) "(u, ca1, ce1, af1) ∈ K'" "(u, ca2, ce2, af2) ∈ K'"
           | (LR) "(u, ca1, ce1, af1) ∈ K0" "(u, ca2, ce2, af2) ∈ K'"
           | (RL) "(u, ca1, ce1, af1) ∈ K'" "(u, ca2, ce2, af2) ∈ K0"
      using m1 m2 by blast
    then show ?thesis
    proof cases
      case LL then show ?thesis using compile_proc_calls_source_unique[OF cp] by blast
    next
      case RR then show ?thesis using Cons.IH[OF rest] by blast
    next
      case LR then show ?thesis using not_both by blast
    next
      case RL then show ?thesis using not_both by blast
    qed
  qed
qed

text ‹Whole-program call-source uniqueness: the fact a routed-context analysis needs
  to resolve the formals of the one call at a node without ambiguity, for any
  \<^const>‹compile_prog› output. Combines the declared-procedures pass and the ‹main›
  pass the same way the well-formedness theorem combines its own two passes.›

theorem compile_prog_calls_source_unique:
  assumes "(u, ca1, ce1, af1) ∈ calls (compile_prog Π ps)"
    and "(u, ca2, ce2, af2) ∈ calls (compile_prog Π ps)"
  shows "ca1 = ca2 ∧ ce1 = ce2 ∧ af1 = af2"
proof -
  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 g: "calls (compile_prog Π ps) = Kprocs ∪ Kmain"
    by (rule compile_prog_intra_split)
  have not_both: "⋀u' act1' ce1' af1' act2' ce2' af2'.
      (u', act1', ce1', af1') ∈ Kprocs ⟹ (u', act2', ce2', af2') ∈ Kmain ⟹ False"
    using compile_procs_calls_source_range[OF procs] compile_proc_calls_source_range[OF mainc]
    by fastforce
  from assms show ?thesis unfolding g
    using compile_procs_calls_source_unique[OF procs] compile_proc_calls_source_unique[OF mainc]
      not_both by (elim UnE) (blast | (drule not_both; blast))+
qed


text ‹The ‹Statement› indices a compiled fragment touches.  Sources are always freshly
  allocated, so they lie in the fragment's own counter range; a target may in addition be the
  continuation, which belongs to the enclosing construct.  ‹kstmt› names that one extra
  index, and is empty when the continuation is not a ‹Statement› node.›

definition frag_stmts ::
  "(cfg_node × edge_action × cfg_node) set
   ⇒ (cfg_node × call_action × cfg_node × cfg_node) set ⇒ nat set"
where
  "frag_stmts E K =
     {j. ∃a v. (Statement j, a, v) ∈ E} ∪ {j. ∃u a. (u, a, Statement j) ∈ E}
   ∪ {j. ∃act ce af. (Statement j, act, ce, af) ∈ K}
   ∪ {j. ∃u act ce. (u, act, ce, Statement j) ∈ K}"

fun kstmt :: "cfg_node ⇒ nat set" where
  "kstmt (Statement j) = {j}"
| "kstmt (FunctionEntry q) = {}"
| "kstmt (FunctionResult q) = {}"

lemma kstmt_iff [simp]: "j ∈ kstmt v ⟷ v = Statement j"
  by (cases v) auto

lemma frag_stmts_empty [simp]: "frag_stmts {} {} = {}"
  by (simp add: frag_stmts_def)

lemma frag_stmts_Un:
  "frag_stmts (E1 ∪ E2) (K1 ∪ K2) = frag_stmts E1 K1 ∪ frag_stmts E2 K2"
  by (auto simp: frag_stmts_def)

lemma frag_stmts_E_srcI [intro]:
  "(Statement j, a, v) ∈ E ⟹ j ∈ frag_stmts E K"
  unfolding frag_stmts_def by blast

lemma frag_stmts_E_tgtI [intro]:
  "(u, a, Statement j) ∈ E ⟹ j ∈ frag_stmts E K"
  unfolding frag_stmts_def by blast

lemma frag_stmts_K_srcI [intro]:
  "(Statement j, act, ce, af) ∈ K ⟹ j ∈ frag_stmts E K"
  unfolding frag_stmts_def by blast

lemma frag_stmts_K_tgtI [intro]:
  "(u, act, ce, Statement j) ∈ K ⟹ j ∈ frag_stmts E K"
  unfolding frag_stmts_def by blast

lemma compile_frag_stmts_range:
  "compile Π p c k n = (n', en, E, K) ⟹ frag_stmts E K ⊆ {n..<n'} ∪ kstmt k"
proof (induction c arbitrary: k n n' en E K rule: gcom.induct)
  case (Seq c1 c2)
  from Seq.prems 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" and E: "E = E1 ∪ E2" and K: "K = K1 ∪ K2"
    by (auto simp: Let_def split: prod.splits)
  have i1: "n1 = n + csize c1" using compile_next_id[OF c1] .
  have i2: "n2 = n + csize c1 + csize c2" using compile_next_id[OF c2] by simp
  have r1: "frag_stmts E1 K1 ⊆ {n..<n1} ∪ {n + csize c1}" using Seq.IH(1)[OF c1] by simp
  have r2: "frag_stmts E2 K2 ⊆ {n + csize c1..<n2} ∪ kstmt k" using Seq.IH(2)[OF c2] .
  show ?case
    using r1 r2 i1 i2 csize_pos[of c2]
    unfolding E K n' by (simp only: frag_stmts_Un) auto
next
  case (If i b c1 c2)
  from If.prems obtain n1 E1 K1 n2 E2 K2 where
    c1: "compile Π p c1 k (Suc n) = (n1, Statement (Suc n), E1, K1)"
    and c2: "compile Π p c2 k (Suc n + csize c1) =
      (n2, Statement (Suc n + csize c1), E2, K2)"
    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)"
    and K: "K = K1 ∪ K2"
    by (rule compile_IfE)
  have ids: "n1 = Suc n + csize c1" "n2 = Suc n + csize c1 + csize c2"
    "n' = n + csize (If i b c1 c2)"
    using compile_next_id[OF c1] compile_next_id[OF c2] compile_next_id[OF If.prems]
    by simp_all
  have sub: "frag_stmts E K ⊆ frag_stmts E1 K1 ∪ frag_stmts E2 K2
      ∪ {n, Suc n, Suc n + csize c1} ∪ kstmt k"
    unfolding E K frag_stmts_def by auto
  show ?case
    using sub If.IH(1)[OF c1] If.IH(2)[OF c2] ids csize_pos[of c1] csize_pos[of c2]
    by fastforce
next
  case (While i b c)
  from While.prems obtain n1 en1 E1 K1 where
    c1: "compile Π p c (Statement n) (Suc n) = (n1, en1, E1, K1)"
    and n': "n' = n1"
    and E: "E = {(Statement n, EA_Assume b, en1), (Statement n, EA_AssumeNot b, k)} ∪ E1"
    and K: "K = {} ∪ K1"
    by (auto split: prod.splits)
  have e1: "en1 = Statement (Suc n)" using compile_entry[OF c1] .
  have i1: "n1 = Suc n + csize c" using compile_next_id[OF c1] .
  have r1: "frag_stmts E1 K1 ⊆ {Suc n..<n1} ∪ {n}" using While.IH[OF c1] by simp
  have guard: "frag_stmts {(Statement n, EA_Assume b, en1),
                           (Statement n, EA_AssumeNot b, k)} {} ⊆ {n..<n1} ∪ kstmt k"
    using e1 i1 csize_pos[of c] by (auto simp: frag_stmts_def)
  have dec: "frag_stmts E K
               = frag_stmts {(Statement n, EA_Assume b, en1),
                             (Statement n, EA_AssumeNot b, k)} {} ∪ frag_stmts E1 K1"
    unfolding E K by (rule frag_stmts_Un)
  show ?case unfolding n' dec using guard r1 i1 csize_pos[of c] by force
qed (auto simp: frag_stmts_def split: option.splits)

subsection ‹Finiteness›

text ‹Each pass emits finitely many edges.  Everything downstream that folds over the graph
  -- the join at a node, the equation enumeration, the solver's variable set -- needs this
  and nothing else about the compiler.›

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

lemma compile_proc_finite:
  "compile_proc Π p decl n = (n', E, K) ⟹ finite E ∧ finite K"
  by (auto simp: compile_proc_def Let_def split: prod.splits dest: compile_finite)

lemma compile_procs_finite:
  "compile_procs Π ps n = (n', E, K) ⟹ finite E ∧ finite K"
proof (induction ps arbitrary: n n' E K)
  case Nil then show ?case by simp
next
  case (Cons p ps)
  show ?case
  proof (cases "Π p")
    case None with Cons show ?thesis by simp
  next
    case (Some decl)
    with Cons.prems obtain n1 E0 K0 n2 E' K' where
      cp: "compile_proc Π p decl n = (n1, E0, K0)"
      and rest: "compile_procs Π ps n1 = (n2, E', K')"
      and E: "E = E0 ∪ E'" and K: "K = K0 ∪ K'"
      by (auto split: prod.splits)
    from compile_proc_finite[OF cp] Cons.IH[OF rest] show ?thesis
      unfolding E K by simp
  qed
qed

lemma compile_prog_finite:
  "finite (intra (compile_prog Π ps))
   ∧ finite (calls (compile_prog Π ps))"
  unfolding compile_prog_def
  by (auto simp: Let_def split: prod.splits
       dest: compile_procs_finite compile_proc_finite)

subsection ‹Edge shapes for well-formedness›

text ‹Every emitted call edge targets a ‹FunctionEntry›; a call is never an intra edge.›
lemma compile_call_ce_entry:
  "compile Π p c k n = (n', en, E, K) ⟹ (u, act, ce, af) ∈ K
   ⟹ ∃q. ce = FunctionEntry q"
  by (induction c arbitrary: k n n' en E K)
     (auto simp: Let_def split: prod.splits if_splits option.splits)

text ‹Edge endpoints: a source is always an allocated ‹Statement›; a target is an allocated
  ‹Statement›, the own \<^term>‹FunctionResult p›, or the continuation.  The continuation
  disjunct is what continuation passing adds, and it is what lets the two \<^const>‹wf_cfg›
  conditions below be discharged without carrying a side condition through the induction.›
lemma compile_E_shape:
  "compile Π p c k n = (n', en, E, K) ⟹ (u, a, v) ∈ E
   ⟹ (∃j. u = Statement j)
       ∧ (v = k ∨ v = FunctionResult p ∨ (∃j. v = Statement j))"
proof (induction c arbitrary: k n n' en E K)
  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 E: "E = E1 ∪ E2"
    by (auto simp: Let_def split: prod.splits)
  consider (L) "(u, a, v) ∈ E1" | (R) "(u, a, v) ∈ E2"
    using Seq.prems(2) E by auto
  then show ?case
  proof cases
    case L from Seq.IH(1)[OF c1 L] show ?thesis by auto
  next
    case R from Seq.IH(2)[OF c2 R] show ?thesis by auto
  qed
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 E: "E = {(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)"
    by (auto split: prod.splits)
  have e1: "en1 = Statement (Suc n)" using compile_entry[OF c1] .
  have e2: "en2 = Statement n1" using compile_entry[OF c2] .
  consider (Guard) "(u, a, v) ∈ {(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)}"
    | (L) "(u, a, v) ∈ E1" | (R) "(u, a, v) ∈ E2"
    using If.prems(2) E by (auto split: if_splits)
  then show ?case
  proof cases
    case Guard then show ?thesis using e1 e2 by (auto split: if_splits)
  next
    case L from If.IH(1)[OF c1 L] show ?thesis by auto
  next
    case R from If.IH(2)[OF c2 R] show ?thesis by auto
  qed
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 E: "E = {(Statement n, EA_Assume b, en1), (Statement n, EA_AssumeNot b, k)} ∪ E1"
    by (auto split: prod.splits)
  have e1: "en1 = Statement (Suc n)" using compile_entry[OF c1] .
  consider (Guard) "(u, a, v) ∈ {(Statement n, EA_Assume b, en1),
                                 (Statement n, EA_AssumeNot b, k)}"
    | (Body) "(u, a, v) ∈ E1"
    using While.prems(2) E by auto
  then show ?case
  proof cases
    case Guard then show ?thesis using e1 by auto
  next
    case Body from While.IH[OF c1 Body] show ?thesis by auto
  qed
qed (auto split: prod.splits option.splits)

text ‹Every ‹EA_Ret› edge lands on the matching ‹FunctionResult› --- the enclosing
  procedure name in the action equals the one in the target node.›
lemma compile_ret_wf:
  "compile Π p c k n = (n', en, E, K) ⟹ (u, EA_Ret e q, v) ∈ E
   ⟹ ∀r. k ≠ FunctionResult r ⟹ v = FunctionResult q"
  by (induction c arbitrary: k n n' en E K)
     (auto simp: Let_def split: prod.splits if_splits option.splits)

lemma compile_proc_call_ce_entry:
  "compile_proc Π p decl n = (n', E, K) ⟹ (u, act, ce, af) ∈ K
   ⟹ ∃q. ce = FunctionEntry q"
  by (auto simp: compile_proc_def Let_def split: prod.splits
       dest: compile_call_ce_entry)

lemma compile_proc_intra_tgt_not_entry:
  "compile_proc Π p decl n = (n', E, K) ⟹ (u, a, v) ∈ E ⟹ v ≠ FunctionEntry q"
  by (auto simp: compile_proc_def Let_def split: prod.splits if_splits
       dest: compile_E_shape compile_entry)

lemma compile_proc_ret_wf:
  "compile_proc Π p decl n = (n', E, K) ⟹ (u, EA_Ret e q, v) ∈ E
   ⟹ v = FunctionResult q"
  by (auto simp: compile_proc_def Let_def split: prod.splits if_splits
       dest: compile_ret_wf)

lemma compile_procs_call_ce_entry:
  "compile_procs Π ps n = (n', E, K) ⟹ (u, act, ce, af) ∈ K
   ⟹ ∃q. ce = FunctionEntry q"
  using compile_procs_calls_origin compile_proc_call_ce_entry by metis

lemma compile_procs_intra_tgt_not_entry:
  "compile_procs Π ps n = (n', E, K) ⟹ (u, a, v) ∈ E ⟹ v ≠ FunctionEntry q"
  using compile_procs_intra_origin compile_proc_intra_tgt_not_entry by metis

lemma compile_procs_ret_wf:
  "compile_procs Π ps n = (n', E, K) ⟹ (u, EA_Ret e q, v) ∈ E ⟹ v = FunctionResult q"
  using compile_procs_intra_origin compile_proc_ret_wf by metis

subsection ‹The compiled program is well-formed›

text ‹The per-pass shape facts above, collected into the single predicate the CFG layer
  states its own theorems over.  Nothing after this point has to know that a graph was
  compiled rather than written by hand.›
theorem compile_prog_wf: "wf_cfg (compile_prog Π ps)"
proof -
  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 g: "intra (compile_prog Π ps) = Eprocs ∪ Emain"
           "calls (compile_prog Π ps) = Kprocs ∪ Kmain"
    by (rule compile_prog_intra_split)
  show ?thesis
    unfolding wf_cfg_def g
    using compile_procs_call_ce_entry[OF procs] compile_proc_call_ce_entry[OF mainc]
      compile_procs_intra_tgt_not_entry[OF procs] compile_proc_intra_tgt_not_entry[OF mainc]
      compile_procs_ret_wf[OF procs] compile_proc_ret_wf[OF mainc]
    by (intro conjI allI impI; elim UnE) blast+
qed

subsection ‹Naming one compiled graph›

text ‹A worked example names its graph with a definition and then wants the five facts above
  about that name rather than about \<^const>‹compile_prog›.  Restating them per example costs a
  proof each and re-derives nothing: the facts hold of every compiled graph, with no
  well-formedness hypothesis.  Interpreting this locale at the defining equation supplies all
  five at once, already phrased in the example's own name.›

locale compiled_cfg = finite_cfg g
  for Π :: "'a ptable" and ps :: "pname list" and g :: cfg +
  assumes cfg_eq: "g = compile_prog Π ps"
begin

text ‹‹entry› and ‹exit› are deliberately not ‹[simp]›: an interpretation would make them
  global rewrites that unfold ‹cfg_entry g› under the example's own graph name, which the
  placement examples reason about symbolically. The finiteness facts (‹finite_intra›,
  ‹finite_calls›) come from the ‹finite_cfg› sublocale and carry no such risk.›

lemma entry: "cfg_entry g = FunctionEntry prog_main_name"
  unfolding cfg_eq by (rule cfg_entry_compile_prog)

lemma exit: "cfg_exit g = FunctionResult prog_main_name"
  unfolding cfg_eq by (rule cfg_exit_compile_prog)

lemma wf: "wf_cfg g"
  unfolding cfg_eq by (rule compile_prog_wf)

end

end