theory Array_Array_List64
imports Array_Array_List IICF_Array_List64
begin
subsection ‹Array of Array Lists of maximum length \<^term>‹uint64_max››
definition length_aa64 :: ‹('a::heap array_list64) array ⇒ uint64 ⇒ uint64 Heap› where
‹length_aa64 xs i = do {
x ← nth_u64_code xs i;
arl64_length x}›
lemma arrayO_assn_Array_nth[sep_heap_rules]:
‹b < length xs ⟹
<arrayO_assn (arl64_assn R) xs a> Array.nth a b
<λp. arrayO_except_assn (arl64_assn R) [b] xs a (λp'. ↑(p=p'!b))*
arl64_assn R (xs ! b) (p)>›
unfolding length_aa64_def nth_u64_code_def Array.nth'_def
apply (subst arrayO_except_assn_array0_index[symmetric, of b])
apply simp
unfolding arrayO_except_assn_def arl_assn_def hr_comp_def
apply (sep_auto simp: arrayO_except_assn_def arl_length_def arl_assn_def arl64_assn_def
eq_commute[of ‹(_, _)›] is_array_list64_def hr_comp_def length_ll_def array_assn_def
is_array_def uint64_nat_rel_def br_def
dest: list_all2_lengthD split: prod.splits)
done
lemma arl64_length[sep_heap_rules]:
‹<arl64_assn R b a> arl64_length a< λr. arl64_assn R b a * ↑(nat_of_uint64 r = length b)>›
by (sep_auto simp: arrayO_except_assn_def arl_length_def arl_assn_def arl64_assn_def
eq_commute[of ‹(_, _)›] is_array_list64_def hr_comp_def length_ll_def array_assn_def
is_array_def uint64_nat_rel_def br_def arl64_length_def list_rel_imp_same_length[symmetric]
dest: list_all2_lengthD split: prod.splits)
lemma length_aa64_rule[sep_heap_rules]:
‹b < length xs ⟹ (b', b) ∈ uint64_nat_rel ⟹ <arrayO_assn (arl64_assn R) xs a> length_aa64 a b'
<λr. arrayO_assn (arl64_assn R) xs a * ↑ (nat_of_uint64 r = length_ll xs b)>⇩t›
unfolding length_aa64_def nth_u64_code_def Array.nth'_def
apply (sep_auto simp flip: nat_of_uint64_code simp: br_def uint64_nat_rel_def length_ll_def)
apply (subst arrayO_except_assn_array0_index[symmetric, of b])
apply (simp add: nat_of_uint64_code br_def uint64_nat_rel_def)
apply (sep_auto simp: arrayO_except_assn_def)
done
lemma length_aa64_hnr[sepref_fr_rules]: ‹(uncurry length_aa64, uncurry (RETURN ∘∘ length_ll)) ∈
[λ(xs, i). i < length xs]⇩a (arrayO_assn (arl64_assn R))⇧k *⇩a uint64_nat_assn⇧k → uint64_nat_assn›
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def)
lemma arl64_get_hnr[sep_heap_rules]:
assumes ‹(n', n) ∈ uint64_nat_rel› and ‹n < length a› and ‹CONSTRAINT is_pure R›
shows ‹<arl64_assn R a b>
arl64_get b n'
<λr. arl64_assn R a b * R (a ! n) r>›
proof -
obtain A' where
A: ‹pure A' = R›
using assms pure_the_pure by auto
then have A': ‹the_pure R = A'›
by auto
show ?thesis
using param_nth[of n a n ‹take (nat_of_uint64 (snd b)) _› ‹the_pure R›, simplified] assms
unfolding arl64_get_def arl64_assn_def nth_u64_code_def Array.nth'_def
by (sep_auto simp flip: nat_of_uint64_code A simp: br_def uint64_nat_rel_def hr_comp_def
is_array_list64_def list_rel_imp_same_length[symmetric] pure_app_eq dest:
split: prod.splits)
qed
definition nth_aa64 where
‹nth_aa64 xs i j = do {
x ← Array.nth xs i;
y ← arl64_get x j;
return y}›
lemma nth_aa64_hnr[sepref_fr_rules]:
assumes p: ‹CONSTRAINT is_pure R›
shows
‹(uncurry2 nth_aa64, uncurry2 (RETURN ∘∘∘ nth_ll)) ∈
[λ((l,i),j). i < length l ∧ j < length_ll l i]⇩a
(arrayO_assn (arl64_assn R))⇧k *⇩a nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have H: ‹list_all2 (λx x'. (x, x') ∈ the_pure (λa c. ↑ ((c, a) ∈ R'))) bc (a ! ba) ⟹
b < length (a ! ba) ⟹
(bc ! b, a ! ba ! b) ∈ R'› for bc a ba b
by (auto simp add: ent_refl_true list_all2_conv_all_nth is_pure_alt_def pure_app_eq[symmetric])
show ?thesis
using p
apply sepref_to_hoare
apply (sep_auto simp: nth_aa64_def length_ll_def nth_ll_def)
apply (subst arrayO_except_assn_array0_index[symmetric, of ba])
apply simp
apply (sep_auto simp: arrayO_except_assn_def arrayO_assn_def arl64_assn_def hr_comp_def list_rel_def
list_all2_lengthD
star_aci(3) R R' pure_def H)
done
qed
definition append64_el_aa :: "('a::{default,heap} array_list64) array ⇒
nat ⇒ 'a ⇒ ('a array_list64) array Heap"where
"append64_el_aa ≡ λa i x. do {
j ← Array.nth a i;
a' ← arl64_append j x;
Array.upd i a' a
}"
declare arrayO_nth_rule[sep_heap_rules]
lemma sep_auto_is_stupid:
fixes R :: ‹'a ⇒ 'b::{heap,default} ⇒ assn›
assumes p: ‹is_pure R› and ‹length l' < uint64_max›
shows
‹<∃⇩Ap. R1 p * R2 p * arl64_assn R l' aa * R x x' * R4 p>
arl64_append aa x' <λr. (∃⇩Ap. arl64_assn R (l' @ [x]) r * R1 p * R2 p * R x x' * R4 p * true) >›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have bbi: ‹(x', x) ∈ the_pure R› if
‹(aa, bb) ⊨ is_array_list64 (ba @ [x']) (a, baa) * R1 p * R2 p * pure R' x x' * R4 p * true›
for aa bb a ba baa p
using that by (auto simp: mod_star_conv R R')
show ?thesis
using assms(2)
unfolding arl_assn_def hr_comp_def
by (sep_auto simp: list_rel_def R R' arl64_assn_def hr_comp_def list_all2_lengthD
intro!: list_all2_appendI dest!: bbi)
qed
lemma append_aa64_hnr[sepref_fr_rules]:
fixes R :: ‹'a ⇒ 'b :: {heap, default} ⇒ assn›
assumes p: ‹is_pure R›
shows
‹(uncurry2 append64_el_aa, uncurry2 (RETURN ∘∘∘ append_ll)) ∈
[λ((l,i),x). i < length l ∧ length (l ! i) < uint64_max]⇩a (arrayO_assn (arl64_assn R))⇧d *⇩a nat_assn⇧k *⇩a R⇧k → (arrayO_assn (arl64_assn R))›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have [simp]: ‹(∃⇩Ax. arrayO_assn (arl64_assn R) a ai * R x r * true * ↑ (x = a ! ba ! b)) =
(arrayO_assn (arl64_assn R) a ai * R (a ! ba ! b) r * true)› for a ai ba b r
by (auto simp: ex_assn_def)
show ?thesis
apply sepref_to_hoare
apply (sep_auto simp: append64_el_aa_def)
apply (simp add: arrayO_except_assn_def)
apply (rule sep_auto_is_stupid[OF p])
apply simp
apply (sep_auto simp: array_assn_def is_array_def append_ll_def)
apply (simp add: arrayO_except_assn_array0[symmetric] arrayO_except_assn_def)
apply (subst_tac (2) i = ba in heap_list_all_nth_remove1)
apply (solves ‹simp›)
apply (simp add: array_assn_def is_array_def)
apply (rule_tac x=‹p[ba := (ab, bc)]› in ent_ex_postI)
apply (subst_tac (2)xs'=a and ys'=p in heap_list_all_nth_cong)
apply (solves ‹auto›)+
apply sep_auto
done
qed
definition update_aa64 :: "('a::{heap} array_list64) array ⇒ nat ⇒ uint64 ⇒ 'a ⇒ ('a array_list64) array Heap" where
‹update_aa64 a i j y = do {
x ← Array.nth a i;
a' ← arl64_set x j y;
Array.upd i a' a
}›
declare nth_rule[sep_heap_rules del]
declare arrayO_nth_rule[sep_heap_rules]
lemma arrayO_except_assn_arl_set[sep_heap_rules]:
fixes R :: ‹'a ⇒ 'b :: {heap}⇒ assn›
assumes p: ‹is_pure R› and ‹bb < length a› and
‹ba < length_ll a bb› and ‹(ba' , ba) ∈ uint64_nat_rel›
shows ‹
<arrayO_except_assn (arl64_assn R) [bb] a ai
(λp'. ↑ ((aa, bc) = p' ! bb)) *
arl64_assn R (a ! bb) (aa, bc) *
R b bi>
arl64_set (aa, bc) ba' bi
<λ(aa, bc). arrayO_except_assn (arl64_assn R) [bb] a ai
(λr'. arl64_assn R ((a ! bb)[ba := b]) (aa, bc)) * R b bi * true>›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
show ?thesis
using assms
apply (sep_auto simp: arrayO_except_assn_def arl64_assn_def hr_comp_def list_rel_imp_same_length
list_rel_update length_ll_def)
done
qed
lemma Array_upd_arrayO_except_assn[sep_heap_rules]:
assumes
‹bb < length a› and
‹ba < length_ll a bb› and ‹(ba', ba) ∈ uint64_nat_rel›
shows ‹<arrayO_except_assn (arl64_assn R) [bb] a ai
(λr'. arl64_assn R xu (aa, bc)) *
R b bi *
true>
Array.upd bb (aa, bc) ai
<λr. ∃⇩Ax. R b bi * arrayO_assn (arl64_assn R) x r * true *
↑ (x = a[bb := xu])>›
proof -
have H[simp, intro]: ‹ba ≤ length l'›
if
‹ba ≤ length (a ! bb)› and
aa: ‹(take n' l', a ! bb) ∈ ⟨the_pure R⟩list_rel›
for l' :: ‹'b list› and n'
proof -
show ?thesis
using list_rel_imp_same_length[OF aa] that assms(3)
by (auto simp: uint64_nat_rel_def br_def list_rel_imp_same_length[symmetric])
qed
have [simp]: ‹(take ba l', take ba (a ! bb)) ∈ ⟨the_pure R⟩list_rel›
if
‹ba ≤ length (a ! bb)› and
‹n' ≤ length l'› and
take: ‹(take n' l', a ! bb) ∈ ⟨the_pure R⟩list_rel›
for l' :: ‹'b list› and n'
proof -
have [simp]: ‹n' = length (a ! bb)›
using list_rel_imp_same_length[OF take] that by auto
have 1: ‹take ba l' = take ba (take n' l')›
using that by (auto simp: min_def)
show ?thesis
using take
unfolding 1
by (rule list_rel_take)
qed
show ?thesis
using assms
unfolding arrayO_except_assn_def
apply (subst (2) arl64_assn_def)
apply (subst is_array_list64_def[abs_def])
apply (subst hr_comp_def[abs_def])
apply (subst array_assn_def)
apply (subst is_array_def[abs_def])
apply (subst hr_comp_def[abs_def])
apply sep_auto
apply (subst arrayO_except_assn_array0_index[symmetric, of bb])
apply (solves simp)
unfolding arrayO_except_assn_def array_assn_def is_array_def
apply (subst (3) arl64_assn_def)
apply (subst is_array_list64_def[abs_def])
apply (subst (2) hr_comp_def[abs_def])
apply (subst ex_assn_move_out)+
apply (rule_tac x=‹p[bb := (aa, bc)]› in ent_ex_postI)
apply (rule_tac x=‹take (nat_of_uint64 bc) l'› in ent_ex_postI)
apply (sep_auto simp: uint64_nat_rel_def br_def list_rel_imp_same_length intro!: split: prod.splits)
apply (subst (2) heap_list_all_nth_cong[of _ _ a _ p])
apply auto
apply sep_auto
done
qed
lemma update_aa64_rule[sep_heap_rules]:
assumes p: ‹is_pure R› and ‹bb < length a› and ‹ba < length_ll a bb› ‹(ba', ba) ∈ uint64_nat_rel›
shows ‹<R b bi * arrayO_assn (arl64_assn R) a ai> update_aa64 ai bb ba' bi
<λr. R b bi * (∃⇩Ax. arrayO_assn (arl64_assn R) x r * ↑ (x = update_ll a bb ba b))>⇩t›
using assms
by (sep_auto simp add: update_aa64_def update_ll_def p)
lemma update_aa_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 update_aa64, uncurry3 (RETURN oooo update_ll)) ∈
[λ(((l,i), j), x). i < length l ∧ j < length_ll l i]⇩a (arrayO_assn (arl64_assn R))⇧d *⇩a nat_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a R⇧k → (arrayO_assn (arl64_assn R))›
by sepref_to_hoare (sep_auto simp: assms)
definition last_aa64 :: "('a::heap array_list64) array ⇒ uint64 ⇒ 'a Heap" where
‹last_aa64 xs i = do {
x ← nth_u64_code xs i;
arl64_last x
}›
lemma arl64_last_rule[sep_heap_rules]:
assumes p: ‹is_pure R› ‹ai ≠ []›
shows ‹<arl64_assn R ai a> arl64_last a
<λr. arl64_assn R ai a * R (last ai) r>⇩t›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have [simp]: ‹⋀aa n l'.
(take (nat_of_uint64 n) l', ai) ∈ ⟨the_pure R⟩list_rel ⟹
l' ≠ [] ⟹ nat_of_uint64 n > 0›
using assms by (cases ai; auto simp: min_def split: if_splits dest!: list_rel_imp_same_length[symmetric]
simp flip: nat_of_uint64_le_iff simp: nat_of_uint64_ge_minus; fail)+
have [simp]: ‹⋀aa n l'.
(take (nat_of_uint64 n) l', ai) ∈ ⟨the_pure R⟩list_rel ⟹
l' ≠ [] ⟹ nat_of_uint64 (n - 1) = nat_of_uint64 n - 1›
using assms by (cases ai; auto simp: min_def split: if_splits dest!: list_rel_imp_same_length[symmetric]
simp flip: nat_of_uint64_le_iff simp: nat_of_uint64_ge_minus; fail)+
have [simp]: ‹⋀aa n l'.
(take (nat_of_uint64 n) l', ai) ∈ ⟨the_pure R⟩list_rel ⟹
nat_of_uint64 n ≤ length l' ⟹
l' ≠ [] ⟹ length l' ≤ uint64_max ⟹ nat_of_uint64 n - Suc 0 < length l'›
using assms by (cases ai; auto simp: min_def split: if_splits dest!: list_rel_imp_same_length[symmetric]
simp flip: nat_of_uint64_le_iff)+
have [intro!]: ‹(take (nat_of_uint64 n) l', ai) ∈ ⟨R'⟩list_rel ⟹
a = (aa, n) ⟹
nat_of_uint64 n ≤ length l' ⟹
l' ≠ [] ⟹
length l' ≤ uint64_max ⟹
(aaa, b) ⊨ aa ↦⇩a l' ⟹
(l' ! (nat_of_uint64 n - Suc 0), ai ! (length ai - Suc 0)) ∈ R'› for aa n l' aaa b
using assms
nat_of_uint64_ge_minus[of 1 n] param_last[OF assms(2), of ‹take (nat_of_uint64 n) l'› R']
by (auto simp: min_def R' last_conv_nth split: if_splits
simp flip: nat_of_uint64_le_iff)
show ?thesis
using assms supply nth_rule[sep_heap_rules] apply -
by (sep_auto simp add: update_aa64_def update_ll_def p arl64_last_def arl64_assn_def R'
pure_app_eq last_take_nth_conv last_conv_nth
nth_u64_code_def Array.nth'_def hr_comp_def is_array_list64_def nat_of_uint64_ge_minus
simp flip: nat_of_uint64_code
dest: list_rel_imp_same_length[symmetric])
qed
lemma last_aa64_rule[sep_heap_rules]:
assumes
p: ‹is_pure R› and
‹b < length a› and
‹a ! b ≠ []› and ‹(b', b) ∈ uint64_nat_rel›
shows ‹
<arrayO_assn (arl64_assn R) a ai>
last_aa64 ai b'
<λr. arrayO_assn (arl64_assn R) a ai * (∃⇩Ax. R x r * ↑ (x = last_ll a b))>⇩t›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have ‹⋀b.
b < length a ⟹ (b', b) ∈ uint64_nat_rel ⟹
a ! b ≠ [] ⟹
<arrayO_assn (arl64_assn R) a ai>
last_aa64 ai b'
<λr. arrayO_assn (arl64_assn R) a ai * (∃⇩Ax. R x r * ↑ (x = last_ll a b))>⇩t›
apply (sep_auto simp add: last_aa64_def last_ll_def assms nth_u64_code_def Array.nth'_def
uint64_nat_rel_def br_def
simp flip: nat_of_uint64_code)
apply (sep_auto simp add: last_aa64_def arrayO_except_assn_def array_assn_def is_array_def
hr_comp_def arl64_assn_def)
apply (subst_tac i= ‹nat_of_uint64 b'› in arrayO_except_assn_array0_index[symmetric])
apply (solves ‹simp›)
apply (subst arrayO_except_assn_def)
apply (auto simp add: last_aa_def arrayO_except_assn_def array_assn_def is_array_def hr_comp_def)
apply (rule_tac x=‹p› in ent_ex_postI)
apply (subst_tac (2)xs'=a and ys'=p in heap_list_all_nth_cong)
apply (solves ‹auto›)
apply (solves ‹auto›)
apply (rule_tac x=‹ba› in ent_ex_postI)
unfolding R unfolding R'
apply (sep_auto simp: pure_def param_last)
done
from this[of b] show ?thesis
using assms unfolding R' by blast
qed
lemma last_aa_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows ‹(uncurry last_aa64, uncurry (RETURN oo last_ll)) ∈
[λ(l,i). i < length l ∧ l ! i ≠ []]⇩a (arrayO_assn (arl64_assn R))⇧k *⇩a uint64_nat_assn⇧k → R›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
show ?thesis
using assms by sepref_to_hoare sep_auto
qed
definition swap_aa64 :: "('a::heap array_list64) array ⇒ nat ⇒ uint64 ⇒ uint64 ⇒ ('a array_list64) array Heap" where
‹swap_aa64 xs k i j = do {
xi ← nth_aa64 xs k i;
xj ← nth_aa64 xs k j;
xs ← update_aa64 xs k i xj;
xs ← update_aa64 xs k j xi;
return xs
}›
lemma nth_aa64_heap[sep_heap_rules]:
assumes p: ‹is_pure R› and ‹b < length aa› and ‹ba < length_ll aa b› and ‹(ba', ba) ∈ uint64_nat_rel›
shows ‹
<arrayO_assn (arl64_assn R) aa a>
nth_aa64 a b ba'
<λr. ∃⇩Ax. arrayO_assn (arl64_assn R) aa a *
(R x r *
↑ (x = nth_ll aa b ba)) *
true>›
proof -
have ‹<arrayO_assn (arl64_assn R) aa a>
nth_aa64 a b ba'
<λr. ∃⇩Ax. arrayO_assn (arl64_assn R) aa a *
R x r *
true *
↑ (x = nth_ll aa b ba)>›
using p assms nth_aa64_hnr[of R] unfolding hfref_def hn_refine_def nth_aa64_def pure_app_eq
by auto
then show ?thesis
unfolding hoare_triple_def
by (auto simp: Let_def pure_def)
qed
lemma update_aa_rule_pure:
assumes p: ‹is_pure R› and ‹b < length aa› and ‹ba < length_ll aa b› and
‹(ba', ba) ∈ uint64_nat_rel›
shows ‹
<arrayO_assn (arl64_assn R) aa a * R be bb>
update_aa64 a b ba' bb
<λr. ∃⇩Ax. invalid_assn (arrayO_assn (arl64_assn R)) aa a * arrayO_assn (arl64_assn R) x r *
true *
↑ (x = update_ll aa b ba be)>›
proof -
obtain R' where R': ‹R' = the_pure R› and RR': ‹R = pure R'›
using p by fastforce
have bb: ‹pure R' be bb = ↑((bb, be) ∈ R')›
by (auto simp: pure_def)
have ‹<arrayO_assn (arl64_assn R) aa a * R be bb>
update_aa64 a b ba' bb
<λr. ∃⇩Ax. invalid_assn (arrayO_assn (arl64_assn R)) aa a * nat_assn b b * nat_assn ba ba *
R be bb *
arrayO_assn (arl64_assn R) x r *
true *
↑ (x = update_ll aa b ba be)>›
using p assms update_aa_hnr[of R] unfolding hfref_def hn_refine_def pure_app_eq
by auto
then show ?thesis
unfolding R'[symmetric] unfolding hoare_triple_def RR' bb
by (auto simp: Let_def pure_def)
qed
lemma arl64_set_rule_arl64_assn: "
i<length l ⟹ (i', i) ∈ uint64_nat_rel ⟹ (x', x) ∈ the_pure R ⟹
<arl64_assn R l a>
arl64_set a i' x'
<arl64_assn R (l[i:=x])>"
supply arl64_set_rule[where i=i, sep_heap_rules]
by (sep_auto simp: arl64_assn_def hr_comp_def list_rel_imp_same_length
split: prod.split simp flip: nat_of_uint64_code intro!: list_rel_update')
lemma swap_aa_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 swap_aa64, uncurry3 (RETURN oooo swap_ll)) ∈
[λ(((xs, k), i), j). k < length xs ∧ i < length_ll xs k ∧ j < length_ll xs k]⇩a
(arrayO_assn (arl64_assn R))⇧d *⇩a nat_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k → (arrayO_assn (arl64_assn R))›
proof -
note update_aa_rule_pure[sep_heap_rules]
obtain R' where R': ‹R' = the_pure R› and RR': ‹R = pure R'›
using assms by fastforce
have [simp]: ‹the_pure (λa b. ↑ ((b, a) ∈ R')) = R'›
unfolding pure_def[symmetric] by auto
show ?thesis
using assms unfolding R'[symmetric] unfolding swap_aa64_def
apply sepref_to_hoare
supply nth_aa64_heap[sep_heap_rules del]
apply (sep_auto simp: swap_ll_def arrayO_except_assn_def
length_ll_update_ll uint64_nat_rel_def br_def)
supply nth_aa64_heap[sep_heap_rules]
apply (sep_auto simp: swap_ll_def arrayO_except_assn_def
length_ll_update_ll uint64_nat_rel_def br_def)
supply nth_aa64_heap[sep_heap_rules del]
apply (sep_auto simp: swap_ll_def arrayO_except_assn_def
length_ll_update_ll uint64_nat_rel_def br_def)
apply (rule frame_rule)
apply (rule frame_rule)
apply (rule_tac ba= ‹nat_of_uint64 bi› in nth_aa64_heap[of ])
apply (auto simp: swap_ll_def arrayO_except_assn_def
length_ll_update_ll uint64_nat_rel_def br_def)
supply update_aa_rule_pure[sep_heap_rules del] update_aa64_rule[sep_heap_rules del]
apply (sep_auto simp: uint64_nat_rel_def br_def)
apply (rule frame_rule, rule frame_rule)
apply (rule update_aa_rule_pure)
apply (auto simp: swap_ll_def arrayO_except_assn_def
length_ll_update_ll uint64_nat_rel_def br_def)
apply sep_auto
apply (rule cons_post_rule)
apply (subst assn_times_assoc)
apply (rule frame_rule)
apply (rule frame_rule_left)
apply (subst assn_times_comm)
apply (rule_tac R=R and ba= ‹nat_of_uint64 bi› in update_aa64_rule)
apply (auto simp: length_ll_def update_ll_def uint64_nat_rel_def br_def)[4]
apply (sep_auto simp: uint64_nat_rel_def br_def length_ll_def update_ll_def nth_ll_def swap_def)
done
qed
text ‹It is not possible to do a direct initialisation: there is no element that can be put
everywhere.›
definition arrayO_ara_empty_sz where
‹arrayO_ara_empty_sz n =
(let xs = fold (λ_ xs. [] # xs) [0..<n] [] in
op_list_copy xs)
›
lemma of_list_op_list_copy_arrayO[sepref_fr_rules]:
‹(Array.of_list, RETURN ∘ op_list_copy) ∈ (list_assn (arl64_assn R))⇧d →⇩a arrayO_assn (arl64_assn R)›
apply sepref_to_hoare
apply (sep_auto simp: arrayO_assn_def array_assn_def)
apply (rule_tac ?psi=‹xa ↦⇩a xi * list_assn (arl64_assn R) x xi ⟹⇩A
is_array xi xa * heap_list_all (arl64_assn R) x xi * true› in asm_rl)
by (sep_auto simp: heap_list_all_list_assn is_array_def)
sepref_definition
arrayO_ara_empty_sz_code
is "RETURN o arrayO_ara_empty_sz"
:: ‹nat_assn⇧k →⇩a arrayO_assn (arl64_assn (R::'a ⇒ 'b::{heap, default} ⇒ assn))›
unfolding arrayO_ara_empty_sz_def op_list_empty_def[symmetric]
apply (rewrite at ‹(#) ⌑› op_arl64_empty_def[symmetric])
apply (rewrite at ‹fold _ _ ⌑› op_HOL_list_empty_def[symmetric])
supply [[goals_limit = 1]]
by sepref
definition init_lrl64 :: ‹nat ⇒ _› where
[simp]: ‹init_lrl64 = init_lrl›
lemma arrayO_ara_empty_sz_init_lrl: ‹arrayO_ara_empty_sz n = init_lrl64 n›
by (induction n) (auto simp: arrayO_ara_empty_sz_def init_lrl_def)
lemma arrayO_raa_empty_sz_init_lrl[sepref_fr_rules]:
‹(arrayO_ara_empty_sz_code, RETURN o init_lrl64) ∈
nat_assn⇧k →⇩a arrayO_assn (arl64_assn R)›
using arrayO_ara_empty_sz_code.refine unfolding arrayO_ara_empty_sz_init_lrl .
definition (in -) shorten_take_aa64 where
‹shorten_take_aa64 L j W = do {
(a, n) ← Array.nth W L;
Array.upd L (a, j) W
}›
lemma Array_upd_arrayO_except_assn2[sep_heap_rules]:
assumes
‹ba ≤ length (b ! a)› and
‹a < length b› and ‹(ba', ba) ∈ uint64_nat_rel›
shows ‹<arrayO_except_assn (arl64_assn R) [a] b bi
(λr'. ↑ ((aaa, n) = r' ! a)) * arl64_assn R (b ! a) (aaa, n)>
Array.upd a (aaa, ba') bi
<λr. ∃⇩Ax. arrayO_assn (arl64_assn R) x r * true *
↑ (x = b[a := take ba (b ! a)])>›
using Array_upd_arrayO_except_assn
proof -
have [simp]: ‹nat_of_uint64 ba' ≤ length l'›
if
‹ba ≤ length (b ! a)› and
aa: ‹(take n' l', b ! a) ∈ ⟨the_pure R⟩list_rel›
for l' :: ‹'b list› and n'
proof -
show ?thesis
using list_rel_imp_same_length[OF aa] that assms(3)
by (auto simp: uint64_nat_rel_def br_def)
qed
have [simp]: ‹(take (nat_of_uint64 ba') l', take (nat_of_uint64 ba') (b ! a)) ∈ ⟨the_pure R⟩list_rel›
if
‹ba ≤ length (b ! a)› and
‹n' ≤ length l'› and
take: ‹(take n' l', b ! a) ∈ ⟨the_pure R⟩list_rel›
for l' :: ‹'b list› and n'
proof -
have [simp]: ‹n' = length (b ! a)›
using list_rel_imp_same_length[OF take] that by auto
have 1: ‹take (nat_of_uint64 ba') l' = take (nat_of_uint64 ba') (take n' l')›
using that assms(3) by (auto simp: min_def uint64_nat_rel_def br_def)
show ?thesis
using take
unfolding 1
by (rule list_rel_take)
qed
show ?thesis
using assms
unfolding arrayO_except_assn_def
apply (subst (2) arl64_assn_def)
apply (subst is_array_list64_def[abs_def])
apply (subst hr_comp_def[abs_def])
apply (subst array_assn_def)
apply (subst is_array_def[abs_def])
apply (subst hr_comp_def[abs_def])
apply sep_auto
apply (subst arrayO_except_assn_array0_index[symmetric, of a])
apply (solves simp)
unfolding arrayO_except_assn_def array_assn_def is_array_def
apply (subst (3) arl64_assn_def)
apply (subst is_array_list64_def[abs_def])
apply (subst (2) hr_comp_def[abs_def])
apply (subst ex_assn_move_out)+
apply (rule_tac x=‹p[a := (aaa, ba')]› in ent_ex_postI)
apply (rule_tac x=‹take ba l'› in ent_ex_postI)
apply (sep_auto simp: uint64_nat_rel_def br_def list_rel_imp_same_length
nat_of_uint64_le_uint64_max intro!: split: prod.splits)
apply (subst (2) heap_list_all_nth_cong[of _ _ b _ p])
apply auto
apply sep_auto
done
qed
lemma shorten_take_aa_hnr[sepref_fr_rules]:
‹(uncurry2 shorten_take_aa64, uncurry2 (RETURN ooo shorten_take_ll)) ∈
[λ((L, j), W). j ≤ length (W ! L) ∧ L < length W]⇩a
nat_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a (arrayO_assn (arl64_assn R))⇧d → arrayO_assn (arl64_assn R)›
unfolding shorten_take_aa64_def shorten_take_ll_def
by sepref_to_hoare sep_auto
definition nth_aa64_u where
‹nth_aa64_u x L L' = nth_aa64 x (nat_of_uint32 L) L'›
lemma nth_aa_uint_hnr[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure R›
shows
‹(uncurry2 nth_aa64_u, uncurry2 (RETURN ooo nth_rll)) ∈
[λ((x, L), L'). L < length x ∧ L' < length (x ! L)]⇩a
(arrayO_assn (arl64_assn R))⇧k *⇩a uint32_nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
unfolding nth_aa_u_def
apply auto
by sepref_to_hoare
(use assms in ‹sep_auto simp: uint32_nat_rel_def br_def length_ll_def nth_ll_def
nth_rll_def nth_aa64_u_def›)
lemma nth_aa64_u_code[code]:
‹nth_aa64_u x L L' = nth_u_code x L ⤜ (λx. arl64_get x L' ⤜ return)›
unfolding nth_aa64_u_def nth_aa64_def arl_get_u_def[symmetric] Array.nth'_def[symmetric]
nth_nat_of_uint32_nth' nth_u_code_def[symmetric] ..
definition nth_aa64_i64_u64 where
‹nth_aa64_i64_u64 xs x L = nth_aa64 xs (nat_of_uint64 x) L›
lemma nth_aa64_i64_u64_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_aa64_i64_u64, uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arrayO_assn (arl64_assn R))⇧k *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
unfolding nth_aa64_i64_u64_def
supply nth_aa64_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare
(sep_auto simp: br_def nth_aa64_i64_u64_def uint64_nat_rel_def
length_rll_def length_ll_def nth_rll_def nth_ll_def)
definition nth_aa64_i32_u64 where
‹nth_aa64_i32_u64 xs x L = nth_aa64 xs (nat_of_uint32 x) L›
lemma nth_aa64_i32_u64_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_aa64_i32_u64, uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arrayO_assn (arl64_assn R))⇧k *⇩a uint32_nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
unfolding nth_aa64_i32_u64_def
supply nth_aa64_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare
(sep_auto simp: uint32_nat_rel_def br_def uint64_nat_rel_def
length_rll_def length_ll_def nth_rll_def nth_ll_def)
definition append64_el_aa32 :: "('a::{default,heap} array_list64) array ⇒
uint32 ⇒ 'a ⇒ ('a array_list64) array Heap"where
"append64_el_aa32 ≡ λa i x. do {
j ← nth_u_code a i;
a' ← arl64_append j x;
heap_array_set_u a i a'
}"
lemma append64_aa32_hnr[sepref_fr_rules]:
fixes R :: ‹'a ⇒ 'b :: {heap, default} ⇒ assn›
assumes p: ‹is_pure R›
shows
‹(uncurry2 append64_el_aa32, uncurry2 (RETURN ∘∘∘ append_ll)) ∈
[λ((l,i),x). i < length l ∧ length (l ! i) < uint64_max]⇩a (arrayO_assn (arl64_assn R))⇧d *⇩a uint32_nat_assn⇧k *⇩a R⇧k → (arrayO_assn (arl64_assn R))›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have [simp]: ‹(∃⇩Ax. arrayO_assn (arl64_assn R) a ai * R x r * true * ↑ (x = a ! ba ! b)) =
(arrayO_assn (arl64_assn R) a ai * R (a ! ba ! b) r * true)› for a ai ba b r
by (auto simp: ex_assn_def)
show ?thesis
apply sepref_to_hoare
apply (sep_auto simp: append64_el_aa32_def nth_u_code_def Array.nth'_def uint32_nat_rel_def br_def
nat_of_uint32_code[symmetric] heap_array_set'_u_def heap_array_set_u_def Array.upd'_def)
apply (simp add: arrayO_except_assn_def)
apply (rule sep_auto_is_stupid[OF p])
apply simp
apply (sep_auto simp: array_assn_def is_array_def append_ll_def)
apply (simp add: arrayO_except_assn_array0[symmetric] arrayO_except_assn_def)
apply (subst_tac (2) i = ‹nat_of_uint32 bia› in heap_list_all_nth_remove1)
apply (solves ‹simp›)
apply (simp add: array_assn_def is_array_def)
apply (rule_tac x=‹p[nat_of_uint32 bia := (ab, bb)]› in ent_ex_postI)
apply (subst_tac (2)xs'=a and ys'=p in heap_list_all_nth_cong)
apply (solves ‹auto›)+
apply sep_auto
done
qed
definition update_aa64_u32 :: "('a::{heap} array_list64) array ⇒ uint32 ⇒ uint64 ⇒ 'a ⇒ ('a array_list64) array Heap" where
‹update_aa64_u32 a i j y = update_aa64 a (nat_of_uint32 i) j y›
lemma update_aa_u64_u32_code[code]:
‹update_aa64_u32 a i j y = do {
x ← nth_u_code a i;
a' ← arl64_set x j y;
Array_upd_u i a' a
}›
unfolding update_aa64_u32_def update_aa64_def update_aa_def nth_nat_of_uint32_nth' nth_nat_of_uint32_nth'
arl_get_u_def[symmetric] nth_u64_code_def Array.nth'_def comp_def Array_upd_u_def nth_u_code_def
heap_array_set'_u_def[symmetric] Array_upd_u64_def nat_of_uint64_code[symmetric]
by auto
lemma update_aa64_u32_rule[sep_heap_rules]:
assumes p: ‹is_pure R› and ‹bb < length a› and ‹ba < length_ll a bb› ‹(ba', ba) ∈ uint64_nat_rel› ‹(bb', bb) ∈ uint32_nat_rel›
shows ‹<R b bi * arrayO_assn (arl64_assn R) a ai> update_aa64_u32 ai bb' ba' bi
<λr. R b bi * (∃⇩Ax. arrayO_assn (arl64_assn R) x r * ↑ (x = update_ll a bb ba b))>⇩t›
using assms supply return_sp_rule[sep_heap_rules] upd_rule[sep_heap_rules del]
apply (sep_auto simp add: update_aa64_u32_def update_ll_def nth_u_code_def Array.nth'_def
nat_of_uint32_code[symmetric] uint32_nat_rel_def br_def)
done
lemma update_aa64_u32_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 update_aa64_u32, uncurry3 (RETURN oooo update_ll)) ∈
[λ(((l,i), j), x). i < length l ∧ j < length_ll l i]⇩a (arrayO_assn (arl64_assn R))⇧d *⇩a uint32_nat_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a R⇧k → (arrayO_assn (arl64_assn R))›
by sepref_to_hoare (sep_auto simp: assms)
definition nth_aa64_u64 where
‹nth_aa64_u64 xs i j = do {
x ← nth_u64_code xs i;
y ← arl64_get x j;
return y}›
lemma nth_aa64_u64_hnr[sepref_fr_rules]:
assumes p: ‹CONSTRAINT is_pure R›
shows
‹(uncurry2 nth_aa64_u64, uncurry2 (RETURN ∘∘∘ nth_ll)) ∈
[λ((l,i),j). i < length l ∧ j < length_ll l i]⇩a
(arrayO_assn (arl64_assn R))⇧k *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have H: ‹list_all2 (λx x'. (x, x') ∈ the_pure (λa c. ↑ ((c, a) ∈ R'))) bc (a ! ba) ⟹
b < length (a ! ba) ⟹
(bc ! b, a ! ba ! b) ∈ R'› for bc a ba b
by (auto simp add: ent_refl_true list_all2_conv_all_nth is_pure_alt_def pure_app_eq[symmetric])
show ?thesis
using p
apply sepref_to_hoare
apply (sep_auto simp: nth_aa64_u64_def length_ll_def nth_ll_def nth_u64_def nth_u64_code_def Array.nth'_def
nat_of_uint64_code[symmetric] br_def uint64_nat_rel_def)
apply (subst arrayO_except_assn_array0_index[symmetric, of ‹nat_of_uint64 bia›])
apply simp
apply (sep_auto simp: arrayO_except_assn_def arrayO_assn_def arl64_assn_def hr_comp_def list_rel_def
list_all2_lengthD
star_aci(3) R R' pure_def H)
done
qed
definition arl64_get_nat :: "'a::heap array_list64 ⇒ nat ⇒ 'a Heap" where
"arl64_get_nat ≡ λ(a,n) i. Array.nth a i"
lemma arl_get_rule[sep_heap_rules]: "
i<length l ⟹
<is_array_list64 l a>
arl64_get_nat a i
<λr. is_array_list64 l a * ↑(r=l!i)>"
supply nth_rule[sep_heap_rules]
by (sep_auto simp: is_array_list64_def arl64_get_nat_def is_array_list_def split: prod.split)
lemma arl_get_rule_arl64[sep_heap_rules]: "
i<length l ⟹
<arl64_assn T l a>
arl64_get_nat a i
<λr. arl64_assn T l a * ↑((r, l!i) ∈ the_pure T)>"
using param_nth[of i l i _ ‹the_pure T›]
by (sep_auto simp: arl64_assn_def hr_comp_def dest: list_rel_imp_same_length split: prod.split)
definition nth_aa64_nat where
‹nth_aa64_nat xs i j = do {
x ← Array.nth xs i;
y ← arl64_get_nat x j;
return y}›
lemma nth_aa64_nat_hnr[sepref_fr_rules]:
assumes p: ‹CONSTRAINT is_pure R›
shows
‹(uncurry2 nth_aa64_nat, uncurry2 (RETURN ∘∘∘ nth_ll)) ∈
[λ((l,i),j). i < length l ∧ j < length_ll l i]⇩a
(arrayO_assn (arl64_assn R))⇧k *⇩a nat_assn⇧k *⇩a nat_assn⇧k → R›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
have [simp]: ‹the_pure (λa c. ↑ ((c, a) ∈ R')) = R'›
unfolding R[symmetric] pure_app_eq[symmetric] by auto
show ?thesis
using p
apply sepref_to_hoare
apply (sep_auto simp: nth_aa64_nat_def length_ll_def nth_ll_def)
apply (subst arrayO_except_assn_array0_index[symmetric, of ba])
apply simp
apply (sep_auto simp: arrayO_except_assn_def arrayO_assn_def arl64_assn_def hr_comp_def list_rel_def
star_aci(3) R R' pure_def)
done
qed
definition length_aa64_nat :: ‹('a::heap array_list64) array ⇒ nat ⇒ nat Heap› where
‹length_aa64_nat xs i = do {
x ← Array.nth xs i;
n ← arl64_length x;
return (nat_of_uint64 n)}›
lemma length_aa64_nat_rule[sep_heap_rules]:
‹b < length xs ⟹ <arrayO_assn (arl64_assn R) xs a> length_aa64_nat a b
<λr. arrayO_assn (arl64_assn R) xs a * ↑ (r = length_ll xs b)>⇩t›
unfolding length_aa64_nat_def nth_u64_code_def Array.nth'_def
apply (sep_auto simp flip: nat_of_uint64_code simp: br_def uint64_nat_rel_def length_ll_def)
apply (subst arrayO_except_assn_array0_index[symmetric, of b])
apply (simp add: nat_of_uint64_code br_def uint64_nat_rel_def)
apply (sep_auto simp: arrayO_except_assn_def)
done
lemma length_aa64_nat_hnr[sepref_fr_rules]: ‹(uncurry length_aa64_nat, uncurry (RETURN ∘∘ length_ll)) ∈
[λ(xs, i). i < length xs]⇩a (arrayO_assn (arl64_assn R))⇧k *⇩a nat_assn⇧k → nat_assn›
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def)
end