theory ArchRetype_AI

lemma pspace_respects_device_regionD:
  assumes inv:  "pspace_aligned s" "valid_objs s" "pspace_respects_device_region s"
  shows uat: "\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage False sz))
                \<Longrightarrow> obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> - device_region s"
      and dat: "\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage True sz))
                \<Longrightarrow> obj_range ptr (ArchObj $ DataPage True sz) \<subseteq> device_region s" using inv apply (simp_all add: pspace_respects_device_region_def) apply (rule subsetI) apply (drule obj_range_respect_device_range[OF _ inv(1)]) apply (clarsimp split: if_splits) apply (drule(1) subsetD[rotated]) apply (drule(1) subsetD[rotated]) apply (simp add: dom_def) apply (rule subsetI) apply (drule obj_range_respect_device_range[OF _ inv(1)]) apply (clarsimp split: if_splits) apply (drule(1) subsetD[rotated]) apply (drule(1) subsetD[rotated]) apply (simp add: dom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage False sz)) \<Longrightarrow> obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> - dom (device_state (machine_state s))) &&& (\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage True sz)) \<Longrightarrow> obj_range ptr (ArchObj $ DataPage True sz) \<subseteq> dom (device_state (machine_state s))) proof (prove)
using this:
pspace_aligned s
valid_objs s
pspace_respects_device_region s

goal (1 subgoal):
 1. (\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage False sz)) \<Longrightarrow> obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> - dom (device_state (machine_state s))) &&& (\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage True sz)) \<Longrightarrow> obj_range ptr (ArchObj $ DataPage True sz) \<subseteq> dom (device_state (machine_state s))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr sz. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage False sz)); pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj (DataPage False sz)) \<subseteq> - dom (device_state (machine_state s))
 2. \<And>ptr sz. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage True sz)); pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> dom (device_state (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>ptr sz x. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage False sz)); pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s)); x \<in> obj_range ptr (ArchObj (DataPage False sz))\<rbrakk> \<Longrightarrow> x \<in> - dom (device_state (machine_state s))
 2. \<And>ptr sz. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage True sz)); pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> dom (device_state (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>ptr sz x. \<lbrakk>pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s)); x \<in> obj_range ptr (ArchObj (DataPage False sz)); obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> (if False then dom (device_mem s) else dom (user_mem s))\<rbrakk> \<Longrightarrow> x \<in> - dom (device_state (machine_state s))
 2. \<And>ptr sz. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage True sz)); pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> dom (device_state (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>ptr sz x y. \<lbrakk>pspace_aligned s; valid_objs s; x \<in> obj_range ptr (ArchObj (DataPage False sz)); obj_range ptr (ArchObj (DataPage False sz)) \<subseteq> dom (user_mem s); dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)); dom (device_mem s) \<subseteq> dom (device_state (machine_state s)); device_state (machine_state s) x = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr sz. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage True sz)); pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> dom (device_state (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>ptr sz x y. \<lbrakk>pspace_aligned s; valid_objs s; obj_range ptr (ArchObj (DataPage False sz)) \<subseteq> dom (user_mem s); dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)); dom (device_mem s) \<subseteq> dom (device_state (machine_state s)); device_state (machine_state s) x = Some y; x \<in> dom (user_mem s)\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr sz. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage True sz)); pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> dom (device_state (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>ptr sz x y. \<lbrakk>pspace_aligned s; valid_objs s; obj_range ptr (ArchObj (DataPage False sz)) \<subseteq> dom (user_mem s); dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)); dom (device_mem s) \<subseteq> dom (device_state (machine_state s)); device_state (machine_state s) x = Some y; x \<in> - dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr sz. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage True sz)); pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> dom (device_state (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>ptr sz. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage True sz)); pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> dom (device_state (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>ptr sz x. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage True sz)); pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s)); x \<in> obj_range ptr (ArchObj (DataPage True sz))\<rbrakk> \<Longrightarrow> x \<in> dom (device_state (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>ptr sz x. \<lbrakk>pspace_aligned s; valid_objs s; dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)) \<and> dom (device_mem s) \<subseteq> dom (device_state (machine_state s)); x \<in> obj_range ptr (ArchObj (DataPage True sz)); obj_range ptr (ArchObj $ DataPage True sz) \<subseteq> (if True then dom (device_mem s) else dom (user_mem s))\<rbrakk> \<Longrightarrow> x \<in> dom (device_state (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>ptr sz x. \<lbrakk>pspace_aligned s; valid_objs s; x \<in> obj_range ptr (ArchObj (DataPage True sz)); obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> dom (device_mem s); dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)); dom (device_mem s) \<subseteq> dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> \<exists>y. device_state (machine_state s) x = Some y proof (prove)
goal (1 subgoal):
 1. \<And>ptr sz x. \<lbrakk>pspace_aligned s; valid_objs s; obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> dom (device_mem s); dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)); dom (device_mem s) \<subseteq> dom (device_state (machine_state s)); x \<in> dom (device_mem s)\<rbrakk> \<Longrightarrow> \<exists>y. device_state (machine_state s) x = Some y proof (prove)
goal (1 subgoal):
 1. \<And>ptr sz x. \<lbrakk>pspace_aligned s; valid_objs s; obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> dom (device_mem s); dom (user_mem s) \<subseteq> - dom (device_state (machine_state s)); dom (device_mem s) \<subseteq> dom (device_state (machine_state s)); x \<in> dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> \<exists>y. device_state (machine_state s) x = Some y proof (prove)
goal:
No subgoals!