From adec152c8dbf61363763140563285dd15590b364 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 31 Jul 2017 19:16:19 +0200
Subject: [PATCH] Notation for shift_loc (finally \!).

---
 theories/lang/heap.v                          | 35 ++++++++--------
 theories/lang/lang.v                          | 32 +++++++-------
 theories/lang/lib/arc.v                       | 32 +++++++-------
 theories/lang/lib/new_delete.v                |  2 +-
 theories/lang/lib/spawn.v                     |  4 +-
 theories/lang/lifting.v                       |  2 +-
 theories/lang/notation.v                      |  4 +-
 theories/lang/races.v                         |  4 +-
 theories/typing/lib/arc.v                     | 18 ++++----
 theories/typing/lib/mutex/mutex.v             |  8 ++--
 theories/typing/lib/mutex/mutexguard.v        |  8 ++--
 theories/typing/lib/rc/rc.v                   | 42 +++++++++----------
 theories/typing/lib/rc/weak.v                 |  8 ++--
 theories/typing/lib/refcell/ref_code.v        |  4 +-
 theories/typing/lib/refcell/refcell.v         | 12 +++---
 theories/typing/lib/refcell/refcell_code.v    |  6 +--
 theories/typing/lib/rwlock/rwlock.v           | 12 +++---
 theories/typing/lib/rwlock/rwlock_code.v      |  6 +--
 theories/typing/lib/rwlock/rwlockreadguard.v  |  4 +-
 .../typing/lib/rwlock/rwlockreadguard_code.v  |  2 +-
 theories/typing/lib/rwlock/rwlockwriteguard.v |  4 +-
 .../typing/lib/rwlock/rwlockwriteguard_code.v |  4 +-
 theories/typing/own.v                         |  2 +-
 theories/typing/product.v                     |  6 +--
 theories/typing/sum.v                         | 10 ++---
 theories/typing/type.v                        |  8 ++--
 theories/typing/type_context.v                |  2 +-
 theories/typing/type_sum.v                    |  2 +-
 28 files changed, 143 insertions(+), 140 deletions(-)

diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 58df7d54..6523f643 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -48,7 +48,7 @@ Section definitions.
     seal_eq heap_mapsto_aux.
 
   Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
-    ([∗ list] i ↦ v ∈ vl, heap_mapsto (shift_loc l i) q v)%I.
+    ([∗ list] i ↦ v ∈ vl, heap_mapsto (l +ₗ i) q v)%I.
 
   Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitC) :=
     match n with O => ∅ | S n => <[i0 := Excl ()]>(inter (i0+1) n) end.
@@ -150,7 +150,7 @@ Section heap.
   Proof. by rewrite /heap_mapsto_vec. Qed.
 
   Lemma heap_mapsto_vec_app l q vl1 vl2 :
-    l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ shift_loc l (length vl1) ↦∗{q} vl2.
+    l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ (l +ₗ length vl1) ↦∗{q} vl2.
   Proof.
     rewrite /heap_mapsto_vec big_sepL_app.
     do 2 f_equiv. intros k v. by rewrite shift_loc_assoc_nat.
@@ -160,7 +160,7 @@ Section heap.
   Proof. by rewrite /heap_mapsto_vec /= shift_loc_0 right_id. Qed.
 
   Lemma heap_mapsto_vec_cons l q v vl:
-    l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ shift_loc l 1 ↦∗{q} vl.
+    l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vl.
   Proof.
     by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
   Qed.
@@ -173,7 +173,7 @@ Section heap.
     - revert l. induction Hlen as [|v1 v2 vl1 vl2 _ _ IH]=> l.
       { rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
       rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
-      iDestruct (IH (shift_loc l 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
+      iDestruct (IH (l +â‚— 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
       rewrite (inj_iff (:: vl2)).
       iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
       iSplit; first done. iFrame.
@@ -212,7 +212,7 @@ Section heap.
   Lemma heap_mapsto_vec_combine l q vl :
     vl ≠ [] →
     l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl,
-      {[shift_loc l i := (q, Cinr 0%nat, to_agree v)]}).
+      {[l +â‚— i := (q, Cinr 0%nat, to_agree v)]}).
   Proof.
     rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
     by rewrite (big_opL_commute (Auth None)) big_opL_commute1 //.
@@ -269,7 +269,7 @@ Section heap.
   Proof. revert i. induction n as [|n IH]=>i. done. by apply insert_valid. Qed.
 
   Lemma heap_freeable_op_eq l q1 q2 n n' :
-    †{q1}l…n ∗ †{q2}shift_loc l n…n' ⊣⊢ †{q1+q2}l…(n+n').
+    †{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
   Proof.
     by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
       op_singleton pair_op inter_op.
@@ -277,7 +277,7 @@ Section heap.
 
   (** Properties about heap_freeable_rel and heap_freeable *)
   Lemma heap_freeable_rel_None σ l hF :
-    (∀ m : Z, σ !! shift_loc l m = None) → heap_freeable_rel σ hF →
+    (∀ m : Z, σ !! (l +ₗ m) = None) → heap_freeable_rel σ hF →
     hF !! l.1 = None.
   Proof.
     intros FRESH REL. apply eq_None_not_Some. intros [[q s] [Hsne REL']%REL].
@@ -288,7 +288,7 @@ Section heap.
   Lemma heap_freeable_is_Some σ hF l n i :
     heap_freeable_rel σ hF →
     hF !! l.1 = Some (1%Qp, inter (l.2) n) →
-    is_Some (σ !! shift_loc l i) ↔ 0 ≤ i ∧ i < n.
+    is_Some (σ !! (l +ₗ i)) ↔ 0 ≤ i ∧ i < n.
   Proof.
     destruct l as [b j]; rewrite /shift_loc /=. intros REL Hl.
     destruct (REL b (1%Qp, inter j n)) as [_ ->]; simpl in *; auto.
@@ -299,7 +299,7 @@ Section heap.
 
   Lemma heap_freeable_rel_init_mem l h vl σ:
     vl ≠ [] →
-    (∀ m : Z, σ !! shift_loc l m = None) →
+    (∀ m : Z, σ !! (l +ₗ m) = None) →
     heap_freeable_rel σ h →
     heap_freeable_rel (init_mem l vl σ)
                       (<[l.1 := (1%Qp, inter (l.2) (length vl))]> h).
@@ -311,8 +311,7 @@ Section heap.
       + rewrite inter_lookup_Some //.
         destruct (lookup_init_mem_Some σ l (l.1, i) vl); naive_solver.
       + rewrite inter_lookup_None; last lia. rewrite lookup_init_mem_ne /=; last lia.
-        replace (l.1,i) with (shift_loc l (i - l.2))
-          by (rewrite /shift_loc; f_equal; lia).
+        replace (l.1,i) with (l +â‚— (i - l.2)) by (rewrite /shift_loc; f_equal; lia).
         by rewrite FRESH !is_Some_alt.
     - destruct (REL blk qs) as [? Hs]; auto.
       split; [done|]=> i. by rewrite -Hs lookup_init_mem_ne; last auto.
@@ -339,16 +338,16 @@ Section heap.
 
   (** Weakest precondition *)
   Lemma heap_alloc_vs σ l vl :
-    (∀ m : Z, σ !! shift_loc l m = None) →
+    (∀ m : Z, σ !! (l +ₗ m) = None) →
     own heap_name (● to_heap σ)
     ==∗ own heap_name (● to_heap (init_mem l vl σ))
        ∗ own heap_name (◯ [^op list] i ↦ v ∈ vl,
-           {[shift_loc l i := (1%Qp, Cinr 0%nat, to_agree v)]}).
+           {[l +â‚— i := (1%Qp, Cinr 0%nat, to_agree v)]}).
   Proof.
     intros FREE. rewrite -own_op. apply own_update, auth_update_alloc.
     revert l FREE. induction vl as [|v vl IH]=> l FRESH; [done|].
     rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=.
-    etrans; first apply (IH (shift_loc l 1)).
+    etrans; first apply (IH (l +â‚— 1)).
     { intros. by rewrite shift_loc_assoc. }
     rewrite shift_loc_0 -insert_singleton_op; last first.
     { rewrite -equiv_None big_opL_commute equiv_None big_opL_None=> l' v' ?.
@@ -360,7 +359,7 @@ Section heap.
 
   Lemma heap_alloc σ l n vl :
     0 < n →
-    (∀ m, σ !! shift_loc l m = None) →
+    (∀ m, σ !! (l +ₗ m) = None) →
     Z.of_nat (length vl) = n →
     heap_ctx σ ==∗
       heap_ctx (init_mem l vl σ) ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl.
@@ -382,7 +381,7 @@ Section heap.
 
   Lemma heap_free_vs σ l vl :
     own heap_name (● to_heap σ) ∗ own heap_name (◯ [^op list] i ↦ v ∈ vl,
-      {[shift_loc l i := (1%Qp, Cinr 0%nat, to_agree v)]})
+      {[l +â‚— i := (1%Qp, Cinr 0%nat, to_agree v)]})
     ==∗ own heap_name (● to_heap (free_mem l (length vl) σ)).
   Proof.
     rewrite -own_op. apply own_update, auth_update_dealloc.
@@ -390,7 +389,7 @@ Section heap.
     rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /= shift_loc_0.
     apply local_update_total_valid=> _ Hvalid _.
     assert (([^op list] k↦y ∈ vl,
-      {[shift_loc l (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None).
+      {[l +â‚— (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None).
     { move: (Hvalid l). rewrite lookup_op lookup_singleton.
       by move=> /(cmra_discrete_valid_iff 0) /exclusiveN_Some_l. }
     rewrite -insert_singleton_op //. etrans.
@@ -403,7 +402,7 @@ Section heap.
   Lemma heap_free σ l vl (n : Z) :
     n = length vl →
     heap_ctx σ -∗ l ↦∗ vl -∗ †l…(length vl)
-    ==∗ ⌜0 < n⌝ ∗ ⌜∀ m, is_Some (σ !! (shift_loc l m)) ↔ (0 ≤ m < n)⌝ ∗
+    ==∗ ⌜0 < n⌝ ∗ ⌜∀ m, is_Some (σ !! (l +ₗ m)) ↔ (0 ≤ m < n)⌝ ∗
         heap_ctx (free_mem l (Z.to_nat n) σ).
   Proof.
     iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 6cf3ef52..14520ff7 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -9,6 +9,10 @@ Open Scope Z_scope.
 Definition block : Set := positive.
 Definition loc : Set := block * Z.
 
+Bind Scope loc_scope with loc.
+Delimit Scope loc_scope with L.
+Open Scope loc_scope.
+
 Inductive base_lit : Set :=
 | LitUnit | LitLoc (l : loc) | LitInt (n : Z).
 Inductive bin_op : Set :=
@@ -194,16 +198,18 @@ Definition lit_of_bool (b : bool) : base_lit :=
 
 Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
 
+Notation "l +â‚— z" := (shift_loc l%L z%Z) (at level 50, left associativity).
+
 Fixpoint init_mem (l:loc) (init:list val) (σ:state) : state :=
   match init with
   | [] => σ
-  | inith :: initq => <[l:=(RSt 0, inith)]>(init_mem (shift_loc l 1) initq σ)
+  | inith :: initq => <[l:=(RSt 0, inith)]>(init_mem (l +ₗ 1) initq σ)
   end.
 
 Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
   match n with
   | O => σ
-  | S n => delete l (free_mem (shift_loc l 1) n σ)
+  | S n => delete l (free_mem (l +ₗ 1) n σ)
   end.
 
 Inductive lit_eq (σ : state) : base_lit → base_lit → Prop :=
@@ -238,7 +244,7 @@ Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_l
 | 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).
+    bin_op_eval σ OffsetOp (LitLoc l) (LitInt z) (LitLoc $ l +ₗ z).
 
 Definition stuck_term := App (Lit $ LitInt 0) [].
 
@@ -303,13 +309,13 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
               []
 | AllocS n l init σ :
     0 < n →
-    (∀ m, σ !! shift_loc l m = None) →
+    (∀ m, σ !! (l +ₗ m) = None) →
     Z.of_nat (length init) = n →
     head_step (Alloc $ Lit $ LitInt n) σ
               (Lit $ LitLoc l) (init_mem l init σ) []
 | FreeS n l σ :
     0 < n →
-    (∀ m, is_Some (σ !! shift_loc l m) ↔ 0 ≤ m < n) →
+    (∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) →
     head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
               (Lit LitUnit) (free_mem l (Z.to_nat n) σ)
               []
@@ -377,22 +383,20 @@ Proof.
   destruct (list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2); auto. congruence.
 Qed.
 
-Lemma shift_loc_assoc l n n' :
-  shift_loc (shift_loc l n) n' = shift_loc l (n+n').
+Lemma shift_loc_assoc l n n' : l +â‚— n +â‚— n' = l +â‚— (n + n').
 Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
-Lemma shift_loc_0 l : shift_loc l 0 = l.
+Lemma shift_loc_0 l : l +â‚— 0 = l.
 Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
 
-Lemma shift_loc_assoc_nat l (n n' : nat) :
-  shift_loc (shift_loc l n) n' = shift_loc l (n+n')%nat.
+Lemma shift_loc_assoc_nat l (n n' : nat) : l +â‚— n +â‚— n' = l +â‚— (n + n')%nat.
 Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
-Lemma shift_loc_0_nat l : shift_loc l 0%nat = l.
+Lemma shift_loc_0_nat l : l +â‚— 0%nat = l.
 Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
 
 Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
 Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
 
-Lemma shift_loc_block l n : (shift_loc l n).1 = l.1.
+Lemma shift_loc_block l n : (l +â‚— n).1 = l.1.
 Proof. done. Qed.
 
 Lemma lookup_init_mem σ (l l' : loc) vl :
@@ -424,7 +428,7 @@ Lemma lookup_init_mem_ne σ (l l' : loc) vl :
   init_mem l vl σ !! l' = σ !! l'.
 Proof.
   revert l. induction vl as [|v vl IH]=> /= l Hl; auto.
-  rewrite -(IH (shift_loc l 1)); last (simpl; intuition lia).
+  rewrite -(IH (l +â‚— 1)); last (simpl; intuition lia).
   apply lookup_insert_ne. intros ->; intuition lia.
 Qed.
 
@@ -633,6 +637,6 @@ Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
 Notation SeqCtx e2 := (LetCtx BAnon e2).
 Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
 Coercion lit_of_bool : bool >-> base_lit.
-Notation If e0 e1 e2 := (Case e0 [e2;e1]).
+Notation If e0 e1 e2 := (Case e0 (@cons expr e2 (@cons expr e1 (@nil expr)))).
 Notation Newlft := (Lit LitUnit) (only parsing).
 Notation Endlft := Skip (only parsing).
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 0baed576..16613046 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -130,12 +130,12 @@ Section def.
       match st with
       | (Some (Cinl (q, strong, wlock)), weak) =>
          ∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ P1 q' ∗ l ↦ #(Zpos strong) ∗
-           if wlock then shift_loc l 1 ↦ #(-1) ∗ ⌜weak = 0%nat⌝
-           else shift_loc l 1 ↦ #(S weak)
+           if wlock then (l +ₗ 1) ↦ #(-1) ∗ ⌜weak = 0%nat⌝
+           else (l +ₗ 1) ↦ #(S weak)
       | (Some (Cinr _), weak) =>
-        l ↦ #0 ∗ shift_loc l 1 ↦ #(S weak)
+        l ↦ #0 ∗ (l +ₗ 1) ↦ #(S weak)
       | (None, (S _) as weak) =>
-        l ↦ #0 ∗ shift_loc l 1 ↦ #weak ∗ P2
+        l ↦ #0 ∗ (l +ₗ 1) ↦ #weak ∗ P2
       | _ => True
       end)%I.
 
@@ -183,7 +183,7 @@ Section arc.
   Proof. solve_proper. Qed.
 
   Lemma create_arc E l :
-    l ↦ #1 -∗ shift_loc l 1 ↦ #1 -∗ P1 1%Qp ={E}=∗
+    l ↦ #1 -∗ (l +ₗ 1) ↦ #1 -∗ P1 1%Qp ={E}=∗
       ∃ γ q, is_arc P1 P2 N γ l ∗ P1 q ∗ arc_tok γ q.
   Proof using HP1.
     iIntros "Hl1 Hl2 [HP1 HP1']".
@@ -195,7 +195,7 @@ Section arc.
   Qed.
 
   Lemma create_weak E l :
-    l ↦ #0 -∗ shift_loc l 1 ↦ #1 -∗ P2 ={E}=∗ ∃ γ, is_arc P1 P2 N γ l ∗ weak_tok γ.
+    l ↦ #0 -∗ (l +ₗ 1) ↦ #1 -∗ P2 ={E}=∗ ∃ γ, is_arc P1 P2 N γ l ∗ weak_tok γ.
   Proof.
     iIntros "Hl1 Hl2 HP2".
     iMod (own_alloc ((● (None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H● H◯]"; first done.
@@ -345,9 +345,9 @@ Section arc.
     {{{ P }}} clone_weak [ #l] {{{ RET #(); P ∗ weak_tok γ }}}.
   Proof.
     iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
-    iAssert (□ (P ={⊤,⊤∖↑N}=∗ ∃ w : Z, shift_loc l 1 ↦ #w ∗
-              (shift_loc l 1 ↦ #(w + 1) ={⊤∖↑N,⊤}=∗ P ∗ weak_tok γ) ∧
-              (shift_loc l 1 ↦ #w ={⊤∖↑N,⊤}=∗ P)))%I as "#Hproto".
+    iAssert (□ (P ={⊤,⊤∖↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
+              ((l +ₗ 1) ↦ #(w + 1) ={⊤∖↑N,⊤}=∗ P ∗ weak_tok γ) ∧
+              ((l +ₗ 1) ↦ #w ={⊤∖↑N,⊤}=∗ P)))%I as "#Hproto".
     { iIntros "!# HP". iInv N as (st) "[>H● H]" "Hclose1".
       iMod ("Hacc" with "HP") as "[Hown Hclose2]".
       iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
@@ -437,13 +437,13 @@ Section arc.
   Lemma drop_weak_spec (γ : gname) (l : loc) :
     is_arc P1 P2 N γ l -∗
     {{{ weak_tok γ }}} drop_weak [ #l]
-    {{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ shift_loc l 1 ↦ #0 else True }}}.
+    {{{ (b : bool), RET #b ; if b then P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0 else True }}}.
   Proof.
     iIntros "#INV !# * Hown HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
-    iAssert (□ (weak_tok γ ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, shift_loc l 1 ↦ #w ∗
-              (shift_loc l 1 ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠ 1⌝ ∨
-               ▷ P2 ∗ l ↦ #0 ∗ shift_loc l 1 ↦ #0) ∧
-              (shift_loc l 1 ↦ #w ={⊤ ∖ ↑N,⊤}=∗ weak_tok γ)))%I as "#Hproto".
+    iAssert (□ (weak_tok γ ={⊤,⊤ ∖ ↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
+              ((l +ₗ 1) ↦ #(w - 1) ={⊤ ∖ ↑N,⊤}=∗ ⌜w ≠ 1⌝ ∨
+               ▷ P2 ∗ l ↦ #0 ∗ (l +ₗ 1) ↦ #0) ∧
+              ((l +ₗ 1) ↦ #w ={⊤ ∖ ↑N,⊤}=∗ weak_tok γ)))%I as "#Hproto".
     { iIntros "!# Hown". iInv N as (st) "[>H● H]" "Hclose1".
       iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
       destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..].
@@ -565,7 +565,7 @@ Section arc.
     is_arc P1 P2 N γ l -∗
     {{{ arc_tok γ q ∗ P1 q }}} is_unique [ #l]
     {{{ (b : bool), RET #b ;
-        if b then l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ P1 1
+        if b then l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ P1 1
         else arc_tok γ q ∗ P1 q }}}.
   Proof using HP1.
     iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _). wp_op.
@@ -627,7 +627,7 @@ Section arc.
     {{{ (x : fin 3), RET #x ;
         match x : nat with
         (* No other reference : we get everything. *)
-        | 0%nat => l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ P1 1
+        | 0%nat => l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ P1 1
         (* No other strong, but there are weaks : we get P1,
            plus the option to get a weak if we pay P2. *)
         | 1%nat => P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ)
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index c78267bc..dfe6bc79 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -45,5 +45,5 @@ Notation "'letalloc:' x <- e1 'in' e2" :=
   ((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
   (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
 Notation "'letalloc:' x <-{ n } ! e1 'in' e2" :=
-  ((Lam (@cons binder x%E%E%E nil) (x <-{n%Z%V} !e1 ;; e2)) [new [ #n]])%E
+  ((Lam (@cons binder x%E%E%E nil) (x <-{n%Z%V%L} !e1 ;; e2)) [new [ #n]])%E
   (at level 102, x at level 1, e1, e2 at level 150) : expr_scope.
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 2716c48b..34a1ef52 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -41,10 +41,10 @@ Context `{!lrustG Σ, !spawnG Σ} (N : namespace).
 Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (own γf (Excl ()) ∗ own γj (Excl ()) ∨
    ∃ b, c ↦ #(lit_of_bool b) ∗
-        if b then ∃ v, shift_loc c 1 ↦ v ∗ Ψ v ∗ own γf (Excl ()) else True)%I.
+        if b then ∃ v, (c +ₗ 1) ↦ v ∗ Ψ v ∗ own γf (Excl ()) else True)%I.
 
 Definition finish_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
-  (∃ γf γj v, own γf (Excl ()) ∗ shift_loc c 1 ↦ v ∗ inv N (spawn_inv γf γj c Ψ))%I.
+  (∃ γf γj v, own γf (Excl ()) ∗ (c +ₗ 1) ↦ v ∗ inv N (spawn_inv γf γj c Ψ))%I.
 
 Definition join_handle (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (∃ γf γj Ψ', own γj (Excl ()) ∗ † c … 2 ∗ inv N (spawn_inv γf γj c Ψ') ∗
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index fa19c209..a5a6a9de 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -296,7 +296,7 @@ Qed.
 (* TODO: wp_eq for locations, if needed. *)
 
 Lemma wp_offset E l z Φ :
-  ▷ Φ (LitV $ LitLoc $ shift_loc l z) -∗
+  ▷ Φ (LitV $ LitLoc $ l +ₗ z) -∗
     WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
 Proof.
   iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 01f30578..46f57ef6 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -20,8 +20,8 @@ Notation "[ x1 ; x2 ; .. ; xn ]" :=
 
 (* No scope for the values, does not conflict and scope is often not inferred
 properly. *)
-Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
-Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
+Notation "# l" := (LitV l%Z%V%L) (at level 8, format "# l").
+Notation "# l" := (Lit l%Z%V%L) (at level 8, format "# l") : expr_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 647f112b..5baaf0a7 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -25,7 +25,7 @@ Inductive next_access_head : expr → state → access_kind * order → loc →
 | Access_free n l σ i :
     0 ≤ i < n →
     next_access_head (Free (Lit $ LitInt n) (Lit $ LitLoc l))
-                     σ (FreeAcc, Na2Ord) (shift_loc l i).
+                     σ (FreeAcc, Na2Ord) (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) σ →
@@ -139,7 +139,7 @@ Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' o1 a2 l :
   False.
 Proof.
   intros Ha1 Hstep Ha2 Hred2.
-  assert (FREE : ∀ l n i, 0 ≤ i ∧ i < n → free_mem l (Z.to_nat n) σ !! shift_loc l i = None).
+  assert (FREE : ∀ l n i, 0 ≤ i ∧ i < n → free_mem l (Z.to_nat n) σ !! (l +ₗ i) = None).
   { clear. intros l n i Hi.
     replace n with (Z.of_nat (Z.to_nat n)) in Hi by (apply Z2Nat.id; lia).
     revert l i Hi. induction (Z.to_nat n) as [|? IH]=>/=l i Hi. lia.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 0e4bb55b..249e6cc7 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -20,15 +20,15 @@ Section arc.
   Let P1 ν q := (q.[ν])%I.
   Instance P1_fractional ν : Fractional (P1 ν).
   Proof. unfold P1. apply _. Qed.
-  Let P2 l n := († l…(2 + n) ∗ shift_loc l 2 ↦∗: λ vl, ⌜length vl = n⌝)%I.
+  Let P2 l n := († l…(2 + n) ∗ (l +ₗ 2) ↦∗: λ vl, ⌜length vl = n⌝)%I.
   Definition arc_persist tid ν (γ : gname) (l : loc) (ty : type) : iProp Σ :=
     (is_arc (P1 ν) (P2 l ty.(ty_size)) arc_invN γ l ∗
      (* We use this disjunction, and not simply [ty_shr] here, *)
      (*    because [weak_new] cannot prove ty_shr, even for a dead *)
      (*    lifetime. *)
-     (ty.(ty_shr) ν tid (shift_loc l 2) ∨ [†ν]) ∗
+     (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
      □ (1.[ν] ={↑lftN ∪ ↑arc_endN,∅}▷=∗
-          [†ν] ∗ ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size))))%I.
+          [†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size))))%I.
 
   Global Instance arc_persist_ne tid ν γ l n :
     Proper (type_dist2 n ==> dist n) (arc_persist tid ν γ l).
@@ -64,8 +64,8 @@ Section arc.
      content. The reason is that get_mut does not have the
      masks to rebuild the invariants. *)
   Definition full_arc_own l ty tid : iProp Σ:=
-    (l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ † l…(2 + ty.(ty_size)) ∗
-       ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid)%I.
+    (l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ † l…(2 + ty.(ty_size)) ∗
+       ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid)%I.
   Definition shared_arc_own l ty tid : iProp Σ:=
     (∃ γ ν q, arc_persist tid ν γ l ty ∗ arc_tok γ q ∗ q.[ν])%I.
   Lemma arc_own_share E l ty tid :
@@ -889,7 +889,7 @@ Section arc.
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
         iFrame. iCombine "Hr1" "Hr2" as "Hr1". iCombine "Hr0" "Hr1" as "Hr".
-        rewrite -[in shift_loc _ ty.(ty_size)]Hlen -heap_mapsto_vec_app
+        rewrite -[in _ +â‚— ty.(ty_size)]Hlen -heap_mapsto_vec_app
                 -heap_mapsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
         iExists O, _, _. iSplit; first by auto. iFrame. iIntros "!> !% /=".
         rewrite app_length drop_length. lia. }
@@ -1034,7 +1034,7 @@ Section arc.
       { iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
         iFrame. iLeft. by iFrame. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
-      iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #(shift_loc rc 2) ◁ &uniq{α}ty;
+      iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #(rc +ₗ 2) ◁ &uniq{α}ty;
                                 r ◁ box (uninit 1) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
@@ -1052,7 +1052,7 @@ Section arc.
       iDestruct (ty_size_eq with "Hown") as %Hlen'.
       wp_apply (wp_memcpy with "[$Hrc2 $H↦]"); [lia..|].
       iIntros "[H↦ H↦']". wp_seq. wp_write.
-      iMod ("Hclose2" $! (shift_loc l 2 ↦∗: ty_own ty tid)%I
+      iMod ("Hclose2" $! ((l +ₗ 2) ↦∗: ty_own ty tid)%I
         with "[Hrc'↦ Hrc0 Hrc1 H†] [H↦ Hown]") as "[Hb Hα1]"; [|by auto with iFrame|].
       { iIntros "!> H↦". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
         iLeft. iFrame. iDestruct "H†" as "[?|%]"=>//.
@@ -1094,7 +1094,7 @@ Section arc.
       wp_apply (wp_delete with "[$Hcl↦ Hcl†]");
         [lia|by replace (length vl) with (ty.(ty_size))|].
       iIntros "_". wp_seq. wp_write.
-      iMod ("Hclose2" $! (shift_loc l' 2 ↦∗: ty_own ty tid)%I with
+      iMod ("Hclose2" $! ((l' +ₗ 2) ↦∗: ty_own ty tid)%I with
           "[Hrc'↦ Hl' Hl'1  Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
       { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
         iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 12ae9140..18ce32b1 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -34,7 +34,7 @@ Section mutex.
            ⌜∃ b, z = Z_of_bool b⌝ ∗ ty.(ty_own) tid vl'
          | _ => False end;
        ty_shr κ tid l := ∃ κ', κ ⊑ κ' ∗
-           &at{κ, mutexN} (lock_proto l (&{κ'} shift_loc l 1 ↦∗: ty.(ty_own) tid))
+           &at{κ, mutexN} (lock_proto l (&{κ'} (l +ₗ 1) ↦∗: ty.(ty_own) tid))
     |}%I.
   Next Obligation.
     iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
@@ -48,7 +48,7 @@ Section mutex.
     iDestruct "H" as "[>EQ Hown]". iDestruct "EQ" as %[b ->].
     (* We need to turn the ohne borrow into two, so we close it -- and then
        we open one of them again. *)
-    iMod ("Hclose" $! ((∃ b, l ↦ #(Z_of_bool b)) ∗ (shift_loc l 1 ↦∗: ty_own ty tid))%I
+    iMod ("Hclose" $! ((∃ b, l ↦ #(Z_of_bool b)) ∗ ((l +ₗ 1) ↦∗: ty_own ty tid))%I
           with "[] [Hl H↦ Hown]") as "[Hbor Htok]".
     { clear. iNext. iIntros "[Hl Hown] !>". iNext. iDestruct "Hl" as (b) "Hl".
       iDestruct "Hown" as (vl) "[H↦ Hown]". iExists (#(Z_of_bool b) :: vl).
@@ -233,13 +233,13 @@ Section code.
     destruct vl as [|[[|m'|]|] vl]; try done. simpl.
     iDestruct (heap_mapsto_vec_cons with "H↦") as "[H↦1 H↦2]".
     iDestruct "Hm'" as "[% Hvl]".
-    iMod ("Hclose2" $! (shift_loc lm' 1 ↦∗: ty_own ty tid)%I with "[H↦1] [H↦2 Hvl]") as "[Hbor Hα]".
+    iMod ("Hclose2" $! ((lm' +ₗ 1) ↦∗: ty_own ty tid)%I with "[H↦1] [H↦2 Hvl]") as "[Hbor Hα]".
     { iIntros "!> Hlm' !>". iNext. clear vl. iDestruct "Hlm'" as (vl) "[H↦ Hlm']".
       iExists (_ :: _). rewrite heap_mapsto_vec_cons. do 2 iFrame. done. }
     { iExists vl. iFrame. }
     iMod ("Hclose1" with "Hα HL") as "HL".
     (* Switch back to typing mode. *)
-    iApply (type_type _ _ _ [ m ◁ own_ptr _ _; #(shift_loc lm' 1) ◁ &uniq{α} ty]
+    iApply (type_type _ _ _ [ m ◁ own_ptr _ _; #(lm' +ₗ 1) ◁ &uniq{α} ty]
         with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. }
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index c2b4b68c..e68e4fc3 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -35,13 +35,13 @@ Section mguard.
          match vl return _ with
          | [ #(LitLoc l) ] =>
            ∃ β, α ⊑ β ∗
-             &at{α, mutexN} (lock_proto l (&{β} shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
-             &{β} (shift_loc l 1 ↦∗: ty.(ty_own) tid)
+             &at{α, mutexN} (lock_proto l (&{β} (l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+             &{β} ((l +ₗ 1) ↦∗: ty.(ty_own) tid)
          | _ => False end;
        ty_shr κ tid l :=
          ∃ (l':loc), &frac{κ}(λ q', l ↦{q'} #l') ∗
             □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α⊓κ]
-                ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (α⊓κ) tid (shift_loc l' 1) ∗ q.[α⊓κ]
+                ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (α⊓κ) tid (l' +ₗ 1) ∗ q.[α⊓κ]
     |}%I.
   Next Obligation. by iIntros (? ty tid [|[[]|][]]) "H". Qed.
   (* This is to a large extend copy-pasted from RWLock's write guard. *)
@@ -136,7 +136,7 @@ Section code.
 
   Lemma mutex_acc E l ty tid q α κ :
     ↑lftN ⊆ E → ↑mutexN ⊆ E →
-    let R := (&{κ} shift_loc l 1 ↦∗: ty_own ty tid)%I in
+    let R := (&{κ} (l +ₗ 1) ↦∗: ty_own ty tid)%I in
     lft_ctx -∗ &at{α,mutexN} lock_proto l R -∗ α ⊑ κ -∗
     □ ((q).[α] ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ (q).[α])).
   Proof.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index a4226927..4254db32 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -60,16 +60,16 @@ Section rc.
     (∃ st : rc_stR, own γ (● st) ∗
       match st with
       | (Some (Cinl (q, strong)), weak) => ∃ q',
-        l ↦ #(Zpos strong) ∗ shift_loc l 1 ↦ #(S weak) ∗ † l…(2 + ty.(ty_size)) ∗
+        l ↦ #(Zpos strong) ∗ (l +ₗ 1) ↦ #(S weak) ∗ † l…(2 + ty.(ty_size)) ∗
           ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
           (* We keep this view shift decomposed because we store the persistent
              part in ty_own, to make it available with one step less. *)
-          ([†ν] ={↑lftN}=∗ ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid)
+          ([†ν] ={↑lftN}=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid)
       | (Some (Cinr _), weak) =>
-        l ↦ #0 ∗ shift_loc l 1 ↦ #(S weak)
+        l ↦ #0 ∗ (l +ₗ 1) ↦ #(S weak)
       | (None, (S _) as weak) =>
-        l ↦ #0 ∗ shift_loc l 1 ↦ #weak ∗ † l…(2 + ty.(ty_size)) ∗
-          shift_loc l 2 ↦∗: λ vl, ⌜length vl = ty.(ty_size)⌝
+        l ↦ #0 ∗ (l +ₗ 1) ↦ #weak ∗ † l…(2 + ty.(ty_size)) ∗
+          (l +ₗ 2) ↦∗: λ vl, ⌜length vl = ty.(ty_size)⌝
       | _ => True
       end)%I.
 
@@ -85,7 +85,7 @@ Section rc.
               (* We use this disjunction, and not simply [ty_shr] here,
                  because [weak_new] cannot prove ty_shr, even for a dead
                  lifetime. *)
-              (ty.(ty_shr) ν tid (shift_loc l 2) ∨ [†ν]) ∗
+              (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
               □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]))%I.
 
   Global Instance rc_persist_ne ν γ l n :
@@ -114,8 +114,8 @@ Section rc.
               shared protocol or the full ownership of the
               content. The reason is that get_mut does not have the
               masks to rebuild the invariants. *)
-           (l ↦ #1 ∗ shift_loc l 1 ↦ #1 ∗ † l…(2 + ty.(ty_size)) ∗
-            ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid) ∨
+           (l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ † l…(2 + ty.(ty_size)) ∗
+            ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid) ∨
            (∃ γ ν q, rc_persist tid ν γ l ty ∗ own γ (rc_tok q) ∗ q.[ν])
          | _ => False end;
        ty_shr κ tid l :=
@@ -241,25 +241,25 @@ Section code.
     !#l
     {{{ strong, RET #(Zpos strong); l ↦ #(Zpos strong) ∗
         (((⌜strong = 1%positive⌝ ∗
-           (∃ weak : Z, shift_loc l 1 ↦ #weak ∗
+           (∃ weak : Z, (l +ₗ 1) ↦ #weak ∗
              ((⌜weak = 1⌝ ∗
                |={⊤,∅}▷=> † l…(2 + ty.(ty_size)) ∗
-                          ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid ∗ na_own tid F) ∨
+                          ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ na_own tid F) ∨
              (⌜weak > 1⌝ ∗
-              ((l ↦ #1 -∗ shift_loc l 1 ↦ #weak
+              ((l ↦ #1 -∗ (l +ₗ 1) ↦ #weak
                 ={⊤}=∗ na_own tid F ∗ ty_own (rc ty) tid [ #l ]) ∧
-               (l ↦ #0 -∗ shift_loc l 1 ↦ #(weak - 1)
-                ={⊤,∅}▷=∗ ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid ∗
-                (shift_loc l 2 ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
+               (l ↦ #0 -∗ (l +ₗ 1) ↦ #(weak - 1)
+                ={⊤,∅}▷=∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗
+                ((l +ₗ 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
                  ={⊤}=∗ na_own tid F)))))) ∧
            (l ↦ #0 ={⊤,∅}▷=∗
-             ▷ shift_loc l 2 ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size)) ∗ na_own tid F ∗
+             ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size)) ∗ na_own tid F ∗
              (na_own tid F ={⊤}=∗ ∃ weak : Z,
-                shift_loc l 1 ↦ #weak ∗
+                (l +ₗ 1) ↦ #weak ∗
                 ((⌜weak = 1⌝ ∗ l ↦ #0 ∗ na_own tid F) ∨
                  (⌜weak > 1⌝ ∗
-                   († l…(2 + ty.(ty_size)) -∗ shift_loc l 1 ↦ #(weak-1) -∗
-                    shift_loc l 2 ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
+                   († l…(2 + ty.(ty_size)) -∗ (l +ₗ 1) ↦ #(weak-1) -∗
+                    (l +ₗ 2) ↦∗: (λ vl, ⌜length vl = ty.(ty_size)⌝)
                     ={⊤}=∗ na_own tid F))))))
          ) ∨
          (⌜(1 < strong)%positive⌝ ∗
@@ -1035,13 +1035,13 @@ Section code.
         iDestruct (ty_size_eq with "Hty") as %?.
         wp_apply (wp_memcpy with "[$Hlr3 $H↦vlr]"); [lia..|]. iIntros "[Hlr3 Hvlr]".
         wp_seq. wp_write. wp_op. iMod ("Hproto" with "[Hvlr]") as "Hna"; first by eauto.
-        iMod ("Hclose2" $! (shift_loc lr 2 ↦∗: ty_own ty tid)%I
+        iMod ("Hclose2" $! ((lr +ₗ 2) ↦∗: ty_own ty tid)%I
               with "[Hrc' Hlr1 Hlr2 H†] [Hlr3 Hty]") as "[Hb Hα1]".
         { iIntros "!> H !>". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
           iLeft. iFrame. rewrite Z2Nat.inj_pos Pos2Nat.inj_succ SuccNat2Pos.id_succ //. }
         { iExists _. iFrame. }
         iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
-        iApply (type_type _ _ _ [ r ◁ box (uninit 1); #(shift_loc lr 2) ◁ &uniq{α} ty;
+        iApply (type_type _ _ _ [ r ◁ box (uninit 1); #(lr +ₗ 2) ◁ &uniq{α} ty;
                                   rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
@@ -1092,7 +1092,7 @@ Section code.
       wp_apply (wp_delete with "[$Hcl↦ Hcl†]");
         [lia|by replace (length vl) with (ty.(ty_size))|].
       iIntros "_". wp_seq. wp_write.
-      iMod ("Hclose2" $! (shift_loc l' 2 ↦∗: ty_own ty tid)%I with
+      iMod ("Hclose2" $! ((l' +ₗ 2) ↦∗: ty_own ty tid)%I with
           "[Hrc' Hl' Hl'1  Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
       { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
         iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 34417e1c..c19b2451 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -320,7 +320,7 @@ Section code.
     iModIntro. wp_let. wp_op.
     (* Finally, finally... opening the thread-local Rc protocol. *)
     iPoseProof "Hpersist" as (ty') "(_ & Hinv & _ & _)".
-    iAssert (∃ wv : Z, shift_loc l' 1 ↦ #wv ∗ (shift_loc l' 1 ↦ #(wv + 1) ={⊤}=∗
+    iAssert (∃ wv : Z, (l' +ₗ 1) ↦ #wv ∗ ((l' +ₗ 1) ↦ #(wv + 1) ={⊤}=∗
                na_own tid ⊤ ∗ (q / 2).[α] ∗ own γ weak_tok))%I
       with "[> Hna Hα1]" as (wv) "[Hwv Hclose2]".
     { iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
@@ -389,11 +389,11 @@ Section code.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hw' _]]".
     rewrite !tctx_hasty_val [[w]]lock. destruct w' as [[|lw|]|]; try done. wp_op.
     iDestruct "Hw'" as (γ ν) "[#Hpersist Hwtok]".
-    iAssert (∃ wv : Z, shift_loc lw 1 ↦ #wv ∗
+    iAssert (∃ wv : Z, (lw +ₗ 1) ↦ #wv ∗
         ((⌜wv = 1⌝ ∗ na_own tid ⊤ ∗
-          ∃ s, lw ↦ s ∗ (shift_loc lw 2 ↦∗: λ vl, ⌜length vl = ty.(ty_size)⌝) ∗
+          ∃ s, lw ↦ s ∗ ((lw +ₗ 2) ↦∗: λ vl, ⌜length vl = ty.(ty_size)⌝) ∗
                † lw … (2 + ty_size ty)) ∨
-         (⌜wv > 1⌝ ∗ (shift_loc lw 1 ↦ #(wv - 1) ={⊤}=∗ na_own tid ⊤))))%I
+         (⌜wv > 1⌝ ∗ ((lw +ₗ 1) ↦ #(wv - 1) ={⊤}=∗ na_own tid ⊤))))%I
       with "[>Hna Hwtok]" as (wv) "[Hlw [(% & Hna & H)|[% Hclose]]]".
     { iPoseProof "Hpersist" as (ty') "([>Hszeq _] & Hinv & _ & _)".
       iDestruct "Hszeq" as %Hszeq.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 7bceb017..cb559fbd 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -15,8 +15,8 @@ Section ref_functions.
     own γ (◯ reading_st q ν) -∗
     ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
             own γ (● Some (to_agree ν, Cinr (q', n)) ⋅ ◯ reading_st q ν) ∗
-            ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
-            ((1).[ν] ={↑lftN,∅}▷=∗ &{α} shift_loc l 1 ↦∗: ty_own ty tid) ∗
+            ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
+            ((1).[ν] ={↑lftN,∅}▷=∗ &{α} (l +ₗ 1) ↦∗: ty_own ty tid) ∗
             ∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν].
   Proof.
     iIntros "INV Hâ—¯".
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index f34f6305..e51da96b 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -36,14 +36,14 @@ Section refcell_inv.
       match st return _ with
       | None =>
         (* Not borrowed. *)
-        &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
+        &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
       | Some (agν, st) =>
         ∃ ν, agν ≡ to_agree ν ∗
-             (1.[ν] ={↑lftN,∅}▷=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
+             (1.[ν] ={↑lftN,∅}▷=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
              match st with
              | Cinr (q, n) =>
                (* Immutably borrowed. *)
-               ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
+               ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
                ∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
              | _ => (* Mutably borrowed. *) True
              end
@@ -72,8 +72,8 @@ Section refcell_inv.
     rewrite eqtype_unfold. iIntros (Hty) "HL".
     iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
     iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
-    iAssert (□ (&{α} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
-                &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I as "#Hb".
+    iAssert (□ (&{α} (l +ₗ 1) ↦∗: ty_own ty1 tid -∗
+                &{α} (l +ₗ 1) ↦∗: ty_own ty2 tid))%I as "#Hb".
     { iIntros "!# H". iApply bor_iff; last done.
       iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
@@ -116,7 +116,7 @@ Section refcell.
     iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
     iDestruct "H" as "[>% Hown]".
     iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ n⌝) ∗
-            shift_loc l 1 ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
+            (l +ₗ 1) ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
     { iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
       iDestruct "Hvl" as (vl') "[H↦ Hvl]".
       iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗%". }
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index e596aca9..cf20a8c7 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -97,7 +97,7 @@ Section refcell_functions.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
     iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ z⌝) ∗
-        (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with "[> Hx']" as "[_ Hx']".
+        (&uniq{α} ty).(ty_own) tid [ #(lx' +ₗ 1)])%I with "[> Hx']" as "[_ Hx']".
     { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
       - iIntros "[H1 H2]". iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
         iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
@@ -108,7 +108,7 @@ Section refcell_functions.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
     iApply (type_type _ _ _
-            [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]
+            [ #lx ◁ box (uninit 1); #(lx' +ₗ 1) ◁ &uniq{α}ty]
             with "[] LFT HE Hna HL HC [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
@@ -174,7 +174,7 @@ Section refcell_functions.
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
       iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
-                       ty_shr ty (β ⊓ ν) tid (shift_loc lx 1) ∗
+                       ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
                        own γ (◯ reading_st qν ν) ∗ refcell_inv tid lx γ β ty)%I
         with "[> Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV)".
       { destruct st as [[agν [|[q n]|]]|]; try done.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 7b68f992..5a3ff7ba 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -35,13 +35,13 @@ Section rwlock_inv.
       match st return _ with
       | None =>
         (* Not locked. *)
-        &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)
+        &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)
       | Some (Cinr (agν, q, n)) =>
         (* Locked for read. *)
         ∃ (ν : lft) q', agν ≡ to_agree ν ∗
                 □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗
-                ([†ν] ={↑lftN}=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
-                ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
+                ([†ν] ={↑lftN}=∗ &{α}((l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+                ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
                 ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν]
       | _ => (* Locked for write. *) True
       end)%I.
@@ -68,8 +68,8 @@ Section rwlock_inv.
     rewrite eqtype_unfold. iIntros (Hty) "HL".
     iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
     iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
-    iAssert (□ (&{α} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
-                &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I as "#Hb".
+    iAssert (□ (&{α} (l +ₗ 1) ↦∗: ty_own ty1 tid -∗
+                &{α} (l +ₗ 1) ↦∗: ty_own ty2 tid))%I as "#Hb".
     { iIntros "!# H". iApply bor_iff; last done.
       iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
@@ -111,7 +111,7 @@ Section rwlock.
     iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
     iDestruct "H" as "[>% Hown]".
     iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ n⌝) ∗
-            shift_loc l 1 ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
+            (l +ₗ 1) ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
     { iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
       iDestruct "Hvl" as (vl') "[H↦ Hvl]".
       iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗%". }
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 1df9e471..a97ecbc0 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -97,7 +97,7 @@ Section rwlock_functions.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
     iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ z⌝) ∗
-        (&uniq{α} ty).(ty_own) tid [ #(shift_loc lx' 1)])%I with "[> Hx']" as "[_ Hx']".
+        (&uniq{α} ty).(ty_own) tid [ #(lx' +ₗ 1)])%I with "[> Hx']" as "[_ Hx']".
     { iApply bor_sep; [done..|]. iApply (bor_proper with "Hx'"). iSplit.
       - iIntros "[H1 H2]". iDestruct "H1" as (z) "[??]". iDestruct "H2" as (vl) "[??]".
         iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. iFrame.
@@ -108,7 +108,7 @@ Section rwlock_functions.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
     iApply (type_type _ _ _
-            [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]
+            [ #lx ◁ box (uninit 1); #(lx' +ₗ 1) ◁ &uniq{α}ty]
             with "[] LFT HE Hna HL HC [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
@@ -181,7 +181,7 @@ Section rwlock_functions.
       destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?]=>?.
       + iApply (wp_cas_int_suc with "Hlx"); first done. iNext. iIntros "Hlx".
         iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
-                         ty_shr ty (β ⊓ ν) tid (shift_loc lx 1) ∗
+                         ty_shr ty (β ⊓ ν) tid (lx +ₗ 1) ∗
                          own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
                          ((1).[ν] ={↑lftN,∅}▷=∗ [†ν]))%I
           with "[> Hlx Hownst Hst Hβtok2]"
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 6bbcfe1d..1beca19d 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -20,7 +20,7 @@ Section rwlockreadguard.
        ty_own tid vl :=
          match vl return _ with
          | [ #(LitLoc l) ] =>
-           ∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
+           ∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
              α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
              q.[ν] ∗ own γ (◯ reading_st q ν) ∗
              (1.[ν] ={↑lftN,∅}▷=∗ [†ν])
@@ -29,7 +29,7 @@ Section rwlockreadguard.
        ty_shr κ tid l :=
          ∃ (l' : loc),
            &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
-           ▷ ty.(ty_shr) (α ⊓ κ) tid (shift_loc l' 1) |}%I.
+           ▷ ty.(ty_shr) (α ⊓ κ) tid (l' +ₗ 1) |}%I.
   Next Obligation. intros α ty tid [|[[]|] []]; auto. Qed.
   Next Obligation.
     iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index a746c7a1..0450bc94 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -35,7 +35,7 @@ Section rwlockreadguard_functions.
     iMod ("Hcloseα" with "[$H↦]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rwlockreadguard β ty);
-                              #(shift_loc l' 1) ◁ &shr{α}ty]
+                              #(l' +ₗ 1) ◁ &shr{α}ty]
       with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb; first done.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 9ba6c327..1d2f6512 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -21,7 +21,7 @@ Section rwlockwriteguard.
        ty_own tid vl :=
          match vl return _ with
          | [ #(LitLoc l) ] =>
-           ∃ γ β, &{β}(shift_loc l 1 ↦∗: ty.(ty_own) tid) ∗
+           ∃ γ β, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
              α ⊑ β ∗ &at{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
              own γ (◯ writing_st)
          | _ => False
@@ -30,7 +30,7 @@ Section rwlockwriteguard.
          ∃ (l' : loc),
            &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ] ={F, F∖↑shrN}▷=∗
-               ty.(ty_shr) (α ⊓ κ) tid (shift_loc l' 1) ∗ q.[α ⊓ κ] |}%I.
+               ty.(ty_shr) (α ⊓ κ) tid (l' +ₗ 1) ∗ q.[α ⊓ κ] |}%I.
   Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
   Next Obligation.
     iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index c19d95e4..4b6bd11f 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -44,7 +44,7 @@ Section rwlockwriteguard_functions.
     iMod ("Hclose" with "[$] HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rwlockwriteguard β ty);
-                              #(shift_loc l' 1) ◁ &shr{α}ty]
+                              #(l' +ₗ 1) ◁ &shr{α}ty]
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb; first done.
@@ -88,7 +88,7 @@ Section rwlockwriteguard_functions.
     wp_read. wp_op. wp_let. iMod "Hb".
     iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose" with "Hα HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
-    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(shift_loc l 1) ◁ &uniq{α}ty]
+    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(l +ₗ 1) ◁ &uniq{α}ty]
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (bor_shorten with "[] Hb"). iApply lft_incl_glb.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 47db32f4..d1b7551d 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -32,7 +32,7 @@ Section own.
   Proof. rewrite freeable_sz_full. iSplit; auto. iIntros "[$|%]"; done. Qed.
 
   Lemma freeable_sz_split n sz1 sz2 l :
-    freeable_sz n sz1 l ∗ freeable_sz n sz2 (shift_loc l sz1) ⊣⊢
+    freeable_sz n sz1 l ∗ freeable_sz n sz2 (l +ₗ sz1) ⊣⊢
                 freeable_sz n (sz1 + sz2) l.
   Proof.
     destruct sz1; [|destruct sz2;[|rewrite /freeable_sz plus_Sn_m; destruct n]].
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 6fab9f41..f69b9873 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -38,7 +38,7 @@ Section product.
   Lemma split_prod_mt tid ty1 ty2 q l :
     (l ↦∗{q}: λ vl,
        ∃ vl1 vl2, ⌜vl = vl1 ++ vl2⌝ ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
-       ⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ shift_loc l ty1.(ty_size) ↦∗{q}: ty2.(ty_own) tid.
+       ⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ (l +ₗ ty1.(ty_size)) ↦∗{q}: ty2.(ty_own) tid.
   Proof.
     iSplit; iIntros "H".
     - iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
@@ -57,7 +57,7 @@ Section product.
          ⌜vl = vl1 ++ vl2⌝ ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
        ty_shr κ tid l :=
          (ty1.(ty_shr) κ tid l ∗
-          ty2.(ty_shr) κ tid (shift_loc l ty1.(ty_size)))%I |}.
+          ty2.(ty_shr) κ tid (l +ₗ ty1.(ty_size)))%I |}.
   Next Obligation.
     iIntros (ty1 ty2 tid vl) "H". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
     subst. rewrite app_length !ty_size_eq.
@@ -116,7 +116,7 @@ Section product.
     { rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. omega. }
     iMod (@copy_shr_acc with "LFT H2 Htl Htok2") as (q2) "(Htl & H2 & Hclose2)"; first solve_ndisj.
     { move: HF. rewrite /= -plus_assoc shr_locsE_shift.
-      assert (shr_locsE l (ty_size ty1) ⊥ shr_locsE (shift_loc l (ty_size ty1)) (ty_size ty2 + 1))
+      assert (shr_locsE l (ty_size ty1) ⊥ shr_locsE (l +ₗ (ty_size ty1)) (ty_size ty2 + 1))
              by exact: shr_locsE_disj.
       set_solver. }
     iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 585a95e4..3a345f96 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -32,8 +32,8 @@ Section sum.
                                ⌜length vl = S (max_list_with ty_size tyl)⌝ ∗
                                ty_own (nth i tyl emp0) tid vl')%I
     ⊣⊢ ∃ (i : nat), (l ↦{q} #i ∗
-                     shift_loc l (S $ (nth i tyl emp0).(ty_size)) ↦∗{q}: is_pad i tyl) ∗
-                              shift_loc l 1 ↦∗{q}: (nth i tyl emp0).(ty_own) tid.
+                     (l +ₗ (S $ (nth i tyl emp0).(ty_size))) ↦∗{q}: is_pad i tyl) ∗
+                              (l +ₗ 1) ↦∗{q}: (nth i tyl emp0).(ty_own) tid.
   Proof.
     iSplit; iIntros "H".
     - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl' vl'') "(% & % & Hown)".
@@ -61,8 +61,8 @@ Section sum.
        ty_shr κ tid l :=
          (∃ (i : nat),
              (&frac{κ} λ q, l ↦{q} #i ∗
-                       shift_loc l (S $ (nth i tyl emp0).(ty_size)) ↦∗{q}: is_pad i tyl) ∗
-               (nth i tyl emp0).(ty_shr) κ tid (shift_loc l 1))%I
+                       (l +ₗ (S $ (nth i tyl emp0).(ty_size))) ↦∗{q}: is_pad i tyl) ∗
+               (nth i tyl emp0).(ty_shr) κ tid (l +ₗ 1))%I
     |}.
   Next Obligation.
     iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (i vl' vl'') "(%&%&_)".
@@ -197,7 +197,7 @@ Section sum.
         apply shr_locsE_subseteq. omega. }
       iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
       { apply difference_mono_l.
-        trans (shr_locsE (shift_loc l 1) (max_list_with ty_size tyl)).
+        trans (shr_locsE (l +â‚— 1) (max_list_with ty_size tyl)).
         - apply shr_locsE_subseteq. omega.
         - set_solver+. }
       destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 7adb46bc..091e9dc6 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -389,7 +389,7 @@ Ltac solve_type_proper :=
 Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
   match n with
   | 0%nat => ∅
-  | S n => ↑shrN.@l ∪ shr_locsE (shift_loc l 1%nat) n
+  | S n => ↑shrN.@l ∪ shr_locsE (l +ₗ 1%nat) n
   end.
 
 Class Copy `{typeG Σ} (t : type) := {
@@ -436,7 +436,7 @@ Section type.
 
   (** Copy types *)
   Lemma shr_locsE_shift l n m :
-    shr_locsE l (n + m) = shr_locsE l n ∪ shr_locsE (shift_loc l n) m.
+    shr_locsE l (n + m) = shr_locsE l n ∪ shr_locsE (l +ₗ n) m.
   Proof.
     revert l; induction n; intros l.
     - rewrite shift_loc_0. set_solver+.
@@ -445,7 +445,7 @@ Section type.
   Qed.
 
   Lemma shr_locsE_disj l n m :
-    shr_locsE l n ⊥ shr_locsE (shift_loc l n) m.
+    shr_locsE l n ⊥ shr_locsE (l +ₗ n) m.
   Proof.
     revert l; induction n; intros l.
     - simpl. set_solver+.
@@ -473,7 +473,7 @@ Section type.
 
   Lemma shr_locsE_split_tok l n m tid :
     na_own tid (shr_locsE l (n + m)) ⊣⊢
-      na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (shift_loc l n) m).
+      na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (l +ₗ n) m).
   Proof.
     rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
   Qed.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 7b1b47e9..aec79f46 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -26,7 +26,7 @@ Section type_context.
     match p with
     | BinOp OffsetOp e (Lit (LitInt n)) =>
       match eval_path e with
-      | Some (#(LitLoc l)) => Some (#(shift_loc l n))
+      | Some (#(LitLoc l)) => Some (#(l +â‚— n))
       | _ => None
       end
     | e => to_val e
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index b642ba74..e01d100f 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -76,7 +76,7 @@ Section case.
     wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
     iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'.
     destruct Hety as [Hety|Hety].
-    - iMod ("Hclose'" $! (shift_loc l 1 ↦∗: ty.(ty_own) tid)%I
+    - iMod ("Hclose'" $! ((l +ₗ 1) ↦∗: ty.(ty_own) tid)%I
             with "[H↦i H↦vl''] [H↦vl' Hown]") as "[Hb Htok]".
       { iIntros "!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
         iExists (#i::vl'2++vl''). iIntros "!>". iNext.
-- 
GitLab