From f995f01c747877cb8595dbf71b05d23205d697d8 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 7 Jul 2021 16:21:13 +0200 Subject: some progress in canonbuilding --- scheduling/BTL_SEimpl.v | 120 ++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 106 insertions(+), 14 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index a2b5cc43..25819ffa 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -474,6 +474,8 @@ Proof. - intros X; inversion REF. erewrite H1; eauto. Qed. +Global Opaque hrexec_store. +Local Hint Resolve hrexec_store_correct: wlp. (** ** Assignment of registers *) @@ -786,9 +788,103 @@ Qed. Global Opaque hrs_sreg_set. Local Hint Resolve hrs_sreg_set_correct: wlp. +(* transfer *) + +Lemma ok_hrset_red_sreg ctx r rsv hrs: + ris_ok ctx (ris_sreg_set hrs (red_PTree_set r rsv hrs)) + <-> (ris_ok ctx hrs). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. +Qed. + +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 => {| ris_smem := hrs.(ris_smem); + ris_input_init := false; + ok_rsval := hrs.(ok_rsval); + ris_sreg:= PTree.empty _ + |} + | r::l => + let hrs' := transfer_hrs l hrs in + ris_sreg_set hrs' (red_PTree_set r (ris_sreg_get hrs r) hrs') + end. + +Lemma ok_transfer_hrs ctx inputs hrs: + ris_ok ctx (transfer_hrs inputs hrs) + <-> (ris_ok ctx hrs). +Proof. + induction inputs as [|r l]; simpl. + + split; destruct 1; econstructor; simpl in *; intuition eauto. + + rewrite ok_hrset_red_sreg. auto. +Qed. + +Lemma transfer_hrs_correct ctx inputs hrs sis: + ris_refines ctx hrs sis -> + ris_refines ctx (transfer_hrs inputs hrs) (transfer_sis inputs sis). +Proof. + destruct 1; intros. + induction inputs as [|r l]. + + econstructor; eauto. + * erewrite ok_transfer_sis, ok_transfer_hrs; eauto. + * erewrite ok_transfer_hrs; eauto. + * erewrite ok_transfer_hrs; simpl; unfold ris_sreg_get; simpl; eauto. + intros; rewrite PTree.gempty. simpl; auto. + + econstructor; eauto. + * erewrite ok_transfer_sis, ok_transfer_hrs; eauto. + * erewrite ok_transfer_hrs; simpl. + intros; inversion IHl. erewrite MEM_EQ0. + - unfold transfer_sis; simpl; eauto. + - rewrite ok_transfer_hrs; simpl; eauto. + * erewrite ok_transfer_hrs; simpl. + intros H r0; inversion IHl. + erewrite red_PTree_set_refines; eauto. + - destruct (Pos.eq_dec); eauto. + - rewrite ok_transfer_hrs. auto. +Qed. + +Definition tr_hrs := poly_tr (fun f tbl or => transfer_hrs (Regset.elements (pre_inputs f tbl or))). + +Local Hint Resolve transfer_hrs_correct ok_transfer_hrs: core. +Local Opaque transfer_hrs. + +Lemma ok_tr_hrs ctx fi hrs: + ris_ok ctx (tr_hrs (cf ctx) fi hrs) + <-> (ris_ok ctx hrs). +Proof. + destruct fi; simpl; eauto. +Qed. + +Lemma hrs_ok_tr_okpreserv ctx fi hrs: ris_ok ctx (tr_hrs (cf ctx) fi hrs) -> ris_ok ctx hrs. +Proof. + rewrite ok_tr_hrs; auto. +Qed. + +Lemma tr_hrs_correct ctx fi hrs sis: + ris_refines ctx hrs sis -> + ris_refines ctx (tr_hrs (cf ctx) fi hrs) (tr_sis (cf ctx) fi sis). +Proof. + intros REF. rewrite <- tr_sis_alt_def. + destruct fi; simpl; eauto. +Qed. + Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := match ib with - | BF fin _ => RET (Rfinal (tr_ris f fin hrs) (sexec_final_sfv fin hrs)) + | BF fin _ => RET (Rfinal (tr_hrs f fin hrs) (sexec_final_sfv fin hrs)) (* basic instructions *) | Bnop _ => k hrs | Bop op args dst _ => @@ -817,6 +913,9 @@ Definition hrexec f ib := DO init <~ hrs_init;; hrexec_rec f ib init (fun _ => RET Rabort). +Local Hint Resolve exec_final_refpreserv tr_hrs_correct hrs_ok_tr_okpreserv: core. +Local Hint Constructors rst_refines: core. + Lemma hrexec_rec_correct1 ctx ib: forall rk k (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) @@ -835,23 +934,16 @@ Lemma hrexec_rec_correct1 ctx ib: WHEN hrexec_rec (cf ctx) ib hrs rk ~> rst THEN rst_refines ctx rst st. Proof. - induction ib; wlp_simplify. - - admit. - - eapply CONT; eauto. - - autodestruct; try_simplify_someHyps; try congruence; intros; subst. -(* - unfold sexec_load. - exploit hrs_sreg_set_correct; eauto. - eapply CONT; eauto. - destruct next. - - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto. + induction ib; try (wlp_simplify; fail). + - wlp_simplify; eapply CONT; eauto. + - destruct trap; wlp_simplify. - (* seq *) - intros; subst. - eapply IHib1. 3-6: eauto. + wlp_simplify. + eapply IHib1. 3-7: eauto. + simpl. eapply sexec_rec_okpreserv; eauto. + intros; subst. eapply IHib2; eauto. - (* cond *) - intros rk k CONTh CONT hrs sis lsis sfv st REF EXEC OUT OK. subst. + simpl; intros; wlp_simplify. assert (rOK: ris_ok ctx hrs). { erewrite <- OK_EQUIV. 2: eauto. eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. -- cgit