theory Untyped_R

lemma createNewCaps_children:
  "\<lbrace>\<lambda>s. cap = UntypedCap d (ptr && ~~ mask sz) sz idx
     \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrace>
     createNewCaps tp ptr n us d
   \<lbrace>\<lambda>rv s. \<forall>y \<in> set rv. (sameRegionAs cap y)\<rbrace>" apply (rule hoare_assume_pre) apply (rule hoare_chain [OF createNewCaps_range_helper2]) apply fastforce apply clarsimp apply (drule(1) bspec) apply (clarsimp simp: sameRegionAs_def3 isCap_simps) apply (drule(1) subsetD) apply clarsimp apply (erule order_trans[rotated]) apply (rule word_and_le2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrace> createNewCaps tp ptr n us d \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. global.sameRegionAs cap y\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n \<Longrightarrow> \<lbrace>\<lambda>s. cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrace> createNewCaps tp ptr n us d \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. global.sameRegionAs cap y\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n; cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrakk> \<Longrightarrow> range_cover ptr (?sz3 s) (APIType_capBits tp us) n \<and> 0 < n
 2. \<And>s rv sa. \<lbrakk>cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n; \<forall>cp\<in>set rv. capRange cp \<noteq> {} \<and> capRange cp \<subseteq> {ptr..(ptr && ~~ mask (?sz3 s)) + 2 ^ ?sz3 s - 1}\<rbrakk> \<Longrightarrow> \<forall>y\<in>set rv. global.sameRegionAs cap y proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx \<and> range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n; \<forall>cp\<in>set rv. capRange cp \<noteq> {} \<and> capRange cp \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> \<forall>y\<in>set rv. global.sameRegionAs cap y proof (prove)
goal (1 subgoal):
 1. \<And>rv x. \<lbrakk>\<forall>cp\<in>set rv. capRange cp \<noteq> {} \<and> capRange cp \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; x \<in> set rv; cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; range_cover ptr sz (APIType_capBits tp us) n; 0 < n\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x proof (prove)
goal (1 subgoal):
 1. \<And>rv x. \<lbrakk>x \<in> set rv; cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; range_cover ptr sz (APIType_capBits tp us) n; 0 < n; capRange x \<noteq> {} \<and> capRange x \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.UntypedCap d (ptr && ~~ mask sz) sz idx) x proof (prove)
goal (1 subgoal):
 1. \<And>rv x xa. \<lbrakk>x \<in> set rv; cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; range_cover ptr sz (APIType_capBits tp us) n; 0 < n; xa \<in> capRange x; capRange x \<noteq> {}; capRange x \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> xa \<and> xa \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>rv x xa. \<lbrakk>x \<in> set rv; cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; range_cover ptr sz (APIType_capBits tp us) n; 0 < n; xa \<in> capRange x; capRange x \<noteq> {}; xa \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> xa \<and> xa \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>rv x xa. \<lbrakk>x \<in> set rv; cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; range_cover ptr sz (APIType_capBits tp us) n; 0 < n; xa \<in> capRange x; capRange x \<noteq> {}; ptr \<le> xa; xa \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> xa proof (prove)
goal (1 subgoal):
 1. \<And>rv x xa. \<lbrakk>x \<in> set rv; cap = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; range_cover ptr sz (APIType_capBits tp us) n; 0 < n; xa \<in> capRange x; capRange x \<noteq> {}; xa \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> ptr proof (prove)
goal:
No subgoals!