Trying a inductive predicate for BTL-RTL proof

1 files changed, 41 insertions, 10 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 92e05d48..7f6f21c7 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -106,14 +106,28 @@ 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
+Inductive iblock_istep_gen sp dupmap stack f rs0 m0 pc0 cfg: state -> trace -> bool -> option final -> option node -> Prop :=
+  | ibis_synced ib rs1 m1 opc pc1
+      (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 None)
+      (HOPC: opc = Some pc1)
+      (MIB : match_iblock dupmap cfg true pc0 ib opc)
+      : iblock_istep_gen sp dupmap stack f rs0 m0 pc0 cfg (State stack f sp pc0 rs0 m0) E0 true None opc
+  | ibis_stutter ib rs1 m1 fin ofin s t
+      (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
+      (HFIN: ofin = Some fin)
+      (MIB : match_iblock dupmap cfg false pc0 ib None)
+      (FS : final_step ge stack f sp rs1 m1 fin t s)
+      : iblock_istep_gen sp dupmap stack f rs0 m0 pc0 cfg s t false ofin None.
+
+Lemma iblock_step_simulation
+ sp dupmap stack stack' f f' rs0 m0 ofin pc0 opc t s isfst
  (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)
+ (*(IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin)*)
+ (*(MIB : match_iblock dupmap cfg' isfst pc0 ib opc)*)
+ (*(FS : final_step ge stack f sp rs1 m1 fin t s)*)
+(*FNC : (fn_code f) ! pc = Some ib*)
+ (IBGEN: iblock_istep_gen sp dupmap stack f rs0 m0 pc0 (RTL.fn_code f') s t isfst ofin opc)
  :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:
@@ -126,7 +140,22 @@ Proof.
 
     Au final, il faut sans doute introduire un "Inductive" pour capturer ces idées dans un prédicat "lisible"/"manipulable"...
   *)
-  induction IBIS.
+  (* XXX keep IBIS, MIB, and FS ? *)
+  induction IBGEN.
+  - inv IBIS.
+    + inv MIB.
+      eexists. split. apply plus_one.
+      eapply exec_Inop; eauto.
+      econstructor; eauto.
+      try_simplify_someHyps.
+      admit.
+    + admit.
+    + admit.
+    + admit.
+    + admit.
+    + admit.
+  - admit.
+  (* induction IBIS.
   - (* exec_final *) 
     try_simplify_someHyps. (* TODO: introduire un lemme pour ce cas specifique ? *)
     admit.
@@ -154,7 +183,7 @@ Proof.
   - (* exec_cond *)
     try_simplify_someHyps.
     inv MIB.
-    admit.
+     admit.*)
 Admitted.
 
 Theorem plus_simulation s1 t s1':
@@ -168,7 +197,8 @@ Proof.
   - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (ib' & FNC & MIB).
     try_simplify_someHyps. destruct STEP as (rs' & m' & fin & IBIS & FS).
-    intros; exploit iblock_step_simulation; eauto.
+    admit.
+    (*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.
@@ -187,7 +217,8 @@ Proof.
     eexists. split.
     + eapply plus_one. constructor.
     + inv H1. econstructor; eauto.
-Qed.
+(*Qed.*)
+Admitted.
 
 Theorem transf_program_correct:
   forward_simulation (semantics prog) (RTL.semantics tprog).