theory Untyped_R

lemma next_wont_bite:
  "\<lbrakk> mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some cte \<rbrakk>
  \<Longrightarrow> \<not> sameRegionAs c' (cteCap cte)" using range ut_rev apply (cases cte) apply clarsimp apply (cases "m \<turnstile> parent \<rightarrow> mdbNext parent_node") apply (drule (2) descendants_rangeD') apply (drule capRange_sameRegionAs) apply (erule valid_capI') apply (simp add: phys) apply blast apply (erule notE, rule direct_parent) apply (clarsimp simp: mdb_next_unfold parent) apply assumption apply (simp add: parentOf_def parent) apply (insert is_untyped same_region) apply (clarsimp simp: isMDBParentOf_CTE) apply (rule conjI) apply (erule (1) sameRegionAs_trans) apply (simp add: ut_revocable'_def) apply (insert parent) apply simp apply (clarsimp simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some cte\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c' (cteCap cte) proof (prove)
using this:
descendants_range' c' parent m
ut_revocable' m

goal (1 subgoal):
 1. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some cte\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c' (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some cte; descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c' (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; m \<turnstile> parent \<rightarrow> mdbNext parent_node\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; \<not> m \<turnstile> parent \<rightarrow> mdbNext parent_node\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; m \<turnstile> parent \<rightarrow> mdbNext parent_node; capRange x1 \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; \<not> m \<turnstile> parent \<rightarrow> mdbNext parent_node\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); ut_revocable' m; cte = CTE x1 x2; m \<turnstile> parent \<rightarrow> mdbNext parent_node; capRange x1 \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> valid_cap' x1 (?s9 x1 x2)
 2. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); ut_revocable' m; cte = CTE x1 x2; m \<turnstile> parent \<rightarrow> mdbNext parent_node; capRange x1 \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> capClass c' = PhysicalClass \<or> capClass x1 = PhysicalClass
 3. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); ut_revocable' m; cte = CTE x1 x2; m \<turnstile> parent \<rightarrow> mdbNext parent_node; capRange x1 \<inter> capRange c' = {}; capRange c' \<inter> capRange x1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; \<not> m \<turnstile> parent \<rightarrow> mdbNext parent_node\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); ut_revocable' m; cte = CTE x1 x2; m \<turnstile> parent \<rightarrow> mdbNext parent_node; capRange x1 \<inter> capRange c' = {}\<rbrakk> \<Longrightarrow> capClass c' = PhysicalClass \<or> capClass x1 = PhysicalClass
 2. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); ut_revocable' m; cte = CTE x1 x2; m \<turnstile> parent \<rightarrow> mdbNext parent_node; capRange x1 \<inter> capRange c' = {}; capRange c' \<inter> capRange x1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; \<not> m \<turnstile> parent \<rightarrow> mdbNext parent_node\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); ut_revocable' m; cte = CTE x1 x2; m \<turnstile> parent \<rightarrow> mdbNext parent_node; capRange x1 \<inter> capRange c' = {}; capRange c' \<inter> capRange x1 \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; \<not> m \<turnstile> parent \<rightarrow> mdbNext parent_node\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; \<not> m \<turnstile> parent \<rightarrow> mdbNext parent_node\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto> mdbNext parent_node
 2. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0
 3. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1\<rbrakk> \<Longrightarrow> m \<turnstile> parent parentOf mdbNext parent_node proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0
 2. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1\<rbrakk> \<Longrightarrow> m \<turnstile> parent parentOf mdbNext parent_node proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1\<rbrakk> \<Longrightarrow> m \<turnstile> parent parentOf mdbNext parent_node proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE parent_cap parent_node) (CTE x1 x2) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; isUntypedCap parent_cap; global.sameRegionAs parent_cap c'\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE parent_cap parent_node) (CTE x1 x2) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; isUntypedCap parent_cap; global.sameRegionAs parent_cap c'\<rbrakk> \<Longrightarrow> global.sameRegionAs parent_cap x1 \<and> mdbRevocable parent_node \<and> (capBadge parent_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; isUntypedCap parent_cap; global.sameRegionAs parent_cap c'\<rbrakk> \<Longrightarrow> global.sameRegionAs parent_cap x1
 2. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; isUntypedCap parent_cap; global.sameRegionAs parent_cap c'\<rbrakk> \<Longrightarrow> mdbRevocable parent_node \<and> (capBadge parent_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; ut_revocable' m; cte = CTE x1 x2; global.sameRegionAs c' x1; isUntypedCap parent_cap; global.sameRegionAs parent_cap c'\<rbrakk> \<Longrightarrow> mdbRevocable parent_node \<and> (capBadge parent_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; \<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; cte = CTE x1 x2; global.sameRegionAs c' x1; isUntypedCap parent_cap; global.sameRegionAs parent_cap c'\<rbrakk> \<Longrightarrow> mdbRevocable parent_node \<and> (capBadge parent_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; \<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; cte = CTE x1 x2; global.sameRegionAs c' x1; isUntypedCap parent_cap; global.sameRegionAs parent_cap c'; m parent = Some (CTE parent_cap parent_node)\<rbrakk> \<Longrightarrow> mdbRevocable parent_node \<and> (capBadge parent_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>mdbNext parent_node \<noteq> 0; m (mdbNext parent_node) = Some (CTE x1 x2); descendants_range' c' parent m; \<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; cte = CTE x1 x2; global.sameRegionAs c' x1; isUntypedCap parent_cap; global.sameRegionAs parent_cap c'; m parent = Some (CTE parent_cap parent_node)\<rbrakk> \<Longrightarrow> (capBadge parent_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2) proof (prove)
goal:
No subgoals!