Implementing atomic-pair-snapshot example from Sergey et al. (ESOP'15)

_CoqProject

@@ -87,15 +87,19 @@ theories/heap_lang/notation.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v
 theories/heap_lang/total_adequacy.v
+theories/heap_lang/prophecy.v
 theories/heap_lang/lib/spawn.v
 theories/heap_lang/lib/par.v
 theories/heap_lang/lib/assert.v
 theories/heap_lang/lib/lock.v
 theories/heap_lang/lib/spin_lock.v
 theories/heap_lang/lib/ticket_lock.v
+theories/heap_lang/lib/coin_flip.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
+theories/heap_lang/lib/atomic_snapshot.v
+theories/heap_lang/lib/atomic_snapshot_spec.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v

theories/heap_lang/lib/atomic_snapshot.v

+From iris.algebra Require Import excl auth gmap agree.
+From iris.heap_lang Require Export lifting notation.
+From iris.base_logic.lib Require Export invariants.
+From iris.program_logic Require Export atomic.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation par prophecy.
+From iris.bi.lib Require Import fractional.
+Set Default Proof Using "Type".
+
+(** Specifying snapshots with histories
+    Implementing atomic pair snapshot data structure from Sergey et al. (ESOP 2015) *)
+
+(** The CMRA & functor we need. *)
+
+Definition timestampUR := gmapUR Z $ agreeR valC.
+
+Class atomic_snapshotG Σ := AtomicSnapshotG {
+                                atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ prodC valC valC;
+                                atomic_snapshot_timestampG :> inG Σ $ authR $ timestampUR
+}.
+Definition atomic_snapshotΣ : gFunctors :=
+  #[GFunctor (authR $ optionUR $ exclR $ prodC valC valC); GFunctor (authR timestampUR)].
+
+Instance subG_atomic_snapshotΣ {Σ} : subG atomic_snapshotΣ Σ → atomic_snapshotG Σ.
+Proof. solve_inG. Qed.
+
+Section atomic_snapshot.
+
+  Context {Σ} `{!heapG Σ, !atomic_snapshotG Σ}.
+
+  (*
+     newPair x y :=
+       (ref (ref (x, 0)), ref y)
+   *)
+  Definition newPair : val :=
+    λ: "args",
+      let: "x" := Fst "args" in
+      let: "y" := Snd "args" in
+      (ref (ref ("x", #0)), ref "y").
+
+  (*
+    writeY (xp, yp) y :=
+      yp <- y
+  *)
+  Definition writeY : val :=
+    λ: "args",
+      let: "p" := Fst "args" in
+      Snd "p" <- Snd "args".
+
+  (*
+    writeX (xp, yp) x :=
+      let xp1 = !xp in
+      let v   = (!xp1).2
+      let xp2 = ref (x, v + 1)
+      if CAS xp xp1 xp2
+        then ()
+        else writeX (xp, yp) x
+  *)
+  Definition writeX : val :=
+    rec: "writeX" "args" :=
+      let: "p"    := Fst "args"             in
+      let: "x"    := Snd "args"             in
+      let: "xp"   := Fst "p"                in
+      let: "xp1"  := !"xp"                  in
+      let: "v"    := Snd (!"xp1")           in
+      let: "xp2"  := ref ("x", "v" + #1)    in
+      if: CAS "xp" "xp1" "xp2"
+        then #()
+      else "writeX" "args".
+
+  (*
+    readX (xp, yp) :=
+      !!xp
+   *)
+  Definition readX : val :=
+    λ: "p",
+      let: "xp" := Fst "p" in
+      !(!"xp").
+
+   Definition readY : val :=
+    λ: "p",
+      let: "yp" := Snd "p" in
+      !"yp".
+
+  (*
+    readPair l :=
+      let (x, v)  = readX l in
+      let y       = readY l in
+      let (_, v') = readX l in
+      if v = v'
+        then (x, y)
+        else readPair l
+  *)
+  Definition readPair : val :=
+    rec: "readPair" "l" :=
+      let: "x"  := readX "l"  in
+      let: "y"  := readY "l"  in
+      let: "x'" := readX "l"  in
+      if: Snd "x" = Snd "x'"
+        then (Fst "x", Fst "y")
+        else  "readPair" "l".
+
+  Definition readPair_proph pr : val :=
+    rec: "readPair" "l" :=
+      let: "xv1"    := readX "l"           in
+      let: "proph"  := new_prophecy pr #() in
+      let: "y"      := readY "l"           in
+      let: "xv2"    := readX "l"           in
+      let: "v2"     := Snd "xv2"           in
+      let: "v_eq"   := Snd "xv1" = "v2"    in
+      resolve_prophecy pr "proph" "v_eq" ;;
+      if: "v_eq"
+        then (Fst "xv1", "y")
+      else "readPair" "l".
+
+  Variable N: namespace.
+
+  Definition gmap_to_UR T : timestampUR := to_agree <$> T.
+
+  Definition pair_inv γ1 γ2 l1 l2 : iProp Σ :=
+    (∃ q (l1':loc) (T : gmap Z val) x y (t : Z),
+      (* we add the q to make the l1' map fractional. that way,
+         we can take a fraction of the l1' map out of the invariant
+         and do a case analysis on whether the pointer is the same
+         throughout invariant openings *)
+      l1 ↦ #l1' ∗ l1' ↦{q} (x, #t) ∗ l2 ↦ y ∗
+         own γ1 (● Excl' (x, y)) ∗ own γ2 (● gmap_to_UR T) ∗
+         ⌜T !! t = Some x⌝ ∗
+         ⌜forall (t' : Z), t' ∈ dom (gset Z) T -> (t' <= t)%Z⌝)%I.
+
+  Definition is_pair (γs: gname * gname) (p : val) :=
+    (∃ (l1 l2 : loc), ⌜p = (#l1, #l2)%V⌝ ∗ inv N (pair_inv γs.1 γs.2 l1 l2))%I.
+
+  Global Instance is_pair_persistent γs p : Persistent (is_pair γs p) := _.
+
+  Definition pair_content (γs : gname * gname) (a : val * val) :=
+    (own γs.1 (◯ Excl' a))%I.
+
+  Global Instance pair_content_timeless γs a : Timeless (pair_content γs a) := _.
+
+  Lemma pair_content_exclusive γs a1 a2 :
+    pair_content γs a1 -∗ pair_content γs a2 -∗ False.
+  Proof.
+    iIntros "H1 H2". iDestruct (own_valid_2 with "H1 H2") as %[].
+  Qed.
+
+  Definition new_timestamp t v : gmap Z val := {[ t := v ]}.
+
+  Lemma newPair_spec (e : expr) (v1 v2 : val) :
+      IntoVal e (v1, v2) ->
+      {{{ True }}}
+        newPair e
+      {{{ γs p, RET p; is_pair γs p ∗ pair_content γs (v1, v2) }}}.
+  Proof.
+    iIntros (<- Φ _) "Hp". rewrite /newPair. wp_lam.
+    repeat (wp_proj; wp_let).
+    iApply wp_fupd.
+    wp_alloc lx' as "Hlx'".
+    wp_alloc lx as "Hlx".
+    wp_alloc ly as "Hly".
+    set (Excl' (v1, v2)) as p.
+    iMod (own_alloc (● p ⋅ ◯ p)) as (γ1) "[Hp⚫ Hp◯]". {
+      rewrite /p. apply auth_valid_discrete_2. split; done.
+    }
+    set (new_timestamp 0 v1) as t.
+    iMod (own_alloc (● gmap_to_UR t ⋅ ◯ gmap_to_UR t)) as (γ2) "[Ht⚫ Ht◯]". {
+      rewrite /t /new_timestamp. apply auth_valid_discrete_2.
+      split; first done. rewrite /gmap_to_UR map_fmap_singleton. apply singleton_valid. done.
+    }
+    iApply ("Hp" $! (γ1, γ2)).
+    iMod (inv_alloc N _ (pair_inv γ1 γ2 lx ly) with "[-Hp◯ Ht◯]") as "#Hinv". {
+      iNext. rewrite /pair_inv. iExists _, _, _, _, _. iExists 0. iFrame.
+      iPureIntro. split; first done. intros ?. subst t. rewrite /new_timestamp dom_singleton.
+      rewrite elem_of_singleton. lia.
+    }
+    iModIntro. iSplitR. rewrite /is_pair. repeat (iExists _). iSplitL; eauto.
+    rewrite /pair_content. rewrite /p. iApply "Hp◯".
+  Qed.
+
+ Lemma excl_update γ n' n m :
+    own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) ==∗
+      own γ (● (Excl' n')) ∗ own γ (◯ (Excl' n')).
+  Proof.
+    iIntros "Hγ● Hγ◯".
+    iMod (own_update_2 _ _ _ (● Excl' n' ⋅ ◯ Excl' n') with "Hγ● Hγ◯") as "[$$]".
+    { by apply auth_update, option_local_update, exclusive_local_update. }
+    done.
+  Qed.
+
+  Lemma excl_sync γ n m :
+    own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) -∗ ⌜m = n⌝.
+  Proof.
+    iIntros "Hγ● Hγ◯".
+    iDestruct (own_valid_2 with "Hγ● Hγ◯") as
+        %[H%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+    done.
+  Qed.
+
+  Lemma timestamp_dupl γ T:
+    own γ (● T) ==∗ own γ (● T) ∗ own γ (◯ T).
+  Proof.
+    iIntros "Ht". iApply own_op. iApply (own_update with "Ht").
+    apply auth_update_alloc. apply local_update_unital_discrete => f Hv. rewrite left_id => <-.
+    split; first done. apply core_id_dup. apply _.
+  Qed.
+
+  Lemma timestamp_update γ (T : gmap Z val) (t : Z) x :
+    T !! t = None ->
+    own γ (● gmap_to_UR T) ==∗ own γ (● gmap_to_UR (<[ t := x ]> T)).
+  Proof.
+    iIntros (HT) "Ht".
+    set (<[ t := x ]> T) as T'.
+    iDestruct (own_update _ _ (● gmap_to_UR T' ⋅ ◯ gmap_to_UR {[ t := x ]}) with "Ht") as "Ht". {
+      apply auth_update_alloc. rewrite /T' /gmap_to_UR map_fmap_singleton. rewrite fmap_insert.
+      apply alloc_local_update; last done. rewrite lookup_fmap HT. done.
+    }
+    iMod (own_op with "Ht") as "[Ht● Ht◯]". iModIntro. iFrame.
+  Qed.
+
+  Lemma fmap_undo {A B} (f : A -> B) (m : gmap Z A) k v :
+    f <$> m !! k = Some v ->
+    exists v', m !! k = Some v' /\ v = f v'.
+  Proof.
+    intros Hl. destruct (m !! k); inversion Hl. subst. eauto.
+  Qed.
+
+  Lemma timestamp_sub γ (T1 T2 : gmap Z val):
+    own γ (● gmap_to_UR T1) ∗ own γ (◯ gmap_to_UR T2) -∗
+    ⌜forall t x, T2 !! t = Some x -> T1 !! t = Some x⌝.
+  Proof.
+    iIntros "[Hγ⚫ Hγ◯]".
+    iDestruct (own_valid_2 with "Hγ⚫ Hγ◯") as
+        %[H Hv]%auth_valid_discrete_2. iPureIntro. intros t x Ht.
+    pose proof (iffLR (lookup_included (gmap_to_UR T2) (gmap_to_UR T1)) H t) as Hsub.
+    repeat rewrite lookup_fmap in Hsub.
+    rewrite Ht in Hsub. simpl in Hsub.
+    pose proof (mk_is_Some (Some (to_agree x)) _ eq_refl) as Hsome.
+    pose proof (is_Some_included _ _ Hsub Hsome) as Hsome'; clear Hsome.
+    destruct Hsome' as [c Heqx]. rewrite Heqx in Hsub.
+    apply (iffLR (Some_included_total _ _)) in Hsub.
+    destruct (fmap_undo to_agree _ _ _ Heqx) as [c' [Heq1 Heq2]]. subst.
+    apply to_agree_included  in Hsub. apply leibniz_equiv in Hsub. subst. done.
+  Qed.
+
+  Lemma writeY_spec e (y2: val) γ p :
+      IntoVal e y2 ->
+      is_pair γ p -∗
+      <<< ∀ x y : val, pair_content γ (x, y) >>>
+        writeY (p, e)
+        @ ⊤∖↑N
+      <<< pair_content γ (x, y2), RET #() >>>.
+  Proof.
+    iIntros (<-) "Hp". iApply wp_atomic_intro. iIntros (Φ) "AU".
+    iDestruct "Hp" as (l1 l2 ->) "#Hinv".
+    repeat (wp_lam; wp_proj). wp_proj.
+    iApply wp_fupd.
+    iInv N as (q l1' T x) "Hinvp".
+    iDestruct "Hinvp" as (y v') "[Hl1 [Hl1' [Hl2 [Hp⚫ Htime]]]]".
+    wp_store.
+    iMod "AU" as (xv yv) "[Hpair [_ Hclose]]".
+    rewrite /pair_content.
+    iDestruct (excl_sync with "Hp⚫ Hpair") as %[= -> ->].
+    iMod (excl_update _ (x, y2) with "Hp⚫ Hpair") as "[Hp⚫ Hp◯]".
+    iMod ("Hclose" with "Hp◯") as "HΦ".
+    iModIntro. iSplitR "HΦ"; last done.
+    iNext. unfold pair_inv. eauto 7 with iFrame.
+  Qed.
+
+  Lemma writeX_spec e (x2: val) γ p :
+      IntoVal e x2 ->
+      is_pair γ p  -∗
+      <<< ∀ x y : val, pair_content γ (x, y) >>>
+        writeX (p, e)
+        @ ⊤∖↑N
+      <<< pair_content γ (x2, y), RET #() >>>.
+  Proof.
+    iIntros (<-) "Hp". iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH".
+    iDestruct "Hp" as (l1 l2 ->) "#Hinv".
+    repeat (wp_lam; wp_proj). wp_lam. wp_bind (!_)%E.
+    (* first read *)
+    (* open invariant *)
+    iInv N as (q l1' T x) "Hinvp".
+      iDestruct "Hinvp" as (y v') "[Hl1 [Hl1' [Hl2 [Hp⚫ Htime]]]]".
+      wp_load.
+      iDestruct "Hl1'" as "[Hl1'frac1 Hl1'frac2]".
+      iModIntro. iSplitR "AU Hl1'frac2".
+      (* close invariant *)
+      { iNext. rewrite /pair_inv. eauto 10 with iFrame. }
+    wp_let. wp_bind (!_)%E. clear T.
+    wp_load. wp_proj. wp_let. wp_op. wp_alloc l1'new as "Hl1'new".
+    wp_let.
+    (* CAS *)
+    wp_bind (CAS _ _ _)%E.
+    (* open invariant *)
+    iInv N as (q' l1'' T x') ">Hinvp".
+    iDestruct  "Hinvp" as (y' v'') "[Hl1 [Hl1'' [Hl2 [Hp⚫ [Ht● Ht]]]]]".
+    iDestruct "Ht" as %[Ht Hvt].
+    destruct (decide (l1'' = l1')) as [-> | Hn].
+    - wp_cas_suc.
+      iDestruct (mapsto_agree with "Hl1'frac2 Hl1''") as %[= -> ->]. iClear "Hl1'frac2".
+      (* open AU *)
+      iMod "AU" as (xv yv) "[Hpair [_ Hclose]]".
+        (* update pair ghost state to (x2, y') *)
+        iDestruct (excl_sync with "Hp⚫ Hpair") as %[= -> ->].
+        iMod (excl_update _ (x2, y') with "Hp⚫ Hpair") as "[Hp⚫ Hp◯]".
+        (* close AU *)
+        iMod ("Hclose" with "Hp◯") as "HΦ".
+      (* update timestamp *)
+      iMod (timestamp_update _ T (v'' + 1)%Z x2 with "[Ht●]") as "Ht".
+      { eapply (not_elem_of_dom (D:=gset Z) T). intros Hd. specialize (Hvt _ Hd). omega. }
+      { done. }
+      (* close invariant *)
+      iModIntro. iSplitR "HΦ".
+      + iNext. rewrite /pair_inv.
+        set (<[ v'' + 1 := x2]> T) as T'.
+        iExists 1%Qp, l1'new, T', x2, y', (v'' + 1).
+        iFrame.
+        iPureIntro. split.
+        * apply: lookup_insert.
+        * intros ? Hv. destruct (decide (t' = (v'' + 1)%Z)) as [-> | Hn]; first done.
+          assert (dom (gset Z) T' = {[(v'' + 1)%Z]} ∪ dom (gset Z) T) as Hd. {
+            apply leibniz_equiv. rewrite dom_insert. done.
+          }
+          rewrite Hd in Hv. clear Hd. apply elem_of_union in Hv.
+          destruct Hv as [Hv%elem_of_singleton_1 | Hv]; first done.
+          specialize (Hvt _ Hv). lia.
+      + wp_if. done.
+    - wp_cas_fail. iModIntro. iSplitR "AU".
+      + iNext. rewrite /pair_inv. eauto 10 with iFrame.
+      + wp_if. iApply "IH"; last eauto. rewrite /is_pair. eauto.
+  Qed.
+
+  Lemma readY_spec γ p :
+    is_pair γ p -∗
+    <<< ∀ v1 v2 : val, pair_content γ (v1, v2) >>>
+      readY p
+      @ ⊤∖↑N
+    <<< pair_content γ (v1, v2), RET v2 >>>.
+  Proof.
+    iIntros "Hp". iApply wp_atomic_intro. iIntros (Φ) "AU".
+    iDestruct "Hp" as (l1 l2 ->) "#Hinv".
+    repeat (wp_lam; wp_proj). wp_let.
+    iApply wp_fupd.
+    iInv N as (q l1' T x) "Hinvp".
+    iDestruct "Hinvp" as (y v') "[Hl1 [Hl1' [Hl2 [Hp⚫ Htime]]]]".
+    wp_load.
+    iMod "AU" as (xv yv) "[Hpair [_ Hclose]]".
+    rewrite /pair_content.
+    iDestruct (excl_sync with "Hp⚫ Hpair") as %[= -> ->].
+    iMod ("Hclose" with "Hpair") as "HΦ".
+    iModIntro. iSplitR "HΦ"; last done.
+    iNext. unfold pair_inv. eauto 7 with iFrame.
+  Qed.
+
+  Lemma readX_spec γ p :
+    is_pair γ p -∗
+    <<< ∀ v1 v2 : val, pair_content γ (v1, v2) >>>
+      readX p
+      @ ⊤∖↑N
+    <<< ∃ (t: Z), pair_content γ (v1, v2), RET (v1, #t) >>>.
+  Proof.
+    iIntros "Hp". iApply wp_atomic_intro. iIntros (Φ) "AU".
+    iDestruct "Hp" as (l1 l2 ->) "#Hinv".
+    repeat (wp_lam; wp_proj). wp_let. wp_bind (! #l1)%E.
+    (* open invariant for 1st read *)
+    iInv N as (q l1' T x) ">Hinvp".
+      iDestruct "Hinvp" as (y v') "[Hl1 [Hl1' [Hl2 [Hp⚫ Htime]]]]".
+      wp_load.
+      iDestruct "Hl1'" as "[Hl1' Hl1'frac]".
+      iMod "AU" as (xv yv) "[Hpair [_ Hclose]]".
+      iDestruct (excl_sync with "Hp⚫ Hpair") as %[= -> ->].
+      iMod ("Hclose" with "Hpair") as "HΦ".
+      (* close invariant *)
+      iModIntro. iSplitR "HΦ Hl1'". {
+        iNext. unfold pair_inv. eauto 7 with iFrame.
+      }
+    iApply wp_fupd. clear T y.
+    wp_load. eauto.
+  Qed.
+
+  Definition val_to_bool (v:val) : bool :=
+    match v with
+    | LitV (LitBool b) => b
+    | _                => false
+    end.
+
+  Variable pr: prophecy.
+
+  Lemma readPair_spec γ p :
+    is_pair γ p -∗
+    <<< ∀ v1 v2 : val, pair_content γ (v1, v2) >>>
+       readPair_proph pr p
+       @ ⊤∖↑N
+    <<< pair_content γ (v1, v2), RET (v1, v2) >>>.
+  Proof.
+    iIntros "Hp". iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH".
+    wp_let.
+    (* ************ 1st readX ********** *)
+    iDestruct "Hp" as (l1 l2 ->) "#Hinv".
+    repeat (wp_lam; wp_proj). wp_let. wp_bind (! #l1)%E.
+    (* open invariant for 1st read *)
+    iInv N as (q_x1 l1' T_x x1) ">Hinvp".
+      iDestruct "Hinvp" as (y_x1 v_x1) "[Hl1 [Hl1' [Hl2 [Hp⚫ [Ht_x Htime_x]]]]]".
+      iDestruct "Htime_x" as %[Hlookup_x Hdom_x].
+      wp_load.
+      iDestruct "Hl1'" as "[Hl1' Hl1'frac]".
+      iMod "AU" as (xv yv) "[Hpair [Hclose _]]".
+      iDestruct (excl_sync with "Hp⚫ Hpair") as %[= -> ->].
+      iMod ("Hclose" with "Hpair") as "AU".
+      (* duplicate timestamp T_x1 *)
+      iMod (timestamp_dupl with "Ht_x") as "[Ht_x1⚫ Ht_x1◯]".
+      (* close invariant *)
+      iModIntro. iSplitR "AU Hl1' Ht_x1◯". {
+        iNext. unfold pair_inv. eauto 8 with iFrame.
+      }
+    wp_load. wp_let.
+    (* ************ new prophecy ********** *)
+    wp_apply new_prophecy_spec; first done.
+    iIntros (proph) "Hpr". iDestruct "Hpr" as (proph_val) "Hpr".
+    wp_let.
+    (* ************ readY ********** *)
+    repeat (wp_lam; wp_proj). wp_let. wp_bind (!_)%E.
+    iInv N as (q_y l1'_y T_y x_y) ">Hinvp".
+    iDestruct "Hinvp" as (y_y v_y) "[Hl1 [Hl1'_y [Hl2 [Hp⚫ [Ht_y Htime_y]]]]]".
+    iDestruct "Htime_y" as %[Hlookup_y Hdom_y].
+    wp_load.
+    (* linearization point *)
+    iMod "AU" as (xv yv) "[Hpair Hclose]".
+    rewrite /pair_content.
+    iDestruct (excl_sync with "Hp⚫ Hpair") as %[= -> ->].
+    destruct (val_to_bool proph_val) eqn:Hproph.
+    - (* prophecy value is predicting that timestamp has not changed, so we commit *)
+      (* committing AU *)
+      iMod ("Hclose" with "Hpair") as "HΦ".
+      (* duplicate timestamp T_y *)
+      iMod (timestamp_dupl with "Ht_y") as "[Ht_y● Ht_y◯]".
+      (* show that T_x <= T_y *)
+      iDestruct (timestamp_sub with "[Ht_y● Ht_x1◯]") as "#Hs"; first by iFrame.
+      iDestruct "Hs" as %Hs.
+      iModIntro.
+      (* closing invariant *)
+      iSplitR "HΦ Hl1' Ht_x1◯ Ht_y◯ Hpr".
+      { iNext. unfold pair_inv. eauto 10 with iFrame. }
+      wp_let.
+      (* ************ 2nd readX ********** *)
+      repeat (wp_lam; wp_proj). wp_let. wp_bind (! #l1)%E.
+      (* open invariant *)
+      iInv N as (q_x2 l1'_x2 T_x2 x2) ">Hinvp".
+      iDestruct "Hinvp" as (y_x2 v_x2) "[Hl1 [Hl1'_x2 [Hl2 [Hp⚫ [Ht_x2 Htime_x2]]]]]".
+      iDestruct "Htime_x2" as %[Hlookup_x2 Hdom_x2].
+      iDestruct "Hl1'_x2" as "[Hl1'_x2 Hl1'_x2_frag]".
+      wp_load.
+      (* show that T_y <= T_x2 *)
+      iDestruct (timestamp_sub with "[Ht_x2 Ht_y◯]") as "#Hs'"; first by iFrame.
+      iDestruct "Hs'" as %Hs'.
+      iModIntro. iSplitR "HΦ Hl1'_x2_frag Hpr". {
+        iNext. unfold pair_inv. eauto 8 with iFrame.
+      }
+      wp_load. wp_let. wp_proj. wp_let. wp_proj. wp_op.
+      case_bool_decide; wp_let; wp_apply (resolve_prophecy_spec with "Hpr");
+        iIntros (->); wp_seq; wp_if.
+      + inversion H; subst; clear H. wp_proj.
+        assert (v_x2 = v_y) as ->. {
+          assert (v_x2 <= v_y) as vneq. {
+            apply Hdom_y.
+            eapply (iffRL (elem_of_dom T_y _)). eauto using mk_is_Some.
+          }
+          assert (v_y <= v_x2) as vneq'. {
+            apply Hdom_x2.
+            eapply (iffRL (elem_of_dom T_x2 _)). eauto using mk_is_Some.
+          }
+          apply Z.le_antisymm; auto.
+        }
+        assert (x1 = x_y) as ->. {
+          specialize (Hs _ _ Hlookup_x). rewrite Hs in Hlookup_y. inversion Hlookup_y. done.
+        }
+        done.
+      + inversion Hproph.
+    - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hpair") as "AU".
+      iModIntro.
+      (* closing invariant *)
+      iSplitR "AU Hpr".
+      { iNext. unfold pair_inv. eauto 10 with iFrame. }
+      wp_let.
+      (* ************ 2nd readX ********** *)
+      repeat (wp_lam; wp_proj). wp_let. wp_bind (! #l1)%E.
+      (* open invariant *)
+      iInv N as (q_x2 l1'_x2 T_x2 x2) ">Hinvp".
+      iDestruct "Hinvp" as (y_x2 v_x2) "[Hl1 [Hl1'_x2 [Hl2 [Hp⚫ [Ht_x2 Htime_x2]]]]]".
+      iDestruct "Hl1'_x2" as "[Hl1'_x2 Hl1'_x2_frag]".
+      wp_load.
+      iModIntro. iSplitR "AU Hl1'_x2_frag Hpr". {
+        iNext. unfold pair_inv. eauto 8 with iFrame.
+      }
+      wp_load. repeat (wp_let; wp_proj). wp_op. wp_let.
+      wp_apply (resolve_prophecy_spec with "Hpr").
+      iIntros (Heq). subst.
+      case_bool_decide.
+      + inversion H; subst; clear H. inversion Hproph.
+      + wp_seq. wp_if. iApply "IH"; rewrite /is_pair; eauto.
+  Qed.
+
+End atomic_snapshot.

theories/heap_lang/lib/atomic_snapshot_spec.v

+From iris.algebra Require Import excl auth list.
+From iris.heap_lang Require Export lifting notation.
+From iris.base_logic.lib Require Export invariants.
+From iris.program_logic Require Export atomic.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation par prophecy.
+From iris.bi.lib Require Import fractional.
+Set Default Proof Using "Type".
+
+(** Specifying snapshots with histories
+    Implementing atomic pair snapshot data structure from Sergey et al. (ESOP 2015) *)
+
+Section atomic_snapshot_spec.
+
+  Record atomic_snapshot {Σ} `{!heapG Σ} := AtomicSnapshot {
+    newPair : val;
+    writeX : val;
+    writeY : val;
+    readPair : val;
+    (* other data *)
+    name: Type;
+    (* predicates *)
+    is_pair (N : namespace) (γ : name) (p : val) : iProp Σ;
+    pair_content (γ : name) (a: val * val) : iProp Σ;
+    (* predicate properties *)
+    is_pair_persistent N γ p : Persistent (is_pair N γ p);
+    pair_content_timeless γ a : Timeless (pair_content γ a);
+    pair_content_exclusive γ a1 a2 :
+      pair_content γ a1 -∗ pair_content γ a2 -∗ False;
+    (* specs *)
+    newPair_spec N (e : expr) (v1 v2 : val) :
+      IntoVal e (v1, v2) ->
+      {{{ True }}} newPair e {{{ γ p, RET p; is_pair N γ p ∗ pair_content γ (v1, v2) }}};
+    writeX_spec N e (v: val) p γ :
+      IntoVal e v ->
+      is_pair N γ p -∗
+      <<< ∀ v1 v2 : val, pair_content γ (v1, v2) >>>
+        writeX (p, e)
+        @ ⊤∖↑N
+      <<< pair_content γ (v, v2), RET #() >>>;
+    writeY_spec N e (v: val) p γ:
+      IntoVal e v ->
+      is_pair N γ p -∗
+      <<< ∀ v1 v2 : val, pair_content γ (v1, v2)  >>>
+        writeY (p, e)
+        @ ⊤∖↑N
+      <<< pair_content γ (v1, v), RET #() >>>;
+    readPair_spec N γ p :
+      is_pair N γ p -∗
+      <<< ∀ v1 v2 : val, pair_content γ (v1, v2) >>>
+        readPair p
+        @ ⊤∖↑N
+      <<< pair_content γ (v1, v2), RET (v1, v2) >>>;
+    }.
+
+  End atomic_snapshot_spec.