From 58312db34d43803a2cb63e20667a5059988dc0d1 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Fri, 18 Jun 2021 15:16:21 +0200
Subject: lemma on eqregs?

---
 scheduling/BTL_Scheduler.v      |  2 +-
 scheduling/BTL_Schedulerproof.v | 19 ++++++-------------
 2 files changed, 7 insertions(+), 14 deletions(-)

(limited to 'scheduling')

diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index c50eb364..12840f62 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -41,7 +41,7 @@ Record match_function (f1 f2: BTL.function): Prop := {
   preserv_fnparams: fn_params f1 = fn_params f2;
   preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2;
   preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2;
-  preserv_inputs: equiv_input_regs f1 f2; (* TODO: a-t-on besoin de ça ? *)
+  preserv_inputs: equiv_input_regs f1 f2;
   symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 ->
                     exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2);
 }.
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 6963ee8b..1a4c5757 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -80,7 +80,6 @@ Lemma match_stack_equiv stk1 stk2:
   forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
   list_forall2 match_stackframes stk1 stk3.
 Proof.
-  (*Local Hint Resolve match_stackframes_equiv: core.*)
   induction 1; intros stk3 EQ; inv EQ; constructor; eauto.
   inv H3; inv H; econstructor; eauto.
   intros; rewrite <- EQUIV; auto.
@@ -297,17 +296,13 @@ Qed.
 
 End SYMBOLIC_CTX.
 
-Lemma iblock_step_eqregs sp ib:
-  forall rs rs'
+Lemma iblock_step_eqregs stk sp f ib:
+  forall rs rs' m s t
   (EQREGS: forall r, rs # r = rs' # r)
-  fin m rs2 m2 (ISTEP: iblock_istep tpge sp rs m ib rs2 m2 (Some fin)),
-  iblock_istep tpge sp rs' m ib rs2 m2 (Some fin).
+  (STEP: iblock_step tr_inputs tpge stk f sp rs m ib s t),
+  iblock_step tr_inputs tpge stk f sp rs' m ib s t.
 Proof.
-  induction ib; intros; inv ISTEP.
-  - 
-    admit.
-  - econstructor; eauto.
-  - econstructor. eapply IHib1; eauto.
+
 Admitted.
 
 Lemma iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m ibf t s pc
@@ -325,9 +320,7 @@ Proof.
   exploit symbolic_simu_correct; repeat (eauto; simpl).
   intros (s' & STEP2 & MS).
   exists ib2; exists s'. repeat split; auto.
-  destruct STEP2 as (rs2 & m2 & fin & ISTEP2 & FSTEP2).
-  unfold iblock_step. exists rs2; exists m2; exists fin.
-  split; auto.
+  eapply iblock_step_eqregs; eauto.
 Admitted.
 
 Local Hint Constructors step: core.
-- 
cgit