theory Ipc_DR

lemma not_idle_after_blocked_cancel_ipc:
  "\<lbrace>valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace>
    blocked_cancel_ipc state obj_id' \<lbrace>\<lambda>y. valid_idle\<rbrace>" including no_pre apply (simp add:blocked_cancel_ipc_def) apply wp apply (clarsimp simp:not_idle_thread_def) apply (clarsimp simp:get_blocking_object_def) apply (case_tac state) apply clarsimp+ apply (clarsimp simp:valid_def return_def st_tcb_at_def valid_objs_def obj_at_def) apply (drule_tac x = obj_id' in bspec) apply (clarsimp simp:valid_obj_def valid_tcb_def valid_tcb_state_def)+ apply (drule_tac t = "tcb_state tcb" in sym) apply (clarsimp simp:obj_at_def is_ep_def2) apply (clarsimp simp:valid_def return_def st_tcb_at_def obj_at_def valid_objs_def) apply (drule_tac x = obj_id' in bspec) apply (clarsimp simp:valid_obj_def valid_tcb_def valid_tcb_state_def)+ apply (drule_tac t = "tcb_state tcb" in sym) apply (clarsimp simp:obj_at_def is_ep_def2) apply (clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> blocked_cancel_ipc state obj_id' \<lbrace>\<lambda>y. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> blocked_cancel_ipc state obj_id' \<lbrace>\<lambda>y. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> do epptr <- get_blocking_object state;
ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
y <- set_endpoint epptr (case remove1 obj_id' queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 obj_id' queue));
set_thread_state obj_id' Inactive
od \<lbrace>\<lambda>y. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> get_blocking_object state \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. partial_inv kernel_object.Endpoint ko \<noteq> None) epptr s \<and> valid_idle s \<and> (obj_id' = idle_thread s \<longrightarrow> idle Inactive)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> get_blocking_object state \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (8 subgoals):
 1. state = Running \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 2. inactive state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 3. state = Restart \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. \<And>x41 x42. state = BlockedOnReceive x41 x42 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 5. \<And>x51 x52. state = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 6. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 7. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 8. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42. state = BlockedOnReceive x41 x42 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) (BlockedOnReceive x41 x42)) obj_id'\<rbrace> return x41 \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 2. \<And>x51 x52. state = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 3. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 5. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 s tcb. \<lbrakk>state = tcb_state tcb; valid_idle s; obj_id' \<noteq> idle_thread s; \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s obj_id' = Some (TCB tcb); BlockedOnReceive x41 x42 = tcb_state tcb\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x41 = Some ko \<and> (\<exists>y. kernel_object.Endpoint y = ko)
 2. \<And>x51 x52. state = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 3. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 5. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x41 x42 s tcb. \<lbrakk>state = tcb_state tcb; valid_idle s; obj_id' \<noteq> idle_thread s; kheap s obj_id' = Some (TCB tcb); BlockedOnReceive x41 x42 = tcb_state tcb\<rbrakk> \<Longrightarrow> obj_id' \<in> dom (kheap s)
 2. \<And>x41 x42 s tcb. \<lbrakk>state = tcb_state tcb; valid_idle s; obj_id' \<noteq> idle_thread s; kheap s obj_id' = Some (TCB tcb); BlockedOnReceive x41 x42 = tcb_state tcb; \<exists>obj. kheap s obj_id' = Some obj \<and> valid_obj obj_id' obj s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x41 = Some ko \<and> (\<exists>y. kernel_object.Endpoint y = ko)
 3. \<And>x51 x52. state = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 5. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 6. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 s tcb. \<lbrakk>state = tcb_state tcb; valid_idle s; obj_id' \<noteq> idle_thread s; kheap s obj_id' = Some (TCB tcb); BlockedOnReceive x41 x42 = tcb_state tcb; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr obj_id' (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); case tcb_state tcb of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x41 = Some ko \<and> (\<exists>y. kernel_object.Endpoint y = ko)
 2. \<And>x51 x52. state = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 3. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 5. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 s tcb. \<lbrakk>valid_idle s; obj_id' \<noteq> idle_thread s; kheap s obj_id' = Some (TCB tcb); BlockedOnReceive x41 x42 = tcb_state tcb; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr obj_id' (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); case tcb_state tcb of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; tcb_state tcb = state\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x41 = Some ko \<and> (\<exists>y. kernel_object.Endpoint y = ko)
 2. \<And>x51 x52. state = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 3. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 5. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52. state = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 2. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 3. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 s tcb. \<lbrakk>state = tcb_state tcb; valid_idle s; obj_id' \<noteq> idle_thread s; \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s obj_id' = Some (TCB tcb); BlockedOnSend x51 x52 = tcb_state tcb\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x51 = Some ko \<and> (\<exists>y. kernel_object.Endpoint y = ko)
 2. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 3. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x51 x52 s tcb. \<lbrakk>state = tcb_state tcb; valid_idle s; obj_id' \<noteq> idle_thread s; kheap s obj_id' = Some (TCB tcb); BlockedOnSend x51 x52 = tcb_state tcb\<rbrakk> \<Longrightarrow> obj_id' \<in> dom (kheap s)
 2. \<And>x51 x52 s tcb. \<lbrakk>state = tcb_state tcb; valid_idle s; obj_id' \<noteq> idle_thread s; kheap s obj_id' = Some (TCB tcb); BlockedOnSend x51 x52 = tcb_state tcb; \<exists>obj. kheap s obj_id' = Some obj \<and> valid_obj obj_id' obj s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x51 = Some ko \<and> (\<exists>y. kernel_object.Endpoint y = ko)
 3. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 5. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 s tcb. \<lbrakk>state = tcb_state tcb; valid_idle s; obj_id' \<noteq> idle_thread s; kheap s obj_id' = Some (TCB tcb); BlockedOnSend x51 x52 = tcb_state tcb; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr obj_id' (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); case tcb_state tcb of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x51 = Some ko \<and> (\<exists>y. kernel_object.Endpoint y = ko)
 2. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 3. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 s tcb. \<lbrakk>valid_idle s; obj_id' \<noteq> idle_thread s; kheap s obj_id' = Some (TCB tcb); BlockedOnSend x51 x52 = tcb_state tcb; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr obj_id' (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); case tcb_state tcb of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; tcb_state tcb = state\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x51 = Some ko \<and> (\<exists>y. kernel_object.Endpoint y = ko)
 2. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 3. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 4. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal (3 subgoals):
 1. awaiting_reply state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 2. \<And>x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 3. idle state \<Longrightarrow> \<lbrace>valid_idle and (\<lambda>s. obj_id' \<noteq> idle_thread s) and valid_objs and st_tcb_at ((=) state) obj_id'\<rbrace> case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail \<lbrace>\<lambda>epptr s. obj_at (\<lambda>ko. \<exists>y. kernel_object.Endpoint y = ko) epptr s \<and> valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace> proof (prove)
goal:
No subgoals!