theory Untyped_R

lemma usableRange_disjoint:
      "usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz
       (unat ((ptr && mask sz) + of_nat (length slots) * 2 ^ APIType_capBits tp us))) \<inter>
       {ptr..ptr + of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} = {}" proof - have idx_compare''[simp]:
       "unat ((ptr && mask sz) + (of_nat (length slots) * (2::word32) ^ APIType_capBits tp us)) < 2 ^ sz
        \<Longrightarrow> ptr + of_nat (length slots) * 2 ^ APIType_capBits tp us - 1
        < ptr + of_nat (length slots) * 2 ^ APIType_capBits tp us" apply (rule word_leq_le_minus_one,simp) apply (rule neq_0_no_wrap) apply (rule machine_word_plus_mono_right_split) apply (simp add: shiftl_t2n range_cover_unat[OF cover] field_simps) apply (simp add: range_cover.sz(1)
        [where 'a=32, folded word_bits_def, OF cover])+ done show ?thesis apply (clarsimp simp: mask_out_sub_mask) apply (drule idx_compare'') apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} = {} proof (state)
goal (1 subgoal):
 1. usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} = {} proof (prove)
goal (1 subgoal):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1 < ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us proof (prove)
goal (1 subgoal):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz \<Longrightarrow> ptr \<le> ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us
 2. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz \<Longrightarrow> unat (ptr && mask ?sz6) + unat (word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ ?sz6
 2. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz \<Longrightarrow> ?sz6 < word_bits
 3. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz \<Longrightarrow> sz < word_bits
 2. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal:
No subgoals! proof (state)
this:
unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1 < ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us

goal (1 subgoal):
 1. usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} = {} proof (prove)
goal (1 subgoal):
 1. usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us) < 2 ^ sz; ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us \<le> ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1; ptr \<le> ptr - (ptr && mask sz) + 2 ^ sz - 1; ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us \<le> ptr - (ptr && mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us \<le> ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1; ptr \<le> ptr - (ptr && mask sz) + 2 ^ sz - 1; ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us \<le> ptr - (ptr && mask sz) + 2 ^ sz - 1; ptr \<le> ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1; ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1 < ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
usableUntypedRange (capability.UntypedCap d (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ APIType_capBits tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} = {}

goal:
No subgoals!