1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory DomainSepInv 12imports 13 "Ipc_AC" (* for transfer_caps_loop_pres_dest lec_valid_cap' set_simple_ko_get_tcb thread_set_tcb_fault_update_valid_mdb *) 14 "Lib.WPBang" 15begin 16 17context begin interpretation Arch . (*FIXME: arch_split*) 18 19text {* 20 We define and prove an invariant that is necessary to achieve domain 21 separation on seL4. In its strongest form, we require that all IRQs, other than 22 those for the timer, are inactive, and that no IRQControl or 23 IRQHandler caps are present (to prevent any inactive IRQs from becoming 24 active in the future). 25 26 It always requires that there are no domain caps. 27*} 28 29text {* 30 When @{term irqs} is @{term False} we require that non-timer IRQs are off permanently. 31*} 32definition domain_sep_inv where 33 "domain_sep_inv irqs st s \<equiv> 34 (\<forall> slot. \<not> cte_wp_at ((=) DomainCap) slot s) \<and> 35 (irqs \<or> (\<forall> irq slot. \<not> cte_wp_at ((=) IRQControlCap) slot s 36 \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) slot s 37 \<and> interrupt_states s irq \<noteq> IRQSignal 38 \<and> interrupt_states s irq \<noteq> IRQReserved 39 \<and> interrupt_states s = interrupt_states st))" 40 41definition domain_sep_inv_cap where 42 "domain_sep_inv_cap irqs cap \<equiv> case cap of 43 IRQControlCap \<Rightarrow> irqs 44 | IRQHandlerCap irq \<Rightarrow> irqs 45 | DomainCap \<Rightarrow> False 46 | _ \<Rightarrow> True" 47 48 49lemma cte_wp_at_not_domain_sep_inv_cap: 50 "cte_wp_at (not domain_sep_inv_cap irqs) slot s \<longleftrightarrow> 51 ((irqs \<longrightarrow> False) \<and> 52 (\<not> irqs \<longrightarrow> (cte_wp_at ((=) IRQControlCap) slot s \<or> 53 (\<exists> irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s))) 54 ) 55 \<or> cte_wp_at ((=) DomainCap) slot s" 56 apply(rule iffI) 57 apply(drule cte_wp_at_eqD) 58 apply clarsimp 59 apply(case_tac c, simp_all add: domain_sep_inv_cap_def pred_neg_def) 60 apply(auto elim: cte_wp_at_weakenE split: if_splits) 61 done 62 63lemma domain_sep_inv_def2: 64 "domain_sep_inv irqs st s = 65 ((\<forall> slot. \<not> cte_wp_at ((=) DomainCap) slot s) \<and> 66 (irqs \<or> (\<forall> irq slot. \<not> cte_wp_at ((=) IRQControlCap) slot s 67 \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<and> 68 (irqs \<or> (\<forall> irq. 69 interrupt_states s irq \<noteq> IRQSignal 70 \<and> interrupt_states s irq \<noteq> IRQReserved 71 \<and> interrupt_states s = interrupt_states st)))" 72 apply(fastforce simp: domain_sep_inv_def) 73 done 74 75lemma domain_sep_inv_wp: 76 assumes nctrl: "\<And>slot. \<lbrace>(\<lambda>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s) and P\<rbrace> f \<lbrace>\<lambda>_ s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace>" 77 assumes irq_pres: "\<And>P. \<not> irqs \<Longrightarrow> \<lbrace>(\<lambda>s. P (interrupt_states s)) and R\<rbrace> f \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>" 78 shows "\<lbrace>domain_sep_inv irqs st and P and (\<lambda>s. irqs \<or> R s)\<rbrace> f \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 79 apply (clarsimp simp: domain_sep_inv_def2 valid_def) 80 apply (subst conj_assoc[symmetric]) 81 apply (rule conjI) 82 apply (rule conjI) 83 apply(intro allI) 84 apply(erule use_valid[OF _ hoare_strengthen_post[OF nctrl]]) 85 apply(fastforce simp: cte_wp_at_not_domain_sep_inv_cap) 86 apply(fastforce simp: cte_wp_at_not_domain_sep_inv_cap) 87 apply(fastforce elim!: use_valid[OF _ hoare_strengthen_post[OF nctrl]] simp: cte_wp_at_not_domain_sep_inv_cap) 88 apply(case_tac "irqs") 89 apply blast 90 apply(rule disjI2) 91 apply simp 92 apply(intro allI conjI) 93 apply(erule_tac P1="\<lambda>x. x irq \<noteq> IRQSignal" in use_valid[OF _ irq_pres], assumption) 94 apply blast 95 apply(erule use_valid[OF _ irq_pres], assumption) 96 apply blast 97 apply(erule use_valid[OF _ irq_pres], assumption) 98 apply blast 99 done 100 101lemma domain_sep_inv_triv: 102 assumes cte_pres: "\<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 103 assumes irq_pres: "\<And>P. \<lbrace>\<lambda>s. P (interrupt_states s)\<rbrace> f \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>" 104 shows 105 "\<lbrace>domain_sep_inv irqs st\<rbrace> f \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 106 apply(rule domain_sep_inv_wp[where P="\<top>" and R="\<top>", simplified]) 107 apply(rule cte_pres, rule irq_pres) 108 done 109 110(* FIXME: clagged from FinalCaps *) 111lemma set_object_wp: 112 "\<lbrace> \<lambda> s. P (s\<lparr>kheap := kheap s(ptr \<mapsto> obj)\<rparr>) \<rbrace> 113 set_object ptr obj 114 \<lbrace> \<lambda>_. P \<rbrace>" 115 unfolding set_object_def 116 apply (wp) 117 done 118 119(* FIXME: following 3 lemmas clagged from FinalCaps *) 120lemma set_cap_neg_cte_wp_at_other_helper': 121 "\<lbrakk>oslot \<noteq> slot; 122 ko_at (TCB x) (fst oslot) s; 123 tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr); 124 kheap 125 (s\<lparr>kheap := kheap s(fst oslot \<mapsto> 126 TCB (osetF (\<lambda> x. cap) x))\<rparr>) 127 (fst slot) = 128 Some (TCB tcb); 129 tcb_cap_cases (snd slot) = Some (getF, setF, restr); 130 P (getF tcb)\<rbrakk> \<Longrightarrow> 131 cte_wp_at P slot s" 132 apply(case_tac "fst oslot = fst slot") 133 apply(rule cte_wp_at_tcbI) 134 apply(fastforce split: if_splits simp: obj_at_def) 135 apply assumption 136 apply(fastforce split: if_splits simp: tcb_cap_cases_def dest: prod_eqI) 137 apply(rule cte_wp_at_tcbI) 138 apply(fastforce split: if_splits simp: obj_at_def) 139 apply assumption 140 apply assumption 141 done 142 143lemma set_cap_neg_cte_wp_at_other_helper: 144 "\<lbrakk>\<not> cte_wp_at P slot s; oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s; 145 tcb_cap_cases (snd oslot) = Some (getF, setF, restr)\<rbrakk> \<Longrightarrow> 146 \<not> cte_wp_at P slot (s\<lparr>kheap := kheap s(fst oslot \<mapsto> TCB (setF (\<lambda> x. cap) x))\<rparr>)" 147 apply(rule notI) 148 apply(erule cte_wp_atE) 149 apply(fastforce elim: notE intro: cte_wp_at_cteI split: if_splits) 150 apply(fastforce elim: notE intro: set_cap_neg_cte_wp_at_other_helper') 151 done 152 153 154lemma set_cap_neg_cte_wp_at_other: 155 "oslot \<noteq> slot \<Longrightarrow> \<lbrace> \<lambda> s. \<not> (cte_wp_at P slot s)\<rbrace> set_cap cap oslot \<lbrace> \<lambda>rv s. \<not> (cte_wp_at P slot s) \<rbrace>" 156 apply(rule hoare_pre) 157 unfolding set_cap_def 158 apply(wp set_object_wp get_object_wp | wpc | simp add: split_def)+ 159 apply(intro allI impI conjI) 160 apply(rule notI) 161 apply(erule cte_wp_atE) 162 apply (fastforce split: if_splits dest: prod_eqI elim: notE intro: cte_wp_at_cteI simp: obj_at_def) 163 apply(fastforce split: if_splits elim: notE intro: cte_wp_at_tcbI) 164 apply(auto dest: set_cap_neg_cte_wp_at_other_helper) 165 done 166 167lemma set_cap_neg_cte_wp_at: 168 "\<lbrace>(\<lambda>s. \<not> cte_wp_at P slot s) and K (\<not> P capa)\<rbrace> 169 set_cap capa slota 170 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 171 apply(case_tac "slot = slota") 172 apply simp 173 apply(simp add: set_cap_def set_object_def) 174 apply(rule hoare_pre) 175 apply(wp get_object_wp | wpc)+ 176 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 177 apply(rule hoare_pre) 178 apply(rule set_cap_neg_cte_wp_at_other, simp+) 179 done 180 181lemma domain_sep_inv_cap_IRQControlCap: 182 "\<lbrakk>domain_sep_inv_cap irqs cap; \<not> irqs\<rbrakk> \<Longrightarrow> cap \<noteq> IRQControlCap" 183 apply(auto simp: domain_sep_inv_cap_def) 184 done 185 186lemma domain_sep_inv_cap_IRQHandlerCap: 187 "\<lbrakk>domain_sep_inv_cap irqs cap; \<not> irqs\<rbrakk> \<Longrightarrow> cap \<noteq> IRQHandlerCap irq" 188 apply(auto simp: domain_sep_inv_cap_def) 189 done 190 191lemma set_cap_domain_sep_inv: 192 "\<lbrace>domain_sep_inv irqs st and K (domain_sep_inv_cap irqs cap)\<rbrace> 193 set_cap cap slot 194 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 195 apply(rule hoare_gen_asm) 196 apply(rule hoare_pre) 197 apply(rule domain_sep_inv_wp) 198 apply(wp set_cap_neg_cte_wp_at | simp add: pred_neg_def | blast)+ 199 done 200 201lemma cte_wp_at_domain_sep_inv_cap: 202 "\<lbrakk>domain_sep_inv irqs st s; cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap" 203 apply(case_tac slot) 204 apply(auto simp: domain_sep_inv_def domain_sep_inv_cap_def split: cap.splits) 205 done 206 207lemma weak_derived_irq_handler: 208 "weak_derived (IRQHandlerCap irq) cap \<Longrightarrow> cap = (IRQHandlerCap irq)" 209 apply(auto simp: weak_derived_def copy_of_def same_object_as_def split: cap.splits if_splits arch_cap.splits) 210 done 211 212(* FIXME: move to CSpace_AI *) 213lemma weak_derived_DomainCap: 214 "weak_derived c' c \<Longrightarrow> (c' = cap.DomainCap) = (c = cap.DomainCap)" 215 apply (clarsimp simp: weak_derived_def) 216 apply (erule disjE) 217 apply (clarsimp simp: copy_of_def split: if_split_asm) 218 apply (auto simp: is_cap_simps same_object_as_def 219 split: cap.splits arch_cap.splits)[1] 220 apply simp 221 done 222 223lemma cte_wp_at_weak_derived_domain_sep_inv_cap: 224 "\<lbrakk>domain_sep_inv irqs st s; cte_wp_at (weak_derived cap) slot s\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap" 225 apply (cases slot) 226 apply (force simp: domain_sep_inv_def domain_sep_inv_cap_def 227 split: cap.splits 228 dest: cte_wp_at_eqD weak_derived_irq_handler weak_derived_DomainCap) 229 done 230 231lemma is_derived_IRQHandlerCap: 232 "is_derived m src (IRQHandlerCap irq) cap \<Longrightarrow> (cap = IRQHandlerCap irq)" 233 apply(clarsimp simp: is_derived_def) 234 apply(case_tac cap, simp_all add: is_cap_simps cap_master_cap_def) 235 done 236 237(* FIXME: move to CSpace_AI *) 238lemma DomainCap_is_derived: 239 "is_derived m src cap.DomainCap cap \<Longrightarrow> cap = DomainCap" 240by (auto simp: is_derived_def is_reply_cap_def is_pg_cap_def is_master_reply_cap_def cap_master_cap_def split: cap.splits) 241 242lemma cte_wp_at_is_derived_domain_sep_inv_cap: 243 "\<lbrakk>domain_sep_inv irqs st s; cte_wp_at (is_derived (cdt s) slot cap) slot s\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs cap" 244apply (cases slot) 245apply (fastforce simp: domain_sep_inv_def domain_sep_inv_cap_def 246 split: cap.splits 247 dest: cte_wp_at_eqD DomainCap_is_derived is_derived_IRQHandlerCap) 248done 249 250lemma domain_sep_inv_exst_update[simp]: 251 "domain_sep_inv irqs st (trans_state f s) = domain_sep_inv irqs st s" 252 apply(simp add: domain_sep_inv_def) 253 done 254 255lemma domain_sep_inv_is_original_cap_update[simp]: 256 "domain_sep_inv irqs st (s\<lparr>is_original_cap := X\<rparr>) = domain_sep_inv irqs st s" 257 apply(simp add: domain_sep_inv_def) 258 done 259 260lemma domain_sep_inv_cdt_update[simp]: 261 "domain_sep_inv irqs st (s\<lparr>cdt := X\<rparr>) = domain_sep_inv irqs st s" 262 apply(simp add: domain_sep_inv_def) 263 done 264 265crunch domain_sep_inv[wp]: update_cdt "domain_sep_inv irqs st" 266 267lemma set_untyped_cap_as_full_domain_sep_inv[wp]: 268 "\<lbrace>domain_sep_inv irqs st\<rbrace> set_untyped_cap_as_full a b c \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 269 apply(clarsimp simp: set_untyped_cap_as_full_def) 270 apply(rule hoare_pre) 271 apply(rule set_cap_domain_sep_inv) 272 apply(case_tac a, simp_all add: domain_sep_inv_cap_def) 273 done 274 275lemma cap_insert_domain_sep_inv: 276 "\<lbrace> domain_sep_inv irqs st and (\<lambda>s. cte_wp_at (is_derived (cdt s) slot cap) slot s) \<rbrace> 277 cap_insert cap slot dest_slot 278 \<lbrace> \<lambda>_. domain_sep_inv irqs st \<rbrace>" 279 apply(simp add: cap_insert_def) 280 apply(wp set_cap_domain_sep_inv get_cap_wp set_original_wp dxo_wp_weak | simp split del: if_split)+ 281 apply(blast dest: cte_wp_at_is_derived_domain_sep_inv_cap) 282 done 283 284lemma domain_sep_inv_cap_NullCap[simp]: 285 "domain_sep_inv_cap irqs NullCap" 286 apply(simp add: domain_sep_inv_cap_def) 287 done 288 289lemma cap_move_domain_sep_inv: 290 "\<lbrace> domain_sep_inv irqs st and (\<lambda>s. cte_wp_at (weak_derived cap) slot s) \<rbrace> 291 cap_move cap slot dest_slot 292 \<lbrace> \<lambda>_. domain_sep_inv irqs st \<rbrace>" 293 apply(simp add: cap_move_def) 294 apply(wp set_cap_domain_sep_inv get_cap_wp set_original_wp dxo_wp_weak | simp split del: if_split | blast dest: cte_wp_at_weak_derived_domain_sep_inv_cap)+ 295 done 296 297lemma domain_sep_inv_machine_state_update[simp]: 298 "domain_sep_inv irqs st (s\<lparr>machine_state := X\<rparr>) = domain_sep_inv irqs st s" 299 apply(simp add: domain_sep_inv_def) 300 done 301 302lemma set_irq_state_domain_sep_inv: 303 "\<lbrace>domain_sep_inv irqs st and (\<lambda>s. stt = interrupt_states s irq)\<rbrace> 304 set_irq_state stt irq 305 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 306 apply(simp add: set_irq_state_def) 307 apply(wp | simp add: do_machine_op_def | wpc)+ 308 done 309 310lemma deleted_irq_handler_domain_sep_inv: 311 "\<lbrace>domain_sep_inv irqs st and K irqs\<rbrace> deleted_irq_handler a \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 312 apply(rule hoare_gen_asm) 313 apply(simp add: deleted_irq_handler_def) 314 apply(simp add: set_irq_state_def) 315 apply wp 316 apply(rule domain_sep_inv_triv, wp+) 317 apply(simp add: domain_sep_inv_def) 318 done 319 320lemma empty_slot_domain_sep_inv: 321 "\<lbrace>\<lambda>s. domain_sep_inv irqs st s \<and> (\<not> irqs \<longrightarrow> b = NullCap)\<rbrace> 322 empty_slot a b 323 \<lbrace>\<lambda>_ s. domain_sep_inv irqs st s\<rbrace>" 324 unfolding empty_slot_def 325 by (wpsimp wp: get_cap_wp set_cap_domain_sep_inv set_original_wp dxo_wp_weak static_imp_wp 326 deleted_irq_handler_domain_sep_inv) 327 328lemma set_simple_ko_neg_cte_wp_at[wp]: 329 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> set_simple_ko f a b \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 330 apply(simp add: set_simple_ko_def) 331 apply(wp set_object_wp get_object_wp 332 | simp add: partial_inv_def a_type_def split: kernel_object.splits)+ 333 apply(case_tac "a = fst slot") 334 apply(clarsimp split: kernel_object.splits) 335 apply(fastforce elim: cte_wp_atE simp: obj_at_def) 336 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 337 done 338 339crunch domain_sep_inv[wp]: set_simple_ko "domain_sep_inv irqs st" 340 (wp: domain_sep_inv_triv) 341 342lemma set_thread_state_neg_cte_wp_at[wp]: 343 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> set_thread_state a b \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 344 apply(simp add: set_thread_state_def) 345 apply(wp set_object_wp get_object_wp dxo_wp_weak| simp)+ 346 apply(case_tac "a = fst slot") 347 apply(clarsimp split: kernel_object.splits) 348 apply(erule notE) 349 apply(erule cte_wp_atE) 350 apply(fastforce simp: obj_at_def) 351 apply(drule get_tcb_SomeD) 352 apply(rule cte_wp_at_tcbI) 353 apply(simp) 354 apply assumption 355 apply (fastforce simp: tcb_cap_cases_def split: if_splits) 356 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 357 done 358 359lemma set_bound_notification_neg_cte_wp_at[wp]: 360 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> set_bound_notification a b \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 361 apply(simp add: set_bound_notification_def) 362 apply(wp set_object_wp get_object_wp dxo_wp_weak| simp)+ 363 apply(case_tac "a = fst slot") 364 apply(clarsimp split: kernel_object.splits) 365 apply(erule notE) 366 apply(erule cte_wp_atE) 367 apply(fastforce simp: obj_at_def) 368 apply(drule get_tcb_SomeD) 369 apply(rule cte_wp_at_tcbI) 370 apply(simp) 371 apply assumption 372 apply (fastforce simp: tcb_cap_cases_def split: if_splits) 373 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 374 done 375 376crunch domain_sep_inv[wp]: set_thread_state, set_bound_notification, get_bound_notification "domain_sep_inv irqs st" 377 (wp: domain_sep_inv_triv) 378 379lemma thread_set_tcb_fault_update_neg_cte_wp_at[wp]: 380 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> 381 thread_set (tcb_fault_update blah) param_a 382 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 383 apply(simp add: thread_set_def) 384 apply(wp set_object_wp get_object_wp | simp)+ 385 apply(case_tac "param_a = fst slot") 386 apply(clarsimp split: kernel_object.splits) 387 apply(erule notE) 388 apply(erule cte_wp_atE) 389 apply(fastforce simp: obj_at_def) 390 apply(drule get_tcb_SomeD) 391 apply(rule cte_wp_at_tcbI) 392 apply(simp) 393 apply assumption 394 apply (fastforce simp: tcb_cap_cases_def split: if_splits) 395 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 396 done 397 398lemma thread_set_tcb_fault_update_domain_sep_inv[wp]: 399 "\<lbrace>domain_sep_inv irqs st\<rbrace> 400 thread_set (tcb_fault_update blah) param_a 401 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 402 apply(wp domain_sep_inv_triv) 403 done 404 405crunch domain_sep_inv[wp]: cap_delete_one "domain_sep_inv irqs st" 406 (wp: mapM_x_wp' hoare_unless_wp dxo_wp_weak ignore: tcb_sched_action reschedule_required simp: crunch_simps) 407 408lemma reply_cancel_ipc_domain_sep_inv[wp]: 409 "\<lbrace>domain_sep_inv irqs st\<rbrace> 410 reply_cancel_ipc t 411 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 412 apply(simp add: reply_cancel_ipc_def) 413 apply (wp select_wp) 414 apply(rule hoare_strengthen_post[OF thread_set_tcb_fault_update_domain_sep_inv]) 415 apply auto 416 done 417 418lemma domain_sep_inv_arch_state_update[simp]: 419 "domain_sep_inv irqs st (s\<lparr>arch_state := blah\<rparr>) = domain_sep_inv irqs st s" 420 apply(simp add: domain_sep_inv_def) 421 done 422 423lemma set_pt_neg_cte_wp_at[wp]: 424 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> 425 set_pt ptr pt 426 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 427 unfolding set_pt_def 428 apply(wp set_object_wp get_object_wp | simp)+ 429 apply(case_tac "ptr = fst slot") 430 apply(clarsimp split: kernel_object.splits) 431 apply(fastforce elim: cte_wp_atE simp: obj_at_def) 432 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 433 done 434 435crunch domain_sep_inv[wp]: set_pt "domain_sep_inv irqs st" 436 (wp: domain_sep_inv_triv) 437 438lemma set_pd_neg_cte_wp_at[wp]: 439 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> 440 set_pd ptr pt 441 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 442 unfolding set_pd_def 443 apply(wp set_object_wp get_object_wp | simp)+ 444 apply(case_tac "ptr = fst slot") 445 apply(clarsimp split: kernel_object.splits) 446 apply(fastforce elim: cte_wp_atE simp: obj_at_def) 447 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 448 done 449 450crunch domain_sep_inv[wp]: set_pd "domain_sep_inv irqs st" 451 (wp: domain_sep_inv_triv) 452 453lemma set_asid_pool_neg_cte_wp_at[wp]: 454 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> 455 set_asid_pool ptr pt 456 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 457 unfolding set_asid_pool_def 458 apply(wp set_object_wp get_object_wp | simp)+ 459 apply(case_tac "ptr = fst slot") 460 apply(clarsimp split: kernel_object.splits) 461 apply(fastforce elim: cte_wp_atE simp: obj_at_def) 462 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 463 done 464 465crunch domain_sep_inv[wp]: set_asid_pool "domain_sep_inv irqs st" 466 (wp: domain_sep_inv_triv) 467 468 469crunch domain_sep_inv[wp]: finalise_cap "domain_sep_inv irqs st" 470 (wp: crunch_wps dxo_wp_weak simp: crunch_simps ignore: set_object tcb_sched_action) 471 472lemma finalise_cap_domain_sep_inv_cap: 473 "\<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>" 474 including no_pre 475 apply(case_tac cap) 476 apply(wp | simp add: o_def split del: if_split split: cap.splits arch_cap.splits | fastforce split: if_splits simp: domain_sep_inv_cap_def)+ 477 apply(rule hoare_pre, wp, fastforce) 478 apply(rule hoare_pre, simp, wp, fastforce simp: domain_sep_inv_cap_def) 479 apply(simp add: arch_finalise_cap_def) 480 apply(rule hoare_pre) 481 apply(wpc | wp | simp)+ 482 done 483 484lemma get_cap_domain_sep_inv_cap: 485 "\<lbrace>domain_sep_inv irqs st\<rbrace> get_cap cap \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs rv\<rbrace>" 486 apply(wp get_cap_wp) 487 apply(blast dest: cte_wp_at_domain_sep_inv_cap) 488 done 489 490crunch domain_sep_inv[wp]: cap_swap_for_delete "domain_sep_inv irqs st" 491 (wp: get_cap_domain_sep_inv_cap dxo_wp_weak simp: crunch_simps ignore: cap_swap_ext) 492 493lemma finalise_cap_returns_NullCap: 494 "\<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> 495 finalise_cap cap b 496 \<lbrace>\<lambda>rv s. \<not> irqs \<longrightarrow> snd rv = NullCap\<rbrace>" 497 apply(case_tac cap) 498 by (wpsimp simp: o_def split_del: if_split | clarsimp simp: domain_sep_inv_cap_def arch_finalise_cap_def)+ 499 500lemma rec_del_domain_sep_inv': 501 notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del] 502 rec_del.simps[simp del] 503 shows 504 "s \<turnstile> \<lbrace> domain_sep_inv irqs st\<rbrace> 505 (rec_del call) 506 \<lbrace>\<lambda> a s. (case call of (FinaliseSlotCall x y) \<Rightarrow> (y \<or> fst a) \<longrightarrow> \<not> irqs \<longrightarrow> snd a = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv irqs st s\<rbrace>,\<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 507 proof (induct s arbitrary: rule: rec_del.induct, simp_all only: rec_del_fails hoare_fail_any) 508 case (1 slot exposed s) show ?case 509 apply(simp add: split_def rec_del.simps) 510 apply(wp empty_slot_domain_sep_inv drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp] | simp)+ 511 apply(rule spec_strengthen_postE[OF "1.hyps"]) 512 apply fastforce 513 done 514 next 515 case (2 slot exposed s) show ?case 516 apply(simp add: rec_del.simps split del: if_split) 517 apply(rule hoare_pre_spec_validE) 518 apply(wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp] set_cap_domain_sep_inv 519 |simp add: split_def split del: if_split)+ 520 apply(rule spec_strengthen_postE) 521 apply(rule "2.hyps", fastforce+) 522 apply(rule drop_spec_validE, (wp preemption_point_inv| simp)+)[1] 523 apply simp 524 apply(rule spec_strengthen_postE) 525 apply(rule "2.hyps", fastforce+) 526 apply(wp finalise_cap_domain_sep_inv_cap get_cap_wp 527 finalise_cap_returns_NullCap 528 drop_spec_validE[OF liftE_wp] set_cap_domain_sep_inv 529 |simp add: without_preemption_def split del: if_split 530 |wp_once hoare_drop_imps)+ 531 apply(blast dest: cte_wp_at_domain_sep_inv_cap) 532 done 533 next 534 case (3 ptr bits n slot s) show ?case 535 apply(simp add: rec_del.simps) 536 apply (wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp]) 537 apply(rule hoare_pre_spec_validE) 538 apply (wp drop_spec_validE[OF assertE_wp]) 539 apply(fastforce) 540 done 541 next 542 case (4 ptr bits n slot s) show ?case 543 apply(simp add: rec_del.simps) 544 apply (wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp] set_cap_domain_sep_inv 545 drop_spec_validE[OF assertE_wp] get_cap_wp | simp add: without_preemption_def)+ 546 apply (rule spec_strengthen_postE[OF "4.hyps"]) 547 apply(simp add: returnOk_def return_def) 548 apply(clarsimp simp: domain_sep_inv_cap_def) 549 done 550 qed 551 552lemma rec_del_domain_sep_inv: 553 "\<lbrace> domain_sep_inv irqs st\<rbrace> 554 (rec_del call) 555 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 556 apply (rule validE_valid) 557 apply (rule use_spec) 558 apply (rule spec_strengthen_postE[OF rec_del_domain_sep_inv']) 559 by fastforce 560 561crunch domain_sep_inv[wp]: cap_delete "domain_sep_inv irqs st" 562 563lemma preemption_point_domain_sep_inv[wp]: 564 "\<lbrace>domain_sep_inv irqs st\<rbrace> preemption_point \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 565 by (wp preemption_point_inv | simp)+ 566 567lemma cap_revoke_domain_sep_inv': 568 notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del] 569 shows 570 "s \<turnstile> \<lbrace> domain_sep_inv irqs st\<rbrace> 571 cap_revoke slot 572 \<lbrace> \<lambda>_. domain_sep_inv irqs st\<rbrace>, \<lbrace> \<lambda>_. domain_sep_inv irqs st\<rbrace>" 573 proof(induct rule: cap_revoke.induct[where ?a1.0=s]) 574 case (1 slot s) 575 show ?case 576 apply(subst cap_revoke.simps) 577 apply(rule hoare_pre_spec_validE) 578 apply (wp "1.hyps") 579 apply(wp spec_valid_conj_liftE2 | simp)+ 580 apply(wp drop_spec_validE[OF valid_validE[OF preemption_point_domain_sep_inv]] 581 drop_spec_validE[OF valid_validE[OF cap_delete_domain_sep_inv]] 582 drop_spec_validE[OF assertE_wp] drop_spec_validE[OF returnOk_wp] 583 drop_spec_validE[OF liftE_wp] select_wp 584 | simp | wp_once hoare_drop_imps)+ 585 done 586 qed 587 588lemmas cap_revoke_domain_sep_inv[wp] = use_spec(2)[OF cap_revoke_domain_sep_inv'] 589 590lemma cap_move_cte_wp_at_other: 591 "\<lbrace> cte_wp_at P slot and K (slot \<noteq> dest_slot \<and> slot \<noteq> src_slot) \<rbrace> 592 cap_move cap src_slot dest_slot 593 \<lbrace> \<lambda>_. cte_wp_at P slot \<rbrace>" 594 unfolding cap_move_def 595 apply (rule hoare_pre) 596 apply (wp set_cdt_cte_wp_at set_cap_cte_wp_at' dxo_wp_weak static_imp_wp 597 set_original_wp | simp)+ 598 done 599 600lemma cte_wp_at_weak_derived_ReplyCap: 601 "cte_wp_at ((=) (ReplyCap x False)) slot s 602 \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False)) slot s" 603 apply(erule cte_wp_atE) 604 apply(rule cte_wp_at_cteI) 605 apply assumption 606 apply assumption 607 apply assumption 608 apply simp 609 apply(rule cte_wp_at_tcbI) 610 apply auto 611 done 612 613lemma thread_set_tcb_registers_caps_merge_default_tcb_neg_cte_wp_at[wp]: 614 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> 615 thread_set (tcb_registers_caps_merge default_tcb) word 616 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 617 unfolding thread_set_def 618 apply(wp set_object_wp | simp)+ 619 apply(case_tac "word = fst slot") 620 apply(clarsimp split: kernel_object.splits) 621 apply(erule notE) 622 apply(erule cte_wp_atE) 623 apply(fastforce simp: obj_at_def) 624 apply(drule get_tcb_SomeD) 625 apply(rule cte_wp_at_tcbI) 626 apply(simp) 627 apply assumption 628 apply (clarsimp simp: tcb_cap_cases_def tcb_registers_caps_merge_def split: if_splits) 629 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 630 done 631 632lemma thread_set_tcb_registers_caps_merge_default_tcb_domain_sep_inv[wp]: 633 "\<lbrace>domain_sep_inv irqs st\<rbrace> 634 thread_set (tcb_registers_caps_merge default_tcb) word 635 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 636 apply(wp domain_sep_inv_triv) 637 done 638 639lemma cancel_badged_sends_domain_sep_inv[wp]: 640 "\<lbrace>domain_sep_inv irqs st\<rbrace> 641 cancel_badged_sends epptr badge 642 \<lbrace>\<lambda>rv. domain_sep_inv irqs st\<rbrace>" 643 apply(simp add: cancel_badged_sends_def) 644 apply(rule hoare_pre) 645 apply(wp dxo_wp_weak mapM_wp | wpc | simp add: filterM_mapM | rule subset_refl | wp_once hoare_drop_imps)+ 646 done 647 648crunch domain_sep_inv[wp]: finalise_slot "domain_sep_inv irqs st" 649 650lemma invoke_cnode_domain_sep_inv: 651 "\<lbrace> domain_sep_inv irqs st and valid_cnode_inv ci\<rbrace> 652 invoke_cnode ci 653 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 654 unfolding invoke_cnode_def 655 apply(case_tac ci) 656 apply(wp cap_insert_domain_sep_inv cap_move_domain_sep_inv | simp split del: if_split)+ 657 apply(rule hoare_pre) 658 apply(wp cap_move_domain_sep_inv cap_move_cte_wp_at_other get_cap_wp | simp | blast dest: cte_wp_at_weak_derived_domain_sep_inv_cap | wpc)+ 659 apply(fastforce dest: cte_wp_at_weak_derived_ReplyCap) 660 apply(wp | simp | wpc | rule hoare_pre)+ 661 done 662 663lemma create_cap_domain_sep_inv[wp]: 664 "\<lbrace> domain_sep_inv irqs st\<rbrace> 665 create_cap tp sz p dev slot 666 \<lbrace> \<lambda>_. domain_sep_inv irqs st\<rbrace>" 667 apply(simp add: create_cap_def) 668 apply(rule hoare_pre) 669 apply(wp set_cap_domain_sep_inv dxo_wp_weak | wpc | simp)+ 670 apply clarsimp 671 apply(case_tac tp, simp_all add: domain_sep_inv_cap_def) 672 done 673 674lemma detype_interrupts_states[simp]: 675 "interrupt_states (detype S s) = interrupt_states s" 676 apply(simp add: detype_def) 677 done 678 679lemma detype_domain_sep_inv[simp]: 680 "domain_sep_inv irqs st s \<longrightarrow> domain_sep_inv irqs st (detype S s)" 681 apply(fastforce simp: domain_sep_inv_def) 682 done 683 684lemma domain_sep_inv_detype_lift: 685 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. domain_sep_inv irqs st\<rbrace> \<Longrightarrow> 686 \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. domain_sep_inv irqs st (detype S s)\<rbrace>" 687 apply(strengthen detype_domain_sep_inv, assumption) 688 done 689 690lemma retype_region_neg_cte_wp_at_not_domain_sep_inv_cap: 691 "\<lbrace>\<lambda>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s \<rbrace> 692 retype_region base n sz ty dev 693 \<lbrace>\<lambda>rv s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace>" 694 apply(rule hoare_pre) 695 apply(simp only: retype_region_def retype_addrs_def 696 697 foldr_upd_app_if fun_app_def K_bind_def) 698 apply(wp dxo_wp_weak |simp)+ 699 apply clarsimp 700 apply(case_tac "fst slot \<in> (\<lambda>p. ptr_add base (p * 2 ^ obj_bits_api ty sz)) ` 701 {0..<n}") 702 apply clarsimp 703 apply(erule cte_wp_atE) 704 apply(clarsimp simp: default_object_def empty_cnode_def split: apiobject_type.splits if_splits simp: pred_neg_def) 705 apply(clarsimp simp: default_object_def default_tcb_def tcb_cap_cases_def split: apiobject_type.splits if_splits simp: pred_neg_def) 706 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_tcbI cte_wp_at_cteI) 707 done 708 709 710lemma retype_region_domain_sep_inv[wp]: 711 "\<lbrace>domain_sep_inv irqs st\<rbrace> 712 retype_region base n sz tp dev 713 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 714 apply(rule domain_sep_inv_wp[where P="\<top>" and R="\<top>", simplified]) 715 apply(rule retype_region_neg_cte_wp_at_not_domain_sep_inv_cap) 716 apply wp 717 done 718 719lemma domain_sep_inv_cap_UntypedCap[simp]: 720 "domain_sep_inv_cap irqs (UntypedCap dev base sz n)" 721 apply(simp add: domain_sep_inv_cap_def) 722 done 723 724crunch domain_sep_inv[wp]: invoke_untyped "domain_sep_inv irqs st" 725 (ignore: freeMemory retype_region wp: crunch_wps domain_sep_inv_detype_lift 726 get_cap_wp mapME_x_inv_wp 727 simp: crunch_simps mapM_x_def_bak unless_def) 728 729lemma perform_page_invocation_domain_sep_inv_get_cap_helper: 730 "\<lbrace>\<top>\<rbrace> 731 get_cap blah 732 \<lbrace>\<lambda>rv s. 733 domain_sep_inv_cap irqs 734 (ArchObjectCap (F rv))\<rbrace>" 735 apply(simp add: domain_sep_inv_cap_def) 736 apply(rule wp_post_taut) 737 done 738 739 740lemma set_object_tcb_context_update_neg_cte_wp_at: 741 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> obj_at ((=) (TCB tcb)) ptr s\<rbrace> 742 set_object ptr (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (arch_tcb tcb)\<rparr>)) 743 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 744 apply(wp set_object_wp) 745 apply clarsimp 746 apply(case_tac "ptr = fst slot") 747 apply(erule cte_wp_atE) 748 apply(fastforce simp: obj_at_def) 749 apply(erule notE) 750 apply(clarsimp simp: obj_at_def) 751 apply(rule cte_wp_at_tcbI) 752 apply(simp) 753 apply(fastforce) 754 apply(fastforce simp: tcb_cap_cases_def split: if_splits) 755 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 756 done 757 758lemma as_user_neg_cte_wp_at[wp]: 759 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> 760 as_user t f 761 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 762 unfolding as_user_def 763 apply(wp set_object_tcb_context_update_neg_cte_wp_at | simp add: split_def)+ 764 apply(fastforce simp: obj_at_def) 765 done 766 767crunch domain_sep_inv[wp]: as_user "domain_sep_inv irqs st" 768 (wp: domain_sep_inv_triv) 769 770lemma set_object_tcb_context_update_domain_sep_inv: 771 "\<lbrace>\<lambda>s. domain_sep_inv irqs st s \<and> obj_at ((=) (TCB tcb)) ptr s\<rbrace> 772 set_object ptr (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set X (tcb_arch tcb)\<rparr>)) 773 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 774 apply(rule hoare_pre) 775 apply(rule domain_sep_inv_wp) 776 apply(rule hoare_pre) 777 apply(rule set_object_tcb_context_update_neg_cte_wp_at) 778 apply(fastforce) 779 apply(wp | simp | elim conjE | assumption)+ 780 apply blast 781 done 782 783crunch domain_sep_inv[wp]: set_mrs "domain_sep_inv irqs st" 784 (ignore: set_object 785 wp: crunch_wps set_object_tcb_context_update_domain_sep_inv 786 simp: crunch_simps arch_tcb_set_registers_def) 787 788 789crunch domain_sep_inv[wp]: send_signal "domain_sep_inv irqs st" (wp: dxo_wp_weak ignore: possible_switch_to) 790 791crunch domain_sep_inv[wp]: copy_mrs, set_message_info, invalidate_tlb_by_asid "domain_sep_inv irqs st" 792 (wp: crunch_wps) 793 794lemma perform_page_invocation_domain_sep_inv: 795 "\<lbrace>domain_sep_inv irqs st and valid_page_inv pgi\<rbrace> 796 perform_page_invocation pgi 797 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 798 apply(rule hoare_pre) 799 apply(wp mapM_wp[OF _ subset_refl] set_cap_domain_sep_inv 800 mapM_x_wp[OF _ subset_refl] 801 perform_page_invocation_domain_sep_inv_get_cap_helper static_imp_wp 802 | simp add: perform_page_invocation_def o_def | wpc)+ 803 apply(clarsimp simp: valid_page_inv_def) 804 apply(case_tac xa, simp_all add: domain_sep_inv_cap_def is_pg_cap_def) 805 done 806 807lemma perform_page_table_invocation_domain_sep_inv: 808 "\<lbrace>domain_sep_inv irqs st and valid_pti pgi\<rbrace> 809 perform_page_table_invocation pgi 810 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 811 apply(rule hoare_pre) 812 apply(simp add: perform_page_table_invocation_def) 813 apply(wp crunch_wps perform_page_invocation_domain_sep_inv_get_cap_helper 814 set_cap_domain_sep_inv 815 | wpc 816 | simp add: o_def)+ 817 apply(clarsimp simp: valid_pti_def) 818 apply(case_tac x, simp_all add: domain_sep_inv_cap_def is_pt_cap_def) 819 done 820 821lemma perform_page_directory_invocation_domain_sep_inv: 822 "\<lbrace>domain_sep_inv irqs st\<rbrace> 823 perform_page_directory_invocation pti 824 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 825 apply (simp add: perform_page_directory_invocation_def) 826 apply (cases pti) 827 apply (simp | wp)+ 828 done 829 830lemma cap_insert_domain_sep_inv': 831 "\<lbrace> domain_sep_inv irqs st and K (domain_sep_inv_cap irqs cap) \<rbrace> 832 cap_insert cap slot dest_slot 833 \<lbrace> \<lambda>_. domain_sep_inv irqs st\<rbrace>" 834 apply(simp add: cap_insert_def) 835 apply(wp set_cap_domain_sep_inv get_cap_wp dxo_wp_weak | simp split del: if_split)+ 836 done 837 838lemma domain_sep_inv_cap_max_free_index_update[simp]: 839 "domain_sep_inv_cap irqs (max_free_index_update cap) = 840 domain_sep_inv_cap irqs cap" 841 apply(simp add: max_free_index_def free_index_update_def split: cap.splits) 842 done 843 844lemma domain_sep_inv_cap_ArchObjectCap[simp]: 845 "domain_sep_inv_cap irqs (ArchObjectCap arch_cap)" 846 by(simp add: domain_sep_inv_cap_def) 847 848lemma perform_asid_control_invocation_domain_sep_inv: 849 notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 850 shows 851 "\<lbrace>domain_sep_inv irqs st\<rbrace> 852 perform_asid_control_invocation blah 853 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 854 unfolding perform_asid_control_invocation_def 855 apply(rule hoare_pre) 856 apply (wp modify_wp cap_insert_domain_sep_inv' set_cap_domain_sep_inv 857 get_cap_domain_sep_inv_cap[where st=st] static_imp_wp 858 | wpc | simp )+ 859 done 860 861lemma perform_asid_pool_invocation_domain_sep_inv: 862 "\<lbrace>domain_sep_inv irqs st\<rbrace> 863 perform_asid_pool_invocation blah 864 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 865 apply(simp add: perform_asid_pool_invocation_def) 866 apply(rule hoare_pre) 867 apply(wp set_cap_domain_sep_inv get_cap_wp | wpc | simp)+ 868 done 869 870lemma arch_perform_invocation_domain_sep_inv: 871 "\<lbrace>domain_sep_inv irqs st and valid_arch_inv ai\<rbrace> 872 arch_perform_invocation ai 873 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 874 unfolding arch_perform_invocation_def 875 apply(rule hoare_pre) 876 apply(wp perform_page_table_invocation_domain_sep_inv 877 perform_page_directory_invocation_domain_sep_inv 878 perform_page_invocation_domain_sep_inv 879 perform_asid_control_invocation_domain_sep_inv 880 perform_asid_pool_invocation_domain_sep_inv 881 | wpc)+ 882 apply(clarsimp simp: valid_arch_inv_def split: arch_invocation.splits) 883 done 884 885(* when blah is AckIRQ the preconditions here contradict each other, which 886 is why this lemma is true *) 887lemma invoke_irq_handler_domain_sep_inv: 888 "\<lbrace>domain_sep_inv irqs st and irq_handler_inv_valid blah\<rbrace> 889 invoke_irq_handler blah 890 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 891 apply(case_tac blah) 892 apply(wp cap_insert_domain_sep_inv' | simp)+ 893 apply(rename_tac irq cap cslot_ptr s) 894 apply(case_tac cap, simp_all add: domain_sep_inv_cap_def)[1] 895 apply(wp | auto simp: domain_sep_inv_def)+ 896 done 897 898 899(* similarly, the preconditions here tend to contradict one another *) 900lemma invoke_control_domain_sep_inv: 901 "\<lbrace>domain_sep_inv irqs st and irq_control_inv_valid blah\<rbrace> 902 invoke_irq_control blah 903 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 904 including no_pre 905 apply (case_tac blah) 906 apply (case_tac irqs) 907 apply (wp cap_insert_domain_sep_inv' | simp )+ 908 apply (simp add: set_irq_state_def, wp, simp) 909 apply (fastforce simp: domain_sep_inv_def domain_sep_inv_cap_def) 910 apply (fastforce simp: valid_def domain_sep_inv_def) 911 apply (wp | simp)+ 912 apply (case_tac x2) 913 apply (simp) 914 apply (rule hoare_seq_ext[where B="\<lambda>_. domain_sep_inv irqs st and irq_control_inv_valid blah"]) 915 apply simp 916 apply (case_tac irqs) 917 prefer 2 918 apply (fastforce simp: valid_def domain_sep_inv_def arch_irq_control_inv_valid_def) 919 apply (wp cap_insert_domain_sep_inv' | simp )+ 920 apply (simp add: set_irq_state_def, wp, simp) 921 apply (fastforce simp: domain_sep_inv_def domain_sep_inv_cap_def) 922 apply wpsimp 923 apply (simp add: arch_irq_control_inv_valid_def) 924 apply (rule hoare_pre) 925 apply (wpsimp wp: do_machine_op_domain_sep_inv) 926 apply clarsimp 927 done 928 929 930 931crunch domain_sep_inv[wp]: receive_signal "domain_sep_inv irqs st" 932 933lemma domain_sep_inv_cap_ReplyCap[simp]: 934 "domain_sep_inv_cap irqs (ReplyCap param_a param_b)" 935 by(simp add: domain_sep_inv_cap_def) 936 937lemma setup_caller_cap_domain_sep_inv[wp]: 938 "\<lbrace>domain_sep_inv irqs st\<rbrace> 939 setup_caller_cap a b 940 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 941 apply(simp add: setup_caller_cap_def) 942 apply(wp cap_insert_domain_sep_inv' | simp)+ 943 done 944 945crunch domain_sep_inv[wp]: set_extra_badge "domain_sep_inv irqs st" 946 947lemma derive_cap_domain_sep_inv_cap: 948 "\<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> 949 derive_cap slot cap 950 \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs rv\<rbrace>,-" 951 apply(simp add: derive_cap_def) 952 apply(rule hoare_pre) 953 apply(wp | wpc | simp add: arch_derive_cap_def)+ 954 apply auto 955 done 956 957lemma transfer_caps_domain_sep_inv: 958 "\<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb 959 and (\<lambda> s. (\<forall>x\<in>set caps. 960 s \<turnstile> fst x) \<and> 961 (\<forall>x\<in>set caps. 962 cte_wp_at 963 (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> 964 cp = fst x) 965 (snd x) s \<and> 966 real_cte_at (snd x) s))\<rbrace> 967 transfer_caps mi caps endpoint receiver receive_buffer 968 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 969 unfolding transfer_caps_def 970 apply (wpsimp wp: transfer_caps_loop_pres_dest cap_insert_domain_sep_inv hoare_vcg_all_lift hoare_vcg_imp_lift) 971 apply (fastforce elim: cte_wp_at_weakenE) 972 done 973 974 975lemma do_normal_transfer_domain_sep_inv: 976 "\<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb\<rbrace> 977 do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer 978 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 979 unfolding do_normal_transfer_def 980 apply (wp transfer_caps_domain_sep_inv hoare_vcg_ball_lift lec_valid_cap' | simp)+ 981 done 982 983crunch domain_sep_inv[wp]: do_fault_transfer "domain_sep_inv irqs st" 984 985lemma do_ipc_transfer_domain_sep_inv: 986 "\<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb\<rbrace> 987 do_ipc_transfer sender ep badge grant receiver 988 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 989 unfolding do_ipc_transfer_def 990 apply (wp do_normal_transfer_domain_sep_inv hoare_vcg_all_lift | wpc | wp_once hoare_drop_imps)+ 991 apply clarsimp 992 done 993 994(* FIXME: clagged from FinalCaps *) 995lemma valid_ep_recv_dequeue': 996 "\<lbrakk> ko_at (Endpoint (Structures_A.endpoint.RecvEP (t # ts))) epptr s; 997 valid_objs s\<rbrakk> 998 \<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> Structures_A.endpoint.IdleEP 999 | b # bs \<Rightarrow> Structures_A.endpoint.RecvEP ts) s" 1000 unfolding valid_objs_def valid_obj_def valid_ep_def obj_at_def 1001 apply (drule bspec) 1002 apply (auto split: list.splits) 1003 done 1004 1005lemma send_ipc_domain_sep_inv: 1006 "\<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb and 1007 sym_refs \<circ> state_refs_of\<rbrace> 1008 send_ipc block call badge can_grant thread epptr 1009 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1010 unfolding send_ipc_def 1011 apply (wp setup_caller_cap_domain_sep_inv | wpc | simp)+ 1012 apply(rule_tac Q="\<lambda> r s. domain_sep_inv irqs st s" in hoare_strengthen_post) 1013 apply(wp do_ipc_transfer_domain_sep_inv dxo_wp_weak | wpc | simp)+ 1014 apply (wp_once hoare_drop_imps) 1015 apply (wp get_simple_ko_wp)+ 1016 apply clarsimp 1017 apply (fastforce simp: valid_objs_def valid_obj_def obj_at_def ep_q_refs_of_def 1018 valid_simple_obj_def a_type_def ep_redux_simps neq_Nil_conv valid_ep_def case_list_cons_cong 1019 elim: ep_queued_st_tcb_at) 1020 done 1021 1022(* FIXME: following 2 clagged from FinalCaps *) 1023lemma hd_tl_in_set: 1024 "tl xs = (x # xs') \<Longrightarrow> x \<in> set xs" 1025 apply(case_tac xs, auto) 1026 done 1027 1028lemma set_tl_subset: 1029 "list \<noteq> [] \<Longrightarrow> set (tl list) \<subseteq> set list" 1030 apply(case_tac list) 1031 apply auto 1032 done 1033 1034crunch domain_sep_inv[wp]: complete_signal "domain_sep_inv irqs st" 1035 1036lemma receive_ipc_base_domain_sep_inv: 1037 "\<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb and 1038 sym_refs \<circ> state_refs_of and ko_at (Endpoint ep) epptr \<rbrace> 1039 receive_ipc_base aag receiver ep epptr rights is_blocking 1040 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1041 apply (clarsimp cong: endpoint.case_cong thread_get_def get_thread_state_def) 1042 apply (rule hoare_pre) 1043 apply (wp setup_caller_cap_domain_sep_inv dxo_wp_weak 1044 | wpc | simp split del: if_split)+ 1045 apply(rule_tac Q="\<lambda> r s. domain_sep_inv irqs st s" in hoare_strengthen_post) 1046 apply(wp do_ipc_transfer_domain_sep_inv hoare_vcg_all_lift | wpc | simp)+ 1047 apply(wp hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1] hoare_vcg_all_lift get_simple_ko_wp 1048 | wpc | simp add: valid_simple_obj_def a_type_def do_nbrecv_failed_transfer_def)+ 1049 apply (clarsimp simp: conj_comms) 1050 apply (fastforce simp: valid_objs_def valid_obj_def obj_at_def 1051 ep_redux_simps neq_Nil_conv valid_ep_def case_list_cons_cong) 1052 done 1053 1054lemma receive_ipc_domain_sep_inv: 1055 "\<lbrace>domain_sep_inv irqs st and valid_objs and valid_mdb and 1056 sym_refs \<circ> state_refs_of \<rbrace> 1057 receive_ipc receiver cap is_blocking 1058 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1059 unfolding receive_ipc_def 1060 apply (simp add: receive_ipc_def split: cap.splits, clarsimp) 1061 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 1062 apply (rule hoare_seq_ext[OF _ gbn_sp]) 1063 apply (case_tac ntfnptr, simp) 1064 apply (wp receive_ipc_base_domain_sep_inv get_simple_ko_wp | simp split: if_split option.splits)+ 1065 done 1066 1067lemma send_fault_ipc_domain_sep_inv: 1068 "\<lbrace>domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and 1069 K (valid_fault fault)\<rbrace> 1070 send_fault_ipc thread fault 1071 \<lbrace>\<lambda>rv. domain_sep_inv irqs st\<rbrace>" 1072 apply(rule hoare_gen_asm)+ 1073 unfolding send_fault_ipc_def 1074 apply(wp send_ipc_domain_sep_inv thread_set_valid_objs thread_set_tcb_fault_update_valid_mdb 1075 thread_set_refs_trivial thread_set_obj_at_impossible 1076 hoare_vcg_ex_lift 1077 | wpc| simp add: Let_def split_def lookup_cap_def valid_tcb_fault_update split del: if_split)+ 1078 apply (wpe get_cap_inv[where P="domain_sep_inv irqs st and valid_objs and valid_mdb 1079 and sym_refs o state_refs_of"]) 1080 apply (wp | simp)+ 1081 done 1082 1083crunch domain_sep_inv[wp]: handle_fault "domain_sep_inv irqs st" 1084 1085crunch domain_sep_inv[wp]: do_reply_transfer "domain_sep_inv irqs st" 1086 (wp: dxo_wp_weak crunch_wps ignore: set_object thread_set possible_switch_to) 1087 1088crunch domain_sep_inv[wp]: reply_from_kernel "domain_sep_inv irqs st" 1089 (wp: crunch_wps simp: crunch_simps) 1090 1091crunch domain_sep_inv[wp]: setup_reply_master "domain_sep_inv irqs st" 1092 (wp: crunch_wps simp: crunch_simps) 1093 1094crunch domain_sep_inv[wp]: restart "domain_sep_inv irqs st" 1095 (wp: crunch_wps dxo_wp_weak simp: crunch_simps ignore: tcb_sched_action possible_switch_to) 1096 1097lemma thread_set_tcb_ipc_buffer_update_neg_cte_wp_at[wp]: 1098 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> 1099 thread_set (tcb_ipc_buffer_update f) t 1100 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 1101 unfolding thread_set_def 1102 apply(wp set_object_wp | simp)+ 1103 apply(case_tac "t = fst slot") 1104 apply(clarsimp split: kernel_object.splits) 1105 apply(erule notE) 1106 apply(erule cte_wp_atE) 1107 apply(fastforce simp: obj_at_def) 1108 apply(drule get_tcb_SomeD) 1109 apply(rule cte_wp_at_tcbI) 1110 apply(simp) 1111 apply assumption 1112 apply (fastforce simp: tcb_cap_cases_def split: if_splits) 1113 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 1114 done 1115 1116lemma thread_set_tcb_ipc_buffer_update_domain_sep_inv[wp]: 1117 "\<lbrace>domain_sep_inv irqs st\<rbrace> 1118 thread_set (tcb_ipc_buffer_update f) t 1119 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1120 by (rule domain_sep_inv_triv; wp) 1121 1122lemma thread_set_tcb_fault_handler_update_neg_cte_wp_at[wp]: 1123 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> 1124 thread_set (tcb_fault_handler_update blah) t 1125 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 1126 unfolding thread_set_def 1127 apply(wp set_object_wp | simp)+ 1128 apply(case_tac "t = fst slot") 1129 apply(clarsimp split: kernel_object.splits) 1130 apply(erule notE) 1131 apply(erule cte_wp_atE) 1132 apply(fastforce simp: obj_at_def) 1133 apply(drule get_tcb_SomeD) 1134 apply(rule cte_wp_at_tcbI) 1135 apply(simp) 1136 apply assumption 1137 apply (fastforce simp: tcb_cap_cases_def split: if_splits) 1138 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 1139 done 1140 1141lemma thread_set_tcb_fault_handler_update_domain_sep_inv[wp]: 1142 "\<lbrace>domain_sep_inv irqs st\<rbrace> 1143 thread_set (tcb_fault_handler_update blah) t 1144 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1145 by (rule domain_sep_inv_triv; wp) 1146 1147lemma thread_set_tcb_tcb_mcpriority_update_neg_cte_wp_at[wp]: 1148 "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> 1149 thread_set (tcb_mcpriority_update blah) t 1150 \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" 1151 unfolding thread_set_def 1152 apply(wp set_object_wp | simp)+ 1153 apply(case_tac "t = fst slot") 1154 apply(clarsimp split: kernel_object.splits) 1155 apply(erule notE) 1156 apply(erule cte_wp_atE) 1157 apply(fastforce simp: obj_at_def) 1158 apply(drule get_tcb_SomeD) 1159 apply(rule cte_wp_at_tcbI) 1160 apply(simp) 1161 apply assumption 1162 apply (fastforce simp: tcb_cap_cases_def split: if_splits) 1163 apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) 1164 done 1165 1166lemma thread_set_tcb_tcp_mcpriority_update_domain_sep_inv[wp]: 1167 "\<lbrace>domain_sep_inv irqs st\<rbrace> 1168 thread_set (tcb_mcpriority_update blah) t 1169 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1170 by (rule domain_sep_inv_triv; wp) 1171 1172lemma same_object_as_domain_sep_inv_cap: 1173 "\<lbrakk>same_object_as a cap; domain_sep_inv_cap irqs cap\<rbrakk> 1174 \<Longrightarrow> domain_sep_inv_cap irqs a" 1175 apply(case_tac a, simp_all add: same_object_as_def domain_sep_inv_cap_def) 1176 apply(case_tac cap, simp_all) 1177 done 1178 1179lemma checked_cap_insert_domain_sep_inv: 1180 "\<lbrace>domain_sep_inv irqs st\<rbrace> 1181 check_cap_at a b (check_cap_at c d (cap_insert a b e)) 1182 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1183 apply(wp get_cap_wp cap_insert_domain_sep_inv' | simp add: check_cap_at_def)+ 1184 apply clarsimp 1185 apply(drule_tac cap=cap in cte_wp_at_domain_sep_inv_cap) 1186 apply assumption 1187 apply(erule (1) same_object_as_domain_sep_inv_cap) 1188 done 1189 1190crunch domain_sep_inv[wp]: bind_notification,reschedule_required "domain_sep_inv irqs st" 1191 1192lemma dxo_domain_sep_inv[wp]: 1193 "\<lbrace>domain_sep_inv irqs st\<rbrace> do_extended_op eop \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1194 by (simp | wp dxo_wp_weak)+ 1195 1196 1197lemma set_mcpriority_domain_sep_inv[wp]: 1198 "\<lbrace>domain_sep_inv irqs st\<rbrace> set_mcpriority tcb_ref mcp \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1199 unfolding set_mcpriority_def by wp 1200 1201lemma invoke_tcb_domain_sep_inv: 1202 "\<lbrace>domain_sep_inv irqs st and 1203 Tcb_AI.tcb_inv_wf tinv\<rbrace> 1204 invoke_tcb tinv 1205 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1206 apply(case_tac tinv) 1207 apply((wp restart_domain_sep_inv hoare_vcg_if_lift mapM_x_wp[OF _ subset_refl] 1208 | wpc 1209 | simp split del: if_split add: check_cap_at_def 1210 | clarsimp)+)[3] 1211 defer 1212 apply((wp | simp )+)[2] 1213 (* just NotificationControl and ThreadControl left *) 1214 apply (rename_tac option) 1215 apply (case_tac option) 1216 apply ((wp | simp)+)[1] 1217 apply (simp add: split_def cong: option.case_cong) 1218 apply (wp checked_cap_insert_domain_sep_inv hoare_vcg_all_lift_R 1219 hoare_vcg_all_lift hoare_vcg_const_imp_lift_R 1220 cap_delete_domain_sep_inv 1221 cap_delete_deletes 1222 dxo_wp_weak 1223 cap_delete_valid_cap cap_delete_cte_at static_imp_wp 1224 |wpc 1225 |simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def 1226 tcb_at_st_tcb_at 1227 |strengthen use_no_cap_to_obj_asid_strg)+ 1228 apply(rule hoare_pre) 1229 apply(simp add: option_update_thread_def tcb_cap_cases_def 1230 | wp hoare_vcg_all_lift 1231 thread_set_emptyable 1232 thread_set_valid_cap static_imp_wp 1233 thread_set_cte_at thread_set_no_cap_to_trivial 1234 | wpc)+ 1235 done 1236 1237lemma invoke_domain_domain_set_inv: 1238 "\<lbrace>domain_sep_inv irqs st\<rbrace> 1239 invoke_domain word1 word2 1240 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1241apply (simp add: invoke_domain_def set_domain_extended.dxo_eq) 1242apply (wp dxo_wp_weak | simp)+ 1243done 1244 1245 1246 1247lemma perform_invocation_domain_sep_inv': 1248 "\<lbrace>domain_sep_inv irqs st and valid_invocation iv and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of\<rbrace> 1249 perform_invocation block call iv 1250 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1251 apply(case_tac iv) 1252 apply(wp send_ipc_domain_sep_inv invoke_tcb_domain_sep_inv 1253 invoke_cnode_domain_sep_inv invoke_control_domain_sep_inv 1254 invoke_irq_handler_domain_sep_inv arch_perform_invocation_domain_sep_inv 1255 invoke_domain_domain_set_inv 1256 | simp add: split_def 1257 | blast)+ 1258 done 1259 1260lemma perform_invocation_domain_sep_inv: 1261 "\<lbrace>domain_sep_inv irqs st and valid_invocation iv and invs\<rbrace> 1262 perform_invocation block call iv 1263 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1264apply (rule hoare_weaken_pre[OF perform_invocation_domain_sep_inv']) 1265apply auto 1266done 1267 1268lemma handle_invocation_domain_sep_inv: 1269 "\<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> 1270 handle_invocation calling blocking 1271 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1272 apply (simp add: handle_invocation_def ts_Restart_case_helper split_def 1273 liftE_liftM_liftME liftME_def bindE_assoc 1274 split del: if_split) 1275 apply(wp syscall_valid perform_invocation_domain_sep_inv 1276 set_thread_state_runnable_valid_sched 1277 | simp split del: if_split)+ 1278 apply(rule_tac E="\<lambda>ft. domain_sep_inv irqs st and 1279 valid_objs and 1280 sym_refs \<circ> state_refs_of and 1281 valid_mdb and 1282 (\<lambda>y. valid_fault ft)" and R="Q" and Q=Q for Q in hoare_post_impErr) 1283 apply(wp 1284 | simp | clarsimp)+ 1285 apply(rule_tac E="\<lambda>ft. domain_sep_inv irqs st and 1286 valid_objs and 1287 sym_refs \<circ> state_refs_of and 1288 valid_mdb and 1289 (\<lambda>y. valid_fault (CapFault x False ft))" and R="Q" and Q=Q 1290 for Q in hoare_post_impErr) 1291 apply (wp lcs_ex_cap_to2 1292 | clarsimp)+ 1293 apply (auto intro: st_tcb_ex_cap simp: ct_in_state_def) 1294 done 1295 1296lemma handle_send_domain_sep_inv: 1297 "\<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> 1298 handle_send a 1299 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1300 apply(simp add: handle_send_def) 1301 apply(wp handle_invocation_domain_sep_inv) 1302 done 1303 1304lemma handle_call_domain_sep_inv: 1305 "\<lbrace>domain_sep_inv irqs st and invs and ct_active\<rbrace> 1306 handle_call 1307 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1308 apply(simp add: handle_call_def) 1309 apply(wp handle_invocation_domain_sep_inv) 1310 done 1311 1312lemma handle_reply_domain_sep_inv: 1313 "\<lbrace>domain_sep_inv irqs st and invs\<rbrace> handle_reply \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1314 apply(simp add: handle_reply_def) 1315 apply(wp get_cap_wp | wpc)+ 1316 apply auto 1317 done 1318 1319crunch domain_sep_inv[wp]: delete_caller_cap "domain_sep_inv irqs st" 1320 1321(* FIXME: clagged from Syscall_AC *) 1322lemma lookup_slot_for_thread_cap_fault: 1323 "\<lbrace>invs\<rbrace> lookup_slot_for_thread t s -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>" 1324 apply (simp add: lookup_slot_for_thread_def) 1325 apply (wp resolve_address_bits_valid_fault2) 1326 apply clarsimp 1327 apply (erule (1) invs_valid_tcb_ctable) 1328 done 1329 1330 1331lemma handle_recv_domain_sep_inv: 1332 "\<lbrace>domain_sep_inv irqs st and invs\<rbrace> 1333 handle_recv is_blocking 1334 \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1335 apply (simp add: handle_recv_def Let_def lookup_cap_def split_def) 1336 apply (wp hoare_vcg_all_lift lookup_slot_for_thread_cap_fault 1337 receive_ipc_domain_sep_inv delete_caller_cap_domain_sep_inv 1338 get_cap_wp get_simple_ko_wp 1339 | wpc | simp 1340 | rule_tac Q="\<lambda>rv. invs and (\<lambda>s. cur_thread s = thread)" in hoare_strengthen_post, wp, 1341 clarsimp simp: invs_valid_objs invs_sym_refs)+ 1342 apply (rule_tac Q'="\<lambda>r s. domain_sep_inv irqs st s \<and> invs s \<and> tcb_at thread s \<and> thread = cur_thread s" in hoare_post_imp_R) 1343 apply wp 1344 apply ((clarsimp simp add: invs_valid_objs invs_sym_refs 1345 | intro impI allI conjI 1346 | rule cte_wp_valid_cap caps_of_state_cteD 1347 | fastforce simp: valid_fault_def 1348 )+)[1] 1349 apply (wp delete_caller_cap_domain_sep_inv | simp add: split_def cong: conj_cong)+ 1350 apply(wp | simp add: invs_valid_objs invs_mdb invs_sym_refs tcb_at_invs)+ 1351 done 1352 1353crunch domain_sep_inv[wp]: handle_interrupt "domain_sep_inv irqs st" 1354 (wp: dxo_wp_weak ignore: getActiveIRQ resetTimer ackInterrupt ignore: timer_tick) 1355 1356crunch domain_sep_inv[wp]: handle_vm_fault, handle_hypervisor_fault "domain_sep_inv irqs st" 1357 (ignore: getFAR getDFSR getIFSR) 1358 1359lemma handle_event_domain_sep_inv: 1360 "\<lbrace> domain_sep_inv irqs st and invs and 1361 (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) \<rbrace> 1362 handle_event ev 1363 \<lbrace> \<lambda>_. domain_sep_inv irqs st\<rbrace>" 1364 apply(case_tac ev, simp_all) 1365 apply(rule hoare_pre) 1366 apply(wpc 1367 | wp handle_send_domain_sep_inv handle_call_domain_sep_inv 1368 handle_recv_domain_sep_inv handle_reply_domain_sep_inv 1369 hy_inv 1370 | simp add: invs_valid_objs invs_mdb invs_sym_refs valid_fault_def)+ 1371 apply(rule_tac E="\<lambda>rv s. domain_sep_inv irqs st s \<and> invs s \<and> valid_fault rv" and R="Q" and Q=Q for Q in hoare_post_impErr) 1372 apply(wp handle_vm_fault_domain_sep_inv | simp add: invs_valid_objs invs_mdb invs_sym_refs valid_fault_def | auto)+ 1373 done 1374 1375crunch domain_sep_inv[wp]: activate_thread "domain_sep_inv irqs st" 1376 1377lemma domain_sep_inv_cur_thread_update[simp]: 1378 "domain_sep_inv irqs st (s\<lparr>cur_thread := X\<rparr>) = domain_sep_inv irqs st s" 1379 apply(simp add: domain_sep_inv_def) 1380 done 1381 1382crunch domain_sep_inv[wp]: choose_thread "domain_sep_inv irqs st" 1383 (wp: crunch_wps dxo_wp_weak ignore: tcb_sched_action ARM.clearExMonitor) 1384 1385end 1386 1387lemma (in is_extended') domain_sep_inv[wp]: "I (domain_sep_inv irqs st)" by (rule lift_inv, simp) 1388 1389context begin interpretation Arch . (*FIXME: arch_split*) 1390 1391lemma schedule_domain_sep_inv: "\<lbrace>domain_sep_inv irqs st\<rbrace> (schedule :: (unit,det_ext) s_monad) \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" 1392 apply (simp add: schedule_def allActiveTCBs_def) 1393 apply (wp add: alternative_wp select_wp guarded_switch_to_lift hoare_drop_imps 1394 del: ethread_get_wp 1395 | wpc | clarsimp simp: get_thread_state_def thread_get_def trans_state_update'[symmetric] 1396 schedule_choose_new_thread_def)+ 1397 done 1398 1399lemma call_kernel_domain_sep_inv: 1400 "\<lbrace> domain_sep_inv irqs st and invs and 1401 (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) \<rbrace> 1402 call_kernel ev :: (unit,det_ext) s_monad 1403 \<lbrace> \<lambda>_. domain_sep_inv irqs st\<rbrace>" 1404apply (simp add: call_kernel_def getActiveIRQ_def) 1405apply (wp handle_interrupt_domain_sep_inv handle_event_domain_sep_inv schedule_domain_sep_inv 1406 | simp)+ 1407done 1408 1409end 1410 1411end 1412