theory Retype_AI

lemma valid_cap_pres:
  "\<lbrakk> s \<turnstile> c; cte_wp_at ((=) c) (oref,cref) s \<rbrakk> \<Longrightarrow> s' \<turnstile> c" using cover mem orth apply (simp add:s'_def ps_def) apply (rule valid_untyped_helper[ OF _ _ tyunt cover _ _ _ vp ]) apply simp+ apply (simp add:cte_wp_at_caps_of_state) apply (drule res[unfolded caps_overlap_reserved_def,THEN bspec,OF ranI]) apply simp apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s\<rbrakk> \<Longrightarrow> s' \<turnstile> c proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n
caps_no_overlap ptr sz s
pspace_no_overlap (up_aligned_area ptr sz) s

goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s\<rbrakk> \<Longrightarrow> s' \<turnstile> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> c proof (prove)
goal (5 subgoals):
 1. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> s \<turnstile> c
 2. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) c) ?q6 s
 3. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c \<inter> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api ty us) - 1} = {}
 4. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s
 5. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}
 2. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s
 3. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s \<turnstile> c; caps_of_state s (oref, cref) = Some c; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; is_untyped_cap c\<rbrakk> \<Longrightarrow> usable_untyped_range c \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}
 2. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s
 3. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s \<turnstile> c; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; is_untyped_cap c; is_untyped_cap c \<longrightarrow> usable_untyped_range c \<inter> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api ty us) - 1} = {}\<rbrakk> \<Longrightarrow> usable_untyped_range c \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}
 2. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s
 3. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s
 2. \<lbrakk>s \<turnstile> c; cte_wp_at ((=) c) (oref, cref) s; range_cover ptr sz (obj_bits_api ty us) n; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal:
No subgoals!