add length function for singly linked list

tutorial/proofs/t03_list/generated_proof_length.v

+From refinedc.typing Require Import typing.
+From refinedc.tutorial.t03_list Require Import generated_code.
+From refinedc.tutorial.t03_list Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [tutorial/t03_list.c]. *)
+Section proof_length.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [length]. *)
+  Lemma type_length :
+    ⊢ typed_function impl_length type_of_length.
+  Proof.
+    start_function "length" ([p l]) => arg_p local_len.
+    split_blocks ((
+      <[ "#1" :=
+        ∃ q : loc,
+        ∃ l1 : list type,
+        arg_p ◁ₗ (q @ (&own (l1 @ (list_t)))) ∗
+        local_len ◁ₗ ((length l - length l1) @ (int (size_t))) ∗
+        (p ◁ₗ (wand (q ◁ₗ l1 @ list_t) (l @ (list_t))))
+    ]> $
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "length" "#0".
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "length" "#1".
+    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
+    all: print_sidecondition_goal "length".
+  Qed.
+End proof_length.

tutorial/proofs/t03_list/generated_spec.v

@@ -122,6 +122,11 @@ Section spec.
     fn(∀ l : (list type); (l @ (list_t)); True)
       → ∃ () : (), ((rev l) @ (list_t)); True.
 
+  (* Specifications for function [length]. *)
+  Definition type_of_length :=
+    fn(∀ (p, l) : loc * (list type); (p @ (&own (l @ (list_t)))); ⌜length l <= max_int size_t⌝)
+      → ∃ () : (), ((length l) @ (int (size_t))); (p ◁ₗ (l @ (list_t))).
+
   (* Specifications for function [append]. *)
   Definition type_of_append :=
     fn(∀ (p, l1, l2) : loc * (list type) * (list type); (p @ (&own (l1 @ (list_t)))), (l2 @ (list_t)); True)

tutorial/proofs/t03_list/proof_files

@@ -5,6 +5,7 @@ generated_proof_free.v
 generated_proof_free_array.v
 generated_proof_init.v
 generated_proof_is_empty.v
+generated_proof_length.v
 generated_proof_member.v
 generated_proof_pop.v
 generated_proof_push.v

tutorial/t03_list.c

@@ -80,6 +80,23 @@ list_t reverse (list_t p) {
     return w;
 }
 
+[[rc::parameters("p : loc", "l : {list type}")]]
+[[rc::args("p @ &own<l @ list_t>")]]
+[[rc::requires("{length l <= max_int size_t}")]]
+[[rc::returns("{length l} @ int<size_t>")]]
+[[rc::ensures("p @ &own<l @ list_t>")]]
+size_t length (list_t *p) {
+  size_t len = 0;
+  [[rc::exists("q : loc", "l1 : {list type}")]]
+  [[rc::inv_vars("p : q @ &own<l1 @ list_t>", "len : {length l - length l1} @ int<size_t>")]]
+  [[rc::constraints("p @ &own<wand<{q ◁ₗ l1 @ list_t}, l @ list_t>>")]]
+  while (*p != NULL) {
+    p = &(*p)->tail;
+    len += 1;
+  }
+  return len;
+}
+
 [[rc::parameters("p : loc", "l1 : {list type}", "l2 : {list type}")]]
 [[rc::args("p @ &own<l1 @ list_t>", "l2 @ list_t")]]
 [[rc::ensures("p @ &own<{l1 ++ l2} @ list_t>")]]