theory Detype_R

lemma placeNewObject_ko_wp_at':
  "\<lbrace>\<lambda>s. (if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val))
         then P (injectKOS val)
         else ko_wp_at' P slot s) \<and>
        objBitsKO (injectKOS val) + us < word_bits \<and>
        is_aligned ptr (objBitsKO (injectKOS val) + us) \<and>
        pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and>
        pspace_aligned' s \<and> pspace_distinct' s\<rbrace>
   placeNewObject ptr val us
   \<lbrace>\<lambda>a. ko_wp_at' P slot\<rbrace>" apply (clarsimp simp:valid_def split del:if_split) apply (simp add:simpler_placeNewObject_def simpler_modify_def) apply (subst data_map_insert_def[symmetric])+ apply (subst retype_ko_wp_at') apply simp+ apply (rule range_cover_rel[OF range_cover_full]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s) \<and> objBitsKO (injectKOS val) + us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>a. ko_wp_at' P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (placeNewObject ptr val us s); if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> ko_wp_at' P slot b proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> ko_wp_at' P slot (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> ko_wp_at' P slot (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s)\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_distinct' s
 3. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (?sz15 s) s
 4. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz15 s) (objBitsKO (injectKOS val)) (2 ^ us)
 5. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val)) (2 ^ us)
 2. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (injectKOS val) + us)
 2. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS val) + us < word_bits
 3. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS val) \<le> objBitsKO (injectKOS val) + us
 4. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> 2 ^ us = 2 ^ (objBitsKO (injectKOS val) + us - objBitsKO (injectKOS val)) * Suc 0
 5. \<And>s. \<lbrakk>if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s; objBitsKO (injectKOS val) + us < word_bits; is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> if slot \<in> set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s proof (prove)
goal:
No subgoals!