theory SR_lemmas_C

lemma cap_get_tag_isCap_ArchObject0:
  assumes cr: "ccap_relation (capability.ArchObjectCap cap) cap'"
  shows "(cap_get_tag cap' = scast cap_asid_control_cap) = isASIDControlCap cap
  \<and> (cap_get_tag cap' = scast cap_asid_pool_cap) = isASIDPoolCap cap
  \<and> (cap_get_tag cap' = scast cap_page_table_cap) = isPageTableCap cap
  \<and> (cap_get_tag cap' = scast cap_page_directory_cap) = isPageDirectoryCap cap
  \<and> (cap_get_tag cap' = scast cap_small_frame_cap) = (isPageCap cap \<and> capVPSize cap = ARMSmallPage)
  \<and> (cap_get_tag cap' = scast cap_frame_cap) = (isPageCap cap \<and> capVPSize cap \<noteq> ARMSmallPage)" apply (rule ccap_relationE[OF cr]) apply (simp add: cap_to_H_def cap_lift_def Let_def isArchCap_def) by (clarsimp simp: isCap_simps cap_tag_defs word_le_nat_alt pageSize_def Let_def split: if_split_asm) \<comment> \<open>takes a while\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap) = isASIDControlCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap) = isASIDPoolCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap) = isPageTableCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = isPageDirectoryCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (isPageCap cap \<and> capVPSize cap = Wellformed_C.ARMSmallPage) \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) = (isPageCap cap \<and> capVPSize cap \<noteq> Wellformed_C.ARMSmallPage) proof (prove)
goal (1 subgoal):
 1. \<And>vl. \<lbrakk>cap_lift cap' = Some vl; capability.ArchObjectCap cap = cap_to_H vl; c_valid_cap cap'\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap) = isASIDControlCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap) = isASIDPoolCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap) = isPageTableCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = isPageDirectoryCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (isPageCap cap \<and> capVPSize cap = Wellformed_C.ARMSmallPage) \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) = (isPageCap cap \<and> capVPSize cap \<noteq> Wellformed_C.ARMSmallPage) proof (prove)
goal (1 subgoal):
 1. \<And>vl. \<lbrakk>(if cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap then Some Cap_null_cap else if cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap then Some Cap_asid_control_cap else if cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap then Some Cap_irq_control_cap else if cap_get_tag cap' = 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 cap_get_tag cap' = 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 cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None) = Some vl; capability.ArchObjectCap cap = (case vl of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap); c_valid_cap cap'\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap) = isASIDControlCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap) = isASIDPoolCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap) = isPageTableCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = isPageDirectoryCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (isPageCap cap \<and> capVPSize cap = Wellformed_C.ARMSmallPage) \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) = (isPageCap cap \<and> capVPSize cap \<noteq> Wellformed_C.ARMSmallPage)