From d422c63cbcad7ba156d5d324e0221db9d13f9559 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Sat, 8 May 2021 07:56:20 +0200
Subject: sexec: renommage Sdead -> Sabort + simplification de sexec_correct

---
 scheduling/BTL_SEtheory.v | 78 +++++++++++++----------------------------------
 1 file changed, 21 insertions(+), 57 deletions(-)

(limited to 'scheduling/BTL_SEtheory.v')

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 8aa8f32b..0a2c0a04 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -732,7 +732,7 @@ Qed.
 Inductive sstate :=
   | Sfinal (sis: sistate) (sfv: sfval)
   | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate)
-  | Sdead
+  | Sabort
  .
 
 (* transition (t,s) produced by a sstate in initial context ctx *)
@@ -745,7 +745,7 @@ Inductive sem_sstate ctx t s: sstate -> Prop :=
      (SEVAL: seval_condition ctx cond args sm = Some b)
      (SELECT: sem_sstate ctx t s (if b then ifso else ifnot))
      : sem_sstate ctx t s (Scond cond args sm ifso ifnot)
-  (* NB: Sdead: fails to produce a transition *) 
+  (* NB: Sabort: fails to produce a transition *) 
   .
 
 (** * Idée de l'execution symbolique en Continuation Passing Style 
@@ -766,7 +766,7 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate :=
   | Bnop => k sis
   | Bop op args res => k (sexec_op op args res sis)
   | Bload TRAP chunk addr args dst => k (sexec_load TRAP chunk addr args dst sis)
-  | Bload NOTRAP chunk addr args dst => Sdead (* TODO *)
+  | Bload NOTRAP chunk addr args dst => Sabort (* TODO *)
   | Bstore chunk addr args src => k (sexec_store chunk addr args src sis)
  (* composed instructions *)
   | Bseq ib1 ib2 =>
@@ -779,63 +779,28 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate :=
   end
   .
 
-Definition sexec ib := sexec_rec ib sis_init (fun _ => Sdead).
+Definition sexec ib := sexec_rec ib sis_init (fun _ => Sabort).
 
 Local Hint Constructors sem_sstate: core.
-Local Hint Resolve sexec_final_svf_correct sis_init_correct: core.
+Local Hint Resolve sexec_op_correct sexec_final_svf_correct 
+                   sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core.
 
 Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
-  (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): 
-  forall k 
-  (CONT: forall sis, ofin = None -> sem_sistate ctx sis rs1 m1 -> sem_sstate ctx t s (k sis))
-  sis 
+  (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): forall sis k
   (SIS: sem_sistate ctx sis rs m)
-  , match ofin with
-    | Some fin =>
-        final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s -> 
-        sem_sstate ctx t s (sexec_rec ib sis k)
-    | None => sem_sstate ctx t s (sexec_rec ib sis k)
-    end.
-Proof.
-  induction ISTEP; simpl; eauto.
-  - (* op *)
-    intros; eapply CONT; eauto.
-    eapply sexec_op_correct; eauto.
-  - (* load *)
-    intros; eapply CONT; eauto.
-    eapply sexec_load_TRAP_correct; eauto.
-  - (* store *)
-    intros; eapply CONT; eauto.
-    eapply sexec_store_correct; eauto.
-  - (* seq_stop *)
-    intros; eapply IHISTEP; eauto.
-    try congruence.
-  - (* seq_continue *)
-    intros. destruct ofin as [fin|].
-    + (* Some *)
-      clear CONT.
-      intros; eapply IHISTEP1; eauto.
-      intros; eapply IHISTEP2; eauto.
-      try congruence.
-    + (* None *)
-      intros; eapply IHISTEP1; eauto.
-  - (* cond *)
-    intros.
-    assert (IFEQ: (if b then sexec_rec ifso sis k else sexec_rec ifnot sis k) = sexec_rec (if b then ifso else ifnot) sis k).
-    { destruct b; simpl; auto. }
-    destruct ofin as [fin|].
-    + (* Some *)
-      clear CONT.
-      intro FSTEP; eapply sem_Scond; eauto.
-      * erewrite seval_condition_eq; eauto.
-      * rewrite IFEQ. 
-        eapply IHISTEP; eauto.
-        try congruence.
-    + (* None *)
-      eapply sem_Scond; eauto.
-      * erewrite seval_condition_eq; eauto.
-      * rewrite IFEQ. 
-        eapply IHISTEP; eauto.
+  (CONT: match ofin with
+         | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx t s (k sis')
+         | Some fin => final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
+         end),
+  sem_sstate ctx t s (sexec_rec ib sis k).
+Proof.
+  induction ISTEP; simpl; try autodestruct; eauto.
+  (* condition *)
+  all: intros;
+    eapply sem_Scond; eauto; [
+      erewrite seval_condition_eq; eauto |
+      replace (if b then sexec_rec ifso sis k else sexec_rec ifnot sis k) with (sexec_rec (if b then ifso else ifnot) sis k); 
+      try autodestruct; eauto ].
 Qed.
 
 (* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) 
@@ -846,6 +811,5 @@ Theorem sexec_correct ctx ib t s:
   sem_sstate ctx t s (sexec ib).
 Proof.
   destruct 1 as (rs' & m' & fin & ISTEP & FSTEP).
-  unfold sexec.
-  exploit sexec_rec_correct; simpl; eauto || congruence.
+  eapply sexec_rec_correct; simpl; eauto.
 Qed.
-- 
cgit