theory Ipc_R

lemma maskCapRights_vsCapRef[simp]:
  "vsCapRef (maskCapRights msk cap) = vsCapRef cap" unfolding vsCapRef_def apply (cases cap, simp_all add: maskCapRights_def isCap_simps Let_def) apply (rename_tac arch_capability) apply (case_tac arch_capability;
         simp add: maskCapRights_def ARM_H.maskCapRights_def isCap_simps Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vsCapRef (global.maskCapRights msk cap) = vsCapRef cap proof (prove)
goal (1 subgoal):
 1. (case global.maskCapRights msk cap of capability.ArchObjectCap (arch_capability.ASIDPoolCap x asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb ARMSection None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb 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] | capability.ArchObjectCap (arch_capability.PageCap x xa xb ARMSuperSection None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb 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] | capability.ArchObjectCap (arch_capability.PageCap x xa xb _ None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb _ (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] | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (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] | capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = (case cap of capability.ArchObjectCap (arch_capability.ASIDPoolCap x asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb ARMSection None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb 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] | capability.ArchObjectCap (arch_capability.PageCap x xa xb ARMSuperSection None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb 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] | capability.ArchObjectCap (arch_capability.PageCap x xa xb _ None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb _ (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] | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (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] | capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> (case Arch.maskCapRights msk x8 of capability.ArchObjectCap (arch_capability.ASIDPoolCap x asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb ARMSection None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb 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] | capability.ArchObjectCap (arch_capability.PageCap x xa xb ARMSuperSection None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb 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] | capability.ArchObjectCap (arch_capability.PageCap x xa xb _ None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb _ (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] | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (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] | capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = (case x8 of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb 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] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb 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] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (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] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (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] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. cap = capability.ArchObjectCap arch_capability \<Longrightarrow> (case Arch.maskCapRights msk arch_capability of capability.ArchObjectCap (arch_capability.ASIDPoolCap x asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb ARMSection None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb 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] | capability.ArchObjectCap (arch_capability.PageCap x xa xb ARMSuperSection None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb 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] | capability.ArchObjectCap (arch_capability.PageCap x xa xb _ None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb _ (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] | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (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] | capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = (case arch_capability of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb 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] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb 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] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (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] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (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] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) proof (prove)
goal:
No subgoals!