theory ArchVSpace_AI

lemma pd_slots_helper:
  "\<lbrakk>a \<in> set slots; b \<in> set slots;
    cte_wp_at (parent_for_refs (Inr (pde, slots))) cptr s\<rbrakk>
   \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits" apply (clarsimp simp add: cte_wp_at_def parent_for_refs_def) apply (drule imageI[where f="\<lambda>x. x && ~~ mask pd_bits"]) apply (drule imageI[where f="\<lambda>x. x && ~~ mask pd_bits"]) apply (simp add: obj_refs_def) apply (case_tac cap, simp+) apply (rename_tac arch_cap) apply (case_tac arch_cap, simp+) apply (drule (1) set_rev_mp) apply (drule (1) set_rev_mp) apply force apply (drule (1) set_rev_mp) apply (drule (1) set_rev_mp) apply force apply (drule (1) set_rev_mp) apply (drule (1) set_rev_mp) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> set slots; b \<in> set slots; cte_wp_at (parent_for_refs (Inr (pde, slots))) cptr s\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>cap y. \<lbrakk>a \<in> set slots; b \<in> set slots; fst (get_cap cptr s) = {(cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> obj_refs cap; is_pd_cap cap; cap_asid cap = Some y\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>cap y. \<lbrakk>b \<in> set slots; fst (get_cap cptr s) = {(cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> obj_refs cap; is_pd_cap cap; cap_asid cap = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>cap y. \<lbrakk>fst (get_cap cptr s) = {(cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> obj_refs cap; is_pd_cap cap; cap_asid cap = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>cap y. \<lbrakk>fst (get_cap cptr s) = {(cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> rec_cap {} (\<lambda>dev r s f. {}) (\<lambda>r b cr. {r}) (\<lambda>r b cr. {r}) (\<lambda>r m cr. {}) (\<lambda>r bits guard. {r}) (\<lambda>r. {r}) {} {} (\<lambda>irq. {}) (\<lambda>ptr b n. {ptr}) (\<lambda>x. set_option (aobj_ref x)) cap; is_pd_cap cap; cap_asid cap = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>cap y x12. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap x12, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref x12); is_pd_cap (ArchObjectCap x12); cap_asid (ArchObjectCap x12) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>cap y arch_cap. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>cap y arch_cap x31 x32 x33 x34 x35. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap (PageCap x31 x32 x33 x34 x35), s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> {x32}; is_pd_cap (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); cap_asid (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits
 2. \<And>cap y arch_cap x41 x42. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits
 3. \<And>cap y arch_cap x51 x52. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>cap y arch_cap x31 x32 x33 x34 x35. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap (PageCap x31 x32 x33 x34 x35), s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> {x32}; is_pd_cap (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); cap_asid (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) = Some y; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); arch_cap = PageCap x31 x32 x33 x34 x35; a && ~~ mask pd_bits \<in> {x32}\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits
 2. \<And>cap y arch_cap x41 x42. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits
 3. \<And>cap y arch_cap x51 x52. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>cap y arch_cap x31 x32 x33 x34 x35. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap (PageCap x31 x32 x33 x34 x35), s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> {x32}; is_pd_cap (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); cap_asid (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) = Some y; cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); arch_cap = PageCap x31 x32 x33 x34 x35; a && ~~ mask pd_bits \<in> {x32}; b && ~~ mask pd_bits \<in> {x32}\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits
 2. \<And>cap y arch_cap x41 x42. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits
 3. \<And>cap y arch_cap x51 x52. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>cap y arch_cap x41 x42. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits
 2. \<And>cap y arch_cap x51 x52. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>cap y arch_cap x41 x42. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageTableCap x41 x42; a && ~~ mask pd_bits \<in> set_option (aobj_ref arch_cap)\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits
 2. \<And>cap y arch_cap x51 x52. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>cap y arch_cap x41 x42. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; cap = ArchObjectCap arch_cap; arch_cap = PageTableCap x41 x42; a && ~~ mask pd_bits \<in> set_option (aobj_ref arch_cap); b && ~~ mask pd_bits \<in> set_option (aobj_ref arch_cap)\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits
 2. \<And>cap y arch_cap x51 x52. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>cap y arch_cap x51 x52. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; a && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>cap y arch_cap x51 x52. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; b && ~~ mask pd_bits \<in> (\<lambda>x. x && ~~ mask pd_bits) ` set slots; cap = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52; a && ~~ mask pd_bits \<in> set_option (aobj_ref arch_cap)\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>cap y arch_cap x51 x52. \<lbrakk>fst (get_cap cptr s) = {(ArchObjectCap arch_cap, s)}; (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> set_option (aobj_ref arch_cap); is_pd_cap (ArchObjectCap arch_cap); cap_asid (ArchObjectCap arch_cap) = Some y; cap = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52; a && ~~ mask pd_bits \<in> set_option (aobj_ref arch_cap); b && ~~ mask pd_bits \<in> set_option (aobj_ref arch_cap)\<rbrakk> \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits proof (prove)
goal:
No subgoals!