essai avec le cond_star_step

1 files changed, 45 insertions, 12 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index ef640d22..31652697 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -106,11 +106,30 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
+(* FIXME: unused ?
 Definition is_goto (i: final): option exit :=
   match i with
   | Bgoto pc => Some pc
   | _ => None
   end.
+*)
+
+(* variant of [star RTL.step] but requiring proposition [P] on the [refl] (stutttering) case. *)
+Inductive cond_star_step (P: Prop): RTL.state -> trace -> RTL.state -> Prop :=
+  | css_refl s: P -> cond_star_step P s E0 s
+  | css_plus s1 t s2: plus RTL.step tge s1 t s2 -> cond_star_step P s1 t s2
+  .
+
+Lemma css_plus_trans P Q s0 s1 s2 t:
+  plus RTL.step tge s0 E0 s1 ->
+  cond_star_step P s1 t s2 ->
+  cond_star_step Q s0 t s2.
+Proof.
+  intros PLUS STAR.
+  eapply css_plus.
+  inv STAR; auto.
+  eapply plus_trans; eauto.
+Qed.
 
 (* suggestion *)
 Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
@@ -122,12 +141,15 @@ Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
   | 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 =>
      (* A CHANGER ? *)
-     exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin opc
-                /\ star RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
+     exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin None
+                /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
   end.
 Proof.
   induction IBIS; simpl; intros.
-  - repeat econstructor; eauto.
+  - assert (X: opc = None). { inv MIB; auto. }
+    subst.
+    repeat eexists; eauto.
+    eapply css_refl; auto.
   - inv MIB. exists pc'; split; auto.
     apply plus_one. apply exec_Inop; trivial.
   - inv MIB. exists pc'; split; auto.
@@ -144,8 +166,6 @@ Proof.
     intros; rewrite symbols_preserved; trivial.
   - inv MIB.
     exploit IHIBIS; eauto.
-    intros (isfst' & pc1 & M1 & STAR).
-    inv M1.
   - inv MIB.
     exploit IHIBIS1; eauto.
     intros (pc1 & EQpc1 & STEP1); inv EQpc1.
@@ -153,9 +173,7 @@ Proof.
     destruct ofin; simpl.
     + intros (ifst2 & pc2 & M2 & STEP2).
       repeat eexists; eauto.
-      eapply star_trans; eauto.
-      eapply plus_star; eauto.
-      eauto.
+      eapply css_plus_trans; eauto.
     + intros (pc2 & EQpc2 & STEP2); inv EQpc2.
       eexists; split; auto.
       eapply plus_trans; eauto.
@@ -163,6 +181,20 @@ Proof.
     destruct b; exploit IHIBIS; eauto.
 Admitted.
 
+Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s
+ (STACKS: list_forall2 match_stackframes stack stack')
+ (TRANSF: match_function dupmap f f')
+ (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
+ (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None)
+ (FS : final_step ge stack f sp rs1 m1 fin t s)
+ :exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
+Proof.
+  intros; exploit iblock_istep_simulation; eauto.
+  simpl.
+Admitted.
+
+(* BROUILLON
+
 Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option final -> option node -> Prop :=
   | ibis_synced opc pc1
       (HOPC: opc = Some pc1)
@@ -233,6 +265,8 @@ Proof.
        admit.*)
 Admitted.
 
+*)
+
 Theorem plus_simulation s1 t s1':
   step ge s1 t s1' ->
   forall s2 (MS: match_states s1 s2),
@@ -244,8 +278,7 @@ Proof.
   - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (ib' & FNC & MIB).
     try_simplify_someHyps. destruct STEP as (rs' & m' & fin & IBIS & FS).
-    admit.
-    (*intros; exploit iblock_step_simulation; eauto.*)
+    intros; exploit iblock_step_simulation; eauto.
   (* exec_function_internal *)
   - inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split.
     + eapply plus_one. apply RTL.exec_function_internal.
@@ -264,8 +297,8 @@ Proof.
     eexists. split.
     + eapply plus_one. constructor.
     + inv H1. econstructor; eauto.
-(*Qed.*)
-Admitted.
+Qed.
+(* Admitted. *)
 
 Theorem transf_program_correct:
   forward_simulation (semantics prog) (RTL.semantics tprog).