theory CSpace_C

lemma get_capSizeBits_valid_shift:
  "\<lbrakk> ccap_relation hcap ccap; capAligned hcap \<rbrakk> \<Longrightarrow>
   get_capSizeBits_CL (cap_lift ccap) < 32" unfolding get_capSizeBits_CL_def apply (cases hcap;
         simp add: cap_get_tag_isCap_unfolded_H_cap cap_lift_def cap_tag_defs) 
     (* zombie *)
      apply (clarsimp simp: Let_def split: if_split) apply (frule cap_get_tag_isCap_unfolded_H_cap) apply (clarsimp simp: ccap_relation_def map_option_Some_eq2
                           cap_lift_zombie_cap cap_to_H_def
                           Let_def capAligned_def objBits_simps'
                           word_bits_conv) apply (subst less_mask_eq, simp add: word_less_nat_alt, assumption) 
    (* arch *)
     apply (rename_tac arch_capability) apply (case_tac arch_capability,
           simp_all add: cap_get_tag_isCap_unfolded_H_cap cap_lift_def
                         cap_tag_defs asid_low_bits_def) apply (rename_tac vmpage_size option) apply (case_tac vmpage_size,
           simp_all add: cap_get_tag_isCap_unfolded_H_cap cap_lift_def
                         cap_tag_defs pageBitsForSize_def) apply (clarsimp split: vmpage_size.split)+ 
   (* untyped *)
    apply (frule cap_get_tag_isCap_unfolded_H_cap) apply (clarsimp simp: cap_lift_def cap_tag_defs mask_def) apply (subgoal_tac "index (cap_C.words_C ccap) 1 && 0x1F \<le> 0x1F") apply (simp add: unat_arith_simps) apply (simp add: word_and_le1) 
  (* cnode *)
   apply (frule cap_get_tag_isCap_unfolded_H_cap) apply (clarsimp simp: ccap_relation_def map_option_Some_eq2
                        cap_lift_cnode_cap cap_to_H_def
                        Let_def capAligned_def objBits_simps'
                        word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation hcap ccap; capAligned hcap\<rbrakk> \<Longrightarrow> get_capSizeBits_CL (cap_lift ccap) < 32 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation hcap ccap; capAligned hcap\<rbrakk> \<Longrightarrow> (case cap_lift ccap of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32 proof (prove)
goal (4 subgoals):
 1. \<And>x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) ccap; capAligned (capability.Zombie x71 x72 x73); hcap = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (let type = (cap_C.words_C ccap.[0] >> 8) && mask 6 in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4) < 32
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (case let tag = cap_get_tag ccap in if tag = 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C ccap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C ccap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C ccap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C ccap.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_notification_cap then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C ccap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C ccap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C ccap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C ccap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C ccap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_frame_cap then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C ccap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C ccap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C ccap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C ccap.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C ccap.[1] >> 0, capZombieType_CL = (cap_C.words_C ccap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32
 3. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 4. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (4 subgoals):
 1. \<And>x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) ccap; capAligned (capability.Zombie x71 x72 x73); hcap = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (let type = (cap_C.words_C ccap.[0] >> 8) && mask 6 in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4) < 32
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (case let tag = cap_get_tag ccap in if tag = 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C ccap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C ccap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C ccap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C ccap.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_notification_cap then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C ccap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C ccap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C ccap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C ccap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C ccap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_frame_cap then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C ccap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C ccap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C ccap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C ccap.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C ccap.[1] >> 0, capZombieType_CL = (cap_C.words_C ccap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32
 3. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 4. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (4 subgoals):
 1. \<And>x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) ccap; capAligned (capability.Zombie x71 x72 x73); hcap = capability.Zombie x71 x72 x73; \<not> isZombieTCB_C ((cap_C.words_C ccap.[0] >> 8) && mask 6)\<rbrakk> \<Longrightarrow> unat (((cap_C.words_C ccap.[0] >> 8) && mask 6) && mask 5) < 28
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (case let tag = cap_get_tag ccap in if tag = 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C ccap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C ccap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C ccap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C ccap.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_notification_cap then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C ccap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C ccap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C ccap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C ccap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C ccap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_frame_cap then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C ccap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C ccap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C ccap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C ccap.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C ccap.[1] >> 0, capZombieType_CL = (cap_C.words_C ccap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32
 3. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 4. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (4 subgoals):
 1. \<And>x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) ccap; capAligned (capability.Zombie x71 x72 x73); hcap = capability.Zombie x71 x72 x73; \<not> isZombieTCB_C ((cap_C.words_C ccap.[0] >> 8) && mask 6); cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrakk> \<Longrightarrow> unat (((cap_C.words_C ccap.[0] >> 8) && mask 6) && mask 5) < 28
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (case let tag = cap_get_tag ccap in if tag = 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C ccap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C ccap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C ccap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C ccap.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_notification_cap then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C ccap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C ccap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C ccap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C ccap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C ccap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_frame_cap then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C ccap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C ccap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C ccap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C ccap.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C ccap.[1] >> 0, capZombieType_CL = (cap_C.words_C ccap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32
 3. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 4. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>hcap = capability.Zombie (cap_C.words_C ccap.[Suc 0] && ~~ mask (Suc (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6)))) (ZombieCNode (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6))) (unat (cap_C.words_C ccap.[Suc 0] && mask (Suc (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6))))); \<not> isZombieTCB_C ((cap_C.words_C ccap.[0] >> 8) && mask 6); cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; is_aligned (cap_C.words_C ccap.[Suc 0] && ~~ mask (Suc (unat ((cap_C.words_C ccap.[0] >> 8) && mask 6)))) (4 + unat ((cap_C.words_C ccap.[0] >> 8) && mask 6)); unat ((cap_C.words_C ccap.[0] >> 8) && mask 6) < 28\<rbrakk> \<Longrightarrow> unat (((cap_C.words_C ccap.[0] >> 8) && mask 6) && mask 5) < 28
 2. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (case let tag = cap_get_tag ccap in if tag = 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C ccap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C ccap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C ccap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C ccap.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_notification_cap then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C ccap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C ccap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C ccap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C ccap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C ccap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_frame_cap then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C ccap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C ccap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C ccap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C ccap.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C ccap.[1] >> 0, capZombieType_CL = (cap_C.words_C ccap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32
 3. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 4. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (3 subgoals):
 1. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (case let tag = cap_get_tag ccap in if tag = 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C ccap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C ccap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C ccap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C ccap.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_notification_cap then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C ccap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C ccap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C ccap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C ccap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C ccap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_frame_cap then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C ccap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C ccap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C ccap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C ccap.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C ccap.[1] >> 0, capZombieType_CL = (cap_C.words_C ccap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32
 2. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 3. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (3 subgoals):
 1. \<And>x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) ccap; capAligned (capability.ArchObjectCap x8); hcap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (case let tag = cap_get_tag ccap in if tag = 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C ccap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C ccap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C ccap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C ccap.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_notification_cap then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C ccap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C ccap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C ccap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C ccap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C ccap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_frame_cap then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C ccap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C ccap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C ccap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C ccap.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C ccap.[1] >> 0, capZombieType_CL = (cap_C.words_C ccap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32
 2. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 3. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (3 subgoals):
 1. \<And>arch_capability. \<lbrakk>ccap_relation (capability.ArchObjectCap arch_capability) ccap; capAligned (capability.ArchObjectCap arch_capability); hcap = capability.ArchObjectCap arch_capability\<rbrakk> \<Longrightarrow> (case let tag = cap_get_tag ccap in if tag = 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C ccap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C ccap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C ccap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C ccap.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_notification_cap then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C ccap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C ccap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C ccap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C ccap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C ccap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_frame_cap then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C ccap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C ccap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C ccap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C ccap.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C ccap.[1] >> 0, capZombieType_CL = (cap_C.words_C ccap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32
 2. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 3. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (3 subgoals):
 1. \<And>arch_capability x31 x32 x33 x34 x35. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (case let tag = cap_get_tag ccap in if tag = 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C ccap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C ccap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C ccap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C ccap.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_notification_cap then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C ccap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C ccap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C ccap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C ccap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C ccap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_frame_cap then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C ccap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C ccap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C ccap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C ccap.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C ccap.[1] >> 0, capZombieType_CL = (cap_C.words_C ccap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32
 2. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 3. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (3 subgoals):
 1. \<And>arch_capability x31 x32 x33 vmpage_size option. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 vmpage_size option); arch_capability = arch_capability.PageCap x31 x32 x33 vmpage_size option\<rbrakk> \<Longrightarrow> (case let tag = cap_get_tag ccap in if tag = 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C ccap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C ccap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C ccap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C ccap.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_notification_cap then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C ccap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C ccap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C ccap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C ccap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C ccap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C ccap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C ccap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_frame_cap then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C ccap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C ccap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C ccap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C ccap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C ccap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C ccap.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C ccap.[1] >> 0, capZombieType_CL = (cap_C.words_C ccap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of None \<Rightarrow> 0 | Some (Cap_untyped_cap c) \<Rightarrow> unat (capBlockSize_CL c) | Some (Cap_endpoint_cap c) \<Rightarrow> 4 | Some (Cap_notification_cap c) \<Rightarrow> 4 | Some (Cap_cnode_cap c) \<Rightarrow> unat (capCNodeRadix_CL c) + 4 | Some (Cap_thread_cap c) \<Rightarrow> 9 | Some (Cap_small_frame_cap c) \<Rightarrow> 12 | Some (Cap_frame_cap c) \<Rightarrow> pageBitsForSize (gen_framesize_to_H $ generic_frame_cap_get_capFSize_CL (cap_lift ccap)) | Some (Cap_asid_pool_cap c) \<Rightarrow> local.asidLowBits + 2 | Some (Cap_page_table_cap c) \<Rightarrow> 10 | Some (Cap_page_directory_cap c) \<Rightarrow> 14 | Some (Cap_zombie_cap c) \<Rightarrow> let type = capZombieType_CL c in if isZombieTCB_C type then 9 else unat (type && mask 5) + 4 | Some _ \<Rightarrow> 0) < 32
 2. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 3. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (5 subgoals):
 1. \<And>arch_capability x31 x32 x33 vmpage_size option. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMLargePage option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMLargePage option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMLargePage option); arch_capability = arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMLargePage option; vmpage_size = Wellformed_C.ARMLargePage\<rbrakk> \<Longrightarrow> (case gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>))) of local.ARMSmallPage \<Rightarrow> 12 | local.ARMLargePage \<Rightarrow> 16 | local.ARMSection \<Rightarrow> 20 | local.ARMSuperSection \<Rightarrow> 24) < 32
 2. \<And>arch_capability x31 x32 x33 vmpage_size option. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSection option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSection option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSection option); arch_capability = arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSection option; vmpage_size = Wellformed_C.ARMSection\<rbrakk> \<Longrightarrow> (case gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>))) of local.ARMSmallPage \<Rightarrow> 12 | local.ARMLargePage \<Rightarrow> 16 | local.ARMSection \<Rightarrow> 20 | local.ARMSuperSection \<Rightarrow> 24) < 32
 3. \<And>arch_capability x31 x32 x33 vmpage_size option. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSuperSection option)) ccap; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSuperSection option)); hcap = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSuperSection option); arch_capability = arch_capability.PageCap x31 x32 x33 Wellformed_C.ARMSuperSection option; vmpage_size = Wellformed_C.ARMSuperSection\<rbrakk> \<Longrightarrow> (case gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C ccap.[Suc 0] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C ccap.[Suc 0] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C ccap.[Suc 0] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C ccap.[Suc 0] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C ccap.[0] >> 29) && 1, capFMappedASIDHigh_CL = (cap_C.words_C ccap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C ccap.[0] << 10) && ~~ mask 14\<rparr>))) of local.ARMSmallPage \<Rightarrow> 12 | local.ARMLargePage \<Rightarrow> 16 | local.ARMSection \<Rightarrow> 20 | local.ARMSuperSection \<Rightarrow> 24) < 32
 4. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 5. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (2 subgoals):
 1. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 2. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (2 subgoals):
 1. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 2. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (2 subgoals):
 1. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && mask 5) < 32
 2. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (2 subgoals):
 1. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104; cap_get_tag ccap = 2\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && 0x1F) < 32
 2. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (3 subgoals):
 1. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104; cap_get_tag ccap = 2; cap_C.words_C ccap.[1] && 0x1F \<le> 0x1F\<rbrakk> \<Longrightarrow> unat (cap_C.words_C ccap.[Suc 0] && 0x1F) < 32
 2. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104; cap_get_tag ccap = 2\<rbrakk> \<Longrightarrow> cap_C.words_C ccap.[1] && 0x1F \<le> 0x1F
 3. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (2 subgoals):
 1. \<And>x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) ccap; capAligned (capability.UntypedCap x101 x102 x103 x104); hcap = capability.UntypedCap x101 x102 x103 x104; cap_get_tag ccap = 2\<rbrakk> \<Longrightarrow> cap_C.words_C ccap.[1] && 0x1F \<le> 0x1F
 2. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (1 subgoal):
 1. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (1 subgoal):
 1. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal (1 subgoal):
 1. \<And>x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) ccap; capAligned (capability.CNodeCap x111 x112 x113 x114); hcap = capability.CNodeCap x111 x112 x113 x114; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap\<rbrakk> \<Longrightarrow> unat ((cap_C.words_C ccap.[Suc 0] >> 18) && mask 5) < 28 proof (prove)
goal:
No subgoals!