theory Interrupt_R

lemma invoke_irq_handler_invs'[wp]:
  "\<lbrace>invs' and irq_handler_inv_valid' i\<rbrace>
    InterruptDecls_H.invokeIRQHandler i \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (cases i; simp add: Interrupt_H.invokeIRQHandler_def) apply wpsimp apply (wp cteInsert_invs)+ apply (strengthen ntfn_badge_derived_enough_strg isnt_irq_handler_strg) apply (wp cteDeleteOne_other_cap cteDeleteOne_other_cap[unfolded o_def]) apply (rename_tac word1 cap word2) apply (simp add: getInterruptState_def getIRQSlot_def locateSlot_conv) apply wp apply (rename_tac word1 cap word2 s) apply (clarsimp simp: ucast_nat_def) apply (drule_tac irq=word1 in valid_globals_ex_cte_cap_irq) apply clarsimp+ apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_to'_def
                        isCap_simps untyped_derived_eq_def) apply (fastforce simp: cte_level_bits_def badge_derived'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and irq_handler_inv_valid' i\<rbrace> InterruptDecls_H.invokeIRQHandler i \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1. i = AckIRQ x1 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) x1 \<noteq> irqstate.IRQInactive)\<rbrace> local.invokeIRQHandler (AckIRQ x1) \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x2. i = irqhandler_invocation.ClearIRQHandler x2 \<Longrightarrow> \<lbrace>invs'\<rbrace> getIRQSlot x2 >>= cteDeleteOne \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x31 x32 x33. i = irqhandler_invocation.SetIRQHandler x31 x32 x33 \<Longrightarrow> \<lbrace>invs' and (valid_cap' x32 and valid_cap' (capability.IRQHandlerCap x31) and (\<lambda>y. isNotificationCap x32) and cte_wp_at' (badge_derived' x32 \<circ> cteCap) x33 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap x31) ptr' s) and ex_cte_cap_wp_to' isCNodeCap x33)\<rbrace> do irqSlot <- getIRQSlot x31;
y <- cteDeleteOne irqSlot;
cteInsert x32 x33 irqSlot
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2. i = irqhandler_invocation.ClearIRQHandler x2 \<Longrightarrow> \<lbrace>invs'\<rbrace> getIRQSlot x2 >>= cteDeleteOne \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>x31 x32 x33. i = irqhandler_invocation.SetIRQHandler x31 x32 x33 \<Longrightarrow> \<lbrace>invs' and (valid_cap' x32 and valid_cap' (capability.IRQHandlerCap x31) and (\<lambda>y. isNotificationCap x32) and cte_wp_at' (badge_derived' x32 \<circ> cteCap) x33 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap x31) ptr' s) and ex_cte_cap_wp_to' isCNodeCap x33)\<rbrace> do irqSlot <- getIRQSlot x31;
y <- cteDeleteOne irqSlot;
cteInsert x32 x33 irqSlot
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 irqSlot. i = irqhandler_invocation.SetIRQHandler x31 x32 x33 \<Longrightarrow> \<lbrace>?P'36 x31 x32 x33 irqSlot\<rbrace> cteDeleteOne irqSlot \<lbrace>\<lambda>rv s. cte_wp_at' (is_derived' (ctes_of s) x33 x32 \<circ> cteCap) x33 s \<and> cte_wp_at' (untyped_derived_eq x32 \<circ> cteCap) x33 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) irqSlot s \<and> (\<forall>irq. x32 = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace>
 2. \<And>x31 x32 x33. i = irqhandler_invocation.SetIRQHandler x31 x32 x33 \<Longrightarrow> \<lbrace>?Q19 x31 x32 x33\<rbrace> getIRQSlot x31 \<lbrace>\<lambda>irqSlot s. invs' s \<and> True \<and> valid_cap' x32 s \<and> x33 \<noteq> irqSlot \<and> ?P'36 x31 x32 x33 irqSlot s\<rbrace>
 3. \<And>x31 x32 x33 s. \<lbrakk>i = irqhandler_invocation.SetIRQHandler x31 x32 x33; (invs' and (valid_cap' x32 and valid_cap' (capability.IRQHandlerCap x31) and (\<lambda>y. isNotificationCap x32) and cte_wp_at' (badge_derived' x32 \<circ> cteCap) x33 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap x31) ptr' s) and ex_cte_cap_wp_to' isCNodeCap x33)) s\<rbrakk> \<Longrightarrow> ?Q19 x31 x32 x33 s proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 irqSlot. i = irqhandler_invocation.SetIRQHandler x31 x32 x33 \<Longrightarrow> \<lbrace>?P'36 x31 x32 x33 irqSlot\<rbrace> cteDeleteOne irqSlot \<lbrace>\<lambda>r s. cte_wp_at' (\<lambda>cte. isNotificationCap x32 \<and> badge_derived' x32 (cteCap cte)) x33 s \<and> cte_wp_at' (untyped_derived_eq x32 \<circ> cteCap) x33 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) irqSlot s \<and> \<not> isIRQHandlerCap x32\<rbrace>
 2. \<And>x31 x32 x33. i = irqhandler_invocation.SetIRQHandler x31 x32 x33 \<Longrightarrow> \<lbrace>?Q19 x31 x32 x33\<rbrace> getIRQSlot x31 \<lbrace>\<lambda>irqSlot s. invs' s \<and> True \<and> valid_cap' x32 s \<and> x33 \<noteq> irqSlot \<and> ?P'36 x31 x32 x33 irqSlot s\<rbrace>
 3. \<And>x31 x32 x33 s. \<lbrakk>i = irqhandler_invocation.SetIRQHandler x31 x32 x33; (invs' and (valid_cap' x32 and valid_cap' (capability.IRQHandlerCap x31) and (\<lambda>y. isNotificationCap x32) and cte_wp_at' (badge_derived' x32 \<circ> cteCap) x33 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap x31) ptr' s) and ex_cte_cap_wp_to' isCNodeCap x33)) s\<rbrakk> \<Longrightarrow> ?Q19 x31 x32 x33 s proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33. i = irqhandler_invocation.SetIRQHandler x31 x32 x33 \<Longrightarrow> \<lbrace>?Q19 x31 x32 x33\<rbrace> getIRQSlot x31 \<lbrace>\<lambda>irqSlot s. invs' s \<and> True \<and> valid_cap' x32 s \<and> x33 \<noteq> irqSlot \<and> (cte_wp_at' (\<lambda>x. isNotificationCap x32 \<and> badge_derived' x32 (cteCap x)) x33 and K (x33 \<noteq> irqSlot)) s \<and> (cte_wp_at' (untyped_derived_eq x32 \<circ> cteCap) x33 and K (x33 \<noteq> irqSlot)) s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) irqSlot s \<and> \<not> isIRQHandlerCap x32\<rbrace>
 2. \<And>x31 x32 x33 s. \<lbrakk>i = irqhandler_invocation.SetIRQHandler x31 x32 x33; (invs' and (valid_cap' x32 and valid_cap' (capability.IRQHandlerCap x31) and (\<lambda>y. isNotificationCap x32) and cte_wp_at' (badge_derived' x32 \<circ> cteCap) x33 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap x31) ptr' s) and ex_cte_cap_wp_to' isCNodeCap x33)) s\<rbrakk> \<Longrightarrow> ?Q19 x31 x32 x33 s proof (prove)
goal (2 subgoals):
 1. \<And>word1 cap word2. i = irqhandler_invocation.SetIRQHandler word1 cap word2 \<Longrightarrow> \<lbrace>?Q19 word1 cap word2\<rbrace> getIRQSlot word1 \<lbrace>\<lambda>irqSlot s. invs' s \<and> True \<and> valid_cap' cap s \<and> word2 \<noteq> irqSlot \<and> (cte_wp_at' (\<lambda>x. isNotificationCap cap \<and> badge_derived' cap (cteCap x)) word2 and K (word2 \<noteq> irqSlot)) s \<and> (cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) word2 and K (word2 \<noteq> irqSlot)) s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) irqSlot s \<and> \<not> isIRQHandlerCap cap\<rbrace>
 2. \<And>x31 x32 x33 s. \<lbrakk>i = irqhandler_invocation.SetIRQHandler x31 x32 x33; (invs' and (valid_cap' x32 and valid_cap' (capability.IRQHandlerCap x31) and (\<lambda>y. isNotificationCap x32) and cte_wp_at' (badge_derived' x32 \<circ> cteCap) x33 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap x31) ptr' s) and ex_cte_cap_wp_to' isCNodeCap x33)) s\<rbrakk> \<Longrightarrow> ?Q19 x31 x32 x33 s proof (prove)
goal (2 subgoals):
 1. \<And>word1 cap word2. i = irqhandler_invocation.SetIRQHandler word1 cap word2 \<Longrightarrow> \<lbrace>?Q19 word1 cap word2\<rbrace> do node <- liftM intStateIRQNode (gets ksInterruptState);
return (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1)
od \<lbrace>\<lambda>irqSlot s. invs' s \<and> valid_cap' cap s \<and> word2 \<noteq> irqSlot \<and> cte_wp_at' (\<lambda>x. isNotificationCap cap \<and> badge_derived' cap (cteCap x)) word2 s \<and> word2 \<noteq> irqSlot \<and> cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) word2 s \<and> word2 \<noteq> irqSlot \<and> ex_cte_cap_wp_to' (\<lambda>_. True) irqSlot s \<and> \<not> isIRQHandlerCap cap\<rbrace>
 2. \<And>x31 x32 x33 s. \<lbrakk>i = irqhandler_invocation.SetIRQHandler x31 x32 x33; (invs' and (valid_cap' x32 and valid_cap' (capability.IRQHandlerCap x31) and (\<lambda>y. isNotificationCap x32) and cte_wp_at' (badge_derived' x32 \<circ> cteCap) x33 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap x31) ptr' s) and ex_cte_cap_wp_to' isCNodeCap x33)) s\<rbrakk> \<Longrightarrow> ?Q19 x31 x32 x33 s proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 s. \<lbrakk>i = irqhandler_invocation.SetIRQHandler x31 x32 x33; (invs' and (valid_cap' x32 and valid_cap' (capability.IRQHandlerCap x31) and (\<lambda>y. isNotificationCap x32) and cte_wp_at' (badge_derived' x32 \<circ> cteCap) x33 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap x31) ptr' s) and ex_cte_cap_wp_to' isCNodeCap x33)) s\<rbrakk> \<Longrightarrow> ((\<lambda>node a. invs' a \<and> valid_cap' x32 a \<and> x33 \<noteq> node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) x31 \<and> cte_wp_at' (\<lambda>x. isNotificationCap x32 \<and> badge_derived' x32 (cteCap x)) x33 a \<and> x33 \<noteq> node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) x31 \<and> cte_wp_at' (untyped_derived_eq x32 \<circ> cteCap) x33 a \<and> x33 \<noteq> node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) x31 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) x31) a \<and> \<not> isIRQHandlerCap x32) \<circ> intStateIRQNode) (ksInterruptState s) s proof (prove)
goal (1 subgoal):
 1. \<And>word1 cap word2 s. \<lbrakk>i = irqhandler_invocation.SetIRQHandler word1 cap word2; (invs' and (valid_cap' cap and valid_cap' (capability.IRQHandlerCap word1) and (\<lambda>y. isNotificationCap cap) and cte_wp_at' (badge_derived' cap \<circ> cteCap) word2 and (\<lambda>s. \<exists>ptr'. cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word1) ptr' s) and ex_cte_cap_wp_to' isCNodeCap word2)) s\<rbrakk> \<Longrightarrow> ((\<lambda>node a. invs' a \<and> valid_cap' cap a \<and> word2 \<noteq> node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1 \<and> cte_wp_at' (\<lambda>x. isNotificationCap cap \<and> badge_derived' cap (cteCap x)) word2 a \<and> word2 \<noteq> node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1 \<and> cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) word2 a \<and> word2 \<noteq> node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1) a \<and> \<not> isIRQHandlerCap cap) \<circ> intStateIRQNode) (ksInterruptState s) s proof (prove)
goal (1 subgoal):
 1. \<And>word1 cap word2 s ptr'. \<lbrakk>i = irqhandler_invocation.SetIRQHandler word1 cap word2; invs' s; valid_cap' cap s; valid_cap' (capability.IRQHandlerCap word1) s; isNotificationCap cap; cte_wp_at' (badge_derived' cap \<circ> cteCap) word2 s; ex_cte_cap_wp_to' isCNodeCap word2 s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word1) ptr' s\<rbrakk> \<Longrightarrow> word2 \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1 \<and> cte_wp_at' (\<lambda>x. badge_derived' cap (cteCap x)) word2 s \<and> word2 \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1 \<and> cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) word2 s \<and> word2 \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1) s \<and> \<not> isIRQHandlerCap cap proof (prove)
goal (3 subgoals):
 1. \<And>word1 cap word2 s ptr'. \<lbrakk>i = irqhandler_invocation.SetIRQHandler word1 cap word2; invs' s; valid_cap' cap s; valid_cap' (capability.IRQHandlerCap word1) s; isNotificationCap cap; cte_wp_at' (badge_derived' cap \<circ> cteCap) word2 s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word1) ptr' s\<rbrakk> \<Longrightarrow> valid_global_refs' s
 2. \<And>word1 cap word2 s ptr'. \<lbrakk>i = irqhandler_invocation.SetIRQHandler word1 cap word2; invs' s; valid_cap' cap s; valid_cap' (capability.IRQHandlerCap word1) s; isNotificationCap cap; cte_wp_at' (badge_derived' cap \<circ> cteCap) word2 s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word1) ptr' s\<rbrakk> \<Longrightarrow> valid_objs' s
 3. \<And>word1 cap word2 s ptr'. \<lbrakk>i = irqhandler_invocation.SetIRQHandler word1 cap word2; invs' s; valid_cap' cap s; valid_cap' (capability.IRQHandlerCap word1) s; isNotificationCap cap; cte_wp_at' (badge_derived' cap \<circ> cteCap) word2 s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word1) ptr' s; word2 \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1\<rbrakk> \<Longrightarrow> word2 \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1 \<and> cte_wp_at' (\<lambda>x. badge_derived' cap (cteCap x)) word2 s \<and> word2 \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1 \<and> cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) word2 s \<and> word2 \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1) s \<and> \<not> isIRQHandlerCap cap proof (prove)
goal (1 subgoal):
 1. \<And>word1 cap word2 s ptr'. \<lbrakk>i = irqhandler_invocation.SetIRQHandler word1 cap word2; invs' s; valid_cap' cap s; valid_cap' (capability.IRQHandlerCap word1) s; isNotificationCap cap; cte_wp_at' (badge_derived' cap \<circ> cteCap) word2 s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.IRQHandlerCap word1) ptr' s; word2 \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>x. badge_derived' cap (cteCap x)) word2 s \<and> cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) word2 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1) s \<and> \<not> isIRQHandlerCap cap proof (prove)
goal (1 subgoal):
 1. \<And>word1 word2 s ptr' v0 cte ctea v1 v2 v3. \<lbrakk>i = irqhandler_invocation.SetIRQHandler word1 (capability.NotificationCap v0 v1 v2 v3) word2; invs' s; valid_cap' (capability.NotificationCap v0 v1 v2 v3) s; valid_cap' (capability.IRQHandlerCap word1) s; word2 \<noteq> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1; ctes_of s word2 = Some cte; badge_derived' (capability.NotificationCap v0 v1 v2 v3) (cteCap cte); ctes_of s ptr' = Some ctea; cteCap ctea = capability.IRQHandlerCap word1\<rbrakk> \<Longrightarrow> \<exists>cref cte. ctes_of s cref = Some cte \<and> irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) word1 \<in> cte_refs' (cteCap cte) (irq_node' s) proof (prove)
goal:
No subgoals!