theory Retype_AI

lemma use_retype_region_proofs':
  assumes x: "\<And>s. \<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>x s f. Q x (trans_state f s) = Q x 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.  {ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)} \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s)
        \<and> P 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 add:y trans_state_update[symmetric] del: trans_state_update)+) 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 add: range_cover_def obj_bits_api_def
     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\<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\<rbrace> do y <- when (ty \<noteq> Untyped) (do kh <- gets kheap;
y <- do_extended_op (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 (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\<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> (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; P s; 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> (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> (ty = Untyped \<longrightarrow> Q (retype_addrs ptr Untyped n us) s) proof (prove)
goal (2 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; P s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) 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>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; P s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s; ty = Untyped\<rbrakk> \<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; P s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) 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; P s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> P s
 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; P s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s; ty = Untyped\<rbrakk> \<Longrightarrow> Q (retype_addrs ptr Untyped n us) s proof (prove)
goal (4 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; P s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) 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; P s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) 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; P s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> P s
 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; P s; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s; ty = Untyped\<rbrakk> \<Longrightarrow> Q (retype_addrs ptr Untyped n us) s proof (prove)
goal:
No subgoals!