x64: get StateRelation, Invariants_H building
This will now allow sorrying of proofs in refine to aid parallelism as we proceed. Note: the invariants are in no way complete and the aim should be to update them as required - allowing people to start working on refine proofs without the high initial cost of fixing/writing all of the invariants.
This commit is contained in:
Joel Beeren
parent
903b2ae87a
commit
e4c5679050
|
|
@ -39,17 +39,6 @@ crunch_ignore (add:
|
|||
unify_failure throw_on_false
|
||||
)
|
||||
|
||||
context Arch begin (*FIXME: arch_split*)
|
||||
|
||||
crunch_ignore (add:
|
||||
invalidateTLB_ASID invalidateTLB_VAASID
|
||||
cleanByVA cleanByVA_PoU invalidateByVA invalidateByVA_I invalidate_I_PoU
|
||||
cleanInvalByVA branchFlush clean_D_PoU cleanInvalidate_D_PoC cleanInvalidateL2Range
|
||||
invalidateL2Range cleanL2Range flushBTAC writeContextID isb dsb dmb
|
||||
setHardwareASID setCurrentPD)
|
||||
|
||||
end
|
||||
|
||||
crunch_ignore (add:
|
||||
storeWordVM loadWord setRegister getRegister getRestartPC
|
||||
debugPrint set_register get_register
|
||||
|
|
@ -92,12 +81,15 @@ lemma isCap_simps:
|
|||
"isIRQHandlerCap v = (\<exists>v0. v = IRQHandlerCap v0)"
|
||||
"isNullCap v = (v = NullCap)"
|
||||
"isDomainCap v = (v = DomainCap)"
|
||||
"isPageCap w = (\<exists>d v0 v1 v2 v3. w = PageCap d v0 v1 v2 v3)"
|
||||
"isPageCap w = (\<exists>d v0 v1 v2 v3 v4. w = PageCap v0 v1 v2 v3 d v4)"
|
||||
"isPageTableCap w = (\<exists>v0 v1. w = PageTableCap v0 v1)"
|
||||
"isPageDirectoryCap w = (\<exists>v0 v1. w = PageDirectoryCap v0 v1)"
|
||||
"isPDPointerTableCap w = (\<exists>v0 v1. w = PDPointerTableCap v0 v1)"
|
||||
"isPML4Cap w = (\<exists>v0 v1. w = PML4Cap v0 v1)"
|
||||
"isIOPortCap w = (\<exists>v0 v1. w = IOPortCap v0 v1)"
|
||||
"isASIDControlCap w = (w = ASIDControlCap)"
|
||||
"isASIDPoolCap w = (\<exists>v0 v1. w = ASIDPoolCap v0 v1)"
|
||||
"isArchPageCap cap = (\<exists>d ref rghts sz data. cap = ArchObjectCap (PageCap d ref rghts sz data))"
|
||||
"isArchPageCap cap = (\<exists>d ref rghts sz data typ. cap = ArchObjectCap (PageCap ref rghts typ sz d data))"
|
||||
by (auto simp: isCap_defs split: capability.splits arch_capability.splits)
|
||||
|
||||
lemma untyped_not_null [simp]:
|
||||
|
|
@ -385,7 +377,7 @@ lemma ko_at_cte_ctable:
|
|||
|
||||
lemma ko_at_cte_vtable:
|
||||
fixes ko :: tcb
|
||||
shows "\<lbrakk> ko_at' tcb p s \<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbVTable tcb) (p + 16) s"
|
||||
shows "\<lbrakk> ko_at' tcb p s \<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbVTable tcb) (p + 32) s"
|
||||
apply (clarsimp simp: obj_at'_def objBits_simps projectKOs)
|
||||
apply (erule(2) cte_wp_at_tcbI')
|
||||
apply fastforce
|
||||
|
|
@ -503,7 +495,7 @@ lemma withoutPreemption_R:
|
|||
by (wp withoutPreemption_lift)
|
||||
|
||||
lemma ko_at_cte_ipcbuffer:
|
||||
"ko_at' tcb p s \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbIPCBufferFrame tcb) (p + tcbIPCBufferSlot * 0x10) s"
|
||||
"ko_at' tcb p s \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbIPCBufferFrame tcb) (p + tcbIPCBufferSlot * 0x20) s"
|
||||
apply (clarsimp simp: obj_at'_def projectKOs objBits_simps)
|
||||
apply (erule (2) cte_wp_at_tcbI')
|
||||
apply (fastforce simp add: tcb_cte_cases_def tcbIPCBufferSlot_def)
|
||||
|
|
|
|||
|
|
@ -81,6 +81,10 @@ abbreviation
|
|||
"pde_at' \<equiv> typ_at' (ArchT PDET)"
|
||||
abbreviation
|
||||
"pte_at' \<equiv> typ_at' (ArchT PTET)"
|
||||
abbreviation
|
||||
"pdpte_at' \<equiv> typ_at' (ArchT PDPTET)"
|
||||
abbreviation
|
||||
"pml4e_at' \<equiv> typ_at' (ArchT PML4ET)"
|
||||
end
|
||||
|
||||
record itcb' =
|
||||
|
|
@ -151,10 +155,10 @@ definition
|
|||
tcb_cte_cases :: "machine_word \<rightharpoonup> ((tcb \<Rightarrow> cte) \<times> ((cte \<Rightarrow> cte) \<Rightarrow> tcb \<Rightarrow> tcb))"
|
||||
where
|
||||
"tcb_cte_cases \<equiv> [ 0 \<mapsto> (tcbCTable, tcbCTable_update),
|
||||
16 \<mapsto> (tcbVTable, tcbVTable_update),
|
||||
32 \<mapsto> (tcbReply, tcbReply_update),
|
||||
48 \<mapsto> (tcbCaller, tcbCaller_update),
|
||||
64 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update) ]"
|
||||
32 \<mapsto> (tcbVTable, tcbVTable_update),
|
||||
64 \<mapsto> (tcbReply, tcbReply_update),
|
||||
96 \<mapsto> (tcbCaller, tcbCaller_update),
|
||||
128 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update) ]"
|
||||
|
||||
definition
|
||||
max_ipc_words :: machine_word
|
||||
|
|
@ -1007,22 +1011,19 @@ where
|
|||
"valid_refs' R \<equiv> \<lambda>m. \<forall>c \<in> ran m. R \<inter> capRange (cteCap c) = {}"
|
||||
|
||||
definition
|
||||
page_directory_refs' :: "machine_word \<Rightarrow> machine_word set"
|
||||
table_refs' :: "machine_word \<Rightarrow> machine_word set"
|
||||
where
|
||||
"page_directory_refs' x \<equiv> (\<lambda>y. x + (y << 2)) ` {y. y < 2 ^ 12}"
|
||||
|
||||
definition
|
||||
page_table_refs' :: "machine_word \<Rightarrow> machine_word set"
|
||||
where
|
||||
"page_table_refs' x \<equiv> (\<lambda>y. x + (y << 2)) ` {y. y < 2 ^ 8}"
|
||||
"table_refs' x \<equiv> (\<lambda>y. x + (y << word_size_bits)) ` {y. y < 2^ptTranslationBits}"
|
||||
|
||||
definition
|
||||
global_refs' :: "kernel_state \<Rightarrow> obj_ref set"
|
||||
where
|
||||
"global_refs' \<equiv> \<lambda>s.
|
||||
{ksIdleThread s} \<union>
|
||||
page_directory_refs' (armKSGlobalPD (ksArchState s)) \<union>
|
||||
(\<Union>pt \<in> set (armKSGlobalPTs (ksArchState s)). page_table_refs' pt) \<union>
|
||||
table_refs' (x64KSGlobalPML4 (ksArchState s)) \<union>
|
||||
(\<Union>pt \<in> set (x64KSGlobalPDs (ksArchState s)). table_refs' pt) \<union>
|
||||
(\<Union>pt \<in> set (x64KSGlobalPTs (ksArchState s)). table_refs' pt) \<union>
|
||||
(\<Union>pt \<in> set (x64KSGlobalPDPTs (ksArchState s)). table_refs' pt) \<union>
|
||||
range (\<lambda>irq :: irq. irq_node' s + 16 * ucast irq)"
|
||||
|
||||
definition
|
||||
|
|
@ -1055,21 +1056,31 @@ where
|
|||
"valid_global_pts' pts \<equiv> \<lambda>s. \<forall>p \<in> set pts. page_table_at' p s"
|
||||
|
||||
definition
|
||||
valid_asid_map' :: "(machine_word \<rightharpoonup> word8 \<times> machine_word) \<Rightarrow> bool"
|
||||
valid_global_pds' :: "machine_word list \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
where
|
||||
"valid_asid_map' m \<equiv> inj_on (option_map snd o m) (dom m)
|
||||
"valid_global_pds' pds \<equiv> \<lambda>s. \<forall>p \<in> set pds. page_directory_at' p s"
|
||||
|
||||
definition
|
||||
valid_global_pdpts' :: "machine_word list \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
where
|
||||
"valid_global_pdpts' pdpts \<equiv> \<lambda>s. \<forall>p \<in> set pdpts. pd_pointer_table_at' p s"
|
||||
|
||||
definition
|
||||
valid_asid_map' :: "(asid \<rightharpoonup> machine_word) \<Rightarrow> bool"
|
||||
where
|
||||
"valid_asid_map' m \<equiv> inj_on m (dom m)
|
||||
\<and> dom m \<subseteq> ({0 .. mask asid_bits} - {0})"
|
||||
|
||||
definition
|
||||
valid_arch_state' :: "kernel_state \<Rightarrow> bool"
|
||||
where
|
||||
"valid_arch_state' \<equiv> \<lambda>s.
|
||||
valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and>
|
||||
page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and>
|
||||
valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and>
|
||||
is_inv (armKSHWASIDTable (ksArchState s))
|
||||
(option_map fst o armKSASIDMap (ksArchState s)) \<and>
|
||||
valid_asid_map' (armKSASIDMap (ksArchState s))"
|
||||
valid_asid_table' (x64KSASIDTable (ksArchState s)) s \<and>
|
||||
page_directory_at' (x64KSGlobalPML4 (ksArchState s)) s \<and>
|
||||
valid_global_pds' (x64KSGlobalPDs (ksArchState s)) s \<and>
|
||||
valid_global_pdpts' (x64KSGlobalPDPTs (ksArchState s)) s \<and>
|
||||
valid_global_pts' (x64KSGlobalPTs (ksArchState s)) s \<and>
|
||||
valid_asid_map' (x64KSASIDMap (ksArchState s))"
|
||||
|
||||
definition
|
||||
irq_issued' :: "irq \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
|
|
@ -1204,6 +1215,8 @@ definition
|
|||
| ArchT atp \<Rightarrow> (case atp of
|
||||
PDET \<Rightarrow> injectKO (makeObject :: pde)
|
||||
| PTET \<Rightarrow> injectKO (makeObject :: pte)
|
||||
| PDPTET \<Rightarrow> injectKO (makeObject :: pdpte)
|
||||
| PML4ET \<Rightarrow> injectKO (makeObject :: pml4e)
|
||||
| ASIDPoolT \<Rightarrow> injectKO (makeObject :: asidpool))"
|
||||
|
||||
definition
|
||||
|
|
@ -1495,15 +1508,6 @@ lemmas objBitsKO_simps = objBits_simps
|
|||
|
||||
lemmas wordRadix_def' = wordRadix_def[simplified]
|
||||
|
||||
lemma valid_duplicates'_D:
|
||||
"\<lbrakk>vs_valid_duplicates' m; m (p::machine_word) = Some ko;is_aligned p' 2;
|
||||
p && ~~ mask (vs_ptr_align ko) = p' && ~~ mask (vs_ptr_align ko)\<rbrakk>
|
||||
\<Longrightarrow> m p' = Some ko "
|
||||
apply (clarsimp simp:vs_valid_duplicates'_def)
|
||||
apply (drule_tac x = p in spec)
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma ps_clear_def2:
|
||||
"p \<le> p + 1 \<Longrightarrow> ps_clear p n s = ({p + 1 .. p + (1 << n) - 1} \<inter> dom (ksPSpace s) = {})"
|
||||
apply (simp add: ps_clear_def)
|
||||
|
|
@ -1532,7 +1536,7 @@ lemma singleton_in_magnitude_check:
|
|||
by (simp add: magnitudeCheck_def when_def in_monad return_def
|
||||
split: if_split_asm option.split_asm)
|
||||
|
||||
lemma wordSizeCase_simp [simp]: "wordSizeCase a b = a"
|
||||
lemma wordSizeCase_simp [simp]: "wordSizeCase a b = b"
|
||||
by (simp add: wordSizeCase_def wordBits_def word_size)
|
||||
|
||||
lemma projectKO_eq:
|
||||
|
|
@ -1596,10 +1600,10 @@ lemma cte_at'_def:
|
|||
|
||||
lemma tcb_cte_cases_simps[simp]:
|
||||
"tcb_cte_cases 0 = Some (tcbCTable, tcbCTable_update)"
|
||||
"tcb_cte_cases 16 = Some (tcbVTable, tcbVTable_update)"
|
||||
"tcb_cte_cases 32 = Some (tcbReply, tcbReply_update)"
|
||||
"tcb_cte_cases 48 = Some (tcbCaller, tcbCaller_update)"
|
||||
"tcb_cte_cases 64 = Some (tcbIPCBufferFrame, tcbIPCBufferFrame_update)"
|
||||
"tcb_cte_cases 32 = Some (tcbVTable, tcbVTable_update)"
|
||||
"tcb_cte_cases 64 = Some (tcbReply, tcbReply_update)"
|
||||
"tcb_cte_cases 96 = Some (tcbCaller, tcbCaller_update)"
|
||||
"tcb_cte_cases 128 = Some (tcbIPCBufferFrame, tcbIPCBufferFrame_update)"
|
||||
by (simp add: tcb_cte_cases_def)+
|
||||
|
||||
lemma refs_of'_simps[simp]:
|
||||
|
|
@ -1867,6 +1871,7 @@ lemma
|
|||
| IRQHandlerCap irq \<Rightarrow> False
|
||||
| ReplyCap r m \<Rightarrow> False
|
||||
| ArchObjectCap ASIDControlCap \<Rightarrow> False
|
||||
| ArchObjectCap (IOPortCap _ _) \<Rightarrow> False
|
||||
| _ \<Rightarrow> True)"
|
||||
by (simp split: capability.splits arch_capability.splits zombie_type.splits)
|
||||
|
||||
|
|
@ -1875,16 +1880,14 @@ lemma sch_act_sane_not:
|
|||
by (auto simp: sch_act_sane_def)
|
||||
|
||||
lemma objBits_cte_conv:
|
||||
"objBits (cte :: cte) = 4"
|
||||
"objBits (cte :: cte) = 5"
|
||||
by (simp add: objBits_def objBitsKO_def wordSizeCase_def word_size)
|
||||
|
||||
lemma valid_pde_mapping'_simps[simp]:
|
||||
"valid_pde_mapping' offset (InvalidPDE) = True"
|
||||
"valid_pde_mapping' offset (SectionPDE ptr a b c d e w)
|
||||
"valid_pde_mapping' offset (LargePagePDE ptr a b c d e w x y)
|
||||
= valid_pde_mapping_offset' offset"
|
||||
"valid_pde_mapping' offset (SuperSectionPDE ptr a' b' c' d' w)
|
||||
= valid_pde_mapping_offset' offset"
|
||||
"valid_pde_mapping' offset (PageTablePDE ptr x z'')
|
||||
"valid_pde_mapping' offset (PageTablePDE ptr x z'' g h f)
|
||||
= valid_pde_mapping_offset' offset"
|
||||
by (clarsimp simp: valid_pde_mapping'_def)+
|
||||
|
||||
|
|
@ -1976,7 +1979,7 @@ lemma valid_cap'_pspaceI:
|
|||
(force intro: obj_at'_pspaceI[rotated]
|
||||
cte_wp_at'_pspaceI valid_untyped'_pspaceI
|
||||
typ_at'_pspaceI[rotated]
|
||||
simp: page_table_at'_def page_directory_at'_def
|
||||
simp: page_table_at'_def page_directory_at'_def pd_pointer_table_at'_def page_map_l4_at'_def
|
||||
split: arch_capability.split zombie_type.split option.splits)+
|
||||
|
||||
lemma valid_arch_obj'_pspaceI:
|
||||
|
|
@ -1991,6 +1994,10 @@ lemma valid_arch_obj'_pspaceI:
|
|||
apply (case_tac pde;
|
||||
auto simp: page_table_at'_def valid_mapping'_def
|
||||
intro: typ_at'_pspaceI[rotated])
|
||||
apply (rename_tac pdpte)
|
||||
apply (case_tac pdpte; auto simp: valid_mapping'_def)
|
||||
apply (rename_tac pml4e)
|
||||
apply (case_tac pml4e; auto simp: valid_mapping'_def)
|
||||
done
|
||||
|
||||
lemma valid_obj'_pspaceI:
|
||||
|
|
@ -2363,7 +2370,7 @@ lemma tcb_ctes_clear:
|
|||
lemma cte_wp_at_cases':
|
||||
shows "cte_wp_at' P p s =
|
||||
((\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits
|
||||
\<and> P cte \<and> ps_clear p 4 s) \<or>
|
||||
\<and> P cte \<and> ps_clear p 5 s) \<or>
|
||||
(\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9
|
||||
\<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s))"
|
||||
(is "?LHS = ?RHS")
|
||||
|
|
@ -2389,7 +2396,8 @@ lemma cte_wp_at_cases':
|
|||
erule rsubst[where P="\<lambda>x. ksPSpace s x = v" for s v],
|
||||
fastforce simp add: field_simps, simp)+
|
||||
apply (subst(asm) in_magnitude_check3, simp+)
|
||||
apply (simp split: if_split_asm)
|
||||
apply (simp split: if_split_asm
|
||||
add: )
|
||||
apply (simp add: cte_wp_at'_def getObject_def split_def
|
||||
bind_def simpler_gets_def return_def
|
||||
assert_opt_def fail_def
|
||||
|
|
@ -2451,8 +2459,7 @@ lemma cte_wp_atE' [consumes 1, case_names CTE TCB]:
|
|||
\<lbrakk> ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' 9 s; is_aligned ptr' 9;
|
||||
tcb_cte_cases (ptr - ptr') = Some (getF, setF); P (getF tcb) \<rbrakk> \<Longrightarrow> R"
|
||||
shows "R"
|
||||
by (rule disjE [OF iffD1 [OF cte_wp_at_cases' cte]])
|
||||
(auto intro: r1 r2 simp: cte_level_bits_def)
|
||||
by (rule disjE [OF iffD1 [OF cte_wp_at_cases' cte]]) (auto intro: r1 r2 simp: cte_level_bits_def)
|
||||
|
||||
lemma cte_wp_at_cteI':
|
||||
assumes "ksPSpace s ptr = Some (KOCTE cte)"
|
||||
|
|
@ -2618,6 +2625,18 @@ lemma typ_at_lift_page_table_at':
|
|||
unfolding page_table_at'_def All_less_Ball
|
||||
by (wp hoare_vcg_const_Ball_lift x)
|
||||
|
||||
lemma typ_at_lift_pd_pointer_table_at':
|
||||
assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
|
||||
shows "\<lbrace>pd_pointer_table_at' p\<rbrace> f \<lbrace>\<lambda>rv. pd_pointer_table_at' p\<rbrace>"
|
||||
unfolding pd_pointer_table_at'_def All_less_Ball
|
||||
by (wp hoare_vcg_const_Ball_lift x)
|
||||
|
||||
lemma typ_at_lift_page_map_l4_at':
|
||||
assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
|
||||
shows "\<lbrace>page_map_l4_at' p\<rbrace> f \<lbrace>\<lambda>rv. page_map_l4_at' p\<rbrace>"
|
||||
unfolding page_map_l4_at'_def All_less_Ball
|
||||
by (wp hoare_vcg_const_Ball_lift x)
|
||||
|
||||
lemma ko_wp_typ_at':
|
||||
"ko_wp_at' P p s \<Longrightarrow> \<exists>T. typ_at' T p s"
|
||||
by (clarsimp simp: typ_at'_def ko_wp_at'_def)
|
||||
|
|
@ -2637,7 +2656,7 @@ lemma typ_at_lift_valid_untyped':
|
|||
apply (clarsimp simp: valid_def split del:if_split)
|
||||
apply (frule ko_wp_typ_at')
|
||||
apply clarsimp
|
||||
apply (cut_tac T=T and p=ptr' in P)
|
||||
apply (cut_tac T1=T and p1=ptr' in P)
|
||||
apply (simp add: valid_def)
|
||||
apply (erule_tac x=s in allE)
|
||||
apply (erule impE)
|
||||
|
|
@ -2666,7 +2685,7 @@ lemma typ_at_lift_valid_cap':
|
|||
apply (simp add: valid_cap'_def)
|
||||
apply wp
|
||||
apply (case_tac cap;
|
||||
simp add: valid_cap'_def P [where P=id, simplified] typ_at_lift_tcb'
|
||||
simp add: valid_cap'_def P[where P1=id, simplified] typ_at_lift_tcb'
|
||||
hoare_vcg_prop typ_at_lift_ep'
|
||||
typ_at_lift_ntfn' typ_at_lift_cte_at'
|
||||
hoare_vcg_conj_lift [OF typ_at_lift_cte_at'])
|
||||
|
|
@ -2675,8 +2694,9 @@ lemma typ_at_lift_valid_cap':
|
|||
apply (wp typ_at_lift_tcb' P hoare_vcg_all_lift typ_at_lift_cte')+
|
||||
apply (rename_tac arch_capability)
|
||||
apply (case_tac arch_capability,
|
||||
simp_all add: P [where P=id, simplified] page_table_at'_def
|
||||
hoare_vcg_prop page_directory_at'_def All_less_Ball
|
||||
simp_all add: P [where P1=id, simplified] page_table_at'_def
|
||||
hoare_vcg_prop page_directory_at'_def pd_pointer_table_at'_def
|
||||
All_less_Ball page_map_l4_at'_def
|
||||
split del: if_splits)
|
||||
apply (wp hoare_vcg_const_Ball_lift P typ_at_lift_valid_untyped'
|
||||
hoare_vcg_all_lift typ_at_lift_cte')+
|
||||
|
|
@ -2700,6 +2720,16 @@ lemma valid_pte_lift':
|
|||
shows "\<lbrace>\<lambda>s. valid_pte' pte s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pte' pte s\<rbrace>"
|
||||
by (cases pte) (simp add: valid_mapping'_def|wp x typ_at_lift_page_directory_at')+
|
||||
|
||||
lemma valid_pdpte_lift':
|
||||
assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
|
||||
shows "\<lbrace>\<lambda>s. valid_pdpte' pdpte s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pdpte' pdpte s\<rbrace>"
|
||||
by (cases pdpte) (simp add: valid_mapping'_def|wp x typ_at_lift_pd_pointer_table_at')+
|
||||
|
||||
lemma valid_pml4e_lift':
|
||||
assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
|
||||
shows "\<lbrace>\<lambda>s. valid_pml4e' pml4e s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pml4e' pml4e s\<rbrace>"
|
||||
by (cases pml4e) (simp add: valid_mapping'_def|wp x typ_at_lift_page_map_l4_at')+
|
||||
|
||||
lemma valid_asid_pool_lift':
|
||||
assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
|
||||
shows "\<lbrace>\<lambda>s. valid_asid_pool' ap s\<rbrace> f \<lbrace>\<lambda>rv s. valid_asid_pool' ap s\<rbrace>"
|
||||
|
|
@ -2715,6 +2745,8 @@ lemmas typ_at_lifts = typ_at_lift_tcb' typ_at_lift_ep'
|
|||
typ_at_lift_cte_at'
|
||||
typ_at_lift_page_table_at'
|
||||
typ_at_lift_page_directory_at'
|
||||
typ_at_lift_page_map_l4_at'
|
||||
typ_at_lift_pd_pointer_table_at'
|
||||
typ_at_lift_asid_at'
|
||||
typ_at_lift_valid_untyped'
|
||||
typ_at_lift_valid_cap'
|
||||
|
|
@ -2972,10 +3004,26 @@ lemma page_directory_at_update' [iff]:
|
|||
"page_directory_at' p (f s) = page_directory_at' p s"
|
||||
by (simp add: page_directory_at'_def)
|
||||
|
||||
lemma pd_pointer_table_at_update' [iff]:
|
||||
"pd_pointer_table_at' p (f s) = pd_pointer_table_at' p s"
|
||||
by (simp add: pd_pointer_table_at'_def)
|
||||
|
||||
lemma page_map_l4_at_update' [iff]:
|
||||
"page_map_l4_at' p (f s) = page_map_l4_at' p s"
|
||||
by (simp add: page_map_l4_at'_def)
|
||||
|
||||
lemma valid_global_pts_update' [iff]:
|
||||
"valid_global_pts' pts (f s) = valid_global_pts' pts s"
|
||||
by (simp add: valid_global_pts'_def)
|
||||
|
||||
lemma valid_global_pds_update' [iff]:
|
||||
"valid_global_pds' pds (f s) = valid_global_pds' pds s"
|
||||
by (simp add: valid_global_pds'_def)
|
||||
|
||||
lemma valid_global_pdpts_update' [iff]:
|
||||
"valid_global_pdpts' pdpts (f s) = valid_global_pdpts' pdpts s"
|
||||
by (simp add: valid_global_pdpts'_def)
|
||||
|
||||
lemma no_0_obj'_update [iff]:
|
||||
"no_0_obj' (f s) = no_0_obj' s"
|
||||
by (simp add: no_0_obj'_def pspace)
|
||||
|
|
@ -3192,13 +3240,17 @@ lemma ex_cte_cap_to'_pres:
|
|||
done
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
lemma page_directory_pde_atI':
|
||||
"\<lbrakk> page_directory_at' p s; x < 2 ^ pageBits \<rbrakk> \<Longrightarrow> pde_at' (p + (x << 2)) s"
|
||||
"\<lbrakk> page_directory_at' p s; x < 2 ^ ptTranslationBits \<rbrakk> \<Longrightarrow> pde_at' (p + (x << word_size_bits)) s"
|
||||
by (simp add: page_directory_at'_def pageBits_def)
|
||||
|
||||
lemma page_table_pte_atI':
|
||||
"\<lbrakk> page_table_at' p s; x < 2^(ptBits - 2) \<rbrakk> \<Longrightarrow> pte_at' (p + (x << 2)) s"
|
||||
"\<lbrakk> page_table_at' p s; x < 2^ptTranslationBits \<rbrakk> \<Longrightarrow> pte_at' (p + (x << word_size_bits)) s"
|
||||
by (simp add: page_table_at'_def pageBits_def ptBits_def)
|
||||
|
||||
lemma pd_pointer_table_pdpte_atI':
|
||||
"\<lbrakk> pd_pointer_table_at' p s; x < 2^ptTranslationBits \<rbrakk> \<Longrightarrow> pdpte_at' (p + (x << word_size_bits)) s"
|
||||
by (simp add: pd_pointer_table_at'_def pageBits_def)
|
||||
|
||||
lemma valid_global_refsD':
|
||||
"\<lbrakk> ctes_of s p = Some cte; valid_global_refs' s \<rbrakk> \<Longrightarrow>
|
||||
kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs"
|
||||
|
|
@ -3369,24 +3421,27 @@ lemma vms_sch_act_update'[iff]:
|
|||
by (simp add: valid_machine_state'_def )
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
lemma objBitsT_simps:
|
||||
"objBitsT EndpointT = 4"
|
||||
"objBitsT NotificationT = 4"
|
||||
"objBitsT CTET = 4"
|
||||
"objBitsT EndpointT = 5"
|
||||
"objBitsT NotificationT = 5"
|
||||
"objBitsT CTET = 5"
|
||||
"objBitsT TCBT = 9"
|
||||
"objBitsT UserDataT = pageBits"
|
||||
"objBitsT UserDataDeviceT = pageBits"
|
||||
"objBitsT KernelDataT = pageBits"
|
||||
"objBitsT (ArchT PDET) = 2"
|
||||
"objBitsT (ArchT PTET) = 2"
|
||||
"objBitsT (ArchT PDET) = word_size_bits"
|
||||
"objBitsT (ArchT PTET) = word_size_bits"
|
||||
"objBitsT (ArchT PDPTET) = word_size_bits"
|
||||
"objBitsT (ArchT PML4ET) = word_size_bits"
|
||||
"objBitsT (ArchT ASIDPoolT) = pageBits"
|
||||
unfolding objBitsT_def makeObjectT_def
|
||||
by (simp_all add: makeObject_simps objBits_simps archObjSize_def)
|
||||
by (simp add: makeObject_simps objBits_simps archObjSize_def bit_simps)+
|
||||
|
||||
|
||||
lemma objBitsT_koTypeOf :
|
||||
"(objBitsT (koTypeOf ko)) = objBitsKO ko"
|
||||
apply (cases ko; simp add: objBits_simps objBitsT_simps)
|
||||
apply (rename_tac arch_kernel_object)
|
||||
apply (case_tac arch_kernel_object; simp add: archObjSize_def objBitsT_simps)
|
||||
apply (case_tac arch_kernel_object; simp add: archObjSize_def objBitsT_simps bit_simps)
|
||||
done
|
||||
|
||||
lemma sane_update [intro!]:
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
|
|||
lemmas makeObject_simps =
|
||||
makeObject_endpoint makeObject_notification makeObject_cte
|
||||
makeObject_tcb makeObject_user_data makeObject_pde makeObject_pte
|
||||
makeObject_asidpool
|
||||
makeObject_asidpool makeObject_pdpte makeObject_pml4e
|
||||
end
|
||||
definition
|
||||
"diminished' cap cap' \<equiv> \<exists>R. cap = maskCapRights R cap'"
|
||||
|
|
|
|||
|
|
@ -17,8 +17,10 @@ imports Invariants_H
|
|||
begin
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
||||
(* FIXME x64: should this be 32 bc cte_level_bits is 5 not 4 *)
|
||||
definition
|
||||
cte_map :: "cslot_ptr \<Rightarrow> word32"
|
||||
cte_map :: "cslot_ptr \<Rightarrow> machine_word"
|
||||
where
|
||||
"cte_map \<equiv> \<lambda>(oref, cref). oref + (of_bl cref * 16)"
|
||||
|
||||
|
|
@ -32,9 +34,9 @@ where
|
|||
| ExceptionTypes_A.GuardMismatch n g \<Rightarrow> Fault_H.GuardMismatch n (of_bl g) (length g)"
|
||||
|
||||
primrec
|
||||
arch_fault_map :: "Machine_A.ARM_A.arch_fault \<Rightarrow> ArchFault_H.ARM_H.arch_fault"
|
||||
arch_fault_map :: "Machine_A.X64_A.arch_fault \<Rightarrow> ArchFault_H.X64_H.arch_fault"
|
||||
where
|
||||
"arch_fault_map (Machine_A.ARM_A.VMFault ptr msg) = ArchFault_H.ARM_H.VMFault ptr msg"
|
||||
"arch_fault_map (Machine_A.X64_A.VMFault ptr msg) = ArchFault_H.X64_H.VMFault ptr msg"
|
||||
|
||||
primrec
|
||||
fault_map :: "ExceptionTypes_A.fault \<Rightarrow> Fault_H.fault"
|
||||
|
|
@ -57,7 +59,7 @@ text {*
|
|||
*}
|
||||
|
||||
type_synonym obj_relation_cut = "Structures_A.kernel_object \<Rightarrow> Structures_H.kernel_object \<Rightarrow> bool"
|
||||
type_synonym obj_relation_cuts = "(word32 \<times> obj_relation_cut) set"
|
||||
type_synonym obj_relation_cuts = "(machine_word \<times> obj_relation_cut) set"
|
||||
|
||||
definition
|
||||
vmrights_map :: "rights set \<Rightarrow> vmrights"
|
||||
|
|
@ -79,12 +81,16 @@ where
|
|||
arch_capability.ASIDPoolCap x y)"
|
||||
| "acap_relation (arch_cap.ASIDControlCap) c = (c =
|
||||
arch_capability.ASIDControlCap)"
|
||||
| "acap_relation (arch_cap.PageCap dev word rghts sz data) c = (c =
|
||||
arch_capability.PageCap dev word (vmrights_map rghts) sz data)"
|
||||
| "acap_relation (arch_cap.PageCap dev word rghts typ sz data) c = (c =
|
||||
arch_capability.PageCap word (vmrights_map rghts) typ sz dev data)"
|
||||
| "acap_relation (arch_cap.PageTableCap word data) c = (c =
|
||||
arch_capability.PageTableCap word data)"
|
||||
| "acap_relation (arch_cap.PageDirectoryCap word data) c = (c =
|
||||
arch_capability.PageDirectoryCap word data)"
|
||||
| "acap_relation (arch_cap.PDPointerTableCap word data) c = (c =
|
||||
arch_capability.PDPointerTableCap word data)"
|
||||
| "acap_relation (arch_cap.PML4Cap word data) c = (c =
|
||||
arch_capability.PML4Cap word data)"
|
||||
|
||||
primrec
|
||||
cap_relation :: "cap \<Rightarrow> capability \<Rightarrow> bool"
|
||||
|
|
@ -123,7 +129,7 @@ where
|
|||
\<and> cs y = Some cap \<and> cap_relation cap (cteCap cte)"
|
||||
|
||||
definition
|
||||
asid_pool_relation :: "(10 word \<rightharpoonup> word32) \<Rightarrow> asidpool \<Rightarrow> bool"
|
||||
asid_pool_relation :: "(9 word \<rightharpoonup> machine_word) \<Rightarrow> asidpool \<Rightarrow> bool"
|
||||
where
|
||||
"asid_pool_relation \<equiv> \<lambda>p p'. p = inv ASIDPool p' o ucast"
|
||||
|
||||
|
|
@ -202,85 +208,90 @@ where
|
|||
(TCB tcb, KOTCB tcb') \<Rightarrow> tcb_relation tcb tcb'
|
||||
| (Endpoint ep, KOEndpoint ep') \<Rightarrow> ep_relation ep ep'
|
||||
| (Notification ntfn, KONotification ntfn') \<Rightarrow> ntfn_relation ntfn ntfn'
|
||||
| (ArchObj (ARM_A.ASIDPool pool), KOArch (KOASIDPool pool'))
|
||||
| (ArchObj (X64_A.ASIDPool pool), KOArch (KOASIDPool pool'))
|
||||
\<Rightarrow> asid_pool_relation pool pool'
|
||||
| _ \<Rightarrow> False)"
|
||||
|
||||
primrec
|
||||
pde_relation' :: "ARM_A.pde \<Rightarrow> ARM_H.pde \<Rightarrow> bool"
|
||||
pml4e_relation' :: "X64_A.pml4e \<Rightarrow> X64_H.pml4e \<Rightarrow> bool"
|
||||
where
|
||||
"pde_relation' ARM_A.InvalidPDE x = (x = ARM_H.InvalidPDE)"
|
||||
| "pde_relation' (ARM_A.PageTablePDE ptr atts domain) x
|
||||
= (x = ARM_H.PageTablePDE ptr (ParityEnabled \<in> atts) domain)"
|
||||
| "pde_relation' (ARM_A.SectionPDE ptr atts domain rghts) x
|
||||
= (x = ARM_H.SectionPDE ptr (ParityEnabled \<in> atts) domain
|
||||
(PageCacheable \<in> atts) (Global \<in> atts) (XNever \<in> atts) (vmrights_map rghts))"
|
||||
| "pde_relation' (ARM_A.SuperSectionPDE ptr atts rghts) x
|
||||
= (x = ARM_H.SuperSectionPDE ptr (ParityEnabled \<in> atts)
|
||||
(PageCacheable \<in> atts) (Global \<in> atts) (XNever \<in> atts) (vmrights_map rghts))"
|
||||
"pml4e_relation' X64_A.InvalidPML4E x = (x = X64_H.InvalidPML4E)"
|
||||
| "pml4e_relation' (X64_A.PDPointerTablePML4E ptr atts rights) x
|
||||
= (x = X64_H.PDPointerTablePML4E ptr (Accessed \<in> atts) (CacheDisabled \<in> atts) (WriteThrough \<in> atts)
|
||||
(ExecuteDisable \<in> atts) (vmrights_map rights))"
|
||||
|
||||
|
||||
primrec
|
||||
pte_relation' :: "ARM_A.pte \<Rightarrow> ARM_H.pte \<Rightarrow> bool"
|
||||
pdpte_relation' :: "X64_A.pdpte \<Rightarrow> X64_H.pdpte \<Rightarrow> bool"
|
||||
where
|
||||
"pte_relation' ARM_A.InvalidPTE x = (x = ARM_H.InvalidPTE)"
|
||||
| "pte_relation' (ARM_A.LargePagePTE ptr atts rghts) x
|
||||
= (x = ARM_H.LargePagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts)
|
||||
(XNever \<in> atts) (vmrights_map rghts))"
|
||||
| "pte_relation' (ARM_A.SmallPagePTE ptr atts rghts) x
|
||||
= (x = ARM_H.SmallPagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts)
|
||||
(XNever \<in> atts) (vmrights_map rghts))"
|
||||
"pdpte_relation' X64_A.InvalidPDPTE x = (x = X64_H.InvalidPDPTE)"
|
||||
| "pdpte_relation' (X64_A.PageDirectoryPDPTE ptr atts rights) x
|
||||
= (x = X64_H.PageDirectoryPDPTE ptr (Accessed \<in> atts) (CacheDisabled \<in> atts) (WriteThrough \<in> atts)
|
||||
(ExecuteDisable \<in> atts) (vmrights_map rights))"
|
||||
| "pdpte_relation' (X64_A.HugePagePDPTE ptr atts rghts) x
|
||||
= (x = X64_H.HugePagePDPTE ptr (Global \<in> atts) (PAT \<in> atts) (Dirty \<in> atts)
|
||||
(PTAttr Accessed \<in> atts) (PTAttr CacheDisabled \<in> atts)
|
||||
(PTAttr WriteThrough \<in> atts) (PTAttr ExecuteDisable \<in> atts)
|
||||
(vmrights_map rghts))"
|
||||
|
||||
|
||||
definition
|
||||
pde_align' :: "ARM_H.pde \<Rightarrow> nat"
|
||||
primrec
|
||||
pde_relation' :: "X64_A.pde \<Rightarrow> X64_H.pde \<Rightarrow> bool"
|
||||
where
|
||||
"pde_align' pde \<equiv>
|
||||
case pde of ARM_H.pde.SuperSectionPDE _ _ _ _ _ _ \<Rightarrow> 4 | _ \<Rightarrow> 0"
|
||||
"pde_relation' X64_A.InvalidPDE x = (x = X64_H.InvalidPDE)"
|
||||
| "pde_relation' (X64_A.PageTablePDE ptr atts rights) x
|
||||
= (x = X64_H.PageTablePDE ptr (Accessed \<in> atts) (CacheDisabled \<in> atts) (WriteThrough \<in> atts)
|
||||
(ExecuteDisable \<in> atts) (vmrights_map rights))"
|
||||
| "pde_relation' (X64_A.LargePagePDE ptr atts rghts) x
|
||||
= (x = X64_H.LargePagePDE ptr (Global \<in> atts) (PAT \<in> atts) (Dirty \<in> atts)
|
||||
(PTAttr Accessed \<in> atts) (PTAttr CacheDisabled \<in> atts)
|
||||
(PTAttr WriteThrough \<in> atts) (PTAttr ExecuteDisable \<in> atts)
|
||||
(vmrights_map rghts))"
|
||||
|
||||
lemmas pde_align_simps[simp] =
|
||||
pde_align'_def[split_simps ARM_A.pde.split]
|
||||
|
||||
definition
|
||||
pte_align' :: "ARM_H.pte \<Rightarrow> nat"
|
||||
primrec
|
||||
pte_relation' :: "X64_A.pte \<Rightarrow> X64_H.pte \<Rightarrow> bool"
|
||||
where
|
||||
"pte_align' pte \<equiv> case pte of ARM_H.pte.LargePagePTE _ _ _ _ _ \<Rightarrow> 4 | _ \<Rightarrow> 0"
|
||||
|
||||
lemmas pte_align_simps[simp] =
|
||||
pte_align'_def[split_simps ARM_A.pte.split]
|
||||
|
||||
definition
|
||||
"pde_relation_aligned y pde pde' \<equiv>
|
||||
if is_aligned y (pde_align' pde') then pde_relation' pde pde'
|
||||
else pde = ARM_A.InvalidPDE"
|
||||
|
||||
definition
|
||||
"pte_relation_aligned y pte pte' \<equiv>
|
||||
if is_aligned y (pte_align' pte') then pte_relation' pte pte'
|
||||
else pte = ARM_A.InvalidPTE"
|
||||
"pte_relation' X64_A.InvalidPTE x = (x = X64_H.InvalidPTE)"
|
||||
| "pte_relation' (X64_A.SmallPagePTE ptr atts rghts) x
|
||||
= (x = X64_H.SmallPagePTE ptr (Global \<in> atts) (PAT \<in> atts) (Dirty \<in> atts)
|
||||
(PTAttr Accessed \<in> atts) (PTAttr CacheDisabled \<in> atts)
|
||||
(PTAttr WriteThrough \<in> atts) (PTAttr ExecuteDisable \<in> atts)
|
||||
(vmrights_map rghts))"
|
||||
|
||||
definition
|
||||
"pte_relation y \<equiv> \<lambda>ko ko'. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> ko' = KOArch (KOPTE pte)
|
||||
\<and> pte_relation_aligned y (pt y) pte"
|
||||
\<and> pte_relation' (pt y) pte"
|
||||
|
||||
definition
|
||||
"pde_relation y \<equiv> \<lambda>ko ko'. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> ko' = KOArch (KOPDE pde)
|
||||
\<and> pde_relation_aligned y (pd y) pde"
|
||||
\<and> pde_relation' (pd y) pde"
|
||||
|
||||
definition
|
||||
"pdpte_relation y \<equiv> \<lambda>ko ko'. \<exists>pd pdpte. ko = ArchObj (PDPointerTable pd) \<and> ko' = KOArch (KOPDPTE pdpte)
|
||||
\<and> pdpte_relation' (pd y) pdpte"
|
||||
|
||||
definition
|
||||
"pml4e_relation y \<equiv> \<lambda>ko ko'. \<exists>pd pml4e. ko = ArchObj (PageMapL4 pd) \<and> ko' = KOArch (KOPML4E pml4e)
|
||||
\<and> pml4e_relation' (pd y) pml4e"
|
||||
|
||||
primrec
|
||||
aobj_relation_cuts :: "ARM_A.arch_kernel_obj \<Rightarrow> word32 \<Rightarrow> obj_relation_cuts"
|
||||
aobj_relation_cuts :: "X64_A.arch_kernel_obj \<Rightarrow> machine_word \<Rightarrow> obj_relation_cuts"
|
||||
where
|
||||
"aobj_relation_cuts (DataPage dev sz) x =
|
||||
{(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = (if dev then KOUserDataDevice else KOUserData) ) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }"
|
||||
| "aobj_relation_cuts (ARM_A.ASIDPool pool) x =
|
||||
| "aobj_relation_cuts (X64_A.ASIDPool pool) x =
|
||||
{(x, other_obj_relation)}"
|
||||
| "aobj_relation_cuts (PageTable pt) x =
|
||||
(\<lambda>y. (x + (ucast y << 2), pte_relation y)) ` UNIV"
|
||||
(\<lambda>y. (x + (ucast y << word_size_bits), pte_relation y)) ` UNIV"
|
||||
| "aobj_relation_cuts (PageDirectory pd) x =
|
||||
(\<lambda>y. (x + (ucast y << 2), pde_relation y)) ` UNIV"
|
||||
(\<lambda>y. (x + (ucast y << word_size_bits), pde_relation y)) ` UNIV"
|
||||
| "aobj_relation_cuts (PDPointerTable pdpt) x =
|
||||
(\<lambda>y. (x + (ucast y << word_size_bits), pdpte_relation y)) ` UNIV"
|
||||
| "aobj_relation_cuts (PageMapL4 pm) x =
|
||||
(\<lambda>y. (x + (ucast y << word_size_bits), pml4e_relation y)) ` UNIV"
|
||||
|
||||
primrec
|
||||
obj_relation_cuts :: "Structures_A.kernel_object \<Rightarrow> word32 \<Rightarrow> obj_relation_cuts"
|
||||
obj_relation_cuts :: "Structures_A.kernel_object \<Rightarrow> machine_word \<Rightarrow> obj_relation_cuts"
|
||||
where
|
||||
"obj_relation_cuts (CNode sz cs) x =
|
||||
(if well_formed_cnode_n sz cs
|
||||
|
|
@ -297,31 +308,39 @@ lemma obj_relation_cuts_def2:
|
|||
(case ko of CNode sz cs \<Rightarrow> if well_formed_cnode_n sz cs
|
||||
then {(cte_map (x, y), cte_relation y) | y. y \<in> dom cs}
|
||||
else {(x, \<bottom>\<bottom>)}
|
||||
| ArchObj (PageTable pt) \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pte_relation y))
|
||||
` (UNIV :: word8 set)
|
||||
| ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pde_relation y))
|
||||
` (UNIV :: 12 word set)
|
||||
| ArchObj (PageTable pt) \<Rightarrow> (\<lambda>y. (x + (ucast y << word_size_bits), pte_relation y))
|
||||
` (UNIV :: 9 word set)
|
||||
| ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>y. (x + (ucast y << word_size_bits), pde_relation y))
|
||||
` (UNIV :: 9 word set)
|
||||
| ArchObj (PDPointerTable pdpt) \<Rightarrow> (\<lambda>y. (x + (ucast y << word_size_bits), pdpte_relation y))
|
||||
` (UNIV :: 9 word set)
|
||||
| ArchObj (PageMapL4 pm) \<Rightarrow> (\<lambda>y. (x + (ucast y << word_size_bits), pml4e_relation y))
|
||||
` (UNIV :: 9 word set)
|
||||
| ArchObj (DataPage dev sz) \<Rightarrow>
|
||||
{(x + n * 2 ^ pageBits, \<lambda>_ obj. obj =(if dev then KOUserDataDevice else KOUserData)) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }
|
||||
| _ \<Rightarrow> {(x, other_obj_relation)})"
|
||||
by (simp split: Structures_A.kernel_object.split
|
||||
ARM_A.arch_kernel_obj.split)
|
||||
X64_A.arch_kernel_obj.split)
|
||||
|
||||
lemma obj_relation_cuts_def3:
|
||||
"obj_relation_cuts ko x =
|
||||
(case (a_type ko) of
|
||||
ACapTable n \<Rightarrow> {(cte_map (x, y), cte_relation y) | y. length y = n}
|
||||
| AArch APageTable \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pte_relation y))
|
||||
` (UNIV :: word8 set)
|
||||
| AArch APageDirectory \<Rightarrow> (\<lambda>y. (x + (ucast y << 2), pde_relation y))
|
||||
` (UNIV :: 12 word set)
|
||||
| AArch APageTable \<Rightarrow> (\<lambda>y. (x + (ucast y << word_size_bits), pte_relation y))
|
||||
` (UNIV :: 9 word set)
|
||||
| AArch APageDirectory \<Rightarrow> (\<lambda>y. (x + (ucast y << word_size_bits), pde_relation y))
|
||||
` (UNIV :: 9 word set)
|
||||
| AArch APDPointerTable \<Rightarrow> (\<lambda>y. (x + (ucast y << word_size_bits), pdpte_relation y))
|
||||
` (UNIV :: 9 word set)
|
||||
| AArch APageMapL4 \<Rightarrow> (\<lambda>y. (x + (ucast y << word_size_bits), pml4e_relation y))
|
||||
` (UNIV :: 9 word set)
|
||||
| AArch (AUserData sz) \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = KOUserData) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }
|
||||
| AArch (ADeviceData sz) \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = KOUserDataDevice ) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }
|
||||
| AGarbage _ \<Rightarrow> {(x, \<bottom>\<bottom>)}
|
||||
| _ \<Rightarrow> {(x, other_obj_relation)})"
|
||||
apply (simp add: obj_relation_cuts_def2 a_type_def
|
||||
split: Structures_A.kernel_object.split
|
||||
ARM_A.arch_kernel_obj.split)
|
||||
X64_A.arch_kernel_obj.split)
|
||||
apply (clarsimp simp: well_formed_cnode_n_def length_set_helper)
|
||||
done
|
||||
|
||||
|
|
@ -331,6 +350,8 @@ definition
|
|||
ACapTable n \<Rightarrow> False
|
||||
| AArch APageTable \<Rightarrow> False
|
||||
| AArch APageDirectory \<Rightarrow> False
|
||||
| AArch APDPointerTable \<Rightarrow> False
|
||||
| AArch APageMapL4 \<Rightarrow> False
|
||||
| AArch (AUserData _) \<Rightarrow> False
|
||||
| AArch (ADeviceData _) \<Rightarrow> False
|
||||
| AGarbage _ \<Rightarrow> False
|
||||
|
|
@ -355,12 +376,12 @@ lemma is_other_obj_relation_type:
|
|||
split: a_type.splits aa_type.splits)
|
||||
|
||||
definition
|
||||
pspace_dom :: "Structures_A.kheap \<Rightarrow> word32 set"
|
||||
pspace_dom :: "Structures_A.kheap \<Rightarrow> machine_word set"
|
||||
where
|
||||
"pspace_dom ps \<equiv> \<Union>x\<in>dom ps. fst ` (obj_relation_cuts (the (ps x)) x)"
|
||||
|
||||
definition
|
||||
pspace_relation :: "Structures_A.kheap \<Rightarrow> (word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> bool"
|
||||
pspace_relation :: "Structures_A.kheap \<Rightarrow> (machine_word \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> bool"
|
||||
where
|
||||
"pspace_relation ab con \<equiv>
|
||||
(pspace_dom ab = dom con) \<and>
|
||||
|
|
@ -375,7 +396,7 @@ where
|
|||
\<and> tcb_domain etcb = tcbDomain tcb'"
|
||||
|
||||
definition
|
||||
ekheap_relation :: "(obj_ref \<Rightarrow> etcb option) \<Rightarrow> (word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> bool"
|
||||
ekheap_relation :: "(obj_ref \<Rightarrow> etcb option) \<Rightarrow> (machine_word \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> bool"
|
||||
where
|
||||
"ekheap_relation ab con \<equiv>
|
||||
\<forall>x \<in> dom ab. \<exists>tcb'. con x = Some (KOTCB tcb') \<and> etcb_relation (the (ab x)) tcb'"
|
||||
|
|
@ -394,7 +415,7 @@ where
|
|||
"ready_queues_relation qs qs' \<equiv> \<forall>d p. (qs d p = qs' (d, p))"
|
||||
|
||||
definition
|
||||
ghost_relation :: "Structures_A.kheap \<Rightarrow> (word32 \<rightharpoonup> vmpage_size) \<Rightarrow> (word32 \<rightharpoonup> nat) \<Rightarrow> bool"
|
||||
ghost_relation :: "Structures_A.kheap \<Rightarrow> (machine_word \<rightharpoonup> vmpage_size) \<Rightarrow> (machine_word \<rightharpoonup> nat) \<Rightarrow> bool"
|
||||
where
|
||||
"ghost_relation h ups cns \<equiv>
|
||||
(\<forall>a sz. (\<exists>dev. h a = Some (ArchObj (DataPage dev sz))) \<longleftrightarrow> ups a = Some sz) \<and>
|
||||
|
|
@ -441,16 +462,22 @@ where
|
|||
\<and> (\<forall>irq. irq_state_relation (irqs irq) (irqs' irq)))"
|
||||
|
||||
definition
|
||||
arch_state_relation :: "(arch_state \<times> ARM_H.kernel_state) set"
|
||||
cr3_relation :: "CR3 \<Rightarrow> cr3 \<Rightarrow> bool"
|
||||
where
|
||||
"cr3_relation c c' \<equiv> CR3BaseAddress c = cr3BaseAddress c' \<and> CR3pcid c = cr3pcid c'"
|
||||
|
||||
definition
|
||||
arch_state_relation :: "(arch_state \<times> X64_H.kernel_state) set"
|
||||
where
|
||||
"arch_state_relation \<equiv> {(s, s') .
|
||||
arm_asid_table s = armKSASIDTable s' o ucast
|
||||
\<and> arm_global_pd s = armKSGlobalPD s'
|
||||
\<and> arm_hwasid_table s = armKSHWASIDTable s'
|
||||
\<and> arm_global_pts s = armKSGlobalPTs s'
|
||||
\<and> arm_next_asid s = armKSNextASID s'
|
||||
\<and> arm_asid_map s = armKSASIDMap s'
|
||||
\<and> arm_kernel_vspace s = armKSKernelVSpace s'}"
|
||||
x64_asid_table s = x64KSASIDTable s' o ucast
|
||||
\<and> x64_global_pml4 s = x64KSGlobalPML4 s'
|
||||
\<and> x64_global_pdpts s = x64KSGlobalPDPTs s'
|
||||
\<and> x64_global_pds s = x64KSGlobalPDs s'
|
||||
\<and> x64_global_pts s = x64KSGlobalPTs s'
|
||||
\<and> x64_asid_map s = x64KSASIDMap s'
|
||||
\<and> cr3_relation (x64_current_cr3 s) (x64KSCurrentCR3 s')
|
||||
\<and> x64_kernel_vspace s = x64KSKernelVSpace s'}"
|
||||
|
||||
|
||||
definition
|
||||
|
|
@ -465,11 +492,17 @@ lemma obj_relation_cutsE:
|
|||
\<And>sz cs z cap cte. \<lbrakk> ko = CNode sz cs; well_formed_cnode_n sz cs; y = cte_map (x, z);
|
||||
ko' = KOCTE cte; cs z = Some cap; cap_relation cap (cteCap cte) \<rbrakk>
|
||||
\<Longrightarrow> R;
|
||||
\<And>pt (z :: word8) pte'. \<lbrakk> ko = ArchObj (PageTable pt); y = x + (ucast z << 2);
|
||||
ko' = KOArch (KOPTE pte'); pte_relation_aligned z (pt z) pte' \<rbrakk>
|
||||
\<And>pt (z :: 9 word) pte'. \<lbrakk> ko = ArchObj (PageTable pt); y = x + (ucast z << word_size_bits);
|
||||
ko' = KOArch (KOPTE pte'); pte_relation' (pt z) pte' \<rbrakk>
|
||||
\<Longrightarrow> R;
|
||||
\<And>pd (z :: 12 word) pde'. \<lbrakk> ko = ArchObj (PageDirectory pd); y = x + (ucast z << 2);
|
||||
ko' = KOArch (KOPDE pde'); pde_relation_aligned z (pd z) pde' \<rbrakk>
|
||||
\<And>pd (z :: 9 word) pde'. \<lbrakk> ko = ArchObj (PageDirectory pd); y = x + (ucast z << word_size_bits);
|
||||
ko' = KOArch (KOPDE pde'); pde_relation' (pd z) pde' \<rbrakk>
|
||||
\<Longrightarrow> R;
|
||||
\<And>pdpt (z :: 9 word) pdpte'. \<lbrakk> ko = ArchObj (PDPointerTable pdpt); y = x + (ucast z << word_size_bits);
|
||||
ko' = KOArch (KOPDPTE pdpte'); pdpte_relation' (pdpt z) pdpte' \<rbrakk>
|
||||
\<Longrightarrow> R;
|
||||
\<And>pml4 (z :: 9 word) pml4e'. \<lbrakk> ko = ArchObj (PageMapL4 pml4); y = x + (ucast z << word_size_bits);
|
||||
ko' = KOArch (KOPML4E pml4e'); pml4e_relation' (pml4 z) pml4e' \<rbrakk>
|
||||
\<Longrightarrow> R;
|
||||
\<And>sz dev n. \<lbrakk> ko = ArchObj (DataPage dev sz); ko' = (if dev then KOUserDataDevice else KOUserData);
|
||||
y = x + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize sz - pageBits) \<rbrakk> \<Longrightarrow> R;
|
||||
|
|
@ -478,9 +511,10 @@ lemma obj_relation_cutsE:
|
|||
apply (simp add: obj_relation_cuts_def2 is_other_obj_relation_type_def
|
||||
a_type_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 ((clarsimp split: if_splits,
|
||||
force simp: cte_relation_def pte_relation_def pde_relation_def)+)[5]
|
||||
force simp: cte_relation_def pte_relation_def pde_relation_def
|
||||
pdpte_relation_def pml4e_relation_def)+)
|
||||
done
|
||||
|
||||
lemma eq_trans_helper:
|
||||
|
|
@ -533,7 +567,7 @@ where
|
|||
| "syscall_error_map (ExceptionTypes_A.NotEnoughMemory n) = Fault_H.syscall_error.NotEnoughMemory n"
|
||||
|
||||
definition
|
||||
APIType_map :: "Structures_A.apiobject_type \<Rightarrow> ARM_H.object_type"
|
||||
APIType_map :: "Structures_A.apiobject_type \<Rightarrow> X64_H.object_type"
|
||||
where
|
||||
"APIType_map ty \<equiv> case ty of
|
||||
Structures_A.Untyped \<Rightarrow> APIObjectType ArchTypes_H.Untyped
|
||||
|
|
@ -544,10 +578,11 @@ where
|
|||
| ArchObject ao \<Rightarrow> (case ao of
|
||||
SmallPageObj \<Rightarrow> SmallPageObject
|
||||
| LargePageObj \<Rightarrow> LargePageObject
|
||||
| SectionObj \<Rightarrow> SectionObject
|
||||
| SuperSectionObj \<Rightarrow> SuperSectionObject
|
||||
| HugePageObj \<Rightarrow> HugePageObject
|
||||
| PageTableObj \<Rightarrow> PageTableObject
|
||||
| PageDirectoryObj \<Rightarrow> PageDirectoryObject)"
|
||||
| PageDirectoryObj \<Rightarrow> PageDirectoryObject
|
||||
| PDPTObj \<Rightarrow> PDPointerTableObject
|
||||
| PML4Obj \<Rightarrow> PML4Object)"
|
||||
|
||||
lemma get_tcb_at: "tcb_at t s \<Longrightarrow> (\<exists>tcb. get_tcb t s = Some tcb)"
|
||||
by (simp add: tcb_at_def)
|
||||
|
|
@ -671,9 +706,9 @@ lemma objBits_obj_bits:
|
|||
by (simp add: other_obj_relation_def objBitsKO_simps pageBits_def
|
||||
archObjSize_def
|
||||
split: Structures_A.kernel_object.split_asm
|
||||
ARM_A.arch_kernel_obj.split_asm
|
||||
X64_A.arch_kernel_obj.split_asm
|
||||
Structures_H.kernel_object.split_asm
|
||||
ARM_H.arch_kernel_object.split_asm)
|
||||
X64_H.arch_kernel_object.split_asm)
|
||||
|
||||
lemma replicate_length_cong:
|
||||
"x = y \<Longrightarrow> replicate x n = replicate y n" by simp
|
||||
|
|
@ -684,6 +719,7 @@ lemmas isCap_defs =
|
|||
isEndpointCap_def isUntypedCap_def isNullCap_def
|
||||
isIRQHandlerCap_def isIRQControlCap_def isReplyCap_def
|
||||
isPageCap_def isPageTableCap_def isPageDirectoryCap_def
|
||||
isPDPointerTableCap_def isPML4Cap_def isIOPortCap_def
|
||||
isASIDControlCap_def isASIDPoolCap_def isArchPageCap_def
|
||||
isDomainCap_def
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue