theory Example_Valid_State

lemma Sys1_pas_refined:
  "pas_refined Sys1PAS s0_internal" apply (clarsimp simp: pas_refined_def) apply (intro conjI) apply (simp add: Sys1_pas_wellformed) apply (clarsimp simp: irq_map_wellformed_aux_def s0_internal_def Sys1PAS_def) apply (clarsimp simp: Sys1AgentMap_def) apply (clarsimp simp: s0_ptr_defs ptr_range_def pageBits_def cte_level_bits_def) apply word_bitwise apply (clarsimp simp: tcb_domain_map_wellformed_aux_def
                           Sys1PAS_def Sys1AgentMap_def
                           default_domain_def minBound_word
                           High_domain_def Low_domain_def cte_level_bits_def) apply (clarsimp simp: auth_graph_map_def
                          Sys1PAS_def
                          state_objs_to_policy_def
                          state_bits_to_policy_def) apply (erule state_bits_to_policyp.cases, simp_all, clarsimp) apply (drule s0_caps_of_state, clarsimp) apply (simp add: Sys1AuthGraph_def) apply (elim disjE conjE, auto simp: Sys1AgentMap_simps cap_auth_conferred_def cap_rights_to_auth_def)[1] apply (drule s0_caps_of_state, clarsimp) apply (elim disjE, simp_all)[1] apply (clarsimp simp: state_refs_of_def thread_st_auth_def tcb_states_of_state_s0
             Sys1AuthGraph_def Sys1AgentMap_simps split: if_splits) apply (clarsimp simp: state_refs_of_def thread_st_auth_def thread_bounds_of_state_s0) apply (simp add: s0_internal_def)  (* this is OK because cdt is empty..*)
      apply (simp add: s0_internal_def)  (* this is OK because cdt is empty..*)
     apply (clarsimp simp: state_vrefs_def
                           vs_refs_no_global_pts_def
                           s0_internal_def kh0_def  Sys1AgentMap_simps
                           kh0_obj_def comp_def Low_pt'_def High_pt'_def
                           pte_ref_def pde_ref2_def Low_pd'_def High_pd'_def
                           Sys1AuthGraph_def ptr_range_def vspace_cap_rights_to_auth_def
                           vm_read_only_def vm_read_write_def

                     dest!: graph_ofD
                     split: if_splits) apply (rule Sys1AgentMap_simps(13)) apply (simp add: ptr_range_def pageBits_def shared_page_ptr_phys_def) apply (erule notE) apply (rule Sys1AgentMap_simps(13)[symmetric]) apply (simp add: ptr_range_def pageBits_def shared_page_ptr_phys_def) apply (rule subsetI, clarsimp) apply (erule state_asids_to_policy_aux.cases) apply clarsimp apply (drule s0_caps_of_state, clarsimp) apply (simp add: Sys1AuthGraph_def Sys1PAS_def Sys1ASIDMap_def) apply (elim disjE conjE, simp_all add: Sys1AgentMap_simps cap_auth_conferred_def
                                            cap_rights_to_auth_def Low_asid_def High_asid_def
       asid_low_bits_def asid_high_bits_of_def )[1] apply (clarsimp simp: state_vrefs_def
                           vs_refs_no_global_pts_def
                           s0_internal_def kh0_def  Sys1AgentMap_simps
                           kh0_obj_def comp_def Low_pt'_def High_pt'_def
                           pte_ref_def pde_ref2_def Low_pd'_def High_pd'_def
                           Sys1AuthGraph_def ptr_range_def
                     dest!: graph_ofD
                     split: if_splits) apply (clarsimp simp: s0_internal_def arch_state0_def) apply (rule subsetI, clarsimp) apply (erule state_irqs_to_policy_aux.cases) apply (simp add: Sys1AuthGraph_def Sys1PAS_def Sys1ASIDMap_def) apply (drule s0_caps_of_state) apply (simp add: Sys1AuthGraph_def Sys1PAS_def Sys1ASIDMap_def) apply (elim disjE conjE, simp_all add: Sys1AgentMap_simps cap_auth_conferred_def cap_rights_to_auth_def Low_asid_def High_asid_def
     asid_low_bits_def asid_high_bits_of_def )[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined Sys1PAS s0_internal proof (prove)
goal (1 subgoal):
 1. pas_wellformed Sys1PAS \<and> irq_map_wellformed Sys1PAS s0_internal \<and> tcb_domain_map_wellformed_aux Sys1PAS {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)} \<and> state_objs_in_policy Sys1PAS s0_internal \<and> state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS \<and> state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (6 subgoals):
 1. pas_wellformed Sys1PAS
 2. irq_map_wellformed Sys1PAS s0_internal
 3. tcb_domain_map_wellformed_aux Sys1PAS {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)}
 4. state_objs_in_policy Sys1PAS s0_internal
 5. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 6. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (5 subgoals):
 1. irq_map_wellformed Sys1PAS s0_internal
 2. tcb_domain_map_wellformed_aux Sys1PAS {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)}
 3. state_objs_in_policy Sys1PAS s0_internal
 4. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 5. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (5 subgoals):
 1. \<And>irq. Sys1AgentMap (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) = partition_label IRQ0
 2. tcb_domain_map_wellformed_aux Sys1PAS {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)}
 3. state_objs_in_policy Sys1PAS s0_internal
 4. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 5. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (5 subgoals):
 1. \<And>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<in> ptr_range shared_page_ptr_virt pageBits \<Longrightarrow> False
 2. tcb_domain_map_wellformed_aux Sys1PAS {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)}
 3. state_objs_in_policy Sys1PAS s0_internal
 4. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 5. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (5 subgoals):
 1. \<And>irq. \<lbrakk>0xE0006000 \<le> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE0006FFF\<rbrakk> \<Longrightarrow> False
 2. tcb_domain_map_wellformed_aux Sys1PAS {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)}
 3. state_objs_in_policy Sys1PAS s0_internal
 4. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 5. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. tcb_domain_map_wellformed_aux Sys1PAS {(High_tcb_ptr, High_domain), (Low_tcb_ptr, Low_domain), (idle_tcb_ptr, default_domain)}
 2. state_objs_in_policy Sys1PAS s0_internal
 3. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (3 subgoals):
 1. state_objs_in_policy Sys1PAS s0_internal
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (3 subgoals):
 1. \<And>x auth y. state_bits_to_policyp (caps_of_state s0_internal) (thread_st_auth s0_internal) (thread_bound_ntfns s0_internal) (cdt s0_internal) (state_vrefs s0_internal) x auth y \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap y) \<in> Sys1AuthGraph
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (9 subgoals):
 1. \<And>a b cap oref autha. \<lbrakk>caps_of_state s0_internal (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 s0_internal 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 s0_internal 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 s0_internal 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 s0_internal slot' = Some slot; \<not> is_transferable_in slot' s0_internal\<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 s0_internal 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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 8. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 9. state_irqs_to_policy Sys1PAS s0_internal \<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 = Low_cnode_ptr \<and> b = the_nat_to_bl 10 (Suc 0) \<and> cap = ThreadCap Low_tcb_ptr \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 3 \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 (Suc 0) \<and> cap = ThreadCap High_tcb_ptr \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 3 \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowRead} \<or> a = Silc_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Silc_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite} \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 4 \<and> cap = NullCap \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite} \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = High_tcb_ptr \<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 s0_internal 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 s0_internal 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 s0_internal 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 s0_internal slot' = Some slot; \<not> is_transferable_in slot' s0_internal\<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 s0_internal 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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 8. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 9. state_irqs_to_policy Sys1PAS s0_internal \<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 = Low_cnode_ptr \<and> b = the_nat_to_bl 10 (Suc 0) \<and> cap = ThreadCap Low_tcb_ptr \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 3 \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 (Suc 0) \<and> cap = ThreadCap High_tcb_ptr \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 3 \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowRead} \<or> a = Silc_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Silc_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite} \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 4 \<and> cap = NullCap \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite} \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 4 \<and> cap = NullCap\<rbrakk> \<Longrightarrow> Sys1AgentMap a = partition_label High \<and> autha = Read \<and> Sys1AgentMap oref = partition_label Low \<or> Sys1AgentMap a = partition_label Low \<and> autha = Notify \<and> Sys1AgentMap oref = partition_label High \<or> Sys1AgentMap a = partition_label Low \<and> autha = Reset \<and> Sys1AgentMap oref = partition_label High \<or> Sys1AgentMap a = SilcLabel \<and> autha = Notify \<and> Sys1AgentMap oref = partition_label High \<or> Sys1AgentMap a = SilcLabel \<and> autha = Reset \<and> Sys1AgentMap oref = partition_label High \<or> Sys1AgentMap a = Sys1AgentMap oref
 2. \<And>x auth y ptr cap oref. \<lbrakk>x = fst ptr; auth = Control; y = oref; caps_of_state s0_internal 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 s0_internal 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 s0_internal 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 s0_internal slot' = Some slot; \<not> is_transferable_in slot' s0_internal\<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 s0_internal 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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 8. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 9. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal 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 s0_internal 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 s0_internal 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 s0_internal slot' = Some slot; \<not> is_transferable_in slot' s0_internal\<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 s0_internal 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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 7. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 8. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (8 subgoals):
 1. \<And>a b cap oref. \<lbrakk>oref \<in> untyped_range cap; cap = NullCap \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 (Suc 0) \<and> cap = ThreadCap Low_tcb_ptr \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 3 \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> a = Low_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 (Suc 0) \<and> cap = ThreadCap High_tcb_ptr \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 3 \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> a = High_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowRead} \<or> a = Silc_cnode_ptr \<and> b = the_nat_to_bl 10 2 \<and> cap = CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Silc_cnode_ptr \<and> b = the_nat_to_bl 10 318 \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite} \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = Low_tcb_ptr \<and> b = tcb_cnode_index 4 \<and> cap = NullCap \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 0 \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index (Suc 0) \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 2 \<and> cap = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite} \<or> a = High_tcb_ptr \<and> b = tcb_cnode_index 3 \<and> cap = NullCap \<or> a = High_tcb_ptr \<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 s0_internal 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 s0_internal 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 s0_internal slot' = Some slot; \<not> is_transferable_in slot' s0_internal\<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 s0_internal 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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 7. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 8. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (7 subgoals):
 1. \<And>x auth y. (y, auth) \<in> thread_st_auth s0_internal 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 s0_internal 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 s0_internal slot' = Some slot; \<not> is_transferable_in slot' s0_internal\<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 s0_internal 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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 6. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 7. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal 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 s0_internal slot' = Some slot; \<not> is_transferable_in slot' s0_internal\<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 s0_internal 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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 5. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 6. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal slot' = Some slot; \<not> is_transferable_in slot' s0_internal\<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 s0_internal 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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 4. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 5. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal 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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 3. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal 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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 3. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal x\<rbrakk> \<Longrightarrow> (Sys1AgentMap x, auth, Sys1AgentMap ptr') \<in> Sys1AuthGraph
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>ac. \<lbrakk>partition_label High \<noteq> Sys1AgentMap ac; ptrFromPAddr shared_page_ptr_phys \<le> ac; ac \<le> 0xFFF + ptrFromPAddr shared_page_ptr_phys\<rbrakk> \<Longrightarrow> Sys1AgentMap ac = partition_label Low
 2. \<And>ac ba. \<lbrakk>ba = Read \<or> ba = Write; ba = Notify \<longrightarrow> Sys1AgentMap ac \<noteq> partition_label High; partition_label Low \<noteq> Sys1AgentMap ac; ptrFromPAddr shared_page_ptr_phys \<le> ac; ac \<le> 0xFFF + ptrFromPAddr shared_page_ptr_phys\<rbrakk> \<Longrightarrow> ba = Reset \<and> Sys1AgentMap ac = partition_label High
 3. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>ac. \<lbrakk>partition_label High \<noteq> Sys1AgentMap ac; ptrFromPAddr shared_page_ptr_phys \<le> ac; ac \<le> 0xFFF + ptrFromPAddr shared_page_ptr_phys\<rbrakk> \<Longrightarrow> ac \<in> ptr_range shared_page_ptr_virt pageBits
 2. \<And>ac ba. \<lbrakk>ba = Read \<or> ba = Write; ba = Notify \<longrightarrow> Sys1AgentMap ac \<noteq> partition_label High; partition_label Low \<noteq> Sys1AgentMap ac; ptrFromPAddr shared_page_ptr_phys \<le> ac; ac \<le> 0xFFF + ptrFromPAddr shared_page_ptr_phys\<rbrakk> \<Longrightarrow> ba = Reset \<and> Sys1AgentMap ac = partition_label High
 3. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (3 subgoals):
 1. \<And>ac ba. \<lbrakk>ba = Read \<or> ba = Write; ba = Notify \<longrightarrow> Sys1AgentMap ac \<noteq> partition_label High; partition_label Low \<noteq> Sys1AgentMap ac; ptrFromPAddr shared_page_ptr_phys \<le> ac; ac \<le> 0xFFF + ptrFromPAddr shared_page_ptr_phys\<rbrakk> \<Longrightarrow> ba = Reset \<and> Sys1AgentMap ac = partition_label High
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (3 subgoals):
 1. \<And>ac ba. \<lbrakk>ba = Read \<or> ba = Write; ba = Notify \<longrightarrow> Sys1AgentMap ac \<noteq> partition_label High; ptrFromPAddr shared_page_ptr_phys \<le> ac; ac \<le> 0xFFF + ptrFromPAddr shared_page_ptr_phys\<rbrakk> \<Longrightarrow> partition_label Low = Sys1AgentMap ac
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (3 subgoals):
 1. \<And>ac ba. \<lbrakk>ba = Read \<or> ba = Write; ba = Notify \<longrightarrow> Sys1AgentMap ac \<noteq> partition_label High; ptrFromPAddr shared_page_ptr_phys \<le> ac; ac \<le> 0xFFF + ptrFromPAddr shared_page_ptr_phys\<rbrakk> \<Longrightarrow> ac \<in> ptr_range shared_page_ptr_virt pageBits
 2. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (2 subgoals):
 1. state_asids_to_policy_aux Sys1PAS (caps_of_state s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<subseteq> pasPolicy Sys1PAS
 2. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal) (asid_table s0_internal) (state_vrefs s0_internal) \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 2. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal 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 s0_internal (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s0_internal 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 s0_internal (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>ab ba acap asid. \<lbrakk>caps_of_state s0_internal (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 s0_internal (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s0_internal 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 s0_internal (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>ab ba acap asid. \<lbrakk>asid \<in> acap_asid' acap; ab = Low_cnode_ptr \<and> ba = the_nat_to_bl 10 3 \<and> acap = PageDirectoryCap Low_pd_ptr (Some Low_asid) \<or> ab = High_cnode_ptr \<and> ba = the_nat_to_bl 10 3 \<and> acap = PageDirectoryCap High_pd_ptr (Some High_asid) \<or> ab = Low_tcb_ptr \<and> ba = tcb_cnode_index (Suc 0) \<and> acap = PageDirectoryCap Low_pd_ptr (Some Low_asid) \<or> ab = High_tcb_ptr \<and> ba = tcb_cnode_index (Suc 0) \<and> acap = PageDirectoryCap High_pd_ptr (Some High_asid)\<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 s0_internal (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s0_internal 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 s0_internal (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (4 subgoals):
 1. \<And>ab ba acap asid. \<lbrakk>asid \<in> acap_asid' acap; ab = Low_cnode_ptr \<and> ba = the_nat_to_bl 10 3 \<and> acap = PageDirectoryCap Low_pd_ptr (Some Low_asid) \<or> ab = High_cnode_ptr \<and> ba = the_nat_to_bl 10 3 \<and> acap = PageDirectoryCap High_pd_ptr (Some High_asid) \<or> ab = Low_tcb_ptr \<and> ba = tcb_cnode_index (Suc 0) \<and> acap = PageDirectoryCap Low_pd_ptr (Some Low_asid) \<or> ab = High_tcb_ptr \<and> ba = tcb_cnode_index (Suc 0) \<and> acap = PageDirectoryCap High_pd_ptr (Some High_asid)\<rbrakk> \<Longrightarrow> (asid_high_bits_of asid = asid_high_bits_of High_asid \<longrightarrow> (asid_high_bits_of High_asid = asid_high_bits_of Low_asid \<longrightarrow> Sys1AgentMap ab = partition_label Low) \<and> (asid_high_bits_of High_asid \<noteq> asid_high_bits_of Low_asid \<longrightarrow> Sys1AgentMap ab = partition_label High)) \<and> (asid_high_bits_of asid \<noteq> asid_high_bits_of High_asid \<longrightarrow> (asid_high_bits_of asid = asid_high_bits_of Low_asid \<longrightarrow> Sys1AgentMap ab = partition_label Low) \<and> (asid_high_bits_of asid \<noteq> asid_high_bits_of Low_asid \<longrightarrow> Sys1AgentMap ab = undefined))
 2. \<And>a aa b asid poolptr pdptr ab. \<lbrakk>a = pasASIDAbs Sys1PAS asid; aa = ab; b = pasObjectAbs Sys1PAS pdptr; asid_table s0_internal (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s0_internal 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 s0_internal (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 4. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal (asid_high_bits_of asid) = Some poolptr; (pdptr, asid && mask local.asid_low_bits, AASIDPool, ab) \<in> state_vrefs s0_internal 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 s0_internal (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 3. state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy Sys1PAS
 2. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (1 subgoal):
 1. state_irqs_to_policy Sys1PAS s0_internal \<subseteq> pasPolicy Sys1PAS proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy Sys1PAS s0_internal \<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 s0_internal 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 = partition_label IRQ0; caps_of_state s0_internal ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> Sys1AgentMap (fst ptr) = partition_label IRQ0 proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = Sys1AgentMap (fst ptr); aa = Control; b = partition_label IRQ0; irq \<in> cap_irqs_controlled cap; cap = NullCap \<or> (ptr, 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)}\<rbrakk> \<Longrightarrow> Sys1AgentMap (fst ptr) = partition_label IRQ0 proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = Sys1AgentMap (fst ptr); aa = Control; b = partition_label IRQ0; irq \<in> cap_irqs_controlled cap; cap = NullCap \<or> ptr = (Low_cnode_ptr, the_nat_to_bl 10 (Suc 0)) \<and> cap = ThreadCap Low_tcb_ptr \<or> ptr = (Low_cnode_ptr, the_nat_to_bl 10 2) \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> ptr = (Low_cnode_ptr, the_nat_to_bl 10 3) \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> ptr = (Low_cnode_ptr, the_nat_to_bl 10 318) \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> ptr = (High_cnode_ptr, the_nat_to_bl 10 (Suc 0)) \<and> cap = ThreadCap High_tcb_ptr \<or> ptr = (High_cnode_ptr, the_nat_to_bl 10 2) \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> ptr = (High_cnode_ptr, the_nat_to_bl 10 3) \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> ptr = (High_cnode_ptr, the_nat_to_bl 10 318) \<and> cap = NotificationCap ntfn_ptr 0 {AllowRead} \<or> ptr = (Silc_cnode_ptr, the_nat_to_bl 10 2) \<and> cap = CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> ptr = (Silc_cnode_ptr, the_nat_to_bl 10 318) \<and> cap = NotificationCap ntfn_ptr 0 {AllowWrite} \<or> ptr = (Low_tcb_ptr, tcb_cnode_index 0) \<and> cap = CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> ptr = (Low_tcb_ptr, tcb_cnode_index (Suc 0)) \<and> cap = ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)) \<or> ptr = (Low_tcb_ptr, tcb_cnode_index 2) \<and> cap = ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite} \<or> ptr = (Low_tcb_ptr, tcb_cnode_index 3) \<and> cap = NullCap \<or> ptr = (Low_tcb_ptr, tcb_cnode_index 4) \<and> cap = NullCap \<or> ptr = (High_tcb_ptr, tcb_cnode_index 0) \<and> cap = CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2) \<or> ptr = (High_tcb_ptr, tcb_cnode_index (Suc 0)) \<and> cap = ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)) \<or> ptr = (High_tcb_ptr, tcb_cnode_index 2) \<and> cap = ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite} \<or> ptr = (High_tcb_ptr, tcb_cnode_index 3) \<and> cap = NullCap \<or> ptr = (High_tcb_ptr, tcb_cnode_index 4) \<and> cap = NullCap\<rbrakk> \<Longrightarrow> Sys1AgentMap (fst ptr) = partition_label IRQ0 proof (prove)
goal:
No subgoals!