diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-01 17:06:58 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-01 17:06:58 +0100 |
commit | d5ce8079b6a9bb35d44911fa7d9631c2f5cb5efb (patch) | |
tree | 68fb484b6f0f3833d51a95e42a47b2e484ef9910 | |
parent | 9a0cf394fb3b3e0e7ae064c4d7cec218c52a2828 (diff) | |
download | compcert-kvx-d5ce8079b6a9bb35d44911fa7d9631c2f5cb5efb.tar.gz compcert-kvx-d5ce8079b6a9bb35d44911fa7d9631c2f5cb5efb.zip |
proof of fsval_proj_correct
-rw-r--r-- | scheduling/RTLpathSE_impl.v | 34 |
1 files changed, 27 insertions, 7 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index f98dc11c..76d046fd 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -292,6 +292,15 @@ Definition hSop (op:operation) (lhsv: list_hsval): ?? hsval := DO hv <~ hSop_hcodes op lhsv;; hC_hsval {| hdata:=HSop op lhsv unknown_hid; hcodes :=hv |}. +Lemma hSop_fSop_correct op lhsv: + WHEN hSop op lhsv ~> hv THEN forall ge sp rs0 m0, + seval_hsval ge sp hv rs0 m0 = seval_hsval ge sp (fSop op lhsv) rs0 m0. +Proof. + wlp_simplify. +Qed. +Global Opaque hSop. +Local Hint Resolve hSop_fSop_correct: wlp_raw. + Lemma hSop_correct op lhsv: WHEN hSop op lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm m (MEM: seval_smem ge sp sm rs0 m0 = Some m) @@ -299,12 +308,11 @@ Lemma hSop_correct op lhsv: (LR: list_sval_refines ge sp rs0 m0 lhsv lsv), sval_refines ge sp rs0 m0 hv (Sop op lsv sm). Proof. - wlp_simplify. - rewrite <- H, MEM, LR. - destruct (seval_list_sval _ _ lsv _); try congruence. - eapply op_valid_pointer_eq; eauto. + generalize fSop_correct; simpl. + intros X. + wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw). + erewrite H, X; eauto. Qed. -Global Opaque hSop. Local Hint Resolve hSop_correct: wlp. Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval):= @@ -469,14 +477,26 @@ with fsval_list_proj hsl: ?? list_hsval := Lemma fsval_proj_correct hsv: WHEN fsval_proj hsv ~> hsv' THEN forall ge sp rs0 m0, seval_hsval ge sp hsv rs0 m0 = seval_hsval ge sp hsv' rs0 m0. -Admitted. +Proof. + induction hsv using hsval_mut + with (P0 := fun lhsv => + WHEN fsval_list_proj lhsv ~> lhsv' THEN forall ge sp rs0 m0, + seval_list_hsval ge sp lhsv rs0 m0 = seval_list_hsval ge sp lhsv' rs0 m0) + (P1 := fun sm => True); try (wlp_simplify; tauto). + - wlp_xsimplify ltac:(intuition eauto with wlp_raw wlp). + rewrite H, H0; auto. + - wlp_simplify; erewrite H0, H1; eauto. +Qed. Global Opaque fsval_proj. Local Hint Resolve fsval_proj_correct: wlp. Lemma fsval_list_proj_correct lhsv: WHEN fsval_list_proj lhsv ~> lhsv' THEN forall ge sp rs0 m0, seval_list_hsval ge sp lhsv rs0 m0 = seval_list_hsval ge sp lhsv' rs0 m0. -Admitted. +Proof. + induction lhsv; wlp_simplify. + erewrite H0, H1; eauto. +Qed. Global Opaque fsval_list_proj. Local Hint Resolve fsval_list_proj_correct: wlp. |