x64: s/ARM/X64/g proof/refine/X64/*.thy
This commit is contained in:
Joel Beeren
parent
72f6b33659
commit
263ebe904a
|
|
@ -76,43 +76,43 @@ lemma vm_rights_of_vmrights_map_id[simp]:
|
|||
|
||||
definition
|
||||
absPageTable :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> obj_ref \<Rightarrow>
|
||||
word8 \<Rightarrow> ARM_A.pte"
|
||||
word8 \<Rightarrow> X64_A.pte"
|
||||
where
|
||||
"absPageTable h a \<equiv> %offs.
|
||||
case (h (a + (ucast offs << 2))) of
|
||||
Some (KOArch (KOPTE (ARM_H.InvalidPTE))) \<Rightarrow> ARM_A.InvalidPTE
|
||||
| Some (KOArch (KOPTE (ARM_H.LargePagePTE p c g xn rights))) \<Rightarrow>
|
||||
Some (KOArch (KOPTE (X64_H.InvalidPTE))) \<Rightarrow> X64_A.InvalidPTE
|
||||
| Some (KOArch (KOPTE (X64_H.LargePagePTE p c g xn rights))) \<Rightarrow>
|
||||
if is_aligned offs 4 then
|
||||
ARM_A.LargePagePTE p
|
||||
X64_A.LargePagePTE p
|
||||
{x. c & x=PageCacheable | g & x=Global | xn & x=XNever}
|
||||
(vm_rights_of rights)
|
||||
else ARM_A.InvalidPTE
|
||||
| Some (KOArch (KOPTE (ARM_H.SmallPagePTE p c g xn rights))) \<Rightarrow>
|
||||
ARM_A.SmallPagePTE p {x. c & x=PageCacheable |
|
||||
else X64_A.InvalidPTE
|
||||
| Some (KOArch (KOPTE (X64_H.SmallPagePTE p c g xn rights))) \<Rightarrow>
|
||||
X64_A.SmallPagePTE p {x. c & x=PageCacheable |
|
||||
g & x=Global |
|
||||
xn & x=XNever} (vm_rights_of rights)"
|
||||
|
||||
definition
|
||||
absPageDirectory :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> obj_ref \<Rightarrow>
|
||||
12 word \<Rightarrow> ARM_A.pde"
|
||||
12 word \<Rightarrow> X64_A.pde"
|
||||
where
|
||||
"absPageDirectory h a \<equiv> %offs.
|
||||
case (h (a + (ucast offs << 2))) of
|
||||
Some (KOArch (KOPDE (ARM_H.InvalidPDE))) \<Rightarrow> ARM_A.InvalidPDE
|
||||
| Some (KOArch (KOPDE (ARM_H.PageTablePDE p e mw))) \<Rightarrow>
|
||||
ARM_A.PageTablePDE p {x. e & x=ParityEnabled} mw
|
||||
| Some (KOArch (KOPDE (ARM_H.SectionPDE p e mw c g xn rights))) \<Rightarrow>
|
||||
ARM_A.SectionPDE p {x. e & x=ParityEnabled |
|
||||
Some (KOArch (KOPDE (X64_H.InvalidPDE))) \<Rightarrow> X64_A.InvalidPDE
|
||||
| Some (KOArch (KOPDE (X64_H.PageTablePDE p e mw))) \<Rightarrow>
|
||||
X64_A.PageTablePDE p {x. e & x=ParityEnabled} mw
|
||||
| Some (KOArch (KOPDE (X64_H.SectionPDE p e mw c g xn rights))) \<Rightarrow>
|
||||
X64_A.SectionPDE p {x. e & x=ParityEnabled |
|
||||
c & x=PageCacheable |
|
||||
g & x=Global |
|
||||
xn & x=XNever} mw (vm_rights_of rights)
|
||||
| Some (KOArch (KOPDE (ARM_H.SuperSectionPDE p e c g xn rights))) \<Rightarrow>
|
||||
| Some (KOArch (KOPDE (X64_H.SuperSectionPDE p e c g xn rights))) \<Rightarrow>
|
||||
if is_aligned offs 4 then
|
||||
ARM_A.SuperSectionPDE p
|
||||
X64_A.SuperSectionPDE p
|
||||
{x. e & x=ParityEnabled | c & x=PageCacheable
|
||||
| g & x=Global | xn & x=XNever}
|
||||
(vm_rights_of rights)
|
||||
else ARM_A.InvalidPDE"
|
||||
else X64_A.InvalidPDE"
|
||||
|
||||
(* Can't pull the whole heap off at once, start with arch specific stuff.*)
|
||||
definition
|
||||
|
|
@ -121,8 +121,8 @@ definition
|
|||
where
|
||||
"absHeapArch h a \<equiv> %ako.
|
||||
(case ako of
|
||||
KOASIDPool (ARM_H.ASIDPool ap) \<Rightarrow>
|
||||
Some (ARM_A.ASIDPool (\<lambda>w. ap (ucast w)))
|
||||
KOASIDPool (X64_H.ASIDPool ap) \<Rightarrow>
|
||||
Some (X64_A.ASIDPool (\<lambda>w. ap (ucast w)))
|
||||
| KOPTE _ \<Rightarrow>
|
||||
if is_aligned a pt_bits then Some (PageTable (absPageTable h a))
|
||||
else None
|
||||
|
|
@ -138,10 +138,10 @@ lemma
|
|||
Some (KOArch (KOPTE pte')))"
|
||||
and pte_rights:
|
||||
"\<forall>x. case ksPSpace \<sigma> x of
|
||||
Some (KOArch (KOPTE (ARM_H.LargePagePTE _ _ _ _ r))) \<Rightarrow>
|
||||
Some (KOArch (KOPTE (X64_H.LargePagePTE _ _ _ _ r))) \<Rightarrow>
|
||||
r \<noteq> VMNoAccess"
|
||||
"\<forall>x. case ksPSpace \<sigma> x of
|
||||
Some (KOArch (KOPTE (ARM_H.SmallPagePTE _ _ _ _ r))) \<Rightarrow>
|
||||
Some (KOArch (KOPTE (X64_H.SmallPagePTE _ _ _ _ r))) \<Rightarrow>
|
||||
r \<noteq> VMNoAccess"
|
||||
|
||||
assumes pdes:
|
||||
|
|
@ -151,10 +151,10 @@ lemma
|
|||
Some (KOArch (KOPDE pde')))"
|
||||
and pde_rights:
|
||||
"\<forall>x. case ksPSpace \<sigma> x of
|
||||
Some (KOArch (KOPDE (ARM_H.SectionPDE _ _ _ _ _ _ r))) \<Rightarrow>
|
||||
Some (KOArch (KOPDE (X64_H.SectionPDE _ _ _ _ _ _ r))) \<Rightarrow>
|
||||
r \<noteq> VMNoAccess"
|
||||
"\<forall>x. case ksPSpace \<sigma> x of
|
||||
Some (KOArch (KOPDE (ARM_H.SuperSectionPDE _ _ _ _ _ r))) \<Rightarrow>
|
||||
Some (KOArch (KOPDE (X64_H.SuperSectionPDE _ _ _ _ _ r))) \<Rightarrow>
|
||||
r \<noteq> VMNoAccess"
|
||||
|
||||
assumes fst_pte:
|
||||
|
|
@ -251,7 +251,7 @@ lemma
|
|||
apply (erule_tac x=y in allE)
|
||||
apply clarsimp
|
||||
apply (rule_tac x=pte' in exI)
|
||||
apply (simp add: absPageTable_def split: option.splits ARM_H.pte.splits)
|
||||
apply (simp add: absPageTable_def split: option.splits X64_H.pte.splits)
|
||||
apply (clarsimp simp add: vmrights_map_def vm_rights_of_def
|
||||
vm_kernel_only_def vm_read_only_def vm_read_write_def
|
||||
split: vmrights.splits)
|
||||
|
|
@ -267,7 +267,7 @@ lemma
|
|||
apply clarsimp
|
||||
apply (simp add: pde_relation_def pde_relation_aligned_def)
|
||||
apply (simp add: absPageDirectory_def
|
||||
split: option.splits ARM_H.pde.splits)
|
||||
split: option.splits X64_H.pde.splits)
|
||||
apply (clarsimp simp add: vmrights_map_def vm_rights_of_def
|
||||
vm_kernel_only_def vm_read_only_def vm_read_write_def
|
||||
split: vmrights.splits)
|
||||
|
|
@ -415,7 +415,7 @@ lemma LookupFailureMap_lookup_failure_map:
|
|||
primrec
|
||||
ArchFaultMap :: "Fault_H.arch_fault \<Rightarrow> ExceptionTypes_A.arch_fault"
|
||||
where
|
||||
"ArchFaultMap (ArchFault_H.ARM_H.arch_fault.VMFault p m) = Machine_A.ARM_A.arch_fault.VMFault p m"
|
||||
"ArchFaultMap (ArchFault_H.X64_H.arch_fault.VMFault p m) = Machine_A.X64_A.arch_fault.VMFault p m"
|
||||
|
||||
|
||||
primrec
|
||||
|
|
@ -880,10 +880,10 @@ proof -
|
|||
apply (erule_tac x=offs in allE)
|
||||
apply (rename_tac pte')
|
||||
apply (case_tac pte', simp_all add: pte_relation_aligned_def)[1]
|
||||
apply (clarsimp split: ARM_A.pte.splits)
|
||||
apply (clarsimp split: X64_A.pte.splits)
|
||||
apply (rule set_eqI, clarsimp)
|
||||
apply (case_tac x, simp_all)[1]
|
||||
apply (clarsimp split: ARM_A.pte.splits)
|
||||
apply (clarsimp split: X64_A.pte.splits)
|
||||
apply (rule set_eqI, clarsimp)
|
||||
apply (case_tac x, simp_all)[1]
|
||||
apply (clarsimp simp add: pde_relation_def)
|
||||
|
|
@ -925,12 +925,12 @@ proof -
|
|||
apply (erule_tac x=offs in allE)
|
||||
apply (rename_tac pde')
|
||||
apply (case_tac pde', simp_all add: pde_relation_aligned_def)[1]
|
||||
apply (clarsimp split: ARM_A.pde.splits)+
|
||||
apply (clarsimp split: X64_A.pde.splits)+
|
||||
apply (fastforce simp add: subset_eq)
|
||||
apply (clarsimp split: ARM_A.pde.splits)
|
||||
apply (clarsimp split: X64_A.pde.splits)
|
||||
apply (rule set_eqI, clarsimp)
|
||||
apply (case_tac x, simp_all)[1]
|
||||
apply (clarsimp split: ARM_A.pde.splits)
|
||||
apply (clarsimp split: X64_A.pde.splits)
|
||||
apply (rule set_eqI, clarsimp)
|
||||
apply (case_tac x, simp_all)[1]
|
||||
apply (clarsimp simp add: pde_relation_def split: if_split_asm)
|
||||
|
|
@ -983,7 +983,7 @@ shows
|
|||
apply (erule(1) obj_relation_cutsE)
|
||||
apply (clarsimp simp: other_obj_relation_def
|
||||
split: Structures_A.kernel_object.split_asm if_split_asm
|
||||
ARM_A.arch_kernel_obj.split_asm)+
|
||||
X64_A.arch_kernel_obj.split_asm)+
|
||||
done
|
||||
|
||||
text {* The following function can be used to reverse cte_map. *}
|
||||
|
|
@ -1850,10 +1850,10 @@ done
|
|||
definition
|
||||
"absArchState s' \<equiv>
|
||||
case s' of ARMKernelState asid_tbl hwat anext am gpd gpts kvspace \<Rightarrow>
|
||||
\<lparr>arm_asid_table = asid_tbl \<circ> ucast,
|
||||
arm_hwasid_table = hwat, arm_next_asid = anext,
|
||||
arm_asid_map = am, arm_global_pd = gpd, arm_global_pts = gpts,
|
||||
arm_kernel_vspace = kvspace\<rparr>"
|
||||
\<lparr>x64_asid_table = asid_tbl \<circ> ucast,
|
||||
x64_hwasid_table = hwat, x64_next_asid = anext,
|
||||
x64_asid_map = am, x64_global_pd = gpd, x64_global_pts = gpts,
|
||||
x64_kernel_vspace = kvspace\<rparr>"
|
||||
|
||||
lemma absArchState_correct:
|
||||
assumes rel:
|
||||
|
|
@ -1866,7 +1866,7 @@ apply (subgoal_tac "(arch_state s, ksArchState s') \<in> arch_state_relation")
|
|||
apply (simp add: state_relation_def)
|
||||
apply (clarsimp simp add: arch_state_relation_def)
|
||||
by (clarsimp simp add: absArchState_def
|
||||
split: ARM_H.kernel_state.splits)
|
||||
split: X64_H.kernel_state.splits)
|
||||
|
||||
definition absSchedulerAction where
|
||||
"absSchedulerAction action \<equiv>
|
||||
|
|
|
|||
|
|
@ -23,8 +23,8 @@ declare is_aligned_shiftr [intro!]
|
|||
|
||||
definition
|
||||
"asid_ci_map i \<equiv>
|
||||
case i of ARM_A.MakePool frame slot parent base \<Rightarrow>
|
||||
ARM_H.MakePool frame (cte_map slot) (cte_map parent) base"
|
||||
case i of X64_A.MakePool frame slot parent base \<Rightarrow>
|
||||
X64_H.MakePool frame (cte_map slot) (cte_map parent) base"
|
||||
|
||||
definition
|
||||
"valid_aci' aci \<equiv> case aci of MakePool frame slot parent base \<Rightarrow>
|
||||
|
|
@ -442,7 +442,7 @@ lemma ARMMMU_improve_cases:
|
|||
by (cases cap, simp_all add: isCap_simps)
|
||||
|
||||
|
||||
crunch inv [wp]: "ARM_H.decodeInvocation" "P"
|
||||
crunch inv [wp]: "X64_H.decodeInvocation" "P"
|
||||
(wp: crunch_wps mapME_x_inv_wp getASID_wp
|
||||
simp: forME_x_def crunch_simps
|
||||
ARMMMU_improve_cases
|
||||
|
|
@ -511,13 +511,13 @@ lemma page_base_corres[simp]:
|
|||
by (clarsimp simp: pageBase_def page_base_def)
|
||||
|
||||
lemma flush_type_map:
|
||||
"ARM_H.isPageFlushLabel (invocation_type (mi_label mi))
|
||||
\<or> ARM_H.isPDFlushLabel (invocation_type (mi_label mi))
|
||||
"X64_H.isPageFlushLabel (invocation_type (mi_label mi))
|
||||
\<or> X64_H.isPDFlushLabel (invocation_type (mi_label mi))
|
||||
\<Longrightarrow> labelToFlushType (mi_label mi) =
|
||||
flush_type_map (label_to_flush_type (invocation_type (mi_label mi)))"
|
||||
by (clarsimp simp: label_to_flush_type_def labelToFlushType_def flush_type_map_def
|
||||
ARM_H.isPageFlushLabel_def ARM_H.isPDFlushLabel_def
|
||||
split: ARM_A.flush_type.splits invocation_label.splits arch_invocation_label.splits)
|
||||
X64_H.isPageFlushLabel_def X64_H.isPDFlushLabel_def
|
||||
split: X64_A.flush_type.splits invocation_label.splits arch_invocation_label.splits)
|
||||
|
||||
lemma resolve_vaddr_corres:
|
||||
"\<lbrakk> is_aligned pd pd_bits; vaddr < kernel_base \<rbrakk> \<Longrightarrow>
|
||||
|
|
@ -548,7 +548,7 @@ lemma resolve_vaddr_corres:
|
|||
done
|
||||
|
||||
lemma dec_arch_inv_page_flush_corres:
|
||||
"ARM_H.isPageFlushLabel (invocation_type (mi_label mi)) \<Longrightarrow>
|
||||
"X64_H.isPageFlushLabel (invocation_type (mi_label mi)) \<Longrightarrow>
|
||||
corres (ser \<oplus> archinv_relation)
|
||||
(invs and
|
||||
valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and
|
||||
|
|
@ -577,7 +577,7 @@ lemma dec_arch_inv_page_flush_corres:
|
|||
throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
|
||||
returnOk $
|
||||
arch_invocation.InvokePage $
|
||||
ARM_A.page_invocation.PageFlush
|
||||
X64_A.page_invocation.PageFlush
|
||||
(label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr)
|
||||
(end + vaddr - 1) (addrFromPPtr word + start) pd asid
|
||||
odE
|
||||
|
|
@ -606,7 +606,7 @@ lemma dec_arch_inv_page_flush_corres:
|
|||
apply (rule corres_returnOk)
|
||||
apply (clarsimp simp: archinv_relation_def page_invocation_map_def
|
||||
label_to_flush_type_def labelToFlushType_def flush_type_map_def
|
||||
ARM_H.isPageFlushLabel_def
|
||||
X64_H.isPageFlushLabel_def
|
||||
split: flush_type.splits invocation_label.splits arch_invocation_label.splits)
|
||||
apply wp+
|
||||
apply (fastforce simp: valid_cap_def mask_def)
|
||||
|
|
@ -643,11 +643,11 @@ lemma vs_refs_pages_ptI:
|
|||
done
|
||||
|
||||
lemmas vs_refs_pages_pt_largeI
|
||||
= vs_refs_pages_ptI[where pte="ARM_A.pte.LargePagePTE x y z" for x y z,
|
||||
= vs_refs_pages_ptI[where pte="X64_A.pte.LargePagePTE x y z" for x y z,
|
||||
unfolded pte_ref_pages_def, simplified, OF _ refl]
|
||||
|
||||
lemmas vs_refs_pages_pt_smallI
|
||||
= vs_refs_pages_ptI[where pte="ARM_A.pte.SmallPagePTE x y z" for x y z,
|
||||
= vs_refs_pages_ptI[where pte="X64_A.pte.SmallPagePTE x y z" for x y z,
|
||||
unfolded pte_ref_pages_def, simplified, OF _ refl]
|
||||
|
||||
lemma vs_refs_pages_pdI:
|
||||
|
|
@ -660,11 +660,11 @@ lemma vs_refs_pages_pdI:
|
|||
done
|
||||
|
||||
lemmas vs_refs_pages_pd_sectionI
|
||||
= vs_refs_pages_pdI[where pde="ARM_A.pde.SectionPDE x y z w" for x y z w,
|
||||
= vs_refs_pages_pdI[where pde="X64_A.pde.SectionPDE x y z w" for x y z w,
|
||||
unfolded pde_ref_pages_def, simplified, OF _ refl]
|
||||
|
||||
lemmas vs_refs_pages_pd_supersectionI
|
||||
= vs_refs_pages_pdI[where pde="ARM_A.pde.SuperSectionPDE x y z" for x y z,
|
||||
= vs_refs_pages_pdI[where pde="X64_A.pde.SuperSectionPDE x y z" for x y z,
|
||||
unfolded pde_ref_pages_def, simplified, OF _ refl]
|
||||
|
||||
lemma get_master_pde_sp:
|
||||
|
|
@ -829,7 +829,7 @@ shows
|
|||
(Arch.decodeInvocation (mi_label mi) args cptr'
|
||||
(cte_map slot) arch_cap' excaps')"
|
||||
apply (simp add: arch_decode_invocation_def
|
||||
ARM_H.decodeInvocation_def
|
||||
X64_H.decodeInvocation_def
|
||||
decodeARMMMUInvocation_def
|
||||
split del: if_split)
|
||||
apply (cases arch_cap)
|
||||
|
|
@ -1125,12 +1125,12 @@ shows
|
|||
apply simp
|
||||
apply (rule corres_returnOk)
|
||||
apply (clarsimp simp: archinv_relation_def page_invocation_map_def)
|
||||
apply (cases "ARM_H.isPageFlushLabel (invocation_type (mi_label mi))")
|
||||
apply (clarsimp simp: ARM_H.isPageFlushLabel_def split del: if_split)
|
||||
apply (cases "X64_H.isPageFlushLabel (invocation_type (mi_label mi))")
|
||||
apply (clarsimp simp: X64_H.isPageFlushLabel_def split del: if_split)
|
||||
apply (clarsimp split: invocation_label.splits arch_invocation_label.splits split del: if_split)
|
||||
apply (rule dec_arch_inv_page_flush_corres,
|
||||
clarsimp simp: ARM_H.isPageFlushLabel_def)+
|
||||
apply (clarsimp simp: ARM_H.isPageFlushLabel_def split del: if_split)
|
||||
clarsimp simp: X64_H.isPageFlushLabel_def)+
|
||||
apply (clarsimp simp: X64_H.isPageFlushLabel_def split del: if_split)
|
||||
apply (cases "invocation_type (mi_label mi) = ArchInvocationLabel ARMPageGetAddress")
|
||||
apply simp
|
||||
apply (rule corres_returnOk)
|
||||
|
|
@ -1209,7 +1209,7 @@ shows
|
|||
erule invs_pspace_aligned', clarsimp+)
|
||||
apply (simp add: isCap_simps)
|
||||
apply (simp add: isCap_simps split del: if_split)
|
||||
apply (cases "ARM_H.isPDFlushLabel (invocation_type (mi_label mi))")
|
||||
apply (cases "X64_H.isPDFlushLabel (invocation_type (mi_label mi))")
|
||||
apply (clarsimp split del: if_split)
|
||||
apply (cases args, simp)
|
||||
apply (rename_tac a0 as)
|
||||
|
|
@ -1276,7 +1276,7 @@ lemma inv_arch_corres:
|
|||
(invs' and ct_active' and valid_arch_inv' ai' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
|
||||
(arch_perform_invocation ai) (Arch.performInvocation ai')"
|
||||
apply (clarsimp simp: arch_perform_invocation_def
|
||||
ARM_H.performInvocation_def
|
||||
X64_H.performInvocation_def
|
||||
performARMMMUInvocation_def)
|
||||
apply (rule corres_split' [where r'=dc])
|
||||
prefer 2
|
||||
|
|
@ -1358,7 +1358,7 @@ lemma invokeArch_tcb_at':
|
|||
"\<lbrace>invs' and valid_arch_inv' ai and ct_active' and st_tcb_at' active' p\<rbrace>
|
||||
Arch.performInvocation ai
|
||||
\<lbrace>\<lambda>rv. tcb_at' p\<rbrace>"
|
||||
apply (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def)
|
||||
apply (simp add: X64_H.performInvocation_def performARMMMUInvocation_def)
|
||||
apply (cases ai, simp_all)
|
||||
apply (wp, clarsimp simp: pred_tcb_at')
|
||||
apply (wp, clarsimp simp: pred_tcb_at')
|
||||
|
|
@ -1719,7 +1719,7 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]:
|
|||
done
|
||||
|
||||
lemma arch_decodeARMPageFlush_wf:
|
||||
"ARM_H.isPageFlushLabel (invocation_type label) \<Longrightarrow>
|
||||
"X64_H.isPageFlushLabel (invocation_type label) \<Longrightarrow>
|
||||
\<lbrace>invs' and
|
||||
valid_cap'
|
||||
(capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) and
|
||||
|
|
@ -1749,7 +1749,7 @@ lemma arch_decodeInvocation_wf[wp]:
|
|||
Arch.decodeInvocation label args cap_index slot arch_cap excaps
|
||||
\<lbrace>valid_arch_inv'\<rbrace>,-"
|
||||
apply (cases arch_cap)
|
||||
apply (simp add: decodeARMMMUInvocation_def ARM_H.decodeInvocation_def
|
||||
apply (simp add: decodeARMMMUInvocation_def X64_H.decodeInvocation_def
|
||||
Let_def split_def isCap_simps
|
||||
cong: if_cong split del: if_split)
|
||||
apply (rule hoare_pre)
|
||||
|
|
@ -1769,7 +1769,7 @@ lemma arch_decodeInvocation_wf[wp]:
|
|||
apply assumption
|
||||
apply (simp add: asid_low_bits_def asid_bits_def)
|
||||
apply assumption
|
||||
apply (simp add: decodeARMMMUInvocation_def ARM_H.decodeInvocation_def
|
||||
apply (simp add: decodeARMMMUInvocation_def X64_H.decodeInvocation_def
|
||||
Let_def split_def isCap_simps
|
||||
cong: if_cong invocation_label.case_cong arch_invocation_label.case_cong list.case_cong prod.case_cong
|
||||
split del: if_split)
|
||||
|
|
@ -1813,7 +1813,7 @@ lemma arch_decodeInvocation_wf[wp]:
|
|||
apply (simp add: ex_cte_cap_to'_def cte_wp_at_ctes_of)
|
||||
apply (rule_tac x=ba in exI)
|
||||
apply (simp add: diminished_cte_refs')
|
||||
apply (simp add: decodeARMMMUInvocation_def ARM_H.decodeInvocation_def
|
||||
apply (simp add: decodeARMMMUInvocation_def X64_H.decodeInvocation_def
|
||||
Let_def split_def isCap_simps
|
||||
cong: if_cong split del: if_split)
|
||||
apply (cases "invocation_type label = ArchInvocationLabel ARMPageMap")
|
||||
|
|
@ -1876,17 +1876,17 @@ lemma arch_decodeInvocation_wf[wp]:
|
|||
apply (thin_tac "Ball S P" for S P)
|
||||
apply (erule cte_wp_at_weakenE')
|
||||
apply (clarsimp simp: is_arch_update'_def isCap_simps dest!: diminished_capMaster)
|
||||
apply (cases "ARM_H.isPageFlushLabel (invocation_type label)")
|
||||
apply (clarsimp simp: ARM_H.isPageFlushLabel_def split: invocation_label.splits arch_invocation_label.splits)
|
||||
apply (cases "X64_H.isPageFlushLabel (invocation_type label)")
|
||||
apply (clarsimp simp: X64_H.isPageFlushLabel_def split: invocation_label.splits arch_invocation_label.splits)
|
||||
apply (rule arch_decodeARMPageFlush_wf,
|
||||
clarsimp simp: ARM_H.isPageFlushLabel_def)+
|
||||
clarsimp simp: X64_H.isPageFlushLabel_def)+
|
||||
apply (cases "invocation_type label = ArchInvocationLabel ARMPageGetAddress")
|
||||
apply (simp split del: if_split)
|
||||
apply (rule hoare_pre, wp)
|
||||
apply (clarsimp simp: valid_arch_inv'_def valid_page_inv'_def)
|
||||
apply (simp add: ARM_H.isPageFlushLabel_def throwError_R'
|
||||
apply (simp add: X64_H.isPageFlushLabel_def throwError_R'
|
||||
split: invocation_label.split_asm arch_invocation_label.split_asm)
|
||||
apply (simp add: decodeARMMMUInvocation_def ARM_H.decodeInvocation_def
|
||||
apply (simp add: decodeARMMMUInvocation_def X64_H.decodeInvocation_def
|
||||
Let_def split_def isCap_simps vs_entry_align_def
|
||||
cong: if_cong list.case_cong invocation_label.case_cong arch_invocation_label.case_cong prod.case_cong
|
||||
split del: if_split)
|
||||
|
|
@ -1897,7 +1897,7 @@ lemma arch_decodeInvocation_wf[wp]:
|
|||
simp add: valid_arch_inv'_def valid_pti'_def unlessE_whenE|
|
||||
rule_tac x="fst p" in hoare_imp_eq_substR
|
||||
)+)
|
||||
apply (rule_tac Q'="\<lambda>b c. ko_at' ARM_H.pde.InvalidPDE (b + (hd args >> 20 << 2)) c \<longrightarrow>
|
||||
apply (rule_tac Q'="\<lambda>b c. ko_at' X64_H.pde.InvalidPDE (b + (hd args >> 20 << 2)) c \<longrightarrow>
|
||||
cte_wp_at'
|
||||
(is_arch_update'
|
||||
(capability.ArchObjectCap (arch_capability.PageTableCap word (Some (snd p, hd args >> 20 << 20)))))
|
||||
|
|
@ -1933,8 +1933,8 @@ lemma arch_decodeInvocation_wf[wp]:
|
|||
invs_valid_objs' vs_entry_align_def and_not_mask[symmetric])
|
||||
apply (erule order_le_less_trans[rotated])
|
||||
apply (rule word_and_le2)
|
||||
apply (simp add: decodeARMMMUInvocation_def ARM_H.decodeInvocation_def isCap_simps Let_def)
|
||||
apply(cases "ARM_H.isPDFlushLabel (invocation_type label)", simp_all)
|
||||
apply (simp add: decodeARMMMUInvocation_def X64_H.decodeInvocation_def isCap_simps Let_def)
|
||||
apply(cases "X64_H.isPDFlushLabel (invocation_type label)", simp_all)
|
||||
apply(cases args; simp)
|
||||
apply(wp)
|
||||
defer
|
||||
|
|
@ -1988,7 +1988,7 @@ lemma arch_pinv_nosch[wp]:
|
|||
"\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
|
||||
Arch.performInvocation invok
|
||||
\<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
|
||||
by (simp add: ARM_H.performInvocation_def) wp
|
||||
by (simp add: X64_H.performInvocation_def) wp
|
||||
|
||||
lemmas setObject_cte_st_tcb_at' [wp] = setCTE_pred_tcb_at' [unfolded setCTE_def]
|
||||
|
||||
|
|
@ -2050,26 +2050,26 @@ proof(cases ai)
|
|||
txt {* The preservation rules for each invocation have already been proved by crunch, so
|
||||
this just becomes a case distinction. *}
|
||||
case InvokePage thus ?thesis
|
||||
by (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def,
|
||||
by (simp add: X64_H.performInvocation_def performARMMMUInvocation_def,
|
||||
wp performPageInvocation_st_tcb_at', fastforce elim!: pred_tcb'_weakenE)
|
||||
next
|
||||
case InvokeASIDControl thus ?thesis
|
||||
by (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def
|
||||
by (simp add: X64_H.performInvocation_def performARMMMUInvocation_def
|
||||
valid_arch_inv'_def,
|
||||
wp performASIDControlInvocation_st_tcb_at', fastforce elim!: pred_tcb'_weakenE)
|
||||
next
|
||||
case InvokeASIDPool thus ?thesis
|
||||
by (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def
|
||||
by (simp add: X64_H.performInvocation_def performARMMMUInvocation_def
|
||||
valid_arch_inv'_def,
|
||||
wp performASIDPoolInvocation_st_tcb_at', fastforce elim!: pred_tcb'_weakenE)
|
||||
next
|
||||
case InvokePageTable thus ?thesis
|
||||
by (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def
|
||||
by (simp add: X64_H.performInvocation_def performARMMMUInvocation_def
|
||||
valid_arch_inv'_def,
|
||||
wp performPageTableInvocation_st_tcb_at', fastforce elim!: pred_tcb'_weakenE)
|
||||
next
|
||||
case InvokePageDirectory thus ?thesis
|
||||
by (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def
|
||||
by (simp add: X64_H.performInvocation_def performARMMMUInvocation_def
|
||||
valid_arch_inv'_def,
|
||||
wp performPageDirectoryInvocation_st_tcb_at', fastforce elim!: pred_tcb'_weakenE)
|
||||
qed
|
||||
|
|
@ -2100,7 +2100,7 @@ crunch cte_wp_at': "Arch.finaliseCap" "cte_wp_at' P p"
|
|||
lemma invs_asid_table_strenghten':
|
||||
"invs' s \<and> asid_pool_at' ap s \<and> asid \<le> 2 ^ asid_high_bits - 1 \<longrightarrow>
|
||||
invs' (s\<lparr>ksArchState :=
|
||||
armKSASIDTable_update (\<lambda>_. (armKSASIDTable \<circ> ksArchState) s(asid \<mapsto> ap)) (ksArchState s)\<rparr>)"
|
||||
x64KSASIDTable_update (\<lambda>_. (x64KSASIDTable \<circ> ksArchState) s(asid \<mapsto> ap)) (ksArchState s)\<rparr>)"
|
||||
apply (clarsimp simp: invs'_def valid_state'_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_global_refs'_def global_refs'_def)
|
||||
|
|
@ -2256,7 +2256,7 @@ lemma arch_performInvocation_invs':
|
|||
"\<lbrace>invs' and ct_active' and valid_arch_inv' invocation\<rbrace>
|
||||
Arch.performInvocation invocation
|
||||
\<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
unfolding ARM_H.performInvocation_def
|
||||
unfolding X64_H.performInvocation_def
|
||||
by (cases invocation,
|
||||
simp_all add: performARMMMUInvocation_def valid_arch_inv'_def,
|
||||
(wp|simp)+)
|
||||
|
|
|
|||
|
|
@ -64,7 +64,7 @@ lemma maskCapRights_twice:
|
|||
split del: if_split)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability)
|
||||
apply (simp_all add: ARM_H.maskCapRights_def isCap_simps Let_def
|
||||
apply (simp_all add: X64_H.maskCapRights_def isCap_simps Let_def
|
||||
maskVMRights_def
|
||||
split del: if_split)
|
||||
apply (simp split: vmrights.split bool.split)
|
||||
|
|
@ -100,7 +100,7 @@ lemma cap_relation_NullCap:
|
|||
apply simp
|
||||
apply simp
|
||||
apply (clarsimp simp: word_size word_size_def)
|
||||
apply (clarsimp simp: ARM_H.updateCapData_def isCap_simps split del: if_split)
|
||||
apply (clarsimp simp: X64_H.updateCapData_def isCap_simps split del: if_split)
|
||||
done
|
||||
|
||||
(* Sometimes I need something about the state. This is neater (IMHO) and req *)
|
||||
|
|
@ -399,7 +399,7 @@ lemma mask_Zombiness[simp]:
|
|||
"isZombie (maskCapRights R cap) = isZombie cap"
|
||||
apply (cases cap, simp_all add: maskCapRights_def isCap_simps Let_def)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability, simp_all add: ARM_H.maskCapRights_def Let_def)
|
||||
apply (case_tac arch_capability, simp_all add: X64_H.maskCapRights_def Let_def)
|
||||
done
|
||||
|
||||
lemma updateCapData_Zombie:
|
||||
|
|
@ -426,7 +426,7 @@ lemma capBadge_updateCapData_True:
|
|||
"updateCapData True x c \<noteq> NullCap \<Longrightarrow> capBadge (updateCapData True x c) = capBadge c"
|
||||
apply (simp add: updateCapData_def isCap_simps Let_def
|
||||
split: if_split_asm split del: if_split)
|
||||
apply (simp add: ARM_H.updateCapData_def)
|
||||
apply (simp add: X64_H.updateCapData_def)
|
||||
done
|
||||
|
||||
lemma badge_derived_updateCapData:
|
||||
|
|
@ -613,7 +613,7 @@ lemma finalise_cap_not_reachable_pg_cap:
|
|||
valid_arch_objs and
|
||||
valid_objs and
|
||||
cte_wp_at (op = cap) slot and
|
||||
(\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s)
|
||||
(\<lambda>s. valid_asid_table (x64_asid_table (arch_state s)) s)
|
||||
and K (is_pg_cap cap \<longrightarrow> is_final)
|
||||
\<rbrace> finalise_cap cap is_final
|
||||
\<lbrace>\<lambda>_ s. \<not> reachable_pg_cap cap s\<rbrace>"
|
||||
|
|
@ -4946,7 +4946,7 @@ proof -
|
|||
apply (erule_tac x=p in allE)
|
||||
apply simp
|
||||
apply (case_tac n)
|
||||
apply (clarsimp simp: s_d_swap_def nullMDBNode_def ARM_H.nullPointer_def split: if_split_asm)
|
||||
apply (clarsimp simp: s_d_swap_def nullMDBNode_def X64_H.nullPointer_def split: if_split_asm)
|
||||
done
|
||||
qed
|
||||
|
||||
|
|
@ -8567,7 +8567,7 @@ lemma sameRegion_cap'_src [simp]:
|
|||
apply (case_tac "isReplyCap src_cap")
|
||||
apply simp
|
||||
apply (clarsimp simp: capMasterCap_def split: capability.splits arch_capability.splits)
|
||||
apply (auto simp: sameRegionAs_def ARM_H.sameRegionAs_def isCap_simps split: if_split_asm)
|
||||
apply (auto simp: sameRegionAs_def X64_H.sameRegionAs_def isCap_simps split: if_split_asm)
|
||||
done
|
||||
|
||||
lemma chunked':
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ imports
|
|||
"../../invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI"
|
||||
begin
|
||||
|
||||
context Arch begin global_naming ARM_A (*FIXME: arch_split*)
|
||||
context Arch begin global_naming X64_A (*FIXME: arch_split*)
|
||||
|
||||
lemmas final_matters_def = final_matters_def[simplified final_matters_arch_def]
|
||||
|
||||
|
|
@ -124,7 +124,7 @@ lemma same_arch_region_as_relation:
|
|||
arch_same_region_as c c' =
|
||||
sameRegionAs (ArchObjectCap d) (ArchObjectCap d')"
|
||||
apply (cases c)
|
||||
apply ((cases c', auto simp: ARM_H.sameRegionAs_def sameRegionAs_def Let_def isCap_simps)[1])+
|
||||
apply ((cases c', auto simp: X64_H.sameRegionAs_def sameRegionAs_def Let_def isCap_simps)[1])+
|
||||
done
|
||||
|
||||
lemma is_phyiscal_relation:
|
||||
|
|
@ -145,7 +145,7 @@ lemma obj_size_relation:
|
|||
split: option.splits sum.splits)
|
||||
apply (rename_tac arch_cap)
|
||||
apply (case_tac arch_cap,
|
||||
simp_all add: objBits_def ARM_H.capUntypedSize_def asid_low_bits_def
|
||||
simp_all add: objBits_def X64_H.capUntypedSize_def asid_low_bits_def
|
||||
pageBits_def)
|
||||
done
|
||||
|
||||
|
|
@ -347,7 +347,7 @@ lemma maskCapRights [simp]:
|
|||
lemma maskCap_valid [simp]:
|
||||
"s \<turnstile>' RetypeDecls_H.maskCapRights R cap = s \<turnstile>' cap"
|
||||
by (simp add: valid_cap'_def maskCapRights_def isCap_simps
|
||||
capAligned_def ARM_H.maskCapRights_def
|
||||
capAligned_def X64_H.maskCapRights_def
|
||||
split: capability.split arch_capability.split
|
||||
split del: if_split)
|
||||
|
||||
|
|
@ -447,7 +447,7 @@ proof -
|
|||
apply (rename_tac arch_cap)
|
||||
apply (case_tac arch_cap)
|
||||
apply (simp_all add: simps arch_update_cap_data_def
|
||||
ARM_H.updateCapData_def)[5]
|
||||
X64_H.updateCapData_def)[5]
|
||||
-- CNodeCap
|
||||
apply (simp add: simps word_bits_def the_cnode_cap_def andCapRights_def
|
||||
rightsFromWord_def data_to_rights_def nth_ucast)
|
||||
|
|
@ -1523,7 +1523,7 @@ lemma capASID_update [simp]:
|
|||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability,
|
||||
simp_all add: updateCapData_def
|
||||
ARM_H.updateCapData_def
|
||||
X64_H.updateCapData_def
|
||||
isCap_simps Let_def)
|
||||
done
|
||||
|
||||
|
|
@ -1534,7 +1534,7 @@ lemma cap_vptr_update' [simp]:
|
|||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability,
|
||||
simp_all add: updateCapData_def
|
||||
ARM_H.updateCapData_def
|
||||
X64_H.updateCapData_def
|
||||
isCap_simps Let_def)
|
||||
done
|
||||
|
||||
|
|
@ -1545,7 +1545,7 @@ lemma cap_asid_base_update' [simp]:
|
|||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability,
|
||||
simp_all add: updateCapData_def
|
||||
ARM_H.updateCapData_def
|
||||
X64_H.updateCapData_def
|
||||
isCap_simps Let_def)
|
||||
done
|
||||
|
||||
|
|
@ -1555,7 +1555,7 @@ lemma updateCapData_Master:
|
|||
apply (cases cap, simp_all add: updateCapData_def isCap_simps Let_def
|
||||
split: if_split_asm)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability, simp_all add: ARM_H.updateCapData_def)
|
||||
apply (case_tac arch_capability, simp_all add: X64_H.updateCapData_def)
|
||||
done
|
||||
|
||||
lemma updateCapData_Reply:
|
||||
|
|
@ -1591,7 +1591,7 @@ lemma capASID_mask [simp]:
|
|||
apply (cases c, simp_all add: maskCapRights_def isCap_simps Let_def)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability,
|
||||
simp_all add: maskCapRights_def ARM_H.maskCapRights_def isCap_simps Let_def)
|
||||
simp_all add: maskCapRights_def X64_H.maskCapRights_def isCap_simps Let_def)
|
||||
done
|
||||
|
||||
lemma cap_vptr_mask' [simp]:
|
||||
|
|
@ -1600,7 +1600,7 @@ lemma cap_vptr_mask' [simp]:
|
|||
apply (cases c, simp_all add: maskCapRights_def isCap_simps Let_def)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability,
|
||||
simp_all add: maskCapRights_def ARM_H.maskCapRights_def isCap_simps Let_def)
|
||||
simp_all add: maskCapRights_def X64_H.maskCapRights_def isCap_simps Let_def)
|
||||
done
|
||||
|
||||
lemma cap_asid_base_mask' [simp]:
|
||||
|
|
@ -1609,7 +1609,7 @@ lemma cap_asid_base_mask' [simp]:
|
|||
apply (cases c, simp_all add: maskCapRights_def isCap_simps Let_def)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability,
|
||||
simp_all add: maskCapRights_def ARM_H.maskCapRights_def isCap_simps Let_def)
|
||||
simp_all add: maskCapRights_def X64_H.maskCapRights_def isCap_simps Let_def)
|
||||
done
|
||||
|
||||
lemma weak_derived_maskCapRights:
|
||||
|
|
@ -1891,7 +1891,7 @@ lemma other_obj_relation_KOCTE[simp]:
|
|||
"\<not> other_obj_relation ko (KOCTE cte)"
|
||||
by (simp add: other_obj_relation_def
|
||||
split: Structures_A.kernel_object.splits
|
||||
ARM_A.arch_kernel_obj.splits)
|
||||
X64_A.arch_kernel_obj.splits)
|
||||
|
||||
lemma cte_map_pulls_tcb_to_abstract:
|
||||
"\<lbrakk> y = cte_map z; pspace_relation (kheap s) (ksPSpace s');
|
||||
|
|
@ -1904,7 +1904,7 @@ lemma cte_map_pulls_tcb_to_abstract:
|
|||
apply (erule(1) obj_relation_cutsE, simp_all split: if_split_asm)
|
||||
apply (clarsimp simp: other_obj_relation_def
|
||||
split: Structures_A.kernel_object.split_asm
|
||||
ARM_A.arch_kernel_obj.split_asm)
|
||||
X64_A.arch_kernel_obj.split_asm)
|
||||
apply (drule tcb_cases_related2)
|
||||
apply clarsimp
|
||||
apply (frule(1) cte_wp_at_tcbI [OF _ _ TrueI, where t="(a, b)" for a b, simplified])
|
||||
|
|
@ -2183,7 +2183,7 @@ lemma pspace_relation_cte_wp_atI':
|
|||
apply (erule(1) obj_relation_cutsE, simp_all split: if_split_asm)
|
||||
apply (simp add: other_obj_relation_def
|
||||
split: Structures_A.kernel_object.split_asm
|
||||
ARM_A.arch_kernel_obj.split_asm)
|
||||
X64_A.arch_kernel_obj.split_asm)
|
||||
apply (subgoal_tac "n = x - y", clarsimp)
|
||||
apply (drule tcb_cases_related2, clarsimp)
|
||||
apply (intro exI, rule conjI)
|
||||
|
|
@ -2899,7 +2899,7 @@ lemma updateMDB_pspace_relation:
|
|||
apply (rule pspace_dom_relatedE, assumption+)
|
||||
apply (rule obj_relation_cutsE, assumption+, simp_all split: if_split_asm)[1]
|
||||
apply (clarsimp split: Structures_A.kernel_object.split_asm
|
||||
ARM_A.arch_kernel_obj.split_asm
|
||||
X64_A.arch_kernel_obj.split_asm
|
||||
simp: other_obj_relation_def)
|
||||
apply (frule(1) tcb_cte_cases_aligned_helpers(1))
|
||||
apply (frule(1) tcb_cte_cases_aligned_helpers(2))
|
||||
|
|
|
|||
|
|
@ -27,12 +27,12 @@ lemma capUntypedPtr_simps [simp]:
|
|||
"capUntypedPtr (UntypedCap d r n f) = r"
|
||||
"capUntypedPtr (CNodeCap r n g n2) = r"
|
||||
"capUntypedPtr (ReplyCap r m) = r"
|
||||
"Arch.capUntypedPtr (ARM_H.ASIDPoolCap r asid) = r"
|
||||
"Arch.capUntypedPtr (ARM_H.PageCap d r rghts sz mapdata) = r"
|
||||
"Arch.capUntypedPtr (ARM_H.PageTableCap r mapdata2) = r"
|
||||
"Arch.capUntypedPtr (ARM_H.PageDirectoryCap r mapdata3) = r"
|
||||
"Arch.capUntypedPtr (X64_H.ASIDPoolCap r asid) = r"
|
||||
"Arch.capUntypedPtr (X64_H.PageCap d r rghts sz mapdata) = r"
|
||||
"Arch.capUntypedPtr (X64_H.PageTableCap r mapdata2) = r"
|
||||
"Arch.capUntypedPtr (X64_H.PageDirectoryCap r mapdata3) = r"
|
||||
by (auto simp: capUntypedPtr_def
|
||||
ARM_H.capUntypedPtr_def)
|
||||
X64_H.capUntypedPtr_def)
|
||||
|
||||
lemma rights_mask_map_UNIV [simp]:
|
||||
"rights_mask_map UNIV = allRights"
|
||||
|
|
@ -43,7 +43,7 @@ declare insert_UNIV[simp]
|
|||
lemma maskCapRights_allRights [simp]:
|
||||
"maskCapRights allRights c = c"
|
||||
unfolding maskCapRights_def isCap_defs allRights_def
|
||||
ARM_H.maskCapRights_def maskVMRights_def
|
||||
X64_H.maskCapRights_def maskVMRights_def
|
||||
by (cases c) (simp_all add: Let_def split: arch_capability.split vmrights.split)
|
||||
|
||||
lemma diminished_refl'[simp]:
|
||||
|
|
@ -613,7 +613,7 @@ lemma isDomainCap [simp]:
|
|||
|
||||
lemma isPhysicalCap[simp]:
|
||||
"isPhysicalCap cap = (capClass cap = PhysicalClass)"
|
||||
by (simp add: isPhysicalCap_def ARM_H.isPhysicalCap_def
|
||||
by (simp add: isPhysicalCap_def X64_H.isPhysicalCap_def
|
||||
split: capability.split arch_capability.split)
|
||||
|
||||
definition
|
||||
|
|
@ -759,7 +759,7 @@ lemma isCap_Master:
|
|||
lemma capUntypedSize_capBits:
|
||||
"capClass cap = PhysicalClass \<Longrightarrow> capUntypedSize cap = 2 ^ (capBits cap)"
|
||||
apply (simp add: capUntypedSize_def objBits_simps
|
||||
ARM_H.capUntypedSize_def
|
||||
X64_H.capUntypedSize_def
|
||||
split: capability.splits arch_capability.splits
|
||||
zombie_type.splits)
|
||||
apply fastforce
|
||||
|
|
@ -790,7 +790,7 @@ lemma sameRegionAs_def2:
|
|||
apply (simp add: capMasterCap_def sameRegionAs_def isArchPageCap_def
|
||||
split: capability.split
|
||||
split del: if_split cong: if_cong)
|
||||
apply (simp add: ARM_H.sameRegionAs_def isCap_simps
|
||||
apply (simp add: X64_H.sameRegionAs_def isCap_simps
|
||||
split: arch_capability.split
|
||||
split del: if_split cong: if_cong)
|
||||
apply (clarsimp simp: capRange_def Let_def)
|
||||
|
|
@ -810,9 +810,9 @@ lemma sameObjectAs_def2:
|
|||
apply (simp add: sameObjectAs_def sameRegionAs_def2
|
||||
isCap_simps capMasterCap_def
|
||||
split: capability.split)
|
||||
apply (clarsimp simp: ARM_H.sameObjectAs_def isCap_simps
|
||||
apply (clarsimp simp: X64_H.sameObjectAs_def isCap_simps
|
||||
split: arch_capability.split cong: if_cong)
|
||||
apply (clarsimp simp: ARM_H.sameRegionAs_def isCap_simps
|
||||
apply (clarsimp simp: X64_H.sameRegionAs_def isCap_simps
|
||||
split del: if_split cong: if_cong)
|
||||
apply (simp add: capRange_def interval_empty)
|
||||
apply fastforce
|
||||
|
|
@ -952,7 +952,7 @@ lemma capMasterCap_maskCapRights[simp]:
|
|||
simp add: maskCapRights_def Let_def isCap_simps capMasterCap_def)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability;
|
||||
simp add: ARM_H.maskCapRights_def Let_def isCap_simps)
|
||||
simp add: X64_H.maskCapRights_def Let_def isCap_simps)
|
||||
done
|
||||
|
||||
lemma capBadge_maskCapRights[simp]:
|
||||
|
|
@ -962,7 +962,7 @@ lemma capBadge_maskCapRights[simp]:
|
|||
simp add: maskCapRights_def Let_def isCap_simps capBadge_def)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability;
|
||||
simp add: ARM_H.maskCapRights_def Let_def isCap_simps)
|
||||
simp add: X64_H.maskCapRights_def Let_def isCap_simps)
|
||||
done
|
||||
|
||||
lemma maskCapRights_region [simp]:
|
||||
|
|
@ -1042,7 +1042,7 @@ lemma capUntypedSize_range:
|
|||
apply simp
|
||||
apply (clarsimp simp add: capAligned_def)
|
||||
apply (erule is_aligned_get_word_bits)
|
||||
apply (simp add: capUntypedSize_def ARM_H.capUntypedSize_def objBits_simps
|
||||
apply (simp add: capUntypedSize_def X64_H.capUntypedSize_def objBits_simps
|
||||
isCap_simps
|
||||
split: capability.splits arch_capability.split
|
||||
zombie_type.splits)
|
||||
|
|
|
|||
|
|
@ -3732,7 +3732,7 @@ lemma deriveCap_derived:
|
|||
| rule is_derived'_def[THEN meta_eq_to_obj_eq, THEN iffD2])+)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability;
|
||||
simp add: ARM_H.deriveCap_def Let_def isCap_simps
|
||||
simp add: X64_H.deriveCap_def Let_def isCap_simps
|
||||
split: if_split,
|
||||
safe)
|
||||
apply ((wp throwError_validE_R undefined_validE_R
|
||||
|
|
@ -6178,7 +6178,7 @@ lemma cte_refs_maskCapRights[simp]:
|
|||
"cte_refs' (maskCapRights rghts cap) = cte_refs' cap"
|
||||
by (rule ext, cases cap,
|
||||
simp_all add: maskCapRights_def isCap_defs Let_def
|
||||
ARM_H.maskCapRights_def
|
||||
X64_H.maskCapRights_def
|
||||
split del: if_split
|
||||
split: arch_capability.split)
|
||||
|
||||
|
|
@ -6427,7 +6427,7 @@ lemma diminished_Untyped' :
|
|||
(* 6 subgoals *)
|
||||
apply (rename_tac arch_capability R)
|
||||
apply (case_tac arch_capability)
|
||||
apply (clarsimp simp: isCap_simps ARM_H.maskCapRights_def maskCapRights_def
|
||||
apply (clarsimp simp: isCap_simps X64_H.maskCapRights_def maskCapRights_def
|
||||
diminished'_def Let_def)+
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -109,7 +109,7 @@ defs deletionIsSafe_def:
|
|||
|
||||
defs ksASIDMapSafe_def:
|
||||
"ksASIDMapSafe \<equiv> \<lambda>s. \<forall>asid hw_asid pd.
|
||||
armKSASIDMap (ksArchState s) asid = Some (hw_asid,pd) \<longrightarrow> page_directory_at' pd s"
|
||||
x64KSASIDMap (ksArchState s) asid = Some (hw_asid,pd) \<longrightarrow> page_directory_at' pd s"
|
||||
|
||||
defs cNodePartialOverlap_def:
|
||||
"cNodePartialOverlap \<equiv> \<lambda>cns inRange. \<exists>p n. cns p = Some n
|
||||
|
|
@ -542,7 +542,7 @@ lemma ksASIDMapSafeI:
|
|||
prefer 2
|
||||
apply fastforce
|
||||
apply (clarsimp simp: valid_asid_map_def graph_of_def)
|
||||
apply (subgoal_tac "arm_asid_map (arch_state s) asid = Some (hw_asid, pd)")
|
||||
apply (subgoal_tac "x64_asid_map (arch_state s) asid = Some (hw_asid, pd)")
|
||||
prefer 2
|
||||
apply (clarsimp simp: state_relation_def arch_state_relation_def)
|
||||
apply (erule allE)+
|
||||
|
|
@ -877,7 +877,7 @@ lemma valid_cap':
|
|||
apply blast
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability,
|
||||
simp_all add: ARM_H.capUntypedPtr_def
|
||||
simp_all add: X64_H.capUntypedPtr_def
|
||||
page_table_at'_def page_directory_at'_def
|
||||
shiftl_t2n
|
||||
del: atLeastAtMost_iff)[1]
|
||||
|
|
@ -2298,11 +2298,11 @@ proof -
|
|||
done
|
||||
qed
|
||||
|
||||
lemmas getObjSize_simps = ARM_H.getObjectSize_def[split_simps ARM_H.object_type.split apiobject_type.split]
|
||||
lemmas getObjSize_simps = X64_H.getObjectSize_def[split_simps X64_H.object_type.split apiobject_type.split]
|
||||
|
||||
lemma arch_toAPIType_simps:
|
||||
"ARM_H.toAPIType ty = Some a \<Longrightarrow> ty = APIObjectType a"
|
||||
by (case_tac ty,auto simp:ARM_H.toAPIType_def)
|
||||
"X64_H.toAPIType ty = Some a \<Longrightarrow> ty = APIObjectType a"
|
||||
by (case_tac ty,auto simp:X64_H.toAPIType_def)
|
||||
|
||||
lemma createObject_cte_wp_at':
|
||||
"\<lbrace>\<lambda>s. Types_H.getObjectSize ty us < word_bits \<and>
|
||||
|
|
@ -2317,7 +2317,7 @@ lemma createObject_cte_wp_at':
|
|||
apply (wpc
|
||||
| wp createObjects_orig_cte_wp_at'[where sz = "(Types_H.getObjectSize ty us)"]
|
||||
threadSet_cte_wp_at'
|
||||
| simp add: ARM_H.createObject_def placeNewDataObject_def
|
||||
| simp add: X64_H.createObject_def placeNewDataObject_def
|
||||
unless_def placeNewObject_def2 objBitsKO_simps range_cover_full
|
||||
curDomain_def pageBits_def ptBits_def
|
||||
pdBits_def getObjSize_simps archObjSize_def
|
||||
|
|
@ -2690,7 +2690,7 @@ lemma magnitudeCheck_det:
|
|||
|
||||
lemma getPDE_det:
|
||||
"ko_wp_at' (op = (KOArch (KOPDE pde))) p s
|
||||
\<Longrightarrow> getObject p s = ({((pde::ARM_H.pde),s)},False)"
|
||||
\<Longrightarrow> getObject p s = ({((pde::X64_H.pde),s)},False)"
|
||||
apply (clarsimp simp:ko_wp_at'_def getObject_def split_def
|
||||
bind_def gets_def return_def get_def
|
||||
assert_opt_def split:if_splits)
|
||||
|
|
@ -2840,7 +2840,7 @@ lemma getPDE_placeNewObject_commute:
|
|||
|
||||
lemma storePDE_det:
|
||||
"ko_wp_at' (op = (KOArch (KOPDE pde))) ptr s
|
||||
\<Longrightarrow> storePDE ptr (new_pde::ARM_H.pde) s =
|
||||
\<Longrightarrow> storePDE ptr (new_pde::X64_H.pde) s =
|
||||
modify
|
||||
(ksPSpace_update (\<lambda>_. ksPSpace s(ptr \<mapsto> KOArch (KOPDE new_pde)))) s"
|
||||
apply (clarsimp simp:ko_wp_at'_def storePDE_def split_def
|
||||
|
|
@ -2979,7 +2979,7 @@ lemma modify_mapM_x:
|
|||
|
||||
lemma doMachineOp_storePDE_commute:
|
||||
"monad_commute (pde_at' src) (doMachineOp f)
|
||||
(storePDE src (new_pde::ARM_H.pde))"
|
||||
(storePDE src (new_pde::X64_H.pde))"
|
||||
proof -
|
||||
have eq_fail: "\<And>sa ks. snd (doMachineOp f (sa\<lparr>ksPSpace := ks\<rparr>)) = snd (doMachineOp f sa)"
|
||||
apply (clarsimp simp:doMachineOp_def bind_def return_def gets_def
|
||||
|
|
@ -3027,7 +3027,7 @@ lemma storePDE_placeNewObject_commute:
|
|||
pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) and
|
||||
K (is_aligned ptr (objBitsKO (injectKOS val) + sz) \<and>
|
||||
objBitsKO (injectKOS val) + sz < word_bits) )
|
||||
(placeNewObject ptr val sz) (storePDE src (new_pde::ARM_H.pde))"
|
||||
(placeNewObject ptr val sz) (storePDE src (new_pde::X64_H.pde))"
|
||||
apply (rule commute_name_pre_state)
|
||||
apply (clarsimp simp:typ_at'_def ko_wp_at'_def)
|
||||
apply (case_tac ko,simp_all)
|
||||
|
|
@ -3127,7 +3127,7 @@ lemma storePDE_setCTE_commute:
|
|||
shows "monad_commute
|
||||
(pde_at' ptr and pspace_distinct' and pspace_aligned' and
|
||||
cte_wp_at' (\<lambda>_. True) src)
|
||||
(setCTE src cte) (storePDE ptr (new_pde::ARM_H.pde))"
|
||||
(setCTE src cte) (storePDE ptr (new_pde::X64_H.pde))"
|
||||
apply (rule commute_name_pre_state)
|
||||
apply (clarsimp simp:typ_at'_def ko_wp_at'_def)
|
||||
apply (case_tac ko,simp_all)
|
||||
|
|
@ -3174,7 +3174,7 @@ lemma storePDE_setCTE_commute:
|
|||
lemma setCTE_gets_globalPD_commute:
|
||||
"monad_commute
|
||||
(cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned')
|
||||
(setCTE src cte) (gets (armKSGlobalPD \<circ> ksArchState))"
|
||||
(setCTE src cte) (gets (x64KSGlobalPD \<circ> ksArchState))"
|
||||
apply (simp add:setCTE_def2)
|
||||
apply (rule monad_commute_guard_imp)
|
||||
apply (rule commute_commute[OF monad_commute_split[where Q = "\<lambda>r. \<top>"]])
|
||||
|
|
@ -3191,7 +3191,7 @@ lemma placeNewObject_gets_globalPD_commute:
|
|||
(pspace_distinct' and pspace_aligned' and
|
||||
K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and
|
||||
pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) )
|
||||
(placeNewObject ptr val us) (gets (armKSGlobalPD \<circ> ksArchState))"
|
||||
(placeNewObject ptr val us) (gets (x64KSGlobalPD \<circ> ksArchState))"
|
||||
apply (rule commute_name_pre_state)
|
||||
apply (rule monad_commute_guard_imp)
|
||||
apply (rule_tac commute_rewrite[where Q = "\<lambda>s.
|
||||
|
|
@ -3278,8 +3278,8 @@ lemma placeNewObject_valid_arch_state:
|
|||
lemma placeNewObject_pd_at':
|
||||
"\<lbrace>K (is_aligned ptr pdBits) and pspace_no_overlap' ptr pdBits and
|
||||
pspace_aligned' and pspace_distinct'\<rbrace>
|
||||
placeNewObject ptr (makeObject::ARM_H.pde)
|
||||
(pdBits - objBits (makeObject::ARM_H.pde))
|
||||
placeNewObject ptr (makeObject::X64_H.pde)
|
||||
(pdBits - objBits (makeObject::X64_H.pde))
|
||||
\<lbrace>\<lambda>rv s. page_directory_at' ptr s\<rbrace>"
|
||||
apply (simp add:page_directory_at'_def typ_at'_def)
|
||||
apply (rule hoare_pre)
|
||||
|
|
@ -3518,11 +3518,11 @@ lemma createObject_setCTE_commute:
|
|||
apply (clarsimp simp: range_cover_def is_aligned_mask)
|
||||
apply (clarsimp simp: createObject_def)
|
||||
apply (case_tac ty,
|
||||
simp_all add: ARM_H.toAPIType_def)
|
||||
simp_all add: X64_H.toAPIType_def)
|
||||
apply (rename_tac apiobject_type)
|
||||
apply (case_tac apiobject_type)
|
||||
apply (simp_all add:
|
||||
ARM_H.getObjectSize_def apiGetObjectSize_def
|
||||
X64_H.getObjectSize_def apiGetObjectSize_def
|
||||
tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def
|
||||
cteSizeBits_def)
|
||||
-- Untyped
|
||||
|
|
@ -3556,7 +3556,7 @@ lemma createObject_setCTE_commute:
|
|||
-- "Arch Objects"
|
||||
apply ((rule monad_commute_guard_imp[OF commute_commute]
|
||||
, rule monad_commute_split[OF commute_commute[OF return_commute]]
|
||||
, clarsimp simp: ARM_H.createObject_def
|
||||
, clarsimp simp: X64_H.createObject_def
|
||||
placeNewDataObject_def bind_assoc split
|
||||
del: if_splits
|
||||
,(rule monad_commute_split return_commute[THEN commute_commute]
|
||||
|
|
@ -3742,7 +3742,7 @@ lemma createObject_gsUntypedZeroRanges_commute:
|
|||
\<top>
|
||||
(RetypeDecls_H.createObject ty ptr us dev)
|
||||
(modify (\<lambda>s. s \<lparr> gsUntypedZeroRanges := f (gsUntypedZeroRanges s) \<rparr> ))"
|
||||
apply (simp add: createObject_def ARM_H.createObject_def
|
||||
apply (simp add: createObject_def X64_H.createObject_def
|
||||
placeNewDataObject_def
|
||||
placeNewObject_def2 bind_assoc fail_commute
|
||||
return_commute toAPIType_def
|
||||
|
|
@ -4163,15 +4163,15 @@ lemma createNewCaps_pspace_no_overlap':
|
|||
pspace_aligned' and pspace_distinct'" in hoare_strengthen_post)
|
||||
apply (case_tac ty)
|
||||
apply (simp_all add: apiGetObjectSize_def
|
||||
ARM_H.toAPIType_def tcbBlockSizeBits_def
|
||||
ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
|
||||
X64_H.toAPIType_def tcbBlockSizeBits_def
|
||||
X64_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
|
||||
cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def
|
||||
createObjects_def)
|
||||
apply (rule hoare_pre)
|
||||
apply wpc
|
||||
apply (clarsimp simp: apiGetObjectSize_def curDomain_def
|
||||
ARM_H.toAPIType_def tcbBlockSizeBits_def
|
||||
ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
|
||||
X64_H.toAPIType_def tcbBlockSizeBits_def
|
||||
X64_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
|
||||
cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def
|
||||
createObjects_def Arch_createNewCaps_def
|
||||
split: apiobject_type.splits
|
||||
|
|
@ -4182,8 +4182,8 @@ lemma createNewCaps_pspace_no_overlap':
|
|||
apply (intro conjI range_cover_le[where n = "Suc n"] | simp)+
|
||||
apply ((simp add:objBits_simps pageBits_def range_cover_def word_bits_def)+)[5]
|
||||
by ((clarsimp simp: apiGetObjectSize_def
|
||||
ARM_H.toAPIType_def tcbBlockSizeBits_def
|
||||
ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
|
||||
X64_H.toAPIType_def tcbBlockSizeBits_def
|
||||
X64_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def
|
||||
cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def
|
||||
createObjects_def Arch_createNewCaps_def
|
||||
unless_def
|
||||
|
|
@ -4198,7 +4198,7 @@ lemma createNewCaps_pspace_no_overlap':
|
|||
lemma objSize_eq_capBits:
|
||||
"Types_H.getObjectSize ty us = APIType_capBits ty us"
|
||||
apply (case_tac ty)
|
||||
apply (clarsimp simp:ARM_H.getObjectSize_def objBits_simps
|
||||
apply (clarsimp simp:X64_H.getObjectSize_def objBits_simps
|
||||
APIType_capBits_def apiGetObjectSize_def ptBits_def
|
||||
tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def cteSizeBits_def
|
||||
pageBits_def pdBits_def
|
||||
|
|
@ -4213,17 +4213,17 @@ lemma createNewCaps_ret_len:
|
|||
apply (rule hoare_name_pre_state)
|
||||
apply clarsimp
|
||||
apply (case_tac ty)
|
||||
apply (simp_all add:createNewCaps_def ARM_H.toAPIType_def)
|
||||
apply (simp_all add:createNewCaps_def X64_H.toAPIType_def)
|
||||
apply (rule hoare_pre)
|
||||
apply wpc
|
||||
apply ((wp+)|simp add:Arch_createNewCaps_def ARM_H.toAPIType_def
|
||||
apply ((wp+)|simp add:Arch_createNewCaps_def X64_H.toAPIType_def
|
||||
unat_of_nat_minus_1
|
||||
[where 'a=32, folded word_bits_def] |
|
||||
erule hoare_strengthen_post[OF createObjects_ret],clarsimp+ | intro conjI impI)+
|
||||
apply (rule hoare_pre,
|
||||
((wp+)
|
||||
| simp add: Arch_createNewCaps_def toAPIType_def
|
||||
ARM_H.toAPIType_def unat_of_nat_minus_1
|
||||
X64_H.toAPIType_def unat_of_nat_minus_1
|
||||
| erule hoare_strengthen_post[OF createObjects_ret],clarsimp+
|
||||
| intro conjI impI)+)+
|
||||
done
|
||||
|
|
@ -5044,19 +5044,19 @@ proof -
|
|||
apply (erule range_cover.sz(1)[where 'a=32, folded word_bits_def])
|
||||
apply (simp add: createNewCaps_def)
|
||||
apply (case_tac ty)
|
||||
apply (simp add: ARM_H.toAPIType_def
|
||||
apply (simp add: X64_H.toAPIType_def
|
||||
Arch_createNewCaps_def)
|
||||
apply (rename_tac apiobject_type)
|
||||
apply (case_tac apiobject_type)
|
||||
apply (simp_all add: bind_assoc ARM_H.toAPIType_def
|
||||
apply (simp_all add: bind_assoc X64_H.toAPIType_def
|
||||
)
|
||||
-- Untyped
|
||||
apply (simp add: cteSizeBits_def pageBits_def
|
||||
tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def pdBits_def
|
||||
bind_assoc ARM_H.getObjectSize_def
|
||||
bind_assoc X64_H.getObjectSize_def
|
||||
mapM_def sequence_def Retype_H.createObject_def
|
||||
ARM_H.toAPIType_def
|
||||
createObjects_def ARM_H.createObject_def
|
||||
X64_H.toAPIType_def
|
||||
createObjects_def X64_H.createObject_def
|
||||
Arch_createNewCaps_def comp_def
|
||||
apiGetObjectSize_def shiftl_t2n field_simps
|
||||
shiftL_nat mapM_x_def sequence_x_def append
|
||||
|
|
@ -5064,10 +5064,10 @@ proof -
|
|||
-- "TCB, EP, NTFN"
|
||||
apply (simp add: cteSizeBits_def pageBits_def tcbBlockSizeBits_def
|
||||
epSizeBits_def ntfnSizeBits_def pdBits_def bind_assoc
|
||||
ARM_H.getObjectSize_def
|
||||
X64_H.getObjectSize_def
|
||||
sequence_def Retype_H.createObject_def
|
||||
ARM_H.toAPIType_def
|
||||
createObjects_def ARM_H.createObject_def
|
||||
X64_H.toAPIType_def
|
||||
createObjects_def X64_H.createObject_def
|
||||
Arch_createNewCaps_def comp_def
|
||||
apiGetObjectSize_def shiftl_t2n field_simps
|
||||
shiftL_nat append mapM_x_append2
|
||||
|
|
@ -5136,10 +5136,10 @@ proof -
|
|||
apply simp
|
||||
apply (((simp add: cteSizeBits_def pageBits_def tcbBlockSizeBits_def
|
||||
epSizeBits_def ntfnSizeBits_def pdBits_def bind_assoc
|
||||
ARM_H.getObjectSize_def
|
||||
X64_H.getObjectSize_def
|
||||
mapM_def sequence_def Retype_H.createObject_def
|
||||
ARM_H.toAPIType_def
|
||||
createObjects_def ARM_H.createObject_def
|
||||
X64_H.toAPIType_def
|
||||
createObjects_def X64_H.createObject_def
|
||||
Arch_createNewCaps_def comp_def
|
||||
apiGetObjectSize_def shiftl_t2n field_simps
|
||||
shiftL_nat mapM_x_def sequence_x_def append
|
||||
|
|
@ -5150,10 +5150,10 @@ proof -
|
|||
-- CNode
|
||||
apply (simp add: cteSizeBits_def pageBits_def tcbBlockSizeBits_def
|
||||
epSizeBits_def ntfnSizeBits_def pdBits_def bind_assoc
|
||||
ARM_H.getObjectSize_def
|
||||
X64_H.getObjectSize_def
|
||||
mapM_def sequence_def Retype_H.createObject_def
|
||||
ARM_H.toAPIType_def
|
||||
createObjects_def ARM_H.createObject_def
|
||||
X64_H.toAPIType_def
|
||||
createObjects_def X64_H.createObject_def
|
||||
Arch_createNewCaps_def comp_def
|
||||
apiGetObjectSize_def shiftl_t2n field_simps
|
||||
shiftL_nat mapM_x_def sequence_x_def append
|
||||
|
|
@ -5174,15 +5174,15 @@ proof -
|
|||
-- "SmallPageObject"
|
||||
apply (simp add: Arch_createNewCaps_def
|
||||
Retype_H.createObject_def createObjects_def bind_assoc
|
||||
ARM_H.toAPIType_def ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def placeNewDataObject_def)
|
||||
X64_H.toAPIType_def X64_H.toAPIType_def
|
||||
X64_H.createObject_def placeNewDataObject_def)
|
||||
apply (intro conjI impI)
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
objBits_simps)[6]
|
||||
apply (simp add: bind_assoc placeNewObject_def2 objBits_simps
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
pageBits_def add.commute append)
|
||||
apply ((subst gsUserPages_update gsCNodes_update
|
||||
gsUserPages_upd_createObjects'_comm
|
||||
|
|
@ -5192,10 +5192,10 @@ proof -
|
|||
| simp add: modify_modify_bind o_def)+)[1]
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
objBits_simps)[6]
|
||||
apply (simp add: bind_assoc placeNewObject_def2 objBits_simps
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
pageBits_def add.commute append)
|
||||
apply (subst gsUserPages_update gsCNodes_update
|
||||
gsUserPages_upd_createObjects'_comm
|
||||
|
|
@ -5206,15 +5206,15 @@ proof -
|
|||
-- "LargePageObject"
|
||||
apply (simp add: Arch_createNewCaps_def
|
||||
Retype_H.createObject_def createObjects_def bind_assoc
|
||||
ARM_H.toAPIType_def ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def placeNewDataObject_def)
|
||||
X64_H.toAPIType_def X64_H.toAPIType_def
|
||||
X64_H.createObject_def placeNewDataObject_def)
|
||||
apply (intro conjI impI)
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
objBits_simps)[6]
|
||||
apply (simp add: bind_assoc placeNewObject_def2 objBits_simps
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
pageBits_def add.commute append)
|
||||
apply ((subst gsUserPages_update gsCNodes_update
|
||||
gsUserPages_upd_createObjects'_comm
|
||||
|
|
@ -5224,9 +5224,9 @@ proof -
|
|||
| simp add: modify_modify_bind o_def)+)[1]
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
ARM_H.getObjectSize_def objBits_simps)[6]
|
||||
X64_H.getObjectSize_def objBits_simps)[6]
|
||||
apply (simp add: bind_assoc placeNewObject_def2 objBits_simps
|
||||
ARM_H.getObjectSize_def
|
||||
X64_H.getObjectSize_def
|
||||
pageBits_def add.commute append)
|
||||
apply (subst gsUserPages_update gsCNodes_update
|
||||
gsUserPages_upd_createObjects'_comm
|
||||
|
|
@ -5237,15 +5237,15 @@ proof -
|
|||
-- "SectionObject"
|
||||
apply (simp add: Arch_createNewCaps_def
|
||||
Retype_H.createObject_def createObjects_def bind_assoc
|
||||
toAPIType_def ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def placeNewDataObject_def)
|
||||
toAPIType_def X64_H.toAPIType_def
|
||||
X64_H.createObject_def placeNewDataObject_def)
|
||||
apply (intro conjI impI)
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
objBits_simps)[6]
|
||||
apply (simp add: bind_assoc placeNewObject_def2 objBits_simps
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
pageBits_def add.commute append)
|
||||
apply ((subst gsUserPages_update gsCNodes_update
|
||||
gsUserPages_upd_createObjects'_comm
|
||||
|
|
@ -5255,9 +5255,9 @@ proof -
|
|||
| simp add: modify_modify_bind o_def)+)[1]
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
ARM_H.getObjectSize_def objBits_simps)[6]
|
||||
X64_H.getObjectSize_def objBits_simps)[6]
|
||||
apply (simp add: bind_assoc placeNewObject_def2 objBits_simps
|
||||
ARM_H.getObjectSize_def
|
||||
X64_H.getObjectSize_def
|
||||
pageBits_def add.commute append)
|
||||
apply (subst gsUserPages_update gsCNodes_update
|
||||
gsUserPages_upd_createObjects'_comm
|
||||
|
|
@ -5268,15 +5268,15 @@ proof -
|
|||
-- "SuperSectionObject"
|
||||
apply (simp add: Arch_createNewCaps_def
|
||||
Retype_H.createObject_def createObjects_def bind_assoc
|
||||
toAPIType_def ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def placeNewDataObject_def)
|
||||
toAPIType_def X64_H.toAPIType_def
|
||||
X64_H.createObject_def placeNewDataObject_def)
|
||||
apply (intro conjI impI)
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
objBits_simps)[6]
|
||||
apply (simp add: bind_assoc placeNewObject_def2 objBits_simps
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
pageBits_def add.commute append)
|
||||
apply ((subst gsUserPages_update gsCNodes_update
|
||||
gsUserPages_upd_createObjects'_comm
|
||||
|
|
@ -5286,9 +5286,9 @@ proof -
|
|||
| simp add: modify_modify_bind o_def)+)[1]
|
||||
apply (subst monad_eq, rule createObjects_Cons)
|
||||
apply (simp_all add: field_simps shiftl_t2n pageBits_def
|
||||
ARM_H.getObjectSize_def objBits_simps)[6]
|
||||
X64_H.getObjectSize_def objBits_simps)[6]
|
||||
apply (simp add: bind_assoc placeNewObject_def2 objBits_simps
|
||||
ARM_H.getObjectSize_def
|
||||
X64_H.getObjectSize_def
|
||||
pageBits_def add.commute append)
|
||||
apply (subst gsUserPages_update gsCNodes_update
|
||||
gsUserPages_upd_createObjects'_comm
|
||||
|
|
@ -5298,26 +5298,26 @@ proof -
|
|||
| simp add: modify_modify_bind o_def)+
|
||||
-- "PageTableObject"
|
||||
apply (simp add:Arch_createNewCaps_def Retype_H.createObject_def
|
||||
createObjects_def bind_assoc ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def)
|
||||
createObjects_def bind_assoc X64_H.toAPIType_def
|
||||
X64_H.createObject_def)
|
||||
apply (subst monad_eq,rule createObjects_Cons)
|
||||
apply ((simp add: field_simps shiftl_t2n pageBits_def archObjSize_def
|
||||
getObjectSize_def ARM_H.getObjectSize_def
|
||||
getObjectSize_def X64_H.getObjectSize_def
|
||||
objBits_simps ptBits_def)+)[6]
|
||||
apply (simp add:bind_assoc placeNewObject_def2)
|
||||
apply (simp add: pageBits_def field_simps
|
||||
getObjectSize_def ptBits_def archObjSize_def
|
||||
ARM_H.getObjectSize_def placeNewObject_def2
|
||||
X64_H.getObjectSize_def placeNewObject_def2
|
||||
objBits_simps append)
|
||||
|
||||
-- "PageDirectoryObject"
|
||||
apply (simp add:Arch_createNewCaps_def Retype_H.createObject_def
|
||||
createObjects_def bind_assoc ARM_H.toAPIType_def
|
||||
ARM_H.createObject_def)
|
||||
createObjects_def bind_assoc X64_H.toAPIType_def
|
||||
X64_H.createObject_def)
|
||||
apply (subgoal_tac "distinct (map (\<lambda>n. ptr + (n << 14)) [0.e.((of_nat n)::word32)])")
|
||||
prefer 2
|
||||
apply (clarsimp simp: objBits_simps archObjSize_def pdBits_def pageBits_def
|
||||
ARM_H.getObjectSize_def)
|
||||
X64_H.getObjectSize_def)
|
||||
apply (subst upto_enum_word)
|
||||
apply (clarsimp simp:distinct_map)
|
||||
apply (frule range_cover.range_cover_n_le)
|
||||
|
|
@ -5353,11 +5353,11 @@ proof -
|
|||
apply (simp_all add: word_bits_def)[3]
|
||||
apply (subst monad_eq,rule createObjects_Cons)
|
||||
apply ((simp add: field_simps shiftl_t2n pageBits_def archObjSize_def
|
||||
ARM_H.getObjectSize_def pdBits_def
|
||||
X64_H.getObjectSize_def pdBits_def
|
||||
objBits_simps ptBits_def)+)[6]
|
||||
apply (simp add:objBits_simps archObjSize_def pdBits_def pageBits_def ARM_H.getObjectSize_def)
|
||||
apply (simp add:objBits_simps archObjSize_def pdBits_def pageBits_def X64_H.getObjectSize_def)
|
||||
apply (simp add:bind_assoc)
|
||||
apply (simp add: placeNewObject_def2[where val = "makeObject::ARM_H.pde",simplified,symmetric])
|
||||
apply (simp add: placeNewObject_def2[where val = "makeObject::X64_H.pde",simplified,symmetric])
|
||||
apply (rule_tac Q = "\<lambda>r s. valid_arch_state' s \<and>
|
||||
(\<forall>x\<le>of_nat n. page_directory_at' (ptr + (x << 14)) s) \<and> Q s" for Q in monad_eq_split)
|
||||
apply (rule sym)
|
||||
|
|
@ -5441,7 +5441,7 @@ lemma createObject_def2:
|
|||
defer
|
||||
apply ((clarsimp simp: Arch_createNewCaps_def
|
||||
createObjects_def shiftL_nat
|
||||
ARM_H.createObject_def placeNewDataObject_def
|
||||
X64_H.createObject_def placeNewDataObject_def
|
||||
placeNewObject_def2 objBits_simps bind_assoc
|
||||
clearMemory_def clearMemoryVM_def fun_upd_def[symmetric]
|
||||
word_size mapM_x_singleton storeWordVM_def)+)[6]
|
||||
|
|
@ -5449,7 +5449,7 @@ lemma createObject_def2:
|
|||
apply (case_tac apiobject_type)
|
||||
apply (clarsimp simp: Arch_createNewCaps_def
|
||||
createObjects_def shiftL_nat
|
||||
ARM_H.createObject_def
|
||||
X64_H.createObject_def
|
||||
placeNewObject_def2 objBits_simps bind_assoc
|
||||
clearMemory_def clearMemoryVM_def
|
||||
word_size mapM_x_singleton storeWordVM_def)+
|
||||
|
|
@ -5646,12 +5646,12 @@ lemma ArchCreateObject_pspace_no_overlap':
|
|||
(ptr + (of_nat n << APIType_capBits ty userSize)) sz s \<and>
|
||||
pspace_aligned' s \<and> pspace_distinct' s \<and>
|
||||
range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0\<rbrace>
|
||||
ARM_H.createObject ty
|
||||
X64_H.createObject ty
|
||||
(ptr + (of_nat n << APIType_capBits ty userSize)) userSize d
|
||||
\<lbrace>\<lambda>archCap. pspace_no_overlap'
|
||||
(ptr + (1 + of_nat n << APIType_capBits ty userSize)) sz\<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
apply (clarsimp simp:ARM_H.createObject_def)
|
||||
apply (clarsimp simp:X64_H.createObject_def)
|
||||
apply wpc
|
||||
apply (wp doMachineOp_psp_no_overlap unless_doMachineOp_psp_no_overlap[simplified]
|
||||
createObjects'_pspace_no_overlap2 hoare_when_weak_wp
|
||||
|
|
@ -5774,14 +5774,14 @@ lemma createObject_pspace_aligned_distinct':
|
|||
apply (rule hoare_pre)
|
||||
apply (wp placeNewObject_pspace_aligned' hoare_unless_wp
|
||||
placeNewObject_pspace_distinct'
|
||||
| simp add:ARM_H.createObject_def
|
||||
| simp add:X64_H.createObject_def
|
||||
Retype_H.createObject_def objBits_simps
|
||||
curDomain_def placeNewDataObject_def
|
||||
split del: if_split
|
||||
| wpc | intro conjI impI)+
|
||||
apply (auto simp:APIType_capBits_def pdBits_def objBits_simps
|
||||
pageBits_def word_bits_def archObjSize_def ptBits_def ARM_H.toAPIType_def
|
||||
split:ARM_H.object_type.splits apiobject_type.splits)
|
||||
pageBits_def word_bits_def archObjSize_def ptBits_def X64_H.toAPIType_def
|
||||
split:X64_H.object_type.splits apiobject_type.splits)
|
||||
done
|
||||
|
||||
declare objSize_eq_capBits [simp]
|
||||
|
|
|
|||
|
|
@ -2194,7 +2194,7 @@ lemma finaliseCap_cases[wp]:
|
|||
isZombie (fst rv) \<and> final \<and> \<not> flag \<and> snd rv = None
|
||||
\<and> capUntypedPtr (fst rv) = capUntypedPtr cap
|
||||
\<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)\<rbrace>"
|
||||
apply (simp add: finaliseCap_def ARM_H.finaliseCap_def Let_def
|
||||
apply (simp add: finaliseCap_def X64_H.finaliseCap_def Let_def
|
||||
getThreadCSpaceRoot
|
||||
cong: if_cong split del: if_split)
|
||||
apply (rule hoare_pre)
|
||||
|
|
@ -2339,8 +2339,8 @@ lemma ct_not_inQ_ksArchState_update[simp]:
|
|||
by (simp add: ct_not_inQ_def)
|
||||
|
||||
lemma invs_asid_update_strg':
|
||||
"invs' s \<and> tab = armKSASIDTable (ksArchState s) \<longrightarrow>
|
||||
invs' (s\<lparr>ksArchState := armKSASIDTable_update
|
||||
"invs' s \<and> tab = x64KSASIDTable (ksArchState s) \<longrightarrow>
|
||||
invs' (s\<lparr>ksArchState := x64KSASIDTable_update
|
||||
(\<lambda>_. tab (asid := None)) (ksArchState s)\<rparr>)"
|
||||
apply (simp add: invs'_def)
|
||||
apply (simp add: valid_state'_def)
|
||||
|
|
@ -2424,7 +2424,7 @@ lemma arch_finaliseCap_invs[wp]:
|
|||
"\<lbrace>invs' and valid_cap' (ArchObjectCap cap)\<rbrace>
|
||||
Arch.finaliseCap cap fin
|
||||
\<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
apply (simp add: ARM_H.finaliseCap_def)
|
||||
apply (simp add: X64_H.finaliseCap_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | wpc)+
|
||||
apply clarsimp
|
||||
|
|
@ -2436,7 +2436,7 @@ lemma arch_finaliseCap_removeable[wp]:
|
|||
\<longrightarrow> isFinal (ArchObjectCap cap) slot (cteCaps_of s))\<rbrace>
|
||||
Arch.finaliseCap cap final
|
||||
\<lbrace>\<lambda>rv s. isNullCap rv \<and> removeable' slot s (ArchObjectCap cap)\<rbrace>"
|
||||
apply (simp add: ARM_H.finaliseCap_def
|
||||
apply (simp add: X64_H.finaliseCap_def
|
||||
removeable'_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | wpc)+
|
||||
|
|
@ -2549,7 +2549,7 @@ lemma finaliseCap_cte_refs:
|
|||
finaliseCap cap final flag
|
||||
\<lbrace>\<lambda>rv s. fst rv \<noteq> NullCap \<longrightarrow> cte_refs' (fst rv) = cte_refs' cap\<rbrace>"
|
||||
apply (simp add: finaliseCap_def Let_def getThreadCSpaceRoot
|
||||
ARM_H.finaliseCap_def
|
||||
X64_H.finaliseCap_def
|
||||
cong: if_cong split del: if_split)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | wpc | simp only: o_def)+
|
||||
|
|
@ -2937,7 +2937,7 @@ crunch cte_wp_at'[wp]: unmapPageTable, unmapPage, unbindNotification, finaliseCa
|
|||
|
||||
lemma arch_finaliseCap_cte_wp_at[wp]:
|
||||
"\<lbrace>cte_wp_at' P p\<rbrace> Arch.finaliseCap cap fin \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>"
|
||||
apply (simp add: ARM_H.finaliseCap_def)
|
||||
apply (simp add: X64_H.finaliseCap_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp unmapPage_cte_wp_at'| simp | wpc)+
|
||||
done
|
||||
|
|
@ -3438,7 +3438,7 @@ lemma finaliseCap_valid_cap[wp]:
|
|||
"\<lbrace>valid_cap' cap\<rbrace> finaliseCap cap final flag \<lbrace>\<lambda>rv. valid_cap' (fst rv)\<rbrace>"
|
||||
apply (simp add: finaliseCap_def Let_def
|
||||
getThreadCSpaceRoot
|
||||
ARM_H.finaliseCap_def
|
||||
X64_H.finaliseCap_def
|
||||
cong: if_cong split del: if_split)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | simp only: valid_NullCap o_def fst_conv | wpc)+
|
||||
|
|
@ -3528,7 +3528,7 @@ lemma arch_finalise_cap_corres:
|
|||
final' = isFinal (ArchObjectCap cap') (cte_map sl) (cteCaps_of s)))
|
||||
(arch_finalise_cap cap final) (Arch.finaliseCap cap' final')"
|
||||
apply (cases cap,
|
||||
simp_all add: arch_finalise_cap_def ARM_H.finaliseCap_def
|
||||
simp_all add: arch_finalise_cap_def X64_H.finaliseCap_def
|
||||
final_matters'_def case_bool_If liftM_def[symmetric]
|
||||
o_def dc_def[symmetric]
|
||||
split: option.split,
|
||||
|
|
@ -3953,7 +3953,7 @@ lemma set_thread_all_corres:
|
|||
apply (clarsimp simp: obj_at'_def)
|
||||
apply (clarsimp simp: projectKOs)
|
||||
apply (insert e is_t)
|
||||
by (clarsimp simp: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits ARM_A.arch_kernel_obj.splits)
|
||||
by (clarsimp simp: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits X64_A.arch_kernel_obj.splits)
|
||||
|
||||
lemma tcb_update_all_corres':
|
||||
assumes tcbs: "tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'"
|
||||
|
|
|
|||
|
|
@ -158,8 +158,8 @@ lemma decode_irq_control_corres:
|
|||
(decode_irq_control_invocation label args slot caps)
|
||||
(decodeIRQControlInvocation label args (cte_map slot) caps')"
|
||||
apply (clarsimp simp: decode_irq_control_invocation_def decodeIRQControlInvocation_def
|
||||
arch_check_irq_def ARM_H.checkIRQ_def
|
||||
ARM_H.decodeIRQControlInvocation_def arch_decode_irq_control_invocation_def
|
||||
arch_check_irq_def X64_H.checkIRQ_def
|
||||
X64_H.decodeIRQControlInvocation_def arch_decode_irq_control_invocation_def
|
||||
split del: if_split cong: if_cong
|
||||
split: invocation_label.split)
|
||||
|
||||
|
|
@ -221,7 +221,7 @@ lemma decode_irq_control_valid'[wp]:
|
|||
apply (rule hoare_pre)
|
||||
apply (wp ensureEmptySlot_stronger isIRQActive_wp
|
||||
whenE_throwError_wp
|
||||
| simp add: ARM_H.decodeIRQControlInvocation_def | wpc
|
||||
| simp add: X64_H.decodeIRQControlInvocation_def | wpc
|
||||
| wp_once hoare_drop_imps)+
|
||||
apply (clarsimp simp: minIRQ_def maxIRQ_def word_le_nat_alt unat_of_nat)
|
||||
done
|
||||
|
|
@ -373,7 +373,7 @@ lemma invoke_irq_control_corres:
|
|||
apply (case_tac ctea)
|
||||
apply (clarsimp simp: isCap_simps sameRegionAs_def3)
|
||||
apply (auto dest: valid_irq_handlers_ctes_ofD)[1]
|
||||
apply (clarsimp simp: arch_invoke_irq_control_def ARM_H.performIRQControl_def)
|
||||
apply (clarsimp simp: arch_invoke_irq_control_def X64_H.performIRQControl_def)
|
||||
done
|
||||
|
||||
crunch valid_cap'[wp]: setIRQState "valid_cap' cap"
|
||||
|
|
|
|||
|
|
@ -1423,8 +1423,8 @@ lemma (in delete_one) suspend_corres:
|
|||
|
||||
lemma (in delete_one) prepareThreadDelete_corres:
|
||||
"corres dc (tcb_at t) (tcb_at' t)
|
||||
(prepare_thread_delete t) (ArchRetypeDecls_H.ARM_H.prepareThreadDelete t)"
|
||||
by (simp add: ArchVSpace_A.ARM_A.prepare_thread_delete_def ArchRetype_H.ARM_H.prepareThreadDelete_def)
|
||||
(prepare_thread_delete t) (ArchRetypeDecls_H.X64_H.prepareThreadDelete t)"
|
||||
by (simp add: ArchVSpace_A.X64_A.prepare_thread_delete_def ArchRetype_H.X64_H.prepareThreadDelete_def)
|
||||
|
||||
lemma no_refs_simple_strg':
|
||||
"st_tcb_at' simple' t s' \<and> P {} \<longrightarrow> st_tcb_at' (\<lambda>st. P (tcb_st_refs_of' st)) t s'"
|
||||
|
|
|
|||
|
|
@ -22,8 +22,8 @@ lemma get_mi_corres: "corres (op = \<circ> message_info_map)
|
|||
(get_message_info t) (getMessageInfo t)"
|
||||
apply (rule corres_guard_imp)
|
||||
apply (unfold get_message_info_def getMessageInfo_def fun_app_def)
|
||||
apply (simp add: ARM_H.msgInfoRegister_def
|
||||
ARM.msgInfoRegister_def ARM_A.msg_info_register_def)
|
||||
apply (simp add: X64_H.msgInfoRegister_def
|
||||
ARM.msgInfoRegister_def X64_A.msg_info_register_def)
|
||||
apply (rule corres_split_eqr [OF _ user_getreg_corres])
|
||||
apply (rule corres_trivial, simp add: message_info_from_data_eqv)
|
||||
apply (wp | simp)+
|
||||
|
|
@ -291,7 +291,7 @@ lemma maskCapRights_vsCapRef[simp]:
|
|||
apply (cases cap, simp_all add: maskCapRights_def isCap_simps Let_def)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability;
|
||||
simp add: maskCapRights_def ARM_H.maskCapRights_def isCap_simps Let_def)
|
||||
simp add: maskCapRights_def X64_H.maskCapRights_def isCap_simps Let_def)
|
||||
done
|
||||
|
||||
lemma corres_set_extra_badge:
|
||||
|
|
@ -441,7 +441,7 @@ lemma maskCapRights_eq_null:
|
|||
apply (cases xa; simp add: maskCapRights_def isCap_simps)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability)
|
||||
apply (simp_all add: ARM_H.maskCapRights_def isCap_simps)
|
||||
apply (simp_all add: X64_H.maskCapRights_def isCap_simps)
|
||||
done
|
||||
|
||||
lemma capMasterCap_maskedAsFull[simp]:
|
||||
|
|
@ -904,7 +904,7 @@ lemma deriveCap_not_idle [wp]:
|
|||
apply (wp ensureNoChildren_wp | clarsimp simp: capRange_def)+
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability,
|
||||
simp_all add: ARM_H.deriveCap_def Let_def isCap_simps
|
||||
simp_all add: X64_H.deriveCap_def Let_def isCap_simps
|
||||
split: if_split,
|
||||
safe)
|
||||
apply (wp throwError_validE_R | clarsimp simp: capRange_def)+
|
||||
|
|
@ -914,7 +914,7 @@ lemma maskCapRights_capRange[simp]:
|
|||
"capRange (maskCapRights r c) = capRange c"
|
||||
apply (case_tac c)
|
||||
apply (simp_all add: maskCapRights_def isCap_defs capRange_def Let_def
|
||||
ARM_H.maskCapRights_def
|
||||
X64_H.maskCapRights_def
|
||||
split: arch_capability.split)
|
||||
done
|
||||
|
||||
|
|
@ -1220,7 +1220,7 @@ lemma capRights_Null_eq [simp]:
|
|||
"(maskCapRights R cap = NullCap) = (cap = NullCap)"
|
||||
apply (cases cap)
|
||||
apply (simp_all add: Let_def maskCapRights_def isCap_simps)
|
||||
apply (simp add: ARM_H.maskCapRights_def
|
||||
apply (simp add: X64_H.maskCapRights_def
|
||||
split: arch_capability.split)
|
||||
done
|
||||
|
||||
|
|
@ -1242,7 +1242,7 @@ lemma isIRQControlCap_mask [simp]:
|
|||
apply (clarsimp simp: isCap_simps maskCapRights_def Let_def)+
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability)
|
||||
apply (clarsimp simp: isCap_simps ARM_H.maskCapRights_def
|
||||
apply (clarsimp simp: isCap_simps X64_H.maskCapRights_def
|
||||
maskCapRights_def Let_def)+
|
||||
done
|
||||
|
||||
|
|
@ -1250,7 +1250,7 @@ lemma isPageCap_maskCapRights[simp]:
|
|||
" isArchCap isPageCap (RetypeDecls_H.maskCapRights R c) = isArchCap isPageCap c"
|
||||
apply (case_tac c; simp add: isCap_simps isArchCap_def maskCapRights_def)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability; simp add: isCap_simps ARM_H.maskCapRights_def)
|
||||
apply (case_tac arch_capability; simp add: isCap_simps X64_H.maskCapRights_def)
|
||||
done
|
||||
|
||||
lemma capReplyMaster_mask[simp]:
|
||||
|
|
@ -1272,7 +1272,7 @@ lemma updateCapData_ordering:
|
|||
"\<lbrakk> (x, capBadge cap) \<in> capBadge_ordering P; updateCapData p d cap \<noteq> NullCap \<rbrakk>
|
||||
\<Longrightarrow> (x, capBadge (updateCapData p d cap)) \<in> capBadge_ordering P"
|
||||
apply (cases cap, simp_all add: updateCapData_def isCap_simps Let_def
|
||||
capBadge_def ARM_H.updateCapData_def
|
||||
capBadge_def X64_H.updateCapData_def
|
||||
split: if_split_asm)
|
||||
apply fastforce+
|
||||
done
|
||||
|
|
@ -1285,7 +1285,7 @@ lemma updateCapData_is_Reply[simp]:
|
|||
"(updateCapData p d cap = ReplyCap x y) = (cap = ReplyCap x y)"
|
||||
by (rule ccontr,
|
||||
clarsimp simp: isCap_simps updateCapData_def Let_def
|
||||
ARM_H.updateCapData_def
|
||||
X64_H.updateCapData_def
|
||||
split del: if_split
|
||||
split: if_split_asm)
|
||||
|
||||
|
|
@ -1293,7 +1293,7 @@ lemma updateCapDataIRQ:
|
|||
"updateCapData p d cap \<noteq> NullCap \<Longrightarrow>
|
||||
isIRQControlCap (updateCapData p d cap) = isIRQControlCap cap"
|
||||
apply (cases cap, simp_all add: updateCapData_def isCap_simps Let_def
|
||||
ARM_H.updateCapData_def
|
||||
X64_H.updateCapData_def
|
||||
split: if_split_asm)
|
||||
done
|
||||
|
||||
|
|
@ -1301,7 +1301,7 @@ lemma updateCapData_vsCapRef[simp]:
|
|||
"vsCapRef (updateCapData pr D c) = vsCapRef c"
|
||||
by (rule ccontr,
|
||||
clarsimp simp: isCap_simps updateCapData_def Let_def
|
||||
ARM_H.updateCapData_def
|
||||
X64_H.updateCapData_def
|
||||
vsCapRef_def
|
||||
split del: if_split
|
||||
split: if_split_asm)
|
||||
|
|
@ -1310,7 +1310,7 @@ lemma isPageCap_updateCapData[simp]:
|
|||
"isArchCap isPageCap (updateCapData pr D c) = isArchCap isPageCap c"
|
||||
apply (case_tac c; simp add:updateCapData_def isCap_simps isArchCap_def)
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability; simp add: ARM_H.updateCapData_def isCap_simps isArchCap_def)
|
||||
apply (case_tac arch_capability; simp add: X64_H.updateCapData_def isCap_simps isArchCap_def)
|
||||
apply (clarsimp split:capability.splits simp:Let_def)
|
||||
done
|
||||
|
||||
|
|
@ -1743,12 +1743,12 @@ lemma mk_ft_msg_corres:
|
|||
apply (rule corres_split_eqr [OF _ getRestartPCs_corres])
|
||||
apply (rule corres_trivial, simp add: fromEnum_def enum_bool)
|
||||
apply (wp | simp)+
|
||||
apply (simp add: ARM_H.syscallMessage_def)
|
||||
apply (simp add: X64_H.syscallMessage_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_eqr [OF _ user_mapM_getRegister_corres])
|
||||
apply (rule corres_trivial, simp)
|
||||
apply (wp | simp)+
|
||||
apply (simp add: ARM_H.exceptionMessage_def)
|
||||
apply (simp add: X64_H.exceptionMessage_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_eqr [OF _ user_mapM_getRegister_corres])
|
||||
apply (rule corres_trivial, simp)
|
||||
|
|
@ -1779,7 +1779,7 @@ lemma do_fault_transfer_corres:
|
|||
(do_fault_transfer badge sender receiver recv_buf)
|
||||
(doFaultTransfer badge sender receiver recv_buf)"
|
||||
apply (clarsimp simp: do_fault_transfer_def doFaultTransfer_def split_def
|
||||
ARM_H.badgeRegister_def badge_register_def)
|
||||
X64_H.badgeRegister_def badge_register_def)
|
||||
apply (rule_tac Q="\<lambda>fault. K (\<exists>f. fault = Some f) and
|
||||
tcb_at sender and tcb_at receiver and
|
||||
case_option \<top> in_user_frame recv_buf"
|
||||
|
|
@ -1838,7 +1838,7 @@ lemma invs_mdb_absorb'_ac [simp]:
|
|||
|
||||
lemma lookupIPCBuffer_valid_ipc_buffer [wp]:
|
||||
"\<lbrace>valid_objs'\<rbrace> VSpace_H.lookupIPCBuffer b s \<lbrace>case_option \<top> valid_ipc_buffer_ptr'\<rbrace>"
|
||||
unfolding lookupIPCBuffer_def ARM_H.lookupIPCBuffer_def
|
||||
unfolding lookupIPCBuffer_def X64_H.lookupIPCBuffer_def
|
||||
apply (simp add: Let_def getSlotCap_def getThreadBufferSlot_def
|
||||
locateSlot_conv threadGet_def comp_def)
|
||||
apply (wp getCTE_wp getObject_tcb_wp | wpc)+
|
||||
|
|
@ -4375,7 +4375,7 @@ lemma zobj_refs_maskCapRights[simp]:
|
|||
by (cases cap;
|
||||
clarsimp
|
||||
simp add: maskCapRights_def isCap_simps
|
||||
Let_def ARM_H.maskCapRights_def
|
||||
Let_def X64_H.maskCapRights_def
|
||||
split: arch_capability.split)
|
||||
|
||||
lemma getCTE_cap_to_refs[wp]:
|
||||
|
|
@ -4394,7 +4394,7 @@ lemma lookupCap_cap_to_refs[wp]:
|
|||
|
||||
lemma arch_stt_objs' [wp]:
|
||||
"\<lbrace>valid_objs'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
|
||||
apply (simp add: ARM_H.switchToThread_def)
|
||||
apply (simp add: X64_H.switchToThread_def)
|
||||
apply wp
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -380,8 +380,8 @@ lemma irrelevant_ptr:
|
|||
apply (case_tac a,simp_all
|
||||
add:vs_ptr_align_def
|
||||
split:arch_kernel_object.splits
|
||||
ARM_H.pte.splits
|
||||
ARM_H.pde.splits)
|
||||
X64_H.pte.splits
|
||||
X64_H.pde.splits)
|
||||
apply (drule arg_cong[where f = "\<lambda>x. x && ~~ mask z"])
|
||||
apply (simp add:mask_lower_twice ptBits_def)
|
||||
apply (drule arg_cong[where f = "\<lambda>x. x && ~~ mask z"])
|
||||
|
|
@ -428,13 +428,13 @@ lemma mapM_x_storePTE_update_helper:
|
|||
apply (subgoal_tac "x && ~~ mask sz = y && ~~ mask sz")
|
||||
apply (drule(1) page_table_at_pte_atD')
|
||||
apply (drule mask_out_first_mask_some[where m = ptBits])
|
||||
apply (simp add:vs_ptr_align_def split:ARM_H.pte.splits)
|
||||
apply (simp add:vs_ptr_align_def split:X64_H.pte.splits)
|
||||
apply (simp add:mask_lower_twice vs_ptr_align_def
|
||||
split:ARM_H.pte.splits)
|
||||
split:X64_H.pte.splits)
|
||||
apply (clarsimp simp:typ_at'_def ko_wp_at'_def)
|
||||
apply (clarsimp simp:vs_ptr_align_def
|
||||
split:arch_kernel_obj.splits Structures_H.kernel_object.splits
|
||||
split:ARM_H.pte.splits)
|
||||
split:X64_H.pte.splits)
|
||||
apply (drule mask_out_first_mask_some[where m = sz])
|
||||
apply simp
|
||||
apply (simp add:mask_lower_twice)
|
||||
|
|
@ -453,24 +453,24 @@ lemma mapM_x_storePTE_update_helper:
|
|||
apply (drule mask_out_first_mask_some[where m = ptBits])
|
||||
apply (simp add:vs_ptr_align_def
|
||||
split:kernel_object.splits arch_kernel_object.splits
|
||||
ARM_H.pte.splits ARM_H.pde.splits)
|
||||
X64_H.pte.splits X64_H.pde.splits)
|
||||
apply (subst (asm) mask_lower_twice)
|
||||
apply (simp add:vs_ptr_align_def
|
||||
split:kernel_object.splits arch_kernel_object.splits
|
||||
ARM_H.pte.splits ARM_H.pde.splits)
|
||||
X64_H.pte.splits X64_H.pde.splits)
|
||||
apply simp
|
||||
apply (simp add:vs_ptr_align_def
|
||||
split:kernel_object.splits arch_kernel_object.splits
|
||||
ARM_H.pte.splits)
|
||||
X64_H.pte.splits)
|
||||
apply (simp add:mask_lower_twice)
|
||||
apply (drule mask_out_first_mask_some[where m = sz])
|
||||
apply (simp add:vs_ptr_align_def
|
||||
split:kernel_object.splits arch_kernel_object.splits
|
||||
ARM_H.pte.splits ARM_H.pde.splits)
|
||||
X64_H.pte.splits X64_H.pde.splits)
|
||||
apply (subst (asm) mask_lower_twice)
|
||||
apply (simp add:vs_ptr_align_def
|
||||
split:kernel_object.splits arch_kernel_object.splits
|
||||
ARM_H.pte.splits ARM_H.pde.splits)
|
||||
X64_H.pte.splits X64_H.pde.splits)
|
||||
apply simp
|
||||
apply (clarsimp split:option.splits)
|
||||
apply (drule_tac p' = y in valid_duplicates'_D)
|
||||
|
|
@ -543,13 +543,13 @@ lemma mapM_x_storePDE_update_helper:
|
|||
apply (subgoal_tac "y && ~~ mask sz = x && ~~ mask sz")
|
||||
apply (drule(1) page_directory_at_pde_atD')
|
||||
apply (drule mask_out_first_mask_some[where m = pdBits])
|
||||
apply (simp add:vs_ptr_align_def split:ARM_H.pde.splits)
|
||||
apply (simp add:vs_ptr_align_def split:X64_H.pde.splits)
|
||||
apply (simp add:mask_lower_twice vs_ptr_align_def
|
||||
split:ARM_H.pde.splits)
|
||||
split:X64_H.pde.splits)
|
||||
apply (clarsimp simp:typ_at'_def ko_wp_at'_def)
|
||||
apply (clarsimp simp:vs_ptr_align_def
|
||||
split:arch_kernel_obj.splits Structures_H.kernel_object.splits
|
||||
split:ARM_H.pde.splits)
|
||||
split:X64_H.pde.splits)
|
||||
apply (drule mask_out_first_mask_some[where m = sz])
|
||||
apply simp
|
||||
apply (simp add:mask_lower_twice)
|
||||
|
|
@ -568,24 +568,24 @@ lemma mapM_x_storePDE_update_helper:
|
|||
apply (drule mask_out_first_mask_some[where m = pdBits])
|
||||
apply (simp add:vs_ptr_align_def
|
||||
split:kernel_object.splits arch_kernel_object.splits
|
||||
ARM_H.pte.splits ARM_H.pde.splits)
|
||||
X64_H.pte.splits X64_H.pde.splits)
|
||||
apply (subst (asm) mask_lower_twice)
|
||||
apply (simp add:vs_ptr_align_def
|
||||
split:kernel_object.splits arch_kernel_object.splits
|
||||
ARM_H.pte.splits ARM_H.pde.splits)
|
||||
X64_H.pte.splits X64_H.pde.splits)
|
||||
apply simp
|
||||
apply (simp add:vs_ptr_align_def
|
||||
split:kernel_object.splits arch_kernel_object.splits
|
||||
ARM_H.pde.splits)
|
||||
X64_H.pde.splits)
|
||||
apply (simp add:mask_lower_twice)
|
||||
apply (drule mask_out_first_mask_some[where m = sz])
|
||||
apply (simp add:vs_ptr_align_def
|
||||
split:kernel_object.splits arch_kernel_object.splits
|
||||
ARM_H.pte.splits ARM_H.pde.splits)
|
||||
X64_H.pte.splits X64_H.pde.splits)
|
||||
apply (subst (asm) mask_lower_twice)
|
||||
apply (simp add:vs_ptr_align_def
|
||||
split:kernel_object.splits arch_kernel_object.splits
|
||||
ARM_H.pte.splits ARM_H.pde.splits)
|
||||
X64_H.pte.splits X64_H.pde.splits)
|
||||
apply simp
|
||||
apply (clarsimp split:option.splits)
|
||||
apply (drule_tac p' = y in valid_duplicates'_D)
|
||||
|
|
@ -597,7 +597,7 @@ lemma vs_ptr_align_upbound:
|
|||
by (simp add:vs_ptr_align_def
|
||||
split:Structures_H.kernel_object.splits
|
||||
arch_kernel_object.splits
|
||||
ARM_H.pde.splits ARM_H.pte.splits)
|
||||
X64_H.pde.splits X64_H.pte.splits)
|
||||
|
||||
lemma is_aligned_le_mask:
|
||||
"\<lbrakk>is_aligned a n; a\<le>b\<rbrakk> \<Longrightarrow> a \<le> b && ~~ mask n"
|
||||
|
|
@ -672,10 +672,10 @@ lemma copyGlobalMappings_ksPSpace_stable:
|
|||
assumes ptr_al: "is_aligned ptr pdBits"
|
||||
shows
|
||||
"\<lbrace>\<lambda>s. ksPSpace s x = ko \<and> pspace_distinct' s \<and> pspace_aligned' s \<and>
|
||||
is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrace>
|
||||
is_aligned (x64KSGlobalPD (ksArchState s)) pdBits\<rbrace>
|
||||
copyGlobalMappings ptr
|
||||
\<lbrace>\<lambda>_ s. ksPSpace s x = (if x \<in> {ptr + (kernelBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}
|
||||
then ksPSpace s ((armKSGlobalPD (ksArchState s)) + (x && mask pdBits))
|
||||
then ksPSpace s ((x64KSGlobalPD (ksArchState s)) + (x && mask pdBits))
|
||||
else ko)\<rbrace>"
|
||||
proof -
|
||||
have not_aligned_eq_None:
|
||||
|
|
@ -739,14 +739,14 @@ lemma copyGlobalMappings_ksPSpace_stable:
|
|||
apply (case_tac "\<not> is_aligned x 2")
|
||||
apply (rule hoare_name_pre_state)
|
||||
apply (clarsimp)
|
||||
apply (rule_tac Q = "\<lambda>r s. is_aligned (armKSGlobalPD (ksArchState s)) 2
|
||||
apply (rule_tac Q = "\<lambda>r s. is_aligned (x64KSGlobalPD (ksArchState s)) 2
|
||||
\<and> pspace_aligned' s" in hoare_post_imp)
|
||||
apply (frule_tac x = x in not_aligned_eq_None)
|
||||
apply simp
|
||||
apply (frule_tac x = x and s = sa in not_aligned_eq_None)
|
||||
apply simp
|
||||
apply clarsimp
|
||||
apply (drule_tac x = "armKSGlobalPD (ksArchState sa) + (x && mask pdBits)"
|
||||
apply (drule_tac x = "x64KSGlobalPD (ksArchState sa) + (x && mask pdBits)"
|
||||
and s = sa in not_aligned_eq_None[rotated])
|
||||
apply (subst is_aligned_mask)
|
||||
apply (simp add: mask_add_aligned mask_twice)
|
||||
|
|
@ -763,8 +763,8 @@ lemma copyGlobalMappings_ksPSpace_stable:
|
|||
apply wp
|
||||
apply (rule_tac V="\<lambda>xs s. \<forall>x \<in> (set [kernelBase >> 20.e.2 ^ (pdBits - 2) - 1] - set xs).
|
||||
ksPSpace s (ptr + (x << 2)) = ksPSpace s (globalPD + (x << 2))"
|
||||
and I="\<lambda>s'. globalPD = (armKSGlobalPD (ksArchState s'))
|
||||
\<and> globalPD = (armKSGlobalPD (ksArchState s))"
|
||||
and I="\<lambda>s'. globalPD = (x64KSGlobalPD (ksArchState s'))
|
||||
\<and> globalPD = (x64KSGlobalPD (ksArchState s))"
|
||||
in mapM_x_inv_wp2)
|
||||
apply (cut_tac ptr_al)
|
||||
apply (clarsimp simp:blah pdBits_def pageBits_def)
|
||||
|
|
@ -829,7 +829,7 @@ lemma copyGlobalMappings_ksPSpace_stable:
|
|||
apply (rule hoare_pre)
|
||||
apply (rule hoare_vcg_const_imp_lift)
|
||||
apply wp
|
||||
apply (rule_tac Q = "\<lambda>r s'. ksPSpace s' x = ksPSpace s x \<and> globalPD = armKSGlobalPD (ksArchState s)"
|
||||
apply (rule_tac Q = "\<lambda>r s'. ksPSpace s' x = ksPSpace s x \<and> globalPD = x64KSGlobalPD (ksArchState s)"
|
||||
in hoare_post_imp)
|
||||
apply (wp hoare_vcg_all_lift getPDE_wp mapM_x_wp'
|
||||
| simp add: storePDE_def setObject_def split_def
|
||||
|
|
@ -848,7 +848,7 @@ lemma copyGlobalMappings_ksPSpace_same:
|
|||
shows
|
||||
"\<lbrakk>is_aligned ptr pdBits\<rbrakk> \<Longrightarrow>
|
||||
\<lbrace>\<lambda>s. ksPSpace s x = ko \<and> pspace_distinct' s \<and> pspace_aligned' s \<and>
|
||||
is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ptr = armKSGlobalPD (ksArchState s)\<rbrace>
|
||||
is_aligned (x64KSGlobalPD (ksArchState s)) pdBits \<and> ptr = x64KSGlobalPD (ksArchState s)\<rbrace>
|
||||
copyGlobalMappings ptr
|
||||
\<lbrace>\<lambda>_ s. ksPSpace s x = ko\<rbrace>"
|
||||
apply (simp add:copyGlobalMappings_def)
|
||||
|
|
@ -856,7 +856,7 @@ lemma copyGlobalMappings_ksPSpace_same:
|
|||
apply clarsimp
|
||||
apply (rule hoare_pre)
|
||||
apply wp
|
||||
apply (rule_tac Q = "\<lambda>r s'. ksPSpace s' x = ksPSpace s x \<and> globalPD = armKSGlobalPD (ksArchState s)"
|
||||
apply (rule_tac Q = "\<lambda>r s'. ksPSpace s' x = ksPSpace s x \<and> globalPD = x64KSGlobalPD (ksArchState s)"
|
||||
in hoare_post_imp)
|
||||
apply simp
|
||||
apply (wp hoare_vcg_all_lift getPDE_wp mapM_x_wp'
|
||||
|
|
@ -881,14 +881,14 @@ lemma copyGlobalMappings_ksPSpace_concrete:
|
|||
atLeastAtMost_iff
|
||||
assumes monad: "(r, s') \<in> fst (copyGlobalMappings ptr s)"
|
||||
and ps: "pspace_distinct' s" "pspace_aligned' s"
|
||||
and al: "is_aligned (armKSGlobalPD (ksArchState s)) pdBits"
|
||||
and al: "is_aligned (x64KSGlobalPD (ksArchState s)) pdBits"
|
||||
"is_aligned ptr pdBits"
|
||||
shows "ksPSpace s' = (\<lambda>x.
|
||||
(if x \<in> {ptr + (kernelBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}
|
||||
then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x))"
|
||||
then ksPSpace s ((x && mask pdBits) + x64KSGlobalPD (ksArchState s)) else ksPSpace s x))"
|
||||
proof -
|
||||
have pd: "\<And>pd. \<lbrace>\<lambda>s. armKSGlobalPD (ksArchState s) = pd \<rbrace>
|
||||
copyGlobalMappings ptr \<lbrace>\<lambda>r s. armKSGlobalPD (ksArchState s) = pd \<rbrace>"
|
||||
have pd: "\<And>pd. \<lbrace>\<lambda>s. x64KSGlobalPD (ksArchState s) = pd \<rbrace>
|
||||
copyGlobalMappings ptr \<lbrace>\<lambda>r s. x64KSGlobalPD (ksArchState s) = pd \<rbrace>"
|
||||
by wp
|
||||
have comp: "\<And>x. x \<in> {ptr + (kernelBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}
|
||||
\<Longrightarrow> ptr + (x && mask pdBits) = x"
|
||||
|
|
@ -917,7 +917,7 @@ lemma copyGlobalMappings_ksPSpace_concrete:
|
|||
apply (frule_tac x = x in copyGlobalMappings_ksPSpaceD)
|
||||
apply simp+
|
||||
apply (clarsimp split:if_splits)
|
||||
apply (frule_tac x = "(armKSGlobalPD (ksArchState s') + (x && mask pdBits))"
|
||||
apply (frule_tac x = "(x64KSGlobalPD (ksArchState s') + (x && mask pdBits))"
|
||||
in copyGlobalMappings_ksPSpaceD)
|
||||
apply simp+
|
||||
apply (drule use_valid[OF _ pd])
|
||||
|
|
@ -926,8 +926,8 @@ lemma copyGlobalMappings_ksPSpace_concrete:
|
|||
apply (clarsimp simp: mask_add_aligned)
|
||||
apply (frule comp)
|
||||
apply (clarsimp simp:pdBits_def pageBits_def mask_twice blah)
|
||||
apply (drule_tac y = "armKSGlobalPD a + b" for a b in neg_mask_mono_le[where n = 14])
|
||||
apply (drule_tac x = "armKSGlobalPD a + b" for a b in neg_mask_mono_le[where n = 14])
|
||||
apply (drule_tac y = "x64KSGlobalPD a + b" for a b in neg_mask_mono_le[where n = 14])
|
||||
apply (drule_tac x = "x64KSGlobalPD a + b" for a b in neg_mask_mono_le[where n = 14])
|
||||
apply (frule_tac d1 = "x && mask 14" in is_aligned_add_helper[THEN conjunct2])
|
||||
apply (simp add:mask_def)
|
||||
apply (rule le_less_trans[OF word_and_le1])
|
||||
|
|
@ -956,7 +956,7 @@ lemma copyGlobalMappings_valid_duplicates':
|
|||
atLeastAtMost_iff
|
||||
shows "\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_distinct'
|
||||
and pspace_aligned'
|
||||
and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
|
||||
and (\<lambda>s. is_aligned (x64KSGlobalPD (ksArchState s)) pdBits)
|
||||
and K (is_aligned ptr pdBits)\<rbrace>
|
||||
copyGlobalMappings ptr \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
|
||||
proof -
|
||||
|
|
@ -987,15 +987,15 @@ lemma copyGlobalMappings_valid_duplicates':
|
|||
apply simp
|
||||
apply simp
|
||||
apply (clarsimp split:if_splits)
|
||||
apply (drule_tac p' = "((y && mask pdBits) + armKSGlobalPD (ksArchState s))"
|
||||
apply (drule_tac p' = "((y && mask pdBits) + x64KSGlobalPD (ksArchState s))"
|
||||
in valid_duplicates'_D[rotated])
|
||||
apply (erule aligned_add_aligned[OF is_aligned_andI1])
|
||||
apply (erule is_aligned_weaken[where y = 2])
|
||||
apply (simp add:pdBits_def)
|
||||
apply simp
|
||||
apply (frule_tac x = "x && mask pdBits" and a = x2 and ptr = "armKSGlobalPD (ksArchState s)"
|
||||
apply (frule_tac x = "x && mask pdBits" and a = x2 and ptr = "x64KSGlobalPD (ksArchState s)"
|
||||
in neg_mask_simp)
|
||||
apply (drule_tac x = "y && mask pdBits" and a = x2 and ptr = "armKSGlobalPD (ksArchState s)"
|
||||
apply (drule_tac x = "y && mask pdBits" and a = x2 and ptr = "x64KSGlobalPD (ksArchState s)"
|
||||
in neg_mask_simp)
|
||||
apply (simp add:mask_sub_mask)
|
||||
apply simp
|
||||
|
|
@ -1055,7 +1055,7 @@ shows
|
|||
using pdpt_align
|
||||
apply (clarsimp simp: image_def vs_entry_align_def vs_ptr_align_def
|
||||
new_cap_addrs_def objBits_simps archObjSize_def
|
||||
split:ARM_H.pde.splits ARM_H.pte.splits arch_kernel_object.splits
|
||||
split:X64_H.pde.splits X64_H.pte.splits arch_kernel_object.splits
|
||||
Structures_H.kernel_object.splits)
|
||||
done
|
||||
|
||||
|
|
@ -1084,13 +1084,13 @@ lemma valid_duplicates'_insert_ko:
|
|||
apply clarsimp
|
||||
apply (case_tac ko, simp_all add:vs_ptr_align_def)
|
||||
apply (rename_tac arch_kernel_object)
|
||||
apply (case_tac arch_kernel_object, simp_all split: ARM_H.pte.splits)
|
||||
apply (case_tac arch_kernel_object, simp_all split: X64_H.pte.splits)
|
||||
apply (drule(1) bspec)+
|
||||
apply (drule_tac p' = y in new_cap_addrs_same_align_pdpt_bits)
|
||||
apply (simp add:vs_entry_align_def)
|
||||
apply (simp add:vs_ptr_align_def)
|
||||
apply (simp add:objBits_simps archObjSize_def)+
|
||||
apply (clarsimp split: ARM_H.pde.splits simp:objBits_simps)
|
||||
apply (clarsimp split: X64_H.pde.splits simp:objBits_simps)
|
||||
apply (drule(1) bspec)+
|
||||
apply (drule_tac p' = y in new_cap_addrs_same_align_pdpt_bits)
|
||||
apply (simp add:vs_entry_align_def)
|
||||
|
|
@ -1105,7 +1105,7 @@ lemma valid_duplicates'_insert_ko:
|
|||
apply (drule(2) valid_duplicates'_D)
|
||||
apply (clarsimp simp:vs_ptr_align_def
|
||||
split: Structures_H.kernel_object.splits
|
||||
ARM_H.pde.splits ARM_H.pte.splits
|
||||
X64_H.pde.splits X64_H.pte.splits
|
||||
arch_kernel_object.splits)
|
||||
apply simp
|
||||
done
|
||||
|
|
@ -1132,7 +1132,7 @@ lemma valid_duplicates'_update:
|
|||
simp_all add: vs_ptr_align_def vs_entry_align_def)
|
||||
apply (rename_tac arch_kernel_object)
|
||||
apply (case_tac arch_kernel_object,
|
||||
simp_all split: ARM_H.pde.splits ARM_H.pte.splits)
|
||||
simp_all split: X64_H.pde.splits X64_H.pte.splits)
|
||||
apply (clarsimp split:option.splits)
|
||||
apply (drule(2) pspace_no_overlap_base')
|
||||
apply (drule(2) valid_duplicates'_D)
|
||||
|
|
@ -1145,7 +1145,7 @@ lemma valid_duplicates'_update:
|
|||
lemma createObject_valid_duplicates'[wp]:
|
||||
"\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct'
|
||||
and pspace_no_overlap' ptr (getObjectSize ty us)
|
||||
and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
|
||||
and (\<lambda>s. is_aligned (x64KSGlobalPD (ksArchState s)) pdBits)
|
||||
and K (is_aligned ptr (getObjectSize ty us))
|
||||
and K (ty = APIObjectType apiobject_type.CapTableObject \<longrightarrow> us < 28)\<rbrace>
|
||||
RetypeDecls_H.createObject ty ptr us d
|
||||
|
|
@ -1153,7 +1153,7 @@ lemma createObject_valid_duplicates'[wp]:
|
|||
apply (rule hoare_gen_asm)
|
||||
apply (simp add:createObject_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wpc | wp| simp add: ARM_H.createObject_def split del: if_split)+
|
||||
apply (wpc | wp| simp add: X64_H.createObject_def split del: if_split)+
|
||||
apply (simp add: placeNewObject_def placeNewDataObject_def
|
||||
placeNewObject'_def split_def split del: if_split
|
||||
| wp hoare_unless_wp[where P="d"] hoare_unless_wp[where Q=\<top>]
|
||||
|
|
@ -1200,7 +1200,7 @@ lemma createObject_valid_duplicates'[wp]:
|
|||
,(simp add: objBits_simps pageBits_def word_bits_conv)+)[1]
|
||||
apply (clarsimp simp: new_cap_addrs_fold'[where n = "0x1000",simplified])
|
||||
apply (erule valid_duplicates'_insert_ko[where us = 12,simplified])
|
||||
apply (simp add: ARM_H.toAPIType_def vs_entry_align_def
|
||||
apply (simp add: X64_H.toAPIType_def vs_entry_align_def
|
||||
APIType_capBits_def objBits_simps pageBits_def)+
|
||||
apply (rule none_in_new_cap_addrs[where us =12,simplified]
|
||||
,(simp add: objBits_simps pageBits_def word_bits_conv)+)[1]
|
||||
|
|
@ -1212,7 +1212,7 @@ lemma createObject_valid_duplicates'[wp]:
|
|||
apply (erule valid_duplicates'_insert_ko[where us = 8,simplified])
|
||||
apply (simp add: toAPIType_def archObjSize_def vs_entry_align_def
|
||||
APIType_capBits_def objBits_simps pageBits_def
|
||||
split: ARM_H.pte.splits)+
|
||||
split: X64_H.pte.splits)+
|
||||
apply (rule none_in_new_cap_addrs[where us =8,simplified]
|
||||
,(simp add: objBits_simps pageBits_def word_bits_conv archObjSize_def)+)[1]
|
||||
apply clarsimp
|
||||
|
|
@ -1237,9 +1237,9 @@ lemma createObject_valid_duplicates'[wp]:
|
|||
data_map_insert_def[abs_def])
|
||||
apply (clarsimp simp: archObjSize_def pdBits_def pageBits_def)
|
||||
apply (rule valid_duplicates'_insert_ko[where us = 12,simplified])
|
||||
apply (simp add: ARM_H.toAPIType_def archObjSize_def vs_entry_align_def
|
||||
apply (simp add: X64_H.toAPIType_def archObjSize_def vs_entry_align_def
|
||||
APIType_capBits_def objBits_simps pageBits_def
|
||||
split: ARM_H.pde.splits)+
|
||||
split: X64_H.pde.splits)+
|
||||
apply (rule none_in_new_cap_addrs[where us =12,simplified]
|
||||
,(simp add: objBits_simps pageBits_def word_bits_conv archObjSize_def)+)[1]
|
||||
apply (intro conjI impI allI)
|
||||
|
|
@ -1255,8 +1255,8 @@ lemma createObject_valid_duplicates'[wp]:
|
|||
apply clarsimp
|
||||
apply (drule(2) valid_duplicates'_update) prefer 3
|
||||
apply (fastforce simp: vs_entry_align_def)+
|
||||
apply (clarsimp simp:ARM_H.toAPIType_def word_bits_def
|
||||
split:ARM_H.object_type.splits)
|
||||
apply (clarsimp simp:X64_H.toAPIType_def word_bits_def
|
||||
split:X64_H.object_type.splits)
|
||||
apply (cut_tac ptr = ptr in new_cap_addrs_fold'[where n = "2^us"
|
||||
and ko = "(KOCTE makeObject)",simplified])
|
||||
apply (rule word_1_le_power)
|
||||
|
|
@ -1264,26 +1264,26 @@ lemma createObject_valid_duplicates'[wp]:
|
|||
apply (drule_tac ptr = ptr and ko = "KOCTE makeObject" in
|
||||
valid_duplicates'_insert_ko[where us = us,simplified])
|
||||
apply (simp add: APIType_capBits_def is_aligned_mask
|
||||
ARM_H.toAPIType_def ARM_H.toAPIType_def
|
||||
split: ARM_H.object_type.splits)
|
||||
X64_H.toAPIType_def X64_H.toAPIType_def
|
||||
split: X64_H.object_type.splits)
|
||||
apply (simp add: vs_entry_align_def)
|
||||
apply (simp add: objBits_simps)
|
||||
apply (rule none_in_new_cap_addrs
|
||||
,(simp add: objBits_simps pageBits_def APIType_capBits_def
|
||||
ARM_H.toAPIType_def ARM_H.toAPIType_def
|
||||
X64_H.toAPIType_def X64_H.toAPIType_def
|
||||
word_bits_conv archObjSize_def is_aligned_mask
|
||||
split: ARM_H.object_type.splits)+)[1]
|
||||
split: X64_H.object_type.splits)+)[1]
|
||||
apply (clarsimp simp: word_bits_def)
|
||||
done
|
||||
|
||||
|
||||
crunch arch_inv[wp]: createNewObjects "\<lambda>s. P (armKSGlobalPD (ksArchState s))"
|
||||
crunch arch_inv[wp]: createNewObjects "\<lambda>s. P (x64KSGlobalPD (ksArchState s))"
|
||||
(simp: crunch_simps zipWithM_x_mapM wp: crunch_wps hoare_unless_wp)
|
||||
|
||||
|
||||
lemma createNewObjects_valid_duplicates'[wp]:
|
||||
"\<lbrace> (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_no_overlap' ptr sz
|
||||
and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
|
||||
and pspace_aligned' and pspace_distinct' and (\<lambda>s. is_aligned (x64KSGlobalPD (ksArchState s)) pdBits)
|
||||
and K (range_cover ptr sz (Types_H.getObjectSize ty us) (length dest) \<and>
|
||||
ptr \<noteq> 0 \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28) ) \<rbrace>
|
||||
createNewObjects ty src dest ptr us d
|
||||
|
|
@ -1374,7 +1374,7 @@ lemma valid_duplicates_deleteObjects_helper:
|
|||
apply (rename_tac arch_kernel_object)
|
||||
apply (case_tac arch_kernel_object)
|
||||
apply fastforce+
|
||||
apply (clarsimp split:ARM_H.pte.splits)
|
||||
apply (clarsimp split:X64_H.pte.splits)
|
||||
apply auto[1]
|
||||
apply (drule_tac p' = y in valid_duplicates'_D[OF vd])
|
||||
apply (simp add:vs_ptr_align_def)+
|
||||
|
|
@ -1391,7 +1391,7 @@ lemma valid_duplicates_deleteObjects_helper:
|
|||
apply simp
|
||||
apply (simp add:vs_ptr_align_def)
|
||||
apply simp
|
||||
apply (clarsimp split:ARM_H.pde.splits)
|
||||
apply (clarsimp split:X64_H.pde.splits)
|
||||
apply auto[1]
|
||||
apply (drule_tac p' = y in valid_duplicates'_D[OF vd])
|
||||
apply simp
|
||||
|
|
@ -1453,9 +1453,9 @@ lemma resetUntypedCap_valid_duplicates'[wp]:
|
|||
apply (clarsimp simp add: isCap_simps valid_cap_simps' capAligned_def)
|
||||
done
|
||||
|
||||
lemma is_aligned_armKSGlobalPD:
|
||||
lemma is_aligned_x64KSGlobalPD:
|
||||
"valid_arch_state' s
|
||||
\<Longrightarrow> is_aligned (armKSGlobalPD (ksArchState s)) pdBits"
|
||||
\<Longrightarrow> is_aligned (x64KSGlobalPD (ksArchState s)) pdBits"
|
||||
by (clarsimp simp: valid_arch_state'_def page_directory_at'_def)
|
||||
|
||||
lemma new_CapTable_bound:
|
||||
|
|
@ -1495,7 +1495,7 @@ lemma invokeUntyped_valid_duplicates[wp]:
|
|||
apply (clarsimp simp: cte_wp_at_ctes_of)
|
||||
apply (frule new_CapTable_bound)
|
||||
apply (frule invokeUntyped_proofs.not_0_ptr)
|
||||
apply (strengthen is_aligned_armKSGlobalPD)
|
||||
apply (strengthen is_aligned_x64KSGlobalPD)
|
||||
apply (frule cte_wp_at_valid_objs_valid_cap'[OF ctes_of_cte_wpD], clarsimp+)
|
||||
apply (clarsimp simp add: isCap_simps valid_cap_simps' capAligned_def)
|
||||
apply (auto split: if_split_asm)
|
||||
|
|
@ -1564,7 +1564,7 @@ lemma storePDE_no_duplicates':
|
|||
apply (intro conjI impI)
|
||||
apply (clarsimp simp:vs_ptr_align_def vs_entry_align_def
|
||||
split:option.splits
|
||||
ARM_H.pde.splits)
|
||||
X64_H.pde.splits)
|
||||
apply clarsimp
|
||||
apply (intro conjI impI)
|
||||
apply (clarsimp split:option.splits)
|
||||
|
|
@ -1575,8 +1575,8 @@ lemma storePDE_no_duplicates':
|
|||
apply (clarsimp simp:ko_wp_at'_def vs_entry_align_def
|
||||
vs_ptr_align_def
|
||||
split:if_splits option.splits arch_kernel_object.splits
|
||||
Structures_H.kernel_object.splits ARM_H.pde.splits
|
||||
ARM_H.pte.splits)
|
||||
Structures_H.kernel_object.splits X64_H.pde.splits
|
||||
X64_H.pte.splits)
|
||||
apply (clarsimp split:option.splits)
|
||||
apply (drule_tac p = x and p' = y in valid_duplicates'_D)
|
||||
apply simp+
|
||||
|
|
@ -1597,7 +1597,7 @@ lemma storePTE_no_duplicates':
|
|||
apply (intro conjI impI)
|
||||
apply (clarsimp simp:vs_entry_align_def vs_ptr_align_def
|
||||
split:option.splits
|
||||
ARM_H.pte.splits)
|
||||
X64_H.pte.splits)
|
||||
apply clarsimp
|
||||
apply (intro conjI impI)
|
||||
apply (clarsimp split:option.splits)
|
||||
|
|
@ -1608,8 +1608,8 @@ lemma storePTE_no_duplicates':
|
|||
apply (clarsimp simp:ko_wp_at'_def
|
||||
vs_ptr_align_def vs_entry_align_def
|
||||
split:if_splits option.splits arch_kernel_object.splits
|
||||
Structures_H.kernel_object.splits ARM_H.pde.splits
|
||||
ARM_H.pte.splits)
|
||||
Structures_H.kernel_object.splits X64_H.pde.splits
|
||||
X64_H.pte.splits)
|
||||
apply (clarsimp split:option.splits)
|
||||
apply (drule_tac p = x and p' = y in valid_duplicates'_D)
|
||||
apply simp+
|
||||
|
|
@ -1803,7 +1803,7 @@ lemma unmapPageTable_valid_duplicates'[wp]:
|
|||
obj_at'_real_def projectKO_opt_pde)
|
||||
apply (clarsimp simp:vs_entry_align_def
|
||||
split:arch_kernel_object.splits
|
||||
ARM_H.pde.split Structures_H.kernel_object.splits)
|
||||
X64_H.pde.split Structures_H.kernel_object.splits)
|
||||
apply simp
|
||||
done
|
||||
|
||||
|
|
@ -1821,7 +1821,7 @@ lemma archFinaliseCap_valid_duplicates'[wp]:
|
|||
and (valid_cap' (capability.ArchObjectCap arch_cap))\<rbrace>
|
||||
Arch.finaliseCap arch_cap is_final
|
||||
\<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>"
|
||||
apply (case_tac arch_cap,simp_all add:ARM_H.finaliseCap_def)
|
||||
apply (case_tac arch_cap,simp_all add:X64_H.finaliseCap_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp|wpc|simp)+
|
||||
apply (rule hoare_pre)
|
||||
|
|
@ -1912,8 +1912,8 @@ lemma mapM_x_storePTE_invalid_whole:
|
|||
"\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and>
|
||||
s \<turnstile>' capability.ArchObjectCap (arch_capability.PageTableCap word option) \<and>
|
||||
pspace_aligned' s\<rbrace>
|
||||
mapM_x (swp storePTE ARM_H.pte.InvalidPTE)
|
||||
[word , word + 2 ^ objBits ARM_H.pte.InvalidPTE .e. word + 2 ^ ptBits - 1]
|
||||
mapM_x (swp storePTE X64_H.pte.InvalidPTE)
|
||||
[word , word + 2 ^ objBits X64_H.pte.InvalidPTE .e. word + 2 ^ ptBits - 1]
|
||||
\<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
|
||||
apply (wp mapM_x_storePTE_update_helper
|
||||
[where word = word and sz = ptBits and ptr = word])
|
||||
|
|
@ -1927,9 +1927,9 @@ lemma mapM_x_storePDE_update_invalid:
|
|||
"\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and>
|
||||
(\<exists>option. s \<turnstile>' capability.ArchObjectCap (arch_capability.PageDirectoryCap word option)) \<and>
|
||||
pspace_aligned' s\<rbrace>
|
||||
mapM_x (swp storePDE ARM_H.pde.InvalidPDE)
|
||||
mapM_x (swp storePDE X64_H.pde.InvalidPDE)
|
||||
(map ((\<lambda>x. x + word) \<circ>
|
||||
swp op << (objBits ARM_H.pde.InvalidPDE))
|
||||
swp op << (objBits X64_H.pde.InvalidPDE))
|
||||
[0.e.(kernelBase >> 20) - 1])
|
||||
\<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
|
||||
proof -
|
||||
|
|
@ -2016,7 +2016,7 @@ lemma invokeIRQControl_valid_duplicates'[wp]:
|
|||
\<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
|
||||
apply (simp add:performIRQControl_def )
|
||||
apply (rule hoare_pre)
|
||||
apply (wp|wpc | simp add:ARM_H.performIRQControl_def)+
|
||||
apply (wp|wpc | simp add:X64_H.performIRQControl_def)+
|
||||
apply fastforce
|
||||
done
|
||||
|
||||
|
|
@ -2025,7 +2025,7 @@ lemma invokeIRQHandler_valid_duplicates'[wp]:
|
|||
\<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
|
||||
apply (simp add:invokeIRQHandler_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp|wpc | simp add:ARM_H.performIRQControl_def)+
|
||||
apply (wp|wpc | simp add:X64_H.performIRQControl_def)+
|
||||
done
|
||||
|
||||
lemma invokeCNode_valid_duplicates'[wp]:
|
||||
|
|
@ -2224,7 +2224,7 @@ lemma placeASIDPool_valid_duplicates'[wp]:
|
|||
apply (simp add:pageBits_def)
|
||||
apply blast
|
||||
apply (simp add: pageBits_def
|
||||
split : ARM_H.pte.splits ARM_H.pde.splits
|
||||
split : X64_H.pte.splits X64_H.pde.splits
|
||||
arch_kernel_object.splits Structures_H.kernel_object.splits )
|
||||
apply (drule mask_out_first_mask_some[where m = 12])
|
||||
apply simp
|
||||
|
|
@ -2268,7 +2268,7 @@ lemma performArchInvocation_valid_duplicates':
|
|||
and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
|
||||
Arch.performInvocation ai
|
||||
\<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
|
||||
apply (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def)
|
||||
apply (simp add: X64_H.performInvocation_def performARMMMUInvocation_def)
|
||||
apply (cases ai, simp_all)
|
||||
apply (rename_tac page_table_invocation)
|
||||
apply (case_tac page_table_invocation)
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ begin
|
|||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
||||
definition
|
||||
APIType_map2 :: "kernel_object + ARM_H.object_type \<Rightarrow> Structures_A.apiobject_type"
|
||||
APIType_map2 :: "kernel_object + X64_H.object_type \<Rightarrow> Structures_A.apiobject_type"
|
||||
where
|
||||
"APIType_map2 ty \<equiv> case ty of
|
||||
Inr (APIObjectType ArchTypes_H.Untyped) \<Rightarrow> Structures_A.Untyped
|
||||
|
|
@ -70,7 +70,7 @@ lemma objBitsKO_bounded2[simp]:
|
|||
declare select_singleton_is_return[simp]
|
||||
|
||||
definition
|
||||
APIType_capBits :: "ARM_H.object_type \<Rightarrow> nat \<Rightarrow> nat"
|
||||
APIType_capBits :: "X64_H.object_type \<Rightarrow> nat \<Rightarrow> nat"
|
||||
where
|
||||
"APIType_capBits ty us \<equiv> case ty of
|
||||
APIObjectType ArchTypes_H.Untyped \<Rightarrow> us
|
||||
|
|
@ -86,7 +86,7 @@ where
|
|||
| PageDirectoryObject \<Rightarrow> 14"
|
||||
|
||||
definition
|
||||
makeObjectKO :: "bool \<Rightarrow> (kernel_object + ARM_H.object_type) \<rightharpoonup> kernel_object"
|
||||
makeObjectKO :: "bool \<Rightarrow> (kernel_object + X64_H.object_type) \<rightharpoonup> kernel_object"
|
||||
where
|
||||
"makeObjectKO dev ty \<equiv> case ty of
|
||||
Inl KOUserData \<Rightarrow> Some KOUserData
|
||||
|
|
@ -537,7 +537,7 @@ lemma makeObjectKO_eq:
|
|||
using x
|
||||
by (simp add: makeObjectKO_def eq_commute
|
||||
split: apiobject_type.split_asm sum.split_asm kernel_object.split_asm
|
||||
ARM_H.object_type.split_asm arch_kernel_object.split_asm)+
|
||||
X64_H.object_type.split_asm arch_kernel_object.split_asm)+
|
||||
|
||||
lemma pspace_no_overlap_base':
|
||||
"\<lbrakk>pspace_aligned' s;pspace_no_overlap' x n s; is_aligned x n \<rbrakk> \<Longrightarrow> ksPSpace s x = None"
|
||||
|
|
@ -1160,7 +1160,7 @@ lemma retype_ekheap_relation:
|
|||
split: if_split_asm)
|
||||
subgoal by (clarsimp simp add: makeObjectKO_def APIType_map2_def cong: if_cong
|
||||
split: sum.splits Structures_H.kernel_object.splits
|
||||
arch_kernel_object.splits ARM_H.object_type.splits apiobject_type.splits)
|
||||
arch_kernel_object.splits X64_H.object_type.splits apiobject_type.splits)
|
||||
|
||||
apply (frule ekh_at_tcb_at[OF et])
|
||||
apply (intro impI conjI)
|
||||
|
|
@ -1169,7 +1169,7 @@ lemma retype_ekheap_relation:
|
|||
apply (clarsimp simp add: other_obj_relation_def split: if_split_asm)
|
||||
apply (case_tac ko,simp_all)
|
||||
apply (clarsimp simp add: makeObjectKO_def cong: if_cong split: sum.splits Structures_H.kernel_object.splits
|
||||
arch_kernel_object.splits ARM_H.object_type.splits
|
||||
arch_kernel_object.splits X64_H.object_type.splits
|
||||
apiobject_type.splits if_split_asm)
|
||||
apply (drule_tac x=xa in bspec,simp)
|
||||
subgoal by force
|
||||
|
|
@ -2397,8 +2397,8 @@ proof -
|
|||
using cover
|
||||
apply (simp add: range_cover_def)
|
||||
using cover
|
||||
apply (clarsimp simp: ARM_H.toAPIType_def APIType_capBits_def
|
||||
split: ARM_H.object_type.splits)
|
||||
apply (clarsimp simp: X64_H.toAPIType_def APIType_capBits_def
|
||||
split: X64_H.object_type.splits)
|
||||
|
||||
-- "SmallPageObject"
|
||||
apply wp
|
||||
|
|
@ -2474,9 +2474,9 @@ proof -
|
|||
proof(cases a)
|
||||
case Untyped with Some cover ct show ?thesis
|
||||
apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def)
|
||||
apply (simp_all add: ARM_H.toAPIType_def fromIntegral_def
|
||||
apply (simp_all add: X64_H.toAPIType_def fromIntegral_def
|
||||
toInteger_nat fromInteger_nat APIType_capBits_def
|
||||
split: ARM_H.object_type.splits)
|
||||
split: X64_H.object_type.splits)
|
||||
apply wp
|
||||
apply (intro ballI)
|
||||
apply (clarsimp simp: image_def upto_enum_red' valid_cap'_def capAligned_def
|
||||
|
|
@ -2503,16 +2503,16 @@ proof -
|
|||
case TCBObject with Some cover ct show ?thesis
|
||||
including no_pre
|
||||
apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def)
|
||||
apply (simp_all add: ARM_H.toAPIType_def
|
||||
apply (simp_all add: X64_H.toAPIType_def
|
||||
fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def curDomain_def
|
||||
split: ARM_H.object_type.splits)
|
||||
split: X64_H.object_type.splits)
|
||||
apply (wp mapM_x_wp' hoare_vcg_const_Ball_lift)+
|
||||
apply (rule hoare_post_imp)
|
||||
prefer 2
|
||||
apply (rule createObjects_obj_at [where 'a = "tcb",OF _ not_0])
|
||||
using cover
|
||||
apply (clarsimp simp: ARM_H.toAPIType_def APIType_capBits_def objBits_simps
|
||||
split: ARM_H.object_type.splits)
|
||||
apply (clarsimp simp: X64_H.toAPIType_def APIType_capBits_def objBits_simps
|
||||
split: X64_H.object_type.splits)
|
||||
apply (simp add: projectKOs)
|
||||
apply (clarsimp simp: valid_cap'_def objBits_simps)
|
||||
apply (fastforce intro: capAligned_tcbI)
|
||||
|
|
@ -2521,16 +2521,16 @@ proof -
|
|||
case EndpointObject with Some cover ct show ?thesis
|
||||
including no_pre
|
||||
apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def)
|
||||
apply (simp_all add: ARM_H.toAPIType_def
|
||||
apply (simp_all add: X64_H.toAPIType_def
|
||||
fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def
|
||||
split: ARM_H.object_type.splits)
|
||||
split: X64_H.object_type.splits)
|
||||
apply wp
|
||||
apply (rule hoare_post_imp)
|
||||
prefer 2
|
||||
apply (rule createObjects_obj_at [where 'a=endpoint, OF _ not_0])
|
||||
using cover
|
||||
apply (clarsimp simp: ARM_H.toAPIType_def APIType_capBits_def objBits_simps
|
||||
split: ARM_H.object_type.splits)
|
||||
apply (clarsimp simp: X64_H.toAPIType_def APIType_capBits_def objBits_simps
|
||||
split: X64_H.object_type.splits)
|
||||
apply (simp add: projectKOs)
|
||||
apply (clarsimp simp: valid_cap'_def objBits_simps)
|
||||
apply (fastforce intro: capAligned_epI)
|
||||
|
|
@ -2539,16 +2539,16 @@ proof -
|
|||
case NotificationObject with Some cover ct show ?thesis
|
||||
including no_pre
|
||||
apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def)
|
||||
apply (simp_all add: ARM_H.toAPIType_def
|
||||
apply (simp_all add: X64_H.toAPIType_def
|
||||
fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def
|
||||
split: ARM_H.object_type.splits)
|
||||
split: X64_H.object_type.splits)
|
||||
apply wp
|
||||
apply (rule hoare_post_imp)
|
||||
prefer 2
|
||||
apply (rule createObjects_obj_at [where 'a="notification", OF _ not_0])
|
||||
using cover
|
||||
apply (clarsimp simp: ARM_H.toAPIType_def APIType_capBits_def objBits_simps
|
||||
split: ARM_H.object_type.splits)
|
||||
apply (clarsimp simp: X64_H.toAPIType_def APIType_capBits_def objBits_simps
|
||||
split: X64_H.object_type.splits)
|
||||
apply (simp add: projectKOs)
|
||||
apply (clarsimp simp: valid_cap'_def objBits_simps)
|
||||
apply (fastforce intro: capAligned_ntfnI)
|
||||
|
|
@ -2556,12 +2556,12 @@ proof -
|
|||
next
|
||||
case CapTableObject with Some cover ct show ?thesis
|
||||
apply (clarsimp simp: Arch_createNewCaps_def createNewCaps_def)
|
||||
apply (simp_all add: ARM_H.toAPIType_def
|
||||
apply (simp_all add: X64_H.toAPIType_def
|
||||
fromIntegral_def toInteger_nat fromInteger_nat APIType_capBits_def
|
||||
split: ARM_H.object_type.splits)
|
||||
split: X64_H.object_type.splits)
|
||||
apply wp
|
||||
apply (clarsimp simp: ARM_H.toAPIType_def APIType_capBits_def objBits_simps
|
||||
split: ARM_H.object_type.split object_type.splits)
|
||||
apply (clarsimp simp: X64_H.toAPIType_def APIType_capBits_def objBits_simps
|
||||
split: X64_H.object_type.split object_type.splits)
|
||||
apply (rule hoare_strengthen_post)
|
||||
apply (rule hoare_vcg_conj_lift)
|
||||
apply (rule createObjects_aligned [OF _ _ not_0 ])
|
||||
|
|
@ -2679,7 +2679,7 @@ lemma pagedirectory_relation_retype:
|
|||
apply (fastforce simp:pde_relation_aligned_def)
|
||||
done
|
||||
|
||||
lemmas makeObjectKO_simps = makeObjectKO_def[split_simps ARM_H.object_type.split
|
||||
lemmas makeObjectKO_simps = makeObjectKO_def[split_simps X64_H.object_type.split
|
||||
apiobject_type.split sum.split kernel_object.split ]
|
||||
|
||||
lemma corres_retype:
|
||||
|
|
@ -2712,7 +2712,7 @@ lemma init_arch_objects_APIType_map2:
|
|||
"init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs =
|
||||
(case ty of APIObjectType _ \<Rightarrow> return ()
|
||||
| _ \<Rightarrow> init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs)"
|
||||
apply (clarsimp split: ARM_H.object_type.split)
|
||||
apply (clarsimp split: X64_H.object_type.split)
|
||||
apply (simp add: init_arch_objects_def APIType_map2_def
|
||||
split: apiobject_type.split)
|
||||
done
|
||||
|
|
@ -2722,7 +2722,7 @@ lemma pde_relation_aligned_eq:
|
|||
\<Longrightarrow> pde_relation_aligned (pd + x >> 2) xa ya =
|
||||
pde_relation_aligned (pd' + x >> 2) xa ya"
|
||||
apply (clarsimp simp: pde_relation_aligned_def is_aligned_mask mask_def
|
||||
split: ARM_H.pde.splits)
|
||||
split: X64_H.pde.splits)
|
||||
apply word_bitwise
|
||||
apply auto
|
||||
done
|
||||
|
|
@ -2801,7 +2801,7 @@ lemmas copyGlobalMappings_ctes_of[wp]
|
|||
|
||||
lemmas object_splits =
|
||||
apiobject_type.split_asm
|
||||
ARM_H.object_type.split_asm
|
||||
X64_H.object_type.split_asm
|
||||
sum.split_asm kernel_object.split_asm
|
||||
arch_kernel_object.split_asm
|
||||
|
||||
|
|
@ -3418,7 +3418,7 @@ proof (intro conjI impI)
|
|||
apply (insert sym[OF mko])[1]
|
||||
apply (clarsimp simp: makeObjectKO_def
|
||||
split: bool.split_asm sum.split_asm
|
||||
ARM_H.object_type.split_asm
|
||||
X64_H.object_type.split_asm
|
||||
apiobject_type.split_asm
|
||||
kernel_object.split_asm
|
||||
arch_kernel_object.split_asm)
|
||||
|
|
@ -3749,7 +3749,7 @@ lemma createNewCaps_cte_wp_at2:
|
|||
createNewCaps ty ptr n objsz dev
|
||||
\<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>"
|
||||
including no_pre
|
||||
apply (simp add: createNewCaps_def createObjects_def ARM_H.toAPIType_def
|
||||
apply (simp add: createNewCaps_def createObjects_def X64_H.toAPIType_def
|
||||
split del: if_split)
|
||||
apply (case_tac ty; simp add: createNewCaps_def createObjects_def Arch_createNewCaps_def
|
||||
split del: if_split cong: if_cong)
|
||||
|
|
@ -3834,7 +3834,7 @@ lemma createNewCaps_cte_wp_at':
|
|||
\<and> pspace_no_overlap' ptr sz s\<rbrace>
|
||||
createNewCaps ty ptr n us dev
|
||||
\<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>"
|
||||
apply (simp add: createNewCaps_def ARM_H.toAPIType_def
|
||||
apply (simp add: createNewCaps_def X64_H.toAPIType_def
|
||||
split del: if_split)
|
||||
apply (case_tac ty; simp add: Arch_createNewCaps_def
|
||||
split del: if_split)
|
||||
|
|
@ -3952,7 +3952,7 @@ lemma createNewCaps_valid_cap_other:
|
|||
createNewCaps ty ptr n us dev
|
||||
\<lbrace>\<lambda>_. valid_cap' c\<rbrace>"
|
||||
unfolding createNewCaps_def
|
||||
apply (clarsimp simp: ARM_H.toAPIType_def
|
||||
apply (clarsimp simp: X64_H.toAPIType_def
|
||||
split del: if_split)
|
||||
apply (cases ty, simp_all add: createNewCaps_def Arch_createNewCaps_def
|
||||
split del: if_split)
|
||||
|
|
@ -4051,7 +4051,7 @@ lemma createNewCaps_state_refs_of':
|
|||
createNewCaps ty ptr n us dev
|
||||
\<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>"
|
||||
unfolding createNewCaps_def
|
||||
apply (clarsimp simp: ARM_H.toAPIType_def
|
||||
apply (clarsimp simp: X64_H.toAPIType_def
|
||||
split del: if_split)
|
||||
apply (cases ty; simp add: createNewCaps_def Arch_createNewCaps_def
|
||||
split del: if_split)
|
||||
|
|
@ -4119,7 +4119,7 @@ lemma createNewCaps_iflive'[wp]:
|
|||
\<lbrace>\<lambda>rv s. if_live_then_nonz_cap' s\<rbrace>"
|
||||
unfolding createNewCaps_def
|
||||
apply (insert cover)
|
||||
apply (clarsimp simp: toAPIType_def ARM_H.toAPIType_def)
|
||||
apply (clarsimp simp: toAPIType_def X64_H.toAPIType_def)
|
||||
apply (cases ty, simp_all add: createNewCaps_def Arch_createNewCaps_def
|
||||
split del: if_split)
|
||||
apply (rename_tac apiobject_type)
|
||||
|
|
@ -4314,7 +4314,7 @@ lemma createNewCaps_ko_wp_atQ':
|
|||
\<lbrace>\<lambda>rv s. P (ko_wp_at' P' p s)\<rbrace>"
|
||||
including no_pre
|
||||
apply (rule hoare_name_pre_state)
|
||||
apply (clarsimp simp: createNewCaps_def ARM_H.toAPIType_def
|
||||
apply (clarsimp simp: createNewCaps_def X64_H.toAPIType_def
|
||||
split del: if_split)
|
||||
apply (cases ty, simp_all add: Arch_createNewCaps_def
|
||||
split del: if_split)
|
||||
|
|
@ -4461,7 +4461,7 @@ lemma createNewCaps_idle'[wp]:
|
|||
createNewCaps ty ptr n us d
|
||||
\<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
apply (rule hoare_gen_asm)
|
||||
apply (clarsimp simp: createNewCaps_def ARM_H.toAPIType_def
|
||||
apply (clarsimp simp: createNewCaps_def X64_H.toAPIType_def
|
||||
split del: if_split)
|
||||
apply (cases ty, simp_all add: Arch_createNewCaps_def
|
||||
split del: if_split)
|
||||
|
|
@ -4625,7 +4625,7 @@ lemma getObject_valid_pde_mapping':
|
|||
done
|
||||
|
||||
lemma copyGlobalMappings_pde_mappings':
|
||||
"\<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
|
||||
"\<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (x64KSGlobalPD (ksArchState s)) pdBits)
|
||||
and K (is_aligned pd pdBits)\<rbrace> copyGlobalMappings pd \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>"
|
||||
apply (simp add: copyGlobalMappings_def objBits_simps archObjSize_def)
|
||||
apply wp
|
||||
|
|
@ -4646,7 +4646,7 @@ lemma copyGlobalMappings_pde_mappings':
|
|||
done
|
||||
|
||||
lemma mapM_x_copyGlobalMappings_pde_mappings':
|
||||
"\<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
|
||||
"\<lbrace>valid_pde_mappings' and (\<lambda>s. is_aligned (x64KSGlobalPD (ksArchState s)) pdBits)
|
||||
and K (\<forall>x \<in> set xs. is_aligned x pdBits)\<rbrace>
|
||||
mapM_x copyGlobalMappings xs \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>"
|
||||
apply (rule hoare_gen_asm)
|
||||
|
|
@ -4680,7 +4680,7 @@ lemma createNewCaps_pde_mappings'[wp]:
|
|||
apply (case_tac ty; simp)
|
||||
apply (rename_tac apiobject_type)
|
||||
apply (case_tac apiobject_type)
|
||||
apply (auto simp: ARM_H.toAPIType_def objBits_simps ptBits_def pageBits_def
|
||||
apply (auto simp: X64_H.toAPIType_def objBits_simps ptBits_def pageBits_def
|
||||
makeObject_pde valid_arch_state'_def pdBits_def page_directory_at'_def)
|
||||
done
|
||||
|
||||
|
|
@ -4744,7 +4744,7 @@ lemma createNewCaps_valid_pspace:
|
|||
createNewCaps ty ptr n us dev \<lbrace>\<lambda>r. valid_pspace'\<rbrace>"
|
||||
unfolding createNewCaps_def Arch_createNewCaps_def
|
||||
using valid_obj_makeObject_rules
|
||||
apply (clarsimp simp: ARM_H.toAPIType_def
|
||||
apply (clarsimp simp: X64_H.toAPIType_def
|
||||
split del: if_split cong: option.case_cong)
|
||||
apply (cases ty, simp_all split del: if_split)
|
||||
apply (rename_tac apiobject_type)
|
||||
|
|
@ -4808,7 +4808,7 @@ lemma createNewCaps_vms:
|
|||
| assumption)+
|
||||
apply (case_tac ty)
|
||||
apply (auto simp: APIType_capBits_def archObjSize_def objBits_simps pageBits_def ptBits_def
|
||||
pdBits_def ARM_H.toAPIType_def object_type.splits)
|
||||
pdBits_def X64_H.toAPIType_def object_type.splits)
|
||||
done
|
||||
|
||||
lemma createObjects_pspace_domain_valid':
|
||||
|
|
@ -4862,7 +4862,7 @@ lemma createNewCaps_pspace_domain_valid[wp]:
|
|||
mapM_x_wp'
|
||||
| wpc | simp add: Arch_createNewCaps_def curDomain_def Let_def
|
||||
split del: if_split)+
|
||||
apply (simp add: ARM_H.toAPIType_def
|
||||
apply (simp add: X64_H.toAPIType_def
|
||||
split: object_type.splits)
|
||||
apply (auto simp: objBits_simps APIType_capBits_def pageBits_def
|
||||
archObjSize_def ptBits_def pdBits_def)
|
||||
|
|
@ -5155,7 +5155,7 @@ proof (rule hoare_assume_pre, elim conjE)
|
|||
"range_cover ptr sz (APIType_capBits ty us) n"
|
||||
show ?thesis
|
||||
unfolding createNewCaps_def using valid_obj_makeObject_rules
|
||||
apply (clarsimp simp: ARM_H.toAPIType_def
|
||||
apply (clarsimp simp: X64_H.toAPIType_def
|
||||
split del: if_split)
|
||||
apply (cases ty, simp_all add: Arch_createNewCaps_def
|
||||
split del: if_split)
|
||||
|
|
|
|||
|
|
@ -204,7 +204,7 @@ lemma st_tcb_at_coerce_abstract:
|
|||
apply (clarsimp simp: st_tcb_at_def obj_at_def other_obj_relation_def
|
||||
tcb_relation_def
|
||||
split: Structures_A.kernel_object.split_asm if_split_asm
|
||||
ARM_A.arch_kernel_obj.split_asm)+
|
||||
X64_A.arch_kernel_obj.split_asm)+
|
||||
apply fastforce
|
||||
done
|
||||
|
||||
|
|
@ -224,7 +224,7 @@ lemma arch_switch_thread_corres:
|
|||
and st_tcb_at runnable t)
|
||||
(valid_arch_state' and valid_pspace' and st_tcb_at' runnable' t)
|
||||
(arch_switch_to_thread t) (Arch.switchToThread t)"
|
||||
apply (simp add: arch_switch_to_thread_def ARM_H.switchToThread_def)
|
||||
apply (simp add: arch_switch_to_thread_def X64_H.switchToThread_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split' [OF set_vm_root_corres])
|
||||
apply (rule corres_machine_op[OF corres_rel_imp])
|
||||
|
|
@ -914,7 +914,7 @@ lemma cur_thread_update_corres:
|
|||
done
|
||||
|
||||
lemma arch_switch_thread_tcb_at' [wp]: "\<lbrace>tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. tcb_at' t\<rbrace>"
|
||||
by (unfold ARM_H.switchToThread_def, wp typ_at_lift_tcb')
|
||||
by (unfold X64_H.switchToThread_def, wp typ_at_lift_tcb')
|
||||
|
||||
crunch typ_at'[wp]: "switchToThread" "\<lambda>s. P (typ_at' T p s)"
|
||||
(ignore: clearExMonitor)
|
||||
|
|
@ -924,14 +924,14 @@ lemma Arch_switchToThread_pred_tcb'[wp]:
|
|||
Arch.switchToThread t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace>"
|
||||
proof -
|
||||
have pos: "\<And>P t t'. \<lbrace>pred_tcb_at' proj P t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. pred_tcb_at' proj P t'\<rbrace>"
|
||||
apply (simp add: pred_tcb_at'_def ARM_H.switchToThread_def)
|
||||
apply (simp add: pred_tcb_at'_def X64_H.switchToThread_def)
|
||||
apply (rule hoare_seq_ext)+
|
||||
apply (rule doMachineOp_obj_at)
|
||||
apply (rule setVMRoot_obj_at)
|
||||
done
|
||||
show ?thesis
|
||||
apply (rule P_bool_lift [OF pos])
|
||||
by (rule lift_neg_pred_tcb_at' [OF ArchThreadDecls_H_ARM_H_switchToThread_typ_at' pos])
|
||||
by (rule lift_neg_pred_tcb_at' [OF ArchThreadDecls_H_X64_H_switchToThread_typ_at' pos])
|
||||
qed
|
||||
|
||||
|
||||
|
|
@ -946,7 +946,7 @@ crunch ksQ[wp]: asUser "\<lambda>s. P (ksReadyQueues s p)"
|
|||
|
||||
lemma arch_switch_thread_ksQ[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace>"
|
||||
apply (simp add: ARM_H.switchToThread_def)
|
||||
apply (simp add: X64_H.switchToThread_def)
|
||||
apply (wp)
|
||||
done
|
||||
|
||||
|
|
@ -1011,7 +1011,7 @@ lemma typ_at'_typ_at'_mask: "\<And>s. \<lbrakk> typ_at' t (P s) s \<rbrakk> \<Lo
|
|||
lemma arch_switch_idle_thread_corres:
|
||||
"corres dc \<top> (valid_arch_state' and pspace_aligned') arch_switch_to_idle_thread Arch.switchToIdleThread"
|
||||
apply (simp add: arch_switch_to_idle_thread_def
|
||||
ARM_H.switchToIdleThread_def)
|
||||
X64_H.switchToIdleThread_def)
|
||||
done
|
||||
|
||||
lemma switch_idle_thread_corres:
|
||||
|
|
@ -1250,13 +1250,13 @@ lemma clearExMonitor_invs'[wp]:
|
|||
|
||||
lemma Arch_switchToThread_invs[wp]:
|
||||
"\<lbrace>invs' and tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
apply (simp add: ARM_H.switchToThread_def)
|
||||
apply (simp add: X64_H.switchToThread_def)
|
||||
apply (wp; auto)
|
||||
done
|
||||
|
||||
lemma Arch_switchToThread_tcb'[wp]:
|
||||
"\<lbrace>tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>"
|
||||
apply (simp add: ARM_H.switchToThread_def)
|
||||
apply (simp add: X64_H.switchToThread_def)
|
||||
apply (wp doMachineOp_obj_at hoare_drop_imps)+
|
||||
done
|
||||
|
||||
|
|
@ -1265,13 +1265,13 @@ crunch ksCurDomain[wp]: "Arch.switchToThread" "\<lambda>s. P (ksCurDomain s)"
|
|||
|
||||
lemma Arch_swichToThread_tcbDomain_triv[wp]:
|
||||
"\<lbrace> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace> Arch.switchToThread t \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>"
|
||||
apply (clarsimp simp: ARM_H.switchToThread_def storeWordUser_def)
|
||||
apply (clarsimp simp: X64_H.switchToThread_def storeWordUser_def)
|
||||
apply (wp hoare_drop_imp | simp)+
|
||||
done
|
||||
|
||||
lemma Arch_swichToThread_tcbPriority_triv[wp]:
|
||||
"\<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace> Arch.switchToThread t \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>"
|
||||
apply (clarsimp simp: ARM_H.switchToThread_def storeWordUser_def)
|
||||
apply (clarsimp simp: X64_H.switchToThread_def storeWordUser_def)
|
||||
apply (wp hoare_drop_imp | simp)+
|
||||
done
|
||||
|
||||
|
|
@ -1303,7 +1303,7 @@ lemma Arch_switchToThread_obj_at[wp]:
|
|||
"\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace>
|
||||
Arch.switchToThread t
|
||||
\<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t\<rbrace>"
|
||||
apply (simp add: ARM_H.switchToThread_def )
|
||||
apply (simp add: X64_H.switchToThread_def )
|
||||
apply (rule hoare_seq_ext)+
|
||||
apply (rule doMachineOp_obj_at)
|
||||
apply (rule setVMRoot_obj_at)
|
||||
|
|
@ -1411,7 +1411,7 @@ lemma asUser_invs_no_cicd'[wp]:
|
|||
|
||||
lemma Arch_switchToThread_invs_no_cicd':
|
||||
"\<lbrace>invs_no_cicd'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
|
||||
apply (simp add: ARM_H.switchToThread_def)
|
||||
apply (simp add: X64_H.switchToThread_def)
|
||||
by (wp|rule setVMRoot_invs_no_cicd')+
|
||||
|
||||
|
||||
|
|
@ -1758,7 +1758,7 @@ lemma setThreadState_rct:
|
|||
|
||||
lemma switchToIdleThread_invs'[wp]:
|
||||
"\<lbrace>invs'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
apply (clarsimp simp: Thread_H.switchToIdleThread_def ARM_H.switchToIdleThread_def)
|
||||
apply (clarsimp simp: Thread_H.switchToIdleThread_def X64_H.switchToIdleThread_def)
|
||||
apply (wp_trace setCurThread_invs_idle_thread)
|
||||
apply clarsimp
|
||||
|
||||
|
|
@ -1975,7 +1975,7 @@ qed
|
|||
|
||||
lemma switchToIdleThread_invs_no_cicd':
|
||||
"\<lbrace>invs_no_cicd'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
apply (clarsimp simp: Thread_H.switchToIdleThread_def ARM_H.switchToIdleThread_def)
|
||||
apply (clarsimp simp: Thread_H.switchToIdleThread_def X64_H.switchToIdleThread_def)
|
||||
apply (wp setCurThread_invs_no_cicd'_idle_thread storeWordUser_invs_no_cicd')
|
||||
apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_idle'_def)
|
||||
done
|
||||
|
|
@ -1986,7 +1986,7 @@ crunch obj_at'[wp]: "Arch.switchToIdleThread" "\<lambda>s. obj_at' P t s"
|
|||
lemma switchToIdleThread_activatable[wp]:
|
||||
"\<lbrace>invs'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>"
|
||||
apply (simp add: Thread_H.switchToIdleThread_def
|
||||
ARM_H.switchToIdleThread_def)
|
||||
X64_H.switchToIdleThread_def)
|
||||
apply (wp setCurThread_ct_in_state)
|
||||
apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def
|
||||
pred_tcb_at'_def obj_at'_def)
|
||||
|
|
@ -2743,7 +2743,7 @@ lemma switchToThread_ct_not_queued_2:
|
|||
(is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>")
|
||||
apply (simp add: Thread_H.switchToThread_def)
|
||||
apply (wp)
|
||||
apply (simp add: ARM_H.switchToThread_def setCurThread_def)
|
||||
apply (simp add: X64_H.switchToThread_def setCurThread_def)
|
||||
apply (wp tcbSchedDequeue_not_tcbQueued | simp )+
|
||||
done
|
||||
|
||||
|
|
@ -2781,7 +2781,7 @@ lemma switchToIdleThread_ct_not_queued_no_cicd':
|
|||
lemma switchToIdleThread_activatable_2[wp]:
|
||||
"\<lbrace>invs_no_cicd'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>"
|
||||
apply (simp add: Thread_H.switchToIdleThread_def
|
||||
ARM_H.switchToIdleThread_def)
|
||||
X64_H.switchToIdleThread_def)
|
||||
apply (wp setCurThread_ct_in_state)
|
||||
apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_idle'_def
|
||||
pred_tcb_at'_def obj_at'_def)
|
||||
|
|
@ -2793,7 +2793,7 @@ lemma switchToThread_tcb_in_cur_domain':
|
|||
apply (simp add: Thread_H.switchToThread_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp)
|
||||
apply (simp add: ARM_H.switchToThread_def setCurThread_def)
|
||||
apply (simp add: X64_H.switchToThread_def setCurThread_def)
|
||||
apply (wp tcbSchedDequeue_not_tcbQueued | simp )+
|
||||
apply (simp add:tcb_in_cur_domain'_def)
|
||||
apply (wp tcbSchedDequeue_tcbDomain | wps)+
|
||||
|
|
@ -2957,7 +2957,7 @@ lemma stt_nosch:
|
|||
"\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
|
||||
switchToThread t
|
||||
\<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
|
||||
apply (simp add: Thread_H.switchToThread_def ARM_H.switchToThread_def storeWordUser_def)
|
||||
apply (simp add: Thread_H.switchToThread_def X64_H.switchToThread_def storeWordUser_def)
|
||||
apply (wp setCurThread_nosch hoare_drop_imp |simp)+
|
||||
done
|
||||
|
||||
|
|
@ -2966,7 +2966,7 @@ lemma stit_nosch[wp]:
|
|||
switchToIdleThread
|
||||
\<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
|
||||
apply (simp add: Thread_H.switchToIdleThread_def
|
||||
ARM_H.switchToIdleThread_def storeWordUser_def)
|
||||
X64_H.switchToIdleThread_def storeWordUser_def)
|
||||
apply (wp setCurThread_nosch | simp add: getIdleThread_def)+
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -716,7 +716,7 @@ lemma diminished_ReplyCap' [simp]:
|
|||
apply (rule iffI)
|
||||
apply (clarsimp simp: diminished'_def maskCapRights_def Let_def split del: if_split)
|
||||
apply (cases cap, simp_all add: isCap_simps)[1]
|
||||
apply (simp add: ARM_H.maskCapRights_def isPageCap_def split: arch_capability.splits)
|
||||
apply (simp add: X64_H.maskCapRights_def isPageCap_def split: arch_capability.splits)
|
||||
apply (simp add: diminished'_def maskCapRights_def isCap_simps Let_def)
|
||||
done
|
||||
|
||||
|
|
@ -1903,14 +1903,14 @@ lemma getIFSR_invs'[wp]:
|
|||
by (simp add: getIFSR_def doMachineOp_def split_def select_f_returns | wp)+
|
||||
|
||||
lemma hv_invs'[wp]: "\<lbrace>invs' and tcb_at' t'\<rbrace> handleVMFault t' vptr \<lbrace>\<lambda>r. invs'\<rbrace>"
|
||||
apply (simp add: ARM_H.handleVMFault_def
|
||||
apply (simp add: X64_H.handleVMFault_def
|
||||
cong: vmfault_type.case_cong)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | wpcw | simp)+
|
||||
done
|
||||
|
||||
lemma hv_tcb'[wp]: "\<lbrace>tcb_at' t\<rbrace> handleVMFault t' vptr \<lbrace>\<lambda>r. tcb_at' t\<rbrace>"
|
||||
apply (simp add: ARM_H.handleVMFault_def
|
||||
apply (simp add: X64_H.handleVMFault_def
|
||||
cong: vmfault_type.case_cong)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp | wpcw)+
|
||||
|
|
@ -1922,7 +1922,7 @@ crunch nosch[wp]: handleVMFault "\<lambda>s. P (ksSchedulerAction s)"
|
|||
|
||||
lemma hv_inv_ex':
|
||||
"\<lbrace>P\<rbrace> handleVMFault t vp \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>"
|
||||
apply (simp add: ARM_H.handleVMFault_def
|
||||
apply (simp add: X64_H.handleVMFault_def
|
||||
cong: vmfault_type.case_cong)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp dmo_inv' getDFSR_inv getFAR_inv getIFSR_inv getRestartPC_inv
|
||||
|
|
@ -2346,7 +2346,7 @@ crunch ksit[wp]: handleVMFault,handleHypervisorFault "\<lambda>s. P (ksIdleThrea
|
|||
|
||||
lemma hv_inv':
|
||||
"\<lbrace>P\<rbrace> handleVMFault p t \<lbrace>\<lambda>_. P\<rbrace>"
|
||||
apply (simp add: ARM_H.handleVMFault_def)
|
||||
apply (simp add: X64_H.handleVMFault_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp dmo_inv' getDFSR_inv getFAR_inv getIFSR_inv getRestartPC_inv
|
||||
det_getRestartPC asUser_inv
|
||||
|
|
@ -2355,7 +2355,7 @@ lemma hv_inv':
|
|||
|
||||
lemma hh_inv':
|
||||
"\<lbrace>P\<rbrace> handleHypervisorFault p t \<lbrace>\<lambda>_. P\<rbrace>"
|
||||
apply (simp add: ARM_H.handleHypervisorFault_def)
|
||||
apply (simp add: X64_H.handleHypervisorFault_def)
|
||||
apply (cases t; clarsimp)
|
||||
done
|
||||
|
||||
|
|
@ -2429,13 +2429,13 @@ lemma inv_irq_IRQInactive:
|
|||
-, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>"
|
||||
apply (simp add: performIRQControl_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wpc|wp|simp add: ARM_H.performIRQControl_def)+
|
||||
apply (wpc|wp|simp add: X64_H.performIRQControl_def)+
|
||||
done
|
||||
|
||||
lemma inv_arch_IRQInactive:
|
||||
"\<lbrace>\<top>\<rbrace> Arch.performInvocation invocation
|
||||
-, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>"
|
||||
apply (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def)
|
||||
apply (simp add: X64_H.performInvocation_def performARMMMUInvocation_def)
|
||||
apply wp
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -358,7 +358,7 @@ lemma pspace_relation_tcb_at:
|
|||
apply (erule(1) obj_relation_cutsE)
|
||||
apply (clarsimp simp: other_obj_relation_def is_tcb obj_at_def
|
||||
split: Structures_A.kernel_object.split_asm if_split_asm
|
||||
ARM_A.arch_kernel_obj.split_asm)+
|
||||
X64_A.arch_kernel_obj.split_asm)+
|
||||
done
|
||||
|
||||
lemma threadSet_corres_noopT:
|
||||
|
|
@ -3576,7 +3576,7 @@ lemma store_word_corres:
|
|||
done
|
||||
|
||||
lemmas msgRegisters_unfold
|
||||
= ARM_H.msgRegisters_def
|
||||
= X64_H.msgRegisters_def
|
||||
msg_registers_def
|
||||
ARM.msgRegisters_def
|
||||
[unfolded upto_enum_def, simplified,
|
||||
|
|
@ -3591,12 +3591,12 @@ lemma get_mrs_corres:
|
|||
have S: "get = gets id"
|
||||
by (simp add: gets_def)
|
||||
have T: "corres (\<lambda>con regs. regs = map con msg_registers) (tcb_at t) (tcb_at' t)
|
||||
(thread_get (arch_tcb_context_get o tcb_arch) t) (asUser t (mapM getRegister ARM_H.msgRegisters))"
|
||||
(thread_get (arch_tcb_context_get o tcb_arch) t) (asUser t (mapM getRegister X64_H.msgRegisters))"
|
||||
apply (subst thread_get_as_user)
|
||||
apply (rule corres_as_user')
|
||||
apply (subst mapM_gets)
|
||||
apply (simp add: getRegister_def)
|
||||
apply (simp add: S ARM_H.msgRegisters_def msg_registers_def)
|
||||
apply (simp add: S X64_H.msgRegisters_def msg_registers_def)
|
||||
done
|
||||
show ?thesis
|
||||
apply (case_tac mi, simp add: get_mrs_def getMRs_def split del: if_split)
|
||||
|
|
@ -3913,7 +3913,7 @@ lemma lipcb_corres':
|
|||
(tcb_at' t and valid_objs' and pspace_aligned'
|
||||
and pspace_distinct' and no_0_obj')
|
||||
(lookup_ipc_buffer w t) (lookupIPCBuffer w t)"
|
||||
apply (simp add: lookup_ipc_buffer_def ARM_H.lookupIPCBuffer_def)
|
||||
apply (simp add: lookup_ipc_buffer_def X64_H.lookupIPCBuffer_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_eqr [OF _ threadget_corres])
|
||||
apply (simp add: getThreadBufferSlot_def locateSlot_conv)
|
||||
|
|
@ -4991,7 +4991,7 @@ lemma set_eobject_corres':
|
|||
apply (clarsimp simp: non_exst_same_def)
|
||||
apply (case_tac bb; simp)
|
||||
apply (clarsimp simp: obj_at'_def other_obj_relation_def cte_relation_def tcb_relation_def projectKOs split: if_split_asm)+
|
||||
apply (clarsimp simp: aobj_relation_cuts_def split: ARM_A.arch_kernel_obj.splits)
|
||||
apply (clarsimp simp: aobj_relation_cuts_def split: X64_A.arch_kernel_obj.splits)
|
||||
apply (rename_tac arch_kernel_obj obj d p ts)
|
||||
apply (case_tac arch_kernel_obj; simp)
|
||||
apply (clarsimp simp: pte_relation_def pde_relation_def is_tcb_def
|
||||
|
|
@ -5003,7 +5003,7 @@ lemma set_eobject_corres':
|
|||
apply (clarsimp simp: obj_at'_def)
|
||||
apply (clarsimp simp: projectKOs)
|
||||
apply (insert e)
|
||||
apply (clarsimp simp: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits ARM_A.arch_kernel_obj.splits)
|
||||
apply (clarsimp simp: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits X64_A.arch_kernel_obj.splits)
|
||||
done
|
||||
|
||||
lemma set_eobject_corres:
|
||||
|
|
|
|||
|
|
@ -829,7 +829,7 @@ lemma sameObject_corres2:
|
|||
apply clarsimp
|
||||
apply (case_tac d, (simp_all split: arch_cap.split)[11])
|
||||
apply (rename_tac arch_capa)
|
||||
apply (clarsimp simp add: ARM_H.sameObjectAs_def Let_def)
|
||||
apply (clarsimp simp add: X64_H.sameObjectAs_def Let_def)
|
||||
apply (intro conjI impI)
|
||||
apply (case_tac arch_cap; simp add: isCap_simps del: not_ex)
|
||||
apply (case_tac arch_capa; clarsimp simp del: not_ex)
|
||||
|
|
@ -999,7 +999,7 @@ lemma isValidVTableRootD:
|
|||
\<Longrightarrow> isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap)
|
||||
\<and> capPDMappedASID (capCap cap) \<noteq> None"
|
||||
by (simp add: isValidVTableRoot_def
|
||||
ARM_H.isValidVTableRoot_def
|
||||
X64_H.isValidVTableRoot_def
|
||||
isCap_simps
|
||||
split: capability.split_asm arch_capability.split_asm
|
||||
option.split_asm)
|
||||
|
|
@ -1221,7 +1221,7 @@ proof -
|
|||
do bufferSlot \<leftarrow> getThreadBufferSlot a;
|
||||
doE y \<leftarrow> cteDelete bufferSlot True;
|
||||
do y \<leftarrow> threadSet (tcbIPCBuffer_update (\<lambda>_. ptr)) a;
|
||||
y \<leftarrow> asUser a (setRegister ARM_H.tpidrurwRegister ptr);
|
||||
y \<leftarrow> asUser a (setRegister X64_H.tpidrurwRegister ptr);
|
||||
liftE
|
||||
(case_option (return ())
|
||||
(case_prod
|
||||
|
|
@ -1248,7 +1248,7 @@ proof -
|
|||
apply (rule corres_split_norE)
|
||||
apply (rule corres_split_nor)
|
||||
apply (rule corres_split')
|
||||
apply (simp add: ARM_H.tpidrurwRegister_def ARM.tpidrurwRegister_def)
|
||||
apply (simp add: X64_H.tpidrurwRegister_def ARM.tpidrurwRegister_def)
|
||||
apply (rule user_setreg_corres)
|
||||
apply (rule corres_trivial)
|
||||
apply simp
|
||||
|
|
@ -1267,7 +1267,7 @@ proof -
|
|||
in corres_gen_asm)
|
||||
apply (rule corres_split_nor)
|
||||
apply (rule corres_split[rotated])
|
||||
apply (simp add: ARM_H.tpidrurwRegister_def ARM.tpidrurwRegister_def)
|
||||
apply (simp add: X64_H.tpidrurwRegister_def ARM.tpidrurwRegister_def)
|
||||
apply (rule user_setreg_corres)
|
||||
prefer 3
|
||||
apply simp
|
||||
|
|
@ -1977,7 +1977,7 @@ lemma check_valid_ipc_corres:
|
|||
(checkValidIPCBuffer vptr cap')"
|
||||
apply (simp add: check_valid_ipc_buffer_def
|
||||
checkValidIPCBuffer_def
|
||||
ARM_H.checkValidIPCBuffer_def
|
||||
X64_H.checkValidIPCBuffer_def
|
||||
unlessE_def Let_def
|
||||
split: cap_relation_split_asm arch_cap.split_asm bool.splits)
|
||||
apply (simp add: capTransferDataSize_def msgMaxLength_def
|
||||
|
|
@ -1993,7 +1993,7 @@ lemma checkValidIPCBuffer_ArchObject_wp:
|
|||
checkValidIPCBuffer x cap
|
||||
\<lbrace>\<lambda>rv s. P s\<rbrace>,-"
|
||||
apply (simp add: checkValidIPCBuffer_def
|
||||
ARM_H.checkValidIPCBuffer_def
|
||||
X64_H.checkValidIPCBuffer_def
|
||||
whenE_def unlessE_def
|
||||
cong: capability.case_cong
|
||||
arch_capability.case_cong
|
||||
|
|
@ -2148,7 +2148,7 @@ lemma decode_set_space_corres:
|
|||
apply (rule corres_whenE)
|
||||
apply (case_tac vroot_cap', simp_all add:
|
||||
is_valid_vtable_root_def isValidVTableRoot_def
|
||||
ARM_H.isValidVTableRoot_def)[1]
|
||||
X64_H.isValidVTableRoot_def)[1]
|
||||
apply (rename_tac arch_cap)
|
||||
apply (clarsimp, case_tac arch_cap, simp_all)[1]
|
||||
apply (simp split: option.split)
|
||||
|
|
@ -2382,7 +2382,7 @@ lemma tcb_real_cte_16:
|
|||
|
||||
lemma isValidVTableRoot:
|
||||
"isValidVTableRoot c = (\<exists>p asid. c = ArchObjectCap (PageDirectoryCap p (Some asid)))"
|
||||
by (simp add: ARM_H.isValidVTableRoot_def isCap_simps
|
||||
by (simp add: X64_H.isValidVTableRoot_def isCap_simps
|
||||
split: capability.splits arch_capability.splits option.splits)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -65,7 +65,7 @@ lemma APIType_map2_CapTable[simp]:
|
|||
"(APIType_map2 ty = Structures_A.CapTableObject)
|
||||
= (ty = Inr (APIObjectType ArchTypes_H.CapTableObject))"
|
||||
by (simp add: APIType_map2_def
|
||||
split: sum.split ARM_H.object_type.split
|
||||
split: sum.split X64_H.object_type.split
|
||||
apiobject_type.split
|
||||
kernel_object.split arch_kernel_object.splits)
|
||||
|
||||
|
|
@ -186,7 +186,7 @@ next
|
|||
by (simp add: whenE_def returnOk_def)
|
||||
have Q: "\<And>v. corres (ser \<oplus> (\<lambda>a b. APIType_map2 (Inr (toEnum (unat v))) = a)) \<top> \<top>
|
||||
(data_to_obj_type v)
|
||||
(whenE (fromEnum (maxBound :: ARM_H.object_type) < unat v)
|
||||
(whenE (fromEnum (maxBound :: X64_H.object_type) < unat v)
|
||||
(throwError (Fault_H.syscall_error.InvalidArgument 0)))"
|
||||
apply (simp only: data_to_obj_type_def returnOk_bindE fun_app_def)
|
||||
apply (simp add: maxBound_def enum_apiobject_type
|
||||
|
|
@ -287,9 +287,9 @@ next
|
|||
toInteger_nat fromInteger_nat linorder_not_less)
|
||||
apply fastforce
|
||||
apply (rule whenE_throwError_corres, simp)
|
||||
apply (clarsimp simp: fromAPIType_def ARM_H.fromAPIType_def)
|
||||
apply (clarsimp simp: fromAPIType_def X64_H.fromAPIType_def)
|
||||
apply (rule whenE_throwError_corres, simp)
|
||||
apply (clarsimp simp: fromAPIType_def ARM_H.fromAPIType_def)
|
||||
apply (clarsimp simp: fromAPIType_def X64_H.fromAPIType_def)
|
||||
apply (rule_tac r' = "\<lambda>cap cap'. cap_relation cap cap'" in corres_splitEE[OF _ corres_if])
|
||||
apply (rule_tac corres_split_norE)
|
||||
prefer 2
|
||||
|
|
@ -831,7 +831,7 @@ lemma decodeUntyped_wf[wp]:
|
|||
apply (clarsimp dest!:valid_capAligned
|
||||
simp:capAligned_def objBits_def objBitsKO_def)
|
||||
apply (simp_all add: word_bits_def)[2]
|
||||
apply (clarsimp simp: ARM_H.fromAPIType_def)
|
||||
apply (clarsimp simp: X64_H.fromAPIType_def)
|
||||
apply (subgoal_tac "Suc (unat (args ! 4 + args ! 5 - 1))
|
||||
= unat (args ! 4) + unat (args ! 5)")
|
||||
prefer 2
|
||||
|
|
@ -3291,7 +3291,7 @@ where
|
|||
| "isDeviceCap (ArchObjectCap (PageCap d _ _ _ _)) = d"
|
||||
| "isDeviceCap _ = False"
|
||||
|
||||
lemmas makeObjectKO_simp = makeObjectKO_def[split_simps ARM_H.object_type.split
|
||||
lemmas makeObjectKO_simp = makeObjectKO_def[split_simps X64_H.object_type.split
|
||||
Structures_H.kernel_object.split ArchTypes_H.apiobject_type.split
|
||||
sum.split arch_kernel_object.split]
|
||||
|
||||
|
|
@ -3656,7 +3656,7 @@ lemma getObjectSize_def_eq:
|
|||
apply (rename_tac apiobject_type)
|
||||
apply (case_tac apiobject_type)
|
||||
apply (clarsimp simp: getObjectSize_def apiGetObjectSize_def APIType_map2_def
|
||||
ARM_H.getObjectSize_def obj_bits_api_def tcbBlockSizeBits_def
|
||||
X64_H.getObjectSize_def obj_bits_api_def tcbBlockSizeBits_def
|
||||
epSizeBits_def ntfnSizeBits_def cteSizeBits_def slot_bits_def
|
||||
arch_kobj_size_def default_arch_object_def ptBits_def pageBits_def
|
||||
pdBits_def simp del: APIType_capBits)+
|
||||
|
|
@ -5953,11 +5953,11 @@ lemma zipWithM_x_insertNewCap_invs':
|
|||
|
||||
lemma createNewCaps_not_isZombie[wp]:
|
||||
"\<lbrace>\<top>\<rbrace> createNewCaps ty ptr bits sz d \<lbrace>\<lambda>rv s. (\<forall>cap \<in> set rv. \<not> isZombie cap)\<rbrace>"
|
||||
apply (simp add: createNewCaps_def toAPIType_def ARM_H.toAPIType_def
|
||||
apply (simp add: createNewCaps_def toAPIType_def X64_H.toAPIType_def
|
||||
createNewCaps_def
|
||||
split del: if_split cong: option.case_cong if_cong
|
||||
apiobject_type.case_cong
|
||||
ARM_H.object_type.case_cong)
|
||||
X64_H.object_type.case_cong)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp undefined_valid | wpc
|
||||
| simp add: isCap_simps)+
|
||||
|
|
@ -5988,7 +5988,7 @@ crunch it[wp]: copyGlobalMappings "\<lambda>s. P (ksIdleThread s)"
|
|||
lemma createNewCaps_idlethread[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> createNewCaps tp ptr sz us d \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>"
|
||||
apply (simp add: createNewCaps_def toAPIType_def
|
||||
split: ARM_H.object_type.split
|
||||
split: X64_H.object_type.split
|
||||
apiobject_type.split)
|
||||
apply safe
|
||||
apply (wp mapM_x_wp' | simp)+
|
||||
|
|
|
|||
|
|
@ -28,13 +28,13 @@ crunch_ignore (add: throw_on_false)
|
|||
|
||||
definition
|
||||
"pd_at_asid' pd asid \<equiv> \<lambda>s. \<exists>ap pool.
|
||||
armKSASIDTable (ksArchState s) (ucast (asid_high_bits_of asid)) = Some ap \<and>
|
||||
x64KSASIDTable (ksArchState s) (ucast (asid_high_bits_of asid)) = Some ap \<and>
|
||||
ko_at' (ASIDPool pool) ap s \<and> pool (asid && mask asid_low_bits) = Some pd \<and>
|
||||
page_directory_at' pd s"
|
||||
|
||||
defs checkPDASIDMapMembership_def:
|
||||
"checkPDASIDMapMembership pd asids
|
||||
\<equiv> stateAssert (\<lambda>s. pd \<notin> ran ((option_map snd o armKSASIDMap (ksArchState s) |` (- set asids)))) []"
|
||||
\<equiv> stateAssert (\<lambda>s. pd \<notin> ran ((option_map snd o x64KSASIDMap (ksArchState s) |` (- set asids)))) []"
|
||||
|
||||
crunch inv[wp]:checkPDAt P
|
||||
|
||||
|
|
@ -55,7 +55,7 @@ lemma findPDForASID_pd_at_wp:
|
|||
|
||||
lemma findPDForASIDAssert_pd_at_wp:
|
||||
"\<lbrace>(\<lambda>s. \<forall>pd. pd_at_asid' pd asid s
|
||||
\<and> pd \<notin> ran ((option_map snd o armKSASIDMap (ksArchState s) |` (- {asid})))
|
||||
\<and> pd \<notin> ran ((option_map snd o x64KSASIDMap (ksArchState s) |` (- {asid})))
|
||||
\<longrightarrow> P pd s)\<rbrace>
|
||||
findPDForASIDAssert asid \<lbrace>P\<rbrace>"
|
||||
apply (simp add: findPDForASIDAssert_def const_def
|
||||
|
|
@ -179,8 +179,8 @@ lemma valid_asid_map_inj_map:
|
|||
unique_table_refs (caps_of_state s);
|
||||
valid_vs_lookup s; valid_arch_objs s;
|
||||
valid_arch_state s; valid_global_objs s \<rbrakk>
|
||||
\<Longrightarrow> inj_on (option_map snd \<circ> armKSASIDMap (ksArchState s'))
|
||||
(dom (armKSASIDMap (ksArchState s')))"
|
||||
\<Longrightarrow> inj_on (option_map snd \<circ> x64KSASIDMap (ksArchState s'))
|
||||
(dom (x64KSASIDMap (ksArchState s')))"
|
||||
apply (rule inj_onI)
|
||||
apply (clarsimp simp: valid_asid_map_def state_relation_def
|
||||
arch_state_relation_def)
|
||||
|
|
@ -491,7 +491,7 @@ lemma get_hw_asid_corres:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma arm_context_switch_corres:
|
||||
lemma x64_context_switch_corres:
|
||||
"corres dc
|
||||
(vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask asid_bits)
|
||||
and unique_table_refs o caps_of_state
|
||||
|
|
@ -500,8 +500,8 @@ lemma arm_context_switch_corres:
|
|||
and pspace_aligned and pspace_distinct
|
||||
and valid_arch_state)
|
||||
(pspace_aligned' and pspace_distinct' and no_0_obj')
|
||||
(arm_context_switch pd a) (armv_contextSwitch pd a)"
|
||||
apply (simp add: arm_context_switch_def armv_contextSwitch_def armv_contextSwitch_HWASID_def)
|
||||
(x64_context_switch pd a) (armv_contextSwitch pd a)"
|
||||
apply (simp add: x64_context_switch_def armv_contextSwitch_def armv_contextSwitch_HWASID_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_eqr [OF _ get_hw_asid_corres[where pd=pd]])
|
||||
apply (rule corres_machine_op)
|
||||
|
|
@ -514,7 +514,7 @@ lemma arm_context_switch_corres:
|
|||
lemma hv_corres:
|
||||
"corres (fr \<oplus> dc) (tcb_at thread) (tcb_at' thread)
|
||||
(handle_vm_fault thread fault) (handleVMFault thread fault)"
|
||||
apply (simp add: ARM_H.handleVMFault_def)
|
||||
apply (simp add: X64_H.handleVMFault_def)
|
||||
apply (cases fault)
|
||||
apply simp
|
||||
apply (rule corres_guard_imp)
|
||||
|
|
@ -629,7 +629,7 @@ lemma invalidate_tlb_by_asid_corres_ex:
|
|||
|
||||
crunch valid_global_objs[wp]: do_machine_op "valid_global_objs"
|
||||
lemma state_relation_asid_map:
|
||||
"(s, s') \<in> state_relation \<Longrightarrow> armKSASIDMap (ksArchState s') = arm_asid_map (arch_state s)"
|
||||
"(s, s') \<in> state_relation \<Longrightarrow> x64KSASIDMap (ksArchState s') = x64_asid_map (arch_state s)"
|
||||
by (simp add: state_relation_def arch_state_relation_def)
|
||||
|
||||
lemma find_pd_for_asid_pd_at_asid_again:
|
||||
|
|
@ -680,10 +680,10 @@ lemma set_vm_root_corres:
|
|||
(set_vm_root t) (setVMRoot t)"
|
||||
proof -
|
||||
have P: "corres dc \<top> \<top>
|
||||
(do global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
|
||||
(do global_pd \<leftarrow> gets (x64_global_pd \<circ> arch_state);
|
||||
do_machine_op (setCurrentPD (addrFromPPtr global_pd))
|
||||
od)
|
||||
(do globalPD \<leftarrow> gets (armKSGlobalPD \<circ> ksArchState);
|
||||
(do globalPD \<leftarrow> gets (x64KSGlobalPD \<circ> ksArchState);
|
||||
doMachineOp (setCurrentPD (addrFromPPtr globalPD))
|
||||
od)"
|
||||
apply (rule corres_guard_imp)
|
||||
|
|
@ -695,11 +695,11 @@ proof -
|
|||
done
|
||||
have Q: "\<And>P P'. corres dc P P'
|
||||
(throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch>
|
||||
(\<lambda>_ . do global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
|
||||
(\<lambda>_ . do global_pd \<leftarrow> gets (x64_global_pd \<circ> arch_state);
|
||||
do_machine_op $ setCurrentPD $ addrFromPPtr global_pd
|
||||
od))
|
||||
(throwError Fault_H.lookup_failure.InvalidRoot <catch>
|
||||
(\<lambda>_ . do globalPD \<leftarrow> gets (armKSGlobalPD \<circ> ksArchState);
|
||||
(\<lambda>_ . do globalPD \<leftarrow> gets (x64KSGlobalPD \<circ> ksArchState);
|
||||
doMachineOp $ setCurrentPD $ addrFromPPtr globalPD
|
||||
od))"
|
||||
apply (rule corres_guard_imp)
|
||||
|
|
@ -755,7 +755,7 @@ proof -
|
|||
apply (simp add: lookup_failure_map_def)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (rule arm_context_switch_corres)
|
||||
apply (rule x64_context_switch_corres)
|
||||
apply (wp | simp | wp_once hoare_drop_imps)+
|
||||
apply (simp add: whenE_def split del: if_split, wp)[1]
|
||||
apply (rule find_pd_for_asid_pd_at_asid_again)
|
||||
|
|
@ -798,7 +798,7 @@ lemma get_asid_pool_corres_inv':
|
|||
done
|
||||
|
||||
lemma loadHWASID_wp [wp]:
|
||||
"\<lbrace>\<lambda>s. P (option_map fst (armKSASIDMap (ksArchState s) asid)) s\<rbrace>
|
||||
"\<lbrace>\<lambda>s. P (option_map fst (x64KSASIDMap (ksArchState s) asid)) s\<rbrace>
|
||||
loadHWASID asid \<lbrace>P\<rbrace>"
|
||||
apply (simp add: loadHWASID_def)
|
||||
apply (wp findPDForASIDAssert_pd_at_wp
|
||||
|
|
@ -873,7 +873,7 @@ lemma delete_asid_corres:
|
|||
asid_pool_at (the ((asidTable o ucast) (asid_high_bits_of asid))) s" and
|
||||
P'="pspace_aligned' and pspace_distinct'" and
|
||||
Q="invs and valid_etcbs and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0) and
|
||||
(\<lambda>s. arm_asid_table (arch_state s) = asidTable \<circ> ucast)" in
|
||||
(\<lambda>s. x64_asid_table (arch_state s) = asidTable \<circ> ucast)" in
|
||||
corres_split)
|
||||
prefer 2
|
||||
apply (simp add: dom_def)
|
||||
|
|
@ -936,16 +936,16 @@ lemma delete_asid_corres:
|
|||
lemma valid_arch_state_unmap_strg':
|
||||
"valid_arch_state' s \<longrightarrow>
|
||||
valid_arch_state' (s\<lparr>ksArchState :=
|
||||
armKSASIDTable_update (\<lambda>_. (armKSASIDTable (ksArchState s))(ptr := None))
|
||||
x64KSASIDTable_update (\<lambda>_. (x64KSASIDTable (ksArchState s))(ptr := None))
|
||||
(ksArchState s)\<rparr>)"
|
||||
apply (simp add: valid_arch_state'_def valid_asid_table'_def)
|
||||
apply (auto simp: ran_def split: if_split_asm)
|
||||
done
|
||||
|
||||
crunch armKSASIDTable_inv[wp]: invalidateASIDEntry
|
||||
"\<lambda>s. P (armKSASIDTable (ksArchState s))"
|
||||
crunch armKSASIDTable_inv[wp]: flushSpace
|
||||
"\<lambda>s. P (armKSASIDTable (ksArchState s))"
|
||||
crunch x64KSASIDTable_inv[wp]: invalidateASIDEntry
|
||||
"\<lambda>s. P (x64KSASIDTable (ksArchState s))"
|
||||
crunch x64KSASIDTable_inv[wp]: flushSpace
|
||||
"\<lambda>s. P (x64KSASIDTable (ksArchState s))"
|
||||
|
||||
lemma delete_asid_pool_corres:
|
||||
"corres dc
|
||||
|
|
@ -1054,7 +1054,7 @@ lemma delete_asid_pool_corres:
|
|||
apply (simp only:)
|
||||
apply (rule set_vm_root_corres)
|
||||
apply wp+
|
||||
apply (rule_tac R="\<lambda>_ s. rv = arm_asid_table (arch_state s)"
|
||||
apply (rule_tac R="\<lambda>_ s. rv = x64_asid_table (arch_state s)"
|
||||
in hoare_post_add)
|
||||
apply (drule sym, simp only: )
|
||||
apply (drule sym, simp only: )
|
||||
|
|
@ -1070,7 +1070,7 @@ lemma delete_asid_pool_corres:
|
|||
apply (rule hoare_vcg_conj_lift,
|
||||
(rule mapM_invalidate[where ptr=ptr])?,
|
||||
((wp mapM_wp' | simp)+)[1])+
|
||||
apply (rule_tac R="\<lambda>_ s. rv' = armKSASIDTable (ksArchState s)"
|
||||
apply (rule_tac R="\<lambda>_ s. rv' = x64KSASIDTable (ksArchState s)"
|
||||
in hoare_post_add)
|
||||
apply (simp only: pred_conj_def cong: conj_cong)
|
||||
apply simp
|
||||
|
|
@ -1106,14 +1106,14 @@ proof -
|
|||
and valid_arch_state
|
||||
and pspace_aligned and pspace_distinct)
|
||||
(pspace_aligned' and pspace_distinct' and no_0_obj')
|
||||
(do arm_context_switch pd asid;
|
||||
(do x64_context_switch pd asid;
|
||||
return True
|
||||
od)
|
||||
(do armv_contextSwitch pd asid;
|
||||
return True
|
||||
od)"
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split [OF _ arm_context_switch_corres])
|
||||
apply (rule corres_split [OF _ x64_context_switch_corres])
|
||||
apply (rule corres_trivial)
|
||||
apply (wp | simp)+
|
||||
done
|
||||
|
|
@ -1185,8 +1185,8 @@ lemma findPDForASID_inv2:
|
|||
|
||||
lemma storeHWASID_valid_arch' [wp]:
|
||||
"\<lbrace>valid_arch_state' and
|
||||
(\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and>
|
||||
armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace>
|
||||
(\<lambda>s. x64KSASIDMap (ksArchState s) asid = None \<and>
|
||||
x64KSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace>
|
||||
storeHWASID asid hw_asid
|
||||
\<lbrace>\<lambda>_. valid_arch_state'\<rbrace>"
|
||||
apply (simp add: storeHWASID_def)
|
||||
|
|
@ -1198,7 +1198,7 @@ lemma storeHWASID_valid_arch' [wp]:
|
|||
apply (simp add: findPDForASIDAssert_def const_def
|
||||
checkPDUniqueToASID_def checkPDASIDMapMembership_def)
|
||||
apply wp
|
||||
apply (rule_tac Q'="\<lambda>rv s. valid_asid_map' (armKSASIDMap (ksArchState s))
|
||||
apply (rule_tac Q'="\<lambda>rv s. valid_asid_map' (x64KSASIDMap (ksArchState s))
|
||||
\<and> asid \<noteq> 0 \<and> asid \<le> mask asid_bits"
|
||||
in hoare_post_imp_R)
|
||||
apply (wp findPDForASID_inv2)+
|
||||
|
|
@ -1238,13 +1238,13 @@ lemma findFreeHWASID_valid_arch [wp]:
|
|||
comp_upd_simp valid_asid_map'_def)
|
||||
apply (frule is_inv_inj)
|
||||
apply (drule findNoneD)
|
||||
apply (drule_tac x="armKSNextASID (ksArchState s)" in bspec)
|
||||
apply (drule_tac x="x64KSNextASID (ksArchState s)" in bspec)
|
||||
apply clarsimp
|
||||
apply (clarsimp simp: is_inv_def ran_upd[folded fun_upd_def]
|
||||
dom_option_map inj_on_fun_upd_elsewhere)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (drule_tac x="x" and y="armKSNextASID (ksArchState s)" in inj_onD)
|
||||
apply (drule_tac x="x" and y="x64KSNextASID (ksArchState s)" in inj_onD)
|
||||
apply simp
|
||||
apply blast
|
||||
apply blast
|
||||
|
|
@ -1256,9 +1256,9 @@ lemma findFreeHWASID_valid_arch [wp]:
|
|||
done
|
||||
|
||||
lemma findFreeHWASID_None_map [wp]:
|
||||
"\<lbrace>\<lambda>s. armKSASIDMap (ksArchState s) asid = None\<rbrace>
|
||||
"\<lbrace>\<lambda>s. x64KSASIDMap (ksArchState s) asid = None\<rbrace>
|
||||
findFreeHWASID
|
||||
\<lbrace>\<lambda>rv s. armKSASIDMap (ksArchState s) asid = None\<rbrace>"
|
||||
\<lbrace>\<lambda>rv s. x64KSASIDMap (ksArchState s) asid = None\<rbrace>"
|
||||
apply (simp add: findFreeHWASID_def invalidateHWASIDEntry_def invalidateASID_def
|
||||
doMachineOp_def split_def
|
||||
cong: option.case_cong)
|
||||
|
|
@ -1268,7 +1268,7 @@ lemma findFreeHWASID_None_map [wp]:
|
|||
done
|
||||
|
||||
lemma findFreeHWASID_None_HWTable [wp]:
|
||||
"\<lbrace>\<top>\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. armKSHWASIDTable (ksArchState s) rv = None\<rbrace>"
|
||||
"\<lbrace>\<top>\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. x64KSHWASIDTable (ksArchState s) rv = None\<rbrace>"
|
||||
apply (simp add: findFreeHWASID_def invalidateHWASIDEntry_def invalidateASID_def
|
||||
doMachineOp_def
|
||||
cong: option.case_cong)
|
||||
|
|
@ -1407,7 +1407,7 @@ lemma page_table_mapped_corres:
|
|||
apply (rule corres_trivial)
|
||||
apply (case_tac rv,
|
||||
simp_all add: returnOk_def pde_relation_aligned_def
|
||||
split:if_splits ARM_H.pde.splits)[1]
|
||||
split:if_splits X64_H.pde.splits)[1]
|
||||
apply (wp | simp add: lookup_pd_slot_def Let_def)+
|
||||
apply (simp add: word_neq_0_conv)
|
||||
apply simp
|
||||
|
|
@ -1506,7 +1506,7 @@ lemma check_mapping_corres:
|
|||
auto simp add: is_aligned_mask[symmetric]
|
||||
is_aligned_shiftr pg_entry_align_def
|
||||
unlessE_def returnOk_def pte_relation_aligned_def
|
||||
split: ARM_A.pte.split if_splits ARM_H.pte.split )
|
||||
split: X64_A.pte.split if_splits X64_H.pte.split )
|
||||
apply wp+
|
||||
apply simp
|
||||
apply (simp add:is_aligned_mask[symmetric] is_aligned_shiftr pg_entry_align_def)
|
||||
|
|
@ -1517,7 +1517,7 @@ lemma check_mapping_corres:
|
|||
auto simp add: is_aligned_mask[symmetric]
|
||||
is_aligned_shiftr pg_entry_align_def
|
||||
unlessE_def returnOk_def pde_relation_aligned_def
|
||||
split: ARM_A.pde.split if_splits ARM_H.pde.split )
|
||||
split: X64_A.pde.split if_splits X64_H.pde.split )
|
||||
apply wp+
|
||||
apply simp+
|
||||
done
|
||||
|
|
@ -1674,10 +1674,10 @@ lemma unmap_page_corres:
|
|||
|
||||
definition
|
||||
"flush_type_map type \<equiv> case type of
|
||||
ARM_A.flush_type.Clean \<Rightarrow> ARM_H.flush_type.Clean
|
||||
| ARM_A.flush_type.Invalidate \<Rightarrow> ARM_H.flush_type.Invalidate
|
||||
| ARM_A.flush_type.CleanInvalidate \<Rightarrow> ARM_H.flush_type.CleanInvalidate
|
||||
| ARM_A.flush_type.Unify \<Rightarrow> ARM_H.flush_type.Unify"
|
||||
X64_A.flush_type.Clean \<Rightarrow> X64_H.flush_type.Clean
|
||||
| X64_A.flush_type.Invalidate \<Rightarrow> X64_H.flush_type.Invalidate
|
||||
| X64_A.flush_type.CleanInvalidate \<Rightarrow> X64_H.flush_type.CleanInvalidate
|
||||
| X64_A.flush_type.Unify \<Rightarrow> X64_H.flush_type.Unify"
|
||||
|
||||
lemma do_flush_corres:
|
||||
"corres_underlying Id nf nf' dc \<top> \<top>
|
||||
|
|
@ -1698,8 +1698,8 @@ lemma do_flush_corres:
|
|||
|
||||
definition
|
||||
"page_directory_invocation_map pdi pdi' \<equiv> case pdi of
|
||||
ARM_A.PageDirectoryNothing \<Rightarrow> pdi' = PageDirectoryNothing
|
||||
| ARM_A.PageDirectoryFlush typ start end pstart pd asid \<Rightarrow>
|
||||
X64_A.PageDirectoryNothing \<Rightarrow> pdi' = PageDirectoryNothing
|
||||
| X64_A.PageDirectoryFlush typ start end pstart pd asid \<Rightarrow>
|
||||
pdi' = PageDirectoryFlush (flush_type_map typ) start end pstart pd asid"
|
||||
|
||||
lemma perform_page_directory_corres:
|
||||
|
|
@ -1733,19 +1733,19 @@ lemma perform_page_directory_corres:
|
|||
|
||||
definition
|
||||
"page_invocation_map pgi pgi' \<equiv> case pgi of
|
||||
ARM_A.PageMap a c ptr m \<Rightarrow>
|
||||
X64_A.PageMap a c ptr m \<Rightarrow>
|
||||
\<exists>c' m'. pgi' = PageMap a c' (cte_map ptr) m' \<and>
|
||||
cap_relation c c' \<and>
|
||||
mapping_map m m'
|
||||
|
||||
| ARM_A.PageRemap a m \<Rightarrow>
|
||||
| X64_A.PageRemap a m \<Rightarrow>
|
||||
\<exists>m'. pgi' = PageRemap a m' \<and> mapping_map m m'
|
||||
| ARM_A.PageUnmap c ptr \<Rightarrow>
|
||||
| X64_A.PageUnmap c ptr \<Rightarrow>
|
||||
\<exists>c'. pgi' = PageUnmap c' (cte_map ptr) \<and>
|
||||
acap_relation c c'
|
||||
| ARM_A.PageFlush typ start end pstart pd asid \<Rightarrow>
|
||||
| X64_A.PageFlush typ start end pstart pd asid \<Rightarrow>
|
||||
pgi' = PageFlush (flush_type_map typ) start end pstart pd asid
|
||||
| ARM_A.PageGetAddr ptr \<Rightarrow>
|
||||
| X64_A.PageGetAddr ptr \<Rightarrow>
|
||||
pgi' = PageGetAddr ptr"
|
||||
|
||||
definition
|
||||
|
|
@ -1789,7 +1789,7 @@ proof -
|
|||
using assms
|
||||
apply -
|
||||
apply (clarsimp simp:valid_slots_duplicated'_def
|
||||
split:ARM_H.pte.splits)
|
||||
split:X64_H.pte.splits)
|
||||
apply (subgoal_tac "p \<le> p + mask 6")
|
||||
apply (clarsimp simp:upto_enum_step_def not_less)
|
||||
apply (intro conjI impI,simp)
|
||||
|
|
@ -1837,7 +1837,7 @@ proof -
|
|||
using assms
|
||||
apply -
|
||||
apply (clarsimp simp:valid_slots_duplicated'_def
|
||||
split:ARM_H.pde.splits)
|
||||
split:X64_H.pde.splits)
|
||||
apply (subgoal_tac "p \<le> p + mask 6")
|
||||
apply (clarsimp simp:upto_enum_step_def not_less)
|
||||
apply (intro conjI impI,simp)
|
||||
|
|
@ -1924,7 +1924,7 @@ lemma corres_store_pde_with_invalid_tail:
|
|||
"\<forall>slot \<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab)
|
||||
\<Longrightarrow>corres dc ((\<lambda>s. \<forall>y\<in> set ys. pde_at y s) and pspace_aligned and valid_etcbs)
|
||||
(pspace_aligned' and pspace_distinct')
|
||||
(mapM (swp store_pde ARM_A.pde.InvalidPDE) ys)
|
||||
(mapM (swp store_pde X64_A.pde.InvalidPDE) ys)
|
||||
(mapM (swp storePDE ab) ys)"
|
||||
apply (rule_tac S ="{(x,y). x = y \<and> x \<in> set ys}"
|
||||
in corres_mapM[where r = dc and r' = dc])
|
||||
|
|
@ -1947,7 +1947,7 @@ lemma corres_store_pte_with_invalid_tail:
|
|||
"\<forall>slot\<in> set ys. \<not> is_aligned (slot >> 2) (pte_align' aa)
|
||||
\<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs)
|
||||
(pspace_aligned' and pspace_distinct')
|
||||
(mapM (swp store_pte ARM_A.pte.InvalidPTE) ys)
|
||||
(mapM (swp store_pte X64_A.pte.InvalidPTE) ys)
|
||||
(mapM (swp storePTE aa) ys)"
|
||||
apply (rule_tac S ="{(x,y). x = y \<and> x \<in> set ys}"
|
||||
in corres_mapM[where r = dc and r' = dc])
|
||||
|
|
@ -2040,7 +2040,7 @@ definition
|
|||
(\<lambda>s. \<exists>pd. vspace_at_asid asid pd s)"
|
||||
|
||||
lemma set_cap_valid_page_map_inv:
|
||||
"\<lbrace>valid_page_inv (ARM_A.page_invocation.PageMap asid cap slot m)\<rbrace> set_cap cap slot \<lbrace>\<lambda>rv. valid_page_map_inv asid cap slot m\<rbrace>"
|
||||
"\<lbrace>valid_page_inv (X64_A.page_invocation.PageMap asid cap slot m)\<rbrace> set_cap cap slot \<lbrace>\<lambda>rv. valid_page_map_inv asid cap slot m\<rbrace>"
|
||||
apply (simp add: valid_page_inv_def valid_page_map_inv_def)
|
||||
apply (wp set_cap_cte_wp_at_cases hoare_vcg_ex_lift| simp)+
|
||||
apply clarsimp
|
||||
|
|
@ -2186,7 +2186,7 @@ proof -
|
|||
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. vspace_at_asid word pd s)" in hoare_strengthen_post)
|
||||
prefer 2
|
||||
apply auto[1]
|
||||
apply (wp mapM_swp_store_pte_invs[where pte="ARM_A.pte.InvalidPTE", simplified] hoare_vcg_ex_lift)
|
||||
apply (wp mapM_swp_store_pte_invs[where pte="X64_A.pte.InvalidPTE", simplified] hoare_vcg_ex_lift)
|
||||
apply (wp mapM_UNIV_wp | simp add: swp_def del: fun_upd_apply)+
|
||||
apply (clarsimp simp:pte_relation_aligned_def)
|
||||
apply (clarsimp dest!:valid_slots_duplicated_pteD')
|
||||
|
|
@ -2227,7 +2227,7 @@ proof -
|
|||
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. vspace_at_asid word pd s)" in hoare_strengthen_post)
|
||||
prefer 2
|
||||
apply auto[1]
|
||||
apply (wp mapM_swp_store_pde_invs_unmap[where pde="ARM_A.pde.InvalidPDE", simplified] hoare_vcg_ex_lift)
|
||||
apply (wp mapM_swp_store_pde_invs_unmap[where pde="X64_A.pde.InvalidPDE", simplified] hoare_vcg_ex_lift)
|
||||
apply (wp mapM_UNIV_wp store_pde_pd_at_asid | clarsimp simp add: swp_def)+
|
||||
apply (clarsimp simp: pde_relation_aligned_def)
|
||||
apply (clarsimp dest!:valid_slots_duplicated_pdeD')
|
||||
|
|
@ -2253,7 +2253,7 @@ proof -
|
|||
apply (clarsimp simp: cap_range_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
|
||||
apply (clarsimp split: Structures_A.kernel_object.split_asm if_split_asm ARM_A.arch_kernel_obj.splits)
|
||||
apply (clarsimp split: Structures_A.kernel_object.split_asm if_split_asm X64_A.arch_kernel_obj.splits)
|
||||
apply (rule conjI[rotated], fastforce)
|
||||
apply (erule ballEI)
|
||||
apply (clarsimp simp: pde_at_def obj_at_def
|
||||
|
|
@ -2297,7 +2297,7 @@ proof -
|
|||
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. vspace_at_asid word pd s)" in hoare_strengthen_post)
|
||||
prefer 2
|
||||
apply auto[1]
|
||||
apply (wp mapM_swp_store_pte_invs[where pte="ARM_A.pte.InvalidPTE", simplified] hoare_vcg_ex_lift)
|
||||
apply (wp mapM_swp_store_pte_invs[where pte="X64_A.pte.InvalidPTE", simplified] hoare_vcg_ex_lift)
|
||||
apply (wp mapM_UNIV_wp | simp add: swp_def del: fun_upd_apply)+
|
||||
apply (clarsimp simp:pte_relation_aligned_def valid_page_inv'_def)
|
||||
apply (clarsimp dest!:valid_slots_duplicated_pteD')
|
||||
|
|
@ -2338,7 +2338,7 @@ proof -
|
|||
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. vspace_at_asid word pd s)" in hoare_strengthen_post)
|
||||
prefer 2
|
||||
apply auto[1]
|
||||
apply (wp mapM_swp_store_pde_invs_unmap[where pde="ARM_A.pde.InvalidPDE", simplified] hoare_vcg_ex_lift)
|
||||
apply (wp mapM_swp_store_pde_invs_unmap[where pde="X64_A.pde.InvalidPDE", simplified] hoare_vcg_ex_lift)
|
||||
apply (wp mapM_UNIV_wp store_pde_pd_at_asid | clarsimp simp add: swp_def)+
|
||||
apply (clarsimp simp: pde_relation_aligned_def valid_page_inv'_def)
|
||||
apply (clarsimp dest!:valid_slots_duplicated_pdeD')
|
||||
|
|
@ -2465,11 +2465,11 @@ qed
|
|||
|
||||
definition
|
||||
"page_table_invocation_map pti pti' \<equiv> case pti of
|
||||
ARM_A.PageTableMap cap ptr pde p \<Rightarrow>
|
||||
X64_A.PageTableMap cap ptr pde p \<Rightarrow>
|
||||
\<exists>cap' pde'. pti' = PageTableMap cap' (cte_map ptr) pde' p \<and>
|
||||
cap_relation cap cap' \<and>
|
||||
pde_relation' pde pde' \<and> is_aligned (p >> 2) (pde_align' pde')
|
||||
| ARM_A.PageTableUnmap cap ptr \<Rightarrow>
|
||||
| X64_A.PageTableUnmap cap ptr \<Rightarrow>
|
||||
\<exists>cap'. pti' = PageTableUnmap cap' (cte_map ptr) \<and>
|
||||
cap_relation cap (ArchObjectCap cap')"
|
||||
|
||||
|
|
@ -2488,9 +2488,9 @@ definition
|
|||
lemma clear_page_table_corres:
|
||||
"corres dc (pspace_aligned and page_table_at p and valid_etcbs)
|
||||
(pspace_aligned' and pspace_distinct')
|
||||
(mapM_x (swp store_pte ARM_A.InvalidPTE)
|
||||
(mapM_x (swp store_pte X64_A.InvalidPTE)
|
||||
[p , p + 4 .e. p + 2 ^ ptBits - 1])
|
||||
(mapM_x (swp storePTE ARM_H.InvalidPTE)
|
||||
(mapM_x (swp storePTE X64_H.InvalidPTE)
|
||||
[p , p + 4 .e. p + 2 ^ ptBits - 1])"
|
||||
apply (rule_tac F="is_aligned p ptBits" in corres_req)
|
||||
apply (clarsimp simp: obj_at_def a_type_def)
|
||||
|
|
@ -2547,7 +2547,7 @@ lemma perform_page_table_corres:
|
|||
apply auto[1]
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of valid_pti'_def)
|
||||
apply auto[1]
|
||||
apply (clarsimp simp:valid_pde_mapping'_def split:ARM_H.pde.split)
|
||||
apply (clarsimp simp:valid_pde_mapping'_def split:X64_H.pde.split)
|
||||
apply (rename_tac cap a b)
|
||||
apply (clarsimp simp: page_table_invocation_map_def)
|
||||
apply (rule_tac F="is_pt_cap cap" in corres_req)
|
||||
|
|
@ -2616,7 +2616,7 @@ lemma pap_corres:
|
|||
apply (rename_tac word1 word2 prod)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split [OF _ getSlotCap_corres])
|
||||
apply (rule_tac F="\<exists>p asid. rv = Structures_A.ArchObjectCap (ARM_A.PageDirectoryCap p asid)" in corres_gen_asm)
|
||||
apply (rule_tac F="\<exists>p asid. rv = Structures_A.ArchObjectCap (X64_A.PageDirectoryCap p asid)" in corres_gen_asm)
|
||||
apply clarsimp
|
||||
apply (rule_tac Q="valid_objs and pspace_aligned and pspace_distinct and asid_pool_at word2 and valid_etcbs and
|
||||
cte_wp_at (\<lambda>c. cap_master_cap c =
|
||||
|
|
@ -2660,8 +2660,8 @@ crunch obj_at[wp]: setVMRoot "\<lambda>s. P (obj_at' P' t s)"
|
|||
|
||||
lemma storeHWASID_invs:
|
||||
"\<lbrace>invs' and
|
||||
(\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and>
|
||||
armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace>
|
||||
(\<lambda>s. x64KSASIDMap (ksArchState s) asid = None \<and>
|
||||
x64KSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace>
|
||||
storeHWASID asid hw_asid
|
||||
\<lbrace>\<lambda>x. invs'\<rbrace>"
|
||||
apply (rule hoare_add_post)
|
||||
|
|
@ -2676,8 +2676,8 @@ lemma storeHWASID_invs:
|
|||
|
||||
lemma storeHWASID_invs_no_cicd':
|
||||
"\<lbrace>invs_no_cicd' and
|
||||
(\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and>
|
||||
armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace>
|
||||
(\<lambda>s. x64KSASIDMap (ksArchState s) asid = None \<and>
|
||||
x64KSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace>
|
||||
storeHWASID asid hw_asid
|
||||
\<lbrace>\<lambda>x. invs_no_cicd'\<rbrace>"
|
||||
apply (rule hoare_add_post)
|
||||
|
|
@ -3754,7 +3754,7 @@ lemma diminished_valid':
|
|||
apply (rule ext)
|
||||
apply (simp add: maskCapRights_def Let_def split del: if_split)
|
||||
apply (cases cap'; simp add: isCap_simps valid_cap'_def capAligned_def split del: if_split)
|
||||
by (simp add: ARM_H.maskCapRights_def isPageCap_def Let_def split del: if_split split: arch_capability.splits)
|
||||
by (simp add: X64_H.maskCapRights_def isPageCap_def Let_def split del: if_split split: arch_capability.splits)
|
||||
|
||||
lemma diminished_isPDCap:
|
||||
"diminished' cap cap' \<Longrightarrow> isPDCap cap' = isPDCap cap"
|
||||
|
|
|
|||
Loading…
Reference in New Issue