theory Retype_AC

lemma retype_region_pas_refined':
  "\<lbrace>pas_refined aag and pas_cur_domain aag and invs and
    caps_overlap_reserved {ptr..ptr + of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and
    (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda> c. c = (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s \<and>
               (idx \<le> unat (ptr && mask sz) \<or>
                (descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s) \<and>
                pspace_no_overlap_range_cover ptr sz s)) and
    K (sz < word_bits) and
    K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and
    K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) and
    K ((type = CapTableObject \<longrightarrow> 0 < o_bits))\<rbrace>
   retype_region ptr num_objects o_bits type dev
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm)+ apply (rule hoare_weaken_pre) apply (rule use_retype_region_proofs_ext'[where P="invs and pas_refined aag"]) apply clarsimp apply (erule (2) retype_region_proofs'_pas_refined[OF retype_region_proofs'.intro]) apply (wp retype_region_ext_pas_refined) apply simp apply fastforce apply fastforce apply clarsimp apply clarsimp apply (frule valid_cap_range_untyped[OF invs_valid_objs]) apply (fastforce simp: cte_wp_at_caps_of_state) apply (cases slot) apply (auto intro: cte_wp_at_caps_no_overlapI descendants_range_caps_no_overlapI
                     cte_wp_at_pspace_no_overlapI
               simp: cte_wp_at_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s)) and K (sz < word_bits) and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) and K (type = CapTableObject \<longrightarrow> 0 < o_bits)\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s))\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s))) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; retype_region_proofs s type o_bits ptr ?sz11 num_objects dev; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr type num_objects o_bits) then Some (default_object type dev o_bits) else kheap s x\<rparr>)
 2. \<And>xs. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and ?R11 xs\<rbrace> retype_region_ext xs type \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>f xs s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits\<rbrakk> \<Longrightarrow> ?R11 xs (kheap_update f s) = ?R11 xs s
 4. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 5. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s))) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> ?R11 (retype_addrs ptr type num_objects o_bits) s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; retype_region_proofs s type o_bits ptr ?sz11 num_objects dev; invs s; pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr type num_objects o_bits) then Some (default_object type dev o_bits) else kheap s x\<rparr>)
 2. \<And>xs. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and ?R11 xs\<rbrace> retype_region_ext xs type \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>f xs s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits\<rbrakk> \<Longrightarrow> ?R11 xs (kheap_update f s) = ?R11 xs s
 4. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 5. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s))) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> ?R11 (retype_addrs ptr type num_objects o_bits) s proof (prove)
goal (5 subgoals):
 1. \<And>xs. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and ?R11 xs\<rbrace> retype_region_ext xs type \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>f xs s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits\<rbrakk> \<Longrightarrow> ?R11 xs (kheap_update f s) = ?R11 xs s
 3. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 4. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 5. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s))) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> ?R11 (retype_addrs ptr type num_objects o_bits) s proof (prove)
goal (5 subgoals):
 1. \<And>xs s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (pas_refined aag and ?R11 xs) s\<rbrakk> \<Longrightarrow> (pas_refined aag and pas_cur_domain aag and K (\<forall>x\<in>set xs. is_subject aag x)) s
 2. \<And>f xs s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits\<rbrakk> \<Longrightarrow> ?R11 xs (kheap_update f s) = ?R11 xs s
 3. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 4. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 5. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s))) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> ?R11 (retype_addrs ptr type num_objects o_bits) s proof (prove)
goal (4 subgoals):
 1. \<And>f xs s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits\<rbrakk> \<Longrightarrow> (pas_cur_domain aag (kheap_update f s) \<and> (\<forall>x\<in>set xs. is_subject aag x)) = (pas_cur_domain aag s \<and> (\<forall>x\<in>set xs. is_subject aag x))
 2. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 3. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s))) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> pas_cur_domain aag s \<and> (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 2. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s))) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> pas_cur_domain aag s \<and> (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s))) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> pas_cur_domain aag s \<and> (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; (pas_refined aag and pas_cur_domain aag and invs and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and (\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s))) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> pas_cur_domain aag s \<and> (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) proof (prove)
goal (1 subgoal):
 1. \<And>s idx. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; pas_refined aag s; pas_cur_domain aag s; invs s; caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s; cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s; idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) proof (prove)
goal (2 subgoals):
 1. \<And>s idx. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; pas_refined aag s; pas_cur_domain aag s; invs s; caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s; cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s; idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap (?dev50 s idx) (?ptr50 s idx && ~~ mask (?sz50 s idx)) (?sz50 s idx) (?idx50 s idx))) (?slot50 s idx) s
 2. \<And>s idx. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; pas_refined aag s; pas_cur_domain aag s; invs s; caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s; cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s; idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s; cte_wp_at (\<lambda>c. up_aligned_area (?ptr50 s idx) (?sz50 s idx) \<subseteq> cap_range c \<and> cap_is_device c = ?dev50 s idx) (?slot50 s idx) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) proof (prove)
goal (1 subgoal):
 1. \<And>s idx. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; pas_refined aag s; pas_cur_domain aag s; invs s; caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s; cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s; idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) proof (prove)
goal (1 subgoal):
 1. \<And>s idx a b. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; \<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x; range_cover ptr sz (obj_bits_api type o_bits) num_objects; sz < word_bits; pas_refined aag s; pas_cur_domain aag s; invs s; caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s; cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s; idx \<le> unat (ptr && mask sz) \<or> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s \<and> pspace_no_overlap (up_aligned_area ptr sz) s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s; slot = (a, b)\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz11 (obj_bits_api type o_bits) num_objects \<and> caps_no_overlap ptr ?sz11 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz11) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz11 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) proof (prove)
goal:
No subgoals!