End of main scheduling proof

3 files changed, 90 insertions, 59 deletions

diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index 10f780e2..c50eb364 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -52,6 +52,7 @@ Definition check_symbolic_simu (f tf: BTL.function): res unit := OK tt. (* TODO:
 
 Lemma check_symbolic_simu_input_equiv x f1 f2:
   check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2.
+Proof.
 Admitted.
 
 Lemma check_symbolic_simu_correct x f1 f2:
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 85b185c5..6963ee8b 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -105,6 +105,11 @@ Qed.
 Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.
 Proof.
+  intros TRANSF; destruct f; simpl. monadInv TRANSF.
+  + exploit transf_function_correct; eauto.
+    (*intros (dupmap & MATCH_F).*)
+    (*eapply match_Internal; eauto.*)
+  (*+ eapply match_External.*)
 Admitted.
 
 Lemma function_ptr_preserved:
@@ -196,58 +201,79 @@ Theorem symbolic_simu_ssem stk1 stk2 st st' s t:
     /\ match_states s s'.
 Proof.
   intros SIMU SST1 STACKS MF. inversion MF.
-  (*destruct SST1.*)
-  (*- [> sem_Sfinal <]*)
-    (*admit.*)
-  (*- [> sem_Scond <]*)
-
   exploit sem_sstate_run; eauto.
   intros (sis1 & sfv1 & rs' & m' & SOUT1 & SIS1 & SF).
   exploit sem_si_ok; eauto. intros SOK.
-  exploit SIMU; simpl; eauto. (* rewrite SEVAL; eauto. *)
+  exploit SIMU; simpl; eauto.
   intros (sis2 & sfv2 & SOUT2 & SSIMU & SFVSIM).
   remember SIS1 as EQSFV. clear HeqEQSFV.
   eapply SFVSIM in EQSFV.
-
-
-  exploit SSIMU; eauto.
-  intros SIS2.
-
-
-
+  exploit SSIMU; eauto. intros SIS2.
   destruct SIS1 as (PRE1 & SMEM1 & SREGS1).
   try_simplify_someHyps; intros.
-  (*exploit sem_sfval_equiv; eauto.*)
-  (*intros (s' & SF' & EQUIV).*)
   set (EQSFV2:=sfv2).
-  inversion EQSFV; subst.
-  - 
-  inversion SF; subst.
-  exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
-  + erewrite <- str_regs_equiv; simpl; eauto.
-  + econstructor.
-  + intros SST2. eexists; split; eauto.
-    econstructor; simpl; eauto.
-    erewrite equiv_input_regs_tr_inputs; eauto.
-
-  - 
-  inversion SF; subst.
-  exploit sfind_function_preserved; eauto. intros (fd' & SFIND & FUND).
-  exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
-  + erewrite <- str_regs_equiv; eauto.
-  + econstructor; eauto.
-    * apply function_sig_translated; auto.
-    * erewrite <- ARGS; eauto.
-  + intros SST2. eexists; split; eauto.
-    econstructor; simpl; eauto.
-    * erewrite equiv_input_regs_tr_inputs; eauto.
-      repeat (econstructor; eauto).
-    * apply transf_fundef_correct; auto.
-  - 
-      
-
-admit.
-Admitted.
+  inversion EQSFV; subst; inversion SF; subst.
+  - (* goto *)
+    exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+    + erewrite <- str_regs_equiv; simpl; eauto.
+    + econstructor.
+    + intros SST2. eexists; split; eauto.
+      econstructor; simpl; eauto.
+      erewrite equiv_input_regs_tr_inputs; eauto.
+  - (* call *)
+    exploit sfind_function_preserved; eauto. intros (fd' & SFIND & FUND).
+    exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+    + erewrite <- str_regs_equiv; eauto.
+    + econstructor; eauto.
+      * apply function_sig_translated; auto.
+      * erewrite <- ARGS; eauto.
+    + intros SST2. eexists; split; eauto.
+      econstructor; simpl; eauto.
+      * erewrite equiv_input_regs_tr_inputs; eauto.
+        repeat (econstructor; eauto).
+      * apply transf_fundef_correct; auto.
+  - (* tailcall *)
+    exploit sfind_function_preserved; eauto. intros (fd' & SFIND & FUND).
+    exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+    + econstructor; eauto.
+      * apply function_sig_translated; auto.
+      * simpl; erewrite <- preserv_fnstacksize; eauto.
+      * erewrite <- ARGS; eauto.
+    + intros SST2. eexists; split; eauto.
+      econstructor; simpl; eauto.
+      apply transf_fundef_correct; auto.
+  - (* builtin *)
+    exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+    + erewrite <- str_regs_equiv; simpl; eauto.
+    + econstructor.
+      * eapply eval_builtin_sargs_preserved.
+        eapply senv_preserved.
+        eapply eval_list_builtin_sval_correct; eauto.
+        inv BARGS.
+        erewrite <- eval_list_builtin_sval_preserved in H0; auto.
+      * simpl in *; eapply external_call_symbols_preserved; eauto.
+        eapply senv_preserved.
+    + intros SST2. eexists; split; eauto.
+      econstructor; simpl; eauto.
+      erewrite equiv_input_regs_tr_inputs; eauto.
+  - (* jumptable *)
+    exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+    + erewrite <- str_regs_equiv; simpl; eauto.
+    + econstructor; eauto.
+      rewrite <- VAL; auto.
+    + intros SST2. eexists; split; eauto.
+      econstructor; simpl; eauto.
+      erewrite equiv_input_regs_tr_inputs; eauto.
+  - (* return *)
+    exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+    + econstructor; eauto.
+      * simpl; erewrite <- preserv_fnstacksize; eauto.
+      * inv OPT; eauto.
+        rewrite <- SIMU0; auto.
+    + intros SST2. eexists; split; eauto.
+      econstructor; simpl; eauto.
+  Unshelve. all: auto.
+Qed.
 
 Theorem symbolic_simu_correct stk1 stk2 ibf1 ibf2 s t:
   sstate_simu ctx (sexec f1 ibf1.(entry)) (sexec f2 ibf2.(entry)) ->
@@ -269,17 +295,21 @@ Proof.
   eapply match_states_equiv; eauto.
 Qed.
 
-Lemma iblock_step_eqregs tr ge stk f sp ib:
-  forall rs m rs' t s,
-  (forall r, rs # r = rs' # r) ->
-  iblock_step tr ge stk f sp rs m ib t s <->
-  iblock_step tr ge stk f sp rs' m ib t s.
+End SYMBOLIC_CTX.
+
+Lemma iblock_step_eqregs sp ib:
+  forall rs rs'
+  (EQREGS: forall r, rs # r = rs' # r)
+  fin m rs2 m2 (ISTEP: iblock_istep tpge sp rs m ib rs2 m2 (Some fin)),
+  iblock_istep tpge sp rs' m ib rs2 m2 (Some fin).
 Proof.
-  induction ib; try_simplify_someHyps.
+  induction ib; intros; inv ISTEP.
+  - 
+    admit.
+  - econstructor; eauto.
+  - econstructor. eapply IHib1; eauto.
 Admitted.
 
-End SYMBOLIC_CTX.
-
 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)
   (PC: (fn_code f1) ! pc = Some ibf)
@@ -291,12 +321,13 @@ Lemma iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m ibf t s pc
     /\ iblock_step tr_inputs tpge stk2 f2 sp rs' m ibf'.(entry) t s'
     /\ match_states s s'.
 Proof.
-  (*destruct STEP as (rs1 & m1 & fin & ISTEP & FSTEP).*)
   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.
-  erewrite iblock_step_eqregs; eauto.
+  exists ib2; exists s'. repeat split; auto.
+  destruct STEP2 as (rs2 & m2 & fin & ISTEP2 & FSTEP2).
+  unfold iblock_step. exists rs2; exists m2; exists fin.
+  split; auto.
 Admitted.
 
 Local Hint Constructors step: core.
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index f5c2f3db..4af5668c 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -252,11 +252,10 @@ Lemma transf_function_correct f f':
   transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
 Proof.
   unfold transf_function; unfold bind. repeat autodestruct.
-  intros H _ _ X. inversion X; subst; clear X.
-(*
-  eexists; eapply verify_function_correct; simpl; eauto.
-*)
-Admitted.
+  intros LIVE VER _ _ X. inv X. eexists; econstructor.
+  - eapply verify_function_correct; simpl; eauto.
+  - unfold liveness_ok_function; destruct u0; auto.
+Qed.
 
 Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.