theory ArchTcb_IF

lemma tc_reads_respects_f[Tcb_IF_assms]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  and tc[simp]: "ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48"
  notes validE_valid[wp del] hoare_weak_lift_imp [wp]
  shows
    "reads_respects_f aag l
       (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action
                        and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti
                        and is_subject aag \<circ> cur_thread
                        and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti))
       (invoke_tcb ti)" apply (simp add: split_def cong: option.case_cong) apply (wpsimp wp: set_priority_reads_respects[THEN reads_respects_f[where  st=st and Q=\<top>]]) apply (wpsimp wp: hoare_vcg_const_imp_lift_R simp: when_def | wpc)+ apply (rule conjI) apply ((wpsimp wp: reschedule_required_reads_respects_f)+)[4] apply ((wp reads_respects_f[OF cap_insert_reads_respects, where st=st]
                           reads_respects_f[OF thread_set_reads_respects, where st=st and Q="\<top>"]
                           set_priority_reads_respects[THEN
                                               reads_respects_f[where aag=aag and st=st and Q=\<top>]]
                           set_mcpriority_reads_respects[THEN
                                               reads_respects_f[where aag=aag and st=st and Q=\<top>]]
                           check_cap_inv[OF check_cap_inv[OF cap_insert_valid_list]]
                           check_cap_inv[OF check_cap_inv[OF cap_insert_valid_sched]]
                           check_cap_inv[OF check_cap_inv[OF cap_insert_schedact]]
                           check_cap_inv[OF check_cap_inv[OF cap_insert_cur_domain]]
                           check_cap_inv[OF check_cap_inv[OF cap_insert_ct]]
                           get_thread_state_rev[THEN
                                               reads_respects_f[where aag=aag and st=st and Q=\<top>]]
                           hoare_vcg_all_lift_R hoare_vcg_all_lift
                           cap_delete_reads_respects[where st=st] checked_insert_pas_refined
                           thread_set_pas_refined
                           reads_respects_f[OF checked_insert_reads_respects, where st=st]
                           checked_cap_insert_silc_inv[where st=st]
                           cap_delete_silc_inv_not_transferable[where st=st]
                           checked_cap_insert_only_timer_irq_inv[where st=st' and irq=irq]
                           cap_delete_only_timer_irq_inv[where st=st' and irq=irq]
                           set_priority_only_timer_irq_inv[where st=st' and irq=irq]
                           set_mcpriority_only_timer_irq_inv[where st=st' and irq=irq]
                           cap_delete_deletes cap_delete_valid_cap cap_delete_cte_at
                           cap_delete_pas_refined' itr_wps(12) itr_wps(14) cap_insert_cte_at
                           checked_insert_no_cap_to hoare_vcg_const_imp_lift_R hoare_vcg_conj_lift
                           as_user_reads_respects_f thread_set_mdb cap_delete_invs
                      | wpc
                      | simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def
                                  tcb_at_st_tcb_at when_def
                      | strengthen use_no_cap_to_obj_asid_strg invs_mdb
                                   invs_psp_aligned invs_vspace_objs invs_arch_state
                      | solves auto)+)[7] apply ((simp add: conj_comms, strengthen imp_consequent[where Q="x = None" for x]
                                      , simp cong: conj_cong)
                 | wp reads_respects_f[OF cap_insert_reads_respects, where st=st]
                      reads_respects_f[OF thread_set_reads_respects, where st=st and Q="\<top>"]
                      set_priority_reads_respects[THEN reads_respects_f[where st=st and Q=\<top>]]
                      set_mcpriority_reads_respects[THEN reads_respects_f[where st=st and Q=\<top>]]
                      check_cap_inv[OF check_cap_inv[OF cap_insert_valid_list]]
                      check_cap_inv[OF check_cap_inv[OF cap_insert_valid_sched]]
                      check_cap_inv[OF check_cap_inv[OF cap_insert_schedact]]
                      check_cap_inv[OF check_cap_inv[OF cap_insert_cur_domain]]
                      check_cap_inv[OF check_cap_inv[OF cap_insert_ct]]
                      get_thread_state_rev[THEN reads_respects_f[where st=st and Q=\<top>]]
                      hoare_vcg_all_lift_R hoare_vcg_all_lift
                      cap_delete_reads_respects[where st=st] checked_insert_pas_refined
                      thread_set_pas_refined reads_respects_f[OF checked_insert_reads_respects]
                      checked_cap_insert_silc_inv[where st=st]
                      cap_delete_silc_inv_not_transferable[where st=st]
                      checked_cap_insert_only_timer_irq_inv[where st=st' and irq=irq]
                      cap_delete_only_timer_irq_inv[where st=st' and irq=irq]
                      set_priority_only_timer_irq_inv[where st=st' and irq=irq]
                      set_mcpriority_only_timer_irq_inv[where st=st' and irq=irq]
                      cap_delete_deletes cap_delete_valid_cap cap_delete_cte_at
                      cap_delete_pas_refined' itr_wps(12) itr_wps(14) cap_insert_cte_at
                      checked_insert_no_cap_to hoare_vcg_const_imp_lift_R
                      as_user_reads_respects_f cap_delete_invs
                 | wpc
                 | simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def when_def st_tcb_at_triv
                 | strengthen use_no_cap_to_obj_asid_strg invs_mdb
                              invs_psp_aligned invs_vspace_objs invs_arch_state
                 | wp (once) hoare_drop_imp)+ apply (simp add: option_update_thread_def tcb_cap_cases_def
           | wp hoare_weak_lift_imp hoare_weak_lift_imp_conj thread_set_pas_refined
                reads_respects_f[OF thread_set_reads_respects, where st=st and Q="\<top>"]
           | wpc)+ apply (wp hoare_vcg_all_lift thread_set_tcb_fault_handler_update_invs
             thread_set_tcb_fault_handler_update_silc_inv
             thread_set_not_state_valid_sched
             thread_set_pas_refined thread_set_emptyable thread_set_valid_cap
             thread_set_cte_at thread_set_no_cap_to_trivial
             thread_set_tcb_fault_handler_update_only_timer_irq_inv
          | simp add: tcb_cap_cases_def | wpc | wp (once) hoare_drop_imp)+ apply (clarsimp simp: authorised_tcb_inv_def  authorised_tcb_inv_extra_def emptyable_def) by (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def is_valid_vtable_root_def det_setRegister
      | intro impI conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain 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 is_subject aag \<circ> cur_thread and (\<lambda>y. authorised_tcb_inv aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48) \<and> authorised_tcb_inv_extra aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48))) (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) proof (prove)
goal (19 subgoals):
 1. \<And>a b rvg. x48 = Some (a, b) \<Longrightarrow> reads_respects_f aag l (?Q64 a b () () () () (a, b) () () () rvg) (when (x41 = rvg) reschedule_required)
 2. \<And>rv rva rvb rvc x2 rvd rve rvf. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'58 rv rva rvb rvc x2 rvd rve rvf) (liftE (gets cur_thread))
 3. \<And>rv rva rvb rvc x2 rvd rve rvf. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''58 rv rva rvb rvc x2 rvd rve rvf\<rbrace> liftE (gets cur_thread) \<lbrace>?Q64 (fst x2) (snd x2) rv rva rvb rvc x2 rvd rve rvf\<rbrace>, -
 4. \<And>rv rva rvb rvc x2 rvd rve. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'57 rv rva rvb rvc x2 rvd rve) (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)))))
 5. \<And>rv rva rvb rvc x2 rvd rve. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''57 rv rva rvb rvc x2 rvd rve\<rbrace> 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)))) \<lbrace>\<lambda>rvf s. ?P'58 rv rva rvb rvc x2 rvd rve rvf s \<and> ?P''58 rv rva rvb rvc x2 rvd rve rvf s\<rbrace>, -
 6. \<And>rv rva rvb rvc x2 rvd. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'56 rv rva rvb rvc x2 rvd) (liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) x41))
 7. \<And>rv rva rvb rvc x2 rvd. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''56 rv rva rvb rvc x2 rvd\<rbrace> liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) x41) \<lbrace>\<lambda>rve s. ?P'57 rv rva rvb rvc x2 rvd rve s \<and> ?P''57 rv rva rvb rvc x2 rvd rve s\<rbrace>, -
 8. \<And>rv rva rvb rvc x2. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'55 rv rva rvb rvc x2) (cap_delete (x41, tcb_cnode_index 4))
 9. \<And>rv rva rvb rvc x2. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''55 rv rva rvb rvc x2\<rbrace> cap_delete (x41, tcb_cnode_index 4) \<lbrace>\<lambda>rvd s. ?P'56 rv rva rvb rvc x2 rvd s \<and> ?P''56 rv rva rvb rvc x2 rvd s\<rbrace>, -
 10. \<And>rv rva rvb rvc. \<lbrace>?P''11 rv rva rvb rvc\<rbrace> 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 \<lbrace>\<lambda>rvd s. ((x45 = None \<longrightarrow> True) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (silc_inv aag st and (pas_refined aag and K (is_subject aag x41) and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) and (\<lambda>_. True)) s)) \<and> True\<rbrace>, -
A total of 19 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>a b rvg. x48 = Some (a, b) \<Longrightarrow> (x41 = rvg \<longrightarrow> reads_respects_f aag l (?Q64 a b () () () () (a, b) () () () rvg) reschedule_required) \<and> (x41 \<noteq> rvg \<longrightarrow> reads_respects_f aag l (?Q64 a b () () () () (a, b) () () () rvg) (return ()))
 2. \<And>rv rva rvb rvc x2 rvd rve rvf. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'58 rv rva rvb rvc x2 rvd rve rvf) (liftE (gets cur_thread))
 3. \<And>rv rva rvb rvc x2 rvd rve rvf. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''58 rv rva rvb rvc x2 rvd rve rvf\<rbrace> liftE (gets cur_thread) \<lbrace>?Q64 (fst x2) (snd x2) rv rva rvb rvc x2 rvd rve rvf\<rbrace>, -
 4. \<And>rv rva rvb rvc x2 rvd rve. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'57 rv rva rvb rvc x2 rvd rve) (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)))))
 5. \<And>rv rva rvb rvc x2 rvd rve. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''57 rv rva rvb rvc x2 rvd rve\<rbrace> 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)))) \<lbrace>\<lambda>rvf s. ?P'58 rv rva rvb rvc x2 rvd rve rvf s \<and> ?P''58 rv rva rvb rvc x2 rvd rve rvf s\<rbrace>, -
 6. \<And>rv rva rvb rvc x2 rvd. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'56 rv rva rvb rvc x2 rvd) (liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) x41))
 7. \<And>rv rva rvb rvc x2 rvd. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''56 rv rva rvb rvc x2 rvd\<rbrace> liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) x41) \<lbrace>\<lambda>rve s. ?P'57 rv rva rvb rvc x2 rvd rve s \<and> ?P''57 rv rva rvb rvc x2 rvd rve s\<rbrace>, -
 8. \<And>rv rva rvb rvc x2. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'55 rv rva rvb rvc x2) (cap_delete (x41, tcb_cnode_index 4))
 9. \<And>rv rva rvb rvc x2. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''55 rv rva rvb rvc x2\<rbrace> cap_delete (x41, tcb_cnode_index 4) \<lbrace>\<lambda>rvd s. ?P'56 rv rva rvb rvc x2 rvd s \<and> ?P''56 rv rva rvb rvc x2 rvd s\<rbrace>, -
 10. \<And>rv rva rvb rvc. \<lbrace>?P''11 rv rva rvb rvc\<rbrace> 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 \<lbrace>\<lambda>rvd s. ((x45 = None \<longrightarrow> True) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (silc_inv aag st and (pas_refined aag and K (is_subject aag x41) and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) and (\<lambda>_. True)) s)) \<and> True\<rbrace>, -
A total of 19 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>a b rvg. x48 = Some (a, b) \<Longrightarrow> x41 = rvg \<longrightarrow> reads_respects_f aag l (?Q64 a b () () () () (a, b) () () () rvg) reschedule_required
 2. \<And>a b rvg. x48 = Some (a, b) \<Longrightarrow> x41 \<noteq> rvg \<longrightarrow> reads_respects_f aag l (?Q64 a b () () () () (a, b) () () () rvg) (return ())
 3. \<And>rv rva rvb rvc x2 rvd rve rvf. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'58 rv rva rvb rvc x2 rvd rve rvf) (liftE (gets cur_thread))
 4. \<And>rv rva rvb rvc x2 rvd rve rvf. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''58 rv rva rvb rvc x2 rvd rve rvf\<rbrace> liftE (gets cur_thread) \<lbrace>?Q64 (fst x2) (snd x2) rv rva rvb rvc x2 rvd rve rvf\<rbrace>, -
 5. \<And>rv rva rvb rvc x2 rvd rve. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'57 rv rva rvb rvc x2 rvd rve) (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)))))
 6. \<And>rv rva rvb rvc x2 rvd rve. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''57 rv rva rvb rvc x2 rvd rve\<rbrace> 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)))) \<lbrace>\<lambda>rvf s. ?P'58 rv rva rvb rvc x2 rvd rve rvf s \<and> ?P''58 rv rva rvb rvc x2 rvd rve rvf s\<rbrace>, -
 7. \<And>rv rva rvb rvc x2 rvd. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'56 rv rva rvb rvc x2 rvd) (liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) x41))
 8. \<And>rv rva rvb rvc x2 rvd. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''56 rv rva rvb rvc x2 rvd\<rbrace> liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) x41) \<lbrace>\<lambda>rve s. ?P'57 rv rva rvb rvc x2 rvd rve s \<and> ?P''57 rv rva rvb rvc x2 rvd rve s\<rbrace>, -
 9. \<And>rv rva rvb rvc x2. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'55 rv rva rvb rvc x2) (cap_delete (x41, tcb_cnode_index 4))
 10. \<And>rv rva rvb rvc x2. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''55 rv rva rvb rvc x2\<rbrace> cap_delete (x41, tcb_cnode_index 4) \<lbrace>\<lambda>rvd s. ?P'56 rv rva rvb rvc x2 rvd s \<and> ?P''56 rv rva rvb rvc x2 rvd s\<rbrace>, -
A total of 20 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva rvb rvc x2 rvd rve. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'57 rv rva rvb rvc x2 rvd rve) (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)))))
 2. \<And>rv rva rvb rvc x2 rvd rve. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''57 rv rva rvb rvc x2 rvd rve\<rbrace> 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)))) \<lbrace>\<lambda>rvf s. silc_inv aag (?st92 rv rva rvb rvc x2 rvd rve rvf) s \<and> (silc_inv aag (?st83 (fst x2) (snd x2) rv rva rvb rvc x2 rvd rve rvf (cur_thread s)) and pas_refined aag) s\<rbrace>, -
 3. \<And>rv rva rvb rvc x2 rvd. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'56 rv rva rvb rvc x2 rvd) (liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) x41))
 4. \<And>rv rva rvb rvc x2 rvd. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''56 rv rva rvb rvc x2 rvd\<rbrace> liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. fst x2)) x41) \<lbrace>\<lambda>rve s. ?P'57 rv rva rvb rvc x2 rvd rve s \<and> ?P''57 rv rva rvb rvc x2 rvd rve s\<rbrace>, -
 5. \<And>rv rva rvb rvc x2. x48 = Some x2 \<Longrightarrow> reads_respects_f aag l (?P'55 rv rva rvb rvc x2) (cap_delete (x41, tcb_cnode_index 4))
 6. \<And>rv rva rvb rvc x2. x48 = Some x2 \<Longrightarrow> \<lbrace>?P''55 rv rva rvb rvc x2\<rbrace> cap_delete (x41, tcb_cnode_index 4) \<lbrace>\<lambda>rvd s. ?P'56 rv rva rvb rvc x2 rvd s \<and> ?P''56 rv rva rvb rvc x2 rvd s\<rbrace>, -
 7. \<And>rv rva rvb rvc. \<lbrace>?P''11 rv rva rvb rvc\<rbrace> 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 \<lbrace>\<lambda>rvd s. ((x45 = None \<longrightarrow> True) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (silc_inv aag st and (pas_refined aag and K (is_subject aag x41) and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))) and (\<lambda>_. True)) s)) \<and> True\<rbrace>, -
 8. \<And>rv rva rvb. reads_respects_f aag l (?P'10 rv rva rvb) (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)
 9. \<And>rv rva rvb. \<lbrace>?P''10 rv rva rvb\<rbrace> 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 \<lbrace>\<lambda>rvc s. ((x48 = None \<longrightarrow> True) \<and> (\<forall>x. x48 = Some x \<longrightarrow> ?P'55 rv rva rvb rvc x s \<and> ?P''55 rv rva rvb rvc x s)) \<and> ?P''11 rv rva rvb rvc s\<rbrace>, -
 10. \<And>rv rva. reads_respects_f aag l (?P'9 rv rva) (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)
A total of 16 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb. reads_respects_f aag l (?P'10 rv rva rvb) (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)
 2. \<And>rv rva rvb. \<lbrace>?P''10 rv rva rvb\<rbrace> 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 \<lbrace>\<lambda>rvc s. ((x48 = None \<longrightarrow> True) \<and> (\<forall>x. x48 = Some x \<longrightarrow> (silc_inv aag st and only_timer_irq_inv (?irq336 rv rva rvb rvc x) (?st'336 rv rva rvb rvc x) and einvs and simple_sched_action and pas_refined aag and emptyable (x41, tcb_cnode_index 4) and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> (((silc_inv aag st and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and pas_refined aag and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> True) \<and> True) \<and> ((snd x = None \<longrightarrow> True) \<and> (\<forall>xa. snd x = Some xa \<longrightarrow> ((silc_inv aag st and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and pas_refined aag and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> K (is_subject aag (fst (snd xa)) \<and> is_subject aag (fst x42) \<and> is_subject aag (fst (x41, tcb_cnode_index 4))) s) \<and> K (is_subject aag (fst (snd xa)) \<and> is_subject aag (fst (x41, tcb_cnode_index 4))) s)) \<and> ((snd x = None \<longrightarrow> (silc_inv aag st and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and pas_refined aag and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s) \<and> (\<forall>xa. snd x = Some xa \<longrightarrow> (silc_inv aag st and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and pas_refined aag and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> K (is_subject aag (fst (snd xa)) \<and> is_subject aag (fst (x41, tcb_cnode_index 4))) s)) \<and> ((snd x = None \<longrightarrow> (silc_inv aag st and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and pas_refined aag and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s) \<and> (\<forall>xa. snd x = Some xa \<longrightarrow> (silc_inv aag st and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and pas_refined aag and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> K (is_subject aag (fst (snd xa)) \<and> is_subject aag (fst (x41, tcb_cnode_index 4))) s)) \<and> (snd x = None \<longrightarrow> (((pas_refined aag and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (\<forall>xa. snd x = Some xa \<longrightarrow> ((((((((pas_refined aag and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> K (\<not> is_master_reply_cap (fst xa) \<and> is_subject aag x41 \<and> is_subject aag (fst (snd xa)) \<and> pas_cap_cur_auth aag (fst xa)) s))) \<and> ((x45 = None \<longrightarrow> True) \<and> (\<forall>x. x45 = Some x \<longrightarrow> (((x48 = None \<longrightarrow> silc_inv aag st s) \<and> (\<forall>x. x48 = Some x \<longrightarrow> (silc_inv aag st and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and pas_refined aag and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> (snd x = None \<longrightarrow> (silc_inv aag st and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and pas_refined aag and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s) \<and> (\<forall>xa. snd x = Some xa \<longrightarrow> (silc_inv aag st and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and pas_refined aag and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> K (is_subject aag (fst (snd xa)) \<and> is_subject aag (fst (x41, tcb_cnode_index 4))) s))) \<and> ((((x48 = None \<longrightarrow> pas_refined aag s) \<and> (\<forall>x. x48 = Some x \<longrightarrow> (pas_refined aag and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> (snd x = None \<longrightarrow> (((pas_refined aag and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (\<forall>xa. snd x = Some xa \<longrightarrow> ((((((((pas_refined aag and einvs and simple_sched_action and emptyable (x41, tcb_cnode_index 4) and K (is_subject aag (fst (x41, tcb_cnode_index 4)))) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s \<and> (invs and emptyable (x41, tcb_cnode_index 4)) s) \<and> K (\<not> is_master_reply_cap (fst xa) \<and> is_subject aag x41 \<and> is_subject aag (fst (snd xa)) \<and> pas_cap_cur_auth aag (fst xa)) s))) \<and> K (is_subject aag x41) s) \<and> (x48 = None \<longrightarrow> pas_cur_domain aag s) \<and> (\<forall>x. x48 = Some x \<longrightarrow> pas_cur_domain aag s \<and> (snd x = None \<longrightarrow> pas_cur_domain aag s) \<and> (\<forall>xa. snd x = Some xa \<longrightarrow> pas_cur_domain aag s))) \<and> (x48 = None \<longrightarrow> is_subject aag (cur_thread s)) \<and> (\<forall>x. x48 = Some x \<longrightarrow> is_subject aag (cur_thread s) \<and> (snd x = None \<longrightarrow> is_subject aag (cur_thread s)) \<and> (\<forall>xa. snd x = Some xa \<longrightarrow> is_subject aag (cur_thread s)))) \<and> True)) \<and> True\<rbrace>, -
 3. \<And>rv rva. reads_respects_f aag l (?P'9 rv rva) (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)
 4. \<And>rv rva. \<lbrace>?P''9 rv rva\<rbrace> 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 \<lbrace>\<lambda>rvb s. ?P'10 rv rva rvb s \<and> ?P''10 rv rva rvb s\<rbrace>, -
 5. \<And>rv. reads_respects_f aag l (?P'8 rv) (liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> set_mcpriority x41 (fst x2)))
 6. \<And>rv. \<lbrace>?P''8 rv\<rbrace> liftE (case x44 of None \<Rightarrow> return () | Some x2 \<Rightarrow> set_mcpriority x41 (fst x2)) \<lbrace>\<lambda>rva s. ?P'9 rv rva s \<and> ?P''9 rv rva s\<rbrace>, -
 7. reads_respects_f aag l ?P'7 (liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43))
 8. \<lbrace>?P''7\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>\<lambda>rv s. ?P'8 rv s \<and> ?P''8 rv s\<rbrace>, -
 9. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain 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 is_subject aag \<circ> cur_thread and (\<lambda>y. authorised_tcb_inv aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48) \<and> authorised_tcb_inv_extra aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48))) s \<Longrightarrow> ?P'7 s \<and> ?P''7 s proof (prove)
goal (3 subgoals):
 1. reads_respects_f aag l ?P'7 (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43)
 2. \<lbrace>?P''7\<rbrace> liftE (option_update_thread x41 (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) x43) \<lbrace>\<lambda>rv s. ((x44 = None \<longrightarrow> True) \<and> (\<forall>x. x44 = Some x \<longrightarrow> (silc_inv aag st and (\<lambda>_. True) and (\<lambda>_. True)) s)) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> (x44 = None \<longrightarrow> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> emptyable (x41, tcb_cnode_index 0) s \<and> is_subject aag x41 \<and> is_subject aag xa \<and> is_subject aag (fst x42)) \<and> (\<forall>x. x44 = Some x \<longrightarrow> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> (invs and tcb_at x41) s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> is_subject aag x41 \<and> is_subject aag xa \<and> is_subject aag (fst x42))) \<and> (\<forall>x xa. (\<exists>xb. x47 = Some (x, xa, xb)) \<longrightarrow> (x44 = None \<longrightarrow> invs s \<and> pas_refined aag s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> valid_list s \<and> is_subject aag xa \<and> is_subject aag x41 \<and> is_subject aag (fst x42) \<and> emptyable (x41, tcb_cnode_index (Suc 0)) s \<and> valid_sched s \<and> only_timer_irq_inv irq st' s \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a)) \<and> (\<forall>x. x44 = Some x \<longrightarrow> (invs and tcb_at x41) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> valid_list s \<and> is_subject aag xa \<and> is_subject aag x41 \<and> is_subject aag (fst x42) \<and> valid_sched s \<and> only_timer_irq_inv irq st' s \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x))) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> (x44 = None \<longrightarrow> invs s \<and> pas_refined aag s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> valid_list s \<and> is_subject aag x41 \<and> emptyable (x41, tcb_cnode_index 4) s \<and> valid_sched s \<and> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag aa) \<and> ((\<exists>a aa b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag (fst x42)) \<and> (\<forall>a. (\<exists>aa b. xa = Some (a, aa, b)) \<longrightarrow> \<not> is_master_reply_cap a \<and> pas_cap_cur_auth aag a) \<and> (\<forall>a aa b. x47 = Some (a, aa, b) \<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> 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> (tcb_at x41 s \<longrightarrow> is_valid_vtable_root a \<or> NullCap = a)) \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x))) \<and> (\<forall>x. x44 = Some x \<longrightarrow> (invs and tcb_at x41) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> valid_list s \<and> is_subject aag x41 \<and> valid_sched s \<and> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb) \<and> ((\<exists>a aa b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag (fst x42)) \<and> (\<forall>x. (\<exists>a b. xa = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<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> 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> (is_valid_vtable_root x \<or> NullCap = x)) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x)))) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag x41 \<and> (x44 = None \<longrightarrow> pas_refined aag s \<and> silc_inv aag st s \<and> is_subject aag (cur_thread s) \<and> pas_cur_domain aag s \<and> (\<forall>a. (\<exists>aa b. x47 = Some (a, aa, b)) \<longrightarrow> \<not> is_master_reply_cap a \<and> pas_cap_cur_auth aag a) \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (x41, tcb_cnode_index 0) s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s))) \<and> (\<forall>x. x44 = Some x \<longrightarrow> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> silc_inv aag st s \<and> is_subject aag (cur_thread s) \<and> pas_cur_domain aag s \<and> (\<forall>x. (\<exists>a b. x47 = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> (invs and tcb_at x41) s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s))))\<rbrace>, -
 3. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain 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 is_subject aag \<circ> cur_thread and (\<lambda>y. authorised_tcb_inv aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48) \<and> authorised_tcb_inv_extra aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48))) s \<Longrightarrow> ?P'7 s \<and> ?P''7 s proof (prove)
goal (2 subgoals):
 1. \<And>x2. x43 = Some x2 \<Longrightarrow> \<lbrace>?R3713 x2\<rbrace> thread_set (tcb_fault_handler_update (\<lambda>y. x2)) x41 \<lbrace>\<lambda>rv s. (\<forall>x xa. (\<exists>xb. x46 = Some (x, xa, xb)) \<longrightarrow> (x44 = None \<longrightarrow> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> emptyable (x41, tcb_cnode_index 0) s \<and> is_subject aag x41 \<and> is_subject aag xa \<and> is_subject aag (fst x42)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> tcb_at x41 s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x41 \<and> is_subject aag xa \<and> is_subject aag (fst x42))) \<and> (\<forall>x xa. (\<exists>xb. x47 = Some (x, xa, xb)) \<longrightarrow> (x44 = None \<longrightarrow> invs s \<and> pas_refined aag s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> valid_list s \<and> is_subject aag xa \<and> is_subject aag x41 \<and> is_subject aag (fst x42) \<and> emptyable (x41, tcb_cnode_index (Suc 0)) s \<and> valid_sched s \<and> only_timer_irq_inv irq st' s \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at x41 s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> valid_list s \<and> is_subject aag xa \<and> is_subject aag x41 \<and> is_subject aag (fst x42) \<and> valid_sched s \<and> only_timer_irq_inv irq st' s \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x))) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> (x44 = None \<longrightarrow> invs s \<and> pas_refined aag s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> valid_list s \<and> is_subject aag x41 \<and> emptyable (x41, tcb_cnode_index 4) s \<and> valid_sched s \<and> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag aa) \<and> ((\<exists>a aa b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag (fst x42)) \<and> (\<forall>a. (\<exists>aa b. xa = Some (a, aa, b)) \<longrightarrow> \<not> is_master_reply_cap a \<and> pas_cap_cur_auth aag a) \<and> (\<forall>a aa b. x47 = Some (a, aa, b) \<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> 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> (tcb_at x41 s \<longrightarrow> is_valid_vtable_root a \<or> NullCap = a)) \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at x41 s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> valid_list s \<and> is_subject aag x41 \<and> valid_sched s \<and> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb) \<and> ((\<exists>a aa b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag (fst x42)) \<and> (\<forall>x. (\<exists>a b. xa = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<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> 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> (is_valid_vtable_root x \<or> NullCap = x)) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x)))) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag x41 \<and> (x44 = None \<longrightarrow> pas_refined aag s \<and> silc_inv aag st s \<and> is_subject aag (cur_thread s) \<and> pas_cur_domain aag s \<and> (\<forall>a. (\<exists>aa b. x47 = Some (a, aa, b)) \<longrightarrow> \<not> is_master_reply_cap a \<and> pas_cap_cur_auth aag a) \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (x41, tcb_cnode_index 0) s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> silc_inv aag st s \<and> is_subject aag (cur_thread s) \<and> pas_cur_domain aag s \<and> (\<forall>x. (\<exists>a b. x47 = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> invs s \<and> tcb_at x41 s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s))))\<rbrace>
 2. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain 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 is_subject aag \<circ> cur_thread and (\<lambda>y. authorised_tcb_inv aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48) \<and> authorised_tcb_inv_extra aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48))) s \<Longrightarrow> ((x43 = None \<longrightarrow> True) \<and> (\<forall>x. x43 = Some x \<longrightarrow> (silc_inv aag st and (\<lambda>_. True) and (\<lambda>_. True)) s)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> (x43 = None \<longrightarrow> silc_inv aag st s) \<and> (\<forall>x. x43 = Some x \<longrightarrow> silc_inv aag st s)) \<and> (x43 = None \<longrightarrow> (\<forall>x xa. (\<exists>xb. x46 = Some (x, xa, xb)) \<longrightarrow> (x44 = None \<longrightarrow> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> emptyable (x41, tcb_cnode_index 0) s \<and> is_subject aag x41 \<and> is_subject aag xa \<and> is_subject aag (fst x42)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> tcb_at x41 s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x41 \<and> is_subject aag xa \<and> is_subject aag (fst x42))) \<and> (\<forall>x xa. (\<exists>xb. x47 = Some (x, xa, xb)) \<longrightarrow> (x44 = None \<longrightarrow> invs s \<and> pas_refined aag s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> valid_list s \<and> is_subject aag xa \<and> is_subject aag x41 \<and> is_subject aag (fst x42) \<and> emptyable (x41, tcb_cnode_index (Suc 0)) s \<and> valid_sched s \<and> only_timer_irq_inv irq st' s \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at x41 s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> valid_list s \<and> is_subject aag xa \<and> is_subject aag x41 \<and> is_subject aag (fst x42) \<and> valid_sched s \<and> only_timer_irq_inv irq st' s \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x))) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> (x44 = None \<longrightarrow> invs s \<and> pas_refined aag s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> valid_list s \<and> is_subject aag x41 \<and> emptyable (x41, tcb_cnode_index 4) s \<and> valid_sched s \<and> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag aa) \<and> ((\<exists>a aa b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag (fst x42)) \<and> (\<forall>a. (\<exists>aa b. xa = Some (a, aa, b)) \<longrightarrow> \<not> is_master_reply_cap a \<and> pas_cap_cur_auth aag a) \<and> (\<forall>a aa b. x47 = Some (a, aa, b) \<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> 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> (tcb_at x41 s \<longrightarrow> is_valid_vtable_root a \<or> NullCap = a)) \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> invs s \<and> tcb_at x41 s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> simple_sched_action s \<and> silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> valid_list s \<and> is_subject aag x41 \<and> valid_sched s \<and> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb) \<and> ((\<exists>a aa b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag (fst x42)) \<and> (\<forall>x. (\<exists>a b. xa = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<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> 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> (is_valid_vtable_root x \<or> NullCap = x)) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x)))) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag x41 \<and> (x44 = None \<longrightarrow> pas_refined aag s \<and> silc_inv aag st s \<and> is_subject aag (cur_thread s) \<and> pas_cur_domain aag s \<and> (\<forall>a. (\<exists>aa b. x47 = Some (a, aa, b)) \<longrightarrow> \<not> is_master_reply_cap a \<and> pas_cap_cur_auth aag a) \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> emptyable (x41, tcb_cnode_index 0) s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> silc_inv aag st s \<and> is_subject aag (cur_thread s) \<and> pas_cur_domain aag s \<and> (\<forall>x. (\<exists>a b. x47 = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> invs s \<and> tcb_at x41 s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s))))) \<and> (\<forall>x. x43 = Some x \<longrightarrow> ?R3713 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> tcb_at x41 s \<and> (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s \<and> (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)) 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> 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)) s \<and> (case x47 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> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (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 x48 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (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)) 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) \<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 x43 of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits) \<and> (case x45 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) \<and> (case x44 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s) \<and> ex_nonz_cap_to x41 s \<and> is_subject aag (cur_thread s) \<and> authorised_tcb_inv aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48) \<and> authorised_tcb_inv_extra aag (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48) \<Longrightarrow> (x43 = None \<longrightarrow> (\<forall>x xa. (\<exists>xb. x46 = Some (x, xa, xb)) \<longrightarrow> (x44 = None \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_subject aag x41 \<and> is_subject aag xa \<and> is_subject aag (fst x42)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x41 \<and> is_subject aag xa \<and> is_subject aag (fst x42))) \<and> (\<forall>x xa. (\<exists>xb. x47 = Some (x, xa, xb)) \<longrightarrow> (x44 = None \<longrightarrow> is_subject aag xa \<and> is_subject aag x41 \<and> is_subject aag (fst x42) \<and> emptyable (x41, tcb_cnode_index (Suc 0)) s \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xa \<and> is_subject aag x41 \<and> is_subject aag (fst x42) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x))) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> (x44 = None \<longrightarrow> is_subject aag x41 \<and> emptyable (x41, tcb_cnode_index 4) s \<and> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag aa) \<and> ((\<exists>a aa b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag (fst x42)) \<and> (\<forall>a. (\<exists>aa b. xa = Some (a, aa, b)) \<longrightarrow> \<not> is_master_reply_cap a \<and> pas_cap_cur_auth aag a) \<and> (\<forall>a aa b. x47 = Some (a, aa, b) \<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> 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> (is_valid_vtable_root a \<or> NullCap = a)) \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x41 \<and> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb) \<and> ((\<exists>a aa b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag (fst x42)) \<and> (\<forall>x. (\<exists>a b. xa = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<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> 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> (is_valid_vtable_root x \<or> NullCap = x)) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x)))) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag x41 \<and> (x44 = None \<longrightarrow> (\<forall>a. (\<exists>aa b. x47 = Some (a, aa, b)) \<longrightarrow> \<not> is_master_reply_cap a \<and> pas_cap_cur_auth aag a) \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<forall>x. (\<exists>a b. x47 = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s))))) \<and> (\<forall>x. x43 = Some x \<longrightarrow> (\<forall>xa xb. (\<exists>x. x46 = Some (xa, xb, x)) \<longrightarrow> (x44 = None \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> emptyable (x41, tcb_cnode_index 0) s \<and> is_subject aag x41 \<and> is_subject aag xb \<and> is_subject aag (fst x42)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x41 \<and> is_subject aag xb \<and> is_subject aag (fst x42))) \<and> (\<forall>xa xb. (\<exists>x. x47 = Some (xa, xb, x)) \<longrightarrow> (x44 = None \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xb \<and> is_subject aag x41 \<and> is_subject aag (fst x42) \<and> emptyable (x41, tcb_cnode_index (Suc 0)) s \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xb \<and> is_subject aag x41 \<and> is_subject aag (fst x42) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x))) \<and> (\<forall>xa xb. x48 = Some (xa, xb) \<longrightarrow> (x44 = None \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x41 \<and> emptyable (x41, tcb_cnode_index 4) s \<and> (\<forall>x xa. (\<exists>b. xb = Some (x, xa, b)) \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a aa b. xb = Some (a, aa, b)) \<longrightarrow> is_subject aag (fst x42)) \<and> (\<forall>x. (\<exists>a b. xb = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<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> 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> (is_valid_vtable_root x \<or> NullCap = x)) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> emptyable (x41, tcb_cnode_index 0) s \<and> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x41 \<and> (\<forall>x xa. (\<exists>b. xb = Some (x, xa, b)) \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a aa b. xb = Some (a, aa, b)) \<longrightarrow> is_subject aag (fst x42)) \<and> (\<forall>x. (\<exists>a b. xb = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<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> 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> (is_valid_vtable_root x \<or> NullCap = x)) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x)))) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> is_subject aag x41 \<and> (x44 = None \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<forall>x. (\<exists>a b. x47 = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>xa xb xc. x46 = Some (xa, xb, xc) \<longrightarrow> length x = word_bits \<and> emptyable (x41, tcb_cnode_index 0) s \<and> \<not> is_master_reply_cap xa \<and> is_subject aag xb \<and> pas_cap_cur_auth aag xa \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch xa \<and> s \<turnstile> xa \<and> (is_pt_cap xa \<longrightarrow> (\<exists>y. cap_asid xa = Some y)) \<and> (is_pd_cap xa \<longrightarrow> (\<exists>y. cap_asid xa = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xb, xc) s \<and> no_cap_to_obj_dr_emp xa s))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<forall>x. (\<exists>a b. x47 = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>xa xb xc. x46 = Some (xa, xb, xc) \<longrightarrow> length x = word_bits \<and> \<not> is_master_reply_cap xa \<and> is_subject aag xb \<and> pas_cap_cur_auth aag xa \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch xa \<and> s \<turnstile> xa \<and> (is_pt_cap xa \<longrightarrow> (\<exists>y. cap_asid xa = Some y)) \<and> (is_pd_cap xa \<longrightarrow> (\<exists>y. cap_asid xa = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xb, xc) s \<and> no_cap_to_obj_dr_emp xa s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; pas_cur_domain aag s; tcb_at x41 s; (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; case x46 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2); (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 x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s; case x47 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; (case x47 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> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (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 x48 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; 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); (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) x42 s \<and> ex_cte_cap_wp_to (\<lambda>_. True) x42 s; (\<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; (\<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; case x43 of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = word_bits; case x45 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s; case x44 of None \<Rightarrow> True | Some x2 \<Rightarrow> mcpriority_tcb_at ((\<le>) (fst x2)) (snd x2) s; ex_nonz_cap_to x41 s; is_subject aag (cur_thread 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); is_subject aag (fst x42)\<rbrakk> \<Longrightarrow> (x43 = None \<longrightarrow> (\<forall>x xa. (\<exists>xb. x46 = Some (x, xa, xb)) \<longrightarrow> (x44 = None \<longrightarrow> is_subject aag xa) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xa)) \<and> (\<forall>x xa. (\<exists>xb. x47 = Some (x, xa, xb)) \<longrightarrow> (x44 = None \<longrightarrow> is_subject aag xa \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xa \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x))) \<and> (\<forall>x xa. x48 = Some (x, xa) \<longrightarrow> (x44 = None \<longrightarrow> (\<forall>a aa. (\<exists>b. xa = Some (a, aa, b)) \<longrightarrow> is_subject aag aa) \<and> (\<forall>a. (\<exists>aa b. xa = Some (a, aa, b)) \<longrightarrow> \<not> is_master_reply_cap a \<and> pas_cap_cur_auth aag a) \<and> (\<forall>a aa b. x47 = Some (a, aa, b) \<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> 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> (is_valid_vtable_root a \<or> NullCap = a)) \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s \<and> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<forall>x xb. (\<exists>b. xa = Some (x, xb, b)) \<longrightarrow> is_subject aag xb) \<and> (\<forall>x. (\<exists>a b. xa = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<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> 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> (is_valid_vtable_root x \<or> NullCap = x)) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x)))) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (x44 = None \<longrightarrow> (\<forall>a. (\<exists>aa b. x47 = Some (a, aa, b)) \<longrightarrow> \<not> is_master_reply_cap a \<and> pas_cap_cur_auth aag a) \<and> (\<forall>a aa b. x46 = Some (a, aa, b) \<longrightarrow> \<not> is_master_reply_cap a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag a \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch a \<and> s \<turnstile> a \<and> (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> cte_wp_at (\<lambda>_. True) (aa, b) s \<and> no_cap_to_obj_dr_emp a s))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<forall>x. (\<exists>a b. x47 = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s))))) \<and> (\<forall>x. x43 = Some x \<longrightarrow> (\<forall>xa xb. (\<exists>x. x46 = Some (xa, xb, x)) \<longrightarrow> (x44 = None \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xb) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xb)) \<and> (\<forall>xa xb. (\<exists>x. x47 = Some (xa, xb, x)) \<longrightarrow> (x44 = None \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xb \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x)) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag xb \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x))) \<and> (\<forall>xa xb. x48 = Some (xa, xb) \<longrightarrow> (x44 = None \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<forall>x xa. (\<exists>b. xb = Some (x, xa, b)) \<longrightarrow> is_subject aag xa) \<and> (\<forall>x. (\<exists>a b. xb = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<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> 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> (is_valid_vtable_root x \<or> NullCap = x)) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> length x = word_bits \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<forall>x xa. (\<exists>b. xb = Some (x, xa, b)) \<longrightarrow> is_subject aag xa) \<and> (\<forall>x. (\<exists>a b. xb = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x xa xb. x47 = Some (x, xa, xb) \<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> 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> (is_valid_vtable_root x \<or> NullCap = x)) \<and> (\<forall>x xa xb. x46 = Some (x, xa, xb) \<longrightarrow> is_cnode_or_valid_arch x \<and> s \<turnstile> x \<and> (is_pt_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> (is_pd_cap x \<longrightarrow> (\<exists>y. cap_asid x = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xa, xb) s \<and> no_cap_to_obj_dr_emp x s \<and> \<not> is_master_reply_cap x \<and> is_subject aag xa \<and> pas_cap_cur_auth aag x \<and> (\<forall>x. (\<exists>xa xb. x47 = Some (x, xa, xb)) \<longrightarrow> is_valid_vtable_root x \<or> NullCap = x)))) \<and> ((\<exists>a b. x45 = Some (a, b)) \<longrightarrow> (x44 = None \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<forall>x. (\<exists>a b. x47 = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>xa xb xc. x46 = Some (xa, xb, xc) \<longrightarrow> length x = word_bits \<and> \<not> is_master_reply_cap xa \<and> is_subject aag xb \<and> pas_cap_cur_auth aag xa \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch xa \<and> s \<turnstile> xa \<and> (is_pt_cap xa \<longrightarrow> (\<exists>y. cap_asid xa = Some y)) \<and> (is_pd_cap xa \<longrightarrow> (\<exists>y. cap_asid xa = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xb, xc) s \<and> no_cap_to_obj_dr_emp xa s))) \<and> ((\<exists>a b. x44 = Some (a, b)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (\<forall>x. (\<exists>a b. x47 = Some (x, a, b)) \<longrightarrow> \<not> is_master_reply_cap x \<and> pas_cap_cur_auth aag x) \<and> (\<forall>xa xb xc. x46 = Some (xa, xb, xc) \<longrightarrow> length x = word_bits \<and> \<not> is_master_reply_cap xa \<and> is_subject aag xb \<and> pas_cap_cur_auth aag xa \<and> ((\<exists>x xa b. x47 = Some (x, xa, b)) \<longrightarrow> is_cnode_or_valid_arch xa \<and> s \<turnstile> xa \<and> (is_pt_cap xa \<longrightarrow> (\<exists>y. cap_asid xa = Some y)) \<and> (is_pd_cap xa \<longrightarrow> (\<exists>y. cap_asid xa = Some y)) \<and> cte_wp_at (\<lambda>_. True) (xb, xc) s \<and> no_cap_to_obj_dr_emp xa s)))))