theory Retype_R

lemma createNewCaps_urz:
  "\<lbrace>untyped_ranges_zero'
      and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz
      and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0) \<rbrace>
   createNewCaps ty ptr n us dev
   \<lbrace>\<lambda>archCaps. untyped_ranges_zero'\<rbrace>" apply (simp add: untyped_ranges_zero_inv_null_filter_cteCaps_of) apply (rule hoare_pre) apply (rule untyped_ranges_zero_lift) apply (wp createNewCaps_null_filter')+ apply (auto simp: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>archCaps. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. untyped_ranges_zero_inv (map_option cteCap \<circ> null_filter' (ctes_of s)) (gsUntypedZeroRanges s)) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>archCaps s. untyped_ranges_zero_inv (map_option cteCap \<circ> null_filter' (ctes_of s)) (gsUntypedZeroRanges s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>archCaps s. untyped_ranges_zero_inv (map_option cteCap \<circ> null_filter' (ctes_of s)) (gsUntypedZeroRanges s)\<rbrace>
 2. \<And>s. ((\<lambda>s. untyped_ranges_zero_inv (map_option cteCap \<circ> null_filter' (ctes_of s)) (gsUntypedZeroRanges s)) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (gsUntypedZeroRanges s)\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>archCaps s. P (gsUntypedZeroRanges s)\<rbrace>
 2. \<And>f. \<lbrace>?P3 f\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>archCaps s. untyped_ranges_zero_inv (map_option cteCap \<circ> null_filter' (ctes_of s)) f\<rbrace>
 3. \<And>s. ((\<lambda>s. untyped_ranges_zero_inv (map_option cteCap \<circ> null_filter' (ctes_of s)) (gsUntypedZeroRanges s)) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> ?P3 (gsUntypedZeroRanges s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. untyped_ranges_zero_inv (map_option cteCap \<circ> null_filter' (ctes_of s)) (gsUntypedZeroRanges s)) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> ((\<lambda>sa. untyped_ranges_zero_inv (map_option cteCap \<circ> null_filter' (ctes_of sa)) (gsUntypedZeroRanges s)) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (?sz12 (gsUntypedZeroRanges s)) and K (range_cover ptr (?sz12 (gsUntypedZeroRanges s)) (APIType_capBits ty us) n \<and> n \<noteq> 0)) s proof (prove)
goal:
No subgoals!