theory Untyped_AI

lemma (in Untyped_AI_nonempty_table) create_cap_invs[wp]:
  "\<lbrace>invs
      and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_is_device (default_cap tp oref sz dev)  = cap_is_device c
                         \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and>
                         untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range c
                         \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p
      and descendants_range (default_cap tp oref sz dev) p
      and cte_wp_at ((=) cap.NullCap) cref
      and valid_cap (default_cap tp oref sz dev)
      and ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref
      and real_cte_at cref
      and (\<lambda>(s::'state_ext state). \<forall>r\<in>obj_refs (default_cap tp oref 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 K (p \<noteq> cref \<and> tp \<noteq> ArchObject ASIDPoolObj)\<rbrace>
     create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. invs\<rbrace>" apply (rule hoare_pre) apply (simp add: invs_def valid_state_def valid_pspace_def) apply (wp create_cap_refs_respects_device | simp add: valid_cap_def)+ apply clarsimp apply (clarsimp simp: cte_wp_at_caps_of_state valid_pspace_def) apply (frule_tac p1 = p in valid_cap_aligned[OF caps_of_state_valid]) apply simp apply (simp add: invs_def valid_state_def valid_pspace_def ) apply (simp add: cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_is_device (default_cap tp oref sz dev) = cap_is_device c \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p and descendants_range (default_cap tp oref sz dev) p and cte_wp_at ((=) NullCap) cref and valid_cap (default_cap tp oref sz dev) and ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref and real_cte_at cref and (\<lambda>s. \<forall>r\<in>obj_refs (default_cap tp oref 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 K (p \<noteq> cref \<and> tp \<noteq> ArchObject ASIDPoolObj)\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. (invs and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_is_device (default_cap tp oref sz dev) = cap_is_device c \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p and descendants_range (default_cap tp oref sz dev) p and cte_wp_at ((=) NullCap) cref and valid_cap (default_cap tp oref sz dev) and ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref and real_cte_at cref and (\<lambda>s. \<forall>r\<in>obj_refs (default_cap tp oref 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 K (p \<noteq> cref \<and> tp \<noteq> ArchObject ASIDPoolObj)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace>
 2. \<And>s. (invs and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_is_device (default_cap tp oref sz dev) = cap_is_device c \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p and descendants_range (default_cap tp oref sz dev) p and cte_wp_at ((=) NullCap) cref and valid_cap (default_cap tp oref sz dev) and ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref and real_cte_at cref and (\<lambda>s. \<forall>r\<in>obj_refs (default_cap tp oref 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 K (p \<noteq> cref \<and> tp \<noteq> ArchObject ASIDPoolObj)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p s \<and> descendants_range (default_cap tp oref sz dev) p s \<and> cte_wp_at ((=) NullCap) cref s \<and> cap_aligned (default_cap tp oref sz dev) \<and> (case default_cap tp oref sz dev of UntypedCap deva p b f \<Rightarrow> valid_untyped (default_cap tp oref sz dev) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True) \<and> ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref s \<and> real_cte_at cref s \<and> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \<and> p \<noteq> cref \<and> tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> cte_wp_at (\<lambda>_. True) cref s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cte_wp_at (\<lambda>c. obj_is_device tp dev = cap_is_device c \<and> is_untyped_cap c \<and> cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p s \<and> cur_tcb s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_is_device tp dev = cap_is_device c \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p s; descendants_range (default_cap tp oref sz dev) p s; cte_wp_at ((=) NullCap) cref s; cap_aligned (default_cap tp oref sz dev); case default_cap tp oref sz dev of UntypedCap deva p b f \<Rightarrow> valid_untyped (default_cap tp oref sz dev) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref s; real_cte_at cref s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; p \<noteq> cref; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_objs s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range c \<and> untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range c = {}) p s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> cte_wp_at (\<lambda>_. True) cref s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cte_wp_at (\<lambda>c. obj_is_device tp dev = cap_is_device c \<and> is_untyped_cap c \<and> cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p s \<and> cur_tcb s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>invs s; descendants_range (default_cap tp oref sz dev) p s; caps_of_state s cref = Some NullCap; cap_aligned (default_cap tp oref sz dev); case default_cap tp oref sz dev of UntypedCap deva p b f \<Rightarrow> valid_untyped (default_cap tp oref sz dev) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref s; real_cte_at cref s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; p \<noteq> cref; tp \<noteq> ArchObject ASIDPoolObj; caps_of_state s p = Some cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap; obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap; untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap \<and> cur_tcb s proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>invs s; descendants_range (default_cap tp oref sz dev) p s; caps_of_state s cref = Some NullCap; cap_aligned (default_cap tp oref sz dev); case default_cap tp oref sz dev of UntypedCap deva p b f \<Rightarrow> valid_untyped (default_cap tp oref sz dev) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref s; real_cte_at cref s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; p \<noteq> cref; tp \<noteq> ArchObject ASIDPoolObj; caps_of_state s p = Some cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap; obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap; untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> caps_of_state s p = Some (?cap120 s cap)
 2. \<And>s cap. \<lbrakk>invs s; descendants_range (default_cap tp oref sz dev) p s; caps_of_state s cref = Some NullCap; cap_aligned (default_cap tp oref sz dev); case default_cap tp oref sz dev of UntypedCap deva p b f \<Rightarrow> valid_untyped (default_cap tp oref sz dev) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref s; real_cte_at cref s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; p \<noteq> cref; tp \<noteq> ArchObject ASIDPoolObj; caps_of_state s p = Some cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap; obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap; untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; cap_aligned (?cap120 s cap)\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap \<and> cur_tcb s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>invs s; descendants_range (default_cap tp oref sz dev) p s; caps_of_state s cref = Some NullCap; cap_aligned (default_cap tp oref sz dev); case default_cap tp oref sz dev of UntypedCap deva p b f \<Rightarrow> valid_untyped (default_cap tp oref sz dev) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref s; real_cte_at cref s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; p \<noteq> cref; tp \<noteq> ArchObject ASIDPoolObj; caps_of_state s p = Some cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap; obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap; untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; cap_aligned cap\<rbrakk> \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_objs s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap \<and> cur_tcb s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s; descendants_range (default_cap tp oref sz dev) p s; caps_of_state s cref = Some NullCap; cap_aligned (default_cap tp oref sz dev); case default_cap tp oref sz dev of UntypedCap deva p b f \<Rightarrow> valid_untyped (default_cap tp oref sz dev) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True; ex_cte_cap_wp_to (appropriate_cte_cap (default_cap tp oref sz dev)) cref s; real_cte_at cref s; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; p \<noteq> cref; tp \<noteq> ArchObject ASIDPoolObj; caps_of_state s p = Some cap; is_untyped_cap cap; obj_is_device tp dev = cap_is_device cap; obj_refs (default_cap tp oref sz dev) \<subseteq> untyped_range cap; untyped_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap; untyped_range (default_cap tp oref sz dev) \<inter> usable_untyped_range cap = {}; cap_aligned cap\<rbrakk> \<Longrightarrow> cap_range (default_cap tp oref sz dev) \<subseteq> untyped_range cap proof (prove)
goal:
No subgoals!