theory Syscall_IF

lemma perform_invocation_reads_respects_f_g:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_f_g aag l
           (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag
                            and einvs and schact_is_rct and valid_invocation oper and ct_active
                            and authorised_invocation aag oper and is_subject aag \<circ> cur_thread
                            and authorised_for_globals_inv oper
                            and K (authorised_invocation_extra aag oper))
           (perform_invocation blocking calling oper)" proof (cases oper) case InvokeUntyped then show ?thesis apply simp apply (rule equiv_valid_guard_imp) apply (wpc | simp | wp reads_respects_f_g'[OF invoke_untyped_reads_respects_g]
                            invoke_untyped_silc_inv)+ by (simp add: authorised_invocation_def) next case InvokeEndpoint then show ?thesis apply simp apply (rule equiv_valid_guard_imp) apply (wpc | simp | wp reads_respects_f_g'[OF send_ipc_reads_respects_g] send_ipc_silc_inv)+ by (fastforce intro: read_reply_thread_read_thread_rev[OF reads_lrefl]
                   simp: authorised_invocation_def reads_equiv_f_g_def) next case InvokeNotification then show ?thesis apply simp apply (rule equiv_valid_guard_imp) apply (wpc | simp | wp reads_respects_f_g'[OF send_signal_reads_respects_g, where Q="\<top>"])+ by (fastforce simp: authorised_invocation_def valid_sched_def) next case InvokeReply then show ?thesis apply simp apply (rule equiv_valid_guard_imp) apply (wpc | simp | wp do_reply_transfer_reads_respects_f_g)+ by (fastforce intro: read_reply_thread_read_thread_rev[OF reads_lrefl] emptyable_cte_wp_atD
                   simp: reads_equiv_f_g_def authorised_invocation_def is_cap_simps
                   dest: emptyable_cte_wp_atD) next case InvokeTCB then show ?thesis apply simp apply (rule equiv_valid_guard_imp) apply (wpc | simp | wp invoke_tcb_reads_respects_f_g)+ by (fastforce simp: authorised_invocation_def authorised_invocation_extra_def) next case InvokeDomain then show ?thesis apply simp apply (rule equiv_valid_guard_imp) apply (wpc | simp | wp invoke_domain_reads_respects_f_g)+ by (simp add: authorised_invocation_def) next case InvokeCNode then show ?thesis apply simp apply (rule equiv_valid_guard_imp) apply (wpc | simp | wp invoke_cnode_reads_respects_f_g)+ by (fastforce simp: authorised_invocation_def) next case InvokeIRQControl then show ?thesis apply simp apply (rule equiv_valid_guard_imp) apply (wpc | simp | wp reads_respects_f_g'[OF invoke_irq_control_reads_respects_g]
                            invoke_irq_control_silc_inv)+ by (simp add: invs_def valid_state_def authorised_invocation_def) next case InvokeIRQHandler then show ?thesis apply simp apply (rule equiv_valid_guard_imp) apply (wpc | simp | wp invoke_irq_handler_reads_respects_f_g)+ by (fastforce simp: authorised_invocation_def) next case InvokeArchObject then show ?thesis apply simp apply (rule equiv_valid_guard_imp) apply (wpc | simp | wp reads_respects_f_g'[OF arch_perform_invocation_reads_respects_g]
                            arch_perform_invocation_silc_inv)+ by (fastforce simp: authorised_invocation_def authorised_for_globals_inv_def) qed

(* 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 pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
goal (10 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x21 x22 x23 x24. oper = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 8. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 9. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 10. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
this:
oper = InvokeUntyped x1_

goal (10 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x21 x22 x23 x24. oper = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 8. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 9. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 10. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (chain)
picking this:
oper = InvokeUntyped x1_ proof (prove)
using this:
oper = InvokeUntyped x1_

goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (prove)
goal (1 subgoal):
 1. oper = InvokeUntyped x1_ \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_untyped_inv x1_ and ct_active and authorised_invocation aag (InvokeUntyped x1_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeUntyped x1_) and (\<lambda>y. authorised_invocation_extra aag (InvokeUntyped x1_))) (doE y <- invoke_untyped x1_;
returnOk []
odE) proof (prove)
goal (2 subgoals):
 1. oper = InvokeUntyped x1_ \<Longrightarrow> reads_respects_f_g aag l ?Q1 (doE y <- invoke_untyped x1_;
returnOk []
odE)
 2. \<And>s. \<lbrakk>oper = InvokeUntyped x1_; (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_untyped_inv x1_ and ct_active and authorised_invocation aag (InvokeUntyped x1_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeUntyped x1_) and (\<lambda>y. authorised_invocation_extra aag (InvokeUntyped x1_))) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oper = InvokeUntyped x1_; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> schact_is_rct s \<and> valid_untyped_inv x1_ s \<and> ct_active s \<and> authorised_invocation aag (InvokeUntyped x1_) s \<and> is_subject aag (cur_thread s) \<and> authorised_for_globals_inv (InvokeUntyped x1_) s \<and> authorised_invocation_extra aag (InvokeUntyped x1_)\<rbrakk> \<Longrightarrow> silc_inv aag ?st7 s \<and> only_timer_irq_inv ?irq8 ?st8 s \<and> authorised_untyped_inv aag x1_ \<and> ?P''5 s proof (state)
this:
reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)

goal (9 subgoals):
 1. \<And>x21 x22 x23 x24. oper = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 8. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 9. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
goal (9 subgoals):
 1. \<And>x21 x22 x23 x24. oper = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 8. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 9. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
this:
oper = InvokeEndpoint x21_ x22_ x23_ x24_

goal (9 subgoals):
 1. \<And>x21 x22 x23 x24. oper = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 8. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 9. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (chain)
picking this:
oper = InvokeEndpoint x21_ x22_ x23_ x24_ proof (prove)
using this:
oper = InvokeEndpoint x21_ x22_ x23_ x24_

goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (prove)
goal (1 subgoal):
 1. oper = InvokeEndpoint x21_ x22_ x23_ x24_ \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and (ep_at x21_ and ex_nonz_cap_to x21_) and ct_active and authorised_invocation aag (InvokeEndpoint x21_ x22_ x23_ x24_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeEndpoint x21_ x22_ x23_ x24_) and (\<lambda>y. authorised_invocation_extra aag (InvokeEndpoint x21_ x22_ x23_ x24_))) (liftE (do thread <- gets cur_thread;
y <- send_ipc blocking calling x22_ x23_ x24_ thread x21_;
return []
od)) proof (prove)
goal (2 subgoals):
 1. oper = InvokeEndpoint x21_ x22_ x23_ x24_ \<Longrightarrow> reads_respects_f_g aag l ?Q1 (liftE (do thread <- gets cur_thread;
y <- send_ipc blocking calling x22_ x23_ x24_ thread x21_;
return []
od))
 2. \<And>s. \<lbrakk>oper = InvokeEndpoint x21_ x22_ x23_ x24_; (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and (ep_at x21_ and ex_nonz_cap_to x21_) and ct_active and authorised_invocation aag (InvokeEndpoint x21_ x22_ x23_ x24_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeEndpoint x21_ x22_ x23_ x24_) and (\<lambda>y. authorised_invocation_extra aag (InvokeEndpoint x21_ x22_ x23_ x24_))) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oper = InvokeEndpoint x21_ x22_ x23_ x24_; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> schact_is_rct s \<and> ep_at x21_ s \<and> ex_nonz_cap_to x21_ s \<and> ct_active s \<and> authorised_invocation aag (InvokeEndpoint x21_ x22_ x23_ x24_) s \<and> is_subject aag (cur_thread s) \<and> authorised_for_globals_inv (InvokeEndpoint x21_ x22_ x23_ x24_) s \<and> authorised_invocation_extra aag (InvokeEndpoint x21_ x22_ x23_ x24_)\<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> silc_inv aag (?st9 (cur_thread s)) s \<and> (x23_ \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag x21_) \<in> pasPolicy aag) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x21_) \<in> pasPolicy aag \<and> (x24_ \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag x21_) \<in> pasPolicy aag) \<and> (x23_ \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag x21_) \<in> pasPolicy aag) proof (state)
this:
reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)

goal (8 subgoals):
 1. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 8. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
goal (8 subgoals):
 1. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 8. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
this:
oper = InvokeNotification x31_ x32_

goal (8 subgoals):
 1. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 8. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (chain)
picking this:
oper = InvokeNotification x31_ x32_ proof (prove)
using this:
oper = InvokeNotification x31_ x32_

goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (prove)
goal (1 subgoal):
 1. oper = InvokeNotification x31_ x32_ \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and (ntfn_at x31_ and ex_nonz_cap_to x31_) and ct_active and authorised_invocation aag (InvokeNotification x31_ x32_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeNotification x31_ x32_) and (\<lambda>y. authorised_invocation_extra aag (InvokeNotification x31_ x32_))) (doE y <- liftE (send_signal x31_ x32_);
returnOk []
odE) proof (prove)
goal (2 subgoals):
 1. oper = InvokeNotification x31_ x32_ \<Longrightarrow> reads_respects_f_g aag l ?Q1 (doE y <- liftE (send_signal x31_ x32_);
returnOk []
odE)
 2. \<And>s. \<lbrakk>oper = InvokeNotification x31_ x32_; (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and (ntfn_at x31_ and ex_nonz_cap_to x31_) and ct_active and authorised_invocation aag (InvokeNotification x31_ x32_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeNotification x31_ x32_) and (\<lambda>y. authorised_invocation_extra aag (InvokeNotification x31_ x32_))) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oper = InvokeNotification x31_ x32_; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> schact_is_rct s \<and> ntfn_at x31_ s \<and> ex_nonz_cap_to x31_ s \<and> ct_active s \<and> authorised_invocation aag (InvokeNotification x31_ x32_) s \<and> is_subject aag (cur_thread s) \<and> authorised_for_globals_inv (InvokeNotification x31_ x32_) s \<and> authorised_invocation_extra aag (InvokeNotification x31_ x32_)\<rbrakk> \<Longrightarrow> silc_inv aag ?st8 s \<and> valid_etcbs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_global_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> valid_idle s \<and> sym_refs (state_refs_of s) \<and> (pasSubject aag, Notify, pasObjectAbs aag x31_) \<in> pasPolicy aag \<and> ?P''5 s proof (state)
this:
reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)

goal (7 subgoals):
 1. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
goal (7 subgoals):
 1. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
this:
oper = InvokeReply x41_ x42_ x43_

goal (7 subgoals):
 1. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 7. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (chain)
picking this:
oper = InvokeReply x41_ x42_ x43_ proof (prove)
using this:
oper = InvokeReply x41_ x42_ x43_

goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (prove)
goal (1 subgoal):
 1. oper = InvokeReply x41_ x42_ x43_ \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and (tcb_at x41_ and cte_wp_at (\<lambda>cap. \<exists>R. cap = ReplyCap x41_ False R) x42_) and ct_active and authorised_invocation aag (InvokeReply x41_ x42_ x43_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeReply x41_ x42_ x43_) and (\<lambda>y. authorised_invocation_extra aag (InvokeReply x41_ x42_ x43_))) (liftE (do sender <- gets cur_thread;
y <- do_reply_transfer sender x41_ x42_ x43_;
return []
od)) proof (prove)
goal (2 subgoals):
 1. oper = InvokeReply x41_ x42_ x43_ \<Longrightarrow> reads_respects_f_g aag l ?Q1 (liftE (do sender <- gets cur_thread;
y <- do_reply_transfer sender x41_ x42_ x43_;
return []
od))
 2. \<And>s. \<lbrakk>oper = InvokeReply x41_ x42_ x43_; (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and (tcb_at x41_ and cte_wp_at (\<lambda>cap. \<exists>R. cap = ReplyCap x41_ False R) x42_) and ct_active and authorised_invocation aag (InvokeReply x41_ x42_ x43_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeReply x41_ x42_ x43_) and (\<lambda>y. authorised_invocation_extra aag (InvokeReply x41_ x42_ x43_))) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oper = InvokeReply x41_ x42_ x43_; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> schact_is_rct s \<and> tcb_at x41_ s \<and> cte_wp_at (\<lambda>cap. \<exists>R. cap = ReplyCap x41_ False R) x42_ s \<and> ct_active s \<and> authorised_invocation aag (InvokeReply x41_ x42_ x43_) s \<and> is_subject aag (cur_thread s) \<and> authorised_for_globals_inv (InvokeReply x41_ x42_ x43_) s \<and> authorised_invocation_extra aag (InvokeReply x41_ x42_ x43_)\<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> silc_inv aag (?st9 (cur_thread s)) s \<and> tcb_at (cur_thread s) s \<and> emptyable x42_ s \<and> (x43_ \<longrightarrow> is_subject aag x41_) \<and> aag_can_read aag x41_ \<and> is_subject aag (fst x42_) proof (state)
this:
reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)

goal (6 subgoals):
 1. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
goal (6 subgoals):
 1. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
this:
oper = InvokeTCB x5_

goal (6 subgoals):
 1. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 6. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (chain)
picking this:
oper = InvokeTCB x5_ proof (prove)
using this:
oper = InvokeTCB x5_

goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (prove)
goal (1 subgoal):
 1. oper = InvokeTCB x5_ \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and tcb_inv_wf x5_ and ct_active and authorised_invocation aag (InvokeTCB x5_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeTCB x5_) and (\<lambda>y. authorised_invocation_extra aag (InvokeTCB x5_))) (invoke_tcb x5_) proof (prove)
goal (2 subgoals):
 1. oper = InvokeTCB x5_ \<Longrightarrow> reads_respects_f_g aag l ?Q1 (invoke_tcb x5_)
 2. \<And>s. \<lbrakk>oper = InvokeTCB x5_; (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and tcb_inv_wf x5_ and ct_active and authorised_invocation aag (InvokeTCB x5_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeTCB x5_) and (\<lambda>y. authorised_invocation_extra aag (InvokeTCB x5_))) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oper = InvokeTCB x5_; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> schact_is_rct s \<and> tcb_inv_wf x5_ s \<and> ct_active s \<and> authorised_invocation aag (InvokeTCB x5_) s \<and> is_subject aag (cur_thread s) \<and> authorised_for_globals_inv (InvokeTCB x5_) s \<and> authorised_invocation_extra aag (InvokeTCB x5_)\<rbrakk> \<Longrightarrow> silc_inv aag ?st5 s \<and> only_timer_irq_inv ?irq5 ?st'5 s \<and> simple_sched_action s \<and> authorised_tcb_inv aag x5_ \<and> authorised_tcb_inv_extra aag x5_ proof (state)
this:
reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)

goal (5 subgoals):
 1. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
goal (5 subgoals):
 1. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
this:
oper = InvokeDomain x61_ x62_

goal (5 subgoals):
 1. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 5. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (chain)
picking this:
oper = InvokeDomain x61_ x62_ proof (prove)
using this:
oper = InvokeDomain x61_ x62_

goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (prove)
goal (1 subgoal):
 1. oper = InvokeDomain x61_ x62_ \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and (tcb_at x61_ and (\<lambda>s. x61_ \<noteq> idle_thread s)) and ct_active and authorised_invocation aag (InvokeDomain x61_ x62_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeDomain x61_ x62_) and (\<lambda>y. authorised_invocation_extra aag (InvokeDomain x61_ x62_))) (invoke_domain x61_ x62_) proof (prove)
goal (2 subgoals):
 1. oper = InvokeDomain x61_ x62_ \<Longrightarrow> reads_respects_f_g aag l ?Q1 (invoke_domain x61_ x62_)
 2. \<And>s. \<lbrakk>oper = InvokeDomain x61_ x62_; (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and (tcb_at x61_ and (\<lambda>s. x61_ \<noteq> idle_thread s)) and ct_active and authorised_invocation aag (InvokeDomain x61_ x62_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeDomain x61_ x62_) and (\<lambda>y. authorised_invocation_extra aag (InvokeDomain x61_ x62_))) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oper = InvokeDomain x61_ x62_; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> schact_is_rct s \<and> tcb_at x61_ s \<and> x61_ \<noteq> idle_thread s \<and> ct_active s \<and> authorised_invocation aag (InvokeDomain x61_ x62_) s \<and> is_subject aag (cur_thread s) \<and> authorised_for_globals_inv (InvokeDomain x61_ x62_) s \<and> authorised_invocation_extra aag (InvokeDomain x61_ x62_)\<rbrakk> \<Longrightarrow> False proof (state)
this:
reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)

goal (4 subgoals):
 1. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
goal (4 subgoals):
 1. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
this:
oper = InvokeCNode x7_

goal (4 subgoals):
 1. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 4. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (chain)
picking this:
oper = InvokeCNode x7_ proof (prove)
using this:
oper = InvokeCNode x7_

goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (prove)
goal (1 subgoal):
 1. oper = InvokeCNode x7_ \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_cnode_inv x7_ and ct_active and authorised_invocation aag (InvokeCNode x7_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeCNode x7_) and (\<lambda>y. authorised_invocation_extra aag (InvokeCNode x7_))) (doE y <- invoke_cnode x7_;
returnOk []
odE) proof (prove)
goal (2 subgoals):
 1. oper = InvokeCNode x7_ \<Longrightarrow> reads_respects_f_g aag l ?Q1 (doE y <- invoke_cnode x7_;
returnOk []
odE)
 2. \<And>s. \<lbrakk>oper = InvokeCNode x7_; (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_cnode_inv x7_ and ct_active and authorised_invocation aag (InvokeCNode x7_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeCNode x7_) and (\<lambda>y. authorised_invocation_extra aag (InvokeCNode x7_))) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oper = InvokeCNode x7_; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> schact_is_rct s \<and> valid_cnode_inv x7_ s \<and> ct_active s \<and> authorised_invocation aag (InvokeCNode x7_) s \<and> is_subject aag (cur_thread s) \<and> authorised_for_globals_inv (InvokeCNode x7_) s \<and> authorised_invocation_extra aag (InvokeCNode x7_)\<rbrakk> \<Longrightarrow> silc_inv aag ?st7 s \<and> only_timer_irq_inv ?irq7 ?st'7 s \<and> simple_sched_action s \<and> cnode_inv_auth_derivations x7_ s \<and> authorised_cnode_inv aag x7_ s proof (state)
this:
reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)

goal (3 subgoals):
 1. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
goal (3 subgoals):
 1. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
this:
oper = InvokeIRQControl x8_

goal (3 subgoals):
 1. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 3. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (chain)
picking this:
oper = InvokeIRQControl x8_ proof (prove)
using this:
oper = InvokeIRQControl x8_

goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (prove)
goal (1 subgoal):
 1. oper = InvokeIRQControl x8_ \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and irq_control_inv_valid x8_ and ct_active and authorised_invocation aag (InvokeIRQControl x8_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeIRQControl x8_) and (\<lambda>y. authorised_invocation_extra aag (InvokeIRQControl x8_))) (doE y <- invoke_irq_control x8_;
returnOk []
odE) proof (prove)
goal (2 subgoals):
 1. oper = InvokeIRQControl x8_ \<Longrightarrow> reads_respects_f_g aag l ?Q1 (doE y <- invoke_irq_control x8_;
returnOk []
odE)
 2. \<And>s. \<lbrakk>oper = InvokeIRQControl x8_; (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and irq_control_inv_valid x8_ and ct_active and authorised_invocation aag (InvokeIRQControl x8_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeIRQControl x8_) and (\<lambda>y. authorised_invocation_extra aag (InvokeIRQControl x8_))) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oper = InvokeIRQControl x8_; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> schact_is_rct s \<and> irq_control_inv_valid x8_ s \<and> ct_active s \<and> authorised_invocation aag (InvokeIRQControl x8_) s \<and> is_subject aag (cur_thread s) \<and> authorised_for_globals_inv (InvokeIRQControl x8_) s \<and> authorised_invocation_extra aag (InvokeIRQControl x8_)\<rbrakk> \<Longrightarrow> silc_inv aag ?st7 s \<and> valid_global_objs s \<and> valid_arch_state s \<and> authorised_irq_ctl_inv aag x8_ \<and> ?P''5 s proof (state)
this:
reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)

goal (2 subgoals):
 1. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
goal (2 subgoals):
 1. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
this:
oper = InvokeIRQHandler x9_

goal (2 subgoals):
 1. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)
 2. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (chain)
picking this:
oper = InvokeIRQHandler x9_ proof (prove)
using this:
oper = InvokeIRQHandler x9_

goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (prove)
goal (1 subgoal):
 1. oper = InvokeIRQHandler x9_ \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and irq_handler_inv_valid x9_ and ct_active and authorised_invocation aag (InvokeIRQHandler x9_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeIRQHandler x9_) and (\<lambda>y. authorised_invocation_extra aag (InvokeIRQHandler x9_))) (doE y <- liftE (invoke_irq_handler x9_);
returnOk []
odE) proof (prove)
goal (2 subgoals):
 1. oper = InvokeIRQHandler x9_ \<Longrightarrow> reads_respects_f_g aag l ?Q1 (doE y <- liftE (invoke_irq_handler x9_);
returnOk []
odE)
 2. \<And>s. \<lbrakk>oper = InvokeIRQHandler x9_; (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and irq_handler_inv_valid x9_ and ct_active and authorised_invocation aag (InvokeIRQHandler x9_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeIRQHandler x9_) and (\<lambda>y. authorised_invocation_extra aag (InvokeIRQHandler x9_))) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oper = InvokeIRQHandler x9_; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> schact_is_rct s \<and> irq_handler_inv_valid x9_ s \<and> ct_active s \<and> authorised_invocation aag (InvokeIRQHandler x9_) s \<and> is_subject aag (cur_thread s) \<and> authorised_for_globals_inv (InvokeIRQHandler x9_) s \<and> authorised_invocation_extra aag (InvokeIRQHandler x9_)\<rbrakk> \<Longrightarrow> silc_inv aag ?st8 s \<and> authorised_irq_hdl_inv aag x9_ proof (state)
this:
reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)

goal (1 subgoal):
 1. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
goal (1 subgoal):
 1. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (state)
this:
oper = InvokeArchObject x10_

goal (1 subgoal):
 1. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (chain)
picking this:
oper = InvokeArchObject x10_ proof (prove)
using this:
oper = InvokeArchObject x10_

goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper) proof (prove)
goal (1 subgoal):
 1. oper = InvokeArchObject x10_ \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_arch_inv x10_ and ct_active and authorised_invocation aag (InvokeArchObject x10_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeArchObject x10_) and (\<lambda>y. authorised_invocation_extra aag (InvokeArchObject x10_))) (arch_perform_invocation x10_) proof (prove)
goal (2 subgoals):
 1. oper = InvokeArchObject x10_ \<Longrightarrow> reads_respects_f_g aag l ?Q1 (arch_perform_invocation x10_)
 2. \<And>s. \<lbrakk>oper = InvokeArchObject x10_; (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_arch_inv x10_ and ct_active and authorised_invocation aag (InvokeArchObject x10_) and is_subject aag \<circ> cur_thread and authorised_for_globals_inv (InvokeArchObject x10_) and (\<lambda>y. authorised_invocation_extra aag (InvokeArchObject x10_))) s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oper = InvokeArchObject x10_; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> schact_is_rct s \<and> valid_arch_inv x10_ s \<and> ct_active s \<and> authorised_invocation aag (InvokeArchObject x10_) s \<and> is_subject aag (cur_thread s) \<and> authorised_for_globals_inv (InvokeArchObject x10_) s \<and> authorised_invocation_extra aag (InvokeArchObject x10_)\<rbrakk> \<Longrightarrow> silc_inv aag ?st5 s \<and> authorised_arch_inv aag x10_ s \<and> authorised_for_globals_arch_inv x10_ s \<and> authorised_arch_inv aag x10_ s proof (state)
this:
reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and schact_is_rct and valid_invocation oper and ct_active and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and authorised_for_globals_inv oper and K (authorised_invocation_extra aag oper)) (perform_invocation blocking calling oper)

goal:
No subgoals!