Theory Examples.Sorting_Quicksort_Partition

theory Sorting_Quicksort_Partition
imports Sorting_Quicksort_Scheme
begin
  
hide_const (open) Transcendental.pi ― ‹‹pi› is the implementation of ‹p›, not some constant related to a circle ;)›

(* TODO: Move. Found useful for ATPs *)
lemma strict_itrans: "a < c ⟹ a < b ∨ b < c" for a b c :: "_::linorder"
  by auto


context weak_ordering begin
  
subsection ‹Find Median›

definition "move_median_to_first ri ai bi ci (xs::'a list) ≡ doN {
    ASSERT (ai≠bi ∧ ai≠ci ∧ bi≠ci ∧ ri≠ai ∧ ri≠bi ∧ ri≠ci);
    a ← mop_list_get xs ai;
    b ← mop_list_get xs bi;
    c ← mop_list_get xs ci;
  
    if a<b then (
      if b<c then
        mop_list_swap xs ri bi
      else if a<c then
        mop_list_swap xs ri ci
      else 
        mop_list_swap xs ri ai
    ) 
    else if a<c then
      mop_list_swap xs ri ai
    else if b<c then 
      mop_list_swap xs ri ci
    else 
      mop_list_swap xs ri bi
  }"

lemma move_median_to_first_alt: "move_median_to_first ri ai bi ci (xs::'a list) = doN {
    ASSERT (ai≠bi ∧ ai≠ci ∧ bi≠ci ∧ ri≠ai ∧ ri≠bi ∧ ri≠ci);
  
    ifN mop_cmp_idxs xs ai bi then (
      ifN mop_cmp_idxs xs bi ci then
        mop_list_swap xs ri bi
      else ifN mop_cmp_idxs xs ai ci then
        mop_list_swap xs ri ci
      else 
        mop_list_swap xs ri ai
    ) 
    else ifN mop_cmp_idxs xs ai ci then
      mop_list_swap xs ri ai
    else ifN mop_cmp_idxs xs bi ci then 
      mop_list_swap xs ri ci
    else 
      mop_list_swap xs ri bi
  }"
  unfolding move_median_to_first_def
  by (auto simp: pw_eq_iff refine_pw_simps split!: if_splits)
  
  
lemma move_median_to_first_correct:
  "⟦ ri<ai; ai<bi; bi<ci; ci<length xs ⟧ ⟹ 
  move_median_to_first ri ai bi ci xs 
    ≤ SPEC (λxs'. ∃i∈{ai,bi,ci}. 
        xs' = swap xs ri i
      ∧ (∃j∈{ai,bi,ci}-{i}. xs!i≤xs!j)   
      ∧ (∃j∈{ai,bi,ci}-{i}. xs!i≥xs!j)   
      )"
  unfolding move_median_to_first_def
  apply refine_vcg
  supply aux = bexI[where P="λx. _=_ x ∧ _ x", OF conjI[OF refl]]
  apply ((rule aux)?; insert connex,auto simp: unfold_lt_to_le)+
  done
  
    
lemma move_median_to_first_correct':
  "⟦ ri<ai; ai<bi; bi<ci; ci<length xs ⟧ ⟹ 
  move_median_to_first ri ai bi ci xs 
    ≤ SPEC (λxs'. slice_eq_mset ri (ci+1) xs' xs 
      ∧ (∃i∈{ai,bi,ci}. xs'!i≤xs'!ri)
      ∧ (∃i∈{ai,bi,ci}. xs'!i≥xs'!ri)
      )"
  apply (rule order_trans[OF move_median_to_first_correct])    
  by auto
  
(* TODO: Clean up prove below, to use more concise aux-lemma! *)  
lemma move_median_to_first_correct'':
  "⟦ ri<ai; ai<bi; bi<ci; ci<length xs ⟧ ⟹ 
  move_median_to_first ri ai bi ci xs 
    ≤ SPEC (λxs'. slice_eq_mset ri (ci+1) xs' xs 
      ∧ (∃i∈{ai..ci}. xs'!i≤xs'!ri)
      ∧ (∃i∈{ai..ci}. xs'!i≥xs'!ri)
      )"
  apply (rule order_trans[OF move_median_to_first_correct'])    
  by auto
  
end

context sort_impl_context begin 
  
sepref_register move_median_to_first

sepref_def move_median_to_first_impl [llvm_inline] is "uncurry4 (PR_CONST move_median_to_first)" 
  :: "[λ_. True]c size_assnk *a size_assnk *a size_assnk *a size_assnk *a (arr_assn)d 
    → arr_assn [λ((((_,_),_),_),ai) r. r=ai]c"
  unfolding move_median_to_first_alt PR_CONST_def
  by sepref 
                    
end

context weak_ordering begin  
  
subsection ‹Hoare Partitioning Scheme›  


definition "ungrd_qsp_next_l_spec xs pi li hi ≡ 
  doN {
    ASSERT (pi<li ∧ pi<hi ∧ hi≤length xs);
    ASSERT (∃i∈{li..<hi}. xs!i ≥ xs!pi); 
    SPEC (λli'. li≤li' ∧ li'<hi ∧ (∀i∈{li..<li'}. xs!i<xs!pi) ∧ xs!li'≥xs!pi)
  }"

definition "ungrd_qsp_next_h_spec xs pi hi ≡ 
  doN {
    ASSERT (pi<length xs ∧ hi≤length xs ∧ (∃i∈{pi<..<hi}. (xs!i) ≤ xs!pi)); 
    SPEC (λhi'. hi'<hi ∧ (∀i∈{hi'<..<hi}. xs!i>xs!pi) ∧ xs!hi'≤xs!pi)
  }"
  
  
definition qsp_next_l :: "'a list ⇒ nat ⇒ nat ⇒ nat ⇒ nat nres" where            
  "qsp_next_l xs pi li hi ≡ doN {
    monadic_WHILEIT (λli'. (∃i∈{li'..<hi}. xs!i≥xs!pi) ∧ li≤li' ∧ (∀i∈{li..<li'}. xs!i<xs!pi)) 
      (λli. doN {ASSERT (li≠pi); mop_cmp_idxs xs li pi}) (λli. RETURN (li + 1)) li
  }"  

  
lemma qsp_next_l_refine: "(qsp_next_l,PR_CONST ungrd_qsp_next_l_spec)∈Id→Id→Id→Id→⟨Id⟩nres_rel"
  unfolding qsp_next_l_def ungrd_qsp_next_l_spec_def PR_CONST_def
  apply (intro fun_relI; clarsimp)
  subgoal for xs p li hi
    apply (refine_vcg monadic_WHILEIT_rule[where R="measure (λli. hi - li)"])
    apply simp_all
    subgoal by auto
    apply safe
    subgoal by (metis atLeastLessThan_iff leI le_less_Suc_eq wo_leD)
    subgoal by (metis atLeastLessThan_iff leI le_less_Suc_eq)
    subgoal using less_eq_Suc_le by force
    subgoal by auto
    subgoal by (auto simp: unfold_le_to_lt)
    done  
  done


definition qsp_next_h :: "'a list ⇒ nat ⇒ nat ⇒ nat nres" where
  "qsp_next_h xs pi hi ≡ doN {
    ASSERT (hi>0);
    let hi = hi - 1;
    ASSERT (hi<length xs);
    monadic_WHILEIT (λhi'. hi'≤hi ∧ (∃i≤hi'. xs!i≤xs!pi) ∧ (∀i∈{hi'<..hi}. xs!i>xs!pi))
      (λhi. doN {ASSERT(pi≠hi); mop_cmp_idxs xs pi hi}) (λhi. doN { ASSERT(hi>0); RETURN (hi - 1)}) hi
  }"  

  
lemma qsp_next_h_refine: "(qsp_next_h,PR_CONST (ungrd_qsp_next_h_spec)) ∈ Id → Id → Id → ⟨Id⟩nres_rel"
  unfolding qsp_next_h_def ungrd_qsp_next_h_spec_def PR_CONST_def
  apply (refine_vcg monadic_WHILEIT_rule[where R="measure id"] split_ifI)
  apply (all ‹(determ ‹elim conjE exE›)?›)
  apply simp_all
  subgoal by force
  subgoal by (meson greaterThanLessThan_iff nat_le_Suc_less_imp)
  subgoal by (meson greaterThanAtMost_iff greaterThanLessThan_iff nat_le_Suc_less_imp wo_leD)
  subgoal by (metis gr0I le_zero_eq unfold_lt_to_le)
  subgoal by (metis One_nat_def le_step_down_nat wo_leD)
  subgoal by (metis Suc_pred greaterThanAtMost_iff linorder_neqE_nat not_less_eq)
  subgoal by (meson greaterThanAtMost_iff greaterThanLessThan_iff nat_le_Suc_less_imp)
  subgoal using wo_leI by blast
  done  

definition "qs_partition li0 hi0 pi xs0 ≡ doN {
  ASSERT (pi < li0 ∧ li0<hi0 ∧ hi0≤length xs0);
  
  ― ‹Initialize›
  li ← ungrd_qsp_next_l_spec xs0 pi li0 hi0;
  hi ← ungrd_qsp_next_h_spec xs0 pi hi0;
  
  ASSERT (li0≤hi);
  
  (xs,li,hi) ← WHILEIT 
    (λ(xs,li,hi). 
        li0≤li ∧ hi<hi0
      ∧ li<hi0 ∧ hi≥li0  
      ∧ slice_eq_mset li0 hi0 xs xs0
      ∧ xs!pi = xs0!pi
      ∧ (∀i∈{li0..<li}. xs!i ≤ xs0!pi)
      ∧ xs!li ≥ xs0!pi
      ∧ (∀i∈{hi<..<hi0}. xs!i ≥ xs0!pi)
      ∧ xs!hi ≤ xs0!pi  
    )
    (λ(xs,li,hi). li<hi) 
    (λ(xs,li,hi). doN {
      ASSERT(li<hi ∧ li<length xs ∧ hi<length xs ∧ li≠hi);
      xs ← mop_list_swap xs li hi;
      let li = li + 1;
      li ← ungrd_qsp_next_l_spec xs pi li hi0;
      hi ← ungrd_qsp_next_h_spec xs pi hi;
      RETURN (xs,li,hi)
    }) 
    (xs0,li,hi);
  
  RETURN (xs,li)
}"  


lemma qs_partition_correct:
  "⟦ pi<li; li<hi; hi≤length xs0; ∃i∈{li..<hi}. xs0!pi≤xs0!i; ∃i∈{li..<hi}. xs0!i≤xs0!pi ⟧ ⟹ qs_partition li hi pi xs0 
  ≤ SPEC (λ(xs,i). slice_eq_mset li hi xs xs0 ∧ li≤i ∧ i<hi ∧ (∀i∈{li..<i}. xs!i≤xs0!pi) ∧ (∀i∈{i..<hi}. xs!i≥xs0!pi) )"  
  unfolding qs_partition_def ungrd_qsp_next_l_spec_def ungrd_qsp_next_h_spec_def
  apply (refine_vcg WHILEIT_rule[where R="measure (λ(_,_,hi). hi)"])  
  supply [[put_named_ss HOL_ss]]
  apply (all ‹(clarsimp;fail)?›)
  apply clarsimp_all
  supply [[put_named_ss Main_ss]]
  apply (simp_all add: slice_eq_mset_eq_length unfold_lt_to_le)
  
  subgoal by fastforce
  subgoal by auto
  subgoal
    by (metis slice_eq_mset_eq_length swap_length) 
  subgoal apply (clarsimp simp: swap_def)
    by (metis (full_types) More_List.swap_def atLeastSucLessThan_greaterThanLessThan greaterThanLessThan_iff less_le_trans swap_nth2) 
  subgoal
    by (metis (mono_tags) greaterThanLessThan_iff leD le_less_trans less_le_trans nat_le_linear not_less_eq_eq slice_eq_mset_eq_length swap_indep swap_nth1) 
  subgoal 
    by (smt Suc_le_lessD dual_order.trans greaterThanLessThan_iff leI less_imp_le_nat swap_indep swap_length swap_nth1) 
  subgoal
    by (smt Suc_le_lessD atLeastLessThan_iff le_less_trans less_imp_le_nat slice_eq_mset_eq_length slice_eq_mset_swap(2)) 
    
  subgoal apply clarsimp
    by (metis less_irrefl less_imp_not_less less_le_trans swap_indep)
    
  subgoal apply clarsimp
    by (smt Suc_leI atLeastLessThan_iff le_def less_le_trans less_Suc_eq swap_indep swap_length swap_nth1)
  subgoal apply clarsimp
    by (metis le_def less_trans swap_indep)
      
  subgoal apply clarsimp
    by (smt greaterThanLessThan_iff le_def less_le_trans le_neq_implies_less less_imp_le_nat slice_eq_mset_eq_length swap_indep swap_nth2)
    
  subgoal
    by (metis le_def less_trans swap_indep)
  subgoal
    by (metis greaterThanLessThan_iff strict_itrans le_neq_implies_less)
  done    


definition "partition_pivot xs0 l h ≡ doN {
  ASSERT (l≤h ∧ h≤length xs0 ∧ h-l≥4);
  let m = l + (h-l) div 2;
  xs1 ← move_median_to_first l (l+1) m (h-1) xs0;
  ASSERT (l<length xs1 ∧ length xs1 = length xs0);
  (xs,m) ← qs_partition (l+1) h l xs1;

  ― ‹TODO: Use an auxiliary lemma, instead of this assertion chain! ›
  ASSERT (l<m ∧ m<h);
  ASSERT ((∀i∈{l+1..<m}. xs!i≤xs1!l) ∧ xs!l≤xs1!l);
  ASSERT (∀i∈{l..<m}. xs!i≤xs1!l);
  ASSERT (∀i∈{m..<h}. xs1!l≤xs!i);
  
  
  RETURN (xs,m)
}"

lemma slice_LT_I_aux:
  assumes B: "l<m" "m<h" "h≤length xs"
  assumes BND: "∀i∈{l..<m}. xs!i≤p" "∀i∈{m..<h}. p≤xs!i"
  shows "slice_LT (≤) (slice l m xs) (slice m h xs)"
  unfolding slice_LT_def
  using B apply (clarsimp simp: in_set_conv_nth slice_nth)
  subgoal for i j
    apply (rule trans[OF BND(1)[THEN bspec, of "l+i"] BND(2)[THEN bspec, of "m+j"]])
    by auto
  done
  
lemma partition_pivot_correct: "⟦(xs,xs')∈Id; (l,l')∈Id; (h,h')∈Id⟧ 
  ⟹ partition_pivot xs l h ≤ ⇓Id (partition3_spec xs' l' h')"
  unfolding partition_pivot_def partition3_spec_def
  apply (refine_vcg move_median_to_first_correct'' qs_partition_correct)
  apply (all ‹auto 0 3 dest: slice_eq_mset_eq_length; fail›) [17]
  apply clarsimp
  subgoal for xs1 xs2 i m j
    apply (subst slice_eq_mset_nth_outside, assumption)
    apply (auto dest: slice_eq_mset_eq_length)
    done
  subgoal apply clarsimp by (metis (full_types) Suc_leI atLeastLessThan_iff le_neq_implies_less)
  subgoal by auto  
  subgoal 
    apply simp
    by (metis Suc_le_eq le_add2 le_refl order.strict_trans plus_1_eq_Suc slice_eq_mset_subslice slice_eq_mset_trans)
  apply (all ‹auto; fail›) [2]
  subgoal by (auto dest: slice_eq_mset_eq_length intro!: slice_LT_I_aux)
  done
  
end  
  
context sort_impl_context begin
  
sepref_register ungrd_qsp_next_l_spec ungrd_qsp_next_h_spec 

(* TODO: We can get rid of the length xs restriction: the stopper element will always lie within <h, which is size_t representable! *)
sepref_definition qsp_next_l_impl [llvm_inline] is "uncurry3 (qsp_next_l)" :: "(arr_assn)k *a size_assnk *a size_assnk *a size_assnk →a size_assn"
  unfolding qsp_next_l_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  by sepref

lemmas [sepref_fr_rules] = qsp_next_l_impl.refine[FCOMP qsp_next_l_refine]  
  
sepref_definition qsp_next_h_impl [llvm_inline] is "uncurry2 (qsp_next_h)" :: "(arr_assn)k *a size_assnk *a size_assnk →a size_assn"
  unfolding qsp_next_h_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  by sepref
  
lemmas [sepref_fr_rules] = qsp_next_h_impl.refine[FCOMP qsp_next_h_refine]  
  
                        
sepref_register qs_partition  
sepref_def qs_partition_impl (*[llvm_inline]*) is "uncurry3 (PR_CONST qs_partition)" 
  :: "[λ_. True]c size_assnk *a size_assnk *a size_assnk *a (arr_assn)d 
    → arr_assn ×a size_assn [λ(((_,_),_),ai) (r,_). r=ai]c"
  unfolding qs_partition_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  supply [dest] = slice_eq_mset_eq_length
  by sepref

(*sepref_register qs_partitionXXX  
sepref_def qs_partitionXXX_impl (*[llvm_inline]*) is "uncurry3 (PR_CONST qs_partitionXXX)" :: "[λ(((l,h),p),xs). length xs < max_snat LENGTH(size_t)]a size_assnk *a size_assnk *a size_assnk *a (arr_assn)d → arr_assn ×a size_assn"
  unfolding qs_partitionXXX_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  supply [dest] = slice_eq_mset_eq_length
  by sepref
*)  

sepref_register partition_pivot  
sepref_def partition_pivot_impl [llvm_inline] is "uncurry2 (PR_CONST partition_pivot)" 
  :: "[λ_. True]c arr_assnd *a size_assnk *a size_assnk → arr_assn ×a size_assn [λ((ai,_),_) (r,_). r=ai]c"
  unfolding partition_pivot_def PR_CONST_def    
  apply (annot_snat_const "TYPE(size_t)")
  by sepref

  

end


subsection ‹Parameterization›

context parameterized_weak_ordering begin
  thm WO.qsp_next_l_def

  definition qsp_next_l_param :: "'cparam ⇒ 'a list ⇒ nat ⇒ nat ⇒ nat ⇒ nat nres" where            
    "qsp_next_l_param cparam xs pi li hi ≡ doN {
      monadic_WHILEIT (λ_. True) 
        (λli. doN {ASSERT (li≠pi); pcmp_idxs2 cparam xs li pi}) 
        (λli. doN {ASSERT (li<hi); RETURN (li + 1)}) li
    }"  
  
  lemma qsp_next_l_param_refine[refine]: "⟦
    (xs',xs)∈cdom_list_rel cparam; (p',p)∈Id; (i',i)∈Id; (h',h)∈Id
  ⟧ ⟹ qsp_next_l_param cparam xs' p' i' h' ≤⇓nat_rel (WO.ungrd_qsp_next_l_spec cparam xs p i h)"
  proof (goal_cases)
    case 1
    then have "qsp_next_l_param cparam xs' p' i' h' ≤⇓nat_rel (WO.qsp_next_l cparam xs p i h)" 
      unfolding qsp_next_l_param_def WO.qsp_next_l_def
      apply refine_rcg
      by auto
    also note WO.qsp_next_l_refine[param_fo, OF IdI IdI IdI IdI, of cparam xs p i h, THEN nres_relD]
    finally show ?case unfolding PR_CONST_def .
  qed 
  
    
  definition qsp_next_h_param :: "'cparam ⇒ 'a list ⇒ nat ⇒ nat ⇒ nat nres" where
    "qsp_next_h_param cparam xs pi hi ≡ doN {
      ASSERT (hi>0);
      let hi = hi - 1;
      ASSERT (hi<length xs);
      monadic_WHILEIT (λ_. True)
        (λhi. doN {ASSERT(pi≠hi); pcmp_idxs2 cparam xs pi hi}) 
        (λhi. doN { ASSERT(hi>0); RETURN (hi - 1)}) hi
    }"  

  lemma qsp_next_h_param_refine[refine]: "⟦
    (xs',xs)∈cdom_list_rel cparam; (p',p)∈Id; (h',h)∈Id
  ⟧ ⟹ qsp_next_h_param cparam xs' p' h' ≤⇓nat_rel (WO.ungrd_qsp_next_h_spec cparam xs p h)"      
  proof goal_cases
    case 1
    then have "qsp_next_h_param cparam xs' p' h' ≤⇓nat_rel (WO.qsp_next_h cparam xs p h)"
      unfolding qsp_next_h_param_def WO.qsp_next_h_def
      apply refine_rcg
      by (auto simp: cdom_list_rel_alt in_br_conv)
    also note WO.qsp_next_h_refine[param_fo, THEN nres_relD]
    finally show ?thesis by simp 
  qed    
    
  definition "qs_partition_param cparam li0 hi0 pi xs0 ≡ doN {
    ASSERT (pi < li0 ∧ li0<hi0 ∧ hi0≤length xs0);
    
    ― ‹Initialize›
    li ← qsp_next_l_param cparam xs0 pi li0 hi0;
    hi ← qsp_next_h_param cparam xs0 pi hi0;
    
    ASSERT (li0≤hi);
    
    (xs,li,hi) ← WHILEIT 
      (λ_. True)
      (λ(xs,li,hi). li<hi) 
      (λ(xs,li,hi). doN {
        ASSERT(li<hi ∧ li<length xs ∧ hi<length xs ∧ li≠hi);
        xs ← mop_list_swap xs li hi;
        let li = li + 1;
        li ← qsp_next_l_param cparam xs pi li hi0;
        hi ← qsp_next_h_param cparam xs pi hi;
        RETURN (xs,li,hi)
      }) 
      (xs0,li,hi);
    
    RETURN (xs,li)
  }"  

  lemma qs_partition_param_refine[refine]: "⟦
    (li',li)∈Id; (hi',hi)∈Id; (pi',pi)∈Id; (xs',xs)∈cdom_list_rel cparam
  ⟧ ⟹ qs_partition_param cparam li' hi' pi' xs' 
    ≤ ⇓(cdom_list_rel cparam ×r nat_rel) (WO.qs_partition cparam li hi pi xs)" 
    unfolding qs_partition_param_def WO.qs_partition_def
    supply [refine_dref_RELATES] = RELATESI[of "cdom_list_rel cparam"]
    apply refine_rcg
    apply refine_dref_type
    apply (auto simp: cdom_list_rel_alt in_br_conv)
    done

 definition "move_median_to_first_param cparam ri ai bi ci (xs::'a list) = doN {
    ASSERT (ai ≠ bi ∧ ai ≠ ci ∧ bi ≠ ci ∧ ri ≠ ai ∧ ri ≠ bi ∧ ri ≠ ci);
    ifN pcmp_idxs2 cparam xs ai bi then (
      ifN pcmp_idxs2 cparam xs bi ci then
        mop_list_swap xs ri bi
      else ifN pcmp_idxs2 cparam xs ai ci then
        mop_list_swap xs ri ci
      else 
        mop_list_swap xs ri ai
    ) 
    else ifN pcmp_idxs2 cparam xs ai ci then
      mop_list_swap xs ri ai
    else ifN pcmp_idxs2 cparam xs bi ci then 
      mop_list_swap xs ri ci
    else 
      mop_list_swap xs ri bi
  }"

  
  (* TODO:Move *)
  lemma mop_list_swap_cdom_refine[refine]: "⟦
    (xs',xs)∈cdom_list_rel cparam; (i',i)∈Id; (j',j)∈Id
  ⟧ ⟹ mop_list_swap xs' i' j' ≤ ⇓ (cdom_list_rel cparam) (mop_list_swap xs i j)"
    apply simp
    apply refine_rcg
    apply (clarsimp_all simp: cdom_list_rel_def list_rel_imp_same_length)
    apply (parametricity)
    by auto
  
  lemma move_median_to_first_param_refine[refine]: "⟦
    (ri',ri)∈Id; (ai',ai)∈Id; (bi',bi)∈Id; (ci',ci)∈Id; (xs',xs)∈cdom_list_rel cparam 
  ⟧ ⟹ move_median_to_first_param cparam ri' ai' bi' ci' xs' 
    ≤ ⇓(cdom_list_rel cparam) (WO.move_median_to_first cparam ri ai bi ci xs)"
    unfolding move_median_to_first_param_def WO.move_median_to_first_alt
    apply refine_rcg  
    by auto  
    
  definition "partition_pivot_param cparam xs0 l h ≡ doN {
    ASSERT (l≤h ∧ h≤length xs0 ∧ h-l≥4);
    let m = l + (h-l) div 2;
    xs1 ← move_median_to_first_param cparam l (l+1) m (h-1) xs0;
    ASSERT (l<length xs1 ∧ length xs1 = length xs0);
    (xs,m) ← qs_partition_param cparam (l+1) h l xs1;
  
    RETURN (xs,m)
  }"

  lemma partition_pivot_param_refine[refine]: "⟦ (xs',xs)∈cdom_list_rel cparam; (l',l)∈Id; (h',h)∈Id
    ⟧ ⟹ partition_pivot_param cparam xs' l' h' 
        ≤ ⇓(cdom_list_rel cparam ×r nat_rel) (WO.partition_pivot cparam xs l h)"
    unfolding partition_pivot_param_def WO.partition_pivot_def   
    apply refine_rcg
    apply (auto simp: cdom_list_rel_alt in_br_conv)
    done    
        
end


context parameterized_sort_impl_context begin

  (* TODO: Move *)
  abbreviation "arr_assn ≡ wo_assn"

  
sepref_register qsp_next_l_param qsp_next_h_param

(* TODO: We can get rid of the length xs restriction: the stopper element will always lie within <h, which is size_t representable! *)
sepref_def qsp_next_l_impl [llvm_inline] is "uncurry4 (PR_CONST qsp_next_l_param)" 
  :: "cparam_assnk *a (arr_assn)k *a size_assnk *a size_assnk *a size_assnk →a size_assn"
  unfolding qsp_next_l_param_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  by sepref
 
sepref_def qsp_next_h_impl [llvm_inline] is "uncurry3 (PR_CONST qsp_next_h_param)" :: "cparam_assnk *a (arr_assn)k *a size_assnk *a size_assnk →a size_assn"
  unfolding qsp_next_h_param_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  by sepref
  
                        
sepref_register qs_partition_param  
sepref_def qs_partition_impl is "uncurry4 (PR_CONST qs_partition_param)" 
  :: "[λ_. True]c cparam_assnk *a size_assnk *a size_assnk *a size_assnk *a (arr_assn)d 
    → arr_assn ×a size_assn [λ((((_,_),_),_),ai) (r,_). r=ai]c"
  unfolding qs_partition_param_def PR_CONST_def
  apply (annot_snat_const "TYPE(size_t)")
  supply [dest] = slice_eq_mset_eq_length
  by sepref

sepref_register move_median_to_first_param

sepref_def move_median_to_first_param_impl (*[llvm_inline] *)
  is "uncurry5 (PR_CONST move_median_to_first_param)" 
  :: "[λ_. True]c cparam_assnk *a size_assnk *a size_assnk *a size_assnk *a size_assnk *a (arr_assn)d 
    → arr_assn [λ(((((_,_),_),_),_),ai) r. r=ai]c"
  unfolding move_median_to_first_param_def PR_CONST_def
  by sepref  
  
  
sepref_register partition_pivot_param  
sepref_def partition_pivot_impl (*[llvm_inline] *)
  is "uncurry3 (PR_CONST partition_pivot_param)" 
  :: "[λ_. True]c cparam_assnk *a arr_assnd *a size_assnk *a size_assnk 
    → arr_assn ×a size_assn [λ(((_,ai),_),_) (r,_). r=ai]c"
  unfolding partition_pivot_param_def PR_CONST_def    
  apply (annot_snat_const "TYPE(size_t)")
  by sepref
  

end

end