theory PageTableDuplicates

lemma handleEvent_valid_duplicates':
  "\<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
    sch_act_simple and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)\<rbrace>
   handleEvent e
   \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (case_tac e, simp_all add: handleEvent_def) apply (rename_tac syscall) apply (case_tac syscall) apply (wp handleReply_sane
              | simp add: active_from_running' simple_sane_strg cong: if_cong
              | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)\<rbrace> handleEvent e \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1. e = SyscallEvent x1 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> case x1 of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. e = Interrupt \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple\<rbrace> liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> liftE (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> liftE (do thread <- getCurThread;
handleHypervisorFault thread x6
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>syscall. e = SyscallEvent syscall \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. e = Interrupt \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple\<rbrace> liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> liftE (do thread <- getCurThread;
handleVMFault thread x5 <catch> handleFault thread
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> liftE (do thread <- getCurThread;
handleHypervisorFault thread x6
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (13 subgoals):
 1. \<And>syscall. \<lbrakk>e = SyscallEvent syscall; syscall = SysCall\<rbrakk> \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>syscall. \<lbrakk>e = SyscallEvent syscall; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>syscall. \<lbrakk>e = SyscallEvent syscall; syscall = SysSend\<rbrakk> \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>syscall. \<lbrakk>e = SyscallEvent syscall; syscall = SysNBSend\<rbrakk> \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>syscall. \<lbrakk>e = SyscallEvent syscall; syscall = SysRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>syscall. \<lbrakk>e = SyscallEvent syscall; syscall = SysReply\<rbrakk> \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>syscall. \<lbrakk>e = SyscallEvent syscall; syscall = SysYield\<rbrakk> \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 8. \<And>syscall. \<lbrakk>e = SyscallEvent syscall; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> case syscall of SysCall \<Rightarrow> handleCall | SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SysSend \<Rightarrow> handleSend True | SysNBSend \<Rightarrow> handleSend False | SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SysReply \<Rightarrow> withoutPreemption handleReply | SysYield \<Rightarrow> withoutPreemption handleYield | SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 9. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UnknownSyscallException (word_of_nat x2))
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 10. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and ct_running'\<rbrace> liftE (do thread <- getCurThread;
handleFault thread (Fault_H.fault.UserException x31 (x32 && mask 28))
od) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
A total of 13 subgoals... proof (prove)
goal:
No subgoals!