theory Syscall_DR

lemma handle_reply_corres:
  "dcorres dc \<top> (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs)
  Syscall_D.handle_reply Syscall_A.handle_reply" apply (simp add: Syscall_D.handle_reply_def Syscall_A.handle_reply_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cur_thread_corres]) apply simp apply (rename_tac thread) apply (rule_tac R="\<lambda>_. \<top>" and
                      R'="\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread
                                and not_idle_thread thread
                                and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)"
                  in  corres_split) apply (rule get_cap_corres) apply (clarsimp simp: simp: transform_tcb_slot_simp) apply (simp add: transform_cap_def corres_fail split: cap.split) apply (clarsimp simp: corres_fail dc_def[symmetric] split: bool.split) apply (rename_tac word rights) apply (rule corres_guard_imp) apply (rule do_reply_transfer_corres) apply (simp add: transform_tcb_slot_simp) apply simp apply (clarsimp simp:ct_running_not_idle_etc) apply (frule caps_of_state_valid(1)) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (simp add:valid_cap_def)+ apply (clarsimp simp:valid_state_def invs_def valid_reply_caps_def dest!:has_reply_cap_cte_wpD) apply (drule_tac x = word in spec, simp add: cte_wp_at_def) apply (clarsimp simp:not_idle_thread_def pred_tcb_at_def obj_at_def valid_idle_def
                             cte_wp_at_def has_reply_cap_def is_reply_cap_to_def) apply blast apply (wpsimp wp: get_cap_wp)+ apply (clarsimp simp:ct_in_state_def invs_def valid_state_def pred_tcb_at_def tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) Syscall_D.handle_reply Syscall_A.handle_reply proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) (do tcb_id <- gets_the cdl_current_thread;
caller_cap <- KHeap_D.get_cap (tcb_id, tcb_caller_slot);
case caller_cap of cdl_cap.NullCap \<Rightarrow> return () | cdl_cap.ReplyCap target rights \<Rightarrow> Endpoint_D.do_reply_transfer tcb_id target (tcb_id, tcb_caller_slot) (AllowGrant \<in> rights) | _ \<Rightarrow> fail
od) (do thread <- gets cur_thread;
caller_cap <- CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3);
case caller_cap of cap.NullCap \<Rightarrow> return () | cap.ReplyCap caller True R \<Rightarrow> fail | cap.ReplyCap caller False R \<Rightarrow> Ipc_A.do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (do tcb_id <- gets_the cdl_current_thread;
caller_cap <- KHeap_D.get_cap (tcb_id, tcb_caller_slot);
case caller_cap of cdl_cap.NullCap \<Rightarrow> return () | cdl_cap.ReplyCap target rights \<Rightarrow> Endpoint_D.do_reply_transfer tcb_id target (tcb_id, tcb_caller_slot) (AllowGrant \<in> rights) | _ \<Rightarrow> fail
od) (do thread <- gets cur_thread;
caller_cap <- CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3);
case caller_cap of cap.NullCap \<Rightarrow> return () | cap.ReplyCap caller True R \<Rightarrow> fail | cap.ReplyCap caller False R \<Rightarrow> Ipc_A.do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>tcb_id thread. tcb_id = thread \<Longrightarrow> dcorres dc (?R4 tcb_id) (?R'4 thread) (do caller_cap <- KHeap_D.get_cap (tcb_id, tcb_caller_slot);
case caller_cap of cdl_cap.NullCap \<Rightarrow> return () | cdl_cap.ReplyCap target rights \<Rightarrow> Endpoint_D.do_reply_transfer tcb_id target (tcb_id, tcb_caller_slot) (AllowGrant \<in> rights) | _ \<Rightarrow> fail
od) (do caller_cap <- CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3);
case caller_cap of cap.NullCap \<Rightarrow> return () | cap.ReplyCap caller True R \<Rightarrow> fail | cap.ReplyCap caller False R \<Rightarrow> Ipc_A.do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od)
 2. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>tcb_id. dcorres dc (?R4 tcb_id) (?R'4 tcb_id) (KHeap_D.get_cap (tcb_id, tcb_caller_slot) >>= case_cdl_cap (return ()) (\<lambda>bool set1 set2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>target rights. Endpoint_D.do_reply_transfer tcb_id target (tcb_id, tcb_caller_slot) (AllowGrant \<in> rights)) (\<lambda>word. fail) (\<lambda>word1 word2 nat1 nat2. fail) (\<lambda>word. fail) fail (\<lambda>word1 word2 bool1 bool2 bool3 bool4. fail) (\<lambda>word bool1 bool2. fail) (\<lambda>word. fail) fail fail fail (\<lambda>word. fail) (\<lambda>bool word set nat cdl_frame_cap_type option. fail) (\<lambda>word cdl_frame_cap_type option. fail) (\<lambda>word cdl_frame_cap_type option. fail) fail (\<lambda>word nat. fail) (\<lambda>word set. fail) fail (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail)) (CSpaceAcc_A.get_cap (tcb_id, tcb_cnode_index 3) >>= case_cap (return ()) (\<lambda>bool word nat1 nat2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>caller bool R. case bool of True \<Rightarrow> fail | False \<Rightarrow> Ipc_A.do_reply_transfer tcb_id caller (tcb_id, tcb_cnode_index 3) (AllowGrant \<in> R)) (\<lambda>word nat list. fail) (\<lambda>word. fail) fail fail (\<lambda>word. fail) (\<lambda>word option nat. fail) (\<lambda>arch_cap. fail))
 2. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>thread. dcorres dc (?R4 thread) (?R'4 thread) (KHeap_D.get_cap (thread, tcb_caller_slot) >>= case_cdl_cap (return ()) (\<lambda>bool set1 set2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>target rights. Endpoint_D.do_reply_transfer thread target (thread, tcb_caller_slot) (AllowGrant \<in> rights)) (\<lambda>word. fail) (\<lambda>word1 word2 nat1 nat2. fail) (\<lambda>word. fail) fail (\<lambda>word1 word2 bool1 bool2 bool3 bool4. fail) (\<lambda>word bool1 bool2. fail) (\<lambda>word. fail) fail fail fail (\<lambda>word. fail) (\<lambda>bool word set nat cdl_frame_cap_type option. fail) (\<lambda>word cdl_frame_cap_type option. fail) (\<lambda>word cdl_frame_cap_type option. fail) fail (\<lambda>word nat. fail) (\<lambda>word set. fail) fail (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail) (\<lambda>word. fail)) (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) >>= case_cap (return ()) (\<lambda>bool word nat1 nat2. fail) (\<lambda>word1 word2 set. fail) (\<lambda>word1 word2 set. fail) (\<lambda>caller bool R. case bool of True \<Rightarrow> fail | False \<Rightarrow> Ipc_A.do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R)) (\<lambda>word nat list. fail) (\<lambda>word. fail) fail fail (\<lambda>word. fail) (\<lambda>word option nat. fail) (\<lambda>arch_cap. fail))
 2. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>thread. dcorres (?r'8 thread) (?P8 thread) (?P'8 thread) (KHeap_D.get_cap (thread, tcb_caller_slot)) (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3))
 2. \<And>thread rv rv'. ?r'8 thread rv rv' \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) rv') (thread, tcb_cnode_index 3)) (case rv of cdl_cap.NullCap \<Rightarrow> return () | cdl_cap.ReplyCap target rights \<Rightarrow> Endpoint_D.do_reply_transfer thread target (thread, tcb_caller_slot) (AllowGrant \<in> rights) | _ \<Rightarrow> fail) (case rv' of cap.NullCap \<Rightarrow> return () | cap.ReplyCap caller True R \<Rightarrow> fail | cap.ReplyCap caller False R \<Rightarrow> Ipc_A.do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail)
 3. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. ?P8 thread and ?Q8 thread\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. ?P'8 thread and ?Q'8 thread\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>thread. (thread, tcb_caller_slot) = transform_cslot_ptr (thread, tcb_cnode_index 3)
 2. \<And>thread rv rv'. rv = transform_cap rv' \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) rv') (thread, tcb_cnode_index 3)) (case rv of cdl_cap.NullCap \<Rightarrow> return () | cdl_cap.ReplyCap target rights \<Rightarrow> Endpoint_D.do_reply_transfer thread target (thread, tcb_caller_slot) (AllowGrant \<in> rights) | _ \<Rightarrow> fail) (case rv' of cap.NullCap \<Rightarrow> return () | cap.ReplyCap caller True R \<Rightarrow> fail | cap.ReplyCap caller False R \<Rightarrow> Ipc_A.do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail)
 3. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread rv rv'. rv = transform_cap rv' \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) rv') (thread, tcb_cnode_index 3)) (case rv of cdl_cap.NullCap \<Rightarrow> return () | cdl_cap.ReplyCap target rights \<Rightarrow> Endpoint_D.do_reply_transfer thread target (thread, tcb_caller_slot) (AllowGrant \<in> rights) | _ \<Rightarrow> fail) (case rv' of cap.NullCap \<Rightarrow> return () | cap.ReplyCap caller True R \<Rightarrow> fail | cap.ReplyCap caller False R \<Rightarrow> Ipc_A.do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail)
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread rv rv'. rv = (case rv' of cap.NullCap \<Rightarrow> cdl_cap.NullCap | cap.UntypedCap dev ptr size_bits idx \<Rightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ size_bits - 1} (free_range_of_untyped idx size_bits ptr) | cap.EndpointCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.EndpointCap ptr badge cap_rights_ | cap.NotificationCap ptr badge cap_rights_ \<Rightarrow> cdl_cap.NotificationCap ptr badge cap_rights_ | cap.ReplyCap ptr is_master cap_rights_ \<Rightarrow> if is_master then MasterReplyCap ptr else cdl_cap.ReplyCap ptr cap_rights_ | cap.CNodeCap ptr size_bits guard \<Rightarrow> cdl_cap.CNodeCap ptr (of_bl guard) (length guard) size_bits | ThreadCap ptr \<Rightarrow> TcbCap ptr | cap.DomainCap \<Rightarrow> cdl_cap.DomainCap | IRQControlCap \<Rightarrow> IrqControlCap | IRQHandlerCap irq \<Rightarrow> IrqHandlerCap irq | Zombie ptr x xa \<Rightarrow> ZombieCap ptr | ArchObjectCap (ASIDPoolCap ptr asid) \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ArchObjectCap ASIDControlCap \<Rightarrow> AsidControlCap | ArchObjectCap (PageCap dev ptr cap_rights_ sz mp) \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageTableCap ptr mp) \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | ArchObjectCap (arch_cap.PageDirectoryCap ptr mp) \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp)) \<Longrightarrow> \<forall>x51 x53. rv' = cap.ReplyCap x51 False x53 \<longrightarrow> dcorres dc (\<lambda>_. True) (invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) (cap.ReplyCap x51 False x53)) (thread, tcb_cnode_index 3)) (Endpoint_D.do_reply_transfer thread x51 (thread, tcb_caller_slot) (AllowGrant \<in> x53)) (Ipc_A.do_reply_transfer thread x51 (thread, tcb_cnode_index 3) (AllowGrant \<in> x53))
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread x51 x53. dcorres dc (\<lambda>_. True) (invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) (cap.ReplyCap x51 False x53)) (thread, tcb_cnode_index 3)) (Endpoint_D.do_reply_transfer thread x51 (thread, tcb_caller_slot) (AllowGrant \<in> x53)) (Ipc_A.do_reply_transfer thread x51 (thread, tcb_cnode_index 3) (AllowGrant \<in> x53))
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread word rights. dcorres dc (\<lambda>_. True) (invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3)) (Endpoint_D.do_reply_transfer thread word (thread, tcb_caller_slot) (AllowGrant \<in> rights)) (Ipc_A.do_reply_transfer thread word (thread, tcb_cnode_index 3) (AllowGrant \<in> rights))
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>thread word rights. dcorres dc (?Q36 thread word rights) (?Q'36 thread word rights) (Endpoint_D.do_reply_transfer thread word (thread, tcb_caller_slot) (AllowGrant \<in> rights)) (Ipc_A.do_reply_transfer thread word (thread, tcb_cnode_index 3) (AllowGrant \<in> rights))
 2. \<And>thread word rights s. True \<Longrightarrow> ?Q36 thread word rights s
 3. \<And>thread word rights s. (invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3)) s \<Longrightarrow> ?Q'36 thread word rights s
 4. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>thread word rights. (thread, tcb_caller_slot) = transform_cslot_ptr (thread, tcb_cnode_index 3)
 2. \<And>thread word rights s. True \<Longrightarrow> True
 3. \<And>thread word rights s. (invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3)) s \<Longrightarrow> (invs and tcb_at word and tcb_at thread and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (thread, tcb_cnode_index 3) and (\<lambda>s. not_idle_thread (cur_thread s) s) and not_idle_thread word and not_idle_thread thread and valid_etcbs) s
 4. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>thread word rights s. True \<Longrightarrow> True
 2. \<And>thread word rights s. (invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3)) s \<Longrightarrow> (invs and tcb_at word and tcb_at thread and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (thread, tcb_cnode_index 3) and (\<lambda>s. not_idle_thread (cur_thread s) s) and not_idle_thread word and not_idle_thread thread and valid_etcbs) s
 3. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread word rights s. (invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3)) s \<Longrightarrow> (invs and tcb_at word and tcb_at thread and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (thread, tcb_cnode_index 3) and (\<lambda>s. not_idle_thread (cur_thread s) s) and not_idle_thread word and not_idle_thread thread and valid_etcbs) s
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread word rights s. \<lbrakk>invs s; valid_etcbs s; ct_running s; tcb_at thread s; not_idle_thread thread s; cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> tcb_at word s \<and> cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (thread, tcb_cnode_index 3) s \<and> not_idle_thread word s
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>thread word rights s. \<lbrakk>invs s; valid_etcbs s; ct_running s; tcb_at thread s; not_idle_thread thread s; cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> caps_of_state s (?p49 thread word rights s) = Some (?cap49 thread word rights s)
 2. \<And>thread word rights s. \<lbrakk>invs s; valid_etcbs s; ct_running s; tcb_at thread s; not_idle_thread thread s; cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3) s; s \<turnstile> ?cap49 thread word rights s\<rbrakk> \<Longrightarrow> tcb_at word s \<and> cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (thread, tcb_cnode_index 3) s \<and> not_idle_thread word s
 3. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>thread word rights s. \<lbrakk>invs s; valid_etcbs s; ct_running s; tcb_at thread s; not_idle_thread thread s; caps_of_state s (thread, tcb_cnode_index 3) = Some (cap.ReplyCap word False rights)\<rbrakk> \<Longrightarrow> caps_of_state s (?p49 thread word rights s) = Some (?cap49 thread word rights s)
 2. \<And>thread word rights s. \<lbrakk>invs s; valid_etcbs s; ct_running s; tcb_at thread s; not_idle_thread thread s; cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3) s; s \<turnstile> ?cap49 thread word rights s\<rbrakk> \<Longrightarrow> tcb_at word s \<and> cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (thread, tcb_cnode_index 3) s \<and> not_idle_thread word s
 3. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread word rights s. \<lbrakk>invs s; valid_etcbs s; ct_running s; tcb_at thread s; not_idle_thread thread s; cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3) s; cap_aligned (cap.ReplyCap word False rights) \<and> tcb_at word s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (thread, tcb_cnode_index 3) s \<and> not_idle_thread word s
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread word rights s. \<lbrakk>valid_etcbs s; ct_running s; tcb_at thread s; not_idle_thread thread s; cte_wp_at ((=) (cap.ReplyCap word False rights)) (thread, tcb_cnode_index 3) s; valid_pspace s; cap_aligned (cap.ReplyCap word False rights); valid_mdb s; tcb_at word s; valid_ioc s; AllowWrite \<in> rights; valid_idle s; AllowRead \<notin> rights; AllowGrantReply \<notin> rights; only_idle s; if_unsafe_then_cap s; \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (thread, tcb_cnode_index 3) s \<and> not_idle_thread word s
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread word rights s. \<lbrakk>valid_etcbs s; ct_running s; tcb_at thread s; not_idle_thread thread s; fst (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) s) = {(cap.ReplyCap word False rights, s)}; valid_pspace s; cap_aligned (cap.ReplyCap word False rights); valid_mdb s; tcb_at word s; valid_ioc s; AllowWrite \<in> rights; valid_idle s; AllowRead \<notin> rights; AllowGrantReply \<notin> rights; only_idle s; if_unsafe_then_cap s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; has_reply_cap word s \<longrightarrow> st_tcb_at awaiting_reply word s\<rbrakk> \<Longrightarrow> not_idle_thread word s
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread rights s ko tcb. \<lbrakk>valid_etcbs s; ct_running s; thread \<noteq> idle_thread_ptr; fst (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) s) = {(cap.ReplyCap idle_thread_ptr False rights, s)}; valid_pspace s; cap_aligned (cap.ReplyCap idle_thread_ptr False rights); valid_mdb s; valid_ioc s; AllowWrite \<in> rights; AllowRead \<notin> rights; AllowGrantReply \<notin> rights; only_idle s; if_unsafe_then_cap s; unique_reply_caps (caps_of_state s); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>a b cap. fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)} \<longrightarrow> (\<forall>rights. cap \<noteq> cap.ReplyCap idle_thread_ptr False rights); idle_thread s = idle_thread_ptr; kheap s thread = Some ko; is_tcb ko; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> False
 2. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>thread. \<lbrace>?Q8 thread\<rbrace> KHeap_D.get_cap (thread, tcb_caller_slot) \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>thread. \<lbrace>?Q'8 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread and cte_wp_at ((=) cap) (thread, tcb_cnode_index 3)\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q8 thread\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. valid_idle and not_idle_thread (fst (thread, tcb_cnode_index 3)) and valid_etcbs and ?Q'8 thread\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. (invs and (\<lambda>s. not_idle_thread (cur_thread s) s \<and> ct_running s) and valid_etcbs) s \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; not_idle_thread (cur_thread s) s; ct_running s; valid_etcbs s\<rbrakk> \<Longrightarrow> valid_idle s \<and> ((\<exists>cap. cte_wp_at ((=) cap) (cur_thread s, tcb_cnode_index 3) s) \<longrightarrow> tcb_at (cur_thread s) s) proof (prove)
goal:
No subgoals!