Theory Sep_Array_Block_RS
section ‹Array-Blocks --- Reasoning Setup›
theory Sep_Array_Block_RS
imports "../basic/LLVM_Basic_Main" Sep_Block_Allocator_RS
begin
type_synonym 'aval ablock = "nat ⇒ 'aval"
instantiation baddr :: (this_addr) addr_algebra begin
definition "abase ≡ λBADDR i va ⇒ va=this_addr"
definition "(~⇩a) ≡ λBADDR i1 va1 ⇒ λBADDR i2 va2 ⇒ va1=this_addr ∧ va2=this_addr"
definition "(-⇩a) ≡ λBADDR i1 va1 ⇒ λBADDR i2 va2 ⇒ i1 - i2"
definition "(+⇩a) ≡ λBADDR i va ⇒ λj. BADDR (i+j) va"
lemma abase_baddr_simp[simp]: "abase (BADDR i va) ⟷ va=this_addr"
by (simp add: abase_baddr_def)
lemma acompat_baddr_simp[simp]: "BADDR i1 va1 ~⇩a BADDR i2 va2 ⟷ va1=this_addr ∧ va2=this_addr"
by (simp add: acompat_baddr_def)
lemma adiff_baddr_simp[simp]: "BADDR i1 va1 -⇩a BADDR i2 va2 = i1 - i2"
by (simp add: adiff_baddr_def)
lemma aidx_baddr_simp[simp]: "BADDR i va +⇩a j = BADDR (i+j) va"
by (simp add: aidx_baddr_def)
instance
apply standard
apply (intro part_equivpI sympI transpI)
apply (auto
simp: abase_baddr_def acompat_baddr_def adiff_baddr_def aidx_baddr_def
split: baddr.splits)
done
end
locale array_block2 = array_block1 static_err mem_err vload vstore vgep
for static_err :: 'err
and mem_err :: 'err
and vload :: "'vaddr::this_addr ⇒ ('val,_,_,'val,'err) M"
and vstore :: "'val ⇒ 'vaddr ⇒ (unit,_,_,'val,'err) M"
and vgep :: "'vaddr ⇒ 'vidx ⇒ ('vaddr,_,_,'val,'err) M"
+ fixes αv :: "'val ⇒ 'aval::unique_zero_sep_algebra"
and vpto :: "'val ⇒ 'vaddr ⇒ 'aval ⇒ bool"
and vcomplete :: "'aval ⇒ bool"
assumes vload_rule: "notime.htriple αv (vpto x va) (vload va) (λr. ↑(r=x) ** vpto x va)"
and vstore_rule: "notime.htriple αv (vpto xx va) (vstore x va) (λ_. vpto x va)"
and vpto_notZ: "⋀x a. ¬vpto x a 0"
and vcompleteD: "⋀v v'. ⟦vcomplete v; v##v'⟧ ⟹ v'=0"
and vpto_this: "⋀v av. vpto v this_addr av ⟷ av = αv v"
and αv_complete: "⋀v. vcomplete (αv v)"
begin
definition is_block_ptr :: "'vaddr baddr addr rptr ⇒ bool"
where "is_block_ptr ≡ λRP_ADDR (ADDR bi ba) ⇒ ba=this_addr | _ ⇒ False"
lemma is_block_ptr_simps[simp]:
"¬is_block_ptr RP_NULL"
"is_block_ptr (RP_ADDR (ADDR bi ba)) ⟷ ba=this_addr"
by (auto simp: is_block_ptr_def)
lemma block_ptr_imp_abase[simp, intro]: "is_block_ptr p ⟹ abase p"
by (auto simp: is_block_ptr_def this_addr_baddr_def split: rptr.splits addr.splits)
lemma αv_notZ[simp]: "αv v ≠ 0"
using vpto_notZ vpto_this by fastforce
definition "α ≡ listα αv"
definition pto :: "'val ⇒ 'vaddr baddr ⇒ 'aval ablock ⇒ bool"
where "pto ≡ λx. λBADDR i va ⇒ λs. ∃v. i≥0 ∧ s=0(nat i:=v) ∧ vpto x va v"
definition tag_of :: "'val block ⇒ int" where "tag_of ≡ int o length"
definition "is_complete_tag ablk n ≡ 0≤n ∧ (∀i. (ablk i ≠ 0 ⟷ i<nat n) ∧ (∀i. ablk i ≠ 0 ⟶ vcomplete (ablk i)))"
definition "array_lifter i ≡ idx_lifter (λ_. ()) αv i"
lemma array_lifter_simps[simp]:
"sep_lifter.αs (array_lifter i) = αv"
"sep_lifter.αb (array_lifter i) = α"
"sep_lifter.L (array_lifter i) = idx⇩L i"
unfolding array_lifter_def α_def by auto
interpretation array_lifter: sep_lifter "array_lifter i" for i
unfolding array_lifter_def by simp
lemma pto_is_lift: "pto x = (λBADDR i va ⇒ (↑(i≥0) ** array_lifter.lift_assn (nat i) (vpto x va)))"
unfolding array_lifter.lift_assn_def
apply (rule ext)
apply (clarsimp simp: array_lifter_def pto_def split: baddr.splits)
apply (intro ext)
apply (auto simp: sep_algebra_simps pred_lift_extract_simps)
by (metis fun_upd_triv fun_upd_upd)
lemma lift_is_pto: "i≥0 ⟹ array_lifter.lift_assn (nat i) (vpto x va) = pto x (BADDR i va)"
by (simp add: pto_is_lift sep_algebra_simps pred_lift_extract_simps)
declare vpto_notZ[simp]
lemma load_rule: "notime.htriple α (pto x va) (load va) (λr. ↑(r=x) ** pto x va)"
unfolding load_def
supply pto_is_lift[simp]
apply (cases va; clarsimp simp: notime.htriple_extract_pre_pure sep_algebra_simps)
using array_lifter.lift_operation[simplified, OF _ vload_rule, simplified]
.
lemma store_rule: "notime.htriple α (pto xx va) (store x va) (λ_. pto x va)"
unfolding store_def
supply pto_is_lift[simp]
apply (cases va; clarsimp simp: notime.htriple_extract_pre_pure sep_algebra_simps)
using array_lifter.lift_operation[simplified, OF _ vstore_rule, simplified]
.
lemma load_pres_tag: "wlp (load a) (λ_ s'. tag_of s' = tag_of s) s"
unfolding load_def
apply (auto simp: wlp_def run_simps tag_of_def split: prod.splits option.splits baddr.splits)
apply (rule mwp_trivI)
by auto
lemma store_pres_tag: "wlp (store a x) (λ_ s'. tag_of s' = tag_of s) s"
unfolding store_def
apply (auto simp: wlp_def run_simps tag_of_def split: prod.splits option.splits baddr.splits)
apply (rule mwp_trivI)
by auto
lemma complete_tag:
"⟦is_complete_tag ablock (tag_of cblock); ablock ## f; α cblock = ablock + f⟧ ⟹ f = 0"
apply (auto simp: is_complete_tag_def tag_of_def)
by (smt α_def disjoint_zero_sym listα_in_range sep_add_disj_eq sep_disj_fun_def sep_disj_zero unique_zero vcompleteD)
lemma Z_upd_eq_Z_iff[simp]: "0(i:=x) = 0 ⟷ x=0" by (auto simp: fun_eq_iff)
lemma pto_notZ: "¬ pto x a 0"
apply (cases a)
apply (auto simp: pto_def sep_algebra_simps)
done
lemma checked_idx_baddr_rule: "abase a
⟹ notime.htriple α (pto xx (a +⇩a i)) (checked_idx_baddr a i) (λr. ↑(r=a +⇩a i) ** pto xx (a +⇩a i))"
apply (rule notime.htripleI')
unfolding checked_idx_baddr_def check_addr_def pto_is_lift
apply (clarsimp simp: pred_lift_extract_simps split: baddr.splits)
apply (frule (1) array_lifter.infer_pre_get_with_frame, simp, simp)
apply (force simp: wpn_def run_simps aidx_baddr_def abase_baddr_def sep_algebra_simps split: prod.splits baddr.splits)
done
sublocale ba: block_allocator2 static_err mem_err load store check_addr α pto tag_of is_complete_tag
apply unfold_locales
apply (rule load_rule)
apply (rule store_rule)
apply (rule load_pres_tag)
apply (rule store_pres_tag)
apply (rule complete_tag; assumption)
apply (rule pto_notZ)
done
lemma listα_rep_nn: "listα αv (replicate n v) n = 0"
by (auto simp: listα_def)
lemma pto_this_exact: "pto x (BADDR i this_addr) = (↑(i≥0) ** EXACT (0(nat i:=αv x)))"
by (auto simp: pto_def vpto_this pred_lift_extract_simps del: ext intro!: ext)
lemma ba_pto_this_exact:
"⟦is_block_ptr p; i≥0⟧
⟹ ba.pto x (p +⇩a i) = EXACT (0(rptr_the_block_index p := (0(nat i:=αv x),0)))"
apply (auto
simp: ba.pto_def aidx_baddr_def pto_this_exact this_addr_baddr_def
simp: pred_lift_extract_simps is_block_ptr_def
split: rptr.splits addr.splits baddr.splits)
done
lemma lift_pto_exact: "i≥0 ⟹ ba.block_lifter.lift_assn bi (pto v (this_addr +⇩a i)) = EXACT (0(bi := (0(nat i:=αv v),0)))"
apply (auto
simp: aidx_baddr_def pto_this_exact this_addr_baddr_def
simp: pred_lift_extract_simps is_block_ptr_def
split: rptr.splits addr.splits baddr.splits)
done
lemma atLeast_lessThan_plus1:
"l≤v ⟹ {l..<1+v::int} = insert v {l..<v}"
"l≤v ⟹ {l..<v+1::int} = insert v {l..<v}"
by auto
lemma sep_set_img_int_range_to_nat: "(⋃*i∈{0..<int n}. f i) = (⋃*i∈{0..<n}. f (int i))"
apply (induction n)
apply (auto simp: atLeast_lessThan_plus1 atLeast0_lessThan_Suc)
done
lemma ba_block_alt:
"ba.block (α (init v n)) p = (↑(is_block_ptr p) ** (⋃*i∈{0..<int n}. ba.pto v (p +⇩a i)))"
proof -
have ba_block_alt_aux: "(⋃*i∈{0..<int n}. EXACT (0(x1 := (0(nat i := αv v), 0)))) = EXACT (0(x1 := (listα αv (replicate n v), 0)))"
for x1::nat
apply (induction n)
supply replicate_Suc_conv_snoc[simp] replicate_Suc[simp del]
subgoal by (auto simp: sep_algebra_simps del: ext intro!: ext)
subgoal
apply simp
by (auto
simp: listα_snoc sep_algebra_simps sep_disj_fun_def atLeast0_lessThan_Suc atLeast_lessThan_plus1 sep_conj_def listα_rep_nn
cong del: if_cong
del: ext intro!: ext)
done
have foo: "⟦P=Q; Q ⟹ X=Y⟧ ⟹ (↑P**X) = (↑Q**Y)" for P Q X Y by auto
have [simp]: "(⋃*x∈{0..<int n}. ba.pto v ((RP_ADDR (ADDR x1 (this_addr +⇩a x)))))
= (⋃*x∈{0..<int n}. EXACT (0(x1 := (0(nat x := αv v), 0))))" for x1
apply (rule sep_set_img_cong)
apply (auto simp: lift_pto_exact)
done
note [simp del] = ba.pto_addr_eq
show ?thesis
unfolding init_def ba.block_def
by (auto
split: rptr.splits addr.splits
simp: sep_algebra_simps
simp: α_def ba_block_alt_aux
intro!: foo
)
qed
lemma ba_block_exs_alt_aux:
assumes "n≥0"
shows "(⋃*i∈{0..<n}. (EXS x. ba.pto x ((RP_ADDR (ADDR bi (this_addr +⇩a i))))))
= (EXS xs. ↑(int (length xs) = n) ** EXACT (0(bi := (listα αv xs, 0))))"
using assms
proof (induction n rule: int_induct[where k=0])
case base
then show ?case by (auto simp: sep_algebra_simps pred_lift_extract_simps del: ext intro!: ext)
next
case (step1 n)
note [simp] = ‹0≤n›
note IH = step1.IH[simplified]
have [simp]: "n+1≠0" using ‹0≤n› by linarith
note replicate_Suc_conv_snoc[simp] replicate_Suc[simp del]
show ?case
apply (simp add: atLeast_lessThan_plus1)
apply (simp add: IH)
apply (rule ext)
apply (auto simp: sep_algebra_simps pred_lift_extract_simps sep_disj_fun_def sep_conj_def listα_at_len lift_pto_exact)
subgoal for x xs
apply (rule exI[where x="xs@[x]"])
apply (auto del: ext intro!: ext simp: listα_snoc sep_algebra_simps listα_at_len
simp: this_addr_baddr_def pto_this_exact
)
done
subgoal for xs
apply (rule exI[where x="last xs"])
apply (rule exI[where x="butlast xs"]; simp)
apply (cases xs rule: rev_cases)
apply (auto simp: listα_gt_len sep_algebra_simps listα_snoc del: ext intro!: ext)
done
done
next
case (step2 n) thus ?case by (auto)
qed
lemma ba_block_exs_alt:
"⟦is_block_ptr p; n≥0⟧ ⟹ (⋃*i∈{0..<n}. EXS v. ba.pto v (p +⇩a i)) = (EXS blk. ↑(int (length blk) = n) ** ba.block (α blk) p)"
unfolding init_def ba.block_def
supply [simp del] = ba.pto_addr_eq
apply (cases p rule: ba.rptr_cases.cases; simp)
apply (rule ext)
apply (auto
split: rptr.splits addr.splits
simp: sep_algebra_simps pred_lift_extract_simps α_def ba_block_exs_alt_aux
)
done
lemma tag_of_init[simp]: "tag_of (init v n) = int n" by (auto simp: tag_of_def init_def)
lemma ba_allocn_rule: "notime.htriple ba.α □ (ba_allocn v n) (λr. (⋃*i∈{0..<int n}. ba.pto v (r +⇩a i)) ** ba.tag (int n) r ** ↑(abase r))"
unfolding ba_allocn_def
apply (rule notime.cons_rule[OF ba.alloc_rule])
apply simp
apply (simp add: ba_block_alt sep_algebra_simps pred_lift_extract_simps)
done
lemma blk_complete_tag[simp]: "is_complete_tag (α blk) (int (length blk))"
by (auto simp: is_complete_tag_def α_def listα_def αv_complete)
lemma ba_tag_extr_baseptr: "ba.tag n p = (↑(is_block_ptr p ∧ 0≤n) ** ba.tag n p)"
apply (rule ext)
apply (auto simp: ba.tag_def sep_algebra_simps pred_lift_extract_simps split: addr.splits rptr.splits)
apply (auto simp: tag_of_def)
done
lemma ba_freen_rule: "notime.htriple ba.α ((⋃*i∈{0..<n}. EXS v. ba.pto v (p+⇩ai)) ∧* ba.tag n p) (ba.free p) (λ_. □)"
apply (subst ba_tag_extr_baseptr)
apply (rule notime.htripleI')
apply (clarsimp simp: sep_algebra_simps pred_lift_extract_simps)
apply (simp add: ba_block_exs_alt)
apply (clarsimp simp: sep_algebra_simps pred_lift_extract_simps)
subgoal for pp s f blk
supply R = ba.free_rule[of "α blk" p "int (length blk)"]
apply (rule R[THEN notime.htripleD', THEN notime.wp_monoI])
apply assumption+
apply (simp add: sep_algebra_simps)
apply (simp add: sep_algebra_simps)
done
done
lemma checked_idx_baddr_pres_tag: "wlp (checked_idx_baddr (BADDR a b) i) (λ_ s'. tag_of s' = tag_of sa) sa"
by (auto simp: wlp_def checked_idx_baddr_def check_addr_def run_simps split: prod.splits baddr.splits)
lemma checked_idx_ptr_rule: "abase p
⟹ notime.htriple ba.α (ba.pto xx (p +⇩a i)) (checked_idx_ptr p i) (λr. ↑(r=p +⇩a i) ** ba.pto xx (p +⇩a i))"
unfolding checked_idx_ptr_def
apply (cases p rule: ba.rptr_cases.cases; simp add: zoom_bind)
supply [vcg_rules] = ba.block_lifter.lift_operation[simplified, OF _ _ checked_idx_baddr_rule]
supply [vcg_rules] = ba.block_lifter.lift_operation[simplified, OF _ _ notime_return_rule]
supply [simp] = pto_notZ checked_idx_baddr_pres_tag abase_baddr_def
supply [named_ss fri_prepare_simps] = aidx_baddr_simp
supply [split] = baddr.splits
apply vcg
done
end
end