A bit of new Ltac and renaming

1 files changed, 70 insertions, 23 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index ec48c975..91937ffb 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -20,14 +20,29 @@ Local Open Scope impure.
 Import ListNotations.
 Local Open Scope list_scope.
 
-Ltac wlp_intro varname hname := apply wlp_unfold; intros varname hname.
-Ltac wlp_bind varname hname := apply wlp_bind; wlp_intro varname hname.
+Ltac wlp_intro vname hname := apply wlp_unfold; intros vname hname.
+Ltac wlp_bind vname hname := apply wlp_bind; intros vname hname.
+Ltac wlp_ret vname := let H := fresh "H" vname in wlp_intro vname H; apply mayRet_ret in H; subst.
+
+Tactic Notation "wlp_intro" ident(v) ident(h) := wlp_intro v h.
+Tactic Notation "wlp_intro" ident(v) := let H := fresh "H" v in wlp_intro v H.
+Tactic Notation "wlp_bind" ident(v) ident(h) := wlp_bind v h.
+Tactic Notation "wlp_bind" ident(v) := let H := fresh "H" v in wlp_bind v H.
 
 Ltac wlp_absurd := match goal with
   | [ H : FAILWITH ?msg |- _ ] => eapply (_FAILWITH_correct _ _ (fun _ => False)) in H; inv H
   | [ H : DO r <~ fail ?msg;; RET ?expr ~~> ?exta |- _ ] => eapply (_FAILWITH_correct _ _ (fun _ => False)) in H; inv H
 end.
 
+Ltac wlp_hbind var := match goal with
+  | [ H : DO _ <~ ?expr;; _ ~~> _ |- _ ] => 
+      let Hvar := fresh "H" var in (apply mayRet_bind in H; destruct H as (var & Hvar & H))
+  end.
+
+Ltac wlp_hret := match goal with
+  | [ H : RET _ ~~> _ |- _ ] => apply mayRet_ret in H; subst; clear H
+  end.
+
 (** * Implementation of Data-structure use in Hash-consing *)
 
 (** ** Implementation of symbolic values/symbolic memories with hash-consing data *)
@@ -373,14 +388,14 @@ Definition red_PTree_set (r: reg) (hsv: hsval) (hst: PTree.t hsval): PTree.t hsv
   | _ => PTree.set r hsv hst
   end.
 
-Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) lsv: ?? hsistate_local :=
-  DO hsiok <~
-   (if may_trap rsv lsv
-    then DO hv <~ root_apply rsv lsv hst;; RET (hv::(hsi_ok_lsval hst))
+Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local :=
+  DO ok_lhsv <~
+   (if may_trap rsv lr
+    then DO hv <~ root_apply rsv lr hst;; RET (hv::(hsi_ok_lsval hst))
     else RET (hsi_ok_lsval hst));;
-  DO simp <~ simplify rsv lsv hst;;
+  DO simp <~ simplify rsv lr hst;;
   RET {| hsi_smem := hst;
-         hsi_ok_lsval := hsiok;
+         hsi_ok_lsval := ok_lhsv;
          hsi_sreg := red_PTree_set r simp (hsi_sreg hst) |}.
 
 (** ** Execution of one instruction *)
@@ -1047,7 +1062,7 @@ Remark init_hsistate_correct_dyn ge sp rs0 m0 pc:
   WHEN init_hsistate pc ~> hst THEN
   hsistate_refines_dyn ge sp rs0 m0 hst (init_sistate pc).
 Proof.
-  unfold init_hsistate. wlp_bind hst HST.
+  unfold init_hsistate. wlp_bind hst.
   wlp_simplify.
   constructor; simpl; auto; [|constructor].
   - apply list_forall2_nil.
@@ -1529,7 +1544,7 @@ Lemma sval_refines_local_get ge sp rs0 m0 hsl sl r:
   WHEN hsi_sreg_get hsl r ~> hsv THEN
   sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
 Proof.
-  intros HOK HREF. wlp_intro hsv HSV. unfold sval_refines.
+  intros HOK HREF. wlp_intro hsv. unfold sval_refines.
   erewrite <- hsi_sreg_eval_correct; eauto.
   destruct HREF as (_ & _ & A & _). rewrite <- A; [| assumption].
   reflexivity.
@@ -1542,7 +1557,7 @@ Lemma hsum_left_correct ge sp rs0 m0 hsl sl ros:
   sum_refines ge sp rs0 m0 svos (sum_left_map (si_sreg sl) ros).
 Proof.
   intros HOK HREF. destruct ros; [| wlp_simplify].
-  wlp_bind hr HGET. wlp_simplify. unfold sval_refines.
+  wlp_bind hr. wlp_simplify. unfold sval_refines.
   rewrite sval_refines_local_get; eauto.
 Qed.
 
@@ -1573,7 +1588,7 @@ Lemma hsi_sreg_get_refines ge sp rs0 m0 hsl sl r:
   WHEN hsi_sreg_get hsl r ~> hsv THEN
   sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
 Proof.
-  intros HOK HREF. wlp_intro hsv HGET. destruct HREF as (_ & _ & A & _).
+  intros HOK HREF. wlp_intro hsv. destruct HREF as (_ & _ & A & _).
   unfold sval_refines. erewrite <- hsi_sreg_eval_correct by eassumption.
   rewrite A by assumption. reflexivity.
 Qed.
@@ -1599,7 +1614,7 @@ Lemma hsval_proj_correct ge sp rs0 m0 hsl sl hsv r:
   hsval_proj hsv = hsval_proj hsv' ->
   sval_refines ge sp rs0 m0 hsv (si_sreg sl r).
 Proof.
-  intros HOK HREF. wlp_intro hsv' HGET. intros PROJ.
+  intros HOK HREF. wlp_intro hsv'. intros PROJ.
   unfold sval_refines. unfold seval_hsval.
   rewrite PROJ. enough (seval_sval ge sp (hsval_proj hsv') rs0 m0 = seval_hsval ge sp hsv' rs0 m0) as ->; [|reflexivity].
   erewrite hsi_sreg_get_refines; eauto.
@@ -1614,8 +1629,8 @@ Lemma hlist_args_correct ge sp rs0 m0 hsl sl:
 Proof.
   intros HOK HREF. induction lr.
   - simpl. wlp_simplify. destruct exta; try discriminate. constructor.
-  - simpl. wlp_bind v V. wlp_bind lhsv HLSV. wlp_simplify.
-    apply IHlr in HLSV. clear IHlr.
+  - simpl. wlp_bind v. wlp_bind lhsv. wlp_simplify.
+    apply IHlr in Hlhsv. clear IHlr.
     destruct exta; try discriminate. simpl in H. inv H. constructor.
     + eapply hsval_list_proj_correct; eauto.
     + eapply hsval_proj_correct; eauto.
@@ -1634,7 +1649,7 @@ Proof.
   induction br.
   all: try (wlp_simplify; constructor; auto; fail).
   (* BA *)
-  - simpl. wlp_bind hsv HGET. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
+  - simpl. wlp_bind hsv. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
 Qed.
 
 Lemma hbuiltin_args_correct ge sp rs0 m0 hsl sl:
@@ -1646,7 +1661,7 @@ Lemma hbuiltin_args_correct ge sp rs0 m0 hsl sl:
 Proof.
   intros HOK HREF.
   induction lbr; [wlp_simplify; constructor|].
-  simpl. wlp_bind ha HA. wlp_bind hl HL. wlp_simplify.
+  simpl. wlp_bind ha. wlp_bind hl. wlp_simplify.
   constructor; [|auto]. eapply hbuiltin_arg_correct; eauto.
 Qed.
 
@@ -1659,20 +1674,20 @@ Proof.
   intro HOK.
   destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone).
   (* Scall *)
-  - wlp_bind svos SVOS. wlp_bind sargs SARGS. wlp_simplify. constructor.
+  - wlp_bind svos. wlp_bind sargs. wlp_simplify. constructor.
     + eapply hsum_left_correct; eauto.
     + eapply hlist_args_correct; eauto.
   (* Stailcall *)
-  - wlp_bind svos SVOS. wlp_bind sargs SARGS. wlp_simplify. constructor.
+  - wlp_bind svos. wlp_bind sargs. wlp_simplify. constructor.
     + eapply hsum_left_correct; eauto.
     + eapply hlist_args_correct; eauto.
   (* Sbuiltin *)
   - wlp_simplify. constructor. eapply hbuiltin_args_correct; eauto.
   (* Sjumptable *)
-  - wlp_bind sv SV. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
+  - wlp_bind sv. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto.
   (* Sreturn *)
   - destruct o.
-    -- wlp_bind sv HGET. wlp_simplify. constructor. simpl.
+    -- wlp_bind sv. wlp_simplify. constructor. simpl.
        eapply hsi_sreg_get_refines; eauto.
     -- wlp_simplify. repeat constructor.
 Qed.
@@ -1748,12 +1763,12 @@ Proof.
   - destruct bs2; wlp_simplify; try wlp_absurd. congruence.
   (* BA_splitlong *)
   - destruct bs2; try (wlp_simplify; wlp_absurd). simpl.
-    wlp_bind b1 B1. wlp_intro b2 B2.
+    wlp_bind b1. wlp_intro b2.
     rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption.
     reflexivity.
   (* BA_addptr *)
   - destruct bs2; try (wlp_simplify; wlp_absurd). simpl.
-    wlp_bind b1 B1. wlp_intro b2 B2.
+    wlp_bind b1. wlp_intro b2.
     rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption.
     reflexivity.
 Qed.
@@ -1898,6 +1913,31 @@ Proof.
   destruct NESTED as [|st0 se lse TOP NEST]; econstructor; simpl; auto.
 Qed.
 
+(* Completely lost on that one *)
+(* Lemma hsok_local_set_sreg ge sp rs0 m0 hst r (rsv:root_sval) lr:
+  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
+  hok_args ge sp rs0 m0 hst lr ->
+  hsok_local ge sp rs0 m0 hst'
+  <-> (hsok_local ge sp rs0 m0 hst /\ (WHEN root_apply rsv lr hst ~> hsv THEN seval_hsval ge sp hsv rs0 m0 <> None)).
+Proof.
+  unfold hslocal_set_sreg. wlp_bind lhsvok. wlp_bind hsv. wlp_ret hst'.
+  intros HOK.
+  destruct may_trap eqn: MAYTRAP.
+  - wlp_hbind hv. wlp_hret. constructor.
+    + unfold hsok_local. simpl. intro. constructor.
+      * intros. apply H. right. assumption.
+      * wlp_intro hsv'. apply H.
+
+
+  unfold hok_args, hsok_local. simpl.
+
+  unfold hslocal_set_sreg, ok_args, hsok_local; simpl.
+  destruct may_trap eqn: MAYTRAP; simpl; intuition (subst; eauto).
+  eapply may_trap_correct; eauto.
+Qed. *)
+
+(** 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':
   WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN
   hsilocal_refines ge sp rs0 m0 hst st ->
@@ -1907,6 +1947,12 @@ Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lr sv':
     seval_sval ge sp sv' rs0 m0 = seval_hsval ge sp hsv rs0 m0) ->
   hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r sv').
 Proof.
+  unfold hslocal_set_sreg. wlp_bind lhsvok. wlp_bind hsv. wlp_ret hst'.
+  intros (ROK & RMEM & RVAL) OKA RSV.
+  unfold hsilocal_refines. simpl.
+  split.
+  + rewrite <- ROK in RSV.
+
 (*   intros (ROK & RMEM & RVAL) OKA RSV.
   unfold hsilocal_refines; simpl. rewrite! hsok_local_set_sreg; eauto. split.
   + rewrite <- ROK in RSV; rewrite sok_local_set_sreg; eauto.
@@ -1923,6 +1969,7 @@ 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.