diff --git a/opam.pins b/opam.pins
index 4bcf1fff021472e9b3226de2cb28aa88432a52c8..57d2788c63d2f4eb4779af0ea059b967ef0d4d1f 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq f8e2c74ce745f092c4d20e9ef855d7657e25134c
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2407263c14e0a44a8eafedcc2f5391b6c16ef1c4
diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index f44b27824a057c43d5546b9334428979249a91d2..3e5b379468ec466d3fa58ccce8bcb7b1647dc33d 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -48,10 +48,38 @@ Lemma wp_le E (n1 n2 : Z) P Φ :
   (n2 < n1 → P -∗ ▷ |={E}=> Φ (LitV false)) →
   P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
+  iIntros (Hl Hg) "HP". iApply wp_fupd.
+  destruct (bool_decide_reflect (n1 ≤ n2)); [rewrite Hl //|rewrite Hg; last omega];
+    clear Hl Hg; (iApply wp_bin_op_pure; first by econstructor); iNext; iIntros (?? Heval);
+    inversion_clear Heval; [rewrite bool_decide_true //|rewrite bool_decide_false //].
 Qed.
 
+Lemma wp_offset E l z Φ :
+  ▷ (|={E}=> Φ (LitV $ LitLoc $ shift_loc l z)) -∗
+    WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $LitInt z) @ E {{ Φ }}.
+Proof.
+  iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
+  iNext. iIntros (?? Heval). inversion_clear Heval. done.
+Qed.
+
+Lemma wp_plus E z1 z2 Φ :
+  ▷ (|={E}=> Φ (LitV $ LitInt $ z1 + z2)) -∗
+    WP BinOp PlusOp (Lit $ LitInt z1) (Lit $LitInt z2) @ E {{ Φ }}.
+Proof.
+  iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
+  iNext. iIntros (?? Heval). inversion_clear Heval. done.
+Qed.
+
+Lemma wp_minus E z1 z2 Φ :
+  ▷ (|={E}=> Φ (LitV $ LitInt $ z1 - z2)) -∗
+    WP BinOp MinusOp (Lit $ LitInt z1) (Lit $LitInt z2) @ E {{ Φ }}.
+Proof.
+  iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
+  iNext. iIntros (?? Heval). inversion_clear Heval. done.
+Qed.
+
+(* TODO: Add lemmas for remaining binary operators. *)
+
 Lemma wp_if E (b : bool) e1 e2 Φ :
   (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I -∗
   WP If (Lit b) e1 e2 @ E {{ Φ }}.
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 9289944881bb346bb25bc2d95f47e1123dff21db..a2f0e148d18eeed9b17580c1371a420fd596190b 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -529,8 +529,8 @@ Section heap.
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
-  Lemma wp_cas_int_fail E l q z1 e2 v2 zl :
-    ↑heapN ⊆ E → to_val e2 = Some v2 → z1 ≠ zl →
+  Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
+    ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 → z1 ≠ zl →
     {{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitInt zl) }}}
       CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
     {{{ RET LitV $ LitInt 0; l ↦{q} (LitV $ LitInt zl) }}}.
@@ -539,14 +539,36 @@ Section heap.
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
-    iApply (wp_cas_fail_pst with "[$Hσ]"); eauto.
-    { by rewrite /= bool_decide_false. }
-    iNext. iIntros "Hσ". iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
+    iApply (wp_cas_pst with "[$Hσ]"); eauto.
+    { right. by constructor. }
+    { inversion 1. done. }
+    iNext. iIntros ([|]).
+    { iIntros "[Heq _]". iDestruct "Heq" as %Heq. inversion Heq. done. }
+    iIntros "[_ Hσ]". iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
-  Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 v2 l' vl' :
-    ↑heapN ⊆ E → to_val e2 = Some v2 → l1 ≠ l' →
+  Lemma wp_cas_int_suc E l z1 e2 lit2 :
+    ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 →
+    {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitInt z1) }}}
+      CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
+    {{{ RET LitV $ LitInt 1; l ↦ LitV lit2 }}}.
+  Proof.
+    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
+    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
+    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
+    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
+    iApply (wp_cas_pst with "[$Hσ]"); eauto.
+    { left. by constructor. }
+    iNext. iIntros ([|]); last first.
+    { iIntros "[Hneq _]". iDestruct "Hneq" as %Hneq. inversion Hneq. done. }
+    iIntros "[_ Hσ]". iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
+    iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
+    iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
+  Qed.
+
+  Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
+    ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 → l1 ≠ l' →
     {{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
       CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
     {{{ RET LitV $ LitInt 0;
@@ -558,46 +580,33 @@ Section heap.
     iDestruct (heap_mapsto_lookup with "Hvalσ Hl") as %[n Hσl].
     iDestruct (heap_mapsto_lookup with "Hvalσ Hl'") as %[n' Hσl'].
     iDestruct (heap_mapsto_lookup with "Hvalσ Hl1") as %[n1 Hσl1].
-    iApply (wp_cas_fail_pst with "[$Hσ]"); eauto.
-    { by rewrite /= bool_decide_false // Hσl1 Hσl'. }
-    iNext. iIntros "Hσ ".
-    iMod ("Hclose" with "[-Hl Hl' Hl1 HΦ]") as "_"; last by iApply "HΦ"; iFrame.
+    iApply (wp_cas_pst with "[$Hσ]"); eauto.
+    { right. by constructor. }
+    { inversion 1; subst; simplify_option_eq. }
+    iNext. iIntros ([|]).
+    { iIntros "[Heq _]". iDestruct "Heq" as %Heq. inversion Heq; simplify_option_eq. }
+    iIntros "[_ Hσ]". iMod ("Hclose" with "[-Hl Hl' Hl1 HΦ]") as "_"; last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. by iFrame.
   Qed.
 
-  Lemma wp_cas_int_suc E l z1 e2 v2 :
-    ↑heapN ⊆ E → to_val e2 = Some v2 →
-    {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitInt z1) }}}
-      CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
-    {{{ RET LitV $ LitInt 1; l ↦ v2 }}}.
-  Proof.
-    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
-    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
-    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
-    iApply (wp_cas_suc_pst with "[$Hσ]"); eauto.
-    { by rewrite /= bool_decide_true. }
-    iNext. iIntros "Hσ".
-    iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
-    iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
-  Qed.
-
-  Lemma wp_cas_loc_suc E l l1 e2 v2 :
-    ↑heapN ⊆ E → to_val e2 = Some v2 →
+  Lemma wp_cas_loc_suc E l l1 e2 lit2 :
+    ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 →
     {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitLoc l1) }}}
       CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
-    {{{ RET LitV $ LitInt 1; l ↦ v2 }}}.
+    {{{ RET LitV $ LitInt 1; l ↦ LitV lit2 }}}.
   Proof.
     iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
-    iApply (wp_cas_suc_pst with "[$Hσ]"); eauto.
-    { by rewrite /= bool_decide_true. }
-    iNext. iIntros "Hσ".
-    iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
+    iApply (wp_cas_pst with "[$Hσ]"); eauto.
+    { left. by constructor. }
+    iNext. iIntros ([|]); last first.
+    { iIntros "[Hneq _]". iDestruct "Hneq" as %Hneq. inversion Hneq. done. }
+    iIntros "[_ Hσ]". iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
   Qed.
+
+  (* TODO: Add a lemma for non-deterministic CAS on locations. *)
 End heap.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 8acb16ccbf9a777126b621ea696096d1ed6c58ec..87ff9a73a028a4003f505efa860a963cb24848c9 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -11,7 +11,7 @@ Definition loc : Set := block * Z.
 Inductive base_lit : Set :=
 | LitUnit | LitLoc (l : loc) | LitInt (n : Z).
 Inductive bin_op : Set :=
-| PlusOp | MinusOp | LeOp | ProjOp.
+| PlusOp | MinusOp | LeOp | EqOp | OffsetOp.
 Inductive order : Set :=
 | ScOrd | Na1Ord | Na2Ord.
 
@@ -167,17 +167,7 @@ Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :
 Definition lit_of_bool (b : bool) : base_lit :=
   LitInt (if b then 1 else 0).
 
-Definition shift_loc (l : loc) (n : Z) : loc := (l.1, l.2 + n).
-
-Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
-  match op, l1, l2 with
-  | PlusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 + n2)
-  | MinusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 - n2)
-  | LeOp, LitInt n1, LitInt n2 =>
-    Some $ lit_of_bool $ bool_decide (n1 ≤ n2)
-  | ProjOp, LitLoc l, LitInt n => Some $ LitLoc $ shift_loc l n
-  | _, _, _ => None
-  end.
+Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
 
 Fixpoint init_mem (l:loc) (init:list val) (σ:state) : state :=
   match init with
@@ -191,21 +181,41 @@ Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
   | S n => delete l (free_mem (shift_loc l 1) n σ)
   end.
 
-Definition value_eq (σ : state) (v1 v2 : val) : option bool :=
-  match v1, v2 with
-  | LitV (LitInt z1), LitV (LitInt z2) => Some (bool_decide (z1 = z2))
-  | LitV (LitLoc l1), LitV (LitLoc l2) =>
-    if bool_decide (l1 = l2) then Some true
-    else match σ !! l1, σ !! l2 with
-         | Some _, Some _ => Some false
-         | _, _ => None
-         end
-  | _, _ => None
-  end.
+Inductive lit_eq (σ : state) : base_lit → base_lit → Prop :=
+| IntRefl z : lit_eq σ (LitInt z) (LitInt z)
+| LocRefl l : lit_eq σ (LitLoc l) (LitLoc l)
+| LocUnallocL l1 l2 :
+    σ !! l1 = None →
+    lit_eq σ (LitLoc l1) (LitLoc l2)
+| LocUnallocR l1 l2 :
+    σ !! l2 = None →
+    lit_eq σ (LitLoc l1) (LitLoc l2).
+
+Inductive lit_neq (σ : state) : base_lit → base_lit → Prop :=
+| IntNeq z1 z2 :
+    z1 ≠ z2 → lit_neq σ (LitInt z1) (LitInt z2)
+| LocNeq l1 l2 :
+    l1 ≠ l2 → lit_neq σ (LitLoc l1) (LitLoc l2).
+
+Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_lit → Prop :=
+| BinOpPlus z1 z2 :
+    bin_op_eval σ PlusOp (LitInt z1) (LitInt z2) (LitInt (z1 + z2))
+| BinOpMinus z1 z2 :
+    bin_op_eval σ MinusOp (LitInt z1) (LitInt z2) (LitInt (z1 - z2))
+| BinOpLe z1 z2 :
+    bin_op_eval σ LeOp (LitInt z1) (LitInt z2) (lit_of_bool $ bool_decide (z1 ≤ z2))
+| BinOpEqTrue l1 l2 :
+    lit_eq σ l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool true)
+| BinOpEqFalse l1 l2 :
+    lit_neq σ l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool false)
+| BinOpOffset l z :
+    bin_op_eval σ OffsetOp (LitLoc l) (LitInt z) (LitLoc $ shift_loc l z).
+
+Definition stuck_term := App (Lit $ LitInt 0) [].
 
 Inductive head_step : expr → state → expr → state → list expr → Prop :=
 | BinOpS op l1 l2 l' σ :
-    bin_op_eval op l1 l2 = Some l' →
+    bin_op_eval σ op l1 l2 l' →
     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ []
 | BetaS f xl e e' el σ:
     Forall (λ ei, is_Some (to_val ei)) el →
@@ -243,17 +253,24 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
     head_step (Write Na2Ord (Lit $ LitLoc l) e) σ
               (Lit LitUnit) (<[l:=(RSt 0, v)]>σ)
               []
-| CasFailS l n e1 v1 e2 v2 vl σ :
-    to_val e1 = Some v1 → to_val e2 = Some v2 →
-    σ !! l = Some (RSt n, vl) →
-    value_eq σ v1 vl = Some false →
+| CasFailS l n e1 lit1 e2 lit2 litl σ :
+    to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
+    σ !! l = Some (RSt n, LitV litl) →
+    lit_neq σ lit1 litl →
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ lit_of_bool false) σ  []
-| CasSucS l e1 v1 e2 v2 vl σ :
-    to_val e1 = Some v1 → to_val e2 = Some v2 →
-    σ !! l = Some (RSt 0, vl) →
-    value_eq σ v1 vl = Some true →
+| CasSucS l e1 lit1 e2 lit2 litl σ :
+    to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
+    σ !! l = Some (RSt 0, LitV litl) →
+    lit_eq σ lit1 litl →
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ
-              (Lit $ lit_of_bool true) (<[l:=(RSt 0, v2)]>σ)
+              (Lit $ lit_of_bool true) (<[l:=(RSt 0, LitV lit2)]>σ)
+              []
+| CasStuckS l n e1 lit1 e2 lit2 litl σ :
+    to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
+    σ !! l = Some (RSt n, LitV litl) → 0 < n →
+    lit_eq σ lit1 litl →
+    head_step (CAS (Lit $ LitLoc l) e1 e2) σ
+              stuck_term σ
               []
 | AllocS n l init σ :
     0 < n →
@@ -451,6 +468,29 @@ Proof. intros. apply is_closed_subst with []; set_solver. Qed.
 Lemma is_closed_of_val X v : is_closed X (of_val v).
 Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
 
+(* Operations on literals *)
+Lemma lit_eq_state σ1 σ2 l1 l2 :
+  (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
+  lit_eq σ1 l1 l2 → lit_eq σ2 l1 l2.
+Proof. intros Heq. inversion 1; econstructor; eauto; eapply Heq; done. Qed.
+
+Lemma lit_neq_state σ1 σ2 l1 l2 :
+  (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
+  lit_neq σ1 l1 l2 → lit_neq σ2 l1 l2.
+Proof. intros Heq. inversion 1; econstructor; eauto; eapply Heq; done. Qed.
+
+Lemma bin_op_eval_state σ1 σ2 op l1 l2 l' :
+  (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
+  bin_op_eval σ1 op l1 l2 l' → bin_op_eval σ2 op l1 l2 l'.
+Proof.
+  intros Heq. inversion 1; econstructor; eauto using lit_eq_state, lit_neq_state.
+Qed.
+
+(* Misc *)
+Lemma stuck_not_head_step σ e' σ' ef :
+  ¬head_step stuck_term σ e' σ' ef.
+Proof. inversion 1. Qed.
+
 (** Equality and other typeclass stuff *)
 Instance base_lit_dec_eq : EqDecision base_lit.
 Proof. solve_decision. Defined.
@@ -527,3 +567,16 @@ Solve Obligations with eauto using to_of_val, of_to_val,
   val_stuck, fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
 
 Canonical Structure lrust_lang := ectx_lang expr.
+
+(* Lemmas about the language. *)
+Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ.
+Proof.
+  intros ??? Hstep. edestruct step_is_head as (?&?&?&?); [..|by do 3 eexists|].
+  - done.
+  - clear. intros Ki K e' Heq (?&?&? & Hstep). destruct Ki; inversion Heq.
+    + destruct K as [|Ki K].
+      * simpl in *. subst. inversion Hstep.
+      * destruct Ki; simpl in *; done.
+    + destruct (map of_val vl); last done. destruct (fill K e'); done.
+  - by eapply stuck_not_head_step.
+Qed.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index a0fc74912e16d223de9c322b9aedb5fa886a60b8..c36762987b346b6ce926cf9e9f22ce192b579ff3 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -31,7 +31,7 @@ Lemma wp_alloc_pst E σ n:
       ownP σ' }}}.
 Proof.
   iIntros (? Φ) "HP HΦ". iApply (wp_lift_atomic_head_step _ σ); eauto.
-  iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
+  iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
   rewrite big_sepL_nil right_id. by iApply "HΦ"; iFrame; eauto.
 Qed.
 
@@ -42,7 +42,7 @@ Lemma wp_free_pst E σ l n :
   {{{ RET LitV $ LitUnit; ownP (free_mem l (Z.to_nat n) σ) }}}.
 Proof.
   iIntros (???)  "HP HΦ". iApply (wp_lift_atomic_head_step _ σ); eauto.
-  iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
+  iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
   rewrite big_sepL_nil right_id. by iApply "HΦ".
 Qed.
 
@@ -74,7 +74,7 @@ Lemma wp_read_na1_pst E l Φ :
 Proof.
   iIntros "HΦP". iApply (wp_lift_head_step E); auto.
   iMod "HΦP" as (σ n v) "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
-  iNext. iIntros (e2 σ2 ef) "[% HΦ]". inv_head_step.
+  iNext. iIntros (e2 σ2 ef) "% HΦ". inv_head_step.
   rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
 Qed.
 
@@ -105,32 +105,30 @@ Lemma wp_write_na1_pst E l v Φ :
 Proof.
   iIntros "HΦP". iApply (wp_lift_head_step E); auto.
   iMod "HΦP" as (σ v') "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
-  iNext. iIntros (e2 σ2 ef) "[% HΦ]". inv_head_step.
+  iNext. iIntros (e2 σ2 ef) "% HΦ". inv_head_step.
   rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
 Qed.
 
-Lemma wp_cas_fail_pst E σ l n e1 v1 v2 vl :
-  to_val e1 = Some v1 →
-  σ !! l = Some (RSt n, vl) →
-  value_eq σ v1 vl = Some false →
-  {{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (of_val v2) @ E
-  {{{ RET LitV $ LitInt 0; ownP σ }}}.
+Lemma wp_cas_pst E n σ l e1 lit1 lit2 litl :
+  to_val e1 = Some $ LitV lit1 →
+  σ !! l = Some (RSt n, LitV litl) →
+  (lit_eq σ lit1 litl ∨ lit_neq σ lit1 litl) →
+  (lit_eq σ lit1 litl → n = 0%nat) →
+  {{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (Lit lit2) @ E
+  {{{ b, RET LitV $ lit_of_bool b;
+      if b is true then ⌜lit_eq σ lit1 litl⌝ ∗ ownP (<[l:=(RSt 0, LitV lit2)]>σ)
+      else ⌜lit_neq σ lit1 litl⌝ ∗ ownP σ }}}.
 Proof.
-  iIntros (?%of_to_val ???) "HP HΦ". subst.
-  iApply wp_lift_atomic_det_head_step; eauto. by intros; inv_head_step; eauto.
-  iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?". by iApply "HΦ".
-Qed.
-
-Lemma wp_cas_suc_pst E σ l e1 v1 v2 vl :
-  to_val e1 = Some v1 →
-  σ !! l = Some (RSt 0, vl) →
-  value_eq σ v1 vl = Some true →
-  {{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (of_val v2) @ E
-  {{{ RET LitV $ LitInt 1; ownP (<[l:=(RSt 0, v2)]>σ) }}}.
-Proof.
-  iIntros (?%of_to_val ???) "HP HΦ". subst.
-  iApply wp_lift_atomic_det_head_step; eauto. by intros; inv_head_step; eauto.
-  iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?". by iApply "HΦ".
+  iIntros (?%of_to_val ? Hdec Hn ?) "HP HΦ". subst.
+  iApply wp_lift_atomic_head_step; eauto.
+  { destruct Hdec as [Heq|Hneq].
+    - specialize (Hn Heq). subst. do 3 eexists. by eapply CasSucS.
+    - do 3 eexists. by eapply CasFailS. }
+  iFrame. iNext. iIntros (e2 σ2 efs Hs) "Ho".
+  inv_head_step; rewrite big_sepL_nil right_id.
+  - iApply ("HΦ" $! false). eauto.
+  - iApply ("HΦ" $! true). eauto.
+  - exfalso. refine (_ (Hn _)); last done. intros. omega.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
@@ -154,13 +152,27 @@ Proof.
   by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
 Qed.
 
-Lemma wp_bin_op E op l1 l2 l' Φ :
-  bin_op_eval op l1 l2 = Some l' →
-  ▷ (|={E}=> Φ (LitV l')) -∗ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
+Lemma wp_bin_op_heap E σ op l1 l2 l' :
+  bin_op_eval σ op l1 l2 l' →
+  {{{ ▷ ownP σ }}} BinOp op (Lit l1) (Lit l2) @ E
+  {{{ l'', RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ ∗ ownP σ }}}.
+Proof.
+  iIntros (? Φ) "HP HΦ". iApply wp_lift_atomic_head_step; eauto.
+  iFrame "HP". iNext. iIntros (e2 σ2 efs Hs) "Ho". 
+  inv_head_step; rewrite big_sepL_nil right_id.
+  iApply "HΦ". eauto.
+Qed.
+
+Lemma wp_bin_op_pure E op l1 l2 l' :
+  (∀ σ, bin_op_eval σ op l1 l2 l') →
+  {{{ True }}} BinOp op (Lit l1) (Lit l2) @ E
+  {{{ l'' σ, RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ }}}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_pure_det_head_step; eauto.
-  by intros; inv_head_step; eauto.
-  iNext. rewrite big_sepL_nil right_id. iMod "H". by iApply wp_value.
+  iIntros (? Φ) "HΦ". iApply wp_lift_pure_head_step; eauto.
+  { intros. inv_head_step. done. }
+  iNext. iIntros (e2 efs σ Hs). 
+  inv_head_step; rewrite big_sepL_nil right_id.
+  rewrite -wp_value //. iApply "HΦ". eauto.
 Qed.
 
 Lemma wp_case E i e el Φ :
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 719f38bd50dc29696270886fe743092d877986e6..54bf50d14663078b722ef13f49cd89e65982e2a4 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -49,7 +49,7 @@ Notation "'rec:' f [ ] := e" := (Rec f%RustB nil e%E)
   (at level 102, f at level 1, e at level 200) : expr_scope.
 Notation "'rec:' f [ ] := e" := (RecV f%RustB nil e%E)
   (at level 102, f at level 1, e at level 200) : val_scope.
-Notation "e1 +â‚— e2" := (BinOp ProjOp e1%E e2%E)
+Notation "e1 +â‚— e2" := (BinOp OffsetOp e1%E e2%E)
   (at level 50, left associativity) : expr_scope.
 
 (** Derived notions, in order of declaration. The notations for let and seq
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 5d78a388f498bf8ca840e04d2480b507d99dce43..dc94392dab068d3bf2d6ee1b193b7322389e2576 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -5,25 +5,51 @@ From lrust.lang Require Import tactics.
 
 Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
 
+(* This is a crucial definition; if we forget to sync it with head_step,
+   the results proven here are worthless. *)
 Inductive next_access_head : expr → state → access_kind * order → loc → Prop :=
 | Access_read ord l σ :
     next_access_head (Read ord (Lit $ LitLoc l)) σ (ReadAcc, ord) l
 | Access_write ord l e σ :
     is_Some (to_val e) →
     next_access_head (Write ord (Lit $ LitLoc l) e) σ (WriteAcc, ord) l
-| Access_cas_fail l st e1 v1 e2 vl σ :
-    to_val e1 = Some v1 → is_Some (to_val e2) →  v1 ≠ vl →
-    σ !! l = Some (st, vl) →
+| Access_cas_fail l st e1 lit1 e2 lit2 litl σ :
+    to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
+    lit_neq σ lit1 litl → σ !! l = Some (st, LitV litl) →
     next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (ReadAcc, ScOrd) l
-| Access_cas_suc l st e1 v1 e2 v2 σ :
-    to_val e1 = Some v1 → to_val e2 = Some v2 →
-    σ !! l = Some (st, v1) →
+| Access_cas_suc l st e1 lit1 e2 lit2 litl σ :
+    to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
+    lit_eq σ lit1 litl → σ !! l = Some (st, LitV litl) →
     next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (WriteAcc, ScOrd) l
 | Access_free n l σ i :
     0 ≤ i < n →
     next_access_head (Free (Lit $ LitInt n) (Lit $ LitLoc l))
                      σ (FreeAcc, Na2Ord) (shift_loc l i).
 
+(* Some sanity checks to make sure the definition above is not entirely insensible. *)
+Goal ∀ e1 e2 e3 σ, head_reducible (CAS e1 e2 e3) σ →
+                   ∃ a l, next_access_head (CAS e1 e2 e3) σ a l.
+Proof.
+  intros ??? σ (?&?&?&?). inversion H; do 2 eexists;
+    (eapply Access_cas_fail; done) || eapply Access_cas_suc; done.
+Qed.
+Goal ∀ o e σ, head_reducible (Read o e) σ →
+              ∃ a l, next_access_head (Read o e) σ a l.
+Proof.
+  intros ?? σ (?&?&?&?). inversion H; do 2 eexists; eapply Access_read; done.
+Qed.
+Goal ∀ o e1 e2 σ, head_reducible (Write o e1 e2) σ →
+              ∃ a l, next_access_head (Write o e1 e2) σ a l.
+Proof.
+  intros ??? σ (?&?&?&?). inversion H; do 2 eexists;
+    eapply Access_write; try done; eexists; done.
+Qed.
+Goal ∀ e1 e2 σ, head_reducible (Free e1 e2) σ →
+              ∃ a l, next_access_head (Free e1 e2) σ a l.
+Proof.
+  intros ?? σ (?&?&?&?). inversion H; do 2 eexists; eapply Access_free; done.
+Qed.
+
 Definition next_access_thread (e: expr) (σ : state)
            (a : access_kind * order) (l : loc) : Prop :=
   ∃ K e', next_access_head e' σ a l ∧ e = fill K e'.
@@ -53,18 +79,20 @@ Qed.
 Lemma next_access_head_reductible_ctx e σ σ' a l K :
   next_access_head e σ' a l → reducible (fill K e) σ → head_reducible e σ.
 Proof.
-  intros Ha (e'&σ''&ef&Hstep). assert (to_val e = None). by destruct Ha.
-  change fill with ectx_language.fill in Hstep.
-  apply fill_step_inv in Hstep; last done. destruct Hstep as (e2'&_&Hstep).
-  clear K. destruct Hstep as [K e1' e2'' ?? Hstep]. subst. destruct K as [|K0 K].
-    by unfold head_reducible; eauto.
-  exfalso. simpl in Ha. apply next_access_head_head in Ha.
-  change to_val with ectxi_language.to_val in Ha.
-  rewrite fill_not_val in Ha. by eapply is_Some_None. by eapply val_stuck.
+  intros Ha. apply step_is_head.
+  - by destruct Ha.
+  - clear -Ha. intros Ki K e' Heq (?&?&?&Hstep).
+    subst e. apply next_access_head_head in Ha.
+    change to_val with ectxi_language.to_val in Ha.
+    rewrite fill_not_val in Ha. by eapply is_Some_None. by eapply val_stuck.
 Qed.
 
+Definition head_reduce_not_to_stuck e σ :=
+  ∀ e' σ' efs, ectx_language.head_step e σ e' σ' efs → e' ≠ App (Lit $ LitInt 0) [].
+
 Lemma next_access_head_reducible_state e σ a l :
   next_access_head e σ a l → head_reducible e σ →
+  head_reduce_not_to_stuck e σ →
   match a with
   | (ReadAcc, ScOrd | Na1Ord) => ∃ v n, σ !! l = Some (RSt n, v)
   | (ReadAcc, Na2Ord) => ∃ v n, σ !! l = Some (RSt (S n), v)
@@ -73,11 +101,14 @@ Lemma next_access_head_reducible_state e σ a l :
   | (FreeAcc, _) => ∃ v ls, σ !! l = Some (ls, v)
   end.
 Proof.
-  assert (Hrefl : ∀ v, value_eq σ v v ≠ Some false).
-  by destruct v as [[]|]=>//=; rewrite bool_decide_true.
-  intros Ha (e'&σ'&ef&Hstep). destruct Ha; inv_head_step; eauto.
-  by edestruct Hrefl.
-  match goal with H : ∀ m, _ |- _ => destruct (H i) as [_ [[]?]] end; eauto.
+(*  assert (Hrefl : ∀ l, ~lit_neq σ l l).
+    { intros ? Hneq. inversion Hneq; done. } *)
+  intros Ha (e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_head_step; eauto.
+  - destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
+    eapply CasStuckS; done.
+  - exfalso. eapply Hrednonstuck; last done.
+    eapply CasStuckS; done.
+  - match goal with H : ∀ m, _ |- _ => destruct (H i) as [_ [[]?]] end; eauto.
 Qed.
 
 Lemma next_access_head_Na1Ord_step e1 e2 ef σ1 σ2 a l :
@@ -96,7 +127,20 @@ Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' a1 a2 l :
   next_access_head e2 σ' a2 l.
 Proof.
   intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_head_step;
-  destruct Ha2; simplify_eq; econstructor; eauto; apply lookup_insert.
+  destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
+  (* Oh my. FIXME RJ. *)
+  - eapply lit_neq_state; last done.
+    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+  - eapply lit_eq_state; last done.
+    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+  - eapply lit_neq_state; last done.
+    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+  - eapply lit_eq_state; last done.
+    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
 Qed.
 
 Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' o1 a2 l :
@@ -121,6 +165,38 @@ Proof.
   eapply (@is_Some_None (lock_state * val)). rewrite -FREE'. naive_solver.
 Qed.
 
+Lemma safe_step_not_reduce_to_stuck el σ K e e' σ' ef :
+  (∀ el' σ' e', rtc step (el, σ) (el', σ') →
+                e' ∈ el' → to_val e' = None → reducible e' σ') →
+  fill K e ∈ el → head_step e σ e' σ' ef → head_reduce_not_to_stuck e' σ'.
+Proof.
+  intros Hsafe Hi Hstep e1 σ1 ? Hstep1 Hstuck.
+  cut (reducible (fill K e1) σ1).
+  { subst. intros (?&?&?&?). eapply stuck_irreducible. done. }
+  destruct (elem_of_list_split _ _ Hi) as (?&?&->).
+  eapply Hsafe; last by (apply: fill_not_val; subst).
+  - eapply rtc_l, rtc_l, rtc_refl.
+    + econstructor. done. done. econstructor; done.
+    + econstructor. done. done. econstructor; done.
+  - subst. set_solver+.
+Qed.
+
+(* TODO: Unify this and the above. *)
+Lemma safe_not_reduce_to_stuck el σ K e :
+  (∀ el' σ' e', rtc step (el, σ) (el', σ') →
+                e' ∈ el' → to_val e' = None → reducible e' σ') →
+  fill K e ∈ el → head_reduce_not_to_stuck e σ.
+Proof.
+  intros Hsafe Hi e1 σ1 ? Hstep1 Hstuck.
+  cut (reducible (fill K e1) σ1).
+  { subst. intros (?&?&?&?). eapply stuck_irreducible. done. }
+  destruct (elem_of_list_split _ _ Hi) as (?&?&->).
+  eapply Hsafe; last by (apply: fill_not_val; subst).
+  - eapply rtc_l, rtc_refl.
+    + econstructor. done. done. econstructor; done.
+  - subst. set_solver+.
+Qed.
+
 Theorem safe_nonracing el σ :
   (∀ el' σ' e', rtc step (el, σ) (el', σ') →
                 e' ∈ el' → to_val e' = None → reducible e' σ') →
@@ -132,9 +208,11 @@ Proof.
   assert (to_val e1 = None). by destruct Ha1.
   assert (Hrede1:head_reducible e1 σ).
   { eapply (next_access_head_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
-    set_solver. }
-  assert (Hσe1:=next_access_head_reducible_state _ _ _ _ Ha1 Hrede1).
-  destruct Hrede1 as (e1'&σ1'&ef1&Hstep1).
+    abstract set_solver. }
+  assert (Hnse1:head_reduce_not_to_stuck e1 σ).
+  { eapply safe_not_reduce_to_stuck with (K:=K1); first done. set_solver+. }
+  assert (Hσe1:=next_access_head_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
+  destruct Hrede1 as (e1'&σ1'&ef1&Hstep1). clear Hnse1.
   assert (Ha1' : a1.2 = Na1Ord → next_access_head e1' σ1' (a1.1, Na2Ord) l).
   { intros. eapply next_access_head_Na1Ord_step, Hstep1.
     by destruct a1; simpl in *; subst. }
@@ -147,13 +225,17 @@ Proof.
   { destruct a1 as [a1 []]=>// _.
     eapply (next_access_head_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
            fill_not_val=>//.
-    by auto. set_solver. by destruct Hstep1; inversion Ha1. }
+    by auto. abstract set_solver. by destruct Hstep1; inversion Ha1. }
+  assert (Hnse1: head_reduce_not_to_stuck e1' σ1').
+  { eapply safe_step_not_reduce_to_stuck with (K:=K1); first done; last done. set_solver+. }
 
   assert (to_val e2 = None). by destruct Ha2.
   assert (Hrede2:head_reducible e2 σ).
   { eapply (next_access_head_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
-    set_solver. }
-  assert (Hσe2:=next_access_head_reducible_state _ _ _ _ Ha2 Hrede2).
+    abstract set_solver. }
+  assert (Hnse2:head_reduce_not_to_stuck e2 σ).
+  { eapply safe_not_reduce_to_stuck with (K:=K2); first done. set_solver+. }
+  assert (Hσe2:=next_access_head_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
   destruct Hrede2 as (e2'&σ2'&ef2&Hstep2).
   assert (Ha2' : a2.2 = Na1Ord → next_access_head e2' σ2' (a2.1, Na2Ord) l).
   { intros. eapply next_access_head_Na1Ord_step, Hstep2.
@@ -167,30 +249,39 @@ Proof.
   { destruct a2 as [a2 []]=>// _.
     eapply (next_access_head_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
            fill_not_val=>//.
-    by auto. set_solver. by destruct Hstep2; inversion Ha2. }
-
+    by auto. abstract set_solver. by destruct Hstep2; inversion Ha2. }
+  assert (Hnse2':head_reduce_not_to_stuck e2' σ2').
+  { eapply safe_step_not_reduce_to_stuck with (K:=K2); first done; last done. set_solver+. }
 
   assert (Ha1'2 : a1.2 = Na1Ord → next_access_head e2 σ1' a2 l).
   { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
     by rewrite <-HNa, <-surjective_pairing. }
   assert (Hrede1_2: head_reducible e2 σ1').
   { intros. eapply (next_access_head_reductible_ctx e2 σ1' σ  a2 l K2), Hsafe, fill_not_val=>//.
-    set_solver. }
+    abstract set_solver. }
+  assert (Hnse1_2:head_reduce_not_to_stuck e2 σ1').
+  { eapply safe_not_reduce_to_stuck with (K:=K2).
+    - intros. eapply Hsafe. etrans; last done. done. done. done.
+    - set_solver+. }
   assert (Hσe1'1:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord)).
+    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
   assert (Hσe1'2:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2).
+    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
 
   assert (Ha2'1 : a2.2 = Na1Ord → next_access_head e1 σ2' a1 l).
   { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
     by rewrite <-HNa, <-surjective_pairing. }
   assert (Hrede2_1: head_reducible e1 σ2').
   { intros. eapply (next_access_head_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
-    set_solver. }
+    abstract set_solver. }
+  assert (Hnse2_1:head_reduce_not_to_stuck e1 σ2').
+  { eapply safe_not_reduce_to_stuck with (K:=K1).
+    - intros. eapply Hsafe. etrans; last done. done. done. done.
+    - set_solver+. }
   assert (Hσe2'1:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1).
+    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
   assert (Hσe2'2:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord)).
+    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord) Hnse2').
 
   assert (a1.1 = FreeAcc → False).
   { destruct a1 as [[]?]; inversion 1.
@@ -207,7 +298,7 @@ Proof.
     end;
     try congruence.
 
-  clear e2' Hstep2 σ2' Hrtc_step2 Hrede2_1. destruct Hrede1_2 as (e2'&σ'&ef&?).
+  clear e2' Hnse2' Hnse2_1 Hstep2 σ2' Hrtc_step2 Hrede2_1. destruct Hrede1_2 as (e2'&σ'&ef&?).
   inv_head_step.
   match goal with
   | H : <[l:=_]> σ !! l = _ |- _ => by rewrite lookup_insert in H
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 21e3309ba8c83e4f188836669ef099d0fa920f04..d19ef64ec38354f32f8463b3343962897b31b6b4 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -155,7 +155,8 @@ Proof.
   intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef.
     destruct e; simpl; try done; repeat (case_match; try done);
-    inversion 1; rewrite ?to_of_val; naive_solver eauto.
+    inversion 1; try (apply val_irreducible; rewrite ?language.to_of_val; naive_solver eauto); [].
+    rewrite -[stuck_term](fill_empty). apply stuck_irreducible.
   - intros [|Ki K] e' Hfill Hnotval; [done|exfalso].
     apply (fill_not_val K), eq_None_not_Some in Hnotval. apply Hnotval. simpl.
     revert He. destruct e; simpl; try done; repeat (case_match; try done);
diff --git a/theories/lang/wp_tactics.v b/theories/lang/wp_tactics.v
index 0d136c4826ebfb35ab5c9157f5e0521b5bd3dd5d..12d8f8ca3265b674682c4a0340c1f59d27583d73 100644
--- a/theories/lang/wp_tactics.v
+++ b/theories/lang/wp_tactics.v
@@ -85,8 +85,12 @@ Tactic Notation "wp_op" :=
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
-    | BinOp _ _ _ =>
-       wp_bind_core K; etrans; [|eapply wp_bin_op; try fast_done]; wp_finish
+    | BinOp OffsetOp _ _ =>
+       wp_bind_core K; etrans; [|eapply wp_offset; try fast_done]; wp_finish
+    | BinOp PlusOp _ _ =>
+       wp_bind_core K; etrans; [|eapply wp_plus; try fast_done]; wp_finish
+    | BinOp MinusOp _ _ =>
+       wp_bind_core K; etrans; [|eapply wp_minus; try fast_done]; wp_finish
     end) || fail "wp_op: cannot find 'BinOp' in" e
   | _ => fail "wp_op: not a 'wp'"
   end.
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 7d658cfc03efeb63c7c1c3c42f4a0c5537b20511..664a6c6f444e2abb223ead396bc8708df80ffdc2 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 
 Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
-           (κ : lft) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
+           (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
 Notation "&na{ κ , tid , N } P" := (na_bor κ tid N P)
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N } P" := (na_bor κ tid N P)
 
 Section na_bor.
   Context `{invG Σ, lftG Σ, na_invG Σ}
-          (tid : thread_id) (N : namespace) (P : iProp Σ).
+          (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
 
   Global Instance na_bor_persistent κ : PersistentP (&na{κ,tid,N} P) := _.
   Global Instance na_bor_proper κ :
diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index e44f9e1687b516a06847a37ede361b9ae42ef882..e7effc6e8b8ca4d066a0792de0602d314aee8287 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -6,11 +6,11 @@ From lrust.lifetime Require Import borrow frac_borrow.
 Section perm.
   Context `{iris_typeG Σ}.
 
-  Definition perm {Σ} := thread_id → iProp Σ.
+  Definition perm {Σ} := na_inv_pool_name → iProp Σ.
 
   Fixpoint eval_expr (ν : expr) : option val :=
     match ν with
-    | BinOp ProjOp e (Lit (LitInt n)) =>
+    | BinOp OffsetOp e (Lit (LitInt n)) =>
       match eval_expr e with
       | Some (#(LitLoc l)) => Some (#(shift_loc l n))
       | _ => None
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 32990b8dcbe93e19e09e9bcfc21227b58663d76d..873d26289fd2d670dba9795c02a9eb155440ff78 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -17,8 +17,8 @@ Section type.
 
   Record type :=
     { ty_size : nat;
-      ty_own : thread_id → list val → iProp Σ;
-      ty_shr : lft → thread_id → coPset → loc → iProp Σ;
+      ty_own : na_inv_pool_name → list val → iProp Σ;
+      ty_shr : lft → na_inv_pool_name → coPset → loc → iProp Σ;
 
       ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
 
@@ -54,7 +54,7 @@ Section type.
      bellow will not be acceptable by Coq. *)
   Record simple_type `{iris_typeG Σ} :=
     { st_size : nat;
-      st_own : thread_id → list val → iProp Σ;
+      st_own : na_inv_pool_name → list val → iProp Σ;
 
       st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = st_size⌝;
       st_own_persistent tid vl : PersistentP (st_own tid vl) }.