theory Wellformed_C

lemma  c_valid_cap_simps [simp]:
  "cap_get_tag c = scast cap_small_frame_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_thread_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_notification_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_endpoint_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_cnode_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_page_directory_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_asid_control_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_irq_control_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_page_table_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_asid_pool_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_untyped_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_zombie_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_reply_cap \<Longrightarrow> c_valid_cap c"
  "cap_get_tag c = scast cap_null_cap \<Longrightarrow> c_valid_cap c" unfolding c_valid_cap_def  cap_lift_def cap_tag_defs by (simp add: cl_valid_cap_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> c_valid_cap c) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_thread_cap \<Longrightarrow> c_valid_cap c) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<Longrightarrow> c_valid_cap c)) &&& ((cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<Longrightarrow> c_valid_cap c) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<Longrightarrow> c_valid_cap c)) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<Longrightarrow> c_valid_cap c) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap \<Longrightarrow> c_valid_cap c)) &&& ((cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap \<Longrightarrow> c_valid_cap c) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap \<Longrightarrow> c_valid_cap c) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap \<Longrightarrow> c_valid_cap c)) &&& ((cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<Longrightarrow> c_valid_cap c) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<Longrightarrow> c_valid_cap c)) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<Longrightarrow> c_valid_cap c) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<Longrightarrow> c_valid_cap c) proof (prove)
goal (1 subgoal):
 1. (((cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 1 \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 0xC \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 6 \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x)) &&& ((cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 4 \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 0xA \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x)) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 9 \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 0xB \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x)) &&& ((cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 0xE \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 7 \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 5 \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x)) &&& ((cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 2 \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 0x2E \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x)) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 8 \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x) &&& (cap_get_tag c = SCAST(32 signed \<rightarrow> 32) 0 \<Longrightarrow> case let tag = cap_get_tag c in if tag = SCAST(32 signed \<rightarrow> 32) 0 then Some Cap_null_cap else if tag = SCAST(32 signed \<rightarrow> 32) 2 then Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C c.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C c.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C c.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 4 then Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C c.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C c.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C c.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C c.[1] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 6 then Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C c.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C c.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C c.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 8 then Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C c.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xA then Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C c.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C c.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C c.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 5\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xC then Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 1 then Some (Cap_small_frame_cap \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 22) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 20) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 12) && ~~ mask 12, capFIsDevice_CL = (cap_C.words_C c.[0] >> 31) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 24) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 8) && ~~ mask 12\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 3 then Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C c.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C c.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C c.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C c.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C c.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C c.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C c.[0] << 10) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 5 then Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 4\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 7 then Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C c.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C c.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C c.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 10\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 9 then Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C c.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C c.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C c.[0] << 0) && ~~ mask 14\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0xB then Some Cap_asid_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0xE then Some Cap_irq_control_cap else if tag = SCAST(32 signed \<rightarrow> 32) 0x1E then Some (Cap_irq_handler_cap \<lparr>capIRQ_CL = (cap_C.words_C c.[1] >> 0) && mask 8\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x2E then Some (Cap_zombie_cap \<lparr>capZombieID_CL = cap_C.words_C c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) 0x3E then Some Cap_domain_cap else None of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x)