theory Arch_R

lemma safe_parent_strg':
  "cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap False frame pageBits idx) p s \<and>
   descendants_of' p (ctes_of s) = {} \<and>
   valid_pspace' s
  \<longrightarrow> safe_parent_for' (ctes_of s) p (ArchObjectCap (ASIDPoolCap frame base))" apply (clarsimp simp: safe_parent_for'_def cte_wp_at_ctes_of) apply (case_tac cte) apply (simp add: isCap_simps) apply (subst conj_comms) apply (rule context_conjI) apply (drule ctes_of_valid_cap', fastforce) apply (clarsimp simp: valid_cap'_def capAligned_def) apply (drule is_aligned_no_overflow) apply (clarsimp simp: capRange_def asid_low_bits_def pageBits_def) apply (clarsimp simp: sameRegionAs_def2 isCap_simps capRange_def asid_low_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap False frame pageBits idx) p s \<and> descendants_of' p (ctes_of s) = {} \<and> valid_pspace' s \<longrightarrow> safe_parent_for' (ctes_of s) p (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap False frame pageBits idx\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>node. cte = CTE parent node) \<and> global.sameRegionAs parent (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<and> isUntypedCap parent \<and> capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> capBits parent proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap False frame pageBits idx; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>parent. (\<exists>node. cte = CTE parent node) \<and> global.sameRegionAs parent (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<and> isUntypedCap parent \<and> capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> capBits parent proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; ctes_of s p = Some (CTE (capability.UntypedCap False frame pageBits idx) x2); x1 = capability.UntypedCap False frame pageBits idx; cte = CTE (capability.UntypedCap False frame pageBits idx) x2\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap False frame pageBits idx) (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<and> capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; ctes_of s p = Some (CTE (capability.UntypedCap False frame pageBits idx) x2); x1 = capability.UntypedCap False frame pageBits idx; cte = CTE (capability.UntypedCap False frame pageBits idx) x2\<rbrakk> \<Longrightarrow> (capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits) \<and> global.sameRegionAs (capability.UntypedCap False frame pageBits idx) (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) proof (prove)
goal (2 subgoals):
 1. \<And>cte x1 x2. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; ctes_of s p = Some (CTE (capability.UntypedCap False frame pageBits idx) x2); x1 = capability.UntypedCap False frame pageBits idx; cte = CTE (capability.UntypedCap False frame pageBits idx) x2\<rbrakk> \<Longrightarrow> capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits
 2. \<And>cte x1 x2. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; ctes_of s p = Some (CTE (capability.UntypedCap False frame pageBits idx) x2); x1 = capability.UntypedCap False frame pageBits idx; cte = CTE (capability.UntypedCap False frame pageBits idx) x2; capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap False frame pageBits idx) (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) proof (prove)
goal (2 subgoals):
 1. \<And>cte x1 x2. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; x1 = capability.UntypedCap False frame pageBits idx; cte = CTE (capability.UntypedCap False frame pageBits idx) x2; valid_cap' (capability.UntypedCap False frame pageBits idx) s\<rbrakk> \<Longrightarrow> capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits
 2. \<And>cte x1 x2. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; ctes_of s p = Some (CTE (capability.UntypedCap False frame pageBits idx) x2); x1 = capability.UntypedCap False frame pageBits idx; cte = CTE (capability.UntypedCap False frame pageBits idx) x2; capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap False frame pageBits idx) (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; is_aligned frame pageBits; valid_untyped' False frame pageBits idx s; frame \<noteq> 0; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) minUntypedSizeBits\<rbrakk> \<Longrightarrow> capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits
 2. \<And>cte x1 x2. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; ctes_of s p = Some (CTE (capability.UntypedCap False frame pageBits idx) x2); x1 = capability.UntypedCap False frame pageBits idx; cte = CTE (capability.UntypedCap False frame pageBits idx) x2; capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap False frame pageBits idx) (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; valid_untyped' False frame pageBits idx s; frame \<noteq> 0; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; idx \<le> 2 ^ pageBits; is_aligned (word_of_nat idx) minUntypedSizeBits; frame \<le> frame + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits
 2. \<And>cte x1 x2. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; ctes_of s p = Some (CTE (capability.UntypedCap False frame pageBits idx) x2); x1 = capability.UntypedCap False frame pageBits idx; cte = CTE (capability.UntypedCap False frame pageBits idx) x2; capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap False frame pageBits idx) (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) proof (prove)
goal (1 subgoal):
 1. \<And>cte x1 x2. \<lbrakk>descendants_of' p (ctes_of s) = {}; valid_pspace' s; ctes_of s p = Some (CTE (capability.UntypedCap False frame pageBits idx) x2); x1 = capability.UntypedCap False frame pageBits idx; cte = CTE (capability.UntypedCap False frame pageBits idx) x2; capRange (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) \<noteq> {} \<and> Suc (Suc local.asid_low_bits) \<le> pageBits\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap False frame pageBits idx) (capability.ArchObjectCap (arch_capability.ASIDPoolCap frame base)) proof (prove)
goal:
No subgoals!