theory Untyped_DR

lemma retype_transform_obj_ref_in_untyped_range:
  notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff
  shows "\<lbrakk>y \<in> set (retype_addrs ptr type n us);
  range_cover ptr sz (obj_bits_api type us) n\<rbrakk>
  \<Longrightarrow> retype_transform_obj_ref type us y \<subseteq>
  {ptr &&~~ mask sz ..(ptr && ~~ mask sz) + (2 ^ sz - 1)}" apply (frule retype_addrs_subset_ptr_bits) apply (clarsimp simp:retype_transform_obj_ref_def) apply (rule conjI) apply (drule(1) set_mp) apply clarsimp apply (erule set_mp[rotated]) apply (frule(1) retype_addrs_range_subset) apply (simp add:obj_bits_api_def) apply (erule subset_trans) apply (clarsimp simp: atLeastatMost_subset_iff field_simps) apply (rule word_and_le2) apply clarsimp apply (erule set_mp[rotated]) apply (erule subset_trans) apply (clarsimp simp: atLeastatMost_subset_iff field_simps) apply (rule word_and_le2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n\<rbrakk> \<Longrightarrow> retype_transform_obj_ref type us y \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> retype_transform_obj_ref type us y \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> (type = apiobject_type.Untyped \<longrightarrow> {y..y + 2 ^ us - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)}) \<and> (type \<noteq> apiobject_type.Untyped \<longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type = apiobject_type.Untyped \<longrightarrow> {y..y + 2 ^ us - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)}
 2. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; y \<in> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type = apiobject_type.Untyped \<longrightarrow> {y..y + 2 ^ us - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)}
 2. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; y \<in> up_aligned_area ptr sz; type = apiobject_type.Untyped; x \<in> {y..y + 2 ^ us - 1}\<rbrakk> \<Longrightarrow> x \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)}
 2. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; y \<in> up_aligned_area ptr sz; type = apiobject_type.Untyped\<rbrakk> \<Longrightarrow> {y..y + 2 ^ us - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)}
 2. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; y \<in> up_aligned_area ptr sz; type = apiobject_type.Untyped; {y..y + 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {y..y + 2 ^ us - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)}
 2. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); range_cover ptr sz us n; y \<in> up_aligned_area ptr sz; type = apiobject_type.Untyped; {y..y + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {y..y + 2 ^ us - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)}
 2. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); range_cover ptr sz us n; y \<in> up_aligned_area ptr sz; type = apiobject_type.Untyped\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)}
 2. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); range_cover ptr sz us n; y \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; type = apiobject_type.Untyped; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> ptr
 2. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> set (retype_addrs ptr type n us); range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz; type \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> y \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api type us) n; set (retype_addrs ptr type n us) \<subseteq> up_aligned_area ptr sz; type \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> set (retype_addrs ptr type n us) \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api type us) n; type \<noteq> apiobject_type.Untyped\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api type us) n; type \<noteq> apiobject_type.Untyped; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> ptr proof (prove)
goal:
No subgoals!