theory VSpace_C

lemma cap_to_H_PageCap_tag:
  "\<lbrakk> cap_to_H cap = ArchObjectCap (PageCap d p R sz A);
     cap_lift C_cap = Some cap \<rbrakk> \<Longrightarrow>
    cap_get_tag C_cap = scast cap_frame_cap \<or> cap_get_tag C_cap = scast cap_small_frame_cap" apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) by (simp_all add: Let_def cap_lift_def split_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_to_H cap = capability.ArchObjectCap (arch_capability.PageCap d p R sz A); cap_lift C_cap = Some cap\<rbrakk> \<Longrightarrow> cap_get_tag C_cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag C_cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap proof (prove)
goal (4 subgoals):
 1. \<And>x8. \<lbrakk>cap_lift C_cap = Some (Cap_small_frame_cap x8); cap = Cap_small_frame_cap x8; cap_small_frame_cap_CL.capFMappedASIDHigh_CL x8 = 0; cap_small_frame_cap_CL.capFMappedASIDLow_CL x8 = 0; d = to_bool (cap_small_frame_cap_CL.capFIsDevice_CL x8); p = cap_small_frame_cap_CL.capFBasePtr_CL x8; R = vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL x8); sz = Wellformed_C.ARMSmallPage; A = None; cap_get_tag C_cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> cap_get_tag C_cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap
 2. \<And>x8. \<lbrakk>cap_lift C_cap = Some (Cap_small_frame_cap x8); cap = Cap_small_frame_cap x8; cap_small_frame_cap_CL.capFMappedASIDHigh_CL x8 = 0 \<longrightarrow> cap_small_frame_cap_CL.capFMappedASIDLow_CL x8 \<noteq> 0; d = to_bool (cap_small_frame_cap_CL.capFIsDevice_CL x8); p = cap_small_frame_cap_CL.capFBasePtr_CL x8; R = vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL x8); sz = Wellformed_C.ARMSmallPage; A = Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL x8 << local.asid_low_bits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL x8, cap_small_frame_cap_CL.capFMappedAddress_CL x8); cap_get_tag C_cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> cap_get_tag C_cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap
 3. \<And>x9. \<lbrakk>cap_lift C_cap = Some (Cap_frame_cap x9); cap = Cap_frame_cap x9; cap_frame_cap_CL.capFMappedASIDHigh_CL x9 = 0; cap_frame_cap_CL.capFMappedASIDLow_CL x9 = 0; d = to_bool (cap_frame_cap_CL.capFIsDevice_CL x9); p = cap_frame_cap_CL.capFBasePtr_CL x9; R = vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL x9); sz = framesize_to_H (capFSize_CL x9); A = None; cap_get_tag C_cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> cap_get_tag C_cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap
 4. \<And>x9. \<lbrakk>cap_lift C_cap = Some (Cap_frame_cap x9); cap = Cap_frame_cap x9; cap_frame_cap_CL.capFMappedASIDHigh_CL x9 = 0 \<longrightarrow> cap_frame_cap_CL.capFMappedASIDLow_CL x9 \<noteq> 0; d = to_bool (cap_frame_cap_CL.capFIsDevice_CL x9); p = cap_frame_cap_CL.capFBasePtr_CL x9; R = vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL x9); sz = framesize_to_H (capFSize_CL x9); A = Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL x9 << local.asid_low_bits) + cap_frame_cap_CL.capFMappedASIDLow_CL x9, cap_frame_cap_CL.capFMappedAddress_CL x9); cap_get_tag C_cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> cap_get_tag C_cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap