theory VSpace_R

lemma perform_pt_invs [wp]:
  notes no_irq[wp]
  shows
  "\<lbrace>invs' and valid_page_inv' pt\<rbrace> performPageInvocation pt \<lbrace>\<lambda>_. invs'\<rbrace>" apply (simp add: performPageInvocation_def) apply (cases pt) apply clarsimp apply ((wp dmo_invs' hoare_vcg_all_lift setVMRootForFlush_invs' | simp add: tcb_at_invs')+)[2] apply (rule hoare_pre_imp[of _ \<top>], assumption) apply (clarsimp simp: valid_def
                             disj_commute[of "pointerInUserData p s" for p s]) apply (thin_tac "x : fst (setVMRootForFlush a b s)" for x a b) apply (erule use_valid) apply (clarsimp simp: doFlush_def split: flush_type.splits) apply (clarsimp split: sum.split | intro conjI impI
               | wp)+ apply (clarsimp simp: valid_page_inv'_def valid_slots'_def
                           valid_pde_slots'_def
                    split: sum.split option.splits | intro conjI impI
            | wp mapM_storePTE_invs mapM_storePDE_invs
                 hoare_vcg_all_lift hoare_vcg_const_imp_lift
                 arch_update_updateCap_invs unmapPage_cte_wp_at' getSlotCap_wp
            | wpc)+ apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte) apply clarsimp apply (drule ctes_of_valid_cap', fastforce) apply (clarsimp simp: valid_cap'_def cte_wp_at_ctes_of valid_page_inv'_def
                         capAligned_def is_arch_update'_def isCap_simps) apply clarsimp apply (wp arch_update_updateCap_invs unmapPage_cte_wp_at' getSlotCap_wp|wpc)+ apply (rename_tac acap word a b) apply (rule_tac Q="\<lambda>_. invs' and cte_wp_at' (\<lambda>cte. \<exists>d r R sz m. cteCap cte =
                                       ArchObjectCap (PageCap d r R sz m)) word"
               in hoare_strengthen_post) apply (wp unmapPage_cte_wp_at') apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte) apply clarsimp apply (frule ctes_of_valid_cap') apply (auto simp: valid_page_inv'_def valid_slots'_def
                      cte_wp_at_ctes_of valid_pde_slots'_def)[1] apply (simp add: is_arch_update'_def isCap_simps) apply (simp add: valid_cap'_def capAligned_def) apply (clarsimp simp: cte_wp_at_ctes_of) apply (simp add: is_arch_update'_def isCap_simps) apply (case_tac cte) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_page_inv' pt\<rbrace> performPageInvocation pt \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x1. pt = ARM_H.PageGetAddr x1 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>x21 x22 x23 x24 x25 x26. pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 3. \<And>x31 x32 x33 x34. pt = ARM_H.PageMap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 4. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x1. pt = ARM_H.PageGetAddr x1 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' (ARM_H.PageGetAddr x1)\<rbrace> return [ARM_H.fromPAddr (addrFromPPtr x1)] \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>x21 x22 x23 x24 x25 x26. pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 3. \<And>x31 x32 x33 x34. pt = ARM_H.PageMap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 4. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24 x25 x26 m. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23\<rbrakk> \<Longrightarrow> \<lbrace>?P29 x21 x22 x23 x24 x25 x26 m\<rbrace> setVMRootForFlush x25 x26 \<lbrace>\<lambda>rv s. \<forall>x\<in>fst (doFlush x21 x22 x23 x24 m). case x of (r, m') \<Rightarrow> \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>x21 x22 x23 x24 x25 x26. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 x21 x22 x23 x24 x25 x26\<rbrace> setVMRootForFlush x25 x26 \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x21 x22 x23 x24 x25 x26 s. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; (invs' and valid_page_inv' (ARM_H.PageFlush x21 x22 x23 x24 x25 x26)) s\<rbrakk> \<Longrightarrow> (if x22 < x23 then \<lambda>s. (\<forall>x. ?P29 x21 x22 x23 x24 x25 x26 x s) \<and> ?P'28 x21 x22 x23 x24 x25 x26 s else invs') s
 4. \<And>x31 x32 x33 x34. pt = ARM_H.PageMap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 5. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24 x25 x26 m. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> setVMRootForFlush x25 x26 \<lbrace>\<lambda>rv s. \<forall>x\<in>fst (doFlush x21 x22 x23 x24 m). case x of (r, m') \<Rightarrow> \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>x21 x22 x23 x24 x25 x26. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 x21 x22 x23 x24 x25 x26\<rbrace> setVMRootForFlush x25 x26 \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x21 x22 x23 x24 x25 x26 s. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; (invs' and valid_page_inv' (ARM_H.PageFlush x21 x22 x23 x24 x25 x26)) s\<rbrakk> \<Longrightarrow> (if x22 < x23 then \<lambda>s. (\<forall>x. True) \<and> ?P'28 x21 x22 x23 x24 x25 x26 s else invs') s
 4. \<And>x31 x32 x33 x34. pt = ARM_H.PageMap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 5. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24 x25 x26 m s a b ba p. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23; (a, b) \<in> fst (setVMRootForFlush x25 x26 s); ((), ba) \<in> fst (doFlush x21 x22 x23 x24 m); \<not> pointerInDeviceData p b; \<not> pointerInUserData p b\<rbrakk> \<Longrightarrow> underlying_memory ba p = underlying_memory m p
 2. \<And>x21 x22 x23 x24 x25 x26. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 x21 x22 x23 x24 x25 x26\<rbrace> setVMRootForFlush x25 x26 \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x21 x22 x23 x24 x25 x26 s. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; (invs' and valid_page_inv' (ARM_H.PageFlush x21 x22 x23 x24 x25 x26)) s\<rbrakk> \<Longrightarrow> (if x22 < x23 then \<lambda>s. (\<forall>x. True) \<and> ?P'28 x21 x22 x23 x24 x25 x26 s else invs') s
 4. \<And>x31 x32 x33 x34. pt = ARM_H.PageMap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 5. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24 x25 x26 m s a b ba p. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23; ((), ba) \<in> fst (doFlush x21 x22 x23 x24 m); \<not> pointerInDeviceData p b; \<not> pointerInUserData p b\<rbrakk> \<Longrightarrow> underlying_memory ba p = underlying_memory m p
 2. \<And>x21 x22 x23 x24 x25 x26. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 x21 x22 x23 x24 x25 x26\<rbrace> setVMRootForFlush x25 x26 \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>x21 x22 x23 x24 x25 x26 s. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; (invs' and valid_page_inv' (ARM_H.PageFlush x21 x22 x23 x24 x25 x26)) s\<rbrakk> \<Longrightarrow> (if x22 < x23 then \<lambda>s. (\<forall>x. True) \<and> ?P'28 x21 x22 x23 x24 x25 x26 s else invs') s
 4. \<And>x31 x32 x33 x34. pt = ARM_H.PageMap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 5. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 x24 x25 x26 m s a b ba p. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23; \<not> pointerInDeviceData p b; \<not> pointerInUserData p b\<rbrakk> \<Longrightarrow> \<lbrace>?P51 x21 x22 x23 x24 x25 x26 m s a b ba p\<rbrace> doFlush x21 x22 x23 x24 \<lbrace>\<lambda>a b. underlying_memory b p = underlying_memory m p\<rbrace>
 2. \<And>x21 x22 x23 x24 x25 x26 m s a b ba p. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23; \<not> pointerInDeviceData p b; \<not> pointerInUserData p b\<rbrakk> \<Longrightarrow> ?P51 x21 x22 x23 x24 x25 x26 m s a b ba p m
 3. \<And>x21 x22 x23 x24 x25 x26. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 x21 x22 x23 x24 x25 x26\<rbrace> setVMRootForFlush x25 x26 \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x21 x22 x23 x24 x25 x26 s. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; (invs' and valid_page_inv' (ARM_H.PageFlush x21 x22 x23 x24 x25 x26)) s\<rbrakk> \<Longrightarrow> (if x22 < x23 then \<lambda>s. (\<forall>x. True) \<and> ?P'28 x21 x22 x23 x24 x25 x26 s else invs') s
 5. \<And>x31 x32 x33 x34. pt = ARM_H.PageMap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 6. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 x24 x25 x26 m s a b ba p. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23; \<not> pointerInDeviceData p b; \<not> pointerInUserData p b\<rbrakk> \<Longrightarrow> (x21 = ARM_H.Clean \<longrightarrow> \<lbrace>?P51 ARM_H.Clean x22 x23 x24 x25 x26 m s a b ba p\<rbrace> cleanCacheRange_RAM x22 x23 x24 \<lbrace>\<lambda>a b. underlying_memory b p = underlying_memory m p\<rbrace>) \<and> (x21 = ARM_H.Invalidate \<longrightarrow> \<lbrace>?P51 ARM_H.Invalidate x22 x23 x24 x25 x26 m s a b ba p\<rbrace> invalidateCacheRange_RAM x22 x23 x24 \<lbrace>\<lambda>a b. underlying_memory b p = underlying_memory m p\<rbrace>) \<and> (x21 = ARM_H.CleanInvalidate \<longrightarrow> \<lbrace>?P51 ARM_H.CleanInvalidate x22 x23 x24 x25 x26 m s a b ba p\<rbrace> cleanInvalidateCacheRange_RAM x22 x23 x24 \<lbrace>\<lambda>a b. underlying_memory b p = underlying_memory m p\<rbrace>) \<and> (x21 = ARM_H.Unify \<longrightarrow> \<lbrace>?P51 ARM_H.Unify x22 x23 x24 x25 x26 m s a b ba p\<rbrace> do y <- cleanCacheRange_PoU x22 x23 x24;
y <- dsb;
y <- invalidateCacheRange_I x22 x23 x24;
y <- branchFlushRange x22 x23 x24;
isb
od \<lbrace>\<lambda>a b. underlying_memory b p = underlying_memory m p\<rbrace>)
 2. \<And>x21 x22 x23 x24 x25 x26 m s a b ba p. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23; \<not> pointerInDeviceData p b; \<not> pointerInUserData p b\<rbrakk> \<Longrightarrow> ?P51 x21 x22 x23 x24 x25 x26 m s a b ba p m
 3. \<And>x21 x22 x23 x24 x25 x26. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; x22 < x23\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 x21 x22 x23 x24 x25 x26\<rbrace> setVMRootForFlush x25 x26 \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>x21 x22 x23 x24 x25 x26 s. \<lbrakk>pt = ARM_H.PageFlush x21 x22 x23 x24 x25 x26; (invs' and valid_page_inv' (ARM_H.PageFlush x21 x22 x23 x24 x25 x26)) s\<rbrakk> \<Longrightarrow> (if x22 < x23 then \<lambda>s. (\<forall>x. True) \<and> ?P'28 x21 x22 x23 x24 x25 x26 s else invs') s
 5. \<And>x31 x32 x33 x34. pt = ARM_H.PageMap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 6. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 a b tlbFlush. pt = ARM_H.PageMap x31 x32 x33 (Inl (a, b)) \<Longrightarrow> \<lbrace>?B136 x31 x32 x33 a b () tlbFlush\<rbrace> mapM (swp storePTE a) b \<lbrace>\<lambda>a. invs'\<rbrace>
 2. \<And>x31 x32 x33 a b y. pt = ARM_H.PageMap x31 x32 x33 (Inl (a, b)) \<Longrightarrow> \<lbrace>?B133 x31 x32 x33 a b y\<rbrace> pteCheckIfMapped (hd b) \<lbrace>?B136 x31 x32 x33 a b y\<rbrace>
 3. \<And>x31 x32 x33 a b. pt = ARM_H.PageMap x31 x32 x33 (Inl (a, b)) \<Longrightarrow> \<lbrace>?Q132 x31 x32 x33 a b\<rbrace> updateCap x33 x32 \<lbrace>?B133 x31 x32 x33 a b\<rbrace>
 4. \<And>x31 x32 x33 a b s. \<lbrakk>pt = ARM_H.PageMap x31 x32 x33 (Inl (a, b)); (invs' and valid_page_inv' (ARM_H.PageMap x31 x32 x33 (Inl (a, b)))) s\<rbrakk> \<Longrightarrow> ?Q132 x31 x32 x33 a b s
 5. \<And>x31 x32 x33 x34. pt = ARM_H.PageMap x31 x32 x33 x34 \<Longrightarrow> \<forall>a b. x34 = Inr (a, b) \<longrightarrow> \<lbrace>invs' and valid_page_inv' (ARM_H.PageMap x31 x32 x33 (Inr (a, b)))\<rbrace> do y <- updateCap x33 x32;
y <- do tlbFlush <- pdeCheckIfMapped (hd b);
y <- mapM (swp storePDE a) b;
y <- doMachineOp (cleanCacheRange_PoU (hd b) (last b + (2 ^ pdeBits - 1)) (addrFromPPtr (hd b)));
when tlbFlush (invalidateTLBByASID x31)
od;
return []
od \<lbrace>\<lambda>_. invs'\<rbrace>
 6. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<lbrace>invs' and valid_page_inv' pt\<rbrace> case pt of ARM_H.PageGetAddr ptr \<Rightarrow> return [ARM_H.fromPAddr $ addrFromPPtr ptr] | ARM_H.PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od;
return []
od | ARM_H.PageMap asid cap ctSlot entries \<Rightarrow> do updateCap ctSlot cap;
case entries 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 asid
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 asid
od;
return []
od | ARM_H.PageUnmap cap ctSlot \<Rightarrow> do case capVPMappedAddress cap of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmapPage (capVPSize cap) asid vaddr (capVPBasePtr cap);
cap <- liftM capCap $ getSlotCap ctSlot;
updateCap ctSlot (capability.ArchObjectCap $ capVPMappedAddress_update (\<lambda>_. Nothing) cap);
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x42 s d r R sz. \<lbrakk>pt = ARM_H.PageUnmap (arch_capability.PageCap d r R sz None) x42; invs' s; cte_wp_at' (is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None))) x42 s; valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) x42 s \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) (capCap cap)))) x42 s \<and> valid_cap' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) (capCap cap))) s
 2. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<forall>a b. capVPMappedAddress x41 = Some (a, b) \<longrightarrow> \<lbrace>invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)\<rbrace> do y <- unmapPage (capVPSize x41) a b (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x42 s d r R sz cte. \<lbrakk>pt = ARM_H.PageUnmap (arch_capability.PageCap d r R sz None) x42; invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s; ctes_of s x42 = Some cte; is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) cte\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) (capCap (cteCap cte)))) cte \<and> valid_cap' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) (capCap (cteCap cte)))) s
 2. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<forall>a b. capVPMappedAddress x41 = Some (a, b) \<longrightarrow> \<lbrace>invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)\<rbrace> do y <- unmapPage (capVPSize x41) a b (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x42 s d r R sz cte x1 x2. \<lbrakk>pt = ARM_H.PageUnmap (arch_capability.PageCap d r R sz None) x42; invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s; ctes_of s x42 = Some cte; is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) cte; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) (capCap (cteCap cte)))) cte \<and> valid_cap' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) (capCap (cteCap cte)))) s
 2. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<forall>a b. capVPMappedAddress x41 = Some (a, b) \<longrightarrow> \<lbrace>invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)\<rbrace> do y <- unmapPage (capVPSize x41) a b (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x42 s d r R sz x1 x2. \<lbrakk>pt = ARM_H.PageUnmap (arch_capability.PageCap d r R sz None) x42; invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s; ctes_of s x42 = Some (CTE x1 x2); is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) (CTE x1 x2)\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) (capCap x1))) (CTE x1 x2) \<and> valid_cap' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) (capCap x1))) s
 2. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<forall>a b. capVPMappedAddress x41 = Some (a, b) \<longrightarrow> \<lbrace>invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)\<rbrace> do y <- unmapPage (capVPSize x41) a b (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x42 s d r R sz x1 x2. \<lbrakk>pt = ARM_H.PageUnmap (arch_capability.PageCap d r R sz None) x42; invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s; is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) (CTE x1 x2); valid_cap' x1 s\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) (capCap x1))) (CTE x1 x2) \<and> valid_cap' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) (capCap x1))) s
 2. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<forall>a b. capVPMappedAddress x41 = Some (a, b) \<longrightarrow> \<lbrace>invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)\<rbrace> do y <- unmapPage (capVPSize x41) a b (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42. pt = ARM_H.PageUnmap x41 x42 \<Longrightarrow> \<forall>a b. capVPMappedAddress x41 = Some (a, b) \<longrightarrow> \<lbrace>invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)\<rbrace> do y <- unmapPage (capVPSize x41) a b (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 a b. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)\<rbrace> do y <- unmapPage (capVPSize x41) a b (capVPBasePtr x41);
cap <- liftM capCap (getSlotCap x42);
y <- updateCap x42 (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap));
return []
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 a b. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q274 x41 x42 a b\<rbrace> unmapPage (capVPSize x41) a b (capVPBasePtr x41) \<lbrace>\<lambda>y s. \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) x42 s \<and> ((\<lambda>cap s. cte_wp_at' (is_arch_update' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap))) x42 s \<and> invs' s \<and> valid_cap' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap)) s) \<circ> capCap) cap s\<rbrace>
 2. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> ?Q274 x41 x42 a b s proof (prove)
goal (2 subgoals):
 1. \<And>acap word a b. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q274 acap word a b\<rbrace> unmapPage (capVPSize acap) a b (capVPBasePtr acap) \<lbrace>\<lambda>y s. \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) word s \<and> ((\<lambda>cap s. cte_wp_at' (is_arch_update' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap))) word s \<and> invs' s \<and> valid_cap' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap)) s) \<circ> capCap) cap s\<rbrace>
 2. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> ?Q274 x41 x42 a b s proof (prove)
goal (3 subgoals):
 1. \<And>acap word a b. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?Q274 acap word a b\<rbrace> unmapPage (capVPSize acap) a b (capVPBasePtr acap) \<lbrace>\<lambda>_. invs' and cte_wp_at' (\<lambda>cte. \<exists>d r R sz m. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) word\<rbrace>
 2. \<And>acap word a b rv s. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b); (invs' and cte_wp_at' (\<lambda>cte. \<exists>d r R sz m. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) word) s\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) word s \<and> ((\<lambda>cap s. cte_wp_at' (is_arch_update' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap))) word s \<and> invs' s \<and> valid_cap' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap)) s) \<circ> capCap) cap s
 3. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> ?Q274 x41 x42 a b s proof (prove)
goal (2 subgoals):
 1. \<And>acap word a b rv s. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b); (invs' and cte_wp_at' (\<lambda>cte. \<exists>d r R sz m. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) word) s\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) word s \<and> ((\<lambda>cap s. cte_wp_at' (is_arch_update' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap))) word s \<and> invs' s \<and> valid_cap' (capability.ArchObjectCap (capVPMappedAddress_update (\<lambda>_. None) cap)) s) \<circ> capCap) cap s
 2. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>a. \<exists>d r R sz m. cteCap a = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x42 s proof (prove)
goal (2 subgoals):
 1. \<And>acap word a b s cte d r R sz m. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b); invs' s; ctes_of s word = Some cte; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) cte \<and> valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s
 2. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>a. \<exists>d r R sz m. cteCap a = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x42 s proof (prove)
goal (2 subgoals):
 1. \<And>acap word a b s cte d r R sz m x1 x2. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b); invs' s; ctes_of s word = Some cte; cteCap cte = capability.ArchObjectCap (arch_capability.PageCap d r R sz m); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) cte \<and> valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s
 2. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>a. \<exists>d r R sz m. cteCap a = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x42 s proof (prove)
goal (2 subgoals):
 1. \<And>acap word a b s d r R sz m x2. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b); invs' s; ctes_of s word = Some (CTE (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x2)\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) (CTE (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x2) \<and> valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s
 2. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>a. \<exists>d r R sz m. cteCap a = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x42 s proof (prove)
goal (3 subgoals):
 1. \<And>acap word a b s d r R sz m x2. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b); invs' s; ctes_of s word = Some (CTE (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x2)\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>acap word a b s d r R sz m x2. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b); invs' s; ctes_of s word = Some (CTE (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x2); valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) s\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) (CTE (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x2) \<and> valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s
 3. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>a. \<exists>d r R sz m. cteCap a = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x42 s proof (prove)
goal (2 subgoals):
 1. \<And>acap word a b s d r R sz m x2. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b); invs' s; ctes_of s word = Some (CTE (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x2); valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) s\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) (CTE (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x2) \<and> valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s
 2. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>a. \<exists>d r R sz m. cteCap a = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x42 s proof (prove)
goal (2 subgoals):
 1. \<And>acap word a b s d r R sz m x2. \<lbrakk>pt = ARM_H.PageUnmap acap word; capVPMappedAddress acap = Some (a, b); invs' s; ctes_of s word = Some (CTE (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x2); valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) s\<rbrakk> \<Longrightarrow> valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz None)) s
 2. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>a. \<exists>d r R sz m. cteCap a = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x42 s proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 a b s. \<lbrakk>pt = ARM_H.PageUnmap x41 x42; capVPMappedAddress x41 = Some (a, b); (invs' and (\<lambda>s. (\<exists>d r R sz m. x41 = arch_capability.PageCap d r R sz m) \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap x41)) x42 s \<and> valid_cap' (capability.ArchObjectCap x41) s)) s\<rbrakk> \<Longrightarrow> invs' s \<and> cte_wp_at' (\<lambda>a. \<exists>d r R sz m. cteCap a = capability.ArchObjectCap (arch_capability.PageCap d r R sz m)) x42 s proof (prove)
goal (1 subgoal):
 1. \<And>x42 a b s d r R sz cte. \<lbrakk>pt = ARM_H.PageUnmap (arch_capability.PageCap d r R sz (Some (a, b))) x42; invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz (Some (a, b)))) s; ctes_of s x42 = Some cte; is_arch_update' (capability.ArchObjectCap (arch_capability.PageCap d r R sz (Some (a, b)))) cte\<rbrakk> \<Longrightarrow> \<exists>d r R sz m. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap d r R sz m) proof (prove)
goal (1 subgoal):
 1. \<And>x42 a b s d r R sz cte. \<lbrakk>pt = ARM_H.PageUnmap (arch_capability.PageCap d r R sz (Some (a, b))) x42; invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz (Some (a, b)))) s; ctes_of s x42 = Some cte; capability.ArchObjectCap (arch_capability.PageCap d r VMReadWrite sz None) = capMasterCap (cteCap cte)\<rbrakk> \<Longrightarrow> \<exists>d r R sz m. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap d r R sz m) proof (prove)
goal (1 subgoal):
 1. \<And>x42 a b s d r R sz cte x1 x2. \<lbrakk>pt = ARM_H.PageUnmap (arch_capability.PageCap d r R sz (Some (a, b))) x42; invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d r R sz (Some (a, b)))) s; ctes_of s x42 = Some cte; capability.ArchObjectCap (arch_capability.PageCap d r VMReadWrite sz None) = capMasterCap (cteCap cte); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>d r R sz m. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap d r R sz m) proof (prove)
goal:
No subgoals!