From c8b2438685f1a6c4a98cf58727d32a9e474c4f34 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 3 May 2021 13:53:43 +0200
Subject: A better structure for inductive prop

---
 scheduling/BTLtoRTLproof.v | 60 +++++++++++++++++++---------------------------
 1 file changed, 25 insertions(+), 35 deletions(-)

(limited to 'scheduling/BTLtoRTLproof.v')

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 7f6f21c7..904b3814 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -106,28 +106,29 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
-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)
+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)
       (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))
+      : iblock_istep_gen sp dupmap stack f pc0 cfg ib E0 true None opc
+  | ibis_stutter rs1 m1 fin ofin s t
       (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.
+      : iblock_istep_gen sp dupmap stack f pc0 cfg ib t false ofin None.
+
+(*Lemma iblock_istep_gen_correct *)
+(*TODO *)
 
 Lemma iblock_step_simulation
- sp dupmap stack stack' f f' rs0 m0 ofin pc0 opc t s isfst
+ sp dupmap stack stack' f f' rs0 m0 rs1 m1 ib 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)*)
+ (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)
+ (IBGEN: iblock_istep_gen sp dupmap stack f pc0 (RTL.fn_code f') ib 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:
@@ -141,35 +142,24 @@ Proof.
     Au final, il faut sans doute introduire un "Inductive" pour capturer ces idées dans un prédicat "lisible"/"manipulable"...
   *)
   (* 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.
+  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 *)
+  - inversion IBGEN; subst; try_simplify_someHyps.
+    inv MIB.
+    eexists. split. apply plus_one.
+    eapply exec_Inop; eauto.
+    try_simplify_someHyps.
+      admit.
   - (* exec_op *)
-    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
+    admit. (* cas absurde car hypothese OFIN trop restrictive *)
   - (* exec_load_TRAP *)
-    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
+    admit. (* cas absurde car hypothese OFIN trop restrictive *)
   - (* exec_load_store *)
-    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
+    admit. (* cas absurde car hypothese OFIN trop restrictive *)
   - (* exec_seq_stop *)
-    try_simplify_someHyps.
-    inv MIB.
+    (*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.
@@ -178,12 +168,12 @@ Proof.
   - (* 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.
+    (*inv MIB.*)
     admit.
   - (* exec_cond *)
     try_simplify_someHyps.
-    inv MIB.
-     admit.*)
+    (*inv MIB.*)
+     admit.
 Admitted.
 
 Theorem plus_simulation s1 t s1':
-- 
cgit