theory ArchVSpaceEntries_AI

lemma call_kernel_valid_pdpt[wp]:
  "\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and valid_pdpt_objs\<rbrace>
      (call_kernel e) :: (unit,unit) s_monad
   \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>" apply (cases e, simp_all add: call_kernel_def) apply (rule hoare_pre) apply (wp | simp add: if_apply_def2 | wpc
                 | rule conjI | clarsimp simp: ct_in_state_def
                 | erule pred_tcb_weakenE
                 | wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> call_kernel e \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1. e = SyscallEvent x1 \<Longrightarrow> \<lbrace>invs and ct_running and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- (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) <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs and ct_running and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 3. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs and ct_running and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 4. e = Interrupt \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 5. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs and ct_running and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 6. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs and ct_running and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x1. e = SyscallEvent x1 \<Longrightarrow> \<lbrace>?Q4 x1\<rbrace> do y <- (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) <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>x1 s. \<lbrakk>e = SyscallEvent x1; (invs and ct_running and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) s\<rbrakk> \<Longrightarrow> ?Q4 x1 s
 3. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>invs and ct_running and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- liftE (do thread <- gets cur_thread;
handle_fault thread (UnknownSyscallException (word_of_nat x2))
od);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 4. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>invs and ct_running and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- liftE (do thread <- gets cur_thread;
handle_fault thread (UserException x31 (x32 && mask 28))
od);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 5. e = Interrupt \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 6. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> \<lbrace>invs and ct_running and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- liftE (do thread <- gets cur_thread;
handle_vm_fault thread x5 <catch> handle_fault thread
od);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 7. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> \<lbrace>invs and ct_running and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> do y <- liftE (do thread <- gets cur_thread;
handle_hypervisor_fault thread x6
od);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal:
No subgoals!