nothing admitted !!

2 files changed, 25 insertions, 17 deletions

diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index a3053add..0662a357 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -62,31 +62,35 @@ Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res uni
 
 Definition erase_input_regs f1 f2 :=
   let code := PTree.map (fun pc ibf =>
-    let oibf := match (fn_code f1)!pc with
+    let oibf := match (fn_code f2)!pc with
                 | None => ibf
                 | Some oibf => oibf
                 end in
-    let regs := oibf.(input_regs) in
-    {| entry:= ibf.(entry); input_regs := regs; binfo := ibf.(binfo) |}) (fn_code f2) in
+    {| entry:= oibf.(entry); input_regs := ibf.(input_regs); binfo := oibf.(binfo) |}) (fn_code f1) in
   BTL.mkfunction (fn_sig f2) (fn_params f2) (fn_stacksize f2) code (fn_entrypoint f2).
 
 Lemma erase_input_regs_correct f1 f2 f3:
   erase_input_regs f1 f2 = f3 ->
   equiv_input_regs f1 f3.
 Proof.
-  unfold erase_input_regs; destruct f3; simpl; intros.
-  unfold equiv_input_regs; intuition auto. simpl.
-Admitted.
+  unfold erase_input_regs; simpl; intros.
+  unfold equiv_input_regs; intuition auto.
+  - subst; simpl. rewrite PTree.gmap, H0; simpl; auto.
+  - subst; simpl in H0. rewrite PTree.gmap in H0.
+    destruct ((fn_code f1)!pc) eqn:EQF; simpl in H0; inv H0; auto.
+  - subst; simpl in H1. rewrite PTree.gmap in H1.
+    rewrite H0 in H1; simpl in H1; inv H1; simpl; auto.
+Qed.
+Global Opaque erase_input_regs.
 
 Definition check_symbolic_simu (f1 f2: BTL.function): res unit :=
-  (*let f3 := erase_input_regs f1 f2 in*)
   check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))).
 
-Lemma check_symbolic_simu_input_equiv x f1 f2:
-  check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2.
-Proof.
-  unfold check_symbolic_simu; simpl; intros X.
-Admitted.
+Definition transf_function (f: BTL.function) :=
+  let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f) in
+  let tf' := erase_input_regs f tf in
+  do _ <- check_symbolic_simu f tf';
+  OK tf'.
 
 Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x,
   check_symbolic_simu_rec f1 f2 lpc = OK x ->
@@ -111,10 +115,13 @@ Proof.
   apply PTree.elements_correct in PC. eapply (in_map fst) in PC; auto.
 Qed.
 
-Definition transf_function (f: BTL.function) :=
-  let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f) in
-  do _ <- check_symbolic_simu f tf;
-  OK tf.
+Lemma check_symbolic_simu_input_equiv x f1 f2:
+  transf_function f1 = OK f2 ->
+  check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2.
+Proof.
+  unfold transf_function; intros TRANSF X; monadInv TRANSF.
+  exploit erase_input_regs_correct; eauto.
+Qed.
 
 Definition transf_fundef (f: fundef) : res fundef :=
   transf_partial_fundef (fun f => transf_function f) f.
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 05028f11..27efe56f 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -95,7 +95,8 @@ Qed.
 Lemma transf_function_correct f f':
   transf_function f = OK f' -> match_function f f'.
 Proof.
-  unfold transf_function. intros H. monadInv H.
+  unfold transf_function. intros H.
+  assert (OH: transf_function f = OK f') by auto. monadInv H.
   econstructor; eauto.
   eapply check_symbolic_simu_input_equiv; eauto.
   eapply check_symbolic_simu_correct; eauto.