branches expansions support

2 files changed, 17 insertions, 16 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index 7711c72d..305c3cfa 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -682,12 +682,13 @@ Lemma cbranch_expanse_correct hrs c l:
   (REF : ris_refines ctx hrs sis)
   (OK: ris_ok ctx hrs),
   eval_scondition ctx (fst r) (snd r) =
-  eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l))
-  /\ (fst r) = c.
+  eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)).
 Proof.
   unfold cbranch_expanse.
-  wlp_simplify; inv REF.
-  unfold eval_scondition; erewrite <- H; eauto.
+  destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify;
+  unfold eval_scondition; try erewrite <- H; inversion REF; eauto.
+  destruct p as [c' l']; simpl.
+  exploit target_cbranch_expanse_correct; eauto.
 Qed.
 Local Hint Resolve cbranch_expanse_correct: wlp.
 Global Opaque cbranch_expanse.
@@ -1133,9 +1134,9 @@ Proof.
       erewrite <- OK_EQUIV. 2: eauto.
       eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
     }
-    exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
+    exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
               (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k));
-    exploit H; eauto; intros (SEVAL & EQC); subst; auto.
+    exploit H; eauto; intros SEVAL; auto.
     all:
       simpl in SOUT; generalize SOUT; clear SOUT;
       inversion_SOME b0; try_simplify_someHyps.
@@ -1217,9 +1218,9 @@ Proof.
     assert (rOK: ris_ok ctx hrs). {
       simpl in H2; generalize H2; inversion_SOME b0; destruct b0; try_simplify_someHyps.
     }
-    exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
+    exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
               (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k));
-    exploit H; eauto; intros (SEVAL & EQC); subst; auto.
+    exploit H; eauto; intros SEVAL; auto.
     all:
       simpl in H2; generalize H2; clear H2;
       inversion_SOME b0; try_simplify_someHyps.
@@ -1444,11 +1445,11 @@ Fixpoint rst_simu_check (rst1 rst2: rstate) {struct rst1} :=
       hrs_simu_check hrs1 hrs2;;
       sfval_simu_check sfv1 sfv2
   | Rcond cond1 lsv1 rsL1 rsR1, Rcond cond2 lsv2 rsL2 rsR2 =>
-      struct_check cond1 cond2 "hsstate_simu_check: conditions do not match";;
-      phys_check lsv1 lsv2 "hsstate_simu_check: args do not match";;
+      struct_check cond1 cond2 "rst_simu_check: conditions do not match";;
+      phys_check lsv1 lsv2 "rst_simu_check: args do not match";;
       rst_simu_check rsL1 rsL2;;
       rst_simu_check rsR1 rsR2
-  | _, _ => FAILWITH "hsstate_simu_check: simu_check failed"
+  | _, _ => FAILWITH "rst_simu_check: simu_check failed"
   end.
 
 Lemma rst_simu_check_correct rst1: forall rst2,
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index c812c607..7af1af62 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -260,11 +260,11 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop :=
       (RIS: ris_refines ctx ris sis)
       (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv)
       : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv)
-  | Refcond cond rargs args rifso rifnot ifso ifnot
-      (RCOND: eval_scondition ctx cond rargs = eval_scondition ctx cond args)
-      (REFso: eval_scondition ctx cond rargs = Some true -> rst_refines ctx rifso ifso)
-      (REFnot: eval_scondition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot)
-      : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args ifso ifnot)
+  | Refcond rcond cond rargs args rifso rifnot ifso ifnot
+      (RCOND: eval_scondition ctx rcond rargs = eval_scondition ctx cond args)
+      (REFso: eval_scondition ctx rcond rargs = Some true -> rst_refines ctx rifso ifso)
+      (REFnot: eval_scondition ctx rcond rargs = Some false -> rst_refines ctx rifnot ifnot)
+      : rst_refines ctx (Rcond rcond rargs rifso rifnot) (Scond cond args ifso ifnot)
   | Refabort
       : rst_refines ctx Rabort Sabort
   .