prove the trick of simplify (as implemented in RTLpathSE_impl_junk)

1 files changed, 6 insertions, 18 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index 96da94e9..7be12f78 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -977,20 +977,17 @@ Definition simplify (rsv: root_sval) lsv sm: sval :=
   | Rop op =>
      match is_move_operation op lsv with
      | Some arg => arg  (* optimization of Omove *)
-     | None => 
-       if op_depends_on_memory op then
-          rsv lsv sm
-       else
-          Sop op (list_sval_inj lsv) Sinit (* magically remove the dependency on sm ! *)
+     | None => Sop op (list_sval_inj lsv) Sinit (* magically remove the dependency on sm ! *)
      end
   | _ => rsv lsv sm
   end.
 
 Lemma simplify_correct (rsv: root_sval) lsv sm (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) v:
+  (forall m b ofs, seval_smem ge sp sm rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) ->
   seval_sval ge sp (rsv lsv sm) rs0 m0 = Some v ->
   seval_sval ge sp (simplify rsv lsv sm) rs0 m0 = Some v.
 Proof.
-  destruct rsv; simpl; auto.
+  intros MVALID; destruct rsv; simpl; auto.
   - (* Rop *)
     destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence.
     destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
@@ -999,9 +996,9 @@ Proof.
     + exploit is_move_operation_correct; eauto.
       intros (Hop & Hlsv); subst; simpl in *.
       explore. auto.
-    + clear Hmove; destruct (op_depends_on_memory op) eqn: Hop; simpl; explore; try congruence.
+    + clear Hmove; simpl; explore; try congruence.
       inversion Hargs; subst.
-      erewrite op_depends_on_memory_correct; eauto.
+      erewrite <- op_valid_pointer_eq; eauto.
   - (* Rload *)
     destruct trap; simpl; auto.
     destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence.
@@ -1030,16 +1027,6 @@ Proof.
   - rewrite PTree.gro, PTree.gso; simpl; auto.
 Qed.
 
-(* naive version:
-@Cyril: éventuellement, tu peux utiliser la version naive dans un premier temps pour simplifier les preuves...
-
-Definition naive_hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv sm :=
-  let sv := rsv lsv sm in
-  {| hsi_lsmem := hsi_lsmem hst;
-     hsi_ok_lsval := sv::(hsi_ok_lsval hst);
-     hsi_sreg:= PTree.set r sv (hsi_sreg hst) |}.
-*)
-
 Definition hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv :=
   {| hsi_smem := hsi_smem hst;
      hsi_ok_lsval := if may_trap rsv lsv (hsi_smem hst) then (rsv lsv (hsi_smem hst))::(hsi_ok_lsval hst) else hsi_ok_lsval hst;
@@ -1093,6 +1080,7 @@ Proof.
     * subst. rewrite PTree.gss, RSV; auto.
       destruct (seval_sval ge sp (rsv lsv (hsi_smem hst))) eqn: RSV3; simpl; try congruence.
       eapply simplify_correct; eauto.
+      intros m b ofs; rewrite RMEM; eauto.
     * intros; rewrite PTree.gso; auto.
       rewrite <- RVAL, hsi_sreg_eval_correct; auto.
 Qed.