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