Some advance in proof and NOTRAP loads fix

1 files changed, 53 insertions, 4 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index f5ea9fdc..023837f9 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -256,9 +256,59 @@ Lemma opt_simu_intro
               (RTL.State st f sp pcR1 rs m))
   (BTL_RUN : iblock_istep_run tge sp (entry ib0) rs0 m0 =
             iblock_istep_run tge sp ib rs m)
-  : exists (oib : option iblock),
-      omeasure oib < omeasure (Some ib) /\
-      t = E0 /\ match_states oib s1' (State st' f' sp pcB0 rs0 m0).
+  : exists (oib' : option iblock),
+     (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2')
+  \/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)).
+Proof.
+  inv MIB.
+  - (* mib_BF *)
+    admit.
+  - (* mib_exit *)
+    (* destruct t.
+    2: { 
+    eexists; left. eexists; split.
+    + eapply exec_iblock; eauto.
+      econstructor; repeat eexists.
+      eapply iblock_istep_run_equiv; eauto.
+      inv STEP.
+       eapply exec_Bgoto.*) admit.
+  - (* mib_seq *)
+    inv H.
+    + (* Bnop *)
+      inversion STEP; subst; try_simplify_someHyps. (* TODO maybe move that for each subcase *)
+      exists (Some b2); right; repeat (split; auto).
+      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      eapply star_right; eauto.
+    + (* Bop *)
+      inversion STEP; subst; try_simplify_someHyps.
+      exists (Some b2); right; repeat (split; auto).
+      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      eapply star_right; eauto.
+      erewrite eval_operation_preserved in H10.
+      erewrite H10 in BTL_RUN; simpl in BTL_RUN; auto.
+      intros; rewrite <- symbols_preserved; trivial.
+    + (* Bload *)
+      inversion STEP; subst; try_simplify_someHyps.
+      exists (Some (b2)); right; repeat (split; auto).
+      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      eapply star_right; eauto.
+      erewrite eval_addressing_preserved in H10.
+      erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
+      intros; rewrite <- symbols_preserved; trivial.
+    + (* Bstore *)
+      inversion STEP; subst; try_simplify_someHyps.
+      exists (Some b2); right; repeat (split; auto).
+      econstructor; eauto. inv RIGHTA; auto; discriminate.
+      eapply star_right; eauto.
+      erewrite eval_addressing_preserved in H10.
+      erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto.
+      intros; rewrite <- symbols_preserved; trivial.
+    + (* Absurd case *)
+      inv RIGHTA. inv H4. inv H.
+    + (* Bcond *)
+      admit.
+  - (* mib_cond *)
+    admit.
 Admitted.
 
 Theorem opt_simu s1 t s1' oib s2:
@@ -272,7 +322,6 @@ Proof.
   inversion 2; subst; clear H0.
   - (* State *)
     exploit opt_simu_intro; eauto.
-    intros (oib' & SIMU); exists oib'; right; assumption.
   - (* Callstate *)
     inv H.
     + (* Internal function *)