make calls extensible and add rc::inlined

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/ocaml_runtime/generated_code.v

@@ -5,56 +5,81 @@ Set Default Proof Using "Type".
 
 (* Generated from [examples/ocaml_runtime.c]. *)
 Section code.
-  Definition file_0 : string := "examples/ocaml_runtime.c".
-  Definition loc_2 : location_info := LocationInfo file_0 29 2 29 39.
-  Definition loc_3 : location_info := LocationInfo file_0 30 2 30 30.
-  Definition loc_4 : location_info := LocationInfo file_0 32 2 32 32.
-  Definition loc_5 : location_info := LocationInfo file_0 33 2 33 57.
-  Definition loc_6 : location_info := LocationInfo file_0 35 2 35 28.
-  Definition loc_7 : location_info := LocationInfo file_0 36 2 36 28.
-  Definition loc_8 : location_info := LocationInfo file_0 38 2 38 54.
-  Definition loc_9 : location_info := LocationInfo file_0 39 2 39 28.
-  Definition loc_10 : location_info := LocationInfo file_0 40 2 40 39.
-  Definition loc_11 : location_info := LocationInfo file_0 40 9 40 37.
-  Definition loc_12 : location_info := LocationInfo file_0 40 9 40 23.
-  Definition loc_13 : location_info := LocationInfo file_0 40 9 40 23.
-  Definition loc_14 : location_info := LocationInfo file_0 40 10 40 23.
-  Definition loc_15 : location_info := LocationInfo file_0 40 10 40 23.
-  Definition loc_16 : location_info := LocationInfo file_0 40 27 40 37.
-  Definition loc_17 : location_info := LocationInfo file_0 39 9 39 26.
-  Definition loc_18 : location_info := LocationInfo file_0 39 9 39 20.
-  Definition loc_19 : location_info := LocationInfo file_0 39 10 39 14.
-  Definition loc_20 : location_info := LocationInfo file_0 39 10 39 14.
-  Definition loc_21 : location_info := LocationInfo file_0 39 18 39 19.
-  Definition loc_22 : location_info := LocationInfo file_0 39 24 39 26.
-  Definition loc_23 : location_info := LocationInfo file_0 38 33 38 53.
-  Definition loc_24 : location_info := LocationInfo file_0 38 51 38 53.
-  Definition loc_25 : location_info := LocationInfo file_0 38 51 38 53.
-  Definition loc_28 : location_info := LocationInfo file_0 36 9 36 26.
-  Definition loc_29 : location_info := LocationInfo file_0 36 10 36 20.
-  Definition loc_30 : location_info := LocationInfo file_0 36 11 36 15.
-  Definition loc_31 : location_info := LocationInfo file_0 36 11 36 15.
-  Definition loc_32 : location_info := LocationInfo file_0 36 18 36 19.
-  Definition loc_33 : location_info := LocationInfo file_0 36 24 36 25.
-  Definition loc_34 : location_info := LocationInfo file_0 35 9 35 26.
-  Definition loc_35 : location_info := LocationInfo file_0 35 10 35 20.
-  Definition loc_36 : location_info := LocationInfo file_0 35 11 35 15.
-  Definition loc_37 : location_info := LocationInfo file_0 35 11 35 15.
-  Definition loc_38 : location_info := LocationInfo file_0 35 18 35 19.
-  Definition loc_39 : location_info := LocationInfo file_0 35 24 35 25.
-  Definition loc_40 : location_info := LocationInfo file_0 33 13 33 56.
-  Definition loc_41 : location_info := LocationInfo file_0 33 14 33 51.
-  Definition loc_42 : location_info := LocationInfo file_0 33 22 33 51.
-  Definition loc_43 : location_info := LocationInfo file_0 33 24 33 44.
-  Definition loc_44 : location_info := LocationInfo file_0 33 33 33 44.
-  Definition loc_45 : location_info := LocationInfo file_0 33 33 33 44.
-  Definition loc_46 : location_info := LocationInfo file_0 33 48 33 49.
-  Definition loc_47 : location_info := LocationInfo file_0 33 54 33 55.
-  Definition loc_50 : location_info := LocationInfo file_0 32 13 32 31.
-  Definition loc_51 : location_info := LocationInfo file_0 32 21 32 31.
-  Definition loc_52 : location_info := LocationInfo file_0 32 22 32 31.
-  Definition loc_55 : location_info := LocationInfo file_0 30 27 30 29.
-  Definition loc_58 : location_info := LocationInfo file_0 29 28 29 38.
+  Definition file_0 : string := "include/refinedc.h".
+  Definition file_1 : string := "examples/ocaml_runtime.c".
+  Definition loc_2 : location_info := LocationInfo file_0 50 2 50 47.
+  Definition loc_3 : location_info := LocationInfo file_0 50 9 50 46.
+  Definition loc_4 : location_info := LocationInfo file_0 50 9 50 32.
+  Definition loc_5 : location_info := LocationInfo file_0 50 33 50 37.
+  Definition loc_6 : location_info := LocationInfo file_0 50 33 50 37.
+  Definition loc_7 : location_info := LocationInfo file_0 50 39 50 45.
+  Definition loc_8 : location_info := LocationInfo file_0 50 39 50 45.
+  Definition loc_11 : location_info := LocationInfo file_1 29 2 29 39.
+  Definition loc_12 : location_info := LocationInfo file_1 30 2 30 30.
+  Definition loc_13 : location_info := LocationInfo file_1 32 2 32 32.
+  Definition loc_14 : location_info := LocationInfo file_1 33 2 33 57.
+  Definition loc_15 : location_info := LocationInfo file_1 35 2 35 28.
+  Definition loc_16 : location_info := LocationInfo file_1 36 2 36 28.
+  Definition loc_17 : location_info := LocationInfo file_1 38 2 38 54.
+  Definition loc_18 : location_info := LocationInfo file_1 39 2 39 28.
+  Definition loc_19 : location_info := LocationInfo file_1 40 2 40 39.
+  Definition loc_20 : location_info := LocationInfo file_1 40 9 40 37.
+  Definition loc_21 : location_info := LocationInfo file_1 40 9 40 23.
+  Definition loc_22 : location_info := LocationInfo file_1 40 9 40 23.
+  Definition loc_23 : location_info := LocationInfo file_1 40 10 40 23.
+  Definition loc_24 : location_info := LocationInfo file_1 40 10 40 23.
+  Definition loc_25 : location_info := LocationInfo file_1 40 27 40 37.
+  Definition loc_26 : location_info := LocationInfo file_1 39 9 39 26.
+  Definition loc_27 : location_info := LocationInfo file_1 39 9 39 20.
+  Definition loc_28 : location_info := LocationInfo file_1 39 10 39 14.
+  Definition loc_29 : location_info := LocationInfo file_1 39 10 39 14.
+  Definition loc_30 : location_info := LocationInfo file_1 39 18 39 19.
+  Definition loc_31 : location_info := LocationInfo file_1 39 24 39 26.
+  Definition loc_32 : location_info := LocationInfo file_1 38 33 38 53.
+  Definition loc_33 : location_info := LocationInfo file_1 38 51 38 53.
+  Definition loc_34 : location_info := LocationInfo file_1 38 51 38 53.
+  Definition loc_37 : location_info := LocationInfo file_1 36 9 36 26.
+  Definition loc_38 : location_info := LocationInfo file_1 36 10 36 20.
+  Definition loc_39 : location_info := LocationInfo file_1 36 11 36 15.
+  Definition loc_40 : location_info := LocationInfo file_1 36 11 36 15.
+  Definition loc_41 : location_info := LocationInfo file_1 36 18 36 19.
+  Definition loc_42 : location_info := LocationInfo file_1 36 24 36 25.
+  Definition loc_43 : location_info := LocationInfo file_1 35 9 35 26.
+  Definition loc_44 : location_info := LocationInfo file_1 35 10 35 20.
+  Definition loc_45 : location_info := LocationInfo file_1 35 11 35 15.
+  Definition loc_46 : location_info := LocationInfo file_1 35 11 35 15.
+  Definition loc_47 : location_info := LocationInfo file_1 35 18 35 19.
+  Definition loc_48 : location_info := LocationInfo file_1 35 24 35 25.
+  Definition loc_49 : location_info := LocationInfo file_1 33 13 33 56.
+  Definition loc_50 : location_info := LocationInfo file_1 33 14 33 51.
+  Definition loc_51 : location_info := LocationInfo file_1 33 22 33 51.
+  Definition loc_52 : location_info := LocationInfo file_1 33 24 33 44.
+  Definition loc_53 : location_info := LocationInfo file_1 33 33 33 44.
+  Definition loc_54 : location_info := LocationInfo file_1 33 33 33 44.
+  Definition loc_55 : location_info := LocationInfo file_1 33 48 33 49.
+  Definition loc_56 : location_info := LocationInfo file_1 33 54 33 55.
+  Definition loc_59 : location_info := LocationInfo file_1 32 13 32 31.
+  Definition loc_60 : location_info := LocationInfo file_1 32 21 32 31.
+  Definition loc_61 : location_info := LocationInfo file_1 32 22 32 31.
+  Definition loc_64 : location_info := LocationInfo file_1 30 27 30 29.
+  Definition loc_67 : location_info := LocationInfo file_1 29 28 29 38.
+
+  (* Definition of function [copy_alloc_id]. *)
+  Definition impl_copy_alloc_id : function := {|
+    f_args := [
+      ("to", it_layout uintptr_t);
+      ("from", void*)
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_2 ;
+        Return (LocInfoE loc_3 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_5 (use{it_layout uintptr_t} (LocInfoE loc_6 ("to")))) (LocInfoE loc_7 (use{void*} (LocInfoE loc_8 ("from"))))))
+      ]> $∅
+    )%E
+  |}.
 
   (* Definition of function [client]. *)
   Definition impl_client : function := {|
@@ -71,23 +96,23 @@ Section code.
     f_code := (
       <[ "#0" :=
         "large_int" <-{ it_layout u64 }
-          LocInfoE loc_58 (UnOp (CastOp $ IntOp u64) (IntOp u32) (LocInfoE loc_58 (i2v 3735928559 u32))) ;
+          LocInfoE loc_67 (UnOp (CastOp $ IntOp u64) (IntOp u32) (LocInfoE loc_67 (i2v 3735928559 u32))) ;
         "small_int" <-{ it_layout u32 }
-          LocInfoE loc_55 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_55 (i2v 42 i32))) ;
+          LocInfoE loc_64 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_64 (i2v 42 i32))) ;
         "v1" <-{ it_layout u64 }
-          LocInfoE loc_50 (UnOp (CastOp $ IntOp u64) (PtrOp) (LocInfoE loc_51 (&(LocInfoE loc_52 ("large_int"))))) ;
+          LocInfoE loc_59 (UnOp (CastOp $ IntOp u64) (PtrOp) (LocInfoE loc_60 (&(LocInfoE loc_61 ("large_int"))))) ;
         "v2" <-{ it_layout u64 }
-          LocInfoE loc_40 ((LocInfoE loc_41 (UnOp (CastOp $ IntOp u64) (IntOp u64) (LocInfoE loc_42 ((LocInfoE loc_43 (UnOp (CastOp $ IntOp u64) (IntOp u32) (LocInfoE loc_44 (use{it_layout u32} (LocInfoE loc_45 ("small_int")))))) <<{IntOp u64, IntOp u64} (LocInfoE loc_46 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_46 (i2v 1 i32)))))))) +{IntOp u64, IntOp u64} (LocInfoE loc_47 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_47 (i2v 1 i32))))) ;
-        locinfo: loc_6 ;
-        assert: (LocInfoE loc_34 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_34 ((LocInfoE loc_35 ((LocInfoE loc_36 (use{it_layout u64} (LocInfoE loc_37 ("v1")))) &{IntOp u64, IntOp u64} (LocInfoE loc_38 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_38 (i2v 1 i32)))))) ={IntOp u64, IntOp u64} (LocInfoE loc_39 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_39 (i2v 0 i32)))))))) ;
-        locinfo: loc_7 ;
-        assert: (LocInfoE loc_28 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_28 ((LocInfoE loc_29 ((LocInfoE loc_30 (use{it_layout u64} (LocInfoE loc_31 ("v2")))) &{IntOp u64, IntOp u64} (LocInfoE loc_32 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_32 (i2v 1 i32)))))) !={IntOp u64, IntOp u64} (LocInfoE loc_33 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_33 (i2v 0 i32)))))))) ;
+          LocInfoE loc_49 ((LocInfoE loc_50 (UnOp (CastOp $ IntOp u64) (IntOp u64) (LocInfoE loc_51 ((LocInfoE loc_52 (UnOp (CastOp $ IntOp u64) (IntOp u32) (LocInfoE loc_53 (use{it_layout u32} (LocInfoE loc_54 ("small_int")))))) <<{IntOp u64, IntOp u64} (LocInfoE loc_55 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_55 (i2v 1 i32)))))))) +{IntOp u64, IntOp u64} (LocInfoE loc_56 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_56 (i2v 1 i32))))) ;
+        locinfo: loc_15 ;
+        assert: (LocInfoE loc_43 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_43 ((LocInfoE loc_44 ((LocInfoE loc_45 (use{it_layout u64} (LocInfoE loc_46 ("v1")))) &{IntOp u64, IntOp u64} (LocInfoE loc_47 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_47 (i2v 1 i32)))))) ={IntOp u64, IntOp u64} (LocInfoE loc_48 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_48 (i2v 0 i32)))))))) ;
+        locinfo: loc_16 ;
+        assert: (LocInfoE loc_37 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_37 ((LocInfoE loc_38 ((LocInfoE loc_39 (use{it_layout u64} (LocInfoE loc_40 ("v2")))) &{IntOp u64, IntOp u64} (LocInfoE loc_41 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_41 (i2v 1 i32)))))) !={IntOp u64, IntOp u64} (LocInfoE loc_42 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_42 (i2v 0 i32)))))))) ;
         "large_int_ptr" <-{ void* }
-          LocInfoE loc_23 (UnOp (CastOp $ PtrOp) (IntOp u64) (LocInfoE loc_24 (use{it_layout u64} (LocInfoE loc_25 ("v1"))))) ;
-        locinfo: loc_9 ;
-        assert: (LocInfoE loc_17 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_17 ((LocInfoE loc_18 ((LocInfoE loc_19 (use{it_layout u64} (LocInfoE loc_20 ("v2")))) >>{IntOp u64, IntOp u64} (LocInfoE loc_21 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_21 (i2v 1 i32)))))) ={IntOp u64, IntOp u64} (LocInfoE loc_22 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_22 (i2v 42 i32)))))))) ;
-        locinfo: loc_10 ;
-        assert: (LocInfoE loc_11 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_11 ((LocInfoE loc_12 (use{it_layout u64} (LocInfoE loc_14 (!{void*} (LocInfoE loc_15 ("large_int_ptr")))))) ={IntOp u64, IntOp u64} (LocInfoE loc_16 (UnOp (CastOp $ IntOp u64) (IntOp u32) (LocInfoE loc_16 (i2v 3735928559 u32)))))))) ;
+          LocInfoE loc_32 (UnOp (CastOp $ PtrOp) (IntOp u64) (LocInfoE loc_33 (use{it_layout u64} (LocInfoE loc_34 ("v1"))))) ;
+        locinfo: loc_18 ;
+        assert: (LocInfoE loc_26 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_26 ((LocInfoE loc_27 ((LocInfoE loc_28 (use{it_layout u64} (LocInfoE loc_29 ("v2")))) >>{IntOp u64, IntOp u64} (LocInfoE loc_30 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_30 (i2v 1 i32)))))) ={IntOp u64, IntOp u64} (LocInfoE loc_31 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_31 (i2v 42 i32)))))))) ;
+        locinfo: loc_19 ;
+        assert: (LocInfoE loc_20 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_20 ((LocInfoE loc_21 (use{it_layout u64} (LocInfoE loc_23 (!{void*} (LocInfoE loc_24 ("large_int_ptr")))))) ={IntOp u64, IntOp u64} (LocInfoE loc_25 (UnOp (CastOp $ IntOp u64) (IntOp u32) (LocInfoE loc_25 (i2v 3735928559 u32)))))))) ;
         Return (VOID)
       ]> $∅
     )%E