theory ArchSchedule_AI

lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]:
  "valid invs (do_machine_op (mapM (\<lambda>p. storeWord p 0) S)) (\<lambda>_. invs)" apply (simp add: dom_mapM ef_storeWord) apply (rule mapM_UNIV_wp) apply (simp add: do_machine_op_def split_def) apply wp apply (clarsimp simp: invs_def valid_state_def cur_tcb_def
                        valid_machine_state_def) apply (rule conjI) apply(erule use_valid[OF _ storeWord_valid_irq_states], simp) apply (erule use_valid) apply (simp add: storeWord_def word_rsplit_0) apply wp apply (clarsimp simp: word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op (mapM (\<lambda>p. storeWord p 0) S) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> mapM (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) S \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set S \<Longrightarrow> \<lbrace>invs\<rbrace> (do_machine_op \<circ> (\<lambda>p. storeWord p 0)) x \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set S \<Longrightarrow> \<lbrace>invs\<rbrace> do ms <- gets machine_state;
p <- select_f (storeWord x 0 ms);
modify (machine_state_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>x \<in> set S; invs s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (storeWord x 0 (machine_state s)). invs (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x s b. \<lbrakk>x \<in> set S; ((), b) \<in> fst (storeWord x 0 (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := b\<rparr>) \<and> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = 0) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b)\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x s b. \<lbrakk>x \<in> set S; ((), b) \<in> fst (storeWord x 0 (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := b\<rparr>)
 2. \<And>x s b. \<lbrakk>x \<in> set S; ((), b) \<in> fst (storeWord x 0 (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = 0) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b)\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x s b. \<lbrakk>x \<in> set S; ((), b) \<in> fst (storeWord x 0 (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = 0) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), b)\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), b)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x s b. \<lbrakk>x \<in> set S; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> \<lbrace>?P62 x s b\<rbrace> storeWord x 0 \<lbrace>\<lambda>a b. (\<forall>p. in_user_frame p s \<or> underlying_memory b p = 0) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd (a, b)\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd (a, b)\<rparr>)\<rbrace>
 2. \<And>x s b. \<lbrakk>x \<in> set S; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> ?P62 x s b (machine_state s) proof (prove)
goal (2 subgoals):
 1. \<And>x s b. \<lbrakk>x \<in> set S; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> \<lbrace>?P62 x s b\<rbrace> do y <- assert (x && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(x := 0, x + 1 := 0, x + 2 := 0, x + 3 := 0)))
od \<lbrace>\<lambda>a b. (\<forall>p. in_user_frame p s \<or> underlying_memory b p = 0) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd (a, b)\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd (a, b)\<rparr>)\<rbrace>
 2. \<And>x s b. \<lbrakk>x \<in> set S; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> ?P62 x s b (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>x s b. \<lbrakk>x \<in> set S; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> x && mask 2 = 0 \<longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory (underlying_memory_update (\<lambda>m. m(x := 0, x + 1 := 0, x + 2 := 0, x + 3 := 0)) (machine_state s)) p = 0) \<and> pspace_respects_device_region (s\<lparr>machine_state := snd ((), underlying_memory_update (\<lambda>m. m(x := 0, x + 1 := 0, x + 2 := 0, x + 3 := 0)) (machine_state s))\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := snd ((), underlying_memory_update (\<lambda>m. m(x := 0, x + 1 := 0, x + 2 := 0, x + 3 := 0)) (machine_state s))\<rparr>) proof (prove)
goal:
No subgoals!