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

access-control: update for new definition of set_object

This commit is contained in:
Victor Phan 2019-04-04 15:50:05 +11:00
parent 93888ccb07
commit bed48eba13
8 changed files with 127 additions and 164 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
proof/access-control/Access.thy
View File

@ -2354,8 +2354,7 @@ lemma set_object_integrity_autarch:
"\<lbrace>integrity aag X st and K (is_subject aag ptr)\<rbrace>
set_object ptr obj
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: set_object_def)
apply (wp gets_the_wp)
apply (wpsimp wp: set_object_wp)
apply (rule integrity_update_autarch, simp_all)
done
@ -2646,8 +2645,8 @@ done
lemma as_user_state_vrefs[wp]:
"\<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> as_user t f \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>"
apply (simp add: as_user_def set_object_def split_def)
apply wp
apply (simp add: as_user_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: state_vrefs_def vs_refs_no_global_pts_def get_tcb_def
elim!: rsubst[where P=P, OF _ ext]
split: option.split_asm Structures_A.kernel_object.split)
@ -2655,9 +2654,9 @@ lemma as_user_state_vrefs[wp]:
lemma as_user_tcb_states[wp]:
"\<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> as_user t f \<lbrace>\<lambda>rv s. P (tcb_states_of_state s)\<rbrace>"
apply (simp add: as_user_def set_object_def split_def tcb_states_of_state_def)
apply wp
apply (clarsimp simp: thread_states_def get_tcb_def
apply (simp add: as_user_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: thread_states_def get_tcb_def tcb_states_of_state_def
elim!: rsubst[where P=P, OF _ ext] split: option.split)
done

14
proof/access-control/Arch_AC.thy
View File

@ -533,7 +533,7 @@ crunch thread_states[wp]: do_machine_op "\<lambda>s. P (thread_states s)"
(* FIXME: move *)
lemma set_mrs_state_vrefs[wp]:
"\<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>"
apply (simp add: set_mrs_def split_def set_object_def)
apply (simp add: set_mrs_def split_def set_object_def get_object_def)
apply (wp gets_the_wp get_wp put_wp mapM_x_wp'
| wpc
| simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def)+
@ -545,7 +545,7 @@ lemma set_mrs_state_vrefs[wp]:
(* FIXME: move *)
lemma set_mrs_thread_states[wp]:
"\<lbrace>\<lambda>s. P (thread_states s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. P (thread_states s)\<rbrace>"
apply (simp add: set_mrs_def split_def set_object_def)
apply (simp add: set_mrs_def split_def set_object_def get_object_def)
apply (wp gets_the_wp get_wp put_wp mapM_x_wp'
| wpc
| simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def)+
@ -554,7 +554,7 @@ lemma set_mrs_thread_states[wp]:
lemma set_mrs_thread_bound_ntfns[wp]:
"\<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. P (thread_bound_ntfns s)\<rbrace>"
apply (simp add: set_mrs_def split_def set_object_def)
apply (simp add: set_mrs_def split_def set_object_def get_object_def)
apply (wp gets_the_wp get_wp put_wp mapM_x_wp' dmo_wp
| wpc
| simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def no_irq_storeWord)+
@ -1315,10 +1315,10 @@ lemma set_asid_pool_respects_clear:
\<longrightarrow> asid_pool_integrity {pasSubject aag} aag pool' pool)
and integrity aag X st\<rbrace>
set_asid_pool ptr pool \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: obj_at_def
split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm)
apply (simp add: set_asid_pool_def)
apply (wpsimp wp: set_object_wp_strong
simp: obj_at_def a_type_def
split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm if_splits)
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def)
apply (rule tro_asidpool_clear; simp add: asid_pool_integrity_def)

101
proof/access-control/CNode_AC.thy
View File

@ -331,9 +331,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
@ -343,12 +341,7 @@ lemma set_object_caps_of_state:
lemma set_object_domains_of_state[wp]:
"\<lbrace> \<lambda>s. P (domains_of_state s) \<rbrace> set_object a b \<lbrace> \<lambda>_ s. P (domains_of_state s) \<rbrace>"
unfolding set_object_def
apply wp
apply (rule rsubst[where P=P])
apply assumption
apply (clarsimp simp: get_etcb_def)
done
by (wpsimp wp: set_object_wp)
lemma set_cap_pas_refined:
"\<lbrace>pas_refined aag and (\<lambda>s. (is_transferable_in ptr s \<and> (\<not> Option.is_none (cdt s ptr)))
@ -809,31 +802,33 @@ method monad_commute_default =
| solves \<open>(changed \<open>wp | fastforce\<close>)+\<close>
| fastforce\<close>
(* Now the commute steps *)
(* FIXME: remove and generalise version in ainvs *)
lemma set_original_set_cap_comm:
"(do set_original slot' val; set_cap cap slot od) =
(do set_cap cap slot; set_original slot' val od)"
apply (clarsimp simp: set_original_def set_cap_def get_object_def set_object_def
simp del: K_bind_def
split: prod.splits)
apply (simp only: gets_modify_def modify_def[symmetric])
apply (rule monad_commuteI2)
apply monad_commute_default
apply (monad_eq; fastforce)
apply (rule ext)
apply (clarsimp simp: bind_def split_def set_cap_def set_original_def
get_object_def set_object_def get_def put_def
simpler_gets_def simpler_modify_def
assert_def fail_def)
apply (case_tac y; simp add: return_def fail_def)
done
lemma set_cdt_set_cap_comm:
"(do set_cdt c; set_cap cap slot od) =
(do set_cap cap slot; set_cdt c od)"
apply (clarsimp simp: set_cdt_def set_cap_def get_object_def set_object_def
simp del: K_bind_def
split: prod.splits)
apply (simp only: modify_def[symmetric] gets_modify_def)
apply (rule monad_commuteI2)
apply monad_commute_default
apply (monad_eq; fastforce)
apply (rule ext)
apply (clarsimp simp: bind_def split_def set_cap_def set_cdt_def
get_object_def set_object_def get_def put_def
simpler_gets_def simpler_modify_def
assert_def fail_def)
apply (case_tac y; simp add: return_def fail_def)
done
lemma set_cdt_set_original_comm:
"(do set_cdt c; set_original slot val od) =
(do set_original slot val; set_cdt c od)"
@ -862,14 +857,13 @@ lemma set_cdt_empty_slot_ext_comm:
lemma set_cap_empty_slot_ext_comm:
"(do set_cap cap slot; empty_slot_ext slot' slot_p od) =
(do empty_slot_ext slot' slot_p; set_cap cap slot od :: (det_ext state \<Rightarrow> _))"
apply (clarsimp simp: set_cap_def get_object_def set_object_def
empty_slot_ext_def update_cdt_list_def set_cdt_list_def
simp del: K_bind_def
split: prod.splits)
apply (simp only: modify_def[symmetric] gets_modify_def)
apply (rule monad_commuteI2)
apply monad_commute_default
apply (monad_eq split: option.splits; fastforce)
apply (rule ext)
apply (clarsimp simp: bind_def split_def set_cap_def empty_slot_ext_def
update_cdt_list_def set_cdt_list_def
get_object_def set_object_def get_def put_def
simpler_gets_def simpler_modify_def
assert_def fail_def)
apply (case_tac y; simp add: return_def fail_def split: option.splits)
done
(* FIXME: MOVE *)
@ -1247,9 +1241,8 @@ lemma sts_respects_restart_ep:
and (\<lambda>s. \<exists>ep. aag_has_auth_to aag Reset ep \<and> st_tcb_at (blocked_on ep) thread s)\<rbrace>
set_thread_state thread Structures_A.Restart
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply wp
apply clarsimp
apply (simp add: set_thread_state_def)
apply (wpsimp wp: set_object_wp)
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def get_tcb_def)
apply (rule_tac tro_tcb_restart [OF refl refl])
@ -1277,8 +1270,8 @@ lemma mapM_mapM_x_valid:
lemma sts_st_vrefs[wp]:
"\<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (wp dxo_wp_weak |simp)+
apply (simp add: set_thread_state_def)
apply (wpsimp wp: set_object_wp dxo_wp_weak)
apply (clarsimp simp: state_vrefs_def vs_refs_no_global_pts_def
elim!: rsubst[where P=P, OF _ ext]
dest!: get_tcb_SomeD)
@ -1286,8 +1279,8 @@ lemma sts_st_vrefs[wp]:
lemma sts_thread_bound_ntfns[wp]:
"\<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. P (thread_bound_ntfns s)\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (wp dxo_wp_weak |simp)+
apply (simp add: set_thread_state_def)
apply (wpsimp wp: set_object_wp dxo_wp_weak)
apply (clarsimp simp: thread_bound_ntfns_def get_tcb_def
split: if_split option.splits kernel_object.splits
elim!: rsubst[where P=P, OF _ ext])
@ -1295,8 +1288,8 @@ lemma sts_thread_bound_ntfns[wp]:
lemma sts_thread_states[wp]:
"\<lbrace>\<lambda>s. P ((thread_states s)(t := tcb_st_to_auth st))\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. P (thread_states s)\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (wp dxo_wp_weak |simp)+
apply (simp add: set_thread_state_def)
apply (wpsimp wp: set_object_wp dxo_wp_weak)
apply (clarsimp simp: get_tcb_def thread_states_def tcb_states_of_state_def
elim!: rsubst[where P=P, OF _ ext])
done
@ -1305,8 +1298,8 @@ lemma sbn_thread_bound_ntfns[wp]:
"\<lbrace>\<lambda>s. P ((thread_bound_ntfns s)(t := ntfn))\<rbrace>
set_bound_notification t ntfn
\<lbrace>\<lambda>rv s. P (thread_bound_ntfns s)\<rbrace>"
apply (simp add: set_bound_notification_def set_object_def)
apply (wp dxo_wp_weak |simp)+
apply (simp add: set_bound_notification_def)
apply (wpsimp wp: set_object_wp dxo_wp_weak)
apply (clarsimp simp: get_tcb_def thread_bound_ntfns_def
elim!: rsubst[where P=P, OF _ ext])
done
@ -1393,8 +1386,8 @@ lemma set_simple_ko_pas_refined[wp]:
lemma thread_set_st_vrefs[wp]:
"\<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>"
apply (simp add: thread_set_def set_object_def)
apply (wp | simp)+
apply (simp add: thread_set_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: state_vrefs_def vs_refs_no_global_pts_def
elim!: rsubst[where P=P, OF _ ext] dest!: get_tcb_SomeD)
done
@ -1402,9 +1395,9 @@ lemma thread_set_st_vrefs[wp]:
lemma thread_set_thread_states_trivT:
assumes st: "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
shows "\<lbrace>\<lambda>s. P (thread_states s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (thread_states s)\<rbrace>"
apply (simp add: thread_set_def set_object_def)
apply (wp | simp)+
apply (clarsimp simp: st get_tcb_def thread_states_def tcb_states_of_state_def split: option.split
apply (simp add: thread_set_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: st get_tcb_def thread_states_def tcb_states_of_state_def
elim!: rsubst[where P=P, OF _ ext]
split: Structures_A.kernel_object.split_asm)
done
@ -1412,9 +1405,9 @@ lemma thread_set_thread_states_trivT:
lemma thread_set_thread_bound_ntfns_trivT:
assumes ntfn: "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
shows "\<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (thread_bound_ntfns s)\<rbrace>"
apply (simp add: thread_set_def set_object_def)
apply (wp | simp)+
apply (clarsimp simp: ntfn get_tcb_def thread_bound_ntfns_def tcb_states_of_state_def split: option.split
apply (simp add: thread_set_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: ntfn get_tcb_def thread_bound_ntfns_def tcb_states_of_state_def
elim!: rsubst[where P=P, OF _ ext]
split: Structures_A.kernel_object.split_asm)
done
@ -1612,8 +1605,8 @@ lemma set_asid_pool_st_vrefs[wp]:
lemma set_asid_pool_thread_states[wp]:
"\<lbrace>\<lambda>s. P (thread_states s)\<rbrace> set_asid_pool p pool \<lbrace>\<lambda>rv s. P (thread_states s)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (simp add: set_asid_pool_def)
apply (wpsimp wp: set_object_wp_strong)
apply (clarsimp simp: thread_states_def obj_at_def get_tcb_def tcb_states_of_state_def
elim!: rsubst[where P=P, OF _ ext]
split: Structures_A.kernel_object.split_asm option.split)
@ -1621,8 +1614,8 @@ lemma set_asid_pool_thread_states[wp]:
lemma set_asid_pool_thread_bound_ntfns[wp]:
"\<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_asid_pool p pool \<lbrace>\<lambda>rv s. P (thread_bound_ntfns s)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def)
apply (wp get_object_wp)
apply (simp add: set_asid_pool_def)
apply (wpsimp wp: set_object_wp_strong)
apply (clarsimp simp: thread_bound_ntfns_def obj_at_def get_tcb_def tcb_states_of_state_def
elim!: rsubst[where P=P, OF _ ext]
split: Structures_A.kernel_object.split_asm option.split)

13
proof/access-control/DomainSepInv.thy
View File

@ -112,9 +112,7 @@ lemma set_object_wp:
"\<lbrace> \<lambda> s. P (s\<lparr>kheap := kheap s(ptr \<mapsto> obj)\<rparr>) \<rbrace>
set_object ptr obj
\<lbrace> \<lambda>_. P \<rbrace>"
unfolding set_object_def
apply (wp)
done
by (wpsimp wp: set_object_wp)
(* FIXME: following 3 lemmas clagged from FinalCaps *)
lemma set_cap_neg_cte_wp_at_other_helper':
@ -328,7 +326,7 @@ lemma empty_slot_domain_sep_inv:
lemma set_simple_ko_neg_cte_wp_at[wp]:
"\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> set_simple_ko f a b \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>"
apply(simp add: set_simple_ko_def)
apply(wp set_object_wp get_object_wp
apply(wp set_object_wp_strong get_object_wp
| simp add: partial_inv_def a_type_def split: kernel_object.splits)+
apply(case_tac "a = fst slot")
apply(clarsimp split: kernel_object.splits)
@ -654,9 +652,10 @@ lemma invoke_cnode_domain_sep_inv:
unfolding invoke_cnode_def
apply(case_tac ci)
apply(wp cap_insert_domain_sep_inv cap_move_domain_sep_inv | simp split del: if_split)+
apply(rule hoare_pre)
(* this tactic takes 2 min *)
apply(wp cap_move_domain_sep_inv cap_move_cte_wp_at_other get_cap_wp | simp | blast dest: cte_wp_at_weak_derived_domain_sep_inv_cap | wpc)+
apply(rule hoare_pre)
apply (wpsimp wp: cap_move_domain_sep_inv cap_move_cte_wp_at_other get_cap_wp,
blast dest: cte_wp_at_weak_derived_domain_sep_inv_cap)+
apply (wpsimp wp: cap_move_domain_sep_inv get_cap_wp)
apply(fastforce dest: cte_wp_at_weak_derived_ReplyCap)
apply(wp | simp | wpc | rule hoare_pre)+
done

21
proof/access-control/Finalise_AC.thy
View File

@ -195,16 +195,16 @@ lemma set_bound_notification_ekheap[wp]:
lemma sbn_thread_states[wp]:
"\<lbrace>\<lambda>s. P (thread_states s)\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv s. P (thread_states s)\<rbrace>"
apply (simp add: set_bound_notification_def set_object_def)
apply (wp dxo_wp_weak |simp)+
apply (simp add: set_bound_notification_def)
apply (wpsimp wp: set_object_wp dxo_wp_weak)
apply (clarsimp simp: get_tcb_def thread_states_def tcb_states_of_state_def
elim!: rsubst[where P=P, OF _ ext])
done
lemma sbn_st_vrefs[wp]:
"\<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> set_bound_notification t st \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>"
apply (simp add: set_bound_notification_def set_object_def)
apply (wp dxo_wp_weak |simp)+
apply (simp add: set_bound_notification_def)
apply (wpsimp wp: set_object_wp dxo_wp_weak)
apply (clarsimp simp: state_vrefs_def vs_refs_no_global_pts_def
elim!: rsubst[where P=P, OF _ ext]
dest!: get_tcb_SomeD)
@ -354,9 +354,8 @@ lemma sbn_unbind_respects[wp]:
(pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag))\<rbrace>
set_bound_notification t None
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_bound_notification_def set_object_def)
apply wp
apply clarsimp
apply (simp add: set_bound_notification_def)
apply (wpsimp wp: set_object_wp)
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def obj_at_def pred_tcb_at_def)
apply (rule tro_tcb_unbind)
@ -482,8 +481,8 @@ lemma cap_delete_one_respects_transferable[wp_transferable]:
lemma thread_set_tcb_state_trivial:
"(\<And> tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow>
\<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (tcb_states_of_state 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 elim!: rsubst[where P=P] dest!: get_tcb_SomeD)
by (auto simp: tcb_states_of_state_def get_tcb_def)
@ -975,8 +974,8 @@ lemma thread_set_pas_refined_triv_idleT:
apply (simp add: pas_refined_def state_objs_to_policy_def)
apply (rule hoare_pre)
apply (wps thread_set_caps_of_state_trivial[OF cps])
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 simp: pred_tcb_def2 fun_upd_def[symmetric]
del: subsetI)
apply (erule_tac P="\<lambda> ts ba. auth_graph_map a (state_bits_to_policy cps ts ba cd vr) \<subseteq> ag"

53
proof/access-control/Ipc_AC.thy
View File

@ -339,7 +339,7 @@ lemma set_mrs_respects_in_signalling':
set_mrs thread buf msgs
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: set_mrs_def split_def set_object_def)
apply (simp add: set_mrs_def split_def set_object_def get_object_def)
apply (wp gets_the_wp get_wp put_wp
| wpc
| simp split del: if_split
@ -368,14 +368,14 @@ lemma as_user_set_register_respects:
K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st) \<and> (aag_has_auth_to aag SyncSend ep \<or> aag_has_auth_to aag Notify ep)) \<rbrace>
as_user thread (set_register r v)
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: as_user_def split_def set_object_def)
apply (simp add: as_user_def split_def set_object_def get_object_def)
apply wp
apply (clarsimp simp: in_monad setRegister_def)
apply (cases "is_subject aag thread")
apply (erule (1) integrity_update_autarch [unfolded fun_upd_def])
apply (clarsimp simp: st_tcb_def2)
apply (rule send_upd_ctxintegrity [OF disjI1, unfolded fun_upd_def])
apply (auto simp: direct_send_def st_tcb_def2)
apply (auto simp: direct_send_def st_tcb_def2)
done
lemma lookup_ipc_buffer_ptr_range:
@ -404,7 +404,7 @@ lemma set_thread_state_respects_in_signalling:
and K (aag_has_auth_to aag Notify ntfnptr)\<rbrace>
set_thread_state thread Structures_A.thread_state.Running
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (simp add: set_thread_state_def set_object_def get_object_def)
apply wp
apply (clarsimp)
apply (cases "is_subject aag thread")
@ -479,8 +479,8 @@ crunch integrity_once_ts_upd: set_thread_state_ext "integrity_once_ts_upd t ts a
lemma set_thread_state_integrity_once_ts_upd:
"\<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace>
set_thread_state t ts' \<lbrace>\<lambda>_. integrity_once_ts_upd t ts aag X st\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (wp set_thread_state_ext_integrity_once_ts_upd)
apply (simp add: set_thread_state_def)
apply (wpsimp wp: set_object_wp set_thread_state_ext_integrity_once_ts_upd)
apply (clarsimp simp: fun_upd_def dest!: get_tcb_SomeD)
apply (simp add: get_tcb_def cong: if_cong)
done
@ -534,11 +534,8 @@ lemma cancel_ipc_receive_blocked_respects:
lemma set_thread_state_integrity':
"\<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> set_thread_state t ts \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (wp)
apply (clarsimp dest!: get_tcb_SomeD cong: if_cong)
using empty_def insertI1 mk_disjoint_insert
by fastforce
apply (simp add: set_thread_state_def)
by (wpsimp wp: set_object_wp)
lemma as_user_set_register_respects_indirect:
"\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and
@ -547,7 +544,7 @@ lemma as_user_set_register_respects_indirect:
\<and> (aag_has_auth_to aag Notify ntfnptr)) \<rbrace>
as_user thread (set_register r v)
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: as_user_def split_def set_object_def)
apply (simp add: as_user_def split_def set_object_def get_object_def)
apply wp
apply (clarsimp simp: in_monad setRegister_def)
apply (cases "is_subject aag thread")
@ -1640,9 +1637,8 @@ lemma set_thread_state_running_respects:
\<and> st_tcb_at (send_blocked_on ep) sender s)\<rbrace>
set_thread_state sender Structures_A.Running
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply wp
apply clarsimp
apply (simp add: set_thread_state_def)
apply (wpsimp wp: set_object_wp)
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def)
apply (clarsimp dest!: get_tcb_SomeD)
@ -1667,7 +1663,7 @@ lemma sts_receive_Inactive_respects:
and K (aag_has_auth_to aag Receive ep)\<rbrace>
set_thread_state thread Structures_A.thread_state.Inactive
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (simp add: set_thread_state_def set_object_def get_object_def)
apply wp
apply clarsimp
apply (erule integrity_trans)
@ -1719,7 +1715,7 @@ lemma set_thread_state_blocked_on_reply_respects:
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (rule hoare_pre)
apply (simp add: set_thread_state_def set_object_def)
apply (simp add: set_thread_state_def set_object_def get_object_def)
apply wp
apply clarsimp
apply (erule integrity_trans)
@ -2015,7 +2011,7 @@ lemma as_user_respects_in_ipc:
"\<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>
as_user thread m
\<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>"
apply (simp add: as_user_def set_object_def)
apply (simp add: as_user_def set_object_def get_object_def)
apply (wp gets_the_wp get_wp put_wp mapM_x_wp'
| wpc
| simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def)+
@ -2074,8 +2070,9 @@ lemma set_object_respects_in_ipc_autarch:
and K (is_subject aag ptr)\<rbrace>
set_object ptr obj
\<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
apply (simp add: integrity_tcb_in_ipc_def set_object_def)
apply (rule hoare_pre, wp )
apply (simp add: integrity_tcb_in_ipc_def)
apply (rule hoare_pre, wp)
apply (wpsimp wp: set_object_wp)
apply (simp only: pred_conj_def)
apply (elim conjE)
apply (intro conjI ; (solves \<open>simp\<close>)?)
@ -2274,7 +2271,7 @@ lemma set_mrs_respects_in_ipc:
set_mrs receiver recv_buf msgs
\<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: set_mrs_def set_object_def)
apply (simp add: set_mrs_def set_object_def get_object_def)
apply (wp mapM_x_wp' store_word_offs_respects_in_ipc
| wpc
| simp split del: if_split add: zipWithM_x_mapM_x split_def)+
@ -2373,9 +2370,10 @@ lemma set_thread_state_running_respects_in_ipc:
"\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and st_tcb_at(receive_blocked_on epptr) receiver and K(aag_has_auth_to aag SyncSend epptr)\<rbrace>
set_thread_state receiver Structures_A.thread_state.Running
\<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (wp sts_ext_running_noop)
apply (simp add: set_thread_state_def)
apply (wpsimp wp: set_object_wp sts_ext_running_noop)
apply (auto simp: st_tcb_at_def obj_at_def get_tcb_def
get_tcb_rev update_tcb_state_in_ipc
cong: if_cong
elim: update_tcb_state_in_ipc[unfolded fun_upd_def])
done
@ -2887,7 +2885,7 @@ lemma set_thread_state_running_respects_in_ipc_reply:
and K (aag_has_auth_to aag Reply receiver)\<rbrace>
set_thread_state receiver Structures_A.thread_state.Running
\<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>"
apply (simp add: set_thread_state_def set_object_def)
apply (simp add: set_thread_state_def set_object_def get_object_def)
apply (wp sts_ext_running_noop)
apply (auto simp: st_tcb_at_def obj_at_def get_tcb_def
cong: if_cong
@ -3069,11 +3067,8 @@ lemma as_user_respects_in_fault_reply:
"\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>
as_user thread m
\<lbrace>\<lambda>rv. integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>"
apply (simp add: as_user_def set_object_def)
apply (wp gets_the_wp get_wp put_wp mapM_x_wp'
| wpc
| simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def)+
apply (clarsimp simp: st_tcb_def2 tcb_at_def fun_upd_def[symmetric])
apply (simp add: as_user_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: integrity_tcb_in_fault_reply_def)
apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD)
apply (rule tifr_context[OF refl refl])

71
proof/access-control/Syscall_AC.thy
View File

@ -238,10 +238,8 @@ lemma sts_first_restart:
set_thread_state thread Structures_A.thread_state.Restart
\<lbrace>\<lambda>rv s. \<forall>p ko. kheap s p = Some ko \<longrightarrow>
(is_tcb ko \<longrightarrow> p \<noteq> cur_thread st) \<longrightarrow> kheap st p = Some ko\<rbrace>"
unfolding set_thread_state_def set_object_def
apply (wp dxo_wp_weak |simp)+
apply (clarsimp simp: is_tcb)
done
unfolding set_thread_state_def
by (wpsimp wp: set_object_wp dxo_wp_weak simp: is_tcb)
lemma lcs_reply_owns:
"\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
@ -687,9 +685,9 @@ lemma set_thread_state_restart_to_running_respects:
set_thread_state thread Structures_A.thread_state.Running
od
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (simp add: set_thread_state_def set_object_def as_user_def split_def setNextPC_def
getRestartPC_def setRegister_def bind_assoc getRegister_def)
apply wp
apply (simp add: set_thread_state_def as_user_def split_def setNextPC_def
getRestartPC_def setRegister_def bind_assoc getRegister_def)
apply (wpsimp wp: set_object_wp)
apply (clarsimp simp: in_monad fun_upd_def[symmetric] cong: if_cong)
apply (cases "is_subject aag thread")
apply (cut_tac aag=aag in integrity_update_autarch, simp+)
@ -806,7 +804,7 @@ lemma as_user_set_register_respects_indirect:
\<and> (aag_has_auth_to aag Notify ntfnptr)) \<rbrace>
as_user thread (setRegister r v)
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: as_user_def split_def set_object_def)
apply (simp add: as_user_def split_def set_object_def get_object_def)
apply wp
apply (clarsimp simp: in_monad setRegister_def)
apply (cases "is_subject aag thread")
@ -1106,16 +1104,11 @@ lemma set_thread_state_current_ipc_buffer_register[wp]:
lemma set_simple_ko_current_ipc_buffer_register[wp]:
"\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_simple_ko f t ep \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>"
apply (clarsimp simp: set_simple_ko_def )
apply (wp dxo_wp_weak | wpc)+
apply (clarsimp simp: set_thread_state_def get_object_def set_object_def valid_def put_def
gets_def assert_def bind_def get_def return_def fail_def gets_the_def
assert_opt_def
split: option.splits kernel_object.splits)
apply simp
apply (wp get_object_wp | simp add: get_simple_ko_def | wpc)+
apply (auto simp: a_type_def partial_inv_def obj_at_def current_ipc_buffer_register_def get_tcb_def
split: kernel_object.split_asm)
apply (simp add: set_simple_ko_def)
including unfold_objects
apply (wpsimp wp: set_object_wp_strong)
apply (auto simp: a_type_def partial_inv_def current_ipc_buffer_register_def get_tcb_def
split: kernel_object.split_asm if_splits)
done
lemma update_tcb_current_ipc_buffer_register:
@ -1156,28 +1149,18 @@ lemma set_bounded_notification_current_ipc_buffer_register[wp]:
lemma set_pd_current_ipc_buffer_register[wp]:
"\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_pd ptr pd \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>"
apply (clarsimp simp: set_pd_def )
apply (wp | wpc)+
apply (clarsimp simp: set_thread_state_def get_object_def set_object_def valid_def put_def
gets_def assert_def bind_def get_def return_def fail_def gets_the_def
assert_opt_def
split: option.splits kernel_object.splits)
apply simp
apply (wp get_object_wp | simp add: get_simple_ko_def | wpc)+
apply (auto simp: obj_at_def current_ipc_buffer_register_def get_tcb_def split: kernel_object.split_asm)
apply (clarsimp simp: set_pd_def)
apply (wpsimp wp: set_object_wp_strong)
apply (auto simp: obj_at_def current_ipc_buffer_register_def get_tcb_def
split: kernel_object.split_asm)
done
lemma set_pt_current_ipc_buffer_register[wp]:
"\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_pt ptr pt \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>"
apply (clarsimp simp: set_pt_def )
apply (wp | wpc)+
apply (clarsimp simp: set_thread_state_def get_object_def set_object_def valid_def put_def
gets_def assert_def bind_def get_def return_def fail_def gets_the_def
assert_opt_def
split: option.splits kernel_object.splits)
apply simp
apply (wp get_object_wp | simp add: get_simple_ko_def | wpc)+
apply (auto simp: obj_at_def current_ipc_buffer_register_def get_tcb_def split: kernel_object.split_asm)
apply (clarsimp simp: set_pt_def)
apply (wpsimp wp: set_object_wp_strong)
apply (auto simp: obj_at_def current_ipc_buffer_register_def get_tcb_def
split: kernel_object.split_asm)
done
crunch current_ipc_buffer_register [wp]: post_cap_deletion, cap_delete_one "\<lambda>s. P (current_ipc_buffer_register s)"
@ -1290,15 +1273,10 @@ lemma reply_cancel_ipc_current_ipc_buffer_register[wp]:
lemma set_asid_pool_current_ipc_buffer_register[wp]:
"\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_asid_pool a b \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>"
apply (clarsimp simp: set_asid_pool_def)
apply (rule_tac Q = "\<lambda>r s. P (current_ipc_buffer_register s)" in hoare_post_imp)
apply simp
apply (clarsimp simp: get_object_def set_object_def valid_def put_def
gets_def assert_def bind_def get_def return_def
fail_def gets_the_def
thread_set_def assert_opt_def get_tcb_def
split: option.splits kernel_object.splits)
apply (clarsimp simp: current_ipc_buffer_register_def get_tcb_def)
apply (simp add: set_asid_pool_def)
apply (wpsimp wp: set_object_wp_strong
simp: current_ipc_buffer_register_def get_tcb_def obj_at_def
split: kernel_object.splits)
done
crunch current_ipc_buffer_register [wp]: finalise_cap "\<lambda>s. P (current_ipc_buffer_register s)"
@ -1352,7 +1330,8 @@ lemma set_tcb_context_current_ipc_buffer_register:
obj_at (\<lambda>obj. obj = TCB tcb) f s)) \<and> P (current_ipc_buffer_register s)\<rbrace>
set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>))
\<lbrace>\<lambda>_ s. P (current_ipc_buffer_register s)\<rbrace>"
by (auto simp: current_ipc_buffer_register_def get_tcb_def set_object_def get_def put_def bind_def valid_def return_def obj_at_def)
apply (wpsimp wp: set_object_wp)
by (auto simp: current_ipc_buffer_register_def get_tcb_def obj_at_def)
lemma as_user_current_ipc_buffer_register[wp]:
assumes uc: "\<And>P. \<lbrace>\<lambda>s. P (s TPIDRURW)\<rbrace> a \<lbrace>\<lambda>r s. P (s TPIDRURW)\<rbrace>"

5
proof/access-control/Tcb_AC.thy
View File

@ -373,9 +373,8 @@ lemma sbn_bind_respects:
and K ((pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> is_subject aag t)\<rbrace>
set_bound_notification t (Some ntfn)
\<lbrace>\<lambda>rv. integrity aag X st \<rbrace>"
apply (simp add: set_bound_notification_def set_object_def)
apply wp
apply clarsimp
apply (simp add: set_bound_notification_def)
apply (wpsimp wp: set_object_wp)
apply (erule integrity_trans)
apply (clarsimp simp: integrity_def obj_at_def pred_tcb_at_def)
done