From d579dc8dedafd52d02938d664492a64311069619 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 Jun 2019 11:59:52 +0200
Subject: [PATCH] bump Iris for comparison changes

---
 opam                                          |  2 +-
 .../concurrent_stacks/concurrent_stack1.v     | 85 ++++++++++---------
 .../concurrent_stacks/concurrent_stack2.v     | 78 ++++++++---------
 .../concurrent_stacks/concurrent_stack3.v     | 65 +++++++-------
 .../concurrent_stacks/concurrent_stack4.v     | 65 +++++++-------
 theories/hocap/fg_bag.v                       | 77 +++++++++--------
 theories/logatom/elimination_stack/stack.v    | 12 ++-
 theories/logatom/treiber2.v                   |  6 +-
 theories/logrel_heaplang/ltyping.v            |  5 +-
 theories/spanning_tree/spanning.v             |  4 +-
 10 files changed, 209 insertions(+), 190 deletions(-)

diff --git a/opam b/opam
index 5888ae5e..1611db52 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2019-06-18.2.e039d7c7") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-18.8.72595700") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/concurrent_stacks/concurrent_stack1.v b/theories/concurrent_stacks/concurrent_stack1.v
index 2ce3dd95..ef691423 100644
--- a/theories/concurrent_stacks/concurrent_stack1.v
+++ b/theories/concurrent_stacks/concurrent_stack1.v
@@ -36,9 +36,19 @@ Section stacks.
     iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
   Qed.
 
-  Definition is_list_pre (P : val → iProp Σ) (F : val -d> iProp Σ) :
-     val -d> iProp Σ := λ v,
-    (v ≡ NONEV ∨ ∃ (l : loc) (h t : val), ⌜v ≡ SOMEV #l⌝ ∗ l ↦{-} (h, t)%V ∗ P h ∗ ▷ F t)%I.
+  Definition oloc_to_val (ol: option loc) : val :=
+    match ol with
+    | None => NONEV
+    | Some loc => SOMEV (#loc)
+    end.
+  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
+  Proof. intros [|][|]; simpl; congruence. Qed.
+
+  Definition is_list_pre (P : val → iProp Σ) (F : option loc -d> iProp Σ) :
+     option loc -d> iProp Σ := λ v, match v with
+     | None => True
+     | Some l => ∃ (h : val) (t : option loc), l ↦{-} (h, oloc_to_val t)%V ∗ P h ∗ ▷ F t
+     end%I.
 
   Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P).
   Proof.
@@ -58,28 +68,22 @@ Section stacks.
     rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
   Qed.
 
-  (* TODO: shouldn't have to explicitly return is_list *)
-  Lemma is_list_unboxed (P : val → iProp Σ) v :
-      is_list P v -∗ ⌜val_is_unboxed v⌝ ∗ is_list P v.
-  Proof.
-    iIntros "Hstack"; iSplit; last done;
-    iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]";
-    last iDestruct "Hstack" as (l h t) "(-> & _)"; done.
-  Qed.
-
-  Lemma is_list_disj (P : val → iProp Σ) v :
-    is_list P v -∗ is_list P v ∗ (⌜v ≡ NONEV⌝ ∨ ∃ (l : loc) h t, ⌜v ≡ SOMEV #l%V⌝ ∗ l ↦{-} (h, t)%V).
+  Lemma is_list_dup (P : val → iProp Σ) v :
+    is_list P v -∗ is_list P v ∗ match v with
+      | None => True
+      | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+      end.
   Proof.
-    iIntros "Hstack".
-    iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq.
-    - rewrite is_list_unfold; iSplitR; [iLeft|]; eauto.
-    - iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)".
-      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq.
-      rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame.
+    iIntros "Hstack". iDestruct (is_list_unfold with "Hstack") as "Hstack".
+    destruct v as [l|].
+    - iDestruct "Hstack" as (h t) "(Hl & Hlist)".
+      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
+      rewrite (is_list_unfold _ (Some _)); iSplitR "Hl2"; iExists _, _; by iFrame.
+    - rewrite is_list_unfold; iSplitR; eauto.
   Qed.
 
   Definition stack_inv P v :=
-    (∃ l v', ⌜v = #l⌝ ∗ l ↦ v' ∗ is_list P v')%I.
+    (∃ l ol', ⌜v = #l⌝ ∗ l ↦ oloc_to_val ol' ∗ is_list P ol')%I.
 
   Definition is_stack (P : val → iProp Σ) v :=
     inv N (stack_inv P v).
@@ -92,8 +96,8 @@ Section stacks.
     wp_lam.
     wp_alloc â„“ as "Hl".
     iMod (inv_alloc N ⊤ (stack_inv P #ℓ) with "[Hl]") as "Hinv".
-    { iNext; iExists â„“, NONEV; iFrame;
-      by iSplit; last (iApply is_list_unfold; iLeft). }
+    { iNext; iExists â„“, None; iFrame;
+      by iSplit; last (iApply is_list_unfold). }
     by iApply "Hpost".
   Qed.
 
@@ -109,17 +113,17 @@ Section stacks.
     { iNext; iExists _, _; by iFrame. }
     iModIntro. wp_let. wp_alloc â„“' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
     iInv N as (â„“'' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq.
-    destruct (decide (v' = v'')) as [ -> |].
-    - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
-      wp_cas_suc.
+    destruct (decide (v' = v'')) as [->|Hne].
+    - wp_cas_suc. { destruct v''; left; done. }
       iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
-      { iNext; iExists _, (InjRV #â„“'); iFrame; iSplit; first done;
-        rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. }
+      { iNext; iExists _, (Some â„“'); iFrame; iSplit; first done;
+        rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
       iModIntro.
       wp_if.
       by iApply "HΦ".
-    - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
-      wp_cas_fail.
+    - wp_cas_fail.
+      { destruct v', v''; simpl; congruence. }
+      { destruct v''; left; done. }
       iMod ("Hclose" with "[Hl Hlist]") as "_".
       { iNext; iExists _, _; by iFrame. }
       iModIntro.
@@ -134,37 +138,36 @@ Section stacks.
     iLöb as "IH".
     wp_lam. wp_bind (Load _).
     iInv N as (â„“ v') "(>% & Hl & Hlist)" "Hclose"; subst.
+    iDestruct (is_list_dup with "Hlist") as "[Hlist Hlist2]".
     wp_load.
-    iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]".
     iMod ("Hclose" with "[Hl Hlist]") as "_".
     { iNext; iExists _, _; by iFrame. }
     iModIntro.
-    iDestruct "Hdisj" as "[-> | Heq]".
+    destruct v' as [l|]; last first.
     - wp_match.
       iApply "HΦ"; by iLeft.
-    - iDestruct "Heq" as (l h t) "[-> Hl]".
-      wp_match. wp_bind (Load _).
+    - wp_match. wp_bind (Load _).
       iInv N as (â„“' v') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
-      iDestruct "Hl" as (q) "Hl".
+      iDestruct "Hlist2" as (???) "Hl".
       wp_load.
       iMod ("Hclose" with "[Hl' Hlist]") as "_".
       { iNext; iExists _, _; by iFrame. }
       iModIntro.
       wp_pures. wp_bind (CAS _ _ _).
       iInv N as (â„“'' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
-      destruct (decide (v'' = InjRV #l)) as [-> |].
+      destruct (decide (v'' = (Some l))) as [-> |].
       * rewrite is_list_unfold.
-        iDestruct "Hlist" as "[>% | H]"; first done.
-        iDestruct "H" as (â„“''' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq.
+        iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
         iDestruct "Hl''" as (q') "Hl''".
+        simpl.
         wp_cas_suc.
-        iDestruct (mapsto_agree with "Hl'' Hl") as "%"; simplify_eq.
+        iDestruct (mapsto_agree with "Hl'' Hl") as %[= <- <-%oloc_to_val_inj].
         iMod ("Hclose" with "[Hl' Hlist]") as "_".
         { iNext; iExists â„“'', _; by iFrame. }
         iModIntro.
         wp_pures.
-        iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame.
-      * wp_cas_fail.
+        iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
+      * wp_cas_fail. { destruct v''; simpl; congruence. }
         iMod ("Hclose" with "[Hl' Hlist]") as "_".
         { iNext; iExists â„“'', _; by iFrame. }
         iModIntro.
diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v
index b9163822..ae45ce80 100644
--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
@@ -246,9 +246,19 @@ Section stack_works.
     iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
   Qed.
 
-  Definition is_list_pre (P : val → iProp Σ) (F : val -d> iProp Σ) :
-     val -d> iProp Σ := λ v,
-    (v ≡ NONEV ∨ ∃ (l : loc) (h t : val), ⌜v ≡ SOMEV #l⌝ ∗ l ↦{-} (h, t)%V ∗ P h ∗ ▷ F t)%I.
+  Definition oloc_to_val (ol: option loc) : val :=
+    match ol with
+    | None => NONEV
+    | Some loc => SOMEV (#loc)
+    end.
+  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
+  Proof. intros [|][|]; simpl; congruence. Qed.
+
+  Definition is_list_pre (P : val → iProp Σ) (F : option loc -d> iProp Σ) :
+     option loc -d> iProp Σ := λ v, match v with
+     | None => True
+     | Some l => ∃ (h : val) (t : option loc), l ↦{-} (h, oloc_to_val t)%V ∗ P h ∗ ▷ F t
+     end%I.
 
   Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P).
   Proof.
@@ -268,27 +278,21 @@ Section stack_works.
     rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
   Qed.
 
-  (* TODO: shouldn't have to explicitly return is_list *)
-  Lemma is_list_unboxed (P : val → iProp Σ) v :
-      is_list P v -∗ ⌜val_is_unboxed v⌝ ∗ is_list P v.
-  Proof.
-    iIntros "Hstack"; iSplit; last done;
-    iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]";
-    last iDestruct "Hstack" as (l h t) "(-> & _)"; done.
-  Qed.
-
-  Lemma is_list_disj (P : val → iProp Σ) v :
-    is_list P v -∗ is_list P v ∗ (⌜v ≡ NONEV⌝ ∨ ∃ (l : loc) h t, ⌜v ≡ SOMEV #l%V⌝ ∗ l ↦{-} (h, t)%V).
+  Lemma is_list_dup (P : val → iProp Σ) v :
+    is_list P v -∗ is_list P v ∗ match v with
+      | None => True
+      | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+      end.
   Proof.
-    iIntros "Hstack".
-    iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq.
-    - rewrite is_list_unfold; iSplitR; [iLeft|]; eauto.
-    - iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)".
-      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq.
-      rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame.
+    iIntros "Hstack". iDestruct (is_list_unfold with "Hstack") as "Hstack".
+    destruct v as [l|].
+    - iDestruct "Hstack" as (h t) "(Hl & Hlist)".
+      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
+      rewrite (is_list_unfold _ (Some _)); iSplitR "Hl2"; iExists _, _; by iFrame.
+    - rewrite is_list_unfold; iSplitR; eauto.
   Qed.
 
-  Definition stack_inv P l := (∃ v, l ↦ v ∗ is_list P v)%I.
+  Definition stack_inv P l := (∃ v, l ↦ oloc_to_val v ∗ is_list P v)%I.
   Definition is_stack P v :=
     (∃ mailbox l, ⌜v = (mailbox, #l)%V⌝ ∗ is_mailbox Nmailbox P mailbox ∗ inv N (stack_inv P l))%I.
 
@@ -302,7 +306,7 @@ Section stack_works.
     wp_apply mk_mailbox_works; first done.
     iIntros (mailbox) "#Hmailbox".
     iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hinv".
-    { by iNext; iExists _; iFrame; rewrite is_list_unfold; iLeft. }
+    { iNext; iExists None; iFrame. rewrite is_list_unfold. done. }
     wp_pures; iModIntro; iApply "Hpost"; iExists _, _; auto.
   Qed.
 
@@ -325,16 +329,16 @@ Section stack_works.
       wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
       iInv N as (list) "(Hl & Hlist)" "Hclose".
       destruct (decide (v'' = list)) as [ -> |].
-      * iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
-        wp_cas_suc.
+      * wp_cas_suc. { destruct list; left; done. }
         iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
-        { iNext; iExists (SOMEV _); iFrame.
-          rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. }
+        { iNext; iExists (Some _); iFrame.
+          rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
         iModIntro.
         wp_if.
         by iApply "HΦ".
-      * iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
-        wp_cas_fail.
+      * wp_cas_fail.
+        { destruct list, v''; simpl; congruence. }
+        { destruct list; left; done. }
         iMod ("Hclose" with "[Hl Hlist]") as "_".
         { iNext; iExists _; by iFrame. }
         iModIntro.
@@ -355,27 +359,25 @@ Section stack_works.
     - wp_match. wp_bind (Load _).
       iInv N as (list) "[Hl Hlist]" "Hclose".
       wp_load.
-      iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]".
+      iDestruct (is_list_dup with "Hlist") as "[Hlist Hlist2]".
       iMod ("Hclose" with "[Hl Hlist]") as "_".
       { iNext; iExists _; by iFrame. }
       iModIntro.
-      iDestruct "Hdisj" as "[-> | Heq]".
+      destruct list as [list|]; last first.
       * wp_match.
         iApply "HΦ"; by iLeft.
-      * iDestruct "Heq" as (l' h t) "[-> Hl']".
-        wp_match. wp_bind (Load _).
+      * wp_match. wp_bind (Load _).
         iInv N as (v') "[>Hl Hlist]" "Hclose".
-        iDestruct "Hl'" as (q) "Hl'".
+        iDestruct "Hlist2" as (???) "Hl'".
         wp_load.
         iMod ("Hclose" with "[Hl Hlist]") as "_".
         { iNext; iExists _; by iFrame. }
         iModIntro.
         wp_let. wp_proj. wp_bind (CAS _ _ _). wp_pures.
         iInv N as (v'') "[Hl Hlist]" "Hclose".
-        destruct (decide (v'' = InjRV #l')) as [-> |].
+        destruct (decide (v'' = Some list)) as [-> |].
         + rewrite is_list_unfold.
-          iDestruct "Hlist" as "[>% | H]"; first done.
-          iDestruct "H" as (l'' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq.
+          iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
           iDestruct "Hl''" as (q') "Hl''".
           wp_cas_suc.
           iDestruct (mapsto_agree with "Hl'' Hl'") as "%"; simplify_eq.
@@ -383,8 +385,8 @@ Section stack_works.
           { iNext; iExists _; by iFrame. }
           iModIntro.
           wp_pures.
-          iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame.
-        + wp_cas_fail.
+          iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
+        + wp_cas_fail. { destruct v''; simpl; congruence. }
           iMod ("Hclose" with "[Hl Hlist]") as "_".
           { iNext; iExists _; by iFrame. }
           iModIntro.
diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v
index 33201c1d..4b516184 100644
--- a/theories/concurrent_stacks/concurrent_stack3.v
+++ b/theories/concurrent_stacks/concurrent_stack3.v
@@ -44,47 +44,51 @@ Section stack_works.
     iApply (mapsto_agree with "H1 H2").
   Qed.
 
+  Definition oloc_to_val (ol: option loc) : val :=
+    match ol with
+    | None => NONEV
+    | Some loc => SOMEV (#loc)
+    end.
+  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
+  Proof. intros [|][|]; simpl; congruence. Qed.
+
   Fixpoint is_list xs v : iProp Σ :=
-    (match xs with
-     | [] => ⌜v = NONEV⌝
-     | x :: xs => ∃ l (t : val), ⌜v = SOMEV #l%V⌝ ∗ l ↦{-} (x, t)%V ∗ is_list xs t
+    (match xs, v with
+     | [], None => True
+     | x :: xs, Some l => ∃ t, l ↦{-} (x, oloc_to_val t)%V ∗ is_list xs t
+     | _, _ => False
      end)%I.
 
-  Lemma is_list_disj xs v :
-    is_list xs v -∗ is_list xs v ∗ (⌜v = NONEV⌝ ∨ ∃ l (h t : val), ⌜v = SOMEV #l⌝ ∗ l ↦{-} (h, t)%V).
+  Lemma is_list_dup xs v :
+    is_list xs v -∗ is_list xs v ∗ match v with
+      | None => True
+      | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+      end.
   Proof.
-    destruct xs; auto.
-    iIntros "H"; iDestruct "H" as (l t) "(-> & Hl & Hstack)".
+    destruct xs, v; simpl; auto; first by iIntros "[]".
+    iIntros "H"; iDestruct "H" as (t) "(Hl & Hstack)".
     iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
-    iSplitR "Hl2"; first by (iExists _, _; iFrame). iRight; auto.
-  Qed.
-
-  Lemma is_list_unboxed xs v :
-      is_list xs v -∗ ⌜val_is_unboxed v⌝ ∗ is_list xs v.
-  Proof.
-    iIntros "Hlist"; iDestruct (is_list_disj with "Hlist") as "[$ Heq]".
-    iDestruct "Heq" as "[-> | H]"; first done; by iDestruct "H" as (? ? ?) "[-> ?]".
+    iSplitR "Hl2"; first by (iExists _; iFrame). by iExists _, _.
   Qed.
 
   Lemma is_list_empty xs :
-    is_list xs (InjLV #()) -∗ ⌜xs = []⌝.
+    is_list xs None -∗ ⌜xs = []⌝.
   Proof.
     destruct xs; iIntros "Hstack"; auto.
-    iDestruct "Hstack" as (? ?) "(% & H)"; discriminate.
   Qed.
 
   Lemma is_list_cons xs l h t :
     l ↦{-} (h, t)%V -∗
-    is_list xs (InjRV #l) -∗
+    is_list xs (Some l) -∗
     ∃ ys, ⌜xs = h :: ys⌝.
   Proof.
     destruct xs; first by iIntros "? %".
-    iIntros "Hl Hstack"; iDestruct "Hstack" as (l' t') "(% & Hl' & Hrest)"; simplify_eq.
+    iIntros "Hl Hstack"; iDestruct "Hstack" as (t') "(Hl' & Hrest)".
     iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
   Qed.
 
   Definition stack_inv P l :=
-    (∃ v xs, l ↦ v ∗ is_list xs v ∗ P xs)%I.
+    (∃ v xs, l ↦ oloc_to_val v ∗ is_list xs v ∗ P xs)%I.
 
   Definition is_stack_pred P v :=
     (∃ l, ⌜v = #l⌝ ∗ inv N (stack_inv P l))%I.
@@ -96,7 +100,7 @@ Section stack_works.
     rewrite -wp_fupd.
     wp_lam. wp_alloc l as "Hl".
     iMod (inv_alloc N _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
-    { by iNext; iExists _, []; iFrame. }
+    { iNext; iExists None, []; iFrame. }
     iModIntro; iApply "HΦ"; iExists _; auto.
   Qed.
 
@@ -116,16 +120,17 @@ Section stack_works.
     iModIntro.
     wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
     iInv N as (list' xs) "(Hl & Hlist & HP)" "Hclose".
-    iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
     destruct (decide (list = list')) as [ -> |].
-    - wp_cas_suc.
+    - wp_cas_suc. { destruct list'; left; done. }
       iMod ("Hupd" with "HP") as "[HP HΨ]".
       iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
-      { iNext; iExists (SOMEV _), (v :: xs); iFrame; iExists _, _; iFrame; auto. }
+      { iNext; iExists (Some _), (v :: xs); iFrame; iExists _; iFrame; auto. }
       iModIntro.
       wp_if.
       by iApply ("HΦ" with "HΨ").
     - wp_cas_fail.
+      { destruct list, list'; simpl; congruence. }
+      { destruct list'; left; done. }
       iMod ("Hclose" with "[Hl HP Hlist]").
       { iExists _, _; iFrame. }
       iModIntro.
@@ -146,8 +151,8 @@ Section stack_works.
     wp_lam. wp_bind (Load _).
     iInv N as (v xs) "(Hl & Hlist & HP)" "Hclose".
     wp_load.
-    iDestruct (is_list_disj with "Hlist") as "[Hlist H]".
-    iDestruct "H" as "[-> | HSome]".
+    iDestruct (is_list_dup with "Hlist") as "[Hlist H]".
+    destruct v as [l'|]; last first.
     - iDestruct (is_list_empty with "Hlist") as %->.
       iDestruct "Hupd" as "[_ Hupdnil]".
       iMod ("Hupdnil" with "HP") as "[HP HΨ]".
@@ -156,7 +161,7 @@ Section stack_works.
       iModIntro.
       wp_match.
       iApply ("HΦ" with "HΨ").
-    - iDestruct "HSome" as (l' h t) "[-> Hl']".
+    - iDestruct "H" as (h t) "Hl'".
       iMod ("Hclose" with "[Hlist Hl HP]") as "_".
       { iNext; iExists _, _; iFrame. }
       iModIntro.
@@ -169,13 +174,13 @@ Section stack_works.
       iModIntro.
       wp_let. wp_proj. wp_bind (CAS _ _ _). wp_pures.
       iInv N as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
-      destruct (decide (v' = (SOMEV #l'))) as [ -> |].
+      destruct (decide (v' = (Some l'))) as [ -> |].
       * wp_cas_suc.
         iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
         simplify_eq.
         iDestruct "Hupd" as "[Hupdcons _]".
         iMod ("Hupdcons" with "HP") as "[HP HΨ]".
-        iDestruct "Hlist" as (l'' t') "(% & Hl'' & Hlist)"; simplify_eq.
+        iDestruct "Hlist" as (t') "(Hl'' & Hlist)".
         iDestruct "Hl''" as (q') "Hl''".
         iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq.
         iMod ("Hclose" with "[Hlist Hl HP]") as "_".
@@ -183,7 +188,7 @@ Section stack_works.
         iModIntro.
         wp_pures.
         iApply ("HΦ" with "HΨ").
-      * wp_cas_fail.
+      * wp_cas_fail. { destruct v'; simpl; congruence. }
         iMod ("Hclose" with "[Hlist Hl HP]") as "_".
         { iNext; iExists _, _; iFrame. }
         iModIntro.
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index 3265ef23..e406b588 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -267,47 +267,51 @@ Section proofs.
     iApply (mapsto_agree with "H1 H2").
   Qed.
 
+  Definition oloc_to_val (ol: option loc) : val :=
+    match ol with
+    | None => NONEV
+    | Some loc => SOMEV (#loc)
+    end.
+  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
+  Proof. intros [|][|]; simpl; congruence. Qed.
+
   Fixpoint is_list xs v : iProp Σ :=
-    (match xs with
-     | [] => ⌜v = NONEV⌝
-     | x :: xs => ∃ l (t : val), ⌜v = SOMEV #l%V⌝ ∗ l ↦{-} (x, t)%V ∗ is_list xs t
+    (match xs, v with
+     | [], None => True
+     | x :: xs, Some l => ∃ t, l ↦{-} (x, oloc_to_val t)%V ∗ is_list xs t
+     | _, _ => False
      end)%I.
 
-  Lemma is_list_disj xs v :
-    is_list xs v -∗ is_list xs v ∗ (⌜v = NONEV⌝ ∨ ∃ l (h t : val), ⌜v = SOMEV #l⌝ ∗ l ↦{-} (h, t)%V).
+  Lemma is_list_dup xs v :
+    is_list xs v -∗ is_list xs v ∗ match v with
+      | None => True
+      | Some l => ∃ h t, l ↦{-} (h, oloc_to_val t)%V
+      end.
   Proof.
-    destruct xs; auto.
-    iIntros "H"; iDestruct "H" as (l t) "(-> & Hl & Hstack)".
+    destruct xs, v; simpl; auto; first by iIntros "[]".
+    iIntros "H"; iDestruct "H" as (t) "(Hl & Hstack)".
     iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
-    iSplitR "Hl2"; first by (iExists _, _; iFrame). iRight; auto.
-  Qed.
-
-  Lemma is_list_unboxed xs v :
-      is_list xs v -∗ ⌜val_is_unboxed v⌝ ∗ is_list xs v.
-  Proof.
-    iIntros "Hlist"; iDestruct (is_list_disj with "Hlist") as "[$ Heq]".
-    iDestruct "Heq" as "[-> | H]"; first done; by iDestruct "H" as (? ? ?) "[-> ?]".
+    iSplitR "Hl2"; first by (iExists _; iFrame). by iExists _, _.
   Qed.
 
   Lemma is_list_empty xs :
-    is_list xs (InjLV #()) -∗ ⌜xs = []⌝.
+    is_list xs None -∗ ⌜xs = []⌝.
   Proof.
     destruct xs; iIntros "Hstack"; auto.
-    iDestruct "Hstack" as (? ?) "(% & H)"; discriminate.
   Qed.
 
   Lemma is_list_cons xs l h t :
     l ↦{-} (h, t)%V -∗
-    is_list xs (InjRV #l) -∗
+    is_list xs (Some l) -∗
     ∃ ys, ⌜xs = h :: ys⌝.
   Proof.
     destruct xs; first by iIntros "? %".
-    iIntros "Hl Hstack"; iDestruct "Hstack" as (l' t') "(% & Hl' & Hrest)"; simplify_eq.
+    iIntros "Hl Hstack"; iDestruct "Hstack" as (t') "(Hl' & Hrest)".
     iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
   Qed.
 
   Definition stack_inv P l :=
-    (∃ v xs, l ↦ v ∗ is_list xs v ∗ P xs)%I.
+    (∃ v xs, l ↦ oloc_to_val v ∗ is_list xs v ∗ P xs)%I.
 
   Definition is_stack_pred P v :=
     (∃ mailbox l, ⌜v = (mailbox, #l)%V⌝ ∗ is_mailbox P mailbox ∗ inv Nstack (stack_inv P l))%I.
@@ -321,7 +325,7 @@ Section proofs.
     wp_alloc l as "Hl".
     wp_apply mk_mailbox_works ; first done. iIntros (v) "#Hmailbox".
     iMod (inv_alloc Nstack _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
-    { by iNext; iExists _, []; iFrame. }
+    { by iNext; iExists None, []; iFrame. }
     wp_pures. iModIntro; iApply "HΦ"; iExists _; auto.
   Qed.
 
@@ -348,18 +352,19 @@ Section proofs.
       iModIntro.
       wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
       iInv Nstack as (list' xs) "(Hl & Hlist & HP)" "Hclose".
-      iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
       destruct (decide (list = list')) as [ -> |].
-      * wp_cas_suc.
+      * wp_cas_suc. { destruct list'; left; done. }
         iMod (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
         iMod ("Hupd" with "HP") as "[HP HΨ]".
         iMod "Hupd'" as "_".
         iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
-        { iNext; iExists (SOMEV _), (v' :: xs); iFrame; iExists _, _; iFrame; auto. }
+        { iNext; iExists (Some _), (v' :: xs); iFrame; iExists _; iFrame; auto. }
         iModIntro.
         wp_if.
         by iApply ("HΦ" with "HΨ").
       * wp_cas_fail.
+      { destruct list, list'; simpl; congruence. }
+      { destruct list'; left; done. }
         iMod ("Hclose" with "[Hl HP Hlist]").
         { iExists _, _; iFrame. }
         iModIntro.
@@ -399,8 +404,8 @@ Section proofs.
     - wp_match. wp_bind (Load _).
       iInv Nstack as (v xs) "(Hl & Hlist & HP)" "Hclose".
       wp_load.
-      iDestruct (is_list_disj with "Hlist") as "[Hlist H]".
-      iDestruct "H" as "[-> | HSome]".
+      iDestruct (is_list_dup with "Hlist") as "[Hlist H]".
+    destruct v as [l'|]; last first.
       * iDestruct (is_list_empty with "Hlist") as %->.
         iMod (fupd_intro_mask' (⊤ ∖ ↑Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
         iMod ("Hupd" with "HP") as "[HP HΨ]".
@@ -410,7 +415,7 @@ Section proofs.
         iModIntro.
         wp_match.
         iApply ("HΦ" with "HΨ").
-      * iDestruct "HSome" as (l' h t) "[-> Hl']".
+      * iDestruct "H" as (h t) "Hl'".
         iMod ("Hclose" with "[Hlist Hl HP]") as "_".
         { iNext; iExists _, _; iFrame. }
         iModIntro.
@@ -423,7 +428,7 @@ Section proofs.
         iModIntro.
         wp_pures. wp_bind (CAS _ _ _).
         iInv Nstack as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
-        destruct (decide (v' = (SOMEV #l'))) as [ -> |].
+        destruct (decide (v' = (Some l'))) as [ -> |].
         + wp_cas_suc.
           iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
           simplify_eq.
@@ -431,7 +436,7 @@ Section proofs.
           iDestruct "Hupd" as "[Hupdcons _]".
           iMod ("Hupdcons" with "HP") as "[HP HΨ]".
           iMod "Hupd'" as "_".
-          iDestruct "Hlist" as (l'' t') "(% & Hl'' & Hlist)"; simplify_eq.
+          iDestruct "Hlist" as (t') "(Hl'' & Hlist)".
           iDestruct "Hl''" as (q') "Hl''".
           iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq.
           iMod ("Hclose" with "[Hlist Hl HP]") as "_".
@@ -439,7 +444,7 @@ Section proofs.
           iModIntro.
           wp_pures.
           iApply ("HΦ" with "HΨ").
-        + wp_cas_fail.
+        + wp_cas_fail. { destruct v'; simpl; congruence. }
           iMod ("Hclose" with "[Hlist Hl HP]") as "_".
           { iNext; iExists _, _; iFrame. }
           iModIntro.
diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v
index 916c489f..b8c8c532 100644
--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -49,49 +49,51 @@ Section proof.
   Lemma rown_duplicate l v : rown l v -∗ rown l v ∗ rown l v.
   Proof. iDestruct 1 as (q) "[Hl Hl']". iSplitL "Hl"; iExists _; eauto. Qed.
 
-  Fixpoint is_list (hd : val) (xs : list val) : iProp Σ :=
-    match xs with
-    | [] => ⌜hd = NONEV⌝%I
-    | x::xs => (∃ (l : loc) (tl : val),
-                   ⌜hd = SOMEV #l⌝ ∗ rown l (x, tl) ∗ is_list tl xs)%I
+  Definition oloc_to_val (ol: option loc) : val :=
+    match ol with
+    | None => NONEV
+    | Some loc => SOMEV (#loc)
     end.
+  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
+  Proof. intros [|][|]; simpl; congruence. Qed.
 
-  Lemma is_list_unboxed hd xs :
-    is_list hd xs -∗ ⌜val_is_unboxed hd⌝.
-  Proof.
-    destruct xs.
-    - iIntros (->). done.
-    - iIntros "Hl". iDestruct "Hl" as (?? ->) "_". done.
-  Qed.
+  Fixpoint is_list (hd : option loc) (xs : list val) : iProp Σ :=
+    match xs, hd with
+    | [], None => True
+    | x::xs, Some l => ∃ (tl : option loc),
+                   rown l (x, oloc_to_val tl) ∗ is_list tl xs
+    | _, _ => False
+    end%I.
 
   Lemma is_list_duplicate hd xs : is_list hd xs -∗ is_list hd xs ∗ is_list hd xs.
   Proof.
     iInduction xs as [ | x xs ] "IH" forall (hd); simpl; eauto.
-    iDestruct 1 as (l tl) "[% [Hro Htl]]"; simplify_eq.
+    destruct hd; last by auto.
+    iDestruct 1 as (tl) "[Hro Htl]".
     rewrite rown_duplicate. iDestruct "Hro" as "[Hro Hro']".
     iDestruct ("IH" with "Htl") as "[Htl Htl']".
-    iSplitL "Hro Htl"; iExists _,_; iFrame; eauto.
+    iSplitL "Hro Htl"; iExists _; iFrame; eauto.
   Qed.
 
   Lemma is_list_agree hd xs ys : is_list hd xs -∗ is_list hd ys -∗ ⌜xs = ys⌝.
   Proof.
     iInduction xs as [ | x xs ] "IH" forall (hd ys); simpl; eauto.
-    - iIntros "%"; subst.
-      destruct ys; eauto. simpl.
-      iDestruct 1 as (? ?) "[% ?]". simplify_eq.
-    - iDestruct 1 as (l tl) "(% & Hro & Hls)"; simplify_eq.
+    - destruct hd; first by auto.
+      destruct ys; eauto.
+    - destruct hd; last by auto.
       destruct ys as [| y ys]; eauto. simpl.
-      iDestruct 1 as (l' tl') "(% & Hro' & Hls')"; simplify_eq.
+      iDestruct 1 as (tl) "(Hro & Hls)".
+      iDestruct 1 as (tl') "(Hro' & Hls')".
       iDestruct "Hro" as (q) "Hro".
       iDestruct "Hro'" as (q') "Hro'".
-      iDestruct (mapsto_agree l' q q' (PairV x tl) (PairV y tl')
+      iDestruct (mapsto_agree l q q' (PairV x (oloc_to_val tl)) (PairV y (oloc_to_val tl'))
                 with "Hro Hro'") as %?. simplify_eq/=.
       iDestruct ("IH" with "Hls Hls'") as %->. done.
   Qed.
 
   Definition bag_inv (γb : gname) (b : loc) : iProp Σ :=
-    (∃ (hd : val) (ls : list val),
-        b ↦ hd ∗ is_list hd ls ∗ own γb ((1/2)%Qp, to_agree (list_to_set_disj ls)))%I.
+    (∃ (hd : option loc) (ls : list val),
+        b ↦ oloc_to_val hd ∗ is_list hd ls ∗ own γb ((1/2)%Qp, to_agree (list_to_set_disj ls)))%I.
   Definition is_bag (γb : gname) (x : val) :=
     (∃ (b : loc), ⌜x = #b⌝ ∗ inv N (bag_inv γb b))%I.
   Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ :=
@@ -134,7 +136,7 @@ Section proof.
     wp_alloc r as "Hr".
     iMod (own_alloc (1%Qp, to_agree ∅)) as (γb) "[Ha Hf]"; first done.
     iMod (inv_alloc N _ (bag_inv γb r) with "[Ha Hr]") as "#Hinv".
-    { iNext. iExists _,[]. simpl. iFrame. eauto. }
+    { iNext. iExists None,[]. simpl. iFrame. }
     iModIntro. iApply "HΦ".
     rewrite /is_bag /bag_contents. iFrame.
     iExists _. by iFrame "Hinv".
@@ -162,15 +164,16 @@ Section proof.
     wp_alloc n as "Hn".
     wp_pures. wp_bind (CAS _ _ _).
     iInv N as (o' ls) "[Ho [Hls >Hb]]" "Hcl".
-    iPoseProof (is_list_unboxed with "Hls") as "#>%".
     destruct (decide (o = o')) as [->|?].
-    - wp_cas_suc.
+    - wp_cas_suc. { destruct o'; left; done. }
       iMod ("Hvs" with "[$Hb $HP]") as "[Hb HQ]".
       iMod ("Hcl" with "[Ho Hn Hls Hb]") as "_".
-      { iNext. iExists _,(v::ls). iFrame "Ho Hb".
-        simpl. iExists _,_. iFrame. iSplit; eauto. by iExists 1%Qp. }
+      { iNext. iExists (Some _),(v::ls). iFrame "Ho Hb".
+        simpl. iExists _. iFrame. by iExists 1%Qp. }
       iModIntro. wp_if_true. by iApply "HΦ".
     - wp_cas_fail.
+      { destruct o, o'; simpl; congruence. }
+      { destruct o'; left; done. }
       iMod ("Hcl" with "[Ho Hls Hb]") as "_".
       { iNext. iExists _,ls. by iFrame "Ho Hb". }
       iModIntro. wp_if_false.
@@ -196,38 +199,38 @@ Section proof.
     iInv N as (o ls) "[Ho [Hls >Hb]]" "Hcl".
     wp_load.
     destruct ls as [|x ls]; simpl.
-    - iDestruct "Hls" as %->.
+    - destruct o; first done.
       iMod ("Hvs2" with "[$Hb $HP]") as "[Hb HQ]".
       iMod ("Hcl" with "[Ho Hb]") as "_".
       { iNext. iExists _,[]. by iFrame. }
       iModIntro. repeat wp_pure _.
       by iApply "HΦ".
-    - iDestruct "Hls" as (hd tl) "(% & Hhd & Hls)"; simplify_eq/=.
+    - destruct o as [hd|]; last done.
+      iDestruct "Hls" as (tl) "(Hhd & Hls)"; simplify_eq/=.
       rewrite rown_duplicate. iDestruct "Hhd" as "[Hhd Hhd']".
       rewrite is_list_duplicate. iDestruct "Hls" as "[Hls Hls']".
       iMod ("Hcl" with "[Ho Hb Hhd Hls]") as "_".
-      { iNext. iExists _,(x::ls). simpl; iFrame; eauto.
-        iExists _, _; eauto. by iFrame. }
+      { iNext. iExists (Some _),(x::ls). simpl; iFrame; eauto.
+        iExists _; eauto. by iFrame. }
       iModIntro. repeat wp_pure _.
       iDestruct "Hhd'" as (q) "Hhd".
       wp_load. repeat wp_pure _.
       wp_bind (CAS _ _ _).
       iInv N as (o' ls') "[Ho [Hls >Hb]]" "Hcl".
-      destruct (decide (o' = (InjRV #hd))) as [->|?].
+      destruct (decide (o' = (Some hd))) as [->|?].
       + wp_cas_suc.
         (* The list is still the same *)
         rewrite (is_list_duplicate tl). iDestruct "Hls'" as "[Hls' Htl]".
-        iAssert (is_list (InjRV #hd) (x::ls)) with "[Hhd Hls']" as "Hls'".
-        { simpl. iExists hd,tl. iFrame; iSplit; eauto.
-          iExists q. iFrame. }
+        iAssert (is_list (Some hd) (x::ls)) with "[Hhd Hls']" as "Hls'".
+        { simpl. iExists tl. iFrame. iExists q. iFrame. }
         iDestruct (is_list_agree with "Hls Hls'") as %?. simplify_eq.
         iClear "Hls'".
-        iDestruct "Hls" as (hd' tl') "(% & Hro' & Htl')". simplify_eq.
+        iDestruct "Hls" as (tl') "(Hro' & Htl')".
         iMod ("Hvs1" with "[$Hb $HP]") as "[Hb HQ]".
         iMod ("Hcl" with "[Ho Htl Hb]") as "_".
         { iNext. iExists _,ls. by iFrame "Ho Hb". }
         iModIntro. wp_pures. by iApply "HΦ".
-      + wp_cas_fail.
+      + wp_cas_fail. { destruct o'; simpl; congruence. }
         iMod ("Hcl" with "[Ho Hls Hb]") as "_".
         { iNext. iExists _,ls'. by iFrame "Ho Hb". }
         iModIntro. wp_if_false.
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index 7b7aec1a..5b824184 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -106,6 +106,10 @@ Section stack.
   Local Instance stack_elem_to_val_inj : Inj (=) (=) stack_elem_to_val.
   Proof. rewrite /Inj /stack_elem_to_val=>??. repeat case_match; congruence. Qed.
 
+  Lemma stack_elem_to_val_for_compare rep :
+    val_for_compare (stack_elem_to_val rep) = stack_elem_to_val rep.
+  Proof. destruct rep; done. Qed.
+
   Fixpoint list_inv (l : list val) (rep : option loc) : iProp :=
     match l with
     | nil => ⌜rep = None⌝
@@ -203,7 +207,7 @@ Section stack.
     awp_apply cas_spec; [by destruct stack_rep|].
     iInv stackN as (stack_rep' offer_rep l) "(>Hs● & >H↦ & Hlist & Hoffer)".
     iAaccIntro with "H↦"; first by eauto 10 with iFrame.
-    iIntros "H↦".
+    iIntros "H↦". rewrite !stack_elem_to_val_for_compare.
     destruct (decide (stack_elem_to_val stack_rep' = stack_elem_to_val stack_rep)) as
       [->%stack_elem_to_val_inj|_].
     - (* The CAS succeeded. Update everything accordingly. *)
@@ -299,6 +303,7 @@ Section stack.
       iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)".
       iAaccIntro with "H↦"; first by eauto 10 with iFrame.
       iIntros "H↦". change (InjRV #tail) with (stack_elem_to_val (Some tail)).
+      rewrite !stack_elem_to_val_for_compare.
       destruct (decide (stack_elem_to_val stack_rep = stack_elem_to_val (Some tail))) as
         [->%stack_elem_to_val_inj|_].
       + (* CAS succeeded! It must still be the same head element in the list,
@@ -308,8 +313,7 @@ Section stack.
           %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
         destruct l as [|v' l]; simpl.
         { (* Contradiction. *) iDestruct "Hlist" as ">%". done. }
-        iDestruct "Hlist" as (tail' q' rep') "[>Heq [>Htail' Hlist]]".
-        iDestruct "Heq" as %[= <-].
+        iDestruct "Hlist" as (tail' q' rep') "[>% [>Htail' Hlist]]". simplify_eq.
         iDestruct (mapsto_agree with "Htail Htail'") as %[= <- <-%stack_elem_to_val_inj].
         iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
         { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
@@ -334,7 +338,7 @@ Section stack.
         iDestruct "Hoff" as (Poff Qoff γo) "[#Hoinv #AUoff]".
         iInv offerN as (offer_st) "[>Hoff↦ Hoff]".
         iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame.
-        iIntros "Hoff↦".
+        iIntros "Hoff↦". simpl.
         destruct (decide (#(offer_state_rep offer_st) = #0)) as [Heq|_]; last first.
         { (* CAS failed, we don't do a thing. *)
           iSplitR "AU"; first by eauto 10 with iFrame.
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index 05ee4dc3..25d1181d 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -266,7 +266,7 @@ Proof.
   (* We now reason by case on the success/failure of the CAS. *)
   destruct (decide (u = w)) as [[= ->]|NE].
   - (* The CAS succeeded. *)
-    wp_cas_suc. { case w; done. (* Administrative stuff. *) }
+    wp_cas_suc. { case w; left; done. (* Administrative stuff. *) }
     (* This was the linearization point. We access the preconditon. *)
     iMod "AU" as (zs) "[Hγ◯ [_ HClose]]".
     (* Use agreement on ressource [γ] to learn [zs = ys]. *)
@@ -280,7 +280,7 @@ Proof.
     (* And conclude the proof easily, after some computation steps. *)
     wp_if. iExact "H".
   - (* The CAS failed. *)
-    wp_cas_fail. { eapply not_inj. done. }
+    wp_cas_fail. { case u, w; simpl; congruence. }
     { case u, w; simpl; eauto. (* Administrative stuff. *) }
     (* We can eliminate the modality. *)
     iModIntro. iSplitL "Hγ● Hl HPhys"; first by eauto 10 with iFrame.
@@ -324,7 +324,7 @@ Proof.
     (* We reason by case on the success/failure of the CAS. *)
     destruct (decide (u = Some w)) as [[= ->]|Hx].
     * (* The CAS succeeded, so this is the linearization point. *)
-      wp_cas_suc; first done.
+      wp_cas_suc.
       (* The list [ys] must be non-empty, otherwise the proof is trivial. *)
       destruct ys; first done.
       (* We access the precondition, prior to performing an update. *)
diff --git a/theories/logrel_heaplang/ltyping.v b/theories/logrel_heaplang/ltyping.v
index 4e35302f..d260fe9f 100644
--- a/theories/logrel_heaplang/ltyping.v
+++ b/theories/logrel_heaplang/ltyping.v
@@ -383,9 +383,6 @@ Section types_properties.
     wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "HA2".
     iDestruct (lty_unboxed with "HA2") as %?.
     wp_apply (wp_wand with "(H1 [//])"); iIntros (w1); iDestruct 1 as (l ->) "#?".
-    iInv (tyN.@l) as (v) "[>Hl Hv]".
-    destruct (decide (v = w2)) as [->|].
-    - wp_cas_suc. eauto 10.
-    - wp_cas_fail. eauto 10.
+    iInv (tyN.@l) as (v) "[>Hl Hv]". wp_cas as ?|?; eauto 10.
   Qed.
 End types_properties.
diff --git a/theories/spanning_tree/spanning.v b/theories/spanning_tree/spanning.v
index 661cc591..98a7f21e 100644
--- a/theories/spanning_tree/spanning.v
+++ b/theories/spanning_tree/spanning.v
@@ -75,7 +75,7 @@ Section Helpers.
     rewrite Hil2' in Hil2; inversion Hil2; subst.
     iDestruct (auth_own_graph_valid with "Hi1") as %Hvl.
     destruct u as [[] uch].
-    - wp_cas_fail; first done.
+    - wp_cas_fail.
       iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3";
       eauto.
       { iFrame. iExists _; eauto. iSplitR; eauto. by iExists _; iFrame. }
@@ -85,7 +85,7 @@ Section Helpers.
       { iNext. unfold graph_inv at 2. iExists _; iFrame; auto. }
       iModIntro. iFrame. iRight; by iFrame.
     - (* CAS succeeds *)
-      wp_cas_suc; first done.
+      wp_cas_suc.
       iMod (mark_graph _ _ x uch with "[Hi1 Hx]") as "[Hi1 Hx]"; try by iFrame.
       { apply (proj1 (not_elem_of_dom (D := gset loc) G' x)).
         intros Hid. eapply in_dom_of_graph in Hid; eauto; tauto. }
-- 
GitLab