From 6c0efaa166b1acbabcdcd051c5ec389b9b562fe6 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Thu, 10 Jun 2021 08:15:06 +0200
Subject: remove history

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

(limited to 'scheduling/BTL_SEtheory.v')

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 9074b071..5a94b235 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -25,6 +25,8 @@ Record iblock_exec_context := Bctx {
 
 (** * Syntax and semantics of symbolic values *)
 
+(* TODO: introduire les hash-code directement ici - avec les "fake" smart constructors qui mettent un unknown_hid ? *)
+
 (* symbolic value *)
 Inductive sval :=
   | Sundef
@@ -717,12 +719,12 @@ Record soutcome := sout {
    _sfv: sfval;
 }.
 
-Fixpoint run_sem_isstate ctx (st:sstate): option soutcome :=
+Fixpoint get_soutcome ctx (st:sstate): option soutcome :=
   match st with
   | Sfinal sis sfv => Some (sout sis sfv)
   | Scond cond args ifso ifnot =>
      SOME b <- seval_condition ctx cond args IN
-     run_sem_isstate ctx (if b then ifso else ifnot)
+     get_soutcome ctx (if b then ifso else ifnot)
   | Sabort => None
   end.
 
@@ -742,7 +744,7 @@ Inductive sem_sstate ctx stk t s: sstate -> Prop :=
 Lemma sem_sstate_run ctx stk st t s:
   sem_sstate ctx stk t s st -> 
   exists sis sfv rs m, 
-      run_sem_isstate ctx st = Some (sout sis sfv)
+      get_soutcome ctx st = Some (sout sis sfv)
    /\ sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m
    /\ sem_sfval ctx stk sfv rs m t s
    .
@@ -753,7 +755,7 @@ Qed.
 Local Hint Resolve sem_Sfinal: core.
 
 Lemma run_sem_sstate ctx st sis sfv:
-  run_sem_isstate ctx st = Some (sout sis sfv) ->
+  get_soutcome ctx st = Some (sout sis sfv) ->
   forall rs m stk s t, 
   sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m ->
   sem_sfval ctx stk sfv rs m t s ->
@@ -1154,8 +1156,8 @@ Qed.
 
 
 Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): Prop :=
-  forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> si_ok (bctx1 ctx) sis1 ->
-  exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) 
+  forall sis1 sfv1, get_soutcome (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> si_ok (bctx1 ctx) sis1 ->
+  exists sis2 sfv2, get_soutcome (bctx2 ctx) st2 = Some (sout sis2 sfv2) 
                    /\ sistate_simu ctx sis1 sis2
                    /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sfv_simu ctx sfv1 sfv2)
   .
@@ -1261,8 +1263,8 @@ Proof.
 Qed.
 
 (* TODO: useless ?
-Lemma run_sem_isstate_preserved sis:
-  run_sem_isstate (bctx1 ctx) sis = run_sem_isstate (bctx2 ctx) sis.
+Lemma get_soutcome_preserved sis:
+  get_soutcome (bctx1 ctx) sis = get_soutcome (bctx2 ctx) sis.
 Proof.
   induction sis; simpl; eauto.
   erewrite seval_condition_preserved.
-- 
cgit