Some more proof cases, comments and cleanup

2 files changed, 97 insertions, 97 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index d7ffa118..a87f674b 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -793,6 +793,7 @@ Definition is_atom (ib: iblock): bool :=
  | _ => true
  end.
 
+(** Is expand property to only support atomic instructions on the left part of a Bseq *)
 Inductive is_expand: iblock -> Prop :=
   | exp_Bseq ib1 ib2:
      is_atom ib1 = true ->
@@ -844,71 +845,3 @@ Proof.
   destruct (cfg!pc); simpl; intros; try_simplify_someHyps.
   apply expand_None_correct; auto.
 Qed.
-
-
-(* TODO: eliminer toute la suite quand "right_assoc" sera remplace par "expand" *)
-
-Definition is_seq (ib: iblock): bool :=
- match ib with
- | Bseq _ _ => true 
- | _ => false
- end.
-
-
-Inductive is_right_assoc: iblock -> Prop :=
-  | ira_Bseq ib1 ib2:
-     is_seq ib1 = false ->
-     is_right_assoc ib1 ->
-     is_right_assoc ib2 -> 
-     is_right_assoc (Bseq ib1 ib2)
- | ira_Bcond cond args ib1 ib2 i:
-     is_right_assoc ib1 ->
-     is_right_assoc ib2 -> 
-     is_right_assoc (Bcond cond args ib1 ib2 i)
- | ira_others ib:
-     is_atom ib = true ->
-     is_right_assoc ib
-     .
-Local Hint Constructors is_right_assoc: core.
-
-Fixpoint right_assoc (ib: iblock): iblock :=
-  match ib with
-  | Bseq ib1 ib2 => rec_rotate ib1 (right_assoc ib2)
-  | Bcond cond args ib1 ib2 i => 
-     Bcond cond args (right_assoc ib1) (right_assoc ib2) i
-  | ib => ib
-  end
-with rec_rotate (ib: iblock) rem: iblock :=
-  match ib with
-  | Bseq ib1 ib2 => 
-     rec_rotate ib1 (rec_rotate ib2 rem)
-  | Bcond cond args ib1 ib2 i => 
-     Bseq (Bcond cond args (right_assoc ib1) (right_assoc ib2) i) rem
-  | ib => Bseq ib rem
-end.
-
-Lemma right_assoc_rec_rotate_correct ib:
-    is_right_assoc (right_assoc ib)
- /\ (forall rem, is_right_assoc rem -> is_right_assoc (rec_rotate ib rem)).
-Proof.
-  induction ib; simpl; intuition.
-Qed.
-
-Lemma right_assoc_correct ib:
-  is_right_assoc (right_assoc ib).
-Proof.
-  destruct (right_assoc_rec_rotate_correct ib); auto.
-Qed.
-
-Definition right_assoc_code (cfg: code): code :=
-  (PTree.map (fun _ ib => {| entry:=right_assoc ib.(entry); input_regs := ib.(input_regs) |}) cfg).
-
-Lemma right_assoc_code_correct cfg pc ib :
-  (right_assoc_code cfg)!pc=Some ib -> is_right_assoc (ib.(entry)).
-Proof.
-  unfold right_assoc_code.
-  rewrite PTree.gmap.
-  destruct (cfg!pc); simpl; intros; try_simplify_someHyps.
-  apply right_assoc_correct; auto.
-Qed.
-
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 ->