theory ArchTcb_AI

lemma use_no_cap_to_obj_asid_strg: (* arch specific *)
  "(cte_at p s \<and> no_cap_to_obj_dr_emp cap s \<and> valid_cap cap s \<and> invs s)
         \<longrightarrow> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap
                \<longrightarrow> table_cap_ref c = table_cap_ref cap \<and> pt_pd_asid c = pt_pd_asid cap) p s" apply (clarsimp simp: cte_wp_at_caps_of_state
                     no_cap_to_obj_with_diff_ref_def
           simp del: split_paired_All) apply (frule caps_of_state_valid_cap, fastforce) apply (erule allE)+ apply (erule (1) impE)+ apply (simp add: table_cap_ref_def pt_pd_asid_def split: cap.splits arch_cap.splits option.splits prod.splits) apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) p s \<and> no_cap_to_obj_dr_emp cap s \<and> s \<turnstile> cap \<and> invs s \<longrightarrow> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<longrightarrow> table_cap_ref c = table_cap_ref cap \<and> pt_pd_asid c = pt_pd_asid cap) p s proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some capa; \<forall>p capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s p = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap; s \<turnstile> cap; invs s; obj_refs capa = obj_refs cap\<rbrakk> \<Longrightarrow> pt_pd_asid capa = pt_pd_asid cap proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some capa; \<forall>p capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s p = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap; s \<turnstile> cap; invs s; obj_refs capa = obj_refs cap; s \<turnstile> capa\<rbrakk> \<Longrightarrow> pt_pd_asid capa = pt_pd_asid cap proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some capa; s \<turnstile> cap; invs s; obj_refs capa = obj_refs cap; s \<turnstile> capa; obj_refs (?cap25 capa) = obj_refs cap \<longrightarrow> caps_of_state s (?p23 capa) = Some (?cap25 capa) \<longrightarrow> table_cap_ref (?cap25 capa) = table_cap_ref cap\<rbrakk> \<Longrightarrow> pt_pd_asid capa = pt_pd_asid cap proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some capa; s \<turnstile> cap; invs s; obj_refs capa = obj_refs cap; s \<turnstile> capa; table_cap_ref capa = table_cap_ref cap\<rbrakk> \<Longrightarrow> pt_pd_asid capa = pt_pd_asid cap proof (prove)
goal (2 subgoals):
 1. \<And>capa x12 x12a x41 x42 x41a x42a x2 x2a x1 x2b x1a x2c. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageTableCap x41 (Some (x1a, x2c)))); s \<turnstile> ArchObjectCap (PageTableCap x41 (Some (x1, x2b))); invs s; x41a = x41; s \<turnstile> ArchObjectCap (PageTableCap x41 (Some (x1a, x2c))); cap = ArchObjectCap (PageTableCap x41 (Some (x1, x2b))); capa = ArchObjectCap (PageTableCap x41 (Some (x1a, x2c))); x12 = PageTableCap x41 (Some (x1, x2b)); x12a = PageTableCap x41 (Some (x1a, x2c)); x42 = Some (x1, x2b); x42a = Some (x1a, x2c); x2 = (x1, x2b); x2a = (x1a, x2c); x2c >> 20 = x2b >> 20 \<and> x1a && mask local.asid_low_bits = x1 && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)\<rbrakk> \<Longrightarrow> x1a = x1
 2. \<And>capa x12 x12a x51 x52 x51a x52a x2 x2a. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageDirectoryCap x51 (Some x2a))); s \<turnstile> ArchObjectCap (PageDirectoryCap x51 (Some x2)); invs s; x51a = x51; s \<turnstile> ArchObjectCap (PageDirectoryCap x51 (Some x2a)); cap = ArchObjectCap (PageDirectoryCap x51 (Some x2)); capa = ArchObjectCap (PageDirectoryCap x51 (Some x2a)); x12 = PageDirectoryCap x51 (Some x2); x12a = PageDirectoryCap x51 (Some x2a); x52 = Some x2; x52a = Some x2a; x2a && mask local.asid_low_bits = x2 && mask local.asid_low_bits \<and> UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2a) = UCAST(7 \<rightarrow> 32) (asid_high_bits_of x2)\<rbrakk> \<Longrightarrow> x2a = x2 proof (prove)
goal:
No subgoals!