added test function for binary search

examples/binary_search.c

 #include <stddef.h>
 #include <stdbool.h>
 #include <refinedc.h>
+#include <alloc.h>
 
 //@rc::import binary_search_extra from refinedc.examples.binary_search
 
 typedef bool (*comp_fn)(void *, void *);
 
-[[rc::parameters("R: {Z → Z → Prop}", "ls : {list Z}", "x : Z", "p : loc", "ty : {Z → type}")]]
-[[rc::args("p @ &own<array<LPtr, {(fun x => &own (ty x) : type) <$> ls}>>", "{length ls} @ int<i32>",
-           "&own<{ty x}>", "function_ptr<{fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝}>")]]
+[[rc::parameters("R : {Z → Z → Prop}", "ls : {list Z}", "x : Z", "p : loc", "ty : {Z → type}", "px : loc")]]
+[[rc::args("function_ptr<{fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝}>",
+      "p @ &own<array<LPtr, {(fun x => &own (ty x) : type) <$> ls}>>", "{length ls} @ int<i32>", "px @ &own<{ty x}>")]]
 [[rc::requires("{StronglySorted R ls}", "{Transitive R}")]]
 [[rc::exists("n : nat")]]
 [[rc::returns("n @ int<i32>")]]
 [[rc::ensures("{∀ i y, (i < n)%nat → ls !! i = Some y → R y x}",
               "{∀ i y, (n ≤ i)%nat → ls !! i = Some y → ¬ R y x}")]]
 [[rc::ensures("p @ &own<array<LPtr, {(fun x => &own (ty x) : type) <$> ls}>>")]]
+[[rc::ensures("px @ &own<{ty x}>")]]
 [[rc::tactics("all: try by [revert select (∀ i j, _ → _ → ¬ R _ _); apply; [| done];solve_goal].")]]
 [[rc::tactics("all: try by apply: (binary_search_cond_1 y); solve_goal.")]]
 [[rc::tactics("all: try by apply: (binary_search_cond_2 y); solve_goal.")]]
-int binary_search(void **xs, int n, void *x, comp_fn comp) {
+int binary_search(comp_fn comp, void **xs, int n, void *x) {
   int l = 0, r = n;
   [[rc::exists("vl : nat", "vr : nat")]]
   [[rc::inv_vars("l : vl @ int<i32>", "r : vr @ int<i32>")]]
@@ -35,3 +37,41 @@ int binary_search(void **xs, int n, void *x, comp_fn comp) {
   }
   return l;
 }
+
+[[rc::parameters("x : Z", "y : Z", "px : loc", "py : loc")]]
+[[rc::args("px @ &own<x @ int<size_t>>", "py @ &own<y @ int<size_t>>")]]
+[[rc::exists("b : bool")]]
+[[rc::returns("b @ boolean<bool_it>")]]
+[[rc::ensures("px @ &own<x @ int<size_t>>", "py @ &own<y @ int<size_t>>", "{b ↔ Z.le x y}")]]
+bool compare_int(void *x, void *y) {
+  size_t *xi = x, *yi = y;
+  return *xi <= *yi;
+}
+
+[[rc::requires("[alloc_initialized]")]]
+[[rc::tactics("all: try by repeat constructor; lia.")]]
+[[rc::tactics("all: try by apply _.")]]
+[[rc::tactics("all: try by do 4 (destruct x'; [ naive_solver lia |]); exfalso; apply: (H0 3%nat) => //; lia.")]]
+void test() {
+  size_t *ptrs[5];
+  ptrs[0] = alloc(sizeof(size_t));
+  ptrs[1] = alloc(sizeof(size_t));
+  ptrs[2] = alloc(sizeof(size_t));
+  ptrs[3] = alloc(sizeof(size_t));
+  ptrs[4] = alloc(sizeof(size_t));
+  *ptrs[0] = 0;
+  *ptrs[1] = 1;
+  *ptrs[2] = 2;
+  *ptrs[3] = 3;
+  *ptrs[4] = 4;
+
+  size_t needle = 2;
+  int res = binary_search(compare_int, (void **)ptrs, 5, &needle);
+  assert(res == 3);
+
+  free(sizeof(size_t), ptrs[0]);
+  free(sizeof(size_t), ptrs[1]);
+  free(sizeof(size_t), ptrs[2]);
+  free(sizeof(size_t), ptrs[3]);
+  free(sizeof(size_t), ptrs[4]);
+}

examples/proofs/binary_search/generated_proof_binary_search.v

@@ -12,15 +12,15 @@ Section proof_binary_search.
   Lemma type_binary_search :
     ⊢ typed_function impl_binary_search type_of_binary_search.
   Proof.
-    start_function "binary_search" ([[[[R ls] x] p] ty]) => arg_xs arg_n arg_x arg_comp local_r local_l local_k.
+    start_function "binary_search" ([[[[[R ls] x] p] ty] px]) => arg_comp arg_xs arg_n arg_x local_r local_l local_k.
     split_blocks ((
       <[ "#1" :=
         ∃ vl : nat,
         ∃ vr : nat,
+        arg_comp ◁ₗ (function_ptr (fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝)) ∗
         arg_xs ◁ₗ (p @ (&own (array (LPtr) ((fun x => &own (ty x) : type) <$> ls)))) ∗
         arg_n ◁ₗ ((length ls) @ (int (i32))) ∗
-        arg_x ◁ₗ (&own (ty x)) ∗
-        arg_comp ◁ₗ (function_ptr (fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝)) ∗
+        arg_x ◁ₗ (px @ (&own (ty x))) ∗
         local_k ◁ₗ uninit (it_layout i32) ∗
         local_l ◁ₗ (vl @ (int (i32))) ∗
         local_r ◁ₗ (vr @ (int (i32))) ∗

examples/proofs/binary_search/generated_proof_compare_int.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.binary_search Require Import generated_code.
+From refinedc.examples.binary_search Require Import generated_spec.
+From refinedc.examples.binary_search Require Import binary_search_extra.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/binary_search.c]. *)
+Section proof_compare_int.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [compare_int]. *)
+  Lemma type_compare_int :
+    ⊢ typed_function impl_compare_int type_of_compare_int.
+  Proof.
+    start_function "compare_int" ([[[x y] px] py]) => arg_x arg_y local_xi local_yi.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "compare_int" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "compare_int".
+  Qed.
+End proof_compare_int.

examples/proofs/binary_search/generated_proof_test.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.binary_search Require Import generated_code.
+From refinedc.examples.binary_search Require Import generated_spec.
+From refinedc.examples.binary_search Require Import binary_search_extra.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/binary_search.c]. *)
+Section proof_test.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [test]. *)
+  Lemma type_test (alloc binary_search compare_int free : loc) :
+    alloc ◁ᵥ alloc @ function_ptr type_of_alloc -∗
+    binary_search ◁ᵥ binary_search @ function_ptr type_of_binary_search -∗
+    compare_int ◁ᵥ compare_int @ function_ptr type_of_compare_int -∗
+    free ◁ᵥ free @ function_ptr type_of_free -∗
+    typed_function (impl_test alloc binary_search compare_int free) type_of_test.
+  Proof.
+    start_function "test" ([]) => local_res local_ptrs local_needle.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "test" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: try by repeat constructor; lia.
+    all: try by apply _.
+    all: try by do 4 (destruct x'; [ naive_solver lia |]); exfalso; apply: (H0 3%nat) => //; lia.
+    all: print_sidecondition_goal "test".
+  Qed.
+End proof_test.

examples/proofs/binary_search/generated_spec.v

@@ -7,10 +7,43 @@ Set Default Proof Using "Type".
 Section spec.
   Context `{!typeG Σ} `{!globalG Σ}.
 
+  (* Inlined code. *)
+
+  Definition alloc_initialized := initialized "allocator_state" ().
+
   (* Type definitions. *)
 
+  (* 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))
+      → ∃ () : (), (&own (uninit (Layout size 3))); True.
+
+  (* Specifications for function [free]. *)
+  Definition type_of_free :=
+    fn(∀ size : nat; (size @ (int (size_t))), (&own (uninit (Layout size 3))); (alloc_initialized) ∗ ⌜(8 | size)⌝)
+      → ∃ () : (), (void); True.
+
+  (* Specifications for function [alloc_array]. *)
+  Definition type_of_alloc_array :=
+    fn(∀ (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); ⌜size * n + 16 ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); True.
+
+  (* Specifications for function [free_array]. *)
+  Definition type_of_free_array :=
+    fn(∀ (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); ⌜size * n ≤ max_int size_t⌝ ∗ ⌜(8 | size)⌝ ∗ (alloc_initialized))
+      → ∃ () : (), (void); True.
+
   (* Specifications for function [binary_search]. *)
   Definition type_of_binary_search :=
-    fn(∀ (R, ls, x, p, ty) : (Z → Z → Prop) * (list Z) * Z * loc * (Z → type); (p @ (&own (array (LPtr) ((fun x => &own (ty x) : type) <$> ls)))), ((length ls) @ (int (i32))), (&own (ty x)), (function_ptr (fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝)); ⌜StronglySorted R ls⌝ ∗ ⌜Transitive R⌝)
-      → ∃ n : nat, (n @ (int (i32))); ⌜∀ i y, (i < n)%nat → ls !! i = Some y → R y x⌝ ∗ ⌜∀ i y, (n ≤ i)%nat → ls !! i = Some y → ¬ R y x⌝ ∗ (p ◁ₗ (array (LPtr) ((fun x => &own (ty x) : type) <$> ls))).
+    fn(∀ (R, ls, x, p, ty, px) : (Z → Z → Prop) * (list Z) * Z * loc * (Z → type) * loc; (function_ptr (fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝)), (p @ (&own (array (LPtr) ((fun x => &own (ty x) : type) <$> ls)))), ((length ls) @ (int (i32))), (px @ (&own (ty x))); ⌜StronglySorted R ls⌝ ∗ ⌜Transitive R⌝)
+      → ∃ n : nat, (n @ (int (i32))); ⌜∀ i y, (i < n)%nat → ls !! i = Some y → R y x⌝ ∗ ⌜∀ i y, (n ≤ i)%nat → ls !! i = Some y → ¬ R y x⌝ ∗ (p ◁ₗ (array (LPtr) ((fun x => &own (ty x) : type) <$> ls))) ∗ (px ◁ₗ (ty x)).
+
+  (* Specifications for function [compare_int]. *)
+  Definition type_of_compare_int :=
+    fn(∀ (x, y, px, py) : Z * Z * loc * loc; (px @ (&own (x @ (int (size_t))))), (py @ (&own (y @ (int (size_t))))); True)
+      → ∃ b : bool, (b @ (boolean (bool_it))); (px ◁ₗ (x @ (int (size_t)))) ∗ (py ◁ₗ (y @ (int (size_t)))) ∗ ⌜b ↔ Z.le x y⌝.
+
+  (* Specifications for function [test]. *)
+  Definition type_of_test :=
+    fn(∀ () : (); (alloc_initialized)) → ∃ () : (), (void); True.
 End spec.

examples/proofs/binary_search/proof_files

+generated_proof_alloc.v
+generated_proof_alloc_array.v
 generated_proof_binary_search.v
+generated_proof_compare_int.v
+generated_proof_free.v
+generated_proof_free_array.v
+generated_proof_test.v

theories/lithium/interpreter.v

@@ -459,6 +459,7 @@ Ltac liExist protect :=
         custom_exist_tac A protect
       | lazymatch A with
         | TCForall2 _ _ _ => eexists _
+        (* | Type => eexists _ *)
         | @eq ?B ?x _ => exists (@eq_refl B x)
         | prod _ _ => apply: tac_exist_prod
         | sigT _ => apply: tac_exist_sigT

theories/typing/array.v

@@ -128,9 +128,17 @@ Section type.
     simplify_hyp (l ◁ₗ{β} uninit (mk_array_layout ly n)) T.
   Proof. iIntros "[% HT] Hl". iApply "HT". rewrite array_replicate_uninit_equiv // {1}/ly_size/=. Qed.
   Global Instance simplify_hyp_uninit_array_inst ly l β n:
-    SimplifyHyp (l ◁ₗ{β} uninit (mk_array_layout ly n)) (Some 0%N) :=
+    SimplifyHypPlace l β (uninit (mk_array_layout ly n)) (Some 50%N) :=
     λ T, i2p (simplify_hyp_uninit_array ly l β T n).
 
+  Lemma simplify_goal_uninit_array ly l β T n:
+    (⌜layout_wf ly⌝ ∗ T (l ◁ₗ{β} array ly (replicate n (uninit ly)))) -∗
+     simplify_goal (l ◁ₗ{β} uninit (mk_array_layout ly n)) T.
+  Proof. iIntros "[% HT]". iExists _. iFrame. iIntros "?". rewrite array_replicate_uninit_equiv //. Qed.
+  Global Instance simplify_goal_uninit_array_inst ly l β n:
+    SimplifyGoalPlace l β (uninit (mk_array_layout ly n)) (Some 50%N) :=
+    λ T, i2p (simplify_goal_uninit_array ly l β T n).
+
   Lemma subsume_uninit_array_replicate l β T n (ly1 : layout) ly2:
     ⌜layout_wf ly2⌝ ∗ ⌜ly1 = mk_array_layout ly2 n⌝ ∗ T -∗
     subsume (l ◁ₗ{β} uninit ly1) (l ◁ₗ{β} array ly2 (replicate n (uninit ly2))) T.