theory IICF_Array_List64
imports
"Refine_Imperative_HOL.IICF_List"
Separation_Logic_Imperative_HOL.Array_Blit
Array_UInt
WB_Word_Assn
begin
type_synonym 'a array_list64 = "'a Heap.array × uint64"
definition "is_array_list64 l ≡ λ(a,n). ∃⇩Al'. a ↦⇩a l' * ↑(nat_of_uint64 n ≤ length l' ∧ l = take (nat_of_uint64 n) l' ∧ length l'>0 ∧ nat_of_uint64 n ≤ uint64_max ∧ length l' ≤ uint64_max)"
lemma is_array_list64_prec[safe_constraint_rules]: "precise is_array_list64"
unfolding is_array_list64_def[abs_def]
apply(rule preciseI)
apply(simp split: prod.splits)
using preciseD snga_prec by fastforce
definition "arl64_empty ≡ do {
a ← Array.new initial_capacity default;
return (a,0)
}"
definition "arl64_empty_sz init_cap ≡ do {
a ← Array.new (min uint64_max (max init_cap minimum_capacity)) default;
return (a,0)
}"
definition uint64_max_uint64 :: uint64 where
‹uint64_max_uint64 = 2 ^64 - 1›
definition "arl64_append ≡ λ(a,n) x. do {
len ← length_u64_code a;
if n<len then do {
a ← Array_upd_u64 n x a;
return (a,n+1)
} else do {
let newcap = (if len < uint64_max_uint64 >> 1 then 2 * len else uint64_max_uint64);
a ← array_grow a (nat_of_uint64 newcap) default;
a ← Array_upd_u64 n x a;
return (a,n+1)
}
}"
definition "arl64_copy ≡ λ(a,n). do {
a ← array_copy a;
return (a,n)
}"
definition arl64_length :: "'a::heap array_list64 ⇒ uint64 Heap" where
"arl64_length ≡ λ(a,n). return (n)"
definition arl64_is_empty :: "'a::heap array_list64 ⇒ bool Heap" where
"arl64_is_empty ≡ λ(a,n). return (n=0)"
definition arl64_last :: "'a::heap array_list64 ⇒ 'a Heap" where
"arl64_last ≡ λ(a,n). do {
nth_u64_code a (n - 1)
}"
definition arl64_butlast :: "'a::heap array_list64 ⇒ 'a array_list64 Heap" where
"arl64_butlast ≡ λ(a,n). do {
let n = n - 1;
len ← length_u64_code a;
if (n*4 < len ∧ nat_of_uint64 n*2≥minimum_capacity) then do {
a ← array_shrink a (nat_of_uint64 n*2);
return (a,n)
} else
return (a,n)
}"
definition arl64_get :: "'a::heap array_list64 ⇒ uint64 ⇒ 'a Heap" where
"arl64_get ≡ λ(a,n) i. nth_u64_code a i"
definition arl64_set :: "'a::heap array_list64 ⇒ uint64 ⇒ 'a ⇒ 'a array_list64 Heap" where
"arl64_set ≡ λ(a,n) i x. do { a ← heap_array_set_u64 a i x; return (a,n)}"
lemma arl64_empty_rule[sep_heap_rules]: "< emp > arl64_empty <is_array_list64 []>"
by (sep_auto simp: arl64_empty_def is_array_list64_def initial_capacity_def uint64_max_def)
lemma arl64_empty_sz_rule[sep_heap_rules]: "< emp > arl64_empty_sz N <is_array_list64 []>"
by (sep_auto simp: arl64_empty_sz_def is_array_list64_def minimum_capacity_def uint64_max_def)
lemma arl64_copy_rule[sep_heap_rules]: "< is_array_list64 l a > arl64_copy a <λr. is_array_list64 l a * is_array_list64 l r>"
by (sep_auto simp: arl64_copy_def is_array_list64_def)
lemma [simp]: ‹nat_of_uint64 uint64_max_uint64 = uint64_max›
by (auto simp: nat_of_uint64_mult_le nat_of_uint64_shiftl uint64_max_uint64_def uint64_max_def)[]
lemma ‹2 * (uint64_max div 2) = uint64_max - 1›
by (auto simp: nat_of_uint64_mult_le nat_of_uint64_shiftl uint64_max_uint64_def uint64_max_def)[]
lemma nat_of_uint64_0_iff: ‹nat_of_uint64 x2 = 0 ⟷ x2 = 0›
using word_nat_of_uint64_Rep_inject by fastforce
lemma arl64_append_rule[sep_heap_rules]:
assumes ‹length l < uint64_max›
shows "< is_array_list64 l a >
arl64_append a x
<λa. is_array_list64 (l@[x]) a >⇩t"
proof -
have [simp]: ‹⋀x1 x2 y ys.
x2 < uint64_of_nat ys ⟹
nat_of_uint64 x2 ≤ ys ⟹
ys ≤ uint64_max ⟹ nat_of_uint64 x2 < ys›
by (metis nat_of_uint64_less_iff nat_of_uint64_uint64_of_nat_id)
have [simp]: ‹⋀x2 ys. x2 < uint64_of_nat (Suc (ys)) ⟹
Suc (ys) ≤ uint64_max ⟹
nat_of_uint64 (x2 + 1) = 1 + nat_of_uint64 x2›
by (smt ab_semigroup_add_class.add.commute le_neq_implies_less less_or_eq_imp_le
less_trans_Suc linorder_neqE_nat nat_of_uint64_012(3) nat_of_uint64_add
nat_of_uint64_less_iff nat_of_uint64_uint64_of_nat_id not_less_eq plus_1_eq_Suc)
have [dest]: ‹⋀x2a x2 ys. x2 < uint64_of_nat (Suc (ys)) ⟹
Suc (ys) ≤ uint64_max ⟹
nat_of_uint64 x2 = Suc x2a ⟹Suc x2a ≤ ys›
by (metis less_Suc_eq_le nat_of_uint64_less_iff nat_of_uint64_uint64_of_nat_id)
have [simp]: ‹⋀ys. ys ≤ uint64_max ⟹
uint64_of_nat ys ≤ uint64_max_uint64 >> Suc 0 ⟹
nat_of_uint64 (2 * uint64_of_nat ys) = 2 * ys›
by (subst (asm) nat_of_uint64_le_iff[symmetric])
(auto simp: nat_of_uint64_uint64_of_nat_id uint64_max_uint64_def uint64_max_def nat_of_uint64_shiftl
nat_of_uint64_mult_le)
have [simp]: ‹⋀ys. ys ≤ uint64_max ⟹
uint64_of_nat ys ≤ uint64_max_uint64 >> Suc 0 ⟷ ys ≤ uint64_max div 2›
by (subst nat_of_uint64_le_iff[symmetric])
(auto simp: nat_of_uint64_uint64_of_nat_id uint64_max_uint64_def uint64_max_def nat_of_uint64_shiftl
nat_of_uint64_mult_le)
have [simp]: ‹⋀ys. ys ≤ uint64_max ⟹
uint64_of_nat ys < uint64_max_uint64 >> Suc 0 ⟷ ys < uint64_max div 2›
by (subst nat_of_uint64_less_iff[symmetric])
(auto simp: nat_of_uint64_uint64_of_nat_id uint64_max_uint64_def uint64_max_def nat_of_uint64_shiftl
nat_of_uint64_mult_le)
show ?thesis
using assms
apply (sep_auto
simp: arl64_append_def is_array_list64_def take_update_last neq_Nil_conv nat_of_uint64_mult_le
length_u64_code_def min_def nat_of_uint64_add nat_of_uint64_uint64_of_nat_id
take_Suc_conv_app_nth list_update_append nat_of_uint64_0_iff
split: if_split
split: prod.splits nat.split)
apply (subst Array_upd_u64_def)
apply (sep_auto
simp: arl64_append_def is_array_list64_def take_update_last neq_Nil_conv nat_of_uint64_mult_le
length_u64_code_def min_def nat_of_uint64_add nat_of_uint64_uint64_of_nat_id
take_Suc_conv_app_nth list_update_append
split: if_split
split: prod.splits nat.split)
apply (sep_auto
simp: arl64_append_def is_array_list64_def take_update_last neq_Nil_conv nat_of_uint64_mult_le
length_u64_code_def min_def nat_of_uint64_add nat_of_uint64_uint64_of_nat_id
take_Suc_conv_app_nth list_update_append
split: if_split
split: prod.splits nat.split)
apply (sep_auto
simp: arl64_append_def is_array_list64_def take_update_last neq_Nil_conv nat_of_uint64_mult_le
length_u64_code_def min_def nat_of_uint64_add nat_of_uint64_uint64_of_nat_id
take_Suc_conv_app_nth list_update_append
split: if_split
split: prod.splits nat.split)
apply (subst Array_upd_u64_def)
apply (sep_auto
simp: arl64_append_def is_array_list64_def take_update_last neq_Nil_conv nat_of_uint64_mult_le
length_u64_code_def min_def nat_of_uint64_add nat_of_uint64_uint64_of_nat_id
take_Suc_conv_app_nth list_update_append
split: if_split
split: prod.splits nat.split)
apply (sep_auto
simp: arl64_append_def is_array_list64_def take_update_last neq_Nil_conv nat_of_uint64_mult_le
length_u64_code_def min_def nat_of_uint64_add nat_of_uint64_uint64_of_nat_id
take_Suc_conv_app_nth list_update_append
split: if_split
split: prod.splits nat.split)
apply (sep_auto
simp: arl64_append_def is_array_list64_def take_update_last neq_Nil_conv nat_of_uint64_mult_le
length_u64_code_def min_def nat_of_uint64_add nat_of_uint64_uint64_of_nat_id
take_Suc_conv_app_nth list_update_append
split: if_split
split: prod.splits nat.split)
apply (subst Array_upd_u64_def)
apply (rule frame_rule)
apply (rule upd_rule)
apply (sep_auto
simp: arl64_append_def is_array_list64_def take_update_last neq_Nil_conv nat_of_uint64_mult_le
length_u64_code_def min_def nat_of_uint64_add nat_of_uint64_uint64_of_nat_id
take_Suc_conv_app_nth list_update_append nat_of_uint64_0_iff
split: if_splits
split: prod.splits nat.split)
apply (sep_auto
simp: arl64_append_def is_array_list64_def take_update_last neq_Nil_conv nat_of_uint64_mult_le
length_u64_code_def min_def nat_of_uint64_add nat_of_uint64_uint64_of_nat_id
take_Suc_conv_app_nth list_update_append
split: if_splits
split: prod.splits nat.split)
done
qed
lemma arl64_length_rule[sep_heap_rules]: "
<is_array_list64 l a>
arl64_length a
<λr. is_array_list64 l a * ↑(nat_of_uint64 r=length l)>"
by (sep_auto simp: arl64_length_def is_array_list64_def)
lemma arl64_is_empty_rule[sep_heap_rules]: "
<is_array_list64 l a>
arl64_is_empty a
<λr. is_array_list64 l a * ↑(r⟷(l=[]))>"
by (sep_auto simp: arl64_is_empty_def nat_of_uint64_0_iff is_array_list64_def)
lemma arl64_last_rule[sep_heap_rules]: "
l≠[] ⟹
<is_array_list64 l a>
arl64_last a
<λr. is_array_list64 l a * ↑(r=last l)>"
by (sep_auto simp: arl64_last_def is_array_list64_def nth_u64_code_def Array.nth'_def last_take_nth_conv
nat_of_integer_integer_of_nat nat_of_uint64_ge_minus nat_of_uint64_le_iff[symmetric]
simp flip: nat_of_uint64_code)
lemma arl64_get_rule[sep_heap_rules]: "
i<length l ⟹ (i', i) ∈ uint64_nat_rel ⟹
<is_array_list64 l a>
arl64_get a i'
<λr. is_array_list64 l a * ↑(r=l!i)>"
by (sep_auto simp: arl64_get_def nth_u64_code_def is_array_list64_def uint64_nat_rel_def
Array.nth'_def br_def split: prod.split simp flip: nat_of_uint64_code)
lemma arl64_set_rule[sep_heap_rules]: "
i<length l ⟹ (i', i) ∈ uint64_nat_rel ⟹
<is_array_list64 l a>
arl64_set a i' x
<is_array_list64 (l[i:=x])>"
by (sep_auto simp: arl64_set_def is_array_list64_def heap_array_set_u64_def uint64_nat_rel_def
heap_array_set'_u64_def br_def Array.upd'_def split: prod.split simp flip: nat_of_uint64_code)
definition "arl64_assn A ≡ hr_comp is_array_list64 (⟨the_pure A⟩list_rel)"
lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure "arl64_assn A" for A]
lemma arl64_assn_comp: "is_pure A ⟹ hr_comp (arl64_assn A) (⟨B⟩list_rel) = arl64_assn (hr_comp A B)"
unfolding arl64_assn_def
by (auto simp: hr_comp_the_pure hr_comp_assoc list_rel_compp)
lemma arl64_assn_comp': "hr_comp (arl64_assn id_assn) (⟨B⟩list_rel) = arl64_assn (pure B)"
by (simp add: arl64_assn_comp)
context
notes [fcomp_norm_unfold] = arl64_assn_def[symmetric] arl64_assn_comp'
notes [intro!] = hfrefI hn_refineI[THEN hn_refine_preI]
notes [simp] = pure_def hn_ctxt_def invalid_assn_def
begin
lemma arl64_empty_hnr_aux: "(uncurry0 arl64_empty,uncurry0 (RETURN op_list_empty)) ∈ unit_assn⇧k →⇩a is_array_list64"
by sep_auto
sepref_decl_impl (no_register) arl64_empty: arl64_empty_hnr_aux .
lemma arl64_empty_sz_hnr_aux: "(uncurry0 (arl64_empty_sz N),uncurry0 (RETURN op_list_empty)) ∈ unit_assn⇧k →⇩a is_array_list64"
by sep_auto
sepref_decl_impl (no_register) arl64_empty_sz: arl64_empty_sz_hnr_aux .
definition "op_arl64_empty ≡ op_list_empty"
definition "op_arl64_empty_sz (N::nat) ≡ op_list_empty"
lemma arl64_copy_hnr_aux: "(arl64_copy,RETURN o op_list_copy) ∈ is_array_list64⇧k →⇩a is_array_list64"
by sep_auto
sepref_decl_impl arl64_copy: arl64_copy_hnr_aux .
lemma arl64_append_hnr_aux: "(uncurry arl64_append,uncurry (RETURN oo op_list_append)) ∈ [λ(xs, x). length xs < uint64_max]⇩a (is_array_list64⇧d *⇩a id_assn⇧k) → is_array_list64"
by sep_auto
sepref_decl_impl arl64_append: arl64_append_hnr_aux
unfolding fref_param1 by (auto intro!: frefI nres_relI simp: list_rel_imp_same_length)
lemma arl64_length_hnr_aux: "(arl64_length,RETURN o op_list_length) ∈ is_array_list64⇧k →⇩a uint64_nat_assn"
by (sep_auto simp: uint64_nat_rel_def br_def)
sepref_decl_impl arl64_length: arl64_length_hnr_aux .
lemma arl64_is_empty_hnr_aux: "(arl64_is_empty,RETURN o op_list_is_empty) ∈ is_array_list64⇧k →⇩a bool_assn"
by sep_auto
sepref_decl_impl arl64_is_empty: arl64_is_empty_hnr_aux .
lemma arl64_last_hnr_aux: "(arl64_last,RETURN o op_list_last) ∈ [pre_list_last]⇩a is_array_list64⇧k → id_assn"
by sep_auto
sepref_decl_impl arl64_last: arl64_last_hnr_aux .
lemma arl64_get_hnr_aux: "(uncurry arl64_get,uncurry (RETURN oo op_list_get)) ∈ [λ(l,i). i<length l]⇩a (is_array_list64⇧k *⇩a uint64_nat_assn⇧k) → id_assn"
by sep_auto
sepref_decl_impl arl64_get: arl64_get_hnr_aux .
lemma arl64_set_hnr_aux: "(uncurry2 arl64_set,uncurry2 (RETURN ooo op_list_set)) ∈ [λ((l,i),_). i<length l]⇩a (is_array_list64⇧d *⇩a uint64_nat_assn⇧k *⇩a id_assn⇧k) → is_array_list64"
by sep_auto
sepref_decl_impl arl64_set: arl64_set_hnr_aux .
sepref_definition arl64_swap is "uncurry2 mop_list_swap" :: "((arl64_assn id_assn)⇧d *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a arl64_assn id_assn)"
unfolding gen_mop_list_swap[abs_def]
by sepref
sepref_decl_impl (ismop) arl64_swap: arl64_swap.refine .
end
interpretation arl64: list_custom_empty "arl64_assn A" arl64_empty op_arl64_empty
apply unfold_locales
apply (rule arl64_empty_hnr)
by (auto simp: op_arl64_empty_def)
lemma [def_pat_rules]: "op_arl64_empty_sz$N ≡ UNPROTECT (op_arl64_empty_sz N)" by simp
interpretation arl64_sz: list_custom_empty "arl64_assn A" "arl64_empty_sz N" "PR_CONST (op_arl64_empty_sz N)"
apply unfold_locales
apply (rule arl64_empty_sz_hnr)
by (auto simp: op_arl64_empty_sz_def)
definition arl64_to_arl_conv where
‹arl64_to_arl_conv S = S›
definition arl64_to_arl :: ‹'a array_list64 ⇒ 'a array_list› where
‹arl64_to_arl = (λ(xs, n). (xs, nat_of_uint64 n))›
lemma arl64_to_arl_hnr[sepref_fr_rules]:
‹(return o arl64_to_arl, RETURN o arl64_to_arl_conv) ∈ (arl64_assn R)⇧d →⇩a arl_assn R›
by (sepref_to_hoare)
(sep_auto simp: arl64_to_arl_def arl64_to_arl_conv_def arl_assn_def arl64_assn_def is_array_list64_def
is_array_list_def hr_comp_def)
definition arl64_take where
‹arl64_take n = (λ(xs, _). (xs, n))›
lemma arl64_take[sepref_fr_rules]:
‹(uncurry (return oo arl64_take), uncurry (RETURN oo take)) ∈
[λ(n, xs). n ≤ length xs]⇩a uint64_nat_assn⇧k *⇩a (arl64_assn R)⇧d → arl64_assn R›
by (sepref_to_hoare)
(sep_auto simp: arl64_assn_def arl64_take_def is_array_list64_def hr_comp_def
uint64_nat_rel_def br_def list_rel_def list_all2_conv_all_nth)
definition arl64_of_arl :: ‹'a list ⇒ 'a list› where
‹arl64_of_arl S = S›
definition arl64_of_arl_code :: ‹'a :: heap array_list ⇒ 'a array_list64 Heap› where
‹arl64_of_arl_code = (λ(a, n). do {
m ← Array.len a;
if m > uint64_max then do {
a ← array_shrink a uint64_max;
return (a, (uint64_of_nat n))}
else return (a, (uint64_of_nat n))})›
lemma arl64_of_arl[sepref_fr_rules]:
‹(arl64_of_arl_code, RETURN o arl64_of_arl) ∈ [λn. length n ≤ uint64_max]⇩a (arl_assn R)⇧d → arl64_assn R›
proof -
have [iff]: ‹take uint64_max l' = [] ⟷ l' = []› ‹0 < uint64_max› for l'
by (auto simp: uint64_max_def)
have H: ‹x2 ≤ length l' ⟹
(take x2 l', x) ∈ ⟨the_pure R⟩list_rel ⟹ length x = x2›
‹x2 ≤ length l' ⟹
(take x2 l', x) ∈ ⟨the_pure R⟩list_rel ⟹ take (length x) = take x2› for x x2 l'
subgoal H by (auto dest: list_rel_imp_same_length)
subgoal using H by blast
done
show ?thesis
by sepref_to_hoare
(sep_auto simp: arl_assn_def arl64_assn_def is_array_list_def is_array_list64_def hr_comp_def arl64_of_arl_def
arl64_of_arl_code_def nat_of_uint64_code[symmetric] nat_of_uint64_uint64_of_nat_id
H min_def
split: prod.splits if_splits)
qed
definition arl_nat_of_uint64_conv :: ‹nat list ⇒ nat list› where
‹arl_nat_of_uint64_conv S = S›
lemma arl_nat_of_uint64_conv_alt_def:
‹arl_nat_of_uint64_conv = map nat_of_uint64_conv›
unfolding nat_of_uint64_conv_def arl_nat_of_uint64_conv_def by auto
sepref_definition arl_nat_of_uint64_code
is array_nat_of_uint64
:: ‹(arl_assn uint64_nat_assn)⇧k →⇩a arl_assn nat_assn›
unfolding op_map_def array_nat_of_uint64_def arl_fold_custom_replicate
apply (rewrite at ‹do {let _ = ⌑; _}› annotate_assn[where A=‹arl_assn nat_assn›])
by sepref
lemma arl_nat_of_uint64_conv_hnr[sepref_fr_rules]:
‹(arl_nat_of_uint64_code, (RETURN ∘ arl_nat_of_uint64_conv))
∈ (arl_assn uint64_nat_assn)⇧k →⇩a arl_assn nat_assn›
using arl_nat_of_uint64_code.refine[unfolded array_nat_of_uint64_def,
FCOMP op_map_map_rel[unfolded convert_fref]] unfolding arl_nat_of_uint64_conv_alt_def
by simp
end