theory ArchVSpaceEntries_AI

lemma perform_invocation_valid_pdpt[wp]:
  "\<lbrace>invs and ct_active and valid_invocation i and valid_pdpt_objs
           and invocation_duplicates_valid i\<rbrace>
      perform_invocation blocking call i
         \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (cases i, simp_all) apply (wp send_signal_interrupt_states | simp)+ apply (simp add: arch_perform_invocation_def) apply (rule hoare_pre) apply (wp | wpc | simp)+ apply (auto simp: valid_arch_inv_def invocation_duplicates_valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active and valid_invocation i and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid i\<rbrace> perform_invocation blocking call i \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x1. i = InvokeUntyped x1 \<Longrightarrow> \<lbrace>invs and ct_active and valid_untyped_inv x1 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeUntyped x1)\<rbrace> doE y <- invoke_untyped x1;
returnOk []
odE \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>x21 x22 x23 x24. i = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs and ct_active and (ep_at x21 and ex_nonz_cap_to x21) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeEndpoint x21 x22 x23 x24)\<rbrace> liftE (do thread <- gets cur_thread;
y <- send_ipc blocking call x22 x23 x24 thread x21;
return []
od) \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 3. \<And>x31 x32. i = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>invs and ct_active and (ntfn_at x31 and ex_nonz_cap_to x31) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeNotification x31 x32)\<rbrace> doE y <- liftE (send_signal x31 x32);
returnOk []
odE \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 4. \<And>x41 x42 x43. i = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>invs and ct_active and (tcb_at x41 and cte_wp_at (\<lambda>cap. \<exists>R. cap = ReplyCap x41 False R) x42) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeReply x41 x42 x43)\<rbrace> liftE (do sender <- gets cur_thread;
y <- do_reply_transfer sender x41 x42 x43;
return []
od) \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 5. \<And>x5. i = InvokeTCB x5 \<Longrightarrow> \<lbrace>invs and ct_active and tcb_inv_wf x5 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeTCB x5)\<rbrace> invoke_tcb x5 \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 6. \<And>x61 x62. i = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>invs and ct_active and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeDomain x61 x62)\<rbrace> invoke_domain x61 x62 \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 7. \<And>x7. i = InvokeCNode x7 \<Longrightarrow> \<lbrace>invs and ct_active and valid_cnode_inv x7 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeCNode x7)\<rbrace> doE y <- invoke_cnode x7;
returnOk []
odE \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 8. \<And>x8. i = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>invs and ct_active and irq_control_inv_valid x8 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeIRQControl x8)\<rbrace> doE y <- invoke_irq_control x8;
returnOk []
odE \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 9. \<And>x9. i = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>invs and ct_active and irq_handler_inv_valid x9 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeIRQHandler x9)\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 10. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>invs and ct_active and valid_arch_inv x10 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeArchObject x10)\<rbrace> arch_perform_invocation x10 \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>?Q76 x10\<rbrace> arch_perform_invocation x10 \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>x10 s. \<lbrakk>i = InvokeArchObject x10; (invs and ct_active and valid_arch_inv x10 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeArchObject x10)) s\<rbrakk> \<Longrightarrow> ?Q76 x10 s proof (prove)
goal (2 subgoals):
 1. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>?Q76 x10\<rbrace> case x10 of InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od \<lbrace>\<lambda>rv s. Ball (ran (kheap s)) obj_valid_pdpt\<rbrace>
 2. \<And>x10 s. \<lbrakk>i = InvokeArchObject x10; (invs and ct_active and valid_arch_inv x10 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeArchObject x10)) s\<rbrakk> \<Longrightarrow> ?Q76 x10 s proof (prove)
goal (3 subgoals):
 1. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>?Q78 x10\<rbrace> case x10 of InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od \<lbrace>\<lambda>rv s. Ball (ran (kheap s)) obj_valid_pdpt\<rbrace>
 2. \<And>x10 s. \<lbrakk>i = InvokeArchObject x10; ?Q76 x10 s\<rbrakk> \<Longrightarrow> ?Q78 x10 s
 3. \<And>x10 s. \<lbrakk>i = InvokeArchObject x10; (invs and ct_active and valid_arch_inv x10 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invocation_duplicates_valid (InvokeArchObject x10)) s\<rbrakk> \<Longrightarrow> ?Q76 x10 s proof (prove)
goal (1 subgoal):
 1. \<And>x10 s. \<lbrakk>i = InvokeArchObject x10; invs s \<and> ct_active s \<and> valid_arch_inv x10 s \<and> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> invocation_duplicates_valid (InvokeArchObject x10) s\<rbrakk> \<Longrightarrow> (\<forall>x. x10 = InvokePageTable x \<longrightarrow> valid_pti x s \<and> pti_duplicates_valid x s) \<and> (\<forall>x. x10 = InvokePageDirectory x \<longrightarrow> valid_pdi x s) \<and> (\<forall>x. x10 = InvokePage x \<longrightarrow> valid_page_inv x s \<and> page_inv_duplicates_valid x s) proof (prove)
goal:
No subgoals!