theory ArchCNodeInv_AI

lemma vs_cap_ref_master [CNodeInv_AI_assms]:
  "\<lbrakk> cap_master_cap cap = cap_master_cap cap';
           cap_asid cap = cap_asid cap';
           cap_asid_base cap = cap_asid_base cap';
           cap_vptr cap = cap_vptr cap' \<rbrakk>
        \<Longrightarrow> vs_cap_ref cap = vs_cap_ref cap'" apply (rule ccontr) apply (clarsimp simp: vs_cap_ref_def cap_master_cap_def
                 split: cap.split_asm) apply (clarsimp simp: cap_asid_def split: arch_cap.split_asm option.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_master_cap cap = cap_master_cap cap'; cap_asid cap = cap_asid cap'; cap_asid_base cap = cap_asid_base cap'; cap_vptr cap = cap_vptr cap'\<rbrakk> \<Longrightarrow> vs_cap_ref cap = vs_cap_ref cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_master_cap cap = cap_master_cap cap'; cap_asid cap = cap_asid cap'; cap_asid_base cap = cap_asid_base cap'; cap_vptr cap = cap_vptr cap'; vs_cap_ref cap \<noteq> vs_cap_ref cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x12 x12a. \<lbrakk>cap' = ArchObjectCap x12; (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) = (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); cap_asid (ArchObjectCap x12a) = cap_asid (ArchObjectCap x12); cap_asid_base (ArchObjectCap x12a) = cap_asid_base (ArchObjectCap x12); cap_vptr (ArchObjectCap x12a) = cap_vptr (ArchObjectCap x12); cap = ArchObjectCap x12a; (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 asida) \<Rightarrow> Some [VSRef (asida && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asida)) None]) \<noteq> (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])\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!