theory Untyped_AI

lemma cte_wp_at_caps_no_overlapI:
  "\<lbrakk> invs s;cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s;
  idx \<le> unat (ptr && mask sz);sz < word_bits \<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s" apply (frule invs_mdb) apply (frule(1) le_mask_le_2p) apply (clarsimp simp: valid_mdb_def cte_wp_at_caps_of_state) apply (frule caps_of_state_valid_cap) apply (simp add: invs_valid_objs) apply (unfold caps_no_overlap_def) apply (intro ballI impI) apply (erule ranE) apply (subgoal_tac "is_untyped_cap cap") prefer 2 apply (rule untyped_range_is_untyped_cap) apply blast apply (drule untyped_incD) apply simp+ apply (elim conjE) apply (erule subset_splitE) apply (erule subset_trans[OF _ psubset_imp_subset,rotated]) apply (clarsimp simp: word_and_le2) apply simp apply (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (elim conjE) apply (drule disjoint_subset2[rotated,
       where B' = "{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}"]) apply clarsimp apply (rule le_plus'[OF word_and_le2]) apply simp apply (erule word_of_nat_le) apply simp apply simp apply (erule subset_trans[OF _  equalityD1,rotated]) apply (clarsimp simp: word_and_le2) apply (thin_tac "P\<longrightarrow>Q" for P Q)+ apply (drule disjoint_subset[rotated,
       where A' = "{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}"]) apply (clarsimp simp: word_and_le2 Int_ac)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; idx \<le> unat (ptr && mask sz); sz < word_bits\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx\<rbrakk> \<Longrightarrow> \<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; cap \<in> ran (caps_of_state s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> is_untyped_cap cap
 2. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap\<rbrakk> \<Longrightarrow> untyped_range cap \<noteq> {}
 2. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (5 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> caps_of_state s (?p'35 cap x) = Some (?c'35 cap x)
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> is_untyped_cap (?c'35 cap x)
 4. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> untyped_inc (?m35 cap x) (caps_of_state s)
 5. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<subseteq> untyped_range (?c'35 cap x) \<or> untyped_range (?c'35 cap x) \<subseteq> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<or> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> untyped_range (?c'35 cap x) = {}) \<and> (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<subset> untyped_range (?c'35 cap x) \<longrightarrow> cref \<in> descendants_of (?p'35 cap x) (?m35 cap x) \<and> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> usable_untyped_range (?c'35 cap x) = {}) \<and> (untyped_range (?c'35 cap x) \<subset> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<longrightarrow> ?p'35 cap x \<in> descendants_of cref (?m35 cap x) \<and> untyped_range (?c'35 cap x) \<inter> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = {}) \<and> (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = untyped_range (?c'35 cap x) \<longrightarrow> ?p'35 cap x \<in> descendants_of cref (?m35 cap x) \<and> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = {} \<or> cref \<in> descendants_of (?p'35 cap x) (?m35 cap x) \<and> usable_untyped_range (?c'35 cap x) = {} \<or> cref = ?p'35 cap x)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; ({ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap \<or> untyped_range cap \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<or> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}) \<and> ({ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}) \<and> (untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \<and> ({ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap \<or> untyped_range cap \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<or> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 4. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 4. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s); x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> ptr + word_of_nat idx \<le> ptr + 2 ^ sz - 1 \<longrightarrow> usable_untyped_range cap = {} \<or> cref = x; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of cref (cdt s); untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of cref (cdt s)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of cref (cdt s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 4. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<And>cap a b x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s (a, b) = Some cap; is_untyped_cap cap; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<notin> untyped_range cap; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr && ~~ mask sz \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + word_of_nat idx \<le> ptr
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of cref (cdt s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 4. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<And>cap a b x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s (a, b) = Some cap; is_untyped_cap cap; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<notin> untyped_range cap; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr && ~~ mask sz \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr - (ptr && ~~ mask sz)
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of cref (cdt s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 4. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (4 subgoals):
 1. \<And>cap a b x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s (a, b) = Some cap; is_untyped_cap cap; (a, b) \<in> descendants_of cref (cdt s); untyped_range cap \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<notin> untyped_range cap; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr && ~~ mask sz \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr && mask sz
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of cref (cdt s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 4. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> descendants_of cref (cdt s); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 3. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subset> untyped_range cap \<longrightarrow> cref \<in> descendants_of x (cdt s) \<and> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> usable_untyped_range cap = {}; untyped_range cap \<subset> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> untyped_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = untyped_range cap \<longrightarrow> x \<in> descendants_of cref (cdt s) \<and> \<not> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 \<or> cref \<in> descendants_of x (cdt s) \<and> usable_untyped_range cap = {} \<or> cref = x; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>cap x. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; idx < 2 ^ sz; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; caps_of_state s x = Some cap; is_untyped_cap cap; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal:
No subgoals!