add example of length without pointer indirection

theories/typing/singleton.v

@@ -27,6 +27,17 @@ Section singleton_val.
     SimplifyHypVal v (singleton_val ly p) (Some 0%N) :=
     λ T, i2p (singleton_val_simplify v T ly p).
 
+  Lemma singleton_val_subsume_goal v v' ly ty `{!Movable ty} T:
+    (v ◁ᵥ ty -∗ ⌜ty.(ty_layout) = ly⌝ ∗ ⌜v = v'⌝ ∗ T) -∗
+    subsume (v ◁ᵥ ty) (v ◁ᵥ singleton_val ly v') T.
+  Proof.
+    iIntros "HT Hty". iDestruct (ty_size_eq with "Hty") as %Hly.
+    by iDestruct ("HT" with "Hty") as (<- ->) "$".
+  Qed.
+  Global Instance singleton_val_subsume_goal_inst v v' ly ty `{!Movable ty}:
+    SubsumeVal v ty (singleton_val ly v') :=
+    λ T, i2p (singleton_val_subsume_goal v v' ly ty T).
+
   Lemma singleton_val_merge v l ly T:
     (find_in_context (FindVal v) (λ ty:mtype, ⌜ty.(ty_layout) = ly⌝ ∗ (l ◁ₗ ty -∗ T))) -∗
       simplify_hyp (l ◁ₗ singleton_val ly v) T.

tutorial/proofs/t03_list/generated_proof_length_val_rec.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_val_rec.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [length_val_rec]. *)
+  Lemma type_length_val_rec (global_length_val_rec : loc) :
+    global_length_val_rec ◁ᵥ global_length_val_rec @ function_ptr type_of_length_val_rec -∗
+    typed_function (impl_length_val_rec global_length_val_rec) type_of_length_val_rec.
+  Proof.
+    start_function "length_val_rec" ([v l]) => arg_p.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "length_val_rec" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "length_val_rec".
+  Qed.
+End proof_length_val_rec.

tutorial/proofs/t03_list/generated_spec.v

@@ -127,6 +127,11 @@ Section spec.
     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 [length_val_rec]. *)
+  Definition type_of_length_val_rec :=
+    fn(∀ (v, l) : val * (list type); (singleton_val (LPtr) (v)); (v ◁ᵥ l @ list_t) ∗ ⌜length l <= max_int size_t⌝)
+      → ∃ () : (), ((length l) @ (int (size_t))); (v ◁ᵥ 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

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

tutorial/t03_list.c

@@ -97,6 +97,19 @@ size_t length (list_t *p) {
   return len;
 }
 
+[[rc::parameters("v : val", "l : {list type}")]]
+[[rc::args("singleton_val<LPtr, v>")]]
+[[rc::requires("[v ◁ᵥ l @ list_t]")]]
+[[rc::requires("{length l <= max_int size_t}")]]
+[[rc::returns("{length l} @ int<size_t>")]]
+[[rc::ensures("[v ◁ᵥ l @ list_t]")]]  // TODO: there should be nicer syntax for this
+size_t length_val_rec (list_t p) {
+  if(p == NULL) {
+    return 0;
+  }
+  return length_val_rec(p->tail) + 1;
+}
+
 [[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>")]]