Theory 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 (aibi  aici  bici  riai  ribi  rici);
    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 (aibi  aici  bici  riai  ribi  rici);
  
    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!ixs!j)   
       (j{ai,bi,ci}-{i}. xs!ixs!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'!ixs'!ri)
       (i{ai,bi,ci}. xs'!ixs'!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'!ixs'!ri)
       (i{ai..ci}. xs'!ixs'!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  hilength xs);
    ASSERT (i{li..<hi}. xs!i  xs!pi); 
    SPEC (λli'. lili'  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  hilength 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!ixs!pi)  lili'  (i{li..<li'}. xs!i<xs!pi)) 
      (λli. doN {ASSERT (lipi); 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)IdIdIdIdIdnres_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  (ihi'. xs!ixs!pi)  (i{hi'<..hi}. xs!i>xs!pi))
      (λhi. doN {ASSERT(pihi); 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  Idnres_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  hi0length xs0);
  
  ― ‹Initialize
  li  ungrd_qsp_next_l_spec xs0 pi li0 hi0;
  hi  ungrd_qsp_next_h_spec xs0 pi hi0;
  
  ASSERT (li0hi);
  
  (xs,li,hi)  WHILEIT 
    (λ(xs,li,hi). 
        li0li  hi<hi0
       li<hi0  hili0  
       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  lihi);
      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; hilength xs0; i{li..<hi}. xs0!pixs0!i; i{li..<hi}. xs0!ixs0!pi   qs_partition li hi pi xs0 
   SPEC (λ(xs,i). slice_eq_mset li hi xs xs0  lii  i<hi  (i{li..<i}. xs!ixs0!pi)  (i{i..<hi}. xs!ixs0!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 (lh  hlength xs0  h-l4);
  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!ixs1!l)  xs!lxs1!l);
  ASSERT (i{l..<m}. xs!ixs1!l);
  ASSERT (i{m..<h}. xs1!lxs!i);
  
  
  RETURN (xs,m)
}"

lemma slice_LT_I_aux:
  assumes B: "l<m" "m<h" "hlength xs"
  assumes BND: "i{l..<m}. xs!ip" "i{m..<h}. pxs!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 (lipi); 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(pihi); 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  hi0length xs0);
    
    ― ‹Initialize
    li  qsp_next_l_param cparam xs0 pi li0 hi0;
    hi  qsp_next_h_param cparam xs0 pi hi0;
    
    ASSERT (li0hi);
    
    (xs,li,hi)  WHILEIT 
      (λ_. True)
      (λ(xs,li,hi). li<hi) 
      (λ(xs,li,hi). doN {
        ASSERT(li<hi  li<length xs  hi<length xs  lihi);
        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 (lh  hlength xs0  h-l4);
    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