diff --git a/theories/typing/constrained.v b/theories/typing/constrained.v
index 7be3d2bc8c8ce050f25523b75e7d7b8a40fdda68..2c66d4e198ad0ade141186ab0ef2ac2fc022caeb 100644
--- a/theories/typing/constrained.v
+++ b/theories/typing/constrained.v
@@ -34,8 +34,8 @@ Section own_constrained.
   Next Obligation. iIntros (?????) "[? $]". by iApply ty_deref. Qed.
   Next Obligation. iIntros (???????) "Hl [? $]". by iApply (ty_ref with "[//] [Hl]"). Qed.
 
-  Global Instance own_constrained_loc_in_bounds ty β P `{!OwnConstraint P} `{!LocInBounds ty β} :
-    LocInBounds (own_constrained P ty) β.
+  Global Instance own_constrained_loc_in_bounds ty β n P `{!OwnConstraint P} `{!LocInBounds ty β n} :
+    LocInBounds (own_constrained P ty) β n.
   Proof.
     constructor. iIntros (l) "[Hl _]". by iApply loc_in_bounds_in_bounds.
   Qed.
diff --git a/theories/typing/exist.v b/theories/typing/exist.v
index 0a206acc7efda3dc851a50240692f6f1839335e1..510e67cd54dd77021f041a4328a33d988abf171c 100644
--- a/theories/typing/exist.v
+++ b/theories/typing/exist.v
@@ -42,8 +42,8 @@ Section tyexist.
   Next Obligation. iIntros (ty ? ? x l v). rewrite tyexists_eq. by apply ty_ref. Qed.
   Next Obligation. move => ?? H x1 x2 /=. move: (H x1 x2). by inversion 1. Qed.
 
-  Global Instance tyexists_loc_in_bounds ty β `{!∀ x, LocInBounds (ty x) β} :
-    LocInBounds (tyexists ty) β.
+  Global Instance tyexists_loc_in_bounds ty β n `{!∀ x, LocInBounds (ty x) β n} :
+    LocInBounds (tyexists ty) β n.
   Proof.
     constructor. iIntros (l) "Hl". iDestruct "Hl" as (x) "Hl".
     rewrite tyexists_eq. by iApply loc_in_bounds_in_bounds.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index c951bdb3a40c03c78048a64069f5d6f2809faee4..e49c9dd6c699e24ea7da3d2111419fe09e81ef15 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -39,7 +39,7 @@ Section int.
     by iApply heap_mapsto_own_state_loc_in_bounds.
   Qed.
 
-  Global Instance loc_in_bounds_int n it β: LocInBounds (n @ int it) β.
+  Global Instance loc_in_bounds_int n it β: LocInBounds (n @ int it) β (bytes_per_int it).
   Proof.
     constructor. iIntros (l) "Hl".
     iDestruct (int_loc_in_bounds with "Hl") as "Hlib".
diff --git a/theories/typing/optional.v b/theories/typing/optional.v
index 861f6b57e23a314eeb01e37c940614fdb05e6320..110f29731092344dfdd844c58a0c47b3e41eb563 100644
--- a/theories/typing/optional.v
+++ b/theories/typing/optional.v
@@ -92,6 +92,13 @@ Section optional.
   Qed.
   Next Obligation. done. Qed.
 
+  Global Instance optional_loc_in_bounds ty e ot β n `{!LocInBounds ty β n} `{!LocInBounds ot β n}:
+    LocInBounds (e @ optional ty ot) β n.
+  Proof.
+    constructor. rewrite /with_refinement /=. iIntros (l) "Hl".
+    iDestruct "Hl" as "[[_ Hl]|[_ Hl]]"; by iApply (loc_in_bounds_in_bounds with "Hl").
+  Qed.
+
   (* We could add rules like *)
   (* Lemma simplify_optional_goal ty optty l β T b `{!Decision b}: *)
   (*   T (if decide b then l◁ₗ{β}ty else l◁ₗ{β}optty) -∗ *)
@@ -283,8 +290,8 @@ Section optionalO.
   Qed.
   Next Obligation. done. Qed.
 
-  Global Instance optionalO_loc_in_bounds A (ty : A → type) e ot β `{!∀ x, LocInBounds (ty x) β} `{!LocInBounds ot β}:
-    LocInBounds (e @ optionalO ty ot) β.
+  Global Instance optionalO_loc_in_bounds A (ty : A → type) e ot β n `{!∀ x, LocInBounds (ty x) β n} `{!LocInBounds ot β n}:
+    LocInBounds (e @ optionalO ty ot) β n.
   Proof.
     constructor. iIntros (l) "Hl". rewrite /with_refinement /=.
     destruct e; by iApply (loc_in_bounds_in_bounds with "Hl").
diff --git a/theories/typing/own.v b/theories/typing/own.v
index b06f0d91318db074572feeef784c1db40481095c..10a0bf5d9a70f9cdbf300b5b1d6273a17c872b1b 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -37,11 +37,11 @@ Section own.
   Next Obligation. iIntros (β ty l l' v ?) "Hl [-> Hl']". iFrame. iSplit => //. by rewrite left_id. Qed.
   Next Obligation. done. Qed.
 
-  Global Instance frac_ptr_loc_in_bounds l ty β1 β2 : LocInBounds (l @ frac_ptr β1 ty) β2.
+  Global Instance frac_ptr_loc_in_bounds l ty β1 β2 : LocInBounds (l @ frac_ptr β1 ty) β2 bytes_per_addr.
   Proof.
     constructor. iIntros (?) "(_&Hl&_)".
     iDestruct (heap_mapsto_own_state_loc_in_bounds with "Hl") as "Hb".
-    iApply loc_in_bounds_shorten; last done. lia.
+    iApply loc_in_bounds_shorten; last done. by rewrite /val_of_loc.
   Qed.
 
   Lemma frac_ptr_mono ty1 ty2 l β β' p p' T:
@@ -196,21 +196,22 @@ Section own.
     λ T, i2p (type_place_cast_ptr_ptr K l ty β T).
 
   (* Allow direct casts to other integer types. *)
-  Lemma type_cast_ptr_int (p : loc) β ty T:
-    ((p ◁ₗ{β} ty -∗ loc_in_bounds p 0 ∗ True) ∧ (p ◁ₗ{β} ty -∗ T (i2v p.2 size_t) (t2mt (p.2 @ int size_t)))) -∗
+  Lemma type_cast_ptr_int (p : loc) β ty n `{!LocInBounds ty β n} T:
+    (⌜min_alloc_start ≤ p.2 ∧ p.2 + n ≤ max_alloc_end⌝ -∗
+      p ◁ₗ{β} ty -∗ T (i2v p.2 size_t) (t2mt (p.2 @ int uintptr_t))) -∗
     typed_un_op p (p ◁ₗ{β} ty) (CastOp (IntOp uintptr_t)) PtrOp T.
   Proof.
     iIntros "HT Hp" (Φ) "HΦ".
-    iAssert (⌜p.2 ∈ size_t⌝)%I as %[? Heq]%val_of_int_is_some.
-    { iDestruct "HT" as "[HT _]". iDestruct ("HT" with "Hp") as "[Hlib _]".
-      by iApply loc_in_bounds_in_range_uintptr_t. }
-    iDestruct "HT" as "[_ HT]". rewrite /i2v Heq.
+    iDestruct (loc_in_bounds_in_bounds with "Hp") as "#Hlib".
+    iDestruct (loc_in_bounds_in_range_uintptr_t with "Hlib") as %[? H]%val_of_int_is_some.
+    iDestruct (loc_in_bounds_ptr_in_range with "Hlib") as %?.
+    iDestruct ("HT" with "[] Hp") as "HT"; first done.
     iApply wp_cast_ptr_int => //=; first by rewrite val_to_of_loc.
-    iApply ("HΦ" with "[] [HT Hp]"); last by iApply "HT". done.
+    rewrite /i2v H /=. iApply ("HΦ" with "[] [HT]"); last done. done.
   Qed.
-  Global Instance type_cast_ptr_int_inst (p : loc) β ty:
+  Global Instance type_cast_ptr_int_inst (p : loc) β ty n `{!LocInBounds ty β n}:
     TypedUnOp p (p ◁ₗ{β} ty)%I (CastOp (IntOp uintptr_t)) PtrOp :=
-    λ T, i2p (type_cast_ptr_int p β ty T).
+    λ T, i2p (type_cast_ptr_int p β ty n T).
 
   Lemma type_cast_int_ptr n v it T:
     (⌜n ∈ it⌝ -∗ T (val_of_loc (None, n)) (t2mt ((None, n) @ frac_ptr Own (place (None, n))))) -∗
@@ -331,11 +332,11 @@ Section ptr.
   Next Obligation. iIntros (l l' v ?) "Hl ->". by iFrame. Qed.
   Next Obligation. done. Qed.
 
-  Instance ptr_loc_in_bounds l β : LocInBounds (l @ ptr) β.
+  Instance ptr_loc_in_bounds l β : LocInBounds (l @ ptr) β bytes_per_addr.
   Proof.
     constructor. iIntros (?) "[_ Hl]".
     iDestruct (heap_mapsto_own_state_loc_in_bounds with "Hl") as "Hb".
-    iApply loc_in_bounds_shorten; last done. lia.
+    iApply loc_in_bounds_shorten; last done. by rewrite /val_of_loc.
   Qed.
 
   (* TODO: Think about this. This instance is probably not a good idea
@@ -431,11 +432,11 @@ Section null.
   Next Obligation. iIntros (?) "[% ?]". iExists _. by iFrame. Qed.
   Next Obligation. iIntros (???) "? ->". by iFrame. Qed.
 
-  Global Instance null_loc_in_bounds β : LocInBounds null β.
+  Global Instance null_loc_in_bounds β : LocInBounds null β bytes_per_addr.
   Proof.
     constructor. iIntros (l) "[_ Hl]".
     iDestruct (heap_mapsto_own_state_loc_in_bounds with "Hl") as "Hb".
-    iApply loc_in_bounds_shorten; last done. lia.
+    by iApply loc_in_bounds_shorten.
   Qed.
 
   Lemma type_null T :
@@ -487,23 +488,24 @@ Section null.
     TypedBinOp v1 (v1 ◁ᵥ null) v2 (v2 ◁ᵥ null) op PtrOp PtrOp :=
     λ T, i2p (type_binop_null_null v1 v2 op T).
 
-  Lemma type_binop_ptr_null v2 op T (l : loc) ty β `{!LocInBounds ty β}:
+  Lemma type_binop_ptr_null v2 op T (l : loc) ty β n `{!LocInBounds ty β n}:
     (⌜match op with | EqOp | NeOp => True | _ => False end⌝ ∗ ∀ v, l ◁ₗ{β} ty -∗
           T v (t2mt ((if op is EqOp then false else true) @ boolean i32))) -∗
     typed_bin_op l (l ◁ₗ{β} ty) v2 (v2 ◁ᵥ null) op PtrOp PtrOp T.
   Proof.
     iIntros "[% HT] Hl" (-> Φ) "HΦ".
     iDestruct (loc_in_bounds_in_bounds with "Hl") as "#Hb".
+    iDestruct (loc_in_bounds_shorten _ _ 0 with "Hb") as "#Hb0"; first by lia.
     iApply (wp_binop_det (i2v (Z_of_bool (if op is EqOp then false else true)) i32)). iSplit.
     { iIntros (??) "Hctx".
-      iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hb Hctx") as %?.
+      iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hb0 Hctx") as %?.
       iPureIntro. destruct op => //; split => Heq; subst; try by [inversion Heq].
       all: econstructor; rewrite ?val_to_of_loc /val_of_bool/i2v//. }
     iApply "HΦ". 2: by iApply "HT". by destruct op.
   Qed.
-  Global Instance type_binop_ptr_null_inst v2 op (l : loc) ty β `{!LocInBounds ty β}:
+  Global Instance type_binop_ptr_null_inst v2 op (l : loc) ty β n `{!LocInBounds ty β n}:
     TypedBinOp l (l ◁ₗ{β} ty) v2 (v2 ◁ᵥ null) op PtrOp PtrOp :=
-    λ T, i2p (type_binop_ptr_null v2 op T l ty β).
+    λ T, i2p (type_binop_ptr_null v2 op T l ty β n).
 
 End null.
 
diff --git a/theories/typing/padded.v b/theories/typing/padded.v
index 6b1710bb9e66ae0e74e8cfab59a567173c044d4a..6736cfb4e3ea58a6825ec90c4536c90d1b2187be 100644
--- a/theories/typing/padded.v
+++ b/theories/typing/padded.v
@@ -54,9 +54,9 @@ Section padded.
     rewrite app_length Heq1 Heq2 /ly_size /= -!/(ly_size _). lia.
   Qed.
 
-  Global Instance loc_in_bounds_padded ty lyty ly β: LocInBounds (padded ty lyty ly) β.
+  Global Instance loc_in_bounds_padded ty lyty ly β: LocInBounds (padded ty lyty ly) β (ly_size ly).
   Proof.
-    constructor. iIntros (l) "(_&_&H&_)". iApply loc_in_bounds_shorten; last done. lia.
+    constructor. by iIntros (l) "(_&_&H&_)".
   Qed.
 
   Lemma simpl_padded_hyp_eq_layout l β ty ly T:
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 249f5d4166adf86e5280c5793451ed131c307802..ecc454ddfaf2e6af677bbedc3119ed34ab703dce 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -437,16 +437,18 @@ Section typing.
 
   Global Instance related_to_loc_in_bounds l n : RelatedTo (loc_in_bounds l n) := {| rt_fic := FindLoc l |}.
 
-  Lemma subsume_loc_in_bounds ty β l `{!LocInBounds ty β} T :
-    (l ◁ₗ{β} ty -∗ T) -∗
-    subsume (l ◁ₗ{β} ty) (loc_in_bounds l 0) T.
+  Lemma subsume_loc_in_bounds ty β l (n m : nat) `{!LocInBounds ty β m} T :
+    (l ◁ₗ{β} ty -∗ ⌜n ≤ m⌝ ∗ T) -∗
+    subsume (l ◁ₗ{β} ty) (loc_in_bounds l n) T.
   Proof.
-    iIntros "HT Hl". iSplit; last by iApply "HT".
-    by iApply loc_in_bounds_in_bounds.
+    iIntros "HT Hl".
+    iAssert ⌜n ≤ m⌝%I as %?. { by iDestruct ("HT" with "Hl") as "[% _]". }
+    iSplit; last by iDestruct ("HT" with "Hl") as "[_ $]".
+    iApply loc_in_bounds_shorten; last by iApply loc_in_bounds_in_bounds. lia.
   Qed.
-  Global Instance subsume_loc_in_bounds_inst ty β l `{!LocInBounds ty β} :
-    Subsume (l ◁ₗ{β} ty) (loc_in_bounds l 0) :=
-    λ T, i2p (subsume_loc_in_bounds ty β l T).
+  Global Instance subsume_loc_in_bounds_inst ty β l n m `{!LocInBounds ty β m} :
+    Subsume (l ◁ₗ{β} ty) (loc_in_bounds l n) :=
+    λ T, i2p (subsume_loc_in_bounds ty β l n m T).
 
   Lemma apply_subsume_place_true l1 β1 ty1 l2 β2 ty2:
     l1 ◁ₗ{β1} ty1 -∗
diff --git a/theories/typing/struct.v b/theories/typing/struct.v
index d2a577e23a85d7c2b3dbb498c31ca531fad69640..a991569cd1004cdccac2e37eeea31b65ce5f3275 100644
--- a/theories/typing/struct.v
+++ b/theories/typing/struct.v
@@ -156,10 +156,9 @@ Section struct.
       all: rewrite drop_app_alt ?take_length// Hv; cbn; lia.
   Qed.
 
-  Global Instance struct_loc_in_bounds sl tys β : LocInBounds (struct sl tys) β.
+  Global Instance struct_loc_in_bounds sl tys β : LocInBounds (struct sl tys) β (ly_size sl).
   Proof.
-    constructor. iIntros (l) "(_&_&?&_)".
-    iApply loc_in_bounds_shorten; last done. lia.
+    constructor. by iIntros (l) "(_&_&?&_)".
   Qed.
 
   Global Instance strip_guarded_struct sl tys tys' E1 E2 β {Hs :StripGuardedLst β E1 E2 tys tys'}:
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 8e97021bbb4843fd4e01da1b516809feae70ed3a..48d39e4b414879ef8e21d0604971d8f394d2691f 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -302,19 +302,27 @@ Class Copyable `{!typeG Σ} (ty : type) `{!Movable ty} := {
 }.
 Existing Instance copy_own_persistent.
 
-Class LocInBounds `{!typeG Σ} (ty : type) (β : own_state) := {
-  loc_in_bounds_in_bounds l : ty.(ty_own) β l -∗ loc_in_bounds l 0
+Class LocInBounds `{!typeG Σ} (ty : type) (β : own_state) (n : nat) := {
+  loc_in_bounds_in_bounds l : ty.(ty_own) β l -∗ loc_in_bounds l n
 }.
+Arguments loc_in_bounds_in_bounds {_ _} _ _ _ {_} _.
+Hint Mode LocInBounds + + + + - : typeclass_instances.
 
 Section loc_in_bounds.
   Context `{!typeG Σ}.
 
   Lemma movable_loc_in_bounds ty l `{!Movable ty} :
-    ty_own ty Own l -∗ loc_in_bounds l (ly_size (ty_layout ty)).
+    ty.(ty_own) Own l -∗ loc_in_bounds l (ly_size (ty_layout ty)).
   Proof.
     iIntros "Hl". iDestruct (ty_deref with "Hl") as (v) "[Hl Hv]".
     iDestruct (ty_size_eq with "Hv") as %<-. by iApply heap_mapsto_loc_in_bounds.
   Qed.
+
+  Global Instance movable_loc_in_bounds_inst ty `{!Movable ty}:
+    LocInBounds ty Own (ly_size (ty_layout ty)).
+  Proof.
+    constructor. iIntros (?) "?". by iApply movable_loc_in_bounds.
+  Qed.
 End loc_in_bounds.
 
 Notation "l ◁ₗ{ β } ty" := (ty_own ty β l) (at level 15, format "l  ◁ₗ{ β }  ty") : bi_scope.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 4c2c30175f14b64930e7a4f2a06f7a5481006bc3..f84ba9ea9117ed2218a0d1c39bb09c8782360131 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -31,11 +31,10 @@ Section uninit.
     by iApply heap_mapsto_own_state_loc_in_bounds.
   Qed.
 
-  Global Instance loc_in_bounds_uninit ly β: LocInBounds (uninit ly) β.
+  Global Instance loc_in_bounds_uninit ly β: LocInBounds (uninit ly) β (ly_size ly).
   Proof.
     constructor. iIntros (l) "Hl".
-    iDestruct (uninit_loc_in_bounds with "Hl") as "#Hb".
-    iApply loc_in_bounds_shorten; last done. lia.
+    by iDestruct (uninit_loc_in_bounds with "Hl") as "#Hb".
   Qed.
 
   (* This only works for own because of ty might have interior mutability. *)
diff --git a/theories/typing/wand.v b/theories/typing/wand.v
index 78fa49af1d2e5105d6a6c2f752c63726314b9b09..2c7c8e6e496f4dd65d0b4c2b2cf40f7bf9937be2 100644
--- a/theories/typing/wand.v
+++ b/theories/typing/wand.v
@@ -92,13 +92,12 @@ Section wand_val.
   Next Obligation. iIntros (?????) "Hl". iDestruct "Hl" as (v) "(?&?&?&?)". eauto with iFrame. Qed.
   Next Obligation. iIntros (????? v) "??[??]". iExists v. iFrame. Qed.
 
-  Global Instance wand_val_loc_in_bounds P ly (ty : A → type)
-         `{!∀ x, Movable (ty x)} `{!∀ x, LocInBounds (ty x) β}:
-    LocInBounds (wand_val_ex ly P ty) β.
+  Global Instance wand_val_loc_in_bounds P ly (ty : A → type) `{!∀ x, Movable (ty x)}:
+    LocInBounds (wand_val_ex ly P ty) β (ly_size ly).
   Proof.
-    constructor. iIntros (l) "Hl". iDestruct "Hl" as (?) "(_&_&Hl&_)".
+    constructor. iIntros (l) "Hl". iDestruct "Hl" as (?) "(_&Hly&Hl&_)".
     iDestruct (heap_mapsto_own_state_loc_in_bounds with "Hl") as "H".
-    iApply (loc_in_bounds_shorten with "H"). lia.
+    by iDestruct "Hly" as %->.
   Qed.
 
   Lemma subsume_wand_val v ly1 ly2 P1 P2 ty1 ty2 T `{!∀ x, Movable (ty1 x)} `{!∀ x, Movable (ty2 x)}:
diff --git a/theories/typing/zeroed.v b/theories/typing/zeroed.v
index a25f4b5685cee5ba6b75edc6129ccf3377929816..7b8dcad78a5a09c6158764e7454e22c4fb924ef5 100644
--- a/theories/typing/zeroed.v
+++ b/theories/typing/zeroed.v
@@ -26,7 +26,7 @@ Section zeroed.
     by rewrite replicate_length.
   Qed.
 
-  Global Instance loc_in_bounds_zeroed ly β: LocInBounds (zeroed ly) β.
+  Global Instance loc_in_bounds_zeroed ly β: LocInBounds (zeroed ly) β (ly_size ly).
   Proof.
     constructor. iIntros (l) "Hl".
     iDestruct (zeroed_loc_in_bounds with "Hl") as "#Hb".