diff --git a/theories/caesium/heap.v b/theories/caesium/heap.v
index 5ce0d5187ea36ca02fee4679ee498d6d2021ed63..fd0acab6c3cd592be6b2269a3c695ba5ef5cbec0 100644
--- a/theories/caesium/heap.v
+++ b/theories/caesium/heap.v
@@ -423,6 +423,7 @@ Fixpoint mem_cast (v : val) (ot : op_type) (st : (gset addr * heap_state)) : val
       (* The following reimplements integer to pointer casts as described in the VIP paper. *)
       v' ← val_to_bytes v;
       a ← val_to_Z v' usize_t;
+      (* Technically, this clause is redundant since val_to_loc already converts 0 to NULL. *)
       if bool_decide (a = 0) then
         Some (val_of_loc (ProvNull, a))
       else if bool_decide (a ∈ st.1) then
diff --git a/theories/caesium/lifting.v b/theories/caesium/lifting.v
index 46843995518f12d564c3d5891ba2eb4291635384..a7f5591f56afb68a343990cceba463a421c4bfae 100644
--- a/theories/caesium/lifting.v
+++ b/theories/caesium/lifting.v
@@ -1729,11 +1729,18 @@ Qed.
 Lemma wp_get_member_union `{!LayoutAlg} Φ vl l ul uls n E:
   use_union_layout_alg uls = Some ul →
   val_to_loc vl = Some l →
-  Φ (val_of_loc (l at_union{ul}ₗ n)) -∗ WP Val vl at_union{uls} n @ E {{ Φ }}.
-Proof.
-  iIntros (Halg ->%val_of_to_loc) "?".
-  rewrite /GetMemberUnion/GetMemberUnionLoc.
-  by iApply @wp_value.
+ (* Technically, we only need vl ≠ NULL_bytes here, but we use
+  the loc_in_bounds precondition for uniformity with wp_get_member *)
+  loc_in_bounds l 0 (ly_size ul) -∗
+  Φ (val_of_loc (l at_union{ul}ₗ n)) -∗
+  WP Val vl at_union{uls} n @ E {{ Φ }}.
+Proof.
+  iIntros (Halg [|[??]]%val_of_to_loc) "Hlib HΦ"; subst.
+  2: {
+    iDestruct (loc_in_bounds_is_alloc with "Hlib") as %[[?[=]] | (? & ? & ?)].
+    rewrite /GetMemberUnion/GetMemberUnionLoc. by iApply @wp_value.
+  }
+  rewrite /GetMemberUnion/GetMemberUnionLoc. by iApply @wp_value.
 Qed.
 
 (* TODO: lemmas for accessing discriminant/data of enum *)
@@ -2288,12 +2295,9 @@ Proof.
   iModIntro. iSplit; first by eauto 10 using FreeS, val_to_of_loc.
   iNext. iIntros (???? Hstep ?) "Hcred". inv_stmt_step. iModIntro.
   iSplitR; first done.
-  match goal with
-  | H : val_to_loc _ = Some ?l |- _ => apply val_of_to_loc in H; injection H; intros <-; intros
-  end.
-  rewrite (free_block_inj σ.(st_heap) l (Layout n_size n_align) HeapAlloc hs' σ'); [ | done..].
-  iFrame.
-  by iApply ("HWP" with "Hcred").
+  revert select (val_to_loc _ = Some _) => /val_of_to_loc[/(inj _ _ _)Heq|[??]//]. subst.
+  erewrite (free_block_inj σ.(st_heap) _ (Layout n_size n_align) HeapAlloc hs' σ'); [ | done..].
+  iFrame. by iApply ("HWP" with "Hcred").
 Qed.
 
 Lemma wps_skip_credits Q Ψ s n m:
diff --git a/theories/caesium/notation.v b/theories/caesium/notation.v
index e95d8d0b6e404a39c693f836a1d6d34baa0a37c8..7298f5b616fbee38e17a23943397c31a99f3b003 100644
--- a/theories/caesium/notation.v
+++ b/theories/caesium/notation.v
@@ -66,6 +66,8 @@ Notation "e1 'sub_ptr{' ly , ot1 , ot2 } e2" := (BinOp (PtrDiffOp ly) ot2 ot1 e1
   (at level 70, format "e1  sub_ptr{ ly ,  ot1 ,  ot2 }  e2") : expr_scope.
 Notation "'if{' ot ',' join '}' ':' e1 'then' s1 'else' s2" := (IfS ot join e1%E s1%E s2%E)
   (at level 102, e1, s1, s2 at level 150, format "'[v' 'if{' ot ','  join '}' ':'  e1  'then' '/  ' s1 '/' 'else' '/  ' s2 ']'") : expr_scope.
+Notation "'if{' ot '}' ':' e1 'then' s1 'else' s2" := (IfS ot None e1%E s1%E s2%E)
+  (at level 102, e1, s1, s2 at level 150, format "'[v' 'if{' ot '}' ':'  e1  'then' '/  ' s1 '/' 'else' '/  ' s2 ']'") : expr_scope.
 Notation "'expr:' e ; s" := (ExprS e%E s%E)
   (at level 80, s at level 200, format "'[v' 'expr:'  e ';' '/' s ']'") : expr_scope.
 
diff --git a/theories/caesium/val.v b/theories/caesium/val.v
index 55f19b5e23769b4fab9f5df6847f0369f06cee92..96c3b5b1c8d0ea143c42946280bd3a6ec9329290 100644
--- a/theories/caesium/val.v
+++ b/theories/caesium/val.v
@@ -43,9 +43,19 @@ Definition val_of_loc_n (n : nat) (l : loc) : val :=
 Definition val_of_loc : loc → val :=
   val_of_loc_n bytes_per_addr.
 
+(* [NULL_bytes(_n)] is the alternative representation of NULL as integer 0 bytes. *)
+Definition NULL_bytes_n (n : nat) : val := repeat (MByte byte0 None) n.
+Definition NULL_bytes := NULL_bytes_n bytes_per_addr.
+
 Definition val_to_loc_n (n : nat) (v : val) : option loc :=
   if v is MPtrFrag l _ :: _ then
     if (bool_decide (v = val_of_loc_n n l)) then Some l else None
+  (* A list of 0s is interpreted as NULL. This is mainly useful when
+  memcasting is turned off. Interpreting 0s as NULL does not cause the
+  steps for pointers to overlap with the steps for integers since the
+  steps are dispatched based on the op_type, not on val_to_loc. *)
+  else if v is MByte b _ :: _ then
+    if (bool_decide (v = NULL_bytes_n n)) then Some NULL_loc else None
   else None.
 
 Definition val_to_loc : val → option loc :=
@@ -76,32 +86,30 @@ Proof.
 Qed.
 
 Lemma val_of_to_loc_n n v l:
-  val_to_loc_n n v = Some l → v = val_of_loc_n n l.
+  val_to_loc_n n v = Some l → v = val_of_loc_n n l ∨ v = NULL_bytes_n n ∧ l = NULL_loc.
 Proof.
   rewrite /val_to_loc_n.
-  destruct v as [|b v'] eqn:Hv; first done. repeat case_match => //.
-  revert select (_ = _) => /bool_decide_eq_true -> ?. by simplify_eq.
+  destruct v as [|b v'] eqn:Hv; first done.
+  repeat case_match => //; case_bool_decide; naive_solver.
 Qed.
 
 Lemma val_of_to_loc v l:
-  val_to_loc v = Some l → v = val_of_loc l.
-Proof.
-  by move => /val_of_to_loc_n ->.
-Qed.
+  val_to_loc v = Some l → v = val_of_loc l ∨ v = NULL_bytes ∧ l = NULL_loc.
+Proof. apply val_of_to_loc_n. Qed.
 
 Lemma val_to_loc_n_length n v:
   is_Some (val_to_loc_n n v) → length v = n.
 Proof.
   rewrite /val_to_loc_n. move => [? H]. repeat case_match => //; simplify_eq.
-  revert select (bool_decide _ = _) => /bool_decide_eq_true ->.
-  by rewrite val_of_loc_n_length.
+  - revert select (bool_decide _ = _) => /bool_decide_eq_true ->.
+    rewrite /NULL_bytes_n. by rewrite repeat_length.
+  - revert select (bool_decide _ = _) => /bool_decide_eq_true ->.
+    by rewrite val_of_loc_n_length.
 Qed.
 
 Lemma val_to_loc_length v:
   is_Some (val_to_loc v) → length v = bytes_per_addr.
-Proof.
-  apply val_to_loc_n_length.
-Qed.
+Proof. apply val_to_loc_n_length. Qed.
 
 Global Instance val_of_loc_inj : Inj (=) (=) val_of_loc.
 Proof. move => x y Heq. have := val_to_of_loc x. have := val_to_of_loc y. rewrite Heq. by simplify_eq. Qed.
@@ -309,11 +317,15 @@ Proof.
     by case_bool_decide.
 Qed.
 
-Lemma val_to_loc_to_Z_disjoint v l it z:
+Lemma val_to_Z_val_of_loc_None l it:
+  val_to_Z (val_of_loc l) it = None.
+Proof. apply val_to_Z_val_of_loc_n_None. Qed.
+
+Lemma val_to_loc_to_Z_overlap v l it z:
   val_to_loc v = Some l →
   val_to_Z v it = Some z →
-  False.
-Proof. destruct v => //=. rewrite /val_to_loc/val_to_Z/=. destruct m => // _. by case_bool_decide. Qed.
+  v = NULL_bytes.
+Proof. move => /val_of_to_loc[->|[-> ?//]]. by rewrite val_to_Z_val_of_loc_None. Qed.
 
 Lemma val_of_Z_bool_is_Some p it b:
   is_Some (val_of_Z (bool_to_Z b) it p).
diff --git a/theories/rust_typing/program_rules.v b/theories/rust_typing/program_rules.v
index b5176e755a257de4362952d1b3e44f4edae65033..081b26f229fad410d115cc7eb316f5e48950ee63 100644
--- a/theories/rust_typing/program_rules.v
+++ b/theories/rust_typing/program_rules.v
@@ -3012,10 +3012,10 @@ Section typing.
     iApply wps_assert_bool; [done.. | ]. iIntros "!> Hcred". by iApply ("Hs" with "CTX HE HL").
   Qed.
 
-  Lemma type_if E L π e s1 s2 fn R ϝ:
+  Lemma type_if E L π e s1 s2 fn R join ϝ :
     typed_val_expr π E L e (λ L' v rt ty r, typed_if E L' v (v ◁ᵥ{π} r @ ty)
           (typed_stmt π E L' s1 fn R ϝ) (typed_stmt π E L' s2 fn R ϝ))
-    ⊢ typed_stmt π E L (if{BoolOp}: e then s1 else s2) fn R ϝ.
+    ⊢ typed_stmt π E L (if{BoolOp, join}: e then s1 else s2) fn R ϝ.
   Proof.
     iIntros "He #CTX #HE HL". wps_bind.
     iApply ("He" with "CTX HE HL"). iIntros (L' v rt ty r) "HL Hv Hs".