Theory Sorting_Setup
section ‹Sorting Setup›
theory Sorting_Setup
imports "../../sepref/Hnr_Primitives_Experiment" Sorting_Misc "../../nrest/Refine_Heuristics"
"../../nrest/NREST_Automation"
begin
hide_const (open) Word.slice
paragraph ‹Summary›
text ‹This theory sets up reasoning infrastructur and basic operations used in the verification of
sorting algorithms.›
paragraph ‹Main Theorems/Definitions›
text ‹
▪ mop_cmpo_idxs, mop_cmp_idxs, mop_cmpo_idx_v, mop_cmp_v_idx, mop_cmpo_v_idx:
specifications for compare operations on arrays and option arrays
▪ myswap: algorithm for swapping elements on array using option arrays internatlly.
▪ TR_cmp_swap: exchange rate that exchanges from using the mops above and myswap
to using implementations that only use LLVM instructions.
›
subsection ‹Weakordering Locales›
definition "le_by_lt lt a b ≡ ¬lt b a"
definition "lt_by_le le a b ≡ le a b ∧ ¬le b a"
locale weak_ordering_le =
fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infix "❙≤" 50)
assumes trans: "a ❙≤ b ⟹ b ❙≤ c ⟹ a ❙≤ c"
assumes connex: "a❙≤b ∨ b❙≤a"
locale weak_ordering_lt =
fixes less :: "'a ⇒ 'a ⇒ bool" (infix "❙<" 50)
assumes asym: "a❙<b ⟹ ¬b❙<a"
assumes itrans: "a❙<c ⟹ a❙<b ∨ b❙<c"
locale weak_ordering =
fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infix "❙≤" 50)
fixes less :: "'a ⇒ 'a ⇒ bool" (infix "❙<" 50)
assumes trans[trans]: "a ❙≤ b ⟹ b ❙≤ c ⟹ a ❙≤ c"
assumes connex: "a❙≤b ∨ b❙≤a"
assumes asym: "a❙<b ⟹ ¬b❙<a"
assumes itrans: "a❙<c ⟹ a❙<b ∨ b❙<c"
assumes lt_by_le: "lt_by_le (❙≤) = (❙<)"
assumes le_by_lt: "le_by_lt (❙<) = (❙≤)"
begin
lemma unfold_lt_to_le: "a ❙< b ⟷ a❙≤b ∧ ¬b❙≤a" unfolding lt_by_le[symmetric] lt_by_le_def by simp
lemma unfold_le_to_lt: "a ❙≤ b ⟷ ¬b❙<a" unfolding le_by_lt[symmetric] le_by_lt_def by simp
abbreviation (input) greater_eq (infix "❙≥" 50) where "b❙≥a ≡ a❙≤b"
abbreviation (input) greater (infix "❙>" 50) where "b❙>a ≡ a❙<b"
lemma wo_refl[iff]: "a ❙≤ a" using connex by auto
lemma wo_irrefl[iff]: "¬a❙<a" using asym by blast
lemma wo_less_trans[trans]: "a❙<b ⟹ b❙<c ⟹ a❙<c" using asym itrans by blast
lemma [iff]:
shows transp_le: "transp (❙≤)"
and reflp_le: "reflp (❙≤)"
and transp_lt: "transp (❙<)"
and irreflp_lt: "irreflp (❙<)"
unfolding transp_def reflp_def irreflp_def
using trans wo_less_trans
by blast+
definition eq (infix "❙=" 50) where "a ❙= b ≡ ¬a❙<b ∧ ¬b❙<a"
lemma eq_refl[iff]: "a ❙= a"
unfolding eq_def by blast
lemma eq_sym: "a ❙= b ⟷ b ❙= a"
unfolding eq_def by blast
lemma eq_trans: "a ❙= b ⟹ b ❙= c ⟹ a ❙= c"
unfolding eq_def using itrans by blast
lemma eq_equiv: "equivp (❙=)"
apply (intro equivpI reflpI sympI transpI)
using eq_sym eq_trans by blast+
text ‹Compatibility lemmas, similar names as for order›
lemma wo_leI: "¬ x ❙< y ⟹ y ❙≤ x" by (simp add: unfold_le_to_lt)
lemma wo_leD: "y ❙≤ x ⟹ ¬ x ❙< y" by (simp add: unfold_le_to_lt)
lemma wo_not_le_imp_less: "¬ y ❙≤ x ⟹ x ❙< y" by (simp add: unfold_le_to_lt)
lemma wo_le_less_trans[trans]: "x ❙≤ y ⟹ y ❙< z ⟹ x ❙< z"
using itrans wo_leD by blast
lemma wo_less_le_trans[trans]: "x ❙< y ⟹ y ❙≤ z ⟹ x ❙< z"
using itrans wo_leD by blast
lemma wo_less_not_sym: "x ❙< y ⟹ ¬ (y ❙< x)"
using asym by blast
lemma wo_less_asym: "x ❙< y ⟹ (¬ P ⟹ y ❙< x) ⟹ P"
using asym by blast
end
sublocale weak_ordering_lt < weak_ordering "le_by_lt (❙<)"
apply (unfold_locales)
unfolding le_by_lt_def lt_by_le_def using asym itrans by blast+
sublocale weak_ordering_le < weak_ordering "(❙≤)" "lt_by_le (❙≤)"
apply (unfold_locales)
unfolding le_by_lt_def lt_by_le_def using trans connex by blast+
lemma linwo: "weak_ordering (≤) ((<)::_::linorder ⇒ _)"
apply unfold_locales
unfolding le_by_lt_def lt_by_le_def
by (auto simp: fun_eq_iff)
lemma funwo: "weak_ordering (λa b. f a ≤ f b) (λa b. f a < f b)" for f :: "'a ⇒ 'b::linorder"
apply unfold_locales
unfolding le_by_lt_def lt_by_le_def
by (auto simp: fun_eq_iff)
lemma le_by_linorder[simp]: "le_by_lt ((<)::_::linorder ⇒ _) = (≤)"
unfolding le_by_lt_def less_le_not_le by (intro ext) auto
lemma lt_by_linorder[simp]: "lt_by_le ((≤)::_::linorder ⇒ _) = (<)"
unfolding lt_by_le_def less_le_not_le by (intro ext) auto
lemma bex_intv_shift_aux: "(∀x∈{0..<Suc n}. P x) ⟷ (P 0 ∧ (∀x∈{0..<n}. P (Suc x)))"
apply auto
using less_Suc_eq_0_disj by auto
lemma sorted_wrt_adjacent: "⟦transp R⟧ ⟹ sorted_wrt R xs ⟷ (∀i∈{0..<length xs-1}. R (xs!i) (xs!Suc i))"
supply [simp del] = sorted_wrt.simps(2) and [simp] = sorted_wrt2_simps
apply (induction xs rule: induct_list012)
apply (auto simp: bex_intv_shift_aux)
done
abbreviation "sorted_wrt_lt lt ≡ sorted_wrt (le_by_lt lt)"
lemma sorted_wrt_lt_adjacent:
assumes "weak_ordering_lt lt"
shows "sorted_wrt_lt lt xs ⟷ (∀i∈{0..<length xs-1}. ¬lt (xs!Suc i) (xs!i))"
proof -
interpret weak_ordering_lt lt by fact
show ?thesis
apply (subst sorted_wrt_adjacent)
apply (simp_all add: le_by_lt_def)
done
qed
subsection ‹Specification of Sorting Algorithms›
lemma sorted_sorted_wrt_lt: "sorted = sorted_wrt_lt ((<)::_::linorder ⇒_)"
apply (intro ext) unfolding sorted_sorted_wrt by simp
definition "sort_spec lt xs xs' ≡ mset xs'=mset xs ∧ sorted_wrt_lt lt xs'"
definition "slice_sort_spec lt xs⇩0 l h ≡ doN {
ASSERT (l≤h ∧ h≤length xs⇩0);
SPEC (λxs. length xs = length xs⇩0 ∧ take l xs = take l xs⇩0 ∧ drop h xs = drop h xs⇩0 ∧ sort_spec lt (Misc.slice l h xs⇩0) (Misc.slice l h xs))
(λ_. cost ''slice_sort'' 1)
}"
definition "slice_sort_specT T lt xs⇩0 l h ≡ doN {
ASSERT (l≤h ∧ h≤length xs⇩0);
SPEC (λxs. length xs = length xs⇩0 ∧ take l xs = take l xs⇩0 ∧ drop h xs = drop h xs⇩0 ∧ sort_spec lt (Misc.slice l h xs⇩0) (Misc.slice l h xs))
(λ_. T)
}"
lemma slice_sort_spec_refine_sort: "⟦(xsi,xs) ∈ slice_rel xs⇩0 l h; l'=l; h'=h⟧ ⟹ slice_sort_spec lt xsi l h ≤⇓(slice_rel xs⇩0 l' h') (SPEC (sort_spec lt xs) (λ_. cost ''slice_sort'' (1::enat)))"
unfolding slice_sort_spec_def sort_spec_def
apply (refine_rcg)
by (auto simp: slice_rel_def in_br_conv)
lemma slice_sort_spec_eq_sort': "⟦(xsi,xs) ∈ slicep_rel l h; xsi'=xsi; l'=l; h'=h⟧ ⟹ ⇓(slice_rel xsi' l' h') (SPEC (sort_spec lt xs) (λ_. cost ''slice_sort'' (1::enat))) = slice_sort_spec lt xsi l h"
unfolding slice_sort_spec_def sort_spec_def
apply (auto simp: slice_rel_def slicep_rel_def in_br_conv build_rel_SPEC_conv intro!: SPEC_cong)
done
corollary slice_sort_spec_refine_sort': "⟦(xsi,xs) ∈ slicep_rel l h; xsi'=xsi; l'=l; h'=h⟧ ⟹ slice_sort_spec lt xsi l h ≤⇓(slice_rel xsi' l' h') (SPEC (sort_spec lt xs) (λ_. cost ''slice_sort'' (1::enat)))"
by (simp add: slice_sort_spec_eq_sort')
corollary slice_sort_spec_refine_sort'_sym: "⟦(xsi,xs) ∈ slicep_rel l h; xsi'=xsi; l'=l; h'=h⟧ ⟹ ⇓(slice_rel xsi' l' h') (SPEC (sort_spec lt xs) (λ_. cost ''slice_sort'' (1::enat))) ≤ slice_sort_spec lt xsi l h"
by (simp add: slice_sort_spec_eq_sort')
lemma slice_sort_spec_alt: "slice_sort_spec lt xs l h = doN {
ASSERT (l≤h ∧ h≤length xs);
SPEC (λxs'. eq_outside_range xs' xs l h
∧ mset (slice l h xs') = mset (slice l h xs)
∧ sorted_wrt_lt lt (slice l h xs')
) (λ_. cost ''slice_sort'' (1::enat))
}"
unfolding slice_sort_spec_def sort_spec_def eq_outside_range_def
by (auto simp: pw_acost_eq_iff refine_pw_simps)
lemma slice_sort_spec_sem_alt: "slice_sort_spec lt xs l h = doN {
ASSERT (l ≤ h ∧ h ≤ length xs);
SPEC (λxs'. slice_eq_mset l h xs xs' ∧ sorted_wrt_lt lt (slice l h xs')) (λ_. cost ''slice_sort'' (1::enat))
}"
unfolding slice_sort_spec_alt
by (auto simp: pw_acost_eq_iff SPEC_def refine_pw_simps slice_eq_mset_alt slice_eq_mset_eq_length eq_outside_rane_lenD dest: eq_outside_range_sym)
text ‹ Sorting a permutation of a list amounts to sorting the list! ›
lemma sort_spec_permute: "⟦mset xs' = mset xs; sort_spec lt xs' ys⟧ ⟹ sort_spec lt xs ys"
unfolding sort_spec_def by auto
subsection ‹Specification of Compare Operations on Arrays›
context weak_ordering begin
context
fixes T :: "(string, enat) acost"
begin
definition "mop_cmpo_idxs xs i j = doN {
ASSERT (i<length xs ∧ j<length xs ∧ xs!i≠None ∧ xs!j≠None);
consume (RETURNT (the (xs!i) ❙< the (xs!j))) T
}"
sepref_register mop_cmpo_idxs
lemma mop_cmpo_idxs_param: "(mop_cmpo_idxs,mop_cmpo_idxs) ∈ ⟨⟨Id::'a rel⟩option_rel⟩list_rel → nat_rel → nat_rel → ⟨bool_rel⟩ nrest_rel"
unfolding mop_cmpo_idxs_def
apply(intro fun_relI)
apply (parametricity)
unfolding list_rel_id_simp option_rel_id_simp apply (simp add: Id_def)
apply (simp add: Id_def)
apply(rule nrest_relI)
by simp
end
context
fixes T :: "(string, enat) acost"
begin
definition "mop_cmp_idxs xs i j = doN {
ASSERT (i<length xs ∧ j<length xs);
consume (RETURNT ( (xs!i) ❙< (xs!j))) T
}"
sepref_register mop_cmp_idxs
lemma mop_cmp_idxs_param: "(mop_cmp_idxs,mop_cmp_idxs) ∈ ⟨Id::'a rel⟩list_rel → nat_rel → nat_rel → ⟨bool_rel⟩ nrest_rel"
unfolding mop_cmp_idxs_def
apply(intro fun_relI)
apply (parametricity)
unfolding list_rel_id_simp option_rel_id_simp
apply(rule nrest_relI)
by simp
end
context
fixes T :: "(string, enat) acost"
begin
definition [simp]: "mop_cmp_v_idx xs v j = doN {
ASSERT (j<length xs);
consume (RETURNT ( v ❙< (xs!j))) T
}"
sepref_register mop_cmp_v_idx
lemma mop_cmp_v_idx_param: "(mop_cmp_v_idx,mop_cmp_v_idx) ∈ ⟨Id::'a rel⟩list_rel → (Id::'a rel) → nat_rel → ⟨bool_rel⟩ nrest_rel"
unfolding mop_cmp_v_idx_def
apply(intro fun_relI)
apply (parametricity)
unfolding list_rel_id_simp
apply(rule nrest_relI)
by simp
end
context
fixes T :: "(string, enat) acost"
begin
definition [simp]: "mop_cmpo_v_idx xs v j = doN {
ASSERT (j<length xs ∧ xs!j ≠ None);
consume (RETURNT ( v ❙< the (xs!j))) T
}"
sepref_register mop_cmpo_v_idx
lemma mop_cmpo_v_idx_param: "(mop_cmpo_v_idx,mop_cmpo_v_idx) ∈ ⟨⟨Id::'a rel⟩option_rel⟩list_rel → (Id::'a rel) → nat_rel → ⟨bool_rel⟩ nrest_rel"
unfolding mop_cmpo_v_idx_def
apply(intro fun_relI)
apply (parametricity)
unfolding list_rel_id_simp option_rel_id_simp
apply(simp add: Id_def)
apply(rule nrest_relI)
by simp
end
context
fixes T :: "(string, enat) acost"
begin
definition "mop_cmpo_idx_v xs i v = doN {
ASSERT (i<length xs ∧ xs!i ≠ None);
consume (RETURNT ( the (xs!i) ❙< v)) T
}"
sepref_register mop_cmpo_idx_v
lemma mop_cmpo_idx_v_param: "(mop_cmpo_idx_v,mop_cmpo_idx_v) ∈ ⟨⟨Id::'a rel⟩option_rel⟩list_rel → nat_rel → (Id::'a rel) → ⟨bool_rel⟩ nrest_rel"
unfolding mop_cmpo_idx_v_def
apply(intro fun_relI)
apply (parametricity)
unfolding list_rel_id_simp option_rel_id_simp
apply(simp add: Id_def)
apply(rule nrest_relI)
by simp
end
end
definition "SPECc3 c aop == ( (λa b. SPECT ( [(aop a b)↦ c])))"
lemma gwp_SPECc3[vcg_rules']:
fixes t :: ecost
assumes "Some (t + c) ≤ Q (op a b)"
shows "Some t ≤ gwp (SPECc3 c op a b) Q"
unfolding SPECc3_def
apply(refine_vcg ‹-›)
using assms by auto
lemma SPECc3_alt: "SPECc3 c aop = ( (λa b. consume (RETURNT (aop a b)) c))"
unfolding SPECc3_def consume_def by(auto simp: RETURNT_def intro!: ext)
lemma SPECc3_refine:
fixes c :: ecost
shows "(op x y, op' x' y')∈R ⟹ c ≤ timerefineA TR c' ⟹ SPECc3 c op x y ≤ ⇓ R (⇓⇩C TR (SPECc3 c' op' x' y'))"
unfolding SPECc3_def
apply(subst SPECT_refine_t) by auto
context
fixes c :: ecost and f:: "('a ⇒ 'b ⇒ 'c)"
begin
sepref_register timed_binop': "SPECc3 c f"
end
definition "refines_relp A c op Rimpl ≡ (uncurry Rimpl,uncurry (PR_CONST (SPECc3 c op))) ∈ A⇧k*⇩aA⇧k→⇩abool1_assn"
lemma gen_refines_relpD: "GEN_ALGO Rimpl (refines_relp A c op)
⟹ (uncurry Rimpl,uncurry (PR_CONST (SPECc3 c op))) ∈ A⇧k*⇩aA⇧k→⇩abool1_assn"
by (simp add: GEN_ALGO_def refines_relp_def)
lemma gen_refines_relpI[intro?]: "(uncurry Rimpl,uncurry (SPECc3 c op)) ∈ A⇧k*⇩aA⇧k→⇩abool1_assn ⟹ GEN_ALGO Rimpl (refines_relp A c op)"
by (simp add: GEN_ALGO_def refines_relp_def)
subsection ‹Locale for Specifying the Word Length›
locale size_t_context =
fixes size_t :: "'size_t::len2 itself"
assumes SIZE_T: "8≤LENGTH('size_t)"
begin
lemma size_t_le_maxI[simp]:
assumes "n<128"
shows "n<max_snat LENGTH('size_t)"
proof -
from SIZE_T have "7 ≤ LENGTH('size_t)-1"
using SIZE_T
by simp
hence "2^7 ≤ max_snat LENGTH('size_t)"
unfolding max_snat_def
by (simp add: numeral_2_eq_2)
with assms show ?thesis by simp
qed
lemma size_t_le_maxI'[simp]:
fixes n :: nat
assumes "n<128"
shows "n<2^(LENGTH('size_t)-Suc 0)"
using size_t_le_maxI assms
unfolding max_snat_def by simp
abbreviation "size_assn ≡ snat_assn' TYPE('size_t)"
end
subsection ‹Locale for assuming an implementation of the compare operation›
term array_assn
locale sort_impl_context = size_t_context size_t + weak_ordering
for size_t :: "'size_t::len2 itself" +
fixes
lt_impl :: "'ai::llvm_rep ⇒ 'ai ⇒ 1 word llM"
and lt_acost :: "(_,nat) acost"
and elem_assn :: "'a ⇒ 'ai ⇒ assn"
assumes lt_impl: "GEN_ALGO lt_impl (refines_relp elem_assn (lift_acost lt_acost) (❙<))"
assumes no_clash:
"the_acost (lift_acost lt_acost) ''eo_extract'' = 0"
"the_acost (lift_acost lt_acost) ''eo_set'' = 0"
assumes lt_acost_finite: "finite {a. the_acost lt_acost a ≠ 0}"
notes lt_hnr[sepref_fr_rules] = gen_refines_relpD[OF lt_impl]
notes [[sepref_register_adhoc "(❙<)"]]
notes [[sepref_register_adhoc "lt_acost"]]
begin
lemmas size_t_min = SIZE_T
abbreviation "arr_assn ≡ array_assn elem_assn"
abbreviation "lt_cost == (lift_acost lt_acost)"
thm lt_hnr
subsubsection ‹Implementing the Array-Compare Operations›
definition "cmpo_idxs2 xs⇩0 i j ≡ doN {
ASSERT (i ≠ j);
(vi,xs) ← mop_eo_extract (λ_. cost ''eo_extract'' 1) xs⇩0 i;
(vj,xs) ← mop_eo_extract (λ_. cost ''eo_extract'' 1) xs j;
r ← SPECc3 lt_cost (❙<) vi vj;
xs ← mop_eo_set (λ_. cost ''eo_set'' 1) xs i vi;
xs ← mop_eo_set (λ_. cost ''eo_set'' 1) xs j vj;
unborrow xs xs⇩0;
RETURN r
}"
definition "cmpo_v_idx2 xs⇩0 v j ≡ doN {
(vj,xs) ← mop_eo_extract (λ_. cost ''eo_extract'' 1) xs⇩0 j;
r ← SPECc3 lt_cost (❙<) v vj;
xs ← mop_eo_set (λ_. cost ''eo_set'' 1) xs j vj;
unborrow xs xs⇩0;
RETURN r
}"
definition "cmpo_idx_v2 xs⇩0 i v ≡ doN {
(vi,xs) ← mop_eo_extract (λ_. cost ''eo_extract'' 1) xs⇩0 i;
r ← SPECc3 lt_cost (❙<) vi v;
xs ← mop_eo_set (λ_. cost ''eo_set'' 1) xs i vi;
unborrow xs xs⇩0;
RETURN r
}"
definition "cmp_idxs2 xs⇩0 i j ≡ doN {
xs ← mop_to_eo_conv xs⇩0;
b ← cmpo_idxs2 xs i j;
xs ← mop_to_wo_conv xs;
unborrow xs xs⇩0;
RETURN b
}"
lemma cmpo_idxs2_refine: "(uncurry2 cmpo_idxs2, uncurry2 (PR_CONST (mop_cmpo_idxs (cost ''eo_set'' 1 + cost ''eo_set'' 1 + cost ''eo_extract'' 1 + cost ''eo_extract'' 1 + lt_cost)))) ∈ [λ((xs,i),j). i≠j]⇩f (Id×⇩rId)×⇩rId → ⟨Id⟩nrest_rel"
unfolding cmpo_idxs2_def mop_cmpo_idxs_def unborrow_def SPECc2_def
apply (intro frefI nrest_relI)
apply clarsimp
subgoal for xs i j
apply(rule gwp_specifies_acr_I)
apply (refine_vcg ‹-›)
apply (simp_all add: list_update_swap[of i j] map_update[symmetric])
subgoal apply(simp add: add.assoc) done
subgoal by (metis list_update_id list_update_overwrite option.sel)
done
done
definition "E_cmpo_idxs ≡ TId(''cmpo_idxs'':=(cost ''eo_extract'' 2) + lt_cost)"
lemma cmpo_v_idx2_refine: "(cmpo_v_idx2, PR_CONST (mop_cmpo_v_idx (cost ''eo_set'' 1 + (cost ''eo_extract'' 1 + lt_cost)))) ∈ Id → Id → Id → ⟨Id⟩nrest_rel"
unfolding cmpo_v_idx2_def mop_cmpo_v_idx_def unborrow_def SPECc2_def
apply (intro frefI nrest_relI fun_relI)
apply clarsimp
subgoal for xs i j
apply(rule gwp_specifies_acr_I)
apply (refine_vcg ‹-›)
subgoal by force
subgoal by (metis Pair_inject list_update_id list_update_overwrite option.sel)
subgoal by auto
subgoal by auto
done
done
lemma cmpo_idx_v2_refine: "(cmpo_idx_v2, PR_CONST (mop_cmpo_idx_v (cost ''eo_set'' 1 + (cost ''eo_extract'' 1 + lt_cost)))) ∈ Id → Id → Id → ⟨Id⟩nrest_rel"
unfolding cmpo_idx_v2_def mop_cmpo_idx_v_def unborrow_def SPECc2_def
apply (intro frefI nrest_relI fun_relI)
apply clarsimp
subgoal for xs i j
apply(rule gwp_specifies_acr_I)
apply (refine_vcg ‹-›)
subgoal by force
subgoal by (metis Pair_inject list_update_id list_update_overwrite option.sel)
subgoal by auto
subgoal by auto
done
done
definition "cmpo_idxs2' xs⇩0 i j ≡ doN {
ASSERT (i ≠ j);
(vi,xs) ← mop_oarray_extract xs⇩0 i;
(vj,xs) ← mop_oarray_extract xs j;
r ← SPECc3 lt_cost (❙<) vi vj;
xs ← mop_oarray_upd xs i vi;
xs ← mop_oarray_upd xs j vj;
unborrow xs xs⇩0;
RETURN r
}"
definition "cmpo_v_idx2' xs⇩0 v i ≡ doN {
(vi,xs) ← mop_oarray_extract xs⇩0 i;
r ← SPECc3 lt_cost (❙<) v vi;
xs ← mop_oarray_upd xs i vi;
unborrow xs xs⇩0;
RETURN r
}"
definition "cmpo_idx_v2' xs⇩0 i v ≡ doN {
(vi,xs) ← mop_oarray_extract xs⇩0 i;
r ← SPECc3 lt_cost (❙<) vi v;
xs ← mop_oarray_upd xs i vi;
unborrow xs xs⇩0;
RETURN r
}"
definition "cmp_idxs2' xs⇩0 i j ≡ doN {
xs ← mop_to_eo_conv xs⇩0;
b ← cmpo_idxs2' xs i j;
xs ← mop_to_wo_conv xs;
unborrow xs xs⇩0;
RETURN b
}"
sepref_register cmpo_idx_v2' cmpo_v_idx2' cmpo_idxs2' cmp_idxs2'
definition "E_mop_oarray_extract ≡ TId(''eo_extract'':=lift_acost mop_array_nth_cost, ''eo_set'':=lift_acost mop_array_upd_cost)"
lemma mop_oarray_extract_refine:
"mop_oarray_extract a b ≤ ⇓ Id (timerefine E_mop_oarray_extract (mop_eo_extract (λ_. cost ''eo_extract'' 1) a b))"
unfolding mop_oarray_extract_def E_mop_oarray_extract_def mop_eo_extract_def
apply(intro refine0)
by(auto simp: timerefineA_update_apply_same_cost intro!: wfR''_upd)
lemma mop_eo_set_ghost[refine]:
"(x,x') ∈ A ⟹ (xs,xs') ∈ ⟨⟨A⟩option_rel⟩list_rel ⟹ (i,i')∈nat_rel ⟹ wfR'' R ⟹
lift_acost mop_array_upd_cost ≤ R ''eo_set'' ⟹ mop_oarray_upd xs i x ≤ ⇓ (⟨⟨A⟩option_rel⟩list_rel) (timerefine R (mop_eo_set (λ_. cost ''eo_set'' 1) xs' i' x'))"
unfolding mop_oarray_upd_def mop_eo_set_def
apply(intro refine0)
apply safe
subgoal
by (simp add: list_rel_imp_same_length)
subgoal
using param_nth by fastforce
subgoal by(simp add: timerefineA_cost)
subgoal
by (smt length_list_update list_rel_eq_listrel listrel_iff_nth nth_list_update option_relI(2) relAPP_def)
done
lemma unborrow_refine[refine]:
fixes E :: "'e ⇒ ('c, enat) acost"
shows "((), ()) ∈ R ⟹ (a, a') ∈ Id ⟹ (b, b') ∈ Id ⟹ unborrow a b ≤ ⇓R (timerefine E (unborrow a' b'))"
unfolding unborrow_def
apply(intro refine0)
apply simp_all
done
lemma the_acost_timerefineA_upd_if_neq: "the_acost T y = 0 ⟹ timerefineA (F(y := t)) T = timerefineA F T"
unfolding timerefineA_def
unfolding fun_upd_def
apply simp apply(rule ext)
apply(rule Sum_any.cong) by auto
lemma SPECc2_lt_refine[refine]:
"(a,a')∈Id ⟹ (b,b')∈Id ⟹ SPECc3 lt_cost (❙<) a b ≤ ⇓ bool_rel (timerefine E_mop_oarray_extract (SPECc3 lt_cost (❙<) a' b'))"
apply(rule SPECc3_refine)
apply (auto simp: cost_n_leq_TId_n E_mop_oarray_extract_def)
using no_clash
unfolding less_eq_acost_def
apply(auto)
subgoal for x
apply(cases "x=''eo_extract''") apply simp
apply(cases "x=''eo_set''") apply simp
apply(subst the_acost_timerefineA_upd_if_neq) apply simp
apply(subst the_acost_timerefineA_upd_if_neq) apply simp
by simp
done
lemma wfR_E: "wfR'' E_mop_oarray_extract"
by(auto simp: E_mop_oarray_extract_def intro!: wfR''_upd)
lemma cmpo_v_idx2'_refine: "(cmpo_v_idx2', cmpo_v_idx2) ∈ Id → Id → Id → nrest_trel Id E_mop_oarray_extract"
unfolding cmpo_v_idx2'_def cmpo_v_idx2_def
unfolding nrest_trel_def_internal
apply (intro frefI nrest_relI fun_relI)
apply safe
supply bindT_refine_conc_time2[refine]
supply mop_oarray_extract_refine[refine]
apply (refine_rcg)
apply refine_dref_type
apply (simp_all add: wfR_E)
apply (simp add: E_mop_oarray_extract_def )
done
lemma cmpo_idx_v2'_refine: "(cmpo_idx_v2', cmpo_idx_v2) ∈ Id → Id → Id → nrest_trel Id E_mop_oarray_extract"
unfolding cmpo_idx_v2'_def cmpo_idx_v2_def
unfolding nrest_trel_def_internal
apply (intro frefI nrest_relI fun_relI)
apply safe
supply bindT_refine_conc_time2[refine]
supply mop_oarray_extract_refine[refine]
apply (refine_rcg)
apply refine_dref_type
apply (simp_all add: wfR_E)
apply (simp add: E_mop_oarray_extract_def )
done
lemma cmp_idxs2_refine: "(uncurry2 cmp_idxs2,uncurry2 (PR_CONST (mop_cmp_idxs (cost ''eo_set'' 1 + cost ''eo_set'' 1 + cost ''eo_extract'' 1 + cost ''eo_extract'' 1 + lt_cost))))∈[λ((xs,i),j). i≠j]⇩f (Id×⇩rId)×⇩rId → ⟨Id⟩nrest_rel"
unfolding cmp_idxs2_def mop_cmp_idxs_def PR_CONST_def cmpo_idxs2_def unborrow_def SPECc2_def
unfolding mop_to_eo_conv_def mop_to_wo_conv_def
apply (intro frefI nrest_relI)
apply clarsimp
subgoal for xs i j
apply(rule gwp_specifies_acr_I)
apply (refine_vcg ‹-›)
subgoal apply (simp add: lift_acost_zero add.assoc) by force
subgoal by auto
subgoal by auto
subgoal by (metis Pair_inject list_update_id list_update_overwrite list_update_swap option.sel)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
done
definition "cmpo_v_idx2'_cost = lift_acost mop_array_nth_cost + (lt_cost + lift_acost mop_array_upd_cost)"
lemma cmpo_v_idx2'_refines_mop_cmpo_v_idx_with_E:
assumes "wfR'' EE"
and "cmpo_v_idx2'_cost ≤ timerefineA EE (cost ''cmpo_v_idx'' 1)"
shows "(a,a')∈Id ⟹ (b,b')∈Id ⟹ (c,c')∈Id ⟹ cmpo_v_idx2' a b c ≤ ⇓ bool_rel (timerefine EE (mop_cmpo_v_idx (cost ''cmpo_v_idx'' 1) a' b' c'))"
supply conc_Id[simp del]
unfolding cmpo_v_idx2'_def mop_cmpo_v_idx_def
unfolding mop_oarray_extract_def mop_eo_extract_def unborrow_def SPECc3_alt
mop_oarray_upd_def mop_eo_set_def consume_alt
apply normalize_blocks apply(split prod.splits)+
apply normalize_blocks
apply simp
apply(intro refine0 consumea_refine bindT_refine_easy)
apply refine_dref_type
subgoal by auto
subgoal by auto
subgoal using assms(1) by auto
subgoal by auto
subgoal
apply(rule order.trans[OF _ assms(2)])
by(simp add: cmpo_v_idx2'_cost_def)
subgoal by simp
done
definition "cmpo_idxs2'_cost = lift_acost mop_array_nth_cost + (lift_acost mop_array_nth_cost
+ (lt_cost + (lift_acost mop_array_upd_cost + lift_acost mop_array_upd_cost)))"
lemma cmpo_idxs2'_refines_mop_cmpo_idxs_with_E:
assumes "wfR'' E"
"cmpo_idxs2'_cost ≤ timerefineA E (cost ''cmpo_idxs'' 1)"
shows
"b'≠c' ⟹ (a,a')∈Id ⟹ (b,b')∈Id ⟹ (c,c')∈Id ⟹
cmpo_idxs2' a b c ≤ ⇓ bool_rel (timerefine E (mop_cmpo_idxs (cost ''cmpo_idxs'' 1) a' b' c'))"
supply conc_Id[simp del]
unfolding cmpo_idxs2'_def mop_cmpo_idxs_def
unfolding mop_oarray_extract_def mop_eo_extract_def unborrow_def SPECc3_alt
mop_oarray_upd_def mop_eo_set_def consume_alt
apply normalize_blocks apply(split prod.splits)+
apply normalize_blocks
apply simp
apply(intro refine0 consumea_refine bindT_refine_easy)
apply refine_dref_type
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (metis list_update_id list_update_overwrite list_update_swap option.sel)
subgoal using assms(1) by simp
subgoal by simp
subgoal
apply(rule order.trans[OF _ assms(2)])
by(simp add: cmpo_idxs2'_cost_def)
subgoal by simp
done
definition "cmp_idxs2'_cost = lift_acost mop_array_nth_cost + (lift_acost mop_array_nth_cost
+ (lt_cost + (lift_acost mop_array_upd_cost
+ lift_acost mop_array_upd_cost)))"
lemma cmp_idxs2'_refines_mop_cmp_idxs_with_E:
assumes "wfR'' E"
"cmp_idxs2'_cost ≤ timerefineA E (cost ''cmp_idxs'' 1)"
shows
"b'≠c' ⟹ (a,a')∈Id ⟹ (b,b')∈Id ⟹ (c,c')∈Id ⟹
cmp_idxs2' a b c ≤ ⇓ bool_rel (timerefine E (mop_cmp_idxs (cost ''cmp_idxs'' 1) a' b' c'))"
supply conc_Id[simp del]
unfolding cmp_idxs2'_def cmpo_idxs2'_def mop_cmp_idxs_def
unfolding mop_oarray_extract_def mop_eo_extract_def unborrow_def SPECc3_alt
mop_oarray_upd_def mop_eo_set_def consume_alt
unfolding mop_to_eo_conv_def mop_to_wo_conv_def
apply normalize_blocks apply(split prod.splits)+
apply normalize_blocks
apply simp
apply(intro refine0 consumea_refine bindT_refine_easy)
apply refine_dref_type
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (metis list_update_id list_update_overwrite list_update_swap option.sel)
subgoal using assms(1) by simp
subgoal by simp
subgoal
apply(rule order.trans[OF _ assms(2)])
by (simp add: lift_acost_zero cmp_idxs2'_cost_def)
subgoal by simp
done
subsubsection ‹Synthesizing LLVM Code for the Array-Compare Operations›
sepref_def cmpo_idxs_impl [llvm_inline] is "uncurry2 (PR_CONST cmpo_idxs2')" :: "(eoarray_assn elem_assn)⇧k *⇩a snat_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
unfolding cmpo_idxs2'_def PR_CONST_def
by sepref
sepref_def cmpo_v_idx_impl [llvm_inline] is "uncurry2 (PR_CONST cmpo_v_idx2')" :: "(eoarray_assn elem_assn)⇧k *⇩a elem_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
unfolding cmpo_v_idx2'_def PR_CONST_def
by sepref
thm cmp_idxs2_def cmp_idxs2'_def
term cmp_idxs2'
sepref_def cmp_idxs_impl [llvm_inline] is "uncurry2 (PR_CONST cmp_idxs2')" :: "(array_assn elem_assn)⇧k *⇩a snat_assn⇧k *⇩a snat_assn⇧k →⇩a bool1_assn"
unfolding cmp_idxs2'_def cmpo_idxs2'_def PR_CONST_def
supply [sepref_fr_rules] = mop_to_wo_conv_hnr_dep mop_to_eo_conv_hnr_dep
by sepref
sepref_definition cmpo_idx_v_impl [llvm_inline] is "uncurry2 cmpo_idx_v2'" :: "(eoarray_assn elem_assn)⇧k *⇩a snat_assn⇧k *⇩a elem_assn⇧k →⇩a bool1_assn"
unfolding cmpo_idx_v2'_def PR_CONST_def
by sepref
end
locale pure_sort_impl_context = sort_impl_context +
constrains size_t :: "'size_t::len2 itself"
assumes pureA[safe_constraint_rules]: "CONSTRAINT is_pure elem_assn"
notes [sepref_frame_free_rules] = mk_free_is_pure[OF CONSTRAINT_D[OF pureA]]
begin
end
lemma SPECc3_to_SPECc2: "SPECc3 (cost n 1) aop = SPECc2 n aop"
unfolding SPECc3_def SPECc2_def by auto
thm hn_unat_ops(13)
lemma unat_sort_impl_context: "8 ≤ LENGTH('size_t) ⟹ pure_sort_impl_context TYPE('size_t::len2) (≤) (<) ll_icmp_ult (cost ''icmp_ult'' 1) unat_assn"
apply intro_locales
subgoal apply unfold_locales .
apply (rule linwo)
apply unfold_locales
apply rule
apply(simp_all only: lift_acost_cost )
unfolding Extended_Nat.enat_1 SPECc3_to_SPECc2
apply (rule hn_unat_ops[unfolded PR_CONST_def])
apply (simp add: zero_acost_def cost_def)
apply (simp add: zero_acost_def cost_def)
apply (metis finite_sum_nonzero_cost)
apply (solve_constraint)
done
subsection ‹Random Access Iterator›
text ‹The compare function takes an external parameter.›
term mop_eo_set
locale random_access_iterator =
fixes wo_assn :: "'a list ⇒ 'oi::llvm_rep ⇒ assn"
and eo_assn :: "'a option list ⇒ 'oi ⇒ assn"
and elem_assn :: "'a ⇒ 'ai::llvm_rep ⇒ assn"
and to_eo_impl :: "'oi ⇒ 'oi llM"
and to_wo_impl :: "'oi ⇒ 'oi llM"
and extract_impl :: "'oi ⇒ 'size::len2 word ⇒ ('ai × 'oi) llM"
and extract_impl_cost :: "ecost"
and set_impl :: "'oi ⇒ 'size word ⇒ 'ai ⇒ 'oi llM"
and set_impl_cost :: "ecost"
assumes
to_eo_hnr: "(to_eo_impl, mop_to_eo_conv) ∈ wo_assn⇧d →⇩a⇩d (λ_ ai. cnc_assn (λx. x=ai) eo_assn)"
and to_wo_hnr: "(to_wo_impl, mop_to_wo_conv) ∈ eo_assn⇧d →⇩a⇩d (λ_ ai. cnc_assn (λx. x=ai) wo_assn)"
and eo_extract_hnr_aux: "(uncurry extract_impl, uncurry (mop_eo_extract (λ_. extract_impl_cost))) ∈ eo_assn⇧d *⇩a snat_assn⇧k →⇩a⇩d (λ_ (ai,_). elem_assn ×⇩a cnc_assn (λx. x = ai) eo_assn)"
and eo_set_hnr_aux: "(uncurry2 set_impl, uncurry2 (mop_eo_set (λ_. set_impl_cost))) ∈ eo_assn⇧d *⇩a snat_assn⇧k *⇩a elem_assn⇧d →⇩a⇩d (λ_ ((ai,_),_). cnc_assn (λx. x=ai) eo_assn)"
notes [[sepref_register_adhoc to_eo_impl to_wo_impl extract_impl set_impl]]
begin
context
notes [fcomp_norm_simps] = option_rel_id_simp list_rel_id prod_rel_id_simp hrr_comp_id_conv
begin
private method rl_mono =
(rule hfref_cons;
clarsimp_all;
clarsimp_all simp: cnc_assn_def sep_algebra_simps entails_lift_extract_simps)
lemma eo_extract_nodep_hnr_aux:
"(uncurry extract_impl, uncurry (mop_eo_extract (λ_. extract_impl_cost))) ∈ eo_assn⇧d *⇩a snat_assn⇧k →⇩a elem_assn ×⇩a eo_assn"
using eo_extract_hnr_aux
by rl_mono
lemma eo_set_nodep_hnr_aux:
"(uncurry2 set_impl, uncurry2 (mop_eo_set (λ_. set_impl_cost))) ∈ eo_assn⇧d *⇩a snat_assn⇧k *⇩a elem_assn⇧d →⇩a eo_assn"
using eo_set_hnr_aux
by rl_mono
lemma to_eo_nodep_hnr[sepref_fr_rules]: "(to_eo_impl, mop_to_eo_conv) ∈ wo_assn⇧d →⇩a eo_assn"
using to_eo_hnr
by rl_mono
lemma to_wo_nodep_hnr[sepref_fr_rules]: "(to_wo_impl, mop_to_wo_conv) ∈ eo_assn⇧d →⇩a wo_assn"
using to_wo_hnr
by rl_mono
end
end
definition "refines_param_relp P A R Rimpl ≡ (uncurry2 Rimpl,uncurry2 R) ∈ P⇧k*⇩aA⇧k*⇩aA⇧k→⇩abool1_assn"
lemma gen_refines_param_relpD: "GEN_ALGO Rimpl (refines_param_relp P A R)
⟹ (uncurry2 Rimpl,uncurry2 R) ∈ P⇧k*⇩aA⇧k*⇩aA⇧k→⇩abool1_assn"
by (simp add: GEN_ALGO_def refines_param_relp_def)
subsection "Some more commands"
context
fixes T :: "(nat × nat × nat) ⇒ (char list, enat) acost"
begin
definition mop_list_swap :: "'a list ⇒ nat ⇒ nat ⇒ ('a list, _) nrest"
where [simp]: "mop_list_swap xs i j ≡ do { ASSERT (i<length xs ∧ j<length xs); consume (RETURNT (swap xs i j)) (T (length xs,i,j)) }"
sepref_register "mop_list_swap"
end
lemma param_mop_list_get:
"(mop_list_swap T, mop_list_swap T) ∈ ⟨the_pure A⟩ list_rel → nat_rel → nat_rel → ⟨⟨the_pure A⟩ list_rel⟩ nrest_rel"
apply(intro nrest_relI fun_relI)
unfolding mop_list_swap_def swap_def
apply (auto simp: pw_acost_le_iff refine_pw_simps list_rel_imp_same_length)
apply parametricity
by auto
abbreviation "mop_list_swapN ≡ mop_list_swap (λ_. cost ''list_swap'' 1)"
abbreviation "mop_list_getN ≡ mop_list_get (λ_. cost ''list_get'' 1)"
abbreviation "mop_list_setN ≡ mop_list_set (λ_. cost ''list_set'' 1)"
abbreviation "SPECc2F aop ≡ ( (λa b. consume (RETURNT (aop a b)) top))"
abbreviation "mop_list_getF ≡ mop_list_get (λ_. top)"
abbreviation "mop_list_setF ≡ mop_list_set (λ_. top)"
abbreviation "mop_list_swapF ≡ mop_list_swap (λ_. top)"
abbreviation (in weak_ordering) "mop_cmp_idxsF ≡ mop_cmp_idxs top"
subsubsection ‹Implementing Swap›
definition myswap where "myswap xs l h =
doN {
xs ← mop_to_eo_conv xs;
(x,xs) ← mop_oarray_extract xs l;
(y,xs) ← mop_oarray_extract xs h;
xs ← mop_oarray_upd xs l y;
xs ← mop_oarray_upd xs h x;
xs ← mop_to_wo_conv xs;
RETURN xs
}"
definition myswap_cost :: ecost where
"myswap_cost = lift_acost mop_array_nth_cost + lift_acost mop_array_nth_cost + lift_acost mop_array_upd_cost + lift_acost mop_array_upd_cost "
lemma myswap_refine:
assumes "wfR'' E"
"myswap_cost ≤ timerefineA E (cost ''list_swap'' 1)"
shows
"l≠h ⟹ (xs,xs')∈Id ⟹ (l,l')∈Id ⟹ (h,h')∈Id
⟹ myswap xs l h ≤ ⇓ (⟨Id⟩list_rel) (timerefine E (mop_list_swapN xs' l' h'))"
unfolding myswap_def mop_list_swap_def
unfolding mop_to_eo_conv_def mop_to_wo_conv_def
unfolding mop_oarray_extract_def mop_oarray_upd_def
unfolding mop_eo_extract_def mop_eo_set_def
apply normalize_blocks
apply(split prod.splits)+
apply normalize_blocks
apply safe
apply(intro refine0 bindT_refine_conc_time_my_inres consumea_refine)
apply refine_dref_type
subgoal apply auto done
subgoal apply auto done
subgoal apply auto done
subgoal apply auto done
subgoal apply auto
by (metis None_notin_image_Some list.set_map list_update_overwrite list_update_swap map_update)
subgoal using assms by auto
subgoal by auto
subgoal
apply(rule order.trans[OF _ assms(2)])
unfolding myswap_cost_def
by (auto simp: add.assoc timerefineA_update_apply_same_cost lift_acost_zero)
subgoal by (auto simp add: More_List.swap_def list_update_swap map_update option.exhaust_sel)
done
subsection ‹An Exchange Rate that refines compare and swap operations to executable ones›
context sort_impl_context
begin
abbreviation "TR_cmp_swap ≡ TId(''cmp_idxs'':=cmp_idxs2'_cost, ''cmpo_idxs'':=cmpo_idxs2'_cost,''cmpo_v_idx'':=cmpo_v_idx2'_cost, ''list_swap'':= myswap_cost)"
lemma wfR''E[simp]: " wfR'' TR_cmp_swap" by (auto intro!: wfR''_upd)
lemma sp_E45[simp]: "struct_preserving TR_cmp_swap"
by (auto intro!: struct_preserving_upd_I)
lemma myswap_TR_cmp_swap_refine:
"l≠h ⟹ (xs,xs')∈Id ⟹ (l,l')∈Id ⟹ (h,h')∈Id
⟹ myswap xs l h ≤ ⇓ (⟨Id⟩list_rel) (timerefine TR_cmp_swap (mop_list_swapN xs' l' h'))"
apply(rule myswap_refine)
by (auto simp: timerefineA_update_apply_same_cost lift_acost_zero)
lemma mop_oarray_upd_refines:
assumes "wfR'' TR"
and "preserves_curr TR ''store''"
and "preserves_curr TR ''ofs_ptr''"
shows "(a,a')∈Id ⟹ (b,b')∈Id ⟹ (c,c')∈Id ⟹
mop_oarray_upd a b c ≤ ⇓ Id (timerefine TR (mop_oarray_upd a' b' c'))"
unfolding mop_oarray_upd_def mop_eo_set_def
using assms
apply(intro refine0)
apply (auto simp: timerefineA_cost_apply_costmult timerefineA_propagate
lift_acost_propagate lift_acost_cost timerefineA_update_apply_same_cost intro!: wfR''_upd)
apply(simp add: assms(2,3)[THEN preserves_curr_D] costmult_cost)
done
lemma mop_oarray_extract_refines:
assumes "wfR'' TR"
and "preserves_curr TR ''load''"
and "preserves_curr TR ''ofs_ptr''"
shows "(x,x')∈Id ⟹ (i,i')∈Id ⟹
mop_oarray_extract x i ≤ ⇓ Id (timerefine TR (mop_oarray_extract x' i'))"
unfolding mop_oarray_extract_def mop_eo_extract_def
using assms
apply(intro refine0)
apply (auto simp: timerefineA_cost_apply_costmult timerefineA_propagate
lift_acost_propagate lift_acost_cost timerefineA_update_apply_same_cost intro!: wfR''_upd)
apply(simp add: assms(2,3)[THEN preserves_curr_D] costmult_cost)
done
end
end