theory Array_UInt
imports Array_List_Array WB_Word_Assn WB_More_Refinement_List
begin
hide_const Autoref_Fix_Rel.CONSTRAINT
lemma convert_fref:
"WB_More_Refinement.fref = Sepref_Rules.fref"
"WB_More_Refinement.freft = Sepref_Rules.freft"
unfolding WB_More_Refinement.fref_def Sepref_Rules.fref_def
by auto
subsection ‹More about general arrays›
text ‹
This function does not resize the array: this makes sense for our purpose, but may be not in
general.›
definition butlast_arl where
‹butlast_arl = (λ(xs, i). (xs, fast_minus i 1))›
lemma butlast_arl_hnr[sepref_fr_rules]:
‹(return o butlast_arl, RETURN o butlast) ∈ [λxs. xs ≠ []]⇩a (arl_assn A)⇧d → arl_assn A›
proof -
have [simp]: ‹b ≤ length l' ⟹ (take b l', x) ∈ ⟨the_pure A⟩list_rel ⟹
(take (b - Suc 0) l', take (length x - Suc 0) x) ∈ ⟨the_pure A⟩list_rel›
for b l' x
using list_rel_take[of ‹take b l'› x ‹the_pure A› ‹b -1›]
by (auto simp: list_rel_imp_same_length[symmetric]
butlast_conv_take min_def
simp del: take_butlast_conv)
show ?thesis
by sepref_to_hoare
(sep_auto simp: butlast_arl_def arl_assn_def hr_comp_def is_array_list_def
butlast_conv_take
simp del: take_butlast_conv)
qed
subsection ‹Setup for array accesses via unsigned integer›
text ‹
NB: not all code printing equation are defined here, but this is needed to use the (more efficient)
array operation by avoid the conversions back and forth to infinite integer.
›
subsubsection ‹Getters (Array accesses)›
paragraph ‹32-bit unsigned integers›
definition nth_aa_u where
‹nth_aa_u x L L' = nth_aa x (nat_of_uint32 L) L'›
definition nth_aa' where
‹nth_aa' xs i j = do {
x ← Array.nth' xs i;
y ← arl_get x j;
return y}›
lemma nth_aa_u[code]:
‹nth_aa_u x L L' = nth_aa' x (integer_of_uint32 L) L'›
unfolding nth_aa_u_def nth_aa'_def nth_aa_def Array.nth'_def nat_of_uint32_code
by auto
lemma nth_aa_uint_hnr[sepref_fr_rules]:
fixes R :: ‹_ ⇒ _ ⇒ assn›
assumes ‹CONSTRAINT Sepref_Basic.is_pure R›
shows
‹(uncurry2 nth_aa_u, uncurry2 (RETURN ooo nth_rll)) ∈
[λ((x, L), L'). L < length x ∧ L' < length (x ! L)]⇩a
(arrayO_assn (arl_assn R))⇧k *⇩a uint32_nat_assn⇧k *⇩a nat_assn⇧k → R›
unfolding nth_aa_u_def
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›)
definition nth_raa_u where
‹nth_raa_u x L = nth_raa x (nat_of_uint32 L)›
lemma nth_raa_uint_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_raa_u, uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint32_nat_assn⇧k *⇩a nat_assn⇧k → R›
unfolding nth_raa_u_def
supply nth_aa_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare (sep_auto simp: uint32_nat_rel_def br_def)
lemma array_replicate_custom_hnr_u[sepref_fr_rules]:
‹CONSTRAINT is_pure A ⟹
(uncurry (λn. Array.new (nat_of_uint32 n)), uncurry (RETURN ∘∘ op_array_replicate)) ∈
uint32_nat_assn⇧k *⇩a A⇧k →⇩a array_assn A›
using array_replicate_custom_hnr[of A]
unfolding hfref_def
by (sep_auto simp: uint32_nat_assn_nat_assn_nat_of_uint32)
definition nth_u where
‹nth_u xs n = nth xs (nat_of_uint32 n)›
definition nth_u_code where
‹nth_u_code xs n = Array.nth' xs (integer_of_uint32 n)›
lemma nth_u_hnr[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure A›
shows ‹(uncurry nth_u_code, uncurry (RETURN oo nth_u)) ∈
[λ(xs, n). nat_of_uint32 n < length xs]⇩a (array_assn A)⇧k *⇩a uint32_assn⇧k → A›
proof -
obtain A' where
A: ‹pure A' = A›
using assms pure_the_pure by auto
then have A': ‹the_pure A = A'›
by auto
have [simp]: ‹the_pure (λa c. ↑ ((c, a) ∈ A')) = A'›
unfolding pure_def[symmetric] by auto
show ?thesis
by sepref_to_hoare
(sep_auto simp: array_assn_def is_array_def
hr_comp_def list_rel_pres_length list_rel_update param_nth A' A[symmetric] ent_refl_true
list_rel_eq_listrel listrel_iff_nth pure_def nth_u_code_def nth_u_def Array.nth'_def
nat_of_uint32_code)
qed
lemma array_get_hnr_u[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure A›
shows ‹(uncurry nth_u_code,
uncurry (RETURN ∘∘ op_list_get)) ∈ [pre_list_get]⇩a (array_assn A)⇧k *⇩a uint32_nat_assn⇧k → A›
proof -
obtain A' where
A: ‹pure A' = A›
using assms pure_the_pure by auto
then have A': ‹the_pure A = A'›
by auto
have [simp]: ‹the_pure (λa c. ↑ ((c, a) ∈ A')) = A'›
unfolding pure_def[symmetric] by auto
show ?thesis
by sepref_to_hoare
(sep_auto simp: uint32_nat_rel_def br_def ex_assn_up_eq2 array_assn_def is_array_def
hr_comp_def list_rel_pres_length list_rel_update param_nth A' A[symmetric] ent_refl_true
list_rel_eq_listrel listrel_iff_nth pure_def nth_u_code_def Array.nth'_def
nat_of_uint32_code)
qed
definition arl_get' :: "'a::heap array_list ⇒ integer ⇒ 'a Heap" where
[code del]: "arl_get' a i = arl_get a (nat_of_integer i)"
definition arl_get_u :: "'a::heap array_list ⇒ uint32 ⇒ 'a Heap" where
"arl_get_u ≡ λa i. arl_get' a (integer_of_uint32 i)"
lemma arrayO_arl_get_u_rule[sep_heap_rules]:
assumes i: ‹i < length a› and ‹(i' , i) ∈ uint32_nat_rel›
shows ‹<arlO_assn (array_assn R) a ai> arl_get_u ai i' <λr. arlO_assn_except (array_assn R) [i] a ai
(λr'. array_assn R (a ! i) r * ↑(r = r' ! i))>›
using assms
by (sep_auto simp: arl_get_u_def arl_get'_def nat_of_uint32_code[symmetric]
uint32_nat_rel_def br_def)
definition arl_get_u' where
[symmetric, code]: ‹arl_get_u' = arl_get_u›
code_printing constant arl_get_u' ⇀ (SML) "(fn/ ()/ =>/ Array.sub/ (fst (_),/ Word32.toInt (_)))"
lemma arl_get'_nth'[code]: ‹arl_get' = (λ(a, n). Array.nth' a)›
unfolding arl_get_def arl_get'_def Array.nth'_def
by (intro ext) auto
lemma arl_get_hnr_u[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure A›
shows ‹(uncurry arl_get_u, uncurry (RETURN ∘∘ op_list_get))
∈ [pre_list_get]⇩a (arl_assn A)⇧k *⇩a uint32_nat_assn⇧k → A›
proof -
obtain A' where
A: ‹pure A' = A›
using assms pure_the_pure by auto
then have A': ‹the_pure A = A'›
by auto
have [simp]: ‹the_pure (λa c. ↑ ((c, a) ∈ A')) = A'›
unfolding pure_def[symmetric] by auto
show ?thesis
by sepref_to_hoare
(sep_auto simp: uint32_nat_rel_def br_def ex_assn_up_eq2 array_assn_def is_array_def
hr_comp_def list_rel_pres_length list_rel_update param_nth arl_assn_def
A' A[symmetric] pure_def arl_get_u_def Array.nth'_def arl_get'_def
nat_of_uint32_code[symmetric])
qed
definition nth_rll_nu where
‹nth_rll_nu = nth_rll›
definition nth_raa_u' where
‹nth_raa_u' xs x L = nth_raa xs x (nat_of_uint32 L)›
lemma nth_raa_u'_uint_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_raa_u', uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arlO_assn (array_assn R))⇧k *⇩a nat_assn⇧k *⇩a uint32_nat_assn⇧k → R›
unfolding nth_raa_u_def
supply nth_aa_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare (sep_auto simp: uint32_nat_rel_def br_def nth_raa_u'_def)
lemma nth_nat_of_uint32_nth': ‹Array.nth x (nat_of_uint32 L) = Array.nth' x (integer_of_uint32 L)›
by (auto simp: Array.nth'_def nat_of_uint32_code)
lemma nth_aa_u_code[code]:
‹nth_aa_u x L L' = nth_u_code x L ⤜ (λx. arl_get x L' ⤜ return)›
unfolding nth_aa_u_def nth_aa_def arl_get_u_def[symmetric] Array.nth'_def[symmetric]
nth_nat_of_uint32_nth' nth_u_code_def[symmetric] ..
definition nth_aa_i64_u32 where
‹nth_aa_i64_u32 xs x L = nth_aa xs (nat_of_uint64 x) (nat_of_uint32 L)›
lemma nth_aa_i64_u32_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_aa_i64_u32, uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arrayO_assn (arl_assn R))⇧k *⇩a uint64_nat_assn⇧k *⇩a uint32_nat_assn⇧k → R›
unfolding nth_aa_i64_u32_def
supply nth_aa_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare
(sep_auto simp: uint32_nat_rel_def br_def nth_raa_u'_def uint64_nat_rel_def
length_rll_def length_ll_def nth_rll_def nth_ll_def)
definition nth_aa_i64_u64 where
‹nth_aa_i64_u64 xs x L = nth_aa xs (nat_of_uint64 x) (nat_of_uint64 L)›
lemma nth_aa_i64_u64_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_aa_i64_u64, uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arrayO_assn (arl_assn R))⇧k *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
unfolding nth_aa_i64_u64_def
supply nth_aa_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare
(sep_auto simp: br_def nth_raa_u'_def uint64_nat_rel_def
length_rll_def length_ll_def nth_rll_def nth_ll_def)
definition nth_aa_i32_u64 where
‹nth_aa_i32_u64 xs x L = nth_aa xs (nat_of_uint32 x) (nat_of_uint64 L)›
lemma nth_aa_i32_u64_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_aa_i32_u64, uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arrayO_assn (arl_assn R))⇧k *⇩a uint32_nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
unfolding nth_aa_i32_u64_def
supply nth_aa_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare
(sep_auto simp: uint32_nat_rel_def br_def nth_raa_u'_def uint64_nat_rel_def
length_rll_def length_ll_def nth_rll_def nth_ll_def)
paragraph ‹64-bit unsigned integers›
definition nth_u64 where
‹nth_u64 xs n = nth xs (nat_of_uint64 n)›
definition nth_u64_code where
‹nth_u64_code xs n = Array.nth' xs (integer_of_uint64 n)›
lemma nth_u64_hnr[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure A›
shows ‹(uncurry nth_u64_code, uncurry (RETURN oo nth_u64)) ∈
[λ(xs, n). nat_of_uint64 n < length xs]⇩a (array_assn A)⇧k *⇩a uint64_assn⇧k → A›
proof -
obtain A' where
A: ‹pure A' = A›
using assms pure_the_pure by auto
then have A': ‹the_pure A = A'›
by auto
have [simp]: ‹the_pure (λa c. ↑ ((c, a) ∈ A')) = A'›
unfolding pure_def[symmetric] by auto
show ?thesis
by sepref_to_hoare
(sep_auto simp: array_assn_def is_array_def
hr_comp_def list_rel_pres_length list_rel_update param_nth A' A[symmetric] ent_refl_true
list_rel_eq_listrel listrel_iff_nth pure_def nth_u64_code_def Array.nth'_def
nat_of_uint64_code nth_u64_def)
qed
lemma array_get_hnr_u64[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure A›
shows ‹(uncurry nth_u64_code,
uncurry (RETURN ∘∘ op_list_get)) ∈ [pre_list_get]⇩a (array_assn A)⇧k *⇩a uint64_nat_assn⇧k → A›
proof -
obtain A' where
A: ‹pure A' = A›
using assms pure_the_pure by auto
then have A': ‹the_pure A = A'›
by auto
have [simp]: ‹the_pure (λa c. ↑ ((c, a) ∈ A')) = A'›
unfolding pure_def[symmetric] by auto
show ?thesis
by sepref_to_hoare
(sep_auto simp: uint64_nat_rel_def br_def ex_assn_up_eq2 array_assn_def is_array_def
hr_comp_def list_rel_pres_length list_rel_update param_nth A' A[symmetric] ent_refl_true
list_rel_eq_listrel listrel_iff_nth pure_def nth_u64_code_def Array.nth'_def
nat_of_uint64_code)
qed
subsubsection ‹Setters›
paragraph ‹32-bits›
definition heap_array_set'_u where
‹heap_array_set'_u a i x = Array.upd' a (integer_of_uint32 i) x›
definition heap_array_set_u where
‹heap_array_set_u a i x = heap_array_set'_u a i x ⪢ return a›
lemma array_set_hnr_u[sepref_fr_rules]:
‹CONSTRAINT is_pure A ⟹
(uncurry2 heap_array_set_u, uncurry2 (RETURN ∘∘∘ op_list_set)) ∈
[pre_list_set]⇩a (array_assn A)⇧d *⇩a uint32_nat_assn⇧k *⇩a A⇧k → array_assn A›
by sepref_to_hoare
(sep_auto simp: uint32_nat_rel_def br_def ex_assn_up_eq2 array_assn_def is_array_def
hr_comp_def list_rel_pres_length list_rel_update heap_array_set'_u_def
heap_array_set_u_def Array.upd'_def
nat_of_uint32_code[symmetric])
definition update_aa_u where
‹update_aa_u xs i j = update_aa xs (nat_of_uint32 i) j›
lemma Array_upd_upd': ‹Array.upd i x a = Array.upd' a (of_nat i) x ⪢ return a›
by (auto simp: Array.upd'_def upd_return)
definition Array_upd_u where
‹Array_upd_u i x a = Array.upd (nat_of_uint32 i) x a›
lemma Array_upd_u_code[code]: ‹Array_upd_u i x a = heap_array_set'_u a i x ⪢ return a›
unfolding Array_upd_u_def heap_array_set'_u_def
Array.upd'_def
by (auto simp: nat_of_uint32_code upd_return)
lemma update_aa_u_code[code]:
‹update_aa_u a i j y = do {
x ← nth_u_code a i;
a' ← arl_set x j y;
Array_upd_u i a' a
}›
unfolding update_aa_u_def update_aa_def nth_nat_of_uint32_nth' nth_nat_of_uint32_nth'
arl_get_u_def[symmetric] nth_u_code_def[symmetric]
heap_array_set'_u_def[symmetric] Array_upd_u_def[symmetric]
by auto
definition arl_set'_u where
‹arl_set'_u a i x = arl_set a (nat_of_uint32 i) x›
definition arl_set_u :: ‹'a::heap array_list ⇒ uint32 ⇒ 'a ⇒ 'a array_list Heap›where
‹arl_set_u a i x = arl_set'_u a i x›
lemma arl_set_hnr_u[sepref_fr_rules]:
‹CONSTRAINT is_pure A ⟹
(uncurry2 arl_set_u, uncurry2 (RETURN ∘∘∘ op_list_set)) ∈
[pre_list_set]⇩a (arl_assn A)⇧d *⇩a uint32_nat_assn⇧k *⇩a A⇧k → arl_assn A›
by sepref_to_hoare
(sep_auto simp: uint32_nat_rel_def br_def ex_assn_up_eq2 array_assn_def is_array_def
hr_comp_def list_rel_pres_length list_rel_update heap_array_set'_u_def
heap_array_set_u_def Array.upd'_def arl_set_u_def arl_set'_u_def arl_assn_def
nat_of_uint32_code[symmetric])
paragraph ‹64-bits›
definition heap_array_set'_u64 where
‹heap_array_set'_u64 a i x = Array.upd' a (integer_of_uint64 i) x›
definition heap_array_set_u64 where
‹heap_array_set_u64 a i x = heap_array_set'_u64 a i x ⪢ return a›
lemma array_set_hnr_u64[sepref_fr_rules]:
‹CONSTRAINT is_pure A ⟹
(uncurry2 heap_array_set_u64, uncurry2 (RETURN ∘∘∘ op_list_set)) ∈
[pre_list_set]⇩a (array_assn A)⇧d *⇩a uint64_nat_assn⇧k *⇩a A⇧k → array_assn A›
by sepref_to_hoare
(sep_auto simp: uint64_nat_rel_def br_def ex_assn_up_eq2 array_assn_def is_array_def
hr_comp_def list_rel_pres_length list_rel_update heap_array_set'_u64_def
heap_array_set_u64_def Array.upd'_def
nat_of_uint64_code[symmetric])
definition arl_set'_u64 where
‹arl_set'_u64 a i x = arl_set a (nat_of_uint64 i) x›
definition arl_set_u64 :: ‹'a::heap array_list ⇒ uint64 ⇒ 'a ⇒ 'a array_list Heap›where
‹arl_set_u64 a i x = arl_set'_u64 a i x›
lemma arl_set_hnr_u64[sepref_fr_rules]:
‹CONSTRAINT is_pure A ⟹
(uncurry2 arl_set_u64, uncurry2 (RETURN ∘∘∘ op_list_set)) ∈
[pre_list_set]⇩a (arl_assn A)⇧d *⇩a uint64_nat_assn⇧k *⇩a A⇧k → arl_assn A›
by sepref_to_hoare
(sep_auto simp: uint64_nat_rel_def br_def ex_assn_up_eq2 array_assn_def is_array_def
hr_comp_def list_rel_pres_length list_rel_update heap_array_set'_u_def
heap_array_set_u_def Array.upd'_def arl_set_u64_def arl_set'_u64_def arl_assn_def
nat_of_uint64_code[symmetric])
lemma nth_nat_of_uint64_nth': ‹Array.nth x (nat_of_uint64 L) = Array.nth' x (integer_of_uint64 L)›
by (auto simp: Array.nth'_def nat_of_uint64_code)
definition nth_raa_i_u64 where
‹nth_raa_i_u64 x L L' = nth_raa x L (nat_of_uint64 L')›
lemma nth_raa_i_uint64_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_raa_i_u64, uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arlO_assn (array_assn R))⇧k *⇩a nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
unfolding nth_raa_i_u64_def
supply nth_aa_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def)
definition arl_get_u64 :: "'a::heap array_list ⇒ uint64 ⇒ 'a Heap" where
"arl_get_u64 ≡ λa i. arl_get' a (integer_of_uint64 i)"
lemma arl_get_hnr_u64[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure A›
shows ‹(uncurry arl_get_u64, uncurry (RETURN ∘∘ op_list_get))
∈ [pre_list_get]⇩a (arl_assn A)⇧k *⇩a uint64_nat_assn⇧k → A›
proof -
obtain A' where
A: ‹pure A' = A›
using assms pure_the_pure by auto
then have A': ‹the_pure A = A'›
by auto
have [simp]: ‹the_pure (λa c. ↑ ((c, a) ∈ A')) = A'›
unfolding pure_def[symmetric] by auto
show ?thesis
by sepref_to_hoare
(sep_auto simp: uint64_nat_rel_def br_def ex_assn_up_eq2 array_assn_def is_array_def
hr_comp_def list_rel_pres_length list_rel_update param_nth arl_assn_def
A' A[symmetric] pure_def arl_get_u64_def Array.nth'_def arl_get'_def
nat_of_uint64_code[symmetric])
qed
definition nth_raa_u64' where
‹nth_raa_u64' xs x L = nth_raa xs x (nat_of_uint64 L)›
lemma nth_raa_u64'_uint_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_raa_u64', uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arlO_assn (array_assn R))⇧k *⇩a nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
supply nth_aa_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def nth_raa_u64'_def)
definition nth_raa_u64 where
‹nth_raa_u64 x L = nth_raa x (nat_of_uint64 L)›
lemma nth_raa_uint64_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_raa_u64, uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint64_nat_assn⇧k *⇩a nat_assn⇧k → R›
unfolding nth_raa_u64_def
supply nth_aa_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def)
definition nth_raa_u64_u64 where
‹nth_raa_u64_u64 x L L' = nth_raa x (nat_of_uint64 L) (nat_of_uint64 L')›
lemma nth_raa_uint64_uint64_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_raa_u64_u64, uncurry2 (RETURN ∘∘∘ nth_rll)) ∈
[λ((l,i),j). i < length l ∧ j < length_rll l i]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
unfolding nth_raa_u64_u64_def
supply nth_aa_hnr[to_hnr, sep_heap_rules]
using assms
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def)
lemma heap_array_set_u64_upd:
‹heap_array_set_u64 x j xi = Array.upd (nat_of_uint64 j) xi x ⤜ (λxa. return x) ›
by (auto simp: heap_array_set_u64_def heap_array_set'_u64_def
Array.upd'_def nat_of_uint64_code[symmetric])
subsubsection ‹Append (32 bit integers only)›
definition append_el_aa_u' :: "('a::{default,heap} array_list) array ⇒
uint32 ⇒ 'a ⇒ ('a array_list) array Heap"where
"append_el_aa_u' ≡ λa i x.
Array.nth' a (integer_of_uint32 i) ⤜
(λj. arl_append j x ⤜
(λa'. Array.upd' a (integer_of_uint32 i) a' ⤜ (λ_. return a)))"
lemma append_el_aa_append_el_aa_u':
‹append_el_aa xs (nat_of_uint32 i) j = append_el_aa_u' xs i j›
unfolding append_el_aa_def append_el_aa_u'_def Array.nth'_def nat_of_uint32_code Array.upd'_def
by (auto simp add: upd'_def upd_return max_def)
lemma append_aa_hnr_u:
fixes R :: ‹'a ⇒ 'b :: {heap, default} ⇒ assn›
assumes p: ‹is_pure R›
shows
‹(uncurry2 (λxs i. append_el_aa xs (nat_of_uint32 i)), uncurry2 (RETURN ∘∘∘ (λxs i. append_ll xs (nat_of_uint32 i)))) ∈
[λ((l,i),x). nat_of_uint32 i < length l]⇩a (arrayO_assn (arl_assn R))⇧d *⇩a uint32_assn⇧k *⇩a R⇧k → (arrayO_assn (arl_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 (arl_assn R) a ai * R x r * true * ↑ (x = a ! ba ! b)) =
(arrayO_assn (arl_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: append_el_aa_def uint32_nat_rel_def br_def)
apply (simp add: arrayO_except_assn_def)
apply (rule sep_auto_is_stupid[OF p])
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 ba› 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 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›)[2]
apply (auto simp: star_aci)
done
qed
lemma append_el_aa_hnr'[sepref_fr_rules]:
shows ‹(uncurry2 append_el_aa_u', uncurry2 (RETURN ooo append_ll))
∈ [λ((W,L), j). L < length W]⇩a
(arrayO_assn (arl_assn nat_assn))⇧d *⇩a uint32_nat_assn⇧k *⇩a nat_assn⇧k → (arrayO_assn (arl_assn nat_assn))›
(is ‹?a ∈ [?pre]⇩a ?init → ?post›)
using append_aa_hnr_u[of nat_assn, simplified] unfolding hfref_def uint32_nat_rel_def br_def pure_def
hn_refine_def append_el_aa_append_el_aa_u'
by auto
lemma append_el_aa_uint32_hnr'[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure R›
shows ‹(uncurry2 append_el_aa_u', uncurry2 (RETURN ooo append_ll))
∈ [λ((W,L), j). L < length W]⇩a
(arrayO_assn (arl_assn R))⇧d *⇩a uint32_nat_assn⇧k *⇩a R⇧k →
(arrayO_assn (arl_assn R))›
(is ‹?a ∈ [?pre]⇩a ?init → ?post›)
using append_aa_hnr_u[of R, simplified] assms
unfolding hfref_def uint32_nat_rel_def br_def pure_def
hn_refine_def append_el_aa_append_el_aa_u'
by auto
lemma append_el_aa_u'_code[code]:
"append_el_aa_u' = (λa i x. nth_u_code a i ⤜
(λj. arl_append j x ⤜
(λa'. heap_array_set'_u a i a' ⤜ (λ_. return a))))"
unfolding append_el_aa_u'_def nth_u_code_def heap_array_set'_u_def
by auto
definition update_raa_u32 where
‹update_raa_u32 a i j y = do {
x ← arl_get_u a i;
Array.upd j y x ⤜ arl_set_u a i
}›
lemma update_raa_u32_rule[sep_heap_rules]:
assumes p: ‹is_pure R› and ‹bb < length a› and ‹ba < length_rll a bb› and
‹(bb', bb) ∈ uint32_nat_rel›
shows ‹<R b bi * arlO_assn (array_assn R) a ai> update_raa_u32 ai bb' ba bi
<λr. R b bi * (∃⇩Ax. arlO_assn (array_assn R) x r * ↑ (x = update_rll a bb ba b))>⇩t›
using assms
apply (cases ai)
apply (sep_auto simp add: update_raa_u32_def update_rll_def p)
apply (sep_auto simp add: update_raa_u32_def arlO_assn_except_def array_assn_def hr_comp_def
arl_assn_def arl_set_u_def arl_set'_u_def)
apply (solves ‹simp add: br_def uint32_nat_rel_def›)
apply (rule_tac x=‹a[bb := (a ! bb)[ba := b]]› in ent_ex_postI)
apply (subst_tac i=bb in arlO_assn_except_array0_index[symmetric])
apply (auto simp add: br_def uint32_nat_rel_def)[]
apply (auto simp add: update_raa_def arlO_assn_except_def array_assn_def is_array_def hr_comp_def)
apply (rule_tac x=‹p[bb := xa]› in ent_ex_postI)
apply (rule_tac x=‹baa› 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›)
by (sep_auto simp: arl_assn_def uint32_nat_rel_def br_def)
lemma update_raa_u32_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 update_raa_u32, uncurry3 (RETURN oooo update_rll)) ∈
[λ(((l,i), j), x). i < length l ∧ j < length_rll l i]⇩a (arlO_assn (array_assn R))⇧d *⇩a uint32_nat_assn⇧k *⇩a nat_assn⇧k *⇩a R⇧k → (arlO_assn (array_assn R))›
by sepref_to_hoare (sep_auto simp: assms)
lemma update_aa_u_rule[sep_heap_rules]:
assumes p: ‹is_pure R› and ‹bb < length a› and ‹ba < length_ll a bb› and ‹(bb', bb) ∈ uint32_nat_rel›
shows ‹<R b bi * arrayO_assn (arl_assn R) a ai> update_aa_u ai bb' ba bi
<λr. R b bi * (∃⇩Ax. arrayO_assn (arl_assn R) x r * ↑ (x = update_ll a bb ba b))>⇩t›
solve_direct
using assms
by (sep_auto simp add: update_aa_u_def update_ll_def p uint32_nat_rel_def br_def)
lemma update_aa_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 update_aa_u, uncurry3 (RETURN oooo update_ll)) ∈
[λ(((l,i), j), x). i < length l ∧ j < length_ll l i]⇩a
(arrayO_assn (arl_assn R))⇧d *⇩a uint32_nat_assn⇧k *⇩a nat_assn⇧k *⇩a R⇧k → (arrayO_assn (arl_assn R))›
by sepref_to_hoare (sep_auto simp: assms)
subsubsection ‹Length›
paragraph ‹32-bits›
definition (in -)length_u_code where
‹length_u_code C = do { n ← Array.len C; return (uint32_of_nat n)}›
lemma (in -)length_u_hnr[sepref_fr_rules]:
‹(length_u_code, RETURN o length_uint32_nat) ∈ [λC. length C ≤ uint32_max]⇩a (array_assn R)⇧k → uint32_nat_assn›
supply length_rule[sep_heap_rules]
by sepref_to_hoare
(sep_auto simp: length_u_code_def array_assn_def hr_comp_def is_array_def
uint32_nat_rel_def list_rel_imp_same_length br_def nat_of_uint32_uint32_of_nat_id)
definition length_arl_u_code :: ‹('a::heap) array_list ⇒ uint32 Heap› where
‹length_arl_u_code xs = do {
n ← arl_length xs;
return (uint32_of_nat n)}›
lemma length_arl_u_hnr[sepref_fr_rules]:
‹(length_arl_u_code, RETURN o length_uint32_nat) ∈
[λxs. length xs ≤ uint32_max]⇩a (arl_assn R)⇧k → uint32_nat_assn›
by sepref_to_hoare
(sep_auto simp: length_u_code_def nat_of_uint32_uint32_of_nat_id
length_arl_u_code_def arl_assn_def
arl_length_def hr_comp_def is_array_list_def list_rel_pres_length[symmetric]
uint32_nat_rel_def br_def)
paragraph ‹64-bits›
definition (in -)length_u64_code where
‹length_u64_code C = do { n ← Array.len C; return (uint64_of_nat n)}›
lemma (in -)length_u64_hnr[sepref_fr_rules]:
‹(length_u64_code, RETURN o length_uint64_nat)
∈ [λC. length C ≤ uint64_max]⇩a (array_assn R)⇧k → uint64_nat_assn›
supply length_rule[sep_heap_rules]
by sepref_to_hoare
(sep_auto simp: length_u_code_def array_assn_def hr_comp_def is_array_def length_u64_code_def
uint64_nat_rel_def list_rel_imp_same_length br_def nat_of_uint64_uint64_of_nat_id)
subsubsection ‹Length for arrays in arrays›
paragraph ‹32-bits›
definition (in -)length_aa_u :: ‹('a::heap array_list) array ⇒ uint32 ⇒ nat Heap› where
‹length_aa_u xs i = length_aa xs (nat_of_uint32 i)›
lemma length_aa_u_code[code]:
‹length_aa_u xs i = nth_u_code xs i ⤜ arl_length›
unfolding length_aa_u_def length_aa_def nth_u_def[symmetric] nth_u_code_def
Array.nth'_def
by (auto simp: nat_of_uint32_code)
lemma length_aa_u_hnr[sepref_fr_rules]: ‹(uncurry length_aa_u, uncurry (RETURN ∘∘ length_ll)) ∈
[λ(xs, i). i < length xs]⇩a (arrayO_assn (arl_assn R))⇧k *⇩a uint32_nat_assn⇧k → nat_assn›
by sepref_to_hoare (sep_auto simp: uint32_nat_rel_def length_aa_u_def br_def)
definition length_raa_u :: ‹'a::heap arrayO_raa ⇒ nat ⇒ uint32 Heap› where
‹length_raa_u xs i = do {
x ← arl_get xs i;
length_u_code x}›
lemma length_raa_u_alt_def: ‹length_raa_u xs i = do {
n ← length_raa xs i;
return (uint32_of_nat n)}›
unfolding length_raa_u_def length_raa_def length_u_code_def
by auto
definition length_rll_n_uint32 where
[simp]: ‹length_rll_n_uint32 = length_rll›
lemma length_raa_rule[sep_heap_rules]:
‹b < length xs ⟹ <arlO_assn (array_assn R) xs a> length_raa_u a b
<λr. arlO_assn (array_assn R) xs a * ↑ (r = uint32_of_nat (length_rll xs b))>⇩t›
unfolding length_raa_u_alt_def length_u_code_def
by sep_auto
lemma length_raa_u_hnr[sepref_fr_rules]:
shows ‹(uncurry length_raa_u, uncurry (RETURN ∘∘ length_rll_n_uint32)) ∈
[λ(xs, i). i < length xs ∧ length (xs ! i) ≤ uint32_max]⇩a
(arlO_assn (array_assn R))⇧k *⇩a nat_assn⇧k → uint32_nat_assn›
by sepref_to_hoare (sep_auto simp: uint32_nat_rel_def br_def length_rll_def
nat_of_uint32_uint32_of_nat_id)+
text ‹TODO: proper fix to avoid the conversion to uint32›
definition length_aa_u_code :: ‹('a::heap array) array_list ⇒ nat ⇒ uint32 Heap› where
‹length_aa_u_code xs i = do {
n ← length_raa xs i;
return (uint32_of_nat n)}›
paragraph ‹64-bits›
definition (in -)length_aa_u64 :: ‹('a::heap array_list) array ⇒ uint64 ⇒ nat Heap› where
‹length_aa_u64 xs i = length_aa xs (nat_of_uint64 i)›
lemma length_aa_u64_code[code]:
‹length_aa_u64 xs i = nth_u64_code xs i ⤜ arl_length›
unfolding length_aa_u64_def length_aa_def nth_u64_def[symmetric] nth_u64_code_def
Array.nth'_def
by (auto simp: nat_of_uint64_code)
lemma length_aa_u64_hnr[sepref_fr_rules]: ‹(uncurry length_aa_u64, uncurry (RETURN ∘∘ length_ll)) ∈
[λ(xs, i). i < length xs]⇩a (arrayO_assn (arl_assn R))⇧k *⇩a uint64_nat_assn⇧k → nat_assn›
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def length_aa_u64_def br_def)
definition length_raa_u64 :: ‹'a::heap arrayO_raa ⇒ nat ⇒ uint64 Heap› where
‹length_raa_u64 xs i = do {
x ← arl_get xs i;
length_u64_code x}›
lemma length_raa_u64_alt_def: ‹length_raa_u64 xs i = do {
n ← length_raa xs i;
return (uint64_of_nat n)}›
unfolding length_raa_u64_def length_raa_def length_u64_code_def
by auto
definition length_rll_n_uint64 where
[simp]: ‹length_rll_n_uint64 = length_rll›
lemma length_raa_u64_hnr[sepref_fr_rules]:
shows ‹(uncurry length_raa_u64, uncurry (RETURN ∘∘ length_rll_n_uint64)) ∈
[λ(xs, i). i < length xs ∧ length (xs ! i) ≤ uint64_max]⇩a
(arlO_assn (array_assn R))⇧k *⇩a nat_assn⇧k → uint64_nat_assn›
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def length_rll_def
nat_of_uint64_uint64_of_nat_id length_raa_u64_alt_def)+
subsubsection ‹Delete at index›
definition delete_index_and_swap_aa where
‹delete_index_and_swap_aa xs i j = do {
x ← last_aa xs i;
xs ← update_aa xs i j x;
set_butlast_aa xs i
}›
lemma delete_index_and_swap_aa_ll_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry2 delete_index_and_swap_aa, uncurry2 (RETURN ooo delete_index_and_swap_ll))
∈ [λ((l,i), j). i < length l ∧ j < length_ll l i]⇩a (arrayO_assn (arl_assn R))⇧d *⇩a nat_assn⇧k *⇩a nat_assn⇧k
→ (arrayO_assn (arl_assn R))›
using assms unfolding delete_index_and_swap_aa_def
by sepref_to_hoare (sep_auto dest: le_length_ll_nemptyD
simp: delete_index_and_swap_ll_def update_ll_def last_ll_def set_butlast_ll_def
length_ll_def[symmetric])
subsubsection ‹Last (arrays of arrays)›
definition last_aa_u where
‹last_aa_u xs i = last_aa xs (nat_of_uint32 i)›
lemma last_aa_u_code[code]:
‹last_aa_u xs i = nth_u_code xs i ⤜ arl_last›
unfolding last_aa_u_def last_aa_def nth_nat_of_uint32_nth' nth_nat_of_uint32_nth'
arl_get_u_def[symmetric] nth_u_code_def[symmetric] ..
lemma length_delete_index_and_swap_ll[simp]:
‹length (delete_index_and_swap_ll s i j) = length s›
by (auto simp: delete_index_and_swap_ll_def)
definition set_butlast_aa_u where
‹set_butlast_aa_u xs i = set_butlast_aa xs (nat_of_uint32 i)›
lemma set_butlast_aa_u_code[code]:
‹set_butlast_aa_u a i = do {
x ← nth_u_code a i;
a' ← arl_butlast x;
Array_upd_u i a' a
}›
unfolding set_butlast_aa_u_def set_butlast_aa_def
nth_u_code_def Array_upd_u_def
by (auto simp: Array.nth'_def nat_of_uint32_code)
definition delete_index_and_swap_aa_u where
‹delete_index_and_swap_aa_u xs i = delete_index_and_swap_aa xs (nat_of_uint32 i)›
lemma delete_index_and_swap_aa_u_code[code]:
‹delete_index_and_swap_aa_u xs i j = do {
x ← last_aa_u xs i;
xs ← update_aa_u xs i j x;
set_butlast_aa_u xs i
}›
unfolding delete_index_and_swap_aa_u_def delete_index_and_swap_aa_def
last_aa_u_def update_aa_u_def set_butlast_aa_u_def
by auto
lemma delete_index_and_swap_aa_ll_hnr_u[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry2 delete_index_and_swap_aa_u, uncurry2 (RETURN ooo delete_index_and_swap_ll))
∈ [λ((l,i), j). i < length l ∧ j < length_ll l i]⇩a (arrayO_assn (arl_assn R))⇧d *⇩a uint32_nat_assn⇧k *⇩a nat_assn⇧k
→ (arrayO_assn (arl_assn R))›
using assms unfolding delete_index_and_swap_aa_def delete_index_and_swap_aa_u_def
by sepref_to_hoare (sep_auto dest: le_length_ll_nemptyD
simp: delete_index_and_swap_ll_def update_ll_def last_ll_def set_butlast_ll_def
length_ll_def[symmetric] uint32_nat_rel_def br_def)
subsubsection ‹Swap›
definition swap_u_code :: "'a ::heap array ⇒ uint32 ⇒ uint32 ⇒ 'a array Heap" where
‹swap_u_code xs i j = do {
ki ← nth_u_code xs i;
kj ← nth_u_code xs j;
xs ← heap_array_set_u xs i kj;
xs ← heap_array_set_u xs j ki;
return xs
}›
lemma op_list_swap_u_hnr[sepref_fr_rules]:
assumes p: ‹CONSTRAINT is_pure R›
shows ‹(uncurry2 swap_u_code, uncurry2 (RETURN ooo op_list_swap)) ∈
[λ((xs, i), j). i < length xs ∧ j < length xs]⇩a
(array_assn R)⇧d *⇩a uint32_nat_assn⇧k *⇩a uint32_nat_assn⇧k → array_assn R›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
show ?thesis
by (sepref_to_hoare)
(sep_auto simp: swap_u_code_def swap_def nth_u_code_def is_array_def
array_assn_def hr_comp_def nth_nat_of_uint32_nth'[symmetric]
list_rel_imp_same_length uint32_nat_rel_def br_def
heap_array_set_u_def heap_array_set'_u_def Array.upd'_def
nat_of_uint32_code[symmetric] R IICF_List.swap_def[symmetric] IICF_List.swap_param
intro!: list_rel_update[of _ _ R true _ _ ‹(_, {})›, unfolded R] param_nth)
qed
definition swap_u64_code :: "'a ::heap array ⇒ uint64 ⇒ uint64 ⇒ 'a array Heap" where
‹swap_u64_code xs i j = do {
ki ← nth_u64_code xs i;
kj ← nth_u64_code xs j;
xs ← heap_array_set_u64 xs i kj;
xs ← heap_array_set_u64 xs j ki;
return xs
}›
lemma op_list_swap_u64_hnr[sepref_fr_rules]:
assumes p: ‹CONSTRAINT is_pure R›
shows ‹(uncurry2 swap_u64_code, uncurry2 (RETURN ooo op_list_swap)) ∈
[λ((xs, i), j). i < length xs ∧ j < length xs]⇩a
(array_assn R)⇧d *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k → array_assn R›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
show ?thesis
by (sepref_to_hoare)
(sep_auto simp: swap_u64_code_def swap_def nth_u64_code_def is_array_def
array_assn_def hr_comp_def nth_nat_of_uint64_nth'[symmetric]
list_rel_imp_same_length uint64_nat_rel_def br_def
heap_array_set_u64_def heap_array_set'_u64_def Array.upd'_def
nat_of_uint64_code[symmetric] R IICF_List.swap_def[symmetric] IICF_List.swap_param
intro!: list_rel_update[of _ _ R true _ _ ‹(_, {})›, unfolded R] param_nth)
qed
definition swap_aa_u64 :: "('a::{heap,default}) arrayO_raa ⇒ nat ⇒ uint64 ⇒ uint64 ⇒ 'a arrayO_raa Heap" where
‹swap_aa_u64 xs k i j = do {
xi ← arl_get xs k;
xj ← swap_u64_code xi i j;
xs ← arl_set xs k xj;
return xs
}›
lemma swap_aa_u64_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 swap_aa_u64, uncurry3 (RETURN oooo swap_ll)) ∈
[λ(((xs, k), i), j). k < length xs ∧ i < length_rll xs k ∧ j < length_rll xs k]⇩a
(arlO_assn (array_assn R))⇧d *⇩a nat_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k →
(arlO_assn (array_assn R))›
proof -
note update_raa_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
have H: ‹<is_array_list p (aa, bc) *
heap_list_all_nth (array_assn (λa c. ↑ ((c, a) ∈ R'))) (remove1 bb [0..<length p]) a p *
array_assn (λa c. ↑ ((c, a) ∈ R')) (a ! bb) (p ! bb)>
Array.nth (p ! bb) (nat_of_integer (integer_of_uint64 bia))
<λr. ∃⇩A p'. is_array_list p' (aa, bc) * ↑ (bb < length p' ∧ p' ! bb = p ! bb ∧ length a = length p') *
heap_list_all_nth (array_assn (λa c. ↑ ((c, a) ∈ R'))) (remove1 bb [0..<length p']) a p' *
array_assn (λa c. ↑ ((c, a) ∈ R')) (a ! bb) (p' ! bb) *
R (a ! bb ! (nat_of_uint64 bia)) r >›
if
‹is_pure (λa c. ↑ ((c, a) ∈ R'))› and
‹bb < length p› and
‹nat_of_uint64 bia < length (a ! bb)› and
‹nat_of_uint64 bi < length (a ! bb)› and
‹length a = length p›
for bi :: ‹uint64› and bia :: ‹uint64› and bb :: ‹nat› and a :: ‹'a list list› and
aa :: ‹'b array array› and bc :: ‹nat› and p :: ‹'b array list›
using that
by (sep_auto simp: array_assn_def hr_comp_def is_array_def nat_of_uint64_code[symmetric]
list_rel_imp_same_length RR' pure_def param_nth)
have H': ‹is_array_list p' (aa, ba) * p' ! bb ↦⇩a b [nat_of_uint64 bia := b ! nat_of_uint64 bi,
nat_of_uint64 bi := xa] *
heap_list_all_nth (λa b. ∃⇩Aba. b ↦⇩a ba * ↑ ((ba, a) ∈ ⟨R'⟩list_rel))
(remove1 bb [0..<length p']) a p' * R (a ! bb ! nat_of_uint64 bia) xa ⟹⇩A
is_array_list p' (aa, ba) *
heap_list_all
(λa c. ∃⇩Ab. c ↦⇩a b * ↑ ((b, a) ∈ ⟨R'⟩list_rel))
(a[bb := (a ! bb) [nat_of_uint64 bia := a ! bb ! nat_of_uint64 bi,
nat_of_uint64 bi := a ! bb ! nat_of_uint64 bia]])
p' * true›
if
‹is_pure (λa c. ↑ ((c, a) ∈ R'))› and
le: ‹nat_of_uint64 bia < length (a ! bb)› and
le': ‹nat_of_uint64 bi < length (a ! bb)› and
‹bb < length p'› and
‹length a = length p'› and
a: ‹(b, a ! bb) ∈ ⟨R'⟩list_rel›
for bi :: ‹uint64› and bia :: ‹uint64› and bb :: ‹nat› and a :: ‹'a list list› and
xa :: ‹'b› and p' :: ‹'b array list› and b :: ‹'b list› and aa :: ‹'b array array› and ba :: ‹nat›
proof -
have 1: ‹(b[nat_of_uint64 bia := b ! nat_of_uint64 bi, nat_of_uint64 bi := xa],
(a ! bb)[nat_of_uint64 bia := a ! bb ! nat_of_uint64 bi,
nat_of_uint64 bi := a ! bb ! nat_of_uint64 bia]) ∈ ⟨R'⟩list_rel›
if ‹(xa, a ! bb ! nat_of_uint64 bia) ∈ R'›
using that a le le'
unfolding list_rel_def list_all2_conv_all_nth
by auto
have 2: ‹heap_list_all_nth (λa b. ∃⇩Aba. b ↦⇩a ba * ↑ ((ba, a) ∈ ⟨R'⟩list_rel)) (remove1 bb [0..<length p']) a p' =
heap_list_all_nth (λa c. ∃⇩Ab. c ↦⇩a b * ↑ ((b, a) ∈ ⟨R'⟩list_rel)) (remove1 bb [0..<length p'])
(a[bb := (a ! bb)[nat_of_uint64 bia := a ! bb ! nat_of_uint64 bi, nat_of_uint64 bi := a ! bb ! nat_of_uint64 bia]]) p'›
by (rule heap_list_all_nth_cong) auto
show ?thesis using that
unfolding heap_list_all_heap_list_all_nth_eq
by (subst (2) heap_list_all_nth_remove1[of bb])
(sep_auto simp: heap_list_all_heap_list_all_nth_eq swap_def fr_refl RR'
pure_def 2[symmetric] intro!: 1)+
qed
show ?thesis
using assms unfolding R'[symmetric] unfolding RR'
apply sepref_to_hoare
apply (sep_auto simp: swap_aa_u64_def swap_ll_def arlO_assn_except_def length_rll_def
length_rll_update_rll nth_raa_i_u64_def uint64_nat_rel_def br_def
swap_def nth_rll_def list_update_swap swap_u64_code_def nth_u64_code_def Array.nth'_def
heap_array_set_u64_def heap_array_set'_u64_def arl_assn_def IICF_List.swap_def
Array.upd'_def)
apply (rule H; assumption)
apply (sep_auto simp: array_assn_def nat_of_uint64_code[symmetric] hr_comp_def is_array_def
list_rel_imp_same_length arlO_assn_def arl_assn_def hr_comp_def[abs_def])
apply (rule H'; assumption)
done
qed
definition arl_swap_u_code
:: "'a ::heap array_list ⇒ uint32 ⇒ uint32 ⇒ 'a array_list Heap"
where
‹arl_swap_u_code xs i j = do {
ki ← arl_get_u xs i;
kj ← arl_get_u xs j;
xs ← arl_set_u xs i kj;
xs ← arl_set_u xs j ki;
return xs
}›
lemma arl_op_list_swap_u_hnr[sepref_fr_rules]:
assumes p: ‹CONSTRAINT is_pure R›
shows ‹(uncurry2 arl_swap_u_code, uncurry2 (RETURN ooo op_list_swap)) ∈
[λ((xs, i), j). i < length xs ∧ j < length xs]⇩a
(arl_assn R)⇧d *⇩a uint32_nat_assn⇧k *⇩a uint32_nat_assn⇧k → arl_assn R›
proof -
obtain R' where R: ‹the_pure R = R'› and R': ‹R = pure R'›
using p by fastforce
show ?thesis
by (sepref_to_hoare)
(sep_auto simp: arl_swap_u_code_def swap_def nth_u_code_def is_array_def
array_assn_def hr_comp_def nth_nat_of_uint32_nth'[symmetric]
list_rel_imp_same_length uint32_nat_rel_def br_def arl_assn_def
heap_array_set_u_def heap_array_set'_u_def Array.upd'_def
arl_set'_u_def R R' IICF_List.swap_def[symmetric] IICF_List.swap_param
nat_of_uint32_code[symmetric] R arl_set_u_def arl_get'_def arl_get_u_def
intro!: list_rel_update[of _ _ R true _ _ ‹(_, {})›, unfolded R] param_nth)
qed
subsubsection ‹Take›
definition shorten_take_aa_u32 where
‹shorten_take_aa_u32 L j W = do {
(a, n) ← nth_u_code W L;
heap_array_set_u W L (a, j)
}›
lemma shorten_take_aa_u32_alt_def:
‹shorten_take_aa_u32 L j W = shorten_take_aa (nat_of_uint32 L) j W›
by (auto simp: shorten_take_aa_u32_def shorten_take_aa_def uint32_nat_rel_def br_def
Array.nth'_def heap_array_set_u_def heap_array_set'_u_def Array.upd'_def
nth_u_code_def nat_of_uint32_code[symmetric] upd_return)
lemma shorten_take_aa_u32_hnr[sepref_fr_rules]:
‹(uncurry2 shorten_take_aa_u32, uncurry2 (RETURN ooo shorten_take_ll)) ∈
[λ((L, j), W). j ≤ length (W ! L) ∧ L < length W]⇩a
uint32_nat_assn⇧k *⇩a nat_assn⇧k *⇩a (arrayO_assn (arl_assn R))⇧d → arrayO_assn (arl_assn R)›
unfolding shorten_take_aa_u32_alt_def shorten_take_ll_def nth_u_code_def uint32_nat_rel_def br_def
Array.nth'_def heap_array_set_u_def heap_array_set'_u_def Array.upd'_def shorten_take_aa_def
by sepref_to_hoare (sep_auto simp: nat_of_uint32_code[symmetric])
subsubsection ‹List of Lists›
paragraph ‹Getters›
definition nth_raa_i32 :: ‹'a::heap arrayO_raa ⇒ uint32 ⇒ nat ⇒ 'a Heap› where
‹nth_raa_i32 xs i j = do {
x ← arl_get_u xs i;
y ← Array.nth x j;
return y}›
lemma nth_raa_i32_hnr[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure R›
shows
‹(uncurry2 nth_raa_i32, uncurry2 (RETURN ooo nth_rll)) ∈
[λ((xs, i), j). i < length xs ∧ j < length (xs !i)]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint32_nat_assn⇧k *⇩a nat_assn⇧k → R›
proof -
have 1: ‹a * b * array_assn R x y = array_assn R x y * a * b› for a b c :: assn and x y
by (auto simp: ac_simps)
have 2: ‹a * arl_assn R x y * c = arl_assn R x y * a * c› for a c :: assn and x y and R
by (auto simp: ac_simps)
have [simp]: ‹R a b = ↑((b,a) ∈ the_pure R)› for a b
using assms by (metis CONSTRAINT_D pure_app_eq pure_the_pure)
show ?thesis
using assms
apply sepref_to_hoare
apply (sep_auto simp: nth_raa_i32_def arl_get_u_def
uint32_nat_rel_def br_def nat_of_uint32_code[symmetric]
arlO_assn_except_def 1 arl_get'_def
)
apply (sep_auto simp: array_assn_def hr_comp_def is_array_def list_rel_imp_same_length
param_nth nth_rll_def)
apply (sep_auto simp: arlO_assn_def 2 )
apply (subst mult.assoc)+
apply (rule fr_refl')
apply (subst heap_list_all_heap_list_all_nth_eq)
apply (subst_tac (2) i=‹nat_of_uint32 bia› in heap_list_all_nth_remove1)
apply (sep_auto simp: nth_rll_def is_array_def hr_comp_def)+
done
qed
definition nth_raa_i32_u64 :: ‹'a::heap arrayO_raa ⇒ uint32 ⇒ uint64 ⇒ 'a Heap› where
‹nth_raa_i32_u64 xs i j = do {
x ← arl_get_u xs i;
y ← nth_u64_code x j;
return y}›
lemma nth_raa_i32_u64_hnr[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure R›
shows
‹(uncurry2 nth_raa_i32_u64, uncurry2 (RETURN ooo nth_rll)) ∈
[λ((xs, i), j). i < length xs ∧ j < length (xs !i)]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint32_nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
proof -
have 1: ‹a * b * array_assn R x y = array_assn R x y * a * b› for a b c :: assn and x y
by (auto simp: ac_simps)
have 2: ‹a * arl_assn R x y * c = arl_assn R x y * a * c› for a c :: assn and x y and R
by (auto simp: ac_simps)
have [simp]: ‹R a b = ↑((b,a) ∈ the_pure R)› for a b
using assms by (metis CONSTRAINT_D pure_app_eq pure_the_pure)
show ?thesis
using assms
apply sepref_to_hoare
apply (sep_auto simp: nth_raa_i32_u64_def arl_get_u_def
uint32_nat_rel_def br_def nat_of_uint32_code[symmetric]
arlO_assn_except_def 1 arl_get'_def Array.nth'_def nth_u64_code_def
nat_of_uint64_code[symmetric] uint64_nat_rel_def)
apply (sep_auto simp: array_assn_def hr_comp_def is_array_def list_rel_imp_same_length
param_nth nth_rll_def)
apply (sep_auto simp: arlO_assn_def 2 )
apply (subst mult.assoc)+
apply (rule fr_refl')
apply (subst heap_list_all_heap_list_all_nth_eq)
apply (subst_tac (2) i=‹nat_of_uint32 bia› in heap_list_all_nth_remove1)
apply (sep_auto simp: nth_rll_def is_array_def hr_comp_def)+
done
qed
definition nth_raa_i32_u32 :: ‹'a::heap arrayO_raa ⇒ uint32 ⇒ uint32 ⇒ 'a Heap› where
‹nth_raa_i32_u32 xs i j = do {
x ← arl_get_u xs i;
y ← nth_u_code x j;
return y}›
lemma nth_raa_i32_u32_hnr[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure R›
shows
‹(uncurry2 nth_raa_i32_u32, uncurry2 (RETURN ooo nth_rll)) ∈
[λ((xs, i), j). i < length xs ∧ j < length (xs !i)]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint32_nat_assn⇧k *⇩a uint32_nat_assn⇧k → R›
proof -
have 1: ‹a * b * array_assn R x y = array_assn R x y * a * b› for a b c :: assn and x y
by (auto simp: ac_simps)
have 2: ‹a * arl_assn R x y * c = arl_assn R x y * a * c› for a c :: assn and x y and R
by (auto simp: ac_simps)
have [simp]: ‹R a b = ↑((b,a) ∈ the_pure R)› for a b
using assms by (metis CONSTRAINT_D pure_app_eq pure_the_pure)
show ?thesis
using assms
apply sepref_to_hoare
apply (sep_auto simp: nth_raa_i32_u32_def arl_get_u_def
uint32_nat_rel_def br_def nat_of_uint32_code[symmetric]
arlO_assn_except_def 1 arl_get'_def Array.nth'_def nth_u_code_def
nat_of_uint32_code[symmetric] uint32_nat_rel_def)
apply (sep_auto simp: array_assn_def hr_comp_def is_array_def list_rel_imp_same_length
param_nth nth_rll_def)
apply (sep_auto simp: arlO_assn_def 2 )
apply (subst mult.assoc)+
apply (rule fr_refl')
apply (subst heap_list_all_heap_list_all_nth_eq)
apply (subst_tac (2) i=‹nat_of_uint32 bia› in heap_list_all_nth_remove1)
apply (sep_auto simp: nth_rll_def is_array_def hr_comp_def)+
done
qed
definition nth_aa_i32_u32 where
‹nth_aa_i32_u32 x L L' = nth_aa x (nat_of_uint32 L) (nat_of_uint32 L')›
definition nth_aa_i32_u32' where
‹nth_aa_i32_u32' xs i j = do {
x ← nth_u_code xs i;
y ← arl_get_u x j;
return y}›
lemma nth_aa_i32_u32[code]:
‹nth_aa_i32_u32 x L L' = nth_aa_i32_u32' x L L'›
unfolding nth_aa_u_def nth_aa'_def nth_aa_def Array.nth'_def nat_of_uint32_code
nth_aa_i32_u32_def nth_aa_i32_u32'_def nth_u_code_def arl_get_u_def arl_get'_def
by (auto simp: nat_of_uint32_code[symmetric])
lemma nth_aa_i32_u32_hnr[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure R›
shows
‹(uncurry2 nth_aa_i32_u32, uncurry2 (RETURN ooo nth_rll)) ∈
[λ((x, L), L'). L < length x ∧ L' < length (x ! L)]⇩a
(arrayO_assn (arl_assn R))⇧k *⇩a uint32_nat_assn⇧k *⇩a uint32_nat_assn⇧k → R›
unfolding nth_aa_i32_u32_def
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›)
definition nth_raa_i64_u32 :: ‹'a::heap arrayO_raa ⇒ uint64 ⇒ uint32 ⇒ 'a Heap› where
‹nth_raa_i64_u32 xs i j = do {
x ← arl_get_u64 xs i;
y ← nth_u_code x j;
return y}›
lemma nth_raa_i64_u32_hnr[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure R›
shows
‹(uncurry2 nth_raa_i64_u32, uncurry2 (RETURN ooo nth_rll)) ∈
[λ((xs, i), j). i < length xs ∧ j < length (xs !i)]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint64_nat_assn⇧k *⇩a uint32_nat_assn⇧k → R›
proof -
have 1: ‹a * b * array_assn R x y = array_assn R x y * a * b› for a b c :: assn and x y
by (auto simp: ac_simps)
have 2: ‹a * arl_assn R x y * c = arl_assn R x y * a * c› for a c :: assn and x y and R
by (auto simp: ac_simps)
have [simp]: ‹R a b = ↑((b,a) ∈ the_pure R)› for a b
using assms by (metis CONSTRAINT_D pure_app_eq pure_the_pure)
show ?thesis
using assms
apply sepref_to_hoare
apply (sep_auto simp: nth_raa_i64_u32_def arl_get_u64_def
uint32_nat_rel_def br_def nat_of_uint32_code[symmetric]
arlO_assn_except_def 1 arl_get'_def Array.nth'_def nth_u64_code_def
nat_of_uint64_code[symmetric] uint64_nat_rel_def nth_u_code_def)
apply (sep_auto simp: array_assn_def hr_comp_def is_array_def list_rel_imp_same_length
param_nth nth_rll_def)
apply (sep_auto simp: arlO_assn_def 2)
apply (subst mult.assoc)+
apply (rule fr_refl')
apply (subst heap_list_all_heap_list_all_nth_eq)
apply (subst_tac (2) i=‹nat_of_uint64 bia› in heap_list_all_nth_remove1)
apply (sep_auto simp: nth_rll_def is_array_def hr_comp_def)+
done
qed
thm nth_aa_uint_hnr
find_theorems nth_aa_u
lemma nth_aa_hnr[sepref_fr_rules]:
assumes p: ‹is_pure R›
shows
‹(uncurry2 nth_aa, uncurry2 (RETURN ∘∘∘ nth_ll)) ∈
[λ((l,i),j). i < length l ∧ j < length_ll l i]⇩a
(arrayO_assn (arl_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 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
apply sepref_to_hoare
apply (subst (2) arrayO_except_assn_array0_index[symmetric])
apply (solves ‹auto›)[]
apply (sep_auto simp: nth_aa_def nth_ll_def length_ll_def)
apply (sep_auto simp: arrayO_except_assn_def arrayO_assn_def arl_assn_def hr_comp_def list_rel_def
list_all2_lengthD
star_aci(3) R R' pure_def H)
done
qed
definition nth_raa_i64_u64 :: ‹'a::heap arrayO_raa ⇒ uint64 ⇒ uint64 ⇒ 'a Heap› where
‹nth_raa_i64_u64 xs i j = do {
x ← arl_get_u64 xs i;
y ← nth_u64_code x j;
return y}›
lemma nth_raa_i64_u64_hnr[sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure R›
shows
‹(uncurry2 nth_raa_i64_u64, uncurry2 (RETURN ooo nth_rll)) ∈
[λ((xs, i), j). i < length xs ∧ j < length (xs !i)]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k → R›
proof -
have 1: ‹a * b * array_assn R x y = array_assn R x y * a * b› for a b c :: assn and x y
by (auto simp: ac_simps)
have 2: ‹a * arl_assn R x y * c = arl_assn R x y * a * c› for a c :: assn and x y and R
by (auto simp: ac_simps)
have [simp]: ‹R a b = ↑((b,a) ∈ the_pure R)› for a b
using assms by (metis CONSTRAINT_D pure_app_eq pure_the_pure)
show ?thesis
using assms
apply sepref_to_hoare
apply (sep_auto simp: nth_raa_i64_u64_def arl_get_u64_def
uint32_nat_rel_def br_def nat_of_uint32_code[symmetric]
arlO_assn_except_def 1 arl_get'_def Array.nth'_def nth_u64_code_def
nat_of_uint64_code[symmetric] uint64_nat_rel_def nth_u64_code_def)
apply (sep_auto simp: array_assn_def hr_comp_def is_array_def list_rel_imp_same_length
param_nth nth_rll_def)
apply (sep_auto simp: arlO_assn_def 2)
apply (subst mult.assoc)+
apply (rule fr_refl')
apply (subst heap_list_all_heap_list_all_nth_eq)
apply (subst_tac (2) i=‹nat_of_uint64 bia› in heap_list_all_nth_remove1)
apply (sep_auto simp: nth_rll_def is_array_def hr_comp_def)+
done
qed
lemma nth_aa_i64_u64_code[code]:
‹nth_aa_i64_u64 x L L' = nth_u64_code x L ⤜ (λx. arl_get_u64 x L' ⤜ return)›
unfolding nth_aa_u_def nth_aa_def arl_get_u_def[symmetric] Array.nth'_def[symmetric]
nth_nat_of_uint32_nth' nth_u_code_def[symmetric] nth_nat_of_uint64_nth'
nth_aa_i64_u64_def nth_u64_code_def arl_get_u64_def arl_get'_def
nat_of_uint64_code[symmetric]
..
lemma nth_aa_i64_u32_code[code]:
‹nth_aa_i64_u32 x L L' = nth_u64_code x L ⤜ (λx. arl_get_u x L' ⤜ return)›
unfolding nth_aa_u_def nth_aa_def arl_get_u_def[symmetric] Array.nth'_def[symmetric]
nth_nat_of_uint32_nth' nth_u_code_def[symmetric] nth_nat_of_uint64_nth'
nth_aa_i64_u32_def nth_u64_code_def arl_get_u64_def arl_get'_def
nat_of_uint64_code[symmetric] arl_get_u_def nat_of_uint32_code[symmetric]
..
lemma nth_aa_i32_u64_code[code]:
‹nth_aa_i32_u64 x L L' = nth_u_code x L ⤜ (λx. arl_get_u64 x L' ⤜ return)›
unfolding nth_aa_u_def nth_aa_def arl_get_u_def[symmetric] Array.nth'_def[symmetric]
nth_nat_of_uint32_nth' nth_u_code_def[symmetric] nth_nat_of_uint64_nth'
nth_aa_i32_u64_def nth_u64_code_def arl_get_u64_def arl_get'_def
nat_of_uint64_code[symmetric] arl_get_u_def nat_of_uint32_code[symmetric]
..
paragraph ‹Length›
definition length_raa_i64_u :: ‹'a::heap arrayO_raa ⇒ uint64 ⇒ uint32 Heap› where
‹length_raa_i64_u xs i = do {
x ← arl_get_u64 xs i;
length_u_code x}›
lemma length_raa_i64_u_alt_def: ‹length_raa_i64_u xs i = do {
n ← length_raa xs (nat_of_uint64 i);
return (uint32_of_nat n)}›
unfolding length_raa_i64_u_def length_raa_def length_u_code_def arl_get_u64_def arl_get'_def
by (auto simp: nat_of_uint64_code)
lemma length_raa_i64_u_rule[sep_heap_rules]:
‹nat_of_uint64 b < length xs ⟹ <arlO_assn (array_assn R) xs a> length_raa_i64_u a b
<λr. arlO_assn (array_assn R) xs a * ↑ (r = uint32_of_nat (length_rll xs (nat_of_uint64 b)))>⇩t›
unfolding length_raa_i64_u_alt_def length_u_code_def
by sep_auto
lemma length_raa_i64_u_hnr[sepref_fr_rules]:
shows ‹(uncurry length_raa_i64_u, uncurry (RETURN ∘∘ length_rll_n_uint32)) ∈
[λ(xs, i). i < length xs ∧ length (xs ! i) ≤ uint32_max]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint64_nat_assn⇧k → uint32_nat_assn›
by sepref_to_hoare (sep_auto simp: uint32_nat_rel_def br_def length_rll_def
nat_of_uint32_uint32_of_nat_id uint64_nat_rel_def)+
definition length_raa_i64_u64 :: ‹'a::heap arrayO_raa ⇒ uint64 ⇒ uint64 Heap› where
‹length_raa_i64_u64 xs i = do {
x ← arl_get_u64 xs i;
length_u64_code x}›
lemma length_raa_i64_u64_alt_def: ‹length_raa_i64_u64 xs i = do {
n ← length_raa xs (nat_of_uint64 i);
return (uint64_of_nat n)}›
unfolding length_raa_i64_u64_def length_raa_def length_u64_code_def arl_get_u64_def arl_get'_def
by (auto simp: nat_of_uint64_code)
lemma length_raa_i64_u64_rule[sep_heap_rules]:
‹nat_of_uint64 b < length xs ⟹ <arlO_assn (array_assn R) xs a> length_raa_i64_u64 a b
<λr. arlO_assn (array_assn R) xs a * ↑ (r = uint64_of_nat (length_rll xs (nat_of_uint64 b)))>⇩t›
unfolding length_raa_i64_u64_alt_def length_u64_code_def
by sep_auto
lemma length_raa_i64_u64_hnr[sepref_fr_rules]:
shows ‹(uncurry length_raa_i64_u64, uncurry (RETURN ∘∘ length_rll_n_uint32)) ∈
[λ(xs, i). i < length xs ∧ length (xs ! i) ≤ uint64_max]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint64_nat_assn⇧k → uint64_nat_assn›
by sepref_to_hoare
(sep_auto simp: uint32_nat_rel_def br_def length_rll_def
nat_of_uint64_uint64_of_nat_id uint64_nat_rel_def)+
definition length_raa_i32_u64 :: ‹'a::heap arrayO_raa ⇒ uint32 ⇒ uint64 Heap› where
‹length_raa_i32_u64 xs i = do {
x ← arl_get_u xs i;
length_u64_code x}›
lemma length_raa_i32_u64_alt_def: ‹length_raa_i32_u64 xs i = do {
n ← length_raa xs (nat_of_uint32 i);
return (uint64_of_nat n)}›
unfolding length_raa_i32_u64_def length_raa_def length_u64_code_def arl_get_u_def
arl_get'_def nat_of_uint32_code[symmetric]
by auto
definition length_rll_n_i32_uint64 where
[simp]: ‹length_rll_n_i32_uint64 = length_rll›
lemma length_raa_i32_u64_hnr[sepref_fr_rules]:
shows ‹(uncurry length_raa_i32_u64, uncurry (RETURN ∘∘ length_rll_n_i32_uint64)) ∈
[λ(xs, i). i < length xs ∧ length (xs ! i) ≤ uint64_max]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint32_nat_assn⇧k → uint64_nat_assn›
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def length_rll_def
nat_of_uint64_uint64_of_nat_id length_raa_i32_u64_alt_def arl_get_u_def
arl_get'_def nat_of_uint32_code[symmetric] uint32_nat_rel_def)+
definition delete_index_and_swap_aa_i64 where
‹delete_index_and_swap_aa_i64 xs i = delete_index_and_swap_aa xs (nat_of_uint64 i)›
definition last_aa_u64 where
‹last_aa_u64 xs i = last_aa xs (nat_of_uint64 i)›
lemma last_aa_u64_code[code]:
‹last_aa_u64 xs i = nth_u64_code xs i ⤜ arl_last›
unfolding last_aa_u64_def last_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
nat_of_uint64_code[symmetric]
..
definition length_raa_i32_u :: ‹'a::heap arrayO_raa ⇒ uint32 ⇒ uint32 Heap› where
‹length_raa_i32_u xs i = do {
x ← arl_get_u xs i;
length_u_code x}›
lemma length_raa_i32_rule[sep_heap_rules]:
assumes ‹nat_of_uint32 b < length xs›
shows ‹<arlO_assn (array_assn R) xs a> length_raa_i32_u a b
<λr. arlO_assn (array_assn R) xs a * ↑ (r = uint32_of_nat (length_rll xs (nat_of_uint32 b)))>⇩t›
proof -
have 1: ‹a * b* c = c * a *b› for a b c :: assn
by (auto simp: ac_simps)
have [sep_heap_rules]: ‹<arlO_assn_except (array_assn R) [nat_of_uint32 b] xs a
(λr'. array_assn R (xs ! nat_of_uint32 b) x *
↑ (x = r' ! nat_of_uint32 b))>
Array.len x <λr. arlO_assn (array_assn R) xs a *
↑ (r = length (xs ! nat_of_uint32 b))>›
for x
unfolding arlO_assn_except_def
apply (subst arlO_assn_except_array0_index[symmetric, OF assms])
apply sep_auto
apply (subst 1)
by (sep_auto simp: array_assn_def is_array_def hr_comp_def list_rel_imp_same_length
arlO_assn_except_def)
show ?thesis
using assms
unfolding length_raa_i32_u_def length_u_code_def arl_get_u_def arl_get'_def length_rll_def
by (sep_auto simp: nat_of_uint32_code[symmetric])
qed
lemma length_raa_i32_u_hnr[sepref_fr_rules]:
shows ‹(uncurry length_raa_i32_u, uncurry (RETURN ∘∘ length_rll_n_uint32)) ∈
[λ(xs, i). i < length xs ∧ length (xs ! i) ≤ uint32_max]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint32_nat_assn⇧k → uint32_nat_assn›
by sepref_to_hoare (sep_auto simp: uint32_nat_rel_def br_def length_rll_def
nat_of_uint32_uint32_of_nat_id)+
definition (in -)length_aa_u64_o64 :: ‹('a::heap array_list) array ⇒ uint64 ⇒ uint64 Heap› where
‹length_aa_u64_o64 xs i = length_aa_u64 xs i >>= (λn. return (uint64_of_nat n))›
definition arl_length_o64 where
‹arl_length_o64 x = do {n ← arl_length x; return (uint64_of_nat n)}›
lemma length_aa_u64_o64_code[code]:
‹length_aa_u64_o64 xs i = nth_u64_code xs i ⤜ arl_length_o64›
unfolding length_aa_u64_o64_def length_aa_u64_def nth_u_def[symmetric] nth_u64_code_def
Array.nth'_def arl_length_o64_def length_aa_def
by (auto simp: nat_of_uint32_code nat_of_uint64_code[symmetric])
lemma length_aa_u64_o64_hnr[sepref_fr_rules]:
‹(uncurry length_aa_u64_o64, uncurry (RETURN ∘∘ length_ll)) ∈
[λ(xs, i). i < length xs ∧ length (xs ! i) ≤ uint64_max]⇩a
(arrayO_assn (arl_assn R))⇧k *⇩a uint64_nat_assn⇧k → uint64_nat_assn›
by sepref_to_hoare (sep_auto simp: uint32_nat_rel_def length_aa_u64_o64_def br_def
length_aa_u64_def uint64_nat_rel_def nat_of_uint64_uint64_of_nat_id
length_ll_def)
definition (in -)length_aa_u32_o64 :: ‹('a::heap array_list) array ⇒ uint32 ⇒ uint64 Heap› where
‹length_aa_u32_o64 xs i = length_aa_u xs i >>= (λn. return (uint64_of_nat n))›
lemma length_aa_u32_o64_code[code]:
‹length_aa_u32_o64 xs i = nth_u_code xs i ⤜ arl_length_o64›
unfolding length_aa_u32_o64_def length_aa_u64_def nth_u_def[symmetric] nth_u_code_def
Array.nth'_def arl_length_o64_def length_aa_u_def length_aa_def
by (auto simp: nat_of_uint64_code[symmetric] nat_of_uint32_code[symmetric])
lemma length_aa_u32_o64_hnr[sepref_fr_rules]:
‹(uncurry length_aa_u32_o64, uncurry (RETURN ∘∘ length_ll)) ∈
[λ(xs, i). i < length xs ∧ length (xs ! i) ≤ uint64_max]⇩a
(arrayO_assn (arl_assn R))⇧k *⇩a uint32_nat_assn⇧k → uint64_nat_assn›
by sepref_to_hoare (sep_auto simp: uint32_nat_rel_def length_aa_u32_o64_def br_def
length_aa_u64_def uint64_nat_rel_def nat_of_uint64_uint64_of_nat_id
length_ll_def length_aa_u_def)
definition length_raa_u32 :: ‹'a::heap arrayO_raa ⇒ uint32 ⇒ nat Heap› where
‹length_raa_u32 xs i = do {
x ← arl_get_u xs i;
Array.len x}›
lemma length_raa_u32_rule[sep_heap_rules]:
‹b < length xs ⟹ (b', b) ∈ uint32_nat_rel ⟹ <arlO_assn (array_assn R) xs a> length_raa_u32 a b'
<λr. arlO_assn (array_assn R) xs a * ↑ (r = length_rll xs b)>⇩t›
supply arrayO_raa_nth_rule[sep_heap_rules]
unfolding length_raa_u32_def arl_get_u_def arl_get'_def uint32_nat_rel_def br_def
apply (cases a)
apply (sep_auto simp: nat_of_uint32_code[symmetric])
apply (sep_auto simp: arlO_assn_except_def arl_length_def array_assn_def
eq_commute[of ‹(_, _)›] is_array_def hr_comp_def length_rll_def
dest: list_all2_lengthD)
apply (sep_auto simp: arlO_assn_except_def arl_length_def arl_assn_def
hr_comp_def[abs_def] arl_get'_def
eq_commute[of ‹(_, _)›] is_array_list_def hr_comp_def length_rll_def list_rel_def
dest: list_all2_lengthD)[]
unfolding arlO_assn_def[symmetric] arl_assn_def[symmetric]
apply (subst arlO_assn_except_array0_index[symmetric, of b])
apply simp
unfolding arlO_assn_except_def arl_assn_def hr_comp_def is_array_def
apply sep_auto
done
lemma length_raa_u32_hnr[sepref_fr_rules]:
‹(uncurry length_raa_u32, uncurry (RETURN ∘∘ length_rll)) ∈
[λ(xs, i). i < length xs]⇩a (arlO_assn (array_assn R))⇧k *⇩a uint32_nat_assn⇧k → nat_assn›
by sepref_to_hoare sep_auto
definition length_raa_u32_u64 :: ‹'a::heap arrayO_raa ⇒ uint32 ⇒ uint64 Heap› where
‹length_raa_u32_u64 xs i = do {
x ← arl_get_u xs i;
length_u64_code x}›
lemma length_raa_u32_u64_hnr[sepref_fr_rules]:
shows ‹(uncurry length_raa_u32_u64, uncurry (RETURN ∘∘ length_rll_n_uint64)) ∈
[λ(xs, i). i < length xs ∧ length (xs ! i) ≤ uint64_max]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint32_nat_assn⇧k → uint64_nat_assn›
proof -
have 1: ‹a * b * c = c * a * b› for a b c :: assn
by (auto simp: ac_simps)
have H: ‹<arlO_assn_except (array_assn R) [nat_of_uint32 bi] a (aa, ba)
(λr'. array_assn R (a ! nat_of_uint32 bi) x *
↑ (x = r' ! nat_of_uint32 bi))>
Array.len x <λr. ↑(r = length (a ! nat_of_uint32 bi)) *
arlO_assn (array_assn R) a (aa, ba)>›
if
‹nat_of_uint32 bi < length a› and
‹length (a ! nat_of_uint32 bi) ≤ uint64_max›
for bi :: ‹uint32› and a :: ‹'b list list› and aa :: ‹'a array array› and ba :: ‹nat› and
x :: ‹'a array›
proof -
show ?thesis
using that apply -
apply (subst arlO_assn_except_array0_index[symmetric, OF that(1)])
by (sep_auto simp: array_assn_def arl_get_def hr_comp_def is_array_def
list_rel_imp_same_length arlO_assn_except_def)
qed
show ?thesis
apply sepref_to_hoare
apply (sep_auto simp: uint64_nat_rel_def br_def length_rll_def
nat_of_uint64_uint64_of_nat_id length_raa_u32_u64_def arl_get_u_def arl_get'_def
uint32_nat_rel_def nat_of_uint32_code[symmetric] length_u64_code_def
intro!:)+
apply (rule H; assumption)
apply (sep_auto simp: array_assn_def arl_get_def nat_of_uint64_uint64_of_nat_id)
done
qed
definition length_raa_u64_u64 :: ‹'a::heap arrayO_raa ⇒ uint64 ⇒ uint64 Heap› where
‹length_raa_u64_u64 xs i = do {
x ← arl_get_u64 xs i;
length_u64_code x}›
lemma length_raa_u64_u64_hnr[sepref_fr_rules]:
shows ‹(uncurry length_raa_u64_u64, uncurry (RETURN ∘∘ length_rll_n_uint64)) ∈
[λ(xs, i). i < length xs ∧ length (xs ! i) ≤ uint64_max]⇩a
(arlO_assn (array_assn R))⇧k *⇩a uint64_nat_assn⇧k → uint64_nat_assn›
proof -
have 1: ‹a * b * c = c * a * b› for a b c :: assn
by (auto simp: ac_simps)
have H: ‹<arlO_assn_except (array_assn R) [nat_of_uint64 bi] a (aa, ba)
(λr'. array_assn R (a ! nat_of_uint64 bi) x *
↑ (x = r' ! nat_of_uint64 bi))>
Array.len x <λr. ↑(r = length (a ! nat_of_uint64 bi)) *
arlO_assn (array_assn R) a (aa, ba)>›
if
‹nat_of_uint64 bi < length a› and
‹length (a ! nat_of_uint64 bi) ≤ uint64_max›
for bi :: ‹uint64› and a :: ‹'b list list› and aa :: ‹'a array array› and ba :: ‹nat› and
x :: ‹'a array›
proof -
show ?thesis
using that apply -
apply (subst arlO_assn_except_array0_index[symmetric, OF that(1)])
by (sep_auto simp: array_assn_def arl_get_def hr_comp_def is_array_def
list_rel_imp_same_length arlO_assn_except_def)
qed
show ?thesis
apply sepref_to_hoare
apply (sep_auto simp: uint64_nat_rel_def br_def length_rll_def
nat_of_uint64_uint64_of_nat_id length_raa_u32_u64_def arl_get_u64_def arl_get'_def
uint32_nat_rel_def nat_of_uint32_code[symmetric] length_u64_code_def length_raa_u64_u64_def
nat_of_uint64_code[symmetric]
intro!:)+
apply (rule H; assumption)
apply (sep_auto simp: array_assn_def arl_get_def nat_of_uint64_uint64_of_nat_id)
done
qed
definition length_arlO_u where
‹length_arlO_u xs = do {
n ← length_ra xs;
return (uint32_of_nat n)}›
lemma length_arlO_u[sepref_fr_rules]:
‹(length_arlO_u, RETURN o length_uint32_nat) ∈ [λxs. length xs ≤ uint32_max]⇩a (arlO_assn R)⇧k → uint32_nat_assn›
by sepref_to_hoare
(sep_auto simp: length_arlO_u_def arl_length_def uint32_nat_rel_def
br_def nat_of_uint32_uint32_of_nat_id)
definition arl_length_u64_code where
‹arl_length_u64_code C = do {
n ← arl_length C;
return (uint64_of_nat n)
}›
lemma arl_length_u64_code[sepref_fr_rules]:
‹(arl_length_u64_code, RETURN o length_uint64_nat) ∈
[λxs. length xs ≤ uint64_max]⇩a (arl_assn R)⇧k → uint64_nat_assn›
by sepref_to_hoare
(sep_auto simp: arl_length_u64_code_def arl_length_def uint64_nat_rel_def
br_def nat_of_uint64_uint64_of_nat_id arl_assn_def hr_comp_def[abs_def]
is_array_list_def dest: list_rel_imp_same_length)
paragraph ‹Setters›
definition update_aa_u64 where
‹update_aa_u64 xs i j = update_aa xs (nat_of_uint64 i) j›
definition Array_upd_u64 where
‹Array_upd_u64 i x a = Array.upd (nat_of_uint64 i) x a›
lemma Array_upd_u64_code[code]: ‹Array_upd_u64 i x a = heap_array_set'_u64 a i x ⪢ return a›
unfolding Array_upd_u64_def heap_array_set'_u64_def
Array.upd'_def
by (auto simp: nat_of_uint64_code upd_return)
lemma update_aa_u64_code[code]:
‹update_aa_u64 a i j y = do {
x ← nth_u64_code a i;
a' ← arl_set x j y;
Array_upd_u64 i a' a
}›
unfolding update_aa_u64_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
heap_array_set'_u_def[symmetric] Array_upd_u64_def nat_of_uint64_code[symmetric]
by auto
definition set_butlast_aa_u64 where
‹set_butlast_aa_u64 xs i = set_butlast_aa xs (nat_of_uint64 i)›
lemma set_butlast_aa_u64_code[code]:
‹set_butlast_aa_u64 a i = do {
x ← nth_u64_code a i;
a' ← arl_butlast x;
Array_upd_u64 i a' a
}›
unfolding set_butlast_aa_u64_def set_butlast_aa_def
nth_u64_code_def Array_upd_u64_def
by (auto simp: Array.nth'_def nat_of_uint64_code)
lemma delete_index_and_swap_aa_i64_code[code]:
‹delete_index_and_swap_aa_i64 xs i j = do {
x ← last_aa_u64 xs i;
xs ← update_aa_u64 xs i j x;
set_butlast_aa_u64 xs i
}›
unfolding delete_index_and_swap_aa_i64_def delete_index_and_swap_aa_def
last_aa_u64_def update_aa_u64_def set_butlast_aa_u64_def
by auto
lemma delete_index_and_swap_aa_i64_ll_hnr_u[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry2 delete_index_and_swap_aa_i64, uncurry2 (RETURN ooo delete_index_and_swap_ll))
∈ [λ((l,i), j). i < length l ∧ j < length_ll l i]⇩a (arrayO_assn (arl_assn R))⇧d *⇩a uint64_nat_assn⇧k *⇩a nat_assn⇧k
→ (arrayO_assn (arl_assn R))›
using assms unfolding delete_index_and_swap_aa_def delete_index_and_swap_aa_i64_def
by sepref_to_hoare (sep_auto dest: le_length_ll_nemptyD
simp: delete_index_and_swap_ll_def update_ll_def last_ll_def set_butlast_ll_def
length_ll_def[symmetric] uint32_nat_rel_def br_def uint64_nat_rel_def)
definition delete_index_and_swap_aa_i32_u64 where
‹delete_index_and_swap_aa_i32_u64 xs i j =
delete_index_and_swap_aa xs (nat_of_uint32 i) (nat_of_uint64 j)›
definition update_aa_u32_i64 where
‹update_aa_u32_i64 xs i j = update_aa xs (nat_of_uint32 i) (nat_of_uint64 j)›
lemma update_aa_u32_i64_code[code]:
‹update_aa_u32_i64 a i j y = do {
x ← nth_u_code a i;
a' ← arl_set_u64 x j y;
Array_upd_u i a' a
}›
unfolding update_aa_u32_i64_def update_aa_def nth_nat_of_uint32_nth' nth_nat_of_uint32_nth'
arl_get_u_def[symmetric] nth_u_code_def Array.nth'_def comp_def arl_set'_u64_def
heap_array_set'_u_def[symmetric] Array_upd_u_def nat_of_uint64_code[symmetric]
nat_of_uint32_code arl_set_u64_def
by auto
lemma delete_index_and_swap_aa_i32_u64_code[code]:
‹delete_index_and_swap_aa_i32_u64 xs i j = do {
x ← last_aa_u xs i;
xs ← update_aa_u32_i64 xs i j x;
set_butlast_aa_u xs i
}›
unfolding delete_index_and_swap_aa_i32_u64_def delete_index_and_swap_aa_def
last_aa_u_def update_aa_u_def set_butlast_aa_u_def update_aa_u32_i64_def
by auto
lemma delete_index_and_swap_aa_i32_u64_ll_hnr_u[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry2 delete_index_and_swap_aa_i32_u64, uncurry2 (RETURN ooo delete_index_and_swap_ll))
∈ [λ((l,i), j). i < length l ∧ j < length_ll l i]⇩a (arrayO_assn (arl_assn R))⇧d *⇩a
uint32_nat_assn⇧k *⇩a uint64_nat_assn⇧k
→ (arrayO_assn (arl_assn R))›
using assms unfolding delete_index_and_swap_aa_def delete_index_and_swap_aa_i32_u64_def
by sepref_to_hoare (sep_auto dest: le_length_ll_nemptyD
simp: delete_index_and_swap_ll_def update_ll_def last_ll_def set_butlast_ll_def
length_ll_def[symmetric] uint32_nat_rel_def br_def uint64_nat_rel_def)
paragraph ‹Swap›
definition swap_aa_i32_u64 :: "('a::{heap,default}) arrayO_raa ⇒ uint32 ⇒ uint64 ⇒ uint64 ⇒ 'a arrayO_raa Heap" where
‹swap_aa_i32_u64 xs k i j = do {
xi ← arl_get_u xs k;
xj ← swap_u64_code xi i j;
xs ← arl_set_u xs k xj;
return xs
}›
lemma swap_aa_i32_u64_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 swap_aa_i32_u64, uncurry3 (RETURN oooo swap_ll)) ∈
[λ(((xs, k), i), j). k < length xs ∧ i < length_rll xs k ∧ j < length_rll xs k]⇩a
(arlO_assn (array_assn R))⇧d *⇩a uint32_nat_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k →
(arlO_assn (array_assn R))›
proof -
note update_raa_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
have H: ‹<is_array_list p (aa, bc) *
heap_list_all_nth (array_assn (λa c. ↑ ((c, a) ∈ R'))) (remove1 bb [0..<length p]) a p *
array_assn (λa c. ↑ ((c, a) ∈ R')) (a ! bb) (p ! bb)>
Array.nth (p ! bb) (nat_of_integer (integer_of_uint64 bia))
<λr. ∃⇩A p'. is_array_list p' (aa, bc) * ↑ (bb < length p' ∧ p' ! bb = p ! bb ∧ length a = length p') *
heap_list_all_nth (array_assn (λa c. ↑ ((c, a) ∈ R'))) (remove1 bb [0..<length p']) a p' *
array_assn (λa c. ↑ ((c, a) ∈ R')) (a ! bb) (p' ! bb) *
R (a ! bb ! (nat_of_uint64 bia)) r >›
if
‹is_pure (λa c. ↑ ((c, a) ∈ R'))› and
‹bb < length p› and
‹nat_of_uint64 bia < length (a ! bb)› and
‹nat_of_uint64 bi < length (a ! bb)› and
‹length a = length p›
for bi :: ‹uint64› and bia :: ‹uint64› and bb :: ‹nat› and a :: ‹'a list list› and
aa :: ‹'b array array› and bc :: ‹nat› and p :: ‹'b array list›
using that
by (sep_auto simp: array_assn_def hr_comp_def is_array_def nat_of_uint64_code[symmetric]
list_rel_imp_same_length RR' pure_def param_nth)
have H': ‹is_array_list p' (aa, ba) * p' ! bb ↦⇩a b [nat_of_uint64 bia := b ! nat_of_uint64 bi,
nat_of_uint64 bi := xa] *
heap_list_all_nth (λa b. ∃⇩Aba. b ↦⇩a ba * ↑ ((ba, a) ∈ ⟨R'⟩list_rel))
(remove1 bb [0..<length p']) a p' * R (a ! bb ! nat_of_uint64 bia) xa ⟹⇩A
is_array_list p' (aa, ba) *
heap_list_all
(λa c. ∃⇩Ab. c ↦⇩a b * ↑ ((b, a) ∈ ⟨R'⟩list_rel))
(a[bb := (a ! bb) [nat_of_uint64 bia := a ! bb ! nat_of_uint64 bi,
nat_of_uint64 bi := a ! bb ! nat_of_uint64 bia]])
p' * true›
if
‹is_pure (λa c. ↑ ((c, a) ∈ R'))› and
le: ‹nat_of_uint64 bia < length (a ! bb)› and
le': ‹nat_of_uint64 bi < length (a ! bb)› and
‹bb < length p'› and
‹length a = length p'› and
a: ‹(b, a ! bb) ∈ ⟨R'⟩list_rel›
for bi :: ‹uint64› and bia :: ‹uint64› and bb :: ‹nat› and a :: ‹'a list list› and
xa :: ‹'b› and p' :: ‹'b array list› and b :: ‹'b list› and aa :: ‹'b array array› and ba :: ‹nat›
proof -
have 1: ‹(b[nat_of_uint64 bia := b ! nat_of_uint64 bi, nat_of_uint64 bi := xa],
(a ! bb)[nat_of_uint64 bia := a ! bb ! nat_of_uint64 bi,
nat_of_uint64 bi := a ! bb ! nat_of_uint64 bia]) ∈ ⟨R'⟩list_rel›
if ‹(xa, a ! bb ! nat_of_uint64 bia) ∈ R'›
using that a le le'
unfolding list_rel_def list_all2_conv_all_nth
by auto
have 2: ‹heap_list_all_nth (λa b. ∃⇩Aba. b ↦⇩a ba * ↑ ((ba, a) ∈ ⟨R'⟩list_rel)) (remove1 bb [0..<length p']) a p' =
heap_list_all_nth (λa c. ∃⇩Ab. c ↦⇩a b * ↑ ((b, a) ∈ ⟨R'⟩list_rel)) (remove1 bb [0..<length p'])
(a[bb := (a ! bb)[nat_of_uint64 bia := a ! bb ! nat_of_uint64 bi, nat_of_uint64 bi := a ! bb ! nat_of_uint64 bia]]) p'›
by (rule heap_list_all_nth_cong) auto
show ?thesis using that
unfolding heap_list_all_heap_list_all_nth_eq
by (subst (2) heap_list_all_nth_remove1[of bb])
(sep_auto simp: heap_list_all_heap_list_all_nth_eq swap_def fr_refl RR'
pure_def 2[symmetric] intro!: 1)+
qed
show ?thesis
using assms unfolding R'[symmetric] unfolding RR'
apply sepref_to_hoare
apply (sep_auto simp: swap_aa_i32_u64_def swap_ll_def arlO_assn_except_def length_rll_def
length_rll_update_rll nth_raa_i_u64_def uint64_nat_rel_def br_def
swap_def nth_rll_def list_update_swap swap_u64_code_def nth_u64_code_def Array.nth'_def
heap_array_set_u64_def heap_array_set'_u64_def arl_assn_def
Array.upd'_def)
apply (rule H; assumption)
apply (sep_auto simp: array_assn_def nat_of_uint64_code[symmetric] hr_comp_def is_array_def
list_rel_imp_same_length arlO_assn_def arl_assn_def hr_comp_def[abs_def] arl_set_u_def
arl_set'_u_def list_rel_pres_length uint32_nat_rel_def br_def)
apply (rule H'; assumption)
done
qed
subsubsection ‹Conversion from list of lists of \<^typ>‹nat› to list of lists of \<^typ>‹uint64› ›
sepref_definition array_nat_of_uint64_code
is array_nat_of_uint64
:: ‹(array_assn uint64_nat_assn)⇧k →⇩a array_assn nat_assn›
unfolding op_map_def array_nat_of_uint64_def array_fold_custom_replicate
apply (rewrite at ‹do {let _ = ⌑; _}› annotate_assn[where A=‹array_assn nat_assn›])
by sepref
lemma array_nat_of_uint64_conv_hnr[sepref_fr_rules]:
‹(array_nat_of_uint64_code, (RETURN ∘ array_nat_of_uint64_conv))
∈ (array_assn uint64_nat_assn)⇧k →⇩a array_assn nat_assn›
using array_nat_of_uint64_code.refine[unfolded array_nat_of_uint64_def,
FCOMP op_map_map_rel[unfolded convert_fref]] unfolding array_nat_of_uint64_conv_alt_def
by simp
sepref_definition array_uint64_of_nat_code
is array_uint64_of_nat
:: ‹[λxs. ∀a∈set xs. a ≤ uint64_max]⇩a
(array_assn nat_assn)⇧k → array_assn uint64_nat_assn›
supply [[goals_limit=1]]
unfolding op_map_def array_uint64_of_nat_def array_fold_custom_replicate
apply (rewrite at ‹do {let _ = ⌑; _}› annotate_assn[where A=‹array_assn uint64_nat_assn›])
by sepref
lemma array_uint64_of_nat_conv_alt_def:
‹array_uint64_of_nat_conv = map uint64_of_nat_conv›
unfolding uint64_of_nat_conv_def array_uint64_of_nat_conv_def by auto
lemma array_uint64_of_nat_conv_hnr[sepref_fr_rules]:
‹(array_uint64_of_nat_code, (RETURN ∘ array_uint64_of_nat_conv))
∈ [λxs. ∀a∈set xs. a ≤ uint64_max]⇩a
(array_assn nat_assn)⇧k → array_assn uint64_nat_assn›
using array_uint64_of_nat_code.refine[unfolded array_uint64_of_nat_def,
FCOMP op_map_map_rel[unfolded convert_fref]] unfolding array_uint64_of_nat_conv_alt_def
by simp
definition swap_arl_u64 where
‹swap_arl_u64 = (λ(xs, n) i j. do {
ki ← nth_u64_code xs i;
kj ← nth_u64_code xs j;
xs ← heap_array_set_u64 xs i kj;
xs ← heap_array_set_u64 xs j ki;
return (xs, n)
})›
lemma swap_arl_u64_hnr[sepref_fr_rules]:
‹(uncurry2 swap_arl_u64, uncurry2 (RETURN ooo op_list_swap)) ∈
[pre_list_swap]⇩a (arl_assn A)⇧d *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k → arl_assn A›
unfolding swap_arl_u64_def arl_assn_def is_array_list_def hr_comp_def
nth_u64_code_def Array.nth'_def heap_array_set_u64_def heap_array_set_def
heap_array_set'_u64_def Array.upd'_def
apply sepref_to_hoare
apply (sep_auto simp: nat_of_uint64_code[symmetric] uint64_nat_rel_def br_def
list_rel_imp_same_length[symmetric] swap_def)
apply (subst_tac n=‹bb› in nth_take[symmetric])
apply (simp; fail)
apply (subst_tac (2) n=‹bb› in nth_take[symmetric])
apply (simp; fail)
by (sep_auto simp: nat_of_uint64_code[symmetric] uint64_nat_rel_def br_def
list_rel_imp_same_length[symmetric] swap_def IICF_List.swap_def
simp del: nth_take
intro!: list_rel_update' param_nth)
definition butlast_nonresizing :: ‹'a list ⇒ 'a list›where
[simp]: ‹butlast_nonresizing = butlast›
definition arl_butlast_nonresizing :: ‹'a array_list ⇒ 'a array_list› where
‹arl_butlast_nonresizing = (λ(xs, a). (xs, fast_minus a 1))›
lemma butlast_nonresizing_hnr[sepref_fr_rules]:
‹(return o arl_butlast_nonresizing, RETURN o butlast_nonresizing) ∈
[λxs. xs ≠ []]⇩a (arl_assn R)⇧d → arl_assn R›
by sepref_to_hoare
(sep_auto simp: arl_butlast_nonresizing_def arl_assn_def hr_comp_def
is_array_list_def butlast_take list_rel_imp_same_length
dest:
list_rel_butlast[of ‹take _ _›])
lemma update_aa_u64_rule[sep_heap_rules]:
assumes p: ‹is_pure R› and ‹bb < length a› and ‹ba < length_ll a bb› and ‹(bb', bb) ∈ uint32_nat_rel› and
‹(ba', ba) ∈ uint64_nat_rel›
shows ‹<R b bi * arrayO_assn (arl_assn R) a ai> update_aa_u32_i64 ai bb' ba' bi
<λr. R b bi * (∃⇩Ax. arrayO_assn (arl_assn R) x r * ↑ (x = update_ll a bb ba b))>⇩t›
using assms
by (sep_auto simp add: update_aa_u32_i64_def update_ll_def p uint64_nat_rel_def uint32_nat_rel_def br_def)
lemma update_aa_u32_i64_hnr[sepref_fr_rules]:
assumes ‹is_pure R›
shows ‹(uncurry3 update_aa_u32_i64, uncurry3 (RETURN oooo update_ll)) ∈
[λ(((l,i), j), x). i < length l ∧ j < length_ll l i]⇩a
(arrayO_assn (arl_assn R))⇧d *⇩a uint32_nat_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a R⇧k → (arrayO_assn (arl_assn R))›
by sepref_to_hoare (sep_auto simp: assms)
lemma min_uint64_nat_assn:
‹(uncurry (return oo min), uncurry (RETURN oo min)) ∈ uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a uint64_nat_assn›
by (sepref_to_hoare; sep_auto simp: br_def uint64_nat_rel_def min_def nat_of_uint64_le_iff)
lemma nat_of_uint64_shiftl: ‹nat_of_uint64 (xs >> a) = nat_of_uint64 xs >> a›
by transfer (auto simp: unat_shiftr nat_shifl_div)
lemma bit_lshift_uint64_nat_assn[sepref_fr_rules]:
‹(uncurry (return oo (>>)), uncurry (RETURN oo (>>))) ∈
uint64_nat_assn⇧k *⇩a nat_assn⇧k →⇩a uint64_nat_assn›
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def nat_of_uint64_shiftl)
lemma [code]: "uint32_max_uint32 = 4294967295"
using nat_of_uint32_uint32_max_uint32
by (auto simp: uint32_max_uint32_def uint32_max_def)
end