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 (is_frame_cap cap \<and> reset_cap_asid cap = reset_cap_asid ipc_buffer_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 (rule hoare_name_pre_stateE) apply (clarsimp simp: tcb_update_ipc_buffer_def sep_any_All) apply (wp whenE_wp tcb_update_thread_slot_wp[sep_wandise] get_cap_rv[where cap=cap]) apply (rule hoare_allI) apply (rule hoare_impI) apply (clarsimp) apply (safe) apply (wp) apply (clarsimp simp: cdl_same_arch_obj_as_def) apply (clarsimp simp: cap_type_def split: cdl_cap.splits dest!:reset_cap_asid_cap_type) apply (wp tcb_empty_thread_slot_wpE[sep_wandise]) apply (clarsimp) apply (sep_cancel)+ apply (safe) apply (sep_solve)+ apply (clarsimp simp: cdl_same_arch_obj_as_def cap_type_def reset_cap_asid_def split: cdl_cap.splits dest!:reset_cap_asid_cap_type) 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 (is_frame_cap cap \<and> reset_cap_asid cap = reset_cap_asid ipc_buffer_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. \<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 K (is_frame_cap cap \<and> reset_cap_asid cap = reset_cap_asid ipc_buffer_cap)) s \<Longrightarrow> \<lbrace>(=) s\<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. \<And>s sz. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<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 (3 subgoals):
 1. \<And>s sz y. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 s sz y\<rbrace> corrupt_tcb_intent target_tcb \<lbrace>\<lambda>rv s. \<forall>c. reset_cap_asid c = reset_cap_asid cap \<longrightarrow> (if cdl_same_arch_obj_as ipc_buffer_cap c 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) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType)) 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)) s\<rbrace>
 2. \<And>s sz. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s sz\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>\<lambda>y sa. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R18 s sz y) sa \<and> ?P'14 s sz y sa\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s sz 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) s; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); s = sa\<rbrakk> \<Longrightarrow> ?Q5 s sz sa proof (prove)
goal (3 subgoals):
 1. \<And>s sz y c. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 s sz y\<rbrace> corrupt_tcb_intent target_tcb \<lbrace>\<lambda>rv s. reset_cap_asid c = reset_cap_asid cap \<longrightarrow> (if cdl_same_arch_obj_as ipc_buffer_cap c 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) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType)) 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)) s\<rbrace>
 2. \<And>s sz. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s sz\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>\<lambda>y sa. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R18 s sz y) sa \<and> ?P'14 s sz y sa\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s sz 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) s; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); s = sa\<rbrakk> \<Longrightarrow> ?Q5 s sz sa proof (prove)
goal (3 subgoals):
 1. \<And>s sz y c. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); reset_cap_asid c = reset_cap_asid cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 s sz y\<rbrace> corrupt_tcb_intent target_tcb \<lbrace>\<lambda>rv. if cdl_same_arch_obj_as ipc_buffer_cap c 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) and K (cap_type ipc_buffer_cap \<noteq> Some UntypedType)) 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>
 2. \<And>s sz. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s sz\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>\<lambda>y sa. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R18 s sz y) sa \<and> ?P'14 s sz y sa\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s sz 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) s; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); s = sa\<rbrakk> \<Longrightarrow> ?Q5 s sz sa proof (prove)
goal (3 subgoals):
 1. \<And>s sz c. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); reset_cap_asid c = reset_cap_asid ipc_buffer_cap\<rbrakk> \<Longrightarrow> (cdl_same_arch_obj_as ipc_buffer_cap c \<longrightarrow> \<lbrace>?P'14 s sz ()\<rbrace> corrupt_tcb_intent target_tcb \<lbrace>\<lambda>rv a. 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)) a \<and> cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrace>) \<and> (\<not> cdl_same_arch_obj_as ipc_buffer_cap c \<longrightarrow> \<lbrace>?P'14 s sz ()\<rbrace> corrupt_tcb_intent target_tcb \<lbrace>\<lambda>rv. 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>)
 2. \<And>s sz. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s sz\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>\<lambda>y sa. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R18 s sz y) sa \<and> ?P'14 s sz y sa\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s sz 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) s; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); s = sa\<rbrakk> \<Longrightarrow> ?Q5 s sz sa proof (prove)
goal (4 subgoals):
 1. \<And>s sz c. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); reset_cap_asid c = reset_cap_asid ipc_buffer_cap; cdl_same_arch_obj_as ipc_buffer_cap c\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 s sz ()\<rbrace> corrupt_tcb_intent target_tcb \<lbrace>\<lambda>rv a. 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)) a \<and> cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrace>
 2. \<And>s sz c. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); reset_cap_asid c = reset_cap_asid ipc_buffer_cap; \<not> cdl_same_arch_obj_as ipc_buffer_cap c\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 s sz ()\<rbrace> corrupt_tcb_intent target_tcb \<lbrace>\<lambda>rv. 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>
 3. \<And>s sz. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s sz\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>\<lambda>y sa. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R18 s sz y) sa \<and> ?P'14 s sz y sa\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>s sz 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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> ?Q5 sa sz sa proof (prove)
goal (3 subgoals):
 1. \<And>s sz c. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); reset_cap_asid c = reset_cap_asid ipc_buffer_cap; \<not> cdl_same_arch_obj_as ipc_buffer_cap c\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. 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)) a \<and> cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrace> corrupt_tcb_intent target_tcb \<lbrace>\<lambda>rv. 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>
 2. \<And>s sz. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s sz\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>\<lambda>y sa. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R18 s sz y) 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 \<and> cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s sz 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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> ?Q5 sa sz sa proof (prove)
goal (3 subgoals):
 1. \<And>s sz c. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); reset_cap_asid c = reset_cap_asid ipc_buffer_cap; \<not> (case ipc_buffer_cap of FrameCap dev ra x sa xa xb \<Rightarrow> case c of FrameCap dev' rb x sb xa xb \<Rightarrow> rb = ra \<and> sb = sa \<and> dev = dev' | _ \<Rightarrow> False | PageTableCap a x xa \<Rightarrow> case c of PageTableCap b x xa \<Rightarrow> b = a | _ \<Rightarrow> False | PageDirectoryCap a x xa \<Rightarrow> case c of PageDirectoryCap b x xa \<Rightarrow> b = a | _ \<Rightarrow> False | AsidControlCap \<Rightarrow> case c of AsidControlCap \<Rightarrow> True | _ \<Rightarrow> False | AsidPoolCap x xa \<Rightarrow> case c of AsidPoolCap y xa \<Rightarrow> y = x | _ \<Rightarrow> False | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. 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)) a \<and> cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrace> corrupt_tcb_intent target_tcb \<lbrace>\<lambda>rv. 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>
 2. \<And>s sz. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s sz\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>\<lambda>y sa. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R18 s sz y) 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 \<and> cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s sz 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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> ?Q5 sa sz sa proof (prove)
goal (2 subgoals):
 1. \<And>s sz. \<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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s sz\<rbrace> tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot \<lbrace>\<lambda>y sa. cdl.lift (ipc_buffer_slot \<mapsto>c cap \<and>* ?R18 s sz y) 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 \<and> cap_type ipc_buffer_cap \<noteq> Some UntypedType\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s sz 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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<rbrakk> \<Longrightarrow> ?Q5 sa sz sa proof (prove)
goal (1 subgoal):
 1. \<And>s sz 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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<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>* ?R448 sa sz) 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 \<and> cap_type ipc_buffer_cap \<noteq> Some UntypedType))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sz 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; reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz)\<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>* ?R448 sa sz) 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 \<and> cap_type ipc_buffer_cap \<noteq> Some UntypedType))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sz sa s sb. \<lbrakk>reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); ((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>* ?R448 sa sz) 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 \<and> cap_type ipc_buffer_cap \<noteq> Some UntypedType proof (prove)
goal (3 subgoals):
 1. \<And>sz sa s sb. \<lbrakk>reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); ((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>* ?R448 sa sz) sb
 2. \<And>sz sa s sb. \<lbrakk>reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); ((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
 3. \<And>sz sa s sb. \<lbrakk>reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); ((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; is_untyped_cap ipc_buffer_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>sz sa s sb. \<lbrakk>reset_cap_asid cap = reset_cap_asid ipc_buffer_cap; cap_type cap = Some (FrameType sz); ((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; is_untyped_cap ipc_buffer_cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!