theory ArchTcb_IF

lemma invoke_tcb_thread_preservation[Tcb_IF_assms]:
  assumes cap_delete_P: "\<And>slot. \<lbrace>invs and P and emptyable slot\<rbrace> cap_delete slot \<lbrace>\<lambda>_. P\<rbrace>"
  assumes cap_insert_P: "\<And>new_cap src dest. \<lbrace>invs and P\<rbrace> cap_insert new_cap src dest \<lbrace>\<lambda>_. P\<rbrace>"
  assumes thread_set_P: "\<And>f ptr. \<lbrace>invs and P\<rbrace> thread_set (tcb_ipc_buffer_update f) ptr \<lbrace>\<lambda>_. P\<rbrace>"
  assumes thread_set_P': "\<And>f ptr. \<lbrace>invs and P\<rbrace> thread_set (tcb_fault_handler_update f) ptr \<lbrace>\<lambda>_. P\<rbrace>"
  assumes set_mcpriority_P: "\<And>mcp ptr. \<lbrace>invs and P\<rbrace> set_mcpriority ptr mcp \<lbrace>\<lambda>_.P\<rbrace>"
  assumes P_trans[simp]: "\<And>f s. P (trans_state f s) = P s"
  shows
    "\<lbrace>P and invs and tcb_inv_wf (tcb_invocation.ThreadControl t sl ep mcp prio croot vroot buf)\<rbrace>
     invoke_tcb (tcb_invocation.ThreadControl t sl ep mcp prio croot vroot buf)
     \<lbrace>\<lambda>rv s :: det_state. P s\<rbrace>" supply set_priority_extended.dxo_eq[simp del]
         reschedule_required_ext_extended.dxo_eq[simp del] apply (simp add: split_def cong: option.case_cong) apply (rule hoare_vcg_precond_imp) apply (rule_tac P="case ep of Some v \<Rightarrow> length v = word_bits | _ \<Rightarrow> True"
                in hoare_gen_asm) apply wp apply ((simp add: conj_comms(1, 2) del: hoare_True_E_R
                | rule wp_split_const_if wp_split_const_if_R hoare_vcg_all_lift_R
                       hoare_vcg_E_elim hoare_vcg_const_imp_lift_R hoare_vcg_R_conj
                | (wp check_cap_inv2[where Q="\<lambda>_. pas_refined aag"]
                      check_cap_inv2[where Q="\<lambda>_ s. t \<noteq> idle_thread s"]
                      out_invs_trivial case_option_wpE cap_delete_deletes
                      cap_delete_valid_cap cap_insert_valid_cap out_cte_at
                      cap_insert_cte_at cap_delete_cte_at out_valid_cap out_tcb_valid
                      hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
                      thread_set_tcb_ipc_buffer_cap_cleared_invs
                      thread_set_invs_trivial[OF ball_tcb_cap_casesI]
                      hoare_vcg_all_lift thread_set_valid_cap out_emptyable
                      check_cap_inv [where P="valid_cap c" for c]
                      check_cap_inv [where P="tcb_cap_valid c p" for c p]
                      check_cap_inv[where P="cte_at p0" for p0]
                      check_cap_inv[where P="tcb_at p0" for p0]
                      thread_set_cte_at thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI]
                      checked_insert_no_cap_to
                      thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI]
                      out_no_cap_to_trivial[OF ball_tcb_cap_casesI] thread_set_ipc_tcb_cap_valid
                      check_cap_inv2[where Q="\<lambda>_. P"] cap_delete_P cap_insert_P
                      thread_set_P thread_set_P' set_mcpriority_P set_mcpriority_idle_thread
                      dxo_wp_weak hoare_weak_lift_imp)
                | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified] emptyable_def
                       del: hoare_True_E_R
                | wpc
                | strengthen use_no_cap_to_obj_asid_strg
                             tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"]
                             tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"])+) apply (unfold option_update_thread_def) apply (wp itr_wps thread_set_P thread_set_P'
         | simp add: emptyable_def | wpc)+  (*slow*)
   apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified]
                        is_cap_simps is_valid_vtable_root_def
                        is_cnode_or_valid_arch_def tcb_cap_valid_def
                        tcb_at_st_tcb_at[symmetric] invs_valid_objs
                        cap_asid_def vs_cap_ref_def
                        clas_no_asid cli_no_irqs no_cap_to_idle_thread
                 split: option.split_asm
         | rule conjI)+  (* also slow *)
   done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and invs and tcb_inv_wf (ThreadControl t sl ep mcp prio croot vroot buf)\<rbrace> invoke_tcb (ThreadControl t sl ep mcp prio croot vroot buf) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and invs and tcb_inv_wf (ThreadControl t sl ep mcp prio croot vroot buf)\<rbrace> invoke_tcb (ThreadControl t sl ep mcp prio croot vroot buf) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and invs and (tcb_at t and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case croot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case vroot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case buf of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case buf of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s)) and (\<lambda>y. case ep of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) and (\<lambda>s. case prio of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and ex_nonz_cap_to t)\<rbrace> doE y <- liftE (option_update_thread t (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) ep);
y <- liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> set_mcpriority t (fst x2));
y <- case croot of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index 0);
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index 0))))
odE;
y <- case vroot of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index (Suc 0));
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index (Suc 0)))))
odE;
y <- case buf of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) t);
y <- liftE (case snd x2 of None \<Rightarrow> return () | Some x2 \<Rightarrow> check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (t = cur) (do_extended_op reschedule_required))
odE;
y <- liftE (case prio of None \<Rightarrow> return () | Some x2 \<Rightarrow> do_extended_op (set_priority t (fst x2)));
returnOk []
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q6\<rbrace> doE y <- liftE (option_update_thread t (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) ep);
y <- liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> set_mcpriority t (fst x2));
y <- case croot of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index 0);
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index 0))))
odE;
y <- case vroot of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index (Suc 0));
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index (Suc 0)))))
odE;
y <- case buf of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) t);
y <- liftE (case snd x2 of None \<Rightarrow> return () | Some x2 \<Rightarrow> check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (t = cur) (do_extended_op reschedule_required))
odE;
y <- liftE (case prio of None \<Rightarrow> return () | Some x2 \<Rightarrow> do_extended_op (set_priority t (fst x2)));
returnOk []
odE \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. (P and invs and (tcb_at t and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case croot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case vroot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case buf of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case buf of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s)) and (\<lambda>y. case ep of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) and (\<lambda>s. case prio of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and ex_nonz_cap_to t)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (2 subgoals):
 1. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?P'9\<rbrace> doE y <- liftE (option_update_thread t (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) ep);
y <- liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> set_mcpriority t (fst x2));
y <- case croot of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index 0);
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index 0))))
odE;
y <- case vroot of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index (Suc 0));
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index (Suc 0)))))
odE;
y <- case buf of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) t);
y <- liftE (case snd x2 of None \<Rightarrow> return () | Some x2 \<Rightarrow> check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (t = cur) (do_extended_op reschedule_required))
odE;
y <- liftE (case prio of None \<Rightarrow> return () | Some x2 \<Rightarrow> do_extended_op (set_priority t (fst x2)));
returnOk []
odE \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. (P and invs and (tcb_at t and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case croot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case vroot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case buf of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case buf of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s)) and (\<lambda>y. case ep of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) and (\<lambda>s. case prio of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and ex_nonz_cap_to t)) s \<Longrightarrow> (?P'9 and K (case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits)) s proof (prove)
goal (7 subgoals):
 1. \<And>y ya yb yc yd. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?B16 y ya yb yc yd\<rbrace> case prio of None \<Rightarrow> return () | Some x2 \<Rightarrow> do_extended_op (set_priority t (fst x2)) \<lbrace>\<lambda>ye. P\<rbrace>
 2. \<And>y ya yb yc. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?B15 y ya yb yc\<rbrace> case buf of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) t);
y <- liftE (case snd x2 of None \<Rightarrow> return () | Some x2 \<Rightarrow> check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (t = cur) (do_extended_op reschedule_required))
odE \<lbrace>?B16 y ya yb yc\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>y ya yb. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?B14 y ya yb\<rbrace> case vroot of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index (Suc 0));
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index (Suc 0)))))
odE \<lbrace>?B15 y ya yb\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>y ya. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?B13 y ya\<rbrace> case croot of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (t, tcb_cnode_index 0);
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap t) sl (cap_insert (fst x2) (snd x2) (t, tcb_cnode_index 0))))
odE \<lbrace>?B14 y ya\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>y. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?B12 y\<rbrace> liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> set_mcpriority t (fst x2)) \<lbrace>?B13 y\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 6. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?P'9\<rbrace> liftE (option_update_thread t (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) ep) \<lbrace>?B12\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 7. \<And>s. (P and invs and (tcb_at t and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case croot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case vroot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case buf of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case buf of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s)) and (\<lambda>y. case ep of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) and (\<lambda>s. case prio of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and ex_nonz_cap_to t)) s \<Longrightarrow> (?P'9 and K (case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits)) s proof (prove)
goal (4 subgoals):
 1. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?P'10312\<rbrace> option_update_thread t (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) ep \<lbrace>\<lambda>rv. P\<rbrace>
 2. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?P'10310\<rbrace> option_update_thread t (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) ep \<lbrace>\<lambda>rv s. (\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s\<rbrace>
 3. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?P'10308\<rbrace> option_update_thread t (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) ep \<lbrace>\<lambda>rv s. ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> (prio = None \<longrightarrow> (buf = None \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (snd (the buf) = None \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a aa b. snd (the buf) = Some (a, aa, b)) \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))))) \<and> ((\<exists>a b. prio = Some (a, b)) \<longrightarrow> (buf = None \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (snd (the buf) = None \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a aa b. snd (the buf) = Some (a, aa, b)) \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))))))\<rbrace>
 4. \<And>s. (P and invs and (tcb_at t and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case croot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case vroot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case buf of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case buf of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s)) and (\<lambda>y. case ep of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) and (\<lambda>s. case prio of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and ex_nonz_cap_to t)) s \<Longrightarrow> ((\<lambda>s. ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> ?P'10312 s) \<and> ?P'10310 s) \<and> ?P'10308 s) and K (case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits)) s proof (prove)
goal (4 subgoals):
 1. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?P'10312\<rbrace> case ep of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set ((tcb_fault_handler_update \<circ> (\<lambda>x y. x)) v) t \<lbrace>\<lambda>rv. P\<rbrace>
 2. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?P'10310\<rbrace> case ep of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set ((tcb_fault_handler_update \<circ> (\<lambda>x y. x)) v) t \<lbrace>\<lambda>rv s. (\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s\<rbrace>
 3. case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits \<Longrightarrow> \<lbrace>?P'10308\<rbrace> case ep of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set ((tcb_fault_handler_update \<circ> (\<lambda>x y. x)) v) t \<lbrace>\<lambda>rv s. ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> (prio = None \<longrightarrow> (buf = None \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (snd (the buf) = None \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a aa b. snd (the buf) = Some (a, aa, b)) \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))))) \<and> ((\<exists>a b. prio = Some (a, b)) \<longrightarrow> (buf = None \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (snd (the buf) = None \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a aa b. snd (the buf) = Some (a, aa, b)) \<longrightarrow> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s))) \<and> (vroot = None \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> P s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> P s \<and> tcb_at t s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> invs s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at t s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> invs s \<and> is_cnode_or_valid_arch (fst (the croot)) \<and> tcb_at t s \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))))))))\<rbrace>
 4. \<And>s. (P and invs and (tcb_at t and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case croot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case vroot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case buf of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case buf of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s)) and (\<lambda>y. case ep of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) and (\<lambda>s. case prio of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and ex_nonz_cap_to t)) s \<Longrightarrow> ((\<lambda>s. ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> invs s \<and> ?P'10312 s) \<and> ?P'10310 s) \<and> ?P'10308 s) and K (case ep of None \<Rightarrow> True | Some v \<Rightarrow> length v = word_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<and> invs s \<and> tcb_at t s \<and> (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case croot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) \<and> (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s \<and> (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case vroot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) \<and> (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case buf of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (case buf of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> (case ep of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) \<and> (case prio of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) \<and> ex_nonz_cap_to t s \<Longrightarrow> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (vroot = None \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> (prio = None \<longrightarrow> (buf = None \<longrightarrow> (\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (snd (the buf) = None \<longrightarrow> (vroot = None \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a aa b. snd (the buf) = Some (a, aa, b)) \<longrightarrow> (vroot = None \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))))) \<and> ((\<exists>a b. prio = Some (a, b)) \<longrightarrow> (buf = None \<longrightarrow> (\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (snd (the buf) = None \<longrightarrow> (vroot = None \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a aa b. snd (the buf) = Some (a, aa, b)) \<longrightarrow> (vroot = None \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<and> invs s \<and> tcb_at t s \<and> (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case croot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) \<and> (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s \<and> (case croot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case vroot of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) \<and> (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case vroot of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case buf of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (case buf of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) \<and> (case buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) sl s \<and> ex_cte_cap_wp_to (\<lambda>_. True) sl s) \<and> (case ep of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) \<and> (case prio of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) \<and> ex_nonz_cap_to t s \<Longrightarrow> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (vroot = None \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> (prio = None \<longrightarrow> (buf = None \<longrightarrow> (\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (snd (the buf) = None \<longrightarrow> (vroot = None \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a aa b. snd (the buf) = Some (a, aa, b)) \<longrightarrow> (vroot = None \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))))) \<and> ((\<exists>a b. prio = Some (a, b)) \<longrightarrow> (buf = None \<longrightarrow> (\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a b. buf = Some (a, b)) \<longrightarrow> (snd (the buf) = None \<longrightarrow> (vroot = None \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))) \<and> ((\<exists>a aa b. snd (the buf) = Some (a, aa, b)) \<longrightarrow> (vroot = None \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))) \<and> ((\<exists>a aa b. vroot = Some (a, aa, b)) \<longrightarrow> (croot = None \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> (croot = None \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the vroot))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the vroot)) \<or> NullCap = fst (the vroot)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> (croot = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the vroot)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the vroot))) \<and> (is_pd_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> (is_pt_cap (fst (the vroot)) \<longrightarrow> (croot = None \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (\<exists>y. cap_asid (fst (the vroot)) = Some y))) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> no_cap_to_obj_dr_emp (fst (the vroot)) s)) \<and> ((\<exists>a aa b. croot = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y))) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the croot)) \<and> s \<turnstile> fst (the croot) \<and> no_cap_to_obj_dr_emp (fst (the croot)) s \<and> cte_wp_at (\<lambda>_. True) (snd (the croot)) s \<and> (is_pd_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)) \<and> (is_pt_cap (fst (the croot)) \<longrightarrow> (\<exists>y. cap_asid (fst (the croot)) = Some y)))))))) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!