diff --git a/README.md b/README.md
index 0634f073b25b6d67b13022436c737945836601e3..f9e6a9b9f5e752cca64cc3ab468c04a3599fa9c3 100644
--- a/README.md
+++ b/README.md
@@ -33,11 +33,11 @@ CPU cores.
 
 * The folder [lang](theories/lang) contains the formalization of abstract
   specifications for several data structures in the [ORC11] relaxed memory
-  semantics. These data structures are the building blocks for the RMRM's
+  semantics. These data structures are the building blocks for the RBrlx's
   version of Rust libraries.
   * The repository [ORC11] formalizes the operational relaxed memory semantics
-    employed by RMRM.
-  * The repository [GPFSL] formalizes the actual language of RMRM, as well as
+    employed by RBrlx.
+  * The repository [GPFSL] formalizes the actual language of RBrlx, as well as
     the logic for general verification of programs written that language. The
     language combines ORC11 with an CPS-style expression language (following
     that of lambda-Rust).
@@ -167,8 +167,8 @@ lifetime logic is in [lifetime_sig.v](theories/lifetime/lifetime_sig.v).
 
 * Do the change in [GPFSL], push it.
 * Wait for CI to publish a new Iris version on the opam archive.
-* In RMRM, change opam to depend on the new version.
-* Run `make build-dep` (in RMRM) to install the new version of Iris.
+* In RBrlx, change opam to depend on the new version.
+* Run `make build-dep` (in RBrlx) to install the new version of Iris.
 * You may have to do `make clean` as Coq will likely complain about .vo file
   mismatches.
 
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
deleted file mode 100644
index 7ea33f076ef2ee264da84a6ba65ac5c20660720a..0000000000000000000000000000000000000000
--- a/theories/lang/adequacy.v
+++ /dev/null
@@ -1,32 +0,0 @@
-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/lang.v b/theories/lang/lang.v
deleted file mode 100644
index cd64baa245f76e4c1fa06e997840c6e782820f2b..0000000000000000000000000000000000000000
--- a/theories/lang/lang.v
+++ /dev/null
@@ -1,660 +0,0 @@
-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/lifting.v b/theories/lang/lifting.v
deleted file mode 100644
index 2da5f05eb6849d61538c86685326918cf26af522..0000000000000000000000000000000000000000
--- a/theories/lang/lifting.v
+++ /dev/null
@@ -1,377 +0,0 @@
-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/proofmode.v b/theories/lang/proofmode.v
deleted file mode 100644
index 4abc2eaadd41f86ed351926f10afce2540d5252c..0000000000000000000000000000000000000000
--- a/theories/lang/proofmode.v
+++ /dev/null
@@ -1,259 +0,0 @@
-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/races.v b/theories/lang/races.v
deleted file mode 100644
index 1423c77f6f34c3e92693a79d0a1ce2d134f9845d..0000000000000000000000000000000000000000
--- a/theories/lang/races.v
+++ /dev/null
@@ -1,299 +0,0 @@
-From stdpp Require Import gmap.
-From iris.program_logic Require Export hoare.
-From iris.program_logic Require Import adequacy.
-From lrust.lang Require Import tactics.
-Set Default Proof Using "Type".
-
-Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
-
-(* This is a crucial definition; if we forget to sync it with head_step,
-   the results proven here are worthless. *)
-Inductive next_access_head : expr → state → access_kind * order → loc → Prop :=
-| Access_read ord l σ :
-    next_access_head (Read ord (Lit $ LitLoc l)) σ (ReadAcc, ord) l
-| Access_write ord l e σ :
-    is_Some (to_val e) →
-    next_access_head (Write ord (Lit $ LitLoc l) e) σ (WriteAcc, ord) l
-| Access_cas_fail l st e1 lit1 e2 lit2 litl σ :
-    to_val e1 = Some (LitV lit1) → to_val e2 = Some (LitV lit2) →
-    lit_neq lit1 litl → σ !! l = Some (st, LitV litl) →
-    next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (ReadAcc, ScOrd) l
-| Access_cas_suc l st e1 lit1 e2 lit2 litl σ :
-    to_val e1 = Some (LitV lit1) → to_val e2 = Some (LitV lit2) →
-    lit_eq σ lit1 litl → σ !! l = Some (st, LitV litl) →
-    next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (WriteAcc, ScOrd) l
-| Access_free n l σ i :
-    0 ≤ i < n →
-    next_access_head (Free (Lit $ LitInt n) (Lit $ LitLoc l))
-                     σ (FreeAcc, Na2Ord) (l +ₗ i).
-
-(* Some sanity checks to make sure the definition above is not entirely insensible. *)
-Goal ∀ e1 e2 e3 σ, head_reducible (CAS e1 e2 e3) σ →
-                   ∃ a l, next_access_head (CAS e1 e2 e3) σ a l.
-Proof.
-  intros ??? σ (?&?&?&?&?). inversion H; do 2 eexists;
-    (eapply Access_cas_fail; done) || eapply Access_cas_suc; done.
-Qed.
-Goal ∀ o e σ, head_reducible (Read o e) σ →
-              ∃ a l, next_access_head (Read o e) σ a l.
-Proof.
-  intros ?? σ (?&?&?&?&?). inversion H; do 2 eexists; eapply Access_read; done.
-Qed.
-Goal ∀ o e1 e2 σ, head_reducible (Write o e1 e2) σ →
-              ∃ a l, next_access_head (Write o e1 e2) σ a l.
-Proof.
-  intros ??? σ (?&?&?&?&?). inversion H; do 2 eexists;
-    eapply Access_write; try done; eexists; done.
-Qed.
-Goal ∀ e1 e2 σ, head_reducible (Free e1 e2) σ →
-              ∃ a l, next_access_head (Free e1 e2) σ a l.
-Proof.
-  intros ?? σ (?&?&?&?&?). inversion H; do 2 eexists; eapply Access_free; done.
-Qed.
-
-Definition next_access_thread (e: expr) (σ : state)
-           (a : access_kind * order) (l : loc) : Prop :=
-  ∃ K e', next_access_head e' σ a l ∧ e = fill K e'.
-
-Definition next_accesses_threadpool (el: list expr) (σ : state)
-           (a1 a2 : access_kind * order) (l : loc): Prop :=
-  ∃ t1 e1 t2 e2 t3, el = t1 ++ e1 :: t2 ++ e2 :: t3 ∧
-                    next_access_thread e1 σ a1 l ∧ next_access_thread e2 σ a2 l.
-
-Definition nonracing_accesses (a1 a2 : access_kind * order) : Prop :=
-  match a1, a2 with
-  | (_, ScOrd), (_, ScOrd) => True
-  | (ReadAcc, _), (ReadAcc, _) => True
-  | _, _ => False
-  end.
-
-Definition nonracing_threadpool (el : list expr) (σ : state) : Prop :=
-  ∀ l a1 a2, next_accesses_threadpool el σ a1 a2 l →
-             nonracing_accesses a1 a2.
-
-Lemma next_access_head_reductible_ctx e σ σ' a l K :
-  next_access_head e σ' a l → reducible (fill K e) σ → head_reducible e σ.
-Proof.
-  intros Hhead Hred. apply prim_head_reducible.
-  - eapply (reducible_fill (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
-  - apply ectxi_language_sub_redexes_are_values. intros [] ? ->; inversion Hhead; eauto.
-Qed.
-
-Definition head_reduce_not_to_stuck (e : expr) (σ : state) :=
-  ∀ κ e' σ' efs, ectx_language.head_step e σ κ e' σ' efs → e' ≠ App (Lit $ LitInt 0) [].
-
-Lemma next_access_head_reducible_state e σ a l :
-  next_access_head e σ a l → head_reducible e σ →
-  head_reduce_not_to_stuck e σ →
-  match a with
-  | (ReadAcc, ScOrd | Na1Ord) => ∃ v n, σ !! l = Some (RSt n, v)
-  | (ReadAcc, Na2Ord) => ∃ v n, σ !! l = Some (RSt (S n), v)
-  | (WriteAcc, ScOrd | Na1Ord) => ∃ v, σ !! l = Some (RSt 0, v)
-  | (WriteAcc, Na2Ord) => ∃ v, σ !! l = Some (WSt, v)
-  | (FreeAcc, _) => ∃ v ls, σ !! l = Some (ls, v)
-  end.
-Proof.
-  intros Ha (κ&e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_head_step; eauto.
-  - destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
-    by eapply CasStuckS.
-  - exfalso. eapply Hrednonstuck; last done.
-    eapply CasStuckS; done.
-  - match goal with H : ∀ m, _ |- _ => destruct (H i) as [_ [[]?]] end; eauto.
-Qed.
-
-Lemma next_access_head_Na1Ord_step e1 e2 ef σ1 σ2 κ a l :
-  next_access_head e1 σ1 (a, Na1Ord) l →
-  head_step e1 σ1 κ e2 σ2 ef →
-  next_access_head e2 σ2 (a, Na2Ord) l.
-Proof.
-  intros Ha Hstep. inversion Ha; subst; clear Ha; inv_head_step; constructor; by rewrite to_of_val.
-Qed.
-
-Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' κ a1 a2 l :
-  next_access_head e1 σ (a1, Na1Ord) l →
-  head_step e1 σ κ e1' σ' e'f →
-  next_access_head e2 σ a2 l →
-  next_access_head e2 σ' a2 l.
-Proof.
-  intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_head_step;
-  destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
-  (* Oh my. FIXME. *)
-  - eapply lit_eq_state; last done.
-    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
-  - eapply lit_eq_state; last done.
-    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
-Qed.
-
-Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' κ o1 a2 l :
-  next_access_head e1 σ (FreeAcc, o1) l → head_step e1 σ κ e1' σ' e'f →
-  next_access_head e2 σ a2 l → head_reducible e2 σ' →
-  False.
-Proof.
-  intros Ha1 Hstep Ha2 Hred2.
-  assert (FREE : ∀ l n i, 0 ≤ i ∧ i < n → free_mem l (Z.to_nat n) σ !! (l +ₗ i) = None).
-  { clear. intros l n i Hi.
-    replace n with (Z.of_nat (Z.to_nat n)) in Hi by (apply Z2Nat.id; lia).
-    revert l i Hi. induction (Z.to_nat n) as [|? IH]=>/=l i Hi. lia.
-    destruct (decide (i = 0)).
-    - subst. by rewrite /shift_loc Z.add_0_r -surjective_pairing lookup_delete.
-    - replace i with (1+(i-1)) by lia.
-      rewrite lookup_delete_ne -shift_loc_assoc ?IH //. lia.
-      destruct l; intros [=?]. lia. }
-  assert (FREE' : σ' !! l = None).
-  { inversion Ha1; clear Ha1; inv_head_step. auto. }
-  destruct Hred2 as (κ'&e2'&σ''&ef&?).
-  inversion Ha2; clear Ha2; inv_head_step.
-  eapply (@is_Some_None (lock_state * val)). rewrite -FREE'. naive_solver.
-Qed.
-
-Lemma safe_step_not_reduce_to_stuck el σ K e e' σ' ef κ :
-  (∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
-                e' ∈ el' → to_val e' = None → reducible e' σ') →
-  fill K e ∈ el → head_step e σ κ e' σ' ef → head_reduce_not_to_stuck e' σ'.
-Proof.
-  intros Hsafe Hi Hstep κ1 e1 σ1 ? Hstep1 Hstuck.
-  cut (reducible (fill K e1) σ1).
-  { subst. intros (?&?&?&?&?). by eapply stuck_irreducible. }
-  destruct (elem_of_list_split _ _ Hi) as (?&?&->).
-  eapply Hsafe; last by (apply: fill_not_val; subst).
-  - eapply rtc_l, rtc_l, rtc_refl.
-    + eexists. econstructor. done. done. econstructor; done.
-    + eexists. econstructor. done. done. econstructor; done.
-  - subst. set_solver+.
-Qed.
-
-(* TODO: Unify this and the above. *)
-Lemma safe_not_reduce_to_stuck el σ K e :
-  (∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
-                e' ∈ el' → to_val e' = None → reducible e' σ') →
-  fill K e ∈ el → head_reduce_not_to_stuck e σ.
-Proof.
-  intros Hsafe Hi κ e1 σ1 ? Hstep1 Hstuck.
-  cut (reducible (fill K e1) σ1).
-  { subst. intros (?&?&?&?&?). by eapply stuck_irreducible. }
-  destruct (elem_of_list_split _ _ Hi) as (?&?&->).
-  eapply Hsafe; last by (apply: fill_not_val; subst).
-  - eapply rtc_l, rtc_refl.
-    + eexists. econstructor. done. done. econstructor; done.
-  - subst. set_solver+.
-Qed.
-
-Theorem safe_nonracing el σ :
-  (∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
-                e' ∈ el' → to_val e' = None → reducible e' σ') →
-  nonracing_threadpool el σ.
-Proof.
-  intros Hsafe l a1 a2 (t1&?&t2&?&t3&->&(K1&e1&Ha1&->)&(K2&e2&Ha2&->)).
-
-  assert (to_val e1 = None). by destruct Ha1.
-  assert (Hrede1:head_reducible e1 σ).
-  { eapply (next_access_head_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
-    abstract set_solver. }
-  assert (Hnse1:head_reduce_not_to_stuck e1 σ).
-  { eapply safe_not_reduce_to_stuck with (K:=K1); first done. set_solver+. }
-  assert (Hσe1:=next_access_head_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
-  destruct Hrede1 as (κ1'&e1'&σ1'&ef1&Hstep1). clear Hnse1.
-  assert (Ha1' : a1.2 = Na1Ord → next_access_head e1' σ1' (a1.1, Na2Ord) l).
-  { intros. eapply next_access_head_Na1Ord_step, Hstep1.
-    by destruct a1; simpl in *; subst. }
-  assert (Hrtc_step1:
-    rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
-        (t1 ++ fill K1 e1' :: t2 ++ fill K2 e2 :: t3 ++ ef1, σ1')).
-  { eapply rtc_l, rtc_refl. eexists. eapply step_atomic, Ectx_step, Hstep1; try  done.
-    by rewrite -assoc. }
-  assert (Hrede1: a1.2 = Na1Ord → head_reducible e1' σ1').
-  { destruct a1 as [a1 []]=>// _.
-    eapply (next_access_head_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
-           fill_not_val=>//.
-    by auto. abstract set_solver. by destruct Hstep1; inversion Ha1. }
-  assert (Hnse1: head_reduce_not_to_stuck e1' σ1').
-  { eapply safe_step_not_reduce_to_stuck with (K:=K1); first done; last done. set_solver+. }
-
-  assert (to_val e2 = None). by destruct Ha2.
-  assert (Hrede2:head_reducible e2 σ).
-  { eapply (next_access_head_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
-    abstract set_solver. }
-  assert (Hnse2:head_reduce_not_to_stuck e2 σ).
-  { eapply safe_not_reduce_to_stuck with (K:=K2); first done. set_solver+. }
-  assert (Hσe2:=next_access_head_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
-  destruct Hrede2 as (κ2'&e2'&σ2'&ef2&Hstep2).
-  assert (Ha2' : a2.2 = Na1Ord → next_access_head e2' σ2' (a2.1, Na2Ord) l).
-  { intros. eapply next_access_head_Na1Ord_step, Hstep2.
-    by destruct a2; simpl in *; subst. }
-  assert (Hrtc_step2:
-    rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
-        (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2' :: t3 ++ ef2, σ2')).
-  { eapply rtc_l, rtc_refl. rewrite app_comm_cons assoc. eexists.
-    eapply step_atomic, Ectx_step, Hstep2; try done. by rewrite -assoc. }
-  assert (Hrede2: a2.2 = Na1Ord → head_reducible e2' σ2').
-  { destruct a2 as [a2 []]=>// _.
-    eapply (next_access_head_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
-           fill_not_val=>//.
-    by auto. abstract set_solver. by destruct Hstep2; inversion Ha2. }
-  assert (Hnse2':head_reduce_not_to_stuck e2' σ2').
-  { eapply safe_step_not_reduce_to_stuck with (K:=K2); first done; last done. set_solver+. }
-
-  assert (Ha1'2 : a1.2 = Na1Ord → next_access_head e2 σ1' a2 l).
-  { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
-    by rewrite <-HNa, <-surjective_pairing. }
-  assert (Hrede1_2: head_reducible e2 σ1').
-  { intros. eapply (next_access_head_reductible_ctx e2 σ1' σ  a2 l K2), Hsafe, fill_not_val=>//.
-    abstract set_solver. }
-  assert (Hnse1_2:head_reduce_not_to_stuck e2 σ1').
-  { eapply safe_not_reduce_to_stuck with (K:=K2).
-    - intros. eapply Hsafe. etrans; last done. done. done. done.
-    - set_solver+. }
-  assert (Hσe1'1:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
-  assert (Hσe1'2:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
-
-  assert (Ha2'1 : a2.2 = Na1Ord → next_access_head e1 σ2' a1 l).
-  { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
-    by rewrite <-HNa, <-surjective_pairing. }
-  assert (Hrede2_1: head_reducible e1 σ2').
-  { intros. eapply (next_access_head_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
-    abstract set_solver. }
-  assert (Hnse2_1:head_reduce_not_to_stuck e1 σ2').
-  { eapply safe_not_reduce_to_stuck with (K:=K1).
-    - intros. eapply Hsafe. etrans; last done. done. done. done.
-    - set_solver+. }
-  assert (Hσe2'1:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
-  assert (Hσe2'2:=
-    λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord) Hnse2').
-
-  assert (a1.1 = FreeAcc → False).
-  { destruct a1 as [[]?]; inversion 1.
-    eauto using next_access_head_Free_concurent_step. }
-  assert (a2.1 = FreeAcc → False).
-  { destruct a2 as [[]?]; inversion 1.
-    eauto using next_access_head_Free_concurent_step. }
-
-  destruct Ha1 as [[]|[]| | |], Ha2 as [[]|[]| | |]=>//=; simpl in *;
-    repeat match goal with
-    | H : _ = Na1Ord → _ |- _ => specialize (H (eq_refl Na1Ord)) || clear H
-    | H : False |- _ => destruct H
-    | H : ∃ _, _ |- _ => destruct H
-    end;
-    try congruence.
-
-  clear κ2' e2' Hnse2' Hnse2_1 Hstep2 σ2' Hrtc_step2 Hrede2_1.
-  destruct Hrede1_2 as (κ2'&e2'&σ'&ef&?).
-  inv_head_step.
-  match goal with
-  | H : <[l:=_]> σ !! l = _ |- _ => by rewrite lookup_insert in H
-  end.
-Qed.
-
-Corollary adequate_nonracing e1 t2 σ1 σ2 φ :
-  adequate NotStuck e1 σ1 φ →
-  rtc erased_step ([e1], σ1) (t2, σ2) →
-  nonracing_threadpool t2 σ2.
-Proof.
-  intros [_ Had] Hrtc. apply safe_nonracing. intros el' σ' e' ?? He'.
-  edestruct (Had el' σ' e') as [He''|]; try done. etrans; eassumption.
-  rewrite /language.to_val /= He' in He''. by edestruct @is_Some_None.
-Qed.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
deleted file mode 100644
index 894acff4797614d663edf0f142fa7ff9cad3c43f..0000000000000000000000000000000000000000
--- a/theories/lang/tactics.v
+++ /dev/null
@@ -1,275 +0,0 @@
-From stdpp Require Import fin_maps.
-From lrust.lang Require Export lang.
-Set Default Proof Using "Type".
-
-(** We define an alternative representation of expressions in which the
-embedding of values and closed expressions is explicit. By reification of
-expressions into this type we can implement substitution, closedness
-checking, atomic checking, and conversion into values, by computation. *)
-Module W.
-Inductive expr :=
-| Val (v : val) (e : lang.expr) (H : to_val e = Some v)
-| ClosedExpr (e : lang.expr) `{!Closed [] e}
-| 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).
-
-Fixpoint to_expr (e : expr) : lang.expr :=
-  match e with
-  | Val v e' _ => e'
-  | ClosedExpr e => e
-  | Var x => lang.Var x
-  | Lit l => lang.Lit l
-  | Rec f xl e => lang.Rec f xl (to_expr e)
-  | BinOp op e1 e2 => lang.BinOp op (to_expr e1) (to_expr e2)
-  | App e el => lang.App (to_expr e) (map to_expr el)
-  | Read o e => lang.Read o (to_expr e)
-  | Write o e1 e2 => lang.Write o (to_expr e1) (to_expr e2)
-  | CAS e0 e1 e2 => lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
-  | Alloc e => lang.Alloc (to_expr e)
-  | Free e1 e2 => lang.Free (to_expr e1) (to_expr e2)
-  | Case e el => lang.Case (to_expr e) (map to_expr el)
-  | Fork e => lang.Fork (to_expr e)
-  end.
-
-Ltac of_expr e :=
-  lazymatch e with
-  | lang.Var ?x => constr:(Var x)
-  | lang.Lit ?l => constr:(Lit l)
-  | lang.Rec ?f ?xl ?e => let e := of_expr e in constr:(Rec f xl e)
-  | lang.BinOp ?op ?e1 ?e2 =>
-    let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
-  | lang.App ?e ?el =>
-    let e := of_expr e in let el := of_expr el in constr:(App e el)
-  | lang.Read ?o ?e => let e := of_expr e in constr:(Read o e)
-  | lang.Write ?o ?e1 ?e2 =>
-    let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Write o e1 e2)
-  | lang.CAS ?e0 ?e1 ?e2 =>
-     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
-     constr:(CAS e0 e1 e2)
-  | lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
-  | lang.Free ?e1 ?e2 =>
-    let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Free e1 e2)
-  | lang.Case ?e ?el =>
-     let e := of_expr e in let el := of_expr el in constr:(Case e el)
-  | lang.Fork ?e => let e := of_expr e in constr:(Fork e)
-  | @nil lang.expr => constr:(@nil expr)
-  | @cons lang.expr ?e ?el =>
-    let e := of_expr e in let el := of_expr el in constr:(e::el)
-  | to_expr ?e => e
-  | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
-  | _ => match goal with
-         | H : to_val e = Some ?v |- _ => constr:(Val v e H)
-         | H : Closed [] e |- _ => constr:(@ClosedExpr e H)
-         end
-  end.
-
-Fixpoint is_closed (X : list string) (e : expr) : bool :=
-  match e with
-  | Val _ _ _ | ClosedExpr _ => true
-  | 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.
-Lemma is_closed_correct X e : is_closed X e → lang.is_closed X (to_expr e).
-Proof.
-  revert e X. fix FIX 1; destruct e=>/=;
-    try naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
-  - induction el=>/=; naive_solver.
-  - induction el=>/=; naive_solver.
-Qed.
-
-(* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
-constructors are only generated for closed expressions of which we know nothing
-about apart from being closed. Notice that the reverse implication of
-[to_val_Some] thus does not hold. *)
-Definition to_val (e : expr) : option val :=
-  match e with
-  | Val v _ _ => Some v
-  | Rec f xl e =>
-    if decide (is_closed (f :b: xl +b+ []) e) is left H
-    then Some (@RecV f xl (to_expr e) (is_closed_correct _ _ H)) else None
-  | Lit l => Some (LitV l)
-  | _ => None
-  end.
-Lemma to_val_Some e v :
-  to_val e = Some v → of_val v = W.to_expr e.
-Proof.
-  revert v. induction e; intros; simplify_option_eq; auto using of_to_val.
-Qed.
-Lemma to_val_is_Some e :
-  is_Some (to_val e) → ∃ v, of_val v = to_expr e.
-Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
-Lemma to_val_is_Some' e :
-  is_Some (to_val e) → is_Some (lang.to_val (to_expr e)).
-Proof. intros [v ?]%to_val_is_Some. exists v. rewrite -to_of_val. by f_equal. Qed.
-
-Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
-  match e with
-  | Val v e H => Val v e H
-  | ClosedExpr e => ClosedExpr e
-  | 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.
-Lemma to_expr_subst x er e :
-  to_expr (subst x er e) = lang.subst x (to_expr er) (to_expr e).
-Proof.
-  revert e x er. fix FIX 1; destruct e=>/= ? er; repeat case_bool_decide;
-    f_equal; eauto using is_closed_nil_subst, is_closed_to_val, eq_sym.
-  - induction el=>//=. f_equal; auto.
-  - induction el=>//=. f_equal; auto.
-Qed.
-
-Definition is_atomic (e: expr) : bool :=
-  match e with
-  | Read (ScOrd | Na2Ord) e | Alloc e => bool_decide (is_Some (to_val e))
-  | Write (ScOrd | Na2Ord) e1 e2 | Free e1 e2 =>
-    bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
-  | CAS e0 e1 e2 =>
-    bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2))
-  | _ => false
-  end.
-Lemma is_atomic_correct e : is_atomic e → Atomic WeaklyAtomic (to_expr e).
-Proof.
-  intros He. apply ectx_language_atomic.
-  - intros σ e' σ' ef.
-    destruct e; simpl; try done; repeat (case_match; try done);
-    inversion 1; try (apply val_irreducible; rewrite ?language.to_of_val; naive_solver eauto); [].
-    rewrite -[stuck_term](fill_empty). apply stuck_irreducible.
-  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
-    revert He. destruct e; simpl; try done; repeat (case_match; try done);
-    rewrite ?bool_decide_spec;
-    destruct Ki; inversion Hfill; subst; clear Hfill;
-    try naive_solver eauto using to_val_is_Some'.
-Qed.
-End W.
-
-Ltac solve_closed :=
-  match goal with
-  | |- Closed ?X ?e =>
-     let e' := W.of_expr e in change (Closed X (W.to_expr e'));
-     apply W.is_closed_correct; vm_compute; exact I
-  end.
-Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
-
-Ltac solve_into_val :=
-  match goal with
-  | |- IntoVal ?e ?v =>
-     let e' := W.of_expr e in change (of_val v = W.to_expr e');
-     apply W.to_val_Some; simpl; unfold W.to_expr;
-     ((unlock; exact eq_refl) || (idtac; exact eq_refl))
-  end.
-Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
-
-Ltac solve_as_val :=
-  match goal with
-  | |- AsVal ?e =>
-     let e' := W.of_expr e in change (∃ v, of_val v = W.to_expr e');
-     apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
-  end.
-Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
-
-Ltac solve_atomic :=
-  match goal with
-  | |- Atomic ?s ?e =>
-     let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
-     apply W.is_atomic_correct; vm_compute; exact I
-  end.
-Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
-
-(** Substitution *)
-Ltac simpl_subst :=
-  unfold subst_v; simpl;
-  repeat match goal with
-  | |- context [subst ?x ?er ?e] =>
-      let er' := W.of_expr er in let e' := W.of_expr e in
-      change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
-      rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
-  end;
-  unfold W.to_expr; simpl.
-Arguments W.to_expr : simpl never.
-Arguments subst : simpl never.
-
-(** The tactic [inv_head_step] performs inversion on hypotheses of the
-shape [head_step]. The tactic will discharge head-reductions starting
-from values, and simplifies hypothesis related to conversions from and
-to values, and finite map operations. This tactic is slightly ad-hoc
-and tuned for proving our lifting lemmas. *)
-Ltac inv_head_step :=
-  repeat match goal with
-  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
-  | H : to_val _ = Some _ |- _ => apply of_to_val in H
-  | H : Lit _ = of_val ?v |- _ =>
-    apply (f_equal (to_val)) in H; rewrite to_of_val in H;
-    injection H; clear H; intro
-  | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
-  | H : head_step ?e _ _ _ _ _ |- _ =>
-     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
-     and can thus better be avoided. *)
-     inversion H; subst; clear H
-  end.
-
-(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
-evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
-for each possible decomposition until [tac] succeeds. *)
-Ltac reshape_val e tac :=
-  let rec go e :=
-  match e with
-  | of_val ?v => v
-  | Lit ?l => constr:(LitV l)
-  | Rec ?f ?xl ?e => constr:(RecV f xl e)
-  end in let v := go e in tac v.
-
-Ltac reshape_expr e tac :=
-  let rec go_fun K f vs es :=
-    match es with
-    | ?e :: ?es => reshape_val e ltac:(fun v => go_fun K f (v :: vs) es)
-    | ?e :: ?es => go (AppRCtx f (reverse vs) es :: K) e
-    end
-  with go K e :=
-  match e with
-  | _ => tac K e
-  | BinOp ?op ?e1 ?e2 =>
-     reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
-  | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
-  | App ?e ?el => reshape_val e ltac:(fun f => go_fun K f (@nil val) el)
-  | App ?e ?el => go (AppLCtx el :: K) e
-  | Read ?o ?e => go (ReadCtx o :: K) e
-  | Write ?o ?e1 ?e2 =>
-    reshape_val e1 ltac:(fun v1 => go (WriteRCtx o v1 :: K) e2)
-  | Write ?o ?e1 ?e2 => go (WriteLCtx o e2 :: K) e1
-  | CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
-     [ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
-     | go (CasMCtx v0 e2 :: K) e1 ])
-  | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
-  | Alloc ?e => go (AllocCtx :: K) e
-  | Free ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (FreeRCtx v1 :: K) e2)
-  | Free ?e1 ?e2 => go (FreeLCtx e2 :: K) e1
-  | Case ?e ?el => go (CaseCtx el :: K) e
-  end
-  in go (@nil ectx_item) e.