theory PageTableDuplicates

lemma unmapPage_valid_duplicates'[wp]:
  notes checkMappingPPtr_inv[wp del] shows
  "\<lbrace>pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))
   and K (vmsz_aligned' vptr vmpage_size)\<rbrace>
  unmapPage vmpage_size asiv vptr word \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add:unmapPage_def) 
   (* make sure checkMappingPPtr_SmallPage is first tried before checkMappingPPtr_inv *)
   apply ((wp storePTE_no_duplicates' mapM_x_mapM_valid
    storePDE_no_duplicates' checkMappingPPtr_Section
    mapM_x_storePDE_update_helper[where sz = 6]
    lookupPTSlot_page_table_at'
    checkMappingPPtr_SmallPage)+ | wpc
    | simp add:split_def conj_comms | wp (once) checkMappingPPtr_inv)+ apply (rule_tac ptr = "p && ~~ mask ptBits" and word = p
            in mapM_x_storePTE_update_helper[where sz = 6]) apply simp apply (wp mapM_x_mapM_valid)+ apply (wp checkMappingPPtr_inv lookupPTSlot_page_table_at')+ apply (rule hoare_post_imp_R[OF lookupPTSlot_aligned[where sz= vmpage_size]]) apply (simp add:pageBitsForSize_def) apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified]) apply (clarsimp simp: mask_def add.commute upto_enum_step_def largePagePTEOffsets_def
                            pteBits_def take_bit_Suc) apply wp+ apply ((wp storePTE_no_duplicates' mapM_x_mapM_valid
          storePDE_no_duplicates' checkMappingPPtr_Section
          checkMappingPPtr_SmallPage)+ | wpc
          | simp add:split_def conj_comms | wp (once) checkMappingPPtr_inv)+ apply (rule_tac ptr = "p && ~~ mask pdBits" and word = p
          in mapM_x_storePDE_update_helper[where sz = 6]) apply wp+ apply (clarsimp simp:conj_comms) apply (wp checkMappingPPtr_inv hoare_weak_lift_imp)+ apply (clarsimp simp:conj_comms) apply (rule hoare_post_imp_R[where Q'= "\<lambda>r. pspace_aligned' and
     (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
     K(vmsz_aligned' vptr vmpage_size \<and> is_aligned r pdBits)
     and page_directory_at' (lookup_pd_slot r vptr && ~~ mask pdBits)"]) apply (wp findPDForASID_page_directory_at' | simp)+ apply (clarsimp simp add:pdBits_def pageBits_def vmsz_aligned'_def) apply (drule is_aligned_lookup_pd_slot) apply (erule is_aligned_weaken,simp) apply simp apply (drule upto_enum_step_shift[where n = 6 and m = 2,simplified]) apply (clarsimp simp: mask_def add.commute upto_enum_step_def superSectionPDEOffsets_def
                         pdeBits_def take_bit_Suc) apply (clarsimp simp:ptBits_def pageBits_def vs_entry_align_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and K (vmsz_aligned' vptr vmpage_size)\<rbrace> unmapPage vmpage_size asiv vptr word \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)\<rbrace> ignoreFailure (doE pd <- findPDForASID asiv;
y <- case vmpage_size of ARMSmallPage \<Rightarrow> doE p <- lookupPTSlot pd vptr;
checkMappingPPtr word vmpage_size (Inl p);
withoutFailure $ do storePTE p ARM_H.InvalidPTE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookupPTSlot pd vptr;
checkMappingPPtr word vmpage_size (Inl p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) largePagePTEOffsets);
mapM (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE;
liftE (flushPage vmpage_size pd asiv vptr)
odE) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)\<rbrace> ignoreFailure (doE pd <- findPDForASID asiv;
y <- case vmpage_size of ARMSmallPage \<Rightarrow> doE p <- lookupPTSlot pd vptr;
checkMappingPPtr word vmpage_size (Inl p);
withoutFailure $ do storePTE p ARM_H.InvalidPTE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookupPTSlot pd vptr;
checkMappingPPtr word vmpage_size (Inl p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) largePagePTEOffsets);
mapM (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE;
liftE (flushPage vmpage_size pd asiv vptr)
odE) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>pd p slots. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?B74 pd p () slots\<rbrace> mapM_x (swp storePTE ARM_H.InvalidPTE) slots \<lbrace>\<lambda>xa s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>pd p x. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?P'69 pd p x\<rbrace> return (map (\<lambda>x. x + p) largePagePTEOffsets) \<lbrace>?B74 pd p x\<rbrace>
 3. \<And>pd p. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?B66 pd p\<rbrace> checkMappingPPtr word vmpage_size (Inl p) \<lbrace>\<lambda>x s. True \<and> ?P'69 pd p x s\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>pd. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?R14 pd\<rbrace> lookupPTSlot pd vptr \<lbrace>?B66 pd\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>pd. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?R13 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> ?R14 pd s) \<and> (vmpage_size = ARMSection \<longrightarrow> ?R13 pd s) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 8. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>pd p x. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?P'69 pd p x\<rbrace> return (map (\<lambda>x. x + p) largePagePTEOffsets) \<lbrace>\<lambda>a b. vs_valid_duplicates' (ksPSpace b) \<and> pspace_aligned' b \<and> page_table_at' (p && ~~ mask ptBits) b \<and> p && ~~ mask ptBits = p && ~~ mask ptBits \<and> 6 \<le> ptBits \<and> 6 \<le> 6 \<and> is_aligned p 6 \<and> a = [p , p + 4 .e. p + mask 6]\<rbrace>
 2. \<And>pd p. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?B66 pd p\<rbrace> checkMappingPPtr word vmpage_size (Inl p) \<lbrace>\<lambda>x s. True \<and> ?P'69 pd p x s\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>pd. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?R14 pd\<rbrace> lookupPTSlot pd vptr \<lbrace>?B66 pd\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>pd. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?R13 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> ?R14 pd s) \<and> (vmpage_size = ARMSection \<longrightarrow> ?R13 pd s) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>pd p. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?P'69 pd p ()\<rbrace> return (map (\<lambda>x. x + p) largePagePTEOffsets) \<lbrace>\<lambda>a b. vs_valid_duplicates' (ksPSpace b) \<and> pspace_aligned' b \<and> page_table_at' (p && ~~ mask ptBits) b \<and> 6 \<le> ptBits \<and> is_aligned p 6 \<and> a = [p , p + 4 .e. p + mask 6]\<rbrace>
 2. \<And>pd p. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?B66 pd p\<rbrace> checkMappingPPtr word vmpage_size (Inl p) \<lbrace>\<lambda>x s. True \<and> ?P'69 pd p x s\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>pd. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?R14 pd\<rbrace> lookupPTSlot pd vptr \<lbrace>?B66 pd\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>pd. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?R13 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> ?R14 pd s) \<and> (vmpage_size = ARMSection \<longrightarrow> ?R13 pd s) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>pd p. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?B66 pd p\<rbrace> checkMappingPPtr word vmpage_size (Inl p) \<lbrace>\<lambda>x s. True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> page_table_at' (p && ~~ mask ptBits) s \<and> 6 \<le> ptBits \<and> is_aligned p 6 \<and> map (\<lambda>x. x + p) largePagePTEOffsets = [p , p + 4 .e. p + mask 6]\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>pd. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?R14 pd\<rbrace> lookupPTSlot pd vptr \<lbrace>?B66 pd\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>pd. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?R13 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> ?R14 pd s) \<and> (vmpage_size = ARMSection \<longrightarrow> ?R13 pd s) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>pd. vmpage_size = ARMLargePage \<Longrightarrow> \<lbrace>?P'120 pd\<rbrace> lookupPTSlot pd vptr \<lbrace>\<lambda>rv s. is_aligned rv 6 \<and> map (\<lambda>x. x + rv) largePagePTEOffsets = [rv , rv + 4 .e. rv + mask 6]\<rbrace>, -
 2. \<And>pd. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?R13 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> ?P'120 pd s) \<and> (vmpage_size = ARMSection \<longrightarrow> ?R13 pd s) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>pd rv s. \<lbrakk>vmpage_size = ARMLargePage; is_aligned rv (pageBitsForSize vmpage_size - 10)\<rbrakk> \<Longrightarrow> is_aligned rv 6 \<and> map (\<lambda>x. x + rv) largePagePTEOffsets = [rv , rv + 4 .e. rv + mask 6]
 2. \<And>pd. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?R13 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> ?R13 pd s) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>rv. \<lbrakk>vmpage_size = ARMLargePage; is_aligned rv 6\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + rv) largePagePTEOffsets = [rv , rv + 4 .e. rv + mask 6]
 2. \<And>pd. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?R13 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> ?R13 pd s) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>rv. \<lbrakk>vmpage_size = ARMLargePage; [rv , rv + 4 .e. 0x3F + rv] = map ((+) rv) [0 , 4 .e. 0x3F]\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + rv) largePagePTEOffsets = [rv , rv + 4 .e. rv + mask 6]
 2. \<And>pd. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?R13 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> ?R13 pd s) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>pd. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?R13 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> ?R13 pd s) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>pd p x. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?P'132 pd p x\<rbrace> storePDE p ARM_H.InvalidPDE \<lbrace>\<lambda>xa s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>pd p. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?B129 pd p\<rbrace> checkMappingPPtr word vmpage_size (Inr p) \<lbrace>\<lambda>x s. True \<and> ?P'132 pd p x s\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>pd. vmpage_size = ARMSection \<Longrightarrow> \<lbrace>?R13 pd\<rbrace> returnOk (lookupPDSlot pd vptr) \<lbrace>?B129 pd\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr word vmpage_size (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> ?R13 pd s) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>pd p slots. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?B172 pd p () slots\<rbrace> mapM_x (swp storePDE ARM_H.InvalidPDE) slots \<lbrace>\<lambda>xa s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>pd p x. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?P'167 pd p x\<rbrace> return (map (\<lambda>x. x + p) superSectionPDEOffsets) \<lbrace>?B172 pd p x\<rbrace>
 3. \<And>pd p. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?B164 pd p\<rbrace> checkMappingPPtr word vmpage_size (Inr p) \<lbrace>\<lambda>x s. True \<and> ?P'167 pd p x s\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> returnOk (lookupPDSlot pd vptr) \<lbrace>?B164 pd\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>pd p x. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?P'167 pd p x\<rbrace> return (map (\<lambda>x. x + p) superSectionPDEOffsets) \<lbrace>\<lambda>a b. vs_valid_duplicates' (ksPSpace b) \<and> pspace_aligned' b \<and> page_directory_at' (p && ~~ mask pdBits) b \<and> p && ~~ mask pdBits = p && ~~ mask pdBits \<and> 6 \<le> pdBits \<and> 6 \<le> 6 \<and> is_aligned p 6 \<and> a = [p , p + 4 .e. p + mask 6]\<rbrace>
 2. \<And>pd p. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?B164 pd p\<rbrace> checkMappingPPtr word vmpage_size (Inr p) \<lbrace>\<lambda>x s. True \<and> ?P'167 pd p x s\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> returnOk (lookupPDSlot pd vptr) \<lbrace>?B164 pd\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>pd p. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?B164 pd p\<rbrace> checkMappingPPtr word vmpage_size (Inr p) \<lbrace>\<lambda>x s. True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> page_directory_at' (p && ~~ mask pdBits) s \<and> p && ~~ mask pdBits = p && ~~ mask pdBits \<and> 6 \<le> pdBits \<and> 6 \<le> 6 \<and> is_aligned p 6 \<and> map (\<lambda>x. x + p) superSectionPDEOffsets = [p , p + 4 .e. p + mask 6]\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> returnOk (lookupPDSlot pd vptr) \<lbrace>?B164 pd\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>pd p. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?B164 pd p\<rbrace> checkMappingPPtr word ARMSuperSection (Inr p) \<lbrace>\<lambda>x s. pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> is_aligned p 6 \<and> 6 \<le> pdBits \<and> page_directory_at' (p && ~~ mask pdBits) s \<and> map (\<lambda>x. x + p) superSectionPDEOffsets = [p , p + 4 .e. p + mask 6]\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>pd. vmpage_size = ARMSuperSection \<Longrightarrow> \<lbrace>?R12 pd\<rbrace> returnOk (lookupPDSlot pd vptr) \<lbrace>?B164 pd\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> findPDForASID asiv \<lbrace>\<lambda>pd s. (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (vmpage_size = ARMSuperSection \<longrightarrow> ?R12 pd s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'214\<rbrace> findPDForASID asiv \<lbrace>\<lambda>rv s. vmpage_size = ARMSuperSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> is_aligned (lookupPDSlot rv vptr) 6 \<and> 6 \<le> pdBits \<and> page_directory_at' (lookupPDSlot rv vptr && ~~ mask pdBits) s \<and> map (\<lambda>x. x + lookupPDSlot rv vptr) superSectionPDEOffsets = [lookupPDSlot rv vptr , lookupPDSlot rv vptr + 4 .e. lookupPDSlot rv vptr + mask 6]\<rbrace>, -
 2. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> ?P'214 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'214\<rbrace> findPDForASID asiv \<lbrace>\<lambda>rv s. vmpage_size = ARMSuperSection \<longrightarrow> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> 6 \<le> pdBits \<and> is_aligned (lookup_pd_slot rv vptr) 6 \<and> page_directory_at' (lookup_pd_slot rv vptr && ~~ mask pdBits) s \<and> map (\<lambda>x. x + lookup_pd_slot rv vptr) superSectionPDEOffsets = [lookup_pd_slot rv vptr , lookup_pd_slot rv vptr + 4 .e. lookup_pd_slot rv vptr + mask 6]\<rbrace>, -
 2. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> ?P'214 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'214\<rbrace> findPDForASID asiv \<lbrace>\<lambda>r. pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and K (vmsz_aligned' vptr vmpage_size \<and> is_aligned r pdBits) and page_directory_at' (lookup_pd_slot r vptr && ~~ mask pdBits)\<rbrace>, -
 2. \<And>rv s. (pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and K (vmsz_aligned' vptr vmpage_size \<and> is_aligned rv pdBits) and page_directory_at' (lookup_pd_slot rv vptr && ~~ mask pdBits)) s \<Longrightarrow> vmpage_size = ARMSuperSection \<longrightarrow> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> 6 \<le> pdBits \<and> is_aligned (lookup_pd_slot rv vptr) 6 \<and> page_directory_at' (lookup_pd_slot rv vptr && ~~ mask pdBits) s \<and> map (\<lambda>x. x + lookup_pd_slot rv vptr) superSectionPDEOffsets = [lookup_pd_slot rv vptr , lookup_pd_slot rv vptr + 4 .e. lookup_pd_slot rv vptr + mask 6]
 3. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> ?P'214 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> vmsz_aligned' vptr vmpage_size \<and> is_aligned rv pdBits \<and> page_directory_at' (lookup_pd_slot rv vptr && ~~ mask pdBits) s \<Longrightarrow> vmpage_size = ARMSuperSection \<longrightarrow> 6 \<le> pdBits \<and> is_aligned (lookup_pd_slot rv vptr) 6 \<and> map (\<lambda>x. x + lookup_pd_slot rv vptr) superSectionPDEOffsets = [lookup_pd_slot rv vptr , lookup_pd_slot rv vptr + 4 .e. lookup_pd_slot rv vptr + mask 6]
 2. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<and> vmsz_aligned' vptr vmpage_size \<and> valid_objs' s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); is_aligned vptr 24; is_aligned rv (12 + pdeBits); page_directory_at' (lookup_pd_slot rv vptr && ~~ mask (12 + pdeBits)) s; vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot rv vptr) 6 \<and> map (\<lambda>x. x + lookup_pd_slot rv vptr) superSectionPDEOffsets = [lookup_pd_slot rv vptr , lookup_pd_slot rv vptr + 4 .e. lookup_pd_slot rv vptr + mask 6]
 2. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<and> vmsz_aligned' vptr vmpage_size \<and> valid_objs' s \<and> True proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); is_aligned rv (12 + pdeBits); page_directory_at' (lookup_pd_slot rv vptr && ~~ mask (12 + pdeBits)) s; vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> is_aligned (?pd245 rv s) 6
 2. \<And>rv s. \<lbrakk>pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); is_aligned rv (12 + pdeBits); page_directory_at' (lookup_pd_slot rv vptr && ~~ mask (12 + pdeBits)) s; vmpage_size = ARMSuperSection; is_aligned (lookup_pd_slot (?pd245 rv s) vptr) 6\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot rv vptr) 6 \<and> map (\<lambda>x. x + lookup_pd_slot rv vptr) superSectionPDEOffsets = [lookup_pd_slot rv vptr , lookup_pd_slot rv vptr + 4 .e. lookup_pd_slot rv vptr + mask 6]
 3. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<and> vmsz_aligned' vptr vmpage_size \<and> valid_objs' s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); is_aligned rv (12 + pdeBits); page_directory_at' (lookup_pd_slot rv vptr && ~~ mask (12 + pdeBits)) s; vmpage_size = ARMSuperSection; is_aligned (lookup_pd_slot rv vptr) 6\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot rv vptr) 6 \<and> map (\<lambda>x. x + lookup_pd_slot rv vptr) superSectionPDEOffsets = [lookup_pd_slot rv vptr , lookup_pd_slot rv vptr + 4 .e. lookup_pd_slot rv vptr + mask 6]
 2. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<and> vmsz_aligned' vptr vmpage_size \<and> valid_objs' s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); is_aligned rv (12 + pdeBits); page_directory_at' (lookup_pd_slot rv vptr && ~~ mask (12 + pdeBits)) s; vmpage_size = ARMSuperSection; is_aligned (lookup_pd_slot rv vptr) 6\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + lookup_pd_slot rv vptr) superSectionPDEOffsets = [lookup_pd_slot rv vptr , lookup_pd_slot rv vptr + 4 .e. lookup_pd_slot rv vptr + mask 6]
 2. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<and> vmsz_aligned' vptr vmpage_size \<and> valid_objs' s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>pspace_aligned' s; vs_valid_duplicates' (ksPSpace s); is_aligned rv (12 + pdeBits); page_directory_at' (lookup_pd_slot rv vptr && ~~ mask (12 + pdeBits)) s; vmpage_size = ARMSuperSection; [lookup_pd_slot rv vptr , lookup_pd_slot rv vptr + 4 .e. 0x3F + lookup_pd_slot rv vptr] = map ((+) (lookup_pd_slot rv vptr)) [0 , 4 .e. 0x3F]\<rbrakk> \<Longrightarrow> map (\<lambda>x. x + lookup_pd_slot rv vptr) superSectionPDEOffsets = [lookup_pd_slot rv vptr , lookup_pd_slot rv vptr + 4 .e. lookup_pd_slot rv vptr + mask 6]
 2. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<and> vmsz_aligned' vptr vmpage_size \<and> valid_objs' s \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and valid_objs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>y. vmsz_aligned' vptr vmpage_size)) s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> (vmpage_size = ARMSmallPage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0 \<and> True) \<and> (vmpage_size = ARMLargePage \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> True \<and> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> valid_objs' s \<and> 6 \<le> ptBits \<and> valid_objs' s \<and> vmsz_aligned' vptr vmpage_size \<and> vmpage_size \<noteq> ARMSuperSection) \<and> (vmpage_size = ARMSection \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> vs_valid_duplicates' (ksPSpace s) \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0 \<and> True) \<and> (pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<and> vmsz_aligned' vptr vmpage_size \<and> valid_objs' s \<and> True proof (prove)
goal:
No subgoals!