theory Retype_C

lemma createObject_descendants_range_in':
  "\<lbrace>\<lambda>s.  descendants_range_in' S q (ctes_of s) \<and>
         pspace_aligned' s \<and>
         pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and>
         is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits
    \<rbrace>createObject ty ptr us dev \<lbrace>\<lambda>rv s. descendants_range_in' S q (ctes_of s)\<rbrace>" apply (simp add:createObject_def3 descendants_range_in'_def2) apply (wp createNewCaps_null_filter') apply clarsimp apply (intro conjI) apply simp apply (simp add:range_cover_full) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_range_in' S q (ctes_of s) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>rv s. descendants_range_in' S q (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv s. \<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> ((\<lambda>s. \<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ?sz11 and K (range_cover ptr ?sz11 (APIType_capBits ty us) (Suc 0) \<and> Suc 0 \<noteq> 0)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr (APIType_capBits ty us) s; is_aligned ptr (APIType_capBits ty us); APIType_capBits ty us < word_bits\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr ?sz11 s \<and> range_cover ptr ?sz11 (APIType_capBits ty us) (Suc 0) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr (APIType_capBits ty us) s; is_aligned ptr (APIType_capBits ty us); APIType_capBits ty us < word_bits\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr ?sz11 s
 2. \<And>s. \<lbrakk>\<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr (APIType_capBits ty us) s; is_aligned ptr (APIType_capBits ty us); APIType_capBits ty us < word_bits\<rbrakk> \<Longrightarrow> range_cover ptr ?sz11 (APIType_capBits ty us) (Suc 0) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>p'\<in>descendants_of' q (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr (APIType_capBits ty us) s; is_aligned ptr (APIType_capBits ty us); APIType_capBits ty us < word_bits\<rbrakk> \<Longrightarrow> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) proof (prove)
goal:
No subgoals!