Progress towards tracking pointer provenance in integers

examples/intptr.c

@@ -2,19 +2,49 @@
 #include <stdint.h>
 #include <stddef.h>
 
-[[rc::args("&own<int<i32>>")]]
-[[rc::returns("int<size_t>")]]
-size_t int_ptr(int* p){
-  size_t i = (size_t) p;
+//@rc::inlined
+//@Notation "P ? l : r" :=
+//@  (if bool_decide P then l else r)
+//@  (at level 100, l at next level, r at next level).
+//@rc::end
+
+/**** Casting a pointer to an integer ***************************************/
+
+// Cast a pointer to an integer, keeping the provenance. 
+[[rc::parameters("l : loc")]]
+[[rc::args("l @ &own<int<i32>>")]]
+[[rc::returns("l @ intptr<uintptr_t>")]]
+uintptr_t int_ptr1(int* p){
+  uintptr_t i = (uintptr_t) p;
+  // return (i + 0); ← Does not work (provenance dropped by arithmetic).
+  return i;
+}
+
+// Cast a pointer to an integer, but losing the provenance.
+[[rc::parameters("l : loc")]]
+[[rc::args("l @ &own<int<i32>>")]]
+[[rc::returns("{l.2} @ int<uintptr_t>")]]
+uintptr_t int_ptr2(int* p){
+  uintptr_t i = (uintptr_t) p;
   return i;
 }
 
+// Cast a pointer to an integer, but losing the provenance.
+[[rc::parameters("l : loc")]]
+[[rc::args("l @ &own<int<i32>>")]]
+[[rc::returns("{l.2} @ int<uintptr_t>")]]
+uintptr_t int_ptr3(int* p){
+  uintptr_t i = (uintptr_t) p;
+  return i + 0; // ← We can do arithmetic (provenance not required).
+}
+
+// Weird function working on integers obtained from pointers.
 [[rc::parameters("p1 : loc", "p2 : loc")]]
 [[rc::args("p1 @ &own<int<i32>>", "p2 @ &own<int<i32>>")]]
-[[rc::returns("{p1.2 `min` p2.2} @ int<size_t>")]]
-size_t min_ptr_val(int *p1, int *p2){
-  size_t i1 = (size_t) p1;
-  size_t i2 = (size_t) p2;
+[[rc::returns("{p1.2 `min` p2.2} @ int<uintptr_t>")]]
+uintptr_t min_ptr_val1(int *p1, int *p2){
+  uintptr_t i1 = (uintptr_t) p1;
+  uintptr_t i2 = (uintptr_t) p2;
 
   if(i1 <= i2){
     return i1;
@@ -23,53 +53,106 @@ size_t min_ptr_val(int *p1, int *p2){
   return i2;
 }
 
+// The same but keeping the provenance.
+[[rc::parameters("p1 : loc", "p2 : loc")]]
+[[rc::args("p1 @ &own<int<i32>>", "p2 @ &own<int<i32>>")]]
+[[rc::returns("{p1.2 ≤ p2.2 ? p1 : p2} @ intptr<uintptr_t>")]]
+uintptr_t min_ptr_val2(int *p1, int *p2){
+  uintptr_t i1 = (uintptr_t) p1;
+  uintptr_t i2 = (uintptr_t) p2;
+
+  if(i1 <= i2){
+    return i1;
+  }
+
+  return i2;
+}
+
+/**** Casting an integer to a pointer ***************************************/
+
+// Simple roundtrip cast.
 [[rc::parameters("p : loc")]]
 [[rc::args("p @ &own<int<i32>>")]]
-[[rc::returns("{(None, p.2)} @ &own<place<{(None, p.2)}>>")]]
+[[rc::returns("p @ &own<place<p>>")]]
 int* roundtrip1(int* p){
-  size_t i = (size_t) p;
-  void *q = (void*) i;
+  uintptr_t i = (uintptr_t) p;
+  void *q = (void*) i; // ← The provenance transfered back.
+  return q;
+}
+
+// Roundtrip cast with dummy arithmetic.
+[[rc::parameters("p : loc")]]
+[[rc::args("p @ &own<int<i32>>")]]
+[[rc::exists("id : {option alloc_id}")]] // ← Only ∃ on provenance.
+[[rc::returns("{(id, p.2)} @ &own<place<{(id, p.2)}>>")]]
+int* roundtrip2(int* p){
+  uintptr_t i = (uintptr_t) p;
+  void *q = (void*) (i + 0); // ← The provenance is lost here.
   return q;
 }
 
+// Roundtrip cast with dummy arithmetic and provenance recovery.
 [[rc::parameters("p : loc", "n : Z")]]
 [[rc::args("p @ &own<n @ int<i32>>")]]
 [[rc::returns("p @ &own<n @ int<i32>>")]]
-[[rc::tactics("all: try solve_loc_eq.")]]
-int* roundtrip2(int* p){
-  size_t i = (size_t) p;
-  int *q = (void*) i;
-  return rc_copy_alloc_id(q, p);
+int* roundtrip3(int* p){
+  uintptr_t i = (uintptr_t) p;
+  int *q = (void*) (i + 0); // ← The provenance is lost here.
+  return rc_copy_alloc_id(q, p); // ← Copy provenance from [p].
 }
 
+// Roundrip cast with flow of ownership.
 [[rc::parameters("l : loc", "n : Z")]]
 [[rc::args("l @ &own<n @ int<i32>>")]]
 [[rc::returns("n @ int<i32>")]]
 [[rc::ensures("own l : n @ int<i32>")]]
-int roundtrip_and_read(int* p){
-  size_t i = (size_t) p;
+int roundtrip_and_read1(int* p){
+  uintptr_t i = (uintptr_t) p;
   int *q = (int*) i;
+  int r = *q;
+  return r;
+}
+
+// Roundrip cast with flow of ownership and provenance recovery.
+[[rc::parameters("l : loc", "n : Z")]]
+[[rc::args("l @ &own<n @ int<i32>>")]]
+[[rc::returns("n @ int<i32>")]]
+[[rc::ensures("own l : n @ int<i32>")]]
+int roundtrip_and_read2(int* p){
+  uintptr_t i = (uintptr_t) p;
+  int *q = (int*) (i * 1);
   q = rc_copy_alloc_id(q, p);
   int r = *q;
   return r;
 }
 
+// Small variation in syntax (for testing).
 [[rc::parameters("p : loc", "n : Z")]]
 [[rc::args("p @ &own<n @ int<i32>>")]]
 [[rc::returns("n @ int<i32>")]]
 [[rc::ensures("own p : n @ int<i32>")]]
-int roundtrip_and_read2(int* p){
+int roundtrip_and_read3(int* p){
   uintptr_t i = (uintptr_t) p;
-  int *q = rc_copy_alloc_id((int*) i, p);
+  int *q = rc_copy_alloc_id((int*) (i * 1), p);
   return *q;
 }
 
+// Another variant of the same example.
 [[rc::parameters("p : loc", "n : Z")]]
 [[rc::args("p @ &own<n @ int<i32>>")]]
 [[rc::returns("n @ int<i32>")]]
 [[rc::ensures("own p : n @ int<i32>")]]
-int roundtrip_and_read3(int* p){
-  size_t i = (size_t) p;
-  int *q = (int*) i;
+int roundtrip_and_read4(int* p){
+  uintptr_t i = (uintptr_t) p;
+  int *q = (int*) (i * 1);
   return *(rc_copy_alloc_id(q, p));
 }
+
+// Copy the provenance from an int.
+[[rc::parameters("p : loc")]]
+[[rc::args("p @ intptr<uintptr_t>")]]
+[[rc::returns("p @ &own<place<p>>")]]
+void* int_to_ptr(uintptr_t p){
+  void *q = (void*) (p * 1);
+  return (rc_copy_alloc_id(q, p));
+}

examples/mutable_map.c

@@ -111,7 +111,7 @@ size_t fsm_slot_for_key(size_t len, size_t key) {
 [[rc::ensures("{∃ x, items !! n = Some x ∧ probe_ref key items = Some (n, x)}")]]
  [[rc::lemmas("lookup_lt_is_Some_2")]]
  [[rc::tactics("all: try by eexists _; split => //; apply probe_ref_take_Some; naive_solver.")]]
- [[rc::tactics("all: try by apply: probe_ref_go_next_take=> //i; intros Hi%lookup_rotate_r_Some; try lia; simplify_eq; naive_solver.")]]
+ [[rc::tactics("all: try by apply: probe_ref_go_next_take => // ? /lookup_rotate_r_Some ?; try lia; simplify_eq; naive_solver.")]]
 size_t fsm_probe(struct fixed_size_map *m, size_t key) {
     size_t slot_idx = fsm_slot_for_key(m->length, key);
 

examples/proofs/intptr/generated_proof_int_ptr.v → examples/proofs/intptr/generated_proof_int_ptr1.v

@@ -4,23 +4,23 @@ From refinedc.examples.intptr Require Import generated_spec.
 Set Default Proof Using "Type".
 
 (* Generated from [examples/intptr.c]. *)
-Section proof_int_ptr.
+Section proof_int_ptr1.
   Context `{!typeG Σ} `{!globalG Σ}.
 
-  (* Typing proof for [int_ptr]. *)
-  Lemma type_int_ptr :
-    ⊢ typed_function impl_int_ptr type_of_int_ptr.
+  (* Typing proof for [int_ptr1]. *)
+  Lemma type_int_ptr1 :
+    ⊢ typed_function impl_int_ptr1 type_of_int_ptr1.
   Proof.
     Open Scope printing_sugar.
-    start_function "int_ptr" ([]) => arg_p local_i.
+    start_function "int_ptr1" (l) => arg_p local_i.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((
       ∅
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
-      all: print_typesystem_goal "int_ptr" "#0".
+      all: print_typesystem_goal "int_ptr1" "#0".
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
-    all: print_sidecondition_goal "int_ptr".
+    all: print_sidecondition_goal "int_ptr1".
   Qed.
-End proof_int_ptr.
+End proof_int_ptr1.

examples/proofs/intptr/generated_proof_min_ptr_val.v → examples/proofs/intptr/generated_proof_int_ptr2.v

@@ -4,23 +4,23 @@ From refinedc.examples.intptr Require Import generated_spec.
 Set Default Proof Using "Type".
 
 (* Generated from [examples/intptr.c]. *)
-Section proof_min_ptr_val.
+Section proof_int_ptr2.
   Context `{!typeG Σ} `{!globalG Σ}.
 
-  (* Typing proof for [min_ptr_val]. *)
-  Lemma type_min_ptr_val :
-    ⊢ typed_function impl_min_ptr_val type_of_min_ptr_val.
+  (* Typing proof for [int_ptr2]. *)
+  Lemma type_int_ptr2 :
+    ⊢ typed_function impl_int_ptr2 type_of_int_ptr2.
   Proof.
     Open Scope printing_sugar.
-    start_function "min_ptr_val" ([p1 p2]) => arg_p1 arg_p2 local_i2 local_i1.
+    start_function "int_ptr2" (l) => arg_p local_i.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((
       ∅
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
-      all: print_typesystem_goal "min_ptr_val" "#0".
+      all: print_typesystem_goal "int_ptr2" "#0".
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
-    all: print_sidecondition_goal "min_ptr_val".
+    all: print_sidecondition_goal "int_ptr2".
   Qed.
-End proof_min_ptr_val.
+End proof_int_ptr2.

examples/proofs/intptr/generated_proof_roundtrip_and_read.v → examples/proofs/intptr/generated_proof_int_ptr3.v

@@ -4,23 +4,23 @@ From refinedc.examples.intptr Require Import generated_spec.
 Set Default Proof Using "Type".
 
 (* Generated from [examples/intptr.c]. *)
-Section proof_roundtrip_and_read.
+Section proof_int_ptr3.
   Context `{!typeG Σ} `{!globalG Σ}.
 
-  (* Typing proof for [roundtrip_and_read]. *)
-  Lemma type_roundtrip_and_read :
-    ⊢ typed_function impl_roundtrip_and_read type_of_roundtrip_and_read.
+  (* Typing proof for [int_ptr3]. *)
+  Lemma type_int_ptr3 :
+    ⊢ typed_function impl_int_ptr3 type_of_int_ptr3.
   Proof.
     Open Scope printing_sugar.
-    start_function "roundtrip_and_read" ([l n]) => arg_p local_i local_r local_q.
+    start_function "int_ptr3" (l) => arg_p local_i.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((
       ∅
     )%I : gmap label (iProp Σ)).
     - repeat liRStep; liShow.
-      all: print_typesystem_goal "roundtrip_and_read" "#0".
+      all: print_typesystem_goal "int_ptr3" "#0".
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
-    all: print_sidecondition_goal "roundtrip_and_read".
+    all: print_sidecondition_goal "int_ptr3".
   Qed.
-End proof_roundtrip_and_read.
+End proof_int_ptr3.

examples/proofs/intptr/generated_proof_int_to_ptr.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.intptr Require Import generated_code.
+From refinedc.examples.intptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/intptr.c]. *)
+Section proof_int_to_ptr.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [int_to_ptr]. *)
+  Lemma type_int_to_ptr :
+    ⊢ typed_function impl_int_to_ptr type_of_int_to_ptr.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "int_to_ptr" (p) => arg_p local_q.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "int_to_ptr" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "int_to_ptr".
+  Qed.
+End proof_int_to_ptr.

examples/proofs/intptr/generated_proof_min_ptr_val1.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.intptr Require Import generated_code.
+From refinedc.examples.intptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/intptr.c]. *)
+Section proof_min_ptr_val1.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [min_ptr_val1]. *)
+  Lemma type_min_ptr_val1 :
+    ⊢ typed_function impl_min_ptr_val1 type_of_min_ptr_val1.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "min_ptr_val1" ([p1 p2]) => arg_p1 arg_p2 local_i2 local_i1.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "min_ptr_val1" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "min_ptr_val1".
+  Qed.
+End proof_min_ptr_val1.

examples/proofs/intptr/generated_proof_min_ptr_val2.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.intptr Require Import generated_code.
+From refinedc.examples.intptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/intptr.c]. *)
+Section proof_min_ptr_val2.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [min_ptr_val2]. *)
+  Lemma type_min_ptr_val2 :
+    ⊢ typed_function impl_min_ptr_val2 type_of_min_ptr_val2.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "min_ptr_val2" ([p1 p2]) => arg_p1 arg_p2 local_i2 local_i1.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "min_ptr_val2" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "min_ptr_val2".
+  Qed.
+End proof_min_ptr_val2.

examples/proofs/intptr/generated_proof_roundtrip2.v

@@ -12,7 +12,7 @@ Section proof_roundtrip2.
     ⊢ typed_function impl_roundtrip2 type_of_roundtrip2.
   Proof.
     Open Scope printing_sugar.
-    start_function "roundtrip2" ([p n]) => arg_p local_i local_q.
+    start_function "roundtrip2" (p) => arg_p local_i local_q.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((
@@ -21,7 +21,6 @@ Section proof_roundtrip2.
     - repeat liRStep; liShow.
       all: print_typesystem_goal "roundtrip2" "#0".
     Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
-    all: try solve_loc_eq.
     all: print_sidecondition_goal "roundtrip2".
   Qed.
 End proof_roundtrip2.

examples/proofs/intptr/generated_proof_roundtrip3.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.intptr Require Import generated_code.
+From refinedc.examples.intptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/intptr.c]. *)
+Section proof_roundtrip3.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [roundtrip3]. *)
+  Lemma type_roundtrip3 :
+    ⊢ typed_function impl_roundtrip3 type_of_roundtrip3.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "roundtrip3" ([p n]) => arg_p local_i local_q.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "roundtrip3" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "roundtrip3".
+  Qed.
+End proof_roundtrip3.

examples/proofs/intptr/generated_proof_roundtrip_and_read1.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.intptr Require Import generated_code.
+From refinedc.examples.intptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/intptr.c]. *)
+Section proof_roundtrip_and_read1.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [roundtrip_and_read1]. *)
+  Lemma type_roundtrip_and_read1 :
+    ⊢ typed_function impl_roundtrip_and_read1 type_of_roundtrip_and_read1.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "roundtrip_and_read1" ([l n]) => arg_p local_i local_r local_q.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "roundtrip_and_read1" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "roundtrip_and_read1".
+  Qed.
+End proof_roundtrip_and_read1.

examples/proofs/intptr/generated_proof_roundtrip_and_read2.v

@@ -12,7 +12,7 @@ Section proof_roundtrip_and_read2.
     ⊢ typed_function impl_roundtrip_and_read2 type_of_roundtrip_and_read2.
   Proof.
     Open Scope printing_sugar.
-    start_function "roundtrip_and_read2" ([p n]) => arg_p local_i local_q.
+    start_function "roundtrip_and_read2" ([l n]) => arg_p local_i local_r local_q.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((

examples/proofs/intptr/generated_proof_roundtrip_and_read4.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.intptr Require Import generated_code.
+From refinedc.examples.intptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/intptr.c]. *)
+Section proof_roundtrip_and_read4.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [roundtrip_and_read4]. *)
+  Lemma type_roundtrip_and_read4 :
+    ⊢ typed_function impl_roundtrip_and_read4 type_of_roundtrip_and_read4.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "roundtrip_and_read4" ([p n]) => arg_p local_i local_q.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "roundtrip_and_read4" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "roundtrip_and_read4".
+  Qed.
+End proof_roundtrip_and_read4.

examples/proofs/intptr/generated_spec.v

@@ -6,40 +6,76 @@ Set Default Proof Using "Type".
 Section spec.
   Context `{!typeG Σ} `{!globalG Σ}.
 
+  (* Inlined code. *)
+
+  Notation "P ? l : r" :=
+    (if bool_decide P then l else r)
+    (at level 100, l at next level, r at next level).
+
   (* Type definitions. *)
 
-  (* Specifications for function [int_ptr]. *)
-  Definition type_of_int_ptr :=
-    fn(∀ () : (); (&own (int (i32))); True)
-      → ∃ () : (), (int (size_t)); True.
+  (* Specifications for function [int_ptr1]. *)
+  Definition type_of_int_ptr1 :=
+    fn(∀ l : loc; (l @ (&own (int (i32)))); True)
+      → ∃ () : (), (l @ (intptr (uintptr_t))); True.
+
+  (* Specifications for function [int_ptr2]. *)
+  Definition type_of_int_ptr2 :=
+    fn(∀ l : loc; (l @ (&own (int (i32)))); True)
+      → ∃ () : (), ((l.2) @ (int (uintptr_t))); True.
+
+  (* Specifications for function [int_ptr3]. *)
+  Definition type_of_int_ptr3 :=
+    fn(∀ l : loc; (l @ (&own (int (i32)))); True)
+      → ∃ () : (), ((l.2) @ (int (uintptr_t))); True.
 
-  (* Specifications for function [min_ptr_val]. *)
-  Definition type_of_min_ptr_val :=
+  (* Specifications for function [min_ptr_val1]. *)
+  Definition type_of_min_ptr_val1 :=
     fn(∀ (p1, p2) : loc * loc; (p1 @ (&own (int (i32)))), (p2 @ (&own (int (i32)))); True)
-      → ∃ () : (), ((p1.2 `min` p2.2) @ (int (size_t))); True.
+      → ∃ () : (), ((p1.2 `min` p2.2) @ (int (uintptr_t))); True.
+
+  (* Specifications for function [min_ptr_val2]. *)
+  Definition type_of_min_ptr_val2 :=
+    fn(∀ (p1, p2) : loc * loc; (p1 @ (&own (int (i32)))), (p2 @ (&own (int (i32)))); True)
+      → ∃ () : (), ((p1.2 ≤ p2.2 ? p1 : p2) @ (intptr (uintptr_t))); True.
 
   (* Specifications for function [roundtrip1]. *)
   Definition type_of_roundtrip1 :=
     fn(∀ p : loc; (p @ (&own (int (i32)))); True)
-      → ∃ () : (), (((None, p.2)) @ (&own (place ((None, p.2))))); True.
+      → ∃ () : (), (p @ (&own (place (p)))); True.
 
   (* Specifications for function [roundtrip2]. *)
   Definition type_of_roundtrip2 :=
+    fn(∀ p : loc; (p @ (&own (int (i32)))); True)
+      → ∃ id : (option alloc_id), (((id, p.2)) @ (&own (place ((id, p.2))))); True.
+
+  (* Specifications for function [roundtrip3]. *)
+  Definition type_of_roundtrip3 :=
     fn(∀ (p, n) : loc * Z; (p @ (&own (n @ (int (i32))))); True)
       → ∃ () : (), (p @ (&own (n @ (int (i32))))); True.
 
-  (* Specifications for function [roundtrip_and_read]. *)
-  Definition type_of_roundtrip_and_read :=
+  (* Specifications for function [roundtrip_and_read1]. *)
+  Definition type_of_roundtrip_and_read1 :=
     fn(∀ (l, n) : loc * Z; (l @ (&own (n @ (int (i32))))); True)
       → ∃ () : (), (n @ (int (i32))); (l ◁ₗ (n @ (int (i32)))).
 
   (* Specifications for function [roundtrip_and_read2]. *)
   Definition type_of_roundtrip_and_read2 :=
-    fn(∀ (p, n) : loc * Z; (p @ (&own (n @ (int (i32))))); True)
-      → ∃ () : (), (n @ (int (i32))); (p ◁ₗ (n @ (int (i32)))).
+    fn(∀ (l, n) : loc * Z; (l @ (&own (n @ (int (i32))))); True)
+      → ∃ () : (), (n @ (int (i32))); (l ◁ₗ (n @ (int (i32)))).
 
   (* Specifications for function [roundtrip_and_read3]. *)
   Definition type_of_roundtrip_and_read3 :=
     fn(∀ (p, n) : loc * Z; (p @ (&own (n @ (int (i32))))); True)
       → ∃ () : (), (n @ (int (i32))); (p ◁ₗ (n @ (int (i32)))).
+