theory PageTableDuplicates

lemma performPageInvocation_valid_duplicates'[wp]:
  "\<lbrace>invs' and valid_arch_inv' (invocation.InvokePage page_invocation)
  and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
    performPageInvocation page_invocation
    \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>" apply (rule hoare_name_pre_state) apply (case_tac page_invocation)
  \<comment> \<open>PageFlush\<close> apply (simp_all add:performPageInvocation_def pteCheckIfMapped_def pdeCheckIfMapped_def) apply ((wp|simp|wpc)+)[2]
   \<comment> \<open>PageMap\<close> apply (clarsimp simp: pteCheckIfMapped_def pdeCheckIfMapped_def) apply (clarsimp simp:valid_pde_slots'_def valid_page_inv'_def
       valid_slots_duplicated'_def valid_arch_inv'_def ) apply (rename_tac word1 cap word2 sum) apply (case_tac sum) apply (case_tac a) apply (case_tac aa) apply (clarsimp simp: pteCheckIfMapped_def) apply (wp mapM_x_mapM_valid | wpc | simp)+ apply (clarsimp simp:valid_slots_duplicated'_def mapM_x_singleton)+ apply (rule PageTableDuplicates.storePTE_no_duplicates', rule getPTE_wp) apply (wp hoare_vcg_all_lift hoare_drop_imps) apply (simp add:vs_entry_align_def)+ apply (clarsimp simp: pteCheckIfMapped_def) apply (wp mapM_x_mapM_valid | simp)+ apply (rule_tac sz = 6 and ptr = "p && ~~ mask ptBits" and word = p in
         mapM_x_storePTE_update_helper) apply (wp getPTE_wp hoare_vcg_all_lift hoare_drop_imps)+ apply (simp add:ptBits_def pageBits_def)+ apply (simp add:invs_pspace_aligned') apply simp apply (clarsimp simp:mapM_singleton pteCheckIfMapped_def) apply (wp PageTableDuplicates.storePTE_no_duplicates' getPTE_wp hoare_drop_imps | simp)+ apply (simp add:vs_entry_align_def)+ apply (clarsimp simp: pdeCheckIfMapped_def) apply (case_tac a) apply (clarsimp simp:valid_arch_inv'_def
          valid_page_inv'_def valid_slots'_def
          valid_slots_duplicated'_def mapM_singleton) apply (wp PageTableDuplicates.storePDE_no_duplicates' getPDE_wp hoare_drop_imps | simp)+ apply (simp add:vs_entry_align_def)+ apply (clarsimp simp:valid_arch_inv'_def
          valid_page_inv'_def valid_slots'_def
          valid_slots_duplicated'_def mapM_singleton) apply (wp PageTableDuplicates.storePDE_no_duplicates' getPDE_wp hoare_drop_imps | simp)+ apply (simp add:vs_entry_align_def)+ apply (clarsimp simp:valid_arch_inv'_def
          valid_page_inv'_def valid_slots'_def
          valid_slots_duplicated'_def mapM_singleton) apply (wp PageTableDuplicates.storePDE_no_duplicates' getPDE_wp hoare_drop_imps | simp)+ apply (simp add:vs_entry_align_def)+ apply (clarsimp simp:valid_arch_inv'_def
          valid_page_inv'_def valid_slots'_def
          valid_slots_duplicated'_def mapM_x_singleton) apply (wp mapM_x_mapM_valid | simp)+ apply (rule_tac sz = 6 and ptr = "p && ~~ mask pdBits" and word = p
          in mapM_x_storePDE_update_helper) apply wp+ apply (simp add:pageBits_def pdBits_def ptBits_def)+ apply (simp add:invs_pspace_aligned')+ apply clarsimp apply (rule hoare_pre) apply (wp |wpc |simp)+ apply (clarsimp simp:valid_page_inv'_def
      valid_arch_inv'_def valid_cap'_def invs_valid_objs' invs_pspace_aligned') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage page_invocation) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> performPageInvocation page_invocation \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and valid_arch_inv' (invocation.InvokePage page_invocation) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> performPageInvocation page_invocation \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s x1. \<lbrakk>(invs' and valid_arch_inv' (invocation.InvokePage page_invocation) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s; page_invocation = ARM_H.PageGetAddr x1\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performPageInvocation page_invocation \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x21 x22 x23 x24 x25 x26. \<lbrakk>(invs' and valid_arch_inv' (invocation.InvokePage page_invocation) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s; page_invocation = ARM_H.PageFlush x21 x22 x23 x24 x25 x26\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performPageInvocation page_invocation \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x31 x32 x33 x34. \<lbrakk>(invs' and valid_arch_inv' (invocation.InvokePage page_invocation) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s; page_invocation = ARM_H.PageMap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performPageInvocation page_invocation \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s x41 x42. \<lbrakk>(invs' and valid_arch_inv' (invocation.InvokePage page_invocation) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s; page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> performPageInvocation page_invocation \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s x1. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageGetAddr x1)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageGetAddr x1\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> return [ARM_H.fromPAddr (addrFromPPtr x1)] \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x21 x22 x23 x24 x25 x26. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageFlush x21 x22 x23 x24 x25 x26)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageFlush x21 x22 x23 x24 x25 x26\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- when (x22 < x23) (do root_switched <- setVMRootForFlush x25 x26;
y <- doMachineOp (doFlush x21 x22 x23 x24);
when root_switched (getCurThread >>= setVMRoot)
od);
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x31 x32 x33 x34. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageMap x31 x32 x33 x34)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageMap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap x33 x32;
y <- case x34 of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID x31
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID x31
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s x31 x32 x33 x34. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageMap x31 x32 x33 x34)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageMap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap x33 x32;
y <- case x34 of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID x31
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID x31
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s x31 x32 x33 x34. \<lbrakk>page_invocation = ARM_H.PageMap x31 x32 x33 x34; invs' s; valid_arch_inv' (invocation.InvokePage (ARM_H.PageMap x31 x32 x33 x34)) s; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap x33 x32;
y <- case x34 of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID x31
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID x31
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s x31 x32 x33 x34. \<lbrakk>page_invocation = ARM_H.PageMap x31 x32 x33 x34; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' x32) x33 s; valid_slots' x34 s; valid_cap' x32 s; case x34 of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case x34 of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap x33 x32;
y <- case x34 of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID x31
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID x31
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s word1 cap word2 sum. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s word1 cap word2 sum a. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s word1 cap word2 sum a aa b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s word1 cap word2 sum a aa b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.InvalidPTE\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 sum a aa b x21 x22 x23 x24 x25. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 5. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s word1 cap word2 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pt <- getObject p;
y <- mapM (swp storePTE ARM_H.InvalidPTE) [p];
y <- doMachineOp (cleanCacheRange_PoU p (p + (2 ^ pteBits - 1)) (addrFromPPtr p));
when (pt \<noteq> ARM_H.InvalidPTE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 sum a aa b x21 x22 x23 x24 x25. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 5. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s word1 cap word2 p pt. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B61 s word1 cap word2 p () pt\<rbrace> mapM_x (swp storePTE ARM_H.InvalidPTE) [p] \<lbrace>\<lambda>r a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 p y. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B58 s word1 cap word2 p y\<rbrace> getObject p \<lbrace>?B61 s word1 cap word2 p y\<rbrace>
 3. \<And>s word1 cap word2 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 s word1 cap word2 p\<rbrace> updateCap word2 cap \<lbrace>?B58 s word1 cap word2 p\<rbrace>
 4. \<And>s word1 cap word2 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s; s = sa\<rbrakk> \<Longrightarrow> ?Q57 s word1 cap word2 p sa
 5. \<And>s word1 cap word2 sum a aa b x21 x22 x23 x24 x25. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 6. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 7. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 8. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s word1 cap word2 p pt. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B61 s word1 cap word2 p () pt\<rbrace> storePTE p ARM_H.InvalidPTE \<lbrace>\<lambda>r a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 p y. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B58 s word1 cap word2 p y\<rbrace> getObject p \<lbrace>?B61 s word1 cap word2 p y\<rbrace>
 3. \<And>s word1 cap word2 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 s word1 cap word2 p\<rbrace> updateCap word2 cap \<lbrace>?B58 s word1 cap word2 p\<rbrace>
 4. \<And>s word1 cap word2 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s; s = sa\<rbrakk> \<Longrightarrow> ?Q57 s word1 cap word2 p sa
 5. \<And>s word1 cap word2 sum a aa b x21 x22 x23 x24 x25. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 6. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 7. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 8. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s word1 cap word2 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 s word1 cap word2 p\<rbrace> updateCap word2 cap \<lbrace>\<lambda>y s. \<forall>ko. ko_at' ko p s \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0\<rbrace>
 2. \<And>s word1 cap word2 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s; s = sa\<rbrakk> \<Longrightarrow> ?Q57 s word1 cap word2 p sa
 3. \<And>s word1 cap word2 sum a aa b x21 x22 x23 x24 x25. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 5. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 6. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s word1 cap word2 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.InvalidPTE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.InvalidPTE, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s; s = sa\<rbrakk> \<Longrightarrow> \<forall>x. vs_valid_duplicates' (ksPSpace sa) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p sa \<and> vs_entry_align (KOArch (KOPTE ARM_H.InvalidPTE)) = 0
 2. \<And>s word1 cap word2 sum a aa b x21 x22 x23 x24 x25. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 5. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s word1 cap word2 sum a aa b x21 x22 x23 x24 x25. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b)) s; valid_cap' cap s; \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s; sum = Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); a = (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do tlbFlush <- pteCheckIfMapped (hd b);
y <- mapM (swp storePTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pteBits - 1)) (addrFromPPtr (hd b)));
when tlbFlush (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s word1 cap word2 x21 x22 x23 x24 x25 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])) s; valid_cap' cap s; is_aligned p 6; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pt <- getObject (hd [p , p + 4 .e. p + mask 6]);
y <- mapM (swp storePTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)) [p , p + 4 .e. p + mask 6];
y <- doMachineOp (cleanCacheRange_PoU (hd [p , p + 4 .e. p + mask 6]) (last [p , p + 4 .e. p + mask 6] + (2 ^ pteBits - 1)) (addrFromPPtr (hd [p , p + 4 .e. p + mask 6])));
when (pt \<noteq> ARM_H.InvalidPTE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s word1 cap word2 x21 x22 x23 x24 x25 p pt. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])) s; valid_cap' cap s; is_aligned p 6; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B105 s word1 cap word2 x21 x22 x23 x24 x25 p () pt\<rbrace> mapM_x (swp storePTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)) [p , p + 4 .e. p + mask 6] \<lbrace>\<lambda>r a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 x21 x22 x23 x24 x25 p y. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])) s; valid_cap' cap s; is_aligned p 6; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B102 s word1 cap word2 x21 x22 x23 x24 x25 p y\<rbrace> getObject (hd [p , p + 4 .e. p + mask 6]) \<lbrace>?B105 s word1 cap word2 x21 x22 x23 x24 x25 p y\<rbrace>
 3. \<And>s word1 cap word2 x21 x22 x23 x24 x25 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])) s; valid_cap' cap s; is_aligned p 6; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 s word1 cap word2 x21 x22 x23 x24 x25 p\<rbrace> updateCap word2 cap \<lbrace>?B102 s word1 cap word2 x21 x22 x23 x24 x25 p\<rbrace>
 4. \<And>s word1 cap word2 x21 x22 x23 x24 x25 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])) s; valid_cap' cap s; is_aligned p 6; page_table_at' (p && ~~ mask ptBits) s; s = sa\<rbrakk> \<Longrightarrow> ?Q101 s word1 cap word2 x21 x22 x23 x24 x25 p sa
 5. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 6. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 7. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s word1 cap word2 x21 x22 x23 x24 x25 p y. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])) s; valid_cap' cap s; is_aligned p 6; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B102 s word1 cap word2 x21 x22 x23 x24 x25 p y\<rbrace> getObject (hd [p , p + 4 .e. p + mask 6]) \<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> [p , p + 4 .e. p + mask 6] = [p , p + 4 .e. p + mask 6]\<rbrace>
 2. \<And>s word1 cap word2 x21 x22 x23 x24 x25 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])) s; valid_cap' cap s; is_aligned p 6; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q101 s word1 cap word2 x21 x22 x23 x24 x25 p\<rbrace> updateCap word2 cap \<lbrace>?B102 s word1 cap word2 x21 x22 x23 x24 x25 p\<rbrace>
 3. \<And>s word1 cap word2 x21 x22 x23 x24 x25 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])) s; valid_cap' cap s; is_aligned p 6; page_table_at' (p && ~~ mask ptBits) s; s = sa\<rbrakk> \<Longrightarrow> ?Q101 s word1 cap word2 x21 x22 x23 x24 x25 p sa
 4. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 5. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 6. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s word1 cap word2 x21 x22 x23 x24 x25 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])) s; valid_cap' cap s; is_aligned p 6; page_table_at' (p && ~~ mask ptBits) s; s = sa\<rbrakk> \<Longrightarrow> \<forall>x. vs_valid_duplicates' (ksPSpace sa) \<and> pspace_aligned' sa \<and> page_table_at' (p && ~~ mask ptBits) sa \<and> p && ~~ mask ptBits = p && ~~ mask ptBits \<and> 6 \<le> ptBits \<and> 6 \<le> 6 \<and> is_aligned p 6 \<and> [p , p + 4 .e. p + mask 6] = [p , p + 4 .e. p + mask 6]
 2. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s word1 cap word2 x21 x22 x23 x24 x25 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])); invs' sa; vs_valid_duplicates' (ksPSpace sa); cte_wp_at' (is_arch_update' cap) word2 sa; valid_slots' (Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, [p , p + 4 .e. p + mask 6])) sa; valid_cap' cap sa; is_aligned p 6; page_table_at' (p && ~~ mask (8 + pteBits)) sa; s = sa\<rbrakk> \<Longrightarrow> pspace_aligned' sa
 2. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s word1 cap word2 sum a aa b x31 x32 x33 x34 x35. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b)) s; valid_cap' cap s; \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s; sum = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do tlbFlush <- pteCheckIfMapped (hd b);
y <- mapM (swp storePTE (ARM_H.SmallPagePTE x31 x32 x33 x34 x35)) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pteBits - 1)) (addrFromPPtr (hd b)));
when tlbFlush (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s word1 cap word2 x31 x32 x33 x34 x35 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p])) s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pt <- getObject p;
r <- storePTE p (ARM_H.SmallPagePTE x31 x32 x33 x34 x35);
y <- doMachineOp (cleanCacheRange_PoU p (p + (2 ^ pteBits - 1)) (addrFromPPtr p));
when (pt \<noteq> ARM_H.InvalidPTE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s word1 cap word2 x31 x32 x33 x34 x35 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p])); invs' sa; vs_valid_duplicates' (ksPSpace sa); cte_wp_at' (is_arch_update' cap) word2 sa; valid_slots' (Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, [p])) sa; valid_cap' cap sa; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p sa; page_table_at' (p && ~~ mask ptBits) sa; s = sa\<rbrakk> \<Longrightarrow> vs_entry_align (KOArch (KOPTE (ARM_H.SmallPagePTE x31 x32 x33 x34 x35))) = 0
 2. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 sum; invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' sum s; valid_cap' cap s; case sum of Inl (pte, xs) \<Rightarrow> True | Inr (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case sum of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case sum of Inl (pte, slots) \<Rightarrow> do tlbFlush <- pteCheckIfMapped (head slots);
mapM (swp storePTE pte) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od | Inr (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (head slots);
mapM (swp storePDE pde) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots));
when tlbFlush $ invalidateTLBByASID word1
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s word1 cap word2 sum b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr b); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr b) s; valid_cap' cap s; case b of (pde, xs) \<Rightarrow> \<forall>x\<in>set xs. valid_pde_mapping' (x && mask pdBits) pde; case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; sum = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- case b of (pde, slots) \<Rightarrow> do tlbFlush <- pdeCheckIfMapped (hd slots);
y <- mapM (swp storePDE pde) slots;
y <- doMachineOp (cleanCacheRange_PoU (hd slots) (last slots + (2 ^ pdeBits - 1)) (addrFromPPtr (hd slots)));
when tlbFlush (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s word1 cap word2 a b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s word1 cap word2 a b. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 a b x21 x22 x23. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 a b x31 x32 x33 x34 x35 x36 x37. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s word1 cap word2 a b x41 x42 x43 x44 x45 x46. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 5. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s word1 cap word2 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.InvalidPDE, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_cap' cap s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject p;
r <- storePDE p ARM_H.InvalidPDE;
y <- doMachineOp (cleanCacheRange_PoU p (p + (2 ^ pdeBits - 1)) (addrFromPPtr p));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 a b x21 x22 x23. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 a b x31 x32 x33 x34 x35 x36 x37. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s word1 cap word2 a b x41 x42 x43 x44 x45 x46. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 5. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s word1 cap word2 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.InvalidPDE, [p])); invs' sa; vs_valid_duplicates' (ksPSpace sa); cte_wp_at' (is_arch_update' cap) word2 sa; valid_cap' cap sa; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p sa; page_directory_at' (p && ~~ mask pdBits) sa; s = sa\<rbrakk> \<Longrightarrow> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0
 2. \<And>s word1 cap word2 a b x21 x22 x23. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 a b x31 x32 x33 x34 x35 x36 x37. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s word1 cap word2 a b x41 x42 x43 x44 x45 x46. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 5. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s word1 cap word2 a b x21 x22 x23. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.PageTablePDE x21 x22 x23, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (ARM_H.PageTablePDE x21 x22 x23, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits); \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. (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) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE (ARM_H.PageTablePDE x21 x22 x23)) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 a b x31 x32 x33 x34 x35 x36 x37. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 a b x41 x42 x43 x44 x45 x46. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s word1 cap word2 x21 x22 x23 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.PageTablePDE x21 x22 x23, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; is_aligned x21 ptBits; valid_cap' cap s; valid_pde_mapping_offset' (p && mask pdBits); ko_wp_at' (\<lambda>ko. (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) p s; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject p;
r <- storePDE p (ARM_H.PageTablePDE x21 x22 x23);
y <- doMachineOp (cleanCacheRange_PoU p (p + (2 ^ pdeBits - 1)) (addrFromPPtr p));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 a b x31 x32 x33 x34 x35 x36 x37. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 a b x41 x42 x43 x44 x45 x46. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s word1 cap word2 x21 x22 x23 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.PageTablePDE x21 x22 x23, [p])); invs' sa; vs_valid_duplicates' (ksPSpace sa); cte_wp_at' (is_arch_update' cap) word2 sa; is_aligned x21 ptBits; valid_cap' cap sa; valid_pde_mapping_offset' (p && mask pdBits); ko_wp_at' (\<lambda>ko. (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) p sa; page_directory_at' (p && ~~ mask pdBits) sa; s = sa\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p sa \<and> vs_entry_align (KOArch (KOPDE (ARM_H.PageTablePDE x21 x22 x23))) = 0
 2. \<And>s word1 cap word2 a b x31 x32 x33 x34 x35 x36 x37. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s word1 cap word2 a b x41 x42 x43 x44 x45 x46. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 4. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s word1 cap word2 a b x31 x32 x33 x34 x35 x36 x37. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits); \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. (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) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37)) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 a b x41 x42 x43 x44 x45 x46. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s word1 cap word2 x31 x32 x33 x34 x35 x36 x37 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_mapping' x31 ARMSection s; valid_cap' cap s; valid_pde_mapping_offset' (p && mask pdBits); ko_wp_at' (\<lambda>ko. (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) p s; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject p;
r <- storePDE p (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37);
y <- doMachineOp (cleanCacheRange_PoU p (p + (2 ^ pdeBits - 1)) (addrFromPPtr p));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 a b x41 x42 x43 x44 x45 x46. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s word1 cap word2 x31 x32 x33 x34 x35 x36 x37 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, [p])); invs' sa; vs_valid_duplicates' (ksPSpace sa); cte_wp_at' (is_arch_update' cap) word2 sa; valid_mapping' x31 ARMSection sa; valid_cap' cap sa; valid_pde_mapping_offset' (p && mask pdBits); ko_wp_at' (\<lambda>ko. (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) p sa; page_directory_at' (p && ~~ mask pdBits) sa; s = sa\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p sa \<and> vs_entry_align (KOArch (KOPDE (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37))) = 0
 2. \<And>s word1 cap word2 a b x41 x42 x43 x44 x45 x46. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (a, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (a, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping' (x && mask pdBits) a; case a of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | _ \<Rightarrow> \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s word1 cap word2 a b x41 x42 x43 x44 x45 x46. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, b)); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_slots' (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, b)) s; valid_cap' cap s; \<forall>x\<in>set b. valid_pde_mapping_offset' (x && mask pdBits); \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s; a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd b);
y <- mapM (swp storePDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s word1 cap word2 x41 x42 x43 x44 x45 x46 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_mapping' x41 ARMSuperSection s; valid_cap' cap s; \<forall>x\<in>set [p , p + 4 .e. p + mask 6]. valid_pde_mapping_offset' (x && mask pdBits); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- updateCap word2 cap;
y <- do pd <- getObject (hd [p , p + 4 .e. p + mask 6]);
y <- mapM (swp storePDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)) [p , p + 4 .e. p + mask 6];
y <- doMachineOp (cleanCacheRange_PoU (hd [p , p + 4 .e. p + mask 6]) (last [p , p + 4 .e. p + mask 6] + (2 ^ pdeBits - 1)) (addrFromPPtr (hd [p , p + 4 .e. p + mask 6])));
when (pd \<noteq> ARM_H.InvalidPDE) (invalidateTLBByASID word1)
od;
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s word1 cap word2 x41 x42 x43 x44 x45 x46 p pd. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_mapping' x41 ARMSuperSection s; valid_cap' cap s; \<forall>x\<in>set [p , p + 4 .e. p + mask 6]. valid_pde_mapping_offset' (x && mask pdBits); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B303 s word1 cap word2 x41 x42 x43 x44 x45 x46 p () pd\<rbrace> mapM_x (swp storePDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)) [p , p + 4 .e. p + mask 6] \<lbrace>\<lambda>r a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s word1 cap word2 x41 x42 x43 x44 x45 x46 p y. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_mapping' x41 ARMSuperSection s; valid_cap' cap s; \<forall>x\<in>set [p , p + 4 .e. p + mask 6]. valid_pde_mapping_offset' (x && mask pdBits); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B300 s word1 cap word2 x41 x42 x43 x44 x45 x46 p y\<rbrace> getObject (hd [p , p + 4 .e. p + mask 6]) \<lbrace>?B303 s word1 cap word2 x41 x42 x43 x44 x45 x46 p y\<rbrace>
 3. \<And>s word1 cap word2 x41 x42 x43 x44 x45 x46 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_mapping' x41 ARMSuperSection s; valid_cap' cap s; \<forall>x\<in>set [p , p + 4 .e. p + mask 6]. valid_pde_mapping_offset' (x && mask pdBits); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q299 s word1 cap word2 x41 x42 x43 x44 x45 x46 p\<rbrace> updateCap word2 cap \<lbrace>?B300 s word1 cap word2 x41 x42 x43 x44 x45 x46 p\<rbrace>
 4. \<And>s word1 cap word2 x41 x42 x43 x44 x45 x46 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_mapping' x41 ARMSuperSection s; valid_cap' cap s; \<forall>x\<in>set [p , p + 4 .e. p + mask 6]. valid_pde_mapping_offset' (x && mask pdBits); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s; s = sa\<rbrakk> \<Longrightarrow> ?Q299 s word1 cap word2 x41 x42 x43 x44 x45 x46 p sa
 5. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s word1 cap word2 x41 x42 x43 x44 x45 x46 p y. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_mapping' x41 ARMSuperSection s; valid_cap' cap s; \<forall>x\<in>set [p , p + 4 .e. p + mask 6]. valid_pde_mapping_offset' (x && mask pdBits); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?B300 s word1 cap word2 x41 x42 x43 x44 x45 x46 p y\<rbrace> getObject (hd [p , p + 4 .e. p + mask 6]) \<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> [p , p + 4 .e. p + mask 6] = [p , p + 4 .e. p + mask 6]\<rbrace>
 2. \<And>s word1 cap word2 x41 x42 x43 x44 x45 x46 p. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_mapping' x41 ARMSuperSection s; valid_cap' cap s; \<forall>x\<in>set [p , p + 4 .e. p + mask 6]. valid_pde_mapping_offset' (x && mask pdBits); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q299 s word1 cap word2 x41 x42 x43 x44 x45 x46 p\<rbrace> updateCap word2 cap \<lbrace>?B300 s word1 cap word2 x41 x42 x43 x44 x45 x46 p\<rbrace>
 3. \<And>s word1 cap word2 x41 x42 x43 x44 x45 x46 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_mapping' x41 ARMSuperSection s; valid_cap' cap s; \<forall>x\<in>set [p , p + 4 .e. p + mask 6]. valid_pde_mapping_offset' (x && mask pdBits); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s; s = sa\<rbrakk> \<Longrightarrow> ?Q299 s word1 cap word2 x41 x42 x43 x44 x45 x46 p sa
 4. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s word1 cap word2 x41 x42 x43 x44 x45 x46 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, [p , p + 4 .e. p + mask 6])); invs' s; vs_valid_duplicates' (ksPSpace s); cte_wp_at' (is_arch_update' cap) word2 s; valid_mapping' x41 ARMSuperSection s; valid_cap' cap s; \<forall>x\<in>set [p , p + 4 .e. p + mask 6]. valid_pde_mapping_offset' (x && mask pdBits); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s; s = sa\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace sa) \<and> pspace_aligned' sa \<and> page_directory_at' (p && ~~ mask pdBits) sa \<and> p && ~~ mask pdBits = p && ~~ mask pdBits \<and> 6 \<le> pdBits \<and> 6 \<le> 6 \<and> is_aligned p 6 \<and> [p , p + 4 .e. p + mask 6] = [p , p + 4 .e. p + mask 6]
 2. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s word1 cap word2 x41 x42 x43 x44 x45 x46 p sa. \<lbrakk>page_invocation = ARM_H.PageMap word1 cap word2 (Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, [p , p + 4 .e. p + mask 6])); invs' sa; vs_valid_duplicates' (ksPSpace sa); cte_wp_at' (is_arch_update' cap) word2 sa; valid_mapping' x41 ARMSuperSection sa; valid_cap' cap sa; \<forall>x\<in>set [p , p + 4 .e. p + mask 6]. valid_pde_mapping_offset' (x && mask (12 + pdeBits)); is_aligned p 6; page_directory_at' (p && ~~ mask (12 + pdeBits)) sa; s = sa\<rbrakk> \<Longrightarrow> pspace_aligned' sa
 2. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x41 x42. \<lbrakk>invs' s \<and> valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s \<and> vs_valid_duplicates' (ksPSpace s); page_invocation = ARM_H.PageUnmap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x41 x42. \<lbrakk>page_invocation = ARM_H.PageUnmap x41 x42; invs' s; valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s x41 x42. \<lbrakk>page_invocation = ARM_H.PageUnmap x41 x42; invs' s; valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> \<lbrace>?Q332 s x41 x42\<rbrace> do y <- case capVPMappedAddress x41 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize x41) asid vaddr (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>s x41 x42 sa. \<lbrakk>page_invocation = ARM_H.PageUnmap x41 x42; invs' s; valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) s; vs_valid_duplicates' (ksPSpace s); s = sa\<rbrakk> \<Longrightarrow> ?Q332 s x41 x42 sa proof (prove)
goal (1 subgoal):
 1. \<And>s x41 x42 sa. \<lbrakk>page_invocation = ARM_H.PageUnmap x41 x42; invs' sa; valid_arch_inv' (invocation.InvokePage (ARM_H.PageUnmap x41 x42)) sa; vs_valid_duplicates' (ksPSpace sa); s = sa\<rbrakk> \<Longrightarrow> \<forall>a b. capVPMappedAddress x41 = Some (a, b) \<longrightarrow> pspace_aligned' sa \<and> valid_objs' sa \<and> vmsz_aligned' b (capVPSize x41) proof (prove)
goal:
No subgoals!