theory TCB_DP

lemma tcb_update_ipc_buffer_wp:
"\<lbrace>< (ipc_buffer_slot) \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c (TcbCap target_tcb) \<and>* R>
    and K (\<not> is_untyped_cap (ipc_buffer_cap) \<and>  ~is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)\<rbrace>
 tcb_update_ipc_buffer target_tcb tcb_cap_slot (ipc_buffer_cap, ipc_buffer_slot)
\<lbrace>\<lambda>_. <(target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c (TcbCap target_tcb) \<and>* (ipc_buffer_slot) \<mapsto>c cap \<and>* R>\<rbrace>, \<lbrace>E\<rbrace>" apply (clarsimp simp: tcb_update_ipc_buffer_def sep_any_All) apply (rule hoare_name_pre_stateE) apply (wp whenE_wp tcb_update_thread_slot_wp[sep_wand_side_wpE]) apply (clarsimp) apply (wp get_cap_rv'[where cap=cap]) apply (clarsimp) apply (wp) apply (wp tcb_empty_thread_slot_wpE[sep_wandise]) apply (clarsimp simp: pred_conj_def) apply (sep_cancel) apply (sep_cancel) apply (safe) apply (sep_solve)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)\<rbrace> tcb_update_ipc_buffer target_tcb tcb_cap_slot (ipc_buffer_cap, ipc_buffer_slot) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)\<rbrace> doE y <- tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot;
y <- liftE (corrupt_tcb_intent target_tcb);
src_cap <- liftE (get_cap ipc_buffer_slot);
whenE (cdl_same_arch_obj_as ipc_buffer_cap src_cap) (tcb_update_thread_slot target_tcb tcb_cap_slot tcb_ipcbuffer_slot (ipc_buffer_cap, ipc_buffer_slot))
odE \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot;
y <- liftE (corrupt_tcb_intent target_tcb);
src_cap <- liftE (get_cap ipc_buffer_slot);
whenE (cdl_same_arch_obj_as ipc_buffer_cap src_cap) (tcb_update_thread_slot target_tcb tcb_cap_slot tcb_ipcbuffer_slot (ipc_buffer_cap, ipc_buffer_slot))
odE \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s y ya src_cap. \<lbrakk>(cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s; cdl_same_arch_obj_as ipc_buffer_cap src_cap\<rbrakk> \<Longrightarrow> cap_type ipc_buffer_cap \<noteq> Some UntypedType
 2. \<And>s y ya. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>?B4 s y ya\<rbrace> liftE (get_cap ipc_buffer_slot) \<lbrace>\<lambda>src_cap. if cdl_same_arch_obj_as ipc_buffer_cap src_cap then cdl.lift (((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) else cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s y. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>?B3 s y\<rbrace> liftE (corrupt_tcb_intent target_tcb) \<lbrace>?B4 s y\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>s. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>?B3 s\<rbrace>, \<lbrace>E\<rbrace>
 5. \<And>s sa. \<lbrakk>(cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s y ya. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>?B4 s y ya\<rbrace> liftE (get_cap ipc_buffer_slot) \<lbrace>\<lambda>src_cap. if cdl_same_arch_obj_as ipc_buffer_cap src_cap then cdl.lift (((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) else cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s y. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>?B3 s y\<rbrace> liftE (corrupt_tcb_intent target_tcb) \<lbrace>?B4 s y\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>?B3 s\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>s sa. \<lbrakk>(cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s y. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>?B3 s y\<rbrace> liftE (corrupt_tcb_intent target_tcb) \<lbrace>\<lambda>ya sa. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R10 s y ya) sa \<and> (if cdl_same_arch_obj_as ipc_buffer_cap cap then cdl.lift (((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) else cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) sa \<and> \<not> is_memory_cap cap\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>?B3 s\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s sa. \<lbrakk>(cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type ipc_buffer_cap \<noteq> Some UntypedType; \<not> is_memory_cap cap; cdl_same_arch_obj_as ipc_buffer_cap cap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 s ()\<rbrace> corrupt_tcb_intent target_tcb \<lbrace>\<lambda>ya sa. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R10 s () ()) sa \<and> cdl.lift (((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) sa\<rbrace>
 2. \<And>s. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>?B3 s\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s sa. \<lbrakk>(cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>\<lambda>a b. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R23 s a) b \<and> cdl.lift (((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) b\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s sa. \<lbrakk>(cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa
flex-flex pairs:
\<lambda>s. ?R23 s () \<equiv>\<^sup>? \<lambda>s. ?R10 s () () proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and (\<lambda>y. cap_type ipc_buffer_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap cap \<and> cdl_same_arch_obj_as ipc_buffer_cap cap)) s; s = sa\<rbrakk> \<Longrightarrow> cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<longrightarrow>* (\<lambda>a. (ipc_buffer_slot \<mapsto>c cap \<and>* ?R10 s () ()) a \<and> (((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) a))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sa; cap_type ipc_buffer_cap \<noteq> Some UntypedType; \<not> is_memory_cap cap; cdl_same_arch_obj_as ipc_buffer_cap cap\<rbrakk> \<Longrightarrow> cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<longrightarrow>* (\<lambda>a. (ipc_buffer_slot \<mapsto>c cap \<and>* ?R10 sa () ()) a \<and> (((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) a))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa s. \<lbrakk>cap_type ipc_buffer_cap \<noteq> Some UntypedType; \<not> is_memory_cap cap; cdl_same_arch_obj_as ipc_buffer_cap cap; (ipc_buffer_slot \<mapsto>c cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<longrightarrow>* (\<lambda>a. (ipc_buffer_slot \<mapsto>c cap \<and>* ?R10 sa () ()) a \<and> ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) a)) s proof (prove)
goal (1 subgoal):
 1. \<And>sa s sb. \<lbrakk>cap_type ipc_buffer_cap \<noteq> Some UntypedType; \<not> is_memory_cap cap; cdl_same_arch_obj_as ipc_buffer_cap cap; ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sb\<rbrakk> \<Longrightarrow> (ipc_buffer_slot \<mapsto>c cap \<and>* ?R10 sa () ()) sb \<and> ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) sb proof (prove)
goal (2 subgoals):
 1. \<And>sa s sb. \<lbrakk>cap_type ipc_buffer_cap \<noteq> Some UntypedType; \<not> is_memory_cap cap; cdl_same_arch_obj_as ipc_buffer_cap cap; ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sb\<rbrakk> \<Longrightarrow> (ipc_buffer_slot \<mapsto>c cap \<and>* ?R10 sa () ()) sb
 2. \<And>sa s sb. \<lbrakk>cap_type ipc_buffer_cap \<noteq> Some UntypedType; \<not> is_memory_cap cap; cdl_same_arch_obj_as ipc_buffer_cap cap; ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sb\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipc_buffer_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipc_buffer_slot \<mapsto>c cap \<and>* R)) sb proof (prove)
goal:
No subgoals!