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

enable XN in abstract spec; update AInvs and Refine

This commit is contained in:
Gerwin Klein 2014-11-22 16:48:11 +11:00
parent 21e7e33878
commit 7e7d39c24e
23 changed files with 72 additions and 561 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

103
proof/invariant-abstract/ArchAcc_AI.thy
View File

@ -386,14 +386,12 @@ definition
Inl (pte, xs) \<Rightarrow>
\<lambda>s. xs \<noteq> [] \<and>
(\<forall>p \<in> set xs. (\<exists>\<rhd> (p && ~~ mask pt_bits) and pte_at p) s) \<and>
wellformed_pte pte \<and> valid_pte pte s \<and>
executable_pte pte
wellformed_pte pte \<and> valid_pte pte s
| Inr (pde, xs) \<Rightarrow>
\<lambda>s. xs \<noteq> [] \<and>
(\<forall>p \<in> set xs. (\<exists>\<rhd> (p && ~~ mask pd_bits) and pde_at p) s \<and>
ucast (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and>
wellformed_pde pde \<and> valid_pde pde s \<and>
executable_pde pde"
wellformed_pde pde \<and> valid_pde pde s"
crunch inv[wp]: get_master_pte P
crunch inv[wp]: get_master_pde P
@ -1141,19 +1139,7 @@ lemma set_pd_arch_objs_unmap:
done
lemma set_pd_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs and K (executable_arch_obj (PageDirectory pd'))\<rbrace>
set_pd p pd' \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
apply (simp add: set_pd_def)
apply (wp set_object_executable_arch_objs get_object_wp)
apply (fastforce simp: obj_at_def a_type_def
split: Structures_A.kernel_object.splits arch_kernel_obj.splits)
done
declare graph_of_None_update[simp]
declare graph_of_Some_update[simp]
@ -1342,17 +1328,6 @@ lemma set_pt_arch_objs [wp]:
done
lemma set_pt_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs and K (executable_arch_obj (ARM_Structs_A.PageTable pt))\<rbrace>
set_pt p pt
\<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
apply (simp add: set_pt_def)
apply (wp set_object_executable_arch_objs get_object_wp)
apply (clarsimp simp: obj_at_def)
apply (clarsimp simp: a_type_def split: Structures_A.kernel_object.splits arch_kernel_obj.splits)
done
lemma set_pt_vs_lookup [wp]:
"\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> set_pt p pt \<lbrace>\<lambda>x s. P (vs_lookup s)\<rbrace>"
unfolding set_pt_def set_object_def
@ -1719,8 +1694,7 @@ crunch valid_irq_states[wp]: set_pd "valid_irq_states"
(wp: crunch_wps)
lemma set_pt_invs:
"\<lbrace>invs and (%s. \<forall>i. wellformed_pte (pt i)) and
(%s. \<forall>i. executable_pte (pt i)) and
"\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pte (pt i)) and
(\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (ARM_Structs_A.PageTable pt) s) and
(\<lambda>s. \<exists>slot asid. caps_of_state s slot =
Some (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) \<and>
@ -1795,7 +1769,6 @@ lemmas invs_ran_asid_table = invs_valid_asid_table[THEN valid_asid_table_ran]
lemma store_pte_invs [wp]:
"\<lbrace>invs and (\<lambda>s. (\<exists>\<rhd>(p && ~~ mask pt_bits)) s \<longrightarrow> valid_pte pte s) and
(\<lambda>s. wellformed_pte pte) and
(\<lambda>s. executable_pte pte) and
(\<lambda>s. \<exists>slot asid. caps_of_state s slot =
Some (cap.ArchObjectCap
(arch_cap.PageTableCap (p && ~~ mask pt_bits) asid)) \<and>
@ -1812,11 +1785,8 @@ lemma store_pte_invs [wp]:
apply (wp dmo_invs set_pt_invs)
apply clarsimp
apply (intro conjI)
apply (drule invs_valid_objs)
apply (fastforce simp: valid_objs_def dom_def obj_at_def valid_obj_def)
apply clarsimp
apply (drule executable_arch_objsD, fastforce)
apply simp
apply (drule invs_valid_objs)
apply (fastforce simp: valid_objs_def dom_def obj_at_def valid_obj_def)
apply clarsimp
apply (drule (1) valid_arch_objsD, fastforce)
apply simp
@ -2019,16 +1989,6 @@ lemma set_asid_pool_arch_objs_unmap:
done
lemma set_asid_pool_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs and ko_at (ArchObj (ARM_Structs_A.ASIDPool ap')) p\<rbrace>
set_asid_pool p ap \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
apply (simp add: set_asid_pool_def)
apply (wp get_object_wp set_object_executable_arch_objs)
apply (clarsimp simp: obj_at_def)
apply (clarsimp simp: a_type_def split: Structures_A.kernel_object.splits arch_kernel_obj.splits)
done
lemma set_asid_pool_table_caps [wp]:
"\<lbrace>valid_table_caps\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_table_caps\<rbrace>"
apply (simp add: valid_table_caps_def)
@ -2267,7 +2227,6 @@ lemma set_asid_pool_invs_restrict:
set_asid_pool_arch_objs_unmap valid_irq_handlers_lift
set_asid_pool_vs_lookup_unmap set_asid_pool_restrict_asid_map)
apply simp
apply fastforce
done
@ -2782,8 +2741,7 @@ lemma create_mapping_entries_valid_slots [wp]:
and pspace_aligned and valid_global_objs
and \<exists>\<rhd> pd and page_directory_at pd and typ_at (AArch (AIntData sz)) (Platform.ptrFromPAddr base) and
K (is_aligned base pageBits \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and>
vm_rights \<in> valid_vm_rights) and
K (XNever \<notin> attrib)\<rbrace>
vm_rights \<in> valid_vm_rights)\<rbrace>
create_mapping_entries base vptr sz vm_rights attrib pd
\<lbrace>\<lambda>m. valid_slots m\<rbrace>, -"
apply (cases sz)
@ -2970,16 +2928,6 @@ lemma store_pde_arch_objs_unmap:
apply (simp add: graph_of_def split: split_if_asm)
done
lemma store_pde_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs
and K (executable_pde pde)\<rbrace>
store_pde p pde \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
apply (simp add: store_pde_def)
apply wp
apply clarsimp
apply (drule (1) executable_arch_objsD, fastforce)
done
(* FIXME: remove magic numbers in other lemmas, use in pde_at_aligned_vptr et al *)
lemma lookup_pd_slot_add_eq:
@ -3124,21 +3072,8 @@ lemma store_pte_valid_arch_objs[wp]:
apply auto
done
lemma store_pte_executable_arch_objs[wp]:
"\<lbrace>executable_arch_objs and K (executable_pte pte)\<rbrace>
store_pte p pte
\<lbrace>\<lambda>_. (executable_arch_objs)\<rbrace>"
unfolding store_pte_def
apply wp
apply clarsimp
apply (unfold executable_arch_objs_def)
apply (erule_tac x="p && ~~ mask pt_bits" in allE)
apply auto
done
crunch valid_arch [wp]: store_pte valid_arch_state
lemma set_pd_vs_lookup_unmap:
"\<lbrace>valid_vs_lookup and
obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p\<rbrace>
@ -3446,8 +3381,7 @@ lemma vs_refs_pages_subset2:
lemma set_pd_invs_unmap:
"\<lbrace>invs and (%s. \<forall>i. wellformed_pde (pd i)) and
(%s. \<forall>i. executable_pde (pd i)) and
"\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and
(\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (PageDirectory pd) s) and
obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p and
obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and
@ -3474,22 +3408,17 @@ lemma set_pd_invs_unmap:
lemma store_pde_invs_unmap:
"\<lbrace>invs and valid_pde pde and (%s. wellformed_pde pde)
and (%s. executable_pde pde)
"\<lbrace>invs and valid_pde pde and (\<lambda>s. wellformed_pde pde)
and K (ucast (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots)
and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s)
and K (pde = ARM_Structs_A.InvalidPDE)\<rbrace>
store_pde p pde \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: store_pde_def del: split_paired_Ex)
apply (wp dmo_invs set_pd_invs_unmap)
apply (wp set_pd_invs_unmap)
apply (clarsimp simp del: split_paired_Ex del: exE)
apply (rule conjI)
apply (drule invs_valid_objs)
apply (fastforce simp: valid_objs_def dom_def obj_at_def valid_obj_def)
apply (rule conjI)
apply clarsimp
apply (drule executable_arch_objsD, fastforce)
apply simp
apply (rule conjI)
apply clarsimp
apply (drule (1) valid_arch_objsD, fastforce)
@ -3508,11 +3437,6 @@ lemma store_word_offs_arch_objs :
by (wp|simp add: store_word_offs_def)+
lemma store_word_offs_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs\<rbrace> store_word_offs a b c \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
by (wp|simp add: store_word_offs_def)+
lemma store_pde_state_refs_of:
"\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>"
apply (simp add: store_pde_def set_pd_def set_object_def)
@ -3539,13 +3463,4 @@ lemma set_mrs_arch_objs:
done
lemma set_mrs_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs\<rbrace> set_mrs a b c \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
apply (simp add: set_mrs_def)
apply (wp mapM_wp' set_object_executable_arch_objs hoare_drop_imps
|wpc|simp add: zipWithM_x_mapM split_def split del: split_if)+
apply (clarsimp cong: if_cong)
done
end

4
proof/invariant-abstract/Arch_AI.thy
View File

@ -1424,10 +1424,6 @@ lemma diminished_pd_self:
apply (clarsimp simp: acap_rights_update_def split: cap.splits arch_cap.splits)
done
lemma XNever_attribs_from_word[simp]:
"XNever \<notin> attribs_from_word w"
by (simp add: attribs_from_word_def)
lemma cte_wp_at_page_cap_weaken:
"cte_wp_at (diminished (ArchObjectCap (PageCap word seta vmpage_size None))) slot s \<Longrightarrow>
cte_wp_at (\<lambda>a. \<exists>p R sz m. a = ArchObjectCap (PageCap p R sz m)) slot s"

7
proof/invariant-abstract/CNodeInv_AI.thy
View File

@ -2015,13 +2015,6 @@ crunch arch_objs [wp]: cap_move "valid_arch_objs"
crunch arch_objs [wp]: empty_slot "valid_arch_objs"
crunch executable_arch_objs [wp]: cap_swap "executable_arch_objs"
crunch executable_arch_objs [wp]: cap_move "executable_arch_objs"
crunch executable_arch_objs [wp]: empty_slot "executable_arch_objs"
crunch valid_global_objs [wp]: cap_swap "valid_global_objs"

8
proof/invariant-abstract/CSpace_AI.thy
View File

@ -3924,15 +3924,9 @@ lemma cap_insert_valid_global_refs[wp]:
crunch irq_node[wp]: cap_insert "\<lambda>s. P (interrupt_irq_node s)"
(wp: crunch_wps)
crunch arch_objs [wp]: cap_insert "valid_arch_objs"
(wp: crunch_wps simp: crunch_simps)
crunch executable_arch_objs [wp]: cap_insert "executable_arch_objs"
(wp: crunch_wps simp: crunch_simps)
crunch arch_caps[wp]: update_cdt "valid_arch_caps"
@ -5072,8 +5066,6 @@ crunch arch[wp]: setup_reply_master "valid_arch_state"
crunch arch_objs[wp]: setup_reply_master "valid_arch_objs"
crunch executable_arch_objs[wp]: setup_reply_master "executable_arch_objs"
lemma setup_reply_master_irq_handlers[wp]:
"\<lbrace>valid_irq_handlers and tcb_at t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>"

7
proof/invariant-abstract/Detype_AI.thy
View File

@ -871,13 +871,6 @@ proof (simp add: invs_def valid_state_def valid_pspace_def
apply (auto intro: valid_arch_obj)
done
have "executable_arch_objs s"
using invs by fastforce
thus "executable_arch_objs (detype (untyped_range cap) s)"
unfolding executable_arch_objs_def
apply (auto)
done
have unique_table_caps:
"\<And>cps P. unique_table_caps cps
\<Longrightarrow> unique_table_caps (\<lambda>x. if P x then None else cps x)"

32
proof/invariant-abstract/Finalise_AI.thy
View File

@ -1605,11 +1605,6 @@ lemma invalidate_tlb_by_asid_pspace_aligned:
crunch valid_arch_objs[wp]: invalidate_tlb_by_asid, page_table_mapped
"valid_arch_objs"
crunch executable_arch_objs[wp]: invalidate_tlb_by_asid, page_table_mapped
"executable_arch_objs"
crunch cte_wp_at[wp]: invalidate_tlb_by_asid, page_table_mapped
"\<lambda>s. P (cte_wp_at P' p s)"
@ -1670,16 +1665,6 @@ lemma mapM_x_store_pte_valid_arch_objs:
done
lemma mapM_x_store_pte_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs\<rbrace>
mapM_x (\<lambda>p. store_pte p ARM_Structs_A.InvalidPTE) pteptrs
\<lbrace>\<lambda>rv. executable_arch_objs\<rbrace>"
apply (rule hoare_strengthen_post)
apply (wp mapM_x_wp')
apply (fastforce simp: is_pt_cap_def)+
done
lemma mapM_x_swp_store_empty_table_set:
"\<lbrace>page_table_at p
and pspace_aligned
@ -2295,12 +2280,6 @@ lemma store_pde_arch_objs_invalid:
apply (simp add: pde_ref_def)
done
lemma store_pde_executable_arch_objs_invalid [wp]:
"\<lbrace>executable_arch_objs\<rbrace> store_pde p ARM_Structs_A.pde.InvalidPDE \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
apply (wp)
apply (simp)
done
lemma mapM_x_store_pde_InvalidPDE_empty2:
"\<lbrace>invs and (\<lambda>s. word \<notin> global_refs s) and K (is_aligned word pd_bits) and K (slots = (map (\<lambda>a. (a << 2) + word) [0.e.(kernel_base >> 20) - 1])) \<rbrace>
mapM_x (\<lambda>x. store_pde x ARM_Structs_A.pde.InvalidPDE) slots
@ -2743,17 +2722,6 @@ lemma set_asid_pool_empty_table_objs:
apply simp
done
lemma set_asid_pool_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs and asid_pool_at p\<rbrace>
set_asid_pool p empty
\<lbrace>\<lambda>rv. executable_arch_objs\<rbrace>"
apply (simp add: set_asid_pool_def)
apply (wp get_object_wp set_object_executable_arch_objs)
apply (clarsimp simp: obj_at_def)
apply (clarsimp simp: a_type_def split: Structures_A.kernel_object.splits arch_kernel_obj.splits)
done
lemma set_asid_pool_empty_table_lookup:
"\<lbrace>valid_vs_lookup and asid_pool_at p and
(\<lambda>s. \<exists>p'. caps_of_state s p' = Some (cap.ArchObjectCap (arch_cap.ASIDPoolCap p base)))\<rbrace>

3
proof/invariant-abstract/InterruptAcc_AI.thy
View File

@ -55,8 +55,7 @@ definition all_invs_but_valid_irq_states_for where
valid_asid_map and
valid_global_pd_mappings and
pspace_in_kernel_window and
cap_refs_in_kernel_window and cur_tcb and
executable_arch_objs"
cap_refs_in_kernel_window and cur_tcb"
lemma dmo_maskInterrupt_invs:
"\<lbrace>all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)\<rbrace>

100
proof/invariant-abstract/Invariants_AI.thy
View File

@ -677,13 +677,13 @@ where
\<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}. uses x = use)
\<and> (use = ArmVSpaceKernelWindow
\<or> use = ArmVSpaceDeviceWindow))
\<and> rghts = {} \<and> XNever \<notin> atts
\<and> rghts = {}
| ARM_Structs_A.LargePagePTE ptr atts rghts \<Rightarrow>
Platform.ptrFromPAddr ptr = (vref && ~~ mask (pageBitsForSize ARMLargePage))
\<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}. uses x = use)
\<and> (use = ArmVSpaceKernelWindow
\<or> use = ArmVSpaceDeviceWindow))
\<and> rghts = {} \<and> XNever \<notin> atts"
\<and> rghts = {}"
definition
valid_pt_kernel_mappings :: "vspace_ref \<Rightarrow> arm_vspace_region_uses \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
@ -709,12 +709,12 @@ where
\<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}. uses x = use)
\<and> (use = ArmVSpaceKernelWindow
\<or> use = ArmVSpaceDeviceWindow))
\<and> rghts = {} \<and> XNever \<notin> atts)
\<and> rghts = {})
| ARM_Structs_A.SuperSectionPDE ptr atts rghts \<Rightarrow>
(\<lambda>s. Platform.ptrFromPAddr ptr = (vref && ~~ mask (pageBitsForSize ARMSuperSection))
\<and> (\<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}.
uses x = ArmVSpaceKernelWindow)
\<and> rghts = {} \<and> XNever \<notin> atts)"
\<and> rghts = {})"
definition
valid_pd_kernel_mappings :: "arm_vspace_region_uses \<Rightarrow> 'z::state_ext state
@ -1286,37 +1286,6 @@ definition
"valid_machine_state \<equiv>
\<lambda>s. \<forall>p. in_user_frame p (s::'z::state_ext state) \<or> underlying_memory (machine_state s) p = 0"
definition
executable_pte :: "ARM_Structs_A.pte \<Rightarrow> bool"
where
"executable_pte pte \<equiv> case pte of
ARM_Structs_A.pte.LargePagePTE p attr r \<Rightarrow>
XNever \<notin> attr
| ARM_Structs_A.pte.SmallPagePTE p attr r \<Rightarrow>
XNever \<notin> attr
| _ \<Rightarrow> True"
definition
executable_pde :: "ARM_Structs_A.pde \<Rightarrow> bool"
where
"executable_pde pde \<equiv> case pde of
ARM_Structs_A.pde.SectionPDE p attr mw r \<Rightarrow> XNever \<notin> attr
| ARM_Structs_A.pde.SuperSectionPDE p attr r \<Rightarrow> XNever \<notin> attr
| _ \<Rightarrow> True"
definition
executable_arch_obj :: "arch_kernel_obj \<Rightarrow> bool"
where
"executable_arch_obj ao \<equiv> case ao of
PageTable pt \<Rightarrow> (\<forall>pte\<in>range pt. executable_pte pte)
| PageDirectory pd \<Rightarrow> (\<forall>pde\<in>range pd. executable_pde pde)
| _ \<Rightarrow> True"
definition
executable_arch_objs :: "'z::state_ext state \<Rightarrow> bool"
where
"executable_arch_objs \<equiv> \<lambda>s. \<forall>p ao. ko_at (ArchObj ao) p s \<longrightarrow> executable_arch_obj ao"
definition
valid_state :: "'z::state_ext state \<Rightarrow> bool"
where
@ -1342,8 +1311,7 @@ where
and valid_asid_map
and valid_global_pd_mappings
and pspace_in_kernel_window
and cap_refs_in_kernel_window
and executable_arch_objs"
and cap_refs_in_kernel_window"
definition
"ct_in_state test \<equiv> \<lambda>s. st_tcb_at test (cur_thread s) s"
@ -1432,7 +1400,6 @@ abbreviation(input)
and equal_kernel_mappings and valid_asid_map
and valid_global_pd_mappings
and pspace_in_kernel_window and cap_refs_in_kernel_window
and executable_arch_objs
and cur_tcb"
@ -1732,18 +1699,6 @@ lemmas
wellformed_arch_obj_simps[simp] =
wellformed_arch_obj_def[split_simps arch_kernel_obj.split]
lemmas
executable_pte_simps[simp] =
executable_pte_def[split_simps ARM_Structs_A.pte.split]
lemmas
executable_pde_simps[simp] =
executable_pde_def[split_simps ARM_Structs_A.pde.split]
lemmas
executable_arch_obj_simps[simp] =
executable_arch_obj_def[split_simps arch_kernel_obj.split]
lemma valid_objsI [intro]:
"(\<And>obj x. kheap s x = Some obj \<Longrightarrow> valid_obj x obj s) \<Longrightarrow> valid_objs s"
unfolding valid_objs_def by auto
@ -1872,24 +1827,6 @@ lemma valid_arch_objs_stateI:
apply (erule (3) vao)
done
lemma executable_arch_objsD:
"\<lbrakk> ko_at (ArchObj ao) p s; executable_arch_objs s \<rbrakk> \<Longrightarrow> executable_arch_obj ao"
by (fastforce simp add: executable_arch_objs_def)
(* should work for unmap and non-arch ops *)
lemma executable_arch_objs_stateI:
assumes 1: "executable_arch_objs s"
assumes vao: "\<And>p ref ao'.
\<lbrakk> \<forall>ao. ko_at (ArchObj ao) p s \<longrightarrow> executable_arch_obj ao;
ko_at (ArchObj ao') p s' \<rbrakk> \<Longrightarrow> executable_arch_obj ao'"
shows "executable_arch_objs s'"
using 1 unfolding executable_arch_objs_def
apply clarsimp
apply (rule vao)
apply fastforce
apply fastforce
done
lemma asid_pool_at_ko:
"asid_pool_at p s \<Longrightarrow> \<exists>pool. ko_at (ArchObj (ARM_Structs_A.ASIDPool pool)) p s"
apply (clarsimp simp: obj_at_def a_type_def)
@ -3338,10 +3275,6 @@ lemma valid_pd_kernel_mappings [iff]:
= valid_pd_kernel_mappings uses s"
by (rule ext, simp add: valid_pd_kernel_mappings_def)
lemma executable_arch_objs_update [iff]:
"executable_arch_objs (f s) = executable_arch_objs s"
by (simp add: executable_arch_objs_def)
end
locale arch_update_eq =
@ -4488,16 +4421,8 @@ lemma valid_arch_objsI [intro?]:
"(\<And>p ao. \<lbrakk> (\<exists>\<rhd> p) s; ko_at (ArchObj ao) p s \<rbrakk> \<Longrightarrow> valid_arch_obj ao s) \<Longrightarrow> valid_arch_objs s"
by (simp add: valid_arch_objs_def)
lemma executable_arch_objsI [intro?]:
"(\<And>p ao. \<lbrakk> ko_at (ArchObj ao) p s \<rbrakk> \<Longrightarrow> executable_arch_obj ao) \<Longrightarrow> executable_arch_objs s"
by (simp add: executable_arch_objs_def)
(* FIXME: duplicated with caps_of_state_valid_cap *)
lemma caps_of_state_valid:
"\<lbrakk> caps_of_state s p = Some cap; valid_objs s \<rbrakk> \<Longrightarrow> s \<turnstile> cap"
apply (drule caps_of_state_cteD)
apply (erule (1) cte_wp_valid_cap)
done
lemmas caps_of_state_valid = caps_of_state_valid_cap
lemma vs_lookup1_stateI2:
assumes 1: "(r \<rhd>1 r') s"
@ -4724,15 +4649,6 @@ lemma valid_arch_objs_lift:
hoare_convert_imp [OF y] valid_arch_obj_typ z)
done
lemma executable_arch_objs_lift:
assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
and y: "\<And>ao p. \<lbrace>\<lambda>s. \<not> ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> ko_at (ArchObj ao) p s\<rbrace>"
shows "\<lbrace>executable_arch_objs\<rbrace> f \<lbrace>\<lambda>rv. executable_arch_objs\<rbrace>"
apply (simp add: executable_arch_objs_def)
apply (wp hoare_vcg_all_lift
hoare_convert_imp [OF y] valid_arch_obj_typ z)
done
lemma valid_validate_vm_rights[simp]:
"validate_vm_rights rs \<in> valid_vm_rights"
and validate_vm_rights_subseteq[simp]:
@ -4884,10 +4800,6 @@ lemma invs_arch_objs [elim!]:
"invs s \<Longrightarrow> valid_arch_objs s"
by (simp add: invs_def valid_state_def)
lemma invs_executable_arch_objs [elim!]:
"invs s \<Longrightarrow> executable_arch_objs s"
by (simp add: invs_def valid_state_def)
lemma invs_valid_idle[elim!]:
"invs s \<Longrightarrow> valid_idle s"
by (fastforce simp: invs_def valid_state_def)

17
proof/invariant-abstract/Ipc_AI.thy
View File

@ -1058,23 +1058,12 @@ lemma transfer_caps_loop_irq_handlers[wp]:
crunch valid_arch_objs [wp]: set_extra_badge valid_arch_objs
crunch executable_arch_objs [wp]: set_extra_badge executable_arch_objs
lemma transfer_caps_loop_arch_objs[wp]:
"\<lbrace>valid_arch_objs\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
by (rule transfer_caps_loop_pres) wp
lemma transfer_caps_loop_executable_arch_objs[wp]:
"\<lbrace>executable_arch_objs\<rbrace>
transfer_caps_loop ep diminish buffer n caps slots mi
\<lbrace>\<lambda>rv. executable_arch_objs\<rbrace>"
by (rule transfer_caps_loop_pres) wp
crunch valid_arch_caps [wp]: set_extra_badge valid_arch_caps
@ -1910,10 +1899,6 @@ crunch arch_objs[wp]: do_ipc_transfer "valid_arch_objs"
(wp: crunch_wps simp: zipWithM_x_mapM crunch_simps)
crunch executable_arch_objs[wp]: do_ipc_transfer "executable_arch_objs"
(wp: crunch_wps simp: zipWithM_x_mapM crunch_simps)
lemmas set_mrs_valid_global_objs[wp]
= set_mrs_thread_set_dmo [OF thread_set_valid_globals do_machine_op_valid_global_objs]
@ -2756,8 +2741,6 @@ crunch irq_handlers[wp]: set_endpoint "valid_irq_handlers"
crunch arch_objs [wp]: setup_caller_cap "valid_arch_objs"
crunch executable_arch_objs [wp]: setup_caller_cap "executable_arch_objs"
crunch v_ker_map[wp]: setup_caller_cap "valid_kernel_mappings"
crunch eq_ker_map[wp]: setup_caller_cap "equal_kernel_mappings"

77
proof/invariant-abstract/KHeap_AI.thy
View File

@ -1464,67 +1464,6 @@ lemma set_cap_vs_lookup_pages [wp]:
done
lemma set_object_executable_arch_objs:
"\<lbrace>executable_arch_objs and typ_at (a_type ko) p and
(\<lambda>s. case ko of ArchObj ao \<Rightarrow> executable_arch_obj ao
| _ \<Rightarrow> True)\<rbrace>
set_object p ko
\<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
apply (simp add: executable_arch_objs_def)
apply (subst imp_conv_disj)+
apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift set_object_neg_lookup set_object_neg_ko)
apply (clarsimp simp: pred_neg_def obj_at_def)
apply fastforce
done
lemma set_ep_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs\<rbrace> set_endpoint p ep \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
unfolding set_endpoint_def
apply (wp set_object_executable_arch_objs get_object_wp)
apply (clarsimp simp: vs_refs_def obj_at_def a_type_def
split: Structures_A.kernel_object.splits)
done
lemma set_aep_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs\<rbrace> set_async_ep p aep \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
unfolding set_async_ep_def
apply (wp set_object_executable_arch_objs get_object_wp)
apply (clarsimp simp: vs_refs_def obj_at_def a_type_def
split: Structures_A.kernel_object.splits)
done
lemma sts_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs\<rbrace> set_thread_state p st \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
unfolding set_thread_state_def
apply (wp, simp, wp set_object_executable_arch_objs)
apply (fastforce simp: vs_refs_def obj_at_def a_type_def get_tcb_def
split: Structures_A.kernel_object.splits option.splits)
done
lemma thread_set_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs\<rbrace> thread_set f p \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
unfolding thread_set_def
apply (wp set_object_executable_arch_objs)
apply (fastforce simp: vs_refs_def obj_at_def a_type_def get_tcb_def
split: Structures_A.kernel_object.splits option.splits)
done
lemma set_cap_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs\<rbrace> set_cap cap p \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
unfolding set_cap_def split_def
apply (rule hoare_pre)
apply (wp set_object_executable_arch_objs get_object_wp
| wpc)+
apply (clarsimp simp: vs_refs_def obj_at_def simp del: fun_upd_apply)
apply (simp add: a_type_def wf_cs_upd)
done
lemma valid_irq_handlers_lift:
assumes x: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>"
assumes y: "\<And>P. \<lbrace>\<lambda>s. P (interrupt_states s)\<rbrace> f \<lbrace>\<lambda>rv s. P (interrupt_states s)\<rbrace>"
@ -2132,14 +2071,6 @@ lemma do_machine_op_arch_objs [wp]:
done
lemma do_machine_op_executable_arch_objs [wp]:
"\<lbrace>executable_arch_objs\<rbrace> do_machine_op f \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
apply (simp add: do_machine_op_def split_def)
apply wp
apply simp
done
lemma empty_table_lift:
assumes S: "\<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>_ s. P (S s)\<rbrace>"
assumes o: "\<And>P. \<lbrace>obj_at P p and Q\<rbrace> f \<lbrace>\<lambda>_. obj_at P p\<rbrace>"
@ -2174,14 +2105,6 @@ lemma as_user_arch_obj:
done
lemma as_user_executable_arch_obj:
"\<lbrace>executable_arch_objs\<rbrace> as_user f t \<lbrace>\<lambda>_. executable_arch_objs\<rbrace>"
apply (simp add: as_user_def)
apply (wp set_object_executable_arch_objs hoare_drop_imps|simp add: split_def)+
apply (clarsimp cong: if_cong)
done
lemma tcb_cap_valid_caps_of_stateD:
"\<And>P. \<lbrakk> caps_of_state s p = Some cap; valid_objs s \<rbrakk> \<Longrightarrow>
tcb_cap_valid cap p s"

6
proof/invariant-abstract/KernelInit_AI.thy
View File

@ -364,10 +364,8 @@ lemma invs_A:
apply (rule less_imp_le)
apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
apply (rule in_kernel_base|simp)+
apply (rule conjI)
apply (simp add: cap_refs_in_kernel_window_def caps_of_state_init_A_st_Null
valid_refs_def[unfolded cte_wp_at_caps_of_state])
apply (simp add: executable_arch_objs_def obj_at_def state_defs)
apply (simp add: cap_refs_in_kernel_window_def caps_of_state_init_A_st_Null
valid_refs_def[unfolded cte_wp_at_caps_of_state])
apply word_bitwise
done

45
proof/invariant-abstract/Retype_AI.thy
View File

@ -1389,8 +1389,7 @@ abbreviation(input)
and valid_arch_caps and valid_global_objs and valid_kernel_mappings
and valid_asid_map and valid_global_pd_mappings
and pspace_in_kernel_window and cap_refs_in_kernel_window
and cur_tcb and valid_ioc and valid_machine_state
and executable_arch_objs"
and cur_tcb and valid_ioc and valid_machine_state"
lemma all_invs_but_equal_kernel_mappings_restricted_eq:
@ -1696,8 +1695,6 @@ lemma store_pde_vms[wp]:
crunch valid_irq_states[wp]: store_pde "valid_irq_states"
crunch executable_arch_objs[wp]: get_pde executable_arch_objs
lemma copy_global_invs_mappings_restricted:
"\<lbrace>(\<lambda>s. all_invs_but_equal_kernel_mappings_restricted (insert pd S) s)
and (\<lambda>s. insert pd S \<inter> global_refs s = {})
@ -1735,11 +1732,6 @@ lemma copy_global_invs_mappings_restricted:
apply (simp add: valid_objs_def dom_def obj_at_def valid_obj_def)
apply (drule spec, erule impE, fastforce, clarsimp)
apply (clarsimp simp: obj_at_def empty_table_def kernel_vsrefs_def)
apply (rule conjI)
apply (clarsimp simp: obj_at_def empty_table_def kernel_vsrefs_def)
apply (drule executable_arch_objsD[rotated])
apply (fastforce simp: obj_at_def)
apply simp
apply clarsimp
apply (erule minus_one_helper5[rotated])
apply (simp add: pd_bits_def pageBits_def)
@ -3187,38 +3179,6 @@ lemma vms:
apply (rule_tac x=sz in exI, clarsimp simp: obj_at_def orthr)
done
lemma executable_arch_obj_default:
assumes tyunt: "ty \<noteq> Structures_A.apiobject_type.Untyped"
shows "ArchObj ao = default_object ty us \<Longrightarrow> executable_arch_obj ao"
apply (cases ty, simp_all add: default_object_def tyunt)
apply (simp add: default_arch_object_def split: aobject_type.splits)
done
lemma executable_arch_objs':
assumes ea: "executable_arch_objs s"
shows "executable_arch_objs s'"
proof
fix p ao
assume "ko_at (ArchObj ao) p s'"
hence "ko_at (ArchObj ao) p s \<or> ArchObj ao = default_object ty us"
by (simp add: ps_def obj_at_def s'_def split: split_if_asm)
moreover
{ assume "ArchObj ao = default_object ty us" with tyunt
have "executable_arch_obj ao" by (rule executable_arch_obj_default)
}
moreover
{ assume "ko_at (ArchObj ao) p s"
with ea
have "executable_arch_obj ao"
by (auto simp: vs_lookup' elim: executable_arch_objsD)
hence "executable_arch_obj ao"
apply (cases ao, simp_all add: obj_at_pres)
done
}
ultimately
show "executable_arch_obj ao" by blast
qed
lemma post_retype_invs:
"\<lbrakk> invs s; region_in_kernel_window {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} s \<rbrakk>
\<Longrightarrow> post_retype_invs ty (retype_addrs ptr ty n us) s'"
@ -3235,8 +3195,7 @@ lemma post_retype_invs:
valid_kernel_mappings valid_asid_map
valid_global_pd_mappings valid_ioc vms
pspace_in_kernel_window
cap_refs_in_kernel_window valid_irq_states
executable_arch_objs')
cap_refs_in_kernel_window valid_irq_states)
end

4
proof/invariant-abstract/Untyped_AI.thy
View File

@ -3138,10 +3138,6 @@ crunch valid_arch_objs[wp]: create_cap "valid_arch_objs"
(simp: crunch_simps)
crunch executable_arch_objs[wp]: create_cap "executable_arch_objs"
(simp: crunch_simps)
definition
nonempty_table :: "word32 set \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
where

40
proof/invariant-abstract/VSpace_AI.thy
View File

@ -199,10 +199,6 @@ lemma find_free_hw_asid_arch_objs [wp]:
apply (simp add: valid_arch_objs_arch_update)
done
crunch executable_arch_objs [wp]: find_free_hw_asid executable_arch_objs
lemma find_free_hw_asid_pd_at_asid [wp]:
"\<lbrace>pd_at_asid pd asid\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. pd_at_asid pd asid\<rbrace>"
apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def
@ -464,9 +460,6 @@ lemma flush_space_arch_objs[wp]:
done
crunch executable_arch_objs [wp]: flush_space executable_arch_objs
crunch typ_at [wp]: invalidate_asid_entry "\<lambda>s. P (typ_at T p s)"
@ -524,10 +517,6 @@ crunch arch_objs [wp]: invalidate_asid_entry valid_arch_objs
(simp: valid_arch_objs_arch_update)
crunch executable_arch_objs [wp]: invalidate_asid_entry executable_arch_objs
(simp: valid_arch_objs_arch_update)
lemma flush_space_pd_at_asid [wp]:
"\<lbrace>pd_at_asid a pd\<rbrace> flush_space asid \<lbrace>\<lambda>_. pd_at_asid a pd\<rbrace>"
apply (simp add: flush_space_def)
@ -1077,9 +1066,6 @@ crunch arch_objs [wp]: set_vm_root_for_flush valid_arch_objs
(simp: valid_arch_objs_arch_update)
crunch executable_arch_objs [wp]: set_vm_root_for_flush executable_arch_objs
crunch typ_at [wp]: flush_table "\<lambda>s. P (typ_at T p s)"
(simp: assertE_def whenE_def when_def wp: crunch_wps)
@ -1407,9 +1393,6 @@ lemma lookup_pd_slot_pd:
crunch arch_objs [wp]: flush_page valid_arch_objs
(simp: crunch_simps valid_arch_objs_arch_update)
crunch executable_arch_objs [wp]: flush_page executable_arch_objs
(simp: crunch_simps)
crunch equal_mappings [wp]: flush_page equal_kernel_mappings
(simp: crunch_simps)
@ -1584,8 +1567,7 @@ where
definition
"valid_pti pti \<equiv> case pti of
ArchInvocation_A.PageTableMap cap ptr pde p \<Rightarrow>
pde_at p and (%s. wellformed_pde pde) and
(%s. executable_pde pde) and
pde_at p and (\<lambda>s. wellformed_pde pde) and
valid_pde pde and valid_cap cap and
cte_wp_at (\<lambda>c. is_arch_update cap c \<and> cap_asid c = None) ptr and
empty_pde_at p and
@ -2281,8 +2263,7 @@ lemma vs_refs_pdI2:
by (auto simp: vs_refs_def pde_ref_def graph_of_def)
lemma set_pd_invs_map:
"\<lbrace>invs and (%s. \<forall>i. wellformed_pde (pd i)) and
(%s. \<forall>i. executable_pde (pd i)) and
"\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and
obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko \<union> S) p and
obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and
obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd')
@ -2614,8 +2595,7 @@ lemma valid_cap_to_pd_cap:
split: cap.splits option.splits arch_cap.splits)
lemma store_pde_map_invs:
"\<lbrace>(%s. wellformed_pde pde) and invs and empty_pde_at p and valid_pde pde
and (%s. executable_pde pde)
"\<lbrace>(\<lambda>s. wellformed_pde pde) and invs and empty_pde_at p and valid_pde pde
and (\<lambda>s. \<forall>p. pde_ref pde = Some p \<longrightarrow> (\<exists>ao. ko_at (ArchObj ao) p s \<and> valid_arch_obj ao s))
and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)
\<notin> kernel_vsrefs)
@ -2638,10 +2618,6 @@ lemma store_pde_map_invs:
apply (rule conjI)
apply (drule invs_valid_objs)
apply (fastforce simp: valid_objs_def dom_def obj_at_def valid_obj_def)
apply (rule conjI)
apply clarsimp
apply (frule executable_arch_objsD, fastforce)
apply simp
apply (rule conjI)
apply (clarsimp simp: empty_pde_at_def)
apply (clarsimp simp: obj_at_def)
@ -2797,7 +2773,6 @@ lemma mapM_swp_store_pte_invs[wp]:
"\<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. (\<exists>\<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow>
valid_pte pte s) and
(\<lambda>s. wellformed_pte pte) and
(\<lambda>s. executable_pte pte) and
(\<lambda>s. \<exists>slot. cte_wp_at
(\<lambda>c. image (\<lambda>x. x && ~~ mask pt_bits) (set slots) \<subseteq> obj_refs c \<and>
is_pt_cap c \<and> (pte = ARM_Structs_A.InvalidPTE \<or>
@ -2854,7 +2829,6 @@ lemma vs_refs_pdI3:
lemma set_pd_invs_unmap':
"\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and
(\<lambda>s. \<forall>i. executable_pde (pd i)) and
(\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (PageDirectory pd) s) and
obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T) p and
obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and
@ -2940,7 +2914,6 @@ lemma store_pde_invs_unmap':
and valid_pde pde
and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s)
and K (wellformed_pde pde \<and> pde_ref pde = None)
and K (executable_pde pde)
and K (ucast (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots
\<and> (\<exists>xs. slots = p # xs) )
and (\<lambda>s. \<exists>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s)\<rbrace>
@ -2963,12 +2936,6 @@ lemma store_pde_invs_unmap':
apply (erule impE)
apply (clarsimp simp: obj_at_def vs_refs_def)+
apply (rule conjI)
apply (clarsimp simp add: invs_def valid_state_def executable_arch_objs_def)
apply (erule allE[where x="(p && ~~ mask pd_bits)"])
apply (erule_tac x="PageDirectory pd" in allE)
apply (clarsimp simp: obj_at_def)
apply (rule conjI)
apply (clarsimp simp add: invs_def valid_state_def valid_arch_objs_def)
apply (erule_tac P="\<lambda>x. (\<exists>y. ?a y x) \<longrightarrow> ?b x" in allE[where x="(p && ~~ mask pd_bits)"])
@ -3097,7 +3064,6 @@ lemma mapM_x_swp_store_pte_invs [wp]:
"\<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. (\<exists>\<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow>
valid_pte pte s) and
(\<lambda>s. wellformed_pte pte) and
(\<lambda>s. executable_pte pte) and
(\<lambda>s. \<exists>slot. cte_wp_at
(\<lambda>c. image (\<lambda>x. x && ~~ mask pt_bits) (set slots) \<subseteq> obj_refs c \<and>
is_pt_cap c \<and> (pte = ARM_Structs_A.InvalidPTE \<or>

57
proof/refine/ADT_H.thy
View File

@ -72,14 +72,16 @@ definition
"absPageTable h a \<equiv> %offs.
case (h (a + (ucast offs << 2))) of
Some (KOArch (KOPTE (Hardware_H.InvalidPTE))) \<Rightarrow> ARM_Structs_A.InvalidPTE
| Some (KOArch (KOPTE (Hardware_H.LargePagePTE p c g rights))) \<Rightarrow>
| Some (KOArch (KOPTE (Hardware_H.LargePagePTE p c g xn rights))) \<Rightarrow>
if is_aligned offs 4 then
ARM_Structs_A.LargePagePTE p
{x. c & x=PageCacheable | g & x=Global} (vm_rights_of rights)
{x. c & x=PageCacheable | g & x=Global | xn & x=XNever}
(vm_rights_of rights)
else ARM_Structs_A.InvalidPTE
| Some (KOArch (KOPTE (Hardware_H.SmallPagePTE p c g rights))) \<Rightarrow>
| Some (KOArch (KOPTE (Hardware_H.SmallPagePTE p c g xn rights))) \<Rightarrow>
ARM_Structs_A.SmallPagePTE p {x. c & x=PageCacheable |
g & x=Global} (vm_rights_of rights)"
g & x=Global |
xn & x=XNever} (vm_rights_of rights)"
definition
absPageDirectory :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> obj_ref \<Rightarrow>
@ -90,14 +92,16 @@ definition
Some (KOArch (KOPDE (Hardware_H.InvalidPDE))) \<Rightarrow> ARM_Structs_A.InvalidPDE
| Some (KOArch (KOPDE (Hardware_H.PageTablePDE p e mw))) \<Rightarrow>
ARM_Structs_A.PageTablePDE p {x. e & x=ParityEnabled} mw
| Some (KOArch (KOPDE (Hardware_H.SectionPDE p e mw c g rights))) \<Rightarrow>
| Some (KOArch (KOPDE (Hardware_H.SectionPDE p e mw c g xn rights))) \<Rightarrow>
ARM_Structs_A.SectionPDE p {x. e & x=ParityEnabled |
c & x=PageCacheable |
g & x=Global} mw (vm_rights_of rights)
| Some (KOArch (KOPDE (Hardware_H.SuperSectionPDE p e c g rights))) \<Rightarrow>
g & x=Global |
xn & x=XNever} mw (vm_rights_of rights)
| Some (KOArch (KOPDE (Hardware_H.SuperSectionPDE p e c g xn rights))) \<Rightarrow>
if is_aligned offs 4 then
ARM_Structs_A.SuperSectionPDE p
{x. e & x=ParityEnabled | c & x=PageCacheable | g & x=Global}
{x. e & x=ParityEnabled | c & x=PageCacheable
| g & x=Global | xn & x=XNever}
(vm_rights_of rights)
else ARM_Structs_A.InvalidPDE"
@ -125,10 +129,10 @@ lemma
Some (KOArch (KOPTE pte')))"
and pte_rights:
"\<forall>x. case ksPSpace \<sigma> x of
Some (KOArch (KOPTE (Hardware_H.LargePagePTE _ _ _ r))) \<Rightarrow>
Some (KOArch (KOPTE (Hardware_H.LargePagePTE _ _ _ _ r))) \<Rightarrow>
r \<noteq> VMNoAccess"
"\<forall>x. case ksPSpace \<sigma> x of
Some (KOArch (KOPTE (Hardware_H.SmallPagePTE _ _ _ r))) \<Rightarrow>
Some (KOArch (KOPTE (Hardware_H.SmallPagePTE _ _ _ _ r))) \<Rightarrow>
r \<noteq> VMNoAccess"
assumes pdes:
@ -138,10 +142,10 @@ lemma
Some (KOArch (KOPDE pde')))"
and pde_rights:
"\<forall>x. case ksPSpace \<sigma> x of
Some (KOArch (KOPDE (Hardware_H.SectionPDE _ _ _ _ _ r))) \<Rightarrow>
Some (KOArch (KOPDE (Hardware_H.SectionPDE _ _ _ _ _ _ r))) \<Rightarrow>
r \<noteq> VMNoAccess"
"\<forall>x. case ksPSpace \<sigma> x of
Some (KOArch (KOPDE (Hardware_H.SuperSectionPDE _ _ _ _ r))) \<Rightarrow>
Some (KOArch (KOPDE (Hardware_H.SuperSectionPDE _ _ _ _ _ r))) \<Rightarrow>
r \<noteq> VMNoAccess"
assumes fst_pte:
@ -558,7 +562,6 @@ lemma absHeap_correct:
assumes pspace_aligned: "pspace_aligned s"
assumes pspace_distinct: "pspace_distinct s"
assumes valid_objs: "valid_objs s"
assumes executable_arch_objs: "executable_arch_objs s"
assumes pspace_relation: "pspace_relation (kheap s) (ksPSpace s')"
assumes ghost_relation:
"ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')"
@ -805,20 +808,10 @@ proof -
apply (case_tac pte, simp_all add: pte_relation_aligned_def)[1]
apply (clarsimp split: ARM_Structs_A.pte.splits)
apply (rule set_eqI, clarsimp)
apply (case_tac x, simp_all)
using executable_arch_objs[simplified executable_arch_objs_def]
apply (erule_tac x=y in allE)
apply (clarsimp simp: obj_at_def executable_pte_def)
apply (erule_tac x=offs in allE)
apply clarsimp
apply (case_tac x, simp_all)[1]
apply (clarsimp split: ARM_Structs_A.pte.splits)
apply (rule set_eqI, clarsimp)
apply (case_tac x, simp_all)
using executable_arch_objs[simplified executable_arch_objs_def]
apply (erule_tac x=y in allE)
apply (clarsimp simp: obj_at_def executable_pte_def)
apply (erule_tac x=offs in allE)
apply clarsimp
apply (case_tac x, simp_all)[1]
apply (clarsimp simp add: pde_relation_def)
apply clarsimp+
@ -862,20 +855,10 @@ proof -
apply (fastforce simp add: subset_eq)
apply (clarsimp split: ARM_Structs_A.pde.splits)
apply (rule set_eqI, clarsimp)
apply (case_tac x, simp_all)
using executable_arch_objs[simplified executable_arch_objs_def]
apply (erule_tac x=y in allE)
apply (clarsimp simp: obj_at_def executable_pde_def)
apply (erule_tac x=offs in allE)
apply clarsimp
apply (case_tac x, simp_all)[1]
apply (clarsimp split: ARM_Structs_A.pde.splits)
apply (rule set_eqI, clarsimp)
apply (case_tac x, simp_all)
using executable_arch_objs[simplified executable_arch_objs_def]
apply (erule_tac x=y in allE)
apply (clarsimp simp: obj_at_def executable_pde_def)
apply (erule_tac x=offs in allE)
apply clarsimp
apply (case_tac x, simp_all)[1]
apply (clarsimp simp add: pde_relation_def)
done
qed

26
proof/refine/ArchAcc_R.thy
View File

@ -878,18 +878,6 @@ lemma set_pt_corres:
apply (simp add: caps_of_state_after_update obj_at_def swp_cte_at_caps_of)
done
lemma word_from_vm_rights [simp]:
"fromEnum (vmrights_map R) = unat (word_from_vm_rights R)"
by (simp add: vmrights_map_def fromEnum_def enum_vmrights word_from_vm_rights_def
vm_read_only_def vm_kernel_only_def vm_read_write_def)
lemma word_from_pde_corres:
"pde_relation' pde pde' \<Longrightarrow> wordFromPDE pde'= word_from_pde pde"
apply (simp add: word_from_pde_def wordFromPDE_def)
apply (cases pde)
apply (auto simp: ucast_id shiftL_nat shiftl_t2n)
done
lemma store_pde_corres:
"pde_relation_aligned (p >> 2) pde pde' \<Longrightarrow>
corres dc (pde_at p and pspace_aligned and valid_etcbs) (pde_at' p) (store_pde p pde) (storePDE p pde')"
@ -918,13 +906,6 @@ lemma store_pde_corres':
apply auto
done
lemma word_from_pte_corres:
"pte_relation' pte pte' \<Longrightarrow> wordFromPTE pte'= word_from_pte pte"
apply (simp add: word_from_pte_def wordFromPTE_def)
apply (cases pte)
apply (auto simp: ucast_id word_from_vm_rights shiftL_nat shiftl_t2n field_simps)
done
lemma store_pte_corres:
"pte_relation_aligned (p>>2) pte pte' \<Longrightarrow>
corres dc (pte_at p and pspace_aligned and valid_etcbs) (pte_at' p) (store_pte p pte) (storePTE p pte')"
@ -1243,7 +1224,7 @@ lemma arch_derive_corres:
done
definition
"vmattributes_map \<equiv> \<lambda>R. VMAttributes (PageCacheable \<in> R) (ParityEnabled \<in> R)"
"vmattributes_map \<equiv> \<lambda>R. VMAttributes (PageCacheable \<in> R) (ParityEnabled \<in> R) (XNever \<in> R)"
definition
mapping_map :: "ARM_Structs_A.pte \<times> word32 list + ARM_Structs_A.pde \<times> word32 list \<Rightarrow>
@ -1300,16 +1281,15 @@ definition
lemma valid_slots_typ_at':
assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
assumes y: "\<And>arch p. \<lbrace>ko_wp_at' (op = (KOArch arch)) p\<rbrace> f \<lbrace>\<lambda>rv. ko_wp_at' (op = (KOArch arch)) p\<rbrace>"
shows "\<lbrace>valid_slots' m\<rbrace> f \<lbrace>\<lambda>rv. valid_slots' m\<rbrace>"
unfolding valid_slots'_def
apply (cases m)
apply (case_tac a)
apply simp
apply (wp x y hoare_vcg_const_Ball_lift valid_pte_lift')
apply (wp x valid_pte_lift')
apply (case_tac b)
apply simp
apply (wp x y hoare_vcg_const_Ball_lift valid_pde_lift')
apply (wp x valid_pde_lift')
done
lemma createMappingEntries_valid_slots' [wp]:

4
proof/refine/Arch_R.thy
View File

@ -1423,13 +1423,13 @@ lemma findPDForASID_page_directory_at':
definition "slots_duplicated_ensured \<equiv> \<lambda>m s. case m of
Inl (pte, xs) \<Rightarrow> (case pte of
pte.LargePagePTE _ _ _ _ \<Rightarrow> \<exists>p. xs = [p, p+4 .e. p + mask 6] \<and> is_aligned p 6
pte.LargePagePTE _ _ _ _ _ \<Rightarrow> \<exists>p. xs = [p, p+4 .e. p + mask 6] \<and> is_aligned p 6
\<and> page_table_at' (p && ~~ mask ptBits) s
| pte.InvalidPTE \<Rightarrow> False
| _ \<Rightarrow> \<exists>p. xs = [p]
\<and> page_table_at' (p && ~~ mask ptBits) s)
| Inr (pde, xs) \<Rightarrow> (case pde of
pde.SuperSectionPDE _ _ _ _ _ \<Rightarrow> \<exists>p. xs = [p, p+4 .e. p + mask 6] \<and> is_aligned p 6
pde.SuperSectionPDE _ _ _ _ _ _ \<Rightarrow> \<exists>p. xs = [p, p+4 .e. p + mask 6] \<and> is_aligned p 6
\<and> page_directory_at' (p && ~~ mask pdBits) s \<and> is_aligned p 6
| pde.InvalidPDE \<Rightarrow> False
| _ \<Rightarrow> \<exists>p. xs = [p]

18
proof/refine/Invariants_H.thy
View File

@ -393,16 +393,16 @@ primrec
valid_pte' :: "Hardware_H.pte \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"valid_pte' (InvalidPTE) = \<top>"
| "valid_pte' (LargePagePTE ptr x y z) = (valid_mapping' ptr ARMLargePage)"
| "valid_pte' (SmallPagePTE ptr x y z) = (valid_mapping' ptr ARMSmallPage)"
| "valid_pte' (LargePagePTE ptr _ _ _ _) = (valid_mapping' ptr ARMLargePage)"
| "valid_pte' (SmallPagePTE ptr _ _ _ _) = (valid_mapping' ptr ARMSmallPage)"
primrec
valid_pde' :: "Hardware_H.pde \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"valid_pde' (InvalidPDE) = \<top>"
| "valid_pde' (SectionPDE ptr x y z z' w) = (valid_mapping' ptr ARMSection)"
| "valid_pde' (SuperSectionPDE ptr x y z w) = (valid_mapping' ptr ARMSuperSection)"
| "valid_pde' (PageTablePDE ptr x z) = (\<lambda>_. is_aligned ptr ptBits)"
| "valid_pde' (SectionPDE ptr _ _ _ _ _ _) = (valid_mapping' ptr ARMSection)"
| "valid_pde' (SuperSectionPDE ptr _ _ _ _ _) = (valid_mapping' ptr ARMSuperSection)"
| "valid_pde' (PageTablePDE ptr _ _) = (\<lambda>_. is_aligned ptr ptBits)"
primrec
valid_asid_pool' :: "asidpool \<Rightarrow> kernel_state \<Rightarrow> bool"
@ -696,8 +696,8 @@ definition
definition
vs_ptr_align :: "Structures_H.kernel_object \<Rightarrow> nat" where
"vs_ptr_align obj \<equiv>
case obj of KOArch (KOPTE (Hardware_H.pte.LargePagePTE _ _ _ _)) \<Rightarrow> 6
| KOArch (KOPDE (Hardware_H.pde.SuperSectionPDE _ _ _ _ _)) \<Rightarrow> 6
case obj of KOArch (KOPTE (Hardware_H.pte.LargePagePTE _ _ _ _ _)) \<Rightarrow> 6
| KOArch (KOPDE (Hardware_H.pde.SuperSectionPDE _ _ _ _ _ _)) \<Rightarrow> 6
| _ \<Rightarrow> 0"
definition "vs_valid_duplicates' \<equiv> \<lambda>h.
@ -1410,9 +1410,9 @@ lemma objBits_cte_conv:
lemma valid_pde_mapping'_simps[simp]:
"valid_pde_mapping' offset (InvalidPDE) = True"
"valid_pde_mapping' offset (SectionPDE ptr x y z z' w)
"valid_pde_mapping' offset (SectionPDE ptr a b c d e w)
= valid_pde_mapping_offset' offset"
"valid_pde_mapping' offset (SuperSectionPDE ptr x y' z w)
"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' offset"

14
proof/refine/StateRelation.thy
View File

@ -198,10 +198,10 @@ where
= (x = Hardware_H.PageTablePDE ptr (ParityEnabled \<in> atts) domain)"
| "pde_relation' (ARM_Structs_A.SectionPDE ptr atts domain rghts) x
= (x = Hardware_H.SectionPDE ptr (ParityEnabled \<in> atts) domain
(PageCacheable \<in> atts) (Global \<in> atts) (vmrights_map rghts))"
(PageCacheable \<in> atts) (Global \<in> atts) (XNever \<in> atts) (vmrights_map rghts))"
| "pde_relation' (ARM_Structs_A.SuperSectionPDE ptr atts rghts) x
= (x = Hardware_H.SuperSectionPDE ptr (ParityEnabled \<in> atts)
(PageCacheable \<in> atts) (Global \<in> atts) (vmrights_map rghts))"
(PageCacheable \<in> atts) (Global \<in> atts) (XNever \<in> atts) (vmrights_map rghts))"
primrec
@ -209,16 +209,18 @@ primrec
where
"pte_relation' ARM_Structs_A.InvalidPTE x = (x = Hardware_H.InvalidPTE)"
| "pte_relation' (ARM_Structs_A.LargePagePTE ptr atts rghts) x
= (x = Hardware_H.LargePagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts) (vmrights_map rghts))"
= (x = Hardware_H.LargePagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts)
(XNever \<in> atts) (vmrights_map rghts))"
| "pte_relation' (ARM_Structs_A.SmallPagePTE ptr atts rghts) x
= (x = Hardware_H.SmallPagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts) (vmrights_map rghts))"
= (x = Hardware_H.SmallPagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts)
(XNever \<in> atts) (vmrights_map rghts))"
definition
pde_align' :: "Hardware_H.pde \<Rightarrow> nat"
where
"pde_align' pde \<equiv>
case pde of Hardware_H.pde.SuperSectionPDE _ _ _ _ _ \<Rightarrow> 4 | _ \<Rightarrow> 0"
case pde of Hardware_H.pde.SuperSectionPDE _ _ _ _ _ _ \<Rightarrow> 4 | _ \<Rightarrow> 0"
lemmas pde_align_simps[simp] =
pde_align'_def[split_simps ARM_Structs_A.pde.split]
@ -226,7 +228,7 @@ lemmas pde_align_simps[simp] =
definition
pte_align' :: "Hardware_H.pte \<Rightarrow> nat"
where
"pte_align' pte \<equiv> case pte of Hardware_H.pte.LargePagePTE _ _ _ _ \<Rightarrow> 4 | _ \<Rightarrow> 0"
"pte_align' pte \<equiv> case pte of Hardware_H.pte.LargePagePTE _ _ _ _ _ \<Rightarrow> 4 | _ \<Rightarrow> 0"
lemmas pte_align_simps[simp] =
pte_align'_def[split_simps ARM_Structs_A.pte.split]

4
proof/refine/VSpace_R.thy
View File

@ -1750,12 +1750,12 @@ definition
definition "valid_slots_duplicated' \<equiv> \<lambda>m s. case m of
Inl (pte, xs) \<Rightarrow> (case pte of
pte.LargePagePTE _ _ _ _ \<Rightarrow> \<exists>p. xs = [p, p+4 .e. p + mask 6] \<and> is_aligned p 6
pte.LargePagePTE _ _ _ _ _ \<Rightarrow> \<exists>p. xs = [p, p+4 .e. p + mask 6] \<and> is_aligned p 6
\<and> page_table_at' (p && ~~ mask ptBits) s
| _ \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s
\<and> page_table_at' (p && ~~ mask ptBits) s)
| Inr (pde, xs) \<Rightarrow> (case pde of
pde.SuperSectionPDE _ _ _ _ _ \<Rightarrow> \<exists>p. xs = [p, p+4 .e. p + mask 6] \<and> is_aligned p 6
pde.SuperSectionPDE _ _ _ _ _ _ \<Rightarrow> \<exists>p. xs = [p, p+4 .e. p + mask 6] \<and> is_aligned p 6
\<and> page_directory_at' (p && ~~ mask pdBits) s
| _ \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s
\<and> page_directory_at' (p && ~~ mask pdBits) s)"

48
spec/abstract/ArchVSpaceAcc_A.thy
View File

@ -35,54 +35,6 @@ definition
"kernel_base \<equiv> 0xf0000000"
*)
text {* Convert a set of rights into binary form. *}
definition
word_from_vm_rights :: "vm_rights \<Rightarrow> word32" where
"word_from_vm_rights R \<equiv>
if vm_read_write \<subseteq> R then 3
else if vm_read_only \<subseteq> R then 2
else 1"
text {* Encode a page directory entry into the equivalent entry that the page
table walker implemented in ARM hardware would parse. *}
definition
word_from_pde :: "pde \<Rightarrow> machine_word" where
"word_from_pde pde \<equiv> case pde of
InvalidPDE \<Rightarrow> 0
| PageTablePDE table attrib domain \<Rightarrow> 1 ||
table && 0xfffffc00 ||
(if ParityEnabled \<in> attrib then 1 << 9 else 0) ||
((domain && 0xf) << 5)
| SectionPDE frame attrib domain rights \<Rightarrow> 2 ||
frame && 0xfff00000 ||
(if ParityEnabled \<in> attrib then (1 << 9) else 0) ||
(if PageCacheable \<in> attrib then (1 << 2) || (1 << 3) else 0) ||
((domain && 0xf) << 5) ||
(if Global \<in> attrib then 0 else (1 << 17)) ||
(word_from_vm_rights rights << 10)
| SuperSectionPDE frame attrib rights \<Rightarrow> 2 ||
(1 << 18) ||
(frame && 0xff000000) ||
(if ParityEnabled \<in> attrib then 1 << 9 else 0) ||
(if PageCacheable \<in> attrib then (1 << 2) || (1 << 3) else 0) ||
(if Global \<in> attrib then 0 else (1 << 17)) ||
(word_from_vm_rights rights << 10)"
text {* Encode a page table entry into the equivalent entry that the page
table walker implemented in ARM hardware would parse. *}
definition
word_from_pte :: "pte \<Rightarrow> machine_word" where
"word_from_pte pte \<equiv> case pte of
InvalidPTE \<Rightarrow> 0
| LargePagePTE frame attrib rights \<Rightarrow> 1 ||
(frame && 0xffff0000) ||
(if PageCacheable \<in> attrib then (1 << 2) || (1 << 3) else 0) ||
(word_from_vm_rights rights * 85 << 4)
| (SmallPagePTE frame attrib rights) \<Rightarrow> 2 ||
(frame && 0xfffff000) ||
(if PageCacheable \<in> attrib then (1 << 2) || (1 << 3) else 0) ||
(word_from_vm_rights rights * 85 << 4)"
text {* The high bits of a virtual ASID. *}
definition
asid_high_bits_of :: "asid \<Rightarrow> word8" where

5
spec/abstract/ArchVSpace_A.thy
View File

@ -709,8 +709,9 @@ mapping is to have. *}
definition
attribs_from_word :: "word32 \<Rightarrow> vm_attributes" where
"attribs_from_word w \<equiv>
let V = (if w !!0 then {PageCacheable} else {})
in if w!!1 then insert ParityEnabled V else V"
let V = (if w !!0 then {PageCacheable} else {});
V' = (if w!!1 then insert ParityEnabled V else V)
in if w!!2 then insert XNever V' else V'"
text {* Update the mapping data saved in a page or page table capability. *}
definition

4
spec/abstract/Syscall_A.thy
View File

@ -68,12 +68,12 @@ result in a fault;
\item the fault handler @{text h_fault} to execute if the first
operation resulted in a fault;
\item the second operation @{text m_error} to execute (if no fault
occured in the first operation); this second operation may result in
occurred in the first operation); this second operation may result in
an error;
\item the error handler @{text h_error} to execute if the second
operation resulted in an error;
\item the third and last operation @{text h_error} to execute (if
no error occured in the second operation); this operation may be
no error occurred in the second operation); this operation may be
interrupted.
\end{itemize}
*}