theory KHeap_AI

lemma dmo_invs1:
  assumes "\<And>P. f \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace>"
  shows
  "\<lbrace>\<lambda>s. \<forall>m. \<forall>(r,m')\<in>fst (f m). m = machine_state s \<longrightarrow>
               (\<forall>p. in_user_frame p s  \<or> underlying_memory m' p = underlying_memory m p) \<and>
               (\<forall>irq. (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or>
                       irq_masks m' irq = irq_masks m irq) \<and>
               invs s\<rbrace>
   do_machine_op f
   \<lbrace>\<lambda>_. invs\<rbrace>" unfolding do_machine_op_def apply wpsimp apply (rename_tac s rv s') apply (clarsimp simp: invs_def cur_tcb_def valid_state_def valid_machine_state_def
                   intro!: valid_irq_states_machine_state_updateI
                   elim: valid_irq_statesE) apply (frule_tac P1 = "(=) (device_state (machine_state s))" in use_valid[OF _ assms], simp) apply (fastforce simp: invs_def cur_tcb_def valid_state_def valid_machine_state_def
                   intro: valid_irq_states_machine_state_updateI
                    elim: valid_irq_statesE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (f m). m = machine_state s \<longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s\<rbrace> do_machine_op f \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (f m). m = machine_state s \<longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (f ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>\<forall>m. \<forall>x\<in>fst (f m). case x of (r, m') \<Rightarrow> m = machine_state s \<longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory (machine_state s) p) \<and> (\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq \<or> irq_masks m' irq = irq_masks (machine_state s) irq) \<and> invs s; (x, xa) \<in> fst (f (machine_state s))\<rbrakk> \<Longrightarrow> invs (s\<lparr>machine_state := xa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s rv s'. \<lbrakk>\<forall>m. \<forall>x\<in>fst (f m). case x of (r, m') \<Rightarrow> m = machine_state s \<longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory (machine_state s) p) \<and> (\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq \<or> irq_masks m' irq = irq_masks (machine_state s) irq) \<and> invs s; (rv, s') \<in> fst (f (machine_state s))\<rbrakk> \<Longrightarrow> invs (s\<lparr>machine_state := s'\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s rv s'. \<lbrakk>\<forall>m. \<forall>x\<in>fst (f m). case x of (r, m') \<Rightarrow> m = machine_state s \<longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory (machine_state s) p) \<and> (\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq \<or> irq_masks m' irq = irq_masks (machine_state s) irq) \<and> valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> (\<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0) \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> tcb_at (cur_thread s) s; (rv, s') \<in> fst (f (machine_state s))\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states (s\<lparr>machine_state := s'\<rparr>) \<and> valid_ioports s \<and> (\<forall>p. in_user_frame p s \<or> underlying_memory s' p = 0) \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region (s\<lparr>machine_state := s'\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := s'\<rparr>) \<and> tcb_at (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s rv s'. \<lbrakk>\<forall>m. \<forall>x\<in>fst (f m). case x of (r, m') \<Rightarrow> m = machine_state s \<longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory (machine_state s) p) \<and> (\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq \<or> irq_masks m' irq = irq_masks (machine_state s) irq) \<and> valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> (\<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0) \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> tcb_at (cur_thread s) s; (rv, s') \<in> fst (f (machine_state s)); device_state (machine_state s) = device_state s'\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states (s\<lparr>machine_state := s'\<rparr>) \<and> valid_ioports s \<and> (\<forall>p. in_user_frame p s \<or> underlying_memory s' p = 0) \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region (s\<lparr>machine_state := s'\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := s'\<rparr>) \<and> tcb_at (cur_thread s) s proof (prove)
goal:
No subgoals!