From 2311cb788e6dcf0103266fd6c6aa76096c283e34 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Fri, 28 May 2021 16:33:23 +0200
Subject: remove dupmap from BTL_Scheduler !

---
 scheduling/BTL_SEtheory.v | 24 ++++++++++--------------
 1 file changed, 10 insertions(+), 14 deletions(-)

(limited to 'scheduling/BTL_SEtheory.v')

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index ea7082a9..3083ca71 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -1020,10 +1020,7 @@ Proof.
     inversion SEXEC.
 Qed.
 
-(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] 
-
-TODO: à revoir complètement. Il faut passer le dupmap en paramètre et match les états symboliques modulo le dupmap.
-*)
+(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *)
 
 Record simu_proof_context := Sctx {
    sge1: BTL.genv;
@@ -1031,7 +1028,7 @@ Record simu_proof_context := Sctx {
    sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s;
    sstk1: list BTL.stackframe;
    sstk2: list BTL.stackframe;
-   sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2;  (* REM: equiv_stackframe n'est pas suffisant, il faut le dupmap dedans ! *)
+   sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2;
    ssp: val;
    srs0: regset; 
    sm0: mem
@@ -1040,24 +1037,23 @@ Record simu_proof_context := Sctx {
 Definition bctx1 f1 (ctx: simu_proof_context):= Bctx ctx.(sge1) ctx.(sstk1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0).
 Definition bctx2 f2 (ctx: simu_proof_context):= Bctx ctx.(sge2) ctx.(sstk2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0).
 
-(* TODO: A REVOIR ! *)
 Definition sstate_simu f1 f2 (ctx: simu_proof_context) (st1 st2: sstate) :=
   forall t s1, sem_sstate (bctx1 f1 ctx) t s1 st1 ->
   exists s2, sem_sstate (bctx2 f2 ctx) t s2 st2 /\ equiv_state s1 s2.
 
-Definition symbolic_simu f1 f2 ctx ib1 ib2: sstate_simu f1 f2 ctx (sexec (f1 ctx) ib1) (sexec (f2 ctx) ib2).
+Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall ctx, sstate_simu f1 f2 ctx (sexec f1 ib1) (sexec f2 ib2).
 
-Theorem symbolic_simu_correct f1 f2 ctx ib1 ib2:
-  symbolic_simu ctx ib1 ib2 ->
-  forall t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) (sf1 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 ->
-  exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) (sf2 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2.
+Theorem symbolic_simu_correct f1 f2 ib1 ib2:
+  symbolic_simu f1 f2 ib1 ib2 ->
+  forall ctx t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 ->
+  exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2.
 Proof.
   unfold symbolic_simu, sstate_simu.
-  intros SIMU t s1 STEP1.
-  exploit (sexec_correct (bctx1 ctx)); simpl; eauto.
+  intros SIMU ctx t s1 STEP1.
+  exploit (sexec_correct (bctx1 f1 ctx)); simpl; eauto.
   intros; exploit SIMU; eauto.
   intros (s2 & SEM1 & EQ1).
-  exploit (sexec_exact (bctx2 ctx)); simpl; eauto.
+  exploit (sexec_exact (bctx2 f2 ctx)); simpl; eauto.
   intros (s3 & STEP2 & EQ2).
   clear STEP1; eexists; split; eauto.
   eapply equiv_state_trans; eauto.
-- 
cgit