1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory Ipc_IF 12imports Finalise_IF 13begin 14 15context begin interpretation Arch . (*FIXME: arch_split*) 16 17section "reads_respects" 18subsection "Notifications" 19 20lemma equiv_valid_2_get_assert: 21 "equiv_valid_2 I A A R P P' f f' \<Longrightarrow> 22 equiv_valid_2 I A A R P P' (get >>= (\<lambda> s. assert (g s) >>= (\<lambda> y. f))) (get >>= (\<lambda> s. assert (g' s) >>= (\<lambda> y. f')))" 23 apply(rule equiv_valid_2_guard_imp) 24 apply(rule_tac R'="\<top>\<top>" in equiv_valid_2_bind) 25 apply(rule_tac R'="\<top>\<top>" in equiv_valid_2_bind) 26 apply assumption 27 apply(simp add: assert_ev2) 28 apply(wp equiv_valid_rv_trivial | simp)+ 29 done 30 31lemma dummy_machine_state_update: 32 "st = st\<lparr>machine_state := machine_state st\<rparr>" 33 apply simp 34 done 35 36lemma dmo_storeWord_modifies_at_most: 37 "modifies_at_most aag (pasObjectAbs aag ` ptr_range p 2) \<top> 38 (do_machine_op (storeWord p w))" 39 apply(rule modifies_at_mostI) 40 apply(simp add: do_machine_op_def storeWord_def) 41 apply(wp modify_wp | simp add: split_def)+ 42 apply clarsimp 43 apply(erule use_valid) 44 apply(wp modify_wp) 45 apply(clarsimp simp: equiv_but_for_labels_def) 46 apply(subst (asm) is_aligned_mask[symmetric]) 47 apply(subst dummy_machine_state_update) 48 apply(rule states_equiv_for_machine_state_update) 49 apply assumption 50 apply (erule states_equiv_forE_mem) 51 apply (intro conjI equiv_forI) 52 apply(fastforce simp: image_def dest: distinct_lemma[where f="pasObjectAbs aag"] intro: ptr_range_memI ptr_range_add_memI)+ 53 done 54 55 56 57lemma get_object_reads_respects: 58 "reads_respects aag l (K (aag_can_read aag oref \<or> aag_can_affect aag l oref)) (get_object oref)" 59 unfolding get_object_def 60 apply(subst gets_apply) 61 apply(wp gets_apply_ev | wpc | simp)+ 62 apply(blast intro: reads_affects_equiv_kheap_eq) 63 done 64 65lemma get_cap_reads_respects: 66 "reads_respects aag l (K (aag_can_read aag (fst slot) \<or> aag_can_affect aag l (fst slot))) (get_cap slot)" 67 apply(simp add: get_cap_def split_def) 68 apply(wp get_object_reads_respects | wpc | simp)+ 69 done 70 71lemma lookup_ipc_buffer_reads_respects: 72 "reads_respects aag l (K (aag_can_read aag thread \<or> aag_can_affect aag l thread)) (lookup_ipc_buffer is_receiver thread)" 73 unfolding lookup_ipc_buffer_def 74 apply(wp thread_get_reads_respects get_cap_reads_respects | wpc | simp)+ 75 done 76 77 78lemmas lookup_ipc_buffer_reads_respects_g = reads_respects_g_from_inv[OF lookup_ipc_buffer_reads_respects lookup_ipc_buffer_inv] 79 80lemma as_user_equiv_but_for_labels: 81 "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace> 82 as_user thread f 83 \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" 84 unfolding as_user_def 85 apply (wp set_object_equiv_but_for_labels | simp add: split_def)+ 86 apply(blast dest: get_tcb_not_asid_pool_at) 87 done 88 89crunch equiv_but_for_labels: set_message_info "equiv_but_for_labels aag L st" 90 91 92lemma storeWord_equiv_but_for_labels: 93 "\<lbrace>\<lambda>ms. equiv_but_for_labels aag L st (s\<lparr>machine_state := ms\<rparr>) \<and> 94 for_each_byte_of_word (\<lambda> x. pasObjectAbs aag x \<in> L) p\<rbrace> 95 storeWord p v \<lbrace>\<lambda>a b. equiv_but_for_labels aag L st (s\<lparr>machine_state := b\<rparr>)\<rbrace>" 96 unfolding storeWord_def 97 apply (wp modify_wp) 98 apply (clarsimp simp: equiv_but_for_labels_def) 99 apply (rule states_equiv_forI) 100 apply(fastforce intro!: equiv_forI elim!: states_equiv_forE dest: equiv_forD[where f=kheap]) 101 apply (simp add: states_equiv_for_def) 102 apply (rule conjI) 103 apply(rule equiv_forI) 104 apply clarsimp 105 apply(drule_tac f=underlying_memory in equiv_forD,fastforce) 106 apply(fastforce intro: is_aligned_no_wrap' word_plus_mono_right simp: is_aligned_mask for_each_byte_of_word_def) 107 apply(rule equiv_forI) 108 apply clarsimp 109 apply(drule_tac f=device_state in equiv_forD,fastforce) 110 apply clarsimp 111 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt]) 112 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ekheap]) 113 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt_list]) 114 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=is_original_cap]) 115 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_states]) 116 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_irq_node]) 117 apply(fastforce simp: equiv_asids_def equiv_asid_def elim: states_equiv_forE) 118 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ready_queues]) 119 done 120 121lemma store_word_offs_equiv_but_for_labels: 122 "\<lbrace> equiv_but_for_labels aag L st and K (for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (ptr + of_nat offs * of_nat word_size)) \<rbrace> 123 store_word_offs ptr offs v 124 \<lbrace> \<lambda>_. equiv_but_for_labels aag L st \<rbrace>" 125 unfolding store_word_offs_def 126 apply(wp modify_wp | simp add: do_machine_op_def split_def)+ 127 apply clarsimp 128 apply(erule use_valid[OF _ storeWord_equiv_but_for_labels]) 129 apply simp 130 done 131 132definition 133 ipc_buffer_has_read_auth :: "'a PAS \<Rightarrow> 'a \<Rightarrow> word32 option \<Rightarrow> bool" 134where 135"ipc_buffer_has_read_auth aag l \<equiv> 136 case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits \<and> (\<forall>x \<in> ptr_range buf' msg_align_bits. (l,Read,pasObjectAbs aag x) \<in> (pasPolicy aag)))" 137 138 139lemma set_mrs_equiv_but_for_labels: 140 "\<lbrace> equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> 141 (case buf of (Some buf') \<Rightarrow> 142 is_aligned buf' msg_align_bits \<and> 143 (\<forall>x \<in> ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L) 144 | _ \<Rightarrow> True)) \<rbrace> 145 set_mrs thread buf msgs 146 \<lbrace> \<lambda>_. equiv_but_for_labels aag L st \<rbrace>" 147 unfolding set_mrs_def 148 apply (wp | wpc)+ 149 apply(subst zipWithM_x_mapM_x) 150 apply(rule_tac Q="\<lambda>_. equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> 151 (case buf of (Some buf') \<Rightarrow> 152 is_aligned buf' msg_align_bits \<and> 153 (\<forall>x \<in> ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L) 154 | _ \<Rightarrow> True))" in hoare_strengthen_post) 155 apply(wp mapM_x_wp' store_word_offs_equiv_but_for_labels | simp add: split_def)+ 156 apply(case_tac xa, clarsimp split: if_split_asm elim!: in_set_zipE) 157 apply(clarsimp simp: for_each_byte_of_word_def) 158 apply(erule bspec) 159 apply(clarsimp simp: ptr_range_def) 160 apply(rule conjI) 161 apply(erule order_trans[rotated]) 162 apply(erule is_aligned_no_wrap') 163 apply(rule mul_word_size_lt_msg_align_bits_ofnat) 164 apply(fastforce simp: msg_max_length_def msg_align_bits) 165 apply(erule order_trans) 166 apply(subst p_assoc_help) 167 apply(simp add: add.assoc) 168 apply(rule word_plus_mono_right) 169 apply(rule word_less_sub_1) 170 apply(rule_tac y="of_nat msg_max_length * of_nat word_size + 3" in le_less_trans) 171 apply(rule word_plus_mono_left) 172 apply(rule word_mult_le_mono1) 173 apply(erule disjE) 174 apply(rule word_of_nat_le) 175 apply(simp add: msg_max_length_def) 176 apply clarsimp 177 apply(rule word_of_nat_le) 178 apply(simp add: msg_max_length_def) 179 apply(simp add: word_size_def) 180 apply(simp add: msg_max_length_def word_size_def) 181 apply(simp add: msg_max_length_def word_size_def) 182 apply(rule mul_add_word_size_lt_msg_align_bits_ofnat) 183 apply(simp add: msg_max_length_def msg_align_bits) 184 apply simp 185 apply(erule is_aligned_no_overflow') 186 apply simp 187 apply(wp set_object_equiv_but_for_labels hoare_vcg_all_lift static_imp_wp | simp)+ 188 apply (fastforce dest: get_tcb_not_asid_pool_at)+ 189 done 190 191 192definition all_to_which_has_auth where 193 "all_to_which_has_auth aag auth source \<equiv> {t. (source,auth,t) \<in> pasPolicy aag}" 194 195definition all_with_auth_to where 196 "all_with_auth_to aag auth target \<equiv> {x. (x, auth, target) \<in> pasPolicy aag}" 197 198lemma valid_ntfn_WaitingNtfn_tl: 199 "\<lbrakk>ntfn_obj ntfn = (WaitingNtfn list); valid_ntfn ntfn s; tl list \<noteq> []; ntfn' = ntfn\<lparr>ntfn_obj := (WaitingNtfn (tl list))\<rparr> \<rbrakk> \<Longrightarrow> 200 valid_ntfn ntfn' s" 201 apply(case_tac list, simp_all) 202 apply(rename_tac a lista) 203 apply(case_tac lista, simp_all) 204 apply(clarsimp simp: valid_ntfn_def split: option.splits) 205 done 206 207lemma update_waiting_ntfn_reads_respects: 208 assumes domains_distinct[wp]: "pas_domains_distinct aag" 209 notes tl_drop_1[simp del] 210 shows 211 "reads_respects aag l (valid_objs and sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag and ko_at (Notification ntfn) ntfnptr and (\<lambda>s. is_subject aag (cur_thread s)) and K (ntfn_obj ntfn = WaitingNtfn queue)) (update_waiting_ntfn ntfnptr queue bound_tcb badge)" 212 unfolding update_waiting_ntfn_def fun_app_def 213 apply (wp assert_sp possible_switch_to_reads_respects gets_cur_thread_ev | simp add: split_def)+ 214 apply (wp as_user_set_register_reads_respects' set_thread_state_reads_respects 215 set_simple_ko_reads_respects set_thread_state_pas_refined 216 set_simple_ko_valid_objs hoare_vcg_disj_lift set_simple_ko_pas_refined 217 | simp add: split_def reads_lrefl)+ 218 done 219 220lemma set_thread_state_ext_runnable_equiv_but_for_labels: 221 "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L) and st_tcb_at runnable thread\<rbrace> 222 set_thread_state_ext thread 223 \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" 224 apply (simp add: set_thread_state_ext_def) 225 apply wp 226 apply (rule hoare_pre_cont) 227 apply (wp gts_wp)+ 228 apply (force simp: st_tcb_at_def obj_at_def) 229 done 230 231lemma set_thread_state_runnable_equiv_but_for_labels: 232 "runnable tst \<Longrightarrow> \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace> 233 set_thread_state thread tst 234 \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" 235 unfolding set_thread_state_def 236 apply (wp set_object_equiv_but_for_labels set_thread_state_ext_runnable_equiv_but_for_labels | simp add: split_def)+ 237 apply (simp add: set_object_def, wp+) 238 apply (fastforce dest: get_tcb_not_asid_pool_at simp: st_tcb_at_def obj_at_def) 239 done 240 241lemma tcb_sched_action_equiv_but_for_labels: 242 "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L) and pas_refined aag\<rbrace> 243 tcb_sched_action action thread 244 \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" 245 apply (simp add: tcb_sched_action_def, wp) 246 apply (clarsimp simp: etcb_at_def equiv_but_for_labels_def split: option.splits) 247 apply (rule states_equiv_forI) 248 apply(fastforce intro!: equiv_forI elim!: states_equiv_forE dest: equiv_forD[where f=kheap]) 249 apply (simp add: states_equiv_for_def) 250 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt]) 251 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ekheap]) 252 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt_list]) 253 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=is_original_cap]) 254 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_states]) 255 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_irq_node]) 256 apply(fastforce simp: equiv_asids_def equiv_asid_def elim: states_equiv_forE) 257 apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def split: option.splits) 258 apply (rule equiv_forI) 259 apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE) 260 apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ready_queues]) 261 apply (force intro: domtcbs) 262 done 263 264lemma possible_switch_to_equiv_but_for_labels: 265 "\<lbrace>equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s) and K (pasObjectAbs aag target \<in> L) and pas_refined aag\<rbrace> 266 possible_switch_to target 267 \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" 268 apply (simp add: possible_switch_to_def) 269 apply (wp tcb_sched_action_equiv_but_for_labels) 270 (* possible_switch_to does not modify scheduler action if target is in different domain *) 271 apply (rule hoare_pre_cont) 272 apply (wp tcb_sched_action_equiv_but_for_labels) 273 apply (rule hoare_pre_cont) 274 apply (wp tcb_sched_action_equiv_but_for_labels)+ 275 apply (clarsimp simp: etcb_at_def split: option.splits) 276 done 277 278crunch etcb_at_cdom[wp]: set_thread_state_ext, set_thread_state, set_simple_ko 279 "\<lambda>s. etcb_at (P (cur_domain s)) t s" 280 (wp: crunch_wps) 281 282lemma update_waiting_ntfn_equiv_but_for_labels: 283 notes tl_drop_1[simp del] 284 shows 285 "\<lbrace> equiv_but_for_labels aag L st and pas_refined aag and valid_objs and 286 ko_at (Notification ntfn) ntfnptr and 287 sym_refs \<circ> state_refs_of and 288 (\<lambda>s. \<forall>t\<in> set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) and 289 K (ntfn_obj ntfn = WaitingNtfn list \<and> pasObjectAbs aag ntfnptr \<in> L \<and> 290 all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<subseteq> L \<and> 291 \<Union> ((all_to_which_has_auth aag Write) ` (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) \<subseteq> L)\<rbrace> 292 update_waiting_ntfn ntfnptr list boundtcb badge 293 \<lbrace> \<lambda>_. equiv_but_for_labels aag L st \<rbrace>" 294 unfolding update_waiting_ntfn_def 295 apply (wp static_imp_wp as_user_equiv_but_for_labels set_thread_state_runnable_equiv_but_for_labels 296 set_thread_state_pas_refined set_notification_equiv_but_for_labels 297 set_simple_ko_pred_tcb_at set_simple_ko_pas_refined 298 hoare_vcg_disj_lift possible_switch_to_equiv_but_for_labels 299 | wpc | simp add: split_def)+ 300 apply (clarsimp simp: conj_ac) 301 apply(frule_tac P="receive_blocked_on ntfnptr" and t="hd list" in ntfn_queued_st_tcb_at') 302 apply(fastforce) 303 apply assumption 304 apply assumption 305 apply simp 306 apply (subgoal_tac "pasObjectAbs aag (hd list) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)") 307 apply(fastforce) 308 apply(clarsimp simp: all_with_auth_to_def) 309 apply (erule pas_refined_mem[rotated]) 310 apply (rule sta_ts) 311 apply(clarsimp simp: thread_states_def split: option.split simp: tcb_states_of_state_def st_tcb_def2) 312 apply(case_tac "tcb_state tcb", simp_all) 313 done 314 315 316lemma update_waiting_ntfn_modifies_at_most: 317 "modifies_at_most aag 318 ({pasObjectAbs aag ntfnptr} \<union> 319 all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> 320 \<Union> ((all_to_which_has_auth aag Write) ` (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) 321 (pas_refined aag and valid_objs and 322 ko_at (Notification ntfn) ntfnptr and 323 (\<lambda>s. \<forall>t\<in> set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) and 324 sym_refs \<circ> state_refs_of and K (ntfn_obj ntfn = WaitingNtfn list)) 325 (update_waiting_ntfn ntfnptr list boundtcb badge)" 326 apply(rule modifies_at_mostI) 327 apply(wp update_waiting_ntfn_equiv_but_for_labels | fastforce)+ 328 done 329 330 331lemma invisible_ntfn_invisible_receivers_and_ipcbuffers: 332 "\<lbrakk>labels_are_invisible aag l {pasObjectAbs aag ntfnptr}; 333 (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> 334 \<Longrightarrow> labels_are_invisible aag l 335 ({pasObjectAbs aag ntfnptr} \<union> 336 all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> 337 \<Union>(all_to_which_has_auth aag Write ` 338 all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))" 339 apply(auto simp: labels_are_invisible_def aag_can_affect_label_def dest: reads_read_page_read_thread reads_read_queued_thread_read_ep simp: all_to_which_has_auth_def all_with_auth_to_def) 340 done 341 342lemma invisible_ntfn_invisible_receivers_and_receivers: 343 "\<lbrakk>labels_are_invisible aag l {pasObjectAbs aag ntfnptr}; 344 (pasSubject aag, auth, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; 345 auth \<in> {Notify,Receive,SyncSend}\<rbrakk> 346 \<Longrightarrow> labels_are_invisible aag l 347 ({pasObjectAbs aag ntfnptr} \<union> 348 all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> 349 (\<Union>(all_to_which_has_auth aag Receive ` 350 all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) \<union> 351 (\<Union>(all_to_which_has_auth aag Write ` 352 all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))))" 353 by (auto simp: labels_are_invisible_def aag_can_affect_label_def 354 dest: read_sync_ep_read_senders_strong read_sync_ep_read_receivers_strong 355 reads_read_queued_thread_read_ep 356 reads_read_page_read_thread 357 reads_ep 358 simp: all_to_which_has_auth_def all_with_auth_to_def) 359 360lemma read_queued_thread_reads_ntfn: 361 "\<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t; 362 valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue; 363 (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> 364 \<Longrightarrow> aag_can_read aag ntfnptr" 365 apply(frule_tac P="receive_blocked_on ntfnptr" and t=t in ntfn_queued_st_tcb_at') 366 apply(fastforce) 367 apply assumption 368 apply assumption 369 apply simp 370 apply (rule_tac t="pasObjectAbs aag t" and auth="Receive" and auth'="Notify" in reads_read_queued_thread_read_ep) 371 apply assumption 372 apply simp 373 apply (erule pas_refined_mem[rotated]) 374 apply (rule sta_ts) 375 apply(clarsimp simp: thread_states_def split: option.split simp: tcb_states_of_state_def st_tcb_def2) 376 apply (case_tac "tcb_state tcb", simp_all)[1] 377 apply simp 378 apply simp 379 done 380 381lemma not_etcb_at_not_cdom_can_read: 382 assumes domains_distinct[wp]: "pas_domains_distinct aag" 383 shows 384 "\<lbrakk>\<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; 385 tcb_at t s; valid_etcbs s; pas_refined aag s; pas_cur_domain aag s\<rbrakk> 386 \<Longrightarrow> aag_can_read aag t" 387 apply (clarsimp simp: valid_etcbs_def tcb_at_st_tcb_at etcb_at_def is_etcb_at_def 388 pas_refined_def tcb_domain_map_wellformed_aux_def) 389 apply (erule_tac x="(t, cur_domain s)" in ballE) 390 apply (force dest: domains_distinct[THEN pas_domains_distinct_inj]) 391 apply (force intro: domtcbs) 392 done 393 394lemma tcb_at_ntfn_queue: 395 "\<lbrakk>valid_objs s; t \<in> set queue; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn queue\<rbrakk> 396 \<Longrightarrow> tcb_at t s" 397 apply (erule valid_objsE, force simp: obj_at_def) 398 apply (simp add: valid_obj_def valid_ntfn_def) 399 done 400 401 402lemma invisible_ep_invisible_receiver: 403 "\<lbrakk>labels_are_invisible aag l {pasObjectAbs aag epptr}; 404 (pasObjectAbs aag tcb, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag; 405 (pasObjectAbs aag tcb, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> 406 \<Longrightarrow> labels_are_invisible aag l 407 ({pasObjectAbs aag epptr} \<union> {pasObjectAbs aag tcb})" 408 apply (auto simp: labels_are_invisible_def aag_can_affect_label_def 409 all_with_auth_to_def 410 dest: reads_ep reads_read_queued_thread_read_ep) 411 done 412 413 414lemma no_fail_gts:"no_fail (tcb_at tcb) (get_thread_state tcb)" 415 apply (clarsimp simp: get_thread_state_def thread_get_def) 416 apply (rule no_fail_pre) 417 apply wp 418 by (clarsimp simp: get_tcb_def tcb_at_def) 419 420lemma monadic_rewrite_impossible: "monadic_rewrite F E (\<lambda>_. False) f g" 421 by (clarsimp simp: monadic_rewrite_def) 422 423lemma monadic_rewrite_add_get: 424 "monadic_rewrite F E P (do x <- get; f od) (do x <- get; g od) \<Longrightarrow> 425 monadic_rewrite F E P f g" 426 by (clarsimp simp: bind_def get_def) 427 428lemma sts_noop: 429 "monadic_rewrite True True (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) 430 (set_thread_state_ext tcb) 431 (return ())" 432 apply (rule monadic_rewrite_imp) 433 apply (rule monadic_rewrite_add_get) 434 apply (rule monadic_rewrite_bind_tail) 435 apply (clarsimp simp: set_thread_state_ext_def) 436 apply (rule_tac x="tcb_state (the (get_tcb tcb x))" in monadic_rewrite_symb_exec) 437 apply (wp gts_wp | simp)+ 438 apply (rule monadic_rewrite_symb_exec) 439 apply wp+ 440 apply (rule monadic_rewrite_symb_exec) 441 apply wp+ 442 apply (simp only: when_def) 443 apply (rule monadic_rewrite_trans) 444 apply (rule monadic_rewrite_if) 445 apply (rule monadic_rewrite_impossible[where g="return ()"]) 446 apply (rule monadic_rewrite_refl) 447 apply simp 448 apply (rule monadic_rewrite_refl) 449 apply wp 450 by (auto simp: pred_tcb_at_def obj_at_def is_tcb_def get_tcb_def) 451 452lemma sts_to_modify': 453 "monadic_rewrite True True (tcb_at tcb and (\<lambda>s :: det_ext state. tcb \<noteq> cur_thread s)) 454 (set_thread_state tcb st) (modify (\<lambda>s. s\<lparr>kheap := kheap s(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))" 455 apply (clarsimp simp: set_thread_state_def set_object_def) 456 apply (rule monadic_rewrite_add_get) 457 apply (rule monadic_rewrite_bind_tail) 458 apply (rule monadic_rewrite_imp) 459 apply (rule monadic_rewrite_trans) 460 apply (simp only: bind_assoc[symmetric]) 461 apply (rule monadic_rewrite_bind_tail) 462 apply (rule sts_noop) 463 apply wp 464 apply simp 465 apply (rule_tac x="the (get_tcb tcb x)" in monadic_rewrite_symb_exec,(wp | simp)+) 466 apply (rule_tac x="x" in monadic_rewrite_symb_exec,(wp | simp)+) 467 apply (rule_tac P="(=) x" in monadic_rewrite_refl3) 468 apply (clarsimp simp add: put_def modify_def get_def bind_def) 469 apply assumption 470 apply wp 471 by (clarsimp simp: get_tcb_def tcb_at_def) 472 473 474lemma 475 monadic_rewrite_weaken_failure: 476 "monadic_rewrite True True P f f' \<Longrightarrow> 477 no_fail P' f \<Longrightarrow> no_fail Q' f' \<Longrightarrow> 478 monadic_rewrite F E (P and P' and Q') f f'" 479 by (clarsimp simp: monadic_rewrite_def no_fail_def) 480 481lemma 482 sts_no_fail: 483 "no_fail (\<lambda>s :: det_ext state. tcb_at tcb s) (set_thread_state tcb st)" 484 apply (simp add: set_thread_state_def set_object_def) 485 apply (simp add: set_thread_state_ext_def get_thread_state_def thread_get_def set_scheduler_action_def) 486 apply (rule no_fail_pre) 487 apply wp 488 by (clarsimp simp: get_tcb_def tcb_at_def) 489 490lemmas sts_to_modify = monadic_rewrite_weaken_failure[OF sts_to_modify' sts_no_fail no_fail_modify,simplified] 491 492definition "blocked_cancel_ipc_nosts tcb \<equiv> 493 do state <- get_thread_state tcb; 494 epptr \<leftarrow> get_blocking_object state; 495 ep \<leftarrow> get_endpoint epptr; 496 queue \<leftarrow> get_ep_queue ep; 497 queue' \<leftarrow> return $ remove1 tcb queue; 498 ep' \<leftarrow> return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue'); 499 set_endpoint epptr ep'; 500 set_thread_state tcb Running 501 od" 502 503lemma cancel_ipc_to_blocked_nosts: 504 "monadic_rewrite False False 505 (\<lambda>s. st_tcb_at receive_blocked tcb (s :: det_ext state) \<and> 506 cur_thread s \<noteq> tcb) 507 (blocked_cancel_ipc_nosts tcb) 508 (cancel_ipc tcb >>= (\<lambda>_. set_thread_state tcb Running))" 509 apply (simp add: cancel_ipc_def bind_assoc blocked_cancel_ipc_nosts_def) 510 apply (rule monadic_rewrite_bind_tail) 511 apply (rule monadic_rewrite_transverse) 512 apply (rename_tac state) 513 apply (rule_tac P="\<lambda>_. \<exists>xa. state = BlockedOnReceive xa" in monadic_rewrite_bind_head) 514 apply (rule monadic_rewrite_gen_asm[where Q=\<top>,simplified]) 515 apply clarsimp 516 apply (rule monadic_rewrite_refl) 517 apply (simp add: blocked_cancel_ipc_def blocked_cancel_ipc_nosts_def bind_assoc) 518 apply (rule monadic_rewrite_bind_tail) 519 apply (rule monadic_rewrite_bind_tail) 520 apply (rule monadic_rewrite_bind_tail) 521 apply (rule monadic_rewrite_bind_tail) 522 apply (rule monadic_rewrite_trans) 523 apply (rule sts_to_modify) 524 apply (rule monadic_rewrite_transverse) 525 apply (rule monadic_rewrite_bind) 526 apply (rule sts_to_modify) 527 apply (rule sts_to_modify) 528 apply (rule hoare_modifyE_var[where P="tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)"]) 529 apply (clarsimp simp: tcb_at_def get_tcb_def) 530 apply (simp add: modify_modify) 531 apply (rule monadic_rewrite_refl2) 532 apply (fastforce simp add: simpler_modify_def o_def get_tcb_def) 533 apply (wp gts_wp)+ 534 apply (simp add: set_thread_state_def bind_assoc gets_the_def) 535 apply (clarsimp simp add: pred_tcb_at_def receive_blocked_def obj_at_def is_tcb_def split: thread_state.splits) 536 by (case_tac "tcb_state tcba";fastforce) 537 538 539lemma gts_reads_respects: 540 "reads_respects aag l (K (aag_can_read aag thread \<or> aag_can_affect aag l thread)) (get_thread_state thread)" 541 unfolding get_thread_state_def 542 by (wp thread_get_reads_respects) 543 544 545lemma ev2_invisible_simple: 546 assumes domains_distinct: "pas_domains_distinct aag" 547 shows 548 "labels_are_invisible aag l L \<Longrightarrow> 549 modifies_at_most aag L Q f \<Longrightarrow> 550 reads_respects aag l Q (f :: det_ext state \<Rightarrow> (unit \<times> det_ext state) set \<times> bool)" 551 apply (simp add: equiv_valid_def2) 552 apply (rule equiv_valid_2_guard_imp) 553 apply (rule ev2_invisible[OF domains_distinct]) 554 by fastforce+ 555 556lemma blocked_cancel_ipc_nosts_equiv_but_for_labels: 557 "\<lbrace>pas_refined aag and 558 st_tcb_at (\<lambda>st. st = BlockedOnReceive x) t and 559 bound_tcb_at ((=) (Some ntfnptr)) t and 560 equiv_but_for_labels aag L st and 561 K(pasObjectAbs aag x \<in> L) and 562 K(pasObjectAbs aag t \<in> L) \<rbrace> 563 blocked_cancel_ipc_nosts t 564 \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" 565 unfolding blocked_cancel_ipc_nosts_def get_blocking_object_def 566 apply (wp set_endpoint_equiv_but_for_labels get_object_wp gts_wp 567 set_thread_state_runnable_equiv_but_for_labels 568 | wpc 569 | simp)+ 570 by (clarsimp simp: pred_tcb_at_def obj_at_def) 571 572lemma blocked_cancel_ipc_nosts_reads_respects: 573 assumes domains_distinct[wp]: "pas_domains_distinct aag" 574 shows 575 "reads_respects aag l (pas_refined aag 576 and st_tcb_at (\<lambda>st. \<exists>xa. st = (BlockedOnReceive x)) t 577 578 and bound_tcb_at ((=) (Some ntfnptr)) t 579 and (\<lambda>s. is_subject aag (cur_thread s)) 580 and K ( 581 (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag 582 \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag 583 \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) 584 (blocked_cancel_ipc_nosts t)" 585 unfolding blocked_cancel_ipc_nosts_def 586 apply (simp only:bind_assoc[symmetric]) 587 apply (rule bind_ev[where P''=\<top>,simplified]) 588 apply (wp set_thread_state_runnable_reads_respects,simp) 589 590 subgoal 591 proof (cases "aag_can_read_label aag (pasObjectAbs aag x) \<or> aag_can_affect aag l x") 592 case True thus ?thesis \<comment> \<open>boring case, can read or affect ep\<close> 593 unfolding blocked_cancel_ipc_nosts_def get_blocking_object_def 594 apply clarsimp 595 apply (rule pre_ev) 596 apply ((wp set_thread_state_reads_respects get_ep_queue_reads_respects 597 get_simple_ko_reads_respects get_blocking_object_reads_respects 598 gts_reads_respects set_simple_ko_reads_respects 599 gts_wp 600 | wpc 601 | simp add: get_blocking_object_def get_thread_state_rev)+)[2] 602 apply (clarsimp simp: pred_tcb_at_def obj_at_def) 603 by (fastforce dest:read_sync_ep_read_receivers_strong ) 604 605 next 606 case False thus ?thesis apply - \<comment> \<open>can't read or affect ep\<close> 607 apply (rule gen_asm_ev) 608 apply (drule label_is_invisible[THEN iffD2]) 609 apply clarsimp 610 apply (rule ev2_invisible_simple[OF domains_distinct],assumption) 611 apply (simp add: get_blocking_object_def) 612 apply (rule modifies_at_mostI) 613 apply (rule hoare_pre) 614 apply (wp set_thread_state_runnable_equiv_but_for_labels 615 set_endpoint_equiv_but_for_labels get_object_wp gts_wp 616 set_thread_state_runnable_equiv_but_for_labels 617 | wpc 618 | simp)+ 619 by (fastforce simp: pred_tcb_at_def obj_at_def) 620 qed 621 by wp 622 623crunch silc_inv[wp]: "blocked_cancel_ipc_nosts" "silc_inv aag st" 624 625lemmas blocked_cancel_ipc_nosts_reads_respects_f = 626 reads_respects_f[where Q=\<top>,simplified, 627 OF blocked_cancel_ipc_nosts_reads_respects 628 blocked_cancel_ipc_nosts_silc_inv, 629 simplified] 630 631lemma monadic_rewrite_is_valid: 632 "monadic_rewrite False False P' f f' \<Longrightarrow> 633 \<lbrace>P\<rbrace> do x <- f; g x od \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P and P'\<rbrace> do x <- f'; g x od \<lbrace>Q\<rbrace>" 634 by (fastforce simp: monadic_rewrite_def valid_def bind_def) 635 636lemma monadic_rewrite_reads_respects: 637 "monadic_rewrite False False P f f' \<Longrightarrow> 638 reads_respects l aag P' (do x <- f; g x od) \<Longrightarrow> 639 reads_respects l aag (P and P') (do x <- f'; g x od)" 640 apply (clarsimp simp: monadic_rewrite_def equiv_valid_def 641 spec_equiv_valid_def equiv_valid_2_def 642 bind_def) 643 apply (frule_tac x=st in spec) 644 apply (drule_tac x=t in spec) 645 by fastforce 646 647 648lemmas cancel_ipc_reads_respects_rewrite = 649 monadic_rewrite_reads_respects[OF cancel_ipc_to_blocked_nosts, simplified bind_assoc] 650 651lemmas cancel_ipc_valid_rewrite = 652 monadic_rewrite_is_valid[OF cancel_ipc_to_blocked_nosts, simplified bind_assoc] 653 654crunch etcb_at[wp]: blocked_cancel_ipc_nosts "etcb_at P t" 655crunch cur_domain[wp]: blocked_cancel_ipc_nosts "\<lambda>s. P (cur_domain s)" 656crunch pas_refined[wp]: blocked_cancel_ipc_nosts "pas_refined aag" 657crunch cur_thread[wp]: blocked_cancel_ipc_nosts "\<lambda>s. P (cur_thread s)" 658 659lemma BlockedOnReceive_inj: 660 "x = (case (BlockedOnReceive x) of BlockedOnReceive x \<Rightarrow> x)" 661 by (cases "BlockedOnReceive x";simp) 662 663 664lemma send_signal_reads_respects: 665 assumes domains_distinct[wp]: "pas_domains_distinct aag" 666 notes set_thread_state_owned_reads_respects[wp del] 667 cancel_ipc_pas_refined[wp del] 668 shows 669 "reads_respects aag l (pas_refined aag and pas_cur_domain aag and 670 (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and 671 (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and 672 K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) 673 (send_signal ntfnptr badge)" 674 unfolding send_signal_def fun_app_def 675 subgoal 676 proof (cases "aag_can_read aag ntfnptr \<or> aag_can_affect aag l ntfnptr") 677 case True 678 note visible = this 679 show ?thesis 680 apply (rule pre_ev) 681 apply (simp split del: if_split 682 | rule_tac ntfnptr=ntfnptr in blocked_cancel_ipc_nosts_reads_respects 683 | rule cancel_ipc_reads_respects_rewrite 684 | wp_once 685 set_simple_ko_reads_respects 686 possible_switch_to_reads_respects 687 as_user_set_register_reads_respects' 688 set_thread_state_pas_refined 689 set_thread_state_pas_refined 690 set_simple_ko_reads_respects 691 gts_reads_respects 692 cancel_ipc_receive_blocked_pas_refined 693 gts_wp 694 hoare_vcg_imp_lift 695 update_waiting_ntfn_reads_respects 696 get_simple_ko_wp 697 get_simple_ko_reads_respects 698 | wpc 699 | simp )+ 700 apply (insert visible) 701 apply clarsimp 702 apply (rule conjI[rotated]) 703 apply fastforce 704 apply (rule disjI2) 705 apply (intro impI allI) 706 apply (simp add: obj_at_def) 707 apply (rule conjI) 708 apply (frule (3) ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)",OF _ _ _ _ refl]) 709 apply (frule (1) bound_tcb_at_implies_receive) 710 apply (elim disjE) 711 apply (rule disjI1) 712 apply (fastforce dest:read_sync_ep_read_receivers_strong) 713 apply (rule disjI2) 714 apply (fastforce dest:read_sync_ep_read_receivers_strong) 715 apply (clarsimp) 716 apply (frule (1) ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)",OF _ _ _ _ refl]) 717 apply (fastforce simp: obj_at_def) 718 apply assumption 719 apply (rule conjI) 720 apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def) 721 apply (rule conjI[rotated]) 722 apply (frule (1) bound_tcb_at_implies_receive) 723 apply (frule (1) bound_tcb_at_implies_reset) 724 apply (clarsimp simp: pred_tcb_at_def get_tcb_def obj_at_def) 725 apply (rule context_conjI) 726 apply (fastforce simp: receive_blocked_def intro!: BlockedOnReceive_inj split:thread_state.splits) 727 apply (frule_tac t=x and tcb=tcb and ep = "case (tcb_state tcb) of BlockedOnReceive a \<Rightarrow> a" 728 in get_tcb_recv_blocked_implies_receive) 729 apply (fastforce simp: pred_tcb_at_def get_tcb_def obj_at_def) 730 apply (fastforce simp: receive_blocked_def split:thread_state.splits) 731 apply (fastforce simp: receive_blocked_def intro!: BlockedOnReceive_inj split:thread_state.splits) 732 by (fastforce simp: pred_tcb_at_def get_tcb_def obj_at_def receive_blocked_def 733 ct_in_state_def 734 split:thread_state.splits) 735 736 next 737 case False note invisible = this show ?thesis 738 apply (insert label_is_invisible[THEN iffD2, OF invisible]) 739 apply (rule gen_asm_ev) 740 apply (drule (1) invisible_ntfn_invisible_receivers_and_receivers) 741 apply simp 742 apply (rule ev2_invisible_simple[OF domains_distinct],assumption) 743 apply (rule modifies_at_mostI) 744 745 apply ( simp split del: if_split 746 | rule cancel_ipc_valid_rewrite 747 | wp_once 748 set_notification_equiv_but_for_labels 749 possible_switch_to_equiv_but_for_labels 750 as_user_equiv_but_for_labels 751 set_thread_state_runnable_equiv_but_for_labels 752 set_thread_state_pas_refined 753 blocked_cancel_ipc_nosts_equiv_but_for_labels 754 gts_wp 755 update_waiting_ntfn_equiv_but_for_labels 756 get_simple_ko_wp 757 | wpc 758 | wps 759 )+ 760 761 apply (elim conjE) 762 apply (match premises in "ntfn_bound_tcb _ = _" \<Rightarrow> \<open>fail\<close> 763 \<bar> _ \<Rightarrow> \<open>rule allI impI conjI\<close>)+ 764 prefer 2 765 apply (intro conjI allI impI; fastforce?) 766 subgoal waiting_ntfn 767 apply clarsimp 768 apply (rule ccontr) 769 apply (frule (3) not_etcb_at_not_cdom_can_read[OF domains_distinct, rotated 2]) 770 apply (rule tcb_at_ntfn_queue;assumption) 771 apply(frule (7) read_queued_thread_reads_ntfn) 772 using invisible 773 by (fastforce simp add: all_with_auth_to_def all_to_which_has_auth_def) 774 775 apply (frule (1) 776 ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)",OF _ _ _ _ refl]) 777 apply (fastforce simp: obj_at_def) 778 apply assumption 779 apply (intro allI conjI impI) 780 apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def split:thread_state.splits 781 intro!: BlockedOnReceive_inj) 782 apply assumption 783 apply distinct_subgoals 784 apply (fold_subgoals (prefix)) 785 apply (frule st_tcb_at_tcb_at) 786 subgoal bound_ntfn premises prems for st s ntfn x sta 787 prefer 2 788 apply (rule disjI2) 789 apply (rule disjI1) 790 subgoal bound_tcb_can_receive 791 using prems 792 apply (clarsimp simp: all_with_auth_to_def obj_at_def) 793 by (rule bound_tcb_at_implies_receive;assumption) 794 apply (rule disjI2) 795 apply (rule disjI2) 796 apply (rule disjI1) 797 subgoal bound_ep_can_receive 798 apply (rule bexI[OF _ bound_tcb_can_receive]) 799 apply (simp add: all_with_auth_to_def all_to_which_has_auth_def) 800 using prems 801 apply (case_tac sta;(clarsimp simp: pred_tcb_at_def obj_at_def receive_blocked_def split:thread_state.splits)) 802 apply (rule get_tcb_recv_blocked_implies_receive, assumption) 803 apply (fastforce simp: get_tcb_def) 804 by (fastforce split:thread_state.splits) 805 apply (rule ccontr) 806 apply (insert prems) 807 apply (frule (4) not_etcb_at_not_cdom_can_read[OF domains_distinct]) 808 using bound_tcb_can_receive 809 apply (fastforce simp: labels_are_invisible_def all_with_auth_to_def all_to_which_has_auth_def) 810 apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def) 811 apply (rule ccontr) 812 apply clarsimp 813 using invisible bound_tcb_can_receive reads_ep 814 by (fastforce simp add: all_with_auth_to_def all_to_which_has_auth_def) 815 done 816 qed 817 done 818 819lemma receive_signal_reads_respects: 820 assumes domains_distinct[wp]: "pas_domains_distinct aag" 821 shows 822 "reads_respects aag l (valid_objs and pas_refined aag and 823 (\<lambda>s. is_subject aag (cur_thread s)) and 824 K ((\<forall>ntfnptr\<in>Access.obj_refs cap. 825 (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) 826 \<in> pasPolicy aag \<and> is_subject aag thread))) 827 (receive_signal thread cap is_blocking)" 828 unfolding receive_signal_def fun_app_def do_nbrecv_failed_transfer_def 829 apply(wp set_simple_ko_reads_respects set_thread_state_reads_respects 830 as_user_set_register_reads_respects' get_simple_ko_reads_respects hoare_vcg_all_lift 831 | wpc 832 | wp_once hoare_drop_imps)+ 833 apply(force dest: reads_ep) 834 done 835 836subsection "Sync IPC" 837 838(* FIXME move *) 839lemma conj_imp: 840 "\<lbrakk>Q \<longrightarrow> R; P \<longrightarrow> Q; P' \<longrightarrow> Q\<rbrakk> \<Longrightarrow> 841 (P \<longrightarrow> R) \<and> (P' \<longrightarrow> R)" 842 by(fastforce) 843 844(* basically clagged directly from lookup_ipc_buffer_has_auth *) 845lemma lookup_ipc_buffer_has_read_auth: 846 "\<lbrace>pas_refined aag and valid_objs\<rbrace> 847 lookup_ipc_buffer is_receiver thread 848 \<lbrace>\<lambda>rv s. ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) rv\<rbrace>" 849 apply (rule hoare_pre) 850 apply (simp add: lookup_ipc_buffer_def) 851 apply (wp get_cap_wp thread_get_wp' 852 | wpc)+ 853 apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_read_auth_def get_tcb_ko_at [symmetric]) 854 apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"]) 855 apply (simp add: dom_tcb_cap_cases) 856 apply (frule (1) caps_of_state_valid_cap) 857 apply (clarsimp simp: vm_read_only_def vm_read_write_def) 858 apply (rule_tac Q="AllowRead \<in> xc" in conj_imp) 859 apply (clarsimp simp: valid_cap_simps cap_aligned_def) 860 apply (rule conjI) 861 apply (erule aligned_add_aligned) 862 apply (rule is_aligned_andI1) 863 apply (drule (1) valid_tcb_objs) 864 apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def 865 split: if_splits) 866 apply (rule order_trans [OF _ pbfs_atleast_pageBits]) 867 apply (simp add: msg_align_bits pageBits_def) 868 apply (drule (1) cap_auth_caps_of_state) 869 apply (clarsimp simp: aag_cap_auth_def cap_auth_conferred_def vspace_cap_rights_to_auth_def vm_read_only_def) 870 apply (drule bspec) 871 apply (erule (3) ipcframe_subset_page) 872 apply (clarsimp split: if_split_asm simp: vspace_cap_rights_to_auth_def is_page_cap_def) 873 apply(simp_all) 874 done 875 876 877definition 878 aag_can_read_or_affect_ipc_buffer :: "'a PAS \<Rightarrow> 'a \<Rightarrow> word32 option \<Rightarrow> bool" 879where 880"aag_can_read_or_affect_ipc_buffer aag l \<equiv> 881 case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits \<and> (\<forall>x \<in> ptr_range buf' msg_align_bits. aag_can_read aag x \<or> aag_can_affect aag l x))" 882 883 884lemma lookup_ipc_buffer_aag_can_read_or_affect: 885 "\<lbrace>pas_refined aag and valid_objs and K (aag_can_read aag thread \<or> aag_can_affect aag l thread)\<rbrace> 886 lookup_ipc_buffer is_receiver thread 887 \<lbrace>\<lambda>rv s. aag_can_read_or_affect_ipc_buffer aag l rv\<rbrace>" 888 apply(rule hoare_gen_asm) 889 apply(rule hoare_strengthen_post[OF lookup_ipc_buffer_has_read_auth]) 890 apply(auto simp: ipc_buffer_has_read_auth_def aag_can_read_or_affect_ipc_buffer_def intro: reads_read_thread_read_pages simp: aag_can_affect_label_def split: option.splits) 891 done 892 893lemma cptrs_in_ipc_buffer: 894 "\<lbrakk>x \<in> set [buffer_cptr_index..< 895 buffer_cptr_index + unat (mi_extra_caps mi)]; 896 is_aligned a msg_align_bits; 897 buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - 2)\<rbrakk> 898 \<Longrightarrow> 899 ptr_range (a + of_nat x * of_nat word_size) 2 \<subseteq> 900 ptr_range (a :: word32) msg_align_bits" 901 apply(rule ptr_range_subset) 902 apply assumption 903 apply(simp add: msg_align_bits) 904 apply(simp add: msg_align_bits word_bits_def) 905 apply(simp add: word_size_def) 906 apply(subst upto_enum_step_shift_red[where us=2, simplified]) 907 apply (simp add: msg_align_bits word_bits_def)+ 908 done 909 910lemma for_each_byte_of_word_def2: 911 "for_each_byte_of_word P ptr \<equiv> (\<forall> x\<in>ptr_range ptr 2. P x)" 912 apply(simp add: for_each_byte_of_word_def ptr_range_def add.commute) 913 done 914 915lemma aag_has_auth_to_read_cptrs: 916 "\<lbrakk>x \<in> set [buffer_cptr_index..< 917 buffer_cptr_index + unat (mi_extra_caps mi)]; 918 ipc_buffer_has_read_auth aag (pasSubject aag) (Some a); 919 buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - 2)\<rbrakk> 920 \<Longrightarrow> 921 for_each_byte_of_word (\<lambda> y. aag_can_read aag y) 922 (a + of_nat x * of_nat word_size)" 923 apply(simp add: for_each_byte_of_word_def2 ipc_buffer_has_read_auth_def) 924 apply(rule ballI) 925 apply(rule reads_read) 926 apply(clarify) 927 apply(erule bspec) 928 apply(rule subsetD[OF cptrs_in_ipc_buffer]) 929 apply fastforce 930 apply assumption 931 apply assumption 932 apply assumption 933 done 934 935lemma get_extra_cptrs_rev: 936 "reads_equiv_valid_inv A aag (K (ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and> (buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - 2)))) 937 (get_extra_cptrs buffer mi)" 938 unfolding get_extra_cptrs_def 939 apply (rule gen_asm_ev) 940 apply clarsimp 941 apply(case_tac buffer, simp_all add: return_ev_pre) 942 apply (wp mapM_ev equiv_valid_guard_imp[OF load_word_offs_rev] 943 | erule (2) aag_has_auth_to_read_cptrs)+ 944 done 945 946lemma lookup_extra_caps_rev: 947 shows "reads_equiv_valid_inv A aag (pas_refined aag and (K (is_subject aag thread)) and (\<lambda> s. ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and> buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - 2))) 948 (lookup_extra_caps thread buffer mi)" 949 apply(rule gen_asm_ev) 950 unfolding lookup_extra_caps_def fun_app_def 951 apply (wp mapME_ev cap_fault_on_failure_rev lookup_cap_and_slot_rev 952 get_extra_cptrs_rev) 953 apply simp 954 done 955 956lemmas lookup_extra_caps_reads_respects_g = reads_respects_g_from_inv[OF lookup_extra_caps_rev lookup_extra_caps_inv] 957 958lemma msg_in_ipc_buffer: 959 "\<lbrakk>x = msg_max_length \<or> x < msg_max_length; 960 unat (mi_length mi) < 2 ^ (msg_align_bits - 2); 961 is_aligned a msg_align_bits\<rbrakk> 962 \<Longrightarrow> 963 ptr_range (a + of_nat x * of_nat word_size) 2 \<subseteq> 964 ptr_range (a::word32) msg_align_bits" 965 apply(rule ptr_range_subset) 966 apply assumption 967 apply(simp add: msg_align_bits) 968 apply(simp add: msg_align_bits word_bits_def) 969 apply(simp add: word_size_def) 970 apply(subst upto_enum_step_shift_red[where us=2, simplified]) 971 apply (simp add: msg_align_bits word_bits_def)+ 972 apply(simp add: image_def) 973 apply(rule_tac x=x in bexI) 974 apply(rule refl) 975 apply(auto simp: msg_max_length_def) 976 done 977 978 979lemma aag_has_auth_to_read_msg: 980 "\<lbrakk>x = msg_max_length \<or> x < msg_max_length; 981 ipc_buffer_has_read_auth aag (pasSubject aag) (Some a); 982 unat (mi_length mi) < 2 ^ (msg_align_bits - 2)\<rbrakk> 983 \<Longrightarrow> 984 for_each_byte_of_word (aag_can_read aag) 985 (a + of_nat x * of_nat word_size)" 986 apply(simp add: for_each_byte_of_word_def2 ipc_buffer_has_read_auth_def) 987 apply(rule ballI) 988 apply(rule reads_read) 989 apply(clarify) 990 apply(erule bspec) 991 apply(rule subsetD[OF msg_in_ipc_buffer[where x=x]]) 992 apply assumption 993 apply assumption 994 apply assumption 995 apply assumption 996 done 997 998(* only called within do_reply_transfer for which access assumes sender 999 and receiver in same domain *) 1000lemma get_mrs_rev: 1001 shows "reads_equiv_valid_inv A aag ((K (is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf \<and> unat (mi_length mi) < 2 ^ (msg_align_bits - 2)))) (get_mrs thread buf mi)" 1002 apply (rule gen_asm_ev) 1003 unfolding get_mrs_def 1004 apply (wp mapM_ev'' load_word_offs_rev thread_get_rev 1005 | wpc 1006 | rule aag_has_auth_to_read_msg[where mi=mi] 1007 | clarsimp split: if_split_asm)+ 1008 done 1009 1010lemmas get_mrs_reads_respects_g = reads_respects_g_from_inv[OF get_mrs_rev get_mrs_inv] 1011 1012 1013 1014lemma setup_caller_cap_reads_respects: 1015 "reads_respects aag l (K (is_subject aag sender \<and> is_subject aag receiver)) 1016 (setup_caller_cap sender receiver)" 1017 unfolding setup_caller_cap_def 1018 apply(wp cap_insert_reads_respects set_thread_state_owned_reads_respects | simp)+ 1019 done 1020 1021 1022lemma const_on_failure_ev: 1023 "equiv_valid_inv I A P m \<Longrightarrow> 1024 equiv_valid_inv I A P (const_on_failure c m)" 1025 unfolding const_on_failure_def catch_def 1026 apply(wp | wpc | simp)+ 1027 done 1028 1029 1030lemma set_extra_badge_reads_respects: 1031 "reads_respects aag l \<top> (set_extra_badge buffer badge n)" 1032 unfolding set_extra_badge_def 1033 by (rule store_word_offs_reads_respects) 1034 1035lemma reads_equiv_cdt_has_children: 1036 "\<lbrakk>pas_refined aag s; pas_refined aag s'; is_subject aag (fst slot); 1037 equiv_for (aag_can_read aag \<circ> fst) cdt s s'\<rbrakk> \<Longrightarrow> 1038 (\<exists> c. (cdt s) c = Some slot) = (\<exists> c. (cdt s') c = Some slot)" 1039 apply(rule iffI) 1040 apply(erule exE) 1041 apply(frule (2) aag_owned_cdt_link) 1042 apply(fastforce elim: equiv_forE dest: aag_can_read_self) 1043 apply(erule exE) 1044 apply(drule (2) aag_owned_cdt_link[rotated]) 1045 apply(erule equiv_forE) 1046 apply(drule_tac x=c in meta_spec) 1047 apply(fastforce dest: aag_can_read_self) 1048 done 1049 1050lemma ensure_no_children_rev: 1051 "reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag (fst slot))) 1052 (ensure_no_children slot)" 1053 unfolding ensure_no_children_def fun_app_def equiv_valid_def2 1054 apply(rule equiv_valid_rv_guard_imp) 1055 apply(rule_tac Q="\<lambda> rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s" in equiv_valid_rv_liftE_bindE[OF equiv_valid_rv_guard_imp[OF gets_cdt_revrv']]) 1056 apply(rule TrueI) 1057 apply(clarsimp simp: equiv_valid_2_def) 1058 apply(drule reads_equiv_cdt_has_children) 1059 apply assumption 1060 apply assumption 1061 apply(fastforce elim: reads_equivE) 1062 apply(fastforce simp: in_whenE in_throwError) 1063 apply(wp ,simp) 1064 done 1065 1066lemma arch_derive_cap_reads_respects: 1067 "reads_respects aag l \<top> (arch_derive_cap cap)" 1068 unfolding arch_derive_cap_def 1069 apply(rule equiv_valid_guard_imp) 1070 apply(wp | wpc)+ 1071 apply(simp) 1072 done 1073 1074lemma derive_cap_rev': 1075 "reads_equiv_valid_inv A aag (\<lambda> s. (\<exists>x xa xb d. cap = cap.UntypedCap d x xa xb) \<longrightarrow> 1076 pas_refined aag s \<and> is_subject aag (fst slot)) (derive_cap slot cap)" 1077 unfolding derive_cap_def arch_derive_cap_def 1078 apply(rule equiv_valid_guard_imp) 1079 apply(wp ensure_no_children_rev | wpc | simp)+ 1080 done 1081 1082lemma derive_cap_rev: 1083 "reads_equiv_valid_inv A aag (\<lambda> s. pas_refined aag s \<and> is_subject aag (fst slot)) (derive_cap slot cap)" 1084 by(blast intro: equiv_valid_guard_imp[OF derive_cap_rev']) 1085 1086 1087lemma transfer_caps_loop_reads_respects: 1088 "reads_respects aag l 1089 (pas_refined aag and 1090 K ((\<forall>cap\<in>set caps. is_subject aag (fst (snd cap)) \<and> 1091 pas_cap_cur_auth aag (fst cap)) \<and> 1092 (\<forall>slot\<in>set slots. is_subject aag (fst slot)))) 1093 (transfer_caps_loop ep rcv_buffer n caps slots mi)" 1094 apply(induct caps arbitrary: slots n mi) 1095 apply simp 1096 apply(rule return_ev_pre) 1097 apply(case_tac a) 1098 apply(simp split del: if_split) 1099 apply(rule equiv_valid_guard_imp) 1100 apply(wp const_on_failure_ev 1101 | simp | intro conjI impI)+ 1102 apply fast 1103 apply(wp set_extra_badge_reads_respects | simp)+ 1104 apply fast 1105 apply(wp cap_insert_reads_respects cap_insert_pas_refined whenE_throwError_wp derive_cap_rev derive_cap_cap_cur_auth | simp split del: if_split | wp_once hoare_drop_imps)+ 1106 apply(clarsimp simp: remove_rights_cur_auth) 1107 apply(fastforce dest: subsetD[OF set_tl_subset]) 1108 done 1109 1110lemma empty_on_failure_ev: 1111 "equiv_valid_inv I A P m \<Longrightarrow> 1112 equiv_valid_inv I A P (empty_on_failure m)" 1113 unfolding empty_on_failure_def catch_def 1114 apply(wp | wpc | simp)+ 1115 done 1116 1117lemma unify_failure_ev: 1118 "equiv_valid_inv I A P m \<Longrightarrow> 1119 equiv_valid_inv I A P (unify_failure m)" 1120 unfolding unify_failure_def handleE'_def 1121 apply(wp | wpc | simp)+ 1122 done 1123 1124lemma lookup_slot_for_cnode_op_rev: 1125 "reads_equiv_valid_inv A aag (\<lambda>s. ((depth \<noteq> 0 \<and> depth \<le> word_bits) \<longrightarrow> (pas_refined aag s \<and> (is_cnode_cap croot \<longrightarrow> is_subject aag (obj_ref_of croot))))) (lookup_slot_for_cnode_op is_source croot ptr depth)" 1126 unfolding lookup_slot_for_cnode_op_def 1127 apply (clarsimp split del: if_split) 1128 apply (wp resolve_address_bits_rev lookup_error_on_failure_rev 1129 whenE_throwError_wp 1130 | wpc 1131 | rule hoare_post_imp_R[OF hoare_True_E_R[where P="\<top>"]] 1132 | simp add: split_def split del: if_split)+ 1133 done 1134 1135lemma lookup_slot_for_cnode_op_reads_respects: 1136 "reads_respects aag l (pas_refined aag and K (is_subject aag (obj_ref_of croot))) (lookup_slot_for_cnode_op is_source croot ptr depth)" 1137 apply(rule equiv_valid_guard_imp[OF lookup_slot_for_cnode_op_rev]) 1138 by simp 1139 1140lemma lookup_cap_rev: 1141 "reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread)) (lookup_cap thread ref)" 1142 unfolding lookup_cap_def split_def fun_app_def 1143 apply(wp lookup_slot_for_thread_rev get_cap_rev | simp)+ 1144 apply(rule lookup_slot_for_thread_authorised) 1145 apply(simp) 1146 done 1147 1148lemma captransfer_indices_in_range: 1149 "x \<in> {0..2} \<Longrightarrow> 1150 ((2::word32) + (of_nat msg_max_length + of_nat msg_max_extra_caps)) * word_size + (x * word_size) \<le> 2 ^ msg_align_bits - 1" 1151 apply(rule order_trans) 1152 prefer 2 1153 apply(rule word_less_sub_1) 1154 apply(rule_tac p=127 in mul_word_size_lt_msg_align_bits_ofnat) 1155 apply(simp add: msg_align_bits) 1156 apply(rule_tac y="0x7F * word_size" in order_trans) 1157 apply(clarsimp simp: msg_max_length_def msg_max_extra_caps_def word_size_def) 1158 apply(drule_tac k=4 in word_mult_le_mono1) 1159 apply simp 1160 apply simp 1161 apply(drule_tac x="0x1F4" in word_plus_mono_right) 1162 apply simp 1163 apply simp 1164 apply (simp add: word_size_def) 1165 done 1166 1167 1168lemma word_plus_power_2_offset_le: 1169 "\<lbrakk>is_aligned (p :: 'a :: len word) n; is_aligned q m; p < q; n \<le> m; n < len_of TYPE('a)\<rbrakk> \<Longrightarrow> p + (2^n) \<le> q" 1170 apply(drule is_aligned_weaken, assumption) 1171 apply(clarsimp simp: is_aligned_def) 1172 apply(elim dvdE) 1173 apply(rename_tac k ka) 1174 apply(rule_tac ua=0 and n="int k" and n'="int ka" in udvd_incr') 1175 apply assumption 1176 apply(clarsimp simp: uint_nat)+ 1177 done 1178 1179 1180lemma is_aligned_mult_word_size: 1181 "is_aligned (p * word_size) 2" 1182 apply(rule_tac k=p in is_alignedI) 1183 apply(fastforce simp: word_size_def) 1184 done 1185 1186 1187lemma captransfer_in_ipc_buffer: 1188 "\<lbrakk>is_aligned (buffer :: word32) msg_align_bits; 1189 x \<in> {0..2}\<rbrakk> \<Longrightarrow> 1190 ptr_range (buffer + (2 + (of_nat msg_max_length + of_nat msg_max_extra_caps)) * 1191 word_size + x * word_size) 2 \<subseteq> ptr_range buffer msg_align_bits" 1192 apply(rule ptr_range_subset) 1193 apply assumption 1194 apply(simp add: msg_align_bits) 1195 apply(simp add: msg_align_bits word_bits_def) 1196 apply(simp add: word_size_def) 1197 apply(subst upto_enum_step_shift_red[where us=2, simplified]) 1198 apply (simp add: msg_align_bits word_bits_def)+ 1199 apply(simp add: image_def msg_max_length_def msg_max_extra_caps_def) 1200 apply(rule_tac x="(125::nat) + unat x" in bexI) 1201 apply simp+ 1202 apply(fastforce intro: unat_less_helper minus_one_helper5) 1203 done 1204 1205lemma aag_has_auth_to_read_captransfer: 1206 "\<lbrakk>ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer); 1207 x \<in> {0..2}\<rbrakk> \<Longrightarrow> 1208 for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (of_nat msg_max_length + of_nat msg_max_extra_caps)) * 1209 word_size + x * word_size)" 1210 apply(simp add: for_each_byte_of_word_def2 ipc_buffer_has_read_auth_def) 1211 apply(rule ballI) 1212 apply(rule reads_read) 1213 apply(clarify) 1214 apply(erule bspec) 1215 apply(rule subsetD[OF captransfer_in_ipc_buffer]) 1216 apply fastforce+ 1217 done 1218 1219lemma load_cap_transfer_rev: 1220 "reads_equiv_valid_inv A aag (K (ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer))) 1221 (load_cap_transfer buffer)" 1222 unfolding load_cap_transfer_def fun_app_def captransfer_from_words_def 1223 apply(wp dmo_loadWord_rev | simp)+ 1224 apply safe 1225 apply(erule aag_has_auth_to_read_captransfer[where x=0, simplified]) 1226 apply(erule aag_has_auth_to_read_captransfer[where x=1, simplified]) 1227 apply(erule aag_has_auth_to_read_captransfer[where x=2, simplified]) 1228 done 1229 1230 1231lemma get_endpoint_rev: 1232 "reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (get_endpoint ptr)" 1233 unfolding get_simple_ko_def 1234 apply(wp get_object_rev | wpc | simp)+ 1235 done 1236 1237lemma send_endpoint_threads_blocked: 1238"\<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; 1239 ko_at (Endpoint (SendEP list)) ep s; x\<in>set list\<rbrakk> \<Longrightarrow> 1240 st_tcb_at (send_blocked_on ep) x s" 1241 apply (rule ep_queued_st_tcb_at'') 1242 apply simp+ 1243 done 1244 1245lemma send_blocked_threads_have_SyncSend_auth: 1246 "\<lbrakk>pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); 1247 st_tcb_at (send_blocked_on ep) x s\<rbrakk> \<Longrightarrow> 1248 (pasObjectAbs aag x,SyncSend,pasObjectAbs aag ep) \<in> pasPolicy aag" 1249 apply(drule_tac auth="SyncSend" and x=x in pas_refined_mem[rotated]) 1250 apply(rule sta_ts) 1251 apply(clarsimp simp: thread_states_def split: option.split simp: tcb_states_of_state_def st_tcb_def2) 1252 apply(case_tac "tcb_state tcb", simp_all) 1253 done 1254 1255 1256(*MOVE*) 1257lemma ev_invisible: 1258 assumes domains_distinct: "pas_domains_distinct aag" 1259 shows 1260 "\<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f; \<forall>s t. P s \<and> P t \<longrightarrow> (\<forall>(rva, s') \<in> fst (f s). \<forall>(rvb, t') \<in> fst(f t). W rva rvb)\<rbrakk> \<Longrightarrow> 1261 equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) W (P and Q) (P and Q) f f" 1262 apply (rule ev2_invisible[OF domains_distinct]) 1263 apply simp+ 1264 done 1265 1266 1267lemma get_thread_state_reads_respects: 1268 "reads_respects aag l (\<lambda> s. aag_can_read aag thread \<or> aag_can_affect aag l thread) (get_thread_state thread)" 1269 unfolding get_thread_state_def 1270 apply(rule equiv_valid_guard_imp) 1271 apply(wp thread_get_reads_respects | simp)+ 1272 done 1273 1274lemma send_endpoint_reads_affects_queued: 1275 "\<lbrakk>(pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; 1276 auth \<in> {Receive,Reset}; 1277 aag_can_read_label aag (pasObjectAbs aag epptr) \<or> 1278 aag_can_affect aag l epptr; 1279 pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); 1280 ko_at (Endpoint (SendEP list)) epptr s; ep = SendEP list; 1281 x \<in> set list\<rbrakk> 1282 \<Longrightarrow> 1283 aag_can_read_label aag (pasObjectAbs aag x) \<or> 1284 aag_can_affect aag l x" 1285 apply(frule send_endpoint_threads_blocked, (simp | assumption)+) 1286 apply(drule send_blocked_threads_have_SyncSend_auth, (simp | assumption)+) 1287 apply(auto dest: read_sync_ep_read_senders) 1288 done 1289 1290(* 1291lemma cancel_badged_sends_equiv_but_for_labels: 1292 "\<lbrace> pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and 1293 equiv_but_for_labels aag L st and 1294 K ({pasObjectAbs aag epptr} \<union> all_with_auth_to aag SyncSend (pasObjectAbs aag epptr) \<subseteq> L) \<rbrace> 1295 cancel_badged_sends epptr badge 1296 \<lbrace> \<lambda>_. equiv_but_for_labels aag L st \<rbrace>" 1297 unfolding cancel_badged_sends_def 1298 apply(wp set_endpoint_equiv_but_for_labels | wpc | simp)+ 1299 apply(rule_tac Q="\<lambda> r s. equiv_but_for_labels aag L st s \<and> 1300 {pasObjectAbs aag epptr} \<union> all_with_auth_to aag SyncSend (pasObjectAbs aag epptr) \<subseteq> L \<and> (\<forall>x\<in>set list. (pasObjectAbs aag x, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)" in hoare_strengthen_post) 1301 apply(wp mapM_wp' set_thread_state_equiv_but_for_labels gts_wp | simp add: filterM_mapM)+ 1302 apply(fastforce simp: all_with_auth_to_def) 1303 apply simp 1304 apply(wp set_endpoint_equiv_but_for_labels get_simple_ko_wp | simp)+ 1305 apply clarsimp 1306 apply(frule send_endpoint_threads_blocked, (simp | assumption)+) 1307 apply(drule send_blocked_threads_have_SyncSend_auth, (simp | assumption)+) 1308 done 1309*) 1310 1311(* 1312lemma cancel_badged_sends_reads_respects: 1313 shows 1314 "reads_respects aag l (pas_refined aag and valid_objs and (sym_refs \<circ> state_refs_of) and K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (cancel_badged_sends epptr badge)" 1315 apply (rule gen_asm_ev)+ 1316 apply(case_tac "aag_can_read aag epptr \<or> aag_can_affect aag l epptr") 1317 apply(simp add: cancel_badged_sends_def fun_app_def) 1318 apply wp 1319 apply (rule_tac Q="\<lambda>s. 1320 (case rv of SendEP list \<Rightarrow> \<forall>x\<in>set list. aag_can_read aag x \<or> aag_can_affect aag l x | _ \<Rightarrow> True)" in equiv_valid_guard_imp) 1321 apply (case_tac rv) 1322 apply ((wp mapM_ev'' get_thread_state_reads_respects set_thread_state_reads_respects set_simple_ko_reads_respects get_simple_ko_reads_respects hoare_vcg_ball_lift | wpc | simp add: filterM_mapM tcb_at_st_tcb_at[symmetric])+) 1323 apply (wp get_simple_ko_wp) 1324 apply (intro impI allI conjI) 1325 apply simp 1326 apply (case_tac ep,simp_all) 1327 apply (elim conjE, rule ballI) 1328 apply (rule send_endpoint_reads_affects_queued, (simp | assumption)+) 1329 apply(simp add: equiv_valid_def2) 1330 apply(rule equiv_valid_rv_guard_imp) 1331 apply(rule_tac Q="pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of" and L="{pasObjectAbs aag epptr} \<union> all_with_auth_to aag SyncSend (pasObjectAbs aag epptr)" in ev_invisible) 1332 apply(auto dest: reads_read_queued_thread_read_ep simp: labels_are_invisible_def aag_can_affect_label_def all_with_auth_to_def)[1] 1333 apply(rule modifies_at_mostI) 1334 apply(wp cancel_badged_sends_equiv_but_for_labels | simp)+ 1335 done 1336*) 1337 1338lemma mapM_ev''': 1339 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (Q and P x) (m x)" 1340 assumes inv: "\<And> x. x \<in> set lst \<Longrightarrow> invariant (m x) (\<lambda> s. Q s \<and> (\<forall>x\<in>set lst. P x s))" 1341 shows "equiv_valid_inv D A (\<lambda> s. Q s \<and> (\<forall>x\<in>set lst. P x s)) (mapM m lst)" 1342 apply(rule mapM_ev) 1343 apply(rule equiv_valid_guard_imp[OF reads_res], simp+) 1344 apply(wpsimp wp: inv) 1345 done 1346 1347lemma cancel_badged_sends_reads_respects: 1348 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1349 notes gts_st_tcb_at[wp del] 1350 shows 1351 "reads_respects aag l (pas_refined aag and valid_objs and (sym_refs \<circ> state_refs_of) and (\<lambda>s. is_subject aag (cur_thread s)) and K (is_subject aag epptr)) (cancel_badged_sends epptr badge)" 1352 apply (rule gen_asm_ev)+ 1353 apply(simp add: cancel_badged_sends_def fun_app_def) 1354 apply wp 1355 apply ((wp mapM_ev'' mapM_wp get_thread_state_reads_respects set_thread_state_runnable_reads_respects 1356 set_simple_ko_reads_respects get_simple_ko_reads_respects hoare_vcg_ball_lift 1357 tcb_sched_action_reads_respects set_thread_state_pas_refined 1358 | wpc | simp add: filterM_mapM tcb_at_st_tcb_at[symmetric] | wp_once hoare_drop_imps | rule subset_refl | force)+)[1] 1359 apply (wp get_simple_ko_reads_respects) 1360 apply (wp get_simple_ko_wp) 1361 apply simp 1362 apply (intro conjI allI impI ballI, elim conjE) 1363 apply (rule send_endpoint_reads_affects_queued[where epptr = epptr]) 1364 apply (force simp: pas_refined_def policy_wellformed_def | assumption)+ 1365 done 1366 1367lemma get_cap_ret_is_subject': 1368 "\<lbrace>pas_refined aag and K (is_subject aag (fst ptr))\<rbrace> get_cap ptr 1369 \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> (\<forall>x\<in>Access.obj_refs rv. is_subject aag x)\<rbrace>" 1370 apply(rule hoare_strengthen_post[OF get_cap_ret_is_subject]) 1371 apply(clarsimp simp: is_cap_simps) 1372 done 1373 1374 1375lemma get_receive_slots_rev: 1376 "reads_equiv_valid_inv A aag (pas_refined aag and (K (is_subject aag thread \<and> 1377 ipc_buffer_has_read_auth aag (pasSubject aag) buf))) 1378 (get_receive_slots thread buf)" 1379 apply(case_tac buf) 1380 apply(fastforce intro: return_ev_pre) 1381 apply(simp add: lookup_cap_def split_def 1382 | wp empty_on_failure_ev unify_failure_ev lookup_slot_for_cnode_op_rev get_cap_rev 1383 lookup_slot_for_thread_rev lookup_slot_for_thread_authorised 1384 get_cap_ret_is_subject get_cap_ret_is_subject' load_cap_transfer_rev 1385 | wp_once hoare_drop_imps)+ 1386 done 1387 1388lemma transfer_caps_reads_respects: 1389 "reads_respects aag l (pas_refined aag 1390 and K (is_subject aag receiver \<and> 1391 ipc_buffer_has_read_auth aag (pasSubject aag) receive_buffer \<and> 1392 (\<forall>cap\<in>set caps. 1393 is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap)))) 1394 (transfer_caps mi caps endpoint receiver receive_buffer)" 1395 unfolding transfer_caps_def fun_app_def 1396 apply(wp transfer_caps_loop_reads_respects get_receive_slots_rev get_receive_slots_authorised 1397 hoare_vcg_all_lift static_imp_wp 1398 | wpc | simp)+ 1399 done 1400 1401lemma mrs_in_ipc_buffer: 1402 "\<lbrakk>is_aligned (buf :: word32) msg_align_bits; 1403 x \<in> set [length msg_registers + 1..<Suc n]; 1404 n < 2 ^ (msg_align_bits - 2)\<rbrakk> 1405 \<Longrightarrow> ptr_range 1406 (buf + of_nat x * of_nat word_size) 2 \<subseteq> ptr_range buf msg_align_bits" 1407 apply(rule ptr_range_subset) 1408 apply assumption 1409 apply(simp add: msg_align_bits) 1410 apply(simp add: msg_align_bits word_bits_def) 1411 apply(simp add: word_size_def) 1412 apply(subst upto_enum_step_shift_red[where us=2, simplified]) 1413 apply (simp add: msg_align_bits word_bits_def)+ 1414 apply(simp add: image_def) 1415 apply(rule_tac x=x in bexI) 1416 apply(rule refl) 1417 apply (fastforce split: if_split_asm) 1418 done 1419 1420lemma aag_has_auth_to_read_mrs: 1421 "\<lbrakk>aag_can_read_or_affect_ipc_buffer aag l (Some buf); 1422 x \<in> set [length msg_registers + 1..<Suc n]; 1423 n < 2 ^ (msg_align_bits - 2)\<rbrakk> 1424 \<Longrightarrow> for_each_byte_of_word (\<lambda>x. aag_can_read_label aag (pasObjectAbs aag x) \<or> aag_can_affect aag l x) 1425 (buf + of_nat x * of_nat word_size)" 1426 apply(simp add: for_each_byte_of_word_def2 aag_can_read_or_affect_ipc_buffer_def) 1427 apply(rule ballI) 1428 apply(erule conjE) 1429 apply(erule bspec) 1430 apply(rule subsetD[OF mrs_in_ipc_buffer[where x=x and n=n]]) 1431 apply assumption 1432 apply (clarsimp split: if_splits) 1433 apply assumption 1434 apply assumption 1435 done 1436 1437 1438abbreviation aag_can_read_or_affect where 1439 "aag_can_read_or_affect aag l x \<equiv> 1440 aag_can_read aag x \<or> aag_can_affect aag l x" 1441 1442lemma dmo_loadWord_reads_respects: 1443 "reads_respects aag l (K (for_each_byte_of_word (\<lambda> x. aag_can_read_or_affect aag l x) p)) 1444 (do_machine_op (loadWord p))" 1445 apply(rule gen_asm_ev) 1446 apply(rule use_spec_ev) 1447 apply(rule spec_equiv_valid_hoist_guard) 1448 1449 apply(rule do_machine_op_spec_reads_respects) 1450 apply(simp add: loadWord_def equiv_valid_def2 spec_equiv_valid_def) 1451 apply(rule_tac R'="\<lambda> rv rv'. for_each_byte_of_word (\<lambda> y. rv y = rv' y) p" and Q="\<top>\<top>" and Q'="\<top>\<top>" and P="\<top>" and P'="\<top>" in equiv_valid_2_bind_pre) 1452 apply(rule_tac R'="(=)" and Q="\<lambda> r s. p && mask 2 = 0" and Q'="\<lambda> r s. p && mask 2 = 0" and P="\<top>" and P'="\<top>" in equiv_valid_2_bind_pre) 1453 apply(rule return_ev2) 1454 apply(rule_tac f="word_rcat" in arg_cong) 1455 apply(fastforce intro: is_aligned_no_wrap' word_plus_mono_right simp: is_aligned_mask for_each_byte_of_word_def) (* slow *) 1456 apply(rule assert_ev2[OF refl]) 1457 apply(rule assert_wp)+ 1458 apply simp+ 1459 apply(clarsimp simp: equiv_valid_2_def in_monad for_each_byte_of_word_def) 1460 apply(fastforce elim: equiv_forD orthD1 simp: ptr_range_def add.commute) 1461 apply (wp wp_post_taut loadWord_inv | simp)+ 1462 done 1463 1464lemma load_word_offs_reads_respects: 1465 "reads_respects aag l (\<lambda> s. for_each_byte_of_word (\<lambda> x. aag_can_read_or_affect aag l x) (a + of_nat x * of_nat word_size)) (load_word_offs a x)" 1466 unfolding load_word_offs_def fun_app_def 1467 apply(rule equiv_valid_guard_imp[OF dmo_loadWord_reads_respects]) 1468 apply(clarsimp) 1469 done 1470 1471lemma as_user_reads_respects: 1472 "reads_respects aag l (K (det f \<and> aag_can_read_or_affect aag l thread)) (as_user thread f)" 1473 apply (simp add: as_user_def fun_app_def split_def) 1474 apply (rule gen_asm_ev) 1475 apply (wp set_object_reads_respects select_f_ev gets_the_ev) 1476 apply (auto intro: reads_affects_equiv_get_tcb_eq[where aag=aag]) 1477 done 1478 1479lemma copy_mrs_reads_respects: 1480 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1481 shows 1482 "reads_respects aag l (K (aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect_ipc_buffer aag l sbuf \<and> unat n < 2 ^ (msg_align_bits - 2))) (copy_mrs sender sbuf receiver rbuf n)" 1483 unfolding copy_mrs_def fun_app_def 1484 apply(rule gen_asm_ev) 1485 apply(wp mapM_ev'' store_word_offs_reads_respects 1486 load_word_offs_reads_respects as_user_set_register_reads_respects' 1487 as_user_reads_respects 1488 | wpc 1489 | simp add: det_setRegister det_getRegister split del: if_split)+ 1490 apply clarsimp 1491 apply(rename_tac n') 1492 apply(subgoal_tac " ptr_range (x + of_nat n' * of_nat word_size) 2 1493 \<subseteq> ptr_range x msg_align_bits") 1494 apply(simp add: for_each_byte_of_word_def2) 1495 apply(simp add: aag_can_read_or_affect_ipc_buffer_def) 1496 apply(erule conjE) 1497 apply(rule ballI) 1498 apply(erule bspec) 1499 apply(erule (1) subsetD[rotated]) 1500 apply(rule ptr_range_subset) 1501 apply(simp add: aag_can_read_or_affect_ipc_buffer_def) 1502 apply(simp add: msg_align_bits) 1503 apply(simp add: msg_align_bits word_bits_def) 1504 apply(simp add: word_size_def) 1505 apply(subst upto_enum_step_shift_red[where us=2, simplified]) 1506 apply (simp add: msg_align_bits word_bits_def aag_can_read_or_affect_ipc_buffer_def )+ 1507 apply(fastforce simp: image_def) 1508 done 1509 1510lemma get_mi_length': 1511 "\<lbrace>\<top>\<rbrace> get_message_info sender 1512 \<lbrace>\<lambda>rv s. buffer_cptr_index + unat (mi_extra_caps rv) 1513 < 2 ^ (msg_align_bits - 2)\<rbrace>" 1514 apply(rule hoare_post_imp[OF _ get_mi_valid']) 1515 apply(clarsimp simp: valid_message_info_def msg_align_bits msg_max_length_def word_le_nat_alt buffer_cptr_index_def msg_max_extra_caps_def) 1516 done 1517 1518lemma validE_E_wp_post_taut: 1519 "\<lbrace> P \<rbrace> f -, \<lbrace>\<lambda> r s. True \<rbrace>" 1520 by(auto simp: validE_E_def validE_def valid_def) 1521 1522lemma aag_has_read_auth_can_read_or_affect_ipc_buffer: 1523 "ipc_buffer_has_read_auth aag (pasSubject aag) buf \<Longrightarrow> 1524 aag_can_read_or_affect_ipc_buffer aag l buf" 1525 apply(clarsimp simp: ipc_buffer_has_read_auth_def 1526 aag_can_read_or_affect_ipc_buffer_def 1527 split: option.splits) 1528 apply(rule reads_read) 1529 apply blast 1530 done 1531 1532lemma ev_irrelevant_bind: 1533 assumes inv: "\<And> P. \<lbrace> P \<rbrace> f \<lbrace>\<lambda>_. P \<rbrace>" 1534 assumes ev: "equiv_valid I A A P g" 1535 shows "equiv_valid I A A P (do y \<leftarrow> f; g od)" 1536 apply(simp add: equiv_valid_def2) 1537 apply(rule equiv_valid_rv_guard_imp) 1538 apply(rule equiv_valid_2_bind) 1539 apply(rule ev[simplified equiv_valid_def2]) 1540 apply(wp equiv_valid_rv_trivial[OF inv] inv | simp)+ 1541 done 1542 1543lemma get_message_info_reads_respects: 1544 "reads_respects aag l (K (aag_can_read_or_affect aag l ptr)) (get_message_info ptr)" 1545 apply (simp add: get_message_info_def) 1546 apply (wp as_user_reads_respects | clarsimp simp: getRegister_def)+ 1547 done 1548 1549lemma do_normal_transfer_reads_respects: 1550 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1551 shows 1552 "reads_respects aag l (pas_refined aag and 1553 K (aag_can_read_or_affect aag l sender \<and> 1554 ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> 1555 ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> 1556 (grant \<longrightarrow> (is_subject aag sender \<and> is_subject aag receiver)))) 1557 (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf)" 1558 apply(case_tac grant) 1559 apply(rule gen_asm_ev) 1560 apply(simp add: do_normal_transfer_def) 1561 apply(wp get_message_info_rev lookup_extra_caps_rev 1562 as_user_set_register_reads_respects' set_message_info_reads_respects 1563 transfer_caps_reads_respects copy_mrs_reads_respects 1564 lookup_extra_caps_rev lookup_extra_caps_authorised 1565 lookup_extra_caps_auth get_message_info_rev 1566 get_mi_length' get_mi_length validE_E_wp_post_taut 1567 | wpc 1568 | simp add: det_setRegister ball_conj_distrib)+ 1569 apply (fastforce intro: aag_has_read_auth_can_read_or_affect_ipc_buffer) 1570 apply(rule gen_asm_ev) 1571 apply(simp add: do_normal_transfer_def transfer_caps_def) 1572 apply(subst transfer_caps_loop.simps) 1573 apply(wp ev_irrelevant_bind[where f="get_receive_slots receiver rbuf"] 1574 as_user_set_register_reads_respects' 1575 set_message_info_reads_respects copy_mrs_reads_respects 1576 get_message_info_reads_respects get_mi_length 1577 |wpc 1578 |simp)+ 1579 apply(auto simp: ipc_buffer_has_read_auth_def aag_can_read_or_affect_ipc_buffer_def dest: reads_read_thread_read_pages split: option.splits) 1580 done 1581 1582lemma getRestartPC_det: 1583 "det getRestartPC" 1584 apply (clarsimp simp: getRestartPC_def getRegister_def) 1585 done 1586 1587lemma getRegister_det: 1588 "det (getRegister x)" 1589 by (clarsimp simp: getRegister_def) 1590 1591lemma make_fault_msg_reads_respects: 1592 "reads_respects aag l (K (aag_can_read_or_affect aag l sender)) (make_fault_msg rva sender)" 1593 apply(case_tac rva) 1594 apply (wp as_user_reads_respects 1595 | simp split del: if_split 1596 add: getRestartPC_det getRegister_det 1597 | rule det_mapM 1598 | rule subset_refl)+ 1599 apply (case_tac x4) 1600 apply (wp as_user_reads_respects 1601 | simp split del: if_split 1602 add: getRestartPC_det getRegister_det)+ 1603 done 1604 1605lemma set_mrs_returns_a_constant: 1606 "\<exists> x. \<lbrace> \<top> \<rbrace> set_mrs thread buf msgs \<lbrace> \<lambda> rv s. rv = x \<rbrace>" 1607 apply(case_tac buf) 1608 apply(rule exI) 1609 apply((simp add: set_mrs_def | wp | rule impI)+)[1] 1610 apply(rule exI) 1611 apply((simp add: set_mrs_def split del: if_split | wp | rule impI)+)[1] 1612 done 1613 1614lemma set_mrs_ret_eq: 1615 "\<forall>(s::'a::state_ext state) (t::'a::state_ext state). \<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s). 1616 \<forall>(rvb, t')\<in>fst (set_mrs thread buf msgs t). rva = rvb" 1617 apply(clarsimp) 1618 apply(cut_tac thread=thread and buf=buf and msgs=msgs in set_mrs_returns_a_constant) 1619 apply(erule exE) 1620 apply(subgoal_tac "a = x \<and> aa = x") 1621 apply simp 1622 apply(rule conjI) 1623 apply(erule (1) use_valid | simp)+ 1624 done 1625 1626 1627lemma set_mrs_reads_respects': 1628 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1629 shows 1630 "reads_respects aag l (K (ipc_buffer_has_auth aag thread buf \<and> (case buf of (Some buf') \<Rightarrow> 1631 is_aligned buf' msg_align_bits | _ \<Rightarrow> True))) (set_mrs thread buf msgs)" 1632 apply(case_tac "aag_can_read_or_affect aag l thread") 1633 apply((wp equiv_valid_guard_imp[OF set_mrs_reads_respects] | simp)+)[1] 1634 apply(rule gen_asm_ev) 1635 apply(simp add: equiv_valid_def2) 1636 apply(rule equiv_valid_rv_guard_imp) 1637 apply(case_tac buf) 1638 apply(rule_tac Q="\<top>" and P="\<top>" and L="{pasObjectAbs aag thread}" in ev_invisible[OF domains_distinct]) 1639 apply(clarsimp simp: labels_are_invisible_def) 1640 apply(rule modifies_at_mostI) 1641 apply(simp add: set_mrs_def) 1642 apply((wp set_object_equiv_but_for_labels | simp | auto dest: get_tcb_not_asid_pool_at)+)[1] 1643 apply(simp) 1644 apply(rule set_mrs_ret_eq) 1645 apply(rename_tac buf') 1646 apply(rule_tac Q="\<top>" and L="{pasObjectAbs aag thread} \<union> (pasObjectAbs aag) ` (ptr_range buf' msg_align_bits)" in ev_invisible[OF domains_distinct]) 1647 apply(auto simp: labels_are_invisible_def ipc_buffer_has_auth_def dest: reads_read_page_read_thread simp: aag_can_affect_label_def)[1] 1648 apply(rule modifies_at_mostI) 1649 apply(wp set_mrs_equiv_but_for_labels | simp)+ 1650 apply(rule set_mrs_ret_eq) 1651 by simp 1652 1653lemma do_fault_transfer_reads_respects: 1654 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1655 shows 1656 "reads_respects aag l (K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_auth aag receiver buf \<and> 1657 (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))) (do_fault_transfer badge sender receiver buf)" 1658 unfolding do_fault_transfer_def 1659 apply (wp as_user_set_register_reads_respects' as_user_reads_respects set_message_info_reads_respects 1660 set_mrs_reads_respects' make_fault_msg_reads_respects thread_get_reads_respects 1661 | wpc 1662 | simp add: split_def det_setRegister 1663 | wp_once hoare_drop_imps)+ 1664 done 1665 1666 1667 1668lemma tl_tl_in_set: 1669 "tl xs = (x # xs') \<Longrightarrow> set xs' \<subseteq> set xs" 1670 apply(case_tac xs, auto) 1671 done 1672 1673(* GENERALIZE the following is possible *) 1674lemma ptr_in_obj_range: 1675 "\<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj\<rbrakk> 1676 \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<in> obj_range ptr obj" 1677 apply (simp add: obj_range_def) 1678 apply (rule context_conjI) 1679 apply (frule(1) pspace_alignedD) 1680 apply (erule is_aligned_no_wrap') 1681 apply (rule and_mask_less') 1682 apply (drule valid_obj_sizes) 1683 apply fastforce 1684 apply (simp add: word_bits_def) 1685 apply (simp add: p_assoc_help) 1686 apply (rule word_plus_mono_right) 1687 apply (rule word_less_sub_1) 1688 apply (drule valid_obj_sizes) 1689 apply fastforce 1690 apply (simp add: word_bits_def and_mask_less') 1691 apply (rule is_aligned_no_overflow') 1692 apply (erule(1) pspace_alignedD) 1693 done 1694 1695lemma do_ipc_transfer_reads_respects: 1696 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1697 shows 1698 "reads_respects aag l (valid_objs and valid_global_refs and pspace_distinct and pspace_aligned 1699 and valid_arch_state and pas_refined aag and 1700 K ((grant \<longrightarrow> (is_subject aag sender \<and> 1701 is_subject aag receiver)) \<and> 1702 aag_can_read_or_affect aag l sender \<and> 1703 aag_can_read_or_affect aag l receiver 1704 )) 1705 (do_ipc_transfer sender ep badge grant receiver)" 1706 unfolding do_ipc_transfer_def 1707 apply (wp do_normal_transfer_reads_respects lookup_ipc_buffer_reads_respects 1708 lookup_ipc_buffer_has_read_auth do_fault_transfer_reads_respects 1709 thread_get_reads_respects lookup_ipc_buffer_has_auth 1710 lookup_ipc_buffer_aligned 1711 | wpc 1712 | simp 1713 | wp_once hoare_drop_imps)+ 1714 done 1715 1716crunch pas_cur_domain[wp]: set_extra_badge, do_ipc_transfer "pas_cur_domain aag" 1717 (wp: crunch_wps transfer_caps_loop_pres ignore: const_on_failure simp: crunch_simps) 1718 1719lemma complete_signal_reads_respects: 1720 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1721 shows 1722 "reads_respects aag l ( K(aag_can_read aag ntfnptr \<or> aag_can_affect aag l ntfnptr)) 1723 (complete_signal ntfnptr receiver)" 1724 unfolding complete_signal_def 1725 apply (wp set_simple_ko_reads_respects 1726 get_simple_ko_reads_respects 1727 as_user_set_register_reads_respects' 1728 | wpc 1729 | simp)+ 1730 done 1731 1732lemma receive_ipc_base_reads_respects: 1733 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1734 notes do_nbrecv_failed_transfer_def[simp] 1735 shows "reads_respects aag l 1736 (valid_objs 1737 and valid_global_refs 1738 and pspace_distinct and pspace_aligned 1739 and pas_refined aag 1740 and pas_cur_domain aag 1741 and valid_arch_state 1742 and ko_at (Endpoint ep) epptr 1743 and (\<lambda>s. is_subject aag (cur_thread s) \<and> sym_refs (state_refs_of s)) 1744 and K (is_subject aag thread 1745 \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag)) 1746 (receive_ipc_base aag thread ep epptr rights is_blocking)" 1747 apply (rule gen_asm_ev) 1748 apply (simp add: thread_get_def split: endpoint.split) 1749 apply (intro conjI impI) 1750 prefer 2 defer 1751 apply ((wp set_thread_state_reads_respects set_simple_ko_reads_respects 1752 as_user_set_register_reads_respects' 1753 | simp | intro allI impI | rule pre_ev, wpc)+)[2] 1754 apply (intro allI impI) 1755 apply (wp static_imp_wp set_simple_ko_reads_respects set_thread_state_reads_respects 1756 setup_caller_cap_reads_respects do_ipc_transfer_reads_respects 1757 possible_switch_to_reads_respects 1758 gets_cur_thread_ev set_thread_state_pas_refined 1759 | wpc 1760 | simp)+ 1761 apply (rename_tac list rvc rvd) 1762 apply (rule_tac Q="\<lambda>rv s. pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and> 1763 (sender_can_grant rvd \<longrightarrow> is_subject aag (hd list))" 1764 in hoare_strengthen_post) 1765 apply(wp set_simple_ko_reads_respects 1766 hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1] 1767 hoare_vcg_all_lift 1768 set_thread_state_reads_respects get_simple_ko_reads_respects 1769 get_simple_ko_wp do_ipc_transfer_pas_refined 1770 | wpc | simp add: get_thread_state_def thread_get_def)+ 1771 apply (clarsimp simp: conj_comms) 1772 apply (rename_tac x s) 1773 apply (rule context_conjI[rotated]) 1774 apply clarsimp 1775 apply(rule conjI, rule impI) 1776 (* clagged from Ipc_AC *) 1777 apply (subgoal_tac "aag_has_auth_to aag Control (hd x)") 1778 apply (fastforce simp add: pas_refined_refl dest!: aag_Control_into_owns) 1779 apply (rule_tac ep = "pasObjectAbs aag epptr" in aag_wellformed_grant_Control_to_send [OF _ _ pas_refined_wellformed]) 1780 apply (rule_tac s = s in pas_refined_mem [OF sta_ts]) 1781 apply (clarsimp simp: tcb_at_def thread_states_def tcb_states_of_state_def dest!: pred_tcb_at_tcb_at) 1782 apply (frule (1) sym_refs_obj_atD) 1783 apply clarsimp 1784 apply (drule (1) bspec [OF _ hd_in_set]) 1785 apply (clarsimp simp: obj_at_def tcb_bound_refs_def dest!: get_tcb_SomeD split: option.splits) 1786 apply assumption+ 1787 apply(rule conjI) 1788 (* clagged from Ipc_AC *) 1789 apply (auto elim!: ep_queued_st_tcb_at 1790 simp: tcb_at_st_tcb_at valid_ep_def valid_obj_def neq_Nil_conv 1791 split: list.split)[1] 1792 apply (simp add: obj_at_def) 1793 apply (erule (1) valid_objsE) 1794 apply (fastforce simp: valid_obj_def valid_ep_def dest: distinct_drop[where i=1]) 1795 apply (simp add: obj_at_def) 1796 apply (erule (1) valid_objsE) 1797 apply (fastforce simp: valid_obj_def valid_ep_def dest: distinct_drop[where i=1]) 1798 apply(rule send_endpoint_reads_affects_queued, simp+) 1799 apply(fastforce dest: reads_ep) 1800 apply simp+ 1801 apply(clarsimp) 1802 apply(rule_tac aag=aag and l=l in reads_affects_equiv_get_tcb_eq) 1803 apply(rule send_endpoint_reads_affects_queued) 1804 apply assumption 1805 apply blast 1806 apply(fastforce dest: reads_ep) 1807 apply assumption 1808 apply assumption 1809 apply assumption 1810 apply assumption 1811 apply(rule refl) 1812 apply simp 1813 apply simp 1814 apply simp 1815 done 1816 1817lemma receive_ipc_reads_respects: 1818 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1819 shows 1820 "reads_respects aag l (valid_objs and pspace_distinct and pspace_aligned and 1821 valid_global_refs and valid_arch_state and sym_refs \<circ> state_refs_of and 1822 pas_refined aag and pas_cur_domain aag and valid_cap cap and (\<lambda>s. is_subject aag (cur_thread s)) and K (is_subject aag receiver \<and> (\<forall>epptr\<in>Access.obj_refs cap. 1823 (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag))) (receive_ipc receiver cap is_blocking)" 1824 apply (rule gen_asm_ev) 1825 apply (simp add: receive_ipc_def thread_get_def split: cap.split) 1826 apply (clarsimp simp: fail_ev_pre) 1827 apply (rename_tac word1 word2 rights) 1828 apply (wp receive_ipc_base_reads_respects[simplified AllowSend_def] 1829 complete_signal_reads_respects 1830 | simp)+ 1831 apply (wp static_imp_wp set_simple_ko_reads_respects set_thread_state_reads_respects 1832 setup_caller_cap_reads_respects do_ipc_transfer_reads_respects 1833 complete_signal_reads_respects thread_get_reads_respects 1834 get_thread_state_reads_respects 1835 possible_switch_to_reads_respects 1836 gets_cur_thread_ev set_thread_state_pas_refined 1837 do_ipc_transfer_pas_refined 1838 hoare_vcg_all_lift 1839 get_simple_ko_reads_respects 1840 get_bound_notification_reads_respects' 1841 gbn_wp 1842 get_simple_ko_reads_respects 1843 get_simple_ko_wp 1844 get_simple_ko_wp 1845 | wpc 1846 | simp)+ 1847 apply (clarsimp) 1848 apply(rule conjI) 1849 apply(auto dest: reads_ep)[1] 1850 apply clarsimp 1851 apply(rule context_conjI, rule allI, rule impI) 1852 apply (rule disjI1) 1853 apply (frule bound_tcb_at_implies_receive) 1854 apply simp 1855 apply (frule bound_tcb_at_implies_read[where t = receiver]) 1856 apply simp 1857 apply simp 1858 apply simp 1859 apply clarsimp 1860 done 1861 1862lemma receive_endpoint_threads_blocked: 1863"\<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; 1864 ko_at (Endpoint (RecvEP list)) ep s; x\<in>set list\<rbrakk> \<Longrightarrow> 1865 st_tcb_at (receive_blocked_on ep) x s" 1866 apply (rule ep_queued_st_tcb_at'') 1867 apply simp+ 1868 done 1869 1870lemma receive_blocked_threads_have_Receive_auth: 1871 "\<lbrakk>pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); 1872 st_tcb_at (receive_blocked_on ep) x s\<rbrakk> \<Longrightarrow> 1873 (pasObjectAbs aag x,Receive,pasObjectAbs aag ep) \<in> pasPolicy aag" 1874 apply(drule_tac auth="Receive" and x=x in pas_refined_mem[rotated]) 1875 apply(rule sta_ts) 1876 apply(clarsimp simp: thread_states_def split: option.split simp: tcb_states_of_state_def st_tcb_def2) 1877 apply(case_tac "tcb_state tcb", simp_all) 1878 done 1879 1880lemma receive_endpoint_reads_affects_queued: 1881 "\<lbrakk>(pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; 1882 aag_can_read_label aag (pasObjectAbs aag epptr) \<or> 1883 aag_can_affect aag l epptr; 1884 pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); 1885 ko_at (Endpoint (RecvEP list)) epptr s; ep = RecvEP list; 1886 x \<in> set list\<rbrakk> 1887 \<Longrightarrow> 1888 aag_can_read_label aag (pasObjectAbs aag x) \<or> 1889 aag_can_affect aag l x" 1890 apply(frule receive_endpoint_threads_blocked, (simp | assumption)+) 1891 apply(drule receive_blocked_threads_have_Receive_auth, (simp | assumption)+) 1892 apply(auto dest: read_sync_ep_read_receivers) 1893 done 1894 1895lemma send_ipc_reads_respects: 1896 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1897 shows 1898 "reads_respects aag l (pas_refined aag and pas_cur_domain aag and valid_objs and pspace_distinct and 1899 pspace_aligned and valid_arch_state and valid_global_refs and sym_refs \<circ> state_refs_of and 1900 (\<lambda>s. is_subject aag (cur_thread s)) and 1901 (\<lambda>s. \<exists>ep. ko_at (Endpoint ep) epptr s 1902 \<and> (can_grant \<longrightarrow> ((\<forall>(t, rt) \<in> ep_q_refs_of ep. rt = EPRecv \<longrightarrow> is_subject aag t) 1903 \<and> aag_has_auth_to aag Grant epptr))) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (send_ipc block call badge can_grant thread epptr)" 1904 apply(rule gen_asm_ev) 1905 apply(simp add: send_ipc_def) 1906 apply (wp set_simple_ko_reads_respects set_thread_state_reads_respects 1907 when_ev setup_caller_cap_reads_respects thread_get_reads_respects 1908 | wpc | simp split del: if_split)+ 1909 apply(rename_tac list word list' rvb) 1910 apply(rule_tac Q="\<lambda>r s. is_subject aag (cur_thread s) \<and> 1911 (can_grant \<longrightarrow> is_subject aag (hd list))" 1912 in hoare_strengthen_post) 1913 apply(wp set_thread_state_reads_respects 1914 do_ipc_transfer_reads_respects 1915 set_simple_ko_reads_respects 1916 hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1] hoare_vcg_all_lift 1917 get_simple_ko_reads_respects get_simple_ko_wp 1918 possible_switch_to_reads_respects 1919 gets_cur_thread_ev set_thread_state_pas_refined 1920 do_ipc_transfer_pas_refined 1921 | wpc 1922 | simp add: get_thread_state_def thread_get_def)+ 1923 apply (rule conjI) 1924 apply(fastforce dest: reads_ep) 1925 apply clarsimp 1926 apply(subgoal_tac "\<forall> s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> 1927 get_tcb xa s = get_tcb xa t") 1928 apply (clarsimp simp: conj_comms cong: conj_cong) 1929 apply(rule conjI) 1930 (* clagged from Ipc_AC *) 1931 apply (clarsimp simp: split_def obj_at_def) 1932 apply(rule conjI) 1933 apply (rule obj_at_valid_objsE, assumption+) 1934 apply (clarsimp cong: conj_cong imp_cong simp: tcb_at_st_tcb_at conj_comms) 1935 apply (auto dest: ep_queued_st_tcb_at [where P = \<top>] simp: tcb_at_st_tcb_at valid_ep_def valid_obj_def obj_at_def split: list.split)[1] 1936 apply(rule receive_endpoint_reads_affects_queued) 1937 apply (assumption | simp)+ 1938 apply(fastforce dest: reads_ep) 1939 apply (assumption | simp)+ 1940 apply clarsimp 1941 apply(rule_tac aag=aag and l=l in reads_affects_equiv_get_tcb_eq) 1942 apply(rule receive_endpoint_reads_affects_queued) 1943 apply assumption 1944 apply(fastforce dest: reads_ep) 1945 apply assumption 1946 apply assumption 1947 apply assumption 1948 apply assumption 1949 apply(rule refl) 1950 apply simp 1951 apply simp 1952 apply simp 1953 done 1954 1955 1956subsection "Faults" 1957 1958lemma send_fault_ipc_reads_respects: 1959 assumes domains_distinct[wp]: "pas_domains_distinct aag" 1960 shows 1961 "reads_respects aag l (sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag 1962 and valid_objs and pspace_distinct and pspace_aligned 1963 and valid_global_refs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and K (is_subject aag thread \<and> valid_fault fault)) (send_fault_ipc thread fault)" 1964 apply (rule gen_asm_ev) 1965 apply (simp add: send_fault_ipc_def Let_def lookup_cap_def split_def) 1966 apply (wp send_ipc_reads_respects thread_set_reads_respects 1967 thread_set_refs_trivial thread_set_obj_at_impossible 1968 thread_set_valid_objs'' 1969 hoare_vcg_conj_lift hoare_vcg_ex_lift hoare_vcg_all_lift 1970 thread_set_pas_refined cap_fault_on_failure_rev 1971 lookup_slot_for_thread_rev 1972 lookup_slot_for_thread_authorised hoare_vcg_all_lift_R 1973 thread_get_reads_respects get_cap_auth_wp[where aag=aag] get_cap_rev 1974 | wpc 1975 | simp add: split_def del: if_split add: tcb_cap_cases_def)+ 1976 (* clagged from Ipc_AC *) 1977 apply (rule_tac Q'="\<lambda>rv s. pas_refined aag s 1978 \<and> pas_cur_domain aag s 1979 \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s 1980 \<and> valid_global_refs s \<and> valid_arch_state s 1981 \<and> sym_refs (state_refs_of s) 1982 \<and> valid_fault fault 1983 \<and> is_subject aag (fst (fst rv)) 1984 \<and> is_subject aag (cur_thread s)" 1985 in hoare_post_imp_R[rotated]) 1986 apply (clarsimp simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state 1987 | intro conjI)+ 1988 apply (fastforce intro: valid_tcb_fault_update) 1989 apply (frule caps_of_state_valid_cap, assumption) 1990 apply (clarsimp simp: valid_cap_simps obj_at_def is_ep) 1991 apply rule 1992 apply clarsimp 1993 apply (subgoal_tac "\<forall>auth. aag_has_auth_to aag auth x") 1994 apply (erule (3) owns_ep_owns_receivers', simp add: obj_at_def, assumption) 1995 apply (auto dest!: pas_refined_mem[OF sta_caps] 1996 simp: cap_auth_conferred_def cap_rights_to_auth_def)[3] 1997 1998 apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised 1999 thread_get_reads_respects 2000 | simp add: add: lookup_cap_def split_def)+ 2001 done 2002 2003 2004lemma handle_fault_reads_respects: 2005 assumes domains_distinct[wp]: "pas_domains_distinct aag" 2006 shows 2007 "reads_respects aag l (sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag 2008 and valid_objs and pspace_distinct and pspace_aligned 2009 and valid_global_refs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) 2010 and K (is_subject aag thread \<and> valid_fault fault)) (handle_fault thread fault)" 2011 unfolding handle_fault_def catch_def fun_app_def handle_double_fault_def 2012 apply(wp_once hoare_drop_imps | 2013 wp set_thread_state_reads_respects send_fault_ipc_reads_respects | wpc | simp)+ 2014 apply(fastforce intro: reads_affects_equiv_get_tcb_eq reads_lrefl) 2015 done 2016 2017 2018 2019subsection "Replies" 2020 2021lemma handle_arch_fault_reply_reads_respects: 2022 "reads_respects aag l (K (is_subject aag thread)) (handle_arch_fault_reply afault thread x y)" 2023 by (simp add: handle_arch_fault_reply_def, wp) 2024 2025lemma handle_fault_reply_reads_respects: 2026 "reads_respects aag l (K (is_subject aag thread)) (handle_fault_reply fault thread x y)" 2027 apply(case_tac fault) 2028 apply (wp as_user_reads_respects thread_get_reads_respects 2029 thread_get_wp' handle_arch_fault_reply_reads_respects[simplified K_def] 2030 | simp add: reads_lrefl det_zipWithM_x det_setRegister)+ 2031 done 2032 2033lemma lookup_ipc_buffer_has_read_auth': 2034 "\<lbrace>pas_refined aag and valid_objs and K (is_subject aag thread)\<rbrace> 2035 lookup_ipc_buffer is_receiver thread 2036 \<lbrace>\<lambda>rv s. ipc_buffer_has_read_auth aag (pasSubject aag) rv\<rbrace>" 2037 apply(rule hoare_gen_asm) 2038 apply(rule hoare_strengthen_post[OF lookup_ipc_buffer_has_read_auth]) 2039 apply(drule sym, simp) 2040 done 2041 2042 2043crunch valid_ko_at_arm[wp]: handle_fault_reply "valid_ko_at_arm" 2044 2045crunch pas_cur_domain[wp]: handle_fault_reply "pas_cur_domain aag" 2046 2047lemma do_reply_transfer_reads_respects_f: 2048 assumes domains_distinct[wp]: "pas_domains_distinct aag" 2049 shows 2050 "reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and (\<lambda>s. is_subject aag (cur_thread s)) and K (is_subject aag sender \<and> is_subject aag receiver \<and> is_subject aag (fst slot))) (do_reply_transfer sender receiver slot)" 2051 unfolding do_reply_transfer_def 2052 apply (wp gets_cur_thread_ev[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]] 2053 set_thread_state_reads_respects cap_delete_one_reads_respects_f 2054 do_ipc_transfer_reads_respects do_ipc_transfer_pas_refined 2055 thread_set_reads_respects handle_fault_reply_reads_respects 2056 get_mrs_rev lookup_ipc_buffer_reads_respects 2057 lookup_ipc_buffer_has_read_auth' get_message_info_rev 2058 get_mi_length 2059 cap_delete_one_silc_inv do_ipc_transfer_silc_inv 2060 set_thread_state_pas_refined thread_set_fault_pas_refined' 2061 possible_switch_to_reads_respects[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]] when_ev 2062 | wpc | simp split del: if_split | wp_once reads_respects_f[where aag=aag and st=st] | elim conjE | assumption | simp split del: if_split cong: if_cong 2063 | wp_once hoare_drop_imps)+ 2064 apply(rule_tac Q="\<lambda> rv s. pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> is_subject aag sender \<and> silc_inv aag st s \<and> is_subject aag receiver" in hoare_strengthen_post) 2065 apply((wp_once hoare_drop_imps 2066 | wp cap_delete_one_invs hoare_vcg_all_lift 2067 cap_delete_one_silc_inv reads_respects_f[OF thread_get_reads_respects] 2068 reads_respects_f[OF get_thread_state_rev] 2069 | simp add: invs_valid_objs invs_psp_aligned invs_valid_global_refs invs_distinct invs_arch_state invs_valid_ko_at_arm | rule conjI | elim conjE | assumption)+)[8] 2070 apply(clarsimp simp: conj_comms) 2071 apply(rule conjI, fastforce intro: reads_lrefl)+ 2072 apply(rule allI) 2073 apply(rule conjI, fastforce intro: reads_lrefl)+ 2074 apply(fastforce intro: reads_lrefl) 2075 done 2076 2077lemma handle_reply_reads_respects_f: 2078 assumes domains_distinct[wp]: "pas_domains_distinct aag" 2079 shows 2080 "reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) (handle_reply)" 2081 unfolding handle_reply_def 2082 apply (wp do_reply_transfer_reads_respects_f get_cap_wp reads_respects_f[OF get_cap_reads_respects, where Q="\<top>" and st=st] hoare_vcg_all_lift | wpc | blast)+ 2083 apply(rule conjI) 2084 apply(fastforce intro: requiv_cur_thread_eq simp: reads_equiv_f_def) 2085 apply clarsimp 2086 apply(rule conjI) 2087 apply assumption 2088 apply(rule conjI) 2089 apply(drule cte_wp_valid_cap) 2090 apply(erule invs_valid_objs) 2091 apply(simp add: valid_cap_simps) 2092 apply(rule conjI, fastforce simp: tcb_at_invs) 2093 apply(rule conjI) 2094 apply(erule emptyable_cte_wp_atD) 2095 apply(erule invs_valid_objs) 2096 apply(simp add: is_master_reply_cap_def) 2097 apply(frule_tac p="(cur_thread s, tcb_cnode_index 3)" in cap_cur_auth_caps_of_state[rotated]) 2098 apply simp 2099 apply(simp add: cte_wp_at_caps_of_state) 2100 apply(simp add: aag_cap_auth_Reply) 2101 done 2102 2103lemma reply_from_kernel_reads_respects: 2104 assumes domains_distinct[wp]: "pas_domains_distinct aag" 2105 shows 2106 "reads_respects aag l (K (is_subject aag thread)) (reply_from_kernel thread x)" 2107 unfolding reply_from_kernel_def fun_app_def 2108 apply (wp set_message_info_reads_respects set_mrs_reads_respects 2109 as_user_reads_respects lookup_ipc_buffer_reads_respects 2110 | simp add: split_def reads_lrefl det_setRegister)+ 2111 done 2112 2113 2114 2115section "globals_equiv" 2116 2117subsection "Sync IPC" 2118 2119lemma setup_caller_cap_globals_equiv: 2120 "\<lbrace>globals_equiv s and valid_ko_at_arm and valid_global_objs\<rbrace> setup_caller_cap sender receiver 2121 \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" 2122 unfolding setup_caller_cap_def 2123 apply(wp cap_insert_globals_equiv'' set_thread_state_globals_equiv) 2124 apply(simp_all) 2125 done 2126 2127lemma set_extra_badge_globals_equiv: 2128 "\<lbrace>globals_equiv s \<rbrace> 2129 set_extra_badge buffer badge n 2130 \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" 2131 unfolding set_extra_badge_def 2132 apply(wp store_word_offs_globals_equiv) 2133 done 2134 2135lemma transfer_caps_loop_globals_equiv: 2136 "\<lbrace>globals_equiv st and valid_ko_at_arm and valid_global_objs\<rbrace> 2137 transfer_caps_loop ep rcv_buffer n caps slots mi 2138 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2139proof (induct caps arbitrary: slots n mi) 2140 case Nil 2141 thus ?case by (simp, wp, simp) 2142next 2143 case (Cons c caps') 2144 show ?case 2145 apply(cases c) 2146 apply(simp split del: if_split cong: if_cong) 2147 apply(rule hoare_pre) 2148 apply(wp) 2149 apply(erule conjE, erule subst, rule Cons.hyps) 2150 apply(clarsimp) 2151 apply(wp set_extra_badge_globals_equiv)+ 2152 apply(rule Cons.hyps) 2153 apply(simp) 2154 apply(wp cap_insert_globals_equiv'') 2155 apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_global_objs" 2156 and 2157 E="\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_global_objs" in hoare_post_impErr) 2158 apply(simp add: whenE_def, rule conjI) 2159 apply(rule impI, wp)+ 2160 apply(simp)+ 2161 apply wp+ 2162 apply(fastforce) 2163 done 2164qed 2165 2166lemma transfer_caps_globals_equiv: 2167 "\<lbrace>globals_equiv st and valid_ko_at_arm and valid_global_objs\<rbrace> 2168 transfer_caps info caps endpoint receiver recv_buffer 2169 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2170 unfolding transfer_caps_def 2171 apply(wp transfer_caps_loop_globals_equiv | wpc | simp)+ 2172 done 2173 2174lemma copy_mrs_globals_equiv: 2175 "\<lbrace>globals_equiv s and valid_ko_at_arm and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> 2176 copy_mrs sender sbuf receiver rbuf n 2177 \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" 2178 unfolding copy_mrs_def including no_pre 2179 apply(wp | wpc)+ 2180 apply(rule_tac Q="\<lambda>_. globals_equiv s" 2181 in hoare_strengthen_post) 2182 apply(wp mapM_wp' | wpc)+ 2183 apply(wp store_word_offs_globals_equiv)+ 2184 apply fastforce 2185 apply simp 2186 apply(rule_tac Q="\<lambda>_. globals_equiv s and valid_ko_at_arm and (\<lambda>sa. receiver \<noteq> idle_thread sa)" 2187 in hoare_strengthen_post) 2188 apply(wp mapM_wp' as_user_globals_equiv) 2189 apply(simp) 2190 apply(fastforce) 2191 apply simp 2192 done 2193 2194(* FIXME: move *) 2195lemma validE_to_valid: 2196 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>v. rv = Inr v \<longrightarrow> Q v s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v. Q v\<rbrace>, -" 2197 apply(rule validE_validE_R) 2198 apply(simp add: validE_def valid_def) 2199 done 2200 2201 2202lemma do_normal_transfer_globals_equiv: 2203 "\<lbrace>globals_equiv st and valid_ko_at_arm and valid_global_objs and 2204 (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace> 2205 do_normal_transfer sender sbuf endpoint badge grant receiver rbuf 2206 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2207 unfolding do_normal_transfer_def 2208 apply(wp as_user_globals_equiv set_message_info_globals_equiv transfer_caps_globals_equiv) 2209 apply(wp copy_mrs_globals_equiv) 2210 apply(subst K_def) 2211 apply(wp | rule impI)+ 2212 apply(clarsimp) 2213 done 2214 2215 2216 2217lemma do_fault_transfer_globals_equiv: 2218 "\<lbrace>globals_equiv s and valid_ko_at_arm and 2219 (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace> 2220 do_fault_transfer badge sender receiver buf 2221 \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" 2222 unfolding do_fault_transfer_def 2223 apply(wp) 2224 apply(simp add: split_def) 2225 apply(wp as_user_globals_equiv set_message_info_globals_equiv 2226 set_mrs_globals_equiv | wpc)+ 2227 apply(clarsimp) 2228 apply(rule hoare_drop_imps) 2229 apply(wp thread_get_inv, simp) 2230 done 2231 2232lemma lookup_ipc_buffer_ptr_range': 2233 "\<lbrace>valid_objs\<rbrace> 2234 lookup_ipc_buffer True thread 2235 \<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits\<rbrace>" 2236 unfolding lookup_ipc_buffer_def 2237 apply (rule hoare_pre) 2238 apply (wp get_cap_wp thread_get_wp' | wpc)+ 2239 apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_auth_def get_tcb_ko_at [symmetric]) 2240 apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"]) 2241 apply (simp add: dom_tcb_cap_cases) 2242 apply (clarsimp simp: auth_ipc_buffers_def get_tcb_ko_at [symmetric]) 2243 apply (drule(1) valid_tcb_objs) 2244 apply (drule get_tcb_SomeD)+ 2245 apply (simp add: vm_read_write_def valid_tcb_def valid_ipc_buffer_cap_def split: bool.splits) 2246 done 2247 2248lemma lookup_ipc_buffer_aligned': 2249 "\<lbrace>valid_objs\<rbrace> lookup_ipc_buffer True thread 2250\<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> is_aligned buf' msg_align_bits\<rbrace>" 2251 apply(insert lookup_ipc_buffer_aligned) 2252 apply(fastforce simp: valid_def) 2253 done 2254 2255lemma set_collection: "a = {x. x\<in>a}" 2256 by simp 2257 2258lemma do_ipc_transfer_globals_equiv: 2259 "\<lbrace>globals_equiv st and valid_ko_at_arm and valid_objs and valid_arch_state and valid_global_refs 2260 and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> 2261 do_ipc_transfer sender ep badge grant receiver 2262 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2263 unfolding do_ipc_transfer_def 2264 apply(wp do_normal_transfer_globals_equiv do_fault_transfer_globals_equiv | wpc)+ 2265 apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_global_objs and 2266 (\<lambda>sa. receiver \<noteq> idle_thread sa) and 2267 (\<lambda>sa. (\<forall>rb. recv_buffer = Some rb \<longrightarrow> 2268 auth_ipc_buffers sa receiver = ptr_range rb msg_align_bits) \<and> 2269 (\<forall>rb. recv_buffer = Some rb \<longrightarrow> is_aligned rb msg_align_bits))" 2270 in hoare_strengthen_post) 2271 apply(wp) 2272 apply(clarsimp | rule conjI)+ 2273 apply(wp hoare_vcg_all_lift lookup_ipc_buffer_ptr_range' lookup_ipc_buffer_aligned' | fastforce)+ 2274 done 2275 2276crunch valid_ko_at_arm[wp]: do_ipc_transfer "valid_ko_at_arm" 2277 2278lemma send_ipc_globals_equiv: 2279 "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs 2280 and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace> 2281 send_ipc block call badge can_grant thread epptr 2282 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2283 unfolding send_ipc_def 2284 apply(wp set_simple_ko_globals_equiv set_thread_state_globals_equiv 2285 setup_caller_cap_globals_equiv | wpc)+ 2286 apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_global_objs" 2287 in hoare_strengthen_post) 2288 apply(rule thread_get_inv) 2289 apply(fastforce) 2290 apply(wp set_thread_state_globals_equiv dxo_wp_weak | simp)+ 2291 apply wpc 2292 apply(wp do_ipc_transfer_globals_equiv)+ 2293 apply(clarsimp) 2294 apply(rule hoare_drop_imps) 2295 apply(wp set_simple_ko_globals_equiv)+ 2296 apply(rule_tac Q="\<lambda>ep. ko_at (Endpoint ep) epptr and globals_equiv st and valid_objs 2297 and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned 2298 and valid_global_objs and (\<lambda>s. sym_refs (state_refs_of s)) and valid_idle" 2299 in hoare_strengthen_post) 2300 apply(wp get_simple_ko_sp) 2301 apply(clarsimp simp: valid_arch_state_ko_at_arm)+ 2302 apply (rule context_conjI) 2303 apply(rule valid_ep_recv_dequeue') 2304 apply(simp)+ 2305 apply (frule_tac x=xa in receive_endpoint_threads_blocked,simp+) 2306 by (clarsimp simp add: valid_idle_def pred_tcb_at_def obj_at_def)+ 2307 2308 2309lemma valid_ep_send_enqueue: "\<lbrakk>ko_at (Endpoint (SendEP (t # ts))) a s; valid_objs s\<rbrakk> 2310 \<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> SendEP (b # bs)) s" 2311 unfolding valid_objs_def valid_obj_def valid_ep_def obj_at_def 2312 apply (drule bspec) 2313 apply (auto split: list.splits) 2314 done 2315 2316crunch globals_equiv[wp]: complete_signal "globals_equiv st" 2317 2318 2319lemma receive_ipc_globals_equiv: 2320 notes do_nbrecv_failed_transfer_def[simp] 2321 shows "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct 2322 and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> 2323 receive_ipc thread cap is_blocking 2324 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2325 unfolding receive_ipc_def thread_get_def including no_pre 2326 apply(wp) 2327 apply(simp add: split_def) 2328 apply(wp set_simple_ko_globals_equiv set_thread_state_globals_equiv 2329 setup_caller_cap_globals_equiv dxo_wp_weak as_user_globals_equiv 2330 | wpc 2331 | simp split del: if_split)+ 2332 apply (rule hoare_strengthen_post[where Q= "\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_global_objs"]) 2333 apply (wp do_ipc_transfer_globals_equiv as_user_globals_equiv) 2334 apply clarsimp 2335 apply (wp gts_wp get_simple_ko_sp | wpc)+ 2336 apply (wp hoare_vcg_all_lift hoare_drop_imps)[1] 2337 apply(wp set_simple_ko_globals_equiv | wpc)+ 2338 apply(wp set_thread_state_globals_equiv) 2339 apply (wp get_simple_ko_wp gbn_wp get_simple_ko_wp as_user_globals_equiv | wpc | simp)+ 2340 apply (rule hoare_pre) 2341 apply(wpc) 2342 apply(rule fail_wp | rule return_wp)+ 2343 by (auto intro: valid_arch_state_ko_at_arm valid_ep_send_enqueue 2344 simp: neq_Nil_conv cong: case_list_cons_cong) 2345 2346 2347subsection "Notifications" 2348 2349lemma valid_ntfn_dequeue: 2350 "\<lbrakk> ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = (WaitingNtfn (t # ts)); 2351 valid_objs s; ts \<noteq> []\<rbrakk> 2352 \<Longrightarrow> valid_ntfn ntfn s" 2353 unfolding valid_objs_def valid_obj_def valid_ntfn_def obj_at_def 2354 apply (drule bspec) 2355 apply (auto split: list.splits) 2356 done 2357 2358 2359(* FIXME: NTFN OBJECT CHANGED *) 2360 2361lemma update_waiting_ntfn_globals_equiv: 2362 "\<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and ko_at (Notification ntfn) ntfnptr and pspace_distinct and sym_refs \<circ> state_refs_of and (\<lambda>s. idle_thread s \<notin> set queue) and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace> 2363 update_waiting_ntfn ntfnptr queue bound_tcb badge 2364 \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" 2365 unfolding update_waiting_ntfn_def 2366 apply(wp) 2367 apply(simp add: split_def) 2368 apply(wp set_thread_state_globals_equiv as_user_globals_equiv 2369 set_notification_globals_equiv set_notification_valid_ko_at_arm 2370 dxo_wp_weak | simp)+ 2371 by (auto intro: valid_arch_state_ko_at_arm simp: neq_Nil_conv) 2372 2373lemma 2374 blocked_cancel_ipc_globals_equiv[wp]: 2375 "\<lbrace>globals_equiv st and valid_ko_at_arm\<rbrace> blocked_cancel_ipc a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2376 unfolding blocked_cancel_ipc_def 2377 by (wp set_thread_state_globals_equiv set_simple_ko_globals_equiv | wpc | simp)+ 2378 2379 2380 2381 2382lemma cancel_ipc_blocked_globals_equiv: 2383 "\<lbrace>globals_equiv st and valid_ko_at_arm and st_tcb_at receive_blocked a\<rbrace> 2384 cancel_ipc a \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2385 unfolding cancel_ipc_def 2386 apply (rule hoare_seq_ext[OF _ gts_sp]) 2387 apply (rule hoare_pre) 2388 apply (wpc; (simp,rule blocked_cancel_ipc_globals_equiv)?) 2389 apply (rule hoare_pre_cont)+ 2390 apply clarsimp 2391 apply (case_tac state;(clarsimp simp: pred_tcb_at_def obj_at_def receive_blocked_def)) 2392 by (simp add: eq_commute) 2393 2394 2395crunch globals_equiv[wp]: possible_switch_to "globals_equiv (st :: det_ext state)" 2396 (wp: tcb_sched_action_extended.globals_equiv reschedule_required_ext_extended.globals_equiv 2397 crunch_wps) 2398 2399lemma send_signal_globals_equiv: 2400 "\<lbrace>globals_equiv (s :: det_ext state) and valid_objs and valid_arch_state 2401 and valid_global_refs and sym_refs \<circ> state_refs_of and 2402 pspace_distinct and valid_idle\<rbrace> send_signal ntfnptr badge 2403 \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" 2404 unfolding send_signal_def 2405 apply (wp set_notification_globals_equiv 2406 possible_switch_to_globals_equiv 2407 set_thread_state_globals_equiv 2408 as_user_globals_equiv 2409 cancel_ipc_blocked_globals_equiv 2410 update_waiting_ntfn_globals_equiv 2411 get_simple_ko_wp 2412 gts_wp 2413 | wpc 2414 | simp)+ 2415 apply clarsimp 2416 apply (frule (1) sym_refs_ko_atD) 2417 apply (intro allI impI conjI) 2418 prefer 8 2419 apply clarsimp 2420 apply (frule_tac t="idle_thread sa" and P="\<lambda>ref. \<not> idle ref" in ntfn_queued_st_tcb_at') 2421 by (auto intro: valid_arch_state_ko_at_arm 2422 simp: pred_tcb_at_def obj_at_def valid_idle_def receive_blocked_def) 2423 2424(*FIXME: belongs in Arch_IF*) 2425 2426lemma receive_signal_globals_equiv: 2427 "\<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs 2428 and pspace_distinct and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> 2429 receive_signal thread cap is_blocking 2430 \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" 2431 unfolding receive_signal_def fun_app_def do_nbrecv_failed_transfer_def 2432 apply (rule hoare_pre) 2433 apply(wp set_notification_globals_equiv set_thread_state_globals_equiv 2434 as_user_globals_equiv get_simple_ko_wp 2435 | wpc)+ 2436 apply(simp add: valid_arch_state_ko_at_arm) 2437 done 2438 2439lemma set_object_valid_global_refs: 2440 "\<lbrace>valid_global_refs and (\<lambda>s. \<forall>b. (\<forall>sz fun. obj=CNode sz fun \<longrightarrow> well_formed_cnode_n sz fun \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {})) \<and> (\<forall>tcb. obj = (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr) \<or> global_refs s \<inter> cap_range(get tcb) = {}))))\<rbrace> set_object ptr obj 2441 \<lbrace>\<lambda>_. valid_global_refs\<rbrace>" 2442 unfolding set_object_def valid_global_refs_def valid_refs_def 2443 apply(clarsimp simp: cte_wp_at_cases) 2444 apply(wp) 2445 apply(clarify) 2446 apply(rule conjI) 2447 apply(clarsimp) 2448 apply(clarsimp) 2449 apply(erule_tac x=b in allE) 2450 apply(erule_tac x=get in allE) 2451 apply(simp) 2452 done 2453 2454 2455lemma send_fault_ipc_globals_equiv: 2456 "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs 2457 and pspace_distinct and pspace_aligned 2458 and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)\<rbrace> 2459 send_fault_ipc tptr fault 2460 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2461 unfolding send_fault_ipc_def 2462 apply(wp) 2463 apply(simp add: Let_def) 2464 apply(wp send_ipc_globals_equiv thread_set_globals_equiv thread_set_valid_objs'' thread_set_fault_valid_global_refs thread_set_valid_idle_trivial thread_set_refs_trivial | wpc | simp)+ 2465 apply(rule_tac Q'="\<lambda>_. globals_equiv st and valid_objs and valid_arch_state and valid_global_refs 2466 and pspace_distinct and pspace_aligned and 2467 valid_global_objs and K (valid_fault fault) and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))" 2468 in hoare_post_imp_R) 2469 apply(wp | simp)+ 2470 apply(clarsimp simp: valid_arch_state_ko_at_arm) 2471 apply(rule valid_tcb_fault_update) 2472 apply(wp | simp)+ 2473 done 2474 2475lemma handle_double_fault_globals_equiv: 2476 "\<lbrace>globals_equiv s and valid_ko_at_arm\<rbrace> handle_double_fault tptr ex1 ex2 2477 \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" 2478 unfolding handle_double_fault_def 2479 by (wp set_thread_state_globals_equiv) 2480 2481lemma send_ipc_valid_global_objs: 2482 "\<lbrace>valid_global_objs \<rbrace> send_ipc block call badge can_grant thread epptr 2483 \<lbrace>\<lambda>_. valid_global_objs\<rbrace>" 2484 unfolding send_ipc_def 2485 apply(wp | wpc)+ 2486 apply(rule_tac Q="\<lambda>_. valid_global_objs" in hoare_strengthen_post) 2487 apply(wp, simp, (wp dxo_wp_weak |simp)+) 2488 apply(wpc) 2489 apply(rule fail_wp | rule return_wp | wp)+ 2490 apply(simp) 2491 apply(rule hoare_drop_imps) 2492 apply(wp)+ 2493 apply(rule_tac Q="\<lambda>_. valid_global_objs" in hoare_strengthen_post) 2494 apply(wp, simp+) 2495 done 2496 2497lemma send_fault_ipc_valid_global_objs: 2498 "\<lbrace>valid_global_objs \<rbrace> send_fault_ipc tptr fault 2499 \<lbrace>\<lambda>_. valid_global_objs\<rbrace>" 2500 unfolding send_fault_ipc_def 2501 apply(wp) 2502 apply(simp add: Let_def) 2503 apply(wp send_ipc_valid_global_objs | wpc)+ 2504 apply(rule_tac Q'="\<lambda>_. valid_global_objs" in hoare_post_imp_R) 2505 apply(wp | simp)+ 2506 done 2507 2508crunch valid_ko_at_arm[wp]: send_ipc "valid_ko_at_arm" 2509 (wp: hoare_drop_imps hoare_vcg_if_lift2 dxo_wp_weak) 2510 2511lemma send_fault_ipc_valid_ko_at_arm[wp]: 2512 "invariant (send_fault_ipc a b) valid_ko_at_arm" 2513 unfolding send_fault_ipc_def 2514 apply wp 2515 apply(simp add: Let_def) 2516 apply (wp send_ipc_valid_ko_at_arm | wpc)+ 2517 apply(rule_tac Q'="\<lambda>_. valid_ko_at_arm" in hoare_post_imp_R) 2518 apply (wp | simp)+ 2519done 2520 2521lemma handle_fault_globals_equiv: 2522 "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs 2523 and pspace_distinct and pspace_aligned 2524 and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) 2525 and K (valid_fault ex)\<rbrace> handle_fault thread ex 2526 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2527 unfolding handle_fault_def 2528 apply(wp handle_double_fault_globals_equiv) 2529 apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arm" and 2530 E="\<lambda>_. globals_equiv st and valid_ko_at_arm" in hoare_post_impErr) 2531 apply(wp send_fault_ipc_globals_equiv 2532 | simp add: valid_arch_state_ko_at_arm)+ 2533 done 2534 2535 2536lemma handle_fault_reply_globals_equiv: 2537 "\<lbrace>globals_equiv st and valid_ko_at_arm and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> handle_fault_reply fault thread x y 2538 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2539 apply(case_tac fault) 2540 apply(wp as_user_globals_equiv | simp add: handle_arch_fault_reply_def)+ 2541 done 2542 2543crunch valid_global_objs: handle_fault_reply "valid_global_objs" 2544 2545lemma do_reply_transfer_globals_equiv: 2546 "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct 2547 and pspace_aligned and valid_global_objs and valid_idle\<rbrace> 2548 do_reply_transfer sender receiver slot 2549 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2550 unfolding do_reply_transfer_def 2551 apply(wp set_thread_state_globals_equiv cap_delete_one_globals_equiv do_ipc_transfer_globals_equiv 2552 thread_set_globals_equiv handle_fault_reply_globals_equiv dxo_wp_weak | wpc | simp split del: if_split)+ 2553 apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_objs and valid_arch_state 2554 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) 2555 apply (wp gts_wp | fastforce simp: valid_arch_state_ko_at_arm pred_tcb_at_def obj_at_def valid_idle_def)+ 2556 done 2557 2558lemma handle_reply_globals_equiv: 2559 "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs 2560 and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle\<rbrace> handle_reply 2561 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" 2562 unfolding handle_reply_def 2563 apply(wp do_reply_transfer_globals_equiv | wpc)+ 2564 apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_objs and valid_arch_state and valid_global_refs 2565 and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle" 2566 in hoare_strengthen_post) 2567 apply(wp | simp)+ 2568 done 2569 2570lemma reply_from_kernel_globals_equiv: 2571 "\<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct 2572 and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> reply_from_kernel thread x 2573 \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" 2574 unfolding reply_from_kernel_def 2575 apply(wp set_message_info_globals_equiv set_mrs_globals_equiv 2576 as_user_globals_equiv | simp add: split_def)+ 2577 apply(insert length_msg_lt_msg_max) 2578 apply(simp add: valid_arch_state_ko_at_arm) 2579 done 2580 2581section "reads_respects_g" 2582 2583subsection "Notifications" 2584 2585lemma send_signal_reads_respects_g: 2586 assumes domains_distinct: "pas_domains_distinct aag" 2587 shows 2588 "reads_respects_g aag l (pas_refined aag and pas_cur_domain aag and valid_etcbs and 2589 valid_objs and valid_global_objs and valid_arch_state and valid_global_refs and 2590 pspace_distinct and valid_idle and sym_refs \<circ> state_refs_of and ct_active and 2591 is_subject aag \<circ> cur_thread and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (send_signal ntfnptr badge)" 2592 apply(rule equiv_valid_guard_imp[OF reads_respects_g]) 2593 apply(rule send_signal_reads_respects[OF domains_distinct]) 2594 apply(rule doesnt_touch_globalsI) 2595 apply(wp send_signal_globals_equiv | simp)+ 2596 done 2597 2598lemma receive_signal_reads_respects_g: 2599 assumes domains_distinct: "pas_domains_distinct aag" 2600 shows 2601 "reads_respects_g aag l (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pas_refined aag and (\<lambda>s. thread \<noteq> idle_thread s) and is_subject aag \<circ> cur_thread and K ((\<forall>ntfnptr\<in>Access.obj_refs cap. 2602 (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) 2603 \<in> pasPolicy aag \<and> 2604 is_subject aag thread))) (receive_signal thread cap is_blocking)" 2605 apply(rule equiv_valid_guard_imp[OF reads_respects_g]) 2606 apply(rule receive_signal_reads_respects[OF domains_distinct]) 2607 apply(rule doesnt_touch_globalsI) 2608 apply(wp receive_signal_globals_equiv | simp)+ 2609 done 2610 2611subsection "Sycn IPC" 2612 2613lemma send_ipc_reads_respects_g: 2614 assumes domains_distinct: "pas_domains_distinct aag" 2615 shows 2616 "reads_respects_g aag l (pas_refined aag and pas_cur_domain aag and valid_objs and valid_global_objs 2617 and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned 2618 and valid_idle and sym_refs \<circ> state_refs_of and is_subject aag \<circ> cur_thread and (\<lambda> s. \<exists>ep. ko_at (Endpoint ep) epptr s \<and> 2619 (can_grant \<longrightarrow> 2620 (\<forall>x\<in>ep_q_refs_of ep. 2621 (\<lambda>(t, rt). rt = EPRecv \<longrightarrow> is_subject aag t) x) \<and> 2622 (pasSubject aag, Grant, pasObjectAbs aag epptr) 2623 \<in> pasPolicy aag)) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (send_ipc block call badge can_grant thread epptr)" 2624 apply(rule equiv_valid_guard_imp[OF reads_respects_g]) 2625 apply(rule send_ipc_reads_respects[OF domains_distinct]) 2626 apply(rule doesnt_touch_globalsI) 2627 apply(wp send_ipc_globals_equiv | simp)+ 2628 done 2629 2630lemma receive_ipc_reads_respects_g: 2631 assumes domains_distinct: "pas_domains_distinct aag" 2632 shows 2633 "reads_respects_g aag l (valid_objs and valid_global_objs and valid_arch_state and valid_global_refs 2634 and pspace_distinct and pspace_aligned and (\<lambda>s. receiver \<noteq> idle_thread s) and sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread and K (is_subject aag receiver \<and> (\<forall>epptr\<in>Access.obj_refs cap. 2635 (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag))) (receive_ipc receiver cap is_blocking)" 2636 apply(rule equiv_valid_guard_imp[OF reads_respects_g]) 2637 apply(rule receive_ipc_reads_respects[OF domains_distinct]) 2638 apply(rule doesnt_touch_globalsI) 2639 apply(wp receive_ipc_globals_equiv | simp)+ 2640 done 2641 2642 2643subsection "Faults" 2644 2645lemma send_fault_ipc_reads_respects_g: 2646 assumes domains_distinct: "pas_domains_distinct aag" 2647 shows 2648 "reads_respects_g aag l (sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag and valid_objs and valid_global_objs and valid_arch_state and valid_global_refs 2649 and pspace_distinct and pspace_aligned and valid_idle and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) (send_fault_ipc thread fault)" 2650 apply(rule equiv_valid_guard_imp[OF reads_respects_g]) 2651 apply(rule send_fault_ipc_reads_respects[OF domains_distinct]) 2652 apply(rule doesnt_touch_globalsI) 2653 apply(wp send_fault_ipc_globals_equiv | simp)+ 2654 done 2655 2656 2657lemma handle_fault_reads_respects_g: 2658 assumes domains_distinct: "pas_domains_distinct aag" 2659 shows 2660 "reads_respects_g aag l (sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag 2661 and valid_objs and valid_global_objs and valid_arch_state and valid_global_refs 2662 and pspace_distinct and pspace_aligned and valid_idle and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) (handle_fault thread fault)" 2663 apply(rule equiv_valid_guard_imp[OF reads_respects_g]) 2664 apply(rule handle_fault_reads_respects[OF domains_distinct]) 2665 apply(rule doesnt_touch_globalsI) 2666 apply(wp handle_fault_globals_equiv | simp)+ 2667 done 2668 2669subsection "Replies" 2670 2671lemma handle_fault_reply_reads_respects_g: 2672 "reads_respects_g aag l (valid_ko_at_arm and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) (handle_fault_reply fault thread x y)" 2673 apply(rule equiv_valid_guard_imp[OF reads_respects_g]) 2674 apply(rule handle_fault_reply_reads_respects) 2675 apply(rule doesnt_touch_globalsI) 2676 apply(wp handle_fault_reply_globals_equiv | simp)+ 2677 done 2678 2679lemma do_reply_transfer_reads_respects_f_g: 2680 assumes domains_distinct: "pas_domains_distinct aag" 2681 shows 2682 "reads_respects_f_g aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread and K (is_subject aag sender \<and> is_subject aag receiver \<and> is_subject aag (fst slot))) (do_reply_transfer sender receiver slot)" 2683 apply(rule equiv_valid_guard_imp[OF reads_respects_f_g]) 2684 apply(rule do_reply_transfer_reads_respects_f[OF domains_distinct]) 2685 apply(rule doesnt_touch_globalsI) 2686 apply(wp do_reply_transfer_globals_equiv | simp)+ 2687 apply(simp add: invs_def valid_state_def valid_pspace_def | blast)+ 2688 done 2689 2690lemma handle_reply_reads_respects_g: 2691 assumes domains_distinct: "pas_domains_distinct aag" 2692 shows 2693 "reads_respects_f_g aag l (silc_inv aag st and invs and 2694 pas_refined aag and pas_cur_domain aag and 2695 is_subject aag \<circ> cur_thread) (handle_reply)" 2696 apply(rule equiv_valid_guard_imp[OF reads_respects_f_g]) 2697 apply(rule handle_reply_reads_respects_f[OF domains_distinct]) 2698 apply(rule doesnt_touch_globalsI) 2699 apply(wp handle_reply_globals_equiv | simp)+ 2700 apply(simp add: invs_def valid_state_def valid_pspace_def | blast)+ 2701 done 2702 2703lemma reply_from_kernel_reads_respects_g: 2704 assumes domains_distinct: "pas_domains_distinct aag" 2705 shows 2706 "reads_respects_g aag l (valid_global_objs and 2707 valid_objs and valid_arch_state and valid_global_refs and pspace_distinct 2708 and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) (reply_from_kernel thread x)" 2709 apply(rule equiv_valid_guard_imp[OF reads_respects_g]) 2710 apply(rule reply_from_kernel_reads_respects[OF domains_distinct]) 2711 apply(rule doesnt_touch_globalsI) 2712 apply(wp reply_from_kernel_globals_equiv | simp)+ 2713 done 2714 2715end 2716 2717end 2718