theory ArchRetype_AI

lemma obj_range_respect_device_range:
  "\<lbrakk>kheap s ptr = Some (ArchObj (DataPage dev sz));pspace_aligned s\<rbrakk> \<Longrightarrow>
  obj_range ptr (ArchObj $ DataPage dev sz) \<subseteq> (if dev then dom (device_mem s) else dom (user_mem s))" apply (drule(1) pspace_alignedD[rotated]) apply (clarsimp simp: user_mem_def in_user_frame_def obj_at_def obj_range_def device_mem_def in_device_frame_def) apply (intro impI conjI) apply clarsimp apply (rule exI[where x = sz]) apply (simp add: mask_in_range[symmetric,THEN iffD1] a_type_def) apply clarsimp apply (rule exI[where x = sz]) apply (simp add: mask_in_range[symmetric,THEN iffD1] a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage dev sz)); pspace_aligned s\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj $ DataPage dev sz) \<subseteq> (if dev then dom (device_mem s) else dom (user_mem s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage dev sz)); is_aligned ptr (obj_bits (ArchObj (DataPage dev sz)))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj $ DataPage dev sz) \<subseteq> (if dev then dom (device_mem s) else dom (user_mem s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage dev sz)); is_aligned ptr (pageBitsForSize sz)\<rbrakk> \<Longrightarrow> (dev \<longrightarrow> {ptr..ptr + 2 ^ pageBitsForSize sz - 1} \<subseteq> dom (\<lambda>p. if \<exists>sz ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz) then Some p else None)) \<and> (\<not> dev \<longrightarrow> {ptr..ptr + 2 ^ pageBitsForSize sz - 1} \<subseteq> dom (\<lambda>p. if \<exists>sz ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz) then Some (underlying_memory (machine_state s) p) else None)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage dev sz)); is_aligned ptr (pageBitsForSize sz); dev\<rbrakk> \<Longrightarrow> {ptr..ptr + 2 ^ pageBitsForSize sz - 1} \<subseteq> dom (\<lambda>p. if \<exists>sz ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz) then Some p else None)
 2. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage dev sz)); is_aligned ptr (pageBitsForSize sz); \<not> dev\<rbrakk> \<Longrightarrow> {ptr..ptr + 2 ^ pageBitsForSize sz - 1} \<subseteq> dom (\<lambda>p. if \<exists>sz ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz) then Some (underlying_memory (machine_state s) p) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage True sz)); is_aligned ptr (pageBitsForSize sz); dev; ptr \<le> x; x \<le> ptr + 2 ^ pageBitsForSize sz - 1\<rbrakk> \<Longrightarrow> \<exists>sz ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)
 2. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage dev sz)); is_aligned ptr (pageBitsForSize sz); \<not> dev\<rbrakk> \<Longrightarrow> {ptr..ptr + 2 ^ pageBitsForSize sz - 1} \<subseteq> dom (\<lambda>p. if \<exists>sz ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz) then Some (underlying_memory (machine_state s) p) else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage True sz)); is_aligned ptr (pageBitsForSize sz); dev; ptr \<le> x; x \<le> ptr + 2 ^ pageBitsForSize sz - 1\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)
 2. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage dev sz)); is_aligned ptr (pageBitsForSize sz); \<not> dev\<rbrakk> \<Longrightarrow> {ptr..ptr + 2 ^ pageBitsForSize sz - 1} \<subseteq> dom (\<lambda>p. if \<exists>sz ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz) then Some (underlying_memory (machine_state s) p) else None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage dev sz)); is_aligned ptr (pageBitsForSize sz); \<not> dev\<rbrakk> \<Longrightarrow> {ptr..ptr + 2 ^ pageBitsForSize sz - 1} \<subseteq> dom (\<lambda>p. if \<exists>sz ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz) then Some (underlying_memory (machine_state s) p) else None) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage False sz)); is_aligned ptr (pageBitsForSize sz); \<not> dev; ptr \<le> x; x \<le> ptr + 2 ^ pageBitsForSize sz - 1\<rbrakk> \<Longrightarrow> \<exists>sz ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kheap s ptr = Some (ArchObj (DataPage False sz)); is_aligned ptr (pageBitsForSize sz); \<not> dev; ptr \<le> x; x \<le> ptr + 2 ^ pageBitsForSize sz - 1\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz) proof (prove)
goal:
No subgoals!