Theory Voblint_Compile.Procedure_Ownership

theory Procedure_Ownership
  imports Compile_Invariants "Voblint_CFG.Activation_Trace_Def"
begin

section ‹Each procedure owns a disjoint block of nodes›

text ‹
  An activation's own local \<^const>‹path_of› stays inside one compiled procedure fragment.  A
  ∗‹fragment› of procedure ‹r› compiled over ‹[m, m')› is \<^term>‹FunctionEntry r›,
  \<^term>‹FunctionResult r›, and the \<^term>‹Statement› nodes in that counter range.  Every intra edge
  keeps both endpoints in one fragment, every call edge keeps its source and continuation there
  (the callee \<^term>‹FunctionEntry› is the only cross-fragment endpoint), and distinct fragments are
  node-disjoint, so a single activation entered at \<^term>‹FunctionEntry p› reaches
  \<^term>‹FunctionResult q› only for ‹p = q›.
›

definition pfn :: "pname ⇒ nat ⇒ nat ⇒ cfg_node set" where
  "pfn r m m' = insert (FunctionEntry r) (insert (FunctionResult r) (Statement ` {m..<m'}))"

lemma pfn_disjoint:
  "p ≠ r ⟹ mp' ≤ m ∨ m' ≤ mp ⟹ x ∈ pfn p mp mp' ⟹ x ∉ pfn r m m'"
  by (auto simp: pfn_def)

subsection ‹Edges keep endpoints in one fragment›

text ‹At command level both endpoints lie in the fragment's own node set or are its
  continuation (‹compile_E_shape›).  At procedure level the continuation is the epilogue node,
  which is inside the fragment's range, so the extra alternative collapses.›

lemma compile_K_shape:
  "compile Π p c k n = (n', en, E, K) ⟹ (u, ce, tgt, af) ∈ K
   ⟹ (∃j. u = Statement j) ∧ (∃q. tgt = FunctionEntry q)
       ∧ (af = k ∨ (∃j. af = Statement j))"
proof (induction c arbitrary: k n n' en E K)
  case (Seq c1 c2)
  from Seq.prems(1) obtain n1 E1 K1 n2 E2 K2 where
    c1: "compile Π p c1 (Statement (n + csize c1)) n = (n1, Statement n, E1, K1)"
    and c2: "compile Π p c2 k (n + csize c1) = (n2, Statement (n + csize c1), E2, K2)"
    and K: "K = K1 ∪ K2"
    by (rule compile_SeqE)
  from Seq.prems(2) K show ?case using Seq.IH(1)[OF c1] Seq.IH(2)[OF c2] by auto
next
  case (If i b c1 c2)
  from If.prems(1) 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 K: "K = K1 ∪ K2"
    by (rule compile_IfE)
  from If.prems(2) K show ?case using If.IH(1)[OF c1] If.IH(2)[OF c2] by auto
next
  case (While i b c)
  from While.prems(1) obtain n1 E1 K1 where
    c1: "compile Π p c (Statement n) (Suc n) = (n1, Statement (Suc n), E1, K1)"
    and K: "K = K1"
    by (rule compile_WhileE)
  from While.prems(2) K show ?case using While.IH[OF c1] by auto
qed (auto split: if_splits option.splits)

lemma compile_intra_pfn:
  assumes cp: "compile Π p c k n = (n', en, E, K)" and e: "(u, a, v) ∈ E"
  shows "u ∈ insert k (pfn p n n') ∧ v ∈ insert k (pfn p n n')"
proof -
  have rng: "frag_stmts E K ⊆ {n..<n'} ∪ kstmt k" using compile_frag_stmts_range[OF cp] .
  from compile_E_shape[OF cp e] obtain ku where u: "u = Statement ku"
    and vshape: "v = k ∨ v = FunctionResult p ∨ (∃kv. v = Statement kv)" by blast
  have "ku ∈ frag_stmts E K" using frag_stmts_E_srcI[of ku a v E] e u by simp
  hence uin: "u ∈ insert k (pfn p n n')" using rng u by (auto simp: pfn_def)
  have vin: "v ∈ insert k (pfn p n n')"
  proof (cases "v = k ∨ v = FunctionResult p")
    case True then show ?thesis by (auto simp: pfn_def)
  next
    case False
    then obtain kv where v: "v = Statement kv" using vshape by blast
    have "kv ∈ frag_stmts E K" using frag_stmts_E_tgtI[of u a kv E] e v by simp
    then show ?thesis using rng v False by (auto simp: pfn_def)
  qed
  from uin vin show ?thesis ..
qed

lemma compile_calls_pfn:
  assumes cp: "compile Π p c k n = (n', en, E, K)" and e: "(u, ce, tgt, af) ∈ K"
  shows "u ∈ insert k (pfn p n n') ∧ af ∈ insert k (pfn p n n')"
proof -
  have rng: "frag_stmts E K ⊆ {n..<n'} ∪ kstmt k" using compile_frag_stmts_range[OF cp] .
  from compile_K_shape[OF cp e] obtain ku where u: "u = Statement ku"
    and afshape: "af = k ∨ (∃kaf. af = Statement kaf)" by blast
  have "ku ∈ frag_stmts E K" using frag_stmts_K_srcI[of ku ce tgt af K E] e u by simp
  hence uin: "u ∈ insert k (pfn p n n')" using rng u by (auto simp: pfn_def)
  have "af ∈ insert k (pfn p n n')"
  proof (cases "af = k")
    case True then show ?thesis by simp
  next
    case False
    then obtain kaf where af: "af = Statement kaf" using afshape by blast
    have "kaf ∈ frag_stmts E K" using frag_stmts_K_tgtI[of u ce tgt kaf K E] e af by simp
    then show ?thesis using rng af False by (auto simp: pfn_def)
  qed
  with uin show ?thesis ..
qed

text ‹The entry wiring edge targets the first statement index of the fragment, which is what
  identifies a fragment by its start counter alone.›
lemma compile_proc_entry_edge:
  assumes cp: "compile_proc Π p decl n = (n', E, K)"
  shows "(FunctionEntry p, EA_Body p, Statement n) ∈ E"
  using cp by auto

lemma compile_proc_intra_pfn:
  assumes cp: "compile_proc Π r decl n = (n', E, K)" and e: "(u, a, v) ∈ E"
  shows "u ∈ pfn r n n' ∧ v ∈ pfn r n n'"
proof -
  from cp obtain Eb where
    cb: "compile Π r (body decl) (Statement (n + csize (body decl))) n
           = (n + csize (body decl), Statement n, Eb, K)"
    and E: "E = insert (FunctionEntry r, EA_Body r, Statement n)
              (insert (Statement (n + csize (body decl)), EA_Ret None r, FunctionResult r) Eb)"
    and n': "n' = Suc (n + csize (body decl))"
    by (rule compile_procE)
  have kin: "Statement (n + csize (body decl)) ∈ pfn r n n'"
    using n' by (auto simp: pfn_def)
  have entryin: "Statement n ∈ pfn r n n'"
    using n' csize_pos[of "body decl"] by (auto simp: pfn_def)
  have inner: "insert (Statement (n + csize (body decl)))
                 (pfn r n (n + csize (body decl))) ⊆ pfn r n n'"
    using n' by (auto simp: pfn_def)
  consider "(u, a, v) = (FunctionEntry r, EA_Body r, Statement n)"
    | "(u, a, v) = (Statement (n + csize (body decl)), EA_Ret None r, FunctionResult r)"
    | "(u, a, v) ∈ Eb"
    using e E by (auto split: if_splits)
  then show ?thesis
  proof cases
    case 1 then show ?thesis using entryin by (auto simp: pfn_def)
  next
    case 2 then show ?thesis using kin by (auto simp: pfn_def)
  next
    case 3 then show ?thesis using compile_intra_pfn[OF cb] inner by blast
  qed
qed

lemma compile_proc_calls_pfn:
  assumes cp: "compile_proc Π r decl n = (n', E, K)" and e: "(u, ce, tgt, af) ∈ K"
  shows "u ∈ pfn r n n' ∧ af ∈ pfn r n n'"
proof -
  from cp obtain Eb where
    cb: "compile Π r (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)
  have inner: "insert (Statement (n + csize (body decl)))
                 (pfn r n (n + csize (body decl))) ⊆ pfn r n n'"
    using n' by (auto simp: pfn_def)
  show ?thesis using compile_calls_pfn[OF cb e] inner by blast
qed

text ‹A fragment of another procedure over a disjoint counter range sources none of its edges
  in ‹pfn r m m'›.›
lemma compile_proc_src_notin_pfn:
  assumes cp: "compile_proc Π p decl mp = (mp', Ep, Kp)"
    and neq: "p ≠ r" and disjoint: "mp' ≤ m ∨ m' ≤ mp"
  shows "(u, a, v) ∈ Ep ⟹ u ∉ pfn r m m'"
    and "(u, ce, tgt, af) ∈ Kp ⟹ u ∉ pfn r m m'"
  using compile_proc_intra_pfn[OF cp] compile_proc_calls_pfn[OF cp] pfn_disjoint[OF neq disjoint]
  by blast+

lemma compile_procs_intra_src_notin_pfn:
  assumes cps: "compile_procs Π ps n = (n', E, K)" and e: "(u, a, v) ∈ E"
    and absent: "r ∉ set ps" and disjoint: "n' ≤ m ∨ m' ≤ n"
  shows "u ∉ pfn r m m'"
proof -
  from compile_procs_intra_origin[OF cps e] obtain p decl mp mp' Ep Kp
    where "p ∈ set ps" and cp: "compile_proc Π p decl mp = (mp', Ep, Kp)"
      and "n ≤ mp" "mp' ≤ n'" and ep: "(u, a, v) ∈ Ep" by blast
  have "p ≠ r" using ‹p ∈ set ps› absent by blast
  moreover have "mp' ≤ m ∨ m' ≤ mp" using ‹n ≤ mp› ‹mp' ≤ n'› disjoint by auto
  ultimately show ?thesis using compile_proc_src_notin_pfn(1)[OF cp _ _ ep] by blast
qed

lemma compile_procs_calls_src_notin_pfn:
  assumes cps: "compile_procs Π ps n = (n', E, K)" and e: "(u, ce, tgt, af) ∈ K"
    and absent: "r ∉ set ps" and disjoint: "n' ≤ m ∨ m' ≤ n"
  shows "u ∉ pfn r m m'"
proof -
  from compile_procs_calls_origin[OF cps e] obtain p decl mp mp' Ep Kp
    where "p ∈ set ps" and cp: "compile_proc Π p decl mp = (mp', Ep, Kp)"
      and "n ≤ mp" "mp' ≤ n'" and ep: "(u, ce, tgt, af) ∈ Kp" by blast
  have "p ≠ r" using ‹p ∈ set ps› absent by blast
  moreover have "mp' ≤ m ∨ m' ≤ mp" using ‹n ≤ mp› ‹mp' ≤ n'› disjoint by auto
  ultimately show ?thesis using compile_proc_src_notin_pfn(2)[OF cp _ _ ep] by blast
qed

subsection ‹A procedure entry has a unique out-edge›

text ‹Within a compiled procedure only the entry wiring edge sources from \<^term>‹FunctionEntry›
  (bodies source from \<^term>‹Statement› nodes by ‹compile_E_shape›, the exit wiring from the exit
  \<^term>‹Statement›), so the source name is the procedure and the target is unique.›
lemma compile_proc_entry_mem:
  assumes cp: "compile_proc Π q decl n = (n', E, K)" and e: "(FunctionEntry r, a, v) ∈ E"
  shows "r = q"
proof -
  from cp obtain Eb where
    cb: "compile Π q (body decl) (Statement (n + csize (body decl))) n
           = (n + csize (body decl), Statement n, Eb, K)"
    and E: "E = insert (FunctionEntry q, EA_Body q, Statement n)
              (insert (Statement (n + csize (body decl)), EA_Ret None q, FunctionResult q) Eb)"
    by (rule compile_procE)
  have "⋀aa vv. (FunctionEntry r, aa, vv) ∉ Eb" using compile_E_shape[OF cb] by blast
  then show ?thesis using e E by (auto split: if_splits)
qed

lemma compile_proc_entry_unique:
  assumes cp: "compile_proc Π q decl n = (n', E, K)"
    and e1: "(FunctionEntry r, a1, v1) ∈ E" and e2: "(FunctionEntry r, a2, v2) ∈ E"
  shows "v1 = v2"
proof -
  from cp obtain Eb where
    cb: "compile Π q (body decl) (Statement (n + csize (body decl))) n
           = (n + csize (body decl), Statement n, Eb, K)"
    and E: "E = insert (FunctionEntry q, EA_Body q, Statement n)
              (insert (Statement (n + csize (body decl)), EA_Ret None q, FunctionResult q) Eb)"
    by (rule compile_procE)
  have nb: "⋀aa vv. (FunctionEntry r, aa, vv) ∉ Eb" using compile_E_shape[OF cb] by blast
  from e1 E nb have "v1 = Statement n" by (auto split: if_splits)
  moreover from e2 E nb have "v2 = Statement n" by (auto split: if_splits)
  ultimately show ?thesis by simp
qed

lemma compile_procs_entry_mem:
  "compile_procs Π ps n = (n', E, K) ⟹ (FunctionEntry r, a, v) ∈ E ⟹ r ∈ set ps"
  using compile_procs_intra_origin compile_proc_entry_mem by blast

text ‹Under ‹distinct ps› a member's fragment owns every edge of the pass that sources in the
  member's nodes: the other members are compiled over disjoint counter ranges, and their
  edges stay in their own fragments.›
lemma compile_procs_member_frag:
  assumes "compile_procs Π ps n = (n', E, K)" and "distinct ps"
    and "r ∈ set ps" and "Π r = Some decl"
  shows "∃m m' Er Kr. compile_proc Π r decl m = (m', Er, Kr) ∧ n ≤ m ∧ m' ≤ n'
           ∧ Er ⊆ E ∧ Kr ⊆ K
           ∧ (∀u a v. (u, a, v) ∈ E ⟶ u ∈ pfn r m m' ⟶ (u, a, v) ∈ Er)
           ∧ (∀u ce tgt af. (u, ce, tgt, af) ∈ K ⟶ u ∈ pfn r m m'
                ⟶ (u, ce, tgt, af) ∈ Kr)"
  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)" "distinct qs" "r ∈ set qs"
      by auto
    from Cons.IH[OF this Cons.prems(4)] show ?thesis .
  next
    case (Some dq)
    with Cons.prems(1) obtain n1 E0 K0 n2 E' K' where
        cp0: "compile_proc Π q dq n = (n1, E0, K0)"
      and rest: "compile_procs Π qs n1 = (n2, E', K')"
      and n': "n' = n2" and E: "E = E0 ∪ E'" and K: "K = K0 ∪ K'"
      by (auto split: prod.splits)
    have qnotin: "q ∉ set qs" and dqs: "distinct qs" using Cons.prems(2) by simp_all
    show ?thesis
    proof (cases "r = q")
      case True
      with Cons.prems(4) Some cp0 have cpr: "compile_proc Π r decl n = (n1, E0, K0)" by simp
      have rnotin: "r ∉ set qs" using qnotin True by simp
      have tailE: "⋀u a v. (u, a, v) ∈ E' ⟹ u ∉ pfn r n n1"
        using compile_procs_intra_src_notin_pfn[OF rest _ rnotin] by blast
      have tailK: "⋀u ce tgt af. (u, ce, tgt, af) ∈ K' ⟹ u ∉ pfn r n n1"
        using compile_procs_calls_src_notin_pfn[OF rest _ rnotin] by blast
      have "∀u a v. (u, a, v) ∈ E ⟶ u ∈ pfn r n n1 ⟶ (u, a, v) ∈ E0"
        using E tailE by blast
      moreover have "∀u ce tgt af. (u, ce, tgt, af) ∈ K ⟶ u ∈ pfn r n n1
                       ⟶ (u, ce, tgt, af) ∈ K0"
        using K tailK by blast
      moreover have "n1 ≤ n'" using compile_procs_counter_mono[OF rest] n' by simp
      moreover have "E0 ⊆ E" "K0 ⊆ K" using E K by auto
      ultimately show ?thesis using cpr by blast
    next
      case False
      have rqs: "r ∈ set qs" using Cons.prems(3) False by simp
      from Cons.IH[OF rest dqs rqs Cons.prems(4)] obtain m m' Er Kr where
          cpr: "compile_proc Π r decl m = (m', Er, Kr)" and bnds: "n1 ≤ m" "m' ≤ n2"
        and sub: "Er ⊆ E'" "Kr ⊆ K'"
        and ownE: "∀u a v. (u, a, v) ∈ E' ⟶ u ∈ pfn r m m' ⟶ (u, a, v) ∈ Er"
        and ownK: "∀u ce tgt af. (u, ce, tgt, af) ∈ K' ⟶ u ∈ pfn r m m'
                     ⟶ (u, ce, tgt, af) ∈ Kr"
        by blast
      have qr: "q ≠ r" using False by simp
      have headE: "⋀u a v. (u, a, v) ∈ E0 ⟹ u ∉ pfn r m m'"
        and headK: "⋀u ce tgt af. (u, ce, tgt, af) ∈ K0 ⟹ u ∉ pfn r m m'"
        using compile_proc_src_notin_pfn[OF cp0 qr] bnds(1) by blast+
      have "∀u a v. (u, a, v) ∈ E ⟶ u ∈ pfn r m m' ⟶ (u, a, v) ∈ Er"
        using E ownE headE by blast
      moreover have "∀u ce tgt af. (u, ce, tgt, af) ∈ K ⟶ u ∈ pfn r m m'
                       ⟶ (u, ce, tgt, af) ∈ Kr"
        using K ownK headK by blast
      moreover have "n ≤ m" using compile_proc_counter_mono[OF cp0] bnds(1) by simp
      moreover have "m' ≤ n'" using bnds(2) n' by simp
      moreover have "Er ⊆ E" "Kr ⊆ K" using sub E K by auto
      ultimately show ?thesis using cpr by blast
    qed
  qed
qed

lemma compile_procs_entry_unique:
  assumes cps: "compile_procs Π ps n = (n', E, K)" and distinct: "distinct ps"
    and e1: "(FunctionEntry r, a1, v1) ∈ E" and e2: "(FunctionEntry r, a2, v2) ∈ E"
  shows "v1 = v2"
proof -
  from compile_procs_intra_origin[OF cps e1] obtain decl
    where rin: "r ∈ set ps" and decl: "Π r = Some decl"
    using compile_proc_entry_mem by metis
  from compile_procs_member_frag[OF cps distinct rin decl] obtain m m' Er Kr where
      cp: "compile_proc Π r decl m = (m', Er, Kr)"
    and own: "∀u a v. (u, a, v) ∈ E ⟶ u ∈ pfn r m m' ⟶ (u, a, v) ∈ Er" by blast
  have "(FunctionEntry r, a1, v1) ∈ Er" "(FunctionEntry r, a2, v2) ∈ Er"
    using own e1 e2 by (auto simp: pfn_def)
  then show ?thesis by (rule compile_proc_entry_unique[OF cp])
qed

text ‹In a whole compiled program \<^term>‹FunctionEntry r› has a unique out-target: ‹main› and the
  callees are node-disjoint (‹prog_main_name ∉ set ps›), and each contributes a single entry edge.›
lemma compile_prog_entry_out_unique:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and e1: "(FunctionEntry r, a1, v1) ∈ intra (compile_prog Π ps)"
    and e2: "(FunctionEntry r, a2, v2) ∈ intra (compile_prog Π ps)"
  shows "v1 = v2"
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 EI: "intra (compile_prog Π ps) = Eprocs ∪ Emain"
    by (rule compile_prog_intra_split)
  have main_mem: "⋀b w. (FunctionEntry r, b, w) ∈ Emain ⟹ r = prog_main_name"
    using compile_proc_entry_mem[OF mainc] by simp
  have procs_mem: "⋀b w. (FunctionEntry r, b, w) ∈ Eprocs ⟹ r ∈ set ps"
    using compile_procs_entry_mem[OF procs] by simp
  show ?thesis
  proof (cases "r = prog_main_name")
    case True
    have "(FunctionEntry r, a1, v1) ∈ Emain" "(FunctionEntry r, a2, v2) ∈ Emain"
      using e1 e2 EI procs_mem True wf_compile_inputD(11)[OF wf] by auto
    then show ?thesis using compile_proc_entry_unique[OF mainc] by blast
  next
    case False
    have "(FunctionEntry r, a1, v1) ∈ Eprocs" "(FunctionEntry r, a2, v2) ∈ Eprocs"
      using e1 e2 EI main_mem False by auto
    then show ?thesis using compile_procs_entry_unique[OF procs wf_compile_inputD(9)[OF wf]]
      by blast
  qed
qed

subsection ‹Whole-program edge shapes›

text ‹Two shape facts a consumer of a compiled graph may use without redoing the
  callee/‹main› split: a call edge always leaves a \<^term>‹Statement› node, and an entry edge
  names a procedure the table declares.  The first is a range property each pass has on its
  own; the second needs well-formed input, which is what ties the compiled procedure list
  back to the table.›lemma compile_prog_calls_source_stmt:
  assumes "(u, ce, tgt, af) ∈ calls (compile_prog Π ps)"
  shows "∃k. u = Statement k"
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 KC: "calls (compile_prog Π ps) = Kprocs ∪ Kmain"
    by (rule compile_prog_intra_split)
  from assms KC show ?thesis
    using compile_procs_calls_source_range[OF procs] compile_proc_calls_source_range[OF mainc]
    by blast
qed

lemma compile_prog_entry_declared:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and e: "(FunctionEntry p, a, v) ∈ intra (compile_prog Π ps)"
  shows "∃d. Π p = Some d"
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 EI: "intra (compile_prog Π ps) = Eprocs ∪ Emain"
    by (rule compile_prog_intra_split)
  from e EI consider "(FunctionEntry p, a, v) ∈ Eprocs" | "(FunctionEntry p, a, v) ∈ Emain"
    by auto
  then show ?thesis
  proof cases
    case 1
    then have "p ∈ set ps" using compile_procs_entry_mem[OF procs] by blast
    with wf_compile_inputD(10)[OF wf] show ?thesis by auto
  next
    case 2
    then have "p = prog_main_name" by (rule compile_proc_entry_mem[OF mainc])
    with wf_compile_inputD(2)[OF wf] show ?thesis by blast
  qed
qed

subsection ‹Edges stay in the activation fragment›

text ‹The fragment a procedure's entry wiring identifies owns every edge of the program that
  sources in its nodes.  The callee pass and ‹main› occupy disjoint counter ranges, and inside
  the pass ‹compile_procs_member_frag› settles ownership; the entry edge pins the start counter
  through ‹compile_prog_entry_out_unique›.›
lemma compile_prog_entry_frag:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and decl: "Π r = Some d"
    and cb: "compile_proc Π r d m = (m', Ep, Kp)"
    and ent: "(FunctionEntry r, EA_Body r, Statement m) ∈ intra (compile_prog Π ps)"
  shows "(∀u a v. (u, a, v) ∈ intra (compile_prog Π ps) ⟶ u ∈ pfn r m m'
             ⟶ (u, a, v) ∈ Ep)
       ∧ (∀u ce tgt af. (u, ce, tgt, af) ∈ calls (compile_prog Π ps)
             ⟶ u ∈ pfn r m m' ⟶ (u, ce, tgt, af) ∈ Kp)"
proof -
  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 EI: "intra ?g = Eprocs ∪ Emain" and KC: "calls ?g = Kprocs ∪ Kmain"
    by (rule compile_prog_intra_split)
  have distinct: "distinct ps" and setps: "set ps = {p. Π p ≠ None} - {prog_main_name}"
    and main_notin: "prog_main_name ∉ set ps"
    using wf_compile_inputD(9,10,11)[OF wf] by blast+
  show ?thesis
  proof (cases "r = prog_main_name")
    case True
    have dd: "d = ⦇formals = [], body = (main_body Π)⦈"
      using decl True wf_compile_inputD(2)[OF wf] by simp
    have entmain: "(FunctionEntry prog_main_name, EA_Body prog_main_name, Statement n1) ∈ intra ?g"
      using EI compile_proc_entry_edge[OF mainc] by simp
    have entr: "(FunctionEntry prog_main_name, EA_Body prog_main_name, Statement m) ∈ intra ?g"
      using ent True by simp
    have mn: "m = n1" using compile_prog_entry_out_unique[OF wf entr entmain] by simp
    have mout: "m' = n2" "Ep = Emain" "Kp = Kmain" using cb mainc True dd mn by simp_all
    show ?thesis unfolding True mn mout
      using EI KC compile_procs_intra_src_notin_pfn[OF procs _ main_notin]
        compile_procs_calls_src_notin_pfn[OF procs _ main_notin] by auto
  next
    case False
    have rin: "r ∈ set ps" using decl setps False by auto
    from compile_procs_member_frag[OF procs distinct rin decl] obtain m0 m0' Er Kr where
        cpr: "compile_proc Π r d m0 = (m0', Er, Kr)" and upper: "m0' ≤ n1"
      and Ersub: "Er ⊆ Eprocs"
      and ownE: "∀u a v. (u, a, v) ∈ Eprocs ⟶ u ∈ pfn r m0 m0' ⟶ (u, a, v) ∈ Er"
      and ownK: "∀u ce tgt af. (u, ce, tgt, af) ∈ Kprocs ⟶ u ∈ pfn r m0 m0'
                   ⟶ (u, ce, tgt, af) ∈ Kr"
      by blast
    have ent0: "(FunctionEntry r, EA_Body r, Statement m0) ∈ intra ?g"
      using EI Ersub compile_proc_entry_edge[OF cpr] by auto
    have mm: "m = m0" using compile_prog_entry_out_unique[OF wf ent ent0] by simp
    have mout: "m' = m0'" "Ep = Er" "Kp = Kr" using cb cpr mm by simp_all
    have neq: "prog_main_name ≠ r" using False by simp
    show ?thesis unfolding mm mout
      using EI KC ownE ownK compile_proc_src_notin_pfn[OF mainc neq] upper by blast
  qed
qed

text ‹Given a genuine procedure fragment (declared body, entry wiring) and a node in it, every
  intra edge leaving that node, and every call leaving it, lands its same-activation successor
  back in the fragment.›
lemma frag_edge_intra:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and decl: "Π r = Some d"
    and cb: "compile_proc Π r d m = (m', Ep, Kp)"
    and ent: "(FunctionEntry r, EA_Body r, Statement m) ∈ intra (compile_prog Π ps)"
    and uin: "u ∈ pfn r m m'"
    and e: "(u, a, v) ∈ intra (compile_prog Π ps)"
  shows "v ∈ pfn r m m'"
  using compile_prog_entry_frag[OF wf decl cb ent] compile_proc_intra_pfn[OF cb] uin e by blast

lemma frag_edge_calls:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and decl: "Π r = Some d"
    and cb: "compile_proc Π r d m = (m', Ep, Kp)"
    and ent: "(FunctionEntry r, EA_Body r, Statement m) ∈ intra (compile_prog Π ps)"
    and uin: "u ∈ pfn r m m'"
    and e: "(u, ce, tgt, af) ∈ calls (compile_prog Π ps)"
  shows "af ∈ pfn r m m'"
  using compile_prog_entry_frag[OF wf decl cb ent] compile_proc_calls_pfn[OF cb] uin e by blast

subsection ‹Procedure locality of a valid activation›

text ‹Every declared procedure of a compiled program owns a fragment, identified by the start
  counter its entry wiring edge points at.›
lemma compile_prog_proc_frag:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and decl: "Π q = Some d"
  obtains m m' Ep Kp where
    "compile_proc Π q d m = (m', Ep, Kp)"
    "(FunctionEntry q, EA_Body q, Statement m) ∈ intra (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 EI: "intra (compile_prog Π ps) = Eprocs ∪ Emain"
    by (rule compile_prog_intra_split)
  show thesis
  proof (cases "q = prog_main_name")
    case True
    have dd: "d = ⦇formals = [], body = (main_body Π)⦈"
      using decl True wf_compile_inputD(2)[OF wf] by simp
    have "(FunctionEntry q, EA_Body q, Statement n1) ∈ intra (compile_prog Π ps)"
      using EI compile_proc_entry_edge[OF mainc] True by auto
    then show ?thesis using that[of n1 n2 Emain Kmain] mainc True dd by simp
  next
    case False
    have rin: "q ∈ set ps" using decl wf_compile_inputD(10)[OF wf] False by auto
    obtain m m' Ep Kp where cp0: "compile_proc Π q d m = (m', Ep, Kp)" and sub: "Ep ⊆ Eprocs"
      using compile_procs_member[OF procs rin decl] by blast
    have "(FunctionEntry q, EA_Body q, Statement m) ∈ intra (compile_prog Π ps)"
      using EI sub compile_proc_entry_edge[OF cp0] by auto
    then show ?thesis using that cp0 by blast
  qed
qed

text ‹‹frag_ok u›: the activation ‹u› either lies wholly inside a genuine procedure fragment
  (declared body, entry wiring, all path nodes in the fragment) or is a single-node activation
  stuck at an undeclared \<^term>‹FunctionEntry› --- which can never advance and never reaches a
  \<^term>‹FunctionResult›.›
definition frag_ok :: "'a ptable ⇒ pname list ⇒ activation_trace ⇒ bool" where
  "frag_ok Π ps u ⟷
     (∃r d m m' Ep Kp. Π r = Some d
        ∧ compile_proc Π r d m = (m', Ep, Kp)
        ∧ (FunctionEntry r, EA_Body r, Statement m) ∈ intra (compile_prog Π ps)
        ∧ fst (hd (path_of u)) = FunctionEntry r
        ∧ (∀nd ∈ fst ` set (path_of u). nd ∈ pfn r m m'))
   ∨ (∃p s. path_of u = [(FunctionEntry p, s)] ∧ Π p = None)"

lemma frag_okI_frag:
  assumes "Π r = Some d" "compile_proc Π r d m = (m', Ep, Kp)"
    "(FunctionEntry r, EA_Body r, Statement m) ∈ intra (compile_prog Π ps)"
    "fst (hd (path_of u)) = FunctionEntry r"
    "⋀nd. nd ∈ fst ` set (path_of u) ⟹ nd ∈ pfn r m m'"
  shows "frag_ok Π ps u"
  unfolding frag_ok_def using assms by blast

lemma frag_okE [elim]:
  assumes "frag_ok Π ps u"
  obtains (frag) r d m m' Ep Kp where "Π r = Some d" "compile_proc Π r d m = (m', Ep, Kp)"
    "(FunctionEntry r, EA_Body r, Statement m) ∈ intra (compile_prog Π ps)"
    "fst (hd (path_of u)) = FunctionEntry r" "∀nd ∈ fst ` set (path_of u). nd ∈ pfn r m m'"
  | (stub) p s where "path_of u = [(FunctionEntry p, s)]" "Π p = None"
  using assms unfolding frag_ok_def by meson

lemma sink_in_path_nodes:
  "t ∈ 𝒯⇘𝒢,g,S⇙ ⟹ sink_node t ∈ fst ` set (path_of t)"
  using valid_activation_trace_path_nonempty by (auto simp: sink_node_def)

text ‹Extending a fragment-local activation by one node keeps it fragment-local when the step
  to that node stays inside every genuine fragment holding its sink and no step leaves a stub.
  An intra step and the resumption after a call are the two such extensions.›
lemma frag_ok_snoc:
  assumes t: "t ∈ 𝒯⇘𝒢,compile_prog Π ps,S⇙" and ok: "frag_ok Π ps t"
    and pu: "path_of u = path_of t @ [(v, s)]"
    and stay: "⋀r d m m' Ep Kp. Π r = Some d ⟹ compile_proc Π r d m = (m', Ep, Kp) ⟹
      (FunctionEntry r, EA_Body r, Statement m) ∈ intra (compile_prog Π ps) ⟹
      sink_node t ∈ pfn r m m' ⟹ v ∈ pfn r m m'"
    and nostub: "⋀q. sink_node t = FunctionEntry q ⟹ Π q = None ⟹ False"
  shows "frag_ok Π ps u"
  using ok
proof (cases rule: frag_okE)
  case (frag r d m m' Ep Kp)
  have "sink_node t ∈ pfn r m m'" using sink_in_path_nodes[OF t] frag(5) by blast
  from stay[OF frag(1,2,3) this] have v_in: "v ∈ pfn r m m'" .
  show ?thesis
    by (rule frag_okI_frag[OF frag(1,2,3)])
       (use frag(4,5) valid_activation_trace_path_nonempty[OF t] v_in in ‹auto simp: pu hd_append›)
next
  case (stub q s0)
  have "sink_node t = FunctionEntry q" using stub(1) by (simp add: sink_node_def)
  from nostub[OF this stub(2)] show ?thesis ..
qed

text ‹Every activation in the caller chain of a valid activation trace is fragment-local.  The property is
  carried over the whole \<^const>‹callers› chain so that the return case, which resumes the caller,
  can read the caller's own fragment (‹caller ∈ callers callee›).›
lemma valid_activation_trace_frag_callers:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and t: "t ∈ 𝒯⇘𝒢,compile_prog Π ps,S⇙"
  shows "∀u ∈ callers t. frag_ok Π ps u"
proof -
  let ?g = "compile_prog Π ps"
  show ?thesis
  proof (rule caller_chain_closure)
    fix s assume "s ∈ S"
    have main_decl: "Π prog_main_name = Some ⦇formals = [], body = (main_body Π)⦈"
      by (rule wf_compile_inputD(2)[OF wf])
    obtain m m' Ep Kp where
      cb: "compile_proc Π prog_main_name ⦇formals = [], body = (main_body Π)⦈ m = (m', Ep, Kp)"
      and ent: "(FunctionEntry prog_main_name, EA_Body prog_main_name, Statement m) ∈ intra ?g"
      by (rule compile_prog_proc_frag[OF wf main_decl])
    show "frag_ok Π ps (Root [(cfg_entry ?g, s)])"
      by (rule frag_okI_frag[OF main_decl cb ent])
         (simp_all add: pfn_def)
  next
    fix t a v s'
    assume ht: "t ∈ 𝒯⇘𝒢,?g,S⇙" and ch: "∀u ∈ callers t. frag_ok Π ps u"
      and e: "(sink_node t, a, v) ∈ intra ?g"
    have "frag_ok Π ps t" using ch callers_refl by blast
    then show "frag_ok Π ps (extend t (v, s'))"
      by (rule frag_ok_snoc[OF ht _ _ frag_edge_intra[OF wf _ _ _ _ e]])
         (use e in ‹auto dest: compile_prog_entry_declared[OF wf]›)
  next
    fix caller dst pars args p cont
    assume "(sink_node caller, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls ?g"
    show "frag_ok Π ps (Call caller
            [(FunctionEntry p, call_enter 𝒢 (CallEdge dst pars args) (sink_store caller))])"
    proof (cases "Π p")
      case None
      then show ?thesis unfolding frag_ok_def by fastforce
    next
      case (Some d)
      obtain m m' Ep Kp where
        cb: "compile_proc Π p d m = (m', Ep, Kp)"
        and ent: "(FunctionEntry p, EA_Body p, Statement m) ∈ intra ?g"
        by (rule compile_prog_proc_frag[OF wf Some])
      show ?thesis
        by (rule frag_okI_frag[OF Some cb ent]) (simp_all add: pfn_def)
    qed
  next
    fix callee caller p dst pars args cont
    assume cvcallee: "callee ∈ 𝒯⇘𝒢,?g,S⇙"
      and ch: "∀u ∈ callers callee. frag_ok Π ps u"
      and cof: "caller_of callee = Some caller" and "sink_node callee = FunctionResult p"
      and e: "(sink_node caller, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls ?g"
    have cin: "caller ∈ callers callee" using cof callers_caller_subset callers_refl by blast
    have cv: "caller ∈ 𝒯⇘𝒢,?g,S⇙" using valid_activation_trace_caller_valid[OF cvcallee cof] .
    have "frag_ok Π ps caller" using ch cin by blast
    then show "frag_ok Π ps (Resume caller callee (path_of caller
            @ [(cont, combine_collect 𝒢 dst (sink_store caller) (sink_store callee))]))"
      by (rule frag_ok_snoc[OF cv _ _ frag_edge_calls[OF wf _ _ _ _ e]])
         (use e in ‹auto dest: compile_prog_calls_source_stmt›)
  next
    show "t ∈ 𝒯⇘𝒢,?g,S⇙" by (rule t)
  qed
qed

text ‹An activation entered at \<^term>‹FunctionEntry p› reaches \<^term>‹FunctionResult q› only for
  ‹p = q›.›
lemma valid_activation_trace_entry_result_eq:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and t: "t ∈ 𝒯⇘𝒢,compile_prog Π ps,S⇙"
    and en: "fst (hd (path_of t)) = FunctionEntry p"
    and sk: "sink_node t = FunctionResult q"
  shows "p = q"
proof -
  have "frag_ok Π ps t"
    using valid_activation_trace_frag_callers[OF wf t] callers_refl by blast
  then show ?thesis
  proof (cases rule: frag_okE)
    case (frag r d m m' Ep Kp)
    have "sink_node t ∈ pfn r m m'" using sink_in_path_nodes[OF t] frag(5) by blast
    with frag(4) en sk show ?thesis by (auto simp: pfn_def)
  next
    case (stub p' s)
    then have "sink_node t = FunctionEntry p'" by (simp add: sink_node_def)
    with sk show ?thesis by simp
  qed
qed

end