theory CSpace_C

lemma untypedZeroRange_idx_forward_helper:
  "isUntypedCap cap
    \<Longrightarrow> capFreeIndex cap \<le> idx
    \<Longrightarrow> idx \<le> 2 ^ capBlockSize cap
    \<Longrightarrow> valid_cap' cap s
    \<Longrightarrow> (case (untypedZeroRange cap, untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap))
       of (Some (a, b), Some (a', b')) \<Rightarrow> {a' ..+ unat (b' + 1 - a')} \<subseteq> {a ..+ unat (b + 1 - a)}
        | _ \<Rightarrow> True)" apply (clarsimp split: option.split) apply (clarsimp simp: untypedZeroRange_def max_free_index_def Let_def
                        isCap_simps valid_cap_simps' capAligned_def untypedBits_defs
                 split: if_split_asm) apply (erule subsetD[rotated], rule intvl_both_le) apply (clarsimp simp: getFreeRef_def) apply (rule word_plus_mono_right) apply (rule PackedTypes.of_nat_mono_maybe_le) apply (erule order_le_less_trans, rule power_strict_increasing, simp_all) apply (erule is_aligned_no_wrap') apply (rule word_of_nat_less, simp) apply (simp add: getFreeRef_def) apply (simp add: unat_plus_simple[THEN iffD1, OF is_aligned_no_wrap']
                   word_of_nat_less) apply (simp add: word_of_nat_le unat_sub
                   order_le_less_trans[OF _ power_strict_increasing]
                   unat_of_nat_eq[where 'a=32, folded word_bits_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap cap; capFreeIndex cap \<le> idx; idx \<le> 2 ^ capBlockSize cap; valid_cap' cap s\<rbrakk> \<Longrightarrow> case (untypedZeroRange cap, untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap)) of (None, ba) \<Rightarrow> True | (Some (a, b), None) \<Rightarrow> True | (Some (a, b), Some (a', b')) \<Rightarrow> {a'..+unat (b' + 1 - a')} \<subseteq> {a..+unat (b + 1 - a)} proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba x. \<lbrakk>isUntypedCap cap; capFreeIndex cap \<le> idx; idx \<le> 2 ^ capBlockSize cap; valid_cap' cap s; untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) = Some (aa, ba); untypedZeroRange cap = Some (a, b); x \<in> {aa..+unat (ba + 1 - aa)}\<rbrakk> \<Longrightarrow> x \<in> {a..+unat (b + 1 - a)} proof (prove)
goal (1 subgoal):
 1. \<And>x d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; x \<in> {getFreeRef v0 idx..+unat (v0 + 2 ^ v1 - getFreeRef v0 idx)}; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> x \<in> {getFreeRef v0 f..+unat (v0 + 2 ^ v1 - getFreeRef v0 f)} proof (prove)
goal (2 subgoals):
 1. \<And>x d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> getFreeRef v0 f \<le> getFreeRef v0 idx
 2. \<And>x d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> unat (getFreeRef v0 idx) + unat (v0 + 2 ^ v1 - getFreeRef v0 idx) \<le> unat (getFreeRef v0 f) + unat (v0 + 2 ^ v1 - getFreeRef v0 f) proof (prove)
goal (2 subgoals):
 1. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> v0 + word_of_nat f \<le> v0 + word_of_nat idx
 2. \<And>x d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> unat (getFreeRef v0 idx) + unat (v0 + 2 ^ v1 - getFreeRef v0 idx) \<le> unat (getFreeRef v0 f) + unat (v0 + 2 ^ v1 - getFreeRef v0 f) proof (prove)
goal (3 subgoals):
 1. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> word_of_nat f \<le> word_of_nat idx
 2. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> v0 \<le> v0 + word_of_nat idx
 3. \<And>x d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> unat (getFreeRef v0 idx) + unat (v0 + 2 ^ v1 - getFreeRef v0 idx) \<le> unat (getFreeRef v0 f) + unat (v0 + 2 ^ v1 - getFreeRef v0 f) proof (prove)
goal (4 subgoals):
 1. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> idx < 2 ^ LENGTH(32)
 2. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> f \<le> idx
 3. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> v0 \<le> v0 + word_of_nat idx
 4. \<And>x d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> unat (getFreeRef v0 idx) + unat (v0 + 2 ^ v1 - getFreeRef v0 idx) \<le> unat (getFreeRef v0 f) + unat (v0 + 2 ^ v1 - getFreeRef v0 f) proof (prove)
goal (2 subgoals):
 1. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> v0 \<le> v0 + word_of_nat idx
 2. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> unat (getFreeRef v0 idx) + unat (v0 + 2 ^ v1 - getFreeRef v0 idx) \<le> unat (getFreeRef v0 f) + unat (v0 + 2 ^ v1 - getFreeRef v0 f) proof (prove)
goal (2 subgoals):
 1. \<And>d da v0 v1 f. \<lbrakk>v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> word_of_nat idx < 2 ^ v1
 2. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> unat (getFreeRef v0 idx) + unat (v0 + 2 ^ v1 - getFreeRef v0 idx) \<le> unat (getFreeRef v0 f) + unat (v0 + 2 ^ v1 - getFreeRef v0 f) proof (prove)
goal (1 subgoal):
 1. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> unat (getFreeRef v0 idx) + unat (v0 + 2 ^ v1 - getFreeRef v0 idx) \<le> unat (getFreeRef v0 f) + unat (v0 + 2 ^ v1 - getFreeRef v0 f) proof (prove)
goal (1 subgoal):
 1. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> unat (v0 + word_of_nat idx) + unat (2 ^ v1 - word_of_nat idx) \<le> unat (v0 + word_of_nat f) + unat (2 ^ v1 - word_of_nat f) proof (prove)
goal (1 subgoal):
 1. \<And>d da v0 v1 f. \<lbrakk>is_aligned v0 v1; v1 < word_bits; valid_untyped' False v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; is_aligned (word_of_nat f) 4; f \<le> idx; idx \<le> 2 ^ v1; cap = capability.UntypedCap False v0 v1 f; \<not> d; idx \<noteq> 2 ^ v1; \<not> da\<rbrakk> \<Longrightarrow> unat (word_of_nat idx) + unat (2 ^ v1 - word_of_nat idx) \<le> unat (word_of_nat f) + unat (2 ^ v1 - word_of_nat f) proof (prove)
goal:
No subgoals!