diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
new file mode 100644
index 0000000000000000000000000000000000000000..7ea33f076ef2ee264da84a6ba65ac5c20660720a
--- /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/lang.v b/theories/lang/lang.v
new file mode 100644
index 0000000000000000000000000000000000000000..cd64baa245f76e4c1fa06e997840c6e782820f2b
--- /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/lifting.v b/theories/lang/lifting.v
new file mode 100644
index 0000000000000000000000000000000000000000..29f273d482227154f448f785e93e1f29e68f8d91
--- /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 omega.
+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
new file mode 100644
index 0000000000000000000000000000000000000000..4abc2eaadd41f86ed351926f10afce2540d5252c
--- /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/races.v b/theories/lang/races.v
new file mode 100644
index 0000000000000000000000000000000000000000..1423c77f6f34c3e92693a79d0a1ce2d134f9845d
--- /dev/null
+++ b/theories/lang/races.v
@@ -0,0 +1,299 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..894acff4797614d663edf0f142fa7ff9cad3c43f
--- /dev/null
+++ b/theories/lang/tactics.v
@@ -0,0 +1,275 @@
+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.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index bfd979a1e2ba6575036bd6a299524aa316cec003..e10721eccb7b1c40157817e869b2f1b5dbc1f251 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -67,4 +67,6 @@ Theorem type_soundness_closed (main : val) σ t :
   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 𝓥) σ).
-Proof. intros. eapply @type_soundness; try done. apply _. Qed.
+Proof.
+  intros. eapply @type_soundness; try done. apply _.
+Qed.