theory TCB_DP

lemma invoke_tcb_threadcontrol_wp':
  "(\<exists>x y z. faultep = Some fltep \<and>
  croot = Some x \<and>  vroot = Some y \<and> ipc_buffer = Some z \<and>
  crt_slot = snd x \<and> vrt_slot = snd y \<and> ipcbuff_slot = snd z \<and>
  is_pd_cap vrt_cap \<and> is_frame_cap ipcbuff_cap \<and>
  is_cnode_cap crt_cap' \<and>
  is_cnode_cap crt_cap \<and> cap_object crt_cap = cap_object crt_cap' \<and>
  reset_cap_asid crt_cap = reset_cap_asid (fst x) \<and>
  reset_cap_asid vrt_cap = reset_cap_asid (fst y) \<and>
  reset_cap_asid ipcbuff_cap = reset_cap_asid (fst z) ) \<Longrightarrow>
  \<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> \<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 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[where cap = crt_cap',sep_wand_side_wpE]
     | clarsimp | fastforce)+ apply (clarsimp cong:cap_type_bad_cong) apply wp 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[where cap = crt_cap,sep_wand_side_wpE]
      | clarsimp | fastforce)+ apply (frule sep_map_c_asid_reset[where ptr=vrt_slot and cap=vrt_cap]) apply (frule sep_map_c_asid_reset[where ptr="(target_tcb, tcb_vspace_slot)" and cap=vrt_cap]) apply (frule sep_map_c_asid_reset[where ptr="(target_tcb,tcb_ipcbuffer_slot)" and cap=ipcbuff_cap]) apply (clarsimp simp: sep_conj_assoc pred_conj_def cong:cap_type_bad_cong
     | sep_cancel | safe)+ apply (frule sep_map_c_asid_reset[where ptr="(target_tcb,tcb_cspace_slot)" and cap=crt_cap]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x y z. faultep = Some fltep \<and> croot = Some x \<and> vroot = Some y \<and> ipc_buffer = Some z \<and> crt_slot = snd x \<and> vrt_slot = snd y \<and> ipcbuff_slot = snd z \<and> is_pd_cap vrt_cap \<and> is_frame_cap ipcbuff_cap \<and> is_cnode_cap crt_cap' \<and> is_cnode_cap crt_cap \<and> cap_object crt_cap = cap_object crt_cap' \<and> reset_cap_asid crt_cap = reset_cap_asid (fst x) \<and> reset_cap_asid vrt_cap = reset_cap_asid (fst y) \<and> reset_cap_asid ipcbuff_cap = reset_cap_asid (fst z) \<Longrightarrow> \<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)\<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>\<exists>x y z. faultep = Some fltep \<and> croot = Some x \<and> vroot = Some y \<and> ipc_buffer = Some z \<and> crt_slot = snd x \<and> vrt_slot = snd y \<and> ipcbuff_slot = snd z \<and> is_pd_cap vrt_cap \<and> is_frame_cap ipcbuff_cap \<and> is_cnode_cap crt_cap' \<and> is_cnode_cap crt_cap \<and> cap_object crt_cap = cap_object crt_cap' \<and> reset_cap_asid crt_cap = reset_cap_asid (fst x) \<and> reset_cap_asid vrt_cap = reset_cap_asid (fst y) \<and> reset_cap_asid ipcbuff_cap = reset_cap_asid (fst z); 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\<rbrakk> \<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 a aa b ab ac ba ad ae bb sz. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad\<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 (a, aa, b);
y <- tcb_update_vspace_root target_tcb tcb_cap_slot (ab, ac, ba);
tcb_update_ipc_buffer target_tcb tcb_cap_slot (ad, ae, bb)
odE \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* (aa, b) \<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 (3 subgoals):
 1. \<And>s a aa b ab ac ba ad ae bb sz. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad\<rbrakk> \<Longrightarrow> cap_type a \<noteq> Some UntypedType \<and> cap_object crt_cap' = cap_object a
 2. \<And>s a aa b ab ac ba ad ae bb sz. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad\<rbrakk> \<Longrightarrow> \<lbrace>?Q38 s a aa b ab ac ba ad ae bb sz\<rbrace> liftE (update_thread target_tcb (cdl_tcb_fault_endpoint_update (\<lambda>_. fltep))) \<lbrace>\<lambda>y. cdl.lift ((((aa, b) \<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 a \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (aa, b) \<mapsto>c crt_cap' \<longrightarrow>* (((ac, ba) \<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 ab \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ac, ba) \<mapsto>c vrt_cap \<longrightarrow>* (((ae, bb) \<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 ad \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* (aa, b) \<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 a aa b ab ac ba ad ae bb sz sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad; s = sa\<rbrakk> \<Longrightarrow> ?Q38 s a aa b ab ac ba ad ae bb sz sa proof (prove)
goal (2 subgoals):
 1. \<And>s a aa b ab ac ba ad ae bb sz. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad\<rbrakk> \<Longrightarrow> \<lbrace>?Q38 s a aa b ab ac ba ad ae bb sz\<rbrace> liftE (update_thread target_tcb (cdl_tcb_fault_endpoint_update (\<lambda>_. fltep))) \<lbrace>\<lambda>y. cdl.lift ((((aa, b) \<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 a \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (aa, b) \<mapsto>c crt_cap' \<longrightarrow>* (((ac, ba) \<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 ab \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ac, ba) \<mapsto>c vrt_cap \<longrightarrow>* (((ae, bb) \<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 ad \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* (aa, b) \<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 a aa b ab ac ba ad ae bb sz sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad; s = sa\<rbrakk> \<Longrightarrow> ?Q38 s a aa b ab ac ba ad ae bb sz sa proof (prove)
goal (2 subgoals):
 1. \<And>s a aa b ab ac ba ad ae bb sz. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad\<rbrakk> \<Longrightarrow> \<lbrace>?Q38 s a aa b ab ac ba ad ae bb sz\<rbrace> update_thread target_tcb (cdl_tcb_fault_endpoint_update (\<lambda>_. fltep)) \<lbrace>\<lambda>y. cdl.lift ((((aa, b) \<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 a \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (aa, b) \<mapsto>c crt_cap' \<longrightarrow>* (((ac, ba) \<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 ab \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ac, ba) \<mapsto>c vrt_cap \<longrightarrow>* (((ae, bb) \<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 ad \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R))))\<rbrace>
 2. \<And>s a aa b ab ac ba ad ae bb sz sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad; s = sa\<rbrakk> \<Longrightarrow> ?Q38 s a aa b ab ac ba ad ae bb sz sa proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba ad ae bb sz sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) sa; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad\<rbrakk> \<Longrightarrow> cdl.lift (target_tcb \<mapsto>f Tcb (?tcb66 sa a aa b ab ac ba ad ae bb sz) \<and>* (target_tcb \<mapsto>f Tcb (?tcb66 sa a aa b ab ac ba ad ae bb sz\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<longrightarrow>* (((aa, b) \<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 a \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (aa, b) \<mapsto>c crt_cap' \<longrightarrow>* (((ac, ba) \<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 ab \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ac, ba) \<mapsto>c vrt_cap \<longrightarrow>* (((ae, bb) \<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 ad \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R))))) sa proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba ad ae bb sz sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) sa; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad; vrt_slot \<mapsto>c vrt_cap = vrt_slot \<mapsto>c ab\<rbrakk> \<Longrightarrow> cdl.lift (target_tcb \<mapsto>f Tcb (?tcb66 sa a aa b ab ac ba ad ae bb sz) \<and>* (target_tcb \<mapsto>f Tcb (?tcb66 sa a aa b ab ac ba ad ae bb sz\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<longrightarrow>* (((aa, b) \<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 a \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (aa, b) \<mapsto>c crt_cap' \<longrightarrow>* (((ac, ba) \<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 ab \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ac, ba) \<mapsto>c vrt_cap \<longrightarrow>* (((ae, bb) \<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 ad \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R))))) sa proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba ad ae bb sz sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) sa; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad; vrt_slot \<mapsto>c vrt_cap = vrt_slot \<mapsto>c ab; (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap = (target_tcb, tcb_vspace_slot) \<mapsto>c ab\<rbrakk> \<Longrightarrow> cdl.lift (target_tcb \<mapsto>f Tcb (?tcb66 sa a aa b ab ac ba ad ae bb sz) \<and>* (target_tcb \<mapsto>f Tcb (?tcb66 sa a aa b ab ac ba ad ae bb sz\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<longrightarrow>* (((aa, b) \<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 a \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (aa, b) \<mapsto>c crt_cap' \<longrightarrow>* (((ac, ba) \<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 ab \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ac, ba) \<mapsto>c vrt_cap \<longrightarrow>* (((ae, bb) \<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 ad \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R))))) sa proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba ad ae bb sz sa. \<lbrakk>cdl.lift (target_tcb \<mapsto>f Tcb tcb \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) sa; faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap vrt_cap; cap_type ipcbuff_cap = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap crt_cap; cap_object crt_cap = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad; vrt_slot \<mapsto>c vrt_cap = vrt_slot \<mapsto>c ab; (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap = (target_tcb, tcb_vspace_slot) \<mapsto>c ab; (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap = (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ad\<rbrakk> \<Longrightarrow> cdl.lift (target_tcb \<mapsto>f Tcb (?tcb66 sa a aa b ab ac ba ad ae bb sz) \<and>* (target_tcb \<mapsto>f Tcb (?tcb66 sa a aa b ab ac ba ad ae bb sz\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<longrightarrow>* (((aa, b) \<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 a \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (aa, b) \<mapsto>c crt_cap' \<longrightarrow>* (((ac, ba) \<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 ab \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ac, ba) \<mapsto>c vrt_cap \<longrightarrow>* (((ae, bb) \<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 ad \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<longrightarrow>* (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* (ae, bb) \<mapsto>c ipcbuff_cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* (ac, ba) \<mapsto>c vrt_cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* (aa, b) \<mapsto>c crt_cap' \<and>* target_tcb \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := fltep\<rparr>) \<and>* R))))) sa proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba ad ae bb sz sa. \<lbrakk>faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap ab; cap_type ad = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap a; cap_object a = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad; (ac, ba) \<mapsto>c vrt_cap = (ac, ba) \<mapsto>c ab; (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap = (target_tcb, tcb_vspace_slot) \<mapsto>c ab; (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap = (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ad; ((target_tcb, tcb_cspace_slot) \<mapsto>c a) sa\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap) sa proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba ad ae bb sz sa. \<lbrakk>faultep = Some fltep; croot = Some (a, aa, b); vroot = Some (ab, ac, ba); ipc_buffer = Some (ad, ae, bb); crt_slot = (aa, b); vrt_slot = (ac, ba); ipcbuff_slot = (ae, bb); is_pd_cap ab; cap_type ad = Some (FrameType sz); is_cnode_cap crt_cap'; is_cnode_cap a; cap_object a = cap_object crt_cap'; reset_cap_asid crt_cap = reset_cap_asid a; reset_cap_asid vrt_cap = reset_cap_asid ab; reset_cap_asid ipcbuff_cap = reset_cap_asid ad; (ac, ba) \<mapsto>c vrt_cap = (ac, ba) \<mapsto>c ab; (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap = (target_tcb, tcb_vspace_slot) \<mapsto>c ab; (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ipcbuff_cap = (target_tcb, tcb_ipcbuffer_slot) \<mapsto>c ad; ((target_tcb, tcb_cspace_slot) \<mapsto>c a) sa; (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap = (target_tcb, tcb_cspace_slot) \<mapsto>c a\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap) sa proof (prove)
goal:
No subgoals!