theory ArchTcb_AI

lemma tc_invs[Tcb_AI_asms]:
  "\<lbrace>invs and tcb_at a
       and (case_option \<top> (valid_cap o fst) e)
       and (case_option \<top> (valid_cap o fst) f)
       and (case_option \<top> (case_option \<top> (valid_cap o fst) o snd) g)
       and (case_option \<top> (cte_at o snd) e)
       and (case_option \<top> (cte_at o snd) f)
       and (case_option \<top> (case_option \<top> (cte_at o snd) o snd) g)
       and (case_option \<top> (no_cap_to_obj_dr_emp o fst) e)
       and (case_option \<top> (no_cap_to_obj_dr_emp o fst) f)
       and (case_option \<top> (case_option \<top> (no_cap_to_obj_dr_emp o fst) o snd) g)
       \<comment> \<open>only set prio \<le> mcp of authorising thread\<close>
       and (\<lambda>s. case_option True (\<lambda>(pr, auth). mcpriority_tcb_at (\<lambda>mcp. pr \<le> mcp) auth s) pr)
       \<comment> \<open>only set mcp \<le> mcp of authorising thread\<close>
       and (\<lambda>s. case_option True (\<lambda>(mcp, auth). mcpriority_tcb_at (\<lambda>m. mcp \<le> m) auth s) mcp)
       and K (case_option True (is_cnode_cap o fst) e)
       and K (case_option True (is_valid_vtable_root o fst) f)
       and K (case_option True (\<lambda>v. case_option True
                          ((swp valid_ipc_buffer_cap (fst v)
                             and is_arch_cap and is_cnode_or_valid_arch)
                                o fst) (snd v)) g)
       and K (case_option True (\<lambda>bl. length bl = word_bits) b)\<rbrace>
      invoke_tcb (ThreadControl a sl b mcp pr e f g)
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (rule hoare_gen_asm)+ apply (simp add: split_def set_mcpriority_def cong: option.case_cong) apply (rule hoare_vcg_precond_imp) apply wp 
      (* takes long: (30 sec) *)
       apply ((simp only: simp_thms cong: conj_cong
        | (strengthen invs_strengthen)+
        | 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 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
             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_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI]
             thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI]
             checked_insert_no_cap_to
             out_no_cap_to_trivial[OF ball_tcb_cap_casesI]
             thread_set_ipc_tcb_cap_valid
             hoare_weak_lift_imp hoare_weak_lift_imp_conj)[1]
        | 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 (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] is_nondevice_page_cap_arch_def
                        is_cap_simps is_valid_vtable_root_def is_nondevice_page_cap_simps
                        is_cnode_or_valid_arch_def tcb_cap_valid_def
                        invs_valid_objs cap_asid_def vs_cap_ref_def
                 split: option.split_asm )+ apply (simp add: case_bool_If valid_ipc_buffer_cap_def is_nondevice_page_cap_simps
                       is_nondevice_page_cap_arch_def
                split: arch_cap.splits if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at a and (case e of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap \<circ> fst) x) and (case f of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap \<circ> fst) x) and (case g of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (case_option (\<lambda>_. True) (valid_cap \<circ> fst) \<circ> snd) x) and (case e of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (cte_wp_at (\<lambda>_. True) \<circ> snd) x) and (case f of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (cte_wp_at (\<lambda>_. True) \<circ> snd) x) and (case g of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (case_option (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) \<circ> snd) \<circ> snd) x) and (case e of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (no_cap_to_obj_dr_emp \<circ> fst) x) and (case f of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (no_cap_to_obj_dr_emp \<circ> fst) x) and (case g of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (case_option (\<lambda>_. True) (no_cap_to_obj_dr_emp \<circ> fst) \<circ> snd) x) and (\<lambda>s. case pr of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (mcp, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) mcp) auth s) and K (case e of None \<Rightarrow> True | Some x \<Rightarrow> (is_cnode_cap \<circ> fst) x) and K (case f of None \<Rightarrow> True | Some x \<Rightarrow> (is_valid_vtable_root \<circ> fst) x) and K (case g of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x \<Rightarrow> ((swp valid_ipc_buffer_cap (fst v) and is_arch_cap and is_cnode_or_valid_arch) \<circ> fst) x) and K (case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits)\<rbrace> invoke_tcb (ThreadControl a sl b mcp pr e f g) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x \<Rightarrow> ((swp valid_ipc_buffer_cap (fst v) and is_arch_cap and is_cnode_or_valid_arch) \<circ> fst) x; case f of None \<Rightarrow> True | Some x \<Rightarrow> (is_valid_vtable_root \<circ> fst) x; case e of None \<Rightarrow> True | Some x \<Rightarrow> (is_cnode_cap \<circ> fst) x\<rbrakk> \<Longrightarrow> \<lbrace>invs and tcb_at a and (case e of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap \<circ> fst) x) and (case f of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap \<circ> fst) x) and (case g of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (case_option (\<lambda>_. True) (valid_cap \<circ> fst) \<circ> snd) x) and (case e of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (cte_wp_at (\<lambda>_. True) \<circ> snd) x) and (case f of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (cte_wp_at (\<lambda>_. True) \<circ> snd) x) and (case g of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (case_option (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) \<circ> snd) \<circ> snd) x) and (case e of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (no_cap_to_obj_dr_emp \<circ> fst) x) and (case f of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (no_cap_to_obj_dr_emp \<circ> fst) x) and (case g of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (case_option (\<lambda>_. True) (no_cap_to_obj_dr_emp \<circ> fst) \<circ> snd) x) and (\<lambda>s. case pr of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (mcp, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) mcp) auth s)\<rbrace> invoke_tcb (ThreadControl a sl b mcp pr e f g) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>invs and tcb_at a and (case e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case g 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 e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) and (case g 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 (case e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case g 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>s. case pr 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)\<rbrace> doE y <- liftE (option_update_thread a (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) b);
y <- liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> thread_set (tcb_mcpriority_update (\<lambda>_. fst x2)) a);
y <- case e of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 0);
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index 0))))
odE;
y <- case f of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index (Suc 0));
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index (Suc 0)))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) a);
y <- liftE (case snd x2 of None \<Rightarrow> return () | Some x2 \<Rightarrow> check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (a = cur) (do_extended_op reschedule_required))
odE;
y <- liftE (case pr of None \<Rightarrow> return () | Some x2 \<Rightarrow> do_extended_op (set_priority a (fst x2)));
returnOk []
odE \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> doE y <- liftE (option_update_thread a (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) b);
y <- liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> thread_set (tcb_mcpriority_update (\<lambda>_. fst x2)) a);
y <- case e of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 0);
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index 0))))
odE;
y <- case f of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index (Suc 0));
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index (Suc 0)))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) a);
y <- liftE (case snd x2 of None \<Rightarrow> return () | Some x2 \<Rightarrow> check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (a = cur) (do_extended_op reschedule_required))
odE;
y <- liftE (case pr of None \<Rightarrow> return () | Some x2 \<Rightarrow> do_extended_op (set_priority a (fst x2)));
returnOk []
odE \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2); (invs and tcb_at a and (case e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case g 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 e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) and (case g 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 (case e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case g 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>s. case pr 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)) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (7 subgoals):
 1. \<And>y ya yb yc yd. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B17 y ya yb yc yd\<rbrace> case pr of None \<Rightarrow> return () | Some x2 \<Rightarrow> do_extended_op (set_priority a (fst x2)) \<lbrace>\<lambda>ye. invs\<rbrace>
 2. \<And>y ya yb yc. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B16 y ya yb yc\<rbrace> case g of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) a);
y <- liftE (case snd x2 of None \<Rightarrow> return () | Some x2 \<Rightarrow> check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (a = cur) (do_extended_op reschedule_required))
odE \<lbrace>?B17 y ya yb yc\<rbrace>, \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>y ya yb. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B15 y ya yb\<rbrace> case f of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index (Suc 0));
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index (Suc 0)))))
odE \<lbrace>?B16 y ya yb\<rbrace>, \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>y ya. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B14 y ya\<rbrace> case e of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 0);
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index 0))))
odE \<lbrace>?B15 y ya\<rbrace>, \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>y. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 y\<rbrace> liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> thread_set (tcb_mcpriority_update (\<lambda>_. fst x2)) a) \<lbrace>?B14 y\<rbrace>, \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> liftE (option_update_thread a (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) b) \<lbrace>?B13\<rbrace>, \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>s. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2); (invs and tcb_at a and (case e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case g 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 e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) and (case g 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 (case e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case g 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>s. case pr 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)) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (7 subgoals):
 1. \<And>y ya yb yc yd. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B17 y ya yb yc yd\<rbrace> case pr of None \<Rightarrow> return () | Some x2 \<Rightarrow> do_extended_op (set_priority a (fst x2)) \<lbrace>\<lambda>ye. invs\<rbrace>
 2. \<And>y ya yb yc. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B16 y ya yb yc\<rbrace> case g of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) a);
y <- liftE (case snd x2 of None \<Rightarrow> return () | Some x2 \<Rightarrow> check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (a = cur) (do_extended_op reschedule_required))
odE \<lbrace>?B17 y ya yb yc\<rbrace>, \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>y ya yb. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B15 y ya yb\<rbrace> case f of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index (Suc 0));
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index (Suc 0)))))
odE \<lbrace>?B16 y ya yb\<rbrace>, \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>y ya. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B14 y ya\<rbrace> case e of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 0);
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap a) sl (cap_insert (fst x2) (snd x2) (a, tcb_cnode_index 0))))
odE \<lbrace>?B15 y ya\<rbrace>, \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>y. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B13 y\<rbrace> liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> thread_set (tcb_mcpriority_update (\<lambda>_. fst x2)) a) \<lbrace>?B14 y\<rbrace>, \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> liftE (option_update_thread a (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) b) \<lbrace>?B13\<rbrace>, \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>s. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2); (invs and tcb_at a and (case e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case g 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 e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) and (case g 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 (case e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case g 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>s. case pr 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)) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>case b of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case g 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); case f of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case e of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2); invs s \<and> tcb_at a s \<and> (case e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case g 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 e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) s \<and> (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) s \<and> (case g 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)) s \<and> (case e of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case f of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case g 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 pr 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)\<rbrakk> \<Longrightarrow> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the e)) \<and> (mcp = None \<longrightarrow> s \<turnstile> fst (the e)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the e)) \<and> (is_pt_cap (fst (the e)) \<longrightarrow> (\<exists>y. cap_asid (fst (the e)) = Some y)) \<and> (is_pd_cap (fst (the e)) \<longrightarrow> (\<exists>y. cap_asid (fst (the e)) = Some y)) \<and> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the e)) s) \<and> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s)) \<and> ((\<exists>a aa b. f = Some (a, aa, b)) \<longrightarrow> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the e)) \<and> (mcp = None \<longrightarrow> s \<turnstile> fst (the e)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the e)) \<and> (is_pt_cap (fst (the e)) \<longrightarrow> (\<exists>y. cap_asid (fst (the e)) = Some y)) \<and> (is_pd_cap (fst (the e)) \<longrightarrow> (\<exists>y. cap_asid (fst (the e)) = Some y)) \<and> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the e)) s) \<and> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s)) \<and> (e = None \<longrightarrow> is_cnode_or_valid_arch (fst (the f))) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the f))) \<and> (e = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the f)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the f))) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the f)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the f))) \<and> (e = None \<longrightarrow> is_valid_vtable_root (fst (the f)) \<or> NullCap = fst (the f)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the f)) \<or> NullCap = fst (the f)) \<and> (e = None \<longrightarrow> (is_pt_cap (fst (the f)) \<longrightarrow> (\<exists>y. cap_asid (fst (the f)) = Some y)) \<and> (is_pd_cap (fst (the f)) \<longrightarrow> (\<exists>y. cap_asid (fst (the f)) = Some y))) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (is_pt_cap (fst (the f)) \<longrightarrow> (\<exists>y. cap_asid (fst (the f)) = Some y)) \<and> (is_pd_cap (fst (the f)) \<longrightarrow> (\<exists>y. cap_asid (fst (the f)) = Some y))) \<and> (e = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the f)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the f)) s)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the f)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the f)) s)) \<and> (e = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s) \<and> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s))) \<and> ((\<exists>a b. g = Some (a, b)) \<longrightarrow> ((\<exists>a aa b. f = Some (a, aa, b)) \<longrightarrow> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the e)) \<and> (mcp = None \<longrightarrow> s \<turnstile> fst (the e)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the e)) \<and> (is_pt_cap (fst (the e)) \<longrightarrow> (\<exists>y. cap_asid (fst (the e)) = Some y)) \<and> (is_pd_cap (fst (the e)) \<longrightarrow> (\<exists>y. cap_asid (fst (the e)) = Some y)) \<and> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the e)) s) \<and> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s)) \<and> (e = None \<longrightarrow> is_cnode_or_valid_arch (fst (the f))) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch (fst (the f))) \<and> (e = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the f)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the f))) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> fst (the f)) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> fst (the f))) \<and> (e = None \<longrightarrow> is_valid_vtable_root (fst (the f)) \<or> NullCap = fst (the f)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_valid_vtable_root (fst (the f)) \<or> NullCap = fst (the f)) \<and> (e = None \<longrightarrow> (is_pt_cap (fst (the f)) \<longrightarrow> (\<exists>y. cap_asid (fst (the f)) = Some y)) \<and> (is_pd_cap (fst (the f)) \<longrightarrow> (\<exists>y. cap_asid (fst (the f)) = Some y))) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (is_pt_cap (fst (the f)) \<longrightarrow> (\<exists>y. cap_asid (fst (the f)) = Some y)) \<and> (is_pd_cap (fst (the f)) \<longrightarrow> (\<exists>y. cap_asid (fst (the f)) = Some y))) \<and> (e = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the f)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the f)) s)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the f)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (snd (the f)) s)) \<and> (e = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s) \<and> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s))) \<and> (\<forall>a aa b. snd (the g) = Some (a, aa, b) \<longrightarrow> (f = None \<longrightarrow> (e = None \<longrightarrow> is_cnode_or_valid_arch a) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch a)) \<and> ((\<exists>a aa b. f = Some (a, aa, b)) \<longrightarrow> (e = None \<longrightarrow> is_cnode_or_valid_arch a) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_cnode_or_valid_arch a)) \<and> (f = None \<longrightarrow> (e = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> a) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> a)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> a) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> a))) \<and> ((\<exists>a aa b. f = Some (a, aa, b)) \<longrightarrow> (e = None \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> a) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> a)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> s \<turnstile> a) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> s \<turnstile> a))) \<and> (f = None \<longrightarrow> (e = None \<longrightarrow> is_nondevice_page_cap a) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_nondevice_page_cap a)) \<and> ((\<exists>a aa b. f = Some (a, aa, b)) \<longrightarrow> (e = None \<longrightarrow> is_nondevice_page_cap a) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> is_nondevice_page_cap a)) \<and> (f = None \<longrightarrow> (e = None \<longrightarrow> valid_ipc_buffer_cap a (fst (the g))) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> valid_ipc_buffer_cap a (fst (the g)))) \<and> ((\<exists>a aa b. f = Some (a, aa, b)) \<longrightarrow> (e = None \<longrightarrow> valid_ipc_buffer_cap a (fst (the g))) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> valid_ipc_buffer_cap a (fst (the g)))) \<and> (f = None \<longrightarrow> (e = None \<longrightarrow> (is_pt_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)) \<and> (is_pd_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y))) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (is_pt_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)) \<and> (is_pd_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)))) \<and> ((\<exists>a aa b. f = Some (a, aa, b)) \<longrightarrow> (e = None \<longrightarrow> (is_pt_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)) \<and> (is_pd_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y))) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (is_pt_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)) \<and> (is_pd_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)))) \<and> (f = None \<longrightarrow> (e = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) s)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) s))) \<and> ((\<exists>a aa b. f = Some (a, aa, b)) \<longrightarrow> (e = None \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) s)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (aa, b) s))) \<and> (f = None \<longrightarrow> (e = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp a s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp a s)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp a s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp a s) \<and> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s))) \<and> ((\<exists>a aa b. f = Some (a, aa, b)) \<longrightarrow> (e = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp a s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp a s)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp a s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp a s) \<and> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s)) \<and> (e = None \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s)) \<and> ((\<exists>a aa b. e = Some (a, aa, b)) \<longrightarrow> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the f)) s) \<and> (mcp = None \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s) \<and> ((\<exists>a b. mcp = Some (a, b)) \<longrightarrow> no_cap_to_obj_dr_emp (fst (the e)) s))))) proof (prove)
goal (32 subgoals):
 1. \<And>s aa ac ae bb. \<lbrakk>g = Some (aa, Some (ArchObjectCap ac, ae, bb)); f = None; e = None; b = None; invs s; tcb_at a s; s \<turnstile> ArchObjectCap ac; cte_wp_at (\<lambda>_. True) (ae, bb) s; no_cap_to_obj_dr_emp (ArchObjectCap ac) s; pr = None; valid_ipc_buffer_cap (ArchObjectCap ac) aa; mcp = None; (\<exists>p asid. ac = PageTableCap p asid) \<longrightarrow> (\<exists>y. (case ac of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); (\<exists>p asid. ac = PageDirectoryCap p asid) \<longrightarrow> (\<exists>y. (case ac of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y)\<rbrakk> \<Longrightarrow> case ac of PageCap True obj_ref rights sz vr \<Rightarrow> False | PageCap False obj_ref rights sz vr \<Rightarrow> True | _ \<Rightarrow> False
 2. \<And>s aa ac ad bb af bc. \<lbrakk>g = Some (aa, Some (ArchObjectCap ac, af, bc)); f = None; e = None; b = None; invs s; tcb_at a s; s \<turnstile> ArchObjectCap ac; cte_wp_at (\<lambda>_. True) (af, bc) s; no_cap_to_obj_dr_emp (ArchObjectCap ac) s; pr = None; valid_ipc_buffer_cap (ArchObjectCap ac) aa; (\<exists>p asid. ac = PageTableCap p asid) \<longrightarrow> (\<exists>y. (case ac of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); (\<exists>p asid. ac = PageDirectoryCap p asid) \<longrightarrow> (\<exists>y. (case ac of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); mcp = Some (ad, bb); mcpriority_tcb_at ((\<le>) ad) bb s\<rbrakk> \<Longrightarrow> case ac of PageCap True obj_ref rights sz vr \<Rightarrow> False | PageCap False obj_ref rights sz vr \<Rightarrow> True | _ \<Rightarrow> False
 3. \<And>s aa ac bb ad af bc. \<lbrakk>g = Some (aa, Some (ArchObjectCap ad, af, bc)); f = None; e = None; b = None; invs s; tcb_at a s; s \<turnstile> ArchObjectCap ad; cte_wp_at (\<lambda>_. True) (af, bc) s; no_cap_to_obj_dr_emp (ArchObjectCap ad) s; valid_ipc_buffer_cap (ArchObjectCap ad) aa; pr = Some (ac, bb); mcpriority_tcb_at ((\<le>) ac) bb s; mcp = None; (\<exists>p asid. ad = PageTableCap p asid) \<longrightarrow> (\<exists>y. (case ad of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); (\<exists>p asid. ad = PageDirectoryCap p asid) \<longrightarrow> (\<exists>y. (case ad of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y)\<rbrakk> \<Longrightarrow> case ad of PageCap True obj_ref rights sz vr \<Rightarrow> False | PageCap False obj_ref rights sz vr \<Rightarrow> True | _ \<Rightarrow> False
 4. \<And>s aa ac bb ad ae bc ag bd. \<lbrakk>g = Some (aa, Some (ArchObjectCap ad, ag, bd)); f = None; e = None; b = None; invs s; tcb_at a s; s \<turnstile> ArchObjectCap ad; cte_wp_at (\<lambda>_. True) (ag, bd) s; no_cap_to_obj_dr_emp (ArchObjectCap ad) s; valid_ipc_buffer_cap (ArchObjectCap ad) aa; pr = Some (ac, bb); mcpriority_tcb_at ((\<le>) ac) bb s; (\<exists>p asid. ad = PageTableCap p asid) \<longrightarrow> (\<exists>y. (case ad of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); (\<exists>p asid. ad = PageDirectoryCap p asid) \<longrightarrow> (\<exists>y. (case ad of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); mcp = Some (ae, bc); mcpriority_tcb_at ((\<le>) ae) bc s\<rbrakk> \<Longrightarrow> case ad of PageCap True obj_ref rights sz vr \<Rightarrow> False | PageCap False obj_ref rights sz vr \<Rightarrow> True | _ \<Rightarrow> False
 5. \<And>s aa ab ba r bits ga ae ag bc. \<lbrakk>g = Some (aa, Some (ArchObjectCap ae, ag, bc)); f = None; e = Some (CNodeCap r bits ga, ab, ba); b = None; invs s; tcb_at a s; s \<turnstile> CNodeCap r bits ga; s \<turnstile> ArchObjectCap ae; cte_wp_at (\<lambda>_. True) (ab, ba) s; cte_wp_at (\<lambda>_. True) (ag, bc) s; no_cap_to_obj_dr_emp (CNodeCap r bits ga) s; no_cap_to_obj_dr_emp (ArchObjectCap ae) s; pr = None; valid_ipc_buffer_cap (ArchObjectCap ae) aa; mcp = None; (\<exists>p asid. ae = PageTableCap p asid) \<longrightarrow> (\<exists>y. (case ae of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); (\<exists>p asid. ae = PageDirectoryCap p asid) \<longrightarrow> (\<exists>y. (case ae of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y)\<rbrakk> \<Longrightarrow> case ae of PageCap True obj_ref rights sz vr \<Rightarrow> False | PageCap False obj_ref rights sz vr \<Rightarrow> True | _ \<Rightarrow> False
 6. \<And>s aa ab ba r bits ga ae af bc ah bd. \<lbrakk>g = Some (aa, Some (ArchObjectCap ae, ah, bd)); f = None; e = Some (CNodeCap r bits ga, ab, ba); b = None; invs s; tcb_at a s; s \<turnstile> CNodeCap r bits ga; s \<turnstile> ArchObjectCap ae; cte_wp_at (\<lambda>_. True) (ab, ba) s; cte_wp_at (\<lambda>_. True) (ah, bd) s; no_cap_to_obj_dr_emp (CNodeCap r bits ga) s; no_cap_to_obj_dr_emp (ArchObjectCap ae) s; pr = None; valid_ipc_buffer_cap (ArchObjectCap ae) aa; (\<exists>p asid. ae = PageTableCap p asid) \<longrightarrow> (\<exists>y. (case ae of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); (\<exists>p asid. ae = PageDirectoryCap p asid) \<longrightarrow> (\<exists>y. (case ae of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); mcp = Some (af, bc); mcpriority_tcb_at ((\<le>) af) bc s\<rbrakk> \<Longrightarrow> case ae of PageCap True obj_ref rights sz vr \<Rightarrow> False | PageCap False obj_ref rights sz vr \<Rightarrow> True | _ \<Rightarrow> False
 7. \<And>s aa ab ba r bits ga ae bc af ah bd. \<lbrakk>g = Some (aa, Some (ArchObjectCap af, ah, bd)); f = None; e = Some (CNodeCap r bits ga, ab, ba); b = None; invs s; tcb_at a s; s \<turnstile> CNodeCap r bits ga; s \<turnstile> ArchObjectCap af; cte_wp_at (\<lambda>_. True) (ab, ba) s; cte_wp_at (\<lambda>_. True) (ah, bd) s; no_cap_to_obj_dr_emp (CNodeCap r bits ga) s; no_cap_to_obj_dr_emp (ArchObjectCap af) s; valid_ipc_buffer_cap (ArchObjectCap af) aa; pr = Some (ae, bc); mcpriority_tcb_at ((\<le>) ae) bc s; mcp = None; (\<exists>p asid. af = PageTableCap p asid) \<longrightarrow> (\<exists>y. (case af of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); (\<exists>p asid. af = PageDirectoryCap p asid) \<longrightarrow> (\<exists>y. (case af of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y)\<rbrakk> \<Longrightarrow> case af of PageCap True obj_ref rights sz vr \<Rightarrow> False | PageCap False obj_ref rights sz vr \<Rightarrow> True | _ \<Rightarrow> False
 8. \<And>s aa ab ba r bits ga ae bc af ag bd ai be. \<lbrakk>g = Some (aa, Some (ArchObjectCap af, ai, be)); f = None; e = Some (CNodeCap r bits ga, ab, ba); b = None; invs s; tcb_at a s; s \<turnstile> CNodeCap r bits ga; s \<turnstile> ArchObjectCap af; cte_wp_at (\<lambda>_. True) (ab, ba) s; cte_wp_at (\<lambda>_. True) (ai, be) s; no_cap_to_obj_dr_emp (CNodeCap r bits ga) s; no_cap_to_obj_dr_emp (ArchObjectCap af) s; valid_ipc_buffer_cap (ArchObjectCap af) aa; pr = Some (ae, bc); mcpriority_tcb_at ((\<le>) ae) bc s; (\<exists>p asid. af = PageTableCap p asid) \<longrightarrow> (\<exists>y. (case af of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); (\<exists>p asid. af = PageDirectoryCap p asid) \<longrightarrow> (\<exists>y. (case af of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); mcp = Some (ag, bd); mcpriority_tcb_at ((\<le>) ag) bd s\<rbrakk> \<Longrightarrow> case af of PageCap True obj_ref rights sz vr \<Rightarrow> False | PageCap False obj_ref rights sz vr \<Rightarrow> True | _ \<Rightarrow> False
 9. \<And>s aa ab ba r ac aaa ag bc. \<lbrakk>g = Some (aa, Some (ArchObjectCap aaa, ag, bc)); f = Some (ArchObjectCap (PageDirectoryCap r (Some ac)), ab, ba); e = None; b = None; invs s; tcb_at a s; s \<turnstile> ArchObjectCap (PageDirectoryCap r (Some ac)); s \<turnstile> ArchObjectCap aaa; cte_wp_at (\<lambda>_. True) (ab, ba) s; cte_wp_at (\<lambda>_. True) (ag, bc) s; no_cap_to_obj_dr_emp (ArchObjectCap (PageDirectoryCap r (Some ac))) s; no_cap_to_obj_dr_emp (ArchObjectCap aaa) s; pr = None; valid_ipc_buffer_cap (ArchObjectCap aaa) aa; mcp = None; (\<exists>p asid. aaa = PageTableCap p asid) \<longrightarrow> (\<exists>y. (case aaa of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); (\<exists>p asid. aaa = PageDirectoryCap p asid) \<longrightarrow> (\<exists>y. (case aaa of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y)\<rbrakk> \<Longrightarrow> case aaa of PageCap True obj_ref rights sz vr \<Rightarrow> False | PageCap False obj_ref rights sz vr \<Rightarrow> True | _ \<Rightarrow> False
 10. \<And>s aa ab ba r ac aaa af bc ah bd. \<lbrakk>g = Some (aa, Some (ArchObjectCap aaa, ah, bd)); f = Some (ArchObjectCap (PageDirectoryCap r (Some ac)), ab, ba); e = None; b = None; invs s; tcb_at a s; s \<turnstile> ArchObjectCap (PageDirectoryCap r (Some ac)); s \<turnstile> ArchObjectCap aaa; cte_wp_at (\<lambda>_. True) (ab, ba) s; cte_wp_at (\<lambda>_. True) (ah, bd) s; no_cap_to_obj_dr_emp (ArchObjectCap (PageDirectoryCap r (Some ac))) s; no_cap_to_obj_dr_emp (ArchObjectCap aaa) s; pr = None; valid_ipc_buffer_cap (ArchObjectCap aaa) aa; (\<exists>p asid. aaa = PageTableCap p asid) \<longrightarrow> (\<exists>y. (case aaa of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); (\<exists>p asid. aaa = PageDirectoryCap p asid) \<longrightarrow> (\<exists>y. (case aaa of PageCap dev obj_ref rights sz None \<Rightarrow> None | PageCap dev obj_ref rights sz (Some (asid, xd)) \<Rightarrow> Some asid | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, xaa)) \<Rightarrow> Some asid | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some xa) \<Rightarrow> Some xa | _ \<Rightarrow> None) = Some y); mcp = Some (af, bc); mcpriority_tcb_at ((\<le>) af) bc s\<rbrakk> \<Longrightarrow> case aaa of PageCap True obj_ref rights sz vr \<Rightarrow> False | PageCap False obj_ref rights sz vr \<Rightarrow> True | _ \<Rightarrow> False
A total of 32 subgoals... proof (prove)
goal:
No subgoals!