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

x64 ainvs: update for GrantReply (SELFOUR-6)

This commit is contained in:
Rafal Kolanski 2018-10-23 00:32:47 +11:00 committed by Japheth Lim
parent 25a6d636e0
commit 8d137b4e86
12 changed files with 89 additions and 151 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
proof/invariant-abstract/X64/ArchCNodeInv_AI.thy
View File

@ -70,7 +70,7 @@ lemma copy_mask [simp, CNodeInv_AI_assms]:
apply (auto simp: copy_of_def is_cap_simps mask_cap_def
cap_rights_update_def same_object_as_def
bits_of_def acap_rights_update_def
split: cap.splits arch_cap.splits)
split: cap.splits arch_cap.splits bool.splits)
done
lemma update_cap_data_mask_Null [simp, CNodeInv_AI_assms]:
@ -154,6 +154,16 @@ lemma same_object_as_update_cap_data [CNodeInv_AI_assms]:
split: if_split_asm cap.splits)
done
lemma is_reply_update_cap_data[simp]:
"is_reply_cap (update_cap_data P x c) = is_reply_cap c"
by (simp add:is_reply_cap_def update_cap_data_def arch_update_cap_data_def the_cnode_cap_def
is_arch_cap_def badge_update_def split:cap.split)
lemma is_master_reply_update_cap_data[simp]:
"is_master_reply_cap (update_cap_data P x c) = is_master_reply_cap c"
by (simp add:is_master_reply_cap_def update_cap_data_def arch_update_cap_data_def
the_cnode_cap_def is_arch_cap_def badge_update_def split:cap.split)
lemma weak_derived_update_cap_data [CNodeInv_AI_assms]:
"\<lbrakk>update_cap_data P x c \<noteq> NullCap; weak_derived c c'\<rbrakk>
\<Longrightarrow> weak_derived (update_cap_data P x c) c'"
@ -164,14 +174,8 @@ lemma weak_derived_update_cap_data [CNodeInv_AI_assms]:
split del: if_split cong: if_cong)
apply (erule disjE)
apply (clarsimp split: if_split_asm)
apply (erule disjE)
apply (clarsimp simp: is_cap_simps)
apply (simp add: update_cap_data_def arch_update_cap_data_def is_cap_simps)
apply (erule disjE)
apply (clarsimp simp: is_cap_simps)
apply (simp add: update_cap_data_def arch_update_cap_data_def is_cap_simps)
apply (clarsimp simp: is_cap_simps)
apply (simp add: update_cap_data_def arch_update_cap_data_def is_cap_simps)
apply (erule (1) same_object_as_update_cap_data)
apply clarsimp
apply (rule conjI, clarsimp simp: is_cap_simps update_cap_data_def split del: if_split)+
@ -199,7 +203,7 @@ lemma cap_badge_update_cap_data [CNodeInv_AI_assms]:
lemma cap_vptr_rights_update[simp, CNodeInv_AI_assms]:
"cap_vptr (cap_rights_update f c) = cap_vptr c"
by (simp add: cap_vptr_def cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits)
split: cap.splits arch_cap.splits bool.splits)
lemma cap_vptr_mask[simp, CNodeInv_AI_assms]:
"cap_vptr (mask_cap m c) = cap_vptr c"
@ -207,8 +211,8 @@ lemma cap_vptr_mask[simp, CNodeInv_AI_assms]:
lemma cap_asid_base_rights [simp, CNodeInv_AI_assms]:
"cap_asid_base (cap_rights_update R c) = cap_asid_base c"
by (simp add: cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits)
by (auto simp add: cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits bool.splits)
lemma cap_asid_base_mask[simp, CNodeInv_AI_assms]:
"cap_asid_base (mask_cap m c) = cap_asid_base c"

4
proof/invariant-abstract/X64/ArchCSpaceInvPre_AI.thy
View File

@ -352,5 +352,9 @@ lemma state_hyp_refs_of_revokable[simp]:
"state_hyp_refs_of (s \<lparr> is_original_cap := m \<rparr>) = state_hyp_refs_of s"
by (rule revokable_update.state_hyp_refs_update)
lemma is_valid_vtable_root_is_arch_cap:
"is_valid_vtable_root cap \<Longrightarrow> is_arch_cap cap"
by (clarsimp simp: is_valid_vtable_root_def is_arch_cap_def)
end
end

15
proof/invariant-abstract/X64/ArchCSpaceInv_AI.thy
View File

@ -144,7 +144,11 @@ lemma replace_cap_invs:
apply (rule conjI)
apply (unfold reply_caps_mdb_def)[1]
apply (erule allEI, erule allEI)
subgoal by (fastforce split: if_split_asm simp: is_cap_simps)
apply (clarsimp split: if_split simp add: is_cap_simps
simp del: split_paired_Ex split_paired_All)
apply (rename_tac ptra ptrb rights')
apply (rule_tac x="(ptra,ptrb)" in exI)
apply fastforce
apply (unfold reply_masters_mdb_def)[1]
apply (erule allEI, erule allEI)
subgoal by (fastforce split: if_split_asm simp: is_cap_simps)
@ -155,16 +159,19 @@ lemma replace_cap_invs:
apply (clarsimp simp: ioport_revocable_def is_cap_simps)
apply (rule conjI)
apply (erule disjE)
apply (clarsimp)
apply (clarsimp simp add: is_reply_cap_to_def)
apply (drule caps_of_state_cteD)
apply (erule(1) valid_reply_capsD [OF has_reply_cap_cte_wpD])
apply (subgoal_tac "cte_wp_at (is_reply_cap_to t) p s")
apply (erule(1) valid_reply_capsD [OF has_reply_cap_cte_wpD])
apply (erule cte_wp_at_lift)
apply (fastforce simp add:is_reply_cap_to_def)
apply (simp add: is_cap_simps)
apply (frule(1) valid_global_refsD2)
apply (frule(1) cap_refs_in_kernel_windowD)
apply (rule conjI)
apply (erule disjE)
apply (clarsimp simp: valid_reply_masters_def cte_wp_at_caps_of_state)
apply (cases p, fastforce)
apply (cases p, fastforce simp:is_master_reply_cap_to_def)
apply (simp add: is_cap_simps)
apply (elim disjE)
apply simp

2
proof/invariant-abstract/X64/ArchCSpacePre_AI.thy
View File

@ -277,7 +277,7 @@ lemma valid_arch_mdb_weak_derived_update:
lemma valid_arch_mdb_tcb_cnode_update:
"valid_arch_mdb (is_original_cap s) (caps_of_state s) \<Longrightarrow>
valid_arch_mdb ((is_original_cap s) ((t, tcb_cnode_index 2) := True))
(caps_of_state s((t, tcb_cnode_index 2) \<mapsto> ReplyCap t True))"
(caps_of_state s((t, tcb_cnode_index 2) \<mapsto> ReplyCap t True canReplyGrant))"
by (clarsimp simp: valid_arch_mdb_def ioport_revocable_def)
lemmas valid_arch_mdb_updates = valid_arch_mdb_free_index_update valid_arch_mdb_not_arch_cap_update

22
proof/invariant-abstract/X64/ArchCSpace_AI.thy
View File

@ -55,20 +55,6 @@ lemma weak_derived_valid_cap [CSpace_AI_assms]:
split: cap.splits arch_cap.splits option.splits)
done
(* FIXME: unused *)
lemma weak_derived_tcb_cap_valid:
"\<lbrakk> tcb_cap_valid cap p s; weak_derived cap cap' \<rbrakk> \<Longrightarrow> tcb_cap_valid cap' p s"
apply (clarsimp simp add: tcb_cap_valid_def weak_derived_def
obj_at_def is_tcb
split: option.split)
apply (clarsimp simp: st_tcb_def2)
apply (erule disjE; simp add: copy_of_def split: if_split_asm; (solves \<open>clarsimp\<close>)?)
apply (clarsimp simp: tcb_cap_cases_def split: if_split_asm)
apply (auto simp: is_cap_simps same_object_as_def valid_ipc_buffer_cap_def
split: cap.split_asm arch_cap.split_asm
thread_state.split_asm)
done
lemma copy_obj_refs [CSpace_AI_assms]:
"copy_of cap cap' \<Longrightarrow> obj_refs cap' = obj_refs cap"
apply (cases cap)
@ -465,7 +451,7 @@ lemma mask_cap_valid[simp, CSpace_AI_assms]:
apply (cases c, simp_all add: valid_cap_def mask_cap_def
cap_rights_update_def
cap_aligned_def
acap_rights_update_def)
acap_rights_update_def split:bool.splits)
using valid_validate_vm_rights[simplified valid_vm_rights_def]
apply (rename_tac arch_cap)
by (case_tac arch_cap, simp_all)
@ -474,14 +460,14 @@ lemma mask_cap_objrefs[simp, CSpace_AI_assms]:
"obj_refs (mask_cap rs cap) = obj_refs cap"
by (cases cap, simp_all add: mask_cap_def cap_rights_update_def
acap_rights_update_def
split: arch_cap.split)
split: arch_cap.split bool.splits)
lemma mask_cap_zobjrefs[simp, CSpace_AI_assms]:
"zobj_refs (mask_cap rs cap) = zobj_refs cap"
by (cases cap, simp_all add: mask_cap_def cap_rights_update_def
acap_rights_update_def
split: arch_cap.split)
split: arch_cap.split bool.splits)
lemma derive_cap_valid_cap [CSpace_AI_assms]:
@ -497,7 +483,7 @@ lemma valid_cap_update_rights[simp, CSpace_AI_assms]:
"valid_cap cap s \<Longrightarrow> valid_cap (cap_rights_update cr cap) s"
apply (case_tac cap,
simp_all add: cap_rights_update_def valid_cap_def cap_aligned_def
acap_rights_update_def)
acap_rights_update_def split:bool.splits)
using valid_validate_vm_rights[simplified valid_vm_rights_def]
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all)

47
proof/invariant-abstract/X64/ArchFinalise_AI.thy
View File

@ -676,7 +676,7 @@ lemma tcb_cap_valid_pagetable:
"tcb_cap_valid (ArchObjectCap (PageTableCap word (Some v))) slot
= tcb_cap_valid (ArchObjectCap (PageTableCap word None)) slot"
apply (rule ext)
apply (simp add: tcb_cap_valid_def tcb_cap_cases_def
apply (simp add: tcb_cap_valid_def tcb_cap_cases_def is_valid_vtable_root_def
is_cap_simps valid_ipc_buffer_cap_def
split: Structures_A.thread_state.split)
done
@ -685,7 +685,7 @@ lemma tcb_cap_valid_pagedirectory:
"tcb_cap_valid (ArchObjectCap (PageDirectoryCap word (Some v))) slot
= tcb_cap_valid (ArchObjectCap (PageDirectoryCap word None)) slot"
apply (rule ext)
apply (simp add: tcb_cap_valid_def tcb_cap_cases_def
apply (simp add: tcb_cap_valid_def tcb_cap_cases_def is_valid_vtable_root_def
is_cap_simps valid_ipc_buffer_cap_def
split: Structures_A.thread_state.split)
done
@ -694,16 +694,7 @@ lemma tcb_cap_valid_pdpt:
"tcb_cap_valid (ArchObjectCap (PDPointerTableCap word (Some v))) slot
= tcb_cap_valid (ArchObjectCap (PDPointerTableCap word None)) slot"
apply (rule ext)
apply (simp add: tcb_cap_valid_def tcb_cap_cases_def
is_cap_simps valid_ipc_buffer_cap_def
split: Structures_A.thread_state.split)
done
lemma tcb_cap_valid_pml4:
"tcb_cap_valid (ArchObjectCap (PML4Cap word (Some v))) slot
= tcb_cap_valid (ArchObjectCap (PML4Cap word None)) slot"
apply (rule ext)
apply (simp add: tcb_cap_valid_def tcb_cap_cases_def
apply (simp add: tcb_cap_valid_def tcb_cap_cases_def is_valid_vtable_root_def
is_cap_simps valid_ipc_buffer_cap_def
split: Structures_A.thread_state.split)
done
@ -1008,31 +999,6 @@ lemma replaceable_reset_pdpt:
apply simp_all
done
lemma replaceable_reset_pml4:
"\<lbrakk>cap = PML4Cap p m \<and>
cte_wp_at ((=) (ArchObjectCap cap)) slot s \<and>
(\<forall>vs. vs_cap_ref (ArchObjectCap cap) = Some vs \<longrightarrow> \<not> (vs \<unrhd> p) s) \<and>
is_final_cap' (ArchObjectCap cap) s \<and>
obj_at (empty_table (set (second_level_tables (arch_state s)))) p s\<rbrakk> \<Longrightarrow>
replaceable s slot (ArchObjectCap (PML4Cap p None))
(ArchObjectCap cap)"
apply (elim conjE)
apply (cases m, simp_all add: replaceable_def gen_obj_refs_def cap_range_def is_cap_simps
tcb_cap_valid_pml4)
apply (rule conjI)
apply (frule is_final_cap_pml4_asid_eq) defer
apply clarsimp
apply (drule cte_wp_at_obj_refs_singleton_pml4)
apply (erule exE)
apply (drule_tac x="asid" in is_final_cap_pml4_asid_eq)
apply (drule final_cap_pml4_slot_eq)
apply simp_all
apply (rule_tac
cap="ArchObjectCap cap"
in no_cap_to_obj_with_diff_ref_finalI)
apply simp_all
done
crunch caps_of_state [wp]: arch_finalise_cap "\<lambda>s. P (caps_of_state s)"
(wp: crunch_wps simp: crunch_simps)
@ -1670,7 +1636,7 @@ lemma safe_ioport_insert_not_ioport:
"\<not>is_ioport_cap cap \<Longrightarrow> safe_ioport_insert cap cap' s"
by (clarsimp simp: is_cap_simps safe_ioport_insert_def cap_ioports_def split: cap.splits arch_cap.splits)
lemmas safe_ioport_insert_simps[simp] = safe_ioport_insert_not_ioport[where cap="ReplyCap a False" for a, simplified is_cap_simps, simplified]
lemmas safe_ioport_insert_simps[simp] = safe_ioport_insert_not_ioport[where cap="ReplyCap a False b" for a b, simplified is_cap_simps, simplified]
lemma cap_insert_ioports_not:
"\<lbrace>valid_ioports and K (\<not> is_ioport_cap cap \<and> dest \<noteq> src)\<rbrace>
@ -1685,8 +1651,9 @@ lemma cap_insert_ioports_not:
done
lemma setup_caller_cap_ioports:
"\<lbrace>valid_ioports\<rbrace> setup_caller_cap a b \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
by (wpsimp simp: setup_caller_cap_def is_cap_simps wp: cap_insert_ioports_not)
"\<lbrace>valid_ioports\<rbrace> setup_caller_cap a b c \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
by (wpsimp simp: setup_caller_cap_def is_cap_simps wp: cap_insert_ioports_not
split_del: if_split)
crunches set_mrs, as_user, set_message_info, copy_mrs, make_arch_fault_msg
for ioports[wp]: valid_ioports

2
proof/invariant-abstract/X64/ArchInterrupt_AI.thy
View File

@ -188,7 +188,7 @@ lemma invoke_irq_handler_invs'[Interrupt_AI_asms]:
(\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and
(\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s)
src s) and
(\<lambda>s. \<forall>t. cap = ReplyCap t False \<longrightarrow>
(\<lambda>s. \<forall>t R. cap = ReplyCap t False R \<longrightarrow>
st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and
K (\<not> is_master_reply_cap cap))\<rbrace>
cap_insert cap src dest \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>"

26
proof/invariant-abstract/X64/ArchIpc_AI.thy
View File

@ -38,7 +38,7 @@ lemma update_cap_data_closedform:
| DomainCap \<Rightarrow> DomainCap
| UntypedCap d p n idx \<Rightarrow> UntypedCap d p n idx
| NullCap \<Rightarrow> NullCap
| ReplyCap t m \<Rightarrow> ReplyCap t m
| ReplyCap t m rights \<Rightarrow> ReplyCap t m rights
| IRQControlCap \<Rightarrow> IRQControlCap
| IRQHandlerCap irq \<Rightarrow> IRQHandlerCap irq
| Zombie r b n \<Rightarrow> Zombie r b n
@ -109,14 +109,12 @@ lemma is_derived_cap_rights [simp, Ipc_AI_assms]:
apply (rule ext)
apply (simp add: cap_rights_update_def is_derived_def is_cap_simps)
apply (case_tac x, simp_all)
apply (simp add: cap_master_cap_def bits_of_def is_cap_simps
vs_cap_ref_def
split: cap.split)+
apply (simp add: is_cap_simps is_page_cap_def
cong: arch_cap.case_cong)
apply (simp split: arch_cap.split cap.split
add: is_cap_simps acap_rights_update_def is_pt_cap_def)
done
by (auto simp: cap_master_cap_def bits_of_def is_cap_simps
vs_cap_ref_def is_page_cap_def
acap_rights_update_def is_pt_cap_def
cong: arch_cap.case_cong
split: arch_cap.split cap.split bool.splits)
lemma data_to_message_info_valid [Ipc_AI_assms]:
"valid_message_info (data_to_message_info w)"
@ -187,9 +185,9 @@ lemma arch_derive_cap_objrefs_iszombie [Ipc_AI_assms]:
lemma obj_refs_remove_rights[simp, Ipc_AI_assms]:
"obj_refs (remove_rights rs cap) = obj_refs cap"
by (simp add: remove_rights_def cap_rights_update_def
by (auto simp add: remove_rights_def cap_rights_update_def
acap_rights_update_def
split: cap.splits arch_cap.splits)
split: cap.splits arch_cap.splits bool.splits)
lemma storeWord_um_inv:
"\<lbrace>\<lambda>s. underlying_memory s = um\<rbrace>
@ -395,7 +393,7 @@ lemma do_normal_transfer_non_null_cte_wp_at [Ipc_AI_assms]:
done
lemma is_derived_ReplyCap [simp, Ipc_AI_assms]:
"\<And>m p. is_derived m p (cap.ReplyCap t False) = (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t)"
"\<And>m p R. is_derived m p (cap.ReplyCap t False R) = (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t)"
apply (subst fun_eq_iff)
apply clarsimp
apply (case_tac x, simp_all add: is_derived_def is_cap_simps
@ -428,9 +426,9 @@ lemma do_ipc_transfer_tcb_caps [Ipc_AI_assms]:
done
lemma setup_caller_cap_valid_global_objs[wp, Ipc_AI_assms]:
"\<lbrace>valid_global_objs\<rbrace> setup_caller_cap send recv \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>"
"\<lbrace>valid_global_objs\<rbrace> setup_caller_cap send recv grant \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>"
apply (wp valid_global_objs_lift valid_vso_at_lift)
apply (simp_all add: setup_caller_cap_def)
apply (simp_all add: setup_caller_cap_def split del: if_split)
apply (wp sts_obj_at_impossible | simp add: tcb_not_empty_table)+
done

24
proof/invariant-abstract/X64/ArchKernelInit_AI.thy
View File

@ -196,6 +196,12 @@ lemma caps_of_state_init_A_st_Null:
apply (auto simp add: state_defs tcb_cap_cases_def split: if_split_asm)
done
lemma cte_wp_at_init_A_st_Null:
"cte_wp_at P p init_A_st \<Longrightarrow> P cap.NullCap"
apply (subst(asm) cte_wp_at_caps_of_state)
apply (simp add:caps_of_state_init_A_st_Null split: if_splits)
done
lemmas cte_wp_at_caps_of_state_eq
= cte_wp_at_caps_of_state[where P="(=) cap" for cap]
@ -235,7 +241,7 @@ lemma valid_global_vspace_mappings_init_A_st: "valid_global_vspace_mappings init
done
lemma invs_A:
"invs init_A_st"
"invs init_A_st" (is "invs ?st")
apply (simp add: invs_def)
apply (rule conjI)
prefer 2
@ -279,12 +285,16 @@ lemma invs_A:
apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def state_defs valid_arch_idle_def)
apply (rule conjI, clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def state_defs)
apply (rule conjI, clarsimp simp: if_unsafe_then_cap_def caps_of_state_init_A_st_Null)
apply (clarsimp simp: valid_reply_caps_def unique_reply_caps_def
has_reply_cap_def pred_tcb_at_def obj_at_def
caps_of_state_init_A_st_Null
cte_wp_at_caps_of_state_eq
valid_reply_masters_def valid_global_refs_def
valid_refs_def[unfolded cte_wp_at_caps_of_state])
apply (subgoal_tac "valid_reply_caps ?st \<and> valid_reply_masters ?st \<and> valid_global_refs ?st")
prefer 2
subgoal
using cte_wp_at_init_A_st_Null
by (fastforce simp: valid_reply_caps_def unique_reply_caps_def
has_reply_cap_def is_reply_cap_to_def pred_tcb_at_def obj_at_def
caps_of_state_init_A_st_Null is_master_reply_cap_to_def
valid_reply_masters_def valid_global_refs_def
valid_refs_def[unfolded cte_wp_at_caps_of_state])
apply (clarsimp, (thin_tac "_")+) (* use new proven assumptions, then drop them *)
apply (rule conjI)
apply (clarsimp simp: valid_arch_state_def)
apply (rule conjI)

16
proof/invariant-abstract/X64/ArchTcbAcc_AI.thy
View File

@ -53,12 +53,16 @@ lemma vm_sets_diff[simp]:
lemmas vm_sets_diff2[simp] = not_sym[OF vm_sets_diff]
lemma cap_master_cap_tcb_cap_valid_arch:
"\<lbrakk> cap_master_cap c = cap_master_cap c'; is_arch_cap c \<rbrakk> \<Longrightarrow>
tcb_cap_valid c p s = tcb_cap_valid c' p s"
by (simp add: cap_master_cap_def tcb_cap_valid_def tcb_cap_cases_def
valid_ipc_buffer_cap_def is_cap_simps
split: option.splits cap.splits arch_cap.splits
thread_state.splits)
"\<lbrakk> cap_master_cap c = cap_master_cap c'; is_arch_cap c' ;
is_valid_vtable_root c \<Longrightarrow> is_valid_vtable_root c' ; tcb_cap_valid c p s \<rbrakk> \<Longrightarrow>
tcb_cap_valid c' p s"
(* slow: 5 to 10s *)
by (auto simp: cap_master_cap_def tcb_cap_valid_def tcb_cap_cases_def
valid_ipc_buffer_cap_def is_cap_simps
is_nondevice_page_cap_simps is_nondevice_page_cap_arch_def
elim: pred_tcb_weakenE
split: option.splits cap.splits arch_cap.splits
Structures_A.thread_state.splits)
lemma storeWord_invs[wp, TcbAcc_AI_assms]:
"\<lbrace>in_user_frame p and invs\<rbrace> do_machine_op (storeWord p w) \<lbrace>\<lambda>rv. invs\<rbrace>"

4
proof/invariant-abstract/X64/ArchUntyped_AI.thy
View File

@ -34,7 +34,7 @@ lemma cnode_cap_ex_cte[Untyped_AI_assms]:
apply (simp only: ex_cte_cap_wp_to_def)
apply (rule exI, erule cte_wp_at_weakenE)
apply (clarsimp simp: is_cap_simps bits_of_def)
apply (case_tac c, simp_all add: mask_cap_def cap_rights_update_def)
apply (case_tac c, simp_all add: mask_cap_def cap_rights_update_def split:bool.splits)
apply (clarsimp simp: nat_to_cref_def word_bits_def)
apply (erule(2) valid_CNodeCapE)
apply (simp add: word_bits_def cte_level_bits_def)
@ -153,7 +153,7 @@ proof -
apply (rule conjI, assumption)
apply (clarsimp simp: diminished_def is_cap_simps mask_cap_def
cap_rights_update_def,
simp split: cap.splits )
simp split: cap.splits bool.splits)
done
qed

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

@ -1376,6 +1376,8 @@ lemma arch_update_cap_invs_map:
simp del: imp_disjL)
apply (frule master_cap_cap_range, simp del: imp_disjL)
apply (thin_tac "cap_range a = cap_range b" for a b)
apply (rule conjI)
apply (fastforce simp:is_valid_vtable_root_def vs_cap_ref_def split:arch_cap.splits vmpage_size.splits option.splits)
apply (rule conjI)
apply (rule ext)
apply (simp add: cap_master_cap_def split: cap.splits arch_cap.splits)
@ -1449,7 +1451,7 @@ lemma arch_update_cap_invs_unmap_page:
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def
is_cap_simps cap_master_cap_simps
fun_eq_iff appropriate_cte_cap_irqs
is_pt_cap_def
is_pt_cap_def is_valid_vtable_root_def
dest!: cap_master_cap_eqDs
simp del: imp_disjL)
apply (rule conjI)
@ -1486,7 +1488,7 @@ lemma arch_update_cap_invs_unmap_page_table:
set_cap_cap_refs_respects_device_region_spec[where ptr = p])
apply (simp add: final_cap_at_eq)
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def
is_cap_simps cap_master_cap_simps
is_cap_simps cap_master_cap_simps is_valid_vtable_root_def
appropriate_cte_cap_irqs is_pt_cap_def
fun_eq_iff[where f="cte_refs cap" for cap]
dest!: cap_master_cap_eqDs
@ -1530,7 +1532,7 @@ lemma arch_update_cap_invs_unmap_page_directory:
set_cap_cap_refs_respects_device_region_spec[where ptr = p])
apply (simp add: final_cap_at_eq)
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def
is_cap_simps cap_master_cap_simps
is_cap_simps cap_master_cap_simps is_valid_vtable_root_def
appropriate_cte_cap_irqs is_pt_cap_def
fun_eq_iff[where f="cte_refs cap" for cap]
dest!: cap_master_cap_eqDs
@ -1574,51 +1576,7 @@ lemma arch_update_cap_invs_unmap_pd_pointer_table:
set_cap_cap_refs_respects_device_region_spec[where ptr = p])
apply (simp add: final_cap_at_eq)
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def
is_cap_simps cap_master_cap_simps
appropriate_cte_cap_irqs is_pt_cap_def
fun_eq_iff[where f="cte_refs cap" for cap]
dest!: cap_master_cap_eqDs
simp del: imp_disjL)
apply (rule conjI)
apply (drule(1) if_unsafe_then_capD [OF caps_of_state_cteD])
apply (clarsimp simp: cap_master_cap_def)
apply (erule ex_cte_cap_wp_to_weakenE)
apply (clarsimp simp: appropriate_cte_cap_def)
apply (rule conjI)
apply (drule valid_global_refsD2, clarsimp)
apply (simp add: cap_range_def)
apply (frule(1) cap_refs_in_kernel_windowD)
apply (simp add: cap_range_def gen_obj_refs_def image_def)
apply (intro conjI)
apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
cte_wp_at_caps_of_state)
apply fastforce
apply (clarsimp simp: obj_at_def empty_table_def)
apply (clarsimp split: Structures_A.kernel_object.split_asm
arch_kernel_obj.split_asm)
apply clarsimp
apply fastforce
done
lemma arch_update_cap_invs_unmap_page_map_l4:
"\<lbrace>cte_wp_at (is_arch_update cap) p
and invs and valid_cap cap
and (\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s)
and obj_at (empty_table {}) (obj_ref_of cap)
and (\<lambda>s. cte_wp_at (\<lambda>c. \<forall>r. vs_cap_ref c = Some r
\<longrightarrow> \<not> (r \<unrhd> obj_ref_of cap) s) p s)
and K (is_pml4_cap cap \<and> vs_cap_ref cap = None)\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: invs_def valid_state_def)
apply (rule hoare_pre)
apply (wp arch_update_cap_pspace arch_update_cap_valid_mdb set_cap_idle
update_cap_ifunsafe valid_irq_node_typ set_cap_typ_at
set_cap_irq_handlers set_cap_valid_arch_caps set_cap_ioports_no_new_ioports
set_cap_cap_refs_respects_device_region_spec[where ptr = p])
apply (simp add: final_cap_at_eq)
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def
is_cap_simps cap_master_cap_simps
is_cap_simps cap_master_cap_simps is_valid_vtable_root_def
appropriate_cte_cap_irqs is_pt_cap_def
fun_eq_iff[where f="cte_refs cap" for cap]
dest!: cap_master_cap_eqDs