From 0cda2f3441252eadc1d7901942935bf0c2a2949c Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 7 Jul 2021 12:06:09 +0200
Subject: symbolic_simu impl definitions

---
 scheduling/BTL_SEimpl.v | 56 ++++++++-----------------------------------------
 1 file changed, 9 insertions(+), 47 deletions(-)

(limited to 'scheduling')

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index c32001d4..a2b5cc43 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -1158,66 +1158,28 @@ Proof. (* TODO *)
     1-3: wlp_simplify. unfold hrexec.
     simpl. eauto.
     intuition eauto.
-  + intros; eapply rexec_correct2; eauto.
-  intros ctxz.
+    admit.
 Admitted.
 Global Opaque simu_check_single.
 Global Hint Resolve simu_check_single_correct: wlp.
 
-Fixpoint simu_check_rec (f1 f2: function) (blks: list node): ?? unit :=
-  match blks with
-  | nil => RET tt
-  | pc :: blk' =>
-      DO ibf1 <~ some_or_fail (fn_code f1)!pc "simu_check_rec: incorrect PTree for f1";;
-      DO ibf2 <~ some_or_fail (fn_code f2)!pc "simu_check_rec: incorrect PTree for f2";;
-      DO res <~ simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);;
-      simu_check_rec f1 f2 blk'
-  end.
-
-Lemma simu_check_rec_correct f1 f2:
-  WHEN simu_check_rec f1 f2 (PTree.elements (fn_code f1)) ~> _ THEN
-  symbolic_simu f1 f2 .
-Proof.
-  induction lm; wlp_simplify.
-  match goal with
-  | X: (_,_) = (_,_) |- _ => inversion X; subst
-  end.
-  subst; eauto.
-Qed.
-Global Opaque simu_check_rec.
-Global Hint Resolve simu_check_rec_correct: wlp.
-
-Definition imp_simu_check (f tf: function): ?? unit :=
-   simu_check_rec f tf ;;
-   DEBUG("simu_check OK!").
-
-Local Hint Resolve PTree.elements_correct: core.
-Lemma imp_simu_check_correct f tf:
-  WHEN imp_simu_check f tf ~> _ THEN
-  forall sexec_simu f tf.
-Proof.
-  wlp_simplify.
-Qed.
-Global Opaque imp_simu_check.
-Global Hint Resolve imp_simu_check_correct: wlp.
-
-Program Definition aux_simu_check (f tf: function): ?? bool :=
+Program Definition aux_simu_check (f1 f2: function) (ib1 ib2: iblock): ?? bool :=
    DO r <~ 
      (TRY 
-       imp_simu_check f tf;; 
+       simu_check_single f1 f2 ib1 ib2;; 
        RET true
       CATCH_FAIL s, _ =>
        println ("simu_check_failure:" +; s);;
        RET false
-      ENSURE (sexec_simu f tf));;
+       ENSURE (fun b => b=true -> symbolic_simu f1 f2 ib1 ib2));;
    RET (`r).
 Obligation 1.
   split; wlp_simplify. discriminate.
 Qed.
 
-Lemma aux_simu_check_correct f tf:
-  WHEN aux_simu_check f tf ~> b THEN
-  sexec_simu f tf.
+Lemma aux_simu_check_correct (f1 f2: function) (ib1 ib2: iblock):
+  WHEN aux_simu_check f1 f2 ib1 ib2 ~> b THEN
+  b=true -> symbolic_simu f1 f2 ib1 ib2.
 Proof.
   unfold aux_simu_check; wlp_simplify.
   destruct exta; simpl; auto.
@@ -1227,8 +1189,8 @@ Qed.
 
 Import UnsafeImpure.
 
-Definition simu_check (f tf: function) : res unit := 
-  match unsafe_coerce (aux_simu_check f tf) with
+Definition simu_check (f1 f2: function) (ib1 ib2: iblock): res unit := 
+  match unsafe_coerce (aux_simu_check f1 f2 ib1 ib2) with
   | Some true => OK tt
   | _ => Error (msg "simu_check has failed")
   end.
-- 
cgit