Merge remote-tracking branch 'origin/eq-loc'

_CoqProject

@@ -27,6 +27,7 @@ theories/lang/lib/new_delete.v
 theories/lang/lib/spawn.v
 theories/lang/lib/lock.v
 theories/lang/lib/arc.v
+theories/lang/lib/tests.v
 theories/typing/base.v
 theories/typing/type.v
 theories/typing/util.v

theories/lang/lib/tests.v

+From iris.program_logic Require Import weakestpre.
+From iris.proofmode Require Import tactics.
+From lrust.lang Require Import lang proofmode notation.
+Set Default Proof Using "Type".
+
+Section tests.
+  Context `{!lrustG Σ}.
+
+  Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
+    {{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}
+      #l1 = #l2 @ E
+    {{{ (b: bool), RET LitV (lit_of_bool b); (if b then ⌜l1 = l2⌝ else ⌜l1 ≠ l2⌝) ∗
+                                     l1 ↦{q1} v1 ∗ l2 ↦{q2} v2 }}}.
+  Proof.
+    iIntros (Φ) "[Hl1 Hl2] HΦ". wp_op; try (by eauto); [|];
+      intros ?; iApply "HΦ"; by iFrame.
+  Qed.
+End tests.

theories/lang/lifting.v

@@ -268,15 +268,54 @@ Lemma wp_eq_int E (n1 n2 : Z) P Φ :
   (n1 ≠ n2 → P -∗ ▷ Φ (LitV false)) →
   P -∗ WP BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
-  iIntros (Hl Hg) "HP".
-  destruct (bool_decide_reflect (n1 = n2)); [rewrite Hl //|rewrite Hg //];
-    clear Hl Hg; iApply wp_bin_op_pure; subst.
+  iIntros (Heq Hne) "HP".
+  destruct (bool_decide_reflect (n1 = n2)); [rewrite Heq //|rewrite Hne //];
+    clear Hne Heq; iApply wp_bin_op_pure; subst.
   - intros. apply BinOpEqTrue. constructor.
   - iNext; iIntros (?? Heval). by inversion_clear Heval; inv_lit.
   - intros. apply BinOpEqFalse. by constructor.
   - iNext; iIntros (?? Heval). by inversion_clear Heval; inv_lit.
 Qed.
 
+Lemma wp_eq_loc E (l1 : loc) (l2: loc) P Φ :
+  (P -∗ ∃ q v, ▷ l1 ↦{q} v) →
+  (P -∗ ∃ q v, ▷ l2 ↦{q} v) →
+  (l1 = l2 → P -∗ ▷ Φ (LitV true)) →
+  (l1 ≠ l2 → P -∗ ▷ Φ (LitV false)) →
+  P -∗ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
+Proof.
+  iIntros (Hl1 Hl2 Heq Hne) "HP".
+  destruct (bool_decide_reflect (l1 = l2)).
+  - rewrite Heq // {Heq Hne}. iApply wp_bin_op_pure; subst.
+    + intros. apply BinOpEqTrue. constructor.
+    + iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
+  - clear Heq. iApply wp_lift_atomic_head_step_no_fork; subst=>//.
+    iIntros (σ1) "Hσ1". iModIntro. inv_head_step.
+    iSplitR.
+    { iPureIntro. eexists _, _, _. constructor. apply BinOpEqFalse. by auto. }
+    (* We need to do a little gymnastics here to apply Hne now and strip away a
+       ▷ but also have the ↦s. *)
+    iAssert ((▷ ∃ q v, l1 ↦{q} v) ∧ (▷ ∃ q v, l2 ↦{q} v) ∧ ▷ Φ (LitV false))%I with "[HP]" as "HP".
+    { iSplit; last iSplit.
+      - iDestruct (Hl1 with "HP") as (??) "?". iNext. eauto.
+      - iDestruct (Hl2 with "HP") as (??) "?". iNext. eauto.
+      - by iApply Hne. }
+    clear Hne Hl1 Hl2. iNext.
+    iIntros (e2 σ2 efs Hs) "!>".
+    inv_head_step. iSplitR=>//.
+    match goal with [ H : bin_op_eval _ _ _ _ _ |- _ ] => inversion H end;
+      inv_lit=>//.
+    * iExFalso. iDestruct "HP" as "[Hl1 _]".
+      iDestruct "Hl1" as (??) "Hl1".
+      iDestruct (heap_read σ2 with "Hσ1 Hl1") as (n') "%".
+      simplify_eq.
+    * iExFalso. iDestruct "HP" as "[_ [Hl2 _]]".
+      iDestruct "Hl2" as (??) "Hl2".
+      iDestruct (heap_read σ2 with "Hσ1 Hl2") as (n') "%".
+      simplify_eq.
+    * iDestruct "HP" as "[_ [_ $]]". done.
+Qed.
+
 Lemma wp_eq_loc_0_r E (l : loc) P Φ :
   (P -∗ ▷ Φ (LitV false)) →
   P -∗ WP BinOp EqOp (Lit (LitLoc l)) (Lit (LitInt 0)) @ E {{ Φ }}.
@@ -293,8 +332,6 @@ Proof.
   rewrite HΦ. iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
 Qed.
 
-(* TODO: wp_eq for locations, if needed. *)
-
 Lemma wp_offset E l z Φ :
   ▷ Φ (LitV $ LitLoc $ l +ₗ z) -∗
     WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.

theories/lang/proofmode.v

@@ -94,6 +94,8 @@ Tactic Notation "wp_op" :=
     | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; 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 EqOp (Lit (LitLoc _)) (Lit (LitInt 0)) =>
       wp_bind_core K; apply wp_eq_loc_0_r; wp_finish
     | BinOp EqOp (Lit (LitInt 0)) (Lit (LitLoc _)) =>