Theory Residual_Location

theory Residual_Location
  imports VIMP_Proc_to_CFG
begin

section ‹Where a partly executed command sits in the graph›

text ‹
  Running a command part way leaves a ∗‹residual›: the piece still to execute.
  ‹control_at Π p c0 k n r v› states that residual ‹r› of the fragment ‹c0› --- compiled at
  offset ‹n› with continuation ‹k› --- corresponds to CFG node ‹v›.  It tracks control only;
  store agreement is the simulation relation's business.

  A command that ∗‹reduces to› \<^const>‹SKIP› is located at the continuation ‹k›, because
  \<^const>‹compile› takes the continuation as an input rather than allocating an exit node of
  its own.  A literal source \<^const>‹SKIP› is the exception: it keeps its own statement node
  until its \<^term>‹EA_Nop› edge is taken.

  The relation also locates positions no execution reaches, such as the second half of a
  \<^const>‹Seq› whose first half always returns.  That is harmless: the compiled graph has the
  matching edges there too, since every procedure body ends at an epilogue whose return edge
  \<^const>‹compile_proc› always emits.
›

subsection ‹Located residuals›

text ‹\<^const>‹Restore› and \<^const>‹Unwind› have no clause: they are runtime-only activation
  markers rather than compiled commands.  Once a \<^const>‹Return› fires the CFG is already at
  \<^term>‹FunctionResult p› through the \<^term>‹EA_Ret› edge, and the activation return that
  remains is performed by ‹cstep› popping a frame, not by any fragment node.›

inductive control_at ::
  "'a ptable ⇒ pname ⇒ 'a acom ⇒ cfg_node ⇒ nat ⇒ 'a acom ⇒ cfg_node ⇒ bool"
  for Π :: "'a ptable" and p :: pname
where
  Skip [intro]:
    "control_at Π p (SKIP i) k n (SKIP i) (Statement n)"
| Assign [intro]:
    "control_at Π p (Assign i x a) k n (Assign i x a) (Statement n)"
| AssignDone [intro]:
    "control_at Π p (Assign i x a) k n (SKIP i) k"
| Check [intro]:
    "control_at Π p (VIMP_Proc.gcom.Check i l c) k n (VIMP_Proc.gcom.Check i l c) (Statement n)"
| CheckDone [intro]:
    "control_at Π p (VIMP_Proc.gcom.Check i l c) k n (SKIP i) k"
| SeqLeft [intro]:
    "control_at Π p c1 (Statement (n + csize c1)) n r v ⟹
     control_at Π p (Seq c1 c2) k n (Seq r c2) v"
| SeqRight [intro]:
    "control_at Π p c2 k (n + csize c1) r v ⟹
     control_at Π p (Seq c1 c2) k n r v"
| IfHead [intro]:
    "control_at Π p (If i b c1 c2) k n (If i b c1 c2) (Statement n)"
| IfLeft [intro]:
    "control_at Π p c1 k (Suc n) r v ⟹ ¬ is_SKIP c1 ⟹
     control_at Π p (If i b c1 c2) k n r v"
| IfRight [intro]:
    "control_at Π p c2 k (Suc n + csize c1) r v ⟹ ¬ is_SKIP c2 ⟹
     control_at Π p (If i b c1 c2) k n r v"
| IfDone [intro]:
    "c1 = SKIP j ∨ c2 = SKIP j ⟹ control_at Π p (If i b c1 c2) k n (SKIP j) k"
| WhileHead [intro]:
    "control_at Π p (While i b c) k n (While i b c) (Statement n)"
| WhileUnfolded [intro]:
    "control_at Π p (While i b c) k n
       (If i b (Seq c (While i b c)) (SKIP i)) (Statement n)"
| WhileBody [intro]:
    "control_at Π p c (Statement n) (Suc n) r v ⟹
     control_at Π p (While i b c) k n (Seq r (While i b c)) v"
| WhileDone [intro]:
    "control_at Π p (While i b c) k n (SKIP i) k"
| CallHead [intro]:
    "control_at Π p (Call i dst q actuals) k n (Call i dst q actuals) (Statement n)"
| CallDone [intro]:
    "control_at Π p (Call i dst q actuals) k n (SKIP i) k"
| ReturnHead [intro]:
    "control_at Π p (Return i e) k n (Return i e) (Statement n)"


text ‹Inversion by the shape of the fragment ‹c0›, which is what every consumer knows and
  cases on.  \<^const>‹Seq›, \<^const>‹If› and \<^const>‹While› stay plain ‹[elim]› because their
  clauses recurse into a sub-fragment, and an eager rule would chase the nesting; the rest
  are ‹[elim!]›.  \<^const>‹Restore› and \<^const>‹Unwind› have no clause at all, so inverting
  them is outright refutation --- that is what makes ‹control_at_not_unwind› a one-liner.›
inductive_cases control_at_SkipE [elim!]:    "control_at Π p (SKIP i) k n r v"
inductive_cases control_at_AssignE [elim!]:  "control_at Π p (Assign i x a) k n r v"
inductive_cases control_at_CheckE [elim!]:
  "control_at Π p (VIMP_Proc.gcom.Check i l b) k n r v"
inductive_cases control_at_SeqE [elim]:      "control_at Π p (Seq c1 c2) k n r v"
inductive_cases control_at_IfE [elim]:       "control_at Π p (If i b c1 c2) k n r v"
inductive_cases control_at_WhileE [elim]:    "control_at Π p (While i b c) k n r v"
inductive_cases control_at_CallE [elim!]:
  "control_at Π p (Call i dst q actuals) k n r v"
inductive_cases control_at_ReturnE [elim!]:  "control_at Π p (Return i e) k n r v"
inductive_cases control_at_RestoreE [elim!]: "control_at Π p (Restore i) k n r v"
inductive_cases control_at_UnwindE [elim!]:  "control_at Π p (Unwind i) k n r v"


subsection ‹Initial location›

text ‹A source command is initially located at its entry node ‹Statement n›.›
lemma control_at_initial:
  "source_com c ⟹ control_at Π p c k n c (Statement n)"
  by (induction c arbitrary: k n) auto

subsection ‹Normal completion is located at the continuation›

text ‹A completed residual is at the continuation already, except for a source \<^const>‹SKIP›,
  whose own node still carries one store-preserving \<^const>‹EA_Nop› edge to it: both
  branches of a conditional are compiled with the same continuation, so a completed branch
  is at ‹k› directly.›
lemma compile_control_at_SKIP_exit_path:
  "control_at Π p c0 k n (SKIP i) v ⟹ compile Π p c0 k n = (n', en, E, K)
   ⟹ E ⊆ intra g ⟹ intra_path g (v, s) (k, s)"
proof (induction c0 k n "SKIP i :: 'a acom" v arbitrary: n' en E K rule: control_at.induct)
  case (Skip k n)
  then have "(Statement n, EA_Nop, k) ∈ intra g" by auto
  then show ?case by (rule intra_path_nop)
next
  case (SeqRight c2 k n c1 v)
  from SeqRight.prems(1) obtain n2 E2 K2 where
    c2: "compile Π p c2 k (n + csize c1) = (n2, Statement (n + csize c1), E2, K2)"
    and "E2 ⊆ E"
    by (rule compile_SeqE) blast
  with SeqRight.prems(2) show ?case by (intro SeqRight.hyps(2)[OF c2]) blast
next
  case (IfLeft c1 k n v i b c2)
  from IfLeft.prems(1) obtain n1 E1 K1 where
    c1: "compile Π p c1 k (Suc n) = (n1, Statement (Suc n), E1, K1)" and "E1 ⊆ E"
    by (rule compile_If_leftE[OF _ IfLeft.hyps(3)]) blast
  with IfLeft.prems(2) show ?case by (intro IfLeft.hyps(2)[OF c1]) blast
next
  case (IfRight c2 k n c1 v i b)
  from IfRight.prems(1) obtain n2 E2 K2 where
    c2: "compile Π p c2 k (Suc n + csize c1) = (n2, Statement (Suc n + csize c1), E2, K2)"
    and "E2 ⊆ E"
    by (rule compile_If_rightE[OF _ IfRight.hyps(3)]) blast
  with IfRight.prems(2) show ?case by (intro IfRight.hyps(2)[OF c2]) blast
qed simp_all

subsection ‹Located residuals remain source commands›

text ‹Execution never introduces the runtime-only commands into a residual: whatever remains
  of a source procedure is itself source syntax.  The simulation needs this to rule out the
  frame-popping cases when it is reasoning inside a procedure body.›

lemma control_at_source_com:
  assumes "control_at Π p c0 k n r v" and "source_com c0"
  shows "source_com r"  using assms
  by (induction rule: control_at.induct) auto

lemma source_com_no_Restore:
  "source_com c ⟹ ¬ is_Restore c"
  by auto

end