theory Untyped_AI

lemma retype_ret_valid_caps:
  "\<lbrace>pspace_no_overlap_range_cover ptr sz
      and K (tp = Structures_A.CapTableObject \<longrightarrow> us > 0)
      and K (tp = Untyped \<longrightarrow> untyped_min_bits \<le> us)
      and K (tp \<noteq> ArchObject ASIDPoolObj)
      and K (range_cover ptr sz (obj_bits_api tp us) n \<and> ptr \<noteq> 0)\<rbrace>
        retype_region ptr n us tp dev\<lbrace>\<lambda>rv (s::'state_ext state). \<forall>y\<in>set rv. s \<turnstile> default_cap tp y us dev\<rbrace>" apply (simp add: retype_region_def split del: if_split cong: if_cong) apply wp apply (simp only: trans_state_update[symmetric] more_update.valid_cap_update) apply wp apply (case_tac tp,simp_all) defer apply ((clarsimp simp:valid_cap_def default_object_def cap_aligned_def
        is_obj_defs well_formed_cnode_n_def empty_cnode_def
        dom_def  ptr_add_def | rule conjI | intro conjI obj_at_foldr_intro imageI
      | rule is_aligned_add_multI[OF _ le_refl],
        (simp add:range_cover_def word_bits_def obj_bits_api_def)+)+)[3] apply (rule_tac ptr=ptr and sz=sz in retype_ret_valid_caps_captable; simp) apply (rule_tac ptr=ptr and sz=sz in retype_ret_valid_caps_aobj; simp) apply (clarsimp simp:valid_cap_def default_object_def cap_aligned_def
        is_obj_defs well_formed_cnode_n_def empty_cnode_def
        dom_def ptr_add_def | intro conjI obj_at_foldr_intro
        imageI
      | rule is_aligned_add_multI[OF _ le_refl]
      | fastforce simp:range_cover_def obj_bits_api_def
          word_bits_def a_type_def)+ apply (clarsimp simp:valid_cap_def valid_untyped_def) apply (drule(1) pspace_no_overlap_obj_range) apply (frule range_cover_cell_subset) apply (erule of_nat_mono_maybe[rotated]) apply (drule range_cover.range_cover_n_less) apply (simp add:word_bits_def) apply (simp add:obj_bits_api_def field_simps
               del:atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
           Int_atLeastAtMost atLeastatMost_empty_iff) apply blast apply (erule(2) range_cover_no_0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap (up_aligned_area ptr sz) and K (tp = CapTableObject \<longrightarrow> 0 < us) and K (tp = Untyped \<longrightarrow> untyped_min_bits \<le> us) and K (tp \<noteq> ArchObject ASIDPoolObj) and K (range_cover ptr sz (obj_bits_api tp us) n \<and> ptr \<noteq> 0)\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. s \<turnstile> default_cap tp y us dev\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>y. tp = CapTableObject \<longrightarrow> 0 < us) and (\<lambda>y. tp = Untyped \<longrightarrow> untyped_min_bits \<le> us) and (\<lambda>y. tp \<noteq> ArchObject ASIDPoolObj) and (\<lambda>y. range_cover ptr sz (obj_bits_api tp us) n \<and> ptr \<noteq> 0)\<rbrace> do y <- when (tp \<noteq> Untyped) (do kh <- gets kheap;
y <- do_extended_op (retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]) tp);
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object tp dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]) kh))
od);
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n])
od \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. s \<turnstile> default_cap tp y us dev\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>kh s f. tp \<noteq> Untyped \<Longrightarrow> (\<forall>y\<in>set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]). trans_state f s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object tp dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]) kh\<rparr> \<turnstile> default_cap tp y us dev) = (\<forall>y\<in>set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]). s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object tp dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]) kh\<rparr> \<turnstile> default_cap tp y us dev)
 2. tp \<noteq> Untyped \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets kheap \<lbrace>\<lambda>kh s. \<forall>y\<in>set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]). s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object tp dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]) kh\<rparr> \<turnstile> default_cap tp y us dev\<rbrace>
 3. \<And>s. (pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>y. tp = CapTableObject \<longrightarrow> 0 < us) and (\<lambda>y. tp = Untyped \<longrightarrow> untyped_min_bits \<le> us) and (\<lambda>y. tp \<noteq> ArchObject ASIDPoolObj) and (\<lambda>y. range_cover ptr sz (obj_bits_api tp us) n \<and> ptr \<noteq> 0)) s \<Longrightarrow> (if tp \<noteq> Untyped then ?Q3 else (\<lambda>a. \<forall>y\<in>set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]). a \<turnstile> default_cap tp y us dev)) s proof (prove)
goal (2 subgoals):
 1. tp \<noteq> Untyped \<Longrightarrow> \<lbrace>?Q3\<rbrace> gets kheap \<lbrace>\<lambda>kh s. \<forall>y\<in>set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]). s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object tp dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]) kh\<rparr> \<turnstile> default_cap tp y us dev\<rbrace>
 2. \<And>s. (pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>y. tp = CapTableObject \<longrightarrow> 0 < us) and (\<lambda>y. tp = Untyped \<longrightarrow> untyped_min_bits \<le> us) and (\<lambda>y. tp \<noteq> ArchObject ASIDPoolObj) and (\<lambda>y. range_cover ptr sz (obj_bits_api tp us) n \<and> ptr \<noteq> 0)) s \<Longrightarrow> (if tp \<noteq> Untyped then ?Q3 else (\<lambda>a. \<forall>y\<in>set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]). a \<turnstile> default_cap tp y us dev)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>y. tp = CapTableObject \<longrightarrow> 0 < us) and (\<lambda>y. tp = Untyped \<longrightarrow> untyped_min_bits \<le> us) and (\<lambda>y. tp \<noteq> ArchObject ASIDPoolObj) and (\<lambda>y. range_cover ptr sz (obj_bits_api tp us) n \<and> ptr \<noteq> 0)) s \<Longrightarrow> (if tp \<noteq> Untyped then \<lambda>s. \<forall>y\<in>set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]). s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object tp dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]) (kheap s)\<rparr> \<turnstile> default_cap tp y us dev else (\<lambda>a. \<forall>y\<in>set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]). a \<turnstile> default_cap tp y us dev)) s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> untyped_min_bits \<le> us \<and> range_cover ptr sz (obj_bits_api Untyped us) n \<and> ptr \<noteq> 0; tp = Untyped\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s \<turnstile> UntypedCap dev (ptr_add ptr (y * 2 ^ obj_bits_api Untyped us)) us 0
 2. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> range_cover ptr sz (obj_bits_api TCBObject us) n \<and> ptr \<noteq> 0; tp = TCBObject\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object TCBObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api TCBObject us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ThreadCap (ptr_add ptr (y * 2 ^ obj_bits_api TCBObject us))
 3. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> range_cover ptr sz (obj_bits_api EndpointObject us) n \<and> ptr \<noteq> 0; tp = EndpointObject\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object EndpointObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api EndpointObject us)) [0..<n]) (kheap s)\<rparr> \<turnstile> EndpointCap (ptr_add ptr (y * 2 ^ obj_bits_api EndpointObject us)) 0 UNIV
 4. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> range_cover ptr sz (obj_bits_api NotificationObject us) n \<and> ptr \<noteq> 0; tp = NotificationObject\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object NotificationObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api NotificationObject us)) [0..<n]) (kheap s)\<rparr> \<turnstile> NotificationCap (ptr_add ptr (y * 2 ^ obj_bits_api NotificationObject us)) 0 {AllowRead, AllowWrite}
 5. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> 0 < us \<and> range_cover ptr sz (obj_bits_api CapTableObject us) n \<and> ptr \<noteq> 0; tp = CapTableObject\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object CapTableObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api CapTableObject us)) [0..<n]) (kheap s)\<rparr> \<turnstile> CNodeCap (ptr_add ptr (y * 2 ^ obj_bits_api CapTableObject us)) us []
 6. \<And>s x6. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> x6 \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \<and> ptr \<noteq> 0; tp = ArchObject x6\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x6) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev) proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> range_cover ptr sz (obj_bits_api TCBObject us) n \<and> ptr \<noteq> 0; tp = TCBObject\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object TCBObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api TCBObject us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ThreadCap (ptr_add ptr (y * 2 ^ obj_bits_api TCBObject us))
 2. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> range_cover ptr sz (obj_bits_api EndpointObject us) n \<and> ptr \<noteq> 0; tp = EndpointObject\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object EndpointObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api EndpointObject us)) [0..<n]) (kheap s)\<rparr> \<turnstile> EndpointCap (ptr_add ptr (y * 2 ^ obj_bits_api EndpointObject us)) 0 UNIV
 3. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> range_cover ptr sz (obj_bits_api NotificationObject us) n \<and> ptr \<noteq> 0; tp = NotificationObject\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object NotificationObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api NotificationObject us)) [0..<n]) (kheap s)\<rparr> \<turnstile> NotificationCap (ptr_add ptr (y * 2 ^ obj_bits_api NotificationObject us)) 0 {AllowRead, AllowWrite}
 4. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> 0 < us \<and> range_cover ptr sz (obj_bits_api CapTableObject us) n \<and> ptr \<noteq> 0; tp = CapTableObject\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object CapTableObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api CapTableObject us)) [0..<n]) (kheap s)\<rparr> \<turnstile> CNodeCap (ptr_add ptr (y * 2 ^ obj_bits_api CapTableObject us)) us []
 5. \<And>s x6. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> x6 \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \<and> ptr \<noteq> 0; tp = ArchObject x6\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x6) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)
 6. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> untyped_min_bits \<le> us \<and> range_cover ptr sz (obj_bits_api Untyped us) n \<and> ptr \<noteq> 0; tp = Untyped\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s \<turnstile> UntypedCap dev (ptr_add ptr (y * 2 ^ obj_bits_api Untyped us)) us 0 proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> 0 < us \<and> range_cover ptr sz (obj_bits_api CapTableObject us) n \<and> ptr \<noteq> 0; tp = CapTableObject\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object CapTableObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api CapTableObject us)) [0..<n]) (kheap s)\<rparr> \<turnstile> CNodeCap (ptr_add ptr (y * 2 ^ obj_bits_api CapTableObject us)) us []
 2. \<And>s x6. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> x6 \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \<and> ptr \<noteq> 0; tp = ArchObject x6\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x6) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)
 3. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> untyped_min_bits \<le> us \<and> range_cover ptr sz (obj_bits_api Untyped us) n \<and> ptr \<noteq> 0; tp = Untyped\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s \<turnstile> UntypedCap dev (ptr_add ptr (y * 2 ^ obj_bits_api Untyped us)) us 0 proof (prove)
goal (2 subgoals):
 1. \<And>s x6. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> x6 \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \<and> ptr \<noteq> 0; tp = ArchObject x6\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x6) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0..<n]) (kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)
 2. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> untyped_min_bits \<le> us \<and> range_cover ptr sz (obj_bits_api Untyped us) n \<and> ptr \<noteq> 0; tp = Untyped\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s \<turnstile> UntypedCap dev (ptr_add ptr (y * 2 ^ obj_bits_api Untyped us)) us 0 proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s \<and> untyped_min_bits \<le> us \<and> range_cover ptr sz (obj_bits_api Untyped us) n \<and> ptr \<noteq> 0; tp = Untyped\<rbrakk> \<Longrightarrow> \<forall>y\<in>{0..<n}. s \<turnstile> UntypedCap dev (ptr_add ptr (y * 2 ^ obj_bits_api Untyped us)) us 0 proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap dev (ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us) us 0) s
 2. \<And>s y. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s y p obj. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> obj_range p obj \<subseteq> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<and> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<inter> obj_range p obj = {}
 2. \<And>s y. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s y p obj. \<lbrakk>tp = Untyped; y < n; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<noteq> {}; obj_range p obj \<inter> up_aligned_area ptr sz = {}\<rbrakk> \<Longrightarrow> obj_range p obj \<subseteq> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<and> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<inter> obj_range p obj = {}
 2. \<And>s y. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<And>s y p obj. \<lbrakk>tp = Untyped; y < n; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<noteq> {}; obj_range p obj \<inter> up_aligned_area ptr sz = {}\<rbrakk> \<Longrightarrow> ?x110 s y p obj < word_of_nat n
 2. \<And>s y p obj. \<lbrakk>tp = Untyped; y < n; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<noteq> {}; obj_range p obj \<inter> up_aligned_area ptr sz = {}; {ptr + ?x110 s y p obj * 2 ^ obj_bits_api Untyped us..ptr + ?x110 s y p obj * 2 ^ obj_bits_api Untyped us + 2 ^ obj_bits_api Untyped us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> obj_range p obj \<subseteq> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<and> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<inter> obj_range p obj = {}
 3. \<And>s y. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<And>s y p obj. \<lbrakk>tp = Untyped; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<noteq> {}; obj_range p obj \<inter> up_aligned_area ptr sz = {}\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH(32)
 2. \<And>s y p obj. \<lbrakk>tp = Untyped; y < n; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<noteq> {}; obj_range p obj \<inter> up_aligned_area ptr sz = {}; {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ obj_bits_api Untyped us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> obj_range p obj \<subseteq> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<and> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<inter> obj_range p obj = {}
 3. \<And>s y. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<And>s y p obj. \<lbrakk>tp = Untyped; untyped_min_bits \<le> us; ptr \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<noteq> {}; obj_range p obj \<inter> up_aligned_area ptr sz = {}; n < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH(32)
 2. \<And>s y p obj. \<lbrakk>tp = Untyped; y < n; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<noteq> {}; obj_range p obj \<inter> up_aligned_area ptr sz = {}; {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ obj_bits_api Untyped us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> obj_range p obj \<subseteq> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<and> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<inter> obj_range p obj = {}
 3. \<And>s y. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s y p obj. \<lbrakk>tp = Untyped; y < n; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<noteq> {}; obj_range p obj \<inter> up_aligned_area ptr sz = {}; {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ obj_bits_api Untyped us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> obj_range p obj \<subseteq> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<and> {ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us..ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us + 2 ^ us - 1} \<inter> obj_range p obj = {}
 2. \<And>s y. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s y p obj. \<lbrakk>tp = Untyped; y < n; untyped_min_bits \<le> us; range_cover ptr sz us n; ptr \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr + word_of_nat y * 2 ^ us..ptr + (2 ^ us + word_of_nat y * 2 ^ us) - 1} \<noteq> {}; obj_range p obj \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr + word_of_nat y * 2 ^ us..ptr + (2 ^ us + word_of_nat y * 2 ^ us) - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> obj_range p obj \<subseteq> {ptr + word_of_nat y * 2 ^ us..ptr + (2 ^ us + word_of_nat y * 2 ^ us) - 1} \<and> {ptr + word_of_nat y * 2 ^ us..ptr + (2 ^ us + word_of_nat y * 2 ^ us) - 1} \<inter> obj_range p obj = {}
 2. \<And>s y. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>tp = Untyped; y < n; pspace_no_overlap (up_aligned_area ptr sz) s; untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api Untyped us) n; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat y * 2 ^ obj_bits_api Untyped us \<noteq> 0 proof (prove)
goal:
No subgoals!