theory Recycle_C

lemma ctcb_relation_blocking_ipc_badge:
  "\<lbrakk> ctcb_relation tcb ctcb; isBlockedOnSend (tcbState tcb) \<rbrakk> \<Longrightarrow>
      tsType_CL (thread_state_lift (tcbState_C ctcb)) = scast ThreadState_BlockedOnSend"
  "\<lbrakk> ctcb_relation tcb ctcb;
        tsType_CL (thread_state_lift (tcbState_C ctcb)) = scast ThreadState_BlockedOnSend \<rbrakk>
      \<Longrightarrow> blockingIPCBadge (tcbState tcb)
             = blockingIPCBadge_CL (thread_state_lift (tcbState_C ctcb))" apply (clarsimp simp add: ctcb_relation_def) apply (simp add: isBlockedOnSend_def split: Structures_H.thread_state.split_asm) apply (clarsimp simp: cthread_state_relation_def) apply (clarsimp simp add: ctcb_relation_def cthread_state_relation_def) apply (cases "tcbState tcb", simp_all add: "StrictC'_thread_state_defs") done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>ctcb_relation tcb ctcb; isBlockedOnSend (tcbState tcb)\<rbrakk> \<Longrightarrow> tsType_CL (thread_state_lift (tcbState_C ctcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend) &&& (\<lbrakk>ctcb_relation tcb ctcb; tsType_CL (thread_state_lift (tcbState_C ctcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend\<rbrakk> \<Longrightarrow> blockingIPCBadge (tcbState tcb) = blockingIPCBadge_CL (thread_state_lift (tcbState_C ctcb))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isBlockedOnSend (tcbState tcb); tcbFaultHandler tcb = tcbFaultHandler_C ctcb; cthread_state_relation (tcbState tcb) (tcbState_C ctcb, tcbFault_C ctcb); tcbIPCBuffer tcb = tcbIPCBuffer_C ctcb; carch_tcb_relation (tcbArch tcb) (tcbArch_C ctcb); tcbQueued tcb = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ctcb))); UCAST(8 \<rightarrow> 32) (tcbDomain tcb) = tcbDomain_C ctcb; UCAST(8 \<rightarrow> 32) (tcbPriority tcb) = tcbPriority_C ctcb; UCAST(8 \<rightarrow> 32) (tcbMCP tcb) = tcbMCP_C ctcb; tcbTimeSlice tcb = unat (tcbTimeSlice_C ctcb); cfault_rel (tcbFault tcb) (seL4_Fault_lift (tcbFault_C ctcb)) (lookup_fault_lift (tcbLookupFailure_C ctcb)); option_to_ptr (tcbBoundNotification tcb) = tcbBoundNotification_C ctcb\<rbrakk> \<Longrightarrow> tsType_CL (thread_state_lift (tcbState_C ctcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend
 2. \<lbrakk>ctcb_relation tcb ctcb; tsType_CL (thread_state_lift (tcbState_C ctcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend\<rbrakk> \<Longrightarrow> blockingIPCBadge (tcbState tcb) = blockingIPCBadge_CL (thread_state_lift (tcbState_C ctcb)) proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72 x73 x74 x75. \<lbrakk>tcbFaultHandler tcb = tcbFaultHandler_C ctcb; cthread_state_relation (Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75) (tcbState_C ctcb, tcbFault_C ctcb); tcbIPCBuffer tcb = tcbIPCBuffer_C ctcb; carch_tcb_relation (tcbArch tcb) (tcbArch_C ctcb); tcbQueued tcb = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ctcb))); UCAST(8 \<rightarrow> 32) (tcbDomain tcb) = tcbDomain_C ctcb; UCAST(8 \<rightarrow> 32) (tcbPriority tcb) = tcbPriority_C ctcb; UCAST(8 \<rightarrow> 32) (tcbMCP tcb) = tcbMCP_C ctcb; tcbTimeSlice tcb = unat (tcbTimeSlice_C ctcb); cfault_rel (tcbFault tcb) (seL4_Fault_lift (tcbFault_C ctcb)) (lookup_fault_lift (tcbLookupFailure_C ctcb)); option_to_ptr (tcbBoundNotification tcb) = tcbBoundNotification_C ctcb; tcbState tcb = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> tsType_CL (thread_state_lift (tcbState_C ctcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend
 2. \<lbrakk>ctcb_relation tcb ctcb; tsType_CL (thread_state_lift (tcbState_C ctcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend\<rbrakk> \<Longrightarrow> blockingIPCBadge (tcbState tcb) = blockingIPCBadge_CL (thread_state_lift (tcbState_C ctcb)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctcb_relation tcb ctcb; tsType_CL (thread_state_lift (tcbState_C ctcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend\<rbrakk> \<Longrightarrow> blockingIPCBadge (tcbState tcb) = blockingIPCBadge_CL (thread_state_lift (tcbState_C ctcb)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tsType_CL (thread_state_lift (tcbState_C ctcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend; tcbFaultHandler tcb = tcbFaultHandler_C ctcb; cthread_state_relation_lifted (tcbState tcb) (thread_state_lift (tcbState_C ctcb), seL4_Fault_lift (tcbFault_C ctcb)); tcbIPCBuffer tcb = tcbIPCBuffer_C ctcb; carch_tcb_relation (tcbArch tcb) (tcbArch_C ctcb); tcbQueued tcb = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ctcb))); UCAST(8 \<rightarrow> 32) (tcbDomain tcb) = tcbDomain_C ctcb; UCAST(8 \<rightarrow> 32) (tcbPriority tcb) = tcbPriority_C ctcb; UCAST(8 \<rightarrow> 32) (tcbMCP tcb) = tcbMCP_C ctcb; tcbTimeSlice tcb = unat (tcbTimeSlice_C ctcb); cfault_rel (tcbFault tcb) (seL4_Fault_lift (tcbFault_C ctcb)) (lookup_fault_lift (tcbLookupFailure_C ctcb)); option_to_ptr (tcbBoundNotification tcb) = tcbBoundNotification_C ctcb\<rbrakk> \<Longrightarrow> blockingIPCBadge (tcbState tcb) = blockingIPCBadge_CL (thread_state_lift (tcbState_C ctcb)) proof (prove)
goal:
No subgoals!