theory ArchVSpace_AI

lemma store_pde_invs_unmap':
  "\<lbrace>invs
    and (\<exists>\<rhd> (p && ~~ mask pd_bits))
    and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs (Inr (pde, slots))) slot s)
    and (\<lambda>s. \<exists>ptr cap. caps_of_state s ptr = Some cap
                    \<and> is_pg_cap cap
                    \<and> same_refs (Inr (pde, slots)) cap s)
    and valid_pde pde
    and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s)
    and K (wellformed_pde pde \<and> pde_ref pde = None)
    and K (ucast (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots
           \<and> (\<exists>xs. slots = p # xs) )
    and (\<lambda>s. \<exists>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s)\<rbrace>
   store_pde p pde
   \<lbrace>\<lambda>_. invs\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: store_pde_def | wp)+ apply (rule_tac T ="  Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory))
                        ` set_option (pde_ref (pd (ucast (p && mask pd_bits >> 2))))"
                and T'="  Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory))
                        ` set_option (pde_ref_pages (pd (ucast (p && mask pd_bits >> 2))))"
                and S'="  Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory))
                        ` set_option (pde_ref_pages pde)" in set_pd_invs_unmap') apply wp apply (clarsimp simp: obj_at_def) apply (rule conjI) apply (clarsimp simp add: invs_def valid_state_def valid_pspace_def
                             valid_objs_def valid_obj_def dom_def) apply (erule_tac P="\<lambda>x. (\<exists>y. a y x) \<longrightarrow> b x" for a b in allE[where x="(p && ~~ mask pd_bits)"]) apply (erule impE) apply (clarsimp simp: obj_at_def vs_refs_def)+ apply (rule conjI) apply (clarsimp simp add: invs_def valid_state_def valid_vspace_objs_def) apply (erule_tac P="\<lambda>x. (\<exists>y. a y x) \<longrightarrow> b x" for a b in allE[where x="(p && ~~ mask pd_bits)"]) apply (erule impE) apply (erule_tac x=ref in exI) apply (erule_tac x="PageDirectory pd" in allE) apply (clarsimp simp: obj_at_def) apply (rule conjI) apply (safe)[1] apply (clarsimp simp add: vs_refs_def graph_of_def split: if_split_asm) apply (rule pair_imageI) apply (clarsimp) apply (clarsimp simp: vs_refs_def graph_of_def split: if_split_asm) apply (subst (asm) ucast_ucast_mask_shift_helper[symmetric], simp) apply (clarsimp simp: vs_refs_def graph_of_def split: if_split_asm) apply (rule_tac x="(ac, bc)" in image_eqI) apply clarsimp apply (clarsimp simp: ucast_ucast_mask_shift_helper) apply (rule conjI) apply safe[1] apply (clarsimp simp: vs_refs_pages_def graph_of_def
                            ucast_ucast_mask_shift_helper
                      split: if_split_asm) apply (rule_tac x="(ac, bc)" in image_eqI) apply clarsimp apply clarsimp apply (clarsimp simp: vs_refs_pages_def graph_of_def ucast_ucast_id
                     split: if_split_asm) apply (clarsimp simp: vs_refs_pages_def graph_of_def
                    split: if_split_asm) apply (rule_tac x="(ac,bc)" in image_eqI) apply clarsimp apply (clarsimp simp: ucast_ucast_mask_shift_helper) apply (clarsimp simp: vs_refs_pages_def graph_of_def) apply (rule_tac x="(ucast (p && mask pd_bits >> 2), x)" in image_eqI) apply (clarsimp simp: ucast_ucast_mask_shift_helper) apply clarsimp apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def) apply (drule same_refs_rD) apply (clarsimp split: list.splits) apply blast apply (drule same_refs_rD) apply clarsimp apply (drule spec, drule (2) mp[OF _ vs_lookup_vs_lookup_pagesI]) apply ((clarsimp simp: invs_def valid_state_def valid_arch_state_def)+)[2] apply (rule_tac x=aa in exI, rule_tac x=ba in exI, rule_tac x=cap in exI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs (Inr (pde, slots))) slot s) and (\<lambda>s. \<exists>ptr cap. caps_of_state s ptr = Some cap \<and> is_pg_cap cap \<and> same_refs (Inr (pde, slots)) cap s) and valid_pde pde and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s) and K (wellformed_pde pde \<and> pde_ref pde = None) and K (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<and> (\<exists>xs. slots = p # xs)) and (\<lambda>s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s)\<rbrace> store_pde p pde \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs (Inr (pde, slots))) slot s) and (\<lambda>s. \<exists>ptr cap. caps_of_state s ptr = Some cap \<and> is_pg_cap cap \<and> same_refs (Inr (pde, slots)) cap s) and valid_pde pde and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s) and K (wellformed_pde pde \<and> pde_ref pde = None) and K (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<and> (\<exists>xs. slots = p # xs)) and (\<lambda>s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> store_pde p pde \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s ref a b aa ba cap xs pd x. \<lbrakk>invs s; (ref \<rhd> (p && ~~ mask pd_bits)) s; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) s; valid_pde pde s; caps_of_state s (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs s; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap s; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B25 s ref a b aa ba cap xs pd x\<rbrace> set_pd (p && ~~ mask pd_bits) (x(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>s ref a b aa ba cap xs pd. \<lbrakk>invs s; (ref \<rhd> (p && ~~ mask pd_bits)) s; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) s; valid_pde pde s; caps_of_state s (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs s; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap s; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 s ref a b aa ba cap xs pd\<rbrace> get_pd (p && ~~ mask pd_bits) \<lbrace>?B25 s ref a b aa ba cap xs pd\<rbrace>
 3. \<And>s ref a b aa ba cap xs pd sa. \<lbrakk>invs s; (ref \<rhd> (p && ~~ mask pd_bits)) s; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) s; valid_pde pde s; caps_of_state s (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs s; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap s; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; s = sa\<rbrakk> \<Longrightarrow> ?Q24 s ref a b aa ba cap xs pd sa proof (prove)
goal (2 subgoals):
 1. \<And>s ref a b aa ba cap xs pd. \<lbrakk>invs s; (ref \<rhd> (p && ~~ mask pd_bits)) s; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) s; valid_pde pde s; caps_of_state s (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs s; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap s; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 s ref a b aa ba cap xs pd\<rbrace> get_pd (p && ~~ mask pd_bits) \<lbrace>\<lambda>x. invs and (\<lambda>s. \<forall>i. wellformed_pde ((x(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> valid_vspace_obj (PageDirectory (x(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))) s) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (x(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs ko - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))))) (p && ~~ mask pd_bits) and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (x(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages ko - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde)) (p && ~~ mask pd_bits) and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>xa\<in>kernel_mapping_slots. (x(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) xa = pd' xa)) (p && ~~ mask pd_bits) and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s) and (\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) and (\<lambda>s. \<forall>(a, b)\<in>Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)))\<rbrace>
 2. \<And>s ref a b aa ba cap xs pd sa. \<lbrakk>invs s; (ref \<rhd> (p && ~~ mask pd_bits)) s; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) s; valid_pde pde s; caps_of_state s (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs s; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap s; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; s = sa\<rbrakk> \<Longrightarrow> ?Q24 s ref a b aa ba cap xs pd sa proof (prove)
goal (1 subgoal):
 1. \<And>s ref a b aa ba cap xs pd sa. \<lbrakk>invs s; (ref \<rhd> (p && ~~ mask pd_bits)) s; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) s; valid_pde pde s; caps_of_state s (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs s; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap s; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; s = sa\<rbrakk> \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (p && ~~ mask pd_bits) sa \<longrightarrow> (invs and (\<lambda>s. \<forall>i. wellformed_pde ((pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<longrightarrow> valid_vspace_obj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))) s) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs ko - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))))) (p && ~~ mask pd_bits) and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages ko - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde)) (p && ~~ mask pd_bits) and obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. (pda(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x = pd' x)) (p && ~~ mask pd_bits) and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s) and (\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) and (\<lambda>s. \<forall>(a, b)\<in>Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) s \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref)))) sa proof (prove)
goal (1 subgoal):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<forall>i. i \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> wellformed_pde (pd i)) \<and> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) sa)) \<and> vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>i. i \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> wellformed_pde (pd i)
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) sa)) \<and> vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa i. \<lbrakk>(ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); \<forall>ptr. (\<exists>y. kheap sa ptr = Some y) \<longrightarrow> (\<exists>obj. kheap sa ptr = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs sa | TCB t \<Rightarrow> valid_tcb ptr t sa | Endpoint p \<Rightarrow> valid_ep p sa | Notification p \<Rightarrow> valid_ntfn p sa | ArchObj ao \<Rightarrow> arch_valid_obj ao sa)); pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa); valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; i \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> wellformed_pde (pd i)
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) sa)) \<and> vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa i. \<lbrakk>(ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa); valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; i \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); (\<exists>y. kheap sa (p && ~~ mask pd_bits) = Some y) \<longrightarrow> (\<exists>obj. kheap sa (p && ~~ mask pd_bits) = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs sa | TCB t \<Rightarrow> valid_tcb (p && ~~ mask pd_bits) t sa | Endpoint p \<Rightarrow> valid_ep p sa | Notification p \<Rightarrow> valid_ntfn p sa | ArchObj ao \<Rightarrow> arch_valid_obj ao sa))\<rbrakk> \<Longrightarrow> wellformed_pde (pd i)
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) sa)) \<and> vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (3 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa i. \<lbrakk>(ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa); valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; i \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> \<exists>y. kheap sa (p && ~~ mask pd_bits) = Some y
 2. \<And>ref a b aa ba cap xs pd sa i. \<lbrakk>(ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pspace_aligned sa; pspace_distinct sa; if_live_then_nonz_cap sa; zombies_final sa; sym_refs (state_refs_of sa); sym_refs (state_hyp_refs_of sa); valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_machine_state sa; valid_vspace_objs sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; i \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); \<exists>obj. kheap sa (p && ~~ mask pd_bits) = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs sa | TCB t \<Rightarrow> valid_tcb (p && ~~ mask pd_bits) t sa | Endpoint p \<Rightarrow> valid_ep p sa | Notification p \<Rightarrow> valid_ntfn p sa | ArchObj ao \<Rightarrow> arch_valid_obj ao sa)\<rbrakk> \<Longrightarrow> wellformed_pde (pd i)
 3. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) sa)) \<and> vs_refs (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (1 subgoal):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) sa)) \<and> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) sa)
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>(ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); valid_pspace sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_machine_state sa; \<forall>p. (\<exists>rs. (rs \<rhd> p) sa) \<longrightarrow> (\<forall>ao. ako_at ao p sa \<longrightarrow> valid_vspace_obj ao sa); valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; x \<notin> kernel_mapping_slots; (refa \<rhd> (p && ~~ mask pd_bits)) sa; x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> valid_pde (pd x) sa
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>(ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); valid_pspace sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_machine_state sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; x \<notin> kernel_mapping_slots; (refa \<rhd> (p && ~~ mask pd_bits)) sa; x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); (\<exists>y. (y \<rhd> (p && ~~ mask pd_bits)) sa) \<longrightarrow> (\<forall>ao. ako_at ao (p && ~~ mask pd_bits) sa \<longrightarrow> valid_vspace_obj ao sa)\<rbrakk> \<Longrightarrow> valid_pde (pd x) sa
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (3 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>(ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); valid_pspace sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_machine_state sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; x \<notin> kernel_mapping_slots; (refa \<rhd> (p && ~~ mask pd_bits)) sa; x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)\<rbrakk> \<Longrightarrow> \<exists>y. (y \<rhd> (p && ~~ mask pd_bits)) sa
 2. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>(ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); valid_pspace sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_machine_state sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; x \<notin> kernel_mapping_slots; (refa \<rhd> (p && ~~ mask pd_bits)) sa; x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); \<forall>ao. ako_at ao (p && ~~ mask pd_bits) sa \<longrightarrow> valid_vspace_obj ao sa\<rbrakk> \<Longrightarrow> valid_pde (pd x) sa
 3. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>(ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); valid_pspace sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_machine_state sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; x \<notin> kernel_mapping_slots; (refa \<rhd> (p && ~~ mask pd_bits)) sa; x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); \<forall>ao. ako_at ao (p && ~~ mask pd_bits) sa \<longrightarrow> valid_vspace_obj ao sa\<rbrakk> \<Longrightarrow> valid_pde (pd x) sa
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>(ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); valid_pspace sa; valid_mdb sa; valid_ioc sa; valid_idle sa; only_idle sa; if_unsafe_then_cap sa; valid_reply_caps sa; valid_reply_masters sa; valid_global_refs sa; valid_arch_state sa; valid_irq_node sa; valid_irq_handlers sa; valid_irq_states sa; valid_machine_state sa; valid_arch_caps sa; valid_global_objs sa; valid_kernel_mappings sa; equal_kernel_mappings sa; valid_asid_map sa; valid_global_vspace_mappings sa; pspace_in_kernel_window sa; cap_refs_in_kernel_window sa; pspace_respects_device_region sa; cap_refs_respects_device_region sa; cur_tcb sa; x \<notin> kernel_mapping_slots; (refa \<rhd> (p && ~~ mask pd_bits)) sa; x \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); ako_at (PageDirectory pd) (p && ~~ mask pd_bits) sa \<longrightarrow> valid_vspace_obj (PageDirectory pd) sa\<rbrakk> \<Longrightarrow> valid_pde (pd x) sa
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (1 subgoal):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<and> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))))
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (4 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ab bb ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ac, bc) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x))\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))
 2. \<And>ref a b aa ba cap xs pd sa ab bb ac bc x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ac, x) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)); pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) = Some x; UCAST(12 \<rightarrow> 32) ac = p && mask pd_bits >> 2\<rbrakk> \<Longrightarrow> False
 3. \<And>ref a b aa ba cap xs pd sa ab bb ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); (ac, bc) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x))
 4. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (4 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); ac \<notin> kernel_mapping_slots; ac \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) = Some y}
 2. \<And>ref a b aa ba cap xs pd sa ab bb ac bc x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ac, x) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)); pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) = Some x; UCAST(12 \<rightarrow> 32) ac = p && mask pd_bits >> 2\<rbrakk> \<Longrightarrow> False
 3. \<And>ref a b aa ba cap xs pd sa ab bb ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); (ac, bc) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x))
 4. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (4 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); ac \<notin> kernel_mapping_slots; ac \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (ac, bc) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) = Some y}
 2. \<And>ref a b aa ba cap xs pd sa ab bb ac bc x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ac, x) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)); pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) = Some x; UCAST(12 \<rightarrow> 32) ac = p && mask pd_bits >> 2\<rbrakk> \<Longrightarrow> False
 3. \<And>ref a b aa ba cap xs pd sa ab bb ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); (ac, bc) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x))
 4. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (3 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ab bb ac bc x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ac, x) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)); pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) = Some x; UCAST(12 \<rightarrow> 32) ac = p && mask pd_bits >> 2\<rbrakk> \<Longrightarrow> False
 2. \<And>ref a b aa ba cap xs pd sa ab bb ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); (ac, bc) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x))
 3. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (3 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac x. \<lbrakk>pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) = Some x; UCAST(12 \<rightarrow> 32) ac = p && mask pd_bits >> 2; invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); ac \<notin> kernel_mapping_slots; ac \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref (pd ac) = Some x\<rbrakk> \<Longrightarrow> False
 2. \<And>ref a b aa ba cap xs pd sa ab bb ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); (ac, bc) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x))
 3. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ab bb ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); (ac, bc) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x))
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); ac \<notin> kernel_mapping_slots; pde_ref (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = Some y}
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (3 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); ac \<notin> kernel_mapping_slots; pde_ref (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) = (case (ac, bc) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); ac \<notin> kernel_mapping_slots; pde_ref (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (ac, bc) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = Some y}
 3. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); ac \<notin> kernel_mapping_slots; pde_ref (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (ac, bc) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = Some y}
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (1 subgoal):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde) \<and> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) - Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))) \<union> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde)
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (5 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ab bb. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); (ab, bb) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde)\<rbrakk> \<Longrightarrow> (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory pd))
 2. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde); pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) = Some x\<rbrakk> \<Longrightarrow> False
 3. \<And>ref a b aa ba cap xs pd sa ab bb. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory pd)); (ab, bb) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))))\<rbrakk> \<Longrightarrow> (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 4. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 5. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (5 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde); ac \<notin> kernel_mapping_slots; ac \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref_pages (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) = Some y}
 2. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde); pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) = Some x\<rbrakk> \<Longrightarrow> False
 3. \<And>ref a b aa ba cap xs pd sa ab bb. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory pd)); (ab, bb) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))))\<rbrakk> \<Longrightarrow> (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 4. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 5. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (6 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde); ac \<notin> kernel_mapping_slots; ac \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref_pages (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) = (case (ac, bc) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde); ac \<notin> kernel_mapping_slots; ac \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref_pages (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (ac, bc) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) = Some y}
 3. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde); pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) = Some x\<rbrakk> \<Longrightarrow> False
 4. \<And>ref a b aa ba cap xs pd sa ab bb. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory pd)); (ab, bb) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))))\<rbrakk> \<Longrightarrow> (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 5. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 6. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (5 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde); ac \<notin> kernel_mapping_slots; ac \<noteq> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2); pde_ref_pages (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (ac, bc) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) = Some y}
 2. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde); pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) = Some x\<rbrakk> \<Longrightarrow> False
 3. \<And>ref a b aa ba cap xs pd sa ab bb. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory pd)); (ab, bb) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))))\<rbrakk> \<Longrightarrow> (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 4. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 5. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (4 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages pde); pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) = Some x\<rbrakk> \<Longrightarrow> False
 2. \<And>ref a b aa ba cap xs pd sa ab bb. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory pd)); (ab, bb) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))))\<rbrakk> \<Longrightarrow> (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 3. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 4. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (3 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ab bb. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory pd)); (ab, bb) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))))\<rbrakk> \<Longrightarrow> (ab, bb) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 2. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 3. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (3 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); ac \<notin> kernel_mapping_slots; pde_ref_pages (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = Some y}
 2. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 3. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (4 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); ac \<notin> kernel_mapping_slots; pde_ref_pages (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) = (case (ac, bc) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); ac \<notin> kernel_mapping_slots; pde_ref_pages (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (ac, bc) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = Some y}
 3. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 4. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (3 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ac bc. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (VSRef (UCAST(12 \<rightarrow> 32) ac) (Some APageDirectory), bc) \<notin> Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) ` set_option (pde_ref_pages (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)))); ac \<notin> kernel_mapping_slots; pde_ref_pages (pd ac) = Some bc\<rbrakk> \<Longrightarrow> (ac, bc) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = Some y}
 2. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 3. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa ab bb x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = Some y}
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (3 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (VSRef (p && mask pd_bits >> 2) (Some APageDirectory), x) = (case (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2), x) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>ref a b aa ba cap xs pd sa x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2), x) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = Some y}
 3. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa x. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2), x) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages ((pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)) x)) = Some y}
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (1 subgoal):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (\<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref)) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa capa y. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); caps_of_state sa (a, b) = Some capa; p && ~~ mask pd_bits \<in> obj_refs capa; (\<lambda>x. x && ~~ mask pd_bits) ` set xs \<subseteq> obj_refs capa; is_pd_cap capa; cap_asid capa = Some y\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref)) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa capa y. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); caps_of_state sa (a, b) = Some capa; p && ~~ mask pd_bits \<in> obj_refs capa; (\<lambda>x. x && ~~ mask pd_bits) ` set xs \<subseteq> obj_refs capa; is_pd_cap capa; cap_asid capa = Some y; (\<exists>p. pde_ref_pages pde = Some p \<and> p \<in> obj_refs cap) \<and> (\<forall>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref)) proof (prove)
goal (2 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa capa y pa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); caps_of_state sa (a, b) = Some capa; p && ~~ mask pd_bits \<in> obj_refs capa; (\<lambda>x. x && ~~ mask pd_bits) ` set xs \<subseteq> obj_refs capa; is_pd_cap capa; cap_asid capa = Some y; \<forall>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref); pde_ref_pages pde = Some pa; pa \<in> obj_refs cap\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> is_pd_cap cap \<and> p && ~~ mask pd_bits \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)
 2. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref)) proof (prove)
goal (1 subgoal):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; same_refs (Inr (pde, p # xs)) cap sa; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref)) proof (prove)
goal (1 subgoal):
 1. \<And>ref a b aa ba cap xs pd sa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); (\<exists>p. pde_ref_pages pde = Some p \<and> p \<in> obj_refs cap) \<and> (\<forall>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set_option (pde_ref_pages pde). \<forall>ref. (ref \<unrhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> (\<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref)) proof (prove)
goal (1 subgoal):
 1. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); \<forall>ref. (ref \<rhd> (p && ~~ mask pd_bits)) sa \<longrightarrow> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref); pde_ref_pages pde = Some x; x \<in> obj_refs cap; (refa \<unrhd> (p && ~~ mask pd_bits)) sa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # refa) proof (prove)
goal (3 subgoals):
 1. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x; x \<in> obj_refs cap; (refa \<unrhd> (p && ~~ mask pd_bits)) sa\<rbrakk> \<Longrightarrow> valid_vspace_objs sa
 2. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x; x \<in> obj_refs cap; (refa \<unrhd> (p && ~~ mask pd_bits)) sa\<rbrakk> \<Longrightarrow> valid_asid_table (asid_table sa) sa
 3. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x; x \<in> obj_refs cap; (refa \<unrhd> (p && ~~ mask pd_bits)) sa; vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # refa)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # refa) proof (prove)
goal (1 subgoal):
 1. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x; x \<in> obj_refs cap; (refa \<unrhd> (p && ~~ mask pd_bits)) sa; vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # refa)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state sa (a, b) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # refa) proof (prove)
goal (1 subgoal):
 1. \<And>ref a b aa ba cap xs pd sa x refa. \<lbrakk>invs sa; (ref \<rhd> (p && ~~ mask pd_bits)) sa; cte_wp_at (parent_for_refs (Inr (pde, p # xs))) (a, b) sa; valid_pde pde sa; caps_of_state sa (aa, ba) = Some cap; p && ~~ mask pd_bits \<notin> global_refs sa; is_pg_cap cap; wellformed_pde pde; pde_ref pde = None; UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; slots = p # xs; kheap sa (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pde_ref_pages pde = Some x; x \<in> obj_refs cap; (refa \<unrhd> (p && ~~ mask pd_bits)) sa; vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # refa)\<rbrakk> \<Longrightarrow> caps_of_state sa (aa, ba) = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # refa) proof (prove)
goal:
No subgoals!