Theory IICF_Array

theory IICF_Array
imports "../Intf/IICF_List" 
begin

(* TODO: Move *)
    lemma list_rel_take: "(xs,ys)Alist_rel  (take n xs, take n ys)  Alist_rel"  
      unfolding list_rel_def by auto
      
    lemma list_rel_drop: "(xs,ys)Alist_rel  (drop n xs, drop n ys)  Alist_rel"  
      unfolding list_rel_def by auto
      
    lemma list_rel_append: "(xs1,ys1) Alist_rel  (xs2,ys2) Alist_rel  (xs1@xs2,ys1@ys2) Alist_rel"  
      unfolding list_rel_def 
      using list_all2_appendI by blast
    


section Plain Arrays Implementing List Interface

subsection Abstract Replicate-Init Operation
  definition [simp]: "replicate_init_raw n  replicate n init"

  locale replicate_init = 
    fixes repl :: "'a  nat  'a list"  
    assumes repl_def[simp]: "repl i n = replicate n i"
  begin
  
    context fixes i::'a begin
      sepref_register "repl i" 
    end
    
    lemma replicate_init_param:
      fixes A :: "'a  'c::llvm_rep  assn"
      assumes INIT: "GEN_ALGO i (is_init A)"
      shows "(RETURN o replicate_init_raw, RETURN o PR_CONST (repl i))  nat_rel f the_pure Alist_relnres_rel"
    proof -
      from INIT have [param]: "(init,i)  the_pure A" unfolding is_init_def GEN_ALGO_def by simp
      show ?thesis
        unfolding repl_def replicate_init_raw_def PR_CONST_def 
        apply (rule frefI)
        apply (parametricity)
        done
        
    qed
    
    lemma fold_replicate_init: "replicate n i = repl i n" by simp
  end

subsection Abstract grow-init Operation

  definition [simp]: "op_list_grow_init i ns os xs  take os xs @ replicate (ns - os) i" 
  context fixes i begin
    sepref_register "op_list_grow_init i"
  end

  definition [simp]: "grow_init_raw ns os xs  take os xs @ replicate (ns - os) init"

  lemma grow_init_param:
    fixes A :: "'a  'c::llvm_rep  assn"
    assumes INIT: "GEN_ALGO i (is_init A)"
    shows "(uncurry2 (RETURN ooo grow_init_raw), uncurry2 (RETURN ooo PR_CONST (op_list_grow_init i)))  [λ_. True]f (nat_rel ×r nat_rel) ×r the_pure Alist_rel  the_pure Alist_relnres_rel"
  proof -  
    from INIT have [param]: "(init,i)  the_pure A" unfolding is_init_def GEN_ALGO_def by simp
    have "(grow_init_raw, op_list_grow_init i)  nat_rel  nat_rel  the_pure Alist_rel  the_pure Alist_rel"
      unfolding op_list_grow_init_def grow_init_raw_def
      by parametricity
    from this[to_fref] show ?thesis unfolding PR_CONST_def  
      by (auto intro!: frefI nres_relI dest!: frefD)
      
  qed
  
  
    
    
  sepref_decl_op list_free: "λ_::_ list. ()" :: "Alist_rel  unit_rel" .

  

subsection Definition of Assertion

  text Lists of fixed length are directly implemented with arrays. 
  
  hide_const (open) LLVM_DS_Array.array_assn
  
  abbreviation "raw_array_assn  LLVM_DS_NArray.narray_assn"

  definition array_assn where "array_assn A  hr_comp raw_array_assn (the_pure Alist_rel)"
  lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure "array_assn A" for A]

  lemma array_assn_comp: "hr_comp (array_assn id_assn) (the_pure Alist_rel) = array_assn (A)"
    unfolding array_assn_def by simp
  
  
subsection Interface Implementation  
    
definition [simp]: "array_replicate_init i n  replicate n i"
interpretation array: replicate_init array_replicate_init by unfold_locales simp




context 
  notes [fcomp_norm_unfold] = array_assn_def[symmetric] array_assn_comp
  (*notes [simp] = pure_def hn_ctxt_def is_array_def invalid_assn_def*)
begin  

  lemma array_get_hnr_aux: "(uncurry array_nth,uncurry (RETURN oo op_list_get)) 
     [λ(l,i). i<length l]a raw_array_assnk *a snat_assnk  id_assn"  
    unfolding snat_rel_def snat.assn_is_rel[symmetric]
    apply sepref_to_hoare
    apply vcg'
    done
    
  sepref_decl_impl array_get: array_get_hnr_aux .  

  lemma array_set_hnr_aux: "(uncurry2 array_upd,uncurry2 (RETURN ooo op_list_set)) 
     [λ((l,i),_). i<length l]a [λ_. True]c raw_array_assnd *a snat_assnk *a id_assnk 
      d (λ_. raw_array_assn) [λ((ai,_),_) r. r=ai]c"  
    unfolding snat_rel_def snat.assn_is_rel[symmetric] 
    apply sepref_to_hoare
    apply (clarsimp simp: invalid_assn_def)
    apply (rule htriple_pure_preI, ((determ drule pure_part_split_conj|erule conjE)+)?)
    apply vcg
    done
    
  sepref_decl_impl array_set: array_set_hnr_aux .

  sepref_definition array_swap [llvm_code] is "uncurry2 (mop_list_swap)" 
    :: "[λ_. True]c (array_assn id_assn)d *a (snat_assn)k *a (snat_assn)k 
       array_assn id_assn [λ((ai,_),_) r. r=ai]c"
    unfolding gen_mop_list_swap by sepref
    
  sepref_decl_impl (ismop) array_swap.refine .
  
    
  lemma hn_array_repl_init_raw:
    shows "(narray_new TYPE('c::llvm_rep),RETURN o replicate_init_raw)  snat_assnk a raw_array_assn"
    unfolding snat_rel_def snat.assn_is_rel[symmetric]
    apply sepref_to_hoare
    apply vcg'
    done

  sepref_decl_impl (no_mop) hn_array_repl_init_raw uses array.replicate_init_param . 
  
  lemma hn_array_grow_init_raw:
    shows "(uncurry2 array_grow, uncurry2 (RETURN ooo grow_init_raw)) 
       [λ((ns,os),xs). oslength xs  osns]a snat_assnk *a snat_assnk *a raw_array_assnd  raw_array_assn"
    unfolding snat_rel_def snat.assn_is_rel[symmetric]
    apply sepref_to_hoare
    by vcg'
    
  sepref_decl_impl (no_mop) hn_array_grow_init_raw uses grow_init_param .
  
  sepref_decl_op array_custom_replicate: op_list_replicate :: "nat_rel  A  Alist_rel" .
  
  lemma hn_array_replicate_new_raw:
    "(uncurry narray_new_init, uncurry (RETURN oo op_array_custom_replicate))  snat_assnk *a id_assnk a raw_array_assn"
    unfolding snat_rel_def snat.assn_is_rel[symmetric]
    apply sepref_to_hoare
    by vcg
    
  sepref_decl_impl hn_array_replicate_new_raw .
  
  lemma array_fold_custom_replicate: 
    "replicate = op_array_custom_replicate"
    "op_list_replicate = op_array_custom_replicate"
    "mop_list_replicate = mop_array_custom_replicate"
    by (auto del: ext intro!: ext)
  
  lemma hn_array_free_raw: "(narray_free,RETURN o op_list_free)  raw_array_assnd a unit_assn"
    by sepref_to_hoare vcg
  
  sepref_decl_impl array_free: hn_array_free_raw .
  lemmas array_mk_free[sepref_frame_free_rules] = hn_MK_FREEI[OF array_free_hnr]
  
end  
  
section Array Slice

subsection Definition of Assertion

  text Lists of fixed length are directly implemented with arrays. 
  
  hide_const (open) LLVM_DS_Array.array_assn
  
  abbreviation "raw_array_slice_assn  LLVM_DS_NArray.array_slice_assn"

  definition array_slice_assn where "array_slice_assn A  hr_comp raw_array_slice_assn (the_pure Alist_rel)"
  lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure "array_slice_assn A" for A]

  lemma array_slice_assn_comp: "hr_comp (array_slice_assn id_assn) (the_pure Alist_rel) = array_slice_assn (A)"
    unfolding array_slice_assn_def by simp
  
  
subsection Interface Implementation  

context 
  notes [fcomp_norm_unfold] = array_slice_assn_def[symmetric] array_slice_assn_comp
  (*notes [simp] = pure_def hn_ctxt_def is_array_def invalid_assn_def*)
begin  

  lemma array_slice_get_hnr_aux: "(uncurry array_nth,uncurry (RETURN oo op_list_get)) 
     [λ(l,i). i<length l]a raw_array_slice_assnk *a snat_assnk  id_assn"  
    unfolding snat_rel_def snat.assn_is_rel[symmetric]
    apply sepref_to_hoare
    apply vcg'
    done
    
  sepref_decl_impl array_slice_get: array_slice_get_hnr_aux .  

  lemma array_slice_set_hnr_aux: "(uncurry2 array_upd,uncurry2 (RETURN ooo op_list_set)) 
     [λ((l,i),_). i<length l]a [λ_. True]c raw_array_slice_assnd *a snat_assnk *a id_assnk 
    d (λ_. raw_array_slice_assn) [λ((ai,_),_) r. r=ai]c"  
    unfolding snat_rel_def snat.assn_is_rel[symmetric] 
    apply sepref_to_hoare
    apply (clarsimp simp: invalid_assn_def)
    apply (rule htriple_pure_preI, ((determ drule pure_part_split_conj|erule conjE)+)?)
    apply vcg
    done
    
  sepref_decl_impl array_slice_set: array_slice_set_hnr_aux .

  sepref_definition array_slice_swap [llvm_code] is "uncurry2 (mop_list_swap)" 
    :: "[λ_. True]c (array_slice_assn id_assn)d *a (snat_assn)k *a (snat_assn)k 
       array_slice_assn id_assn [λ((ai,_),_) r. r=ai]c"
    unfolding gen_mop_list_swap by sepref
    
  sepref_decl_impl (ismop) array_slice_swap.refine .
  
  definition ars_split :: "_ word  'a::llvm_rep ptr  ('a ptr × 'a ptr) llM" 
    where [llvm_inline]: "ars_split i p  doM { p2  ll_ofs_ptr p i; Mreturn (p,p2)}"
  definition ars_join :: "'a::llvm_rep ptr  'a ptr  'a ptr llM" 
    where [llvm_inline]: "ars_join p1 p2  Mreturn p1"
  
  context begin
    interpretation llvm_prim_mem_setup .  
    interpretation llvm_prim_arith_setup .  

    (* TODO: Move *)
    lemma in_snat_rel_int: "(ii,i)snat_rel  sint ii = int i"
      by (metis cnv_snat_to_uint(2) in_br_conv snat.rel_def snat_eq_unat(2) snat_rel_def uint_nat)
    
    lemma ll_ofs_ptr_raw_array_slice_rl[vcg_rules]:
      assumes A: "i<length a"
      shows "llvm_htriple (snat_assn i ii ** raw_array_slice_assn a ai) (ll_ofs_ptr ai ii) (λr. (r=ai+aint i) ** snat_assn i ii ** raw_array_slice_assn a ai)"
      unfolding LLVM_DS_NArray.array_slice_assn_def
      apply (subgoal_tac "a[]")
      subgoal
        apply simp
        supply [simp] = in_snat_rel_int A
        by vcg
      subgoal using A by simp
      done
      
    definition "ars_joinable ai1 ai2 n  ai2 = ai1 +a int n"    
    lemma ars_join_rl[vcg_rules]:
      shows "llvm_htriple 
        (raw_array_slice_assn a1 ai1 ** raw_array_slice_assn a2 ai2 ** !(ars_joinable ai1 ai2 (length a1))) 
        (ars_join ai1 ai2) 
        (λr. (r=ai1) ** raw_array_slice_assn (a1@a2) ai1)"    
      unfolding ars_join_def
      supply [simp] = array_slice_assn_split
      unfolding ars_joinable_def
      by vcg  
        
    lemma ars_split_rl[vcg_rules]:
      "llvm_htriple 
        (snat_assn i ii ** raw_array_slice_assn a ai ** d(i < length a)) 
        (ars_split ii ai)
        (λ(a1,a2). raw_array_slice_assn (take i a) a1 ** raw_array_slice_assn (drop i a) a2 ** snat_assn i ii ** (a1=ai  ars_joinable a1 a2 i))"
      unfolding ars_split_def ars_joinable_def
      apply vcg
      apply (subst append_take_drop_id[symmetric, where n=i])
      apply (subst array_slice_assn_split)
      apply vcg_try_solve
      done
  
      
    definition "WITH_SPLIT i xs m  doN {
      ASSERT (i<length xs);
      let xs1 = take i xs;
      let xs2 = drop i xs;
      (r,xs1',xs2')  m xs1 xs2;
      ASSERT (length xs1' = length xs1  length xs2'=length xs2);
      RETURN (r,xs1'@xs2')
    }"  
    
    (* Monotonicity setup *)
    lemma WITH_SPLIT_mono[refine_mono]: 
      "a b. f a b  f' a b  WITH_SPLIT xs n f  WITH_SPLIT xs n f'"
      unfolding WITH_SPLIT_def
      by refine_mono
    
    (* Monadifier setup *)
    lemma WITH_SPLIT_arity[sepref_monadify_arity]: "WITH_SPLIT  λ2xs n f. SP WITH_SPLIT$xs$n$(λ2a b. f$a$b)"
      by simp
    
    lemma WITH_SPLIT_comb[sepref_monadify_comb]:  
      "WITH_SPLIT$xs$n$f = Refine_Basic.bind$(EVAL$xs)$(λ2xs. Refine_Basic.bind$(EVAL$n)$(λ2n. SP WITH_SPLIT$xs$n$f))"
      by simp
    
    lemma WITH_SPLIT_mono_flat[refine_mono]: 
      "a b. flat_ge (f a b) (f' a b)  flat_ge (WITH_SPLIT xs n f) (WITH_SPLIT xs n f')"
      unfolding WITH_SPLIT_def
      by refine_mono
    
    lemma WITH_SPLIT_rule[refine_vcg]:
      assumes "n<length xs"
      assumes "xs1 xs2. xs=xs1@xs2; length xs1=n   
        m xs1 xs2  SPEC (λ(r',xs1',xs2'). 
                      length xs1'=length xs1 
                     length xs2'=length xs2 
                     P (r', xs1'@xs2'))"
      shows "WITH_SPLIT n xs m  SPEC P"  
      using assms(1) unfolding WITH_SPLIT_def
      apply (refine_vcg assms(2)[of "take n xs" "drop n xs"])
      apply auto
      done

    lemma WITH_split_refine[refine]:
      assumes "(n',n)Id"
      assumes "(xs',xs)  Alist_rel"
      assumes [refine]: "n < length xs; n' < length xs'  m' (take n' xs') (drop n' xs')  (R×rAlist_rel×rAlist_rel) (m (take n xs) (drop n xs))"
      shows "WITH_SPLIT n' xs' m' (R ×r Alist_rel) (WITH_SPLIT n xs m)"
      unfolding WITH_SPLIT_def
      apply refine_rcg
      using assms(1,2)
      apply (auto simp: list_rel_imp_same_length list_rel_append)
      done
      

      
      
      
    thm sepref_monadify_comb  
      
      
    definition [llvm_inline]: "ars_with_split i a m  doM {
      (a1,a2)  ars_split i a;
      (r,_,_)  m a1 a2;
      ars_join a1 a2;
      Mreturn (r,a)
    }"

    lemma ars_with_split_for_paper: "ars_with_split i a m = doM {
      p2  ll_ofs_ptr a i;
      (r, _, _)  m a p2;
      Mreturn (r, a)
    }"
      unfolding ars_with_split_def ars_split_def ars_join_def
      by simp
    
      
    (* Monotonicity setup *)
    lemma ars_with_split_mono[partial_function_mono]:
      assumes "xs1 xs2. M_mono' (λD. m D xs1 xs2)"
      shows "M_mono' (λD. ars_with_split i a (m D))"
      unfolding ars_with_split_def using assms
      by pf_mono_prover
    

    lemma hn_WITH_SPLIT_aux:
      assumes MHN: "xs1 xsi1 xs2 xsi2. hn_refine (raw_array_slice_assn xs1 xsi1 ** raw_array_slice_assn xs2 xsi2 ** F) (mi xsi1 xsi2) (F') (R ×a raw_array_slice_assn ×a raw_array_slice_assn) (CP' xsi1 xsi2) (m xs1 xs2)"
      assumes CP': "xsi1 xsi2 ri xsi1' xsi2'. CP' xsi1 xsi2 (ri,xsi1',xsi2')  xsi1'=xsi1  xsi2'=xsi2  CP ri"
      shows "hn_refine 
        (raw_array_slice_assn xs xsi ** snat_assn n ni ** F) 
        (ars_with_split ni xsi mi) 
        (snat_assn n ni) 
        (λ(r,xs) (ri,xsi). R r ri ** raw_array_slice_assn xs xsi ** F') 
        (λ(ri,xsi'). xsi'=xsi  CP ri) 
        (WITH_SPLIT n xs m)"  
      apply (sepref_to_hoare)
      unfolding ars_with_split_def WITH_SPLIT_def
      
      supply [simp del] = List.take_all List.drop_all
      supply [simp] = pure_def refine_pw_simps
      
      apply (clarsimp simp: )
      
      supply [vcg_rules] = hn_refineD[OF MHN]
      
      apply vcg
      apply (drule CP')
      apply (fold inres_def)
      apply vcg
      done

    lemma hn_WITH_SPLIT_simplified:
      assumes MHN: "xs1 xsi1 xs2 xsi2. 
        hn_refine (raw_array_slice_assn xs1 xsi1 ** raw_array_slice_assn xs2 xsi2) 
                  (mi xsi1 xsi2) 
                  () 
                  (R ×a raw_array_slice_assn ×a raw_array_slice_assn) 
                  (λ(ri,xsi1',xsi2'). xsi1'=xsi1  xsi2' = xsi2) 
                  (m xs1 xs2)"
      shows "hn_refine 
        (raw_array_slice_assn xs xsi ** snat_assn n ni) 
        (ars_with_split ni xsi mi) 
        (snat_assn n ni) 
        (λ(r,xs) (ri,xsi). R r ri ** raw_array_slice_assn xs xsi) 
        (λ(ri,xsi'). xsi'=xsi) 
        (WITH_SPLIT n xs m)"  
      using hn_WITH_SPLIT_aux[where 
        F= and F'= and
        CP'="λxsi1 xsi2 (ri,xsi1',xsi2'). xsi1'=xsi1  xsi2' = xsi2" and
        CP="λ_. True"] MHN
      apply (simp add: sep_algebra_simps) 
      by blast
      
      
    (*  
    lemma hn_WITH_SPLIT_array_slice:
      assumes MHN: "⋀xs1 xs2 xsi2. hn_refine 
        (hn_ctxt (array_slice_assn A) xs1 xsi ** hn_ctxt (array_slice_assn A) xs2 xsi2 ** F) 
        (mi xsi xsi2) (F') 
        (R ×a array_slice_assn A ×a array_slice_assn A) 
        (CP' xsi xsi2) 
        (m xs1 xs2)"
      assumes CP': "⋀xsi2 ri xsi1' xsi2'. CP' xsi xsi2 (ri,xsi1',xsi2') ⟹ xsi1'=xsi ∧ xsi2'=xsi2 ∧ CP ri"
      shows "hn_refine 
        (hn_ctxt (array_slice_assn A) xs xsi ** hn_ctxt snat_assn n ni ** F) 
        (ars_with_split ni xsi mi) 
        (hn_ctxt snat_assn n ni ** F') 
        (R ×a array_slice_assn A) 
        (λ(ri,xsi'). xsi'=xsi ∧ CP ri) 
        (WITH_SPLIT n xs m)"  
      apply (sepref_to_hoare)
      unfolding ars_with_split_def WITH_SPLIT_def array_slice_assn_def hr_comp_def
      
      supply [simp del] = List.take_all List.drop_all
      supply [simp] = pure_def refine_pw_simps list_rel_imp_same_length
      supply [elim] = list_rel_take list_rel_drop list_rel_append
      
      apply (clarsimp simp: )
      
      supply R = hn_refineD[OF MHN, unfolded hn_ctxt_def array_slice_assn_def hr_comp_def prod_assn_def]
      thm R
      supply [vcg_rules] = R
      
      apply vcg
      apply (drule CP')
      apply (fold inres_def)
      apply vcg
      done
    *)
      
    lemma hn_WITH_SPLIT_template_aux:
      assumes sl_assn_def: "sl_assn = hr_comp raw_array_slice_assn (Alist_rel)"
      assumes MHN: "xs1 xs2 xsi2. hn_refine 
        (hn_ctxt (sl_assn) xs1 xsi ** hn_ctxt (sl_assn) xs2 xsi2 ** hn_ctxt snat_assn n ni ** F) 
        (mi xsi xsi2) (F') 
        (R ×a sl_assn ×a sl_assn) 
        (CP' xsi xsi2) 
        (m xs1 xs2)"
      assumes CP': "xsi2 ri xsi1' xsi2'. CP' xsi xsi2 (ri,xsi1',xsi2')  xsi1'=xsi  xsi2'=xsi2  CP ri"
      shows "hn_refine 
        (hn_ctxt (sl_assn) xs xsi ** hn_ctxt snat_assn n ni ** F) 
        (ars_with_split ni xsi mi) 
        (hn_ctxt snat_assn n ni ** F') 
        (R ×a sl_assn) 
        (λ(ri,xsi'). xsi'=xsi  CP ri) 
        (WITH_SPLIT n xs m)"  
      apply (sepref_to_hoare)
      unfolding ars_with_split_def WITH_SPLIT_def sl_assn_def hr_comp_def
      
      supply [simp del] = List.take_all List.drop_all
      supply [simp] = pure_def refine_pw_simps list_rel_imp_same_length
      supply [elim] = list_rel_take list_rel_drop list_rel_append
      
      apply (clarsimp simp: )
      
      supply R = hn_refineD[OF MHN, unfolded hn_ctxt_def sl_assn_def hr_comp_def prod_assn_def]
      thm R
      supply [vcg_rules] = R
      
      apply vcg
      apply (drule CP')
      apply (fold inres_def)
      apply vcg
      done
      
      
      
    lemma hn_WITH_SPLIT_template: 
      assumes sl_assn_def: "sl_assn = hr_comp raw_array_slice_assn (Alist_rel)"
      assumes FR: "Γ  hn_ctxt sl_assn xs xsi ** hn_ctxt snat_assn n ni ** Γ1"
      assumes HN: "xs1 xsi1 xs2 xsi2.  CP_assm (xsi1 = xsi)   hn_refine 
        (hn_ctxt sl_assn xs1 xsi1 ** hn_ctxt sl_assn xs2 xsi2 ** hn_ctxt snat_assn n ni ** Γ1) 
        (mi xsi1 xsi2) 
        (Γ2 xs1 xsi1 xs2 xsi2) (R) (CP xsi1 xsi2) (m xs1 xs2)"
      assumes CP: "xsi2 ri' xsi1' xsi2'. CP_assm (CP xsi xsi2 (ri',xsi1',xsi2'))  CP_cond (xsi1' = xsi  xsi2'=xsi2)"  
      assumes FR2: "xs1 xsi1 xs2 xsi2. Γ2 xs1 xsi1 xs2 xsi2 
        hn_invalid sl_assn xs1 xsi1 ** hn_invalid sl_assn xs2 xsi2 ** Γ1'"
      assumes FR3: "x xi. hn_ctxt R x xi  hn_ctxt (R' ×a sl_assn ×a sl_assn) x xi"  
        
      (*  
      assumes FR3: "⋀xs1' xsi1' xs2' xsi2' r' ri'. hn_ctxt R (r',xs1',xs2') (ri',xsi1',xsi2') ⊢
        hn_ctxt R' r' ri' ** hn_ctxt (array_slice_assn A) xs1' xsi1' ** hn_ctxt (array_slice_assn A) xs2' xsi2'" *)
      assumes CP2: "xsi2. CP_simplify (CP_EX32 (CP xsi xsi2)) (CP')"  
      shows "hn_refine 
        (Γ) 
        (ars_with_split ni xsi mi) 
        (hn_invalid sl_assn xs xsi ** Γ1') 
        (R' ×a sl_assn) 
        (CP') 
        (WITH_SPLIT$n$xs$(λ2a b. m a b))"  
      unfolding autoref_tag_defs PROTECT2_def
      apply (rule hn_refine_cons_pre)
      applyS (rule FR)
      apply1 extract_hnr_invalids
      supply R = hn_WITH_SPLIT_template_aux[OF sl_assn_def,where CP="λri. xsi2 xsi2'. CP xsi xsi2 (ri,xsi,xsi2')"]
      thm R
      apply (rule hn_refine_cons_cp[OF _ R])
      applyS (fri)
      apply1 extract_hnr_invalids
      apply (rule hn_refine_cons[OF _ HN])
      applyS (fri)
      applyS (simp add: CP_defs)
      applyS (sep_drule FR2; simp; rule entails_refl)
      focus
        apply clarsimp
        apply (sep_drule FR3[unfolded hn_ctxt_def])
        apply simp
        apply (rule entails_refl)
        solved
      focus
        using CP unfolding CP_defs apply blast solved
      applyS (simp add: hn_ctxt_def invalid_pure_recover)
      applyS (rule entails_refl)
      focus
        using CP2 unfolding CP_defs apply blast solved
      done  

      
    lemma hn_WITH_SPLIT_array_slice[sepref_comb_rules]: 
      assumes FR: "Γ  hn_ctxt (array_slice_assn A) xs xsi ** hn_ctxt snat_assn n ni ** Γ1"
      assumes HN: "xs1 xsi1 xs2 xsi2.  CP_assm (xsi1 = xsi)   hn_refine 
        (hn_ctxt (array_slice_assn A) xs1 xsi1 ** hn_ctxt (array_slice_assn A) xs2 xsi2 ** hn_ctxt snat_assn n ni ** Γ1) 
        (mi xsi1 xsi2) 
        (Γ2 xs1 xsi1 xs2 xsi2) (R) (CP xsi1 xsi2) (m xs1 xs2)"
      assumes CP: "xsi2 ri' xsi1' xsi2'. CP_assm (CP xsi xsi2 (ri',xsi1',xsi2'))  CP_cond (xsi1' = xsi  xsi2'=xsi2)"  
      assumes FR2: "xs1 xsi1 xs2 xsi2. Γ2 xs1 xsi1 xs2 xsi2 
        hn_invalid (array_slice_assn A) xs1 xsi1 ** hn_invalid (array_slice_assn A) xs2 xsi2 ** Γ1'"
      assumes FR3: "x xi. hn_ctxt R x xi  hn_ctxt (R' ×a array_slice_assn A ×a array_slice_assn A) x xi"  
        
      (*  
      assumes FR3: "⋀xs1' xsi1' xs2' xsi2' r' ri'. hn_ctxt R (r',xs1',xs2') (ri',xsi1',xsi2') ⊢
        hn_ctxt R' r' ri' ** hn_ctxt (array_slice_assn A) xs1' xsi1' ** hn_ctxt (array_slice_assn A) xs2' xsi2'" *)
      assumes CP2: "xsi2. CP_simplify (CP_EX32 (CP xsi xsi2)) (CP')"  
      shows "hn_refine 
        (Γ) 
        (ars_with_split ni xsi mi) 
        (hn_invalid (array_slice_assn A) xs xsi ** Γ1') 
        (R' ×a array_slice_assn A) 
        (CP') 
        (WITH_SPLIT$n$xs$(λ2a b. m a b))"  
        
      apply (rule hn_WITH_SPLIT_template[of "array_slice_assn A", OF _ assms]; assumption?)
      unfolding array_slice_assn_def ..


      
      
      
      
    definition "WITH_SPLIT_ro i xs m  doN {
      ASSERT (i<length xs);
      let xs1 = take i xs;
      let xs2 = drop i xs;
      m xs1 xs2
    }"  
    
    (* Monotonicity setup *)
    lemma WITH_SPLIT_ro_mono[refine_mono]: 
      "a b. f a b  f' a b  WITH_SPLIT_ro xs n f  WITH_SPLIT_ro xs n f'"
      unfolding WITH_SPLIT_ro_def
      by refine_mono
    
    (* Monadifier setup *)
    lemma WITH_SPLIT_ro_arity[sepref_monadify_arity]: "WITH_SPLIT_ro  λ2xs n f. SP WITH_SPLIT_ro$xs$n$(λ2a b. f$a$b)"
      by simp
    
    lemma WITH_SPLIT_ro_comb[sepref_monadify_comb]:  
      "WITH_SPLIT_ro$xs$n$f = Refine_Basic.bind$(EVAL$xs)$(λ2xs. Refine_Basic.bind$(EVAL$n)$(λ2n. SP WITH_SPLIT_ro$xs$n$f))"
      by simp
    
    lemma WITH_SPLIT_ro_mono_flat[refine_mono]: 
      "a b. flat_ge (f a b) (f' a b)  flat_ge (WITH_SPLIT_ro xs n f) (WITH_SPLIT_ro xs n f')"
      unfolding WITH_SPLIT_ro_def
      by refine_mono
    
    lemma WITH_SPLIT_ro_rule[refine_vcg]:
      assumes "n<length xs"
      assumes "xs1 xs2. xs=xs1@xs2; length xs1=n   m xs1 xs2  SPEC P"
      shows "WITH_SPLIT_ro n xs m  SPEC P"  
      using assms(1) unfolding WITH_SPLIT_ro_def
      apply (refine_vcg assms(2)[of "take n xs" "drop n xs"])
      apply auto
      done

    lemma WITH_ro_split_refine[refine]:
      assumes "(n',n)Id"
      assumes "(xs',xs)  Alist_rel"
      assumes [refine]: "n < length xs; n' < length xs'  m' (take n' xs') (drop n' xs')  R (m (take n xs) (drop n xs))"
      shows "WITH_SPLIT_ro n' xs' m' R (WITH_SPLIT_ro n xs m)"
      unfolding WITH_SPLIT_ro_def
      apply refine_rcg
      using assms(1,2)
      apply (auto simp: list_rel_imp_same_length list_rel_append)
      done
      

    definition [llvm_inline]: "ars_with_split_ro i a m  doM {
      (a1,a2)  ars_split i a;
      r  m a1 a2;
      ars_join a1 a2;
      Mreturn r
    }"
      
    (* Monotonicity setup *)
    lemma ars_with_split_ro_mono[partial_function_mono]:
      assumes "xs1 xs2. M_mono' (λD. m D xs1 xs2)"
      shows "M_mono' (λD. ars_with_split_ro i a (m D))"
      unfolding ars_with_split_ro_def using assms
      by pf_mono_prover
    

    lemma hn_WITH_SPLIT_ro_aux:
      assumes MHN: "xs1 xsi1 xs2 xsi2. hn_refine (raw_array_slice_assn xs1 xsi1 ** raw_array_slice_assn xs2 xsi2 ** F) (mi xsi1 xsi2) (raw_array_slice_assn xs1 xsi1 ** raw_array_slice_assn xs2 xsi2 ** F') R (CP' xsi1 xsi2) (m xs1 xs2)"
      assumes CP': "xsi1 xsi2 ri. CP' xsi1 xsi2 ri  CP ri"
      shows "hn_refine 
        (raw_array_slice_assn xs xsi ** snat_assn n ni ** F) 
        (ars_with_split_ro ni xsi mi) 
        (raw_array_slice_assn xs xsi ** snat_assn n ni ** F') 
        R 
        CP 
        (WITH_SPLIT_ro n xs m)"  
      apply (sepref_to_hoare)
      unfolding ars_with_split_ro_def WITH_SPLIT_ro_def
      
      supply [simp del] = List.take_all List.drop_all
      supply [simp] = pure_def refine_pw_simps
      
      apply (clarsimp simp: )
      
      supply [vcg_rules] = hn_refineD[OF MHN]
      
      apply vcg
      apply (drule CP')
      apply (fold inres_def)
      apply vcg
      done

    lemma hn_WITH_SPLIT_ro_simplified:
      assumes MHN: "xs1 xsi1 xs2 xsi2. 
        hn_refine (raw_array_slice_assn xs1 xsi1 ** raw_array_slice_assn xs2 xsi2) 
                  (mi xsi1 xsi2) 
                  (raw_array_slice_assn xs1 xsi1 ** raw_array_slice_assn xs2 xsi2) 
                  R
                  (λ_. True) 
                  (m xs1 xs2)"
      shows "hn_refine 
        (raw_array_slice_assn xs xsi ** snat_assn n ni) 
        (ars_with_split_ro ni xsi mi) 
        (raw_array_slice_assn xs xsi ** snat_assn n ni) 
        R 
        (λ_. True)  
        (WITH_SPLIT_ro n xs m)"  
      using hn_WITH_SPLIT_ro_aux[where 
        F= and F'= and
        CP'="λ_ _ _. True" and
        CP="λ_. True"] MHN
      apply (simp add: sep_algebra_simps) 
      by blast
      
      
    lemma WITH_SPLIT_aux_append_list_rel: " (xsi1,take n xs)Alist_rel; (xsi2,drop n xs)Alist_rel   (xsi1@xsi2,xs)  Alist_rel"  
      by (metis atd_lem list_rel_append)
      
    lemma hn_WITH_SPLIT_ro_template_aux:
      assumes sl_assn_def: "sl_assn = hr_comp raw_array_slice_assn (Alist_rel)"
      assumes MHN: "xs1 xs2 xsi2. hn_refine 
        (hn_ctxt (sl_assn) xs1 xsi ** hn_ctxt (sl_assn) xs2 xsi2 ** hn_ctxt snat_assn n ni ** F) 
        (mi xsi xsi2) (hn_ctxt (sl_assn) xs1 xsi ** hn_ctxt (sl_assn) xs2 xsi2 ** F') 
        (R) 
        (CP' xsi xsi2) 
        (m xs1 xs2)"
      assumes CP': "ri xsi2. CP' xsi xsi2 ri  CP ri"
      shows "hn_refine 
        (hn_ctxt (sl_assn) xs xsi ** hn_ctxt snat_assn n ni ** F) 
        (ars_with_split_ro ni xsi mi) 
        (hn_ctxt (sl_assn) xs xsi ** hn_ctxt snat_assn n ni ** F') 
        R
        CP 
        (WITH_SPLIT_ro n xs m)"  
      apply (sepref_to_hoare)
      unfolding ars_with_split_ro_def WITH_SPLIT_ro_def sl_assn_def hr_comp_def
      
      supply [simp del] = List.take_all List.drop_all
      supply [simp] = pure_def refine_pw_simps list_rel_imp_same_length WITH_SPLIT_aux_append_list_rel
      supply [elim] = list_rel_take list_rel_drop list_rel_append
      
      apply (clarsimp simp: )
      
      supply R = hn_refineD[OF MHN, unfolded hn_ctxt_def sl_assn_def hr_comp_def prod_assn_def]
      thm R
      supply [vcg_rules] = R
      
      apply vcg
      apply (drule CP')
      apply (fold inres_def)
      apply vcg
      done
      
      
    lemma hn_WITH_SPLIT_ro_template: 
      assumes sl_assn_def: "sl_assn = hr_comp raw_array_slice_assn (Alist_rel)"
      assumes FR: "Γ  hn_ctxt sl_assn xs xsi ** hn_ctxt snat_assn n ni ** Γ1"
      assumes HN: "xs1 xsi1 xs2 xsi2.  CP_assm (xsi1 = xsi)   hn_refine 
        (hn_ctxt sl_assn xs1 xsi1 ** hn_ctxt sl_assn xs2 xsi2 ** hn_ctxt snat_assn n ni ** Γ1) 
        (mi xsi1 xsi2) 
        (Γ2 xs1 xsi1 xs2 xsi2) (R) (CP xsi1 xsi2) (m xs1 xs2)"
      assumes FR2: "xs1 xsi1 xs2 xsi2. Γ2 xs1 xsi1 xs2 xsi2 
        hn_ctxt sl_assn xs1 xsi1 ** hn_ctxt sl_assn xs2 xsi2 ** Γ1'"
        
      assumes CP2: "xsi2. CP_simplify (CP xsi xsi2) (CP')"  
      shows "hn_refine 
        (Γ) 
        (ars_with_split_ro ni xsi mi) 
        (hn_ctxt sl_assn xs xsi ** Γ1') 
        R
        (CP') 
        (WITH_SPLIT_ro$n$xs$(λ2a b. m a b))"  
      unfolding autoref_tag_defs PROTECT2_def
      apply (rule hn_refine_cons_pre)
      applyS (rule FR)
      apply1 extract_hnr_invalids
      supply R = hn_WITH_SPLIT_ro_template_aux[OF sl_assn_def, where CP=CP']
      thm R
      apply (rule hn_refine_cons_cp[OF _ R])
      applyS (fri)
      apply1 extract_hnr_invalids
      apply (rule hn_refine_cons[OF _ HN])
      applyS (fri)
      applyS (simp add: CP_defs)
      applyS (sep_drule FR2; simp; rule entails_refl)
      applyS(rule entails_refl)
      focus using CP2 unfolding CP_defs apply blast solved
      applyS (simp add: hn_ctxt_def invalid_pure_recover)
      applyS (rule entails_refl)
      applyS blast
      done  

      
    lemma hn_WITH_SPLIT_ro_array_slice[sepref_comb_rules]: 
      assumes FR: "Γ  hn_ctxt (array_slice_assn A) xs xsi ** hn_ctxt snat_assn n ni ** Γ1"
      assumes HN: "xs1 xsi1 xs2 xsi2.  CP_assm (xsi1 = xsi)   hn_refine 
        (hn_ctxt (array_slice_assn A) xs1 xsi1 ** hn_ctxt (array_slice_assn A) xs2 xsi2 ** hn_ctxt snat_assn n ni ** Γ1) 
        (mi xsi1 xsi2) 
        (Γ2 xs1 xsi1 xs2 xsi2) (R) (CP xsi1 xsi2) (m xs1 xs2)"
      assumes FR2: "xs1 xsi1 xs2 xsi2. Γ2 xs1 xsi1 xs2 xsi2 
        hn_ctxt (array_slice_assn A) xs1 xsi1 ** hn_ctxt (array_slice_assn A) xs2 xsi2 ** Γ1'"
        
      assumes CP2: "xsi2. CP_simplify (CP xsi xsi2) (CP')"  
      shows "hn_refine 
        (Γ) 
        (ars_with_split_ro ni xsi mi) 
        (hn_ctxt (array_slice_assn A) xs xsi ** Γ1') 
        (R) 
        (CP') 
        (WITH_SPLIT_ro$n$xs$(λ2a b. m a b))"  
        
      apply (rule hn_WITH_SPLIT_ro_template[of "array_slice_assn A", OF _ assms]; assumption?)
      unfolding array_slice_assn_def ..
      
                  
  end  
end  

  
  
section Arrays with Length

definition "larray1_rel = br snd (λ(n,xs). n = length xs)"
abbreviation "larray_impl_assn' TYPE('b::len2)  snat_assn' TYPE('b) ×a array_assn id_assn"
definition "raw_larray_assn  hr_comp (larray_impl_assn' TYPE(_)) larray1_rel"

definition "larray_assn A   hr_comp raw_larray_assn (the_pure Alist_rel)"

abbreviation larray_assn' 
  :: "'b itself  ('a  'c  llvm_amemory  bool)  'a list  'b::len2 word × 'c::llvm_rep ptr  llvm_amemory  bool" 
  where
  "larray_assn' _ == larray_assn"

type_synonym ('x,'l) larray = "'l word × 'x ptr"

lemma larray1_rel_prenorm: "((n, xs), ys)  larray1_rel  n = length ys  xs=ys"  
  by (auto simp: larray1_rel_def in_br_conv)


lemma larray_assn_comp: "hr_comp (larray_assn id_assn) (the_pure Alist_rel) = larray_assn A"
  unfolding larray_assn_def by simp
    
definition [simp]: "larray_replicate_init i n  replicate n i"
interpretation larray: replicate_init larray_replicate_init by unfold_locales simp
  

context 
  notes [fcomp_norm_unfold] = raw_larray_assn_def[symmetric] larray_assn_def[symmetric] larray_assn_comp
  notes [fcomp_prenorm_simps] = larray1_rel_prenorm
begin

sepref_decl_op larray_custom_replicate: op_list_replicate :: "nat_rel  A  Alist_rel" .

definition "la_replicate1 n i  (n, replicate n i)"
lemma la_replicate1_refine: "(la_replicate1,op_larray_custom_replicate)  nat_rel  Id  larray1_rel"
  by (auto simp: larray1_rel_def in_br_conv la_replicate1_def)
  
sepref_definition la_replicate_impl [llvm_inline] is "uncurry (RETURN oo la_replicate1)" 
  :: "(snat_assn' TYPE('b::len2))k *a id_assnk a larray_impl_assn' TYPE('b::len2)"
  unfolding la_replicate1_def 
  apply (rewrite array_fold_custom_replicate)
  apply sepref_dbg_keep
  done
  
sepref_decl_impl la_replicate_impl.refine[FCOMP la_replicate1_refine] . 

lemma larray_fold_custom_replicate: 
  "replicate = op_larray_custom_replicate"
  "op_list_replicate = op_larray_custom_replicate"
  "mop_list_replicate = mop_larray_custom_replicate"
  by (auto del: ext intro!: ext)



definition "la_replicate_init1 n  (n, array_replicate_init init n)"
lemma la_replicate_init1_refine: "(la_replicate_init1, replicate_init_raw)  nat_rel  larray1_rel"
  by (auto simp: larray1_rel_def in_br_conv la_replicate_init1_def)
  
    
sepref_definition la_replicate_init_impl [llvm_inline] is "(RETURN o la_replicate_init1)" 
  :: "(snat_assn' TYPE('b::len2))k a larray_impl_assn' TYPE('b::len2)"
  unfolding la_replicate_init1_def 
  apply sepref_dbg_keep
  done

sepref_decl_impl (no_mop) la_replicate_init_impl.refine[FCOMP la_replicate_init1_refine] uses larray.replicate_init_param .
  


definition "la_grow_init1  λns os (n,xs). (ns, op_list_grow_init init ns os xs)"
lemma la_grow_init1_refine: "(uncurry2 la_grow_init1, uncurry2 grow_init_raw) 
   [λ((ns,os),xs). oslength xs  osns]f (nat_rel ×r nat_rel) ×r larray1_rel  larray1_rel"
  by (auto simp: larray1_rel_def in_br_conv la_grow_init1_def intro!: frefI)
  
    
sepref_definition la_grow_init_impl [llvm_inline] is "(uncurry2 (RETURN ooo la_grow_init1))" 
  :: "[λ((ns,os),(n,xs)). oslength xs  osns]a (snat_assn' TYPE('b::len2))k *a (snat_assn' TYPE('b::len2))k *a (larray_impl_assn' TYPE('b::len2))d  larray_impl_assn' TYPE('b::len2)"
  unfolding la_grow_init1_def 
  by sepref

sepref_decl_impl (no_mop) la_grow_init_impl.refine[FCOMP la_grow_init1_refine] uses grow_init_param .

definition [simp]: "op_list_grow_init' i ns xs  xs@replicate (ns-length xs) i"

lemma op_list_grow_init'_alt: "op_list_grow_init' i ns xs = op_list_grow_init i ns (length xs) xs" by simp


definition "la_length1 nxs  case nxs of (n,_)  id n"
lemma la_length1_refine: "(la_length1,op_list_length)  larray1_rel  nat_rel"
  by (auto simp: larray1_rel_def in_br_conv la_length1_def)

sepref_definition la_length_impl [llvm_inline] is "RETURN o la_length1" :: "(larray_impl_assn' TYPE('b::len2))k a snat_assn' TYPE('b)"
  unfolding la_length1_def 
  apply sepref_dbg_keep
  done
  
sepref_decl_impl la_length_impl.refine[FCOMP la_length1_refine] . 


  
definition "la_is_empty1 nxs  case nxs of (n,_)  n=0"
lemma la_is_empty1_refine: "(la_is_empty1,op_list_is_empty)  larray1_rel  bool_rel"
  by (auto simp: larray1_rel_def in_br_conv la_is_empty1_def)
    
sepref_definition la_is_empty_impl [llvm_inline] is "RETURN o la_is_empty1" :: "(larray_impl_assn' TYPE('b::len2))k a bool1_assn"
  unfolding la_is_empty1_def 
  apply (annot_snat_const "TYPE('b)")
  apply sepref_dbg_keep
  done

sepref_decl_impl la_is_empty_impl.refine[FCOMP la_is_empty1_refine] . 
  

  
definition "la_get1 nxs i  case nxs of (n,xs)  xs!i"
lemma la_get1_refine: "(la_get1,op_list_get)  larray1_rel  nat_rel  Id"
  by (auto simp: larray1_rel_def in_br_conv la_get1_def)
  
sepref_definition la_get_impl [llvm_inline] is "uncurry (RETURN oo la_get1)" :: "[λ(la,i). i<length (snd la)]a (larray_impl_assn' TYPE('b::len2))k *a (snat_assn' TYPE('c::len2))k  id_assn"
  unfolding la_get1_def la_length1_def
  apply sepref_dbg_keep
  done
  
sepref_decl_impl la_get_impl.refine[FCOMP la_get1_refine] .
  

definition "la_set1 nxs i x  case nxs of (n,xs)  (n,xs[i:=x])"
lemma la_set1_refine: "(la_set1,op_list_set)  larray1_rel  nat_rel  Id  larray1_rel"
  by (auto simp: larray1_rel_def in_br_conv la_set1_def)
  
sepref_definition la_set_impl [llvm_inline] is "uncurry2 (RETURN ooo la_set1)" 
  :: "[λ((la,i),_). i<length (snd la)]a (larray_impl_assn' TYPE('b::len2))d *a (snat_assn' TYPE('c::len2))k *a id_assnk  larray_impl_assn' TYPE('b::len2)"
  unfolding la_set1_def
  apply sepref_dbg_keep
  done
  
sepref_decl_impl la_set_impl.refine[FCOMP la_set1_refine] .

sepref_definition larray_swap is "uncurry2 (mop_list_swap)" 
  :: "(larray_assn' TYPE('l::len2) id_assn)d *a (snat_assn)k *a (snat_assn)k a larray_assn' TYPE('l::len2) id_assn"
  unfolding gen_mop_list_swap by sepref
  
sepref_decl_impl (ismop) larray_swap.refine .




definition "la_free1 nxs  case nxs of (_,xs)  op_list_free xs"
lemma la_free1_refine: "(la_free1,op_list_free)  larray1_rel  unit_rel" by auto

sepref_definition la_free_impl [llvm_inline] is "RETURN o la_free1" :: "(larray_impl_assn' TYPE(_))d a unit_assn"
  unfolding la_free1_def
  by sepref

sepref_decl_impl larray_free: la_free_impl.refine[FCOMP la_free1_refine] .
lemmas larray_mk_free[sepref_frame_free_rules] = hn_MK_FREEI[OF larray_free_hnr]
  
end
  

lemma larray_boundD[sepref_bounds_dest]: 
  "rdomp (larray_assn' TYPE('a::len2) A) xs  length xs < max_snat LENGTH('a)"
  unfolding larray_assn_def raw_larray_assn_def larray1_rel_def
  apply (auto simp: rdomp_hrcomp_conv in_br_conv snat_rel_def snat.rel_def)
  by (simp add: list_rel_pres_length)




subsection Ad-Hoc Regression Tests
  
sepref_definition example1 [llvm_code] is "λn. RETURN (replicate (n+1) (snat_init TYPE(32)))" 
  :: "[λn. n{1..<150}]a (snat_assn' TYPE(32))k  array_assn (snat_assn' TYPE(32))"
  apply (annot_snat_const "TYPE(32)")
  apply (rewrite array.fold_replicate_init)
  apply sepref
  done
  
sepref_definition example2 [llvm_code] is λn. do {
  ASSERT (n>10);
  let a = replicate n (snat_const TYPE(64) 42);
  let a = a[snat_const TYPE(32) 3:=0];
  ASSERT (a!1=42  a!2=42);
  RETURN (a!snat_const TYPE(32) 1 + a!snat_const TYPE(32) 2)
} :: "(snat_assn' TYPE(32))k a snat_assn' TYPE(64)"
  apply (annot_snat_const "TYPE(64)")
  apply (rewrite array_fold_custom_replicate)
  apply sepref
  done
  
  
sepref_definition example1n [llvm_code] is "λn. RETURN (replicate (n+1) (snat_init TYPE(8)))" 
  :: "[λn. n{1..<150}]a (snat_assn' TYPE(32))k  larray_assn' TYPE(32) (snat_assn' TYPE(8))"
  apply (rewrite larray.fold_replicate_init)
  apply (annot_snat_const "TYPE(32)")
  apply sepref
  done
  
  
sepref_definition example2n [llvm_code] is λn. do {
  ASSERT (n>10);
  let a = replicate n (snat_const TYPE(64) 42);
  let a = a[snat_const TYPE(32) 3:=0];
  ASSERT (a!1=42  a!2=42);
  RETURN (a!snat_const TYPE(32) 1 + a!snat_const TYPE(32) 2)
} :: "(snat_assn' TYPE(32))k a snat_assn' TYPE(64)"
  apply (annot_snat_const "TYPE(64)")
  apply (rewrite larray_fold_custom_replicate)
  apply sepref
  done

  
  
sepref_definition example3 [llvm_code] is uncurry (λxs n. RECT (λD (xs,n). doN {
  ASSERT (n = length xs);
  if n<10 then RETURN xs
  else doN {
    (_,xs)  WITH_SPLIT 5 xs (λxs1 xs2. doN {
      xs1  mop_list_set xs1 0 3;
      xs2  D (xs2, (n-5));
      RETURN (True,xs1,xs2)
    });
    RETURN xs
  }
}) (xs,n)) :: "[λ_. True]c (array_slice_assn (snat_assn' TYPE(64)))d *a (snat_assn' TYPE(64))k  array_slice_assn (snat_assn' TYPE(64)) [λ(xs,n) r. r=xs]c"
  apply (annot_snat_const "TYPE(64)")
  apply (subst RECT_cp_annot[where CP="λ(xs,n) r. r=xs"])
  apply sepref
  done
  
  
  
export_llvm example1 example2 example1n example2n example3
    

  
end