arch_split: invariants: fixup CSpaceInv_AI, working on Finalise_AI
This commit is contained in:
Matthew Brecknell
parent
aa632d4822
commit
d683425e0d
|
|
@ -74,26 +74,34 @@ definition
|
|||
(\<exists>vref. vs_cap_ref cap = Some vref \<and> (vref \<unrhd> obj_ref_of cap) s)"
|
||||
|
||||
definition
|
||||
replaceable_arch_cap :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
|
||||
replaceable_final_arch_cap :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
|
||||
where
|
||||
"replaceable_arch_cap s sl newcap \<equiv> \<lambda>cap.
|
||||
(\<forall>vref. vs_cap_ref cap = Some vref
|
||||
\<longrightarrow> (vs_cap_ref newcap = Some vref
|
||||
\<and> obj_refs newcap = obj_refs cap)
|
||||
\<or> (\<forall>oref \<in> obj_refs cap. \<not> (vref \<unrhd> oref) s))
|
||||
\<and> no_cap_to_obj_with_diff_ref newcap {sl} s
|
||||
\<and> ((is_pt_cap newcap \<or> is_pd_cap newcap) \<longrightarrow> cap_asid newcap = None
|
||||
\<longrightarrow> (\<forall> r \<in> obj_refs newcap. obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s))
|
||||
\<and> ((is_pt_cap newcap \<or> is_pd_cap newcap)
|
||||
\<longrightarrow> ((is_pt_cap newcap \<and> is_pt_cap cap \<or> is_pd_cap newcap \<and> is_pd_cap cap)
|
||||
\<longrightarrow> (cap_asid newcap = None \<longrightarrow> cap_asid cap = None)
|
||||
\<longrightarrow> obj_refs cap \<noteq> obj_refs newcap)
|
||||
\<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs newcap
|
||||
\<and> (is_pd_cap newcap \<and> is_pd_cap cap' \<or> is_pt_cap newcap \<and> is_pt_cap cap')
|
||||
\<and> (cap_asid newcap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = sl))
|
||||
\<and> \<not>is_ap_cap newcap"
|
||||
"replaceable_final_arch_cap s sl newcap \<equiv> \<lambda>cap.
|
||||
(\<forall>vref. vs_cap_ref cap = Some vref
|
||||
\<longrightarrow> (vs_cap_ref newcap = Some vref
|
||||
\<and> obj_refs newcap = obj_refs cap)
|
||||
\<or> (\<forall>oref \<in> obj_refs cap. \<not> (vref \<unrhd> oref) s))
|
||||
\<and> no_cap_to_obj_with_diff_ref newcap {sl} s
|
||||
\<and> ((is_pt_cap newcap \<or> is_pd_cap newcap) \<longrightarrow> cap_asid newcap = None
|
||||
\<longrightarrow> (\<forall> r \<in> obj_refs newcap.
|
||||
obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s))
|
||||
\<and> ((is_pt_cap newcap \<or> is_pd_cap newcap)
|
||||
\<longrightarrow> ((is_pt_cap newcap \<and> is_pt_cap cap \<or> is_pd_cap newcap \<and> is_pd_cap cap)
|
||||
\<longrightarrow> (cap_asid newcap = None \<longrightarrow> cap_asid cap = None)
|
||||
\<longrightarrow> obj_refs cap \<noteq> obj_refs newcap)
|
||||
\<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs newcap
|
||||
\<and> (is_pd_cap newcap \<and> is_pd_cap cap' \<or> is_pt_cap newcap \<and> is_pt_cap cap')
|
||||
\<and> (cap_asid newcap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = sl))
|
||||
\<and> \<not>is_ap_cap newcap"
|
||||
|
||||
declare replaceable_arch_cap_def[simp]
|
||||
definition
|
||||
replaceable_non_final_arch_cap :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
|
||||
where
|
||||
"replaceable_non_final_arch_cap s sl newcap \<equiv> \<lambda>cap. \<not> reachable_pg_cap cap s"
|
||||
|
||||
declare
|
||||
replaceable_final_arch_cap_def[simp]
|
||||
replaceable_non_final_arch_cap_def[simp]
|
||||
|
||||
(*FIXME arch_split: These are probably subsumed by the lifting lemmas *)
|
||||
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@
|
|||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
(*
|
||||
(*
|
||||
CSpace invariants
|
||||
*)
|
||||
|
||||
|
|
@ -18,8 +18,8 @@ begin
|
|||
|
||||
unqualify_consts (in Arch)
|
||||
cap_master_arch_cap :: "arch_cap \<Rightarrow> arch_cap"
|
||||
replaceable_arch_cap :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
|
||||
reachable_pg_cap :: "cap \<Rightarrow> 'a state \<Rightarrow> bool"
|
||||
replaceable_final_arch_cap :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
|
||||
replaceable_non_final_arch_cap :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
|
||||
unique_table_refs :: "('a \<Rightarrow> cap option) \<Rightarrow> bool"
|
||||
|
||||
unqualify_facts (in Arch)
|
||||
|
|
@ -1100,18 +1100,19 @@ lemma no_cap_to_obj_with_diff_ref_Null:
|
|||
by (rule ext, clarsimp simp: no_cap_to_obj_with_diff_ref_def
|
||||
cte_wp_at_caps_of_state abj_ref_none_no_refs)
|
||||
|
||||
|
||||
|
||||
lemma "(a \<or> (\<not>b \<and> c \<and> d) \<or> (b \<and> e \<and> f)) \<longleftrightarrow> (a \<or> (if b then e else c) \<and> (if b then f else d))"
|
||||
by simp
|
||||
|
||||
definition
|
||||
replaceable :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
|
||||
where
|
||||
"replaceable s sl newcap \<equiv> \<lambda>cap.
|
||||
(cap = newcap)
|
||||
\<or> (\<not> is_final_cap' cap s \<and> newcap = cap.NullCap \<and> \<not> reachable_pg_cap cap s)
|
||||
\<or> (\<not> is_final_cap' cap s
|
||||
\<and> newcap = NullCap
|
||||
\<and> replaceable_non_final_arch_cap s sl newcap cap)
|
||||
\<or> (is_final_cap' cap s
|
||||
\<and> (\<forall>p\<in>zobj_refs cap - zobj_refs newcap.
|
||||
obj_at (Not \<circ> live) p s)
|
||||
\<and> (\<forall>p\<in>zobj_refs cap - zobj_refs newcap. obj_at (Not \<circ> live) p s)
|
||||
\<and> (\<forall>p'. p' \<in> cte_refs cap (interrupt_irq_node s)
|
||||
\<and> (p' \<notin> cte_refs newcap (interrupt_irq_node s)
|
||||
\<or> (\<exists>cp. appropriate_cte_cap cp cap
|
||||
|
|
@ -1128,9 +1129,8 @@ where
|
|||
\<and> \<not> is_untyped_cap newcap \<and> \<not> is_master_reply_cap newcap
|
||||
\<and> \<not> is_reply_cap newcap
|
||||
\<and> newcap \<noteq> cap.IRQControlCap
|
||||
\<and> (newcap \<noteq> cap.NullCap \<longrightarrow> cap_class newcap = cap_class cap))
|
||||
\<and> replaceable_arch_cap s sl newcap cap
|
||||
"
|
||||
\<and> (newcap \<noteq> cap.NullCap \<longrightarrow> cap_class newcap = cap_class cap)
|
||||
\<and> replaceable_final_arch_cap s sl newcap cap)"
|
||||
|
||||
lemma range_not_empty_is_physical:
|
||||
"valid_cap cap s \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})"
|
||||
|
|
|
|||
|
|
@ -15,6 +15,9 @@ imports
|
|||
Retype_AI
|
||||
begin
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
vs_cap_ref :: "cap \<Rightarrow> vs_ref list option"
|
||||
|
||||
text {* Properties about empty_slot *}
|
||||
|
||||
definition
|
||||
|
|
@ -215,12 +218,13 @@ lemma no_cap_to_obj_with_diff_rvk_update[simp]:
|
|||
= no_cap_to_obj_with_diff_ref cap S s"
|
||||
by (simp add: no_cap_to_obj_with_diff_ref_def)
|
||||
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma reachable_pg_cap_cdt_update[simp]:
|
||||
"reachable_pg_cap x (cdt_update f s) = reachable_pg_cap x s"
|
||||
by (simp add: reachable_pg_cap_def)
|
||||
end
|
||||
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma replaceable_cdt_update[simp]:
|
||||
"replaceable (cdt_update f s) = replaceable s"
|
||||
by (fastforce simp: replaceable_def tcb_cap_valid_def)
|
||||
|
|
@ -232,6 +236,7 @@ lemma reachable_pg_cap_is_original_cap_update[simp]:
|
|||
lemma replaceable_revokable_update[simp]:
|
||||
"replaceable (is_original_cap_update f s) = replaceable s"
|
||||
by (fastforce simp: replaceable_def is_final_cap'_def2 tcb_cap_valid_def)
|
||||
end
|
||||
|
||||
lemma zombies_final_cdt_update[simp]:
|
||||
"zombies_final (cdt_update f s) = zombies_final s"
|
||||
|
|
@ -282,22 +287,25 @@ proof -
|
|||
by (clarsimp simp: st_tcb_def2)
|
||||
qed
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma reachable_pg_cap_update[simp]:
|
||||
"reachable_pg_cap cap' (trans_state f s) = reachable_pg_cap cap' s"
|
||||
by (simp add:reachable_pg_cap_def vs_lookup_pages_def
|
||||
vs_lookup_pages1_def obj_at_def)
|
||||
end
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma replaceable_more_update[simp]:
|
||||
"replaceable (trans_state f s) sl cap cap' = replaceable s sl cap cap'"
|
||||
by (simp add: replaceable_def)
|
||||
|
||||
|
||||
(* FIXME: move *)
|
||||
lemma obj_ref_ofI: "obj_refs cap = {x} \<Longrightarrow> obj_ref_of cap = x"
|
||||
by (case_tac cap, simp_all) (rename_tac arch_cap, case_tac arch_cap, simp_all)
|
||||
lemmas obj_ref_ofI' = obj_ref_ofI[OF obj_ref_elemD]
|
||||
end
|
||||
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma vs_lookup_pages_eq:
|
||||
"\<lbrakk>valid_arch_objs s; valid_asid_table (arm_asid_table (arch_state s)) s;
|
||||
valid_cap cap s; table_cap_ref cap = Some vref; oref \<in> obj_refs cap\<rbrakk>
|
||||
|
|
@ -310,8 +318,9 @@ lemma vs_lookup_pages_eq:
|
|||
apply (simp add: valid_cap_def)
|
||||
apply (erule vs_lookup_vs_lookup_pagesI', clarsimp+)
|
||||
done
|
||||
end
|
||||
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma empty_slot_invs:
|
||||
"\<lbrace>\<lambda>s. invs s \<and> cte_wp_at (replaceable s sl cap.NullCap) sl s \<and>
|
||||
emptyable sl s \<and>
|
||||
|
|
@ -387,6 +396,7 @@ lemma empty_slot_invs:
|
|||
apply auto[1]
|
||||
apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state)
|
||||
done
|
||||
end
|
||||
|
||||
crunch cte_wp_at[wp]: deleted_irq_handler "cte_wp_at P p"
|
||||
|
||||
|
|
@ -458,10 +468,10 @@ lemma tcb_cap_cases_lt:
|
|||
by (simp add: tcb_cap_cases_def
|
||||
| erule less_handy_casesE)+
|
||||
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma nat_to_cref_unat_of_bl':
|
||||
"\<lbrakk> length xs < 32; n = length xs \<rbrakk> \<Longrightarrow>
|
||||
nat_to_cref n (unat (of_bl xs :: word32)) = xs"
|
||||
nat_to_cref n (unat (of_bl xs :: machine_word)) = xs"
|
||||
apply (simp add: nat_to_cref_def word_bits_def)
|
||||
apply (rule nth_equalityI)
|
||||
apply simp
|
||||
|
|
@ -473,12 +483,12 @@ lemma nat_to_cref_unat_of_bl':
|
|||
apply fastforce
|
||||
done
|
||||
|
||||
|
||||
lemmas nat_to_cref_unat_of_bl = nat_to_cref_unat_of_bl' [OF _ refl]
|
||||
end
|
||||
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma dom_tcb_cap_cases_lt:
|
||||
"dom tcb_cap_cases = {xs. length xs = 3 \<and> unat (of_bl xs :: word32) < 5}"
|
||||
"dom tcb_cap_cases = {xs. length xs = 3 \<and> unat (of_bl xs :: machine_word) < 5}"
|
||||
apply (rule set_eqI, rule iffI)
|
||||
apply clarsimp
|
||||
apply (simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1 split: split_if_asm)
|
||||
|
|
@ -486,7 +496,7 @@ lemma dom_tcb_cap_cases_lt:
|
|||
apply (frule tcb_cap_cases_lt)
|
||||
apply (clarsimp simp: nat_to_cref_unat_of_bl')
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
lemma cte_refs_CNode_Zombie_helper[simp]:
|
||||
"{xs. length xs = n \<and> unat (of_bl xs :: word32) < 2 ^ n}
|
||||
|
|
@ -617,7 +627,7 @@ lemma unbind_notification_cte_wp_at[wp]:
|
|||
"\<lbrace>\<lambda>s. cte_wp_at P slot s\<rbrace> unbind_notification t \<lbrace>\<lambda>rv s. cte_wp_at P slot s\<rbrace>"
|
||||
by (wp thread_set_cte_wp_at_trivial hoare_drop_imp | wpc | simp add: unbind_notification_def tcb_cap_cases_def)+
|
||||
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma unbind_notification_final[wp]:
|
||||
"\<lbrace>is_final_cap' cap\<rbrace> unbind_notification t \<lbrace> \<lambda>rv. is_final_cap' cap\<rbrace>"
|
||||
unfolding unbind_notification_def
|
||||
|
|
@ -636,7 +646,6 @@ lemma deleting_irq_handler_final:
|
|||
apply simp
|
||||
done
|
||||
|
||||
|
||||
lemma finalise_cap_cases1:
|
||||
"\<lbrace>\<lambda>s. final \<longrightarrow> is_final_cap' cap s
|
||||
\<and> cte_wp_at (op = cap) slot s\<rbrace>
|
||||
|
|
@ -667,6 +676,7 @@ lemma finalise_cap_cases1:
|
|||
apply (rule hoare_pre)
|
||||
apply (wp | wpc | simp only: simp_thms)+
|
||||
done
|
||||
end
|
||||
|
||||
|
||||
lemma finalise_cap_cases:
|
||||
|
|
@ -703,12 +713,13 @@ lemma is_final_cap'_objrefsE:
|
|||
crunch typ_at[wp]: deleting_irq_handler "\<lambda>s. P (typ_at T p s)"
|
||||
(wp:crunch_wps simp:crunch_simps unless_def assertE_def)
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
crunch typ_at[wp]: arch_finalise_cap "\<lambda>s. P (typ_at T p s)"
|
||||
(wp: crunch_wps simp: crunch_simps unless_def assertE_def
|
||||
ignore: maskInterrupt )
|
||||
end
|
||||
|
||||
context
|
||||
begin
|
||||
context begin
|
||||
declare if_cong[cong]
|
||||
crunch typ_at[wp]: finalise_cap "\<lambda>s. P (typ_at T p s)"
|
||||
end
|
||||
|
|
@ -722,6 +733,7 @@ lemma unbind_notification_valid_cap[wp]:
|
|||
unfolding unbind_notification_def
|
||||
by (wp abs_typ_at_lifts hoare_drop_imps | wpc | clarsimp)+
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma finalise_cap_new_valid_cap[wp]:
|
||||
"\<lbrace>valid_cap cap\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv. valid_cap (fst rv)\<rbrace>"
|
||||
apply (cases cap, simp_all)
|
||||
|
|
@ -736,7 +748,9 @@ lemma finalise_cap_new_valid_cap[wp]:
|
|||
apply (wp|simp add: o_def valid_cap_def cap_aligned_def
|
||||
split del: split_if|clarsimp|wpc)+
|
||||
done
|
||||
end
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma invs_arm_asid_table_unmap:
|
||||
"invs s \<and> is_aligned base asid_low_bits \<and> base \<le> mask asid_bits
|
||||
\<and> (\<forall>x\<in>set [0.e.2 ^ asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None)
|
||||
|
|
@ -748,6 +762,7 @@ lemma invs_arm_asid_table_unmap:
|
|||
apply (simp add: valid_irq_node_def valid_kernel_mappings_def
|
||||
valid_global_objs_arch_update)
|
||||
apply (simp add: valid_table_caps_def valid_machine_state_def)
|
||||
apply (simp add: valid_global_refs_def global_refs_def)
|
||||
done
|
||||
|
||||
lemma delete_asid_pool_invs[wp]:
|
||||
|
|
@ -803,10 +818,11 @@ lemma delete_asid_invs[wp]:
|
|||
apply (simp add: mask_def)
|
||||
apply blast
|
||||
done
|
||||
end
|
||||
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma arch_finalise_cap_invs[wp]:
|
||||
"\<lbrace>invs and valid_cap (cap.ArchObjectCap cap)\<rbrace>
|
||||
"\<lbrace>invs and valid_cap (ArchObjectCap cap)\<rbrace>
|
||||
arch_finalise_cap cap final
|
||||
\<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (simp add: arch_finalise_cap_def)
|
||||
|
|
@ -815,6 +831,7 @@ lemma arch_finalise_cap_invs[wp]:
|
|||
apply (clarsimp simp: valid_cap_def cap_aligned_def)
|
||||
apply (auto simp: mask_def vmsz_aligned_def)
|
||||
done
|
||||
end
|
||||
|
||||
lemma refs_in_ntfn_q_refs:
|
||||
"(x, ref) \<in> ntfn_q_refs_of ntfn \<Longrightarrow> ref = NTFNSignal"
|
||||
|
|
@ -863,7 +880,9 @@ lemma unbind_maybe_notification_invs:
|
|||
|
||||
crunch invs[wp]: fast_finalise "invs"
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
crunch invs: page_table_mapped "invs"
|
||||
end
|
||||
|
||||
lemma cnode_at_unlive[elim!]:
|
||||
"s \<turnstile> cap.CNodeCap ptr bits gd \<Longrightarrow> obj_at (\<lambda>ko. \<not> live ko) ptr s"
|
||||
|
|
@ -894,7 +913,7 @@ lemma tcb_cap_valid_imp_NullCap:
|
|||
split: Structures_A.thread_state.split_asm)
|
||||
done
|
||||
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma delete_asid_pool_unmapped[wp]:
|
||||
"\<lbrace>\<top>\<rbrace>
|
||||
delete_asid_pool asid poolptr
|
||||
|
|
@ -926,7 +945,6 @@ lemma delete_asid_pool_unmapped[wp]:
|
|||
dest!: graph_ofD)
|
||||
done
|
||||
|
||||
|
||||
lemma set_asid_pool_unmap:
|
||||
"\<lbrace>[VSRef highbits None] \<rhd> poolptr\<rbrace>
|
||||
set_asid_pool poolptr (pool(lowbits := None))
|
||||
|
|
@ -941,7 +959,6 @@ lemma set_asid_pool_unmap:
|
|||
dest!: graph_ofD)
|
||||
done
|
||||
|
||||
|
||||
lemma delete_asid_unmapped[wp]:
|
||||
"\<lbrace>\<top>\<rbrace>
|
||||
delete_asid asid pd
|
||||
|
|
@ -963,34 +980,36 @@ lemma delete_asid_unmapped[wp]:
|
|||
apply (clarsimp simp: obj_at_def vs_refs_def up_ucast_inj_eq
|
||||
dest!: graph_ofD)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
lemma a_type_arch_live:
|
||||
"a_type ko = AArch tp \<Longrightarrow> \<not> live ko"
|
||||
by (simp add: a_type_def
|
||||
split: Structures_A.kernel_object.split_asm)
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma obj_at_not_live_valid_arch_cap_strg:
|
||||
"(s \<turnstile> cap.ArchObjectCap cap \<and> aobj_ref cap = Some r)
|
||||
"(s \<turnstile> ArchObjectCap cap \<and> aobj_ref cap = Some r)
|
||||
\<longrightarrow> obj_at (\<lambda>ko. \<not> live ko) r s"
|
||||
by (clarsimp simp: valid_cap_def obj_at_def
|
||||
a_type_arch_live
|
||||
split: arch_cap.split_asm)
|
||||
end
|
||||
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma set_pt_tcb_at:
|
||||
"\<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pt a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>"
|
||||
by (clarsimp simp: simpler_set_pt_def valid_def obj_at_def)
|
||||
|
||||
|
||||
lemma set_pd_tcb_at:
|
||||
"\<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pd a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>"
|
||||
by (clarsimp simp: simpler_set_pd_def valid_def obj_at_def)
|
||||
end
|
||||
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
crunch tcb_at: unmap_page "\<lambda>s. P (ko_at (TCB tcb) t s)"
|
||||
(simp: crunch_simps wp: crunch_wps set_pt_tcb_at set_pd_tcb_at)
|
||||
|
||||
end
|
||||
|
||||
lemma pred_tcb_at_def2:
|
||||
"pred_tcb_at proj P t \<equiv> \<lambda>s. \<exists>tcb. ko_at (TCB tcb) t s \<and> P (proj (tcb_to_itcb tcb))"
|
||||
|
|
@ -999,7 +1018,7 @@ lemma pred_tcb_at_def2:
|
|||
(* sseefried: 'st_tcb_at_def2' only exists to make existing proofs go through. Can use 'pred_tcb_at_def2' instead *)
|
||||
lemmas st_tcb_at_def2 = pred_tcb_at_def2[where proj=itcb_state,simplified]
|
||||
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma unmap_page_tcb_cap_valid:
|
||||
"\<lbrace>\<lambda>s. tcb_cap_valid cap r s\<rbrace>
|
||||
unmap_page sz asid vaddr pptr
|
||||
|
|
@ -1009,7 +1028,7 @@ lemma unmap_page_tcb_cap_valid:
|
|||
apply (simp add: pred_tcb_at_def2)
|
||||
apply (wp unmap_page_tcb_at hoare_vcg_ex_lift hoare_vcg_all_lift)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
lemma imp_and_strg: "Q \<and> C \<longrightarrow> (A \<longrightarrow> Q \<and> C) \<and> C" by blast
|
||||
|
||||
|
|
@ -1018,6 +1037,7 @@ lemma cases_conj_strg: "A \<and> B \<longrightarrow> (P \<and> A) \<or> (\<not>
|
|||
|
||||
lemma and_not_not_or_imp: "(~ A & ~ B | C) = ((A | B) \<longrightarrow> C)" by blast
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma arch_finalise_cap_replaceable[wp]:
|
||||
notes strg = tcb_cap_valid_imp_NullCap
|
||||
obj_at_not_live_valid_arch_cap_strg[where cap=cap]
|
||||
|
|
@ -1058,6 +1078,7 @@ lemma arch_finalise_cap_replaceable[wp]:
|
|||
elim!: tcb_cap_valid_imp_NullCap[rule_format, rotated]
|
||||
split: cap.splits arch_cap.splits vmpage_size.splits)[1]
|
||||
done
|
||||
end
|
||||
|
||||
lemmas tcb_cap_valid_imp = mp [OF mp [OF tcb_cap_valid_imp'], rotated]
|
||||
|
||||
|
|
@ -1091,7 +1112,7 @@ lemma cnode_zombie_thread_appropriate[simp]:
|
|||
"appropriate_cte_cap cp (cap.Zombie h i j)"
|
||||
by (simp add: appropriate_cte_cap_def split: cap.splits)+
|
||||
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma deleting_irq_handler_slot_not_irq_node:
|
||||
"\<lbrace>if_unsafe_then_cap and valid_global_refs
|
||||
and cte_wp_at (\<lambda>cp. cap_irqs cp \<noteq> {}) sl\<rbrace>
|
||||
|
|
@ -1113,7 +1134,6 @@ lemma deleting_irq_handler_slot_not_irq_node:
|
|||
apply (clarsimp simp: appropriate_cte_cap_def split: cap.split_asm)
|
||||
done
|
||||
|
||||
|
||||
lemma no_cap_to_obj_with_diff_ref_finalI:
|
||||
"\<lbrakk> cte_wp_at (op = cap) p s; is_final_cap' cap s;
|
||||
obj_refs cap' = obj_refs cap \<rbrakk>
|
||||
|
|
@ -1135,7 +1155,6 @@ lemma no_cap_to_obj_with_diff_ref_finalI:
|
|||
obj_irq_refs_Int)
|
||||
done
|
||||
|
||||
|
||||
lemma suspend_no_cap_to_obj_ref[wp]:
|
||||
"\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
|
||||
suspend t
|
||||
|
|
@ -1146,6 +1165,7 @@ lemma suspend_no_cap_to_obj_ref[wp]:
|
|||
apply (clarsimp simp: table_cap_ref_simps
|
||||
dest!: obj_ref_none_no_asid[rule_format])
|
||||
done
|
||||
end
|
||||
|
||||
lemma unbind_notification_not_bound:
|
||||
"\<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = Some tcbptr) ntfnptr s
|
||||
|
|
@ -1192,6 +1212,7 @@ lemma unbind_notification_no_cap_to_obj_ref[wp]:
|
|||
apply (wp unbind_notification_caps_of_state)
|
||||
done
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma finalise_cap_replaceable:
|
||||
"\<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s
|
||||
\<and> cte_wp_at (op = cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
|
||||
|
|
@ -1243,6 +1264,7 @@ lemma finalise_cap_replaceable:
|
|||
obj_irq_refs_subset vs_cap_ref_def)+
|
||||
apply (fastforce split: option.splits vmpage_size.splits)
|
||||
done
|
||||
end
|
||||
|
||||
lemma empty_slot_cte_wp_elsewhere:
|
||||
"\<lbrace>(\<lambda>s. cte_wp_at P p s) and K (p \<noteq> p')\<rbrace> empty_slot p' opt \<lbrace>\<lambda>rv s. cte_wp_at P p s\<rbrace>"
|
||||
|
|
@ -1274,7 +1296,7 @@ lemma cap_delete_one_cte_wp_at_preserved:
|
|||
apply (clarsimp simp: cte_wp_at_caps_of_state x)
|
||||
done
|
||||
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma deleting_irq_handler_cte_preserved:
|
||||
assumes x: "\<And>cap flag. P cap \<Longrightarrow> \<not> can_fast_finalise cap"
|
||||
shows "\<lbrace>cte_wp_at P p\<rbrace> deleting_irq_handler irq \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>"
|
||||
|
|
@ -1282,9 +1304,9 @@ lemma deleting_irq_handler_cte_preserved:
|
|||
apply (wp cap_delete_one_cte_wp_at_preserved | simp add: x)+
|
||||
done
|
||||
|
||||
|
||||
crunch cte_wp_at[wp]: arch_finalise_cap "\<lambda>s. P (cte_wp_at P' p s)"
|
||||
(simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at)
|
||||
end
|
||||
|
||||
|
||||
interpretation delete_one_pre
|
||||
|
|
@ -1407,7 +1429,7 @@ lemma fast_finalise_emptyable[wp]:
|
|||
apply (wp unbind_maybe_notification_invs hoare_drop_imps | simp add: o_def | wpc)+
|
||||
done
|
||||
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma cap_delete_one_invs[wp]:
|
||||
"\<lbrace>invs and emptyable ptr\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (simp add: cap_delete_one_def unless_def is_final_cap_def)
|
||||
|
|
@ -1416,6 +1438,7 @@ lemma cap_delete_one_invs[wp]:
|
|||
apply clarsimp
|
||||
apply (drule cte_wp_at_valid_objs_valid_cap, fastforce+)
|
||||
done
|
||||
end
|
||||
|
||||
lemma cap_delete_one_deletes[wp]:
|
||||
"\<lbrace>\<top>\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = cap.NullCap) ptr\<rbrace>"
|
||||
|
|
|
|||
|
|
@ -2638,21 +2638,11 @@ interpretation arch_update:
|
|||
by unfold_locales auto
|
||||
sublocale Arch \<subseteq> arch_update: Arch_pspace_update_eq "arch_state_update f" by unfold_locales
|
||||
|
||||
interpretation more_update':
|
||||
pspace_int_update_eq "trans_state f"
|
||||
by unfold_locales auto
|
||||
sublocale Arch \<subseteq> more_update': Arch_pspace_update_eq "trans_state f" by unfold_locales
|
||||
|
||||
interpretation irq_node_update_arch:
|
||||
p_arch_update_eq "interrupt_irq_node_update f"
|
||||
by unfold_locales auto
|
||||
sublocale Arch \<subseteq> irq_node_update_arch: Arch_p_arch_update_eq "interrupt_irq_node_update f" by unfold_locales
|
||||
|
||||
interpretation more_update_arch:
|
||||
p_arch_update_eq "trans_state f"
|
||||
by unfold_locales auto
|
||||
sublocale Arch \<subseteq> more_update_arch: Arch_p_arch_update_eq "trans_state f" by unfold_locales
|
||||
|
||||
|
||||
lemma obj_ref_in_untyped_range:
|
||||
"\<lbrakk> is_untyped_cap c; cap_aligned c \<rbrakk> \<Longrightarrow> obj_ref_of c \<in> untyped_range c"
|
||||
|
|
@ -2978,15 +2968,6 @@ lemma zombies_final_more_update [iff]:
|
|||
"zombies_final (trans_state f s) = zombies_final s"
|
||||
by (simp add: zombies_final_def is_final_cap'_def)
|
||||
|
||||
lemma state_refs_arch_update [iff]:
|
||||
"state_refs_of (arch_state_update f s) = state_refs_of s"
|
||||
by (simp add: state_refs_of_def)
|
||||
|
||||
lemma valid_global_refs_more_update[iff]:
|
||||
"valid_global_refs (trans_state f s) = valid_global_refs s"
|
||||
by (rule more_update.valid_global_refs_update)
|
||||
|
||||
|
||||
lemma valid_ioc_arch_state_update[iff]:
|
||||
"valid_ioc (arch_state_update f s) = valid_ioc s"
|
||||
by (simp add: valid_ioc_def)
|
||||
|
|
|
|||
|
|
@ -317,6 +317,7 @@ lemma get_epq_sp:
|
|||
apply (wp|simp)+
|
||||
done
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
|
||||
crunch v_ker_map[wp]: set_endpoint "valid_kernel_mappings"
|
||||
(ignore: set_object wp: set_object_v_ker_map crunch_wps)
|
||||
|
|
@ -324,18 +325,7 @@ crunch v_ker_map[wp]: set_endpoint "valid_kernel_mappings"
|
|||
crunch eq_ker_map[wp]: set_endpoint "equal_kernel_mappings"
|
||||
(ignore: set_object wp: set_object_equal_mappings crunch_wps)
|
||||
|
||||
|
||||
lemma set_endpoint_global_pd_mappings[wp]:
|
||||
"\<lbrace>valid_global_pd_mappings\<rbrace>
|
||||
set_endpoint p val
|
||||
\<lbrace>\<lambda>rv. valid_global_pd_mappings\<rbrace>"
|
||||
apply (simp add: set_endpoint_def)
|
||||
apply (wp get_object_wp set_object_global_pd_mappings)
|
||||
apply (clarsimp simp: obj_at_def a_type_def
|
||||
split: Structures_A.kernel_object.split_asm
|
||||
arch_kernel_obj.splits)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
lemma set_ep_cap_refs_in_kernel_window [wp]:
|
||||
"\<lbrace>cap_refs_in_kernel_window\<rbrace> set_endpoint ep p \<lbrace>\<lambda>_. cap_refs_in_kernel_window\<rbrace>"
|
||||
|
|
@ -357,14 +347,6 @@ lemma set_endpoint_valid_ioc[wp]:
|
|||
done
|
||||
|
||||
|
||||
lemma set_endpoint_vms[wp]:
|
||||
"\<lbrace>valid_machine_state\<rbrace> set_endpoint p q \<lbrace>\<lambda>rv. valid_machine_state\<rbrace>"
|
||||
apply (simp add: valid_machine_state_def in_user_frame_def)
|
||||
apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift hoare_vcg_ex_lift)
|
||||
apply (simp add: set_endpoint_def)
|
||||
apply (wp hoare_drop_imps)
|
||||
done
|
||||
|
||||
lemma refs_in_tcb_bound_refs:
|
||||
"(x, ref) \<in> tcb_bound_refs ntfn \<Longrightarrow> ref = TCBBound"
|
||||
by (auto simp: tcb_bound_refs_def split: option.splits)
|
||||
|
|
|
|||
|
|
@ -114,7 +114,7 @@ lemma dmo_kheap_arch_state[wp]:
|
|||
by (clarsimp simp: do_machine_op_def simpler_gets_def select_f_def
|
||||
simpler_modify_def return_def bind_def valid_def)
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma set_vm_root_kheap_arch_state[wp]:
|
||||
"\<lbrace>\<lambda>s. P (kheap s) (arm_globals_frame (arch_state s))\<rbrace> set_vm_root a
|
||||
\<lbrace>\<lambda>_ s. P (kheap s) (arm_globals_frame (arch_state s))\<rbrace>" (is "valid ?P _ _")
|
||||
|
|
@ -128,14 +128,18 @@ lemma set_vm_root_kheap_arch_state[wp]:
|
|||
apply (wp | simp add: returnOk_def validE_E_def validE_def)+
|
||||
apply (wp | simp add: throwError_def validE_R_def validE_def)+
|
||||
done
|
||||
end
|
||||
|
||||
context ARM begin (*FIXME: arch_split*)
|
||||
lemma clearExMonitor_invs [wp]:
|
||||
"\<lbrace>invs\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_. invs\<rbrace>"
|
||||
apply (wp dmo_invs)
|
||||
apply (clarsimp simp: clearExMonitor_def machine_op_lift_def
|
||||
machine_rest_lift_def in_monad select_f_def)
|
||||
done
|
||||
end
|
||||
|
||||
context begin interpretation ARM . (*FIXME: arch_split*)
|
||||
lemma arch_stt_invs [wp]:
|
||||
"\<lbrace>invs\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace>"
|
||||
apply (simp add: arch_switch_to_thread_def)
|
||||
|
|
@ -181,7 +185,7 @@ lemma stt_invs [wp]:
|
|||
apply (clarsimp simp: invs_def valid_state_def valid_idle_def
|
||||
valid_irq_node_def valid_machine_state_def)
|
||||
apply (fastforce simp: cur_tcb_def obj_at_def
|
||||
elim: valid_pspace_eqI ifunsafe_pspaceI)
|
||||
elim: valid_pspace_eqI ifunsafe_pspaceI)
|
||||
apply wp
|
||||
apply clarsimp
|
||||
apply (simp add: is_tcb_def)
|
||||
|
|
@ -290,6 +294,4 @@ lemma schedule_ct_activateable[wp]:
|
|||
done
|
||||
qed
|
||||
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue