theory Tcb_R

lemma checked_insert_tcb_invs'[wp]:
  "\<lbrace>invs' and cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) slot
         and valid_cap' new_cap
         and K (capBadge new_cap = None)
         and K (slot \<in> cte_refs' (ThreadCap target) 0)
         and K (\<not> isReplyCap new_cap \<and> \<not> isIRQControlCap new_cap)\<rbrace>
     checkCapAt new_cap src_slot
      (checkCapAt (ThreadCap target) slot'
       (assertDerived src_slot new_cap (cteInsert new_cap src_slot slot))) \<lbrace>\<lambda>rv. invs'\<rbrace>" supply if_weak_cong[cong] apply (simp add: checkCapAt_def liftM_def assertDerived_def stateAssert_def) apply (wp getCTE_cteCap_wp cteInsert_invs) apply (clarsimp split: option.splits) apply (subst(asm) tree_cte_cteCap_eq[unfolded o_def]) apply (clarsimp split: option.splits) apply (rule conjI) apply (clarsimp simp: sameObjectAs_def3) apply (clarsimp simp: tree_cte_cteCap_eq
                        is_derived'_def untyped_derived_eq_from_sameObjectAs
                        ex_cte_cap_to'_cteCap) apply (erule sameObjectAsE)+ apply (clarsimp simp: badge_derived'_def) apply (frule capBadgeNone_masters, simp) apply (rule conjI) apply (rule_tac x=slot' in exI) subgoal by fastforce apply (clarsimp simp: isCap_simps cteCaps_of_def) apply (erule(1) valid_irq_handlers_ctes_ofD) apply (clarsimp simp: invs'_def valid_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot and valid_cap' new_cap and K (capBadge new_cap = None) and K (slot \<in> cte_refs' (capability.ThreadCap target) 0) and K (\<not> isReplyCap new_cap \<and> \<not> isIRQControlCap new_cap)\<rbrace> checkCapAt new_cap src_slot (checkCapAt (capability.ThreadCap target) slot' (assertDerived src_slot new_cap (cteInsert new_cap src_slot slot))) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot and valid_cap' new_cap and K (capBadge new_cap = None) and K (slot \<in> cte_refs' (capability.ThreadCap target) 0) and K (\<not> isReplyCap new_cap \<and> \<not> isIRQControlCap new_cap)\<rbrace> checkCapAt new_cap src_slot (checkCapAt (capability.ThreadCap target) slot' (assertDerived src_slot new_cap (cteInsert new_cap src_slot slot))) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot and valid_cap' new_cap and (\<lambda>y. capBadge new_cap = None) and (\<lambda>y. slot \<in> (+) target ` dom tcb_cte_cases) and (\<lambda>y. \<not> isReplyCap new_cap \<and> \<not> isIRQControlCap new_cap)\<rbrace> do x <- getCTE src_slot;
when (global.sameObjectAs new_cap (cteCap x)) (do x <- getCTE slot';
when (global.sameObjectAs (capability.ThreadCap target) (cteCap x)) (do y <- do s <- get;
assert (cte_wp_at' (is_derived' (ctes_of s) src_slot new_cap \<circ> cteCap) src_slot s)
od;
cteInsert new_cap src_slot slot
od)
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot and valid_cap' new_cap and (\<lambda>y. capBadge new_cap = None) and (\<lambda>y. slot \<in> (+) target ` dom tcb_cte_cases) and (\<lambda>y. \<not> isReplyCap new_cap \<and> \<not> isIRQControlCap new_cap)) s \<Longrightarrow> case cteCaps_of s src_slot of None \<Rightarrow> True | Some cap \<Rightarrow> (if global.sameObjectAs new_cap cap then \<lambda>s. case cteCaps_of s slot' of None \<Rightarrow> True | Some cap \<Rightarrow> (if global.sameObjectAs (capability.ThreadCap target) cap then \<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src_slot new_cap \<circ> cteCap) src_slot s \<longrightarrow> (invs' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and valid_cap' new_cap and (\<lambda>s. src_slot \<noteq> slot) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src_slot new_cap \<circ> cteCap) src_slot s) and cte_wp_at' (untyped_derived_eq new_cap \<circ> cteCap) src_slot and ex_cte_cap_wp_to' (\<lambda>_. True) slot and (\<lambda>s. \<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)) s else invs') s else invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x a b x2a. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (target + x) s; valid_cap' new_cap s; capBadge new_cap = None; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some x2; cteCaps_of s src_slot = Some x2a; global.sameObjectAs new_cap x2a; global.sameObjectAs (capability.ThreadCap target) x2; cte_wp_at' (is_derived' (ctes_of s) src_slot new_cap \<circ> cteCap) src_slot s\<rbrakk> \<Longrightarrow> src_slot \<noteq> target + x \<and> cte_wp_at' (untyped_derived_eq new_cap \<circ> cteCap) src_slot s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (target + x) s \<and> (\<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x a b x2a. \<lbrakk>invs' s; case cteCaps_of s (target + x) of None \<Rightarrow> False | Some a \<Rightarrow> a = capability.NullCap; valid_cap' new_cap s; capBadge new_cap = None; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some x2; cteCaps_of s src_slot = Some x2a; global.sameObjectAs new_cap x2a; global.sameObjectAs (capability.ThreadCap target) x2; cte_wp_at' (is_derived' (ctes_of s) src_slot new_cap \<circ> cteCap) src_slot s\<rbrakk> \<Longrightarrow> src_slot \<noteq> target + x \<and> cte_wp_at' (untyped_derived_eq new_cap \<circ> cteCap) src_slot s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (target + x) s \<and> (\<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x a b x2a. \<lbrakk>valid_cap' new_cap s; capBadge new_cap = None; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some x2; cteCaps_of s src_slot = Some x2a; global.sameObjectAs new_cap x2a; global.sameObjectAs (capability.ThreadCap target) x2; cte_wp_at' (is_derived' (ctes_of s) src_slot new_cap \<circ> cteCap) src_slot s; invs' s; cteCaps_of s (target + x) = Some capability.NullCap\<rbrakk> \<Longrightarrow> src_slot \<noteq> target + x \<and> cte_wp_at' (untyped_derived_eq new_cap \<circ> cteCap) src_slot s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (target + x) s \<and> (\<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 x a b x2a. \<lbrakk>valid_cap' new_cap s; capBadge new_cap = None; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some x2; cteCaps_of s src_slot = Some x2a; global.sameObjectAs new_cap x2a; global.sameObjectAs (capability.ThreadCap target) x2; cte_wp_at' (is_derived' (ctes_of s) src_slot new_cap \<circ> cteCap) src_slot s; invs' s; cteCaps_of s (target + x) = Some capability.NullCap\<rbrakk> \<Longrightarrow> src_slot \<noteq> target + x
 2. \<And>s x2 x a b x2a. \<lbrakk>valid_cap' new_cap s; capBadge new_cap = None; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some x2; cteCaps_of s src_slot = Some x2a; global.sameObjectAs new_cap x2a; global.sameObjectAs (capability.ThreadCap target) x2; cte_wp_at' (is_derived' (ctes_of s) src_slot new_cap \<circ> cteCap) src_slot s; invs' s; cteCaps_of s (target + x) = Some capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at' (untyped_derived_eq new_cap \<circ> cteCap) src_slot s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (target + x) s \<and> (\<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x a b x2a. \<lbrakk>valid_cap' new_cap s; capBadge new_cap = None; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some x2; cteCaps_of s src_slot = Some x2a; global.sameObjectAs new_cap x2a; global.sameObjectAs (capability.ThreadCap target) x2; cte_wp_at' (is_derived' (ctes_of s) src_slot new_cap \<circ> cteCap) src_slot s; invs' s; cteCaps_of s (target + x) = Some capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at' (untyped_derived_eq new_cap \<circ> cteCap) src_slot s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (target + x) s \<and> (\<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x a b x2a. \<lbrakk>valid_cap' new_cap s; capBadge new_cap = None; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some x2; cteCaps_of s src_slot = Some x2a; global.sameObjectAs new_cap x2a; global.sameObjectAs (capability.ThreadCap target) x2; invs' s; cteCaps_of s (target + x) = Some capability.NullCap; new_cap \<noteq> capability.NullCap; \<not> isZombie x2a; badge_derived' new_cap x2a; isUntypedCap x2a \<longrightarrow> descendants_of' src_slot (ctes_of s) = {}; \<not> isReplyCap x2a; vsCapRef x2a = vsCapRef new_cap \<or> isArchCap isPageCap new_cap; isArchCap isPageTableCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); isArchCap isPageDirectoryCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y)\<rbrakk> \<Longrightarrow> (\<exists>p' c. cteCaps_of s p' = Some c \<and> target + x \<in> cte_refs' c (irq_node' s)) \<and> (\<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x a b x2a. \<lbrakk>valid_cap' new_cap s; capBadge new_cap = None; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some x2; cteCaps_of s src_slot = Some x2a; invs' s; cteCaps_of s (target + x) = Some capability.NullCap; new_cap \<noteq> capability.NullCap; \<not> isZombie x2a; badge_derived' new_cap x2a; isUntypedCap x2a \<longrightarrow> descendants_of' src_slot (ctes_of s) = {}; \<not> isReplyCap x2a; vsCapRef x2a = vsCapRef new_cap \<or> isArchCap isPageCap new_cap; isArchCap isPageTableCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); isArchCap isPageDirectoryCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); capMasterCap new_cap = capMasterCap x2a; \<not> isNullCap new_cap; \<not> isZombie new_cap; \<not> isUntypedCap new_cap; isArchPageCap new_cap \<Longrightarrow> capRange new_cap \<noteq> {}; capMasterCap (capability.ThreadCap target) = capMasterCap x2; \<not> isNullCap (capability.ThreadCap target); \<not> isZombie (capability.ThreadCap target); \<not> isUntypedCap (capability.ThreadCap target); isArchPageCap (capability.ThreadCap target) \<Longrightarrow> capRange (capability.ThreadCap target) \<noteq> {}\<rbrakk> \<Longrightarrow> (\<exists>p' c. cteCaps_of s p' = Some c \<and> target + x \<in> cte_refs' c (irq_node' s)) \<and> (\<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b x2a. \<lbrakk>valid_cap' new_cap s; capBadge new_cap = None; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some (capability.ThreadCap target); cteCaps_of s src_slot = Some x2a; invs' s; cteCaps_of s (target + x) = Some capability.NullCap; new_cap \<noteq> capability.NullCap; \<not> isZombie x2a; capBadge x2a = None; isUntypedCap x2a \<longrightarrow> descendants_of' src_slot (ctes_of s) = {}; \<not> isReplyCap x2a; vsCapRef x2a = vsCapRef new_cap \<or> isArchCap isPageCap new_cap; isArchCap isPageTableCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); isArchCap isPageDirectoryCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); capMasterCap new_cap = capMasterCap x2a; \<not> isZombie new_cap; \<not> isUntypedCap new_cap; isArchPageCap new_cap \<Longrightarrow> capRange new_cap \<noteq> {}; \<not> isZombie (capability.ThreadCap target); isArchPageCap (capability.ThreadCap target) \<Longrightarrow> capRange (capability.ThreadCap target) \<noteq> {}\<rbrakk> \<Longrightarrow> (\<exists>p' c. cteCaps_of s p' = Some c \<and> target + x \<in> cte_refs' c (irq_node' s)) \<and> (\<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b x2a. \<lbrakk>valid_cap' new_cap s; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some (capability.ThreadCap target); cteCaps_of s src_slot = Some x2a; invs' s; cteCaps_of s (target + x) = Some capability.NullCap; new_cap \<noteq> capability.NullCap; \<not> isZombie x2a; capBadge x2a = None; isUntypedCap x2a \<longrightarrow> descendants_of' src_slot (ctes_of s) = {}; \<not> isReplyCap x2a; vsCapRef x2a = vsCapRef new_cap \<or> isArchCap isPageCap new_cap; isArchCap isPageTableCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); isArchCap isPageDirectoryCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); capMasterCap new_cap = capMasterCap x2a; \<not> isZombie new_cap; \<not> isUntypedCap new_cap; isArchPageCap new_cap \<Longrightarrow> capRange new_cap \<noteq> {}; \<not> isZombie (capability.ThreadCap target); isArchPageCap (capability.ThreadCap target) \<Longrightarrow> capRange (capability.ThreadCap target) \<noteq> {}; capBadge new_cap = None\<rbrakk> \<Longrightarrow> (\<exists>p' c. cteCaps_of s p' = Some c \<and> target + x \<in> cte_refs' c (irq_node' s)) \<and> (\<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s) proof (prove)
goal (2 subgoals):
 1. \<And>s x a b x2a. \<lbrakk>valid_cap' new_cap s; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some (capability.ThreadCap target); cteCaps_of s src_slot = Some x2a; invs' s; cteCaps_of s (target + x) = Some capability.NullCap; new_cap \<noteq> capability.NullCap; \<not> isZombie x2a; capBadge x2a = None; isUntypedCap x2a \<longrightarrow> descendants_of' src_slot (ctes_of s) = {}; \<not> isReplyCap x2a; vsCapRef x2a = vsCapRef new_cap \<or> isArchCap isPageCap new_cap; isArchCap isPageTableCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); isArchCap isPageDirectoryCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); capMasterCap new_cap = capMasterCap x2a; \<not> isZombie new_cap; \<not> isUntypedCap new_cap; isArchPageCap new_cap \<Longrightarrow> capRange new_cap \<noteq> {}; \<not> isZombie (capability.ThreadCap target); isArchPageCap (capability.ThreadCap target) \<Longrightarrow> capRange (capability.ThreadCap target) \<noteq> {}; capBadge new_cap = None\<rbrakk> \<Longrightarrow> \<exists>p' c. cteCaps_of s p' = Some c \<and> target + x \<in> cte_refs' c (irq_node' s)
 2. \<And>s x a b x2a. \<lbrakk>valid_cap' new_cap s; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some (capability.ThreadCap target); cteCaps_of s src_slot = Some x2a; invs' s; cteCaps_of s (target + x) = Some capability.NullCap; new_cap \<noteq> capability.NullCap; \<not> isZombie x2a; capBadge x2a = None; isUntypedCap x2a \<longrightarrow> descendants_of' src_slot (ctes_of s) = {}; \<not> isReplyCap x2a; vsCapRef x2a = vsCapRef new_cap \<or> isArchCap isPageCap new_cap; isArchCap isPageTableCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); isArchCap isPageDirectoryCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); capMasterCap new_cap = capMasterCap x2a; \<not> isZombie new_cap; \<not> isUntypedCap new_cap; isArchPageCap new_cap \<Longrightarrow> capRange new_cap \<noteq> {}; \<not> isZombie (capability.ThreadCap target); isArchPageCap (capability.ThreadCap target) \<Longrightarrow> capRange (capability.ThreadCap target) \<noteq> {}; capBadge new_cap = None\<rbrakk> \<Longrightarrow> \<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s proof (prove)
goal (2 subgoals):
 1. \<And>s x a b x2a. \<lbrakk>valid_cap' new_cap s; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some (capability.ThreadCap target); cteCaps_of s src_slot = Some x2a; invs' s; cteCaps_of s (target + x) = Some capability.NullCap; new_cap \<noteq> capability.NullCap; \<not> isZombie x2a; capBadge x2a = None; isUntypedCap x2a \<longrightarrow> descendants_of' src_slot (ctes_of s) = {}; \<not> isReplyCap x2a; vsCapRef x2a = vsCapRef new_cap \<or> isArchCap isPageCap new_cap; isArchCap isPageTableCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); isArchCap isPageDirectoryCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); capMasterCap new_cap = capMasterCap x2a; \<not> isZombie new_cap; \<not> isUntypedCap new_cap; isArchPageCap new_cap \<Longrightarrow> capRange new_cap \<noteq> {}; \<not> isZombie (capability.ThreadCap target); isArchPageCap (capability.ThreadCap target) \<Longrightarrow> capRange (capability.ThreadCap target) \<noteq> {}; capBadge new_cap = None\<rbrakk> \<Longrightarrow> \<exists>c. cteCaps_of s slot' = Some c \<and> target + x \<in> cte_refs' c (irq_node' s)
 2. \<And>s x a b x2a. \<lbrakk>valid_cap' new_cap s; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some (capability.ThreadCap target); cteCaps_of s src_slot = Some x2a; invs' s; cteCaps_of s (target + x) = Some capability.NullCap; new_cap \<noteq> capability.NullCap; \<not> isZombie x2a; capBadge x2a = None; isUntypedCap x2a \<longrightarrow> descendants_of' src_slot (ctes_of s) = {}; \<not> isReplyCap x2a; vsCapRef x2a = vsCapRef new_cap \<or> isArchCap isPageCap new_cap; isArchCap isPageTableCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); isArchCap isPageDirectoryCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); capMasterCap new_cap = capMasterCap x2a; \<not> isZombie new_cap; \<not> isUntypedCap new_cap; isArchPageCap new_cap \<Longrightarrow> capRange new_cap \<noteq> {}; \<not> isZombie (capability.ThreadCap target); isArchPageCap (capability.ThreadCap target) \<Longrightarrow> capRange (capability.ThreadCap target) \<noteq> {}; capBadge new_cap = None\<rbrakk> \<Longrightarrow> \<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' new_cap s_; slot = target + x_; tcb_cte_cases x_ = Some (a_, b_); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s_ slot' = Some (capability.ThreadCap target); cteCaps_of s_ src_slot = Some x2a_; invs' s_; cteCaps_of s_ (target + x_) = Some capability.NullCap; new_cap \<noteq> capability.NullCap; \<not> isZombie x2a_; capBadge x2a_ = None; isUntypedCap x2a_ \<longrightarrow> descendants_of' src_slot (ctes_of s_) = {}; \<not> isReplyCap x2a_; vsCapRef x2a_ = vsCapRef new_cap \<or> isArchCap isPageCap new_cap; isArchCap isPageTableCap x2a_ \<longrightarrow> capASID x2a_ = capASID new_cap \<and> (\<exists>y. capASID x2a_ = Some y); isArchCap isPageDirectoryCap x2a_ \<longrightarrow> capASID x2a_ = capASID new_cap \<and> (\<exists>y. capASID x2a_ = Some y); capMasterCap new_cap = capMasterCap x2a_; \<not> isZombie new_cap; \<not> isUntypedCap new_cap; isArchPageCap new_cap \<Longrightarrow> capRange new_cap \<noteq> {}; \<not> isZombie (capability.ThreadCap target); isArchPageCap (capability.ThreadCap target) \<Longrightarrow> capRange (capability.ThreadCap target) \<noteq> {}; capBadge new_cap = None\<rbrakk> \<Longrightarrow> \<exists>c. cteCaps_of s_ slot' = Some c \<and> target + x_ \<in> cte_refs' c (irq_node' s_) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b x2a. \<lbrakk>valid_cap' new_cap s; slot = target + x; tcb_cte_cases x = Some (a, b); \<not> isReplyCap new_cap; \<not> isIRQControlCap new_cap; cteCaps_of s slot' = Some (capability.ThreadCap target); cteCaps_of s src_slot = Some x2a; invs' s; cteCaps_of s (target + x) = Some capability.NullCap; new_cap \<noteq> capability.NullCap; \<not> isZombie x2a; capBadge x2a = None; isUntypedCap x2a \<longrightarrow> descendants_of' src_slot (ctes_of s) = {}; \<not> isReplyCap x2a; vsCapRef x2a = vsCapRef new_cap \<or> isArchCap isPageCap new_cap; isArchCap isPageTableCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); isArchCap isPageDirectoryCap x2a \<longrightarrow> capASID x2a = capASID new_cap \<and> (\<exists>y. capASID x2a = Some y); capMasterCap new_cap = capMasterCap x2a; \<not> isZombie new_cap; \<not> isUntypedCap new_cap; isArchPageCap new_cap \<Longrightarrow> capRange new_cap \<noteq> {}; \<not> isZombie (capability.ThreadCap target); isArchPageCap (capability.ThreadCap target) \<Longrightarrow> capRange (capability.ThreadCap target) \<noteq> {}; capBadge new_cap = None\<rbrakk> \<Longrightarrow> \<forall>irq. new_cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s proof (prove)
goal (1 subgoal):
 1. \<And>s x a b z za zb irq. \<lbrakk>valid_cap' (capability.IRQHandlerCap irq) s; slot = target + x; tcb_cte_cases x = Some (a, b); invs' s; ctes_of s slot' = Some z; cteCap z = capability.ThreadCap target; ctes_of s src_slot = Some za; ctes_of s (target + x) = Some zb; cteCap zb = capability.NullCap; new_cap = capability.IRQHandlerCap irq; cteCap za = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> irq_issued' irq s proof (prove)
goal (1 subgoal):
 1. \<And>s x a b z za zb irq. \<lbrakk>valid_cap' (capability.IRQHandlerCap irq) s; slot = target + x; tcb_cte_cases x = Some (a, b); invs' s; ctes_of s slot' = Some z; cteCap z = capability.ThreadCap target; ctes_of s (target + x) = Some zb; cteCap zb = capability.NullCap; new_cap = capability.IRQHandlerCap irq; cteCap za = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> valid_irq_handlers' s proof (prove)
goal:
No subgoals!