theory Example_Valid_State

lemma s0_caps_of_state :
  "caps_of_state s0_internal p = Some cap \<Longrightarrow>
     cap = NullCap \<or>
     (p,cap) \<in>
       { ((Low_cnode_ptr::obj_ref,(the_nat_to_bl_10 1)),  ThreadCap Low_tcb_ptr),
         ((Low_cnode_ptr::obj_ref,(the_nat_to_bl_10 2)),  CNodeCap Low_cnode_ptr 10 (the_nat_to_bl_10 2)),
         ((Low_cnode_ptr::obj_ref,(the_nat_to_bl_10 3)),  ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))),
         ((Low_cnode_ptr::obj_ref,(the_nat_to_bl_10 318)),NotificationCap ntfn_ptr 0 {AllowSend}),
         ((High_cnode_ptr::obj_ref,(the_nat_to_bl_10 1)),  ThreadCap High_tcb_ptr),
         ((High_cnode_ptr::obj_ref,(the_nat_to_bl_10 2)),  CNodeCap High_cnode_ptr 10 (the_nat_to_bl_10 2)),
         ((High_cnode_ptr::obj_ref,(the_nat_to_bl_10 3)),  ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))),
         ((High_cnode_ptr::obj_ref,(the_nat_to_bl_10 318)),NotificationCap  ntfn_ptr 0 {AllowRecv}) ,
         ((Silc_cnode_ptr::obj_ref,(the_nat_to_bl_10 2)),CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl_10 2)),
         ((Silc_cnode_ptr::obj_ref,(the_nat_to_bl_10 318)),NotificationCap ntfn_ptr 0 {AllowSend}),
         ((Low_tcb_ptr::obj_ref, (tcb_cnode_index 0)), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl_10 2)),
         ((Low_tcb_ptr::obj_ref, (tcb_cnode_index 1)), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))),
         ((Low_tcb_ptr::obj_ref, (tcb_cnode_index 2)), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}),
         ((Low_tcb_ptr::obj_ref, (tcb_cnode_index 3)), NullCap),
         ((Low_tcb_ptr::obj_ref, (tcb_cnode_index 4)), NullCap),
         ((High_tcb_ptr::obj_ref, (tcb_cnode_index 0)), CNodeCap High_cnode_ptr 10 (the_nat_to_bl_10 2)),
         ((High_tcb_ptr::obj_ref, (tcb_cnode_index 1)), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))),
         ((High_tcb_ptr::obj_ref, (tcb_cnode_index 2)), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}),
         ((High_tcb_ptr::obj_ref, (tcb_cnode_index 3)), NullCap),
         ((High_tcb_ptr::obj_ref, (tcb_cnode_index 4)), NullCap)} " supply if_cong[cong] apply (insert High_caps_well_formed) apply (insert Low_caps_well_formed) apply (insert Silc_caps_well_formed) apply (simp add: caps_of_state_cte_wp_at cte_wp_at_cases s0_internal_def kh0_def kh0_obj_def) apply (case_tac p, clarsimp) apply (clarsimp split: if_splits) apply (clarsimp simp: cte_wp_at_cases tcb_cap_cases_def
                       split: if_split_asm)+ apply (clarsimp simp: Silc_caps_def split: if_splits) apply (clarsimp simp: High_caps_def split: if_splits) apply (clarsimp simp: Low_caps_def cte_wp_at_cases split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s0_internal p = Some cap \<Longrightarrow> cap = NullCap \<or> (p, 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)} proof (prove)
goal (1 subgoal):
 1. caps_of_state s0_internal p = Some cap \<Longrightarrow> cap = NullCap \<or> (p, 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)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s0_internal p = Some cap; well_formed_cnode_n 10 High_caps\<rbrakk> \<Longrightarrow> cap = NullCap \<or> (p, 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)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s0_internal p = Some cap; well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps\<rbrakk> \<Longrightarrow> cap = NullCap \<or> (p, 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)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s0_internal p = Some cap; well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps\<rbrakk> \<Longrightarrow> cap = NullCap \<or> (p, 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)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if \<exists>cap. (\<exists>sz fun. (if fst p = init_global_pd then Some (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) else if fst p = init_globals_frame then Some (ArchObj (DataPage False ARMSmallPage)) else if fst p = idle_tcb_ptr then Some (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>) else if fst p = High_tcb_ptr then Some (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>) else if fst p = Low_tcb_ptr then Some (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>) else if fst p = High_pt_ptr then Some (ArchObj (PageTable High_pt')) else if fst p = Low_pt_ptr then Some (ArchObj (PageTable Low_pt')) else if fst p = High_pd_ptr then Some (ArchObj (PageDirectory High_pd')) else if fst p = Low_pd_ptr then Some (ArchObj (PageDirectory Low_pd')) else if fst p = irq_cnode_ptr then Some (CNode 0 [[] \<mapsto> NullCap]) else if fst p = ntfn_ptr then Some (Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>) else if fst p = Silc_cnode_ptr then Some (CNode 10 Silc_caps) else if fst p = High_cnode_ptr then Some (CNode 10 High_caps) else if fst p = Low_cnode_ptr then Some (CNode 10 Low_caps) else if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = fst p then Some (CNode 0 (empty_cnode 0)) else None) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some cap) \<or> (\<exists>tcb. (if fst p = init_global_pd then Some (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) else if fst p = init_globals_frame then Some (ArchObj (DataPage False ARMSmallPage)) else if fst p = idle_tcb_ptr then Some (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>) else if fst p = High_tcb_ptr then Some (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>) else if fst p = Low_tcb_ptr then Some (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>) else if fst p = High_pt_ptr then Some (ArchObj (PageTable High_pt')) else if fst p = Low_pt_ptr then Some (ArchObj (PageTable Low_pt')) else if fst p = High_pd_ptr then Some (ArchObj (PageDirectory High_pd')) else if fst p = Low_pd_ptr then Some (ArchObj (PageDirectory Low_pd')) else if fst p = irq_cnode_ptr then Some (CNode 0 [[] \<mapsto> NullCap]) else if fst p = ntfn_ptr then Some (Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>) else if fst p = Silc_cnode_ptr then Some (CNode 10 Silc_caps) else if fst p = High_cnode_ptr then Some (CNode 10 High_caps) else if fst p = Low_cnode_ptr then Some (CNode 10 Low_caps) else if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = fst p then Some (CNode 0 (empty_cnode 0)) else None) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> cap = get tcb)) then Some (THE cap. (\<exists>sz fun. (if fst p = init_global_pd then Some (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) else if fst p = init_globals_frame then Some (ArchObj (DataPage False ARMSmallPage)) else if fst p = idle_tcb_ptr then Some (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>) else if fst p = High_tcb_ptr then Some (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>) else if fst p = Low_tcb_ptr then Some (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>) else if fst p = High_pt_ptr then Some (ArchObj (PageTable High_pt')) else if fst p = Low_pt_ptr then Some (ArchObj (PageTable Low_pt')) else if fst p = High_pd_ptr then Some (ArchObj (PageDirectory High_pd')) else if fst p = Low_pd_ptr then Some (ArchObj (PageDirectory Low_pd')) else if fst p = irq_cnode_ptr then Some (CNode 0 [[] \<mapsto> NullCap]) else if fst p = ntfn_ptr then Some (Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>) else if fst p = Silc_cnode_ptr then Some (CNode 10 Silc_caps) else if fst p = High_cnode_ptr then Some (CNode 10 High_caps) else if fst p = Low_cnode_ptr then Some (CNode 10 Low_caps) else if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = fst p then Some (CNode 0 (empty_cnode 0)) else None) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some cap) \<or> (\<exists>tcb. (if fst p = init_global_pd then Some (ArchObj (PageDirectory ((\<lambda>_. InvalidPDE)(UCAST(32 \<rightarrow> 12) (kernel_base >> 20) := SectionPDE (addrFromPPtr kernel_base) {} 0 {})))) else if fst p = init_globals_frame then Some (ArchObj (DataPage False ARMSmallPage)) else if fst p = idle_tcb_ptr then Some (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>) else if fst p = High_tcb_ptr then Some (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>) else if fst p = Low_tcb_ptr then Some (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>) else if fst p = High_pt_ptr then Some (ArchObj (PageTable High_pt')) else if fst p = Low_pt_ptr then Some (ArchObj (PageTable Low_pt')) else if fst p = High_pd_ptr then Some (ArchObj (PageDirectory High_pd')) else if fst p = Low_pd_ptr then Some (ArchObj (PageDirectory Low_pd')) else if fst p = irq_cnode_ptr then Some (CNode 0 [[] \<mapsto> NullCap]) else if fst p = ntfn_ptr then Some (Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>) else if fst p = Silc_cnode_ptr then Some (CNode 10 Silc_caps) else if fst p = High_cnode_ptr then Some (CNode 10 High_caps) else if fst p = Low_cnode_ptr then Some (CNode 10 Low_caps) else if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = fst p then Some (CNode 0 (empty_cnode 0)) else None) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> cap = get tcb))) else None) = Some cap; well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps\<rbrakk> \<Longrightarrow> cap = NullCap \<or> p = (Low_cnode_ptr, the_nat_to_bl 10 (Suc 0)) \<and> cap = ThreadCap Low_tcb_ptr \<or> p = (Low_cnode_ptr, the_nat_to_bl 10 2) \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> p = (Low_cnode_ptr, the_nat_to_bl 10 3) \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> p = (Low_cnode_ptr, the_nat_to_bl 10 318) \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> p = (High_cnode_ptr, the_nat_to_bl 10 (Suc 0)) \<and> cap = ThreadCap High_tcb_ptr \<or> p = (High_cnode_ptr, the_nat_to_bl 10 2) \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> p = (High_cnode_ptr, the_nat_to_bl 10 3) \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> p = (High_cnode_ptr, the_nat_to_bl 10 318) \<and> cap = NotificationCap ntfn_ptr 0 {AllowRead} \<or> p = (Silc_cnode_ptr, the_nat_to_bl 10 2) \<and> cap = CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> p = (Silc_cnode_ptr, the_nat_to_bl 10 318) \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> p = (Low_tcb_ptr, tcb_cnode_index 0) \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> p = (Low_tcb_ptr, tcb_cnode_index (Suc 0)) \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> p = (Low_tcb_ptr, tcb_cnode_index 2) \<and> cap = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite} \<or> p = (Low_tcb_ptr, tcb_cnode_index 3) \<and> cap = NullCap \<or> p = (Low_tcb_ptr, tcb_cnode_index 4) \<and> cap = NullCap \<or> p = (High_tcb_ptr, tcb_cnode_index 0) \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> p = (High_tcb_ptr, tcb_cnode_index (Suc 0)) \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> p = (High_tcb_ptr, tcb_cnode_index 2) \<and> cap = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite} \<or> p = (High_tcb_ptr, tcb_cnode_index 3) \<and> cap = NullCap \<or> p = (High_tcb_ptr, tcb_cnode_index 4) \<and> cap = NullCap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(if \<exists>cap. (\<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 if a = init_globals_frame then Some (ArchObj (DataPage False ARMSmallPage)) else if a = idle_tcb_ptr then Some (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>) else if a = High_tcb_ptr then Some (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>) else if a = Low_tcb_ptr then Some (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>) else if a = High_pt_ptr then Some (ArchObj (PageTable High_pt')) else if a = Low_pt_ptr then Some (ArchObj (PageTable Low_pt')) else if a = High_pd_ptr then Some (ArchObj (PageDirectory High_pd')) else if a = Low_pd_ptr then Some (ArchObj (PageDirectory Low_pd')) else if a = irq_cnode_ptr then Some (CNode 0 [[] \<mapsto> NullCap]) else if a = ntfn_ptr then Some (Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>) else if a = Silc_cnode_ptr then Some (CNode 10 Silc_caps) else if a = High_cnode_ptr then Some (CNode 10 High_caps) else if a = Low_cnode_ptr then Some (CNode 10 Low_caps) else if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = a then Some (CNode 0 (empty_cnode 0)) else None) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some cap) \<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 if a = init_globals_frame then Some (ArchObj (DataPage False ARMSmallPage)) else if a = idle_tcb_ptr then Some (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>) else if a = High_tcb_ptr then Some (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>) else if a = Low_tcb_ptr then Some (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>) else if a = High_pt_ptr then Some (ArchObj (PageTable High_pt')) else if a = Low_pt_ptr then Some (ArchObj (PageTable Low_pt')) else if a = High_pd_ptr then Some (ArchObj (PageDirectory High_pd')) else if a = Low_pd_ptr then Some (ArchObj (PageDirectory Low_pd')) else if a = irq_cnode_ptr then Some (CNode 0 [[] \<mapsto> NullCap]) else if a = ntfn_ptr then Some (Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>) else if a = Silc_cnode_ptr then Some (CNode 10 Silc_caps) else if a = High_cnode_ptr then Some (CNode 10 High_caps) else if a = Low_cnode_ptr then Some (CNode 10 Low_caps) else if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = a then Some (CNode 0 (empty_cnode 0)) else None) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb)) then Some (THE cap. (\<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 if a = init_globals_frame then Some (ArchObj (DataPage False ARMSmallPage)) else if a = idle_tcb_ptr then Some (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>) else if a = High_tcb_ptr then Some (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>) else if a = Low_tcb_ptr then Some (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>) else if a = High_pt_ptr then Some (ArchObj (PageTable High_pt')) else if a = Low_pt_ptr then Some (ArchObj (PageTable Low_pt')) else if a = High_pd_ptr then Some (ArchObj (PageDirectory High_pd')) else if a = Low_pd_ptr then Some (ArchObj (PageDirectory Low_pd')) else if a = irq_cnode_ptr then Some (CNode 0 [[] \<mapsto> NullCap]) else if a = ntfn_ptr then Some (Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>) else if a = Silc_cnode_ptr then Some (CNode 10 Silc_caps) else if a = High_cnode_ptr then Some (CNode 10 High_caps) else if a = Low_cnode_ptr then Some (CNode 10 Low_caps) else if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = a then Some (CNode 0 (empty_cnode 0)) else None) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun b = Some cap) \<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 if a = init_globals_frame then Some (ArchObj (DataPage False ARMSmallPage)) else if a = idle_tcb_ptr then Some (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>) else if a = High_tcb_ptr then Some (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>) else if a = Low_tcb_ptr then Some (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>) else if a = High_pt_ptr then Some (ArchObj (PageTable High_pt')) else if a = Low_pt_ptr then Some (ArchObj (PageTable Low_pt')) else if a = High_pd_ptr then Some (ArchObj (PageDirectory High_pd')) else if a = Low_pd_ptr then Some (ArchObj (PageDirectory Low_pd')) else if a = irq_cnode_ptr then Some (CNode 0 [[] \<mapsto> NullCap]) else if a = ntfn_ptr then Some (Notification \<lparr>ntfn_obj = WaitingNtfn [High_tcb_ptr], ntfn_bound_tcb = None\<rparr>) else if a = Silc_cnode_ptr then Some (CNode 10 Silc_caps) else if a = High_cnode_ptr then Some (CNode 10 High_caps) else if a = Low_cnode_ptr then Some (CNode 10 Low_caps) else if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = a then Some (CNode 0 (empty_cnode 0)) else None) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> cap = get tcb))) else None) = Some cap; well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (a, b); cap \<noteq> NullCap; b = the_nat_to_bl 10 (Suc 0) \<longrightarrow> a = Low_cnode_ptr \<longrightarrow> cap \<noteq> ThreadCap Low_tcb_ptr; b = the_nat_to_bl 10 2 \<longrightarrow> a = Low_cnode_ptr \<longrightarrow> cap \<noteq> CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 3 \<longrightarrow> a = Low_cnode_ptr \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)); b = the_nat_to_bl 10 318 \<longrightarrow> a = Low_cnode_ptr \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowWrite}; b = the_nat_to_bl 10 (Suc 0) \<longrightarrow> a = High_cnode_ptr \<longrightarrow> cap \<noteq> ThreadCap High_tcb_ptr; b = the_nat_to_bl 10 2 \<longrightarrow> a = High_cnode_ptr \<longrightarrow> cap \<noteq> CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 3 \<longrightarrow> a = High_cnode_ptr \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)); b = the_nat_to_bl 10 318 \<longrightarrow> a = High_cnode_ptr \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowRead}; b = the_nat_to_bl 10 2 \<longrightarrow> a = Silc_cnode_ptr \<longrightarrow> cap \<noteq> CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 318 \<longrightarrow> a = Silc_cnode_ptr \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowWrite}; b = tcb_cnode_index 0 \<longrightarrow> a = Low_tcb_ptr \<longrightarrow> cap \<noteq> CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2); b = tcb_cnode_index (Suc 0) \<longrightarrow> a = Low_tcb_ptr \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)); b = tcb_cnode_index 2 \<longrightarrow> a = Low_tcb_ptr \<longrightarrow> cap \<noteq> ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}; b = tcb_cnode_index 0 \<longrightarrow> a = High_tcb_ptr \<longrightarrow> cap \<noteq> CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2); b = tcb_cnode_index (Suc 0) \<longrightarrow> a = High_tcb_ptr \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)); b = tcb_cnode_index 2 \<longrightarrow> a = High_tcb_ptr \<longrightarrow> cap \<noteq> ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>b get set restr. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (idle_tcb_ptr, b); 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> \<noteq> NullCap; cap = 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> False
 2. \<And>b get set restr. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (High_tcb_ptr, b); 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> \<noteq> NullCap; b \<noteq> tcb_cnode_index 0; b \<noteq> tcb_cnode_index (Suc 0); b \<noteq> tcb_cnode_index 2; cap = 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> False
 3. \<And>b get set restr. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (Low_tcb_ptr, b); 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> \<noteq> NullCap; b \<noteq> tcb_cnode_index 0; b \<noteq> tcb_cnode_index (Suc 0); b \<noteq> tcb_cnode_index 2; cap = 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> False
 4. \<And>b. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (Silc_cnode_ptr, b); cap \<noteq> NullCap; b = the_nat_to_bl 10 2 \<longrightarrow> cap \<noteq> CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 318 \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowWrite}; Silc_caps b = Some cap\<rbrakk> \<Longrightarrow> False
 5. \<And>b. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (High_cnode_ptr, b); cap \<noteq> NullCap; b = the_nat_to_bl 10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap High_tcb_ptr; b = the_nat_to_bl 10 2 \<longrightarrow> cap \<noteq> CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)); b = the_nat_to_bl 10 318 \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowRead}; High_caps b = Some cap\<rbrakk> \<Longrightarrow> False
 6. \<And>b. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (Low_cnode_ptr, b); cap \<noteq> NullCap; b = the_nat_to_bl 10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap Low_tcb_ptr; b = the_nat_to_bl 10 2 \<longrightarrow> cap \<noteq> CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)); b = the_nat_to_bl 10 318 \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowWrite}; Low_caps b = Some cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (Silc_cnode_ptr, b); cap \<noteq> NullCap; b = the_nat_to_bl 10 2 \<longrightarrow> cap \<noteq> CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 318 \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowWrite}; Silc_caps b = Some cap\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (High_cnode_ptr, b); cap \<noteq> NullCap; b = the_nat_to_bl 10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap High_tcb_ptr; b = the_nat_to_bl 10 2 \<longrightarrow> cap \<noteq> CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)); b = the_nat_to_bl 10 318 \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowRead}; High_caps b = Some cap\<rbrakk> \<Longrightarrow> False
 3. \<And>b. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (Low_cnode_ptr, b); cap \<noteq> NullCap; b = the_nat_to_bl 10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap Low_tcb_ptr; b = the_nat_to_bl 10 2 \<longrightarrow> cap \<noteq> CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)); b = the_nat_to_bl 10 318 \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowWrite}; Low_caps b = Some cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (High_cnode_ptr, b); cap \<noteq> NullCap; b = the_nat_to_bl 10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap High_tcb_ptr; b = the_nat_to_bl 10 2 \<longrightarrow> cap \<noteq> CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)); b = the_nat_to_bl 10 318 \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowRead}; High_caps b = Some cap\<rbrakk> \<Longrightarrow> False
 2. \<And>b. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (Low_cnode_ptr, b); cap \<noteq> NullCap; b = the_nat_to_bl 10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap Low_tcb_ptr; b = the_nat_to_bl 10 2 \<longrightarrow> cap \<noteq> CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)); b = the_nat_to_bl 10 318 \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowWrite}; Low_caps b = Some cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>well_formed_cnode_n 10 High_caps; well_formed_cnode_n 10 Low_caps; well_formed_cnode_n 10 Silc_caps; p = (Low_cnode_ptr, b); cap \<noteq> NullCap; b = the_nat_to_bl 10 (Suc 0) \<longrightarrow> cap \<noteq> ThreadCap Low_tcb_ptr; b = the_nat_to_bl 10 2 \<longrightarrow> cap \<noteq> CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2); b = the_nat_to_bl 10 3 \<longrightarrow> cap \<noteq> ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)); b = the_nat_to_bl 10 318 \<longrightarrow> cap \<noteq> NotificationCap ntfn_ptr 0 {AllowWrite}; Low_caps b = Some cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!