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

repair ARM proofs up to Refine after factoring out architecture

This commit is contained in:
Daniel Matichuk 2016-01-12 16:44:35 +11:00
parent fad2c6aae9
commit ca808130e6
48 changed files with 655 additions and 721 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
lib/Eisbach_Methods.thy
View File

@ -239,37 +239,18 @@ section \<open>Utility methods\<close>
subsection \<open>Finding a goal based on successful application of a method\<close>
text \<open>This method works by creating "tagged" subgoals in order to use the + operator
to iterate over all goals without looping indefinitely.
Effectively this looks like a while-loop, which breaks out when either
the "end" subgoal is found or when the method succeeds and the "success"
subgoal is found.\<close>
context begin
private definition "goal_tag (x :: unit) \<equiv> Trueprop True"
method_setup find_goal =
\<open>Method_Closure.parse_method >> (fn m => fn ctxt => fn facts =>
let
fun prefer_first i = SELECT_GOAL
(fn st' =>
(case Seq.pull (Method_Closure.method_evaluate m ctxt facts st') of
SOME ((_, st''),_) => Seq.single st''
| NONE => Seq.empty)) i THEN prefer_tac i
private lemma goal_tagI: "PROP goal_tag x"
unfolding goal_tag_def
by simp
private method make_tag_goal for tag_id :: unit = (rule thin_rl[of "PROP goal_tag tag_id"])
private method clear_tagged_goal for tag_id :: unit = (rule goal_tagI[of tag_id])
private definition "goals_end \<equiv> ()"
private definition "method_succeed \<equiv> ()"
private definition "method_failure \<equiv> ()"
method find_goal methods m =
(make_tag_goal goals_end,
defer_tac,
(fails \<open>clear_tagged_goal method_succeed | clear_tagged_goal goals_end\<close>,
(((m)[1],make_tag_goal method_succeed)
| defer_tac))+,
clear_tagged_goal method_succeed,
all \<open>(clear_tagged_goal goals_end)?\<close>)
in SIMPLE_METHOD (FIRSTGOAL prefer_first) facts end)\<close>
end

2
lib/WordEnum.thy
View File

@ -102,7 +102,7 @@ end
definition
upto_enum_step :: "word32 \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> word32 list" ("[_ , _ .e. _]")
upto_enum_step :: "('a :: len) word \<Rightarrow> 'a word \<Rightarrow> 'a word \<Rightarrow> 'a word list" ("[_ , _ .e. _]")
where
"upto_enum_step a b c \<equiv>
if c < a then [] else map (\<lambda>x. a + x * (b - a)) [0 .e. (c - a) div (b - a)]"

14
lib/WordLemmaBucket.thy
View File

@ -598,11 +598,10 @@ lemma upto_enum_red2:
apply (subst word_le_nat_alt, simp)
done
(* FIXME: WordEnum.upto_enum_step_def is fixed to word32. *)
lemma upto_enum_step_red:
assumes szv: "sz < word_bits"
assumes szv: "sz < len_of (TYPE('a))"
and usszv: "us \<le> sz"
shows "[0 , 2 ^ us .e. 2 ^ sz - 1] =
shows "[0 :: 'a :: len word , 2 ^ us .e. 2 ^ sz - 1] =
map (\<lambda>x. of_nat x * 2 ^ us) [0 ..< 2 ^ (sz - us)]" using szv
unfolding upto_enum_step_def
apply (subst if_not_P)
@ -614,10 +613,9 @@ lemma upto_enum_step_red:
apply simp
apply (subst upto_enum_red)
apply (simp del: upt.simps)
apply (subst Suc_div_unat_helper [where 'a = 32, folded word_bits_def, OF szv usszv, symmetric])
apply (subst Suc_div_unat_helper [where 'a = 'a, folded word_bits_def, OF szv usszv, symmetric])
apply clarsimp
apply (subst toEnum_of_nat)
apply (subst word_bits_len_of)
apply (erule order_less_trans)
using szv
apply simp
@ -1915,7 +1913,7 @@ qed
lemma distinct_prop_enum:
"\<lbrakk> \<And>x y. \<lbrakk> x \<le> stop; y \<le> stop; x \<noteq> y \<rbrakk>
\<Longrightarrow> P x y \<rbrakk>
\<Longrightarrow> distinct_prop P [(0 :: word32) .e. stop]"
\<Longrightarrow> distinct_prop P [0 :: 'a :: len word .e. stop]"
apply (simp add: upto_enum_def distinct_prop_map
del: upt.simps)
apply (rule distinct_prop_distinct)
@ -2142,8 +2140,8 @@ lemma upto_enum_step_shift:
done
lemma upto_enum_step_shift_red:
"\<lbrakk> is_aligned p sz; sz < word_bits; us \<le> sz \<rbrakk>
\<Longrightarrow> [p, p + 2 ^ us .e. p + 2 ^ sz - 1]
"\<lbrakk> is_aligned p sz; sz < len_of (TYPE('a)); us \<le> sz \<rbrakk>
\<Longrightarrow> [p :: 'a :: len word, p + 2 ^ us .e. p + 2 ^ sz - 1]
= map (\<lambda>x. p + of_nat x * 2 ^ us) [0 ..< 2 ^ (sz - us)]"
apply (subst upto_enum_step_shift, assumption)
apply (simp add: upto_enum_step_red)

2
lib/WordSetup.thy
View File

@ -38,7 +38,7 @@ definition
"is_aligned ptr n \<equiv> 2^n dvd unat ptr"
definition
ptr_add :: "word32 \<Rightarrow> nat \<Rightarrow> word32" where
ptr_add :: "'a :: len word \<Rightarrow> nat \<Rightarrow> 'a word" where
"ptr_add ptr n \<equiv> ptr + of_nat n"
definition

42
proof/invariant-abstract/ADT_AI.thy
View File

@ -196,7 +196,7 @@ where
"get_pd_of_thread khp astate tcb_ref \<equiv>
case khp tcb_ref of Some (TCB tcb) \<Rightarrow>
(case tcb_vtable tcb of
cap.ArchObjectCap (ARM_Structs_A.PageDirectoryCap pd_ref (Some asid))
cap.ArchObjectCap (Arch_Structs_A.PageDirectoryCap pd_ref (Some asid))
\<Rightarrow> (case arm_asid_table astate (asid_high_bits_of asid) of
None \<Rightarrow> arm_global_pd astate
| Some p \<Rightarrow> (case khp p of None \<Rightarrow> arm_global_pd astate
@ -232,7 +232,7 @@ lemma get_pd_of_thread_def2:
"get_pd_of_thread khp astate tcb_ref \<equiv>
case khp tcb_ref of Some (TCB tcb) \<Rightarrow>
(case tcb_vtable tcb of
cap.ArchObjectCap (ARM_Structs_A.PageDirectoryCap pd_ref (Some asid))
cap.ArchObjectCap (Arch_Structs_A.PageDirectoryCap pd_ref (Some asid))
\<Rightarrow> if (\<exists>p apool.
arm_asid_table astate (asid_high_bits_of asid) = Some p \<and>
khp p = Some (ArchObj (arch_kernel_obj.ASIDPool apool)) \<and>
@ -256,7 +256,7 @@ lemma get_pd_of_thread_vs_lookup:
(case kheap s tcb_ref of
Some (TCB tcb) \<Rightarrow>
(case tcb_vtable tcb of
cap.ArchObjectCap (ARM_Structs_A.PageDirectoryCap r (Some asid)) \<Rightarrow>
cap.ArchObjectCap (Arch_Structs_A.PageDirectoryCap r (Some asid)) \<Rightarrow>
if (the (vs_cap_ref (tcb_vtable tcb)) \<rhd> r) s then r
else arm_global_pd (arch_state s)
| _ \<Rightarrow> arm_global_pd (arch_state s))
@ -332,7 +332,7 @@ lemma get_pd_of_thread_eq:
get_pd_of_thread (kheap s) (arch_state s) tcb_ref = pd_ref \<longleftrightarrow>
(\<exists>tcb. kheap s tcb_ref = Some (TCB tcb) \<and>
(\<exists>asid. tcb_vtable tcb =
cap.ArchObjectCap (ARM_Structs_A.PageDirectoryCap
cap.ArchObjectCap (Arch_Structs_A.PageDirectoryCap
pd_ref (Some asid)) \<and>
(the (vs_cap_ref (tcb_vtable tcb)) \<rhd> pd_ref) s))"
by (auto simp: get_pd_of_thread_vs_lookup vs_cap_ref_def
@ -357,7 +357,7 @@ text {* Non-monad versions of @{term get_pte} and @{term get_pde}.
definition
"get_pt_entry ahp pt_ref vptr \<equiv>
case ahp pt_ref of
Some (ARM_Structs_A.PageTable pt) \<Rightarrow>
Some (Arch_Structs_A.PageTable pt) \<Rightarrow>
Some (pt (ucast ((vptr >> 12) && mask 8)))
| _ \<Rightarrow> None"
definition
@ -474,8 +474,8 @@ done
definition
"get_pt_info ahp pt_ref vptr \<equiv>
case get_pt_entry ahp pt_ref vptr of
Some (ARM_Structs_A.SmallPagePTE base attrs rights) \<Rightarrow> Some (base, 12, attrs, rights)
| Some (ARM_Structs_A.LargePagePTE base attrs rights) \<Rightarrow> Some (base, 16, attrs, rights)
Some (Arch_Structs_A.SmallPagePTE base attrs rights) \<Rightarrow> Some (base, 12, attrs, rights)
| Some (Arch_Structs_A.LargePagePTE base attrs rights) \<Rightarrow> Some (base, 16, attrs, rights)
| _ \<Rightarrow> None"
text {*
@ -494,10 +494,10 @@ where
get_page_info_def:
"get_page_info ahp pd_ref vptr \<equiv>
case get_pd_entry ahp pd_ref vptr of
Some (ARM_Structs_A.PageTablePDE p _ _) \<Rightarrow>
Some (Arch_Structs_A.PageTablePDE p _ _) \<Rightarrow>
get_pt_info ahp (Platform.ptrFromPAddr p) vptr
| Some (ARM_Structs_A.SectionPDE base attrs _ rights) \<Rightarrow> Some (base, 20, attrs, rights)
| Some (ARM_Structs_A.SuperSectionPDE base attrs rights) \<Rightarrow> Some (base,24, attrs, rights)
| Some (Arch_Structs_A.SectionPDE base attrs _ rights) \<Rightarrow> Some (base, 20, attrs, rights)
| Some (Arch_Structs_A.SuperSectionPDE base attrs rights) \<Rightarrow> Some (base,24, attrs, rights)
| _ \<Rightarrow> None"
@ -536,7 +536,7 @@ by (auto simp add: lookup_pt_slot_def lookup_pd_slot_def liftE_def bindE_def
get_pde_def get_pd_def Union_eq get_object_def simpler_gets_def
assert_def fail_def mask_eqs
split: sum.splits split_if_asm Structures_A.kernel_object.splits
arch_kernel_obj.splits ARM_Structs_A.pde.splits)
arch_kernel_obj.splits Arch_Structs_A.pde.splits)
(* FIXME: Lemma can be found in ArchAcc_R *)
lemma shiftr_shiftl_mask_pd_bits:
@ -558,14 +558,14 @@ lemma lookup_pt_slot_no_fail:
kheap s pd = Some (ArchObj (PageDirectory pdo)) \<Longrightarrow>
lookup_pt_slot pd vptr s =
(case pdo (ucast (vptr >> 20)) of
ARM_Structs_A.InvalidPDE \<Rightarrow>
Arch_Structs_A.InvalidPDE \<Rightarrow>
({(Inl (ExceptionTypes_A.MissingCapability 20),s)},False)
| ARM_Structs_A.PageTablePDE p _ _ \<Rightarrow>
| Arch_Structs_A.PageTablePDE p _ _ \<Rightarrow>
({(Inr (Platform.ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2)),s)},
False)
| ARM_Structs_A.SectionPDE _ _ _ _ \<Rightarrow>
| Arch_Structs_A.SectionPDE _ _ _ _ \<Rightarrow>
({(Inl (ExceptionTypes_A.MissingCapability 20),s)},False)
| ARM_Structs_A.SuperSectionPDE _ _ _ \<Rightarrow>
| Arch_Structs_A.SuperSectionPDE _ _ _ \<Rightarrow>
({(Inl (ExceptionTypes_A.MissingCapability 20),s)},False) )"
apply (frule pd_shifting'[of _ vptr])
apply (cut_tac shiftr_shiftl_mask_pd_bits[of vptr])
@ -583,7 +583,7 @@ by (clarsimp simp add: lookup_pt_slot_def lookup_pd_slot_def liftE_def bindE_def
get_pde_def get_pd_def Union_eq get_object_def simpler_gets_def
assert_def fail_def mask_add_aligned
split: sum.splits split_if_asm kernel_object.splits arch_kernel_obj.splits
ARM_Structs_A.pde.splits)
Arch_Structs_A.pde.splits)
lemma get_page_info_pte:
"is_aligned pd_ref pd_bits \<Longrightarrow>
@ -592,8 +592,8 @@ lemma get_page_info_pte:
get_pte x s = ({(pte,s)},False) \<Longrightarrow>
get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr =
(case pte of
ARM_Structs_A.SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)
| ARM_Structs_A.LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights)
Arch_Structs_A.SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)
| Arch_Structs_A.LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights)
| _ \<Rightarrow> None)"
apply (clarsimp simp add: get_page_info_def get_pd_entry_def
split: option.splits)
@ -605,7 +605,7 @@ apply (intro conjI impI allI)
apply (frule lookup_pt_slot_fail[of _ vptr s],
clarsimp simp add: get_arch_obj_def)
apply (frule (1) lookup_pt_slot_no_fail[where vptr=vptr])
apply (clarsimp split: ARM_Structs_A.pde.splits option.splits)
apply (clarsimp split: Arch_Structs_A.pde.splits option.splits)
apply (clarsimp simp add: get_pt_info_def split: option.splits)
apply (intro conjI impI)
apply (drule get_pt_entry_None_iff_get_pte_fail[where s=s and vptr=vptr])
@ -618,7 +618,7 @@ done
lemma get_page_info_section:
"is_aligned pd_ref pd_bits \<Longrightarrow>
get_pde (lookup_pd_slot pd_ref vptr) s =
({(ARM_Structs_A.SectionPDE base attrs X rights, s)},False) \<Longrightarrow>
({(Arch_Structs_A.SectionPDE base attrs X rights, s)},False) \<Longrightarrow>
get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr =
Some (base, 20, attrs, rights)"
apply (simp add: lookup_pd_slot_def get_page_info_def split: option.splits)
@ -632,7 +632,7 @@ done
lemma get_page_info_super_section:
"is_aligned pd_ref pd_bits \<Longrightarrow>
get_pde (lookup_pd_slot pd_ref vptr) s =
({(ARM_Structs_A.SuperSectionPDE base attrs rights,s)},False) \<Longrightarrow>
({(Arch_Structs_A.SuperSectionPDE base attrs rights,s)},False) \<Longrightarrow>
get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr =
Some (base, 24, attrs, rights)"
apply (simp add: lookup_pd_slot_def get_page_info_def split: option.splits)

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

@ -118,7 +118,7 @@ lemma some_get_page_info_kmapsD:
kernel_mappings_slots_eq
split: option.splits Structures_A.kernel_object.splits
arch_kernel_obj.splits
ARM_Structs_A.pde.splits ARM_Structs_A.pte.splits)
Arch_Structs_A.pde.splits Arch_Structs_A.pte.splits)
apply (rule conjI, rule_tac x=ARMLargePage in exI, simp)
apply (simp add: valid_pde_kernel_mappings_def obj_at_def
valid_pt_kernel_mappings_def)
@ -181,7 +181,7 @@ lemma some_get_page_info_umapsD:
apply (simp add: obj_at_def)
apply (simp add: valid_arch_obj_def)
apply (drule bspec, simp)
apply (simp split: ARM_Structs_A.pde.splits)
apply (simp split: Arch_Structs_A.pde.splits)
apply (rename_tac rs pd pt_ref rights w)
apply (subgoal_tac
"((rs, pd_ref) \<rhd>1
@ -199,7 +199,7 @@ lemma some_get_page_info_umapsD:
apply (simp add: get_pt_info_def get_pt_entry_def)
apply (drule_tac x="(ucast ((p >> 12) && mask 8))" in spec)
apply (clarsimp simp: obj_at_def valid_arch_obj_def
split: ARM_Structs_A.pte.splits)
split: Arch_Structs_A.pte.splits)
apply (clarsimp simp: pspace_aligned_def)
apply (drule_tac x = "(Platform.ptrFromPAddr b)" in bspec, fastforce)
apply (drule is_aligned_ptrFromPAddrD)

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

@ -82,13 +82,13 @@ bundle pagebits =
pd_bits_def[simp] pt_bits_def[simp]
pageBits_def[simp] mask_lower_twice[simp]
word_bool_alg.conj_assoc[symmetric,simp] obj_at_def[simp]
ARM_Structs_A.pde.splits[split]
ARM_Structs_A.pte.splits[split]
Arch_Structs_A.pde.splits[split]
Arch_Structs_A.pte.splits[split]
lemma get_master_pde_wp:
"\<lbrace>\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s
\<longrightarrow> Q (case (pd (ucast (p && ~~ mask 6 && mask pd_bits >> 2))) of
ARM_Structs_A.pde.SuperSectionPDE x xa xb \<Rightarrow> pd (ucast (p && ~~ mask 6 && mask pd_bits >> 2))
Arch_Structs_A.pde.SuperSectionPDE x xa xb \<Rightarrow> pd (ucast (p && ~~ mask 6 && mask pd_bits >> 2))
| _ \<Rightarrow> pd (ucast (p && mask pd_bits >> 2))) s\<rbrace>
get_master_pde p
\<lbrace>Q\<rbrace>"
@ -132,7 +132,7 @@ lemma get_pte_inv [wp]:
lemma get_master_pte_wp:
"\<lbrace>\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s \<longrightarrow>
Q (case pt (ucast (p && ~~ mask 6 && mask pt_bits >> 2)) of
ARM_Structs_A.pte.LargePagePTE x xa xb \<Rightarrow>
Arch_Structs_A.pte.LargePagePTE x xa xb \<Rightarrow>
pt (ucast (p && ~~ mask 6 && mask pt_bits >> 2))
| _ \<Rightarrow> pt (ucast (p && mask pt_bits >> 2)))
s\<rbrace>
@ -364,19 +364,19 @@ lemma arch_derive_cap_inv:
definition
"valid_mapping_entries m \<equiv> case m of
Inl (ARM_Structs_A.InvalidPTE, _) \<Rightarrow> \<top>
| Inl (ARM_Structs_A.LargePagePTE _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pte_at p s
| Inl (ARM_Structs_A.SmallPagePTE _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pte_at p s
| Inr (ARM_Structs_A.InvalidPDE, _) \<Rightarrow> \<top>
| Inr (ARM_Structs_A.PageTablePDE _ _ _, _) \<Rightarrow> \<bottom>
| Inr (ARM_Structs_A.SectionPDE _ _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pde_at p s
| Inr (ARM_Structs_A.SuperSectionPDE _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pde_at p s"
Inl (Arch_Structs_A.InvalidPTE, _) \<Rightarrow> \<top>
| Inl (Arch_Structs_A.LargePagePTE _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pte_at p s
| Inl (Arch_Structs_A.SmallPagePTE _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pte_at p s
| Inr (Arch_Structs_A.InvalidPDE, _) \<Rightarrow> \<top>
| Inr (Arch_Structs_A.PageTablePDE _ _ _, _) \<Rightarrow> \<bottom>
| Inr (Arch_Structs_A.SectionPDE _ _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pde_at p s
| Inr (Arch_Structs_A.SuperSectionPDE _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pde_at p s"
definition "invalid_pte_at p \<equiv> obj_at (\<lambda>ko. \<exists>pt. ko = (ArchObj (PageTable pt))
\<and> pt (ucast (p && mask pt_bits) >> 2) = ARM_Structs_A.pte.InvalidPTE) (p && ~~ mask pt_bits)"
\<and> pt (ucast (p && mask pt_bits) >> 2) = Arch_Structs_A.pte.InvalidPTE) (p && ~~ mask pt_bits)"
definition "invalid_pde_at p \<equiv> obj_at (\<lambda>ko. \<exists>pd. ko = (ArchObj (PageDirectory pd))
\<and> pd (ucast (p && mask pd_bits) >> 2) = ARM_Structs_A.pde.InvalidPDE) (p && ~~ mask pd_bits)"
\<and> pd (ucast (p && mask pd_bits) >> 2) = Arch_Structs_A.pde.InvalidPDE) (p && ~~ mask pd_bits)"
definition
"valid_slots m \<equiv> case m of
@ -676,7 +676,7 @@ lemma lookup_pt_slot_ptes_aligned_valid:
done
lemma p_0x3C_shift:
"is_aligned p 6 \<Longrightarrow>
"is_aligned (p :: word32) 6 \<Longrightarrow>
(\<forall>p\<in>set [p , p + 4 .e. p + 0x3C]. f p) = (\<forall>x\<in>set [0, 4 .e. 0x3C]. f (x + p))"
apply (clarsimp simp: upto_enum_step_def add.commute)
apply (frule is_aligned_no_overflow, simp add: word_bits_def)
@ -1285,7 +1285,7 @@ crunch interrupt_states[wp]: set_pt "\<lambda>s. P (interrupt_states s)"
lemma set_pt_arch_objs [wp]:
"\<lbrace>valid_arch_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (ARM_Structs_A.PageTable pt) s)\<rbrace>
"\<lbrace>valid_arch_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (Arch_Structs_A.PageTable pt) s)\<rbrace>
set_pt p pt
\<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (simp add: set_pt_def)
@ -1372,7 +1372,7 @@ lemma set_pt_table_caps [wp]:
"\<lbrace>valid_table_caps and (\<lambda>s. valid_caps (caps_of_state s) s) and
(\<lambda>s. ((\<exists>slot. caps_of_state s slot =
Some (cap.ArchObjectCap (arch_cap.PageTableCap p None))) \<longrightarrow>
pt = (\<lambda>x. ARM_Structs_A.InvalidPTE)) \<or>
pt = (\<lambda>x. Arch_Structs_A.InvalidPTE)) \<or>
(\<forall>slot. \<exists>asid. caps_of_state s slot =
Some (cap.ArchObjectCap (arch_cap.PageTableCap p (Some asid)))))\<rbrace>
set_pt p pt
@ -1542,7 +1542,7 @@ lemma set_pt_arch_caps [wp]:
(\<lambda>s. valid_caps (caps_of_state s) s) and
(\<lambda>s. ((\<exists>slot. caps_of_state s slot =
Some (cap.ArchObjectCap (arch_cap.PageTableCap p None))) \<longrightarrow>
pt = (\<lambda>x. ARM_Structs_A.InvalidPTE)) \<or>
pt = (\<lambda>x. Arch_Structs_A.InvalidPTE)) \<or>
(\<forall>slot. \<exists>asid. caps_of_state s slot =
Some (cap.ArchObjectCap (arch_cap.PageTableCap p (Some asid))))) and
(\<lambda>s. ((\<exists>\<rhd> p) s \<longrightarrow> (\<forall>x. valid_pte (pt x) s)) \<and>
@ -1673,10 +1673,10 @@ crunch valid_irq_states[wp]: set_pd "valid_irq_states"
lemma set_pt_invs:
"\<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>\<rhd>p) s \<longrightarrow> valid_arch_obj (Arch_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>
(pt = (\<lambda>x. ARM_Structs_A.InvalidPTE) \<or> asid \<noteq> None)) and
(pt = (\<lambda>x. Arch_Structs_A.InvalidPTE) \<or> asid \<noteq> None)) and
(\<lambda>s. \<forall>ref. (ref \<unrhd> p) s \<longrightarrow>
(\<forall>x p. pte_ref_pages (pt x) = Some p \<longrightarrow>
(\<exists>p' cap. caps_of_state s p' = Some cap \<and>
@ -1731,10 +1731,10 @@ lemma vs_lookup_pages_pt_eq:
apply (erule (2) vs_lookup_pagesE_alt)
apply (clarsimp simp: obj_at_def)+
apply (clarsimp simp: obj_at_def pde_ref_pages_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
apply (erule (5) vs_lookup_pdI)
apply (clarsimp simp: obj_at_def pte_ref_pages_def
split: ARM_Structs_A.pte.splits)
split: Arch_Structs_A.pte.splits)
done
@ -1750,7 +1750,7 @@ lemma store_pte_invs [wp]:
(\<lambda>s. \<exists>slot asid. caps_of_state s slot =
Some (cap.ArchObjectCap
(arch_cap.PageTableCap (p && ~~ mask pt_bits) asid)) \<and>
(pte = ARM_Structs_A.InvalidPTE \<or> asid \<noteq> None)) and
(pte = Arch_Structs_A.InvalidPTE \<or> asid \<noteq> None)) and
(\<lambda>s. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow>
(\<forall>q. pte_ref_pages pte = Some q \<longrightarrow>
(\<exists>p' cap. caps_of_state s p' = Some cap \<and>
@ -1948,8 +1948,8 @@ crunch interrupt_states[wp]: set_asid_pool "\<lambda>s. P (interrupt_states s)"
lemma set_asid_pool_arch_objs_unmap':
"\<lbrace>valid_arch_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (ARM_Structs_A.ASIDPool ap) s) and
obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ARM_Structs_A.ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace>
"\<lbrace>valid_arch_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_arch_obj (Arch_Structs_A.ASIDPool ap) s) and
obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (Arch_Structs_A.ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace>
set_asid_pool p ap \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (simp add: set_asid_pool_def)
apply (wp get_object_wp set_object_arch_objs)
@ -1962,7 +1962,7 @@ lemma set_asid_pool_arch_objs_unmap':
lemma set_asid_pool_arch_objs_unmap:
"\<lbrace>valid_arch_objs and ko_at (ArchObj (ARM_Structs_A.ASIDPool ap)) p\<rbrace>
"\<lbrace>valid_arch_objs and ko_at (ArchObj (Arch_Structs_A.ASIDPool ap)) p\<rbrace>
set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (wp set_asid_pool_arch_objs_unmap')
apply (clarsimp simp: obj_at_def graph_of_restrict_map)
@ -1992,7 +1992,7 @@ lemma vs_lookup_pages_stateI:
lemma set_asid_pool_vs_lookup_unmap':
"\<lbrace>valid_vs_lookup and
obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ARM_Structs_A.ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace>
obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (Arch_Structs_A.ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace>
set_asid_pool p ap \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>"
apply (simp add: valid_vs_lookup_def pred_conj_def)
apply (rule hoare_lift_Pf2 [where f=caps_of_state];wp?)
@ -2011,7 +2011,7 @@ lemma set_asid_pool_vs_lookup_unmap':
lemma set_asid_pool_vs_lookup_unmap:
"\<lbrace>valid_vs_lookup and ko_at (ArchObj (ARM_Structs_A.ASIDPool ap)) p\<rbrace>
"\<lbrace>valid_vs_lookup and ko_at (ArchObj (Arch_Structs_A.ASIDPool ap)) p\<rbrace>
set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>"
apply (wp set_asid_pool_vs_lookup_unmap')
by (clarsimp simp: obj_at_def
@ -2059,7 +2059,7 @@ crunch v_ker_map[wp]: set_asid_pool "valid_kernel_mappings"
lemma set_asid_pool_restrict_asid_map:
"\<lbrace>valid_asid_map and ko_at (ArchObj (ARM_Structs_A.ASIDPool ap)) p and
"\<lbrace>valid_asid_map and ko_at (ArchObj (Arch_Structs_A.ASIDPool ap)) p and
(\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid \<notin> S \<longrightarrow>
arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow>
arm_asid_map (arch_state s) asid = None)\<rbrace>
@ -2104,7 +2104,7 @@ lemma set_asid_pool_restrict_asid_map:
lemma set_asid_pool_asid_map_unmap:
"\<lbrace>valid_asid_map and ko_at (ArchObj (ARM_Structs_A.ASIDPool ap)) p and
"\<lbrace>valid_asid_map and ko_at (ArchObj (Arch_Structs_A.ASIDPool ap)) p and
(\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow>
ucast asid = x \<longrightarrow>
arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow>
@ -2115,7 +2115,7 @@ lemma set_asid_pool_asid_map_unmap:
lemma set_asid_pool_arch_objs_unmap_single:
"\<lbrace>valid_arch_objs and ko_at (ArchObj (ARM_Structs_A.ASIDPool ap)) p\<rbrace>
"\<lbrace>valid_arch_objs and ko_at (ArchObj (Arch_Structs_A.ASIDPool ap)) p\<rbrace>
set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
using set_asid_pool_arch_objs_unmap[where S="- {x}"]
by (simp add: restrict_map_def fun_upd_def if_flip)
@ -2183,7 +2183,7 @@ lemma set_asid_pool_vms[wp]:
lemma set_asid_pool_invs_restrict:
"\<lbrace>invs and ko_at (ArchObj (ARM_Structs_A.ASIDPool ap)) p and
"\<lbrace>invs and ko_at (ArchObj (Arch_Structs_A.ASIDPool ap)) p and
(\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid \<notin> S \<longrightarrow>
arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow>
arm_asid_map (arch_state s) asid = None)\<rbrace>
@ -2212,7 +2212,7 @@ lemma mdb_cte_at_set_asid_pool[wp]:
done
lemma set_asid_pool_invs_unmap:
"\<lbrace>invs and ko_at (ArchObj (ARM_Structs_A.ASIDPool ap)) p and
"\<lbrace>invs and ko_at (ArchObj (Arch_Structs_A.ASIDPool ap)) p and
(\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid = x \<longrightarrow>
arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow>
arm_asid_map (arch_state s) asid = None)\<rbrace>
@ -3319,12 +3319,12 @@ lemma set_pd_vms[wp]:
(* FIXME: Move to Invariants_A *)
lemma vs_refs_pages_subset: "vs_refs ko \<subseteq> vs_refs_pages ko"
apply (clarsimp simp: vs_refs_pages_def vs_refs_def graph_of_def pde_ref_def pde_ref_pages_def
split: Structures_A.kernel_object.splits arch_kernel_obj.splits ARM_Structs_A.pde.splits)
split: Structures_A.kernel_object.splits arch_kernel_obj.splits Arch_Structs_A.pde.splits)
subgoal for "fun" a b
using
imageI[where A="{(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages (fun x)) = Some y}"
and f="(\<lambda>(r, y). (VSRef (ucast r) (Some APageDirectory), y))" and x="(a,b)"]
by (clarsimp simp: pde_ref_def pde_ref_pages_def split: if_splits ARM_Structs_A.pde.splits)+
by (clarsimp simp: pde_ref_def pde_ref_pages_def split: if_splits Arch_Structs_A.pde.splits)+
done
@ -3350,7 +3350,7 @@ lemma vs_refs_pages_subset2:
imageI[where
A="{(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (fun x)) = Some y}"
and f="(\<lambda>(r, y). (VSRef (ucast r) (Some APageDirectory), y))" and x="(a,b)"]
apply (clarsimp simp: pde_ref_def pde_ref_pages_def split: ARM_Structs_A.pde.splits)
apply (clarsimp simp: pde_ref_def pde_ref_pages_def split: Arch_Structs_A.pde.splits)
apply (drule bspec, simp)+
apply (clarsimp simp: obj_at_def a_type_def)
apply (drule bspec, simp)+
@ -3391,7 +3391,7 @@ lemma store_pde_invs_unmap:
"\<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>
and K (pde = Arch_Structs_A.InvalidPDE)\<rbrace>
store_pde p pde \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: store_pde_def del: split_paired_Ex)
apply (wp set_pd_invs_unmap)

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

@ -1133,7 +1133,7 @@ lemma create_mappings_empty [wp]:
lemma empty_pde_atI:
"\<lbrakk> ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s;
pd (ucast (p && mask pd_bits >> 2)) = ARM_Structs_A.InvalidPDE \<rbrakk> \<Longrightarrow>
pd (ucast (p && mask pd_bits >> 2)) = Arch_Structs_A.InvalidPDE \<rbrakk> \<Longrightarrow>
empty_pde_at p s"
by (fastforce simp add: empty_pde_at_def)
@ -1318,7 +1318,7 @@ lemma create_mapping_entries_same_refs:
apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def
mask_cap_def cap_rights_update_def)
apply (clarsimp split: Structures_A.cap.splits )
apply (clarsimp simp: acap_rights_update_def split: ARM_Structs_A.arch_cap.splits)
apply (clarsimp simp: acap_rights_update_def split: Arch_Structs_A.arch_cap.splits)
apply (frule (1) vs_lookup_and_unique_refs)
apply (simp_all add: table_cap_ref_def obj_refs_def)[4]
apply (frule_tac p=pd and p'="Platform.ptrFromPAddr x" in vs_lookup_step)
@ -1353,7 +1353,7 @@ lemma create_mapping_entries_same_refs:
apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def
mask_cap_def cap_rights_update_def)
apply (clarsimp split: Structures_A.cap.splits )
apply (clarsimp simp: acap_rights_update_def split: ARM_Structs_A.arch_cap.splits)
apply (clarsimp simp: acap_rights_update_def split: Arch_Structs_A.arch_cap.splits)
apply (frule (1) vs_lookup_and_unique_refs)
apply (simp_all add: table_cap_ref_def obj_refs_def)[4]
apply (frule_tac p=pd and p'="Platform.ptrFromPAddr x" in vs_lookup_step)
@ -1380,7 +1380,7 @@ lemma create_mapping_entries_same_refs:
apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def
mask_cap_def cap_rights_update_def)
apply (clarsimp split: Structures_A.cap.splits )
apply (clarsimp simp: acap_rights_update_def split: ARM_Structs_A.arch_cap.splits)
apply (clarsimp simp: acap_rights_update_def split: Arch_Structs_A.arch_cap.splits)
apply (frule (1) vs_lookup_and_unique_refs)
apply (simp_all add: table_cap_ref_def obj_refs_def)[4]
apply (drule (1) ref_is_unique)
@ -1394,7 +1394,7 @@ lemma create_mapping_entries_same_refs:
apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def
mask_cap_def cap_rights_update_def)
apply (clarsimp split: Structures_A.cap.splits )
apply (clarsimp simp: acap_rights_update_def split: ARM_Structs_A.arch_cap.splits)
apply (clarsimp simp: acap_rights_update_def split: Arch_Structs_A.arch_cap.splits)
apply (frule (1) vs_lookup_and_unique_refs)
apply (simp_all add: table_cap_ref_def obj_refs_def)[4]
apply (drule (1) ref_is_unique)
@ -1555,7 +1555,7 @@ lemma arch_decode_inv_wf[wp]:
apply (clarsimp simp:diminished_def)
apply (simp add: arch_decode_invocation_def Let_def split_def
cong: if_cong split del: split_if)
apply (cases "invocation_type label = ARMPageMap")
apply (cases "invocation_type label = ArchInvocationLabel ARMPageMap")
apply (rename_tac word rights vmpage_size option)
apply (simp split del: split_if)
apply (rule hoare_pre)
@ -1584,7 +1584,7 @@ lemma arch_decode_inv_wf[wp]:
elim: is_aligned_weaken split: vmpage_size.split
intro!: is_aligned_addrFromPPtr pbfs_atleast_pageBits,
(fastforce intro: diminished_pd_self)+)[1]
apply (cases "invocation_type label = ARMPageRemap")
apply (cases "invocation_type label = ArchInvocationLabel ARMPageRemap")
apply (rename_tac word rights vmpage_size option)
apply (simp split del: split_if)
apply (rule hoare_pre)
@ -1608,7 +1608,7 @@ lemma arch_decode_inv_wf[wp]:
elim: is_aligned_weaken
intro!: is_aligned_addrFromPPtr pbfs_atleast_pageBits,
fastforce+)[1]
apply (cases "invocation_type label = ARMPageUnmap")
apply (cases "invocation_type label = ArchInvocationLabel ARMPageUnmap")
apply (simp split del: split_if)
apply (rule hoare_pre, wp)
apply (clarsimp simp: valid_arch_inv_def valid_page_inv_def)
@ -1620,7 +1620,7 @@ lemma arch_decode_inv_wf[wp]:
apply (fastforce simp: vmsz_aligned_def elim: is_aligned_weaken intro!: pbfs_atleast_pageBits)
apply (erule cte_wp_at_weakenE)
apply (clarsimp simp: is_arch_diminished_def is_cap_simps)
apply (cases "isPageFlush (invocation_type label)")
apply (cases "isPageFlushLabel (invocation_type label)")
apply (simp split del: split_if)
apply (rule hoare_pre)
apply (wp whenE_throwError_wp static_imp_wp hoare_drop_imps)
@ -1628,7 +1628,7 @@ lemma arch_decode_inv_wf[wp]:
apply (wp find_pd_for_asid_pd_at_asid | wpc)+
apply (clarsimp simp: valid_cap_def mask_def)
apply (simp split del: split_if)
apply (cases "invocation_type label = ARMPageGetAddress")
apply (cases "invocation_type label = ArchInvocationLabel ARMPageGetAddress")
apply (simp split del: split_if)
apply (rule hoare_pre, wp)
apply (clarsimp simp: valid_arch_inv_def valid_page_inv_def)
@ -1654,7 +1654,7 @@ lemma arch_decode_inv_wf[wp]:
apply (erule impE)
apply clarsimp
apply (erule impE)
apply (clarsimp split:ARM_Structs_A.pde.splits)
apply (clarsimp split:Arch_Structs_A.pde.splits)
apply assumption
apply ((wp whenE_throwError_wp hoare_vcg_all_lift_R
find_pd_for_asid_lookup_slot [unfolded lookup_pd_slot_def Let_def]
@ -1707,7 +1707,7 @@ lemma arch_decode_inv_wf[wp]:
apply (simp add: kernel_base_def)
apply (clarsimp simp: cte_wp_at_def is_arch_diminished_def is_cap_simps)
apply (simp add: arch_decode_invocation_def Let_def split del: split_if)
apply (cases "isPDFlush (invocation_type label)")
apply (cases "isPDFlushLabel (invocation_type label)")
apply (simp split del: split_if)
apply (rule hoare_pre)
apply (wp whenE_throwError_wp static_imp_wp hoare_drop_imp | wpc | simp)+

2
proof/invariant-abstract/Bits_AI.thy
View File

@ -111,4 +111,4 @@ lemma pbfs_atleast_pageBits:
"pageBits \<le> pageBitsForSize sz"
by (cases sz) (auto simp: pageBits_def)
end
end

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

@ -235,12 +235,9 @@ lemma derive_cap_zobjrefs:
lemma update_cap_objrefs:
"\<lbrakk> update_cap_data P dt cap \<noteq> cap.NullCap \<rbrakk> \<Longrightarrow>
obj_refs (update_cap_data P dt cap) = obj_refs cap"
apply (case_tac cap,
by (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
lemma update_cap_zobjrefs:
@ -278,8 +275,8 @@ lemma update_cap_data_mask_Null [simp]:
"(update_cap_data P x (mask_cap m c) = cap.NullCap) = (update_cap_data P x c = cap.NullCap)"
unfolding update_cap_data_def mask_cap_def
apply (cases c)
apply (auto simp add: the_cnode_cap_def Let_def is_cap_simps cap_rights_update_def badge_update_def)
done
by (auto simp add: the_cnode_cap_def Let_def is_cap_simps cap_rights_update_def badge_update_def
arch_update_cap_data_def)
lemma cap_master_update_cap_data:
@ -1321,7 +1318,7 @@ lemma copy_of_cap_range:
apply (cases cap', simp_all add: same_object_as_def)
apply (clarsimp simp: is_cap_simps bits_of_def cap_range_def
split: cap.split_asm)+
apply (subgoal_tac "\<exists>acap . cap = cap.ArchObjectCap acap", clarsimp)
apply (rename_tac acap' acap)
apply (case_tac acap, simp_all)
apply (clarsimp split: arch_cap.split_asm cap.split_asm)+
done
@ -1942,7 +1939,7 @@ lemma copy_of_zobj_refs:
apply (cases cap', simp_all add: same_object_as_def)
apply (clarsimp simp: is_cap_simps bits_of_def
split: cap.split_asm)+
apply (subgoal_tac "\<exists>acap . cap = cap.ArchObjectCap acap", clarsimp)
apply (rename_tac acap' acap)
apply (case_tac acap, simp_all)
apply (clarsimp split: arch_cap.split_asm cap.split_asm)+
done
@ -1960,22 +1957,15 @@ lemma copy_of_is_zombie:
lemma copy_of_reply_cap:
"copy_of (cap.ReplyCap t False) cap \<Longrightarrow> cap = cap.ReplyCap t False"
apply (clarsimp simp: copy_of_def is_cap_simps)
apply (cases cap, simp_all add: same_object_as_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all)
done
by (cases cap, simp_all add: same_object_as_def)
lemma copy_of_cap_irqs:
"copy_of cap cap' \<Longrightarrow> cap_irqs cap = cap_irqs cap'"
apply (clarsimp simp: copy_of_def cap_irqs_def split: split_if_asm)
apply (cases cap', simp_all add: same_object_as_def)
apply (clarsimp simp: is_cap_simps bits_of_def cap_range_def
by (clarsimp simp: is_cap_simps bits_of_def cap_range_def
split: cap.split_asm)+
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all)
apply (clarsimp split: arch_cap.split_asm cap.split_asm)+
done
lemma cap_swap_valid_idle[wp]:

2
proof/invariant-abstract/CSpaceInv_AI.thy
View File

@ -1604,7 +1604,7 @@ lemma unique_table_refsD:
lemma table_cap_ref_vs_cap_ref_Some:
"table_cap_ref x = Some y \<Longrightarrow> vs_cap_ref x = Some y"
by (clarsimp simp: table_cap_ref_def vs_cap_ref_def
split: Structures_A.cap.splits ARM_Structs_A.arch_cap.splits)
split: Structures_A.cap.splits Arch_Structs_A.arch_cap.splits)
lemma set_cap_valid_vs_lookup:

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

@ -561,11 +561,11 @@ where
| Structures_A.IRQHandlerCap irq \<Rightarrow> True
| Structures_A.Zombie r b n \<Rightarrow> True
| Structures_A.ArchObjectCap ac \<Rightarrow> (case ac of
ARM_Structs_A.ASIDPoolCap r as \<Rightarrow> True
| ARM_Structs_A.ASIDControlCap \<Rightarrow> False
| ARM_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> False
| ARM_Structs_A.PageTableCap r mapdata \<Rightarrow> True
| ARM_Structs_A.PageDirectoryCap r mapdata \<Rightarrow> True)"
Arch_Structs_A.ASIDPoolCap r as \<Rightarrow> True
| Arch_Structs_A.ASIDControlCap \<Rightarrow> False
| Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> False
| Arch_Structs_A.PageTableCap r mapdata \<Rightarrow> True
| Arch_Structs_A.PageDirectoryCap r mapdata \<Rightarrow> True)"
lemmas final_matters_simps[simp]
@ -889,8 +889,8 @@ end
definition
"cap_vptr cap \<equiv> case cap of
Structures_A.ArchObjectCap (ARM_Structs_A.PageCap _ _ _ (Some (_, vptr))) \<Rightarrow> Some vptr
| Structures_A.ArchObjectCap (ARM_Structs_A.PageTableCap _ (Some (_, vptr))) \<Rightarrow> Some vptr
Structures_A.ArchObjectCap (Arch_Structs_A.PageCap _ _ _ (Some (_, vptr))) \<Rightarrow> Some vptr
| Structures_A.ArchObjectCap (Arch_Structs_A.PageTableCap _ (Some (_, vptr))) \<Rightarrow> Some vptr
| _ \<Rightarrow> None"

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

@ -1810,12 +1810,11 @@ lemma timer_tick_valid_sched[wp]:
| wp gts_wp reschedule_required_valid_sched tcb_sched_action_append_valid_blocked
| wpc | rule hoare_strengthen_post, rule dec_domain_time_valid_sched,
simp add: valid_sched_def valid_sched_action_def)+
apply (fastforce simp: valid_sched_def valid_etcbs_def valid_queues_def pred_tcb_weakenE
by (fastforce simp: valid_sched_def valid_etcbs_def valid_queues_def pred_tcb_weakenE
valid_sched_action_def weak_valid_sched_action_def etcb_at_def is_etcb_at_def
get_etcb_def in_cur_domain_def ct_in_cur_domain_2_def switch_in_cur_domain_def
valid_idle_etcb_2_def
split: option.splits)
done
lemma cancel_badged_sends_filterM_valid_etcbs[wp]:
"\<lbrace>valid_etcbs\<rbrace>
@ -2192,10 +2191,9 @@ lemma possible_switch_to_not_queued:
\<lbrace>\<lambda>_. not_queued t\<rbrace>"
apply (simp add: possible_switch_to_def reschedule_required_def
set_scheduler_action_def tcb_sched_action_def | wp | wpc)+
apply (fastforce simp: etcb_at_def tcb_sched_enqueue_def simple_sched_action_def
by (fastforce simp: etcb_at_def tcb_sched_enqueue_def simple_sched_action_def
not_queued_def scheduler_act_not_def
split: option.splits)
done
crunch sched_act_not[wp]: attempt_switch_to, switch_if_required_to

23
proof/invariant-abstract/EmptyFail_AI.thy
View File

@ -298,25 +298,24 @@ crunch (empty_fail) empty_fail[wp]: find_pd_for_asid, get_master_pde, check_vp_a
lemmas empty_fail_return[wp]
lemma arch_decode_ARMASIDControlMakePool_empty_fail:
"invocation_type label = ARMASIDControlMakePool
"invocation_type label = ArchInvocationLabel ARMASIDControlMakePool
\<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)"
apply (simp add: arch_decode_invocation_def Let_def)
apply (intro impI conjI allI)
apply (simp add: isPageFlush_def isPDFlush_def split: arch_cap.splits)+
apply (simp add: isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits)+
apply (rule impI)
apply (simp add: split_def)
apply wp
apply simp
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
apply (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: split_if_asm)
apply (simp add: Let_def split: cap.splits arch_cap.splits option.splits | wp | intro conjI impI allI)+
done
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: split_if_asm)
by (simp add: Let_def split: cap.splits arch_cap.splits option.splits | wp | intro conjI impI allI)+
lemma arch_decode_ARMASIDPoolAssign_empty_fail:
"invocation_type label = ARMASIDPoolAssign
"invocation_type label = ArchInvocationLabel ARMASIDPoolAssign
\<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)"
apply (simp add: arch_decode_invocation_def split_def Let_def isPageFlush_def isPDFlush_def split: arch_cap.splits cap.splits option.splits | intro impI allI)+
apply (simp add: arch_decode_invocation_def split_def Let_def isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits cap.splits option.splits | intro impI allI)+
apply (rule empty_fail_bindE)
apply simp
apply (rule empty_fail_bindE)
@ -327,16 +326,18 @@ lemma arch_decode_ARMASIDPoolAssign_empty_fail:
apply ((simp | wp)+)[1]
apply (subst bindE_assoc[symmetric])
apply (rule empty_fail_bindE)
apply (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def bind_def return_def returnOk_def lift_def liftE_def select_ext_def select_def gets_def get_def assert_def fail_def)
subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def bind_def return_def returnOk_def lift_def liftE_def select_ext_def select_def gets_def get_def assert_def fail_def)
apply wp
done
lemma arch_decode_invocation_empty_fail[wp]:
"empty_fail (arch_decode_invocation label b c d e f)"
apply (case_tac "invocation_type label")
prefer 44
prefer 45
apply ((simp add: arch_decode_ARMASIDControlMakePool_empty_fail arch_decode_ARMASIDPoolAssign_empty_fail)+)[2]
apply (find_goal \<open>match premises in "_ = ArchInvocationLabel _" \<Rightarrow> \<open>-\<close>\<close>)
apply (rename_tac alabel)
apply (case_tac alabel; simp)
apply (find_goal \<open>erule arch_decode_ARMASIDControlMakePool_empty_fail\<close>)
apply (find_goal \<open>erule arch_decode_ARMASIDPoolAssign_empty_fail\<close>)
by ((simp add: arch_decode_invocation_def Let_def split: arch_cap.splits cap.splits option.splits | wp | intro conjI impI allI)+)
crunch (empty_fail) empty_fail[wp]: maskInterrupt, empty_slot, setInterruptMode,

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

@ -1664,7 +1664,7 @@ lemma tcb_cap_valid_pagedirectory:
lemma store_pde_unmap_empty:
"\<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
store_pde pd_slot ARM_Structs_A.pde.InvalidPDE
store_pde pd_slot Arch_Structs_A.pde.InvalidPDE
\<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>"
apply (clarsimp simp: store_pde_def set_pd_def set_object_def)
apply (wp get_object_wp)
@ -1679,7 +1679,7 @@ crunch empty[wp]: find_free_hw_asid, store_hw_asid, load_hw_asid, set_vm_root_fo
lemma store_pte_unmap_empty:
"\<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
store_pte xa ARM_Structs_A.pte.InvalidPTE
store_pte xa Arch_Structs_A.pte.InvalidPTE
\<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>"
apply (wp get_object_wp | simp add: store_pte_def set_pt_def set_object_def)+
apply (clarsimp simp: obj_at_def empty_table_def)
@ -1752,7 +1752,7 @@ lemma unmap_page_table_empty:
lemma mapM_x_store_pte_valid_arch_objs:
"\<lbrace>invs and (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and>
(\<forall>x \<in> set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap)) \<rbrace>
mapM_x (\<lambda>p. store_pte p ARM_Structs_A.InvalidPTE) pteptrs
mapM_x (\<lambda>p. store_pte p Arch_Structs_A.InvalidPTE) pteptrs
\<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
apply (rule hoare_strengthen_post)
apply (wp mapM_x_wp')
@ -1765,7 +1765,7 @@ lemma mapM_x_swp_store_empty_table_set:
and pspace_aligned
and K ((UNIV :: word8 set) \<subseteq> (\<lambda>sl. ucast ((sl && mask pt_bits) >> 2)) ` set slots
\<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p))\<rbrace>
mapM_x (swp store_pte ARM_Structs_A.InvalidPTE) slots
mapM_x (swp store_pte Arch_Structs_A.InvalidPTE) slots
\<lbrace>\<lambda>rv s. obj_at (empty_table (S s)) p s\<rbrace>"
apply (rule hoare_strengthen_post)
apply (rule mapM_x_swp_store_empty_table)
@ -2016,7 +2016,7 @@ lemma page_directory_at_def2:
definition
pde_wp_at :: "(ARM_Structs_A.pde \<Rightarrow> bool) \<Rightarrow> word32 \<Rightarrow> (12 word) \<Rightarrow> 'z state \<Rightarrow> bool"
pde_wp_at :: "(Arch_Structs_A.pde \<Rightarrow> bool) \<Rightarrow> word32 \<Rightarrow> (12 word) \<Rightarrow> 'z state \<Rightarrow> bool"
where
"pde_wp_at P ptr slot s \<equiv>
(case (kheap s ptr) of
@ -2036,9 +2036,9 @@ lemma store_pde_pde_wp_at:
lemma store_pde_pde_wp_at2:
"\<lbrace>pde_wp_at (\<lambda>pde. pde = ARM_Structs_A.pde.InvalidPDE) ptr slot\<rbrace>
store_pde p' ARM_Structs_A.pde.InvalidPDE
\<lbrace>\<lambda>_. pde_wp_at (\<lambda>pde. pde = ARM_Structs_A.pde.InvalidPDE) ptr slot\<rbrace>"
"\<lbrace>pde_wp_at (\<lambda>pde. pde = Arch_Structs_A.pde.InvalidPDE) ptr slot\<rbrace>
store_pde p' Arch_Structs_A.pde.InvalidPDE
\<lbrace>\<lambda>_. pde_wp_at (\<lambda>pde. pde = Arch_Structs_A.pde.InvalidPDE) ptr slot\<rbrace>"
apply (wp
| simp add: store_pde_def set_pd_def set_object_def get_object_def
obj_at_def pde_wp_at_def
@ -2049,7 +2049,7 @@ lemma store_pde_pde_wp_at2:
lemma obj_at_empty_tableI:
"invs s \<and>
(\<forall>x. x \<notin> kernel_mapping_slots \<longrightarrow>
pde_wp_at (\<lambda>pde. pde = ARM_Structs_A.pde.InvalidPDE) p x s)
pde_wp_at (\<lambda>pde. pde = Arch_Structs_A.pde.InvalidPDE) p x s)
\<Longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) p s"
apply safe
apply (simp add: obj_at_def empty_table_def pde_wp_at_def)
@ -2166,7 +2166,7 @@ lemma pd_shifting_global_refs:
lemma mapM_x_store_pde_InvalidPDE_empty:
"\<lbrace>(invs and (\<lambda>s. word \<notin> global_refs s)) and K(is_aligned word pd_bits)\<rbrace>
mapM_x (swp store_pde ARM_Structs_A.pde.InvalidPDE)
mapM_x (swp store_pde Arch_Structs_A.pde.InvalidPDE)
(map (\<lambda>a. (a << 2) + word) [0.e.(kernel_base >> 20) - 1])
\<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>"
apply (rule hoare_gen_asm)
@ -2373,14 +2373,14 @@ lemma replaceable_or_arch_update_pg:
done
lemma store_pde_arch_objs_invalid:
"\<lbrace>valid_arch_objs\<rbrace> store_pde p ARM_Structs_A.pde.InvalidPDE \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
"\<lbrace>valid_arch_objs\<rbrace> store_pde p Arch_Structs_A.pde.InvalidPDE \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (wp store_pde_arch_objs_unmap)
apply (simp add: pde_ref_def)
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
mapM_x (\<lambda>x. store_pde x Arch_Structs_A.pde.InvalidPDE) slots
\<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>"
apply (rule hoare_gen_asm)
apply simp
@ -2398,21 +2398,21 @@ lemma mapM_x_swp_store_invalid_pte_invs:
"\<lbrace>invs and (\<lambda>s. \<exists>slot. cte_wp_at
(\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and>
is_pt_cap c) slot s)\<rbrace>
mapM_x (\<lambda>x. store_pte x ARM_Structs_A.pte.InvalidPTE) slots \<lbrace>\<lambda>_. invs\<rbrace>"
mapM_x (\<lambda>x. store_pte x Arch_Structs_A.pte.InvalidPTE) slots \<lbrace>\<lambda>_. invs\<rbrace>"
by (simp add:
mapM_x_swp_store_pte_invs[unfolded swp_def,
where pte=ARM_Structs_A.pte.InvalidPTE, simplified])
where pte=Arch_Structs_A.pte.InvalidPTE, simplified])
lemma mapM_x_swp_store_invalid_pde_invs:
"\<lbrace>invs and
(\<lambda>s. \<forall>sl\<in>set slots.
ucast (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and
(\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s)\<rbrace>
mapM_x (\<lambda>x. store_pde x ARM_Structs_A.pde.InvalidPDE) slots
mapM_x (\<lambda>x. store_pde x Arch_Structs_A.pde.InvalidPDE) slots
\<lbrace>\<lambda>rv. invs \<rbrace>"
apply (simp add:mapM_x_mapM)
apply (wp mapM_swp_store_pde_invs_unmap[unfolded swp_def,
where pde=ARM_Structs_A.pde.InvalidPDE, simplified])
where pde=Arch_Structs_A.pde.InvalidPDE, simplified])
done
lemma arch_cap_recycle_replaceable:

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

@ -37,7 +37,7 @@ where
primrec
irq_control_inv_valid :: "irq_control_invocation \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"irq_control_inv_valid (Invocations_A.InterruptControl ivk) = \<bottom>"
"irq_control_inv_valid (Invocations_A.ArchInvokeIRQControl ivk) = \<bottom>"
| "irq_control_inv_valid (Invocations_A.IRQControl irq ptr ptr') =
(cte_wp_at (op = cap.NullCap) ptr and
cte_wp_at (op = cap.IRQControlCap) ptr'
@ -72,7 +72,7 @@ crunch inv[wp]: is_irq_active "P"
lemma decode_irq_control_invocation_inv[wp]:
"\<lbrace>P\<rbrace> decode_irq_control_invocation label args slot caps \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: decode_irq_control_invocation_def Let_def
arch_decode_interrupt_control_def whenE_def, safe)
arch_decode_irq_control_def whenE_def, safe)
apply (wp | simp)+
done
@ -85,7 +85,7 @@ lemma decode_irq_control_valid[wp]:
\<lbrace>irq_control_inv_valid\<rbrace>,-"
apply (simp add: decode_irq_control_invocation_def Let_def split_def
lookup_target_slot_def whenE_def
arch_decode_interrupt_control_def
arch_decode_irq_control_def
split del: split_if cong: if_cong)
apply (rule hoare_pre)
apply (wp ensure_empty_stronger | simp add: cte_wp_at_eq_simp

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

@ -156,7 +156,7 @@ where
PageTable pt \<Rightarrow> APageTable
| PageDirectory pd \<Rightarrow> APageDirectory
| DataPage sz \<Rightarrow> AIntData sz
| ARM_Structs_A.ASIDPool f \<Rightarrow> AASIDPool)"
| Arch_Structs_A.ASIDPool f \<Rightarrow> AASIDPool)"
abbreviation
"typ_at T \<equiv> obj_at (\<lambda>ob. a_type ob = T)"
@ -278,13 +278,13 @@ definition
where
"wellformed_acap ac \<equiv>
case ac of
ARM_Structs_A.ASIDPoolCap r as
Arch_Structs_A.ASIDPoolCap r as
\<Rightarrow> is_aligned as asid_low_bits \<and> as \<le> 2^asid_bits - 1
| ARM_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> rghts \<in> valid_vm_rights \<and>
| Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> rghts \<in> valid_vm_rights \<and>
case_option True (wellformed_mapdata sz) mapdata
| ARM_Structs_A.PageTableCap r (Some mapdata) \<Rightarrow>
| Arch_Structs_A.PageTableCap r (Some mapdata) \<Rightarrow>
wellformed_mapdata ARMSection mapdata
| ARM_Structs_A.PageDirectoryCap r (Some asid) \<Rightarrow>
| Arch_Structs_A.PageDirectoryCap r (Some asid) \<Rightarrow>
0 < asid \<and> asid \<le> 2^asid_bits - 1
| _ \<Rightarrow> True"
@ -319,11 +319,11 @@ where
| Structures_A.Zombie r b n \<Rightarrow>
(case b of None \<Rightarrow> tcb_at r s | Some b \<Rightarrow> cap_table_at b r s)
| Structures_A.ArchObjectCap ac \<Rightarrow> (case ac of
ARM_Structs_A.ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s
| ARM_Structs_A.ASIDControlCap \<Rightarrow> True
| ARM_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> typ_at (AArch (AIntData sz)) r s
| ARM_Structs_A.PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s
| ARM_Structs_A.PageDirectoryCap r mapdata\<Rightarrow>typ_at(AArch APageDirectory) r s)"
Arch_Structs_A.ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s
| Arch_Structs_A.ASIDControlCap \<Rightarrow> True
| Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow> typ_at (AArch (AIntData sz)) r s
| Arch_Structs_A.PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s
| Arch_Structs_A.PageDirectoryCap r mapdata\<Rightarrow>typ_at(AArch APageDirectory) r s)"
definition
@ -346,21 +346,21 @@ where
(case b of None \<Rightarrow> tcb_at r s \<and> n \<le> 5
| Some b \<Rightarrow> cap_table_at b r s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0)
| Structures_A.ArchObjectCap ac \<Rightarrow> (case ac of
ARM_Structs_A.ASIDPoolCap r as \<Rightarrow>
Arch_Structs_A.ASIDPoolCap r as \<Rightarrow>
typ_at (AArch AASIDPool) r s \<and> is_aligned as asid_low_bits
\<and> as \<le> 2^asid_bits - 1
| ARM_Structs_A.ASIDControlCap \<Rightarrow> True
| ARM_Structs_A.PageCap r rghts sz mapdata \<Rightarrow>
| Arch_Structs_A.ASIDControlCap \<Rightarrow> True
| Arch_Structs_A.PageCap r rghts sz mapdata \<Rightarrow>
typ_at (AArch (AIntData sz)) r s \<and> rghts \<in> valid_vm_rights \<and>
(case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2^asid_bits - 1
\<and> vmsz_aligned ref sz \<and> ref < kernel_base)
| ARM_Structs_A.PageTableCap r mapdata \<Rightarrow>
| Arch_Structs_A.PageTableCap r mapdata \<Rightarrow>
typ_at (AArch APageTable) r s \<and>
(case mapdata of None \<Rightarrow> True
| Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ asid_bits - 1
\<and> vref < kernel_base
\<and> is_aligned vref (pageBitsForSize ARMSection))
| ARM_Structs_A.PageDirectoryCap r mapdata \<Rightarrow>
| Arch_Structs_A.PageDirectoryCap r mapdata \<Rightarrow>
typ_at (AArch APageDirectory) r s \<and>
case_option True (\<lambda>asid. 0 < asid \<and> asid \<le> 2^asid_bits - 1) mapdata))"
@ -537,57 +537,57 @@ where
\<longrightarrow> (\<forall>w \<in> kernel_mapping_slots. pd w = pd' w)"
primrec
valid_pte :: "ARM_Structs_A.pte \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
valid_pte :: "Arch_Structs_A.pte \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"valid_pte (ARM_Structs_A.InvalidPTE) = \<top>"
| "valid_pte (ARM_Structs_A.LargePagePTE ptr x y) =
"valid_pte (Arch_Structs_A.InvalidPTE) = \<top>"
| "valid_pte (Arch_Structs_A.LargePagePTE ptr x y) =
(\<lambda>s. is_aligned ptr pageBits \<and>
typ_at (AArch (AIntData ARMLargePage)) (Platform.ptrFromPAddr ptr) s)"
| "valid_pte (ARM_Structs_A.SmallPagePTE ptr x y) =
| "valid_pte (Arch_Structs_A.SmallPagePTE ptr x y) =
(\<lambda>s. is_aligned ptr pageBits \<and>
typ_at (AArch (AIntData ARMSmallPage)) (Platform.ptrFromPAddr ptr) s)"
primrec
valid_pde :: "ARM_Structs_A.pde \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
valid_pde :: "Arch_Structs_A.pde \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"valid_pde (ARM_Structs_A.InvalidPDE) = \<top>"
| "valid_pde (ARM_Structs_A.SectionPDE ptr x y z) =
"valid_pde (Arch_Structs_A.InvalidPDE) = \<top>"
| "valid_pde (Arch_Structs_A.SectionPDE ptr x y z) =
(\<lambda>s. is_aligned ptr pageBits \<and>
typ_at (AArch (AIntData ARMSection)) (Platform.ptrFromPAddr ptr) s)"
| "valid_pde (ARM_Structs_A.SuperSectionPDE ptr x z) =
| "valid_pde (Arch_Structs_A.SuperSectionPDE ptr x z) =
(\<lambda>s. is_aligned ptr pageBits \<and>
typ_at (AArch (AIntData ARMSuperSection))
(Platform.ptrFromPAddr ptr) s)"
| "valid_pde (ARM_Structs_A.PageTablePDE ptr x z) =
| "valid_pde (Arch_Structs_A.PageTablePDE ptr x z) =
(typ_at (AArch APageTable) (Platform.ptrFromPAddr ptr))"
primrec
valid_arch_obj :: "arch_kernel_obj \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"valid_arch_obj (ARM_Structs_A.ASIDPool pool) =
"valid_arch_obj (Arch_Structs_A.ASIDPool pool) =
(\<lambda>s. \<forall>x \<in> ran pool. typ_at (AArch APageDirectory) x s)"
| "valid_arch_obj (ARM_Structs_A.PageDirectory pd) =
| "valid_arch_obj (Arch_Structs_A.PageDirectory pd) =
(\<lambda>s. \<forall>x \<in> -kernel_mapping_slots. valid_pde (pd x) s)"
| "valid_arch_obj (ARM_Structs_A.PageTable pt) = (\<lambda>s. \<forall>x. valid_pte (pt x) s)"
| "valid_arch_obj (Arch_Structs_A.PageTable pt) = (\<lambda>s. \<forall>x. valid_pte (pt x) s)"
| "valid_arch_obj (DataPage sz) = \<top>"
definition
wellformed_pte :: "ARM_Structs_A.pte \<Rightarrow> bool"
wellformed_pte :: "Arch_Structs_A.pte \<Rightarrow> bool"
where
"wellformed_pte pte \<equiv> case pte of
ARM_Structs_A.pte.LargePagePTE p attr r \<Rightarrow>
Arch_Structs_A.pte.LargePagePTE p attr r \<Rightarrow>
ParityEnabled \<notin> attr \<and> r \<in> valid_vm_rights
| ARM_Structs_A.pte.SmallPagePTE p attr r \<Rightarrow>
| Arch_Structs_A.pte.SmallPagePTE p attr r \<Rightarrow>
ParityEnabled \<notin> attr \<and> r \<in> valid_vm_rights
| _ \<Rightarrow> True"
definition
wellformed_pde :: "ARM_Structs_A.pde \<Rightarrow> bool"
wellformed_pde :: "Arch_Structs_A.pde \<Rightarrow> bool"
where
"wellformed_pde pde \<equiv> case pde of
ARM_Structs_A.pde.PageTablePDE p attr mw \<Rightarrow> attr \<subseteq> {ParityEnabled}
| ARM_Structs_A.pde.SectionPDE p attr mw r \<Rightarrow> r \<in> valid_vm_rights
| ARM_Structs_A.pde.SuperSectionPDE p attr r \<Rightarrow> r \<in> valid_vm_rights
Arch_Structs_A.pde.PageTablePDE p attr mw \<Rightarrow> attr \<subseteq> {ParityEnabled}
| Arch_Structs_A.pde.SectionPDE p attr mw r \<Rightarrow> r \<in> valid_vm_rights
| Arch_Structs_A.pde.SuperSectionPDE p attr r \<Rightarrow> r \<in> valid_vm_rights
| _ \<Rightarrow> True"
definition
@ -614,10 +614,10 @@ where
"valid_objs s \<equiv> \<forall>ptr \<in> dom $ kheap s. \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s"
definition
pde_ref :: "ARM_Structs_A.pde \<Rightarrow> obj_ref option"
pde_ref :: "Arch_Structs_A.pde \<Rightarrow> obj_ref option"
where
"pde_ref pde \<equiv> case pde of
ARM_Structs_A.PageTablePDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
Arch_Structs_A.PageTablePDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
| _ \<Rightarrow> None"
datatype vs_ref = VSRef word32 "aa_type option"
@ -629,9 +629,9 @@ definition
definition
vs_refs :: "Structures_A.kernel_object \<Rightarrow> (vs_ref \<times> obj_ref) set" where
"vs_refs \<equiv> \<lambda>ko. case ko of
ArchObj (ARM_Structs_A.ASIDPool pool) \<Rightarrow>
ArchObj (Arch_Structs_A.ASIDPool pool) \<Rightarrow>
(\<lambda>(r,p). (VSRef (ucast r) (Some AASIDPool), p)) ` graph_of pool
| ArchObj (ARM_Structs_A.PageDirectory pd) \<Rightarrow>
| ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
(\<lambda>(r,p). (VSRef (ucast r) (Some APageDirectory), p)) `
graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
| _ \<Rightarrow> {}"
@ -684,31 +684,31 @@ where
"valid_arch_objs \<equiv> \<lambda>s. \<forall>p rs ao. (rs \<rhd> p) s \<longrightarrow> ko_at (ArchObj ao) p s \<longrightarrow> valid_arch_obj ao s"
definition
pde_ref_pages :: "ARM_Structs_A.pde \<Rightarrow> obj_ref option"
pde_ref_pages :: "Arch_Structs_A.pde \<Rightarrow> obj_ref option"
where
"pde_ref_pages pde \<equiv> case pde of
ARM_Structs_A.PageTablePDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
| ARM_Structs_A.SectionPDE ptr x y z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
| ARM_Structs_A.SuperSectionPDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
Arch_Structs_A.PageTablePDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
| Arch_Structs_A.SectionPDE ptr x y z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
| Arch_Structs_A.SuperSectionPDE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
| _ \<Rightarrow> None"
definition
pte_ref_pages :: "ARM_Structs_A.pte \<Rightarrow> obj_ref option"
pte_ref_pages :: "Arch_Structs_A.pte \<Rightarrow> obj_ref option"
where
"pte_ref_pages pte \<equiv> case pte of
ARM_Structs_A.SmallPagePTE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
| ARM_Structs_A.LargePagePTE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
Arch_Structs_A.SmallPagePTE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
| Arch_Structs_A.LargePagePTE ptr x z \<Rightarrow> Some (Platform.ptrFromPAddr ptr)
| _ \<Rightarrow> None"
definition
vs_refs_pages :: "Structures_A.kernel_object \<Rightarrow> (vs_ref \<times> obj_ref) set" where
"vs_refs_pages \<equiv> \<lambda>ko. case ko of
ArchObj (ARM_Structs_A.ASIDPool pool) \<Rightarrow>
ArchObj (Arch_Structs_A.ASIDPool pool) \<Rightarrow>
(\<lambda>(r,p). (VSRef (ucast r) (Some AASIDPool), p)) ` graph_of pool
| ArchObj (ARM_Structs_A.PageDirectory pd) \<Rightarrow>
| ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
(\<lambda>(r,p). (VSRef (ucast r) (Some APageDirectory), p)) `
graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x))
| ArchObj (ARM_Structs_A.PageTable pt) \<Rightarrow>
| ArchObj (Arch_Structs_A.PageTable pt) \<Rightarrow>
(\<lambda>(r,p). (VSRef (ucast r) (Some APageTable), p)) `
graph_of (pte_ref_pages o pt)
| _ \<Rightarrow> {}"
@ -758,20 +758,20 @@ where
"pte_mapping_bits \<equiv> pageBitsForSize ARMSmallPage"
definition
valid_pte_kernel_mappings :: "ARM_Structs_A.pte \<Rightarrow> vspace_ref
valid_pte_kernel_mappings :: "Arch_Structs_A.pte \<Rightarrow> vspace_ref
\<Rightarrow> arm_vspace_region_uses \<Rightarrow> bool"
where
"valid_pte_kernel_mappings pte vref uses \<equiv> case pte of
ARM_Structs_A.InvalidPTE \<Rightarrow>
Arch_Structs_A.InvalidPTE \<Rightarrow>
\<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}.
uses x \<noteq> ArmVSpaceKernelWindow
| ARM_Structs_A.SmallPagePTE ptr atts rghts \<Rightarrow>
| Arch_Structs_A.SmallPagePTE ptr atts rghts \<Rightarrow>
Platform.ptrFromPAddr ptr = vref
\<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pte_mapping_bits - 1}. uses x = use)
\<and> (use = ArmVSpaceKernelWindow
\<or> use = ArmVSpaceDeviceWindow))
\<and> rghts = {}
| ARM_Structs_A.LargePagePTE ptr atts rghts \<Rightarrow>
| Arch_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
@ -788,22 +788,22 @@ where
| _ \<Rightarrow> False"
definition
valid_pde_kernel_mappings :: "ARM_Structs_A.pde \<Rightarrow> vspace_ref \<Rightarrow> arm_vspace_region_uses \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
valid_pde_kernel_mappings :: "Arch_Structs_A.pde \<Rightarrow> vspace_ref \<Rightarrow> arm_vspace_region_uses \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"valid_pde_kernel_mappings pde vref uses \<equiv> case pde of
ARM_Structs_A.InvalidPDE \<Rightarrow>
Arch_Structs_A.InvalidPDE \<Rightarrow>
(\<lambda>s. \<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}.
uses x \<noteq> ArmVSpaceKernelWindow)
| ARM_Structs_A.PageTablePDE ptr _ _ \<Rightarrow>
| Arch_Structs_A.PageTablePDE ptr _ _ \<Rightarrow>
obj_at (valid_pt_kernel_mappings vref uses)
(Platform.ptrFromPAddr ptr)
| ARM_Structs_A.SectionPDE ptr atts _ rghts \<Rightarrow>
| Arch_Structs_A.SectionPDE ptr atts _ rghts \<Rightarrow>
(\<lambda>s. Platform.ptrFromPAddr ptr = vref
\<and> (\<exists>use. (\<forall>x \<in> {vref .. vref + 2 ^ pde_mapping_bits - 1}. uses x = use)
\<and> (use = ArmVSpaceKernelWindow
\<or> use = ArmVSpaceDeviceWindow))
\<and> rghts = {})
| ARM_Structs_A.SuperSectionPDE ptr atts rghts \<Rightarrow>
| Arch_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)
@ -834,24 +834,24 @@ where
definition
"valid_pde_mappings pde \<equiv> case pde of
ARM_Structs_A.SectionPDE ptr _ _ _ \<Rightarrow> is_aligned ptr pageBits
| ARM_Structs_A.SuperSectionPDE ptr _ _ \<Rightarrow> is_aligned ptr pageBits
Arch_Structs_A.SectionPDE ptr _ _ _ \<Rightarrow> is_aligned ptr pageBits
| Arch_Structs_A.SuperSectionPDE ptr _ _ \<Rightarrow> is_aligned ptr pageBits
| _ \<Rightarrow> True"
definition
"empty_table S ko \<equiv>
case ko of
ArchObj (ARM_Structs_A.PageDirectory pd) \<Rightarrow>
ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
\<forall>x. (\<forall>r. pde_ref (pd x) = Some r \<longrightarrow> r \<in> S) \<and>
valid_pde_mappings (pd x) \<and>
(x \<notin> kernel_mapping_slots \<longrightarrow> pd x = ARM_Structs_A.InvalidPDE)
| ArchObj (ARM_Structs_A.PageTable pt) \<Rightarrow>
pt = (\<lambda>x. ARM_Structs_A.InvalidPTE)
(x \<notin> kernel_mapping_slots \<longrightarrow> pd x = Arch_Structs_A.InvalidPDE)
| ArchObj (Arch_Structs_A.PageTable pt) \<Rightarrow>
pt = (\<lambda>x. Arch_Structs_A.InvalidPTE)
| _ \<Rightarrow> False"
definition
"valid_kernel_mappings_if_pd S ko \<equiv> case ko of
ArchObj (ARM_Structs_A.PageDirectory pd) \<Rightarrow>
ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
\<forall>x r. pde_ref (pd x) = Some r
\<longrightarrow> ((r \<in> S) = (x \<in> kernel_mapping_slots))
| _ \<Rightarrow> True"
@ -859,12 +859,12 @@ definition
definition
"aligned_pte pte \<equiv>
case pte of
ARM_Structs_A.LargePagePTE p _ _ \<Rightarrow> vmsz_aligned p ARMLargePage
| ARM_Structs_A.SmallPagePTE p _ _ \<Rightarrow> vmsz_aligned p ARMSmallPage
Arch_Structs_A.LargePagePTE p _ _ \<Rightarrow> vmsz_aligned p ARMLargePage
| Arch_Structs_A.SmallPagePTE p _ _ \<Rightarrow> vmsz_aligned p ARMSmallPage
| _ \<Rightarrow> True"
lemmas aligned_pte_simps[simp] =
aligned_pte_def[split_simps ARM_Structs_A.pte.split]
aligned_pte_def[split_simps Arch_Structs_A.pte.split]
definition
valid_global_objs :: "'z::state_ext state \<Rightarrow> bool"
@ -1286,30 +1286,30 @@ definition
vs_cap_ref :: "cap \<Rightarrow> vs_ref list option"
where
"vs_cap_ref cap \<equiv> case cap of
Structures_A.ArchObjectCap (ARM_Structs_A.ASIDPoolCap _ asid) \<Rightarrow>
Structures_A.ArchObjectCap (Arch_Structs_A.ASIDPoolCap _ asid) \<Rightarrow>
Some [VSRef (ucast (asid_high_bits_of asid)) None]
| Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow>
| Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow>
Some [VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None]
| Structures_A.ArchObjectCap (ARM_Structs_A.PageTableCap _ (Some (asid, vptr))) \<Rightarrow>
| Structures_A.ArchObjectCap (Arch_Structs_A.PageTableCap _ (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]
| Structures_A.ArchObjectCap (ARM_Structs_A.PageCap word rights ARMSmallPage (Some (asid, vptr))) \<Rightarrow>
| Structures_A.ArchObjectCap (Arch_Structs_A.PageCap word rights ARMSmallPage (Some (asid, vptr))) \<Rightarrow>
Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable),
VSRef (vptr >> 20) (Some APageDirectory),
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None]
| Structures_A.ArchObjectCap (ARM_Structs_A.PageCap word rights ARMLargePage (Some (asid, vptr))) \<Rightarrow>
| Structures_A.ArchObjectCap (Arch_Structs_A.PageCap word rights ARMLargePage (Some (asid, vptr))) \<Rightarrow>
Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable),
VSRef (vptr >> 20) (Some APageDirectory),
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None]
| Structures_A.ArchObjectCap (ARM_Structs_A.PageCap word rights ARMSection (Some (asid, vptr))) \<Rightarrow>
| Structures_A.ArchObjectCap (Arch_Structs_A.PageCap word rights 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]
| Structures_A.ArchObjectCap (ARM_Structs_A.PageCap word rights ARMSuperSection (Some (asid, vptr))) \<Rightarrow>
| Structures_A.ArchObjectCap (Arch_Structs_A.PageCap word rights ARMSuperSection (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]
@ -1328,9 +1328,9 @@ definition
definition
"cap_asid cap \<equiv> case cap of
Structures_A.ArchObjectCap (ARM_Structs_A.PageCap _ _ _ (Some (asid, _))) \<Rightarrow> Some asid
| Structures_A.ArchObjectCap (ARM_Structs_A.PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
| Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid
Structures_A.ArchObjectCap (Arch_Structs_A.PageCap _ _ _ (Some (asid, _))) \<Rightarrow> Some asid
| Structures_A.ArchObjectCap (Arch_Structs_A.PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
| Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid
| _ \<Rightarrow> None"
(* needed for retype: if reachable, then cap, if cap then protected by untyped cap.
@ -1363,14 +1363,14 @@ definition
table_cap_ref :: "cap \<Rightarrow> vs_ref list option"
where
"table_cap_ref cap \<equiv> case cap of
Structures_A.ArchObjectCap (ARM_Structs_A.ASIDPoolCap _ asid) \<Rightarrow>
Structures_A.ArchObjectCap (Arch_Structs_A.ASIDPoolCap _ asid) \<Rightarrow>
Some [VSRef (ucast (asid_high_bits_of asid)) None]
| Structures_A.ArchObjectCap
(ARM_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow>
(Arch_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow>
Some [VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None]
| Structures_A.ArchObjectCap
(ARM_Structs_A.PageTableCap _ (Some (asid, vptr))) \<Rightarrow>
(Arch_Structs_A.PageTableCap _ (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]
@ -1470,10 +1470,10 @@ definition
| AEndpoint \<Rightarrow> obj_bits (Endpoint undefined)
| ANTFN \<Rightarrow> obj_bits (Notification undefined)
| AArch T' \<Rightarrow> (case T' of
AASIDPool \<Rightarrow> obj_bits (ArchObj (ARM_Structs_A.ASIDPool undefined))
AASIDPool \<Rightarrow> obj_bits (ArchObj (Arch_Structs_A.ASIDPool undefined))
| AIntData sz \<Rightarrow> obj_bits (ArchObj (DataPage sz))
| APageDirectory \<Rightarrow> obj_bits (ArchObj (ARM_Structs_A.PageDirectory undefined))
| APageTable \<Rightarrow> obj_bits (ArchObj (ARM_Structs_A.PageTable undefined)))"
| APageDirectory \<Rightarrow> obj_bits (ArchObj (Arch_Structs_A.PageDirectory undefined))
| APageTable \<Rightarrow> obj_bits (ArchObj (Arch_Structs_A.PageTable undefined)))"
definition
"typ_range p T \<equiv> {p .. p + 2^obj_bits_type T - 1}"
@ -1824,11 +1824,11 @@ lemma st_tcb_idle_cap_valid_Null [simp]:
lemmas
wellformed_pte_simps[simp] =
wellformed_pte_def[split_simps ARM_Structs_A.pte.split]
wellformed_pte_def[split_simps Arch_Structs_A.pte.split]
lemmas
wellformed_pde_simps[simp] =
wellformed_pde_def[split_simps ARM_Structs_A.pde.split]
wellformed_pde_def[split_simps Arch_Structs_A.pde.split]
lemmas
wellformed_arch_obj_simps[simp] =
@ -1963,7 +1963,7 @@ lemma valid_arch_objs_stateI:
done
lemma asid_pool_at_ko:
"asid_pool_at p s \<Longrightarrow> \<exists>pool. ko_at (ArchObj (ARM_Structs_A.ASIDPool pool)) p s"
"asid_pool_at p s \<Longrightarrow> \<exists>pool. ko_at (ArchObj (Arch_Structs_A.ASIDPool pool)) p s"
apply (clarsimp simp: obj_at_def a_type_def)
apply (case_tac ko, simp_all split: split_if_asm)
apply (rename_tac arch_kernel_obj)
@ -3216,7 +3216,7 @@ lemma typ_at_eq_kheap_obj:
"typ_at AGarbage p s \<longleftrightarrow>
(\<exists>n cs. kheap s p = Some (CNode n cs) \<and> \<not> well_formed_cnode_n n cs)"
"typ_at (AArch AASIDPool) p s \<longleftrightarrow>
(\<exists>f. kheap s p = Some (ArchObj (ARM_Structs_A.ASIDPool f)))"
(\<exists>f. kheap s p = Some (ArchObj (Arch_Structs_A.ASIDPool f)))"
"typ_at (AArch APageTable) p s \<longleftrightarrow>
(\<exists>pt. kheap s p = Some (ArchObj (PageTable pt)))"
"typ_at (AArch APageDirectory) p s \<longleftrightarrow>
@ -3812,14 +3812,14 @@ lemma obj_at_default_cap_valid:
arch_default_cap_def default_arch_object_def
a_type_def valid_vm_rights_def
split: Structures_A.apiobject_type.splits
ARM_Structs_A.aobject_type.split_asm
Arch_Structs_A.aobject_type.split_asm
option.splits)
lemma obj_ref_default [simp]:
"obj_ref_of (default_cap ty x us) = x"
by (cases ty,
auto simp: arch_default_cap_def
split: ARM_Structs_A.aobject_type.split)
split: Arch_Structs_A.aobject_type.split)
lemma valid_pspace_aligned2 [elim!]:
"valid_pspace s \<Longrightarrow> pspace_aligned s"
@ -4018,7 +4018,7 @@ lemma vs_lookup1_ko_at_dest:
apply (clarsimp split: Structures_A.kernel_object.split_asm split_if_asm)
apply (clarsimp split: split_if_asm)
apply (simp add: pde_ref_def a_type_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
apply (erule_tac x=a in ballE)
apply (clarsimp simp add: obj_at_def)
apply simp
@ -4096,7 +4096,7 @@ lemma vs_lookup_pdI:
ap b = Some p\<^sub>2;
kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd));
c \<notin> kernel_mapping_slots;
pd c = ARM_Structs_A.pde.PageTablePDE p f w\<rbrakk>
pd c = Arch_Structs_A.pde.PageTablePDE p f w\<rbrakk>
\<Longrightarrow> ([VSRef (ucast c) (Some APageDirectory),
VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None]
\<rhd> Platform.ptrFromPAddr p) s"
@ -4130,7 +4130,7 @@ lemma vs_lookup_pages_vs_lookupI: "(ref \<rhd> p) s \<Longrightarrow> (ref \<unr
apply (clarsimp simp: split_def graph_of_def image_def split: split_if_asm)
apply (intro exI conjI impI, assumption)
apply (simp add: pde_ref_def pde_ref_pages_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
apply (rule refl)
done
@ -4157,7 +4157,7 @@ lemma vs_lookup_pages_ptI:
kheap s p\<^sub>1 = Some (ArchObj (arch_kernel_obj.ASIDPool ap));
ap b = Some p\<^sub>2;
kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd));
c \<notin> kernel_mapping_slots; pd c = ARM_Structs_A.PageTablePDE addr x y;
c \<notin> kernel_mapping_slots; pd c = Arch_Structs_A.PageTablePDE addr x y;
kheap s (Platform.ptrFromPAddr addr) = Some (ArchObj (PageTable pt));
pte_ref_pages (pt d) = Some p\<rbrakk>
\<Longrightarrow> ([VSRef (ucast d) (Some APageTable),
@ -4248,7 +4248,7 @@ lemma valid_arch_objs_alt:
ap b = Some p\<^sub>2 \<longrightarrow>
kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)) \<longrightarrow>
c \<notin> kernel_mapping_slots \<longrightarrow>
pd c = ARM_Structs_A.pde.PageTablePDE addr f w \<longrightarrow>
pd c = Arch_Structs_A.pde.PageTablePDE addr f w \<longrightarrow>
kheap s (Platform.ptrFromPAddr addr) =
Some (ArchObj (PageTable pt)) \<longrightarrow>
(\<forall>d. valid_pte (pt d) s))"
@ -4307,7 +4307,7 @@ lemma valid_arch_objs_alt:
apply (clarsimp simp: graph_of_def split: split_if_asm)
apply (drule_tac x=ab in spec)
apply (clarsimp simp: pde_ref_def obj_at_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
apply (clarsimp dest!: vs_lookup1D)
apply (clarsimp simp: vs_asid_refs_def graph_of_def)
apply (drule spec, drule spec, erule impE, assumption)
@ -4322,7 +4322,7 @@ lemma valid_arch_objs_alt:
apply (clarsimp simp: graph_of_def split: split_if_asm)
apply (drule_tac x=ab in spec)
apply (clarsimp simp: pde_ref_def obj_at_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
done
lemma vs_lookupE:
@ -4381,9 +4381,9 @@ proof -
apply (erule converse_rtranclE)
apply clarsimp
apply (erule (5) 2)
apply (simp add: valid_pde_def pde_ref_def split: ARM_Structs_A.pde.splits)
apply (simp add: valid_pde_def pde_ref_def split: Arch_Structs_A.pde.splits)
by (clarsimp simp: obj_at_def pde_ref_def vs_refs_def
split: ARM_Structs_A.pde.splits
split: Arch_Structs_A.pde.splits
dest!: vs_lookup1D)
qed
@ -4413,7 +4413,7 @@ lemma vs_lookup_pagesE_alt:
kheap s p\<^sub>1 = Some (ArchObj (arch_kernel_obj.ASIDPool ap));
ap b = Some p\<^sub>2;
kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd));
c \<notin> kernel_mapping_slots; pd c = ARM_Structs_A.PageTablePDE addr x y;
c \<notin> kernel_mapping_slots; pd c = Arch_Structs_A.PageTablePDE addr x y;
kheap s (Platform.ptrFromPAddr addr) = Some (ArchObj (PageTable pt));
pte_ref_pages (pt d) = Some p; valid_pte (pt d) s\<rbrakk>
\<Longrightarrow> R [VSRef (ucast d) (Some APageTable),
@ -4450,7 +4450,7 @@ proof -
apply (clarsimp simp: vs_refs_pages_def graph_of_def obj_at_def
pde_ref_pages_def
dest!: vs_lookup_pages1D
split: split_if_asm ARM_Structs_A.pde.splits)
split: split_if_asm Arch_Structs_A.pde.splits)
apply (frule_tac d=ac in vpt, assumption+)
apply (erule converse_rtranclE)
apply clarsimp
@ -4458,7 +4458,7 @@ proof -
apply (clarsimp simp: vs_refs_pages_def graph_of_def obj_at_def
pte_ref_pages_def
dest!: vs_lookup_pages1D
split: ARM_Structs_A.pte.splits)
split: Arch_Structs_A.pte.splits)
done
qed
@ -4475,7 +4475,7 @@ lemma pde_graph_ofI:
by (rule graph_ofI, simp)
lemma vs_refs_pdI:
"\<lbrakk>pd (ucast r) = ARM_Structs_A.PageTablePDE x a b;
"\<lbrakk>pd (ucast r) = Arch_Structs_A.PageTablePDE x a b;
ucast r \<notin> kernel_mapping_slots; \<forall>n \<ge> 12. n < 32 \<longrightarrow> \<not> r !! n\<rbrakk>
\<Longrightarrow> (VSRef r (Some APageDirectory), Platform.ptrFromPAddr x)
\<in> vs_refs (ArchObj (PageDirectory pd))"
@ -4490,7 +4490,7 @@ lemma vs_refs_pdI:
done
lemma a_type_pdD:
"a_type ko = AArch APageDirectory \<Longrightarrow> \<exists>pd. ko = ArchObj (ARM_Structs_A.PageDirectory pd)"
"a_type ko = AArch APageDirectory \<Longrightarrow> \<exists>pd. ko = ArchObj (Arch_Structs_A.PageDirectory pd)"
by (clarsimp simp: a_type_def
split: Structures_A.kernel_object.splits
arch_kernel_obj.splits split_if_asm)
@ -4584,7 +4584,7 @@ lemma vs_ref_order:
apply (frule prefix_length_le, clarsimp)
apply (drule valid_arch_objsD, simp add: obj_at_def, assumption)
apply (clarsimp simp: pde_ref_def
split: ARM_Structs_A.pde.split_asm split_if_asm)
split: Arch_Structs_A.pde.split_asm split_if_asm)
apply (drule_tac x=a in bspec, simp)
apply (case_tac rs, simp_all)[1]
apply (case_tac list, simp_all)[1]

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

@ -151,13 +151,14 @@ lemma update_cap_data_closedform:
| cap.IRQControlCap \<Rightarrow> cap.IRQControlCap
| cap.IRQHandlerCap irq \<Rightarrow> cap.IRQHandlerCap irq
| cap.Zombie r b n \<Rightarrow> cap.Zombie r b n
| cap.ArchObjectCap cap \<Rightarrow> cap.ArchObjectCap (arch_update_cap_data w cap))"
| cap.ArchObjectCap cap \<Rightarrow> cap.ArchObjectCap cap)"
apply (cases cap,
simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True
is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size
cap_ep_badge.simps badge_update_def o_def cap_rights_update_def
simp_thms cap_rights.simps Let_def split_def
the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def
arch_update_cap_data_def
cong: if_cong)
apply auto
done

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

@ -1715,7 +1715,7 @@ lemma valid_global_pd_mappings_pres:
apply (drule_tac x=x in spec)
apply (clarsimp simp: valid_pde_kernel_mappings_def obj_at_def
valid_pt_kernel_mappings_def pde_ref_def
split: ARM_Structs_A.pde.split_asm)
split: Arch_Structs_A.pde.split_asm)
apply (simp split: Structures_A.kernel_object.split_asm
arch_kernel_obj.split_asm)
apply (drule spec, drule spec, drule(1) mp)

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

@ -165,7 +165,7 @@ definition
PageTable pt \<Rightarrow> APageTable
| PageDirectory pd \<Rightarrow> APageDirectory
| DataPage sz \<Rightarrow> AIntData sz
| ARM_Structs_A.ASIDPool f \<Rightarrow> AASIDPool)"
| Arch_Structs_A.ASIDPool f \<Rightarrow> AASIDPool)"
lemmas a_base_type_simps [simp] =
a_base_type_def [split_simps kernel_object.split arch_kernel_obj.split]
@ -342,8 +342,8 @@ definition
ao_clean :: "arch_kernel_obj \<Rightarrow> component set \<Rightarrow> arch_kernel_obj" where
"ao_clean ao cmps \<equiv>
(case ao
of ARM_Structs_A.ASIDPool aobj \<Rightarrow>
ao_override (ARM_Structs_A.ASIDPool undefined) ao cmps
of Arch_Structs_A.ASIDPool aobj \<Rightarrow>
ao_override (Arch_Structs_A.ASIDPool undefined) ao cmps
| PageTable aobj \<Rightarrow> ao_override (PageTable undefined) ao cmps
| PageDirectory aobj \<Rightarrow> ao_override (PageDirectory undefined) ao cmps
| DataPage aobj \<Rightarrow> DataPage aobj)" (* type only *)

140
proof/invariant-abstract/PDPTEntries_AI.thy
View File

@ -13,36 +13,36 @@ imports Syscall_AI
begin
primrec
pde_range_sz :: "ARM_Structs_A.pde \<Rightarrow> nat"
pde_range_sz :: "Arch_Structs_A.pde \<Rightarrow> nat"
where
"pde_range_sz (ARM_Structs_A.InvalidPDE) = 0"
| "pde_range_sz (ARM_Structs_A.SectionPDE ptr x y z) = 0"
| "pde_range_sz (ARM_Structs_A.SuperSectionPDE ptr x z) = 4"
| "pde_range_sz (ARM_Structs_A.PageTablePDE ptr x z) = 0"
"pde_range_sz (Arch_Structs_A.InvalidPDE) = 0"
| "pde_range_sz (Arch_Structs_A.SectionPDE ptr x y z) = 0"
| "pde_range_sz (Arch_Structs_A.SuperSectionPDE ptr x z) = 4"
| "pde_range_sz (Arch_Structs_A.PageTablePDE ptr x z) = 0"
primrec
pte_range_sz :: "ARM_Structs_A.pte \<Rightarrow> nat"
pte_range_sz :: "Arch_Structs_A.pte \<Rightarrow> nat"
where
"pte_range_sz (ARM_Structs_A.InvalidPTE) = 0"
| "pte_range_sz (ARM_Structs_A.LargePagePTE ptr x y) = 4"
| "pte_range_sz (ARM_Structs_A.SmallPagePTE ptr x y) = 0"
"pte_range_sz (Arch_Structs_A.InvalidPTE) = 0"
| "pte_range_sz (Arch_Structs_A.LargePagePTE ptr x y) = 4"
| "pte_range_sz (Arch_Structs_A.SmallPagePTE ptr x y) = 0"
primrec
pde_range :: "ARM_Structs_A.pde \<Rightarrow> 12 word \<Rightarrow> 12 word set"
pde_range :: "Arch_Structs_A.pde \<Rightarrow> 12 word \<Rightarrow> 12 word set"
where
"pde_range (ARM_Structs_A.InvalidPDE) p = {}"
| "pde_range (ARM_Structs_A.SectionPDE ptr x y z) p = {p}"
| "pde_range (ARM_Structs_A.SuperSectionPDE ptr x z) p =
"pde_range (Arch_Structs_A.InvalidPDE) p = {}"
| "pde_range (Arch_Structs_A.SectionPDE ptr x y z) p = {p}"
| "pde_range (Arch_Structs_A.SuperSectionPDE ptr x z) p =
(if is_aligned p 4 then {x. x && ~~ mask 4 = p && ~~ mask 4} else {p})"
| "pde_range (ARM_Structs_A.PageTablePDE ptr x z) p = {p}"
| "pde_range (Arch_Structs_A.PageTablePDE ptr x z) p = {p}"
primrec
pte_range :: "ARM_Structs_A.pte \<Rightarrow> word8 \<Rightarrow> word8 set"
pte_range :: "Arch_Structs_A.pte \<Rightarrow> word8 \<Rightarrow> word8 set"
where
"pte_range (ARM_Structs_A.InvalidPTE) p = {}"
| "pte_range (ARM_Structs_A.LargePagePTE ptr x y) p =
"pte_range (Arch_Structs_A.InvalidPTE) p = {}"
| "pte_range (Arch_Structs_A.LargePagePTE ptr x y) p =
(if is_aligned p 4 then {x. x && ~~ mask 4 = p && ~~ mask 4} else {p})"
| "pte_range (ARM_Structs_A.SmallPagePTE ptr x y) p = {p}"
| "pte_range (Arch_Structs_A.SmallPagePTE ptr x y) p = {p}"
definition valid_entries :: " ('b \<Rightarrow> ('a::len) word \<Rightarrow> 'c set) \<Rightarrow> (('a::len) word \<Rightarrow> 'b) \<Rightarrow> bool"
where "valid_entries \<equiv> \<lambda>range fun. \<forall>x y. x \<noteq> y \<longrightarrow> range (fun x) x \<inter> range (fun y) y = {}"
@ -164,7 +164,7 @@ lemmas valid_entries_overwrite_group
lemma shift_0x3C_set:
"\<lbrakk> is_aligned p 6; 8 \<le> bits; bits < 32; len_of TYPE('a) = bits - 2 \<rbrakk> \<Longrightarrow>
(\<lambda>x. ucast (x + p && mask bits >> 2) :: ('a :: len) word) ` set [0 , 4 .e. 0x3C]
(\<lambda>x. ucast (x + p && mask bits >> 2) :: ('a :: len) word) ` set [0 :: word32 , 4 .e. 0x3C]
= {x. x && ~~ mask 4 = ucast (p && mask bits >> 2)}"
apply (clarsimp simp: upto_enum_step_def word32_shift_by_2 image_image)
apply (subst image_cong[where N="{x. x < 2 ^ 4}"])
@ -223,11 +223,11 @@ lemma mapM_x_store_pte_updates:
lemma valid_pt_entries_invalid[simp]:
"valid_pt_entries (\<lambda>x. ARM_Structs_A.pte.InvalidPTE)"
"valid_pt_entries (\<lambda>x. Arch_Structs_A.pte.InvalidPTE)"
by (simp add:valid_entries_def)
lemma valid_pd_entries_invalid[simp]:
"valid_pd_entries (\<lambda>x. ARM_Structs_A.pde.InvalidPDE)"
"valid_pd_entries (\<lambda>x. Arch_Structs_A.pde.InvalidPDE)"
by (simp add:valid_entries_def)
lemma entries_align_pte_update:
@ -257,7 +257,7 @@ lemma valid_pdpt_objs_ptD:
lemma mapM_x_store_invalid_pte_valid_pdpt:
"\<lbrace>valid_pdpt_objs and K (is_aligned p 6) \<rbrace>
mapM_x (\<lambda>x. store_pte (x + p) ARM_Structs_A.InvalidPTE) [0, 4 .e. 0x3C]
mapM_x (\<lambda>x. store_pte (x + p) Arch_Structs_A.InvalidPTE) [0, 4 .e. 0x3C]
\<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
apply (rule hoare_gen_asm)+
apply (rule hoare_pre, rule_tac p="p && ~~ mask pt_bits" in mapM_x_store_pte_updates)
@ -320,7 +320,7 @@ lemma mapM_x_store_pde_updates:
lemma mapM_x_store_pde_valid_pdpt_objs:
"\<lbrace>valid_pdpt_objs and K (is_aligned p 6)\<rbrace>
mapM_x (\<lambda>x. store_pde (x + p) ARM_Structs_A.InvalidPDE) [0, 4 .e. 0x3C]
mapM_x (\<lambda>x. store_pde (x + p) Arch_Structs_A.InvalidPDE) [0, 4 .e. 0x3C]
\<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
apply (rule hoare_gen_asm)+
apply (rule hoare_pre, rule_tac p="p && ~~ mask pd_bits" in mapM_x_store_pde_updates)
@ -361,7 +361,7 @@ lemma valid_entriesD:
lemma store_invalid_pde_valid_pdpt:
"\<lbrace>valid_pdpt_objs and
(\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s
\<longrightarrow> pde = ARM_Structs_A.InvalidPDE)\<rbrace>
\<longrightarrow> pde = Arch_Structs_A.InvalidPDE)\<rbrace>
store_pde p pde \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
apply (simp add: store_pde_def set_pd_def, wp get_object_wp)
apply (clarsimp simp: obj_at_def)
@ -403,7 +403,7 @@ lemma store_pde_non_master_valid_pdpt:
lemma store_invalid_pte_valid_pdpt:
"\<lbrace>valid_pdpt_objs and
(\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s
\<longrightarrow> pte = ARM_Structs_A.InvalidPTE)\<rbrace>
\<longrightarrow> pte = Arch_Structs_A.InvalidPTE)\<rbrace>
store_pte p pte \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
apply (simp add: store_pte_def set_pt_def, wp get_object_wp)
apply (clarsimp simp: obj_at_def)
@ -652,7 +652,7 @@ lemma shiftr_eq_neg_mask_eq:
lemma mapM_x_store_pte_valid_pdpt2:
"\<lbrace>valid_pdpt_objs and K (is_aligned ptr pt_bits)\<rbrace>
mapM_x (\<lambda>x. store_pte x ARM_Structs_A.pte.InvalidPTE) [ptr, ptr + 4 .e. ptr + 2 ^ pt_bits - 1]
mapM_x (\<lambda>x. store_pte x Arch_Structs_A.pte.InvalidPTE) [ptr, ptr + 4 .e. ptr + 2 ^ pt_bits - 1]
\<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
apply (rule hoare_gen_asm)+
apply (rule mapM_x_wp')
@ -673,7 +673,7 @@ lemma mapM_x_store_pte_valid_pdpt2:
lemma mapM_x_store_pde_valid_pdpt2:
"\<lbrace>valid_pdpt_objs and K (is_aligned pd pd_bits)\<rbrace>
mapM_x (\<lambda>x. store_pde ((x << 2) + pd) ARM_Structs_A.pde.InvalidPDE)
mapM_x (\<lambda>x. store_pde ((x << 2) + pd) Arch_Structs_A.pde.InvalidPDE)
[0.e.(kernel_base >> 20) - 1]
\<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
apply (rule hoare_gen_asm)
@ -694,12 +694,12 @@ lemma mapM_x_store_pde_valid_pdpt2:
done
lemma non_invalid_in_pde_range:
"pde \<noteq> ARM_Structs_A.pde.InvalidPDE
"pde \<noteq> Arch_Structs_A.pde.InvalidPDE
\<Longrightarrow> x \<in> pde_range pde x"
by (case_tac pde,simp_all)
lemma non_invalid_in_pte_range:
"pte \<noteq> ARM_Structs_A.pte.InvalidPTE
"pte \<noteq> Arch_Structs_A.pte.InvalidPTE
\<Longrightarrow> x \<in> pte_range pte x"
by (case_tac pte,simp_all)
@ -1155,13 +1155,13 @@ crunch valid_pdpt_objs[wp]: perform_asid_pool_invocation,
abbreviation (input)
"safe_pt_range \<equiv> \<lambda>slots s. obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt)
\<and> (\<forall>x\<in>set (tl slots). pt (ucast (x && mask pt_bits >> 2))
= ARM_Structs_A.pte.InvalidPTE))
= Arch_Structs_A.pte.InvalidPTE))
(hd slots && ~~ mask pt_bits) s"
abbreviation (input)
"safe_pd_range \<equiv> \<lambda>slots s. obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd)
\<and> (\<forall>x\<in>set (tl slots). pd (ucast (x && mask pd_bits >> 2))
= ARM_Structs_A.pde.InvalidPDE))
= Arch_Structs_A.pde.InvalidPDE))
(hd slots && ~~ mask pd_bits) s"
definition
@ -1180,8 +1180,8 @@ definition
(hd slots && ~~ mask pd_bits)
and K (pde_range_sz pde = 0)
else (\<lambda>s. (\<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0, 4 .e. 0x3C])))
and K (case entries of Inl (pte,slots) \<Rightarrow> pte \<noteq> ARM_Structs_A.InvalidPTE
| Inr (pde,slots) \<Rightarrow> pde \<noteq> ARM_Structs_A.InvalidPDE)"
and K (case entries of Inl (pte,slots) \<Rightarrow> pte \<noteq> Arch_Structs_A.InvalidPTE
| Inr (pde,slots) \<Rightarrow> pde \<noteq> Arch_Structs_A.InvalidPDE)"
definition
"page_inv_entries_safe entries \<equiv>
@ -1214,7 +1214,7 @@ definition
lemma pte_range_interD:
"pte_range pte p \<inter> pte_range pte' p' \<noteq> {}
\<Longrightarrow> pte \<noteq> ARM_Structs_A.InvalidPTE \<and> pte' \<noteq> ARM_Structs_A.InvalidPTE
\<Longrightarrow> pte \<noteq> Arch_Structs_A.InvalidPTE \<and> pte' \<noteq> Arch_Structs_A.InvalidPTE
\<and> p && ~~ mask 4 = p' && ~~ mask 4"
apply (drule WordLemmaBucket.int_not_emptyD)
apply (case_tac pte,simp_all split:if_splits)
@ -1226,7 +1226,7 @@ lemma pte_range_interD:
lemma pde_range_interD:
"pde_range pde p \<inter> pde_range pde' p' \<noteq> {}
\<Longrightarrow> pde \<noteq> ARM_Structs_A.InvalidPDE \<and> pde' \<noteq> ARM_Structs_A.InvalidPDE
\<Longrightarrow> pde \<noteq> Arch_Structs_A.InvalidPDE \<and> pde' \<noteq> Arch_Structs_A.InvalidPDE
\<and> p && ~~ mask 4 = p' && ~~ mask 4"
apply (drule WordLemmaBucket.int_not_emptyD)
apply (case_tac pde,simp_all split:if_splits)
@ -1307,7 +1307,7 @@ lemma store_pte_valid_pdpt:
apply (clarsimp simp:store_pte_def set_pt_def)
apply (wp get_pt_wp get_object_wp)
apply (clarsimp simp:obj_at_def
split:ARM_Structs_A.pte.splits arch_kernel_obj.splits)
split:Arch_Structs_A.pte.splits arch_kernel_obj.splits)
apply (rule conjI)
apply (drule(1) valid_pdpt_objs_ptD)
apply (rule valid_entries_overwrite_0)
@ -1324,7 +1324,7 @@ lemma store_pte_valid_pdpt:
apply (clarsimp simp:store_pte_def set_pt_def)
apply (wp get_pt_wp get_object_wp)
apply (clarsimp simp:obj_at_def
split:ARM_Structs_A.pte.splits arch_kernel_obj.splits)
split:Arch_Structs_A.pte.splits arch_kernel_obj.splits)
apply (drule(1) valid_pdpt_objs_ptD)
apply (rule conjI)
apply (rule valid_entries_overwrite_0)
@ -1392,7 +1392,7 @@ lemma store_pde_valid_pdpt:
apply (clarsimp simp:store_pde_def set_pd_def)
apply (wp get_pd_wp get_object_wp)
apply (clarsimp simp:obj_at_def
split:ARM_Structs_A.pde.splits arch_kernel_obj.splits)
split:Arch_Structs_A.pde.splits arch_kernel_obj.splits)
apply (drule(1) valid_pdpt_objs_pdD)
apply (rule conjI)
apply (rule valid_entries_overwrite_0)
@ -1409,7 +1409,7 @@ lemma store_pde_valid_pdpt:
apply (clarsimp simp:store_pde_def set_pd_def)
apply (wp get_pd_wp get_object_wp)
apply (clarsimp simp:obj_at_def
split:ARM_Structs_A.pde.splits arch_kernel_obj.splits)
split:Arch_Structs_A.pde.splits arch_kernel_obj.splits)
apply (drule(1) valid_pdpt_objs_pdD)
apply (rule conjI)
apply (rule valid_entries_overwrite_0)
@ -1498,16 +1498,16 @@ lemma perform_page_valid_pdpt[wp]:
apply (wp store_pte_valid_pdpt store_pde_valid_pdpt get_master_pte_wp get_master_pde_wp
store_pte_non_master_valid_pdpt store_pde_non_master_valid_pdpt
mapM_x_wp'[OF store_invalid_pte_valid_pdpt
[where pte=ARM_Structs_A.pte.InvalidPTE, simplified]]
[where pte=Arch_Structs_A.pte.InvalidPTE, simplified]]
mapM_x_wp'[OF store_invalid_pde_valid_pdpt
[where pde=ARM_Structs_A.pde.InvalidPDE, simplified]]
[where pde=Arch_Structs_A.pde.InvalidPDE, simplified]]
set_cap_page_inv_entries_safe
hoare_vcg_imp_lift[OF set_cap_arch_obj_neg] hoare_vcg_all_lift
| clarsimp simp: valid_page_inv_def cte_wp_at_weakenE[OF _ TrueI] obj_at_def
pte_range_sz_def pde_range_sz_def swp_def valid_page_inv_def
valid_slots_def page_inv_entries_safe_def pte_check_if_mapped_def
pde_check_if_mapped_def
split: ARM_Structs_A.pte.splits ARM_Structs_A.pde.splits
split: Arch_Structs_A.pte.splits Arch_Structs_A.pde.splits
| wp_once hoare_drop_imps)+
done
@ -1703,19 +1703,19 @@ lemma mask_out_same_pd:
done
lemma ensure_safe_mapping_ensures[wp]:
"\<lbrace>valid_pdpt_objs and (case entries of (Inl (ARM_Structs_A.SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
| (Inl (ARM_Structs_A.SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
| (Inl (ARM_Structs_A.LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (ARM_Structs_A.SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top>
| (Inr (ARM_Structs_A.SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (ARM_Structs_A.SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom>
"\<lbrace>valid_pdpt_objs and (case entries of (Inl (Arch_Structs_A.SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
| (Inl (Arch_Structs_A.SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
| (Inl (Arch_Structs_A.LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (Arch_Structs_A.SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top>
| (Inr (Arch_Structs_A.SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (Arch_Structs_A.SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom>
| _ \<Rightarrow> page_inv_entries_pre entries)\<rbrace>
ensure_safe_mapping entries
\<lbrace>\<lambda>rv. page_inv_entries_safe entries\<rbrace>,-"
proof -
have [simp]:
"\<And>s a. page_inv_entries_pre (Inl (ARM_Structs_A.pte.InvalidPTE, a)) s \<Longrightarrow>
page_inv_entries_safe (Inl (ARM_Structs_A.pte.InvalidPTE, a)) s"
"\<And>s a. page_inv_entries_pre (Inl (Arch_Structs_A.pte.InvalidPTE, a)) s \<Longrightarrow>
page_inv_entries_safe (Inl (Arch_Structs_A.pte.InvalidPTE, a)) s"
apply (clarsimp simp:page_inv_entries_pre_def page_inv_entries_safe_def
split:if_splits)
done
@ -1729,13 +1729,13 @@ lemma ensure_safe_mapping_ensures[wp]:
"\<And>a m n. a && ~~ mask m && mask n = a && mask n && ~~ mask m"
by (simp add:word_bw_comms word_bw_lcs)
have align_entry_ptD:
"\<And>pt m x xb xc. \<lbrakk>pt m = ARM_Structs_A.pte.LargePagePTE x xb xc; entries_align pte_range_sz pt\<rbrakk>
"\<And>pt m x xb xc. \<lbrakk>pt m = Arch_Structs_A.pte.LargePagePTE x xb xc; entries_align pte_range_sz pt\<rbrakk>
\<Longrightarrow> is_aligned m 4"
apply (simp add:entries_align_def)
apply (drule_tac x = m in spec,simp)
done
have align_entry_pdD:
"\<And>pd m x xb xc. \<lbrakk>pd m = ARM_Structs_A.pde.SuperSectionPDE x xb xc; entries_align pde_range_sz pd\<rbrakk>
"\<And>pd m x xb xc. \<lbrakk>pd m = Arch_Structs_A.pde.SuperSectionPDE x xb xc; entries_align pde_range_sz pd\<rbrakk>
\<Longrightarrow> is_aligned m 4"
apply (simp add:entries_align_def)
apply (drule_tac x = m in spec,simp)
@ -1751,7 +1751,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply word_bitwise
done
have mask_neq_0:
"\<And>z zs xa p g. \<lbrakk>[0 , 4 .e. 0x3C] = z # zs; xa \<in> set zs; is_aligned p 6; 6 \<le> g\<rbrakk>
"\<And>z zs xa p g. \<lbrakk>[0 :: word32, 4 .e. 0x3C] = z # zs; xa \<in> set zs; is_aligned p 6; 6 \<le> g\<rbrakk>
\<Longrightarrow> (p + xa && mask g >> 2) && mask 4 \<noteq> 0"
apply (rule ccontr)
apply (simp add:is_aligned_mask[symmetric])
@ -1817,16 +1817,16 @@ lemma ensure_safe_mapping_ensures[wp]:
done
have invalid_pteI:
"\<And>a pt x y z. \<lbrakk>valid_pt_entries pt; (a && ~~ mask 4) \<noteq> a;
pt (a && ~~ mask 4) = ARM_Structs_A.pte.LargePagePTE x y z \<rbrakk>
\<Longrightarrow> pt a = ARM_Structs_A.pte.InvalidPTE"
pt (a && ~~ mask 4) = Arch_Structs_A.pte.LargePagePTE x y z \<rbrakk>
\<Longrightarrow> pt a = Arch_Structs_A.pte.InvalidPTE"
apply (drule(1) valid_entriesD[rotated])
apply (case_tac "pt a"; simp add:mask_lower_twice is_aligned_neg_mask split:if_splits)
apply fastforce
done
have invalid_pdeI:
"\<And>a pd x y z. \<lbrakk>valid_pd_entries pd; (a && ~~ mask 4) \<noteq> a;
pd (a && ~~ mask 4) = ARM_Structs_A.pde.SuperSectionPDE x y z \<rbrakk>
\<Longrightarrow> pd a = ARM_Structs_A.pde.InvalidPDE"
pd (a && ~~ mask 4) = Arch_Structs_A.pde.SuperSectionPDE x y z \<rbrakk>
\<Longrightarrow> pd a = Arch_Structs_A.pde.InvalidPDE"
apply (drule(1) valid_entriesD[rotated])
apply (case_tac "pd a",
simp_all add:mask_lower_twice is_aligned_neg_mask
@ -1856,7 +1856,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply wp
apply (rule_tac Q' = "\<lambda>r s. \<forall>x \<in> set slots. obj_at
(\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and>
pt (ucast (x && mask pt_bits >> 2)) = ARM_Structs_A.pte.InvalidPTE)
pt (ucast (x && mask pt_bits >> 2)) = Arch_Structs_A.pte.InvalidPTE)
(hd (slot # slots) && ~~ mask pt_bits) s" in hoare_post_imp_R)
apply (wp mapME_x_accumulate_checks[where Q = "\<lambda>s. valid_pdpt_objs s"] )
apply (wp get_master_pte_wp| wpc | simp)+
@ -1871,7 +1871,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply (frule_tac x = z in mask_out_same_pt)
apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2)
apply (clarsimp simp:field_simps obj_at_def
split:ARM_Structs_A.pte.splits)
split:Arch_Structs_A.pte.splits)
apply (intro conjI impI)
apply (clarsimp)
apply (drule(1) valid_pdpt_objs_ptD)
@ -1896,7 +1896,7 @@ lemma ensure_safe_mapping_ensures[wp]:
| wp | intro conjI impI)+
apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton)
apply (wp get_master_pte_wp |wpc | simp)+
apply (clarsimp simp:obj_at_def split:ARM_Structs_A.pte.splits)
apply (clarsimp simp:obj_at_def split:Arch_Structs_A.pte.splits)
apply (clarsimp simp:page_inv_entries_safe_def split:list.splits)
apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton)
apply (case_tac b,case_tac a)
@ -1907,7 +1907,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton)
apply (wp get_master_pde_wp | wpc | simp)+
apply (clarsimp simp:obj_at_def page_inv_entries_safe_def
split:ARM_Structs_A.pde.splits)
split:Arch_Structs_A.pde.splits)
apply (simp split:list.splits if_splits
add:page_inv_entries_pre_def Let_def page_inv_entries_safe_def)
apply (elim conjE exE)
@ -1916,7 +1916,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply wp
apply (rule_tac Q' = "\<lambda>r s. \<forall>x \<in> set x22. obj_at
(\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and>
pd (ucast (x && mask pd_bits >> 2)) = ARM_Structs_A.pde.InvalidPDE)
pd (ucast (x && mask pd_bits >> 2)) = Arch_Structs_A.pde.InvalidPDE)
(hd (x21 # x22) && ~~ mask pd_bits) s" in hoare_post_imp_R)
apply (wp mapME_x_accumulate_checks[where Q = "\<lambda>s. valid_pdpt_objs s"] )
apply (wp get_master_pde_wp| wpc | simp)+
@ -1931,7 +1931,7 @@ lemma ensure_safe_mapping_ensures[wp]:
apply (frule_tac x = z in mask_out_same_pd)
apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2)
apply (clarsimp simp:field_simps obj_at_def
split:ARM_Structs_A.pde.splits)
split:Arch_Structs_A.pde.splits)
apply (drule(1) valid_pdpt_objs_pdD)
apply (intro conjI impI)
apply clarsimp
@ -1962,12 +1962,12 @@ lemma create_mapping_entries_safe[wp]:
and valid_arch_objs and pspace_aligned and
(\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits))\<rbrace>
create_mapping_entries ptr vptr sz rights attrib pd
\<lbrace>\<lambda>entries. case entries of (Inl (ARM_Structs_A.SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
| (Inl (ARM_Structs_A.SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
| (Inl (ARM_Structs_A.LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (ARM_Structs_A.SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top>
| (Inr (ARM_Structs_A.SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom>
| (Inr (ARM_Structs_A.SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
\<lbrace>\<lambda>entries. case entries of (Inl (Arch_Structs_A.SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
| (Inl (Arch_Structs_A.SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
| (Inl (Arch_Structs_A.LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
| (Inr (Arch_Structs_A.SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top>
| (Inr (Arch_Structs_A.SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom>
| (Inr (Arch_Structs_A.SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
| _ \<Rightarrow> page_inv_entries_pre entries\<rbrace>,-"
apply (cases sz, simp_all)
defer 2
@ -2008,7 +2008,7 @@ lemma create_mapping_entries_safe[wp]:
apply (clarsimp simp:not_less[symmetric])
apply (subgoal_tac
"(\<exists>xa xb. pda (ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2))
= ARM_Structs_A.pde.PageTablePDE x xa xb)
= Arch_Structs_A.pde.PageTablePDE x xa xb)
\<longrightarrow> is_aligned (Platform.ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6")
apply clarsimp
apply (subgoal_tac "

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

@ -360,7 +360,7 @@ lemma obj_bits_api_def3:
definition
"retype_addrs \<equiv> \<lambda>ptr' ty n us. map (\<lambda>p. ptr_add ptr' (p * 2 ^ obj_bits_api ty us))
"retype_addrs \<equiv> \<lambda>(ptr' :: obj_ref) ty n us. map (\<lambda>p. ptr_add ptr' (p * 2 ^ obj_bits_api ty us))
[0..< n]"
lemma retype_addrs_base [simp]:

11
proof/invariant-abstract/Tcb_AI.thy
View File

@ -428,10 +428,9 @@ lemma same_object_obj_refs:
"\<lbrakk> same_object_as cap cap' \<rbrakk>
\<Longrightarrow> obj_refs cap = obj_refs cap'"
apply (cases cap, simp_all add: same_object_as_def)
apply (clarsimp simp: is_cap_simps bits_of_def
split: cap.split_asm arch_cap.split_asm)+
apply (rename_tac arch_cap, case_tac arch_cap, simp_all)+
done
apply ((clarsimp simp: is_cap_simps bits_of_def
split: cap.split_asm )+)
by (cases "the_arch_cap cap"; cases "the_arch_cap cap'"; simp)
lemma same_object_zombies:
@ -486,8 +485,8 @@ lemma cap_master_pt_pd:
definition
"pt_pd_asid cap \<equiv> case cap of
Structures_A.ArchObjectCap (ARM_Structs_A.PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
| Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid
Structures_A.ArchObjectCap (Arch_Structs_A.PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
| Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid
| _ \<Rightarrow> None"

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

@ -1633,7 +1633,7 @@ lemmas of_nat_shift_distinct_helper32 = of_nat_shift_distinct_helper[where 'a=32
lemma ptr_add_distinct_helper:
"\<lbrakk> ptr_add p (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \<noteq> y;
"\<lbrakk> ptr_add (p :: word32) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \<noteq> y;
x < bnd; y < bnd; n < word_bits;
bnd \<le> 2 ^ (word_bits - n) \<rbrakk>
\<Longrightarrow> P"
@ -1853,7 +1853,7 @@ proof -
apply (simp add: init_arch_objects_def create_word_objects_def
pres reserve_region_def
split: Structures_A.apiobject_type.split
ARM_Structs_A.aobject_type.split)
Arch_Structs_A.aobject_type.split)
apply clarsimp
apply (rule hoare_pre)
apply (wp mapM_x_wp' copy_global_mappings_hoare_lift wp)

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

@ -20,9 +20,9 @@ begin
definition
glob_vs_refs :: "Structures_A.kernel_object \<Rightarrow> (vs_ref \<times> obj_ref) set"
where "glob_vs_refs \<equiv> \<lambda>ko. case ko of
ArchObj (ARM_Structs_A.ASIDPool pool) \<Rightarrow>
ArchObj (Arch_Structs_A.ASIDPool pool) \<Rightarrow>
(\<lambda>(r,p). (VSRef (ucast r) (Some AASIDPool), p)) ` graph_of pool
| ArchObj (ARM_Structs_A.PageDirectory pd) \<Rightarrow>
| ArchObj (Arch_Structs_A.PageDirectory pd) \<Rightarrow>
(\<lambda>(r,p). (VSRef (ucast r) (Some APageDirectory), p))
` graph_of (pde_ref o pd)
| _ \<Rightarrow> {}"
@ -1504,7 +1504,7 @@ definition
and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>cap. same_refs m cap s) slot s)
and (\<lambda>s. \<exists>pd. pd_at_asid asid pd s)
| ArchInvocation_A.PageUnmap cap ptr \<Rightarrow>
\<lambda>s. \<exists>r R sz m. cap = ARM_Structs_A.PageCap r R sz m \<and>
\<lambda>s. \<exists>r R sz m. cap = Arch_Structs_A.PageCap r R sz m \<and>
case_option True (valid_unmap sz) m \<and>
cte_wp_at (is_arch_diminished (cap.ArchObjectCap cap)) ptr s \<and>
s \<turnstile> (cap.ArchObjectCap cap)
@ -1552,7 +1552,7 @@ definition
where
"empty_pde_at p \<equiv> \<lambda>s.
\<exists>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s \<and>
pd (ucast (p && mask pd_bits >> 2)) = ARM_Structs_A.InvalidPDE"
pd (ucast (p && mask pd_bits >> 2)) = Arch_Structs_A.InvalidPDE"
definition
@ -2223,14 +2223,14 @@ lemma glob_vs_refs_subset:
lemma vs_refs_pages_pdI:
"\<lbrakk>pde_ref_pages (pd x) = Some a; x \<notin> kernel_mapping_slots\<rbrakk>
\<Longrightarrow> (VSRef (ucast x) (Some APageDirectory), a) \<in> vs_refs_pages (ArchObj (PageDirectory pd))"
by (auto simp: pde_ref_pages_def vs_refs_pages_def graph_of_def image_def split: ARM_Structs_A.pde.splits)
by (auto simp: pde_ref_pages_def vs_refs_pages_def graph_of_def image_def split: Arch_Structs_A.pde.splits)
lemma pde_ref_pde_ref_pagesI[elim!]:
"pde_ref (pd x) = Some a \<Longrightarrow> pde_ref_pages (pd x) = Some a"
by (auto simp: pde_ref_def pde_ref_pages_def split: ARM_Structs_A.pde.splits)
by (auto simp: pde_ref_def pde_ref_pages_def split: Arch_Structs_A.pde.splits)
lemma vs_refs_pdI2:
"\<lbrakk>pd r = ARM_Structs_A.pde.PageTablePDE x a b; r \<notin> kernel_mapping_slots\<rbrakk>
"\<lbrakk>pd r = Arch_Structs_A.pde.PageTablePDE x a b; r \<notin> kernel_mapping_slots\<rbrakk>
\<Longrightarrow> (VSRef (ucast r) (Some APageDirectory), Platform.ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pd))"
by (auto simp: vs_refs_def pde_ref_def graph_of_def)
@ -2292,7 +2292,7 @@ lemma set_pd_invs_map:
apply (erule_tac x=r in allE, drule (1) mp, drule (1) bspec)
apply clarsimp
apply (rule conjI)
apply (clarsimp simp: pde_ref_def split: ARM_Structs_A.pde.splits)
apply (clarsimp simp: pde_ref_def split: Arch_Structs_A.pde.splits)
apply (drule (1) vs_refs_pdI2)
apply (clarsimp simp: obj_at_def)
apply (erule disjE)
@ -2457,7 +2457,7 @@ lemma ref_is_unique:
apply (clarsimp simp: obj_at_def)
apply (erule (1) vs_lookupE_alt[OF _ _ valid_asid_table_ran], clarsimp)
apply ((clarsimp simp: obj_at_def)+)[2]
apply (simp add: pde_ref_def split: ARM_Structs_A.pde.splits)
apply (simp add: pde_ref_def split: Arch_Structs_A.pde.splits)
apply (drule (5) vs_lookup_pdI)+
apply (clarsimp dest!: valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI]
obj_ref_elemD)
@ -2537,7 +2537,7 @@ lemma vs_lookup_vs_lookup_pagesI':
apply simp
apply (clarsimp simp: pde_ref_def pde_ref_pages_def valid_pde_def obj_at_def
a_type_def
split:ARM_Structs_A.pde.splits )
split:Arch_Structs_A.pde.splits )
apply (rule vs_lookupI)
apply (fastforce simp: vs_asid_refs_def graph_of_def)
apply (rule_tac y="([VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None], p\<^sub>2)" in rtrancl_trans)
@ -2552,7 +2552,7 @@ lemma vs_lookup_vs_lookup_pagesI':
apply (clarsimp simp: pde_ref_def)
apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)])
apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def pte_ref_pages_def a_type_def
split: ARM_Structs_A.pte.splits)
split: Arch_Structs_A.pte.splits)
done
lemma vs_lookup_vs_lookup_pagesI:
@ -2575,7 +2575,7 @@ lemma store_pde_map_invs:
(\<forall>p'. pde_ref_pages pde = Some p' \<longrightarrow>
(\<exists>p'' cap. caps_of_state s p'' = Some cap \<and> p' \<in> obj_refs cap
\<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # r))
\<and> (\<forall>p''' a b. pde = ARM_Structs_A.PageTablePDE p''' a b \<longrightarrow>
\<and> (\<forall>p''' a b. pde = Arch_Structs_A.PageTablePDE p''' a b \<longrightarrow>
(\<forall>pt. ko_at (ArchObj (PageTable pt)) (Platform.ptrFromPAddr p''') s \<longrightarrow>
(\<forall>x word. pte_ref_pages (pt x) = Some word \<longrightarrow>
(\<exists>p'' cap. caps_of_state s p'' = Some cap \<and> word \<in> obj_refs cap
@ -2645,7 +2645,7 @@ lemma store_pde_map_invs:
apply clarsimp
apply (simp add: ucast_ucast_mask mask_shift_mask_helper)
apply (clarsimp simp: pde_ref_pages_def obj_at_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
apply (erule_tac x=d in allE, erule_tac x=q' in allE)
apply (frule (2) ref_is_unique[OF _ vs_lookup_vs_lookup_pagesI])
apply ((clarsimp simp: invs_def valid_state_def valid_arch_caps_def
@ -2747,7 +2747,7 @@ lemma mapM_swp_store_pte_invs[wp]:
(\<lambda>s. wellformed_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>
is_pt_cap c \<and> (pte = Arch_Structs_A.InvalidPTE \<or>
cap_asid c \<noteq> None)) slot s) and
(\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow>
(\<forall>q. pte_ref_pages pte = Some q \<longrightarrow>
@ -2782,7 +2782,7 @@ lemma mapM_swp_store_pde_invs_unmap:
(\<lambda>s. \<forall>sl\<in>set slots.
ucast (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and
(\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and
K (pde = ARM_Structs_A.pde.InvalidPDE)\<rbrace>
K (pde = Arch_Structs_A.pde.InvalidPDE)\<rbrace>
mapM (swp store_pde pde) slots \<lbrace>\<lambda>_. invs\<rbrace>"
apply (rule hoare_post_imp)
prefer 2
@ -2967,7 +2967,7 @@ lemma update_self_reachable:
apply (erule (2) vs_lookupE_alt[OF _ _ valid_asid_table_ran])
apply (rule vs_lookup_atI, clarsimp)
apply (rule_tac ap=ap in vs_lookup_apI, auto simp: obj_at_def)[1]
apply (clarsimp simp: pde_ref_def split: ARM_Structs_A.pde.splits)
apply (clarsimp simp: pde_ref_def split: Arch_Structs_A.pde.splits)
apply (rule_tac ap=ap and pd=pd in vs_lookup_pdI, auto simp: obj_at_def)[1]
done
@ -2980,10 +2980,10 @@ lemma update_self_reachable_pages:
apply (rule_tac ap=ap in vs_lookup_pages_apI, auto simp: obj_at_def)[1]
apply (rule_tac ap=ap and pd=pd in vs_lookup_pages_pdI,
auto simp: obj_at_def pde_ref_pages_def
split: ARM_Structs_A.pde.splits)[1]
split: Arch_Structs_A.pde.splits)[1]
apply (rule_tac ap=ap and pd=pd in vs_lookup_pages_ptI,
auto simp: obj_at_def pde_ref_pages_def pte_ref_pages_def
split: ARM_Structs_A.pde.splits ARM_Structs_A.pte.splits)[1]
split: Arch_Structs_A.pde.splits Arch_Structs_A.pte.splits)[1]
done
lemma pd_slots_helper:
@ -3030,7 +3030,7 @@ lemma pde_update_valid_arch_objs:
apply (erule allE[where x=s])
apply (clarsimp simp: split_def simpler_store_pde_def obj_at_def a_type_def
split: split_if_asm option.splits Structures_A.kernel_object.splits
ARM_Structs_A.arch_kernel_obj.splits)
Arch_Structs_A.arch_kernel_obj.splits)
done
lemma mapM_x_swp_store_pte_invs [wp]:
@ -3039,7 +3039,7 @@ lemma mapM_x_swp_store_pte_invs [wp]:
(\<lambda>s. wellformed_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>
is_pt_cap c \<and> (pte = Arch_Structs_A.InvalidPTE \<or>
cap_asid c \<noteq> None)) slot s) and
(\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow>
(\<forall>q. pte_ref_pages pte = Some q \<longrightarrow>
@ -3057,7 +3057,7 @@ lemma mapM_x_swp_store_pde_invs_unmap:
"\<lbrace>invs and K (\<forall>sl\<in>set slots.
ucast (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and
(\<lambda>s. \<forall>sl \<in> set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and
K (pde = ARM_Structs_A.pde.InvalidPDE)\<rbrace>
K (pde = Arch_Structs_A.pde.InvalidPDE)\<rbrace>
mapM_x (swp store_pde pde) slots \<lbrace>\<lambda>_. invs\<rbrace>"
by (simp add: mapM_x_mapM | wp mapM_swp_store_pde_invs_unmap)+
@ -3330,9 +3330,9 @@ lemmas unmap_page_table_final_cap[wp] = final_cap_lift [OF unmap_page_table_caps
lemma mapM_x_swp_store_empty_table':
"\<lbrace>obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt)
\<and> (\<forall>x. x \<in> (\<lambda>sl. ucast ((sl && mask pt_bits) >> 2)) ` set slots
\<or> pt x = ARM_Structs_A.InvalidPTE)) p
\<or> pt x = Arch_Structs_A.InvalidPTE)) p
and K (is_aligned p pt_bits \<and> (\<forall>x \<in> set slots. x && ~~ mask pt_bits = p))\<rbrace>
mapM_x (swp store_pte ARM_Structs_A.InvalidPTE) slots
mapM_x (swp store_pte Arch_Structs_A.InvalidPTE) slots
\<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>"
apply (rule hoare_gen_asm)
apply (induct slots, simp_all add: mapM_x_Nil mapM_x_Cons)
@ -3350,7 +3350,7 @@ lemma mapM_x_swp_store_empty_table:
"\<lbrace>page_table_at p and pspace_aligned
and K ((UNIV :: word8 set) \<subseteq> (\<lambda>sl. ucast ((sl && mask pt_bits) >> 2)) ` set slots
\<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p))\<rbrace>
mapM_x (swp store_pte ARM_Structs_A.InvalidPTE) slots
mapM_x (swp store_pte Arch_Structs_A.InvalidPTE) slots
\<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>"
apply (wp mapM_x_swp_store_empty_table')
apply (clarsimp simp: obj_at_def a_type_def)
@ -3460,7 +3460,7 @@ lemma store_pde_unmap_pt:
"\<lbrace>[VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pd
and K (is_aligned pd pd_bits)\<rbrace>
store_pde (pd + (vaddr >> 20 << 2)) ARM_Structs_A.pde.InvalidPDE
store_pde (pd + (vaddr >> 20 << 2)) Arch_Structs_A.pde.InvalidPDE
\<lbrace>\<lambda>rv s.
\<not> ([VSRef (vaddr >> 20) (Some APageDirectory),
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
@ -3501,7 +3501,7 @@ lemma store_pde_unmap_page:
"\<lbrace>[VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pd
and K (is_aligned pd pd_bits)\<rbrace>
store_pde (pd + (vaddr >> 20 << 2)) ARM_Structs_A.pde.InvalidPDE
store_pde (pd + (vaddr >> 20 << 2)) Arch_Structs_A.pde.InvalidPDE
\<lbrace>\<lambda>rv s.
\<not> ([VSRef (vaddr >> 20) (Some APageDirectory),
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
@ -3529,12 +3529,12 @@ crunch vs_lookup_pages[wp]: do_machine_op "\<lambda>s. P (vs_lookup_pages s)"
(* FIXME: move to Invariants_A *)
lemma pte_ref_pages_invalid_None[simp]:
"pte_ref_pages ARM_Structs_A.InvalidPTE = None"
"pte_ref_pages Arch_Structs_A.InvalidPTE = None"
by (simp add: pte_ref_pages_def)
lemma store_pte_no_lookup_pages:
"\<lbrace>\<lambda>s. \<not> (r \<unrhd> q) s\<rbrace>
store_pte p ARM_Structs_A.InvalidPTE
store_pte p Arch_Structs_A.InvalidPTE
\<lbrace>\<lambda>_ s. \<not> (r \<unrhd> q) s\<rbrace>"
apply (simp add: store_pte_def set_pt_def set_object_def)
apply (wp get_object_wp)
@ -3550,11 +3550,11 @@ lemma store_pte_no_lookup_pages:
(* FIXME: move to Invariants_A *)
lemma pde_ref_pages_invalid_None[simp]:
"pde_ref_pages ARM_Structs_A.InvalidPDE = None"
"pde_ref_pages Arch_Structs_A.InvalidPDE = None"
by (simp add: pde_ref_pages_def)
lemma store_pde_no_lookup_pages:
"\<lbrace>\<lambda>s. \<not> (r \<unrhd> q) s\<rbrace> store_pde p ARM_Structs_A.InvalidPDE \<lbrace>\<lambda>_ s. \<not> (r \<unrhd> q) s\<rbrace>"
"\<lbrace>\<lambda>s. \<not> (r \<unrhd> q) s\<rbrace> store_pde p Arch_Structs_A.InvalidPDE \<lbrace>\<lambda>_ s. \<not> (r \<unrhd> q) s\<rbrace>"
apply (simp add: store_pde_def set_pd_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def)
@ -3654,7 +3654,7 @@ lemma unmap_page_table_unmapped3:
split: split_if_asm)
apply (drule bspec, fastforce)
apply (clarsimp simp: obj_at_def valid_pde_def pde_ref_def pde_ref_pages_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
done
lemma is_final_cap_caps_of_state_2D:
@ -3753,7 +3753,7 @@ lemma perform_page_table_invocation_invs[wp]:
cap_master_cap_def cap_asid_def vs_cap_ref_simps
is_arch_cap_def pde_ref_def pde_ref_pages_def
split: cap.splits arch_cap.splits option.splits
ARM_Structs_A.pde.splits)
Arch_Structs_A.pde.splits)
apply (intro allI impI conjI, fastforce)
apply (clarsimp simp: caps_of_def cap_of_def)
apply (thin_tac "All P" for P)
@ -4190,7 +4190,7 @@ lemma dmo_ccr_invs[wp]:
(* FIXME: move to Invariants_A *)
lemmas pte_ref_pages_simps[simp] =
pte_ref_pages_def[split_simps ARM_Structs_A.pte.split]
pte_ref_pages_def[split_simps Arch_Structs_A.pte.split]
lemma ex_pt_cap_eq:
"(\<exists>ref cap. caps_of_state s ref = Some cap \<and>
@ -4258,7 +4258,7 @@ lemma store_pte_unmap_page:
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pt) s
\<and> is_aligned pt pt_bits \<and> p = (pt + ((vaddr >> 12) && mask 8 << 2 )))\<rbrace>
store_pte p ARM_Structs_A.pte.InvalidPTE
store_pte p Arch_Structs_A.pte.InvalidPTE
\<lbrace>\<lambda>rv s.\<not> ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable),
VSRef (vaddr >> 20) (Some APageDirectory),
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
@ -4274,7 +4274,7 @@ lemma store_pte_unmap_page:
apply (thin_tac "(VSRef a (Some AASIDPool), b) \<in> c" for a b c)
apply (clarsimp simp: graph_of_def
split: Structures_A.kernel_object.split_asm
ARM_Structs_A.arch_kernel_obj.splits
Arch_Structs_A.arch_kernel_obj.splits
split_if_asm)
apply (erule_tac P="a = c" for c in swap)
apply (rule up_ucast_inj[where 'a=8 and 'b=32])
@ -4291,13 +4291,13 @@ lemma store_pte_unmap_page:
shiftl_less_t2n'[where m=8 and n=2, simplified]
shiftr_less_t2n'[where m=8 and n=2, simplified]
word_bits_def shiftl_shiftr_id)+
apply (clarsimp split: Structures_A.kernel_object.split_asm ARM_Structs_A.arch_kernel_obj.split_asm )
apply (clarsimp split: Structures_A.kernel_object.split_asm Arch_Structs_A.arch_kernel_obj.split_asm )
apply (clarsimp simp: pde_ref_def pte_ref_pages_def pde_ref_pages_def
is_aligned_add_helper less_le_trans[OF ucast_less]
shiftl_less_t2n'[where m=8 and n=2, simplified]
dest!: graph_ofD ucast_up_inj[where 'a=10 and 'b=32, simplified]
ucast_up_inj[where 'a=8 and 'b=32, simplified]
split: split_if_asm ARM_Structs_A.pde.splits ARM_Structs_A.pte.splits)
split: split_if_asm Arch_Structs_A.pde.splits Arch_Structs_A.pte.splits)
done
crunch pd_at: flush_page "\<lambda>s. P (ko_at (ArchObj (PageDirectory pd)) x s)"
@ -4313,16 +4313,16 @@ lemma vs_lookup_pages_pteD:
VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pg) s
\<Longrightarrow> \<exists>ap fun pd funa pt funb. ([VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> ap) s
\<and> (arm_asid_table (arch_state s)) (asid_high_bits_of asid) = Some ap
\<and> ko_at (ArchObj (ARM_Structs_A.ASIDPool fun)) ap s
\<and> ko_at (ArchObj (Arch_Structs_A.ASIDPool fun)) ap s
\<and> ([VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pd) s
\<and> fun (ucast (asid && mask asid_low_bits)) = Some pd
\<and> ko_at (ArchObj (ARM_Structs_A.PageDirectory funa)) pd s
\<and> ko_at (ArchObj (Arch_Structs_A.PageDirectory funa)) pd s
\<and> ([VSRef (vaddr >> 20) (Some APageDirectory),
VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pt) s
\<and> pde_ref_pages (funa (ucast (vaddr >> 20))) = Some pt
\<and> ko_at (ArchObj (ARM_Structs_A.PageTable funb)) pt s
\<and> ko_at (ArchObj (Arch_Structs_A.PageTable funb)) pt s
\<and> pte_ref_pages (funb (ucast ((vaddr >> 12) && mask 8 ))) = Some pg"
apply (frule vs_lookup_pages_2ConsD)
@ -4342,7 +4342,7 @@ lemma vs_lookup_pages_pteD:
mask_asid_low_bits_ucast_ucast pde_ref_pages_def pte_ref_pages_def
split: split_if_asm)
apply (simp add: ucast_ucast_id
split: ARM_Structs_A.pde.split_asm ARM_Structs_A.pte.split_asm)
split: Arch_Structs_A.pde.split_asm Arch_Structs_A.pte.split_asm)
done
lemma vs_lookup_pages_pdeD:
@ -4351,11 +4351,11 @@ lemma vs_lookup_pages_pdeD:
VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> p) s
\<Longrightarrow> \<exists>ap fun pd funa. ([VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> ap) s
\<and> (arm_asid_table (arch_state s)) (asid_high_bits_of asid) = Some ap
\<and> ko_at (ArchObj (ARM_Structs_A.ASIDPool fun)) ap s
\<and> ko_at (ArchObj (Arch_Structs_A.ASIDPool fun)) ap s
\<and> ([VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pd) s
\<and> fun (ucast (asid && mask asid_low_bits)) = Some pd
\<and> ko_at (ArchObj (ARM_Structs_A.PageDirectory funa)) pd s
\<and> ko_at (ArchObj (Arch_Structs_A.PageDirectory funa)) pd s
\<and> pde_ref_pages (funa (ucast (vaddr >> 20))) = Some p"
apply (frule vs_lookup_pages_2ConsD)
@ -4373,14 +4373,14 @@ lemma vs_lookup_pages_pdeD:
mask_asid_low_bits_ucast_ucast pde_ref_pages_def
split: split_if_asm)
apply (simp add: ucast_ucast_id
split: ARM_Structs_A.pde.split_asm)
split: Arch_Structs_A.pde.split_asm)
done
lemma vs_lookup_ap_mappingD:
"([VSRef (asid && mask asid_low_bits) (Some AASIDPool),
VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pd) s
\<Longrightarrow> \<exists>ap fun. (arm_asid_table (arch_state s)) (asid_high_bits_of asid) = Some ap
\<and> ko_at (ArchObj (ARM_Structs_A.ASIDPool fun)) ap s
\<and> ko_at (ArchObj (Arch_Structs_A.ASIDPool fun)) ap s
\<and> fun (ucast (asid && mask asid_low_bits)) = Some pd"
apply (clarsimp simp: vs_lookup_def vs_asid_refs_def
dest!: graph_ofD vs_lookup1_rtrancl_iterations)
@ -4533,7 +4533,7 @@ lemma unmap_page_unmapped:
apply clarsimp+
(* This should be somewhere else but isn't *)
apply (subgoal_tac "\<exists>xs. [0, 4 .e. 0x3C] = 0 # xs")
apply (subgoal_tac "\<exists>xs. [0 :: word32, 4 .e. 0x3C] = 0 # xs")
prefer 2
apply (simp add: upto_enum_step_def upto_enum_word upt_rec)
apply (clarsimp simp: unmap_page_def lookup_pd_slot_def lookup_pt_slot_def Let_def
@ -4574,11 +4574,11 @@ lemma unmap_page_unmapped:
apply assumption
apply (simp, drule bspec, fastforce)
apply (clarsimp simp: pde_ref_pages_def
split: ARM_Structs_A.pde.splits
split: Arch_Structs_A.pde.splits
dest!: )
apply (frule pt_aligned[rotated])
apply (simp add: obj_at_def a_type_def)
apply (simp split: Structures_A.kernel_object.splits ARM_Structs_A.arch_kernel_obj.splits, blast)
apply (simp split: Structures_A.kernel_object.splits Arch_Structs_A.arch_kernel_obj.splits, blast)
apply (clarsimp simp: obj_at_def)
apply (simp add: vaddr_segment_nonsense3[where vaddr=vaddr]
vaddr_segment_nonsense4[where vaddr=vaddr])
@ -4594,7 +4594,7 @@ lemma unmap_page_unmapped:
shiftl_shiftr_id[where n=2,
OF _ less_le_trans[OF and_mask_less'[where n=8]],
unfolded mask_def word_bits_def, simplified]
split: ARM_Structs_A.pte.splits)
split: Arch_Structs_A.pte.splits)
apply ((clarsimp simp: obj_at_def a_type_def)+)[2]
apply (drule vs_lookup_pages_pteD)
@ -4610,11 +4610,11 @@ lemma unmap_page_unmapped:
apply assumption
apply (simp, drule bspec, fastforce)
apply (clarsimp simp: pde_ref_pages_def
split: ARM_Structs_A.pde.splits
split: Arch_Structs_A.pde.splits
dest!: )
apply (frule pt_aligned[rotated])
apply (simp add: obj_at_def a_type_def)
apply (simp split: Structures_A.kernel_object.splits ARM_Structs_A.arch_kernel_obj.splits, blast)
apply (simp split: Structures_A.kernel_object.splits Arch_Structs_A.arch_kernel_obj.splits, blast)
apply (clarsimp simp: obj_at_def)
apply (simp add: vaddr_segment_nonsense3[where vaddr=vaddr]
vaddr_segment_nonsense4[where vaddr=vaddr])
@ -4630,7 +4630,7 @@ lemma unmap_page_unmapped:
shiftl_shiftr_id[where n=2,
OF _ less_le_trans[OF and_mask_less'[where n=8]],
unfolded mask_def word_bits_def, simplified]
split: ARM_Structs_A.pte.splits)
split: Arch_Structs_A.pte.splits)
apply ((clarsimp simp: obj_at_def a_type_def)+)[2]
apply (drule vs_lookup_pages_pdeD)
@ -4646,7 +4646,7 @@ lemma unmap_page_unmapped:
apply assumption
apply (simp, drule bspec, fastforce)
apply (clarsimp simp: pde_ref_pages_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
apply (clarsimp simp: obj_at_def)
apply (drule_tac p="rv" in vs_lookup_vs_lookup_pagesI')
apply ((simp add: obj_at_def a_type_def)+)[3]
@ -4655,7 +4655,7 @@ lemma unmap_page_unmapped:
apply (simp add: valid_arch_obj_def)
apply (drule bspec[where x="ucast (vaddr >> 20)"], simp)
apply (clarsimp simp: obj_at_def a_type_def pd_bits_def pageBits_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
apply (clarsimp simp: obj_at_def a_type_def)
apply (drule vs_lookup_pages_pdeD)
@ -4671,7 +4671,7 @@ lemma unmap_page_unmapped:
apply assumption
apply (simp, drule bspec, fastforce)
apply (clarsimp simp: pde_ref_pages_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
apply (clarsimp simp: obj_at_def)
apply (drule_tac p="rv" in vs_lookup_vs_lookup_pagesI')
apply ((simp add: obj_at_def a_type_def)+)[3]
@ -4680,7 +4680,7 @@ lemma unmap_page_unmapped:
apply (simp add: valid_arch_obj_def)
apply (drule bspec[where x="ucast (vaddr >> 20)"], simp)
apply (clarsimp simp: obj_at_def a_type_def pd_bits_def pageBits_def
split: ARM_Structs_A.pde.splits)
split: Arch_Structs_A.pde.splits)
apply (clarsimp simp: obj_at_def a_type_def pd_bits_def pageBits_def)
done
@ -4893,7 +4893,7 @@ lemma perform_page_invs [wp]:
apply (rule conjI)
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
apply (clarsimp split: Structures_A.kernel_object.split_asm
split_if_asm ARM_Structs_A.arch_kernel_obj.splits)
split_if_asm Arch_Structs_A.arch_kernel_obj.splits)
apply (erule ballEI)
apply (clarsimp simp: pde_at_def obj_at_def
caps_of_state_cteD'[where P=\<top>, simplified])
@ -4940,7 +4940,7 @@ lemma perform_page_invs [wp]:
is_pg_cap_def
split: cap.splits Structures_A.kernel_object.splits
split_if_asm
ARM_Structs_A.arch_kernel_obj.splits option.splits
Arch_Structs_A.arch_kernel_obj.splits option.splits
arch_cap.splits)+)[2]
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
apply (rule conjI)
@ -5003,9 +5003,9 @@ lemma perform_page_invs [wp]:
locale asid_pool_map =
fixes s ap pool asid pdp pd s'
defines "(s' :: ('a::state_ext) state) \<equiv>
s\<lparr>kheap := kheap s(ap \<mapsto> ArchObj (ARM_Structs_A.ASIDPool
s\<lparr>kheap := kheap s(ap \<mapsto> ArchObj (Arch_Structs_A.ASIDPool
(pool(asid \<mapsto> pdp))))\<rparr>"
assumes ap: "kheap s ap = Some (ArchObj (ARM_Structs_A.ASIDPool pool))"
assumes ap: "kheap s ap = Some (ArchObj (Arch_Structs_A.ASIDPool pool))"
assumes new: "pool asid = None"
assumes pd: "kheap s pdp = Some (ArchObj (PageDirectory pd))"
assumes pde: "empty_table (set (arm_global_pts (arch_state s)))
@ -5120,7 +5120,7 @@ lemma not_kernel_slot_not_global_pt:
lemma set_asid_pool_arch_objs_map:
"\<lbrace>valid_arch_objs and valid_arch_state and valid_global_objs and
valid_kernel_mappings and
ko_at (ArchObj (ARM_Structs_A.ASIDPool pool)) ap and
ko_at (ArchObj (Arch_Structs_A.ASIDPool pool)) ap and
K (pool asid = None) and
\<exists>\<rhd> ap and page_directory_at pd and
(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) pd s) \<rbrace>
@ -5179,7 +5179,7 @@ lemma obj_at_not_pt_not_in_global_pts:
lemma set_asid_pool_valid_arch_caps_map:
"\<lbrace>valid_arch_caps and valid_arch_state and valid_global_objs and valid_objs
and valid_arch_objs and ko_at (ArchObj (ARM_Structs_A.ASIDPool pool)) ap
and valid_arch_objs and ko_at (ArchObj (Arch_Structs_A.ASIDPool pool)) ap
and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap
\<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some ((VSRef (ucast asid) (Some AASIDPool)) # rf))
\<and> (VSRef (ucast asid) (Some AASIDPool) # rf \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]))
@ -5225,7 +5225,7 @@ lemma set_asid_pool_valid_arch_caps_map:
done
lemma set_asid_pool_asid_map:
"\<lbrace>valid_asid_map and ko_at (ArchObj (ARM_Structs_A.ASIDPool pool)) ap
"\<lbrace>valid_asid_map and ko_at (ArchObj (Arch_Structs_A.ASIDPool pool)) ap
and K (pool asid = None)\<rbrace>
set_asid_pool ap (pool(asid \<mapsto> pd))
\<lbrace>\<lambda>rv. valid_asid_map\<rbrace>"
@ -5264,7 +5264,7 @@ lemma set_asid_pool_asid_map:
done
lemma set_asid_pool_invs_map:
"\<lbrace>invs and ko_at (ArchObj (ARM_Structs_A.ASIDPool pool)) ap
"\<lbrace>invs and ko_at (ArchObj (Arch_Structs_A.ASIDPool pool)) ap
and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap
\<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some ((VSRef (ucast asid) (Some AASIDPool)) # rf))
\<and> (VSRef (ucast asid) (Some AASIDPool) # rf \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]))

38
proof/refine/ADT_H.thy
View File

@ -67,43 +67,43 @@ lemma vm_rights_of_vmrights_map_id[simp]:
definition
absPageTable :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> obj_ref \<Rightarrow>
word8 \<Rightarrow> ARM_Structs_A.pte"
word8 \<Rightarrow> Arch_Structs_A.pte"
where
"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.InvalidPTE))) \<Rightarrow> Arch_Structs_A.InvalidPTE
| Some (KOArch (KOPTE (Hardware_H.LargePagePTE p c g xn rights))) \<Rightarrow>
if is_aligned offs 4 then
ARM_Structs_A.LargePagePTE p
Arch_Structs_A.LargePagePTE p
{x. c & x=PageCacheable | g & x=Global | xn & x=XNever}
(vm_rights_of rights)
else ARM_Structs_A.InvalidPTE
else Arch_Structs_A.InvalidPTE
| Some (KOArch (KOPTE (Hardware_H.SmallPagePTE p c g xn rights))) \<Rightarrow>
ARM_Structs_A.SmallPagePTE p {x. c & x=PageCacheable |
Arch_Structs_A.SmallPagePTE p {x. c & x=PageCacheable |
g & x=Global |
xn & x=XNever} (vm_rights_of rights)"
definition
absPageDirectory :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> obj_ref \<Rightarrow>
12 word \<Rightarrow> ARM_Structs_A.pde"
12 word \<Rightarrow> Arch_Structs_A.pde"
where
"absPageDirectory h a \<equiv> %offs.
case (h (a + (ucast offs << 2))) of
Some (KOArch (KOPDE (Hardware_H.InvalidPDE))) \<Rightarrow> ARM_Structs_A.InvalidPDE
Some (KOArch (KOPDE (Hardware_H.InvalidPDE))) \<Rightarrow> Arch_Structs_A.InvalidPDE
| Some (KOArch (KOPDE (Hardware_H.PageTablePDE p e mw))) \<Rightarrow>
ARM_Structs_A.PageTablePDE p {x. e & x=ParityEnabled} mw
Arch_Structs_A.PageTablePDE p {x. e & x=ParityEnabled} mw
| Some (KOArch (KOPDE (Hardware_H.SectionPDE p e mw c g xn rights))) \<Rightarrow>
ARM_Structs_A.SectionPDE p {x. e & x=ParityEnabled |
Arch_Structs_A.SectionPDE p {x. e & x=ParityEnabled |
c & x=PageCacheable |
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
Arch_Structs_A.SuperSectionPDE p
{x. e & x=ParityEnabled | c & x=PageCacheable
| g & x=Global | xn & x=XNever}
(vm_rights_of rights)
else ARM_Structs_A.InvalidPDE"
else Arch_Structs_A.InvalidPDE"
(* Can't pull the whole heap off at once, start with arch specific stuff.*)
definition
@ -112,8 +112,8 @@ definition
where
"absHeapArch h a \<equiv> %ako.
(case ako of
KOASIDPool (ARMStructures_H.ASIDPool ap) \<Rightarrow>
Some (ARM_Structs_A.ASIDPool (\<lambda>w. ap (ucast w)))
KOASIDPool (ArchStructures_H.ASIDPool ap) \<Rightarrow>
Some (Arch_Structs_A.ASIDPool (\<lambda>w. ap (ucast w)))
| KOPTE _ \<Rightarrow>
if is_aligned a pt_bits then Some (PageTable (absPageTable h a))
else None
@ -823,10 +823,10 @@ proof -
apply (erule_tac x=offs in allE)
apply (rename_tac pte')
apply (case_tac pte', simp_all add: pte_relation_aligned_def)[1]
apply (clarsimp split: ARM_Structs_A.pte.splits)
apply (clarsimp split: Arch_Structs_A.pte.splits)
apply (rule set_eqI, clarsimp)
apply (case_tac x, simp_all)[1]
apply (clarsimp split: ARM_Structs_A.pte.splits)
apply (clarsimp split: Arch_Structs_A.pte.splits)
apply (rule set_eqI, clarsimp)
apply (case_tac x, simp_all)[1]
apply (clarsimp simp add: pde_relation_def)
@ -869,12 +869,12 @@ proof -
apply (erule_tac x=offs in allE)
apply (rename_tac pde')
apply (case_tac pde', simp_all add: pde_relation_aligned_def)[1]
apply (clarsimp split: ARM_Structs_A.pde.splits)+
apply (clarsimp split: Arch_Structs_A.pde.splits)+
apply (fastforce simp add: subset_eq)
apply (clarsimp split: ARM_Structs_A.pde.splits)
apply (clarsimp split: Arch_Structs_A.pde.splits)
apply (rule set_eqI, clarsimp)
apply (case_tac x, simp_all)[1]
apply (clarsimp split: ARM_Structs_A.pde.splits)
apply (clarsimp split: Arch_Structs_A.pde.splits)
apply (rule set_eqI, clarsimp)
apply (case_tac x, simp_all)[1]
apply (clarsimp simp add: pde_relation_def)
@ -927,7 +927,7 @@ shows
apply (erule(1) obj_relation_cutsE, simp_all)
apply (clarsimp simp: other_obj_relation_def
split: Structures_A.kernel_object.split_asm
ARM_Structs_A.arch_kernel_obj.split_asm)
Arch_Structs_A.arch_kernel_obj.split_asm)
done
text {* The following function can be used to reverse cte_map. *}

12
proof/refine/ArchAcc_R.thy
View File

@ -331,7 +331,7 @@ lemma get_master_pde_corres:
projectKOs and_not_mask_twice)
apply (simp add: bind_assoc exec_gets)
apply (clarsimp simp: pde_at_def obj_at_def)
apply (clarsimp split:ARM_Structs_A.pde.splits)
apply (clarsimp split:Arch_Structs_A.pde.splits)
apply (intro conjI impI)
-- "master_pde = InvaliatePTE"
apply (clarsimp simp add: a_type_def return_def get_pd_def
@ -603,7 +603,7 @@ lemma get_master_pte_corres:
projectKOs and_not_mask_twice)
apply (simp add: bind_assoc exec_gets)
apply (clarsimp simp: pte_at_def obj_at_def)
apply (clarsimp split:ARM_Structs_A.pte.splits)
apply (clarsimp split:Arch_Structs_A.pte.splits)
apply (intro conjI impI)
-- "master_pde = InvaliatePTE"
apply (clarsimp simp add: a_type_def return_def get_pt_def
@ -1190,10 +1190,10 @@ lemma arch_cap_rights_update:
cap_relation (cap.ArchObjectCap (acap_rights_update (acap_rights c \<inter> msk) c))
(ArchRetypeDecls_H.maskCapRights (rights_mask_map msk) c')"
apply (cases c, simp_all add: ArchRetype_H.maskCapRights_def
acap_rights_update_def Let_def)
acap_rights_update_def Let_def isCap_simps)
apply (simp add: maskVMRights_def vmrights_map_def rights_mask_map_def
validate_vm_rights_def vm_read_write_def vm_read_only_def
vm_kernel_only_def)
vm_kernel_only_def )
done
lemma arch_deriveCap_inv:
@ -1237,7 +1237,7 @@ definition
"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>
mapping_map :: "Arch_Structs_A.pte \<times> word32 list + Arch_Structs_A.pde \<times> word32 list \<Rightarrow>
Hardware_H.pte \<times> word32 list + Hardware_H.pde \<times> word32 list \<Rightarrow> bool"
where
"mapping_map \<equiv> pte_relation' \<otimes> (op =) \<oplus> pde_relation' \<otimes> (op =)"
@ -1281,7 +1281,7 @@ lemma create_mapping_entries_corres:
done
lemma pte_relation'_Invalid_inv [simp]:
"pte_relation' x Hardware_H.pte.InvalidPTE = (x = ARM_Structs_A.pte.InvalidPTE)"
"pte_relation' x Hardware_H.pte.InvalidPTE = (x = Arch_Structs_A.pte.InvalidPTE)"
by (cases x) auto
definition

84
proof/refine/Arch_R.thy
View File

@ -524,13 +524,13 @@ lemma page_base_corres[simp]:
by (clarsimp simp: pageBase_def page_base_def complement_def)
lemma flush_type_map:
"InvocationLabels_H.isPageFlush (invocation_type (mi_label mi))
\<or> InvocationLabels_H.isPDFlush (invocation_type (mi_label mi))
"ArchLabelFuns_H.isPageFlushLabel (invocation_type (mi_label mi))
\<or> ArchLabelFuns_H.isPDFlushLabel (invocation_type (mi_label mi))
\<Longrightarrow> labelToFlushType (mi_label mi) =
flush_type_map (label_to_flush_type (invocation_type (mi_label mi)))"
by (clarsimp simp: label_to_flush_type_def labelToFlushType_def flush_type_map_def
InvocationLabels_H.isPageFlush_def InvocationLabels_H.isPDFlush_def
split: ArchInvocation_A.flush_type.splits invocation_label.splits)
ArchLabelFuns_H.isPageFlushLabel_def ArchLabelFuns_H.isPDFlushLabel_def
split: ArchInvocation_A.flush_type.splits invocation_label.splits arch_invocation_label.splits)
lemma resolve_vaddr_corres:
"\<lbrakk> is_aligned pd pd_bits; vaddr < kernel_base \<rbrakk> \<Longrightarrow>
@ -561,7 +561,7 @@ lemma resolve_vaddr_corres:
done
lemma dec_arch_inv_page_flush_corres:
"InvocationLabels_H.isPageFlush (invocation_type (mi_label mi)) \<Longrightarrow>
"ArchLabelFuns_H.isPageFlushLabel (invocation_type (mi_label mi)) \<Longrightarrow>
corres (ser \<oplus> archinv_relation)
(invs and
valid_cap (cap.ArchObjectCap (arch_cap.PageCap word seta vmpage_size option)) and
@ -619,8 +619,8 @@ lemma dec_arch_inv_page_flush_corres:
apply (rule corres_returnOk)
apply (clarsimp simp: archinv_relation_def page_invocation_map_def
label_to_flush_type_def labelToFlushType_def flush_type_map_def
InvocationLabels_H.isPageFlush_def
split: ArchRetypeDecls_H.flush_type.splits invocation_label.splits)
ArchLabelFuns_H.isPageFlushLabel_def
split: ArchRetypeDecls_H.flush_type.splits invocation_label.splits arch_invocation_label.splits)
apply wp
apply (fastforce simp: valid_cap_def mask_def)
apply auto
@ -656,11 +656,11 @@ lemma vs_refs_pages_ptI:
done
lemmas vs_refs_pages_pt_largeI
= vs_refs_pages_ptI[where pte="ARM_Structs_A.pte.LargePagePTE x y z" for x y z,
= vs_refs_pages_ptI[where pte="Arch_Structs_A.pte.LargePagePTE x y z" for x y z,
unfolded pte_ref_pages_def, simplified, OF _ refl]
lemmas vs_refs_pages_pt_smallI
= vs_refs_pages_ptI[where pte="ARM_Structs_A.pte.SmallPagePTE x y z" for x y z,
= vs_refs_pages_ptI[where pte="Arch_Structs_A.pte.SmallPagePTE x y z" for x y z,
unfolded pte_ref_pages_def, simplified, OF _ refl]
lemma vs_refs_pages_pdI:
@ -673,11 +673,11 @@ lemma vs_refs_pages_pdI:
done
lemmas vs_refs_pages_pd_sectionI
= vs_refs_pages_pdI[where pde="ARM_Structs_A.pde.SectionPDE x y z w" for x y z w,
= vs_refs_pages_pdI[where pde="Arch_Structs_A.pde.SectionPDE x y z w" for x y z w,
unfolded pde_ref_pages_def, simplified, OF _ refl]
lemmas vs_refs_pages_pd_supersectionI
= vs_refs_pages_pdI[where pde="ARM_Structs_A.pde.SuperSectionPDE x y z" for x y z,
= vs_refs_pages_pdI[where pde="Arch_Structs_A.pde.SuperSectionPDE x y z" for x y z,
unfolded pde_ref_pages_def, simplified, OF _ refl]
lemma get_master_pde_sp:
@ -841,8 +841,8 @@ shows
split del: split_if)
apply (cases arch_cap)
apply (simp add: isCap_simps split del: split_if)
apply (cases "invocation_type (mi_label mi) \<noteq> ARMASIDPoolAssign")
apply (simp split: invocation_label.split)
apply (cases "invocation_type (mi_label mi) \<noteq> ArchInvocationLabel ARMASIDPoolAssign")
apply (simp split: invocation_label.split arch_invocation_label.split)
apply (rename_tac word1 word2)
apply (cases "excaps", simp)
apply (cases "excaps'", simp)
@ -895,8 +895,8 @@ shows
apply (clarsimp simp: valid_cap_def)
apply auto[1]
apply (simp add: isCap_simps split del: split_if)
apply (cases "invocation_type (mi_label mi) \<noteq> ARMASIDControlMakePool")
apply (simp split: invocation_label.split)
apply (cases "invocation_type (mi_label mi) \<noteq> ArchInvocationLabel ARMASIDControlMakePool")
apply (simp split: invocation_label.split arch_invocation_label.split)
apply (subgoal_tac "length excaps' = length excaps")
prefer 2
apply (simp add: list_all2_iff)
@ -981,7 +981,7 @@ shows
apply fastforce
apply (rename_tac word cap_rights vmpage_size option)
apply (simp add: isCap_simps split del: split_if)
apply (cases "invocation_type (mi_label mi) = ARMPageMap")
apply (cases "invocation_type (mi_label mi) = ArchInvocationLabel ARMPageMap")
apply (case_tac "\<not>(2 < length args \<and> excaps \<noteq> [])")
apply (auto split: list.split)[1]
apply (simp add: Let_def neq_Nil_conv)
@ -1055,7 +1055,7 @@ shows
apply (wp hoare_drop_imps)
apply (clarsimp simp: invs_def valid_state_def)
apply fastforce
apply (cases "invocation_type (mi_label mi) = ARMPageRemap")
apply (cases "invocation_type (mi_label mi) = ArchInvocationLabel ARMPageRemap")
apply (case_tac "\<not>(1 < length args \<and> excaps \<noteq> [])")
apply (auto split: list.split)[1]
apply (simp add: Let_def split: list.split)
@ -1127,24 +1127,24 @@ shows
apply fastforce
apply (simp split del: split_if)
apply (cases "invocation_type (mi_label mi) = ARMPageUnmap")
apply (cases "invocation_type (mi_label mi) = ArchInvocationLabel ARMPageUnmap")
apply simp
apply (rule corres_returnOk)
apply (clarsimp simp: archinv_relation_def page_invocation_map_def)
apply (cases "InvocationLabels_H.isPageFlush (invocation_type (mi_label mi))")
apply (clarsimp simp: InvocationLabels_H.isPageFlush_def split del: split_if)
apply (clarsimp split: invocation_label.splits split del: split_if)
apply (rule dec_arch_inv_page_flush_corres,
clarsimp simp: InvocationLabels_H.isPageFlush_def)+
apply (clarsimp simp: InvocationLabels_H.isPageFlush_def split del: split_if)
apply (cases "invocation_type (mi_label mi) = ARMPageGetAddress")
apply (cases "ArchLabelFuns_H.isPageFlushLabel (invocation_type (mi_label mi))")
apply (clarsimp simp: ArchLabelFuns_H.isPageFlushLabel_def split del: split_if)
apply (clarsimp split: invocation_label.splits arch_invocation_label.splits split del: split_if)
apply (rule dec_arch_inv_page_flush_corres,
clarsimp simp: ArchLabelFuns_H.isPageFlushLabel_def)+
apply (clarsimp simp: ArchLabelFuns_H.isPageFlushLabel_def split del: split_if)
apply (cases "invocation_type (mi_label mi) = ArchInvocationLabel ARMPageGetAddress")
apply simp
apply (rule corres_returnOk)
apply (clarsimp simp: archinv_relation_def page_invocation_map_def)
apply (clarsimp split: invocation_label.splits split del: split_if)
apply (clarsimp split: invocation_label.splits arch_invocation_label.splits split del: split_if)
apply (simp add: isCap_simps split del: split_if)
apply (simp split: invocation_label.split split del: split_if)
apply (intro conjI impI)
apply (simp split: invocation_label.split arch_invocation_label.splits split del: split_if)
apply (intro conjI impI allI)
apply (simp split: list.split, intro conjI impI allI, simp_all)[1]
apply (clarsimp simp: neq_Nil_conv)
apply (rule whenE_throwError_corres_initial, simp+)
@ -1215,7 +1215,7 @@ shows
erule invs_pspace_aligned', clarsimp+)
apply (simp add: isCap_simps)
apply (simp add: isCap_simps split del: split_if)
apply (cases "InvocationLabels_H.isPDFlush (invocation_type (mi_label mi))")
apply (cases "ArchLabelFuns_H.isPDFlushLabel (invocation_type (mi_label mi))")
apply (clarsimp split del: split_if)
apply (cases args, simp)
apply (rename_tac a0 as)
@ -1733,7 +1733,7 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]:
done
lemma arch_decodeARMPageFlush_wf:
"InvocationLabels_H.isPageFlush (invocation_type label) \<Longrightarrow>
"ArchLabelFuns_H.isPageFlushLabel (invocation_type label) \<Longrightarrow>
\<lbrace>invs' and
valid_cap'
(capability.ArchObjectCap (arch_capability.PageCap word vmrights vmpage_size option)) and
@ -1785,7 +1785,7 @@ lemma arch_decodeInvocation_wf[wp]:
apply assumption
apply (simp add: decodeARMMMUInvocation_def ArchRetype_H.decodeInvocation_def
Let_def split_def isCap_simps
cong: if_cong invocation_label.case_cong list.case_cong prod.case_cong
cong: if_cong invocation_label.case_cong arch_invocation_label.case_cong list.case_cong prod.case_cong
split del: split_if)
apply (rule hoare_pre)
apply ((wp whenE_throwError_wp ensureEmptySlot_stronger|
@ -1830,7 +1830,7 @@ lemma arch_decodeInvocation_wf[wp]:
apply (simp add: decodeARMMMUInvocation_def ArchRetype_H.decodeInvocation_def
Let_def split_def isCap_simps
cong: if_cong split del: split_if)
apply (cases "invocation_type label = ARMPageMap")
apply (cases "invocation_type label = ArchInvocationLabel ARMPageMap")
apply (rename_tac word vmrights vmpage_size option)
apply (simp add: split_def split del: split_if
cong: list.case_cong prod.case_cong)
@ -1856,7 +1856,7 @@ lemma arch_decodeInvocation_wf[wp]:
apply (simp add:vmsz_aligned_def)
apply (erule order_le_less_trans[rotated])
apply (erule is_aligned_no_overflow'[simplified field_simps])
apply (cases "invocation_type label = ARMPageRemap")
apply (cases "invocation_type label = ArchInvocationLabel ARMPageRemap")
apply (rename_tac word vmrights vmpage_size option)
apply (simp add: split_def invs_valid_objs' split del: split_if
cong: list.case_cong prod.case_cong)
@ -1883,26 +1883,26 @@ lemma arch_decodeInvocation_wf[wp]:
vmsz_aligned'_def pdBits_def pageBits_def vmsz_aligned_def
dest!: diminished_capMaster)
apply (erule is_aligned_addrFromPPtr_n, case_tac vmpage_size, simp_all)[1]
apply (cases "invocation_type label = ARMPageUnmap")
apply (cases "invocation_type label = ArchInvocationLabel ARMPageUnmap")
apply (simp split del: split_if)
apply (rule hoare_pre, wp)
apply (clarsimp simp: valid_arch_inv'_def valid_page_inv'_def)
apply (thin_tac "Ball S P" for S P)
apply (erule cte_wp_at_weakenE')
apply (clarsimp simp: is_arch_update'_def isCap_simps dest!: diminished_capMaster)
apply (cases "InvocationLabels_H.isPageFlush (invocation_type label)")
apply (clarsimp simp: InvocationLabels_H.isPageFlush_def split: invocation_label.splits)
apply (cases "ArchLabelFuns_H.isPageFlushLabel (invocation_type label)")
apply (clarsimp simp: ArchLabelFuns_H.isPageFlushLabel_def split: invocation_label.splits arch_invocation_label.splits)
apply (rule arch_decodeARMPageFlush_wf,
clarsimp simp: InvocationLabels_H.isPageFlush_def)+
apply (cases "invocation_type label = ARMPageGetAddress")
clarsimp simp: ArchLabelFuns_H.isPageFlushLabel_def)+
apply (cases "invocation_type label = ArchInvocationLabel ARMPageGetAddress")
apply (simp split del: split_if)
apply (rule hoare_pre, wp)
apply (clarsimp simp: valid_arch_inv'_def valid_page_inv'_def)
apply (simp add: InvocationLabels_H.isPageFlush_def throwError_R'
split: invocation_label.split_asm)
apply (simp add: ArchLabelFuns_H.isPageFlushLabel_def throwError_R'
split: invocation_label.split_asm arch_invocation_label.split_asm)
apply (simp add: decodeARMMMUInvocation_def ArchRetype_H.decodeInvocation_def
Let_def split_def isCap_simps vs_entry_align_def
cong: if_cong list.case_cong invocation_label.case_cong prod.case_cong
cong: if_cong list.case_cong invocation_label.case_cong arch_invocation_label.case_cong prod.case_cong
split del: split_if)
apply (rename_tac word option)
apply (rule hoare_pre)
@ -1948,7 +1948,7 @@ lemma arch_decodeInvocation_wf[wp]:
apply (erule order_le_less_trans[rotated])
apply (rule word_and_le2)
apply (simp add: decodeARMMMUInvocation_def ArchRetype_H.decodeInvocation_def isCap_simps Let_def)
apply(cases "isPDFlush (invocation_type label)", simp_all)
apply(cases "ArchLabelFuns_H.isPDFlushLabel (invocation_type label)", simp_all)
apply(cases args, simp_all)
apply(rule hoare_pre, wp)
defer

62
proof/refine/CNodeInv_R.thy
View File

@ -165,11 +165,11 @@ lemma cnode_invok_case_cleanup:
lemma reycleRightsEq:
"cap_relation cap cap' \<Longrightarrow> hasRecycleRights cap' = has_recycle_rights cap"
apply (auto simp: hasRecycleRights_def has_recycle_rights_def all_rights_def
by (auto simp: hasRecycleRights_def has_recycle_rights_def all_rights_def
arch_has_recycle_rights_def
ArchRetype_H.hasRecycleRights_def vmrights_map_def
split: cap.splits arch_cap.splits bool.splits if_splits
|case_tac x)+
done
split: cap.splits arch_cap.splits bool.splits if_splits |
case_tac x)+
lemma dec_cnode_inv_corres:
"\<lbrakk> cap_relation (cap.CNodeCap w n list) cap'; list_all2 cap_relation cs cs';
@ -207,9 +207,9 @@ lemma dec_cnode_inv_corres:
in corres_splitEE)
prefer 2
apply (rule corres_trivial)
apply (auto split: list.split invocation_label.split,
auto simp: returnOk_def all_rights_def
rightsFromWord_correspondence)[1]
subgoal by (auto split: list.split invocation_label.split,
auto simp: returnOk_def all_rights_def
rightsFromWord_correspondence)
apply (rule_tac r'=cap_relation in corres_splitEE)
prefer 2
apply (simp add: returnOk_def del: imp_disjL)
@ -222,12 +222,12 @@ lemma dec_cnode_inv_corres:
apply (clarsimp simp: maskCapRights_twice cap_map_update_data
split: option.split)
apply (rule corres_trivial)
apply (auto simp add: whenE_def, auto simp add: returnOk_def)[1]
subgoal by (auto simp add: whenE_def, auto simp add: returnOk_def)
apply (wp | wpc | simp(no_asm))+
apply (wp hoare_vcg_const_imp_lift_R hoare_vcg_const_imp_lift
hoare_vcg_all_lift_R hoare_vcg_all_lift lsfco_cte_at' hoare_drop_imps
| clarsimp)+
apply (auto elim!: valid_cnode_capI)[1]
subgoal by (auto elim!: valid_cnode_capI)
apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def)
-- "Revoke"
apply (simp add: decode_cnode_invocation_def decodeCNodeInvocation_def
@ -534,8 +534,7 @@ lemma decodeCNodeInv_wf[wp]:
simp_all add: decodeCNodeInvocation_def isCNodeCap_CNodeCap
unlessE_whenE cnode_invok_case_cleanup
split: list.split_asm list.split)
apply (auto simp: valid_def validE_def validE_R_def in_monad)
done
by (auto simp: valid_def validE_def validE_R_def in_monad)
declare updateCapData_Zombie' [simp del]
@ -548,8 +547,11 @@ lemma decodeCNodeInvocation_inv[wp]:
apply (simp_all add: decodeCNodeInvocation_def isCNodeCap_CNodeCap split_def
Let_def whenE_def unlessE_def cnode_invok_case_cleanup
split del: split_if cong del: if_cong)[6]
apply (safe intro!: hoare_pre[where P=P],
(wp hoare_drop_imps | simp | wpcw)+)[6]
apply fold_subgoals[6]
subgoal
apply unfold_subgoals
by (safe intro!: hoare_pre[where P=P],
(wp hoare_drop_imps | simp | wpcw)+)
apply (elim disjE exE conjE,
simp_all add: decodeCNodeInvocation_def isCNodeCap_CNodeCap
cnode_invok_case_cleanup unlessE_whenE
@ -3062,8 +3064,7 @@ proof -
thus ?thesis using md nz
unfolding n_def n'_def
apply (simp only: dest2_next dest2_prev)
apply (clarsimp simp add: modify_map_same modify_map_other)
done
by (clarsimp simp add: modify_map_same modify_map_other)
qed
qed
@ -3087,8 +3088,7 @@ proof -
thus ?thesis using nz md neg_pos
unfolding n_def n'_def
apply (simp only: dest2_next dest2_prev)
apply (clarsimp simp add: modify_map_same modify_map_other)
done
by (clarsimp simp add: modify_map_same modify_map_other)
next
case pos_neg
hence pd: "mdbPrev src_node = dest" by simp
@ -3104,15 +3104,13 @@ proof -
thus ?thesis using md p_0 pd pos_neg nz
unfolding n_def n'_def
apply (simp only: dest2_next dest2_prev)
apply (clarsimp simp add: modify_map_same modify_map_other del: dest2_parts )
done
by (clarsimp simp add: modify_map_same modify_map_other del: dest2_parts )
next
case neg_neg
thus ?thesis using md nz
unfolding n_def n'_def
apply (simp only: dest2_next dest2_prev)
apply (clarsimp simp add: modify_map_same modify_map_other)
done
by (clarsimp simp add: modify_map_same modify_map_other)
qed
qed
@ -4438,8 +4436,7 @@ lemma (in mdb_swap) n_cap_eq':
apply (rule conjI, clarsimp)
apply (rule iffI)
apply (fastforce dest: n_cap)
apply (simp add: n_def modify_map_if dest2_node_def n'_def)
apply auto[1]
subgoal by (simp add: n_def modify_map_if dest2_node_def n'_def, auto)
apply clarsimp
apply (rule conjI, fastforce)
apply clarsimp
@ -4966,9 +4963,8 @@ proof -
apply (frule n_cap)
apply (frule revokable)
apply (auto simp: weak_derived'_def dest2_node_def
split: split_if_asm)
done
by (auto simp: weak_derived'_def dest2_node_def
split: split_if_asm)
qed
lemma scap_class[simp]:
@ -5841,16 +5837,16 @@ lemma make_zombie_invs':
apply clarify
apply (thin_tac "\<not> isUntypedCap cap" for cap)
apply (clarsimp simp: isCap_simps split: split_if_asm)
apply ((elim disjE | clarsimp simp: isCap_simps)+)[1]
apply (fastforce simp: isCap_simps sameRegionAs_def3)
subgoal by ((elim disjE | clarsimp simp: isCap_simps)+)
subgoal by (fastforce simp: isCap_simps sameRegionAs_def3)
apply (clarsimp simp: mdb_next_unfold)
apply (erule_tac x=p in allE)
apply (erule_tac x="mdbNext node" in allE)
apply simp
subgoal by simp
apply (rule conjI)
apply clarsimp
apply (erule (1) caps_contained_subrange, simp)
apply (clarsimp simp: isCap_simps)
subgoal by (clarsimp simp: isCap_simps)
apply (clarsimp simp add: isCap_simps)
apply (subgoal_tac "valid_mdb' s")
prefer 2
@ -8790,8 +8786,7 @@ proof
apply (erule_tac x=p in allE, erule_tac x=src in allE,
erule allE, erule impE, erule exI)
apply clarsimp
apply fastforce
done
by fastforce
from valid
have "caps_contained' m" by (simp add: valid_mdb_ctes_def)
@ -8812,8 +8807,7 @@ proof
apply (drule capMaster_capRange)
apply clarsimp
apply blast
apply fastforce
done
by fastforce
show "mdb_chunked m'" by (rule chunked')

8
proof/refine/CSpace1_R.thy
View File

@ -1902,7 +1902,7 @@ lemma other_obj_relation_KOCTE[simp]:
"\<not> other_obj_relation ko (KOCTE cte)"
by (simp add: other_obj_relation_def
split: Structures_A.kernel_object.splits
ARM_Structs_A.arch_kernel_obj.splits)
Arch_Structs_A.arch_kernel_obj.splits)
lemma cte_map_pulls_tcb_to_abstract:
"\<lbrakk> y = cte_map z; pspace_relation (kheap s) (ksPSpace s');
@ -1915,7 +1915,7 @@ lemma cte_map_pulls_tcb_to_abstract:
apply (erule(1) obj_relation_cutsE, simp_all)
apply (clarsimp simp: other_obj_relation_def
split: Structures_A.kernel_object.split_asm
ARM_Structs_A.arch_kernel_obj.split_asm)
Arch_Structs_A.arch_kernel_obj.split_asm)
apply (drule tcb_cases_related2)
apply clarsimp
apply (frule(1) cte_wp_at_tcbI [OF _ _ TrueI, where t="(a, b)" for a b, simplified])
@ -2194,7 +2194,7 @@ lemma pspace_relation_cte_wp_atI':
apply (erule(1) obj_relation_cutsE, simp_all)
apply (simp add: other_obj_relation_def
split: Structures_A.kernel_object.split_asm
ARM_Structs_A.arch_kernel_obj.split_asm)
Arch_Structs_A.arch_kernel_obj.split_asm)
apply (subgoal_tac "n = x - y", clarsimp)
apply (drule tcb_cases_related2, clarsimp)
apply (intro exI, rule conjI)
@ -2925,7 +2925,7 @@ lemma updateMDB_pspace_relation:
apply (rule pspace_dom_relatedE, assumption+)
apply (rule obj_relation_cutsE, assumption+, simp_all)[1]
apply (clarsimp split: Structures_A.kernel_object.split_asm
ARM_Structs_A.arch_kernel_obj.split_asm
Arch_Structs_A.arch_kernel_obj.split_asm
simp: other_obj_relation_def)
apply (frule(1) tcb_cte_cases_aligned_helpers(1))
apply (frule(1) tcb_cte_cases_aligned_helpers(2))

52
proof/refine/CSpace_R.thy
View File

@ -1034,7 +1034,7 @@ lemma cap_move_corres:
apply (drule updateCap_stuff, clarsimp)
apply (subgoal_tac "pspace_distinct' b \<and> pspace_aligned' b")
prefer 2
apply fastforce
subgoal by fastforce
apply (thin_tac "ctes_of t = s" for t s)+
apply (thin_tac "ksMachineState t = p" for t p)+
apply (thin_tac "ksCurThread t = p" for t p)+
@ -1076,7 +1076,7 @@ lemma cap_move_corres:
apply clarsimp
apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
prefer 2
apply (clarsimp simp: null_filter_def split: if_splits)
subgoal by (clarsimp simp: null_filter_def split: if_splits)
apply clarsimp
apply (subgoal_tac "cte_at (aa,bb) a")
prefer 2
@ -1093,7 +1093,7 @@ lemma cap_move_corres:
apply fastforce
apply fastforce
apply clarsimp
apply (simp add: null_filter_def split: if_splits)
subgoal by (simp add: null_filter_def split: if_splits)
apply (subgoal_tac "mdb_move (ctes_of b) (cte_map ptr) src_cap src_node (cte_map ptr') cap' old_dest_node")
prefer 2
apply (rule mdb_move.intro)
@ -1165,7 +1165,7 @@ lemma cap_move_corres:
apply(simp, fastforce, simp)
apply(fastforce split: option.splits)
apply(case_tac "ctes_of b (cte_map (aa, bb))")
apply(clarsimp simp: modify_map_def split: split_if_asm)
subgoal by (clarsimp simp: modify_map_def split: split_if_asm)
apply(case_tac ab)
apply(frule mdb_move.m'_next)
apply(simp, fastforce)
@ -1184,15 +1184,14 @@ lemma cap_move_corres:
apply(case_tac "next_slot (aa, bb) (cdt_list (a)) (cdt a) = Some ptr")
apply(frule(3) cte_at_next_slot)
apply(erule_tac x=aa in allE, erule_tac x=bb in allE)
apply(clarsimp simp: cte_map_inj_eq valid_pspace_def split: split_if_asm)
subgoal by (clarsimp simp: cte_map_inj_eq valid_pspace_def split: split_if_asm)
apply(simp)
apply(case_tac "next_slot (aa, bb) (cdt_list (a)) (cdt a)")
apply(simp)
apply(frule(3) cte_at_next_slot)
apply(frule(3) cte_at_next_slot')
apply(erule_tac x=aa in allE, erule_tac x=bb in allE)
apply(clarsimp simp: cte_map_inj_eq valid_pspace_def split: split_if_asm)
done
by(clarsimp simp: cte_map_inj_eq valid_pspace_def split: split_if_asm)
lemmas cur_tcb_lift =
hoare_lift_Pf [where f = ksCurThread and P = tcb_at', folded cur_tcb'_def]
@ -2558,15 +2557,15 @@ proof -
defer
apply (clarsimp simp:modify_map_cases dest0 src0)
apply (clarsimp simp:revokable'_def badge_derived'_def)
apply (case_tac src_cap,auto simp:isCap_simps sameRegionAs_def)[1]
subgoal by (case_tac src_cap,auto simp:isCap_simps sameRegionAs_def)
apply (clarsimp simp:modify_map_cases valid_badges_def)
apply (frule_tac x=src in spec, erule_tac x=word1 in allE, erule allE, erule impE)
apply fastforce
apply simp
apply (clarsimp simp:mdb_next_unfold badge_derived'_def split: split_if_asm)
apply (thin_tac "All P" for P)
apply (cases src_cap,
auto simp:mdb_next_unfold isCap_simps sameRegionAs_def Let_def split: if_splits)[1]
subgoal by (cases src_cap,
auto simp:mdb_next_unfold isCap_simps sameRegionAs_def Let_def split: if_splits)
apply (case_tac "word1 = p'")
apply (clarsimp simp:modify_map_cases valid_badges_def mdb_next_unfold src0 dest0 no0)+
apply (case_tac "p = dest")
@ -2575,8 +2574,7 @@ proof -
apply (rename_tac capability mdbnode)
apply clarsimp
apply (drule_tac x = p in spec,drule_tac x = "mdbNext mdbnode" in spec)
apply (auto simp:isCap_simps sameRegionAs_def)
done
by (auto simp:isCap_simps sameRegionAs_def)
from badge
have isUntyped_eq: "isUntypedCap cap = isUntypedCap src_cap"
@ -2623,7 +2621,7 @@ proof -
apply (case_tac "p = src")
apply (clarsimp simp:modify_map_def split:if_splits)
apply (drule capRange_untyped)
apply (case_tac cap,auto simp:isCap_simps badge_derived'_def)[1]
subgoal by (case_tac cap,auto simp:isCap_simps badge_derived'_def)
apply (clarsimp simp:modify_map_def split:if_splits)
apply (drule_tac x = word1 in spec)
apply (drule_tac x = src in spec)
@ -2639,8 +2637,7 @@ proof -
apply (drule_tac x = p' in spec)
apply (clarsimp simp:modify_map_def split:if_splits)
apply ((case_tac z,fastforce)+)[5]
apply fastforce+
done
by fastforce+
show "valid_nullcaps ?C"
using is_der vn cofs vd no0
@ -4323,7 +4320,7 @@ lemma arch_update_setCTE_mdb:
apply (clarsimp split: split_if_asm)
apply (clarsimp simp: isCap_simps)
prefer 2
apply fastforce
subgoal by fastforce
apply (erule_tac x=pa in allE)
apply (erule_tac x=p in allE)
apply simp
@ -4340,14 +4337,14 @@ lemma arch_update_setCTE_mdb:
apply (drule sym [where s="capMasterCap cap"])
apply (frule masterCap.intro)
apply (clarsimp simp: masterCap.isUntypedCap split: split_if_asm)
apply fastforce
apply fastforce
subgoal by fastforce
subgoal by fastforce
apply (erule_tac x=pa in allE)
apply (erule_tac x=p in allE)
apply fastforce
apply (erule_tac x=pa in allE)
apply (erule_tac x=p' in allE)
apply fastforce
subgoal by fastforce
apply (rule conjI)
apply (cases oldcte)
apply (clarsimp simp: is_arch_update'_def)
@ -4360,19 +4357,19 @@ lemma arch_update_setCTE_mdb:
apply (clarsimp simp: masterCap.sameRegionAs)
apply (simp add: masterCap.sameRegionAs is_chunk_def mdb_next_trans_next_pres
mdb_next_rtrans_next_pres)
apply fastforce
subgoal by fastforce
apply (erule_tac x=pa in allE)
apply (erule_tac x=p in allE)
apply (clarsimp simp: masterCap.sameRegionAs)
apply (simp add: masterCap.sameRegionAs is_chunk_def mdb_next_trans_next_pres
mdb_next_rtrans_next_pres)
apply fastforce
subgoal by fastforce
apply (erule_tac x=pa in allE)
apply (erule_tac x=p' in allE)
apply clarsimp
apply (simp add: masterCap.sameRegionAs is_chunk_def mdb_next_trans_next_pres
mdb_next_rtrans_next_pres)
apply fastforce
subgoal by fastforce
apply (rule conjI)
apply (clarsimp simp: is_arch_update'_def untyped_mdb'_def arch_update_descendants'
simp del: fun_upd_apply)
@ -4970,7 +4967,7 @@ lemma cins_corres_simple:
apply(case_tac "ca=src")
apply(simp)
apply(clarsimp simp: modify_map_def)
apply(fastforce split: split_if_asm)
subgoal by(fastforce split: split_if_asm)
apply(case_tac "ca = dest")
apply(simp)
apply(case_tac "next_slot src (cdt_list (a)) (cdt a)")
@ -5014,8 +5011,7 @@ lemma cins_corres_simple:
apply(simp_all)[6]
apply(drule cte_map_inj_eq)
apply(simp_all)[6]
apply(fastforce)
done
by(fastforce)
declare split_if [split]
@ -5035,10 +5031,9 @@ lemma safe_parent_for_capRange_capBits:
apply (clarsimp simp: safe_parent_for'_def)
apply (erule disjE)
apply (clarsimp simp: capRange_def)
apply (auto simp: sameRegionAs_def2 isCap_simps capRange_def
by (auto simp: sameRegionAs_def2 isCap_simps capRange_def
capMasterCap_def capRange_Master objBits_simps
split:capability.splits arch_capability.splits)
done
lemma safe_parent_Null:
"\<lbrakk> m src = Some (CTE NullCap n); safe_parent_for' m src c' \<rbrakk> \<Longrightarrow> False"
@ -5100,10 +5095,9 @@ lemma safe_parent_not_ntfn':
lemma safe_parent_capClass:
"\<lbrakk> safe_parent_for' m p cap; m p = Some (CTE src_cap n) \<rbrakk> \<Longrightarrow> capClass cap = capClass src_cap"
apply (auto simp: safe_parent_for'_def isCap_simps sameRegionAs_def2 capRange_Master capRange_def
by (auto simp: safe_parent_for'_def isCap_simps sameRegionAs_def2 capRange_Master capRange_def
capMasterCap_def
split: capability.splits arch_capability.splits)
done
locale mdb_insert_simple' = mdb_insert_simple +
fixes n'

28
proof/refine/Detype_R.thy
View File

@ -1974,22 +1974,15 @@ lemma simpler_updateObject_def:
tcbIPCBufferSlot_def
tcbCallerSlot_def tcbReplySlot_def
tcbCTableSlot_def tcbVTableSlot_def)
apply (intro conjI impI)
apply simp_all
apply (clarsimp simp:alignCheck_def unless_def when_def not_less[symmetric]
alignError_def is_aligned_mask magnitudeCheck_def
cte_update_def return_def tcbIPCBufferSlot_def
tcbCallerSlot_def tcbReplySlot_def
tcbCTableSlot_def tcbVTableSlot_def objBits_simps
cteSizeBits_def split:option.splits,
(fastforce simp:return_def fail_def bind_def | intro conjI)+)+
apply (clarsimp simp:alignCheck_def unless_def when_def not_less[symmetric]
alignError_def is_aligned_mask magnitudeCheck_def
cte_update_def return_def tcbIPCBufferSlot_def
tcbCallerSlot_def tcbReplySlot_def bind_def fail_def
tcbCTableSlot_def tcbVTableSlot_def objBits_simps
cteSizeBits_def split:option.splits)+
done
by (intro conjI impI;
clarsimp simp:alignCheck_def unless_def when_def not_less[symmetric]
alignError_def is_aligned_mask magnitudeCheck_def
cte_update_def return_def tcbIPCBufferSlot_def
tcbCallerSlot_def tcbReplySlot_def
tcbCTableSlot_def tcbVTableSlot_def objBits_simps
cteSizeBits_def split:option.splits;
fastforce simp:return_def fail_def bind_def)+
lemma setCTE_def2:
"(setCTE src cte) =
@ -3696,8 +3689,7 @@ lemma new_cap_object_commute:
apply (intro conjI exI)
apply (clarsimp simp: no_0_def)
apply (clarsimp simp: weak_valid_dlist_def modify_map_def Let_def)
apply (intro conjI impI)
apply fastforce+
subgoal by (intro conjI impI; fastforce)
apply (clarsimp simp:valid_nullcaps_def)
apply (frule_tac x = "p" in spec)
apply (case_tac ctec)

38
proof/refine/Finalise_R.thy
View File

@ -1563,11 +1563,10 @@ lemma empty_slot_corres:
apply (rule mdb_empty.intro)
apply (rule mdb_ptr.intro)
apply (rule vmdb.intro)
apply (simp add: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def)
subgoal by (simp add: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def)
apply (rule mdb_ptr_axioms.intro)
apply simp
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv)
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv)
apply (simp add: pspace_relations_def)
apply (rule conjI)
prefer 2
@ -1585,7 +1584,7 @@ lemma empty_slot_corres:
apply(case_tac "cdt a slot")
apply(simp add: next_slot_eq[OF mdb_empty_abs'.next_slot_no_parent])
apply(case_tac "next_slot (aa, bb) (cdt_list a) (cdt a)")
apply(simp)
subgoal by (simp)
apply(clarsimp)
apply(frule(1) mdb_empty.n_next)
apply(clarsimp)
@ -1599,7 +1598,7 @@ lemma empty_slot_corres:
prefer 2
apply(drule_tac cte="CTE s_cap s_node" in valid_mdbD2')
apply(clarsimp simp: valid_mdb_ctes_def no_0_def)
apply(frule invs_mdb', simp)
subgoal by (frule invs_mdb', simp)
apply(clarsimp)
apply(rule cte_map_inj_eq)
apply(assumption)
@ -1612,7 +1611,7 @@ lemma empty_slot_corres:
apply(simp add: next_slot_eq[OF mdb_empty_abs'.next_slot] split del: split_if)
apply(case_tac "next_slot (aa, bb) (cdt_list a) (cdt a)")
apply(simp)
subgoal by (simp)
apply(case_tac "(aa, bb) = slot", simp)
apply(case_tac "next_slot (aa, bb) (cdt_list a) (cdt a) = Some slot")
apply(simp)
@ -1627,7 +1626,7 @@ lemma empty_slot_corres:
apply(simp)
apply(drule_tac cte="CTE cap' node'" in valid_mdbD1')
apply(fastforce simp: valid_mdb_ctes_def no_0_def)
apply(simp add: valid_mdb'_def)
subgoal by (simp add: valid_mdb'_def)
apply(clarsimp)
apply(simp)
apply(frule(1) mdb_empty.n_next)
@ -1648,7 +1647,7 @@ lemma empty_slot_corres:
apply(drule(3) cte_at_next_slot)
apply(assumption)+
apply(simp)
apply(simp)
subgoal by (simp)
apply (simp add: revokable_relation_def)
apply (clarsimp simp: in_set_cap_cte_at)
apply (rule conjI)
@ -1660,13 +1659,13 @@ lemma empty_slot_corres:
apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
prefer 2
apply (drule set_cap_caps_of_state_monad)
apply (force simp: null_filter_def)
subgoal by (force simp: null_filter_def)
apply clarsimp
apply (subgoal_tac "cte_at (aa, bb) a")
prefer 2
apply (drule null_filter_caps_of_stateD, erule cte_wp_cte_at)
apply (drule (2) cte_map_inj_ps, fastforce)
apply simp
subgoal by simp
apply (clarsimp simp add: cdt_relation_def)
apply (subst mdb_empty_abs.descendants, assumption)
apply (subst mdb_empty.descendants, assumption)
@ -1683,11 +1682,11 @@ lemma empty_slot_corres:
apply fastforce
apply fastforce
apply fastforce
apply simp
apply simp
subgoal by simp
subgoal by simp
apply simp
apply (subgoal_tac "cte_map slot \<notin> descendants_of' (cte_map (aa,bb)) (ctes_of b)")
apply simp
subgoal by simp
apply (erule_tac x=aa in allE, erule allE, erule (1) impE)
apply (drule_tac s="cte_map ` u" for u in sym)
apply clarsimp
@ -2079,15 +2078,14 @@ lemma final_cap_corres':
apply (rule classical)
apply (frule(1) zombies_finalD2[OF _ _ _ invs_zombies],
simp?, clarsimp, assumption+)
apply (clarsimp simp: sameObjectAs_def3 isCap_simps valid_cap_def
subgoal by (clarsimp simp: sameObjectAs_def3 isCap_simps valid_cap_def
obj_at_def is_obj_defs a_type_def final_matters'_def
split: cap.split_asm arch_cap.split_asm
option.split_asm split_if_asm,
simp_all add: is_cap_defs)
apply (rule classical)
apply (clarsimp simp: cap_irqs_def cap_irq_opt_def sameObjectAs_def3 isCap_simps
by (clarsimp simp: cap_irqs_def cap_irq_opt_def sameObjectAs_def3 isCap_simps
split: cap.split_asm)
done
lemma final_cap_corres:
"corres (\<lambda>rv rv'. final_matters' (cteCap cte) \<longrightarrow> rv = rv')
@ -4039,14 +4037,14 @@ lemma arch_recycle_cap_corres:
apply (clarsimp simp: upto_enum_step_def)
apply (erule page_table_pte_atI[simplified shiftl_t2n mult.commute mult.left_commute,simplified])
apply (simp add: ptBits_def pageBits_def pt_bits_stuff)
apply (simp add: word_less_nat_alt unat_of_nat)
apply (simp add: word_less_nat_alt word_le_nat_alt unat_of_nat)
apply clarsimp
apply (cases slot, clarsimp)
apply (intro exI, erule cte_wp_at_weakenE)
apply (clarsimp simp: is_cap_simps word32_shift_by_2 upto_enum_step_def)
apply (rule conjunct2[OF is_aligned_add_helper[OF _ shiftl_less_t2n]],
simp_all add: pt_bits_def pageBits_def ptBits_def)[1]
apply (simp add: word_less_nat_alt unat_of_nat)
apply (simp add: word_less_nat_alt word_le_nat_alt unat_of_nat)
apply clarsimp
apply (clarsimp simp: valid_cap'_def page_table_at'_def shiftl_t2n mult.commute mult.left_commute)
apply (rule conjI[rotated])
@ -4054,7 +4052,7 @@ lemma arch_recycle_cap_corres:
apply (clarsimp simp: upto_enum_step_def)
apply (drule spec, erule mp)
apply (simp add: ptBits_def pageBits_def)
apply (simp add: word_less_nat_alt unat_of_nat)
apply (simp add: word_less_nat_alt word_le_nat_alt unat_of_nat)
-- "PageDirectory"
apply (rule corres_guard_imp)
apply (rule corres_split)
@ -4227,7 +4225,7 @@ lemma set_thread_all_corres:
apply (clarsimp simp: obj_at'_def)
apply (clarsimp simp: projectKOs)
apply (insert e is_t)
apply (clarsimp simp: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits ARM_Structs_A.arch_kernel_obj.splits)
apply (clarsimp simp: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits Arch_Structs_A.arch_kernel_obj.splits)
done
lemma tcb_update_all_corres':

2
proof/refine/Include.thy
View File

@ -12,7 +12,7 @@ theory Include
imports
"../../spec/abstract/Syscall_A"
"../../spec/design/API_H"
"../../spec/design/Intermediate_H"
"../../spec/design/$L4V_ARCH/Intermediate_H"
begin
no_notation bind_drop (infixl ">>" 60)

36
proof/refine/Interrupt_R.thy
View File

@ -25,16 +25,13 @@ where
(\<exists>cap'. x = SetIRQHandler irq cap' (cte_map ptr) \<and> cap_relation cap cap')"
| "irq_handler_inv_relation (Invocations_A.SetMode irq trig pol) x = (x = SetMode irq trig pol)"
consts
interrupt_control_relation :: "arch_interrupt_control \<Rightarrow> interrupt_control \<Rightarrow> bool"
primrec
irq_control_inv_relation :: "irq_control_invocation \<Rightarrow> irqcontrol_invocation \<Rightarrow> bool"
where
"irq_control_inv_relation (Invocations_A.IRQControl irq slot slot') x
= (x = IssueIRQHandler irq (cte_map slot) (cte_map slot'))"
| "irq_control_inv_relation (Invocations_A.InterruptControl ivk) x
= (\<exists>ivk'. x = InterruptControl ivk' \<and> interrupt_control_relation ivk ivk')"
| "irq_control_inv_relation (Invocations_A.ArchInvokeIRQControl z) x
= (x = Invocations_H.ArchInvokeIRQControl ARMNoArchIRQControl)"
primrec
irq_handler_inv_valid' :: "irqhandler_invocation \<Rightarrow> kernel_state \<Rightarrow> bool"
@ -52,12 +49,12 @@ where
primrec
irq_control_inv_valid' :: "irqcontrol_invocation \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"irq_control_inv_valid' (InterruptControl ivk) = \<bottom>"
| "irq_control_inv_valid' (IssueIRQHandler irq ptr ptr') =
"irq_control_inv_valid' (IssueIRQHandler irq ptr ptr') =
(cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) ptr and
cte_wp_at' (\<lambda>cte. cteCap cte = IRQControlCap) ptr' and
ex_cte_cap_to' ptr and real_cte_at' ptr and
(Not o irq_issued' irq) and K (irq \<le> maxIRQ))"
| "irq_control_inv_valid' (ArchInvokeIRQControl _) = \<bottom>"
lemma data_to_bool_toBool[simp]:
"data_to_bool dat = toBool dat"
@ -128,17 +125,17 @@ lemma whenE_rangeCheck_eq:
(whenE (x < fromIntegral y \<or> fromIntegral z < x)
(throwError (RangeError (fromIntegral y) (fromIntegral z))))"
by (simp add: rangeCheck_def unlessE_whenE ucast_id linorder_not_le[symmetric])
thm decodeIRQControl_def
lemma decode_irq_control_corres:
"list_all2 cap_relation caps caps' \<Longrightarrow>
corres (ser \<oplus> irq_control_inv_relation)
(invs and (\<lambda>s. \<forall>cp \<in> set caps. s \<turnstile> cp)) (invs' and (\<lambda>s. \<forall>cp \<in> set caps'. s \<turnstile>' cp))
(decode_irq_control_invocation label args slot caps)
(decodeIRQControlInvocation label args (cte_map slot) caps')"
apply (clarsimp simp: decode_irq_control_invocation_def decodeIRQControlInvocation_def
decodeInterruptControl_def arch_decode_interrupt_control_def
split del: split_if cong: if_cong
split: invocation_label.split)
unfolding decode_irq_control_invocation_def decodeIRQControlInvocation_def
decodeIRQControl_def arch_decode_irq_control_def
apply (cases "invocation_type label";
clarsimp split del: split_if cong: if_cong)
apply (cases caps, simp split: list.split)
apply (case_tac "\<exists>n. length args = Suc (Suc (Suc n))")
apply (clarsimp simp: list_all2_Cons1 Let_def split_def liftE_bindE
@ -165,7 +162,7 @@ lemma decode_irq_control_corres:
done
crunch inv[wp]: decodeIRQControlInvocation "P"
(simp: crunch_simps decodeInterruptControl_def)
(simp: crunch_simps)
(* Levity: added (20090201 10:50:27) *)
declare ensureEmptySlot_stronger [wp]
@ -197,7 +194,7 @@ lemma decode_irq_control_valid'[wp]:
apply (rule hoare_pre)
apply (wp ensureEmptySlot_stronger isIRQActive_wp
whenE_throwError_wp
| simp add: decodeInterruptControl_def | wpc
| simp add: decodeIRQControl_def | wpc
| wp_once hoare_drop_imps)+
apply (clarsimp simp: minIRQ_def maxIRQ_def
toEnum_of_nat word_le_nat_alt unat_of_nat)
@ -331,8 +328,8 @@ lemma invoke_irq_control_corres:
corres (intr \<oplus> dc) (einvs and irq_control_inv_valid i)
(invs' and irq_control_inv_valid' i')
(invoke_irq_control i)
(invokeIRQControl i')"
apply (cases i, simp_all add: invokeIRQControl_def)
(performIRQControl i')"
apply (cases i, simp_all add: performIRQControl_def)
apply (rule corres_guard_imp)
apply (rule corres_split_nor [OF _ set_irq_state_corres])
apply (rule cins_corres_simple)
@ -348,7 +345,6 @@ lemma invoke_irq_control_corres:
apply (case_tac ctea)
apply (clarsimp simp: isCap_simps sameRegionAs_def3)
apply (auto dest: valid_irq_handlers_ctes_ofD)[1]
apply (clarsimp simp: arch_invoke_irq_control_def invokeInterruptControl_def)
done
crunch valid_cap'[wp]: setIRQState "valid_cap' cap"
@ -370,8 +366,8 @@ lemma setIRQState_issued[wp]:
done
lemma invoke_irq_control_invs'[wp]:
"\<lbrace>invs' and irq_control_inv_valid' i\<rbrace> invokeIRQControl i \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (cases i, simp_all add: invokeIRQControl_def)
"\<lbrace>invs' and irq_control_inv_valid' i\<rbrace> performIRQControl i \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (cases i, simp_all add: performIRQControl_def)
apply (rule hoare_pre)
apply (wp cteInsert_simple_invs | simp add: cte_wp_at_ctes_of)+
apply (clarsimp simp: cte_wp_at_ctes_of IRQHandler_valid'
@ -450,8 +446,6 @@ lemma tcbSchedAppend_invs_but_ct_not_inQ':
"\<lbrace>invs' and st_tcb_at' runnable' t \<rbrace>
tcbSchedAppend t \<lbrace>\<lambda>_. all_invs_but_ct_not_inQ'\<rbrace>"
apply (simp add: invs'_def valid_state'_def)
thm ct_idle_or_in_cur_domain'_lift2
thm valid_queues_def
apply (wp sch_act_wf_lift valid_irq_node_lift irqs_masked_lift
valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2
| simp add: cteCaps_of_def

10
proof/refine/Invariants_H.thy
View File

@ -370,18 +370,18 @@ where valid_cap'_def:
\<and> (case b of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0
\<and> (\<forall>addr. real_cte_at' (r + 16 * (addr && mask n)) s))
| Structures_H.ArchObjectCap ac \<Rightarrow> (case ac of
ARMStructures_H.ASIDPoolCap pool asid \<Rightarrow>
ArchStructures_H.ASIDPoolCap pool asid \<Rightarrow>
typ_at' (ArchT ASIDPoolT) pool s \<and> is_aligned asid asid_low_bits \<and> asid \<le> 2^asid_bits - 1
| ARMStructures_H.ASIDControlCap \<Rightarrow> True
| ARMStructures_H.PageCap ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and>
| ArchStructures_H.ASIDControlCap \<Rightarrow> True
| ArchStructures_H.PageCap ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and>
(\<forall>p < 2 ^ (pageBitsForSize sz - pageBits). typ_at' UserDataT (ref + p * 2 ^ pageBits) s) \<and>
(case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow>
0 < asid \<and> asid \<le> 2 ^ asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < kernelBase)
| ARMStructures_H.PageTableCap ref mapdata \<Rightarrow>
| ArchStructures_H.PageTableCap ref mapdata \<Rightarrow>
page_table_at' ref s \<and>
(case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow>
0 < asid \<and> asid \<le> 2^asid_bits - 1 \<and> ref < kernelBase)
| ARMStructures_H.PageDirectoryCap ref mapdata \<Rightarrow>
| ArchStructures_H.PageDirectoryCap ref mapdata \<Rightarrow>
page_directory_at' ref s \<and>
case_option True (\<lambda>asid. 0 < asid \<and> asid \<le> 2^asid_bits - 1) mapdata))"

37
proof/refine/Ipc_R.thy
View File

@ -21,7 +21,7 @@ lemma get_mi_corres: "corres (op = \<circ> message_info_map)
apply (rule corres_guard_imp)
apply (unfold get_message_info_def getMessageInfo_def fun_app_def)
apply (simp add: State_H.msgInfoRegister_def
ARMMachineTypes.msgInfoRegister_def msg_info_register_def)
MachineTypes.msgInfoRegister_def msg_info_register_def)
apply (rule corres_split_eqr [OF _ user_getreg_corres])
apply (rule corres_trivial, simp add: message_info_from_data_eqv)
apply (wp | simp)+
@ -657,8 +657,8 @@ next
apply clarsimp
apply (intro conjI)
apply (drule(1) bspec,clarsimp)+
apply (case_tac "capa = aa")
apply ((clarsimp split:if_splits simp:masked_as_full_def is_cap_simps)+)[2]
subgoal for \<dots> aa _ _ capa
by (case_tac "capa = aa"; clarsimp split:if_splits simp:masked_as_full_def is_cap_simps)
apply (case_tac "isEndpointCap (fst y) \<and> capEPPtr (fst y) = the ep \<and> (\<exists>y. ep = Some y)")
apply (clarsimp simp:conj_comms split del:split_if)
apply (subst if_not_P)
@ -682,8 +682,7 @@ next
apply (rule conjI)
apply clarsimp+
apply (case_tac "cteCap cteb = ab")
apply (clarsimp simp: isCap_simps maskedAsFull_def split:if_splits)+
done
by (clarsimp simp: isCap_simps maskedAsFull_def split:if_splits)+
qed
declare constOnFailure_wp [wp]
@ -846,8 +845,7 @@ lemma transferCapsToSlots_presM:
apply (rule conjI | clarsimp)+
apply (case_tac "cteCap cteb \<noteq> aa")
apply (clarsimp simp:maskedAsFull_def isCap_simps )
apply (clarsimp simp:maskedAsFull_def split:split_if_asm)
done
by (clarsimp simp:maskedAsFull_def split:split_if_asm)
lemmas transferCapsToSlots_pres2
= transferCapsToSlots_presM[where vo=False and emx=True
@ -1305,8 +1303,7 @@ lemma capRights_Null_eq [simp]:
lemma updateCapData_not_nullD:
"updateCapData p d cap \<noteq> NullCap \<Longrightarrow> cap \<noteq> NullCap"
apply (cases cap)
apply (simp_all add: updateCapData_def isCap_simps)
done
by (simp_all add: updateCapData_def isCap_simps)
lemma cte_wp_at_orth':
"\<lbrakk> cte_wp_at' (\<lambda>c. P c) p s; cte_wp_at' (\<lambda>c. \<not> P c) p s \<rbrakk> \<Longrightarrow> False"
@ -2060,7 +2057,7 @@ lemma handle_fault_reply_registers_corres:
(do y \<leftarrow> as_user t
(zipWithM_x
(\<lambda>r v. set_register r
(ARMMachineTypes.sanitiseRegister r v))
(MachineTypes.sanitiseRegister r v))
msg_template msg);
return (label = 0)
od)
@ -2768,7 +2765,7 @@ proof -
apply (drule(1) sym_refs_obj_atD[where P="\<lambda>ob. ob = e" for e])
apply (clarsimp simp: st_tcb_at_refs_of_rev st_tcb_at_reply_cap_valid st_tcb_at_caller_cap_null)
apply (fastforce simp: st_tcb_def2 valid_sched_def valid_sched_action_def)
apply (auto simp: valid_ep'_def invs'_def valid_state'_def split: list.split)[1]
subgoal by (auto simp: valid_ep'_def invs'_def valid_state'_def split: list.split)
apply wp
apply (clarsimp)+
apply (rule corres_guard_imp)
@ -2852,9 +2849,9 @@ proof -
apply (clarsimp simp: st_tcb_at_refs_of_rev st_tcb_at_reply_cap_valid
st_tcb_at_caller_cap_null)
apply (fastforce simp: st_tcb_def2 valid_sched_def valid_sched_action_def)
apply (auto simp: valid_ep'_def
split: list.split)[1]
apply (clarsimp simp: invs'_def valid_state'_def)+
subgoal by (auto simp: valid_ep'_def
split: list.split;
clarsimp simp: invs'_def valid_state'_def)
apply wp
apply (clarsimp)+
done
@ -4370,10 +4367,10 @@ lemma rai_invs'[wp]:
lemma zobj_refs_maskCapRights[simp]:
"zobj_refs' (maskCapRights msk cap) = zobj_refs' cap"
by (cases cap,
simp_all add: maskCapRights_def isCap_simps
by (cases cap;
clarsimp
simp add: maskCapRights_def isCap_simps
Let_def ArchRetype_H.maskCapRights_def
split del: split_if
split: arch_capability.split)
lemma getCTE_cap_to_refs[wp]:
@ -4570,7 +4567,7 @@ lemma si_invs'[wp]:
simp: tcb_bound_refs'_def)
apply (clarsimp simp: set_eq_subset)
apply (rule conjI, erule delta_sym_refs)
apply (fastforce simp: obj_at'_def projectKOs symreftype_inverse'
subgoal by (fastforce simp: obj_at'_def projectKOs symreftype_inverse'
split: split_if_asm)
apply (fastforce simp: tcb_bound_refs'_def symreftype_inverse'
split: split_if_asm)
@ -4657,8 +4654,8 @@ lemma sts_invs_minor'':
apply (drule obj_at_valid_objs')
apply (clarsimp simp: valid_pspace'_def)
apply (clarsimp simp: valid_obj'_def valid_tcb'_def projectKOs)
apply (fastforce simp: valid_tcb_state'_def
split: Structures_H.thread_state.splits)
subgoal by (fastforce simp: valid_tcb_state'_def
split: Structures_H.thread_state.splits)
apply (rule conjI)
apply (clarsimp dest!: st_tcb_at_state_refs_ofD'
elim!: rsubst[where P=sym_refs]

8
proof/refine/KHeap_R.thy
View File

@ -166,7 +166,7 @@ lemma koType_objBitsKO:
"koTypeOf k = koTypeOf k' \<Longrightarrow> objBitsKO k = objBitsKO k'"
by (auto simp: objBitsKO_def archObjSize_def
split: Structures_H.kernel_object.splits
ARMStructures_H.arch_kernel_object.splits)
ArchStructures_H.arch_kernel_object.splits)
lemma updateObject_objBitsKO:
"(ko', t') \<in> fst (updateObject (val :: 'a :: pspace_storable) ko p q n t)
@ -180,7 +180,7 @@ lemma objBitsKO_bounded:
apply (cases ko)
apply (simp_all add: word_bits_def pageBits_def
objBitsKO_simps archObjSize_def
split: ARMStructures_H.arch_kernel_object.splits)
split: ArchStructures_H.arch_kernel_object.splits)
done
lemma updateObject_cte_is_tcb_or_cte:
@ -981,7 +981,7 @@ lemma obj_relation_cut_same_type:
pte_relation_def pde_relation_def
split: Structures_A.kernel_object.split_asm split_if_asm
Structures_H.kernel_object.split_asm
ARM_Structs_A.arch_kernel_obj.split_asm)
Arch_Structs_A.arch_kernel_obj.split_asm)
done
definition exst_same :: "Structures_H.tcb \<Rightarrow> Structures_H.tcb \<Rightarrow> bool"
@ -1055,7 +1055,7 @@ lemma set_other_obj_corres:
apply (clarsimp simp: obj_at'_def)
apply (erule_tac x=obj in allE)
apply (clarsimp simp: projectKO_eq project_inject)
apply (clarsimp simp: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type t exst_same_def split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits ARM_Structs_A.arch_kernel_obj.splits)
apply (clarsimp simp: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type t exst_same_def split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits Arch_Structs_A.arch_kernel_obj.splits)
done
lemma set_ep_corres:

4
proof/refine/Orphanage.thy
View File

@ -1966,9 +1966,9 @@ lemma invokeCNode_no_orphans [wp]:
lemma invokeIRQControl_no_orphans [wp]:
"\<lbrace> \<lambda>s. no_orphans s \<rbrace>
invokeIRQControl i
performIRQControl i
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
apply (cases i, simp_all add: invokeIRQControl_def invokeInterruptControl_def)
apply (cases i, simp_all add: performIRQControl_def ArchInterrupt_H.performIRQControl_def)
apply (wp | clarsimp)+
done

8
proof/refine/PageTableDuplicates.thy
View File

@ -2039,11 +2039,11 @@ crunch valid_duplicates'[wp]:
sendSignal "\<lambda>s. vs_valid_duplicates' (ksPSpace s)"
lemma invokeIRQControl_valid_duplicates'[wp]:
"\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<rbrace> invokeIRQControl a
"\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<rbrace> performIRQControl a
\<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
apply (simp add:invokeIRQControl_def invokeInterruptControl_def)
apply (simp add:performIRQControl_def )
apply (rule hoare_pre)
apply (wp|wpc | simp add:invokeInterruptControl_def)+
apply (wp|wpc | simp add:ArchInterrupt_H.performIRQControl_def)+
apply fastforce
done
@ -2052,7 +2052,7 @@ lemma invokeIRQHandler_valid_duplicates'[wp]:
\<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
apply (simp add:invokeIRQHandler_def)
apply (rule hoare_pre)
apply (wp|wpc | simp add:invokeInterruptControl_def)+
apply (wp|wpc | simp add:ArchInterrupt_H.performIRQControl_def)+
done
lemma invokeCNode_valid_duplicates'[wp]:

11
proof/refine/Retype_R.thy
View File

@ -1183,7 +1183,7 @@ lemma retype_ekheap_relation:
apply (clarsimp simp add: ekheap_relation_def
pspace_relation_def default_ext_def cong: if_cong
split: split_if_asm)
apply (clarsimp simp add: makeObjectKO_def APIType_map2_def cong: if_cong split: sum.splits Structures_H.kernel_object.splits
subgoal by (clarsimp simp add: makeObjectKO_def APIType_map2_def cong: if_cong split: sum.splits Structures_H.kernel_object.splits
arch_kernel_object.splits ArchTypes_H.object_type.splits ArchTypes_H.apiobject_type.splits)
apply (frule ekh_at_tcb_at[OF et])
apply (intro impI conjI)
@ -1194,7 +1194,8 @@ lemma retype_ekheap_relation:
apply (clarsimp simp add: makeObjectKO_def cong: if_cong split: sum.splits Structures_H.kernel_object.splits
arch_kernel_object.splits ArchTypes_H.object_type.splits ArchTypes_H.apiobject_type.splits)
apply (drule_tac x=xa in bspec,simp)
apply (force+)[2]
subgoal by force
subgoal by force
apply (simp add: foldr_upd_app_if' foldr_upd_app_if[folded data_map_insert_def])
apply (simp add: obj_relation_retype_addrs_eq[OF not_unt num_r orr cover,symmetric])
apply (clarsimp simp add: APIType_map2_def default_ext_def ekheap_relation_def
@ -4562,7 +4563,7 @@ lemma createNewCaps_ko_wp_atQ':
apply (rename_tac apiobject_type)
apply (case_tac apiobject_type, simp_all split del: split_if)[1]
apply (rule hoare_pre, wp, simp)
apply (wp mapM_x_threadSet_createNewCaps_futz
by (wp mapM_x_threadSet_createNewCaps_futz
mapM_x_wp' createWordObjects_orig_ko_wp_at
createObjects_obj_at
createObjects_ko_wp_at2 createObjects_makeObject_not_tcbQueued
@ -4570,7 +4571,6 @@ lemma createNewCaps_ko_wp_atQ':
| simp add: makeObjectKO_def objBitsKO_def archObjSize_def APIType_capBits_def
objBits_def pageBits_def pdBits_def ptBits_def curDomain_def
| intro conjI | fastforce)+
done
lemmas createNewCaps_ko_wp_at'
= createNewCaps_ko_wp_atQ'[simplified, unfolded fold_K]
@ -5750,8 +5750,7 @@ proof -
createObjects_ct_idle_or_in_cur_domain'
| simp)+
apply clarsimp
apply (intro conjI)
apply (simp_all add:valid_pspace'_def objBits_def)
apply (intro conjI; simp add:valid_pspace'_def objBits_def)
apply (fastforce simp add: no_cte no_tcb split_def split: option.splits)
apply (clarsimp simp:invs'_def no_cte no_tcb valid_state'_def no_cte split:option.splits)
done

2
proof/refine/Schedule_R.thy
View File

@ -202,7 +202,7 @@ lemma st_tcb_at_coerce_abstract:
apply (clarsimp simp: st_tcb_at_def obj_at_def other_obj_relation_def
tcb_relation_def
split: Structures_A.kernel_object.split_asm
ARM_Structs_A.arch_kernel_obj.split_asm)
Arch_Structs_A.arch_kernel_obj.split_asm)
apply fastforce
done

44
proof/refine/StateRelation.thy
View File

@ -117,7 +117,7 @@ where
\<and> cs y = Some cap \<and> cap_relation cap (cteCap cte)"
definition
asid_pool_relation :: "(10 word \<rightharpoonup> word32) \<Rightarrow> ARMStructures_H.asidpool \<Rightarrow> bool"
asid_pool_relation :: "(10 word \<rightharpoonup> word32) \<Rightarrow> ArchStructures_H.asidpool \<Rightarrow> bool"
where
"asid_pool_relation \<equiv> \<lambda>p p'. p = inv ASIDPool p' o ucast"
@ -189,32 +189,32 @@ where
(TCB tcb, KOTCB tcb') \<Rightarrow> tcb_relation tcb tcb'
| (Endpoint ep, KOEndpoint ep') \<Rightarrow> ep_relation ep ep'
| (Notification ntfn, KONotification ntfn') \<Rightarrow> ntfn_relation ntfn ntfn'
| (ArchObj (ARM_Structs_A.ASIDPool pool), KOArch (KOASIDPool pool'))
| (ArchObj (Arch_Structs_A.ASIDPool pool), KOArch (KOASIDPool pool'))
\<Rightarrow> asid_pool_relation pool pool'
| _ \<Rightarrow> False)"
primrec
pde_relation' :: "ARM_Structs_A.pde \<Rightarrow> Hardware_H.pde \<Rightarrow> bool"
pde_relation' :: "Arch_Structs_A.pde \<Rightarrow> Hardware_H.pde \<Rightarrow> bool"
where
"pde_relation' ARM_Structs_A.InvalidPDE x = (x = Hardware_H.InvalidPDE)"
| "pde_relation' (ARM_Structs_A.PageTablePDE ptr atts domain) x
"pde_relation' Arch_Structs_A.InvalidPDE x = (x = Hardware_H.InvalidPDE)"
| "pde_relation' (Arch_Structs_A.PageTablePDE ptr atts domain) x
= (x = Hardware_H.PageTablePDE ptr (ParityEnabled \<in> atts) domain)"
| "pde_relation' (ARM_Structs_A.SectionPDE ptr atts domain rghts) x
| "pde_relation' (Arch_Structs_A.SectionPDE ptr atts domain rghts) x
= (x = Hardware_H.SectionPDE ptr (ParityEnabled \<in> atts) domain
(PageCacheable \<in> atts) (Global \<in> atts) (XNever \<in> atts) (vmrights_map rghts))"
| "pde_relation' (ARM_Structs_A.SuperSectionPDE ptr atts rghts) x
| "pde_relation' (Arch_Structs_A.SuperSectionPDE ptr atts rghts) x
= (x = Hardware_H.SuperSectionPDE ptr (ParityEnabled \<in> atts)
(PageCacheable \<in> atts) (Global \<in> atts) (XNever \<in> atts) (vmrights_map rghts))"
primrec
pte_relation' :: "ARM_Structs_A.pte \<Rightarrow> Hardware_H.pte \<Rightarrow> bool"
pte_relation' :: "Arch_Structs_A.pte \<Rightarrow> Hardware_H.pte \<Rightarrow> bool"
where
"pte_relation' ARM_Structs_A.InvalidPTE x = (x = Hardware_H.InvalidPTE)"
| "pte_relation' (ARM_Structs_A.LargePagePTE ptr atts rghts) x
"pte_relation' Arch_Structs_A.InvalidPTE x = (x = Hardware_H.InvalidPTE)"
| "pte_relation' (Arch_Structs_A.LargePagePTE ptr atts rghts) x
= (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
| "pte_relation' (Arch_Structs_A.SmallPagePTE ptr atts rghts) x
= (x = Hardware_H.SmallPagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts)
(XNever \<in> atts) (vmrights_map rghts))"
@ -226,7 +226,7 @@ where
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]
pde_align'_def[split_simps Arch_Structs_A.pde.split]
definition
pte_align' :: "Hardware_H.pte \<Rightarrow> nat"
@ -234,17 +234,17 @@ where
"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]
pte_align'_def[split_simps Arch_Structs_A.pte.split]
definition
"pde_relation_aligned y pde pde' \<equiv>
if is_aligned y (pde_align' pde') then pde_relation' pde pde'
else pde = ARM_Structs_A.InvalidPDE"
else pde = Arch_Structs_A.InvalidPDE"
definition
"pte_relation_aligned y pte pte' \<equiv>
if is_aligned y (pte_align' pte') then pte_relation' pte pte'
else pte = ARM_Structs_A.InvalidPTE"
else pte = Arch_Structs_A.InvalidPTE"
definition
"pte_relation y \<equiv> \<lambda>ko ko'. \<exists>pt pte. ko = ArchObj (PageTable pt) \<and> ko' = KOArch (KOPTE pte)
@ -256,10 +256,10 @@ definition
primrec
aobj_relation_cuts :: "ARM_Structs_A.arch_kernel_obj \<Rightarrow> word32 \<Rightarrow> obj_relation_cuts"
aobj_relation_cuts :: "Arch_Structs_A.arch_kernel_obj \<Rightarrow> word32 \<Rightarrow> obj_relation_cuts"
where
"aobj_relation_cuts (DataPage sz) x = {(x + n * 2 ^ pageBits, \<lambda>_. (op =) KOUserData) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }"
| "aobj_relation_cuts (ARM_Structs_A.ASIDPool pool) x =
| "aobj_relation_cuts (Arch_Structs_A.ASIDPool pool) x =
{(x, other_obj_relation)}"
| "aobj_relation_cuts (PageTable pt) x =
(\<lambda>y. (x + (ucast y << 2), pte_relation y)) ` UNIV"
@ -291,7 +291,7 @@ lemma obj_relation_cuts_def2:
| ArchObj (DataPage sz) \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_. (op =) KOUserData) | n . n < 2 ^ (pageBitsForSize sz - pageBits) }
| _ \<Rightarrow> {(x, other_obj_relation)})"
by (simp split: Structures_A.kernel_object.split
ARM_Structs_A.arch_kernel_obj.split)
Arch_Structs_A.arch_kernel_obj.split)
lemma obj_relation_cuts_def3:
"obj_relation_cuts ko x =
@ -306,7 +306,7 @@ lemma obj_relation_cuts_def3:
| _ \<Rightarrow> {(x, other_obj_relation)})"
apply (simp add: obj_relation_cuts_def2 a_type_def
split: Structures_A.kernel_object.split
ARM_Structs_A.arch_kernel_obj.split)
Arch_Structs_A.arch_kernel_obj.split)
apply (clarsimp simp: well_formed_cnode_n_def length_set_helper)
done
@ -458,7 +458,7 @@ lemma obj_relation_cutsE:
apply (simp add: obj_relation_cuts_def2 is_other_obj_relation_type_def
a_type_def
split: Structures_A.kernel_object.split_asm split_if_asm
ARM_Structs_A.arch_kernel_obj.split_asm)
Arch_Structs_A.arch_kernel_obj.split_asm)
apply (force simp: cte_relation_def pte_relation_def pde_relation_def)+
done
@ -650,9 +650,9 @@ lemma objBits_obj_bits:
by (simp add: other_obj_relation_def objBitsKO_simps pageBits_def
archObjSize_def
split: Structures_A.kernel_object.split_asm
ARM_Structs_A.arch_kernel_obj.split_asm
Arch_Structs_A.arch_kernel_obj.split_asm
Structures_H.kernel_object.split_asm
ARMStructures_H.arch_kernel_object.split_asm)
ArchStructures_H.arch_kernel_object.split_asm)
lemma replicate_length_cong:
"x = y \<Longrightarrow> replicate x n = replicate y n" by simp

14
proof/refine/Syscall_R.thy
View File

@ -594,12 +594,12 @@ lemma invokeTCB_typ_at'[wp]:
done
lemmas invokeTCB_typ_ats[wp] = typ_at_lifts [OF invokeTCB_typ_at']
term Interrupt_H.performIRQControl
crunch typ_at'[wp]: doReplyTransfer "\<lambda>s. P (typ_at' T p s)"
(wp: hoare_drop_imps)
lemmas doReplyTransfer_typ_ats[wp] = typ_at_lifts [OF doReplyTransfer_typ_at']
crunch typ_at'[wp]: invokeIRQControl "\<lambda>s. P (typ_at' T p s)"
lemmas invokeIRQControl_typ_ats[wp] = typ_at_lifts [OF invokeIRQControl_typ_at']
crunch typ_at'[wp]: "InterruptDecls_H.performIRQControl" "\<lambda>s. P (typ_at' T p s)"
lemmas invokeIRQControl_typ_ats[wp] = typ_at_lifts [OF InterruptDecls_H_performIRQControl_typ_at']
crunch typ_at'[wp]: invokeIRQHandler "\<lambda>s. P (typ_at' T p s)"
lemmas invokeIRQHandler_typ_ats[wp] = typ_at_lifts [OF invokeIRQHandler_typ_at']
@ -688,7 +688,7 @@ lemma diminished_ReplyCap' [simp]:
apply (rule iffI)
apply (clarsimp simp: diminished'_def maskCapRights_def Let_def split del: split_if)
apply (cases cap, simp_all add: isCap_simps)[1]
apply (simp add: ArchRetype_H.maskCapRights_def split: arch_capability.splits)
apply (simp add: ArchRetype_H.maskCapRights_def isPageCap_def split: arch_capability.splits)
apply (simp add: diminished'_def maskCapRights_def isCap_simps Let_def)
done
@ -2393,11 +2393,11 @@ proof -
qed
lemma inv_irq_IRQInactive:
"\<lbrace>\<top>\<rbrace> invokeIRQControl irqcontrol_invocation
"\<lbrace>\<top>\<rbrace> performIRQControl irqcontrol_invocation
-, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>"
apply (simp add: invokeIRQControl_def)
apply (simp add: performIRQControl_def)
apply (rule hoare_pre)
apply (wpc|wp|simp add: invokeInterruptControl_def)+
apply (wpc|wp|simp add: ArchInterrupt_H.performIRQControl_def)+
done
lemma inv_arch_IRQInactive:

16
proof/refine/TcbAcc_R.thy
View File

@ -356,7 +356,7 @@ lemma pspace_relation_tcb_at:
apply (erule(1) obj_relation_cutsE, simp_all)
apply (clarsimp simp: other_obj_relation_def
split: Structures_A.kernel_object.split_asm
ARM_Structs_A.arch_kernel_obj.split_asm)
Arch_Structs_A.arch_kernel_obj.split_asm)
apply (simp add: is_tcb obj_at_def)
done
@ -1342,8 +1342,7 @@ proof -
|clarsimp simp: y z a domains|rule refl)+
apply (clarsimp simp: obj_at'_def projectKOs pred_tcb_at'_def)
apply (clarsimp simp: cur_tcb'_def valid_irq_node'_def valid_queues'_def)
apply (fastforce simp: domains ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def z a)
done
by (fastforce simp: domains ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def z a)
qed
lemmas threadSet_invs_trivial =
@ -2159,7 +2158,7 @@ lemma tcbSchedDequeue_corres:
apply (clarsimp simp: in_monad ethread_get_def set_tcb_queue_def is_etcb_at_def state_relation_def)
apply (subgoal_tac "t \<notin> set (ready_queues a (tcb_domain y) (tcb_priority y))")
prefer 2
apply (force simp: tcb_sched_dequeue_def Invariants_H.valid_queues_def valid_queues_no_bitmap_def
subgoal by (force simp: tcb_sched_dequeue_def Invariants_H.valid_queues_def valid_queues_no_bitmap_def
ready_queues_relation_def obj_at'_def inQ_def projectKO_eq project_inject)
apply (subst gets_the_exec)
apply (simp add: get_etcb_def)
@ -3627,7 +3626,7 @@ lemma store_word_corres:
lemmas msgRegisters_unfold
= State_H.msgRegisters_def
msg_registers_def
ARMMachineTypes.msgRegisters_def
MachineTypes.msgRegisters_def
[unfolded upto_enum_def, simplified,
unfolded fromEnum_def enum_register, simplified,
unfolded toEnum_def enum_register, simplified]
@ -4757,9 +4756,8 @@ lemma sts_invs_minor':
apply (drule obj_at_valid_objs')
apply (clarsimp simp: valid_pspace'_def)
apply (clarsimp simp: valid_obj'_def valid_tcb'_def projectKOs)
apply (fastforce simp: valid_tcb_state'_def
by (fastforce simp: valid_tcb_state'_def
split: Structures_H.thread_state.splits)
done
lemma sbn_invs_minor':
"\<lbrace>bound_tcb_at' (\<lambda>ntfn'. tcb_bound_refs' ntfn' = tcb_bound_refs' ntfn) t
@ -5050,7 +5048,7 @@ lemma set_eobject_corres':
apply (clarsimp simp: non_exst_same_def)
apply (case_tac bb; simp)
apply (clarsimp simp: obj_at'_def other_obj_relation_def cte_relation_def tcb_relation_def projectKOs split: split_if_asm)+
apply (clarsimp simp: aobj_relation_cuts_def split: ARM_Structs_A.arch_kernel_obj.splits)
apply (clarsimp simp: aobj_relation_cuts_def split: Arch_Structs_A.arch_kernel_obj.splits)
apply (rename_tac arch_kernel_obj obj d p ts)
apply (case_tac arch_kernel_obj; simp)
apply (clarsimp simp: pte_relation_def pde_relation_def is_tcb_def)+
@ -5061,7 +5059,7 @@ lemma set_eobject_corres':
apply (clarsimp simp: obj_at'_def)
apply (clarsimp simp: projectKOs)
apply (insert e)
apply (clarsimp simp: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits ARM_Structs_A.arch_kernel_obj.splits)
apply (clarsimp simp: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits Arch_Structs_A.arch_kernel_obj.splits)
done
lemma set_eobject_corres:

2
proof/refine/Tcb_R.thy
View File

@ -1414,7 +1414,7 @@ lemma setSchedulerAction_invs'[wp]:
done
consts
copyregsets_map :: "arm_copy_register_sets \<Rightarrow> copy_register_sets"
copyregsets_map :: "arch_copy_register_sets \<Rightarrow> copy_register_sets"
primrec
tcbinv_relation :: "tcb_invocation \<Rightarrow> tcbinvocation \<Rightarrow> bool"

5
proof/refine/Untyped_R.thy
View File

@ -1599,8 +1599,7 @@ shows
apply(clarsimp)
apply(simp)
apply(clarsimp)
apply(drule cte_map_inj_eq)
apply(simp_all add: cte_wp_at_caps_of_state)[6]
apply(drule cte_map_inj_eq; simp add: cte_wp_at_caps_of_state)
apply(clarsimp)
apply(case_tac z)
apply(clarsimp simp: state_relation_def cdt_list_relation_def)
@ -3046,7 +3045,7 @@ lemma inv_untyped_corres_helper1:
apply (rule conjI)
apply clarsimp
apply (rule conjI)
apply fastforce
subgoal by fastforce
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps valid_cap_def)
apply (fastforce simp: image_def)
apply (rule hoare_pre)

43
proof/refine/VSpace_R.thy
View File

@ -1503,22 +1503,22 @@ lemma check_mapping_corres:
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ get_pte_corres'])
apply (rule corres_trivial)
apply (cases sz,
subgoal by (cases sz,
auto simp add: is_aligned_mask[symmetric]
is_aligned_shiftr pg_entry_align_def
unlessE_def returnOk_def pte_relation_aligned_def
split: ARM_Structs_A.pte.split if_splits Hardware_H.pte.split )[1]
split: Arch_Structs_A.pte.split if_splits Hardware_H.pte.split )
apply wp
apply simp
apply (simp add:is_aligned_mask[symmetric] is_aligned_shiftr pg_entry_align_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ get_pde_corres'])
apply (rule corres_trivial)
apply (cases sz,
subgoal by (cases sz,
auto simp add: is_aligned_mask[symmetric]
is_aligned_shiftr pg_entry_align_def
unlessE_def returnOk_def pde_relation_aligned_def
split: ARM_Structs_A.pde.split if_splits Hardware_H.pde.split )[1]
split: Arch_Structs_A.pde.split if_splits Hardware_H.pde.split )
apply wp
apply simp+
done
@ -1926,7 +1926,7 @@ lemma corres_store_pde_with_invalid_tail:
"\<forall>slot \<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab)
\<Longrightarrow>corres dc ((\<lambda>s. \<forall>y\<in> set ys. pde_at y s) and pspace_aligned and valid_etcbs)
(pspace_aligned' and pspace_distinct')
(mapM (swp store_pde ARM_Structs_A.pde.InvalidPDE) ys)
(mapM (swp store_pde Arch_Structs_A.pde.InvalidPDE) ys)
(mapM (swp storePDE ab) ys)"
apply (rule_tac S ="{(x,y). x = y \<and> x \<in> set ys}"
in corres_mapM[where r = dc and r' = dc])
@ -1949,7 +1949,7 @@ lemma corres_store_pte_with_invalid_tail:
"\<forall>slot\<in> set ys. \<not> is_aligned (slot >> 2) (pte_align' aa)
\<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs)
(pspace_aligned' and pspace_distinct')
(mapM (swp store_pte ARM_Structs_A.pte.InvalidPTE) ys)
(mapM (swp store_pte Arch_Structs_A.pte.InvalidPTE) ys)
(mapM (swp storePTE aa) ys)"
apply (rule_tac S ="{(x,y). x = y \<and> x \<in> set ys}"
in corres_mapM[where r = dc and r' = dc])
@ -2189,7 +2189,7 @@ proof -
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. pd_at_asid word pd s)" in hoare_strengthen_post)
prefer 2
apply auto[1]
apply (wp mapM_swp_store_pte_invs[where pte="ARM_Structs_A.pte.InvalidPTE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_swp_store_pte_invs[where pte="Arch_Structs_A.pte.InvalidPTE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_UNIV_wp | simp add: swp_def del: fun_upd_apply)+
apply (clarsimp simp:pte_relation_aligned_def)
apply (clarsimp dest!:valid_slots_duplicated_pteD')
@ -2230,7 +2230,7 @@ proof -
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. pd_at_asid word pd s)" in hoare_strengthen_post)
prefer 2
apply auto[1]
apply (wp mapM_swp_store_pde_invs_unmap[where pde="ARM_Structs_A.pde.InvalidPDE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_swp_store_pde_invs_unmap[where pde="Arch_Structs_A.pde.InvalidPDE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_UNIV_wp store_pde_pd_at_asid | clarsimp simp add: swp_def del: fun_upd_apply)+
apply (clarsimp simp: pde_relation_aligned_def)
apply (clarsimp dest!:valid_slots_duplicated_pdeD')
@ -2256,7 +2256,7 @@ proof -
apply (clarsimp simp: cap_range_def)
apply (rule conjI)
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
apply (clarsimp split: Structures_A.kernel_object.split_asm split_if_asm ARM_Structs_A.arch_kernel_obj.splits)
apply (clarsimp split: Structures_A.kernel_object.split_asm split_if_asm Arch_Structs_A.arch_kernel_obj.splits)
apply (rule conjI[rotated], fastforce)
apply (erule ballEI)
apply (clarsimp simp: pde_at_def obj_at_def
@ -2300,7 +2300,7 @@ proof -
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. pd_at_asid word pd s)" in hoare_strengthen_post)
prefer 2
apply auto[1]
apply (wp mapM_swp_store_pte_invs[where pte="ARM_Structs_A.pte.InvalidPTE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_swp_store_pte_invs[where pte="Arch_Structs_A.pte.InvalidPTE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_UNIV_wp | simp add: swp_def del: fun_upd_apply)+
apply (clarsimp simp:pte_relation_aligned_def valid_page_inv'_def)
apply (clarsimp dest!:valid_slots_duplicated_pteD')
@ -2341,7 +2341,7 @@ proof -
apply (rule_tac Q="\<lambda>_. K (word \<le> mask asid_bits \<and> word \<noteq> 0) and invs and (\<lambda>s. \<exists>pd. pd_at_asid word pd s)" in hoare_strengthen_post)
prefer 2
apply auto[1]
apply (wp mapM_swp_store_pde_invs_unmap[where pde="ARM_Structs_A.pde.InvalidPDE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_swp_store_pde_invs_unmap[where pde="Arch_Structs_A.pde.InvalidPDE", simplified] hoare_vcg_ex_lift)
apply (wp mapM_UNIV_wp store_pde_pd_at_asid | clarsimp simp add: swp_def del: fun_upd_apply)+
apply (clarsimp simp: pde_relation_aligned_def valid_page_inv'_def)
apply (clarsimp dest!:valid_slots_duplicated_pdeD')
@ -2366,13 +2366,15 @@ proof -
apply (clarsimp simp: valid_caps_def)
apply (drule spec, drule spec, drule_tac x=capa in spec, drule (1) mp)
apply (case_tac aa, simp_all)
apply ((clarsimp simp: valid_cap_def obj_at_def a_type_def is_ep_def
apply fold_subgoals[2]
subgoal
by ((clarsimp simp: valid_cap_def obj_at_def a_type_def is_ep_def
is_ntfn_def is_cap_table_def is_tcb_def
is_pg_cap_def
split: cap.splits Structures_A.kernel_object.splits
split_if_asm
ARM_Structs_A.arch_kernel_obj.splits option.splits
arch_cap.splits)+)[2]
Arch_Structs_A.arch_kernel_obj.splits option.splits
arch_cap.splits)+)
apply (clarsimp simp: pde_at_def obj_at_def a_type_def)
apply (case_tac ko, simp_all split: split_if_asm)[1]
apply (rename_tac arch_kernel_obj)
@ -2497,7 +2499,7 @@ definition
lemma clear_page_table_corres:
"corres dc (pspace_aligned and page_table_at p and valid_etcbs)
(pspace_aligned' and pspace_distinct')
(mapM_x (swp store_pte ARM_Structs_A.InvalidPTE)
(mapM_x (swp store_pte Arch_Structs_A.InvalidPTE)
[p , p + 4 .e. p + 2 ^ ptBits - 1])
(mapM_x (swp storePTE Hardware_H.InvalidPTE)
[p , p + 4 .e. p + 2 ^ ptBits - 1])"
@ -2522,7 +2524,7 @@ lemma clear_page_table_corres:
apply (simp add: list_all2_refl)
apply (clarsimp simp: upto_enum_step_def)
apply (erule page_table_pte_atI[simplified shiftl_t2n mult.commute, simplified])
apply (simp add: ptBits_def pageBits_def pt_bits_def word_less_nat_alt unat_of_nat)
apply (simp add: ptBits_def pageBits_def pt_bits_def word_less_nat_alt word_le_nat_alt unat_of_nat)
apply simp
done
@ -2625,7 +2627,7 @@ lemma pap_corres:
apply (rename_tac word1 word2 prod)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ getSlotCap_corres])
apply (rule_tac F="\<exists>p asid. rv = Structures_A.ArchObjectCap (ARM_Structs_A.PageDirectoryCap p asid)" in corres_gen_asm)
apply (rule_tac F="\<exists>p asid. rv = Structures_A.ArchObjectCap (Arch_Structs_A.PageDirectoryCap p asid)" in corres_gen_asm)
apply clarsimp
apply (rule_tac Q="valid_objs and pspace_aligned and pspace_distinct and asid_pool_at word2 and valid_etcbs and
cte_wp_at (\<lambda>c. cap_master_cap c =
@ -3751,15 +3753,14 @@ lemma isPDCap_PD :
"isPDCap (ArchObjectCap (PageDirectoryCap r m))"
by (simp add: isPDCap_def)
lemma diminished_valid':
"diminished' cap cap' \<Longrightarrow> valid_cap' cap = valid_cap' cap'"
apply (clarsimp simp add: diminished'_def)
apply (rule ext)
apply (simp add: maskCapRights_def Let_def split del: split_if)
apply (cases cap')
apply (simp_all add: isCap_simps valid_cap'_def capAligned_def split del: split_if)
apply (simp add: ArchRetype_H.maskCapRights_def Let_def split del: split_if split: arch_capability.splits)
done
apply (cases cap'; simp add: isCap_simps valid_cap'_def capAligned_def split del: split_if)
by (simp add: ArchRetype_H.maskCapRights_def isPageCap_def Let_def split del: split_if split: arch_capability.splits)
lemma diminished_isPDCap:
"diminished' cap cap' \<Longrightarrow> isPDCap cap' = isPDCap cap"