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

infoflow: replace valid_ko_at_arch with valid_arch_state 

Signed-off-by: Ryan Barry <ryan.barry@unsw.edu.au>
This commit is contained in:
Ryan Barry 2021-09-22 16:31:20 +10:00 committed by Gerwin Klein
parent 8124b326b4
commit 87c3045bec
16 changed files with 181 additions and 463 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/infoflow/ADT_IF.thy
View File

@ -1678,7 +1678,7 @@ lemma schedule_if_globals_equiv_scheduler[wp]:
apply (simp add: schedule_if_def)
apply wp
apply (wp globals_equiv_scheduler_inv'[where P="invs"] activate_thread_globals_equiv)
apply (simp add: invs_valid_ko_at_arch invs_valid_idle)
apply (simp add: invs_arch_state invs_valid_idle)
apply (wp | simp)+
done

255
proof/infoflow/ARM/ArchArch_IF.thy
View File

@ -12,10 +12,6 @@ context Arch begin global_naming ARM
named_theorems Arch_IF_assms
definition valid_ko_at_arch :: "det_state \<Rightarrow> bool" where
"valid_ko_at_arch \<equiv>
\<lambda>s. \<exists>pd. ko_at (ArchObj (PageDirectory pd)) (arm_global_pd (arch_state s)) s"
lemma irq_state_clearExMonitor[wp]:
"clearExMonitor \<lbrace>\<lambda>s. P (irq_state s)\<rbrace>"
by (simp add: clearExMonitor_def | wp modify_wp)+
@ -118,106 +114,63 @@ lemma store_word_offs_reads_respects[Arch_IF_assms]:
done
lemma set_simple_ko_globals_equiv[Arch_IF_assms]:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
set_simple_ko f ptr ep
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_simple_ko_def
apply (wpsimp wp: set_object_globals_equiv[THEN hoare_set_object_weaken_pre] get_object_wp
simp: partial_inv_def)+
apply (fastforce simp: obj_at_def valid_ko_at_arch_def)
apply (fastforce simp: obj_at_def valid_arch_state_def)
done
lemma set_simple_ko_valid_ko_at_arch[Arch_IF_assms, wp]:
"\<lbrace>valid_ko_at_arch\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>_. valid_ko_at_arch\<rbrace>"
unfolding set_simple_ko_def set_object_def
by (wpsimp wp: get_object_wp
simp: partial_inv_def a_type_def obj_at_def valid_ko_at_arch_def)+
lemma set_thread_state_globals_equiv[Arch_IF_assms]:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
set_thread_state ref ts
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_thread_state_def
apply (wp set_object_globals_equiv dxo_wp_weak |simp)+
apply (intro impI conjI allI)
apply (clarsimp simp: valid_ko_at_arch_def obj_at_def tcb_at_def2 get_tcb_def is_tcb_def
apply (clarsimp simp: valid_arch_state_def obj_at_def tcb_at_def2 get_tcb_def is_tcb_def
dest: get_tcb_SomeD
split: option.splits kernel_object.splits)+
done
lemma set_object_valid_ko_at_arch[wp]:
"\<lbrace>valid_ko_at_arch and (\<lambda>s. ptr = arm_global_pd (arch_state s)
\<longrightarrow> a_type obj = AArch APageDirectory)\<rbrace>
set_object ptr obj
\<lbrace>\<lambda>_. valid_ko_at_arch\<rbrace>"
by (wpsimp wp: set_object_wp
simp: a_type_def valid_ko_at_arch_def obj_at_def
split: kernel_object.splits arch_kernel_obj.splits if_splits)
lemma valid_ko_at_arch_exst_update[Arch_IF_assms, simp]:
"valid_ko_at_arch (trans_state f s) = valid_ko_at_arch s"
by (simp add: valid_ko_at_arch_def)
lemma set_thread_state_valid_ko_at_arch[Arch_IF_assms, wp]:
"set_thread_state ref ts \<lbrace>valid_ko_at_arch\<rbrace>"
unfolding set_thread_state_def
apply (wp set_object_valid_ko_at_arch dxo_wp_weak |simp)+
apply (fastforce simp: valid_ko_at_arch_def get_tcb_ko_at obj_at_def)
done
lemma set_cap_globals_equiv''[Arch_IF_assms]:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
set_cap cap p
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_cap_def
apply (simp only: split_def)
apply (wp set_object_globals_equiv hoare_vcg_all_lift get_object_wp | wpc | simp)+
apply (fastforce simp: valid_ko_at_arch_def obj_at_def is_tcb_def)+
done
lemma set_cap_valid_ko_at_arch[Arch_IF_assms, wp]:
"set_cap cap p \<lbrace>valid_ko_at_arch\<rbrace>"
apply (simp add: valid_ko_at_arch_def)
apply (rule hoare_ex_wp)
apply (rule hoare_pre)
apply (simp add: set_cap_def split_def)
apply (wp | wpc)+
apply (simp add: set_object_def)
apply (wp get_object_wp | wpc)+
apply (fastforce simp: obj_at_def)
apply (fastforce simp: valid_arch_state_def obj_at_def is_tcb_def)+
done
lemma as_user_globals_equiv[Arch_IF_assms]:
"\<lbrace>globals_equiv s and valid_ko_at_arch and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
as_user tptr f
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding as_user_def
apply (wpsimp wp: set_object_globals_equiv simp: split_def)
apply (clarsimp simp: valid_ko_at_arch_def get_tcb_def obj_at_def)
apply (clarsimp simp: valid_arch_state_def get_tcb_def obj_at_def)
done
end
context begin interpretation Arch .
requalify_consts
valid_ko_at_arch
requalify_facts
set_simple_ko_globals_equiv
set_simple_ko_valid_ko_at_arch
retype_region_irq_state_of_state
arch_perform_invocation_irq_state_of_state
declare
set_simple_ko_valid_ko_at_arch[wp]
retype_region_irq_state_of_state[wp]
arch_perform_invocation_irq_state_of_state[wp]
end
global_interpretation Arch_IF_1?: Arch_IF_1 valid_ko_at_arch
global_interpretation Arch_IF_1?: Arch_IF_1
proof goal_cases
interpret Arch .
case 1 show ?case
@ -227,16 +180,8 @@ qed
context Arch begin global_naming ARM
lemma valid_arch_state_ko_at_arch:
"valid_arch_state s \<Longrightarrow> valid_ko_at_arch s"
by (fastforce simp: valid_arch_state_def valid_ko_at_arch_def obj_at_def dest: a_type_pdD)
lemma invs_valid_ko_at_arch:
"invs s \<Longrightarrow> valid_ko_at_arch s"
by (simp add: invs_def valid_state_def valid_arch_state_ko_at_arch)
lemmas invs_imps =
invs_valid_vs_lookup invs_sym_refs invs_psp_aligned invs_distinct invs_valid_ko_at_arch
invs_valid_vs_lookup invs_sym_refs invs_psp_aligned invs_distinct invs_arch_state
invs_valid_global_objs invs_arch_state invs_valid_objs invs_valid_global_refs tcb_at_invs
invs_cur invs_kernel_mappings
@ -1109,13 +1054,13 @@ lemma delete_asid_reads_respects:
done
lemma set_asid_pool_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
set_asid_pool ptr pool
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_asid_pool_def
apply (wpsimp wp: set_object_globals_equiv[THEN hoare_set_object_weaken_pre]
simp: a_type_def)
apply (fastforce simp: valid_ko_at_arch_def obj_at_def)
apply (fastforce simp: valid_arch_state_def obj_at_def)
done
crunch globals_equiv[wp]: invalidate_hw_asid_entry "globals_equiv s"
@ -1199,13 +1144,13 @@ crunch globals_equiv[wp]: invalidate_tlb_by_asid "globals_equiv s"
(simp: invalidateLocalTLB_ASID_def wp: dmo_mol_globals_equiv ignore: machine_op_lift do_machine_op)
lemma set_pt_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
set_pt ptr pt
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_pt_def
apply (wpsimp wp: set_object_globals_equiv[THEN hoare_set_object_weaken_pre]
simp: a_type_def)
apply (fastforce simp: valid_ko_at_arch_def obj_at_def)
apply (fastforce simp: valid_arch_state_def obj_at_def)
done
crunch globals_equiv: store_pte "globals_equiv s"
@ -1279,7 +1224,9 @@ declare dmo_mol_globals_equiv[wp]
lemma unmap_page_table_globals_equiv:
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup
and valid_global_refs and valid_arch_state and globals_equiv st\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>"
and valid_global_refs and valid_arch_state and globals_equiv st\<rbrace>
unmap_page_table asid vaddr pt
\<lbrace>\<lambda>rv. globals_equiv st\<rbrace>"
unfolding unmap_page_table_def page_table_mapped_def
apply (wp store_pde_globals_equiv | wpc | simp add: cleanByVA_PoU_def)+
apply (rule_tac Q="\<lambda>_. globals_equiv st and (\<lambda>sa. lookup_pd_slot pd vaddr &&
@ -1288,59 +1235,19 @@ lemma unmap_page_table_globals_equiv:
apply (wp find_pd_for_asid_not_arm_global_pd hoare_post_imp_dc2E_actual | simp)+
done
lemma set_pt_valid_ko_at_arch[wp]:
"set_pt ptr pt \<lbrace>valid_ko_at_arch\<rbrace>"
unfolding set_pt_def
by (wpsimp wp: set_object_wp_strong simp: valid_ko_at_arch_def obj_at_def a_type_def)
crunch valid_ko_at_arch[wp]: store_pte "valid_ko_at_arch"
lemma mapM_x_swp_store_pte_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
mapM_x (swp store_pte A) slots
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
apply (rule_tac Q="\<lambda>_. globals_equiv s and valid_ko_at_arch" in hoare_strengthen_post)
apply (wp mapM_x_wp' store_pte_globals_equiv store_pte_valid_ko_at_arch | simp)+
apply (rule_tac Q="\<lambda>_. globals_equiv s and valid_arch_state" in hoare_strengthen_post)
apply (wp mapM_x_wp' store_pte_globals_equiv | simp)+
done
lemma mapM_x_swp_store_pte_valid_ko_at_arch[wp]:
"mapM_x (swp store_pte A) slots \<lbrace>valid_ko_at_arch\<rbrace>"
lemma mapM_x_swp_store_pte_valid_arch_state[wp]:
"mapM_x (swp store_pte A) slots \<lbrace>valid_arch_state\<rbrace>"
by (wp mapM_x_wp' | simp add: swp_def)+
lemma do_machine_op_valid_ko_at_arch[wp]:
"do_machine_op mol \<lbrace>valid_ko_at_arch\<rbrace>"
unfolding do_machine_op_def machine_op_lift_def split_def valid_ko_at_arch_def
by (wp modify_wp, simp)
lemma valid_ko_at_arch_interrupt_states[simp]:
"valid_ko_at_arch (s\<lparr>interrupt_states := f\<rparr>) = valid_ko_at_arch s"
by (simp add: valid_ko_at_arch_def)
lemma valid_ko_at_arch_next_asid[simp]:
"valid_ko_at_arch (s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := x\<rparr>\<rparr>) = valid_ko_at_arch s"
by (simp add: valid_ko_at_arch_def)
lemma valid_ko_at_arch_asid_map[simp]:
"valid_ko_at_arch (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := x\<rparr>\<rparr>) = valid_ko_at_arch s"
by (simp add: valid_ko_at_arch_def)
lemma valid_ko_at_arch_hwasid_table[simp]:
"valid_ko_at_arch (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := x\<rparr>\<rparr>) = valid_ko_at_arch s"
by (simp add: valid_ko_at_arch_def)
lemma valid_ko_at_arch_asid_table[simp]:
"valid_ko_at_arch (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := A\<rparr>\<rparr>) = valid_ko_at_arch s"
by (simp add: valid_ko_at_arch_def)
lemma valid_ko_at_arch_arch[simp]:
"arm_global_pd A = arm_global_pd (arch_state s)
\<Longrightarrow> valid_ko_at_arch (s\<lparr>arch_state := A\<rparr>) = valid_ko_at_arch s"
by (simp add: valid_ko_at_arch_def)
crunch valid_ko_at_arch[wp]: arm_context_switch, set_vm_root, set_pd "valid_ko_at_arch"
(wp: find_pd_for_asid_assert_wp crunch_wps simp: crunch_simps)
crunch valid_ko_at_arch[wp]: unmap_page_table "valid_ko_at_arch"
crunch valid_arch_state[wp]: unmap_page_table "valid_arch_state"
(wp: crunch_wps simp: crunch_simps a_type_simps)
definition authorised_for_globals_page_table_inv :: "page_table_invocation \<Rightarrow> 'z state \<Rightarrow> bool" where
@ -1361,7 +1268,7 @@ lemma perform_page_table_invocation_globals_equiv:
mapM_x_swp_store_pte_globals_equiv unmap_page_table_globals_equiv
| wpc | simp add: cleanByVA_PoU_def)+
apply (fastforce simp: authorised_for_globals_page_table_inv_def
valid_arch_state_def valid_ko_at_arch_def obj_at_def
valid_arch_state_def obj_at_def
dest: a_type_pdD)
done
@ -1390,10 +1297,10 @@ lemma flush_page_arm_global_pd[wp]:
by (wp | simp cong: if_cong split del: if_split)+
lemma mapM_swp_store_pte_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
mapM (swp store_pte A) slots
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (rule_tac Q="\<lambda> _. globals_equiv st and valid_ko_at_arch"
apply (rule_tac Q="\<lambda> _. globals_equiv st and valid_arch_state"
in hoare_strengthen_post)
apply (wp mapM_wp' store_pte_globals_equiv | simp)+
done
@ -1408,9 +1315,9 @@ lemma mapM_swp_store_pde_globals_equiv:
apply (wp mapM_wp' store_pde_globals_equiv | simp)+
done
lemma mapM_swp_store_pte_valid_ko_at_arch[wp]:
"mapM (swp store_pte A) slots \<lbrace>valid_ko_at_arch\<rbrace>"
by (wp mapM_wp' store_pte_valid_ko_at_arch | simp)+
lemma mapM_swp_store_pte_valid_arch_state[wp]:
"mapM (swp store_pte A) slots \<lbrace>valid_arch_state\<rbrace>"
by (wp mapM_wp' | simp)+
lemma mapM_x_swp_store_pde_globals_equiv :
"\<lbrace>globals_equiv st and (\<lambda>s. \<forall>x \<in> set slots. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))\<rbrace>
@ -1422,9 +1329,6 @@ lemma mapM_x_swp_store_pde_globals_equiv :
apply (wp mapM_x_wp' store_pde_globals_equiv | simp)+
done
crunch valid_ko_at_arch[wp]: flush_page "valid_ko_at_arch"
(wp: crunch_wps simp: crunch_simps)
lemma unmap_page_globals_equiv:
"\<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs
and valid_global_objs and valid_vs_lookup and valid_global_refs\<rbrace>
@ -1460,15 +1364,14 @@ lemma unmap_page_globals_equiv:
apply (simp)
apply (rule hoare_pre)
apply wp
apply (simp add: valid_arch_state_ko_at_arch)
apply (simp)
apply (simp)
apply (rule hoare_pre)
apply (wp dmo_cacheRangeOp_lift mapM_swp_store_pde_globals_equiv store_pde_globals_equiv
lookup_pt_slot_inv mapM_swp_store_pte_globals_equiv hoare_drop_imps
| simp add: cleanByVA_PoU_def)+
apply (simp add: valid_arch_state_ko_at_arch)
apply ((wp dmo_cacheRangeOp_lift mapM_swp_store_pde_globals_equiv store_pde_globals_equiv
lookup_pt_slot_inv mapM_swp_store_pte_globals_equiv hoare_drop_imps
| simp add: cleanByVA_PoU_def)+)[2]
apply (rule hoare_pre)
apply (wp store_pde_globals_equiv | simp add: valid_arch_state_ko_at_arch cleanByVA_PoU_def)+
apply (wp store_pde_globals_equiv | simp add: cleanByVA_PoU_def)+
apply (wp find_pd_for_asid_not_arm_global_pd hoare_drop_imps)+
apply (clarsimp)
done (* don't know what happened here. wp deleted globals_equiv from precon *)
@ -1491,15 +1394,14 @@ definition authorised_for_globals_page_inv ::
"authorised_for_globals_page_inv pgi \<equiv> \<lambda>s.
case pgi of PageMap asid cap ptr m \<Rightarrow> \<exists>slot. cte_wp_at (parent_for_refs m) slot s | _ \<Rightarrow> True"
crunch valid_ko_at_arch[wp]: unmap_page "valid_ko_at_arch"
crunch valid_arch_state[wp]: unmap_page "valid_arch_state"
(wp: crunch_wps)
lemma arm_global_pd_not_tcb:
"valid_ko_at_arch s \<Longrightarrow> get_tcb (arm_global_pd (arch_state s)) s = None"
unfolding valid_ko_at_arch_def
"valid_arch_state s \<Longrightarrow> get_tcb (arm_global_pd (arch_state s)) s = None"
unfolding valid_arch_state_def
apply (case_tac "get_tcb (arm_global_pd (arch_state s)) s")
apply simp
apply (clarsimp simp: valid_ko_at_arch_def get_tcb_ko_at obj_at_def)
apply (auto simp: get_tcb_ko_at obj_at_def)
done
lemma length_msg_lt_msg_max:
@ -1507,7 +1409,7 @@ lemma length_msg_lt_msg_max:
by (simp add: msg_registers_def msgRegisters_def upto_enum_def fromEnum_def enum_register msg_max_length_def)
lemma set_mrs_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch and (\<lambda>sa. thread \<noteq> idle_thread sa)\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)\<rbrace>
set_mrs thread buf msgs
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_mrs_def
@ -1529,9 +1431,6 @@ lemma set_mrs_globals_equiv:
apply (clarsimp simp:arm_global_pd_not_tcb)+
done
crunch valid_ko_at_arch[wp]: set_mrs valid_ko_at_arch
(wp: crunch_wps simp: crunch_simps arm_global_pd_not_tcb)
lemma perform_page_invocation_globals_equiv:
"\<lbrace>authorised_for_globals_page_inv pgi and valid_page_inv pgi and globals_equiv st and
valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and
@ -1548,7 +1447,7 @@ lemma perform_page_invocation_globals_equiv:
| wpc | simp add: do_machine_op_bind cleanByVA_PoU_def)+
by (auto simp: cte_wp_parent_not_global_pd authorised_for_globals_page_inv_def valid_page_inv_def
valid_slots_def valid_idle_def st_tcb_def2 ct_in_state_def pred_tcb_at_def obj_at_def
dest: valid_arch_state_ko_at_arch dest!: rev_subsetD[OF _ tl_subseteq])
dest!: rev_subsetD[OF _ tl_subseteq])
lemma retype_region_ASIDPoolObj_globals_equiv:
"\<lbrace>globals_equiv s and (\<lambda>sa. ptr \<noteq> arm_global_pd (arch_state s)) and (\<lambda>sa. ptr \<noteq> idle_thread sa)\<rbrace>
@ -1560,35 +1459,6 @@ lemma retype_region_ASIDPoolObj_globals_equiv:
apply (fastforce simp: globals_equiv_def idle_equiv_def tcb_at_def2)
done
lemma retype_region_ASIDPoolObj_valid_ko_at_arch:
"\<lbrace>valid_ko_at_arch and (\<lambda>s. ptr \<noteq> arm_global_pd (arch_state s))\<rbrace>
retype_region ptr 1 0 (ArchObject ASIDPoolObj) dev
\<lbrace>\<lambda>_. valid_ko_at_arch\<rbrace>"
supply retype_region_ext_extended.dxo_eq[simp del]
apply (simp add: retype_region_def)
apply (wp modify_wp dxo_wp_weak |simp add: trans_state_update[symmetric] del: trans_state_update)+
apply (clarsimp simp: valid_ko_at_arch_def)
apply (rule_tac x=pd in exI)
apply (fold fun_upd_def)
apply (clarsimp simp: fun_upd_def obj_at_def)
done
lemma detype_valid_ko_at_arch:
"\<lbrace>valid_ko_at_arch and (\<lambda>s. arm_global_pd (arch_state s) \<notin> {ptr..ptr + 2 ^ bits - 1})\<rbrace>
modify (detype {ptr..ptr + 2 ^ bits - 1})
\<lbrace>\<lambda>_. valid_ko_at_arch\<rbrace>"
apply (wp modify_wp)
apply (fastforce simp: valid_ko_at_arch_def detype_def obj_at_def)
done
lemma delete_objects_valid_ko_at_arch:
"\<lbrace>valid_ko_at_arch and (\<lambda>s. arm_global_pd (arch_state s) \<notin> ptr_range p b)
and K (is_aligned p b \<and> 2 \<le> b \<and> b < word_bits)\<rbrace>
delete_objects p b
\<lbrace>\<lambda>_. valid_ko_at_arch\<rbrace>"
unfolding delete_objects_def
by (wp detype_valid_ko_at_arch do_machine_op_valid_ko_at_arch | simp add: ptr_range_def)+
lemma perform_asid_control_invocation_globals_equiv:
notes delete_objects_invs[wp del]
notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
@ -1602,7 +1472,7 @@ lemma perform_asid_control_invocation_globals_equiv:
apply (wp modify_wp cap_insert_globals_equiv''
retype_region_ASIDPoolObj_globals_equiv[simplified]
retype_region_invs_extras(5)[where sz=pageBits]
retype_region_ASIDPoolObj_valid_ko_at_arch[simplified]
retype_region_invs_extras(6)[where sz=pageBits]
set_cap_globals_equiv
max_index_upd_invs_simple set_cap_no_overlap
set_cap_caps_no_overlap max_index_upd_caps_overlap_reserved
@ -1613,7 +1483,7 @@ lemma perform_asid_control_invocation_globals_equiv:
(* factor out the implication -- we know what the relevant components of the
cap referred to in the cte_wp_at are anyway from valid_aci, so just use
those directly to simplify the reasoning later on *)
apply (rule_tac Q="\<lambda>a b. globals_equiv s b \<and> invs b \<and> valid_ko_at_arch b \<and>
apply (rule_tac Q="\<lambda>a b. globals_equiv s b \<and> invs b \<and>
word1 \<noteq> arm_global_pd (arch_state b) \<and> word1 \<noteq> idle_thread b \<and>
(\<exists>idx. cte_wp_at ((=) (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \<and>
descendants_of cslot_ptr2 (cdt b) = {} \<and>
@ -1630,7 +1500,8 @@ lemma perform_asid_control_invocation_globals_equiv:
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (strengthen refl caps_region_kernel_window_imp[mk_strg I E])
apply (simp add: invs_valid_objs invs_cap_refs_in_kernel_window
atLeastatMost_subset_iff word_and_le2)
atLeastatMost_subset_iff word_and_le2
cong: conj_cong)
apply (rule conjI, rule descendants_range_caps_no_overlapI)
apply assumption
apply (simp add: cte_wp_at_caps_of_state)
@ -1639,10 +1510,10 @@ lemma perform_asid_control_invocation_globals_equiv:
apply (subst is_aligned_neg_mask_eq[THEN sym], assumption)
apply (simp add: word_bw_assocs pageBits_def mask_zero)
apply (wp add: delete_objects_invs_ex delete_objects_pspace_no_overlap[where dev=False]
delete_objects_globals_equiv delete_objects_valid_ko_at_arch hoare_vcg_ex_lift
delete_objects_globals_equiv hoare_vcg_ex_lift
del: Untyped_AI.delete_objects_pspace_no_overlap
| simp add: page_bits_def)+
apply (clarsimp simp: conj_comms invs_valid_ko_at_arch
apply (clarsimp simp: conj_comms
invs_psp_aligned invs_valid_objs valid_aci_def)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (frule_tac cap="UntypedCap False a b c" for a b c in caps_of_state_valid, assumption)
@ -1671,7 +1542,7 @@ lemma perform_asid_control_invocation_globals_equiv:
done
lemma perform_asid_pool_invocation_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace> perform_asid_pool_invocation api \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace> perform_asid_pool_invocation api \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding perform_asid_pool_invocation_def
apply (rule hoare_weaken_pre)
apply (wp modify_wp set_asid_pool_globals_equiv set_cap_globals_equiv''
@ -1697,7 +1568,6 @@ lemma arch_perform_invocation_globals_equiv:
perform_asid_control_invocation_globals_equiv
perform_asid_pool_invocation_globals_equiv)+
apply (auto simp: authorised_for_globals_arch_inv_def
dest: valid_arch_state_ko_at_arch
simp: invs_def valid_state_def valid_arch_inv_def invs_valid_vs_lookup)
done
@ -1714,15 +1584,6 @@ lemma find_pd_for_asid_authority3:
use_validE_R[OF _ find_pd_for_asid_lookup])
done
lemma as_user_valid_ko_at_arch[wp]:
"as_user thread f \<lbrace>valid_ko_at_arch\<rbrace>"
unfolding as_user_def
apply wp
apply (case_tac x)
apply (simp | wp select_wp)+
apply (fastforce simp: valid_ko_at_arch_def get_tcb_ko_at obj_at_def)
done
lemma valid_arch_arm_asid_table_unmap:
"valid_arch_state s \<and> tab = arm_asid_table (arch_state s)
\<longrightarrow> valid_arch_state
@ -1854,9 +1715,7 @@ lemma mapM_x_swp_store_pde_pas_refined_simple:
crunch valid_global_objs[wp]: arch_post_cap_deletion "valid_global_objs"
lemma get_thread_state_globals_equiv[wp]:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
get_thread_state ref
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
"get_thread_state ref \<lbrace>globals_equiv s\<rbrace>"
unfolding get_thread_state_def
by (wpsimp wp: set_object_globals_equiv dxo_wp_weak)
@ -1875,12 +1734,12 @@ lemma auth_ipc_buffers_mem_Write':
lemma thread_set_globals_equiv:
"(\<And>tcb. arch_tcb_context_get (tcb_arch (f tcb)) = arch_tcb_context_get (tcb_arch tcb))
\<Longrightarrow> \<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace> thread_set f tptr \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
\<Longrightarrow> \<lbrace>globals_equiv s and valid_arch_state\<rbrace> thread_set f tptr \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding thread_set_def
apply (wp set_object_globals_equiv)
apply simp
apply (intro impI conjI allI)
apply (fastforce simp: valid_ko_at_arch_def obj_at_def get_tcb_def)+
apply (fastforce simp: valid_arch_state_def obj_at_def get_tcb_def)+
apply (clarsimp simp: get_tcb_def tcb_at_def2 split: kernel_object.splits option.splits)
done
@ -1901,36 +1760,22 @@ requalify_facts
thread_set_globals_equiv
arch_post_modify_registers_cur_domain
arch_post_modify_registers_cur_thread
valid_arch_state_ko_at_arch
invs_valid_ko_at_arch
invs_imps
do_machine_op_valid_ko_at_arch
valid_ko_at_arch_interrupt_states
length_msg_lt_msg_max
set_mrs_globals_equiv
set_mrs_valid_ko_at_arch
store_word_offs_valid_ko_at_arch
arch_perform_invocation_globals_equiv
as_user_valid_ko_at_arch
as_user_globals_equiv
prepare_thread_delete_st_tcb_at_halted
make_arch_fault_msg_inv
check_valid_ipc_buffer_inv
arch_tcb_update_aux2
valid_ko_at_arch_interrupt_states
declare
arch_post_cap_deletion_valid_global_objs[wp]
get_thread_state_globals_equiv[wp]
arch_post_modify_registers_cur_domain[wp]
arch_post_modify_registers_cur_thread[wp]
do_machine_op_valid_ko_at_arch[wp]
valid_ko_at_arch_interrupt_states[wp]
set_mrs_valid_ko_at_arch[wp]
store_word_offs_valid_ko_at_arch[wp]
as_user_valid_ko_at_arch[wp]
prepare_thread_delete_st_tcb_at_halted[wp]
valid_ko_at_arch_interrupt_states[simp]
end

36
proof/infoflow/ARM/ArchFinalise_IF.thy
View File

@ -313,35 +313,21 @@ lemma set_irq_state_globals_equiv[Finalise_IF_assms]:
done
lemma set_notification_globals_equiv[Finalise_IF_assms]:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
set_notification ptr ntfn
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding set_simple_ko_def
apply (wp set_object_globals_equiv get_object_wp)
apply (fastforce simp: valid_ko_at_arch_def obj_at_def)
apply (fastforce simp: obj_at_def valid_arch_state_def)
done
lemma set_asid_pool_valid_ko_at_arch[wp]:
"\<lbrace>valid_ko_at_arch\<rbrace> set_asid_pool a b\<lbrace>\<lambda>_.valid_ko_at_arch\<rbrace>"
unfolding set_asid_pool_def
apply (wpsimp wp: set_object_wp_strong simp: a_type_def)
apply (fastforce simp: valid_ko_at_arch_def get_tcb_ko_at obj_at_def)
done
crunches thread_set, prepare_thread_delete, arch_post_cap_deletion, arch_finalise_cap
for valid_ko_at_arch[Finalise_IF_assms, wp]: "valid_ko_at_arch"
(wp: hoare_vcg_if_lift2 hoare_drop_imps select_wp modify_wp mapM_wp' dxo_wp_weak
simp: unless_def crunch_simps arm_global_pd_not_tcb
ignore: empty_slot_ext)
lemma delete_asid_globals_equiv:
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
delete_asid asid pd
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding delete_asid_def
by (wp set_vm_root_globals_equiv set_asid_pool_globals_equiv invalidate_asid_entry_globals_equiv
flush_space_globals_equiv invalidate_asid_entry_valid_ko_at_arch
| wpc | simp add: valid_arch_state_ko_at_arch)+
by (wpsimp wp: set_vm_root_globals_equiv set_asid_pool_globals_equiv
invalidate_asid_entry_globals_equiv flush_space_globals_equiv)
lemma pagebitsforsize_ge_2[simp]:
"2 \<le> pageBitsForSize vmpage_size"
@ -377,26 +363,16 @@ crunch globals_equiv[Finalise_IF_assms, wp]: prepare_thread_delete "globals_equi
(wp: dxo_wp_weak)
lemma set_bound_notification_globals_equiv[Finalise_IF_assms]:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
set_bound_notification ref ts
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_bound_notification_def
apply (wp set_object_globals_equiv dxo_wp_weak |simp)+
apply (intro impI conjI allI)
by (clarsimp simp: valid_ko_at_arch_def obj_at_def tcb_at_def2 get_tcb_def is_tcb_def
by (clarsimp simp: valid_arch_state_def obj_at_def tcb_at_def2 get_tcb_def is_tcb_def
dest: get_tcb_SomeD
split: option.splits kernel_object.splits)+
lemma set_bound_notification_valid_ko_at_arch[Finalise_IF_assms, wp]:
"set_bound_notification ref ts \<lbrace>valid_ko_at_arch\<rbrace>"
unfolding set_bound_notification_def
apply (wp set_object_valid_ko_at_arch dxo_wp_weak |simp)+
apply (fastforce simp: valid_ko_at_arch_def get_tcb_ko_at obj_at_def)
done
crunch valid_ko_at_arch[Finalise_IF_assms, wp]: set_original, set_cdt valid_ko_at_arch
(simp: valid_ko_at_arch_def)
end

7
proof/infoflow/ARM/ArchInterrupt_IF.thy
View File

@ -29,14 +29,13 @@ lemma arch_invoke_irq_control_reads_respects[Interrupt_IF_assms]:
done
lemma arch_invoke_irq_control_globals_equiv[Interrupt_IF_assms]:
"\<lbrace>globals_equiv st and valid_ko_at_arch and valid_global_objs\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
arch_invoke_irq_control ai
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (induct ai)
apply (simp add: setIRQTrigger_def)
apply (wp set_irq_state_valid_ko_at_arch set_irq_state_globals_equiv
set_irq_state_valid_global_objs cap_insert_globals_equiv'' dmo_mol_globals_equiv
| simp)+
apply (wpsimp wp: set_irq_state_globals_equiv set_irq_state_valid_global_objs
cap_insert_globals_equiv'' dmo_mol_globals_equiv)
done
lemma arch_invoke_irq_handler_globals_equiv[Interrupt_IF_assms, wp]:

5
proof/infoflow/ARM/ArchIpc_IF.thy
View File

@ -242,9 +242,6 @@ lemma arch_get_sanitise_register_info_reads_respects[Ipc_IF_assms, wp]:
declare arch_get_sanitise_register_info_inv[Ipc_IF_assms]
crunches handle_arch_fault_reply
for arch_get_sanitise_register_info[Ipc_IF_assms, wp]: "valid_ko_at_arch"
lemma lookup_ipc_buffer_ptr_range'[Ipc_IF_assms]:
"\<lbrace>valid_objs\<rbrace>
lookup_ipc_buffer True thread
@ -270,7 +267,7 @@ lemma lookup_ipc_buffer_aligned'[Ipc_IF_assms]:
done
lemma handle_arch_fault_reply_globals_equiv[Ipc_IF_assms]:
"\<lbrace>globals_equiv st and valid_ko_at_arch and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
handle_arch_fault_reply vmf thread x y
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
by (wpsimp simp: handle_arch_fault_reply_def)+

2
proof/infoflow/ARM/ArchScheduler_IF.thy
View File

@ -125,7 +125,7 @@ lemma thread_set_context_globals_equiv[Scheduler_IF_assms]:
apply (subgoal_tac "t \<noteq> arm_global_pd (arch_state s)")
apply (clarsimp simp: idle_equiv_def globals_equiv_def tcb_at_def2 get_tcb_def idle_context_def)
apply (clarsimp split: option.splits kernel_object.splits)
apply (drule arm_global_pd_not_tcb[OF invs_valid_ko_at_arch])
apply (drule arm_global_pd_not_tcb[OF invs_arch_state])
apply clarsimp
done

6
proof/infoflow/ARM/ArchSyscall_IF.thy
View File

@ -19,14 +19,14 @@ lemma globals_equiv_irq_state_update[Syscall_IF_assms, simp]:
by (auto simp: globals_equiv_def idle_equiv_def)
lemma thread_set_globals_equiv'[Syscall_IF_assms]:
"\<lbrace>globals_equiv s and valid_ko_at_arch and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
thread_set f tptr
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding thread_set_def
apply (wp set_object_globals_equiv)
apply simp
apply (intro impI conjI allI)
apply (fastforce simp: valid_ko_at_arch_def obj_at_def get_tcb_def)+
apply (fastforce simp: obj_at_def get_tcb_def valid_arch_state_def)+
done
lemma arch_perform_invocation_reads_respects_g[Syscall_IF_assms]:
@ -96,7 +96,7 @@ lemma handle_hypervisor_fault_reads_respects[Syscall_IF_assms]:
by (cases hypfault_type; wpsimp)
lemma handle_vm_fault_globals_equiv[Syscall_IF_assms]:
"\<lbrace>globals_equiv st and valid_ko_at_arch and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
handle_vm_fault thread vmfault_type
\<lbrace>\<lambda>r. globals_equiv st\<rbrace>"
apply (cases vmfault_type)

6
proof/infoflow/ARM/ArchTcb_IF.thy
View File

@ -34,10 +34,6 @@ lemma cap_ne_global_pd:
apply blast
done
lemma valid_ko_at_arch_irq_state_independent_A[Tcb_IF_assms, simp, intro!]:
"irq_state_independent_A (valid_ko_at_arch)"
by (auto simp: irq_state_independent_A_def valid_ko_at_arch_def)
lemma valid_arch_caps_vs_lookup[Tcb_IF_assms]:
"valid_arch_caps s \<Longrightarrow> valid_vs_lookup s"
by (simp add: valid_arch_caps_def)
@ -61,7 +57,7 @@ lemma no_cap_to_idle_thread''[Tcb_IF_assms]:
crunches arch_post_modify_registers
for globals_equiv[Tcb_IF_assms, wp]: "globals_equiv st"
and valid_ko_at_arch[Tcb_IF_assms, wp]: valid_ko_at_arch
and valid_arch_state[Tcb_IF_assms, wp]: valid_arch_state
lemma arch_post_modify_registers_reads_respects_f[Tcb_IF_assms, wp]:
"reads_respects_f aag l \<top> (arch_post_modify_registers cur t)"

27
proof/infoflow/Arch_IF.thy
View File

@ -369,8 +369,7 @@ crunch irq_state_of_state[wp]: cancel_badged_sends "\<lambda>s. P (irq_state_of_
locale Arch_IF_1 =
fixes valid_ko_at_arch :: "det_state \<Rightarrow> bool"
and aag :: "'a PAS"
fixes aag :: "'a PAS"
assumes arch_post_cap_deletion_valid_global_refs:
"arch_post_cap_deletion acap \<lbrace>\<lambda>s :: det_state. valid_global_refs s\<rbrace>"
and arch_post_cap_deletion_irq_state_of_state[wp]:
@ -399,30 +398,22 @@ locale Arch_IF_1 =
and store_word_offs_reads_respects:
"reads_respects aag l \<top> (store_word_offs ptr offs v)"
and set_endpoint_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
set_endpoint ptr ep
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
and set_cap_globals_equiv'':
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
set_cap cap p
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
and set_thread_state_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
set_thread_state ref ts
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
and as_user_globals_equiv:
"\<And>f :: unit user_monad.
\<lbrace>globals_equiv s and valid_ko_at_arch and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
as_user tptr f
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
and set_endpoint_valid_ko_at_arch[wp]:
"set_endpoint ptr ep \<lbrace>valid_ko_at_arch\<rbrace>"
and set_cap_valid_ko_at_arch[wp]:
"set_cap cap p \<lbrace>valid_ko_at_arch\<rbrace>"
and set_thread_state_valid_ko_at_arch[wp]:
"set_thread_state ref ts \<lbrace>valid_ko_at_arch\<rbrace>"
and valid_ko_at_arch_exst_update[simp]:
"\<And>f. valid_ko_at_arch (trans_state f s) = valid_ko_at_arch s"
begin
crunch valid_global_refs[wp]: empty_slot "\<lambda>s :: det_state. valid_global_refs s"
@ -483,10 +474,8 @@ lemma set_mrs_reads_respects:
apply (auto intro: reads_affects_equiv_get_tcb_eq)
done
crunch valid_ko_at_arch[wp]: set_untyped_cap_as_full valid_ko_at_arch
lemma cap_insert_globals_equiv'':
"\<lbrace>globals_equiv s and valid_global_objs and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace>
cap_insert new_cap src_slot dest_slot
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding cap_insert_def
@ -494,13 +483,13 @@ lemma cap_insert_globals_equiv'':
set_cap_globals_equiv'' dxo_wp_weak hoare_drop_imps)
lemma set_message_info_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
set_message_info thread info
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_message_info_def by (wp as_user_globals_equiv)
lemma cancel_badged_sends_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
cancel_badged_sends epptr badge
\<lbrace>\<lambda>_. globals_equiv s\<rbrace> "
unfolding cancel_badged_sends_def

87
proof/infoflow/Finalise_IF.thy
View File

@ -24,13 +24,7 @@ locale Finalise_IF_1 =
"pas_domains_distinct aag
\<Longrightarrow> reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (set_thread_state ref ts)"
and set_bound_notification_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace> set_bound_notification ref nopt \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
and set_bound_notification_valid_ko_at_arch[wp]:
"set_bound_notification ref nopt \<lbrace>valid_ko_at_arch\<rbrace>"
and set_original_valid_ko_at_arch[wp]:
"set_original slot v \<lbrace>valid_ko_at_arch\<rbrace>"
and set_cdt_valid_ko_at_arch[wp]:
"set_cdt ct \<lbrace>valid_ko_at_arch\<rbrace>"
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace> set_bound_notification ref nopt \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
and set_thread_state_runnable_reads_respects:
"\<lbrakk> pas_domains_distinct aag; runnable ts \<rbrakk> \<Longrightarrow> reads_respects aag l \<top> (set_thread_state ref ts)"
and set_bound_notification_none_reads_respects:
@ -56,7 +50,7 @@ locale Finalise_IF_1 =
arch_finalise_cap acap ex
\<lbrace>\<lambda>rv s :: det_state. \<forall>t \<in> Access.obj_refs (fst rv). halted_if_tcb t s\<rbrace>"
and set_notification_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
set_notification ntfnptr ntfn
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
and arch_post_cap_deletion_globals_equiv[wp]:
@ -70,14 +64,6 @@ locale Finalise_IF_1 =
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
and prepare_thread_delete_globals_equiv[wp]:
"prepare_thread_delete t \<lbrace>globals_equiv st\<rbrace>"
and thread_set_valid_ko_at_arch[wp]:
"\<And>f. thread_set f t \<lbrace>valid_ko_at_arch\<rbrace>"
and prepare_thread_delete_valid_ko_at_arch[wp]:
"prepare_thread_delete t \<lbrace>valid_ko_at_arch\<rbrace>"
and arch_post_cap_deletion_valid_ko_at_arch[wp]:
"arch_post_cap_deletion acap \<lbrace>valid_ko_at_arch\<rbrace>"
and arch_finalise_cap_valid_ko_at_arch[wp]:
"arch_finalise_cap acap ex \<lbrace>valid_ko_at_arch\<rbrace>"
begin
lemma set_irq_state_reads_respects:
@ -1003,7 +989,6 @@ context Finalise_IF_1 begin
lemma reply_cancel_ipc_reads_respects_f:
assumes domains_distinct[wp]: "pas_domains_distinct aag"
notes gets_ev[wp del] thread_set_valid_ko_at_arch[wp del]
shows "reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs
and tcb_at tptr and K (is_subject aag tptr))
(reply_cancel_ipc tptr)"
@ -1428,14 +1413,14 @@ lemma globals_equiv_interrupt_states_update:
by (auto simp: globals_equiv_def idle_equiv_def)
lemma cancel_all_ipc_globals_equiv':
"cancel_all_ipc epptr \<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>"
"cancel_all_ipc epptr \<lbrace>globals_equiv st and valid_arch_state\<rbrace>"
unfolding cancel_all_ipc_def
by (wp mapM_x_wp[OF _ subset_refl] set_thread_state_globals_equiv
set_simple_ko_globals_equiv hoare_vcg_all_lift get_object_inv dxo_wp_weak
| wpc | simp | wp (once) hoare_drop_imps)+
lemma cancel_all_ipc_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
cancel_all_ipc epptr
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
by (fastforce intro: hoare_strengthen_post[OF cancel_all_ipc_globals_equiv'])
@ -1443,27 +1428,15 @@ lemma cancel_all_ipc_globals_equiv:
crunch valid_global_objs: fast_finalise "valid_global_objs"
(wp: crunch_wps dxo_wp_weak ignore: reschedule_required)
lemma tcb_sched_action_enqueue_valid_ko_at_arch[wp]:
"tcb_sched_action tcb_sched_enqueue word \<lbrace>valid_ko_at_arch\<rbrace>"
by (wpsimp simp: tcb_sched_action_def etcb_at_def)
lemma tcb_sched_action_dequeue_valid_ko_at_arch[wp]:
"tcb_sched_action tcb_sched_dequeue word \<lbrace>valid_ko_at_arch\<rbrace>"
by (wpsimp simp: tcb_sched_action_def etcb_at_def)
crunch valid_ko_at_arch[wp]: set_message_info "valid_ko_at_arch"
crunch valid_ko_at_arch[wp]: set_extra_badge "valid_ko_at_arch"
crunch valid_ko_at_arch[wp]: copy_mrs "valid_ko_at_arch" (wp: mapM_wp')
lemma cancel_all_signals_globals_equiv':
"cancel_all_signals epptr \<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>"
"cancel_all_signals epptr \<lbrace>globals_equiv st and valid_arch_state\<rbrace>"
unfolding cancel_all_signals_def
by (wp mapM_x_wp[OF _ subset_refl] set_thread_state_globals_equiv
set_simple_ko_globals_equiv hoare_vcg_all_lift get_object_inv dxo_wp_weak
| wpc | simp | wp (once) hoare_drop_imps)+
lemma cancel_all_signals_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
cancel_all_signals epptr
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
by (fastforce intro: hoare_strengthen_post[OF cancel_all_signals_globals_equiv'])
@ -1472,32 +1445,22 @@ lemma cancel_all_signals_globals_equiv:
context Finalise_IF_1 begin
lemma unbind_notification_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
unbind_notification t
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding unbind_notification_def
by (wpsimp wp: gbn_wp set_bound_notification_globals_equiv set_notification_globals_equiv)
lemma unbind_maybe_notification_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
unbind_maybe_notification a
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding unbind_maybe_notification_def
by (wpsimp wp: gbn_wp set_bound_notification_globals_equiv
set_notification_globals_equiv get_simple_ko_wp)
lemma unbind_notification_valid_ko_at_arch[wp]:
"unbind_notification t \<lbrace>valid_ko_at_arch\<rbrace>"
unfolding unbind_notification_def
by (wpsimp wp: gbn_wp set_bound_notification_valid_ko_at_arch)+
lemma unbind_maybe_notification_valid_ko_at_arch[wp]:
"unbind_maybe_notification a \<lbrace>valid_ko_at_arch\<rbrace>"
unfolding unbind_maybe_notification_def
by (wpsimp wp: gbn_wp set_bound_notification_valid_ko_at_arch get_simple_ko_wp)
lemma fast_finalise_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
fast_finalise cap final
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (cases cap)
@ -1505,21 +1468,10 @@ lemma fast_finalise_globals_equiv:
unbind_maybe_notification_globals_equiv
simp: when_def split_del: if_split)+
crunch valid_ko_at_arch[wp]: fast_finalise "valid_ko_at_arch"
(wp: mapM_x_wp' dxo_wp_weak ignore: reschedule_required)
crunch valid_ko_at_arch[wp]: cap_insert "valid_ko_at_arch"
(wp: hoare_drop_imps dxo_wp_weak simp: crunch_simps simp_del: cap_insert_ext_extended.dxo_eq)
lemma transfer_caps_valid_ko_at_arch[wp]:
"transfer_caps a b c d e \<lbrace>valid_ko_at_arch\<rbrace>"
unfolding transfer_caps_def
by (wpsimp wp: transfer_caps_loop_pres cap_insert_valid_ko_at_arch)
crunch globals_equiv[wp]: deleted_irq_handler "globals_equiv st"
lemma empty_slot_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace> empty_slot s b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace> empty_slot s b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding empty_slot_def post_cap_deletion_def
by (wpsimp wp: set_cap_globals_equiv'' set_original_globals_equiv hoare_vcg_if_lift2
set_cdt_globals_equiv dxo_wp_weak hoare_drop_imps hoare_vcg_all_lift)
@ -1530,19 +1482,13 @@ crunch globals_equiv: cap_delete_one "globals_equiv st"
(*FIXME: Lots of this stuff should be in arch *)
crunch globals_equiv[wp]: deleting_irq_handler "globals_equiv st"
crunch valid_ko_at_arch[wp]: finalise_cap "valid_ko_at_arch"
(wp: hoare_vcg_if_lift2 hoare_drop_imps select_wp modify_wp mapM_wp' dxo_wp_weak
simp: unless_def crunch_simps
ignore: empty_slot_ext)
crunch valid_ko_at_arch[wp]: setup_reply_master "valid_ko_at_arch"
crunch globals_equiv[wp]: cancel_ipc "globals_equiv st"
(wp: mapM_x_wp select_inv hoare_drop_imps hoare_vcg_if_lift2 cancel_signal_valid_ko_at_arch
simp: unless_def)
(wp: mapM_x_wp select_inv hoare_drop_imps hoare_vcg_if_lift2 simp: unless_def)
lemma suspend_globals_equiv[ wp]:
"\<lbrace>globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_ko_at_arch\<rbrace> suspend t \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
"\<lbrace>globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state\<rbrace>
suspend t
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding suspend_def update_restart_pc_def
apply (wp tcb_sched_action_extended.globals_equiv dxo_wp_weak)
apply simp
@ -1558,6 +1504,9 @@ lemma suspend_globals_equiv[ wp]:
apply auto
done
crunches unbind_notification
for valid_arch_state[wp]: valid_arch_state
lemma finalise_cap_globals_equiv:
"\<lbrace>globals_equiv st and (\<lambda>s. \<forall>p. cap = ThreadCap p \<longrightarrow> p \<noteq> idle_thread s)
and valid_global_objs and valid_arch_state and pspace_aligned
@ -1569,7 +1518,7 @@ lemma finalise_cap_globals_equiv:
cancel_all_signals_globals_equiv cancel_all_signals_valid_global_objs
arch_finalise_cap_globals_equiv unbind_maybe_notification_globals_equiv
unbind_notification_globals_equiv liftM_wp when_def
| clarsimp simp: valid_arch_state_ko_at_arch | intro impI conjI)+
| clarsimp | intro impI conjI)+
end

21
proof/infoflow/Interrupt_IF.thy
View File

@ -20,7 +20,7 @@ locale Interrupt_IF_1 =
"reads_respects aag l (K (arch_authorised_irq_ctl_inv aag irq_ctl_inv))
(arch_invoke_irq_control irq_ctl_inv)"
and arch_invoke_irq_control_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and valid_global_objs\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
arch_invoke_irq_control ai
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
and arch_invoke_irq_handler_globals_equiv[wp]:
@ -73,21 +73,21 @@ lemma invoke_irq_control_reads_respects:
done
lemma invoke_irq_control_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and valid_global_objs\<rbrace> invoke_irq_control a
"\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
invoke_irq_control a
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (induct a)
apply (wp set_irq_state_valid_ko_at_arch set_irq_state_globals_equiv cap_insert_globals_equiv''
set_irq_state_valid_global_objs arch_invoke_irq_control_globals_equiv
| simp)+
apply (wpsimp wp: set_irq_state_globals_equiv cap_insert_globals_equiv''
set_irq_state_valid_global_objs arch_invoke_irq_control_globals_equiv)+
done
lemma invoke_irq_handler_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and valid_global_objs\<rbrace>
invoke_irq_handler a
"\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
invoke_irq_handler a
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (induct a)
by (wpsimp wp: modify_wp cap_insert_globals_equiv'' cap_delete_one_globals_equiv
cap_delete_one_valid_ko_at_arch cap_delete_one_valid_global_objs)+
by (wpsimp wp: modify_wp cap_insert_globals_equiv''
cap_delete_one_globals_equiv cap_delete_one_valid_global_objs)+
subsection "reads_respects_g"
@ -102,11 +102,10 @@ lemma invoke_irq_handler_reads_respects_f_g:
apply (rule invoke_irq_handler_reads_respects_f[OF domains_distinct])
apply (rule doesnt_touch_globalsI)
apply (wp invoke_irq_handler_globals_equiv | simp)+
apply (simp add: invs_valid_ko_at_arch invs_valid_global_objs)
by auto
lemma invoke_irq_control_reads_respects_g:
"reads_respects_g aag l (valid_global_objs and valid_ko_at_arch
"reads_respects_g aag l (valid_global_objs and valid_arch_state
and K (authorised_irq_ctl_inv aag i))
(invoke_irq_control i)"
apply (rule equiv_valid_guard_imp[OF reads_respects_g])

99
proof/infoflow/Ipc_IF.thy
View File

@ -160,8 +160,6 @@ locale Ipc_IF_1 =
"reads_respects aag l (K (aag_can_read aag thread)) (handle_arch_fault_reply afault thread x y)"
and arch_get_sanitise_register_info_reads_respects[wp]:
"reads_respects aag l \<top> (arch_get_sanitise_register_info t)"
and handle_arch_fault_reply_valid_ko_at_arch[wp]:
"handle_arch_fault_reply vmf t x y \<lbrace>valid_ko_at_arch\<rbrace>"
and arch_get_sanitise_register_info_valid_global_objs[wp]:
"arch_get_sanitise_register_info t \<lbrace>\<lambda>s :: det_state. valid_global_objs s\<rbrace>"
and handle_arch_fault_reply_valid_global_objs[wp]:
@ -175,7 +173,7 @@ locale Ipc_IF_1 =
lookup_ipc_buffer True t
\<lbrace>\<lambda>rv s :: det_state. rv = Some buf' \<longrightarrow> is_aligned buf' msg_align_bits\<rbrace>"
and handle_arch_fault_reply_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
handle_arch_fault_reply vmf thread x y
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
begin
@ -1609,8 +1607,6 @@ lemma lookup_ipc_buffer_has_read_auth':
apply (drule sym, simp)
done
crunch valid_ko_at_arch[wp]: handle_fault_reply valid_ko_at_arch
end
context Ipc_IF_2 begin
@ -1652,7 +1648,7 @@ lemma do_reply_transfer_reads_respects_f:
cap_delete_one_silc_inv reads_respects_f[OF thread_get_reads_respects]
reads_respects_f[OF get_thread_state_rev]
| simp add: invs_valid_objs invs_psp_aligned invs_valid_global_refs
invs_distinct invs_arch_state invs_valid_ko_at_arch
invs_distinct invs_arch_state
invs_psp_aligned invs_vspace_objs invs_arch_state
| rule conjI
| elim conjE
@ -1707,7 +1703,7 @@ section "globals_equiv"
subsection "Sync IPC"
lemma setup_caller_cap_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch and valid_global_objs\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state and valid_global_objs\<rbrace>
setup_caller_cap sender receiver grant
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding setup_caller_cap_def
@ -1721,7 +1717,7 @@ lemma set_extra_badge_globals_equiv:
by (wp store_word_offs_globals_equiv)
lemma transfer_caps_loop_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and valid_global_objs\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
transfer_caps_loop ep rcv_buffer n caps slots mi
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
proof (induct caps arbitrary: slots n mi)
@ -1740,8 +1736,8 @@ next
apply (rule Cons.hyps)
apply (simp)
apply (wp cap_insert_globals_equiv'')
apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arch and valid_global_objs"
and E="\<lambda>_. globals_equiv st and valid_ko_at_arch and valid_global_objs"
apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs"
and E="\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs"
in hoare_post_impErr)
apply (simp add: whenE_def, rule conjI)
apply (rule impI, wp)+
@ -1752,14 +1748,14 @@ next
qed
lemma transfer_caps_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and valid_global_objs\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs\<rbrace>
transfer_caps info caps endpoint receiver recv_buffer
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding transfer_caps_def
by (wp transfer_caps_loop_globals_equiv | wpc | simp)+
lemma copy_mrs_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
copy_mrs sender sbuf receiver rbuf n
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding copy_mrs_def including no_pre
@ -1769,7 +1765,7 @@ lemma copy_mrs_globals_equiv:
apply (wp store_word_offs_globals_equiv)+
apply fastforce
apply simp
apply (rule_tac Q="\<lambda>_. globals_equiv s and valid_ko_at_arch and (\<lambda>sa. receiver \<noteq> idle_thread sa)"
apply (rule_tac Q="\<lambda>_. globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)"
in hoare_strengthen_post)
apply (wp mapM_wp' as_user_globals_equiv)
apply (simp)
@ -1785,7 +1781,7 @@ lemma validE_to_valid:
done
lemma do_normal_transfer_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace>
do_normal_transfer sender sbuf endpoint badge grant receiver rbuf
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding do_normal_transfer_def
@ -1797,7 +1793,7 @@ lemma do_normal_transfer_globals_equiv:
done
lemma do_fault_transfer_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace>
do_fault_transfer badge sender receiver buf
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding do_fault_transfer_def
@ -1813,9 +1809,6 @@ lemma do_fault_transfer_globals_equiv:
lemma set_collection: "a = {x. x\<in>a}"
by simp
crunch valid_ko_at_arch[wp]: do_ipc_transfer "valid_ko_at_arch"
(wp: make_arch_fault_msg_inv)
lemma valid_ep_send_enqueue:
"\<lbrakk> ko_at (Endpoint (SendEP (t # ts))) a s; valid_objs s \<rbrakk>
\<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> SendEP (b # bs)) s"
@ -1835,14 +1828,14 @@ lemma case_list_cons_cong:
context Ipc_IF_1 begin
lemma do_ipc_transfer_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and valid_objs and valid_arch_state and valid_global_refs
"\<lbrace>globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs
and pspace_distinct and pspace_aligned
and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
do_ipc_transfer sender ep badge grant receiver
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding do_ipc_transfer_def
apply (wp do_normal_transfer_globals_equiv do_fault_transfer_globals_equiv | wpc)+
apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arch and valid_global_objs and
apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs and
(\<lambda>sa. receiver \<noteq> idle_thread sa) and
(\<lambda>sa. (\<forall>rb. recv_buffer = Some rb
\<longrightarrow> auth_ipc_buffers sa receiver = ptr_range rb msg_align_bits) \<and>
@ -1862,7 +1855,7 @@ lemma send_ipc_globals_equiv:
unfolding send_ipc_def
apply (wp set_simple_ko_globals_equiv set_thread_state_globals_equiv
setup_caller_cap_globals_equiv | wpc)+
apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arch and valid_global_objs"
apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs"
in hoare_strengthen_post[rotated])
apply (fastforce)
apply (wp set_thread_state_globals_equiv dxo_wp_weak | simp)+
@ -1877,7 +1870,7 @@ lemma send_ipc_globals_equiv:
(\<lambda>s. sym_refs (state_refs_of s)) and valid_idle"
in hoare_strengthen_post)
apply (wp get_simple_ko_sp)
apply (clarsimp simp: valid_arch_state_ko_at_arch)+
apply (clarsimp)+
apply (rule context_conjI)
apply (rule valid_ep_recv_dequeue')
apply (simp)+
@ -1898,7 +1891,7 @@ lemma receive_ipc_globals_equiv:
setup_caller_cap_globals_equiv dxo_wp_weak as_user_globals_equiv
| wpc
| simp split del: if_split)+
apply (rule hoare_strengthen_post[where Q= "\<lambda>_. globals_equiv st and valid_ko_at_arch
apply (rule hoare_strengthen_post[where Q= "\<lambda>_. globals_equiv st and valid_arch_state
and valid_global_objs"])
apply (wp do_ipc_transfer_globals_equiv as_user_globals_equiv)
apply clarsimp
@ -1910,8 +1903,7 @@ lemma receive_ipc_globals_equiv:
apply (rule hoare_pre)
apply (wpc)
apply (rule fail_wp | rule return_wp)+
by (auto intro: valid_arch_state_ko_at_arch valid_ep_send_enqueue
simp: neq_Nil_conv cong: case_list_cons_cong)
by (auto intro: valid_ep_send_enqueue simp: neq_Nil_conv cong: case_list_cons_cong)
end
@ -1939,10 +1931,10 @@ lemma update_waiting_ntfn_globals_equiv:
supply possible_switch_to_extended.dxo_eq[simp del]
apply (wpsimp wp: set_thread_state_globals_equiv as_user_globals_equiv
set_notification_globals_equiv dxo_wp_weak)
by (auto intro: valid_arch_state_ko_at_arch simp: neq_Nil_conv)
by (auto simp: neq_Nil_conv)
lemma cancel_ipc_blocked_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and st_tcb_at receive_blocked a\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and st_tcb_at receive_blocked a\<rbrace>
cancel_ipc a
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding cancel_ipc_def
@ -1971,11 +1963,10 @@ lemma send_signal_globals_equiv:
apply clarsimp
apply (frule (1) sym_refs_ko_atD)
apply (intro allI impI conjI)
prefer 8
prefer 4
apply clarsimp
apply (frule_tac t="idle_thread sa" and P="\<lambda>ref. \<not> idle ref" in ntfn_queued_st_tcb_at')
by (auto intro: valid_arch_state_ko_at_arch
simp: pred_tcb_at_def obj_at_def valid_idle_def receive_blocked_def)
by (auto simp: pred_tcb_at_def obj_at_def valid_idle_def receive_blocked_def)
(* FIXME: belongs in Arch_IF *)
@ -1986,14 +1977,12 @@ lemma receive_signal_globals_equiv:
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding receive_signal_def fun_app_def do_nbrecv_failed_transfer_def
apply (rule hoare_pre)
apply (wp set_notification_globals_equiv set_thread_state_globals_equiv
as_user_globals_equiv get_simple_ko_wp
| wpc)+
apply (simp add: valid_arch_state_ko_at_arch)
apply (wpsimp wp: set_notification_globals_equiv set_thread_state_globals_equiv
as_user_globals_equiv get_simple_ko_wp)+
done
lemma handle_double_fault_globals_equiv:
"\<lbrace>globals_equiv s and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
handle_double_fault tptr ex1 ex2
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding handle_double_fault_def
@ -2016,19 +2005,6 @@ lemma send_fault_ipc_valid_global_objs:
apply (wp | simp)+
done
crunch valid_ko_at_arch[wp]: send_ipc "valid_ko_at_arch"
(wp: hoare_drop_imps hoare_vcg_if_lift2 dxo_wp_weak)
lemma send_fault_ipc_valid_ko_at_arch[wp]:
"send_fault_ipc a b \<lbrace>valid_ko_at_arch\<rbrace>"
unfolding send_fault_ipc_def
apply wp
apply (simp add: Let_def)
apply (wp send_ipc_valid_ko_at_arch | wpc)+
apply (rule_tac Q'="\<lambda>_. valid_ko_at_arch" in hoare_post_imp_R)
apply (wp | simp)+
done
context Ipc_IF_1 begin
@ -2049,11 +2025,15 @@ lemma send_fault_ipc_globals_equiv:
valid_global_objs and K (valid_fault fault) and valid_idle and
(\<lambda>s. sym_refs (state_refs_of s))" in hoare_post_imp_R)
apply (wp | simp)+
apply (clarsimp simp: valid_arch_state_ko_at_arch)
apply (clarsimp)
apply (rule valid_tcb_fault_update)
apply (wp | simp)+
done
crunches send_fault_ipc
for valid_arch_state[wp]: valid_arch_state
(wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps)
lemma handle_fault_globals_equiv:
"\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
and pspace_distinct and pspace_aligned and valid_global_objs
@ -2062,13 +2042,13 @@ lemma handle_fault_globals_equiv:
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding handle_fault_def
apply (wp handle_double_fault_globals_equiv)
apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arch" and
E="\<lambda>_. globals_equiv st and valid_ko_at_arch" in hoare_post_impErr)
apply (wp send_fault_ipc_globals_equiv | simp add: valid_arch_state_ko_at_arch)+
apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_arch_state" and
E="\<lambda>_. globals_equiv st and valid_arch_state" in hoare_post_impErr)
apply (wp send_fault_ipc_globals_equiv | simp)+
done
lemma handle_fault_reply_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
handle_fault_reply fault thread x y
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
by (cases fault; wpsimp wp: as_user_globals_equiv handle_arch_fault_reply_globals_equiv)
@ -2084,13 +2064,12 @@ lemma do_reply_transfer_globals_equiv:
apply (wp set_thread_state_globals_equiv cap_delete_one_globals_equiv do_ipc_transfer_globals_equiv
thread_set_globals_equiv handle_fault_reply_globals_equiv dxo_wp_weak
| wpc | simp split del: if_split)+
apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arch and valid_objs and valid_arch_state
apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_arch_state and valid_objs and valid_arch_state
and valid_global_refs and pspace_distinct
and pspace_aligned and valid_global_objs
and (\<lambda>s. receiver \<noteq> idle_thread s) and valid_idle"
in hoare_strengthen_post)
apply (wp gts_wp
| fastforce simp: valid_arch_state_ko_at_arch pred_tcb_at_def obj_at_def valid_idle_def)+
apply (wp gts_wp | fastforce simp: pred_tcb_at_def obj_at_def valid_idle_def)+
done
lemma handle_reply_globals_equiv:
@ -2116,11 +2095,7 @@ lemma reply_from_kernel_globals_equiv:
reply_from_kernel thread x
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding reply_from_kernel_def
apply (wp set_message_info_globals_equiv set_mrs_globals_equiv
as_user_globals_equiv | simp add: split_def)+
apply (insert length_msg_lt_msg_max)
apply (simp add: valid_arch_state_ko_at_arch)
done
by (wpsimp wp: set_message_info_globals_equiv set_mrs_globals_equiv as_user_globals_equiv)
section "reads_respects_g"
@ -2231,7 +2206,7 @@ subsection "Replies"
lemma handle_fault_reply_reads_respects_g:
"reads_respects_g aag l
(valid_ko_at_arch and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread))
(valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread))
(handle_fault_reply fault thread x y)"
apply (rule equiv_valid_guard_imp[OF reads_respects_g])
apply (rule handle_fault_reply_reads_respects)

14
proof/infoflow/Noninterference.thy
View File

@ -424,7 +424,7 @@ lemma ct_running_not_idle:
by (clarsimp simp add: ct_in_state_def pred_tcb_at_def obj_at_def valid_idle_def)
lemma kernel_entry_if_globals_equiv_scheduler:
"\<lbrace>globals_equiv_scheduler st and valid_ko_at_arch and invs
"\<lbrace>globals_equiv_scheduler st and valid_arch_state and invs
and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)
and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace>
kernel_entry_if e tc
@ -467,7 +467,7 @@ lemma kernel_entry_if_partitionIntegrity:
apply (wp kernel_entry_silc_inv[where st'=st'], simp add: schact_is_rct_simple)
apply (fastforce simp: pas_refined_pasMayActivate_update pas_refined_pasMayEditReadyQueues_update
globals_equiv_scheduler_refl silc_dom_equiv_def equiv_for_refl
invs_valid_ko_at_arch domain_fields_equiv_def ct_active_not_idle')
domain_fields_equiv_def ct_active_not_idle')
apply (fastforce simp: partitionIntegrity_def)
done
@ -525,7 +525,7 @@ lemma pas_refined_pasMayActivate_update[simp]:
done
lemma activate_thread_globals_equiv_scheduler:
"\<lbrace>globals_equiv_scheduler st and valid_ko_at_arch and valid_idle\<rbrace>
"\<lbrace>globals_equiv_scheduler st and valid_arch_state and valid_idle\<rbrace>
activate_thread
\<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>"
by (wp globals_equiv_scheduler_inv' activate_thread_globals_equiv | force | fastforce)+
@ -587,7 +587,7 @@ lemma schedule_if_partitionIntegrity:
silc_dom_equiv_from_silc_inv_valid'[where P="\<top>" and st=st]
domain_fields_equiv_lift schedule_cur_domain schedule_domain_fields
| simp add: silc_inv_def partitionIntegrity_def guarded_pas_domain_def
invs_valid_idle invs_valid_ko_at_arch silc_dom_equiv_def)+
invs_valid_idle silc_dom_equiv_def)+
apply (fastforce simp: equiv_for_refl dest: domains_distinct[THEN pas_domains_distinct_inj])
apply (fastforce simp: partitionIntegrity_def globals_equiv_scheduler_def)+
done
@ -1946,7 +1946,7 @@ end
lemma set_thread_state_runnable_reads_respects_g:
assumes domains_distinct: "pas_domains_distinct aag"
shows "reads_respects_g aag (l :: 'a subject_label)
(valid_ko_at_arch and K (runnable ts)) (set_thread_state t ts)"
(valid_arch_state and K (runnable ts)) (set_thread_state t ts)"
apply (rule gen_asm_ev)
apply (rule equiv_valid_guard_imp)
apply (rule reads_respects_g[OF set_thread_state_runnable_reads_respects[OF domains_distinct]])
@ -2032,12 +2032,12 @@ lemma activate_thread_reads_respects_g:
apply (rule conjI)
apply (blast intro: requiv_g_cur_thread_eq)
apply (frule invs_valid_idle)
apply (simp add: invs_valid_ko_at_arch)
apply simp
apply (rule conjI)
apply blast
apply (rule impI)
apply (clarsimp simp: pred_tcb_at_def obj_at_def valid_idle_def)
apply (fastforce simp: invs_valid_ko_at_arch det_getRestartPC)
apply (fastforce simp: det_getRestartPC)
done
lemma cur_thread_update_reads_respects_g':

4
proof/infoflow/Scheduler_IF.thy
View File

@ -2341,10 +2341,10 @@ lemma activate_thread_reads_respects_scheduler[wp]:
[where P'="\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and>
guarded_pas_domain aag s \<and> invs s"])
apply ((wp scheduler_equiv_lift'[where P="invs and silc_inv aag st"]
globals_equiv_scheduler_inv'[where P="valid_ko_at_arch and valid_idle"]
globals_equiv_scheduler_inv'[where P="valid_arch_state and valid_idle"]
set_thread_state_globals_equiv gts_wp
| wpc
| clarsimp simp: restart_not_idle invs_valid_ko_at_arch silc_inv_not_cur_thread
| clarsimp simp: restart_not_idle silc_inv_not_cur_thread
| force)+)[1]
apply (wp gts_wp| wpc | simp)+
apply (clarsimp simp: guarded_pas_domain_def restart_not_idle invs_valid_idle)

25
proof/infoflow/Syscall_IF.thy
View File

@ -39,7 +39,7 @@ locale Syscall_IF_1 =
machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) =
globals_equiv st s"
and thread_set_globals_equiv':
"\<And>f. \<lbrace>globals_equiv s and valid_ko_at_arch and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
"\<And>f. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>s. tptr \<noteq> idle_thread s)\<rbrace>
thread_set f tptr
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
and sts_authorised_for_globals_inv:
@ -65,7 +65,7 @@ locale Syscall_IF_1 =
and handle_hypervisor_fault_reads_respects:
"reads_respects aag l \<top> (handle_hypervisor_fault thread hypfault_type)"
and handle_vm_fault_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
handle_vm_fault thread vmfault_type
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
and handle_hypervisor_fault_globals_equiv:
@ -103,7 +103,7 @@ lemma invoke_cnode_globals_equiv:
cap_delete_globals_equiv cap_swap_globals_equiv hoare_vcg_all_lift
cancel_badged_sends_globals_equiv
| wpc | wp (once) hoare_drop_imps | simp add: invs_valid_global_objs)+
apply (case_tac cinv; clarsimp simp: invs_valid_ko_at_arch real_cte_emptyable_strg)
apply (case_tac cinv; clarsimp simp: real_cte_emptyable_strg)
done
end
@ -386,8 +386,7 @@ next
apply (rule equiv_valid_guard_imp)
apply (wpc | simp | wp reads_respects_f_g'[OF invoke_irq_control_reads_respects_g]
invoke_irq_control_silc_inv)+
by (simp add: invs_def valid_state_def
authorised_invocation_def valid_arch_state_ko_at_arch)
by (simp add: invs_def valid_state_def authorised_invocation_def)
next
case InvokeIRQHandler
then show ?thesis
@ -408,7 +407,7 @@ qed
end
crunch valid_ko_at_arch[wp]: reply_from_kernel "valid_ko_at_arch" (simp: crunch_simps)
crunch valid_arch_state[wp]: reply_from_kernel valid_arch_state (simp: crunch_simps)
lemma syscall_reads_respects_f_g:
assumes reads_res_m_fault:
@ -486,7 +485,7 @@ lemma authorised_for_globals_triv:
lemma set_thread_state_reads_respects_g:
assumes domains_distinct: "pas_domains_distinct aag"
shows
"reads_respects_g aag (l :: 'a subject_label) (is_subject aag \<circ> cur_thread and valid_ko_at_arch)
"reads_respects_g aag (l :: 'a subject_label) (is_subject aag \<circ> cur_thread and valid_arch_state)
(set_thread_state ref ts)"
apply (rule equiv_valid_guard_imp)
apply (rule reads_respects_g)
@ -592,7 +591,7 @@ lemma handle_invocation_reads_respects_g:
is_subject aag (cur_thread s) \<and> rv \<noteq> idle_thread s"
in hoare_post_imp_R)
apply (wp pinv_invs perform_invocation_silc_inv)
apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_state_ko_at_arch)
apply (simp add: invs_def valid_state_def valid_pspace_def)
apply (wpsimp wp: reads_respects_f_g'
set_thread_state_reads_respects_g[OF domains_distinct])
apply (wp when_ev set_thread_state_only_timer_irq_inv[where st=st']
@ -617,7 +616,7 @@ lemma handle_invocation_reads_respects_g:
apply (rule conjI)
apply (clarsimp simp: requiv_g_cur_thread_eq simp: reads_equiv_f_g_conj)
apply (clarsimp simp: det_getRegister invs_sym_refs invs_def valid_state_def
valid_arch_state_ko_at_arch valid_pspace_vo valid_pspace_distinct)
valid_pspace_vo valid_pspace_distinct)
apply (rule context_conjI)
apply (simp add: ct_active_cur_thread_not_idle_thread)
apply (clarsimp simp: valid_pspace_def ct_in_state_def)
@ -646,7 +645,7 @@ lemma delete_caller_cap_reads_respects_f:
by (rule cap_delete_one_reads_respects_f[OF domains_distinct])
lemma delete_caller_cap_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
delete_caller_cap x
\<lbrace>\<lambda>r. globals_equiv st\<rbrace>"
unfolding delete_caller_cap_def
@ -822,7 +821,7 @@ lemma equiv_valid_hoist_guard:
lemma as_user_reads_respects_g:
"reads_respects_g aag k
(valid_ko_at_arch and (\<lambda>s. thread \<noteq> idle_thread s) and K (det f \<and> is_subject aag thread))
(valid_arch_state and (\<lambda>s. thread \<noteq> idle_thread s) and K (det f \<and> is_subject aag thread))
(as_user thread f)"
apply (rule equiv_valid_guard_imp)
apply (rule reads_respects_g)
@ -858,7 +857,7 @@ lemma handle_interrupt_globals_equiv:
done
lemma handle_vm_fault_reads_respects_g:
"reads_respects_g aag l (K (is_subject aag t) and (valid_ko_at_arch and (\<lambda>s. t \<noteq> idle_thread s)))
"reads_respects_g aag l (K (is_subject aag t) and (valid_arch_state and (\<lambda>s. t \<noteq> idle_thread s)))
(handle_vm_fault t vmfault_type)"
apply (rule reads_respects_g)
apply (rule handle_vm_fault_reads_respects)
@ -949,7 +948,7 @@ lemma activate_thread_reads_respects:
| clarsimp simp: st_tcb_at_def obj_at_def is_tcb_def)+
lemma activate_thread_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch and valid_idle\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state and valid_idle\<rbrace>
activate_thread
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding activate_thread_def

48
proof/infoflow/Tcb_IF.thy
View File

@ -18,7 +18,7 @@ crunches cancel_ipc, restart, deleting_irq_handler, suspend, cap_swap_for_delete
section "globals equiv"
lemma setup_reply_master_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
setup_reply_master t
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding setup_reply_master_def
@ -27,7 +27,7 @@ lemma setup_reply_master_globals_equiv:
done
lemma restart_globals_equiv[wp]:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
restart t
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding restart_def
@ -38,15 +38,12 @@ lemma globals_equiv_ioc_update[simp]:
by (simp add: globals_equiv_def idle_equiv_def)
lemma cap_swap_for_delete_globals_equiv[wp]:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
cap_swap_for_delete a b
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding cap_swap_for_delete_def cap_swap_def set_original_def
by (wp modify_wp set_cdt_globals_equiv set_cap_globals_equiv'' dxo_wp_weak | simp)+
crunch valid_ko_at_arch[wp]: cap_swap_for_delete, restart "valid_ko_at_arch"
(wp: dxo_wp_weak simp_del: cap_swap_ext_extended.dxo_eq possible_switch_to_extended.dxo_eq)
lemma rec_del_preservation2':
assumes finalise_cap_P: "\<And>cap final. \<lbrace>R cap and P\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. P\<rbrace>"
assumes set_cap_P: "\<And>cap b. \<lbrace>Q and P\<rbrace> set_cap cap b \<lbrace>\<lambda>_. P\<rbrace>"
@ -133,7 +130,7 @@ next
show ?case
apply (simp add: spec_validE_def)
apply (rule hoare_pre, wp cap_swap_for_delete_P cap_swap_for_delete_Q)
apply (clarsimp simp: invs_valid_ko_at_arch)
apply (clarsimp)
done
next
case (4 ptr bits n slot s)
@ -182,9 +179,7 @@ lemma rec_del_preservation2:
locale Tcb_IF_1 =
fixes aag :: "'a subject_label PAS"
assumes valid_ko_at_arch_irq_state_independent_A[simp, intro!]:
"irq_state_independent_A valid_ko_at_arch"
and valid_arch_caps_vs_lookup:
assumes valid_arch_caps_vs_lookup:
"valid_arch_caps s \<Longrightarrow> valid_vs_lookup s"
and no_cap_to_idle_thread':
"valid_global_refs s \<Longrightarrow> \<not> ex_nonz_cap_to (idle_thread s) s"
@ -192,20 +187,24 @@ locale Tcb_IF_1 =
"valid_global_refs s \<Longrightarrow> caps_of_state s ref \<noteq> Some (ThreadCap (idle_thread s))"
and arch_post_modify_registers_globals_equiv[wp]:
"arch_post_modify_registers cur t \<lbrace>globals_equiv s\<rbrace>"
and arch_post_modify_registers_valid_ko_at_arch[wp]:
"arch_post_modify_registers cur t \<lbrace>valid_ko_at_arch\<rbrace>"
and arch_post_modify_registers_valid_arch_state[wp]:
"arch_post_modify_registers cur t \<lbrace>\<lambda>s :: det_state. valid_arch_state s\<rbrace>"
and arch_post_modify_registers_reads_respects_f[wp]:
"reads_respects_f aag l \<top> (arch_post_modify_registers cur t)"
and arch_get_sanitise_register_info_reads_respects_f[wp]:
"reads_respects_f aag l \<top> (arch_get_sanitise_register_info t)"
begin
crunches cap_swap_for_delete
for valid_arch_state[wp]: valid_arch_state
(wp: dxo_wp_weak)
lemma rec_del_globals_equiv:
"\<lbrace>\<lambda>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace>
rec_del call
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (wp finalise_cap_globals_equiv
rec_del_preservation2[where Q="valid_ko_at_arch"
rec_del_preservation2[where Q="valid_arch_state"
and R="\<lambda>cap s. valid_global_objs s \<and> valid_arch_state s
\<and> pspace_aligned s \<and> valid_vspace_objs s
\<and> valid_global_refs s \<and> valid_vs_lookup s
@ -213,11 +212,11 @@ lemma rec_del_globals_equiv:
apply simp
apply (wp set_cap_globals_equiv'')
apply simp
apply (wp set_cap_valid_ko_at_arch empty_slot_globals_equiv)+
apply (wp empty_slot_globals_equiv)+
apply simp
apply (wp empty_slot_valid_ko_at_arch)+
apply (wp)+
apply simp
apply (simp add: invs_valid_ko_at_arch)
apply fastforce
apply (clarsimp simp: invs_def valid_state_def valid_arch_caps_vs_lookup
valid_pspace_def no_cap_to_idle_thread'')
apply (wp preemption_point_inv | simp)+
@ -248,19 +247,14 @@ crunch idle_thread'[wp]: restart "\<lambda>s. P (idle_thread s)"
(wp: dxo_wp_weak)
lemma bind_notification_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
bind_notification t ntfnptr
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding bind_notification_def
by (wp set_bound_notification_globals_equiv set_notification_globals_equiv | wpc | simp)+
lemma bind_notification_valid_ko_at_arch[wp]:
"bind_notification t ntfnptr \<lbrace>valid_ko_at_arch\<rbrace>"
unfolding bind_notification_def
by (wp set_bound_notification_valid_ko_at_arch | wpc | simp)+
lemma invoke_tcb_NotificationControl_globals_equiv:
"\<lbrace>globals_equiv st and valid_ko_at_arch\<rbrace>
"\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
invoke_tcb (NotificationControl t ntfn)
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (case_tac ntfn, simp_all)
@ -307,22 +301,22 @@ lemma invoke_tcb_globals_equiv:
supply reschedule_required_ext_extended.dxo_eq[simp del]
apply (case_tac ti; (solves \<open>(wp mapM_x_wp' as_user_globals_equiv
invoke_tcb_NotificationControl_globals_equiv
| simp add: invs_valid_ko_at_arch
| simp
| intro conjI impI
| clarsimp simp: no_cap_to_idle_thread)+\<close>)?)
apply wpsimp
apply (rename_tac word1 word2 bool1 bool2 bool3 bool4 arm_copy_register_sets)
apply (rule_tac Q="\<lambda>_. valid_ko_at_arch and globals_equiv st and
apply (rule_tac Q="\<lambda>_. valid_arch_state and globals_equiv st and
(\<lambda>s. word1 \<noteq> idle_thread s) and (\<lambda>s. word2 \<noteq> idle_thread s)"
in hoare_strengthen_post)
apply ((wp mapM_x_wp' as_user_globals_equiv invoke_tcb_NotificationControl_globals_equiv
| simp add: invs_valid_ko_at_arch
| simp
| intro conjI impI
| clarsimp simp: no_cap_to_idle_thread)+)[6]
apply (simp del: invoke_tcb.simps tcb_inv_wf.simps)
apply (wp invoke_tcb_thread_preservation cap_delete_globals_equiv
cap_insert_globals_equiv'' thread_set_globals_equiv set_mcpriority_globals_equiv
| clarsimp simp: invs_valid_ko_at_arch split del: if_split)+
| fastforce)+
done
end