theory ArchArch_AI

lemma retype_region_no_cap_to_obj:
  "\<lbrace>valid_pspace and valid_mdb
             and caps_overlap_reserved {ptr..ptr + 2 ^ obj_bits_api ty us - 1}
             and caps_no_overlap ptr sz
             and pspace_no_overlap_range_cover ptr sz
             and no_cap_to_obj_with_diff_ref cap S
             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 = Structures_A.CapTableObject \<longrightarrow> 0 < us)
             and K (range_cover ptr sz (obj_bits_api ty us) 1) \<rbrace>
     retype_region ptr 1 us ty dev
   \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>" apply (rule hoare_gen_asm)+ apply (simp add: no_cap_to_obj_with_diff_ref_null_filter) apply (wp retype_region_caps_of | simp)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace and valid_mdb and caps_overlap_reserved {ptr..ptr + 2 ^ obj_bits_api ty us - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and no_cap_to_obj_with_diff_ref cap S 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) 1)\<rbrace> retype_region ptr 1 us ty dev \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) 1; ty = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>valid_pspace and valid_mdb and caps_overlap_reserved {ptr..ptr + 2 ^ obj_bits_api ty us - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and no_cap_to_obj_with_diff_ref cap S 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 1 us ty dev \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) (Suc 0); ty = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>valid_pspace and valid_mdb and caps_overlap_reserved {ptr..ptr + 2 ^ obj_bits_api ty us - 1} and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and (\<lambda>s. \<forall>c\<in>ran (null_filter (caps_of_state s) |` (- S)). obj_refs c = obj_refs cap \<longrightarrow> table_cap_ref c = table_cap_ref cap) 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 (Suc 0) us ty dev \<lbrace>\<lambda>rv s. \<forall>c\<in>ran (null_filter (caps_of_state s) |` (- S)). obj_refs c = obj_refs cap \<longrightarrow> table_cap_ref c = table_cap_ref cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) (Suc 0); ty = CapTableObject \<longrightarrow> 0 < us; valid_pspace s \<and> valid_mdb s \<and> caps_overlap_reserved {ptr..ptr + 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> (\<forall>c\<in>ran (null_filter (caps_of_state s) |` (- S)). obj_refs c = obj_refs cap \<longrightarrow> table_cap_ref c = table_cap_ref cap) \<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)\<rbrakk> \<Longrightarrow> range_cover ptr ?sz5 (obj_bits_api ty us) (Suc 0) \<and> caps_no_overlap ptr ?sz5 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz5) s \<and> (\<exists>a b. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz5 \<subseteq> cap_range c \<and> cap_is_device c = dev) (a, b) s) proof (prove)
goal:
No subgoals!