theory Example_Valid_State

lemma valid_arch_caps_s0[simp]:
  "valid_arch_caps s0_internal" apply (clarsimp simp: valid_arch_caps_def) apply (intro conjI) apply (clarsimp simp: valid_vs_lookup_def vs_lookup_pages_def vs_asid_refs_def
                           s0_internal_def arch_state0_def) apply (clarsimp simp: valid_table_caps_def is_pd_cap_def is_pt_cap_def) apply (drule s0_caps_of_state) apply (erule disjE | simp)+ apply (clarsimp simp: unique_table_caps_def is_pd_cap_def is_pt_cap_def) apply (drule s0_caps_of_state)+ apply (erule disjE | simp)+ apply (clarsimp simp: unique_table_refs_def table_cap_ref_def) apply (drule s0_caps_of_state)+ by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_caps s0_internal proof (prove)
goal (1 subgoal):
 1. valid_vs_lookup s0_internal \<and> valid_table_caps s0_internal \<and> unique_table_caps (caps_of_state s0_internal) \<and> unique_table_refs (caps_of_state s0_internal) proof (prove)
goal (4 subgoals):
 1. valid_vs_lookup s0_internal
 2. valid_table_caps s0_internal
 3. unique_table_caps (caps_of_state s0_internal)
 4. unique_table_refs (caps_of_state s0_internal) proof (prove)
goal (3 subgoals):
 1. valid_table_caps s0_internal
 2. unique_table_caps (caps_of_state s0_internal)
 3. unique_table_refs (caps_of_state s0_internal) proof (prove)
goal (3 subgoals):
 1. \<And>r a b cap. caps_of_state s0_internal (a, b) = Some cap \<Longrightarrow> ((\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s0_internal)))) r s0_internal) \<and> ((\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid)) \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s0_internal)))) r s0_internal)
 2. unique_table_caps (caps_of_state s0_internal)
 3. unique_table_refs (caps_of_state s0_internal) proof (prove)
goal (3 subgoals):
 1. \<And>r a b cap. cap = NullCap \<or> ((a, b), cap) \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)} \<Longrightarrow> ((\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s0_internal)))) r s0_internal) \<and> ((\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid)) \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s0_internal)))) r s0_internal)
 2. unique_table_caps (caps_of_state s0_internal)
 3. unique_table_refs (caps_of_state s0_internal) proof (prove)
goal (2 subgoals):
 1. unique_table_caps (caps_of_state s0_internal)
 2. unique_table_refs (caps_of_state s0_internal) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>caps_of_state s0_internal (a, b) = Some cap; caps_of_state s0_internal (aa, ba) = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> ((\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (\<exists>p asid. cap' = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> aa = a \<and> ba = b) \<and> ((\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid)) \<longrightarrow> (\<exists>p asid. cap' = ArchObjectCap (PageTableCap p asid)) \<longrightarrow> aa = a \<and> ba = b)
 2. unique_table_refs (caps_of_state s0_internal) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba cap cap'. \<lbrakk>cap_asid cap = None; obj_refs cap' = obj_refs cap; cap = NullCap \<or> ((a, b), cap) \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)}; cap' = NullCap \<or> ((aa, ba), 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> ((\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> (\<exists>p asid. cap' = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> aa = a \<and> ba = b) \<and> ((\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid)) \<longrightarrow> (\<exists>p asid. cap' = ArchObjectCap (PageTableCap p asid)) \<longrightarrow> aa = a \<and> ba = b)
 2. unique_table_refs (caps_of_state s0_internal) proof (prove)
goal (1 subgoal):
 1. unique_table_refs (caps_of_state s0_internal) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba cap cap'. \<lbrakk>caps_of_state s0_internal (a, b) = Some cap; caps_of_state s0_internal (aa, ba) = Some cap'; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> (case cap' of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageTableCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageTableCap obj_ref (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageDirectoryCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageDirectoryCap obj_ref (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) = (case cap of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageTableCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageTableCap obj_ref (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageDirectoryCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageDirectoryCap obj_ref (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba cap cap'. \<lbrakk>obj_refs cap' = obj_refs cap; cap = NullCap \<or> ((a, b), cap) \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)}; cap' = NullCap \<or> ((aa, ba), 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> (case cap' of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageTableCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageTableCap obj_ref (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageDirectoryCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageDirectoryCap obj_ref (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) = (case cap of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageTableCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageTableCap obj_ref (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageDirectoryCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageDirectoryCap obj_ref (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None)