Commit d5ce8079 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

proof of fsval_proj_correct

parent 9a0cf394
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment