update paper_example_2 to match paper

examples/paper_example_2_2.c

@@ -16,8 +16,9 @@
 
 typedef struct
 [[rc::refined_by("s: {gmultiset nat}")]]
-[[rc::ptr_type("chunks_t : {s ≠ ∅} @ optional<&own<...>, null>")]]
-[[rc::exists  ("n : nat", "tail : {gmultiset nat}")]]
+[[rc::ptr_type("chunks_t:"
+               "{s ≠ ∅} @ optional<&own<...>, null>")]]
+[[rc::exists  ("n: nat", "tail: {gmultiset nat}")]]
 [[rc::size    ("n")]]
 [[rc::constraints("{s = {[n]} ⊎ tail}",
                   "{∀ k, k ∈ tail → n ≤ k}")]]
@@ -26,25 +27,24 @@ chunk {
   [[rc::field("tail @ chunks_t")]] struct chunk* next;
 }* chunks_t;
 
-[[rc::parameters("s : {gmultiset nat}", "p : loc", "q : loc", "n : nat")]]
-[[rc::args      ("p @ &own<s @ chunks_t>", "q @ &own<uninit<n>>",
+[[rc::parameters("s: {gmultiset nat}", "p: loc", "n: nat")]]
+[[rc::args      ("p @ &own<s @ chunks_t>", "&own<uninit<n>>",
                  "n @ int<size_t>")]]
-[[rc::requires  ("{sizeof struct_chunk ≤ n}")]]
+[[rc::requires  ("{sizeof(struct_chunk) ≤ n}")]]
 [[rc::ensures   ("own p : {{[n]} ⊎ s} @ chunks_t")]]
 [[rc::tactics   ("all: multiset_solver.")]]
-void free(chunks_t* list, void *data, size_t size) {
-  chunks_t *cur = list;
-  [[rc::exists  ("cp : loc", "cs : {gmultiset nat}")]]
-  [[rc::inv_vars("cur : cp @ &own<cs @ chunks_t>")]]
-  [[rc::inv_vars("list : p @ &own<"
-                   "wand<{cp ◁ₗ ({[n]} ⊎ cs) @ chunks_t}, "
-                   "{{[n]} ⊎ s} @ chunks_t>>")]]
+void free(chunks_t* list, void* data, size_t sz) {
+  chunks_t* cur = list;
+  [[rc::exists  ("cp: loc", "cs: {gmultiset nat}")]]
+  [[rc::inv_vars("cur: cp @ &own<cs @ chunks_t>")]]
+  [[rc::inv_vars("list:"
+       "p @ &own<wand<{cp ◁ₗ ({[n]} ⊎ cs) @ chunks_t},"
+                     "{{[n]} ⊎ s} @ chunks_t>>")]]
   while(*cur != NULL) {
-    if(size <= (*cur)->size) break;
+    if(sz <= (*cur)->size) break;
     cur = &(*cur)->next;
   }
   chunks_t entry = data;
-  entry->size = size;
-  entry->next = *cur;
+  entry->size = sz; entry->next = *cur;
   *cur = entry;
 }

examples/proofs/paper_example_2_2/generated_code.v

@@ -6,62 +6,62 @@ Set Default Proof Using "Type".
 (* Generated from [examples/paper_example_2_2.c]. *)
 Section code.
   Definition file_0 : string := "examples/paper_example_2_2.c".
-  Definition loc_2 : location_info := LocationInfo file_0 36 2 36 23.
-  Definition loc_3 : location_info := LocationInfo file_0 42 2 45 3.
-  Definition loc_4 : location_info := LocationInfo file_0 46 2 46 24.
-  Definition loc_5 : location_info := LocationInfo file_0 47 2 47 21.
-  Definition loc_6 : location_info := LocationInfo file_0 48 2 48 21.
+  Definition loc_2 : location_info := LocationInfo file_0 37 2 37 23.
+  Definition loc_3 : location_info := LocationInfo file_0 43 2 46 3.
+  Definition loc_4 : location_info := LocationInfo file_0 47 2 47 24.
+  Definition loc_5 : location_info := LocationInfo file_0 48 2 48 19.
+  Definition loc_6 : location_info := LocationInfo file_0 48 20 48 39.
   Definition loc_7 : location_info := LocationInfo file_0 49 2 49 15.
   Definition loc_8 : location_info := LocationInfo file_0 49 2 49 6.
   Definition loc_9 : location_info := LocationInfo file_0 49 3 49 6.
   Definition loc_10 : location_info := LocationInfo file_0 49 3 49 6.
   Definition loc_11 : location_info := LocationInfo file_0 49 9 49 14.
   Definition loc_12 : location_info := LocationInfo file_0 49 9 49 14.
-  Definition loc_13 : location_info := LocationInfo file_0 48 2 48 13.
-  Definition loc_14 : location_info := LocationInfo file_0 48 2 48 7.
-  Definition loc_15 : location_info := LocationInfo file_0 48 2 48 7.
-  Definition loc_16 : location_info := LocationInfo file_0 48 16 48 20.
-  Definition loc_17 : location_info := LocationInfo file_0 48 16 48 20.
-  Definition loc_18 : location_info := LocationInfo file_0 48 17 48 20.
-  Definition loc_19 : location_info := LocationInfo file_0 48 17 48 20.
-  Definition loc_20 : location_info := LocationInfo file_0 47 2 47 13.
-  Definition loc_21 : location_info := LocationInfo file_0 47 2 47 7.
-  Definition loc_22 : location_info := LocationInfo file_0 47 2 47 7.
-  Definition loc_23 : location_info := LocationInfo file_0 47 16 47 20.
-  Definition loc_24 : location_info := LocationInfo file_0 47 16 47 20.
-  Definition loc_25 : location_info := LocationInfo file_0 46 19 46 23.
-  Definition loc_26 : location_info := LocationInfo file_0 46 19 46 23.
-  Definition loc_29 : location_info := LocationInfo file_0 42 2 45 3.
-  Definition loc_30 : location_info := LocationInfo file_0 42 32 45 3.
-  Definition loc_31 : location_info := LocationInfo file_0 43 4 43 35.
-  Definition loc_32 : location_info := LocationInfo file_0 44 4 44 24.
-  Definition loc_33 : location_info := LocationInfo file_0 42 2 45 3.
-  Definition loc_34 : location_info := LocationInfo file_0 42 2 45 3.
-  Definition loc_35 : location_info := LocationInfo file_0 44 4 44 7.
-  Definition loc_36 : location_info := LocationInfo file_0 44 10 44 23.
-  Definition loc_37 : location_info := LocationInfo file_0 44 11 44 23.
-  Definition loc_38 : location_info := LocationInfo file_0 44 11 44 17.
-  Definition loc_39 : location_info := LocationInfo file_0 44 11 44 17.
-  Definition loc_40 : location_info := LocationInfo file_0 44 13 44 16.
-  Definition loc_41 : location_info := LocationInfo file_0 44 13 44 16.
-  Definition loc_42 : location_info := LocationInfo file_0 43 29 43 35.
-  Definition loc_44 : location_info := LocationInfo file_0 43 7 43 27.
-  Definition loc_45 : location_info := LocationInfo file_0 43 7 43 11.
-  Definition loc_46 : location_info := LocationInfo file_0 43 7 43 11.
-  Definition loc_47 : location_info := LocationInfo file_0 43 15 43 27.
-  Definition loc_48 : location_info := LocationInfo file_0 43 15 43 27.
-  Definition loc_49 : location_info := LocationInfo file_0 43 15 43 21.
-  Definition loc_50 : location_info := LocationInfo file_0 43 15 43 21.
-  Definition loc_51 : location_info := LocationInfo file_0 43 17 43 20.
-  Definition loc_52 : location_info := LocationInfo file_0 43 17 43 20.
-  Definition loc_53 : location_info := LocationInfo file_0 42 8 42 30.
-  Definition loc_54 : location_info := LocationInfo file_0 42 8 42 12.
-  Definition loc_55 : location_info := LocationInfo file_0 42 8 42 12.
-  Definition loc_56 : location_info := LocationInfo file_0 42 9 42 12.
-  Definition loc_57 : location_info := LocationInfo file_0 42 9 42 12.
-  Definition loc_58 : location_info := LocationInfo file_0 42 16 42 30.
-  Definition loc_59 : location_info := LocationInfo file_0 36 18 36 22.
-  Definition loc_60 : location_info := LocationInfo file_0 36 18 36 22.
+  Definition loc_13 : location_info := LocationInfo file_0 48 20 48 31.
+  Definition loc_14 : location_info := LocationInfo file_0 48 20 48 25.
+  Definition loc_15 : location_info := LocationInfo file_0 48 20 48 25.
+  Definition loc_16 : location_info := LocationInfo file_0 48 34 48 38.
+  Definition loc_17 : location_info := LocationInfo file_0 48 34 48 38.
+  Definition loc_18 : location_info := LocationInfo file_0 48 35 48 38.
+  Definition loc_19 : location_info := LocationInfo file_0 48 35 48 38.
+  Definition loc_20 : location_info := LocationInfo file_0 48 2 48 13.
+  Definition loc_21 : location_info := LocationInfo file_0 48 2 48 7.
+  Definition loc_22 : location_info := LocationInfo file_0 48 2 48 7.
+  Definition loc_23 : location_info := LocationInfo file_0 48 16 48 18.
+  Definition loc_24 : location_info := LocationInfo file_0 48 16 48 18.
+  Definition loc_25 : location_info := LocationInfo file_0 47 19 47 23.
+  Definition loc_26 : location_info := LocationInfo file_0 47 19 47 23.
+  Definition loc_29 : location_info := LocationInfo file_0 43 2 46 3.
+  Definition loc_30 : location_info := LocationInfo file_0 43 32 46 3.
+  Definition loc_31 : location_info := LocationInfo file_0 44 4 44 33.
+  Definition loc_32 : location_info := LocationInfo file_0 45 4 45 24.
+  Definition loc_33 : location_info := LocationInfo file_0 43 2 46 3.
+  Definition loc_34 : location_info := LocationInfo file_0 43 2 46 3.
+  Definition loc_35 : location_info := LocationInfo file_0 45 4 45 7.
+  Definition loc_36 : location_info := LocationInfo file_0 45 10 45 23.
+  Definition loc_37 : location_info := LocationInfo file_0 45 11 45 23.
+  Definition loc_38 : location_info := LocationInfo file_0 45 11 45 17.
+  Definition loc_39 : location_info := LocationInfo file_0 45 11 45 17.
+  Definition loc_40 : location_info := LocationInfo file_0 45 13 45 16.
+  Definition loc_41 : location_info := LocationInfo file_0 45 13 45 16.
+  Definition loc_42 : location_info := LocationInfo file_0 44 27 44 33.
+  Definition loc_44 : location_info := LocationInfo file_0 44 7 44 25.
+  Definition loc_45 : location_info := LocationInfo file_0 44 7 44 9.
+  Definition loc_46 : location_info := LocationInfo file_0 44 7 44 9.
+  Definition loc_47 : location_info := LocationInfo file_0 44 13 44 25.
+  Definition loc_48 : location_info := LocationInfo file_0 44 13 44 25.
+  Definition loc_49 : location_info := LocationInfo file_0 44 13 44 19.
+  Definition loc_50 : location_info := LocationInfo file_0 44 13 44 19.
+  Definition loc_51 : location_info := LocationInfo file_0 44 15 44 18.
+  Definition loc_52 : location_info := LocationInfo file_0 44 15 44 18.
+  Definition loc_53 : location_info := LocationInfo file_0 43 8 43 30.
+  Definition loc_54 : location_info := LocationInfo file_0 43 8 43 12.
+  Definition loc_55 : location_info := LocationInfo file_0 43 8 43 12.
+  Definition loc_56 : location_info := LocationInfo file_0 43 9 43 12.
+  Definition loc_57 : location_info := LocationInfo file_0 43 9 43 12.
+  Definition loc_58 : location_info := LocationInfo file_0 43 16 43 30.
+  Definition loc_59 : location_info := LocationInfo file_0 37 18 37 22.
+  Definition loc_60 : location_info := LocationInfo file_0 37 18 37 22.
 
   (* Definition of struct [atomic_flag]. *)
   Program Definition struct_atomic_flag := {|
@@ -93,7 +93,7 @@ Section code.
     f_args := [
       ("list", void*);
       ("data", void*);
-      ("size", it_layout size_t)
+      ("sz", it_layout size_t)
     ];
     f_local_vars := [
       ("cur", void*);
@@ -118,7 +118,7 @@ Section code.
       ]> $
       <[ "#2" :=
         locinfo: loc_44 ;
-        if: LocInfoE loc_44 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_44 ((LocInfoE loc_45 (use{it_layout size_t} (LocInfoE loc_46 ("size")))) ≤{IntOp size_t, IntOp size_t} (LocInfoE loc_47 (use{it_layout size_t} (LocInfoE loc_48 ((LocInfoE loc_49 (!{void*} (LocInfoE loc_51 (!{void*} (LocInfoE loc_52 ("cur")))))) at{struct_chunk} "size")))))))
+        if: LocInfoE loc_44 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_44 ((LocInfoE loc_45 (use{it_layout size_t} (LocInfoE loc_46 ("sz")))) ≤{IntOp size_t, IntOp size_t} (LocInfoE loc_47 (use{it_layout size_t} (LocInfoE loc_48 ((LocInfoE loc_49 (!{void*} (LocInfoE loc_51 (!{void*} (LocInfoE loc_52 ("cur")))))) at{struct_chunk} "size")))))))
         then
         Goto "#5"
         else
@@ -130,7 +130,7 @@ Section code.
           LocInfoE loc_25 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_25 (use{void*} (LocInfoE loc_26 ("data"))))) ;
         locinfo: loc_5 ;
         LocInfoE loc_20 ((LocInfoE loc_21 (!{void*} (LocInfoE loc_22 ("entry")))) at{struct_chunk} "size") <-{ it_layout size_t }
-          LocInfoE loc_23 (use{it_layout size_t} (LocInfoE loc_24 ("size"))) ;
+          LocInfoE loc_23 (use{it_layout size_t} (LocInfoE loc_24 ("sz"))) ;
         locinfo: loc_6 ;
         LocInfoE loc_13 ((LocInfoE loc_14 (!{void*} (LocInfoE loc_15 ("entry")))) at{struct_chunk} "next") <-{ void* }
           LocInfoE loc_16 (use{void*} (LocInfoE loc_18 (!{void*} (LocInfoE loc_19 ("cur"))))) ;

examples/proofs/paper_example_2_2/generated_proof_free.v

@@ -14,13 +14,13 @@ Section proof_free.
     ⊢ typed_function impl_free type_of_free.
   Proof.
     Open Scope printing_sugar.
-    start_function "free" ([[[s p] q] n]) => arg_list arg_data arg_size local_cur local_entry.
+    start_function "free" ([[s p] n]) => arg_list arg_data arg_sz local_cur local_entry.
     split_blocks ((
       <[ "#1" :=
         ∃ cp : loc,
         ∃ cs : gmultiset nat,
-        arg_data ◁ₗ (q @ (&own (uninit (n)))) ∗
-        arg_size ◁ₗ (n @ (int (size_t))) ∗
+        arg_data ◁ₗ (&own (uninit (n))) ∗
+        arg_sz ◁ₗ (n @ (int (size_t))) ∗
         local_entry ◁ₗ uninit void* ∗
         local_cur ◁ₗ (cp @ (&own (cs @ (chunks_t)))) ∗
         arg_list ◁ₗ (p @ (&own (wand (cp ◁ₗ ({[n]} ⊎ cs) @ chunks_t) (({[n]} ⊎ s) @ (chunks_t)))))

examples/proofs/paper_example_2_2/generated_spec.v

@@ -99,7 +99,7 @@ Section spec.
 
   (* Specifications for function [free]. *)
   Definition type_of_free :=
-    fn(∀ (s, p, q, n) : (gmultiset nat) * loc * loc * nat; (p @ (&own (s @ (chunks_t)))), (q @ (&own (uninit (n)))), (n @ (int (size_t))); ⌜sizeof struct_chunk ≤ n⌝)
+    fn(∀ (s, p, n) : (gmultiset nat) * loc * nat; (p @ (&own (s @ (chunks_t)))), (&own (uninit (n))), (n @ (int (size_t))); ⌜sizeof(struct_chunk) ≤ n⌝)
       → ∃ () : (), (void); (p ◁ₗ (({[n]} ⊎ s) @ (chunks_t))).
 End spec.