theory Untyped_AI

lemma retype_region_obj_ref_range:
  "\<lbrakk> \<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev\<lbrace>\<lambda>rv. Q r\<rbrace> \<rbrakk>
  \<Longrightarrow>
   \<lbrace>(\<lambda>s. \<forall>r \<in> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}. P r s) and K (range_cover ptr sz (obj_bits_api ty us) n)\<rbrace>
     retype_region ptr n us ty dev
   \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. \<forall>r \<in> obj_refs (default_cap tp x us dev). Q r s\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_strengthen_post) apply (rule hoare_vcg_conj_lift [OF retype_region_ret, simplified]) apply (rule hoare_vcg_const_Ball_lift) apply assumption apply (clarsimp) apply (drule subsetD[OF obj_refs_default_cap]) apply (drule_tac x = r in  bspec) apply (simp add: ptr_add_def) apply (drule(1) range_cover_mem) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>) \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>r\<in>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}. P r s) and K (range_cover ptr sz (obj_bits_api ty us) n)\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>r\<in>obj_refs (default_cap tp x us dev). Q r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>r\<in>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}. P r s\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. \<forall>r\<in>obj_refs (default_cap tp x us dev). Q r s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>r\<in>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}. P r s\<rbrace> retype_region ptr n us ty dev \<lbrace>?Q2\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; ?Q2 rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. \<forall>r\<in>obj_refs (default_cap tp x us dev). Q r s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>r\<in>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}. P r s\<rbrace> retype_region ptr n us ty dev \<lbrace>?Q'5\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n] \<and> ?Q'5 rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. \<forall>r\<in>obj_refs (default_cap tp x us dev). Q r s proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; r \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>?Q8 r\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n] \<and> (\<forall>x\<in>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}. ?Q8 x rv s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. \<forall>r\<in>obj_refs (default_cap tp x us dev). Q r s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n] \<and> (\<forall>x\<in>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}. Q x s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set rv. \<forall>r\<in>obj_refs (default_cap tp x us dev). Q r s proof (prove)
goal (1 subgoal):
 1. \<And>s x r. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; \<forall>x\<in>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}. Q x s; x < n; r \<in> obj_refs (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev)\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>s x r. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; \<forall>x\<in>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}. Q x s; x < n; r \<in> {ptr_add ptr (x * 2 ^ obj_bits_api ty us)}\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>s x r. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; x < n; r \<in> {ptr_add ptr (x * 2 ^ obj_bits_api ty us)}\<rbrakk> \<Longrightarrow> r \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>s x r. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; x < n; r \<in> {ptr_add ptr (x * 2 ^ obj_bits_api ty us)}; Q r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; x < n; r = ptr + word_of_nat x * 2 ^ obj_bits_api ty us\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<and> ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1
 2. \<And>s x r. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; x < n; r \<in> {ptr_add ptr (x * 2 ^ obj_bits_api ty us)}; Q r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; r = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<and> ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1
 2. \<And>s x r. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; x < n; r \<in> {ptr_add ptr (x * 2 ^ obj_bits_api ty us)}; Q r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>s x r. \<lbrakk>\<And>r. \<lbrace>P r\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. Q r\<rbrace>; range_cover ptr sz (obj_bits_api ty us) n; x < n; r \<in> {ptr_add ptr (x * 2 ^ obj_bits_api ty us)}; Q r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal:
No subgoals!