Theory Bin_Search

theory Bin_Search
imports "../sepref/IICF/IICF" "List-Index.List_Index"
begin

  subsection ‹Binary Search›
    
  subsubsection ‹Abstract Algorithm›
  
  abbreviation "bin_search_invar xs x ≡ (λ(l,h). 
        0≤l ∧ l≤h ∧ h≤length xs 
      ∧ (∀i<l. xs!i<x) ∧ (∀i∈{h..<length xs}. x ≤ xs!i))"
  
  definition "bin_search xs x ≡ do {
    (l,h) ← WHILEIT (bin_search_invar xs x)
      (λ(l,h). l<h) 
      (λ(l,h). do {
        ASSERT (l<length xs ∧ h≤length xs ∧ l≤h);
        let m = l + (h-l) div 2;
        if xs!m < x then RETURN (m+1,h) else RETURN (l,m)
      }) 
      (0,length xs);
    RETURN l
  }"

  
  definition "fi_spec xs x = SPEC (λi. i=find_index (λy. x≤y) xs)"
  
  lemma bin_search_correct:
    assumes "sorted xs"
    shows "bin_search xs x ≤ SPEC (λi. i=find_index (λy. x≤y) xs)"
    unfolding bin_search_def
    apply (refine_vcg WHILEIT_rule[where R="measure (λ(l,h). h-l)"])
    apply (all ‹(auto;fail)?›)

    apply (clarsimp simp: less_Suc_eq_le)
    subgoal for l h i 
      apply (frule sorted_nth_mono[OF assms, of i "l + (h-l) div 2"])
      by auto
    subgoal
      by clarsimp (meson assms leI le_less_trans sorted_iff_nth_mono)
    
    apply clarsimp
    subgoal for i
      by (simp add: find_index_eqI less_le_not_le)
      
    done

  lemma bin_search_correct': "(uncurry bin_search,uncurry fi_spec)
    ∈[λ(xs,_). sorted xs]⇩f Id ×⇩r Id → ⟨nat_rel⟩nres_rel"  
    using bin_search_correct unfolding fi_spec_def
    by (fastforce intro!: frefI nres_relI)
    
    
  subsubsection ‹Implementation›
    
  type_synonym size_t = 64
  type_synonym elem_t = 64

  sepref_def bin_search_impl is "uncurry bin_search"  
    :: "(larray_assn' TYPE(size_t) (sint_assn' TYPE(elem_t)))⇧k 
        *⇩a (sint_assn' TYPE(elem_t))⇧k 
       →⇩a snat_assn' TYPE(size_t)"
    unfolding bin_search_def
    apply (rule hfref_with_rdomI)
    apply (annot_snat_const "TYPE(size_t)")
    apply sepref    
    done

  definition [llvm_code, llvm_inline]: "bin_search_impl' a x ≡ doM {
    a ← ll_load a;
    bin_search_impl a x
  }"  
    
    
  export_llvm bin_search_impl' is ‹int64_t bin_search(larray_t*, elem_t)› 
  defines ‹
    typedef uint64_t elem_t;
    typedef struct {
      int64_t len;
      elem_t *data;
    } larray_t;
  ›
  file "../../regression/gencode/bin_search.ll"
    
  export_llvm bin_search_impl' is ‹int64_t bin_search(larray_t*, elem_t)› 
  defines ‹
    typedef uint64_t elem_t;
    typedef struct {
      int64_t len;
      elem_t *data;
    } larray_t;
  ›
  file "code/bin_search.ll"
  
  
  lemmas bs_impl_correct = bin_search_impl.refine[FCOMP bin_search_correct']
  
  subsubsection ‹Combined Correctness Theorem›
  
  theorem bin_search_impl_correct:
    "llvm_htriple 
      (larray_assn sint_assn xs xsi ** sint_assn x xi ** ↑(sorted xs)) 
      (bin_search_impl xsi xi)
      (λii. EXS i. larray_assn sint_assn xs xsi ** sint_assn x xi ** snat_assn i ii 
                  ** ↑(i=find_index (λy. x≤y) xs))"
  proof -
  
    from bin_search_correct have R: 
        "(uncurry bin_search, uncurry (λxs x. SPEC (λi. i = find_index ((≤) x) xs))) 
      ∈ [λ(xs,x). sorted xs]⇩f Id → ⟨Id⟩nres_rel"
      apply (intro frefI nres_relI)
      apply fastforce 
      done
  
    note bin_search_impl.refine  
    note R = bin_search_impl.refine[FCOMP R]
    note R = R[THEN hfrefD, THEN hn_refineD, of "(xs,x)" "(xsi,xi)", simplified]
    note [vcg_rules] = R
    
    show ?thesis by vcg'
  qed

  theorem bin_search_impl'_correct:
    "llvm_htriple 
      (↿ll_pto xsi xsip ** larray_assn sint_assn xs xsi ** sint_assn x xi ** ↑(sorted xs)) 
      (bin_search_impl' xsip xi)
      (λii. EXS i. ↿ll_pto xsi xsip ** larray_assn sint_assn xs xsi ** sint_assn x xi ** snat_assn i ii 
                  ** ↑(i=find_index (λy. x≤y) xs))"
  proof -
    interpret llvm_prim_setup .
    show ?thesis
      unfolding bin_search_impl'_def
      supply [vcg_rules] = bin_search_impl_correct
      by vcg
  qed
  
end