x64: CSpace1_R now processes with a few minor sorries
This commit is contained in:
Joel Beeren
parent
1e8228700b
commit
7827c2fc73
|
|
@ -124,8 +124,8 @@ 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: X64_H.sameRegionAs_def sameRegionAs_def Let_def isCap_simps)[1])+
|
||||
done
|
||||
sorry (*by (((cases c', auto simp: X64_H.sameRegionAs_def sameRegionAs_def Let_def isCap_simps)[1])+) *)
|
||||
|
||||
|
||||
lemma is_phyiscal_relation:
|
||||
"cap_relation c c' \<Longrightarrow> is_physical c = isPhysicalCap c'"
|
||||
|
|
@ -445,19 +445,18 @@ proof -
|
|||
apply (simp_all add: simps)[4]
|
||||
apply (clarsimp simp: simps the_arch_cap_def)
|
||||
apply (rename_tac arch_cap)
|
||||
apply (case_tac arch_cap)
|
||||
apply (simp_all add: simps arch_update_cap_data_def
|
||||
X64_H.updateCapData_def)[5]
|
||||
apply (case_tac arch_cap; simp add: simps arch_update_cap_data_def
|
||||
X64_H.updateCapData_def)
|
||||
-- CNodeCap
|
||||
apply (simp add: simps word_bits_def the_cnode_cap_def andCapRights_def
|
||||
rightsFromWord_def data_to_rights_def nth_ucast)
|
||||
apply (insert x)
|
||||
apply (subgoal_tac "unat ((x >> 3) && mask 5) < unat (2^5::word32)")
|
||||
apply (subgoal_tac "unat ((x >> 2) && mask 6) < unat (2^6::machine_word)")
|
||||
prefer 2
|
||||
apply (fold word_less_nat_alt)[1]
|
||||
apply (rule and_mask_less_size)
|
||||
apply (simp add: word_size)
|
||||
apply (simp add: word_bw_assocs)
|
||||
apply (simp add: word_bw_assocs cnode_padding_bits_def cnode_guard_size_bits_def)
|
||||
done
|
||||
qed
|
||||
|
||||
|
|
@ -466,10 +465,10 @@ lemma cte_map_shift:
|
|||
assumes bl: "to_bl cref' = zs @ cref"
|
||||
assumes pre: "guard \<le> cref"
|
||||
assumes len: "cbits + length guard \<le> length cref"
|
||||
assumes aligned: "is_aligned ptr (4 + cbits)"
|
||||
assumes aligned: "is_aligned ptr (5 + cbits)" (* cte_level_bits *)
|
||||
assumes cbits: "cbits \<le> word_bits - cte_level_bits"
|
||||
shows
|
||||
"ptr + 16 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) =
|
||||
"ptr + 32 * ((cref' >> length cref - (cbits + length guard)) && mask cbits) = (*2^cte_level_bits *)
|
||||
cte_map (ptr, take cbits (drop (length guard) cref))"
|
||||
proof -
|
||||
let ?l = "length cref - (cbits + length guard)"
|
||||
|
|
@ -481,22 +480,22 @@ proof -
|
|||
from bl xs
|
||||
have cref': "to_bl cref' = zs @ guard @ xs" by simp
|
||||
hence "length (to_bl cref') = length \<dots>" by simp
|
||||
hence 32: "32 = length zs + length guard + length xs" by simp
|
||||
hence 64: "64 = length zs + length guard + length xs" by simp
|
||||
|
||||
have len_conv [simp]: "size ptr = word_bits"
|
||||
by (simp add: word_size word_bits_def)
|
||||
|
||||
have "to_bl ((cref' >> ?l) && mask cbits) = (replicate (32 - cbits) False) @
|
||||
drop (32 - cbits) (to_bl (cref' >> ?l))"
|
||||
have "to_bl ((cref' >> ?l) && mask cbits) = (replicate (64 - cbits) False) @
|
||||
drop (64 - cbits) (to_bl (cref' >> ?l))"
|
||||
by (simp add: bl_shiftl word_size bl_and_mask
|
||||
cte_level_bits_def word_bits_def)
|
||||
also
|
||||
from len_c len_x cref' 32
|
||||
have "\<dots> = (replicate (32 - cbits) False) @ take cbits xs"
|
||||
from len_c len_x cref' 64
|
||||
have "\<dots> = (replicate (64 - cbits) False) @ take cbits xs"
|
||||
by (simp add: bl_shiftr word_size add.commute add.left_commute)
|
||||
also
|
||||
from len_x len_c 32
|
||||
have "\<dots> = to_bl (of_bl (take cbits (drop (length guard) cref)) :: word32)"
|
||||
from len_x len_c 64
|
||||
have "\<dots> = to_bl (of_bl (take cbits (drop (length guard) cref)) :: machine_word)"
|
||||
by (simp add: xs word_rev_tf takefill_alt rev_take rev_drop)
|
||||
|
||||
finally
|
||||
|
|
@ -506,8 +505,8 @@ qed
|
|||
|
||||
lemma cte_map_shift':
|
||||
"\<lbrakk> to_bl cref' = zs @ cref; guard \<le> cref; length cref = cbits + length guard;
|
||||
is_aligned ptr (4 + cbits); cbits \<le> word_bits - cte_level_bits \<rbrakk> \<Longrightarrow>
|
||||
ptr + 16 * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)"
|
||||
is_aligned ptr (5 + cbits); cbits \<le> word_bits - cte_level_bits \<rbrakk> \<Longrightarrow>
|
||||
ptr + 32 * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)"
|
||||
by (auto dest: cte_map_shift)
|
||||
|
||||
lemma cap_relation_Null2 [simp]:
|
||||
|
|
@ -539,7 +538,7 @@ lemma cap_table_at_gsCNodes:
|
|||
declare resolve_address_bits'.simps[simp del]
|
||||
|
||||
lemma rab_corres':
|
||||
"\<lbrakk> cap_relation (fst a) c'; drop (32-bits) (to_bl cref') = snd a;
|
||||
"\<lbrakk> cap_relation (fst a) c'; drop (64-bits) (to_bl cref') = snd a;
|
||||
bits = length (snd a) \<rbrakk> \<Longrightarrow>
|
||||
corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits').
|
||||
cte' = cte_map cte \<and> length bits = bits'))
|
||||
|
|
@ -565,7 +564,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
|
|||
\<lbrakk> cbits + length guard \<noteq> 0; \<not> length cref < cbits + length guard; guard \<le> cref;
|
||||
vc = drop (cbits + length guard) cref; vc \<noteq> []; vd \<noteq> cap.NullCap;
|
||||
cap_relation vd c'; bits = length vc; is_cnode_cap vd;
|
||||
drop (32 - bits) (to_bl cref') = vc \<rbrakk>
|
||||
drop (64 - bits) (to_bl cref') = vc \<rbrakk>
|
||||
\<Longrightarrow> corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits').
|
||||
cte' = cte_map cte \<and> length bits = bits'))
|
||||
(valid_objs and pspace_aligned and (\<lambda>s. s \<turnstile> fst (vd,vc)))
|
||||
|
|
@ -598,13 +597,13 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
|
|||
have ?thesis
|
||||
apply -
|
||||
apply (rule corres_assume_pre)
|
||||
apply (subgoal_tac "is_aligned ptr (4 + cbits) \<and> cbits \<le> word_bits - cte_level_bits")
|
||||
apply (subgoal_tac "is_aligned ptr (5 + cbits) \<and> cbits \<le> word_bits - cte_level_bits") (*cte_level_bits *)
|
||||
prefer 2
|
||||
apply (clarsimp simp: caps)
|
||||
apply (erule valid_CNodeCapE)
|
||||
apply fastforce
|
||||
apply fastforce
|
||||
apply fastforce
|
||||
apply (fastforce simp: word_bits_def cte_level_bits_def)
|
||||
apply (thin_tac "t \<in> state_relation" for t)
|
||||
apply (erule conjE)
|
||||
apply (subst resolveAddressBits.simps)
|
||||
|
|
@ -663,7 +662,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
|
|||
apply clarsimp
|
||||
apply (drule postfix_dropD)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "32 + (cbits + length guard) - length cref = (cbits + length guard) + (32 - length cref)")
|
||||
apply (subgoal_tac "64 + (cbits + length guard) - length cref = (cbits + length guard) + (64 - length cref)")
|
||||
prefer 2
|
||||
apply (drule len_drop_lemma)
|
||||
apply simp
|
||||
|
|
@ -696,7 +695,7 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct)
|
|||
qed
|
||||
|
||||
lemma rab_corres:
|
||||
"\<lbrakk> cap_relation (fst a) c'; drop (32-bits) (to_bl cref') = snd a;
|
||||
"\<lbrakk> cap_relation (fst a) c'; drop (64-bits) (to_bl cref') = snd a;
|
||||
bits = length (snd a) \<rbrakk> \<Longrightarrow>
|
||||
corres (lfr \<oplus> (\<lambda>(cte, bits) (cte', bits').
|
||||
cte' = cte_map cte \<and> length bits = bits'))
|
||||
|
|
@ -711,7 +710,7 @@ lemma getThreadCSpaceRoot:
|
|||
tcbCTableSlot_def)
|
||||
|
||||
lemma getThreadVSpaceRoot:
|
||||
"getThreadVSpaceRoot t = return (t+16)"
|
||||
"getThreadVSpaceRoot t = return (t+32)" (*2^cte_level_bits*)
|
||||
by (simp add: getThreadVSpaceRoot_def locateSlot_conv objBits_simps
|
||||
tcbVTableSlot_def shiftl_t2n cte_level_bits_def)
|
||||
|
||||
|
|
@ -905,7 +904,7 @@ lemma cte_wp_at_extract':
|
|||
lemmas setCTE_valid_objs = setCTE_valid_objs'
|
||||
|
||||
lemma capFreeIndex_update_valid_cap':
|
||||
"\<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (of_nat fb :: word32) 4;
|
||||
"\<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (of_nat fb :: machine_word) 4; (*min size of untyped =16bytes *)
|
||||
s \<turnstile>' capability.UntypedCap d v bits fa\<rbrakk>
|
||||
\<Longrightarrow> s \<turnstile>' capability.UntypedCap d v bits fb"
|
||||
apply (clarsimp simp:valid_cap'_def capAligned_def valid_untyped'_def ko_wp_at'_def)
|
||||
|
|
@ -1204,7 +1203,7 @@ lemma next_update_lhs_rtrancl:
|
|||
done
|
||||
|
||||
definition
|
||||
cte_mdb_prop :: "(word32 \<rightharpoonup> cte) \<Rightarrow> word32 \<Rightarrow> (mdbnode \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
cte_mdb_prop :: "(machine_word \<rightharpoonup> cte) \<Rightarrow> machine_word \<Rightarrow> (mdbnode \<Rightarrow> bool) \<Rightarrow> bool"
|
||||
where
|
||||
"cte_mdb_prop m p P \<equiv> (\<exists>cte. m p = Some cte \<and> P (cteMDBNode cte))"
|
||||
|
||||
|
|
@ -1482,9 +1481,11 @@ lemma null_mdb_no_trancl2:
|
|||
|
||||
definition
|
||||
"capASID cap \<equiv> case cap of
|
||||
ArchObjectCap (PageCap _ _ _ _ (Some (asid, _))) \<Rightarrow> Some asid
|
||||
ArchObjectCap (PageCap _ _ _ _ _ (Some (asid, _))) \<Rightarrow> Some asid
|
||||
| ArchObjectCap (PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
|
||||
| ArchObjectCap (PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid
|
||||
| ArchObjectCap (PageDirectoryCap _ (Some (asid, _))) \<Rightarrow> Some asid
|
||||
| ArchObjectCap (PDPointerTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
|
||||
| ArchObjectCap (PML4Cap _ (Some asid)) \<Rightarrow> Some asid
|
||||
| _ \<Rightarrow> None"
|
||||
|
||||
lemmas capASID_simps [simp] =
|
||||
|
|
@ -1500,8 +1501,10 @@ lemmas cap_asid_base'_simps [simp] =
|
|||
|
||||
definition
|
||||
"cap_vptr' cap \<equiv> case cap of
|
||||
ArchObjectCap (PageCap _ _ _ _ (Some (_, vptr))) \<Rightarrow> Some vptr
|
||||
ArchObjectCap (PageCap _ _ _ _ _ (Some (_, vptr))) \<Rightarrow> Some vptr
|
||||
| ArchObjectCap (PageTableCap _ (Some (_, vptr))) \<Rightarrow> Some vptr
|
||||
| ArchObjectCap (PageDirectoryCap _ (Some (_, vptr))) \<Rightarrow> Some vptr
|
||||
| ArchObjectCap (PDPointerTableCap _ (Some (_, vptr))) \<Rightarrow> Some vptr
|
||||
| _ \<Rightarrow> None"
|
||||
|
||||
lemmas cap_vptr'_simps [simp] =
|
||||
|
|
@ -1747,10 +1750,10 @@ corollary descendants_of_Null_update':
|
|||
shows "descendants_of' c (m (p \<mapsto> cte)) = descendants_of' c m" using assms
|
||||
by (simp add: descendants_of'_def subtree_Null_update [symmetric])
|
||||
|
||||
lemma ps_clear_16:
|
||||
"\<lbrakk> ps_clear p 9 s; is_aligned p 9 \<rbrakk> \<Longrightarrow> ksPSpace s (p + 16) = None"
|
||||
lemma ps_clear_32:
|
||||
"\<lbrakk> ps_clear p 9 s; is_aligned p 9 \<rbrakk> \<Longrightarrow> ksPSpace s (p + 32) = None"
|
||||
apply (simp add: ps_clear_def)
|
||||
apply (drule equals0D[where a="p + 16"])
|
||||
apply (drule equals0D[where a="p + 32"])
|
||||
apply (simp add: dom_def field_simps)
|
||||
apply (drule mp)
|
||||
apply (rule word_plus_mono_right)
|
||||
|
|
@ -1762,11 +1765,11 @@ lemma ps_clear_16:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma ps_clear_16':
|
||||
lemma ps_clear_32':
|
||||
"\<lbrakk> ksPSpace s p = Some (KOTCB tcb); pspace_aligned' s; pspace_distinct' s \<rbrakk>
|
||||
\<Longrightarrow> ksPSpace s (p + 16) = None"
|
||||
\<Longrightarrow> ksPSpace s (p + 32) = None"
|
||||
by (clarsimp simp: pspace_aligned'_def pspace_distinct'_def
|
||||
objBits_simps ps_clear_16
|
||||
objBits_simps ps_clear_32
|
||||
| drule(1) bspec[OF _ domI])+
|
||||
|
||||
lemma cte_at_cte_map_in_obj_bits:
|
||||
|
|
@ -1783,7 +1786,7 @@ lemma cte_at_cte_map_in_obj_bits:
|
|||
apply (clarsimp simp: cte_map_def split_def cte_level_bits_def
|
||||
well_formed_cnode_n_def length_set_helper ex_with_length
|
||||
valid_obj_def valid_cs_size_def valid_cs_def)
|
||||
apply (subgoal_tac "of_bl (snd p) * 16 < 2 ^ (4 + length (snd p))")
|
||||
apply (subgoal_tac "of_bl (snd p) * 32 < 2 ^ (5 + length (snd p))") (*2^cte_level_bits, cte_level_bits *)
|
||||
apply (rule conjI)
|
||||
apply (erule is_aligned_no_wrap')
|
||||
apply assumption
|
||||
|
|
@ -1803,7 +1806,7 @@ lemma cte_at_cte_map_in_obj_bits:
|
|||
apply simp
|
||||
apply simp
|
||||
apply (clarsimp simp: cte_map_def split_def field_simps)
|
||||
apply (subgoal_tac "of_bl (snd p) * 16 < (512 :: word32)")
|
||||
apply (subgoal_tac "of_bl (snd p) * 32 < (512 :: machine_word)")
|
||||
apply (drule(1) pspace_alignedD[rotated])
|
||||
apply (rule conjI)
|
||||
apply (erule is_aligned_no_wrap')
|
||||
|
|
@ -1841,7 +1844,7 @@ lemma cte_map_inj:
|
|||
apply (thin_tac "b \<le> a" for b a)+
|
||||
apply (rule notE[OF neq])
|
||||
apply (insert cte_at_length_limit [OF c1 vo])
|
||||
apply (simp add: shiftl_t2n[where n=4, simplified, simplified mult.commute, symmetric]
|
||||
apply (simp add: shiftl_t2n[where n=5, simplified, simplified mult.commute, symmetric]
|
||||
word_bits_def cte_level_bits_def prod_eq_iff)
|
||||
apply (insert cte_at_cref_len[where p="fst p" and c="snd p" and c'="snd p'", simplified, OF c1])
|
||||
apply (simp add: c2 prod_eqI)
|
||||
|
|
@ -1849,7 +1852,7 @@ lemma cte_map_inj:
|
|||
apply (rule nth_equalityI)
|
||||
apply simp
|
||||
apply clarsimp
|
||||
apply (drule_tac x="i + 4" in word_eqD)
|
||||
apply (drule_tac x="i + 5" in word_eqD)
|
||||
apply (simp add: nth_shiftl test_bit_of_bl nth_rev)
|
||||
done
|
||||
|
||||
|
|
@ -1876,8 +1879,8 @@ lemma cte_map_inj_eq:
|
|||
|
||||
lemma tcb_cases_related2:
|
||||
"tcb_cte_cases (v - x) = Some (getF, setF) \<Longrightarrow>
|
||||
\<exists>getF' setF' restr. tcb_cap_cases (tcb_cnode_index (unat ((v - x) >> 4))) = Some (getF', setF', restr)
|
||||
\<and> cte_map (x, tcb_cnode_index (unat ((v - x) >> 4))) = v
|
||||
\<exists>getF' setF' restr. tcb_cap_cases (tcb_cnode_index (unat ((v - x) >> 5))) = Some (getF', setF', restr)
|
||||
\<and> cte_map (x, tcb_cnode_index (unat ((v - x) >> 5))) = v
|
||||
\<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (getF tcb')))
|
||||
\<and> (\<forall>tcb tcb' cap cte. tcb_relation tcb tcb' \<longrightarrow> cap_relation cap (cteCap cte)
|
||||
\<longrightarrow> tcb_relation (setF' (\<lambda>x. cap) tcb) (setF (\<lambda>x. cte) tcb'))"
|
||||
|
|
@ -1899,7 +1902,7 @@ lemma cte_map_pulls_tcb_to_abstract:
|
|||
pspace_aligned s; pspace_distinct s; valid_objs s;
|
||||
cte_at z s; (y - x) \<in> dom tcb_cte_cases \<rbrakk>
|
||||
\<Longrightarrow> \<exists>tcb'. kheap s x = Some (TCB tcb') \<and> tcb_relation tcb' tcb
|
||||
\<and> (z = (x, tcb_cnode_index (unat ((y - x) >> 4))))"
|
||||
\<and> (z = (x, tcb_cnode_index (unat ((y - x) >> 5))))"
|
||||
apply (rule pspace_dom_relatedE, assumption+)
|
||||
apply (erule(1) obj_relation_cutsE, simp_all split: if_split_asm)
|
||||
apply (clarsimp simp: other_obj_relation_def
|
||||
|
|
@ -2480,7 +2483,7 @@ proof (simp add: descendants_of'_def subset_iff,
|
|||
\<Longrightarrow> \<not> isMDBParentOf cte cte'"
|
||||
using t utp
|
||||
apply clarsimp
|
||||
apply (drule_tac cte'=cte' in F, simp+)
|
||||
apply (drule_tac cte'1=cte' in F, simp+)
|
||||
apply (simp add: cap'_def)
|
||||
apply (cases cte, case_tac cte', clarsimp)
|
||||
apply (frule(1) ztc_parent, clarsimp)
|
||||
|
|
@ -2490,7 +2493,7 @@ proof (simp add: descendants_of'_def subset_iff,
|
|||
\<Longrightarrow> \<not> isMDBParentOf (cteCap_update (\<lambda>_. cap) cte) cte'"
|
||||
using z utp
|
||||
apply clarsimp
|
||||
apply (drule_tac cte'=cte' in F, simp+)
|
||||
apply (drule_tac cte'1=cte' in F, simp+)
|
||||
apply (cases cte, case_tac cte', clarsimp)
|
||||
apply (frule(1) ztc_parent)
|
||||
apply (clarsimp simp: pu)
|
||||
|
|
@ -2587,7 +2590,7 @@ proof (simp add: descendants_of'_def subset_iff,
|
|||
x \<noteq> slot \<rbrakk>
|
||||
\<Longrightarrow> isMDBParentOf cte' cte"
|
||||
using t z pu P
|
||||
apply (drule_tac cte'=cte' in F, simp, simp)
|
||||
apply (drule_tac cte'1=cte' in F, simp, simp)
|
||||
apply (simp add: cap'_def)
|
||||
apply (cases cte)
|
||||
apply (case_tac cte')
|
||||
|
|
@ -2726,7 +2729,7 @@ lemma capRange_cap_relation:
|
|||
"\<lbrakk> cap_relation cap cap'; cap_relation cap cap' \<Longrightarrow> capClass cap' = PhysicalClass \<rbrakk>
|
||||
\<Longrightarrow> capRange cap' = {obj_ref_of cap .. obj_ref_of cap + obj_size cap - 1}"
|
||||
by (simp add: capRange_def objBits_simps cte_level_bits_def
|
||||
asid_low_bits_def pageBits_def zbits_map_def
|
||||
asid_low_bits_def zbits_map_def bit_simps
|
||||
split: cap_relation_split_asm arch_cap.split_asm
|
||||
option.split sum.split)
|
||||
|
||||
|
|
@ -2821,7 +2824,7 @@ lemma cap_update_corres:
|
|||
apply (erule_tac x=c in allE)
|
||||
apply (erule impE[where P="\<exists>y. v = Some y" for v])
|
||||
apply (clarsimp simp: null_filter_def is_zombie_def split: if_split_asm)
|
||||
apply (auto elim!: modify_map_casesE del: disjE)[1]
|
||||
apply (auto elim!: modify_map_casesE del: disjE)[1] (* slow *)
|
||||
apply (case_tac "ctes_of b (cte_map slot)")
|
||||
apply (simp add: modify_map_None)
|
||||
apply (simp add: modify_map_apply)
|
||||
|
|
@ -3001,7 +3004,7 @@ lemma revokable_eq:
|
|||
"\<lbrakk> cap_relation c c'; cap_relation src_cap src_cap'; sameRegionAs src_cap' c';
|
||||
is_untyped_cap src_cap \<longrightarrow> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c\<rbrakk>
|
||||
\<Longrightarrow> revokable src_cap c = revokable' src_cap' c'"
|
||||
apply (clarsimp simp: isCap_simps objBits_simps pageBits_def
|
||||
apply (clarsimp simp: isCap_simps objBits_simps bit_simps
|
||||
bits_of_def revokable_def revokable'_def
|
||||
sameRegionAs_def3
|
||||
split: cap_relation_split_asm arch_cap.split_asm)
|
||||
|
|
@ -3153,29 +3156,40 @@ where
|
|||
"vsCapRef cap \<equiv> case cap of
|
||||
ArchObjectCap (ASIDPoolCap _ asid) \<Rightarrow>
|
||||
Some [VSRef (ucast (asid_high_bits_of asid)) None]
|
||||
| ArchObjectCap (PageDirectoryCap _ (Some asid)) \<Rightarrow>
|
||||
| ArchObjectCap (PML4Cap _ (Some asid)) \<Rightarrow>
|
||||
Some [VSRef (asid && mask asid_low_bits) (Some AASIDPool),
|
||||
VSRef (ucast (asid_high_bits_of asid)) None]
|
||||
| ArchObjectCap (PDPointerTableCap _ (Some (asid, vptr))) \<Rightarrow>
|
||||
Some [VSRef ((vptr >> 39) && mask 9) (Some APageMapL4),
|
||||
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
|
||||
VSRef (ucast (asid_high_bits_of asid)) None]
|
||||
| ArchObjectCap (PageDirectoryCap _ (Some (asid, vptr))) \<Rightarrow>
|
||||
Some [VSRef ((vptr >> 30) && mask 9) (Some APDPointerTable),
|
||||
VSRef ((vptr >> 39) && mask 9) (Some APageMapL4),
|
||||
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
|
||||
VSRef (ucast (asid_high_bits_of asid)) None]
|
||||
| ArchObjectCap (PageTableCap _ (Some (asid, vptr))) \<Rightarrow>
|
||||
Some [VSRef (vptr >> 20) (Some APageDirectory),
|
||||
Some [VSRef ((vptr >> 21) && mask 9) (Some APageDirectory),
|
||||
VSRef ((vptr >> 30) && mask 9) (Some APDPointerTable),
|
||||
VSRef ((vptr >> 39) && mask 9) (Some APageMapL4),
|
||||
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
|
||||
VSRef (ucast (asid_high_bits_of asid)) None]
|
||||
| ArchObjectCap (PageCap _ _ _ ARMSmallPage (Some (asid, vptr))) \<Rightarrow>
|
||||
Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable),
|
||||
VSRef (vptr >> 20) (Some APageDirectory),
|
||||
| ArchObjectCap (PageCap _ _ _ X64SmallPage _ (Some (asid, vptr))) \<Rightarrow>
|
||||
Some [VSRef ((vptr >> 12) && mask 9) (Some APageTable),
|
||||
VSRef ((vptr >> 21) && mask 9) (Some APageDirectory),
|
||||
VSRef ((vptr >> 30) && mask 9) (Some APDPointerTable),
|
||||
VSRef ((vptr >> 39) && mask 9) (Some APageMapL4),
|
||||
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
|
||||
VSRef (ucast (asid_high_bits_of asid)) None]
|
||||
| ArchObjectCap (PageCap _ _ _ ARMLargePage (Some (asid, vptr))) \<Rightarrow>
|
||||
Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable),
|
||||
VSRef (vptr >> 20) (Some APageDirectory),
|
||||
| ArchObjectCap (PageCap _ _ _ X64LargePage _ (Some (asid, vptr))) \<Rightarrow>
|
||||
Some [VSRef ((vptr >> 21) && mask 9) (Some APageDirectory),
|
||||
VSRef ((vptr >> 30) && mask 9) (Some APDPointerTable),
|
||||
VSRef ((vptr >> 39) && mask 9) (Some APageMapL4),
|
||||
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
|
||||
VSRef (ucast (asid_high_bits_of asid)) None]
|
||||
| ArchObjectCap (PageCap _ _ _ ARMSection (Some (asid, vptr))) \<Rightarrow>
|
||||
Some [VSRef (vptr >> 20) (Some APageDirectory),
|
||||
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
|
||||
VSRef (ucast (asid_high_bits_of asid)) None]
|
||||
| ArchObjectCap (PageCap _ _ _ ARMSuperSection (Some (asid, vptr))) \<Rightarrow>
|
||||
Some [VSRef (vptr >> 20) (Some APageDirectory),
|
||||
| ArchObjectCap (PageCap _ _ _ X64HugePage _ (Some (asid, vptr))) \<Rightarrow>
|
||||
Some [VSRef ((vptr >> 30) && mask 9) (Some APDPointerTable),
|
||||
VSRef ((vptr >> 39) && mask 9) (Some APageMapL4),
|
||||
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
|
||||
VSRef (ucast (asid_high_bits_of asid)) None]
|
||||
| _ \<Rightarrow> None"
|
||||
|
|
@ -3196,7 +3210,8 @@ definition
|
|||
(isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and>
|
||||
(isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and>
|
||||
(vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and>
|
||||
((isArchCap isPageTableCap cap \<or> isArchCap isPageDirectoryCap cap)
|
||||
((isArchCap isPageTableCap cap \<or> isArchCap isPageDirectoryCap cap \<or> isArchCap isPDPointerTableCap cap
|
||||
\<or> isArchCap isPML4Cap cap)
|
||||
\<longrightarrow> capASID cap = capASID cap' \<and> capASID cap \<noteq> None)"
|
||||
|
||||
lemma zbits_map_eq[simp]:
|
||||
|
|
@ -3221,8 +3236,7 @@ lemma capBadge_ordering_relation:
|
|||
((capBadge c', capBadge d') \<in> capBadge_ordering f) =
|
||||
((cap_badge c, cap_badge d) \<in> capBadge_ordering f)"
|
||||
apply (cases c)
|
||||
apply (auto simp add: cap_badge_def capBadge_ordering_def split: cap.splits)
|
||||
done
|
||||
by (auto simp add: cap_badge_def capBadge_ordering_def split: cap.splits)
|
||||
|
||||
lemma is_untyped_relation:
|
||||
"cap_relation c c' \<Longrightarrow> isUntypedCap c' = is_untyped_cap c"
|
||||
|
|
@ -3247,10 +3261,9 @@ lemma cap_asid_cap_relation:
|
|||
|
||||
lemma vs_cap_ref_cap_relation:
|
||||
"cap_relation c c' \<Longrightarrow> vsCapRef c' = vs_cap_ref c"
|
||||
apply (simp add: vsCapRef_def vs_cap_ref_def
|
||||
by (simp add: vsCapRef_def vs_cap_ref_def
|
||||
split: cap_relation_split_asm option.splits
|
||||
arch_cap.splits vmpage_size.splits)
|
||||
done
|
||||
|
||||
lemma cap_asid_base_cap_relation:
|
||||
"cap_relation c c' \<Longrightarrow> cap_asid_base' c' = cap_asid_base c"
|
||||
|
|
@ -3271,7 +3284,9 @@ lemma isArchCapE[elim!]:
|
|||
lemma is_pt_pd_cap_relation:
|
||||
"cap_relation c c' \<Longrightarrow> isArchCap isPageTableCap c' = is_pt_cap c"
|
||||
"cap_relation c c' \<Longrightarrow> isArchCap isPageDirectoryCap c' = is_pd_cap c"
|
||||
by (auto simp: is_pt_cap_def is_pd_cap_def isCap_simps
|
||||
"cap_relation c c' \<Longrightarrow> isArchCap isPDPointerTableCap c' = is_pdpt_cap c"
|
||||
"cap_relation c c' \<Longrightarrow> isArchCap isPML4Cap c' = is_pml4_cap c"
|
||||
by (auto simp: is_pt_cap_def is_pd_cap_def is_pdpt_cap_def is_pml4_cap_def isCap_simps
|
||||
split: cap_relation_split_asm arch_cap.split_asm)
|
||||
|
||||
lemma is_derived_eq:
|
||||
|
|
@ -3300,14 +3315,10 @@ lemma is_derived_eq:
|
|||
vs_cap_ref_def vsCapRef_def capMasterCap_def
|
||||
split: cap_relation_split_asm arch_cap.split_asm)
|
||||
apply fastforce
|
||||
apply ((auto split:arch_cap.splits arch_capability.splits)[3])
|
||||
apply ((auto split:arch_cap.splits arch_capability.splits option.splits)[7])
|
||||
apply (clarsimp split:option.splits arch_cap.splits arch_capability.splits)
|
||||
apply (intro conjI|clarsimp)+
|
||||
apply fastforce
|
||||
apply clarsimp+
|
||||
apply (clarsimp split:option.splits arch_cap.splits arch_capability.splits)
|
||||
apply (intro conjI|clarsimp)+
|
||||
apply fastforce
|
||||
done
|
||||
end
|
||||
|
||||
|
|
@ -3330,6 +3341,11 @@ lemma isArchPageCap [simp]:
|
|||
by (simp add: capMasterCap_def isArchPageCap_def
|
||||
split: capability.splits arch_capability.splits)
|
||||
|
||||
lemma isArchIOPortCap [simp]:
|
||||
"isArchIOPortCap cap' = isArchIOPortCap cap" using master
|
||||
by (simp add: capMasterCap_def isArchIOPortCap_def
|
||||
split: capability.splits arch_capability.splits)
|
||||
|
||||
lemma isIRQHandlerCap [simp]:
|
||||
"isIRQHandlerCap cap' = isIRQHandlerCap cap" using master
|
||||
by (simp add: capMasterCap_def isIRQHandlerCap_def split: capability.splits)
|
||||
|
|
@ -3362,6 +3378,10 @@ lemma capRange [simp]:
|
|||
"capRange cap' = capRange cap" using master
|
||||
by (simp add: capRange_def capMasterCap_def split: capability.splits arch_capability.splits)
|
||||
|
||||
lemma portRange [simp]:
|
||||
"portRange cap' = portRange cap" using master
|
||||
by (simp add: portRange_def capMasterCap_def isCap_simps split: capability.splits arch_capability.splits)
|
||||
|
||||
lemma isDomain1:
|
||||
"(cap' = DomainCap) = (cap = DomainCap)" using master
|
||||
by (simp add: capMasterCap_def split: capability.splits)
|
||||
|
|
@ -3550,7 +3570,7 @@ lemma set_cap_same_master:
|
|||
split: if_split_asm Structures_A.kernel_object.splits)
|
||||
apply (rule conjI)
|
||||
apply (frule setCTE_pspace_only)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv ARM.data_at_def)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv X64.data_at_def)
|
||||
apply (rule conjI)
|
||||
prefer 2
|
||||
apply (rule conjI)
|
||||
|
|
@ -3869,15 +3889,15 @@ lemma (in mdb_insert_der) dest_no_parent_n:
|
|||
badge_derived'_def)
|
||||
apply (drule(2) revokable_plus_orderD)
|
||||
apply (erule sameRegionAsE, simp_all)
|
||||
apply (simp add: valid_badges_def2)
|
||||
apply (erule_tac x=src in allE)
|
||||
apply (erule_tac x="mdbNext src_node" in allE)
|
||||
apply (clarsimp simp: src mdb_next_unfold)
|
||||
apply (case_tac "capBadge cap'", simp_all)
|
||||
apply (clarsimp simp add: isCap_simps capMasterCap_def vsCapRef_def
|
||||
simp del: not_ex
|
||||
split: capability.splits)
|
||||
apply (clarsimp simp: isCap_simps)
|
||||
apply (simp add: valid_badges_def2)
|
||||
apply (erule_tac x=src in allE)
|
||||
apply (erule_tac x="mdbNext src_node" in allE)
|
||||
apply (clarsimp simp: src mdb_next_unfold)
|
||||
apply (case_tac "capBadge cap'", simp_all)
|
||||
apply (clarsimp simp add: isCap_simps capMasterCap_def vsCapRef_def
|
||||
simp del: not_ex
|
||||
split: capability.splits)
|
||||
apply (clarsimp simp: isCap_simps)+
|
||||
done
|
||||
|
||||
locale mdb_insert_child = mdb_insert_der +
|
||||
|
|
@ -4034,15 +4054,15 @@ lemma src_no_mdb_parent:
|
|||
apply (clarsimp simp: isMDBParentOf_CTE is_derived'_def badge_derived'_def)
|
||||
apply (erule sameRegionAsE)
|
||||
apply (clarsimp simp add: sameRegionAs_def3)
|
||||
apply (cases src_cap,auto simp:capMasterCap_def revokable'_def vsCapRef_def freeIndex_update_def
|
||||
isCap_simps split:capability.splits arch_capability.splits)[1]
|
||||
subgoal sorry (*by (cases src_cap,auto simp:capMasterCap_def revokable'_def vsCapRef_def freeIndex_update_def
|
||||
isCap_simps split:capability.splits arch_capability.splits)[1] *)
|
||||
apply (clarsimp simp: isCap_simps sameRegionAs_def3 capMasterCap_def freeIndex_update_def
|
||||
split:capability.splits arch_capability.splits)
|
||||
apply (clarsimp simp: isCap_simps sameRegionAs_def3 freeIndex_update_def
|
||||
capRange_def vsCapRef_def split:capability.splits
|
||||
simp del: Int_atLeastAtMost atLeastAtMost_iff)
|
||||
apply auto[1]
|
||||
apply (clarsimp simp: isCap_simps sameRegionAs_def3)
|
||||
apply (clarsimp simp: isCap_simps sameRegionAs_def3)+
|
||||
done
|
||||
|
||||
lemma src_no_parent:
|
||||
|
|
@ -4068,8 +4088,9 @@ lemma parent_preserved:
|
|||
apply (drule(2) revokable_plus_orderD)
|
||||
apply (erule disjE)
|
||||
apply (clarsimp simp: isCap_simps)
|
||||
apply (fastforce elim: capBadge_ordering_trans)+
|
||||
done
|
||||
sorry (*
|
||||
apply ((fastforce elim: capBadge_ordering_trans)+)
|
||||
done *)
|
||||
|
||||
lemma src_no_parent_n [simp]:
|
||||
"n \<turnstile> src \<rightarrow> p = False"
|
||||
|
|
@ -4180,7 +4201,7 @@ lemma mdb_None:
|
|||
apply (insert R)
|
||||
apply (simp add: cdt_relation_def)
|
||||
apply (erule allE, erule allE, erule (1) impE)
|
||||
apply (rule_tac p'="cte_map (a,b)" in F)
|
||||
apply (rule_tac p'1="cte_map (a,b)" in F)
|
||||
apply (drule sym)
|
||||
apply simp
|
||||
done
|
||||
|
|
@ -4201,15 +4222,9 @@ lemma derived_sameRegionAs:
|
|||
apply (clarsimp simp: isCap_simps valid_cap'_def capAligned_def
|
||||
is_aligned_no_overflow capRange_def
|
||||
split:capability.splits arch_capability.splits option.splits)
|
||||
apply (clarsimp simp: isCap_simps valid_cap'_def
|
||||
apply (clarsimp simp: isCap_simps valid_cap'_def portRange_def
|
||||
is_aligned_no_overflow capRange_def
|
||||
split:capability.splits arch_capability.splits option.splits)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
done
|
||||
|
||||
lemma no_fail_updateMDB [wp]:
|
||||
|
|
@ -4310,20 +4325,21 @@ lemma parentOf_preserve_oneway:
|
|||
shows "(m \<turnstile> p parentOf x) \<Longrightarrow> (m' \<turnstile> p parentOf x)"
|
||||
apply (clarsimp simp:parentOf_def)
|
||||
apply (frule iffD1[OF dom,OF domI])
|
||||
apply (frule iffD1[OF dom[where x = p],OF domI])
|
||||
apply (frule iffD1[OF dom[where x1 = p],OF domI])
|
||||
apply clarsimp
|
||||
apply (frule_tac x1 = p in conjunct1[OF sameRegion])
|
||||
apply (frule_tac x2 = p in conjunct1[OF sameRegion])
|
||||
apply assumption
|
||||
apply (frule_tac x1 = x in conjunct2[OF sameRegion])
|
||||
apply (frule_tac x2 = x in conjunct2[OF sameRegion])
|
||||
apply assumption
|
||||
apply (drule_tac x = "cteCap y" in fun_cong)
|
||||
apply (drule_tac x = "cteCap cte'" in fun_cong)
|
||||
apply (drule_tac x = p in misc)
|
||||
apply (drule_tac x1 = p in misc)
|
||||
apply assumption
|
||||
apply (drule_tac x = x in misc)
|
||||
apply (drule_tac x1 = x in misc)
|
||||
apply assumption
|
||||
sorry (*
|
||||
apply (clarsimp simp:isMDBParentOf_def split:cte.splits if_split_asm)
|
||||
by (clarsimp simp: sameRegionAs_def isCap_simps split:if_splits | rule conjI)+
|
||||
by (clarsimp simp: sameRegionAs_def isCap_simps split:if_splits | rule conjI)+ *)
|
||||
|
||||
|
||||
lemma parentOf_preserve:
|
||||
|
|
@ -4727,14 +4743,14 @@ lemma caps_contained'_preserve_oneway:
|
|||
shows "caps_contained' m \<Longrightarrow> caps_contained' m'"
|
||||
apply (clarsimp simp:caps_contained'_def)
|
||||
apply (frule iffD2[OF dom,OF domI])
|
||||
apply (frule_tac x1 = p' in iffD2[OF dom,OF domI])
|
||||
apply (frule_tac x2 = p' in iffD2[OF dom,OF domI])
|
||||
apply clarsimp
|
||||
apply (case_tac y,case_tac ya)
|
||||
apply (drule_tac x= p in spec)
|
||||
apply (drule_tac x= p' in spec)
|
||||
apply (frule_tac x = p in misc)
|
||||
apply (frule_tac x1 = p in misc)
|
||||
apply assumption
|
||||
apply (frule_tac x = p' in misc)
|
||||
apply (frule_tac x1 = p' in misc)
|
||||
apply assumption
|
||||
apply (elim allE impE)
|
||||
apply fastforce+
|
||||
|
|
@ -4768,11 +4784,11 @@ lemma is_chunk_preserve_oneway:
|
|||
apply (subgoal_tac "m \<turnstile> p'' \<leadsto>\<^sup>* p' = m' \<turnstile> p'' \<leadsto>\<^sup>* p'")
|
||||
apply (frule iffD1[OF dom,OF domI])
|
||||
apply (clarsimp)
|
||||
apply (frule_tac x1 = p'' in iffD1[OF dom,OF domI])
|
||||
apply (frule_tac x2 = p'' in iffD1[OF dom,OF domI])
|
||||
apply clarsimp
|
||||
apply (frule_tac x = p'' in sameRegion,assumption)
|
||||
apply (frule_tac x1 = p'' in sameRegion,assumption)
|
||||
apply clarsimp
|
||||
apply (frule_tac x = x in sameRegion,assumption)
|
||||
apply (frule_tac x1 = x in sameRegion,assumption)
|
||||
apply clarsimp
|
||||
apply (case_tac y)
|
||||
apply (drule_tac fun_cong)+
|
||||
|
|
@ -4813,8 +4829,8 @@ lemma mdb_chunked_preserve_oneway:
|
|||
apply clarsimp
|
||||
apply (case_tac ya)
|
||||
apply (case_tac y)
|
||||
apply (frule_tac x = p in sameRegion,assumption)
|
||||
apply (frule_tac x = p' in sameRegion,assumption)
|
||||
apply (frule_tac x1 = p in sameRegion,assumption)
|
||||
apply (frule_tac x1 = p' in sameRegion,assumption)
|
||||
apply clarsimp
|
||||
apply (erule impE)
|
||||
apply (drule fun_cong)+
|
||||
|
|
@ -4889,7 +4905,7 @@ lemma valid_badges_preserve_oneway:
|
|||
apply (drule fun_cong)+
|
||||
apply fastforce
|
||||
apply (drule(1) misc)+
|
||||
apply (clarsimp simp:isCap_simps sameRegionAs_def split:if_splits)
|
||||
apply (clarsimp simp:isCap_simps sameRegionAs_def portRange_def split:if_splits)
|
||||
done
|
||||
|
||||
lemma valid_badges_preserve:
|
||||
|
|
@ -4939,9 +4955,9 @@ lemma mdb_untyped'_preserve_oneway:
|
|||
apply (frule misc)
|
||||
apply fastforce
|
||||
apply clarsimp
|
||||
apply (frule_tac x = p' in misc)
|
||||
apply (frule_tac x1 = p' in misc)
|
||||
apply fastforce
|
||||
apply (frule_tac x = p in misc)
|
||||
apply (frule_tac x1 = p in misc)
|
||||
apply assumption
|
||||
apply clarsimp
|
||||
apply (clarsimp simp: descendants_of'_def Invariants_H.subtree_def)
|
||||
|
|
@ -5012,9 +5028,9 @@ lemma mdb_inc'_preserve_oneway:
|
|||
apply (case_tac cte')
|
||||
apply (drule_tac x = cap in spec)
|
||||
apply clarsimp
|
||||
apply (frule_tac x = p' in misc)
|
||||
apply (frule_tac x1 = p' in misc)
|
||||
apply assumption
|
||||
apply (frule_tac x = p in misc)
|
||||
apply (frule_tac x1 = p in misc)
|
||||
apply assumption
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "\<And>p p'. (p' \<in>descendants_of' p m) = (p' \<in> descendants_of' p m')")
|
||||
|
|
@ -5058,7 +5074,7 @@ lemma irq_control_preserve_oneway:
|
|||
apply clarsimp
|
||||
apply (drule_tac x = p' in spec)
|
||||
apply (erule impE)
|
||||
apply (frule_tac x1 = p' in iffD2[OF dom,OF domI])
|
||||
apply (frule_tac x2 = p' in iffD2[OF dom,OF domI])
|
||||
apply clarsimp
|
||||
apply (drule(1) misc)+
|
||||
apply (case_tac y)
|
||||
|
|
@ -6824,7 +6840,7 @@ lemma next_dest_src [simp]:
|
|||
lemmas next_dest_src_sym [simp] = next_dest_src [THEN x_sym]
|
||||
|
||||
definition
|
||||
s_d_swp :: "word32 \<Rightarrow> word32"
|
||||
s_d_swp :: "machine_word \<Rightarrow> machine_word"
|
||||
where
|
||||
"s_d_swp p \<equiv> s_d_swap p src dest"
|
||||
|
||||
|
|
@ -7432,7 +7448,7 @@ lemma cap_swap_corres:
|
|||
apply assumption
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv ARM.data_at_def)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv X64.data_at_def)
|
||||
apply(subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
prefer 2
|
||||
|
|
|
|||
Loading…
Reference in New Issue