theory Retype_C

lemma createObject_idlethread_range:
  "\<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits
        \<and> ksIdleThread s \<notin> {ptr..ptr + 2 ^ (APIType_capBits ty us) - 1}\<rbrace>
   createObject ty ptr us dev \<lbrace>\<lambda>cap s. ksIdleThread s \<notin> capRange cap\<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_idlethread_ranges[where sz = "APIType_capBits ty us"]]) apply assumption apply clarsimp apply (clarsimp simp:word_bits_conv range_cover_full) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> ksIdleThread s \<notin> {ptr..ptr + 2 ^ APIType_capBits ty us - 1}\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>cap s. ksIdleThread s \<notin> capRange cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> (ptr \<le> ksIdleThread s \<longrightarrow> \<not> ksIdleThread s \<le> ptr + 2 ^ APIType_capBits ty us - 1)\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>cap s. ksIdleThread s \<notin> capRange cap\<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>cap s. ksIdleThread s \<notin> capRange cap\<rbrace>
 2. \<And>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> (ptr \<le> ksIdleThread s \<longrightarrow> \<not> ksIdleThread s \<le> ptr + 2 ^ APIType_capBits ty us - 1) \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>m a. ksIdleThread a \<notin> capRange (hd m)\<rbrace>
 2. \<And>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> (ptr \<le> ksIdleThread s \<longrightarrow> \<not> ksIdleThread s \<le> ptr + 2 ^ APIType_capBits ty us - 1) \<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> ksIdleThread s \<notin> capRange (hd rv)
 3. \<And>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> (ptr \<le> ksIdleThread s \<longrightarrow> \<not> ksIdleThread s \<le> ptr + 2 ^ APIType_capBits ty us - 1) \<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> ksIdleThread s \<notin> capRange (hd rv)
 4. \<And>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> (ptr \<le> ksIdleThread s \<longrightarrow> \<not> ksIdleThread s \<le> ptr + 2 ^ APIType_capBits ty us - 1) \<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> ksIdleThread s \<notin> capRange (hd rv)
 4. \<And>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> (ptr \<le> ksIdleThread s \<longrightarrow> \<not> ksIdleThread s \<le> ptr + 2 ^ APIType_capBits ty us - 1) \<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> ksIdleThread s \<notin> capRange (hd rv)
 3. \<And>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> (ptr \<le> ksIdleThread s \<longrightarrow> \<not> ksIdleThread s \<le> ptr + 2 ^ APIType_capBits ty us - 1) \<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>cap\<in>set rv. ksIdleThread s \<notin> capRange cap \<Longrightarrow> ?Q13 rv s
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> ksIdleThread s \<notin> capRange (hd rv)
 3. \<And>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> (ptr \<le> ksIdleThread s \<longrightarrow> \<not> ksIdleThread s \<le> ptr + 2 ^ APIType_capBits ty us - 1) \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<and> ksIdleThread s \<notin> {ptr..(ptr && ~~ mask (APIType_capBits ty us)) + 2 ^ APIType_capBits ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<And>rv s. rv \<noteq> [] \<and> (\<forall>cap\<in>set rv. ksIdleThread s \<notin> capRange cap) \<Longrightarrow> ksIdleThread s \<notin> capRange (hd rv)
 2. \<And>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> (ptr \<le> ksIdleThread s \<longrightarrow> \<not> ksIdleThread s \<le> ptr + 2 ^ APIType_capBits ty us - 1) \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<and> ksIdleThread s \<notin> {ptr..(ptr && ~~ mask (APIType_capBits ty us)) + 2 ^ APIType_capBits ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> (ptr \<le> ksIdleThread s \<longrightarrow> \<not> ksIdleThread s \<le> ptr + 2 ^ APIType_capBits ty us - 1) \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<and> ksIdleThread s \<notin> {ptr..(ptr && ~~ mask (APIType_capBits ty us)) + 2 ^ APIType_capBits ty us - 1} proof (prove)
goal:
No subgoals!