theory TCB_DP

lemma invoke_tcb_threadcontrol_wp:
"\<lbrace>< target_tcb \<mapsto>f Tcb tcb \<and>*
  (vrt_slot) \<mapsto>c vrt_cap'  \<and>*
  (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>*
  tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>*
  (crt_slot) \<mapsto>c crt_cap'  \<and>*
  (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>*
  (ipcbuff_slot) \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>*
  R> and
  K ( faultep = Some fltep \<and>
  croot = Some (crt_cap, crt_slot) \<and>
  vroot = Some (vrt_cap, vrt_slot) \<and>
  ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot) \<and>
  \<not> is_untyped_cap (vrt_cap) \<and> \<not> is_untyped_cap (crt_cap) \<and> \<not> is_untyped_cap (ipcbuff_cap) \<and>
  ~is_memory_cap (vrt_cap') \<and> \<not> is_memory_cap (crt_cap') \<and>  ~is_memory_cap (ipcbuff_cap') \<and>
  cdl_same_arch_obj_as vrt_cap vrt_cap' \<and> cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap' \<and>
  is_cnode_cap crt_cap' \<and> cap_object crt_cap = cap_object crt_cap') \<rbrace>
 invoke_tcb  (ThreadControl target_tcb tcb_cap_slot faultep croot vroot ipc_buffer)
\<lbrace>\<lambda>_.  <(target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>*
       tcb_cap_slot \<mapsto>c (TcbCap target_tcb)   \<and>*
       (ipcbuff_slot) \<mapsto>c ipcbuff_cap'                    \<and>*
       (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap    \<and>*
       (vrt_slot) \<mapsto>c vrt_cap'                        \<and>*
       (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap    \<and>*
       (crt_slot) \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R >\<rbrace>, \<lbrace>E\<rbrace> " apply (rule hoare_name_pre_stateE) apply (clarsimp simp: invoke_tcb_def) apply (wp) apply (wp tcb_update_ipc_buffer_wp[sep_wand_side_wpE]) apply (fastforce) apply (wp set_cdl_tcb_fault_endpoint_wp[sep_wand_wp]
      tcb_update_ipc_buffer_wp[sep_wand_side_wpE]
      tcb_update_vspace_root_wp[sep_wand_side_wpE]
      tcb_update_cspace_root_wp[sep_wand_side_wpE] | clarsimp cong:cap_type_bad_cong |fastforce)+ apply (clarsimp simp: pred_conj_def | sep_cancel | simp cong:cap_type_bad_cong)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) and K (faultep = Some fltep \<and> croot = Some (crt_cap, crt_slot) \<and> vroot = Some (vrt_cap, vrt_slot) \<and> ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot) \<and> cap_type vrt_cap \<noteq> Some UntypedType \<and> cap_type crt_cap \<noteq> Some UntypedType \<and> cap_type ipcbuff_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap vrt_cap' \<and> \<not> is_memory_cap crt_cap' \<and> \<not> is_memory_cap ipcbuff_cap' \<and> cdl_same_arch_obj_as vrt_cap vrt_cap' \<and> cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap' \<and> is_cnode_cap crt_cap' \<and> cap_object crt_cap = cap_object crt_cap')\<rbrace> invoke_tcb (ThreadControl target_tcb tcb_cap_slot faultep croot vroot ipc_buffer) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* crt_slot \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) and K (faultep = Some fltep \<and> croot = Some (crt_cap, crt_slot) \<and> vroot = Some (vrt_cap, vrt_slot) \<and> ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot) \<and> cap_type vrt_cap \<noteq> Some UntypedType \<and> cap_type crt_cap \<noteq> Some UntypedType \<and> cap_type ipcbuff_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap vrt_cap' \<and> \<not> is_memory_cap crt_cap' \<and> \<not> is_memory_cap ipcbuff_cap' \<and> cdl_same_arch_obj_as vrt_cap vrt_cap' \<and> cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap' \<and> is_cnode_cap crt_cap' \<and> cap_object crt_cap = cap_object crt_cap')) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> invoke_tcb (ThreadControl target_tcb tcb_cap_slot faultep croot vroot ipc_buffer) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* crt_slot \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- liftE (update_thread target_tcb (cdl_tcb_fault_endpoint_update (\<lambda>_. fltep)));
y <- tcb_update_cspace_root target_tcb tcb_cap_slot (crt_cap, crt_slot);
y <- tcb_update_vspace_root target_tcb tcb_cap_slot (vrt_cap, vrt_slot);
tcb_update_ipc_buffer target_tcb tcb_cap_slot (ipcbuff_cap, ipcbuff_slot)
odE \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* crt_slot \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s y ya yb. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s y ya yb\<rbrace> tcb_update_ipc_buffer target_tcb tcb_cap_slot (ipcbuff_cap, ipcbuff_slot) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* crt_slot \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R)\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s y ya. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y ya\<rbrace> tcb_update_vspace_root target_tcb tcb_cap_slot (vrt_cap, vrt_slot) \<lbrace>?B23 s y ya\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s y. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y\<rbrace> tcb_update_cspace_root target_tcb tcb_cap_slot (crt_cap, crt_slot) \<lbrace>?B22 s y\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>s. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 s\<rbrace> liftE (update_thread target_tcb (cdl_tcb_fault_endpoint_update (\<lambda>_. fltep))) \<lbrace>?B21 s\<rbrace>, \<lbrace>E\<rbrace>
 5. \<And>s sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'; s = sa\<rbrakk> \<Longrightarrow> ?Q20 s sa proof (prove)
goal (5 subgoals):
 1. \<And>s y ya yb. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> cap_type ipcbuff_cap \<noteq> Some UntypedType \<and> \<not> is_memory_cap (?cap25 s y ya yb) \<and> cdl_same_arch_obj_as ipcbuff_cap (?cap25 s y ya yb)
 2. \<And>s y ya. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y ya\<rbrace> tcb_update_vspace_root target_tcb tcb_cap_slot (vrt_cap, vrt_slot) \<lbrace>\<lambda>yb. cdl.lift (((ipcbuff_slot \<mapsto>c ?cap25 s y ya yb \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap) \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ipcbuff_slot \<mapsto>c ?cap25 s y ya yb \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* crt_slot \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R))\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s y. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y\<rbrace> tcb_update_cspace_root target_tcb tcb_cap_slot (crt_cap, crt_slot) \<lbrace>?B22 s y\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>s. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 s\<rbrace> liftE (update_thread target_tcb (cdl_tcb_fault_endpoint_update (\<lambda>_. fltep))) \<lbrace>?B21 s\<rbrace>, \<lbrace>E\<rbrace>
 5. \<And>s sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'; s = sa\<rbrakk> \<Longrightarrow> ?Q20 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s y ya. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s y ya\<rbrace> tcb_update_vspace_root target_tcb tcb_cap_slot (vrt_cap, vrt_slot) \<lbrace>\<lambda>yb. cdl.lift (((ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap) \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* crt_slot \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R))\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s y. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s y\<rbrace> tcb_update_cspace_root target_tcb tcb_cap_slot (crt_cap, crt_slot) \<lbrace>?B22 s y\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 s\<rbrace> liftE (update_thread target_tcb (cdl_tcb_fault_endpoint_update (\<lambda>_. fltep))) \<lbrace>?B21 s\<rbrace>, \<lbrace>E\<rbrace>
 4. \<And>s sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'; s = sa\<rbrakk> \<Longrightarrow> ?Q20 s sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) sa; faultep = Some fltep; croot = Some (crt_cap, crt_slot); vroot = Some (vrt_cap, vrt_slot); ipc_buffer = Some (ipcbuff_cap, ipcbuff_slot); cap_type vrt_cap \<noteq> Some UntypedType; cap_type crt_cap \<noteq> Some UntypedType; cap_type ipcbuff_cap \<noteq> Some UntypedType; \<not> is_memory_cap vrt_cap'; \<not> is_memory_cap crt_cap'; \<not> is_memory_cap ipcbuff_cap'; cdl_same_arch_obj_as vrt_cap vrt_cap'; cdl_same_arch_obj_as ipcbuff_cap ipcbuff_cap'; is_cnode_cap crt_cap'; cap_object crt_cap = cap_object crt_cap'\<rbrakk> \<Longrightarrow> cdl.lift (target_tcb \<mapsto>f Tcb (?tcb55 sa) \<and>* (target_tcb \<mapsto>f Tcb (?tcb55 sa\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<longrightarrow>* ((crt_slot \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap) \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* crt_slot \<mapsto>c crt_cap' \<longrightarrow>* ((vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap) \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* vrt_slot \<mapsto>c vrt_cap' \<longrightarrow>* ((ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap) \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ipcbuff_slot \<mapsto>c ipcbuff_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* vrt_slot \<mapsto>c vrt_cap' \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* crt_slot \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R))))) sa proof (prove)
goal:
No subgoals!