theory Retype_AC

lemma retype_region_ret_is_subject:
  "\<lbrace>K (range_cover ptr sz (obj_bits_api tp us) num_objects \<and>
       (\<forall>x\<in>{ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)}. is_subject aag x))\<rbrace>
   retype_region ptr num_objects us tp dev
   \<lbrace>\<lambda>rv. K (\<forall>ref \<in> set rv. is_subject aag ref)\<rbrace>" apply (rule hoare_gen_asm2 | rule hoare_gen_asm)+ apply (rule hoare_strengthen_post) apply (rule retype_region_ret) apply (simp only: K_def) apply (rule ballI) apply (elim conjE) apply (erule bspec) apply (rule rev_subsetD, assumption) apply (simp add: p_assoc_help del: set_map) apply (rule retype_addrs_subset_ptr_bits[simplified retype_addrs_def]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (range_cover ptr sz (obj_bits_api tp us) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x))\<rbrace> retype_region ptr num_objects us tp dev \<lbrace>\<lambda>rv. K (\<forall>ref\<in>set rv. is_subject aag ref)\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api tp us) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> retype_region ptr num_objects us tp dev \<lbrace>\<lambda>rv. K (\<forall>ref\<in>set rv. is_subject aag ref)\<rbrace> proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (obj_bits_api tp us) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> retype_region ptr num_objects us tp dev \<lbrace>?Q2\<rbrace>
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); ?Q2 rv s\<rbrakk> \<Longrightarrow> K (\<forall>ref\<in>set rv. is_subject aag ref) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]\<rbrakk> \<Longrightarrow> K (\<forall>ref\<in>set rv. is_subject aag ref) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]\<rbrakk> \<Longrightarrow> \<forall>ref\<in>set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]). is_subject aag ref proof (prove)
goal (1 subgoal):
 1. \<And>rv s ref. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) num_objects \<and> (\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x); rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]; ref \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects])\<rbrakk> \<Longrightarrow> is_subject aag ref proof (prove)
goal (1 subgoal):
 1. \<And>rv s ref. \<lbrakk>rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]; ref \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]); range_cover ptr sz (obj_bits_api tp us) num_objects; \<forall>x\<in>up_aligned_area ptr sz. is_subject aag x\<rbrakk> \<Longrightarrow> is_subject aag ref proof (prove)
goal (1 subgoal):
 1. \<And>rv s ref. \<lbrakk>rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]; ref \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]); range_cover ptr sz (obj_bits_api tp us) num_objects\<rbrakk> \<Longrightarrow> ref \<in> up_aligned_area ptr sz proof (prove)
goal (1 subgoal):
 1. \<And>rv s ref. \<lbrakk>rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]; ref \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]); range_cover ptr sz (obj_bits_api tp us) num_objects\<rbrakk> \<Longrightarrow> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]) \<subseteq> up_aligned_area ptr sz proof (prove)
goal (1 subgoal):
 1. \<And>rv ref. \<lbrakk>rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]; ref \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]); range_cover ptr sz (obj_bits_api tp us) num_objects\<rbrakk> \<Longrightarrow> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]) \<subseteq> up_aligned_area ptr sz proof (prove)
goal (1 subgoal):
 1. \<And>rv ref. \<lbrakk>rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]; ref \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<num_objects]); range_cover ptr sz (obj_bits_api tp us) num_objects\<rbrakk> \<Longrightarrow> range_cover ptr sz (obj_bits_api tp us) num_objects proof (prove)
goal:
No subgoals!