theory Retype_AC

lemma usable_range_disjoint:
  assumes cte_wp_at: "cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s"
  assumes misc: "distinct slots" "idx \<le> unat (ptr && mask sz) \<or> ptr = ptr && ~~ mask sz"
                "invs s" "slots \<noteq> []" "ct_active s"
                "\<forall>slot\<in>set slots. cte_wp_at ((=) NullCap) slot s"
                "\<forall>x\<in>set slots. ex_cte_cap_wp_to (\<lambda>_. True) x s"
  assumes cover: "range_cover ptr sz (obj_bits_api tp us) (length slots)"
  notes blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff
                         atLeastatMost_subset_iff atLeastLessThan_iff
                         Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
  shows
       "usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz
                                         (unat ((ptr && mask sz) +
                                          of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter>
        {ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {}" proof - have not_0_ptr[simp]: "ptr\<noteq> 0" using misc cte_wp_at apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule(1) caps_of_state_valid) apply (clarsimp simp:valid_cap_def) done have idx_compare''[simp]:
       "unat ((ptr && mask sz) + (of_nat (length slots) * 2 ^ obj_bits_api tp us)) < 2 ^ sz
        \<Longrightarrow> ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1
        < ptr + of_nat (length slots) * 2 ^ obj_bits_api 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 only: word_bits_def range_cover.sz(1)[OF cover]) apply simp done show ?thesis apply (clarsimp simp:mask_out_sub_mask blah) apply (drule idx_compare'') apply (simp add:not_le[symmetric]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {} proof (state)
goal (1 subgoal):
 1. usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {} proof (prove)
goal (1 subgoal):
 1. ptr \<noteq> 0 proof (prove)
using this:
distinct slots
idx \<le> unat (ptr && mask sz) \<or> ptr = ptr && ~~ mask sz
invs s
slots \<noteq> []
ct_active s
\<forall>slot\<in>set slots. cte_wp_at ((=) NullCap) slot s
\<forall>x\<in>set slots. ex_cte_cap_wp_to (\<lambda>_. True) x s
cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s

goal (1 subgoal):
 1. ptr \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct slots; invs s; slots \<noteq> []; ct_active s; \<forall>slot\<in>set slots. caps_of_state s slot = Some NullCap; \<forall>x\<in>set slots. ex_cte_cap_wp_to (\<lambda>_. True) x s; caps_of_state s cref = Some (UntypedCap dev 0 sz idx); ptr = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct slots; slots \<noteq> []; ct_active s; \<forall>slot\<in>set slots. caps_of_state s slot = Some NullCap; \<forall>x\<in>set slots. ex_cte_cap_wp_to (\<lambda>_. True) x s; caps_of_state s cref = Some (UntypedCap dev 0 sz idx); ptr = 0; s \<turnstile> UntypedCap dev 0 sz idx\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
ptr \<noteq> 0

goal (1 subgoal):
 1. usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter> {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {} proof (prove)
goal (1 subgoal):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us proof (prove)
goal (1 subgoal):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr \<le> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us
 2. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> unat (ptr && mask ?sz6) + unat (word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ ?sz6
 2. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ?sz6 < word_bits
 3. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> sz < word_bits
 2. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. unat ((ptr && mask sz) + word_of_nat (length slots) * 2 ^ obj_bits_api 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 ^ obj_bits_api tp us) < 2 ^ sz \<Longrightarrow> ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us

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

goal:
No subgoals!