From 7ea19a10303d7a8e76ef37b0494b1fe0fadc10b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 24 Jun 2019 15:47:11 +0200
Subject: [PATCH] bump Iris (for CmpXchg change)

---
 opam                                    |  2 +-
 theories/examples/coinflip.v            |  9 ++--
 theories/examples/stack/refinement.v    | 23 +++++----
 theories/examples/various.v             |  6 +--
 theories/lib/counter.v                  | 10 ++--
 theories/lib/lock.v                     | 10 ++--
 theories/logic/proofmode/spec_tactics.v | 62 ++++++++++++-------------
 theories/logic/proofmode/tactics.v      | 60 ++++++++++++------------
 theories/logic/rules.v                  | 44 +++++++++---------
 theories/logic/spec_rules.v             | 28 +++++------
 theories/prelude/ctx_subst.v            |  6 +--
 theories/tests/tp_tests.v               |  5 +-
 theories/typing/contextual_refinement.v | 26 +++++------
 theories/typing/fundamental.v           | 18 +++----
 theories/typing/types.v                 |  4 +-
 15 files changed, 158 insertions(+), 155 deletions(-)

diff --git a/opam b/opam
index a7cee3d..18a6991 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2019-06-18.8.72595700") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-24.3.5ef58527") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 5a42d2f..6f9f11e 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -213,7 +213,7 @@ Section proofs.
         iNext. iIntros (vs' ->) "Hp". repeat rel_pure_l.
         repeat rel_pure_r.
         rel_apply_r (refines_rand_r b). repeat rel_pure_r.
-        rel_cas_suc_r. repeat rel_pure_r.
+        rel_cmpxchg_suc_r. repeat rel_pure_r.
         rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
         { iExists vs'. iFrame. iRight. iExists b. iFrame. }
         iNext. repeat rel_pure_l; rel_values.
@@ -273,11 +273,11 @@ Section proofs.
         { eauto with iFrame. }
         rel_apply_l refines_rand_l. iNext. iIntros (b).
         repeat rel_pure_l.
-        rel_cas_l_atomic. iInv coinN as "(Hlk & [[Hc' Hc]|H])" "Hclose".
+        rel_cmpxchg_l_atomic. iInv coinN as "(Hlk & [[Hc' Hc]|H])" "Hclose".
         * iModIntro; iExists _. iFrame. iSplit.
           { iIntros (?); simplify_eq/=. }
           iIntros (_). iNext. iIntros "Hc".
-          rel_pure_l. rel_apply_r (refines_acquire_r with "Hlk").
+          rel_pures_l. rel_apply_r (refines_acquire_r with "Hlk").
           iIntros "Hlk". repeat rel_pure_r. rel_load_r.
           repeat rel_pure_r. rel_apply_r (refines_rand_r b).
           repeat rel_pure_r. rel_store_r.
@@ -291,7 +291,7 @@ Section proofs.
           iModIntro; iExists _. iFrame. iSplit; last first.
           { iIntros (?); simplify_eq/=. }
           iIntros (_). iNext. iIntros "Hc".
-          rel_pure_l. rel_rec_l. do 2 rel_pure_l.
+          rel_pures_l. rel_rec_l. do 2 rel_pure_l.
           iMod ("Hclose" with "[-]") as "_".
           { eauto with iFrame. }
           iApply "IH".
@@ -351,4 +351,3 @@ Proof.
   - eapply (refines_sound #[relocΣ; lockΣ]).
     iIntros (? Δ). iApply coin_lazy'_lazy_refinement.
 Qed.
-
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index f508754..c731587 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -98,17 +98,17 @@ Section proof.
     close_sinv "Hclose" "[Hst Hst' Hl HLK]". clear w.
     repeat rel_pure_l.
     rel_alloc_l nstk as "Hnstk".
-    rel_cas_l_atomic.
+    rel_cmpxchg_l_atomic.
     iInv N as (istk' w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
     iExists _. iFrame "Hst".
     iModIntro. iSplit.
-    - (* CAS fails *)
+    - (* CmpXchg fails *)
       iIntros (?); iNext; iIntros "Hst".
       close_sinv "Hclose" "[Hst Hst' Hl HLK]". clear w.
-      rel_if_false_l. simpl.
+      rel_pures_l. simpl.
       rel_rec_l.
       by iApply "IH".
-    - (* CAS succeeds *)
+    - (* CmpXchg succeeds *)
       iIntros (?). simplify_eq/=. iNext. iIntros "Hst".
       rel_apply_r (refines_CG_push_r with "Hst' Hl").
       iIntros "Hst' Hl".
@@ -119,7 +119,7 @@ Section proof.
         iExists _. iSplitL "Hnstk".
         - iExists 1%Qp; iFrame.
         - iRight. iExists _,_,_,_. eauto. }
-      rel_if_true_l.
+      rel_pures_l.
       rel_values.
   Qed.
 
@@ -157,18 +157,18 @@ Section proof.
       close_sinv "Hclose" "[Hst' Hst Hl HLK2]".
       iDestruct "Histk" as (q) "Histk".
       rel_load_l. repeat rel_pure_l.
-      rel_cas_l_atomic.
+      rel_cmpxchg_l_atomic.
       iInv N as (istk' w) "(>Hst' & >Hl & >Hst & HLK)" "Hclose".
       iExists _. iFrame "Hst".
       iModIntro. iSplit.
-      + (* CAS fails *) iIntros (?); simplify_eq/=.
+      + (* CmpXchg fails *) iIntros (?); simplify_eq/=.
         iNext. iIntros "Hst".
-        rel_if_l.
+        rel_pures_l.
         close_sinv "Hclose" "[Hst Hst' Hl HLK]".
         iApply "IH".
-      + (* CAS succeeds *) iIntros (?); simplify_eq/=.
+      + (* CmpXchg succeeds *) iIntros (?); simplify_eq/=.
         iNext. iIntros "Hst".
-        rel_if_l.
+        rel_pures_l.
         rewrite (stack_link_unfold _ istk).
         iDestruct "HLK" as (w') "(Histk2 & HLK)".
         iAssert (⌜w' = InjRV (y1, #z1)⌝)%I with "[Histk Histk2]" as %->.
@@ -179,7 +179,7 @@ Section proof.
         rel_apply_r (refines_CG_pop_suc_r with "Hst' Hl").
         iIntros "Hst' Hl".
         close_sinv "Hclose" "[-]".
-        rel_pure_l.
+        rel_pures_l.
         rel_values. iModIntro. iExists _,_; eauto.
   Qed.
 
@@ -238,4 +238,3 @@ Proof.
   iIntros (? ?).
   iApply stack_refinement.
 Qed.
-
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 91f5495..09477ad 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -199,20 +199,20 @@ Section proofs.
       iApply refines_arrow.
       iAlways. iIntros (f f') "Hf".
       rel_let_l. rel_let_r.
-      rel_cas_l_atomic.
+      rel_cmpxchg_l_atomic.
       iInv i3n as (n) "(Hx & Hx' & >Hbb)" "Hcl".
       iDestruct "Hbb" as "[(Hb & Hb' & Hx1 & Hx'1) | (Hb & Hb')]"; last first.
       { iModIntro; iExists _; iFrame. simpl.
         iSplitL; last by iIntros (?); congruence.
         iIntros (?); iNext; iIntros "Hb".
-        rel_cas_fail_r; rel_if_r; rel_if_l.
+        rel_cmpxchg_fail_r; rel_pures_r; rel_pures_l.
         iMod ("Hcl" with "[-]").
         { iNext. iExists n. iFrame. iRight. iFrame. }
         rel_values. }
       { iModIntro. iExists _; iFrame. simpl.
         iSplitR; first by iIntros (?); congruence.
         iIntros (?); iNext; iIntros "Hb".
-        rel_cas_suc_r; rel_if_r; rel_if_l.
+        rel_cmpxchg_suc_r; rel_pures_r; rel_pures_l.
         rel_load_r. repeat rel_pure_r.
         iMod ("Hcl" with "[Hb Hb' Hx Hx']") as "_".
         { iNext. iExists _; iFrame. iRight. iFrame. }
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index 703a0f4..749cf87 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -74,8 +74,8 @@ Section CG_Counter.
     iIntros (?) "Hx Hlog".
     rel_rec_r. repeat rel_pure_r.
     rel_load_r. repeat rel_pure_r.
-    rel_cas_suc_r.
-    rel_if_r.
+    rel_cmpxchg_suc_r.
+    rel_pures_r.
     replace (n + 1)%Z with (1 + n)%Z; last lia.
     by iApply "Hlog".
   Qed.
@@ -99,7 +99,7 @@ Section CG_Counter.
     iExists #n. iFrame. iNext. iIntros "Hx".
     iDestruct "Hrev" as "[Hrev _]".
     iMod ("Hrev" with "[HR Hx]") as "_"; first iFrame.
-    repeat rel_pure_l. rel_cas_l_atomic.
+    repeat rel_pure_l. rel_cmpxchg_l_atomic.
     iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
     destruct (decide (n = n')); subst.
     - iExists #n'. iFrame. simpl.
@@ -108,12 +108,12 @@ Section CG_Counter.
       iDestruct "HQ" as "[_ HQ]".
       replace (n' + 1)%Z with (1 + n')%Z; last by lia. (* TODO :( *)
       iSpecialize ("HQ" with "[$Hx $HR]").
-      rel_if_true_l. by iApply "HQ".
+      rel_pures_l. by iApply "HQ".
     - iExists #n'. iFrame. simpl.
       iSplitL; eauto; last first.
       { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
       iIntros "_ !> Hx". simpl.
-      rel_if_false_l.
+      rel_pures_l.
       iDestruct "HQ" as "[HQ _]".
       iMod ("HQ" with "[$Hx $HR]").
       by iApply "IH".
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index e4b1a42..a246d56 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -87,18 +87,18 @@ Section lockG_rules.
     iLöb as "IH".
     rel_rec_l.
     iDestruct "Hlock" as (l) "[% #?]". simplify_eq.
-    rel_cas_l_atomic.
+    rel_cmpxchg_l_atomic.
     iInv N as (b) "[Hl HR]" "Hclose".
     iModIntro. iExists _. iFrame. simpl.
     iSplit.
     - iIntros (?). iNext. iIntros "Hl".
       assert (b = true) as ->. { destruct b; congruence. }
-      rel_if_l.
+      rel_pures_l.
       iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
       by iApply "IH".
     - iIntros (?). simplify_eq.
       iNext. iIntros "Hl".
-      rel_if_l.
+      rel_pures_l.
       iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
       iDestruct "HR" as "[Hlocked HR]".
       iApply ("Hlog" with "Hlocked HR").
@@ -134,8 +134,8 @@ Section lock_rules_r.
     iIntros "Hl Hlog".
     iDestruct "Hl" as (lk ->) "Hl".
     rel_rec_r.
-    rel_cas_suc_r.
-    rel_if_r.
+    rel_cmpxchg_suc_r.
+    rel_pures_r.
     iApply "Hlog". iExists _. by iFrame.
   Qed.
 
diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 1511b7e..4f08c98 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -249,22 +249,22 @@ Tactic Notation "tp_load" constr(j) :=
     |pm_reflexivity || fail "tp_load: this should not happen"
     |(* new goal *)]).
 
-Lemma tac_tp_cas_fail `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc) e1 e2 v' v1 v2 Q q :
+Lemma tac_tp_cmpxchg_fail `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc) e1 e2 v' v1 v2 Q q :
   nclose specN ⊆ E1 →
   envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
   envs_lookup_delete false i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
-  e = fill K' (CAS #l e1 e2) →
+  e = fill K' (CmpXchg #l e1 e2) →
   IntoVal e1 v1 →
   IntoVal e2 v2 →
   envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v')%I →
   val_for_compare v' ≠ val_for_compare v1 →
-  vals_cas_compare_safe v' v1 →
+  vals_cmpxchg_compare_safe v' v1 →
   envs_simple_replace i3 false
-    (Esnoc (Esnoc Enil i2 (j ⤇ fill K' #false)) i3 (l ↦ₛ{q} v')%I) Δ2 = Some Δ3 →
+    (Esnoc (Esnoc Enil i2 (j ⤇ fill K' (v', #false)%V)) i3 (l ↦ₛ{q} v')%I) Δ2 = Some Δ3 →
   envs_entails Δ3 (|={E1,E2}=> Q) →
   envs_entails Δ1 (|={E1,E2}=> Q).
 Proof.
-  rewrite envs_entails_eq. intros ??? Hfill <-<-? Hcas ?? HQ.
+  rewrite envs_entails_eq. intros ??? Hfill <-<-? Hcmpxchg ?? HQ.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' Δ1 false). 2: eassumption.
   rewrite bi.sep_elim_l.
@@ -282,45 +282,45 @@ Proof.
   (* (S (S (spec_ctx ρ) (j => fill _ _)) (S (l ↦ v) ..)) *)
   rewrite assoc.
   rewrite -(assoc _ (spec_ctx ρ) (j ⤇ fill K' _)%I).
-  rewrite step_cas_fail //.
+  rewrite step_cmpxchg_fail //.
   rewrite -(fupd_trans E1 E1 E2).
   rewrite fupd_frame_r.
   apply fupd_mono.
   by rewrite (comm _ (j ⤇ _)%I) /= right_id bi.wand_elim_r.
 Qed.
 
-Tactic Notation "tp_cas_fail" constr(j) :=
+Tactic Notation "tp_cmpxchg_fail" constr(j) :=
   iStartProof;
   with_spec_ctx ltac:(fun _ =>
-  eapply (tac_tp_cas_fail j);
-    [solve_ndisj || fail "tp_cas_fail: cannot prove 'nclose specN ⊆ ?'"
-    |iAssumptionCore || fail "tp_cas_fail: cannot find spec_ctx" (* spec_ctx *)
-    |iAssumptionCore || fail "tp_cas_fail: cannot find '" j " ⤇ ?'"
-    |tp_bind_helper (* e = K'[CAS _ _ _] *)
+  eapply (tac_tp_cmpxchg_fail j);
+    [solve_ndisj || fail "tp_cmpxchg_fail: cannot prove 'nclose specN ⊆ ?'"
+    |iAssumptionCore || fail "tp_cmpxchg_fail: cannot find spec_ctx" (* spec_ctx *)
+    |iAssumptionCore || fail "tp_cmpxchg_fail: cannot find '" j " ⤇ ?'"
+    |tp_bind_helper (* e = K'[CmpXchg _ _ _] *)
     |iSolveTC
     |iSolveTC
-    |iAssumptionCore || fail "tp_cas_fail: cannot find '? ↦ ?'"
+    |iAssumptionCore || fail "tp_cmpxchg_fail: cannot find '? ↦ ?'"
     |try (simpl; congruence) (* v' ≠ v1 *)
-    |try heap_lang.proofmode.solve_vals_cas_compare_safe
-    |pm_reflexivity || fail "tp_cas_fail: this should not happen"
+    |try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
+    |pm_reflexivity || fail "tp_cmpxchg_fail: this should not happen"
     |(* new goal *)]).
 
-Lemma tac_tp_cas_suc `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc) e1 e2 v' v1 v2 Q :
+Lemma tac_tp_cmpxchg_suc `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc) e1 e2 v' v1 v2 Q :
   nclose specN ⊆ E1 →
   envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
   envs_lookup_delete false i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
-  e = fill K' (CAS #l e1 e2) →
+  e = fill K' (CmpXchg #l e1 e2) →
   IntoVal e1 v1 →
   IntoVal e2 v2 →
   envs_lookup i3 Δ2 = Some (false, l ↦ₛ v')%I →
   val_for_compare v' = val_for_compare v1 →
-  vals_cas_compare_safe v' v1 →
+  vals_cmpxchg_compare_safe v' v1 →
   envs_simple_replace i3 false
-    (Esnoc (Esnoc Enil i2 (j ⤇ fill K' #true)) i3 (l ↦ₛ v2)%I) Δ2 = Some Δ3 →
+    (Esnoc (Esnoc Enil i2 (j ⤇ fill K' (v', #true)%V)) i3 (l ↦ₛ v2)%I) Δ2 = Some Δ3 →
   envs_entails Δ3 (|={E1,E2}=> Q) →
   envs_entails Δ1 (|={E1,E2}=> Q).
 Proof.
-  rewrite envs_entails_eq. intros ??? Hfill <-<-? Hcas Hsafe ? HQ.
+  rewrite envs_entails_eq. intros ??? Hfill <-<-? Hcmpxchg Hsafe ? HQ.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' Δ1 false). 2: eassumption.
   rewrite bi.sep_elim_l.
@@ -338,27 +338,27 @@ Proof.
   (* (S (S (spec_ctx ρ) (j => fill _ _)) (S (l ↦ v) ..)) *)
   rewrite assoc.
   rewrite -(assoc _ (spec_ctx ρ) (j ⤇ fill K' _)%I).
-  rewrite step_cas_suc //.
+  rewrite step_cmpxchg_suc //.
   rewrite -(fupd_trans E1 E1 E2).
   rewrite fupd_frame_r.
   apply fupd_mono.
   by rewrite (comm _ (j ⤇ _)%I) bi.wand_elim_r.
 Qed.
 
-Tactic Notation "tp_cas_suc" constr(j) :=
+Tactic Notation "tp_cmpxchg_suc" constr(j) :=
   iStartProof;
   with_spec_ctx ltac:(fun _ =>
-  eapply (tac_tp_cas_suc j);
-    [solve_ndisj || fail "tp_cas_suc: cannot prove 'nclose specN ⊆ ?'"
-    |iAssumptionCore || fail "tp_cas_suc: cannot find spec_ctx" (* spec_ctx *)
-    |iAssumptionCore || fail "tp_cas_suc: cannot find '" j " ⤇ ?'"
-    |tp_bind_helper (* e = K'[CAS _ _ _] *)
+  eapply (tac_tp_cmpxchg_suc j);
+    [solve_ndisj || fail "tp_cmpxchg_suc: cannot prove 'nclose specN ⊆ ?'"
+    |iAssumptionCore || fail "tp_cmpxchg_suc: cannot find spec_ctx" (* spec_ctx *)
+    |iAssumptionCore || fail "tp_cmpxchg_suc: cannot find '" j " ⤇ ?'"
+    |tp_bind_helper (* e = K'[CmpXchg _ _ _] *)
     |iSolveTC
     |iSolveTC
-    |iAssumptionCore || fail "tp_cas_suc: cannot find '? ↦ ?'"
+    |iAssumptionCore || fail "tp_cmpxchg_suc: cannot find '? ↦ ?'"
     |try (simpl; congruence)     (* v' = v1 *)
-    |try heap_lang.proofmode.solve_vals_cas_compare_safe
-    |pm_reflexivity || fail "tp_cas_suc: this should not happen"
+    |try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
+    |pm_reflexivity || fail "tp_cmpxchg_suc: this should not happen"
     |(* new goal *)]).
 
 Lemma tac_tp_faa `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc)  e2 (z1 z2 : Z) Q :
@@ -405,7 +405,7 @@ Tactic Notation "tp_faa" constr(j) :=
     [solve_ndisj || fail "tp_faa: cannot prove 'nclose specN ⊆ ?'"
     |iAssumptionCore || fail "tp_faa: cannot find spec_ctx" (* spec_ctx *)
     |iAssumptionCore || fail "tp_faa: cannot find '" j " ⤇ ?'"
-    |tp_bind_helper (* e = K'[CAS _ _ _] *)
+    |tp_bind_helper (* e = K'[FAA _ _ _] *)
     |iSolveTC (* IntoVal *)
     |iAssumptionCore || fail "tp_faa: cannot find '? ↦ ?'"
     |pm_reflexivity || fail "tp_faa: this should not happen"
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index eef8817..47ca029 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -102,7 +102,7 @@ Tactic Notation "rel_apply_l" open_constr(lem) :=
       end));
   try lazymatch goal with
   | |- val_is_unboxed _ => fast_done
-  | |- vals_cas_compare_safe _ _ =>
+  | |- vals_cmpxchg_compare_safe _ _ =>
     fast_done || (left; fast_done) || (right; fast_done)
   end;
   try rel_finish.
@@ -428,19 +428,19 @@ Tactic Notation "rel_alloc_l" :=
   let H := iFresh "H" in
   rel_alloc_l l as H.
 
-(** Cas *)
-(* TODO: non-atomic tactics for CAS? *)
-Tactic Notation "rel_cas_l_atomic" := rel_apply_l refines_cas_l.
+(** CmpXchg *)
+(* TODO: non-atomic tactics for CmpXchg? *)
+Tactic Notation "rel_cmpxchg_l_atomic" := rel_apply_l refines_cmpxchg_l.
 
-Lemma tac_rel_cas_fail_r `{relocG Σ} K ℶ1 i1 E (l : loc) e1 e2 v1 v2 v e t eres A :
-  e = fill K (CAS (# l) e1 e2) →
+Lemma tac_rel_cmpxchg_fail_r `{relocG Σ} K ℶ1 i1 E (l : loc) e1 e2 v1 v2 v e t eres A :
+  e = fill K (CmpXchg (# l) e1 e2) →
   IntoVal e1 v1 →
   IntoVal e2 v2 →
   nclose specN ⊆ E →
   envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
   val_for_compare v ≠ val_for_compare v1 →
-  vals_cas_compare_safe v v1 →
-  eres = fill K #false →
+  vals_cmpxchg_compare_safe v v1 →
+  eres = fill K (v, #false)%V →
   envs_entails ℶ1 (refines E t eres A) →
   envs_entails ℶ1 (refines E t e A).
 Proof.
@@ -448,19 +448,19 @@ Proof.
   subst e eres.
   rewrite envs_lookup_split // /= Hg; simpl.
   apply bi.wand_elim_l'.
-  eapply refines_cas_fail_r; eauto.
+  eapply refines_cmpxchg_fail_r; eauto.
 Qed.
 
-Lemma tac_rel_cas_suc_r `{relocG Σ} K ℶ1 ℶ2 i1 E (l : loc) e1 e2 v1 v2 v e t eres A :
-  e = fill K (CAS (# l) e1 e2) →
+Lemma tac_rel_cmpxchg_suc_r `{relocG Σ} K ℶ1 ℶ2 i1 E (l : loc) e1 e2 v1 v2 v e t eres A :
+  e = fill K (CmpXchg (# l) e1 e2) →
   IntoVal e1 v1 →
   IntoVal e2 v2 →
   nclose specN ⊆ E →
   envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
   val_for_compare v = val_for_compare v1 →
-  vals_cas_compare_safe v v1 →
+  vals_cmpxchg_compare_safe v v1 →
   envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v2)) ℶ1 = Some ℶ2 →
-  eres = fill K #true →
+  eres = fill K (v, #true)%V →
   envs_entails ℶ2 (refines E t eres A) →
   envs_entails ℶ1 (refines E t e A).
 Proof.
@@ -469,48 +469,48 @@ Proof.
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id Hg.
   apply bi.wand_elim_l'.
-  eapply refines_cas_suc_r; eauto.
+  eapply refines_cmpxchg_suc_r; eauto.
 Qed.
 
-Tactic Notation "rel_cas_fail_r" :=
+Tactic Notation "rel_cmpxchg_fail_r" :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦ₛ _)%I) => l end in
-    iAssumptionCore || fail "rel_cas_fail_r: cannot find" l "↦ₛ ?" in
+    iAssumptionCore || fail "rel_cmpxchg_fail_r: cannot find" l "↦ₛ ?" in
   rel_pures_r;
   first
     [rel_reshape_cont_r ltac:(fun K e' =>
-       eapply (tac_rel_cas_fail_r K);
-       [reflexivity  (** e = fill K (CAS #l e1 e2) *)
+       eapply (tac_rel_cmpxchg_fail_r K);
+       [reflexivity  (** e = fill K (CmpXchg #l e1 e2) *)
        |iSolveTC     (** e1 is a value *)
        |iSolveTC     (** e2 is a value *)
        |idtac..])
-    |fail 1 "rel_cas_fail_r: cannot find 'Cas'"];
-  (* the remaining goals are from tac_rel_cas_fail_r (except for the first one, which has already been solved by this point) *)
-  [solve_ndisj || fail "rel_cas_fail_r: cannot prove 'nclose specN ⊆ ?'"
+    |fail 1 "rel_cmpxchg_fail_r: cannot find 'CmpXchg'"];
+  (* the remaining goals are from tac_rel_cmpxchg_fail_r (except for the first one, which has already been solved by this point) *)
+  [solve_ndisj || fail "rel_cmpxchg_fail_r: cannot prove 'nclose specN ⊆ ?'"
   |solve_mapsto ()
   |try (simpl; congruence)   (** v ≠ v1 *)
-  |try heap_lang.proofmode.solve_vals_cas_compare_safe
+  |try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
   |reflexivity
   |rel_finish  (** new goal *)].
 
-Tactic Notation "rel_cas_suc_r" :=
+Tactic Notation "rel_cmpxchg_suc_r" :=
   let solve_mapsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦ₛ _)%I) => l end in
-    iAssumptionCore || fail "rel_cas_suc_r: cannot find" l "↦ₛ ?" in
+    iAssumptionCore || fail "rel_cmpxchg_suc_r: cannot find" l "↦ₛ ?" in
   rel_pures_r;
   first
     [rel_reshape_cont_r ltac:(fun K e' =>
-       eapply (tac_rel_cas_suc_r K);
-       [reflexivity  (** e = fill K (CAS #l e1 e2) *)
+       eapply (tac_rel_cmpxchg_suc_r K);
+       [reflexivity  (** e = fill K (CmpXchg #l e1 e2) *)
        |iSolveTC     (** e1 is a value *)
        |iSolveTC     (** e2 is a value *)
        |idtac..])
-    |fail 1 "rel_cas_suc_r: cannot find 'Cas'"];
-  (* the remaining goals are from tac_rel_cas_suc_r (except for the first one, which has already been solved by this point) *)
-  [solve_ndisj || fail "rel_cas_suc_r: cannot prove 'nclose specN ⊆ ?'"
+    |fail 1 "rel_cmpxchg_suc_r: cannot find 'CmpXchg'"];
+  (* the remaining goals are from tac_rel_cmpxchg_suc_r (except for the first one, which has already been solved by this point) *)
+  [solve_ndisj || fail "rel_cmpxchg_suc_r: cannot prove 'nclose specN ⊆ ?'"
   |solve_mapsto ()
   |try (simpl; congruence)   (** v = v1 *)
-  |try heap_lang.proofmode.solve_vals_cas_compare_safe
+  |try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
   |pm_reflexivity  (** new env *)
   |reflexivity
   |rel_finish  (** new goal *)].
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 378f916..1328e10 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -194,45 +194,45 @@ Section rules.
     by iApply "Hlog".
   Qed.
 
-  Lemma refines_cas_fail_r E K l e1 e2 v1 v2 v t A :
+  Lemma refines_cmpxchg_fail_r E K l e1 e2 v1 v2 v t A :
     nclose specN ⊆ E →
     IntoVal e1 v1 →
     IntoVal e2 v2 →
-    vals_cas_compare_safe v v1 →
+    vals_cmpxchg_compare_safe v v1 →
     val_for_compare v ≠ val_for_compare v1 →
     l ↦ₛ v -∗
-    (l ↦ₛ v -∗ REL t << fill K (of_val #false) @ E : A)
-    -∗ REL t << fill K (CAS #l e1 e2) @ E : A.
+    (l ↦ₛ v -∗ REL t << fill K (of_val (v, #false)) @ E : A)
+    -∗ REL t << fill K (CmpXchg #l e1 e2) @ E : A.
   Proof.
     iIntros (?<-<-??) "Hl Hlog".
-    pose (Φ := (fun (w : val) => ⌜w = #false⌝ ∗ l ↦ₛ v)%I).
+    pose (Φ := (fun (w : val) => ⌜w = (v, #false)%V⌝ ∗ l ↦ₛ v)%I).
     iApply (refines_step_r Φ with "[Hl]"); eauto.
     { cbv[Φ].
       iIntros (ρ j K') "#Hs Hj /=".
-      tp_cas_fail j; auto.
-      iExists #false. simpl.
+      tp_cmpxchg_fail j; auto.
+      iExists _. simpl.
       iFrame. eauto. }
     iIntros (w) "[% Hl]"; subst.
     by iApply "Hlog".
   Qed.
 
-  Lemma refines_cas_suc_r E K l e1 e2 v1 v2 v t A :
+  Lemma refines_cmpxchg_suc_r E K l e1 e2 v1 v2 v t A :
     nclose specN ⊆ E →
     IntoVal e1 v1 →
     IntoVal e2 v2 →
-    vals_cas_compare_safe v v1 →
+    vals_cmpxchg_compare_safe v v1 →
     val_for_compare v = val_for_compare v1 →
     l ↦ₛ v -∗
-    (l ↦ₛ v2 -∗ REL t << fill K (of_val #true) @ E : A)
-    -∗ REL t << fill K (CAS #l e1 e2) @ E : A.
+    (l ↦ₛ v2 -∗ REL t << fill K (of_val (v, #true)) @ E : A)
+    -∗ REL t << fill K (CmpXchg #l e1 e2) @ E : A.
   Proof.
     iIntros (?<-<-??) "Hl Hlog".
-    pose (Φ := (fun w => ⌜w = #true⌝ ∗ l ↦ₛ v2)%I).
+    pose (Φ := (fun w => ⌜w = (v, #true)%V⌝ ∗ l ↦ₛ v2)%I).
     iApply (refines_step_r Φ with "[Hl]"); eauto.
     { cbv[Φ].
       iIntros (ρ j K') "#Hs Hj /=".
-      tp_cas_suc j; auto.
-      iExists #true. simpl.
+      tp_cmpxchg_suc j; auto.
+      iExists _. simpl.
       iFrame. eauto. }
     iIntros (w) "[% Hl]"; subst.
     by iApply "Hlog".
@@ -385,26 +385,26 @@ Section rules.
     iApply (wp_store _ _ _ _ v' with "Hl"); auto.
   Qed.
 
-  Lemma refines_cas_l K E l e1 e2 v1 v2 t A :
+  Lemma refines_cmpxchg_l K E l e1 e2 v1 v2 t A :
     IntoVal e1 v1 →
     IntoVal e2 v2 →
     val_is_unboxed v1 →
     (|={⊤,E}=> ∃ v', ▷ l ↦ v' ∗
-     (⌜val_for_compare v' ≠ val_for_compare v1⌝ -∗ ▷ (l ↦ v' -∗ REL fill K (of_val #false) << t @ E : A)) ∧
-     (⌜val_for_compare v' = val_for_compare v1⌝ -∗ ▷ (l ↦ v2 -∗ REL fill K (of_val #true) << t @ E : A)))
-    -∗ REL fill K (CAS #l e1 e2) << t : A.
+     (⌜val_for_compare v' ≠ val_for_compare v1⌝ -∗ ▷ (l ↦ v' -∗ REL fill K (of_val (v', #false)) << t @ E : A)) ∧
+     (⌜val_for_compare v' = val_for_compare v1⌝ -∗ ▷ (l ↦ v2 -∗ REL fill K (of_val (v', #true)) << t @ E : A)))
+    -∗ REL fill K (CmpXchg #l e1 e2) << t : A.
   Proof.
     iIntros (<-<-?) "Hlog".
     iApply refines_atomic_l; auto.
     iMod "Hlog" as (v') "[Hl Hlog]". iModIntro.
     destruct (decide (val_for_compare v' = val_for_compare v1)).
-    - (* CAS successful *) subst.
-      iApply (wp_cas_suc with "Hl"); eauto.
+    - (* CmpXchg successful *) subst.
+      iApply (wp_cmpxchg_suc with "Hl"); eauto.
       { by right. }
       iDestruct "Hlog" as "[_ Hlog]".
       iSpecialize ("Hlog" with "[]"); eauto.
-    - (* CAS failed *)
-      iApply (wp_cas_fail with "Hl"); eauto.
+    - (* CmpXchg failed *)
+      iApply (wp_cmpxchg_fail with "Hl"); eauto.
       { by right. }
       iDestruct "Hlog" as "[Hlog _]".
       iSpecialize ("Hlog" with "[]"); eauto.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 85de095..cdb6107 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -212,15 +212,15 @@ Section rules.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.
 
-  (** CAS & FAA *)
-  Lemma step_cas_fail E ρ j K l q v' e1 v1 e2 v2 :
+  (** CmpXchg & FAA *)
+  Lemma step_cmpxchg_fail E ρ j K l q v' e1 v1 e2 v2 :
     IntoVal e1 v1 →
     IntoVal e2 v2 →
     nclose specN ⊆ E →
-    vals_cas_compare_safe v' v1 →
+    vals_cmpxchg_compare_safe v' v1 →
     val_for_compare v' ≠ val_for_compare v1 →
-    spec_ctx ρ ∗ j ⤇ fill K (CAS #l e1 e2) ∗ l ↦ₛ{q} v'
-    ={E}=∗ j ⤇ fill K #false ∗ l ↦ₛ{q} v'.
+    spec_ctx ρ ∗ j ⤇ fill K (CmpXchg #l e1 e2) ∗ l ↦ₛ{q} v'
+    ={E}=∗ j ⤇ fill K (v', #false)%V ∗ l ↦ₛ{q} v'.
   Proof.
     iIntros (<-<-???) "(#Hinv & Hj & Hl)".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
@@ -231,21 +231,22 @@ Section rules.
       as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
-        (exclusive_local_update _ (Excl (fill K (# false)))). }
+        (exclusive_local_update _ (Excl (fill K (_, #false)%V))). }
     iFrame "Hj Hl". iApply "Hclose". iNext.
-    iExists (<[j:=fill K (#false)]> tp), σ.
+    iExists (<[j:=fill K (_, #false)%V]> tp), σ.
     rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
+    rewrite bool_decide_false //.
   Qed.
 
-  Lemma step_cas_suc E ρ j K l e1 v1 v1' e2 v2:
+  Lemma step_cmpxchg_suc E ρ j K l e1 v1 v1' e2 v2:
     IntoVal e1 v1 →
     IntoVal e2 v2 →
     nclose specN ⊆ E →
-    vals_cas_compare_safe v1' v1 →
+    vals_cmpxchg_compare_safe v1' v1 →
     val_for_compare v1' = val_for_compare v1 →
-    spec_ctx ρ ∗ j ⤇ fill K (CAS #l e1 e2) ∗ l ↦ₛ v1'
-    ={E}=∗ j ⤇ fill K #true ∗ l ↦ₛ v2.
+    spec_ctx ρ ∗ j ⤇ fill K (CmpXchg #l e1 e2) ∗ l ↦ₛ v1'
+    ={E}=∗ j ⤇ fill K (v1', #true)%V ∗ l ↦ₛ v2.
   Proof.
     iIntros (<-<-???) "(#Hinv & Hj & Hl)"; subst.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
@@ -256,15 +257,16 @@ Section rules.
       as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
-        (exclusive_local_update _ (Excl (fill K (# true)))). }
+        (exclusive_local_update _ (Excl (fill K (_, #true)%V))). }
     iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
     { eapply auth_update, prod_local_update_2, singleton_local_update,
         (exclusive_local_update _ (1%Qp, to_agree v2)); last done.
       by rewrite /to_gen_heap lookup_fmap Hl. }
     iFrame "Hj Hl". iApply "Hclose". iNext.
-    iExists (<[j:=fill K (# true)]> tp), (state_upd_heap <[l:=v2]> σ).
+    iExists (<[j:=fill K (_, #true)%V]> tp), (state_upd_heap <[l:=v2]> σ).
     rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
+    rewrite bool_decide_true //.
   Qed.
 
   Lemma step_faa E ρ j K l e1 e2 (i1 i2 : Z) :
diff --git a/theories/prelude/ctx_subst.v b/theories/prelude/ctx_subst.v
index a69e74e..ce998bd 100644
--- a/theories/prelude/ctx_subst.v
+++ b/theories/prelude/ctx_subst.v
@@ -24,9 +24,9 @@ Fixpoint subst_map_ctx_item (es : stringmap val) (K : ectx_item)
   | LoadCtx => LoadCtx
   | StoreLCtx v2 => StoreLCtx v2
   | StoreRCtx e1 => StoreRCtx (subst_map es e1)
-  | CasLCtx v1 v2 => CasLCtx v1 v2
-  | CasMCtx e0 v2 => CasMCtx (subst_map es e0) v2
-  | CasRCtx e0 e1 => CasRCtx (subst_map es e0) (subst_map es e1)
+  | CmpXchgLCtx v1 v2 => CmpXchgLCtx v1 v2
+  | CmpXchgMCtx e0 v2 => CmpXchgMCtx (subst_map es e0) v2
+  | CmpXchgRCtx e0 e1 => CmpXchgRCtx (subst_map es e0) (subst_map es e1)
   | FaaLCtx v2 => FaaLCtx v2
   | FaaRCtx e1 => FaaRCtx (subst_map es e1)
   | ResolveLCtx Ki v1 v2 => ResolveLCtx (subst_map_ctx_item es Ki) v1 v2
diff --git a/theories/tests/tp_tests.v b/theories/tests/tp_tests.v
index eb53ced..9213530 100644
--- a/theories/tests/tp_tests.v
+++ b/theories/tests/tp_tests.v
@@ -31,11 +31,12 @@ Lemma test2 E1 j K (l : loc) (n : nat) ρ :
   ={E1}=∗ l ↦ₛ #(n*2) ∗ j ⤇ fill K #true.
 Proof.
   iIntros (?) "#? Hj Hl".
-  tp_cas_fail j. tp_normalise j.
+  tp_cmpxchg_fail j. tp_normalise j.
+  tp_pure j (Snd _). tp_normalise j.
   tp_closure j. tp_normalise j.
   tp_seq j. tp_normalise j.
   tp_binop j. tp_normalise j.
-  tp_cas_suc j. by iFrame.
+  tp_cmpxchg_suc j. tp_pure j (Snd _). by iFrame.
 Qed.
 
 (* fork *)
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index a43aa9f..40dc478 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -46,10 +46,10 @@ Inductive ctx_item :=
   | CTX_Load
   | CTX_StoreL (e2 : expr)
   | CTX_StoreR (e1 : expr)
-  (* Compare and swap used for fine-grained concurrency *)
-  | CTX_CAS_L (e1 : expr) (e2 : expr)
-  | CTX_CAS_M (e0 : expr) (e2 : expr)
-  | CTX_CAS_R (e0 : expr) (e1 : expr).
+  (* Compare-exchange used for fine-grained concurrency *)
+  | CTX_CmpXchg_L (e1 : expr) (e2 : expr)
+  | CTX_CmpXchg_M (e0 : expr) (e2 : expr)
+  | CTX_CmpXchg_R (e0 : expr) (e1 : expr).
 
 Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
   match ctx with
@@ -82,9 +82,9 @@ Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
   | CTX_Load => Load e
   | CTX_StoreL e2 => Store e e2
   | CTX_StoreR e1 => Store e1 e
-  | CTX_CAS_L e1 e2 => CAS e e1 e2
-  | CTX_CAS_M e0 e2 => CAS e0 e e2
-  | CTX_CAS_R e0 e1 => CAS e0 e1 e
+  | CTX_CmpXchg_L e1 e2 => CmpXchg e e1 e2
+  | CTX_CmpXchg_M e0 e2 => CmpXchg e0 e e2
+  | CTX_CmpXchg_R e0 e1 => CmpXchg e0 e1 e
   end.
 
 Definition ctx := list ctx_item.
@@ -180,15 +180,15 @@ Inductive typed_ctx_item :
   | TP_CTX_CasL Γ e1  e2 τ :
      EqType τ → UnboxedType τ →
      typed Γ e1 τ → typed Γ e2 τ →
-     typed_ctx_item (CTX_CAS_L e1 e2) Γ (Tref τ) Γ TBool
+     typed_ctx_item (CTX_CmpXchg_L e1 e2) Γ (Tref τ) Γ (TProd τ TBool)
   | TP_CTX_CasM Γ e0 e2 τ :
      EqType τ → UnboxedType τ →
      typed Γ e0 (Tref τ) → typed Γ e2 τ →
-     typed_ctx_item (CTX_CAS_M e0 e2) Γ τ Γ TBool
+     typed_ctx_item (CTX_CmpXchg_M e0 e2) Γ τ Γ (TProd τ TBool)
   | TP_CTX_CasR Γ e0 e1 τ :
      EqType τ → UnboxedType τ →
      typed Γ e0 (Tref τ) → typed Γ e1 τ →
-     typed_ctx_item (CTX_CAS_R e0 e1) Γ τ Γ TBool.
+     typed_ctx_item (CTX_CmpXchg_R e0 e1) Γ τ Γ (TProd τ TBool).
 
 Inductive typed_ctx: ctx → stringmap type → type → stringmap type → type → Prop :=
   | TPCTX_nil Γ τ :
@@ -362,13 +362,13 @@ Section bin_log_related_under_typed_ctx.
       + iApply (bin_log_related_store with "[]");
           try by iApply binary_fundamental.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_CAS with "[] []");
+      + iApply (bin_log_related_CmpXchg with "[] []");
           try (by iApply binary_fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_CAS with "[] []");
+      + iApply (bin_log_related_CmpXchg with "[] []");
           try (by iApply binary_fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_CAS with "[] []");
+      + iApply (bin_log_related_CmpXchg with "[] []");
           try (by iApply binary_fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
   Qed.
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 3aa081a..836405d 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -275,13 +275,13 @@ Section fundamental.
     - by iApply "IH2".
   Qed.
 
-  Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ
+  Lemma bin_log_related_CmpXchg Δ Γ e1 e2 e3 e1' e2' e3' τ
     (HEqτ : EqType τ)
     (HUbτ : UnboxedType τ) :
     ({Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref τ) -∗
     ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ) -∗
     ({Δ;Γ} ⊨ e3 ≤log≤ e3' : τ) -∗
-    {Δ;Γ} ⊨ CAS e1 e2 e3 ≤log≤ CAS e1' e2' e3' : TBool.
+    {Δ;Γ} ⊨ CmpXchg e1 e2 e3 ≤log≤ CmpXchg e1' e2' e3' : TProd τ TBool.
   Proof.
     iIntros "IH1 IH2 IH3".
     intro_clause.
@@ -292,24 +292,26 @@ Section fundamental.
     iDestruct (unboxed_type_sound with "IH2") as "[% %]"; try fast_done.
     iDestruct (eq_type_sound with "IH2") as "%"; first fast_done.
     iDestruct (eq_type_sound with "IH3") as "%"; first fast_done.
-    simplify_eq. rel_cas_l_atomic.
+    simplify_eq. rel_cmpxchg_l_atomic.
     iInv (relocN .@ "ref" .@ (l,l')) as (v1 v1') "[Hv1 [>Hv2 #Hv]]" "Hclose".
     iModIntro. iExists _; iFrame. simpl.
     destruct (decide (val_for_compare v1 = val_for_compare v2')) as [|Hneq]; subst.
     - iSplitR; first by (iIntros (?); contradiction).
       iIntros (?). iNext. iIntros "Hv1".
       iDestruct (eq_type_sound with "Hv") as "%"; first fast_done.
-      rel_cas_suc_r.
+      rel_cmpxchg_suc_r.
       iMod ("Hclose" with "[-]").
       { iNext; iExists _, _; by iFrame. }
-      rel_values.
+      rel_values. iExists _, _, _, _. do 2 (iSplitL; first done).
+      iFrame "Hv". iExists _. done.
     - iSplitL; last by (iIntros (?); congruence).
       iIntros (?). iNext. iIntros "Hv1".
       iDestruct (eq_type_sound with "Hv") as "%"; first fast_done.
-      rel_cas_fail_r.
+      rel_cmpxchg_fail_r.
       iMod ("Hclose" with "[-]").
       { iNext; iExists _, _; by iFrame. }
-      rel_values.
+      rel_values. iExists _, _, _, _. do 2 (iSplitL; first done).
+      iFrame "Hv". iExists _. done.
   Qed.
 
   Lemma bin_log_related_alloc Δ Γ e e' τ :
@@ -499,7 +501,7 @@ Section fundamental.
     - by iApply bin_log_related_alloc.
     - by iApply bin_log_related_load.
     - by iApply (bin_log_related_store with "[]").
-    - by iApply (bin_log_related_CAS with "[] []").
+    - by iApply (bin_log_related_CmpXchg with "[] []").
   Qed.
 
   Theorem refines_typed e Ï„ :
diff --git a/theories/typing/types.v b/theories/typing/types.v
index f1cdffa..ecc67ba 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -149,10 +149,10 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
   | TAlloc e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : Tref τ
   | TLoad e τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ Load e : τ
   | TStore e e' τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ e' : τ → Γ ⊢ₜ Store e e' : TUnit
-  | TCAS e1 e2 e3 Ï„ :
+  | TCmpXchg e1 e2 e3 Ï„ :
      EqType τ → UnboxedType τ →
      Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
-     Γ ⊢ₜ CAS e1 e2 e3 : TBool
+     Γ ⊢ₜ CmpXchg e1 e2 e3 : TProd τ TBool
 where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
 
 Lemma binop_nat_typed_safe (op : bin_op) (n1 n2 : Z) Ï„ :
-- 
GitLab