theory ArchVSpaceEntries_AI

lemma invoke_untyped_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs and invs and ct_active
          and valid_untyped_inv ui\<rbrace>
       invoke_untyped ui
   \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (rule hoare_pre, rule invoke_untyped_Q) apply (wp init_arch_objects_valid_pdpt | simp)+ apply (auto simp: post_retype_invs_def split: if_split_asm)[1] apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and ct_active and valid_untyped_inv ui\<rbrace> invoke_untyped ui \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tp sz cref slot oref reset ptr us slots dev. ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev \<Longrightarrow> \<lbrace>invs and (\<lambda>x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x) and cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_range (default_cap tp oref us dev) \<subseteq> untyped_range c \<and> {oref..oref + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) slot and cte_wp_at ((=) NullCap) cref and K (cref \<in> set slots \<and> oref \<in> set (retype_addrs ptr tp (length slots) us)) and K (range_cover ptr sz (obj_bits_api tp us) (length slots))\<rbrace> create_cap tp us slot dev (cref, oref) \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 2. \<And>tp slot reset sz slots ptr n us refs dev. ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev \<Longrightarrow> \<lbrace>(\<lambda>x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x) and post_retype_invs tp refs and cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot and K (refs = retype_addrs ptr tp n us \<and> range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> init_arch_objects tp ptr n us refs \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 3. \<And>ptr us tp slot reset sz slots dev. ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (\<forall>x\<in>ran (kheap x). obj_valid_pdpt x) \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 4. \<And>ptr sz idx cref dev. \<lbrace>\<lambda>x. (\<forall>x\<in>ran (kheap x). obj_valid_pdpt x) \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 5. \<lbrace>?Q'3\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 6. \<And>s. ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and ct_active and valid_untyped_inv ui) s \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'3 s) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (5 subgoals):
 1. \<And>tp slot reset sz slots ptr n us dev s. \<lbrakk>ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev; (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> post_retype_invs tp (retype_addrs ptr tp n us) s \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> range_cover ptr sz (obj_bits_api tp us) n\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_arch_state s \<and> (\<exists>usa. retype_addrs ptr tp n us = retype_addrs ptr tp n usa \<and> (\<exists>sz. range_cover ptr sz (obj_bits_api tp usa) n))
 2. \<And>ptr us tp slot reset sz slots dev. ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (\<forall>x\<in>ran (kheap x). obj_valid_pdpt x) \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 3. \<And>ptr sz idx cref dev. \<lbrace>\<lambda>x. (\<forall>x\<in>ran (kheap x). obj_valid_pdpt x) \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 4. \<lbrace>?Q'3\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 5. \<And>s. ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and ct_active and valid_untyped_inv ui) s \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'3 s) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_untyped_inv ui and ct_active) s proof (prove)
goal (4 subgoals):
 1. \<And>ptr us tp slot reset sz slots dev. ui = Retype slot reset (ptr && ~~ mask sz) ptr tp us slots dev \<Longrightarrow> \<lbrace>\<lambda>x. invs x \<and> (\<forall>x\<in>ran (kheap x). obj_valid_pdpt x) \<and> cte_wp_at (\<lambda>c. \<exists>idx. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot x \<and> pspace_no_overlap (up_aligned_area ptr sz) x \<and> range_cover ptr sz (obj_bits_api tp us) (length slots) \<and> (tp = CapTableObject \<longrightarrow> 0 < us) \<and> caps_overlap_reserved {ptr..ptr + word_of_nat (length slots * 2 ^ obj_bits_api tp us) - 1} x \<and> caps_no_overlap ptr sz x\<rbrace> retype_region ptr (length slots) us tp dev \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 2. \<And>ptr sz idx cref dev. \<lbrace>\<lambda>x. (\<forall>x\<in>ran (kheap x). obj_valid_pdpt x) \<and> invs x \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref x \<and> (case ui of Retype slot reset ptr' ptr tp us slots dev' \<Rightarrow> cref = slot \<and> dev' = dev) \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 3. \<lbrace>?Q'3\<rbrace> reset_untyped_cap (case ui of Retype src_slot x xa xb xc xd xe xf \<Rightarrow> src_slot) \<lbrace>\<lambda>rv x. \<forall>x\<in>ran (kheap x). obj_valid_pdpt x\<rbrace>
 4. \<And>s. ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and invs and ct_active and valid_untyped_inv ui) s \<Longrightarrow> (invs and (\<lambda>s. (case ui of Retype x reset xa xb xc xd xe xf \<Rightarrow> reset) \<longrightarrow> ?Q'3 s) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_untyped_inv ui and ct_active) s proof (prove)
goal:
No subgoals!