some advance in sched proof

1 files changed, 92 insertions, 24 deletions

diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index aaa2bf80..c7ecb0dc 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -40,9 +40,10 @@ Inductive match_fundef: fundef -> fundef -> Prop :=
 
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
   | match_stackframe_intro 
-      res f sp pc rs f'
+      res f sp pc rs rs' f'
+      (EQREGS: forall r, rs # r = rs' # r)
       (TRANSF: match_function f f')
-      : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs).
+      : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs').
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro 
@@ -62,6 +63,24 @@ Inductive match_states: state -> state -> Prop :=
       : match_states (Returnstate st v m) (Returnstate st' v m)
    .
 
+Lemma match_stack_equiv stk1 stk2:
+  list_forall2 match_stackframes stk1 stk2 -> 
+  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
+  list_forall2 match_stackframes stk1 stk3.
+Proof.
+  (*Local Hint Resolve match_stackframes_equiv: core.*)
+  induction 1; intros stk3 EQ; inv EQ; constructor; eauto.
+  inv H3; inv H; econstructor; eauto.
+  intros; rewrite <- EQUIV; auto.
+Qed.
+
+Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3.
+Proof.
+  Local Hint Resolve match_stack_equiv: core.
+  destruct 1; intros EQ; inv EQ; econstructor; eauto.
+  intros; rewrite <- EQUIV; auto.
+Qed.
+
 Lemma transf_function_correct f f':
   transf_function f = OK f' -> match_function f f'.
 Proof.
@@ -113,43 +132,89 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
-(* 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
+Theorem symbolic_simu_ssem stk1 stk2 f1 f2 ib1 ib2:
+  forall (ctx: simu_proof_context f1 f2) t s,
+  sem_sstate (bctx1 ctx) stk1 t s (sexec f1 ib1) ->
+  exists s',
+    sem_sstate (bctx2 ctx) stk2 t s' (sexec f2 ib2)
+    /\ match_states s s'.
+Admitted.
+
+Theorem symbolic_simu_correct stk1 stk2 f1 f2 ib1 ib2:
+  symbolic_simu f1 f2 ib1 ib2 ->
+  forall (ctx: simu_proof_context f1 f2) t s, iblock_step tr_inputs (sge1 ctx) stk1 f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s ->
+  exists s',
+    iblock_step tr_inputs (sge2 ctx) stk2 f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s'
+    /\ match_states s s'.
+Proof.
+  unfold symbolic_simu, sstate_simu.
+  intros SIMU ctx t s1 STEP1.
+  exploit (sexec_correct (bctx1 ctx)); simpl; eauto.
+  intros SST1. exploit sem_sstate_run; eauto.
+  intros (sis1 & sfv1 & rs & m & OUTC1 & SIS1 & SV1).
+  exploit sem_si_ok; eauto. intros SOK.
+  intros; exploit SIMU; eauto.
+  intros (sis2 & sfv2 & OUTC2 & SSIMU & SEM).
+  exploit symbolic_simu_ssem; eauto.
+  intros (s2 & SST2 & MS).
+  exploit (sexec_exact (bctx2 ctx)); simpl; eauto.
+  intros (s3 & STEP & EQUIV).
+  exists s3. intuition eauto.
+  eapply match_states_equiv; eauto.
+Qed.
+
+(*
+Lemma iblock_istep_simulation_None stk1 stk2 f f' sp pc rs1 m rs1' m' rs2 ib1 ibf2 s
+  (ISTEP: iblock_istep pge sp rs1 m ib1 rs1' m' None)
+  (PC: (fn_code f') ! pc = Some ibf2)
+  (EQREGS: forall r : positive, rs1 # r = rs2 # r)
+  (STACKS: list_forall2 match_stackframes stk1 stk2)
+  (TRANSF: match_function f f')
+  :exists rs2' s',
+       iblock_istep_run tpge sp ibf2.(entry) rs2 m = Some (out rs2' m' None)
+    /\ match_states s s'.
+Proof.
+  induction ib1; inv ISTEP; eauto.
+Admitted.
+
+Lemma iblock_istep_simulation_Some stk1 stk2 f f' sp ib1: forall fin ibf2 rs1 m rs1' m' rs2 pc 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)
+  (FSTEP: final_step tr_inputs pge stk1 f sp rs1' m' fin t s)
+  (PC: (fn_code f') ! pc = Some ibf2)
   (EQREGS: forall r : positive, rs1 # r = rs2 # r)
-  (STACKS : list_forall2 match_stackframes stk1 stk2)
-  (TRANSF : match_function f f')
-  :exists ib2 rs2' s',
-       (fn_code f') ! pc = Some ib2
-    /\ iblock_istep tpge sp rs2 m ib2.(entry) rs2' m' (Some fin)
+  (STACKS: list_forall2 match_stackframes stk1 stk2)
+  (TRANSF: match_function f f'),
+  exists rs2' s',
+       iblock_istep_run tpge sp ibf2.(entry) rs2 m = Some (out 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.
+  induction ib1; simpl; try_simplify_someHyps; inv ISTEP; eauto; intros.
   - (* BF *)
     admit.
   - (* Bseq continue *)
-    eauto.
+    exploit iblock_istep_simulation_None; eauto.
+    intros (rs2' & s' & ISTEP & MS).
+    admit.
+  - 
 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)
+ *)
+Lemma iblock_step_simulation stk1 stk2 f f' sp rs rs' m ibf t s pc
+  (STEP: iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s)
   (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.
+  :exists ibf' s',
+       (fn_code f') ! pc = Some ibf'
+    /\ iblock_step tr_inputs tpge stk2 f' sp rs' m ibf'.(entry) t s'
+    /\ match_states s s'.
 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.
+  inversion TRANSF. apply symbolic_simu_ok in PC as SYMB.
+  destruct SYMB as (ibf2 & PC' & SYMBS). clear symbolic_simu_ok.
+  unfold symbolic_simu, sstate_simu in SYMBS.
+Admitted.
 
 Local Hint Constructors step: core.
 
@@ -181,6 +246,9 @@ Proof.
     eexists; split.
     + econstructor.
     + inv H1. econstructor; eauto.
+      intros; destruct (Pos.eq_dec res' r); subst.
+      * rewrite !Regmap.gss; reflexivity.
+      * rewrite !Regmap.gso; auto.
 Qed.
 
 Theorem transf_program_correct: