Some more proof cases, comments and cleanup

1 files changed, 96 insertions, 29 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index ac9cb8d8..1fa13242 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -91,7 +91,7 @@ The simulation diagram for match_states_intro is as follows:
 <<
 
         RTL state       match_states_intro        BTL state
-      [pcR0,rs0,m0 ---------------------------- [pcB0,rs0,m0]
+      [pcR0,rs0,m0] ---------------------------- [pcB0,rs0,m0]
            |                                         |
            |                                         |
    RTL_RUN | *E0                                     | BTL_RUN
@@ -200,28 +200,6 @@ Proof.
     rewrite GFS. eassumption. assumption.
 Qed.
 
-(* Inspired from Duplicateproof.v *)
-Lemma list_nth_z_dupmap:
-  forall dupmap ln ln' (pc pc': node) val,
-  list_nth_z ln val = Some pc ->
-  list_forall2 (fun n n' => dupmap!n = Some n') ln ln' ->
-  exists (pc': node),
-     list_nth_z ln' val = Some pc'
-  /\ dupmap!pc = Some pc'.
-Proof.
-  induction ln; intros until val; intros LNZ LFA.
-  - inv LNZ.
-  - inv LNZ. destruct (zeq val 0) eqn:ZEQ.
-    + inv H0. destruct ln'; inv LFA.
-      simpl. exists n. split; auto.
-    + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto.
-Qed.
-
-(* TODO: definir une measure sur les iblocks.
-Cette mesure décroit strictement quand on exécute un "petit-pas" de iblock.
-Par exemple, le nombre de noeuds (ou d'instructions "RTL") dans le iblock devrait convenir.
-La hauteur de l'arbre aussi.
-*)
 (** Representing an intermediate BTL state
 
 We keep a measure of code that remains to be executed with the omeasure
@@ -243,7 +221,7 @@ Definition omeasure (oib: option iblock): nat :=
  | Some ib => measure ib
  end.
 
-Lemma measure_pos: forall ib,
+Remark measure_pos: forall ib,
   measure ib > 0.
 Proof.
   induction ib; simpl; auto; lia.
@@ -268,13 +246,73 @@ Lemma opt_simu_intro
 Proof.
   inv MIB.
   - (* mib_BF *)
-    admit.
+    inv H0;
+    inversion STEP; subst; try_simplify_someHyps; intros.
+    + (* Breturn *)
+      eexists; left; eexists; split.
+      * econstructor; eauto. econstructor.
+        eexists; eexists; split.
+        eapply iblock_istep_run_equiv in BTL_RUN.
+        eapply BTL_RUN. econstructor; eauto.
+        erewrite preserv_fnstacksize; eauto.
+      * econstructor; eauto.
+    + (* Bcall *)
+      rename H10 into FIND.
+      eapply find_function_preserved in FIND.
+      destruct FIND as (fd' & FF & TRANSFUN).
+      eexists; left; eexists; split.
+      * econstructor; eauto. econstructor.
+        eexists; eexists; split.
+        eapply iblock_istep_run_equiv in BTL_RUN.
+        eapply BTL_RUN. econstructor; eauto.
+        eapply function_sig_translated; eauto.
+      * repeat (econstructor; eauto).
+        eapply transf_fundef_correct; eauto.
+    + (* Btailcall *)
+      rename H9 into FIND.
+      eapply find_function_preserved in FIND.
+      destruct FIND as (fd' & FF & TRANSFUN).
+      eexists; left; eexists; split.
+      * econstructor; eauto. econstructor.
+        eexists; eexists; split.
+        eapply iblock_istep_run_equiv in BTL_RUN.
+        eapply BTL_RUN. econstructor; eauto.
+        eapply function_sig_translated; eauto.
+        erewrite preserv_fnstacksize; eauto.
+      * repeat (econstructor; eauto).
+        eapply transf_fundef_correct; eauto.
+    + (* Bbuiltin *)
+      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
+      remember H1 as ODUPLIC; clear HeqODUPLIC.
+      apply DMC in H1 as [ib [FNC MI]]; clear DMC.
+      eexists; left; eexists; split.
+      * econstructor; eauto. econstructor.
+        eexists; eexists; split.
+        eapply iblock_istep_run_equiv in BTL_RUN.
+        eapply BTL_RUN. econstructor; eauto.
+        pose symbols_preserved as SYMPRES.
+        eapply eval_builtin_args_preserved; eauto.
+        eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
+      * econstructor; eauto. eapply code_expand; eauto.
+        apply star_refl.
+    + (* Bjumptable *)
+      admit.
+      (* eexists; left; eexists; split.
+      * econstructor; eauto. econstructor.
+        eexists; eexists; split.
+        eapply iblock_istep_run_equiv in BTL_RUN.
+        eapply BTL_RUN. econstructor; eauto.
+        exploit (list_nth_z_dupmap dupmap ln' ln); eauto.
+       * econstructor; eauto.*)
   - (* mib_exit *)
-    (*
-      simpl in *.
+    (* exists None; right; repeat (split; auto).
+      inversion STEP; subst; try_simplify_someHyps.
+      eexists; left. eexists; split.
+      econstructor; eauto. econstructor.
+      eexists; eexists; split.
       eapply iblock_istep_run_equiv in BTL_RUN.
+      eapply BTL_RUN. econstructor. econstructor; eauto.
       inv BTL_RUN.
-    eexists; left. eexists; split.
     + eapply exec_iblock; eauto.
       econstructor; repeat eexists.
       inv STEP.
@@ -282,7 +320,7 @@ Proof.
   - (* mib_seq *)
     inv H.
     + (* Bnop *)
-      inversion STEP; subst; try_simplify_someHyps. (* TODO maybe move that for each subcase *)
+      inversion STEP; subst; try_simplify_someHyps.
       exists (Some b2); right; repeat (split; auto).
       econstructor; eauto. inv IS_EXPD; auto; discriminate.
       eapply star_right; eauto.
@@ -331,6 +369,35 @@ Proof.
       all: eapply star_right; eauto.
 Admitted.
 
+(** * Main RTL to BTL simulation theorem
+
+Two possible executions:
+
+<<
+
+ **Last instruction:**
+
+    RTL state         match_states          BTL state
+       s1 ------------------------------------ s2
+       |                                       |
+  STEP |       Classical lockstep simu         | 
+       |                                       | 
+       s1' ----------------------------------- s2' 
+
+
+ **Middle instruction:**
+
+    RTL state         match_states [oib]    BTL state
+       s1 ------------------------------------ s2
+       |                               _______/
+  STEP | *E0       ___________________/         
+       |          / match_states [oib']         
+       s1' ______/
+   Where omeasure oib' < omeasure oib
+
+>>
+*)
+
 Theorem opt_simu s1 t s1' oib s2:
  RTL.step ge s1 t s1' ->
  match_states oib s1 s2 ->