From 72da07fabaea1139ce1a5bd26e907c7aea68c73f Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Fri, 7 May 2021 12:12:20 +0200
Subject: a draft for the Bnop case

---
 scheduling/RTLtoBTLproof.v | 36 +++++++++++++++++++++++++-----------
 1 file changed, 25 insertions(+), 11 deletions(-)

(limited to 'scheduling/RTLtoBTLproof.v')

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 79b7ca1a..7d58de5a 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -91,29 +91,29 @@ The simulation diagram for match_states_intro is as follows:
 <<
 
         RTL state       match_states_intro        BTL state
-      [pc0,rs0,m0] ---------------------------- [pc0',rs0,m0]
+      [pcR0,rs0,m0 ---------------------------- [pcB0,rs0,m0]
            |                                         |
            |                                         |
    RTL_RUN | *E0                                     | BTL_RUN
            |                                         |
            |                   MIB                   |
-       [pc,rs,m] ---------------------------------- [ib]
+      [pcR1,rs,m] -------------------------------- [ib]
 
 >>
 *)
 
 Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
   | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *)
-      ib dupmap st f sp pc rs m st' f' pc0' pc0 rs0 m0 isfst ib0
+      ib dupmap st f sp rs m st' f' pcB0 pcR0 pcR1 rs0 m0 isfst ib0
       (STACKS: list_forall2 match_stackframes st st')
       (TRANSF: match_function dupmap f f')
-      (ATpc0: (fn_code f')!pc0' = Some ib0)
-      (DUPLIC: dupmap!pc0' = Some pc0)
-      (MIB: match_iblock dupmap (RTL.fn_code f) isfst pc ib None)
+      (ATpc0: (fn_code f')!pcB0 = Some ib0)
+      (DUPLIC: dupmap!pcB0 = Some pcR0)
+      (MIB: match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None)
       (RIGHTA: is_right_assoc ib)
-      (RTL_RUN: star RTL.step ge (RTL.State st f sp pc0 rs0 m0) E0 (RTL.State st f sp pc rs m))
+      (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs m))
       (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m)
-      : match_states (Some ib) (RTL.State st f sp pc rs m) (State st' f' sp pc0' rs0 m0)
+      : match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)
   | match_states_call
       st st' f f' args m
       (STACKS: list_forall2 match_stackframes st st')
@@ -230,7 +230,12 @@ type defined below. Intuitively, each RTL step corresponds to either
    - no BTL step (as we use a "big step" semantics) but a change in
      the measure which represents the new intermediate state of the BTL code
  *)
-Parameter measure: iblock -> nat.
+Fixpoint measure ib: nat :=
+  match ib with
+  | Bseq ib1 ib2
+  | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2
+  | ib => 1
+  end.
 
 Definition omeasure (oib: option iblock): nat :=
  match oib with
@@ -246,8 +251,17 @@ Theorem opt_simu s1 t s1' oib s2:
   \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) 
  .
 Proof.
-  induction 2.
-  - admit.
+  inversion 2; subst; clear H0.
+  - (* State *)
+    inv H.
+
+    1: { (* Inop *)
+      eexists; right; split.
+      2: split; trivial.
+      2: {
+        econstructor; eauto.
+        all: admit. } admit. }
+    all: admit. 
   - (* Callstate *)
     inv H.
     + (* Internal function *)
-- 
cgit