Proof of simplify_correct

1 files changed, 101 insertions, 45 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 91937ffb..de67185b 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -556,13 +556,6 @@ Global Opaque PTree_frame_eq_check.
 
 (** hsilocal_simu_check and properties *)
 
-Lemma ssem_local_sok ge sp rs0 m0 st rs m:
-  ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st.
-Proof.
-  unfold sok_local, ssem_local. 
-  intuition congruence.
-Qed.
-
 Definition seval_hsval ge sp hsv rs0 m0 := seval_sval ge sp (hsval_proj hsv) rs0 m0.
 Definition seval_hsmem ge sp hsm rs0 m0 := seval_smem ge sp (hsmem_proj hsm) rs0 m0.
 
@@ -593,6 +586,13 @@ Definition hsilocal_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_loca
   /\  (hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0)
   /\  (forall r sv, hst ! r = Some sv -> In sv (hsi_ok_lsval hst)).
 
+Lemma ssem_local_sok ge sp rs0 m0 st rs m:
+  ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st.
+Proof.
+  unfold sok_local, ssem_local. 
+  intuition congruence.
+Qed.
+
 Lemma ssem_local_refines_hok ge sp rs0 m0 hst st rs m:
   ssem_local ge sp st rs0 m0 rs m -> hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst.
 Proof.
@@ -1936,6 +1936,100 @@ Proof.
   eapply may_trap_correct; eauto.
 Qed. *)
 
+Lemma seval_list_sval_proj ge sp rs0 m0: forall lhsv lsv,
+  list_refines ge sp rs0 m0 lhsv lsv ->
+  seval_list_sval ge sp (hsval_list_proj lhsv) rs0 m0 = seval_list_sval ge sp lsv rs0 m0.
+Proof.
+  induction lhsv.
+  - destruct lsv; simpl; intros H; [reflexivity | inv H].
+  - destruct lsv; [intro H; inv H|].
+    intros. inv H. simpl. erewrite IHlhsv; eauto.
+    rewrite H6. reflexivity.
+Qed.
+
+Lemma hSop_correct ge sp rs0 m0 op lhsv lsv hst st:
+  WHEN hSop op lhsv (hsi_smem hst) ~> hsv THEN
+  hsok_local ge sp rs0 m0 hst ->
+  list_refines ge sp rs0 m0 lhsv lsv ->
+  hsilocal_refines ge sp rs0 m0 hst st ->
+  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv (si_smem st)) rs0 m0.
+Proof.
+  wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval.
+  rewrite <- Hexta1. simpl. clear Hexta1.
+  erewrite seval_list_sval_proj; eauto. clear H0.
+  destruct H1 as (A & B & C & D). rewrite <- B; eauto.
+Qed.
+
+(** Version of hSop_correct with weaker hypothesis *)
+Lemma hSop_correct_mem ge sp rs0 m0 op lhsv lsv hsm sm:
+  WHEN hSop op lhsv hsm ~> hsv THEN
+  seval_hsmem ge sp hsm rs0 m0 = seval_smem ge sp sm rs0 m0 ->
+  list_refines ge sp rs0 m0 lhsv lsv ->
+  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv sm) rs0 m0.
+Proof.
+  wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval.
+  rewrite <- Hexta1. simpl. clear Hexta1.
+  erewrite seval_list_sval_proj; eauto. clear H0.
+  rewrite <- H. eauto.
+Qed.
+
+Lemma hSload_correct ge sp rs0 m0 lhsv lsv hst st trap addr chunk:
+  WHEN hSload (hsi_smem hst) trap chunk addr lhsv ~> hsv THEN
+  hsok_local ge sp rs0 m0 hst ->
+  list_refines ge sp rs0 m0 lhsv lsv ->
+  hsilocal_refines ge sp rs0 m0 hst st ->
+  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sload (si_smem st) trap chunk addr lsv) rs0 m0.
+Proof.
+  wlp_simplify. apply hC_hsval_correct in Hexta3. simpl in *. unfold seval_hsval.
+  rewrite <- Hexta3. simpl. clear Hexta3.
+  erewrite seval_list_sval_proj; eauto. clear H0.
+  destruct H1 as (A & B & C & D). rewrite <- B; eauto.
+Qed.
+
+Lemma hsinit_sinit ge sp rs0 m0:
+  WHEN hSinit () ~> init THEN
+  seval_hsmem ge sp init rs0 m0 = seval_smem ge sp Sinit rs0 m0.
+Proof.
+  wlp_intro init. eapply hsinit_seval_hsmem in Hinit; eauto.
+Qed.
+
+Lemma simplify_correct (rsv: root_sval) lr (ge: RTL.genv) (sp: val) rs0 m0 v hst st:
+  WHEN root_apply rsv lr hst ~> hsv THEN
+  hsok_local ge sp rs0 m0 hst ->
+  hsilocal_refines ge sp rs0 m0 hst st ->
+  seval_hsval ge sp hsv rs0 m0 = Some v ->
+  WHEN simplify rsv lr hst ~> hsv' THEN
+  seval_hsval ge sp hsv' rs0 m0 = Some v.
+Proof.
+  wlp_bind lhsv. wlp_intro hsv. intros HOK HREF HEVAL.
+  eapply hlist_args_correct in Hlhsv; eauto.
+  destruct rsv; simpl.
+  (* Rop *)
+  - exploit hSop_correct; eauto. intros EVALMOV. clear Hlhsv. clear Hhsv.
+    destruct (is_move_operation _ _) eqn:IMOVE.
+    + apply is_move_operation_correct in IMOVE. inv IMOVE.
+      rewrite <- HEVAL. rewrite EVALMOV. wlp_intro hsv'.
+      simpl. destruct HREF as (A & B & C & D). rewrite <- C; eauto.
+      rewrite hsi_sreg_eval_correct; eauto.
+      destruct (seval_hsval ge sp hsv' rs0 m0); [|reflexivity].
+      apply A in HOK. destruct HOK as (_ & MOK & _).
+      destruct (seval_smem _ _ _ _ _); [reflexivity|contradiction].
+    + clear IMOVE. wlp_bind hsm. wlp_bind lhsv'. wlp_intro hsv'.
+      eapply hlist_args_correct in Hlhsv'; eauto.
+      rewrite hSop_correct_mem; eauto; [|eapply hsinit_sinit; eauto].
+      clear Hlhsv'. clear Hhsv'. rewrite <- HEVAL. rewrite EVALMOV.
+      admit. (** Voir avec Sylvain - je ne sais plus où on en est sur les dépendances mémoires avec les op *)
+  (* Rload *)
+  - exploit hSload_correct; eauto. intros EVALLOAD.
+    wlp_bind lhsv'. wlp_intro hsv'. eapply hlist_args_correct in Hlhsv'; eauto.
+    rewrite hSload_correct; eauto. rewrite EVALLOAD in HEVAL.
+    destruct trap; simpl; auto. simpl in HEVAL.
+    destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence.
+    destruct (eval_addressing _ _ _ _) as [a|] eqn: Ha; try congruence.
+    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
+    rewrite HEVAL. reflexivity.
+Admitted.
+
 (** TODO - express some lemma about root_apply_correct and simplify_correct
   * Figure out how to prove this stuff *)
 Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lr sv':
@@ -1969,31 +2063,6 @@ Proof.
       rewrite <- RVAL, hsi_sreg_eval_correct; auto. *)
 Admitted.
 
-
-Lemma seval_list_sval_proj ge sp rs0 m0: forall lhsv lsv,
-  list_refines ge sp rs0 m0 lhsv lsv ->
-  seval_list_sval ge sp (hsval_list_proj lhsv) rs0 m0 = seval_list_sval ge sp lsv rs0 m0.
-Proof.
-  induction lhsv.
-  - destruct lsv; simpl; intros H; [reflexivity | inv H].
-  - destruct lsv; [intro H; inv H|].
-    intros. inv H. simpl. erewrite IHlhsv; eauto.
-    rewrite H6. reflexivity.
-Qed.
-
-Lemma hSop_correct ge sp rs0 m0 op lhsv lsv hst st:
-  WHEN hSop op lhsv (hsi_smem hst) ~> hsv THEN
-  hsok_local ge sp rs0 m0 hst ->
-  list_refines ge sp rs0 m0 lhsv lsv ->
-  hsilocal_refines ge sp rs0 m0 hst st ->
-  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sop op lsv (si_smem st)) rs0 m0.
-Proof.
-  wlp_simplify. apply hC_hsval_correct in Hexta1. simpl in *. unfold seval_hsval.
-  rewrite <- Hexta1. simpl. clear Hexta1.
-  erewrite seval_list_sval_proj; eauto. clear H0.
-  destruct H1 as (A & B & C & D). rewrite <- B; eauto.
-Qed.
-
 Lemma seval_list_hsval_refines ge sp rs0 m0 hst st lr:
   hsok_local ge sp rs0 m0 hst ->
   hsilocal_refines ge sp rs0 m0 hst st ->
@@ -2033,19 +2102,6 @@ Proof.
   apply seval_list_sval_none. assumption.
 Qed.
 
-Lemma hSload_correct ge sp rs0 m0 lhsv lsv hst st trap addr chunk:
-  WHEN hSload (hsi_smem hst) trap chunk addr lhsv ~> hsv THEN
-  hsok_local ge sp rs0 m0 hst ->
-  list_refines ge sp rs0 m0 lhsv lsv ->
-  hsilocal_refines ge sp rs0 m0 hst st ->
-  seval_hsval ge sp hsv rs0 m0 = seval_sval ge sp (Sload (si_smem st) trap chunk addr lsv) rs0 m0.
-Proof.
-  wlp_simplify. apply hC_hsval_correct in Hexta3. simpl in *. unfold seval_hsval.
-  rewrite <- Hexta3. simpl. clear Hexta3.
-  erewrite seval_list_sval_proj; eauto. clear H0.
-  destruct H1 as (A & B & C & D). rewrite <- B; eauto.
-Qed.
-
 (* Local Hint Resolve refines_okargs: core. *)
 Lemma hsiexec_inst_correct_dyn ge sp rs0 m0 i hst st hst' st':
   WHEN hsiexec_inst i hst ~> ohst' THEN