theory Retype_C

lemma caps_no_overlap''_le:
  "\<lbrakk>caps_no_overlap'' ptr sz s;us \<le> sz;sz < word_bits\<rbrakk>
    \<Longrightarrow> caps_no_overlap'' ptr us s" apply (clarsimp simp:caps_no_overlap''_def) apply (drule(1) bspec) apply (subgoal_tac  "{ptr..(ptr && ~~ mask us) + 2 ^ us - 1}
                      \<subseteq>  {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}") apply (erule impE) apply (rule ccontr) apply clarify apply (drule(1) disjoint_subset2[rotated -1]) apply simp apply (erule subsetD)+ apply simp apply clarsimp apply (frule neg_mask_diff_bound[where ptr = ptr]) apply (simp add:p_assoc_help) apply (rule word_plus_mcs[where x = "2 ^ us - 1 + (ptr && ~~ mask sz)"]) apply (simp add:field_simps) apply (simp add:field_simps) apply (simp add:p_assoc_help) apply (rule word_plus_mono_right) apply (simp add: word_bits_def) apply (erule two_power_increasing) apply simp apply (rule is_aligned_no_overflow') apply (simp add:is_aligned_neg_mask) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_no_overlap'' ptr sz s; us \<le> sz; sz < word_bits\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr us s proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>\<forall>cte\<in>ran (ctes_of s). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 3. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<not> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 3. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<not> False; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 3. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<not> False; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 3. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1\<rbrakk> \<Longrightarrow> x \<in> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1}
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + 2 ^ us - 1\<rbrakk> \<Longrightarrow> (ptr && ~~ mask us) + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + 2 ^ us - 1; (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> (ptr && ~~ mask us) + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> (ptr && ~~ mask us) + (2 ^ us - 1) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> (ptr && ~~ mask us) + (2 ^ us - 1) - (2 ^ us - 1 + (ptr && ~~ mask sz)) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) - (2 ^ us - 1 + (ptr && ~~ mask sz))
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> 2 ^ us - 1 + (ptr && ~~ mask sz) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> 2 ^ us - 1 + (ptr && ~~ mask sz) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + 2 ^ us - 1; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + 2 ^ us - 1; (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (2 ^ us - 1) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> 2 ^ us - 1 \<le> 2 ^ sz - 1
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < 32; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> 2 ^ us \<le> 2 ^ sz
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<And>cte x. \<lbrakk>sz < 32; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> sz < LENGTH(32)
 2. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>cte x. \<lbrakk>us \<le> sz; sz < word_bits; cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> up_aligned_area ptr us \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask us) + (2 ^ us - 1); untypedRange (cteCap cte) \<inter> up_aligned_area ptr sz \<noteq> {} \<longrightarrow> up_aligned_area ptr sz \<subseteq> untypedRange (cteCap cte); ptr \<le> (ptr && ~~ mask us) + (2 ^ us - 1); (ptr && ~~ mask us) - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ us\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask sz) sz proof (prove)
goal:
No subgoals!