theory Retype_AC

lemma retype_region_pas_refined:
  "\<lbrace>pas_refined aag and invs and pas_cur_domain aag and
    caps_overlap_reserved {ptr..ptr + of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and
    caps_no_overlap ptr sz and pspace_no_overlap_range_cover ptr sz and
    (\<lambda>s. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) sl s) and
    K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and
    K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) and
    K ((type = CapTableObject \<longrightarrow> 0 < o_bits))\<rbrace>
   retype_region ptr num_objects o_bits type dev
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (rule use_retype_region_proofs_ext'[where P = "invs and pas_refined aag"]) apply clarsimp apply (erule (2) retype_region_proofs'_pas_refined[OF retype_region_proofs'.intro]) apply (wp retype_region_ext_pas_refined) apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) sl s) and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) and K (type = CapTableObject \<longrightarrow> 0 < o_bits)\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. type = CapTableObject \<longrightarrow> 0 < o_bits \<Longrightarrow> \<lbrace>pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) sl s) and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x)\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. type = CapTableObject \<longrightarrow> 0 < o_bits \<Longrightarrow> \<lbrace>?Q2\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) sl s) and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x)) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; retype_region_proofs s type o_bits ptr ?sz5 num_objects dev; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr type num_objects o_bits) then Some (default_object type dev o_bits) else kheap s x\<rparr>)
 2. \<And>xs. type = CapTableObject \<longrightarrow> 0 < o_bits \<Longrightarrow> \<lbrace>pas_refined aag and ?R5 xs\<rbrace> retype_region_ext xs type \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>f xs s. type = CapTableObject \<longrightarrow> 0 < o_bits \<Longrightarrow> ?R5 xs (kheap_update f s) = ?R5 xs s
 4. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 5. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) sl s) and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x)) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz5 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz5 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz5) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz5 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> ?R5 (retype_addrs ptr type num_objects o_bits) s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; retype_region_proofs s type o_bits ptr ?sz5 num_objects dev; invs s; pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr type num_objects o_bits) then Some (default_object type dev o_bits) else kheap s x\<rparr>)
 2. \<And>xs. type = CapTableObject \<longrightarrow> 0 < o_bits \<Longrightarrow> \<lbrace>pas_refined aag and ?R5 xs\<rbrace> retype_region_ext xs type \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>f xs s. type = CapTableObject \<longrightarrow> 0 < o_bits \<Longrightarrow> ?R5 xs (kheap_update f s) = ?R5 xs s
 4. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 5. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 6. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) sl s) and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x)) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz5 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz5 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz5) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz5 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> ?R5 (retype_addrs ptr type num_objects o_bits) s proof (prove)
goal (5 subgoals):
 1. \<And>xs. type = CapTableObject \<longrightarrow> 0 < o_bits \<Longrightarrow> \<lbrace>pas_refined aag and ?R5 xs\<rbrace> retype_region_ext xs type \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>f xs s. type = CapTableObject \<longrightarrow> 0 < o_bits \<Longrightarrow> ?R5 xs (kheap_update f s) = ?R5 xs s
 3. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 4. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 5. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) sl s) and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x)) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz5 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz5 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz5) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz5 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> ?R5 (retype_addrs ptr type num_objects o_bits) s proof (prove)
goal (5 subgoals):
 1. \<And>xs s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (pas_refined aag and ?R5 xs) s\<rbrakk> \<Longrightarrow> (pas_refined aag and pas_cur_domain aag and K (\<forall>x\<in>set xs. is_subject aag x)) s
 2. \<And>f xs s. type = CapTableObject \<longrightarrow> 0 < o_bits \<Longrightarrow> ?R5 xs (kheap_update f s) = ?R5 xs s
 3. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 4. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 5. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) sl s) and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x)) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz5 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz5 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz5) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz5 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> ?R5 (retype_addrs ptr type num_objects o_bits) s proof (prove)
goal (4 subgoals):
 1. \<And>f xs s. type = CapTableObject \<longrightarrow> 0 < o_bits \<Longrightarrow> (pas_cur_domain aag (kheap_update f s) \<and> (\<forall>x\<in>set xs. is_subject aag x)) = (pas_cur_domain aag s \<and> (\<forall>x\<in>set xs. is_subject aag x))
 2. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; type = CapTableObject\<rbrakk> \<Longrightarrow> 0 < o_bits
 3. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (invs and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<And>s. \<lbrakk>type = CapTableObject \<longrightarrow> 0 < o_bits; (pas_refined aag and invs and pas_cur_domain aag and caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<exists>sl. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) sl s) and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x)) s\<rbrakk> \<Longrightarrow> valid_pspace s \<and> valid_mdb s \<and> range_cover ptr ?sz5 (obj_bits_api type o_bits) num_objects \<and> caps_overlap_reserved {ptr..ptr + word_of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1} s \<and> caps_no_overlap ptr ?sz5 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz5) s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz5 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> (invs and pas_refined aag) s \<and> pas_cur_domain aag s \<and> (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) proof (prove)
goal:
No subgoals!