Theory Source_Progress

theory Source_Progress
  imports Simulation_Preservation
begin

section ‹Reachable source configurations are never stuck›

text ‹
  A stuck source configuration would silently cut executions short: every later program point
  would be unreachable under \<^const>‹pstep›, so an unreachability verdict could hold for the
  wrong reason.  Progress rules this out for accepted programs: a reachable configuration
  either has finished --- \<^const>‹SKIP› with no caller frame left --- or can take a step.

  The shapes that could get stuck are the runtime markers: a bare \<^const>‹Unwind›, and a
  \<^const>‹Restore› or \<^term>‹Seq (Unwind j) (Restore i)› with no frame to pop.  \<^const>‹csim› already
  pairs every \<^const>‹Restore› with its frame and confines \<^const>‹Unwind› to the returning
  phase, so it is reused here as the invariant; the only additional fact is that call sites
  are well formed.
›

subsection ‹Source commands›

lemma pstep_seq_after_lift:
  "𝒢, Π ⊢ (w, s, frs) →⇩p (w', s', frs')
   ⟹ 𝒢, Π ⊢ (seq_after w afters, s, frs) →⇩p (seq_after w' afters, s', frs')"
  by (induction afters arbitrary: w w') auto

text ‹A well-formed source command is \<^const>‹SKIP› or steps, at any frame stack.  A
  \<^const>‹Return› steps too; whether its \<^const>‹Unwind› can later pop a frame is the
  simulation's concern, not this lemma's.›
lemma wf_source_com_progress:
  assumes distinct_formals: "⋀p decl. Π p = Some decl ⟹ distinct (formals decl)"
      and "wf_source_com Π c"
  shows "is_SKIP c ∨ (∃cfg'. 𝒢, Π ⊢ (c, s, frs) →⇩p cfg')"
  using assms(2)
proof (induction c)
  case (Seq c1 c2)
  from Seq.prems have "wf_source_com Π c1" by simp
  from Seq.IH(1)[OF this] show ?case
  proof
    assume "is_SKIP c1"
    then obtain j where "c1 = SKIP j" by auto
    then show ?thesis by blast
  next
    assume "∃cfg'. 𝒢, Π ⊢ (c1, s, frs) →⇩p cfg'"
    then obtain c1' s' frs' where "𝒢, Π ⊢ (c1, s, frs) →⇩p (c1', s', frs')" by auto
    then show ?thesis by blast
  qed
next
  case (If i b c1 c2)
  show ?case by (cases "truthy (⟦b⟧⇩e s)") blast+
next
  case (Return i e)
  show ?case by (cases e) blast+
next
  case (Call i dst p actuals)
  show ?case
  proof (cases "special_table p")
    case None
    with Call.prems obtain decl where
      decl: "Π p = Some decl" and arity: "length actuals = length (formals decl)"
      by (auto split: option.splits)
    show ?thesis
      using pstep_Call[where Π = Π and p = p, OF decl arity distinct_formals[OF decl]]
      by blast
  next
    case (Some desc)
    with Call.prems obtain sc x where
      sc: "classify_special desc actuals = Some sc" and dst: "dst = Some x"
      by (auto split: option.splits)
    obtain v where "special_result sc s v" using special_result_ex by blast
    with Some sc show ?thesis unfolding dst by blast
  qed
qed auto

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

subsection ‹The frame-pop phase›

text ‹
  A configuration unwinding a finished frame keeps stepping until it is
  ‹Unwind› (‹unwinding_progress›); a ‹Returning› one then pops its frame.
›

lemma unwinding_progress:
  "unwinding u ⟹ (⋀j. u ≠ Unwind j) ⟹ ∃u'. 𝒢, Π ⊢ (u, s, frs) →⇩p (u', s, frs)"
proof (induction u)
  case (Seq u1 c2)
  then have u1: "unwinding u1" and c2: "¬ is_Restore c2" by simp_all
  show ?case
  proof (cases "∃j. u1 = Unwind j")
    case True
    then obtain j where "u1 = Unwind j" by blast
    then show ?thesis using c2 by blast
  next
    case False
    then have "u1 ≠ Unwind j" for j by blast
    from Seq.IH(1)[OF u1 this] obtain u1' where "𝒢, Π ⊢ (u1, s, frs) →⇩p (u1', s, frs)" ..
    then show ?thesis by blast
  qed
next
  case (Unwind x)
  then show ?case by blast
qed simp_all

text ‹The frame a ‹Returning› configuration carries is what lets it pop.›
lemma pop_ready_progress:
  assumes "pop_ready w"
  shows "∃cfg'. 𝒢, Π ⊢ (w, s, Frame fr dst # frs) →⇩p cfg'"
  using assms
proof (cases w rule: pop_ready.cases)
  case 1
  then show ?thesis by blast
next
  case (2 u)
  with assms have uw: "unwinding u" by simp
  show ?thesis
  proof (cases "∃j. u = Unwind j")
    case True
    then obtain j where "u = Unwind j" by blast
    then show ?thesis using 2 by blast
  next
    case False
    then have "u ≠ Unwind j" for j by blast
    from unwinding_progress[OF uw this] obtain u' where
      "𝒢, Π ⊢ (u, s, Frame fr dst # frs) →⇩p (u', s, Frame fr dst # frs)" ..
    then show ?thesis using 2 by blast
  qed
qed (use assms in simp_all)

subsection ‹Progress under the simulation relation›

text ‹Only a ‹Base› activation can have finished: ‹Nested› and ‹Returning› both carry a
  caller frame and a pending \<^const>‹Restore› that will pop it.  No graph fact is used, so
  the relation serves here purely as a shape invariant.›
lemma csim_progress_cfg:
  assumes "Π, g, ρ ⊢ cfg ≈ dg"
      and wf_decls: "⋀p decl. Π p = Some decl ⟹ wf_proc_decl 𝒢 Π decl"
  shows "(is_SKIP (fst cfg) ∧ snd (snd cfg) = []) ∨ (∃cfg'. 𝒢, Π ⊢ cfg →⇩p cfg')"
  using assms(1)
proof (induction rule: csim.induct)
  case (Base p body_p k n c v s)
  from Base.hyps(2) obtain decl where decl: "Π p = Some decl" and body_p: "body_p = body decl"
    by (rule compiled_at_decl)
  have "wf_source_com Π body_p"
    using wf_decls[OF decl] body_p by (simp add: wf_proc_decl_def)
  from control_at_wf_source_com[OF Base.hyps(1) this]
  have "wf_source_com Π c" .
  from wf_source_com_progress[OF _ this, of 𝒢 s "[]"] wf_decls
  show ?case by (auto simp: wf_proc_decl_def)
next
  case (Nested q inner s frs v stk pc body_pc kc nc i afters cont dst args site caller)
  let ?F = "[Frame caller dst]"
  have "∃w'. 𝒢, Π ⊢ (Seq inner (Restore i), s, frs @ ?F) →⇩p w'"
    using Nested.IH
  proof
    assume "is_SKIP (fst (inner, s, frs)) ∧ snd (snd (inner, s, frs)) = []"
    then obtain j where "inner = SKIP j" by auto
    then show ?thesis by blast
  next
    assume "∃cfg'. 𝒢, Π ⊢ (inner, s, frs) →⇩p cfg'"
    then obtain i' s' f' where "𝒢, Π ⊢ (inner, s, frs) →⇩p (i', s', f')" by auto
    from pstep_frame_extend[OF this, of ?F]
    show ?thesis by blast
  qed
  then obtain w' s' f' where "𝒢, Π ⊢ (Seq inner (Restore i), s, frs @ ?F) →⇩p (w', s', f')"
    by auto
  from pstep_seq_after_lift[OF this, of afters] show ?case by auto
next
  case (Returning w i pc body_pc kc nc afters cont dst p args site callee caller)
  from pop_ready_progress[OF Returning.hyps(1), of 𝒢 Π callee caller dst "[]"]
  obtain w' s' f' where "𝒢, Π ⊢ (w, callee, [Frame caller dst]) →⇩p (w', s', f')"
    by auto
  from pstep_seq_after_lift[OF this, of afters] show ?case by auto
qed

theorem csim_progress:
  assumes "Π, g, ρ ⊢ (c, s, frs) ≈ dg"
      and "⋀p decl. Π p = Some decl ⟹ wf_proc_decl 𝒢 Π decl"
  shows "(is_SKIP c ∧ frs = []) ∨ (∃cfg'. 𝒢, Π ⊢ (c, s, frs) →⇩p cfg')"
  using csim_progress_cfg[OF assms] by simp

subsection ‹Progress for accepted programs›

text ‹
  The premise is source well-formedness alone; no compiled graph is involved.  \<^const>‹csim›
  still needs some graph with every body embedded, and the complete graph --- every edge
  present --- embeds anything, so it stands in for the compiler's output.  The finished shape
  is exactly \<^term>‹(SKIP, s, [])›: ‹main› contains no \<^const>‹Return›
  (\<^const>‹no_return›), so a top-level \<^const>‹Unwind› never arises.
›
theorem source_progress:
  assumes wf: "wf_source_program 𝒢 Π"
      and run: "𝒢, Π ⊢ (main_body Π, s0, []) →⇩p⇧* (c, s, frs)"
  shows "(is_SKIP c ∧ frs = []) ∨ (∃cfg'. 𝒢, Π ⊢ (c, s, frs) →⇩p cfg')"
proof -
  define g :: cfg where
    "g = ⦇intra = UNIV, calls = UNIV, cfg_entry = FunctionEntry prog_main_name⦈"
  have pc: "procs_embedded Π g"
    unfolding procs_embedded_def
  proof (intro allI impI)
    fix p decl assume pd: "Π p = Some decl"
    obtain n' en E K where
      cb: "compile Π p (body decl) (Statement (0 + csize (body decl))) 0 = (n', en, E, K)"
      by (metis prod_cases4)
    have "source_com (body decl)" "special_table p = None"
      using wf_source_programD(6,7)[OF wf] pd by (auto simp: source_pi_def)
    with cb 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"
      by (intro exI[of _ "Statement (0 + csize (body decl))"] exI[of _ "0 :: nat"] exI[of _ n']
            exI[of _ en] exI[of _ E] exI[of _ K])
         (simp add: g_def)
  qed
  have main_decl: "Π prog_main_name = Some ⦇formals = [], body = main_body Π⦈"
    by (rule wf_source_programD(2)[OF wf])
  obtain k n en where
    cacc: "compiled_at Π g prog_main_name (body ⦇formals = [], body = main_body Π⦈) k n"
    and ctrl: "control_at Π prog_main_name (body ⦇formals = [], body = main_body Π⦈) k n
                 (body ⦇formals = [], body = main_body Π⦈) en"
    by (rule procs_embedded_activation[OF pc main_decl])
  have base: "Π, g, prog_main_name ⊢ (main_body Π, s0, []) ≈ (en, s0, [])"
    using csim.Base[OF ctrl cacc] by simp
  have safe: "return_safe (main_body Π)"
    using wf_source_programD(8,4)[OF wf] by (rule return_safe_if_no_return)
  from csim_star[OF base pc safe run] obtain dg where "Π, g, prog_main_name ⊢ (c, s, frs) ≈ dg"
    by blast
  then show ?thesis
    by (rule csim_progress) (rule wf_source_programD(5)[OF wf])
qed

end