theory Retype_C

lemma retype_offs_region_actually_is_zero_bytes:
  "\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr; untyped_ranges_zero' s;
      cteCap cte = UntypedCap False (ptr &&~~ mask sz) sz idx;
      idx \<le> unat (ptr && mask sz);
      range_cover ptr sz (getObjectSize newType userSize) num_ret \<rbrakk>
    \<Longrightarrow> region_actually_is_zero_bytes ptr
            (num_ret * 2 ^ APIType_capBits newType userSize) s'" using word_unat_mask_lt[where w=ptr and m=sz] apply - apply (frule range_cover.sz(1)) apply (drule(2) ctes_of_untyped_zero_rf_sr) apply (simp add: untypedZeroRange_def max_free_index_def word_size) apply clarify apply (strengthen heap_list_is_zero_mono2[mk_strg I E]
      region_actually_is_bytes_subset[mk_strg I E]) apply (simp add: getFreeRef_def word_size) apply (rule intvl_both_le) apply (rule order_trans, rule word_plus_mono_right, erule word_of_nat_le) apply (simp add: word_plus_and_or_coroll2 add.commute word_and_le2) apply (simp add: word_plus_and_or_coroll2 add.commute) apply (subst unat_plus_simple[THEN iffD1], rule is_aligned_no_wrap',
    rule is_aligned_neg_mask2) apply (rule word_of_nat_less, simp) apply (simp add: unat_of_nat_eq[OF order_less_trans, OF _ power_strict_increasing[where n=sz]]
    unat_sub[OF word_of_nat_le]) apply (subst word_plus_and_or_coroll2[where x=ptr and w="mask sz", symmetric]) apply (subst unat_plus_simple[THEN iffD1],
    simp add: word_plus_and_or_coroll2 add.commute word_and_le2) apply simp apply (rule order_trans[rotated], erule range_cover.range_cover_compare_bound) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; (s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (getObjectSize newType userSize) num_ret\<rbrakk> \<Longrightarrow> region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr = replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0 proof (prove)
using this:
sz \<le> size ptr \<Longrightarrow> unat (ptr && mask sz) < 2 ^ sz

goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; (s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (getObjectSize newType userSize) num_ret\<rbrakk> \<Longrightarrow> region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr = replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; (s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (getObjectSize newType userSize) num_ret; sz \<le> size ptr \<Longrightarrow> unat (ptr && mask sz) < 2 ^ sz\<rbrakk> \<Longrightarrow> region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr = replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; (s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (getObjectSize newType userSize) num_ret; sz \<le> size ptr \<Longrightarrow> unat (ptr && mask sz) < 2 ^ sz; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr = replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (getObjectSize newType userSize) num_ret; sz \<le> size ptr \<Longrightarrow> unat (ptr && mask sz) < 2 ^ sz; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> untypedZeroRange (cteCap cte) = Some (?start3, ?end3)
 2. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (getObjectSize newType userSize) num_ret; sz \<le> size ptr \<Longrightarrow> unat (ptr && mask sz) < 2 ^ sz; sz < LENGTH(32); region_actually_is_bytes ?start3 (unat (?end3 + 1 - ?start3)) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (?end3 + 1 - ?start3)) ?start3 = replicate (unat (?end3 + 1 - ?start3)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr = replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (getObjectSize newType userSize) num_ret; sz \<le> size ptr \<Longrightarrow> unat (ptr && mask sz) < 2 ^ sz; sz < LENGTH(32); region_actually_is_bytes (getFreeRef (ptr && ~~ mask sz) idx) (unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)) (getFreeRef (ptr && ~~ mask sz) idx) = replicate (unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr = replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (getObjectSize newType userSize) num_ret; sz \<le> size ptr \<Longrightarrow> unat (ptr && mask sz) < 2 ^ sz; sz < LENGTH(32); region_actually_is_bytes (getFreeRef (ptr && ~~ mask sz) idx) (unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)) (getFreeRef (ptr && ~~ mask sz) idx) = replicate (unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr = replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (getObjectSize newType userSize) num_ret; sz \<le> size ptr \<Longrightarrow> unat (ptr && mask sz) < 2 ^ sz; sz < LENGTH(32); region_actually_is_bytes (getFreeRef (ptr && ~~ mask sz) idx) (unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)) (getFreeRef (ptr && ~~ mask sz) idx) = replicate (unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)) 0\<rbrakk> \<Longrightarrow> {ptr..+num_ret * 2 ^ APIType_capBits newType userSize} \<subseteq> {getFreeRef (ptr && ~~ mask sz) idx..+unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)} \<and> {ptr..+num_ret * 2 ^ APIType_capBits newType userSize} \<subseteq> {getFreeRef (ptr && ~~ mask sz) idx..+unat ((ptr && ~~ mask sz) + 2 ^ sz - 1 + 1 - getFreeRef (ptr && ~~ mask sz) idx)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> {ptr..+num_ret * 2 ^ APIType_capBits newType userSize} \<subseteq> {(ptr && ~~ mask sz) + word_of_nat idx..+unat (2 ^ sz - word_of_nat idx)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + word_of_nat idx \<le> ptr
 2. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> unat ptr + num_ret * 2 ^ APIType_capBits newType userSize \<le> unat ((ptr && ~~ mask sz) + word_of_nat idx) + unat (2 ^ sz - word_of_nat idx) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (ptr && mask sz)
 2. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) \<le> ptr
 3. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> unat ptr + num_ret * 2 ^ APIType_capBits newType userSize \<le> unat ((ptr && ~~ mask sz) + word_of_nat idx) + unat (2 ^ sz - word_of_nat idx) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) \<le> ptr
 2. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> unat ptr + num_ret * 2 ^ APIType_capBits newType userSize \<le> unat ((ptr && ~~ mask sz) + word_of_nat idx) + unat (2 ^ sz - word_of_nat idx) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> unat ptr + num_ret * 2 ^ APIType_capBits newType userSize \<le> unat ((ptr && ~~ mask sz) + word_of_nat idx) + unat (2 ^ sz - word_of_nat idx) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> word_of_nat idx < 2 ^ sz
 2. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> unat ptr + num_ret * 2 ^ APIType_capBits newType userSize \<le> unat (ptr && ~~ mask sz) + unat (word_of_nat idx) + unat (2 ^ sz - word_of_nat idx) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (unat (2 ^ sz - word_of_nat idx)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (2 ^ sz - word_of_nat idx)) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (unat (2 ^ sz - word_of_nat idx)) 0\<rbrakk> \<Longrightarrow> unat ptr + num_ret * 2 ^ APIType_capBits newType userSize \<le> unat (ptr && ~~ mask sz) + unat (word_of_nat idx) + unat (2 ^ sz - word_of_nat idx) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (2 ^ sz - idx) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (2 ^ sz - idx) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (2 ^ sz - idx) 0\<rbrakk> \<Longrightarrow> unat ptr + num_ret * 2 ^ APIType_capBits newType userSize \<le> unat (ptr && ~~ mask sz) + 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (2 ^ sz - idx) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (2 ^ sz - idx) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (2 ^ sz - idx) 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (ptr && ~~ mask sz)) + num_ret * 2 ^ APIType_capBits newType userSize \<le> unat (ptr && ~~ mask sz) + 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (2 ^ sz - idx) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (2 ^ sz - idx) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (2 ^ sz - idx) 0\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (ptr && ~~ mask sz) + num_ret * 2 ^ APIType_capBits newType userSize \<le> unat (ptr && ~~ mask sz) + 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (2 ^ sz - idx) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (2 ^ sz - idx) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (2 ^ sz - idx) 0\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + num_ret * 2 ^ APIType_capBits newType userSize \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; untyped_ranges_zero' s; cteCap cte = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz (APIType_capBits newType userSize) num_ret; unat (ptr && mask sz) < 2 ^ sz; sz < 32; region_actually_is_bytes ((ptr && ~~ mask sz) + word_of_nat idx) (2 ^ sz - idx) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (2 ^ sz - idx) ((ptr && ~~ mask sz) + word_of_nat idx) = replicate (2 ^ sz - idx) 0\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + num_ret * 2 ^ APIType_capBits newType userSize \<le> num_ret * 2 ^ APIType_capBits newType userSize + unat (ptr && mask sz) proof (prove)
goal:
No subgoals!