theory CSpace_C

lemma cap_get_capSizeBits_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned_long :== PROC cap_get_capSizeBits(\<acute>cap)
       \<lbrace>\<acute>ret__unsigned_long = of_nat (get_capSizeBits_CL (cap_lift \<^bsup>s\<^esup>cap))\<rbrace>" apply vcg apply (clarsimp simp: get_capSizeBits_CL_def) apply (intro conjI impI) apply (clarsimp simp: cap_lifts gen_framesize_to_H_def
                                              generic_frame_cap_get_capFSize_CL_def
                                              cap_lift_asid_control_cap
                                              cap_lift_irq_control_cap cap_lift_null_cap
                                              Kernel_C.asidLowBits_def asid_low_bits_def
                                              word_sle_def Let_def mask_def
                                              isZombieTCB_C_def ZombieTCB_C_def
                                              cap_lift_domain_cap
                                       dest!: sym [where t = "cap_get_tag cap" for cap])+ 
  (* slow *)
   by (case_tac "cap_lift cap", simp_all, case_tac "a",
               auto simp: cap_lift_def cap_tag_defs Let_def
                  cap_small_frame_cap_lift_def cap_frame_cap_lift_def
                  cap_endpoint_cap_lift_def cap_notification_cap_lift_def
                  cap_cnode_cap_lift_def cap_thread_cap_lift_def
                  cap_zombie_cap_lift_def cap_page_table_cap_lift_def
                  cap_page_directory_cap_lift_def cap_asid_pool_cap_lift_def
                  Let_def cap_untyped_cap_lift_def  split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call cap_get_capSizeBits_'proc \<lbrace>\<acute>ret__unsigned_long = word_of_nat (get_capSizeBits_CL (cap_lift \<^bsup>s\<^esup>cap))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<forall>ret__unsigned. ret__unsigned = cap_get_tag cap \<longrightarrow> (cap_untyped_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capBlockSize_CL (cap_untyped_cap_lift cap) \<longrightarrow> UCAST(32 \<rightarrow> 32) (capBlockSize_CL (cap_untyped_cap_lift cap)) = word_of_nat (get_capSizeBits_CL (cap_lift cap)))) \<and> (cap_untyped_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_endpoint_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 4 = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_endpoint_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_notification_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 4 = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_notification_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_cnode_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capCNodeRadix_CL (cap_cnode_cap_lift cap) \<longrightarrow> UCAST(32 \<rightarrow> 32) (capCNodeRadix_CL (cap_cnode_cap_lift cap) + SCAST(32 signed \<rightarrow> 32) 4) = word_of_nat (get_capSizeBits_CL (cap_lift cap)))) \<and> (cap_cnode_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_thread_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 9 = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_thread_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_zombie_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capZombieType_CL (cap_zombie_cap_lift cap) \<longrightarrow> 0 \<le>s 5 \<and> 5 <s 0x20 \<and> (UCAST(32 \<rightarrow> 32) (capZombieType_CL (cap_zombie_cap_lift cap)) = 1 << unat 5 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 9 = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (UCAST(32 \<rightarrow> 32) (capZombieType_CL (cap_zombie_cap_lift cap)) \<noteq> 1 << unat 5 \<longrightarrow> 0 \<le>s 5 \<and> 5 <s 0x20 \<and> (UCAST(32 \<rightarrow> 32) (capZombieType_CL (cap_zombie_cap_lift cap)) && (1 << unat 5) - 1) + SCAST(32 signed \<rightarrow> 32) 4 = word_of_nat (get_capSizeBits_CL (cap_lift cap))))) \<and> (cap_zombie_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_null_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_null_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_domain_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_domain_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_reply_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_reply_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_irq_control_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_irq_control_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_irq_handler_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_irq_handler_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap \<longrightarrow> (UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<in> insert cap_frame_cap (Collect ((=) cap_small_frame_cap)) \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = generic_frame_cap_get_capFSize_CL (cap_lift cap) \<longrightarrow> generic_frame_cap_get_capFSize_CL (cap_lift cap) && mask 2 = generic_frame_cap_get_capFSize_CL (cap_lift cap) \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = word_of_nat (pageBitsForSize (gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap)))) \<longrightarrow> word_of_nat (pageBitsForSize (gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap)))) = word_of_nat (get_capSizeBits_CL (cap_lift cap))))) \<and> (UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<notin> insert cap_frame_cap (Collect ((=) cap_small_frame_cap)) \<longrightarrow> (cap_page_table_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0xA = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_page_table_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_page_directory_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0xE = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_page_directory_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_asid_pool_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0xC = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_asid_pool_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_asid_control_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = word_of_nat (get_capSizeBits_CL (cap_lift cap))) \<and> (cap_asid_control_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = word_of_nat (get_capSizeBits_CL (cap_lift cap))))))))))))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>cap. (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> capBlockSize_CL (cap_untyped_cap_lift cap) = word_of_nat (case cap_lift cap 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 cap)) | 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)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 4) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 4) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<longrightarrow> capCNodeRadix_CL (cap_cnode_cap_lift cap) + 4 = word_of_nat (case cap_lift cap 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 cap)) | 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)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 9) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> (capZombieType_CL (cap_zombie_cap_lift cap) = 0x20 \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 9) \<and> (capZombieType_CL (cap_zombie_cap_lift cap) \<noteq> 0x20 \<longrightarrow> (capZombieType_CL (cap_zombie_cap_lift cap) && 0x1F) + 4 = word_of_nat (case cap_lift cap 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 cap)) | 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))) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_domain_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_domain_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> word_of_nat (pageBitsForSize (gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap)))) = word_of_nat (case cap_lift cap 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 cap)) | 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)) \<and> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> word_of_nat (pageBitsForSize (gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap)))) = word_of_nat (case cap_lift cap 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 cap)) | 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)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0xA) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_page_table_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0xE) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0xC) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap \<longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0))))))))))))))) proof (prove)
goal (18 subgoals):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<Longrightarrow> capBlockSize_CL (cap_untyped_cap_lift cap) = word_of_nat (case cap_lift cap 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 cap)) | 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)
 2. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap\<rbrakk> \<Longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 4
 3. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_notification_cap\<rbrakk> \<Longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 4
 4. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap\<rbrakk> \<Longrightarrow> capCNodeRadix_CL (cap_cnode_cap_lift cap) + 4 = word_of_nat (case cap_lift cap 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 cap)) | 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)
 5. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap\<rbrakk> \<Longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 9
 6. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; capZombieType_CL (cap_zombie_cap_lift cap) = 0x20\<rbrakk> \<Longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 9
 7. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; capZombieType_CL (cap_zombie_cap_lift cap) \<noteq> 0x20\<rbrakk> \<Longrightarrow> (capZombieType_CL (cap_zombie_cap_lift cap) && 0x1F) + 4 = word_of_nat (case cap_lift cap 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 cap)) | 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)
 8. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0
 9. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_domain_cap\<rbrakk> \<Longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0
 10. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_domain_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_reply_cap\<rbrakk> \<Longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0
A total of 18 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_lift cap \<noteq> Some (Cap_untyped_cap (cap_untyped_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_endpoint_cap (cap_endpoint_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_notification_cap (cap_notification_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_cnode_cap (cap_cnode_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_thread_cap (cap_thread_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_zombie_cap (cap_zombie_cap_lift cap)); cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_domain_cap; cap_lift cap \<noteq> Some (Cap_reply_cap (cap_reply_cap_lift cap)); cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap; cap_lift cap \<noteq> Some (Cap_irq_handler_cap (cap_irq_handler_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_page_table_cap (cap_page_table_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_page_directory_cap (cap_page_directory_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_asid_pool_cap (cap_asid_pool_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_frame_cap (cap_frame_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_small_frame_cap (cap_small_frame_cap_lift cap))\<rbrakk> \<Longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0 proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_lift cap \<noteq> Some (Cap_untyped_cap (cap_untyped_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_endpoint_cap (cap_endpoint_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_notification_cap (cap_notification_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_cnode_cap (cap_cnode_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_thread_cap (cap_thread_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_zombie_cap (cap_zombie_cap_lift cap)); cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_domain_cap; cap_lift cap \<noteq> Some (Cap_reply_cap (cap_reply_cap_lift cap)); cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap; cap_lift cap \<noteq> Some (Cap_irq_handler_cap (cap_irq_handler_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_page_table_cap (cap_page_table_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_page_directory_cap (cap_page_directory_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_asid_pool_cap (cap_asid_pool_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_frame_cap (cap_frame_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_small_frame_cap (cap_small_frame_cap_lift cap))\<rbrakk> \<Longrightarrow> word_of_nat (case cap_lift cap 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 cap)) | 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) = 0