theory Retype_C

lemma zero_ranges_ptr_retyps:
  "zero_ranges_are_zero (gsUntypedZeroRanges s) hrs
    \<Longrightarrow> caps_overlap_reserved' {ptr_val (p :: 'a ptr) ..+ n * size_of TYPE ('a :: mem_type)} s
    \<Longrightarrow> untyped_ranges_zero' s
    \<Longrightarrow> valid_objs' s
    \<Longrightarrow> zero_ranges_are_zero (gsUntypedZeroRanges s)
       (hrs_htd_update (ptr_retyps_gen n p arr) hrs)" apply (clarsimp simp: zero_ranges_are_zero_def untyped_ranges_zero_inv_def
                        hrs_htd_update) apply (drule(1) bspec, clarsimp) apply (rule region_actually_is_bytes_retyp_disjoint, simp_all) apply (clarsimp simp: map_comp_Some_iff cteCaps_of_def
                 elim!: ranE) apply (frule(1) ctes_of_valid') apply (simp add: caps_overlap_reserved'_def,
      drule bspec, erule ranI) apply (frule(1) untypedZeroRange_to_usableCapRange) apply (clarsimp simp: isCap_simps untypedZeroRange_def
                        getFreeRef_def max_free_index_def
                 split: if_split_asm) apply (erule disjoint_subset[rotated]) apply (subst intvl_plus_unat_eq) apply clarsimp apply clarsimp apply (clarsimp simp: word_unat.Rep_inject[symmetric]
                         valid_cap_simps' capAligned_def
                         unat_of_nat
               simp del: word_unat.Rep_inject) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>zero_ranges_are_zero (gsUntypedZeroRanges s) hrs; caps_overlap_reserved' {ptr_val p..+n * size_of TYPE('a)} s; untyped_ranges_zero' s; valid_objs' s\<rbrakk> \<Longrightarrow> zero_ranges_are_zero (gsUntypedZeroRanges s) (hrs_htd_update (ptr_retyps_gen n p arr) hrs) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s). case x of (start, end) \<Rightarrow> region_actually_is_bytes' start (unat (end + 1 - start)) (hrs_htd hrs) \<and> heap_list (hrs_mem hrs) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; caps_overlap_reserved' {ptr_val p..+n * size_of TYPE('a)} s; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s); valid_objs' s; (a, b) \<in> ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s)\<rbrakk> \<Longrightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (ptr_retyps_gen n p arr (hrs_htd hrs)) \<and> heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_overlap_reserved' {ptr_val p..+n * size_of TYPE('a)} s; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s); valid_objs' s; (a, b) \<in> ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s); region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (ptr_retyps_gen n p arr (hrs_htd hrs)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_overlap_reserved' {ptr_val p..+n * size_of TYPE('a)} s; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s); valid_objs' s; (a, b) \<in> ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s); region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0\<rbrakk> \<Longrightarrow> {a..+unat (b + 1 - a)} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b x z. \<lbrakk>caps_overlap_reserved' {ptr_val p..+n * size_of TYPE('a)} s; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; untypedZeroRange (cteCap z) = Some (a, b); ctes_of s x = Some z\<rbrakk> \<Longrightarrow> {a..+unat (b + 1 - a)} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b x z. \<lbrakk>caps_overlap_reserved' {ptr_val p..+n * size_of TYPE('a)} s; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; untypedZeroRange (cteCap z) = Some (a, b); ctes_of s x = Some z; valid_cap' (cteCap z) s\<rbrakk> \<Longrightarrow> {a..+unat (b + 1 - a)} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b x z. \<lbrakk>gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; untypedZeroRange (cteCap z) = Some (a, b); ctes_of s x = Some z; valid_cap' (cteCap z) s; isUntypedCap (cteCap z) \<longrightarrow> usableUntypedRange (cteCap z) \<inter> {ptr_val p..+n * size_of TYPE('a)} = {}\<rbrakk> \<Longrightarrow> {a..+unat (b + 1 - a)} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b x z. \<lbrakk>gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; untypedZeroRange (cteCap z) = Some (a, b); ctes_of s x = Some z; valid_cap' (cteCap z) s; isUntypedCap (cteCap z) \<longrightarrow> usableUntypedRange (cteCap z) \<inter> {ptr_val p..+n * size_of TYPE('a)} = {}; isUntypedCap (cteCap z) \<and> usableUntypedRange (cteCap z) = {a..b} \<and> a \<le> b\<rbrakk> \<Longrightarrow> {a..+unat (b + 1 - a)} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x z d v0 v1 f. \<lbrakk>(let cap = capability.UntypedCap d v0 v1 f in if d then Nothing else Just (fromPPtr (capPtr cap + word_of_nat (capFreeIndex cap)), fromPPtr (capPtr cap + 2 ^ capBlockSize cap - 1))) = Some (v0 + word_of_nat f, v0 + 2 ^ v1 - 1); ctes_of s x = Some z; valid_cap' (capability.UntypedCap d v0 v1 f) s; {v0 + word_of_nat f..v0 + 2 ^ v1 - 1} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {}; cteCap z = capability.UntypedCap d v0 v1 f; v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' (v0 + word_of_nat f) (unat (2 ^ v1 - word_of_nat f)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (2 ^ v1 - word_of_nat f)) (v0 + word_of_nat f) = replicate (unat (2 ^ v1 - word_of_nat f)) 0; f < 2 ^ v1\<rbrakk> \<Longrightarrow> {v0 + word_of_nat f..+unat (2 ^ v1 - word_of_nat f)} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x z d v0 v1 f. \<lbrakk>(let cap = capability.UntypedCap d v0 v1 f in if d then Nothing else Just (fromPPtr (capPtr cap + word_of_nat (capFreeIndex cap)), fromPPtr (capPtr cap + 2 ^ capBlockSize cap - 1))) = Some (v0 + word_of_nat f, v0 + 2 ^ v1 - 1); ctes_of s x = Some z; valid_cap' (capability.UntypedCap d v0 v1 f) s; cteCap z = capability.UntypedCap d v0 v1 f; v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' (v0 + word_of_nat f) (unat (2 ^ v1 - word_of_nat f)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (2 ^ v1 - word_of_nat f)) (v0 + word_of_nat f) = replicate (unat (2 ^ v1 - word_of_nat f)) 0; f < 2 ^ v1\<rbrakk> \<Longrightarrow> {v0 + word_of_nat f..+unat (2 ^ v1 - word_of_nat f)} \<subseteq> {v0 + word_of_nat f..v0 + 2 ^ v1 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x z d v0 v1 f. \<lbrakk>(let cap = capability.UntypedCap d v0 v1 f in if d then Nothing else Just (fromPPtr (capPtr cap + word_of_nat (capFreeIndex cap)), fromPPtr (capPtr cap + 2 ^ capBlockSize cap - 1))) = Some (v0 + word_of_nat f, v0 + 2 ^ v1 - 1); ctes_of s x = Some z; valid_cap' (capability.UntypedCap d v0 v1 f) s; cteCap z = capability.UntypedCap d v0 v1 f; v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' (v0 + word_of_nat f) (unat (2 ^ v1 - word_of_nat f)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (2 ^ v1 - word_of_nat f)) (v0 + word_of_nat f) = replicate (unat (2 ^ v1 - word_of_nat f)) 0; f < 2 ^ v1\<rbrakk> \<Longrightarrow> v0 + word_of_nat f \<le> v0 + word_of_nat f + (2 ^ v1 - word_of_nat f) - 1
 2. \<And>x z d v0 v1 f. \<lbrakk>(let cap = capability.UntypedCap d v0 v1 f in if d then Nothing else Just (fromPPtr (capPtr cap + word_of_nat (capFreeIndex cap)), fromPPtr (capPtr cap + 2 ^ capBlockSize cap - 1))) = Some (v0 + word_of_nat f, v0 + 2 ^ v1 - 1); ctes_of s x = Some z; valid_cap' (capability.UntypedCap d v0 v1 f) s; cteCap z = capability.UntypedCap d v0 v1 f; v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' (v0 + word_of_nat f) (unat (2 ^ v1 - word_of_nat f)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (2 ^ v1 - word_of_nat f)) (v0 + word_of_nat f) = replicate (unat (2 ^ v1 - word_of_nat f)) 0; f < 2 ^ v1\<rbrakk> \<Longrightarrow> 2 ^ v1 - word_of_nat f \<noteq> 0
 3. \<And>x z d v0 v1 f. \<lbrakk>(let cap = capability.UntypedCap d v0 v1 f in if d then Nothing else Just (fromPPtr (capPtr cap + word_of_nat (capFreeIndex cap)), fromPPtr (capPtr cap + 2 ^ capBlockSize cap - 1))) = Some (v0 + word_of_nat f, v0 + 2 ^ v1 - 1); ctes_of s x = Some z; valid_cap' (capability.UntypedCap d v0 v1 f) s; cteCap z = capability.UntypedCap d v0 v1 f; v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' (v0 + word_of_nat f) (unat (2 ^ v1 - word_of_nat f)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (2 ^ v1 - word_of_nat f)) (v0 + word_of_nat f) = replicate (unat (2 ^ v1 - word_of_nat f)) 0; f < 2 ^ v1\<rbrakk> \<Longrightarrow> {v0 + word_of_nat f..v0 + word_of_nat f + (2 ^ v1 - word_of_nat f) - 1} \<subseteq> {v0 + word_of_nat f..v0 + 2 ^ v1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x z d v0 v1 f. \<lbrakk>(let cap = capability.UntypedCap d v0 v1 f in if d then Nothing else Just (fromPPtr (capPtr cap + word_of_nat (capFreeIndex cap)), fromPPtr (capPtr cap + 2 ^ capBlockSize cap - 1))) = Some (v0 + word_of_nat f, v0 + 2 ^ v1 - 1); ctes_of s x = Some z; valid_cap' (capability.UntypedCap d v0 v1 f) s; cteCap z = capability.UntypedCap d v0 v1 f; v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' (v0 + word_of_nat f) (unat (2 ^ v1 - word_of_nat f)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (2 ^ v1 - word_of_nat f)) (v0 + word_of_nat f) = replicate (unat (2 ^ v1 - word_of_nat f)) 0; f < 2 ^ v1\<rbrakk> \<Longrightarrow> 2 ^ v1 - word_of_nat f \<noteq> 0
 2. \<And>x z d v0 v1 f. \<lbrakk>(let cap = capability.UntypedCap d v0 v1 f in if d then Nothing else Just (fromPPtr (capPtr cap + word_of_nat (capFreeIndex cap)), fromPPtr (capPtr cap + 2 ^ capBlockSize cap - 1))) = Some (v0 + word_of_nat f, v0 + 2 ^ v1 - 1); ctes_of s x = Some z; valid_cap' (capability.UntypedCap d v0 v1 f) s; cteCap z = capability.UntypedCap d v0 v1 f; v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' (v0 + word_of_nat f) (unat (2 ^ v1 - word_of_nat f)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (2 ^ v1 - word_of_nat f)) (v0 + word_of_nat f) = replicate (unat (2 ^ v1 - word_of_nat f)) 0; f < 2 ^ v1\<rbrakk> \<Longrightarrow> {v0 + word_of_nat f..v0 + word_of_nat f + (2 ^ v1 - word_of_nat f) - 1} \<subseteq> {v0 + word_of_nat f..v0 + 2 ^ v1 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x z d v0 v1 f. \<lbrakk>(let cap = capability.UntypedCap d v0 v1 f in if d then Nothing else Just (fromPPtr (capPtr cap + word_of_nat (capFreeIndex cap)), fromPPtr (capPtr cap + 2 ^ capBlockSize cap - 1))) = Some (v0 + word_of_nat f, v0 + word_of_nat f - 1); ctes_of s x = Some z; valid_cap' (capability.UntypedCap d v0 v1 f) s; cteCap z = capability.UntypedCap d v0 v1 f; v0 + word_of_nat f \<le> v0 + word_of_nat f - 1; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' (v0 + word_of_nat f) 0 (hrs_htd hrs); f < 2 ^ v1; 2 ^ v1 = word_of_nat f\<rbrakk> \<Longrightarrow> False
 2. \<And>x z d v0 v1 f. \<lbrakk>(let cap = capability.UntypedCap d v0 v1 f in if d then Nothing else Just (fromPPtr (capPtr cap + word_of_nat (capFreeIndex cap)), fromPPtr (capPtr cap + 2 ^ capBlockSize cap - 1))) = Some (v0 + word_of_nat f, v0 + 2 ^ v1 - 1); ctes_of s x = Some z; valid_cap' (capability.UntypedCap d v0 v1 f) s; cteCap z = capability.UntypedCap d v0 v1 f; v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' (v0 + word_of_nat f) (unat (2 ^ v1 - word_of_nat f)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (2 ^ v1 - word_of_nat f)) (v0 + word_of_nat f) = replicate (unat (2 ^ v1 - word_of_nat f)) 0; f < 2 ^ v1\<rbrakk> \<Longrightarrow> {v0 + word_of_nat f..v0 + word_of_nat f + (2 ^ v1 - word_of_nat f) - 1} \<subseteq> {v0 + word_of_nat f..v0 + 2 ^ v1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x z d v0 v1 f. \<lbrakk>(let cap = capability.UntypedCap d v0 v1 f in if d then Nothing else Just (fromPPtr (capPtr cap + word_of_nat (capFreeIndex cap)), fromPPtr (capPtr cap + 2 ^ capBlockSize cap - 1))) = Some (v0 + word_of_nat f, v0 + 2 ^ v1 - 1); ctes_of s x = Some z; valid_cap' (capability.UntypedCap d v0 v1 f) s; cteCap z = capability.UntypedCap d v0 v1 f; v0 + word_of_nat f \<le> v0 + 2 ^ v1 - 1; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); valid_objs' s; region_actually_is_bytes' (v0 + word_of_nat f) (unat (2 ^ v1 - word_of_nat f)) (hrs_htd hrs); heap_list (hrs_mem hrs) (unat (2 ^ v1 - word_of_nat f)) (v0 + word_of_nat f) = replicate (unat (2 ^ v1 - word_of_nat f)) 0; f < 2 ^ v1\<rbrakk> \<Longrightarrow> {v0 + word_of_nat f..v0 + word_of_nat f + (2 ^ v1 - word_of_nat f) - 1} \<subseteq> {v0 + word_of_nat f..v0 + 2 ^ v1 - 1} proof (prove)
goal:
No subgoals!