1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7theory Ipc_AC 8imports Finalise_AC "Lib.MonadicRewrite" 9begin 10 11context begin interpretation Arch . (*FIXME: arch_split*) 12 13section\<open>Notifications\<close> 14 15subsection\<open>@{term "pas_refined"}\<close> 16 17crunch thread_bound_ntfns[wp]: do_machine_op "\<lambda>s. P (thread_bound_ntfns s)" 18 19crunches deleted_irq_handler, send_signal 20 for state_vrefs[wp]: "\<lambda>s. P (state_vrefs (s :: det_ext state))" 21 (wp: crunch_wps hoare_unless_wp select_wp dxo_wp_weak simp: crunch_simps) 22 23lemma cancel_ipc_receive_blocked_caps_of_state: 24 "\<lbrace>\<lambda>s. P (caps_of_state (s :: det_ext state)) \<and> st_tcb_at receive_blocked t s\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" 25 apply (clarsimp simp: cancel_ipc_def) 26 apply (rule hoare_seq_ext[OF _ gts_sp]) 27 apply (rule hoare_pre) 28 apply (wp gts_wp | wpc | simp)+ 29 apply (rule hoare_pre_cont)+ 30 apply (clarsimp simp: st_tcb_def2 receive_blocked_def) 31 apply (clarsimp split: thread_state.splits) 32 done 33 34lemma send_signal_caps_of_state[wp]: 35 "\<lbrace>\<lambda>s :: det_ext state. P (caps_of_state s) \<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" 36 apply (clarsimp simp: send_signal_def) 37 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 38 apply (rule hoare_pre) 39 apply (wp dxo_wp_weak cancel_ipc_receive_blocked_caps_of_state gts_wp static_imp_wp | wpc | simp add: update_waiting_ntfn_def)+ 40 apply (clarsimp simp: fun_upd_def[symmetric] st_tcb_def2) 41 done 42 43crunches deleted_irq_handler, send_signal 44 for arch_state[wp]: "\<lambda>s. P (arch_state (s :: det_ext state))" 45 (wp: crunch_wps hoare_unless_wp select_wp dxo_wp_weak simp: crunch_simps) 46 47crunch mdb[wp]: blocked_cancel_ipc, update_waiting_ntfn "\<lambda>s. P (cdt (s :: det_ext state))" (wp: crunch_wps hoare_unless_wp select_wp dxo_wp_weak simp: crunch_simps) 48 49lemma cancel_ipc_receive_blocked_mdb: 50 "\<lbrace>\<lambda>s. P (cdt (s :: det_ext state)) \<and> st_tcb_at receive_blocked t s\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>" 51 apply (clarsimp simp: cancel_ipc_def) 52 apply (rule hoare_seq_ext[OF _ gts_sp]) 53 apply (rule hoare_pre) 54 apply (wp gts_wp | wpc | simp)+ 55 apply (rule hoare_pre_cont)+ 56 apply (clarsimp simp: st_tcb_def2 receive_blocked_def) 57 apply (clarsimp split: thread_state.splits) 58 done 59 60lemma send_signal_mdb[wp]: 61 "\<lbrace>\<lambda>s. P (cdt (s :: det_ext state))\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>" 62 apply (clarsimp simp: send_signal_def) 63 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 64 apply (rule hoare_pre) 65 apply (wp dxo_wp_weak gts_wp cancel_ipc_receive_blocked_mdb | wpc | simp)+ 66 apply (clarsimp simp: st_tcb_def2) 67 done 68 69crunches possible_switch_to 70 for tcb_domain_map_wellformed[wp]: "tcb_domain_map_wellformed aag" 71 72lemma update_waiting_ntfn_pas_refined: 73 "\<lbrace>pas_refined aag and ko_at (Notification ntfn) ntfnptr and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace> 74 update_waiting_ntfn ntfnptr queue badge val 75 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 76 apply (simp add: update_waiting_ntfn_def) 77 apply (wp set_thread_state_pas_refined set_simple_ko_pas_refined | simp)+ 78 done 79 80lemma cancel_ipc_receive_blocked_pas_refined: 81 "\<lbrace>pas_refined aag and st_tcb_at receive_blocked t\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 82 apply (clarsimp simp: cancel_ipc_def) 83 apply (rule hoare_seq_ext[OF _ gts_sp]) 84 apply (rule hoare_pre) 85 apply (wp gts_wp | wpc | simp)+ 86 apply (clarsimp simp: st_tcb_def2 receive_blocked_def) 87 done 88 89lemma send_signal_pas_refined: 90 "\<lbrace>\<lambda>s. pas_refined aag s\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 91 apply (simp add: send_signal_def) 92 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 93 apply (rule hoare_pre) 94 apply (wp set_simple_ko_pas_refined update_waiting_ntfn_pas_refined gts_wp set_thread_state_pas_refined 95 cancel_ipc_receive_blocked_pas_refined 96 | wpc 97 | simp)+ 98 apply clarsimp 99 apply (fastforce simp: st_tcb_def2) 100 done 101 102lemma receive_signal_pas_refined: 103 "\<lbrace>pas_refined aag and K (\<forall>ntfnptr \<in> obj_refs cap. (pasObjectAbs aag thread, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace> 104 receive_signal thread cap is_blocking 105 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 106 apply (simp add: receive_signal_def) 107 apply (cases cap, simp_all) 108 apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) 109 apply (rule hoare_pre) 110 by (wp set_simple_ko_pas_refined set_thread_state_pas_refined 111 | wpc | simp add: do_nbrecv_failed_transfer_def)+ 112 113 114subsection\<open>integrity\<close> 115 116subsubsection\<open>autarchy\<close> 117 118text\<open> 119 For the case when the currently-running thread owns the receiver 120 (i.e. receiver last to the notification rendezvous or sender owns 121 receiver). 122\<close> 123 124lemma st_tcb_at_tcb_states_of_state: 125 "(st_tcb_at stf p s) = (\<exists>st. tcb_states_of_state s p = Some st \<and> stf st)" 126 unfolding tcb_states_of_state_def st_tcb_def2 by auto 127 128lemma st_tcb_at_tcb_states_of_state_eq: 129 "(st_tcb_at ((=) st) p s) = (tcb_states_of_state s p = Some st)" 130 unfolding tcb_states_of_state_def st_tcb_def2 by auto 131 132lemma kheap_auth_ipc_buffer_same: 133 "kheap st thread = kheap s thread \<Longrightarrow> auth_ipc_buffers st thread = auth_ipc_buffers s thread" 134 unfolding auth_ipc_buffers_def get_tcb_def by simp 135 136lemma tcb_ipc_buffer_not_device: 137 "\<lbrakk>kheap s thread = Some (TCB tcb);valid_objs s\<rbrakk> 138 \<Longrightarrow> \<not> cap_is_device (tcb_ipcframe tcb)" 139 apply (erule(1) valid_objsE) 140 apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def 141 split: cap.split_asm arch_cap.split_asm) 142 done 143 144lemma tro_auth_ipc_buffer_idem: 145 "\<lbrakk> \<forall>x. integrity_obj aag activate subjects (pasObjectAbs aag x) (kheap st x) (kheap s x); 146 pasObjectAbs aag thread \<notin> subjects; valid_objs s \<rbrakk> 147 \<Longrightarrow> auth_ipc_buffers st thread = auth_ipc_buffers s thread" 148 apply (drule spec [where x = thread]) 149 by (erule integrity_objE; 150 simp add: auth_ipc_buffers_def get_tcb_def; 151 fastforce cong: cap.case_cong arch_cap.case_cong if_cong 152 simp: case_bool_if 153 dest!: tcb_ipc_buffer_not_device split:arch_cap.splits cap.splits 154 split: if_splits) 155 156 157lemma dmo_storeWord_respects_ipc: 158 "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and 159 K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st \<and> auth_ipc_buffers st thread = ptr_range buf msg_align_bits) \<and> 160 ipc_buffer_has_auth aag thread (Some buf) \<and> p < 2 ^ (msg_align_bits - 2)) \<rbrace> 161 do_machine_op (storeWord (buf + of_nat p * of_nat word_size) v) 162 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 163 apply (rule hoare_gen_asm) 164 apply (elim conjE) 165 apply (cases "is_subject aag thread") 166 apply (rule hoare_pre) 167 apply (rule dmo_storeWord_respects_Write) 168 apply clarsimp 169 apply (drule (1) ipc_buffer_has_auth_wordE) 170 apply simp 171 apply (simp add: msg_align_bits) 172 apply (erule mul_word_size_lt_msg_align_bits_ofnat) 173 apply simp 174 \<comment> \<open>non auth case\<close> 175 apply (rule hoare_pre) 176 apply (simp add: storeWord_def) 177 apply (wp dmo_wp) 178 apply clarsimp 179 apply (simp add: integrity_def split del: if_split) 180 apply (clarsimp split del: if_split) 181 apply (case_tac "x \<in> ptr_range (buf + of_nat p * of_nat word_size) 2") 182 apply (clarsimp simp add: st_tcb_at_tcb_states_of_state split del: if_split) 183 apply (rule trm_ipc [where p' = thread]) 184 apply simp 185 apply assumption 186 apply (clarsimp simp: ipc_buffer_has_auth_def) 187 apply (erule (1) set_mp [OF ptr_range_subset, rotated -1]) 188 apply simp 189 apply (simp add: msg_align_bits) 190 apply (erule mul_word_size_lt_msg_align_bits_ofnat) 191 apply simp 192 \<comment> \<open>otherwise\<close> 193 apply (auto simp: is_aligned_mask [symmetric] intro!: trm_lrefl ptr_range_memI ptr_range_add_memI) 194 done 195 196lemma store_word_offs_respects: 197 "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and 198 K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st \<and> auth_ipc_buffers st thread = ptr_range buf msg_align_bits) \<and> 199 ipc_buffer_has_auth aag thread (Some buf) \<and> p < 2 ^ (msg_align_bits - 2)) \<rbrace> 200 store_word_offs buf p v 201 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 202 apply (simp add: store_word_offs_def) 203 apply (rule hoare_pre) 204 apply (wp dmo_storeWord_respects_ipc [where thread = thread]) 205 apply fastforce 206 done 207 208 209lemma ipc_buffer_has_auth_None [simp]: 210 "ipc_buffer_has_auth aag receiver None" 211 unfolding ipc_buffer_has_auth_def by simp 212 213(* FIXME: MOVE *) 214lemma cap_auth_caps_of_state: 215 "\<lbrakk> caps_of_state s p = Some cap; pas_refined aag s\<rbrakk> 216 \<Longrightarrow> aag_cap_auth aag (pasObjectAbs aag (fst p)) cap" 217 unfolding aag_cap_auth_def 218 apply (intro conjI) 219 apply clarsimp 220 apply (drule (2) sta_caps) 221 apply (drule auth_graph_map_memI [where x = "pasObjectAbs aag (fst p)", OF _ sym refl]) 222 apply (rule refl) 223 apply (fastforce simp: pas_refined_def) 224 apply clarsimp 225 apply (drule (2) sta_untyped [THEN pas_refined_mem] ) 226 apply simp 227 apply (drule (1) clas_caps_of_state) 228 apply simp 229 apply (drule (1) cli_caps_of_state) 230 apply simp 231 done 232 233lemma lookup_ipc_buffer_has_auth [wp]: 234 "\<lbrace>pas_refined aag and valid_objs\<rbrace> 235 lookup_ipc_buffer True receiver 236 \<lbrace>\<lambda>rv s. ipc_buffer_has_auth aag receiver rv\<rbrace>" 237 apply (rule hoare_pre) 238 apply (simp add: lookup_ipc_buffer_def) 239 apply (wp get_cap_wp thread_get_wp' 240 | wpc)+ 241 apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_auth_def get_tcb_ko_at [symmetric]) 242 apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"]) 243 apply (simp add: dom_tcb_cap_cases) 244 apply (frule (1) caps_of_state_valid_cap) 245 apply (rule conjI) 246 apply (clarsimp simp: valid_cap_simps cap_aligned_def) 247 apply (erule aligned_add_aligned) 248 apply (rule is_aligned_andI1) 249 apply (drule (1) valid_tcb_objs) 250 apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def 251 split: if_splits) 252 apply (rule order_trans [OF _ pbfs_atleast_pageBits]) 253 apply (simp add: msg_align_bits pageBits_def) 254 apply simp 255 apply (drule (1) cap_auth_caps_of_state) 256 apply (clarsimp simp: aag_cap_auth_def cap_auth_conferred_def vspace_cap_rights_to_auth_def 257 vm_read_write_def is_page_cap_def split: if_split_asm) 258 apply (drule bspec) 259 apply (erule (3) ipcframe_subset_page) 260 apply simp 261 done 262 263lemma set_notification_respects: 264 "\<lbrace>integrity aag X st and K (aag_has_auth_to aag auth epptr \<and> auth \<in> {Receive, Notify, Reset})\<rbrace> 265 set_notification epptr ntfn' 266 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 267 apply (simp add: set_simple_ko_def set_object_def) 268 apply (wp get_object_wp) 269 apply (clarsimp simp: obj_at_def partial_inv_def a_type_def) 270 apply (erule integrity_trans) 271 apply (clarsimp simp: integrity_def tro_ntfn) 272 done 273 274lemma receive_signal_integrity_autarch: 275 "\<lbrace>integrity aag X st and pas_refined aag and valid_objs 276 and K ((\<forall>ntfnptr \<in> obj_refs cap. aag_has_auth_to aag Receive ntfnptr) 277 \<and> is_subject aag thread)\<rbrace> 278 receive_signal thread cap is_blocking 279 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 280 apply (simp add: receive_signal_def) 281 apply (cases cap, simp_all) 282 apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) 283 apply (rule hoare_pre) 284 apply (wp set_notification_respects[where auth=Receive] set_thread_state_integrity_autarch as_user_integrity_autarch 285 | wpc 286 | simp add: do_nbrecv_failed_transfer_def)+ 287 done 288 289subsubsection\<open>Non-autarchy: the sender is running\<close> 290 291 292lemma length_msg_registers: 293 "length msg_registers = 4" 294 unfolding msg_registers_def 295 by (simp add: msgRegisters_def upto_enum_def fromEnum_def enum_register) 296 297lemma send_upd_ctxintegrity: 298 "\<lbrakk> direct_send {pasSubject aag} aag ep tcb 299 \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; 300 integrity aag X st s; st_tcb_at ((=) Structures_A.thread_state.Running) thread s; 301 get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'\<rbrakk> 302 \<Longrightarrow> integrity aag X st (s\<lparr>kheap := 303 kheap s(thread \<mapsto> TCB (tcb'\<lparr>tcb_arch := 304 arch_tcb_context_set c' (tcb_arch tcb') 305 \<rparr>)) 306 \<rparr>)" 307 apply (clarsimp simp: integrity_def tcb_states_of_state_preserved st_tcb_def2) 308 apply (drule get_tcb_SomeD)+ 309 apply (drule spec[where x=thread], simp) 310 apply (cases "is_subject aag thread") 311 apply (rule tro_lrefl, solves\<open>simp\<close>) 312 313 (* slow 5s *) 314 by (erule integrity_objE; 315 (* eliminate all TCB unrelated cases and simplifies the other *) 316 clarsimp; 317 (* deal with the orefl case *) 318 ( solves\<open>simp add:direct_send_def indirect_send_def\<close> 319 (* deal with the other case by applying either the reply, call or send rules and then 320 the generic rule *) 321 | rule tro_trans_spec, 322 (rule tro_tcb_reply'[OF refl refl refl] tro_tcb_call[OF refl refl refl] 323 tro_tcb_send[OF refl refl refl]; 324 blast), 325 rule tro_trans_spec, 326 (rule tro_tcb_generic'[OF refl refl refl]; simp), 327 rule tro_orefl, simp, rule tcb.equality; solves\<open>simp add:arch_tcb_context_set_def\<close>)) 328 329lemma set_mrs_respects_in_signalling': 330 "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and 331 K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st 332 \<and> case_option True (\<lambda>buf'. auth_ipc_buffers st thread = ptr_range buf' msg_align_bits) buf) 333 \<and> aag_has_auth_to aag Notify ep \<and> ipc_buffer_has_auth aag thread buf) \<rbrace> 334 set_mrs thread buf msgs 335 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 336 apply (rule hoare_gen_asm) 337 apply (simp add: set_mrs_def split_def set_object_def get_object_def split del: if_split) 338 apply (wp gets_the_wp get_wp put_wp 339 | wpc 340 | simp split del: if_split 341 add: zipWithM_x_mapM_x split_def store_word_offs_def fun_upd_def[symmetric])+ 342 apply (rule hoare_post_imp [where Q = "\<lambda>rv. st_tcb_at ((=) Structures_A.Running) thread and integrity aag X st"]) 343 apply simp 344 apply (wp mapM_x_wp' dmo_storeWord_respects_ipc [where thread = thread and ep = ep]) 345 apply (fastforce simp add: set_zip nth_append simp: msg_align_bits msg_max_length_def 346 split: if_split_asm) 347 apply wp+ 348 apply (rule impI) 349 apply (subgoal_tac "\<forall>c'. integrity aag X st 350 (s\<lparr>kheap := kheap s(thread \<mapsto> 351 TCB ((the (get_tcb thread s))\<lparr>tcb_arch := arch_tcb_set_registers c' (tcb_arch (the (get_tcb thread s))) \<rparr>))\<rparr>)") 352 apply (clarsimp simp: fun_upd_def st_tcb_at_nostate_upd [unfolded fun_upd_def]) 353 apply (rule allI) 354 apply clarsimp 355 apply (cases "is_subject aag thread") 356 apply (erule (1) integrity_update_autarch) 357 apply (clarsimp simp: st_tcb_def2 arch_tcb_set_registers_def) 358 apply (rule send_upd_ctxintegrity[OF disjI1], auto simp: st_tcb_def2 direct_send_def) 359 done 360 361lemma as_user_set_register_respects: 362 "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and 363 K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st) \<and> (aag_has_auth_to aag SyncSend ep \<or> aag_has_auth_to aag Notify ep)) \<rbrace> 364 as_user thread (set_register r v) 365 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 366 apply (simp add: as_user_def split_def set_object_def get_object_def) 367 apply wp 368 apply (clarsimp simp: in_monad setRegister_def) 369 apply (cases "is_subject aag thread") 370 apply (erule (1) integrity_update_autarch [unfolded fun_upd_def]) 371 apply (clarsimp simp: st_tcb_def2) 372 apply (rule send_upd_ctxintegrity [OF disjI1, unfolded fun_upd_def]) 373 apply (auto simp: direct_send_def st_tcb_def2) 374 done 375 376lemma lookup_ipc_buffer_ptr_range: 377 "\<lbrace>valid_objs and integrity aag X st\<rbrace> 378 lookup_ipc_buffer True thread 379 \<lbrace>\<lambda>rv s. \<not> is_subject aag thread \<longrightarrow> (case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits) \<rbrace>" 380 unfolding lookup_ipc_buffer_def 381 apply (rule hoare_pre) 382 apply (wp get_cap_wp thread_get_wp' | wpc)+ 383 apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_auth_def get_tcb_ko_at [symmetric]) 384 apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"]) 385 apply (simp add: dom_tcb_cap_cases) 386 apply (clarsimp simp: auth_ipc_buffers_def get_tcb_ko_at [symmetric] integrity_def) 387 apply (drule spec [where x = thread])+ 388 apply (drule get_tcb_SomeD)+ 389 apply (erule(1) valid_objsE) 390 apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def case_bool_if 391 split: if_split_asm) 392 apply (erule integrity_objE, simp_all add: get_tcb_def vm_read_write_def) 393 apply auto 394 done 395 396lemma set_thread_state_respects_in_signalling: 397 "\<lbrace>integrity aag X st 398 and (\<lambda>s. \<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ntfnptr) thread s) 399 and K (aag_has_auth_to aag Notify ntfnptr)\<rbrace> 400 set_thread_state thread Structures_A.thread_state.Running 401 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 402 apply (simp add: set_thread_state_def set_object_def get_object_def) 403 apply wp 404 apply (clarsimp) 405 apply (cases "is_subject aag thread") 406 apply (erule(1) integrity_update_autarch [unfolded fun_upd_def]) 407 apply (erule integrity_trans) 408 apply (drule get_tcb_SomeD) 409 apply (clarsimp simp: integrity_def st_tcb_def2) 410 apply (clarsimp dest!: get_tcb_SomeD) 411 apply (rule tro_tcb_send [OF refl refl]) 412 apply (rule tcb.equality;simp; rule arch_tcb_context_set_eq[symmetric]) 413 apply (auto simp: indirect_send_def direct_send_def) 414 done 415 416lemma set_notification_obj_at: 417 "\<lbrace>obj_at P ptr and K (ptr \<noteq> ntfnptr)\<rbrace> 418 set_notification ntfnptr queue 419 \<lbrace>\<lambda>rv. obj_at P ptr\<rbrace>" 420 apply (simp add: set_simple_ko_def set_object_def) 421 apply (wp get_object_wp) 422 apply (auto simp: obj_at_def) 423 done 424 425lemma set_ntfn_valid_objs_at: 426 "\<lbrace>valid_objs and (\<lambda>s. ntfn_at p s \<longrightarrow> valid_ntfn ntfn s)\<rbrace> set_notification p ntfn \<lbrace>\<lambda>rv. valid_objs\<rbrace>" 427 unfolding set_simple_ko_def 428 apply (rule hoare_pre) 429 apply (wp set_object_valid_objs get_object_wp) 430 apply (clarsimp simp: valid_obj_def obj_at_def is_ntfn partial_inv_def 431 split: Structures_A.kernel_object.splits) 432 done 433 434lemma drop_Suc0_iff: 435 "xs \<noteq> [] \<Longrightarrow> (drop (Suc 0) xs = ys) = (\<exists>x. xs = x # ys)" 436 by (auto simp: neq_Nil_conv) 437 438lemma receive_blocked_on_def3: 439 "receive_blocked_on ref ts = 440 ((\<exists>pl. ts = Structures_A.BlockedOnReceive ref pl) 441 \<or> ts = Structures_A.BlockedOnNotification ref)" 442 by (cases ts, auto) 443 444 445lemma integrity_receive_blocked_chain: 446 "\<lbrakk> st_tcb_at (receive_blocked_on ep) p s; integrity aag X st s; \<not> is_subject aag p \<rbrakk> \<Longrightarrow> st_tcb_at (receive_blocked_on ep) p st" 447 apply (clarsimp simp: integrity_def st_tcb_at_tcb_states_of_state) 448 apply (drule (1) tsos_tro [where p = p] ) 449 apply (fastforce simp: tcb_states_of_state_def) 450 apply simp 451 apply simp 452 done 453 454crunch integrity[wp]: possible_switch_to "integrity aag X st" 455 (ignore: tcb_sched_action) 456 457abbreviation 458 "integrity_once_ts_upd t ts aag X st s 459 == integrity aag X st (s \<lparr> kheap := (kheap s) ( t := Some (TCB ((the (get_tcb t s)) \<lparr>tcb_state := ts\<rparr>)))\<rparr>)" 460 461lemma set_scheduler_action_integrity_once_ts_upd: 462 "\<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> 463 set_scheduler_action sa \<lbrace>\<lambda>_. integrity_once_ts_upd t ts aag X st\<rbrace>" 464 apply (simp add: set_scheduler_action_def, wp) 465 apply clarsimp 466 apply (erule rsubst[where P="\<lambda>x. x"]) 467 apply (rule trans, rule_tac f="\<lambda>x. sa" in eintegrity_sa_update[symmetric]) 468 apply (rule arg_cong[where f="integrity aag X st"]) 469 apply (simp add: get_tcb_def) 470 done 471 472crunch integrity_once_ts_upd: set_thread_state_ext "integrity_once_ts_upd t ts aag X st" 473 474lemma set_thread_state_integrity_once_ts_upd: 475 "\<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> 476 set_thread_state t ts' \<lbrace>\<lambda>_. integrity_once_ts_upd t ts aag X st\<rbrace>" 477 apply (simp add: set_thread_state_def) 478 apply (wpsimp wp: set_object_wp set_thread_state_ext_integrity_once_ts_upd) 479 apply (clarsimp simp: fun_upd_def dest!: get_tcb_SomeD) 480 apply (simp add: get_tcb_def cong: if_cong) 481 done 482 483lemma get_tcb_recv_blocked_implies_receive: 484 "\<lbrakk>pas_refined aag s; get_tcb t s = Some tcb; ep_recv_blocked ep (tcb_state tcb) \<rbrakk> 485 \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag" 486 apply (erule pas_refined_mem[rotated]) 487 apply (rule sta_ts) 488 apply (simp add: thread_states_def tcb_states_of_state_def) 489 apply (case_tac "tcb_state tcb", simp_all) 490 done 491 492lemma cancel_ipc_receive_blocked_respects: 493 "\<lbrace>integrity aag X st and pas_refined aag and st_tcb_at (receive_blocked) t and 494 (sym_refs o state_refs_of) and 495 bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and 496 K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> 497 (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace> 498 cancel_ipc t \<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace>" 499 apply (clarsimp simp: cancel_ipc_def bind_assoc) 500 apply (rule hoare_seq_ext[OF _ gts_sp]) 501 apply (rule hoare_name_pre_state) 502 apply (subgoal_tac "case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False") 503 apply (simp add: blocked_cancel_ipc_def bind_assoc set_simple_ko_def set_object_def 504 get_ep_queue_def get_blocking_object_def 505 split: thread_state.splits) 506 apply (rule hoare_pre) 507 apply (wp set_thread_state_integrity_once_ts_upd get_object_wp get_simple_ko_wp 508 | wpc)+ 509 apply (clarsimp simp: st_tcb_at_def2 obj_at_def) 510 apply (rename_tac ep payload s tcb ntfn) 511 apply (drule_tac t="tcb_state tcb" in sym) 512 apply (subgoal_tac "st_tcb_at ((=) (tcb_state tcb)) t s") 513 apply (drule(1) sym_refs_st_tcb_atD) 514 apply (clarsimp simp: obj_at_def ep_q_refs_of_def fun_upd_def get_tcb_def 515 split: endpoint.splits cong: if_cong) 516 apply (intro impI conjI, simp_all)[1] 517 apply (erule integrity_trans) 518 apply (simp add: integrity_def) 519 apply (intro impI conjI allI) 520 apply clarsimp 521 apply (rule tro_ep_unblock; simp?) 522 apply (erule get_tcb_recv_blocked_implies_receive, erule get_tcb_rev; solves\<open>simp\<close>) 523 apply (rule_tac ep=ep in tro_tcb_send[OF refl refl]; 524 fastforce intro!: tcb.equality arch_tcb_context_set_eq[symmetric] 525 simp: indirect_send_def pred_tcb_at_def obj_at_def) 526 apply (fastforce simp: indirect_send_def pred_tcb_at_def obj_at_def) 527 apply (fastforce simp: pred_tcb_at_def obj_at_def receive_blocked_def) 528 done 529 530lemma set_thread_state_integrity': 531 "\<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> set_thread_state t ts \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 532 apply (simp add: set_thread_state_def) 533 by (wpsimp wp: set_object_wp) 534 535lemma as_user_set_register_respects_indirect: 536 "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and 537 K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at receive_blocked thread st 538 \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st) 539 \<and> (aag_has_auth_to aag Notify ntfnptr)) \<rbrace> 540 as_user thread (set_register r v) 541 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 542 apply (simp add: as_user_def split_def set_object_def get_object_def) 543 apply wp 544 apply (clarsimp simp: in_monad setRegister_def) 545 apply (cases "is_subject aag thread") 546 apply (erule (1) integrity_update_autarch [unfolded fun_upd_def]) 547 apply (clarsimp simp: st_tcb_def2 receive_blocked_def) 548 apply (simp split: thread_state.split_asm) 549 apply (rule send_upd_ctxintegrity [OF disjI2, unfolded fun_upd_def], 550 auto simp: st_tcb_def2 indirect_send_def pred_tcb_def2 dest: sym) 551 done 552 553lemma integrity_receive_blocked_chain': 554 "\<lbrakk> st_tcb_at receive_blocked p s; integrity aag X st s; \<not> is_subject aag p \<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked p st" 555 apply (clarsimp simp: integrity_def st_tcb_at_tcb_states_of_state receive_blocked_def) 556 apply (simp split: thread_state.split_asm) 557 apply (rename_tac word pl) 558 apply (drule_tac ep=word in tsos_tro [where p = p], simp+ ) 559 done 560 561lemma tba_Some: 562 "thread_bound_ntfns s t = Some a \<Longrightarrow> bound_tcb_at ((=) (Some a)) t s" 563 by (clarsimp simp: thread_bound_ntfns_def pred_tcb_at_def obj_at_def get_tcb_def 564 split: option.splits kernel_object.splits) 565 566 567lemma tsos_tro': 568 "\<lbrakk>\<forall>x. integrity_obj aag activate subjects (pasObjectAbs aag x) (kheap s x) (kheap s' x); 569 thread_bound_ntfns s' p = Some a; pasObjectAbs aag p \<notin> subjects \<rbrakk> 570 \<Longrightarrow> thread_bound_ntfns s p = Some a" 571 apply (drule_tac x=p in spec) 572 apply (erule integrity_objE; 573 simp?; 574 fastforce simp: thread_bound_ntfns_def get_tcb_def 575 tcb_bound_notification_reset_integrity_def) 576 done 577 578lemma integrity_receive_blocked_chain_bound: 579 "\<lbrakk>bound_tcb_at ((=) (Some ntfnptr)) p s; integrity aag X st s; \<not> is_subject aag p\<rbrakk> 580 \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) p st" 581 apply (clarsimp simp: integrity_def) 582 apply (drule bound_tcb_at_thread_bound_ntfns) 583 apply (drule tsos_tro' [where p = p], simp+ ) 584 apply (clarsimp simp:tba_Some) 585 done 586 587lemma send_signal_respects: 588 "\<lbrace>integrity aag X st and pas_refined aag 589 and valid_objs 590 and sym_refs \<circ> state_refs_of 591 and K (aag_has_auth_to aag Notify ntfnptr)\<rbrace> 592 send_signal ntfnptr badge 593 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 594 apply (simp add: send_signal_def) 595 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 596 apply (rule hoare_name_pre_state) 597 apply (case_tac "ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None") 598 \<comment> \<open>ntfn-binding case\<close> 599 apply (rule hoare_pre) 600 apply (wp set_notification_respects[where auth=Notify] 601 as_user_set_register_respects_indirect[where ntfnptr=ntfnptr] 602 set_thread_state_integrity' sts_st_tcb_at' static_imp_wp 603 cancel_ipc_receive_blocked_respects[where ntfnptr=ntfnptr] 604 gts_wp 605 | wpc | simp)+ 606 apply (clarsimp, rule conjI, clarsimp simp: st_tcb_def2) 607 apply (clarsimp simp: receive_blocked_def) 608 apply (simp split: thread_state.split_asm) 609 apply (clarsimp simp: obj_at_def) 610 apply (drule (3) ntfn_bound_tcb_at[where ntfnptr=ntfnptr and P="\<lambda>ntfn. ntfn = Some ntfnptr"], simp+)[1] 611 apply (rule conjI) 612 apply (drule_tac x=ntfnptr and t=y in bound_tcb_at_implies_receive) 613 apply (clarsimp simp: pred_tcb_at_def obj_at_def, simp) 614 apply clarsimp 615 apply (rule conjI) 616 apply (rule_tac s=sa in integrity_receive_blocked_chain') 617 apply (clarsimp simp add: pred_tcb_at_def obj_at_def receive_blocked_def) 618 apply (fastforce split: thread_state.split) 619 apply simp+ 620 apply (rule_tac s=sa in integrity_receive_blocked_chain_bound) 621 apply (clarsimp simp: pred_tcb_at_def obj_at_def) 622 apply simp+ 623 apply (rule hoare_pre) 624 apply clarsimp 625 apply (wpc, clarsimp) 626 apply (wp set_notification_respects[where auth=Notify] 627 sts_st_tcb_at' as_user_set_register_respects 628 set_thread_state_pas_refined set_simple_ko_pas_refined 629 set_thread_state_respects_in_signalling [where ntfnptr = ntfnptr] 630 set_ntfn_valid_objs_at hoare_vcg_disj_lift static_imp_wp 631 | wpc 632 | simp add: update_waiting_ntfn_def)+ 633 apply clarsimp 634 apply (subgoal_tac "st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa") 635 prefer 2 636 apply (rule ntfn_queued_st_tcb_at', assumption) 637 apply (fastforce simp: obj_at_def valid_obj_def valid_ntfn_def) 638 apply assumption+ 639 apply simp 640 apply simp 641 apply (intro impI conjI) 642 \<comment> \<open>st_tcb_at receive_blocked st\<close> 643 apply (erule (2) integrity_receive_blocked_chain) 644 apply clarsimp 645 done 646 647section\<open>Sync IPC\<close> 648 649text\<open> 650 651When transferring caps, i.e. when the grant argument is true on the 652IPC operations, the currently-running thread owns the receiver. Either 653it is the receiver (and ?thesis by well-formedness) or it is the 654sender, and that can send arbitrary caps, hence ?thesis by sbta_ipc 655etc. 656 657\<close> 658 659subsection\<open>auxiliary\<close> 660 661 662lemma cap_master_cap_masked_as_full: 663 "cap_master_cap (masked_as_full a a) = cap_master_cap a " 664 apply(clarsimp simp: cap_master_cap_def split: cap.splits simp: masked_as_full_def) 665 done 666 667lemma cap_badge_masked_as_full: 668 "(cap_badge (masked_as_full a a), cap_badge a) \<in> capBadge_ordering False" 669 apply(case_tac a, simp_all add: masked_as_full_def) 670 done 671 672 673 674lemma masked_as_full_double: 675 "masked_as_full (masked_as_full ab ab) cap' = masked_as_full ab ab" 676 apply(case_tac ab, simp_all add: masked_as_full_def) 677 done 678 679lemma transfer_caps_loop_pres_dest_aux: 680 assumes x: "\<And>cap src dest. 681 \<lbrace>\<lambda>s. P s \<and> dest \<in> slots' \<and> src \<in> snd ` caps' 682 \<and> (valid_objs s \<and> real_cte_at dest s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s 683 \<and> real_cte_at src s 684 \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> cap.NullCap) \<rbrace> 685 cap_insert cap src dest \<lbrace>\<lambda>rv. P\<rbrace>" 686 assumes eb: "\<And>b n'. n' \<le> N \<Longrightarrow> \<lbrace>P\<rbrace> set_extra_badge buffer b n' \<lbrace>\<lambda>_. P\<rbrace>" 687 shows "n + length caps \<le> N \<Longrightarrow> 688 \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and> 689 (valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> 690 (\<forall>x \<in> set slots. real_cte_at x s) \<and> 691 (\<forall>x \<in> set caps. s \<turnstile> fst x \<and> 692 cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s 693 \<and> real_cte_at (snd x) s))\<rbrace> 694 transfer_caps_loop ep buffer n caps slots mi 695 \<lbrace>\<lambda>rv. P\<rbrace>" (is "?L \<Longrightarrow> ?P n caps slots mi") 696proof (induct caps arbitrary: slots n mi) 697 case Nil 698 thus ?case by (simp, wp, simp) 699next 700 case (Cons m ms) 701 hence nN: "n \<le> N" by simp 702 703 from Cons have "\<And>slots mi. ?P (n + 1) ms slots mi" by clarsimp 704 thus ?case 705 apply (cases m) 706 apply (clarsimp simp add: Let_def split_def whenE_def 707 cong: if_cong list.case_cong split del: if_split) 708 apply (rule hoare_pre) 709 apply (wp eb [OF nN] hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift 710 | assumption | simp split del: if_split)+ 711 712 apply (rule cap_insert_assume_null) 713 apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at)+ 714 (* cannot blindly use derive_cap_is_derived_foo here , need to first hoist 715 out of the postcondition the conjunct that the return value is derived, 716 and solve this using derived_cap_is_derived, and then solve the rest 717 using derive_cap_is_derived_foo *) 718 apply (rule_tac Q'="\<lambda>r s. S r s \<and> Q r s" for S Q in hoare_post_imp_R) 719 apply (rule hoare_vcg_conj_lift_R) 720 apply (rule derive_cap_is_derived) 721 prefer 2 722 apply clarsimp 723 apply assumption 724 apply(wp derive_cap_is_derived_foo)+ 725 apply (simp only: tl_drop_1[symmetric]) 726 apply (clarsimp simp: cte_wp_at_caps_of_state 727 ex_cte_cap_to_cnode_always_appropriate_strg 728 real_cte_tcb_valid caps_of_state_valid 729 split del: if_split) 730 apply (clarsimp simp: remove_rights_def caps_of_state_valid 731 neq_Nil_conv cte_wp_at_caps_of_state 732 imp_conjR[symmetric] cap_master_cap_masked_as_full 733 cap_badge_masked_as_full 734 split del: if_split) 735 apply(intro conjI) 736 apply clarsimp 737 apply (case_tac "cap = a",clarsimp simp: remove_rights_def) 738 apply (clarsimp simp:masked_as_full_def is_cap_simps) 739 apply (clarsimp simp: cap_master_cap_simps remove_rights_def split:if_splits) 740 apply clarsimp 741 apply (intro conjI) 742 apply (clarsimp split:if_splits elim!: image_eqI[rotated]) 743 apply (clarsimp split:if_splits simp: remove_rights_def) 744 apply (rule ballI) 745 apply (drule(1) bspec) 746 apply clarsimp 747 apply (intro conjI) 748 apply clarsimp 749 apply clarsimp 750 apply (case_tac "capa = ab",clarsimp simp: masked_as_full_def is_cap_simps split: if_splits) 751 apply (clarsimp simp: masked_as_full_double) 752 done 753qed 754 755 756(* FIXME: move *) 757lemma transfer_caps_loop_pres_dest: 758 assumes x: "\<And>cap src dest. 759 \<lbrace>\<lambda>s. P s \<and> dest \<in> set slots \<and> src \<in> snd ` set caps 760 \<and> (valid_objs s \<and> real_cte_at dest s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s 761 \<and> real_cte_at src s 762 \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> cap.NullCap) \<rbrace> 763 cap_insert cap src dest \<lbrace>\<lambda>rv. P\<rbrace>" 764 assumes eb: "\<And>b n'. n' \<le> n + length caps \<Longrightarrow> \<lbrace>P\<rbrace> set_extra_badge buffer b n' \<lbrace>\<lambda>_. P\<rbrace>" 765 shows "\<lbrace>\<lambda>s. P s \<and> (valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> 766 (\<forall>x \<in> set slots. real_cte_at x s) \<and> 767 (\<forall>x \<in> set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s 768 \<and> real_cte_at (snd x) s))\<rbrace> 769 transfer_caps_loop ep buffer n caps slots mi 770 \<lbrace>\<lambda>rv. P\<rbrace>" 771 apply (rule hoare_pre) 772 apply (rule transfer_caps_loop_pres_dest_aux [OF x eb]) 773 apply assumption 774 apply simp 775 apply simp 776 done 777 778subsection\<open>pas_refined\<close> 779 780lemma lookup_slot_for_thread_authorised: 781 "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> 782 lookup_slot_for_thread thread cref 783 \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>,-" 784 unfolding lookup_slot_for_thread_def 785 apply wp 786 apply (clarsimp simp: owns_thread_owns_cspace) 787 done 788 789lemma cnode_cap_all_auth_owns: 790 "(\<exists>s. is_cnode_cap cap \<and> (\<forall>x\<in>obj_refs cap. 791 \<forall>auth\<in>cap_auth_conferred cap. aag_has_auth_to aag auth x) 792 \<and> pas_refined aag s) 793 \<longrightarrow> (\<forall>x\<in>obj_refs cap. is_subject aag x)" 794 apply (clarsimp simp: is_cap_simps) 795 apply (clarsimp simp: cap_auth_conferred_def pas_refined_all_auth_is_owns) 796 done 797 798lemma get_receive_slots_authorised: 799 "\<lbrace>pas_refined aag and K (\<forall>rbuf. recv_buf = Some rbuf \<longrightarrow> is_subject aag receiver)\<rbrace> 800 get_receive_slots receiver recv_buf 801 \<lbrace>\<lambda>rv s. \<forall>slot \<in> set rv. is_subject aag (fst slot)\<rbrace>" 802 apply (rule hoare_gen_asm) 803 apply (cases recv_buf) 804 apply (simp, wp, simp) 805 apply clarsimp 806 apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised 807 | rule hoare_drop_imps 808 | simp add: add: lookup_cap_def split_def)+ 809 apply (strengthen cnode_cap_all_auth_owns, simp add: aag_cap_auth_def) 810 apply (wp hoare_vcg_all_lift_R hoare_drop_imps)+ 811 apply clarsimp 812 apply (fastforce simp: is_cap_simps) 813 done 814 815crunch pas_refined[wp]: set_extra_badge "pas_refined aag" 816 817lemma remove_rights_clas [simp]: 818 "cap_links_asid_slot aag p (remove_rights R cap) = cap_links_asid_slot aag p cap" 819 unfolding cap_links_asid_slot_def remove_rights_def cap_rights_update_def acap_rights_update_def 820 by (clarsimp split: cap.splits arch_cap.splits bool.splits) 821 822lemma remove_rights_cap_auth_conferred_subset: 823 "x \<in> cap_auth_conferred (remove_rights R cap) \<Longrightarrow> x \<in> cap_auth_conferred cap" 824 unfolding remove_rights_def cap_rights_update_def 825 apply (clarsimp split: if_split_asm cap.splits arch_cap.splits bool.splits 826 simp: cap_auth_conferred_def vspace_cap_rights_to_auth_def acap_rights_update_def 827 validate_vm_rights_def vm_read_only_def vm_kernel_only_def) 828 apply (erule set_mp [OF cap_rights_to_auth_mono, rotated], clarsimp)+ 829 apply (auto simp: is_page_cap_def cap_rights_to_auth_def reply_cap_rights_to_auth_def split:if_splits) 830 done 831 832lemma remove_rights_cli [simp]: 833 "cap_links_irq aag l (remove_rights R cap) = cap_links_irq aag l cap" 834 unfolding remove_rights_def cap_rights_update_def 835 by (clarsimp split: cap.splits arch_cap.splits bool.splits simp: cap_links_irq_def) 836 837lemma remove_rights_untyped_range [simp]: 838 "untyped_range (remove_rights R c) = untyped_range c" 839 unfolding remove_rights_def cap_rights_update_def 840 by (clarsimp split: cap.splits arch_cap.splits bool.splits simp: ) 841 842lemma obj_refs_remove_rights [simp]: 843 "obj_refs (remove_rights rs cap) = obj_refs cap" 844 unfolding remove_rights_def 845 by (cases cap, simp_all add: cap_rights_update_def acap_rights_update_def split: arch_cap.splits bool.splits) 846 847lemma remove_rights_cur_auth: 848 "pas_cap_cur_auth aag cap \<Longrightarrow> pas_cap_cur_auth aag (remove_rights R cap)" 849 unfolding aag_cap_auth_def 850 by (clarsimp dest!: remove_rights_cap_auth_conferred_subset) 851 852(* FIXME MOVE *) 853lemmas hoare_gen_asmE2 = hoare_gen_asmE[where P'=\<top>,simplified pred_and_true_var] 854 855 856lemma derive_cap_is_transferable: 857 "\<lbrace>K(is_transferable_cap cap) \<rbrace> derive_cap slot cap \<lbrace>\<lambda>r s. is_transferable_cap r\<rbrace>, -" 858 apply (rule hoare_gen_asmE2) 859 by (erule is_transferable_capE; wpsimp simp: derive_cap_def) 860 861lemma auth_derived_refl[simp]: 862 " auth_derived cap cap" 863 by (simp add:auth_derived_def) 864 865lemma derive_cap_auth_derived: 866 "\<lbrace>\<top>\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv _. rv \<noteq> NullCap \<longrightarrow> auth_derived rv cap \<rbrace>,-" 867 apply (cases cap ; (wpsimp simp:derive_cap_def)?) 868 apply (case_tac x12 ; 869 simp add:derive_cap_def arch_derive_cap_def; 870 wpc?; 871 wp?; 872 simp add:auth_derived_def cap_auth_conferred_def) 873 done 874 875(* FIXME MOVE *) 876lemma auth_derived_pas_cur_auth: 877 "auth_derived cap cap' \<Longrightarrow> pas_cap_cur_auth aag cap' \<Longrightarrow> pas_cap_cur_auth aag cap" 878 by (force simp:aag_cap_auth_def auth_derived_def cap_links_asid_slot_def cap_links_irq_def) 879 880lemma derive_cap_is_derived_foo': 881 "\<lbrace>\<lambda>s. \<forall>cap'. (cte_wp_at (\<lambda>capa. 882 cap_master_cap capa = cap_master_cap cap \<and> 883 (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and> 884 cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap) 885 slot s \<and> valid_objs s \<and> cap' \<noteq> NullCap 886 \<longrightarrow> cte_at slot s ) 887 \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap') 888 \<and> (cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap) 889 \<longrightarrow> Q cap' s \<rbrace> 890 derive_cap slot cap \<lbrace>Q\<rbrace>,-" 891 apply (clarsimp simp add: validE_R_def validE_def valid_def 892 split: sum.splits) 893 apply (frule in_inv_by_hoareD[OF derive_cap_inv], clarsimp) 894 apply (erule allE) 895 apply (erule impEM) 896 apply (frule use_validE_R[OF _ cap_derive_not_null_helper, OF _ _ imp_refl]) 897 apply (rule derive_cap_inv[THEN valid_validE_R]) 898 apply (intro conjI) 899 apply (clarsimp simp:cte_wp_at_caps_of_state)+ 900 apply (erule(1) use_validE_R[OF _ derive_cap_valid_cap]) 901 apply simp 902 apply (erule use_validE_R[OF _ derive_cap_auth_derived],simp) 903 apply simp 904 done 905 906(* FIXME: cleanup *) 907lemma transfer_caps_loop_presM_extended: 908 fixes P vo em ex buffer slots caps n mi 909 assumes x: "\<And>cap src dest. 910 \<lbrace>\<lambda>s::('state_ext :: state_ext) state . 911 P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> real_cte_at dest s \<and> 912 s \<turnstile> cap \<and> Psrc src \<and> Pdest dest \<and> Pcap cap \<and> 913 tcb_cap_valid cap dest s 914 \<and> real_cte_at src s 915 \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> 916 cap \<noteq> cap.NullCap) 917 \<and> (em \<longrightarrow> cte_wp_at ((=) cap.NullCap) dest s) 918 \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s)\<rbrace> 919 cap_insert cap src dest \<lbrace>\<lambda>rv. P\<rbrace>" 920 assumes eb: "\<And>b n. \<lbrace>P\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. P\<rbrace>" 921 assumes pcap_auth_derived : 922 "\<And>cap cap'. \<lbrakk>auth_derived cap cap'; Pcap cap'\<rbrakk> \<Longrightarrow> Pcap cap" 923 shows "\<lbrace>\<lambda>s. P s \<and> 924 (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> 925 (\<forall>x \<in> set slots. cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s \<and> 926 real_cte_at x s \<and> Pdest x) \<and> 927 (\<forall>x \<in> set caps. valid_cap (fst x) s \<and> Psrc (snd x) \<and> Pcap (fst x) \<and> 928 cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp \<noteq> fst x 929 \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s 930 \<and> real_cte_at (snd x) s)) 931 \<and> (ex \<longrightarrow> (\<forall>x \<in> set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace> 932 transfer_caps_loop ep buffer n caps slots mi 933 \<lbrace>\<lambda>rv. P\<rbrace>" 934 apply (induct caps arbitrary: slots n mi) 935 apply (simp, wp, simp) 936 apply (clarsimp simp add: Let_def split_def whenE_def 937 cong: if_cong list.case_cong split del: if_split) 938 apply (rule hoare_pre) 939 apply (wp eb hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift static_imp_wp 940 | assumption | simp split del: if_split)+ 941 apply (rule cap_insert_assume_null) 942 apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at static_imp_wp)+ 943 apply (rule hoare_vcg_conj_liftE_R) 944 apply (rule derive_cap_is_derived_foo') 945 apply (rule_tac Q' ="\<lambda>cap' s. (vo \<longrightarrow> cap'\<noteq> cap.NullCap \<longrightarrow> 946 cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s) 947 \<and> (cap'\<noteq> cap.NullCap \<longrightarrow> QM s cap')" for QM 948 in hoare_post_imp_R) 949 prefer 2 950 apply clarsimp 951 apply assumption 952 apply (rule hoare_vcg_conj_liftE_R) 953 apply (rule hoare_vcg_const_imp_lift_R) 954 apply (rule derive_cap_is_derived) 955 apply (wp derive_cap_is_derived_foo')+ 956 apply (clarsimp simp: cte_wp_at_caps_of_state 957 ex_cte_cap_to_cnode_always_appropriate_strg 958 real_cte_tcb_valid caps_of_state_valid 959 split del: if_split) 960 apply (clarsimp simp: remove_rights_def caps_of_state_valid 961 neq_Nil_conv cte_wp_at_caps_of_state 962 imp_conjR[symmetric] conj_comms 963 split del: if_split) 964 apply (rule conjI) 965 apply clarsimp 966 apply (case_tac "cap = a",clarsimp) 967 apply (clarsimp simp:masked_as_full_def is_cap_simps) 968 apply (fastforce simp: cap_master_cap_simps split: if_splits) 969 apply (clarsimp split del: if_split) 970 apply (intro conjI) 971 apply (fastforce split: if_split elim!: pcap_auth_derived) 972 apply (fastforce) 973 apply (clarsimp) 974 apply (rule ballI) 975 apply (drule(1) bspec) 976 apply clarsimp 977 apply (intro conjI) 978 apply (case_tac "capa = ac",clarsimp+) 979 apply (case_tac "capa = ac") 980 by (clarsimp simp: masked_as_full_def is_cap_simps split: if_splits)+ 981 982lemma transfer_caps_loop_pas_refined: 983 "\<lbrace>pas_refined aag and valid_objs and valid_mdb 984 and (\<lambda>s. (\<forall>x \<in> set caps. valid_cap (fst x) s \<and> 985 cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s 986 \<and> real_cte_at (snd x) s) \<and> 987 (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s)) 988 and K ((\<forall>slot \<in> set slots. is_subject aag (fst slot)) \<and> 989 (\<forall>x \<in> set caps. is_subject aag (fst (snd x)) \<and> 990 pas_cap_cur_auth aag (fst x)) \<and> distinct slots)\<rbrace> 991 transfer_caps_loop ep buffer n caps slots mi 992 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 993 apply (rule hoare_pre) 994 apply (rule transfer_caps_loop_presM_extended 995 [where vo=True and em=True and ex=False and 996 Psrc="\<lambda>slot . is_subject aag (fst slot)" and 997 Pcap="pas_cap_cur_auth aag" and 998 Pdest="\<lambda>slot . is_subject aag (fst slot)"]) 999 apply (wp cap_insert_pas_refined) 1000 apply (fastforce simp: cte_wp_at_caps_of_state elim!: is_derived_is_transferable) 1001 apply (rule set_extra_badge_pas_refined) 1002 apply (erule(1) auth_derived_pas_cur_auth) 1003 apply (fastforce elim: cte_wp_at_weakenE) 1004 done 1005 1006 1007lemma transfer_caps_pas_refined: 1008 "\<lbrace>pas_refined aag and valid_objs and valid_mdb 1009 and (\<lambda>s. (\<forall>x \<in> set caps. valid_cap (fst x) s \<and> valid_cap (fst x) s \<and> 1010 cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s 1011 \<and> real_cte_at (snd x) s)) 1012 and K (is_subject aag receiver \<and> (\<forall>x \<in> set caps. is_subject aag (fst (snd x))) \<and> (\<forall>x \<in> set caps. pas_cap_cur_auth aag (fst x))) \<rbrace> 1013 transfer_caps info caps endpoint receiver recv_buf 1014 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1015 unfolding transfer_caps_def 1016 apply (rule hoare_pre) 1017 by (wp transfer_caps_loop_pas_refined get_receive_slots_authorised get_recv_slot_inv 1018 hoare_vcg_const_imp_lift hoare_vcg_all_lift grs_distinct 1019 | wpc | simp del: get_receive_slots.simps add: ball_conj_distrib)+ 1020 1021 1022 1023crunch pas_refined[wp]: copy_mrs "pas_refined aag" 1024 (wp: crunch_wps) 1025 1026lemma lookup_cap_and_slot_authorised: 1027 "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> 1028 lookup_cap_and_slot thread xs 1029 \<lbrace>\<lambda>rv s. is_subject aag (fst (snd rv))\<rbrace>, -" 1030 unfolding lookup_cap_and_slot_def 1031 apply (rule hoare_pre) 1032 apply (wp lookup_slot_for_thread_authorised 1033 | simp add: split_def)+ 1034 done 1035 1036lemma lookup_extra_caps_authorised: 1037 "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> 1038 lookup_extra_caps thread buffer mi 1039 \<lbrace>\<lambda>rv s. \<forall>cap \<in> set rv. is_subject aag (fst (snd cap))\<rbrace>, -" 1040 apply (simp add: lookup_extra_caps_def) 1041 apply (wp mapME_set lookup_cap_and_slot_authorised 1042 | simp)+ 1043 done 1044 1045lemma lookup_cap_and_slot_cur_auth: 1046 "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> 1047 lookup_cap_and_slot thread xs 1048 \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag (fst rv)\<rbrace>, -" 1049 unfolding lookup_cap_and_slot_def 1050 apply (rule hoare_pre) 1051 apply (wp get_cap_auth_wp [where aag = aag] lookup_slot_for_thread_authorised 1052 | simp add: split_def)+ 1053 done 1054 1055lemma lookup_extra_caps_auth: 1056 "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> 1057 lookup_extra_caps thread buffer mi 1058 \<lbrace>\<lambda>rv s. \<forall>cap \<in> set rv. pas_cap_cur_auth aag (fst cap)\<rbrace>, -" 1059 apply (simp add: lookup_extra_caps_def) 1060 apply (wp mapME_set lookup_cap_and_slot_cur_auth 1061 | simp)+ 1062 done 1063 1064lemma transfer_caps_empty_inv: 1065 "\<lbrace>P\<rbrace> transfer_caps mi [] endpoint receiver rbuf \<lbrace>\<lambda>_. P\<rbrace>" 1066 unfolding transfer_caps_def 1067 by (wp | wpc | simp) + 1068 1069lemma lcs_valid': 1070 "\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread xs \<lbrace>\<lambda>x s. s \<turnstile> fst x\<rbrace>, -" 1071 unfolding lookup_cap_and_slot_def 1072 apply (rule hoare_pre) 1073 apply wp 1074 apply (simp add: split_def) 1075 apply (wp lookup_slot_for_thread_inv | simp)+ 1076 done 1077 1078lemma lec_valid_cap': 1079 "\<lbrace>valid_objs\<rbrace> lookup_extra_caps thread xa mi \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. s \<turnstile> fst x)\<rbrace>, -" 1080 unfolding lookup_extra_caps_def 1081 by (wpsimp wp: mapME_set lcs_valid') 1082 1083(* FIXME: MOVE *) 1084lemma hoare_conjDR1: 1085 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" 1086 by (simp add:validE_def validE_R_def valid_def) blast 1087 1088lemma hoare_conjDR2: 1089 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-" 1090 by (simp add:validE_def validE_R_def valid_def) blast 1091 1092lemma do_normal_transfer_pas_refined: 1093 "\<lbrace>pas_refined aag 1094 and valid_objs and valid_mdb 1095 and K (grant \<longrightarrow> is_subject aag sender) 1096 and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> 1097 do_normal_transfer sender sbuf endpoint badge grant receiver rbuf 1098 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1099proof(cases grant) 1100 case True thus ?thesis 1101 apply - 1102 apply (rule hoare_gen_asm) 1103 apply (simp add: do_normal_transfer_def) 1104 by (simp 1105 | wp copy_mrs_pas_refined transfer_caps_pas_refined lec_valid_cap' 1106 copy_mrs_cte_wp_at 1107 hoare_vcg_ball_lift 1108 lookup_extra_caps_srcs[simplified ball_conj_distrib,THEN hoare_conjDR1] 1109 lookup_extra_caps_srcs[simplified ball_conj_distrib,THEN hoare_conjDR2] 1110 lookup_extra_caps_authorised lookup_extra_caps_auth lec_valid_cap' 1111 | wpc | simp add:ball_conj_distrib)+ 1112next 1113 case False thus ?thesis 1114 apply (simp add: do_normal_transfer_def) 1115 by (simp 1116 | wp copy_mrs_pas_refined transfer_caps_empty_inv 1117 copy_mrs_cte_wp_at 1118 hoare_vcg_const_imp_lift hoare_vcg_all_lift 1119 | wpc)+ 1120qed 1121 1122crunch pas_refined[wp]: do_fault_transfer "pas_refined aag" 1123 1124lemma do_ipc_transfer_pas_refined: 1125 "\<lbrace>pas_refined aag 1126 and valid_objs and valid_mdb 1127 and K (grant \<longrightarrow> is_subject aag sender) 1128 and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> 1129 do_ipc_transfer sender ep badge grant receiver 1130 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1131 apply (simp add: do_ipc_transfer_def) 1132 apply (wp do_normal_transfer_pas_refined 1133 hoare_vcg_conj_lift hoare_vcg_all_lift 1134 | rule hoare_drop_imps 1135 | wpc)+ 1136 by simp 1137 1138 1139(* FIXME MOVE*) 1140lemma cap_insert_pas_refined_transferable: 1141 "\<lbrace>pas_refined aag and valid_mdb 1142 and K (is_transferable_cap new_cap 1143 \<and> aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap 1144 \<and> (pasObjectAbs aag (fst src_slot), DeleteDerived, pasObjectAbs aag (fst dest_slot)) 1145 \<in> pasPolicy aag) \<rbrace> 1146 cap_insert new_cap src_slot dest_slot 1147 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1148 apply (rule hoare_gen_asm) 1149 apply (simp add: cap_insert_def) 1150 apply (rule hoare_pre) 1151 apply (wp set_cap_pas_refined set_cdt_pas_refined update_cdt_pas_refined hoare_vcg_imp_lift 1152 hoare_weak_lift_imp hoare_vcg_all_lift set_cap_caps_of_state2 1153 set_untyped_cap_as_full_cdt_is_original_cap get_cap_wp 1154 tcb_domain_map_wellformed_lift hoare_vcg_disj_lift 1155 set_untyped_cap_as_full_is_transferable' 1156 | simp split del: if_split del: split_paired_All fun_upd_apply 1157 | strengthen update_one_strg)+ 1158 by (fastforce split: if_split_asm 1159 simp: cte_wp_at_caps_of_state pas_refined_refl valid_mdb_def2 1160 mdb_cte_at_def Option.is_none_def 1161 simp del: split_paired_All 1162 dest: aag_cdt_link_Control aag_cdt_link_DeleteDerived cap_auth_caps_of_state 1163 intro: aag_wellformed_delete_derived_trans[OF _ _ pas_refined_wellformed]) 1164 1165 1166lemma setup_caller_cap_pas_refined: 1167 "\<lbrace>pas_refined aag 1168 and valid_mdb 1169 and K((grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) \<and> 1170 (pasObjectAbs aag receiver, Reply, pasObjectAbs aag sender) \<in> pasPolicy aag )\<rbrace> 1171 setup_caller_cap sender receiver grant 1172 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1173 apply (simp add: setup_caller_cap_def) 1174 apply (rule conjI) 1175 (* if grant *) 1176 apply clarsimp 1177 apply (rule hoare_pre) 1178 apply (wpsimp wp: cap_insert_pas_refined set_thread_state_pas_refined) 1179 apply (fastforce simp: aag_cap_auth_def clas_no_asid cli_no_irqs pas_refined_refl) 1180 (* if not grant *) 1181 apply clarsimp 1182 apply (rule hoare_pre) 1183 apply (wp cap_insert_pas_refined_transferable set_thread_state_pas_refined) 1184 by (fastforce simp: aag_cap_auth_def cap_links_irq_def cap_links_asid_slot_def 1185 cap_auth_conferred_def reply_cap_rights_to_auth_def 1186 intro: aag_wellformed_delete_derived[OF _ pas_refined_wellformed]) 1187 1188(* FIXME: MOVE *) 1189lemma sym_ref_endpoint_recvD: 1190 assumes sym: "sym_refs (state_refs_of s)" 1191 and ep: "ko_at (Endpoint (RecvEP l)) epptr s" 1192 and inl: "t \<in> set l" 1193 shows "\<exists> pl. st_tcb_at ((=) (BlockedOnReceive epptr pl)) t s" 1194proof - 1195 have "(t, EPRecv) \<in> state_refs_of s epptr" 1196 using ep inl by (force simp: state_refs_of_def dest:ko_atD) 1197 hence "(epptr, TCBBlockedRecv) \<in> state_refs_of s t" 1198 using sym by (force dest:sym_refsD[rotated]) 1199 thus ?thesis 1200 by (force simp: st_tcb_at_tcb_states_of_state_eq tcb_states_of_state_def get_tcb_def 1201 state_refs_of_def tcb_st_refs_of_def tcb_bound_refs_def ep_q_refs_of_def 1202 ntfn_q_refs_of_def ntfn_bound_refs_def 1203 split: ntfn.splits endpoint.splits thread_state.splits option.splits 1204 kernel_object.splits) 1205qed 1206 1207lemma pas_refined_ep_recv: 1208 assumes policy: "pas_refined aag s" 1209 and invs: "invs s" 1210 and ep: "ko_at (Endpoint (RecvEP l)) epptr s" 1211 and inl: "t \<in> set l" 1212 shows "(pasObjectAbs aag t, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag" 1213 apply (insert sym_ref_endpoint_recvD[OF invs_sym_refs[OF invs] ep inl]) 1214 apply clarsimp 1215 apply (clarsimp simp:st_tcb_at_tcb_states_of_state_eq) 1216 apply (rule pas_refined_mem[OF _ policy]) 1217 apply (rule sta_ts[of epptr Receive]) 1218 apply (simp add:thread_states_def) 1219 done 1220 1221lemma send_ipc_valid_ep_helper: 1222 "\<lbrakk>invs s ; ko_at (Endpoint (RecvEP (h # t))) epptr s \<rbrakk> \<Longrightarrow> 1223 valid_ep (case t of [] \<Rightarrow> IdleEP | h' # t' \<Rightarrow> RecvEP t) s" 1224 apply (drule invs_valid_objs) 1225 apply (drule ko_atD) 1226 apply (erule(1) valid_objsE) 1227 by (cases t; simp add: valid_obj_def valid_ep_def) 1228 1229lemmas head_in_set = list.set_intros(1)[of h t for h t] 1230 1231 1232lemma send_ipc_pas_refined: 1233 "\<lbrace>pas_refined aag 1234 and invs 1235 and K (is_subject aag thread 1236 \<and> aag_has_auth_to aag SyncSend epptr 1237 \<and> (can_grant_reply \<longrightarrow> aag_has_auth_to aag Call epptr) 1238 \<and> (can_grant \<longrightarrow> aag_has_auth_to aag Grant epptr \<and> aag_has_auth_to aag Call epptr))\<rbrace> 1239 send_ipc block call badge can_grant can_grant_reply thread epptr 1240 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1241 apply (rule hoare_gen_asm) 1242 apply (simp add: send_ipc_def) 1243 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 1244 apply (rule hoare_pre) 1245 apply (wpc | wp set_thread_state_pas_refined)+ 1246 apply (simp add: hoare_if_r_and split del:if_split) 1247 apply (wp setup_caller_cap_pas_refined set_thread_state_pas_refined)+ 1248 apply (simp split del:if_split) 1249 apply (rule_tac Q="\<lambda>rv. valid_mdb 1250 and pas_refined aag and K( 1251 (can_grant \<or> can_grant_reply \<longrightarrow> (reply_can_grant \<longrightarrow> is_subject aag x21) \<and> 1252 (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag))" 1253 in hoare_strengthen_post[rotated]) 1254 apply simp 1255 apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined static_imp_wp gts_wp 1256 | wpc 1257 | simp add: hoare_if_r_and)+ 1258 apply (wp hoare_vcg_all_lift hoare_imp_lift_something | simp add:st_tcb_at_tcb_states_of_state_eq)+ 1259 subgoal for ep s (* post-wp proof *) 1260 apply (intro conjI impI; clarsimp; 1261 frule(2) pas_refined_ep_recv[OF _ _ _ head_in_set]) 1262 1263 subgoal (* can_grant *) 1264 apply (frule(2) aag_wellformed_grant_Control_to_recv[OF _ _ pas_refined_wellformed]) 1265 apply (frule(2) aag_wellformed_reply[OF _ _ pas_refined_wellformed]) 1266 apply (force elim: send_ipc_valid_ep_helper simp:aag_has_auth_to_Control_eq_owns) 1267 done 1268 subgoal (* can_grant_reply and not can_grant*) 1269 apply (frule(2) aag_wellformed_reply[OF _ _ pas_refined_wellformed]) 1270 apply (frule(1) tcb_states_of_state_to_auth) 1271 (* Make the blockedOnReceive state point to epptr *) 1272 apply (frule(1) sym_ref_endpoint_recvD[OF invs_sym_refs _ head_in_set], 1273 clarsimp simp:st_tcb_at_tcb_states_of_state_eq) 1274 apply (fastforce elim: send_ipc_valid_ep_helper 1275 simp: aag_has_auth_to_Control_eq_owns 1276 dest: aag_wellformed_grant_Control_to_recv_by_reply 1277 [OF _ _ _ pas_refined_wellformed]) 1278 done 1279 subgoal (* not can_grant_reply and not can_grant*) 1280 by (force elim: send_ipc_valid_ep_helper) 1281 done 1282 done 1283 1284lemma set_simple_ko_get_tcb: 1285 "\<lbrace>\<lambda>s. P (get_tcb p s)\<rbrace> set_simple_ko f ep epptr \<lbrace>\<lambda>_ s. P (get_tcb p s) \<rbrace>" 1286 unfolding set_simple_ko_def set_object_def 1287 apply (wp get_object_wp) 1288 apply (auto simp: partial_inv_def a_type_def get_tcb_def obj_at_def the_equality 1289 split: Structures_A.kernel_object.splits option.splits) 1290 done 1291 1292lemma get_tcb_is_Some_iff_typ_at: 1293 "(\<exists>y. get_tcb p s = Some y) = typ_at ATCB p s" 1294 by (simp add: tcb_at_typ [symmetric] tcb_at_def) 1295 1296lemma case_list_cons_cong: 1297 "(case xxs of [] \<Rightarrow> f | x # xs \<Rightarrow> g xxs) 1298 = (case xxs of [] \<Rightarrow> f | x # xs \<Rightarrow> g (x # xs))" 1299 by (simp split: list.split) 1300 1301lemma complete_signal_integrity: 1302 "\<lbrace>integrity aag X st and pas_refined aag and valid_objs 1303 and bound_tcb_at ((=) (Some ntfnptr)) thread 1304 and K (is_subject aag thread)\<rbrace> 1305 complete_signal ntfnptr thread 1306 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1307 apply (simp add: complete_signal_def) 1308 apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) 1309 apply (rule hoare_pre) 1310 apply ((wp set_notification_respects[where auth=Receive] set_thread_state_integrity_autarch as_user_integrity_autarch 1311 | wpc 1312 | simp)+)[1] 1313 apply clarsimp 1314 apply (drule_tac t="pasSubject aag" in sym) 1315 apply (fastforce intro!: bound_tcb_at_implies_receive) 1316 done 1317 1318 1319match_abbreviation (input) receive_ipc_base2 1320 in concl receive_ipc_def 1321 select "case_endpoint X Y Z A" (for X Y Z A) 1322 1323abbreviation (input) receive_ipc_base 1324where 1325 "receive_ipc_base aag thread ep epptr rights is_blocking 1326 \<equiv> receive_ipc_base2 thread is_blocking epptr rights ep" 1327 1328 1329lemma sym_ref_endpoint_sendD: 1330 assumes sym: "sym_refs (state_refs_of s)" 1331 and ep: "ko_at (Endpoint (SendEP l)) epptr s" 1332 and inl: "t \<in> set l" 1333 shows "\<exists> pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) t s" 1334proof - 1335 have "(t, EPSend) \<in> state_refs_of s epptr" 1336 using ep inl by (force simp: state_refs_of_def dest:ko_atD) 1337 hence "(epptr, TCBBlockedSend) \<in> state_refs_of s t" 1338 using sym by (force dest:sym_refsD[rotated]) 1339 thus ?thesis 1340 by (force simp: st_tcb_at_tcb_states_of_state_eq tcb_states_of_state_def get_tcb_def 1341 state_refs_of_def tcb_st_refs_of_def tcb_bound_refs_def ep_q_refs_of_def 1342 ntfn_q_refs_of_def ntfn_bound_refs_def 1343 split: ntfn.splits endpoint.splits thread_state.splits option.splits 1344 kernel_object.splits) 1345qed 1346 1347lemma receive_ipc_valid_ep_helper: 1348 "\<lbrakk> invs s; ko_at (Endpoint (SendEP list)) epptr s \<rbrakk> \<Longrightarrow> 1349 valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl list)) s" 1350 apply (drule_tac invs_valid_objs) 1351 apply (drule ko_atD) 1352 apply (erule(1) valid_objsE) 1353 apply (cases list, solves \<open>simp add: valid_obj_def valid_ep_def\<close>) 1354 by (cases "tl list"; clarsimp simp:valid_obj_def valid_ep_def) 1355 1356lemma receive_ipc_sender_helper: 1357 "\<lbrakk>pas_refined aag s ; kheap s thread = Some (TCB tcb) ; tcb_state tcb = BlockedOnSend ep pl\<rbrakk> 1358 \<Longrightarrow> (pasObjectAbs aag thread, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag" 1359 apply (erule pas_refined_mem[rotated]) 1360 apply (rule sta_ts) 1361 apply (simp add: thread_states_def tcb_states_of_state_def get_tcb_def) 1362 done 1363 1364lemma receive_ipc_sender_can_grant_helper: 1365 "\<lbrakk>invs s; pas_refined aag s ; kheap s thread = Some (TCB tcb) ; tcb_state tcb = BlockedOnSend ep pl; 1366 sender_can_grant pl ; aag_has_auth_to aag Receive ep\<rbrakk> 1367 \<Longrightarrow> is_subject aag thread" 1368 apply (frule pas_refined_mem[rotated,where x = "thread" and auth=Grant]) 1369 apply (rule sta_ts) 1370 apply (simp add:thread_states_def tcb_states_of_state_def get_tcb_def) 1371 apply (frule(2) aag_wellformed_grant_Control_to_send[OF _ _ pas_refined_wellformed]) 1372 apply (simp add:aag_has_auth_to_Control_eq_owns) 1373 done 1374 1375 1376lemma receive_ipc_base_pas_refined: 1377 "\<lbrace>pas_refined aag and invs 1378 and ko_at (Endpoint ep) epptr 1379 and K (is_subject aag thread 1380 \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> 1381 (\<forall> auth \<in> cap_rights_to_auth rights True . aag_has_auth_to aag auth epptr))\<rbrace> 1382 receive_ipc_base aag thread ep epptr rights is_blocking 1383 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1384 (* FIXME: proof structure *) 1385 apply (rule hoare_gen_asm) 1386 apply (clarsimp simp: thread_get_def cong: endpoint.case_cong) 1387 apply (rule hoare_pre) 1388 apply (wp set_thread_state_pas_refined get_simple_ko_wp setup_caller_cap_pas_refined 1389 | wpc | simp add: thread_get_def do_nbrecv_failed_transfer_def split del: if_split)+ 1390 apply (rename_tac list sss data) 1391 apply (rule_tac Q="\<lambda>rv s. pas_refined aag s \<and> valid_mdb s \<and> 1392 (sender_can_grant data \<longrightarrow> is_subject aag (hd list)) \<and> 1393 (sender_can_grant_reply data \<longrightarrow> 1394 (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and> 1395 (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag)" 1396 in hoare_strengthen_post[rotated]) 1397 apply (fastforce simp: cap_auth_conferred_def pas_refined_all_auth_is_owns 1398 pas_refined_refl) 1399 apply (wp static_imp_wp do_ipc_transfer_pas_refined set_simple_ko_pas_refined 1400 set_thread_state_pas_refined get_simple_ko_wp hoare_vcg_all_lift 1401 hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1] 1402 | wpc 1403 | simp add: thread_get_def get_thread_state_def do_nbrecv_failed_transfer_def)+ 1404 apply (clarsimp simp: tcb_at_def [symmetric] tcb_at_st_tcb_at) 1405 subgoal premises prems for s 1406 proof - 1407 have "\<And>P Q R. \<lbrakk> R ; P \<Longrightarrow> R \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> (\<not>P \<longrightarrow> R)" by blast 1408 thus ?thesis 1409 apply this 1410 using prems 1411 apply clarsimp 1412 subgoal premises prems for list ep' pl 1413 proof - 1414 have "sender_can_grant pl \<Longrightarrow> is_subject aag (hd list)" 1415 using prems 1416 apply (clarsimp elim!: tcb_atE simp:tcb_at_st_tcb_at[symmetric] get_tcb_def) 1417 apply (frule(1) sym_ref_endpoint_sendD[OF invs_sym_refs,where t= "hd list"],force) 1418 apply (clarsimp simp:st_tcb_at_def elim!:obj_atE) 1419 by (rule receive_ipc_sender_can_grant_helper) 1420 moreover have 1421 "sender_can_grant_reply pl \<Longrightarrow> 1422 (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag" 1423 using prems 1424 apply (clarsimp elim!: tcb_atE simp:tcb_at_st_tcb_at[symmetric] get_tcb_def) 1425 apply (frule(1) sym_ref_endpoint_sendD[OF invs_sym_refs,where t= "hd list"],force) 1426 apply (clarsimp simp:st_tcb_at_def elim!:obj_atE) 1427 apply (frule pas_refined_mem[rotated,where x = "(hd list)" and auth=Call]) 1428 apply (rule sta_ts) 1429 apply (simp add:thread_states_def tcb_states_of_state_def get_tcb_def) 1430 by (erule(2) aag_wellformed_reply[OF _ _ pas_refined_wellformed]) 1431 ultimately show ?thesis 1432 using prems by (force dest:receive_ipc_valid_ep_helper) 1433 qed 1434 apply clarsimp 1435 using prems 1436 apply (intro conjI;clarsimp simp add:cap_rights_to_auth_def) 1437 apply (clarsimp elim!: tcb_atE simp:tcb_at_st_tcb_at[symmetric] get_tcb_def 1438 cap_rights_to_auth_def) 1439 apply (frule_tac t="hd x" in sym_ref_endpoint_sendD[OF invs_sym_refs],assumption,force) 1440 apply (clarsimp simp:st_tcb_at_def elim!:obj_atE) 1441 apply (frule_tac x="hd x" in pas_refined_mem[rotated,where auth=Call]) 1442 apply (rule sta_ts) 1443 apply (simp add:thread_states_def tcb_states_of_state_def get_tcb_def) 1444 apply (frule aag_wellformed_grant_Control_to_send_by_reply[OF _ _ _ pas_refined_wellformed]) 1445 by (force simp:aag_has_auth_to_Control_eq_owns)+ 1446 qed 1447 done 1448 1449lemma complete_signal_pas_refined: 1450 "\<lbrace>pas_refined aag and bound_tcb_at ((=) (Some ntfnptr)) thread\<rbrace> 1451 complete_signal ntfnptr thread 1452 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1453 apply (simp add: complete_signal_def) 1454 apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) 1455 apply (rule hoare_pre) 1456 apply (wp set_simple_ko_pas_refined set_thread_state_pas_refined 1457 | wpc)+ 1458 apply clarsimp 1459 done 1460 1461lemma receive_ipc_pas_refined: 1462 "\<lbrace>pas_refined aag 1463 and invs 1464 and K (is_subject aag thread 1465 \<and> pas_cap_cur_auth aag ep_cap \<and> AllowRead \<in> cap_rights ep_cap)\<rbrace> 1466 receive_ipc thread ep_cap is_blocking 1467 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1468 apply (rule hoare_gen_asm) 1469 apply (simp add: receive_ipc_def thread_get_def split: cap.split) 1470 apply clarsimp 1471 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 1472 apply (rule hoare_seq_ext[OF _ gbn_sp]) 1473 apply (case_tac ntfnptr, simp_all) 1474 (* old receive_ipc stuff *) 1475 apply (rule hoare_pre) 1476 apply (wp receive_ipc_base_pas_refined)[1] 1477 apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def) 1478 (* ntfn-binding case *) 1479 apply clarsimp 1480 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 1481 apply (case_tac "isActive ntfn", simp_all) 1482 apply (wp complete_signal_pas_refined, clarsimp) 1483 (* regular case again *) 1484 apply (rule hoare_pre, wp receive_ipc_base_pas_refined) 1485 apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def) 1486 done 1487 1488 1489subsection \<open>@{term "integrity"}\<close> 1490 1491subsubsection\<open>autarchy\<close> 1492 1493text\<open> 1494 1495 For the case when the currently-running thread owns the receiver 1496 (i.e. receiver last to the IPC rendezvous or sender owns receiver). 1497 1498\<close> 1499 1500 1501lemma set_extra_badge_integrity_autarch: 1502 "\<lbrace>(integrity aag X st and 1503 K (is_subject aag thread \<and> 1504 ipc_buffer_has_auth aag thread (Some buf) \<and> 1505 buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)))\<rbrace> 1506 set_extra_badge buf badge n 1507 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 1508 unfolding set_extra_badge_def 1509 by (wp store_word_offs_integrity_autarch) 1510 1511lemma transfer_caps_integrity_autarch: 1512 "\<lbrace>pas_refined aag 1513 and integrity aag X st 1514 and valid_objs and valid_mdb 1515 and (\<lambda> s. (\<forall>x\<in>set caps. 1516 s \<turnstile> fst x) \<and> 1517 (\<forall>x\<in>set caps. 1518 cte_wp_at 1519 (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> 1520 cp = fst x) 1521 (snd x) s \<and> 1522 real_cte_at (snd x) s)) 1523 and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver receive_buffer \<and> 1524 (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6)\<rbrace> 1525 transfer_caps mi caps endpoint receiver receive_buffer 1526 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1527 apply (rule hoare_gen_asm) 1528 apply (simp add: transfer_caps_def) 1529 apply (wpc | wp)+ 1530 apply (rule_tac P = "\<forall>x \<in> set dest_slots. is_subject aag (fst x)" in hoare_gen_asm) 1531 apply (wp transfer_caps_loop_pres_dest cap_insert_integrity_autarch set_extra_badge_integrity_autarch [where aag = aag and thread = receiver] 1532 get_receive_slots_authorised hoare_vcg_all_lift hoare_vcg_imp_lift 1533 | simp add: msg_align_bits buffer_cptr_index_def msg_max_length_def cte_wp_at_caps_of_state 1534 | blast)+ 1535 done 1536 1537(* FIXME: duplicate somehow *) 1538lemma load_word_offs_inv[wp]: 1539 "\<lbrace>P\<rbrace> load_word_offs buf off \<lbrace>\<lambda>rv. P\<rbrace>" 1540 apply (simp add: load_word_offs_def do_machine_op_def split_def) 1541 apply wp 1542 apply clarsimp 1543 apply (drule in_inv_by_hoareD[OF loadWord_inv]) 1544 apply simp 1545 done 1546 1547lemma copy_mrs_integrity_autarch: 1548 "\<lbrace>pas_refined aag and integrity aag X st and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver rbuf \<and> unat n < 2 ^ (msg_align_bits - 2))\<rbrace> 1549 copy_mrs sender sbuf receiver rbuf n 1550 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1551 apply (rule hoare_gen_asm) 1552 apply (simp add: copy_mrs_def cong: if_cong split del: if_split) 1553 apply (wp mapM_wp' as_user_integrity_autarch 1554 store_word_offs_integrity_autarch [where aag = aag and thread = receiver] 1555 | wpc 1556 | simp 1557 | fastforce simp: length_msg_registers msg_align_bits split: if_split_asm)+ 1558 done 1559 1560(* FIXME: Why was the [wp] attribute clobbered by interpretation of the Arch locale? *) 1561declare as_user_thread_bound_ntfn[wp] 1562 1563lemma get_mi_valid': 1564 "\<lbrace>\<top>\<rbrace> get_message_info a \<lbrace>\<lambda>rv s. valid_message_info rv\<rbrace>" 1565 apply (simp add: get_message_info_def) 1566 apply (wp, rule hoare_post_imp, rule data_to_message_info_valid) 1567 apply wp+ 1568 done 1569 1570lemma lookup_extra_caps_length: 1571 "\<lbrace>K (valid_message_info mi)\<rbrace> lookup_extra_caps thread buf mi \<lbrace>\<lambda>rv s. length rv < 6\<rbrace>, -" 1572 unfolding lookup_extra_caps_def 1573 apply (cases buf, simp_all) 1574 apply (wp mapME_length | simp add: comp_def valid_message_info_def msg_max_extra_caps_def word_le_nat_alt)+ 1575 done 1576 1577lemma get_mi_length: 1578 "\<lbrace>\<top>\<rbrace> get_message_info sender \<lbrace>\<lambda>rv s. unat (mi_length rv) < 2 ^ (msg_align_bits - 2)\<rbrace>" 1579 apply (rule hoare_post_imp [OF _ get_mi_valid']) 1580 apply (clarsimp simp: valid_message_info_def msg_align_bits msg_max_length_def word_le_nat_alt) 1581 done 1582 1583lemma do_normal_transfer_send_integrity_autarch: 1584 notes lec_valid_cap[wp del] 1585 shows 1586 "\<lbrace>pas_refined aag 1587 and integrity aag X st 1588 and valid_objs and valid_mdb 1589 and K (is_subject aag receiver \<and> 1590 ipc_buffer_has_auth aag receiver rbuf \<and> 1591 (grant \<longrightarrow> is_subject aag sender))\<rbrace> 1592 do_normal_transfer sender sbuf endpoint badge grant receiver rbuf 1593 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1594 apply (simp add: do_normal_transfer_def) 1595 apply (wp as_user_integrity_autarch set_message_info_integrity_autarch transfer_caps_integrity_autarch 1596 copy_mrs_integrity_autarch 1597 copy_mrs_tcb copy_mrs_cte_wp_at lookup_extra_caps_authorised 1598 lookup_extra_caps_length get_mi_length get_mi_valid' 1599 hoare_vcg_conj_lift hoare_vcg_ball_lift lec_valid_cap' static_imp_wp 1600 | wpc 1601 | simp)+ 1602 done 1603 1604crunch integrity_autarch: setup_caller_cap "integrity aag X st" 1605 1606lemma do_fault_transfer_integrity_autarch: 1607 "\<lbrace>integrity aag X st and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver recv_buf) \<rbrace> 1608 do_fault_transfer badge sender receiver recv_buf 1609 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1610 apply (simp add: do_fault_transfer_def split_def) 1611 apply (wp as_user_integrity_autarch set_message_info_integrity_autarch set_mrs_integrity_autarch 1612 thread_get_wp' 1613 | wpc | simp)+ 1614 done 1615 1616lemma do_ipc_transfer_integrity_autarch: 1617 "\<lbrace>pas_refined aag 1618 and integrity aag X st 1619 and valid_objs and valid_mdb 1620 and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))\<rbrace> 1621 do_ipc_transfer sender ep badge grant receiver 1622 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1623 apply (simp add: do_ipc_transfer_def) 1624 apply (wp do_normal_transfer_send_integrity_autarch do_fault_transfer_integrity_autarch 1625 thread_get_wp' lookup_ipc_buffer_has_auth hoare_vcg_all_lift 1626 | wpc | simp | wp (once) hoare_drop_imps)+ 1627 done 1628 1629lemma set_thread_state_running_respects: 1630 "\<lbrace>integrity aag X st 1631 and (\<lambda>s. \<exists>ep. aag_has_auth_to aag Receive ep 1632 \<and> st_tcb_at (send_blocked_on ep) sender s)\<rbrace> 1633 set_thread_state sender Structures_A.Running 1634 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 1635 apply (simp add: set_thread_state_def) 1636 apply (wpsimp wp: set_object_wp) 1637 apply (erule integrity_trans) 1638 apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def) 1639 apply (clarsimp dest!: get_tcb_SomeD) 1640 apply (rule_tac new_st=Running in tro_tcb_receive) 1641 apply (auto simp: tcb_bound_notification_reset_integrity_def) 1642 done 1643 1644(* FIXME move *) 1645lemma set_simple_ko_obj_at: 1646 "\<lbrace>obj_at P ptr and K (ptr \<noteq> epptr)\<rbrace> 1647 set_simple_ko f epptr ep 1648 \<lbrace>\<lambda>rv. obj_at P ptr\<rbrace>" 1649 apply (simp add: set_simple_ko_def set_object_def) 1650 apply (wp get_object_wp) 1651 apply (auto simp: obj_at_def) 1652 done 1653 1654(* ep is free here *) 1655lemma sts_receive_Inactive_respects: 1656 "\<lbrace>integrity aag X st and st_tcb_at (send_blocked_on ep) thread 1657 and (\<lambda>s. \<forall>tcb. get_tcb thread s = Some tcb \<longrightarrow> call_blocked ep (tcb_state tcb)) 1658 and K (aag_has_auth_to aag Receive ep)\<rbrace> 1659 set_thread_state thread Structures_A.thread_state.Inactive 1660 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 1661 apply (simp add: set_thread_state_def set_object_def get_object_def) 1662 apply wp 1663 apply clarsimp 1664 apply (erule integrity_trans) 1665 apply (clarsimp simp: integrity_def) 1666 apply (drule get_tcb_SomeD) 1667 apply (rule_tac new_st=Inactive in tro_tcb_receive, simp_all) 1668 apply (fastforce simp add: st_tcb_at_def obj_at_def) 1669 done 1670 1671crunch pred_tcb: do_ipc_transfer "pred_tcb_at proj P t" 1672 (wp: crunch_wps transfer_caps_loop_pres make_fault_message_inv simp: zipWithM_x_mapM) 1673 1674lemma set_untyped_cap_as_full_not_untyped: 1675 "\<lbrace> P and K(\<not> is_untyped_cap cap') \<rbrace> 1676 set_untyped_cap_as_full cap cap' slot 1677 \<lbrace> \<lambda>rv. P\<rbrace>" 1678 unfolding set_untyped_cap_as_full_def 1679 apply wp 1680 apply (rule hoare_pre_cont) 1681 apply wpsimp+ 1682 done 1683 1684 1685lemma cap_insert_integrity_autarch_not_untyped: 1686 "\<lbrace>integrity aag X st and 1687 K (\<not> is_untyped_cap cap \<and> is_subject aag (fst dest_slot))\<rbrace> 1688 cap_insert cap src_slot dest_slot 1689 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 1690 apply (simp add:cap_insert_def) 1691 apply (wp set_original_integrity_autarch cap_insert_ext_extended.list_integ_lift 1692 cap_insert_list_integrity update_cdt_fun_upd_integrity_autarch gets_inv 1693 set_cap_integrity_autarch set_untyped_cap_as_full_not_untyped assert_inv) 1694 apply fastforce 1695 done 1696 1697(* FIXME MOVE*) 1698lemma pred_tcb_atE: 1699 assumes hyp: "pred_tcb_at proj pred t s" 1700 obtains tcb where "kheap s t = Some (TCB tcb)" and " pred (proj (tcb_to_itcb tcb))" 1701 using hyp by (fastforce elim:obj_atE simp:pred_tcb_at_def) 1702 1703 1704lemma set_thread_state_blocked_on_reply_respects: 1705 "\<lbrace> integrity aag X st and 1706 st_tcb_at (send_blocked_on ep) thread and 1707 pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) thread 1708 and K(aag_has_auth_to aag Receive ep)\<rbrace> 1709 set_thread_state thread BlockedOnReply 1710 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 1711 apply (rule hoare_gen_asm) 1712 apply (rule hoare_pre) 1713 apply (simp add: set_thread_state_def set_object_def get_object_def) 1714 apply wp 1715 apply clarsimp 1716 apply (erule integrity_trans) 1717 apply (clarsimp simp:integrity_def dest!:get_tcb_SomeD elim!: pred_tcb_atE) 1718 apply (rule tro_tcb_receive[where new_st=BlockedOnReply]) 1719 by fastforce+ 1720 1721lemma setup_caller_cap_integrity_recv: 1722 "\<lbrace>integrity aag X st and valid_mdb 1723 and st_tcb_at (send_blocked_on ep) sender and 1724 pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) sender 1725 and K (aag_has_auth_to aag Receive ep \<and> is_subject aag receiver 1726 \<and> (grant \<longrightarrow> is_subject aag sender))\<rbrace> 1727 setup_caller_cap sender receiver grant 1728 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1729 apply (rule hoare_gen_asm) 1730 apply (rule hoare_pre) 1731 apply (unfold setup_caller_cap_def) 1732 apply (wp cap_insert_integrity_autarch_not_untyped set_thread_state_blocked_on_reply_respects) 1733 by fastforce 1734 1735lemma pred_tcb_atI: 1736 "\<lbrakk>kheap s t = Some (TCB tcb) ;pred (proj (tcb_to_itcb tcb))\<rbrakk> \<Longrightarrow> pred_tcb_at proj pred t s" 1737 by (fastforce simp:pred_tcb_at_def obj_at_def) 1738 1739(* FIXME MOVE *) 1740abbreviation 1741 sender_can_call :: "sender_payload \<Rightarrow> bool" 1742where 1743 "sender_can_call pl \<equiv> sender_can_grant pl \<or> sender_can_grant_reply pl" 1744 1745lemma receive_ipc_base_integrity: 1746 notes do_nbrecv_failed_transfer_def[simp] 1747 shows "\<lbrace>pas_refined aag and integrity aag X st and invs 1748 and ko_at (Endpoint ep) epptr 1749 and K (is_subject aag receiver 1750 \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag 1751 \<and> (\<forall>auth \<in> cap_rights_to_auth rights True. aag_has_auth_to aag auth epptr))\<rbrace> 1752 receive_ipc_base aag receiver ep epptr rights is_blocking 1753 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1754 apply (rule hoare_gen_asm) 1755 apply (clarsimp simp: thread_get_def get_thread_state_def cong: endpoint.case_cong) 1756 apply (rule hoare_pre) 1757 apply (wp set_endpoinintegrity set_thread_state_running_respects 1758 setup_caller_cap_integrity_recv[where ep = epptr] 1759 do_ipc_transfer_integrity_autarch 1760 set_thread_state_integrity_autarch[where param_a=receiver] 1761 sts_receive_Inactive_respects[where ep = epptr] 1762 as_user_integrity_autarch 1763 | wpc | simp)+ 1764 apply (rename_tac list tcb data) 1765 apply (rule_tac Q="\<lambda>rv s. integrity aag X st s 1766 \<and> valid_mdb s 1767 \<and> is_subject aag receiver 1768 \<and> (sender_can_call data \<longrightarrow> AllowGrant \<in> rights 1769 \<longrightarrow> is_subject aag (hd list)) 1770 \<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list)) 1771 \<and> st_tcb_at (send_blocked_on epptr) (hd list) s 1772 \<and> st_tcb_at (\<lambda>st. st = BlockedOnSend epptr data) (hd list) s" 1773 in hoare_strengthen_post[rotated]) 1774 apply (fastforce simp: st_tcb_at_def obj_at_def get_tcb_rev call_blocked_def 1775 allowed_call_blocked_def 1776 dest!: get_tcb_SomeD 1777 elim: pred_tcb_atI) 1778 apply (wp do_ipc_transfer_integrity_autarch do_ipc_transfer_pred_tcb set_endpoinintegrity 1779 get_simple_ko_wp 1780 set_thread_state_integrity_autarch[where param_a=receiver] 1781 hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1] 1782 hoare_vcg_all_lift as_user_integrity_autarch 1783 | wpc | simp)+ 1784 apply clarsimp 1785 apply (subgoal_tac "ep_at epptr s \<and> (\<exists>auth. aag_has_auth_to aag auth epptr 1786 \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))") 1787 prefer 2 1788 apply (fastforce simp: obj_at_def is_ep) 1789 apply simp 1790 apply (thin_tac "ep_at epptr s \<and> (\<exists>auth. aag_has_auth_to aag auth epptr 1791 \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))") 1792 apply (clarsimp simp: st_tcb_def2 a_type_def) 1793 apply (frule_tac t="hd x" in sym_ref_endpoint_sendD[OF invs_sym_refs],assumption,force) 1794 apply (clarsimp simp: get_tcb_def elim!: pred_tcb_atE) 1795 apply (intro conjI; 1796 (force elim: receive_ipc_valid_ep_helper receive_ipc_sender_can_grant_helper)?) 1797 apply (intro impI) 1798 apply (frule_tac x= "hd x" in pas_refined_mem[rotated,where auth=Call]) 1799 apply (rule sta_ts) 1800 apply (simp add: thread_states_def tcb_states_of_state_def get_tcb_def) 1801 apply (simp add: cap_rights_to_auth_def) 1802 apply (rule aag_has_auth_to_Control_eq_owns[THEN iffD1],assumption) 1803 apply (erule aag_wellformed_grant_Control_to_send_by_reply[OF _ _ _ pas_refined_wellformed];force) 1804 done 1805 1806lemma receive_ipc_integrity_autarch: 1807 "\<lbrace>pas_refined aag and integrity aag X st and invs 1808 and K (is_subject aag receiver 1809 \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap)\<rbrace> 1810 receive_ipc receiver cap is_blocking 1811 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1812 apply (rule hoare_gen_asm) 1813 apply (simp add: receive_ipc_def split: cap.splits) 1814 apply clarsimp 1815 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 1816 apply (rule hoare_seq_ext[OF _ gbn_sp]) 1817 apply (case_tac ntfnptr, simp_all) 1818 (* old receive case, not bound *) 1819 apply (rule hoare_pre, wp receive_ipc_base_integrity) 1820 apply (fastforce simp:aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def) 1821 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 1822 apply (case_tac "isActive ntfn", simp_all) 1823 (* new ntfn-binding case *) 1824 apply (rule hoare_pre, wp complete_signal_integrity, clarsimp) 1825 (* old receive case, bound ntfn not active *) 1826 apply (rule hoare_pre, wp receive_ipc_base_integrity) 1827 apply (fastforce simp:aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def) 1828 done 1829 1830subsubsection\<open>Non-autarchy: the sender is running\<close> 1831 1832text\<open> 1833 1834 If the sender is running (i.e. last to the IPC rendezvous) then we 1835 need this auxiliary machinery to show that the sequence of TCB 1836 updates ends up in the tcb_send, tcb_call or tcb_reply case of @{term integrity_obj}. 1837 1838 This machinery is used for both send_ipc and do_reply_transfer 1839 1840 The sender can update an IPC receiver's context as much as it likes, 1841 provided it eventually changes the thread state to Running. 1842 1843\<close> 1844 1845datatype tcb_respects_state = TRContext | TRFinal | TRFinalOrCall | TRReplyContext 1846 1847inductive 1848 tcb_in_ipc for aag tst l' epptr ko ko' 1849where 1850 tii_lrefl: "\<lbrakk> l' = pasSubject aag \<rbrakk> \<Longrightarrow> tcb_in_ipc aag tst l' epptr ko ko'" 1851| tii_context: "\<lbrakk> ko = Some (TCB tcb); 1852 ko' = Some (TCB tcb'); 1853 can_receive_ipc (tcb_state tcb); 1854 \<exists>ctxt'. tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>; 1855 tst = TRContext\<rbrakk> 1856 \<Longrightarrow> tcb_in_ipc aag tst l' epptr ko ko'" 1857| tii_final: "\<lbrakk> ko = Some (TCB tcb); 1858 ko' = Some (TCB tcb'); 1859 receive_blocked_on epptr (tcb_state tcb); 1860 \<exists>ctxt'. tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb) 1861 , tcb_state := Structures_A.Running\<rparr>; 1862 aag_has_auth_to aag SyncSend epptr; 1863 tst = TRFinal \<or> tst = TRFinalOrCall\<rbrakk> 1864 \<Longrightarrow> tcb_in_ipc aag tst l' epptr ko ko'" 1865| tii_call: "\<lbrakk> ko = Some (TCB tcb); 1866 ko' = Some (TCB tcb'); 1867 ep_recv_blocked epptr (tcb_state tcb); 1868 \<exists>ctxt'. tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), 1869 tcb_state := Structures_A.Running, 1870 tcb_caller := ReplyCap caller False R\<rparr>; 1871 is_subject aag caller; 1872 aag_has_auth_to aag Call epptr; 1873 tst = TRFinal\<rbrakk> 1874 \<Longrightarrow> tcb_in_ipc aag tst l' epptr ko ko'" 1875| tii_reply: "\<lbrakk> ko = Some (TCB tcb); 1876 ko' = Some (TCB tcb'); 1877 \<exists>ctxt'. tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), 1878 tcb_fault := None, 1879 tcb_state := Structures_A.Running\<rparr>; 1880 (pasSubject aag, Reply, l') \<in> pasPolicy aag; 1881 tcb_state tcb = BlockedOnReply; 1882 tst = TRFinal\<rbrakk> 1883 \<Longrightarrow> tcb_in_ipc aag tst l' epptr ko ko'" 1884 1885lemmas tii_subject[simp] = tii_lrefl [OF refl] 1886 1887definition integrity_tcb_in_ipc 1888 :: "'a PAS \<Rightarrow> obj_ref set \<Rightarrow> obj_ref \<Rightarrow> obj_ref \<Rightarrow> tcb_respects_state \<Rightarrow> 1889 det_ext state \<Rightarrow> det_ext state \<Rightarrow> bool" 1890where 1891 "integrity_tcb_in_ipc aag X thread epptr tst st \<equiv> \<lambda>s. 1892 \<not> is_subject aag thread \<and> pas_refined aag st \<and> 1893 (integrity aag X st (s\<lparr>kheap := (kheap s)(thread := kheap st thread), 1894 machine_state := 1895 (machine_state s)\<lparr>underlying_memory := 1896 (\<lambda>p. if p \<in> auth_ipc_buffers st thread then 1897 underlying_memory (machine_state st) p 1898 else underlying_memory (machine_state s) p) \<rparr>\<rparr>) 1899 \<and> (tcb_in_ipc aag tst (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)))" 1900 1901lemma tcb_context_no_change: 1902 "\<exists>ctxt. tcb = tcb\<lparr> tcb_arch := arch_tcb_context_set ctxt (tcb_arch tcb)\<rparr>" 1903 apply (cases tcb, clarsimp) 1904 apply (case_tac tcb_arch) 1905 apply (auto simp: arch_tcb_context_set_def) 1906 done 1907 1908lemma auth_ipc_buffers_mem_Write: 1909 "\<lbrakk> x \<in> auth_ipc_buffers s thread; pas_refined aag s; valid_objs s; is_subject aag thread \<rbrakk> 1910 \<Longrightarrow> aag_has_auth_to aag Write x" 1911 apply (clarsimp simp add: auth_ipc_buffers_member_def) 1912 apply (drule (1) cap_cur_auth_caps_of_state) 1913 apply simp 1914 apply (clarsimp simp: aag_cap_auth_def cap_auth_conferred_def 1915 vspace_cap_rights_to_auth_def vm_read_write_def 1916 is_page_cap_def 1917 split: if_split_asm) 1918 apply (auto dest: ipcframe_subset_page) 1919 done 1920 1921 1922lemma integrity_tcb_in_ipc_final: 1923 "\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRFinal st s \<rbrakk> \<Longrightarrow> integrity aag X st s" 1924 unfolding integrity_tcb_in_ipc_def 1925 apply clarsimp 1926 apply (erule integrity_trans) 1927 apply (clarsimp simp: integrity_def) 1928 apply (rule conjI) 1929 apply (erule tcb_in_ipc.cases; simp) 1930 apply (fastforce intro!: tro_tcb_send simp: direct_send_def) 1931 apply (fastforce intro!: tro_tcb_call simp: direct_call_def) 1932 apply clarsimp 1933 apply (fastforce intro!: tro_tcb_reply tcb.equality simp: direct_reply_def) 1934 \<comment> \<open>rm\<close> 1935 apply clarsimp 1936 apply (cases "is_subject aag thread") 1937 apply (rule trm_write) 1938 apply (solves\<open>simp\<close>) 1939 \<comment> \<open>doesn't own\<close> 1940 apply (erule tcb_in_ipc.cases, simp_all)[1] 1941 apply clarsimp 1942 apply (rule trm_ipc [where p' = thread]) 1943 apply (simp add: tcb_states_of_state_def get_tcb_def) 1944 apply (simp add: tcb_states_of_state_def get_tcb_def) 1945 apply (simp add: auth_ipc_buffers_def get_tcb_def 1946 split: option.split_asm cap.split_asm arch_cap.split_asm if_split_asm split del: if_split) 1947 apply simp 1948 apply clarsimp 1949 apply (rule trm_ipc [where p' = thread]) 1950 apply (simp add: tcb_states_of_state_def get_tcb_def split:thread_state.splits) 1951 apply (simp add: tcb_states_of_state_def get_tcb_def) 1952 apply (simp add: auth_ipc_buffers_def get_tcb_def 1953 split: option.split_asm cap.split_asm arch_cap.split_asm if_split_asm split del: if_split) 1954 apply simp 1955 apply clarsimp 1956 apply (rule trm_ipc [where p' = thread]) 1957 apply (simp add: tcb_states_of_state_def get_tcb_def split:thread_state.splits) 1958 apply (simp add: tcb_states_of_state_def get_tcb_def) 1959 apply (simp add: auth_ipc_buffers_def get_tcb_def 1960 split: option.split_asm cap.split_asm arch_cap.split_asm if_split_asm split del: if_split) 1961 apply simp 1962 done 1963 1964lemma update_tcb_context_in_ipc: 1965 "\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRContext st s; 1966 get_tcb thread s = Some tcb; 1967 tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>\<rbrakk> 1968 \<Longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRContext st 1969 (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)" 1970 unfolding integrity_tcb_in_ipc_def 1971 apply (elim conjE) 1972 apply (intro conjI) 1973 apply assumption+ 1974 apply (erule integrity_trans) 1975 apply (simp cong: if_cong) 1976 apply clarsimp 1977 apply (erule tcb_in_ipc.cases, simp_all) 1978 apply (auto intro!: tii_context[OF refl refl] tii_lrefl[OF refl] tcb_context_no_change 1979 dest!: get_tcb_SomeD simp: arch_tcb_context_set_def) 1980 done 1981 1982 1983lemma update_tcb_state_in_ipc: 1984 "\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRContext st s; 1985 receive_blocked_on epptr (tcb_state tcb); aag_has_auth_to aag SyncSend epptr; 1986 get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Structures_A.thread_state.Running\<rparr> \<rbrakk> 1987 \<Longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRFinalOrCall st 1988 (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)" 1989 unfolding integrity_tcb_in_ipc_def 1990 apply (elim conjE) 1991 apply (intro conjI) 1992 apply assumption+ 1993 apply (erule integrity_trans) 1994 apply (simp cong: if_cong) 1995 apply clarsimp 1996 apply (erule tcb_in_ipc.cases, simp_all) 1997 apply (drule get_tcb_SomeD) 1998 apply (rule tii_final[OF refl refl]) 1999 apply (solves\<open>clarsimp\<close>) 2000 apply (elim exE, intro exI tcb.equality; solves \<open>simp\<close>) 2001 apply fastforce 2002 apply fastforce 2003 done 2004 2005lemma as_user_respects_in_ipc: 2006 "\<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace> 2007 as_user thread m 2008 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>" 2009 apply (simp add: as_user_def set_object_def get_object_def) 2010 apply (wp gets_the_wp get_wp put_wp mapM_x_wp' 2011 | wpc 2012 | simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def)+ 2013 apply (clarsimp simp: st_tcb_def2 tcb_at_def fun_upd_def[symmetric]) 2014 apply (auto elim: update_tcb_context_in_ipc) 2015 done 2016 2017lemma set_message_info_respects_in_ipc: 2018 "\<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace> 2019 set_message_info thread m 2020 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>" 2021 unfolding set_message_info_def 2022 by (wp as_user_respects_in_ipc) 2023 2024lemma mul_add_word_size_lt_msg_align_bits_ofnat: 2025 "\<lbrakk> p < 2 ^ (msg_align_bits - 2); k < 4 \<rbrakk> 2026 \<Longrightarrow> of_nat p * of_nat word_size + k < (2 :: word32) ^ msg_align_bits" 2027 unfolding word_size_def 2028 apply simp 2029 apply (rule is_aligned_add_less_t2n[where n=2]) 2030 apply (simp_all add: msg_align_bits word_bits_conv 2031 is_aligned_word_size_2[simplified word_size_def, simplified]) 2032 apply (erule word_less_power_trans_ofnat [where k = 2 and m=9, simplified], simp) 2033 done 2034 2035 2036lemmas ptr_range_off_off_mems = 2037 ptr_range_add_memI [OF _ mul_word_size_lt_msg_align_bits_ofnat] 2038 ptr_range_add_memI [OF _ mul_add_word_size_lt_msg_align_bits_ofnat, 2039 simplified add.assoc [symmetric]] 2040 2041lemma store_word_offs_respects_in_ipc: 2042 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and 2043 K ((\<not> is_subject aag receiver \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits) 2044 \<and> is_aligned buf msg_align_bits \<and> r < 2 ^ (msg_align_bits - 2))\<rbrace> 2045 store_word_offs buf r v 2046 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2047 apply (simp add: store_word_offs_def storeWord_def pred_conj_def) 2048 apply (rule hoare_pre) 2049 apply (wp dmo_wp) 2050 apply (unfold integrity_tcb_in_ipc_def) 2051 apply (elim conjE) 2052 apply (intro impI conjI) 2053 apply assumption+ 2054 apply (erule integrity_trans) 2055 apply (clarsimp simp: ptr_range_off_off_mems integrity_def is_aligned_mask [symmetric] 2056 cong: imp_cong ) 2057 apply simp 2058 done 2059 2060crunch respects_in_ipc: set_extra_badge "integrity_tcb_in_ipc aag X receiver epptr TRContext st" 2061 (wp: store_word_offs_respects_in_ipc) 2062 2063lemma set_object_respects_in_ipc_autarch: 2064 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st 2065 and K (is_subject aag ptr)\<rbrace> 2066 set_object ptr obj 2067 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2068 apply (simp add: integrity_tcb_in_ipc_def) 2069 apply (rule hoare_pre, wp) 2070 apply (wpsimp wp: set_object_wp) 2071 apply (simp only: pred_conj_def) 2072 apply (elim conjE) 2073 apply (intro conjI ; (solves \<open>simp\<close>)?) 2074 apply (erule integrity_trans) 2075 apply (clarsimp simp: integrity_def) 2076 done 2077 2078lemma set_cap_respects_in_ipc_autarch: 2079 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st 2080 and K (is_subject aag (fst ptr))\<rbrace> 2081 set_cap cap ptr 2082 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2083 apply (simp add: set_cap_def split_def) 2084 apply (wp set_object_respects_in_ipc_autarch get_object_wp 2085 | wpc)+ 2086 apply simp 2087 done 2088 2089lemma set_original_respects_in_ipc_autarch: 2090 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st 2091 and K (is_subject aag (fst slot))\<rbrace> 2092 set_original slot orig 2093 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2094 apply (wp set_original_wp) 2095 apply (clarsimp simp: integrity_tcb_in_ipc_def) 2096 apply (simp add: integrity_def 2097 tcb_states_of_state_def get_tcb_def map_option_def 2098 split del: if_split cong: if_cong) 2099 by (fastforce intro :integrity_cdt_direct) 2100 2101lemma update_cdt_fun_upd_respects_in_ipc_autarch: 2102 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st 2103 and K (is_subject aag (fst slot))\<rbrace> 2104 update_cdt (\<lambda>cdt. cdt (slot := v cdt)) 2105 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2106 apply (simp add: update_cdt_def set_cdt_def) 2107 apply wp 2108 apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def 2109 tcb_states_of_state_def get_tcb_def 2110 split del: if_split cong: if_cong) 2111 by (fastforce intro :integrity_cdt_direct) 2112 2113lemma set_untyped_cap_as_full_integrity_tcb_in_ipc_autarch: 2114 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and 2115 K (is_subject aag (fst src_slot))\<rbrace> 2116 set_untyped_cap_as_full src_cap new_cap src_slot 2117 \<lbrace>\<lambda>ya. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2118 apply(rule hoare_pre) 2119 apply(clarsimp simp: set_untyped_cap_as_full_def) 2120 apply(intro conjI impI) 2121 apply (wp set_cap_respects_in_ipc_autarch | simp)+ 2122 done 2123 2124 2125lemma cap_insert_ext_integrity_in_ipc_autarch: 2126 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and K(is_subject aag (fst src_slot)) 2127 and K(is_subject aag (fst dest_slot))\<rbrace> 2128 cap_insert_ext src_parent src_slot dest_slot src_p dest_p 2129 \<lbrace>\<lambda>yd. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2130 apply (rule hoare_gen_asm)+ 2131 apply (simp add: integrity_tcb_in_ipc_def split del: if_split) 2132 apply (unfold integrity_def) 2133 apply (simp only: integrity_cdt_list_as_list_integ) 2134 apply (rule hoare_lift_Pf[where f="ekheap"]) 2135 apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def 2136 tcb_states_of_state_def get_tcb_def 2137 split del: if_split cong: if_cong) 2138 including no_pre 2139 apply wp 2140 apply (rule hoare_vcg_conj_lift) 2141 apply (simp add: list_integ_def del: split_paired_All) 2142 apply (fold list_integ_def) 2143 apply (wp cap_insert_list_integrity | simp | force)+ 2144 done 2145 2146lemma cap_inserintegrity_in_ipc_autarch: 2147 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st 2148 and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot))\<rbrace> 2149 cap_insert new_cap src_slot dest_slot 2150 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2151 apply (rule hoare_gen_asm) 2152 apply (simp add: cap_insert_def cong: if_cong) 2153 apply (rule hoare_pre) 2154 apply (wp set_original_respects_in_ipc_autarch 2155 set_untyped_cap_as_full_integrity_tcb_in_ipc_autarch 2156 update_cdt_fun_upd_respects_in_ipc_autarch 2157 set_cap_respects_in_ipc_autarch get_cap_wp 2158 cap_insert_ext_integrity_in_ipc_autarch 2159 | simp split del: if_split)+ 2160 done 2161 2162lemma transfer_caps_loop_respects_in_ipc_autarch: 2163 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st 2164 and valid_objs and valid_mdb 2165 and (\<lambda>s. (\<forall>slot \<in> set slots. real_cte_at slot s) 2166 \<and> (\<forall>x \<in> set caps. s \<turnstile> fst x 2167 \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s 2168 \<and> real_cte_at (snd x) s)) 2169 and K ((\<forall>cap \<in> set caps. is_subject aag (fst (snd cap))) 2170 \<and> (\<forall>slot \<in> set slots. is_subject aag (fst slot)) 2171 \<and> (\<not> is_subject aag receiver \<longrightarrow> 2172 auth_ipc_buffers st receiver = ptr_range buffer msg_align_bits) 2173 \<and> is_aligned buffer msg_align_bits 2174 \<and> n + length caps < 6 \<and> distinct slots)\<rbrace> 2175 transfer_caps_loop ep buffer n caps slots mi 2176 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2177 apply (rule hoare_gen_asm) 2178 apply (wp transfer_caps_loop_pres_dest cap_inserintegrity_in_ipc_autarch 2179 set_extra_badge_respects_in_ipc 2180 | simp 2181 | simp add: msg_align_bits buffer_cptr_index_def msg_max_length_def 2182 | blast)+ 2183 apply (auto simp: cte_wp_at_caps_of_state) 2184 done 2185 2186lemma transfer_caps_respects_in_ipc: 2187 "\<lbrace>pas_refined aag 2188 and integrity_tcb_in_ipc aag X receiver epptr TRContext st 2189 and valid_objs and valid_mdb 2190 and tcb_at receiver 2191 and (\<lambda>s. (\<forall>x \<in> set caps. s \<turnstile> fst x) 2192 \<and> (\<forall>x \<in> set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s 2193 \<and> real_cte_at (snd x) s)) 2194 and K ((\<not> null caps \<longrightarrow> is_subject aag receiver) 2195 \<and> (\<forall>cap \<in> set caps. is_subject aag (fst (snd cap))) 2196 \<and> (\<not> is_subject aag receiver \<longrightarrow> 2197 case_option True (\<lambda>buf'. auth_ipc_buffers st receiver 2198 = ptr_range buf' msg_align_bits) recv_buf) 2199 \<and> (case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits) recv_buf) 2200 \<and> length caps < 6)\<rbrace> 2201 transfer_caps mi caps endpoint receiver recv_buf 2202 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2203 apply (rule hoare_gen_asm) 2204 apply (cases recv_buf) 2205 apply (simp add: transfer_caps_def, wp, simp) 2206 apply (cases caps) 2207 apply (simp add: transfer_caps_def del: get_receive_slots.simps, wp, simp) 2208 apply (simp add: transfer_caps_def del: get_receive_slots.simps) 2209 apply (wp transfer_caps_loop_respects_in_ipc_autarch 2210 get_receive_slots_authorised 2211 hoare_vcg_all_lift 2212 | wpc 2213 | rule hoare_drop_imps 2214 | simp add: null_def del: get_receive_slots.simps)+ 2215 done 2216 2217lemma copy_mrs_respects_in_ipc: 2218 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st 2219 and K ((\<not> is_subject aag receiver \<longrightarrow> 2220 case_option True (\<lambda>buf'. auth_ipc_buffers st receiver 2221 = ptr_range buf' msg_align_bits) rbuf) 2222 \<and> (case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits) rbuf) 2223 \<and> unat n < 2 ^ (msg_align_bits - 2))\<rbrace> 2224 copy_mrs sender sbuf receiver rbuf n 2225 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2226 unfolding copy_mrs_def 2227 apply (rule hoare_gen_asm) 2228 apply (wp as_user_respects_in_ipc store_word_offs_respects_in_ipc 2229 mapM_wp' 2230 hoare_vcg_const_imp_lift hoare_vcg_all_lift 2231 | wpc 2232 | fastforce split: if_split_asm simp: length_msg_registers)+ 2233 done 2234 2235lemma do_normal_transfer_respects_in_ipc: 2236 notes lec_valid_cap[wp del] 2237 shows 2238 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st 2239 and pas_refined aag 2240 and valid_objs and valid_mdb 2241 and st_tcb_at can_receive_ipc receiver 2242 and (\<lambda>s. grant \<longrightarrow> is_subject aag sender 2243 \<and> is_subject aag receiver) 2244 and K ((\<not> is_subject aag receiver \<longrightarrow> 2245 (case recv_buf of None \<Rightarrow> True 2246 | Some buf' \<Rightarrow> auth_ipc_buffers st receiver 2247 = ptr_range buf' msg_align_bits)) \<and> 2248 (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace> 2249 do_normal_transfer sender sbuf epopt badge grant receiver recv_buf 2250 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2251 apply (simp add: do_normal_transfer_def) 2252 apply (wp as_user_respects_in_ipc set_message_info_respects_in_ipc 2253 transfer_caps_respects_in_ipc copy_mrs_respects_in_ipc get_mi_valid' 2254 lookup_extra_caps_authorised lookup_extra_caps_length get_mi_length 2255 hoare_vcg_const_Ball_lift hoare_vcg_conj_lift_R hoare_vcg_const_imp_lift 2256 lec_valid_cap' 2257 | rule hoare_drop_imps 2258 | simp)+ 2259 apply (auto simp: null_def intro: st_tcb_at_tcb_at) 2260 done 2261 2262lemma set_mrs_respects_in_ipc: 2263 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and 2264 K ((\<not> is_subject aag receiver \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> 2265 (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace> 2266 set_mrs receiver recv_buf msgs 2267 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2268 unfolding set_mrs_def set_object_def get_object_def 2269 apply (rule hoare_gen_asm) 2270 apply (wp mapM_x_wp' store_word_offs_respects_in_ipc 2271 | wpc 2272 | simp split del: if_split add: zipWithM_x_mapM_x split_def)+ 2273 apply (clarsimp simp add: set_zip nth_append simp: msg_align_bits msg_max_length_def 2274 split: if_split_asm) 2275 apply (simp add: length_msg_registers) 2276 apply arith 2277 apply simp 2278 apply wp+ 2279 apply (clarsimp simp: arch_tcb_set_registers_def) 2280 by (rule update_tcb_context_in_ipc [unfolded fun_upd_def]; fastforce) 2281 2282lemma do_fault_transfer_respects_in_ipc: 2283 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and 2284 K ((\<not> is_subject aag receiver \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> 2285 (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace> 2286 do_fault_transfer badge sender receiver recv_buf 2287 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2288 apply (simp add: do_fault_transfer_def split_def) 2289 apply (wp as_user_respects_in_ipc set_message_info_respects_in_ipc set_mrs_respects_in_ipc 2290 | wpc 2291 | simp 2292 | rule hoare_drop_imps)+ 2293 done 2294 2295lemma lookup_ipc_buffer_ptr_range_in_ipc: 2296 "\<lbrace>valid_objs and integrity_tcb_in_ipc aag X thread epptr tst st\<rbrace> 2297 lookup_ipc_buffer True thread 2298 \<lbrace>\<lambda>rv s. \<not> is_subject aag thread \<longrightarrow> 2299 (case rv of None \<Rightarrow> True 2300 | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits) \<rbrace>" 2301 unfolding lookup_ipc_buffer_def 2302 apply (rule hoare_pre) 2303 apply (wp get_cap_wp thread_get_wp' | wpc)+ 2304 apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_auth_def get_tcb_ko_at [symmetric]) 2305 apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"]) 2306 apply (simp add: dom_tcb_cap_cases) 2307 apply (clarsimp simp: auth_ipc_buffers_def get_tcb_ko_at [symmetric] integrity_tcb_in_ipc_def) 2308 apply (drule get_tcb_SomeD) 2309 apply (erule(1) valid_objsE) 2310 apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def case_bool_if 2311 split: if_split_asm) 2312 apply (erule tcb_in_ipc.cases; clarsimp simp: get_tcb_def vm_read_write_def) 2313 done 2314 2315lemma lookup_ipc_buffer_aligned: 2316 "\<lbrace>valid_objs\<rbrace> 2317 lookup_ipc_buffer True thread 2318 \<lbrace>\<lambda>rv s. (case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits) \<rbrace>" 2319 unfolding lookup_ipc_buffer_def 2320 apply (rule hoare_pre) 2321 apply (wp get_cap_wp thread_get_wp' | wpc)+ 2322 apply (clarsimp simp: cte_wp_at_caps_of_state get_tcb_ko_at [symmetric]) 2323 apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"]) 2324 apply (simp add: dom_tcb_cap_cases) 2325 apply (frule (1) caps_of_state_valid_cap) 2326 apply (clarsimp simp: valid_cap_simps cap_aligned_def) 2327 apply (erule aligned_add_aligned) 2328 apply (rule is_aligned_andI1) 2329 apply (drule (1) valid_tcb_objs) 2330 apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def 2331 split: if_splits) 2332 apply (rule order_trans [OF _ pbfs_atleast_pageBits]) 2333 apply (simp add: msg_align_bits pageBits_def) 2334 done 2335 2336lemma do_ipc_transfer_respects_in_ipc: 2337 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st 2338 and pas_refined aag 2339 and valid_objs and valid_mdb 2340 and st_tcb_at can_receive_ipc receiver 2341 and (\<lambda>s. grant \<longrightarrow> is_subject aag sender 2342 \<and> is_subject aag receiver) 2343 \<rbrace> 2344 do_ipc_transfer sender epopt badge grant receiver 2345 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2346 apply (simp add: do_ipc_transfer_def) 2347 apply (wp do_normal_transfer_respects_in_ipc do_fault_transfer_respects_in_ipc 2348 lookup_ipc_buffer_ptr_range_in_ipc lookup_ipc_buffer_aligned 2349 hoare_vcg_conj_lift 2350 | wpc 2351 | simp 2352 | rule hoare_drop_imps)+ 2353 apply (auto intro: st_tcb_at_tcb_at) 2354 done 2355 2356 2357lemma sts_ext_running_noop: 2358 "\<lbrace>P and st_tcb_at (runnable) receiver\<rbrace> set_thread_state_ext receiver \<lbrace>\<lambda>_. P\<rbrace>" 2359 apply (simp add: set_thread_state_ext_def get_thread_state_def thread_get_def 2360 | wp set_scheduler_action_wp)+ 2361 apply (clarsimp simp add: st_tcb_at_def obj_at_def get_tcb_def) 2362 done 2363 2364lemma set_thread_state_running_respects_in_ipc: 2365 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and st_tcb_at(receive_blocked_on epptr) receiver and K(aag_has_auth_to aag SyncSend epptr)\<rbrace> 2366 set_thread_state receiver Structures_A.thread_state.Running 2367 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st\<rbrace>" 2368 apply (simp add: set_thread_state_def) 2369 apply (wpsimp wp: set_object_wp sts_ext_running_noop) 2370 apply (auto simp: st_tcb_at_def obj_at_def get_tcb_def 2371 get_tcb_rev update_tcb_state_in_ipc 2372 cong: if_cong 2373 elim: update_tcb_state_in_ipc[unfolded fun_upd_def]) 2374 done 2375 2376lemma set_endpoinintegrity_in_ipc: 2377 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st 2378 and K (aag_has_auth_to aag SyncSend epptr)\<rbrace> 2379 set_endpoint epptr ep' 2380 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" 2381 apply (simp add: set_simple_ko_def set_object_def) 2382 apply (wp get_object_wp) 2383 apply (clarsimp split: Structures_A.kernel_object.splits 2384 simp: obj_at_def is_tcb is_ep integrity_tcb_in_ipc_def 2385 partial_inv_def a_type_def) 2386 apply (intro impI conjI) 2387 apply (erule integrity_trans) 2388 apply (clarsimp simp: integrity_def) 2389 apply clarsimp 2390 apply (erule tcb_in_ipc.cases, simp_all) 2391 apply (erule integrity_trans) 2392 apply (clarsimp simp: integrity_def) 2393 apply (fastforce intro: tro_ep) 2394 done 2395 2396(* FIXME: move *) 2397lemma valid_ep_recv_dequeue: 2398 "\<lbrakk> ko_at (Endpoint (Structures_A.endpoint.RecvEP (t # ts))) epptr s; 2399 valid_objs s; sym_refs (state_refs_of s) \<rbrakk> 2400 \<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> Structures_A.endpoint.IdleEP 2401 | b # bs \<Rightarrow> Structures_A.endpoint.RecvEP ts) s" 2402 unfolding valid_objs_def valid_obj_def valid_ep_def obj_at_def 2403 apply (drule bspec) 2404 apply (auto split: list.splits) 2405 done 2406 2407lemma integrity_tcb_in_ipc_refl: 2408 "\<lbrakk> st_tcb_at can_receive_ipc receiver s; \<not> is_subject aag receiver; pas_refined aag s\<rbrakk> 2409 \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRContext s s" 2410 unfolding integrity_tcb_in_ipc_def 2411 apply (clarsimp simp: st_tcb_def2) 2412 apply (rule tii_context [OF get_tcb_SomeD get_tcb_SomeD], assumption+) 2413 apply (rule tcb_context_no_change) 2414 apply simp 2415 done 2416 2417(* stronger *) 2418(* MOVE *) 2419lemma ep_queued_st_tcb_at'': 2420 "\<And>P. \<lbrakk>ko_at (Endpoint ep) ptr s; (t, rt) \<in> ep_q_refs_of ep; 2421 valid_objs s; sym_refs (state_refs_of s); 2422 \<And>pl pl'. (rt = EPSend \<and> P (Structures_A.BlockedOnSend ptr pl)) \<or> 2423 (rt = EPRecv \<and> P (Structures_A.BlockedOnReceive ptr pl')) \<rbrakk> 2424 \<Longrightarrow> st_tcb_at P t s" 2425 apply (case_tac ep, simp_all) 2426 apply (frule (1) sym_refs_ko_atD, fastforce simp: st_tcb_at_def obj_at_def refs_of_rev)+ 2427 done 2428 2429subsubsection \<open>Inserting the reply cap\<close> 2430 2431lemma integrity_tcb_in_ipc_no_call: 2432 "integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st s 2433 \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRFinal st s" 2434 unfolding integrity_tcb_in_ipc_def tcb_in_ipc.simps by clarsimp 2435 2436lemma set_original_respects_in_ipc_reply: 2437 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st 2438 and K(st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st)\<rbrace> 2439 set_original (receiver, tcb_cnode_index 3) orig 2440 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2441 apply (wp set_original_wp) 2442 apply (clarsimp simp: integrity_tcb_in_ipc_def) 2443 apply (simp add: integrity_def tcb_states_of_state_def get_tcb_def 2444 split del: if_split cong: if_cong) 2445 apply (fold get_tcb_def tcb_states_of_state_def) 2446 apply (clarsimp simp:st_tcb_at_tcb_states_of_state) 2447 apply (rule integrity_cdt_change_allowed) 2448 apply (rule cca_reply; force) 2449 done 2450 2451lemma cap_insert_ext_integrity_in_ipc_reply: 2452 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st 2453 and K(is_subject aag (fst src_slot) 2454 \<and> st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st)\<rbrace> 2455 cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p 2456 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2457 apply (rule hoare_gen_asm)+ 2458 apply (simp add: integrity_tcb_in_ipc_def split del: if_split) 2459 apply (unfold integrity_def) 2460 apply (simp only: integrity_cdt_list_as_list_integ) 2461 apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def 2462 tcb_states_of_state_def get_tcb_def 2463 split del: if_split cong: if_cong) 2464 apply wp 2465 apply (simp add: list_integ_def del: split_paired_All) 2466 apply (fold list_integ_def get_tcb_def tcb_states_of_state_def) 2467 apply (wp cap_insert_list_integrity) 2468 apply simp 2469 apply (simp add: list_integ_def del: split_paired_All) 2470 apply (fold list_integ_def get_tcb_def tcb_states_of_state_def) 2471 apply (clarsimp simp: st_tcb_at_tcb_states_of_state) 2472 apply (rule cca_reply; force) 2473 done 2474 2475lemma update_cdt_wp: 2476 "\<lbrace>\<lambda>s. P (s\<lparr> cdt := f (cdt s) \<rparr>)\<rbrace> 2477 update_cdt f 2478 \<lbrace>\<lambda>_. P \<rbrace>" 2479 by (wpsimp simp: update_cdt_def set_cdt_def) 2480 2481lemma update_cdt_reply_in_ipc: 2482 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st 2483 and K(st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st)\<rbrace> 2484 update_cdt (\<lambda>cdt. cdt ((receiver, tcb_cnode_index 3) := val cdt)) 2485 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2486 apply (wp update_cdt_wp) 2487 apply (clarsimp simp: integrity_tcb_in_ipc_def) 2488 apply (simp add: integrity_def tcb_states_of_state_def get_tcb_def 2489 split del: if_split cong: if_cong) 2490 apply (fold get_tcb_def tcb_states_of_state_def) 2491 apply (clarsimp simp:st_tcb_at_tcb_states_of_state) 2492 apply (rule integrity_cdt_change_allowed) 2493 apply (rule cca_reply; force) 2494 done 2495 2496(* FIXME: move to NondetMonad *) 2497lemma spec_valid_direct: 2498 "\<lbrakk> P s \<Longrightarrow> s \<turnstile> \<lbrace> \<top> \<rbrace> f \<lbrace> Q \<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace> Q \<rbrace>" 2499 by (simp add: spec_valid_def valid_def) 2500 2501lemma set_cap_respects_in_ipc_reply: 2502 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st 2503 and K(st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st 2504 \<and> is_subject aag caller)\<rbrace> 2505 set_cap (ReplyCap caller False R) (receiver, tcb_cnode_index 3) 2506 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>" 2507 unfolding set_cap_def 2508 apply simp 2509 apply (rule hoare_seq_ext[OF _ get_object_sp]) 2510 including no_pre 2511 apply (wp set_object_wp) 2512 apply (rule use_spec') 2513 apply (rule spec_valid_direct) 2514 apply (clarsimp simp:tcb_at_def get_tcb_def dest!:ko_atD split:kernel_object.splits) 2515 apply (simp add: spec_valid_def valid_def return_def) 2516 unfolding integrity_tcb_in_ipc_def 2517 apply (clarsimp simp:st_tcb_at_tcb_states_of_state ) 2518 apply (clarsimp simp:tcb_states_of_state_def direct_call_def dest!:get_tcb_SomeD) 2519 by (erule tcb_in_ipc.cases; (force intro:tii_call)) 2520 2521 2522lemma cap_insert_reply_cap_respects_in_ipc: 2523 "\<lbrace> integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and 2524 K (st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> 2525 is_subject aag caller \<and> is_subject aag (fst master_slot))\<rbrace> 2526 cap_insert 2527 (ReplyCap caller False R) 2528 master_slot (receiver, tcb_cnode_index 3) 2529 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>" 2530 unfolding cap_insert_def 2531 apply (rule hoare_pre) 2532 apply (wp add:set_original_respects_in_ipc_reply) 2533 apply simp 2534 apply (wp cap_insert_ext_integrity_in_ipc_reply update_cdt_reply_in_ipc 2535 set_cap_respects_in_ipc_reply set_untyped_cap_as_full_not_untyped get_cap_wp)+ 2536 by fastforce 2537 2538lemma set_scheduler_action_respects_in_ipc_autarch: 2539 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> 2540 set_scheduler_action action 2541 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2542 unfolding set_scheduler_action_def 2543 by (wpsimp simp: integrity_tcb_in_ipc_def integrity_def tcb_states_of_state_def get_tcb_def) 2544 2545lemma exists_cons_append: 2546 "\<exists>xs. xs @ ys = zs \<Longrightarrow> \<exists>xs. xs @ ys = z # zs" 2547 by auto 2548 2549lemma tcb_sched_action_respects_in_ipc_autarch: 2550 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> 2551 tcb_sched_action tcb_sched_enqueue target 2552 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2553 apply (simp add: tcb_sched_action_def) 2554 apply wp 2555 apply (clarsimp simp: integrity_def integrity_tcb_in_ipc_def tcb_states_of_state_def get_tcb_def 2556 integrity_ready_queues_def pas_refined_def tcb_domain_map_wellformed_aux_def 2557 tcb_at_def get_etcb_def tcb_sched_enqueue_def etcb_at_def 2558 split: option.splits) 2559 apply (fastforce intro: exists_cons_append) 2560 done 2561 2562 2563crunches possible_switch_to, set_thread_state for respects_in_ipc_autarch: "integrity_tcb_in_ipc aag X receiver epptr ctxt st" 2564 (wp: tcb_sched_action_respects_in_ipc_autarch ignore:tcb_sched_action ) 2565 2566lemma setup_caller_cap_respects_in_ipc_reply: 2567 "\<lbrace> integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st 2568 and K (is_subject aag sender \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st) \<rbrace> 2569 setup_caller_cap sender receiver grant 2570 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st \<rbrace>" 2571 unfolding setup_caller_cap_def 2572 by (wpsimp wp: cap_insert_reply_cap_respects_in_ipc set_thread_state_respects_in_ipc_autarch) 2573 2574 2575lemma send_ipc_integrity_autarch: 2576 "\<lbrace>integrity aag X st and pas_refined aag 2577 and invs 2578 and is_subject aag \<circ> cur_thread 2579 and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r \<in> refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr 2580 and K (is_subject aag sender \<and> aag_has_auth_to aag SyncSend epptr \<and> 2581 (can_grant_reply \<longrightarrow> aag_has_auth_to aag Call epptr))\<rbrace> 2582 send_ipc block call badge can_grant can_grant_reply sender epptr 2583 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 2584 apply (rule hoare_gen_asm) 2585 apply (simp add: send_ipc_def) 2586 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 2587 apply (case_tac ep) 2588 \<comment> \<open>IdleEP\<close> 2589 apply simp 2590 apply (rule hoare_pre) 2591 apply (wp set_endpoinintegrity set_thread_state_integrity_autarch 2592 | wpc | simp)+ 2593 apply (fastforce simp: obj_at_def is_ep) \<comment> \<open>ep_at and has_auth\<close> 2594 \<comment> \<open>SendEP\<close> 2595 apply simp 2596 apply (rule hoare_pre) 2597 apply (wp set_endpoinintegrity set_thread_state_integrity_autarch 2598 | wpc | simp)+ 2599 apply (fastforce simp: obj_at_def is_ep) \<comment> \<open>ep_at and has_auth\<close> 2600 \<comment> \<open>WaitingEP\<close> 2601 apply (rename_tac list) 2602 apply simp 2603 apply (case_tac "is_subject aag (hd list)") \<comment> \<open>autarch or not on receiver side\<close> 2604 apply clarsimp 2605 apply (rule hoare_pre) 2606 apply (wp setup_caller_cap_integrity_autarch set_thread_state_integrity_autarch thread_get_wp' 2607 | wpc)+ 2608 apply (rule_tac Q="\<lambda>rv s. integrity aag X st s\<and> (can_grant \<longrightarrow> is_subject aag (hd list))" 2609 in hoare_strengthen_post[rotated]) 2610 apply simp+ 2611 apply (wp set_thread_state_integrity_autarch thread_get_wp' 2612 do_ipc_transfer_integrity_autarch 2613 hoare_vcg_all_lift hoare_drop_imps set_endpoinintegrity 2614 | wpc | simp add: get_thread_state_def split del: if_split 2615 del: hoare_True_E_R)+ 2616 apply (fastforce simp: a_type_def obj_at_def is_ep elim: send_ipc_valid_ep_helper) 2617 \<comment> \<open>we don't own head of queue\<close> 2618 apply clarsimp 2619 apply (rule use_spec') \<comment> \<open>Name initial state\<close> 2620 apply (simp add: spec_valid_def) \<comment> \<open>no imp rule?\<close> 2621 apply (rule hoare_pre) 2622 apply (wpc, wp) 2623 apply (rename_tac list s receiver queue) 2624 apply (rule_tac Q = "\<lambda>_ s'. integrity aag X st s \<and> 2625 integrity_tcb_in_ipc aag X receiver epptr TRFinal s s'" in hoare_post_imp) 2626 apply (fastforce dest!: integrity_tcb_in_ipc_final elim!: integrity_trans) 2627 apply (wp setup_caller_cap_respects_in_ipc_reply 2628 set_thread_state_respects_in_ipc_autarch[where param_b = Inactive] 2629 hoare_vcg_if_lift static_imp_wp possible_switch_to_respects_in_ipc_autarch 2630 set_thread_state_running_respects_in_ipc do_ipc_transfer_respects_in_ipc thread_get_inv 2631 set_endpoinintegrity_in_ipc 2632 | wpc 2633 | strengthen integrity_tcb_in_ipc_no_call 2634 | wp hoare_drop_imps 2635 | simp add:get_thread_state_def)+ 2636 2637 apply (clarsimp intro:integrity_tcb_in_ipc_refl) 2638 apply (frule_tac t=x in sym_ref_endpoint_recvD[OF invs_sym_refs],assumption,simp) 2639 apply (clarsimp simp:st_tcb_at_tcb_states_of_state_eq st_tcb_at_tcb_states_of_state direct_call_def) 2640 apply (subgoal_tac "\<not> can_grant") 2641 apply (force intro!: integrity_tcb_in_ipc_refl 2642 simp: st_tcb_at_tcb_states_of_state 2643 elim: send_ipc_valid_ep_helper) 2644 apply (force elim:obj_at_ko_atE) 2645 done 2646 2647section\<open>Faults\<close> 2648 2649(* FIXME: move *) 2650lemma valid_tcb_fault_update: 2651 "\<lbrakk> valid_tcb p t s; valid_fault fault \<rbrakk> \<Longrightarrow> valid_tcb p (t\<lparr>tcb_fault := Some fault\<rparr>) s" 2652 by (simp add: valid_tcb_def ran_tcb_cap_cases) 2653 2654lemma thread_set_fault_pas_refined: 2655 "\<lbrace>pas_refined aag\<rbrace> 2656 thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread 2657 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 2658 apply (wp send_ipc_pas_refined thread_set_pas_refined 2659 thread_set_refs_trivial thread_set_obj_at_impossible 2660 | simp)+ 2661 done 2662 2663lemma owns_ep_owns_receivers': 2664 "\<lbrakk> (\<forall>auth. aag_has_auth_to aag auth epptr); pas_refined aag s; valid_objs s; 2665 sym_refs (state_refs_of s); ko_at (Endpoint ep) epptr s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> 2666 \<Longrightarrow> is_subject aag t" 2667 apply (drule (1) ep_rcv_queued_st_tcb_at [where P = "receive_blocked_on epptr"]) 2668 apply clarsimp 2669 apply clarsimp 2670 apply clarsimp 2671 apply (rule refl) 2672 apply (drule st_tcb_at_to_thread_states) 2673 apply (clarsimp simp: receive_blocked_on_def2) 2674 apply (drule spec [where x = Grant]) 2675 apply (frule aag_wellformed_grant_Control_to_recv [OF _ _ pas_refined_wellformed]) 2676 apply (rule pas_refined_mem [OF sta_ts]) 2677 apply fastforce 2678 apply assumption 2679 apply assumption 2680 apply (erule (1) aag_Control_into_owns) 2681 done 2682 2683lemma send_fault_ipc_pas_refined: 2684 "\<lbrace>pas_refined aag 2685 and invs 2686 and is_subject aag \<circ> cur_thread 2687 and K (valid_fault fault) 2688 and K (is_subject aag thread)\<rbrace> 2689 send_fault_ipc thread fault 2690 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 2691 apply (rule hoare_gen_asm)+ 2692 apply (simp add: send_fault_ipc_def Let_def lookup_cap_def split_def) 2693 apply (wp send_ipc_pas_refined thread_set_fault_pas_refined thread_set_tcb_fault_set_invs 2694 thread_set_refs_trivial thread_set_obj_at_impossible 2695 get_cap_wp thread_set_valid_objs'' 2696 hoare_vcg_conj_lift hoare_vcg_ex_lift hoare_vcg_all_lift 2697 | wpc 2698 | rule hoare_drop_imps 2699 | simp add: split_def split del: if_split)+ 2700 apply (rule_tac Q'="\<lambda>rv s. pas_refined aag s 2701 \<and> is_subject aag (cur_thread s) 2702 \<and> invs s 2703 \<and> valid_fault fault 2704 \<and> is_subject aag (fst (fst rv))" 2705 in hoare_post_imp_R[rotated]) 2706 apply (fastforce dest!: cap_auth_caps_of_state 2707 simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state aag_cap_auth_def 2708 cap_auth_conferred_def cap_rights_to_auth_def AllowSend_def) 2709 apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised 2710 | simp add: lookup_cap_def split_def)+ 2711 done 2712 2713lemma handle_fault_pas_refined: 2714 "\<lbrace>pas_refined aag 2715 and invs 2716 and is_subject aag \<circ> cur_thread 2717 and K (valid_fault fault) 2718 and K (is_subject aag thread)\<rbrace> 2719 handle_fault thread fault 2720 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 2721 apply (simp add: handle_fault_def) 2722 apply (wp set_thread_state_pas_refined send_fault_ipc_pas_refined 2723 | simp add: handle_double_fault_def)+ 2724 done 2725 2726 2727 2728lemma thread_set_tcb_fault_update_valid_mdb: 2729 "\<lbrace>valid_mdb\<rbrace> 2730 thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread 2731 \<lbrace>\<lambda>rv. valid_mdb\<rbrace>" 2732 apply(rule thread_set_mdb) 2733 apply(clarsimp simp: tcb_cap_cases_def) 2734 apply auto 2735 done 2736 2737 2738(* FIXME: MOVE *) 2739lemma obj_at_conj_distrib: 2740 "obj_at (\<lambda>ko. P ko \<and> Q ko) p s = (obj_at (\<lambda>ko. P ko) p s \<and> obj_at (\<lambda>ko. Q ko) p s)" 2741 by (auto simp: obj_at_def) 2742 2743lemma send_fault_ipc_integrity_autarch: 2744 "\<lbrace>pas_refined aag 2745 and invs 2746 and integrity aag X st 2747 and is_subject aag \<circ> cur_thread 2748 and K (valid_fault fault) 2749 and K (is_subject aag thread)\<rbrace> 2750 send_fault_ipc thread fault 2751 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 2752 apply (rule hoare_gen_asm)+ 2753 apply (simp add: send_fault_ipc_def Let_def) 2754 apply (wp send_ipc_integrity_autarch 2755 thread_set_integrity_autarch thread_set_fault_pas_refined 2756 thread_set_valid_objs'' thread_set_refs_trivial 2757 thread_set_tcb_fault_update_valid_mdb 2758 thread_set_tcb_fault_set_invs 2759 | wpc 2760 | simp add: is_obj_defs)+ 2761 (* 14 subgoals *) 2762 apply (rename_tac word1 word2 set) 2763 apply (rule_tac R="\<lambda>rv s. ep_at word1 s" in hoare_post_add) 2764 apply (simp only: obj_at_conj_distrib[symmetric] flip: conj_assoc) 2765 apply (wp thread_set_obj_at_impossible thread_set_tcb_fault_set_invs 2766 get_cap_auth_wp[where aag=aag] 2767 | simp add: lookup_cap_def is_obj_defs split_def)+ 2768 (* down to 3 : normal indentation *) 2769 apply (rule_tac Q'="\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s 2770 \<and> invs s 2771 \<and> valid_fault fault 2772 \<and> is_subject aag (cur_thread s) 2773 \<and> is_subject aag (fst (fst rv))" 2774 in hoare_post_imp_R[rotated]) 2775 apply (clarsimp simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state obj_at_def) 2776 2777 apply (frule(1) caps_of_state_valid) 2778 apply (clarsimp simp: valid_cap_def is_ep aag_cap_auth_def cap_auth_conferred_def 2779 cap_rights_to_auth_def AllowSend_def 2780 elim!: obj_atE) 2781 2782 apply (intro conjI ; fastforce ?) 2783 apply (clarsimp simp:ep_q_refs_of_def split:endpoint.splits) 2784 apply (frule(1) pas_refined_ep_recv, simp add:obj_at_def,assumption) 2785 apply (frule(1) aag_wellformed_grant_Control_to_recv[OF _ _ pas_refined_wellformed,rotated], 2786 blast) 2787 apply (simp add:aag_has_auth_to_Control_eq_owns) 2788 2789 apply (wp lookup_slot_for_thread_authorised)+ 2790 apply simp 2791 done 2792 2793lemma handle_fault_integrity_autarch: 2794 "\<lbrace>pas_refined aag 2795 and integrity aag X st 2796 and is_subject aag \<circ> cur_thread 2797 and invs 2798 and K (valid_fault fault) 2799 and K (is_subject aag thread)\<rbrace> 2800 handle_fault thread fault 2801 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 2802 apply (simp add: handle_fault_def) 2803 apply (wp set_thread_state_integrity_autarch send_fault_ipc_integrity_autarch 2804 | simp add: handle_double_fault_def)+ 2805 done 2806 2807section\<open>Replies\<close> 2808 2809crunch pas_refined[wp]: handle_fault_reply "pas_refined aag" 2810 2811lemma handle_fault_reply_respects: 2812 "\<lbrace>integrity aag X st and K (is_subject aag thread)\<rbrace> 2813 handle_fault_reply fault thread x y 2814 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 2815 apply (cases fault, simp_all) 2816 apply (wp as_user_integrity_autarch 2817 | simp add: handle_arch_fault_reply_def arch_get_sanitise_register_info_def)+ 2818 done 2819 2820lemma tcb_st_to_auth_Restart_Inactive [simp]: 2821 "tcb_st_to_auth (if P then Restart else Inactive) = {}" 2822 by simp 2823 2824 2825lemma do_reply_transfer_pas_refined: 2826 "\<lbrace>pas_refined aag 2827 and invs and K (is_subject aag sender) 2828 and K ((grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))\<rbrace> 2829 do_reply_transfer sender receiver slot grant 2830 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 2831 apply (simp add: do_reply_transfer_def) 2832 apply (rule hoare_pre) 2833 apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined 2834 thread_set_pas_refined K_valid 2835 | wpc 2836 | simp add: thread_get_def split del: if_split)+ 2837 (* otherwise simp does too much *) 2838 apply (rule hoare_strengthen_post, rule gts_inv) 2839 apply (rule impI) 2840 apply assumption 2841 apply auto 2842 done 2843 2844lemma update_tcb_state_in_ipc_reply: 2845 "\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRContext st s; 2846 tcb_state tcb = BlockedOnReply; aag_has_auth_to aag Reply thread; tcb_fault tcb = None; 2847 get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Structures_A.thread_state.Running\<rparr> 2848 \<rbrakk> \<Longrightarrow> 2849 integrity_tcb_in_ipc aag X thread epptr TRFinal st 2850 (s \<lparr> kheap := (kheap s)(thread \<mapsto> TCB tcb') \<rparr>)" 2851 unfolding integrity_tcb_in_ipc_def 2852 apply (elim conjE) 2853 apply (intro conjI) 2854 apply assumption+ 2855 apply (erule integrity_trans) 2856 apply (simp cong: if_cong) 2857 apply clarsimp 2858 apply (erule tcb_in_ipc.cases, simp_all) 2859 apply (drule get_tcb_SomeD) 2860 apply (rule tii_reply[OF refl refl]) 2861 apply (elim exE, intro exI tcb.equality; solves \<open>simp\<close>) 2862 apply auto 2863 done 2864 2865 2866abbreviation "fault_tcb_at \<equiv> pred_tcb_at itcb_fault" 2867 2868lemma fault_tcb_atI: 2869 "\<lbrakk>kheap s ptr = Some (TCB tcb); P (tcb_fault tcb) \<rbrakk> \<Longrightarrow> fault_tcb_at P ptr s" 2870 by (fastforce simp:pred_tcb_at_def obj_at_def) 2871 2872lemma fault_tcb_atE: 2873 assumes hyp:"fault_tcb_at P ptr s" 2874 obtains tcb where "kheap s ptr = Some (TCB tcb)" and "P (tcb_fault tcb)" 2875 using hyp by (fastforce simp:pred_tcb_at_def elim: obj_atE) 2876 2877lemma set_thread_state_running_respects_in_ipc_reply: 2878 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st 2879 and st_tcb_at awaiting_reply receiver 2880 and fault_tcb_at ((=) None) receiver 2881 and K (aag_has_auth_to aag Reply receiver)\<rbrace> 2882 set_thread_state receiver Structures_A.thread_state.Running 2883 \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>" 2884 apply (simp add: set_thread_state_def set_object_def get_object_def) 2885 apply (wp sts_ext_running_noop) 2886 apply (auto simp: st_tcb_at_def obj_at_def get_tcb_def 2887 cong: if_cong 2888 elim!: fault_tcb_atE elim: update_tcb_state_in_ipc_reply[unfolded fun_upd_def]) 2889 done 2890 2891end 2892 2893context is_extended begin 2894 2895interpretation Arch . (*FIXME: arch_split*) 2896 2897lemma list_integ_lift_in_ipc: 2898 assumes li: 2899 "\<lbrace>list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\<rbrace> 2900 f 2901 \<lbrace>\<lambda>_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\<rbrace>" 2902 assumes ekh: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>" 2903 assumes rq: "\<And>P. \<lbrace> \<lambda>s. P (ready_queues s) \<rbrace> f \<lbrace> \<lambda>rv s. P (ready_queues s) \<rbrace>" 2904 shows "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and Q\<rbrace> f \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2905 apply (unfold integrity_tcb_in_ipc_def integrity_def[abs_def]) 2906 apply (simp del:split_paired_All) 2907 apply (rule hoare_pre) 2908 apply (simp only: integrity_cdt_list_as_list_integ) 2909 apply (rule hoare_lift_Pf2[where f="ekheap"]) 2910 apply (simp add: tcb_states_of_state_def get_tcb_def) 2911 apply (wp li[simplified tcb_states_of_state_def get_tcb_def] ekh rq)+ 2912 apply (simp only: integrity_cdt_list_as_list_integ) 2913 apply (simp add: tcb_states_of_state_def get_tcb_def) 2914 done 2915 2916end 2917 2918context begin interpretation Arch . (*FIXME: arch_split*) 2919 2920lemma fast_finalise_reply_respects_in_ipc_autarch: 2921 "\<lbrace> integrity_tcb_in_ipc aag X receiver epptr ctxt st and K (is_reply_cap cap) \<rbrace> 2922 fast_finalise cap final 2923 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>" 2924 by (rule hoare_gen_asm) (fastforce simp: is_cap_simps) 2925 2926lemma empty_slot_list_integrity': 2927 notes split_paired_All[simp del] 2928 shows 2929 "\<lbrace>list_integ P st and (\<lambda>s . cdt_list s slot = []) and K(P slot)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>" 2930 apply (simp add: empty_slot_ext_def split del: if_split) 2931 apply (wp update_cdt_list_wp) 2932 apply (intro impI conjI allI | simp add: list_filter_replace_list list_filter_remove split: option.splits | elim conjE | simp add: list_integ_def)+ 2933 done 2934 2935 2936lemma tcb_state_of_states_cdt_update_behind_kheap[simp]: 2937 "tcb_states_of_state (kheap_update g (cdt_update f s)) = tcb_states_of_state (kheap_update g s)" 2938 by (simp add:tcb_states_of_state_def get_tcb_def) 2939 2940lemma set_cdt_empty_slot_respects_in_ipc_autarch: 2941 "\<lbrace> integrity_tcb_in_ipc aag X receiver epptr ctxt st and (\<lambda>s. m =cdt s) 2942 and (\<lambda>s. descendants_of slot m = {}) and K(is_subject aag (fst slot))\<rbrace> 2943 set_cdt ((\<lambda>p. if m p = Some slot then m slot else m p)(slot := None)) 2944 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>" 2945 unfolding set_cdt_def 2946 apply wp 2947 apply (simp add: integrity_tcb_in_ipc_def integrity_def) 2948 apply (force simp:no_children_empty_desc[symmetric]) 2949 done 2950 2951lemma reply_cap_no_children': 2952 "\<lbrakk> valid_mdb s; caps_of_state s p = Some (ReplyCap t False r) \<rbrakk> \<Longrightarrow> \<forall>p' .cdt s p' \<noteq> Some p" 2953 using reply_cap_no_children .. 2954 2955lemma valid_list_empty: 2956 "\<lbrakk> valid_list_2 list m; descendants_of slot m = {}\<rbrakk> \<Longrightarrow> list slot = []" 2957 unfolding valid_list_2_def 2958 apply (drule no_children_empty_desc[THEN iffD2]) 2959 apply (rule classical) 2960 by (fastforce simp del:split_paired_All split_paired_Ex simp add:neq_Nil_conv) 2961 2962 2963lemma empty_slot_respects_in_ipc_autarch: 2964 "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list 2965 and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))\<rbrace> 2966 empty_slot slot NullCap 2967 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" 2968 unfolding empty_slot_def apply simp 2969 apply (wp add: set_cap_respects_in_ipc_autarch set_original_respects_in_ipc_autarch) 2970 apply (wp empty_slot_extended.list_integ_lift_in_ipc empty_slot_list_integrity') 2971 apply simp 2972 apply wp+ 2973 apply (wp set_cdt_empty_slot_respects_in_ipc_autarch) 2974 apply (simp add: set_cdt_def) 2975 apply wp 2976 apply wp 2977 apply wp 2978 apply (wp get_cap_wp) 2979 apply (clarsimp simp: integrity_tcb_in_ipc_def cte_wp_at_caps_of_state is_cap_simps) 2980 apply (drule(1) reply_cap_no_children') 2981 by (force dest: valid_list_empty simp: no_children_empty_desc simp del: split_paired_All) 2982 2983lemma cte_delete_one_respects_in_ipc_autharch: 2984 "\<lbrace> integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and 2985 cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot)) \<rbrace> 2986 cap_delete_one slot 2987 \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>" 2988 unfolding cap_delete_one_def 2989 apply (wp empty_slot_respects_in_ipc_autarch 2990 fast_finalise_reply_respects_in_ipc_autarch get_cap_wp) 2991 by (fastforce simp:cte_wp_at_caps_of_state is_cap_simps) 2992 2993 2994 2995text \<open>The special case of fault reply need a different machinery than *_in_ipc stuff because, 2996 there is no @{term underlying_memory} modification\<close> 2997 2998datatype tcb_respects_fault_state = TRFContext | TRFRemoveFault | TRFFinal 2999 3000inductive tcb_in_fault_reply for aag tst l' ko ko' 3001where 3002 tifr_lrefl: "\<lbrakk> l' = pasSubject aag \<rbrakk> \<Longrightarrow> tcb_in_fault_reply aag tst l' ko ko'" 3003| tifr_context: "\<lbrakk> ko = Some (TCB tcb); 3004 ko' = Some (TCB tcb'); 3005 \<exists>ctxt'. tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>; 3006 (pasSubject aag, Reply, l') \<in> pasPolicy aag; 3007 tcb_state tcb = BlockedOnReply; 3008 tcb_fault tcb = Some fault; 3009 tst = TRFContext\<rbrakk> 3010 \<Longrightarrow> tcb_in_fault_reply aag tst l' ko ko'" 3011| tifr_remove_fault: "\<lbrakk> ko = Some (TCB tcb); 3012 ko' = Some (TCB tcb'); 3013 \<exists>ctxt'. tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb) 3014 , tcb_fault := None\<rparr>; 3015 (pasSubject aag, Reply, l') \<in> pasPolicy aag; 3016 tcb_state tcb = BlockedOnReply; 3017 tcb_fault tcb = Some fault; 3018 tst = TRFRemoveFault\<rbrakk> 3019 \<Longrightarrow> tcb_in_fault_reply aag tst l' ko ko'" 3020| tifr_reply: "\<lbrakk> ko = Some (TCB tcb); 3021 ko' = Some (TCB tcb'); 3022 \<exists>ctxt'. tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), 3023 tcb_fault := None, 3024 tcb_state := new_st\<rparr>; 3025 new_st = Structures_A.Restart \<or> new_st = Structures_A.Inactive; 3026 (pasSubject aag, Reply, l') \<in> pasPolicy aag; 3027 tcb_state tcb = BlockedOnReply; 3028 tcb_fault tcb = Some fault; 3029 tst = TRFFinal\<rbrakk> 3030 \<Longrightarrow> tcb_in_fault_reply aag tst l' ko ko'" 3031 3032definition integrity_tcb_in_fault_reply :: 3033 "'a PAS \<Rightarrow> obj_ref set \<Rightarrow> obj_ref \<Rightarrow> tcb_respects_fault_state \<Rightarrow> det_ext state 3034 \<Rightarrow> det_ext state \<Rightarrow> bool" 3035where 3036 "integrity_tcb_in_fault_reply aag X thread tst st \<equiv> \<lambda>s. 3037 \<not> is_subject aag thread \<and> pas_refined aag st \<and> \<comment> \<open>more or less convenience\<close> 3038 (integrity aag X st (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>) 3039 \<and> (tcb_in_fault_reply aag tst (pasObjectAbs aag thread) (kheap st thread) (kheap s thread)))" 3040 3041lemma integrity_tcb_in_fault_reply_final: 3042 "\<lbrakk> integrity_tcb_in_fault_reply aag X thread TRFFinal st s \<rbrakk> \<Longrightarrow> integrity aag X st s" 3043 unfolding integrity_tcb_in_fault_reply_def 3044 apply clarsimp 3045 apply (erule integrity_trans) 3046 apply (clarsimp simp: integrity_def) 3047 apply (erule tcb_in_fault_reply.cases; clarsimp) 3048 apply (fastforce intro!:tcb.equality tro_tcb_reply) 3049 done 3050 3051lemma set_scheduler_action_respects_in_fault_reply: 3052 "\<lbrace>integrity_tcb_in_fault_reply aag X receiver ctxt st\<rbrace> 3053 set_scheduler_action action 3054 \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X receiver ctxt st\<rbrace>" 3055 unfolding set_scheduler_action_def 3056 by (wpsimp simp: integrity_tcb_in_fault_reply_def integrity_def 3057 tcb_states_of_state_def get_tcb_def) 3058 3059crunches set_thread_state_ext 3060 for respects_in_fault_reply:"integrity_tcb_in_fault_reply aag X receiver ctxt st" 3061 3062lemma as_user_respects_in_fault_reply: 3063 "\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace> 3064 as_user thread m 3065 \<lbrace>\<lambda>rv. integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>" 3066 apply (simp add: as_user_def) 3067 apply (wpsimp wp: set_object_wp) 3068 apply (clarsimp simp: integrity_tcb_in_fault_reply_def) 3069 apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD) 3070 apply (rule tifr_context[OF refl refl]) 3071 apply (intro exI tcb.equality; simp add: arch_tcb_context_set_def) 3072 by fastforce+ 3073 3074lemma handle_fault_reply_respects_in_fault_reply: 3075 "\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace> 3076 handle_fault_reply f thread label mrs 3077 \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>" 3078 by (cases f; 3079 wpsimp simp: handle_arch_fault_reply_def arch_get_sanitise_register_info_def 3080 wp: as_user_respects_in_fault_reply) 3081 3082lemma thread_set_no_fault_respects_in_fault_reply: 3083 "\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace> 3084 thread_set (\<lambda>tcb. tcb \<lparr> tcb_fault := None \<rparr>) thread 3085 \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace>" 3086 apply (simp add: thread_set_def) 3087 apply (wp set_thread_state_ext_respects_in_fault_reply set_object_wp) 3088 apply (clarsimp simp: integrity_tcb_in_fault_reply_def) 3089 apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD) 3090 apply (rule tifr_remove_fault[OF refl refl]) 3091 apply (intro exI tcb.equality ; simp add: arch_tcb_context_set_def) 3092 by fastforce+ 3093 3094lemma set_thread_state_respects_in_fault_reply: 3095 "tst = Restart \<or> tst = Inactive \<Longrightarrow> 3096 \<lbrace>integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace> 3097 set_thread_state thread tst 3098 \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFFinal st\<rbrace>" 3099 apply (simp add: set_thread_state_def) 3100 apply (wp set_thread_state_ext_respects_in_fault_reply set_object_wp) 3101 apply (clarsimp simp: integrity_tcb_in_fault_reply_def) 3102 apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD) 3103 apply (rule tifr_reply[OF refl refl]) 3104 apply (intro exI tcb.equality; simp add: arch_tcb_context_set_def) 3105 by fastforce+ 3106 3107lemma integrity_tcb_in_fault_reply_refl: 3108 "\<lbrakk> st_tcb_at awaiting_reply receiver s; fault_tcb_at (flip (\<noteq>) None) receiver s; 3109 aag_has_auth_to aag Reply receiver; 3110 \<not> is_subject aag receiver; pas_refined aag s \<rbrakk> 3111 \<Longrightarrow> integrity_tcb_in_fault_reply aag X receiver TRFContext s s" 3112 unfolding integrity_tcb_in_fault_reply_def 3113 apply (clarsimp elim!: pred_tcb_atE) 3114 apply (rule tifr_context[OF refl refl]) 3115 apply (rule tcb_context_no_change) 3116 apply fastforce+ 3117 done 3118 3119lemma emptyable_not_master: 3120 "\<lbrakk> valid_objs s; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap\<rbrakk> 3121 \<Longrightarrow> emptyable slot s" 3122 apply (rule emptyable_cte_wp_atD[rotated 2]) 3123 apply (intro allI impI, assumption) 3124 by (fastforce simp:is_cap_simps cte_wp_at_caps_of_state)+ 3125 3126lemma do_reply_transfer_respects: 3127 "\<lbrace>pas_refined aag 3128 and integrity aag X st 3129 and einvs \<comment> \<open>cap_delete_one\<close> 3130 and tcb_at sender 3131 and cte_wp_at (is_reply_cap_to receiver) slot 3132 and K (is_subject aag sender) 3133 and K (aag_has_auth_to aag Reply receiver) 3134 and K (is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver))\<rbrace> 3135 do_reply_transfer sender receiver slot grant 3136 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 3137 apply (rule hoare_gen_asm)+ 3138 apply (simp add: do_reply_transfer_def thread_get_def get_thread_state_def) 3139 apply (rule hoare_seq_ext[OF _ assert_get_tcb_sp];force?) 3140 apply (rule hoare_seq_ext[OF _ assert_sp]) 3141 apply (rule hoare_seq_ext[OF _ assert_get_tcb_sp];force?) 3142 apply wpc 3143 \<comment> \<open>No fault case\<close> 3144 apply (rule hoare_vcg_if_split[where P= "is_subject aag receiver" and f=f and g=f for f, 3145 simplified if_cancel]) 3146 \<comment> \<open>receiver is a subject\<close> 3147 apply ((wp set_thread_state_integrity_autarch thread_set_integrity_autarch 3148 handle_fault_reply_respects do_ipc_transfer_integrity_autarch 3149 do_ipc_transfer_pas_refined 3150 | simp 3151 | intro conjI impI)+)[1] 3152 \<comment> \<open>receiver is not a subject\<close> 3153 apply (rule use_spec') \<comment> \<open>Name initial state\<close> 3154 apply (simp add: spec_valid_def) \<comment> \<open>no imp rule?\<close> 3155 3156 apply (rule_tac Q = "\<lambda>_ s'. integrity aag X st s \<and> 3157 integrity_tcb_in_ipc aag X receiver _ TRFinal s s'" in hoare_post_imp) 3158 apply (fastforce dest!: integrity_tcb_in_ipc_final elim!: integrity_trans) 3159 apply ((wp possible_switch_to_respects_in_ipc_autarch 3160 set_thread_state_running_respects_in_ipc_reply 3161 cte_delete_one_respects_in_ipc_autharch cap_delete_one_reply_st_tcb_at 3162 do_ipc_transfer_pred_tcb do_ipc_transfer_respects_in_ipc 3163 do_ipc_transfer_non_null_cte_wp_at2 3164 | simp add: is_cap_simps is_reply_cap_to_def 3165 | clarsimp)+)[1] 3166 \<comment> \<open>fault case\<close> 3167 apply (rule hoare_vcg_if_split[where P= "is_subject aag receiver" and f=f and g=f for f, 3168 simplified if_cancel]) 3169 \<comment> \<open>receiver is a subject\<close> 3170 apply ((wp set_thread_state_integrity_autarch thread_set_integrity_autarch 3171 handle_fault_reply_respects 3172 | simp 3173 | intro conjI impI)+)[1] 3174 \<comment> \<open>receiver is not a subject\<close> 3175 apply (rule hoare_seq_ext, simp) 3176 apply (rule use_spec') \<comment> \<open>Name initial state\<close> 3177 apply (simp add: spec_valid_def) \<comment> \<open>no imp rule?\<close> 3178 apply wp 3179 apply (rule_tac Q = "\<lambda>_ s'. integrity aag X st s \<and> 3180 integrity_tcb_in_fault_reply aag X receiver TRFFinal s s'" 3181 in hoare_post_imp) 3182 apply (fastforce dest!: integrity_tcb_in_fault_reply_final elim!: integrity_trans) 3183 apply (wp set_thread_state_respects_in_fault_reply 3184 thread_set_no_fault_respects_in_fault_reply 3185 handle_fault_reply_respects_in_fault_reply 3186 | simp)+ 3187 apply force 3188 apply (strengthen integrity_tcb_in_fault_reply_refl)+ 3189 apply (wp cap_delete_one_reply_st_tcb_at) 3190 3191 \<comment> \<open>the end\<close> 3192 by (force simp: st_tcb_at_tcb_states_of_state cte_wp_at_caps_of_state is_cap_simps 3193 is_reply_cap_to_def 3194 dest!: tcb_states_of_state_kheapD get_tcb_SomeD tcb_atD ko_atD 3195 intro: tcb_atI fault_tcb_atI emptyable_not_master 3196 intro!: integrity_tcb_in_ipc_refl tcb_states_of_state_kheapI 3197 elim!: fault_tcb_atE) 3198 3199 3200lemma reply_from_kernel_integrity_autarch: 3201 "\<lbrace>integrity aag X st and pas_refined aag and valid_objs and K (is_subject aag thread)\<rbrace> 3202 reply_from_kernel thread x 3203 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 3204 apply (simp add: reply_from_kernel_def split_def) 3205 apply (wp set_message_info_integrity_autarch set_mrs_integrity_autarch as_user_integrity_autarch | simp)+ 3206 done 3207 3208end 3209 3210end 3211