theory PageTableDuplicates

lemma valid_duplicates'_update:
  "\<lbrakk>is_aligned ptr (APIType_capBits ty us);pspace_aligned' s;
   vs_valid_duplicates' (ksPSpace s); vs_entry_align ko = 0;
   pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> vs_valid_duplicates'
   (\<lambda>a. if a = ptr then Some ko else ksPSpace s a)" supply option.case_cong_weak[cong] apply (subst vs_valid_duplicates'_def) apply clarsimp apply (intro conjI impI allI) apply (case_tac ko,
           simp_all add: vs_ptr_align_def vs_entry_align_def) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,
           simp_all split: ARM_H.pde.splits ARM_H.pte.splits) apply (clarsimp split:option.splits) apply (drule(2) pspace_no_overlap_base') apply (drule(2) valid_duplicates'_D) apply simp apply (clarsimp split: option.splits)+ apply (drule valid_duplicates'_D) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); vs_entry_align ko = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (\<lambda>a. if a = ptr then Some ko else ksPSpace s a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); vs_entry_align ko = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (\<lambda>a. if a = ptr then Some ko else ksPSpace s a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); vs_entry_align ko = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> \<forall>x y. case if x = ptr then Some ko else ksPSpace s x of None \<Rightarrow> True | Some koa \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align koa) = y && ~~ mask (vs_ptr_align koa) \<longrightarrow> (if x = ptr then Some ko else ksPSpace s x) = (if y = ptr then Some ko else ksPSpace s y) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); vs_entry_align ko = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s\<rbrakk> \<Longrightarrow> (x = ptr \<longrightarrow> (\<forall>y. y \<noteq> ptr \<longrightarrow> is_aligned y 2 \<longrightarrow> ptr && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> Some ko = ksPSpace s y)) \<and> (x \<noteq> ptr \<longrightarrow> (\<forall>y. (y = ptr \<longrightarrow> (case ksPSpace s x of None \<Rightarrow> True | Some koa \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align koa) = y && ~~ mask (vs_ptr_align koa) \<longrightarrow> ksPSpace s x = Some ko)) \<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> ksPSpace s x = ksPSpace s y)))) proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); vs_entry_align ko = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; x = ptr; y \<noteq> ptr; is_aligned y 2; ptr && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko)\<rbrakk> \<Longrightarrow> Some ko = ksPSpace s y
 2. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); vs_entry_align ko = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; x \<noteq> ptr; y = ptr\<rbrakk> \<Longrightarrow> case ksPSpace s x of None \<Rightarrow> True | Some koa \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align koa) = y && ~~ mask (vs_ptr_align koa) \<longrightarrow> ksPSpace s x = Some ko
 3. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); vs_entry_align ko = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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> ksPSpace s x = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>x y x8. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE x \<Rightarrow> pte_align' x | KOPDE x \<Rightarrow> pde_align' x) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; x = ptr; y \<noteq> ptr; is_aligned y 2; ptr && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0); ko = KOArch x8\<rbrakk> \<Longrightarrow> Some (KOArch x8) = ksPSpace s y
 2. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; x \<noteq> ptr; y = ptr\<rbrakk> \<Longrightarrow> case ksPSpace s x of None \<Rightarrow> True | Some koa \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align koa) = y && ~~ mask (vs_ptr_align koa) \<longrightarrow> ksPSpace s x = Some ko
 3. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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> ksPSpace s x = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>x y arch_kernel_object. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE x \<Rightarrow> pte_align' x | KOPDE x \<Rightarrow> pde_align' x) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; x = ptr; y \<noteq> ptr; is_aligned y 2; ptr && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0); ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> Some (KOArch arch_kernel_object) = ksPSpace s y
 2. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; x \<noteq> ptr; y = ptr\<rbrakk> \<Longrightarrow> case ksPSpace s x of None \<Rightarrow> True | Some koa \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align koa) = y && ~~ mask (vs_ptr_align koa) \<longrightarrow> ksPSpace s x = Some ko
 3. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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> ksPSpace s x = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; x \<noteq> ptr; y = ptr\<rbrakk> \<Longrightarrow> case ksPSpace s x of None \<Rightarrow> True | Some koa \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align koa) = y && ~~ mask (vs_ptr_align koa) \<longrightarrow> ksPSpace s x = Some ko
 2. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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> ksPSpace s x = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>x x2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE xa) \<Rightarrow> pte_align' xa | KOArch (KOPDE xa) \<Rightarrow> pde_align' xa | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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 = ko
 2. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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> ksPSpace s x = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>x x2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE xa) \<Rightarrow> pte_align' xa | KOArch (KOPDE xa) \<Rightarrow> pde_align' xa | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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 = None\<rbrakk> \<Longrightarrow> x2 = ko
 2. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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> ksPSpace s x = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>x x2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE xa) \<Rightarrow> pte_align' xa | KOArch (KOPDE xa) \<Rightarrow> pde_align' xa | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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 = None\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = ptr && ~~ mask (vs_ptr_align x2)
 2. \<And>x x2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE xa) \<Rightarrow> pte_align' xa | KOArch (KOPDE xa) \<Rightarrow> pde_align' xa | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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 = None; ksPSpace s ptr = Some x2\<rbrakk> \<Longrightarrow> x2 = ko
 3. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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> ksPSpace s x = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>x x2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE xa) \<Rightarrow> pte_align' xa | KOArch (KOPDE xa) \<Rightarrow> pde_align' xa | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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 = None; ksPSpace s ptr = Some x2\<rbrakk> \<Longrightarrow> x2 = ko
 2. \<And>x y. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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> ksPSpace s x = ksPSpace s y proof (prove)
goal (1 subgoal):
 1. \<And>x y x2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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>x y x2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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 (?p69 x y x2) = Some (?ko69 x y x2)
 2. \<And>x y x2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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 (?p'69 x y x2) 2
 3. \<And>x y x2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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> ?p69 x y x2 && ~~ mask (vs_ptr_align (?ko69 x y x2)) = ?p'69 x y x2 && ~~ mask (vs_ptr_align (?ko69 x y x2))
 4. \<And>x y x2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); pspace_aligned' s; (case ko of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE pte) \<Rightarrow> pte_align' pte | KOArch (KOPDE pde) \<Rightarrow> pde_align' pde | _ \<Rightarrow> 0) = 0; pspace_no_overlap' ptr (APIType_capBits ty us) s; 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 (?p'69 x y x2) = Some (?ko69 x y x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal:
No subgoals!