theory VSpace_C

lemma ccap_relation_PageCap_generics:
  "ccap_relation (ArchObjectCap (PageCap d ptr rghts sz mapdata)) cap'
    \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow>
           generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap')
                    = snd (the mapdata)
         \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap')
                    = fst (the mapdata))
      \<and> ((generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0)
                    = (mapdata = None))
      \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts
      \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz
      \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr
      \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4
      \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4
      \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d" apply (frule ccap_relation_mapped_asid_0) apply (case_tac "sz = ARMSmallPage") apply (frule(1) cap_get_tag_isCap_unfolded_H_cap) apply (clarsimp simp: cap_lift_small_frame_cap cap_to_H_def
                         generic_frame_cap_get_capFMappedAddress_CL_def
                         generic_frame_cap_get_capFVMRights_CL_def
                         generic_frame_cap_get_capFSize_CL_def
                         generic_frame_cap_get_capFMappedASID_CL_def
                         generic_frame_cap_get_capFBasePtr_CL_def
                         generic_frame_cap_get_capFIsDevice_CL_def
                  elim!: ccap_relationE) apply (simp add: gen_framesize_to_H_def) apply (simp add: vm_page_size_defs order_le_less_trans [OF word_and_le1] mask_def
             split: if_split) apply (clarsimp split: if_split_asm) apply (frule(1) cap_get_tag_isCap_unfolded_H_cap) apply (clarsimp simp: cap_lift_frame_cap cap_to_H_def
                        generic_frame_cap_get_capFMappedAddress_CL_def
                        generic_frame_cap_get_capFVMRights_CL_def
                        generic_frame_cap_get_capFSize_CL_def
                        generic_frame_cap_get_capFMappedASID_CL_def
                        generic_frame_cap_get_capFBasePtr_CL_def
                        generic_frame_cap_get_capFIsDevice_CL_def
                        c_valid_cap_def cl_valid_cap_def
                        option_to_0_def
                 elim!: ccap_relationE) apply (simp add: gen_framesize_to_H_is_framesize_to_H_if_not_ARMSmallPage) apply (simp add: vm_page_size_defs order_le_less_trans [OF word_and_le1] mask_def
            split: if_split) apply (clarsimp split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap' \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap'; (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') \<noteq> 0 \<longrightarrow> mapdata \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0 \<longrightarrow> mapdata = None)\<rbrakk> \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap'; (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') \<noteq> 0 \<longrightarrow> mapdata \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0 \<longrightarrow> mapdata = None); sz = Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d
 2. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap'; (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') \<noteq> 0 \<longrightarrow> mapdata \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0 \<longrightarrow> mapdata = None); sz \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap'; (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') \<noteq> 0 \<longrightarrow> mapdata \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0 \<longrightarrow> mapdata = None); sz = Wellformed_C.ARMSmallPage; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d
 2. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap'; (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') \<noteq> 0 \<longrightarrow> mapdata \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0 \<longrightarrow> mapdata = None); sz \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz = Wellformed_C.ARMSmallPage; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; ((cap_C.words_C cap'.[0] >> 24) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && mask 10) \<noteq> 0 \<longrightarrow> (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 \<noteq> 0; ((cap_C.words_C cap'.[0] >> 24) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && mask 10) = 0 \<longrightarrow> (if (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>)) = None; d = to_bool ((cap_C.words_C cap'.[0] >> 31) && 1); ptr = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12; rghts = vmrights_to_H ((cap_C.words_C cap'.[Suc 0] >> 20) && mask 2); mapdata = (if (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>))\<rbrakk> \<Longrightarrow> (((cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 \<noteq> 0) \<longrightarrow> (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12 = snd (the (if (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>))) \<and> ((cap_C.words_C cap'.[0] >> 24) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && mask 10) = fst (the (if (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>)))) \<and> (((cap_C.words_C cap'.[0] >> 24) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && mask 10) = 0) = ((if (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>)) = None) \<and> gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage) = Wellformed_C.ARMSmallPage \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2 < 4 \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage < 4
 2. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap'; (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') \<noteq> 0 \<longrightarrow> mapdata \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0 \<longrightarrow> mapdata = None); sz \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz = Wellformed_C.ARMSmallPage; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; ((cap_C.words_C cap'.[0] >> 24) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && mask 10) \<noteq> 0 \<longrightarrow> (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 \<noteq> 0; ((cap_C.words_C cap'.[0] >> 24) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && mask 10) = 0 \<longrightarrow> (if (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>)) = None; d = to_bool ((cap_C.words_C cap'.[0] >> 31) && 1); ptr = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12; rghts = vmrights_to_H ((cap_C.words_C cap'.[Suc 0] >> 20) && mask 2); mapdata = (if (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>))\<rbrakk> \<Longrightarrow> (((cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 \<noteq> 0) \<longrightarrow> (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12 = snd (the (if (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>))) \<and> ((cap_C.words_C cap'.[0] >> 24) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && mask 10) = fst (the (if (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>)))) \<and> (((cap_C.words_C cap'.[0] >> 24) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && mask 10) = 0) = ((if (cap_C.words_C cap'.[0] >> 24) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10 = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>)) = None) \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2 < 4 \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage < 4
 2. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap'; (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') \<noteq> 0 \<longrightarrow> mapdata \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0 \<longrightarrow> mapdata = None); sz \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz = Wellformed_C.ARMSmallPage; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; ((cap_C.words_C cap'.[0] >> 24) && 0x7F << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && 0x3FF) \<noteq> 0 \<longrightarrow> (cap_C.words_C cap'.[0] >> 24) && 0x7F = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 22) && 0x3FF \<noteq> 0; ((cap_C.words_C cap'.[0] >> 24) && 0x7F << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && 0x3FF) = 0 \<longrightarrow> (if (cap_C.words_C cap'.[0] >> 24) && 0x7F = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && 0x3FF = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>)) = None; d = to_bool ((cap_C.words_C cap'.[0] >> 31) && 1); ptr = (cap_C.words_C cap'.[0] << 8) && 0xFFFFF000; rghts = vmrights_to_H ((cap_C.words_C cap'.[Suc 0] >> 20) && 3); mapdata = (if (cap_C.words_C cap'.[0] >> 24) && 0x7F = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 22) && 0x3FF = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr> << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>, cap_small_frame_cap_CL.capFMappedAddress_CL \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 31) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 8) && ~~ mask 12\<rparr>))\<rbrakk> \<Longrightarrow> ((cap_C.words_C cap'.[0] >> 24) && 0x7F = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 22) && 0x3FF \<noteq> 0) \<longrightarrow> ((cap_C.words_C cap'.[0] >> 24) && 0x7F << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 22) && 0x3FF) \<noteq> 0
 2. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap'; (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') \<noteq> 0 \<longrightarrow> mapdata \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0 \<longrightarrow> mapdata = None); sz \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap'; (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') \<noteq> 0 \<longrightarrow> mapdata \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0 \<longrightarrow> mapdata = None); sz \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ptr rghts sz mapdata)) cap'; (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') \<noteq> 0 \<longrightarrow> mapdata \<noteq> None) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0 \<longrightarrow> mapdata = None); sz \<noteq> Wellformed_C.ARMSmallPage; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') = snd (the mapdata) \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = fst (the mapdata)) \<and> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) = (mapdata = None) \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2 \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage; ((cap_C.words_C cap'.[0] >> 22) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && mask 10) \<noteq> 0 \<longrightarrow> (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 \<noteq> 0; ((cap_C.words_C cap'.[0] >> 22) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && mask 10) = 0 \<longrightarrow> (if (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>)) = None; d = to_bool ((cap_C.words_C cap'.[0] >> 29) && 1); ptr = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14; rghts = vmrights_to_H ((cap_C.words_C cap'.[Suc 0] >> 18) && mask 2); sz = framesize_to_H ((cap_C.words_C cap'.[Suc 0] >> 30) && mask 2); mapdata = (if (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>))\<rbrakk> \<Longrightarrow> (((cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 \<noteq> 0) \<longrightarrow> (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14 = snd (the (if (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>))) \<and> ((cap_C.words_C cap'.[0] >> 22) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && mask 10) = fst (the (if (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>)))) \<and> (((cap_C.words_C cap'.[0] >> 22) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && mask 10) = 0) = ((if (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>)) = None) \<and> gen_framesize_to_H ((cap_C.words_C cap'.[Suc 0] >> 30) && mask 2) = framesize_to_H ((cap_C.words_C cap'.[Suc 0] >> 30) && mask 2) \<and> (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2 < 4 \<and> (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2 < 4 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2 \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage; ((cap_C.words_C cap'.[0] >> 22) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && mask 10) \<noteq> 0 \<longrightarrow> (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 \<noteq> 0; ((cap_C.words_C cap'.[0] >> 22) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && mask 10) = 0 \<longrightarrow> (if (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>)) = None; d = to_bool ((cap_C.words_C cap'.[0] >> 29) && 1); ptr = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14; rghts = vmrights_to_H ((cap_C.words_C cap'.[Suc 0] >> 18) && mask 2); sz = framesize_to_H ((cap_C.words_C cap'.[Suc 0] >> 30) && mask 2); mapdata = (if (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>))\<rbrakk> \<Longrightarrow> (((cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 \<noteq> 0) \<longrightarrow> (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14 = snd (the (if (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>))) \<and> ((cap_C.words_C cap'.[0] >> 22) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && mask 10) = fst (the (if (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>)))) \<and> (((cap_C.words_C cap'.[0] >> 22) && mask 7 << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && mask 10) = 0) = ((if (cap_C.words_C cap'.[0] >> 22) && mask 7 = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10 = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>)) = None) \<and> (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2 < 4 \<and> (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2 < 4 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; (cap_C.words_C cap'.[Suc 0] >> 30) && 3 \<noteq> 0; ((cap_C.words_C cap'.[0] >> 22) && 0x7F << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && 0x3FF) \<noteq> 0 \<longrightarrow> (cap_C.words_C cap'.[0] >> 22) && 0x7F = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 20) && 0x3FF \<noteq> 0; ((cap_C.words_C cap'.[0] >> 22) && 0x7F << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && 0x3FF) = 0 \<longrightarrow> (if (cap_C.words_C cap'.[0] >> 22) && 0x7F = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && 0x3FF = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>)) = None; d = to_bool ((cap_C.words_C cap'.[0] >> 29) && 1); ptr = (cap_C.words_C cap'.[0] << 10) && 0xFFFFC000; rghts = vmrights_to_H ((cap_C.words_C cap'.[Suc 0] >> 18) && 3); sz = framesize_to_H ((cap_C.words_C cap'.[Suc 0] >> 30) && 3); mapdata = (if (cap_C.words_C cap'.[0] >> 22) && 0x7F = 0 \<and> (cap_C.words_C cap'.[Suc 0] >> 20) && 0x3FF = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr> << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>, cap_frame_cap_CL.capFMappedAddress_CL \<lparr>capFSize_CL = (cap_C.words_C cap'.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap'.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap'.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap'.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap'.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C cap'.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap'.[0] << 10) && ~~ mask 14\<rparr>))\<rbrakk> \<Longrightarrow> ((cap_C.words_C cap'.[0] >> 22) && 0x7F = 0 \<longrightarrow> (cap_C.words_C cap'.[Suc 0] >> 20) && 0x3FF \<noteq> 0) \<longrightarrow> ((cap_C.words_C cap'.[0] >> 22) && 0x7F << local.asid_low_bits) + ((cap_C.words_C cap'.[Suc 0] >> 20) && 0x3FF) \<noteq> 0 proof (prove)
goal:
No subgoals!