theory Retype_AI

lemma retype_region_post_retype_invs:
  "\<lbrace>(invs::'state_ext state \<Rightarrow> bool) and caps_no_overlap ptr sz and pspace_no_overlap_range_cover ptr sz
      and caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}
      and region_in_kernel_window {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}
      and (\<lambda>s. \<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 K (ty = Structures_A.CapTableObject \<longrightarrow> 0 < us)
      and K (range_cover ptr sz (obj_bits_api ty us) n) \<rbrace>
      retype_region ptr n us ty dev\<lbrace>\<lambda>rv. post_retype_invs ty rv\<rbrace>" apply (rule hoare_gen_asm)+ apply (rule hoare_pre,
         rule use_retype_region_proofs'[where sz = sz
      and P="invs and region_in_kernel_window {ptr .. (ptr &&~~ mask sz) + 2 ^ sz - 1}"]) apply (rule retype_region_proofs_invs.post_retype_invs
                  [OF retype_region_proofs_assms], simp+) apply (simp add: invs_post_retype_invs) apply (clarsimp simp:invs_def valid_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 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 (ty = CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr sz (obj_bits_api ty us) n)\<rbrace> retype_region ptr n us ty dev \<lbrace>post_retype_invs ty\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 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 ty dev \<lbrace>post_retype_invs ty\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty = CapTableObject \<longrightarrow> 0 < us; retype_region_proofs s ty us ptr sz n dev; (invs and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}) s\<rbrakk> \<Longrightarrow> post_retype_invs ty (retype_addrs ptr ty n us) (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>)
 2. \<And>x s f. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> post_retype_invs ty x (trans_state f s) = post_retype_invs ty x s
 3. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty = CapTableObject \<longrightarrow> 0 < us; ty = CapTableObject\<rbrakk> \<Longrightarrow> 0 < us
 4. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> (invs and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}) s \<longrightarrow> post_retype_invs ty (retype_addrs ptr ty n us) s
 5. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty = CapTableObject \<longrightarrow> 0 < us; (invs and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 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)) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr sz (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 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> (invs and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> invs s \<and> region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s \<longrightarrow> post_retype_invs ty (retype_addrs ptr ty n us) s
 2. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty = CapTableObject \<longrightarrow> 0 < us; (invs and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 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)) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr sz (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 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> (invs and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty = CapTableObject \<longrightarrow> 0 < us; (invs and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 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)) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr sz (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 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> (invs and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}) s proof (prove)
goal:
No subgoals!