theory ArchArch_AC

lemma asid_pool_uniqueness:
  "\<lbrakk> ([VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> p) s;
     arm_asid_table (arch_state s) (asid_high_bits_of asid') = Some p;
     invs s; \<forall>pt. \<not> ko_at (ArchObj (PageTable pt)) p s \<rbrakk>
     \<Longrightarrow> asid_high_bits_of asid' = asid_high_bits_of asid" apply (drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp) apply (drule vs_lookup_atI, drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp) apply (clarsimp dest!: obj_ref_elemD) apply (drule(1) unique_table_refsD[where cps="caps_of_state s", rotated]) apply simp apply (clarsimp simp: vs_cap_ref_def table_cap_ref_def up_ucast_inj_eq
                  split: vmpage_size.splits option.splits cap.splits arch_cap.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> p) s; asid_table s (asid_high_bits_of asid') = Some p; invs s; \<forall>pt. \<not> ako_at (PageTable pt) p s\<rbrakk> \<Longrightarrow> asid_high_bits_of asid' = asid_high_bits_of asid proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid_table s (asid_high_bits_of asid') = Some p; invs s; \<forall>pt. \<not> ako_at (PageTable pt) p s; \<exists>slot cap. caps_of_state s slot = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]\<rbrakk> \<Longrightarrow> asid_high_bits_of asid' = asid_high_bits_of asid proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<forall>pt. \<not> ako_at (PageTable pt) p s; \<exists>slot cap. caps_of_state s slot = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; \<exists>slot cap. caps_of_state s slot = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None]\<rbrakk> \<Longrightarrow> asid_high_bits_of asid' = asid_high_bits_of asid proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ba cap capa. \<lbrakk>invs s; \<forall>pt. \<not> ako_at (PageTable pt) p s; caps_of_state s (a, b) = Some cap; caps_of_state s (aa, ba) = Some capa; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; obj_refs cap = {p}; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None]; obj_refs capa = {p}\<rbrakk> \<Longrightarrow> asid_high_bits_of asid' = asid_high_bits_of asid proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ba cap capa. \<lbrakk>invs s; \<forall>pt. \<not> ako_at (PageTable pt) p s; caps_of_state s (aa, ba) = Some capa; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; obj_refs cap = {p}; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None]; obj_refs capa = {p}\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs capa
 2. \<And>a aa b ba cap capa. \<lbrakk>invs s; \<forall>pt. \<not> ako_at (PageTable pt) p s; caps_of_state s (aa, ba) = Some capa; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; obj_refs cap = {p}; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None]; obj_refs capa = {p}\<rbrakk> \<Longrightarrow> unique_table_refs (caps_of_state s)
 3. \<And>a aa b ba cap capa. \<lbrakk>invs s; \<forall>pt. \<not> ako_at (PageTable pt) p s; caps_of_state s (aa, ba) = Some capa; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; obj_refs cap = {p}; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None]; obj_refs capa = {p}; table_cap_ref cap = table_cap_ref capa\<rbrakk> \<Longrightarrow> asid_high_bits_of asid' = asid_high_bits_of asid proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ba cap capa. \<lbrakk>invs s; \<forall>pt. \<not> ako_at (PageTable pt) p s; caps_of_state s (aa, ba) = Some capa; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; obj_refs cap = {p}; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None]; obj_refs capa = {p}\<rbrakk> \<Longrightarrow> unique_table_refs (caps_of_state s)
 2. \<And>a aa b ba cap capa. \<lbrakk>invs s; \<forall>pt. \<not> ako_at (PageTable pt) p s; caps_of_state s (aa, ba) = Some capa; vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; obj_refs cap = {p}; vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None]; obj_refs capa = {p}; table_cap_ref cap = table_cap_ref capa\<rbrakk> \<Longrightarrow> asid_high_bits_of asid' = asid_high_bits_of asid proof (prove)
goal:
No subgoals!