theory Retype_C

lemma gsCNodes_typ_region_bytes:
  "cvariable_array_map_relation (gsCNodes \<sigma>) ((^) 2) cte_Ptr (hrs_htd hrs)
    \<Longrightarrow> cnodes_retype_have_size {ptr..+2 ^ bits} bits (gsCNodes \<sigma>)
    \<Longrightarrow> 0 \<notin> {ptr..+2 ^ bits} \<Longrightarrow> is_aligned ptr bits
    \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hrs)
        = (clift hrs :: cte_C ptr \<Rightarrow> _)
    \<Longrightarrow> cvariable_array_map_relation (gsCNodes \<sigma>) ((^) 2) cte_Ptr
        (typ_region_bytes ptr bits (hrs_htd hrs))" apply (clarsimp simp: cvariable_array_map_relation_def
                        h_t_array_valid_def) apply (elim allE, drule(1) mp) apply (subst valid_footprint_typ_region_bytes) apply (simp add: uinfo_array_tag_n_m_def typ_uinfo_t_def typ_info_word) apply (clarsimp simp: cnodes_retype_have_size_def field_simps) apply (elim allE, drule(1) mp) apply (subgoal_tac "size_of TYPE(cte_C) * 2 ^ v = 2 ^ (cte_level_bits + v)") prefer 2 apply (simp add: cte_C_size cte_level_bits_def power_add) apply (clarsimp simp add: upto_intvl_eq[symmetric] field_simps) apply (case_tac "p \<in> {ptr ..+ 2 ^ bits}") apply (drule h_t_array_first_element_at[where p="Ptr p" and gd=c_guard for p,
       unfolded h_t_array_valid_def, simplified]) apply simp apply (rule is_aligned_c_guard[where m=2], simp+) apply clarsimp apply (simp add: align_of_def) apply (simp add: size_of_def cte_level_bits_def power_add) apply (simp add: cte_level_bits_def) apply (drule_tac x="cte_Ptr p" in fun_cong) apply (simp add: liftt_if[folded hrs_htd_def] hrs_htd_update
                    h_t_valid_def valid_footprint_typ_region_bytes
             split: if_split_asm) apply (subgoal_tac "p \<in> {p ..+ size_of TYPE(cte_C)}") apply (simp add: cte_C_size) apply blast apply (simp add: intvl_self) apply (simp only: upto_intvl_eq mask_in_range[symmetric]) apply (rule aligned_ranges_subset_or_disjoint_coroll, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cvariable_array_map_relation (gsCNodes \<sigma>) ((^) 2) cte_Ptr (hrs_htd hrs); cnodes_retype_have_size {ptr..+2 ^ bits} bits (gsCNodes \<sigma>); 0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs\<rbrakk> \<Longrightarrow> cvariable_array_map_relation (gsCNodes \<sigma>) ((^) 2) cte_Ptr (typ_region_bytes ptr bits (hrs_htd hrs)) proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>\<forall>p v. gsCNodes \<sigma> p = Some v \<longrightarrow> valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); cnodes_retype_have_size {ptr..+2 ^ bits} bits (gsCNodes \<sigma>); 0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v\<rbrakk> \<Longrightarrow> valid_footprint (typ_region_bytes ptr bits (hrs_htd hrs)) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)) proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>cnodes_retype_have_size {ptr..+2 ^ bits} bits (gsCNodes \<sigma>); 0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v))\<rbrakk> \<Longrightarrow> valid_footprint (typ_region_bytes ptr bits (hrs_htd hrs)) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)) proof (prove)
goal (2 subgoals):
 1. \<And>p v. \<lbrakk>cnodes_retype_have_size {ptr..+2 ^ bits} bits (gsCNodes \<sigma>); 0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v))\<rbrakk> \<Longrightarrow> uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v) \<noteq> typ_uinfo_t TYPE(8 word)
 2. \<And>p v. \<lbrakk>cnodes_retype_have_size {ptr..+2 ^ bits} bits (gsCNodes \<sigma>); 0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v))\<rbrakk> \<Longrightarrow> {p..+size_td (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v))} \<inter> {ptr..+2 ^ bits} = {} \<and> valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)) proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>cnodes_retype_have_size {ptr..+2 ^ bits} bits (gsCNodes \<sigma>); 0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v))\<rbrakk> \<Longrightarrow> {p..+size_td (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v))} \<inter> {ptr..+2 ^ bits} = {} \<and> valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)) proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>\<forall>ptr' sz'. gsCNodes \<sigma> ptr' = Some sz' \<longrightarrow> is_aligned ptr' (sz' + cte_level_bits) \<and> ({ptr'..+2 ^ (sz' + cte_level_bits)} \<inter> {ptr..+2 ^ bits} = {} \<or> sz' + cte_level_bits = bits); 0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v))\<rbrakk> \<Longrightarrow> {p..+size_of TYPE(cte_C) * 2 ^ v} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); is_aligned p (v + cte_level_bits) \<and> ({p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ bits} = {} \<or> v + cte_level_bits = bits)\<rbrakk> \<Longrightarrow> {p..+size_of TYPE(cte_C) * 2 ^ v} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); is_aligned p (v + cte_level_bits) \<and> ({p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ bits} = {} \<or> v + cte_level_bits = bits); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (cte_level_bits + v)\<rbrakk> \<Longrightarrow> {p..+size_of TYPE(cte_C) * 2 ^ v} \<inter> {ptr..+2 ^ bits} = {}
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); is_aligned p (v + cte_level_bits) \<and> ({p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ bits} = {} \<or> v + cte_level_bits = bits)\<rbrakk> \<Longrightarrow> size_of TYPE(cte_C) * 2 ^ v = 2 ^ (cte_level_bits + v) proof (prove)
goal (2 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); is_aligned p (v + cte_level_bits) \<and> ({p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ bits} = {} \<or> v + cte_level_bits = bits)\<rbrakk> \<Longrightarrow> size_of TYPE(cte_C) * 2 ^ v = 2 ^ (cte_level_bits + v)
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); is_aligned p (v + cte_level_bits) \<and> ({p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ bits} = {} \<or> v + cte_level_bits = bits); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (cte_level_bits + v)\<rbrakk> \<Longrightarrow> {p..+size_of TYPE(cte_C) * 2 ^ v} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ bits}; is_aligned ptr bits; clift (hrs_htd_update (typ_region_bytes ptr bits) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); is_aligned p (v + cte_level_bits) \<and> ({p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ bits} = {} \<or> v + cte_level_bits = bits); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (cte_level_bits + v)\<rbrakk> \<Longrightarrow> {p..+size_of TYPE(cte_C) * 2 ^ v} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (4 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> 0 < 2 ^ v
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> c_guard (cte_Ptr p)
 3. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}; hrs_htd hrs \<Turnstile>\<^sub>t cte_Ptr p\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 4. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (3 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> c_guard (cte_Ptr p)
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}; hrs_htd hrs \<Turnstile>\<^sub>t cte_Ptr p\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 3. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (6 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ (v + cte_level_bits)}\<rbrakk> \<Longrightarrow> p \<noteq> 0
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> align_of TYPE(cte_C) = 2\<^sup>2
 3. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> size_of TYPE(cte_C) \<le> 2 ^ (v + cte_level_bits)
 4. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> 2 \<le> v + cte_level_bits
 5. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}; hrs_htd hrs \<Turnstile>\<^sub>t cte_Ptr p\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 6. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (5 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> align_of TYPE(cte_C) = 2\<^sup>2
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> size_of TYPE(cte_C) \<le> 2 ^ (v + cte_level_bits)
 3. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> 2 \<le> v + cte_level_bits
 4. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}; hrs_htd hrs \<Turnstile>\<^sub>t cte_Ptr p\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 5. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (4 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> size_of TYPE(cte_C) \<le> 2 ^ (v + cte_level_bits)
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> 2 \<le> v + cte_level_bits
 3. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}; hrs_htd hrs \<Turnstile>\<^sub>t cte_Ptr p\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 4. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (3 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> 2 \<le> v + cte_level_bits
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}; hrs_htd hrs \<Turnstile>\<^sub>t cte_Ptr p\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 3. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}; hrs_htd hrs \<Turnstile>\<^sub>t cte_Ptr p\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ bits}; hrs_htd hrs \<Turnstile>\<^sub>t cte_Ptr p; clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) (cte_Ptr p) = clift hrs (cte_Ptr p)\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ (v + cte_level_bits)}; {p..+16} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}; valid_footprint (hrs_htd hrs) p (typ_uinfo_t TYPE(cte_C)); c_guard (cte_Ptr p); h_val (fst (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs)) (cte_Ptr p) = h_val (fst hrs) (cte_Ptr p)\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (3 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ (v + cte_level_bits)}; {p..+16} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}; valid_footprint (hrs_htd hrs) p (typ_uinfo_t TYPE(cte_C)); c_guard (cte_Ptr p); h_val (fst (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs)) (cte_Ptr p) = h_val (fst hrs) (cte_Ptr p); p \<in> {p..+size_of TYPE(cte_C)}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ (v + cte_level_bits)}; {p..+16} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}; valid_footprint (hrs_htd hrs) p (typ_uinfo_t TYPE(cte_C)); c_guard (cte_Ptr p); h_val (fst (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs)) (cte_Ptr p) = h_val (fst hrs) (cte_Ptr p)\<rbrakk> \<Longrightarrow> p \<in> {p..+size_of TYPE(cte_C)}
 3. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (3 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); gsCNodes \<sigma> p = Some v; 16 * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ (v + cte_level_bits)}; {p..+16} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}; valid_footprint (hrs_htd hrs) p (typ_uinfo_t TYPE(cte_C)); c_guard (cte_Ptr p); h_val (fst (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs)) (cte_Ptr p) = h_val (fst hrs) (cte_Ptr p); p \<in> {p..+16}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ (v + cte_level_bits)}; {p..+16} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}; valid_footprint (hrs_htd hrs) p (typ_uinfo_t TYPE(cte_C)); c_guard (cte_Ptr p); h_val (fst (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs)) (cte_Ptr p) = h_val (fst hrs) (cte_Ptr p)\<rbrakk> \<Longrightarrow> p \<in> {p..+size_of TYPE(cte_C)}
 3. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (2 subgoals):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); gsCNodes \<sigma> p = Some v; size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<in> {ptr..+2 ^ (v + cte_level_bits)}; {p..+16} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {}; valid_footprint (hrs_htd hrs) p (typ_uinfo_t TYPE(cte_C)); c_guard (cte_Ptr p); h_val (fst (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs)) (cte_Ptr p) = h_val (fst hrs) (cte_Ptr p)\<rbrakk> \<Longrightarrow> p \<in> {p..+size_of TYPE(cte_C)}
 2. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>0 \<notin> {ptr..+2 ^ (v + cte_level_bits)}; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ (v + cte_level_bits)} \<inter> {ptr..+2 ^ (v + cte_level_bits)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>0 && ~~ mask (v + cte_level_bits) \<noteq> ptr; is_aligned ptr (v + cte_level_bits); clift (hrs_htd_update (typ_region_bytes ptr (v + cte_level_bits)) hrs) = clift hrs; gsCNodes \<sigma> p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) (2 ^ v) (2 ^ v)); size_of TYPE(cte_C) * 2 ^ v = 2 ^ (v + cte_level_bits); is_aligned p (v + cte_level_bits); bits = v + cte_level_bits; p && ~~ mask (v + cte_level_bits) \<noteq> ptr\<rbrakk> \<Longrightarrow> {p..p + 2 ^ (v + cte_level_bits) - 1} \<inter> {ptr..ptr + 2 ^ (v + cte_level_bits) - 1} = {} proof (prove)
goal:
No subgoals!