finish main proof

1 files changed, 128 insertions, 18 deletions

diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 1a4c5757..13ea61a6 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -296,32 +296,145 @@ Qed.
 
 End SYMBOLIC_CTX.
 
-Lemma iblock_step_eqregs stk sp f ib:
-  forall rs rs' m s t
+Lemma tr_inputs_eqregs_list f tbl: forall rs rs' r' ores,
+  (forall r : positive, rs # r = rs' # r) ->
+  (tr_inputs f tbl ores rs) # r' =
+  (tr_inputs f tbl ores rs') # r'.
+Proof.
+  induction tbl as [|pc tbl IHtbl];
+  intros; destruct ores; simpl;
+  rewrite !tr_inputs_get; autodestruct.
+Qed.
+
+Lemma find_function_eqregs rs rs' ros fd:
+  (forall r : positive, rs # r = rs' # r) ->
+  find_function tpge ros rs = Some fd ->
+  find_function tpge ros rs' = Some fd.
+Proof.
+  intros EQREGS; destruct ros; simpl.
+  rewrite EQREGS; auto.
+  autodestruct.
+Qed.
+
+Lemma args_eqregs (args: list reg): forall (rs rs': regset),
+  (forall r : positive, rs # r = rs' # r) ->
+  rs ## args = rs' ## args.
+Proof.
+  induction args; simpl; trivial.
+  intros rs rs' EQREGS; rewrite EQREGS.
+  apply f_equal; eauto.
+Qed.
+
+Lemma f_arg_eqregs (rs rs': regset):
+  (forall r : positive, rs # r = rs' # r) ->
+  (fun r : positive => rs # r) = (fun r : positive => rs' # r).
+Proof.
+  intros EQREGS; apply functional_extensionality; eauto.
+Qed.
+
+Lemma eqregs_update (rs rs': regset) v dest:
+  (forall r, rs # r = rs' # r) ->
+  (forall r, (rs # dest <- v) # r = (rs' # dest <- v) # r).
+Proof.
+  intros EQREGS r; destruct (Pos.eq_dec dest r); subst.
+    * rewrite !Regmap.gss; reflexivity.
+    * rewrite !Regmap.gso; auto.
+Qed.
+
+Local Hint Resolve equiv_stack_refl tr_inputs_eqregs_list find_function_eqregs eqregs_update: core.
+
+Lemma iblock_istep_eqregs_None sp ib: forall rs m rs' rs1 m1
   (EQREGS: forall r, rs # r = rs' # r)
-  (STEP: iblock_step tr_inputs tpge stk f sp rs m ib s t),
-  iblock_step tr_inputs tpge stk f sp rs' m ib s t.
+  (ISTEP: iblock_istep tpge sp rs m ib rs1 m1 None),
+  exists rs1',
+    iblock_istep tpge sp rs' m ib rs1' m1 None
+    /\ (forall r, rs1 # r = rs1' # r).
 Proof.
+  induction ib; intros; inv ISTEP.
+  - repeat econstructor; eauto.
+  - repeat econstructor; eauto.
+    erewrite args_eqregs; eauto.
+  - repeat econstructor; eauto.
+    erewrite args_eqregs; eauto.
+  - repeat econstructor; eauto.
+    erewrite args_eqregs; eauto.
+    rewrite <- EQREGS; eauto.
+  - exploit IHib1; eauto.
+    intros (rs1' & ISTEP1 & EQREGS1).
+    exploit IHib2; eauto.
+    intros (rs2' & ISTEP2 & EQREGS2).
+    eexists; split. econstructor; eauto.
+    eauto.
+  - destruct b.
+    1: exploit IHib1; eauto.
+    2: exploit IHib2; eauto.
+    all:
+      intros (rs1' & ISTEP & EQREGS');
+      eexists; split; try eapply exec_cond;
+      try erewrite args_eqregs; eauto.
+Qed.
 
-Admitted.
+Lemma iblock_step_eqregs stk sp f ib: forall rs rs' m t s
+  (EQREGS: forall r, rs # r = rs' # r)
+  (STEP: iblock_step tr_inputs tpge stk f sp rs m ib t s),
+  exists s',
+    iblock_step tr_inputs tpge stk f sp rs' m ib t s'
+    /\ equiv_state s s'.
+Proof.
+  induction ib; intros;
+  destruct STEP as (rs2 & m2 & fin & ISTEP & FSTEP); inv ISTEP.
+  - inv FSTEP;
+    eexists; split; repeat econstructor; eauto.
+    + destruct (or); simpl; try rewrite EQREGS; constructor; eauto.
+    + erewrite args_eqregs; eauto. repeat econstructor; eauto.
+    + erewrite args_eqregs; eauto. econstructor; eauto.
+    + erewrite f_arg_eqregs; eauto.
+    + destruct res; simpl; eauto.
+    + rewrite <- EQREGS; auto.
+  - exploit IHib1; eauto.
+    + econstructor. do 2 eexists; split; eauto.
+    + intros (s' & STEP & EQUIV). clear FSTEP.
+      destruct STEP as (rs3 & m3 & fin2 & ISTEP & FSTEP).
+      repeat (econstructor; eauto).
+  - exploit iblock_istep_eqregs_None; eauto.
+    intros (rs1' & ISTEP1 & EQREGS1).
+    exploit IHib2; eauto.
+    + econstructor. do 2 eexists; split; eauto.
+    + intros (s' & STEP & EQUIV). clear FSTEP.
+      destruct STEP as (rs3 & m3 & fin2 & ISTEP & FSTEP).
+      eexists; split; eauto.
+      econstructor; do 2 eexists; split; eauto.
+      eapply exec_seq_continue; eauto.
+  - destruct b.
+    1: exploit IHib1; eauto.
+    3: exploit IHib2; eauto.
+    1,3: econstructor; do 2 eexists; split; eauto.
+    all:
+      intros (s' & STEP & EQUIV); clear FSTEP;
+      destruct STEP as (rs3 & m3 & fin2 & ISTEP & FSTEP);
+      eexists; split; eauto; econstructor;
+      do 2 eexists; split; eauto;
+      eapply exec_cond; try erewrite args_eqregs; eauto.
+Qed.
 
-Lemma iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m ibf t s pc
-  (STEP: iblock_step tr_inputs pge stk1 f1 sp rs m ibf.(entry) t s)
+Lemma iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m ibf t s1 pc
+  (STEP: iblock_step tr_inputs pge stk1 f1 sp rs m ibf.(entry) t s1)
   (PC: (fn_code f1) ! pc = Some ibf)
   (EQREGS: forall r : positive, rs # r = rs' # r)
   (STACKS: list_forall2 match_stackframes stk1 stk2)
   (TRANSF: match_function f1 f2)
-  :exists ibf' s',
-       (fn_code f2) ! pc = Some ibf'
-    /\ iblock_step tr_inputs tpge stk2 f2 sp rs' m ibf'.(entry) t s'
-    /\ match_states s s'.
+  :exists ibf' s2,
+    (fn_code f2) ! pc = Some ibf'
+    /\ iblock_step tr_inputs tpge stk2 f2 sp rs' m ibf'.(entry) t s2
+    /\ match_states s1 s2.
 Proof.
   exploit symbolic_simu_ok; eauto. intros (ib2 & PC' & SYMBS).
   exploit symbolic_simu_correct; repeat (eauto; simpl).
-  intros (s' & STEP2 & MS).
-  exists ib2; exists s'. repeat split; auto.
-  eapply iblock_step_eqregs; eauto.
-Admitted.
+  intros (s2 & STEP2 & MS).
+  exploit iblock_step_eqregs; eauto. intros (s3 & STEP3 & EQUIV).
+  clear STEP2. exists ib2; exists s3. repeat split; auto.
+  eapply match_states_equiv; eauto.
+Qed.
 
 Local Hint Constructors step: core.
 
@@ -353,9 +466,6 @@ 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: