progress in BTL_SEsimuref

1 files changed, 11 insertions, 23 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 557541ce..9ab64d7d 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -1064,32 +1064,10 @@ Qed.
 
 (** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *)
 
-(*
-Definition equiv_input_regs (f1 f2: BTL.function): Prop :=
-    (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) 
- /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)).
-
-Lemma equiv_input_regs_union f1 f2:
- equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl.
-Proof.
- intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto.
- generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS.
- do 2 autodestruct; intuition; try_simplify_someHyps. 
- intros; exploit EQS; eauto; clear EQS. congruence.
-Qed.
-
-Lemma equiv_input_regs_pre f1 f2 tbl or:
- equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or.
-Proof.
-   intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto.
-Qed.
-*)
-
 Record simu_proof_context {f1 f2: BTL.function} := Sctx {
    sge1: BTL.genv;
    sge2: BTL.genv;
    sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s;
-   (* inputs_equiv: equiv_input_regs f1 f2;*) (* TODO a-t-on besoin de ça ? *)
    ssp: val;
    srs0: regset; 
    sm0: mem
@@ -1156,7 +1134,7 @@ Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate):
   forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) ->
   exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) 
                    /\ sistate_simu ctx sis1 sis2
-                   /\ sfv_simu ctx sfv1 sfv2
+                   /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sfv_simu ctx sfv1 sfv2)
   .
 
 Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2).
@@ -1261,6 +1239,16 @@ Proof.
   rewrite smem_eval_preserved; auto.
 Qed.
 
+(* TODO: useless ?
+Lemma run_sem_isstate_preserved sis:
+  run_sem_isstate (bctx1 ctx) sis = run_sem_isstate (bctx2 ctx) sis.
+Proof.
+  induction sis; simpl; eauto.
+  erewrite seval_condition_preserved.
+  repeat (autodestruct; auto).
+Qed.
+*)
+
 (* additional preservation properties under this additional hypothesis *)
 Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx).