theory Untyped_AI

lemma untyped_mdb_descendants_range:
  "\<lbrakk>caps_of_state s p = Some ucap; is_untyped_cap ucap; valid_mdb s; descendants_range_in S p s; S \<subseteq> untyped_range ucap;
   caps_of_state s slot = Some cap; x\<in> obj_refs cap \<rbrakk>\<Longrightarrow> x\<notin> S" apply (clarsimp simp: valid_mdb_def) apply (drule untyped_mdbD) apply simp+ apply (rule ccontr) apply (clarsimp) apply blast apply simp apply (drule(2) descendants_range_inD) apply (simp add: cap_range_def,blast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some ucap; is_untyped_cap ucap; valid_mdb s; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap\<rbrakk> \<Longrightarrow> x \<notin> S proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some ucap; is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S\<rbrakk> \<Longrightarrow> is_untyped_cap ucap
 2. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S\<rbrakk> \<Longrightarrow> caps_of_state s ?ptr'10 = Some ?cap'10
 3. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S\<rbrakk> \<Longrightarrow> obj_refs ?cap'10 \<inter> untyped_range ucap \<noteq> {}
 4. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S\<rbrakk> \<Longrightarrow> untyped_mdb ?m10 (caps_of_state s)
 5. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S; ?ptr'10 \<in> descendants_of p ?m10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> untyped_range ucap \<noteq> {}
 2. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S\<rbrakk> \<Longrightarrow> untyped_mdb ?m10 (caps_of_state s)
 3. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S; slot \<in> descendants_of p ?m10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S; \<not> obj_refs cap \<inter> untyped_range ucap \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S\<rbrakk> \<Longrightarrow> untyped_mdb ?m10 (caps_of_state s)
 3. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S; slot \<in> descendants_of p ?m10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S; obj_refs cap \<inter> untyped_range ucap = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S\<rbrakk> \<Longrightarrow> untyped_mdb ?m10 (caps_of_state s)
 3. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S; slot \<in> descendants_of p ?m10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S\<rbrakk> \<Longrightarrow> untyped_mdb ?m10 (caps_of_state s)
 2. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S; slot \<in> descendants_of p ?m10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap ucap; descendants_range_in S p s; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S; slot \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap ucap; S \<subseteq> untyped_range ucap; caps_of_state s slot = Some cap; x \<in> obj_refs cap; 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); x \<in> S; slot \<in> descendants_of p (cdt s); cap_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!