theory VSpace_R

lemma unmapPage_invs' [wp]:
  "\<lbrace>invs'\<rbrace> unmapPage sz asid vptr pptr \<lbrace>\<lambda>_. invs'\<rbrace>" apply (simp add: unmapPage_def) apply (rule hoare_pre) apply (wp lookupPTSlot_inv
             mapM_storePTE_invs mapM_storePDE_invs
             hoare_vcg_const_imp_lift
         |wpc
         |simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> unmapPage sz asid vptr pptr \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> ignoreFailure (doE pd <- findPDForASID asid;
y <- case sz of ARMSmallPage \<Rightarrow> doE p <- lookupPTSlot pd vptr;
checkMappingPPtr pptr sz (Inl p);
withoutFailure $ do storePTE p ARM_H.InvalidPTE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookupPTSlot pd vptr;
checkMappingPPtr pptr sz (Inl p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) largePagePTEOffsets);
mapM (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr pptr sz (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr pptr sz (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE;
liftE (flushPage sz pd asid vptr)
odE) \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> ignoreFailure (doE pd <- findPDForASID asid;
y <- case sz of ARMSmallPage \<Rightarrow> doE p <- lookupPTSlot pd vptr;
checkMappingPPtr pptr sz (Inl p);
withoutFailure $ do storePTE p ARM_H.InvalidPTE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE | ARMLargePage \<Rightarrow> doE p <- lookupPTSlot pd vptr;
checkMappingPPtr pptr sz (Inl p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) largePagePTEOffsets);
mapM (swp storePTE ARM_H.InvalidPTE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pteBits - 1)) (addrFromPPtr (head slots))
od
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr pptr sz (Inr p);
withoutFailure $ do storePDE p ARM_H.InvalidPDE;
doMachineOp $ cleanByVA_PoU (VPtr $ fromPPtr p) (addrFromPPtr p)
od
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookupPDSlot pd vptr);
checkMappingPPtr pptr sz (Inr p);
withoutFailure $ do slots <- return (map (\<lambda>x. x + p) superSectionPDEOffsets);
mapM (swp storePDE ARM_H.InvalidPDE) slots;
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) (VPtr $ fromPPtr (last slots) + (HaskellLib_H.bit pdeBits - 1)) (addrFromPPtr (head slots))
od
odE;
liftE (flushPage sz pd asid vptr)
odE) \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!