From d5ce8079b6a9bb35d44911fa7d9631c2f5cb5efb Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Mon, 1 Mar 2021 17:06:58 +0100
Subject: proof of fsval_proj_correct

---
 scheduling/RTLpathSE_impl.v | 34 +++++++++++++++++++++++++++-------
 1 file changed, 27 insertions(+), 7 deletions(-)

(limited to 'scheduling/RTLpathSE_impl.v')

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.
 
-- 
cgit