theory Finalise_R

lemma deletingIRQHandler_removeable':
  "\<lbrace>invs' and (\<lambda>s. isFinal (IRQHandlerCap irq) slot (cteCaps_of s))
          and K (cap = IRQHandlerCap irq)\<rbrace>
     deletingIRQHandler irq
   \<lbrace>\<lambda>rv s. removeable' slot s cap\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: deletingIRQHandler_def getIRQSlot_def locateSlot_conv
                   getInterruptState_def getSlotCap_def) apply (simp add: removeable'_def tree_cte_cteCap_eq[unfolded o_def]) apply (subst tree_cte_cteCap_eq[unfolded o_def])+ apply (wp hoare_use_eq_irq_node' [OF cteDeleteOne_irq_node' cteDeleteOne_cteCaps_of]
            getCTE_wp') apply (clarsimp simp: cte_level_bits_def ucast_nat_def split: option.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. isFinal (capability.IRQHandlerCap irq) slot (cteCaps_of s)) and K (cap = capability.IRQHandlerCap irq)\<rbrace> deletingIRQHandler irq \<lbrace>\<lambda>rv s. removeable' slot s cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. cap = capability.IRQHandlerCap irq \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. isFinal (capability.IRQHandlerCap irq) slot (cteCaps_of s))\<rbrace> deletingIRQHandler irq \<lbrace>\<lambda>rv s. removeable' slot s cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. cap = capability.IRQHandlerCap irq \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. isFinal (capability.IRQHandlerCap irq) slot (cteCaps_of s))\<rbrace> do node <- liftM intStateIRQNode (gets ksInterruptState);
cte <- getCTE (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq);
y <- assert (isNotificationCap (cteCap cte) \<or> cteCap cte = capability.NullCap);
cteDeleteOne (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od \<lbrace>\<lambda>rv s. removeable' slot s (capability.IRQHandlerCap irq)\<rbrace> proof (prove)
goal (1 subgoal):
 1. cap = capability.IRQHandlerCap irq \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. isFinal (capability.IRQHandlerCap irq) slot (cteCaps_of s))\<rbrace> do node <- liftM intStateIRQNode (gets ksInterruptState);
cte <- getCTE (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq);
y <- assert (isNotificationCap (cteCap cte) \<or> cteCap cte = capability.NullCap);
cteDeleteOne (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od \<lbrace>\<lambda>rv s. irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10 \<noteq> slot \<longrightarrow> (\<exists>p. p \<noteq> slot \<and> cte_wp_at' (\<lambda>cte. capMasterCap (cteCap cte) = capability.IRQHandlerCap irq) p s) \<or> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. cap = capability.IRQHandlerCap irq \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. isFinal (capability.IRQHandlerCap irq) slot (cteCaps_of s))\<rbrace> do node <- liftM intStateIRQNode (gets ksInterruptState);
cte <- getCTE (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq);
y <- assert (isNotificationCap (cteCap cte) \<or> cteCap cte = capability.NullCap);
cteDeleteOne (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od \<lbrace>\<lambda>rv s. irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10 \<noteq> slot \<longrightarrow> (\<exists>p. p \<noteq> slot \<and> (case cteCaps_of s p of None \<Rightarrow> False | Some a \<Rightarrow> capMasterCap a = capability.IRQHandlerCap irq)) \<or> (case cteCaps_of s (irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10) of None \<Rightarrow> False | Some a \<Rightarrow> a = capability.NullCap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap = capability.IRQHandlerCap irq; (invs' and (\<lambda>s. isFinal (capability.IRQHandlerCap irq) slot (cteCaps_of s))) s\<rbrakk> \<Longrightarrow> ((\<lambda>node s. \<forall>cte. cte_wp_at' ((=) cte) (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) s \<longrightarrow> isNotificationCap (cteCap cte) \<or> cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail) (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) s \<longrightarrow> irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10 \<noteq> slot \<longrightarrow> (\<exists>p. p \<noteq> slot \<and> (case ((cteCaps_of s)(node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq \<mapsto> capability.NullCap)) p of None \<Rightarrow> False | Some a \<Rightarrow> capMasterCap a = capability.IRQHandlerCap irq)) \<or> (case ((cteCaps_of s)(node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq \<mapsto> capability.NullCap)) (irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10) of None \<Rightarrow> False | Some a \<Rightarrow> a = capability.NullCap)) \<circ> intStateIRQNode) (ksInterruptState s) s proof (prove)
goal:
No subgoals!