theory ExampleSystem

lemma "pas_refined Sys1PAS s1" apply (clarsimp simp: pas_refined_def) apply (intro conjI) subgoal by (simp add: Sys1_wellformed) subgoal by (simp add: irq_map_wellformed_aux_def s1_def Sys1AgentMap_simps Sys1PAS_def) subgoal by (simp  add: tcb_domain_map_wellformed_aux_def) apply (clarsimp simp: auth_graph_map_def
                           Sys1PAS_def
                           state_objs_to_policy_def
                           )+ apply (erule state_bits_to_policy.cases, simp_all, clarsimp) apply (drule s1_caps_of_state, clarsimp) apply (simp add: Sys1AuthGraph_def complete_AuthGraph_def Sys1AuthGraph_aux_def) apply (elim disjE conjE; solves\<open>clarsimp simp: Sys1AgentMap_simps cap_auth_conferred_def cap_rights_to_auth_def\<close>) apply (drule s1_caps_of_state, clarsimp) apply (elim disjE; solves \<open>simp add: thread_bound_ntfns_def\<close>) apply (clarsimp simp: state_refs_of_def thread_st_auth_def tcb_states_of_state_1
               Sys1AuthGraph_def Sys1AgentMap_simps
               complete_AuthGraph_def
               Sys1AuthGraph_aux_def
               split: if_splits) apply (simp add:  thread_bound_ntfns_1) apply (simp add: s1_def)  (* this is OK because cdt is empty..*)
      apply (simp add: s1_def)  (* this is OK because cdt is empty..*)

     apply (fastforce simp: state_vrefs_def
                           vs_refs_no_global_pts_def
                           s1_def kh1_def  Sys1AgentMap_simps
                           kh1_obj_def comp_def pt1_3072_def pt1_3077_def pte_ref_def pde_ref2_def pd1_3065_def pd1_3063_def
                           Sys1AuthGraph_def ptr_range_def
                           complete_AuthGraph_def
                           Sys1AuthGraph_aux_def
                     dest!: graph_ofD
                     split: if_splits) apply (rule subsetI, clarsimp) apply (erule state_asids_to_policy_aux.cases) apply clarsimp apply (drule s1_caps_of_state, clarsimp) apply (simp add: Sys1AuthGraph_def complete_AuthGraph_def Sys1AuthGraph_aux_def Sys1PAS_def Sys1ASIDMap_def) apply (elim disjE conjE, simp_all add: Sys1AgentMap_simps cap_auth_conferred_def cap_rights_to_auth_def asid1_3065_def asid1_3063_def
       asid_low_bits_def asid_high_bits_of_def )[1] apply (clarsimp simp: state_vrefs_def
                           vs_refs_no_global_pts_def
                           s1_def kh1_def  Sys1AgentMap_simps
                           kh1_obj_def comp_def pt1_3072_def pt1_3077_def pte_ref_def pde_ref2_def pd1_3065_def pd1_3063_def
                           Sys1AuthGraph_def ptr_range_def
                           complete_AuthGraph_def
                           Sys1AuthGraph_aux_def
                     dest!: graph_ofD
                     split: if_splits) apply (clarsimp simp: s1_def) apply (rule subsetI, clarsimp) apply (erule state_irqs_to_policy_aux.cases) apply (simp add: Sys1AuthGraph_def complete_AuthGraph_def Sys1AuthGraph_aux_def Sys1PAS_def Sys1ASIDMap_def) apply (drule s1_caps_of_state) apply (simp add: Sys1AuthGraph_def complete_AuthGraph_def Sys1AuthGraph_aux_def Sys1PAS_def Sys1ASIDMap_def) apply (elim disjE conjE, simp_all add: Sys1AgentMap_simps cap_auth_conferred_def cap_rights_to_auth_def asid1_3065_def asid1_3063_def
    asid_low_bits_def asid_high_bits_of_def )[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined Sys1PAS s1 proof (prove)
goal (1 subgoal):
 1. pas_wellformed Sys1PAS \<and> irq_map_wellformed Sys1PAS s1 \<and> tcb_domain_map_wellformed_aux Sys1PAS {} \<and> state_objs_in_policy Sys1PAS s1 \<and> state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS \<and> state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (6 subgoals):
 1. pas_wellformed Sys1PAS
 2. irq_map_wellformed Sys1PAS s1
 3. tcb_domain_map_wellformed_aux Sys1PAS {}
 4. state_objs_in_policy Sys1PAS s1
 5. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 6. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (1 subgoal):
 1. pas_wellformed Sys1PAS proof (prove)
goal (5 subgoals):
 1. irq_map_wellformed Sys1PAS s1
 2. tcb_domain_map_wellformed_aux Sys1PAS {}
 3. state_objs_in_policy Sys1PAS s1
 4. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 5. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (1 subgoal):
 1. irq_map_wellformed Sys1PAS s1 proof (prove)
goal (4 subgoals):
 1. tcb_domain_map_wellformed_aux Sys1PAS {}
 2. state_objs_in_policy Sys1PAS s1
 3. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (1 subgoal):
 1. tcb_domain_map_wellformed_aux Sys1PAS {} proof (prove)
goal (3 subgoals):
 1. state_objs_in_policy Sys1PAS s1
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (3 subgoals):
 1. \<And>x auth y. (x, auth, y) \<in> state_bits_to_policy (caps_of_state s1) (thread_st_auth s1) (thread_bound_ntfns s1) (cdt s1) (state_vrefs s1) \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap y) \<in> Sys1AuthGraph
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (9 subgoals):
 1. \<And>a b cap oref autha. \<lbrakk>caps_of_state s1 (a, b) = Some cap; oref \<in> obj_refs_ac cap; autha \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> (Sys1AgentMap a, autha, Sys1AgentMap oref) \<in> Sys1AuthGraph
 2. \<And>x auth y ptr cap oref. \<lbrakk>x = fst ptr; auth = Control; y = oref; caps_of_state s1 ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst ptr), Control, Sys1AgentMap oref) \<in> Sys1AuthGraph
 3. \<And>x auth y. (y, auth) \<in> thread_st_auth s1 x \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap y) \<in> Sys1AuthGraph
 4. \<And>x auth y oref oref' autha. \<lbrakk>x = oref; auth = autha; y = oref'; thread_bound_ntfns s1 oref = Some oref'; autha = Receive \<or> autha = Reset\<rbrakk> \<Longrightarrow> (Sys1AgentMap oref, autha, Sys1AgentMap oref') \<in> Sys1AuthGraph
 5. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s1 slot' = Some slot; \<not> is_transferable_in slot' s1\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), Control, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 6. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s1 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), DeleteDerived, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 7. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 8. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 9. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (9 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 asid1_3063)) \<or> a = 6 \<and> b = the_nat_to_bl_10 318 \<and> cap = EndpointCap 9 0 {AllowWrite} \<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 asid1_3065)) \<or> a = 7 \<and> b = the_nat_to_bl_10 318 \<and> cap = EndpointCap 9 0 {AllowRead} \<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 asid1_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 asid1_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> (Sys1AgentMap a, autha, Sys1AgentMap oref) \<in> Sys1AuthGraph
 2. \<And>x auth y ptr cap oref. \<lbrakk>x = fst ptr; auth = Control; y = oref; caps_of_state s1 ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst ptr), Control, Sys1AgentMap oref) \<in> Sys1AuthGraph
 3. \<And>x auth y. (y, auth) \<in> thread_st_auth s1 x \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap y) \<in> Sys1AuthGraph
 4. \<And>x auth y oref oref' autha. \<lbrakk>x = oref; auth = autha; y = oref'; thread_bound_ntfns s1 oref = Some oref'; autha = Receive \<or> autha = Reset\<rbrakk> \<Longrightarrow> (Sys1AgentMap oref, autha, Sys1AgentMap oref') \<in> Sys1AuthGraph
 5. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s1 slot' = Some slot; \<not> is_transferable_in slot' s1\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), Control, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 6. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s1 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), DeleteDerived, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 7. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 8. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 9. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (9 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 asid1_3063)) \<or> a = 6 \<and> b = the_nat_to_bl_10 318 \<and> cap = EndpointCap 9 0 {AllowWrite} \<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 asid1_3065)) \<or> a = 7 \<and> b = the_nat_to_bl_10 318 \<and> cap = EndpointCap 9 0 {AllowRead} \<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 asid1_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 asid1_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> Sys1AgentMap a = UT1 \<and> autha = SyncSend \<and> Sys1AgentMap oref = EP1 \<or> Sys1AgentMap a = UT1 \<and> autha = Reset \<and> Sys1AgentMap oref = EP1 \<or> Sys1AgentMap a = T1 \<and> autha = Receive \<and> Sys1AgentMap oref = EP1 \<or> Sys1AgentMap a = T1 \<and> autha = Reset \<and> Sys1AgentMap oref = EP1 \<or> Sys1AgentMap oref = Sys1AgentMap a \<and> (Sys1AgentMap a = T1 \<or> Sys1AgentMap a = UT1)
 2. \<And>x auth y ptr cap oref. \<lbrakk>x = fst ptr; auth = Control; y = oref; caps_of_state s1 ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst ptr), Control, Sys1AgentMap oref) \<in> Sys1AuthGraph
 3. \<And>x auth y. (y, auth) \<in> thread_st_auth s1 x \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap y) \<in> Sys1AuthGraph
 4. \<And>x auth y oref oref' autha. \<lbrakk>x = oref; auth = autha; y = oref'; thread_bound_ntfns s1 oref = Some oref'; autha = Receive \<or> autha = Reset\<rbrakk> \<Longrightarrow> (Sys1AgentMap oref, autha, Sys1AgentMap oref') \<in> Sys1AuthGraph
 5. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s1 slot' = Some slot; \<not> is_transferable_in slot' s1\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), Control, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 6. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s1 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), DeleteDerived, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 7. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 8. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 9. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (8 subgoals):
 1. \<And>x auth y ptr cap oref. \<lbrakk>x = fst ptr; auth = Control; y = oref; caps_of_state s1 ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst ptr), Control, Sys1AgentMap oref) \<in> Sys1AuthGraph
 2. \<And>x auth y. (y, auth) \<in> thread_st_auth s1 x \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap y) \<in> Sys1AuthGraph
 3. \<And>x auth y oref oref' autha. \<lbrakk>x = oref; auth = autha; y = oref'; thread_bound_ntfns s1 oref = Some oref'; autha = Receive \<or> autha = Reset\<rbrakk> \<Longrightarrow> (Sys1AgentMap oref, autha, Sys1AgentMap oref') \<in> Sys1AuthGraph
 4. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s1 slot' = Some slot; \<not> is_transferable_in slot' s1\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), Control, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 5. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s1 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), DeleteDerived, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 6. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 7. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 8. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (8 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 asid1_3063)) \<or> a = 6 \<and> b = the_nat_to_bl_10 318 \<and> cap = EndpointCap 9 0 {AllowWrite} \<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 asid1_3065)) \<or> a = 7 \<and> b = the_nat_to_bl_10 318 \<and> cap = EndpointCap 9 0 {AllowRead} \<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 asid1_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 asid1_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> (Sys1AgentMap a, Control, Sys1AgentMap oref) \<in> Sys1AuthGraph
 2. \<And>x auth y. (y, auth) \<in> thread_st_auth s1 x \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap y) \<in> Sys1AuthGraph
 3. \<And>x auth y oref oref' autha. \<lbrakk>x = oref; auth = autha; y = oref'; thread_bound_ntfns s1 oref = Some oref'; autha = Receive \<or> autha = Reset\<rbrakk> \<Longrightarrow> (Sys1AgentMap oref, autha, Sys1AgentMap oref') \<in> Sys1AuthGraph
 4. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s1 slot' = Some slot; \<not> is_transferable_in slot' s1\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), Control, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 5. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s1 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), DeleteDerived, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 6. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 7. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 8. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (7 subgoals):
 1. \<And>x auth y. (y, auth) \<in> thread_st_auth s1 x \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap y) \<in> Sys1AuthGraph
 2. \<And>x auth y oref oref' autha. \<lbrakk>x = oref; auth = autha; y = oref'; thread_bound_ntfns s1 oref = Some oref'; autha = Receive \<or> autha = Reset\<rbrakk> \<Longrightarrow> (Sys1AgentMap oref, autha, Sys1AgentMap oref') \<in> Sys1AuthGraph
 3. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s1 slot' = Some slot; \<not> is_transferable_in slot' s1\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), Control, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 4. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s1 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), DeleteDerived, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 5. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 6. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 7. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (6 subgoals):
 1. \<And>x auth y oref oref' autha. \<lbrakk>x = oref; auth = autha; y = oref'; thread_bound_ntfns s1 oref = Some oref'; autha = Receive \<or> autha = Reset\<rbrakk> \<Longrightarrow> (Sys1AgentMap oref, autha, Sys1AgentMap oref') \<in> Sys1AuthGraph
 2. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s1 slot' = Some slot; \<not> is_transferable_in slot' s1\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), Control, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 3. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s1 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), DeleteDerived, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 4. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 5. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 6. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (5 subgoals):
 1. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = Control; y = fst slot'; cdt s1 slot' = Some slot; \<not> is_transferable_in slot' s1\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), Control, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 2. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s1 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), DeleteDerived, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 3. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 4. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 5. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s1 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), DeleteDerived, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 2. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 3. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>x auth y slot' slot. \<lbrakk>x = fst slot; auth = DeleteDerived; y = fst slot'; cdt s1 slot' = Some slot\<rbrakk> \<Longrightarrow> (Sys1AgentMap (fst slot), DeleteDerived, Sys1AgentMap (fst slot')) \<in> Sys1AuthGraph
 2. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 3. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (3 subgoals):
 1. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (3 subgoals):
 1. \<And>x auth y ptr' uu_ uv_. \<lbrakk>y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s1 x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (2 subgoals):
 1. state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<subseteq> pasPolicy Sys1PAS
 2. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. (a, aa, b) \<in> state_asids_to_policy_aux Sys1PAS (caps_of_state s1) (asid_table s1) (state_vrefs s1) \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 2. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>a aa b ptr acap asid. \<lbrakk>a = pasObjectAbs Sys1PAS (fst ptr); aa = Control; b = pasASIDAbs Sys1PAS asid; caps_of_state s1 ptr = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs Sys1PAS asid; aa = ab; b = pasObjectAbs Sys1PAS pdptr; asid_table s1 (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s1 poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 3. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs Sys1PAS poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs Sys1PAS asid; asid_table s1 (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>ab ba acap asid. \<lbrakk>caps_of_state s1 (ab, ba) = Some (ArchObjectCap acap); asid \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (pasObjectAbs Sys1PAS ab, Control, pasASIDAbs Sys1PAS asid) \<in> pasPolicy Sys1PAS
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs Sys1PAS asid; aa = ab; b = pasObjectAbs Sys1PAS pdptr; asid_table s1 (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s1 poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 3. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs Sys1PAS poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs Sys1PAS asid; asid_table s1 (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>ab ba acap asid. \<lbrakk>asid \<in> acap_asid' acap; ab = 6 \<and> ba = the_nat_to_bl_10 3 \<and> acap = PageDirectoryCap 0xBF7 (Some asid1_3063) \<or> ab = 7 \<and> ba = the_nat_to_bl_10 3 \<and> acap = PageDirectoryCap 0xBF9 (Some asid1_3065) \<or> ab = 0xC07 \<and> ba = tcb_cnode_index (Suc 0) \<and> acap = PageDirectoryCap 0xBF7 (Some asid1_3063) \<or> ab = 0xC08 \<and> ba = tcb_cnode_index (Suc 0) \<and> acap = PageDirectoryCap 0xBF9 (Some asid1_3065)\<rbrakk> \<Longrightarrow> (pasObjectAbs Sys1PAS ab, Control, pasASIDAbs Sys1PAS asid) \<in> pasPolicy Sys1PAS
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs Sys1PAS asid; aa = ab; b = pasObjectAbs Sys1PAS pdptr; asid_table s1 (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s1 poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 3. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs Sys1PAS poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs Sys1PAS asid; asid_table s1 (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>ab ba acap asid. \<lbrakk>asid \<in> acap_asid' acap; ab = 6 \<and> ba = the_nat_to_bl_10 3 \<and> acap = PageDirectoryCap 0xBF7 (Some asid1_3063) \<or> ab = 7 \<and> ba = the_nat_to_bl_10 3 \<and> acap = PageDirectoryCap 0xBF9 (Some asid1_3065) \<or> ab = 0xC07 \<and> ba = tcb_cnode_index (Suc 0) \<and> acap = PageDirectoryCap 0xBF7 (Some asid1_3063) \<or> ab = 0xC08 \<and> ba = tcb_cnode_index (Suc 0) \<and> acap = PageDirectoryCap 0xBF9 (Some asid1_3065)\<rbrakk> \<Longrightarrow> (asid_high_bits_of asid = asid_high_bits_of asid1_3065 \<longrightarrow> (asid_high_bits_of asid1_3065 = asid_high_bits_of asid1_3063 \<longrightarrow> UT1 = Sys1AgentMap ab \<and> (Sys1AgentMap ab = T1 \<or> Sys1AgentMap ab = UT1)) \<and> (asid_high_bits_of asid1_3065 \<noteq> asid_high_bits_of asid1_3063 \<longrightarrow> T1 = Sys1AgentMap ab \<and> (Sys1AgentMap ab = T1 \<or> Sys1AgentMap ab = UT1))) \<and> (asid_high_bits_of asid \<noteq> asid_high_bits_of asid1_3065 \<longrightarrow> (asid_high_bits_of asid = asid_high_bits_of asid1_3063 \<longrightarrow> UT1 = Sys1AgentMap ab \<and> (Sys1AgentMap ab = T1 \<or> Sys1AgentMap ab = UT1)) \<and> (asid_high_bits_of asid \<noteq> asid_high_bits_of asid1_3063 \<longrightarrow> undefined = Sys1AgentMap ab \<and> (Sys1AgentMap ab = T1 \<or> Sys1AgentMap ab = UT1)))
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs Sys1PAS asid; aa = ab; b = pasObjectAbs Sys1PAS pdptr; asid_table s1 (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s1 poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 3. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs Sys1PAS poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs Sys1PAS asid; asid_table s1 (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (3 subgoals):
 1. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs Sys1PAS asid; aa = ab; b = pasObjectAbs Sys1PAS pdptr; asid_table s1 (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s1 poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 2. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs Sys1PAS poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs Sys1PAS asid; asid_table s1 (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (2 subgoals):
 1. \<And>a aa b asid poolptr. \<lbrakk>a = pasObjectAbs Sys1PAS poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs Sys1PAS asid; asid_table s1 (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 2. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (1 subgoal):
 1. state_irqs_to_policy Sys1PAS s1 \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy Sys1PAS s1 \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = pasObjectAbs Sys1PAS (fst ptr); aa = Control; b = pasIRQAbs Sys1PAS irq; caps_of_state s1 ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = Sys1AgentMap (fst ptr); aa = Control; b = IRQ1; caps_of_state s1 ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> IRQ1 = Sys1AgentMap (fst ptr) \<and> (Sys1AgentMap (fst ptr) = T1 \<or> Sys1AgentMap (fst ptr) = UT1) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = Sys1AgentMap (fst ptr); aa = Control; b = IRQ1; irq \<in> cap_irqs_controlled cap; cap = NullCap \<or> (ptr, cap) \<in> {((6, the_nat_to_bl_10 1), ThreadCap 0xC07), ((6, the_nat_to_bl_10 2), CNodeCap 6 undefined undefined), ((6, the_nat_to_bl_10 3), ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid1_3063))), ((6, the_nat_to_bl_10 318), EndpointCap 9 0 {AllowSend}), ((7, the_nat_to_bl_10 1), ThreadCap 0xC08), ((7, the_nat_to_bl_10 2), CNodeCap 7 undefined undefined), ((7, the_nat_to_bl_10 3), ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid1_3065))), ((7, the_nat_to_bl_10 318), EndpointCap 9 0 {AllowRecv}), ((0xC07, tcb_cnode_index 0), CNodeCap 6 undefined undefined), ((0xC07, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid1_3063))), ((0xC07, tcb_cnode_index 2), ReplyCap 0xC07 True {AllowGrant, AllowWrite}), ((0xC07, tcb_cnode_index 3), NullCap), ((0xC07, tcb_cnode_index 4), NullCap), ((0xC08, tcb_cnode_index 0), CNodeCap 7 undefined undefined), ((0xC08, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid1_3065))), ((0xC08, tcb_cnode_index 2), ReplyCap 0xC08 True {AllowGrant, AllowWrite}), ((0xC08, tcb_cnode_index 3), NullCap), ((0xC08, tcb_cnode_index 4), NullCap)}\<rbrakk> \<Longrightarrow> IRQ1 = Sys1AgentMap (fst ptr) \<and> (Sys1AgentMap (fst ptr) = T1 \<or> Sys1AgentMap (fst ptr) = UT1) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = Sys1AgentMap (fst ptr); aa = Control; b = IRQ1; irq \<in> cap_irqs_controlled cap; cap = NullCap \<or> ptr = (6, the_nat_to_bl_10 (Suc 0)) \<and> cap = ThreadCap 0xC07 \<or> ptr = (6, the_nat_to_bl_10 2) \<and> cap = CNodeCap 6 undefined undefined \<or> ptr = (6, the_nat_to_bl_10 3) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid1_3063)) \<or> ptr = (6, the_nat_to_bl_10 318) \<and> cap = EndpointCap 9 0 {AllowWrite} \<or> ptr = (7, the_nat_to_bl_10 (Suc 0)) \<and> cap = ThreadCap 0xC08 \<or> ptr = (7, the_nat_to_bl_10 2) \<and> cap = CNodeCap 7 undefined undefined \<or> ptr = (7, the_nat_to_bl_10 3) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid1_3065)) \<or> ptr = (7, the_nat_to_bl_10 318) \<and> cap = EndpointCap 9 0 {AllowRead} \<or> ptr = (0xC07, tcb_cnode_index 0) \<and> cap = CNodeCap 6 undefined undefined \<or> ptr = (0xC07, tcb_cnode_index (Suc 0)) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF7 (Some asid1_3063)) \<or> ptr = (0xC07, tcb_cnode_index 2) \<and> cap = ReplyCap 0xC07 True {AllowGrant, AllowWrite} \<or> ptr = (0xC07, tcb_cnode_index 3) \<and> cap = NullCap \<or> ptr = (0xC07, tcb_cnode_index 4) \<and> cap = NullCap \<or> ptr = (0xC08, tcb_cnode_index 0) \<and> cap = CNodeCap 7 undefined undefined \<or> ptr = (0xC08, tcb_cnode_index (Suc 0)) \<and> cap = ArchObjectCap (PageDirectoryCap 0xBF9 (Some asid1_3065)) \<or> ptr = (0xC08, tcb_cnode_index 2) \<and> cap = ReplyCap 0xC08 True {AllowGrant, AllowWrite} \<or> ptr = (0xC08, tcb_cnode_index 3) \<and> cap = NullCap \<or> ptr = (0xC08, tcb_cnode_index 4) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> IRQ1 = Sys1AgentMap (fst ptr) \<and> (Sys1AgentMap (fst ptr) = T1 \<or> Sys1AgentMap (fst ptr) = UT1) proof (prove)
goal:
No subgoals!