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

x64 ainvs: update for PageMap replacing PageRemap (SELFOUR-161)

This commit is contained in:
Victor Phan 2019-09-25 17:19:20 +10:00
parent 10127117ee
commit 89510ac172
2 changed files with 219 additions and 214 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

135
proof/invariant-abstract/X64/ArchArch_AI.thy
View File

@ -962,7 +962,7 @@ lemma sts_valid_slots_inv[wp]:
lemma sts_valid_page_inv[wp]:
"\<lbrace>valid_page_inv page_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv page_invocation\<rbrace>"
by (cases page_invocation,
(wp hoare_vcg_const_Ball_lift hoare_vcg_ex_lift hoare_vcg_imp_lift sts_typ_ats
(wp hoare_vcg_ex_lift hoare_vcg_disj_lift sts_typ_ats
| clarsimp simp: valid_page_inv_def same_refs_def
| wps)+)
@ -1301,20 +1301,38 @@ lemma find_vspace_for_asid_lookup_vspace_wp:
apply (simp | fast)+
done
lemma aligned_sum_less_kernel_base:
"vmsz_aligned p sz
\<Longrightarrow> (p + 2 ^ pageBitsForSize sz - 1 < kernel_base) = (p < kernel_base)"
lemma aligned_sum_less:
fixes p :: "'a::len word"
shows "\<lbrakk> is_aligned p sz; is_aligned q sz; sz < LENGTH('a) \<rbrakk>
\<Longrightarrow> (p + 2 ^ sz - 1 < q) = (p < q)"
apply (rule iffI)
apply (rule le_less_trans)
apply (rule is_aligned_no_overflow)
apply (simp add: vmsz_aligned_def)
apply simp
apply (simp add:field_simps[symmetric])
apply (erule gap_between_aligned)
apply (simp add: vmsz_aligned_def)+
apply (case_tac sz; simp add: kernel_base_def bit_simps is_aligned_def)+
apply (simp add: field_simps[symmetric])
apply (erule gap_between_aligned; simp add: vmsz_aligned_def)
done
lemma aligned_sum_le:
fixes p :: "'a::len word"
shows "\<lbrakk> is_aligned p sz; is_aligned (q+1) sz; 0 < sz; sz < LENGTH('a) \<rbrakk>
\<Longrightarrow> (p + 2 ^ sz - 1 \<le> q) = (p \<le> q)"
using aligned_sum_less[where q="q+1"]
by (case_tac "q = max_word"; simp add: word_Suc_leq)
lemma aligned_sum_less_kernel_base:
"vmsz_aligned p sz \<Longrightarrow> (p + 2 ^ pageBitsForSize sz - 1 < kernel_base) = (p < kernel_base)"
by (cases sz
; rule aligned_sum_less
; simp add: vmsz_aligned_def kernel_base_def bit_simps is_aligned_def)
lemma aligned_sum_le_user_vtop:
"vmsz_aligned p sz \<Longrightarrow> (p + 2 ^ pageBitsForSize sz - 1 \<le> user_vtop) = (p \<le> user_vtop)"
by (cases sz
; rule aligned_sum_le
; simp add: vmsz_aligned_def user_vtop_def pptrUserTop_def bit_simps is_aligned_def)
lemma pml4e_at_shifting_magic:
"\<lbrakk>ako_at (PageMapL4 pm) xa s; is_aligned xa pml4_bits\<rbrakk> \<Longrightarrow>
pml4e_at (xa + (get_pml4_index (args ! 0 && ~~ mask pml4_shift_bits) << word_size_bits)) s"
@ -1362,52 +1380,55 @@ lemma decode_page_invocation_wf[wp]:
apply (cases "invocation_type label = ArchInvocationLabel X64PageMap")
apply (simp split del: if_split)
apply (rule hoare_pre)
apply ((wp whenE_throwError_wp check_vp_wpR hoare_vcg_const_imp_lift_R
create_mapping_entries_parent_for_refs find_vspace_for_asid_vspace_at_asid
create_mapping_entries_valid_slots create_mapping_entries_same_refs_ex
find_vspace_for_asid_lookup_vspace_wp
| wpc
| simp add: valid_arch_inv_def valid_page_inv_def is_pg_cap_def)+)
apply (clarsimp simp: neq_Nil_conv invs_vspace_objs)
apply (frule diminished_cte_wp_at_valid_cap[where p="(a, b)" for a b], clarsimp)
apply (frule diminished_cte_wp_at_valid_cap[where p=slot], clarsimp)
apply (clarsimp simp: cte_wp_at_caps_of_state mask_cap_def
diminished_def[where cap="ArchObjectCap (PageCap d x y t z w)" for d x y t z w]
linorder_not_le aligned_sum_less_kernel_base
dest!: diminished_pm_capD)
apply (clarsimp simp: cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits)
apply (auto,
auto simp: cte_wp_at_caps_of_state invs_def valid_state_def
valid_cap_simps is_arch_update_def
is_arch_cap_def cap_master_cap_simps
vs_cap_ref_def cap_aligned_def bit_simps data_at_def
vmsz_aligned_def
split: vmpage_size.split if_splits,
(fastforce intro: diminished_pm_self)+)[1]
apply (cases "invocation_type label = ArchInvocationLabel X64PageRemap")
apply (simp split del: if_split)
apply (rule hoare_pre)
apply ((wp whenE_throwError_wp check_vp_wpR hoare_vcg_const_imp_lift_R
create_mapping_entries_parent_for_refs
find_vspace_for_asid_lookup_vspace_wp
| wpc
| simp add: valid_arch_inv_def valid_page_inv_def
| (simp add: cte_wp_at_caps_of_state,
wp create_mapping_entries_same_refs_ex hoare_vcg_ex_lift_R))+)[1]
apply (clarsimp simp: valid_cap_simps cap_aligned_def neq_Nil_conv)
apply (frule diminished_cte_wp_at_valid_cap[where p="(a, b)" for a b], clarsimp)
apply (clarsimp simp: cte_wp_at_caps_of_state mask_cap_def
diminished_def[where cap="ArchObjectCap (PageCap d x y t z w)" for d x y t z w])
apply (clarsimp simp: cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits)
apply (cases slot,
auto simp: vmsz_aligned_def mask_def
valid_arch_caps_def cte_wp_at_caps_of_state
neq_Nil_conv invs_def valid_state_def
valid_cap_def cap_aligned_def data_at_def bit_simps
split: if_splits,
fastforce+)[1]
apply (wpsimp wp: whenE_throwError_wp check_vp_wpR hoare_vcg_const_imp_lift_R
hoare_vcg_disj_lift_R hoare_vcg_conj_lift_R create_mapping_entries_parent_for_refs
hoare_vcg_ex_lift_R find_vspace_for_asid_vspace_at_asid
create_mapping_entries_valid_slots create_mapping_entries_same_refs_ex
find_vspace_for_asid_lookup_vspace_wp
simp: valid_arch_inv_def valid_page_inv_def is_pg_cap_def
cte_wp_at_def[where P="(\<lambda>c. same_refs rv c s)" for rv s])
apply (intro allI conjI impI; clarsimp)
apply (rule conjI)
apply (clarsimp simp: cte_wp_at_def is_arch_update_def, rule conjI)
apply (clarsimp simp: is_arch_cap_def)
apply (clarsimp simp: cap_master_cap_simps)
apply (case_tac cap; clarsimp simp: cap_master_cap_simps diminished_def mask_cap_def
cap_rights_update_def)
apply (rename_tac acap rghts)
apply (case_tac acap; clarsimp simp: cap_master_cap_simps acap_rights_update_def)
apply (clarsimp simp: neq_Nil_conv invs_vspace_objs)
apply (frule diminished_cte_wp_at_valid_cap[where p="(a, b)" for a b], clarsimp)
apply (frule diminished_cte_wp_at_valid_cap[where p=slot], clarsimp)
apply (clarsimp simp: cte_wp_at_caps_of_state mask_cap_def
diminished_def[where cap="ArchObjectCap (PageCap d x y t z w)" for d x y t z w]
linorder_not_le aligned_sum_less_kernel_base
dest!: diminished_pm_capD)
apply (clarsimp simp: cap_rights_update_def acap_rights_update_def invs_implies is_cap_simps
is_aligned_pml4 not_less
cong: conj_cong
split: cap.splits arch_cap.splits)
apply (prop_tac "args ! 0 < pptr_base \<and> canonical_address (args ! 0)",
clarsimp dest!: aligned_sum_le_user_vtop, simp)
apply (extract_conjunct \<open>match conclusion in \<open>\<exists>a b cap. P a b cap\<close> for P \<Rightarrow> \<open>-\<close>\<close>,
fastforce simp: diminished_def mask_cap_def cap_rights_update_def acap_rights_update_def)
apply (extract_conjunct \<open>match conclusion in \<open>data_at vmpage_size word _\<close> \<Rightarrow> \<open>-\<close>\<close>,
clarsimp simp: valid_cap_simps data_at_def split: if_splits)
apply (extract_conjunct \<open>match conclusion in \<open>_ \<turnstile> _\<close> \<Rightarrow> \<open>-\<close>\<close>,
clarsimp simp: valid_cap_simps cap_aligned_def vmsz_aligned_def)
apply (clarsimp simp: vs_cap_ref_def split: vmpage_size.split)
apply (clarsimp simp: cte_wp_at_caps_of_state invs_implies is_aligned_pml4)
apply (drule bspec[where x="excaps ! 0"]; clarsimp)
apply (extract_conjunct \<open>match conclusion in \<open>\<exists>a b cap. caps_of_state _ _ = _ \<and> _\<close> \<Rightarrow> \<open>-\<close>\<close>,
cases "snd (excaps ! 0)", fastforce)
apply (extract_conjunct \<open>match conclusion in \<open>data_at vmpage_size word _\<close> \<Rightarrow> \<open>-\<close>\<close>,
clarsimp simp: valid_cap_simps data_at_def split: if_splits)
apply (prop_tac "args ! 0 < pptr_base \<and> canonical_address (args ! 0)",
clarsimp simp: valid_cap_simps, simp)
apply (drule (2) diminished_is_update'[rotated 2]; clarsimp)+
apply (clarsimp simp: cap_rights_update_def acap_rights_update_def)
apply (clarsimp simp: is_arch_update_reset_page get_cap_caps_of_state)
apply (cases "snd (excaps ! 0)", fastforce simp: diminished_def mask_cap_def cap_rights_update_def
acap_rights_update_def)
apply (cases "invocation_type label = ArchInvocationLabel X64PageUnmap")
apply (simp split del: if_split)
apply (rule hoare_pre, wp)
@ -1419,9 +1440,9 @@ lemma decode_page_invocation_wf[wp]:
apply (simp add: valid_unmap_def)
apply (erule cte_wp_at_weakenE)
apply (clarsimp simp: is_arch_diminished_def is_cap_simps)
apply (cases "invocation_type label = ArchInvocationLabel X64PageGetAddress";
simp split del: if_split;
wpsimp simp: valid_arch_inv_def valid_page_inv_def)
apply (cases "invocation_type label = ArchInvocationLabel X64PageGetAddress"
; simp split del: if_split
; wpsimp simp: valid_arch_inv_def valid_page_inv_def)
done
lemma decode_page_table_invocation_wf[wp]:

298
proof/invariant-abstract/X64/ArchVSpace_AI.thy
View File

@ -709,17 +709,14 @@ definition
definition
"valid_page_inv page_inv \<equiv> case page_inv of
PageMap cap ptr m vspace \<Rightarrow>
cte_wp_at (is_arch_update cap and ((=) None \<circ> vs_cap_ref)) ptr
cte_wp_at (is_arch_update cap) ptr
and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s))
and cte_wp_at is_pg_cap ptr
and (\<lambda>s. same_refs m cap s)
and valid_slots m
and valid_cap cap
and K (is_pg_cap cap \<and> empty_refs m)
and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs m) slot s)
| PageRemap m asid vspace\<Rightarrow>
valid_slots m and K (empty_refs m)
and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs m) slot s)
and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>cap. same_refs m cap s) slot s)
| PageUnmap cap ptr \<Rightarrow>
\<lambda>s. \<exists>d r R maptyp sz m. cap = PageCap d r R maptyp sz m \<and>
case_option True (valid_unmap sz) m \<and>
@ -3436,169 +3433,156 @@ lemma unmap_page_unmapped:
by (wpsimp wp: unmap_page_vs_lookup_pages_small unmap_page_vs_lookup_pages_large
unmap_page_vs_lookup_pages_huge)+
lemma set_cap_obj_at_vs_refs_pages[wp]:
"set_cap p cap \<lbrace>obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr\<rbrace>"
by (wpsimp wp: set_cap.aobj_at simp: vs_refs_pages_empty.arch_only)
lemmas invs_implies =
invs_equal_kernel_mappings
invs_arch_state
invs_valid_asid_map
invs_valid_global_objs
invs_valid_ioports
invs_valid_vs_lookup
invs_vspace_objs
invs_psp_aligned
invs_distinct
invs_cur
invs_iflive
invs_ifunsafe
invs_valid_global_refs
invs_valid_idle
invs_valid_irq_node
invs_valid_irq_states
invs_mdb
invs_valid_objs
invs_valid_pspace
invs_valid_reply_caps
invs_valid_reply_masters
invs_valid_stateI
invs_zombies
invs_unique_table_caps
invs_unique_refs
invs_hyp_sym_refs
invs_sym_refs
invs_valid_asid_table
tcb_at_invs
invs_valid_kernel_mappings
lemma vs_cap_ref_None:
"vs_cap_ref (ArchObjectCap (PageCap dev pg_ptr rghts maptype pg_sz mapdata)) = None \<longleftrightarrow> mapdata = None"
by (cases mapdata; clarsimp simp: vs_cap_ref_def split: vmpage_size.splits)
lemma perform_page_invs [wp]:
"\<lbrace>invs and valid_page_inv page_inv\<rbrace> perform_page_invocation page_inv \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: perform_page_invocation_def)
apply (cases page_inv, simp_all)
\<comment> \<open>PageMap\<close>
apply (rename_tac cap cslot_ptr sum)
apply clarsimp
apply (rule hoare_pre)
apply (wp store_pte_invs store_pde_invs store_pdpte_invs
hoare_vcg_const_imp_lift hoare_vcg_all_lift set_cap_arch_obj arch_update_cap_invs_map
| wpc
| simp add: pte_check_if_mapped_def pde_check_if_mapped_def del: fun_upd_apply split_paired_Ex
)+
apply (wp_trace set_cap_cte_wp_at_ex hoare_vcg_imp_lift hoare_vcg_all_lift arch_update_cap_invs_map
set_cap.aobj_at[OF vs_refs_pages_empty.arch_only] | wps)+
apply (clarsimp simp: valid_page_inv_def cte_wp_at_caps_of_state valid_slots_def is_cap_simps parent_for_refs_def
empty_refs_def same_refs_def pt_bits_def is_arch_update_def cap_master_cap_def
split: vm_page_entry.splits
simp del: split_paired_Ex split_paired_All
| strengthen not_in_global_refs_vs_lookup invs_valid_global_refs invs_arch_state invs_valid_vs_lookup
invs_valid_global_objs)+
apply (intro conjI impI allI)
apply (clarsimp simp del: split_paired_Ex split_paired_All)
apply (frule(2) unique_table_caps_ptD[OF _ _ _ _ _ _ invs_unique_table_caps], simp add: is_cap_simps, fastforce simp: is_cap_simps)
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs] is_aligned_pt[OF _ invs_psp_aligned]
simp: obj_refs_def valid_cap_def pt_bits_def is_aligned_neg_mask_eq)
apply simp
apply clarsimp
apply (rule ref_is_unique[OF _ vs_lookup_vs_lookup_pagesI reachable_page_table_not_global])
apply ((fastforce simp: local.invs_valid_kernel_mappings elim:valid_objs_caps[OF invs_valid_objs])+)[16]
apply (drule_tac x = ref in spec)
apply (clarsimp simp: vs_cap_ref_def pde_ref_pages_def split: pde.splits)
apply (clarsimp simp: valid_pde_def split: pde.splits
split: vmpage_size.splits option.split_asm pde.splits)
apply (intro conjI impI allI)
apply fastforce
apply (clarsimp simp del: split_paired_Ex split_paired_All)
apply (frule(2) unique_table_caps_pdD[OF _ _ _ _ _ _ invs_unique_table_caps], simp add: is_cap_simps, fastforce simp: is_cap_simps)
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs] is_aligned_pd[OF _ invs_psp_aligned]
simp: obj_refs_def valid_cap_def pt_bits_def is_aligned_neg_mask_eq)
apply simp
apply clarsimp
apply (rule ref_is_unique[OF _ vs_lookup_vs_lookup_pagesI reachable_page_table_not_global])
apply ((fastforce simp: local.invs_valid_kernel_mappings elim:valid_objs_caps[OF invs_valid_objs])+)[16]
apply (frule(1) caps_of_state_valid[OF _ invs_valid_objs])
apply (drule valid_global_refsD2, fastforce)
apply (clarsimp dest!: is_aligned_pd[OF _ invs_psp_aligned]
simp: is_aligned_neg_mask_eq cap_range_def valid_cap_def)
apply (clarsimp dest!: empty_refs_pageCapD)
\<comment> \<open>PageMap\<close>
apply (rename_tac cap cslot_ptr sum)
apply clarsimp
apply (rule hoare_pre)
apply (wpsimp wp: store_pte_invs store_pde_invs store_pdpte_invs hoare_vcg_const_imp_lift
hoare_vcg_all_lift set_cap_arch_obj arch_update_cap_invs_map
simp: pte_check_if_mapped_def pde_check_if_mapped_def
simp_del: fun_upd_apply split_paired_Ex)
apply (wp set_cap_cte_wp_at_ex hoare_vcg_imp_lift hoare_vcg_all_lift arch_update_cap_invs_map
set_cap.aobj_at[OF vs_refs_pages_empty.arch_only] | wps)+
apply (clarsimp simp: valid_page_inv_def cte_wp_at_caps_of_state valid_slots_def is_cap_simps
parent_for_refs_def empty_refs_def same_refs_def pt_bits_def
is_arch_update_def cap_master_cap_def
split: vm_page_entry.splits
simp del: split_paired_Ex split_paired_All
| strengthen not_in_global_refs_vs_lookup invs_valid_global_refs invs_arch_state
invs_valid_vs_lookup invs_valid_global_objs)+
apply (rule conjI, fastforce)
apply (intro conjI impI allI)
apply (clarsimp simp del: split_paired_Ex split_paired_All)
apply (frule(2) unique_table_caps_pdptD[OF _ _ _ _ _ _ invs_unique_table_caps], simp add: is_cap_simps, fastforce simp: is_cap_simps)
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs] is_aligned_pdpt[OF _ invs_psp_aligned]
simp: obj_refs_def valid_cap_def pdpt_bits_def is_aligned_neg_mask_eq)
apply simp
apply clarsimp
apply (rule ref_is_unique[OF _ vs_lookup_vs_lookup_pagesI reachable_page_table_not_global])
apply ((fastforce simp: local.invs_valid_kernel_mappings elim:valid_objs_caps[OF invs_valid_objs])+)[16]
apply (frule(1) caps_of_state_valid[OF _ invs_valid_objs, where c = "(ArchObjectCap (PDPointerTableCap pc asid))" for pc asid])
apply (drule valid_global_refsD2[where cap = "(ArchObjectCap (PDPointerTableCap pc asid))" for pc asid], fastforce)
apply (clarsimp dest!: is_aligned_pdpt[OF _ invs_psp_aligned]
simp: is_aligned_neg_mask_eq cap_range_def valid_cap_def cap_aligned_def)
\<comment> \<open>PageReMap\<close>
apply (rename_tac sum)
apply clarsimp
apply (rule hoare_pre)
apply (wp store_pte_invs store_pde_invs store_pdpte_invs
hoare_vcg_const_imp_lift hoare_vcg_all_lift set_cap_arch_obj arch_update_cap_invs_map
| wpc
| simp add: pte_check_if_mapped_def pde_check_if_mapped_def del: fun_upd_apply split_paired_Ex
)+
apply (clarsimp simp: valid_page_inv_def cte_wp_at_caps_of_state valid_slots_def is_cap_simps parent_for_refs_def
empty_refs_def same_refs_def pt_bits_def is_arch_update_def cap_master_cap_def
split: vm_page_entry.splits
simp del: split_paired_Ex split_paired_All
| strengthen not_in_global_refs_vs_lookup invs_valid_global_refs invs_arch_state invs_valid_vs_lookup
invs_valid_global_objs)+
apply (intro conjI impI allI)
apply (rule ccontr)
apply (clarsimp simp del: split_paired_Ex split_paired_All)
apply (frule(2) unique_table_caps_ptD[OF _ _ _ _ _ _ invs_unique_table_caps], simp add: is_cap_simps, fastforce simp: is_cap_simps)
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs] is_aligned_pt[OF _ invs_psp_aligned]
simp: obj_refs_def valid_cap_def pt_bits_def is_aligned_neg_mask_eq)
apply simp
apply clarsimp
apply (drule_tac x = ref in spec)
apply (drule vs_lookup_vs_lookup_pagesI')
apply (clarsimp simp del: split_paired_Ex split_paired_All)
apply (frule(2) unique_table_caps_ptD[OF _ _ _ _ _ _ invs_unique_table_caps],
simp add: is_cap_simps, fastforce simp: is_cap_simps)
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs]
simp: valid_cap_simps cap_asid_def pt_bits_def
split: option.split_asm)
apply force
apply force
apply clarsimp
apply (drule ref_is_unique[OF _ _ reachable_page_table_not_global])
apply ((fastforce simp: local.invs_valid_kernel_mappings elim:valid_objs_caps[OF invs_valid_objs])+)[13]
is_aligned_pt[OF _ invs_psp_aligned]
simp: obj_refs_def valid_cap_def pt_bits_def)
apply simp
apply clarsimp
apply (rule ref_is_unique[OF _ vs_lookup_vs_lookup_pagesI reachable_page_table_not_global])
apply ((fastforce simp: local.invs_valid_kernel_mappings
elim: valid_objs_caps[OF invs_valid_objs])+)[16]
apply (drule_tac x = ref in spec)
apply (clarsimp simp: vs_cap_ref_simps pde_ref_def split: pde.splits)
apply (intro conjI impI allI)
apply fastforce
apply (rule ccontr)
apply (clarsimp simp del: split_paired_Ex split_paired_All)
apply (frule(2) unique_table_caps_pdD[OF _ _ _ _ _ _ invs_unique_table_caps], simp add: is_cap_simps, fastforce simp: is_cap_simps)
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs] is_aligned_pd[OF _ invs_psp_aligned]
simp: obj_refs_def valid_cap_def pt_bits_def is_aligned_neg_mask_eq)
apply simp
apply clarsimp
apply (drule vs_lookup_vs_lookup_pagesI')
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs]
simp: valid_cap_simps cap_asid_def pt_bits_def
split: option.split_asm)
apply force
apply force
apply (drule ref_is_unique[OF _ _ reachable_page_table_not_global])
apply ((fastforce simp: local.invs_valid_kernel_mappings elim: valid_objs_caps[OF invs_valid_objs]
| strengthen reachable_page_table_not_global[mk_strg])+)[13]
apply (frule(1) caps_of_state_valid[OF _ invs_valid_objs])
apply (drule valid_global_refsD2, fastforce)
apply (clarsimp simp: vs_cap_ref_def pde_ref_pages_def split: pde.splits)
apply (clarsimp simp: valid_pde_def split: pde.splits
split: vmpage_size.splits option.split_asm pde.splits)
apply (intro conjI impI allI)
apply fastforce
apply (clarsimp simp del: split_paired_Ex split_paired_All)
apply (frule(2) unique_table_caps_pdD[OF _ _ _ _ _ _ invs_unique_table_caps],
simp add: is_cap_simps, fastforce simp: is_cap_simps)
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs] is_aligned_pd[OF _ invs_psp_aligned]
simp: obj_refs_def valid_cap_def pt_bits_def)
apply simp
apply clarsimp
apply (rule ref_is_unique[OF _ vs_lookup_vs_lookup_pagesI reachable_page_table_not_global])
apply ((fastforce simp: local.invs_valid_kernel_mappings
elim: valid_objs_caps[OF invs_valid_objs])+)[16]
apply (frule(1) caps_of_state_valid[OF _ invs_valid_objs])
apply (match premises in P: \<open>caps_of_state _ _ = Some (ArchObjectCap (PageDirectoryCap _ _))\<close>
\<Rightarrow> \<open>rule revcut_rl[OF valid_global_refsD2[OF P]]\<close>, fastforce)
apply (clarsimp dest!: is_aligned_pd[OF _ invs_psp_aligned]
simp: cap_range_def valid_cap_def)
apply (simp add: empty_ref_pageD)
apply (match premises in P: \<open>caps_of_state _ _ = Some (ArchObjectCap (PageDirectoryCap _ _))\<close>
\<Rightarrow> \<open>rule revcut_rl[OF valid_global_refsD2[OF P]]\<close>, fastforce)
apply (clarsimp dest!: is_aligned_pd[OF _ invs_psp_aligned]
simp: is_aligned_neg_mask_eq cap_range_def valid_cap_def)
apply (drule_tac x = ref in spec)
apply (clarsimp simp: vs_cap_ref_simps pdpte_ref_def pdpte_ref_pages_def split: pdpte.splits)
simp: cap_range_def valid_cap_def)
apply (rule conjI)
apply (rename_tac pd_cap_cnode pd_cap_idx pd_asid pd_map_data pg_rghts pg_map_ty
map_asid map_vaddr pde_paddr pde_attrs pde_rghts pg_asid pg_vaddr)
apply (intro allI impI, rename_tac pd_cap_cnode' pd_cap_idx' pd_cap')
apply (case_tac pd_cap'; clarsimp; rename_tac pd_acap'; case_tac pd_acap'; clarsimp)
apply (frule_tac ptr="(pd_cap_cnode, pd_cap_idx)" and ptr'="(pd_cap_cnode', pd_cap_idx')"
in unique_table_capsD[OF invs_unique_table_caps]; assumption?; clarsimp simp: is_cap_simps)
apply (clarsimp, frule (1) vs_lookup_invs_ref_is_unique[OF vs_lookup_vs_lookup_pagesI]
; assumption?; clarsimp)
apply (rule conjI, fastforce)
apply (clarsimp dest!: empty_refs_pageCapD)
apply (intro conjI impI allI)
apply fastforce
apply (rule ccontr)
apply (clarsimp simp del: split_paired_Ex split_paired_All)
apply (frule(2) unique_table_caps_pdptD[OF _ _ _ _ _ _ invs_unique_table_caps], simp add: is_cap_simps, fastforce simp: is_cap_simps)
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs] is_aligned_pdpt[OF _ invs_psp_aligned]
simp: obj_refs_def valid_cap_def pdpt_bits_def is_aligned_neg_mask_eq)
apply (frule(2) unique_table_caps_pdptD[OF _ _ _ _ _ _ invs_unique_table_caps],
simp add: is_cap_simps, fastforce simp: is_cap_simps)
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs]
is_aligned_pdpt[OF _ invs_psp_aligned]
simp: obj_refs_def valid_cap_def pdpt_bits_def)
apply simp
apply clarsimp
apply (drule vs_lookup_vs_lookup_pagesI')
apply (clarsimp dest!: caps_of_state_valid[OF _ invs_valid_objs]
simp: valid_cap_simps cap_asid_def pdpt_bits_def
split: option.split_asm)
apply force
apply force
apply (drule ref_is_unique[OF _ _ reachable_page_table_not_global])
apply ((fastforce simp: local.invs_valid_kernel_mappings elim: valid_objs_caps[OF invs_valid_objs]
| strengthen reachable_page_table_not_global[mk_strg])+)[13]
apply (frule(1) caps_of_state_valid[OF _ invs_valid_objs])
apply (drule valid_global_refsD2, fastforce)
apply (clarsimp dest!: is_aligned_pdpt[OF _ invs_psp_aligned]
simp: is_aligned_neg_mask_eq cap_range_def valid_cap_def)
\<comment> \<open>PageUnmap\<close>
apply (rename_tac arch_cap cslot_ptr)
apply (rule hoare_pre)
apply (wp dmo_invs arch_update_cap_invs_unmap_page get_cap_wp
| wpc | simp add: perform_page_invocation_unmap_def)+
apply (rule_tac Q="\<lambda>_ s. invs s \<and>
cte_wp_at (\<lambda>c. is_pg_cap c \<and>
(\<forall>ref. vs_cap_ref c = Some ref \<longrightarrow>
\<not> (ref \<unrhd> obj_ref_of c) s)) cslot_ptr s"
in hoare_strengthen_post)
prefer 2
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps
update_map_data_def
is_arch_update_def cap_master_cap_simps)
apply (drule caps_of_state_valid, fastforce)
apply (clarsimp simp: valid_cap_def cap_aligned_def vs_cap_ref_def
split: option.splits vmpage_size.splits cap.splits)
apply (simp add: cte_wp_at_caps_of_state)
apply (wp unmap_page_invs hoare_vcg_ex_lift hoare_vcg_all_lift hoare_vcg_imp_lift
unmap_page_unmapped)+
apply (rule ref_is_unique[OF _ vs_lookup_vs_lookup_pagesI reachable_page_table_not_global])
apply ((fastforce simp: local.invs_valid_kernel_mappings
elim: valid_objs_caps[OF invs_valid_objs])+)[16]
apply (frule(1) caps_of_state_valid[
OF _ invs_valid_objs,
where c = "(ArchObjectCap (PDPointerTableCap pc asid))" for pc asid])
apply (drule valid_global_refsD2[
where cap = "(ArchObjectCap (PDPointerTableCap pc asid))" for pc asid], fastforce)
apply (clarsimp dest!: is_aligned_pdpt[OF _ invs_psp_aligned]
simp: cap_range_def valid_cap_def cap_aligned_def)
\<comment> \<open>PageUnmap\<close>
apply (rename_tac arch_cap cslot_ptr)
apply (rule hoare_pre)
apply (wp dmo_invs arch_update_cap_invs_unmap_page get_cap_wp
| wpc | simp add: perform_page_invocation_unmap_def)+
apply (rule_tac Q="\<lambda>_ s. invs s \<and>
cte_wp_at (\<lambda>c. is_pg_cap c \<and>
(\<forall>ref. vs_cap_ref c = Some ref \<longrightarrow>
\<not> (ref \<unrhd> obj_ref_of c) s)) cslot_ptr s"
in hoare_strengthen_post)
prefer 2
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps
update_map_data_def
is_arch_update_def cap_master_cap_simps)
apply (drule caps_of_state_valid, fastforce)
apply (clarsimp simp: valid_cap_def cap_aligned_def vs_cap_ref_def
split: option.splits vmpage_size.splits cap.splits)
apply (simp add: cte_wp_at_caps_of_state)
apply (wp unmap_page_invs hoare_vcg_ex_lift hoare_vcg_all_lift hoare_vcg_imp_lift
unmap_page_unmapped)+
apply (clarsimp simp: valid_page_inv_def cte_wp_at_caps_of_state)
apply (clarsimp simp: is_arch_diminished_def)
apply (drule (2) diminished_is_update')
@ -3608,7 +3592,7 @@ lemma perform_page_invs [wp]:
using valid_validate_vm_rights[simplified valid_vm_rights_def]
apply (auto simp: valid_cap_simps cap_aligned_def mask_def vs_cap_ref_def data_at_def
split: vmpage_size.splits option.splits if_splits)[1]
apply (clarsimp simp: valid_page_inv_def cte_wp_at_caps_of_state valid_cap_def mask_def)
apply (clarsimp simp: valid_page_inv_def cte_wp_at_caps_of_state valid_cap_def mask_def)
\<comment> \<open>PageFlush\<close>
apply wp
apply (simp add: valid_page_inv_def tcb_at_invs)