theory CSpace_C

lemma capBlockSize_CL_maxSize:
  " \<lbrakk> cap_get_tag c = scast cap_untyped_cap \<rbrakk> \<Longrightarrow> capBlockSize_CL (cap_untyped_cap_lift c) < 0x20" apply (clarsimp simp: cap_untyped_cap_lift_def) apply (clarsimp simp: cap_lift_def) apply (clarsimp simp: cap_untyped_cap_def cap_null_cap_def) apply (rule word_and_less') apply (simp add: mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<Longrightarrow> capBlockSize_CL (cap_untyped_cap_lift c) < 0x20 proof (prove)
goal (1 subgoal):
 1. cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<Longrightarrow> capBlockSize_CL (case cap_lift c of Some (Cap_untyped_cap rec) \<Rightarrow> rec) < 0x20 proof (prove)
goal (1 subgoal):
 1. cap_get_tag c = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<Longrightarrow> capBlockSize_CL (case let tag = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap in if cap_untyped_cap = cap_null_cap then Some Cap_null_cap else if tag = tag 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) cap_endpoint_cap 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) cap_notification_cap 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) cap_reply_cap 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) cap_cnode_cap 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) cap_thread_cap 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) cap_small_frame_cap 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) cap_frame_cap 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) cap_asid_pool_cap 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) cap_page_table_cap 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) cap_page_directory_cap 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) 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 c.[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 c.[1] >> 0, capZombieType_CL = (cap_C.words_C c.[0] >> 8) && mask 6\<rparr>) else if tag = SCAST(32 signed \<rightarrow> 32) cap_domain_cap then Some Cap_domain_cap else None of Some (Cap_untyped_cap rec) \<Rightarrow> rec) < 0x20 proof (prove)
goal (1 subgoal):
 1. cap_get_tag c = 2 \<Longrightarrow> cap_C.words_C c.[Suc 0] && mask 5 < 0x20 proof (prove)
goal (1 subgoal):
 1. cap_get_tag c = 2 \<Longrightarrow> mask 5 < 0x20 proof (prove)
goal:
No subgoals!