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

arch_split: Access and InfoFlow now build

This commit is contained in:
Daniel Matichuk 2016-01-25 18:40:30 +11:00
parent 8f9761ab38
commit 7aaa8ed774
12 changed files with 121 additions and 114 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
proof/access-control/Access.thy
View File

@ -268,19 +268,19 @@ where
definition
"pte_ref pte \<equiv> case pte of
ARM_Structs_A.pte.SmallPagePTE addr atts rights
Arch_Structs_A.pte.SmallPagePTE addr atts rights
\<Rightarrow> Some (ptrFromPAddr addr, pageBitsForSize ARMSmallPage, vspace_cap_rights_to_auth rights)
| ARM_Structs_A.pte.LargePagePTE addr atts rights
| Arch_Structs_A.pte.LargePagePTE addr atts rights
\<Rightarrow> Some (ptrFromPAddr addr, pageBitsForSize ARMLargePage, vspace_cap_rights_to_auth rights)
| _ \<Rightarrow> None"
definition
"pde_ref2 pde \<equiv> case pde of
ARM_Structs_A.pde.SectionPDE addr atts domain rights
Arch_Structs_A.pde.SectionPDE addr atts domain rights
\<Rightarrow> Some (ptrFromPAddr addr, pageBitsForSize ARMSection, vspace_cap_rights_to_auth rights)
| ARM_Structs_A.pde.SuperSectionPDE addr atts rights
| Arch_Structs_A.pde.SuperSectionPDE addr atts rights
\<Rightarrow> Some (ptrFromPAddr addr, pageBitsForSize ARMSuperSection, vspace_cap_rights_to_auth rights)
| ARM_Structs_A.pde.PageTablePDE addr atts domain
| Arch_Structs_A.pde.PageTablePDE addr atts domain
\<Rightarrow> Some (ptrFromPAddr addr, 0, {Control}) (* The 0 is a hack, saying that we own only addr, although 12 would also be OK *)
| _ \<Rightarrow> None"
@ -298,12 +298,12 @@ definition
\<Rightarrow> (obj_ref \<times> vs_ref \<times> auth) set"
where
"vs_refs_no_global_pts \<equiv> \<lambda>ko. case ko of
ArchObj (ARM_Structs_A.ASIDPool pool) \<Rightarrow>
ArchObj (Arch_Structs_A.ASIDPool pool) \<Rightarrow>
(\<lambda>(r,p). (p, VSRef (ucast r) (Some AASIDPool), Control)) ` graph_of pool
| ArchObj (ARM_Structs_A.PageDirectory pd) \<Rightarrow>
| ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
\<Union>(r,(p, sz, auth)) \<in> graph_of (pde_ref2 o pd) - {(x,y). (ucast (kernel_base >> 20) \<le> x)}.
(\<lambda>(p, a). (p, VSRef (ucast r) (Some APageDirectory), a)) ` (ptr_range p sz \<times> auth)
| ArchObj (ARM_Structs_A.PageTable pt) \<Rightarrow>
| ArchObj (Arch_Structs_A.PageTable pt) \<Rightarrow>
\<Union>(r,(p, sz, auth)) \<in> graph_of (pte_ref o pt).
(\<lambda>(p, a). (p, VSRef (ucast r) (Some APageTable), a)) ` (ptr_range p sz \<times> auth)
| _ \<Rightarrow> {}"
@ -372,15 +372,15 @@ where
fun
cap_asid' :: "cap \<Rightarrow> asid set"
where
"cap_asid' (Structures_A.ArchObjectCap (ARM_Structs_A.PageCap _ _ _ mapping))
"cap_asid' (Structures_A.ArchObjectCap (Arch_Structs_A.PageCap _ _ _ mapping))
= fst ` set_option mapping"
| "cap_asid' (Structures_A.ArchObjectCap (ARM_Structs_A.PageTableCap _ mapping))
| "cap_asid' (Structures_A.ArchObjectCap (Arch_Structs_A.PageTableCap _ mapping))
= fst ` set_option mapping"
| "cap_asid' (Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap _ asid_opt))
| "cap_asid' (Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap _ asid_opt))
= set_option asid_opt"
| "cap_asid' (Structures_A.ArchObjectCap (ARM_Structs_A.ASIDPoolCap _ asid))
| "cap_asid' (Structures_A.ArchObjectCap (Arch_Structs_A.ASIDPoolCap _ asid))
= {x. asid_high_bits_of x = asid_high_bits_of asid \<and> x \<noteq> 0}"
| "cap_asid' (Structures_A.ArchObjectCap ARM_Structs_A.ASIDControlCap) = UNIV"
| "cap_asid' (Structures_A.ArchObjectCap Arch_Structs_A.ASIDControlCap) = UNIV"
| "cap_asid' _ = {}"
inductive_set
@ -765,8 +765,8 @@ where
tcb' = tcb \<lparr>tcb_bound_notification := None\<rparr>;
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) None subjects aag \<rbrakk>
\<Longrightarrow> integrity_obj aag activate subjects l' ko ko'"
| tro_asidpool_clear: "\<lbrakk> ko = Some (ArchObj (ARM_Structs_A.ASIDPool pool));
ko' = Some (ArchObj (ARM_Structs_A.ASIDPool pool'));
| tro_asidpool_clear: "\<lbrakk> ko = Some (ArchObj (Arch_Structs_A.ASIDPool pool));
ko' = Some (ArchObj (Arch_Structs_A.ASIDPool pool'));
\<forall>x. pool' x \<noteq> pool x \<longrightarrow> pool' x = None
\<and> aag_subjects_have_auth_to subjects aag Control (the (pool x)) \<rbrakk>
\<Longrightarrow> integrity_obj aag activate subjects l' ko ko'"

18
proof/access-control/Arch_AC.thy
View File

@ -188,7 +188,7 @@ lemma clas_update_map_data_strg:
unfolding cap_links_asid_slot_def
by (fastforce simp: is_cap_simps update_map_data_def)
lemmas pte_ref_simps = pte_ref_def[split_simps ARM_Structs_A.pte.split]
lemmas pte_ref_simps = pte_ref_def[split_simps Arch_Structs_A.pte.split]
lemmas store_pde_pas_refined_simple
= store_pde_pas_refined[where pde=InvalidPDE, simplified pde_ref_simps, simplified]
@ -240,7 +240,7 @@ lemma perform_page_table_invocation_pas_refined [wp]:
done
definition
authorised_slots :: "'a PAS \<Rightarrow> ARM_Structs_A.pte \<times> (obj_ref list) + ARM_Structs_A.pde \<times> (obj_ref list) \<Rightarrow> bool"
authorised_slots :: "'a PAS \<Rightarrow> Arch_Structs_A.pte \<times> (obj_ref list) + Arch_Structs_A.pde \<times> (obj_ref list) \<Rightarrow> bool"
where
"authorised_slots aag m \<equiv> case m of
Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a \<in> (snd (snd x)). \<forall>p \<in> ptr_range (fst x) (fst (snd x)).(aag_has_auth_to aag a p)))
@ -267,7 +267,7 @@ lemma ptrFromPAddr_inj: "inj Platform.ptrFromPAddr"
by (auto intro: injI simp: Platform.ptrFromPAddr_def)
lemma vs_refs_no_global_pts_pdI:
"\<lbrakk>pd (ucast r) = ARM_Structs_A.pde.PageTablePDE x a b;
"\<lbrakk>pd (ucast r) = Arch_Structs_A.pde.PageTablePDE x a b;
((ucast r)::12 word) < ucast (kernel_base >> 20) \<rbrakk> \<Longrightarrow>
(Platform.ptrFromPAddr x, VSRef (r && mask 12)
(Some APageDirectory), Control)
@ -315,6 +315,8 @@ lemma lookup_pt_slot_authorised:
done
lemma is_aligned_6_masks:
fixes p :: word32
shows
"\<lbrakk> is_aligned p 6; bits = pt_bits \<or> bits = pd_bits \<rbrakk>
\<Longrightarrow> \<forall>x \<in> set [0, 4 .e. 0x3C]. x + p && ~~ mask bits = p && ~~ mask bits"
apply clarsimp
@ -428,8 +430,8 @@ lemma unmap_page_respects:
| wpc
| simp add: is_aligned_6_masks is_aligned_mask[symmetric] cleanByVA_PoU_def
| wp_once hoare_drop_imps
mapM_set'' [where f = "(\<lambda>a. store_pte a ARM_Structs_A.pte.InvalidPTE)" and I = "\<lambda>x s. is_subject aag (x && ~~ mask pt_bits)" and Q = "integrity aag X st"]
mapM_set'' [where f = "(\<lambda>a. store_pde a ARM_Structs_A.pde.InvalidPDE)" and I = "\<lambda>x s. is_subject aag (x && ~~ mask pd_bits)" and Q = "integrity aag X st"]
mapM_set'' [where f = "(\<lambda>a. store_pte a Arch_Structs_A.pte.InvalidPTE)" and I = "\<lambda>x s. is_subject aag (x && ~~ mask pt_bits)" and Q = "integrity aag X st"]
mapM_set'' [where f = "(\<lambda>a. store_pde a Arch_Structs_A.pde.InvalidPDE)" and I = "\<lambda>x s. is_subject aag (x && ~~ mask pd_bits)" and Q = "integrity aag X st"]
| wp_once hoare_drop_imps[where R="\<lambda>rv s. rv"])+
done
@ -1136,6 +1138,8 @@ lemma decode_arch_invocation_authorised:
-- "PageCap"
apply (clarsimp simp: valid_cap_simps cli_no_irqs)
apply (cases "invocation_type label", simp_all)
apply (rename_tac archlabel)
apply (case_tac archlabel, simp_all)
-- "Map"
apply (clarsimp simp: cap_auth_conferred_def is_cap_simps is_page_cap_def pas_refined_all_auth_is_owns)
apply (rule conjI)
@ -1162,11 +1166,13 @@ lemma decode_arch_invocation_authorised:
apply (simp add: aag_cap_auth_def cli_no_irqs)
-- "PageTableCap"
apply (cases "invocation_type label", simp_all)
apply (rename_tac archlabel)
apply (case_tac archlabel, simp_all)
-- "PTMap"
apply (clarsimp simp: aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def cap_auth_conferred_def is_page_cap_def
pde_ref2_def pas_refined_all_auth_is_owns pas_refined_refl pd_shifting [folded pd_bits_14] )
-- "Unmap"
apply (rename_tac word option)
apply (rename_tac word option archlabel)
apply (clarsimp simp: aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def cap_auth_conferred_def is_page_cap_def
pde_ref2_def pas_refined_all_auth_is_owns pas_refined_refl )
apply (subgoal_tac "x && ~~ mask pt_bits = word")

10
proof/access-control/CNode_AC.thy
View File

@ -983,8 +983,8 @@ lemma store_pde_pas_refined[wp]:
split: split_if_asm)
done
lemmas pde_ref_simps = pde_ref_def[split_simps ARM_Structs_A.pde.split]
pde_ref2_def[split_simps ARM_Structs_A.pde.split]
lemmas pde_ref_simps = pde_ref_def[split_simps Arch_Structs_A.pde.split]
pde_ref2_def[split_simps Arch_Structs_A.pde.split]
lemma set_asid_pool_st_vrefs[wp]:
"\<lbrace>\<lambda>s. P ((state_vrefs s) (p := (\<lambda>(r, p). (p, VSRef (ucast r)
@ -1336,8 +1336,6 @@ lemma update_cap_obj_refs_subset:
apply (case_tac cap,
simp_all add: update_cap_data_closedform
split: split_if_asm)
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all add: aobj_ref_cases arch_update_cap_data_def)
done
(* FIXME: move *)
@ -1378,13 +1376,13 @@ lemma update_cap_cap_auth_conferred_subset:
lemma update_cap_cli:
"cap_links_irq aag l (update_cap_data b w cap) = cap_links_irq aag l cap"
unfolding update_cap_data_def
unfolding update_cap_data_def arch_update_cap_data_def
apply (cases cap, simp_all add: is_cap_simps cli_no_irqs badge_update_def the_cnode_cap_def Let_def)
done
lemma untyped_range_update_cap_data [simp]:
"untyped_range (update_cap_data b w c) = untyped_range c"
unfolding update_cap_data_def
unfolding update_cap_data_def arch_update_cap_data_def
by (cases c, simp_all add: is_cap_simps badge_update_def Let_def the_cnode_cap_def)
end

88
proof/access-control/ExampleSystem.thy
View File

@ -187,7 +187,7 @@ where
(the_nat_to_bl_10 2)
\<mapsto> Structures_A.CNodeCap 6 undefined undefined,
(the_nat_to_bl_10 3)
\<mapsto> Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3063
\<mapsto> Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3063
(Some asid1_3063)),
(the_nat_to_bl_10 318)
\<mapsto> Structures_A.EndpointCap 9 0 {AllowSend} )"
@ -210,7 +210,7 @@ where
(the_nat_to_bl_10 2)
\<mapsto> Structures_A.CNodeCap 7 undefined undefined,
(the_nat_to_bl_10 3)
\<mapsto> Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3065
\<mapsto> Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3065
(Some asid1_3065)),
(the_nat_to_bl_10 318)
\<mapsto> Structures_A.EndpointCap 9 0 {AllowRecv}) "
@ -232,22 +232,22 @@ where
text {* UT1's VSpace (PageDirectory)*}
definition
pt1_3072 :: "word8 \<Rightarrow> ARM_Structs_A.pte "
pt1_3072 :: "word8 \<Rightarrow> Arch_Structs_A.pte "
where
"pt1_3072 \<equiv> (\<lambda>_. ARM_Structs_A.InvalidPTE)"
"pt1_3072 \<equiv> (\<lambda>_. Arch_Structs_A.InvalidPTE)"
definition
obj1_3072 :: Structures_A.kernel_object
where
"obj1_3072 \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageTable pt1_3072)"
"obj1_3072 \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageTable pt1_3072)"
definition
pd1_3063 :: "12 word \<Rightarrow> ARM_Structs_A.pde "
pd1_3063 :: "12 word \<Rightarrow> Arch_Structs_A.pde "
where
"pd1_3063 \<equiv>
(\<lambda>_. ARM_Structs_A.InvalidPDE)
(0 := ARM_Structs_A.PageTablePDE
(\<lambda>_. Arch_Structs_A.InvalidPDE)
(0 := Arch_Structs_A.PageTablePDE
(Platform.addrFromPPtr 3072)
undefined
undefined )"
@ -258,31 +258,31 @@ if it's right *)
definition
obj1_3063 :: Structures_A.kernel_object
where
"obj1_3063 \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageDirectory pd1_3063)"
"obj1_3063 \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageDirectory pd1_3063)"
text {* T1's VSpace (PageDirectory)*}
definition
pt1_3077 :: "word8 \<Rightarrow> ARM_Structs_A.pte "
pt1_3077 :: "word8 \<Rightarrow> Arch_Structs_A.pte "
where
"pt1_3077 \<equiv>
(\<lambda>_. ARM_Structs_A.InvalidPTE)"
(\<lambda>_. Arch_Structs_A.InvalidPTE)"
definition
obj1_3077 :: Structures_A.kernel_object
where
"obj1_3077 \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageTable pt1_3077)"
"obj1_3077 \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageTable pt1_3077)"
definition
pd1_3065 :: "12 word \<Rightarrow> ARM_Structs_A.pde "
pd1_3065 :: "12 word \<Rightarrow> Arch_Structs_A.pde "
where
"pd1_3065 \<equiv>
(\<lambda>_. ARM_Structs_A.InvalidPDE)
(0 := ARM_Structs_A.PageTablePDE
(\<lambda>_. Arch_Structs_A.InvalidPDE)
(0 := Arch_Structs_A.PageTablePDE
(Platform.addrFromPPtr 3077)
undefined
undefined )"
@ -293,7 +293,7 @@ if it's right *)
definition
obj1_3065 :: Structures_A.kernel_object
where
"obj1_3065 \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageDirectory pd1_3065)"
"obj1_3065 \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageDirectory pd1_3065)"
text {* UT1's tcb *}
@ -305,7 +305,7 @@ where
Structures_A.TCB \<lparr>
tcb_ctable = Structures_A.CNodeCap 6 undefined undefined ,
tcb_vtable = Structures_A.ArchObjectCap
(ARM_Structs_A.PageDirectoryCap 3063 (Some asid1_3063)),
(Arch_Structs_A.PageDirectoryCap 3063 (Some asid1_3063)),
tcb_reply = Structures_A.ReplyCap 3079 True, (* master reply cap to itself *)
tcb_caller = Structures_A.NullCap,
tcb_ipcframe = Structures_A.NullCap,
@ -326,7 +326,7 @@ where
Structures_A.TCB \<lparr>
tcb_ctable = Structures_A.CNodeCap 7 undefined undefined ,
tcb_vtable = Structures_A.ArchObjectCap
(ARM_Structs_A.PageDirectoryCap 3065 (Some asid1_3065)),
(Arch_Structs_A.PageDirectoryCap 3065 (Some asid1_3065)),
tcb_reply = Structures_A.ReplyCap 3080 True, (* master reply cap to itself *)
tcb_caller = Structures_A.NullCap,
tcb_ipcframe = Structures_A.NullCap,
@ -496,19 +496,19 @@ lemma s1_caps_of_state :
(p,cap) \<in>
{ ((6::obj_ref,(the_nat_to_bl_10 1)), Structures_A.ThreadCap 3079),
((6::obj_ref,(the_nat_to_bl_10 2)), Structures_A.CNodeCap 6 undefined undefined),
((6::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3063 (Some asid1_3063))),
((6::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3063 (Some asid1_3063))),
((6::obj_ref,(the_nat_to_bl_10 318)),Structures_A.EndpointCap 9 0 {AllowSend}),
((7::obj_ref,(the_nat_to_bl_10 1)), Structures_A.ThreadCap 3080),
((7::obj_ref,(the_nat_to_bl_10 2)), Structures_A.CNodeCap 7 undefined undefined),
((7::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3065 (Some asid1_3065))),
((7::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3065 (Some asid1_3065))),
((7::obj_ref,(the_nat_to_bl_10 318)),Structures_A.EndpointCap 9 0 {AllowRecv}) ,
((3079::obj_ref, (tcb_cnode_index 0)), Structures_A.CNodeCap 6 undefined undefined ),
((3079::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3063 (Some asid1_3063))),
((3079::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3063 (Some asid1_3063))),
((3079::obj_ref, (tcb_cnode_index 2)), Structures_A.ReplyCap 3079 True),
((3079::obj_ref, (tcb_cnode_index 3)), Structures_A.NullCap),
((3079::obj_ref, (tcb_cnode_index 4)), Structures_A.NullCap),
((3080::obj_ref, (tcb_cnode_index 0)), Structures_A.CNodeCap 7 undefined undefined ),
((3080::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3065 (Some asid1_3065))),
((3080::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3065 (Some asid1_3065))),
((3080::obj_ref, (tcb_cnode_index 2)), Structures_A.ReplyCap 3080 True),
((3080::obj_ref, (tcb_cnode_index 3)), Structures_A.NullCap),
((3080::obj_ref, (tcb_cnode_index 4)), Structures_A.NullCap)} "
@ -727,7 +727,7 @@ where
(the_nat_to_bl_10 2)
\<mapsto> Structures_A.CNodeCap 6 undefined undefined,
(the_nat_to_bl_10 3)
\<mapsto> Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3063
\<mapsto> Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3063
(Some asid2_3063)),
(the_nat_to_bl_10 4)
\<mapsto> Structures_A.CNodeCap 5 undefined undefined )"
@ -750,7 +750,7 @@ where
(the_nat_to_bl_10 2)
\<mapsto> Structures_A.CNodeCap 7 undefined undefined,
(the_nat_to_bl_10 3)
\<mapsto> Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3065
\<mapsto> Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3065
(Some asid2_3065)),
(the_nat_to_bl_10 4)
\<mapsto> Structures_A.CNodeCap 5 undefined undefined) "
@ -772,22 +772,22 @@ where
text {* UT2's VSpace (PageDirectory)*}
definition
pt2_3072 :: "word8 \<Rightarrow> ARM_Structs_A.pte "
pt2_3072 :: "word8 \<Rightarrow> Arch_Structs_A.pte "
where
"pt2_3072 \<equiv> (\<lambda>_. ARM_Structs_A.InvalidPTE)"
"pt2_3072 \<equiv> (\<lambda>_. Arch_Structs_A.InvalidPTE)"
definition
obj2_3072 :: Structures_A.kernel_object
where
"obj2_3072 \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageTable pt2_3072)"
"obj2_3072 \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageTable pt2_3072)"
definition
pd2_3063 :: "12 word \<Rightarrow> ARM_Structs_A.pde "
pd2_3063 :: "12 word \<Rightarrow> Arch_Structs_A.pde "
where
"pd2_3063 \<equiv>
(\<lambda>_. ARM_Structs_A.InvalidPDE)
(0 := ARM_Structs_A.PageTablePDE
(\<lambda>_. Arch_Structs_A.InvalidPDE)
(0 := Arch_Structs_A.PageTablePDE
(Platform.addrFromPPtr 3072)
undefined
undefined )"
@ -798,30 +798,30 @@ if it's right *)
definition
obj2_3063 :: Structures_A.kernel_object
where
"obj2_3063 \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageDirectory pd2_3063)"
"obj2_3063 \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageDirectory pd2_3063)"
text {* T1's VSpace (PageDirectory)*}
definition
pt2_3077 :: "word8 \<Rightarrow> ARM_Structs_A.pte "
pt2_3077 :: "word8 \<Rightarrow> Arch_Structs_A.pte "
where
"pt2_3077 \<equiv>
(\<lambda>_. ARM_Structs_A.InvalidPTE)"
(\<lambda>_. Arch_Structs_A.InvalidPTE)"
definition
obj2_3077 :: Structures_A.kernel_object
where
"obj2_3077 \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageTable pt2_3077)"
"obj2_3077 \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageTable pt2_3077)"
definition
pd2_3065 :: "12 word \<Rightarrow> ARM_Structs_A.pde "
pd2_3065 :: "12 word \<Rightarrow> Arch_Structs_A.pde "
where
"pd2_3065 \<equiv>
(\<lambda>_. ARM_Structs_A.InvalidPDE)
(0 := ARM_Structs_A.PageTablePDE
(\<lambda>_. Arch_Structs_A.InvalidPDE)
(0 := Arch_Structs_A.PageTablePDE
(Platform.addrFromPPtr 3077)
undefined
undefined )"
@ -832,7 +832,7 @@ if it's right *)
definition
obj2_3065 :: Structures_A.kernel_object
where
"obj2_3065 \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageDirectory pd2_3065)"
"obj2_3065 \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageDirectory pd2_3065)"
text {* UT1's tcb *}
@ -844,7 +844,7 @@ where
Structures_A.TCB \<lparr>
tcb_ctable = Structures_A.CNodeCap 6 undefined undefined ,
tcb_vtable = Structures_A.ArchObjectCap
(ARM_Structs_A.PageDirectoryCap 3063 (Some asid2_3063)),
(Arch_Structs_A.PageDirectoryCap 3063 (Some asid2_3063)),
tcb_reply = Structures_A.ReplyCap 3079 True, (* master reply cap to itself *)
tcb_caller = Structures_A.NullCap,
tcb_ipcframe = Structures_A.NullCap,
@ -865,7 +865,7 @@ where
Structures_A.TCB \<lparr>
tcb_ctable = Structures_A.CNodeCap 7 undefined undefined ,
tcb_vtable = Structures_A.ArchObjectCap
(ARM_Structs_A.PageDirectoryCap 3065 (Some asid2_3065)),
(Arch_Structs_A.PageDirectoryCap 3065 (Some asid2_3065)),
tcb_reply = Structures_A.ReplyCap 3080 True, (* master reply cap to itself *)
tcb_caller = Structures_A.NullCap,
tcb_ipcframe = Structures_A.NullCap,
@ -1008,19 +1008,19 @@ lemma s2_caps_of_state :
(p,cap) \<in>
{ ((6::obj_ref,(the_nat_to_bl_10 1)), Structures_A.ThreadCap 3079),
((6::obj_ref,(the_nat_to_bl_10 2)), Structures_A.CNodeCap 6 undefined undefined),
((6::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3063 (Some asid2_3063))),
((6::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3063 (Some asid2_3063))),
((6::obj_ref,(the_nat_to_bl_10 4)), Structures_A.CNodeCap 5 undefined undefined),
((7::obj_ref,(the_nat_to_bl_10 1)), Structures_A.ThreadCap 3080),
((7::obj_ref,(the_nat_to_bl_10 2)), Structures_A.CNodeCap 7 undefined undefined),
((7::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3065 (Some asid2_3065))),
((7::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3065 (Some asid2_3065))),
((7::obj_ref,(the_nat_to_bl_10 4)), Structures_A.CNodeCap 5 undefined undefined),
((3079::obj_ref, (tcb_cnode_index 0)), Structures_A.CNodeCap 6 undefined undefined ),
((3079::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3063 (Some asid2_3063))),
((3079::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3063 (Some asid2_3063))),
((3079::obj_ref, (tcb_cnode_index 2)), Structures_A.ReplyCap 3079 True),
((3079::obj_ref, (tcb_cnode_index 3)), Structures_A.NullCap),
((3079::obj_ref, (tcb_cnode_index 4)), Structures_A.NullCap),
((3080::obj_ref, (tcb_cnode_index 0)), Structures_A.CNodeCap 7 undefined undefined ),
((3080::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap 3065 (Some asid2_3065))),
((3080::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap 3065 (Some asid2_3065))),
((3080::obj_ref, (tcb_cnode_index 2)), Structures_A.ReplyCap 3080 True),
((3080::obj_ref, (tcb_cnode_index 3)), Structures_A.NullCap),
((3080::obj_ref, (tcb_cnode_index 4)), Structures_A.NullCap)} "

2
proof/access-control/Finalise_AC.thy
View File

@ -797,7 +797,7 @@ lemma arch_recycle_cap_respects:
cap_aligned_def is_cap_simps valid_cap_def
split: arch_cap.split_asm)
apply (fastforce simp: cap_links_asid_slot_def label_owns_asid_slot_def intro: pas_refined_Control_into_is_subject_asid)
apply (fastforce simp: has_recycle_rights_def vspace_cap_rights_to_auth_def pageBitsForSize_def split: vmpage_size.split)
subgoal by (fastforce simp: has_recycle_rights_def arch_has_recycle_rights_def vspace_cap_rights_to_auth_def pageBitsForSize_def split: vmpage_size.split)
apply (rename_tac word option)
apply (subgoal_tac
"(\<forall>v\<in>List.set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. is_subject aag (v && ~~ mask pt_bits)) \<and>

3
proof/access-control/Retype_AC.thy
View File

@ -100,6 +100,9 @@ lemma Suc_0_lt_cases:
apply (auto simp add: not_less le_Suc_eq)
done
lemmas upto_enum_step_shift_red =
upto_enum_step_shift_red[where 'a=32, simplified, simplified word_bits_def[symmetric, simplified]]
lemma clearMemory_respects:
"\<lbrace>\<lambda> a. integrity aag X st (s\<lparr>machine_state := a\<rparr>) \<and>
is_aligned ptr sz \<and> sz < word_bits \<and> 2 \<le> sz \<and>

2
proof/infoflow/ADT_IF.thy
View File

@ -1347,7 +1347,7 @@ definition
where
"check_active_irq_A_if \<equiv> {((tc, s), irq, (tc', s')). ((irq, tc'), s') \<in> fst (check_active_irq_if tc s)}"
abbreviation internal_state_if :: "((ARMMachineTypes.register \<Rightarrow> 32 word) \<times> 'a) \<times> sys_mode
abbreviation internal_state_if :: "((MachineTypes.register \<Rightarrow> 32 word) \<times> 'a) \<times> sys_mode
\<Rightarrow> 'a" where
"internal_state_if \<equiv> \<lambda>s. (snd (fst s))"

13
proof/infoflow/Arch_IF.thy
View File

@ -810,9 +810,9 @@ lemma unmap_page_reads_respects:
store_pde_reads_respects[simplified] flush_page_reads_respects
find_pd_for_asid_reads_respects find_pd_for_asid_pd_slot_authorised
mapM_ev''[
where m = "(\<lambda>a. store_pte a ARM_Structs_A.pte.InvalidPTE)"
where m = "(\<lambda>a. store_pte a Arch_Structs_A.pte.InvalidPTE)"
and P = "\<lambda>x s. is_subject aag (x && ~~ mask pt_bits)"]
mapM_ev''[where m = "(\<lambda>a. store_pde a ARM_Structs_A.pde.InvalidPDE)"
mapM_ev''[where m = "(\<lambda>a. store_pde a Arch_Structs_A.pde.InvalidPDE)"
and P = "\<lambda>x s. is_subject aag (x && ~~ mask pd_bits)"]
| wpc
@ -2311,10 +2311,10 @@ lemma decode_arch_invocation_authorised_for_globals:
apply (cases cap, simp_all)
-- "PageCap"
apply (clarsimp simp: valid_cap_simps cli_no_irqs)
apply (cases "invocation_type label"; simp add: isPageFlush_def isPDFlush_def)
apply (cases "invocation_type label";(rename_tac arch, case_tac arch; simp add: isPageFlushLabel_def isPDFlushLabel_def))
-- "Map"
apply (rename_tac word cap_rights vmpage_size option)
apply(clarsimp simp: isPageFlush_def isPDFlush_def | rule conjI)+
apply (rename_tac word cap_rights vmpage_size option arch)
apply(clarsimp simp: isPageFlushLabel_def isPDFlushLabel_def | rule conjI)+
apply(drule diminished_cte_wp_at_valid_cap)
apply(clarsimp simp: invs_def valid_state_def)
apply(simp add: valid_cap_def)
@ -2347,8 +2347,7 @@ lemma decode_arch_invocation_authorised_for_globals:
apply(drule diminished_PageDirectoryCapD)
apply(clarsimp simp: cap_range_def)
apply(simp)
apply(fastforce)
done
by(fastforce)
lemma as_user_valid_ko_at_arm[wp]:

52
proof/infoflow/Example_Valid_State.thy
View File

@ -383,7 +383,7 @@ where
(the_nat_to_bl_10 2)
\<mapsto> Structures_A.CNodeCap Low_cnode_ptr 10 (the_nat_to_bl_10 2),
(the_nat_to_bl_10 3)
\<mapsto> Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap Low_pd_ptr
\<mapsto> Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap Low_pd_ptr
(Some Low_asid)),
(the_nat_to_bl_10 318)
\<mapsto> Structures_A.NotificationCap ntfn_ptr 0 {AllowSend} )"
@ -410,7 +410,7 @@ lemma in_ran_If [simp]:
lemma Low_caps_ran:
"ran Low_caps = {Structures_A.ThreadCap Low_tcb_ptr,
Structures_A.CNodeCap Low_cnode_ptr 10 (the_nat_to_bl_10 2),
Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap Low_pd_ptr
Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap Low_pd_ptr
(Some Low_asid)),
Structures_A.NotificationCap ntfn_ptr 0 {AllowSend},
Structures_A.NullCap}"
@ -434,7 +434,7 @@ where
(the_nat_to_bl_10 2)
\<mapsto> Structures_A.CNodeCap High_cnode_ptr 10 (the_nat_to_bl_10 2),
(the_nat_to_bl_10 3)
\<mapsto> Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap High_pd_ptr
\<mapsto> Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap High_pd_ptr
(Some High_asid)),
(the_nat_to_bl_10 318)
\<mapsto> Structures_A.NotificationCap ntfn_ptr 0 {AllowRecv}) "
@ -447,7 +447,7 @@ where
lemma High_caps_ran:
"ran High_caps = {Structures_A.ThreadCap High_tcb_ptr,
Structures_A.CNodeCap High_cnode_ptr 10 (the_nat_to_bl_10 2),
Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap High_pd_ptr
Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap High_pd_ptr
(Some High_asid)),
Structures_A.NotificationCap ntfn_ptr 0 {AllowRecv},
Structures_A.NullCap}"
@ -500,23 +500,23 @@ where
text {* Low's VSpace (PageDirectory)*}
definition
Low_pt' :: "word8 \<Rightarrow> ARM_Structs_A.pte "
Low_pt' :: "word8 \<Rightarrow> Arch_Structs_A.pte "
where
"Low_pt' \<equiv> (\<lambda>_. ARM_Structs_A.InvalidPTE)
(0 := ARM_Structs_A.SmallPagePTE shared_page_ptr {} vm_read_write)"
"Low_pt' \<equiv> (\<lambda>_. Arch_Structs_A.InvalidPTE)
(0 := Arch_Structs_A.SmallPagePTE shared_page_ptr {} vm_read_write)"
definition
Low_pt :: Structures_A.kernel_object
where
"Low_pt \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageTable Low_pt')"
"Low_pt \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageTable Low_pt')"
definition
Low_pd' :: "12 word \<Rightarrow> ARM_Structs_A.pde "
Low_pd' :: "12 word \<Rightarrow> Arch_Structs_A.pde "
where
"Low_pd' \<equiv>
global_pd
(0 := ARM_Structs_A.PageTablePDE
(0 := Arch_Structs_A.PageTablePDE
(Platform.addrFromPPtr Low_pt_ptr)
{}
undefined )"
@ -527,32 +527,32 @@ if it's right *)
definition
Low_pd :: Structures_A.kernel_object
where
"Low_pd \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageDirectory Low_pd')"
"Low_pd \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageDirectory Low_pd')"
text {* High's VSpace (PageDirectory)*}
definition
High_pt' :: "word8 \<Rightarrow> ARM_Structs_A.pte "
High_pt' :: "word8 \<Rightarrow> Arch_Structs_A.pte "
where
"High_pt' \<equiv>
(\<lambda>_. ARM_Structs_A.InvalidPTE)
(0 := ARM_Structs_A.SmallPagePTE shared_page_ptr {} vm_read_only)"
(\<lambda>_. Arch_Structs_A.InvalidPTE)
(0 := Arch_Structs_A.SmallPagePTE shared_page_ptr {} vm_read_only)"
definition
High_pt :: Structures_A.kernel_object
where
"High_pt \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageTable High_pt')"
"High_pt \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageTable High_pt')"
definition
High_pd' :: "12 word \<Rightarrow> ARM_Structs_A.pde "
High_pd' :: "12 word \<Rightarrow> Arch_Structs_A.pde "
where
"High_pd' \<equiv>
global_pd
(0 := ARM_Structs_A.PageTablePDE
(0 := Arch_Structs_A.PageTablePDE
(Platform.addrFromPPtr High_pt_ptr)
{}
undefined )"
@ -563,7 +563,7 @@ if it's right *)
definition
High_pd :: Structures_A.kernel_object
where
"High_pd \<equiv> Structures_A.ArchObj (ARM_Structs_A.PageDirectory High_pd')"
"High_pd \<equiv> Structures_A.ArchObj (Arch_Structs_A.PageDirectory High_pd')"
text {* Low's tcb *}
@ -575,7 +575,7 @@ where
Structures_A.TCB \<lparr>
tcb_ctable = Structures_A.CNodeCap Low_cnode_ptr 10 (the_nat_to_bl_10 2),
tcb_vtable = Structures_A.ArchObjectCap
(ARM_Structs_A.PageDirectoryCap Low_pd_ptr (Some Low_asid)),
(Arch_Structs_A.PageDirectoryCap Low_pd_ptr (Some Low_asid)),
tcb_reply = Structures_A.ReplyCap Low_tcb_ptr True, (* master reply cap to itself *)
tcb_caller = Structures_A.NullCap,
tcb_ipcframe = Structures_A.NullCap,
@ -603,7 +603,7 @@ where
Structures_A.TCB \<lparr>
tcb_ctable = Structures_A.CNodeCap High_cnode_ptr 10 (the_nat_to_bl_10 2) ,
tcb_vtable = Structures_A.ArchObjectCap
(ARM_Structs_A.PageDirectoryCap High_pd_ptr (Some High_asid)),
(Arch_Structs_A.PageDirectoryCap High_pd_ptr (Some High_asid)),
tcb_reply = Structures_A.ReplyCap High_tcb_ptr True, (* master reply cap to itself *)
tcb_caller = Structures_A.NullCap,
tcb_ipcframe = Structures_A.NullCap,
@ -933,21 +933,21 @@ lemma s0_caps_of_state :
(p,cap) \<in>
{ ((Low_cnode_ptr::obj_ref,(the_nat_to_bl_10 1)), Structures_A.ThreadCap Low_tcb_ptr),
((Low_cnode_ptr::obj_ref,(the_nat_to_bl_10 2)), Structures_A.CNodeCap Low_cnode_ptr 10 (the_nat_to_bl_10 2)),
((Low_cnode_ptr::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap Low_pd_ptr (Some Low_asid))),
((Low_cnode_ptr::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap Low_pd_ptr (Some Low_asid))),
((Low_cnode_ptr::obj_ref,(the_nat_to_bl_10 318)),Structures_A.NotificationCap ntfn_ptr 0 {AllowSend}),
((High_cnode_ptr::obj_ref,(the_nat_to_bl_10 1)), Structures_A.ThreadCap High_tcb_ptr),
((High_cnode_ptr::obj_ref,(the_nat_to_bl_10 2)), Structures_A.CNodeCap High_cnode_ptr 10 (the_nat_to_bl_10 2)),
((High_cnode_ptr::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap High_pd_ptr (Some High_asid))),
((High_cnode_ptr::obj_ref,(the_nat_to_bl_10 3)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap High_pd_ptr (Some High_asid))),
((High_cnode_ptr::obj_ref,(the_nat_to_bl_10 318)),Structures_A.NotificationCap ntfn_ptr 0 {AllowRecv}) ,
((Silc_cnode_ptr::obj_ref,(the_nat_to_bl_10 2)),Structures_A.CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl_10 2)),
((Silc_cnode_ptr::obj_ref,(the_nat_to_bl_10 318)),Structures_A.NotificationCap ntfn_ptr 0 {AllowSend}),
((Low_tcb_ptr::obj_ref, (tcb_cnode_index 0)), Structures_A.CNodeCap Low_cnode_ptr 10 (the_nat_to_bl_10 2)),
((Low_tcb_ptr::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap Low_pd_ptr (Some Low_asid))),
((Low_tcb_ptr::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap Low_pd_ptr (Some Low_asid))),
((Low_tcb_ptr::obj_ref, (tcb_cnode_index 2)), Structures_A.ReplyCap Low_tcb_ptr True),
((Low_tcb_ptr::obj_ref, (tcb_cnode_index 3)), Structures_A.NullCap),
((Low_tcb_ptr::obj_ref, (tcb_cnode_index 4)), Structures_A.NullCap),
((High_tcb_ptr::obj_ref, (tcb_cnode_index 0)), Structures_A.CNodeCap High_cnode_ptr 10 (the_nat_to_bl_10 2)),
((High_tcb_ptr::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap High_pd_ptr (Some High_asid))),
((High_tcb_ptr::obj_ref, (tcb_cnode_index 1)), Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap High_pd_ptr (Some High_asid))),
((High_tcb_ptr::obj_ref, (tcb_cnode_index 2)), Structures_A.ReplyCap High_tcb_ptr True),
((High_tcb_ptr::obj_ref, (tcb_cnode_index 3)), Structures_A.NullCap),
((High_tcb_ptr::obj_ref, (tcb_cnode_index 4)), Structures_A.NullCap)} "
@ -1599,11 +1599,11 @@ lemma valid_kernel_mappings_s0[simp]:
"valid_kernel_mappings s0_internal"
apply (clarsimp simp: valid_kernel_mappings_def s0_internal_def ran_def
valid_kernel_mappings_if_pd_def split: Structures_A.kernel_object.splits
ARM_Structs_A.arch_kernel_obj.splits)
Arch_Structs_A.arch_kernel_obj.splits)
apply (drule kh0_SomeD)
apply (clarsimp simp: arch_state0_def kernel_mapping_slots_def)
apply (erule disjE | simp add: pde_ref_def s0_ptr_defs kh0_obj_def High_pd'_def Low_pd'_def
split: split_if_asm ARM_Structs_A.pde.splits)+
split: split_if_asm Arch_Structs_A.pde.splits)+
done
lemma equal_kernel_mappings_s0[simp]:

9
proof/infoflow/FinalCaps.thy
View File

@ -692,8 +692,7 @@ lemma weak_derived_overlaps':
apply simp
apply(simp add: copy_of_def split: split_if_asm add: same_object_as_def split: cap.splits)
apply((case_tac cap; simp)+)[5]
apply(simp split: arch_cap.splits cap.splits)
apply (rename_tac arch_cap, case_tac arch_cap; simp)+
subgoal for arch1 arch2 by (cases arch1; cases arch2; simp)
done
@ -2912,8 +2911,7 @@ lemma same_object_as_cap_points_to_label:
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
apply(simp split: arch_cap.splits cap.splits)
apply(rename_tac arch, case_tac arch; simp)+
subgoal for arch1 arch2 by (cases arch1; cases arch2; simp)
done
lemma same_object_as_slots_holding_overlapping_caps:
@ -2926,8 +2924,7 @@ lemma same_object_as_slots_holding_overlapping_caps:
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
apply(simp split: arch_cap.splits cap.splits)
apply(rename_tac arch, case_tac arch; simp)+
subgoal for arch1 arch2 by (cases arch1; cases arch2; simp)
done
lemma checked_cap_insert_silc_inv:

2
proof/infoflow/Ipc_IF.thy
View File

@ -775,7 +775,7 @@ lemma send_signal_reads_respects:
intro!: BlockedOnReceive_inj)
apply assumption
apply distinct_subgoals
apply fold_subgoals
apply (fold_subgoals (prefix))
apply (frule st_tcb_at_tcb_at)
subgoal bound_ntfn premises prems for st s ntfn x sta
prefer 2

6
proof/infoflow/Retype_IF.thy
View File

@ -422,10 +422,12 @@ lemma ptr_range_memE:
by(clarsimp simp: ptr_range_def)
lemma is_aligned_2_upto_enum_step_mem:
fixes ptr :: "word32"
shows
"\<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits;
x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]\<rbrakk> \<Longrightarrow>
is_aligned x 2"
apply(clarsimp simp: upto_enum_step_shift_red[where us=2, simplified] word_size_def)
apply(clarsimp simp: upto_enum_step_shift_red[where us=2, simplified] word_size_def )
apply(erule aligned_add_aligned)
apply(rule is_alignedI)
apply(simp add: mult.commute)
@ -434,6 +436,8 @@ lemma is_aligned_2_upto_enum_step_mem:
(* TODO: cleanup this beautiful proof *)
lemma ptr_range_subset:
fixes ptr :: "word32"
shows
"\<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits < word_bits;
x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]\<rbrakk> \<Longrightarrow>
ptr_range x 2 \<subseteq> ptr_range ptr bits"