atomic_snapshot.v 17 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14
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.
From iris.bi.lib Require Import fractional.
From iris_examples.logatom.snapshot Require Import spec.
Set Default Proof Using "Type".

(** Specifying snapshots with histories
    Implementing atomic pair snapshot data structure from Sergey et al. (ESOP 2015) *)


15
(*
16 17
     newPair x y :=
       (ref (ref (x, 0)), ref y)
18 19 20 21 22 23 24 25
 *)
Definition newPair : val :=
  λ: "args",
  let: "x" := Fst "args" in
  let: "y" := Snd "args" in
  (ref (ref ("x", #0)), ref "y").

(*
26 27
    writeY (xp, yp) y :=
      yp <- y
28 29 30 31 32
 *)
Definition writeY : val :=
  λ: "args",
  let: "p" := Fst "args" in
  Snd "p" <- Snd "args".
33

34
(*
35 36 37 38 39 40 41
    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
42 43 44 45 46 47 48 49 50 51 52 53 54 55
 *)
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".

(*
56 57
    readX (xp, yp) :=
      !!xp
58 59 60 61 62 63 64 65 66 67 68 69
 *)
Definition readX : val :=
  λ: "p",
  let: "xp" := Fst "p" in
  !(!"xp").

Definition readY : val :=
  λ: "p",
  let: "yp" := Snd "p" in
  !"yp".

(*
70 71 72 73 74 75 76
    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
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
 *)
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 : val :=
  rec: "readPair" "l" :=
    let: "xv1"    := readX "l"           in
    let: "proph"  := NewProph            in
    let: "y"      := readY "l"           in
    let: "xv2"    := readX "l"           in
    let: "v2"     := Snd "xv2"           in
    let: "v_eq"   := Snd "xv1" = "v2"    in
    resolve_proph: "proph" to: "v_eq" ;;
    if: "v_eq"
      then (Fst "xv1", "y")
    else "readPair" "l".


(** The CMRA & functor we need. *)

Definition timestampUR := gmapUR Z $ agreeR valC.

Class atomic_snapshotG Σ := AtomicSnapshotG {
                                atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ valC;
                                atomic_snapshot_timestampG :> inG Σ $ authR $ timestampUR
}.
Definition atomic_snapshotΣ : gFunctors :=
  #[GFunctor (authR $ optionUR $ exclR $ valC); GFunctor (authR timestampUR)].

Instance subG_atomic_snapshotΣ {Σ} : subG atomic_snapshotΣ Σ  atomic_snapshotG Σ.
Proof. solve_inG. Qed.

Section atomic_snapshot.

  Context {Σ} `{!heapG Σ, !atomic_snapshotG Σ}.
118 119 120 121 122

  Variable N: namespace.

  Definition gmap_to_UR T : timestampUR := to_agree <$> T.

123 124
  Definition pair_inv γ1 γ2 l1 : iProp Σ :=
    ( q (l1':loc) (T : gmap Z val) x (t : Z),
125 126 127 128
      (* 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 *)
129 130
      l1  #l1'  l1' {q} (x, #t) 
         own γ1 ( Excl' x)  own γ2 ( gmap_to_UR T) 
131 132 133
         T !! t = Some x 
         forall (t' : Z), t'  dom (gset Z) T  (t' <= t)%Z)%I.

134 135
  Definition is_pair (γs: gname * gname * loc) (p : val) :=
    ( (l1 : loc), p = (#l1, #γs.2)%V  inv N (pair_inv γs.1.1 γs.1.2 l1))%I.
136 137 138

  Global Instance is_pair_persistent γs p : Persistent (is_pair γs p) := _.

139 140
  Definition pair_content (γs : gname * gname * loc) (a : val * val) :=
    (own γs.1.1 ( Excl' a.1)  γs.2  a.2)%I.
141 142 143 144 145 146

  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.
147
    iIntros "[H1 _] [H2 _]". iDestruct (own_valid_2 with "H1 H2") as %[].
148 149 150 151 152 153 154 155 156
  Qed.

  Definition new_timestamp t v : gmap Z val := {[ t := v ]}.

  Lemma newPair_spec (v1 v2 : val) :
      {{{ True }}}
        newPair (v1, v2)%V
      {{{ γs p, RET p; is_pair γs p  pair_content γs (v1, v2) }}}.
  Proof.
157
    iIntros (Φ _) "Hx". rewrite /newPair. wp_lam.
158 159
    repeat (wp_proj; wp_let).
    iApply wp_fupd.
160
    wp_alloc ly as "Hly".
161 162
    wp_alloc lx' as "Hlx'".
    wp_alloc lx as "Hlx".
163 164
    set (Excl' v1) as p.
    iMod (own_alloc ( p   p)) as (γ1) "[Hx⚫ Hx◯]". {
Hai Dang's avatar
Hai Dang committed
165
      rewrite /p. apply auth_both_valid. split; done.
166 167 168
    }
    set (new_timestamp 0 v1) as t.
    iMod (own_alloc ( gmap_to_UR t   gmap_to_UR t)) as (γ2) "[Ht⚫ Ht◯]". {
Hai Dang's avatar
Hai Dang committed
169
      rewrite /t /new_timestamp. apply auth_both_valid.
170 171
      split; first done. rewrite /gmap_to_UR map_fmap_singleton. apply singleton_valid. done.
    }
172 173 174
    wp_pures. iApply ("Hx" $! (γ1, γ2, ly)).
    iMod (inv_alloc N _ (pair_inv γ1 γ2 _) with "[-Hx◯ Ht◯ Hly]") as "#Hinv". {
      iNext. rewrite /pair_inv. iExists _, _, _, _, 0. iFrame.
175 176 177
      iPureIntro. split; first done. intros ?. subst t. rewrite /new_timestamp dom_singleton.
      rewrite elem_of_singleton. lia.
    }
178 179
    iModIntro. rewrite /is_pair /pair_content. iFrame. iExists _.
    iSplitL; first done. done.
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
  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
Hai Dang's avatar
Hai Dang committed
197
        %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
    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 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
Hai Dang's avatar
Hai Dang committed
228
        %[H Hv]%auth_both_valid. iPureIntro. intros t x HT2.
229 230 231 232 233 234 235 236 237 238 239 240 241 242 243
    pose proof (iffLR (lookup_included (gmap_to_UR T2) (gmap_to_UR T1)) H t) as Ht.
    rewrite !lookup_fmap HT2 /= in Ht.
    destruct (is_Some_included _ _ Ht) as [? [t2 [Ht2 ->]]%fmap_Some_1]; first by eauto.
    revert Ht.
    rewrite Ht2 Some_included_total to_agree_included. fold_leibniz.
    by intros ->.
  Qed.

  Lemma writeY_spec γ (y2: val) p :
      is_pair γ p -
      <<<  x y : val, pair_content γ (x, y) >>>
        writeY (p, y2)%V
        @ ∖↑N
      <<< pair_content γ (x, y2), RET #() >>>.
  Proof.
244 245
    iIntros "Hx". iIntros (Φ) "AU".
    iDestruct "Hx" as (l1 ->) "#Hinv". wp_pures.
246 247
    wp_lam. wp_pures.
    iApply wp_fupd.
248
    iMod "AU" as (xv yv) "[[Hx Hy] [_ Hclose]]".
249
    wp_store.
250 251 252
    iMod ("Hclose" with "[Hx Hy]") as "HΦ".
    { rewrite /pair_content. iFrame. }
    eauto.
253 254 255 256 257 258 259 260 261
  Qed.

  Lemma writeX_spec γ (x2: val) p :
      is_pair γ p  -
      <<<  x y : val, pair_content γ (x, y) >>>
        writeX (p, x2)%V
        @ ∖↑N
      <<< pair_content γ (x2, y), RET #() >>>.
  Proof.
262 263
    iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH".
    iDestruct "Hx" as (l1 ->) "#Hinv". wp_pures. wp_lam. wp_pures.
264 265
    (* first read *)
    (* open invariant *)
266
    wp_bind (!_)%E. iInv N as (q l1' T x v') "[Hl1 [Hl1' [Hx⚫ Htime]]]".
267 268 269 270 271 272 273 274 275 276 277
      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 *)
278
    iInv N as (q' l1'' T x' v'') ">[Hl1 [Hl1'' [Hx⚫ [Ht● Ht]]]]".
279 280 281 282 283
    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 *)
284
      iMod "AU" as (xv yv) "[[Hx Hy] [_ Hclose]]".
285
        (* update pair ghost state to (x2, y') *)
286 287
        iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
        iMod (excl_update _ x2 with "Hx⚫ Hx") as "[Hx⚫ Hx◯]".
288
        (* close AU *)
289 290
        iMod ("Hclose" with "[Hx◯ Hy]") as "HΦ".
        { rewrite /pair_content. iFrame. }
291 292 293 294 295 296 297 298
      (* 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'.
299
        iExists 1%Qp, l1'new, T', x2, (v'' + 1).
300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322
        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.
323 324
    iIntros "Hx". iIntros (Φ) "AU".
    iDestruct "Hx" as (l1 ->) "#Hinv".
325 326
    repeat (wp_lam; wp_proj). wp_let.
    iApply wp_fupd.
327
    iMod "AU" as (xv yv) "[[Hx Hy] [_ Hclose]]".
328 329
    wp_load.
    rewrite /pair_content.
330 331
    iMod ("Hclose" with "[$Hx $Hy]") as "HΦ".
    iModIntro. done.
332 333 334 335 336 337 338 339 340
  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.
341 342
    iIntros "Hx". iIntros (Φ) "AU".
    iDestruct "Hx" as (l1 ->) "#Hinv".
343 344
    repeat (wp_lam; wp_proj). wp_let. wp_bind (! #l1)%E.
    (* open invariant for 1st read *)
345
    iInv N as (q l1' T x v') ">[Hl1 [Hl1' [Hx⚫ Htime]]]".
346 347
      wp_load.
      iDestruct "Hl1'" as "[Hl1' Hl1'frac]".
348 349 350 351
      iMod "AU" as (xv yv) "[[Hx Hy] [_ Hclose]]".
      iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
      iMod ("Hclose" with "[Hx Hy]") as "HΦ".
      { rewrite /pair_content. iFrame. }
352 353 354 355
      (* close invariant *)
      iModIntro. iSplitR "HΦ Hl1'". {
        iNext. unfold pair_inv. eauto 7 with iFrame.
      }
356
    iApply wp_fupd. wp_load. eauto.
357 358
  Qed.

359
  Definition prophecy_to_bool (v : list (val * val)) : bool :=
360
    match v with
361 362
    | (_, LitV (LitBool b)) :: _ => b
    | _                          => false
363 364 365 366 367 368 369 370 371
    end.

  Lemma readPair_spec γ p :
    is_pair γ p -
    <<<  v1 v2 : val, pair_content γ (v1, v2) >>>
       readPair_proph p
       @ ∖↑N
    <<< pair_content γ (v1, v2), RET (v1, v2) >>>.
  Proof.
372
    iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH".
373 374
    wp_pures.
    (* ************ 1st readX ********** *)
375
    iDestruct "Hx" as (l1 ->) "#Hinv". repeat (wp_lam; wp_pures).
376 377
    wp_bind (! #l1)%E.
    (* open invariant for 1st read *)
378
    iInv N as (q_x1 l1' T_x x1 v_x1) ">[Hl1 [Hl1' [Hx⚫ [Ht_x Htime_x]]]]".
379 380 381
      iDestruct "Htime_x" as %[Hlookup_x Hdom_x].
      wp_load.
      iDestruct "Hl1'" as "[Hl1' Hl1'frac]".
382 383 384 385
      iMod "AU" as (xv yv) "[[Hx Hy] [Hclose _]]".
      iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
      iMod ("Hclose" with "[Hx Hy]") as "AU".
      { rewrite /pair_content. iFrame. }
386 387 388 389 390 391 392 393 394 395 396 397 398
      (* 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 wp_new_proph; first done.
    iIntros (proph_val proph) "Hpr".
    wp_let.
    (* ************ readY ********** *)
    repeat (wp_lam; wp_pures). wp_bind (!_)%E.
399
    iInv N as (q_y l1'_y T_y x_y v_y) ">[Hl1 [Hl1'_y [Hx⚫ [Ht_y Htime_y]]]]".
400 401
    iDestruct "Htime_y" as %[Hlookup_y Hdom_y].
    (* linearization point *)
402 403 404
    clear yv.
    iMod "AU" as (xv yv) "[[Hx Hy] Hclose]".
    wp_load.
405
    rewrite /pair_content.
406
    iDestruct (excl_sync with "Hx⚫ Hx") as %[= ->].
407
    destruct (prophecy_to_bool proph_val) eqn:Hproph.
408 409
    - (* prophecy value is predicting that timestamp has not changed, so we commit *)
      (* committing AU *)
410
      iMod ("Hclose" with "[$Hx $Hy]") as "HΦ".
411 412 413 414 415
      (* 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.
416
      iModIntro. iModIntro.
417 418 419 420 421 422 423
      (* 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_pures). wp_bind (! #l1)%E.
      (* open invariant *)
424
      iInv N as (q_x2 l1'_x2 T_x2 x2 v_x2) ">[Hl1 [Hl1'_x2 [Hx⚫ [Ht_x2 Htime_x2]]]]".
425 426 427 428 429 430 431 432 433 434 435
      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 (wp_resolve_proph with "Hpr");
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
436
        iIntros (vs') "[Eq _]"; iDestruct "Eq" as %->; wp_seq; wp_if.
437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453
      + inversion H; subst; clear H. wp_pures.
        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.
454 455
    - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "[$Hx $Hy]") as "AU".
      iModIntro. iModIntro.
456 457 458 459 460 461 462
      (* 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 *)
463
      iInv N as (q_x2 l1'_x2 T_x2 x2 v_x2) "[Hl1 [Hl1'_x2 [Hx⚫ [Ht_x2 Htime_x2]]]]".
464 465 466 467 468 469 470
      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 (wp_resolve_proph with "Hpr").
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
471
      iIntros (vs') "[Heq _]"; iDestruct "Heq" as %->.
472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487
      case_bool_decide.
      + inversion H; subst; clear H. inversion Hproph.
      + wp_seq. wp_if. iApply "IH"; rewrite /is_pair; eauto.
  Qed.

End atomic_snapshot.

Definition atomic_snapshot `{!heapG Σ, atomic_snapshotG Σ} :
  spec.atomic_snapshot Σ :=
  {| spec.newPair_spec := newPair_spec;
     spec.writeX_spec := writeX_spec;
     spec.writeY_spec := writeY_spec;
     spec.readPair_spec := readPair_spec;
     spec.pair_content_exclusive := pair_content_exclusive |}.

Typeclasses Opaque pair_content is_pair.