diff --git a/spec/haskell/src/SEL4/API/Invocation/AARCH64.hs b/spec/haskell/src/SEL4/API/Invocation/AARCH64.hs
index 6ad185625..585f2f6cb 100644
--- a/spec/haskell/src/SEL4/API/Invocation/AARCH64.hs
+++ b/spec/haskell/src/SEL4/API/Invocation/AARCH64.hs
@@ -30,13 +30,24 @@ import SEL4.Machine.RegisterSet.AARCH64 (Register(..), VCPUReg(..))
 -- ASID pool structures.
 
 data Invocation
-    = InvokePageTable PageTableInvocation
+    = InvokeVSpaceRoot VSpaceRootInvocation
+    | InvokePageTable PageTableInvocation
     | InvokePage PageInvocation
     | InvokeASIDControl ASIDControlInvocation
     | InvokeASIDPool ASIDPoolInvocation
     | InvokeVCPU VCPUInvocation
     deriving Show
 
+data VSpaceRootInvocation
+    = VSpaceRootFlush {
+        vsFlushType :: FlushType,
+        vsFlushStart :: VPtr,
+        vsFlushEnd :: VPtr,
+        vsFlushPStart :: PAddr,
+        vsFlushSpace :: PPtr PTE,
+        vsFlushASID :: ASID }
+    deriving Show
+
 data PageTableInvocation
     = PageTableUnmap {
         ptUnmapCap :: ArchCapability,
@@ -58,6 +69,13 @@ data PageInvocation
     | PageUnmap {
         pageUnmapCap :: ArchCapability,
         pageUnmapCapSlot :: PPtr CTE }
+    | PageFlush {
+        pageFlushType :: FlushType,
+        pageFlushStart :: VPtr,
+        pageFlushEnd :: VPtr,
+        pageFlushPStart :: PAddr,
+        pageFlushSpace :: PPtr PTE,
+        pageFlushASID :: ASID }
     deriving Show
 
 data ASIDControlInvocation
@@ -75,6 +93,10 @@ data ASIDPoolInvocation
         assignASIDCTSlot :: PPtr CTE }
     deriving Show
 
+data FlushType
+    = Clean | Invalidate | CleanInvalidate | Unify
+    deriving Show
+
 {- VCPUs -}
 
 type HyperReg = VCPUReg
diff --git a/spec/haskell/src/SEL4/API/InvocationLabels/AARCH64.hs b/spec/haskell/src/SEL4/API/InvocationLabels/AARCH64.hs
index edc26129c..0b3dc1a30 100644
--- a/spec/haskell/src/SEL4/API/InvocationLabels/AARCH64.hs
+++ b/spec/haskell/src/SEL4/API/InvocationLabels/AARCH64.hs
@@ -19,11 +19,19 @@ module SEL4.API.InvocationLabels.AARCH64 where
 -- FIXME AARCH64: review enum arch_invocation_label in C, the list is quite
 -- different between ARM and RISCV64
 data ArchInvocationLabel
-        = ARMPageTableMap
+        = ARMVSpaceClean_Data
+        | ARMVSpaceInvalidate_Data
+        | ARMVSpaceCleanInvalidate_Data
+        | ARMVSpaceUnify_Instruction
+        | ARMPageTableMap
         | ARMPageTableUnmap
         | ARMPageMap
         | ARMPageUnmap
         | ARMPageGetAddress
+        | ARMPageClean_Data
+        | ARMPageInvalidate_Data
+        | ARMPageCleanInvalidate_Data
+        | ARMPageUnify_Instruction
         | ARMASIDControlMakePool
         | ARMASIDPoolAssign
         | ARMVCPUSetTCB
diff --git a/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs b/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
index d6777c7cc..924f1480b 100644
--- a/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
+++ b/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
@@ -220,6 +220,19 @@ invalidateTLBByASID asid = do
     when (isJust maybeVMID) $
         doMachineOp $ invalidateTranslationASID $ fromIntegral $ fromJust maybeVMID
 
+doFlush :: FlushType -> VPtr -> VPtr -> PAddr -> MachineMonad ()
+doFlush flushType vstart vend pstart =
+    -- the address calculations that happen here on ARM_HYP are at the caller side in AARCH64
+    case flushType of
+        Clean           -> cleanCacheRange_RAM vstart vend pstart
+        Invalidate      -> invalidateCacheRange_RAM vstart vend pstart
+        CleanInvalidate -> cleanInvalidateCacheRange_RAM vstart vend pstart
+        Unify           -> do
+                               cleanCacheRange_PoU vstart vend pstart
+                               dsb
+                               invalidateCacheRange_I vstart vend pstart
+                               branchFlushRange vstart vend pstart
+                               isb
 
 {- Unmapping and Deletion -}
 
@@ -654,6 +667,14 @@ decodeARMMMUInvocation _ _ _ _ (VCPUCap {}) _ = fail "decodeARMMMUInvocation: no
 
 {- Invocation Implementations -}
 
+performVSpaceRootInvocation :: VSpaceRootInvocation -> Kernel ()
+performVSpaceRootInvocation (VSpaceRootFlush flushType vstart vend pstart space asid) = do
+    let start = VPtr $ fromPPtr $ ptrFromPAddr pstart
+    let end = start + (vend - vstart)
+    when (start < end) $ do
+        doMachineOp $ doFlush flushType start end pstart
+
+
 performPageTableInvocation :: PageTableInvocation -> Kernel ()
 performPageTableInvocation (PageTableMap cap ctSlot pte ptSlot) = do
     updateCap ctSlot cap
@@ -696,6 +717,12 @@ performPageInvocation (PageGetAddr ptr) = do
             msgLabel = 0 }
     setMessageInfo ct msgInfo
 
+performPageInvocation (PageFlush flushType vstart vend pstart space asid) = do
+    let start = VPtr $ fromPPtr $ ptrFromPAddr pstart
+    let end = start + (vend - vstart)
+    when (start < end) $ do
+        doMachineOp $ doFlush flushType start end pstart
+
 
 performASIDControlInvocation :: ASIDControlInvocation -> Kernel ()
 performASIDControlInvocation (MakePool frame slot parent base) = do
@@ -726,6 +753,7 @@ performASIDPoolInvocation (Assign asid poolPtr ctSlot) = do
 performARMMMUInvocation :: ArchInv.Invocation -> KernelP [Word]
 performARMMMUInvocation i = withoutPreemption $ do
     case i of
+        InvokeVSpaceRoot oper -> performVSpaceRootInvocation oper
         InvokePageTable oper -> performPageTableInvocation oper
         InvokePage oper -> performPageInvocation oper
         InvokeASIDControl oper -> performASIDControlInvocation oper
diff --git a/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs b/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs
index 17ab64a86..97f0904d5 100644
--- a/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs
+++ b/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs
@@ -209,6 +209,25 @@ sfence = error "Unimplemented - machine op"
 invalidateTranslationASID :: Word -> MachineMonad ()
 invalidateTranslationASID vmID = error "unimplemented - machine op"
 
+cleanInvalidateCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
+cleanInvalidateCacheRange_RAM vstart vend pstart = error "Unimplemented - machine op"
+
+cleanCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
+cleanCacheRange_RAM vstart vend pstart = error "Unimplemented - machine op"
+
+cleanCacheRange_PoU :: VPtr -> VPtr -> PAddr -> MachineMonad ()
+cleanCacheRange_PoU vstart vend pstart = error "Unimplemented - machine op"
+
+invalidateCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
+invalidateCacheRange_RAM vstart vend pstart = error "Unimplemented - machine op"
+
+invalidateCacheRange_I :: VPtr -> VPtr -> PAddr -> MachineMonad ()
+invalidateCacheRange_I vstart vend pstart = error "Unimplemented - machine op"
+
+branchFlushRange :: VPtr -> VPtr -> PAddr -> MachineMonad ()
+branchFlushRange vstart vend pstart = error "Unimplemented - machine op"
+
+
 {- FPU status/control registers -}
 
 enableFpuEL01 :: MachineMonad ()