theory ArchRetype_AI

lemma clearMemory_invs:
  "\<lbrace>invs\<rbrace> do_machine_op (clearMemory w sz) \<lbrace>\<lambda>_. invs\<rbrace>" apply (wp dmo_invs1) apply clarsimp apply (intro conjI impI allI) apply (clarsimp simp: invs_def valid_state_def) apply (erule_tac p=p in valid_machine_stateE) apply (clarsimp simp: use_valid[OF _ clearMemory_underlying_mem_0]) apply (clarsimp simp: use_valid[OF _ clearMemory_irq_masks_inv[where P="(=) v" for v], OF _ refl]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op (clearMemory w sz) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (clearMemory w sz 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 proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>invs s; ((), b) \<in> fst (clearMemory w sz (machine_state s))\<rbrakk> \<Longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = underlying_memory (machine_state s) p) \<and> (\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks b irq \<or> irq_masks b irq = irq_masks (machine_state s) irq) proof (prove)
goal (2 subgoals):
 1. \<And>s b p. \<lbrakk>invs s; ((), b) \<in> fst (clearMemory w sz (machine_state s))\<rbrakk> \<Longrightarrow> in_user_frame p s \<or> underlying_memory b p = underlying_memory (machine_state s) p
 2. \<And>s b irq. \<lbrakk>invs s; ((), b) \<in> fst (clearMemory w sz (machine_state s)); interrupt_states s irq = IRQInactive\<rbrakk> \<Longrightarrow> irq_masks b irq \<or> irq_masks b irq = irq_masks (machine_state s) irq proof (prove)
goal (2 subgoals):
 1. \<And>s b p. \<lbrakk>((), b) \<in> fst (clearMemory w sz (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; valid_machine_state s; 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; cur_tcb s; underlying_memory b p \<noteq> underlying_memory (machine_state s) p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s b irq. \<lbrakk>invs s; ((), b) \<in> fst (clearMemory w sz (machine_state s)); interrupt_states s irq = IRQInactive\<rbrakk> \<Longrightarrow> irq_masks b irq \<or> irq_masks b irq = irq_masks (machine_state s) irq proof (prove)
goal (2 subgoals):
 1. \<And>s b p. \<lbrakk>((), b) \<in> fst (clearMemory w sz (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; 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; cur_tcb s; underlying_memory b p \<noteq> underlying_memory (machine_state s) p; in_user_frame p s \<or> underlying_memory (machine_state s) p = 0\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s b irq. \<lbrakk>invs s; ((), b) \<in> fst (clearMemory w sz (machine_state s)); interrupt_states s irq = IRQInactive\<rbrakk> \<Longrightarrow> irq_masks b irq \<or> irq_masks b irq = irq_masks (machine_state s) irq proof (prove)
goal (1 subgoal):
 1. \<And>s b irq. \<lbrakk>invs s; ((), b) \<in> fst (clearMemory w sz (machine_state s)); interrupt_states s irq = IRQInactive\<rbrakk> \<Longrightarrow> irq_masks b irq \<or> irq_masks b irq = irq_masks (machine_state s) irq proof (prove)
goal:
No subgoals!