theory Untyped_R

lemma retype_region_caps_overlap_reserved:
  "\<lbrace>valid_pspace and valid_mdb and
    pspace_no_overlap_range_cover ptr sz and caps_no_overlap ptr sz and
    caps_overlap_reserved
      {ptr..ptr + of_nat n * 2^obj_bits_api (APIType_map2 (Inr ao')) us - 1} and
    (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) and
    K (APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us) and
    K (range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n) and
    K (S \<subseteq> {ptr..ptr + of_nat n *
                  2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1})\<rbrace>
   retype_region ptr n us (APIType_map2 (Inr ao')) dev
   \<lbrace>\<lambda>rv s. caps_overlap_reserved S s\<rbrace>" apply (rule hoare_gen_asm)+ apply (simp (no_asm) add:caps_overlap_reserved_def2) apply (rule hoare_pre) apply (wp retype_region_caps_of) apply simp+ apply (simp add:caps_overlap_reserved_def2) apply (intro conjI,simp+) apply clarsimp apply (drule bspec) apply simp+ apply (erule(1) disjoint_subset2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace and valid_mdb and pspace_no_overlap (up_aligned_area ptr sz) and caps_no_overlap ptr sz and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) and K (APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n) and K (S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1})\<rbrace> retype_region ptr n us (APIType_map2 (Inr ao')) dev \<lbrace>\<lambda>rv. caps_overlap_reserved S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>valid_pspace and valid_mdb and pspace_no_overlap (up_aligned_area ptr sz) and caps_no_overlap ptr sz and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s)\<rbrace> retype_region ptr n us (APIType_map2 (Inr ao')) dev \<lbrace>\<lambda>rv. caps_overlap_reserved S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>valid_pspace and valid_mdb and pspace_no_overlap (up_aligned_area ptr sz) and caps_no_overlap ptr sz and (\<lambda>s. \<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} = {}) and (\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s)\<rbrace> retype_region ptr n us (APIType_map2 (Inr ao')) dev \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> retype_region ptr n us (APIType_map2 (Inr ao')) dev \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}\<rbrace>
 2. \<And>s. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us; (valid_pspace and valid_mdb and pspace_no_overlap (up_aligned_area ptr sz) and caps_no_overlap ptr sz and (\<lambda>s. \<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} = {}) and (\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s)) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us; APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> 0 < us
 2. \<And>s. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; APIType_map2 (Inr ao') = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us; (valid_pspace and valid_mdb and pspace_no_overlap (up_aligned_area ptr sz) and caps_no_overlap ptr sz and (\<lambda>s. \<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} = {}) and (\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s)) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz10 (obj_bits_api (APIType_map2 (Inr ao')) us) n \<and> caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s \<and> caps_no_overlap ptr ?sz10 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz10) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz10 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; valid_pspace s \<and> valid_mdb s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> caps_no_overlap ptr sz s \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} = {}) \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s)\<rbrakk> \<Longrightarrow> range_cover ptr ?sz10 (obj_bits_api (APIType_map2 (Inr ao')) us) n \<and> caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} s \<and> caps_no_overlap ptr ?sz10 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz10) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz10 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; valid_pspace s \<and> valid_mdb s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> caps_no_overlap ptr sz s \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} = {}) \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s)\<rbrakk> \<Longrightarrow> range_cover ptr ?sz10 (obj_bits_api (APIType_map2 (Inr ao')) us) n \<and> caps_no_overlap ptr ?sz10 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz10) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz10 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; valid_pspace s \<and> valid_mdb s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> caps_no_overlap ptr sz s \<and> (\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} = {}) \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s)\<rbrakk> \<Longrightarrow> \<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; cap \<in> ran (null_filter (caps_of_state s)); valid_pspace s; valid_mdb s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_no_overlap ptr sz s; \<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} = {}; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s; is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cap a b. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; cap \<in> ran (null_filter (caps_of_state s)); valid_pspace s; valid_mdb s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_no_overlap ptr sz s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s; is_untyped_cap cap\<rbrakk> \<Longrightarrow> ?cap32 s cap a b \<in> ran (null_filter (caps_of_state s))
 2. \<And>s cap a b. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; cap \<in> ran (null_filter (caps_of_state s)); valid_pspace s; valid_mdb s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_no_overlap ptr sz s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s; is_untyped_cap cap; is_untyped_cap (?cap32 s cap a b) \<longrightarrow> usable_untyped_range (?cap32 s cap a b) \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>S \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1}; range_cover ptr sz (obj_bits_api (APIType_map2 (Inr ao')) us) n; ao' = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; cap \<in> ran (null_filter (caps_of_state s)); valid_pspace s; valid_mdb s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_no_overlap ptr sz s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s; is_untyped_cap cap; usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us - 1} = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal:
No subgoals!