diff --git a/opam b/opam
index 600c227bc3c1e69d6f729e91be961c545062dc54..9027351e3ac6483546b5634638e1b61731814aab 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2019-02-27.0.77b1b58a") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-03-04.0.5f34e857") | (= "dev") }
 ]
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
new file mode 100644
index 0000000000000000000000000000000000000000..05315b8ca366ec038cd967817a2f899ded151084
--- /dev/null
+++ b/theories/lang/adequacy.v
@@ -0,0 +1,32 @@
+From iris.program_logic Require Export adequacy weakestpre.
+From iris.algebra Require Import auth.
+From lrust.lang Require Export heap.
+From lrust.lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+Class lrustPreG Σ := HeapPreG {
+  lrust_preG_irig :> invPreG Σ;
+  lrust_preG_heap :> inG Σ (authR heapUR);
+  lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
+}.
+
+Definition lrustΣ : gFunctors :=
+  #[invΣ;
+    GFunctor (constRF (authR heapUR));
+    GFunctor (constRF (authR heap_freeableUR))].
+Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
+Proof. solve_inG. Qed.
+
+Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
+  (∀ `{!lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+  adequate NotStuck e σ (λ v _, φ v).
+Proof.
+  intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
+  iMod (own_alloc (● to_heap σ)) as (vγ) "Hvγ".
+  { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
+  iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ"; first done.
+  set (Hheap := HeapG _ _ _ vγ fγ).
+  iModIntro. iExists (λ σ _, heap_ctx σ). iSplitL.
+  { iExists ∅. by iFrame. }
+  by iApply (Hwp (LRustG _ _ Hheap)).
+Qed.
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
new file mode 100644
index 0000000000000000000000000000000000000000..38b1406200ed9089d7b1cd97e742a9b70a94d31b
--- /dev/null
+++ b/theories/lang/heap.v
@@ -0,0 +1,548 @@
+From Coq Require Import Min.
+From stdpp Require Import coPset.
+From iris.algebra Require Import big_op gmap frac agree.
+From iris.algebra Require Import csum excl auth cmra_big_op.
+From iris.bi Require Import fractional.
+From iris.base_logic Require Export lib.own.
+From iris.proofmode Require Export tactics.
+From lrust.lang Require Export lang.
+Set Default Proof Using "Type".
+Import uPred.
+
+Definition lock_stateR : cmraT :=
+  csumR (exclR unitC) natR.
+
+Definition heapUR : ucmraT :=
+  gmapUR loc (prodR (prodR fracR lock_stateR) (agreeR valC)).
+
+Definition heap_freeableUR : ucmraT :=
+  gmapUR block (prodR fracR (gmapR Z (exclR unitC))).
+
+Class heapG Σ := HeapG {
+  heap_inG :> inG Σ (authR heapUR);
+  heap_freeable_inG :> inG Σ (authR heap_freeableUR);
+  heap_name : gname;
+  heap_freeable_name : gname
+}.
+
+Definition to_lock_stateR (x : lock_state) : lock_stateR :=
+  match x with RSt n => Cinr n | WSt => Cinl (Excl ()) end.
+Definition to_heap : state → heapUR :=
+  fmap (λ v, (1%Qp, to_lock_stateR (v.1), to_agree (v.2))).
+Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
+  ∀ blk qs, hF !! blk = Some qs →
+    qs.2 ≠ ∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
+
+Section definitions.
+  Context `{!heapG Σ}.
+
+  Definition heap_mapsto_st (st : lock_state)
+             (l : loc) (q : Qp) (v: val) : iProp Σ :=
+    own heap_name (◯ {[ l := (q, to_lock_stateR st, to_agree v) ]}).
+
+  Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
+    heap_mapsto_st (RSt 0) l q v.
+  Definition heap_mapsto_aux : seal (@heap_mapsto_def). by eexists. Qed.
+  Definition heap_mapsto := unseal heap_mapsto_aux.
+  Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
+    seal_eq heap_mapsto_aux.
+
+  Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
+    ([∗ 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.
+
+  Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ :=
+    own heap_freeable_name (◯ {[ l.1 := (q, inter (l.2) n) ]}).
+  Definition heap_freeable_aux : seal (@heap_freeable_def). by eexists. Qed.
+  Definition heap_freeable := unseal heap_freeable_aux.
+  Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def :=
+    seal_eq heap_freeable_aux.
+
+  Definition heap_ctx (σ:state) : iProp Σ :=
+    (∃ hF, own heap_name (● to_heap σ)
+         ∗ own heap_freeable_name (● hF)
+         ∗ ⌜heap_freeable_rel σ hF⌝)%I.
+End definitions.
+
+Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
+Instance: Params (@heap_mapsto) 4 := {}.
+Instance: Params (@heap_freeable) 5 := {}.
+
+Notation "l ↦{ q } v" := (heap_mapsto l q v)
+  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
+Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : bi_scope.
+
+Notation "l ↦∗{ q } vl" := (heap_mapsto_vec l q vl)
+  (at level 20, q at level 50, format "l  ↦∗{ q }  vl") : bi_scope.
+Notation "l ↦∗ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : bi_scope.
+
+Notation "l ↦∗{ q }: P" := (∃ vl, l ↦∗{ q } vl ∗ P vl)%I
+  (at level 20, q at level 50, format "l  ↦∗{ q }:  P") : bi_scope.
+Notation "l ↦∗: P " := (∃ vl, l ↦∗ vl ∗ P vl)%I
+  (at level 20, format "l  ↦∗:  P") : bi_scope.
+
+Notation "†{ q } l … n" := (heap_freeable l q n)
+  (at level 20, q at level 50, format "†{ q } l … n") : bi_scope.
+Notation "† l … n" := (heap_freeable l 1 n) (at level 20) : bi_scope.
+
+Section to_heap.
+  Implicit Types σ : state.
+
+  Lemma to_heap_valid σ : ✓ to_heap σ.
+  Proof. intros l. rewrite lookup_fmap. case (σ !! l)=> [[[|n] v]|] //=. Qed.
+
+  Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
+  Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
+
+  Lemma to_heap_insert σ l x v :
+    to_heap (<[l:=(x, v)]> σ)
+    = <[l:=(1%Qp, to_lock_stateR x, to_agree v)]> (to_heap σ).
+  Proof. by rewrite /to_heap fmap_insert. Qed.
+
+  Lemma to_heap_delete σ l : to_heap (delete l σ) = delete l (to_heap σ).
+  Proof. by rewrite /to_heap fmap_delete. Qed.
+End to_heap.
+
+Section heap.
+  Context `{!heapG Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types σ : state.
+  Implicit Types E : coPset.
+
+  (** General properties of mapsto and freeable *)
+  Global Instance heap_mapsto_timeless l q v : Timeless (l↦{q}v).
+  Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
+
+  Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
+  Proof.
+    intros p q.
+    by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton pair_op agree_idemp.
+  Qed.
+  Global Instance heap_mapsto_as_fractional l q v:
+    AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
+  Proof. split. done. apply _. Qed.
+
+  Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
+  Proof. rewrite /heap_mapsto_vec. apply _. Qed.
+
+  Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
+  Proof.
+    intros p q. rewrite /heap_mapsto_vec -big_sepL_sepL.
+    by setoid_rewrite (fractional (Φ := λ q, _ ↦{q} _)%I).
+  Qed.
+  Global Instance heap_mapsto_vec_as_fractional l q vl:
+    AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
+  Proof. split. done. apply _. Qed.
+
+  Global Instance heap_freeable_timeless q l n : Timeless (†{q}l…n).
+  Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
+
+  Lemma heap_mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
+  Proof.
+    rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+    eapply pure_elim; [done|]=> /auth_own_valid /=.
+    rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
+  Qed.
+
+  Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
+  Proof. by rewrite /heap_mapsto_vec. Qed.
+
+  Lemma heap_mapsto_vec_app l q vl1 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.
+  Qed.
+
+  Lemma heap_mapsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
+  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 ∗ (l +ₗ 1) ↦∗{q} vl.
+  Proof.
+    by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
+  Qed.
+
+  Lemma heap_mapsto_vec_op l q1 q2 vl1 vl2 :
+    length vl1 = length vl2 →
+    l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ ⌜vl1 = vl2⌝ ∧ l ↦∗{q1+q2} vl1.
+  Proof.
+    intros Hlen%Forall2_same_length. apply (anti_symm (⊢)).
+    - 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 (l +ₗ 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
+      rewrite (inj_iff (:: vl2)).
+      iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
+      iSplit; first done. iFrame.
+    - by iIntros "[% [$ Hl2]]"; subst.
+  Qed.
+
+  Lemma heap_mapsto_pred_op l q1 q2 n (Φ : list val → iProp Σ) :
+    (∀ vl, Φ vl -∗ ⌜length vl = n⌝) →
+    l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = n⌝) ⊣⊢ l ↦∗{q1+q2}: Φ.
+  Proof.
+    intros Hlen. iSplit.
+    - iIntros "[Hmt1 Hmt2]".
+      iDestruct "Hmt1" as (vl) "[Hmt1 Hown]". iDestruct "Hmt2" as (vl') "[Hmt2 %]".
+      iDestruct (Hlen with "Hown") as %?.
+      iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op; last congruence.
+      iDestruct "Hmt" as "[_ Hmt]". iExists vl. by iFrame.
+    - iIntros "Hmt". iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
+      iDestruct (Hlen with "Hown") as %?.
+      iSplitL "Hmt1 Hown"; iExists _; by iFrame.
+  Qed.
+
+  Lemma heap_mapsto_pred_wand l q Φ1 Φ2 :
+    l ↦∗{q}: Φ1 -∗ (∀ vl, Φ1 vl -∗ Φ2 vl) -∗ l ↦∗{q}: Φ2.
+  Proof.
+    iIntros "Hm Hwand". iDestruct "Hm" as (vl) "[Hm HΦ]". iExists vl.
+    iFrame "Hm". by iApply "Hwand".
+  Qed.
+
+  Lemma heap_mapsto_pred_iff_proper l q Φ1 Φ2 :
+    □ (∀ vl, Φ1 vl ↔ Φ2 vl) -∗ □ (l ↦∗{q}: Φ1 ↔ l ↦∗{q}: Φ2).
+  Proof.
+    iIntros "#HΦ !#". iSplit; iIntros; iApply (heap_mapsto_pred_wand with "[-]"); try done; [|];
+    iIntros; by iApply "HΦ".
+  Qed.
+
+  Lemma heap_mapsto_vec_combine l q vl :
+    vl ≠ [] →
+    l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl,
+      {[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 //.
+  Qed.
+
+  Global Instance heap_mapsto_pred_fractional l (P : list val → iProp Σ):
+    (∀ vl, Persistent (P vl)) → Fractional (λ q, l ↦∗{q}: P)%I.
+  Proof.
+    intros p q q'. iSplit.
+    - iIntros "H". iDestruct "H" as (vl) "[[Hown1 Hown2] #HP]".
+      iSplitL "Hown1"; eauto.
+    - iIntros "[H1 H2]". iDestruct "H1" as (vl1) "[Hown1 #HP1]".
+      iDestruct "H2" as (vl2) "[Hown2 #HP2]".
+      set (ll := min (length vl1) (length vl2)).
+      rewrite -[vl1](firstn_skipn ll) -[vl2](firstn_skipn ll) 2!heap_mapsto_vec_app.
+      iDestruct "Hown1" as "[Hown1 _]". iDestruct "Hown2" as "[Hown2 _]".
+      iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_vec_op; last first.
+      { rewrite !firstn_length. subst ll.
+        rewrite -!min_assoc min_idempotent min_comm -min_assoc min_idempotent min_comm. done. }
+      iDestruct "Hown" as "[H Hown]". iDestruct "H" as %Hl. iExists (take ll vl1). iFrame.
+      destruct (min_spec (length vl1) (length vl2)) as [[Hne Heq]|[Hne Heq]].
+      + iClear "HP2". rewrite take_ge; last first.
+        { rewrite -Heq /ll. done. }
+        rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
+      + iClear "HP1". rewrite Hl take_ge; last first.
+        { rewrite -Heq /ll. done. }
+        rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
+  Qed.
+  Global Instance heap_mapsto_pred_as_fractional l q (P : list val → iProp Σ):
+    (∀ vl, Persistent (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
+  Proof. split. done. apply _. Qed.
+
+  Lemma inter_lookup_Some i j (n : nat):
+    i ≤ j < i+n → inter i n !! j = Excl' ().
+  Proof.
+    revert i. induction n as [|n IH]=>/= i; first lia.
+    rewrite lookup_insert_Some. destruct (decide (i = j)); naive_solver lia.
+  Qed.
+  Lemma inter_lookup_None i j (n : nat):
+    j < i ∨ i+n ≤ j → inter i n !! j = None.
+  Proof.
+    revert i. induction n as [|n IH]=>/= i; first by rewrite lookup_empty.
+    rewrite lookup_insert_None. naive_solver lia.
+  Qed.
+  Lemma inter_op i n n' : inter i n ⋅ inter (i+n) n' ≡ inter i (n+n').
+  Proof.
+    intros j. rewrite lookup_op.
+    destruct (decide (i ≤ j < i+n)); last destruct (decide (i+n ≤ j < i+n+n')).
+    - by rewrite (inter_lookup_None (i+n) j n') ?inter_lookup_Some; try lia.
+    - by rewrite (inter_lookup_None i j n) ?inter_lookup_Some; try lia.
+    - by rewrite !inter_lookup_None; try lia.
+  Qed.
+  Lemma inter_valid i n : ✓ inter i n.
+  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}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.
+  Qed.
+
+  (** Properties about heap_freeable_rel and heap_freeable *)
+  Lemma heap_freeable_rel_None σ l 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].
+    destruct (map_choose s) as [i []%REL'%not_eq_None_Some]; first done.
+    move: (FRESH (i - l.2)). by rewrite /shift_loc Zplus_minus.
+  Qed.
+
+  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 (σ !! (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.
+    destruct (decide (0 ≤ i ∧ i < n)).
+    - rewrite is_Some_alt inter_lookup_Some; lia.
+    - rewrite is_Some_alt inter_lookup_None; lia.
+  Qed.
+
+  Lemma heap_freeable_rel_init_mem l h n σ:
+    n ≠ O →
+    (∀ m : Z, σ !! (l +ₗ m) = None) →
+    heap_freeable_rel σ h →
+    heap_freeable_rel (init_mem l n σ)
+                      (<[l.1 := (1%Qp, inter (l.2) n)]> h).
+  Proof.
+    move=> Hvlnil FRESH REL blk qs /lookup_insert_Some [[<- <-]|[??]].
+    - split.
+      { destruct n as [|n]; simpl in *; [done|]. apply: insert_non_empty. }
+      intros i. destruct (decide (l.2 ≤ i ∧ i < l.2 + n)).
+      + rewrite inter_lookup_Some // lookup_init_mem; naive_solver.
+      + rewrite inter_lookup_None; last lia. rewrite lookup_init_mem_ne /=; last 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.
+  Qed.
+
+  Lemma heap_freeable_rel_free_mem σ hF n l :
+    hF !! l.1 = Some (1%Qp, inter (l.2) n) →
+    heap_freeable_rel σ hF →
+    heap_freeable_rel (free_mem l n σ) (delete (l.1) hF).
+  Proof.
+    intros Hl REL b qs; rewrite lookup_delete_Some=> -[NEQ ?].
+    destruct (REL b qs) as [? REL']; auto.
+    split; [done|]=> i. by rewrite -REL' lookup_free_mem_ne.
+  Qed.
+
+  Lemma heap_freeable_rel_stable σ h l p :
+    heap_freeable_rel σ h → is_Some (σ !! l) →
+    heap_freeable_rel (<[l := p]>σ) h.
+  Proof.
+    intros REL Hσ blk qs Hqs. destruct (REL blk qs) as [? REL']; first done.
+    split; [done|]=> i. rewrite -REL' lookup_insert_is_Some.
+    destruct (decide (l = (blk, i))); naive_solver.
+  Qed.
+
+  (** Weakest precondition *)
+  Lemma heap_alloc_vs σ l n :
+    (∀ m : Z, σ !! (l +ₗ m) = None) →
+    own heap_name (● to_heap σ)
+    ==∗ own heap_name (● to_heap (init_mem l n σ))
+       ∗ own heap_name (◯ [^op list] i ↦ v ∈ (repeat (LitV LitPoison) n),
+           {[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 n as [|n IH]=> l FRESH; [done|].
+    rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=.
+    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' ?.
+      rewrite lookup_singleton_None -{2}(shift_loc_0 l). apply not_inj; lia. }
+    rewrite to_heap_insert. setoid_rewrite shift_loc_assoc.
+    apply alloc_local_update; last done. apply lookup_to_heap_None.
+    rewrite lookup_init_mem_ne /=; last lia. by rewrite -(shift_loc_0 l) FRESH.
+  Qed.
+
+  Lemma heap_alloc σ l n :
+    0 < n →
+    (∀ m, σ !! (l +ₗ m) = None) →
+    heap_ctx σ ==∗
+      heap_ctx (init_mem l (Z.to_nat n) σ) ∗ †l…(Z.to_nat n) ∗
+      l ↦∗ repeat (LitV LitPoison) (Z.to_nat n).
+  Proof.
+    intros ??; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
+    assert (Z.to_nat n ≠ O). { rewrite -(Nat2Z.id 0)=>/Z2Nat.inj. lia. }
+    iMod (heap_alloc_vs _ _ (Z.to_nat n) with "[$Hvalσ]") as "[Hvalσ Hmapsto]"; first done.
+    iMod (own_update _ (● hF) with "HhF") as "[HhF Hfreeable]".
+    { apply auth_update_alloc,
+        (alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
+      - eauto using heap_freeable_rel_None.
+      - split. done. apply inter_valid. }
+    iModIntro. iSplitL "Hvalσ HhF".
+    { iExists _. iFrame. iPureIntro.
+      auto using heap_freeable_rel_init_mem. }
+    rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //.
+    iFrame. destruct (Z.to_nat n); done.
+  Qed.
+
+  Lemma heap_free_vs σ l vl :
+    own heap_name (● to_heap σ) ∗ own heap_name (◯ [^op list] i ↦ v ∈ vl,
+      {[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.
+    revert σ l. induction vl as [|v vl IH]=> σ l; [done|].
+    rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /= shift_loc_0.
+    apply local_update_total_valid=> _ Hvalid _.
+    assert (([^op list] k↦y ∈ vl,
+      {[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.
+    { apply (delete_local_update _ _ l (1%Qp, Cinr 0%nat, to_agree v)).
+      by rewrite lookup_insert. }
+    rewrite delete_insert // -to_heap_delete delete_free_mem.
+    setoid_rewrite <-shift_loc_assoc. apply IH.
+  Qed.
+
+  Lemma heap_free σ l vl (n : Z) :
+    n = length vl →
+    heap_ctx σ -∗ l ↦∗ vl -∗ †l…(length vl)
+    ==∗ ⌜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.
+    iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
+    iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_valid_discrete_2.
+    move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
+    apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
+    { move: (Hv (l.1)). rewrite Hl. by intros [??]. }
+    assert (vl ≠ []).
+    { intros ->. by destruct (REL (l.1) (1%Qp, ∅)) as [[] ?]. }
+    assert (0 < n) by (subst n; by destruct vl).
+    iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
+    { rewrite heap_mapsto_vec_combine //. iFrame. }
+    iMod (own_update_2 with "HhF Hf") as "HhF".
+    { apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
+    iModIntro; subst. repeat iSplit;  eauto using heap_freeable_is_Some.
+    iExists _. subst. rewrite Nat2Z.id. iFrame.
+    eauto using heap_freeable_rel_free_mem.
+  Qed.
+
+  Lemma heap_mapsto_lookup σ l ls q v :
+    own heap_name (● to_heap σ) -∗
+    own heap_name (◯ {[ l := (q, to_lock_stateR ls, to_agree v) ]}) -∗
+    ⌜∃ n' : nat,
+        σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
+  Proof.
+    iIntros "H● H◯".
+    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
+    iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
+    rewrite /to_heap lookup_fmap fmap_Some_equiv.
+    move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
+    move=> /Some_pair_included_total_2
+      [/Some_pair_included [_ Hincl] /to_agree_included->].
+    destruct ls as [|n], ls'' as [|n''],
+       Hincl as [[[|n'|]|] [=]%leibniz_equiv]; subst.
+    by exists O. eauto. exists O. by rewrite Nat.add_0_r.
+  Qed.
+
+  Lemma heap_mapsto_lookup_1 σ l ls v :
+    own heap_name (● to_heap σ) -∗
+    own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, to_agree v) ]}) -∗
+    ⌜σ !! l = Some (ls, v)⌝.
+  Proof.
+    iIntros "H● H◯".
+    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
+    iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
+    rewrite /to_heap lookup_fmap fmap_Some_equiv.
+    move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
+    apply (Some_included_exclusive _ _) in Hincl as [? Hval]; last by destruct ls''.
+    apply (inj to_agree) in Hval. fold_leibniz. subst.
+    destruct ls, ls''; rewrite ?Nat.add_0_r; naive_solver.
+  Qed.
+
+  Lemma heap_read_vs σ n1 n2 nf l q v:
+    σ !! l = Some (RSt (n1 + nf), v) →
+    own heap_name (● to_heap σ) -∗ heap_mapsto_st (RSt n1) l q v
+    ==∗ own heap_name (● to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
+        ∗ heap_mapsto_st (RSt n2) l q v.
+  Proof.
+    intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
+    eapply own_update, auth_update, singleton_local_update.
+    { by rewrite /to_heap lookup_fmap Hσv. }
+    apply prod_local_update_1, prod_local_update_2, csum_local_update_r.
+    apply nat_local_update; lia.
+  Qed.
+
+  Lemma heap_read σ l q v :
+    heap_ctx σ -∗ l ↦{q} v -∗ ∃ n, ⌜σ !! l = Some (RSt n, v)⌝.
+  Proof.
+    iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
+    rewrite heap_mapsto_eq.
+    iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+  Qed.
+
+  Lemma heap_read_1 σ l v :
+    heap_ctx σ -∗ l ↦ v -∗ ⌜σ !! l = Some (RSt 0, v)⌝.
+  Proof.
+    iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
+    rewrite heap_mapsto_eq.
+    iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; auto.
+  Qed.
+
+  Lemma heap_read_na σ l q v :
+    heap_ctx σ -∗ l ↦{q} v ==∗ ∃ n,
+      ⌜σ !! l = Some (RSt n, v)⌝ ∗
+      heap_ctx (<[l:=(RSt (S n), v)]> σ) ∗
+      ∀ σ2, heap_ctx σ2 ==∗ ∃ n2, ⌜σ2 !! l = Some (RSt (S n2), v)⌝ ∗
+        heap_ctx (<[l:=(RSt n2, v)]> σ2) ∗ l ↦{q} v.
+  Proof.
+    iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
+    rewrite heap_mapsto_eq.
+    iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+    iMod (heap_read_vs _ 0 1 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+    iModIntro. iExists n; iSplit; [done|]. iSplitL "HhF Hσ".
+    { iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
+    clear dependent n σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)".
+    iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+    iMod (heap_read_vs _ 1 0 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+    iExists n; iModIntro; iSplit; [done|]. iFrame "Hmt".
+    iExists hF. iFrame. eauto using heap_freeable_rel_stable.
+  Qed.
+
+  Lemma heap_write_vs σ st1 st2 l v v':
+    σ !! l = Some (st1, v) →
+    own heap_name (● to_heap σ) -∗ heap_mapsto_st st1 l 1%Qp v
+    ==∗ own heap_name (● to_heap (<[l:=(st2, v')]> σ))
+        ∗ heap_mapsto_st st2 l 1%Qp v'.
+  Proof.
+    intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
+    eapply own_update, auth_update, singleton_local_update.
+    { by rewrite /to_heap lookup_fmap Hσv. }
+    apply exclusive_local_update. by destruct st2.
+  Qed.
+
+  Lemma heap_write σ l v v' :
+    heap_ctx σ -∗ l ↦ v ==∗ heap_ctx (<[l:=(RSt 0, v')]> σ) ∗ l ↦ v'.
+  Proof.
+    iDestruct 1 as (hF) "(Hσ & HhF & %)". iIntros "Hmt".
+    rewrite heap_mapsto_eq.
+    iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; auto.
+    iMod (heap_write_vs with "Hσ Hmt") as "[Hσ $]"; first done.
+    iModIntro. iExists _. iFrame. eauto using heap_freeable_rel_stable.
+  Qed.
+
+  Lemma heap_write_na σ l v v' :
+    heap_ctx σ -∗ l ↦ v ==∗
+      ⌜σ !! l = Some (RSt 0, v)⌝ ∗
+      heap_ctx (<[l:=(WSt, v)]> σ) ∗
+      ∀ σ2, heap_ctx σ2 ==∗ ⌜σ2 !! l = Some (WSt, v)⌝ ∗
+        heap_ctx (<[l:=(RSt 0, v')]> σ2) ∗ l ↦ v'.
+  Proof.
+    iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
+    rewrite heap_mapsto_eq.
+    iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; eauto.
+    iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+    iModIntro. iSplit; [done|]. iSplitL "HhF Hσ".
+    { iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
+    clear dependent σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)".
+    iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+    iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+    iModIntro; iSplit; [done|]. iFrame "Hmt".
+    iExists hF. iFrame. eauto using heap_freeable_rel_stable.
+  Qed.
+End heap.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
new file mode 100644
index 0000000000000000000000000000000000000000..c302a1c3cd70ba189f75aab431796d9ad51a9fbf
--- /dev/null
+++ b/theories/lang/lang.v
@@ -0,0 +1,660 @@
+From iris.program_logic Require Export language ectx_language ectxi_language.
+From stdpp Require Export strings.
+From stdpp Require Import gmap.
+Set Default Proof Using "Type".
+
+Open Scope Z_scope.
+
+(** Expressions and vals. *)
+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 :=
+| LitPoison | LitLoc (l : loc) | LitInt (n : Z).
+Inductive bin_op : Set :=
+| PlusOp | MinusOp | LeOp | EqOp | OffsetOp.
+Inductive order : Set :=
+| ScOrd | Na1Ord | Na2Ord.
+
+Inductive binder := BAnon | BNamed : string → binder.
+Delimit Scope lrust_binder_scope with RustB.
+Bind Scope lrust_binder_scope with binder.
+
+Notation "[ ]" := (@nil binder) : lrust_binder_scope.
+Notation "a :: b" := (@cons binder a%RustB b%RustB)
+  (at level 60, right associativity) : lrust_binder_scope.
+Notation "[ x1 ; x2 ; .. ; xn ]" :=
+  (@cons binder x1%RustB (@cons binder x2%RustB
+        (..(@cons binder xn%RustB (@nil binder))..))) : lrust_binder_scope.
+Notation "[ x ]" := (@cons binder x%RustB (@nil binder)) : lrust_binder_scope.
+
+Definition cons_binder (mx : binder) (X : list string) : list string :=
+  match mx with BAnon => X | BNamed x => x :: X end.
+Infix ":b:" := cons_binder (at level 60, right associativity).
+Fixpoint app_binder (mxl : list binder) (X : list string) : list string :=
+  match mxl with [] => X | b :: mxl => b :b: app_binder mxl X end.
+Infix "+b+" := app_binder (at level 60, right associativity).
+Instance binder_dec_eq : EqDecision binder.
+Proof. solve_decision. Defined.
+
+Instance set_unfold_cons_binder x mx X P :
+  SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).
+Proof.
+  constructor. rewrite -(set_unfold (x ∈ X) P).
+  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
+Qed.
+Instance set_unfold_app_binder x mxl X P :
+  SetUnfold (x ∈ X) P → SetUnfold (x ∈ mxl +b+ X) (BNamed x ∈ mxl ∨ P).
+Proof.
+  constructor. rewrite -(set_unfold (x ∈ X) P).
+  induction mxl as [|?? IH]; set_solver.
+Qed.
+
+Inductive expr :=
+| Var (x : string)
+| Lit (l : base_lit)
+| Rec (f : binder) (xl : list binder) (e : expr)
+| BinOp (op : bin_op) (e1 e2 : expr)
+| App (e : expr) (el : list expr)
+| Read (o : order) (e : expr)
+| Write (o : order) (e1 e2: expr)
+| CAS (e0 e1 e2 : expr)
+| Alloc (e : expr)
+| Free (e1 e2 : expr)
+| Case (e : expr) (el : list expr)
+| Fork (e : expr).
+
+Arguments App _%E _%E.
+Arguments Case _%E _%E.
+
+Fixpoint is_closed (X : list string) (e : expr) : bool :=
+  match e with
+  | Var x => bool_decide (x ∈ X)
+  | Lit _ => true
+  | Rec f xl e => is_closed (f :b: xl +b+ X) e
+  | BinOp _ e1 e2 | Write _ e1 e2 | Free e1 e2 =>
+    is_closed X e1 && is_closed X e2
+  | App e el | Case e el => is_closed X e && forallb (is_closed X) el
+  | Read _ e | Alloc e | Fork e => is_closed X e
+  | CAS e0 e1 e2 => is_closed X e0 && is_closed X e1 && is_closed X e2
+  end.
+
+Class Closed (X : list string) (e : expr) := closed : is_closed X e.
+Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
+Proof. rewrite /Closed. apply _. Qed.
+Instance closed_decision env e : Decision (Closed env e).
+Proof. rewrite /Closed. apply _. Qed.
+
+Inductive val :=
+| LitV (l : base_lit)
+| RecV (f : binder) (xl : list binder) (e : expr) `{!Closed (f :b: xl +b+ []) e}.
+
+Bind Scope val_scope with val.
+
+Definition of_val (v : val) : expr :=
+  match v with
+  | RecV f x e => Rec f x e
+  | LitV l => Lit l
+  end.
+
+Definition to_val (e : expr) : option val :=
+  match e with
+  | Rec f xl e =>
+    if decide (Closed (f :b: xl +b+ []) e) then Some (RecV f xl e) else None
+  | Lit l => Some (LitV l)
+  | _ => None
+  end.
+
+(** The state: heaps of vals*lockstate. *)
+Inductive lock_state :=
+| WSt | RSt (n : nat).
+Definition state := gmap loc (lock_state * val).
+
+(** Evaluation contexts *)
+Inductive ectx_item :=
+| BinOpLCtx (op : bin_op) (e2 : expr)
+| BinOpRCtx (op : bin_op) (v1 : val)
+| AppLCtx (e2 : list expr)
+| AppRCtx (v : val) (vl : list val) (el : list expr)
+| ReadCtx (o : order)
+| WriteLCtx (o : order) (e2 : expr)
+| WriteRCtx (o : order) (v1 : val)
+| CasLCtx (e1 e2: expr)
+| CasMCtx (v0 : val) (e2 : expr)
+| CasRCtx (v0 : val) (v1 : val)
+| AllocCtx
+| FreeLCtx (e2 : expr)
+| FreeRCtx (v1 : val)
+| CaseCtx (el : list expr).
+
+Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
+  match Ki with
+  | BinOpLCtx op e2 => BinOp op e e2
+  | BinOpRCtx op v1 => BinOp op (of_val v1) e
+  | AppLCtx e2 => App e e2
+  | AppRCtx v vl el => App (of_val v) ((of_val <$> vl) ++ e :: el)
+  | ReadCtx o => Read o e
+  | WriteLCtx o e2 => Write o e e2
+  | WriteRCtx o v1 => Write o (of_val v1) e
+  | CasLCtx e1 e2 => CAS e e1 e2
+  | CasMCtx v0 e2 => CAS (of_val v0) e e2
+  | CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
+  | AllocCtx => Alloc e
+  | FreeLCtx e2 => Free e e2
+  | FreeRCtx v1 => Free (of_val v1) e
+  | CaseCtx el => Case e el
+  end.
+
+(** Substitution *)
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | Var y => if bool_decide (y = x) then es else Var y
+  | Lit l => Lit l
+  | Rec f xl e =>
+    Rec f xl $ if bool_decide (BNamed x ≠ f ∧ BNamed x ∉ xl) then subst x es e else e
+  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
+  | App e el => App (subst x es e) (map (subst x es) el)
+  | Read o e => Read o (subst x es e)
+  | Write o e1 e2 => Write o (subst x es e1) (subst x es e2)
+  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
+  | Alloc e => Alloc (subst x es e)
+  | Free e1 e2 => Free (subst x es e1) (subst x es e2)
+  | Case e el => Case (subst x es e) (map (subst x es) el)
+  | Fork e => Fork (subst x es e)
+  end.
+
+Definition subst' (mx : binder) (es : expr) : expr → expr :=
+  match mx with BNamed x => subst x es | BAnon => id end.
+
+Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :=
+  match xl, esl with
+  | [], [] => Some e
+  | x::xl, es::esl => subst' x es <$> subst_l xl esl e
+  | _, _ => None
+  end.
+Arguments subst_l _%RustB _ _%E.
+
+Definition subst_v (xl : list binder) (vsl : vec val (length xl))
+                   (e : expr) : expr :=
+  Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl.
+Arguments subst_v _%RustB _ _%E.
+
+Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
+  Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.
+Proof.
+  revert vsl. induction xl=>/= vsl; inv_vec vsl=>//=v vsl. by rewrite -IHxl.
+Qed.
+
+(** The stepping relation *)
+(* Be careful to make sure that poison is always stuck when used for anything
+   except for reading from or writing to memory! *)
+Definition Z_of_bool (b : bool) : Z :=
+  if b then 1 else 0.
+
+Definition lit_of_bool (b : bool) : base_lit :=
+  LitInt $ Z_of_bool b.
+
+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) : loc_scope.
+
+Fixpoint init_mem (l:loc) (n:nat) (σ:state) : state :=
+  match n with
+  | O => σ
+  | S n => <[l:=(RSt 0, LitV LitPoison)]>(init_mem (l +ₗ 1) n σ)
+  end.
+
+Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
+  match n with
+  | O => σ
+  | S n => delete l (free_mem (l +ₗ 1) n σ)
+  end.
+
+Inductive lit_eq (σ : state) : base_lit → base_lit → Prop :=
+(* No refl case for poison *)
+| IntRefl z : lit_eq σ (LitInt z) (LitInt z)
+| LocRefl l : lit_eq σ (LitLoc l) (LitLoc l)
+(* Comparing unallocated pointers can non-deterministically say they are equal
+   even if they are not.  Given that our `free` actually makes addresses
+   re-usable, this may not be strictly necessary, but it is the most
+   conservative choice that avoids UB (and we cannot use UB as this operation is
+   possible in safe Rust).  See
+   <https://internals.rust-lang.org/t/comparing-dangling-pointers/3019> for some
+   more background. *)
+| 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 : 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)
+| LocNeqNullR l :
+    lit_neq (LitLoc l) (LitInt 0)
+| LocNeqNullL l :
+    lit_neq (LitInt 0) (LitLoc l).
+
+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 $ l +ₗ z).
+
+Definition stuck_term := App (Lit $ LitInt 0) [].
+
+Inductive head_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
+| BinOpS op l1 l2 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 →
+    Closed (f :b: xl +b+ []) e →
+    subst_l (f::xl) (Rec f xl e :: el) e = Some e' →
+    head_step (App (Rec f xl e) el) σ [] e' σ []
+| ReadScS l n v σ:
+    σ !! l = Some (RSt n, v) →
+    head_step (Read ScOrd (Lit $ LitLoc l)) σ [] (of_val v) σ []
+| ReadNa1S l n v σ:
+    σ !! l = Some (RSt n, v) →
+    head_step (Read Na1Ord (Lit $ LitLoc l)) σ
+              []
+              (Read Na2Ord (Lit $ LitLoc l)) (<[l:=(RSt $ S n, v)]>σ)
+              []
+| ReadNa2S l n v σ:
+    σ !! l = Some (RSt $ S n, v) →
+    head_step (Read Na2Ord (Lit $ LitLoc l)) σ
+              []
+              (of_val v) (<[l:=(RSt n, v)]>σ)
+              []
+| WriteScS l e v v' σ:
+    to_val e = Some v →
+    σ !! l = Some (RSt 0, v') →
+    head_step (Write ScOrd (Lit $ LitLoc l) e) σ
+              []
+              (Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
+              []
+| WriteNa1S l e v v' σ:
+    to_val e = Some v →
+    σ !! l = Some (RSt 0, v') →
+    head_step (Write Na1Ord (Lit $ LitLoc l) e) σ
+              []
+              (Write Na2Ord (Lit $ LitLoc l) e) (<[l:=(WSt, v')]>σ)
+              []
+| WriteNa2S l e v v' σ:
+    to_val e = Some v →
+    σ !! l = Some (WSt, v') →
+    head_step (Write Na2Ord (Lit $ LitLoc l) e) σ
+              []
+              (Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
+              []
+| 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 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, LitV lit2)]>σ)
+              []
+(* A succeeding CAS has to detect concurrent non-atomic read accesses, and
+   trigger UB if there is one.  In lambdaRust, succeeding and failing CAS are
+   not mutually exclusive, so it could happen that a CAS can both fail (and
+   hence not be stuck) but also succeed (and hence be racing with a concurrent
+   non-atomic read).  In that case, we have to explicitly reduce to a stuck
+   state; due to the possibility of failing CAS, we cannot rely on the current
+   state being stuck like we could in a language where failing and succeeding
+   CAS are mutually exclusive.
+
+   This means that CAS is atomic (it always reducs to an irreducible
+   expression), but not strongly atomic (it does not always reduce to a value).
+
+   If there is a concurrent non-atomic write, the CAS itself is stuck: All its
+   reductions are blocked.  *)
+| 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 σ :
+    0 < n →
+    (∀ m, σ !! (l +ₗ m) = None) →
+    head_step (Alloc $ Lit $ LitInt n) σ
+              []
+              (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ)
+              []
+| FreeS n l σ :
+    0 < n →
+    (∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) →
+    head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
+              []
+              (Lit LitPoison) (free_mem l (Z.to_nat n) σ)
+              []
+| CaseS i el e σ :
+    0 ≤ i →
+    el !! (Z.to_nat i) = Some e →
+    head_step (Case (Lit $ LitInt i) el) σ [] e σ []
+| ForkS e σ:
+    head_step (Fork e) σ [] (Lit LitPoison) σ [e].
+
+(** Basic properties about the language *)
+Lemma to_of_val v : to_val (of_val v) = Some v.
+Proof.
+  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
+Qed.
+
+Lemma of_to_val e v : to_val e = Some v → of_val v = e.
+Proof.
+  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
+Qed.
+
+Instance of_val_inj : Inj (=) (=) of_val.
+Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
+
+Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
+
+Lemma fill_item_val Ki e :
+  is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
+Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
+
+Lemma val_stuck e1 σ1 κ e2 σ2 ef :
+  head_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
+Proof. destruct 1; naive_solver. Qed.
+
+Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 ef :
+  head_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
+Proof.
+  destruct Ki; inversion_clear 1; decompose_Forall_hyps;
+    simplify_option_eq; by eauto.
+Qed.
+
+Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
+  to_val e1 = None → to_val e2 = None →
+  map of_val vl1 ++ e1 :: el1 = map of_val vl2 ++ e2 :: el2 →
+  vl1 = vl2 ∧ el1 = el2.
+Proof.
+  revert vl2; induction vl1; destruct vl2; intros H1 H2; inversion 1.
+  - done.
+  - subst. by rewrite to_of_val in H1.
+  - subst. by rewrite to_of_val in H2.
+  - destruct (IHvl1 vl2); auto. split; f_equal; auto. by apply (inj of_val).
+Qed.
+
+Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
+  to_val e1 = None → to_val e2 = None →
+  fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
+Proof.
+  destruct Ki1 as [| | |v1 vl1 el1| | | | | | | | | |],
+           Ki2 as [| | |v2 vl2 el2| | | | | | | | | |];
+  intros He1 He2 EQ; try discriminate; simplify_eq/=;
+    repeat match goal with
+    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
+    end; auto.
+  destruct (list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2); auto. congruence.
+Qed.
+
+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 : 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) : l +ₗ n +ₗ n' = l +ₗ (n + n')%nat.
+Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
+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 : (l +ₗ n).1 = l.1.
+Proof. done. Qed.
+
+Lemma lookup_init_mem σ (l l' : loc) (n : nat) :
+  l.1 = l'.1 → l.2 ≤ l'.2 < l.2 + n →
+  init_mem l n σ !! l' = Some (RSt 0, LitV LitPoison).
+Proof.
+  intros ?. destruct l' as [? l']; simplify_eq/=.
+  revert l. induction n as [|n IH]=> /= l Hl; [lia|].
+  assert (l' = l.2 ∨ l.2 + 1 ≤ l') as [->|?] by lia.
+  { by rewrite -surjective_pairing lookup_insert. }
+  rewrite lookup_insert_ne; last by destruct l; intros ?; simplify_eq/=; lia.
+  rewrite -(shift_loc_block l 1) IH /=; last lia. done.
+Qed.
+
+Lemma lookup_init_mem_ne σ (l l' : loc) (n : nat) :
+  l.1 ≠ l'.1 ∨ l'.2 < l.2 ∨ l.2 + n ≤ l'.2 →
+  init_mem l n σ !! l' = σ !! l'.
+Proof.
+  revert l. induction n as [|n IH]=> /= l Hl; auto.
+  rewrite -(IH (l +ₗ 1)); last (simpl; intuition lia).
+  apply lookup_insert_ne. intros ->; intuition lia.
+Qed.
+
+Definition fresh_block (σ : state) : block :=
+  let loclst : list loc := elements (dom _ σ : gset loc) in
+  let blockset : gset block := foldr (λ l, ({[l.1]} ∪)) ∅ loclst in
+  fresh blockset.
+
+Lemma is_fresh_block σ i : σ !! (fresh_block σ,i) = None.
+Proof.
+  assert (∀ (l : loc) ls (X : gset block),
+    l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪)) X ls) as help.
+  { induction 1; set_solver. }
+  rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
+  move=> /(help _ _ ∅) /=. apply is_fresh.
+Qed.
+
+Lemma alloc_fresh n σ :
+  let l := (fresh_block σ, 0) in
+  let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in
+  0 < n →
+  head_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
+Proof.
+  intros l init Hn. apply AllocS. auto.
+  - intros i. apply (is_fresh_block _ i).
+Qed.
+
+Lemma lookup_free_mem_ne σ l l' n : l.1 ≠ l'.1 → free_mem l n σ !! l' = σ !! l'.
+Proof.
+  revert l. induction n as [|n IH]=> l ? //=.
+  rewrite lookup_delete_ne; last congruence.
+  apply IH. by rewrite shift_loc_block.
+Qed.
+
+Lemma delete_free_mem σ l l' n :
+  delete l (free_mem l' n σ) = free_mem l' n (delete l σ).
+Proof.
+  revert l'. induction n as [|n IH]=> l' //=. by rewrite delete_commute IH.
+Qed.
+
+(** Closed expressions *)
+Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
+Proof.
+  revert e X Y. fix FIX 1; destruct e=>X Y/=; try naive_solver.
+  - naive_solver set_solver.
+  - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
+    induction el=>/=; naive_solver.
+  - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
+    induction el=>/=; naive_solver.
+Qed.
+
+Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
+Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
+
+Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
+Proof.
+  revert e X. fix FIX 1; destruct e=> X /=; rewrite ?bool_decide_spec ?andb_True=> He ?;
+    repeat case_bool_decide; simplify_eq/=; f_equal;
+    try by intuition eauto with set_solver.
+  - case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
+    f_equal; intuition eauto with set_solver.
+  - case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
+    f_equal; intuition eauto with set_solver.
+Qed.
+
+Lemma is_closed_nil_subst e x es : is_closed [] e → subst x es e = e.
+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.
+
+Lemma is_closed_to_val X e v : to_val e = Some v → is_closed X e.
+Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
+
+Lemma subst_is_closed X x es e :
+  is_closed X es → is_closed (x::X) e → is_closed X (subst x es e).
+Proof.
+  revert e X. fix FIX 1; destruct e=>X //=; repeat (case_bool_decide=>//=);
+    try naive_solver; rewrite ?andb_True; intros.
+  - set_solver.
+  - eauto using is_closed_weaken with set_solver.
+  - eapply is_closed_weaken; first done.
+    destruct (decide (BNamed x = f)), (decide (BNamed x ∈ xl)); set_solver.
+  - split; first naive_solver. induction el; naive_solver.
+  - split; first naive_solver. induction el; naive_solver.
+Qed.
+
+Lemma subst'_is_closed X b es e :
+  is_closed X es → is_closed (b:b:X) e → is_closed X (subst' b es e).
+Proof. destruct b; first done. apply subst_is_closed. 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 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.
+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.
+Instance bin_op_dec_eq : EqDecision bin_op.
+Proof. solve_decision. Defined.
+Instance un_op_dec_eq : EqDecision order.
+Proof. solve_decision. Defined.
+
+Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
+  let fix expr_list_beq el el' :=
+    match el, el' with
+    | [], [] => true
+    | eh::eq, eh'::eq' => expr_beq eh eh' && expr_list_beq eq eq'
+    | _, _ => false
+    end
+  in
+  match e, e' with
+  | Var x, Var x' => bool_decide (x = x')
+  | Lit l, Lit l' => bool_decide (l = l')
+  | Rec f xl e, Rec f' xl' e' =>
+    bool_decide (f = f') && bool_decide (xl = xl') && expr_beq e e'
+  | BinOp op e1 e2, BinOp op' e1' e2' =>
+    bool_decide (op = op') && expr_beq e1 e1' && expr_beq e2 e2'
+  | App e el, App e' el' | Case e el, Case e' el' =>
+    expr_beq e e' && expr_list_beq el el'
+  | Read o e, Read o' e' => bool_decide (o = o') && expr_beq e e'
+  | Write o e1 e2, Write o' e1' e2' =>
+    bool_decide (o = o') && expr_beq e1 e1' && expr_beq e2 e2'
+  | CAS e0 e1 e2, CAS e0' e1' e2' =>
+    expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2'
+  | Alloc e, Alloc e' | Fork e, Fork e' => expr_beq e e'
+  | Free e1 e2, Free e1' e2' => expr_beq e1 e1' && expr_beq e2 e2'
+  | _, _ => false
+  end.
+Lemma expr_beq_correct (e1 e2 : expr) : expr_beq e1 e2 ↔ e1 = e2.
+Proof.
+  revert e1 e2; fix FIX 1.
+    destruct e1 as [| | | |? el1| | | | | |? el1|],
+             e2 as [| | | |? el2| | | | | |? el2|]; simpl; try done;
+  rewrite ?andb_True ?bool_decide_spec ?FIX;
+  try (split; intro; [destruct_and?|split_and?]; congruence).
+  - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
+    { revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
+      specialize (FIX el1h). naive_solver. }
+    clear FIX. naive_solver.
+  - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
+    { revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
+      specialize (FIX el1h). naive_solver. }
+    clear FIX. naive_solver.
+Qed.
+Instance expr_dec_eq : EqDecision expr.
+Proof.
+ refine (λ e1 e2, cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
+Defined.
+Instance val_dec_eq : EqDecision val.
+Proof.
+ refine (λ v1 v2, cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
+Defined.
+
+Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
+Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
+
+Canonical Structure stateC := leibnizC state.
+Canonical Structure valC := leibnizC val.
+Canonical Structure exprC := leibnizC expr.
+
+(** Language *)
+Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
+Proof.
+  split; apply _ || eauto using to_of_val, of_to_val,
+    val_stuck, fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
+Qed.
+Canonical Structure lrust_ectxi_lang := EctxiLanguage lrust_lang_mixin.
+Canonical Structure lrust_ectx_lang := EctxLanguageOfEctxi lrust_ectxi_lang.
+Canonical Structure lrust_lang := LanguageOfEctx lrust_ectx_lang.
+
+(* Lemmas about the language. *)
+Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ.
+Proof.
+  apply: (irreducible_fill (K:=ectx_language.fill K)); first done.
+  apply prim_head_irreducible; unfold stuck_term.
+  - inversion 1.
+  - apply ectxi_language_sub_redexes_are_values.
+    intros [] ??; simplify_eq/=; eauto; discriminate_list.
+Qed.
+
+(* Define some derived forms *)
+Notation Lam xl e := (Rec BAnon xl e) (only parsing).
+Notation Let x e1 e2 := (App (Lam [x] e2) [e1]) (only parsing).
+Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
+Notation LamV xl e := (RecV BAnon xl e) (only parsing).
+Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
+Notation SeqCtx e2 := (LetCtx BAnon e2).
+Notation Skip := (Seq (Lit LitPoison) (Lit LitPoison)).
+Coercion lit_of_bool : bool >-> base_lit.
+Notation If e0 e1 e2 := (Case e0 (@cons expr e2 (@cons expr e1 (@nil expr)))) (only parsing).
+Notation Newlft := (Lit LitPoison) (only parsing).
+Notation Endlft := Skip (only parsing).
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
deleted file mode 100644
index 14e394f0fa1d5f298e0838f42e0d2096c61265de..0000000000000000000000000000000000000000
--- a/theories/lang/lib/arc.v
+++ /dev/null
@@ -1,671 +0,0 @@
-From Coq.QArith Require Import Qcanon.
-From iris.base_logic.lib Require Import invariants.
-From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
-From iris.bi Require Import fractional.
-From iris.algebra Require Import excl csum frac auth.
-From lrust.lang Require Import proofmode notation new_delete.
-Set Default Proof Using "Type".
-
-(* JH: while working on Arc, I think figured that the "weak count
-locking" mechanism that Rust is using and that is verified below may
-not be necessary.
-
-Instead, what can be done in get_mut is the following:
-  - First, do a CAS on the strong count to put it to 0 from the expected
-value 1. This has the effect, at the same time, of ensuring that no one
-else has a strong reference, and of forbidding other weak references to
-be upgraded (since the strong count is now at 0). If the CAS fail,
-simply return None.
-  - Second, check the weak count. If it is at 1, then we are sure that
-we are the only owner.
-  - Third, in any case write 1 in the strong count to cancel the CAS.
-
-What's wrong with this protocol? The "only" problem I can see is that if
-someone tries to upgrade a weak after we did the CAS, then this will
-fail even though this could be possible.
-
-RJ: Upgrade failing spuriously sounds like a problem severe enough to
-justify the locking protocol.
-*)
-
-Definition strong_count : val :=
-  λ: ["l"], !ˢᶜ"l".
-
-Definition weak_count : val :=
-  λ: ["l"], !ˢᶜ("l" +ₗ #1).
-
-Definition clone_arc : val :=
-  rec: "clone" ["l"] :=
-    let: "strong" := !ˢᶜ"l" in
-    if: CAS "l" "strong" ("strong" + #1) then #☠ else "clone" ["l"].
-
-Definition clone_weak : val :=
-  rec: "clone" ["l"] :=
-    let: "weak" := !ˢᶜ("l" +ₗ #1) in
-    if: CAS ("l" +ₗ #1) "weak" ("weak" + #1) then #☠ else "clone" ["l"].
-
-Definition downgrade : val :=
-  rec: "downgrade" ["l"] :=
-    let: "weak" := !ˢᶜ("l" +ₗ #1) in
-    if: "weak" = #(-1) then
-      (* -1 in weak indicates that somebody locked the counts; let's spin. *)
-      "downgrade" ["l"]
-    else
-      if: CAS ("l" +ₗ #1) "weak" ("weak" + #1) then #☠
-      else "downgrade" ["l"].
-
-Definition upgrade : val :=
-  rec: "upgrade" ["l"] :=
-    let: "strong" := !ˢᶜ"l" in
-    if: "strong" = #0 then #false
-    else
-      if: CAS "l" "strong" ("strong" + #1) then #true
-      else "upgrade" ["l"].
-
-Definition drop_weak : val :=
-  rec: "drop" ["l"] :=
-    (* This can ignore the lock because the lock is only held when there
-       are no other weak refs in existence, so this code will never be called
-       with the lock held. *)
-    let: "weak" := !ˢᶜ("l" +ₗ #1) in
-    if: CAS ("l" +ₗ #1) "weak" ("weak" - #1) then "weak" = #1
-    else "drop" ["l"].
-
-Definition drop_arc : val :=
-  rec: "drop" ["l"] :=
-    let: "strong" := !ˢᶜ"l" in
-    if: CAS "l" "strong" ("strong" - #1) then "strong" = #1
-    else "drop" ["l"].
-
-Definition try_unwrap : val :=
-  λ: ["l"], CAS "l" #1 #0.
-
-Definition is_unique : val :=
-  λ: ["l"],
-    (* Try to acquire the lock for the last ref by CASing weak count from 1 to -1. *)
-    if: CAS ("l" +ₗ #1) #1 #(-1) then
-      let: "strong" := !ˢᶜ"l" in
-      let: "unique" := "strong" = #1 in
-      "l" +ₗ #1 <-ˢᶜ #1;;
-      "unique"
-    else
-      #false.
-
-Definition try_unwrap_full : val :=
-  λ: ["l"],
-    if: CAS "l" #1 #0 then
-      if: !ˢᶜ("l" +ₗ #1) = #1 then "l" <- #1;; #0
-      else #1
-    else #2.
-
-(** The CMRA we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
-
-(* See rc.v for understanding the structure of this CMRA.
-   The only additional thing is the [optionR (exclR unitC))], used to handle
-   properly the locking mechanisme for the weak count. *)
-Definition arc_stR :=
-  prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitC)))
-                          (exclR unitC))) natUR.
-Class arcG Σ :=
-  RcG :> inG Σ (authR arc_stR).
-Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
-Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
-Proof. solve_inG. Qed.
-
-Section def.
-  Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
-
-  Definition arc_tok γ q : iProp Σ :=
-    own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)).
-  Definition weak_tok γ : iProp Σ :=
-    own γ (◯ (None, 1%nat)).
-
-  Global Instance arc_tok_timeless γ q : Timeless (arc_tok γ q) := _.
-  Global Instance weak_tok_timeless γ : Timeless (weak_tok γ) := _.
-
-  Definition arc_inv (γ : gname) (l : loc) : iProp Σ :=
-    (∃ st : arc_stR, own γ (● st) ∗
-      match st with
-      | (Some (Cinl (q, strong, wlock)), weak) =>
-         ∃ q', ⌜(q + q')%Qp = 1%Qp⌝ ∗ P1 q' ∗ l ↦ #(Zpos strong) ∗
-           if wlock then (l +ₗ 1) ↦ #(-1) ∗ ⌜weak = 0%nat⌝
-           else (l +ₗ 1) ↦ #(S weak)
-      | (Some (Cinr _), weak) =>
-        l ↦ #0 ∗ (l +ₗ 1) ↦ #(S weak)
-      | (None, (S _) as weak) =>
-        l ↦ #0 ∗ (l +ₗ 1) ↦ #weak ∗ P2
-      | _ => True
-      end)%I.
-
-  Definition is_arc (γ : gname) (l : loc) : iProp Σ :=
-    inv N (arc_inv γ l).
-
-  Global Instance is_arc_persistent γ l : Persistent (is_arc γ l) := _.
-
-  Definition arc_tok_acc (γ : gname) P E : iProp Σ :=
-    (□ (P ={E,∅}=∗ ∃ q, arc_tok γ q ∗ (arc_tok γ q ={∅,E}=∗ P)))%I.
-
-  Definition weak_tok_acc (γ : gname) P E : iProp Σ :=
-    (□ (P ={E,∅}=∗ weak_tok γ ∗ (weak_tok γ ={∅,E}=∗ P)))%I.
-
-  Definition drop_spec (drop : val) P : iProp Σ :=
-    ({{{ P ∗ P1 1 }}} drop [] {{{ RET #☠; P ∗ P2 }}})%I.
-End def.
-
-Section arc.
-  (* P1 is the thing that is shared by strong reference owners (in practice,
-     this is the lifetime token), and P2 is the thing that is owned by the
-     protocol when only weak references are left (in practice, P2 is the
-     ownership of the underlying memory incl. deallocation). *)
-  Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
-          (P2 : iProp Σ) (N : namespace).
-
-  Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
-  Proof using HP1. done. Qed.
-
-  Global Instance arc_inv_ne n :
-    Proper (pointwise_relation _ (dist n) ==> dist n ==> eq ==> eq ==> dist n)
-           arc_inv.
-  Proof. solve_proper. Qed.
-  Global Instance arc_inv_proper :
-    Proper (pointwise_relation _ (≡) ==> (≡) ==> eq ==> eq ==> (≡))
-           arc_inv.
-  Proof. solve_proper. Qed.
-
-  Global Instance is_arc_contractive n :
-    Proper (pointwise_relation _ (dist_later n) ==> dist_later n ==> eq ==> eq ==> eq ==> dist n)
-           is_arc.
-  Proof. solve_contractive. Qed.
-  Global Instance is_arc_proper :
-    Proper (pointwise_relation _ (≡) ==> (≡) ==> eq ==> eq ==> eq ==> (≡)) is_arc.
-  Proof. solve_proper. Qed.
-
-  Lemma create_arc E l :
-    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']".
-    iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH, None), O) ⋅
-                      ◯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
-      as (γ) "[H● H◯]"; first done.
-    iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
-    rewrite Qp_div_2. auto.
-  Qed.
-
-  Lemma create_weak E l :
-    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.
-    iExists _. iFrame. iApply inv_alloc. iExists _. iFrame.
-  Qed.
-
-  Lemma arc_tok_auth_val st γ q :
-    own γ (● st) -∗ arc_tok γ q -∗
-    ⌜∃ q' strong wlock weak, st = (Some $ Cinl (q', strong, wlock), weak) ∧
-                             if decide (strong = xH) then q = q' ∧ wlock = None
-                             else ∃ q'', q' = (q + q'')%Qp⌝.
-  Proof.
-    iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
-        %[[Hincl%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
-    destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
-      simpl in *; subst.
-    - setoid_subst. iExists _, _, _, _. by iSplit.
-    - destruct Hincl as [->|[(?&[[??]?]&[=<-]&->&[[[??]%frac_included%Qp_lt_sum
-        ?%pos_included]%prod_included _]%prod_included)|(?&?&[=]&?)]]; first done.
-      iExists _, _, _, _. iSplit=>//. simpl in *. destruct decide; [subst;lia|eauto].
-  Qed.
-
-  Lemma strong_count_spec (γ : gname) (l : loc) (P : iProp Σ) :
-    is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
-    {{{ P }}} strong_count [ #l] {{{ (c : nat), RET #c; P ∗ ⌜(c > 0)%nat⌝ }}}.
-  Proof using HP1.
-    iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec.
-    iInv N as (st) "[>H● H]" "Hclose1".
-    iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]).
-    iDestruct "H" as (?) "(Hq & HP1 & H↦ & Hw)". wp_read.
-    iMod ("Hclose2" with "Hown") as "HP". iModIntro.
-    iMod ("Hclose1" with "[-HP HΦ]") as "_"; [iExists _; auto with iFrame|].
-    iModIntro. rewrite -positive_nat_Z. iApply "HΦ". auto with iFrame lia.
-  Qed.
-
-  (* FIXME : in the case the weak count is locked, we can possibly
-     return -1. This problem already exists in Rust. *)
-  Lemma weak_count_spec (γ : gname) (l : loc) (P : iProp Σ) :
-    is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
-    {{{ P }}} weak_count [ #l] {{{ (c : Z), RET #c; P ∗ ⌜c >= -1⌝ }}}.
-  Proof using HP1.
-    iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op.
-    iInv N as (st) "[>H● H]" "Hclose1".
-    iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &wl&?&[-> _]).
-    iDestruct "H" as (?) "(Hq & HP1 & H↦ & Hw)". destruct wl.
-    - iDestruct "Hw" as ">[Hw %]". wp_read.
-      iMod ("Hclose2" with "Hown") as "HP". iModIntro.
-      iMod ("Hclose1" with "[-HP HΦ]") as "_"; [iExists _; auto with iFrame|].
-      iApply "HΦ". auto with iFrame lia.
-    - wp_read. iMod ("Hclose2" with "Hown") as "HP". iModIntro.
-      iMod ("Hclose1" with "[-HP HΦ]") as "_"; [iExists _; auto with iFrame|].
-      iApply "HΦ". auto with iFrame lia.
-  Qed.
-
-  Lemma clone_arc_spec (γ : gname) (l : loc) (P : iProp Σ) :
-    is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
-    {{{ P }}} clone_arc [ #l]
-    {{{ q', RET #☠; P ∗ arc_tok γ q' ∗ P1 q' }}}.
-  Proof using HP1.
-    iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
-    iInv N as (st) "[>H● H]" "Hclose1".
-    iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(?& strong &?&?&[-> _]).
-    iDestruct "H" as (?) "(Hq & HP1 & H↦ & Hw)". wp_read.
-    iMod ("Hclose2" with "Hown") as "HP". iModIntro.
-    iMod ("Hclose1" with "[-HP HΦ]") as "_"; [iExists _; auto with iFrame|].
-    iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose1".
-    iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(?&strong'&?&?&[-> _]).
-    iDestruct "H" as (q) "(>#Hq & [HP1 HP1'] & Hl & Hw)". iDestruct "Hq" as %Hq.
-    destruct (decide (strong = strong')) as [->|?].
-    - wp_apply (wp_cas_int_suc with "Hl"). iIntros "Hl".
-      iMod (own_update with "H●") as "[H● Hown']".
-      { apply auth_update_alloc, prod_local_update_1,
-         (op_local_update_discrete _ _ (Some (Cinl ((q/2)%Qp, 1%positive, None))))
-           =>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
-        apply frac_valid'. rewrite -Hq comm_L -{2}(Qp_div_2 q).
-        apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
-        apply Qcplus_le_mono_r, Qp_ge_0. }
-      iMod ("Hclose2" with "Hown") as "HP". iModIntro.
-      iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
-      { iExists _. iFrame. iExists _. rewrite /= [xH ⋅ _]comm_L. iFrame.
-        rewrite [(q / 2)%Qp ⋅ _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
-      iModIntro. wp_case. iApply "HΦ". iFrame.
-    - wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
-      iMod ("Hclose2" with "Hown") as "HP". iModIntro.
-      iMod ("Hclose1" with "[-HP HΦ]") as "_".
-      { iExists _. iFrame. iExists q. auto with iFrame. }
-      iModIntro. wp_case. iApply ("IH" with "HP HΦ").
-  Qed.
-
-  Lemma downgrade_spec (γ : gname) (l : loc) (P : iProp Σ) :
-    is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
-    {{{ P }}} downgrade [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
-  Proof.
-    iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
-    iInv N as (st) "[>H● H]" "Hclose1".
-    iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak &[-> _]).
-    iMod ("Hclose2" with "Hown") as "HP". iModIntro.
-    iDestruct "H" as (?) "(? & ? & ? & Hw)". destruct wlock.
-    { iDestruct "Hw" as "(Hw & >%)". subst. wp_read.
-      iMod ("Hclose1" with "[-HP HΦ]") as "_"; first by iExists _; auto with iFrame.
-      iModIntro. wp_let. wp_op. wp_if. iApply ("IH" with "HP HΦ"). }
-    wp_read. iMod ("Hclose1" with "[-HP HΦ]") as "_"; first by iExists _; auto with iFrame.
-    iModIntro. wp_let. wp_op. wp_if. wp_op. wp_op. wp_bind (CAS _ _ _).
-    iInv N as (st) "[>H● H]" "Hclose1".
-    iApply fupd_wp. iMod ("Hacc" with "HP") as (?) "[Hown Hclose2]".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(?&?& wlock & weak' &[-> _]).
-    iMod ("Hclose2" with "Hown") as "HP". iModIntro.
-    iDestruct "H" as (q) "(>Heq & HP1 & Hl & Hl1)". iDestruct "Heq" as %Heq.
-    destruct (decide (weak = weak' ∧ wlock = None)) as [[<- ->]|Hw].
-    - wp_apply (wp_cas_int_suc with "Hl1"). iIntros "Hl1".
-      iMod (own_update with "H●") as "[H● Hown']".
-      { by apply auth_update_alloc, prod_local_update_2,
-              (op_local_update_discrete _ _ (1%nat)). }
-      iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_".
-      { iExists _. iFrame. iExists _.
-        rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. auto with iFrame. }
-      iModIntro. wp_case. iApply "HΦ". iFrame.
-    - destruct wlock.
-      + iDestruct "Hl1" as "[Hl1 >%]". subst.
-        wp_apply (wp_cas_int_fail with "Hl1"); [done..|].
-        iIntros "Hl1". iMod ("Hclose1" with "[-HP HΦ]") as "_".
-        { iExists _. auto with iFrame. }
-        iModIntro. wp_case. iApply ("IH" with "HP HΦ").
-      + wp_apply (wp_cas_int_fail with "Hl1").
-        { contradict Hw. split=>//. apply SuccNat2Pos.inj. lia. }
-        iIntros "Hl1". iMod ("Hclose1" with "[-HP HΦ]") as "_".
-        { iExists _. auto with iFrame. }
-        iModIntro. wp_case. iApply ("IH" with "HP HΦ").
-  Qed.
-
-  Lemma weak_tok_auth_val γ st :
-    own γ (● st) -∗ weak_tok γ -∗ ⌜∃ st' weak, st = (st', S weak) ∧ ✓ st'⌝.
-  Proof.
-    iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
-        %[[Hincl%option_included Hincl'%nat_included]%prod_included [Hval _]]
-         %auth_valid_discrete_2.
-    destruct st as [?[]], Hincl as [_|(?&?&[=]&?)]; simpl in *; try lia. eauto.
-  Qed.
-
-  Lemma clone_weak_spec (γ : gname) (l : loc) (P : iProp Σ) :
-    is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
-    {{{ 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, (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).
-      iMod ("Hclose2" with "Hown") as "HP".
-      destruct st' as [[[[??][?|]]| |]|]; try done; [|iExists _..].
-      - by iDestruct "H" as (?) "(_ & _ & _ & _ & >%)".
-      - iDestruct "H" as (?) "(? & ? & ? & >$)". iIntros "!>"; iSplit; iIntros "?".
-        + iMod (own_update with "H●") as "[H● $]".
-          { by apply auth_update_alloc, prod_local_update_2,
-                  (op_local_update_discrete _ _ (1%nat)). }
-          rewrite Z.add_comm -(Nat2Z.inj_add 1). iFrame.
-          iApply "Hclose1". iExists _. auto with iFrame.
-        + iFrame. iApply ("Hclose1" with "[-]"). iExists _. auto with iFrame.
-      - iDestruct "H" as "[? >$]". iIntros "!>"; iSplit; iIntros "?".
-        + iMod (own_update with "H●") as "[H● $]".
-          { by apply auth_update_alloc, prod_local_update_2,
-                  (op_local_update_discrete _ _ (1%nat)). }
-          rewrite Z.add_comm -(Nat2Z.inj_add 1). iFrame. iApply "Hclose1".
-          iExists _. auto with iFrame.
-        + iFrame. iApply ("Hclose1" with "[-]"). iExists _. auto with iFrame.
-      - iDestruct "H" as "(? & >$ & ?)". iIntros "!>"; iSplit; iIntros "?".
-        + iMod (own_update with "H●") as "[H● $]".
-          { by apply auth_update_alloc, prod_local_update_2,
-                  (op_local_update_discrete _ _ (1%nat)). }
-          rewrite Z.add_comm -(Nat2Z.inj_add 1). iFrame. iApply "Hclose1".
-          iExists _. auto with iFrame.
-        + iFrame. iApply ("Hclose1" with "[-]"). iExists _. auto with iFrame. }
-    iMod ("Hproto" with "HP") as (w) "[Hw [_ Hclose]]". wp_read.
-    iMod ("Hclose" with "Hw") as "HP". iModIntro. wp_let. wp_op. wp_op.
-    wp_bind (CAS _ _ _). iMod ("Hproto" with "HP") as (w') "[H↦ Hclose]".
-    destruct (decide (w = w')) as [<-|].
-    - wp_apply (wp_cas_int_suc with "H↦"). iIntros "H↦".
-      iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "H↦"). iModIntro.
-      wp_case. by iApply "HΦ".
-    - wp_apply (wp_cas_int_fail with "H↦"); try done. iIntros "H↦".
-      iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "H↦") as "Hown".
-      iModIntro. wp_case. by iApply ("IH" with "Hown").
-  Qed.
-
-  Lemma upgrade_spec (γ : gname) (l : loc) (P : iProp Σ) :
-    is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
-    {{{ P }}} upgrade [ #l]
-    {{{ (b : bool) q, RET #b; P ∗ if b then arc_tok γ q ∗ P1 q else True }}}.
-  Proof using HP1.
-    iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
-    iAssert (□ (P ={⊤,∅}=∗ ∃ s : Z, l ↦ #s ∗
-              (⌜s ≠ 0⌝ -∗ l ↦ #(s + 1) ={∅,⊤}=∗ ∃ q, P ∗ arc_tok γ q ∗ ▷ P1 q) ∧
-              (l ↦ #s ={∅,⊤}=∗ 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).
-      destruct st' as [[[[??]?]| |]|]; try done; iExists _.
-      - iDestruct "H" as (q) "(>Heq & [HP1 HP1'] & >$ & ?)". iDestruct "Heq" as %Heq.
-        iIntros "!>"; iSplit; iMod ("Hclose2" with "Hown") as "HP".
-        + iIntros "_ Hl". iExists (q/2)%Qp. iMod (own_update with "H●") as "[H● $]".
-          { apply auth_update_alloc. rewrite -[(_,0%nat)]right_id.
-            apply op_local_update_discrete=>Hv. constructor; last done.
-            split; last by rewrite /= left_id; apply Hv. split=>[|//].
-            apply frac_valid'. rewrite -Heq comm_L -{2}(Qp_div_2 q).
-            apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
-            apply Qcplus_le_mono_r, Qp_ge_0. }
-          iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
-          rewrite /= [xH ⋅ _]comm_L frac_op' [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
-                  Qp_div_2 left_id_L. auto with iFrame.
-        + iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
-          iExists q. auto with iFrame.
-      - iDestruct "H" as "[>$ ?]". iIntros "!>"; iSplit; first by auto with congruence.
-        iIntros "Hl". iMod ("Hclose2" with "Hown") as "$". iApply "Hclose1".
-        iExists _. auto with iFrame.
-      - iDestruct "H" as "[>$ ?]". iIntros "!>"; iSplit; first by auto with congruence.
-        iIntros "Hl". iMod ("Hclose2" with "Hown") as "$". iApply "Hclose1".
-        iExists _. auto with iFrame. }
-    iMod ("Hproto" with "HP") as (s) "[Hs [_ Hclose]]". wp_read.
-    iMod ("Hclose" with "Hs") as "HP". iModIntro. wp_let. wp_op; wp_if; case_bool_decide.
-    - iApply wp_value. iApply ("HΦ" $! _ 1%Qp). auto.
-    - wp_op. wp_bind (CAS _ _ _). iMod ("Hproto" with "HP") as (s') "[H↦ Hclose]".
-      destruct (decide (s = s')) as [<-|].
-      + wp_apply (wp_cas_int_suc with "H↦"). iIntros "H↦".
-        iDestruct "Hclose" as "[Hclose _]".
-        iMod ("Hclose" with "[//] H↦") as (q) "(?&?&?)". iModIntro.
-        wp_case. iApply "HΦ". iFrame.
-      + wp_apply (wp_cas_int_fail with "H↦"); try done. iIntros "H↦".
-        iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "H↦") as "Hown".
-        iModIntro. wp_case. by iApply ("IH" with "Hown").
-  Qed.
-
-  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 ∗ (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, (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 _..].
-      - by iDestruct "H" as (?) "(_ & _ & _ & _ & >%)".
-      - iDestruct "H" as (q) "(>Heq & HP1 & ? & >$)". iIntros "!>"; iSplit; iIntros "Hl1".
-        + iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
-          iExists _. iMod (own_update_2 with "H● Hown") as "$".
-          { apply auth_update_dealloc, prod_local_update_2,
-                  (cancel_local_update_unit 1%nat), _. }
-          iExists _. iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
-        + iFrame. iApply "Hclose1". iExists _. auto with iFrame.
-      - iDestruct "H" as "[? >$]". iIntros "!>"; iSplit; iIntros "Hl1".
-        + iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
-          iExists _. iMod (own_update_2 with "H● Hown") as "$".
-          { apply auth_update_dealloc, prod_local_update_2,
-                  (cancel_local_update_unit 1%nat), _. }
-          iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
-        + iFrame. iApply "Hclose1". iExists _. auto with iFrame.
-      - iDestruct "H" as "(>? & >$ & HP2)". iIntros "!>"; iSplit; iIntros "Hl1".
-        + iMod (own_update_2 with "H● Hown") as "H●".
-          { apply auth_update_dealloc, prod_local_update_2,
-                  (cancel_local_update_unit 1%nat), _. }
-          destruct weak as [|weak].
-          * iMod ("Hclose1" with "[H●]") as "_"; last by auto with iFrame.
-            iExists _. iFrame.
-          * iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
-            iExists _. iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
-        + iFrame. iApply "Hclose1". iExists _. auto with iFrame. }
-    iMod ("Hproto" with "Hown") as (w) "[Hw [_ Hclose]]". wp_read.
-    iMod ("Hclose" with "Hw") as "Hown". iModIntro. wp_let. wp_op. wp_op.
-    wp_bind (CAS _ _ _).
-    iMod ("Hproto" with "Hown") as (w') "[Hw Hclose]". destruct (decide (w = w')) as [<-|?].
-    - wp_apply (wp_cas_int_suc with "Hw"). iIntros "Hw".
-      iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hw") as "HP2". iModIntro.
-      wp_case. wp_op; case_bool_decide; subst; iApply "HΦ"=>//.
-      by iDestruct "HP2" as "[%|$]".
-    - wp_apply (wp_cas_int_fail with "Hw"); try done. iIntros "Hw".
-      iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hw") as "Hown".
-      iModIntro. wp_case. by iApply ("IH" with "Hown").
-  Qed.
-
-  Lemma close_last_strong γ l :
-    is_arc P1 P2 N γ l -∗ own γ (◯ (Some (Cinr (Excl ())), 0%nat)) -∗ P2
-    ={⊤}=∗ weak_tok γ.
-  Proof.
-    iIntros "INV H◯ HP2". iInv N as ([st ?]) "[>H● H]" "Hclose".
-    iDestruct (own_valid_2 with "H● H◯")
-      as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
-    simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
-        try done; try apply _. setoid_subst.
-    iMod (own_update_2 with "H● H◯") as "[H● $]".
-    { apply auth_update, prod_local_update', (op_local_update _ _ 1%nat)=>//.
-      apply delete_option_local_update, _. }
-    iApply "Hclose". iExists _. by iFrame.
-  Qed.
-
-  Lemma drop_arc_spec (γ : gname) (q: Qp) (l : loc) :
-    is_arc P1 P2 N γ l -∗
-    {{{ arc_tok γ q ∗ P1 q }}} drop_arc  [ #l]
-    {{{ (b : bool), RET #b ; if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else True }}}.
-  Proof using HP1.
-    iIntros "#INV !# * [Hown HP1] HΦ". iLöb as "IH".
-    wp_rec. wp_bind (!ˢᶜ_)%E. iInv N as (st) "[>H● H]" "Hclose".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(?& s &?&?&[-> _]).
-    iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
-    iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_". { iExists _. auto with iFrame. }
-    iModIntro. wp_let. wp_op. wp_bind (CAS _ _ _). iInv N as (st) "[>H● H]" "Hclose".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s' & wl & w &[-> Hqq']).
-    iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
-    destruct (decide (s = s')) as [<-|?].
-    - wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs".
-      destruct decide as [->|?].
-      + destruct Hqq' as [<- ->].
-        iMod (own_update_2 with "H● Hown") as "[H● H◯]".
-        { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
-          etrans; first apply cancel_local_update_unit, _.
-          by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
-        iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
-        iModIntro. wp_case. iApply wp_fupd. wp_op.
-        iApply ("HΦ"). rewrite -{2}Hq''. iFrame. by iApply close_last_strong.
-      + destruct Hqq' as [? ->].
-        rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
-                -Pos.add_1_l -2!pair_op -Cinl_op Some_op.
-        iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
-        { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
-        iMod ("Hclose" with "[- HΦ]") as "_".
-        { iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; last by destruct s.
-          iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
-        iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ".
-    - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
-      iSpecialize ("IH" with "Hown HP1 HΦ").
-      iMod ("Hclose" with "[- IH]") as "_"; first by iExists _; auto with iFrame.
-      iModIntro. by wp_case.
-  Qed.
-
-  Lemma try_unwrap_spec (γ : gname) (q: Qp) (l : loc) :
-    is_arc P1 P2 N γ l -∗
-    {{{ arc_tok γ q ∗ P1 q }}} try_unwrap [ #l]
-    {{{ (b : bool), RET #b ;
-        if b then P1 1 ∗ (P2 ={⊤}=∗ weak_tok γ) else arc_tok γ q ∗ P1 q }}}.
-  Proof using HP1.
-    iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. iInv N as (st) "[>H● H]" "Hclose".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s & wl & w &[-> Hqq']).
-    iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
-    destruct (decide (s = xH)) as [->|?].
-    - wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs".
-      destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
-      { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
-        etrans; first apply cancel_local_update_unit, _.
-        by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
-      iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
-      iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. by iApply close_last_strong.
-    - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
-      iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_"; first by iExists _; auto with iFrame.
-      iApply ("HΦ" $! false). by iFrame.
-  Qed.
-
-  Lemma is_unique_spec (γ : gname) (q: Qp) (l : loc) :
-    is_arc P1 P2 N γ l -∗
-    {{{ arc_tok γ q ∗ P1 q }}} is_unique [ #l]
-    {{{ (b : bool), RET #b ;
-        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.
-    iInv N as (st) "[>H● H]" "Hclose".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(? & ? & wl & w &[-> _]).
-    iDestruct "H" as (?) "(>Hq'' & HP1' & >Hs & >Hw)".
-    destruct wl; last (destruct w; last first).
-    - iDestruct "Hw" as "[Hw %]". subst.
-      iApply (wp_cas_int_fail with "Hw")=>//. iNext. iIntros "Hw".
-      iMod ("Hclose" with "[-HΦ Hown HP1]") as "_"; first by iExists _; eauto with iFrame.
-      iModIntro. wp_case. iApply "HΦ". iFrame.
-    - iApply (wp_cas_int_fail with "Hw"); [lia|]. iNext. iIntros "Hw".
-      iMod ("Hclose" with "[-HΦ Hown HP1]") as "_"; first by iExists _; eauto with iFrame.
-      iModIntro. wp_case. iApply "HΦ". iFrame.
-    - iApply (wp_cas_int_suc with "Hw")=>//. iNext. iIntros "Hw".
-      iMod (own_update_2 with "H● Hown") as "[H● H◯]".
-      { by apply auth_update, prod_local_update_1, option_local_update,
-                 csum_local_update_l, prod_local_update_2,
-                 (alloc_option_local_update (Excl ())). }
-      iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame.
-      iModIntro. wp_case. wp_bind (!ˢᶜ_)%E. iInv N as ([st ?]) "[>H● H]" "Hclose".
-      iDestruct (own_valid_2 with "H● H◯") as
-        %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
-      simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
-      + apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
-        destruct Hincl as (?&[[??]?]&[=<-]&->&[[_ Hlt]%prod_included _]%prod_included).
-        simpl in Hlt. apply pos_included in Hlt.
-        iDestruct "H" as (?) "(? & ? & ? & ?)". wp_read.
-        iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
-        iModIntro. wp_let. wp_op; case_bool_decide; [lia|]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
-        iInv N as ([st w]) "[>H● H]" "Hclose".
-        iDestruct (own_valid_2 with "H● H◯") as
-           %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
-        simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first.
-        assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
-        { destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
-          apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
-          destruct Hincl as (?&[[??]?]&[=<-]&->&[_ Hincl%option_included]%prod_included).
-          simpl in Hincl. destruct Hincl as [[=]|(?&?&[=<-]&->&[?|[]%exclusive_included])];
-            [|by apply _|by apply Hval]. setoid_subst. eauto. }
-        iDestruct "H" as (?) "(? & ? & ? & >? & >%)". subst. wp_write.
-        iMod (own_update_2 with "H● H◯") as "[H● H◯]".
-        { apply auth_update, prod_local_update_1, option_local_update,
-          csum_local_update_l, prod_local_update_2, delete_option_local_update, _. }
-        iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
-        iModIntro. wp_seq. iApply "HΦ". iFrame.
-      + setoid_subst. iDestruct "H" as (?) "(Hq & ? & ? & >? & >%)". subst. wp_read.
-        iMod (own_update_2 with "H● H◯") as "H●".
-        { apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
-          apply cancel_local_update_unit, _. }
-        iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame.
-        iModIntro. wp_seq. wp_op. wp_let. wp_op. wp_write. iApply "HΦ".
-        iDestruct "Hq" as %<-. iFrame.
-  Qed.
-
-  Lemma try_unwrap_full_spec (γ : gname) (q: Qp) (l : loc) :
-    is_arc P1 P2 N γ l -∗
-    {{{ arc_tok γ q ∗ P1 q }}} try_unwrap_full [ #l]
-    {{{ (x : fin 3), RET #x ;
-        match x : nat with
-        (* No other reference : we get everything. *)
-        | 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 γ)
-        (* There are other strong : we get back what we gave at the first place. *)
-        | _ (* 2 *) => arc_tok γ q ∗ P1 q
-        end }}}.
-  Proof using HP1.
-    iIntros "#INV !# * [Hown HP1] HΦ". wp_rec. wp_bind (CAS _ _ _).
-    iInv N as (st) "[>H● H]" "Hclose".
-    iDestruct (arc_tok_auth_val with "H● Hown") as %(q' & s & wl & w &[-> Hqq']).
-    iDestruct "H" as (q'') "(>Hq'' & HP1' & Hs & Hw)". iDestruct "Hq''" as %Hq''.
-    destruct (decide (s = xH)) as [->|?].
-    - wp_apply (wp_cas_int_suc with "Hs")=>//. iIntros "Hs".
-      destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
-      { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
-        etrans; first apply cancel_local_update_unit, _.
-        by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
-      iCombine "HP1" "HP1'" as "HP1". rewrite Hq''. clear Hq'' q''.
-      iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
-      clear w. iModIntro. wp_case. wp_op. wp_bind (!ˢᶜ_)%E.
-      iInv N as ([st w']) "[>H● H]" "Hclose".
-      iDestruct (own_valid_2 with "H● H◯")
-        as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
-      simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
-        [|by apply _|done]. setoid_subst. iDestruct "H" as "[Hl Hl1]".
-      wp_read. destruct w'.
-      + iMod (own_update_2 with "H● H◯") as "H●".
-        { apply auth_update_dealloc, prod_local_update_1,
-                delete_option_local_update, _. }
-        iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame. iModIntro.
-        wp_op. wp_if. wp_write. iApply ("HΦ" $! 0%fin). iFrame.
-      + iMod ("Hclose" with "[H● Hl Hl1]") as "_"; first by iExists _; do 2 iFrame.
-        iModIntro. wp_op; case_bool_decide; [lia|]. wp_if. iApply ("HΦ" $! 1%fin). iFrame.
-        by iApply close_last_strong.
-    - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
-      iMod ("Hclose" with "[H● Hs Hw HP1']") as "_"; first by iExists _; auto with iFrame.
-      iModIntro. wp_case. iApply ("HΦ" $! 2%fin). iFrame.
-  Qed.
-End arc.
-
-Typeclasses Opaque is_arc arc_tok weak_tok.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
new file mode 100644
index 0000000000000000000000000000000000000000..4bac769097151f753dddbf74c9c84638fac99ab6
--- /dev/null
+++ b/theories/lang/lifting.v
@@ -0,0 +1,377 @@
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import ectx_lifting.
+From lrust.lang Require Export lang heap.
+From lrust.lang Require Import tactics.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+Import uPred.
+
+Class lrustG Σ := LRustG {
+  lrustG_invG : invG Σ;
+  lrustG_gen_heapG :> heapG Σ
+}.
+
+Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
+  iris_invG := lrustG_invG;
+  state_interp σ κs _ := heap_ctx σ;
+  fork_post _ := True%I;
+}.
+Global Opaque iris_invG.
+
+Ltac inv_lit :=
+  repeat match goal with
+  | H : lit_eq _ ?x ?y |- _ => inversion H; clear H; simplify_map_eq/=
+  | H : lit_neq ?x ?y |- _ => inversion H; clear H; simplify_map_eq/=
+  end.
+
+Ltac inv_bin_op_eval :=
+  repeat match goal with
+  | H : bin_op_eval _ ?c _ _ _ |- _ => is_constructor c; inversion H; clear H; simplify_eq/=
+  end.
+
+Local Hint Extern 0 (atomic _) => solve_atomic.
+Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
+
+Local Hint Constructors head_step bin_op_eval lit_neq lit_eq.
+Local Hint Resolve alloc_fresh.
+Local Hint Resolve to_of_val.
+
+Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) :=
+  as_rec : e = Rec f xl erec.
+Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
+Instance AsRec_rec_locked_val v f xl e :
+  AsRec (of_val v) f xl e → AsRec (of_val (locked v)) f xl e.
+Proof. by unlock. Qed.
+
+Class DoSubst (x : binder) (es : expr) (e er : expr) :=
+  do_subst : subst' x es e = er.
+Hint Extern 0 (DoSubst _ _ _ _) =>
+  rewrite /DoSubst; simpl_subst; reflexivity : typeclass_instances.
+
+Class DoSubstL (xl : list binder) (esl : list expr) (e er : expr) :=
+  do_subst_l : subst_l xl esl e = Some er.
+Instance do_subst_l_nil e : DoSubstL [] [] e e.
+Proof. done. Qed.
+Instance do_subst_l_cons x xl es esl e er er' :
+  DoSubstL xl esl e er' → DoSubst x es er' er →
+  DoSubstL (x :: xl) (es :: esl) e er.
+Proof. rewrite /DoSubstL /DoSubst /= => -> <- //. Qed.
+Instance do_subst_vec xl (vsl : vec val (length xl)) e :
+  DoSubstL xl (of_val <$> vec_to_list vsl) e (subst_v xl vsl e).
+Proof. by rewrite /DoSubstL subst_v_eq. Qed.
+
+Section lifting.
+Context `{!lrustG Σ}.
+Implicit Types P Q : iProp Σ.
+Implicit Types e : expr.
+Implicit Types ef : option expr.
+
+(** Base axioms for core primitives of the language: Stateless reductions *)
+Lemma wp_fork E e :
+  {{{ ▷ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitPoison; True }}}.
+Proof.
+  iIntros (?) "?HΦ". iApply wp_lift_atomic_head_step; [done|].
+  iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iFrame.
+  iModIntro. by iApply "HΦ".
+Qed.
+
+(** Pure reductions *)
+Local Ltac solve_exec_safe :=
+  intros; destruct_and?; subst; do 3 eexists; econstructor; simpl; eauto with lia.
+Local Ltac solve_exec_puredet :=
+  simpl; intros; destruct_and?; inv_head_step; inv_bin_op_eval; inv_lit; done.
+Local Ltac solve_pure_exec :=
+  intros ?; apply nsteps_once, pure_head_step_pure_step;
+    constructor; [solve_exec_safe | solve_exec_puredet].
+
+Global Instance pure_rec e f xl erec erec' el :
+  AsRec e f xl erec →
+  TCForall AsVal el →
+  Closed (f :b: xl +b+ []) erec →
+  DoSubstL (f :: xl) (e :: el) erec erec' →
+  PureExec True 1 (App e el) erec'.
+Proof.
+  rewrite /AsRec /DoSubstL=> -> /TCForall_Forall Hel ??. solve_pure_exec.
+  eapply Forall_impl; [exact Hel|]. intros e' [v <-]. rewrite to_of_val; eauto.
+Qed.
+
+Global Instance pure_le n1 n2 :
+  PureExec True 1 (BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)))
+                  (Lit (bool_decide (n1 ≤ n2))).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_eq_int n1 n2 :
+  PureExec True 1 (BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2))) (Lit (bool_decide (n1 = n2))).
+Proof. case_bool_decide; solve_pure_exec. Qed.
+
+Global Instance pure_eq_loc_0_r l :
+  PureExec True 1 (BinOp EqOp (Lit (LitLoc l)) (Lit (LitInt 0))) (Lit false).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_eq_loc_0_l l :
+  PureExec True 1 (BinOp EqOp (Lit (LitInt 0)) (Lit (LitLoc l))) (Lit false).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_plus z1 z2 :
+  PureExec True 1 (BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2)) (Lit $ LitInt $ z1 + z2).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_minus z1 z2 :
+  PureExec True 1 (BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2)) (Lit $ LitInt $ z1 - z2).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_offset l z  :
+  PureExec True 1 (BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z)) (Lit $ LitLoc $ l +ₗ z).
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_case i e el :
+  PureExec (0 ≤ i ∧ el !! (Z.to_nat i) = Some e) 1 (Case (Lit $ LitInt i) el) e | 10.
+Proof. solve_pure_exec. Qed.
+
+Global Instance pure_if b e1 e2 :
+  PureExec True 1 (If (Lit (lit_of_bool b)) e1 e2) (if b then e1 else e2) | 1.
+Proof. destruct b; solve_pure_exec. Qed.
+
+(** Heap *)
+Lemma wp_alloc E (n : Z) :
+  0 < n →
+  {{{ True }}} Alloc (Lit $ LitInt n) @ E
+  {{{ l (sz: nat), RET LitV $ LitLoc l; ⌜n = sz⌝ ∗ †l…sz ∗ l ↦∗ repeat (LitV LitPoison) sz }}}.
+Proof.
+  iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ !>"; iSplit; first by auto.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
+  iModIntro; iSplit=> //. iFrame.
+  iApply ("HΦ" $! _ (Z.to_nat n)). iFrame. iPureIntro. rewrite Z2Nat.id; lia.
+Qed.
+
+Lemma wp_free E (n:Z) l vl :
+  n = length vl →
+  {{{ ▷ l ↦∗ vl ∗ ▷ †l…(length vl) }}}
+    Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
+  {{{ RET LitV LitPoison; True }}}.
+Proof.
+  iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ".
+  iMod (heap_free _ _ _ n with "Hσ Hmt Hf") as "(% & % & Hσ)"=>//.
+  iModIntro; iSplit; first by auto.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iFrame. iApply "HΦ"; auto.
+Qed.
+
+Lemma wp_read_sc E l q v :
+  {{{ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
+  {{{ RET v; l ↦{q} v }}}.
+Proof.
+  iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_read_na E l q v :
+  {{{ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
+  {{{ RET v; l ↦{q} v }}}.
+Proof.
+  iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 ???) "Hσ".
+  iMod (heap_read_na with "Hσ Hv") as (n) "(% & Hσ & Hσclose)".
+  iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
+  iModIntro. iFrame "Hσ". iSplit; last done.
+  clear dependent σ1 n.
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
+  iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
+Qed.
+
+Lemma wp_write_sc E l e v v' :
+  IntoVal e v →
+  {{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
+  {{{ RET LitV LitPoison; l ↦ v }}}.
+Proof.
+  iIntros (<- Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+  iMod (heap_write _ _ _  v with "Hσ Hv") as "[Hσ Hv]".
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_write_na E l e v v' :
+  IntoVal e v →
+  {{{ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
+  {{{ RET LitV LitPoison; l ↦ v }}}.
+Proof.
+  iIntros (<- Φ) ">Hv HΦ".
+  iApply wp_lift_head_step; auto. iIntros (σ1 ???) "Hσ".
+  iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
+  iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
+  iModIntro. iFrame "Hσ". iSplit; last done.
+  clear dependent σ1. iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
+  iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
+Qed.
+
+Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
+  IntoVal e2 (LitV lit2) → z1 ≠ zl →
+  {{{ ▷ l ↦{q} LitV (LitInt zl) }}}
+    CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
+  {{{ RET LitV $ LitInt 0; l ↦{q} LitV (LitInt zl) }}}.
+Proof.
+  iIntros (<- ? Φ) ">Hv HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; inv_lit.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_cas_suc E l lit1 e2 lit2 :
+  IntoVal e2 (LitV lit2) → lit1 ≠ LitPoison →
+  {{{ ▷ l ↦ LitV lit1 }}}
+    CAS (Lit $ LitLoc l) (Lit lit1) e2 @ E
+  {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
+Proof.
+  iIntros (<- ? Φ) ">Hv HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+  iModIntro; iSplit; first (destruct lit1; by eauto).
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; [inv_lit|].
+  iMod (heap_write with "Hσ Hv") as "[$ Hv]".
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
+
+Lemma wp_cas_int_suc E l z1 e2 lit2 :
+  IntoVal e2 (LitV lit2) →
+  {{{ ▷ l ↦ LitV (LitInt z1) }}}
+    CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
+  {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
+Proof. intros ?. by apply wp_cas_suc. Qed.
+
+Lemma wp_cas_loc_suc E l l1 e2 lit2 :
+  IntoVal e2 (LitV lit2) →
+  {{{ ▷ l ↦ LitV (LitLoc l1) }}}
+    CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+  {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
+Proof. intros ?. by apply wp_cas_suc. Qed.
+
+Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
+  IntoVal e2 (LitV lit2) → l1 ≠ l' →
+  {{{ ▷ l ↦{q} LitV (LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
+    CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+  {{{ RET LitV (LitInt 0);
+      l ↦{q} LitV (LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
+Proof.
+  iIntros (<- ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
+  iDestruct (heap_read with "Hσ Hl'") as %[nl' ?].
+  iDestruct (heap_read with "Hσ Hl1") as %[nl1 ?].
+  iModIntro; iSplit; first by eauto.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; inv_lit.
+  iModIntro; iSplit=> //. iFrame. iApply "HΦ"; iFrame.
+Qed.
+
+Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
+  IntoVal e2 (LitV $ LitLoc l2) →
+  {{{ ▷ l ↦ LitV (LitLoc ll) }}}
+    CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+  {{{ b, RET LitV (lit_of_bool b);
+      if b is true then l ↦ LitV (LitLoc l2)
+      else ⌜l1 ≠ ll⌝ ∗ l ↦ LitV (LitLoc ll) }}}.
+Proof.
+  iIntros (<- Φ) ">Hv HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 ???) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+  iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; last lia.
+  - inv_lit. iModIntro; iSplit; [done|]; iFrame "Hσ".
+    iApply "HΦ"; simpl; auto.
+  - iMod (heap_write with "Hσ Hv") as "[$ Hv]".
+    iModIntro; iSplit; [done|]. iApply "HΦ"; iFrame.
+Qed.
+
+Lemma wp_eq_loc E (l1 : loc) (l2: loc) q1 q2 v1 v2 P Φ :
+  (P -∗ ▷ l1 ↦{q1} v1) →
+  (P -∗ ▷ l2 ↦{q2} v2) →
+  (P -∗ ▷ Φ (LitV (bool_decide (l1 = l2)))) →
+  P -∗ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
+Proof.
+  iIntros (Hl1 Hl2 Hpost) "HP".
+  destruct (bool_decide_reflect (l1 = l2)) as [->|].
+  - iApply wp_lift_pure_det_head_step_no_fork';
+      [done|solve_exec_safe|solve_exec_puredet|].
+    iApply wp_value. by iApply Hpost.
+  - iApply wp_lift_atomic_head_step_no_fork; subst=>//.
+    iIntros (σ1 ???) "Hσ1". iModIntro. inv_head_step.
+    iSplitR.
+    { iPureIntro. repeat eexists. econstructor. eapply BinOpEqFalse. by auto. }
+    (* We need to do a little gymnastics here to apply Hne now and strip away a
+       ▷ but also have the ↦s. *)
+    iAssert ((▷ ∃ q v, l1 ↦{q} v) ∧ (▷ ∃ q v, l2 ↦{q} v) ∧ ▷ Φ (LitV false))%I with "[HP]" as "HP".
+    { iSplit; last iSplit.
+      + iExists _, _. by iApply Hl1.
+      + iExists _, _. by iApply Hl2.
+      + by iApply Hpost. }
+    clear Hl1 Hl2. iNext. iIntros (e2 σ2 efs Hs) "!>".
+    inv_head_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
+    + iExFalso. iDestruct "HP" as "[Hl1 _]".
+      iDestruct "Hl1" as (??) "Hl1".
+      iDestruct (heap_read σ2 with "Hσ1 Hl1") as %[??]; simplify_eq.
+    + iExFalso. iDestruct "HP" as "[_ [Hl2 _]]".
+      iDestruct "Hl2" as (??) "Hl2".
+      iDestruct (heap_read σ2 with "Hσ1 Hl2") as %[??]; simplify_eq.
+    + iDestruct "HP" as "[_ [_ $]]". done.
+Qed.
+
+(** Proof rules for working on the n-ary argument list. *)
+Lemma wp_app_ind E f (el : list expr) (Ql : vec (val → iProp Σ) (length el)) vs Φ :
+  AsVal f →
+  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
+    (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
+                    WP App f (of_val <$> vs ++ vl) @ E {{ Φ }}) -∗
+    WP App f ((of_val <$> vs) ++ el) @ E {{ Φ }}.
+Proof.
+  intros [vf <-]. revert vs Ql.
+  induction el as [|e el IH]=>/= vs Ql; inv_vec Ql; simpl.
+  - iIntros "_ H". iSpecialize ("H" $! [#]). rewrite !app_nil_r /=. by iApply "H".
+  - iIntros (Q Ql) "[He Hl] HΦ".
+    change (App (of_val vf) ((of_val <$> vs) ++ e :: el)) with (fill_item (AppRCtx vf vs el) e).
+    iApply wp_bind. iApply (wp_wand with "He"). iIntros (v) "HQ /=".
+    rewrite cons_middle (assoc app) -(fmap_app _ _ [v]).
+    iApply (IH _ _ with "Hl"). iIntros "* Hvl". rewrite -assoc.
+    iApply ("HΦ" $! (v:::vl)). iFrame.
+Qed.
+
+Lemma wp_app_vec E f el (Ql : vec (val → iProp Σ) (length el)) Φ :
+  AsVal f →
+  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
+    (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
+                    WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
+    WP App f el @ E {{ Φ }}.
+Proof. iIntros (Hf). by iApply (wp_app_ind _ _ _ _ []). Qed.
+
+Lemma wp_app (Ql : list (val → iProp Σ)) E f el Φ :
+  length Ql = length el → AsVal f →
+  ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
+    (∀ vl : list val, ⌜length vl = length el⌝ -∗
+            ([∗ list] k ↦ vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
+             WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
+    WP App f el @ E {{ Φ }}.
+Proof.
+  iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_of_list Ql).
+  generalize (list_to_vec Ql). rewrite Hlen. clear Hlen Ql=>Ql.
+  iApply (wp_app_vec with "Hel"). iIntros (vl) "Hvl".
+  iApply ("HΦ" with "[%] Hvl"). by rewrite vec_to_list_length.
+Qed.
+End lifting.
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index 5883b09e94c52c747cb0316ac1e11e4806efc7ee..aa3f254f47c1ba7a525f4deb551f92244b488f55 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -19,7 +19,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
   (at level 80, n, i at next level,
    format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
 
-Lemma wp_memcpy `{noprolG Σ} tid E l1 l2 vl1 vl2 q (n : Z):
+Lemma wp_memcpy `{!noprolG Σ} tid E l1 l2 vl1 vl2 q (n : Z):
   ↑histN ⊆ E → Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
     #l1 <-{n} !#l2 in tid @ E
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
new file mode 100644
index 0000000000000000000000000000000000000000..a1b3db3e1a85ef863601d8ab98f9845d350230d5
--- /dev/null
+++ b/theories/lang/proofmode.v
@@ -0,0 +1,259 @@
+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import coq_tactics reduction.
+From iris.proofmode Require Export tactics.
+From lrust.lang Require Export tactics lifting.
+From iris.program_logic Require Import lifting.
+Set Default Proof Using "Type".
+Import uPred.
+
+Lemma tac_wp_value `{!lrustG Σ} Δ E Φ e v :
+  IntoVal e v →
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
+Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
+
+Ltac wp_value_head := eapply tac_wp_value; [iSolveTC|reduction.pm_prettify].
+
+Lemma tac_wp_pure `{!lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
+  PureExec φ n e1 e2 →
+  φ →
+  MaybeIntoLaterNEnvs n Δ Δ' →
+  envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite -wp_bind HΔ' -wp_pure_step_later //. by rewrite -wp_bind_inv.
+Qed.
+
+Tactic Notation "wp_pure" open_constr(efoc) :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
+    unify e' efoc;
+    eapply (tac_wp_pure K);
+    [simpl; iSolveTC                (* PureExec *)
+    |try done                       (* The pure condition for PureExec *)
+    |iSolveTC                       (* IntoLaters *)
+    |simpl_subst; try wp_value_head (* new goal *)])
+   || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
+  | _ => fail "wp_pure: not a 'wp'"
+  end.
+
+Lemma tac_wp_eq_loc `{!lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i1 Δ' = Some (false, l1 ↦{q1} v1)%I →
+  envs_lookup i2 Δ' = Some (false, l2 ↦{q2} v2)%I →
+  envs_entails Δ' (WP fill K (Lit (bool_decide (l1 = l2))) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2))) @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq=> ? /envs_lookup_sound /=. rewrite sep_elim_l=> ?.
+  move /envs_lookup_sound; rewrite sep_elim_l=> ? HΔ. rewrite -wp_bind.
+  rewrite into_laterN_env_sound /=. eapply wp_eq_loc; eauto using later_mono.
+Qed.
+
+Tactic Notation "wp_eq_loc" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+     reshape_expr e ltac:(fun K e' => eapply (tac_wp_eq_loc K));
+       [iSolveTC|iAssumptionCore|iAssumptionCore|simpl; try wp_value_head]
+  | _ => fail "wp_pure: not a 'wp'"
+  end.
+
+Tactic Notation "wp_rec" := wp_pure (App _ _).
+Tactic Notation "wp_lam" := wp_rec.
+Tactic Notation "wp_let" := wp_lam.
+Tactic Notation "wp_seq" := wp_let.
+Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
+Tactic Notation "wp_if" := wp_pure (If _ _ _).
+Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
+
+Lemma tac_wp_bind `{!lrustG Σ} K Δ E Φ e :
+  envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
+  envs_entails Δ (WP fill K e @ E {{ Φ }}).
+Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed.
+
+Ltac wp_bind_core K :=
+  lazymatch eval hnf in K with
+  | [] => idtac
+  | _ => apply (tac_wp_bind K); simpl
+  end.
+
+Tactic Notation "wp_bind" open_constr(efoc) :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
+    match e' with
+    | efoc => unify e' efoc; wp_bind_core K
+    end) || fail "wp_bind: cannot find" efoc "in" e
+  | _ => fail "wp_bind: not a 'wp'"
+  end.
+
+Section heap.
+Context `{!lrustG Σ}.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val → iProp Σ.
+Implicit Types Δ : envs (uPredI (iResUR Σ)).
+
+Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ :
+  0 < n →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  (∀ l (sz: nat), n = sz → ∃ Δ'',
+    envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ repeat (LitV LitPoison) sz)) j2 (†l…sz)) Δ'
+      = Some Δ'' ∧
+    envs_entails Δ'' (WP fill K (Lit $ LitLoc l) @ E {{ Φ }})) →
+  envs_entails Δ (WP fill K (Alloc (Lit $ LitInt n)) @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq=> ?? HΔ. rewrite -wp_bind.
+  eapply wand_apply; first exact:wp_alloc.
+  rewrite -persistent_and_sep. apply and_intro; first by auto.
+  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
+  apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc.
+  rewrite sep_and. apply pure_elim_l=> Hn. apply wand_elim_r'.
+  destruct (HΔ l sz) as (Δ''&?&HΔ'); first done.
+  rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
+Qed.
+
+Lemma tac_wp_free K Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
+  n = length vl →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
+  envs_delete false i1 false Δ' = Δ'' →
+  envs_lookup i2 Δ'' = Some (false, †l…n')%I →
+  envs_delete false i2 false Δ'' = Δ''' →
+  n' = length vl →
+  envs_entails Δ''' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Free (Lit $ LitInt n) (Lit $ LitLoc l)) @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind.
+  eapply wand_apply; first exact:wp_free; simpl.
+  rewrite into_laterN_env_sound -!later_sep; apply later_mono.
+  do 2 (rewrite envs_lookup_sound //). by rewrite HΔ True_emp emp_wand -assoc.
+Qed.
+
+Lemma tac_wp_read K Δ Δ' E i l q v o Φ :
+  o = Na1Ord ∨ o = ScOrd →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
+  envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Read o (Lit $ LitLoc l)) @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq; intros [->| ->] ???.
+  - rewrite -wp_bind. eapply wand_apply; first exact:wp_read_na.
+    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
+    by apply later_mono, sep_mono_r, wand_mono.
+  - rewrite -wp_bind. eapply wand_apply; first exact:wp_read_sc.
+    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
+    by apply later_mono, sep_mono_r, wand_mono.
+Qed.
+
+Lemma tac_wp_write K Δ Δ' Δ'' E i l v e v' o Φ :
+  IntoVal e v' →
+  o = Na1Ord ∨ o = ScOrd →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ v)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
+  envs_entails Δ'' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Write o (Lit $ LitLoc l) e) @ E {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq; intros ? [->| ->] ????.
+  - rewrite -wp_bind. eapply wand_apply; first by apply wp_write_na.
+    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
+    rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+  - rewrite -wp_bind. eapply wand_apply; first by apply wp_write_sc.
+    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
+    rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+Qed.
+End heap.
+
+Tactic Notation "wp_apply" open_constr(lem) :=
+  iPoseProofCore lem as false true (fun H =>
+    lazymatch goal with
+    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+      reshape_expr e ltac:(fun K e' =>
+        wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
+      lazymatch iTypeOf H with
+      | Some (_,?P) => fail "wp_apply: cannot apply" P
+      end
+    | _ => fail "wp_apply: not a 'wp'"
+    end).
+
+Tactic Notation "wp_alloc" ident(l) "as" constr(H) constr(Hf) :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc K _ _ _ H Hf))
+      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+    [try fast_done
+    |iSolveTC
+    |let sz := fresh "sz" in let Hsz := fresh "Hsz" in
+     first [intros l sz Hsz | fail 1 "wp_alloc:" l "not fresh"];
+     (* If Hsz is "constant Z = nat", change that to an equation on nat and
+        potentially substitute away the sz. *)
+     try (match goal with Hsz : ?x = _ |- _ => rewrite <-(Z2Nat.id x) in Hsz; last done end;
+          apply Nat2Z.inj in Hsz;
+          try (cbv [Z.to_nat Pos.to_nat] in Hsz;
+               simpl in Hsz;
+               (* Substitute only if we have a literal nat. *)
+               match goal with Hsz : S _ = _ |- _ => subst sz end));
+      eexists; split;
+        [pm_reflexivity || fail "wp_alloc:" H "or" Hf "not fresh"
+        |simpl; try wp_value_head]]
+  | _ => fail "wp_alloc: not a 'wp'"
+  end.
+
+Tactic Notation "wp_alloc" ident(l) :=
+  let H := iFresh in let Hf := iFresh in wp_alloc l as H Hf.
+
+Tactic Notation "wp_free" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_free K))
+      |fail 1 "wp_free: cannot find 'Free' in" e];
+    [try fast_done
+    |iSolveTC
+    |let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
+     iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
+    |pm_reflexivity
+    |let l := match goal with |- _ = Some (_, († ?l … _)%I) => l end in
+     iAssumptionCore || fail "wp_free: cannot find †" l "… ?"
+    |pm_reflexivity
+    |try fast_done
+    |simpl; try first [wp_pure (Seq (Lit LitPoison) _)|wp_value_head]]
+  | _ => fail "wp_free: not a 'wp'"
+  end.
+
+Tactic Notation "wp_read" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_read K))
+      |fail 1 "wp_read: cannot find 'Read' in" e];
+    [(right; fast_done) || (left; fast_done) ||
+     fail "wp_read: order is neither Na2Ord nor ScOrd"
+    |iSolveTC
+    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+     iAssumptionCore || fail "wp_read: cannot find" l "↦ ?"
+    |simpl; try wp_value_head]
+  | _ => fail "wp_read: not a 'wp'"
+  end.
+
+Tactic Notation "wp_write" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_write K); [iSolveTC|..])
+      |fail 1 "wp_write: cannot find 'Write' in" e];
+    [(right; fast_done) || (left; fast_done) ||
+     fail "wp_write: order is neither Na2Ord nor ScOrd"
+    |iSolveTC
+    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+     iAssumptionCore || fail "wp_write: cannot find" l "↦ ?"
+    |pm_reflexivity
+    |simpl; try first [wp_pure (Seq (Lit LitPoison) _)|wp_value_head]]
+  | _ => fail "wp_write: not a 'wp'"
+  end.
diff --git a/theories/lang/swap.v b/theories/lang/swap.v
index 30f49cf6401b8f68983cd0fee92cf650c83a6809..30a59564890e465ca7f1390c895fd7f8d7932c84 100644
--- a/theories/lang/swap.v
+++ b/theories/lang/swap.v
@@ -10,7 +10,7 @@ Definition swap : val :=
          "p2" <- "x";;
          "swap" ["p1" +ₗ #1 ; "p2" +ₗ #1 ; "len" - #1].
 
-Lemma wp_swap `{noprolG Σ} tid E l1 l2 vl1 vl2 (n : Z):
+Lemma wp_swap `{!noprolG Σ} tid E l1 l2 vl1 vl2 (n : Z):
   ↑histN ⊆ E →  Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
     swap [ #l1; #l2; #n] in tid @ E
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 730e5f0d37e8d9f3d1e49d44fd2db01702b3c97f..d0bf4d770afe66562c89faa087fd196e2337cca6 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -9,12 +9,12 @@ Set Default Proof Using "Type".
    created, and the payload could be weakened without synchronizing
    with the end of the lifetime (remember that the underlying payload
    is not necessarily independent of the view for views older than V). *)
-Definition at_bor `{invG Σ, lftG Lat E0 Σ} κ N (P : monPred _ _) : monPred _ _ :=
+Definition at_bor `{!invG Σ, !lftG Lat E0 Σ} κ N (P : monPred _ _) : monPred _ _ :=
   (∃ i, ⌜N ## lftN⌝ ∗ &{κ,i}P ∗ ⎡inv N (∃ V', idx_bor_own i V')⎤)%I.
 Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
 
 Section atomic_bors.
-  Context `{invG Σ, lftG Lat E0 Σ}.
+  Context `{!invG Σ, !lftG Lat E0 Σ}.
 
   Global Instance at_bor_ne κ n N : Proper (dist n ==> dist n) (at_bor κ N).
   Proof. solve_proper. Qed.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 080dd9830e1fc2ea0fc23443ef9a76fa2b7528d5..e9206f03a8589208090c09eac69efcd277ad7f0f 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Definition frac_bor `{invG Σ, lftG Lat E0 Σ, frac_borG Σ} κ
+Definition frac_bor `{!invG Σ, !lftG Lat E0 Σ, !frac_borG Σ} κ
         (φ : Qp → monPred _ _) : monPred _ _ :=
   (* First, we close up to a bunch of things: iff, lifetime inclusion and view
      inclusion. We also existentially bind γ, the ghost name of receipts. *)
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 56220c216c92962f5c8c221aa37a37e50b26d984..283b2572d73c7bee6484dafc10d9d55c78f37b8c 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -26,7 +26,7 @@ Instance lft_inhabited : Inhabited lft := populate static.
 Canonical lftC := leibnizC lft.
 
 Section derived.
-Context `{invG Σ, lftG Lat E0 Σ}.
+Context `{!invG Σ, !lftG Lat E0 Σ}.
 Implicit Types κ : lft.
 
 Lemma lft_tok_dead_subj q κ :
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 358bf53311a888dbc3e6ca1904dfc6ff0476fa63..22432542fd84f1d92c9781d10cbb5e949d11e026 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -30,20 +30,20 @@ Module Type lifetime_sig.
   Context {Σ : gFunctors} {Lat}.
   Notation monPred := (monPredSI (lat_bi_index Lat) (uPredSI (iResUR Σ))).
 
-  Parameter lft_ctx : ∀ `{invG Σ, lftG Lat E0 Σ}, iProp Σ.
+  Parameter lft_ctx : ∀ `{!invG Σ, !lftG Lat E0 Σ}, iProp Σ.
 
-  Parameter lft_tok : ∀ `{lftG Lat E0 Σ} (q : Qp) (κ : lft), monPred.
-  Parameter lft_dead : ∀ `{lftG Lat E0 Σ} (κ : lft), monPred.
+  Parameter lft_tok : ∀ `{!lftG Lat E0 Σ} (q : Qp) (κ : lft), monPred.
+  Parameter lft_dead : ∀ `{!lftG Lat E0 Σ} (κ : lft), monPred.
 
-  Parameter lft_incl : ∀ `{invG Σ, lftG Lat E0 Σ} (κ κ' : lft), monPred.
-  Parameter bor : ∀ `{invG Σ, lftG Lat E0 Σ} (κ : lft) (P : monPred), monPred.
+  Parameter lft_incl : ∀ `{!invG Σ, !lftG Lat E0 Σ} (κ κ' : lft), monPred.
+  Parameter bor : ∀ `{!invG Σ, !lftG Lat E0 Σ} (κ : lft) (P : monPred), monPred.
 
   Parameter bor_idx : Type.
-  Parameter idx_bor_own : ∀ `{lftG Lat E0 Σ} (i : bor_idx), monPred.
+  Parameter idx_bor_own : ∀ `{!lftG Lat E0 Σ} (i : bor_idx), monPred.
   Parameter idx_bor :
-    ∀ `{invG Σ, lftG Lat E0 Σ} (κ : lft) (i : bor_idx) (P : monPred), monPred.
+    ∀ `{!invG Σ, !lftG Lat E0 Σ} (κ : lft) (i : bor_idx) (P : monPred), monPred.
 
-  Parameter in_at_bor : ∀ `{invG Σ, lftG Lat E0 Σ} (κ : lft) (P : monPred), monPred.
+  Parameter in_at_bor : ∀ `{!invG Σ, !lftG Lat E0 Σ} (κ : lft) (P : monPred), monPred.
   End defs.
 
   (** Notation *)
@@ -58,7 +58,7 @@ Module Type lifetime_sig.
   Infix "⊑" := lft_incl (at level 70) : bi_scope.
 
   Section properties.
-  Context `{invG Σ, lftG Lat E0 Σ}.
+  Context `{!invG Σ, !lftG Lat E0 Σ}.
 
   (** Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
@@ -191,7 +191,7 @@ Module Type lifetime_sig.
   Parameter lftΣ : latticeT → gFunctors.
   Global Declare Instance subG_lftPreG Lat Σ : subG (lftΣ Lat) Σ → lftPreG Lat Σ.
 
-  Parameter lft_init : ∀ `{invG Σ, !lftPreG Lat Σ} E E0,
+  Parameter lft_init : ∀ `{!invG Σ, !lftPreG Lat Σ} E E0,
       ↑lftN ⊆ E → ↑lftN ## E0 →
       (|={E}=> ∃ _ : lftG Lat E0 Σ, lft_ctx)%I.
 End lifetime_sig.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 084510de1553f9f94a5d69b318df7f2603e4fdec..3ae7fd4ecc5a61bc339fc878cd7efa2329e96efe 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import csum auth frac gmap agree gset.
 Set Default Proof Using "Type".
 
 Section accessors.
-Context `{invG Σ, lftG Lat E0 Σ}.
+Context `{!invG Σ, !lftG Lat E0 Σ}.
 Implicit Types κ : lft.
 
 (* Internal helper lemmas *)
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 16ef174adb6254bfe517e019a460a7dd80eba44a..061f6f807b0555b0ae195c93e3e4a0676d4fa336 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
 Section borrow.
-Context `{invG Σ, lftG Lat E0 Σ, LatBottom Lat}.
+Context `{!invG Σ, !lftG Lat E0 Σ, LatBottom Lat}.
 Implicit Types κ : lft.
 
 Lemma raw_bor_create E κ P :
@@ -57,7 +57,7 @@ Proof.
   + clear -HE. iIntros "!> H†".
     iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
     iDestruct ("HIlookup" with "HI") as %Hκ.
-    rewrite (big_sepS_elem_of_acc _ _ κ) //. iDestruct "Hinv" as "[Hinv Hclose']". 
+    rewrite (big_sepS_elem_of_acc _ _ κ) //. iDestruct "Hinv" as "[Hinv Hclose']".
     rewrite /lft_dead; iDestruct "H†" as (Λ V') "(% & #HV' & #H†)".
     iDestruct (own_alft_auth_agree A Λ (false, V') with "HA H†") as %EQAΛ.
     rewrite {1}/lft_inv; iDestruct "Hinv" as (Vκ) "[>HVκ [[_ >EQ]|[Hinv >%]]]".
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 7ce4049021d6cad1cbfa67053d389c1c08504f86..65f6a86e0e7c0f65c3474cf83a8867ff5aa7106e 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -28,7 +28,7 @@ Proof.
 Qed.
 
 Section borrow.
-Context `{invG Σ, lftG Lat E0 Σ, LatBottom Lat}.
+Context `{!invG Σ, !lftG Lat E0 Σ, LatBottom Lat}.
 Implicit Types κ : lft.
 
 Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index a95cd0391dab73b9bb618cf2f75ae9becc1a0f1c..5e9d45b8868871bda57fe4d6c99119e1575a56d7 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
 Section creation.
-Context `{invG Σ, lftG Lat E0 Σ, LatBottom Lat}.
+Context `{!invG Σ, !lftG Lat E0 Σ, LatBottom Lat}.
 Implicit Types κ : lft.
 
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) (Vs : lft → Lat) :
@@ -155,7 +155,7 @@ Lemma lft_create E :
 Proof.
   iIntros (?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  destruct (exist_fresh (dom (gset _) A)) as [Λ HΛ%not_elem_of_dom].
+  destruct (exist_fresh (dom (gset atomic_lft) A)) as [Λ HΛ%not_elem_of_dom].
   iMod (own_update with "HA") as "[HA HΛ]".
   { apply auth_update_alloc, (alloc_singleton_local_update _ Λ
            (Cinl (1%Qp, to_latT bot)))=>//. by rewrite lookup_fmap HΛ. }
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 1b1c2de8e04cc7ddd17a8e7c4e1442d977df8b6f..94bed26c60bbc86de4c0fb9e38f1267e29a2c1e2 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -84,7 +84,7 @@ Definition to_borUR {Lat} : gmap slice_name (bor_state Lat) → borUR Lat :=
   fmap Excl.
 
 Section defs.
-  Context {Σ Lat} `{invG Σ, lftG Lat E0 Σ}.
+  Context {Σ Lat} `{!invG Σ, !lftG Lat E0 Σ}.
 
   Notation iProp := (iProp Σ).
   Notation monPred := (monPredSI (lat_bi_index Lat) (uPredSI (iResUR Σ))).
@@ -237,7 +237,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   idx_bor_own idx_bor raw_bor bor.
 
 Section basic_properties.
-Context `{invG Σ, lftG Lat E0 Σ}.
+Context `{!invG Σ, !lftG Lat E0 Σ}.
 Implicit Types κ : lft.
 
 Notation iProp := (iProp Σ).
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 388b8f13e22527606d65ddd2bff41179f404d1fa..0e0016824c416ab60f386f69c0ea43ab3714612e 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
 Section faking.
-Context `{invG Σ, lftG Lat E0 Σ, LatBottom Lat bot}.
+Context `{!invG Σ, !lftG Lat E0 Σ, LatBottom Lat bot}.
 Implicit Types κ : lft.
 
 Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 66f0d929c6a938ead106571aa5baad1c7b33f8c4..6f906e018e039d41b277a775b90f774cbdabe15e 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -5,7 +5,7 @@ From lrust.lifetime.model Require Export definitions boxes.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma lft_init `{invG Σ, !lftPreG Lat Σ} E E0 :
+Lemma lft_init `{!invG Σ, !lftPreG Lat Σ} E E0 :
   ↑lftN ⊆ E → ↑lftN ## E0 → (|={E}=> ∃ _ : lftG Lat E0 Σ, lft_ctx)%I.
 Proof.
   iIntros (? HE0). rewrite /lft_ctx.
@@ -19,7 +19,7 @@ Proof.
 Qed.
 
 Section primitive.
-Context `{invG Σ, lftG Lat E0 Σ}.
+Context `{!invG Σ, !lftG Lat E0 Σ}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name (bor_state Lat)) i s :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 925ac0e678f68f92b171dc25beb4f3c44c088909..3b42ad682b22b40ee972c7fb346f66657564b2bd 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -29,7 +29,7 @@ Proof.
 Qed.
 
 Section reborrow.
-Context `{invG Σ, lftG Lat E0 Σ, LatBottom Lat}.
+Context `{!invG Σ, !lftG Lat E0 Σ, LatBottom Lat}.
 Implicit Types κ : lft.
 
 (* Notice that taking lft_inv for both κ and κ' already implies
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 3763f90146b8b9dea5dc280aacfa97c34f34dd80..5da27ef6803dafe820f9bd19b06d8274d9008c5d 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From gpfsl.logic Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition na_bor `{invG Σ, lftG View E0 Σ, na_invG View bot Σ}
+Definition na_bor `{!invG Σ, !lftG View E0 Σ, na_invG View bot Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : monPred _ _) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own i))%I.
 
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
     (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{invG Σ, lftG View E0 Σ, na_invG View bot Σ}
+  Context `{!invG Σ, !lftG View E0 Σ, na_invG View bot Σ}
           (tid : na_inv_pool_name) (N : namespace).
 
   Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 2dd004c00b8b067d452e1149ecb52115fab153e1..a4ef85d3e2cc3c9ac93cf0eaf02ae30c7fe2485c 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import programs.
 Set Default Proof Using "Type".
 
 Section bool.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition bool : type :=
     {| st_own tid vl :=
@@ -21,7 +21,7 @@ Section bool.
 End bool.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
   Proof.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index cb625d68d7359d287168753ad6ffdfadce751299..64007b0c797b477fb3a22ce34d68960b50ca58b5 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
   concurrently. *)
 
 Section borrow.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma tctx_borrow E L p n ty κ :
     tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 73a9b67263a782eda32bc8ba0d8ba68c3ac610a4..bc673b3d7ece76961f3ea4ac6fd496dc4d61ec38 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import programs.
 Set Default Proof Using "Type".
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** Jumping to and defining a continuation. *)
   Lemma type_jump args argsv E L C T k T' :
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index fe8125a43d477106f60f005ff206875b81e9df29..ee8bb53dadc5c39401ae90e9ed62af79836e5a10 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import type lft_contexts type_context.
 Set Default Proof Using "Type".
 
 Section cont_context_def.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition cont_postcondition : vProp Σ := True%I.
 
@@ -19,7 +19,7 @@ Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ T)
   (at level 70, format "k  ◁cont( L ,  T )").
 
 Section cont_context.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition cctx_elt_interp (tid : type.thread_id) (x : cctx_elt) : vProp Σ :=
     let '(k ◁cont(L, T)) := x in
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 53c49df048a16b0a8d30d6f79de364ca12113742..4e66d19cd4c24c73a941072441ddbdbed2d86d26 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -2,7 +2,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section get_x.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition get_x : val :=
     funrec: <> ["p"] :=
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index ceb1feb0b1fdfded6a4e6a5c1af2f153a632ddc7..6672bf91cd173ad84797469339b89d14e0f8139d 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -2,7 +2,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section init_prod.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition init_prod : val :=
     funrec: <> ["x"; "y"] :=
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 54cd056ff8a5773b26e53dd7f09aec11c5460f6b..c7b0777ad2a02d5333e786c949b1a7ccf29879bd 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -2,7 +2,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section lazy_lft.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition lazy_lft : val :=
     funrec: <> [] :=
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 91141690987ae86ac47a0066482a86dba24098e2..6a26e7bfdd240a0ee0b21adede5d82312a5fd54c 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -12,7 +12,7 @@ From lrust.typing Require Import typing lib.option.
 *)
 
 Section non_lexical.
-  Context `{typeG Σ} (HashMap K V : type)
+  Context `{!typeG Σ} (HashMap K V : type)
           `{!TyWf hashmap, !TyWf K, !TyWf V, !Copy K}
           (defaultv get_mut insert: val).
 
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index aeb0740cac53778e41ff7dc51d9dc0ffd6458798..ba08aef83d14f45f1cb695462c9cb47406005c40 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -2,7 +2,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section rebor.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition rebor : val :=
     funrec: <> ["t1"; "t2"] :=
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 302b78833add5ef989c6844d1a5618bf749ab0e2..b954b686bdd9191ddab695b8e32637bcce090509 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -2,7 +2,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section unbox.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition unbox : val :=
     funrec: <> ["b"] :=
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index ac73edb8e0225762b3fe2a4cc458d80ecbe32c8a..c039ac08ccb60d202fdd4fea99d549b712a4fea3 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Section fixpoint_def.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
 
   Global Instance type_inhabited : Inhabited type := populate bool.
@@ -25,7 +25,7 @@ Section fixpoint_def.
      I believe this gives the right sets for all types that we can define in
      Rust, but I do not have any proof of this.
      TODO : investigate this in more detail. *)
-  Global Instance type_fixpoint_wf `{∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
+  Global Instance type_fixpoint_wf `{!∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
     let lfts :=
       let _ : TyWf type_fixpoint := {| ty_lfts := []; ty_wf_E := [] |} in
       (T type_fixpoint).(ty_lfts)
@@ -37,13 +37,13 @@ Section fixpoint_def.
     {| ty_lfts := lfts; ty_wf_E := wf_E |}.
 End fixpoint_def.
 
-Lemma type_fixpoint_ne `{typeG Σ} (T1 T2 : type → type)
+Lemma type_fixpoint_ne `{!typeG Σ} (T1 T2 : type → type)
     `{!TypeContractive T1, !TypeContractive T2} n :
   (∀ t, T1 t ≡{n}≡ T2 t) → type_fixpoint T1 ≡{n}≡ type_fixpoint T2.
 Proof. eapply fixpointK_ne; apply type_contractive_ne, _. Qed.
 
 Section fixpoint.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
 
   Global Instance fixpoint_copy :
@@ -98,7 +98,7 @@ Section fixpoint.
 End fixpoint.
 
 Section subtyping.
-  Context `{typeG Σ} (E : elctx) (L : llctx).
+  Context `{!typeG Σ} (E : elctx) (L : llctx).
 
   (* TODO : is there a way to declare these as a [Proper] instances ? *)
   Lemma fixpoint_mono T1 `{!TypeContractive T1} T2 `{!TypeContractive T2} :
@@ -114,7 +114,7 @@ Section subtyping.
       apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
-  Lemma fixpoint_proper T1 `{TypeContractive T1} T2 `{TypeContractive T2} :
+  Lemma fixpoint_proper T1 `{!TypeContractive T1} T2 `{!TypeContractive T2} :
     (∀ ty1 ty2, eqtype E L ty1 ty2 → eqtype E L (T1 ty1) (T2 ty2)) →
     eqtype E L (type_fixpoint T1) (type_fixpoint T2).
   Proof.
@@ -127,16 +127,16 @@ Section subtyping.
         apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
-  Lemma fixpoint_unfold_subtype_l ty T `{TypeContractive T} :
+  Lemma fixpoint_unfold_subtype_l ty T `{!TypeContractive T} :
     subtype E L ty (T (type_fixpoint T)) → subtype E L ty (type_fixpoint T).
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_subtype_r ty T `{TypeContractive T} :
+  Lemma fixpoint_unfold_subtype_r ty T `{!TypeContractive T} :
     subtype E L (T (type_fixpoint T)) ty → subtype E L (type_fixpoint T) ty.
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_eqtype_l ty T `{TypeContractive T} :
+  Lemma fixpoint_unfold_eqtype_l ty T `{!TypeContractive T} :
     eqtype E L ty (T (type_fixpoint T)) → eqtype E L ty (type_fixpoint T).
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_eqtype_r ty T `{TypeContractive T} :
+  Lemma fixpoint_unfold_eqtype_r ty T `{!TypeContractive T} :
     eqtype E L (T (type_fixpoint T)) ty → eqtype E L (type_fixpoint T) ty.
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
 End subtyping.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index b38097b850bb45b77a4aab3b20f4ee021f897db9..30516b68c15f56c16ccfdcbfd1f5664febdfdb67 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 Implicit Types tid : thread_id.
 
 Section fn.
-  Context `{typeG Σ} {A : Type} {n : nat}.
+  Context `{!typeG Σ} {A : Type} {n : nat}.
 
   Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
 
@@ -142,7 +142,7 @@ Notation "'fn(' E ')' '→' R" :=
 Instance elctx_empty : Empty (lft → elctx) := λ ϝ, [].
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma fn_subtype {A n} E0 L0 (fp fp' : A → fn_params n) :
     (∀ x ϝ, let EE := E0 ++ (fp' x).(fp_E) ϝ in
@@ -395,7 +395,7 @@ Section typing.
   Qed.
 
   Lemma type_rec {A} E L fb (argsb : list binder) ef e n
-        (fp : A → fn_params n) T `{!CopyC T, !SendC T, Closed _ e} :
+        (fp : A → fn_params n) T `{!CopyC T, !SendC T, !Closed _ e} :
     IntoVal ef (funrec: fb argsb := e) →
     n = length argsb →
     □ (∀ x ϝ (f : val) k (args : vec val (length argsb)),
@@ -418,7 +418,7 @@ Section typing.
   Qed.
 
   Lemma type_fn {A} E L (argsb : list binder) ef e n
-        (fp : A → fn_params n) T `{!CopyC T, !SendC T, Closed _ e} :
+        (fp : A → fn_params n) T `{!CopyC T, !SendC T, !Closed _ e} :
     IntoVal ef (funrec: <> argsb := e) →
     n = length argsb →
     □ (∀ x ϝ k (args : vec val (length argsb)),
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 521f124c3d358440cec5669cdeff64b4cf0ba1c8..e2eb19b7adfffec4fad080ca32fb3208e1aac0f2 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import bool programs.
 Set Default Proof Using "Type".
 
 Section int.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition int : type :=
     {| st_own tid vl :=
@@ -22,7 +22,7 @@ Section int.
 End int.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma type_int_instr (z : Z) : typed_val #z int.
   Proof.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index ffd092fca40a0169b9785b1132318f8d0973711b..a3ffe31ebc2619f0a82e62fca5bd473dae18a45e 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -22,7 +22,7 @@ Notation llctx := (list llctx_elt).
 Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
 
 Section lft_contexts.
-  Context `{invG Σ, lftG view_Lat (↑histN) Σ}.
+  Context `{!invG Σ, !lftG view_Lat (↑histN) Σ}.
   Implicit Type (κ : lft).
 
   (* External lifetime contexts. *)
@@ -308,7 +308,7 @@ Arguments elctx_sat {_ _ _} _ _ _.
 Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
 Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
 
-Lemma elctx_sat_submseteq `{invG Σ, lftG view_Lat (↑histN) Σ} E E' L :
+Lemma elctx_sat_submseteq `{!invG Σ, !lftG view_Lat (↑histN) Σ} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ?) "_ !# H". by iApply big_sepL_submseteq. Qed.
 
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 76aafdbf02c2ac9cd427370dd31115dda1ffd7b5..f76926ac34a251f04b0041703e221d372485ea06 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section cell.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition cell (ty : type) :=
     {| ty_size := ty.(ty_size);
@@ -79,7 +79,7 @@ Section cell.
 End cell.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** The next couple functions essentially show owned-type equalities, as they
       are all different types for the identity function. *)
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index fef8969af1a4323e47e4afd5ccc94b87bb41fa7a..283ea8baaf801ef5b7a9bda0f7f81c1e2892ef27 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section fake_shared.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition fake_shared_box : val :=
     funrec: <> ["x"] := Skip ;; return: ["x"].
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 8ac02855e498e77614ddcd504365133fb0783a25..b7d0b2fd5ed038782bf65f517db52866c20dafd3 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing lib.panic.
 Set Default Proof Using "Type".
 
 Section option.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition option (τ : type) := Σ[unit; τ]%T.
 
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 5296c6c4c7ac7d9d63548977860c605295f10dc2..f6a6b094f87a94a6605e424d6cdb27f7ab83d584 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -11,7 +11,7 @@ Set Default Proof Using "Type".
    [take_mut]. *)
 
 Section panic.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition panic : val :=
     funrec: <> [] := #☠.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 24fd5b888ae8142d0732af2ab14ff4d491a04886..321feb64ae5094cef07641ffba6636fefbab8f8f 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
 Definition refcell_refN := refcellN .@ "ref".
 
 Section ref.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   (* The Rust type looks as follows (after some unfolding):
 
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index dbc32513a4a3821fd25e5c2f89583a840780a55b..2d368942963eb6fff536e571d11a461233ac3479 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.refcell Require Import refcell ref.
 Set Default Proof Using "Type".
 
 Section ref_functions.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   Lemma refcell_inv_reading_inv tid l γ α ty q ν :
     refcell_inv tid l γ α ty -∗
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 86fe5ec9255704695a847b19351fc5e741c0117c..4b97cb064902ace43b609131742dda1dfd604bc0 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -39,7 +39,7 @@ Definition refcellN := lrustN .@ "refcell".
 Definition refcell_invN := refcellN .@ "inv".
 
 Section refcell_inv.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   Definition refcell_inv tid (l : loc) (γ : gname) (α : lft) ty : vProp Σ :=
     (∃ st, l ↦ #(Z_of_refcell_st st) ∗ ⎡own γ (● (refcell_st_to_R st))⎤ ∗
@@ -93,7 +93,7 @@ Section refcell_inv.
 End refcell_inv.
 
 Section refcell.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   (* Original Rust type:
      pub struct RefCell<T: ?Sized> {
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index dc46e979165861ddfa388abb177c2a6730209bda..d0a55fece40b7c2046ad7ede5caba7d022b5d272 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.refcell Require Import refcell ref refmut.
 Set Default Proof Using "Type".
 
 Section refcell_functions.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   (* Constructing a refcell. *)
   Definition refcell_new ty : val :=
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index ed13740bcbf9d538583bd04a9ad3ddc7e88d5641..9161ac9d3c37c50df6e8baf790d5e365d8f64e4b 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -6,7 +6,7 @@ From lrust.typing.lib.refcell Require Import refcell.
 Set Default Proof Using "Type".
 
 Section refmut.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   (* The Rust type looks as follows (after some unfolding):
 
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 7bad72885969f5205706944a76b37f3812d8f110..0610118a3fc7b1cf25cd4611baf264d68dfda25c 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.refcell Require Import refcell refmut.
 Set Default Proof Using "Type".
 
 Section refmut_functions.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   (* Turning a refmut into a shared borrow. *)
   Definition refmut_deref : val :=
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 7afa869b6c09eb37a7a8afdcb3373c877257b325..b2166089f1004bcf0f4123102b740d62e6bc8911 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -44,7 +44,7 @@ Notation st_global st:= (● rwlock_to_st st).
 Notation st_local st := (◯ rwlock_to_st st).
 
 Section rwlock_inv.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
   Local Notation vProp := (vProp Σ).
 
   (* Cmra operations *)
@@ -357,7 +357,7 @@ Section rwlock_inv.
 End rwlock_inv.
 
 Section rwlock.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Original Rust type (we ignore poisoning):
      pub struct RwLock<T: ?Sized> {
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 8ca026100b936a9b6e1a5231ac4c87a618815832..3d29bd596ce936b6be19ee2ec38650d82222ac99 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -22,7 +22,7 @@ Set Default Proof Using "Type".
   - read_unlock uses a release CAS *)
 
 Section rwlock_functions.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Constructing a rwlock. *)
   Definition rwlock_new ty : val :=
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 1a6347111210771f6d1e676670c9b08db8f371f0..2f9d709e2758c1c310feed2425514e1d919c29b2 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -8,7 +8,7 @@ From gpfsl.gps Require Import middleware.
 Set Default Proof Using "Type".
 
 Section rwlockreadguard.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Original Rust type:
     pub struct RwLockReadGuard<'a, T: ?Sized + 'a> {
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 6ac29164b0f3def734039284b00c29f86e55cc99..a1d00eb5bda63188910de1ee60d950da1b8bac36 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -10,7 +10,7 @@ From lrust.logic Require Import gps.
 Set Default Proof Using "Type".
 
 Section rwlockreadguard_functions.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Turning a rwlockreadguard into a shared borrow. *)
   Definition rwlockreadguard_deref : val :=
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 7d16364e5b99e62a59f1aa2801e9d1e3e2c5b4f9..fbf9044936922c08b32fc764e031de454bf5b05b 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -8,7 +8,7 @@ From gpfsl.gps Require Import middleware.
 Set Default Proof Using "Type".
 
 Section rwlockwriteguard.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Original Rust type (we ignore poisoning):
       pub struct RwLockWriteGuard<'a, T: ?Sized + 'a> {
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index aa9174d8fd789557943609baed5c1062e59fcb7a..6d0fa49c80be0f9be6026d2a767fda794cc05a7f 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -10,7 +10,7 @@ From lrust.logic Require Import gps.
 Set Default Proof Using "Type".
 
 Section rwlockwriteguard_functions.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Turning a rwlockwriteguard into a shared borrow. *)
   Definition rwlockwriteguard_deref : val :=
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index 063eb3b57275634daefed254ad50dc2902c66a61..161efa5ef83715e617f33d0469aadd91dd2b6e24 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -3,7 +3,7 @@ From lrust.lang Require Import swap.
 Set Default Proof Using "Type".
 
 Section swap.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition swap ty : val :=
     funrec: <> ["p1"; "p2"] :=
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 2c1617eba44a6ddd65d5a2b1c94cecf4d650748c..2c43e944140d08b6f67c3f88631f73f685006995 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section code.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition take ty (call_once : val) : val :=
     funrec: <> ["x"; "f"] :=
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 9fc5b5fa68c4b302411300728544849272ec6431..d73f29500b7da92a4f8d0fc2c995d020e9e15455 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import util uninit type_context programs.
 Set Default Proof Using "Type".
 
 Section own.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
     match sz, n return _ with
@@ -148,7 +148,7 @@ Section own.
 End own.
 
 Section box.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition box ty := own_ptr ty.(ty_size) ty.
 
@@ -185,7 +185,7 @@ Section box.
 End box.
 
 Section util.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma ownptr_own n ty tid v :
     (own_ptr n ty).(ty_own) tid [v] ⊣⊢
@@ -216,7 +216,7 @@ Section util.
 End util.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** Typing *)
   Lemma write_own {E L} ty ty' n :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index fc4a8d9af4cc7aa65d554d13d64c277fbe2d592c..a1c70ad919878bb653b6705c25787c7846c8e4c6 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -5,7 +5,7 @@ From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
 Section product.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (* TODO: Find a better spot for this. *)
   Lemma Z_nat_add (n1 n2 : nat) : Z.to_nat (n1 + n2) = (n1 + n2)%nat.
@@ -194,7 +194,7 @@ End product.
 Notation Π := product.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Global Instance prod2_assoc E L : Assoc (eqtype E L) product2.
   Proof.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 8130c5aedd2385fd4650d2049abb323c4aec0821..ac4177678019c775375159806cad513006c954ec 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import type_context lft_contexts product own uniq_bor
 Set Default Proof Using "Type".
 
 Section product_split.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** General splitting / merging for pointer types *)
   Fixpoint hasty_ptr_offsets (p : path) (ptr: type → type) tyl (off : nat) : tctx :=
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 5a266503cd2fe32a7f6dafef957c2a6745a9d1ef..2be078c81c64fe3c34afe24328889a70c08fda6d 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 Implicit Types tid : thread_id.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** Function Body *)
   (* This is an iProp because it is also used by the function type. *)
@@ -80,17 +80,17 @@ Section typing.
   Global Arguments typed_read _ _ _%T _%T _%T.
 End typing.
 
-Definition typed_instruction_ty `{typeG Σ} (E : elctx) (L : llctx) (T : tctx)
+Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
     (e : expr) (ty : type) : vPropI Σ :=
   typed_instruction E L T e (λ v, [v ◁ ty]).
 Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
 
-Definition typed_val `{typeG Σ} (v : val) (ty : type) : Prop :=
+Definition typed_val `{!typeG Σ} (v : val) (ty : type) : Prop :=
   ∀ E L, typed_instruction_ty E L [] (of_val v) ty.
 Arguments typed_val _ _ _%V _%T.
 
 Section typing_rules.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (* This lemma is helpful when switching from proving unsafe code in Iris
      back to proving it in the type system. *)
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index b3a58cbf69bc02be96e2b7b3723c217666c9a9f9..4a4474512df53b38315dc78daf98558ff28f334d 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import lft_contexts type_context programs.
 Set Default Proof Using "Type".
 
 Section shr_bor.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition shr_bor (κ : lft) (ty : type) : type :=
     {| st_own tid vl :=
@@ -60,7 +60,7 @@ End shr_bor.
 Notation "&shr{ κ }" := (shr_bor κ) (format "&shr{ κ }") : lrust_type_scope.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma shr_mono' E L κ1 κ2 ty1 ty2 :
     lctx_lft_incl E L κ2 κ1 → subtype E L ty1 ty2 →
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 88594efdf5f732e8755d4425676bae25b5a6c8e2..2ccbebc0cfdc6a8e9ef6dcbe7bf47fb50ace3b0d 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -23,10 +23,10 @@ Proof. solve_inG. Qed.
 Section type_soundness.
   Definition exit_cont : val := λ: [<>], #☠.
 
-  Definition main_type `{typeG Σ} := (fn(∅) → unit)%T.
+  Definition main_type `{!typeG Σ} := (fn(∅) → unit)%T.
 
-  Theorem type_soundness `{typePreG Σ} (main : val) σ t :
-    (∀ `{typeG Σ}, typed_val main main_type) →
+  Theorem type_soundness `{!typePreG Σ} (main : val) σ t :
+    (∀ `{!typeG Σ}, typed_val main main_type) →
     rtc erased_step ([(main [exit_cont] at init_tview)%E], mkGB ∅ ∅ ∅) (t, σ) →
     (* nonracing_threadpool t σ ∧ *)   (* TODO : prove DRF theorem *)
     (∀ e 𝓥, (e at 𝓥)%E ∈ t → is_Some (to_val e) ∨ reducible (e at 𝓥) σ).
@@ -64,7 +64,7 @@ End type_soundness.
 (* Soundness theorem when no other CMRA is needed. *)
 
 Theorem type_soundness_closed (main : val) σ t :
-  (∀ `{typeG typeΣ}, typed_val main main_type) →
+  (∀ `{!typeG typeΣ}, typed_val main main_type) →
   rtc erased_step ([(main [exit_cont] at init_tview)%E], mkGB ∅ ∅ ∅) (t, σ) →
   (* nonracing_threadpool t σ ∧ *)   (* TODO : prove DRF theorem *)
   (∀ e 𝓥, (e at 𝓥)%E ∈ t → is_Some (to_val e) ∨ reducible (e at 𝓥) σ).
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 33c31594e7279e656f7d29a4574da67562f5b030..bbfa4ab43b14e03f07a2094d64b18947bdabcdde 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -5,7 +5,7 @@ From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
 Section sum.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (* We define the actual empty type as being the empty sum, so that it is
      convertible to it---and in particular, we can pattern-match on it
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 5366feb1cb80ab9e45d52cb5129187fb1b9d6a20..4e054112101eb35d9947e8123dc44f6cce559f87 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -21,7 +21,7 @@ Record thread_id :=
   { tid_na_inv_pool :> na_inv_pool_name;
     tid_tid :> history.thread_id }.
 
-Record type `{typeG Σ} :=
+Record type `{!typeG Σ} :=
   { ty_size : nat;
     ty_own : thread_id → list val → vProp Σ;
     ty_shr : lft → thread_id → loc → vProp Σ;
@@ -55,14 +55,14 @@ Instance: Params (@ty_shr) 2 := {}.
 
 Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
 
-Class TyWf `{typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
+Class TyWf `{!typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
 Arguments ty_lfts {_ _} _ {_}.
 Arguments ty_wf_E {_ _} _ {_}.
 
-Definition ty_outlives_E `{typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
+Definition ty_outlives_E `{!typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
   (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
 
-Lemma ty_outlives_E_elctx_sat `{typeG Σ} E L ty `{!TyWf ty} α β :
+Lemma ty_outlives_E_elctx_sat `{!typeG Σ} E L ty `{!TyWf ty} α β :
   ty_outlives_E ty β ⊆+ E →
   lctx_lft_incl E L α β →
   elctx_sat E L (ty_outlives_E ty α).
@@ -76,34 +76,34 @@ Proof.
 Qed.
 
 (* Lift TyWf to lists.  We cannot use `Forall` because that one is restricted to Prop. *)
-Inductive TyWfLst `{typeG Σ} : list type → Type :=
+Inductive TyWfLst `{!typeG Σ} : list type → Type :=
 | tyl_wf_nil : TyWfLst []
 | tyl_wf_cons ty tyl `{!TyWf ty, !TyWfLst tyl} : TyWfLst (ty::tyl).
 Existing Class TyWfLst.
 Existing Instances tyl_wf_nil tyl_wf_cons.
 
-Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
+Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
   match WF with
   | tyl_wf_nil => []
   | tyl_wf_cons ty [] => ty.(ty_lfts)
   | tyl_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
   end.
 
-Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
+Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
   match WF with
   | tyl_wf_nil => []
   | tyl_wf_cons ty [] => ty.(ty_wf_E)
   | tyl_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
   end.
 
-Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
+Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
   match WF with
   | tyl_wf_nil => []
   | tyl_wf_cons ty [] => ty_outlives_E ty κ
   | tyl_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
   end.
 
-Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
+Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
   tyl_outlives_E tyl β ⊆+ E →
   lctx_lft_incl E L α β →
   elctx_sat E L (tyl_outlives_E tyl α).
@@ -115,14 +115,14 @@ Proof.
       (etrans; [|done]); solve_typing.
 Qed.
 
-Record simple_type `{typeG Σ} :=
+Record simple_type `{!typeG Σ} :=
   { st_own : thread_id → list val → vProp Σ;
     st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
     st_own_persistent tid vl : Persistent (st_own tid vl) }.
 Existing Instance st_own_persistent.
 Instance: Params (@st_own) 2 := {}.
 
-Program Definition ty_of_st `{typeG Σ} (st : simple_type) : type :=
+Program Definition ty_of_st `{!typeG Σ} (st : simple_type) : type :=
   {| ty_size := 1; ty_own := st.(st_own);
      (* [st.(st_own) tid vl] needs to be outside of the fractured
          borrow, otherwise I do not know how to prove the shr part of
@@ -151,7 +151,7 @@ Bind Scope lrust_type_scope with type.
 
 (* OFE and COFE structures on types and simple types. *)
 Section ofe.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Inductive type_equiv' (ty1 ty2 : type) : Prop :=
     Type_equiv :
@@ -262,7 +262,7 @@ End ofe.
 
 (** Special metric for type-nonexpansive and Type-contractive functions. *)
 Section type_dist2.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (* Size and shr are n-equal, but own is only n-1-equal.
      We need this to express what shr has to satisfy on a Type-NE-function:
@@ -330,7 +330,7 @@ Notation TypeNonExpansive T := (∀ n, Proper (type_dist2 n ==> type_dist2 n) T)
 Notation TypeContractive T := (∀ n, Proper (type_dist2_later n ==> type_dist2 n) T).
 
 Section type_contractive.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma type_ne_dist_later T :
     TypeNonExpansive T → ∀ n, Proper (type_dist2_later n ==> type_dist2_later n) T.
@@ -391,7 +391,7 @@ Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
   | S n => ↑shrN.@l ∪ shr_locsE (l +ₗ 1) n
   end.
 
-Class Copy `{typeG Σ} (t : type) := {
+Class Copy `{!typeG Σ} (t : type) := {
   copy_persistent tid vl : Persistent (t.(ty_own) tid vl);
   copy_shr_acc κ tid E F l q :
     lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
@@ -404,34 +404,34 @@ Class Copy `{typeG Σ} (t : type) := {
 Existing Instances copy_persistent.
 Instance: Params (@Copy) 2 := {}.
 
-Class LstCopy `{typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
+Class LstCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
 Instance: Params (@LstCopy) 2 := {}.
-Global Instance lst_copy_nil `{typeG Σ} : LstCopy [] := List.Forall_nil _.
-Global Instance lst_copy_cons `{typeG Σ} ty tys :
+Global Instance lst_copy_nil `{!typeG Σ} : LstCopy [] := List.Forall_nil _.
+Global Instance lst_copy_cons `{!typeG Σ} ty tys :
   Copy ty → LstCopy tys → LstCopy (ty :: tys) := List.Forall_cons _ _ _.
 
-Class Send `{typeG Σ} (t : type) :=
+Class Send `{!typeG Σ} (t : type) :=
   send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
 Instance: Params (@Send) 2 := {}.
 
-Class LstSend `{typeG Σ} (tys : list type) := lst_send : Forall Send tys.
+Class LstSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
 Instance: Params (@LstSend) 2 := {}.
-Global Instance lst_send_nil `{typeG Σ} : LstSend [] := List.Forall_nil _.
-Global Instance lst_send_cons `{typeG Σ} ty tys :
+Global Instance lst_send_nil `{!typeG Σ} : LstSend [] := List.Forall_nil _.
+Global Instance lst_send_cons `{!typeG Σ} ty tys :
   Send ty → LstSend tys → LstSend (ty :: tys) := List.Forall_cons _ _ _.
 
-Class Sync `{typeG Σ} (t : type) :=
+Class Sync `{!typeG Σ} (t : type) :=
   sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
 Instance: Params (@Sync) 2 := {}.
 
-Class LstSync `{typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
+Class LstSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
 Instance: Params (@LstSync) 2 := {}.
-Global Instance lst_sync_nil `{typeG Σ} : LstSync [] := List.Forall_nil _.
-Global Instance lst_sync_cons `{typeG Σ} ty tys :
+Global Instance lst_sync_nil `{!typeG Σ} : LstSync [] := List.Forall_nil _.
+Global Instance lst_sync_cons `{!typeG Σ} ty tys :
   Sync ty → LstSync tys → LstSync (ty :: tys) := List.Forall_cons _ _ _.
 
 Section type.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** Copy types *)
   Lemma shr_locsE_shift l n m :
@@ -522,24 +522,24 @@ Section type.
   Qed.
 End type.
 
-Definition type_incl `{typeG Σ} (ty1 ty2 : type) : vPropI Σ :=
+Definition type_incl `{!typeG Σ} (ty1 ty2 : type) : vPropI Σ :=
     (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
      (□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
 Instance: Params (@type_incl) 2 := {}.
 (* Typeclasses Opaque type_incl. *)
 
-Definition subtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
   ∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
 Instance: Params (@subtype) 4 := {}.
 
 (* TODO: The prelude should have a symmetric closure. *)
-Definition eqtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+Definition eqtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
   subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
 Instance: Params (@eqtype) 4 := {}.
 
 Section subtyping.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Global Instance type_incl_ne : NonExpansive2 type_incl.
   Proof.
@@ -673,7 +673,7 @@ Section subtyping.
 End subtyping.
 
 Section type_util.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma heap_mapsto_ty_own l ty tid :
     l ↦∗: ty_own ty tid ⊣⊢ ∃ (vl : vec val ty.(ty_size)), l ↦∗ vl ∗ ty_own ty tid vl.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 3f8cddb1335e87b3a6d2fd9ed1143713a80a5b66..c207d5da8a2a3b03b296b738b95a64be3d3499af 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -8,7 +8,7 @@ Bind Scope expr_scope with path.
 
 (* TODO: Consider making this a pair of a path and the rest. We could
    then e.g. formulate tctx_elt_hasty_path more generally. *)
-Inductive tctx_elt `{typeG Σ} : Type :=
+Inductive tctx_elt `{!typeG Σ} : Type :=
 | TCtx_hasty (p : path) (ty : type)
 | TCtx_blocked (p : path) (κ : lft) (ty : type).
 
@@ -19,7 +19,7 @@ Notation "p ◁{ κ } ty" := (TCtx_blocked p κ ty)
    (at level 70, format "p  ◁{ κ }  ty").
 
 Section type_context.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
   Implicit Types T : tctx.
 
   Fixpoint eval_path (p : path) : option val :=
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 7ef3d4c81d7f40aee0b79f2aaf1c6c152843b72a..94dc27837858680a9b5556e2e66e449bc3e1bd9b 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import lft_contexts type_context programs product.
 Set Default Proof Using "Type".
 
 Section case.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (* FIXME : have a iris version of Forall2. *)
   Lemma type_case_own' E L C T p n tyl el :
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 28875d508995b63e6d3007e02a4a93a2b9c9e463..214c359f1aaae06ac98b3463810d04a8ae4a4a0f 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import product.
 Set Default Proof Using "Type".
 
 Section uninit.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition uninit_1 : type :=
     {| st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 0e59532a02f8fab2ec580fda5445eb8e39ed0d51..097df4d72f61f9fb9c2da8887e282df6d687d907 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import util lft_contexts type_context programs.
 Set Default Proof Using "Type".
 
 Section uniq_bor.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition uniq_bor (κ:lft) (ty:type) :=
     {| ty_size := 1;
@@ -97,7 +97,7 @@ End uniq_bor.
 Notation "&uniq{ κ }" := (uniq_bor κ) (format "&uniq{ κ }") : lrust_type_scope.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma uniq_mono' E L κ1 κ2 ty1 ty2 :
     lctx_lft_incl E L κ2 κ1 → eqtype E L ty1 ty2 →