theory Retype_C

lemma tcb_ctes_typ_region_bytes:
  "cvariable_array_map_relation (map_to_tcbs (ksPSpace \<sigma>))
      (\<lambda>x. 5) cte_Ptr (hrs_htd hrs)
    \<Longrightarrow> pspace_no_overlap' ptr bits \<sigma>
    \<Longrightarrow> pspace_aligned' \<sigma>
    \<Longrightarrow> is_aligned ptr bits
    \<Longrightarrow> cpspace_tcb_relation (ksPSpace \<sigma>) hrs
    \<Longrightarrow> cvariable_array_map_relation (map_to_tcbs (ksPSpace \<sigma>)) (\<lambda>x. 5)
        cte_Ptr (typ_region_bytes ptr bits (hrs_htd hrs))" apply (clarsimp simp: cvariable_array_map_relation_def
                        h_t_array_valid_def) apply (drule spec, drule mp, erule exI) 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 only: map_comp_Some_iff projectKOs
                             pspace_no_overlap'_def is_aligned_neg_mask_eq
                             field_simps upto_intvl_eq[symmetric]) apply (elim allE, drule(1) mp) apply simp apply (drule(1) pspace_alignedD') apply (erule disjoint_subset[rotated]) apply (simp add: upto_intvl_eq[symmetric]) apply (rule intvl_start_le) apply (simp add: objBits_simps' cte_C_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cvariable_array_map_relation (map_to_tcbs (ksPSpace \<sigma>)) (\<lambda>x. 5) cte_Ptr (hrs_htd hrs); pspace_no_overlap' ptr bits \<sigma>; pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs\<rbrakk> \<Longrightarrow> cvariable_array_map_relation (map_to_tcbs (ksPSpace \<sigma>)) (\<lambda>x. 5) cte_Ptr (typ_region_bytes ptr bits (hrs_htd hrs)) proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>\<forall>p. (\<exists>v. map_to_tcbs (ksPSpace \<sigma>) p = Some v) \<longrightarrow> valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5); pspace_no_overlap' ptr bits \<sigma>; pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; map_to_tcbs (ksPSpace \<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) 5 5) proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>pspace_no_overlap' ptr bits \<sigma>; pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; map_to_tcbs (ksPSpace \<sigma>) p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5)\<rbrakk> \<Longrightarrow> valid_footprint (typ_region_bytes ptr bits (hrs_htd hrs)) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5) proof (prove)
goal (2 subgoals):
 1. \<And>p v. \<lbrakk>pspace_no_overlap' ptr bits \<sigma>; pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; map_to_tcbs (ksPSpace \<sigma>) p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5)\<rbrakk> \<Longrightarrow> uinfo_array_tag_n_m TYPE(cte_C) 5 5 \<noteq> typ_uinfo_t TYPE(8 word)
 2. \<And>p v. \<lbrakk>pspace_no_overlap' ptr bits \<sigma>; pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; map_to_tcbs (ksPSpace \<sigma>) p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5)\<rbrakk> \<Longrightarrow> {p..+size_td (uinfo_array_tag_n_m TYPE(cte_C) 5 5)} \<inter> {ptr..+2 ^ bits} = {} \<and> valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5) proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>pspace_no_overlap' ptr bits \<sigma>; pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; map_to_tcbs (ksPSpace \<sigma>) p = Some v; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5)\<rbrakk> \<Longrightarrow> {p..+size_td (uinfo_array_tag_n_m TYPE(cte_C) 5 5)} \<inter> {ptr..+2 ^ bits} = {} \<and> valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5) proof (prove)
goal (1 subgoal):
 1. \<And>p v k'. \<lbrakk>\<forall>x ko. ksPSpace \<sigma> x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr..+2 ^ bits} = {}; pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5); ksPSpace \<sigma> p = Some (KOTCB v)\<rbrakk> \<Longrightarrow> {p..+size_td (uinfo_array_tag_n_m TYPE(cte_C) 5 5)} \<inter> {ptr..+2 ^ bits} = {} \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>p v k'. \<lbrakk>pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5); ksPSpace \<sigma> p = Some (KOTCB v); {p..p + 2 ^ objBitsKO (KOTCB v) - 1} \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> {p..+size_td (uinfo_array_tag_n_m TYPE(cte_C) 5 5)} \<inter> {ptr..+2 ^ bits} = {} \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5); ksPSpace \<sigma> p = Some (KOTCB v); {p..p + 2 ^ objBitsKO (KOTCB v) - 1} \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> {p..+size_of TYPE(cte_C) * 5} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5); {p..p + 2 ^ objBitsKO (KOTCB v) - 1} \<inter> {ptr..+2 ^ bits} = {}; is_aligned p (objBitsKO (KOTCB v))\<rbrakk> \<Longrightarrow> {p..+size_of TYPE(cte_C) * 5} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5); is_aligned p (objBitsKO (KOTCB v))\<rbrakk> \<Longrightarrow> {p..+size_of TYPE(cte_C) * 5} \<subseteq> {p..p + 2 ^ objBitsKO (KOTCB v) - 1} proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5); is_aligned p (objBitsKO (KOTCB v))\<rbrakk> \<Longrightarrow> {p..+size_of TYPE(cte_C) * 5} \<subseteq> {p..+2 ^ objBitsKO (KOTCB v)} proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>pspace_aligned' \<sigma>; is_aligned ptr bits; cpspace_tcb_relation (ksPSpace \<sigma>) hrs; valid_footprint (hrs_htd hrs) p (uinfo_array_tag_n_m TYPE(cte_C) 5 5); is_aligned p (objBitsKO (KOTCB v))\<rbrakk> \<Longrightarrow> size_of TYPE(cte_C) * 5 \<le> 2 ^ objBitsKO (KOTCB v) proof (prove)
goal:
No subgoals!