theory IpcCancel_AI

lemma reply_cancel_ipc_bound_tcb_at[wp]:
  "\<lbrace>bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p \<rbrace>
    reply_cancel_ipc p
   \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace>" unfolding reply_cancel_ipc_def apply (wpsimp wp: cap_delete_one_bound_tcb_at select_inv) apply (rule_tac Q="\<lambda>_. bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p" in  hoare_strengthen_post) apply (wpsimp wp: thread_set_no_change_tcb_pred thread_set_mdb) apply (fastforce simp:tcb_cap_cases_def) apply (wpsimp wp: thread_set_valid_objs_triv simp: ran_tcb_cap_cases) apply clarsimp apply (frule valid_mdb_impl_reply_masters) apply (clarsimp simp: reply_masters_mdb_def) apply (spec p) apply (spec "tcb_cnode_index 2") apply (spec p) apply (clarsimp simp:tcb_at_def) apply (frule(1) valid_tcb_objs) apply (clarsimp simp: valid_tcb_def) apply (erule impE) apply (simp add: caps_of_state_tcb_index_trans tcb_cnode_map_def) apply (clarsimp simp: tcb_cap_cases_def is_master_reply_cap_def split:cap.splits  ) apply (subgoal_tac "descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {}") prefer 2 apply simp apply (drule descendants_of_nullcap, simp) apply (simp add: caps_of_state_tcb_index_trans tcb_cnode_map_def) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p\<rbrace> reply_cancel_ipc p \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p\<rbrace> do thread_set (tcb_fault_update (\<lambda>_. None)) p;
cap <- get_cap (p, tcb_cnode_index 2);
descs <- gets (descendants_of (p, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) $ do assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od
od \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) p \<lbrace>\<lambda>x s. (descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (p, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> bound_tcb_at P t s \<and> (\<forall>x\<in>descendants_of (p, tcb_cnode_index 2) (cdt s). \<exists>t b R. caps_of_state s x = Some (ReplyCap t b R))) \<and> (descendants_of (p, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> bound_tcb_at P t s)\<rbrace>
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q1\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) p \<lbrace>\<lambda>_. bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p\<rbrace>
 2. \<And>rv s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> (descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (p, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> bound_tcb_at P t s \<and> (\<forall>x\<in>descendants_of (p, tcb_cnode_index 2) (cdt s). \<exists>t b R. caps_of_state s x = Some (ReplyCap t b R))) \<and> (descendants_of (p, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> bound_tcb_at P t s)
 3. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>t getF a b. (getF, a, b) \<in> ran tcb_cap_cases \<Longrightarrow> getF (t\<lparr>tcb_fault := None\<rparr>) = getF t
 2. \<lbrace>?P'40\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) p \<lbrace>\<lambda>rv s. valid_objs s \<and> tcb_at p s\<rbrace>
 3. \<And>rv s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> (descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (p, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> bound_tcb_at P t s \<and> (\<forall>x\<in>descendants_of (p, tcb_cnode_index 2) (cdt s). \<exists>t b R. caps_of_state s x = Some (ReplyCap t b R))) \<and> (descendants_of (p, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> bound_tcb_at P t s)
 4. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> ?P'40 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'40\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) p \<lbrace>\<lambda>rv s. valid_objs s \<and> tcb_at p s\<rbrace>
 2. \<And>rv s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> (descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (p, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> bound_tcb_at P t s \<and> (\<forall>x\<in>descendants_of (p, tcb_cnode_index 2) (cdt s). \<exists>t b R. caps_of_state s x = Some (ReplyCap t b R))) \<and> (descendants_of (p, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> bound_tcb_at P t s)
 3. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> ?P'40 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> (descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (p, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> bound_tcb_at P t s \<and> (\<forall>x\<in>descendants_of (p, tcb_cnode_index 2) (cdt s). \<exists>t b R. caps_of_state s x = Some (ReplyCap t b R))) \<and> (descendants_of (p, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> bound_tcb_at P t s)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; tcb_at p s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; tcb_at p s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; reply_masters_mdb (cdt s) (caps_of_state s)\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; tcb_at p s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; \<forall>a b t. (\<exists>rights. caps_of_state s (a, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (a, b) = None \<and> (\<forall>ptr'\<in>descendants_of (a, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; tcb_at p s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; \<forall>b t. (\<exists>rights. caps_of_state s (p, b) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (p, b) = None \<and> (\<forall>ptr'\<in>descendants_of (p, b) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; tcb_at p s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; \<forall>t. (\<exists>rights. caps_of_state s (p, tcb_cnode_index 2) = Some (ReplyCap t True rights)) \<longrightarrow> cdt s (p, tcb_cnode_index 2) = None \<and> (\<forall>ptr'\<in>descendants_of (p, tcb_cnode_index 2) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; tcb_at p s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; (\<exists>rights. caps_of_state s (p, tcb_cnode_index 2) = Some (ReplyCap p True rights)) \<longrightarrow> cdt s (p, tcb_cnode_index 2) = None \<and> (\<forall>ptr'\<in>descendants_of (p, tcb_cnode_index 2) (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap p False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; (\<exists>rights. caps_of_state s (p, tcb_cnode_index 2) = Some (ReplyCap p True rights)) \<longrightarrow> cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights')); get_tcb p s = Some tcb\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; (\<exists>rights. caps_of_state s (p, tcb_cnode_index 2) = Some (ReplyCap p True rights)) \<longrightarrow> cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights')); get_tcb p s = Some tcb; valid_tcb p tcb s\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; (\<exists>rights. caps_of_state s (p, tcb_cnode_index 2) = Some (ReplyCap p True rights)) \<longrightarrow> cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights')); get_tcb p s = Some 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 p (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> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (3 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some 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 p (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> \<exists>rights. caps_of_state s (p, tcb_cnode_index 2) = Some (ReplyCap p True rights)
 2. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some 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 p (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; cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 3. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (3 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some 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 p (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> \<exists>rights. tcb_reply tcb = ReplyCap p True rights
 2. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some 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 p (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; cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 3. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (3 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>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; bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some tcb; tcb_reply tcb = NullCap; s \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> NullCap = tcb_ipcframe tcb; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); halted (tcb_state tcb); s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_ctable tcb\<rbrakk> \<Longrightarrow> False
 2. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some 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 p (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; cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 3. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (4 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>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; bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some tcb; tcb_reply tcb = NullCap; s \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> NullCap = tcb_ipcframe tcb; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); halted (tcb_state tcb); s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_ctable tcb; descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s b aa tcb. \<lbrakk>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; bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some tcb; tcb_reply tcb = NullCap; s \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> NullCap = tcb_ipcframe tcb; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); halted (tcb_state tcb); s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_ctable tcb\<rbrakk> \<Longrightarrow> descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {}
 3. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some 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 p (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; cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 4. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (4 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>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; bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some tcb; tcb_reply tcb = NullCap; s \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> NullCap = tcb_ipcframe tcb; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); halted (tcb_state tcb); s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_ctable tcb\<rbrakk> \<Longrightarrow> descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {}
 2. \<And>s b aa tcb. \<lbrakk>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; bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some tcb; tcb_reply tcb = NullCap; s \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> NullCap = tcb_ipcframe tcb; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); halted (tcb_state tcb); s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_ctable tcb; descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some 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 p (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; cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 4. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (3 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>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; bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some tcb; tcb_reply tcb = NullCap; s \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> NullCap = tcb_ipcframe tcb; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); halted (tcb_state tcb); s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_ctable tcb; descendants_of (p, tcb_cnode_index 2) (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some 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 p (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; cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 3. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (3 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>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; bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some tcb; tcb_reply tcb = NullCap; s \<turnstile> tcb_ipcframe tcb; is_nondevice_page_cap (tcb_ipcframe tcb) \<or> NullCap = tcb_ipcframe tcb; s \<turnstile> tcb_caller tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller tcb); halted (tcb_state tcb); s \<turnstile> tcb_vtable tcb; is_valid_vtable_root (tcb_vtable tcb) \<or> NullCap = tcb_vtable tcb; s \<turnstile> tcb_ctable tcb; caps_of_state s (p, tcb_cnode_index 2) \<noteq> Some NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some 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 p (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; cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 3. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa tcb. \<lbrakk>bound_tcb_at P t s; valid_mdb s; valid_objs s; descendants_of (p, tcb_cnode_index 2) (cdt s) = {(aa, b)}; get_tcb p s = Some 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 p (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; cdt s (p, tcb_cnode_index 2) = None \<and> (\<exists>rights'. caps_of_state s (aa, b) = Some (ReplyCap p False rights'))\<rbrakk> \<Longrightarrow> \<exists>t ba R. caps_of_state s (aa, b) = Some (ReplyCap t ba R)
 2. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal (1 subgoal):
 1. \<And>s. (bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p) s \<Longrightarrow> bound_tcb_at P t s \<and> valid_mdb s \<and> valid_objs s \<and> tcb_at p s proof (prove)
goal:
No subgoals!