theory Syscall_IF

lemma handle_invocation_reads_respects_g:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  notes gts_st_tcb[wp del] gts_st_tcb_at[wp del]
  notes get_message_info_reads_respects_g = reads_respects_g_from_inv[OF get_message_info_rev get_mi_inv]
  shows "reads_respects_f_g aag l
           (silc_inv aag st and only_timer_irq_inv irq st' and einvs and schact_is_rct and ct_active
                            and pas_refined aag and pas_cur_domain aag
                            and is_subject aag \<circ> cur_thread and K (\<not> pasMaySendIrqs aag))
           (handle_invocation calling blocking)" apply (rule gen_asm_ev) apply (simp add: handle_invocation_def split_def) apply (wpc | simp add: tcb_at_st_tcb_at[symmetric] split del: if_split
             | intro impI | erule conjE | rule doesnt_touch_globalsI
             | (wp syscall_requiv_f_g gts_inv when_ev
                   reads_respects_f_g'[OF lookup_extra_caps_reads_respects_g, where Q="\<top>" and st=st]
                   reads_respects_f_g'[OF lookup_ipc_buffer_reads_respects_g, where Q="\<top>" and st=st]
                   reads_respects_f_g'[OF cap_fault_on_failure_rev_g, where Q="\<top>" and st=st]
                   valid_validE_R[OF wp_post_taut] lookup_ipc_buffer_has_read_auth'
                   lookup_cap_and_slot_reads_respects_g' decode_invocation_reads_respects_f_g
                   get_mrs_reads_respects_g handle_fault_reads_respects_g
                   reads_respects_f_g'[OF set_thread_state_reads_respects_g, where st=st and Q="\<top>"]
                   reads_respects_f_g'[OF get_thread_state_reads_respects_g, where st=st and Q="\<top>"]
                   reads_respects_f_g'[OF reads_respects_g[OF reply_from_kernel_reads_respects], where st=st]
                   get_thread_state_reads_respects_g perform_invocation_reads_respects_f_g
                   set_thread_state_pas_refined sts_first_restart set_thread_state_ct_st
                   lookup_extra_caps_authorised lookup_extra_caps_auth handle_fault_globals_equiv
                   set_thread_state_globals_equiv reply_from_kernel_globals_equiv)+
             | rule hoare_drop_imps)+ apply (rule_tac Q'="\<lambda>r s. silc_inv aag st s \<and> invs s \<and> is_subject aag rv \<and>
                                         is_subject aag (cur_thread s) \<and> rv \<noteq> idle_thread s"
                            in hoare_post_imp_R) apply (wp pinv_invs perform_invocation_silc_inv) apply (simp add: invs_def valid_state_def valid_pspace_def) apply (wpsimp wp: reads_respects_f_g'
                                set_thread_state_reads_respects_g[OF domains_distinct]) apply (wp when_ev set_thread_state_only_timer_irq_inv[where st=st']
                       set_thread_state_reads_respects_g set_thread_state_globals_equiv
                       sts_Restart_invs set_thread_state_pas_refined set_thread_state_ct_st
                       set_thread_state_runnable_valid_sched sts_authorised_for_globals_inv
                       sts_schact_is_rct_runnable decode_invocation_reads_respects_f_g
                       reads_respects_f_g'[OF get_mrs_reads_respects_g, where Q="\<top>" and st=st]
                       reads_respects_f_g'[OF handle_fault_reads_respects_g]
                       decode_invocation_authorised decode_invocation_authorised_globals_inv
                       decode_invocation_authorised_extra lec_valid_fault
                       lookup_extra_caps_authorised lookup_extra_caps_auth
                       lookup_ipc_buffer_has_read_auth' lookup_cap_and_slot_valid_fault3
                       lookup_cap_and_slot_authorised lookup_cap_and_slot_cur_auth as_user_silc_inv
                       reads_respects_f_g'[OF reads_respects_g[OF as_user_reads_respects], where Q=\<top> and st=st]
                       reads_respects_f_g'[OF get_message_info_reads_respects_g, where Q="\<top>" and st=st]
                       as_user_globals_equiv user_getreg_inv get_mi_inv get_mi_length get_mi_length'
                    | simp add: o_def
                    | rule doesnt_touch_globalsI
                    | clarify, assumption
                    | wp (once) hoare_drop_imps)+ apply (rule conjI) apply (clarsimp simp: requiv_g_cur_thread_eq simp: reads_equiv_f_g_conj) apply (clarsimp simp: det_getRegister invs_sym_refs invs_def valid_state_def
                        valid_pspace_vo valid_pspace_distinct) apply (rule context_conjI) apply (simp add: ct_active_cur_thread_not_idle_thread) apply (clarsimp simp: valid_pspace_def ct_in_state_def) apply (rule conjI) apply (fastforce intro: reads_lrefl) apply (rule conjI, fastforce)+ apply (simp add: conj_comms) apply (rule conjI) apply (clarsimp elim!: schact_is_rct_simple) apply (rule conjI) apply (rule st_tcb_ex_cap) apply simp+ apply (case_tac "sta",clarsimp+) apply (force simp: only_timer_irq_inv_def runnable_eq_active) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and schact_is_rct and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (\<not> pasMaySendIrqs aag)) (handle_invocation calling blocking) proof (prove)
goal (1 subgoal):
 1. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and schact_is_rct and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) (handle_invocation calling blocking) proof (prove)
goal (1 subgoal):
 1. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and schact_is_rct and ct_active and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) (doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE p <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when blocking (handle_fault thread fault)) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
decode_invocation (mi_label info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when calling (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- perform_invocation blocking calling oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when calling (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE) proof (prove)
goal (14 subgoals):
 1. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''122 rv rva rvb v ()\<rbrace> perform_invocation blocking calling v \<lbrace>\<lambda>rvd s. silc_inv aag st s \<and> aag_can_read aag rv \<and> (calling \<longrightarrow> silc_inv aag st s \<and> is_subject aag rv \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> rv \<noteq> idle_thread s) \<and> (if calling then \<lambda>a. silc_inv aag st a \<and> is_subject aag (cur_thread a) \<and> valid_arch_state a else (\<lambda>s. silc_inv aag st s \<and> (is_subject aag \<circ> cur_thread and valid_arch_state) s)) s\<rbrace>, -
 2. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'121 rv rva rvb v) (liftE (set_thread_state rv Restart))
 3. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''121 rv rva rvb v\<rbrace> liftE (set_thread_state rv Restart) \<lbrace>\<lambda>rvc s. (silc_inv aag (?st307 rv rva rvb v rvc) and only_timer_irq_inv (?irq307 rv rva rvb v rvc) (?st'307 rv rva rvb v rvc) and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation v and ct_active and authorised_invocation aag v and is_subject aag \<circ> cur_thread and authorised_for_globals_inv v and K (authorised_invocation_extra aag v)) s \<and> ?P''122 rv rva rvb v rvc s\<rbrace>, -
 4. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?Q''5 rv rva rvb v) (doE args <- liftE (get_mrs rv (snd (snd (snd v))) rva);
decode_invocation (mi_label rva) args rvb (fst v) (fst (snd v)) (fst (snd (snd v)))
odE)
 5. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?Q'5 rv rva rvb v) (when blocking (handle_fault rv v))
 6. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?Q'''5 rv rva rvb v\<rbrace> doE args <- liftE (get_mrs rv (snd (snd (snd v))) rva);
decode_invocation (mi_label rva) args rvb (fst v) (fst (snd v)) (fst (snd (snd v)))
odE \<lbrace>\<lambda>v s. ?P'121 rv rva rvb v s \<and> ?P''121 rv rva rvb v s\<rbrace>, \<lbrace>\<lambda>v s. calling \<longrightarrow> (silc_inv aag st and (K (is_subject aag rv) and (\<lambda>s. valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> rv \<noteq> idle_thread s)) and ?Q104 rv rva rvb v) s\<rbrace>
 7. \<And>rv rva rvb. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>\<lambda>s. (silc_inv aag st and (pas_refined aag and K (is_subject aag rv) and ?P70 rv rva rvb) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> aag_can_read_or_affect aag l rv \<and> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag rv \<and> buffer_cptr_index + unat (mi_extra_caps rva) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace> doE p <- cap_fault_on_failure (of_bl rvb) False (lookup_cap_and_slot rv rvb);
buffer <- liftE (lookup_ipc_buffer False rv);
extracaps <- lookup_extra_caps rv buffer rva;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rvc. ?Q''5 rv rva rvb rvc and ?Q'''5 rv rva rvb rvc\<rbrace>, \<lbrace>?Q'5 rv rva rvb\<rbrace>
 8. \<And>rv rva. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'4 rv rva) (liftE (liftM to_bl (as_user rv (getRegister cap_register))))
 9. \<And>rv rva. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> liftE (liftM to_bl (as_user rv (getRegister cap_register))) \<lbrace>\<lambda>rvb s. (silc_inv aag st and (pas_refined aag and K (is_subject aag rv) and ?P70 rv rva rvb) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> aag_can_read_or_affect aag l rv \<and> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag rv \<and> buffer_cptr_index + unat (mi_extra_caps rva) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace>, -
 10. \<And>rv. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'3 rv) (liftE (get_message_info rv))
A total of 14 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''122 rv rva rvb v ()\<rbrace> perform_invocation blocking calling v \<lbrace>\<lambda>r s. silc_inv aag st s \<and> invs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> rv \<noteq> idle_thread s\<rbrace>, -
 2. \<And>rv rva rvb v rvc s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s \<and> invs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> rv \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> silc_inv aag st s \<and> aag_can_read aag rv \<and> (calling \<longrightarrow> silc_inv aag st s \<and> is_subject aag rv \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> rv \<noteq> idle_thread s) \<and> (if calling then \<lambda>a. silc_inv aag st a \<and> is_subject aag (cur_thread a) \<and> valid_arch_state a else (\<lambda>s. silc_inv aag st s \<and> (is_subject aag \<circ> cur_thread and valid_arch_state) s)) s
 3. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'121 rv rva rvb v) (liftE (set_thread_state rv Restart))
 4. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''121 rv rva rvb v\<rbrace> liftE (set_thread_state rv Restart) \<lbrace>\<lambda>rvc s. (silc_inv aag (?st307 rv rva rvb v rvc) and only_timer_irq_inv (?irq307 rv rva rvb v rvc) (?st'307 rv rva rvb v rvc) and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation v and ct_active and authorised_invocation aag v and is_subject aag \<circ> cur_thread and authorised_for_globals_inv v and K (authorised_invocation_extra aag v)) s \<and> ?P''122 rv rva rvb v rvc s\<rbrace>, -
 5. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?Q''5 rv rva rvb v) (doE args <- liftE (get_mrs rv (snd (snd (snd v))) rva);
decode_invocation (mi_label rva) args rvb (fst v) (fst (snd v)) (fst (snd (snd v)))
odE)
 6. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?Q'5 rv rva rvb v) (when blocking (handle_fault rv v))
 7. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?Q'''5 rv rva rvb v\<rbrace> doE args <- liftE (get_mrs rv (snd (snd (snd v))) rva);
decode_invocation (mi_label rva) args rvb (fst v) (fst (snd v)) (fst (snd (snd v)))
odE \<lbrace>\<lambda>v s. ?P'121 rv rva rvb v s \<and> ?P''121 rv rva rvb v s\<rbrace>, \<lbrace>\<lambda>v s. calling \<longrightarrow> (silc_inv aag st and (K (is_subject aag rv) and (\<lambda>s. valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> rv \<noteq> idle_thread s)) and ?Q104 rv rva rvb v) s\<rbrace>
 8. \<And>rv rva rvb. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>\<lambda>s. (silc_inv aag st and (pas_refined aag and K (is_subject aag rv) and ?P70 rv rva rvb) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> aag_can_read_or_affect aag l rv \<and> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag rv \<and> buffer_cptr_index + unat (mi_extra_caps rva) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace> doE p <- cap_fault_on_failure (of_bl rvb) False (lookup_cap_and_slot rv rvb);
buffer <- liftE (lookup_ipc_buffer False rv);
extracaps <- lookup_extra_caps rv buffer rva;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rvc. ?Q''5 rv rva rvb rvc and ?Q'''5 rv rva rvb rvc\<rbrace>, \<lbrace>?Q'5 rv rva rvb\<rbrace>
 9. \<And>rv rva. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'4 rv rva) (liftE (liftM to_bl (as_user rv (getRegister cap_register))))
 10. \<And>rv rva. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> liftE (liftM to_bl (as_user rv (getRegister cap_register))) \<lbrace>\<lambda>rvb s. (silc_inv aag st and (pas_refined aag and K (is_subject aag rv) and ?P70 rv rva rvb) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> aag_can_read_or_affect aag l rv \<and> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag rv \<and> buffer_cptr_index + unat (mi_extra_caps rva) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace>, -
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv rva rvb v rvc s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s \<and> invs s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> rv \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> silc_inv aag st s \<and> aag_can_read aag rv \<and> (calling \<longrightarrow> silc_inv aag st s \<and> is_subject aag rv \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> rv \<noteq> idle_thread s) \<and> (if calling then \<lambda>a. silc_inv aag st a \<and> is_subject aag (cur_thread a) \<and> valid_arch_state a else (\<lambda>s. silc_inv aag st s \<and> (is_subject aag \<circ> cur_thread and valid_arch_state) s)) s
 2. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'121 rv rva rvb v) (liftE (set_thread_state rv Restart))
 3. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''121 rv rva rvb v\<rbrace> liftE (set_thread_state rv Restart) \<lbrace>\<lambda>rvc s. (silc_inv aag (?st307 rv rva rvb v rvc) and only_timer_irq_inv (?irq307 rv rva rvb v rvc) (?st'307 rv rva rvb v rvc) and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation v and ct_active and authorised_invocation aag v and is_subject aag \<circ> cur_thread and authorised_for_globals_inv v and K (authorised_invocation_extra aag v)) s \<and> (silc_inv aag st and valid_invocation v and authorised_invocation aag v and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread) s \<and> (invs and ct_active and valid_invocation v) s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> rv \<noteq> idle_thread s\<rbrace>, -
 4. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?Q''5 rv rva rvb v) (doE args <- liftE (get_mrs rv (snd (snd (snd v))) rva);
decode_invocation (mi_label rva) args rvb (fst v) (fst (snd v)) (fst (snd (snd v)))
odE)
 5. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?Q'5 rv rva rvb v) (when blocking (handle_fault rv v))
 6. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?Q'''5 rv rva rvb v\<rbrace> doE args <- liftE (get_mrs rv (snd (snd (snd v))) rva);
decode_invocation (mi_label rva) args rvb (fst v) (fst (snd v)) (fst (snd (snd v)))
odE \<lbrace>\<lambda>v s. ?P'121 rv rva rvb v s \<and> ?P''121 rv rva rvb v s\<rbrace>, \<lbrace>\<lambda>v s. calling \<longrightarrow> (silc_inv aag st and (K (is_subject aag rv) and (\<lambda>s. valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> rv \<noteq> idle_thread s)) and ?Q104 rv rva rvb v) s\<rbrace>
 7. \<And>rv rva rvb. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>\<lambda>s. (silc_inv aag st and (pas_refined aag and K (is_subject aag rv) and ?P70 rv rva rvb) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> aag_can_read_or_affect aag l rv \<and> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag rv \<and> buffer_cptr_index + unat (mi_extra_caps rva) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace> doE p <- cap_fault_on_failure (of_bl rvb) False (lookup_cap_and_slot rv rvb);
buffer <- liftE (lookup_ipc_buffer False rv);
extracaps <- lookup_extra_caps rv buffer rva;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rvc. ?Q''5 rv rva rvb rvc and ?Q'''5 rv rva rvb rvc\<rbrace>, \<lbrace>?Q'5 rv rva rvb\<rbrace>
 8. \<And>rv rva. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'4 rv rva) (liftE (liftM to_bl (as_user rv (getRegister cap_register))))
 9. \<And>rv rva. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> liftE (liftM to_bl (as_user rv (getRegister cap_register))) \<lbrace>\<lambda>rvb s. (silc_inv aag st and (pas_refined aag and K (is_subject aag rv) and ?P70 rv rva rvb) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> aag_can_read_or_affect aag l rv \<and> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag rv \<and> buffer_cptr_index + unat (mi_extra_caps rva) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace>, -
 10. \<And>rv. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'3 rv) (liftE (get_message_info rv))
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'121 rv rva rvb v) (liftE (set_thread_state rv Restart))
 2. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''121 rv rva rvb v\<rbrace> liftE (set_thread_state rv Restart) \<lbrace>\<lambda>rvc s. (silc_inv aag (?st307 rv rva rvb v rvc) and only_timer_irq_inv (?irq307 rv rva rvb v rvc) (?st'307 rv rva rvb v rvc) and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation v and ct_active and authorised_invocation aag v and is_subject aag \<circ> cur_thread and authorised_for_globals_inv v and K (authorised_invocation_extra aag v)) s \<and> (silc_inv aag st and valid_invocation v and authorised_invocation aag v and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread) s \<and> (invs and ct_active and valid_invocation v) s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> rv \<noteq> idle_thread s\<rbrace>, -
 3. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?Q''5 rv rva rvb v) (doE args <- liftE (get_mrs rv (snd (snd (snd v))) rva);
decode_invocation (mi_label rva) args rvb (fst v) (fst (snd v)) (fst (snd (snd v)))
odE)
 4. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?Q'5 rv rva rvb v) (when blocking (handle_fault rv v))
 5. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?Q'''5 rv rva rvb v\<rbrace> doE args <- liftE (get_mrs rv (snd (snd (snd v))) rva);
decode_invocation (mi_label rva) args rvb (fst v) (fst (snd v)) (fst (snd (snd v)))
odE \<lbrace>\<lambda>v s. ?P'121 rv rva rvb v s \<and> ?P''121 rv rva rvb v s\<rbrace>, \<lbrace>\<lambda>v s. calling \<longrightarrow> (silc_inv aag st and (K (is_subject aag rv) and (\<lambda>s. valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> rv \<noteq> idle_thread s)) and ?Q104 rv rva rvb v) s\<rbrace>
 6. \<And>rv rva rvb. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>\<lambda>s. (silc_inv aag st and (pas_refined aag and K (is_subject aag rv) and ?P70 rv rva rvb) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> aag_can_read_or_affect aag l rv \<and> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag rv \<and> buffer_cptr_index + unat (mi_extra_caps rva) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace> doE p <- cap_fault_on_failure (of_bl rvb) False (lookup_cap_and_slot rv rvb);
buffer <- liftE (lookup_ipc_buffer False rv);
extracaps <- lookup_extra_caps rv buffer rva;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rvc. ?Q''5 rv rva rvb rvc and ?Q'''5 rv rva rvb rvc\<rbrace>, \<lbrace>?Q'5 rv rva rvb\<rbrace>
 7. \<And>rv rva. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'4 rv rva) (liftE (liftM to_bl (as_user rv (getRegister cap_register))))
 8. \<And>rv rva. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> liftE (liftM to_bl (as_user rv (getRegister cap_register))) \<lbrace>\<lambda>rvb s. (silc_inv aag st and (pas_refined aag and K (is_subject aag rv) and ?P70 rv rva rvb) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> aag_can_read_or_affect aag l rv \<and> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag rv \<and> buffer_cptr_index + unat (mi_extra_caps rva) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace>, -
 9. \<And>rv. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'3 rv) (liftE (get_message_info rv))
 10. \<And>rv. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> liftE (get_message_info rv) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>, -
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''121 rv rva rvb v\<rbrace> liftE (set_thread_state rv Restart) \<lbrace>\<lambda>rvc s. (silc_inv aag (?st307 rv rva rvb v rvc) and only_timer_irq_inv (?irq307 rv rva rvb v rvc) (?st'307 rv rva rvb v rvc) and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation v and ct_active and authorised_invocation aag v and is_subject aag \<circ> cur_thread and authorised_for_globals_inv v and K (authorised_invocation_extra aag v)) s \<and> (silc_inv aag st and valid_invocation v and authorised_invocation aag v and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread) s \<and> (invs and ct_active and valid_invocation v) s \<and> is_subject aag rv \<and> is_subject aag (cur_thread s) \<and> rv \<noteq> idle_thread s\<rbrace>, -
 2. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?Q''5 rv rva rvb v) (doE args <- liftE (get_mrs rv (snd (snd (snd v))) rva);
decode_invocation (mi_label rva) args rvb (fst v) (fst (snd v)) (fst (snd (snd v)))
odE)
 3. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?Q'5 rv rva rvb v) (when blocking (handle_fault rv v))
 4. \<And>rv rva rvb v. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?Q'''5 rv rva rvb v\<rbrace> doE args <- liftE (get_mrs rv (snd (snd (snd v))) rva);
decode_invocation (mi_label rva) args rvb (fst v) (fst (snd v)) (fst (snd (snd v)))
odE \<lbrace>\<lambda>v s. (silc_inv aag (?st344 rv rva rvb v) and (is_subject aag \<circ> cur_thread and valid_arch_state) and ?Q340 rv rva rvb v) s \<and> ?P''121 rv rva rvb v s\<rbrace>, \<lbrace>\<lambda>v s. calling \<longrightarrow> (silc_inv aag st and (K (is_subject aag rv) and (\<lambda>s. valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> rv \<noteq> idle_thread s)) and ?Q104 rv rva rvb v) s\<rbrace>
 5. \<And>rv rva rvb. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>\<lambda>s. (silc_inv aag st and (pas_refined aag and K (is_subject aag rv) and ?P70 rv rva rvb) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> aag_can_read_or_affect aag l rv \<and> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag rv \<and> buffer_cptr_index + unat (mi_extra_caps rva) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace> doE p <- cap_fault_on_failure (of_bl rvb) False (lookup_cap_and_slot rv rvb);
buffer <- liftE (lookup_ipc_buffer False rv);
extracaps <- lookup_extra_caps rv buffer rva;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>\<lambda>rvc. ?Q''5 rv rva rvb rvc and ?Q'''5 rv rva rvb rvc\<rbrace>, \<lbrace>?Q'5 rv rva rvb\<rbrace>
 6. \<And>rv rva. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'4 rv rva) (liftE (liftM to_bl (as_user rv (getRegister cap_register))))
 7. \<And>rv rva. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''4 rv rva\<rbrace> liftE (liftM to_bl (as_user rv (getRegister cap_register))) \<lbrace>\<lambda>rvb s. (silc_inv aag st and (pas_refined aag and K (is_subject aag rv) and ?P70 rv rva rvb) and (\<lambda>_. True)) s \<and> silc_inv aag st s \<and> aag_can_read_or_affect aag l rv \<and> silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag rv \<and> buffer_cptr_index + unat (mi_extra_caps rva) < 2 ^ (msg_align_bits - word_size_bits)\<rbrace>, -
 8. \<And>rv. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l (?P'3 rv) (liftE (get_message_info rv))
 9. \<And>rv. \<not> pasMaySendIrqs aag \<Longrightarrow> \<lbrace>?P''3 rv\<rbrace> liftE (get_message_info rv) \<lbrace>\<lambda>rva s. ?P'4 rv rva s \<and> ?P''4 rv rva s\<rbrace>, -
 10. \<not> pasMaySendIrqs aag \<Longrightarrow> reads_respects_f_g aag l ?P'2 (liftE (gets cur_thread))
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; 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> schact_is_rct s \<and> ct_active s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_f_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> det (getRegister cap_register) \<and> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> (blocking \<longrightarrow> silc_inv aag (?st2093 (cur_thread s)) s \<and> valid_objs s \<and> silc_inv aag (?st2093 (cur_thread s)) s) \<and> valid_objs s \<and> silc_inv aag (?st2108 (cur_thread s)) s \<and> valid_objs s \<and> (calling \<longrightarrow> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> cur_thread s \<noteq> idle_thread s) \<and> silc_inv aag (?st2145 (cur_thread s)) s \<and> valid_arch_state s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> valid_objs s \<and> domain_sep_inv (pasMaySendIrqs ?aag2204) (?st'2168 (cur_thread s)) s \<and> valid_objs s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> silc_inv aag (?st2209 (cur_thread s)) s \<and> only_timer_irq_inv (?irq2215 (cur_thread s)) st' s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_objs s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> valid_objs s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> valid_objs s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> simple_sched_action s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> cur_thread s \<noteq> idle_thread s \<and> valid_objs s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; 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> schact_is_rct s \<and> ct_active s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> \<forall>s t. reads_equiv_f_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t
 2. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; 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> schact_is_rct s \<and> ct_active s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> det (getRegister cap_register) \<and> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> (blocking \<longrightarrow> silc_inv aag (?st2093 (cur_thread s)) s \<and> valid_objs s \<and> silc_inv aag (?st2093 (cur_thread s)) s) \<and> valid_objs s \<and> silc_inv aag (?st2108 (cur_thread s)) s \<and> valid_objs s \<and> (calling \<longrightarrow> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> cur_thread s \<noteq> idle_thread s) \<and> silc_inv aag (?st2145 (cur_thread s)) s \<and> valid_arch_state s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> valid_objs s \<and> domain_sep_inv (pasMaySendIrqs ?aag2204) (?st'2168 (cur_thread s)) s \<and> valid_objs s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> silc_inv aag (?st2209 (cur_thread s)) s \<and> only_timer_irq_inv (?irq2215 (cur_thread s)) st' s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_objs s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> valid_objs s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> valid_objs s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> simple_sched_action s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> cur_thread s \<noteq> idle_thread s \<and> valid_objs s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; 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> schact_is_rct s \<and> ct_active s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> det (getRegister cap_register) \<and> valid_arch_state s \<and> cur_thread s \<noteq> idle_thread s \<and> (blocking \<longrightarrow> silc_inv aag (?st2093 (cur_thread s)) s \<and> valid_objs s \<and> silc_inv aag (?st2093 (cur_thread s)) s) \<and> valid_objs s \<and> silc_inv aag (?st2108 (cur_thread s)) s \<and> valid_objs s \<and> (calling \<longrightarrow> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> cur_thread s \<noteq> idle_thread s) \<and> silc_inv aag (?st2145 (cur_thread s)) s \<and> valid_arch_state s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> valid_objs s \<and> domain_sep_inv (pasMaySendIrqs ?aag2204) (?st'2168 (cur_thread s)) s \<and> valid_objs s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> silc_inv aag (?st2209 (cur_thread s)) s \<and> only_timer_irq_inv (?irq2215 (cur_thread s)) st' s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> valid_objs s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> valid_objs s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> valid_objs s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> simple_sched_action s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> cur_thread s \<noteq> idle_thread s \<and> valid_objs s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; ct_active s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s \<and> (blocking \<longrightarrow> silc_inv aag (?st2093 (cur_thread s)) s) \<and> silc_inv aag (?st2108 (cur_thread s)) s \<and> (calling \<longrightarrow> pspace_aligned s \<and> cur_thread s \<noteq> idle_thread s) \<and> silc_inv aag (?st2145 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> domain_sep_inv (pasMaySendIrqs ?aag2204) (?st'2168 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> silc_inv aag (?st2209 (cur_thread s)) s \<and> only_timer_irq_inv (?irq2215 (cur_thread s)) st' s \<and> pspace_aligned s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> simple_sched_action s \<and> pspace_aligned s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> cur_thread s \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; ct_active s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s
 2. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; ct_active s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (blocking \<longrightarrow> silc_inv aag (?st2093 (cur_thread s)) s) \<and> silc_inv aag (?st2108 (cur_thread s)) s \<and> (calling \<longrightarrow> pspace_aligned s \<and> cur_thread s \<noteq> idle_thread s) \<and> silc_inv aag (?st2145 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> domain_sep_inv (pasMaySendIrqs ?aag2204) (?st'2168 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> silc_inv aag (?st2209 (cur_thread s)) s \<and> only_timer_irq_inv (?irq2215 (cur_thread s)) st' s \<and> pspace_aligned s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> simple_sched_action s \<and> pspace_aligned s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> cur_thread s \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; ct_active s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (blocking \<longrightarrow> silc_inv aag (?st2093 (cur_thread s)) s) \<and> silc_inv aag (?st2108 (cur_thread s)) s \<and> (calling \<longrightarrow> pspace_aligned s \<and> cur_thread s \<noteq> idle_thread s) \<and> silc_inv aag (?st2145 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> domain_sep_inv (pasMaySendIrqs ?aag2204) (?st'2168 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> silc_inv aag (?st2209 (cur_thread s)) s \<and> only_timer_irq_inv (?irq2215 (cur_thread s)) st' s \<and> pspace_aligned s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> simple_sched_action s \<and> pspace_aligned s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> cur_thread s \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> (blocking \<longrightarrow> silc_inv aag (?st2093 (cur_thread s)) s) \<and> silc_inv aag (?st2108 (cur_thread s)) s \<and> silc_inv aag (?st2145 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> domain_sep_inv (pasMaySendIrqs ?aag2204) (?st'2168 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> silc_inv aag (?st2209 (cur_thread s)) s \<and> only_timer_irq_inv (?irq2215 (cur_thread s)) st' s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> simple_sched_action s \<and> ex_nonz_cap_to (cur_thread s) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> blocking \<longrightarrow> silc_inv aag (?st2093 (cur_thread s)) s
 2. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> silc_inv aag (?st2108 (cur_thread s)) s \<and> silc_inv aag (?st2145 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> domain_sep_inv (pasMaySendIrqs ?aag2204) (?st'2168 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> silc_inv aag (?st2209 (cur_thread s)) s \<and> only_timer_irq_inv (?irq2215 (cur_thread s)) st' s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> simple_sched_action s \<and> ex_nonz_cap_to (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> silc_inv aag (?st2108 (cur_thread s)) s \<and> silc_inv aag (?st2145 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> domain_sep_inv (pasMaySendIrqs ?aag2204) (?st'2168 (cur_thread s)) s \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> pas_refined ?aag2204 s \<and> is_subject ?aag2204 (cur_thread s) \<and> silc_inv aag (?st2209 (cur_thread s)) s \<and> only_timer_irq_inv (?irq2215 (cur_thread s)) st' s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> simple_sched_action s \<and> ex_nonz_cap_to (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at runnable (cur_thread s) s \<and> simple_sched_action s \<and> ex_nonz_cap_to (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> simple_sched_action s \<and> ex_nonz_cap_to (cur_thread s) s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> st_tcb_at runnable (cur_thread s) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> simple_sched_action s
 2. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> ex_nonz_cap_to (cur_thread s) s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> st_tcb_at runnable (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> ex_nonz_cap_to (cur_thread s) s \<and> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> st_tcb_at runnable (cur_thread s) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> ex_nonz_cap_to (cur_thread s) s
 2. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> st_tcb_at runnable (cur_thread s) s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> st_tcb_at (?P2585 s) (cur_thread s) s
 2. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap s
 3. \<And>s sta. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); ?P2585 s sta\<rbrakk> \<Longrightarrow> \<not> halted sta
 4. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> st_tcb_at runnable (cur_thread s) s proof (prove)
goal (2 subgoals):
 1. \<And>s sta. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); active sta\<rbrakk> \<Longrightarrow> \<not> halted sta
 2. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> st_tcb_at runnable (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> pasMaySendIrqs aag; silc_inv aag st s; only_timer_irq_inv irq st' s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_sched s; schact_is_rct s; st_tcb_at active (cur_thread s) s; pas_refined aag s; pas_cur_domain aag s; is_subject aag (cur_thread s); cur_thread s \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> domain_sep_inv False (?st'2266 (cur_thread s)) s \<and> domain_sep_inv False (?st'2331 (cur_thread s)) s \<and> st_tcb_at runnable (cur_thread s) s proof (prove)
goal:
No subgoals!