Started with binary search

_CoqProject

@@ -34,3 +34,4 @@
 -Q _build/default/tutorial/adequacy refinedc.tutorial.adequacy
 -Q _build/default/tutorial/proofs/quicksort_solution refinedc.tutorial.quicksort_solution
 -Q _build/default/tutorial/proofs/quicksort_exercise refinedc.tutorial.quicksort_exercise
+-Q _build/default/examples/proofs/binary_search refinedc.examples.binary_search

examples/binary_search.c

+#include <stddef.h>
+#include <stdbool.h>
+#include <refinedc.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::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::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 l = 0, r = n;
+  [[rc::exists("vl : nat", "vr : nat")]]
+  [[rc::inv_vars("l : vl @ int<i32>", "r : vr @ int<i32>")]]
+  [[rc::constraints("{vl <= vr}", "{vr <= length ls}")]]
+  [[rc::constraints("{∀ i y, (i < vl)%nat → ls !! i = Some y → R y x}",
+                    "{∀ i y, (vr ≤ i)%nat → ls !! i = Some y → ¬ R y x}")]]
+  while(l < r) {
+    int k = l + (r - l) / 2;
+    if (comp(xs[k], x)) {
+      l = k + 1;
+      } else {
+      r = k;
+    }
+  }
+  return l;
+}

examples/proofs/binary_search/binary_search_extra.v

+From refinedc.lang Require Import base.
+
+Lemma binary_search_cond_1 {A} y R (l : list A) i j x z `{!Transitive R}:
+  StronglySorted R l → l !! i = Some x → l !! j = Some y → (i ≤ j)%nat → R y z → R x z.
+Proof.
+  move => ?????.
+  have [||||->|?]:= StronglySorted_lookup_le R l i j x y => //. by etrans.
+Qed.
+
+Lemma binary_search_cond_2 {A} y R (l : list A) i j x z `{!Transitive R}:
+  StronglySorted R l → l !! i = Some x → l !! j = Some y → (j ≤ i)%nat → ¬ R y z → ¬ R x z.
+Proof.
+  move => ???? Hneg. have [||||<-|?]:= StronglySorted_lookup_le R l j i y x => //.
+  contradict Hneg. by etrans.
+Qed.

examples/proofs/binary_search/dune

+; Generated by [refinedc], do not edit.
+(coq.theory
+ (flags -w -notation-overridden -w -redundant-canonical-projection)
+ (name refinedc.examples.binary_search)
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))

examples/proofs/binary_search/generated_code.v

+From refinedc.lang Require Export notation.
+From refinedc.lang Require Import tactics.
+From refinedc.typing Require Import annotations.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/binary_search.c]. *)
+Section code.
+  Definition file_0 : string := "examples/binary_search.c".
+  Definition loc_2 : location_info := LocationInfo file_0 22 2 22 19.
+  Definition loc_3 : location_info := LocationInfo file_0 28 2 35 3.
+  Definition loc_4 : location_info := LocationInfo file_0 36 2 36 11.
+  Definition loc_5 : location_info := LocationInfo file_0 36 9 36 10.
+  Definition loc_6 : location_info := LocationInfo file_0 36 9 36 10.
+  Definition loc_7 : location_info := LocationInfo file_0 28 2 35 3.
+  Definition loc_8 : location_info := LocationInfo file_0 28 15 35 3.
+  Definition loc_9 : location_info := LocationInfo file_0 29 4 29 28.
+  Definition loc_10 : location_info := LocationInfo file_0 30 4 34 5.
+  Definition loc_11 : location_info := LocationInfo file_0 28 2 35 3.
+  Definition loc_12 : location_info := LocationInfo file_0 28 2 35 3.
+  Definition loc_13 : location_info := LocationInfo file_0 30 24 32 7.
+  Definition loc_14 : location_info := LocationInfo file_0 31 6 31 16.
+  Definition loc_15 : location_info := LocationInfo file_0 31 6 31 7.
+  Definition loc_16 : location_info := LocationInfo file_0 31 10 31 15.
+  Definition loc_17 : location_info := LocationInfo file_0 31 10 31 11.
+  Definition loc_18 : location_info := LocationInfo file_0 31 10 31 11.
+  Definition loc_19 : location_info := LocationInfo file_0 31 14 31 15.
+  Definition loc_20 : location_info := LocationInfo file_0 32 13 34 5.
+  Definition loc_21 : location_info := LocationInfo file_0 33 6 33 12.
+  Definition loc_22 : location_info := LocationInfo file_0 33 6 33 7.
+  Definition loc_23 : location_info := LocationInfo file_0 33 10 33 11.
+  Definition loc_24 : location_info := LocationInfo file_0 33 10 33 11.
+  Definition loc_25 : location_info := LocationInfo file_0 30 8 30 22.
+  Definition loc_26 : location_info := LocationInfo file_0 30 8 30 12.
+  Definition loc_27 : location_info := LocationInfo file_0 30 8 30 12.
+  Definition loc_28 : location_info := LocationInfo file_0 30 8 30 12.
+  Definition loc_29 : location_info := LocationInfo file_0 30 13 30 18.
+  Definition loc_30 : location_info := LocationInfo file_0 30 13 30 18.
+  Definition loc_31 : location_info := LocationInfo file_0 30 13 30 18.
+  Definition loc_32 : location_info := LocationInfo file_0 30 13 30 15.
+  Definition loc_33 : location_info := LocationInfo file_0 30 13 30 15.
+  Definition loc_34 : location_info := LocationInfo file_0 30 16 30 17.
+  Definition loc_35 : location_info := LocationInfo file_0 30 16 30 17.
+  Definition loc_36 : location_info := LocationInfo file_0 30 20 30 21.
+  Definition loc_37 : location_info := LocationInfo file_0 30 20 30 21.
+  Definition loc_38 : location_info := LocationInfo file_0 29 12 29 27.
+  Definition loc_39 : location_info := LocationInfo file_0 29 12 29 13.
+  Definition loc_40 : location_info := LocationInfo file_0 29 12 29 13.
+  Definition loc_41 : location_info := LocationInfo file_0 29 16 29 27.
+  Definition loc_42 : location_info := LocationInfo file_0 29 16 29 23.
+  Definition loc_43 : location_info := LocationInfo file_0 29 17 29 18.
+  Definition loc_44 : location_info := LocationInfo file_0 29 17 29 18.
+  Definition loc_45 : location_info := LocationInfo file_0 29 21 29 22.
+  Definition loc_46 : location_info := LocationInfo file_0 29 21 29 22.
+  Definition loc_47 : location_info := LocationInfo file_0 29 26 29 27.
+  Definition loc_50 : location_info := LocationInfo file_0 28 8 28 13.
+  Definition loc_51 : location_info := LocationInfo file_0 28 8 28 9.
+  Definition loc_52 : location_info := LocationInfo file_0 28 8 28 9.
+  Definition loc_53 : location_info := LocationInfo file_0 28 12 28 13.
+  Definition loc_54 : location_info := LocationInfo file_0 28 12 28 13.
+  Definition loc_55 : location_info := LocationInfo file_0 22 17 22 18.
+  Definition loc_56 : location_info := LocationInfo file_0 22 17 22 18.
+  Definition loc_59 : location_info := LocationInfo file_0 22 10 22 11.
+
+  (* Definition of function [binary_search]. *)
+  Definition impl_binary_search : function := {|
+    f_args := [
+      ("xs", LPtr);
+      ("n", it_layout i32);
+      ("x", LPtr);
+      ("comp", LPtr)
+    ];
+    f_local_vars := [
+      ("r", it_layout i32);
+      ("l", it_layout i32);
+      ("k", it_layout i32)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "l" <-{ it_layout i32 } LocInfoE loc_59 (i2v 0 i32) ;
+        "r" <-{ it_layout i32 }
+          LocInfoE loc_55 (use{it_layout i32} (LocInfoE loc_56 ("n"))) ;
+        locinfo: loc_3 ;
+        Goto "#1"
+      ]> $
+      <[ "#1" :=
+        locinfo: loc_50 ;
+        if: LocInfoE loc_50 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_50 ((LocInfoE loc_51 (use{it_layout i32} (LocInfoE loc_52 ("l")))) <{IntOp i32, IntOp i32} (LocInfoE loc_53 (use{it_layout i32} (LocInfoE loc_54 ("r")))))))
+        then
+        Goto "#2"
+        else
+        locinfo: loc_4 ;
+          Goto "#3"
+      ]> $
+      <[ "#2" :=
+        "k" <-{ it_layout i32 }
+          LocInfoE loc_38 ((LocInfoE loc_39 (use{it_layout i32} (LocInfoE loc_40 ("l")))) +{IntOp i32, IntOp i32} (LocInfoE loc_41 ((LocInfoE loc_42 ((LocInfoE loc_43 (use{it_layout i32} (LocInfoE loc_44 ("r")))) -{IntOp i32, IntOp i32} (LocInfoE loc_45 (use{it_layout i32} (LocInfoE loc_46 ("l")))))) /{IntOp i32, IntOp i32} (LocInfoE loc_47 (i2v 2 i32))))) ;
+        locinfo: loc_25 ;
+        "$0" <- LocInfoE loc_27 (use{LPtr} (LocInfoE loc_28 ("comp"))) with
+          [ LocInfoE loc_29 (use{LPtr} (LocInfoE loc_31 ((LocInfoE loc_32 (!{LPtr} (LocInfoE loc_33 ("xs")))) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_34 (use{it_layout i32} (LocInfoE loc_35 ("k"))))))) ;
+          LocInfoE loc_36 (use{LPtr} (LocInfoE loc_37 ("x"))) ] ;
+        locinfo: loc_25 ;
+        if: LocInfoE loc_25 ("$0")
+        then
+        locinfo: loc_14 ;
+          Goto "#5"
+        else
+        locinfo: loc_21 ;
+          Goto "#6"
+      ]> $
+      <[ "#3" :=
+        locinfo: loc_4 ;
+        Return (LocInfoE loc_5 (use{it_layout i32} (LocInfoE loc_6 ("l"))))
+      ]> $
+      <[ "#4" :=
+        locinfo: loc_11 ;
+        Goto "continue2"
+      ]> $
+      <[ "#5" :=
+        locinfo: loc_14 ;
+        LocInfoE loc_15 ("l") <-{ it_layout i32 }
+          LocInfoE loc_16 ((LocInfoE loc_17 (use{it_layout i32} (LocInfoE loc_18 ("k")))) +{IntOp i32, IntOp i32} (LocInfoE loc_19 (i2v 1 i32))) ;
+        locinfo: loc_11 ;
+        Goto "#4"
+      ]> $
+      <[ "#6" :=
+        locinfo: loc_21 ;
+        LocInfoE loc_22 ("r") <-{ it_layout i32 }
+          LocInfoE loc_23 (use{it_layout i32} (LocInfoE loc_24 ("k"))) ;
+        locinfo: loc_11 ;
+        Goto "#4"
+      ]> $
+      <[ "continue2" :=
+        locinfo: loc_3 ;
+        Goto "#1"
+      ]> $∅
+    )%E
+  |}.
+End code.

examples/proofs/binary_search/generated_proof_binary_search.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_binary_search.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [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.
+    split_blocks ((
+      <[ "#1" :=
+        ∃ vl : nat,
+        ∃ vr : nat,
+        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⌝)) ∗
+        local_k ◁ₗ uninit (it_layout i32) ∗
+        local_l ◁ₗ (vl @ (int (i32))) ∗
+        local_r ◁ₗ (vr @ (int (i32))) ∗
+        ⌜vl <= vr⌝ ∗
+        ⌜vr <= length ls⌝ ∗
+        ⌜∀ i y, (i < vl)%nat → ls !! i = Some y → R y x⌝ ∗
+        ⌜∀ i y, (vr ≤ i)%nat → ls !! i = Some y → ¬ R y x⌝
+    ]> $
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "binary_search" "#0".
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "binary_search" "#1".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: try by [revert select (∀ i j, _ → _ → ¬ R _ _); apply; [| done];solve_goal].
+    all: try by apply: (binary_search_cond_1 y); solve_goal.
+    all: try by apply: (binary_search_cond_2 y); solve_goal.
+    all: print_sidecondition_goal "binary_search".
+  Qed.
+End proof_binary_search.

examples/proofs/binary_search/generated_spec.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.binary_search Require Import generated_code.
+From refinedc.examples.binary_search Require Import binary_search_extra.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/binary_search.c]. *)
+Section spec.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Type definitions. *)
+
+  (* 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))).
+End spec.

examples/proofs/binary_search/proof_files

+generated_proof_binary_search.v

theories/lang/base.v

@@ -186,6 +186,15 @@ Lemma bool_decide_eq_x_x_true {A} (x : A) `{!Decision (x = x)} :
   bool_decide (x = x) = true.
 Proof. by case_bool_decide.  Qed.
 
+Lemma StronglySorted_lookup_le {A} R (l : list A) i j x y:
+  StronglySorted R l → l !! i = Some x → l !! j = Some y → (i ≤ j)%nat → x = y ∨ R x y.
+Proof.
+  move => Hsorted. elim: Hsorted i j => // z {}l ? IH Hall [|?] [|?]//=???; simplify_eq; try lia.
+  - by left.
+  - right. by apply: (Forall_lookup_1 _ _ _ _ Hall).
+  - apply: IH => //. lia.
+Qed.
+
 
   Lemma StronglySorted_lookup_lt {A} R (l : list A) i j x y:
     StronglySorted R l → l !! i = Some x → l !! j = Some y → ¬ R y x → x ≠ y → (i < j)%nat.

theories/typing/automation.v

@@ -92,8 +92,9 @@ Ltac liRIntroduceLetInGoal :=
     end
   end.
 
-(* TODO: make this extensible via a hook tactic *)
+Ltac liRInstantiateEvars_hook := idtac.
 Ltac liRInstantiateEvars :=
+  liRInstantiateEvars_hook;
   lazymatch goal with
   | |- (_ < protected ?H)%nat ∧ _ => liInst H (S (protected (EVAR_ID _)))
   (* This is very hard to figure out for unification because of the
@@ -101,6 +102,7 @@ Ltac liRInstantiateEvars :=
   definition of ty without this. This is the reason why do_instantiate
   evars must come before do_side_cond *)
   | |- protected ?H = ( _ @ ?ty)%I ∧ _ => liInst H ((protected (EVAR_ID _)) @ ty)%I
+  | |- protected ?H = ty_of_rty (frac_ptr ?β _)%I ∧ _ => liInst H (frac_ptr β (protected (EVAR_ID _)))%I
   | |- envs_entails _ (subsume (?x ◁ₗ{?β} ?ty) (_ ◁ₗ{_} (protected ?H)) _) => liInst H ty
   | |- envs_entails _ (subsume (?x ◁ₗ{?β} ?ty) (_ ◁ₗ{protected ?H} _) _) => liInst H β
   end.

theories/typing/function.v

@@ -45,6 +45,14 @@ Section function.
   Next Obligation. iIntros (f v ???) "?". iDestruct 1 as (? ->) "?". iFrame. iExists _. by iFrame. Qed.
   Next Obligation. by iIntros (f v). Qed.
 
+  Global Program Instance copyable_function_ptr p fp : Copyable (p @ function_ptr fp).
+  Next Obligation.
+    iIntros (p fp E l ?). iDestruct 1 as (fn Hl) "(Hl&?&?)".
+    iMod (heap_mapsto_own_state_to_mt with "Hl") as (q) "[_ Hl]" => //. iSplitR => //.
+    iExists _, _. iFrame. iModIntro. iSplit. by iExists _; iFrame.
+    by iIntros "_".
+  Qed.
+
   Definition typed_callable (v : val) (ty : type) `{!Movable ty} (T : (A → fn_params) → iProp Σ) : iProp Σ :=
     (v ◁ᵥ ty -∗ ∃ f fn fp, ⌜v = val_of_loc f⌝ ∗ fntbl_entry f fn ∗ ▷ typed_function fn fp ∗ T fp)%I.
 

theories/typing/programs.v

@@ -524,6 +524,14 @@ Section typing.
     SubsumeVal v (x1 @ ty)%I (x2 @ ty)%I | 2:=
     λ T, i2p (subsume_val_refinement_id v ty T x1 x2).
 
+  Lemma subtype_var {A} (ty : A → type) x y l β T:
+    ⌜x = y⌝ ∗ T -∗
+    subsume (l ◁ₗ{β} ty x) (l ◁ₗ{β} ty y) T.
+  Proof. iIntros "[-> $] $". Qed.
+  (* This must be an hint extern because an instance would be a big slowdown . *)
+  Definition subtype_var_inst {A} (ty : A → type) x y l β : SubsumePlace l β (ty x) (ty y) :=
+    λ T, i2p (subtype_var ty x y l β T).
+
   Lemma typed_binop_simplify v1 P1 v2 P2 T o1 o2 ot1 ot2 {SH1 : SimplifyHyp P1 o1} {SH2 : SimplifyHyp P2 o2} op:
     let G1 := (SH1 (find_in_context (FindValP v1) (λ P, typed_bin_op v1 P v2 P2 op ot1 ot2 T))).(i2p_P) in
     let G2 := (SH2 (find_in_context (FindValP v2) (λ P, typed_bin_op v1 P1 v2 P op ot1 ot2 T))).(i2p_P) in
@@ -980,6 +988,10 @@ Section typing.
     λ T, i2p (annot_learn l β ty T).
 End typing.
 
+(* This must be an hint extern because an instance would be a big slowdown . *)
+Hint Extern 1 (SubsumePlace _ _ (?ty _) (?ty2 _)) =>
+  match ty with | ty2 => is_var ty; class_apply subtype_var_inst end : typeclass_instances.
+
 (*** guarded *)
 Section guarded.
   Context `{!typeG Σ}.

theories/typing/singleton.v

@@ -35,7 +35,7 @@ Section singleton_val.
     iIntros "[% [% Hl]]". iApply "HT". by iApply (ty_ref with "[] Hl Hv").
   Qed.
   Global Instance singleton_val_merge_inst v l ly:
-    SimplifyHypPlace l Own (singleton_val ly v)%I (Some 50%N) :=
+    SimplifyHypPlace l Own (singleton_val ly v)%I (Some 50%N) | 20 :=
     λ T, i2p (singleton_val_merge v l ly T).
 
   Lemma type_read_move T l ty ly a `{!Movable ty}: