theory Retype_C

lemma createObject_child:
  "\<lbrace>\<lambda>s.
     is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and>
     {ptr .. ptr + (2^APIType_capBits ty us) - 1} \<subseteq> (untypedRange cap) \<and> isUntypedCap cap
   \<rbrace> createObject ty ptr us dev
   \<lbrace>\<lambda>rv s. sameRegionAs cap rv\<rbrace>" apply (rule hoare_assume_pre) apply (simp add:createObject_def3) apply wp apply (rule hoare_strengthen_post[OF createNewCaps_range_helper[where sz = "APIType_capBits ty us"]]) prefer 2 apply (fastforce simp:range_cover_full) apply clarsimp apply (drule_tac x = ptr in spec) apply (case_tac "capfn ptr"; clarsimp simp: capUntypedPtr_def sameRegionAs_def Let_def isCap_simps) apply (rename_tac arch_capability d v0 v1 f) apply (case_tac arch_capability;
         simp add: ARM_H.capUntypedSize_def ptBits_def pteBits_def pdBits_def pdeBits_def add.commute;
         (simp add: is_aligned_no_wrap')?) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>rv s. global.sameRegionAs cap rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>rv s. global.sameRegionAs cap rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv s. global.sameRegionAs cap rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap \<Longrightarrow> \<lbrace>?Q4\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>m a. global.sameRegionAs cap (hd m)\<rbrace>
 2. \<And>s. \<lbrakk>is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap; True\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap; \<exists>capfn. rv = map capfn (map (\<lambda>p. More_Word_Operations.ptr_add ptr (p * 2 ^ APIType_capBits ty us)) [0..<Suc 0]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap (hd rv)
 2. \<And>s. \<lbrakk>is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap; True\<rbrakk> \<Longrightarrow> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<and> 0 < Suc 0 proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap; True\<rbrakk> \<Longrightarrow> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<and> 0 < Suc 0
 2. \<And>rv s. \<lbrakk>is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap; \<exists>capfn. rv = map capfn (map (\<lambda>p. More_Word_Operations.ptr_add ptr (p * 2 ^ APIType_capBits ty us)) [0..<Suc 0]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap (hd rv) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap \<and> isUntypedCap cap; \<exists>capfn. rv = map capfn (map (\<lambda>p. More_Word_Operations.ptr_add ptr (p * 2 ^ APIType_capBits ty us)) [0..<Suc 0]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us)\<rbrakk> \<Longrightarrow> global.sameRegionAs cap (hd rv) proof (prove)
goal (1 subgoal):
 1. \<And>capfn. \<lbrakk>is_aligned ptr (APIType_capBits ty us); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; APIType_capBits ty us < word_bits; {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> global.sameRegionAs cap (capfn ptr) proof (prove)
goal (1 subgoal):
 1. \<And>capfn. \<lbrakk>is_aligned ptr (APIType_capBits ty us); APIType_capBits ty us < word_bits; {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<subseteq> untypedRange cap; isUntypedCap cap; capClass (capfn ptr) = PhysicalClass \<and> global.capUntypedPtr (capfn ptr) = ptr \<and> capBits (capfn ptr) = APIType_capBits ty us\<rbrakk> \<Longrightarrow> global.sameRegionAs cap (capfn ptr) proof (prove)
goal (1 subgoal):
 1. \<And>capfn x8 d v0 v1 f. \<lbrakk>is_aligned (Arch.capUntypedPtr x8) (APIType_capBits ty us); APIType_capBits ty us < word_bits; capfn (Arch.capUntypedPtr x8) = capability.ArchObjectCap x8; cap = capability.UntypedCap d v0 v1 f; acapClass x8 = PhysicalClass; acapBits x8 = APIType_capBits ty us; ptr = Arch.capUntypedPtr x8; v0 \<le> Arch.capUntypedPtr x8; Arch.capUntypedPtr x8 + 2 ^ APIType_capBits ty us - 1 \<le> v0 + 2 ^ v1 - 1\<rbrakk> \<Longrightarrow> Arch.capUntypedPtr x8 + Arch.capUntypedSize x8 - 1 \<le> v0 + 2 ^ v1 - 1 \<and> Arch.capUntypedPtr x8 \<le> Arch.capUntypedPtr x8 + Arch.capUntypedSize x8 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>capfn arch_capability d v0 v1 f. \<lbrakk>is_aligned (Arch.capUntypedPtr arch_capability) (APIType_capBits ty us); APIType_capBits ty us < word_bits; capfn (Arch.capUntypedPtr arch_capability) = capability.ArchObjectCap arch_capability; cap = capability.UntypedCap d v0 v1 f; acapClass arch_capability = PhysicalClass; acapBits arch_capability = APIType_capBits ty us; ptr = Arch.capUntypedPtr arch_capability; v0 \<le> Arch.capUntypedPtr arch_capability; Arch.capUntypedPtr arch_capability + 2 ^ APIType_capBits ty us - 1 \<le> v0 + 2 ^ v1 - 1\<rbrakk> \<Longrightarrow> Arch.capUntypedPtr arch_capability + Arch.capUntypedSize arch_capability - 1 \<le> v0 + 2 ^ v1 - 1 \<and> Arch.capUntypedPtr arch_capability \<le> Arch.capUntypedPtr arch_capability + Arch.capUntypedSize arch_capability - 1 proof (prove)
goal:
No subgoals!