theory DetSchedSchedule_AI

lemma handle_event_valid_sched:
  "\<lbrace>invs and valid_sched and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)
      and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace>
   handle_event e
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (cases e, simp_all) apply (rename_tac syscall) apply (case_tac syscall, simp_all add: handle_send_def handle_call_def) apply ((rule hoare_pre, wp handle_invocation_valid_sched handle_recv_valid_sched'
              handle_reply_valid_sched
              | fastforce simp: invs_valid_objs invs_sym_refs valid_sched_ct_not_queued)+)[5] apply (wp handle_fault_valid_sched hvmf_active hoare_drop_imps hoare_vcg_disj_lift
                 handle_recv_valid_sched' handle_reply_valid_sched hoare_vcg_all_lift|
              wpc |
              clarsimp simp: ct_in_state_def valid_sched_ct_not_queued |
              fastforce simp: valid_fault_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_sched and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> handle_event e \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1. e = SyscallEvent x1 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> case x1 of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. e = Interrupt \<Longrightarrow> \<lbrace>invs and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>syscall. e = SyscallEvent syscall \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> case syscall of SysCall \<Rightarrow> handle_call | SysReplyRecv \<Rightarrow> without_preemption $ do handle_reply;
handle_recv True
od | SysSend \<Rightarrow> handle_send True | SysNBSend \<Rightarrow> handle_send False | SysRecv \<Rightarrow> without_preemption $ handle_recv True | SysReply \<Rightarrow> without_preemption handle_reply | SysYield \<Rightarrow> without_preemption handle_yield | SysNBRecv \<Rightarrow> without_preemption $ handle_recv False \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. e = Interrupt \<Longrightarrow> \<lbrace>invs and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (13 subgoals):
 1. \<And>syscall. \<lbrakk>e = SyscallEvent SysCall; syscall = SysCall\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> handle_invocation True True \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>syscall. \<lbrakk>e = SyscallEvent SysReplyRecv; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do y <- handle_reply;
handle_recv True
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>syscall. \<lbrakk>e = SyscallEvent SysSend; syscall = SysSend\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> handle_invocation False True \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>syscall. \<lbrakk>e = SyscallEvent SysNBSend; syscall = SysNBSend\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> handle_invocation False False \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>syscall. \<lbrakk>e = SyscallEvent SysRecv; syscall = SysRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (handle_recv True) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>syscall. \<lbrakk>e = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE handle_reply \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>syscall. \<lbrakk>e = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE handle_yield \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>syscall. \<lbrakk>e = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (handle_recv False) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 9. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 10. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
A total of 13 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>syscall. \<lbrakk>e = SyscallEvent SysReply; syscall = SysReply\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE handle_reply \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>syscall. \<lbrakk>e = SyscallEvent SysYield; syscall = SysYield\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE handle_yield \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>syscall. \<lbrakk>e = SyscallEvent SysNBRecv; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (handle_recv False) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. e = Interrupt \<Longrightarrow> \<lbrace>invs and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!