make copy alloc id a function

examples/proofs/binary_search/generated_proof_copy_alloc_id.v

+(* You were too lazy to even write a spec for this function. *)

examples/proofs/binary_search/generated_spec.v

@@ -13,6 +13,8 @@ Section spec.
 
   (* Type definitions. *)
 
+  (* Function [copy_alloc_id] has been skipped. *)
+
   (* Specifications for function [alloc]. *)
   Definition type_of_alloc :=
     fn(∀ size : nat; (size @ (int (size_t))); ⌜size + 16 ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))

examples/proofs/binary_search/proof_files

@@ -2,6 +2,7 @@ generated_proof_alloc.v
 generated_proof_alloc_array.v
 generated_proof_binary_search.v
 generated_proof_compare_int.v
+generated_proof_copy_alloc_id.v
 generated_proof_free.v
 generated_proof_free_array.v
 generated_proof_test.v

examples/proofs/btree/generated_proof_copy_alloc_id.v

+(* You were too lazy to even write a spec for this function. *)

examples/proofs/btree/generated_spec.v

@@ -88,6 +88,8 @@ Section spec.
 
   (* Type definitions. *)
 
+  (* Function [copy_alloc_id] has been skipped. *)
+
   (* Specifications for function [alloc]. *)
   Definition type_of_alloc :=
     fn(∀ size : nat; (size @ (int (size_t))); ⌜size + 16 ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))

examples/proofs/btree/proof_files

@@ -4,6 +4,7 @@ generated_proof_btree_find.v
 generated_proof_btree_insert.v
 generated_proof_btree_make_root.v
 generated_proof_btree_member.v
+generated_proof_copy_alloc_id.v
 generated_proof_free.v
 generated_proof_free_array.v
 generated_proof_free_btree.v

examples/proofs/intptr/generated_proof_copy_alloc_id.v

+(* You were too lazy to even write a spec for this function. *)

examples/proofs/intptr/generated_proof_roundtrip3.v

@@ -8,8 +8,9 @@ Section proof_roundtrip3.
   Context `{!typeG Σ} `{!globalG Σ}.
 
   (* Typing proof for [roundtrip3]. *)
-  Lemma type_roundtrip3 :
-    ⊢ typed_function impl_roundtrip3 type_of_roundtrip3.
+  Lemma type_roundtrip3 (global_copy_alloc_id : loc) :
+    global_copy_alloc_id ◁ᵥ global_copy_alloc_id @ inline_function_ptr impl_copy_alloc_id -∗
+    typed_function (impl_roundtrip3 global_copy_alloc_id) type_of_roundtrip3.
   Proof.
     Open Scope printing_sugar.
     start_function "roundtrip3" ([p n]) => arg_p local_i local_k.

examples/proofs/intptr/generated_proof_roundtrip_and_read2.v

@@ -8,8 +8,9 @@ Section proof_roundtrip_and_read2.
   Context `{!typeG Σ} `{!globalG Σ}.
 
   (* Typing proof for [roundtrip_and_read2]. *)
-  Lemma type_roundtrip_and_read2 :
-    ⊢ typed_function impl_roundtrip_and_read2 type_of_roundtrip_and_read2.
+  Lemma type_roundtrip_and_read2 (global_copy_alloc_id : loc) :
+    global_copy_alloc_id ◁ᵥ global_copy_alloc_id @ inline_function_ptr impl_copy_alloc_id -∗
+    typed_function (impl_roundtrip_and_read2 global_copy_alloc_id) type_of_roundtrip_and_read2.
   Proof.
     Open Scope printing_sugar.
     start_function "roundtrip_and_read2" ([l n]) => arg_p local_i local_r local_q local_j.

examples/proofs/intptr/generated_proof_roundtrip_and_read3.v

@@ -8,8 +8,9 @@ Section proof_roundtrip_and_read3.
   Context `{!typeG Σ} `{!globalG Σ}.
 
   (* Typing proof for [roundtrip_and_read3]. *)
-  Lemma type_roundtrip_and_read3 :
-    ⊢ typed_function impl_roundtrip_and_read3 type_of_roundtrip_and_read3.
+  Lemma type_roundtrip_and_read3 (global_copy_alloc_id : loc) :
+    global_copy_alloc_id ◁ᵥ global_copy_alloc_id @ inline_function_ptr impl_copy_alloc_id -∗
+    typed_function (impl_roundtrip_and_read3 global_copy_alloc_id) type_of_roundtrip_and_read3.
   Proof.
     Open Scope printing_sugar.
     start_function "roundtrip_and_read3" ([p n]) => arg_p local_i local_q.

examples/proofs/intptr/generated_proof_roundtrip_and_read4.v

@@ -8,8 +8,9 @@ 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.
+  Lemma type_roundtrip_and_read4 (global_copy_alloc_id : loc) :
+    global_copy_alloc_id ◁ᵥ global_copy_alloc_id @ inline_function_ptr impl_copy_alloc_id -∗
+    typed_function (impl_roundtrip_and_read4 global_copy_alloc_id) type_of_roundtrip_and_read4.
   Proof.
     Open Scope printing_sugar.
     start_function "roundtrip_and_read4" ([p n]) => arg_p local_i local_q local_j.

examples/proofs/intptr/generated_proof_roundtrip_and_read_past_the_end_copy_alloc_id.v

@@ -8,8 +8,9 @@ Section proof_roundtrip_and_read_past_the_end_copy_alloc_id.
   Context `{!typeG Σ} `{!globalG Σ}.
 
   (* Typing proof for [roundtrip_and_read_past_the_end_copy_alloc_id]. *)
-  Lemma type_roundtrip_and_read_past_the_end_copy_alloc_id :
-    ⊢ typed_function impl_roundtrip_and_read_past_the_end_copy_alloc_id type_of_roundtrip_and_read_past_the_end_copy_alloc_id.
+  Lemma type_roundtrip_and_read_past_the_end_copy_alloc_id (global_copy_alloc_id : loc) :
+    global_copy_alloc_id ◁ᵥ global_copy_alloc_id @ inline_function_ptr impl_copy_alloc_id -∗
+    typed_function (impl_roundtrip_and_read_past_the_end_copy_alloc_id global_copy_alloc_id) type_of_roundtrip_and_read_past_the_end_copy_alloc_id.
   Proof.
     Open Scope printing_sugar.
     start_function "roundtrip_and_read_past_the_end_copy_alloc_id" ([]) => local_x local_q local_p local_pi.

examples/proofs/intptr/generated_spec.v

@@ -14,6 +14,8 @@ Section spec.
 
   (* Type definitions. *)
 
+  (* Function [copy_alloc_id] has been skipped. *)
+
   (* Specifications for function [int_ptr1]. *)
   Definition type_of_int_ptr1 :=
     fn(∀ l : loc; (l @ (&own (int (i32)))); True)

examples/proofs/intptr/proof_files

 generated_proof_cast_NULL.v
+generated_proof_copy_alloc_id.v
 generated_proof_int_ptr1.v
 generated_proof_int_ptr2.v
 generated_proof_int_ptr3.v

examples/proofs/lock/generated_proof_copy_alloc_id.v

+(* You were too lazy to even write a spec for this function. *)

examples/proofs/lock/generated_spec.v

@@ -93,6 +93,8 @@ Section spec.
 
   (* Type definitions. *)
 
+  (* Function [copy_alloc_id] has been skipped. *)
+
   (* Function [atomic_thread_fence] has been skipped. *)
 
   (* Function [atomic_signal_fence] has been skipped. *)