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

arch_split: checkpoint. Checks up to ArchVSpace_AI with two sorries (MattB WIP)

This commit is contained in:
Daniel Matichuk 2016-04-06 14:25:52 +10:00
parent 69d7b50dae
commit ab09d49b59
20 changed files with 5691 additions and 5326 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

84
proof/invariant-abstract/ARM/ArchAcc_AI.thy
View File

@ -56,7 +56,7 @@ lemma set_asid_pool_typ_at:
apply (simp add: set_asid_pool_def set_object_def get_object_def)
apply wp
including unfold_objects
by clarsimp (simp add: a_type_def aa_type_def)
by clarsimp (simp add: a_type_def)
lemmas set_asid_pool_typ_ats [wp] = abs_typ_at_lifts [OF set_asid_pool_typ_at]
@ -104,7 +104,7 @@ lemma store_pde_typ_at [wp]:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> store_pde ptr pde \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>"
apply (simp add: store_pde_def set_pd_def set_object_def get_object_def)
apply wp
apply (clarsimp simp: obj_at_def a_type_def aa_type_def)
apply (clarsimp simp: obj_at_def a_type_def)
done
@ -149,7 +149,7 @@ lemma store_pte_typ_at:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> store_pte ptr pte \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>"
apply (simp add: store_pte_def set_pt_def set_object_def get_object_def)
apply wp
apply (clarsimp simp: obj_at_def a_type_def aa_type_def)
apply (clarsimp simp: obj_at_def a_type_def)
done
@ -338,7 +338,7 @@ lemma set_pd_aligned [wp]:
apply (simp add: set_pd_def)
apply (wp set_object_aligned get_object_wp)
including unfold_objects_asm
by (clarsimp simp: a_type_def aa_type_def)
by (clarsimp simp: a_type_def)
crunch aligned [wp]: store_pde pspace_aligned
@ -355,7 +355,7 @@ lemma arch_derive_cap_valid_cap:
apply(simp add: arch_derive_cap_def)
apply(cases arch_cap, simp_all add: arch_derive_cap_def o_def)
apply(rule hoare_pre, wpc?, wp,
clarsimp simp add: cap_aligned_def valid_cap_def valid_arch_cap_def split: option.splits)+
clarsimp simp add: cap_aligned_def valid_cap_def split: option.splits)+
done
@ -416,7 +416,7 @@ lemma mask_asid_low_bits_ucast_ucast:
apply (simp add: word_size nth_ucast asid_low_bits_def)
done
crunch ct[wp]: set_thread_state "\<lambda>s. P (cur_thread s)"
lemma set_asid_pool_cur [wp]:
"\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> set_asid_pool p a \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>"
@ -443,7 +443,7 @@ lemma set_asid_pool_valid_objs [wp]:
apply (simp add: set_asid_pool_def)
apply (wp set_object_valid_objs get_object_wp)
including unfold_objects
by (clarsimp simp: a_type_def aa_type_def valid_obj_def wellformed_arch_obj_def)
by (clarsimp simp: a_type_def valid_obj_def wellformed_arch_obj_def)
lemma pde_at_aligned_vptr:
"\<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; page_directory_at pd s;
@ -452,7 +452,7 @@ lemma pde_at_aligned_vptr:
apply (clarsimp simp: lookup_pd_slot_def Let_def
obj_at_def pde_at_def)
apply (drule(1) pspace_alignedD[rotated])
apply (clarsimp simp: a_type_def aa_type_def
apply (clarsimp simp: a_type_def
split: kernel_object.split_asm
arch_kernel_obj.split_asm split_if_asm
cong: kernel_object.case_cong)
@ -601,7 +601,7 @@ lemma kernel_mapping_slots_empty_pdeI:
apply (clarsimp simp: invs_def valid_state_def equal_kernel_mappings_def valid_global_objs_def)
apply (erule_tac x=p in allE, erule_tac x="arm_global_pd (arch_state s)" in allE)
including unfold_objects
by (clarsimp simp: empty_table_def valid_arch_state_def a_type_def aa_type_def)
by (clarsimp simp: empty_table_def valid_arch_state_def a_type_def)
lemma invs_valid_global_pts:
@ -824,7 +824,7 @@ lemma set_pt_distinct [wp]:
"\<lbrace>pspace_distinct\<rbrace> set_pt p pt \<lbrace>\<lambda>_. pspace_distinct\<rbrace>"
apply (simp add: set_pt_def)
apply (wp set_object_distinct get_object_wp)
apply (clarsimp simp: obj_at_def a_type_def aa_type_def
apply (clarsimp simp: obj_at_def a_type_def
split: kernel_object.splits arch_kernel_obj.splits)
done
@ -833,7 +833,7 @@ lemma set_pd_distinct [wp]:
"\<lbrace>pspace_distinct\<rbrace> set_pd p pd \<lbrace>\<lambda>_. pspace_distinct\<rbrace>"
apply (simp add: set_pd_def)
apply (wp set_object_distinct get_object_wp)
apply (clarsimp simp: obj_at_def a_type_def aa_type_def
apply (clarsimp simp: obj_at_def a_type_def
split: kernel_object.splits arch_kernel_obj.splits)
done
@ -854,7 +854,7 @@ lemma store_pte_valid_objs [wp]:
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def wellformed_arch_obj_def)
apply assumption
by (simp add: a_type_def aa_type_def)
by (simp add: a_type_def)
done
@ -889,7 +889,7 @@ lemma store_pte_aligned [wp]:
apply (simp add: store_pte_def set_pt_def)
apply (wp set_object_aligned get_object_wp)
including unfold_objects
by (clarsimp simp: a_type_def aa_type_def)
by (clarsimp simp: a_type_def)
lemma store_pde_valid_objs [wp]:
@ -908,7 +908,7 @@ lemma store_pde_valid_objs [wp]:
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def wellformed_arch_obj_def)
apply assumption
by (simp add: a_type_def aa_type_def)
by (simp add: a_type_def)
done
@ -917,14 +917,14 @@ lemma set_asid_pool_aligned [wp]:
apply (simp add: set_asid_pool_def get_object_def)
apply (wp set_object_aligned|wpc)+
including unfold_objects
by (auto simp: a_type_def aa_type_def)
by (auto simp: a_type_def)
lemma set_asid_pool_distinct [wp]:
"\<lbrace>pspace_distinct\<rbrace> set_asid_pool p ptr \<lbrace>\<lambda>_. pspace_distinct\<rbrace>"
apply (simp add: set_asid_pool_def get_object_def)
apply (wp set_object_distinct|wpc)+
including unfold_objects
by (auto simp: a_type_def aa_type_def)
by (auto simp: a_type_def)
lemma store_pde_arch [wp]:
@ -952,7 +952,7 @@ lemma set_pd_typ_at [wp]:
apply clarsimp
apply (erule rsubst [where P=P])
including unfold_objects
by (clarsimp simp: a_type_def aa_type_def)
by (clarsimp simp: a_type_def)
lemma set_pd_valid_objs:
@ -962,7 +962,7 @@ lemma set_pd_valid_objs:
apply (simp add: set_pd_def)
apply (wp get_object_wp set_object_valid_objs)
including unfold_objects
by (clarsimp simp: valid_obj_def wellformed_arch_obj_def a_type_def aa_type_def)
by (clarsimp simp: valid_obj_def wellformed_arch_obj_def a_type_def)
lemma set_pd_iflive:
@ -1113,7 +1113,7 @@ lemma set_pd_arch_objs_unmap:
apply (simp add: set_pd_def)
apply (wp set_object_arch_objs get_object_wp)
including unfold_objects
by (fastforce simp: a_type_def aa_type_def)
by (fastforce simp: a_type_def)
declare graph_of_None_update[simp]
@ -1127,7 +1127,7 @@ lemma set_pt_typ_at [wp]:
apply clarsimp
apply (erule rsubst [where P=P])
including unfold_objects
by (clarsimp simp: a_type_def aa_type_def)
by (clarsimp simp: a_type_def)
lemma set_pt_valid_objs:
@ -1139,7 +1139,7 @@ lemma set_pt_valid_objs:
apply (clarsimp split: kernel_object.splits
arch_kernel_obj.splits)
apply (clarsimp simp: valid_obj_def obj_at_def a_type_def
aa_type_def wellformed_arch_obj_def)
wellformed_arch_obj_def)
done
@ -1282,7 +1282,7 @@ lemma set_pt_aligned [wp]:
"\<lbrace>pspace_aligned\<rbrace> set_pt p pt \<lbrace>\<lambda>_. pspace_aligned\<rbrace>"
apply (simp add: set_pt_def)
apply (wp get_object_wp set_object_aligned)
apply (clarsimp simp: a_type_def aa_type_def obj_at_def
apply (clarsimp simp: a_type_def obj_at_def
split: kernel_object.splits arch_kernel_obj.splits)
done
@ -1299,7 +1299,7 @@ lemma set_pt_arch_objs [wp]:
apply (wp set_object_arch_objs get_object_wp)
apply (clarsimp simp: obj_at_def)
apply (rule conjI)
apply (clarsimp simp: a_type_def aa_type_def
apply (clarsimp simp: a_type_def
split: kernel_object.splits arch_kernel_obj.splits)
apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits)
apply (simp add: vs_refs_def)
@ -1394,7 +1394,7 @@ lemma set_pt_table_caps [wp]:
apply ((drule spec)+, erule impE, assumption)
apply (rename_tac arch_cap)
apply (case_tac arch_cap,
simp_all add: valid_cap_def valid_arch_cap_def obj_at_def aa_type_simps)
simp_all add: valid_cap_def obj_at_def aa_type_simps)
apply clarsimp
apply (erule impE, fastforce simp: cap_asid_def split: option.splits)
apply (erule disjE, simp add: empty_table_def)
@ -1464,7 +1464,7 @@ lemma set_pt_valid_arch_objs[wp]:
apply clarsimp
apply (drule bspec,fastforce)
subgoal for "fun" x
by (cases "fun x"; clarsimp simp: obj_at_def a_type_simps aa_type_simps)
by (cases "fun x"; clarsimp simp: obj_at_def a_type_simps)
done
done
@ -1631,7 +1631,7 @@ lemma set_pt_kernel_window[wp]:
"\<lbrace>pspace_in_kernel_window\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>"
apply (simp add: set_pt_def)
apply (wp set_object_pspace_in_kernel_window get_object_wp)
apply (clarsimp simp: obj_at_def a_type_def aa_type_def
apply (clarsimp simp: obj_at_def a_type_def
split: kernel_object.split_asm
arch_kernel_obj.split_asm)
done
@ -1651,7 +1651,7 @@ lemma set_pt_valid_ioc[wp]:
"\<lbrace>valid_ioc\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_ioc\<rbrace>"
apply (simp add: set_pt_def)
apply (wp set_object_valid_ioc_no_caps get_object_wp)
by (clarsimp simp: a_type_simps aa_type_simps obj_at_def is_tcb is_cap_table
by (clarsimp simp: a_type_simps obj_at_def is_tcb is_cap_table
split: kernel_object.splits arch_kernel_obj.splits)
@ -1794,7 +1794,7 @@ lemma store_pte_invs [wp]:
apply (intro impI conjI allI)
apply (drule (2) vs_lookup_pages_pt_eq[OF invs_arch_objs invs_ran_asid_table,
THEN iffD1, rotated -1])
apply (clarsimp simp: obj_at_def a_type_simps aa_type_simps)
apply (clarsimp simp: obj_at_def a_type_simps)
apply (drule spec, erule impE, assumption)+
apply (erule exEI)+
apply clarsimp
@ -1957,7 +1957,7 @@ lemma set_asid_pool_arch_objs_unmap':
apply (wp get_object_wp set_object_arch_objs)
apply (clarsimp simp: obj_at_def obj_at_def)
apply (rule conjI)
apply (clarsimp simp: a_type_def aa_type_def split: kernel_object.splits arch_kernel_obj.splits)
apply (clarsimp simp: a_type_def split: kernel_object.splits arch_kernel_obj.splits)
apply (clarsimp simp: vs_refs_def)
apply fastforce
done
@ -2044,12 +2044,12 @@ lemma set_asid_pool_global_objs [wp]:
apply (rule conjI)
apply (clarsimp simp: obj_at_def)
apply (rule conjI)
subgoal by (clarsimp simp: valid_arch_state_def obj_at_def a_type_def aa_type_def)
subgoal by (clarsimp simp: valid_arch_state_def obj_at_def a_type_def)
apply clarsimp
apply (erule (1) valid_arch_obj_same_type)
subgoal by (simp add: a_type_def aa_type_def)
subgoal by (simp add: a_type_def)
apply (rule conjI)
subgoal by (clarsimp simp: obj_at_def valid_arch_state_def a_type_def aa_type_def)
subgoal by (clarsimp simp: obj_at_def valid_arch_state_def a_type_def)
apply (clarsimp simp: obj_at_def)
apply (drule (1) bspec)
by clarsimp
@ -2137,7 +2137,7 @@ lemma set_asid_pool_valid_global_pd_mappings[wp]:
apply (simp add: set_asid_pool_def)
apply (wp set_object_global_pd_mappings get_object_wp)
including unfold_objects
by (clarsimp simp: a_type_def aa_type_def)
by (clarsimp simp: a_type_def)
lemma set_asid_pool_kernel_window[wp]:
@ -2145,7 +2145,7 @@ lemma set_asid_pool_kernel_window[wp]:
apply (simp add: set_asid_pool_def)
apply (wp set_object_pspace_in_kernel_window get_object_wp)
including unfold_objects_asm
by (clarsimp simp: a_type_def aa_type_def)
by (clarsimp simp: a_type_def)
lemma set_asid_pool_caps_kernel_window[wp]:
@ -2163,7 +2163,7 @@ lemma set_asid_pool_valid_ioc[wp]:
including unfold_objects
by (clarsimp simp: valid_def get_object_def simpler_gets_def assert_def
return_def fail_def bind_def
a_type_simps aa_type_simps is_tcb is_cap_table)
a_type_simps is_tcb is_cap_table)
lemma set_asid_pool_vms[wp]:
@ -2771,7 +2771,7 @@ lemma create_mapping_entries_valid_slots [wp]:
apply (rule shiftl_less_t2n)
apply (rule word_less_sub_le[THEN iffD1], simp+)
apply (erule lookup_pd_slot_eq[simplified pd_bits])
apply (simp add: a_type_simps aa_type_simps)
apply (simp add: a_type_simps)
apply (subst add.commute)
apply (fastforce intro!: aligned_add_aligned is_aligned_shiftl_self)
done
@ -2826,7 +2826,7 @@ lemma store_pde_lookup_pd:
apply (frule (1) valid_asid_tableD)
apply (frule vs_lookup_atI)
apply (frule (2) stronger_arch_objsD)
apply (clarsimp simp: obj_at_def a_type_def aa_type_def)
apply (clarsimp simp: obj_at_def a_type_def)
apply (case_tac ao, simp_all, clarsimp)
apply (drule tranclD)
apply clarsimp
@ -3102,7 +3102,7 @@ lemma set_pd_table_caps [wp]:
apply (clarsimp simp: is_arch_cap_simps)
apply (simp add: valid_caps_def)
apply (erule_tac x=a in allE, erule allE, erule allE, erule (1) impE)
apply (clarsimp simp: is_arch_cap_simps valid_cap_def valid_arch_cap_def)
apply (clarsimp simp: is_arch_cap_simps valid_cap_def)
apply (clarsimp simp: obj_at_def)
done
@ -3129,12 +3129,12 @@ lemma set_pd_global_objs[wp]:
apply (erule disjE)
apply (drule(1) empty_table_is_valid)+
apply (rule valid_arch_obj_same_type, simp+)
apply (clarsimp simp: a_type_def aa_type_def)
apply (clarsimp simp: a_type_def)
apply clarsimp
apply (drule (1) valid_global_refsD2)
apply (simp add: cap_range_def global_refs_def)
apply (rule valid_arch_obj_same_type, simp+)
apply (simp add: a_type_def aa_type_def)
apply (simp add: a_type_def)
apply (clarsimp simp: obj_at_def)
apply (drule (1) valid_global_refsD2)
apply (simp add: cap_range_def global_refs_def)
@ -3276,7 +3276,7 @@ lemma set_pd_kernel_window[wp]:
"\<lbrace>pspace_in_kernel_window\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>"
apply (simp add: set_pd_def)
apply (wp set_object_pspace_in_kernel_window get_object_wp)
apply (clarsimp simp: obj_at_def a_type_def aa_type_def
apply (clarsimp simp: obj_at_def a_type_def
split: kernel_object.split_asm
arch_kernel_obj.split_asm)
done
@ -3298,7 +3298,7 @@ lemma set_pd_valid_ioc[wp]:
apply (wp set_object_valid_ioc_no_caps get_object_inv)
by (clarsimp simp: valid_def get_object_def simpler_gets_def assert_def
return_def fail_def bind_def
a_type_simps aa_type_simps obj_at_def is_tcb is_cap_table
a_type_simps obj_at_def is_tcb is_cap_table
split: kernel_object.splits arch_kernel_obj.splits)

64
proof/invariant-abstract/ARM/ArchCSpaceInv_AI.thy
View File

@ -72,18 +72,15 @@ lemma pageBitsForSize_simps[simp]:
by (simp add: pageBitsForSize_def)+
definition
"is_ap_cap cap \<equiv> case cap of (arch_cap.ASIDPoolCap ap asid) \<Rightarrow> True | _ \<Rightarrow> False"
"is_ap_cap cap \<equiv> case cap of (ArchObjectCap (arch_cap.ASIDPoolCap ap asid)) \<Rightarrow> True | _ \<Rightarrow> False"
lemmas is_ap_cap_simps [simp] = is_ap_cap_def [split_simps arch_cap.split]
lemmas is_ap_cap_simps [simp] = is_ap_cap_def [split_simps cap.split arch_cap.split]
definition
"reachable_pg_cap cap \<equiv> \<lambda>s.
is_pg_cap cap \<and>
(\<exists>vref. vs_cap_ref cap = Some vref \<and> (vref \<unrhd> obj_ref_of cap) s)"
lemma empty_table_caps_of:
"empty_table S ko \<Longrightarrow> caps_of ko = {}"
by (cases ko, simp_all add: empty_table_def caps_of_def cap_of_def)
(*FIXME arch_split: These are probably subsumed by the lifting lemmas *)
@ -138,10 +135,7 @@ lemma vs_lookup_tcb_update:
by (clarsimp simp add: vs_lookup_def vs_lookup1_tcb_update)
lemma only_idle_tcb_update:
"\<lbrakk>only_idle s; ko_at (TCB t) p s; tcb_state t = tcb_state t' \<or> \<not>idle (tcb_state t') \<rbrakk>
\<Longrightarrow> only_idle (s\<lparr>kheap := kheap s(p \<mapsto> TCB t')\<rparr>)"
by (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def)
lemma tcb_update_global_pd_mappings:
@ -303,6 +297,7 @@ lemma not_arch_not_reachable_pg[simp]:
unfolding is_arch_cap_def reachable_pg_cap_def is_pg_cap_def
by (auto split: cap.splits arch_cap.splits)
(*
lemma set_cap_valid_arch_caps:
"\<lbrace>\<lambda>s. valid_arch_caps s
\<and> (if (\<not>is_arch_cap cap) \<and> (\<forall>cap'. cte_wp_at (op = cap') ptr s \<longrightarrow> \<not>is_arch_cap cap') then
@ -310,7 +305,7 @@ lemma set_cap_valid_arch_caps:
else set_arch_cap_precondition cap ptr s) \<rbrace>
set_cap cap ptr
\<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>"
(*
apply (simp add: valid_arch_caps_def pred_conj_def split del: split_if)
apply (wp set_cap_valid_vs_lookup set_cap_valid_table_caps
set_cap_unique_table_caps set_cap_unique_table_refs)
@ -328,12 +323,30 @@ lemma set_cap_valid_arch_caps:
apply clarsimp
apply (simp add: cte_wp_at_caps_of_state)
apply (case_tac "caps_of_state s ptr"; simp)
find_theorems no_cap_to_obj_with_diff_ref
apply (simp ; blast)
find_consts name:"is_arch_cap"
find_theorems valid_arch_caps
(*
done*) sorry*)
lemma set_cap_valid_arch_caps:
"\<lbrace>\<lambda>s. valid_arch_caps s
\<and> (\<forall>vref cap'. cte_wp_at (op = cap') ptr s
\<longrightarrow> vs_cap_ref cap' = Some vref
\<longrightarrow> (vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap')
\<or> (\<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s)
\<or> (\<forall>oref \<in> obj_refs cap'. \<not> (vref \<unrhd> oref) s))
\<and> no_cap_to_obj_with_diff_ref cap {ptr} s
\<and> ((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow> cap_asid cap = None
\<longrightarrow> (\<forall>r \<in> obj_refs cap. obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s))
\<and> ((is_pt_cap cap \<or> is_pd_cap cap)
\<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow>
(is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap)
\<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None)
\<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)
\<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap
\<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap')
\<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr))\<rbrace>
set_cap cap ptr
\<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>"
sorry
lemma valid_table_capsD:
"\<lbrakk> cte_wp_at (op = cap) ptr s; valid_table_caps s;
is_pt_cap cap | is_pd_cap cap; cap_asid cap = None \<rbrakk>
@ -373,5 +386,24 @@ lemma cap_refs_in_kernel_windowD:
apply (cases ptr, fastforce)
done
lemma valid_cap_imp_valid_vm_rights:
"valid_cap (cap.ArchObjectCap (PageCap mw rs sz m)) s \<Longrightarrow>
rs \<in> valid_vm_rights"
by (simp add: valid_cap_def valid_vm_rights_def)
lemma acap_rights_update_idem [simp]:
"acap_rights_update R (acap_rights_update R' cap) = acap_rights_update R cap"
by (simp add: acap_rights_update_def split: arch_cap.splits)
lemma cap_master_arch_cap_rights [simp]:
"cap_master_arch_cap (acap_rights_update R cap) = cap_master_arch_cap cap"
by (simp add: cap_master_arch_cap_def acap_rights_update_def
split: arch_cap.splits)
lemma acap_rights_update_id [intro!, simp]:
"valid_arch_cap ac s \<Longrightarrow> acap_rights_update (acap_rights ac) ac = ac"
unfolding acap_rights_update_def acap_rights_def valid_arch_cap_def
by (cases ac; simp)
end
end

262
proof/invariant-abstract/ARM/ArchCSpace_AI.thy Normal file
View File

@ -0,0 +1,262 @@
(*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*)
(*
ARM-specific CSpace invariants
*)
theory ArchCSpace_AI
imports "../CSpacePre_AI"
begin
context ARM begin
lemmas typ_at_eq_kheap_obj = typ_at_eq_kheap_obj atyp_at_eq_kheap_obj
lemmas set_cap_atyp_ats[wp] = abs_atyp_at_lifts[OF set_cap_typ_at]
lemmas cap_master_cap_def = cap_master_cap_def[simplified cap_master_arch_cap_def]
definition
"final_matters_arch ac \<equiv>
(case ac of
ASIDPoolCap r as \<Rightarrow> True
| ASIDControlCap \<Rightarrow> False
| PageCap r rghts sz mapdata \<Rightarrow> False
| PageTableCap r mapdata \<Rightarrow> True
| PageDirectoryCap r mapdata \<Rightarrow> True)"
definition
"cap_vptr_arch acap \<equiv> case acap of
(PageCap _ _ _ (Some (_, vptr))) \<Rightarrow> Some vptr
| (PageTableCap _ (Some (_, vptr))) \<Rightarrow> Some vptr
| _ \<Rightarrow> None"
definition
"cap_vptr cap \<equiv> arch_cap_fun_lift cap_vptr_arch None cap"
declare cap_vptr_arch_def[abs_def, simp]
lemmas cap_vptr_simps [simp] =
cap_vptr_def [simplified, split_simps cap.split arch_cap.split option.split prod.split]
definition
"is_derived_arch cap cap' \<equiv>
((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow>
cap_asid cap = cap_asid cap' \<and> cap_asid cap \<noteq> None) \<and>
(vs_cap_ref cap = vs_cap_ref cap' \<or> is_pg_cap cap')"
lemma is_derived_arch_non_arch:
"\<not>is_arch_cap cap \<Longrightarrow> \<not> is_arch_cap cap' \<Longrightarrow>
is_derived_arch cap cap'"
unfolding is_derived_arch_def is_pg_cap_def is_pt_cap_def is_pd_cap_def
vs_cap_ref_def is_arch_cap_def
by (auto split: cap.splits)
lemma is_derived_cap_arch_asid:
"is_derived_arch cap cap' \<Longrightarrow> cap_master_cap cap = cap_master_cap cap' \<Longrightarrow>
is_pt_cap cap' \<or> is_pd_cap cap' \<Longrightarrow> cap_asid cap = cap_asid cap'"
unfolding is_derived_arch_def
apply (cases cap; cases cap'; simp)
by (auto simp: is_cap_simps cap_master_cap_def split: arch_cap.splits)
lemma is_page_cap_PageCap[simp]:
"is_page_cap (PageCap ref rghts pgsiz mapdata)"
by (simp add: is_page_cap_def)
lemma pageBitsForSize_eq[simp]:
"(pageBitsForSize sz = pageBitsForSize sz') = (sz = sz')"
by (case_tac sz) (case_tac sz', simp+)+
lemma
cap_master_cap_arch_simps:
"cap_master_arch_cap ((arch_cap.PageCap ref rghts sz mapdata)) =
(arch_cap.PageCap ref UNIV sz None)"
"cap_master_arch_cap ( (arch_cap.ASIDPoolCap pool asid)) =
(arch_cap.ASIDPoolCap pool 0)"
"cap_master_arch_cap ( (arch_cap.PageTableCap ptr x)) =
(arch_cap.PageTableCap ptr None)"
"cap_master_arch_cap ( (arch_cap.PageDirectoryCap ptr y)) =
(arch_cap.PageDirectoryCap ptr None)"
"cap_master_arch_cap ( arch_cap.ASIDControlCap) =
arch_cap.ASIDControlCap"
by (simp add: cap_master_arch_cap_def)+
lemma aobj_ref_cases':
"aobj_ref acap = (case acap of arch_cap.ASIDControlCap \<Rightarrow> aobj_ref acap
| _ \<Rightarrow> aobj_ref acap)"
by (simp split: arch_cap.split)
lemma aobj_ref_cases:
"aobj_ref acap =
(case acap of
arch_cap.ASIDPoolCap w1 w2 \<Rightarrow> Some w1
| arch_cap.ASIDControlCap \<Rightarrow> None
| arch_cap.PageCap w s sz opt \<Rightarrow> Some w
| arch_cap.PageTableCap w opt \<Rightarrow> Some w
| arch_cap.PageDirectoryCap w opt \<Rightarrow> Some w)"
apply (subst aobj_ref_cases')
apply (clarsimp cong: arch_cap.case_cong)
done
definition
"cap_asid_base_arch cap \<equiv> case cap of
(arch_cap.ASIDPoolCap _ asid) \<Rightarrow> Some asid
| _ \<Rightarrow> None"
declare cap_asid_base_arch_def[abs_def, simp]
definition
"cap_asid_base cap \<equiv> arch_cap_fun_lift cap_asid_base_arch None cap"
lemmas cap_asid_base_simps [simp] =
cap_asid_base_def [simplified, split_simps cap.split arch_cap.split]
definition
"ups_of_heap h \<equiv> \<lambda>p.
case h p of Some (ArchObj (DataPage sz)) \<Rightarrow> Some sz | _ \<Rightarrow> None"
lemma ups_of_heap_typ_at:
"ups_of_heap (kheap s) p = Some sz \<longleftrightarrow> typ_at (AArch (AIntData sz)) p s"
by (simp add: typ_at_eq_kheap_obj ups_of_heap_def
split: option.splits Structures_A.kernel_object.splits
arch_kernel_obj.splits)
lemma ups_of_heap_typ_at_def:
"ups_of_heap (kheap s) \<equiv> \<lambda>p.
if \<exists>!sz. typ_at (AArch (AIntData sz)) p s
then Some (THE sz. typ_at (AArch (AIntData sz)) p s)
else None"
apply (rule eq_reflection)
apply (rule ext)
apply (clarsimp simp: ups_of_heap_typ_at)
apply (intro conjI impI)
apply (frule (1) theI')
apply safe
apply (fastforce simp: ups_of_heap_typ_at)
apply (clarsimp simp add: obj_at_def)
done
lemma ups_of_heap_non_arch_upd:
"h x = Some ko \<Longrightarrow> non_arch_obj ko \<Longrightarrow> non_arch_obj ko' \<Longrightarrow> ups_of_heap (h(x \<mapsto> ko')) = ups_of_heap h"
by (rule ext) (auto simp add: ups_of_heap_def non_arch_obj_def split: kernel_object.splits)
definition
"is_simple_cap_arch cap \<equiv> \<not>is_pt_cap cap \<and> \<not> is_pd_cap cap"
lemma is_simple_cap_arch:
"\<not>is_arch_cap cap \<Longrightarrow> is_simple_cap_arch cap"
by (simp add: is_simple_cap_arch_def)
crunch inv[wp]: lookup_ipc_buffer "I"
lemma vs_cap_ref_to_table_cap_ref:
"\<not> is_pg_cap cap \<Longrightarrow> vs_cap_ref cap = table_cap_ref cap"
by (simp add: is_pg_cap_def table_cap_ref_def vs_cap_ref_simps
split: cap.splits arch_cap.splits)
lemma cap_master_cap_pg_cap:
"\<lbrakk>cap_master_cap cap = cap_master_cap capa\<rbrakk>
\<Longrightarrow> is_pg_cap cap = is_pg_cap capa"
by (clarsimp simp:cap_master_cap_def is_cap_simps
split:cap.splits arch_cap.splits dest!:cap_master_cap_eqDs)
lemma master_arch_cap_obj_refs:
"cap_master_arch_cap c = cap_master_arch_cap c' \<Longrightarrow> aobj_ref c = aobj_ref c'"
by (simp add: cap_master_arch_cap_def split: arch_cap.splits)
lemma master_arch_cap_cap_class:
"cap_master_arch_cap c = cap_master_arch_cap c' \<Longrightarrow> acap_class c = acap_class c'"
by (simp add: cap_master_arch_cap_def split: arch_cap.splits)
lemma is_cap_free_index_update[simp]:
"is_pd_cap (src_cap\<lparr>free_index := a\<rparr>) = is_pd_cap src_cap"
"is_pt_cap (src_cap\<lparr>free_index := a\<rparr>) = is_pt_cap src_cap"
by (simp add:is_cap_simps free_index_update_def split:cap.splits)+
lemma masked_as_full_test_function_stuff[simp]:
"is_pd_cap (masked_as_full a cap ) = is_pd_cap a"
"is_pt_cap (masked_as_full a cap ) = is_pt_cap a"
"vs_cap_ref (masked_as_full a cap ) = vs_cap_ref a"
by (auto simp:masked_as_full_def)
lemma same_aobject_as_commute:
"same_aobject_as x y \<Longrightarrow> same_aobject_as y x"
by (cases x; cases y; clarsimp)
lemmas wellformed_cap_simps = wellformed_cap_simps[simplified wellformed_acap_def, split_simps arch_cap.split]
lemma same_master_cap_same_types:
"cap_master_cap cap = cap_master_cap cap' \<Longrightarrow>
(is_pt_cap cap = is_pt_cap cap') \<and> (is_pd_cap cap = is_pd_cap cap')"
by (clarsimp simp: cap_master_cap_def is_cap_simps
split: cap.splits arch_cap.splits)
lemma is_derived_cap_arch_asid_issues:
"is_derived_arch cap cap' \<Longrightarrow>
cap_master_cap cap = cap_master_cap cap'
\<Longrightarrow> ((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pg_cap cap \<or> (vs_cap_ref cap = vs_cap_ref cap'))"
apply (simp add: is_derived_arch_def)
by (auto simp: cap_master_cap_def is_cap_simps
cap_asid_def
split: cap.splits arch_cap.splits option.splits)
lemma is_pt_pd_Null[simp]:
"\<not> is_pt_cap cap.NullCap \<and> \<not> is_pd_cap cap.NullCap"
by (simp add: is_pt_cap_def is_pd_cap_def)
lemma unique_table_caps_upd_eqD:
"\<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b';
is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'\<rbrakk>
\<Longrightarrow> unique_table_caps (ms (a \<mapsto> b')) = unique_table_caps (ms)"
unfolding unique_table_caps_def
apply (rule iffI)
apply (intro allI impI,elim allE)
apply (erule impE)
apply (rule_tac p = p in fun_upd_Some)
apply assumption
apply (erule impE)
apply (rule_tac p = p' in fun_upd_Some)
apply simp
apply (simp add: if_distrib split:if_splits)
apply (intro allI impI,elim allE)
apply (erule impE)
apply (rule_tac p = p in fun_upd_Some_rev)
apply simp+
apply (erule impE)
apply (rule_tac p = p' in fun_upd_Some_rev)
apply simp+
apply (simp add: if_distrib split:if_splits)
done
lemma set_untyped_cap_as_full_not_final_not_pg_cap:
"\<lbrace>\<lambda>s. (\<exists>a b. (a, b) \<noteq> dest \<and> \<not> is_pg_cap cap'
\<and> cte_wp_at (\<lambda>cap. obj_irq_refs cap = obj_irq_refs cap' \<and> \<not> is_pg_cap cap) (a, b) s)
\<and> cte_wp_at (op = src_cap) src s\<rbrace>
set_untyped_cap_as_full src_cap cap src
\<lbrace>\<lambda>_ s.(\<exists>a b. (a, b) \<noteq> dest \<and> \<not> is_pg_cap cap'
\<and> cte_wp_at (\<lambda>cap. obj_irq_refs cap = obj_irq_refs cap' \<and> \<not> is_pg_cap cap) (a, b) s)\<rbrace>"
apply (rule hoare_pre)
apply (wp hoare_vcg_ex_lift)
apply (rule_tac Q = "cte_wp_at Q slot"
and Q'="cte_wp_at (op = src_cap) src" for Q slot in P_bool_lift' )
apply (wp set_untyped_cap_as_full_cte_wp_at)
subgoal by (auto simp: cte_wp_at_caps_of_state is_cap_simps masked_as_full_def cap_bits_untyped_def)
apply (wp set_untyped_cap_as_full_cte_wp_at_neg)
apply (auto simp: cte_wp_at_caps_of_state is_cap_simps masked_as_full_def cap_bits_untyped_def)
done
end
end

68
proof/invariant-abstract/ARM/ArchInvariants_AI.thy
View File

@ -40,14 +40,15 @@ lemma arch_cap_fun_lift_expand[simp]:
| PageCap obj_ref rights sz vr \<Rightarrow> P_PageCap obj_ref rights sz vr
| PageTableCap obj_ref vr \<Rightarrow> P_PageTableCap obj_ref vr
| PageDirectoryCap obj_ref asid \<Rightarrow> P_PageDirectoryCap obj_ref asid)
F c) =
F) = (\<lambda>c.
(case c of
ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> P_ASIDPoolCap obj_ref asid
| ArchObjectCap (ASIDControlCap) \<Rightarrow> P_ASIDControlCap
| ArchObjectCap (PageCap obj_ref rights sz vr) \<Rightarrow> P_PageCap obj_ref rights sz vr
| ArchObjectCap (PageTableCap obj_ref vr) \<Rightarrow> P_PageTableCap obj_ref vr
| ArchObjectCap (PageDirectoryCap obj_ref asid) \<Rightarrow> P_PageDirectoryCap obj_ref asid
| _ \<Rightarrow> F)"
| _ \<Rightarrow> F))"
apply (rule ext)
by (simp add: arch_cap_fun_lift_def)
lemma arch_obj_fun_lift_expand[simp]:
@ -56,18 +57,23 @@ lemma arch_obj_fun_lift_expand[simp]:
| PageTable pt \<Rightarrow> P_PageTable pt
| PageDirectory pd \<Rightarrow> P_PageDirectory pd
| DataPage s \<Rightarrow> P_DataPage s)
F ko) =
F) = (\<lambda>ko.
(case ko of
ArchObj (ASIDPool pool) \<Rightarrow> P_ASIDPool pool
| ArchObj (PageTable pt) \<Rightarrow> P_PageTable pt
| ArchObj (PageDirectory pd) \<Rightarrow> P_PageDirectory pd
| ArchObj (DataPage s) \<Rightarrow> P_DataPage s
| _ \<Rightarrow> F)"
| _ \<Rightarrow> F))"
apply (rule ext)
by (simp only: arch_obj_fun_lift_def)
lemmas aa_type_simps =
aa_type_def[split_simps arch_kernel_obj.split]
lemmas a_type_simps = a_type_simps aa_type_simps
lemmas a_type_def = a_type_def[simplified aa_type_def]
definition
"vmsz_aligned ref sz \<equiv> is_aligned ref (pageBitsForSize sz)"
@ -159,15 +165,21 @@ where
| "acap_class (PageDirectoryCap x y) = PhysicalClass"
definition
valid_ipc_buffer_cap :: "cap \<Rightarrow> word32 \<Rightarrow> bool"
valid_ipc_buffer_cap_arch :: "arch_cap \<Rightarrow> word32 \<Rightarrow> bool"
where
"valid_ipc_buffer_cap c bufptr \<equiv>
case c of
ArchObjectCap (PageCap ref rghts sz mapdata) \<Rightarrow>
"valid_ipc_buffer_cap_arch ac bufptr \<equiv>
case ac of
(PageCap ref rghts sz mapdata) \<Rightarrow>
is_aligned bufptr msg_align_bits
| _ \<Rightarrow> True"
declare valid_ipc_buffer_cap_arch_def[simp]
definition
"valid_ipc_buffer_cap c bufptr \<equiv>
arch_cap_fun_lift (\<lambda>ac. valid_ipc_buffer_cap_arch ac bufptr) True c"
primrec
valid_pte :: "pte \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
@ -640,18 +652,17 @@ lemma is_arch_cap_simps:
"is_pt_cap cap = (\<exists>p asid. cap = (ArchObjectCap (PageTableCap p asid)))"
by (auto simp add: is_pg_cap_def is_pd_cap_def is_pt_cap_def)
definition
"cap_asid_arch \<equiv> \<lambda> cap. case cap of
"cap_asid_arch cap \<equiv> case cap of
PageCap _ _ _ (Some (asid, _)) \<Rightarrow> Some asid
| PageTableCap _ (Some (asid, _)) \<Rightarrow> Some asid
| PageDirectoryCap _ (Some asid) \<Rightarrow> Some asid
| _ \<Rightarrow> None"
declare cap_asid_arch_def[simp]
declare cap_asid_arch_def[abs_def, simp]
definition
"cap_asid = arch_cap_fun_lift cap_asid_arch None"
"cap_asid cap = arch_cap_fun_lift cap_asid_arch None cap"
(* needed for retype: if reachable, then cap, if cap then protected by untyped cap.
@ -934,7 +945,7 @@ lemma atyp_at_eq_kheap_obj:
"typ_at (AArch APageDirectory) p s \<longleftrightarrow> (\<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd)))"
"typ_at (AArch (AIntData sz)) p s \<longleftrightarrow> (kheap s p = Some (ArchObj (DataPage sz)))"
apply (auto simp add: obj_at_def)
apply (simp_all add: a_type_def aa_type_def
apply (simp_all add: a_type_def
split: split_if_asm kernel_object.splits arch_kernel_obj.splits)
done
@ -1166,7 +1177,7 @@ lemma aobj_at_default_arch_cap_valid:
using assms
by (auto elim!: obj_at_weakenE
simp add: arch_default_cap_def valid_arch_cap_def default_arch_object_def
a_type_def aa_type_def
a_type_def
valid_vm_rights_def
split: apiobject_type.splits aobject_type.splits option.splits)
@ -1203,7 +1214,7 @@ lemma page_directory_pde_atI:
pspace_aligned s \<rbrakk> \<Longrightarrow> pde_at (p + (x << 2)) s"
apply (clarsimp simp: obj_at_def pde_at_def)
apply (drule (1) pspace_alignedD[rotated])
apply (clarsimp simp: a_type_def aa_type_def
apply (clarsimp simp: a_type_def
split: kernel_object.splits arch_kernel_obj.splits split_if_asm)
apply (simp add: aligned_add_aligned is_aligned_shiftl_self word_bits_conv)
apply (subgoal_tac "p = (p + (x << 2) && ~~ mask pd_bits)")
@ -1222,7 +1233,7 @@ lemma page_table_pte_atI:
"\<lbrakk> page_table_at p s; x < 2^(pt_bits - 2); pspace_aligned s \<rbrakk> \<Longrightarrow> pte_at (p + (x << 2)) s"
apply (clarsimp simp: obj_at_def pte_at_def)
apply (drule (1) pspace_alignedD[rotated])
apply (clarsimp simp: a_type_def aa_type_def
apply (clarsimp simp: a_type_def
split: kernel_object.splits arch_kernel_obj.splits split_if_asm)
apply (simp add: aligned_add_aligned is_aligned_shiftl_self word_bits_conv)
apply (subgoal_tac "p = (p + (x << 2) && ~~ mask pt_bits)")
@ -1808,7 +1819,7 @@ lemma vs_ref_order:
apply (erule vs_lookup_induct)
apply (clarsimp simp: valid_arch_state_def valid_asid_table_def ranI)
apply (clarsimp dest!: vs_lookup1D elim!: obj_atE)
apply (clarsimp simp: vs_refs_def a_type_simps aa_type_simps
apply (clarsimp simp: vs_refs_def a_type_simps
split: kernel_object.split_asm arch_kernel_obj.split_asm
dest!: graph_ofD)
apply (drule valid_arch_objsD) apply (simp add: obj_at_def) apply (assumption)
@ -2022,6 +2033,29 @@ lemma acap_rights_update_id [intro!, simp]:
unfolding wellformed_acap_def acap_rights_update_def
by (auto split: arch_cap.splits)
lemmas cap_asid_simps [simp] =
cap_asid_def [simplified, split_simps cap.split arch_cap.split option.split prod.split]
lemma in_user_frame_def:
"in_user_frame p \<equiv> \<lambda>s.
\<exists>sz. typ_at (AArch (AIntData sz)) (p && ~~ mask (pageBitsForSize sz)) s"
apply (rule eq_reflection, rule ext)
apply (simp add: in_user_frame_def obj_at_def)
apply (rule_tac f=Ex in arg_cong)
apply (rule ext, rule iffI)
apply (simp add: a_type_simps)
apply clarsimp
done
lemma in_user_frame_lift:
assumes typ_at: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>_. typ_at (AArch T) p\<rbrace>"
shows "\<lbrace>in_user_frame p\<rbrace> f \<lbrace>\<lambda>_. in_user_frame p\<rbrace>"
unfolding in_user_frame_def
by (wp hoare_vcg_ex_lift typ_at)
end
end

71
proof/invariant-abstract/ARM/ArchKHeap_AI.thy
View File

@ -14,9 +14,12 @@ begin
context ARM begin
sublocale
lemmas is_cap_simps = is_cap_simps is_arch_cap_simps
lemmas valid_cap_def = valid_cap_def[simplified valid_arch_cap_def]
sublocale
empty_table: arch_only_obj_pred "empty_table S" for S
by (unfold_locales, simp add: empty_table_def)
by (unfold_locales, simp add: empty_table_def del: arch_obj_fun_lift_expand)
sublocale
vs_refs: arch_only_obj_pred "\<lambda>ko. x \<in> vs_refs ko" for S
@ -222,15 +225,7 @@ lemma set_object_neg_ko:
apply (simp add: pred_neg_def obj_at_def)
done
lemma set_object_typ_at:
"\<lbrace>\<lambda>s. typ_at (a_type ko) p s \<and> P (typ_at T p' s)\<rbrace>
set_object p ko \<lbrace>\<lambda>rv s. P (typ_at T p' s)\<rbrace>"
apply (simp add: set_object_def)
apply wp
apply clarsimp
apply (erule rsubst [where P=P])
apply (clarsimp simp: obj_at_def)
done
lemma set_object_atyp_at:
"\<lbrace>\<lambda>s. typ_at (AArch (aa_type ako)) p s \<and> P (typ_at (AArch T) p' s)\<rbrace>
@ -336,6 +331,7 @@ lemma arch_lifts:
assumes arch: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
assumes aobj_at: "\<And>P P' pd. arch_obj_pred P' \<Longrightarrow>
\<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>"
notes arch_obj_fun_lift_expand[simp del]
shows
valid_global_pd_mappings_lift:
"\<lbrace>valid_global_pd_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_global_pd_mappings\<rbrace>" and
@ -347,7 +343,11 @@ lemma arch_lifts:
valid_asid_map_lift:
"\<lbrace>valid_asid_map\<rbrace> f \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>" and
valid_kernel_mappings_lift:
"\<lbrace>valid_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>"
"\<lbrace>valid_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" and
valid_global_pts_lift:
"\<lbrace>valid_global_pts\<rbrace> f \<lbrace>\<lambda>rv. valid_global_pts\<rbrace>" and
valid_arch_state_lift_aobj_at:
"\<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
apply -
subgoal
@ -407,6 +407,20 @@ lemma arch_lifts:
apply (case_tac xa; simp add: hoare_vcg_prop)
done
subgoal valid_global_pts
apply (simp add: valid_global_pts_def)
apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch])
apply (rule hoare_vcg_ball_lift)
apply (rule aobj_at)
apply clarsimp
done
subgoal
apply (simp add: valid_arch_state_def valid_asid_table_def)
apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch])
apply (wp hoare_vcg_conj_lift hoare_vcg_ball_lift valid_global_pts | (rule aobj_at, clarsimp))+
done
done
lemma equal_kernel_mappings_lift:
@ -425,23 +439,42 @@ lemma valid_machine_state_lift:
assumes memory: "\<And>P. \<lbrace>\<lambda>s. P (underlying_memory (machine_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (underlying_memory (machine_state s))\<rbrace>"
assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
shows "\<lbrace>valid_machine_state\<rbrace> f \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
unfolding valid_machine_state_def in_user_frame_def
unfolding valid_machine_state_def
apply (rule hoare_lift_Pf[where f="\<lambda>s. underlying_memory (machine_state s)", OF _ memory])
apply (rule hoare_vcg_all_lift)
apply (rule hoare_vcg_disj_lift[OF _ hoare_vcg_prop])
apply (rule hoare_vcg_ex_lift)
subgoal for \<dots> sz
by (rule aobj_at[where P'="\<lambda>ao. ao = ArchObj (DataPage sz)",
simplified obj_at_def[abs_def], simplified])
apply (rule in_user_frame_lift)
apply (wp aobj_at)
apply simp
done
(*
lemma bool_pred_exhaust:
"(P = (\<lambda>x. x)) \<or> (P = (\<lambda>x. \<not>x)) \<or> (P = (\<lambda>_. True)) \<or> (P = (\<lambda>_. False))"
apply (cases "P True"; cases "P False")
apply (rule disjI2, rule disjI2, rule disjI1, rule ext)
defer
apply (rule disjI1, rule ext)
defer
apply (rule disjI2, rule disjI1, rule ext)
defer
apply (rule disjI2, rule disjI2, rule disjI2, rule ext)
apply (match conclusion in "P x = _" for x \<Rightarrow> \<open>cases x; fastforce\<close>)+
done
*)
lemma valid_ao_at_lift:
assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>"
shows "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>"
unfolding valid_ao_at_def
by (wp hoare_vcg_ex_lift y valid_arch_obj_typ z)
lemma valid_ao_at_lift_aobj_at:
assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
shows "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>"
unfolding valid_ao_at_def
by (wp hoare_vcg_ex_lift valid_arch_obj_typ aobj_at | clarsimp)+
lemmas set_object_v_ker_map
= set_object_valid_kernel_mappings
@ -524,7 +557,7 @@ lemma set_object_global_pd_mappings:
apply (simp add: set_object_def, wp)
apply clarsimp
apply (erule valid_global_pd_mappings_pres)
apply (clarsimp simp: obj_at_def a_type_def aa_type_def global_refs_def)+
apply (clarsimp simp: obj_at_def a_type_def global_refs_def)+
done

7
proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy
View File

@ -28,13 +28,6 @@ lemma ptrFormPAddr_addFromPPtr :
"Platform.ARM.ptrFromPAddr (Platform.ARM.addrFromPPtr x) = x"
by (simp add: Platform.ARM.ptrFromPAddr_def Platform.ARM.addrFromPPtr_def)
definition
"cap_asid_base cap \<equiv> case cap of
cap.ArchObjectCap (arch_cap.ASIDPoolCap _ asid) \<Rightarrow> Some asid
| _ \<Rightarrow> None"
lemmas cap_asid_base_simps [simp] =
cap_asid_base_def [split_simps cap.split arch_cap.split]
(****** From GeneralLib *******)

55
proof/invariant-abstract/ARM/ArchTcbAcc_AI.thy Normal file
View File

@ -0,0 +1,55 @@
(*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*)
theory ArchTcbAcc_AI
imports "../CSpace_AI"
begin
context ARM begin
lemmas cap_master_cap_simps =
cap_master_cap_def[simplified cap_master_arch_cap_def, split_simps cap.split arch_cap.split]
lemma cap_master_cap_arch_eqDs:
"cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageCap ref rghts sz mapdata)
\<Longrightarrow> rghts = UNIV \<and> mapdata = None
\<and> (\<exists>rghts mapdata. cap = cap.ArchObjectCap (arch_cap.PageCap ref rghts sz mapdata))"
"cap_master_cap cap = cap.ArchObjectCap arch_cap.ASIDControlCap
\<Longrightarrow> cap = cap.ArchObjectCap arch_cap.ASIDControlCap"
"cap_master_cap cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap pool asid)
\<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap pool asid))"
"cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageTableCap ptr data)
\<Longrightarrow> data = None \<and> (\<exists>data. cap = cap.ArchObjectCap (arch_cap.PageTableCap ptr data))"
"cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap ptr data2)
\<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap ptr data2))"
by (clarsimp simp: cap_master_cap_def
split: cap.split_asm arch_cap.split_asm)+
lemmas cap_master_cap_eqDs =
cap_master_cap_eqDs1 cap_master_cap_arch_eqDs
cap_master_cap_eqDs1 [OF sym] cap_master_cap_arch_eqDs[OF sym]
lemma vm_sets_diff[simp]:
"vm_read_only \<noteq> vm_read_write"
by (simp add: vm_read_write_def vm_read_only_def)
lemmas vm_sets_diff2[simp] = not_sym[OF vm_sets_diff]
lemma cap_master_cap_tcb_cap_valid_arch:
"\<lbrakk> cap_master_cap c = cap_master_cap c'; is_arch_cap c \<rbrakk> \<Longrightarrow>
tcb_cap_valid c p s = tcb_cap_valid c' p s"
by (simp add: cap_master_cap_def tcb_cap_valid_def tcb_cap_cases_def
valid_ipc_buffer_cap_def is_cap_simps
split: option.splits cap.splits arch_cap.splits
Structures_A.thread_state.splits)
end
end

4521
proof/invariant-abstract/ARM/ArchVSpace_AI.thy Normal file
View File

File diff suppressed because it is too large Load Diff

4
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)) = Arch_Structs_A.InvalidPDE \<rbrakk> \<Longrightarrow>
pd (ucast (p && mask pd_bits >> 2)) = InvalidPDE \<rbrakk> \<Longrightarrow>
empty_pde_at p s"
by (fastforce simp add: empty_pde_at_def)
@ -1658,7 +1658,7 @@ lemma arch_decode_inv_wf[wp]:
apply (erule impE)
apply clarsimp
apply (erule impE)
apply (clarsimp split:Arch_Structs_A.pde.splits)
apply (clarsimp split: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]

27
proof/invariant-abstract/CSpaceInvPre_AI.thy
View File

@ -12,9 +12,18 @@ theory CSpaceInvPre_AI
imports "./$L4V_ARCH/ArchAcc_AI"
begin
unqualify_consts (in Arch)
table_cap_ref :: "cap \<Rightarrow> vs_ref list option"
context Arch begin
unqualify_consts
table_cap_ref :: "cap \<Rightarrow> vs_ref list option"
empty_table
unqualify_facts
empty_table_def
end
lemma set_cap_caps_of_state[wp]:
"\<lbrace>\<lambda>s. P ((caps_of_state s) (ptr \<mapsto> cap))\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>"
apply (cases ptr)
@ -123,6 +132,20 @@ where
\<lambda>s. \<forall>p \<in> UNIV - S. \<not> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and>
\<not> (table_cap_ref c = table_cap_ref cap)) p s"
lemma empty_table_caps_of:
"empty_table S ko \<Longrightarrow> caps_of ko = {}"
by (cases ko, simp_all add: empty_table_def caps_of_def cap_of_def)
context begin interpretation ARM . (*FIXME arch_split *)
lemma free_index_update_test_function_stuff[simp]:
"cap_asid (src_cap\<lparr>free_index := a\<rparr>) = cap_asid src_cap"
"obj_irq_refs (src_cap\<lparr>free_index := a\<rparr>) = obj_irq_refs src_cap"
"vs_cap_ref (src_cap\<lparr>free_index := a\<rparr>) = vs_cap_ref src_cap"
"untyped_range (cap \<lparr>free_index :=a \<rparr>) = untyped_range cap"
"zobj_refs (c\<lparr>free_index:=a\<rparr>) = zobj_refs c"
"obj_refs (c\<lparr>free_index:=a\<rparr>) = obj_refs c"
by (auto simp:cap_asid_def free_index_update_def vs_cap_ref_def
is_cap_simps obj_irq_refs_def split:cap.splits arch_cap.splits)
end
end

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

@ -28,6 +28,10 @@ unqualify_facts (in Arch)
valid_validate_vm_rights[simp]
cap_master_arch_inv[simp]
unique_table_refs_def
valid_ipc_buffer_cap_def
acap_rights_update_idem[simp]
cap_master_arch_cap_rights[simp]
acap_rights_update_id [intro!, simp]
lemma remove_rights_cap_valid[simp]:
"s \<turnstile> c \<Longrightarrow> s \<turnstile> remove_rights S c"
@ -377,13 +381,18 @@ lemma cap_master_cap_eqDs1:
"cap_master_cap cap = cap.ReplyCap ref master
\<Longrightarrow> master = True
\<and> (\<exists>master. cap = cap.ReplyCap ref master)"
"cap_master_cap cap = ArchObjectCap acap
\<Longrightarrow> \<exists>ac. cap = ArchObjectCap ac \<and> acap = cap_master_arch_cap ac"
by (clarsimp simp: cap_master_cap_def
split: cap.split_asm)+
lemma cap_master_cap_arch_eqD:
"cap_master_cap cap = ArchObjectCap acap
\<Longrightarrow> \<exists>ac. cap = ArchObjectCap ac \<and> acap = cap_master_arch_cap ac"
by (clarsimp simp: cap_master_cap_def
split: cap.split_asm)+
lemmas cap_master_cap_eqDs = cap_master_cap_eqDs1 cap_master_cap_eqDs1 [OF sym]
lemmas cap_master_cap_eqDs =
cap_master_cap_eqDs1 cap_master_cap_arch_eqD
cap_master_cap_eqDs1 [OF sym] cap_master_cap_arch_eqD [OF sym]
definition
@ -1642,7 +1651,7 @@ lemma replace_cap_invs:
\<and> s \<turnstile> cap\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv s. invs s\<rbrace>"
apply (simp add: invs_def valid_state_def valid_mdb_def2)
(* apply (simp add: invs_def valid_state_def valid_mdb_def2)
apply (rule hoare_pre)
apply (wp replace_cap_valid_pspace
set_cap_caps_of_state2 set_cap_idle
@ -1723,7 +1732,7 @@ lemma replace_cap_invs:
valid_arch_caps_def unique_table_refs_no_cap_asidE)
apply simp
apply (rule Ball_emptyI, simp add: obj_irq_refs_subset)
done
done*) sorry
crunch cte_wp_at: set_cdt "cte_wp_at P p"
@ -1866,21 +1875,13 @@ lemma set_untyped_cap_as_full_cte_wp_at:
done
lemma free_index_update_test_function_stuff[simp]:
"cap_asid (src_cap\<lparr>free_index := a\<rparr>) = cap_asid src_cap"
"obj_irq_refs (src_cap\<lparr>free_index := a\<rparr>) = obj_irq_refs src_cap"
"vs_cap_ref (src_cap\<lparr>free_index := a\<rparr>) = vs_cap_ref src_cap"
"untyped_range (cap \<lparr>free_index :=a \<rparr>) = untyped_range cap"
"zobj_refs (c\<lparr>free_index:=a\<rparr>) = zobj_refs c"
"obj_refs (c\<lparr>free_index:=a\<rparr>) = obj_refs c"
by (auto simp:cap_asid_def free_index_update_def vs_cap_ref_def
is_cap_simps obj_irq_refs_def split:cap.splits arch_cap.splits)
lemma valid_cap_free_index_update[simp]:
"valid_cap cap s \<Longrightarrow> valid_cap (max_free_index_update cap) s"
apply (case_tac cap)
apply (simp_all add:free_index_update_def split:cap.splits arch_cap.splits)
apply (simp_all add:free_index_update_def split:cap.splits )
apply (clarsimp simp:valid_cap_def cap_aligned_def valid_untyped_def max_free_index_def)
done
@ -1898,7 +1899,7 @@ lemma cap_insert_ex_cap:
apply (wp set_cap_cap_to get_cap_wp set_cap_cte_wp_at set_untyped_cap_as_full_cte_wp_at)
apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_splits)
apply (wp set_cap_cap_to get_cap_wp)
apply (clarsimp elim!: cte_wp_at_weakenE simp:is_cap_simps cte_wp_at_caps_of_state)
apply_trace (clarsimp elim!: cte_wp_at_weakenE simp:is_cap_simps cte_wp_at_caps_of_state)
apply (simp add:masked_as_full_def)
done
@ -2052,7 +2053,7 @@ lemma tcb_cap_valid_update_free_index[simp]:
split:if_splits cap.split_asm Structures_A.thread_state.split_asm)
apply (clarsimp simp:pred_tcb_at_def obj_at_def is_cap_simps free_index_update_def
valid_ipc_buffer_cap_def
split:cap.split_asm)
split:cap.splits)
done
@ -2122,13 +2123,13 @@ lemma cap_insert_valid_cap[wp]:
lemma cap_rights_update_idem [simp]:
"cap_rights_update R (cap_rights_update R' cap) = cap_rights_update R cap"
by (simp add: cap_rights_update_def acap_rights_update_def split: cap.splits arch_cap.splits)
by (simp add: cap_rights_update_def split: cap.splits)
lemma cap_master_cap_rights [simp]:
"cap_master_cap (cap_rights_update R cap) = cap_master_cap cap"
by (simp add: cap_master_cap_def cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits)
by (simp add: cap_master_cap_def cap_rights_update_def
split: cap.splits)
lemma cap_insert_obj_at_other:
@ -2138,6 +2139,10 @@ lemma cap_insert_obj_at_other:
apply (wp set_cap_obj_at_other get_cap_wp|simp split del: split_if)+
done
lemma only_idle_tcb_update:
"\<lbrakk>only_idle s; ko_at (TCB t) p s; tcb_state t = tcb_state t' \<or> \<not>idle (tcb_state t') \<rbrakk>
\<Longrightarrow> only_idle (s\<lparr>kheap := kheap s(p \<mapsto> TCB t')\<rparr>)"
by (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def)
lemma as_user_only_idle :
"\<lbrace>only_idle\<rbrace> as_user t m \<lbrace>\<lambda>_. only_idle\<rbrace>"
@ -2151,19 +2156,13 @@ lemma as_user_only_idle :
done
lemma valid_cap_imp_valid_vm_rights:
"valid_cap (cap.ArchObjectCap (arch_cap.PageCap mw rs sz m)) s \<Longrightarrow>
rs \<in> valid_vm_rights"
by (simp add: valid_cap_def valid_vm_rights_def)
lemma cap_rights_update_id [intro!, simp]:
"valid_cap c s \<Longrightarrow> cap_rights_update (cap_rights c) c = c"
unfolding cap_rights_update_def
acap_rights_update_def
apply (cases c, simp_all)
apply (simp add: valid_cap_def)
apply (clarsimp simp: valid_cap_imp_valid_vm_rights split: arch_cap.splits)
apply (fastforce simp: valid_cap_def)
done

126
proof/invariant-abstract/CSpacePre_AI.thy Normal file
View File

@ -0,0 +1,126 @@
(*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*)
(*
CSpace invariants preamble
*)
theory CSpacePre_AI
imports CSpaceInv_AI
begin
unqualify_consts (in Arch)
cap_asid
lemma fun_upd_Some:
"ms p = Some k \<Longrightarrow> (ms(a \<mapsto> b)) p = Some (if a = p then b else k)"
by auto
lemma fun_upd_Some_rev:
"\<lbrakk>ms a = Some k; (ms(a \<mapsto> b)) p = Some cap\<rbrakk>
\<Longrightarrow> ms p = Some (if a = p then k else cap)"
by auto
lemma P_bool_lift':
"\<lbrakk>\<lbrace>Q and Q'\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>(\<lambda>s. \<not> Q s) and Q'\<rbrace> f \<lbrace>\<lambda>r s. \<not> Q s\<rbrace>\<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s. P (Q s) \<and> Q' s\<rbrace> f \<lbrace>\<lambda>r s. P (Q s)\<rbrace>"
apply (clarsimp simp:valid_def)
apply (elim allE)
apply (case_tac "Q s")
apply fastforce+
done
lemma free_index_update_simps[simp]:
"free_index_update g (cap.UntypedCap ref sz f) = cap.UntypedCap ref sz (g f)"
by (simp add:free_index_update_def)
(* FIXME: MOVE*)
lemma is_cap_free_index_update[simp]:
"is_zombie (src_cap\<lparr>free_index := f \<rparr>) = is_zombie src_cap"
"is_cnode_cap (src_cap\<lparr>free_index := f \<rparr>) = is_cnode_cap src_cap"
"is_thread_cap (src_cap\<lparr>free_index := f \<rparr>) = is_thread_cap src_cap"
"is_domain_cap (src_cap\<lparr>free_index := f \<rparr>) = is_domain_cap src_cap"
"is_ep_cap (src_cap\<lparr>free_index := f \<rparr>) = is_ep_cap src_cap"
"is_untyped_cap (src_cap\<lparr>free_index := f \<rparr>) = is_untyped_cap src_cap"
"is_arch_cap (src_cap\<lparr>free_index := f \<rparr>) = is_arch_cap src_cap"
"is_zombie (src_cap\<lparr>free_index := f \<rparr>) = is_zombie src_cap"
"is_ntfn_cap (src_cap\<lparr>free_index := f \<rparr>) = is_ntfn_cap src_cap"
"is_reply_cap (src_cap\<lparr>free_index := f \<rparr>) = is_reply_cap src_cap"
"is_master_reply_cap (src_cap\<lparr>free_index := f \<rparr>) = is_master_reply_cap src_cap"
by (simp add:is_cap_simps free_index_update_def split:cap.splits)+
lemma masked_as_full_simps[simp]:
"masked_as_full (cap.EndpointCap r badge a) cap = (cap.EndpointCap r badge a)"
"masked_as_full (cap.Zombie r bits n) cap = (cap.Zombie r bits n)"
"masked_as_full (cap.ArchObjectCap x) cap = (cap.ArchObjectCap x)"
"masked_as_full (cap.CNodeCap r n g) cap = (cap.CNodeCap r n g)"
"masked_as_full (cap.ReplyCap r m) cap = (cap.ReplyCap r m)"
"masked_as_full cap.NullCap cap = cap.NullCap"
"masked_as_full cap.DomainCap cap = cap.DomainCap"
"masked_as_full (cap.ThreadCap r) cap = cap.ThreadCap r"
"masked_as_full cap (cap.EndpointCap r badge a) = cap"
"masked_as_full cap (cap.Zombie r bits n) = cap"
"masked_as_full cap (cap.ArchObjectCap x) = cap"
"masked_as_full cap (cap.CNodeCap r n g) = cap"
"masked_as_full cap (cap.ReplyCap r m) = cap"
"masked_as_full cap cap.NullCap = cap"
"masked_as_full cap cap.DomainCap = cap"
"masked_as_full cap (cap.ThreadCap r) = cap"
by (simp add:masked_as_full_def)+
lemma maksed_as_full_test_function_stuff[simp]:
"obj_irq_refs (masked_as_full a cap) = obj_irq_refs a"
"cap_asid (masked_as_full a cap ) = cap_asid a"
"obj_refs (masked_as_full a cap ) = obj_refs a"
"is_zombie (masked_as_full a cap ) = is_zombie a"
"is_cnode_cap (masked_as_full a cap ) = is_cnode_cap a"
"is_thread_cap (masked_as_full a cap ) = is_thread_cap a"
"is_domain_cap (masked_as_full a cap ) = is_domain_cap a"
"is_ep_cap (masked_as_full a cap ) = is_ep_cap a"
"is_untyped_cap (masked_as_full a cap ) = is_untyped_cap a"
"is_arch_cap (masked_as_full a cap ) = is_arch_cap a"
"is_zombie (masked_as_full a cap ) = is_zombie a"
"is_ntfn_cap (masked_as_full a cap ) = is_ntfn_cap a"
"is_reply_cap (masked_as_full a cap ) = is_reply_cap a"
"is_master_reply_cap (masked_as_full a cap ) = is_master_reply_cap a"
by (auto simp:masked_as_full_def)
lemma set_untyped_cap_as_full_cte_wp_at_neg:
"\<lbrace>\<lambda>s. (dest \<noteq> src \<and> \<not> (cte_wp_at P dest s) \<or>
dest = src \<and> \<not> cte_wp_at (\<lambda>a. P (masked_as_full a cap)) src s) \<and>
cte_wp_at (op = src_cap) src s\<rbrace>
set_untyped_cap_as_full src_cap cap src
\<lbrace>\<lambda>ya s. \<not> cte_wp_at P dest s\<rbrace>"
apply (clarsimp simp:set_untyped_cap_as_full_def | rule conjI |wp set_cap_cte_wp_at_neg)+
apply (clarsimp simp:cte_wp_at_caps_of_state masked_as_full_def)+
apply wp
apply clarsimp
done
lemma set_untyped_cap_as_full_is_final_cap'_neg:
"\<lbrace>\<lambda>s. \<not> is_final_cap' cap' s \<and> cte_wp_at (op = src_cap) src s\<rbrace>
set_untyped_cap_as_full src_cap cap src
\<lbrace>\<lambda>rv s. \<not> is_final_cap' cap' s\<rbrace>"
apply (rule hoare_pre)
apply (simp add:is_final_cap'_def2)
apply (wp hoare_vcg_all_lift hoare_vcg_ex_lift)
apply (rule_tac Q = "cte_wp_at Q slot"
and Q'="cte_wp_at (op = src_cap) src" for Q slot in P_bool_lift' )
apply (wp set_untyped_cap_as_full_cte_wp_at)
apply clarsimp
apply (wp set_untyped_cap_as_full_cte_wp_at_neg)
apply (clarsimp simp:cte_wp_at_caps_of_state masked_as_full_def)
apply (clarsimp simp:is_final_cap'_def2)
done
end

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

File diff suppressed because it is too large Load Diff

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

@ -58,6 +58,7 @@ definition all_invs_but_valid_irq_states_for where
pspace_in_kernel_window and
cap_refs_in_kernel_window and cur_tcb"
context begin interpretation ARM . (*FIXME: arch_split*)
lemma dmo_maskInterrupt_invs:
"\<lbrace>all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)\<rbrace>
do_machine_op (maskInterrupt (state = IRQInactive) irq)
@ -66,6 +67,7 @@ lemma dmo_maskInterrupt_invs:
apply wp
apply (clarsimp simp: in_monad invs_def valid_state_def all_invs_but_valid_irq_states_for_def valid_irq_states_but_def valid_irq_masks_but_def valid_machine_state_def cur_tcb_def valid_irq_states_def valid_irq_masks_def)
done
end
lemma set_irq_state_invs[wp]:
"\<lbrace>\<lambda>s. invs s \<and> (state \<noteq> irq_state.IRQSignal \<longrightarrow> cap.IRQHandlerCap irq \<notin> ran (caps_of_state s))\<rbrace>

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

@ -2602,7 +2602,7 @@ sublocale Arch \<subseteq> revokable_update: Arch_p_arch_idle_update_int_eq "is_
interpretation machine_state_update:
p_arch_idle_update_int_eq "machine_state_update f"
by unfold_locales auto
sublocale Arch \<subseteq> machine_state_update: Arch_p_arch_idle_update_int_eq "is_original_cap_update f" by unfold_locales
sublocale Arch \<subseteq> machine_state_update: Arch_p_arch_idle_update_int_eq "machine_state_update f" by unfold_locales
interpretation cdt_update:
p_arch_idle_update_int_eq "cdt_update f"

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

@ -111,4 +111,15 @@ locale arch_only_obj_pred =
fixes P :: "kernel_object \<Rightarrow> bool"
assumes arch_only: "arch_obj_pred P"
lemma set_object_typ_at:
"\<lbrace>\<lambda>s. typ_at (a_type ko) p s \<and> P (typ_at T p' s)\<rbrace>
set_object p ko \<lbrace>\<lambda>rv s. P (typ_at T p' s)\<rbrace>"
apply (simp add: set_object_def)
apply wp
apply clarsimp
apply (erule rsubst [where P=P])
apply (clarsimp simp: obj_at_def)
done
end

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

@ -12,8 +12,12 @@ theory KHeap_AI
imports "./$L4V_ARCH/ArchKHeap_AI"
begin
context Arch begin
unqualify_facts (in Arch)
unqualify_consts
valid_ao_at
unqualify_facts
pspace_in_kernel_window_atyp_lift
valid_arch_objs_lift_weak
vs_lookup_arch_obj_at_lift
@ -25,6 +29,12 @@ unqualify_facts (in Arch)
equal_kernel_mappings_lift
valid_global_pd_mappings_lift
valid_machine_state_lift
valid_ao_at_lift_aobj_at
valid_arch_state_lift_aobj_at
valid_global_pts_lift
in_user_frame_lift
end
lemma get_object_wp:
"\<lbrace>\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> Q ko s\<rbrace> get_object p \<lbrace>Q\<rbrace>"
@ -210,6 +220,9 @@ shows
apply (simp add: xopv[simplified trans_state_update'])
done
crunch ct[wp]: set_thread_state "\<lambda>s. P (cur_thread s)"
lemma sts_ep_at_inv[wp]:
"\<lbrace> ep_at ep \<rbrace> set_thread_state t s \<lbrace> \<lambda>rv. ep_at ep \<rbrace>"
apply (simp add: set_thread_state_def)
@ -1248,6 +1261,15 @@ by (rule equal_kernel_mappings_lift, wp aobj_at)
lemma valid_global_pd_mappings[wp]: "\<lbrace>valid_global_pd_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_global_pd_mappings\<rbrace>"
by (rule valid_global_pd_mappings_lift, wp aobj_at)
lemma valid_ao_at[wp]:"\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>_. valid_ao_at p\<rbrace>"
by (rule valid_ao_at_lift_aobj_at; wp aobj_at; simp)
lemma valid_arch_state[wp]:"\<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
by (rule valid_arch_state_lift; wp aobj_at; simp)
lemma in_user_frame[wp]:"\<lbrace>in_user_frame p\<rbrace> f \<lbrace>\<lambda>_. in_user_frame p\<rbrace>"
by (rule in_user_frame_lift; wp aobj_at; simp)
end
@ -1302,9 +1324,9 @@ interpretation
set_endpoint: non_arch_non_cap_non_mem_op "set_endpoint p ep" +
set_notification: non_arch_non_cap_non_mem_op "set_notification p ntfn" +
sts: non_arch_non_cap_non_mem_op "set_thread_state p st" +
sbm: non_arch_non_cap_non_mem_op "set_bound_notification p b" +
sbn: non_arch_non_cap_non_mem_op "set_bound_notification p b" +
as_user: non_arch_non_cap_non_mem_op "as_user p g" +
thread_set: non_arch_op "thread_set f p" +
thread_set: non_arch_non_mem_op "thread_set f p" +
set_cap: non_arch_non_mem_op "set_cap cap p'"
apply (all \<open>unfold_locales; (wp ; fail)?\<close>)
unfolding set_endpoint_def set_notification_def set_thread_state_def

148
proof/invariant-abstract/TcbAcc_AI.thy
View File

@ -9,7 +9,7 @@
*)
theory TcbAcc_AI
imports CSpace_AI
imports "./$L4V_ARCH/ArchTcbAcc_AI"
begin
lemmas gts_inv[wp] = get_thread_state_inv
@ -181,10 +181,11 @@ schematic_goal tcb_ipcframe_in_cases:
"(tcb_ipcframe, ?x) \<in> ran tcb_cap_cases"
by (fastforce simp add: ran_tcb_cap_cases)
context begin interpretation ARM . (*FIXME: arch_split*)
lemma valid_ipc_buffer_cap_0[simp]:
"valid_ipc_buffer_cap cap 0"
by (simp add: valid_ipc_buffer_cap_def split: cap.split arch_cap.split)
end
(* FIXME-NTFN: needs assumption for tcb_bound_notification *)
lemma thread_set_valid_objs_triv:
@ -361,7 +362,7 @@ lemma thread_set_valid_reply_masters_trivial:
crunch interrupt_states[wp]: thread_set "\<lambda>s. P (interrupt_states s)"
lemma thread_set_obj_at_impossible:
"\<lbrakk> \<And>tcb. \<not> P (TCB tcb) \<rbrakk> \<Longrightarrow> \<lbrace>obj_at P p\<rbrace> thread_set f t \<lbrace>\<lambda>rv. obj_at P p\<rbrace>"
"\<lbrakk> \<And>tcb. \<not> (P (TCB tcb)) \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. obj_at P p s\<rbrace> thread_set f t \<lbrace>\<lambda>rv. obj_at P p\<rbrace>"
apply (simp add: thread_set_def set_object_def)
apply wp
apply (clarsimp dest!: get_tcb_SomeD)
@ -373,29 +374,9 @@ lemma tcb_not_empty_table:
"\<not> empty_table S (TCB tcb)"
by (simp add: empty_table_def)
lemmas thread_set_arch_caps_trivial
= valid_arch_caps_lift [OF thread_set_vs_lookup_pages thread_set_caps_of_state_trivial
thread_set_arch thread_set_obj_at_impossible,
OF _ tcb_not_empty_table]
lemmas thread_set_valid_globals[wp]
= valid_global_objs_lift [OF thread_set_arch thread_set_arch
valid_ao_at_lift,
OF thread_set_typ_at _ _ thread_set_obj_at_impossible,
simplified, OF _ _ tcb_not_empty_table,
OF thread_set_obj_at_impossible
thread_set_obj_at_impossible, simplified]
crunch v_ker_map[wp]: thread_set "valid_kernel_mappings"
(wp: set_object_v_ker_map crunch_wps)
crunch eq_ker_map[wp]: thread_set "equal_kernel_mappings"
(wp: set_object_equal_mappings crunch_wps ignore: set_object)
= valid_arch_caps_lift_weak[OF thread_set_arch thread_set.aobj_at
thread_set_caps_of_state_trivial, simplified]
lemma thread_set_only_idle:
"\<lbrace>only_idle and K (\<forall>tcb. tcb_state (f tcb) = tcb_state tcb \<or> \<not>idle (tcb_state (f tcb)))\<rbrace>
@ -407,13 +388,6 @@ lemma thread_set_only_idle:
apply force
done
lemma thread_set_global_pd_mappings[wp]:
"\<lbrace>valid_global_pd_mappings\<rbrace>
thread_set f t \<lbrace>\<lambda>rv. valid_global_pd_mappings\<rbrace>"
apply (simp add: thread_set_def)
apply (wp set_object_global_pd_mappings)
apply (clarsimp simp: obj_at_def dest!: get_tcb_SomeD)
done
lemma thread_set_pspace_in_kernel_window[wp]:
"\<lbrace>pspace_in_kernel_window\<rbrace> thread_set f t \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>"
@ -453,17 +427,9 @@ lemma thread_set_valid_ioc_trivial:
split_def tcb_cnode_map_tcb_cap_cases
split: option.splits Structures_A.kernel_object.splits)
apply (drule_tac x="(get,set,ba)" in bspec)
apply fastforce+
apply (fastforce simp: ranI)+
done
lemma thread_set_vms[wp]:
"\<lbrace>valid_machine_state\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
apply (simp add: thread_set_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp add: valid_machine_state_def in_user_frame_def)
apply (drule_tac x=p in spec, clarsimp, rule_tac x=sz in exI)
by (clarsimp simp: get_tcb_def obj_at_def
split: Structures_A.kernel_object.splits)
lemma thread_set_invs_trivial:
assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
@ -884,6 +850,7 @@ lemma as_user_tcb [wp]: "\<lbrace>tcb_at t'\<rbrace> as_user t m \<lbrace>\<lamb
apply simp
done
context begin interpretation ARM . (*FIXME: arch_split*)
lemma mab_pb [simp]:
"msg_align_bits \<le> pageBits"
unfolding msg_align_bits pageBits_def by simp
@ -891,6 +858,7 @@ lemma mab_pb [simp]:
lemma mab_wb [simp]:
"msg_align_bits < word_bits"
unfolding msg_align_bits word_bits_conv by simp
end
lemma take_min_len:
"take (min (length xs) n) xs = take n xs"
@ -936,26 +904,10 @@ lemma fold_fun_upd:
crunch obj_at[wp]: store_word_offs "\<lambda>s. P (obj_at Q p s)"
lemma store_word_offs_in_user_frame[wp]:
"\<lbrace>\<lambda>s. in_user_frame p s\<rbrace> store_word_offs a x w \<lbrace>\<lambda>_ s. in_user_frame p s\<rbrace>"
unfolding in_user_frame_def
by (wp hoare_vcg_ex_lift)
lemma as_user_in_user_frame[wp]:
"\<lbrace>\<lambda>s. in_user_frame p s\<rbrace> as_user t m \<lbrace>\<lambda>_ s. in_user_frame p s\<rbrace>"
unfolding in_user_frame_def
by (wp hoare_vcg_ex_lift)
crunch obj_at[wp]: load_word_offs "\<lambda>s. P (obj_at Q p s)"
lemma load_word_offs_in_user_frame[wp]:
"\<lbrace>\<lambda>s. in_user_frame p s\<rbrace> load_word_offs a x \<lbrace>\<lambda>_ s. in_user_frame p s\<rbrace>"
unfolding in_user_frame_def
by (wp hoare_vcg_ex_lift)
lemma load_word_offs_P[wp]:
"\<lbrace>P\<rbrace> load_word_offs a x \<lbrace>\<lambda>_. P\<rbrace>"
unfolding load_word_offs_def
by (wp dmo_inv loadWord_inv)
lemma valid_tcb_objs:
@ -971,15 +923,7 @@ proof -
thus ?thesis by (simp add: valid_tcb_def valid_obj_def)
qed
lemma vm_sets_diff[simp]:
"vm_read_only \<noteq> vm_read_write"
by (simp add: vm_read_write_def vm_read_only_def)
lemmas vm_sets_diff2[simp] = not_sym[OF vm_sets_diff]
context begin interpretation ARM . (*FIXME: arch_split*)
lemma get_cap_valid_ipc:
"\<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = v) t\<rbrace>
get_cap (t, tcb_cnode_index 4)
@ -992,7 +936,7 @@ lemma get_cap_valid_ipc:
acap_rights_update_def is_tcb
split: cap.split_asm arch_cap.split_asm)
done
end
lemma get_cap_aligned:
"\<lbrace>valid_objs\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. cap_aligned rv\<rbrace>"
@ -1058,7 +1002,7 @@ lemma wf_cs_0:
done
crunch inv[wp]: lookup_ipc_buffer "I"
lemma ct_active_st_tcb_at_weaken:
@ -1428,6 +1372,7 @@ lemma bound_tcb_ex_cap:
unfolding pred_tcb_at_def
by (erule (1) if_live_then_nonz_capD, fastforce)
context begin interpretation ARM . (*FIXME: arch_split*)
lemma pred_tcb_cap_wp_at:
"\<lbrakk>pred_tcb_at proj P t s; valid_objs s;
ref \<in> dom tcb_cap_cases;
@ -1441,6 +1386,7 @@ lemma pred_tcb_cap_wp_at:
apply (erule_tac x="(getF, setF, restr)" in ballE)
apply fastforce+
done
end
lemma st_tcb_reply_cap_valid:
"\<And>P. \<not> P (Structures_A.Inactive) \<and> \<not> P (Structures_A.IdleThreadState) \<Longrightarrow>
@ -1497,39 +1443,6 @@ lemma sbn_obj_at_impossible:
unfolding set_bound_notification_thread_set
by (wp thread_set_obj_at_impossible, simp)
lemmas sts_arch_caps[wp]
= valid_arch_caps_lift [OF sts_vs_lookup_pages set_thread_state_caps_of_state
set_thread_state_arch sts_obj_at_impossible,
OF tcb_not_empty_table]
lemmas sts_valid_globals[wp]
= valid_global_objs_lift [OF set_thread_state_arch set_thread_state_arch
valid_ao_at_lift,
OF set_thread_state_typ_at sts_obj_at_impossible
sts_obj_at_impossible sts_obj_at_impossible,
simplified, OF tcb_not_empty_table]
lemmas sbn_arch_caps[wp]
= valid_arch_caps_lift [OF set_bound_notification_vs_lookup_pages set_bound_notification_caps_of_state
set_bound_notification_arch sbn_obj_at_impossible,
OF tcb_not_empty_table]
lemmas sbn_valid_globals[wp]
= valid_global_objs_lift [OF set_bound_notification_arch set_bound_notification_arch
valid_ao_at_lift,
OF set_bound_notification_typ_at sbn_obj_at_impossible
sbn_obj_at_impossible sbn_obj_at_impossible,
simplified, OF tcb_not_empty_table]
crunch v_ker_map[wp]: set_thread_state, set_bound_notification "valid_kernel_mappings"
(wp: set_object_v_ker_map crunch_wps)
crunch eq_ker_map[wp]: set_thread_state, set_bound_notification "equal_kernel_mappings"
(wp: set_object_equal_mappings crunch_wps ignore: set_object)
lemma sts_only_idle:
"\<lbrace>only_idle and (\<lambda>s. idle st \<longrightarrow> t = idle_thread s)\<rbrace>
@ -1596,16 +1509,6 @@ lemma set_thread_state_valid_ioc[wp]:
done
lemma set_thread_state_vms[wp]:
"\<lbrace>valid_machine_state\<rbrace> set_thread_state t st \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (wp, simp, wp)
apply (clarsimp simp add: valid_machine_state_def in_user_frame_def)
apply (drule_tac x=p in spec, clarsimp, rule_tac x=sz in exI)
apply (clarsimp simp: get_tcb_def obj_at_def
split: Structures_A.kernel_object.splits)
done
lemma set_bound_notification_valid_ioc[wp]:
"\<lbrace>valid_ioc\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_ioc\<rbrace>"
apply (simp add: set_bound_notification_def)
@ -1619,17 +1522,6 @@ lemma set_bound_notification_valid_ioc[wp]:
split_if_asm)
done
lemma set_bound_notification_vms[wp]:
"\<lbrace>valid_machine_state\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
apply (simp add: set_bound_notification_def set_object_def)
apply (wp, simp)
apply (clarsimp simp add: valid_machine_state_def in_user_frame_def)
apply (drule_tac x=p in spec, clarsimp, rule_tac x=sz in exI)
apply (clarsimp simp: get_tcb_def obj_at_def
split: Structures_A.kernel_object.splits)
done
lemma sts_invs_minor:
"\<lbrace>st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t
and (\<lambda>s. \<not> halted st \<longrightarrow> ex_nonz_cap_to t s)
@ -1709,8 +1601,8 @@ lemma sbn_invs_minor:
apply clarsimp
apply (rule conjI)
apply (simp add: pred_tcb_at_def, erule(1) obj_at_valid_objsE)
apply (clarsimp simp: valid_obj_def valid_tcb_def valid_bound_ntfn_def
split: Structures_A.thread_state.splits option.splits)
subgoal by (clarsimp simp: valid_obj_def valid_tcb_def valid_bound_ntfn_def
split: Structures_A.thread_state.splits option.splits)
apply (clarsimp elim!: rsubst[where P=sym_refs]
intro!: ext
dest!: bound_tcb_at_state_refs_ofD)

225
proof/invariant-abstract/VSpacePre_AI.thy Normal file
View File

@ -0,0 +1,225 @@
(*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*)
(*
VSpace refinement
*)
theory VSpacePre_AI
imports TcbAcc_AI
begin
unqualify_facts (in Arch)
cap_master_cap_tcb_cap_valid_arch
lemma throw_on_false_wp[wp]:
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q () s) \<and> (\<not> rv \<longrightarrow> E x s)\<rbrace>
\<Longrightarrow> \<lbrace>P\<rbrace> throw_on_false x f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
apply (simp add: throw_on_false_def unlessE_def)
apply wp
apply simp
done
crunch_ignore (add: throw_on_false)
definition
"is_arch_update cap cap' \<equiv> is_arch_cap cap \<and> cap_master_cap cap = cap_master_cap cap'"
definition
"is_arch_diminished cap cap' \<equiv> is_arch_cap cap \<and> diminished cap cap'"
lemma dmo_asid_map [wp]:
"\<lbrace>valid_asid_map\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_asid_map\<rbrace>"
apply (simp add: do_machine_op_def split_def)
apply wp
apply simp
done
crunch caps_of_state[wp]: do_machine_op "\<lambda>s. P (caps_of_state s)"
interpretation dmo: non_arch_non_cap_op "do_machine_op f"
apply (unfold_locales)
apply wp
done
declare not_Some_eq_tuple[simp]
lemma valid_irq_states_arch_state_update[simp]:
"valid_irq_states (s\<lparr>arch_state := x\<rparr>) = valid_irq_states s"
by(auto simp: valid_irq_states_def)
lemma pull_out_P:
"P s \<and> (\<forall>c. caps_of_state s p = Some c \<longrightarrow> Q s c) \<longrightarrow> (\<forall>c. caps_of_state s p = Some c \<longrightarrow> P s \<and> Q s c)"
by blast
lemma upto_enum_step_subtract:
"x \<le> z \<Longrightarrow> [x, y .e. z] = (map ((op +) x) [0, y - x .e. z - x])"
by (auto simp add: upto_enum_step_def)
(* FIXME: move *)
lemma returnOk_E': "\<lbrace>P\<rbrace> returnOk r -,\<lbrace>E\<rbrace>"
by (clarsimp simp: returnOk_def validE_E_def validE_def valid_def return_def)
lemma throwError_R': "\<lbrace>P\<rbrace> throwError e \<lbrace>Q\<rbrace>,-"
by (clarsimp simp:throwError_def validE_R_def validE_def valid_def return_def)
lemma invs_valid_irq_states[elim!]:
"invs s \<Longrightarrow> valid_irq_states s"
by(auto simp: invs_def valid_state_def)
lemma bool_function_four_cases:
"f = Not \<or> f = id \<or> f = (\<lambda>_. True) \<or> f = (\<lambda>_. False)"
by (auto simp add: fun_eq_iff all_bool_eq)
lemma uint_ucast:
"(x :: ('a :: len) word) < 2 ^ len_of TYPE ('b)
\<Longrightarrow> uint (ucast x :: ('b :: len) word) = uint x"
apply (simp add: ucast_def)
apply (subst word_uint.Abs_inverse)
apply (simp add: uints_num word_less_alt word_le_def)
apply (frule impI[where P="True"])
apply (subst(asm) uint_2p)
apply (clarsimp simp only: word_neq_0_conv[symmetric])
apply simp_all
done
lemma kernel_base_shift_cast_le:
fixes x :: "12 word"
shows
"(kernel_base >> 20 \<le> ucast x) =
(ucast (kernel_base >> 20) \<le> x)"
apply (simp add: word_le_def)
apply (subst uint_ucast, simp,
simp add: kernel_base_def)
apply (simp add: ucast_def)
apply (subst word_uint.Abs_inverse)
apply (cut_tac x=x in word_uint.Rep)
apply (simp add: uints_num)
apply simp
done
(* FIXME: move *)
lemma inj_on_domD: "\<lbrakk>inj_on f (dom f); f x = Some z; f y = Some z\<rbrakk> \<Longrightarrow> x = y"
by (erule inj_onD) clarsimp+
lemma hoare_name_pre_state2:
"(\<And>s. \<lbrace>P and (op = s)\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
by (auto simp: valid_def intro: hoare_name_pre_state)
lemma pd_casting_shifting:
"size x + 2 < len_of TYPE('a) \<Longrightarrow>
ucast (ucast x << 2 >> 2 :: ('a :: len) word) = x"
apply (rule word_eqI)
apply (simp add: nth_ucast nth_shiftr nth_shiftl word_size)
done
lemma aligned_already_mask:
"is_aligned x n \<Longrightarrow> is_aligned (x && msk) n"
apply (simp add: is_aligned_mask word_bw_assocs)
apply (subst word_bw_comms, subst word_bw_assocs[symmetric])
apply simp
done
lemma set_upto_enum_step_4:
"set [0, 4 .e. x :: word32]
= (\<lambda>x. x << 2) ` {.. x >> 2}"
by (auto simp: upto_enum_step_def shiftl_t2n shiftr_div_2n_w
word_size mult.commute)
lemma arch_update_cap_zombies:
"\<lbrace>\<lambda>s. cte_wp_at (is_arch_update cap) p s \<and> zombies_final s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. zombies_final s\<rbrace>"
apply (simp add: zombies_final_def2 cte_wp_at_caps_of_state del: split_paired_All)
apply wp
apply (intro allI impI)
apply (elim conjE exE)
apply (simp del: split_paired_All add: is_arch_update_def split: split_if_asm)
apply (erule_tac x=p in allE)
apply (erule_tac x=p' in allE)
apply simp
apply (frule master_cap_obj_refs)
apply (drule cap_master_cap_zombie)
apply clarsimp
apply (erule_tac x=pa in allE)
apply (erule_tac x=p in allE)
apply simp
apply (frule master_cap_obj_refs)
apply (drule cap_master_cap_zombie)
apply clarsimp
done
lemma arch_update_cap_pspace:
"\<lbrace>cte_wp_at (is_arch_update cap) p and valid_pspace and valid_cap cap\<rbrace>
set_cap cap p
\<lbrace>\<lambda>rv. valid_pspace\<rbrace>"
apply (simp add: valid_pspace_def)
apply (rule hoare_pre)
apply (wp set_cap_valid_objs update_cap_iflive arch_update_cap_zombies)
apply clarsimp
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def)
apply (frule cap_master_cap_zobj_refs)
apply clarsimp
apply (drule caps_of_state_cteD)
apply (drule (1) cte_wp_tcb_cap_valid)
apply (simp add: cap_master_cap_tcb_cap_valid_arch)
done
lemma arch_update_cap_valid_mdb:
"\<lbrace>cte_wp_at (is_arch_update cap) p and valid_mdb\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_mdb\<rbrace>"
apply (simp add: valid_mdb_def2 pred_conj_def)
apply (rule hoare_lift_Pf2 [where f=cdt])
prefer 2
apply wp[1]
apply (rule hoare_lift_Pf2 [where f=is_original_cap])
prefer 2
apply wp[1]
apply (rule hoare_pre)
apply wp
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (rule conjI)
apply (clarsimp simp: mdb_cte_at_def is_arch_update_def)
apply (fastforce simp: is_cap_simps)
apply (rule conjI)
apply (clarsimp simp: untyped_mdb_def is_arch_update_def)
apply (rule conjI)
apply (fastforce simp: is_cap_simps)
apply clarsimp
apply (drule master_cap_obj_refs)
apply fastforce
apply (rule conjI)
apply (erule(1) descendants_inc_minor)
apply (clarsimp simp:is_arch_update_def)
apply (frule master_cap_class)
apply (clarsimp dest!:master_cap_cap_range)
apply (rule conjI)
apply (clarsimp simp: untyped_inc_def is_arch_update_def)
subgoal by (fastforce simp: is_cap_simps)
apply (rule conjI)
apply (clarsimp simp: ut_revocable_def)
apply (clarsimp simp: is_arch_update_def is_cap_simps)
apply (rule conjI)
apply (clarsimp simp: irq_revocable_def is_arch_update_def is_cap_simps simp del: split_paired_All)
apply (rule conjI)
apply (clarsimp simp: reply_master_revocable_def is_arch_update_def is_cap_simps)
apply (clarsimp simp: reply_mdb_def is_arch_update_def)
apply (rule conjI)
apply (clarsimp simp: reply_caps_mdb_def is_cap_simps cap_master_cap_def
simp del: split_paired_Ex split_paired_All)
apply (fastforce elim!: exEI)
by (clarsimp simp: is_cap_simps cap_master_cap_def reply_masters_mdb_def)
lemma set_cap_arch_obj:
"\<lbrace>ko_at (ArchObj ao) p and cte_at p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>_. ko_at (ArchObj ao) p\<rbrace>"
apply (wp set_cap_obj_at_other)
apply (clarsimp simp: obj_at_def cte_wp_at_cases)
done
end

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

File diff suppressed because it is too large Load Diff