Theory Sep_Block_Allocator_RS
section ‹Generic Block Allocator --- Resoning Setup›
theory Sep_Block_Allocator_RS
imports Sep_Lift "../basic/LLVM_Basic_Main"
begin
lemma listα_at_len: "listα α xs (length xs) = 0"
by (auto simp: listα_def)
lemma listα_gt_len: "i≥length xs ⟹ listα α xs i = 0"
by (auto simp: listα_def)
lemma listα_snoc: "listα α (xs@[x]) = 0(length xs := α x) + listα α xs"
apply (rule ext)
apply (auto simp: listα_def nth_append)
done
lemma listα_in_range: "listα α xs i ≠ 0 ⟹ i<length xs"
by (auto simp: listα_def split: if_splits)
lemma listα_in_rangeD: "listα α xs = x ⟹ x i ≠ 0 ⟹ i<length xs"
by (auto simp: listα_def split: if_splits)
lemma listα_splitE:
assumes "listα α xs = fun_upd 0 i p + fun_upd f i 0"
assumes "p≠0"
obtains "i<length xs" "α (xs!i) = p"
using assms
by (auto simp: listα_def fun_eq_iff split: if_splits)
lemma optionα_splitE:
assumes "optionα α v = p"
assumes "p≠0"
obtains x where "v=Some x" "α x = p"
using assms by (cases v) auto
locale block_allocator2 = block_allocator1 static_err mem_err bload bstore bcheck_addr
for static_err :: 'err
and mem_err :: 'err
and bload :: "'baddr::this_addr ⇒ ('val,_,_,'block,'err) M"
and bstore :: "'val ⇒ 'baddr ⇒ (unit,_,_,'block,'err) M"
and bcheck_addr :: "'baddr ⇒ (unit,_,_,'block,'err) M"
+ fixes αb :: "'block ⇒ 'ablock::unique_zero_sep_algebra"
and bpto :: "'val ⇒ 'baddr ⇒ 'ablock ⇒ bool"
and tag_of :: "'block ⇒ 'tag"
and is_complete_tag :: "'ablock ⇒ 'tag ⇒ bool"
assumes bload_rule: "⋀x a. notime.htriple αb (bpto x a) (bload a) (λr. ↑(r=x) ** bpto x a)"
and bstore_rule: "⋀x xx a. notime.htriple αb (bpto xx a) (bstore x a) (λ_. bpto x a)"
and bload_pres_tag: "⋀s a. wlp (bload a) (λ_ s'. tag_of s' = tag_of s) s"
and bstore_pres_tag: "⋀s a x. wlp (bstore a x) (λ_ s'. tag_of s' = tag_of s) s"
and complete_tag:
"⋀f. ⟦is_complete_tag ablock (tag_of cblock); ablock ## f; αb cblock = ablock + f⟧ ⟹ f=0"
and bpto_notZ: "⋀x a. ¬bpto x a 0"
begin
definition αtag :: "'block ⇒ 'tag tsa_opt" where "αtag blk ≡ TRIV (tag_of blk)"
definition α :: "'block memory ⇒ nat ⇒ 'ablock × 'tag tsa_opt"
where "α ≡ λMEMORY blocks ⇒ listα (optionα (λx. (αb x, αtag x))) blocks"
definition pto :: "'val ⇒ 'baddr addr rptr ⇒ (nat ⇒ 'ablock × 'tag tsa_opt) ⇒ bool"
where "pto x ≡ λRP_ADDR (ADDR bi ba) ⇒ λs. ∃ablk. s=0(bi:=(ablk,0)) ∧ bpto x ba ablk | _ ⇒ sep_false"
definition tag :: "'tag ⇒ 'baddr addr rptr ⇒ (nat ⇒ 'ablock × 'tag tsa_opt) ⇒ bool"
where "tag t ≡ λRP_ADDR (ADDR bi ba) ⇒ EXACT (0(bi:=(0,TRIV t))) ** ↑(ba=this_addr ∧ t∈range tag_of) | _ ⇒ sep_false"
definition block :: "'ablock ⇒ 'baddr addr rptr ⇒ (nat ⇒ 'ablock × 'tag tsa_opt) ⇒ bool"
where "block b ≡ λRP_ADDR (ADDR bi ba) ⇒ EXACT (0(bi:=(b,0))) ** ↑(ba=this_addr) | _ ⇒ sep_false"
lemma alloc_rule: "notime.htriple α □ (alloc b) (λr. block (αb b) r ** tag (tag_of b) r)"
apply (rule notime.htripleI')
apply (auto simp: alloc_def wpn_def run_simps sep_algebra_simps split: option.splits)
proof -
fix s :: "'block memory"
obtain blocks where [simp]: "s = MEMORY blocks" by (cases s)
show "∃p'. p' ## α s ∧
α (put' memory.the_memory⇩L (get' memory.the_memory⇩L s @ [Some b]) s) = p' + α s ∧
(block (αb b) (RP_ADDR (ADDR (length (get' memory.the_memory⇩L s)) this_addr)) ∧*
tag (tag_of b) (RP_ADDR (ADDR (length (get' memory.the_memory⇩L s)) this_addr)))
p'"
apply (rule exI[where x="0(length blocks := (αb b, TRIV (tag_of b)))"]; intro conjI)
apply (clarsimp_all simp: α_def block_def tag_def αtag_def sep_algebra_simps listα_at_len)
subgoal by (simp add: listα_snoc)
subgoal
apply (subst EXACT_split[symmetric])
apply (auto simp: sep_algebra_simps)
done
done
qed
lemma complete_splitE:
assumes C: "is_complete_tag blk t"
assumes DISJ: "f i ## (blk, TRIV t)"
assumes AEQ: "listα (optionα (λx. (αb x, αtag x))) xs = f + fun_upd 0 i (blk, TRIV t)"
obtains cblk where
"i<length xs" "xs!i = Some cblk" "blk = αb cblk" "t = tag_of cblk" "f i = 0"
proof -
have [simp]: "i<length xs"
apply (rule listα_in_rangeD[OF AEQ])
apply (auto simp: sep_algebra_simps DISJ)
done
obtain fib fit where [simp]: "f i = (fib,fit)" by (cases "f i")
from DISJ have [simp]: "blk ## fib" "fit = 0"
by (auto simp: sep_algebra_simps)
obtain cblk where [simp]: "xs!i = Some cblk" "αb cblk = blk + fib" "t = tag_of cblk"
using fun_cong[OF AEQ, of i]
apply (cases "xs!i")
apply (auto simp: listα_def sep_algebra_simps if_splits αtag_def)
done
from complete_tag[OF C[simplified], of fib, simplified] have [simp]: "fib=0" .
show ?thesis
apply (rule that[of cblk])
apply (auto simp: sep_algebra_simps)
done
qed
lemma free_rule: "notime.htriple α (block blk a ** tag t a ** ↑(is_complete_tag blk t)) (free a) (λ_. □)"
apply (rule notime.htripleI')
subgoal for p s f
apply (cases s)
apply (auto simp: free_def wpn_def run_simps sep_algebra_simps split: option.splits addr.splits rptr.splits)
apply (auto simp: block_def tag_def sep_algebra_simps pred_lift_extract_simps)
apply (all ‹subst (asm) EXACT_split[symmetric] sep_disj_fun_def; clarsimp simp: sep_algebra_simps›)
apply (auto simp: α_def sep_algebra_simps merge_fun_singleton split_fun_upd_0)
subgoal
apply (erule (2) complete_splitE)
by auto
subgoal
apply (erule (2) complete_splitE)
by auto
subgoal for xs i
by (force simp: sep_algebra_simps dest: sep_disj_funD[where x=i] listα_in_rangeD[where i=i])
subgoal
apply (erule (2) complete_splitE)
by auto
done
done
definition "block_lifter bi ≡ ⦇
sep_lifter.lift = λx. (0(bi:=(x,0))),
sep_lifter.project = (λf. fst (f bi)),
sep_lifter.carve = (λf. f(bi:=(0,snd (f bi)))),
sep_lifter.splittable = (λf. True),
sep_lifter.L = lens_of_bi bi,
sep_lifter.αb = α,
sep_lifter.αs = αb,
sep_lifter.tyb = λ_. (),
sep_lifter.tys = tag_of
⦈"
lemma block_lifter_simps[simp]:
"sep_lifter.lift (block_lifter bi) = (λx. (0(bi:=(x,0))))"
"sep_lifter.project (block_lifter bi) = (λf. fst (f bi))"
"sep_lifter.carve (block_lifter bi) = (λf. f(bi:=(0,snd (f bi))))"
"sep_lifter.splittable (block_lifter bi) = (λf. True)"
"sep_lifter.L (block_lifter bi) = lens_of_bi bi"
"sep_lifter.αb (block_lifter bi) = α"
"sep_lifter.αs (block_lifter bi) = αb"
"sep_lifter.tyb (block_lifter bi) = (λ_. ())"
"sep_lifter.tys (block_lifter bi) = tag_of"
unfolding block_lifter_def by auto
sublocale block_lifter: sep_lifter "block_lifter bi"
proof -
have aux1[intro]: "a ## fst b ⟹ b ## (a, 0)" for a b
by (cases b) (auto simp: sep_algebra_simps )
show "sep_lifter (block_lifter bi)"
apply unfold_locales
apply (auto simp: sep_algebra_simps sep_disj_funD[where x=bi])
apply (auto
simp: lens_of_bi_def α_def listα_def optionα_alt αtag_def sep_algebra_simps
split: memory.splits if_splits option.splits
del: ext intro!: ext)
done
qed
lemma pto_null_eq[simp]: "pto x RP_NULL = sep_false" by (auto simp: pto_def)
lemma pto_addr_eq[simp]: "pto x (RP_ADDR (ADDR bi ba)) = block_lifter.lift_assn bi (bpto x ba)"
unfolding pto_def block_lifter.lift_assn_def
apply (rule ext)
apply (auto simp: sep_algebra_simps)
by (metis (no_types, hide_lams) fun_upd_same fun_upd_triv fun_upd_upd prod_Z_lower(1) surjective_pairing zero_fun_def)
fun rptr_cases where "rptr_cases (RP_NULL) = ()" | "rptr_cases (RP_ADDR (ADDR _ _)) = ()"
lemma load_rule: "notime.htriple α (pto x a) (load a) (λr. ↑(x=r) ** pto x a)"
unfolding load_def
apply (cases a rule: rptr_cases.cases; simp)
apply (rule notime.cons_post_rule)
apply (rule block_lifter.lift_operation[simplified, OF _ _ bload_rule])
apply (simp add: bpto_notZ)
apply (rule bload_pres_tag)
apply (auto simp: sep_algebra_simps pred_lift_extract_simps)
done
lemma store_rule: "notime.htriple α (pto xx a) (store x a) (λ_. pto x a)"
unfolding store_def
apply (cases a rule: rptr_cases.cases; simp)
apply (rule notime.cons_post_rule)
apply (rule block_lifter.lift_operation[simplified, OF _ _ bstore_rule])
apply (simp add: bpto_notZ)
apply (rule bstore_pres_tag)
apply (auto simp: sep_algebra_simps pred_lift_extract_simps)
done
end
subsection ‹Address Arithmetic›
term "a+b"
class addr_algebra =
fixes abase :: "'a ⇒ bool"
and acompat :: "'a ⇒ 'a ⇒ bool" (infix "~⇩a" 50)
and adiff :: "'a ⇒ 'a ⇒ int" (infix "-⇩a" 65)
and aidx :: "'a ⇒ int ⇒ 'a" (infixl "+⇩a" 65)
assumes
acompat_equiv: "part_equivp acompat"
and acompat_dom: "a⇩1 ~⇩a a⇩2 ⟹ abase a⇩1 ∧ abase a⇩2"
and aidx_Z[simp]: "a +⇩a 0 = a"
and aidx_plus[simp]: "abase a ⟹ a +⇩a i⇩1 +⇩a i⇩2 = a +⇩a (i⇩1 + i⇩2)"
and aidx_inj[simp]: "abase a ⟹ a +⇩a i = a +⇩a j ⟷ i=j"
and abase_idx[simp]: "abase (a +⇩a i) ⟷ abase a"
and adiff_same[simp]: "a -⇩a a = 0"
and aidx_compat[simp]: "abase a ⟹ a ~⇩a a+⇩ai"
and adiff_idx[simp]: "a ~⇩a b ⟹ a +⇩a (b -⇩a a) = b"
begin
lemma acompat_trans[trans]: "a ~⇩a b ⟹ b ~⇩a c ⟹ a ~⇩a c"
using acompat_equiv by (meson part_equivp_transp)
lemma acompat_sym[sym, intro]: "a ~⇩a b ⟹ b ~⇩a a"
using acompat_equiv by (meson part_equivp_symp)
lemma acompat_refl[simp]: "a ~⇩a a ⟷ abase a"
using acompat_sym acompat_trans local.acompat_dom local.aidx_compat by blast
lemma aidx_compat'[simp]:
"abase b ⟹ a ~⇩a b +⇩a i ⟷ a ~⇩a b"
"abase a ⟹ a +⇩a i ~⇩a b ⟷ a ~⇩a b"
using acompat_sym acompat_trans local.aidx_compat by blast+
lemma diff_Z_iff_eq[simp]: "a⇩1 ~⇩a a⇩2 ⟹ a⇩1 -⇩a a⇩2 = 0 ⟷ a⇩1=a⇩2"
by (metis acompat_sym acompat_trans local.adiff_idx local.adiff_same)
lemma diff_Z_iff_eq'[simp]: "a⇩2 ~⇩a a⇩1 ⟹ a⇩1 -⇩a a⇩2 = 0 ⟷ a⇩1=a⇩2"
by (metis acompat_sym acompat_trans local.adiff_idx local.adiff_same)
lemma adiff_idx'[simp]: "b ~⇩a a ⟹ a +⇩a (b -⇩a a) = b"
using acompat_sym local.adiff_idx by blast
lemma idx_diff_distrib[simp]: "p~⇩ap' ⟹ (p+⇩ai)-⇩ap' = (p-⇩ap')+i"
by (metis acompat_dom adiff_idx' aidx_compat aidx_inj aidx_plus)
lemma idx_diff_distrib'[simp]: "p'~⇩ap ⟹ (p+⇩ai)-⇩ap' = (p-⇩ap')+i"
by (metis acompat_dom adiff_idx' aidx_compat aidx_inj aidx_plus)
lemma adiff_idx_idx[simp]:
"p~⇩ap' ⟹ p +⇩a (p' -⇩a p + i) = p' +⇩a i"
"p'~⇩ap ⟹ p +⇩a (p' -⇩a p + i) = p' +⇩a i"
apply (metis acompat_dom adiff_idx aidx_plus)
by (metis acompat_dom adiff_idx' aidx_plus)
lemma acompat_dom'[simp, intro]:
"p~⇩ap' ⟹ abase p"
"p~⇩ap' ⟹ abase p'"
apply (simp_all add: acompat_dom)
done
end
instantiation rptr :: (addr_algebra) addr_algebra begin
fun abase_rptr where "abase_rptr (RP_ADDR a) ⟷ abase a" | "abase_rptr RP_NULL ⟷ False"
lemma abase_rptr_alt: "abase p ⟷ (case p of (RP_ADDR a) ⇒ abase a | RP_NULL ⇒ False)"
by (cases p; simp)
fun acompat_rptr where
"acompat_rptr (RP_ADDR a⇩1) (RP_ADDR a⇩2) ⟷ a⇩1 ~⇩a a⇩2"
| "acompat_rptr _ _ ⟷ False"
lemma acompat_rptr_alt: "p⇩1 ~⇩a p⇩2 ⟷ (case (p⇩1,p⇩2) of (RP_ADDR a⇩1, RP_ADDR a⇩2) ⇒ a⇩1 ~⇩a a⇩2 | _ ⇒ False)"
by (cases p⇩1; cases p⇩2; simp)
fun adiff_rptr where
"adiff_rptr (RP_ADDR a⇩1) (RP_ADDR a⇩2) = (a⇩1 -⇩a a⇩2)"
| "adiff_rptr (RP_NULL) (RP_NULL) = 0"
| "adiff_rptr _ _ = undefined"
lemma adiff_rptr_alt: "p⇩1 -⇩a p⇩2 = (case (p⇩1,p⇩2) of (RP_ADDR a⇩1, RP_ADDR a⇩2) ⇒ a⇩1 -⇩a a⇩2 | (RP_NULL,RP_NULL) ⇒ 0 | _ ⇒ undefined)"
by (cases p⇩1; cases p⇩2; simp)
fun aidx_rptr where
"aidx_rptr (RP_ADDR a) i = RP_ADDR (a +⇩a i)"
| "aidx_rptr RP_NULL _ = RP_NULL"
lemma aidx_rptr_alt: "p⇩1 +⇩a i = (case p⇩1 of RP_ADDR a⇩1 ⇒ RP_ADDR (a⇩1 +⇩a i) | _ ⇒ RP_NULL)"
by (cases p⇩1; simp)
lemma ptr_neq_null_conv: "p≠RP_NULL ⟷ (∃a. p=RP_ADDR a)" by (cases p) (auto)
instance
apply standard
apply (intro part_equivpI sympI transpI)
apply (meson acompat_equiv acompat_rptr.simps(1) part_equivp_def)
apply (auto
simp: acompat_rptr_alt aidx_rptr_alt adiff_rptr_alt acompat_dom
split: rptr.splits
intro!: sympI transpI reflpI
intro: acompat_sym acompat_trans)
done
end
fun rptr_the_block_index where
"rptr_the_block_index (RP_ADDR (ADDR bi _)) = bi" | "rptr_the_block_index _ = undefined"
instantiation addr :: (addr_algebra) addr_algebra begin
fun abase_addr where "abase_addr (ADDR bi ba) ⟷ abase ba"
fun acompat_addr where "ADDR bi⇩1 ba⇩1 ~⇩a ADDR bi⇩2 ba⇩2 ⟷ bi⇩1=bi⇩2 ∧ ba⇩1~⇩aba⇩2"
fun aidx_addr where "ADDR bi ba +⇩a i = ADDR bi (ba +⇩a i)"
fun adiff_addr where "ADDR bi⇩1 ba⇩1 -⇩a ADDR bi⇩2 ba⇩2 = ba⇩1 -⇩a ba⇩2"
lemma abase_addr_alt: "abase = (λ(ADDR bi ba) ⇒ abase ba)" by (intro ext) (auto split: addr.splits)
lemma acomp_addr_alt: "(~⇩a) = (λADDR bi⇩1 ba⇩1 ⇒ λADDR bi⇩2 ba⇩2 ⇒ bi⇩1=bi⇩2 ∧ ba⇩1~⇩aba⇩2)" by (intro ext) (auto split: addr.splits)
lemma aidx_addr_alt: "(+⇩a) = (λADDR bi ba ⇒ λi. ADDR bi (ba +⇩a i))" by (intro ext) (auto split: addr.splits)
lemma adiff_addr_alt: "(-⇩a) = (λADDR bi⇩1 ba⇩1 ⇒ λADDR bi⇩2 ba⇩2 ⇒ ba⇩1 -⇩a ba⇩2)" by (intro ext) (auto split: addr.splits)
instance
apply standard
apply (intro part_equivpI sympI transpI)
apply (meson acompat_equiv acompat_addr.simps(1) part_equivp_def)
apply (auto
simp: abase_addr_alt acomp_addr_alt aidx_addr_alt adiff_addr_alt acompat_dom
split: addr.splits
intro: acompat_sym acompat_trans)
done
end
end