theory CSpace_C

lemma untypedZeroRange_idx_backward_helper:
  "isUntypedCap cap
    \<Longrightarrow> idx \<le> capFreeIndex cap
    \<Longrightarrow> idx \<le> 2 ^ capBlockSize cap
    \<Longrightarrow> valid_cap' cap s
    \<Longrightarrow> (case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap)
       of None \<Rightarrow> True | Some (a', b') \<Rightarrow>
        {a' ..+ unat (b' + 1 - a')} \<subseteq> {capPtr cap + of_nat idx ..+ (capFreeIndex cap - idx)}
            \<union> (case untypedZeroRange cap
               of Some (a, b) \<Rightarrow> {a ..+ unat (b + 1 - a)}
                | None \<Rightarrow> {})
  )" apply (clarsimp split: option.split, intro impI conjI allI) apply (rule intvl_both_le; clarsimp simp: untypedZeroRange_def
                         max_free_index_def Let_def
                         isCap_simps valid_cap_simps' capAligned_def
                  split: if_split_asm) apply (clarsimp simp: getFreeRef_def) apply (clarsimp simp: getFreeRef_def) 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]) apply (subst intvl_close_Un) apply (clarsimp simp: untypedZeroRange_def
                         max_free_index_def Let_def
                         getFreeRef_def
                  split: if_split_asm) apply (clarsimp simp: untypedZeroRange_def
                        max_free_index_def Let_def
                        getFreeRef_def isCap_simps valid_cap_simps'
                 split: if_split_asm) apply (simp add: word_of_nat_le unat_sub capAligned_def
                   order_le_less_trans[OF _ power_strict_increasing]
                   order_le_less_trans[where x=idx]
                   unat_of_nat_eq[where 'a=32, folded word_bits_def]) done

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