theory ArchRetype_AI

lemma copy_global_equal_kernel_mappings_restricted:
  "is_aligned pd pd_bits \<Longrightarrow>
   \<lbrace>\<lambda>s. equal_kernel_mappings (s \<lparr> kheap := restrict_map (kheap s) (- (insert pd S)) \<rparr>)
              \<and> arm_global_pd (arch_state s) \<notin> (insert pd S)
              \<and> pspace_aligned s \<and> valid_arch_state s\<rbrace>
     copy_global_mappings pd
   \<lbrace>\<lambda>rv s. equal_kernel_mappings (s \<lparr> kheap := restrict_map (kheap s) (- S) \<rparr>)\<rbrace>" apply (simp add: copy_global_mappings_def) apply (rule hoare_seq_ext [OF _ gets_sp]) apply (rule hoare_chain) apply (rule hoare_vcg_conj_lift) apply (rule_tac P="global_pd \<notin> (insert pd S)" in hoare_vcg_prop) apply (rule_tac P="is_aligned global_pd pd_bits"
           in hoare_gen_asm(1)) apply (rule_tac S="insert pd S" in mapM_x_store_pde_eq_kernel_mappings_restr) apply clarsimp apply (erule order_le_less_trans) apply (simp add: pd_bits_def pageBits_def) apply (clarsimp simp: invs_aligned_pdD) apply clarsimp apply (frule_tac x="kernel_base >> 20" in spec) apply (drule mp) apply (simp add: kernel_base_def pd_bits_def pageBits_def) apply (clarsimp simp: obj_at_def) apply (subst equal_kernel_mappings_specific_def) apply (fastforce simp add: obj_at_def restrict_map_def) apply (subst(asm) equal_kernel_mappings_specific_def) apply (fastforce simp add: obj_at_def restrict_map_def) apply (clarsimp simp: restrict_map_def obj_at_def) apply (drule_tac x="ucast w" in spec, drule mp) apply (clarsimp simp: kernel_mapping_slots_def) apply (rule conjI) apply (simp add: word_le_nat_alt unat_ucast_kernel_base_rshift) apply (simp only: unat_ucast, subst mod_less) apply (rule order_less_le_trans, rule unat_lt2p) apply simp apply simp apply (rule word_le_minus_one_leq) apply (rule order_less_le_trans, rule ucast_less) apply simp apply (simp add: pd_bits_def pageBits_def) apply (simp add: ucast_down_ucast_id word_size source_size_def
                   target_size_def is_down_def) apply (drule_tac x=p' in spec) apply (simp split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<notin> insert pd S \<and> pspace_aligned s \<and> valid_arch_state s\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<noteq> pd \<and> arm_global_pd (arch_state s) \<notin> S \<and> pspace_aligned s \<and> valid_arch_state s\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]
od \<lbrace>\<lambda>rv s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>(\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<noteq> pd \<and> arm_global_pd (arch_state s) \<notin> S \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>rv s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?P4 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>?Q4 global_pd\<rbrace>
 2. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<noteq> pd \<and> arm_global_pd (arch_state s) \<notin> S \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> ?P4 global_pd s
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ?Q4 global_pd rv s\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?P8 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>?Q8 global_pd\<rbrace>
 2. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?P'8 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>?Q'8 global_pd\<rbrace>
 3. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<noteq> pd \<and> arm_global_pd (arch_state s) \<notin> S \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> ?P8 global_pd s \<and> ?P'8 global_pd s
 4. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; ?Q8 global_pd rv s \<and> ?Q'8 global_pd rv s\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>global_pd. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>?P'8 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>?Q'8 global_pd\<rbrace>
 2. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<noteq> pd \<and> arm_global_pd (arch_state s) \<notin> S \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> global_pd \<notin> insert pd S \<and> ?P'8 global_pd s
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; global_pd \<notin> insert pd S \<and> ?Q'8 global_pd rv s\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>global_pd. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>?P'12 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>?Q'8 global_pd\<rbrace>
 2. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<noteq> pd \<and> arm_global_pd (arch_state s) \<notin> S \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> global_pd \<notin> insert pd S \<and> (?P'12 global_pd and K (is_aligned global_pd pd_bits)) s
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; global_pd \<notin> insert pd S \<and> ?Q'8 global_pd rv s\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>global_pd. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits\<rbrakk> \<Longrightarrow> pd \<in> insert pd S \<and> is_aligned pd pd_bits \<and> is_aligned global_pd pd_bits \<and> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<subseteq> {..<2 ^ (pd_bits - 2)}
 2. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<noteq> pd \<and> arm_global_pd (arch_state s) \<notin> S \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> global_pd \<notin> insert pd S \<and> ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>)) and K (is_aligned global_pd pd_bits)) s
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; global_pd \<notin> insert pd S \<and> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> (\<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]. \<exists>pdv pdv'. ako_at (PageDirectory pdv) pd s \<and> ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits; kernel_base >> 20 \<le> x; x \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> x < 2 ^ (pd_bits - 2)
 2. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<noteq> pd \<and> arm_global_pd (arch_state s) \<notin> S \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> global_pd \<notin> insert pd S \<and> ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>)) and K (is_aligned global_pd pd_bits)) s
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; global_pd \<notin> insert pd S \<and> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> (\<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]. \<exists>pdv pdv'. ako_at (PageDirectory pdv) pd s \<and> ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned pd pd_bits; is_aligned global_pd pd_bits; kernel_base >> 20 \<le> x\<rbrakk> \<Longrightarrow> 2 ^ (pd_bits - 2) - 1 < 2 ^ (pd_bits - 2)
 2. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<noteq> pd \<and> arm_global_pd (arch_state s) \<notin> S \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> global_pd \<notin> insert pd S \<and> ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>)) and K (is_aligned global_pd pd_bits)) s
 3. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; global_pd \<notin> insert pd S \<and> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> (\<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]. \<exists>pdv pdv'. ako_at (PageDirectory pdv) pd s \<and> ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> arm_global_pd (arch_state s) \<noteq> pd \<and> arm_global_pd (arch_state s) \<notin> S \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = global_pd)) s\<rbrakk> \<Longrightarrow> global_pd \<notin> insert pd S \<and> ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>)) and K (is_aligned global_pd pd_bits)) s
 2. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; global_pd \<notin> insert pd S \<and> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> (\<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]. \<exists>pdv pdv'. ako_at (PageDirectory pdv) pd s \<and> ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>global_pd rv s. \<lbrakk>is_aligned pd pd_bits; global_pd \<notin> insert pd S \<and> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<and> (\<forall>x\<in>set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]. \<exists>pdv pdv'. ako_at (PageDirectory pdv) pd s \<and> ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> (\<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> (\<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))); kernel_base >> 20 \<le> kernel_base >> 20 \<and> kernel_base >> 20 \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> (\<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20))))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> (\<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x)))\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> kernel_base >> 20 \<and> kernel_base >> 20 \<le> 2 ^ (pd_bits - 2) - 1
 2. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> (\<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))); \<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>global_pd s. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> (\<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x))); \<exists>pdv. ako_at (PageDirectory pdv) pd s \<and> (\<exists>pdv'. ako_at (PageDirectory pdv') global_pd s \<and> pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>global_pd s pdv pdv'. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>global_pd s pdv pdv'. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20))\<rbrakk> \<Longrightarrow> ako_at (PageDirectory (?pd71 global_pd s pdv pdv')) (?p71 global_pd s pdv pdv') (s\<lparr>kheap := kheap s |` (- S)\<rparr>)
 2. \<And>global_pd s pdv pdv'. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20))\<rbrakk> \<Longrightarrow> \<forall>p' pd'. ako_at (PageDirectory pd') p' (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = ?pd71 global_pd s pdv pdv' w) proof (prove)
goal (1 subgoal):
 1. \<And>global_pd s pdv pdv'. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20))\<rbrakk> \<Longrightarrow> \<forall>p' pd'. ako_at (PageDirectory pd') p' (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w) proof (prove)
goal (2 subgoals):
 1. \<And>global_pd s pdv pdv'. \<lbrakk>\<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S\<rbrakk> \<Longrightarrow> ako_at (PageDirectory (?pd83 global_pd s pdv pdv')) (?p83 global_pd s pdv pdv') (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>)
 2. \<And>global_pd s pdv pdv'. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. ako_at (PageDirectory pd') p' (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = ?pd83 global_pd s pdv pdv' w); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20))\<rbrakk> \<Longrightarrow> \<forall>p' pd'. ako_at (PageDirectory pd') p' (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w) proof (prove)
goal (1 subgoal):
 1. \<And>global_pd s pdv pdv'. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. ako_at (PageDirectory pd') p' (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20))\<rbrakk> \<Longrightarrow> \<forall>p' pd'. ako_at (PageDirectory pd') p' (s\<lparr>kheap := kheap s |` (- S)\<rparr>) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w) proof (prove)
goal (1 subgoal):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); \<forall>x. kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1 \<longrightarrow> pdv (UCAST(32 \<rightarrow> 12) x) = pdv' (UCAST(32 \<rightarrow> 12) x); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (2 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) w \<and> UCAST(12 \<rightarrow> 32) w \<le> 2 ^ (pd_bits - 2) - 1
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (2 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) w \<and> UCAST(12 \<rightarrow> 32) w \<le> 2 ^ (pd_bits - 2) - 1
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (3 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) w
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) w \<le> 2 ^ (pd_bits - 2) - 1
 3. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (3 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w. unat (kernel_base >> 20) \<le> unat w \<longrightarrow> pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); unat (kernel_base >> 20) \<le> unat w\<rbrakk> \<Longrightarrow> unat (kernel_base >> 20) \<le> unat (UCAST(12 \<rightarrow> 32) w)
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) w \<le> 2 ^ (pd_bits - 2) - 1
 3. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (4 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w. unat (kernel_base >> 20) \<le> unat w \<longrightarrow> pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); unat (kernel_base >> 20) \<le> unat w\<rbrakk> \<Longrightarrow> unat w < 2 ^ LENGTH(32)
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w. unat (kernel_base >> 20) \<le> unat w \<longrightarrow> pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); unat (kernel_base >> 20) \<le> unat w\<rbrakk> \<Longrightarrow> unat (kernel_base >> 20) \<le> unat w
 3. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) w \<le> 2 ^ (pd_bits - 2) - 1
 4. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (4 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w. unat (kernel_base >> 20) \<le> unat w \<longrightarrow> pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); unat (kernel_base >> 20) \<le> unat w\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(12) \<le> 2 ^ LENGTH(32)
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w. unat (kernel_base >> 20) \<le> unat w \<longrightarrow> pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); unat (kernel_base >> 20) \<le> unat w\<rbrakk> \<Longrightarrow> unat (kernel_base >> 20) \<le> unat w
 3. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) w \<le> 2 ^ (pd_bits - 2) - 1
 4. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (3 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w. unat (kernel_base >> 20) \<le> unat w \<longrightarrow> pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); unat (kernel_base >> 20) \<le> unat w\<rbrakk> \<Longrightarrow> unat (kernel_base >> 20) \<le> unat w
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) w \<le> 2 ^ (pd_bits - 2) - 1
 3. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (2 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) w \<le> 2 ^ (pd_bits - 2) - 1
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (2 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) w < 2 ^ (pd_bits - 2)
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (3 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> LENGTH(12) < LENGTH(32)
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(12) \<le> 2 ^ (pd_bits - 2)
 3. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (2 subgoals):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<ge>UCAST(32 \<rightarrow> 12) (kernel_base >> 20). pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> w\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(12) \<le> 2 ^ (pd_bits - 2)
 2. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (1 subgoal):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w)) = pdv' (UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) w))\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (1 subgoal):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; \<forall>p' pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w); kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv w = pdv' w\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal (1 subgoal):
 1. \<And>global_pd s pdv pdv' p' pd' w. \<lbrakk>is_aligned pd pd_bits; global_pd \<noteq> pd; global_pd \<notin> S; kheap s pd = Some (ArchObj (PageDirectory pdv)); kheap s global_pd = Some (ArchObj (PageDirectory pdv')); pdv (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) = pdv' (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)); p' \<notin> S; kheap s p' = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots; pdv w = pdv' w; \<forall>pd'. (if p' \<noteq> pd \<and> p' \<notin> S then kheap s p' else None) = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pdv' w)\<rbrakk> \<Longrightarrow> pd' w = pdv' w proof (prove)
goal:
No subgoals!