Preparation for scheduling proof, main lemmas ok

1 files changed, 40 insertions, 13 deletions

diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index f186581f..aaa2bf80 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -46,11 +46,11 @@ Inductive match_stackframes: stackframe -> stackframe -> Prop :=
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro 
-      st f sp pc rs m st' f'
-      (*(ENTRY: (fn_code f) ! pc = Some ibf)*)
+      st f sp pc rs rs' m st' f'
+      (EQREGS: forall r, rs # r = rs' # r)
       (STACKS: list_forall2 match_stackframes st st')
       (TRANSF: match_function f f')
-      : match_states (State st f sp pc rs m) (State st' f' sp pc rs m)
+      : match_states (State st f sp pc rs m) (State st' f' sp pc rs' m)
   | match_states_call
       st st' f f' args m
       (STACKS: list_forall2 match_stackframes st st')
@@ -113,17 +113,44 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
-Lemma iblock_step_simulation stk1 stk2 f f' sp rs m ibf t s1 pc
-  (STEP : iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s1)
-  (ENTRY : (fn_code f) ! pc = Some ibf)
+(* TODO gourdinl
+   generalize with a None version of the lemma *)
+Lemma iblock_istep_simulation stk1 stk2 f f' sp pc fin rs1 m rs1' m' rs2 ib1 t s
+  (ISTEP: iblock_istep pge sp rs1 m ib1 rs1' m' (Some fin))
+  (FSTEP : final_step tr_inputs pge stk1 f sp rs1' m' fin t s)
+  (EQREGS: forall r : positive, rs1 # r = rs2 # r)
   (STACKS : list_forall2 match_stackframes stk1 stk2)
   (TRANSF : match_function f f')
-  :exists s2 : state,
-    (fn_code f') ! pc = Some ibf /\
-    iblock_step tr_inputs tpge stk2 f' sp rs m ibf.(entry) t s2 /\
-    match_states s1 s2.
+  :exists ib2 rs2' s',
+       (fn_code f') ! pc = Some ib2
+    /\ iblock_istep tpge sp rs2 m ib2.(entry) rs2' m' (Some fin)
+    /\ final_step tr_inputs tpge stk2 f' sp rs2' m' fin t s'
+    /\ match_states s s'.
+Proof.
+  induction ib1; inv ISTEP; eauto.
+  - (* BF *)
+    admit.
+  - (* Bseq continue *)
+    eauto.
 Admitted.
 
+Lemma iblock_step_simulation stk1 stk2 f f' sp rs rs' m ibf t s1 pc
+  (STEP: iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s1)
+  (PC: (fn_code f) ! pc = Some ibf)
+  (EQREGS: forall r : positive, rs # r = rs' # r)
+  (STACKS: list_forall2 match_stackframes stk1 stk2)
+  (TRANSF: match_function f f')
+  :exists ibf' s2,
+    (fn_code f') ! pc = Some ibf' /\
+    iblock_step tr_inputs tpge stk2 f' sp rs' m ibf'.(entry) t s2 /\
+    match_states s1 s2.
+Proof.
+  destruct STEP as (rs1 & m1 & fin & ISTEP & FSTEP).
+  exploit iblock_istep_simulation; eauto.
+  intros (ibf2 & rs2' & s' & PC' & ISTEP' & FSTEP' & MS').
+  repeat eexists; eauto.
+Qed.
+
 Local Hint Constructors step: core.
 
 Theorem step_simulation s1 s1' t s2
@@ -133,11 +160,11 @@ Theorem step_simulation s1 s1' t s2
     step tr_inputs tpge s2 t s2'
   /\ match_states s1' s2'.
 Proof.
-  destruct STEP as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; inv MS.
+  destruct STEP as [stack ibf f sp n rs m t s PC STEP | | | ]; inv MS.
   - (* iblock *)
-    simplify_someHyps. intros ENTRY.
+    simplify_someHyps. intros PC.
     exploit iblock_step_simulation; eauto.
-    intros (s2 & ENTRY2 & STEP2 & MS2). 
+    intros (ibf' & s2 & PC2 & STEP2 & MS2). 
     eexists; split; eauto.
   - (* function internal *)
     inversion TRANSF as [xf tf MF |]; subst.