theory Retype_AC

lemma use_retype_region_proofs_ext':
  assumes x: "\<And>(s::det_ext state). \<lbrakk> retype_region_proofs s ty us ptr sz n dev; P s \<rbrakk>
                                      \<Longrightarrow> Q (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>)"
  assumes y: "\<And>xs. \<lbrace>Q xs and R xs\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. Q xs\<rbrace>"
  assumes z: "\<And>f xs s. R xs (kheap_update f s) = R xs s"
  shows
    "\<lbrakk> ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s \<rbrakk>
       \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace s \<and> valid_mdb s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and>
                caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} s \<and>
                caps_no_overlap ptr sz s \<and> pspace_no_overlap_range_cover 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>
                P s \<and> R (retype_addrs ptr ty n us) s\<rbrace>
           retype_region ptr n us ty dev \<lbrace>Q\<rbrace>" apply (simp add: retype_region_def split del: if_split) apply (rule hoare_pre, (wp | simp)+) apply (rule retype_region_ext_kheap_update[OF y]) apply (wp | simp)+ apply (clarsimp simp: retype_addrs_fold
                        foldr_upd_app_if fun_upd_def[symmetric]) apply safe apply (rule x) apply (rule retype_region_proofs.intro, simp_all)[1] apply (fastforce simp: range_cover_def obj_bits_api_def z slot_bits_def2 word_bits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 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> P s \<and> R (retype_addrs ptr ty n us) s\<rbrace> retype_region ptr n us ty dev \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 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>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) \<and> P s \<and> R (retype_addrs ptr ty n us) s\<rbrace> do y <- when (ty \<noteq> Untyped) (do kh <- gets kheap;
y <- retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) ty;
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object ty dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) kh))
od);
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n])
od \<lbrace>Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>kh. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?B7 kh\<rbrace> retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) ty \<lbrace>\<lambda>y s. Q (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) (s\<lparr>kheap := foldr (\<lambda>p kh a. if a = p then Some (default_object ty dev us) else kh a) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) kh\<rparr>)\<rbrace>
 2. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets kheap \<lbrace>?B7\<rbrace>
 3. \<And>s. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; 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>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) \<and> P s \<and> R (retype_addrs ptr ty n us) s\<rbrakk> \<Longrightarrow> (if ty \<noteq> Untyped then ?Q6 else Q (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n])) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets kheap \<lbrace>\<lambda>kh s. Q (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) (s\<lparr>kheap := foldr (\<lambda>p kh a. if a = p then Some (default_object ty dev us) else kh a) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) kh\<rparr>) \<and> R (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) (s\<lparr>kheap := foldr (\<lambda>p kh a. if a = p then Some (default_object ty dev us) else kh a) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) kh\<rparr>)\<rbrace>
 2. \<And>s. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; 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>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) \<and> P s \<and> R (retype_addrs ptr ty n us) s\<rbrakk> \<Longrightarrow> (if ty \<noteq> Untyped then ?Q6 else Q (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n])) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; 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>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) \<and> P s \<and> R (retype_addrs ptr ty n us) s\<rbrakk> \<Longrightarrow> (ty \<noteq> Untyped \<longrightarrow> Q (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) (s\<lparr>kheap := foldr (\<lambda>p kh a. if a = p then Some (default_object ty dev us) else kh a) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) (kheap s)\<rparr>) \<and> R (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) (s\<lparr>kheap := foldr (\<lambda>p kh a. if a = p then Some (default_object ty dev us) else kh a) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) (kheap s)\<rparr>)) \<and> (ty = Untyped \<longrightarrow> Q (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Untyped us)) [0..<n]) s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api ty us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr ty n us) s\<rbrakk> \<Longrightarrow> (ty \<noteq> Untyped \<longrightarrow> Q (retype_addrs ptr ty n us) (s\<lparr>kheap := \<lambda>a. if a \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s a\<rparr>) \<and> R (retype_addrs ptr ty n us) (s\<lparr>kheap := \<lambda>a. if a \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s a\<rparr>)) \<and> (ty = Untyped \<longrightarrow> Q (retype_addrs ptr Untyped n us) s) proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api ty us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> Q (retype_addrs ptr ty n us) (s\<lparr>kheap := \<lambda>a. if a \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s a\<rparr>)
 2. \<And>s a b. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api ty us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> R (retype_addrs ptr ty n us) (s\<lparr>kheap := \<lambda>a. if a \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s a\<rparr>)
 3. \<And>s a b. \<lbrakk>Untyped = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr Untyped n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api Untyped us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api Untyped us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr Untyped n us) s; ty = Untyped\<rbrakk> \<Longrightarrow> Q (retype_addrs ptr Untyped n us) s proof (prove)
goal (4 subgoals):
 1. \<And>s a b. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api ty us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> retype_region_proofs s ty us ptr sz n dev
 2. \<And>s a b. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api ty us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> P s
 3. \<And>s a b. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api ty us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> R (retype_addrs ptr ty n us) (s\<lparr>kheap := \<lambda>a. if a \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s a\<rparr>)
 4. \<And>s a b. \<lbrakk>Untyped = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr Untyped n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api Untyped us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api Untyped us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr Untyped n us) s; ty = Untyped\<rbrakk> \<Longrightarrow> Q (retype_addrs ptr Untyped n us) s proof (prove)
goal (5 subgoals):
 1. \<And>s a b. \<lbrakk>0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr CapTableObject n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api CapTableObject us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api CapTableObject us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr CapTableObject n us) s; ty = CapTableObject\<rbrakk> \<Longrightarrow> us < word_bits - cte_level_bits
 2. \<And>s a b. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api ty us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> \<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
 3. \<And>s a b. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api ty us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> P s
 4. \<And>s a b. \<lbrakk>ty = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api ty us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr ty n us) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> R (retype_addrs ptr ty n us) (s\<lparr>kheap := \<lambda>a. if a \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s a\<rparr>)
 5. \<And>s a b. \<lbrakk>Untyped = CapTableObject \<Longrightarrow> 0 < us; \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr Untyped n us) s; valid_pspace s; valid_mdb s; range_cover ptr sz (obj_bits_api Untyped us) n; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api Untyped us - 1} s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area 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; P s; R (retype_addrs ptr Untyped n us) s; ty = Untyped\<rbrakk> \<Longrightarrow> Q (retype_addrs ptr Untyped n us) s proof (prove)
goal:
No subgoals!