theory Tcb_DR

lemma dcorres_setup_reply_master:
  "dcorres dc \<top> (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs)
             (KHeap_D.set_cap (obj_id, tcb_replycap_slot)
               (cdl_cap.MasterReplyCap obj_id))
             (setup_reply_master obj_id)" apply (clarsimp simp:setup_reply_master_def) apply (rule_tac Q'="\<lambda>rv. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and
     cte_wp_at (\<lambda>c. c = rv) (obj_id,tcb_cnode_index 2)" in corres_symb_exec_r) prefer 2 apply (wp get_cap_cte_wp_at) apply (rule dcorres_expand_pfx) apply (clarsimp simp:tcb_at_def) apply (frule valid_tcb_objs) apply (simp add:tcb_at_def) apply (clarsimp simp:cte_wp_at_cases dest!:get_tcb_SomeD) apply (clarsimp simp:valid_tcb_def) apply (clarsimp simp:tcb_cap_cases_def) apply (case_tac "cap.NullCap = tcb_reply tcb") apply (clarsimp simp:when_def) apply (rule corres_guard_imp) apply (rule dcorres_symb_exec_r) apply (rule set_cap_corres) apply (clarsimp simp:transform_cap_def) apply (clarsimp simp:transform_tcb_slot_simp) apply (wp+)[2] apply (clarsimp simp:transform_def transform_current_thread_def) apply (rule TrueI) apply (clarsimp simp: not_idle_thread_def) apply (clarsimp simp:when_def is_master_reply_cap_def split:cap.split_asm) apply (rename_tac rc_rights) apply (subgoal_tac "opt_cap (obj_id,tcb_replycap_slot) (transform s')
      = Some (cdl_cap.MasterReplyCap obj_id)") apply (clarsimp simp:corres_underlying_def set_cap_is_noop_opt_cap return_def) apply (subgoal_tac "cte_wp_at ((=)  (cap.ReplyCap obj_id True rc_rights))
      (obj_id,tcb_cnode_index 2) s'") apply (clarsimp dest!:iffD1[OF cte_wp_at_caps_of_state]) apply (drule caps_of_state_transform_opt_cap) apply simp apply (clarsimp simp:not_idle_thread_def) apply (simp add:transform_cap_def transform_tcb_slot_simp) apply (clarsimp simp:cte_wp_at_cases) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (setup_reply_master obj_id) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (do old_cap <- CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2);
when (old_cap = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od)
od) proof (prove)
goal (4 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and cte_wp_at (\<lambda>c. c = rv) (obj_id, tcb_cnode_index 2)) (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (rv = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 2. \<lbrace>valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>rv. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and cte_wp_at (\<lambda>c. c = rv) (obj_id, tcb_cnode_index 2)\<rbrace>
 3. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (4 subgoals):
 1. \<lbrace>valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>rv. valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and cte_wp_at (\<lambda>c. c = rv) (obj_id, tcb_cnode_index 2)\<rbrace>
 2. \<And>rv. dcorres dc (\<lambda>_. True) (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and cte_wp_at (\<lambda>c. c = rv) (obj_id, tcb_cnode_index 2)) (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (rv = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 3. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and cte_wp_at (\<lambda>c. c = rv) (obj_id, tcb_cnode_index 2)) (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (rv = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>rv s s'. \<lbrakk>s = transform s'; True; (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs and cte_wp_at (\<lambda>c. c = rv) (obj_id, tcb_cnode_index 2)) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (rv = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>rv s' tcb. \<lbrakk>valid_objs s'; get_tcb obj_id s' = Some tcb; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; cte_wp_at (\<lambda>c. c = rv) (obj_id, tcb_cnode_index 2) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (rv = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (4 subgoals):
 1. \<And>rv s' tcb. \<lbrakk>valid_objs s'; get_tcb obj_id s' = Some tcb; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; cte_wp_at (\<lambda>c. c = rv) (obj_id, tcb_cnode_index 2) s'\<rbrakk> \<Longrightarrow> get_tcb (?thread20 rv s' tcb) s' = Some (?y20 rv s' tcb)
 2. \<And>rv s' tcb. \<lbrakk>valid_objs s'; get_tcb obj_id s' = Some tcb; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; cte_wp_at (\<lambda>c. c = rv) (obj_id, tcb_cnode_index 2) s'; valid_tcb (?thread20 rv s' tcb) (?y20 rv s' tcb) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (rv = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 3. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>rv s' tcb. \<lbrakk>valid_objs s'; get_tcb obj_id s' = Some tcb; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; cte_wp_at (\<lambda>c. c = rv) (obj_id, tcb_cnode_index 2) s'; valid_tcb obj_id tcb s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (rv = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; valid_tcb obj_id tcb s'; kheap s' obj_id = Some (TCB tcb)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB 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); valid_tcb_state (tcb_state tcb) s'; 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> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (4 subgoals):
 1. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 2. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 3. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (4 subgoals):
 1. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od)
 2. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 3. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (6 subgoals):
 1. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc (?Q48 s' tcb) (?Q'48 s' tcb) (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od)
 2. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; transform s' = s\<rbrakk> \<Longrightarrow> ?Q48 s' tcb s
 3. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; s' = s\<rbrakk> \<Longrightarrow> ?Q'48 s' tcb s
 4. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 5. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (8 subgoals):
 1. \<And>s' tcb rv. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc (?Q48 s' tcb) (?Q'52 s' tcb rv) (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2))
 2. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 s' tcb\<rbrace> set_original (obj_id, tcb_cnode_index 2) True \<lbrace>?Q'52 s' tcb\<rbrace>
 3. \<And>s' tcb cs. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_original (obj_id, tcb_cnode_index 2) True \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; transform s' = s\<rbrakk> \<Longrightarrow> ?Q48 s' tcb s
 5. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; s' = s\<rbrakk> \<Longrightarrow> ?Q'48 s' tcb s
 6. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 7. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (9 subgoals):
 1. \<And>s' tcb rv. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> MasterReplyCap obj_id = transform_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite})
 2. \<And>s' tcb rv. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> (obj_id, tcb_replycap_slot) = transform_cslot_ptr (obj_id, tcb_cnode_index 2)
 3. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 s' tcb\<rbrace> set_original (obj_id, tcb_cnode_index 2) True \<lbrace>\<lambda>r s. valid_idle s \<and> fst (obj_id, tcb_cnode_index 2) \<noteq> idle_thread s \<and> valid_etcbs s\<rbrace>
 4. \<And>s' tcb cs. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_original (obj_id, tcb_cnode_index 2) True \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; transform s' = s\<rbrakk> \<Longrightarrow> True
 6. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; s' = s\<rbrakk> \<Longrightarrow> ?Q'48 s' tcb s
 7. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 8. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (8 subgoals):
 1. \<And>s' tcb rv. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> (obj_id, tcb_replycap_slot) = transform_cslot_ptr (obj_id, tcb_cnode_index 2)
 2. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 s' tcb\<rbrace> set_original (obj_id, tcb_cnode_index 2) True \<lbrace>\<lambda>r s. valid_idle s \<and> fst (obj_id, tcb_cnode_index 2) \<noteq> idle_thread s \<and> valid_etcbs s\<rbrace>
 3. \<And>s' tcb cs. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_original (obj_id, tcb_cnode_index 2) True \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; transform s' = s\<rbrakk> \<Longrightarrow> True
 5. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; s' = s\<rbrakk> \<Longrightarrow> ?Q'48 s' tcb s
 6. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 7. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (7 subgoals):
 1. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 s' tcb\<rbrace> set_original (obj_id, tcb_cnode_index 2) True \<lbrace>\<lambda>r s. valid_idle s \<and> fst (obj_id, tcb_cnode_index 2) \<noteq> idle_thread s \<and> valid_etcbs s\<rbrace>
 2. \<And>s' tcb cs. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_original (obj_id, tcb_cnode_index 2) True \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; transform s' = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; s' = s\<rbrakk> \<Longrightarrow> ?Q'48 s' tcb s
 5. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 6. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (6 subgoals):
 1. \<And>s' tcb cs s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; transform s = cs\<rbrakk> \<Longrightarrow> transform (s\<lparr>is_original_cap := (is_original_cap s)((obj_id, tcb_cnode_index 2) := True)\<rparr>) = cs
 2. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; transform s' = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; s' = s\<rbrakk> \<Longrightarrow> valid_idle (s\<lparr>is_original_cap := (is_original_cap s)((obj_id, tcb_cnode_index 2) := True)\<rparr>) \<and> fst (obj_id, tcb_cnode_index 2) \<noteq> idle_thread (s\<lparr>is_original_cap := (is_original_cap s)((obj_id, tcb_cnode_index 2) := True)\<rparr>) \<and> valid_etcbs (s\<lparr>is_original_cap := (is_original_cap s)((obj_id, tcb_cnode_index 2) := True)\<rparr>)
 4. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 5. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (5 subgoals):
 1. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; s' = s\<rbrakk> \<Longrightarrow> valid_idle (s\<lparr>is_original_cap := (is_original_cap s)((obj_id, tcb_cnode_index 2) := True)\<rparr>) \<and> fst (obj_id, tcb_cnode_index 2) \<noteq> idle_thread (s\<lparr>is_original_cap := (is_original_cap s)((obj_id, tcb_cnode_index 2) := True)\<rparr>) \<and> valid_etcbs (s\<lparr>is_original_cap := (is_original_cap s)((obj_id, tcb_cnode_index 2) := True)\<rparr>)
 3. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 4. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (4 subgoals):
 1. \<And>s' tcb s. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); halted (tcb_state tcb); s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap = tcb_reply tcb; s' = s\<rbrakk> \<Longrightarrow> valid_idle (s\<lparr>is_original_cap := (is_original_cap s)((obj_id, tcb_cnode_index 2) := True)\<rparr>) \<and> fst (obj_id, tcb_cnode_index 2) \<noteq> idle_thread (s\<lparr>is_original_cap := (is_original_cap s)((obj_id, tcb_cnode_index 2) := True)\<rparr>) \<and> valid_etcbs (s\<lparr>is_original_cap := (is_original_cap s)((obj_id, tcb_cnode_index 2) := True)\<rparr>)
 2. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 3. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb. \<lbrakk>valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; 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'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> tcb_reply tcb; is_master_reply_cap (tcb_reply tcb) \<and> obj_ref_of (tcb_reply tcb) = obj_id \<and> AllowGrant \<in> Structures_A.cap_rights (tcb_reply tcb) \<or> halted (tcb_state tcb) \<and> tcb_reply tcb = cap.NullCap; s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; cap.NullCap \<noteq> tcb_reply tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (when (tcb_reply tcb = cap.NullCap) (do y <- set_original (obj_id, tcb_cnode_index 2) True;
CSpaceAcc_A.set_cap (cap.ReplyCap obj_id True {AllowGrant, AllowWrite}) (obj_id, tcb_cnode_index 2)
od))
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb x52 x53. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True x53; tcb_reply tcb = cap.ReplyCap obj_id True x53; x52; AllowGrant \<in> x53\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (return ())
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (return ())
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (4 subgoals):
 1. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights; opt_cap (obj_id, tcb_replycap_slot) (transform s') = Some (MasterReplyCap obj_id)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (obj_id, tcb_replycap_slot) (MasterReplyCap obj_id)) (return ())
 2. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) (transform s') = Some (MasterReplyCap obj_id)
 3. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) (transform s') = Some (MasterReplyCap obj_id)
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (4 subgoals):
 1. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights; cte_wp_at ((=) (cap.ReplyCap obj_id True rc_rights)) (obj_id, tcb_cnode_index 2) s'\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) (transform s') = Some (MasterReplyCap obj_id)
 2. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (cap.ReplyCap obj_id True rc_rights)) (obj_id, tcb_cnode_index 2) s'
 3. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (4 subgoals):
 1. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights; caps_of_state s' (obj_id, tcb_cnode_index 2) = Some (cap.ReplyCap obj_id True rc_rights)\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) (transform s') = Some (MasterReplyCap obj_id)
 2. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (cap.ReplyCap obj_id True rc_rights)) (obj_id, tcb_cnode_index 2) s'
 3. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (6 subgoals):
 1. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> valid_etcbs s'
 2. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> fst (obj_id, tcb_cnode_index 2) \<noteq> idle_thread s'
 3. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights; opt_cap (transform_cslot_ptr (obj_id, tcb_cnode_index 2)) (transform s') = Some (transform_cap (cap.ReplyCap obj_id True rc_rights))\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) (transform s') = Some (MasterReplyCap obj_id)
 4. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (cap.ReplyCap obj_id True rc_rights)) (obj_id, tcb_cnode_index 2) s'
 5. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (5 subgoals):
 1. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> fst (obj_id, tcb_cnode_index 2) \<noteq> idle_thread s'
 2. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights; opt_cap (transform_cslot_ptr (obj_id, tcb_cnode_index 2)) (transform s') = Some (transform_cap (cap.ReplyCap obj_id True rc_rights))\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) (transform s') = Some (MasterReplyCap obj_id)
 3. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (cap.ReplyCap obj_id True rc_rights)) (obj_id, tcb_cnode_index 2) s'
 4. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (4 subgoals):
 1. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights; opt_cap (transform_cslot_ptr (obj_id, tcb_cnode_index 2)) (transform s') = Some (transform_cap (cap.ReplyCap obj_id True rc_rights))\<rbrakk> \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) (transform s') = Some (MasterReplyCap obj_id)
 2. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (cap.ReplyCap obj_id True rc_rights)) (obj_id, tcb_cnode_index 2) s'
 3. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb x52 rc_rights. \<lbrakk>s' \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> cap.NullCap = tcb_vtable tcb; s' \<turnstile> tcb_ctable tcb; valid_objs s'; not_idle_thread obj_id s'; valid_idle s'; valid_etcbs s'; kheap s' obj_id = Some (TCB tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s'; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s'; valid_arch_tcb (tcb_arch tcb) s'; s' \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> cap.NullCap = tcb_ipcframe tcb; s' \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap) (tcb_caller tcb); s' \<turnstile> cap.ReplyCap obj_id True rc_rights; tcb_reply tcb = cap.ReplyCap obj_id True rc_rights; x52; AllowGrant \<in> rc_rights\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (cap.ReplyCap obj_id True rc_rights)) (obj_id, tcb_cnode_index 2) s'
 2. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal (1 subgoal):
 1. False \<Longrightarrow> no_fail (valid_objs and tcb_at obj_id and not_idle_thread obj_id and valid_idle and valid_etcbs) (CSpaceAcc_A.get_cap (obj_id, tcb_cnode_index 2)) proof (prove)
goal:
No subgoals!