diff options
Diffstat (limited to 'scheduling/BTL_SEimpl.v')
| -rw-r--r-- | scheduling/BTL_SEimpl.v | 23 |
1 files changed, 12 insertions, 11 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, |