theory Syscall_AC

lemma perform_invocation_respects:
  "\<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action
                    and valid_invocation oper and authorised_invocation aag oper
                    and is_subject aag \<circ> cur_thread
                    and (\<lambda>s. \<forall>p ko. kheap s p = Some ko
                                    \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st)  \<longrightarrow> kheap st p = Some ko)\<rbrace>
   perform_invocation blocking calling oper
   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" supply [wp] = invoke_untyped_integrity send_ipc_integrity_autarch send_signal_respects
                do_reply_transfer_respects invoke_tcb_respects invoke_cnode_respects
                invoke_arch_respects invoke_irq_control_respects invoke_irq_handler_respects supply [simp] = authorised_invocation_def proof (cases oper) case InvokeEndpoint show ?thesis unfolding InvokeEndpoint apply (rule hoare_pre) apply wpsimp apply (fastforce simp: obj_at_def is_tcb split: if_split_asm) done next case InvokeNotification show ?thesis unfolding InvokeNotification apply (rule hoare_pre) apply wpsimp apply fastforce done next case InvokeReply show ?thesis unfolding InvokeReply apply (rule hoare_pre) apply wpsimp apply clarsimp apply (fastforce simp: is_reply_cap_to_def cur_tcb_def dest!: invs_cur) done qed (simp, rule hoare_pre, wpsimp, fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (state)
goal (10 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>x21 x22 x23 x24. oper = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 3. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 4. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 5. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 6. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 7. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 8. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 9. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 10. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (state)
this:
oper = InvokeEndpoint x21_ x22_ x23_ x24_

goal (10 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>x21 x22 x23 x24. oper = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 3. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 4. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 5. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 6. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 7. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 8. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 9. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 10. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation (InvokeEndpoint x21_ x22_ x23_ x24_) and authorised_invocation aag (InvokeEndpoint x21_ x22_ x23_ x24_) and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling (InvokeEndpoint x21_ x22_ x23_ x24_) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> perform_invocation blocking calling (InvokeEndpoint x21_ x22_ x23_ x24_) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>s. (pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation (InvokeEndpoint x21_ x22_ x23_ x24_) and authorised_invocation aag (InvokeEndpoint x21_ x22_ x23_ x24_) and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation (InvokeEndpoint x21_ x22_ x23_ x24_) and authorised_invocation aag (InvokeEndpoint x21_ x22_ x23_ x24_) and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)) s \<Longrightarrow> (integrity aag X st and pas_refined aag and invs and is_subject aag \<circ> cur_thread and obj_at (\<lambda>ep. x23_ \<longrightarrow> (\<forall>r\<in>refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) x21_ and K (is_subject aag (cur_thread s) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x21_) \<in> pasPolicy aag \<and> (x24_ \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag x21_) \<in> pasPolicy aag))) s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>

goal (9 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 3. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 4. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 5. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 6. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 7. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 8. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 9. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (state)
goal (9 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 3. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 4. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 5. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 6. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 7. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 8. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 9. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (state)
this:
oper = InvokeNotification x31_ x32_

goal (9 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>x31 x32. oper = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 3. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 4. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 5. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 6. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 7. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 8. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 9. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation (InvokeNotification x31_ x32_) and authorised_invocation aag (InvokeNotification x31_ x32_) and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling (InvokeNotification x31_ x32_) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> perform_invocation blocking calling (InvokeNotification x31_ x32_) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>s. (pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation (InvokeNotification x31_ x32_) and authorised_invocation aag (InvokeNotification x31_ x32_) and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation (InvokeNotification x31_ x32_) and authorised_invocation aag (InvokeNotification x31_ x32_) and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)) s \<Longrightarrow> (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and K ((pasSubject aag, Notify, pasObjectAbs aag x31_) \<in> pasPolicy aag)) s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>

goal (8 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 3. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 4. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 5. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 6. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 7. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 8. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (state)
goal (8 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 3. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 4. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 5. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 6. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 7. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 8. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (state)
this:
oper = InvokeReply x41_ x42_ x43_

goal (8 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>x41 x42 x43. oper = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 3. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 4. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 5. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 6. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 7. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 8. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation (InvokeReply x41_ x42_ x43_) and authorised_invocation aag (InvokeReply x41_ x42_ x43_) and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling (InvokeReply x41_ x42_ x43_) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> perform_invocation blocking calling (InvokeReply x41_ x42_ x43_) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>s. (pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation (InvokeReply x41_ x42_ x43_) and authorised_invocation aag (InvokeReply x41_ x42_ x43_) and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation (InvokeReply x41_ x42_ x43_) and authorised_invocation aag (InvokeReply x41_ x42_ x43_) and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)) s \<Longrightarrow> (pas_refined aag and integrity aag X st and einvs and tcb_at (cur_thread s) and cte_wp_at (is_reply_cap_to x41_) x42_ and K (is_subject aag (cur_thread s)) and K ((pasSubject aag, Reply, pasObjectAbs aag x41_) \<in> pasPolicy aag) and K (is_subject aag (fst x42_) \<and> (x43_ \<longrightarrow> is_subject aag x41_))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; integrity aag X st s; invs s; valid_list s; valid_sched s; simple_sched_action s; tcb_at x41_ s; cte_wp_at (\<lambda>cap. \<exists>R. cap = ReplyCap x41_ False R) x42_ s; x43_ \<longrightarrow> is_subject aag x41_; is_subject aag (fst x42_); (pasSubject aag, Reply, pasObjectAbs aag x41_) \<in> pasPolicy aag; is_subject aag (cur_thread s); \<forall>p ko. kheap s p = Some ko \<longrightarrow> (is_tcb ko \<longrightarrow> p \<noteq> cur_thread st) \<longrightarrow> kheap st p = Some ko\<rbrakk> \<Longrightarrow> tcb_at (cur_thread s) s \<and> cte_wp_at (is_reply_cap_to x41_) x42_ s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>

goal (7 subgoals):
 1. \<And>x1. oper = InvokeUntyped x1 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. \<And>x5. oper = InvokeTCB x5 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 3. \<And>x61 x62. oper = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 4. \<And>x7. oper = InvokeCNode x7 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 5. \<And>x8. oper = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 6. \<And>x9. oper = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 7. \<And>x10. oper = InvokeArchObject x10 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and simple_sched_action and valid_invocation oper and authorised_invocation aag oper and is_subject aag \<circ> cur_thread and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko)\<rbrace> perform_invocation blocking calling oper \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>