theory PageTableDuplicates

lemma valid_duplicates'_insert_ko:
  "\<lbrakk> vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us);
    vs_entry_align ko \<le> us;
    objBitsKO ko + us < 32;
    \<forall>x\<in> set (new_cap_addrs (2^us) ptr ko). m x = None \<rbrakk>
  \<Longrightarrow>  vs_valid_duplicates'
  (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (2^us) ptr ko) m)" apply (subst vs_valid_duplicates'_def) apply (clarsimp simp: vs_entry_align_def
                        foldr_upd_app_if[folded data_map_insert_def]) apply (clarsimp split:option.splits
         simp:foldr_upd_app_if[unfolded data_map_insert_def[symmetric]]) apply (rule conjI) apply clarsimp apply (case_tac ko, simp_all add:vs_ptr_align_def) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object, simp_all split: ARM_H.pte.splits) apply (drule(1) bspec)+ apply (drule_tac p' = y in new_cap_addrs_same_align_pdpt_bits) apply (simp add:vs_entry_align_def) apply (simp add:vs_ptr_align_def) apply (simp add:objBits_simps archObjSize_def pteBits_def)+ apply (clarsimp split: ARM_H.pde.splits simp:objBits_simps) apply (drule(1) bspec)+ apply (drule_tac p' = y in new_cap_addrs_same_align_pdpt_bits) apply (simp add:vs_entry_align_def) apply (simp add:vs_ptr_align_def) apply (simp add:objBits_simps archObjSize_def pdeBits_def)+ apply clarsimp apply (intro conjI impI allI) apply (drule(1) valid_duplicates'_D) apply fastforce apply (simp add:vs_ptr_align_def) apply simp apply (drule(2) valid_duplicates'_D) apply (clarsimp simp:vs_ptr_align_def
     split: Structures_H.kernel_object.splits
     ARM_H.pde.splits ARM_H.pte.splits
     arch_kernel_object.splits) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); vs_entry_align ko \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (2 ^ us) ptr ko) m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); vs_entry_align ko \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> \<forall>x y. case foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (2 ^ us) ptr ko) m x of None \<Rightarrow> True | Some koa \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align koa) = y && ~~ mask (vs_ptr_align koa) \<longrightarrow> foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (2 ^ us) ptr ko) m x = foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs (2 ^ us) ptr ko) m y proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> (x \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y. y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> Some ko = m y)) \<and> (x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y. (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (case m x of None \<Rightarrow> True | Some koa \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align koa) = y && ~~ mask (vs_ptr_align koa) \<longrightarrow> koa = ko)) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (case m x of None \<Rightarrow> True | Some ko \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> Some ko = m y)))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> (x \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y. y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> Some ko = m y)) \<and> (x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2) \<longrightarrow> Some x2 = m y))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y. y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> Some ko = m y)
 2. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr ko); y \<notin> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko)\<rbrakk> \<Longrightarrow> Some ko = m y
 2. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (2 subgoals):
 1. \<And>x y x8. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch x8) + us); (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE x \<Rightarrow> pte_align' x | KOPDE x \<Rightarrow> pde_align' x) \<le> us; objBitsKO (KOArch x8) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr (KOArch x8)). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch x8)); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch x8)); is_aligned y 2; x && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0); ko = KOArch x8\<rbrakk> \<Longrightarrow> Some (KOArch x8) = m y
 2. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (2 subgoals):
 1. \<And>x y arch_kernel_object. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch arch_kernel_object) + us); (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE x \<Rightarrow> pte_align' x | KOPDE x \<Rightarrow> pde_align' x) \<le> us; objBitsKO (KOArch arch_kernel_object) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr (KOArch arch_kernel_object)). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch arch_kernel_object)); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch arch_kernel_object)); is_aligned y 2; x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0); ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> Some (KOArch arch_kernel_object) = m y
 2. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (3 subgoals):
 1. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 2. \<And>x y arch_kernel_object x3. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPDE x3)) + us); (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0) \<le> us; objBitsKO (KOArch (KOPDE x3)) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); is_aligned y 2; x && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0) = y && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0); ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE x3)) = m y
 3. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (3 subgoals):
 1. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 2. \<And>x y arch_kernel_object x3. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPDE x3)) + us); (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0) \<le> us; objBitsKO (KOArch (KOPDE x3)) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); is_aligned y 2; x && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0) = y && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0); ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE x3)) = m y
 3. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (8 subgoals):
 1. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> vs_entry_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) \<le> us
 2. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))))
 3. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us)
 4. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> us < 30
 5. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned y 2
 6. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None; y \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 7. \<And>x y arch_kernel_object x3. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPDE x3)) + us); (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0) \<le> us; objBitsKO (KOArch (KOPDE x3)) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); is_aligned y 2; x && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0) = y && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0); ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE x3)) = m y
 8. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (7 subgoals):
 1. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))))
 2. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us)
 3. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> us < 30
 4. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned y 2
 5. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None; y \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 6. \<And>x y arch_kernel_object x3. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPDE x3)) + us); (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0) \<le> us; objBitsKO (KOArch (KOPDE x3)) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); is_aligned y 2; x && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0) = y && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0); ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE x3)) = m y
 7. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (6 subgoals):
 1. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us)
 2. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> us < 30
 3. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned y 2
 4. \<And>x y arch_kernel_object x2 x21 x22 x23 x24 x25. \<lbrakk>objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); arch_kernel_object = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) + us); x2 = ARM_H.LargePagePTE x21 x22 x23 x24 x25; 4 \<le> us; m x = None; y \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 5. \<And>x y arch_kernel_object x3. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO (KOArch (KOPDE x3)) + us); (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0) \<le> us; objBitsKO (KOArch (KOPDE x3)) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); is_aligned y 2; x && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0) = y && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0); ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE x3)) = m y
 6. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (2 subgoals):
 1. \<And>x y arch_kernel_object x3. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0) \<le> us; pdeBits + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE x3))); is_aligned y 2; x && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0) = y && ~~ mask (case x3 of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 6 | _ \<Rightarrow> 0); ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE x3)) = m y
 2. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (2 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))). m x = None; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y
 2. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (2 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; x \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y
 2. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (7 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> vs_entry_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) \<le> us
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) + us)
 4. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> us < 30
 5. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned y 2
 6. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None; y \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y
 7. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (6 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) + us)
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> us < 30
 4. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned y 2
 5. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None; y \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y
 6. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (5 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) + us)
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> us < 30
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None\<rbrakk> \<Longrightarrow> is_aligned y 2
 4. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>pdeBits + us < 32; y \<notin> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))); is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; ko = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); vs_valid_duplicates' m; is_aligned ptr (pdeBits + us); 4 \<le> us; m x = None; y \<in> set (new_cap_addrs (2 ^ us) ptr (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y
 5. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr (objBitsKO ko + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; objBitsKO ko + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None\<rbrakk> \<Longrightarrow> x \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> (\<forall>y x2. m x = Some x2 \<longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y)) proof (prove)
goal (1 subgoal):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2\<rbrakk> \<Longrightarrow> (y \<in> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = ko) \<and> (y \<notin> set (new_cap_addrs (2 ^ us) ptr ko) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = m y) proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<in> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x2 = ko
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<notin> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> Some x2 = m y proof (prove)
goal (4 subgoals):
 1. \<And>x y x2. \<lbrakk>is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<in> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> is_aligned (?p'115 x y x2) 2
 2. \<And>x y x2. \<lbrakk>is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<in> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = ?p'115 x y x2 && ~~ mask (vs_ptr_align x2)
 3. \<And>x y x2. \<lbrakk>is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<in> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); m (?p'115 x y x2) = Some x2\<rbrakk> \<Longrightarrow> x2 = ko
 4. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<notin> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> Some x2 = m y proof (prove)
goal (3 subgoals):
 1. \<And>x y x2. \<lbrakk>is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<in> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)
 2. \<And>x y x2. \<lbrakk>is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<in> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); m y = Some x2\<rbrakk> \<Longrightarrow> x2 = ko
 3. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<notin> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> Some x2 = m y proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<in> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); m y = Some x2\<rbrakk> \<Longrightarrow> x2 = ko
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<notin> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> Some x2 = m y proof (prove)
goal (1 subgoal):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<notin> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> Some x2 = m y proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<notin> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)
 2. \<And>x y x2. \<lbrakk>is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<notin> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); m y = Some x2\<rbrakk> \<Longrightarrow> Some x2 = m y proof (prove)
goal (1 subgoal):
 1. \<And>x y x2. \<lbrakk>is_aligned ptr ((case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) \<le> us; (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) + us < 32; \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr ko). m x = None; x \<notin> set (new_cap_addrs (2 ^ us) ptr ko); m x = Some x2; y \<notin> set (new_cap_addrs (2 ^ us) ptr ko); is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); m y = Some x2\<rbrakk> \<Longrightarrow> Some x2 = m y proof (prove)
goal:
No subgoals!