theory ArchIpc_AI

lemma is_derived_cap_rights2[simp, Ipc_AI_assms]:
  "is_derived m p c (cap_rights_update R c') = is_derived m p c c'" apply (case_tac c') apply (simp_all add: cap_rights_update_def) apply (clarsimp simp: is_derived_def is_cap_simps cap_master_cap_def vs_cap_ref_def
                 split: cap.splits bool.splits)+ apply (rename_tac acap1 acap2) apply (case_tac acap1) by (auto simp: acap_rights_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m p c (cap_rights_update R c') = is_derived m p c c' proof (prove)
goal (12 subgoals):
 1. c' = NullCap \<Longrightarrow> is_derived m p c (cap_rights_update R c') = is_derived m p c c'
 2. \<And>x21 x22 x23 x24. c' = UntypedCap x21 x22 x23 x24 \<Longrightarrow> is_derived m p c (cap_rights_update R c') = is_derived m p c c'
 3. \<And>x31 x32 x33. c' = EndpointCap x31 x32 x33 \<Longrightarrow> is_derived m p c (cap_rights_update R c') = is_derived m p c c'
 4. \<And>x41 x42 x43. c' = NotificationCap x41 x42 x43 \<Longrightarrow> is_derived m p c (cap_rights_update R c') = is_derived m p c c'
 5. \<And>x51 x52 x53. c' = ReplyCap x51 x52 x53 \<Longrightarrow> is_derived m p c (cap_rights_update R c') = is_derived m p c c'
 6. \<And>x61 x62 x63. c' = CNodeCap x61 x62 x63 \<Longrightarrow> is_derived m p c (cap_rights_update R c') = is_derived m p c c'
 7. \<And>x7. c' = ThreadCap x7 \<Longrightarrow> is_derived m p c (cap_rights_update R c') = is_derived m p c c'
 8. c' = DomainCap \<Longrightarrow> is_derived m p c (cap_rights_update R c') = is_derived m p c c'
 9. c' = IRQControlCap \<Longrightarrow> is_derived m p c (cap_rights_update R c') = is_derived m p c c'
 10. \<And>x10. c' = IRQHandlerCap x10 \<Longrightarrow> is_derived m p c (cap_rights_update R c') = is_derived m p c c'
A total of 12 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33. c' = EndpointCap x31 x32 x33 \<Longrightarrow> is_derived m p c (EndpointCap x31 x32 R) = is_derived m p c (EndpointCap x31 x32 x33)
 2. \<And>x41 x42 x43. c' = NotificationCap x41 x42 x43 \<Longrightarrow> is_derived m p c (NotificationCap x41 x42 (R - {AllowGrant, AllowGrantReply})) = is_derived m p c (NotificationCap x41 x42 x43)
 3. \<And>x51 x52 x53. c' = ReplyCap x51 x52 x53 \<Longrightarrow> is_derived m p c (ReplyCap x51 x52 (insert AllowWrite (R - {AllowRead, AllowGrantReply}))) = is_derived m p c (ReplyCap x51 x52 x53)
 4. \<And>x12. c' = ArchObjectCap x12 \<Longrightarrow> is_derived m p c (ArchObjectCap (acap_rights_update R x12)) = is_derived m p c (ArchObjectCap x12) proof (prove)
goal (1 subgoal):
 1. \<And>x12 x12a. \<lbrakk>c' = ArchObjectCap x12; c = ArchObjectCap x12a\<rbrakk> \<Longrightarrow> ((case acap_rights_update R x12 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap_rights_update R x12 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case x12a of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> x12a | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. x12a = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap x12a) = cap_asid (ArchObjectCap (acap_rights_update R x12)) \<and> (\<exists>y. cap_asid (ArchObjectCap x12a) = Some y)) \<and> ((\<exists>p asid. x12a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap x12a) = cap_asid (ArchObjectCap (acap_rights_update R x12)) \<and> (\<exists>y. cap_asid (ArchObjectCap x12a) = Some y)) \<and> ((case x12a of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap_rights_update R x12 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p Ra sz m. acap_rights_update R x12 = PageCap dev p Ra sz m))) = ((case x12 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> x12 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case x12a of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> x12a | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. x12a = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap x12a) = cap_asid (ArchObjectCap x12) \<and> (\<exists>y. cap_asid (ArchObjectCap x12a) = Some y)) \<and> ((\<exists>p asid. x12a = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap x12a) = cap_asid (ArchObjectCap x12) \<and> (\<exists>y. cap_asid (ArchObjectCap x12a) = Some y)) \<and> ((case x12a of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case x12 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p R sz m. x12 = PageCap dev p R sz m))) proof (prove)
goal (1 subgoal):
 1. \<And>acap1 acap2. \<lbrakk>c' = ArchObjectCap acap1; c = ArchObjectCap acap2\<rbrakk> \<Longrightarrow> ((case acap_rights_update R acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap_rights_update R acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap_rights_update R acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p Ra sz m. acap_rights_update R acap1 = PageCap dev p Ra sz m))) = ((case acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p R sz m. acap1 = PageCap dev p R sz m))) proof (prove)
goal (5 subgoals):
 1. \<And>acap1 acap2 x11 x12. \<lbrakk>c' = ArchObjectCap acap1; c = ArchObjectCap acap2; acap1 = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> ((case acap_rights_update R acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap_rights_update R acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap_rights_update R acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p Ra sz m. acap_rights_update R acap1 = PageCap dev p Ra sz m))) = ((case acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p R sz m. acap1 = PageCap dev p R sz m)))
 2. \<And>acap1 acap2. \<lbrakk>c' = ArchObjectCap acap1; c = ArchObjectCap acap2; acap1 = ASIDControlCap\<rbrakk> \<Longrightarrow> ((case acap_rights_update R acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap_rights_update R acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap_rights_update R acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p Ra sz m. acap_rights_update R acap1 = PageCap dev p Ra sz m))) = ((case acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p R sz m. acap1 = PageCap dev p R sz m)))
 3. \<And>acap1 acap2 x31 x32 x33 x34 x35. \<lbrakk>c' = ArchObjectCap acap1; c = ArchObjectCap acap2; acap1 = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> ((case acap_rights_update R acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap_rights_update R acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap_rights_update R acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p Ra sz m. acap_rights_update R acap1 = PageCap dev p Ra sz m))) = ((case acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p R sz m. acap1 = PageCap dev p R sz m)))
 4. \<And>acap1 acap2 x41 x42. \<lbrakk>c' = ArchObjectCap acap1; c = ArchObjectCap acap2; acap1 = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> ((case acap_rights_update R acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap_rights_update R acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap_rights_update R acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p Ra sz m. acap_rights_update R acap1 = PageCap dev p Ra sz m))) = ((case acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p R sz m. acap1 = PageCap dev p R sz m)))
 5. \<And>acap1 acap2 x51 x52. \<lbrakk>c' = ArchObjectCap acap1; c = ArchObjectCap acap2; acap1 = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> ((case acap_rights_update R acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap_rights_update R acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap (acap_rights_update R acap1)) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap_rights_update R acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p Ra sz m. acap_rights_update R acap1 = PageCap dev p Ra sz m))) = ((case acap1 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap1 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) = (case acap2 of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap2 | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) \<and> ((\<exists>p asid. acap2 = PageTableCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((\<exists>p asid. acap2 = PageDirectoryCap p asid) \<longrightarrow> cap_asid (ArchObjectCap acap2) = cap_asid (ArchObjectCap acap1) \<and> (\<exists>y. cap_asid (ArchObjectCap acap2) = Some y)) \<and> ((case acap2 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) = (case acap1 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ASIDControlCap \<Rightarrow> None | PageCap dev obj_ref rights ARMSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSection (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] | PageCap dev obj_ref rights ARMSuperSection None \<Rightarrow> None | PageCap dev obj_ref rights ARMSuperSection (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] | PageCap dev obj_ref rights _ None \<Rightarrow> None | PageCap dev obj_ref rights _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), 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] | PageTableCap obj_ref None \<Rightarrow> None | 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] | PageDirectoryCap obj_ref None \<Rightarrow> None | 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]) \<or> (\<exists>dev p R sz m. acap1 = PageCap dev p R sz m)))