theory PageTableDuplicates

lemma mapM_x_storePTE_update_helper:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)
    \<and> pspace_aligned' s
    \<and> page_table_at' ptr s
    \<and> word && ~~ mask ptBits = ptr
    \<and> sz \<le> ptBits \<and> 6 \<le> sz
    \<and> is_aligned word sz
    \<and> xs = [word , word + 4 .e. word + (mask sz)]
  \<rbrace>
  mapM_x (swp storePTE pte) xs
  \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (wp mapM_x_storePTE_updates) apply clarsimp apply (frule(2) page_table_at_set_list) apply simp+ apply (subst vs_valid_duplicates'_def) apply clarsimp apply (intro conjI impI) apply clarsimp apply (thin_tac "x = y" for x y) apply (simp add:mask_lower_twice) apply (subgoal_tac "x && ~~ mask sz = y && ~~ mask sz") apply (drule(1) page_table_at_pte_atD') apply (drule mask_out_first_mask_some[where m = ptBits]) apply (simp add:vs_ptr_align_def split:ARM_H.pte.splits) apply (simp add:mask_lower_twice vs_ptr_align_def
      split:ARM_H.pte.splits) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (clarsimp simp:vs_ptr_align_def
      split:arch_kernel_obj.splits Structures_H.kernel_object.splits
      split:ARM_H.pte.splits) apply (drule mask_out_first_mask_some[where m = sz]) apply simp apply (simp add:mask_lower_twice) apply clarsimp apply (intro conjI impI) apply (thin_tac "x = y" for x y) apply (clarsimp split:option.splits) apply (subgoal_tac "x && ~~ mask sz = y && ~~ mask sz") apply (drule_tac p' = x in page_table_at_pte_atD') apply (drule pspace_alignedD') apply simp apply (simp add:objBits_simps' archObjSize_def pteBits_def
        is_aligned_weaken[where y = 2] pageBits_def pdeBits_def
        split:kernel_object.splits arch_kernel_object.splits) apply (simp add:mask_lower_twice) apply (drule mask_out_first_mask_some[where m = ptBits]) apply (simp add:vs_ptr_align_def
        split:kernel_object.splits arch_kernel_object.splits
        ARM_H.pte.splits ARM_H.pde.splits) apply (subst (asm) mask_lower_twice) apply (simp add:vs_ptr_align_def
        split:kernel_object.splits arch_kernel_object.splits
        ARM_H.pte.splits ARM_H.pde.splits) apply simp apply (simp add:vs_ptr_align_def
      split:kernel_object.splits arch_kernel_object.splits
      ARM_H.pte.splits) apply (simp add:mask_lower_twice) apply (drule mask_out_first_mask_some[where m = sz]) apply (simp add:vs_ptr_align_def
      split:kernel_object.splits arch_kernel_object.splits
      ARM_H.pte.splits ARM_H.pde.splits) apply (subst (asm) mask_lower_twice) apply (simp add:vs_ptr_align_def
      split:kernel_object.splits arch_kernel_object.splits
      ARM_H.pte.splits ARM_H.pde.splits) apply simp apply (clarsimp split:option.splits) apply (drule_tac p' = y in valid_duplicates'_D) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> page_table_at' ptr s \<and> word && ~~ mask ptBits = ptr \<and> sz \<le> ptBits \<and> 6 \<le> sz \<and> is_aligned word sz \<and> xs = [word , word + 4 .e. word + mask sz]\<rbrace> mapM_x (swp storePTE pte) xs \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> page_table_at' ptr s \<and> word && ~~ mask ptBits = ptr \<and> sz \<le> ptBits \<and> 6 \<le> sz \<and> is_aligned word sz \<and> xs = [word , word + 4 .e. word + mask sz] \<Longrightarrow> (\<forall>x\<in>set xs. pte_at' x s) \<and> vs_valid_duplicates' (\<lambda>a. if a \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set [word , word + 4 .e. word + mask sz]. pte_at' x s) \<and> vs_valid_duplicates' (\<lambda>a. if a \<in> set [word , word + 4 .e. word + mask sz] then Some (KOArch (KOPTE pte)) else ksPSpace s a) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]\<rbrakk> \<Longrightarrow> ?p21 s && ~~ mask ptBits = word && ~~ mask ptBits
 2. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]\<rbrakk> \<Longrightarrow> is_aligned (?p21 s) sz
 3. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]\<rbrakk> \<Longrightarrow> 2 \<le> sz
 4. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [?p21 s , ?p21 s + 4 .e. ?p21 s + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = ?p21 s}\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set [word , word + 4 .e. word + mask sz]. pte_at' x s) \<and> vs_valid_duplicates' (\<lambda>a. if a \<in> set [word , word + 4 .e. word + mask sz] then Some (KOArch (KOPTE pte)) else ksPSpace s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (\<lambda>a. if pte_at' a s \<and> a && ~~ mask sz = word then Some (KOArch (KOPTE pte)) else ksPSpace s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}\<rbrakk> \<Longrightarrow> \<forall>x y. case if pte_at' x s \<and> x && ~~ mask sz = word then Some (KOArch (KOPTE pte)) 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 pte_at' x s \<and> x && ~~ mask sz = word then Some (KOArch (KOPTE pte)) else ksPSpace s x) = (if pte_at' y s \<and> y && ~~ mask sz = word then Some (KOArch (KOPTE pte)) else ksPSpace s y) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}\<rbrakk> \<Longrightarrow> (pte_at' x s \<and> x && ~~ mask sz = word \<longrightarrow> (\<forall>y. (pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) \<longrightarrow> Some (KOArch (KOPTE pte)) = ksPSpace s y)) \<and> ((pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word) \<longrightarrow> (\<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (2 subgoals):
 1. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<and> x && ~~ mask sz = word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) \<longrightarrow> Some (KOArch (KOPTE pte)) = ksPSpace s y
 2. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (2 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((x && ~~ mask sz) && ~~ mask ptBits) s; ptr = (x && ~~ mask sz) && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE pte)) = ksPSpace s y
 2. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (2 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((x && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE pte)) = ksPSpace s y
 2. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (2 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE pte)) = ksPSpace s y
 2. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (3 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))); x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE pte)) = ksPSpace s y
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 3. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (4 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))); x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> y && ~~ mask ptBits = x && ~~ mask ptBits
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))); x && ~~ mask sz = y && ~~ mask sz; pte_at' y s\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE pte)) = ksPSpace s y
 3. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 4. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (5 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> vs_ptr_align (KOArch (KOPTE pte)) \<le> ptBits
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz; x && ~~ mask ptBits = (y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))) && ~~ mask ptBits\<rbrakk> \<Longrightarrow> y && ~~ mask ptBits = x && ~~ mask ptBits
 3. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))); x && ~~ mask sz = y && ~~ mask sz; pte_at' y s\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE pte)) = ksPSpace s y
 4. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 5. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (4 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz; x && ~~ mask ptBits = (y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))) && ~~ mask ptBits\<rbrakk> \<Longrightarrow> y && ~~ mask ptBits = x && ~~ mask ptBits
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))); x && ~~ mask sz = y && ~~ mask sz; pte_at' y s\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE pte)) = ksPSpace s y
 3. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 4. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (3 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))); x && ~~ mask sz = y && ~~ mask sz; pte_at' y s\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE pte)) = ksPSpace s y
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 3. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (2 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align (KOArch (KOPTE pte))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE pte)))\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 2. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (2 subgoals):
 1. \<And>s x y x21 x22 x23 x24 x25. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; pte = ARM_H.LargePagePTE x21 x22 x23 x24 x25; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 2. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (3 subgoals):
 1. \<And>s x y x21 x22 x23 x24 x25. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; pte = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> 6 \<le> sz
 2. \<And>s x y x21 x22 x23 x24 x25. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; pte = ARM_H.LargePagePTE x21 x22 x23 x24 x25; x && ~~ mask sz = (y && ~~ mask 6) && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 3. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (2 subgoals):
 1. \<And>s x y x21 x22 x23 x24 x25. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (x && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz]; set [x && ~~ mask sz , (x && ~~ mask sz) + 4 .e. (x && ~~ mask sz) + mask sz] = {xa. pte_at' xa s \<and> xa && ~~ mask sz = x && ~~ mask sz}; pte_at' x s; word = x && ~~ mask sz; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> x && ~~ mask sz; is_aligned y 2; pte = ARM_H.LargePagePTE x21 x22 x23 x24 x25; x && ~~ mask sz = (y && ~~ mask 6) && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 2. \<And>s x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> \<forall>y. (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word\<rbrakk> \<Longrightarrow> (pte_at' y s \<and> y && ~~ mask sz = word \<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> ko = KOArch (KOPTE pte))) \<and> ((pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word) \<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 (2 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<and> y && ~~ mask sz = word\<rbrakk> \<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> ko = KOArch (KOPTE pte)
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (2 subgoals):
 1. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<and> y && ~~ mask sz = word\<rbrakk> \<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> ko = KOArch (KOPTE pte)
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (2 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (3 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 3. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (5 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask ptBits = (y && ~~ mask sz) && ~~ mask ptBits
 3. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; pte_at' x s\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 4. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 5. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (6 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; is_aligned x (objBitsKO x2)\<rbrakk> \<Longrightarrow> is_aligned x 2
 3. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask ptBits = (y && ~~ mask sz) && ~~ mask ptBits
 4. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; pte_at' x s\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 5. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 6. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (5 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; is_aligned x (objBitsKO x2)\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask ptBits = (y && ~~ mask sz) && ~~ mask ptBits
 3. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; pte_at' x s\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 4. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 5. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (4 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask ptBits = (y && ~~ mask sz) && ~~ mask ptBits
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; pte_at' x s\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 3. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 4. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (4 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; \<not> pte_at' x s; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask ptBits = y && ~~ mask ptBits
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; pte_at' x s\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 3. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 4. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (5 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; \<not> pte_at' x s; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> vs_ptr_align x2 \<le> ptBits
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; \<not> pte_at' x s; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz; x && ~~ mask ptBits = (y && ~~ mask (vs_ptr_align x2)) && ~~ mask ptBits\<rbrakk> \<Longrightarrow> x && ~~ mask ptBits = y && ~~ mask ptBits
 3. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; pte_at' x s\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 4. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 5. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (4 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; \<not> pte_at' x s; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz; x && ~~ mask ptBits = (y && ~~ mask (vs_ptr_align x2)) && ~~ mask ptBits\<rbrakk> \<Longrightarrow> x && ~~ mask ptBits = y && ~~ mask ptBits
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; pte_at' x s\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 3. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 4. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (5 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; \<not> pte_at' x s; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> vs_ptr_align x2 \<le> ptBits
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; \<not> pte_at' x s; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz; x && ~~ mask ptBits = y && ~~ mask ptBits\<rbrakk> \<Longrightarrow> x && ~~ mask ptBits = y && ~~ mask ptBits
 3. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; pte_at' x s\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 4. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 5. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (4 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; \<not> pte_at' x s; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz; x && ~~ mask ptBits = y && ~~ mask ptBits\<rbrakk> \<Longrightarrow> x && ~~ mask ptBits = y && ~~ mask ptBits
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; pte_at' x s\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 3. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 4. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (3 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x && ~~ mask sz = y && ~~ mask sz; pte_at' x s\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPTE pte)
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 3. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (2 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' ((y && ~~ mask sz) && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (2 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (y && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (3 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (y && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2\<rbrakk> \<Longrightarrow> vs_ptr_align x2 \<le> sz
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (y && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask sz = (y && ~~ mask (vs_ptr_align x2)) && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 3. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (2 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (y && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask sz = (y && ~~ mask (vs_ptr_align x2)) && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (3 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (y && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2\<rbrakk> \<Longrightarrow> vs_ptr_align x2 \<le> sz
 2. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (y && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 3. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 (2 subgoals):
 1. \<And>s x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (y && ~~ mask ptBits) s; sz \<le> ptBits; 6 \<le> sz; xs = [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz]; set [y && ~~ mask sz , (y && ~~ mask sz) + 4 .e. (y && ~~ mask sz) + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = y && ~~ mask sz}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> y && ~~ mask sz; pte_at' y s; word = y && ~~ mask sz; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> x && ~~ mask sz = y && ~~ mask sz
 2. \<And>s x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word\<rbrakk> \<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 y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s x y x2. \<lbrakk>pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> ksPSpace s (?p288 s x y x2) = Some (?ko288 s x y x2)
 2. \<And>s x y x2. \<lbrakk>pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> is_aligned y 2
 3. \<And>s x y x2. \<lbrakk>pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> ?p288 s x y x2 && ~~ mask (vs_ptr_align (?ko288 s x y x2)) = y && ~~ mask (vs_ptr_align (?ko288 s x y x2))
 4. \<And>s x y x2. \<lbrakk>pspace_aligned' s; page_table_at' (word && ~~ mask ptBits) s; ptr = word && ~~ mask ptBits; sz \<le> ptBits; 6 \<le> sz; is_aligned word sz; xs = [word , word + 4 .e. word + mask sz]; set [word , word + 4 .e. word + mask sz] = {x. pte_at' x s \<and> x && ~~ mask sz = word}; pte_at' x s \<longrightarrow> x && ~~ mask sz \<noteq> word; pte_at' y s \<longrightarrow> y && ~~ mask sz \<noteq> word; ksPSpace s x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace s y = Some (?ko288 s x y x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal:
No subgoals!