diff options
Diffstat (limited to 'scheduling/BTL_SEimpl.v')
| -rw-r--r-- | scheduling/BTL_SEimpl.v | 20 |
1 files changed, 1 insertions, 19 deletions
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index aa27bd19..65d16d01 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -745,7 +745,6 @@ Proof. rewrite Heq; eauto. Qed. -(* TODO gourdinl move this in BTL_SEtheory? *) Lemma eval_list_sval_inj_not_none ctx st: forall l, (forall r, List.In r l -> eval_sval ctx (si_sreg st r) = None -> False) -> eval_list_sval ctx (list_sval_inj (map (si_sreg st) l)) = None -> False. @@ -853,23 +852,6 @@ Proof. split; destruct 1; econstructor; simpl in *; eauto. Qed. -(* TODO useless? -Lemma hrset_red_reg_correct ctx r rsv sv hrs sis: - ris_refines ctx hrs sis -> - (ris_ok ctx hrs -> eval_sval ctx rsv <> None) -> - (ris_ok ctx hrs -> eval_sval ctx rsv = eval_sval ctx sv) -> - ris_refines ctx (ris_sreg_set hrs (red_PTree_set r rsv hrs)) (set_sreg r sv sis). -Proof. - destruct 1; intros. - econstructor; eauto. - + rewrite ok_set_sreg, ok_hrset_red_sreg; intuition congruence. - + rewrite ok_hrset_red_sreg; intuition eauto. - + rewrite ok_hrset_red_sreg. intros; unfold set_sreg; simpl; - erewrite red_PTree_set_refines; eauto. - econstructor; eauto. -Qed. - *) - Fixpoint transfer_hrs (inputs: list reg) (hrs: ristate): ?? ristate := match inputs with | nil => RET {| ris_smem := hrs.(ris_smem); @@ -1474,7 +1456,7 @@ Definition simu_check_single (f1 f2: function) (ibf1 ibf2: iblock_info): ?? unit Lemma simu_check_single_correct (f1 f2: function) (ibf1 ibf2: iblock_info): WHEN simu_check_single f1 f2 ibf1 ibf2 ~> _ THEN symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). -Proof. (* TODO *) +Proof. unfold symbolic_simu; wlp_simplify. eapply rst_simu_correct; eauto. + intros; eapply hrexec_correct1; eauto; wlp_simplify. |