theory Untyped_AI

lemma (in Untyped_AI_nonempty_table) create_caps_invs_inv:
  assumes create_cap_Q[wp]:
    "\<lbrace>invs and Q and cte_wp_at (\<lambda>c. is_untyped_cap c
            \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range c
            \<and> {oref .. oref + 2 ^ (obj_bits_api tp us) - 1} \<subseteq> untyped_range c) p
        and cte_wp_at ((=) NullCap) cref
        and valid_cap (default_cap tp oref sz dev)\<rbrace>
         create_cap tp sz p dev (cref,oref) \<lbrace>\<lambda>_. Q \<rbrace>"
  shows
  "\<lbrace>(\<lambda>s. invs (s::('state_ext::state_ext) state) \<and> Q s
       \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c)  p s
       \<and> (\<forall>tup \<in> set ((cref,oref)#list).
           cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range c
           \<and> {snd tup .. snd tup + 2 ^ (obj_bits_api tp us) - 1} \<subseteq> untyped_range c
           \<and> (untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range c = {})) p s)
       \<and> (\<forall>tup \<in> set ((cref,oref)#list).
           descendants_range (default_cap tp (snd tup) sz dev) p s)
       \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) ((cref,oref)#list))
       \<and> (\<forall>tup \<in> set ((cref,oref)#list).
           cte_wp_at ((=) cap.NullCap) (fst tup) s)
       \<and> (\<forall>tup \<in> set ((cref,oref)#list).
              valid_cap (default_cap tp (snd tup) sz dev) s)
       \<and> (\<forall>tup \<in> set ((cref,oref)#list).
              ex_cte_cap_wp_to is_cnode_cap (fst tup) s)
       \<and> (\<forall>tup \<in> set ((cref,oref)#list).
              real_cte_at (fst tup) s)
       \<and> (\<forall>tup \<in> set ((cref,oref)#list). \<forall>r \<in> obj_refs (default_cap tp (snd tup) sz dev).
                (\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> Structures_A.obj_refs cap) p' s)
              \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
       \<and> distinct (p # (map fst ((cref,oref)#list)))
       \<and> tp \<noteq> ArchObject ASIDPoolObj) \<rbrace>
     create_cap tp sz p dev (cref,oref)
   \<lbrace>(\<lambda>r s.
         invs s \<and> Q s
       \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c)  p s
       \<and> (\<forall>tup \<in> set list.
           cte_wp_at (\<lambda>c.
           cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range c
           \<and> {snd tup .. snd tup + 2 ^ (obj_bits_api tp us) - 1} \<subseteq> untyped_range c
           \<and> (untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range c = {})) p s)
       \<and> (\<forall>tup \<in> set list.
           descendants_range (default_cap tp (snd tup) sz dev) p s)
       \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list)
       \<and> (\<forall>tup \<in> set list.
           cte_wp_at ((=) cap.NullCap) (fst tup) s)
       \<and> (\<forall>tup \<in> set list.
              valid_cap (default_cap tp (snd tup) sz dev) s)
       \<and> (\<forall>tup \<in> set list.
              ex_cte_cap_wp_to is_cnode_cap (fst tup) s)
       \<and> (\<forall>tup \<in> set list.
              real_cte_at (fst tup) s)
       \<and> (\<forall>tup \<in> set list. \<forall>r \<in> obj_refs (default_cap tp (snd tup) sz dev).
                (\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> Structures_A.obj_refs cap) p' s)
              \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
       \<and> distinct (p # (map fst list))
       \<and> tp \<noteq> ArchObject ASIDPoolObj) \<rbrace>" apply (rule hoare_pre) apply (wp hoare_vcg_const_Ball_lift | clarsimp)+ apply (clarsimp simp: conj_comms invs_mdb distinct_sets_prop distinct_prop_map
                        ex_cte_cap_to_cnode_always_appropriate_strg) apply (simp add: cte_wp_at_caps_of_state[where p=p]
      | erule exE conjE)+ apply (intro conjI) apply (clarsimp simp:image_def) apply (drule(1) bspec)+ apply simp apply (fastforce simp:cap_range_def) apply (clarsimp simp:is_cap_simps) apply (simp only: UN_extend_simps UNION_empty_conv) apply (drule(1) bspec)+ apply clarsimp apply blast apply (clarsimp simp: cap_range_def) apply (clarsimp simp: cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> Q s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c) p s \<and> (\<forall>tup\<in>set ((cref, oref) # list). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range c \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range c = {}) p s) \<and> (\<forall>tup\<in>set ((cref, oref) # list). descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) ((cref, oref) # list)) \<and> (\<forall>tup\<in>set ((cref, oref) # list). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set ((cref, oref) # list). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set ((cref, oref) # list). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set ((cref, oref) # list). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set ((cref, oref) # list). \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). (\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \<and> distinct (p # map fst ((cref, oref) # list)) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>r s. invs s \<and> Q s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c) p s \<and> (\<forall>tup\<in>set list. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range c \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range c = {}) p s) \<and> (\<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list) \<and> (\<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set list. real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). (\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \<and> distinct (p # map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>r s. invs s \<and> Q s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c) p s \<and> (\<forall>tup\<in>set list. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range c \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range c = {}) p s) \<and> (\<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list) \<and> (\<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set list. real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). (\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \<and> distinct (p # map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace>
 2. \<And>s. invs s \<and> Q s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c) p s \<and> (\<forall>tup\<in>set ((cref, oref) # list). cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range c \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range c = {}) p s) \<and> (\<forall>tup\<in>set ((cref, oref) # list). descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) ((cref, oref) # list)) \<and> (\<forall>tup\<in>set ((cref, oref) # list). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set ((cref, oref) # list). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set ((cref, oref) # list). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set ((cref, oref) # list). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set ((cref, oref) # list). \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). (\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \<and> distinct (p # map fst ((cref, oref) # list)) \<and> tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; Q s; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c) p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p s; \<forall>tup\<in>set list. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range c \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range c = {}) p s; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list); cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p s \<and> ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) p s \<and> (\<forall>x\<in>set list. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {} \<and> cte_wp_at ((\<noteq>) NullCap) p s \<and> valid_mdb s) \<and> (\<forall>x\<in>set list. fst x \<noteq> cref) \<and> (\<forall>x\<in>set list. \<forall>x\<in>obj_refs (default_cap tp (snd x) sz dev). x \<notin> obj_refs (default_cap tp oref sz dev)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; Q s; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c) p s; cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {} \<and> {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) p s; \<forall>tup\<in>set list. cte_wp_at (\<lambda>c. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range c = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) p s; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set list. fst x \<noteq> cref) \<and> (\<forall>x\<in>set list. \<forall>x\<in>obj_refs (default_cap tp (snd x) sz dev). x \<notin> obj_refs (default_cap tp oref sz dev)) \<and> (\<forall>x\<in>set list. cte_wp_at ((\<noteq>) NullCap) p s \<and> cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}) \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) p s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c \<and> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set list. fst x \<noteq> cref) \<and> (\<forall>x\<in>set list. \<forall>x\<in>obj_refs (default_cap tp (snd x) sz dev). x \<notin> obj_refs (default_cap tp oref sz dev)) \<and> (\<forall>x\<in>set list. NullCap \<noteq> cap \<and> cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}) \<and> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (5 subgoals):
 1. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. fst x \<noteq> cref
 2. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>x\<in>obj_refs (default_cap tp (snd x) sz dev). x \<notin> obj_refs (default_cap tp oref sz dev)
 3. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. NullCap \<noteq> cap \<and> cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}
 4. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap
 5. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (5 subgoals):
 1. \<And>s cap a b ba. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> \<Union> {y. \<exists>x\<in>set list. y = cap_range (default_cap tp (snd x) sz dev)} = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) (a, b) s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap (a, b) s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; cap_table_at (length b) a s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> (a, b); \<forall>x\<in>set list. p \<noteq> fst x; \<forall>x\<in>set list. (a, b) \<noteq> fst x; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap; ((a, b), ba) \<in> set list; cref = (a, b)\<rbrakk> \<Longrightarrow> False
 2. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>x\<in>obj_refs (default_cap tp (snd x) sz dev). x \<notin> obj_refs (default_cap tp oref sz dev)
 3. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. NullCap \<noteq> cap \<and> cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}
 4. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap
 5. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (5 subgoals):
 1. \<And>s cap a b ba. \<lbrakk>invs s; Q s; descendants_range (default_cap tp oref sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> \<Union> {y. \<exists>x\<in>set list. y = cap_range (default_cap tp (snd x) sz dev)} = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) (a, b) s; s \<turnstile> default_cap tp oref sz dev; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cap_table_at (length b) a s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> (a, b); distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap; ((a, b), ba) \<in> set list; cref = (a, b); cap_range (default_cap tp (snd ((a, b), ba)) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd ((a, b), ba)) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd ((a, b), ba)..snd ((a, b), ba) + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp (snd ((a, b), ba)) sz dev) p s; cte_wp_at ((=) NullCap) (fst ((a, b), ba)) s; s \<turnstile> default_cap tp (snd ((a, b), ba)) sz dev; ex_cte_cap_wp_to is_cnode_cap (fst ((a, b), ba)) s; real_cte_at (fst ((a, b), ba)) s; \<forall>r\<in>obj_refs (default_cap tp (snd ((a, b), ba)) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> fst ((a, b), ba); (a, b) \<noteq> fst ((a, b), ba)\<rbrakk> \<Longrightarrow> False
 2. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>x\<in>obj_refs (default_cap tp (snd x) sz dev). x \<notin> obj_refs (default_cap tp oref sz dev)
 3. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. NullCap \<noteq> cap \<and> cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}
 4. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap
 5. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>x\<in>obj_refs (default_cap tp (snd x) sz dev). x \<notin> obj_refs (default_cap tp oref sz dev)
 2. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. NullCap \<noteq> cap \<and> cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}
 3. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap
 4. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. NullCap \<noteq> cap \<and> cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}
 2. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap
 3. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>s a b ba r bits f. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> {r..r + 2 ^ bits - 1} \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) = {} \<and> (snd tup \<le> snd tup + 2 ^ obj_bits_api tp us - 1 \<longrightarrow> r \<le> snd tup \<and> snd tup + 2 ^ obj_bits_api tp us - 1 \<le> r + 2 ^ bits - 1); descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> {r..r + 2 ^ bits - 1}; caps_of_state s p = Some (UntypedCap (obj_is_device tp dev) r bits f); untyped_range (default_cap tp oref sz dev) \<inter> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) = {}; oref \<le> oref + 2 ^ obj_bits_api tp us - 1 \<longrightarrow> r \<le> oref \<and> oref + 2 ^ obj_bits_api tp us - 1 \<le> r + 2 ^ bits - 1; ((a, b), ba) \<in> set list\<rbrakk> \<Longrightarrow> cap_range (default_cap tp ba sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}
 2. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap
 3. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>s a b ba r bits f. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> {r..r + 2 ^ bits - 1} \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) = {} \<and> (snd tup \<le> snd tup + 2 ^ obj_bits_api tp us - 1 \<longrightarrow> r \<le> snd tup \<and> snd tup + 2 ^ obj_bits_api tp us - 1 \<le> r + 2 ^ bits - 1); descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; \<forall>tup\<in>set list. cap_range (default_cap tp oref sz dev) \<inter> cap_range (default_cap tp (snd tup) sz dev) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> {r..r + 2 ^ bits - 1}; caps_of_state s p = Some (UntypedCap (obj_is_device tp dev) r bits f); untyped_range (default_cap tp oref sz dev) \<inter> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) = {}; oref \<le> oref + 2 ^ obj_bits_api tp us - 1 \<longrightarrow> r \<le> oref \<and> oref + 2 ^ obj_bits_api tp us - 1 \<le> r + 2 ^ bits - 1; ((a, b), ba) \<in> set list\<rbrakk> \<Longrightarrow> cap_range (default_cap tp ba sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}
 2. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap
 3. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>s a b ba r bits f. \<lbrakk>invs s; Q s; descendants_range (default_cap tp oref sz dev) p s; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; s \<turnstile> default_cap tp oref sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; real_cte_at cref s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> {r..r + 2 ^ bits - 1}; caps_of_state s p = Some (UntypedCap (obj_is_device tp dev) r bits f); untyped_range (default_cap tp oref sz dev) \<inter> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) = {}; oref \<le> oref + 2 ^ obj_bits_api tp us - 1 \<longrightarrow> r \<le> oref \<and> oref + 2 ^ obj_bits_api tp us - 1 \<le> r + 2 ^ bits - 1; ((a, b), ba) \<in> set list; cap_range (default_cap tp (snd ((a, b), ba)) sz dev) \<subseteq> {r..r + 2 ^ bits - 1} \<and> untyped_range (default_cap tp (snd ((a, b), ba)) sz dev) \<inter> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) = {} \<and> (snd ((a, b), ba) \<le> snd ((a, b), ba) + 2 ^ obj_bits_api tp us - 1 \<longrightarrow> r \<le> snd ((a, b), ba) \<and> snd ((a, b), ba) + 2 ^ obj_bits_api tp us - 1 \<le> r + 2 ^ bits - 1); descendants_range (default_cap tp (snd ((a, b), ba)) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> cap_range (default_cap tp (snd ((a, b), ba)) sz dev) = {}; cte_wp_at ((=) NullCap) (fst ((a, b), ba)) s; s \<turnstile> default_cap tp (snd ((a, b), ba)) sz dev; ex_cte_cap_wp_to is_cnode_cap (fst ((a, b), ba)) s; real_cte_at (fst ((a, b), ba)) s; \<forall>r\<in>obj_refs (default_cap tp (snd ((a, b), ba)) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s)\<rbrakk> \<Longrightarrow> cap_range (default_cap tp ba sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}
 2. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap
 3. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>s a b ba r bits f. \<lbrakk>invs s; Q s; descendants_range (default_cap tp oref sz dev) p s; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; s \<turnstile> default_cap tp oref sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; real_cte_at cref s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> {r..r + 2 ^ bits - 1}; caps_of_state s p = Some (UntypedCap (obj_is_device tp dev) r bits f); untyped_range (default_cap tp oref sz dev) \<inter> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) = {}; oref \<le> oref + 2 ^ obj_bits_api tp us - 1 \<longrightarrow> r \<le> oref \<and> oref + 2 ^ obj_bits_api tp us - 1 \<le> r + 2 ^ bits - 1; ((a, b), ba) \<in> set list; descendants_range (default_cap tp ba sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> cap_range (default_cap tp ba sz dev) = {}; cte_wp_at ((=) NullCap) (a, b) s; s \<turnstile> default_cap tp ba sz dev; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cap_table_at (length b) a s; \<forall>r\<in>obj_refs (default_cap tp ba sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); cap_range (default_cap tp ba sz dev) \<subseteq> {r..r + 2 ^ bits - 1}; untyped_range (default_cap tp ba sz dev) \<inter> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) = {}; ba \<le> ba + 2 ^ obj_bits_api tp us - 1 \<longrightarrow> r \<le> ba \<and> ba + 2 ^ obj_bits_api tp us - 1 \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> cap_range (default_cap tp ba sz dev) \<inter> cap_range (default_cap tp oref sz dev) = {}
 2. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap
 3. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap
 2. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>invs s; Q s; \<forall>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev) \<subseteq> untyped_range cap \<and> untyped_range (default_cap tp (snd tup) sz dev) \<inter> usable_untyped_range cap = {} \<and> {snd tup..snd tup + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; descendants_range (default_cap tp oref sz dev) p s; \<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s; cap_range (default_cap tp oref sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {}; distinct_prop (\<lambda>x y. cap_range (default_cap tp (snd x) sz dev) \<inter> cap_range (default_cap tp (snd y) sz dev) = {}) list; cte_wp_at ((=) NullCap) cref s; \<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s; s \<turnstile> default_cap tp oref sz dev; \<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev; ex_cte_cap_wp_to is_cnode_cap cref s; \<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s; real_cte_at cref s; \<forall>tup\<in>set list. real_cte_at (fst tup) s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); \<forall>tup\<in>set list. \<forall>r\<in>obj_refs (default_cap tp (snd tup) sz dev). \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s); p \<noteq> cref; p \<notin> fst ` set list; cref \<notin> fst ` set list; distinct (map fst list); tp \<noteq> ArchObject ASIDPoolObj; cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; caps_of_state s p = Some cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap\<rbrakk> \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal:
No subgoals!