theory CSpace_C

lemma cap_lift_capEPBadge_mask_eq:
  "cap_lift cap = Some (Cap_endpoint_cap ec)
  \<Longrightarrow> capEPBadge_CL ec && mask 28 = capEPBadge_CL ec" unfolding cap_lift_def by (fastforce simp: Let_def mask_def word_bw_assocs split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_lift cap = Some (Cap_endpoint_cap ec) \<Longrightarrow> capEPBadge_CL ec && mask 28 = capEPBadge_CL ec proof (prove)
goal (1 subgoal):
 1. (let tag = cap_get_tag cap in if tag = SCAST(32 signed \<rightarrow> 32) cap_null_cap 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 cap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C cap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C cap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C cap.[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 cap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C cap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C cap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C cap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C cap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C cap.[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 cap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C cap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C cap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C cap.[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 cap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C cap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C cap.[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 cap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C cap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C cap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C cap.[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 cap.[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 cap.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C cap.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C cap.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C cap.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C cap.[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 cap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C cap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap.[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 cap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C cap.[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 cap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C cap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C cap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C cap.[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 cap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C cap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C cap.[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 cap.[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 cap.[1] >> 0, capZombieType_CL = (cap_C.words_C cap.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None) = Some (Cap_endpoint_cap ec) \<Longrightarrow> capEPBadge_CL ec && mask 28 = capEPBadge_CL ec