proof for symbolic simu, need to finish equiv_inputs

3 files changed, 31 insertions, 23 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index 34f8eb1f..d6cdff59 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -1459,22 +1459,21 @@ Qed.
 Hint Resolve rst_simu_check_correct: wlp.
 Global Opaque rst_simu_check.
 
-(* TODO do we really need both functions *)
-Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit :=
+Definition simu_check_single (f1 f2: function) (ibf1 ibf2: iblock_info): ?? unit :=
   (* creating the hash-consing tables *)
   DO hC_sval <~ hCons hSVAL;;
   DO hC_list_hsval <~ hCons hLSVAL;;
   DO hC_hsmem <~ hCons hSMEM;;
   let hrexec := hrexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in
   (* performing the hash-consed executions *)
-  DO hst1 <~ hrexec f1 ib1;;
-  DO hst2 <~ hrexec f2 ib2;;
+  DO hst1 <~ hrexec f1 ibf1.(entry);;
+  DO hst2 <~ hrexec f2 ibf2.(entry);;
   (* comparing the executions *)
   rst_simu_check hst1 hst2.
 
-Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock):
-  WHEN simu_check_single f1 f2 ib1 ib2 ~> _ THEN
-  symbolic_simu f1 f2 ib1 ib2.
+Lemma simu_check_single_correct (f1 f2: function) (ibf1 ibf2: iblock_info):
+  WHEN simu_check_single f1 f2 ibf1 ibf2 ~> _ THEN
+  symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry).
 Proof. (* TODO *)
   unfold symbolic_simu; wlp_simplify.
   eapply rst_simu_correct; eauto.
@@ -1487,12 +1486,12 @@ Global Hint Resolve simu_check_single_correct: wlp.
 Program Definition aux_simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): ?? bool :=
    DO r <~ 
      (TRY 
-       simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);; 
+       simu_check_single f1 f2 ibf1 ibf2;; 
        RET true
       CATCH_FAIL s, _ =>
        println ("simu_check_failure:" +; s);;
        RET false
-       ENSURE (fun b => b=true -> ibf1.(input_regs) = ibf2.(input_regs) -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry)));;
+       ENSURE (fun b => b=true -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry)));;
    RET (`r).
 Obligation 1.
   split; wlp_simplify. discriminate.
@@ -1500,7 +1499,7 @@ Qed.
 
 Lemma aux_simu_check_correct (f1 f2: function) (ibf1 ibf2: iblock_info):
   WHEN aux_simu_check f1 f2 ibf1 ibf2 ~> b THEN
-  b=true -> ibf1.(input_regs) = ibf2.(input_regs) -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry).
+  b=true -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry).
 Proof.
   unfold aux_simu_check; wlp_simplify.
   destruct exta; simpl; auto.
@@ -1515,3 +1514,13 @@ Definition simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): res unit :=
   | Some true => OK tt
   | _ => Error (msg "simu_check has failed")
   end.
+
+Lemma simu_check_correct f1 f2 ibf1 ibf2:
+  simu_check f1 f2 ibf1 ibf2 = OK tt ->
+  symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry).
+Proof.
+  unfold simu_check.
+  destruct (unsafe_coerce (aux_simu_check f1 f2 ibf1 ibf2)) as [[|]|] eqn:Hres; simpl; try discriminate.
+  intros; eapply aux_simu_check_correct; eauto.
+  eapply unsafe_coerce_not_really_correct; eauto.
+Qed.
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index 63114125..e7d2b37f 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -92,16 +92,16 @@ Qed.
 
 Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x,
   check_symbolic_simu_rec f1 f2 lpc = OK x ->
-  forall pc ib1, (fn_code f1)!pc = Some ib1 ->
+  forall pc ib1, (fn_code f1)!pc = Some ib1 /\ In pc lpc ->
        exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2).
 Proof.
-Admitted.
-  (*
-  induction lpc; simpl; intros f1 f2 x X pc ib1 PC; try (inv X; fail).
-  destruct ((fn_code f1) ! pc), ((fn_code f2) ! pc); inv X.
-  eapply IHlpc; eauto.
+  induction lpc; simpl; intros f1 f2 x X pc ib1 (PC & HIN); try contradiction.
+  destruct HIN; subst.
+  - rewrite PC in X; destruct ((fn_code f2)!pc); monadInv X.
+    exists i; split; auto. destruct x0. eapply simu_check_correct; eauto.
+  - destruct ((fn_code f1)!a), ((fn_code f2)!a); monadInv X.
+    eapply IHlpc; eauto.
 Qed.
-   *)
 
 Lemma check_symbolic_simu_correct x f1 f2:
   check_symbolic_simu f1 f2 = OK x ->
@@ -109,7 +109,8 @@ Lemma check_symbolic_simu_correct x f1 f2:
        exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2).
 Proof.
   unfold check_symbolic_simu; intros X pc ib1 PC.
-  eapply check_symbolic_simu_rec_correct; eauto.
+  eapply check_symbolic_simu_rec_correct; intuition eauto.
+  apply PTree.elements_correct in PC. eapply (in_map fst) in PC; auto.
 Qed.
 
 Definition transf_function (f: BTL.function) :=
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 91e650e8..05028f11 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -105,12 +105,10 @@ Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.
 Proof.
   intros TRANSF; destruct f; simpl; inv TRANSF.
-Admitted. (*
-  + exploit transf_function_correct; eauto.
-    econstructor. intros MATCH_F.
-    eapply match_Internal; eauto.
+  + monadInv H0. exploit transf_function_correct; eauto.
+    constructor; auto.
   + eapply match_External.
-             Qed.*)
+Qed.
 
 Lemma function_ptr_preserved:
   forall v f,