theory TCB_DP

lemma decode_invocation_tcb_rv'':
" \<lbrakk>buffer \<noteq> 0\<rbrakk> \<Longrightarrow>
  \<lbrace>\<lambda>s.\<exists>croot_cap vroot_cap ipcbuff_cap.
      is_tcb_cap cap \<and>
      caps = [(croot_cap,croot_slot), (vroot_cap,vroot_slot), (ipcbuff_cap, ipcbuff_slot)]@xs \<and>
      cap_has_object cap \<and>
      P (InvokeTcb $
        ThreadControl
        (cap_object cap)
         cap_ref
        (Some fault_ep)
        (Some (cdl_update_cnode_cap_data (croot_cap) cspace_root_data, croot_slot))
        (Some (vroot_cap, vroot_slot))
        (Some ((reset_mem_mapping ipcbuff_cap),ipcbuff_slot))) s\<rbrace>
  decode_invocation cap cap_ref caps (TcbIntent $ TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer)
  \<lbrace>P\<rbrace>, -" apply (clarsimp) apply (unfold validE_def validE_R_def) apply (rule hoare_name_pre_state) apply (unfold validE_def[symmetric] validE_R_def[symmetric]) apply (clarsimp simp: decode_tcb_invocation_simps cap_type_def) apply (wp) apply (clarsimp simp: comp_def) apply (wp decode_invocation_tcb_rv') apply (clarsimp simp: split_def) apply (safe) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. buffer \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>croot_cap vroot_cap ipcbuff_cap. is_tcb_cap cap \<and> caps = [(croot_cap, croot_slot), (vroot_cap, vroot_slot), (ipcbuff_cap, ipcbuff_slot)] @ xs \<and> cap_has_object cap \<and> P (InvokeTcb $ ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot))) s\<rbrace> decode_invocation cap cap_ref caps (TcbIntent $ TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer) \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. buffer \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. is_tcb_cap cap \<and> (\<exists>croot_cap vroot_cap ipcbuff_cap. caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs \<and> cap_has_object cap \<and> P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) s)\<rbrace> decode_invocation cap cap_ref caps (TcbIntent (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer)) \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. buffer \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. is_tcb_cap cap \<and> (\<exists>croot_cap vroot_cap ipcbuff_cap. caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs \<and> cap_has_object cap \<and> P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) s)\<rbrace> decode_invocation cap cap_ref caps (TcbIntent (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer)) \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>buffer \<noteq> 0; is_tcb_cap cap \<and> (\<exists>croot_cap vroot_cap ipcbuff_cap. caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs \<and> cap_has_object cap \<and> P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_invocation cap cap_ref caps (TcbIntent (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer)) \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>buffer \<noteq> 0; is_tcb_cap cap \<and> (\<exists>croot_cap vroot_cap ipcbuff_cap. caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs \<and> cap_has_object cap \<and> P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_invocation cap cap_ref caps (TcbIntent (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer)) \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s croot_cap vroot_cap ipcbuff_cap. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftME InvokeTcb (decode_tcb_invocation cap cap_ref ((croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs) (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer)) \<lbrace>P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s croot_cap vroot_cap ipcbuff_cap. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'10 s croot_cap vroot_cap ipcbuff_cap\<rbrace> decode_tcb_invocation cap cap_ref ((croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs) (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer) \<lbrace>P \<circ> InvokeTcb\<rbrace>, -
 2. \<And>s croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) s; s = sa\<rbrakk> \<Longrightarrow> ?P'10 s croot_cap vroot_cap ipcbuff_cap sa proof (prove)
goal (2 subgoals):
 1. \<And>s croot_cap vroot_cap ipcbuff_cap. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'10 s croot_cap vroot_cap ipcbuff_cap\<rbrace> decode_tcb_invocation cap cap_ref ((croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs) (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer) \<lbrace>\<lambda>x. P (InvokeTcb x)\<rbrace>, -
 2. \<And>s croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) s; s = sa\<rbrakk> \<Longrightarrow> ?P'10 s croot_cap vroot_cap ipcbuff_cap sa proof (prove)
goal (1 subgoal):
 1. \<And>s croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) s; s = sa\<rbrakk> \<Longrightarrow> P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data (?croot_cap15 s croot_cap vroot_cap ipcbuff_cap) cspace_root_data, ?croot_slot15 s croot_cap vroot_cap ipcbuff_cap)) (Some (?vroot_cap15 s croot_cap vroot_cap ipcbuff_cap, ?vroot_slot15 s croot_cap vroot_cap ipcbuff_cap)) (Some (reset_mem_mapping (?ipcbuff_cap15 s croot_cap vroot_cap ipcbuff_cap), ?ipcbuff_slot15 s croot_cap vroot_cap ipcbuff_cap)))) sa \<and> (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs = [(?croot_cap15 s croot_cap vroot_cap ipcbuff_cap, ?croot_slot15 s croot_cap vroot_cap ipcbuff_cap), (?vroot_cap15 s croot_cap vroot_cap ipcbuff_cap, ?vroot_slot15 s croot_cap vroot_cap ipcbuff_cap), (?ipcbuff_cap15 s croot_cap vroot_cap ipcbuff_cap, ?ipcbuff_slot15 s croot_cap vroot_cap ipcbuff_cap)] @ ?xs15 s croot_cap vroot_cap ipcbuff_cap \<and> cap_has_object cap \<and> buffer \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) sa\<rbrakk> \<Longrightarrow> P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data (?croot_cap15 sa croot_cap vroot_cap ipcbuff_cap) cspace_root_data, ?croot_slot15 sa croot_cap vroot_cap ipcbuff_cap)) (Some (?vroot_cap15 sa croot_cap vroot_cap ipcbuff_cap, ?vroot_slot15 sa croot_cap vroot_cap ipcbuff_cap)) (Some (reset_mem_mapping (?ipcbuff_cap15 sa croot_cap vroot_cap ipcbuff_cap), ?ipcbuff_slot15 sa croot_cap vroot_cap ipcbuff_cap)))) sa \<and> croot_cap = ?croot_cap15 sa croot_cap vroot_cap ipcbuff_cap \<and> croot_slot = ?croot_slot15 sa croot_cap vroot_cap ipcbuff_cap \<and> vroot_cap = ?vroot_cap15 sa croot_cap vroot_cap ipcbuff_cap \<and> vroot_slot = ?vroot_slot15 sa croot_cap vroot_cap ipcbuff_cap \<and> ipcbuff_cap = ?ipcbuff_cap15 sa croot_cap vroot_cap ipcbuff_cap \<and> ipcbuff_slot = ?ipcbuff_slot15 sa croot_cap vroot_cap ipcbuff_cap \<and> xs = ?xs15 sa croot_cap vroot_cap ipcbuff_cap proof (prove)
goal (8 subgoals):
 1. \<And>croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) sa\<rbrakk> \<Longrightarrow> P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data (?croot_cap15 sa croot_cap vroot_cap ipcbuff_cap) cspace_root_data, ?croot_slot15 sa croot_cap vroot_cap ipcbuff_cap)) (Some (?vroot_cap15 sa croot_cap vroot_cap ipcbuff_cap, ?vroot_slot15 sa croot_cap vroot_cap ipcbuff_cap)) (Some (reset_mem_mapping (?ipcbuff_cap15 sa croot_cap vroot_cap ipcbuff_cap), ?ipcbuff_slot15 sa croot_cap vroot_cap ipcbuff_cap)))) sa
 2. \<And>croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) sa\<rbrakk> \<Longrightarrow> croot_cap = ?croot_cap15 sa croot_cap vroot_cap ipcbuff_cap
 3. \<And>croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) sa\<rbrakk> \<Longrightarrow> croot_slot = ?croot_slot15 sa croot_cap vroot_cap ipcbuff_cap
 4. \<And>croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) sa\<rbrakk> \<Longrightarrow> vroot_cap = ?vroot_cap15 sa croot_cap vroot_cap ipcbuff_cap
 5. \<And>croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) sa\<rbrakk> \<Longrightarrow> vroot_slot = ?vroot_slot15 sa croot_cap vroot_cap ipcbuff_cap
 6. \<And>croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) sa\<rbrakk> \<Longrightarrow> ipcbuff_cap = ?ipcbuff_cap15 sa croot_cap vroot_cap ipcbuff_cap
 7. \<And>croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) sa\<rbrakk> \<Longrightarrow> ipcbuff_slot = ?ipcbuff_slot15 sa croot_cap vroot_cap ipcbuff_cap
 8. \<And>croot_cap vroot_cap ipcbuff_cap sa. \<lbrakk>buffer \<noteq> 0; (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = Some TcbType; caps = (croot_cap, croot_slot) # (vroot_cap, vroot_slot) # (ipcbuff_cap, ipcbuff_slot) # xs; cap_has_object cap; P (InvokeTcb (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data croot_cap cspace_root_data, croot_slot)) (Some (vroot_cap, vroot_slot)) (Some (reset_mem_mapping ipcbuff_cap, ipcbuff_slot)))) sa\<rbrakk> \<Longrightarrow> xs = ?xs15 sa croot_cap vroot_cap ipcbuff_cap proof (prove)
goal:
No subgoals!