theory CSpace_C

lemma cap_get_capPtr_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. (cap_get_tag \<acute>cap = scast cap_zombie_cap
                   \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift \<acute>cap) < 0x1F)\<rbrace>
       \<acute>ret__ptr_to_void :== PROC cap_get_capPtr(\<acute>cap)
       \<lbrace>\<acute>ret__ptr_to_void = get_capPtr_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" apply vcg apply (clarsimp simp: get_capPtr_CL_def generic_frame_cap_get_capFBasePtr_CL_def) apply (intro impI conjI) apply (clarsimp simp: cap_lifts pageBitsForSize_def
                                          cap_lift_asid_control_cap word_sle_def
                                          cap_lift_irq_control_cap cap_lift_null_cap
                                          mask_def objBits_simps' cap_lift_domain_cap
                                          ptr_add_assertion_positive
                                   dest!: sym [where t = "cap_get_tag cap" for cap]
                                   split: vmpage_size.splits)+ 
  (* XXX: slow. there should be a rule for this *)
   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> \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift \<acute>cap) < 0x1F\<rbrace> Call cap_get_capPtr_'proc \<lbrace>\<acute>ret__ptr_to_void = get_capPtr_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F \<Longrightarrow> \<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 = capPtr_CL (cap_untyped_cap_lift cap) \<longrightarrow> PTR_COERCE(32 word \<rightarrow> unit) (PTR(32 word) (UCAST(32 \<rightarrow> 32) (capPtr_CL (cap_untyped_cap_lift cap)))) = get_capPtr_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> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capEPPtr_CL (cap_endpoint_cap_lift cap) \<longrightarrow> PTR_COERCE(endpoint_C \<rightarrow> unit) (ep_Ptr (UCAST(32 \<rightarrow> 32) (capEPPtr_CL (cap_endpoint_cap_lift cap)))) = get_capPtr_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> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capNtfnPtr_CL (cap_notification_cap_lift cap) \<longrightarrow> PTR_COERCE(notification_C \<rightarrow> unit) (ntfn_Ptr (UCAST(32 \<rightarrow> 32) (capNtfnPtr_CL (cap_notification_cap_lift cap)))) = get_capPtr_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 = capCNodePtr_CL (cap_cnode_cap_lift cap) \<longrightarrow> PTR_COERCE(cte_C \<rightarrow> unit) (cte_Ptr (UCAST(32 \<rightarrow> 32) (capCNodePtr_CL (cap_cnode_cap_lift cap)))) = get_capPtr_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> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap \<and> (\<forall>ret__unsigned. ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap) \<longrightarrow> 0 \<le>s 9 \<and> 9 <s 0x20 \<and> ptr_add_assertion' (cte_Ptr (UCAST(32 \<rightarrow> 32) (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) && ~~ ((1 << unat 9) - 1))) (sint 0) False (hrs_htd t_hrs) \<and> PTR_COERCE(cte_C \<rightarrow> unit) (cte_Ptr (UCAST(32 \<rightarrow> 32) (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) && ~~ ((1 << unat 9) - 1)) +\<^sub>p sint 0) = get_capPtr_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> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = get_capZombiePtr_CL (cap_zombie_cap_lift cap) \<longrightarrow> PTR_COERCE(cte_C \<rightarrow> unit) (cte_Ptr (get_capZombiePtr_CL (cap_zombie_cap_lift cap))) = get_capPtr_CL (cap_lift cap))) \<and> (cap_zombie_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> PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0) = get_capPtr_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> PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0) = get_capPtr_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> PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0) = get_capPtr_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> PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0) = get_capPtr_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_capFBasePtr_CL (cap_lift cap) \<longrightarrow> PTR(unit) (generic_frame_cap_get_capFBasePtr_CL (cap_lift cap)) = get_capPtr_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> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capPTBasePtr_CL (cap_page_table_cap_lift cap) \<longrightarrow> PTR_COERCE(pte_C \<rightarrow> unit) (pte_Ptr (UCAST(32 \<rightarrow> 32) (capPTBasePtr_CL (cap_page_table_cap_lift cap)))) = get_capPtr_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> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capPDBasePtr_CL (cap_page_directory_cap_lift cap) \<longrightarrow> PTR_COERCE(pde_C \<rightarrow> unit) (pde_Ptr (UCAST(32 \<rightarrow> 32) (capPDBasePtr_CL (cap_page_directory_cap_lift cap)))) = get_capPtr_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> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capASIDPool_CL (cap_asid_pool_cap_lift cap) \<longrightarrow> PTR_COERCE(asid_pool_C \<rightarrow> unit) (ap_Ptr (UCAST(32 \<rightarrow> 32) (capASIDPool_CL (cap_asid_pool_cap_lift cap)))) = get_capPtr_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> PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0) = get_capPtr_CL (cap_lift cap)) \<and> (cap_asid_control_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0) = get_capPtr_CL (cap_lift cap))))))))))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F \<Longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> capPtr_CL (cap_untyped_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | 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> capEPPtr_CL (cap_endpoint_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)) \<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> capNtfnPtr_CL (cap_notification_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)) \<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> capCNodePtr_CL (cap_cnode_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | 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> ptr_add_assertion (cte_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap) && 0xFFFFFE00)) 0 False (hrs_htd (a, b)) \<and> cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap) && 0xFFFFFE00 = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)) \<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> get_capZombiePtr_CL (cap_zombie_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | 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_domain_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | 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> (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | 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> (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | 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> (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | 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> (case cap_lift cap of Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some _ \<Rightarrow> 0) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)) \<and> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (case cap_lift cap of Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some _ \<Rightarrow> 0) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | 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> capPTBasePtr_CL (cap_page_table_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)) \<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> capPDBasePtr_CL (cap_page_directory_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)) \<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> capASIDPool_CL (cap_asid_pool_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0) = 0)))))))))))))) proof (prove)
goal (17 subgoals):
 1. \<And>a b cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrakk> \<Longrightarrow> capPtr_CL (cap_untyped_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)
 2. \<And>a b cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F; 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> capEPPtr_CL (cap_endpoint_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)
 3. \<And>a b cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F; 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> capNtfnPtr_CL (cap_notification_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)
 4. \<And>a b cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F; 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> capCNodePtr_CL (cap_cnode_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)
 5. \<And>a b cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F; 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> ptr_add_assertion (cte_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap) && 0xFFFFFE00)) 0 False (hrs_htd (a, b))
 6. \<And>a b cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F; 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> cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap) && 0xFFFFFE00 = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)
 7. \<And>a b cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F; 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\<rbrakk> \<Longrightarrow> get_capZombiePtr_CL (cap_zombie_cap_lift cap) = (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0)
 8. \<And>a b cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F; 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_domain_cap\<rbrakk> \<Longrightarrow> (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0) = 0
 9. \<And>a b cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F; 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_domain_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_reply_cap\<rbrakk> \<Longrightarrow> (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0) = 0
 10. \<And>a b cap. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F; 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_domain_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_reply_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap\<rbrakk> \<Longrightarrow> (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0) = 0
A total of 17 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_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> (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | 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_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> (case cap_lift cap of None \<Rightarrow> 0 | Some (Cap_untyped_cap xa) \<Rightarrow> capPtr_CL xa | Some (Cap_endpoint_cap xa) \<Rightarrow> capEPPtr_CL xa | Some (Cap_notification_cap xa) \<Rightarrow> capNtfnPtr_CL xa | Some (Cap_cnode_cap xa) \<Rightarrow> capCNodePtr_CL xa | Some (Cap_thread_cap c) \<Rightarrow> cap_thread_cap_CL.capTCBPtr_CL c && ~~ mask (objBits undefined) | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFBasePtr_CL xa | Some (Cap_asid_pool_cap xa) \<Rightarrow> capASIDPool_CL xa | Some (Cap_page_table_cap xa) \<Rightarrow> capPTBasePtr_CL xa | Some (Cap_page_directory_cap xa) \<Rightarrow> capPDBasePtr_CL xa | Some (Cap_zombie_cap xa) \<Rightarrow> get_capZombiePtr_CL xa | Some _ \<Rightarrow> 0) = 0