theory Ipc_DR

lemma corres_setup_caller_cap:
  "sender \<noteq> receiver \<Longrightarrow> dcorres dc \<top>
  (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver
   and tcb_at sender and tcb_at receiver
   and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs)
           (inject_reply_cap sender receiver can_grant)
           (setup_caller_cap sender receiver can_grant)" apply (rule dcorres_expand_pfx) apply (rule corres_guard_imp) apply (simp add: inject_reply_cap_def setup_caller_cap_def split del: if_split) apply (rule corres_split[OF set_thread_state_corres]) apply (rule reply_cap_insert_corres) apply (simp add: not_idle_thread_def)+ apply (wp set_thread_state_it|simp )+ apply (rule hoare_vcg_conj_lift) apply (clarsimp simp: not_idle_thread_def set_thread_state_def) apply wp apply (simp add: set_object_def get_object_def) apply wp+ apply simp apply (clarsimp simp: not_idle_thread_def tcb_at_def obj_at_def st_tcb_at_def) apply (rule conjI|clarsimp simp: is_tcb_def)+ apply (drule valid_tcb_objs) apply (erule get_tcb_rev) apply (simp add: valid_tcb_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sender \<noteq> receiver \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) (inject_reply_cap sender receiver can_grant) (setup_caller_cap sender receiver can_grant) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (inject_reply_cap sender receiver can_grant) (setup_caller_cap sender receiver can_grant) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q2 s s') (?Q'2 s s') (inject_reply_cap sender receiver can_grant) (setup_caller_cap sender receiver can_grant)
 2. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s s' sa
 3. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> ?Q'2 s s' sa proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> not_idle_thread sender s' \<and> not_idle_thread receiver s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q2 (transform s') s') (?Q'2 (transform s') s') (do y <- KHeap_D.set_cap (sender, tcb_pending_op_slot) (PendingSyncRecvCap sender True False);
insert_cap_child (cdl_cap.ReplyCap sender (if can_grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_replycap_slot) (receiver, tcb_caller_slot)
od) (do y <- set_thread_state sender BlockedOnReply;
cap_insert (cap.ReplyCap sender False (if can_grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)
od)
 2. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s s' sa
 3. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> ?Q'2 s s' sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' y ya. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> not_idle_thread sender s' \<and> not_idle_thread receiver s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R6 s s' y) (?R'6 s s' ya) (insert_cap_child (cdl_cap.ReplyCap sender (if can_grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_replycap_slot) (receiver, tcb_caller_slot)) (cap_insert (cap.ReplyCap sender False (if can_grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3))
 2. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> not_idle_thread sender s' \<and> not_idle_thread receiver s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 (transform s') s'\<rbrace> KHeap_D.set_cap (sender, tcb_pending_op_slot) (PendingSyncRecvCap sender True False) \<lbrace>?R6 s s'\<rbrace>
 3. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> not_idle_thread sender s' \<and> not_idle_thread receiver s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 (transform s') s'\<rbrace> set_thread_state sender BlockedOnReply \<lbrace>?R'6 s s'\<rbrace>
 4. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 s s') sa
 5. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (not_idle_thread sender and K (PendingSyncRecvCap sender True False = infer_tcb_pending_op sender BlockedOnReply) and valid_etcbs and ?Q'10 s s') sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' y ya. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> not_idle_thread sender s' \<and> not_idle_thread receiver s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'; dc y ya\<rbrakk> \<Longrightarrow> sender \<noteq> receiver
 2. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> not_idle_thread sender s' \<and> not_idle_thread receiver s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 (transform s') s'\<rbrace> KHeap_D.set_cap (sender, tcb_pending_op_slot) (PendingSyncRecvCap sender True False) \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> not_idle_thread sender s' \<and> not_idle_thread receiver s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 (transform s') s'\<rbrace> set_thread_state sender BlockedOnReply \<lbrace>\<lambda>ya. valid_idle and not_idle_thread receiver and valid_mdb and st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sender and valid_etcbs and tcb_at receiver and tcb_at sender and valid_objs\<rbrace>
 4. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 s s') sa
 5. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (not_idle_thread sender and K (PendingSyncRecvCap sender True False = infer_tcb_pending_op sender BlockedOnReply) and valid_etcbs and ?Q'10 s s') sa proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> sender \<noteq> idle_thread s' \<and> receiver \<noteq> idle_thread s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'10 (transform s') s'\<rbrace> set_thread_state sender BlockedOnReply \<lbrace>\<lambda>ya. valid_idle and (\<lambda>s. receiver \<noteq> idle_thread s) and valid_mdb and st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sender and valid_etcbs and tcb_at receiver and tcb_at sender and valid_objs\<rbrace>
 2. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 s s') sa
 3. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (not_idle_thread sender and K (PendingSyncRecvCap sender True False = infer_tcb_pending_op sender BlockedOnReply) and valid_etcbs and ?Q'10 s s') sa proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> sender \<noteq> idle_thread s' \<and> receiver \<noteq> idle_thread s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'51 (transform s') s'\<rbrace> set_thread_state sender BlockedOnReply \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sender s \<and> valid_etcbs s \<and> tcb_at receiver s \<and> tcb_at sender s \<and> valid_objs s\<rbrace>
 2. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 s s') sa
 3. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (not_idle_thread sender and K (PendingSyncRecvCap sender True False = infer_tcb_pending_op sender BlockedOnReply) and valid_etcbs and (\<lambda>a. (valid_idle and (\<lambda>s. sender = idle_thread s \<longrightarrow> idle BlockedOnReply)) a \<and> receiver \<noteq> idle_thread a \<and> valid_mdb a \<and> ?P'51 s s' a)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> sender \<noteq> idle_thread s' \<and> receiver \<noteq> idle_thread s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P59 (transform s') s'\<rbrace> set_thread_state sender BlockedOnReply \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sender\<rbrace>
 2. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> sender \<noteq> idle_thread s' \<and> receiver \<noteq> idle_thread s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'58 (transform s') s'\<rbrace> set_thread_state sender BlockedOnReply \<lbrace>\<lambda>rv s. valid_etcbs s \<and> tcb_at receiver s \<and> tcb_at sender s \<and> valid_objs s\<rbrace>
 3. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 s s') sa
 4. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (not_idle_thread sender and K (PendingSyncRecvCap sender True False = infer_tcb_pending_op sender BlockedOnReply) and valid_etcbs and (\<lambda>a. (valid_idle and (\<lambda>s. sender = idle_thread s \<longrightarrow> idle BlockedOnReply)) a \<and> receiver \<noteq> idle_thread a \<and> valid_mdb a \<and> ?P59 s s' a \<and> ?P'58 s s' a)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>sender \<noteq> receiver; valid_mdb s'; valid_idle s'; sender \<noteq> idle_thread s'; receiver \<noteq> idle_thread s'; tcb_at sender s'; tcb_at receiver s'; st_tcb_at (Not \<circ> halted) sender s'; valid_objs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P59 (transform s') s'\<rbrace> do tcb <- gets_the (get_tcb sender);
y <- KHeap_A.set_object sender (TCB (update_tcb_state BlockedOnReply tcb));
set_thread_state_ext sender
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sender\<rbrace>
 2. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> sender \<noteq> idle_thread s' \<and> receiver \<noteq> idle_thread s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'58 (transform s') s'\<rbrace> set_thread_state sender BlockedOnReply \<lbrace>\<lambda>rv s. valid_etcbs s \<and> tcb_at receiver s \<and> tcb_at sender s \<and> valid_objs s\<rbrace>
 3. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 s s') sa
 4. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (not_idle_thread sender and K (PendingSyncRecvCap sender True False = infer_tcb_pending_op sender BlockedOnReply) and valid_etcbs and (\<lambda>a. (valid_idle and (\<lambda>s. sender = idle_thread s \<longrightarrow> idle BlockedOnReply)) a \<and> receiver \<noteq> idle_thread a \<and> valid_mdb a \<and> ?P59 s s' a \<and> ?P'58 s s' a)) sa proof (prove)
goal (5 subgoals):
 1. \<And>s' tcb. \<lbrakk>sender \<noteq> receiver; valid_mdb s'; valid_idle s'; sender \<noteq> idle_thread s'; receiver \<noteq> idle_thread s'; tcb_at sender s'; tcb_at receiver s'; st_tcb_at (Not \<circ> halted) sender s'; valid_objs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?B76 s' tcb\<rbrace> KHeap_A.set_object sender (TCB (update_tcb_state BlockedOnReply tcb)) \<lbrace>\<lambda>x. st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sender\<rbrace>
 2. \<And>s'. \<lbrakk>sender \<noteq> receiver; valid_mdb s'; valid_idle s'; sender \<noteq> idle_thread s'; receiver \<noteq> idle_thread s'; tcb_at sender s'; tcb_at receiver s'; st_tcb_at (Not \<circ> halted) sender s'; valid_objs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P59 (transform s') s'\<rbrace> gets_the (get_tcb sender) \<lbrace>?B76 s'\<rbrace>
 3. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> sender \<noteq> idle_thread s' \<and> receiver \<noteq> idle_thread s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'58 (transform s') s'\<rbrace> set_thread_state sender BlockedOnReply \<lbrace>\<lambda>rv s. valid_etcbs s \<and> tcb_at receiver s \<and> tcb_at sender s \<and> valid_objs s\<rbrace>
 4. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 s s') sa
 5. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (not_idle_thread sender and K (PendingSyncRecvCap sender True False = infer_tcb_pending_op sender BlockedOnReply) and valid_etcbs and (\<lambda>a. (valid_idle and (\<lambda>s. sender = idle_thread s \<longrightarrow> idle BlockedOnReply)) a \<and> receiver \<noteq> idle_thread a \<and> valid_mdb a \<and> ?P59 s s' a \<and> ?P'58 s s' a)) sa proof (prove)
goal (5 subgoals):
 1. \<And>s' tcb. \<lbrakk>sender \<noteq> receiver; valid_mdb s'; valid_idle s'; sender \<noteq> idle_thread s'; receiver \<noteq> idle_thread s'; tcb_at sender s'; tcb_at receiver s'; st_tcb_at (Not \<circ> halted) sender s'; valid_objs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?B76 s' tcb\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh sender = Some y);
return (the (kh sender))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (update_kheap ((kheap s)(sender \<mapsto> TCB (update_tcb_state BlockedOnReply tcb))) s)
od \<lbrace>\<lambda>x. st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sender\<rbrace>
 2. \<And>s'. \<lbrakk>sender \<noteq> receiver; valid_mdb s'; valid_idle s'; sender \<noteq> idle_thread s'; receiver \<noteq> idle_thread s'; tcb_at sender s'; tcb_at receiver s'; st_tcb_at (Not \<circ> halted) sender s'; valid_objs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P59 (transform s') s'\<rbrace> gets_the (get_tcb sender) \<lbrace>?B76 s'\<rbrace>
 3. \<And>s s'. \<lbrakk>sender \<noteq> receiver; s = transform s'; valid_mdb s' \<and> valid_idle s' \<and> sender \<noteq> idle_thread s' \<and> receiver \<noteq> idle_thread s' \<and> tcb_at sender s' \<and> tcb_at receiver s' \<and> st_tcb_at (Not \<circ> halted) sender s' \<and> valid_objs s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'58 (transform s') s'\<rbrace> set_thread_state sender BlockedOnReply \<lbrace>\<lambda>rv s. valid_etcbs s \<and> tcb_at receiver s \<and> tcb_at sender s \<and> valid_objs s\<rbrace>
 4. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 s s') sa
 5. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (not_idle_thread sender and K (PendingSyncRecvCap sender True False = infer_tcb_pending_op sender BlockedOnReply) and valid_etcbs and (\<lambda>a. (valid_idle and (\<lambda>s. sender = idle_thread s \<longrightarrow> idle BlockedOnReply)) a \<and> receiver \<noteq> idle_thread a \<and> valid_mdb a \<and> ?P59 s s' a \<and> ?P'58 s s' a)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q12 s s') sa
 2. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (not_idle_thread sender and K (PendingSyncRecvCap sender True False = infer_tcb_pending_op sender BlockedOnReply) and valid_etcbs and (\<lambda>a. (valid_idle and (\<lambda>s. sender = idle_thread s \<longrightarrow> idle BlockedOnReply)) a \<and> receiver \<noteq> idle_thread a \<and> valid_mdb a \<and> (get_tcb sender a \<noteq> None \<longrightarrow> (\<exists>y. kheap a sender = Some y) \<longrightarrow> a_type (the (kheap a sender)) = ATCB \<longrightarrow> st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sender (update_kheap ((kheap a)(sender \<mapsto> TCB (update_tcb_state BlockedOnReply (the (get_tcb sender a))))) a)) \<and> valid_etcbs a \<and> tcb_at receiver a \<and> tcb_at sender a \<and> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) cap.NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) a)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>sender \<noteq> receiver; s = transform s'; True; (valid_mdb and valid_idle and not_idle_thread sender and not_idle_thread receiver and tcb_at sender and tcb_at receiver and st_tcb_at (Not \<circ> halted) sender and valid_objs and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (not_idle_thread sender and K (PendingSyncRecvCap sender True False = infer_tcb_pending_op sender BlockedOnReply) and valid_etcbs and (\<lambda>a. (valid_idle and (\<lambda>s. sender = idle_thread s \<longrightarrow> idle BlockedOnReply)) a \<and> receiver \<noteq> idle_thread a \<and> valid_mdb a \<and> (get_tcb sender a \<noteq> None \<longrightarrow> (\<exists>y. kheap a sender = Some y) \<longrightarrow> a_type (the (kheap a sender)) = ATCB \<longrightarrow> st_tcb_at (\<lambda>r. r \<noteq> Inactive \<and> r \<noteq> IdleThreadState) sender (update_kheap ((kheap a)(sender \<mapsto> TCB (update_tcb_state BlockedOnReply (the (get_tcb sender a))))) a)) \<and> valid_etcbs a \<and> tcb_at receiver a \<and> tcb_at sender a \<and> (valid_objs and valid_tcb_state BlockedOnReply and (\<lambda>s. (\<forall>a data. BlockedOnReply = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) cap.NullCap) (sender, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) sender s \<or> halted BlockedOnReply \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s))) a)) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa koa tcb. \<lbrakk>sender \<noteq> receiver; valid_mdb sa; valid_idle sa; sender \<noteq> idle_thread sa; receiver \<noteq> idle_thread sa; kheap sa receiver = Some koa; is_tcb koa; valid_objs sa; valid_etcbs sa; kheap sa sender = Some (TCB tcb); \<not> halted (tcb_state tcb)\<rbrakk> \<Longrightarrow> valid_tcb_state BlockedOnReply sa proof (prove)
goal (1 subgoal):
 1. \<And>sa koa tcb. \<lbrakk>sender \<noteq> receiver; valid_mdb sa; valid_idle sa; sender \<noteq> idle_thread sa; receiver \<noteq> idle_thread sa; kheap sa receiver = Some koa; case koa of TCB t \<Rightarrow> True | _ \<Rightarrow> False; valid_objs sa; valid_etcbs sa; kheap sa sender = Some (TCB tcb); \<not> halted (tcb_state tcb)\<rbrakk> \<Longrightarrow> valid_tcb_state BlockedOnReply sa proof (prove)
goal (2 subgoals):
 1. \<And>sa koa tcb. \<lbrakk>sender \<noteq> receiver; valid_mdb sa; valid_idle sa; sender \<noteq> idle_thread sa; receiver \<noteq> idle_thread sa; kheap sa receiver = Some koa; case koa of TCB t \<Rightarrow> True | _ \<Rightarrow> False; valid_etcbs sa; kheap sa sender = Some (TCB tcb); \<not> halted (tcb_state tcb)\<rbrakk> \<Longrightarrow> get_tcb (?thread138 sa koa tcb) sa = Some (?y138 sa koa tcb)
 2. \<And>sa koa tcb. \<lbrakk>sender \<noteq> receiver; valid_mdb sa; valid_idle sa; sender \<noteq> idle_thread sa; receiver \<noteq> idle_thread sa; kheap sa receiver = Some koa; case koa of TCB t \<Rightarrow> True | _ \<Rightarrow> False; valid_etcbs sa; kheap sa sender = Some (TCB tcb); \<not> halted (tcb_state tcb); valid_tcb (?thread138 sa koa tcb) (?y138 sa koa tcb) sa\<rbrakk> \<Longrightarrow> valid_tcb_state BlockedOnReply sa proof (prove)
goal (1 subgoal):
 1. \<And>sa koa tcb. \<lbrakk>sender \<noteq> receiver; valid_mdb sa; valid_idle sa; sender \<noteq> idle_thread sa; receiver \<noteq> idle_thread sa; kheap sa receiver = Some koa; case koa of TCB t \<Rightarrow> True | _ \<Rightarrow> False; valid_etcbs sa; kheap sa sender = Some (TCB tcb); \<not> halted (tcb_state tcb); valid_tcb sender tcb sa\<rbrakk> \<Longrightarrow> valid_tcb_state BlockedOnReply sa proof (prove)
goal:
No subgoals!