theory Untyped_R

lemma createNewCaps_parent_helper:
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap d (ptr && ~~ mask sz) sz idx) p s
      \<and> pspace_aligned' s \<and> pspace_distinct' s
      \<and> pspace_no_overlap' ptr sz s
      \<and> (ty = APIObjectType ArchTypes_H.CapTableObject \<longrightarrow> 0 < us)
      \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<rbrace>
    createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and>
                       (\<forall>tup\<in>set (zip (xs rv) rv).
                                sameRegionAs (cteCap cte) (snd tup)))
    p\<rbrace>" apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<exists>cte. cte_wp_at' ((=) cte) p s
                                           \<and> isUntypedCap (cteCap cte)
                                           \<and> (\<forall>tup\<in>set (zip (xs rv) rv).
                                sameRegionAs (cteCap cte) (snd tup))"]) apply (clarsimp elim!: cte_wp_at_weakenE') apply (rule hoare_pre) apply (wp hoare_vcg_ex_lift createNewCaps_cte_wp_at'
            set_tuple_pick createNewCaps_children) apply (auto simp:cte_wp_at'_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (zip (xs rv) rv). global.sameRegionAs (cteCap cte) (snd tup))) p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<exists>cte. cte_wp_at' ((=) cte) p s \<and> isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (zip (xs rv) rv). global.sameRegionAs (cteCap cte) (snd tup)) \<Longrightarrow> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (zip (xs rv) rv). global.sameRegionAs (cteCap cte) (snd tup))) p s
 2. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<exists>cte. cte_wp_at' ((=) cte) p s \<and> isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (zip (xs rv) rv). global.sameRegionAs (cteCap cte) (snd tup))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<exists>cte. cte_wp_at' ((=) cte) p s \<and> isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (zip (xs rv) rv). global.sameRegionAs (cteCap cte) (snd tup))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q9\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<exists>cte. cte_wp_at' ((=) cte) p s \<and> isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (zip (xs rv) rv). global.sameRegionAs (cteCap cte) (snd tup))\<rbrace>
 2. \<And>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<Longrightarrow> ?Q9 s proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) p s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<Longrightarrow> \<exists>x. (cte_wp_at' ((=) x) p s \<and> range_cover ptr (?sz15 x) (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz15 x) s) \<and> isUntypedCap (cteCap x) \<and> cteCap x = capability.UntypedCap d (ptr && ~~ mask (?sz19 x)) (?sz19 x) (?idx19 x) \<and> range_cover ptr (?sz19 x) (APIType_capBits ty us) n \<and> 0 < n proof (prove)
goal:
No subgoals!