theory ExampleSystem

lemma "pas_refined Sys2PAS s2" apply (clarsimp simp: pas_refined_def) apply (intro conjI) apply (simp add: Sys2_wellformed) apply (simp add: Sys2PAS_def s2_def Sys2AgentMap_def
                      irq_map_wellformed_aux_def) apply (clarsimp simp: auth_graph_map_def
                          Sys2PAS_def
                          state_objs_to_policy_def
                          state_bits_to_policy_def tcb_domain_map_wellformed_aux_def)+ apply (erule state_bits_to_policyp.cases, simp_all) apply (drule s2_caps_of_state, clarsimp) apply (elim disjE, simp_all add: cap_auth_conferred_def
                                          Sys2AgentMap_simps
                                          Sys2AuthGraph_def Sys2AuthGraph_aux_def
                                          complete_AuthGraph_def
                              split: if_split_asm)[1] apply (drule s2_caps_of_state, clarsimp) apply (elim disjE, simp_all)[1] apply (clarsimp simp: state_refs_of_def s2_def kh2_def kh2_obj_def
                       split: if_splits) apply (clarsimp split:if_splits option.splits
                       simp: thread_st_auth_def tcb_states_of_state_def
                             Sys2AgentMap_simps Sys2AuthGraph_def
                             complete_AuthGraph_def Sys2AuthGraph_aux_def
                      dest!: get_tcb_SomeD) apply (simp add: s2_def)  (* this is OK because cdt is empty..*)
      apply (simp add: s2_def)  (* this is OK because cdt is empty..*)

     apply ((clarsimp simp: state_vrefs_def
                           vs_refs_no_global_pts_def
                           s2_def kh2_def
                           kh2_obj_def
                     split: if_splits,
           ((clarsimp split: if_splits
                     simp: pd2_3065_def pd2_3063_def graph_of_def pde_ref_def
                           Sys2AgentMap_simps Sys2AuthGraph_def
                           complete_AuthGraph_def pt2_3077_def pte_ref_def
                           pt2_3072_def pde_ref2_def
                           Sys2AuthGraph_aux_def ptr_range_def)+))+)[1] apply clarsimp apply (erule state_asids_to_policy_aux.cases) apply clarsimp apply (auto simp: Sys2PAS_def Sys2AuthGraph_def Sys2AuthGraph_aux_def
                      complete_AuthGraph_def Sys2AgentMap_simps
                      Sys2ASIDMap_def asid2_3063_def asid2_3065_def
                      asid_low_bits_def
               dest!: s2_caps_of_state)[1] apply (clarsimp simp: state_vrefs_def
                         vs_refs_no_global_pts_def
                         s2_def kh2_def
                         kh2_obj_def
                  split: if_splits) apply (clarsimp simp: s2_def) apply (clarsimp) apply (erule state_irqs_to_policy_aux.cases) apply (auto simp: Sys2PAS_def Sys2AuthGraph_def Sys2AuthGraph_aux_def
                    complete_AuthGraph_def Sys2AgentMap_simps
                    Sys2ASIDMap_def asid2_3063_def asid2_3065_def
             dest!: s2_caps_of_state)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined Sys2PAS s2 proof (prove)
goal (1 subgoal):
 1. pas_wellformed Sys2PAS \<and> irq_map_wellformed Sys2PAS s2 \<and> tcb_domain_map_wellformed_aux Sys2PAS {} \<and> state_objs_in_policy Sys2PAS s2 \<and> state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS \<and> state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (6 subgoals):
 1. pas_wellformed Sys2PAS
 2. irq_map_wellformed Sys2PAS s2
 3. tcb_domain_map_wellformed_aux Sys2PAS {}
 4. state_objs_in_policy Sys2PAS s2
 5. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 6. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (5 subgoals):
 1. irq_map_wellformed Sys2PAS s2
 2. tcb_domain_map_wellformed_aux Sys2PAS {}
 3. state_objs_in_policy Sys2PAS s2
 4. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 5. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (4 subgoals):
 1. tcb_domain_map_wellformed_aux Sys2PAS {}
 2. state_objs_in_policy Sys2PAS s2
 3. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 4. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (3 subgoals):
 1. \<And>x auth y. state_bits_to_policyp (caps_of_state s2) (thread_st_auth s2) (\<lambda>x. None) (cdt s2) (state_vrefs s2) x auth y \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap y) \<in> Sys2AuthGraph
 2. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 3. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (8 subgoals):
 1. \<And>x auth y ptr cap oref autha. \<lbrakk>x = fst ptr; auth = autha; y = oref; caps_of_state s2 ptr = Some cap; oref \<in> obj_refs_ac cap; autha \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst ptr), autha, Sys2AgentMap oref) \<in> Sys2AuthGraph
 2. \<And>x auth y ptr cap oref. \<lbrakk>x = fst ptr; auth = Control; y = oref; caps_of_state s2 ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst ptr), Control, Sys2AgentMap oref) \<in> Sys2AuthGraph
 3. \<And>x auth y. (y, auth) \<in> thread_st_auth s2 x \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap y) \<in> Sys2AuthGraph
 4. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s2 slot' = Some slot; \<not> is_transferable_in slot' s2\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), Control, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 5. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s2 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), DeleteDerived, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 6. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 7. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 8. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (8 subgoals):
 1. \<And>a b cap oref autha. \<lbrakk>oref \<in> obj_refs_ac cap; autha \<in> cap_auth_conferred cap; cap = NullCap \<or> a = 6 \<and> b = the_nat_to_bl_10 (Suc 0) \<and> cap = ThreadCap 0xC07 \<or> a = 6 \<and> b = the_nat_to_bl_10 2 \<and> cap = CNodeCap 6 undefined undefined \<or> a = 6 \<and> b = the_nat_to_bl_10 3 \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)) \<or> a = 6 \<and> b = the_nat_to_bl_10 4 \<and> cap = CNodeCap 5 undefined undefined \<or> a = 7 \<and> b = the_nat_to_bl_10 (Suc 0) \<and> cap = ThreadCap 0xC08 \<or> a = 7 \<and> b = the_nat_to_bl_10 2 \<and> cap = CNodeCap 7 undefined undefined \<or> a = 7 \<and> b = the_nat_to_bl_10 3 \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)) \<or> a = 7 \<and> b = the_nat_to_bl_10 4 \<and> cap = CNodeCap 5 undefined undefined \<or> a = 0xC07 \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap 6 undefined undefined \<or> a = 0xC07 \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)) \<or> a = 0xC07 \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap 0xC07 True {AllowGrant, AllowWrite} \<or> a = 0xC07 \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = 0xC07 \<and> b = tcb_cnode_index 4 \<and> cap = NullCap \<or> a = 0xC08 \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap 7 undefined undefined \<or> a = 0xC08 \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)) \<or> a = 0xC08 \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap 0xC08 True {AllowGrant, AllowWrite} \<or> a = 0xC08 \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = 0xC08 \<and> b = tcb_cnode_index 4 \<and> cap = NullCap\<rbrakk> \<Longrightarrow> (Sys2AgentMap a, autha, Sys2AgentMap oref) \<in> Sys2AuthGraph
 2. \<And>x auth y ptr cap oref. \<lbrakk>x = fst ptr; auth = Control; y = oref; caps_of_state s2 ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst ptr), Control, Sys2AgentMap oref) \<in> Sys2AuthGraph
 3. \<And>x auth y. (y, auth) \<in> thread_st_auth s2 x \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap y) \<in> Sys2AuthGraph
 4. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s2 slot' = Some slot; \<not> is_transferable_in slot' s2\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), Control, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 5. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s2 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), DeleteDerived, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 6. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 7. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 8. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (7 subgoals):
 1. \<And>x auth y ptr cap oref. \<lbrakk>x = fst ptr; auth = Control; y = oref; caps_of_state s2 ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst ptr), Control, Sys2AgentMap oref) \<in> Sys2AuthGraph
 2. \<And>x auth y. (y, auth) \<in> thread_st_auth s2 x \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap y) \<in> Sys2AuthGraph
 3. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s2 slot' = Some slot; \<not> is_transferable_in slot' s2\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), Control, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 4. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s2 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), DeleteDerived, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 5. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 6. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 7. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (7 subgoals):
 1. \<And>a b cap oref. \<lbrakk>oref \<in> untyped_range cap; cap = NullCap \<or> a = 6 \<and> b = the_nat_to_bl_10 (Suc 0) \<and> cap = ThreadCap 0xC07 \<or> a = 6 \<and> b = the_nat_to_bl_10 2 \<and> cap = CNodeCap 6 undefined undefined \<or> a = 6 \<and> b = the_nat_to_bl_10 3 \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)) \<or> a = 6 \<and> b = the_nat_to_bl_10 4 \<and> cap = CNodeCap 5 undefined undefined \<or> a = 7 \<and> b = the_nat_to_bl_10 (Suc 0) \<and> cap = ThreadCap 0xC08 \<or> a = 7 \<and> b = the_nat_to_bl_10 2 \<and> cap = CNodeCap 7 undefined undefined \<or> a = 7 \<and> b = the_nat_to_bl_10 3 \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)) \<or> a = 7 \<and> b = the_nat_to_bl_10 4 \<and> cap = CNodeCap 5 undefined undefined \<or> a = 0xC07 \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap 6 undefined undefined \<or> a = 0xC07 \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)) \<or> a = 0xC07 \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap 0xC07 True {AllowGrant, AllowWrite} \<or> a = 0xC07 \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = 0xC07 \<and> b = tcb_cnode_index 4 \<and> cap = NullCap \<or> a = 0xC08 \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap 7 undefined undefined \<or> a = 0xC08 \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)) \<or> a = 0xC08 \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap 0xC08 True {AllowGrant, AllowWrite} \<or> a = 0xC08 \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = 0xC08 \<and> b = tcb_cnode_index 4 \<and> cap = NullCap\<rbrakk> \<Longrightarrow> (Sys2AgentMap a, Control, Sys2AgentMap oref) \<in> Sys2AuthGraph
 2. \<And>x auth y. (y, auth) \<in> thread_st_auth s2 x \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap y) \<in> Sys2AuthGraph
 3. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s2 slot' = Some slot; \<not> is_transferable_in slot' s2\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), Control, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 4. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s2 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), DeleteDerived, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 5. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 6. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 7. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (6 subgoals):
 1. \<And>x auth y. (y, auth) \<in> thread_st_auth s2 x \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap y) \<in> Sys2AuthGraph
 2. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s2 slot' = Some slot; \<not> is_transferable_in slot' s2\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), Control, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 3. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s2 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), DeleteDerived, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 4. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 5. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 6. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (6 subgoals):
 1. \<And>x auth y. (y, auth) \<in> thread_st_auth \<lparr>kheap = [6 \<mapsto> CNode 10 caps2_6, 7 \<mapsto> CNode 10 caps2_7, 9 \<mapsto> Endpoint IdleEP, 0xBF7 \<mapsto> ArchObj (PageDirectory pd2_3063), 0xBF9 \<mapsto> ArchObj (PageDirectory pd2_3065), 0xC00 \<mapsto> ArchObj (PageTable pt2_3072), 0xC05 \<mapsto> ArchObj (PageTable pt2_3077), 0xC07 \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap 6 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid2_3063)), tcb_reply = ReplyCap 0xC07 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Running, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>, 0xC08 \<mapsto> TCB \<lparr>tcb_ctable = CNodeCap 7 undefined undefined, tcb_vtable = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid2_3065)), tcb_reply = ReplyCap 0xC08 True {AllowGrant, AllowWrite}, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, tcb_fault_handler = undefined, tcb_ipc_buffer = undefined, tcb_fault = undefined, tcb_bound_notification = None, tcb_mcpriority = undefined, tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>], cdt = \<lambda>x. None, is_original_cap = undefined, cur_thread = undefined, idle_thread = undefined, machine_state = undefined, interrupt_irq_node = \<lambda>_. 0x2329, interrupt_states = undefined, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = undefined, arm_next_asid = undefined, arm_asid_map = undefined, arm_global_pd = undefined, arm_global_pts = undefined, arm_kernel_vspace = undefined\<rparr>, exst = exst1\<rparr> x \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap y) \<in> Sys2AuthGraph
 2. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s2 slot' = Some slot; \<not> is_transferable_in slot' s2\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), Control, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 3. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s2 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), DeleteDerived, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 4. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 5. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 6. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (5 subgoals):
 1. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s2 slot' = Some slot; \<not> is_transferable_in slot' s2\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), Control, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 2. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s2 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), DeleteDerived, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 3. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 4. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 5. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (4 subgoals):
 1. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s2 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), DeleteDerived, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 2. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 3. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 4. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (4 subgoals):
 1. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s2 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys2AgentMap (fst slot), DeleteDerived, Sys2AgentMap (fst slot')) \<in> Sys2AuthGraph
 2. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 3. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 4. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (3 subgoals):
 1. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 2. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 3. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (3 subgoals):
 1. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s2 x\<rbrakk> \<Longrightarrow> (Sys2AgentMap x, auth, Sys2AgentMap ptr') \<in> Sys2AuthGraph
 2. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 3. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (2 subgoals):
 1. state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<subseteq> pasPolicy Sys2PAS
 2. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. (a, aa, b) \<in> state_asids_to_policy_aux Sys2PAS (caps_of_state s2) (asid_table s2) (state_vrefs s2) \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS
 2. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (4 subgoals):
 1. \<And>a aa b ptr acap asid. \<lbrakk>a = pasObjectAbs Sys2PAS (fst ptr); aa = Control; b = pasASIDAbs Sys2PAS asid; caps_of_state s2 ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs Sys2PAS asid; aa = ab; b = pasObjectAbs Sys2PAS pdptr; asid_table s2 (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s2 poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS
 3. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs Sys2PAS poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs Sys2PAS asid; asid_table s2 (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS
 4. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (4 subgoals):
 1. \<And>ab ba acap asid. \<lbrakk>caps_of_state s2 (ab, ba) = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (pasObjectAbs Sys2PAS ab, Control, pasASIDAbs Sys2PAS asid) \<in> pasPolicy Sys2PAS
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs Sys2PAS asid; aa = ab; b = pasObjectAbs Sys2PAS pdptr; asid_table s2 (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s2 poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS
 3. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs Sys2PAS poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs Sys2PAS asid; asid_table s2 (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS
 4. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (3 subgoals):
 1. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs Sys2PAS asid; aa = ab; b = pasObjectAbs Sys2PAS pdptr; asid_table s2 (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s2 poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS
 2. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs Sys2PAS poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs Sys2PAS asid; asid_table s2 (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS
 3. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (2 subgoals):
 1. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs Sys2PAS poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs Sys2PAS asid; asid_table s2 (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS
 2. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (1 subgoal):
 1. state_irqs_to_policy Sys2PAS s2 \<subseteq> pasPolicy Sys2PAS proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy Sys2PAS s2 \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = pasObjectAbs Sys2PAS (fst ptr); aa = Control; b = pasIRQAbs Sys2PAS irq; caps_of_state s2 ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys2PAS proof (prove)
goal:
No subgoals!