theory ArchVSpace_AI

lemma pd_at_asid_unique:
  "\<lbrakk> vspace_at_asid asid pd s; vspace_at_asid asid' pd s;
     unique_table_refs (caps_of_state s);
     valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s;
     valid_arch_state s; asid < 2 ^ asid_bits; asid' < 2 ^ asid_bits \<rbrakk>
       \<Longrightarrow> asid = asid'" apply (clarsimp simp: vspace_at_asid_def) apply (drule(1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI])+ apply (clarsimp simp: table_cap_ref_ap_eq[symmetric]) apply (clarsimp simp: table_cap_ref_def
                 split: cap.split_asm arch_cap.split_asm option.split_asm) apply (drule(2) unique_table_refsD,
         simp+, clarsimp simp: table_cap_ref_def,
         erule(1) asid_low_high_bits) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vspace_at_asid asid pd s; vspace_at_asid asid' pd s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; asid < 2 ^ local.asid_bits; asid' < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> asid = asid' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; ([VSRef (asid' && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None] \<rhd> pd) s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; asid < 2 ^ local.asid_bits; asid' < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> asid = asid' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; asid < 2 ^ local.asid_bits; asid' < 2 ^ local.asid_bits; \<exists>slot cap. caps_of_state s slot = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; \<exists>slot cap. caps_of_state s slot = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (asid' && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None]\<rbrakk> \<Longrightarrow> asid = asid' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba cap capa. \<lbrakk>unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; asid < 2 ^ local.asid_bits; asid' < 2 ^ local.asid_bits; caps_of_state s (a, b) = Some cap; caps_of_state s (aa, ba) = Some capa; pd \<in> obj_refs cap; table_cap_ref cap = Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; pd \<in> obj_refs capa; table_cap_ref capa = Some [VSRef (asid' && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None]\<rbrakk> \<Longrightarrow> asid = asid' proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba x2 x2a. \<lbrakk>unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; asid < 2 ^ local.asid_bits; asid' < 2 ^ local.asid_bits; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2))); caps_of_state s (aa, ba) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2a))); x2 && mask local.asid_low_bits = asid && mask local.asid_low_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid); x2a && mask local.asid_low_bits = asid' && mask local.asid_low_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')\<rbrakk> \<Longrightarrow> asid = asid' proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba x2 x2a. \<lbrakk>valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; asid < 2 ^ local.asid_bits; asid' < 2 ^ local.asid_bits; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2))); caps_of_state s (aa, ba) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2a))); x2 && mask local.asid_low_bits = asid' && mask local.asid_low_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid'); x2a && mask local.asid_low_bits = asid' && mask local.asid_low_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid'); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')\<rbrakk> \<Longrightarrow> asid \<le> 2 ^ local.asid_bits - 1
 2. \<And>a aa b ba x2 x2a. \<lbrakk>valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; asid < 2 ^ local.asid_bits; asid' < 2 ^ local.asid_bits; caps_of_state s (a, b) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2))); caps_of_state s (aa, ba) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2a))); x2 && mask local.asid_low_bits = asid' && mask local.asid_low_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid'); x2a && mask local.asid_low_bits = asid' && mask local.asid_low_bits; UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid'); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')\<rbrakk> \<Longrightarrow> asid' \<le> 2 ^ local.asid_bits - 1 proof (prove)
goal:
No subgoals!