theory CSpace_R

lemma usableUntypedRange_empty:
  "valid_cap' cp s \<Longrightarrow> isUntypedCap cp
    \<Longrightarrow> (usableUntypedRange cp = {}) = (capFreeIndex cp = maxFreeIndex (capBlockSize cp))" apply (clarsimp simp: isCap_simps max_free_index_def valid_cap_simps' capAligned_def) apply (rule order_trans, rule word_plus_mono_right) apply (rule_tac x="2 ^ capBlockSize cp - 1" in word_of_nat_le) apply (simp add: unat_2p_sub_1 maxUntypedSizeBits_def) apply (simp add: field_simps is_aligned_no_overflow) apply (simp add: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' cp s; isUntypedCap cp\<rbrakk> \<Longrightarrow> (usableUntypedRange cp = {}) = (capFreeIndex cp = maxFreeIndex (capBlockSize cp)) proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f. \<lbrakk>cp = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; f < 2 ^ v1\<rbrakk> \<Longrightarrow> v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1 proof (prove)
goal (3 subgoals):
 1. \<And>d v0 v1 f. \<lbrakk>cp = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; f < 2 ^ v1\<rbrakk> \<Longrightarrow> word_of_nat f \<le> ?z26 d v0 v1 f
 2. \<And>d v0 v1 f. \<lbrakk>cp = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; f < 2 ^ v1\<rbrakk> \<Longrightarrow> v0 \<le> v0 + ?z26 d v0 v1 f
 3. \<And>d v0 v1 f. \<lbrakk>cp = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; f < 2 ^ v1\<rbrakk> \<Longrightarrow> v0 + ?z26 d v0 v1 f \<le> v0 + 2 ^ v1 - 1 proof (prove)
goal (3 subgoals):
 1. \<And>d v0 v1 f. \<lbrakk>cp = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; f < 2 ^ v1\<rbrakk> \<Longrightarrow> f \<le> unat (2 ^ capBlockSize cp - 1)
 2. \<And>d v0 v1 f. \<lbrakk>cp = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; f < 2 ^ v1\<rbrakk> \<Longrightarrow> v0 \<le> v0 + (2 ^ capBlockSize cp - 1)
 3. \<And>d v0 v1 f. \<lbrakk>cp = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; f < 2 ^ v1\<rbrakk> \<Longrightarrow> v0 + (2 ^ capBlockSize cp - 1) \<le> v0 + 2 ^ v1 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>d v0 v1 f. \<lbrakk>cp = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; f < 2 ^ v1\<rbrakk> \<Longrightarrow> v0 \<le> v0 + (2 ^ capBlockSize cp - 1)
 2. \<And>d v0 v1 f. \<lbrakk>cp = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; f < 2 ^ v1\<rbrakk> \<Longrightarrow> v0 + (2 ^ capBlockSize cp - 1) \<le> v0 + 2 ^ v1 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f. \<lbrakk>cp = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; f < 2 ^ v1\<rbrakk> \<Longrightarrow> v0 + (2 ^ capBlockSize cp - 1) \<le> v0 + 2 ^ v1 - 1 proof (prove)
goal:
No subgoals!