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 Syscall_DR 12imports 13 Tcb_DR 14 Schedule_DR 15 Interrupt_DR 16begin 17 18context begin interpretation Arch . (*FIXME: arch_split*) 19 20(* 21 * Translate an abstract invocation into a corresponding 22 * CDL invocation. 23 *) 24 25definition 26 translate_invocation :: "Invocations_A.invocation \<Rightarrow> cdl_invocation" 27where 28 "translate_invocation x \<equiv> 29 case x of 30 Invocations_A.InvokeUntyped iu \<Rightarrow> 31 Invocations_D.InvokeUntyped $ 32 translate_untyped_invocation iu 33 | Invocations_A.InvokeEndpoint ep bdg grant \<Rightarrow> 34 Invocations_D.InvokeEndpoint $ 35 SyncMessage bdg grant ep 36 | Invocations_A.InvokeNotification ntfn aebdg \<Rightarrow> 37 Invocations_D.InvokeNotification $ 38 Signal aebdg ntfn 39 | Invocations_A.InvokeReply target_tcb reply_slot \<Rightarrow> 40 Invocations_D.InvokeReply $ 41 ReplyMessage target_tcb (transform_cslot_ptr reply_slot) 42 | Invocations_A.InvokeCNode icn \<Rightarrow> 43 Invocations_D.InvokeCNode $ 44 translate_cnode_invocation icn 45 | Invocations_A.InvokeTCB itcb \<Rightarrow> 46 Invocations_D.InvokeTcb $ translate_tcb_invocation itcb 47 | Invocations_A.InvokeDomain itcb d \<Rightarrow> Invocations_D.InvokeDomain $ SetDomain itcb d 48 | Invocations_A.InvokeIRQControl irqc \<Rightarrow> 49 Invocations_D.InvokeIrqControl $ translate_irq_control_invocation irqc 50 | Invocations_A.InvokeIRQHandler irrqh \<Rightarrow> 51 Invocations_D.InvokeIrqHandler $ translate_irq_handler_invocation irrqh 52 " 53 54definition 55 cdl_invocation_relation :: "cdl_invocation \<Rightarrow> Invocations_A.invocation \<Rightarrow> bool" 56where 57 "cdl_invocation_relation x y \<equiv> 58 case y of Invocations_A.InvokeArchObject invo \<Rightarrow> arch_invocation_relation x invo 59 | _ \<Rightarrow> x = translate_invocation y" 60 61(* we store the simplified version of this lemma, since the 'liftME's in 62 * the goal are invariably simplified before this rule is applied *) 63lemma dcorres_liftME_liftME [simplified]: 64 "\<lbrakk>dcorres (dc \<oplus> rvrel) G G' m m'; 65 \<And> r r'. rvrel r r' \<Longrightarrow> rvrel' (f r) (f' r')\<rbrakk> 66 \<Longrightarrow> 67 dcorres (dc \<oplus> rvrel') G G' (liftME f m) (liftME f' m')" 68 apply(simp, rule_tac r'="(dc \<oplus> rvrel)" and r="dc \<oplus> ((\<lambda> x. rvrel' x \<circ> f') \<circ> f)" in corres_rel_imp) 69 apply(assumption) 70 apply(case_tac x, simp) 71 apply(case_tac y, simp_all) 72done 73 74 75(* Decoding NullCap invocations is equivalent. *) 76lemma decode_invocation_nullcap_corres: 77 "\<lbrakk> Some intent = transform_intent (invocation_type label) args'; 78 invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; 79 invoked_cap = transform_cap invoked_cap'; 80 excaps = transform_cap_list excaps'; 81 invoked_cap' = cap.NullCap \<rbrakk> \<Longrightarrow> 82 dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top> 83 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 84 (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" 85 apply (unfold Decode_A.decode_invocation_def Decode_D.decode_invocation_def) 86 apply (clarsimp simp: transform_cap_def) 87 done 88 89(* Decoding UntypedCap invocations is equivalent. *) 90lemma decode_invocation_untypedcap_corres: 91 "\<lbrakk> Some intent = transform_intent (invocation_type label') args'; 92 invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; 93 invoked_cap = transform_cap invoked_cap'; 94 excaps = transform_cap_list excaps'; 95 invoked_cap' = cap.UntypedCap dev a b idx \<rbrakk> \<Longrightarrow> 96 dcorres (dc \<oplus> cdl_invocation_relation) \<top> 97 (invs and cte_wp_at ((=) invoked_cap') invoked_cap_ref' 98 and (\<lambda>s. \<forall>x \<in> set (map fst excaps'). s \<turnstile> x) 99 and (\<lambda>s. \<forall>x \<in> set excaps'. cte_wp_at (diminished (fst x)) (snd x) s) 100 and valid_etcbs) 101 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 102 (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" 103 apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) 104 apply (case_tac "\<exists> ui. intent = UntypedIntent ui") 105 apply (clarsimp simp: throw_opt_def get_untyped_intent_def split: cdl_intent.splits option.splits) 106 apply (rule dcorres_liftME_liftME) 107 apply (rule corres_guard_imp, rule decode_untyped_corres, auto simp: transform_cap_def)[1] 108 apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def) 109 apply (clarsimp simp: throw_opt_def get_untyped_intent_def split: cdl_intent.split) 110 apply (rule absorb_imp,clarsimp)+ 111 apply (rule dcorres_free_throw) 112 apply (subst decode_untyped_label_not_match) 113 apply simp+ 114done 115 116(* Decoding Endpoint invocations is equivalent. *) 117lemma decode_invocation_endpointcap_corres: 118 "\<lbrakk> Some intent = transform_intent (invocation_type label') args'; 119 invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; 120 invoked_cap = transform_cap invoked_cap'; 121 excaps = transform_cap_list excaps'; 122 invoked_cap' = cap.EndpointCap a b c \<rbrakk> \<Longrightarrow> 123 dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top> 124 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 125 (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" 126 apply (clarsimp simp: Decode_A.decode_invocation_def 127 Decode_D.decode_invocation_def) 128 apply (rule corres_returnOk) 129 apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def) 130 done 131 132(* Decoding Async Endpoint invocations is equivalent. *) 133lemma decode_invocation_notificationcap_corres: 134 "\<lbrakk> Some intent = transform_intent (invocation_type label') args'; 135 invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; 136 invoked_cap = transform_cap invoked_cap'; 137 excaps = transform_cap_list excaps'; 138 invoked_cap' = cap.NotificationCap a b c \<rbrakk> \<Longrightarrow> 139 dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top> 140 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 141 (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" 142 apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) 143 apply (auto simp: cdl_invocation_relation_def translate_invocation_def 144 split:rights.splits intro!:corres_returnOk) 145 done 146 147(* Decoding ReplyCap invocations is equivalent. *) 148lemma decode_invocation_replycap_corres: 149 "\<lbrakk> Some intent = transform_intent (invocation_type label') args'; 150 invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; 151 invoked_cap = transform_cap invoked_cap'; 152 excaps = transform_cap_list excaps'; 153 invoked_cap' = cap.ReplyCap a b \<rbrakk> \<Longrightarrow> 154 dcorres (dc \<oplus> cdl_invocation_relation) \<top> (cte_wp_at (Not\<circ> is_master_reply_cap) invoked_cap_ref' and cte_wp_at (diminished invoked_cap') invoked_cap_ref') 155 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 156 (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" 157 apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def ) 158 apply (rule dcorres_expand_pfx) 159 apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def 160 split:rights.splits) 161 apply (clarsimp simp:cte_wp_at_def is_master_reply_cap_def) 162 apply (rule corres_guard_imp[OF dcorres_returnOk]) 163 apply (simp add:cdl_invocation_relation_def translate_invocation_def)+ 164done 165 166(* Decoding CNode invocations is equivalent. *) 167lemma decode_invocation_cnodecap_corres: 168 "\<lbrakk> Some intent = transform_intent (invocation_type label') args'; 169 invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; 170 invoked_cap = transform_cap invoked_cap'; 171 excaps = transform_cap_list excaps'; 172 invoked_cap' = cap.CNodeCap a b c \<rbrakk> \<Longrightarrow> 173 dcorres (dc \<oplus> cdl_invocation_relation) \<top> 174 (invs and valid_cap invoked_cap' and (\<lambda>s. \<forall>e\<in>set excaps'. valid_cap (fst e) s) and valid_etcbs) 175 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 176 (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" 177 apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) 178 apply (case_tac "\<exists> ui. intent = CNodeIntent ui") 179 apply (rotate_tac -1, erule exE) 180 apply (rotate_tac -1, drule sym) 181 apply (clarsimp simp: get_cnode_intent_def throw_opt_def split: cdl_intent.split) 182 apply (rule dcorres_liftME_liftME) 183 apply (rule decode_cnode_corres, auto simp: transform_cap_def)[1] 184 apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def) 185 apply (clarsimp simp: throw_opt_def get_cnode_intent_def split: cdl_intent.split) 186 apply (rule absorb_imp,clarsimp)+ 187 apply (rule dcorres_free_throw) 188 apply (subst decode_cnode_label_not_match) 189 apply simp+ 190done 191 192(* Decoding TCB invocations is equivalent. *) 193lemma decode_invocation_tcbcap_corres: 194 "\<lbrakk> Some intent = transform_intent (invocation_type label') args'; 195 invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; 196 invoked_cap = transform_cap invoked_cap'; 197 excaps = transform_cap_list excaps'; 198 invoked_cap' = cap.ThreadCap a \<rbrakk> \<Longrightarrow> 199 dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top> 200 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 201 (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" 202 apply(case_tac "\<exists> ti. intent = (TcbIntent ti) ") 203 apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) 204 apply (clarsimp simp: throw_opt_def get_cnode_intent_def get_tcb_intent_def split: cdl_intent.split) 205 apply (rule corres_rel_imp[OF decode_tcb_corres],simp+) 206 apply (case_tac x) 207 apply (clarsimp simp:cdl_invocation_relation_def translate_invocation_def)+ 208 209 apply (clarsimp simp:Decode_D.decode_invocation_def throw_opt_def get_tcb_intent_def Decode_A.decode_invocation_def 210 split:cdl_intent.splits) 211 apply (rule absorb_imp,clarsimp)+ 212 apply (rule dcorres_free_throw) 213 apply (rule decode_tcb_cap_label_not_match) 214 apply (drule sym,clarsimp) 215 apply simp 216done 217 218lemma fst_hd_map_eq: "\<lbrakk> xs \<noteq> []; fst (hd xs) = x \<rbrakk> \<Longrightarrow> fst (hd (map (\<lambda>(x, y). (f x, g y)) xs)) = f x" 219 apply (case_tac xs) 220 apply (auto simp: fst_def hd_def split: list.splits) 221 done 222 223lemma decode_domain_corres: 224 "\<lbrakk> Some (DomainIntent i) = transform_intent (invocation_type label') args'; 225 excaps = transform_cap_list excaps' \<rbrakk> \<Longrightarrow> 226 dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). Invocations_A.invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) \<top> \<top> 227 (Tcb_D.decode_domain_invocation excaps i) 228 (Decode_A.decode_domain_invocation label' args' excaps')" 229 apply (unfold Tcb_D.decode_domain_invocation_def Decode_A.decode_domain_invocation_def) 230 apply (unfold transform_cap_list_def) 231 apply (case_labels "invocation_type label'"; simp) 232 apply (clarsimp simp: transform_intent_def option_map_def 233 split: option.splits)+ 234 defer 235 apply (clarsimp simp: transform_intent_def option_map_def split: option.splits)+ 236 apply (clarsimp simp: transform_intent_domain_def) 237 apply (case_tac "args'") 238 apply simp 239 apply (clarsimp simp: bindE_def lift_def) 240 apply (rule_tac Q'="\<lambda>rv s. case rv of Inr b \<Rightarrow> ucast a = b | _ \<Rightarrow> True" in corres_symb_exec_r) 241 apply (case_tac "rv") 242 apply (simp add: lift_def) 243 apply (rule corres_alternate2, simp) 244 apply (simp add: lift_def) 245 apply (fold bindE_def) 246 apply (rule dcorres_whenE_throwError_abstract') 247 apply (rule corres_alternate2) 248 apply simp 249 apply (case_tac "fst (hd (excaps'))"; simp) 250 apply ((rule corres_alternate2, simp)+)[6] 251 apply (rule corres_alternate1) 252 apply (clarsimp simp: returnOk_def cdl_invocation_relation_def translate_invocation_def split: list.splits) 253 apply (simp add: fst_hd_map_eq) 254 apply (rule corres_alternate2, simp)+ 255 apply (rule validE_cases_valid) 256 apply (wp whenE_inv| simp)+ 257 done 258 259lemma decode_domain_cap_label_not_match: 260 "\<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'\<rbrakk> 261 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>" 262 apply (case_tac "invocation_type label' = DomainSetSet") 263 apply (clarsimp simp: Decode_A.decode_domain_invocation_def transform_intent_def)+ 264 apply (clarsimp simp: transform_intent_domain_def split: option.splits list.splits) 265 apply wp 266 apply (simp add: Decode_A.decode_domain_invocation_def) 267 apply wp 268 done 269 270lemma decode_invocation_domaincap_corres: 271 "\<lbrakk> Some intent = transform_intent (invocation_type label) args; 272 invoked_cap_ref = transform_cslot_ptr slot; 273 invoked_cap = transform_cap cap; 274 excaps = transform_cap_list excaps'; 275 cap = cap.DomainCap\<rbrakk> 276 \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top> 277 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 278 (Decode_A.decode_invocation label args cap_index slot cap excaps')" 279 apply (case_tac "\<exists>ti. intent = (DomainIntent ti)") 280 apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) 281 apply (clarsimp simp: throw_opt_def get_domain_intent_def split: cdl_intent.split) 282 apply (rule corres_rel_imp[OF decode_domain_corres],simp+) 283 apply (clarsimp simp:Decode_D.decode_invocation_def throw_opt_def get_domain_intent_def Decode_A.decode_invocation_def 284 split:cdl_intent.splits) 285 apply (rule absorb_imp,clarsimp)+ 286 apply (rule dcorres_free_throw) 287 apply (rule decode_domain_cap_label_not_match) 288 apply (drule sym,clarsimp) 289 done 290 291(* Decoding IRQ Control invocations is equivalent. *) 292lemma decode_invocation_irqcontrolcap_corres: 293 "\<lbrakk> Some intent = transform_intent (invocation_type label') args'; 294 295 invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; 296 invoked_cap = transform_cap invoked_cap'; 297 excaps = transform_cap_list excaps'; 298 invoked_cap' = cap.IRQControlCap \<rbrakk> \<Longrightarrow> 299 dcorres (dc \<oplus> cdl_invocation_relation) 300 \<top> 301 (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. valid_cap (fst e) s) and valid_global_refs and valid_idle and valid_etcbs) 302 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 303 (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" 304 apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) 305 apply(case_tac "\<exists> ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'") 306 apply(erule exE, rotate_tac -1, drule sym) 307 apply(clarsimp simp: throw_opt_def get_irq_control_intent_def) 308 apply (rule dcorres_liftME_liftME) 309 apply (rule decode_irq_control_corres, auto simp: transform_cap_def)[1] 310 apply (clarsimp simp: cdl_irq_control_invocation_relation_def) 311 apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def) 312 apply (rule corres_guard_imp) 313 apply (clarsimp simp: throw_opt_def split: cdl_intent.split option.splits) 314 apply (auto simp: get_irq_control_intent_def split: cdl_intent.split intro!: decode_irq_control_error_corres) 315 done 316 317(* Decoding IRQ Handler invocations is equivalent. *) 318lemma decode_invocation_irqhandlercap_corres: 319 "\<lbrakk> Some intent = transform_intent (invocation_type label') args'; 320 invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; 321 invoked_cap = transform_cap invoked_cap'; 322 excaps = transform_cap_list excaps'; 323 invoked_cap' = cap.IRQHandlerCap x \<rbrakk> \<Longrightarrow> 324 dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top> 325 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 326 (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" 327 apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) 328 apply (clarsimp simp: throw_opt_def get_irq_handler_intent_def split: option.splits) 329 apply (rule conjI) 330 apply (auto simp: decode_irq_handler_invocation_def transform_intent_def 331 split del: if_split 332 split: invocation_label.splits cdl_intent.splits list.splits)[1] 333 apply clarsimp 334 apply (simp split: cdl_intent.splits) 335 apply (rule corres_rel_imp) 336 apply (erule decode_irq_handler_corres, simp+)[1] 337 apply clarsimp 338 apply (case_tac xa, simp) 339 apply (simp add: cdl_invocation_relation_def 340 cdl_irq_handler_invocation_relation_def 341 translate_invocation_def) 342 done 343 344lemma transform_type_eq_None: 345 "(transform_type a = None) \<Longrightarrow> (data_to_obj_type a = throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0))" 346 apply (clarsimp simp:data_to_obj_type_def transform_type_def split:if_split_asm) 347 apply (simp add:unat_arith_simps) 348 apply (clarsimp simp:arch_data_to_obj_type_def) 349 apply (rule conjI,arith,clarsimp)+ 350 done 351 352lemma transform_intent_untyped_cap_None: 353 "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap dev w n idx\<rbrakk> 354 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" 355 including no_pre 356 apply (clarsimp simp:Decode_A.decode_invocation_def) 357 apply wp 358 apply (case_tac "invocation_type label") 359 (* 43 subgoals *) 360 apply (clarsimp simp:Decode_A.decode_untyped_invocation_def unlessE_def) 361 apply wp+ 362 apply (clarsimp simp:transform_intent_def Decode_A.decode_untyped_invocation_def unlessE_def split del:if_split) 363 apply (clarsimp simp:transform_intent_untyped_retype_def split del:if_split) 364 apply (case_tac "args") 365 apply (clarsimp,wp)[1] 366 apply (clarsimp split:list.split_asm split del:if_split) 367 apply (wp+)[5] 368 apply (clarsimp simp: transform_type_eq_None split del:if_split split:option.splits) 369 apply (wp|clarsimp simp:whenE_def|rule conjI)+ 370 apply (clarsimp simp: Decode_A.decode_untyped_invocation_def unlessE_def split del:if_split,wp)+ 371 done 372 373lemma transform_intent_cnode_cap_None: 374 "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap w n list\<rbrakk> 375 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" 376 apply (clarsimp simp:Decode_A.decode_invocation_def) 377 apply (simp add: Decode_A.decode_cnode_invocation_def unlessE_def upto_enum_def 378 fromEnum_def toEnum_def enum_invocation_label 379 whenE_def) 380 apply (intro conjI impI; 381 clarsimp simp: transform_intent_def transform_cnode_index_and_depth_def 382 transform_intent_cnode_copy_def 383 transform_intent_cnode_mint_def transform_intent_cnode_move_def 384 transform_intent_cnode_mutate_def transform_intent_cnode_rotate_def 385 split: list.split_asm; 386 (solves \<open>wpsimp\<close>)?) 387 done 388 389lemma transform_intent_thread_cap_None: 390 "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.ThreadCap w\<rbrakk> 391 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" 392 including no_pre 393 apply (clarsimp simp:Decode_A.decode_invocation_def) 394 apply wp+ 395 apply (simp add:Decode_A.decode_tcb_invocation_def) 396 apply (case_tac "invocation_type label") 397 apply simp_all 398 apply wp+ 399 apply (clarsimp simp: transform_intent_def decode_read_registers_def decode_write_registers_def 400 decode_copy_registers_def decode_tcb_configure_def decode_set_priority_def 401 decode_set_mcpriority_def decode_set_sched_params_def 402 decode_set_ipc_buffer_def transform_intent_tcb_defs 403 split: list.split_asm 404 | wp+)+ 405 apply (clarsimp simp: transform_intent_def decode_set_space_def decode_bind_notification_def 406 decode_unbind_notification_def transform_intent_tcb_set_space_def 407 split: list.split_asm 408 , wp+ 409 | clarsimp simp: transform_intent_def)+ 410 done 411 412lemma transform_intent_irq_control_None: 413 "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.IRQControlCap\<rbrakk> 414 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, 415 \<lbrace>\<lambda>x. (=) s\<rbrace>" 416 including no_pre 417 apply (clarsimp simp:Decode_A.decode_invocation_def) 418 apply wp 419 apply (clarsimp simp:decode_irq_control_invocation_def arch_decode_irq_control_invocation_def 420 split del:if_split) 421 apply (case_tac "invocation_type label") 422 apply (clarsimp, wp)+ 423 apply (clarsimp simp:transform_intent_issue_irq_handler_def transform_intent_def 424 split:list.split_asm split del:if_split,wp+) 425 apply (clarsimp, wp)+ 426 apply (rename_tac arch_label) 427 apply (case_tac "arch_label") 428 apply (clarsimp, wp)+ 429 apply (clarsimp simp:arch_transform_intent_issue_irq_handler_def transform_intent_def 430 split:list.split_asm split del:if_split,wp+) 431 done 432 433lemma transform_intent_irq_handler_None: 434 "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.IRQHandlerCap w\<rbrakk> 435 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" 436 apply (clarsimp simp:Decode_A.decode_invocation_def) 437 apply (wp) 438 apply (clarsimp simp:decode_irq_handler_invocation_def|rule conjI)+ 439 apply (clarsimp simp:transform_intent_def split: list.splits)+ 440 apply (clarsimp simp:transform_intent_def |rule conjI | wp)+ 441done 442 443lemma transform_intent_zombie_cap_None: 444 "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.Zombie w option n\<rbrakk> 445 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" 446 apply (clarsimp simp:Decode_A.decode_invocation_def) 447 apply (wp) 448done 449 450lemma transform_intent_domain_cap_None: 451 "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> 452 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" 453 including no_pre 454 apply (clarsimp simp: Decode_A.decode_invocation_def) 455 apply wp 456 apply (case_tac excaps, simp_all) 457 apply (clarsimp simp: decode_domain_invocation_def) 458 apply (case_tac args, simp_all) 459 apply (wp whenE_inv whenE_inv[THEN valid_validE] | simp)+ 460 apply (clarsimp simp: decode_domain_invocation_def) 461 apply (case_tac args, simp_all) 462 apply ((wp whenE_inv whenE_inv[THEN valid_validE] | simp)+)[1] 463 apply (case_tac "invocation_type label \<noteq> DomainSetSet", simp_all) 464 apply wp 465 apply (clarsimp simp: transform_intent_def transform_intent_domain_def) 466 done 467 468lemma transform_intent_arch_cap_None: 469 "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.ArchObjectCap arch_cap\<rbrakk> 470 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" 471 including no_pre 472 apply (clarsimp simp:Decode_A.decode_invocation_def) 473 apply wp 474 apply (simp add: arch_decode_invocation_def split del: if_split) 475 apply (case_tac arch_cap) 476 apply (case_labels "invocation_type label"; simp split del: if_split, wp?) 477 apply (clarsimp split:if_splits | rule conjI)+ 478 apply (case_tac "excaps ! 0") 479 apply (clarsimp split:cap.splits | rule conjI | wp)+ 480 apply (clarsimp split:arch_cap.splits | rule conjI | wp)+ 481 apply ((clarsimp simp:transform_intent_def | wp) +)[2] 482 apply (case_labels "invocation_type label"; 483 simp add:arch_decode_invocation_def split del: if_split; wp?) 484 apply (case_tac "excaps ! 0") 485 apply (clarsimp simp:transform_intent_def transform_cnode_index_and_depth_def split:list.split_asm) 486 apply wp+ 487 apply (case_labels "invocation_type label"; 488 simp add: arch_decode_invocation_def isPageFlushLabel_def 489 split del: if_split, wp?) 490 apply (clarsimp simp: transform_intent_def transform_intent_page_map_def 491 split: list.split_asm ) 492 apply wp+ 493 apply (clarsimp | rule conjI)+ 494 apply (case_tac "excaps ! 0") 495 apply (clarsimp simp:transform_intent_def transform_intent_page_remap_def split:list.split_asm) 496 apply ((clarsimp simp:transform_intent_def | wp)+) 497 apply (case_labels "invocation_type label"; simp) 498 apply (intro conjI impI | wp)+ 499 apply (clarsimp | rule conjI)+ 500 apply (clarsimp simp: transform_intent_def transform_intent_page_table_map_def 501 split: list.split_asm) 502 apply (intro conjI impI | wp)+ 503 apply ((clarsimp simp: transform_intent_def split: list.split_asm | wp)+)[1] 504 apply (case_labels "invocation_type label"; simp add: isPDFlushLabel_def) 505 apply (wp)+ 506 done 507 508lemma decode_invocation_error_branch: 509 "\<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap)\<rbrakk> 510 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>x. (=) s\<rbrace>" 511 apply (case_tac cap) 512 apply (simp_all add:ep_related_cap_def transform_cap_def split:if_split_asm) 513 apply (clarsimp simp:Decode_A.decode_invocation_def,wp) 514 apply (rule transform_intent_untyped_cap_None,fastforce+) 515 apply (clarsimp simp:Decode_A.decode_invocation_def,wp) 516 apply (rule transform_intent_cnode_cap_None,fastforce+) 517 apply (rule transform_intent_thread_cap_None,fastforce+) 518 apply (rule transform_intent_domain_cap_None,fastforce+) 519 apply (rule transform_intent_irq_control_None,fastforce+) 520 apply (rule transform_intent_irq_handler_None,fastforce+) 521 apply (rule transform_intent_zombie_cap_None,fastforce+) 522 apply (rule transform_intent_arch_cap_None,fastforce+) 523 done 524 525lemma decode_invocation_ep_related_branch: 526 "\<lbrakk>ep_related_cap (transform_cap cap);\<not> is_master_reply_cap cap\<rbrakk> 527 \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top> 528 (Decode_D.decode_invocation (transform_cap cap) (transform_cslot_ptr ref) caps intent) 529 (Decode_A.decode_invocation label args index ref cap caps')" 530 apply (clarsimp simp:ep_related_cap_def transform_cap_def split:cdl_cap.split_asm cap.split_asm arch_cap.split_asm) 531 apply (clarsimp simp:Decode_D.decode_invocation_def Decode_A.decode_invocation_def | rule conjI)+ 532 apply (rule corres_guard_imp[OF dcorres_returnOk],simp add:cdl_invocation_relation_def translate_invocation_def) 533 apply simp+ 534 apply (clarsimp simp:Decode_D.decode_invocation_def Decode_A.decode_invocation_def split:if_split_asm | rule conjI)+ 535 apply (rule corres_guard_imp[OF dcorres_returnOk]) 536 apply (simp add:cdl_invocation_relation_def translate_invocation_def)+ 537 apply (clarsimp simp:Decode_D.decode_invocation_def Decode_A.decode_invocation_def is_master_reply_cap_def | rule conjI)+ 538 apply (rule corres_guard_imp[OF dcorres_returnOk]) 539 apply (simp add:cdl_invocation_relation_def translate_invocation_def)+ 540 done 541 542(* 543 * Decoding zombies invocations is equivalent. 544 * 545 *) 546lemma decode_invocation_zombiecap_corres: 547 "\<lbrakk> Some intent = transform_intent (invocation_type label') args'; 548 invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; 549 invoked_cap = transform_cap invoked_cap'; 550 excaps = transform_cap_list excaps'; 551 invoked_cap' = cap.Zombie x y z \<rbrakk> \<Longrightarrow> 552 dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top> 553 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 554 (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" 555 by (simp add:Decode_A.decode_invocation_def Decode_D.decode_invocation_def) 556 557(* 558 * Show that decoding of invocations corresponds. 559 *) 560lemma decode_invocation_corres: 561 "\<lbrakk> (Some intent) = transform_intent (invocation_type label) args; 562 invoked_cap_ref = transform_cslot_ptr slot; 563 invoked_cap = transform_cap cap; 564 excaps = transform_cap_list excaps' \<rbrakk> \<Longrightarrow> 565 dcorres (dc \<oplus> cdl_invocation_relation) \<top> 566 (invs and valid_cap cap and (\<lambda>s. \<forall>e\<in>set excaps'. valid_cap (fst e) s) 567 and (cte_wp_at (Not \<circ> is_master_reply_cap) slot 568 and cte_wp_at (diminished cap) slot) 569 and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at (diminished (fst x)) (snd x) s) 570 and valid_etcbs) 571 (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) 572 (Decode_A.decode_invocation label args cap_index slot cap excaps')" 573 apply(case_tac cap) 574 apply (rule corres_guard_imp,rule decode_invocation_nullcap_corres, fastforce+)[1] 575 apply (rule corres_guard_imp,rule decode_invocation_untypedcap_corres, 576 (fastforce elim: cte_wp_at_weakenE)+)[1] 577 apply (rule corres_guard_imp,rule decode_invocation_endpointcap_corres, fastforce+)[1] 578 apply (rule corres_guard_imp,rule decode_invocation_notificationcap_corres, fastforce+)[1] 579 apply (rule corres_guard_imp,rule decode_invocation_replycap_corres, fastforce+)[1] 580 apply (rule corres_guard_imp,rule decode_invocation_cnodecap_corres, fastforce+)[1] 581 apply (rule corres_guard_imp, rule decode_invocation_tcbcap_corres, fastforce+)[1] 582 apply (rule corres_guard_imp, rule decode_invocation_domaincap_corres, fastforce+)[1] 583 apply (rule corres_guard_imp, rule decode_invocation_irqcontrolcap_corres, fastforce+)[1] 584 apply (rule corres_guard_imp,rule decode_invocation_irqhandlercap_corres, fastforce+)[1] 585 apply (rule corres_guard_imp,rule decode_invocation_zombiecap_corres, fastforce+)[1] 586 apply (rule corres_guard_imp) 587 apply (rule corres_rel_imp) 588 apply (rule decode_invocation_archcap_corres, fastforce+)[1] 589 apply clarsimp 590 apply (case_tac x, simp) 591 apply (clarsimp simp: cdl_invocation_relation_def) 592 apply simp 593 apply simp 594 done 595 596lemma ct_running_not_idle_etc: 597 "\<lbrakk> invs s; ct_running s \<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s \<and> thread_is_running (cur_thread s) s" 598 apply (simp add: not_idle_thread_def ct_in_state_def) 599 apply (subgoal_tac "valid_idle s") 600 apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) 601 apply (clarsimp simp: invs_def valid_state_def) 602 done 603 604lemma ct_active_not_idle_etc: 605 "\<lbrakk> invs s; ct_active s \<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s" 606 apply (simp add: not_idle_thread_def ct_in_state_def) 607 apply (subgoal_tac "valid_idle s") 608 apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) 609 apply (clarsimp simp: invs_def valid_state_def) 610 done 611 612lemma dcorres_set_eobject_tcb: 613 "\<lbrakk> \<exists>tcb'. (transform_tcb (machine_state s') p' tcb' etcb = Tcb tcb \<and> kheap s' p' = Some (TCB tcb')); 614 p' \<noteq> idle_thread s'; kheap s' p' \<noteq> None; ekheap s' p' \<noteq> None \<rbrakk> \<Longrightarrow> 615 dcorres dc ((=) (transform s')) ((=) s') 616 (KHeap_D.set_object p' (Tcb tcb )) 617 (set_eobject p' etcb)" 618 apply (clarsimp simp: corres_underlying_def set_eobject_def in_monad) 619 apply (clarsimp simp: KHeap_D.set_object_def simpler_modify_def) 620 apply (clarsimp simp: transform_def transform_current_thread_def transform_cdt_def transform_asid_table_def) 621 apply (clarsimp simp: transform_objects_def) 622 apply (rule ext) 623 apply clarsimp 624 apply (clarsimp simp: option_map_def restrict_map_def map_add_def) 625 done 626 627lemma invoke_domain_corres: 628 "\<lbrakk> i = cdl_invocation.InvokeDomain (SetDomain word1 word2); 629 i' = Invocations_A.invocation.InvokeDomain word1 word2\<rbrakk> 630 \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) 631 (invs and ct_active and valid_pdpt_objs and valid_etcbs and 632 invocation_duplicates_valid (Invocations_A.invocation.InvokeDomain word1 word2) and 633 (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) 634 (Tcb_D.invoke_domain (SetDomain word1 word2)) (Tcb_A.invoke_domain word1 word2)" 635 apply (clarsimp simp: Tcb_D.invoke_domain_def Tcb_A.invoke_domain_def) 636 apply (rule corres_bind_return_r) 637 apply (clarsimp simp: Tcb_D.set_domain_def Tcb_A.set_domain_def) 638 apply (rule corres_symb_exec_r) 639 apply (rule_tac Q=\<top> and Q'="tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)" in dcorres_rhs_noop_above) 640 apply (rule tcb_sched_action_dcorres) 641 apply (rule dcorres_rhs_noop_below_True) 642 apply (rule corres_noop) 643 apply (wp reschedule_required_transform tcb_sched_action_transform | simp)+ 644 apply (simp add: update_thread_def ethread_set_def thread_set_domain_def) 645 apply (rule dcorres_gets_the) 646 apply clarsimp 647 apply (drule get_tcb_at) 648 apply (clarsimp simp: opt_object_tcb transform_tcb_def) 649 apply (rule dcorres_set_eobject_tcb[simplified dc_def]) 650 apply (frule get_tcb_SomeD) 651 apply (clarsimp simp: transform_tcb_def) 652 apply simp 653 apply (frule get_tcb_SomeD) 654 apply simp 655 apply (clarsimp simp: get_etcb_def split:option.splits) 656 apply clarsimp 657 apply (drule get_tcb_at) 658 apply (clarsimp simp:opt_object_tcb) 659 apply wp+ 660 apply simp 661 apply wp 662 apply simp 663 done 664 665(* 666 * Show that invocation of a cap corresponds. 667 *) 668lemma perform_invocation_corres: 669 "\<lbrakk>cdl_invocation_relation i i'\<rbrakk> \<Longrightarrow> 670 dcorres (dc \<oplus> dc) 671 \<top> (invs and ct_active and valid_pdpt_objs and valid_etcbs 672 and invocation_duplicates_valid i' and valid_invocation i') 673 (Syscall_D.perform_invocation call block i) 674 (Syscall_A.perform_invocation block call i')" 675 apply (clarsimp simp: cdl_invocation_relation_def) 676 apply (case_tac i') 677 apply (simp_all add: translate_invocation_def split: Invocations_A.invocation.splits) 678(* untyped *) 679 apply (simp add: liftME_def[symmetric]) 680 apply (rule corres_guard_imp, rule invoke_untyped_corres) 681 apply clarsimp 682 apply clarsimp 683 684(* send_ipc *) 685 apply (clarsimp simp:invoke_endpoint_def) 686 apply (rule corres_guard_imp) 687 apply (rule corres_split[OF _ get_cur_thread_corres]) 688 apply (rule corres_dummy_return_l) 689 apply (rule corres_split[OF _ send_sync_ipc_corres]) 690 apply (rule corres_trivial[OF corres_free_return]) 691 apply (wp|clarsimp)+ 692 apply (clarsimp simp:ct_in_state_def obj_at_def pred_tcb_at_def not_idle_thread_def 693 valid_state_def invs_def valid_idle_def) 694 695(* send_signal *) 696 apply (clarsimp simp:invoke_notification_def liftE_bindE) 697 apply (clarsimp simp:liftE_def bind_assoc returnOk_def) 698 apply (rule corres_guard_imp) 699 apply (rule corres_split[OF _ send_signal_corres]) 700 apply (rule corres_trivial) 701 apply (simp add:dc_def corres_free_return) 702 apply (wp | clarsimp)+ 703 704(* invoke_reply *) 705 apply (rename_tac word a b) 706 apply (clarsimp simp:invoke_reply_def) 707 apply (rule corres_guard_imp) 708 apply (rule corres_split[OF _ get_cur_thread_corres]) 709 apply clarsimp 710 apply (rule corres_dummy_return_l) 711 apply (rule corres_split) 712 apply (rule corres_trivial[OF corres_free_return]) 713 apply (rule do_reply_transfer_corres, simp) 714 apply (wp|clarsimp)+ 715 apply (simp add: ct_active_not_idle_etc) 716 apply (rule conjI, fastforce)+ 717 apply (subgoal_tac "valid_idle s \<and> valid_reply_caps s \<and> has_reply_cap word s") 718 apply clarsimp 719 apply (drule (1) valid_reply_capsD) 720 apply (clarsimp simp: valid_idle_def not_idle_thread_def pred_tcb_at_def obj_at_def) 721 apply (fastforce simp: has_reply_cap_def) 722 723(* invoke_tcb *) 724 apply (rule corres_guard_imp) 725 apply (rule invoke_tcb_corres,simp+) 726 727(* invoke_domain *) 728 apply (rule corres_guard_imp) 729 apply (rule invoke_domain_corres,simp+) 730 731(* invoke_cnode *) 732 apply (rule corres_guard_imp) 733 apply (clarsimp simp:bindE_def returnOk_def lift_def bind_assoc) 734 apply (rule corres_dummy_return_l) 735 apply (rule corres_split[OF _ invoke_cnode_corres]) 736 apply (clarsimp simp:lift_def,case_tac rv',simp add: throwError_def) 737 apply (simp) 738 apply (rule hoare_triv[of \<top>], rule hoare_post_taut)+ 739 apply clarsimp+ 740 741(* invoke_irq_control *) 742 subgoal for irq_control_invocation 743 apply (simp add:liftE_def bindE_def) 744 apply (case_tac irq_control_invocation) 745 (* generic *) 746 apply (rule corres_guard_imp) 747 apply (rule corres_split[where r'=dc]) 748 apply (rule_tac F = "\<exists>x. rv' = Inr x" in corres_gen_asm2) 749 apply (rule corres_trivial) 750 apply (clarsimp simp:lift_def returnOk_def) 751 apply (rule dcorres_invoke_irq_control) 752 apply (rule hoare_triv[of \<top>], rule hoare_post_taut)+ 753 apply ((wp|simp add: liftE_def)+) 754 (* arch *) 755 apply (rename_tac arch_label) 756 apply (case_tac arch_label) 757 apply (rule corres_guard_imp) 758 apply (rule corres_split[where r'=dc]) 759 apply (rule_tac F = "\<exists>x. rv' = Inr x" in corres_gen_asm2) 760 apply (rule corres_trivial) 761 apply (clarsimp simp:lift_def returnOk_def) 762 apply (rule dcorres_arch_invoke_irq_control[simplified]) 763 apply (rule hoare_triv[of \<top>], rule hoare_post_taut) 764 apply ((wp|simp add: liftE_def)+) 765 done 766 767(* invoke_irq_handler *) 768 apply (clarsimp simp:liftE_bindE,simp add:liftE_def returnOk_def) 769 apply (rule corres_guard_imp) 770 apply (rule corres_split[OF corres_trivial]) 771 apply clarsimp 772 apply (rule dcorres_invoke_irq_handler) 773 apply (wp|clarsimp)+ 774 775(* invoke_arch *) 776 apply (rule corres_guard_imp[OF invoke_arch_corres],fastforce+) 777done (* invoke_tcb_corres *) 778 779lemma sfi_generate_pending: 780 "\<lbrace>st_tcb_at(\<lambda>st. \<not>(generates_pending st)) thread\<rbrace> Ipc_A.send_fault_ipc thread ft 781 \<lbrace>\<lambda>t. \<top>\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. \<not> (generates_pending st)) thread\<rbrace>" 782 apply (clarsimp simp:send_fault_ipc_def Let_def lookup_cap_def) 783 apply (wp hoare_drop_imps hoare_allI|wpc|clarsimp|rule hoare_conjI)+ 784 done 785 786lemma dcorres_handle_double_fault: 787 "dcorres dc \<top> (valid_mdb and not_idle_thread thread and valid_idle and valid_etcbs) 788 (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap) 789 (handle_double_fault thread ft' ft'a)" 790 apply (simp add:handle_double_fault_def ) 791 apply (rule corres_guard_imp) 792 apply (rule set_thread_state_corres ) 793 apply simp+ 794 done 795 796lemma handle_fault_corres: 797 "dcorres dc \<top> 798 (\<lambda>s. cur_thread s = thread \<and> not_idle_thread thread s \<and> 799 st_tcb_at active thread s \<and> valid_fault ft' \<and> 800 invs s \<and> valid_irq_node s \<and> valid_etcbs s) 801 Endpoint_D.handle_fault 802 (Ipc_A.handle_fault thread ft')" 803 apply (simp add:Endpoint_D.handle_fault_def Ipc_A.handle_fault_def) 804 apply (rule dcorres_gets_the) 805 apply (clarsimp dest!:get_tcb_SomeD) 806 apply (frule(1) valid_etcbs_tcb_etcb, clarsimp) 807 apply (rule corres_guard_imp) 808 apply (rule corres_split_catch[where r=dc and f = dc]) 809 apply (rule_tac F = "obj = cur_thread s'" in corres_gen_asm2) 810 apply simp 811 apply (rule dcorres_handle_double_fault) 812 apply (rule_tac tcb = obj' and etcb=etcb in send_fault_ipc_corres) 813 apply (clarsimp simp:transform_def transform_current_thread_def 814 not_idle_thread_def) 815 apply (wp) 816 apply (simp add:send_fault_ipc_def not_idle_thread_def Let_def) 817 apply (wp hoare_drop_imps hoare_vcg_ball_lift | wpc)+ 818 apply (rule_tac Q'="\<lambda>r s. invs s \<and> valid_etcbs s \<and> obj\<noteq> idle_thread s \<and> obj = cur_thread s'" 819 in hoare_post_imp_R) 820 apply wp 821 apply (clarsimp simp:invs_mdb invs_valid_idle) 822 apply wp 823 apply simp 824 apply (clarsimp simp:obj_at_def transform_def 825 invs_mdb invs_valid_idle 826 transform_current_thread_def not_idle_thread_def) 827 apply (clarsimp dest!:get_tcb_SomeD 828 simp: generates_pending_def not_idle_thread_def st_tcb_at_def obj_at_def)+ 829 apply (auto simp:transform_def transform_current_thread_def 830 not_idle_thread_def split:Structures_A.thread_state.splits) 831 done 832 833lemma get_tcb_mrs_wp: 834 "\<lbrace>ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some (op_buf)) and (=) sa\<rbrace> 835 get_mrs thread (op_buf) (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)) 836 \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace>" 837 apply (case_tac op_buf) 838 apply (clarsimp simp:get_mrs_def thread_get_def gets_the_def arch_tcb_get_registers_def) 839 apply (wp|wpc)+ 840 apply (clarsimp simp:get_tcb_mrs_def Let_def) 841 apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length] split del:if_split) 842 apply (clarsimp simp:get_tcb_message_info_def get_ipc_buffer_words_empty) 843 apply (clarsimp dest!:get_tcb_SomeD simp:obj_at_def) 844 apply (clarsimp simp:get_mrs_def thread_get_def gets_the_def arch_tcb_get_registers_def) 845 apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length] split del:if_split) 846 apply (wp|wpc)+ 847 apply (rule_tac P = "tcb = obj" in hoare_gen_asm) 848 apply (clarsimp simp: get_tcb_mrs_def Let_def get_tcb_message_info_def Suc_leI[OF msg_registers_lt_msg_max_length] split del:if_split) 849 apply (rule_tac Q="\<lambda>buf_mrs s. buf_mrs = 850 (get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))" 851 in hoare_strengthen_post) 852 apply (rule get_ipc_buffer_words[where thread=thread ]) 853 apply simp 854 apply wp 855 apply (clarsimp simp:get_tcb_SomeD obj_at_def) 856 apply simp 857done 858 859lemma get_ipc_buffer_noop: 860 "\<lbrace>P and (\<lambda>s. \<exists>s'. s = transform s' \<and> tcb_at t s' \<and> valid_etcbs s' \<and> not_idle_thread t s')\<rbrace> 861 get_ipc_buffer t True \<exists>\<lbrace>\<lambda>r. P\<rbrace>" 862 apply (simp add:gets_the_def gets_def bind_assoc get_def split_def get_ipc_buffer_def tcb_at_def 863 exs_valid_def fail_def return_def bind_def assert_opt_def split:cdl_cap.splits) 864 apply clarsimp 865 apply (rule_tac x = "(the (opt_cap (t, tcb_ipcbuffer_slot) s),s)" for s in bexI) 866 apply (rule conjI|fastforce simp:fail_def return_def split:option.splits)+ 867 apply (clarsimp split:option.splits simp:fail_def return_def) 868 apply (frule(1) valid_etcbs_get_tcb_get_etcb) 869 apply (clarsimp simp: opt_cap_tcb not_idle_thread_def) 870 done 871 872lemma dcorres_reply_from_kernel: 873 "dcorres dc \<top> (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) (corrupt_ipc_buffer oid True) (reply_from_kernel oid msg_rv)" 874 apply (simp add:reply_from_kernel_def) 875 apply (case_tac msg_rv) 876 apply (clarsimp simp:corrupt_ipc_buffer_def) 877 apply (rule dcorres_expand_pfx) 878 apply (rule_tac Q' = "\<lambda>r. (=) s' and K_bind (evalMonad (lookup_ipc_buffer True oid) s' = Some r)" 879 in corres_symb_exec_r) 880 apply (rule dcorres_expand_pfx) 881 apply (clarsimp) 882 apply (case_tac rv) 883 apply (rule corres_symb_exec_l) 884 apply (rule_tac F="rva = None" in corres_gen_asm) 885 apply clarsimp 886 apply (rule corres_guard_imp) 887 apply (rule corres_corrupt_tcb_intent_dupl) 888 apply (rule corres_split[OF _ set_register_corres]) 889 unfolding K_bind_def 890 apply (rule corres_corrupt_tcb_intent_dupl) 891 apply (rule corres_split[OF _ set_mrs_corres_no_recv_buffer]) 892 unfolding K_bind_def 893 apply (rule set_message_info_corres) 894 apply (wp | clarsimp simp:not_idle_thread_def)+ 895 apply (wp get_ipc_buffer_noop, clarsimp) 896 apply (fastforce simp: not_idle_thread_def) 897 apply (simp add: pred_conj_def) 898 apply (strengthen refl[where t=True]) 899 apply (wp cdl_get_ipc_buffer_None | simp)+ 900 apply clarsimp 901 apply (drule lookup_ipc_buffer_SomeB_evalMonad) 902 apply clarsimp 903 apply (rule corres_symb_exec_l) 904 apply (rule_tac F = "rv = Some ba" in corres_gen_asm) 905 apply clarsimp 906 apply (rule corrupt_frame_include_self[where y = oid]) 907 apply (rule corres_guard_imp) 908 apply (rule corres_split[OF _ set_register_corres]) 909 unfolding K_bind_def 910 apply (rule_tac y = oid in corrupt_frame_include_self') 911 apply (rule corres_guard_imp) 912 apply (rule corres_split[OF _ dcorres_set_mrs]) 913 unfolding K_bind_def 914 apply (rule set_message_info_corres) 915 apply (wp| simp add:not_idle_thread_def)+ 916 apply (clarsimp simp:not_idle_thread_def) 917 apply (clarsimp simp:invs_def not_idle_thread_def valid_state_def valid_pspace_def 918 ipc_frame_wp_at_def ipc_buffer_wp_at_def obj_at_def) 919 apply (clarsimp simp:cte_wp_at_cases obj_at_def) 920 apply (drule_tac s="cap.ArchObjectCap c" for c in sym) 921 apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def) 922 apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def cte_wp_at_cases) 923 apply (drule_tac s="cap.ArchObjectCap c" for c in sym) 924 apply simp 925 apply (wp get_ipc_buffer_noop, clarsimp) 926 apply fastforce 927 apply simp 928 apply (rule cdl_get_ipc_buffer_Some) 929 apply fastforce 930 apply (simp add:tcb_at_def not_idle_thread_def get_tcb_rev)+ 931 apply wp 932 apply (rule evalMonad_wp) 933 apply (simp add:empty_when_fail_lookup_ipc_buffer weak_det_spec_lookup_ipc_buffer)+ 934 apply (wp|clarsimp)+ 935 done 936 937lemma dcorres_set_intent_error: 938 "dcorres dc \<top> 939 (invs and valid_etcbs and (\<lambda>s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er 940 \<and> ko_at (TCB tcb) oid s) and not_idle_thread oid) (mark_tcb_intent_error oid er) (return a)" 941 apply (clarsimp simp:mark_tcb_intent_error_def bind_assoc 942 gets_the_def update_thread_def gets_def ) 943 apply (rule dcorres_absorb_get_l) 944 apply (clarsimp simp: not_idle_thread_def) 945 apply (frule ko_at_tcb_at) 946 apply (frule(1) tcb_at_is_etcb_at) 947 apply (clarsimp simp:tcb_at_def is_etcb_at_def, fold get_etcb_def) 948 apply (clarsimp simp:opt_object_tcb assert_opt_def transform_tcb_def KHeap_D.set_object_def 949 simpler_modify_def corres_underlying_def) 950 apply (simp add:transform_def return_def) 951 apply (rule ext) 952 apply (clarsimp simp:transform_objects_def transform_tcb_def 953 dest!:get_tcb_SomeD get_etcb_SomeD) 954 apply (simp add:transform_full_intent_def Let_def obj_at_def) 955 done 956 957lemma dcorres_when_r: 958 "\<lbrakk>R \<Longrightarrow> dcorres dc \<top> P l r; \<not> R \<Longrightarrow> dcorres dc \<top> Q l (return ())\<rbrakk> 959 \<Longrightarrow> dcorres dc \<top> (\<lambda>s. (R \<longrightarrow> P s) \<and> (\<not> R \<longrightarrow> Q s)) l (when R r)" 960 by (clarsimp simp:when_def) 961 962lemma evalMonad_from_wp: 963 "\<lbrakk>evalMonad f s = Some a;\<lbrace>P\<rbrace>f\<lbrace> \<lambda>rv s. R rv\<rbrace>;P s;empty_when_fail f;\<And>Q. weak_det_spec Q f \<rbrakk>\<Longrightarrow> R a" 964 apply (clarsimp simp:evalMonad_def valid_def) 965 apply (drule_tac x = "(=) s" in meta_spec) 966 apply (fastforce simp:weak_det_spec_def empty_when_fail_def no_fail_def det_spec_def) 967 done 968 969lemma empty_when_fail_get_mrs: 970 notes option.case_cong_weak [cong] 971 shows "empty_when_fail (get_mrs a b c)" 972 apply (clarsimp simp:get_mrs_def) 973 apply (rule empty_when_fail_compose)+ 974 apply (simp add:empty_when_fail_return split:option.splits)+ 975 apply (rule conjI) 976 apply clarsimp 977 apply (rule empty_when_fail_mapM) 978 apply (simp add:empty_when_fail_load_word_offs weak_det_spec_load_word_offs) 979 apply clarsimp 980 apply (rule empty_when_fail_mapM) 981 apply (simp add:empty_when_fail_load_word_offs weak_det_spec_load_word_offs) 982 apply (clarsimp simp:empty_when_fail_return weak_det_spec_simps split:option.splits) 983 apply (rule conjI) 984 apply clarsimp 985 apply (rule weak_det_spec_mapM) 986 apply (simp add:weak_det_spec_load_word_offs) 987 apply clarsimp 988 apply (rule weak_det_spec_mapM) 989 apply (simp add:weak_det_spec_load_word_offs) 990 apply (simp add:empty_when_fail_thread_get) 991 apply (simp add:weak_det_spec_thread_get) 992 done 993 994lemma weak_det_spec_get_mrs: 995 notes option.case_cong_weak [cong] 996 shows "weak_det_spec P (get_mrs a b c)" 997 apply (clarsimp simp:get_mrs_def) 998 apply (rule weak_det_spec_compose)+ 999 apply (simp add:weak_det_spec_simps split:option.splits)+ 1000 apply (rule conjI) 1001 apply clarsimp 1002 apply (rule weak_det_spec_mapM) 1003 apply (simp add:weak_det_spec_load_word_offs) 1004 apply clarsimp 1005 apply (rule weak_det_spec_mapM) 1006 apply (simp add:weak_det_spec_load_word_offs) 1007 apply (simp add:weak_det_spec_thread_get) 1008 done 1009 1010lemma lookup_cap_and_slot_inv: 1011 "\<lbrace>P\<rbrace> CSpace_A.lookup_cap_and_slot t (to_bl (arch_tcb_context_get (tcb_arch obj'a) cap_register)) \<lbrace>\<lambda>x. P\<rbrace>, \<lbrace>\<lambda>ft s. True\<rbrace>" 1012 apply (simp add:CSpace_A.lookup_cap_and_slot_def) 1013 apply (wp | clarsimp simp:liftE_bindE)+ 1014 done 1015 1016(* We need following lemma because we need to match get_mrs in abstract and cdl_intent_op in capdl after state s is fixed *) 1017lemma decode_invocation_corres': 1018 "\<lbrakk>(\<lambda>(cap, slot, extra) (slot', cap', extra', buffer). 1019 cap = transform_cap cap' \<and> slot = transform_cslot_ptr slot' \<and> extra = transform_cap_list extra') 1020 rv rv'; get_tcb (cur_thread s) s = Some ctcb; ct_running s;invs s\<rbrakk> 1021 \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) \<top> 1022 ((=) s and (\<lambda>(slot,cap,excaps,buffer) s. \<not> is_master_reply_cap (cap) \<and> valid_cap cap s \<and> valid_etcbs s 1023 \<and> evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some buffer 1024 \<and> (\<forall>e\<in> set excaps. s \<turnstile> fst e) \<and> cte_wp_at (Not \<circ> is_master_reply_cap) slot s \<and> cte_wp_at (diminished cap) slot s 1025 \<and> (\<forall>e\<in> set excaps. cte_wp_at (diminished (fst e)) (snd e) s)) rv') 1026 ((\<lambda>(cap, cap_ref, extra_caps). 1027 case_option (if ep_related_cap cap then Decode_D.decode_invocation cap cap_ref extra_caps undefined else Monads_D.throw) 1028 (Decode_D.decode_invocation cap cap_ref extra_caps) 1029 (cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb))) 1030 rv) 1031 ((\<lambda>(slot, cap, extracaps, buffer). 1032 do args \<leftarrow> get_mrs (cur_thread s) buffer (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)); 1033 Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) args 1034 (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) slot cap extracaps 1035 od) 1036 rv')" 1037 apply (rule dcorres_expand_pfx) 1038 apply (clarsimp split del:if_split) 1039 apply (rule_tac Q' ="\<lambda>r ns. ns = s 1040 \<and> r = get_tcb_mrs (machine_state s) ctcb" 1041 in corres_symb_exec_r) 1042 apply (clarsimp split:option.split | rule conjI)+ 1043 apply (rule corres_guard_imp[OF decode_invocation_ep_related_branch]) 1044 apply clarsimp+ 1045 defer 1046 apply clarsimp 1047 apply (rule dcorres_expand_pfx) 1048 apply (rule corres_guard_imp[OF decode_invocation_corres]) 1049 apply (clarsimp simp:transform_full_intent_def Let_def get_tcb_message_info_def)+ 1050 apply (wp get_tcb_mrs_wp | clarsimp)+ 1051 apply (rule dcorres_expand_pfx) 1052 apply (rule dcorres_free_throw[OF decode_invocation_error_branch]) 1053 apply (clarsimp simp:transform_full_intent_def Let_def get_tcb_message_info_def)+ 1054 done 1055 1056lemma reply_from_kernel_error: 1057 notes option.case_cong_weak [cong] 1058 shows 1059 "\<lbrace>tcb_at oid and K (fst e \<le> mask 19 \<and> 0 < fst e = er)\<rbrace>reply_from_kernel oid e 1060 \<lbrace>\<lambda>rv s. (\<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er \<and> 1061 ko_at (TCB tcb) oid s)\<rbrace>" 1062 apply (rule hoare_gen_asm) 1063 apply (case_tac e) 1064 apply (clarsimp simp:reply_from_kernel_def guess_error_def split_def set_message_info_def) 1065 apply (rule hoare_pre) 1066 apply (wp) 1067 apply (simp add:as_user_def split_def set_object_def) 1068 apply (wp set_object_at_obj) 1069 apply (rule hoare_strengthen_post[where Q = "\<lambda>x s. x \<le> mask 12"]) 1070 apply (simp add:set_mrs_def) 1071 apply (wp|wpc)+ 1072 apply (clarsimp simp:setRegister_def simpler_modify_def) 1073 apply (drule get_tcb_SomeD) 1074 apply (rule exI) 1075 apply (rule conjI[rotated]) 1076 apply (simp add:obj_at_def) 1077 apply (simp add:get_tcb_message_info_def data_to_message_info_def word_neq_0_conv mask_def) 1078 apply (simp add:shiftr_over_or_dist le_mask_iff word_neq_0_conv) 1079 apply (subst shiftl_shiftr_id) 1080 apply (simp add:word_bits_def mask_def le_mask_iff[symmetric])+ 1081 apply unat_arith 1082 apply (word_bitwise, simp) 1083 apply (wp hoare_drop_imp hoare_vcg_all_lift)+ 1084 apply clarsimp 1085 apply (rule conjI) 1086 apply (rule word_of_nat_le) 1087 apply (rule le_trans[OF min.cobounded1]) 1088 apply (simp add:mask_def) 1089 apply (rule le_trans) 1090 apply (rule less_imp_le[OF msg_registers_lt_msg_max_length]) 1091 apply (simp add:msg_max_length_def) 1092 apply (rule plus_one_helper) 1093 apply (simp add:mask_def) 1094 apply (rule word_of_nat_less) 1095 apply (simp add:msg_max_length_def) 1096 done 1097 1098lemma liftE_distrib': 1099 "liftE (do x \<leftarrow> A;B x od) = 1100 doE x \<leftarrow> liftE A; 1101 liftE (B x) 1102 odE" 1103 by (simp add:bindE_def liftE_def bind_assoc lift_def) 1104 1105crunch valid_etcbs[wp]: reply_from_kernel valid_etcbs 1106 1107lemma dcorres_reply_from_syscall: 1108 "dcorres (dc \<oplus> dc) \<top> (invs and not_idle_thread thread and valid_idle and valid_etcbs) 1109 (do restart \<leftarrow> has_restart_cap thread; 1110 if restart then liftE ( 1111 (do y \<leftarrow> corrupt_ipc_buffer thread True; 1112 y \<leftarrow>when call (mark_tcb_intent_error thread False); 1113 KHeap_D.set_cap (thread, tcb_pending_op_slot) RunningCap 1114 od )) 1115 else returnOk () 1116 od) 1117 (liftE (do x \<leftarrow> get_thread_state thread; 1118 (case x of 1119 Structures_A.thread_state.Restart \<Rightarrow> 1120 do y \<leftarrow> when call (reply_from_kernel thread (0, reply)); 1121 set_thread_state thread Structures_A.thread_state.Running 1122 od 1123 | _ \<Rightarrow> return ()) od))" 1124 apply (clarsimp simp:get_thread_state_def thread_get_def liftE_distrib' liftE_bindE) 1125 apply (rule dcorres_absorb_gets_the) 1126 apply (simp add:has_restart_cap_def get_thread_def gets_the_def 1127 gets_def bind_assoc liftE_distrib') 1128 apply (rule dcorres_absorb_get_l) 1129 apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) 1130 apply (clarsimp simp:opt_object_tcb not_idle_thread_def 1131 liftE_bindE liftE_distrib' infer_tcb_pending_op_def tcb_slots 1132 transform_tcb_def assert_opt_def when_def returnOk_liftE[symmetric] 1133 split: Structures_A.thread_state.splits) 1134 apply (intro conjI impI) 1135 apply (rule dcorres_returnOk',simp)+ 1136 apply (rule corres_guard_imp) 1137 apply (rule corres_split[OF _ dcorres_reply_from_kernel]) 1138 apply (rule corres_dummy_return_pr) 1139 apply (rule corres_split[OF _ dcorres_set_intent_error]) 1140 apply (simp add:liftE_bindE returnOk_liftE) 1141 apply (rule set_thread_state_corres[unfolded tcb_slots]) 1142 apply (wp rfk_invs reply_from_kernel_error)+ 1143 apply (simp add:not_idle_thread_def) 1144 apply (wp rfk_invs) 1145 apply simp 1146 apply (clarsimp simp: tcb_at_def st_tcb_at_def obj_at_def not_idle_thread_def 1147 dest!: get_tcb_SomeD) 1148 apply (rule corres_dummy_return_pr) 1149 apply (rule corres_guard_imp[OF corres_split[where r' = "dc"]]) 1150 apply (simp add: returnOk_liftE) 1151 apply (rule set_thread_state_corres[unfolded tcb_slots]) 1152 apply (rule dcorres_dummy_corrupt_ipc_buffer) 1153 apply wp+ 1154 apply simp 1155 apply (clarsimp simp: tcb_at_def invs_mdb st_tcb_at_def not_idle_thread_def obj_at_def 1156 dest!: get_tcb_SomeD) 1157 apply (rule dcorres_returnOk', simp)+ 1158 done 1159 1160lemmas mapM_x_def_symmetric = mapM_x_def[symmetric] 1161 1162crunch idle[wp] : send_ipc "\<lambda>s::'z::state_ext state. P (idle_thread s)" 1163 (wp: crunch_wps dxo_wp_weak simp: crunch_simps ignore:clearMemory) 1164 1165crunch idle[wp] : send_signal "\<lambda>s::'z::state_ext state. P (idle_thread s)" 1166 (wp: crunch_wps dxo_wp_weak simp: crunch_simps ignore:clearMemory) 1167 1168crunch idle[wp] : do_reply_transfer "\<lambda>s::'z::state_ext state. P (idle_thread s)" 1169 (wp: crunch_wps dxo_wp_weak simp: crunch_simps ignore:clearMemory) 1170 1171lemma check_cap_at_idle: 1172 "\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> check_cap_at a b (check_cap_at c d (cap_insert new_cap src_slot (target, ref))) 1173 \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>" 1174 apply (rule check_cap_at_stable) 1175 apply wp 1176done 1177 1178lemmas cap_revoke_preservation_flat = cap_revoke_preservation[THEN validE_valid] 1179 1180crunch idle[wp] : invoke_tcb, cap_move, cap_swap, cap_revoke "\<lambda>s::'z::state_ext state. P (idle_thread s)" 1181 (rule: cap_revoke_preservation_flat wp: crunch_wps check_cap_at_idle dxo_wp_weak 1182 simp: crunch_simps ignore: check_cap_at) 1183 1184lemma invoke_cnode_idle: 1185 "\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> invoke_cnode pa \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>" 1186 apply (cases pa) 1187 apply (clarsimp simp:invoke_cnode_def 1188 | wpsimp wp: crunch_wps hoare_vcg_all_lift | rule conjI)+ 1189 done 1190 1191crunch idle[wp] : arch_perform_invocation "\<lambda>s. P (idle_thread s)" 1192 (wp: crunch_wps simp: crunch_simps) 1193 1194lemma invoke_domain_idle: 1195 "\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> invoke_domain t d \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>" 1196 by (clarsimp simp: Tcb_A.invoke_domain_def trans_state_def | wp dxo_wp_weak)+ 1197 1198crunch idle[wp]: "Syscall_A.perform_invocation" "\<lambda>s. P (idle_thread s)" 1199 1200lemma msg_from_syscall_error_simp: 1201 "fst (msg_from_syscall_error rv) \<le> mask 19" 1202 "0 < fst (msg_from_syscall_error rv)" 1203 apply (case_tac rv) 1204 apply (clarsimp simp:mask_def)+ 1205 apply (case_tac rv) 1206 apply simp+ 1207 done 1208 1209lemma not_master_reply_cap_lcs[wp]: 1210 "\<lbrace>valid_reply_masters and valid_objs\<rbrace>CSpace_A.lookup_cap_and_slot t ptr 1211 \<lbrace>\<lambda>rv s. \<not> is_master_reply_cap (fst rv)\<rbrace>,-" 1212 apply (simp add:lookup_cap_and_slot_def) 1213 apply wp 1214 apply (simp add:split_def) 1215 apply wp 1216 apply (rule_tac Q ="\<lambda>cap. cte_wp_at (\<lambda>x. x = cap) (fst x) and real_cte_at (fst x) 1217 and valid_reply_masters and valid_objs" in hoare_strengthen_post) 1218 apply (wp get_cap_cte_wp_at) 1219 apply clarify 1220 apply (drule real_cte_not_reply_masterD) 1221 apply clarsimp+ 1222 apply (simp add:cte_wp_at_def) 1223 apply wp 1224 apply simp 1225 done 1226 1227lemma not_master_reply_cap_lcs'[wp]: 1228 "\<lbrace>valid_reply_masters and valid_objs\<rbrace> CSpace_A.lookup_cap_and_slot t ptr 1229 \<lbrace>\<lambda>rv s. cte_wp_at (Not \<circ> is_master_reply_cap) (snd rv) s\<rbrace>,-" 1230 apply (rule_tac Q' = "\<lambda>rv s. \<not> is_master_reply_cap (fst rv) \<and> cte_wp_at (diminished (fst rv)) (snd rv) s" in hoare_post_imp_R) 1231 apply (rule hoare_pre,wp,simp) 1232 apply (clarsimp simp:cte_wp_at_def) 1233 apply (case_tac cap) 1234 apply (simp_all add:is_master_reply_cap_def) 1235 apply clarsimp 1236 apply (case_tac a) 1237 apply (simp_all add:diminished_def mask_cap_def cap_rights_update_def) 1238 done 1239 1240lemma set_thread_state_ct_active: 1241 "\<lbrace>\<lambda>s. cur_thread s = cur_thread s'\<rbrace> 1242 set_thread_state (cur_thread s') Structures_A.thread_state.Restart \<lbrace>\<lambda>rv. ct_active\<rbrace>" 1243 apply (simp add:set_thread_state_def) 1244 apply (wp dxo_wp_weak 1245 | clarsimp simp: set_object_def trans_state_def ct_in_state_def st_tcb_at_def obj_at_def)+ 1246 done 1247 1248lemma invoke_cnode_valid_etcbs[wp]: 1249 "\<lbrace>valid_etcbs\<rbrace> invoke_cnode ci \<lbrace>\<lambda>_. valid_etcbs\<rbrace>" 1250 apply (simp add: invoke_cnode_def) 1251 apply (rule hoare_pre) 1252 apply (wp crunch_wps hoare_vcg_all_lift | wpc | simp add: split del: if_split)+ 1253 done 1254 1255crunch valid_etcbs[wp]: perform_invocation valid_etcbs 1256 (wp: crunch_wps check_cap_inv simp: crunch_simps ignore: without_preemption) 1257 1258(* 1259 * Show that handle_invocation is equivalent. 1260 *) 1261lemma handle_invocation_corres: 1262 "dcorres (dc \<oplus> dc) \<top> 1263 (invs and ct_running and valid_pdpt_objs and valid_etcbs) 1264 (Syscall_D.handle_invocation call block) 1265 (Syscall_A.handle_invocation call block)" 1266 apply (simp add: Syscall_A.handle_invocation_def Syscall_D.handle_invocation_def liftE_bindE) 1267 apply (clarsimp simp:gets_the_def gets_def bind_assoc) 1268 apply (rule dcorres_absorb_get_l) 1269 apply (rule dcorres_absorb_get_r) 1270 apply (clarsimp, frule ct_running_not_idle_etc,simp+) 1271 apply (clarsimp simp: cdl_current_thread transform_current_thread_def not_idle_thread_def assert_opt_def) 1272 apply (simp add:get_message_info_def select_f_get_register bind_assoc liftM_def get_thread_def) 1273 apply (rule dcorres_gets_the) 1274 apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) 1275 prefer 2 1276 apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) 1277 apply (clarsimp simp:opt_object_tcb transform_tcb_def)+ 1278 apply (rule dcorres_absorb_gets_the) 1279 apply (clarsimp simp:Syscall_D.syscall_def Syscall_A.syscall_def liftE_bindE handle_elseE_def) 1280 apply (rule corres_guard_imp) 1281 apply (rule_tac P' = "(=) s'a" and P=\<top> and Q' = "(=) s'a" and Q=\<top> and 1282 rr = "\<lambda>(cap,slot,extra) (slot',cap',extra',buffer). 1283 cap = transform_cap cap' \<and> slot = transform_cslot_ptr slot' 1284 \<and> extra = transform_cap_list extra'" in corres_split_bind_case_sum) 1285 apply (rule_tac Q = "\<lambda>x. \<top>" and Q'="\<lambda>x. (=) s'a" in corres_initial_splitE) 1286 apply (clarsimp simp: transform_full_intent_def Let_def) 1287 apply (rule corres_guard_imp[OF dcorres_lookup_cap_and_slot[simplified]]) 1288 apply (clarsimp simp: word_bits_def not_idle_thread_def invs_def valid_state_def)+ 1289 apply (rule dcorres_symb_exec_r_evalMonad) 1290 apply wp 1291 apply (rule corres_guard_imp) 1292 apply (rule corres_splitEE[OF _ dcorres_lookup_extra_caps]) 1293 apply (rule dcorres_returnOk) 1294 apply simp 1295 apply (wp|clarsimp simp:not_idle_thread_def)+ 1296 apply (simp add:empty_when_fail_lookup_ipc_buffer weak_det_spec_lookup_ipc_buffer)+ 1297 apply (wp lookup_cap_and_slot_inv)+ 1298 apply (simp add:liftE_bindE) 1299 apply (rule corres_when,simp) 1300 apply (rule handle_fault_corres) 1301 apply (rule corres_split_bind_case_sum) 1302 apply (rule decode_invocation_corres') 1303 apply (simp add: split_def)+ 1304 apply (rule dcorres_when_r) 1305 apply (rule corres_dummy_return_r) 1306 apply (rule corres_guard_imp[OF corres_split[OF _ dcorres_reply_from_kernel]]) 1307 apply (simp add:when_def) 1308 apply (rule dcorres_set_intent_error) 1309 apply (wp rfk_invs reply_from_kernel_error | simp add:not_idle_thread_def)+ 1310 apply (rule dcorres_dummy_corrupt_ipc_buffer) 1311 apply (rule corres_split[OF _ dcorres_set_thread_state_Restart2]) 1312 apply (rule corres_splitEE[where r' = dc]) 1313 apply (simp add: whenE_def bind_assoc) 1314 apply (rule dcorres_reply_from_syscall) 1315 apply (rule perform_invocation_corres,simp) 1316 apply wp+ 1317 apply (simp add: not_idle_thread_def) 1318 apply (strengthen invs_valid_idle) 1319 apply wp+ 1320 apply (simp add:conj_comms not_idle_thread_def split_def) 1321 apply (wp sts_Restart_invs set_thread_state_ct_active)+ 1322 apply (simp add:conj_comms split_def msg_from_syscall_error_simp) 1323 apply (wp | simp add:split_def)+ 1324 apply (rule_tac Q'="\<lambda>r s. s = s'a \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_invocation r s \<and> 1325 invocation_duplicates_valid r s" 1326 in hoare_post_imp_R) 1327 apply (simp add:split_def liftE_bindE[symmetric]) 1328 apply (wp decode_inv_wf) 1329 apply (clarsimp simp:ct_in_state_def st_tcb_at_def obj_at_def not_idle_thread_def)+ 1330 apply (rule wp_post_tautE) 1331 apply clarsimp 1332 apply wp 1333 apply (simp add:split_def liftE_bindE[symmetric]) 1334 apply (wp | simp add: split_def liftE_bindE[symmetric])+ 1335 apply (rule_tac Q="\<lambda>r s. s = s'a \<and> 1336 evalMonad (lookup_ipc_buffer False (cur_thread s'a)) s'a = Some r \<and> 1337 cte_wp_at (Not \<circ> is_master_reply_cap) (snd x) s \<and> 1338 cte_wp_at (diminished (fst x)) (snd x) s \<and> s \<turnstile> fst x \<and> 1339 ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> 1340 (\<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> 1341 (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to \<top> r s)" 1342 in hoare_strengthen_post) 1343 apply (wp evalMonad_wp) 1344 apply (simp add: empty_when_fail_lookup_ipc_buffer weak_det_spec_lookup_ipc_buffer)+ 1345 apply wp 1346 apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_idle_def st_tcb_ex_cap 1347 ct_in_state_def pred_tcb_at_def not_idle_thread_def obj_at_def 1348 dest!: get_tcb_SomeD) 1349 apply (wp)+ 1350 apply (clarsimp simp:invs_def valid_state_def not_idle_thread_def pred_tcb_at_def obj_at_def) 1351 apply simp_all 1352 done 1353 1354crunch cur_thread[wp]: complete_signal "\<lambda>s. P (cur_thread s)" 1355 1356lemma receive_ipc_cur_thread: 1357 notes do_nbrecv_failed_transfer_def[simp] 1358 shows 1359 " \<lbrace>\<lambda>s. valid_objs s \<and> P (cur_thread (s :: det_ext state))\<rbrace> receive_ipc a b c \<lbrace>\<lambda>xg s. P (cur_thread s)\<rbrace>" 1360 apply (simp add:receive_ipc_def bind_assoc) 1361 apply (wp|wpc|clarsimp)+ 1362 apply (simp add:setup_caller_cap_def) 1363 apply (wp dxo_wp_weak | simp)+ 1364 apply (rule_tac Q="\<lambda>r s. P (cur_thread s)" in hoare_strengthen_post) 1365 apply wp 1366 apply clarsimp 1367 apply (wp|wpc)+ 1368 apply (rule_tac Q="\<lambda>r s. P (cur_thread s)" in hoare_strengthen_post) 1369 apply wp 1370 apply clarsimp 1371 apply (clarsimp simp:neq_Nil_conv) 1372 apply (rename_tac list queue sender) 1373 apply (rule_tac Q="\<lambda>r s. P (cur_thread s) \<and> tcb_at (hd list) s" in hoare_strengthen_post) 1374 apply wp 1375 apply (clarsimp simp:st_tcb_at_def tcb_at_def) 1376 apply (wp get_simple_ko_wp[where f=Notification] gbn_wp | wpc | simp add: Ipc_A.isActive_def)+ 1377 apply (rule_tac Q="\<lambda>r s. valid_ep r s \<and> P (cur_thread s)" in hoare_strengthen_post) 1378 apply (wp get_simple_ko_valid[where f=Endpoint, simplified valid_ep_def2[symmetric]]) 1379 apply (clarsimp simp:valid_ep_def) 1380 apply auto[1] 1381 apply (rule hoare_pre) 1382 apply (wp | wpc | simp)+ 1383 done 1384 1385lemma cap_delete_one_st_tcb_at_and_valid_etcbs: 1386 "\<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st) and valid_etcbs\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv s. st_tcb_at P t s \<and> valid_etcbs s\<rbrace>" 1387 by (wp cap_delete_one_st_tcb_at cap_delete_one_valid_etcbs | simp)+ 1388 1389crunch ct_it[wp]: deleted_irq_handler, cap_delete_one "\<lambda>s::'z::state_ext state. P (cur_thread s) (idle_thread s)" 1390 (wp: crunch_wps set_thread_state_ext_extended.all_but_exst dxo_wp_weak 1391 simp: crunch_simps unless_def) 1392 1393lemma handle_recv_corres: 1394 "dcorres dc \<top> (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> st_tcb_at active (cur_thread s) s) and valid_etcbs) 1395 Syscall_D.handle_recv (Syscall_A.handle_recv is_blocking)" 1396 apply (simp add: Syscall_D.handle_recv_def Syscall_A.handle_recv_def delete_caller_cap_def) 1397 apply (rule corres_guard_imp) 1398 apply (rule corres_split[OF _ get_cur_thread_corres]) 1399 apply (simp add:liftM_def select_f_get_register get_thread_def bind_assoc) 1400 apply (rule_tac P=\<top> and P'="invs and valid_etcbs and (\<lambda>s. thread = cur_thread s 1401 \<and> not_idle_thread thread s \<and> st_tcb_at active thread s)" 1402 in dcorres_gets_the) 1403 apply (clarsimp simp: not_idle_thread_def, frule(1) valid_etcbs_get_tcb_get_etcb) 1404 apply (clarsimp simp:opt_object_tcb gets_def transform_tcb_def) 1405 apply (simp add:transform_full_intent_def Let_def cap_fault_injection) 1406 apply (rule corres_guard_imp) 1407 apply (rule corres_split_catch[where f= dc,OF handle_fault_corres]) 1408 apply (rule dcorres_injection_handler_rhs) 1409 apply (rule_tac R' ="\<lambda>rv s. (\<forall>ref badge rights. rv = cap.EndpointCap ref badge rights \<longrightarrow> 1410 (ep_at ref s)) \<and> not_idle_thread (cur_thread s') s 1411 \<and> not_idle_thread (cur_thread s) s 1412 \<and> (st_tcb_at active (cur_thread s') s \<and> invs s \<and> valid_etcbs s) \<and> ko_at (TCB obj') (cur_thread s') s " and R= "\<lambda>r. \<top>" 1413 in corres_splitEE[where r'="\<lambda>x y. x = transform_cap y"]) 1414 apply (rule dcorres_expand_pfx) 1415 apply (clarsimp split:cap.splits arch_cap.splits split del: if_split simp:transform_cap_def) 1416 apply (rename_tac word1 word2 set) 1417 apply (rule corres_guard_imp) 1418 apply (case_tac "AllowRead \<in> set"; simp split del: if_split) 1419 apply (rule corres_alternate1) 1420 apply clarsimp 1421 apply (rule corres_split[where r'=dc]) 1422 apply (rule_tac epptr=word1 in recv_sync_ipc_corres) 1423 apply (simp add: cap_ep_ptr_def delete_caller_cap_def)+ 1424 apply (simp add: transform_tcb_slot_simp[symmetric]) 1425 apply (rule delete_cap_simple_corres) 1426 apply (wp | clarsimp simp: delete_caller_cap_def not_idle_thread_def)+ 1427 apply (rule hoare_vcg_conj_lift) 1428 apply (rule_tac t1="cur_thread s'" in hoare_post_imp[OF _ cap_delete_one_st_tcb_at_and_valid_etcbs]) 1429 apply (fastforce simp: obj_at_def generates_pending_def st_tcb_at_def) 1430 apply (rule_tac Q="\<lambda>rv. invs and valid_etcbs" in hoare_strengthen_post) 1431 apply wp 1432 apply (clarsimp simp: invs_def) 1433 apply clarsimp 1434 apply (clarsimp simp: emptyable_def not_idle_thread_def) 1435 defer(* NEED RECEIVE ASYNC IPC *) 1436 apply clarsimp 1437 apply (rule lookup_cap_corres, simp) 1438 apply (simp add: word_bits_def) 1439 apply wp+ 1440 apply (rule hoare_vcg_conj_liftE_R) 1441 apply (rule hoare_post_imp_R, rule lookup_cap_valid) 1442 apply (clarsimp simp: valid_cap_def) 1443 apply wp+ 1444 apply (simp add:injection_handler_def) 1445 apply (wp get_simple_ko_wp |wpc)+ 1446 apply (simp only: conj_ac) 1447 apply wp 1448 apply (rule hoare_vcg_E_elim) 1449 apply (simp add: lookup_cap_def lookup_slot_for_thread_def split_def) 1450 apply wp 1451 apply (rule hoare_post_impErr[OF resolve_address_bits_valid_fault]) 1452 apply simp 1453 apply simp 1454 apply wp 1455 apply (rule validE_validE_R) 1456 apply (clarsimp simp:validE_def) 1457 apply (rule_tac Q = "\<lambda>r s. cur_thread s = cur_thread s' \<and> 1458 not_idle_thread (cur_thread s) s \<and> 1459 st_tcb_at active (cur_thread s) s \<and> 1460 invs s \<and> valid_etcbs s \<and> 1461 valid_irq_node s" in hoare_strengthen_post) 1462 apply wp 1463 apply (clarsimp simp add: valid_fault_def) 1464 apply clarsimp+ 1465 apply (clarsimp dest!: get_tcb_SomeD 1466 simp: invs_valid_tcb_ctable valid_state_def invs_def 1467 obj_at_def valid_pspace_def not_idle_thread_def) 1468 apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) 1469 apply (clarsimp simp:opt_object_tcb not_idle_thread_def) 1470 apply wp+ 1471 apply simp 1472 apply (clarsimp simp:emptyable_def not_idle_thread_def) 1473 apply (clarsimp simp: liftE_bindE get_simple_ko_def get_object_def gets_def bind_assoc) 1474 apply (rule dcorres_absorb_get_r) 1475 apply (clarsimp simp: assert_def corres_free_fail partial_inv_def a_type_def 1476 split: Structures_A.kernel_object.splits) 1477 apply safe[1] 1478 apply (rule corres_alternate1, clarsimp, rule corres_guard_imp[OF recv_signal_corres], (clarsimp simp: transform_cap_def)+)+ 1479 apply (rule corres_alternate2) 1480 apply clarsimp 1481 done 1482 1483(* Show that handle_reply is equivalent. *) 1484lemma handle_reply_corres: 1485 "dcorres dc \<top> (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) 1486 Syscall_D.handle_reply Syscall_A.handle_reply" 1487 apply (simp add: Syscall_D.handle_reply_def Syscall_A.handle_reply_def) 1488 apply (rule corres_guard_imp) 1489 apply (rule corres_split [OF _ get_cur_thread_corres]) 1490 apply simp 1491 apply (rule_tac R="\<lambda>_. \<top>" and 1492 R'="\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread 1493 and not_idle_thread thread 1494 and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)" 1495 in corres_split [OF _ get_cap_corres]) 1496 apply (simp add: transform_cap_def corres_fail split: cap.split) 1497 apply (clarsimp simp: corres_fail dc_def[symmetric] split: bool.split) 1498 apply (rename_tac word) 1499 apply (rule corres_guard_imp) 1500 apply (rule do_reply_transfer_corres) 1501 apply (simp add: transform_tcb_slot_simp) 1502 apply simp 1503 apply (clarsimp simp:ct_running_not_idle_etc) 1504 apply (frule caps_of_state_valid(1)) 1505 apply (clarsimp simp:cte_wp_at_caps_of_state) 1506 apply (simp add:valid_cap_def)+ 1507 apply (clarsimp simp:valid_state_def invs_def valid_reply_caps_def dest!:has_reply_cap_cte_wpD) 1508 apply (drule_tac x = word in spec,simp) 1509 apply (clarsimp simp:not_idle_thread_def pred_tcb_at_def obj_at_def valid_idle_def) 1510 apply (clarsimp simp: transform_tcb_slot_simp|(wp get_cap_wp)+)+ 1511 apply (clarsimp simp:ct_in_state_def invs_def valid_state_def pred_tcb_at_def tcb_at_def obj_at_def) 1512 done 1513 1514lemma handle_vm_fault_wp: 1515 "\<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>\<lambda>rv. P\<rbrace>" 1516 apply (case_tac vmfault_type) 1517 apply (simp) 1518 apply wp 1519 apply (clarsimp simp:do_machine_op_def getDFSR_def) 1520 apply wp 1521 apply (case_tac x) 1522 apply clarsimp 1523 apply (rule_tac P="P and (\<lambda>x. snd (aa,ba) = machine_state x)" in hoare_post_imp) 1524 apply (assumption) 1525 apply (clarsimp simp:valid_def simpler_modify_def return_def bind_def) 1526 apply wp+ 1527 apply (clarsimp simp:gets_def alternative_def get_def bind_def select_def return_def) 1528 apply (clarsimp simp:do_machine_op_def getFAR_def) 1529 apply wp 1530 apply (case_tac x) 1531 apply clarsimp 1532 apply (rule_tac P="P and (\<lambda>x. snd (aa,ba) = machine_state x)" in hoare_post_imp) 1533 apply (assumption) 1534 apply (clarsimp simp:valid_def simpler_modify_def return_def bind_def) 1535 apply wp+ 1536 apply (clarsimp simp:gets_def alternative_def select_def bind_def get_def return_def) 1537 apply simp 1538 apply wp 1539 apply (clarsimp simp:do_machine_op_def getIFSR_def) 1540 apply wp 1541 apply (case_tac x) 1542 apply clarsimp 1543 apply (rule_tac P="P and (\<lambda>x. snd (aa,ba) = machine_state x)" in hoare_post_imp) 1544 apply (assumption) 1545 apply (clarsimp simp:valid_def simpler_modify_def return_def bind_def) 1546 apply wp+ 1547 apply (clarsimp simp:gets_def alternative_def select_def bind_def get_def return_def) 1548 done 1549 1550lemma get_active_irq_corres: 1551 "dcorres (\<lambda>r r'. r' = r) \<top> \<top> get_active_irq (do_machine_op (getActiveIRQ in_kernel))" 1552 apply (clarsimp simp: corres_underlying_def do_machine_op_def 1553 select_f_def bind_def in_monad getActiveIRQ_def 1554 return_def get_active_irq_def select_def 1555 split: if_splits) 1556 apply (rule_tac x="(None, transform b)" in bexI 1557 , (simp add: in_alternative)+) 1558 apply (rule_tac x="(Some (irq_oracle (Suc (irq_state (machine_state b)))), 1559 transform b)" in bexI 1560 , (simp add: in_alternative)+) 1561 done 1562 1563 1564crunch valid_etcbs[wp]: "handle_reply" "valid_etcbs" 1565 (wp: crunch_wps simp: crunch_simps) 1566 1567lemma hr_ct_active_and_valid_etcbs: 1568 "\<lbrace>invs and ct_active and valid_etcbs\<rbrace> Syscall_A.handle_reply \<lbrace>\<lambda>rv. ct_active and valid_etcbs\<rbrace>" 1569 by (wp, simp+) 1570 1571declare tcb_sched_action_transform[wp] 1572 1573crunch transform_inv[wp]: reschedule_required "\<lambda>s. transform s = cs" 1574 1575lemma handle_hypervisor_fault_corres: 1576 "dcorres dc (\<lambda>_. True) 1577 (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_running and valid_etcbs) 1578 Syscall_D.handle_hypervisor_fault (do y \<leftarrow> local.handle_hypervisor_fault thread w; return () od)" 1579 by (cases w; simp add: Syscall_D.handle_hypervisor_fault_def returnOk_def2) 1580 1581lemma handle_event_corres: 1582 "dcorres (dc \<oplus> dc) \<top> 1583 (invs and valid_pdpt_objs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_running s) and valid_etcbs) 1584 (Syscall_D.handle_event ev) (Syscall_A.handle_event ev)" 1585 apply (cases ev, simp_all add: Syscall_D.handle_event_def) 1586 apply (rename_tac syscall) 1587 apply (case_tac syscall) 1588 apply (simp_all add:handle_syscall_def handle_send_def handle_call_def) 1589 apply (rule handle_invocation_corres[THEN corres_guard_imp] | simp)+ 1590 apply (rule corres_guard_imp) 1591 apply (rule corres_split[OF handle_recv_corres handle_reply_corres]) 1592 apply (wp handle_reply_cur_thread_idle_thread) 1593 apply (simp add:not_idle_thread_def) 1594 apply (wp handle_reply_cur_thread_idle_thread handle_reply_valid_etcbs) 1595 apply (rule hoare_post_imp[OF _ hr_ct_active_and_valid_etcbs]) 1596 apply (clarsimp simp:ct_in_state_def) 1597 apply clarsimp+ 1598 apply (frule (1) ct_running_not_idle_etc) 1599 apply ((clarsimp simp: handle_yield_def returnOk_def liftE_def not_idle_thread_def 1600 ct_in_state_def st_tcb_at_def obj_at_def)+)[1] 1601 apply (rule handle_invocation_corres[THEN corres_guard_imp] | simp)+ 1602 apply (rule corres_guard_imp[OF handle_recv_corres]) 1603 apply simp+ 1604 apply (simp add: ct_running_not_idle_etc) 1605 apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def generates_pending_def) 1606 apply (rule corres_guard_imp[OF handle_reply_corres]) 1607 apply simp 1608 apply (simp add: ct_running_not_idle_etc) 1609 apply (clarsimp simp:not_idle_thread_def ct_in_state_def st_tcb_at_def) 1610 apply ((clarsimp simp: handle_yield_def returnOk_def liftE_def not_idle_thread_def 1611 ct_in_state_def st_tcb_at_def obj_at_def)+) 1612 apply (rule dcorres_symb_exec_r) 1613 apply (rule dcorres_return, simp) 1614 apply (wp hoare_TrueI)+ 1615 apply (rule corres_guard_imp) 1616 apply (rule handle_recv_corres, simp) 1617 apply clarsimp 1618 apply (frule (1) ct_running_not_idle_etc) 1619 apply (clarsimp simp: not_idle_thread_def ct_in_state_def st_tcb_at_def obj_at_def) 1620 apply (rule corres_symb_exec_r[OF handle_fault_corres]) 1621 apply wp[1] 1622 apply clarsimp 1623 apply (frule (1) ct_running_not_idle_etc) 1624 apply (fastforce simp: st_tcb_at_def obj_at_def generates_pending_def gets_def get_def 1625 valid_fault_def 1626 split: Structures_A.thread_state.splits)+ 1627 apply (rule corres_symb_exec_r[OF handle_fault_corres]) 1628 apply wp[1] 1629 apply clarsimp 1630 apply (frule (1) ct_running_not_idle_etc) 1631 apply (fastforce simp: st_tcb_at_def obj_at_def generates_pending_def valid_fault_def 1632 split: thread_state.splits)+ 1633 apply (simp add:handle_pending_interrupts_def) 1634 apply (rule corres_guard_imp) 1635 apply (rule corres_split [OF _ get_active_irq_corres]) 1636 apply (clarsimp simp:option.splits) 1637 apply (rule handle_interrupt_corres) 1638 apply (wp | simp)+ 1639 apply (rule corres_symb_exec_r) 1640 apply (rule corres_symb_exec_catch_r) 1641 apply (rule handle_fault_corres) 1642 apply (simp only: conj_comms) 1643 apply (rule hoare_vcg_E_conj) 1644 apply (wp handle_vm_fault_wp | rule hoare_vcg_E_conj)+ 1645 apply (simp add:no_fail_def) 1646 apply wp 1647 apply clarsimp 1648 apply (frule (1) ct_running_not_idle_etc) 1649 apply (clarsimp simp:invs_def valid_state_def st_tcb_at_def generates_pending_def obj_at_def) 1650 apply wpsimp+ 1651 apply (rule corres_symb_exec_r[OF handle_hypervisor_fault_corres[simplified]]; wpsimp) 1652 done 1653 1654end 1655 1656end 1657