theory CSpace_C

lemma cap_get_tag_PageCap_small_frame:
  "ccap_relation cap cap' \<Longrightarrow>
   (cap_get_tag cap' = scast cap_small_frame_cap) =
   (cap =
    capability.ArchObjectCap
     (PageCap (to_bool ((cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap')))) (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap'))
              (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap')))
              vmpage_size.ARMSmallPage
   (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') = 0
        \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap') = 0
    then None else
     Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') << asid_low_bits) +
          cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap'),
          cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift cap')))))" apply (rule iffI) apply (erule ccap_relationE) apply (clarsimp simp add: cap_lifts cap_to_H_def Let_def split: if_split) apply (simp add: cap_get_tag_isCap isCap_simps pageSize_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (cap = capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap'))) (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap')) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap'))) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap') = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') << local.asid_low_bits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap'), cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift cap'))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap'))) (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap')) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap'))) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap') = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') << local.asid_low_bits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap'), cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift cap'))))
 2. \<lbrakk>ccap_relation cap cap'; cap = capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap'))) (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap')) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap'))) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap') = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') << local.asid_low_bits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap'), cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift cap'))))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; cap_lift cap' = Some vl; cap = cap_to_H vl; c_valid_cap cap'\<rbrakk> \<Longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap'))) (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap')) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap'))) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap') = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') << local.asid_low_bits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap'), cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift cap'))))
 2. \<lbrakk>ccap_relation cap cap'; cap = capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap'))) (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap')) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap'))) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap') = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') << local.asid_low_bits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap'), cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift cap'))))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap = capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL (cap_small_frame_cap_lift cap'))) (cap_small_frame_cap_CL.capFBasePtr_CL (cap_small_frame_cap_lift cap')) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap'))) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap') = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift cap') << local.asid_low_bits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift cap'), cap_small_frame_cap_CL.capFMappedAddress_CL (cap_small_frame_cap_lift cap'))))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap proof (prove)
goal:
No subgoals!