theory Untyped_AI

lemma (in Untyped_AI_nonempty_table) create_caps_invs:
  assumes create_cap_Q[wp]: "\<And>cref oref.
    \<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)
        and K (cref \<in> set crefs \<and> oref \<in> set (retype_addrs ptr tp (length slots) us))\<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::('state_ext::state_ext) state \<Rightarrow> bool) 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 (zip crefs orefs).
           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 (zip crefs orefs).
           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)) (zip crefs orefs))
       \<and> (\<forall>tup \<in> set (zip crefs orefs).
           cte_wp_at ((=) cap.NullCap) (fst tup) s)
       \<and> (\<forall>tup \<in> set (zip crefs orefs).
              valid_cap (default_cap tp (snd tup) sz dev) s)
       \<and> (\<forall>tup \<in> set (zip crefs orefs).
              ex_cte_cap_wp_to is_cnode_cap (fst tup) s)
       \<and> (\<forall>tup \<in> set (zip crefs orefs).
              real_cte_at (fst tup) s)
       \<and> (\<forall>tup \<in> set (zip crefs orefs). \<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 (zip crefs orefs)))
       \<and> tp \<noteq> ArchObject ASIDPoolObj)
       and K (set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us))\<rbrace>
     mapM_x (create_cap tp sz p dev) (zip crefs orefs)
   \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>" apply (rule hoare_gen_asm) apply (subgoal_tac "set (zip crefs orefs) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)") prefer 2 apply (auto dest!: set_zip_helper)[1] apply (induct ("zip crefs orefs")) apply (simp add: mapM_x_def sequence_x_def) apply wpsimp apply (clarsimp simp add: mapM_x_def sequence_x_def) apply (rule hoare_seq_ext) apply assumption apply (thin_tac "valid a b c" for a b c) apply (rule hoare_pre) apply (rule hoare_strengthen_post) apply (rule_tac list=list and us=us in create_caps_invs_inv) apply (rule hoare_pre, rule create_cap_Q) apply (clarsimp | drule(1) bspec)+ 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 (zip crefs orefs). 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 (zip crefs orefs). 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)) (zip crefs orefs)) \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set (zip crefs orefs). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). \<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 (zip crefs orefs)) \<and> tp \<noteq> ArchObject ASIDPoolObj) and K (set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us))\<rbrace> mapM_x (create_cap tp sz p dev) (zip crefs orefs) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us) \<Longrightarrow> \<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 (zip crefs orefs). 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 (zip crefs orefs). 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)) (zip crefs orefs)) \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set (zip crefs orefs). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). \<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 (zip crefs orefs)) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> mapM_x (create_cap tp sz p dev) (zip crefs orefs) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set (zip crefs orefs) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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 (zip crefs orefs). 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 (zip crefs orefs). 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)) (zip crefs orefs)) \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set (zip crefs orefs). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). \<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 (zip crefs orefs)) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> mapM_x (create_cap tp sz p dev) (zip crefs orefs) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 2. set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us) \<Longrightarrow> set (zip crefs orefs) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us) proof (prove)
goal (2 subgoals):
 1. set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us) \<Longrightarrow> set (zip crefs orefs) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)
 2. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set (zip crefs orefs) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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 (zip crefs orefs). 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 (zip crefs orefs). 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)) (zip crefs orefs)) \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set (zip crefs orefs). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). \<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 (zip crefs orefs)) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> mapM_x (create_cap tp sz p dev) (zip crefs orefs) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set (zip crefs orefs) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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 (zip crefs orefs). 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 (zip crefs orefs). 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)) (zip crefs orefs)) \<and> (\<forall>tup\<in>set (zip crefs orefs). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set (zip crefs orefs). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (zip crefs orefs). \<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 (zip crefs orefs)) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> mapM_x (create_cap tp sz p dev) (zip crefs orefs) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set [] \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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 []. 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 []. 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)) []) \<and> (\<forall>tup\<in>set []. cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set []. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set []. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set []. real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set []. \<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 []) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> mapM_x (create_cap tp sz p dev) [] \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 2. \<And>a list. \<lbrakk>\<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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 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> mapM_x (create_cap tp sz p dev) list \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>; set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set (a # list) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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 (a # 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 (a # 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)) (a # list)) \<and> (\<forall>tup\<in>set (a # list). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set (a # list). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set (a # list). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set (a # list). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (a # 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 (a # list)) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> mapM_x (create_cap tp sz p dev) (a # list) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us) \<Longrightarrow> \<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> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> return () \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 2. \<And>a list. \<lbrakk>\<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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 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> mapM_x (create_cap tp sz p dev) list \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>; set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set (a # list) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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 (a # 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 (a # 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)) (a # list)) \<and> (\<forall>tup\<in>set (a # list). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set (a # list). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set (a # list). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set (a # list). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (a # 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 (a # list)) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> mapM_x (create_cap tp sz p dev) (a # list) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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 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> mapM_x (create_cap tp sz p dev) list \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>; set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set (a # list) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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 (a # 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 (a # 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)) (a # list)) \<and> (\<forall>tup\<in>set (a # list). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set (a # list). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set (a # list). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set (a # list). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (a # 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 (a # list)) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> mapM_x (create_cap tp sz p dev) (a # list) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b ba list. \<lbrakk>\<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 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>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) \<and> p \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map (create_cap tp sz p dev) list) (return ()) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>; set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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> cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz dev) \<inter> usable_untyped_range 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> descendants_range (default_cap tp ba sz dev) p s \<and> (\<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> cap_range (default_cap tp ba sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {} \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list) \<and> cte_wp_at ((=) NullCap) (a, b) s \<and> (\<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s) \<and> s \<turnstile> default_cap tp ba sz dev \<and> (\<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> cap_table_at (length b) a s \<and> (\<forall>tup\<in>set list. real_cte_at (fst tup) s) \<and> (\<forall>r\<in>obj_refs (default_cap tp ba 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) \<and> (\<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) \<and> p \<noteq> (a, b) \<and> p \<notin> fst ` set list \<and> (a, b) \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> do _ <- create_cap tp sz p dev ((a, b), ba);
foldr (\<lambda>x y. do _ <- x;
y
od) (map (create_cap tp sz p dev) list) (return ())
od \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b ba list uu_. \<lbrakk>\<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 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>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) \<and> p \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map (create_cap tp sz p dev) list) (return ()) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>; set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<lbrace>?B20 a b ba list uu_\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map (create_cap tp sz p dev) list) (return ()) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>
 2. \<And>a b ba list. \<lbrakk>\<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 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>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) \<and> p \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map (create_cap tp sz p dev) list) (return ()) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>; set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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> cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz dev) \<inter> usable_untyped_range 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> descendants_range (default_cap tp ba sz dev) p s \<and> (\<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> cap_range (default_cap tp ba sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {} \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list) \<and> cte_wp_at ((=) NullCap) (a, b) s \<and> (\<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s) \<and> s \<turnstile> default_cap tp ba sz dev \<and> (\<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> cap_table_at (length b) a s \<and> (\<forall>tup\<in>set list. real_cte_at (fst tup) s) \<and> (\<forall>r\<in>obj_refs (default_cap tp ba 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) \<and> (\<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) \<and> p \<noteq> (a, b) \<and> p \<notin> fst ` set list \<and> (a, b) \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> create_cap tp sz p dev ((a, b), ba) \<lbrace>?B20 a b ba list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b ba list. \<lbrakk>\<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 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>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) \<and> p \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> foldr (\<lambda>x y. do _ <- x;
y
od) (map (create_cap tp sz p dev) list) (return ()) \<lbrace>\<lambda>rv s. invs s \<and> Q s\<rbrace>; set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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> cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz dev) \<inter> usable_untyped_range 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> descendants_range (default_cap tp ba sz dev) p s \<and> (\<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> cap_range (default_cap tp ba sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {} \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list) \<and> cte_wp_at ((=) NullCap) (a, b) s \<and> (\<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s) \<and> s \<turnstile> default_cap tp ba sz dev \<and> (\<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> cap_table_at (length b) a s \<and> (\<forall>tup\<in>set list. real_cte_at (fst tup) s) \<and> (\<forall>r\<in>obj_refs (default_cap tp ba 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) \<and> (\<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) \<and> p \<noteq> (a, b) \<and> p \<notin> fst ` set list \<and> (a, b) \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> create_cap tp sz p dev ((a, b), ba) \<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 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>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) \<and> p \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b ba list. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<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> cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz dev) \<inter> usable_untyped_range 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> descendants_range (default_cap tp ba sz dev) p s \<and> (\<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> cap_range (default_cap tp ba sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {} \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list) \<and> cte_wp_at ((=) NullCap) (a, b) s \<and> (\<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s) \<and> s \<turnstile> default_cap tp ba sz dev \<and> (\<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> cap_table_at (length b) a s \<and> (\<forall>tup\<in>set list. real_cte_at (fst tup) s) \<and> (\<forall>r\<in>obj_refs (default_cap tp ba 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) \<and> (\<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) \<and> p \<noteq> (a, b) \<and> p \<notin> fst ` set list \<and> (a, b) \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> create_cap tp sz p dev ((a, b), ba) \<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 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>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) \<and> p \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b ba list. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 a b ba list\<rbrace> create_cap tp sz p dev ((a, b), ba) \<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 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>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) \<and> p \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrace>
 2. \<And>a b ba list s. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us); 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> cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz dev) \<inter> usable_untyped_range 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> descendants_range (default_cap tp ba sz dev) p s \<and> (\<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> cap_range (default_cap tp ba sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {} \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list) \<and> cte_wp_at ((=) NullCap) (a, b) s \<and> (\<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s) \<and> s \<turnstile> default_cap tp ba sz dev \<and> (\<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> cap_table_at (length b) a s \<and> (\<forall>tup\<in>set list. real_cte_at (fst tup) s) \<and> (\<forall>r\<in>obj_refs (default_cap tp ba 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) \<and> (\<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) \<and> p \<noteq> (a, b) \<and> p \<notin> fst ` set list \<and> (a, b) \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> ?Q28 a b ba list s proof (prove)
goal (3 subgoals):
 1. \<And>a b ba list. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<lbrace>?Q28 a b ba list\<rbrace> create_cap tp sz p dev ((a, b), ba) \<lbrace>?Q31 a b ba list\<rbrace>
 2. \<And>a b ba list rv s. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us); ?Q31 a b ba list rv s\<rbrakk> \<Longrightarrow> 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>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) \<and> p \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj
 3. \<And>a b ba list s. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us); 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> cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz dev) \<inter> usable_untyped_range 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> descendants_range (default_cap tp ba sz dev) p s \<and> (\<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> cap_range (default_cap tp ba sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {} \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list) \<and> cte_wp_at ((=) NullCap) (a, b) s \<and> (\<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s) \<and> s \<turnstile> default_cap tp ba sz dev \<and> (\<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> cap_table_at (length b) a s \<and> (\<forall>tup\<in>set list. real_cte_at (fst tup) s) \<and> (\<forall>r\<in>obj_refs (default_cap tp ba 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) \<and> (\<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) \<and> p \<noteq> (a, b) \<and> p \<notin> fst ` set list \<and> (a, b) \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> ?Q28 a b ba list s proof (prove)
goal (3 subgoals):
 1. \<And>a b ba list. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us)\<rbrakk> \<Longrightarrow> \<lbrace>invs and ?Q34 a b ba list and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) p and cte_wp_at ((=) NullCap) (a, b) and valid_cap (default_cap tp ba sz dev)\<rbrace> create_cap tp sz p dev ((a, b), ba) \<lbrace>\<lambda>_. ?Q34 a b ba list\<rbrace>
 2. \<And>a b ba list rv s. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us); invs s \<and> ?Q34 a b ba list 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\<rbrakk> \<Longrightarrow> 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>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) \<and> p \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj
 3. \<And>a b ba list s. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us); 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> cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz dev) \<inter> usable_untyped_range 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> descendants_range (default_cap tp ba sz dev) p s \<and> (\<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> cap_range (default_cap tp ba sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {} \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list) \<and> cte_wp_at ((=) NullCap) (a, b) s \<and> (\<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s) \<and> s \<turnstile> default_cap tp ba sz dev \<and> (\<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> cap_table_at (length b) a s \<and> (\<forall>tup\<in>set list. real_cte_at (fst tup) s) \<and> (\<forall>r\<in>obj_refs (default_cap tp ba 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) \<and> (\<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) \<and> p \<noteq> (a, b) \<and> p \<notin> fst ` set list \<and> (a, b) \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> invs s \<and> ?Q34 a b ba list 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 (((a, b), ba) # 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 (((a, b), ba) # 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)) (((a, b), ba) # list)) \<and> (\<forall>tup\<in>set (((a, b), ba) # list). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set (((a, b), ba) # list). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set (((a, b), ba) # list). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set (((a, b), ba) # list). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (((a, b), ba) # 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 (((a, b), ba) # list)) \<and> tp \<noteq> ArchObject ASIDPoolObj proof (prove)
goal (3 subgoals):
 1. \<And>a b ba list s. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us); (invs and Q and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) p and cte_wp_at ((=) NullCap) (a, b) and valid_cap (default_cap tp ba sz dev)) s\<rbrakk> \<Longrightarrow> (invs and Q and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) p and cte_wp_at ((=) NullCap) (a, b) and valid_cap (default_cap tp ba sz dev) and K ((a, b) \<in> set crefs \<and> ba \<in> set (retype_addrs ptr tp (length slots) us))) s
 2. \<And>a b ba list rv s. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us); 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\<rbrakk> \<Longrightarrow> 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>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) \<and> p \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj
 3. \<And>a b ba list s. \<lbrakk>set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us); set list \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us); (a, b) \<in> set crefs; ba \<in> set (retype_addrs ptr tp (length slots) us); 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> cte_wp_at (\<lambda>c. cap_range (default_cap tp ba sz dev) \<subseteq> untyped_range c \<and> {ba..ba + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c \<and> untyped_range (default_cap tp ba sz dev) \<inter> usable_untyped_range 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> descendants_range (default_cap tp ba sz dev) p s \<and> (\<forall>tup\<in>set list. descendants_range (default_cap tp (snd tup) sz dev) p s) \<and> cap_range (default_cap tp ba sz dev) \<inter> (\<Union>tup\<in>set list. cap_range (default_cap tp (snd tup) sz dev)) = {} \<and> distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) sz dev)) list) \<and> cte_wp_at ((=) NullCap) (a, b) s \<and> (\<forall>tup\<in>set list. cte_wp_at ((=) NullCap) (fst tup) s) \<and> s \<turnstile> default_cap tp ba sz dev \<and> (\<forall>tup\<in>set list. s \<turnstile> default_cap tp (snd tup) sz dev) \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (\<forall>tup\<in>set list. ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> cap_table_at (length b) a s \<and> (\<forall>tup\<in>set list. real_cte_at (fst tup) s) \<and> (\<forall>r\<in>obj_refs (default_cap tp ba 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) \<and> (\<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) \<and> p \<noteq> (a, b) \<and> p \<notin> fst ` set list \<and> (a, b) \<notin> fst ` set list \<and> distinct (map fst list) \<and> tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> 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 (((a, b), ba) # 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 (((a, b), ba) # 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)) (((a, b), ba) # list)) \<and> (\<forall>tup\<in>set (((a, b), ba) # list). cte_wp_at ((=) NullCap) (fst tup) s) \<and> (\<forall>tup\<in>set (((a, b), ba) # list). s \<turnstile> default_cap tp (snd tup) sz dev) \<and> (\<forall>tup\<in>set (((a, b), ba) # list). ex_cte_cap_wp_to is_cnode_cap (fst tup) s) \<and> (\<forall>tup\<in>set (((a, b), ba) # list). real_cte_at (fst tup) s) \<and> (\<forall>tup\<in>set (((a, b), ba) # 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 (((a, b), ba) # list)) \<and> tp \<noteq> ArchObject ASIDPoolObj proof (prove)
goal:
No subgoals!