theory Retype_C

lemma createObject_descendants_range':
  "\<lbrace>\<lambda>s.  descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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' rv q (ctes_of s)\<rbrace>" apply (simp add:createObject_def3) apply (rule hoare_pre) apply wp apply (rule_tac Q = "\<lambda>r s. r \<noteq> [] \<and> Q r s" for Q in hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule hoare_strengthen_post[OF createNewCaps_ret_len]) apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_descendants_range_ret'[where sz = "APIType_capBits ty us"]]) apply assumption apply fastforce apply (clarsimp simp add:word_bits_conv range_cover_full) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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' rv q (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv s. descendants_range' rv q (ctes_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv s. descendants_range' rv q (ctes_of s)\<rbrace>
 2. \<And>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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 \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>m a. descendants_range' (hd m) q (ctes_of a)\<rbrace>
 2. \<And>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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 \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q1\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>r s. r \<noteq> [] \<and> ?Q13 r s\<rbrace>
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> descendants_range' (hd rv) q (ctes_of s)
 3. \<And>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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 \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>rv s. rv \<noteq> []\<rbrace>
 2. \<lbrace>?P'14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q13\<rbrace>
 3. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> descendants_range' (hd rv) q (ctes_of s)
 4. \<And>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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 \<Longrightarrow> ?P14 s \<and> ?P'14 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. Suc 0 = length rv \<Longrightarrow> rv \<noteq> []
 2. \<lbrace>?P'14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q13\<rbrace>
 3. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> descendants_range' (hd rv) q (ctes_of s)
 4. \<And>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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 \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> ?P'14 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q13\<rbrace>
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> descendants_range' (hd rv) q (ctes_of s)
 3. \<And>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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 \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> ?P'14 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<forall>y\<in>set rv. descendants_range' y ?cref25 (ctes_of s) \<Longrightarrow> ?Q13 rv s
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> descendants_range' (hd rv) q (ctes_of s)
 3. \<And>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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 \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> (range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<and> 0 < Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> descendants_range_in' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} ?cref25 (ctes_of s) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. rv \<noteq> [] \<and> (\<forall>y\<in>set rv. descendants_range' y ?cref25 (ctes_of s)) \<Longrightarrow> descendants_range' (hd rv) q (ctes_of s)
 2. \<And>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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 \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> (range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<and> 0 < Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> descendants_range_in' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} ?cref25 (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>s. descendants_range_in' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} 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 \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> (range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<and> 0 < Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> descendants_range_in' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} q (ctes_of s) proof (prove)
goal:
No subgoals!