theory Untyped_AI

lemma ex_nonz_cap_to_overlap:
  "\<lbrakk>ex_nonz_cap_to t s; cte_wp_at ((=) cap) p s; is_untyped_cap cap; invs s;
    descendants_range cap p s \<rbrakk>
   \<Longrightarrow> \<not> t \<in> untyped_range cap" apply (rule ccontr) apply (clarsimp simp: ex_nonz_cap_to_def descendants_range_def2
     cte_wp_at_caps_of_state caps_no_overlap_def zobj_refs_to_obj_refs) apply (frule invs_mdb) apply (clarsimp simp: valid_mdb_def) apply (frule_tac cap' = capa in untyped_mdbD) apply simp+ apply blast apply simp apply (drule(2) descendants_range_inD) apply (simp add: cap_range_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_nonz_cap_to t s; cte_wp_at ((=) cap) p s; is_untyped_cap cap; invs s; descendants_range cap p s\<rbrakk> \<Longrightarrow> t \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_nonz_cap_to t s; cte_wp_at ((=) cap) p s; is_untyped_cap cap; invs s; descendants_range cap p s; \<not> t \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; valid_mdb s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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> False proof (prove)
goal (5 subgoals):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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> is_untyped_cap cap
 2. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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_of_state s (?ptr'18 a b capa) = Some capa
 3. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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> obj_refs capa \<inter> untyped_range cap \<noteq> {}
 4. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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> untyped_mdb (?m18 a b capa) (caps_of_state s)
 5. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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); ?ptr'18 a b capa \<in> descendants_of p (?m18 a b capa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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> obj_refs capa \<inter> untyped_range cap \<noteq> {}
 2. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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> untyped_mdb (?m18 a b capa) (caps_of_state s)
 3. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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); (a, b) \<in> descendants_of p (?m18 a b capa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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> untyped_mdb (?m18 a b capa) (caps_of_state s)
 2. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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); (a, b) \<in> descendants_of p (?m18 a b capa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; descendants_range_in (untyped_range cap) p s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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); (a, b) \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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); (a, b) \<in> descendants_of p (cdt s); cap_range capa \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_untyped_cap cap; invs s; t \<in> untyped_range cap; caps_of_state s (a, b) = Some capa; t \<in> obj_refs capa; \<not> is_zombie capa; 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); (a, b) \<in> descendants_of p (cdt s); (untyped_range capa \<union> obj_refs capa) \<inter> untyped_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!