debroussaillage et precisions...

1 files changed, 58 insertions, 8 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index a3be20b5..92e05d48 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -106,6 +106,57 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
+Lemma iblock_step_simulation sp dupmap stack stack' f f' cfg' ib rs0 m0 rs1 m1 ofin
+ (STACKS: list_forall2 match_stackframes stack stack')
+ (TRANSF: match_function dupmap f f')
+ (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin)
+ fin pc0 t s isfst
+ (OFIN: ofin = Some fin)
+ (MIB : match_iblock dupmap cfg' isfst pc0 ib None)
+ (FS : final_step ge stack f sp rs1 m1 fin t s)
+ :exists s', (if isfst then plus RTL.step else star RTL.step) tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
+Proof.
+  (* TODO: généraliser ce lemme pour pouvoir le prouver par induction sur IBIS:
+       => il faut en particulier généraliser l'hypothèse MIB qui relie le iblock_istep ib en cours d'exécution.
+          avec le code RTL à partir de pc0. 
+       => ici, le "isfst" a déjà été généralisé: quand il vaut "false", ça veut dire qu'on a le droit de faire du "stuttering" côté RTL.
+       => il reste à comprendre comment généraliser le "None" en "opc"
+          ainsi que l'hypothese OFIN pour autoriser le cas "ofin=None" (nécessaire pour l'induction).
+          Idée: si "ofin = None" alors il y a un pc1 tq "opc = Some pc1" qui permet d'exécuter la suite du bloc...
+
+    Au final, il faut sans doute introduire un "Inductive" pour capturer ces idées dans un prédicat "lisible"/"manipulable"...
+  *)
+  induction IBIS.
+  - (* exec_final *) 
+    try_simplify_someHyps. (* TODO: introduire un lemme pour ce cas specifique ? *)
+    admit.
+  - (* exec_nop *)
+    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
+  - (* exec_op *)
+    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
+  - (* exec_load_TRAP *)
+    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
+  - (* exec_load_store *)
+    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
+  - (* exec_seq_stop *)
+    try_simplify_someHyps.
+    inv MIB.
+    eapply IHIBIS; eauto.
+    (* TODO: c'est ici qu'on voit que l'hypothèse MIB est trop restrictive actuellement 
+       normalement, l'hypothèse d'induction IHIBIS devrait permettre de conclure quasi-directement ici.
+    *)
+    admit.
+  - (* exec_seq_continue *)
+    (* TODO: ici l'hypothèse d'induction IHIBIS1 n'est pas utilisable à cause de OFIN trop restrictive *)
+    try_simplify_someHyps.
+    inv MIB.
+    admit.
+  - (* exec_cond *)
+    try_simplify_someHyps.
+    inv MIB.
+    admit.
+Admitted.
+
 Theorem plus_simulation s1 t s1':
   step ge s1 t s1' ->
   forall s2 (MS: match_states s1 s2),
@@ -113,14 +164,11 @@ Theorem plus_simulation s1 t s1':
      plus RTL.step tge s2 t s2'
   /\ match_states s1' s2'.
 Proof.
-  induction 1; intros; inv MS.
+  destruct 1; intros; inv MS.
   - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (ib' & FNC & MIB).
-    inv H0. destruct H1 as (m' & fin & IBIS & FS).
-    admit.
-    (* Définir une relation inductive qui provient du MS,
-       et qui relie le iblock_istep avec le RTL. Il faut prendre en compte
-       le "isfst" pour savoir si on doit avoir du "stuttering" côté RTL. *)
+    try_simplify_someHyps. destruct STEP as (rs' & m' & fin & IBIS & FS).
+    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.
@@ -134,10 +182,12 @@ Proof.
       eapply external_call_symbols_preserved; eauto. apply senv_preserved.
     + constructor. assumption.
   (* exec_return *)
-  - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split.
+  - inversion STACKS as [|a1 al b1 bl H1 HL]; subst.
+    destruct b1 as [res' f' sp' pc' rs'].
+    eexists. split.
     + eapply plus_one. constructor.
     + inv H1. econstructor; eauto.
-Admitted. (* TODO: première étape *)
+Qed.
 
 Theorem transf_program_correct:
   forward_simulation (semantics prog) (RTL.semantics tprog).