theory Example_Valid_State

lemma silc_inv_s0:
  "silc_inv Sys1PAS s0_internal s0_internal" apply (clarsimp simp: silc_inv_def) apply (rule conjI, simp add: Sys1PAS_def) apply (rule conjI) apply (clarsimp simp: Sys1PAS_def Sys1AgentMap_def
                         s0_internal_def kh0_def obj_at_def kh0_obj_def
                         is_cap_table_def Silc_caps_well_formed split: if_split_asm) apply (rule conjI) apply (clarsimp simp: Sys1PAS_def Sys1AuthGraph_def) apply (rule conjI) apply clarsimp apply (rule_tac x=Silc_cnode_ptr in exI) apply (rule conjI) apply (rule_tac x="the_nat_to_bl_10 318" in exI) apply (clarsimp simp: slots_holding_overlapping_caps_def2) apply (case_tac "cap = NullCap") apply clarsimp apply (simp add: cte_wp_at_cases s0_internal_def kh0_def kh0_obj_def) apply (case_tac a, clarsimp) apply (clarsimp split: if_splits) apply ((clarsimp simp: intra_label_cap_def cte_wp_at_cases tcb_cap_cases_def
                                   cap_points_to_label_def split: if_split_asm)+)[8] apply (clarsimp simp: intra_label_cap_def cap_points_to_label_def) apply (drule cte_wp_at_caps_of_state' s0_caps_of_state)+ apply ((erule disjE |
          clarsimp simp: Sys1PAS_def Sys1AgentMap_simps
              the_nat_to_bl_def nat_to_bl_def ctes_wp_at_def cte_wp_at_cases
              s0_internal_def kh0_def kh0_obj_def Silc_caps_well_formed obj_refs_def
         | simp add: Silc_caps_def)+)[1] apply (simp add: Sys1PAS_def Sys1AgentMap_simps) apply (intro conjI) apply (clarsimp simp: all_children_def s0_internal_def silc_dom_equiv_def equiv_for_refl) apply (clarsimp simp: all_children_def s0_internal_def silc_dom_equiv_def equiv_for_refl) apply (clarsimp simp: Invariants_AI.cte_wp_at_caps_of_state ) by (auto simp:is_transferable.simps dest:s0_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_inv Sys1PAS s0_internal s0_internal proof (prove)
goal (1 subgoal):
 1. SilcLabel \<noteq> pasSubject Sys1PAS \<and> (\<forall>x. pasObjectAbs Sys1PAS x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s0_internal)) \<and> (\<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy Sys1PAS) \<longrightarrow> y = SilcLabel) \<and> (\<forall>a b cap. cte_wp_at ((=) cap) (a, b) s0_internal \<and> \<not> intra_label_cap Sys1PAS (a, b) s0_internal \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s0_internal) \<and> pasObjectAbs Sys1PAS a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (1 subgoal):
 1. (\<forall>x. pasObjectAbs Sys1PAS x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s0_internal)) \<and> (\<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy Sys1PAS) \<longrightarrow> y = SilcLabel) \<and> (\<forall>a b cap. cte_wp_at ((=) cap) (a, b) s0_internal \<and> \<not> intra_label_cap Sys1PAS (a, b) s0_internal \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s0_internal) \<and> pasObjectAbs Sys1PAS a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (2 subgoals):
 1. \<forall>x. pasObjectAbs Sys1PAS x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s0_internal)
 2. (\<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy Sys1PAS) \<longrightarrow> y = SilcLabel) \<and> (\<forall>a b cap. cte_wp_at ((=) cap) (a, b) s0_internal \<and> \<not> intra_label_cap Sys1PAS (a, b) s0_internal \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s0_internal) \<and> pasObjectAbs Sys1PAS a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (1 subgoal):
 1. (\<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy Sys1PAS) \<longrightarrow> y = SilcLabel) \<and> (\<forall>a b cap. cte_wp_at ((=) cap) (a, b) s0_internal \<and> \<not> intra_label_cap Sys1PAS (a, b) s0_internal \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s0_internal) \<and> pasObjectAbs Sys1PAS a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (2 subgoals):
 1. \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy Sys1PAS) \<longrightarrow> y = SilcLabel
 2. (\<forall>a b cap. cte_wp_at ((=) cap) (a, b) s0_internal \<and> \<not> intra_label_cap Sys1PAS (a, b) s0_internal \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s0_internal) \<and> pasObjectAbs Sys1PAS a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (1 subgoal):
 1. (\<forall>a b cap. cte_wp_at ((=) cap) (a, b) s0_internal \<and> \<not> intra_label_cap Sys1PAS (a, b) s0_internal \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s0_internal) \<and> pasObjectAbs Sys1PAS a = SilcLabel)) \<and> all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (2 subgoals):
 1. \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s0_internal \<and> \<not> intra_label_cap Sys1PAS (a, b) s0_internal \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s0_internal) \<and> pasObjectAbs Sys1PAS a = SilcLabel)
 2. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s0_internal) \<and> pasObjectAbs Sys1PAS a = SilcLabel
 2. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> (\<exists>b. (Silc_cnode_ptr, b) \<in> slots_holding_overlapping_caps cap s0_internal) \<and> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 2. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> \<exists>b. (Silc_cnode_ptr, b) \<in> slots_holding_overlapping_caps cap s0_internal
 2. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 3. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> slots_holding_overlapping_caps cap s0_internal
 2. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 3. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) s0_internal
 2. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 3. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (4 subgoals):
 1. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal; cap = NullCap\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) s0_internal
 2. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) s0_internal
 3. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 4. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) NullCap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) s0_internal
 2. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) s0_internal
 3. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 4. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>(\<exists>sz fun. (if a = init_global_pd then Some (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) else ((\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage))) a) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some NullCap) \<or> (\<exists>tcb. (if a = init_global_pd then Some (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) else ((\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage))) a) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> NullCap = get tcb)); \<not> intra_label_cap Sys1PAS (a, b) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>
 2. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) s0_internal
 3. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 4. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (4 subgoals):
 1. \<And>b n. \<lbrakk>(\<exists>sz fun. (if word_of_nat n = init_global_pd then Some (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) else ((\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage))) (word_of_nat n)) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some NullCap) \<or> (\<exists>tcb. (if word_of_nat n = init_global_pd then Some (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) else ((\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage))) (word_of_nat n)) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> NullCap = get tcb)); \<not> intra_label_cap Sys1PAS (word_of_nat n, b) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; n < 4294967296\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>
 2. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) s0_internal
 3. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 4. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (11 subgoals):
 1. \<And>b n get set restr. \<lbrakk>\<not> intra_label_cap Sys1PAS (idle_tcb_ptr, b) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; n < 4294967296; word_of_nat n = idle_tcb_ptr; NullCap = get \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>; tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>
 2. \<And>b n get set restr. \<lbrakk>\<not> intra_label_cap Sys1PAS (High_tcb_ptr, b) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; n < 4294967296; word_of_nat n = High_tcb_ptr; NullCap = get \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>; tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>
 3. \<And>b n get set restr. \<lbrakk>\<not> intra_label_cap Sys1PAS (Low_tcb_ptr, b) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; n < 4294967296; word_of_nat n = Low_tcb_ptr; NullCap = get \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>; tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>
 4. \<And>n. \<lbrakk>\<not> intra_label_cap Sys1PAS (irq_cnode_ptr, []) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; n < 4294967296; word_of_nat n = irq_cnode_ptr; well_formed_cnode_n 0 [[] \<mapsto> NullCap]\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>
 5. \<And>b n. \<lbrakk>\<not> intra_label_cap Sys1PAS (Silc_cnode_ptr, b) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; n < 4294967296; word_of_nat n = Silc_cnode_ptr; well_formed_cnode_n 10 Silc_caps; Silc_caps b = Some NullCap\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>
 6. \<And>b n. \<lbrakk>\<not> intra_label_cap Sys1PAS (High_cnode_ptr, b) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; n < 4294967296; word_of_nat n = High_cnode_ptr; well_formed_cnode_n 10 High_caps; High_caps b = Some NullCap\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>
 7. \<And>b n. \<lbrakk>\<not> intra_label_cap Sys1PAS (Low_cnode_ptr, b) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; n < 4294967296; word_of_nat n = Low_cnode_ptr; well_formed_cnode_n 10 Low_caps; Low_caps b = Some NullCap\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>
 8. \<And>n irq. \<lbrakk>\<not> intra_label_cap Sys1PAS (word_of_nat n, []) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>; n < 4294967296; word_of_nat n \<noteq> init_global_pd; word_of_nat n \<noteq> init_globals_frame; word_of_nat n \<noteq> idle_tcb_ptr; word_of_nat n \<noteq> High_tcb_ptr; word_of_nat n \<noteq> Low_tcb_ptr; word_of_nat n \<noteq> High_pt_ptr; word_of_nat n \<noteq> Low_pt_ptr; word_of_nat n \<noteq> High_pd_ptr; word_of_nat n \<noteq> Low_pd_ptr; word_of_nat n \<noteq> irq_cnode_ptr; word_of_nat n \<noteq> ntfn_ptr; word_of_nat n \<noteq> Silc_cnode_ptr; word_of_nat n \<noteq> High_cnode_ptr; word_of_nat n \<noteq> Low_cnode_ptr; init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = word_of_nat n; well_formed_cnode_n 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. False) \<lparr>kheap = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some (CNode 0 (empty_cnode 0)) else None)(Low_cnode_ptr \<mapsto> CNode 10 Low_caps, High_cnode_ptr \<mapsto> CNode 10 High_caps, Silc_cnode_ptr \<mapsto> CNode 10 Silc_caps, ntfn_ptr \<mapsto> Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>, irq_cnode_ptr \<mapsto> CNode 0 [[] \<mapsto> NullCap], Low_pd_ptr \<mapsto> ArchObj (PageDirectory Low_pd'), High_pd_ptr \<mapsto> ArchObj (PageDirectory High_pd'), Low_pt_ptr \<mapsto> ArchObj (PageTable Low_pt'), High_pt_ptr \<mapsto> ArchObj (PageTable High_pt'), Low_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), tcb_reply = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = Low_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, High_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), tcb_vtable = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), tcb_reply = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnNotification ntfn_ptr, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = High_mcp, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, idle_tcb_ptr \<mapsto> TCB \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = IdleThreadState, tcb_fault_handler = replicate word_bits False, tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = default_priority, tcb_arch = \<lparr>tcb_context = empty_context\<rparr>\<rparr>, init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), init_global_pd \<mapsto> ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))), cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>
 9. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) s0_internal
 10. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
A total of 11 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) s0_internal
 2. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 3. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (3 subgoals):
 1. \<And>a b cap capa. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; cap \<noteq> NullCap; cte_wp_at ((=) capa) (a, b) s0_internal; (\<exists>x\<in>obj_refs capa. pasObjectAbs Sys1PAS x \<noteq> pasObjectAbs Sys1PAS a) \<or> (\<exists>x\<in>cap_irqs capa. pasIRQAbs Sys1PAS x \<noteq> pasObjectAbs Sys1PAS a)\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) s0_internal
 2. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 3. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (3 subgoals):
 1. \<And>a b cap capa. \<lbrakk>cap \<noteq> NullCap; (\<exists>x\<in>obj_refs capa. pasObjectAbs Sys1PAS x \<noteq> pasObjectAbs Sys1PAS a) \<or> (\<exists>x\<in>cap_irqs capa. pasIRQAbs Sys1PAS x \<noteq> pasObjectAbs Sys1PAS a); cap = NullCap \<or> ((a, b), cap) \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)}; capa = NullCap \<or> ((a, b), capa) \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)}\<rbrakk> \<Longrightarrow> (Silc_cnode_ptr, the_nat_to_bl 10 318) \<in> ctes_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs c \<noteq> {}) s0_internal
 2. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 3. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>cte_wp_at ((=) cap) (a, b) s0_internal; \<not> intra_label_cap Sys1PAS (a, b) s0_internal\<rbrakk> \<Longrightarrow> pasObjectAbs Sys1PAS Silc_cnode_ptr = SilcLabel
 2. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (1 subgoal):
 1. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal) \<and> silc_dom_equiv Sys1PAS s0_internal s0_internal \<and> (\<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal)) proof (prove)
goal (3 subgoals):
 1. all_children (\<lambda>x. pasObjectAbs Sys1PAS (fst x) = SilcLabel) (cdt s0_internal)
 2. silc_dom_equiv Sys1PAS s0_internal s0_internal
 3. \<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal) proof (prove)
goal (2 subgoals):
 1. silc_dom_equiv Sys1PAS s0_internal s0_internal
 2. \<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal) proof (prove)
goal (1 subgoal):
 1. \<forall>a. pasObjectAbs Sys1PAS a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) s0_internal) proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>pasObjectAbs Sys1PAS a = SilcLabel; caps_of_state s0_internal (a, b) = Some cap; cap \<noteq> NullCap; is_transferable_cap cap\<rbrakk> \<Longrightarrow> False