theory Untyped_AI

lemma retype_region_not_cte_wp_at:
  "\<lbrace>(\<lambda>s. \<not> cte_wp_at P p s) and valid_pspace and
     caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api tp us - 1} and
     valid_mdb and pspace_no_overlap_range_cover ptr sz and caps_no_overlap ptr sz and
     (\<lambda>s. \<exists>cref. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) cref s) and
     K (\<not> P cap.NullCap \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr sz (obj_bits_api tp us) n)\<rbrace>
     retype_region ptr n us tp dev
   \<lbrace>\<lambda>rv s. \<not> cte_wp_at P p s\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp: P_null_filter_caps_of_cte_wp_at[symmetric]) apply (wpsimp wp: retype_region_caps_of) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<not> cte_wp_at P p s) and valid_pspace and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} and valid_mdb and pspace_no_overlap (up_aligned_area ptr sz) and caps_no_overlap ptr sz and (\<lambda>s. \<exists>cref. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) cref s) and K (\<not> P NullCap \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. \<not> cte_wp_at P p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> P NullCap \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr sz (obj_bits_api tp us) n \<Longrightarrow> \<lbrace>(\<lambda>s. \<not> cte_wp_at P p s) and valid_pspace and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} and valid_mdb and pspace_no_overlap (up_aligned_area ptr sz) and caps_no_overlap ptr sz and (\<lambda>s. \<exists>cref. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) cref s)\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. \<not> cte_wp_at P p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P NullCap; tp = CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api tp us) n\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. null_filter (caps_of_state s) p = None \<or> \<not> P (the (null_filter (caps_of_state s) p))) and valid_pspace and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} and valid_mdb and pspace_no_overlap (up_aligned_area ptr sz) and caps_no_overlap ptr sz and (\<lambda>s. \<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)\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. null_filter (caps_of_state s) p = None \<or> \<not> P (the (null_filter (caps_of_state s) p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<not> P NullCap; tp = CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api tp us) n; null_filter (caps_of_state s) p = None \<or> \<not> P (the (null_filter (caps_of_state s) p)); valid_pspace s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; valid_mdb s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_no_overlap 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\<rbrakk> \<Longrightarrow> range_cover ptr ?sz6 (obj_bits_api tp us) n \<and> caps_no_overlap ptr ?sz6 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz6) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz6 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) proof (prove)
goal:
No subgoals!