require alloc alive on pointer to integer cast

examples/proofs/tagged_ptr/generated_code.v

@@ -14,86 +14,86 @@ Section code.
   Definition loc_7 : location_info := LocationInfo file_0 20 27 20 35.
   Definition loc_8 : location_info := LocationInfo file_0 20 28 20 29.
   Definition loc_9 : location_info := LocationInfo file_0 20 33 20 34.
-  Definition loc_12 : location_info := LocationInfo file_0 28 2 28 26.
-  Definition loc_13 : location_info := LocationInfo file_0 29 2 29 139.
-  Definition loc_14 : location_info := LocationInfo file_0 29 9 29 138.
-  Definition loc_15 : location_info := LocationInfo file_0 29 35 29 38.
-  Definition loc_16 : location_info := LocationInfo file_0 29 35 29 38.
-  Definition loc_17 : location_info := LocationInfo file_0 29 40 29 77.
-  Definition loc_18 : location_info := LocationInfo file_0 29 49 29 76.
-  Definition loc_19 : location_info := LocationInfo file_0 29 50 29 71.
-  Definition loc_20 : location_info := LocationInfo file_0 29 50 29 63.
-  Definition loc_21 : location_info := LocationInfo file_0 29 62 29 63.
-  Definition loc_22 : location_info := LocationInfo file_0 29 62 29 63.
-  Definition loc_23 : location_info := LocationInfo file_0 29 66 29 71.
-  Definition loc_24 : location_info := LocationInfo file_0 29 66 29 71.
-  Definition loc_25 : location_info := LocationInfo file_0 29 74 29 75.
-  Definition loc_26 : location_info := LocationInfo file_0 29 74 29 75.
-  Definition loc_27 : location_info := LocationInfo file_0 28 16 28 25.
-  Definition loc_28 : location_info := LocationInfo file_0 28 16 28 22.
-  Definition loc_29 : location_info := LocationInfo file_0 28 16 28 22.
-  Definition loc_30 : location_info := LocationInfo file_0 28 23 28 24.
-  Definition loc_31 : location_info := LocationInfo file_0 28 23 28 24.
-  Definition loc_36 : location_info := LocationInfo file_0 37 2 37 30.
-  Definition loc_37 : location_info := LocationInfo file_0 38 2 38 121.
-  Definition loc_38 : location_info := LocationInfo file_0 38 9 38 120.
-  Definition loc_39 : location_info := LocationInfo file_0 38 35 38 38.
-  Definition loc_40 : location_info := LocationInfo file_0 38 35 38 38.
-  Definition loc_41 : location_info := LocationInfo file_0 38 40 38 68.
-  Definition loc_42 : location_info := LocationInfo file_0 38 49 38 67.
-  Definition loc_43 : location_info := LocationInfo file_0 38 50 38 51.
-  Definition loc_44 : location_info := LocationInfo file_0 38 50 38 51.
-  Definition loc_45 : location_info := LocationInfo file_0 38 54 38 66.
-  Definition loc_46 : location_info := LocationInfo file_0 38 54 38 55.
-  Definition loc_47 : location_info := LocationInfo file_0 38 54 38 55.
-  Definition loc_48 : location_info := LocationInfo file_0 38 58 38 66.
-  Definition loc_49 : location_info := LocationInfo file_0 38 59 38 60.
-  Definition loc_50 : location_info := LocationInfo file_0 38 64 38 65.
-  Definition loc_51 : location_info := LocationInfo file_0 37 16 37 29.
-  Definition loc_52 : location_info := LocationInfo file_0 37 28 37 29.
-  Definition loc_53 : location_info := LocationInfo file_0 37 28 37 29.
-  Definition loc_58 : location_info := LocationInfo file_0 43 2 43 15.
-  Definition loc_59 : location_info := LocationInfo file_0 45 2 45 24.
-  Definition loc_60 : location_info := LocationInfo file_0 46 2 46 26.
-  Definition loc_61 : location_info := LocationInfo file_0 48 2 48 36.
-  Definition loc_62 : location_info := LocationInfo file_0 49 2 49 13.
-  Definition loc_63 : location_info := LocationInfo file_0 49 9 49 12.
-  Definition loc_64 : location_info := LocationInfo file_0 49 9 49 12.
-  Definition loc_65 : location_info := LocationInfo file_0 49 10 49 12.
-  Definition loc_66 : location_info := LocationInfo file_0 49 10 49 12.
-  Definition loc_67 : location_info := LocationInfo file_0 48 15 48 35.
-  Definition loc_68 : location_info := LocationInfo file_0 48 26 48 35.
-  Definition loc_69 : location_info := LocationInfo file_0 48 26 48 31.
-  Definition loc_70 : location_info := LocationInfo file_0 48 26 48 31.
-  Definition loc_71 : location_info := LocationInfo file_0 48 32 48 34.
-  Definition loc_72 : location_info := LocationInfo file_0 48 32 48 34.
-  Definition loc_75 : location_info := LocationInfo file_0 46 9 46 24.
-  Definition loc_76 : location_info := LocationInfo file_0 46 9 46 19.
-  Definition loc_77 : location_info := LocationInfo file_0 46 9 46 15.
-  Definition loc_78 : location_info := LocationInfo file_0 46 9 46 15.
-  Definition loc_79 : location_info := LocationInfo file_0 46 16 46 18.
-  Definition loc_80 : location_info := LocationInfo file_0 46 16 46 18.
-  Definition loc_81 : location_info := LocationInfo file_0 46 23 46 24.
-  Definition loc_82 : location_info := LocationInfo file_0 45 13 45 23.
-  Definition loc_83 : location_info := LocationInfo file_0 45 13 45 16.
-  Definition loc_84 : location_info := LocationInfo file_0 45 13 45 16.
-  Definition loc_85 : location_info := LocationInfo file_0 45 17 45 19.
-  Definition loc_86 : location_info := LocationInfo file_0 45 18 45 19.
-  Definition loc_87 : location_info := LocationInfo file_0 45 21 45 22.
-  Definition loc_90 : location_info := LocationInfo file_0 43 13 43 14.
-  Definition loc_95 : location_info := LocationInfo file_0 58 2 58 30.
-  Definition loc_96 : location_info := LocationInfo file_0 59 2 59 27.
-  Definition loc_97 : location_info := LocationInfo file_0 59 9 59 26.
-  Definition loc_98 : location_info := LocationInfo file_0 59 9 59 21.
-  Definition loc_99 : location_info := LocationInfo file_0 59 9 59 10.
-  Definition loc_100 : location_info := LocationInfo file_0 59 9 59 10.
-  Definition loc_101 : location_info := LocationInfo file_0 59 13 59 21.
-  Definition loc_102 : location_info := LocationInfo file_0 59 14 59 15.
-  Definition loc_103 : location_info := LocationInfo file_0 59 19 59 20.
-  Definition loc_104 : location_info := LocationInfo file_0 59 25 59 26.
-  Definition loc_105 : location_info := LocationInfo file_0 58 16 58 29.
-  Definition loc_106 : location_info := LocationInfo file_0 58 28 58 29.
-  Definition loc_107 : location_info := LocationInfo file_0 58 28 58 29.
+  Definition loc_12 : location_info := LocationInfo file_0 29 2 29 26.
+  Definition loc_13 : location_info := LocationInfo file_0 30 2 30 139.
+  Definition loc_14 : location_info := LocationInfo file_0 30 9 30 138.
+  Definition loc_15 : location_info := LocationInfo file_0 30 35 30 38.
+  Definition loc_16 : location_info := LocationInfo file_0 30 35 30 38.
+  Definition loc_17 : location_info := LocationInfo file_0 30 40 30 77.
+  Definition loc_18 : location_info := LocationInfo file_0 30 49 30 76.
+  Definition loc_19 : location_info := LocationInfo file_0 30 50 30 71.
+  Definition loc_20 : location_info := LocationInfo file_0 30 50 30 63.
+  Definition loc_21 : location_info := LocationInfo file_0 30 62 30 63.
+  Definition loc_22 : location_info := LocationInfo file_0 30 62 30 63.
+  Definition loc_23 : location_info := LocationInfo file_0 30 66 30 71.
+  Definition loc_24 : location_info := LocationInfo file_0 30 66 30 71.
+  Definition loc_25 : location_info := LocationInfo file_0 30 74 30 75.
+  Definition loc_26 : location_info := LocationInfo file_0 30 74 30 75.
+  Definition loc_27 : location_info := LocationInfo file_0 29 16 29 25.
+  Definition loc_28 : location_info := LocationInfo file_0 29 16 29 22.
+  Definition loc_29 : location_info := LocationInfo file_0 29 16 29 22.
+  Definition loc_30 : location_info := LocationInfo file_0 29 23 29 24.
+  Definition loc_31 : location_info := LocationInfo file_0 29 23 29 24.
+  Definition loc_36 : location_info := LocationInfo file_0 39 2 39 30.
+  Definition loc_37 : location_info := LocationInfo file_0 40 2 40 121.
+  Definition loc_38 : location_info := LocationInfo file_0 40 9 40 120.
+  Definition loc_39 : location_info := LocationInfo file_0 40 35 40 38.
+  Definition loc_40 : location_info := LocationInfo file_0 40 35 40 38.
+  Definition loc_41 : location_info := LocationInfo file_0 40 40 40 68.
+  Definition loc_42 : location_info := LocationInfo file_0 40 49 40 67.
+  Definition loc_43 : location_info := LocationInfo file_0 40 50 40 51.
+  Definition loc_44 : location_info := LocationInfo file_0 40 50 40 51.
+  Definition loc_45 : location_info := LocationInfo file_0 40 54 40 66.
+  Definition loc_46 : location_info := LocationInfo file_0 40 54 40 55.
+  Definition loc_47 : location_info := LocationInfo file_0 40 54 40 55.
+  Definition loc_48 : location_info := LocationInfo file_0 40 58 40 66.
+  Definition loc_49 : location_info := LocationInfo file_0 40 59 40 60.
+  Definition loc_50 : location_info := LocationInfo file_0 40 64 40 65.
+  Definition loc_51 : location_info := LocationInfo file_0 39 16 39 29.
+  Definition loc_52 : location_info := LocationInfo file_0 39 28 39 29.
+  Definition loc_53 : location_info := LocationInfo file_0 39 28 39 29.
+  Definition loc_58 : location_info := LocationInfo file_0 45 2 45 15.
+  Definition loc_59 : location_info := LocationInfo file_0 47 2 47 24.
+  Definition loc_60 : location_info := LocationInfo file_0 48 2 48 26.
+  Definition loc_61 : location_info := LocationInfo file_0 50 2 50 36.
+  Definition loc_62 : location_info := LocationInfo file_0 51 2 51 13.
+  Definition loc_63 : location_info := LocationInfo file_0 51 9 51 12.
+  Definition loc_64 : location_info := LocationInfo file_0 51 9 51 12.
+  Definition loc_65 : location_info := LocationInfo file_0 51 10 51 12.
+  Definition loc_66 : location_info := LocationInfo file_0 51 10 51 12.
+  Definition loc_67 : location_info := LocationInfo file_0 50 15 50 35.
+  Definition loc_68 : location_info := LocationInfo file_0 50 26 50 35.
+  Definition loc_69 : location_info := LocationInfo file_0 50 26 50 31.
+  Definition loc_70 : location_info := LocationInfo file_0 50 26 50 31.
+  Definition loc_71 : location_info := LocationInfo file_0 50 32 50 34.
+  Definition loc_72 : location_info := LocationInfo file_0 50 32 50 34.
+  Definition loc_75 : location_info := LocationInfo file_0 48 9 48 24.
+  Definition loc_76 : location_info := LocationInfo file_0 48 9 48 19.
+  Definition loc_77 : location_info := LocationInfo file_0 48 9 48 15.
+  Definition loc_78 : location_info := LocationInfo file_0 48 9 48 15.
+  Definition loc_79 : location_info := LocationInfo file_0 48 16 48 18.
+  Definition loc_80 : location_info := LocationInfo file_0 48 16 48 18.
+  Definition loc_81 : location_info := LocationInfo file_0 48 23 48 24.
+  Definition loc_82 : location_info := LocationInfo file_0 47 13 47 23.
+  Definition loc_83 : location_info := LocationInfo file_0 47 13 47 16.
+  Definition loc_84 : location_info := LocationInfo file_0 47 13 47 16.
+  Definition loc_85 : location_info := LocationInfo file_0 47 17 47 19.
+  Definition loc_86 : location_info := LocationInfo file_0 47 18 47 19.
+  Definition loc_87 : location_info := LocationInfo file_0 47 21 47 22.
+  Definition loc_90 : location_info := LocationInfo file_0 45 13 45 14.
+  Definition loc_95 : location_info := LocationInfo file_0 60 2 60 30.
+  Definition loc_96 : location_info := LocationInfo file_0 61 2 61 27.
+  Definition loc_97 : location_info := LocationInfo file_0 61 9 61 26.
+  Definition loc_98 : location_info := LocationInfo file_0 61 9 61 21.
+  Definition loc_99 : location_info := LocationInfo file_0 61 9 61 10.
+  Definition loc_100 : location_info := LocationInfo file_0 61 9 61 10.
+  Definition loc_101 : location_info := LocationInfo file_0 61 13 61 21.
+  Definition loc_102 : location_info := LocationInfo file_0 61 14 61 15.
+  Definition loc_103 : location_info := LocationInfo file_0 61 19 61 20.
+  Definition loc_104 : location_info := LocationInfo file_0 61 25 61 26.
+  Definition loc_105 : location_info := LocationInfo file_0 60 16 60 29.
+  Definition loc_106 : location_info := LocationInfo file_0 60 28 60 29.
+  Definition loc_107 : location_info := LocationInfo file_0 60 28 60 29.
 
   (* Definition of function [tag_of]. *)
   Definition impl_tag_of : function := {|

examples/proofs/tagged_ptr/generated_proof_is_aligned.v

@@ -12,7 +12,7 @@ Section proof_is_aligned.
     ⊢ typed_function impl_is_aligned type_of_is_aligned.
   Proof.
     Open Scope printing_sugar.
-    start_function "is_aligned" ([[l beta] n]) => arg_p local_i.
+    start_function "is_aligned" ([l n]) => arg_p local_i.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((

examples/proofs/tagged_ptr/generated_proof_tag_of.v

@@ -12,7 +12,7 @@ Section proof_tag_of.
     ⊢ typed_function impl_tag_of type_of_tag_of.
   Proof.
     Open Scope printing_sugar.
-    start_function "tag_of" ([[r ty] v]) => arg_p.
+    start_function "tag_of" ([[[r ty] v] P]) => arg_p.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((

examples/proofs/tagged_ptr/generated_spec.v

@@ -14,18 +14,18 @@ Section spec.
 
   (* Specifications for function [tag_of]. *)
   Definition type_of_tag_of :=
-    fn(∀ (r, ty, v) : (loc * Z) * type * val; (value (void*) (v)); (v ◁ᵥ (r @ (tagged_ptr (Own) (TAG_MOD) (ty)))))
-      → ∃ () : (), ((r.2) @ (int (u8))); ⌜0 ≤ r.2 < TAG_MOD⌝ ∗ (v ◁ᵥ (r @ (tagged_ptr (Own) (TAG_MOD) (ty)))).
+    fn(∀ (r, ty, v, P) : (loc * Z) * type * val * (iProp Σ); (value (void*) (v)); (v ◁ᵥ (r @ (tagged_ptr (Own) (TAG_MOD) (ty)))) ∗ ⌜AllocAlive ty Own P⌝ ∗ (P))
+      → ∃ () : (), ((r.2) @ (int (u8))); ⌜0 ≤ r.2 < TAG_MOD⌝ ∗ (P) ∗ (v ◁ᵥ (r @ (tagged_ptr (Own) (TAG_MOD) (ty)))).
 
   (* Specifications for function [tag]. *)
   Definition type_of_tag :=
     fn(∀ (r, t, ty, P) : (loc * Z) * Z * type * (iProp Σ); (r @ (tagged_ptr (Own) (TAG_MOD) (ty))), (t @ (int (u8))); ⌜0 ≤ t < TAG_MOD⌝ ∗ ⌜AllocAlive ty Own P⌝ ∗ (P))
-      → ∃ () : (), (((r.1, t)) @ (tagged_ptr (Own) (TAG_MOD) (ty))); True.
+      → ∃ () : (), (((r.1, t)) @ (tagged_ptr (Own) (TAG_MOD) (ty))); (P).
 
   (* Specifications for function [untag]. *)
   Definition type_of_untag :=
     fn(∀ (r, ty, P) : (loc * Z) * type * (iProp Σ); (r @ (tagged_ptr (Own) (TAG_MOD) (ty))); ⌜AllocAlive ty Own P⌝ ∗ (P))
-      → ∃ () : (), ((r.1) @ (&own (ty))); True.
+      → ∃ () : (), ((r.1) @ (&own (ty))); (P).
 
   (* Specifications for function [test]. *)
   Definition type_of_test :=
@@ -33,6 +33,6 @@ Section spec.
 
   (* Specifications for function [is_aligned]. *)
   Definition type_of_is_aligned :=
-    fn(∀ (l, beta, n) : loc * own_state * Z; (l @ (&frac{beta} (n @ (int (i32))))); True)
-      → ∃ () : (), ((bool_decide (l `aligned_to` 8%nat)) @ (boolean (i32))); (l ◁ₗ{beta} (n @ (int (i32)))).
+    fn(∀ (l, n) : loc * Z; (l @ (&own (n @ (int (i32))))); True)
+      → ∃ () : (), ((bool_decide (l `aligned_to` 8%nat)) @ (boolean (i32))); (l ◁ₗ (n @ (int (i32)))).
 End spec.

examples/tagged_ptr.c

@@ -10,11 +10,11 @@ typedef unsigned char tag_t;
 
 //@rc::inlined Notation TAG_MOD := (8%nat) (only parsing).
 
-[[rc::parameters("r: {loc * Z}", "ty : type", "v : val")]]
+[[rc::parameters("r: {loc * Z}", "ty : type", "v : val", "P : {iProp Σ}")]]
 [[rc::args("value<void*, v>")]]
-[[rc::requires("v : r @ tagged_ptr<Own, TAG_MOD, ty>")]]
+[[rc::requires("v : r @ tagged_ptr<Own, TAG_MOD, ty>", "{AllocAlive ty Own P}", "[P]")]]
 [[rc::returns("{r.2} @ int<u8>")]]
-[[rc::ensures("{0 ≤ r.2 < TAG_MOD}")]]
+[[rc::ensures("{0 ≤ r.2 < TAG_MOD}", "[P]")]]
 [[rc::ensures("v : r @ tagged_ptr<Own, TAG_MOD, ty>")]]
 tag_t tag_of(void* p){
   return ((uintptr_t) p) % TAG_MOD;
@@ -24,6 +24,7 @@ tag_t tag_of(void* p){
 [[rc::args("r @ tagged_ptr<Own, TAG_MOD, ty>", "t @ int<u8>")]]
 [[rc::requires("{0 ≤ t < TAG_MOD}", "{AllocAlive ty Own P}", "[P]")]]
 [[rc::returns("{(r.1, t)} @ tagged_ptr<Own, TAG_MOD, ty>")]]
+[[rc::ensures("[P]")]]
 void* tag(void* p, tag_t t){
   tag_t old_t = tag_of(p);
   return rc_copy_alloc_id((void*) ((uintptr_t) p - old_t + t), p);
@@ -33,6 +34,7 @@ void* tag(void* p, tag_t t){
 [[rc::args("r @ tagged_ptr<Own, TAG_MOD, ty>")]]
 [[rc::requires("{AllocAlive ty Own P}", "[P]")]]
 [[rc::returns("{r.1} @ &own<ty>")]]
+[[rc::ensures("[P]")]]
 void* untag(void* p){
   uintptr_t i = (uintptr_t) p;
   return rc_copy_alloc_id((void*) (i - i % TAG_MOD), p);
@@ -49,10 +51,10 @@ size_t test(){
   return *px;
 }
 
-[[rc::parameters("l: loc", "beta: own_state", "n: Z")]]
-[[rc::args("l @ &frac<beta, n @ int<i32>>")]]
+[[rc::parameters("l: loc", "n: Z")]]
+[[rc::args("l @ &own<n @ int<i32>>")]]
 [[rc::returns("{bool_decide (l `aligned_to` 8%nat)} @ boolean<i32>")]]
-[[rc::ensures("frac beta l : n @ int<i32>")]]
+[[rc::ensures("own l : n @ int<i32>")]]
 [[rc::tactics("all: unfold aligned_to in *; split; solve_goal.")]]
 int is_aligned(void* p){
   uintptr_t i = (uintptr_t) p;

theories/lang/lang.v

@@ -335,6 +335,7 @@ Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
 | CastOpPI it σ vs vt l:
     val_to_loc vs = Some l →
     val_of_int_repr (IRLoc l) it = Some vt →
+    block_alive l σ.(st_heap) →
     eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
 | CastOpIP it σ vs vt l:
     val_to_loc_weak vs it = Some l →

theories/lang/lifting.v

@@ -350,11 +350,13 @@ Qed.
 Lemma wp_cast_ptr_int Φ v v' l E it:
   val_to_loc v = Some l →
   val_of_int_repr (IRLoc l) it = Some v' →
-  ▷ Φ (v') -∗ WP UnOp (CastOp (IntOp it)) PtrOp (Val v) @ E {{ Φ }}.
+  alloc_alive_loc l ∧ ▷ Φ (v') -∗
+  WP UnOp (CastOp (IntOp it)) PtrOp (Val v) @ E {{ Φ }}.
 Proof.
   iIntros (Hv Hv') "HΦ".
-  iApply wp_unop_det. iSplit => //.
-  iIntros (σ ?) "_ !%". split.
+  iApply wp_unop_det. iSplit; [iDestruct "HΦ" as "[HΦ _]" | iDestruct "HΦ" as "[_ $]"].
+  iIntros (σ ?) "Hctx". iDestruct (alloc_alive_loc_to_block_alive with "HΦ Hctx") as %?.
+  iPureIntro. split.
   - by inversion 1; simplify_eq.
   - move => ->. by econstructor.
 Qed.

theories/typing/intptr.v

@@ -73,10 +73,12 @@ Section programs.
   Context `{!typeG Σ}.
 
   Lemma type_cast_ptr_intptr (p : loc) β it ty T:
-    (∃ n, (p ◁ₗ{β} ty -∗ loc_in_bounds p n ∗ True) ∧
+    (∃ n,
+      (p ◁ₗ{β} ty -∗ loc_in_bounds p n ∗ True) ∧
       (⌜min_alloc_start ≤ p.2 ∧ p.2 + n ≤ max_alloc_end⌝ -∗
        p ◁ₗ{β} ty -∗
-       ⌜p.2 ∈ it⌝ ∗ T (val_of_loc_n (bytes_per_int it) p) (t2mt (p @ intptr it)))
+       ⌜p.2 ∈ it⌝ ∗
+         ((alloc_alive_loc p ∗ True) ∧ T (val_of_loc_n (bytes_per_int it) p) (t2mt (p @ intptr it))))
     ) -∗
     typed_un_op p (p ◁ₗ{β} ty) (CastOp (IntOp it)) PtrOp T.
   Proof.
@@ -88,6 +90,7 @@ Section programs.
     iDestruct ("HT" with "[//] Hp") as (?) "HT".
     iApply wp_cast_ptr_int => //=; first by rewrite val_to_of_loc.
     { rewrite bool_decide_true; naive_solver. }
+    iSplit; [by iDestruct "HT" as "[[$ _] _]" | iDestruct "HT" as "[_ HT]"].
     iApply ("HΦ" with "[] HT").
     iPureIntro. by apply val_to_loc_weak_val_of_loc_n.
   Qed.
@@ -98,7 +101,8 @@ Section programs.
   Lemma type_cast_ptr_intptr_val (v : val) (p : loc) it (n : nat) T:
     (⌜min_alloc_start ≤ p.2 ∧ p.2 + n ≤ max_alloc_end⌝ -∗
       v ◁ᵥ p @ ptr n -∗
-      ⌜p.2 ∈ it⌝ ∗ T (val_of_loc_n (bytes_per_int it) p) (t2mt (p @ intptr it))
+      ⌜p.2 ∈ it⌝ ∗
+       (alloc_alive_loc p ∗ True) ∧ T (val_of_loc_n (bytes_per_int it) p) (t2mt (p @ intptr it))
     ) -∗
     typed_un_op v (v ◁ᵥ p @ ptr n) (CastOp (IntOp it)) PtrOp T.
   Proof.
@@ -107,6 +111,7 @@ Section programs.
     iDestruct ("HT" with "[//] []") as (?) "HT". { by iFrame "Hlib". }
     iApply wp_cast_ptr_int => //=; first by rewrite val_to_of_loc.
     { rewrite bool_decide_true; naive_solver. }
+    iSplit; [by iDestruct "HT" as "[[$ _] _]" | iDestruct "HT" as "[_ HT]"].
     iApply ("HΦ" with "[] HT").
     iPureIntro. by apply val_to_loc_weak_val_of_loc_n.
   Qed.

theories/typing/tagged_ptr.v

@@ -94,7 +94,9 @@ Section tagged_ptr.
         loc_in_bounds r.1 align -∗
         r.1 ◁ₗ{β} ty -∗
         v ◁ᵥ r @ tagged_ptr β align (place r.1) -∗
-        ⌜(r.1.2 + r.2)%Z ∈ it⌝ ∗ T (val_of_loc_n (bytes_per_int it) (r.1 +ₗ r.2)) (t2mt ((r.1 +ₗ r.2) @ intptr it))
+        ⌜(r.1.2 + r.2)%Z ∈ it⌝ ∗
+        ((alloc_alive_loc r.1 ∗ True) ∧
+        T (val_of_loc_n (bytes_per_int it) (r.1 +ₗ r.2)) (t2mt ((r.1 +ₗ r.2) @ intptr it)))
     ) -∗
     typed_un_op v (v ◁ᵥ r @ tagged_ptr β align ty) (CastOp (IntOp it)) PtrOp T.
   Proof.
@@ -104,7 +106,9 @@ Section tagged_ptr.
     { by iFrame "Hlib". }
     iApply wp_cast_ptr_int => //=; first by rewrite val_to_of_loc.
     { by rewrite bool_decide_true. }
-    iApply ("HΦ" with "[] HT").
+    iSplit.
+    { iDestruct "HT" as "[[HT _] _]". by iApply (alloc_alive_loc_mono with "HT"). }
+    iDestruct "HT" as "[_ HT]". iApply ("HΦ" with "[] HT").
     iPureIntro. by apply val_to_loc_weak_val_of_loc_n.
   Qed.
   Global Instance type_cast_tagged_ptr_intptr_val_inst (v : val) (r : loc * Z) β (align : nat) it ty: