theory KHeap_DR

lemma block_lift:
  "\<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; transform_tcb (machine_state b) word tcb_type etcb = Tcb cdl_tcb_type\<rbrakk>
  \<Longrightarrow> is_thread_blocked_on_endpoint cdl_tcb_type ep = (case tcb_state tcb_type of
      Structures_A.thread_state.BlockedOnReceive p _ \<Rightarrow> ep = p
    | Structures_A.thread_state.BlockedOnSend p _ \<Rightarrow> ep = p
    | Structures_A.thread_state.BlockedOnNotification p \<Rightarrow> ep = p
    | _ \<Rightarrow> False)" apply (clarsimp simp:is_thread_blocked_on_endpoint_def transform_tcb_def infer_tcb_pending_op_def infer_tcb_bound_notification_def tcb_slots) apply (case_tac "tcb_state tcb_type") apply (auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; transform_tcb (machine_state b) word tcb_type etcb = Tcb cdl_tcb_type\<rbrakk> \<Longrightarrow> is_thread_blocked_on_endpoint cdl_tcb_type ep = (case tcb_state tcb_type of BlockedOnReceive p x \<Rightarrow> ep = p | BlockedOnSend p x \<Rightarrow> ep = p | BlockedOnNotification p \<Rightarrow> ep = p | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; cdl_tcb_type = \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable tcb_type), Suc 0 \<mapsto> transform_cap (tcb_vtable tcb_type), 2 \<mapsto> transform_cap (tcb_reply tcb_type), 3 \<mapsto> transform_cap (tcb_caller tcb_type), 4 \<mapsto> transform_cap (tcb_ipcframe tcb_type), 5 \<mapsto> case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap, 6 \<mapsto> case tcb_bound_notification tcb_type of None \<Rightarrow> cdl_cap.NullCap | Some x \<Rightarrow> BoundNotificationCap x], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb_type), cdl_tcb_intent = transform_full_intent (machine_state b) word tcb_type, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb_type = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>\<rbrakk> \<Longrightarrow> (case case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap of PendingSyncSendCap p x xa xb xc xd \<Rightarrow> p = ep | PendingSyncRecvCap p is_reply x \<Rightarrow> p = ep \<and> \<not> is_reply | PendingNtfnRecvCap p \<Rightarrow> p = ep | _ \<Rightarrow> False) = (case tcb_state tcb_type of BlockedOnReceive p x \<Rightarrow> ep = p | BlockedOnSend p x \<Rightarrow> ep = p | BlockedOnNotification p \<Rightarrow> ep = p | _ \<Rightarrow> False) proof (prove)
goal (8 subgoals):
 1. \<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; cdl_tcb_type = \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable tcb_type), Suc 0 \<mapsto> transform_cap (tcb_vtable tcb_type), 2 \<mapsto> transform_cap (tcb_reply tcb_type), 3 \<mapsto> transform_cap (tcb_caller tcb_type), 4 \<mapsto> transform_cap (tcb_ipcframe tcb_type), 5 \<mapsto> case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap, 6 \<mapsto> case tcb_bound_notification tcb_type of None \<Rightarrow> cdl_cap.NullCap | Some x \<Rightarrow> BoundNotificationCap x], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb_type), cdl_tcb_intent = transform_full_intent (machine_state b) word tcb_type, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb_type = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>; tcb_state tcb_type = Running\<rbrakk> \<Longrightarrow> (case case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap of PendingSyncSendCap p x xa xb xc xd \<Rightarrow> p = ep | PendingSyncRecvCap p is_reply x \<Rightarrow> p = ep \<and> \<not> is_reply | PendingNtfnRecvCap p \<Rightarrow> p = ep | _ \<Rightarrow> False) = (case tcb_state tcb_type of BlockedOnReceive p x \<Rightarrow> ep = p | BlockedOnSend p x \<Rightarrow> ep = p | BlockedOnNotification p \<Rightarrow> ep = p | _ \<Rightarrow> False)
 2. \<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; cdl_tcb_type = \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable tcb_type), Suc 0 \<mapsto> transform_cap (tcb_vtable tcb_type), 2 \<mapsto> transform_cap (tcb_reply tcb_type), 3 \<mapsto> transform_cap (tcb_caller tcb_type), 4 \<mapsto> transform_cap (tcb_ipcframe tcb_type), 5 \<mapsto> case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap, 6 \<mapsto> case tcb_bound_notification tcb_type of None \<Rightarrow> cdl_cap.NullCap | Some x \<Rightarrow> BoundNotificationCap x], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb_type), cdl_tcb_intent = transform_full_intent (machine_state b) word tcb_type, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb_type = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>; inactive (tcb_state tcb_type)\<rbrakk> \<Longrightarrow> (case case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap of PendingSyncSendCap p x xa xb xc xd \<Rightarrow> p = ep | PendingSyncRecvCap p is_reply x \<Rightarrow> p = ep \<and> \<not> is_reply | PendingNtfnRecvCap p \<Rightarrow> p = ep | _ \<Rightarrow> False) = (case tcb_state tcb_type of BlockedOnReceive p x \<Rightarrow> ep = p | BlockedOnSend p x \<Rightarrow> ep = p | BlockedOnNotification p \<Rightarrow> ep = p | _ \<Rightarrow> False)
 3. \<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; cdl_tcb_type = \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable tcb_type), Suc 0 \<mapsto> transform_cap (tcb_vtable tcb_type), 2 \<mapsto> transform_cap (tcb_reply tcb_type), 3 \<mapsto> transform_cap (tcb_caller tcb_type), 4 \<mapsto> transform_cap (tcb_ipcframe tcb_type), 5 \<mapsto> case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap, 6 \<mapsto> case tcb_bound_notification tcb_type of None \<Rightarrow> cdl_cap.NullCap | Some x \<Rightarrow> BoundNotificationCap x], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb_type), cdl_tcb_intent = transform_full_intent (machine_state b) word tcb_type, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb_type = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>; tcb_state tcb_type = Restart\<rbrakk> \<Longrightarrow> (case case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap of PendingSyncSendCap p x xa xb xc xd \<Rightarrow> p = ep | PendingSyncRecvCap p is_reply x \<Rightarrow> p = ep \<and> \<not> is_reply | PendingNtfnRecvCap p \<Rightarrow> p = ep | _ \<Rightarrow> False) = (case tcb_state tcb_type of BlockedOnReceive p x \<Rightarrow> ep = p | BlockedOnSend p x \<Rightarrow> ep = p | BlockedOnNotification p \<Rightarrow> ep = p | _ \<Rightarrow> False)
 4. \<And>x41 x42. \<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; cdl_tcb_type = \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable tcb_type), Suc 0 \<mapsto> transform_cap (tcb_vtable tcb_type), 2 \<mapsto> transform_cap (tcb_reply tcb_type), 3 \<mapsto> transform_cap (tcb_caller tcb_type), 4 \<mapsto> transform_cap (tcb_ipcframe tcb_type), 5 \<mapsto> case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap, 6 \<mapsto> case tcb_bound_notification tcb_type of None \<Rightarrow> cdl_cap.NullCap | Some x \<Rightarrow> BoundNotificationCap x], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb_type), cdl_tcb_intent = transform_full_intent (machine_state b) word tcb_type, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb_type = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>; tcb_state tcb_type = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> (case case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap of PendingSyncSendCap p x xa xb xc xd \<Rightarrow> p = ep | PendingSyncRecvCap p is_reply x \<Rightarrow> p = ep \<and> \<not> is_reply | PendingNtfnRecvCap p \<Rightarrow> p = ep | _ \<Rightarrow> False) = (case tcb_state tcb_type of BlockedOnReceive p x \<Rightarrow> ep = p | BlockedOnSend p x \<Rightarrow> ep = p | BlockedOnNotification p \<Rightarrow> ep = p | _ \<Rightarrow> False)
 5. \<And>x51 x52. \<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; cdl_tcb_type = \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable tcb_type), Suc 0 \<mapsto> transform_cap (tcb_vtable tcb_type), 2 \<mapsto> transform_cap (tcb_reply tcb_type), 3 \<mapsto> transform_cap (tcb_caller tcb_type), 4 \<mapsto> transform_cap (tcb_ipcframe tcb_type), 5 \<mapsto> case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap, 6 \<mapsto> case tcb_bound_notification tcb_type of None \<Rightarrow> cdl_cap.NullCap | Some x \<Rightarrow> BoundNotificationCap x], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb_type), cdl_tcb_intent = transform_full_intent (machine_state b) word tcb_type, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb_type = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>; tcb_state tcb_type = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> (case case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap of PendingSyncSendCap p x xa xb xc xd \<Rightarrow> p = ep | PendingSyncRecvCap p is_reply x \<Rightarrow> p = ep \<and> \<not> is_reply | PendingNtfnRecvCap p \<Rightarrow> p = ep | _ \<Rightarrow> False) = (case tcb_state tcb_type of BlockedOnReceive p x \<Rightarrow> ep = p | BlockedOnSend p x \<Rightarrow> ep = p | BlockedOnNotification p \<Rightarrow> ep = p | _ \<Rightarrow> False)
 6. \<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; cdl_tcb_type = \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable tcb_type), Suc 0 \<mapsto> transform_cap (tcb_vtable tcb_type), 2 \<mapsto> transform_cap (tcb_reply tcb_type), 3 \<mapsto> transform_cap (tcb_caller tcb_type), 4 \<mapsto> transform_cap (tcb_ipcframe tcb_type), 5 \<mapsto> case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap, 6 \<mapsto> case tcb_bound_notification tcb_type of None \<Rightarrow> cdl_cap.NullCap | Some x \<Rightarrow> BoundNotificationCap x], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb_type), cdl_tcb_intent = transform_full_intent (machine_state b) word tcb_type, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb_type = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>; awaiting_reply (tcb_state tcb_type)\<rbrakk> \<Longrightarrow> (case case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap of PendingSyncSendCap p x xa xb xc xd \<Rightarrow> p = ep | PendingSyncRecvCap p is_reply x \<Rightarrow> p = ep \<and> \<not> is_reply | PendingNtfnRecvCap p \<Rightarrow> p = ep | _ \<Rightarrow> False) = (case tcb_state tcb_type of BlockedOnReceive p x \<Rightarrow> ep = p | BlockedOnSend p x \<Rightarrow> ep = p | BlockedOnNotification p \<Rightarrow> ep = p | _ \<Rightarrow> False)
 7. \<And>x7. \<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; cdl_tcb_type = \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable tcb_type), Suc 0 \<mapsto> transform_cap (tcb_vtable tcb_type), 2 \<mapsto> transform_cap (tcb_reply tcb_type), 3 \<mapsto> transform_cap (tcb_caller tcb_type), 4 \<mapsto> transform_cap (tcb_ipcframe tcb_type), 5 \<mapsto> case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap, 6 \<mapsto> case tcb_bound_notification tcb_type of None \<Rightarrow> cdl_cap.NullCap | Some x \<Rightarrow> BoundNotificationCap x], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb_type), cdl_tcb_intent = transform_full_intent (machine_state b) word tcb_type, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb_type = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>; tcb_state tcb_type = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> (case case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap of PendingSyncSendCap p x xa xb xc xd \<Rightarrow> p = ep | PendingSyncRecvCap p is_reply x \<Rightarrow> p = ep \<and> \<not> is_reply | PendingNtfnRecvCap p \<Rightarrow> p = ep | _ \<Rightarrow> False) = (case tcb_state tcb_type of BlockedOnReceive p x \<Rightarrow> ep = p | BlockedOnSend p x \<Rightarrow> ep = p | BlockedOnNotification p \<Rightarrow> ep = p | _ \<Rightarrow> False)
 8. \<lbrakk>kheap b word = Some (TCB tcb_type); ekheap b word = Some etcb; cdl_tcb_type = \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable tcb_type), Suc 0 \<mapsto> transform_cap (tcb_vtable tcb_type), 2 \<mapsto> transform_cap (tcb_reply tcb_type), 3 \<mapsto> transform_cap (tcb_caller tcb_type), 4 \<mapsto> transform_cap (tcb_ipcframe tcb_type), 5 \<mapsto> case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap, 6 \<mapsto> case tcb_bound_notification tcb_type of None \<Rightarrow> cdl_cap.NullCap | Some x \<Rightarrow> BoundNotificationCap x], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb_type), cdl_tcb_intent = transform_full_intent (machine_state b) word tcb_type, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb_type = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>; idle (tcb_state tcb_type)\<rbrakk> \<Longrightarrow> (case case tcb_state tcb_type of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap word True False | BlockedOnNotification x \<Rightarrow> PendingNtfnRecvCap x | _ \<Rightarrow> cdl_cap.NullCap of PendingSyncSendCap p x xa xb xc xd \<Rightarrow> p = ep | PendingSyncRecvCap p is_reply x \<Rightarrow> p = ep \<and> \<not> is_reply | PendingNtfnRecvCap p \<Rightarrow> p = ep | _ \<Rightarrow> False) = (case tcb_state tcb_type of BlockedOnReceive p x \<Rightarrow> ep = p | BlockedOnSend p x \<Rightarrow> ep = p | BlockedOnNotification p \<Rightarrow> ep = p | _ \<Rightarrow> False) proof (prove)
goal:
No subgoals!