From 6c7fcc52c8e8196c79fc544cae853a2bb3ca2df0 Mon Sep 17 00:00:00 2001
From: Joshua Yanovski <pythonesque@gmail.com>
Date: Tue, 29 Aug 2017 12:52:44 +0200
Subject: [PATCH] Adding location equality.
---
theories/lang/lifting.v | 32 +++++++++++++++++++++++++++++++-
theories/lang/proofmode.v | 5 ++++-
2 files changed, 35 insertions(+), 2 deletions(-)
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index bea9a136..2d5be607 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -240,7 +240,7 @@ Proof.
iApply step_fupd_intro; done.
Qed.
-(* TODO: wp_eq for locations, if needed.
+(*
Lemma wp_bin_op_heap E σ op l1 l2 l' :
bin_op_eval σ op l1 l2 l' →
{{{ ▷ ownP σ }}} BinOp op (Lit l1) (Lit l2) @ E
@@ -290,6 +290,36 @@ Proof.
- iNext; iIntros (?? Heval). by inversion_clear Heval; inv_lit.
Qed.
+Lemma wp_eq_loc E (l1 : loc) (l2: loc) P Φ :
+ (l1 = l2 → P -∗ ▷ Φ (LitV true)) →
+ (l1 ≠ l2 → P -∗ ▷ Φ (LitV false)) →
+ (∃ q1 vl1 q2 vl2, l1 ↦{q1} vl1 ∧ l2 ↦{q2} vl2)%I -∗
+ P -∗ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
+Proof.
+ iIntros (Hl Hg) "Hp HP".
+ iDestruct "Hp" as (q1 vl1 q2 vl2) "Hp".
+ destruct (bool_decide_reflect (l1 = l2)); [rewrite Hl //|rewrite Hg //];
+ clear Hl Hg.
+ - iApply wp_bin_op_pure; subst.
+ + intros. apply BinOpEqTrue. constructor.
+ + iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
+ - iApply wp_lift_atomic_head_step_no_fork; subst=>//.
+ iIntros. iModIntro. inv_head_step.
+ iSplitR.
+ { iPureIntro. eexists _, _, _. constructor. apply BinOpEqFalse. by auto. }
+ iNext.
+ iIntros (e2 σ2 efs Hs) "!>".
+ inv_head_step. iSplitR=>//.
+ inversion H7; inv_lit=>//.
+ * iDestruct "Hp" as "[Hp _]".
+ iDestruct (heap_read σ2 with "~ Hp") as (n') "%".
+ by rewrite H0 in H6.
+ * iDestruct "Hp" as "[_ Hp]".
+ iDestruct (heap_read σ2 with "~ Hp") as (n') "%".
+ by rewrite H0 in H6.
+ * by iFrame.
+Qed.
+
Lemma wp_offset E l z Φ :
▷ Φ (LitV $ LitLoc $ shift_loc l z) -∗
WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 2b47b30c..843c7a55 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -92,7 +92,10 @@ Tactic Notation "wp_op" :=
| |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
- | BinOp EqOp _ _ => wp_bind_core K; apply wp_eq_int; wp_finish
+ | BinOp EqOp (Lit (LitInt _)) (Lit (LitInt _)) =>
+ wp_bind_core K; apply wp_eq_int; wp_finish
+ | BinOp EqOp (Lit (LitLoc _)) (Lit (LitLoc _)) =>
+ wp_bind_core K; apply wp_eq_loc; wp_finish
| BinOp OffsetOp _ _ =>
wp_bind_core K; etrans; [|eapply wp_offset; try fast_done]; wp_finish
| BinOp PlusOp _ _ =>
--
GitLab