theory PageTableDuplicates

lemma storePDE_no_duplicates':
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)
    \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0 ) ptr s
    \<and> vs_entry_align (KOArch (KOPDE pde)) = 0 \<rbrace>
   storePDE ptr pde
  \<lbrace>\<lambda>ya s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add:storePDE_def setObject_def split_def | wp | wpc)+ apply (simp add:updateObject_default_def) apply wp+ apply clarsimp apply (subst vs_valid_duplicates'_def) apply clarsimp apply (intro conjI impI) apply (clarsimp simp:vs_ptr_align_def vs_entry_align_def
     split:option.splits
     ARM_H.pde.splits) apply clarsimp apply (intro conjI impI) apply (clarsimp split:option.splits) apply (drule_tac p = x in valid_duplicates'_D) apply simp apply simp apply simp apply (clarsimp simp:ko_wp_at'_def vs_entry_align_def
     vs_ptr_align_def
     split:if_splits option.splits arch_kernel_object.splits
     Structures_H.kernel_object.splits ARM_H.pde.splits
     ARM_H.pte.splits) apply (clarsimp split:option.splits) apply (drule_tac p = x and 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> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s \<and> vs_entry_align (KOArch (KOPDE pde)) = 0\<rbrace> storePDE ptr pde \<lbrace>\<lambda>ya s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ps p. \<lbrace>?B2 ps p\<rbrace> updateObject_default pde (snd p) ptr (fst p) (snd (lookupAround2 ptr ps)) \<lbrace>\<lambda>obj' s. vs_valid_duplicates' (\<lambda>a. if a = fst p then Some obj' else ps a)\<rbrace>
 2. \<And>ps. \<lbrace>?B1 ps\<rbrace> assert_opt (fst (lookupAround2 ptr ps)) \<lbrace>?B2 ps\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets ksPSpace \<lbrace>?B1\<rbrace>
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s \<and> vs_entry_align (KOArch (KOPDE pde)) = 0 \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ps p. \<lbrace>?B2 ps p\<rbrace> do y <- assert (ptr = fst p);
_ <- projectKO (snd p);
y <- alignCheck ptr (objBits pde);
y <- magnitudeCheck ptr (snd (lookupAround2 ptr ps)) (objBits pde);
return (KOArch (KOPDE pde))
od \<lbrace>\<lambda>obj' s. vs_valid_duplicates' (\<lambda>a. if a = fst p then Some obj' else ps a)\<rbrace>
 2. \<And>ps. \<lbrace>?B1 ps\<rbrace> assert_opt (fst (lookupAround2 ptr ps)) \<lbrace>?B2 ps\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets ksPSpace \<lbrace>?B1\<rbrace>
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s \<and> vs_entry_align (KOArch (KOPDE pde)) = 0 \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s \<and> vs_entry_align (KOArch (KOPDE pde)) = 0 \<Longrightarrow> fst (lookupAround2 ptr (ksPSpace s)) \<noteq> None \<longrightarrow> ptr = fst (the (fst (lookupAround2 ptr (ksPSpace s)))) \<longrightarrow> vs_valid_duplicates' (\<lambda>a. if a = fst (the (fst (lookupAround2 ptr (ksPSpace s)))) then Some (KOArch (KOPDE pde)) else ksPSpace s a) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (\<lambda>a. if a = ptr then Some (KOArch (KOPDE pde)) else ksPSpace s a) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b\<rbrakk> \<Longrightarrow> \<forall>x y. case if x = ptr then Some (KOArch (KOPDE pde)) 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 (KOPDE pde)) else ksPSpace s x) = (if y = ptr then Some (KOArch (KOPDE pde)) else ksPSpace s y) proof (prove)
goal (1 subgoal):
 1. \<And>s b x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b\<rbrakk> \<Longrightarrow> (x = ptr \<longrightarrow> (\<forall>y. y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> ptr && ~~ mask (vs_ptr_align (KOArch (KOPDE pde))) = y && ~~ mask (vs_ptr_align (KOArch (KOPDE pde))) \<longrightarrow> Some (KOArch (KOPDE pde)) = 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 (KOPDE pde))) \<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 (2 subgoals):
 1. \<And>s b x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x = ptr\<rbrakk> \<Longrightarrow> \<forall>y. y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> ptr && ~~ mask (vs_ptr_align (KOArch (KOPDE pde))) = y && ~~ mask (vs_ptr_align (KOArch (KOPDE pde))) \<longrightarrow> Some (KOArch (KOPDE pde)) = ksPSpace s y
 2. \<And>s b x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr\<rbrakk> \<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 (KOPDE pde))) \<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 b x. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr\<rbrakk> \<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 (KOPDE pde))) \<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 b x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr\<rbrakk> \<Longrightarrow> (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 (KOPDE pde))) \<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 (2 subgoals):
 1. \<And>s b x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y = ptr\<rbrakk> \<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 (KOPDE pde)
 2. \<And>s b x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr\<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 b x x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPDE pde)
 2. \<And>s b x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr\<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 b x x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> ksPSpace s x = Some (?ko114 s b x x2)
 2. \<And>s b x x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> is_aligned (?p'114 s b x x2) 2
 3. \<And>s b x x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (?ko114 s b x x2)) = ?p'114 s b x x2 && ~~ mask (vs_ptr_align (?ko114 s b x x2))
 4. \<And>s b x x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2); ksPSpace s (?p'114 s b x x2) = Some (?ko114 s b x x2)\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPDE pde)
 5. \<And>s b x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr\<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 b x x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> is_aligned (?p'114 s b x x2) 2
 2. \<And>s b x x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = ?p'114 s b x x2 && ~~ mask (vs_ptr_align x2)
 3. \<And>s b x x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2); ksPSpace s (?p'114 s b x x2) = Some x2\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPDE pde)
 4. \<And>s b x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr\<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 b x x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2)
 2. \<And>s b x x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2); ksPSpace s ptr = Some x2\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPDE pde)
 3. \<And>s b x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr\<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 b x x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; ksPSpace s x = Some x2; is_aligned ptr 2; x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2); ksPSpace s ptr = Some x2\<rbrakk> \<Longrightarrow> x2 = KOArch (KOPDE pde)
 2. \<And>s b x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr\<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 b x y. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr\<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 b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr; 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 b x y x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr; 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 x = Some (?ko419 s b x y x2)
 2. \<And>s b x y x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr; 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 b x y x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr; 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 (vs_ptr_align (?ko419 s b x y x2)) = y && ~~ mask (vs_ptr_align (?ko419 s b x y x2))
 4. \<And>s b x y x2. \<lbrakk>ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) ptr s; vs_entry_align (KOArch (KOPDE pde)) = 0; ksPSpace s ptr = Some b; x \<noteq> ptr; y \<noteq> ptr; 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 (?ko419 s b x y x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal:
No subgoals!