From e6c82af6f22fdc61914860b5e6a70ff4ef7b09a6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 30 Oct 2017 10:57:17 +0100
Subject: [PATCH] Add poison

---
 theories/lang/heap.v                       | 39 ++++++------
 theories/lang/lang.v                       | 73 +++++++++-------------
 theories/lang/lib/arc.v                    | 14 ++---
 theories/lang/lib/lock.v                   | 10 +--
 theories/lang/lib/memcpy.v                 |  4 +-
 theories/lang/lib/new_delete.v             | 14 ++---
 theories/lang/lib/spawn.v                  |  8 +--
 theories/lang/lib/swap.v                   |  4 +-
 theories/lang/lifting.v                    | 17 +++--
 theories/lang/notation.v                   |  2 +-
 theories/lang/proofmode.v                  | 20 +++---
 theories/typing/function.v                 |  6 +-
 theories/typing/lib/arc.v                  | 40 ++++++------
 theories/typing/lib/panic.v                |  4 +-
 theories/typing/lib/rc/rc.v                | 36 ++++++-----
 theories/typing/lib/refcell/ref_code.v     |  6 +-
 theories/typing/lib/refcell/refcell_code.v |  6 +-
 theories/typing/lib/refcell/refmut_code.v  |  4 +-
 theories/typing/own.v                      |  4 +-
 theories/typing/programs.v                 |  2 +-
 theories/typing/soundness.v                |  2 +-
 21 files changed, 152 insertions(+), 163 deletions(-)

diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 796a8557..d2bde800 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -297,19 +297,18 @@ Section heap.
     - rewrite is_Some_alt inter_lookup_None; lia.
   Qed.
 
-  Lemma heap_freeable_rel_init_mem l h vl σ:
-    vl ≠ [] →
+  Lemma heap_freeable_rel_init_mem l h n σ:
+    n ≠ O →
     (∀ m : Z, σ !! (l +ₗ m) = None) →
     heap_freeable_rel σ h →
-    heap_freeable_rel (init_mem l vl σ)
-                      (<[l.1 := (1%Qp, inter (l.2) (length vl))]> h).
+    heap_freeable_rel (init_mem l n σ)
+                      (<[l.1 := (1%Qp, inter (l.2) n)]> h).
   Proof.
     move=> Hvlnil FRESH REL blk qs /lookup_insert_Some [[<- <-]|[??]].
     - split.
-      { destruct vl as [|v vl]; simpl in *; [done|]. apply: insert_non_empty. }
-      intros i. destruct (decide (l.2 ≤ i ∧ i < l.2 + length vl)).
-      + rewrite inter_lookup_Some //.
-        destruct (lookup_init_mem_Some σ l (l.1, i) vl); naive_solver.
+      { destruct n as [|n]; simpl in *; [done|]. apply: insert_non_empty. }
+      intros i. destruct (decide (l.2 ≤ i ∧ i < l.2 + n)).
+      + rewrite inter_lookup_Some // lookup_init_mem; naive_solver.
       + rewrite inter_lookup_None; last lia. rewrite lookup_init_mem_ne /=; last lia.
         replace (l.1,i) with (l +â‚— (i - l.2)) by (rewrite /shift_loc; f_equal; lia).
         by rewrite FRESH !is_Some_alt.
@@ -337,15 +336,15 @@ Section heap.
   Qed.
 
   (** Weakest precondition *)
-  Lemma heap_alloc_vs σ l vl :
+  Lemma heap_alloc_vs σ l n :
     (∀ m : Z, σ !! (l +ₗ m) = None) →
     own heap_name (● to_heap σ)
-    ==∗ own heap_name (● to_heap (init_mem l vl σ))
-       ∗ own heap_name (◯ [^op list] i ↦ v ∈ vl,
+    ==∗ own heap_name (● to_heap (init_mem l n σ))
+       ∗ own heap_name (◯ [^op list] i ↦ v ∈ (repeat (LitV LitPoison) n),
            {[l +â‚— i := (1%Qp, Cinr 0%nat, to_agree v)]}).
   Proof.
     intros FREE. rewrite -own_op. apply own_update, auth_update_alloc.
-    revert l FREE. induction vl as [|v vl IH]=> l FRESH; [done|].
+    revert l FREE. induction n as [|n IH]=> l FRESH; [done|].
     rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=.
     etrans; first apply (IH (l +â‚— 1)).
     { intros. by rewrite shift_loc_assoc. }
@@ -357,16 +356,16 @@ Section heap.
     rewrite lookup_init_mem_ne /=; last lia. by rewrite -(shift_loc_0 l) FRESH.
   Qed.
 
-  Lemma heap_alloc σ l n vl :
+  Lemma heap_alloc σ l n :
     0 < n →
     (∀ m, σ !! (l +ₗ m) = None) →
-    Z.of_nat (length vl) = n →
     heap_ctx σ ==∗
-      heap_ctx (init_mem l vl σ) ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl.
+      heap_ctx (init_mem l (Z.to_nat n) σ) ∗ †l…(Z.to_nat n) ∗
+      l ↦∗ repeat (LitV LitPoison) (Z.to_nat n).
   Proof.
-    intros ?? HvlLen; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
-    assert (vl ≠ []) by (intros ->; simpl in *; lia).
-    iMod (heap_alloc_vs _ _ vl with "[$Hvalσ]") as "[Hvalσ Hmapsto]"; first done.
+    intros ??; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
+    assert (Z.to_nat n ≠ O). { rewrite -(Nat2Z.id 0)=>/Z2Nat.inj. lia. }
+    iMod (heap_alloc_vs _ _ (Z.to_nat n) with "[$Hvalσ]") as "[Hvalσ Hmapsto]"; first done.
     iMod (own_update _ (● hF) with "HhF") as "[HhF Hfreeable]".
     { apply auth_update_alloc,
         (alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
@@ -374,9 +373,9 @@ Section heap.
       - split. done. apply inter_valid. }
     iModIntro. iSplitL "Hvalσ HhF".
     { iExists _. iFrame. iPureIntro.
-      rewrite -HvlLen Nat2Z.id. auto using heap_freeable_rel_init_mem. }
+      auto using heap_freeable_rel_init_mem. }
     rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //.
-    iFrame.
+    iFrame. destruct (Z.to_nat n); done.
   Qed.
 
   Lemma heap_free_vs σ l vl :
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 0009314d..5deef297 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -14,7 +14,7 @@ Delimit Scope loc_scope with L.
 Open Scope loc_scope.
 
 Inductive base_lit : Set :=
-| LitUnit | LitLoc (l : loc) | LitInt (n : Z).
+| LitPoison | LitLoc (l : loc) | LitInt (n : Z).
 Inductive bin_op : Set :=
 | PlusOp | MinusOp | LeOp | EqOp | OffsetOp.
 Inductive order : Set :=
@@ -190,6 +190,8 @@ Proof.
 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.
 
@@ -201,10 +203,10 @@ 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) (init:list val) (σ:state) : state :=
-  match init with
-  | [] => σ
-  | inith :: initq => <[l:=(RSt 0, inith)]>(init_mem (l +ₗ 1) initq σ)
+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 :=
@@ -214,6 +216,7 @@ Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
   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
@@ -282,7 +285,7 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
     to_val e = Some v →
     σ !! l = Some (RSt 0, v') →
     head_step (Write ScOrd (Lit $ LitLoc l) e) σ
-              (Lit LitUnit) (<[l:=(RSt 0, v)]>σ)
+              (Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
               []
 | WriteNa1S l e v v' σ:
     to_val e = Some v →
@@ -294,7 +297,7 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
     to_val e = Some v →
     σ !! l = Some (WSt, v') →
     head_step (Write Na2Ord (Lit $ LitLoc l) e) σ
-              (Lit LitUnit) (<[l:=(RSt 0, v)]>σ)
+              (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 →
@@ -329,24 +332,23 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ
               stuck_term σ
               []
-| AllocS n l init σ :
+| AllocS n l σ :
     0 < n →
     (∀ m, σ !! (l +ₗ m) = None) →
-    Z.of_nat (length init) = n →
     head_step (Alloc $ Lit $ LitInt n) σ
-              (Lit $ LitLoc l) (init_mem l init σ) []
+              (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 LitUnit) (free_mem l (Z.to_nat n) σ)
+              (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 LitUnit) σ [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.
@@ -421,35 +423,23 @@ 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) vl :
-  l.1 = l'.1 → l.2 ≤ l'.2 < l.2 + length vl →
-  init_mem l vl σ !! l' = (RSt 0,) <$> vl !! Z.to_nat (l'.2 - l.2).
+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 [? n]; simplify_eq/=.
-  revert n l. induction vl as [|v vl IH]=> /= n l Hl; [lia|].
-  assert (n = l.2 ∨ l.2 + 1 ≤ n) as [->|?] by lia.
-  { by rewrite -surjective_pairing lookup_insert Z.sub_diag. }
+  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.
-  cut (Z.to_nat (n - l.2) = S (Z.to_nat (n - (l.2 + 1)))); [by intros ->|].
-  rewrite -Z2Nat.inj_succ; last lia. f_equal; lia.
-Qed.
-
-Lemma lookup_init_mem_Some σ (l l' : loc) vl :
-  l.1 = l'.1 → l.2 ≤ l'.2 < l.2 + length vl → ∃ v,
-  vl !! Z.to_nat (l'.2 - l.2) = Some v ∧
-  init_mem l vl σ !! l' = Some (RSt 0,v).
-Proof.
-  intros. destruct (lookup_lt_is_Some_2 vl (Z.to_nat (l'.2 - l.2))) as [v Hv].
-  { rewrite -(Nat2Z.id (length vl)). apply Z2Nat.inj_lt; lia. }
-  exists v. by rewrite lookup_init_mem ?Hv.
+  rewrite -(shift_loc_block l 1) IH /=; last lia. done.
 Qed.
 
-Lemma lookup_init_mem_ne σ (l l' : loc) vl :
-  l.1 ≠ l'.1 ∨ l'.2 < l.2 ∨ l.2 + length vl ≤ l'.2 →
-  init_mem l vl σ !! l' = σ !! l'.
+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 vl as [|v vl IH]=> /= l Hl; auto.
+  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.
@@ -472,11 +462,10 @@ 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 init σ) [].
+  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).
-  - rewrite repeat_length Z2Nat.id; lia.
 Qed.
 
 Lemma lookup_free_mem_ne σ l l' n : l.1 ≠ l'.1 → free_mem l n σ !! l' = σ !! l'.
@@ -622,8 +611,8 @@ Proof.
  refine (λ v1 v2, cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
 Defined.
 
-Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
-Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
+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.
@@ -657,8 +646,8 @@ Notation Seq e1 e2 := (Let BAnon e1 e2).
 Notation LamV xl e := (RecV BAnon xl e).
 Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
 Notation SeqCtx e2 := (LetCtx BAnon e2).
-Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
+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)))).
-Notation Newlft := (Lit LitUnit) (only parsing).
+Notation Newlft := (Lit LitPoison) (only parsing).
 Notation Endlft := Skip (only parsing).
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 38db542c..9755ee06 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -38,12 +38,12 @@ Definition weak_count : val :=
 Definition clone_arc : val :=
   rec: "clone" ["l"] :=
     let: "strong" := !ˢᶜ"l" in
-    if: CAS "l" "strong" ("strong" + #1) then #() else "clone" ["l"].
+    if: CAS "l" "strong" ("strong" + #1) then #☠ else "clone" ["l"].
 
 Definition clone_weak : val :=
   rec: "clone" ["l"] :=
     let: "weak" := !ˢᶜ("l" +ₗ #1) in
-    if: CAS ("l" +â‚— #1) "weak" ("weak" + #1) then #() else "clone" ["l"].
+    if: CAS ("l" +ₗ #1) "weak" ("weak" + #1) then #☠ else "clone" ["l"].
 
 Definition downgrade : val :=
   rec: "downgrade" ["l"] :=
@@ -52,7 +52,7 @@ Definition downgrade : val :=
       (* -1 in weak indicates that somebody locked the counts; let's spin. *)
       "downgrade" ["l"]
     else
-      if: CAS ("l" +â‚— #1) "weak" ("weak" + #1) then #()
+      if: CAS ("l" +ₗ #1) "weak" ("weak" + #1) then #☠
       else "downgrade" ["l"].
 
 Definition upgrade : val :=
@@ -151,7 +151,7 @@ Section def.
     (□ (P ={E,∅}=∗ weak_tok γ ∗ (weak_tok γ ={∅,E}=∗ P)))%I.
 
   Definition drop_spec (drop : val) P : iProp Σ :=
-    ({{{ P ∗ P1 1 }}} drop [] {{{ RET #(); P ∗ P2 }}})%I.
+    ({{{ P ∗ P1 1 }}} drop [] {{{ RET #☠; P ∗ P2 }}})%I.
 End def.
 
 Section arc.
@@ -255,7 +255,7 @@ Section arc.
   Lemma clone_arc_spec (γ : gname) (l : loc) (P : iProp Σ) :
     is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
     {{{ P }}} clone_arc [ #l]
-    {{{ q', RET #(); P ∗ arc_tok γ q' ∗ P1 q' }}}.
+    {{{ q', RET #☠; P ∗ arc_tok γ q' ∗ P1 q' }}}.
   Proof using HP1.
     iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_bind (!ˢᶜ_)%E.
     iInv N as (st) "[>H● H]" "Hclose1".
@@ -291,7 +291,7 @@ Section arc.
 
   Lemma downgrade_spec (γ : gname) (l : loc) (P : iProp Σ) :
     is_arc P1 P2 N γ l -∗ arc_tok_acc γ P (⊤ ∖ ↑N) -∗
-    {{{ P }}} downgrade [ #l] {{{ RET #(); P ∗ weak_tok γ }}}.
+    {{{ P }}} downgrade [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
   Proof.
     iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
     iInv N as (st) "[>H● H]" "Hclose1".
@@ -342,7 +342,7 @@ Section arc.
 
   Lemma clone_weak_spec (γ : gname) (l : loc) (P : iProp Σ) :
     is_arc P1 P2 N γ l -∗ weak_tok_acc γ P (⊤ ∖ ↑N) -∗
-    {{{ P }}} clone_weak [ #l] {{{ RET #(); P ∗ weak_tok γ }}}.
+    {{{ P }}} clone_weak [ #l] {{{ RET #☠; P ∗ weak_tok γ }}}.
   Proof.
     iIntros "#INV #Hacc !# * HP HΦ". iLöb as "IH". wp_rec. wp_op. wp_bind (!ˢᶜ_)%E.
     iAssert (□ (P ={⊤,⊤∖↑N}=∗ ∃ w : Z, (l +ₗ 1) ↦ #w ∗
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 3832cceb..0d50e7ce 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -8,7 +8,7 @@ Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
 Definition mklock_locked : val := λ: ["l"], "l" <- #true.
 Definition try_acquire : val := λ: ["l"], CAS "l" #false #true.
 Definition acquire : val :=
-  rec: "acquire" ["l"] := if: try_acquire ["l"] then #() else "acquire" ["l"].
+  rec: "acquire" ["l"] := if: try_acquire ["l"] then #☠ else "acquire" ["l"].
 Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
 
 (* It turns out that we need an accessor-based spec so that we can put the
@@ -53,7 +53,7 @@ Section proof.
   Qed.
 
   Lemma mklock_unlocked_spec (R : iProp Σ) (l : loc) v :
-    {{{ l ↦ v ∗ ▷ R }}} mklock_unlocked [ #l ] {{{ RET #(); ▷ lock_proto l R }}}.
+    {{{ l ↦ v ∗ ▷ R }}} mklock_unlocked [ #l ] {{{ RET #☠; ▷ lock_proto l R }}}.
   Proof.
     iIntros (Φ) "[Hl HR] HΦ". wp_lam. rewrite -wp_fupd. wp_write.
     iMod (lock_proto_create with "Hl HR") as "Hproto".
@@ -61,7 +61,7 @@ Section proof.
   Qed.
 
   Lemma mklock_locked_spec (R : iProp Σ) (l : loc) v :
-    {{{ l ↦ v }}} mklock_locked [ #l ] {{{ RET #(); ▷ lock_proto l R }}}.
+    {{{ l ↦ v }}} mklock_locked [ #l ] {{{ RET #☠; ▷ lock_proto l R }}}.
   Proof.
     iIntros (Φ) "Hl HΦ". wp_lam. rewrite -wp_fupd. wp_write.
     iMod (lock_proto_create with "Hl [//]") as "Hproto".
@@ -88,7 +88,7 @@ Section proof.
 
   Lemma acquire_spec E l R P :
     □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
-    {{{ P }}} acquire [ #l ] @ E {{{ RET #(); R ∗ P }}}.
+    {{{ P }}} acquire [ #l ] @ E {{{ RET #☠; R ∗ P }}}.
   Proof.
     iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
     wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
@@ -98,7 +98,7 @@ Section proof.
 
   Lemma release_spec E l R P :
     □ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
-    {{{ R ∗ P }}} release [ #l ] @ E {{{ RET #(); P }}}.
+    {{{ R ∗ P }}} release [ #l ] @ E {{{ RET #☠; P }}}.
   Proof.
     iIntros "#Hproto !# * (HR & HP) HΦ". wp_let.
     iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index ea0b9359..76a180b2 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 Definition memcpy : val :=
   rec: "memcpy" ["dst";"len";"src"] :=
-    if: "len" ≤ #0 then #()
+    if: "len" ≤ #0 then #☠
     else "dst" <- !"src";;
          "memcpy" ["dst" +â‚— #1 ; "len" - #1 ; "src" +â‚— #1].
 
@@ -24,7 +24,7 @@ Lemma wp_memcpy `{lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
   Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
     #l1 <-{n} !#l2 @ E
-  {{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
+  {{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
 Proof.
   iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
   iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 74da98af..48957caa 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -10,7 +10,7 @@ Definition new : val :=
 
 Definition delete : val :=
   λ: ["n"; "loc"],
-    if: "n" ≤ #0 then #()
+    if: "n" ≤ #0 then #☠
     else Free "n" "loc".
 
 Section specs.
@@ -19,21 +19,21 @@ Section specs.
   Lemma wp_new E n:
     0 ≤ n →
     {{{ True }}} new [ #n ] @ E
-    {{{ l vl, RET LitV $ LitLoc l;
-        ⌜n = length vl⌝ ∗ (†l…(Z.to_nat n) ∨ ⌜n = 0⌝) ∗ l ↦∗ vl }}}.
+    {{{ l, RET LitV $ LitLoc l;
+        (†l…(Z.to_nat n) ∨ ⌜n = 0⌝) ∗ l ↦∗ repeat (LitV LitPoison) (Z.to_nat n) }}}.
   Proof.
     iIntros (? Φ) "_ HΦ". wp_lam. wp_op; intros ?.
-    - wp_if. assert (n = 0) as -> by lia. iApply ("HΦ" $! _ []).
+    - wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
       rewrite heap_mapsto_vec_nil. auto.
-    - wp_if. wp_alloc l vl as "H↦" "H†". iApply ("HΦ" $! _ vl).
-      rewrite vec_to_list_length -{2}Hsz Z2Nat.id //. iFrame. auto.
+    - wp_if. wp_alloc l as "H↦" "H†". iApply "HΦ". subst sz.
+      iFrame. auto.
   Qed.
 
   Lemma wp_delete E (n:Z) l vl :
     n = length vl →
     {{{ l ↦∗ vl ∗ (†l…(length vl) ∨ ⌜n = 0⌝) }}}
       delete [ #n; #l] @ E
-    {{{ RET LitV LitUnit; True }}}.
+    {{{ RET #☠; True }}}.
   Proof.
     iIntros (? Φ) "(H↦ & [H†|%]) HΦ";
       wp_lam; wp_op; intros ?; try lia; wp_if; try wp_free; by iApply "HΦ".
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 96a930b5..4090a683 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -16,7 +16,7 @@ Definition finish : val :=
   λ: ["c"; "v"],
     "c" +â‚— #1 <- "v";; (* Store data (non-atomically). *)
     "c" <-ˢᶜ #1;; (* Signal that we finished (atomically!) *)
-    #().
+    #☠.
 Definition join : val :=
   rec: "join" ["c"] :=
     if: !ˢᶜ"c" then
@@ -67,11 +67,11 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
     spawn [e] {{{ c, RET #c; join_handle c Ψ }}}.
 Proof.
   iIntros (<-%of_to_val Φ) "Hf HΦ". rewrite /spawn /=.
-  wp_let. wp_alloc l vl as "Hl" "H†". wp_let. inv_vec vl=>v0 v1.
+  wp_let. wp_alloc l as "Hl" "H†". wp_let.
   iMod (own_alloc (Excl ())) as (γf) "Hγf"; first done.
   iMod (own_alloc (Excl ())) as (γj) "Hγj"; first done.
   rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
-  iDestruct "Hl" as "[Hc Hd]". wp_write. clear v0.
+  iDestruct "Hl" as "[Hc Hd]". wp_write.
   iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?".
   { iNext. iRight. iExists false. auto. }
   wp_apply (wp_fork with "[Hγf Hf Hd]").
@@ -81,7 +81,7 @@ Proof.
 Qed.
 
 Lemma finish_spec (Ψ : val → iProp Σ) c v :
-  {{{ finish_handle c Ψ ∗ Ψ v }}} finish [ #c; v] {{{ RET #(); True }}}.
+  {{{ finish_handle c Ψ ∗ Ψ v }}} finish [ #c; v] {{{ RET #☠; True }}}.
 Proof.
   iIntros (Φ) "[Hfin HΨ] HΦ". iDestruct "Hfin" as (γf γj v0) "(Hf & Hd & #?)".
   wp_lam. wp_op. wp_write.
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index 85724c08..1d3f46fb 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 Definition swap : val :=
   rec: "swap" ["p1";"p2";"len"] :=
-    if: "len" ≤ #0 then #()
+    if: "len" ≤ #0 then #☠
     else let: "x" := !"p1" in
          "p1" <- !"p2";;
          "p2" <- "x";;
@@ -15,7 +15,7 @@ Lemma wp_swap `{lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
   Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
     swap [ #l1; #l2; #n] @ E
-  {{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗ vl1 }}}.
+  {{{ RET #☠; l1 ↦∗ vl2 ∗ l2 ↦∗ vl1 }}}.
 Proof.
   iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
   iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index c8b7ad81..d5b2a32c 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -44,22 +44,21 @@ Proof. exact: weakestpre.wp_bind. Qed.
 Lemma wp_alloc E (n : Z) :
   0 < n →
   {{{ True }}} Alloc (Lit $ LitInt n) @ E
-  {{{ l sz (vl : vec val sz), RET LitV $ LitLoc l; ⌜n = sz⌝ ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
+  {{{ 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Φ" $! _ _ (list_to_vec init)).
-  rewrite vec_to_list_of_list. auto.
+  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 LitUnit; True }}}.
+  {{{ RET LitV LitPoison; True }}}.
 Proof.
   iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ".
@@ -101,7 +100,7 @@ Qed.
 Lemma wp_write_sc E l e v v' :
   to_val e = Some v →
   {{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
-  {{{ RET LitV LitUnit; l ↦ v }}}.
+  {{{ RET LitV LitPoison; l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
@@ -114,7 +113,7 @@ Qed.
 Lemma wp_write_na E l e v v' :
   to_val e = Some v →
   {{{ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
-  {{{ RET LitV LitUnit; l ↦ v }}}.
+  {{{ RET LitV LitPoison; l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) ">Hv HΦ".
   iApply wp_lift_head_step; auto. iIntros (σ1) "Hσ".
@@ -145,7 +144,7 @@ Proof.
 Qed.
 
 Lemma wp_cas_suc E l lit1 e2 lit2 :
-  to_val e2 = Some (LitV lit2) → lit1 ≠ LitUnit →
+  to_val e2 = Some (LitV lit2) → lit1 ≠ LitPoison →
   {{{ ▷ l ↦ LitV lit1 }}}
     CAS (Lit $ LitLoc l) (Lit lit1) e2 @ E
   {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
@@ -211,7 +210,7 @@ Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
 Lemma wp_fork E e :
-  {{{ â–· WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitUnit; True }}}.
+  {{{ â–· WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitPoison; True }}}.
 Proof.
   iIntros (?) "?HΦ". iApply wp_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto. iApply step_fupd_intro; first done. iNext.
@@ -446,7 +445,7 @@ Lemma wp_seq E e1 e2 v Φ :
   ▷ WP e2 @ E {{ Φ }} -∗ WP Seq e1 e2 @ E {{ Φ }}.
 Proof. iIntros (??) "?". by iApply (wp_let _ BAnon). Qed.
 
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ E {{ Φ }}.
+Lemma wp_skip E Φ : ▷ Φ (LitV LitPoison) -∗ WP Skip @ E {{ Φ }}.
 Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
 
 End lifting.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 260661a0..588a67be 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -29,7 +29,7 @@ Notation "'case:' e0 'of' el" := (Case e0%E el%E)
   (at level 102, e0, el at level 150) : expr_scope.
 Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
   (only parsing, at level 102, e1, e2, e3 at level 150) : expr_scope.
-Notation "()" := LitUnit : val_scope.
+Notation "☠" := LitPoison : val_scope.
 Notation "! e" := (Read Na1Ord e%E) (at level 9, format "! e") : expr_scope.
 Notation "!ˢᶜ e" := (Read ScOrd e%E) (at level 9, format "!ˢᶜ e") : expr_scope.
 Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 2a2afc16..b45f4217 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -154,8 +154,8 @@ Implicit Types Δ : envs (iResUR Σ).
 Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
   0 < n →
   IntoLaterNEnvs 1 Δ Δ' →
-  (∀ l sz (vl : vec val sz), n = sz → ∃ Δ'',
-    envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
+  (∀ l (sz: nat), n = sz → ∃ Δ'',
+    envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ repeat (LitV LitPoison) sz)) j2 (†l…sz)) Δ'
       = Some Δ'' ∧
     (Δ'' ⊢ Φ (LitV $ LitLoc l))) →
   Δ ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
@@ -163,9 +163,9 @@ Proof.
   intros ?? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
   rewrite -and_sep_l. apply and_intro; first done.
   rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
-  apply forall_intro=>sz. apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
+  apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc.
   apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
-  destruct (HΔ l _ vl) as (Δ''&?&HΔ'); first done.
+  destruct (HΔ l sz) as (Δ''&?&HΔ'); first done.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΔ' -fupd_intro.
 Qed.
 
@@ -177,7 +177,7 @@ Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
   envs_lookup i2 Δ'' = Some (false, †l…n')%I →
   envs_delete i2 false Δ'' = Δ''' →
   n' = length vl →
-  (Δ''' ⊢ Φ (LitV LitUnit)) →
+  (Δ''' ⊢ Φ (LitV LitPoison)) →
   Δ ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
   intros -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
@@ -209,7 +209,7 @@ Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  (Δ'' ⊢ Φ (LitV LitUnit)) →
+  (Δ'' ⊢ Φ (LitV LitPoison)) →
   Δ ⊢ WP Write o (Lit $ LitLoc l) e @ E {{ Φ }}.
 Proof.
   intros ? [->| ->] ????.
@@ -230,7 +230,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
   | _ => fail "wp_apply: not a 'wp'"
   end.
 
-Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
+Tactic Notation "wp_alloc" ident(l) "as" constr(H) constr(Hf) :=
   iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q =>
@@ -242,7 +242,7 @@ Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
       [try fast_done
       |apply _
       |let sz := fresh "sz" in let Hsz := fresh "Hsz" in
-       first [intros l sz vl Hsz | fail 1 "wp_alloc:" l "or" vl "not fresh"];
+       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;
@@ -257,8 +257,8 @@ Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
   | _ => fail "wp_alloc: not a 'wp'"
   end.
 
-Tactic Notation "wp_alloc" ident(l) ident(vl) :=
-  let H := iFresh in let Hf := iFresh in wp_alloc l vl as H Hf.
+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;
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 044c40b9..0fe49516 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -258,7 +258,7 @@ Section typing.
   Proof.
     iIntros (HE [k' Hk']) "#LFT #HE Htl HL Hκs Hf Hargs Hk". rewrite -(of_to_val k k') //.
     clear dependent k. wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
-    iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#() ;; #()) ;; k' ["_r"])%V⌝):::
+    iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#☠ ;; #☠) ;; k' ["_r"])%V⌝):::
                vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (fp x).(fp_tys))%I
             with "[Hargs]"); first wp_done.
     - rewrite /=. iSplitR "Hargs".
@@ -385,8 +385,8 @@ Section typing.
         intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
     - iIntros (k).
       (* TODO : make [simpl_subst] work here. *)
-      change (subst' "_k" k (p ((λ: ["_r"], (#() ;; #()) ;; "_k" ["_r"])%E :: ps))) with
-             ((subst "_k" k p) ((λ: ["_r"], (#() ;; #()) ;; k ["_r"])%E :: map (subst "_k" k) ps)).
+      change (subst' "_k" k (p ((λ: ["_r"], (#☠ ;; #☠) ;; "_k" ["_r"])%E :: ps))) with
+             ((subst "_k" k p) ((λ: ["_r"], (#☠ ;; #☠) ;; k ["_r"])%E :: map (subst "_k" k) ps)).
       rewrite is_closed_nil_subst //.
       assert (map (subst "_k" k) ps = ps) as ->.
       { clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 290ec5e9..502c96e2 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -738,8 +738,8 @@ Section arc.
          "r" <-{ty.(ty_size),Σ some} !("arc'" +ₗ #2);;
          if: drop_weak ["arc'"] then
            delete [ #(2 + ty.(ty_size)); "arc'" ]
-         else #()
-       else #());;
+         else #☠
+       else #☠);;
       delete [ #1; "arc"];; return: ["r"].
 
   Lemma arc_drop_type ty `{!TyWf ty} :
@@ -800,7 +800,7 @@ Section arc.
       let: "r" := new [ #0] in
       let: "arc'" := !"arc" in
       (if: drop_weak ["arc'"] then delete [ #(2 + ty.(ty_size)); "arc'" ]
-       else #());;
+       else #☠);;
       delete [ #1; "arc"];; return: ["r"].
 
   Lemma weak_drop_type ty `{!TyWf ty} :
@@ -840,7 +840,7 @@ Section arc.
         "r" <-{ty.(ty_size),Σ 0} !("arc'" +ₗ #2);;
         (* Decrement the "strong weak reference" *)
         (if: drop_weak ["arc'"] then delete [ #(2 + ty.(ty_size)); "arc'" ]
-         else #());;
+         else #☠);;
         delete [ #1; "arc"];; return: ["r"]
       else
         "r" <-{Σ 1} "arc'";;
@@ -1009,8 +1009,8 @@ Section arc.
     typed_val clone (fn(∀ α, ∅; &shr{α}ty) → ty) →
     typed_val (arc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α}(arc ty)) → &uniq{α} ty).
   Proof.
-    intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-    iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+    intros Hclone E L. iApply type_fn; [solve_typing..|]. rewrite [(2 + ty_size ty)%nat]lock.
+    iIntros "/= !#". iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
@@ -1044,19 +1044,19 @@ Section arc.
       iApply type_jump; solve_typing.
     - iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _). 
       iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
-      wp_apply wp_new=>//. iIntros (l vl) "(Hlen & H† & Hlvl) (#Hν & Hown & H†') !>".
-      iDestruct "Hlen" as %Hlen. destruct vl as [|?[|]]; simpl in Hlen; try lia.
+      wp_apply wp_new=>//. lia. iIntros (l) "(H† & Hlvl) (#Hν & Hown & H†') !>".
+      rewrite -!lock Nat2Z.id.
       wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
       iDestruct "Hlvl" as "(Hrc0 & Hrc1 & Hrc2)". wp_write. wp_op. wp_write.
       wp_op. wp_op. iDestruct "Hown" as (vl) "[H↦ Hown]".
-      iDestruct (ty_size_eq with "Hown") as %Hlen'.
-      wp_apply (wp_memcpy with "[$Hrc2 $H↦]"); [lia..|].
+      iDestruct (ty_size_eq with "Hown") as %Hsz.
+      wp_apply (wp_memcpy with "[$Hrc2 $H↦]").
+      { by rewrite repeat_length. } { by rewrite Hsz. }
       iIntros "[H↦ H↦']". wp_seq. wp_write.
       iMod ("Hclose2" $! ((l +ₗ 2) ↦∗: ty_own ty tid)%I
         with "[Hrc'↦ Hrc0 Hrc1 H†] [H↦ Hown]") as "[Hb Hα1]"; [|by auto with iFrame|].
       { iIntros "!> H↦". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
-        iLeft. iFrame. iDestruct "H†" as "[?|%]"=>//.
-        by rewrite /Z.to_nat Pos2Nat.inj_succ SuccNat2Pos.id_succ. }
+        iLeft. iFrame. iDestruct "H†" as "[?|%]"=>//. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
       iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); (#l +ₗ #2) ◁ &uniq{α}ty;
                                 r ◁ box (uninit 1) ]
@@ -1067,7 +1067,7 @@ Section arc.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
     - iIntros "[Htok Hν]". wp_case. wp_apply wp_new=>//.
-      iIntros (l [|?[]]) "/= (% & H† & Hl)"; try lia. wp_let. wp_op.
+      iIntros (l) "/= (H† & Hl)". wp_let. wp_op.
       rewrite heap_mapsto_vec_singleton. wp_write. wp_let.
       wp_bind (of_val clone).
       iApply (wp_wand with "[Hna]").
@@ -1083,22 +1083,22 @@ Section arc.
         iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
       iIntros ([[|cl|]|]) "Hna Hαν Hcl //". wp_rec.
       iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
-      iDestruct (ty_size_eq with "Hown") as "#%".
+      iDestruct (ty_size_eq with "Hown") as %Hsz.
       iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
-      wp_apply wp_new=>//. iIntros (l' vl') "(% & Hl'† & Hl')". wp_let. wp_op.
-      rewrite shift_loc_0. destruct vl' as [|?[|??]]; simpl in *; try lia.
+      wp_apply wp_new=>//. lia. iIntros (l') "(Hl'† & Hl')". wp_let. wp_op.
+      rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
       rewrite !heap_mapsto_vec_cons shift_loc_assoc.
       iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
-      wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]"); [lia..|]. iIntros "[Hl'2 Hcl↦]".
-      wp_seq. rewrite freeable_sz_full.
+      wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]").
+      { by rewrite repeat_length. } { by rewrite Hsz. }
+      iIntros "[Hl'2 Hcl↦]". wp_seq. rewrite freeable_sz_full.
       wp_apply (wp_delete with "[$Hcl↦ Hcl†]");
         [lia|by replace (length vl) with (ty.(ty_size))|].
       iIntros "_". wp_seq. wp_write.
       iMod ("Hclose2" $! ((l' +ₗ 2) ↦∗: ty_own ty tid)%I with
           "[Hrc'↦ Hl' Hl'1  Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
       { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
-        iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//.
-        by rewrite /Z.to_nat Pos2Nat.inj_succ SuccNat2Pos.id_succ. }
+        iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//. }
       { iExists _.  iFrame. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
       iApply (type_type _ _ _ [ #rc ◁ arc ty; #l' +ₗ #2 ◁ &uniq{α}ty;
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 5ba70deb..865e9a90 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -14,7 +14,7 @@ Section panic.
   Context `{typeG Σ}.
 
   Definition panic : val :=
-    funrec: <> [] := #().
+    funrec: <> [] := #☠.
 
   Lemma panic_type : typed_val panic (fn(∅) → emp).
   Proof.
@@ -22,4 +22,4 @@ Section panic.
     inv_vec args.  iIntros (tid) "LFT HE Hna HL Hk HT /=". simpl_subst.
     wp_value. done.
   Qed.
-End panic.
\ No newline at end of file
+End panic.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index be11f559..ff86be07 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -693,7 +693,7 @@ Section code.
     iIntros (strong) "[Hrc Hc]". wp_let.
     iDestruct "Hc" as "[[% [_ Hproto]]|[% [Hproto _]]]".
     - subst strong. wp_op=>[_|?]; last done. wp_if. wp_op.
-      rewrite shift_loc_0. wp_write. wp_bind (#();;#())%E.
+      rewrite shift_loc_0. wp_write. wp_bind (#☠;;#☠)%E.
       iApply (wp_step_fupd with "[Hproto Hrc]");
         [| |by iApply ("Hproto" with "Hrc")|];
         [done..|wp_seq; iIntros "(Hty&H†&Hna&Hproto) !>"].
@@ -990,8 +990,9 @@ Section code.
     typed_val clone (fn(∀ α, ∅; &shr{α}ty) → ty) →
     typed_val (rc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α}(rc ty)) → &uniq{α}ty).
   Proof.
-    intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
+    intros Hclone E L. iApply type_fn; [solve_typing..|].
+    rewrite [(2 + ty_size ty)%nat]lock.
+    iIntros "/= !#".  iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α}ty)]));
@@ -1033,17 +1034,20 @@ Section code.
       + wp_op; [lia|move=>_]. wp_if. wp_op. rewrite shift_loc_0. wp_write. wp_op.
         wp_op. wp_write. wp_bind (new _). iSpecialize ("Hrc" with "Hl1 Hl2").
         iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; first lia. done.
-        iNext. iIntros (lr [|? [|??]]) "/= (% & [H†|%] & H↦lr) [Hty Hproto] !>"; try lia.
+        rewrite -!lock Nat2Z.id.
+        iNext. iIntros (lr) "/= ([H†|%] & H↦lr) [Hty Hproto] !>"; last lia.
         rewrite 2!heap_mapsto_vec_cons. iDestruct "H↦lr" as "(Hlr1 & Hlr2 & Hlr3)".
         wp_let. wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_op. wp_op.
         iDestruct "Hty" as (vlr) "[H↦vlr Hty]". rewrite shift_loc_assoc.
-        iDestruct (ty_size_eq with "Hty") as %?.
-        wp_apply (wp_memcpy with "[$Hlr3 $H↦vlr]"); [lia..|]. iIntros "[Hlr3 Hvlr]".
-        wp_seq. wp_write. wp_op. iMod ("Hproto" with "[Hvlr]") as "Hna"; first by eauto.
+        iDestruct (ty_size_eq with "Hty") as %Hsz.
+        wp_apply (wp_memcpy with "[$Hlr3 $H↦vlr]").
+        { by rewrite repeat_length. } { by rewrite Hsz. }
+        iIntros "[Hlr3 Hvlr]". wp_seq. wp_write. wp_op.
+        iMod ("Hproto" with "[Hvlr]") as "Hna"; first by eauto.
         iMod ("Hclose2" $! ((lr +ₗ 2) ↦∗: ty_own ty tid)%I
               with "[Hrc' Hlr1 Hlr2 H†] [Hlr3 Hty]") as "[Hb Hα1]".
         { iIntros "!> H !>". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
-          iLeft. iFrame. rewrite Z2Nat.inj_pos Pos2Nat.inj_succ SuccNat2Pos.id_succ //. }
+          iLeft. iFrame. }
         { iExists _. iFrame. }
         iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
         iApply (type_type _ _ _ [ r ◁ box (uninit 1); #(lr +ₗ 2) ◁ &uniq{α}ty;
@@ -1054,7 +1058,7 @@ Section code.
         iApply type_assign; [solve_typing..|].
         iApply type_jump; solve_typing.
     - wp_apply wp_new; first lia. done.
-      iIntros (lr [|? [|??]]) "/= (% & [H†|%] & H↦lr)"; try lia.
+      iIntros (lr) "/= ([H†|%] & H↦lr)"; last lia.
       iDestruct "Hc" as "[[% ?]|[% [Hproto _]]]"; first lia.
       iMod ("Hproto" with "Hl1") as "[Hna Hty]". wp_let. wp_op.
       rewrite heap_mapsto_vec_singleton. wp_write.
@@ -1086,22 +1090,22 @@ Section code.
         iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
       iIntros ([[|cl|]|]) "Hna Hαν Hcl //". wp_rec.
       iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
-      iDestruct (ty_size_eq with "Hown") as "#%".
+      iDestruct (ty_size_eq with "Hown") as %Hsz.
       iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
-      wp_apply wp_new=>//. iIntros (l' vl') "(% & Hl'† & Hl')". wp_let. wp_op.
-      rewrite shift_loc_0. destruct vl' as [|?[|??]]; simpl in *; try lia.
+      wp_apply wp_new=>//. lia. iIntros (l') "(Hl'† & Hl')". wp_let. wp_op.
+      rewrite shift_loc_0. rewrite -!lock Nat2Z.id.
       rewrite !heap_mapsto_vec_cons shift_loc_assoc.
       iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
-      wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]"); [lia..|]. iIntros "[Hl'2 Hcl↦]".
-      wp_seq. rewrite freeable_sz_full.
+      wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]").
+      { by rewrite repeat_length. } { by rewrite Hsz. }
+      iIntros "[Hl'2 Hcl↦]". wp_seq. rewrite freeable_sz_full.
       wp_apply (wp_delete with "[$Hcl↦ Hcl†]");
         [lia|by replace (length vl) with (ty.(ty_size))|].
       iIntros "_". wp_seq. wp_write.
       iMod ("Hclose2" $! ((l' +ₗ 2) ↦∗: ty_own ty tid)%I with
           "[Hrc' Hl' Hl'1  Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
       { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
-        iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//.
-        by rewrite /Z.to_nat Pos2Nat.inj_succ SuccNat2Pos.id_succ. }
+        iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//. }
       { iExists _.  iFrame. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
       iApply (type_type _ _ _ [ #l ◁ rc ty; #l' +ₗ #2 ◁ &uniq{α}ty;
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 7b3e4d5d..5bdb0f01 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -86,7 +86,7 @@ Section ref_functions.
       - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
         apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
         apply Qcplus_le_mono_r, Qp_ge_0. }
-    wp_apply wp_new; [done..|]. iIntros (lr ?) "(%&?&Hlr)".
+    wp_apply wp_new; [done..|]. iIntros (lr) "(?&Hlr)".
     iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I  with "[H↦1 H↦2]" as "H↦".
     { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
     wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
@@ -231,8 +231,8 @@ Section ref_functions.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; try done.
-    iIntros (lx [|? []]) "(% & H† & Hlx)"; try (simpl in *; lia).
-    rewrite heap_mapsto_vec_singleton. wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
+    iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
+    wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
     iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
     iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 9f1f4b40..1c06d34d 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -169,8 +169,7 @@ Section refcell_functions.
       iApply (type_sum_unit (option $ ref α ty)); [solve_typing..|]; first last.
       simpl. iApply type_jump; solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
-      iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
-      destruct vl as [|?[|?[]]]; try done. wp_let.
+      iIntros (lref) "(H† & Hlref)". wp_let.
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
       iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
@@ -267,8 +266,7 @@ Section refcell_functions.
     iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose'')"; try done.
     iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op=>?; wp_if.
     - wp_write. wp_apply wp_new; [done..|].
-      iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
-      destruct vl as [|?[|?[]]]; try done. wp_let.
+      iIntros (lref) "(H† & Hlref)". wp_let.
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
       destruct st as [[?[|[]|]]|]; try done.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 0e270dd3..13fa187b 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -177,8 +177,8 @@ Section refmut_functions.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; first done. done.
-    iIntros (lx [|? []]) "(% & H† & Hlx)"; try (simpl in *; lia).
-    rewrite heap_mapsto_vec_singleton. wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
+    iIntros (lx) "(H† & Hlx)". rewrite heap_mapsto_vec_singleton.
+    wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
     iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
     iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index d8111cdc..f022a478 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -252,9 +252,9 @@ Section typing.
   Proof.
     iIntros (? tid) "#LFT #HE $ $ _".
     iApply wp_new; try done. iModIntro.
-    iIntros (l vl) "(% & H† & Hlft)". subst. rewrite tctx_interp_singleton tctx_hasty_val.
+    iIntros (l) "(H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
     iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
-    iExists vl. iFrame. by rewrite Nat2Z.id.
+    iExists (repeat #☠ (Z.to_nat n)). iFrame. by rewrite /= repeat_length. 
   Qed.
 
   Lemma type_new {E L C T} (n' : nat) x (n : Z) e :
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 6b102838..54469b36 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -247,7 +247,7 @@ Section typing_rules.
     {{{ lft_ctx ∗ elctx_interp E ∗ na_own tid ⊤ ∗ llctx_interp L qL ∗
         tctx_elt_interp tid (p1 ◁ ty1) ∗ tctx_elt_interp tid (p2 ◁ ty2) }}}
       (p1 <-{n} !p2)
-    {{{ RET #(); na_own tid ⊤ ∗ llctx_interp L qL ∗
+    {{{ RET #☠; na_own tid ⊤ ∗ llctx_interp L qL ∗
                  tctx_elt_interp tid (p1 ◁ ty1') ∗ tctx_elt_interp tid (p2 ◁ ty2') }}}.
   Proof.
     iIntros (<-) "#Hwrt #Hread !#".
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index b716b63c..b88d1123 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -21,7 +21,7 @@ Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
 Proof. solve_inG. Qed.
 
 Section type_soundness.
-  Definition exit_cont : val := λ: [<>], #().
+  Definition exit_cont : val := λ: [<>], #☠.
 
   Definition main_type `{typeG Σ} := (fn(∅) → unit)%T.
 
-- 
GitLab