Theory IICF_Array
theory IICF_Array
imports "../Intf/IICF_List"
begin
lemma list_rel_take: "(xs,ys)∈⟨A⟩list_rel ⟹ (take n xs, take n ys) ∈ ⟨A⟩list_rel"
unfolding list_rel_def by auto
lemma list_rel_drop: "(xs,ys)∈⟨A⟩list_rel ⟹ (drop n xs, drop n ys) ∈ ⟨A⟩list_rel"
unfolding list_rel_def by auto
lemma list_rel_append: "(xs⇩1,ys⇩1)∈ ⟨A⟩list_rel ⟹ (xs⇩2,ys⇩2)∈ ⟨A⟩list_rel ⟹ (xs⇩1@xs⇩2,ys⇩1@ys⇩2)∈ ⟨A⟩list_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 A⟩list_rel⟩nres_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 A⟩list_rel → ⟨⟨the_pure A⟩list_rel⟩nres_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 A⟩list_rel → ⟨the_pure A⟩list_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. ()" :: "⟨A⟩list_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 A⟩list_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 A⟩list_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
begin
lemma array_get_hnr_aux: "(uncurry array_nth,uncurry (RETURN oo op_list_get))
∈ [λ(l,i). i<length l]⇩a raw_array_assn⇧k *⇩a snat_assn⇧k → 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_assn⇧d *⇩a snat_assn⇧k *⇩a id_assn⇧k
→⇩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_assn⇧k →⇩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). os≤length xs ∧ os≤ns]⇩a snat_assn⇧k *⇩a snat_assn⇧k *⇩a raw_array_assn⇧d → 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 → ⟨A⟩list_rel" .
lemma hn_array_replicate_new_raw:
"(uncurry narray_new_init, uncurry (RETURN oo op_array_custom_replicate)) ∈ snat_assn⇧k *⇩a id_assn⇧k →⇩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_assn⇧d →⇩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 A⟩list_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 A⟩list_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
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_assn⇧k *⇩a snat_assn⇧k → 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_assn⇧d *⇩a snat_assn⇧k *⇩a id_assn⇧k
→⇩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 { p⇩2 ← ll_ofs_ptr p i; Mreturn (p,p⇩2)}"
definition ars_join :: "'a::llvm_rep ptr ⇒ 'a ptr ⇒ 'a ptr llM"
where [llvm_inline]: "ars_join p⇩1 p⇩2 ≡ Mreturn p⇩1"
context begin
interpretation llvm_prim_mem_setup .
interpretation llvm_prim_arith_setup .
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 ai⇩1 ai⇩2 n ≡ ai⇩2 = ai⇩1 +⇩a int n"
lemma ars_join_rl[vcg_rules]:
shows "llvm_htriple
(raw_array_slice_assn a⇩1 ai⇩1 ** raw_array_slice_assn a⇩2 ai⇩2 ** ↑⇩!(ars_joinable ai⇩1 ai⇩2 (length a⇩1)))
(ars_join ai⇩1 ai⇩2)
(λr. ↑(r=ai⇩1) ** raw_array_slice_assn (a⇩1@a⇩2) ai⇩1)"
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)
(λ(a⇩1,a⇩2). raw_array_slice_assn (take i a) a⇩1 ** raw_array_slice_assn (drop i a) a⇩2 ** snat_assn i ii ** ↑(a⇩1=ai ∧ ars_joinable a⇩1 a⇩2 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 xs⇩1 = take i xs;
let xs⇩2 = drop i xs;
(r,xs⇩1',xs⇩2') ← m xs⇩1 xs⇩2;
ASSERT (length xs⇩1' = length xs⇩1 ∧ length xs⇩2'=length xs⇩2);
RETURN (r,xs⇩1'@xs⇩2')
}"
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
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 "⋀xs⇩1 xs⇩2. ⟦xs=xs⇩1@xs⇩2; length xs⇩1=n ⟧ ⟹
m xs⇩1 xs⇩2 ≤ SPEC (λ(r',xs⇩1',xs⇩2').
length xs⇩1'=length xs⇩1
∧ length xs⇩2'=length xs⇩2
∧ P (r', xs⇩1'@xs⇩2'))"
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) ∈ ⟨A⟩list_rel"
assumes [refine]: "⟦n < length xs; n' < length xs'⟧ ⟹ m' (take n' xs') (drop n' xs') ≤ ⇓(R×⇩r⟨A⟩list_rel×⇩r⟨A⟩list_rel) (m (take n xs) (drop n xs))"
shows "WITH_SPLIT n' xs' m' ≤⇓(R ×⇩r ⟨A⟩list_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 {
(a⇩1,a⇩2) ← ars_split i a;
(r,_,_) ← m a⇩1 a⇩2;
ars_join a⇩1 a⇩2;
Mreturn (r,a)
}"
lemma ars_with_split_for_paper: "ars_with_split i a m = doM {
p⇩2 ← ll_ofs_ptr a i;
(r, _, _) ← m a p⇩2;
Mreturn (r, a)
}"
unfolding ars_with_split_def ars_split_def ars_join_def
by simp
lemma ars_with_split_mono[partial_function_mono]:
assumes "⋀xs⇩1 xs⇩2. M_mono' (λD. m D xs⇩1 xs⇩2)"
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: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. hn_refine (raw_array_slice_assn xs⇩1 xsi⇩1 ** raw_array_slice_assn xs⇩2 xsi⇩2 ** F) (mi xsi⇩1 xsi⇩2) (F') (R ×⇩a raw_array_slice_assn ×⇩a raw_array_slice_assn) (CP' xsi⇩1 xsi⇩2) (m xs⇩1 xs⇩2)"
assumes CP': "⋀xsi⇩1 xsi⇩2 ri xsi⇩1' xsi⇩2'. CP' xsi⇩1 xsi⇩2 (ri,xsi⇩1',xsi⇩2') ⟹ xsi⇩1'=xsi⇩1 ∧ xsi⇩2'=xsi⇩2 ∧ 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: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2.
hn_refine (raw_array_slice_assn xs⇩1 xsi⇩1 ** raw_array_slice_assn xs⇩2 xsi⇩2)
(mi xsi⇩1 xsi⇩2)
(□)
(R ×⇩a raw_array_slice_assn ×⇩a raw_array_slice_assn)
(λ(ri,xsi⇩1',xsi⇩2'). xsi⇩1'=xsi⇩1 ∧ xsi⇩2' = xsi⇩2)
(m xs⇩1 xs⇩2)"
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'="λxsi⇩1 xsi⇩2 (ri,xsi⇩1',xsi⇩2'). xsi⇩1'=xsi⇩1 ∧ xsi⇩2' = xsi⇩2" and
CP="λ_. True"] MHN
apply (simp add: sep_algebra_simps)
by blast
lemma hn_WITH_SPLIT_template_aux:
assumes sl_assn_def: "sl_assn = hr_comp raw_array_slice_assn (⟨A⟩list_rel)"
assumes MHN: "⋀xs⇩1 xs⇩2 xsi⇩2. hn_refine
(hn_ctxt (sl_assn) xs⇩1 xsi ** hn_ctxt (sl_assn) xs⇩2 xsi⇩2 ** hn_ctxt snat_assn n ni ** F)
(mi xsi xsi⇩2) (F')
(R ×⇩a sl_assn ×⇩a sl_assn)
(CP' xsi xsi⇩2)
(m xs⇩1 xs⇩2)"
assumes CP': "⋀xsi⇩2 ri xsi⇩1' xsi⇩2'. CP' xsi xsi⇩2 (ri,xsi⇩1',xsi⇩2') ⟹ xsi⇩1'=xsi ∧ xsi⇩2'=xsi⇩2 ∧ 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 (⟨A⟩list_rel)"
assumes FR: "Γ ⊢ hn_ctxt sl_assn xs xsi ** hn_ctxt snat_assn n ni ** Γ⇩1"
assumes HN: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. ⟦ CP_assm (xsi⇩1 = xsi) ⟧ ⟹ hn_refine
(hn_ctxt sl_assn xs⇩1 xsi⇩1 ** hn_ctxt sl_assn xs⇩2 xsi⇩2 ** hn_ctxt snat_assn n ni ** Γ⇩1)
(mi xsi⇩1 xsi⇩2)
(Γ⇩2 xs⇩1 xsi⇩1 xs⇩2 xsi⇩2) (R) (CP xsi⇩1 xsi⇩2) (m xs⇩1 xs⇩2)"
assumes CP: "⋀xsi⇩2 ri' xsi⇩1' xsi⇩2'. CP_assm (CP xsi xsi⇩2 (ri',xsi⇩1',xsi⇩2')) ⟹ CP_cond (xsi⇩1' = xsi ∧ xsi⇩2'=xsi⇩2)"
assumes FR2: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. Γ⇩2 xs⇩1 xsi⇩1 xs⇩2 xsi⇩2 ⊢
hn_invalid sl_assn xs⇩1 xsi⇩1 ** hn_invalid sl_assn xs⇩2 xsi⇩2 ** Γ⇩1'"
assumes FR3: "⋀x xi. hn_ctxt R x xi ⊢ hn_ctxt (R' ×⇩a sl_assn ×⇩a sl_assn) x xi"
assumes CP2: "⋀xsi⇩2. CP_simplify (CP_EX32 (CP xsi xsi⇩2)) (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. ∃xsi⇩2 xsi⇩2'. CP xsi xsi⇩2 (ri,xsi,xsi⇩2')"]
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: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. ⟦ CP_assm (xsi⇩1 = xsi) ⟧ ⟹ hn_refine
(hn_ctxt (array_slice_assn A) xs⇩1 xsi⇩1 ** hn_ctxt (array_slice_assn A) xs⇩2 xsi⇩2 ** hn_ctxt snat_assn n ni ** Γ⇩1)
(mi xsi⇩1 xsi⇩2)
(Γ⇩2 xs⇩1 xsi⇩1 xs⇩2 xsi⇩2) (R) (CP xsi⇩1 xsi⇩2) (m xs⇩1 xs⇩2)"
assumes CP: "⋀xsi⇩2 ri' xsi⇩1' xsi⇩2'. CP_assm (CP xsi xsi⇩2 (ri',xsi⇩1',xsi⇩2')) ⟹ CP_cond (xsi⇩1' = xsi ∧ xsi⇩2'=xsi⇩2)"
assumes FR2: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. Γ⇩2 xs⇩1 xsi⇩1 xs⇩2 xsi⇩2 ⊢
hn_invalid (array_slice_assn A) xs⇩1 xsi⇩1 ** hn_invalid (array_slice_assn A) xs⇩2 xsi⇩2 ** Γ⇩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 CP2: "⋀xsi⇩2. CP_simplify (CP_EX32 (CP xsi xsi⇩2)) (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 xs⇩1 = take i xs;
let xs⇩2 = drop i xs;
m xs⇩1 xs⇩2
}"
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
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 "⋀xs⇩1 xs⇩2. ⟦xs=xs⇩1@xs⇩2; length xs⇩1=n ⟧ ⟹ m xs⇩1 xs⇩2 ≤ 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) ∈ ⟨A⟩list_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 {
(a⇩1,a⇩2) ← ars_split i a;
r ← m a⇩1 a⇩2;
ars_join a⇩1 a⇩2;
Mreturn r
}"
lemma ars_with_split_ro_mono[partial_function_mono]:
assumes "⋀xs⇩1 xs⇩2. M_mono' (λD. m D xs⇩1 xs⇩2)"
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: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. hn_refine (raw_array_slice_assn xs⇩1 xsi⇩1 ** raw_array_slice_assn xs⇩2 xsi⇩2 ** F) (mi xsi⇩1 xsi⇩2) (raw_array_slice_assn xs⇩1 xsi⇩1 ** raw_array_slice_assn xs⇩2 xsi⇩2 ** F') R (CP' xsi⇩1 xsi⇩2) (m xs⇩1 xs⇩2)"
assumes CP': "⋀xsi⇩1 xsi⇩2 ri. CP' xsi⇩1 xsi⇩2 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: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2.
hn_refine (raw_array_slice_assn xs⇩1 xsi⇩1 ** raw_array_slice_assn xs⇩2 xsi⇩2)
(mi xsi⇩1 xsi⇩2)
(raw_array_slice_assn xs⇩1 xsi⇩1 ** raw_array_slice_assn xs⇩2 xsi⇩2)
R
(λ_. True)
(m xs⇩1 xs⇩2)"
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: "⟦ (xsi⇩1,take n xs)∈⟨A⟩list_rel; (xsi⇩2,drop n xs)∈⟨A⟩list_rel ⟧ ⟹ (xsi⇩1@xsi⇩2,xs) ∈ ⟨A⟩list_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 (⟨A⟩list_rel)"
assumes MHN: "⋀xs⇩1 xs⇩2 xsi⇩2. hn_refine
(hn_ctxt (sl_assn) xs⇩1 xsi ** hn_ctxt (sl_assn) xs⇩2 xsi⇩2 ** hn_ctxt snat_assn n ni ** F)
(mi xsi xsi⇩2) (hn_ctxt (sl_assn) xs⇩1 xsi ** hn_ctxt (sl_assn) xs⇩2 xsi⇩2 ** F')
(R)
(CP' xsi xsi⇩2)
(m xs⇩1 xs⇩2)"
assumes CP': "⋀ri xsi⇩2. CP' xsi xsi⇩2 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 (⟨A⟩list_rel)"
assumes FR: "Γ ⊢ hn_ctxt sl_assn xs xsi ** hn_ctxt snat_assn n ni ** Γ⇩1"
assumes HN: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. ⟦ CP_assm (xsi⇩1 = xsi) ⟧ ⟹ hn_refine
(hn_ctxt sl_assn xs⇩1 xsi⇩1 ** hn_ctxt sl_assn xs⇩2 xsi⇩2 ** hn_ctxt snat_assn n ni ** Γ⇩1)
(mi xsi⇩1 xsi⇩2)
(Γ⇩2 xs⇩1 xsi⇩1 xs⇩2 xsi⇩2) (R) (CP xsi⇩1 xsi⇩2) (m xs⇩1 xs⇩2)"
assumes FR2: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. Γ⇩2 xs⇩1 xsi⇩1 xs⇩2 xsi⇩2 ⊢
hn_ctxt sl_assn xs⇩1 xsi⇩1 ** hn_ctxt sl_assn xs⇩2 xsi⇩2 ** Γ⇩1'"
assumes CP2: "⋀xsi⇩2. CP_simplify (CP xsi xsi⇩2) (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: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. ⟦ CP_assm (xsi⇩1 = xsi) ⟧ ⟹ hn_refine
(hn_ctxt (array_slice_assn A) xs⇩1 xsi⇩1 ** hn_ctxt (array_slice_assn A) xs⇩2 xsi⇩2 ** hn_ctxt snat_assn n ni ** Γ⇩1)
(mi xsi⇩1 xsi⇩2)
(Γ⇩2 xs⇩1 xsi⇩1 xs⇩2 xsi⇩2) (R) (CP xsi⇩1 xsi⇩2) (m xs⇩1 xs⇩2)"
assumes FR2: "⋀xs⇩1 xsi⇩1 xs⇩2 xsi⇩2. Γ⇩2 xs⇩1 xsi⇩1 xs⇩2 xsi⇩2 ⊢
hn_ctxt (array_slice_assn A) xs⇩1 xsi⇩1 ** hn_ctxt (array_slice_assn A) xs⇩2 xsi⇩2 ** Γ⇩1'"
assumes CP2: "⋀xsi⇩2. CP_simplify (CP xsi xsi⇩2) (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 A⟩list_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 A⟩list_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 → ⟨A⟩list_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_assn⇧k →⇩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). os≤length xs ∧ os≤ns]⇩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)). os≤length xs ∧ os≤ns]⇩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_assn⇧k → 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 (λxs⇩1 xs⇩2. doN {
xs⇩1 ← mop_list_set xs⇩1 0 3;
xs⇩2 ← D (xs⇩2, (n-5));
RETURN (True,xs⇩1,xs⇩2)
});
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