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