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

x64 ainvs: update for new definition of set_object 

Removed update_object, which does the same thing as the new version of
set_object, and replaced it with set_object.

x64 ainvs: update for new definition of set_object

Rename legacy update_object definitions to set_object definitions and
remove related lemmas (to move up into architecture generic
KHeap_AI.thy). Remove simpler_defs as the set_object definitions are now
equivalent.

x64 ainvs: move x64 specific lemma back to ArchKHeap_AI

set_aobject_valid_arch move back after confirmation with Matt Brecknell
that it is x64 specific

x64 ainvs: update for new definition of set_object

Fixed some proofs a result of removing set_arch_obj_simps from the simp
set.
This commit is contained in:
Victor Phan 2019-04-04 14:42:50 +11:00
parent 71b6cfccef
commit e9449ee263
13 changed files with 346 additions and 572 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

564
proof/invariant-abstract/X64/ArchAcc_AI.thy
View File

@ -30,70 +30,7 @@ bundle unfold_objects_asm =
kernel_object.split_asm[split]
arch_kernel_obj.split_asm[split]
definition
"update_object ptr obj = do
kobj <- get_object ptr;
assert (a_type kobj = a_type obj);
set_object ptr obj
od "
lemma set_pd_simpler_def:
"set_pd ptr pd = update_object ptr (ArchObj (PageDirectory pd))"
apply (simp add: set_pd_def update_object_def)
apply (rule bind_eqI)
apply (rule ext)
apply (rule NonDetMonadVCG.bind_eqI)
apply (rule arg_cong)
apply (clarsimp simp: a_type_def split:kernel_object.splits arch_kernel_obj.splits)
apply simp
done
lemma set_pt_simpler_def:
"set_pt ptr pt = update_object ptr (ArchObj (PageTable pt))"
apply (simp add: set_pt_def update_object_def)
apply (rule bind_eqI)
apply (rule ext)
apply (rule NonDetMonadVCG.bind_eqI)
apply (rule arg_cong)
apply (clarsimp simp: a_type_def split:kernel_object.splits arch_kernel_obj.splits)
apply simp
done
lemma set_pml4_simpler_def:
"set_pml4 ptr pml4 = update_object ptr (ArchObj (PageMapL4 pml4))"
apply (simp add: set_pml4_def update_object_def)
apply (rule bind_eqI)
apply (rule ext)
apply (rule NonDetMonadVCG.bind_eqI)
apply (rule arg_cong)
apply (clarsimp simp: a_type_def split:kernel_object.splits arch_kernel_obj.splits)
apply simp
done
lemma set_asid_pool_simpler_def:
"set_asid_pool ptr pool = update_object ptr (ArchObj (ASIDPool pool))"
apply (simp add: set_asid_pool_def update_object_def)
apply (rule bind_eqI)
apply (rule ext)
apply (rule NonDetMonadVCG.bind_eqI)
apply (rule arg_cong)
apply (clarsimp simp: a_type_def split:kernel_object.splits arch_kernel_obj.splits)
apply simp
done
lemma set_pdpt_simpler_def:
"set_pdpt ptr pdpt = update_object ptr (ArchObj (PDPointerTable pdpt))"
apply (simp add: set_pdpt_def update_object_def)
apply (rule bind_eqI)
apply (rule ext)
apply (rule NonDetMonadVCG.bind_eqI)
apply (rule arg_cong)
apply (clarsimp simp: a_type_def split:kernel_object.splits arch_kernel_obj.splits)
apply simp
done
lemmas set_arch_obj_simps[simp] = set_pml4_simpler_def set_pt_simpler_def set_pdpt_simpler_def
set_pd_simpler_def set_asid_pool_simpler_def
lemmas set_arch_obj_simps = set_pml4_def set_pt_def set_pdpt_def set_pd_def set_asid_pool_def
(* None generic proofs for get arch objects *)
@ -163,7 +100,7 @@ lemma get_pde_inv [wp]: "\<lbrace>P\<rbrace> get_pde p \<lbrace>\<lambda>_. P\<r
lemma set_asid_pool_typ_at [wp]:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def get_object_def update_object_def)
apply (simp add: set_asid_pool_def set_object_def get_object_def set_object_def)
apply wp
including unfold_objects
by clarsimp
@ -193,8 +130,8 @@ lemma set_asid_pool_iflive [wp]:
"\<lbrace>\<lambda>s. if_live_then_nonz_cap s\<rbrace>
set_asid_pool p ap
\<lbrace>\<lambda>_ s. if_live_then_nonz_cap s\<rbrace>"
apply (simp add: update_object_def)
apply (wp get_object_wp set_object_iflive)
apply (simp add: set_asid_pool_def)
apply (wp set_object_iflive[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: a_type_def obj_at_def live_def hyp_live_def
split: kernel_object.splits arch_kernel_obj.splits)
done
@ -203,17 +140,16 @@ lemma set_asid_pool_zombies [wp]:
"\<lbrace>\<lambda>s. zombies_final s\<rbrace>
set_asid_pool p ap
\<lbrace>\<lambda>_ s. zombies_final s\<rbrace>"
apply (simp add: set_asid_pool_def update_object_def)
apply (wp get_object_wp set_object_zombies)
apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits)
apply (clarsimp simp: obj_at_def a_type_simps)
apply (simp add: set_asid_pool_def)
including unfold_objects
apply (wpsimp wp: set_object_zombies[THEN hoare_set_object_weaken_pre] simp: a_type_def)
done
lemma set_asid_pool_zombies_state_refs [wp]:
"\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
set_asid_pool p ap
\<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace>"
apply (clarsimp simp: set_asid_pool_def set_object_def update_object_def)
apply (clarsimp simp: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits)
apply (erule rsubst [where P=P])
@ -230,12 +166,13 @@ lemma set_asid_pool_cdt [wp]:
lemma set_asid_pool_caps_of_state [wp]:
"\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
unfolding set_asid_pool_def set_object_def including unfold_objects
apply (wpsimp wp: get_object_wp)
unfolding set_asid_pool_def including unfold_objects
apply (wpsimp wp: set_object_wp_strong simp: a_type_def)
apply (subst cte_wp_caps_of_lift)
prefer 2
apply assumption
subgoal for _ _ y by (cases y, auto simp: cte_wp_at_cases)
subgoal for _ _ y apply (cases y, auto simp: cte_wp_at_cases)
done
done
lemma set_asid_pool_valid_mdb [wp]:
@ -243,8 +180,7 @@ lemma set_asid_pool_valid_mdb [wp]:
set_asid_pool p ap
\<lbrace>\<lambda>_ s. valid_mdb s\<rbrace>"
including unfold_objects
by (wpsimp wp: valid_mdb_lift get_object_wp
simp: set_asid_pool_def update_object_def set_object_def)
by (wpsimp wp: valid_mdb_lift simp: set_asid_pool_def set_object_def get_object_def)
lemma set_asid_pool_reply_masters [wp]:
@ -355,231 +291,48 @@ crunch cte_wp_at[wp]: set_irq_state "\<lambda>s. P (cte_wp_at P' p s)"
(* Generic lemmas about update arch object *)
lemma update_object_typ_at [wp]:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> update_object ptr obj \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>"
apply (simp add: update_object_def get_object_def set_object_def)
apply (wp)
apply (clarsimp simp: obj_at_def)
done
lemmas update_object_typ_ats [wp] = abs_typ_at_lifts [OF update_object_typ_at]
lemma update_object_valid_objs:
"\<lbrace>(%s. valid_obj ptr (ArchObj aobj) s) and valid_objs\<rbrace>
update_object ptr (ArchObj aobj)
\<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (simp add: update_object_def)
apply (wp get_object_wp set_object_valid_objs)
including unfold_objects
apply (clarsimp simp: arch_valid_obj_def a_type_def valid_obj_def)
done
lemma update_object_iflive[wp]:
lemma set_object_iflive[wp]:
"\<lbrace>\<lambda>s. if_live_then_nonz_cap s\<rbrace>
update_object ptr (ArchObj aobj)
set_object ptr (ArchObj aobj)
\<lbrace>\<lambda>_ s. if_live_then_nonz_cap s\<rbrace>"
apply (simp add: update_object_def)
apply (wp get_object_wp set_object_iflive)
apply (wp set_object_iflive[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: a_type_def obj_at_def live_def hyp_live_def
split: kernel_object.splits arch_kernel_obj.splits)
done
lemma typ_at_pspace_aligned:
assumes type_invs: "\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>_. typ_at T p\<rbrace>"
assumes dom_shrink: "\<And>x. \<lbrace>\<lambda>s. x \<notin> dom (kheap s)\<rbrace> f \<lbrace>\<lambda>_ s. x \<notin> dom (kheap s)\<rbrace>"
shows "\<lbrace>pspace_aligned\<rbrace> f \<lbrace>\<lambda>_. pspace_aligned\<rbrace>"
apply (clarsimp simp: valid_def pspace_aligned_def)
apply (drule_tac x = x in bspec)
subgoal indom
apply (rule ccontr)
apply (drule(1) use_valid[OF _ dom_shrink])
apply force
done
apply (frule(1) indom)
apply (clarsimp simp: dom_def obj_bits_T)
apply (drule use_valid[OF _ type_invs])
apply (simp add: obj_at_def)
apply (intro exI conjI, simp+)
apply (simp add: obj_at_def)
done
lemmas update_obj_typ_at[wp] = update_object_typ_at[where P="\<lambda>x. x"]
lemma update_obj_dom_shrink[wp]:
"\<lbrace>\<lambda>s. p \<notin> dom (kheap s) \<rbrace> update_object pt obj \<lbrace>\<lambda>_ s. p \<notin> dom (kheap s)\<rbrace>"
apply (wp set_object_typ_at get_object_wp | simp add: update_object_def set_object_def)+
apply (clarsimp simp: obj_at_def split: if_split_asm)
done
lemma update_obj_pspace_aligned[wp]:
"\<lbrace>pspace_aligned\<rbrace> update_object ptr obj \<lbrace>\<lambda>_. pspace_aligned\<rbrace>"
by (wp typ_at_pspace_aligned)
lemma update_obj_pspace_distinct[wp]:
"\<lbrace>pspace_distinct\<rbrace> update_object ptr obj \<lbrace>\<lambda>_. pspace_distinct\<rbrace>"
apply (simp add: update_object_def)
apply (wp set_object_distinct get_object_wp)
apply (clarsimp simp: obj_at_def)
done
lemma update_aobj_zombies[wp]:
"\<lbrace>\<lambda>s. zombies_final s\<rbrace>
update_object ptr (ArchObj obj)
\<lbrace>\<lambda>_ s. zombies_final s\<rbrace>"
apply (simp add: update_object_def)
apply (wp get_object_wp set_object_zombies)
apply (clarsimp simp: obj_at_def same_caps_def a_type_def
split: kernel_object.split_asm if_split_asm)
done
lemma update_aobj_state_refs[wp]:
"\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
update_object p (ArchObj obj)
\<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace>"
apply (clarsimp simp: update_object_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def a_type_def split: kernel_object.split_asm if_split_asm)
apply (erule rsubst [where P=P])
apply (rule ext)
by (clarsimp simp: state_refs_of_def split: option.splits)
lemma update_aobj_cdt[wp]:
"\<lbrace>\<lambda>s. P (cdt s)\<rbrace>
update_object ptr (ArchObj obj)
\<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>"
apply (clarsimp simp: update_object_def)
apply (wp get_object_wp)
apply simp
done
lemma update_aobj_caps_of_state [wp]:
"\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> update_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
apply (simp add: update_object_def get_object_def bind_assoc set_object_def)
apply wp
apply clarsimp
apply (subst cte_wp_caps_of_lift)
prefer 2
apply assumption
subgoal for _ y
by (cases y, auto simp: cte_wp_at_cases a_type_def)
done
lemma update_aobj_cte_wp_at:
"\<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace>
update_object ptr (ArchObj obj)
\<lbrace>\<lambda>rv s. P (cte_wp_at P' p s)\<rbrace>"
apply (simp add: cte_wp_at_caps_of_state)
apply wp
done
lemma update_object_is_original_cap[wp]:
"\<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> update_object a b
\<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace>"
by (wpsimp wp: get_object_wp simp: update_object_def set_object_def)
lemma update_aobj_valid_mdb[wp]:
"\<lbrace>\<lambda>s. valid_mdb s\<rbrace>
update_object ptr (ArchObj obj)
\<lbrace>\<lambda>_ s. valid_mdb s\<rbrace>"
apply (rule valid_mdb_lift)
apply (wp update_aobj_cdt)
apply (clarsimp simp: update_object_def)
apply (wp get_object_wp | simp)+
done
lemma update_aobj_pred_tcb_at[wp]:
"\<lbrace>pred_tcb_at proj P t\<rbrace> update_object ptr (ArchObj obj) \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>"
apply (simp add: update_object_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: pred_tcb_at_def obj_at_def a_type_def)
done
lemma update_object_cur_thread [wp]:
"\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> update_object ptr obj \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>"
unfolding update_object_def by (wp get_object_wp) simp
lemma update_aobj_cur_tcb [wp]:
"\<lbrace>\<lambda>s. cur_tcb s\<rbrace> update_object ptr (ArchObj obj) \<lbrace>\<lambda>_ s. cur_tcb s\<rbrace>"
unfolding cur_tcb_def
by (rule hoare_lift_Pf [where f=cur_thread]) wp+
crunch arch [wp]: update_object "\<lambda>s. P (arch_state s)"
(wp: get_object_wp)
lemma update_aobj_valid_arch [wp]:
"\<lbrace>valid_arch_state\<rbrace> update_object ptr (ArchObj obj) \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
by (wp valid_arch_state_lift)
lemma update_aobj_valid_objs [wp]:
"\<lbrace>valid_objs and arch_valid_obj obj\<rbrace> update_object ptr (ArchObj obj) \<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (simp add: update_object_def)
apply (wp set_object_valid_objs get_object_wp)
apply (clarsimp simp: a_type_def split: kernel_object.split_asm if_split_asm)
(* lemma set_aobject_valid_objs [wp]:
"\<lbrace>valid_objs and arch_valid_obj obj\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (wpsimp wp: set_object_valid_objs[THEN hoare_set_object_weaken_pre]
simp: a_type_def)
including unfold_objects
by (clarsimp simp: a_type_def valid_obj_def arch_valid_obj_def)
by (clarsimp simp: a_type_def valid_obj_def arch_valid_obj_def) *)
lemma update_aobj_valid_idle[wp]:
"\<lbrace>\<lambda>s. valid_idle s\<rbrace>
update_object ptr (ArchObj obj)
\<lbrace>\<lambda>_ s. valid_idle s\<rbrace>"
apply (wpsimp simp: update_object_def wp: get_object_wp valid_idle_lift)
done
lemma update_aobj_ifunsafe[wp]:
lemma set_aobject_ifunsafe[wp]:
"\<lbrace>\<lambda>s. if_unsafe_then_cap s\<rbrace>
update_object ptr (ArchObj obj)
set_object ptr (ArchObj obj)
\<lbrace>\<lambda>_ s. if_unsafe_then_cap s\<rbrace>"
apply (simp add: update_object_def)
apply (wp get_object_wp set_object_ifunsafe)
including unfold_objects
by (clarsimp simp: a_type_def)
lemma update_aobj_reply_caps[wp]:
"\<lbrace>\<lambda>s. valid_reply_caps s\<rbrace>
update_object ptr (ArchObj obj)
\<lbrace>\<lambda>_ s. valid_reply_caps s\<rbrace>"
by (wp valid_reply_caps_st_cte_lift)
lemma update_aobj_reply_masters[wp]:
"\<lbrace>valid_reply_masters\<rbrace>
update_object ptr (ArchObj obj)
\<lbrace>\<lambda>_. valid_reply_masters\<rbrace>"
by (wp valid_reply_masters_cte_lift)
by (wpsimp wp: set_object_ifunsafe[THEN hoare_set_object_weaken_pre]
simp: a_type_def)
lemma global_refs_kheap [simp]:
"global_refs (kheap_update f s) = global_refs s"
by (simp add: global_refs_def)
crunch global_ref [wp]: update_object "\<lambda>s. P (global_refs s)"
crunch global_ref [wp]: set_object "\<lambda>s. P (global_refs s)"
(wp: crunch_wps)
crunch arch [wp]: update_object "\<lambda>s. P (arch_state s)"
(wp: crunch_wps)
crunch idle [wp]: update_object "\<lambda>s. P (idle_thread s)"
(wp: crunch_wps)
crunch irq [wp]: update_object "\<lambda>s. P (interrupt_irq_node s)"
(wp: crunch_wps)
crunch interrupt_states[wp]: update_object "\<lambda>s. P (interrupt_states s)"
(wp: crunch_wps)
lemma update_aobj_valid_global[wp]:
lemma set_aobj_valid_global[wp]:
"\<lbrace>\<lambda>s. valid_global_refs s\<rbrace>
update_object ptr (ArchObj obj)
set_object ptr (ArchObj obj)
\<lbrace>\<lambda>_ s. valid_global_refs s\<rbrace>"
by (wp valid_global_refs_cte_lift)
lemma update_aobj_valid_kernel_mappings[wp]:
lemma set_aobj_valid_kernel_mappings[wp]:
"\<lbrace>\<lambda>s. valid_kernel_mappings s \<and> valid_kernel_mappings_if_pm (set (second_level_tables (arch_state s))) (ArchObj obj)\<rbrace>
update_object ptr (ArchObj obj)
set_object ptr (ArchObj obj)
\<lbrace>\<lambda>_ s. valid_kernel_mappings s\<rbrace>"
apply (simp add: update_object_def)
apply_trace (wp set_object_v_ker_map get_object_wp)
apply (wp set_object_v_ker_map[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: valid_kernel_mappings_def valid_kernel_mappings_if_pm_def)
done
@ -661,21 +414,21 @@ lemma a_type_of_ArchObj:
"a_type (ArchObj ako) = AArch (aa_type ako)"
by (simp add: a_type_def aa_type_def split: kernel_object.split_asm)
lemma update_object_is_kheap_upd:
assumes wp: "\<lbrace>preR\<rbrace> update_object ptr (ArchObj aobj) \<lbrace>\<lambda>rv. R \<rbrace>"
lemma set_object_is_kheap_upd:
assumes wp: "\<lbrace>preR\<rbrace> set_object ptr (ArchObj aobj) \<lbrace>\<lambda>rv. R \<rbrace>"
shows "\<lbrakk>preR s; kheap s ptr = Some obj; a_type obj = AArch (aa_type aobj) \<rbrakk> \<Longrightarrow> R (s\<lparr>kheap := \<lambda>x. if x = ptr then Some (ArchObj aobj) else kheap s x\<rparr>)"
apply (rule use_valid[OF _ wp, where s = s])
apply (simp add: fun_upd_def update_object_def get_object_def assert_def a_type_simps a_type_of_ArchObj
set_object_def bind_def get_def gets_def return_def put_def fail_def)
apply (simp add: fun_upd_def set_object_def get_object_def assert_def a_type_simps a_type_of_ArchObj
bind_def get_def gets_def return_def put_def fail_def)
apply simp
done
lemma set_pt_global_objs [wp]:
"\<lbrace>valid_global_objs and valid_arch_state
and (\<lambda>s. valid_global_objs_upd ptr obj (arch_state s))\<rbrace>
update_object ptr (ArchObj obj)
set_object ptr (ArchObj obj)
\<lbrace>\<lambda>rv. valid_global_objs\<rbrace>"
apply (clarsimp simp: update_object_def set_object_def valid_global_objs_def
apply (clarsimp simp: set_object_def valid_global_objs_def
second_level_tables_def)
apply (wp get_object_wp)
apply clarsimp
@ -686,7 +439,7 @@ lemma set_pt_global_objs [wp]:
apply (clarsimp dest!: a_type_is_aobj aa_type_pml4D
simp: valid_arch_state_def aa_type_simps
valid_global_objs_upd_def obj_at_def)
apply (rule update_object_is_kheap_upd[OF valid_pml4e_lift])
apply (rule set_object_is_kheap_upd[OF valid_pml4e_lift])
apply (wp | clarsimp | rule conjI | assumption)+
apply (drule_tac x = x in bspec, simp+)
apply (simp add: empty_table_def)
@ -707,10 +460,10 @@ lemma set_pt_global_objs [wp]:
done
(* It is a pity that the following lemmas can not be abstract into a form with update_object *)
(* It is a pity that the following lemmas can not be abstract into a form with set_object *)
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 (simp add: store_pte_def set_pt_def)
apply wp
apply (clarsimp simp: obj_at_def a_type_def)
done
@ -1376,29 +1129,47 @@ lemma page_table_pte_at_lookupI:
lemma store_pte_valid_objs [wp]:
"\<lbrace>(%s. wellformed_pte pte) and valid_objs\<rbrace> store_pte p pte \<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (simp add: store_pte_def get_pt_def bind_assoc set_object_def get_object_def)
apply (simp add: store_pte_def set_pt_def get_pt_def bind_assoc set_object_def get_object_def)
apply (rule hoare_pre)
apply (wp|wpc)+
apply (clarsimp simp: valid_objs_def dom_def simp del: fun_upd_apply)
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def arch_valid_obj_def)
subgoal for \<dots> ptr _
apply (rule valid_obj_same_type)
apply (cases "ptr = p && ~~ mask pt_bits")
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def arch_valid_obj_def)
apply clarsimp
apply fastforce
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def arch_valid_obj_def)
apply assumption
by (simp add: a_type_def)
done
lemma store_pde_valid_objs [wp]:
"\<lbrace>(%s. wellformed_pde pde) and valid_objs\<rbrace> store_pde p pde \<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (simp add: store_pde_def get_pd_def bind_assoc set_object_def get_object_def)
apply (simp add: store_pde_def set_pd_def get_pd_def bind_assoc set_object_def get_object_def)
apply (rule hoare_pre)
apply (wp|wpc)+
apply (clarsimp simp: valid_objs_def dom_def simp del: fun_upd_apply)
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def arch_valid_obj_def)
subgoal for \<dots> ptr _
apply (rule valid_obj_same_type)
apply (cases "ptr = p && ~~ mask pd_bits")
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def arch_valid_obj_def)
apply clarsimp
apply fastforce
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def arch_valid_obj_def)
apply assumption
by (simp add: a_type_def)
done
lemma store_pdpte_valid_objs [wp]:
"\<lbrace>(%s. wellformed_pdpte pdpte) and valid_objs\<rbrace> store_pdpte p pdpte \<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (simp add: store_pdpte_def get_pdpt_def bind_assoc set_object_def get_object_def)
"\<lbrace>valid_objs and (%s. wellformed_pdpte pdpte)\<rbrace> store_pdpte p pdpte \<lbrace>\<lambda>_. valid_objs\<rbrace>"
apply (simp add: store_pdpte_def set_pdpt_def get_pdpt_def bind_assoc get_object_def)
apply (rule hoare_pre)
apply (wp|wpc)+
apply (wp set_object_valid_objs | wpc)+
apply (clarsimp simp: valid_objs_def dom_def simp del: fun_upd_apply)
apply (erule allE, erule impE, blast)
apply (clarsimp simp: valid_obj_def arch_valid_obj_def)
@ -1406,19 +1177,19 @@ lemma store_pdpte_valid_objs [wp]:
lemma store_pml4e_arch [wp]:
"\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> store_pml4e p pml4e \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
by (simp add: store_pml4e_def | wp)+
by (simp add: store_pml4e_def set_arch_obj_simps | wp)+
lemma store_pdpte_arch [wp]:
"\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> store_pdpte p pdpte \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
by (simp add: store_pdpte_def | wp)+
by (simp add: store_pdpte_def set_arch_obj_simps | wp)+
lemma store_pde_arch [wp]:
"\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> store_pde p pde \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
by (simp add: store_pde_def | wp)+
by (simp add: store_pde_def set_arch_obj_simps | wp)+
lemma store_pte_arch [wp]:
"\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> store_pte p pte \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
apply (simp add: store_pte_def | wp)+
apply (simp add: store_pte_def set_arch_obj_simps | wp)+
done
lemma store_pte_valid_pte [wp]:
@ -1427,84 +1198,78 @@ lemma store_pte_valid_pte [wp]:
lemma store_pde_valid_pde [wp]:
"\<lbrace>valid_pde pde\<rbrace> store_pde slot pde' \<lbrace>\<lambda>rv. valid_pde pde\<rbrace>"
by (wp valid_pde_lift | simp add: store_pde_def)+
by (wp valid_pde_lift | simp add: store_pde_def set_arch_obj_simps)+
lemma store_pdpte_valid_pdpte [wp]:
"\<lbrace>valid_pdpte pdpte\<rbrace> store_pdpte slot pdpte' \<lbrace>\<lambda>rv. valid_pdpte pdpte\<rbrace>"
by (wp valid_pdpte_lift | simp add: store_pdpte_def)+
by (wp valid_pdpte_lift | simp add: store_pdpte_def set_arch_obj_simps)+
lemma store_pml4e_valid_pml4e [wp]:
"\<lbrace>valid_pml4e pml4e\<rbrace> store_pml4e slot pml4e' \<lbrace>\<lambda>rv. valid_pml4e pml4e\<rbrace>"
by (wp valid_pml4e_lift | simp add: store_pml4e_def)+
by (wp valid_pml4e_lift | simp add: store_pml4e_def set_arch_obj_simps)+
lemma decrease_predictI:
assumes decrease: "\<And>A B. A\<subseteq>B \<Longrightarrow> P A \<Longrightarrow> P B"
shows "\<lbrakk>A \<subseteq> B; P A \<rbrakk> \<Longrightarrow> P B"
by (auto simp: decrease)
lemma update_aobj_kernel_window[wp]:
"\<lbrace>pspace_in_kernel_window\<rbrace> update_object p (ArchObj obj) \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>"
apply (simp add: update_object_def)
apply (wp set_object_pspace_in_kernel_window get_object_wp)
lemma set_aobj_kernel_window[wp]:
"\<lbrace>pspace_in_kernel_window\<rbrace> set_object p (ArchObj obj) \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>"
apply (wp set_object_pspace_in_kernel_window[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: obj_at_def a_type_def
split: kernel_object.split_asm
arch_kernel_obj.split_asm)
done
lemma update_aobj_valid_global_vspace_mappings[wp]:
lemma set_aobj_valid_global_vspace_mappings[wp]:
"\<lbrace>\<lambda>s. valid_global_vspace_mappings s \<and> valid_global_objs s \<and> (aa_type obj \<noteq> AASIDPool \<longrightarrow> p \<notin> global_refs s)\<rbrace>
update_object p (ArchObj obj)
set_object p (ArchObj obj)
\<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>"
apply (simp add: update_object_def)
apply (wp set_object_global_vspace_mappings get_object_wp)
apply (wp set_object_global_vspace_mappings[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: obj_at_def a_type_def aa_type_def
split: kernel_object.split_asm
arch_kernel_obj.split_asm)
done
lemma update_aobj_valid_ioc[wp]:
"\<lbrace>valid_ioc\<rbrace> update_object p (ArchObj obj) \<lbrace>\<lambda>_. valid_ioc\<rbrace>"
apply (simp add: update_object_def)
apply (wp set_object_valid_ioc_no_caps get_object_wp)
lemma set_aobj_valid_ioc[wp]:
"\<lbrace>valid_ioc\<rbrace> set_object p (ArchObj obj) \<lbrace>\<lambda>_. valid_ioc\<rbrace>"
apply (wp set_object_valid_ioc_no_caps[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: a_type_simps obj_at_def is_tcb is_cap_table
split: kernel_object.splits arch_kernel_obj.splits)
split: kernel_object.splits arch_kernel_obj.splits)
done
lemma update_aobj_only_idle [wp]:
"\<lbrace>only_idle\<rbrace> update_object p (ArchObj aobj) \<lbrace>\<lambda>_. only_idle\<rbrace>"
lemma set_aobj_only_idle [wp]:
"\<lbrace>only_idle\<rbrace> set_object p (ArchObj aobj) \<lbrace>\<lambda>_. only_idle\<rbrace>"
by (wp only_idle_lift)
lemma update_aobj_equal_mappings [wp]:
lemma set_aobj_equal_mappings [wp]:
"\<lbrace>equal_kernel_mappings and
(\<lambda>s. obj_at (\<lambda>ko. (case aobj of (PageMapL4 pm) \<Rightarrow> (\<exists>pm'. ko = (ArchObj (PageMapL4 pm'))
\<and> (\<forall>x \<in> kernel_mapping_slots. pm x = pm' x)) | _ \<Rightarrow> True)) p s)
\<rbrace> update_object p (ArchObj aobj) \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>"
apply (simp add: update_object_def | wp set_object_equal_mappings get_object_wp)+
\<rbrace> set_object p (ArchObj aobj) \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>"
apply (wp set_object_equal_mappings[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: equal_kernel_mappings_def obj_at_def a_type_simps)
done
lemma update_aobj_respects_device_region[wp]:
"\<lbrace>pspace_respects_device_region\<rbrace> update_object p (ArchObj aobj) \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>"
apply (simp add: update_object_def)
apply (wp set_object_pspace_respects_device_region get_object_wp)
lemma set_aobj_respects_device_region[wp]:
"\<lbrace>pspace_respects_device_region\<rbrace> set_object p (ArchObj aobj) \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>"
apply (wp set_object_pspace_respects_device_region[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: obj_at_def a_type_def
split: Structures_A.kernel_object.split_asm
arch_kernel_obj.split_asm)
done
lemma update_aobj_caps_in_kernel_window[wp]:
"\<lbrace>cap_refs_in_kernel_window\<rbrace> update_object p (ArchObj aobj) \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>"
apply (simp add: update_object_def)
apply (wp set_object_cap_refs_in_kernel_window get_object_wp)
lemma set_aobj_caps_in_kernel_window[wp]:
"\<lbrace>cap_refs_in_kernel_window\<rbrace> set_object p (ArchObj aobj) \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>"
apply (wp set_object_cap_refs_in_kernel_window[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: obj_at_def a_type_def
split: kernel_object.split_asm if_splits
arch_kernel_obj.split_asm)
done
lemma update_aobj_caps_respects_device_region[wp]:
"\<lbrace>cap_refs_respects_device_region\<rbrace> update_object p (ArchObj aobj) \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>"
apply (simp add: update_object_def)
apply (wp set_object_cap_refs_respects_device_region get_object_wp)
lemma set_aobj_caps_respects_device_region[wp]:
"\<lbrace>cap_refs_respects_device_region\<rbrace> set_object p (ArchObj aobj) \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>"
apply (wp set_object_cap_refs_respects_device_region[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: obj_at_def a_type_def
split: Structures_A.kernel_object.split_asm if_splits
arch_kernel_obj.split_asm)
@ -1544,9 +1309,9 @@ shows
done
done
lemma update_aobj_vms[wp]:
"\<lbrace>valid_machine_state\<rbrace> update_object p (ArchObj obj) \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
apply (simp add: update_object_def set_object_def)
lemma set_aobj_vms[wp]:
"\<lbrace>valid_machine_state\<rbrace> set_object p (ArchObj obj) \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
apply (simp add: set_object_def)
apply (wp get_object_wp)
apply clarify
apply (erule valid_machine_state_heap_updI)
@ -1569,9 +1334,7 @@ lemma set_object_caps_of_state:
(\<lambda>s. P (caps_of_state s))\<rbrace>
set_object p obj
\<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
apply (clarsimp simp: set_object_def)
apply wp
apply clarify
apply (wpsimp wp: set_object_wp)
apply (erule rsubst[where P=P])
apply (rule ext)
apply (simp add: caps_of_state_cte_wp_at obj_at_def is_cap_table_def
@ -1639,15 +1402,15 @@ lemma a_type_of_arch:
"a_type (ArchObj aobj) = AArch (aa_type aobj)"
by (simp add: a_type_def aa_type_def)
lemma update_objects_caps [wp]:
lemma set_objects_caps [wp]:
"\<lbrace>valid_table_caps and
(\<lambda>s. typ_at (AArch (aa_type aobj)) p s \<longrightarrow> valid_table_caps_aobj (caps_of_state s) (arch_state s) (ArchObj aobj) p)\<rbrace>
update_object p (ArchObj aobj)
set_object p (ArchObj aobj)
\<lbrace>\<lambda>rv. valid_table_caps\<rbrace>"
apply (clarsimp simp: valid_table_caps_def)
apply (rule hoare_pre)
apply (wps update_aobj_caps_of_state)
apply (clarsimp simp: update_object_def set_object_def)
apply (wps set_object_caps_of_state)
apply (clarsimp simp: set_object_def)
apply (wp get_object_wp)
apply clarsimp
apply (case_tac "r \<noteq> p")
@ -1697,7 +1460,7 @@ lemma valid_vspace_obj_kheap_upd:
apply (clarsimp simp: a_type_simps)+
done
lemma update_object_valid_vspace_objs[wp]:
lemma set_object_valid_vspace_objs[wp]:
"\<lbrace> \<lambda>s. valid_vspace_objs s
(* Lattice Preserving *)
@ -1713,11 +1476,11 @@ lemma update_object_valid_vspace_objs[wp]:
\<in> lookupable_refs (vs_lookup1 s) {ref. (ref \<rhd> ptr) s}
(refs_diff vs_lookup1_on_heap_obj obj ptr s))
\<longrightarrow> valid_vspace_obj pobj s)\<rbrace>
update_object ptr (ArchObj obj)
set_object ptr (ArchObj obj)
\<lbrace> \<lambda>_. valid_vspace_objs \<rbrace>"
unfolding refs_diff_def
apply (rule hoare_pre)
apply (clarsimp simp: update_object_def set_object_def)
apply (clarsimp simp: set_object_def)
apply (wp get_object_wp)
apply (subst valid_vspace_objs_def)
apply (clarsimp simp: vs_lookup_def del:ImageE)
@ -1762,7 +1525,7 @@ lemma valid_vs_lookup_fullD:
\<and> (\<exists>slot cap. caps_of_state s slot = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)"
by (simp add: valid_vs_lookup_def)
lemma update_object_valid_vs_lookup[wp]:
lemma set_object_valid_vs_lookup[wp]:
"\<lbrace> \<lambda>s. valid_vspace_objs s \<and> valid_vs_lookup s \<and> valid_asid_table (x64_asid_table (arch_state s)) s
(* Lattice Preserving *)
@ -1778,11 +1541,11 @@ lemma update_object_valid_vs_lookup[wp]:
(refs_diff vs_lookup_pages1_on_heap_obj obj ptr s))
\<longrightarrow> rs \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and>
(\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some rs))\<rbrace>
update_object ptr (ArchObj obj)
set_object ptr (ArchObj obj)
\<lbrace> \<lambda>_. valid_vs_lookup \<rbrace>"
unfolding refs_diff_def
apply (rule hoare_pre)
apply (clarsimp simp: update_object_def set_object_def)
apply (clarsimp simp: set_object_def)
apply (wp get_object_wp)
apply (subst valid_vs_lookup_def)
apply (clarsimp simp: vs_lookup_pages_def del:ImageE)
@ -1813,7 +1576,7 @@ lemma update_object_valid_vs_lookup[wp]:
apply (simp add: vs_lookup_pages_def)
done
lemma update_object_valid_arch_caps[wp]:
lemma set_object_valid_arch_caps[wp]:
"\<lbrace> \<lambda>s. valid_vspace_objs s \<and> valid_arch_caps s
\<and> valid_table_caps_aobj (caps_of_state s) (arch_state s) (ArchObj obj) ptr
@ -1832,24 +1595,24 @@ lemma update_object_valid_arch_caps[wp]:
(refs_diff vs_lookup_pages1_on_heap_obj obj ptr s))
\<longrightarrow> rs \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and>
(\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some rs))\<rbrace>
update_object ptr (ArchObj obj)
set_object ptr (ArchObj obj)
\<lbrace> \<lambda>_. valid_arch_caps \<rbrace>"
by (clarsimp simp: valid_arch_caps_def | wp | fast)+
crunch valid_irq_states[wp]: update_object "valid_irq_states"
crunch valid_irq_states[wp]: set_object "valid_irq_states"
(wp: crunch_wps)
lemma update_object_state_hyp_refs[wp]:
lemma set_object_state_hyp_refs[wp]:
"\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
update_object ptr obj
set_object ptr obj
\<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>"
apply (wpsimp simp: update_object_def set_object_def wp: get_object_wp)
apply (wpsimp simp: set_object_def set_object_def wp: get_object_wp)
including unfold_objects
apply clarsimp
apply (erule rsubst [where P=P])
by (auto simp: state_hyp_refs_of_def split: option.splits)
lemma update_object_invs[wp]:
lemma set_object_invs[wp]:
"\<lbrace> \<lambda>s. invs s \<and> valid_table_caps_aobj (caps_of_state s) (arch_state s) (ArchObj obj) ptr
\<and> (aa_type obj \<noteq> AASIDPool \<longrightarrow> ptr \<notin> global_refs s)
\<and> obj_at (\<lambda>ko. case obj of PageMapL4 pm \<Rightarrow> \<exists>pm'. ko = ArchObj (PageMapL4 pm') \<and> (\<forall>x\<in>kernel_mapping_slots. pm x = pm' x) | _ \<Rightarrow> True) ptr s
@ -1881,11 +1644,12 @@ lemma update_object_invs[wp]:
(refs_diff vs_lookup_pages1_on_heap_obj obj ptr s))
\<longrightarrow> rs \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and>
(\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some rs))\<rbrace>
update_object ptr (ArchObj obj)
set_object ptr (ArchObj obj)
\<lbrace> \<lambda>_. invs \<rbrace>"
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_asid_map_def)
apply (wp valid_irq_node_typ valid_irq_handlers_lift valid_ioports_lift update_aobj_valid_global_vspace_mappings)
apply (clarsimp simp: valid_arch_state_def)
apply (wp valid_irq_node_typ valid_irq_handlers_lift valid_ioports_lift
set_aobj_valid_global_vspace_mappings set_object_valid_objs)
apply (clarsimp simp: valid_arch_state_def valid_obj_def)
done
lemma valid_global_refsD2:
@ -1987,12 +1751,11 @@ lemma valid_pml4e_typ_at:
valid_pml4e pml4e s = valid_pml4e pml4e s'"
by (case_tac pml4e, simp+)
lemmas update_aobj_cte_wp_at1[wp]
= hoare_cte_wp_caps_of_state_lift [OF update_aobj_caps_of_state]
lemma update_aobj_mdb_cte_at[wp]:
lemmas set_aobj_cte_wp_at1[wp]
= hoare_cte_wp_caps_of_state_lift [OF set_aobject_caps_of_state]
lemma set_aobj_mdb_cte_at[wp]:
"\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
update_object ptr (ArchObj pool)
set_object ptr (ArchObj pool)
\<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>"
apply (rule hoare_pre)
apply wps
@ -2659,7 +2422,7 @@ lemma store_pte_invs:
slot s))))
and (\<lambda>s. p && ~~ mask pt_bits \<notin> global_refs s \<and> wellformed_pte pte)\<rbrace>
store_pte p pte \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: store_pte_def)
apply (simp add: store_pte_def set_arch_obj_simps)
apply (wp)
apply (intro impI allI conjI valid_table_caps_aobj_upd_invalid_pte invs_valid_table_caps,
simp_all add: obj_at_def)
@ -2715,7 +2478,7 @@ lemma set_asid_pool_ifunsafe [wp]:
lemma set_asid_pool_pred_tcb_at[wp]:
"\<lbrace>pred_tcb_at proj P t\<rbrace> set_asid_pool ptr val \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def)
apply (simp add: set_asid_pool_def)
apply (wpsimp wp: get_object_wp simp: pred_tcb_at_def obj_at_def)
done
@ -2735,7 +2498,7 @@ lemma set_asid_pool_vs_lookup_unmap':
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?)
apply (simp add: set_asid_pool_def set_object_def update_object_def)
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def simp del: fun_upd_apply del: disjCI
split: kernel_object.splits arch_kernel_obj.splits)
@ -2791,7 +2554,7 @@ lemma set_asid_pool_global_objs [wp]:
"\<lbrace>valid_global_objs and valid_arch_state\<rbrace>
set_asid_pool p ap
\<lbrace>\<lambda>_. valid_global_objs\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def update_object_def)
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp del: fun_upd_apply
split: kernel_object.splits arch_kernel_obj.splits)
@ -2810,14 +2573,16 @@ lemma set_asid_pool_global_objs [wp]:
lemma set_asid_pool_aligned [wp]:
"\<lbrace>pspace_aligned\<rbrace> set_asid_pool p ptr \<lbrace>\<lambda>_. pspace_aligned\<rbrace>"
apply (simp add: set_asid_pool_def get_object_def)
apply (wp set_object_aligned|wpc)+
apply (simp add: set_asid_pool_def)
apply (wpsimp wp: set_object_aligned[THEN hoare_set_object_weaken_pre]
simp: a_type_def obj_at_def)
done
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)+
apply (simp add: set_asid_pool_def)
apply (wpsimp wp: set_object_distinct[THEN hoare_set_object_weaken_pre]
simp: a_type_def obj_at_def)+
done
lemma set_asid_pool_only_idle [wp]:
@ -2827,51 +2592,64 @@ lemma set_asid_pool_only_idle [wp]:
lemma set_asid_pool_equal_mappings [wp]:
"\<lbrace>equal_kernel_mappings\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>"
by (simp add: set_asid_pool_def update_object_def | wp set_object_equal_mappings get_object_wp)+
apply (simp add: set_asid_pool_def)
apply (wpsimp wp: set_object_equal_mappings[THEN hoare_set_object_weaken_pre]
simp: a_type_def)
done
lemma set_asid_pool_valid_global_vspace_mappings[wp]:
"\<lbrace>valid_global_vspace_mappings\<rbrace>
set_asid_pool p ap \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>"
apply (simp add: set_asid_pool_def update_object_def)
apply (wp set_object_global_vspace_mappings get_object_wp)
apply (clarsimp simp: obj_at_def a_type_simps)
apply (simp add: set_asid_pool_def)
including unfold_objects
apply (wp set_object_global_vspace_mappings[THEN hoare_set_object_weaken_pre])
apply (clarsimp simp: a_type_def)
done
lemma set_asid_pool_kernel_window[wp]:
"\<lbrace>pspace_in_kernel_window\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>"
apply (simp add: set_asid_pool_def)
apply (wp set_object_pspace_in_kernel_window get_object_wp)
including unfold_objects
apply (wpsimp wp: set_object_pspace_in_kernel_window[THEN hoare_set_object_weaken_pre]
simp: a_type_def)
done
lemma set_asid_pool_pspace_respects_device_region[wp]:
"\<lbrace>pspace_respects_device_region\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>"
apply (simp add: set_asid_pool_def)
apply (wp set_object_pspace_respects_device_region get_object_wp)
including unfold_objects
apply (wpsimp wp: set_object_pspace_respects_device_region[THEN hoare_set_object_weaken_pre]
simp: a_type_def)
done
lemma set_asid_pool_caps_kernel_window[wp]:
"\<lbrace>cap_refs_in_kernel_window\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>"
apply (simp add: set_asid_pool_def)
apply (wp set_object_cap_refs_in_kernel_window get_object_wp)
including unfold_objects
apply (wpsimp wp: set_object_cap_refs_in_kernel_window[THEN hoare_set_object_weaken_pre]
simp: a_type_def)
done
lemma set_asid_pool_caps_respects_device_region[wp]:
"\<lbrace>cap_refs_respects_device_region\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>"
apply (simp add: set_asid_pool_def)
apply (wp set_object_cap_refs_respects_device_region get_object_wp)
including unfold_objects
apply (wpsimp wp: set_object_cap_refs_respects_device_region[THEN hoare_set_object_weaken_pre]
simp: a_type_def)
done
lemma set_asid_pool_valid_ioc[wp]:
"\<lbrace>valid_ioc\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_ioc\<rbrace>"
apply (simp add: set_asid_pool_def)
apply (wp set_object_valid_ioc_no_caps get_object_inv)
including unfold_objects
apply (wpsimp wp: set_object_valid_ioc_no_caps[THEN hoare_set_object_weaken_pre]
simp: a_type_def is_tcb_def is_cap_table_def)
done
lemma set_asid_pool_vms[wp]:
"\<lbrace>valid_machine_state\<rbrace> set_asid_pool p S \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def update_object_def)
apply (wp get_object_wp)
apply clarify
apply (simp add: set_asid_pool_def)
apply (wpsimp wp: set_object_wp_strong)
apply (erule valid_machine_state_heap_updI)
apply (fastforce simp: a_type_def obj_at_def
split: kernel_object.splits arch_kernel_obj.splits)+
@ -2881,7 +2659,7 @@ lemma set_asid_pool_table_caps [wp]:
"\<lbrace>valid_table_caps\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_table_caps\<rbrace>"
apply (simp add: valid_table_caps_def)
apply (rule hoare_lift_Pf2 [where f=caps_of_state];wp?)
apply (simp add: set_asid_pool_def set_object_def update_object_def)
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def a_type_simps
split: kernel_object.splits arch_kernel_obj.splits)
@ -2893,17 +2671,17 @@ lemma set_asid_pool_zombies_state_hyp_refs [wp]:
"\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
set_asid_pool p ap
\<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>"
by (simp add: update_object_state_hyp_refs)
by (simp add: set_object_state_hyp_refs set_arch_obj_simps)
lemma set_asid_pool_invs_restrict:
"\<lbrace>invs and ko_at (ArchObj (ASIDPool ap)) p \<rbrace>
set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def valid_asid_map_def
valid_arch_caps_def del: set_asid_pool_simpler_def)
valid_arch_caps_def del: set_asid_pool_def)
apply (wp valid_irq_node_typ
set_asid_pool_vspace_objs_unmap valid_irq_handlers_lift
set_asid_pool_vs_lookup_unmap valid_ioports_lift
| simp del: set_asid_pool_simpler_def)+
| simp del: set_asid_pool_def)+
done
lemma set_asid_pool_invs_unmap:
@ -2942,7 +2720,7 @@ lemma store_pde_invs:
slot s))))
and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s \<and> wellformed_pde pde)\<rbrace>
store_pde p pde \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: store_pde_def)
apply (simp add: store_pde_def set_arch_obj_simps)
apply (wp)
apply (intro impI allI conjI valid_table_caps_aobj_upd_invalid_pde invs_valid_table_caps , simp_all add: obj_at_def)
apply (clarsimp simp: obj_at_def aa_type_simps aobj_upd_invalid_slots_simps ucast_ucast_mask
@ -2987,7 +2765,7 @@ lemma store_pdpte_invs:
slot s))))
and (\<lambda>s. p && ~~ mask pdpt_bits \<notin> global_refs s \<and> wellformed_pdpte pdpte)\<rbrace>
store_pdpte p pdpte \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: store_pdpte_def)
apply (simp add: store_pdpte_def set_arch_obj_simps)
apply (wp)
apply (intro impI allI conjI valid_table_caps_aobj_upd_invalid_pdpte invs_valid_table_caps , simp_all add: obj_at_def)
apply (clarsimp simp: obj_at_def aa_type_simps aobj_upd_invalid_slots_simps ucast_ucast_mask
@ -3035,7 +2813,7 @@ lemma store_pml4e_invs:
\<longrightarrow> ucast (p && mask pml4_bits >> word_size_bits) \<in> kernel_mapping_slots \<longrightarrow> pm (ucast (p && mask pml4_bits >> word_size_bits)) = pml4e)
and (\<lambda>s. p && ~~ mask pml4_bits \<notin> global_refs s \<and> wellformed_pml4e pml4e)\<rbrace>
store_pml4e p pml4e \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: store_pml4e_def)
apply (simp add: store_pml4e_def set_arch_obj_simps)
apply (wp)
apply (intro impI allI conjI valid_table_caps_aobj_upd_invalid_pml4e invs_valid_table_caps , simp_all add: obj_at_def)
apply (clarsimp simp: obj_at_def aa_type_simps aobj_upd_invalid_slots_simps ucast_ucast_mask
@ -3114,8 +2892,8 @@ lemma as_user_inv:
have Q: "\<And>s ps. ps (kheap s) = kheap s \<Longrightarrow> kheap_update ps s = s"
by simp
show ?thesis
apply (simp add: as_user_def gets_the_def assert_opt_def set_object_def split_def)
apply wp
apply (simp add: as_user_def gets_the_def assert_opt_def split_def bind_assoc)
apply (wpsimp wp: set_object_wp)
apply (clarsimp dest!: P)
apply (subst Q)
prefer 2

2
proof/invariant-abstract/X64/ArchBCorres2_AI.thy
View File

@ -89,7 +89,7 @@ lemmas schedule_bcorres[wp] = schedule_bcorres1[OF BCorres2_AI_axioms]
context Arch begin global_naming X64
crunch (bcorres)bcorres[wp]: send_ipc,send_signal,do_reply_transfer,arch_perform_invocation truncate_state
(simp: gets_the_def swp_def update_object_def
(simp: gets_the_def swp_def set_object_def
ignore: freeMemory clearMemory loadWord cap_fault_on_failure
storeWord lookup_error_on_failure getRestartPC getRegister mapME )

2
proof/invariant-abstract/X64/ArchDetSchedAux_AI.thy
View File

@ -16,7 +16,7 @@ context Arch begin global_naming X64
named_theorems DetSchedAux_AI_assms
crunch exst[wp]: update_object, init_arch_objects "\<lambda>s. P (exst s)" (wp: crunch_wps hoare_unless_wp)
crunch exst[wp]: set_object, init_arch_objects "\<lambda>s. P (exst s)" (wp: crunch_wps hoare_unless_wp)
crunch ct[wp]: init_arch_objects "\<lambda>s. P (cur_thread s)" (wp: crunch_wps hoare_unless_wp)
crunch st_tcb_at[wp]: init_arch_objects "st_tcb_at Q t" (wp: mapM_x_wp' hoare_unless_wp)
crunch valid_etcbs[wp, DetSchedAux_AI_assms]: init_arch_objects valid_etcbs (wp: valid_etcbs_lift)

22
proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy
View File

@ -215,7 +215,7 @@ lemma set_asid_pool_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (wp hoare_drop_imps valid_sched_lift | simp add: set_asid_pool_def)+
crunch ct_not_in_q[wp]: update_object ct_not_in_q
crunch ct_not_in_q[wp]: set_object ct_not_in_q
(wp: crunch_wps hoare_drop_imps hoare_unless_wp select_inv mapM_wp
subset_refl if_fun_split simp: crunch_simps ignore: tcb_sched_action)
@ -230,14 +230,14 @@ crunch ct_not_in_q [wp, DetSchedSchedule_AI_assms]:
lemma flush_table_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> flush_table a b c d \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
by (wp mapM_x_wp' | wpc | simp add: flush_table_def | rule hoare_pre)+
lemma update_object_valid_etcbs[wp]:
"\<lbrace>valid_etcbs\<rbrace> update_object f tptr \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
by (wp hoare_drop_imps valid_etcbs_lift | simp add: update_object_def)+
lemma set_object_valid_etcbs[wp]:
"\<lbrace>valid_etcbs\<rbrace> set_object f tptr \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>"
by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_object_def)+
crunch valid_etcbs [wp, DetSchedSchedule_AI_assms]:
arch_finalise_cap, prepare_thread_delete valid_etcbs
(wp: hoare_drop_imps hoare_unless_wp select_inv mapM_x_wp mapM_wp subset_refl
if_fun_split simp: crunch_simps ignore: update_object set_object thread_set)
if_fun_split simp: crunch_simps ignore: set_object set_object thread_set)
lemma flush_table_simple_sched_action[wp]: "\<lbrace>simple_sched_action\<rbrace> flush_table a b c d \<lbrace>\<lambda>rv. simple_sched_action\<rbrace>"
by (wp mapM_x_wp' | wpc | simp add: flush_table_def | rule hoare_pre)+
@ -252,7 +252,7 @@ lemma flush_table_valid_sched[wp]: "\<lbrace>valid_sched\<rbrace> flush_table a
lemma store_pte_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> store_pte pter pte \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (wp hoare_drop_imps valid_sched_lift | simp add: store_pte_def)+
by (wp hoare_drop_imps valid_sched_lift | simp add: store_pte_def set_arch_obj_simps)+
lemma store_pm_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> store_pml4e pter pm \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
@ -260,15 +260,17 @@ lemma store_pm_valid_sched[wp]:
lemma store_pdepte_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> store_pdpte pter pd \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (wp add: hoare_drop_imps valid_sched_lift del: store_pdpte_typ_at | simp add: store_pdpte_def)+
by (wp add: hoare_drop_imps valid_sched_lift del: store_pdpte_typ_at
| simp add: store_pdpte_def set_arch_obj_simps)+
lemma store_pde_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> store_pde pter pd \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (wp add: hoare_drop_imps valid_sched_lift del: store_pde_typ_at | simp add: store_pde_def)+
by (wp add: hoare_drop_imps valid_sched_lift del: store_pde_typ_at
| simp add: store_pde_def set_arch_obj_simps)+
crunch valid_sched [wp, DetSchedSchedule_AI_assms]:
arch_tcb_set_ipc_buffer, arch_finalise_cap, prepare_thread_delete valid_sched
(ignore: set_object update_object wp: crunch_wps subset_refl simp: if_fun_split crunch_simps)
(ignore: set_object set_object wp: crunch_wps subset_refl simp: if_fun_split crunch_simps)
lemma activate_thread_valid_sched [DetSchedSchedule_AI_assms]:
"\<lbrace>valid_sched\<rbrace> activate_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>"
@ -279,7 +281,7 @@ lemma activate_thread_valid_sched [DetSchedSchedule_AI_assms]:
lemma store_asid_pool_entry_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> store_asid_pool_entry ptr pool a \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (wp hoare_drop_imps valid_sched_lift | simp add: store_asid_pool_entry_def)+
by (wp hoare_drop_imps valid_sched_lift | simp add: store_asid_pool_entry_def set_arch_obj_simps)+
crunch valid_sched[wp]:
perform_page_invocation, perform_page_table_invocation, perform_asid_pool_invocation,

2
proof/invariant-abstract/X64/ArchDeterministic_AI.thy
View File

@ -19,7 +19,7 @@ named_theorems Deterministic_AI_assms
lemma flush_table_valid_list[wp]: "\<lbrace>valid_list\<rbrace> flush_table a b c d \<lbrace>\<lambda>rv. valid_list\<rbrace>"
by (wp mapM_x_wp' | wpc | simp add: flush_table_def | rule hoare_pre)+
crunch valid_list[wp]: update_object valid_list
crunch valid_list[wp]: set_object valid_list
(wp: get_object_wp)
crunch valid_list[wp, Deterministic_AI_assms]:

4
proof/invariant-abstract/X64/ArchEmptyFail_AI.thy
View File

@ -155,7 +155,7 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slo
(simp: Let_def catch_def split_def OR_choiceE_def mk_ef_def option.splits endpoint.splits
notification.splits thread_state.splits sum.splits cap.splits arch_cap.splits
kernel_object.splits vmpage_size.splits pde.splits bool.splits list.splits
forM_x_def empty_fail_mapM_x update_object_def
forM_x_def empty_fail_mapM_x set_object_def
ignore: nativeThreadUsingFPU_impl switchFpuOwner_impl)
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: setRegister, setNextPC
@ -199,7 +199,7 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_event, activate_t
thread_state.splits endpoint.splits catch_def sum.splits cnode_invocation.splits
page_table_invocation.splits page_invocation.splits asid_control_invocation.splits
asid_pool_invocation.splits arch_invocation.splits irq_state.splits syscall.splits
page_directory_invocation.splits update_object_def
page_directory_invocation.splits set_object_def
ignore: resetTimer_impl)
end

68
proof/invariant-abstract/X64/ArchFinalise_AI.thy
View File

@ -138,7 +138,7 @@ lemma set_asid_pool_unmap:
set_asid_pool poolptr (pool(lowbits := None))
\<lbrace>\<lambda>rv s. \<not> ([VSRef (ucast lowbits) (Some AASIDPool),
VSRef highbits None] \<rhd> x) s\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def update_object_def)
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: vs_lookup_def vs_asid_refs_def
dest!: graph_ofD vs_lookup1_rtrancl_iterations)
@ -173,23 +173,23 @@ lemma delete_asid_unmapped[wp]:
lemma set_pt_tcb_at_arch[simplified, wp]:
"\<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pt a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>"
by (clarsimp simp: valid_def obj_at_def update_object_def get_object_def
set_object_def in_monad a_type_simps)
by (clarsimp simp: valid_def obj_at_def set_object_def get_object_def
in_monad a_type_simps set_arch_obj_simps)
lemma set_pd_tcb_at_arch[simplified, wp]:
"\<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pd a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>"
by (clarsimp simp: valid_def obj_at_def update_object_def get_object_def
set_object_def in_monad a_type_simps)
by (clarsimp simp: valid_def obj_at_def set_object_def get_object_def
in_monad a_type_simps set_arch_obj_simps)
lemma set_pdpt_tcb_at_arch[simplified, wp]:
"\<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pdpt a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>"
by (clarsimp simp: valid_def obj_at_def update_object_def get_object_def
set_object_def in_monad a_type_simps)
by (clarsimp simp: valid_def obj_at_def set_object_def get_object_def
in_monad a_type_simps set_arch_obj_simps)
lemma set_pml4_tcb_at_arch[simplified, wp]:
"\<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pml4 a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>"
by (clarsimp simp: valid_def obj_at_def update_object_def get_object_def
set_object_def in_monad a_type_simps)
by (clarsimp simp: valid_def obj_at_def set_object_def get_object_def
in_monad a_type_simps set_arch_obj_simps)
crunch tcb_at_arch: unmap_page "\<lambda>s. P (ko_at (TCB tcb) t s)"
(simp: crunch_simps wp: crunch_wps ignore: set_pt set_pd set_pdpt)
@ -513,12 +513,12 @@ lemma suspend_unlive':
"\<lbrace>bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t \<rbrace>
suspend t
\<lbrace>\<lambda>rv. obj_at (Not \<circ> live) t\<rbrace>"
apply (simp add: suspend_def set_thread_state_def set_object_def)
apply (wp | simp only: obj_at_exst_update)+
apply (simp add: obj_at_def)
apply (rule_tac Q="\<lambda>_. bound_tcb_at ((=) None) t" in hoare_strengthen_post)
apply wp
apply (auto simp: pred_tcb_def2 live_def hyp_live_def dest: refs_of_live)
apply (simp add: suspend_def set_thread_state_def)
apply (wpsimp wp: set_object_wp | simp only: obj_at_exst_update)+
apply (simp add: obj_at_def)
apply (rule_tac Q="\<lambda>_. bound_tcb_at ((=) None) t" in hoare_strengthen_post)
apply wp
apply (auto simp: pred_tcb_def2 live_def hyp_live_def dest: refs_of_live)
done
crunch obj_at[wp]: fpu_thread_delete
@ -594,7 +594,7 @@ lemma set_asid_pool_cte_wp_at:
"\<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace>
set_asid_pool ptr val
\<lbrace>\<lambda>rv s. P (cte_wp_at P' p s)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def get_object_def update_object_def)
apply (simp add: set_asid_pool_def set_object_def get_object_def)
apply wp
including unfold_objects_asm
by (clarsimp elim!: rsubst[where P=P]
@ -602,9 +602,9 @@ lemma set_asid_pool_cte_wp_at:
crunch cte_wp_at[wp,Finalise_AI_asms]: arch_finalise_cap "\<lambda>s. P (cte_wp_at P' p s)"
(simp: crunch_simps assertE_def
wp: update_aobj_cte_wp_at crunch_wps set_object_cte_at
ignore: update_object set_pt set_pd set_pdpt)
(simp: crunch_simps assertE_def set_arch_obj_simps
wp: set_aobject_cte_wp_at crunch_wps set_object_cte_at
ignore: set_object)
end
@ -669,8 +669,8 @@ crunch irq_node[wp]: arch_finalise_cap "\<lambda>s. P (interrupt_irq_node s)"
(wp: crunch_wps select_wp simp: crunch_simps)
crunch pred_tcb_at[wp]: arch_finalise_cap "pred_tcb_at proj P t"
(simp: crunch_simps wp: crunch_wps update_aobj_pred_tcb_at
ignore: update_object set_object set_pt set_pd set_pdpt set_pml4)
(simp: crunch_simps set_arch_obj_simps wp: crunch_wps set_aobject_pred_tcb_at
ignore: set_object)
lemma tcb_cap_valid_pagetable:
"tcb_cap_valid (ArchObjectCap (PageTableCap word (Some v))) slot
@ -703,7 +703,7 @@ lemma store_pde_unmap_empty:
"\<lbrace>\<lambda>s. obj_at (empty_table (set (x64_global_pdpts (arch_state s)))) word s\<rbrace>
store_pde pd_slot InvalidPDE
\<lbrace>\<lambda>rv s. obj_at (empty_table (set (x64_global_pdpts (arch_state s)))) word s\<rbrace>"
apply (clarsimp simp: store_pde_def set_pd_def set_object_def update_object_def)
apply (clarsimp simp: store_pde_def set_pd_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def empty_table_def pde_ref_def)
done
@ -712,7 +712,7 @@ lemma store_pte_unmap_empty:
"\<lbrace>\<lambda>s. obj_at (empty_table (set (x64_global_pdpts (arch_state s)))) word s\<rbrace>
store_pte xa InvalidPTE
\<lbrace>\<lambda>rv s. obj_at (empty_table (set (x64_global_pdpts (arch_state s)))) word s\<rbrace>"
apply (wp get_object_wp | simp add: store_pte_def set_pt_def set_object_def update_object_def)+
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)
done
@ -720,7 +720,7 @@ lemma store_pdpte_unmap_empty:
"\<lbrace>\<lambda>s. obj_at (empty_table (set (x64_global_pdpts (arch_state s)))) word s\<rbrace>
store_pdpte pd_slot InvalidPDPTE
\<lbrace>\<lambda>rv s. obj_at (empty_table (set (x64_global_pdpts (arch_state s)))) word s\<rbrace>"
apply (clarsimp simp: store_pdpte_def set_pd_def set_object_def update_object_def)
apply (clarsimp simp: store_pdpte_def set_arch_obj_simps set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def empty_table_def pdpte_ref_def)
done
@ -729,7 +729,7 @@ lemma store_pml4e_unmap_empty:
"\<lbrace>\<lambda>s. obj_at (empty_table (set (x64_global_pdpts (arch_state s)))) word s\<rbrace>
store_pml4e pd_slot InvalidPML4E
\<lbrace>\<lambda>rv s. obj_at (empty_table (set (x64_global_pdpts (arch_state s)))) word s\<rbrace>"
apply (clarsimp simp: store_pml4e_def set_pd_def set_object_def update_object_def)
apply (clarsimp simp: store_pml4e_def set_arch_obj_simps set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def empty_table_def pml4e_ref_def)
done
@ -1016,7 +1016,7 @@ lemma delete_asid_empty_table_pml4:
delete_asid a word
\<lbrace>\<lambda>_ s. obj_at (empty_table (set (x64_global_pdpts (arch_state s)))) word s\<rbrace>"
apply (simp add: delete_asid_def)
apply (wp set_object_at_obj get_object_wp | wpc | simp add: update_object_def | wps)+
apply (wpsimp wp: set_object_at_obj simp: set_arch_obj_simps | wps)+
apply (clarsimp simp: obj_at_def empty_table_def)
done
@ -1053,7 +1053,7 @@ lemma store_pml4e_pml4e_wp_at:
\<lbrace>\<lambda>_. pml4e_wp_at
(\<lambda>pde. pde = x) (p && ~~ mask pml4_bits) (ucast (p && mask pml4_bits >> word_size_bits))\<rbrace>"
apply (wp
| simp add: store_pml4e_def set_pml4_def set_object_def get_object_def update_object_def
| simp add: store_pml4e_def set_pml4_def set_object_def get_object_def
obj_at_def pml4e_wp_at_def a_type_simps aa_type_simps)+
done
@ -1062,7 +1062,7 @@ lemma store_pml4e_pml4e_wp_at2:
store_pml4e p' InvalidPML4E
\<lbrace>\<lambda>_. pml4e_wp_at (\<lambda>pde. pde = InvalidPML4E) ptr slot\<rbrace>"
apply (wp
| simp add: store_pml4e_def set_pml4_def set_object_def get_object_def update_object_def
| simp add: store_pml4e_def set_pml4_def set_object_def get_object_def
obj_at_def pml4e_wp_at_def
| clarsimp)+
done
@ -1372,7 +1372,7 @@ lemma set_asid_pool_obj_at_ptr:
"\<lbrace>\<lambda>s. P (ArchObj (arch_kernel_obj.ASIDPool mp))\<rbrace>
set_asid_pool ptr mp
\<lbrace>\<lambda>rv s. obj_at P ptr s\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def update_object_def)
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def)
done
@ -1483,7 +1483,7 @@ lemma set_asid_pool_empty_table_objs:
\<lbrace>\<lambda>rv s. valid_vspace_objs
(s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of word2 \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def update_object_def)
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def valid_vspace_objs_def
simp del: fun_upd_apply
@ -1508,7 +1508,7 @@ lemma set_asid_pool_empty_table_lookup:
\<lbrace>\<lambda>rv s. valid_vs_lookup
(s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def update_object_def)
apply (simp add: set_asid_pool_def set_object_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def valid_vs_lookup_def
simp del: fun_upd_apply)
@ -1539,7 +1539,7 @@ lemma set_asid_pool_invs_table:
\<lbrace>\<lambda>x s. invs (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def valid_asid_map_def
del: set_asid_pool_simpler_def)
del: set_asid_pool_def)
apply (wp valid_irq_node_typ set_asid_pool_typ_at
set_asid_pool_empty_table_objs valid_ioports_lift
valid_irq_handlers_lift set_asid_pool_empty_table_lookup
@ -1603,8 +1603,8 @@ crunch valid_cap [wp]: unmap_page_table,
store_pte, delete_asid_pool, copy_global_mappings,
arch_finalise_cap
"valid_cap c"
(wp: mapM_wp_inv mapM_x_wp' crunch_wps simp: crunch_simps
ignore: set_pd set_pt set_pdpt set_pml4 update_object)
(wp: mapM_wp_inv mapM_x_wp' crunch_wps simp: crunch_simps set_arch_obj_simps
ignore: set_object)
lemmas clearMemory_invs[wp, Finalise_AI_asms] = clearMemory_invs

33
proof/invariant-abstract/X64/ArchKHeap_AI.thy
View File

@ -215,9 +215,7 @@ lemma set_object_neg_lookup:
"\<lbrace>\<lambda>s. \<not> (\<exists>rs. (rs \<rhd> p') s) \<and> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s \<rbrace>
set_object p ko
\<lbrace>\<lambda>_ s. \<not> (\<exists>rs. (rs \<rhd> p') s)\<rbrace>"
apply (simp add: set_object_def)
apply wp
apply clarsimp
apply (wpsimp wp: set_object_wp)
apply (erule_tac x=rs in allE)
apply (erule notE)
apply (erule vs_lookup_stateI)
@ -229,9 +227,7 @@ lemma set_object_vs_lookup:
"\<lbrace>\<lambda>s. obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s \<and> P (vs_lookup s) \<rbrace>
set_object p ko
\<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>"
apply (simp add: set_object_def)
apply wp
apply clarsimp
apply (wpsimp wp: set_object_wp)
apply (erule rsubst [where P=P])
apply (rule order_antisym)
apply (rule vs_lookup_sub)
@ -251,9 +247,7 @@ lemma set_object_pt_not_vs_lookup_pages:
| None \<Rightarrow> True))\<rbrace>
set_object p (ArchObj (PageTable pt))
\<lbrace>\<lambda>_ s. \<not>(ref \<unrhd> p') s\<rbrace>"
apply (simp add: set_object_def)
apply wp
apply (clarsimp simp: obj_at_def)
apply (wpsimp wp: set_object_wp)
apply (case_tac "(\<exists>\<unrhd>p) s")
apply (erule notE)
apply clarsimp
@ -300,9 +294,7 @@ lemma set_object_vs_lookup_pages:
"\<lbrace>\<lambda>s. obj_at (\<lambda>ko'. vs_refs_pages ko = vs_refs_pages ko') p s \<and> P (vs_lookup_pages s) \<rbrace>
set_object p ko
\<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>"
apply (simp add: set_object_def)
apply wp
apply clarsimp
apply (wpsimp wp: set_object_wp)
apply (erule rsubst [where P=P])
apply (rule order_antisym)
apply (rule vs_lookup_pages_sub)
@ -313,14 +305,15 @@ lemma set_object_vs_lookup_pages:
apply simp
done
lemma set_aobject_valid_arch [wp]:
"set_object ptr (ArchObj obj) \<lbrace>valid_arch_state\<rbrace>"
by (wpsimp wp: valid_arch_state_lift set_object_wp)
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>
set_object p (ArchObj ako)
\<lbrace>\<lambda>rv s. P (typ_at (AArch T) p' s)\<rbrace>"
apply (simp add: set_object_def)
apply wp
apply clarsimp
apply (wpsimp wp: set_object_wp)
apply (erule rsubst [where P=P])
apply (clarsimp simp: obj_at_def a_type_aa_type)
done
@ -350,9 +343,8 @@ lemma set_object_valid_kernel_mappings:
ko\<rbrace>
set_object ptr ko
\<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>"
apply (simp add: set_object_def)
apply wp
apply_trace (clarsimp simp: valid_kernel_mappings_def second_level_tables_def
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: valid_kernel_mappings_def second_level_tables_def
elim!: ranE split: if_split_asm)
apply fastforce
done
@ -621,7 +613,7 @@ lemma set_object_equal_mappings:
\<longrightarrow> (\<forall>w \<in> kernel_mapping_slots. pml4 w = pml4' w)))\<rbrace>
set_object p ko
\<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>"
apply (simp add: set_object_def, wp)
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: equal_kernel_mappings_def obj_at_def
split del: if_split)
apply (simp split: if_split_asm)
@ -735,8 +727,7 @@ lemma set_object_global_vspace_mappings:
\<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s)\<rbrace>
set_object p ko
\<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>"
apply (simp add: set_object_def, wp)
apply clarsimp
apply (wpsimp wp: set_object_wp)
apply (erule valid_global_vspace_mappings_pres)
apply (clarsimp simp: obj_at_def a_type_def global_refs_def)+
done

65
proof/invariant-abstract/X64/ArchRetype_AI.thy
View File

@ -63,13 +63,17 @@ lemmas [wp] = hoare_unless_wp
crunch pspace_aligned[wp]: init_arch_objects "pspace_aligned"
(ignore: clearMemory wp: crunch_wps simp: crunch_simps unless_def)
crunch pspace_distinct[wp]: init_arch_objects "pspace_distinct"
(ignore: clearMemory update_object set_pml4 wp: crunch_wps update_obj_pspace_distinct simp: crunch_simps unless_def)
(ignore: clearMemory set_object set_pml4
wp: crunch_wps set_object_distinct
simp: crunch_simps unless_def set_arch_obj_simps)
crunch mdb_inv[wp]: init_arch_objects "\<lambda>s. P (cdt s)"
(ignore: clearMemory set_pml4 wp: crunch_wps simp: crunch_simps unless_def)
(ignore: clearMemory set_pml4 wp: crunch_wps simp: crunch_simps unless_def set_arch_obj_simps)
crunch valid_mdb[wp]: init_arch_objects "valid_mdb"
(ignore: clearMemory set_pml4 wp: crunch_wps simp: crunch_simps unless_def)
(ignore: clearMemory set_pml4 wp: crunch_wps simp: crunch_simps unless_def set_arch_obj_simps)
crunch cte_wp_at[wp]: init_arch_objects "\<lambda>s. P (cte_wp_at P' p s)"
(ignore: clearMemory set_pml4 wp: crunch_wps update_aobj_cte_wp_at simp: crunch_simps unless_def)
(ignore: clearMemory set_pml4
wp: crunch_wps set_aobject_cte_wp_at
simp: crunch_simps unless_def set_arch_obj_simps)
crunch typ_at[wp]: init_arch_objects "\<lambda>s. P (typ_at T p s)"
(ignore: clearMemory wp: crunch_wps simp: crunch_simps unless_def)
@ -107,15 +111,15 @@ lemma store_pml4e_wellformed[wp]:
by (wpsimp simp: store_pml4e_def)
lemma store_pml4e_valid_objs[wp]:
"\<lbrace>valid_objs and K ( wellformed_pml4e p)\<rbrace> store_pml4e x p \<lbrace>\<lambda>rv. valid_objs\<rbrace>"
apply (wpsimp simp: store_pml4e_def)
"\<lbrace>valid_objs and K (wellformed_pml4e p)\<rbrace> store_pml4e x p \<lbrace>\<lambda>rv. valid_objs\<rbrace>"
apply (wpsimp simp: store_pml4e_def set_arch_obj_simps)
by (fastforce simp: valid_objs_def obj_at_def dom_def valid_obj_def)
crunch valid_objs[wp]: init_arch_objects "valid_objs"
(ignore: clearMemory wp: crunch_wps simp: unless_def)
crunch valid_arch_state[wp]: init_arch_objects "valid_arch_state"
(ignore: clearMemory set_pml4 set_object wp: crunch_wps simp: unless_def crunch_simps)
(ignore: clearMemory set_pml4 set_object wp: crunch_wps simp: unless_def crunch_simps set_arch_obj_simps)
lemmas init_arch_objects_valid_cap[wp] = valid_cap_typ [OF init_arch_objects_typ_at]
@ -130,31 +134,31 @@ crunch cap_refs_respects_device_region[wp]: reserve_region cap_refs_respects_dev
crunch invs [wp]: reserve_region "invs"
crunch iflive[wp]: copy_global_mappings "if_live_then_nonz_cap"
(wp: crunch_wps ignore: set_pml4)
(wp: crunch_wps ignore: set_pml4 simp: set_arch_obj_simps)
crunch zombies[wp]: copy_global_mappings "zombies_final"
(wp: crunch_wps)
(wp: crunch_wps simp: set_arch_obj_simps)
crunch state_refs_of[wp]: copy_global_mappings "\<lambda>s. P (state_refs_of s)"
(wp: crunch_wps ignore: set_pml4)
(wp: crunch_wps ignore: set_pml4 simp: set_arch_obj_simps)
crunch valid_idle[wp]: copy_global_mappings "valid_idle"
(wp: crunch_wps ignore: set_pml4)
(wp: crunch_wps ignore: set_pml4 simp: set_arch_obj_simps is_tcb_def)
crunch only_idle[wp]: copy_global_mappings "only_idle"
(wp: crunch_wps ignore: set_pml4)
(wp: crunch_wps ignore: set_pml4 simp: set_arch_obj_simps)
crunch ifunsafe[wp]: copy_global_mappings "if_unsafe_then_cap"
(wp: crunch_wps)
(wp: crunch_wps simp: set_arch_obj_simps)
crunch reply_caps[wp]: copy_global_mappings "valid_reply_caps"
(wp: crunch_wps ignore: set_pml4)
(wp: crunch_wps ignore: set_pml4 simp: set_arch_obj_simps)
crunch reply_masters[wp]: copy_global_mappings "valid_reply_masters"
(wp: crunch_wps ignore: set_pml4)
(wp: crunch_wps ignore: set_pml4 simp: set_arch_obj_simps)
crunch valid_global[wp]: copy_global_mappings "valid_global_refs"
(wp: crunch_wps ignore: set_pml4)
(wp: crunch_wps ignore: set_pml4 simp: set_arch_obj_simps)
crunch irq_node[wp]: copy_global_mappings "\<lambda>s. P (interrupt_irq_node s)"
(wp: crunch_wps)
@ -169,13 +173,13 @@ crunch pspace_in_kernel_window[wp]: copy_global_mappings "pspace_in_kernel_windo
(wp: crunch_wps)
crunch cap_refs_in_kernel_window[wp]: copy_global_mappings "cap_refs_in_kernel_window"
(wp: crunch_wps)
(wp: crunch_wps simp: set_arch_obj_simps)
crunch pspace_respects_device_region[wp]: copy_global_mappings "pspace_respects_device_region"
(wp: crunch_wps ignore: set_pml4)
(wp: crunch_wps ignore: set_pml4 simp: set_arch_obj_simps)
crunch cap_refs_respects_device_region[wp]: copy_global_mappings "cap_refs_respects_device_region"
(wp: crunch_wps)
(wp: crunch_wps simp: set_arch_obj_simps)
(* FIXME: move to VSpace_R *)
lemma vs_refs_add_one'':
@ -225,7 +229,7 @@ lemma mapM_x_store_pml4e_eq_kernel_mappings_restr:
\<and> pmv (ucast x) = pmv' (ucast x)))\<rbrace>"
apply (induct xs rule: rev_induct, simp_all add: mapM_x_Nil mapM_x_append mapM_x_singleton)
apply (erule hoare_seq_ext[rotated])
apply (simp add: store_pml4e_def set_object_def update_object_def cong: bind_cong)
apply (simp add: store_pml4e_def set_object_def set_arch_obj_simps cong: bind_cong)
apply (wp get_object_wp get_pml4e_wp)
apply (clarsimp simp: obj_at_def split del: if_split)
apply (frule shiftl_less_t2n)
@ -318,18 +322,18 @@ lemma store_pde_valid_global_pd_mappings[wp]:
store_pml4e p pml4e
\<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>"
apply (simp add: store_pml4e_def set_pml4_def)
apply (wp update_aobj_valid_global_vspace_mappings)
apply (wp set_aobj_valid_global_vspace_mappings)
apply simp
done
lemma store_pde_valid_ioc[wp]:
"\<lbrace>valid_ioc\<rbrace> store_pml4e ptr pml4e \<lbrace>\<lambda>_. valid_ioc\<rbrace>"
by (wpsimp simp: store_pml4e_def)
by (wpsimp simp: store_pml4e_def set_arch_obj_simps)
lemma store_pde_vms[wp]:
"\<lbrace>valid_machine_state\<rbrace> store_pml4e ptr pml4e \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
by (wpsimp simp: store_pml4e_def)
by (wpsimp simp: store_pml4e_def set_arch_obj_simps)
lemma valid_arch_caps_table_caps:
"valid_arch_caps s \<Longrightarrow> valid_table_caps s"
@ -374,15 +378,15 @@ lemma in_kernel_mapping_slotsI:
lemma set_object_ioports[wp]:
"\<lbrace>valid_ioports and obj_at (same_caps obj) ptr\<rbrace> set_object ptr obj \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
by (wpsimp simp: set_object_def valid_ioports_def caps_of_state_after_update)
by (wpsimp simp: set_object_def get_object_def valid_ioports_def caps_of_state_after_update)
lemma update_aobj_ioports[wp]:
"\<lbrace>valid_ioports\<rbrace> update_object ptr (ArchObj obj) \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
apply (clarsimp simp: update_object_def)
"\<lbrace>valid_ioports\<rbrace> set_object ptr (ArchObj obj) \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
apply (subst set_object_def)
apply (wpsimp wp: get_object_wp)
by (clarsimp simp: obj_at_def a_type_def
split: kernel_object.split_asm if_splits
arch_kernel_obj.split_asm)
apply (clarsimp simp: obj_at_def a_type_def valid_ioports_def caps_of_state_after_update
split: kernel_object.split_asm if_splits arch_kernel_obj.split_asm)
done
lemma copy_global_invs_mappings_restricted:
"\<lbrace>(\<lambda>s. all_invs_but_equal_kernel_mappings_restricted (insert pm S) s)
@ -390,6 +394,7 @@ lemma copy_global_invs_mappings_restricted:
and K (is_aligned pm pml4_bits)\<rbrace>
copy_global_mappings pm
\<lbrace>\<lambda>rv. all_invs_but_equal_kernel_mappings_restricted S\<rbrace>"
supply set_arch_obj_simps[simp]
apply (rule hoare_gen_asm)
apply (simp add: valid_pspace_def pred_conj_def)
apply (rule hoare_conjI, wp copy_global_equal_kernel_mappings_restricted)
@ -1271,7 +1276,7 @@ lemma init_arch_objects_excap[wp]:
by (wp ex_cte_cap_to_pres )
crunch st_tcb_at[wp]: init_arch_objects "st_tcb_at P t"
(wp: crunch_wps ignore: update_object set_pml4)
(wp: crunch_wps ignore: set_object set_pml4 simp: set_arch_obj_simps)
lemma valid_arch_mdb_detype:
"valid_arch_mdb (is_original_cap s) (caps_of_state s) \<Longrightarrow>

4
proof/invariant-abstract/X64/ArchTcbAcc_AI.thy
View File

@ -101,8 +101,8 @@ lemma thread_set_hyp_refs_trivial [TcbAcc_AI_assms]:
assumes x: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
assumes y: "\<And>tcb. tcb_arch_ref (f tcb) = tcb_arch_ref tcb"
shows "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
apply (simp add: thread_set_def set_object_def)
apply wp
apply (simp add: thread_set_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp dest!: get_tcb_SomeD)
apply (clarsimp elim!: rsubst[where P=P])
apply (rule all_ext;

17
proof/invariant-abstract/X64/ArchUntyped_AI.thy
View File

@ -237,7 +237,7 @@ lemma init_arch_objects_descendants_range[wp,Untyped_AI_assms]:
apply (simp add:descendants_range_def)
apply (rule hoare_pre)
apply (wp retype_region_mdb init_arch_objects_hoare_lift)
apply (simp add: store_pml4e_def)
apply (simp add: store_pml4e_def set_arch_obj_simps)
apply (wp hoare_vcg_ball_lift | wps)+
apply simp
apply fastforce
@ -426,9 +426,10 @@ lemma simpler_store_pml4e_def:
({((), s\<lparr>kheap := (kheap s((p && ~~ mask pml4_bits) \<mapsto>
(ArchObj (PageMapL4 (pml4(ucast (p && mask pml4_bits >> word_size_bits) := pde))))))\<rparr>)}, False)
| _ => ({}, True))"
apply (auto simp: store_pml4e_def update_object_def get_object_def simpler_gets_def assert_def a_type_simps
apply (auto simp: store_pml4e_def set_object_def get_object_def simpler_gets_def assert_def a_type_simps
return_def fail_def set_object_def get_def put_def bind_def get_pml4_def aa_type_simps
split: Structures_A.kernel_object.splits option.splits arch_kernel_obj.splits if_split_asm)
set_arch_obj_simps
split: Structures_A.kernel_object.splits option.splits arch_kernel_obj.splits if_split_asm)
done
lemma neg_mask_pml4_bits_3_aligned[simp]:
@ -448,7 +449,7 @@ lemma store_pml4e_weaken:
apply (erule allEI)
apply clarsimp
apply (rule use_valid, assumption)
apply (simp add: update_object_def store_pml4e_def set_object_def)
apply (simp add: store_pml4e_def set_arch_obj_simps set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: pml4e_at_def obj_at_def a_type_simps)
apply (drule bspec, assumption)
@ -463,7 +464,7 @@ lemma store_pml4e_nonempty_table:
\<and> ucast (pml4e_ptr && mask pml4_bits >> 3) \<in> kernel_mapping_slots\<rbrace>
store_pml4e pml4e_ptr pml4e
\<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>"
apply (simp add: store_pml4e_def update_object_def set_object_def)
apply (simp add: store_pml4e_def set_arch_obj_simps set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def nonempty_table_def a_type_def word_size_bits_def empty_table_def)
done
@ -476,7 +477,7 @@ lemma store_pml4e_global_global_objs:
\<rbrace>
store_pml4e pml4e_ptr pml4e
\<lbrace>\<lambda>rv s. valid_global_objs s\<rbrace>"
apply (simp add: store_pml4e_def set_pd_def set_object_def)
apply (simp add: store_pml4e_def set_arch_obj_simps set_pd_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def fun_upd_def[symmetric] bit_simps
valid_global_objs_upd_def empty_table_def valid_global_objs_def)
@ -592,9 +593,9 @@ lemma set_pml4e_cte_wp_at_iin[wp]:
"\<lbrace>\<lambda>s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace>
store_pml4e q pml4
\<lbrace>\<lambda>_ s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace>"
apply (clarsimp simp: store_pml4e_def)
apply (clarsimp simp: store_pml4e_def set_arch_obj_simps)
apply (rule hoare_pre)
apply (wp update_aobj_cte_wp_at | wps | simp)+
apply (wp set_aobject_cte_wp_at | wps | simp)+
done
crunch cte_wp_at_iin[wp]: init_arch_objects

83
proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy
View File

@ -90,7 +90,8 @@ lemma set_object_valid_vspace_objs'[wp]:
"\<lbrace>valid_vspace_objs' and K (obj_valid_vspace obj)\<rbrace>
set_object ptr obj
\<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
apply (simp add: set_object_def, wp)
including unfold_objects
apply (wpsimp wp: set_object_wp_strong simp: a_type_def)
apply (auto simp: fun_upd_def[symmetric] del: ballI elim: ball_ran_updI)
done
@ -147,7 +148,7 @@ lemma mapM_x_store_pte_updates:
apply (simp add: mapM_x_Cons)
apply (rule hoare_seq_ext, assumption)
apply (thin_tac "valid P f Q" for P f Q)
apply (simp add: store_pte_def set_pt_def set_object_def update_object_def word_size_bits_def)
apply (simp add: store_pte_def set_pt_def set_object_def word_size_bits_def)
apply (wp get_pt_wp get_object_wp)
apply (clarsimp simp: obj_at_def a_type_simps)
apply (erule rsubst[where P=Q])
@ -211,7 +212,7 @@ lemma mapM_x_store_pde_updates:
apply (simp add: mapM_x_Cons)
apply (rule hoare_seq_ext, assumption)
apply (thin_tac "valid P f Q" for P f Q)
apply (simp add: store_pde_def set_pd_def set_object_def update_object_def word_size_bits_def)
apply (simp add: store_pde_def set_pd_def set_object_def word_size_bits_def)
apply (wp get_pd_wp get_object_wp)
apply (clarsimp simp: obj_at_def a_type_simps)
apply (erule rsubst[where P=Q])
@ -223,42 +224,45 @@ lemma mapM_x_store_pde_updates:
lemma store_pde_valid_vspace_objs':
"\<lbrace>valid_vspace_objs'\<rbrace>
store_pde p pde \<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
apply (simp add: store_pde_def set_pd_def update_object_def, wp get_object_wp)
apply (simp add: store_pde_def set_pd_def)
apply (wpsimp wp: set_object_valid_vspace_objs')
apply (clarsimp simp: obj_at_def)
apply (rule valid_entries_overwrite_0)
apply (fastforce simp:ran_def)
apply (drule bspec)
apply fastforce
apply (case_tac "pd pa")
apply (rule valid_entries_overwrite_0)
apply (fastforce simp:ran_def)
apply (drule bspec)
apply fastforce
apply (case_tac "pd pa")
apply simp_all
apply (case_tac pde,simp_all)
apply (case_tac pde,simp_all)
apply (case_tac pde,simp_all)
apply (case_tac pde,simp_all)
done
lemma store_pte_valid_vspace_objs':
"\<lbrace>valid_vspace_objs'\<rbrace>
store_pte p pte \<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
apply (simp add: store_pte_def set_pt_def update_object_def, wp get_object_wp)
apply (simp add: store_pte_def set_pt_def)
apply (wpsimp wp: set_object_valid_vspace_objs')
apply (clarsimp simp: obj_at_def)
apply (rule valid_entries_overwrite_0)
apply (fastforce simp:ran_def)
apply (drule bspec)
apply fastforce
apply (case_tac "pt pa")
apply simp
apply (case_tac pte,simp_all)
apply (rule valid_entries_overwrite_0)
apply (fastforce simp:ran_def)
apply (drule bspec)
apply fastforce
apply (case_tac "pt pa")
apply simp
apply (case_tac pte,simp_all)
done
lemma store_pdpte_valid_vspace_objs':
"\<lbrace>valid_vspace_objs'\<rbrace>
store_pdpte p pdpte \<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
apply (simp add: store_pdpte_def set_pdpt_def update_object_def, wp get_object_wp)
apply (simp add: store_pdpte_def set_pdpt_def)
apply (wpsimp wp: set_object_valid_vspace_objs')
apply (clarsimp simp: obj_at_def)
apply (rule valid_entries_overwrite_0)
apply (fastforce simp:ran_def)
apply (drule bspec)
apply fastforce
apply (case_tac "pd pa")
apply (rule valid_entries_overwrite_0)
apply (fastforce simp:ran_def)
apply (drule bspec)
apply fastforce
apply (case_tac "pd pa")
apply simp
apply (case_tac pdpte,simp_all)
apply (case_tac pdpte,simp_all)
@ -267,15 +271,16 @@ lemma store_pdpte_valid_vspace_objs':
lemma store_pml4e_valid_vspace_objs':
"\<lbrace>valid_vspace_objs'\<rbrace>
store_pml4e p pml4e \<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
apply (simp add: store_pml4e_def set_pml4_def update_object_def, wp get_object_wp)
apply (simp add: store_pml4e_def set_pml4_def)
apply (wpsimp wp: set_object_valid_vspace_objs')
apply (clarsimp simp: obj_at_def)
apply (rule valid_entries_overwrite_0)
apply (fastforce simp:ran_def)
apply (drule bspec)
apply fastforce
apply (case_tac "pm pa")
apply simp
apply (case_tac pml4e,simp_all)
apply (rule valid_entries_overwrite_0)
apply (fastforce simp:ran_def)
apply (drule bspec)
apply fastforce
apply (case_tac "pm pa")
apply simp
apply (case_tac pml4e,simp_all)
done
lemma unmap_page_valid_vspace_objs'[wp]:
@ -351,7 +356,7 @@ lemma mapM_x_copy_pml4e_updates:
apply (simp add: mapM_x_Cons)
apply wp
apply (thin_tac "valid P f Q" for P f Q)
apply (simp add: store_pml4e_def set_pml4_def set_object_def update_object_def
apply (simp add: store_pml4e_def set_pml4_def set_object_def
cong: bind_cong split del: if_split)
apply (wp get_object_wp get_pml4e_wp)
apply (clarsimp simp: obj_at_def a_type_simps mask_out_add_aligned[symmetric] word_size_bits_def
@ -560,17 +565,9 @@ lemma invoke_untyped_valid_vspace_objs'[wp]:
apply (wp | simp)+
done
lemma update_object_valid_vspace_objs'[wp]:
"\<lbrace>valid_vspace_objs' and K (obj_valid_vspace obj)\<rbrace>
update_object ptr obj
\<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
apply (simp add: update_object_def, wp get_object_wp)
apply (auto simp: fun_upd_def[symmetric] del: ballI elim: ball_ran_updI)
done
crunch valid_vspace_objs'[wp]: perform_asid_pool_invocation,
perform_asid_control_invocation "valid_vspace_objs'"
(ignore: delete_objects update_object
(ignore: delete_objects set_object
wp: static_imp_wp select_wp crunch_wps
simp: crunch_simps unless_def)

52
proof/invariant-abstract/X64/ArchVSpace_AI.thy
View File

@ -740,7 +740,7 @@ crunch valid_objs[wp]: unmap_page "valid_objs"
crunch caps_of_state [wp]: unmap_page "\<lambda>s. P (caps_of_state s)"
(wp: crunch_wps simp: crunch_simps)
(wp: crunch_wps simp: crunch_simps set_arch_obj_simps)
lemma set_cap_valid_slots[wp]:
"\<lbrace>valid_slots x2\<rbrace> set_cap cap (a, b)
@ -871,7 +871,7 @@ crunch typ_at [wp]: unmap_page "\<lambda>s. P (typ_at T p s)"
(wp: mapM_x_wp_inv_weak crunch_wps simp: crunch_simps)
crunch caps_of_state [wp]: unmap_pdpt "\<lambda>s. P (caps_of_state s)"
(wp: mapM_x_wp_inv_weak crunch_wps simp: crunch_simps)
(wp: mapM_x_wp_inv_weak crunch_wps simp: crunch_simps set_arch_obj_simps)
lemmas flush_table_typ_ats [wp] = abs_typ_at_lifts [OF flush_table_typ_at]
@ -1680,10 +1680,10 @@ lemma update_aobj_not_reachable:
"\<lbrace>\<lambda>s. lookup_refs (Some (ArchObj aobj)) vs_lookup_pages1_on_heap_obj \<subseteq> lookup_refs (kheap s p) vs_lookup_pages1_on_heap_obj
\<and> (b, p) \<in> (vs_lookup_pages s) \<and> (VSRef offset (Some ty), ptr) \<notin> vs_refs_pages (ArchObj aobj)
\<and> valid_asid_table (x64_asid_table (arch_state s)) s\<rbrace>
update_object p
set_object p
(ArchObj aobj)
\<lbrace>\<lambda>yb s. ([VSRef offset (Some ty)] @ b, ptr) \<notin> vs_lookup_pages s\<rbrace>"
apply (simp add: update_object_def set_object_def)
apply (simp add: set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: vs_lookup_pages_def)
apply (erule rtranclE[where b = "(VSRef offset (Some ty) # b, ptr)"])
@ -2005,7 +2005,7 @@ lemma unmap_pdpt_vs_lookup_pages_pre:
note ref_simps[simp] = vs_cap_ref_simps vs_ref_pages_simps
note ucast_simps[simp] = up_ucast_inj_eq ucast_up_ucast mask_asid_low_bits_ucast_ucast ucast_ucast_id
show ?thesis
apply (clarsimp simp: unmap_pdpt_def vs_cap_ref_simps store_pml4e_def)
apply (clarsimp simp: unmap_pdpt_def vs_cap_ref_simps store_pml4e_def set_arch_obj_simps)
apply wp
apply (rule update_aobj_not_reachable[where b = "[b,c]" for b c,simplified])
apply (strengthen lookup_refs_pml4_shrink_strg valid_arch_state_asid_table_strg not_in_vs_refs_pages_strg
@ -2076,14 +2076,14 @@ lemma unmap_pt_vs_lookup_pages_pre:
note ref_simps[simp] = vs_cap_ref_simps vs_ref_pages_simps
note ucast_simps[simp] = up_ucast_inj_eq ucast_up_ucast mask_asid_low_bits_ucast_ucast ucast_ucast_id
show ?thesis
apply (clarsimp simp: unmap_page_table_def vs_cap_ref_simps)
apply (clarsimp simp: unmap_page_table_def)
apply wp
apply (clarsimp simp: unmap_pd_def vs_cap_ref_simps store_pde_def)
apply (clarsimp simp: unmap_pd_def store_pde_def set_arch_obj_simps)
apply wp
apply (rule update_aobj_not_reachable[where b = "[b,c,d,e]" for b c d e,simplified])
apply (strengthen lookup_refs_pd_shrink_strg valid_arch_state_asid_table_strg not_in_vs_refs_pages_strg
| clarsimp )+
apply (strengthen | wp hoare_vcg_imp_lift hoare_vcg_all_lift | clarsimp simp: conj_ac)+
apply (strengthen | wp hoare_vcg_imp_lift hoare_vcg_all_lift | clarsimp)+
apply (wpc | wp get_pdpte_wp get_pml4e_wp get_pde_wp)+
apply ((simp add: lookup_pdpt_slot_def lookup_pd_slot_def | wp get_pdpte_wp get_pml4e_wp | wpc)+)[1]
apply (simp add: find_vspace_for_asid_def | wp | wpc)+
@ -2175,7 +2175,7 @@ lemma unmap_page_vs_lookup_pages_pre:
apply (clarsimp simp: unmap_page_def vs_cap_ref_simps)
apply (wp | wpc)+
(* X64SmallPage *)
apply (clarsimp simp: store_pte_def)
apply (clarsimp simp: store_pte_def set_arch_obj_simps)
apply wp
apply (rule update_aobj_not_reachable[where b = "[b,c,d,e,f]" for b c d e f,simplified])
apply (strengthen lookup_refs_pt_shrink_strg valid_arch_state_asid_table_strg not_in_vs_refs_pages_strg
@ -2184,7 +2184,7 @@ lemma unmap_page_vs_lookup_pages_pre:
apply (wpc | wp get_pte_wp get_pml4e_wp get_pde_wp get_pdpte_wp)+
apply ((simp add: lookup_pt_slot_def lookup_pd_slot_def lookup_pdpt_slot_def | wp get_pdpte_wp get_pml4e_wp get_pde_wp | wpc)+)[1]
(* X64LargePage *)
apply (clarsimp simp: store_pde_def)
apply (clarsimp simp: store_pde_def set_arch_obj_simps)
apply wp
apply (rule update_aobj_not_reachable[where b = "[b,c,d,e]" for b c d e,simplified])
apply (strengthen lookup_refs_pd_shrink_strg valid_arch_state_asid_table_strg not_in_vs_refs_pages_strg
@ -2193,7 +2193,7 @@ lemma unmap_page_vs_lookup_pages_pre:
apply (wpc | wp get_pte_wp get_pml4e_wp get_pde_wp get_pdpte_wp)+
apply ((simp add: lookup_pt_slot_def lookup_pd_slot_def lookup_pdpt_slot_def | wp get_pdpte_wp get_pml4e_wp get_pde_wp | wpc)+)[1]
(* X64HugePage *)
apply (clarsimp simp: store_pdpte_def)
apply (clarsimp simp: store_pdpte_def set_arch_obj_simps)
apply wp
apply (rule update_aobj_not_reachable[where b = "[b,c,d]" for b c d,simplified])
apply (strengthen lookup_refs_pdpt_shrink_strg valid_arch_state_asid_table_strg not_in_vs_refs_pages_strg
@ -2370,12 +2370,12 @@ lemma unmap_pd_vs_lookup_pages_pre:
note ref_simps[simp] = vs_cap_ref_simps vs_ref_pages_simps
note ucast_simps[simp] = up_ucast_inj_eq ucast_up_ucast mask_asid_low_bits_ucast_ucast ucast_ucast_id
show ?thesis
apply (clarsimp simp: unmap_pd_def vs_cap_ref_simps store_pdpte_def)
apply (clarsimp simp: unmap_pd_def store_pdpte_def set_arch_obj_simps)
apply wp
apply (rule update_aobj_not_reachable[where b = "[b,c,d]" for b c d,simplified])
apply (strengthen lookup_refs_pdpt_shrink_strg valid_arch_state_asid_table_strg not_in_vs_refs_pages_strg
| clarsimp )+
apply (strengthen | wp hoare_vcg_imp_lift hoare_vcg_all_lift | clarsimp simp: conj_ac)+
apply (strengthen | wp hoare_vcg_imp_lift hoare_vcg_all_lift | clarsimp)+
apply (wpc | wp get_pdpte_wp get_pml4e_wp )+
apply ((simp add: lookup_pdpt_slot_def | wp get_pml4e_wp | wpc)+)[1]
apply (simp add: find_vspace_for_asid_def | wp | wpc)+
@ -2585,7 +2585,7 @@ lemma mapM_x_swp_store_empty_pt':
apply (clarsimp simp: obj_at_def empty_table_def fun_eq_iff)
apply (rule hoare_seq_ext, assumption)
apply (thin_tac "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" for P f Q)
apply (simp add: store_pte_def update_object_def set_object_def)
apply (simp add: store_pte_def set_object_def set_arch_obj_simps)
apply (wp get_object_wp | simp)
apply (clarsimp simp: obj_at_def)
apply auto
@ -2604,7 +2604,7 @@ lemma mapM_x_swp_store_empty_pd':
apply (clarsimp simp: obj_at_def empty_table_def fun_eq_iff)
apply (rule hoare_seq_ext, assumption)
apply (thin_tac "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" for P f Q)
apply (simp add: store_pde_def update_object_def set_object_def)
apply (simp add: store_pde_def set_object_def set_arch_obj_simps)
apply (wp get_object_wp | simp)
apply (clarsimp simp: obj_at_def)
apply auto
@ -2638,7 +2638,7 @@ lemma mapM_x_swp_store_empty_pdpt':
apply (clarsimp simp: obj_at_def empty_table_def fun_eq_iff)
apply (rule hoare_seq_ext, assumption)
apply (thin_tac "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" for P f Q)
apply (simp add: store_pdpte_def update_object_def set_object_def)
apply (simp add: store_pdpte_def set_object_def set_arch_obj_simps)
apply (wp get_object_wp | simp)
apply (clarsimp simp: obj_at_def)
apply auto
@ -2883,28 +2883,28 @@ lemma valid_pt_cap_asidNone[simp]:
lemma update_aobj_zombies[wp]:
"\<lbrace>\<lambda>s. is_final_cap' cap s\<rbrace>
update_object ptr (ArchObj obj)
set_object ptr (ArchObj obj)
\<lbrace>\<lambda>_ s. is_final_cap' cap s\<rbrace>"
apply (simp add: is_final_cap'_def2)
apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift update_aobj_cte_wp_at)
apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift set_aobject_cte_wp_at)
done
crunch is_final_cap' [wp]: store_pde "is_final_cap' cap"
(wp: crunch_wps simp: crunch_simps ignore: update_object set_pd)
(wp: crunch_wps simp: crunch_simps set_arch_obj_simps ignore: set_object set_pd)
crunch is_final_cap' [wp]: store_pte "is_final_cap' cap"
(wp: crunch_wps simp: crunch_simps ignore: update_object set_pt)
(wp: crunch_wps simp: crunch_simps ignore: set_object set_pt)
crunch is_final_cap' [wp]: store_pdpte "is_final_cap' cap"
(wp: crunch_wps simp: crunch_simps ignore: update_object set_pdpt)
(wp: crunch_wps simp: crunch_simps set_arch_obj_simps ignore: set_object set_pdpt)
crunch is_final_cap' [wp]: store_pml4e "is_final_cap' cap"
(wp: crunch_wps simp: crunch_simps ignore: update_object set_pml4)
(wp: crunch_wps simp: crunch_simps set_arch_obj_simps ignore: set_object set_pml4)
lemma lookup_pages_shrink_store_pdpte:
"\<lbrace>\<lambda>s. p \<notin> vs_lookup_pages s\<rbrace> store_pdpte slot InvalidPDPTE \<lbrace>\<lambda>rv s. p \<notin> vs_lookup_pages s\<rbrace>"
apply (case_tac p)
apply (simp add: store_pdpte_def update_object_def set_object_def | wp get_object_wp | clarsimp)+
apply (simp add: store_pdpte_def set_object_def set_arch_obj_simps | wp get_object_wp | clarsimp)+
apply (simp add: vs_lookup_pages_def)
apply (drule_tac s1 = s in lookup_bound_estimate[OF vs_lookup_pages1_is_wellformed_lookup, rotated -1])
apply (simp add: fun_upd_def[symmetric])
@ -2918,7 +2918,7 @@ lemma lookup_pages_shrink_store_pdpte:
lemma lookup_pages_shrink_store_pde:
"\<lbrace>\<lambda>s. p \<notin> vs_lookup_pages s\<rbrace> store_pde slot InvalidPDE \<lbrace>\<lambda>rv s. p \<notin> vs_lookup_pages s\<rbrace>"
apply (case_tac p)
apply (simp add: store_pde_def update_object_def set_object_def | wp get_object_wp | clarsimp)+
apply (simp add: store_pde_def set_object_def set_arch_obj_simps | wp get_object_wp | clarsimp)+
apply (simp add: vs_lookup_pages_def)
apply (drule_tac s1 = s in lookup_bound_estimate[OF vs_lookup_pages1_is_wellformed_lookup, rotated -1])
apply (simp add: fun_upd_def[symmetric])
@ -2932,7 +2932,7 @@ lemma lookup_pages_shrink_store_pde:
lemma lookup_pages_shrink_store_pte:
"\<lbrace>\<lambda>s. p \<notin> vs_lookup_pages s\<rbrace> store_pte slot InvalidPTE \<lbrace>\<lambda>rv s. p \<notin> vs_lookup_pages s\<rbrace>"
apply (case_tac p)
apply (simp add: store_pte_def update_object_def set_object_def | wp get_object_wp | clarsimp)+
apply (simp add: store_pte_def set_object_def set_arch_obj_simps | wp get_object_wp | clarsimp)+
apply (simp add: vs_lookup_pages_def)
apply (drule_tac s1 = s in lookup_bound_estimate[OF vs_lookup_pages1_is_wellformed_lookup, rotated -1])
apply (simp add: fun_upd_def[symmetric])
@ -3707,7 +3707,7 @@ lemma store_asid_pool_entry_invs:
\<rbrace>
store_asid_pool_entry p asid pml4base \<lbrace>\<lambda>_. invs\<rbrace>"
unfolding store_asid_pool_entry_def
apply simp
apply (simp add: set_arch_obj_simps)
apply wp
apply simp
apply (intro impI allI conjI valid_table_caps_aobj_upd_invalid_pml4e invs_valid_table_caps , simp_all add: obj_at_def)