From 4b370424090ab9e87fdf48ea5b04482728f99b7f Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 30 Jun 2021 17:37:03 +0200
Subject: cbranch expanse

---
 scheduling/BTL_SEimpl.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'scheduling')

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index f01f1cc0..df8cc47f 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -502,6 +502,31 @@ Proof.
     + erewrite H0; eauto.
 Qed.
 
+Definition cbranch_expanse (prev: ristate) (cond: condition) (args: list reg): ?? (condition * list_sval) :=
+  (* TODO gourdinl  
+  match target_cbranch_expanse prev cond args with
+    | Some (cond', vargs) => 
+      DO vargs' <~ fsval_list_proj vargs;;
+      RET (cond', vargs')
+     | None =>*)
+      DO vargs <~ hlist_args prev args ;;
+      RET (cond, vargs).
+    (*end.*)
+
+Lemma cbranch_expanse_correct hrs c l:
+ WHEN cbranch_expanse hrs c l ~> r THEN forall ctx st
+  (REF : ris_refines ctx hrs st)
+  (OK: ris_ok ctx hrs),
+  eval_scondition ctx (fst r) (snd r) =
+  eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)).
+Proof.
+  unfold cbranch_expanse.
+  wlp_simplify; inv REF.
+  unfold eval_scondition; erewrite <- H; eauto.
+Qed.
+Local Hint Resolve cbranch_expanse_correct: wlp.
+Global Opaque cbranch_expanse.
+
 Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
   match o with
   | Some x => RET x
-- 
cgit