Finish implem proof, need to adapt scheduler proof

1 files changed, 54 insertions, 3 deletions

diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index 12840f62..63114125 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -2,7 +2,7 @@ Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import RTL Op Registers OptionMonad BTL.
 
-Require Import Errors Linking BTL_SEtheory.
+Require Import Errors Linking BTL_SEtheory BTL_SEimpl.
 
 (** External oracle *)
 Axiom scheduler: BTL.function -> BTL.code.
@@ -48,18 +48,69 @@ Record match_function (f1 f2: BTL.function): Prop := {
 
 Local Open Scope error_monad_scope.
 
-Definition check_symbolic_simu (f tf: BTL.function): res unit := OK tt. (* TODO: fixme *)
+Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res unit :=
+  match lpc with
+  | nil => OK tt
+  | pc :: lpc' =>
+      match (fn_code f1)!pc, (fn_code f2)!pc with
+      | Some ibf1, Some ibf2 =>
+          do _ <- simu_check f1 f2 ibf1 ibf2;
+          check_symbolic_simu_rec f1 f2 lpc'
+      | _, _ => Error (msg "check_symbolic_simu_rec: code tree mismatch")
+      end
+  end.
+
+Definition check_symbolic_simu (f1 f2: BTL.function): res unit :=
+  check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))).
+
+Lemma check_symbolic_simu_rec_input_equiv lpc: forall f1 f2 x,
+  check_symbolic_simu_rec f1 f2 lpc = OK x ->
+  lpc = (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))) ->
+  equiv_input_regs f1 f2.
+Proof.
+Admitted.
+(*
+  unfold equiv_input_regs; induction lpc; simpl; intros f1 f2 x X EQL1.
+  - destruct (map _ _) eqn:EQL2; inv X; intuition;
+    symmetry in EQL1; apply map_eq_nil in EQL1; apply map_eq_nil in EQL2.
+    + destruct (fn_code f1), (fn_code f2); simpl in *; auto.
+      inv EQL2.
+      unfold PTree.elements in EQL1.
+    + admit.
+    + 
+  destruct ((fn_code f1) ! a), ((fn_code f2) ! a); monadInv X.
+  eapply IHlpc; eauto.
+Qed.
+ *)
 
 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.
+  eapply check_symbolic_simu_rec_input_equiv; eauto.
+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 ->
+       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.
+Qed.
+   *)
 
 Lemma check_symbolic_simu_correct x f1 f2:
   check_symbolic_simu f1 f2 = OK x ->
   forall pc ib1, (fn_code f1)!pc = Some ib1 ->
        exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2).
-Admitted.
+Proof.
+  unfold check_symbolic_simu; intros X pc ib1 PC.
+  eapply check_symbolic_simu_rec_correct; eauto.
+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