theory Detype_R

lemma pspace_no_overlap'_modify:
  "\<lbrace>K (range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)) \<and> ptr \<noteq> 0) and
    pspace_no_overlap' (((1::word32) + of_nat n << objBitsKO val + us) + ptr)
                       (objBitsKO val + us)\<rbrace>
   modify (ksPSpace_update
     (foldr (\<lambda>addr map. map(addr \<mapsto> val))
            (new_cap_addrs (unat ((1::word32) + of_nat n << us)) ptr val)))
   \<lbrace>\<lambda>r. pspace_no_overlap'
          (((1::word32) + of_nat n << objBitsKO val + us) + ptr)
          (objBitsKO val + us)\<rbrace>" proof - note 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 show ?thesis apply (clarsimp simp:simpler_modify_def valid_def pspace_no_overlap'_def) apply (frule(1) range_cover_tail_mask) apply (simp add:field_simps) apply (drule_tac x = x in spec) apply (clarsimp simp:foldr_upd_app_if split:if_splits) apply (frule obj_range'_subset_strong[rotated]) apply (drule range_cover_le[where n = "Suc n"]) apply simp apply (rule range_cover_rel,assumption) apply simp apply clarsimp apply (frule range_cover.unat_of_nat_n_shift[where gbits = us,symmetric]) apply simp+ apply (simp add:field_simps) apply (simp add:obj_range'_def) apply (erule disjoint_subset) apply (frule(1) range_cover_ptr_le) apply (subgoal_tac
    "\<not> ptr + (1 + of_nat n << us + objBitsKO val) \<le> ptr + (1 + of_nat n << us) * 2 ^ objBitsKO val - 1") apply (clarsimp simp:blah field_simps) apply (clarsimp simp: not_le) apply (rule word_leq_le_minus_one) apply (clarsimp simp: power_add[symmetric] shiftl_t2n field_simps objSize_eq_capBits ) apply (rule neq_0_no_wrap) apply (clarsimp simp: power_add[symmetric] shiftl_t2n field_simps objSize_eq_capBits ) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)) \<and> ptr \<noteq> 0) and pspace_no_overlap' ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\<rbrace> modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val))) \<lbrace>\<lambda>r. pspace_no_overlap' ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>K (range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)) \<and> ptr \<noteq> 0) and pspace_no_overlap' ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\<rbrace> modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val))) \<lbrace>\<lambda>r. pspace_no_overlap' ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\<rbrace> proof (state)
this:
untyped_range (cap.UntypedCap ?dev ?p ?n ?f) = {?p..?p + (1 << ?n) - 1}
untyped_range cap.NullCap = {}
untyped_range (cap.EndpointCap ?r ?badge ?rights) = {}
untyped_range (cap.NotificationCap ?r ?badge ?rights) = {}
untyped_range (cap.CNodeCap ?r ?bits ?guard) = {}
untyped_range (cap.ThreadCap ?r) = {}
untyped_range cap.DomainCap = {}
untyped_range (cap.ReplyCap ?r ?master ?rights) = {}
untyped_range cap.IRQControlCap = {}
untyped_range (cap.IRQHandlerCap ?irq) = {}
untyped_range (cap.Zombie ?r ?b ?n) = {}
untyped_range (cap.ArchObjectCap ?cap) = {}
usable_untyped_range (cap.UntypedCap ?uu ?p ?n ?f) = (if ?f < 2 ^ ?n then {?p + word_of_nat ?f..?p + 2 ^ ?n - 1} else {})
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)
(\<exists>x. ?P x) = (\<exists>a b. ?P (a, b))

goal (1 subgoal):
 1. \<lbrace>K (range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)) \<and> ptr \<noteq> 0) and pspace_no_overlap' ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\<rbrace> modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val))) \<lbrace>\<lambda>r. pspace_no_overlap' ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)) \<and> ptr \<noteq> 0) and pspace_no_overlap' ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\<rbrace> modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val))) \<lbrace>\<lambda>r. pspace_no_overlap' ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x ko. \<lbrakk>range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us) = {}; foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s) x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x ko. \<lbrakk>range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us) = {}; foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s) x = Some ko; ptr + (1 + word_of_nat n << objBitsKO val + us) && ~~ mask sz = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x ko. \<lbrakk>range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s) x = Some ko; ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x ko. \<lbrakk>range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s) x = Some ko; ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val)\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val)\<rbrakk> \<Longrightarrow> range_cover ptr (?sz37 s x) (objBitsKO val) (unat (1 + word_of_nat n << us))
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val)\<rbrakk> \<Longrightarrow> Suc n \<le> Suc (Suc n)
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); range_cover ptr sz (us + objBitsKO val) (Suc n)\<rbrakk> \<Longrightarrow> range_cover ptr (?sz37 s x) (objBitsKO val) (unat (1 + word_of_nat n << us))
 3. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); range_cover ptr sz (us + objBitsKO val) (Suc n)\<rbrakk> \<Longrightarrow> range_cover ptr (?sz37 s x) (objBitsKO val) (unat (1 + word_of_nat n << us))
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); range_cover ptr sz (us + objBitsKO val) (Suc n)\<rbrakk> \<Longrightarrow> objBitsKO val \<le> us + objBitsKO val
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); range_cover ptr sz (us + objBitsKO val) (Suc n)\<rbrakk> \<Longrightarrow> unat (1 + word_of_nat n << us) = 2 ^ (us + objBitsKO val - objBitsKO val) * Suc n
 3. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); range_cover ptr sz (us + objBitsKO val) (Suc n)\<rbrakk> \<Longrightarrow> unat (1 + word_of_nat n << us) = 2 ^ (us + objBitsKO val - objBitsKO val) * Suc n
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); range_cover ptr sz (us + objBitsKO val) (Suc n)\<rbrakk> \<Longrightarrow> unat (1 + word_of_nat n << us) = 2 ^ us + 2 ^ us * n
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); range_cover ptr sz (us + objBitsKO val) (Suc n)\<rbrakk> \<Longrightarrow> us \<le> us + objBitsKO val
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); range_cover ptr sz (us + objBitsKO val) (Suc n); Suc n * 2 ^ us = unat (word_of_nat (Suc n) << us)\<rbrakk> \<Longrightarrow> unat (1 + word_of_nat n << us) = 2 ^ us + 2 ^ us * n
 3. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); range_cover ptr sz (us + objBitsKO val) (Suc n); 2 ^ us + n * 2 ^ us = unat (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> unat (1 + word_of_nat n << us) = 2 ^ us + 2 ^ us * n
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); {x..x + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val)\<rbrakk> \<Longrightarrow> {ptr..ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)\<rbrakk> \<Longrightarrow> {ptr..ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val); \<not> ptr + (1 + word_of_nat n << us + objBitsKO val) \<le> ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val - 1\<rbrakk> \<Longrightarrow> {ptr..ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)\<rbrakk> \<Longrightarrow> \<not> ptr + (1 + word_of_nat n << us + objBitsKO val) \<le> ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val - 1 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)\<rbrakk> \<Longrightarrow> \<not> ptr + (1 + word_of_nat n << us + objBitsKO val) \<le> ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val - 1 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val - 1 < ptr + (1 + word_of_nat n << us + objBitsKO val) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val
 2. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask sz = ptr && ~~ mask sz; \<forall>ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << us + objBitsKO val)..2 ^ (us + objBitsKO val) + (ptr + (1 + word_of_nat n << us + objBitsKO val) && ~~ mask (us + objBitsKO val)) - 1} = {}; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ptr \<le> ptr + (1 + word_of_nat n << us + objBitsKO val)\<rbrakk> \<Longrightarrow> ptr \<noteq> 0 proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>K (range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)) \<and> ptr \<noteq> 0) and pspace_no_overlap' ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\<rbrace> modify (ksPSpace_update (foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val))) \<lbrace>\<lambda>r. pspace_no_overlap' ((1 + word_of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\<rbrace>

goal:
No subgoals!