starting RTL->BTL proof

1 files changed, 46 insertions, 4 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index ed661280..aac7772c 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -80,13 +80,26 @@ Let tge := Genv.globalenv tprog.
 
 Local Open Scope nat_scope.
 
-(* TODO:
+(** * Match relation from a RTL state to a BTL state
 
-Le (option iblock) en paramètre représente l'état de l'exécution côté BTL 
-depuis le début de l'exécution du block
+The "option iblock" parameter represents the current BTL execution state.
+Thus, each RTL single step is symbolized by a new BTL "option iblock"
+starting at the equivalent PC.
 
-  faire un dessin ASCII art de la simulation avec match_states_intro 
+The simulation diagram for match_states_intro is as follows:
 
+<<
+
+        RTL state       match_states_intro        BTL state
+      [pc0,rs0,m0] ---------------------------- [pc0',rs0,m0]
+           |                                         |
+           |                                         |
+   RTL_RUN | *E0                                     | BTL_RUN
+           |                                         |
+           |                   MIB                   |
+       [pc,rs,m] ---------------------------------- [ib]
+
+>>
 *)
 
 Inductive match_states: (option iblock) -> RTL.state -> state -> Prop :=
@@ -209,6 +222,14 @@ Cette mesure décroit strictement quand on exécute un "petit-pas" de iblock.
 Par exemple, le nombre de noeuds (ou d'instructions "RTL") dans le iblock devrait convenir.
 La hauteur de l'arbre aussi.
 *)
+(** Representing an intermediate BTL state
+
+We keep a measure of code that remains to be executed with the omeasure
+type defined below. Intuitively, each RTL step corresponds to either
+   - a single BTL step if we are on the last instruction of the block
+   - 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.
 
 Definition omeasure (oib: option iblock): nat :=
@@ -224,6 +245,27 @@ Theorem opt_simu s1 t s1' oib s2:
      (exists s2', step tge s2 t s2' /\ match_states oib' s1' s2')
   \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) 
  .
+Proof.
+  induction 2.
+  - admit.
+  - (* Callstate *)
+    inv H.
+    + (* Internal function *)
+      inv TRANSF.
+      rename H0 into MF.
+      eapply dupmap_entrypoint in MF as ENTRY.
+      eapply dupmap_correct in MF as DMC. unfold match_cfg in DMC.
+      apply DMC in ENTRY as DMC'. destruct DMC' as [ib [CENTRY MI]].
+      eexists; left; eexists; split.
+      * eapply exec_function_internal.
+        erewrite preserv_fnstacksize; eauto.
+      * econstructor; eauto.
+        eapply code_right_assoc; eauto.
+        all: erewrite preserv_fnparams; eauto.
+        constructor.
+    + (* External function *)
+      admit.
+  - admit.
 Admitted.
 
 Local Hint Resolve plus_one star_refl: core.