some advance

1 files changed, 39 insertions, 8 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 97ac75fb..8f892020 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -107,17 +107,45 @@ Proof.
 Qed.
 
 (* suggestion *)
-Lemma iblock_stepi_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
+Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
  (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin):
- forall cfg' pc0 opc isfst
- (MIB: match_iblock dupmap cfg' isfst pc0 ib opc)
+ forall pc0 opc isfst
+ (MIB: match_iblock dupmap (RTL.fn_code f') isfst pc0 ib opc)
  ,
   match ofin with 
   | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
   | Some fin => True (* TODO: A CHANGER *)
   end.
 Proof.
-  induction IBIS; simpl; auto.
+  induction IBIS; simpl; auto;
+  intros.
+  - inv MIB. exists pc'; split; auto.
+    apply plus_one. apply exec_Inop; trivial.
+  - inv MIB. exists pc'; split; auto.
+    apply plus_one. eapply exec_Iop; eauto.
+    erewrite <- eval_operation_preserved; eauto.
+    intros; rewrite symbols_preserved; trivial.
+  - inv MIB. exists pc'; split; auto.
+    apply plus_one. eapply exec_Iload; eauto.
+    erewrite <- eval_addressing_preserved; eauto.
+    intros; rewrite symbols_preserved; trivial.
+  - inv MIB. exists pc'; split; auto.
+    apply plus_one. eapply exec_Istore; eauto.
+    erewrite <- eval_addressing_preserved; eauto.
+    intros; rewrite symbols_preserved; trivial.
+  - 
+    destruct ofin; simpl; auto.
+    inv MIB.
+    admit.
+    (*eexists; split; auto.*)
+    (*apply IHIBIS2.*)
+    (*inv MIB. exists pc'; split; auto.*)
+    (*apply plus_one. eapply exec_Istore; eauto.*)
+    (*erewrite <- eval_addressing_preserved; eauto.*)
+    (*intros; rewrite symbols_preserved; trivial.*)
+  - destruct ofin; simpl; auto. inv MIB.
+    destruct b.
+    eapply IHIBIS.
 Admitted.
 
 Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option final -> option node -> Prop :=
@@ -154,10 +182,13 @@ Proof.
   *)
   (* XXX keep IBIS, MIB, and FS ? *)
   induction IBIS.
-  - (* exec_final *) 
-    try_simplify_someHyps. (* TODO: introduire un lemme pour ce cas specifique ? *)
-    admit.
+  - admit.
+  - inv IBGEN; try_simplify_someHyps.
+    inv MIB. eexists; split.
+    apply plus_one. econstructor; eauto.
+    (*
   - inversion IBGEN; subst; try_simplify_someHyps.
+    exploit iblock_istep_simulation; eauto.
     inv MIB.
     eexists. split. apply plus_one.
     eapply exec_Inop; eauto.
@@ -184,7 +215,7 @@ Proof.
   - (* exec_cond *)
     try_simplify_someHyps.
     (*inv MIB.*)
-     admit.
+       admit.*)
 Admitted.
 
 Theorem plus_simulation s1 t s1':