theory Retype_C

lemma createObject_caps_no_overlap'':
  " \<lbrace>\<lambda>s. caps_no_overlap'' (ptr + (1 + of_nat n << APIType_capBits newType userSize))
                     sz s \<and>
     pspace_aligned' s \<and> pspace_distinct' s \<and>
     pspace_no_overlap' (ptr + (of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s
     \<and> is_aligned ptr (APIType_capBits newType userSize)
     \<and> APIType_capBits newType userSize < word_bits\<rbrace>
   createObject newType (ptr + (of_nat n << APIType_capBits newType userSize)) userSize dev
   \<lbrace>\<lambda>rv s. caps_no_overlap'' (ptr + (1 + of_nat n << APIType_capBits newType userSize))
                     sz s \<rbrace>" apply (clarsimp simp:createObject_def3 caps_no_overlap''_def2) apply (wp createNewCaps_null_filter') apply clarsimp apply (intro conjI) apply simp apply (rule range_cover_full) apply (erule aligned_add_aligned) apply (rule is_aligned_shiftl_self) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps_no_overlap'' (ptr + (1 + word_of_nat n << APIType_capBits newType userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s \<and> is_aligned ptr (APIType_capBits newType userSize) \<and> APIType_capBits newType userSize < word_bits\<rbrace> global.createObject newType (ptr + (word_of_nat n << APIType_capBits newType userSize)) userSize dev \<lbrace>\<lambda>rv. caps_no_overlap'' (ptr + (1 + word_of_nat n << APIType_capBits newType userSize)) sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s \<and> is_aligned ptr (APIType_capBits newType userSize) \<and> APIType_capBits newType userSize < word_bits\<rbrace> do m <- createNewCaps newType (ptr + (word_of_nat n << APIType_capBits newType userSize)) (Suc 0) userSize dev;
return (hd m)
od \<lbrace>\<lambda>rv s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s \<and> is_aligned ptr (APIType_capBits newType userSize) \<and> APIType_capBits newType userSize < word_bits \<Longrightarrow> ((\<lambda>s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) ?sz4 and K (range_cover (ptr + (word_of_nat n << APIType_capBits newType userSize)) ?sz4 (APIType_capBits newType userSize) (Suc 0) \<and> Suc 0 \<noteq> 0)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; is_aligned ptr (APIType_capBits newType userSize); APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) ?sz4 s \<and> range_cover (ptr + (word_of_nat n << APIType_capBits newType userSize)) ?sz4 (APIType_capBits newType userSize) (Suc 0) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; is_aligned ptr (APIType_capBits newType userSize); APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) ?sz4 s
 2. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; is_aligned ptr (APIType_capBits newType userSize); APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> range_cover (ptr + (word_of_nat n << APIType_capBits newType userSize)) ?sz4 (APIType_capBits newType userSize) (Suc 0) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; is_aligned ptr (APIType_capBits newType userSize); APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> range_cover (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) (APIType_capBits newType userSize) (Suc 0) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; is_aligned ptr (APIType_capBits newType userSize); APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> is_aligned (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize)
 2. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; is_aligned ptr (APIType_capBits newType userSize); APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> APIType_capBits newType userSize < word_bits proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat n << APIType_capBits newType userSize) (APIType_capBits newType userSize)
 2. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> APIType_capBits newType userSize \<le> APIType_capBits newType userSize
 3. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; is_aligned ptr (APIType_capBits newType userSize); APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> APIType_capBits newType userSize < word_bits proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> APIType_capBits newType userSize \<le> APIType_capBits newType userSize
 2. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; is_aligned ptr (APIType_capBits newType userSize); APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> APIType_capBits newType userSize < word_bits proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..(ptr + (1 + word_of_nat n << APIType_capBits newType userSize) && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits newType userSize)) (APIType_capBits newType userSize) s; is_aligned ptr (APIType_capBits newType userSize); APIType_capBits newType userSize < word_bits\<rbrakk> \<Longrightarrow> APIType_capBits newType userSize < word_bits proof (prove)
goal:
No subgoals!