theory ArchFinalCaps

lemma invoke_tcb_silc_inv[FinalCaps_assms]:
  notes hoare_weak_lift_imp [wp]
        hoare_weak_lift_imp_conj [wp]
  shows "\<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv
                          and K (authorised_tcb_inv aag tinv)\<rbrace>
         invoke_tcb tinv
         \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (case_tac tinv) apply ((wp restart_silc_inv hoare_vcg_if_lift suspend_silc_inv mapM_x_wp[OF _ subset_refl]
                    hoare_weak_lift_imp
                 | wpc
                 | simp split del: if_split add: authorised_tcb_inv_def check_cap_at_def
                 | clarsimp
                 | strengthen invs_mdb
                 | force intro: notE[rotated,OF idle_no_ex_cap,simplified])+)[3] defer apply ((wp suspend_silc_inv restart_silc_inv | simp add: authorised_tcb_inv_def | force)+)[2] 
    (* NotificationControl *)
     apply (rename_tac option) apply (case_tac option; (wp | simp)+) 
   (* SetTLSBase *)
    apply (wpsimp split: option.splits) 
  (* just ThreadControl left *)
   apply (simp add: split_def cong: option.case_cong) 
  (* slow, ~2 mins *)
   apply (simp only: conj_ac cong: conj_cong imp_cong |
         wp checked_insert_pas_refined checked_cap_insert_silc_inv hoare_vcg_all_lift_R
            hoare_vcg_all_lift hoare_vcg_const_imp_lift_R
            cap_delete_silc_inv_not_transferable
            cap_delete_pas_refined' cap_delete_deletes
            cap_delete_valid_cap cap_delete_cte_at
            check_cap_inv[where P="valid_cap c" for c]
            check_cap_inv[where P="cte_at p0" for p0]
            check_cap_inv[where P="\<lambda>s. \<not> tcb_at t s" for t]
            check_cap_inv2[where Q="\<lambda>_. valid_list"]
            check_cap_inv2[where Q="\<lambda>_. valid_sched"]
            check_cap_inv2[where Q="\<lambda>_. simple_sched_action"]
            checked_insert_no_cap_to
            thread_set_tcb_fault_handler_update_invs
            thread_set_pas_refined thread_set_emptyable thread_set_valid_cap
            thread_set_not_state_valid_sched thread_set_cte_at
            thread_set_no_cap_to_trivial
        | wpc
        | simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def st_tcb_at_triv
                   option_update_thread_def
        | strengthen use_no_cap_to_obj_asid_strg invs_mdb
                    invs_psp_aligned invs_vspace_objs invs_arch_state
        | wp (once) hoare_drop_imps)+ apply (clarsimp simp: authorised_tcb_inv_def emptyable_def) 
  (* also slow, ~15s *)
   by (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def is_valid_vtable_root_def
      | intro impI
      | rule conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. tinv = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x21 x22 x23 x24. tinv = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37. tinv = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>x5. tinv = Suspend x5 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>x6. tinv = Resume x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x5. tinv = Suspend x5 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x6. tinv = Resume x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x5. tinv = Suspend x5 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x6. tinv = Resume x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 option. tinv = NotificationControl x71 option \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and (tcb_at x41 and (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case x46 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case x46 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 x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case x47 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case x47 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 x48 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 x48 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 x48 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case x48 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 x48 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. x46 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s) \<and> ((\<exists>a aa b. x47 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s) \<and> ((\<exists>a b. x48 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s)) and (\<lambda>y. case x43 of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) and (\<lambda>s. case x45 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and (\<lambda>s. case x44 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and ex_nonz_cap_to x41) and (\<lambda>y. authorised_tcb_inv aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48))\<rbrace> doE y <- liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43);
y <- liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> set_mcpriority x41 (fst x2));
y <- case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap x41) x42 (cap_insert (fst x2) (snd x2) (x41, tcb_cnode_index 0))))
odE;
y <- case x47 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index (Suc 0));
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap x41) x42 (cap_insert (fst x2) (snd x2) (x41, tcb_cnode_index (Suc 0)))))
odE;
y <- case x48 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) x41);
y <- liftE (case snd x2 of None \<Rightarrow> return () | Some x2 \<Rightarrow> check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap x41) x42 (cap_insert (fst x2) (snd x2) (x41, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (x41 = cur) reschedule_required)
odE;
y <- liftE (case x45 of None \<Rightarrow> return () | Some x2 \<Rightarrow> set_priority x41 (fst x2));
returnOk []
odE \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and (tcb_at x41 and (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case x46 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case x46 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 x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case x47 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case x47 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 x48 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 x48 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 x48 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case x48 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 x48 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. x46 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s) \<and> ((\<exists>a aa b. x47 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s) \<and> ((\<exists>a b. x48 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s)) and (\<lambda>y. case x43 of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) and (\<lambda>s. case x45 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and (\<lambda>s. case x44 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) and ex_nonz_cap_to x41) and (\<lambda>y. authorised_tcb_inv aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48))\<rbrace> doE y <- liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43);
y <- liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> set_mcpriority x41 (fst x2));
y <- case x46 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 0);
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap x41) x42 (cap_insert (fst x2) (snd x2) (x41, tcb_cnode_index 0))))
odE;
y <- case x47 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index (Suc 0));
liftE (check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap x41) x42 (cap_insert (fst x2) (snd x2) (x41, tcb_cnode_index (Suc 0)))))
odE;
y <- case x48 of None \<Rightarrow> returnOk () | Some x2 \<Rightarrow> doE y <- cap_delete (x41, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) x41);
y <- liftE (case snd x2 of None \<Rightarrow> return () | Some x2 \<Rightarrow> check_cap_at (fst x2) (snd x2) (check_cap_at (ThreadCap x41) x42 (cap_insert (fst x2) (snd x2) (x41, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (x41 = cur) reschedule_required)
odE;
y <- liftE (case x45 of None \<Rightarrow> return () | Some x2 \<Rightarrow> set_priority x41 (fst x2));
returnOk []
odE \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; invs s \<and> pas_refined aag s \<and> ex_nonz_cap_to x41 s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> tcb_at x41 s \<and> valid_list s \<and> (case x47 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) \<and> (case x46 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) \<and> (case x43 of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) \<and> (case x48 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s \<and> authorised_tcb_inv aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48) \<and> (case x44 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) \<and> (case x45 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) \<and> (case x48 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 x48 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 x46 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 x47 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> valid_sched s \<and> ((\<exists>a b. x48 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s) \<and> (case x48 of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_or_valid_arch (fst x2) \<and> is_arch_cap (fst x2) \<and> valid_ipc_buffer_cap (fst x2) (fst v)) \<and> (case x48 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. x46 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s) \<and> ((\<exists>a aa b. x47 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s)\<rbrakk> \<Longrightarrow> (x46 = None \<longrightarrow> (x47 = None \<longrightarrow> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> (x45 = None \<longrightarrow> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag x41 \<and> is_subject aag aa)) \<and> (x44 = None \<longrightarrow> (x43 = None \<longrightarrow> is_subject aag x41) \<and> (\<forall>x. x43 = Some x \<longrightarrow> length x = word_bits \<and> is_subject aag x41)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag x41 \<and> is_subject aag aa)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> (x43 = None \<longrightarrow> is_subject aag x41) \<and> (\<forall>x. x43 = Some x \<longrightarrow> length x = word_bits \<and> is_subject aag x41)))) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag x41 \<and> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag x41 \<and> is_subject aag xa)) \<and> (x44 = None \<longrightarrow> (x43 = None \<longrightarrow> is_subject aag x41 \<and> (\<forall>a b. x48 = Some (a, b) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> is_subject aag x41 \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa))))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> (x43 = None \<longrightarrow> is_subject aag x41 \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> is_subject aag x41 \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa))))))) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> (x44 = None \<longrightarrow> (x43 = None \<longrightarrow> is_subject aag x41 \<and> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>a b. x48 = Some (a, b) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>a aa b. x47 = Some (a, aa, b) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag aa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag aa)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch a \<and> \<not> is_master_reply_cap a \<and> s \<turnstile> a \<and> no_cap_to_obj_dr_emp a s \<and> pas_cap_cur_auth aag a \<and> (is_valid_vtable_root a \<or> NullCap = a) \<and> is_subject aag aa \<and> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> (is_pd_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)) \<and> (is_pt_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb))))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> is_subject aag x41 \<and> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc xd xe. x47 = Some (xc, xd, xe) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xd) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xd)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch xc \<and> \<not> is_master_reply_cap xc \<and> s \<turnstile> xc \<and> no_cap_to_obj_dr_emp xc s \<and> pas_cap_cur_auth aag xc \<and> (is_valid_vtable_root xc \<or> NullCap = xc) \<and> is_subject aag xd \<and> cte_wp_at (\<lambda>_. True) (xd, xe) s \<and> (is_pd_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (is_pt_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)))))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> (x43 = None \<longrightarrow> is_subject aag x41 \<and> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc xd xe. x47 = Some (xc, xd, xe) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xd) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xd)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch xc \<and> \<not> is_master_reply_cap xc \<and> s \<turnstile> xc \<and> no_cap_to_obj_dr_emp xc s \<and> pas_cap_cur_auth aag xc \<and> (is_valid_vtable_root xc \<or> NullCap = xc) \<and> is_subject aag xd \<and> cte_wp_at (\<lambda>_. True) (xd, xe) s \<and> (is_pd_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (is_pt_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb))))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> is_subject aag x41 \<and> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc xd xe. x47 = Some (xc, xd, xe) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xd) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xd)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch xc \<and> \<not> is_master_reply_cap xc \<and> s \<turnstile> xc \<and> no_cap_to_obj_dr_emp xc s \<and> pas_cap_cur_auth aag xc \<and> (is_valid_vtable_root xc \<or> NullCap = xc) \<and> is_subject aag xd \<and> cte_wp_at (\<lambda>_. True) (xd, xe) s \<and> (is_pd_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (is_pt_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb))))))) proof (prove)
goal (1 subgoal):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48; invs s; pas_refined aag s; ex_nonz_cap_to x41 s; simple_sched_action s; silc_inv aag st s; tcb_at x41 s; valid_list s; case x47 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case x46 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2); case x43 of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case x48 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s; (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s; is_subject aag x41; \<forall>x\<in>set_option x46 \<union> set_option x47 \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot); case x44 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s; case x45 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s; (case x48 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; (case x48 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; (case x46 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; (case x47 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; valid_sched s; (\<exists>a b. x48 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (a, b) s; case x48 of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_or_valid_arch (fst x2) \<and> is_arch_cap (fst x2) \<and> valid_ipc_buffer_cap (fst x2) (fst v); (case x48 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; (\<exists>a aa b. x46 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (a, b) s; (\<exists>a aa b. x47 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (a, b) s\<rbrakk> \<Longrightarrow> (x46 = None \<longrightarrow> (x47 = None \<longrightarrow> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> (x45 = None \<longrightarrow> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag aa)) \<and> (x44 = None \<longrightarrow> (\<forall>x. x43 = Some x \<longrightarrow> length x = word_bits)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag aa)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> (\<forall>x. x43 = Some x \<longrightarrow> length x = word_bits)))) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (x44 = None \<longrightarrow> (x43 = None \<longrightarrow> (\<forall>a b. x48 = Some (a, b) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa))))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> (x43 = None \<longrightarrow> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa))))))) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> (x44 = None \<longrightarrow> (x43 = None \<longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>a b. x48 = Some (a, b) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>a aa b. x47 = Some (a, aa, b) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag aa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag aa)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch a \<and> \<not> is_master_reply_cap a \<and> s \<turnstile> a \<and> no_cap_to_obj_dr_emp a s \<and> pas_cap_cur_auth aag a \<and> (is_valid_vtable_root a \<or> NullCap = a) \<and> is_subject aag aa \<and> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> (is_pd_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)) \<and> (is_pt_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb))))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc xd xe. x47 = Some (xc, xd, xe) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xd) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xd)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch xc \<and> \<not> is_master_reply_cap xc \<and> s \<turnstile> xc \<and> no_cap_to_obj_dr_emp xc s \<and> pas_cap_cur_auth aag xc \<and> (is_valid_vtable_root xc \<or> NullCap = xc) \<and> is_subject aag xd \<and> cte_wp_at (\<lambda>_. True) (xd, xe) s \<and> (is_pd_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (is_pt_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)))))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> (x43 = None \<longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc xd xe. x47 = Some (xc, xd, xe) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xd) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xd)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch xc \<and> \<not> is_master_reply_cap xc \<and> s \<turnstile> xc \<and> no_cap_to_obj_dr_emp xc s \<and> pas_cap_cur_auth aag xc \<and> (is_valid_vtable_root xc \<or> NullCap = xc) \<and> is_subject aag xd \<and> cte_wp_at (\<lambda>_. True) (xd, xe) s \<and> (is_pd_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (is_pt_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb))))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc xd xe. x47 = Some (xc, xd, xe) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xd) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xd)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch xc \<and> \<not> is_master_reply_cap xc \<and> s \<turnstile> xc \<and> no_cap_to_obj_dr_emp xc s \<and> pas_cap_cur_auth aag xc \<and> (is_valid_vtable_root xc \<or> NullCap = xc) \<and> is_subject aag xd \<and> cte_wp_at (\<lambda>_. True) (xd, xe) s \<and> (is_pd_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (is_pt_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb))))))) proof (prove)
goal (1 subgoal):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x48 s. \<lbrakk>tinv = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48; invs s; pas_refined aag s; ex_nonz_cap_to x41 s; simple_sched_action s; silc_inv aag st s; tcb_at x41 s; valid_list s; case x47 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); case x46 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2); case x43 of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case x48 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s; (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s; is_subject aag x41; \<forall>x\<in>set_option x46 \<union> set_option x47 \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot); case x44 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s; case x45 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s; (case x48 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; (case x48 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; (case x46 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; (case x47 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; valid_sched s; (\<exists>a b. x48 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (a, b) s; case x48 of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_or_valid_arch (fst x2) \<and> is_arch_cap (fst x2) \<and> valid_ipc_buffer_cap (fst x2) (fst v); (case x48 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; (\<exists>a aa b. x46 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (a, b) s; (\<exists>a aa b. x47 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (a, b) s\<rbrakk> \<Longrightarrow> (x46 = None \<longrightarrow> (x47 = None \<longrightarrow> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> (x45 = None \<longrightarrow> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag aa)) \<and> (x44 = None \<longrightarrow> (\<forall>x. x43 = Some x \<longrightarrow> length x = word_bits)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag aa)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> (\<forall>x. x43 = Some x \<longrightarrow> length x = word_bits)))) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (x44 = None \<longrightarrow> (x43 = None \<longrightarrow> (\<forall>a b. x48 = Some (a, b) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa))))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> (x43 = None \<longrightarrow> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> (is_valid_vtable_root x \<or> NullCap = x) \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa))))))) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> (x44 = None \<longrightarrow> (x43 = None \<longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>a b. x48 = Some (a, b) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>ba. b = Some (x, xa, ba)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>a aa b. x47 = Some (a, aa, b) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag aa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag aa)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch a \<and> \<not> is_master_reply_cap a \<and> s \<turnstile> a \<and> no_cap_to_obj_dr_emp a s \<and> pas_cap_cur_auth aag a \<and> (is_valid_vtable_root a \<or> NullCap = a) \<and> is_subject aag aa \<and> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> (is_pd_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)) \<and> (is_pt_cap a \<longrightarrow> (\<exists>y. cap_asid a = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb))))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc xd xe. x47 = Some (xc, xd, xe) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xd) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xd)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch xc \<and> \<not> is_master_reply_cap xc \<and> s \<turnstile> xc \<and> no_cap_to_obj_dr_emp xc s \<and> pas_cap_cur_auth aag xc \<and> (is_valid_vtable_root xc \<or> NullCap = xc) \<and> is_subject aag xd \<and> cte_wp_at (\<lambda>_. True) (xd, xe) s \<and> (is_pd_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (is_pt_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)))))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> (x43 = None \<longrightarrow> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc xd xe. x47 = Some (xc, xd, xe) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xd) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xd)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch xc \<and> \<not> is_master_reply_cap xc \<and> s \<turnstile> xc \<and> no_cap_to_obj_dr_emp xc s \<and> pas_cap_cur_auth aag xc \<and> (is_valid_vtable_root xc \<or> NullCap = xc) \<and> is_subject aag xd \<and> cte_wp_at (\<lambda>_. True) (xd, xe) s \<and> (is_pd_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (is_pt_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb))))) \<and> (\<forall>xc. x43 = Some xc \<longrightarrow> length xc = word_bits \<and> (x47 = None \<longrightarrow> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xa)) \<and> (\<forall>xc xd. x48 = Some (xc, xd) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xa. (\<exists>b. xd = Some (x, xa, b)) \<longrightarrow> is_subject aag xa)))) \<and> (\<forall>xc xd xe. x47 = Some (xc, xd, xe) \<longrightarrow> is_cnode_or_valid_arch x \<and> \<not> is_master_reply_cap x \<and> s \<turnstile> x \<and> no_cap_to_obj_dr_emp x s \<and> pas_cap_cur_auth aag x \<and> is_subject aag xa \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (x48 = None \<longrightarrow> (x45 = None \<longrightarrow> is_subject aag xd) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag xd)) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> is_cnode_or_valid_arch xc \<and> \<not> is_master_reply_cap xc \<and> s \<turnstile> xc \<and> no_cap_to_obj_dr_emp xc s \<and> pas_cap_cur_auth aag xc \<and> (is_valid_vtable_root xc \<or> NullCap = xc) \<and> is_subject aag xd \<and> cte_wp_at (\<lambda>_. True) (xd, xe) s \<and> (is_pd_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (is_pt_cap xc \<longrightarrow> (\<exists>y. cap_asid xc = Some y)) \<and> (x45 = None \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb)))))))