arm-hyp refine: remove unused ADT_H lemma
This commit is contained in:
Gerwin Klein
Alejandro Gomez-Londono
parent
e9d3c3eb54
commit
bc40dc4a46
|
|
@ -142,154 +142,6 @@ definition
|
|||
vcpu_VGIC = absVGIC vgic,
|
||||
vcpu_regs = regs \<rparr>))"
|
||||
|
||||
(*
|
||||
lemma
|
||||
assumes ptes:
|
||||
"\<forall>x. (\<exists>pte. ksPSpace \<sigma> x = Some (KOArch (KOPTE pte))) \<longrightarrow>
|
||||
is_aligned x pt_bits \<longrightarrow>
|
||||
(\<forall>y::word8. \<exists>pte'. ksPSpace \<sigma> (x + (ucast y << pte_bits)) =
|
||||
Some (KOArch (KOPTE pte')))"
|
||||
and pte_rights:
|
||||
"\<forall>x. case ksPSpace \<sigma> x of
|
||||
Some (KOArch (KOPTE (ARM_HYP_H.LargePagePTE _ _ _ r))) \<Rightarrow>
|
||||
r \<noteq> VMNoAccess"
|
||||
"\<forall>x. case ksPSpace \<sigma> x of
|
||||
Some (KOArch (KOPTE (ARM_HYP_H.SmallPagePTE _ _ _ r))) \<Rightarrow>
|
||||
r \<noteq> VMNoAccess"
|
||||
|
||||
assumes pdes:
|
||||
"\<forall>x. (\<exists>pde. ksPSpace \<sigma> x = Some (KOArch (KOPDE pde))) \<longrightarrow>
|
||||
is_aligned x pd_bits \<longrightarrow>
|
||||
(\<forall>y::12 word. \<exists>pde'. ksPSpace \<sigma> (x + (ucast y << pde_bits)) =
|
||||
Some (KOArch (KOPDE pde')))"
|
||||
and pde_rights:
|
||||
"\<forall>x. case ksPSpace \<sigma> x of
|
||||
Some (KOArch (KOPDE (ARM_HYP_H.SectionPDE _ _ _ r))) \<Rightarrow>
|
||||
r \<noteq> VMNoAccess"
|
||||
"\<forall>x. case ksPSpace \<sigma> x of
|
||||
Some (KOArch (KOPDE (ARM_HYP_H.SuperSectionPDE _ _ _ r))) \<Rightarrow>
|
||||
r \<noteq> VMNoAccess"
|
||||
|
||||
assumes fst_pte:
|
||||
"\<forall>x. (\<exists>pte. ksPSpace \<sigma> x = Some (KOArch (KOPTE pte))) \<longrightarrow>
|
||||
(\<exists>pte'. ksPSpace \<sigma> (x && ~~ mask pt_bits) =
|
||||
Some (KOArch (KOPTE pte')))"
|
||||
assumes fst_pde:
|
||||
"\<forall>x. (\<exists>pde. ksPSpace \<sigma> x = Some (KOArch (KOPDE pde))) \<longrightarrow>
|
||||
(\<exists>pde'. ksPSpace \<sigma> (x && ~~ mask pd_bits) =
|
||||
Some (KOArch (KOPDE pde')))"
|
||||
assumes pspace_aligned': "pspace_aligned' \<sigma>"
|
||||
|
||||
shows
|
||||
"pspace_relation
|
||||
(%x. case ksPSpace \<sigma> x of
|
||||
Some (KOArch ako) \<Rightarrow>
|
||||
map_option ArchObj (absHeapArch (ksPSpace \<sigma>) x ako)
|
||||
| _ \<Rightarrow> None)
|
||||
(%x. case ksPSpace \<sigma> x of Some (KOArch _) \<Rightarrow> ksPSpace \<sigma> x | _ \<Rightarrow> None)"
|
||||
apply (clarsimp simp add: pspace_relation_def dom_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp add: pspace_dom_def dom_def UNION_eq)
|
||||
apply (rule Collect_cong)
|
||||
apply (rule iffI)
|
||||
apply (erule exE)
|
||||
apply (case_tac "ksPSpace \<sigma> x", simp+)
|
||||
apply (clarsimp split: option.splits Structures_H.kernel_object.splits)
|
||||
apply (rename_tac arch_kernel_object aa b z)
|
||||
apply (simp add: absHeapArch_def)
|
||||
apply (case_tac arch_kernel_object)
|
||||
apply (clarsimp split: asidpool.splits)
|
||||
apply (clarsimp split: if_split_asm)
|
||||
using ptes
|
||||
apply (erule_tac x=x in allE)
|
||||
apply simp
|
||||
apply (erule_tac x=y in allE)
|
||||
apply clarsimp
|
||||
apply (clarsimp split: if_split_asm)
|
||||
using pdes
|
||||
apply (erule_tac x=x in allE)
|
||||
apply simp
|
||||
apply (erule_tac x=y in allE)
|
||||
apply clarsimp
|
||||
apply (clarsimp split: option.splits Structures_H.kernel_object.splits)
|
||||
apply (clarsimp simp add: absHeapArch_def)
|
||||
apply (rename_tac arch_kernel_object)
|
||||
apply (case_tac arch_kernel_object)
|
||||
apply (rule_tac x=y in exI)
|
||||
apply (clarsimp split: asidpool.splits)
|
||||
using fst_pte
|
||||
apply (erule_tac x=y in allE)
|
||||
apply (clarsimp split: if_split_asm)
|
||||
apply (rule_tac x="(y && ~~ mask pt_bits)" in exI, simp)
|
||||
apply (simp add: is_aligned_mask mask_AND_NOT_mask)
|
||||
apply (simp add: range_composition[symmetric])
|
||||
apply (rule_tac x="ucast (y >> 2)" in range_eqI)
|
||||
apply (simp add: pt_bits_def pageBits_def)
|
||||
apply (simp add: word_size ucast_ucast_mask and_mask_shiftl_comm)
|
||||
using pspace_aligned'
|
||||
apply (simp add: pspace_aligned'_def dom_def)
|
||||
apply (erule_tac x=y in allE)
|
||||
apply (simp add: objBitsKO_def archObjSize_def is_aligned_neg_mask_eq
|
||||
and_not_mask[symmetric] AND_NOT_mask_plus_AND_mask_eq)
|
||||
using fst_pde
|
||||
apply (erule_tac x=y in allE)
|
||||
apply clarsimp
|
||||
apply (rule_tac x="(y && ~~ mask pd_bits)" in exI, simp)
|
||||
apply (simp add: is_aligned_mask mask_AND_NOT_mask)
|
||||
apply (simp add: range_composition[symmetric])
|
||||
apply (rule_tac x="ucast (y >> 2)" in range_eqI)
|
||||
apply (simp add: pd_bits_def pageBits_def)
|
||||
apply (simp add: word_size ucast_ucast_mask and_mask_shiftl_comm)
|
||||
using pspace_aligned'
|
||||
apply (simp add: pspace_aligned'_def dom_def)
|
||||
apply (erule_tac x=y in allE)
|
||||
apply (simp add: objBitsKO_def archObjSize_def is_aligned_neg_mask_eq
|
||||
and_not_mask[symmetric] AND_NOT_mask_plus_AND_mask_eq)
|
||||
apply (simp split: option.splits Structures_H.kernel_object.splits)
|
||||
apply (intro allI)
|
||||
apply (intro impI)
|
||||
apply (elim exE)
|
||||
apply (clarsimp split: option.splits Structures_H.kernel_object.splits)
|
||||
apply (simp add: absHeapArch_def)
|
||||
apply (rename_tac arch_kernel_object z a b)
|
||||
apply (case_tac arch_kernel_object)
|
||||
apply (clarsimp split: asidpool.splits)
|
||||
apply (simp add: other_obj_relation_def asid_pool_relation_def o_def inv_def)
|
||||
apply simp
|
||||
apply (clarsimp simp: pte_relation_def pte_relation_aligned_def
|
||||
split: if_split_asm)
|
||||
using ptes
|
||||
apply (erule_tac x=x in allE)
|
||||
apply simp
|
||||
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_HYP_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)
|
||||
using pte_rights
|
||||
apply -[1]
|
||||
apply (erule_tac x="x + (ucast y << 2)" in allE)+
|
||||
subgoal by fastforce
|
||||
apply (clarsimp split: if_split_asm)
|
||||
using pdes
|
||||
apply (erule_tac x=x in allE)
|
||||
apply simp
|
||||
apply (erule_tac x=y in allE)
|
||||
apply clarsimp
|
||||
apply (simp add: pde_relation_def pde_relation_aligned_def)
|
||||
apply (simp add: absPageDirectory_def
|
||||
split: option.splits ARM_HYP_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)
|
||||
using pde_rights
|
||||
apply -[1]
|
||||
apply (erule_tac x="x + (ucast y << 2)" in allE)+
|
||||
apply fastforce
|
||||
done*)
|
||||
|
||||
definition
|
||||
"EndpointMap ep \<equiv> case ep of
|
||||
Structures_H.IdleEP \<Rightarrow> Structures_A.IdleEP
|
||||
|
|
|
|||
Loading…
Reference in New Issue