theory PageTableDuplicates

lemma placeASIDPool_valid_duplicates'[wp]:
  notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
  shows "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr pageBits s
   \<and> is_aligned ptr pageBits \<and> pspace_aligned' s\<rbrace>
  placeNewObject' ptr (KOArch (KOASIDPool makeObject)) 0
  \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add:placeNewObject'_def) apply (wp unless_wp | wpc |
    simp add:alignError_def split_def)+ apply (subgoal_tac "vs_valid_duplicates' (\<lambda>a. if a = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s a)") apply fastforce apply (subst vs_valid_duplicates'_def) apply (clarsimp simp: vs_entry_align_def
         foldr_upd_app_if[unfolded data_map_insert_def[symmetric]]) apply (clarsimp split:option.splits
         simp:foldr_upd_app_if[unfolded data_map_insert_def[symmetric]]
         vs_entry_align_def vs_ptr_align_def) apply (rule conjI) apply clarsimp apply (subgoal_tac "x \<in> obj_range' x x2") apply (subgoal_tac "x\<in> {ptr .. ptr + 2 ^ 12 - 1}") apply (drule(2) pspace_no_overlapD3') apply (simp add:pageBits_def) apply blast apply (simp add: pageBits_def
     split : ARM_H.pte.splits ARM_H.pde.splits
     arch_kernel_object.splits Structures_H.kernel_object.splits ) apply (drule mask_out_first_mask_some[where m = 12]) apply simp apply (clarsimp simp:mask_lower_twice field_simps blah word_and_le2) apply (rule order_trans[OF and_neg_mask_plus_mask_mono[where n = 12]]) apply (simp add:mask_def) apply (drule mask_out_first_mask_some[where m = 12]) apply simp apply (clarsimp simp:mask_lower_twice field_simps blah word_and_le2) apply (rule order_trans[OF and_neg_mask_plus_mask_mono[where n = 12]]) apply (simp add:mask_def) apply (simp add:obj_range'_def blah) apply (rule is_aligned_no_overflow) apply (drule(2) pspace_alignedD') apply clarsimp apply (drule valid_duplicates'_D) apply (simp add:vs_entry_align_def vs_ptr_align_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr pageBits s \<and> is_aligned ptr pageBits \<and> pspace_aligned' s\<rbrace> placeNewObject' ptr (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr pageBits s \<and> is_aligned ptr pageBits \<and> pspace_aligned' s\<rbrace> do y <- unless (ptr && mask (objBitsKO (KOArch (KOASIDPool makeObject))) = 0) (alignError (objBitsKO (KOArch (KOASIDPool makeObject))));
ps <- gets ksPSpace;
case lookupAround2 (ptr + (2 ^ objBitsKO (KOArch (KOASIDPool makeObject)) - 1)) ps of (before, uu_) \<Rightarrow> do y <- case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr);
modify (ksPSpace_update (\<lambda>_. ps(ptr \<mapsto> KOArch (KOASIDPool makeObject))))
od
od \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr pageBits s \<and> is_aligned ptr pageBits \<and> pspace_aligned' s \<Longrightarrow> (ptr && mask (objBitsKO (KOArch (KOASIDPool makeObject))) = 0 \<longrightarrow> (\<forall>x. (\<exists>xa. lookupAround2 (ptr + (2 ^ objBitsKO (KOArch (KOASIDPool makeObject)) - 1)) (ksPSpace s) = (x, xa)) \<longrightarrow> (x = None \<longrightarrow> vs_valid_duplicates' (\<lambda>a. if a = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s a)) \<and> (\<forall>a. (\<exists>b. x = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> vs_valid_duplicates' (\<lambda>a. if a = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s a)))) \<and> (ptr && mask (objBitsKO (KOArch (KOASIDPool makeObject))) \<noteq> 0 \<longrightarrow> ?Q61 s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr pageBits s \<and> is_aligned ptr pageBits \<and> pspace_aligned' s; vs_valid_duplicates' (\<lambda>a. if a = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s a)\<rbrakk> \<Longrightarrow> (ptr && mask (objBitsKO (KOArch (KOASIDPool makeObject))) = 0 \<longrightarrow> (\<forall>x. (\<exists>xa. lookupAround2 (ptr + (2 ^ objBitsKO (KOArch (KOASIDPool makeObject)) - 1)) (ksPSpace s) = (x, xa)) \<longrightarrow> (x = None \<longrightarrow> vs_valid_duplicates' (\<lambda>a. if a = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s a)) \<and> (\<forall>a. (\<exists>b. x = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> vs_valid_duplicates' (\<lambda>a. if a = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s a)))) \<and> (ptr && mask (objBitsKO (KOArch (KOASIDPool makeObject))) \<noteq> 0 \<longrightarrow> ?Q61 s)
 2. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr pageBits s \<and> is_aligned ptr pageBits \<and> pspace_aligned' s \<Longrightarrow> vs_valid_duplicates' (\<lambda>a. if a = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr pageBits s \<and> is_aligned ptr pageBits \<and> pspace_aligned' s \<Longrightarrow> vs_valid_duplicates' (\<lambda>a. if a = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' ptr pageBits s \<and> is_aligned ptr pageBits \<and> pspace_aligned' s \<Longrightarrow> \<forall>x y. case if x = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s 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> (if x = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s x) = (if y = ptr then Some (KOArch (KOASIDPool makeObject)) else ksPSpace s y) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s\<rbrakk> \<Longrightarrow> (x = ptr \<longrightarrow> (\<forall>y. y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> ptr && ~~ mask (vs_ptr_align (KOArch (KOASIDPool makeObject))) = y && ~~ mask (vs_ptr_align (KOArch (KOASIDPool makeObject))) \<longrightarrow> Some (KOArch (KOASIDPool makeObject)) = ksPSpace s y)) \<and> (x \<noteq> ptr \<longrightarrow> (\<forall>y. (y = ptr \<longrightarrow> (case ksPSpace s x of None \<Rightarrow> True | Some ko \<Rightarrow> is_aligned ptr 2 \<longrightarrow> x && ~~ mask (vs_ptr_align ko) = ptr && ~~ mask (vs_ptr_align ko) \<longrightarrow> ko = KOArch (KOASIDPool makeObject))) \<and> (y \<noteq> ptr \<longrightarrow> (case ksPSpace s 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 = ksPSpace s y)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> (y = ptr \<longrightarrow> is_aligned ptr 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = KOArch (KOASIDPool makeObject)) \<and> (y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y) proof (prove)
goal (2 subgoals):
 1. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y = ptr \<longrightarrow> is_aligned ptr 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> x2 = KOArch (KOASIDPool makeObject)
 2. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x2 = KOArch (KOASIDPool makeObject)
 2. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> obj_range' x x2\<rbrakk> \<Longrightarrow> x2 = KOArch (KOASIDPool makeObject)
 2. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 3. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> obj_range' x x2; x \<in> {ptr..ptr + 2 ^ 12 - 1}\<rbrakk> \<Longrightarrow> x2 = KOArch (KOASIDPool makeObject)
 2. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> obj_range' x x2\<rbrakk> \<Longrightarrow> x \<in> {ptr..ptr + 2 ^ 12 - 1}
 3. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 4. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> obj_range' x x2; x \<in> {ptr..ptr + 2 ^ 12 - 1}; obj_range' x x2 \<inter> {ptr..ptr + 2 ^ pageBits - 1} = {}\<rbrakk> \<Longrightarrow> x2 = KOArch (KOASIDPool makeObject)
 2. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> obj_range' x x2\<rbrakk> \<Longrightarrow> x \<in> {ptr..ptr + 2 ^ 12 - 1}
 3. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 4. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> obj_range' x x2; x \<in> {ptr..0xFFF + ptr}; obj_range' x x2 \<inter> {ptr..0xFFF + ptr} = {}\<rbrakk> \<Longrightarrow> x2 = KOArch (KOASIDPool makeObject)
 2. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> obj_range' x x2\<rbrakk> \<Longrightarrow> x \<in> {ptr..ptr + 2 ^ 12 - 1}
 3. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 4. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> obj_range' x x2\<rbrakk> \<Longrightarrow> x \<in> {ptr..ptr + 2 ^ 12 - 1}
 2. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 3. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s x x2 x8 x2a x21 x22 x23 x24 x25. \<lbrakk>x \<in> obj_range' x (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); x8 = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); x2a = ARM_H.LargePagePTE x21 x22 x23 x24 x25; x && ~~ mask 6 = ptr\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 2. \<And>s x x2 x8 x3 x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); x8 = KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46); x3 = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; x && ~~ mask 6 = ptr\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 3. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 4. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (5 subgoals):
 1. \<And>s x x2 x8 x2a x21 x22 x23 x24 x25. \<lbrakk>x \<in> obj_range' x (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); x8 = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); x2a = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> 6 \<le> 12
 2. \<And>s x x2 x8 x2a x21 x22 x23 x24 x25. \<lbrakk>x \<in> obj_range' x (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); x8 = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); x2a = ARM_H.LargePagePTE x21 x22 x23 x24 x25; x && ~~ mask 12 = ptr && ~~ mask 12\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 3. \<And>s x x2 x8 x3 x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); x8 = KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46); x3 = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; x && ~~ mask 6 = ptr\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 4. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 5. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s x x2 x8 x2a x21 x22 x23 x24 x25. \<lbrakk>x \<in> obj_range' x (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)); x8 = KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25); x2a = ARM_H.LargePagePTE x21 x22 x23 x24 x25; x && ~~ mask 12 = ptr && ~~ mask 12\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 2. \<And>s x x2 x8 x3 x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); x8 = KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46); x3 = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; x && ~~ mask 6 = ptr\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 3. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 4. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s x x21 x22 x23 x24 x25. \<lbrakk>x \<in> obj_range' x (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' (x && ~~ mask 12) 12 s; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); x \<noteq> x && ~~ mask 12; is_aligned (x && ~~ mask 12) 2; ptr = x && ~~ mask 12\<rbrakk> \<Longrightarrow> x \<le> (x && ~~ mask 12) + 0xFFF
 2. \<And>s x x2 x8 x3 x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); x8 = KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46); x3 = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; x && ~~ mask 6 = ptr\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 3. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 4. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s x x21 x22 x23 x24 x25. \<lbrakk>x \<in> obj_range' x (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' (x && ~~ mask 12) 12 s; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); x \<noteq> x && ~~ mask 12; is_aligned (x && ~~ mask 12) 2; ptr = x && ~~ mask 12\<rbrakk> \<Longrightarrow> (x && ~~ mask 12) + mask 12 \<le> (x && ~~ mask 12) + 0xFFF
 2. \<And>s x x2 x8 x3 x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); x8 = KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46); x3 = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; x && ~~ mask 6 = ptr\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 3. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 4. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>s x x2 x8 x3 x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); x8 = KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46); x3 = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; x && ~~ mask 6 = ptr\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 2. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 3. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s x x2 x8 x3 x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); x8 = KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46); x3 = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> 6 \<le> 12
 2. \<And>s x x2 x8 x3 x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); x8 = KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46); x3 = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; x && ~~ mask 12 = ptr && ~~ mask 12\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 3. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 4. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>s x x2 x8 x3 x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr 12 s; is_aligned ptr 12; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> ptr; is_aligned ptr 2; x2 = KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)); x8 = KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46); x3 = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; x && ~~ mask 12 = ptr && ~~ mask 12\<rbrakk> \<Longrightarrow> x \<in> {ptr..0xFFF + ptr}
 2. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 3. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>s x x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' (x && ~~ mask 12) 12 s; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> x && ~~ mask 12; is_aligned (x && ~~ mask 12) 2; ptr = x && ~~ mask 12\<rbrakk> \<Longrightarrow> x \<le> (x && ~~ mask 12) + 0xFFF
 2. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 3. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>s x x41 x42 x43 x44 x45 x46. \<lbrakk>x \<in> obj_range' x (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' (x && ~~ mask 12) 12 s; pspace_aligned' s; ksPSpace s x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); x \<noteq> x && ~~ mask 12; is_aligned (x && ~~ mask 12) 2; ptr = x && ~~ mask 12\<rbrakk> \<Longrightarrow> (x && ~~ mask 12) + mask 12 \<le> (x && ~~ mask 12) + 0xFFF
 2. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 3. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<in> obj_range' x x2
 2. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ objBitsKO x2 - 1
 2. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>s x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; is_aligned ptr 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = ptr && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO x2)
 2. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (1 subgoal):
 1. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr\<rbrakk> \<Longrightarrow> y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (1 subgoal):
 1. \<And>s x x2 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; y \<noteq> ptr; is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s x x2 y. \<lbrakk>pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; y \<noteq> ptr; is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> ksPSpace s (?p313 s x x2 y) = Some (?ko313 s x x2 y)
 2. \<And>s x x2 y. \<lbrakk>pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; y \<noteq> ptr; is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> is_aligned (?p'313 s x x2 y) 2
 3. \<And>s x x2 y. \<lbrakk>pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; y \<noteq> ptr; is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> ?p313 s x x2 y && ~~ mask (vs_ptr_align (?ko313 s x x2 y)) = ?p'313 s x x2 y && ~~ mask (vs_ptr_align (?ko313 s x x2 y))
 4. \<And>s x x2 y. \<lbrakk>pspace_no_overlap' ptr pageBits s; is_aligned ptr pageBits; pspace_aligned' s; ksPSpace s x = Some x2; x \<noteq> ptr; y \<noteq> ptr; is_aligned y 2; x && ~~ mask (case x2 of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa 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 xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); ksPSpace s (?p'313 s x x2 y) = Some (?ko313 s x x2 y)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal:
No subgoals!