adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

arch_split: invariants: Finalise_AI checking

This commit is contained in:
Matthew Brecknell 2016-04-15 15:11:32 +10:00
parent d683425e0d
commit 4e6369f86d
4 changed files with 187 additions and 191 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

370
proof/invariant-abstract/Finalise_AI.thy
View File

File diff suppressed because it is too large Load Diff

2
proof/invariant-abstract/Invariants_AI.thy
View File

@ -2968,6 +2968,8 @@ 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)
lemmas state_refs_arch_update [iff] = arch_update.state_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)

4
proof/invariant-abstract/KHeap_AI.thy
View File

@ -599,14 +599,14 @@ lemma swp_apply [simp]:
"swp f x y = f y x" by (simp add: swp_def)
lemma hoare_cte_wp_caps_of_state_lift:
assumes c: "\<And>P p. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (caps_of_state s)\<rbrace>"
assumes c: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (caps_of_state s)\<rbrace>"
shows "\<lbrace>\<lambda>s. cte_wp_at P p s\<rbrace> f \<lbrace>\<lambda>r s. cte_wp_at P p s\<rbrace>"
apply (simp add: cte_wp_at_caps_of_state)
apply (rule c)
done
lemma valid_mdb_lift:
assumes c: "\<And>P p. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (caps_of_state s)\<rbrace>"
assumes c: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (caps_of_state s)\<rbrace>"
assumes m: "\<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> f \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>"
assumes r: "\<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> f \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace>"
shows "\<lbrace>valid_mdb\<rbrace> f \<lbrace>\<lambda>r. valid_mdb\<rbrace>"

2
proof/refine/Finalise_R.thy
View File

@ -4034,7 +4034,7 @@ lemma arch_recycle_cap_corres:
apply (wp cteCaps_of_ctes_of_lift mapM_storePTE_invs
mapM_wp' cteCaps_of_ctes_of_lift hoare_vcg_all_lift
| simp add: swp_def)+
apply (clarsimp simp: invs_pspace_alignedI valid_cap_def)
apply (clarsimp simp: invs_psp_aligned valid_cap_def)
apply (intro conjI)
apply (clarsimp simp: upto_enum_step_def)
apply (erule page_table_pte_atI[simplified shiftl_t2n mult.commute mult.left_commute,simplified])