theory Tcb_DR

lemma decode_set_ipc_buffer_translate_tcb_invocation:
  "\<lbrakk>x \<noteq> [];excaps ! 0 = (a,b,c)\<rbrakk> \<Longrightarrow>
    (\<And>s. \<lbrace>(=) s\<rbrace> decode_set_ipc_buffer x (cap.ThreadCap t) slot' excaps
    \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and>
      translate_tcb_invocation_thread_ctrl_buffer (tc_new_buffer rv) = (if (x ! 0) = 0 then None
      else Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c)))
    \<rbrace>,\<lbrace>\<lambda>ft. (=) s\<rbrace>)" apply (clarsimp simp:decode_set_ipc_buffer_def whenE_def | rule conjI)+ apply (wp , simp_all add:translate_tcb_invocation_thread_ctrl_buffer_def) apply (clarsimp | rule conjI)+ apply (wp , clarsimp simp:translate_tcb_invocation_thread_ctrl_buffer_def) apply (wp | clarsimp | rule conjI)+ apply (simp add:check_valid_ipc_buffer_def) apply (wpc|wp)+ apply (simp add:derive_cap_def split del:if_split) apply (wpsimp simp: o_def arch_derive_cap_def split_del:if_split) apply clarsimp apply (clarsimp simp:transform_mapping_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c)\<rbrakk> \<Longrightarrow> (\<And>s. \<lbrace>(=) s\<rbrace> decode_set_ipc_buffer x (ThreadCap t) slot' excaps \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> translate_tcb_invocation_thread_ctrl_buffer (tc_new_buffer rv) = (if x ! 0 = 0 then None else Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c)))\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>x \<noteq> []; [] ! 0 = (a, b, c); x ! 0 = 0; excaps = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> translate_tcb_invocation_thread_ctrl_buffer (tc_new_buffer rv) = None\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>
 2. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 = 0\<rbrakk> \<Longrightarrow> excaps \<noteq> [] \<longrightarrow> \<lbrace>(=) s\<rbrace> returnOk (tcb_invocation.ThreadControl t slot' None None None None None (Some (0, None))) \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> translate_tcb_invocation_thread_ctrl_buffer (tc_new_buffer rv) = None\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>
 3. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c)\<rbrakk> \<Longrightarrow> x ! 0 \<noteq> 0 \<longrightarrow> (excaps = [] \<longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> translate_tcb_invocation_thread_ctrl_buffer (tc_new_buffer rv) = Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c))\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>) \<and> (excaps \<noteq> [] \<longrightarrow> \<lbrace>(=) s\<rbrace> doE newbuf <- doE buffer_cap <- CSpace_A.derive_cap (b, c) a;
y <- check_valid_ipc_buffer (x ! 0) buffer_cap;
returnOk (Some (buffer_cap, b, c))
odE;
returnOk (tcb_invocation.ThreadControl t slot' None None None None None (Some (x ! 0, newbuf)))
odE \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> translate_tcb_invocation_thread_ctrl_buffer (tc_new_buffer rv) = Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c))\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 = 0\<rbrakk> \<Longrightarrow> excaps \<noteq> [] \<longrightarrow> \<lbrace>(=) s\<rbrace> returnOk (tcb_invocation.ThreadControl t slot' None None None None None (Some (0, None))) \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> (case tc_new_buffer rv of None \<Rightarrow> None | Some (a, None) \<Rightarrow> None | Some (a, Some (c, d)) \<Rightarrow> Some (transform_cap c, transform_cslot_ptr d)) = None\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>
 2. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c)\<rbrakk> \<Longrightarrow> x ! 0 \<noteq> 0 \<longrightarrow> (excaps = [] \<longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> (case tc_new_buffer rv of None \<Rightarrow> None | Some (a, None) \<Rightarrow> None | Some (a, Some (c, d)) \<Rightarrow> Some (transform_cap c, transform_cslot_ptr d)) = Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c))\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>) \<and> (excaps \<noteq> [] \<longrightarrow> \<lbrace>(=) s\<rbrace> doE newbuf <- doE buffer_cap <- CSpace_A.derive_cap (b, c) a;
y <- check_valid_ipc_buffer (x ! 0) buffer_cap;
returnOk (Some (buffer_cap, b, c))
odE;
returnOk (tcb_invocation.ThreadControl t slot' None None None None None (Some (x ! 0, newbuf)))
odE \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> (case tc_new_buffer rv of None \<Rightarrow> None | Some (a, None) \<Rightarrow> None | Some (a, Some (c, d)) \<Rightarrow> Some (transform_cap c, transform_cslot_ptr d)) = Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c))\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 = 0; excaps \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> returnOk (tcb_invocation.ThreadControl t slot' None None None None None (Some (0, None))) \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> (case tc_new_buffer rv of None \<Rightarrow> None | Some (a, None) \<Rightarrow> None | Some (a, Some (c, d)) \<Rightarrow> Some (transform_cap c, transform_cslot_ptr d)) = None\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>
 2. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c)\<rbrakk> \<Longrightarrow> x ! 0 \<noteq> 0 \<longrightarrow> (excaps = [] \<longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> (case tc_new_buffer rv of None \<Rightarrow> None | Some (a, None) \<Rightarrow> None | Some (a, Some (c, d)) \<Rightarrow> Some (transform_cap c, transform_cslot_ptr d)) = Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c))\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>) \<and> (excaps \<noteq> [] \<longrightarrow> \<lbrace>(=) s\<rbrace> doE newbuf <- doE buffer_cap <- CSpace_A.derive_cap (b, c) a;
y <- check_valid_ipc_buffer (x ! 0) buffer_cap;
returnOk (Some (buffer_cap, b, c))
odE;
returnOk (tcb_invocation.ThreadControl t slot' None None None None None (Some (x ! 0, newbuf)))
odE \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> (case tc_new_buffer rv of None \<Rightarrow> None | Some (a, None) \<Rightarrow> None | Some (a, Some (c, d)) \<Rightarrow> Some (transform_cap c, transform_cslot_ptr d)) = Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c))\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c)\<rbrakk> \<Longrightarrow> x ! 0 \<noteq> 0 \<longrightarrow> (excaps = [] \<longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> (case tc_new_buffer rv of None \<Rightarrow> None | Some (a, None) \<Rightarrow> None | Some (a, Some (c, d)) \<Rightarrow> Some (transform_cap c, transform_cslot_ptr d)) = Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c))\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>) \<and> (excaps \<noteq> [] \<longrightarrow> \<lbrace>(=) s\<rbrace> doE newbuf <- doE buffer_cap <- CSpace_A.derive_cap (b, c) a;
y <- check_valid_ipc_buffer (x ! 0) buffer_cap;
returnOk (Some (buffer_cap, b, c))
odE;
returnOk (tcb_invocation.ThreadControl t slot' None None None None None (Some (x ! 0, newbuf)))
odE \<lbrace>\<lambda>rv s'. s' = s \<and> rv = tcb_invocation.ThreadControl t slot' None None None None None (tc_new_buffer rv) \<and> (case tc_new_buffer rv of None \<Rightarrow> None | Some (a, None) \<Rightarrow> None | Some (a, Some (c, d)) \<Rightarrow> Some (transform_cap c, transform_cslot_ptr d)) = Some (reset_mem_mapping (transform_cap a), transform_cslot_ptr (b, c))\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>) proof (prove)
goal (3 subgoals):
 1. \<And>s buffer_cap. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B59 s buffer_cap\<rbrace> check_valid_ipc_buffer (x ! 0) buffer_cap \<lbrace>\<lambda>y b. b = s \<and> transform_cap buffer_cap = reset_mem_mapping (transform_cap a)\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>
 2. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s\<rbrace> CSpace_A.derive_cap (b, c) a \<lbrace>?B59 s\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>
 3. \<And>s sa. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []; s = sa\<rbrakk> \<Longrightarrow> ?Q56 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s buffer_cap. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?B59 s buffer_cap\<rbrace> case buffer_cap of ArchObjectCap (PageCap True xa xaa xb xc) \<Rightarrow> throwError IllegalOperation | ArchObjectCap (PageCap False xa xaa xb xc) \<Rightarrow> doE whenE (\<not> is_aligned (x ! 0) msg_align_bits) $ throwError AlignmentError;
returnOk ()
odE | ArchObjectCap _ \<Rightarrow> throwError IllegalOperation | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>y b. b = s \<and> transform_cap buffer_cap = reset_mem_mapping (transform_cap a)\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>
 2. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 s\<rbrace> CSpace_A.derive_cap (b, c) a \<lbrace>?B59 s\<rbrace>, \<lbrace>\<lambda>ft. (=) s\<rbrace>
 3. \<And>s sa. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []; s = sa\<rbrakk> \<Longrightarrow> ?Q56 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'292 s\<rbrace> CSpace_A.derive_cap (b, c) a \<lbrace>\<lambda>buffer_cap sa. (buffer_cap = cap.NullCap \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x xa xb xc. buffer_cap = cap.UntypedCap x xa xb xc \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x xa xb. buffer_cap = cap.EndpointCap x xa xb \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x xa xb. buffer_cap = cap.NotificationCap x xa xb \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x xa xb. buffer_cap = cap.ReplyCap x xa xb \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x xa xb. buffer_cap = cap.CNodeCap x xa xb \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x. buffer_cap = ThreadCap x \<longrightarrow> s = sa \<and> True) \<and> (buffer_cap = cap.DomainCap \<longrightarrow> s = sa \<and> True) \<and> (buffer_cap = IRQControlCap \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x. buffer_cap = IRQHandlerCap x \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x xa xb. buffer_cap = Zombie x xa xb \<longrightarrow> s = sa \<and> True) \<and> (\<forall>xa. buffer_cap = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = ASIDPoolCap x xb \<longrightarrow> s = sa \<and> True) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa \<and> True) \<and> (\<forall>xb xc xd xe xf. xa = PageCap xb xc xd xe xf \<longrightarrow> (xb = True \<longrightarrow> s = sa \<and> True) \<and> (xb = False \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap buffer_cap = reset_mem_mapping (transform_cap a))) sa)) \<and> (\<forall>x xb. xa = arch_cap.PageTableCap x xb \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x xb. xa = arch_cap.PageDirectoryCap x xb \<longrightarrow> s = sa \<and> True))\<rbrace>, -
 2. \<And>s sa. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []; s = sa\<rbrakk> \<Longrightarrow> s = sa \<and> ?P'292 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'292 s\<rbrace> case a of cap.UntypedCap dev ptr sz f \<Rightarrow> doE CSpace_A.ensure_no_children (b, c);
returnOk a
odE | cap.ReplyCap ptr m cr \<Rightarrow> returnOk cap.NullCap | IRQControlCap \<Rightarrow> returnOk cap.NullCap | Zombie ptr n sz \<Rightarrow> returnOk cap.NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk a \<lbrace>\<lambda>buffer_cap sa. (buffer_cap = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. buffer_cap = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. buffer_cap = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. buffer_cap = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. buffer_cap = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. buffer_cap = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. buffer_cap = ThreadCap x) \<longrightarrow> s = sa) \<and> (buffer_cap = cap.DomainCap \<longrightarrow> s = sa) \<and> (buffer_cap = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. buffer_cap = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. buffer_cap = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. buffer_cap = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap buffer_cap = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))\<rbrace>, -
 2. \<And>s sa. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []; s = sa\<rbrakk> \<Longrightarrow> s = sa \<and> ?P'292 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>x \<noteq> []; excaps ! 0 = (a, b, c); x ! 0 \<noteq> 0; excaps \<noteq> []; s = sa\<rbrakk> \<Longrightarrow> s = sa \<and> (a = cap.NullCap \<longrightarrow> (a = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. a = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. a = ThreadCap x) \<longrightarrow> s = sa) \<and> (a = cap.DomainCap \<longrightarrow> s = sa) \<and> (a = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. a = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. a = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap a = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))) \<and> (\<forall>xa xb xc xd. a = cap.UntypedCap xa xb xc xd \<longrightarrow> True \<and> (cap.UntypedCap xa xb xc xd = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xe xf xg. cap.UntypedCap xa xb xc xd = cap.UntypedCap x xe xf xg) \<longrightarrow> s = sa) \<and> ((\<exists>x xe xf. cap.UntypedCap xa xb xc xd = cap.EndpointCap x xe xf) \<longrightarrow> s = sa) \<and> ((\<exists>x xe xf. cap.UntypedCap xa xb xc xd = cap.NotificationCap x xe xf) \<longrightarrow> s = sa) \<and> ((\<exists>x xe xf. cap.UntypedCap xa xb xc xd = cap.ReplyCap x xe xf) \<longrightarrow> s = sa) \<and> ((\<exists>x xe xf. cap.UntypedCap xa xb xc xd = cap.CNodeCap x xe xf) \<longrightarrow> s = sa) \<and> ((\<exists>x. cap.UntypedCap xa xb xc xd = ThreadCap x) \<longrightarrow> s = sa) \<and> (cap.UntypedCap xa xb xc xd = cap.DomainCap \<longrightarrow> s = sa) \<and> (cap.UntypedCap xa xb xc xd = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. cap.UntypedCap xa xb xc xd = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xe xf. cap.UntypedCap xa xb xc xd = Zombie x xe xf) \<longrightarrow> s = sa) \<and> (\<forall>xe. cap.UntypedCap xa xb xc xd = ArchObjectCap xe \<longrightarrow> ((\<exists>x xa. xe = ASIDPoolCap x xa) \<longrightarrow> s = sa) \<and> (xe = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xf. (\<exists>x xa xb xc. xe = PageCap xf x xa xb xc) \<longrightarrow> (xf \<longrightarrow> s = sa) \<and> (\<not> xf \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>a. a = s \<and> transform_cap (cap.UntypedCap xa xb xc xd) = reset_mem_mapping (transform_cap (cap.UntypedCap xa xb xc xd)))) sa)) \<and> ((\<exists>x xa. xe = arch_cap.PageTableCap x xa) \<longrightarrow> s = sa) \<and> ((\<exists>x xa. xe = arch_cap.PageDirectoryCap x xa) \<longrightarrow> s = sa))) \<and> (\<forall>xa xb xc. a = cap.EndpointCap xa xb xc \<longrightarrow> (a = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. a = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. a = ThreadCap x) \<longrightarrow> s = sa) \<and> (a = cap.DomainCap \<longrightarrow> s = sa) \<and> (a = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. a = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. a = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap a = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))) \<and> (\<forall>xa xb xc. a = cap.NotificationCap xa xb xc \<longrightarrow> (a = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. a = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. a = ThreadCap x) \<longrightarrow> s = sa) \<and> (a = cap.DomainCap \<longrightarrow> s = sa) \<and> (a = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. a = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. a = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap a = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))) \<and> (\<forall>xa xb xc. a = cap.ReplyCap xa xb xc \<longrightarrow> (cap.NullCap = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. cap.NullCap = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. cap.NullCap = ThreadCap x) \<longrightarrow> s = sa) \<and> (cap.NullCap = cap.DomainCap \<longrightarrow> s = sa) \<and> (cap.NullCap = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. cap.NullCap = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. cap.NullCap = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap cap.NullCap = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))) \<and> (\<forall>xa xb xc. a = cap.CNodeCap xa xb xc \<longrightarrow> (a = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. a = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. a = ThreadCap x) \<longrightarrow> s = sa) \<and> (a = cap.DomainCap \<longrightarrow> s = sa) \<and> (a = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. a = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. a = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap a = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))) \<and> (\<forall>xa. a = ThreadCap xa \<longrightarrow> (a = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. a = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. a = ThreadCap x) \<longrightarrow> s = sa) \<and> (a = cap.DomainCap \<longrightarrow> s = sa) \<and> (a = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. a = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. a = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap a = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))) \<and> (a = cap.DomainCap \<longrightarrow> (a = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. a = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. a = ThreadCap x) \<longrightarrow> s = sa) \<and> (a = cap.DomainCap \<longrightarrow> s = sa) \<and> (a = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. a = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. a = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap a = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))) \<and> (a = IRQControlCap \<longrightarrow> (cap.NullCap = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. cap.NullCap = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. cap.NullCap = ThreadCap x) \<longrightarrow> s = sa) \<and> (cap.NullCap = cap.DomainCap \<longrightarrow> s = sa) \<and> (cap.NullCap = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. cap.NullCap = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. cap.NullCap = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap cap.NullCap = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))) \<and> (\<forall>xa. a = IRQHandlerCap xa \<longrightarrow> (a = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. a = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. a = ThreadCap x) \<longrightarrow> s = sa) \<and> (a = cap.DomainCap \<longrightarrow> s = sa) \<and> (a = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. a = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. a = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. a = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap a = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))) \<and> (\<forall>xa xb xc. a = Zombie xa xb xc \<longrightarrow> (cap.NullCap = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. cap.NullCap = cap.UntypedCap x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.EndpointCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.NotificationCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.ReplyCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = cap.CNodeCap x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x. cap.NullCap = ThreadCap x) \<longrightarrow> s = sa) \<and> (cap.NullCap = cap.DomainCap \<longrightarrow> s = sa) \<and> (cap.NullCap = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. cap.NullCap = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. cap.NullCap = Zombie x xa xb) \<longrightarrow> s = sa) \<and> (\<forall>xa. cap.NullCap = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> s = sa) \<and> (xa = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xb. (\<exists>x xc xd xe. xa = PageCap xb x xc xd xe) \<longrightarrow> (xb \<longrightarrow> s = sa) \<and> (\<not> xb \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>b. b = s \<and> transform_cap cap.NullCap = reset_mem_mapping (transform_cap a))) sa)) \<and> ((\<exists>x xb. xa = arch_cap.PageTableCap x xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xb. xa = arch_cap.PageDirectoryCap x xb) \<longrightarrow> s = sa))) \<and> (\<forall>xa. a = ArchObjectCap xa \<longrightarrow> (\<forall>xb xc. xa = ASIDPoolCap xb xc \<longrightarrow> (ArchObjectCap xa = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc xd. ArchObjectCap xa = cap.UntypedCap x xb xc xd) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.EndpointCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.NotificationCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.ReplyCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.CNodeCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x. ArchObjectCap xa = ThreadCap x) \<longrightarrow> s = sa) \<and> (ArchObjectCap xa = cap.DomainCap \<longrightarrow> s = sa) \<and> (ArchObjectCap xa = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. ArchObjectCap xa = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = Zombie x xb xc) \<longrightarrow> s = sa) \<and> (\<forall>xb. ArchObjectCap xa = ArchObjectCap xb \<longrightarrow> ((\<exists>x xa. xb = ASIDPoolCap x xa) \<longrightarrow> s = sa) \<and> (xb = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xc. (\<exists>x xa xd xe. xb = PageCap xc x xa xd xe) \<longrightarrow> (xc \<longrightarrow> s = sa) \<and> (\<not> xc \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>a. a = s \<and> transform_cap (ArchObjectCap xa) = reset_mem_mapping (transform_cap (ArchObjectCap xa)))) sa)) \<and> ((\<exists>x xa. xb = arch_cap.PageTableCap x xa) \<longrightarrow> s = sa) \<and> ((\<exists>x xa. xb = arch_cap.PageDirectoryCap x xa) \<longrightarrow> s = sa))) \<and> (xa = ASIDControlCap \<longrightarrow> (ArchObjectCap xa = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc xd. ArchObjectCap xa = cap.UntypedCap x xb xc xd) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.EndpointCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.NotificationCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.ReplyCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.CNodeCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x. ArchObjectCap xa = ThreadCap x) \<longrightarrow> s = sa) \<and> (ArchObjectCap xa = cap.DomainCap \<longrightarrow> s = sa) \<and> (ArchObjectCap xa = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. ArchObjectCap xa = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = Zombie x xb xc) \<longrightarrow> s = sa) \<and> (\<forall>xb. ArchObjectCap xa = ArchObjectCap xb \<longrightarrow> ((\<exists>x xa. xb = ASIDPoolCap x xa) \<longrightarrow> s = sa) \<and> (xb = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xc. (\<exists>x xa xd xe. xb = PageCap xc x xa xd xe) \<longrightarrow> (xc \<longrightarrow> s = sa) \<and> (\<not> xc \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>a. a = s \<and> transform_cap (ArchObjectCap xa) = reset_mem_mapping (transform_cap (ArchObjectCap xa)))) sa)) \<and> ((\<exists>x xa. xb = arch_cap.PageTableCap x xa) \<longrightarrow> s = sa) \<and> ((\<exists>x xa. xb = arch_cap.PageDirectoryCap x xa) \<longrightarrow> s = sa))) \<and> (\<forall>xb xc xd xe xf. xa = PageCap xb xc xd xe xf \<longrightarrow> (ArchObjectCap (PageCap xb xc xd xe None) = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xa xf xg. ArchObjectCap (PageCap xb xc xd xe None) = cap.UntypedCap x xa xf xg) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xf. ArchObjectCap (PageCap xb xc xd xe None) = cap.EndpointCap x xa xf) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xf. ArchObjectCap (PageCap xb xc xd xe None) = cap.NotificationCap x xa xf) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xf. ArchObjectCap (PageCap xb xc xd xe None) = cap.ReplyCap x xa xf) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xf. ArchObjectCap (PageCap xb xc xd xe None) = cap.CNodeCap x xa xf) \<longrightarrow> s = sa) \<and> ((\<exists>x. ArchObjectCap (PageCap xb xc xd xe None) = ThreadCap x) \<longrightarrow> s = sa) \<and> (ArchObjectCap (PageCap xb xc xd xe None) = cap.DomainCap \<longrightarrow> s = sa) \<and> (ArchObjectCap (PageCap xb xc xd xe None) = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. ArchObjectCap (PageCap xb xc xd xe None) = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xf. ArchObjectCap (PageCap xb xc xd xe None) = Zombie x xa xf) \<longrightarrow> s = sa) \<and> (\<forall>xf. ArchObjectCap (PageCap xb xc xd xe None) = ArchObjectCap xf \<longrightarrow> ((\<exists>x xa. xf = ASIDPoolCap x xa) \<longrightarrow> s = sa) \<and> (xf = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xg. (\<exists>x xa xb xc. xf = PageCap xg x xa xb xc) \<longrightarrow> (xg \<longrightarrow> s = sa) \<and> (\<not> xg \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>a. a = s \<and> transform_cap (ArchObjectCap (PageCap xb xc xd xe None)) = reset_mem_mapping (transform_cap (ArchObjectCap xa)))) sa)) \<and> ((\<exists>x xa. xf = arch_cap.PageTableCap x xa) \<longrightarrow> s = sa) \<and> ((\<exists>x xa. xf = arch_cap.PageDirectoryCap x xa) \<longrightarrow> s = sa))) \<and> (\<forall>xb xc. xa = arch_cap.PageTableCap xb xc \<longrightarrow> (xc = None \<longrightarrow> True) \<and> (\<forall>xb. xc = Some xb \<longrightarrow> (ArchObjectCap xa = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc xd. ArchObjectCap xa = cap.UntypedCap x xb xc xd) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.EndpointCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.NotificationCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.ReplyCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.CNodeCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x. ArchObjectCap xa = ThreadCap x) \<longrightarrow> s = sa) \<and> (ArchObjectCap xa = cap.DomainCap \<longrightarrow> s = sa) \<and> (ArchObjectCap xa = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. ArchObjectCap xa = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = Zombie x xb xc) \<longrightarrow> s = sa) \<and> (\<forall>xb. ArchObjectCap xa = ArchObjectCap xb \<longrightarrow> ((\<exists>x xa. xb = ASIDPoolCap x xa) \<longrightarrow> s = sa) \<and> (xb = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xc. (\<exists>x xa xd xe. xb = PageCap xc x xa xd xe) \<longrightarrow> (xc \<longrightarrow> s = sa) \<and> (\<not> xc \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>a. a = s \<and> transform_cap (ArchObjectCap xa) = reset_mem_mapping (transform_cap (ArchObjectCap xa)))) sa)) \<and> ((\<exists>x xa. xb = arch_cap.PageTableCap x xa) \<longrightarrow> s = sa) \<and> ((\<exists>x xa. xb = arch_cap.PageDirectoryCap x xa) \<longrightarrow> s = sa)))) \<and> (\<forall>xb xc. xa = arch_cap.PageDirectoryCap xb xc \<longrightarrow> (xc = None \<longrightarrow> True) \<and> (\<forall>xb. xc = Some xb \<longrightarrow> (ArchObjectCap xa = cap.NullCap \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc xd. ArchObjectCap xa = cap.UntypedCap x xb xc xd) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.EndpointCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.NotificationCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.ReplyCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = cap.CNodeCap x xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x. ArchObjectCap xa = ThreadCap x) \<longrightarrow> s = sa) \<and> (ArchObjectCap xa = cap.DomainCap \<longrightarrow> s = sa) \<and> (ArchObjectCap xa = IRQControlCap \<longrightarrow> s = sa) \<and> ((\<exists>x. ArchObjectCap xa = IRQHandlerCap x) \<longrightarrow> s = sa) \<and> ((\<exists>x xb xc. ArchObjectCap xa = Zombie x xb xc) \<longrightarrow> s = sa) \<and> (\<forall>xb. ArchObjectCap xa = ArchObjectCap xb \<longrightarrow> ((\<exists>x xa. xb = ASIDPoolCap x xa) \<longrightarrow> s = sa) \<and> (xb = ASIDControlCap \<longrightarrow> s = sa) \<and> (\<forall>xc. (\<exists>x xa xd xe. xb = PageCap xc x xa xd xe) \<longrightarrow> (xc \<longrightarrow> s = sa) \<and> (\<not> xc \<longrightarrow> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>sa. s = sa \<and> True else (\<lambda>_. True)) sa \<and> (if \<not> is_aligned (x ! 0) msg_align_bits then \<lambda>s. True \<and> True else (\<lambda>a. a = s \<and> transform_cap (ArchObjectCap xa) = reset_mem_mapping (transform_cap (ArchObjectCap xa)))) sa)) \<and> ((\<exists>x xa. xb = arch_cap.PageTableCap x xa) \<longrightarrow> s = sa) \<and> ((\<exists>x xa. xb = arch_cap.PageDirectoryCap x xa) \<longrightarrow> s = sa))))) proof (prove)
goal (1 subgoal):
 1. \<And>xa xb xc xd xe. \<lbrakk>x \<noteq> []; excaps ! 0 = (ArchObjectCap (PageCap False xb xc xd xe), b, c); x ! 0 \<noteq> 0; excaps \<noteq> []; is_aligned (x ! 0) msg_align_bits; a = ArchObjectCap (PageCap False xb xc xd xe); \<not> xa\<rbrakk> \<Longrightarrow> transform_mapping None = None proof (prove)
goal:
No subgoals!