theory Retype_AI

lemma retype_region_valid_cap:
  "\<lbrakk>ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> 0 < us\<rbrakk>
   \<Longrightarrow> \<lbrace>(\<lambda>s::'state_ext state. valid_pspace s \<and> caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} s \<and>
           valid_mdb s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and>
           caps_no_overlap ptr sz s \<and> pspace_no_overlap_range_cover ptr sz s  \<and>
           (\<exists>slot. cte_wp_at (\<lambda>c.  {ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)} \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and>
           s \<turnstile> cap) and K (untyped_range cap \<inter> {ptr..(ptr &&~~ mask sz) + 2 ^ sz - 1} = {})\<rbrace>
        retype_region ptr n us ty dev
      \<lbrace>\<lambda>r s. s \<turnstile> cap\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (rule use_retype_region_proofs) apply (erule retype_region_proofs_invs.valid_cap[OF retype_region_proofs_assms]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ty = CapTableObject \<Longrightarrow> 0 < us) \<Longrightarrow> \<lbrace>(\<lambda>s. valid_pspace s \<and> caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s \<and> valid_mdb s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> caps_no_overlap ptr sz s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> (\<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> s \<turnstile> cap) and K (untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {})\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>r s. s \<turnstile> cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace s \<and> caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s \<and> valid_mdb s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> caps_no_overlap ptr sz s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> (\<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> s \<turnstile> cap\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>r s. s \<turnstile> cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>r s. s \<turnstile> cap\<rbrace>
 2. \<And>s. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; valid_pspace s \<and> caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s \<and> valid_mdb s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> caps_no_overlap ptr sz s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> (\<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> s \<turnstile> cap\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; retype_region_proofs s ty us ptr ?sz5 n dev; s \<turnstile> cap\<rbrakk> \<Longrightarrow> s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> cap
 2. \<And>s f. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> trans_state f s \<turnstile> cap = s \<turnstile> cap
 3. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; ty = CapTableObject\<rbrakk> \<Longrightarrow> 0 < us
 4. \<And>s. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; valid_pspace s \<and> caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s \<and> valid_mdb s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> caps_no_overlap ptr sz s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> (\<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> s \<turnstile> cap\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz5 (obj_bits_api ty us) n \<and> caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s \<and> caps_no_overlap ptr ?sz5 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz5) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz5 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) \<and> s \<turnstile> cap proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; s \<turnstile> cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask ?sz5) + 2 ^ ?sz5 - 1} = {}
 2. \<And>s f. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> trans_state f s \<turnstile> cap = s \<turnstile> cap
 3. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; ty = CapTableObject\<rbrakk> \<Longrightarrow> 0 < us
 4. \<And>s. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; valid_pspace s \<and> caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s \<and> valid_mdb s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> caps_no_overlap ptr sz s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> (\<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> s \<turnstile> cap\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz5 (obj_bits_api ty us) n \<and> caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s \<and> caps_no_overlap ptr ?sz5 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz5) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz5 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) \<and> s \<turnstile> cap proof (prove)
goal:
No subgoals!