diff --git a/package.yaml b/package.yaml
index bca72b4..41bc5f8 100644
--- a/package.yaml
+++ b/package.yaml
@@ -140,6 +140,7 @@ library:
     - Memory.Vec
     - Memory.ST
     - Memory.IO
+    - Memory.Cache
     - Leak.Arch.Arch
     - Leak.PC.ISA
     - Leak.PC.Leak
diff --git a/proof-smt/Proof/Functional/Induction.hs b/proof-smt/Proof/Functional/Induction.hs
index 1edaa2a..82635c4 100644
--- a/proof-smt/Proof/Functional/Induction.hs
+++ b/proof-smt/Proof/Functional/Induction.hs
@@ -69,7 +69,8 @@ data KState = KState
     kWbRes :: Word,
     kCtrl :: Core.Control Identity,
     kHalt :: Maybe Core.HaltState,
-    kHaltNextPc :: Address
+    kHaltNextPc :: Address,
+    kLoadInFlight :: Bool
   }
 
 -- | Assemble a system state from the symbolic pieces.
@@ -90,7 +91,8 @@ sysOf ss i ra ma =
             Core.stateRegFile = RegArrF ra,
             Core.stateCtrl = kCtrl ss,
             Core.stateHalt = kHalt ss,
-            Core.stateHaltNextPc = kHaltNextPc ss
+            Core.stateHaltNextPc = kHaltNextPc ss,
+            Core.stateLoadInFlight = kLoadInFlight ss
           },
       sysInput = i,
       sysMem = ma
diff --git a/proof/Proof/Leakage/Simulator.hs b/proof/Proof/Leakage/Simulator.hs
index 9c790ca..6c5d159 100644
--- a/proof/Proof/Leakage/Simulator.hs
+++ b/proof/Proof/Leakage/Simulator.hs
@@ -94,9 +94,10 @@ censor sys@(Sys st inp _) =
               stateRegFile = initRFg,
               stateCtrl = initCtrl,
               stateHalt = stateHalt st,
-              stateHaltNextPc = stateHaltNextPc st
+              stateHaltNextPc = stateHaltNextPc st,
+              stateLoadInFlight = stateLoadInFlight st
             },
-        sysInput = Input (inputIsInstr inp) (Identity 0),
+        sysInput = Input (inputIsInstr inp) (Identity 0) True,
         sysMem = ()
       }
 
@@ -196,7 +197,7 @@ scrub l (Sys st inp _) =
               stateRegFile = initRFg,
               stateCtrl = initCtrl
             },
-        sysInput = Input (inputIsInstr inp) (Identity 0),
+        sysInput = Input (inputIsInstr inp) (Identity 0) True,
         sysMem = ()
       }
   where
@@ -276,9 +277,9 @@ stepSimOut w (Sys s i _) =
   let (s', o) = Core.circuit s i
       i' = case getFirst (outMem o) of
         Just (MemAccess isInstr _ _ Nothing) ->
-          Input isInstr (Identity (if isInstr then w else 0))
-        Just (MemAccess isInstr _ _ (Just _)) -> Input isInstr (Identity 0)
-        Nothing -> Input False (Identity 0)
+          Input isInstr (Identity (if isInstr then w else 0)) True
+        Just (MemAccess isInstr _ _ (Just _)) -> Input isInstr (Identity 0) True
+        Nothing -> Input False (Identity 0) True
    in (Sys s' i' (), o)
 
 -- | Put the leaked instruction word on the simulator's bus.
@@ -290,7 +291,7 @@ stepSimOut w (Sys s i _) =
 -- later through 'stepSimOut'.
 installLeak :: Word -> SimSys r -> SimSys r
 installLeak word (Sys s i m)
-  | inputIsInstr i = Sys s (Input True (Identity word)) m
+  | inputIsInstr i = Sys s (Input True (Identity word) True) m
   | otherwise = Sys s i m
 
 -- | The implementation, run for one driver hop, with the observation of each
diff --git a/proof/Proof/Machine.hs b/proof/Proof/Machine.hs
index 66f6242..3519de5 100644
--- a/proof/Proof/Machine.hs
+++ b/proof/Proof/Machine.hs
@@ -24,6 +24,11 @@ module Proof.Machine
     isNopInstr,
     isBubble,
     readMemWord,
+    CacheSys (..),
+    initCacheSys,
+    stepCached,
+    stepCachedOut,
+    stepCachedN,
   )
 where
 
@@ -33,6 +38,7 @@ import Data.Functor.Identity
 import Data.Maybe (isNothing)
 import Data.Monoid (getFirst)
 import Instruction
+import Memory.Cache (CacheOps (..))
 import Memory.Types
 import RegFile
 import Types
@@ -83,10 +89,10 @@ stepSysOut (Sys s i m) =
         -- A read. Note 'Memory.Vec.ramRead' ignores the size and always reads a
         -- word; the size-dependent narrowing happens in 'Core.writeback' via
         -- 'loadExtend'. We reproduce that here.
-        Nothing -> (Input isInstr (pure (memReadWord addr mem)), mem)
+        Nothing -> (Input isInstr (pure (memReadWord addr mem)) True, mem)
         -- A write.
-        Just val -> (Input isInstr (pure 0), memWriteWord size addr (runIdentity val) mem)
-    service Nothing mem = (Input False (pure 0), mem)
+        Just val -> (Input isInstr (pure 0) True, memWriteWord size addr (runIdentity val) mem)
+    service Nothing mem = (Input False (pure 0) True, mem)
 
 stepSysN :: (RegFileOps r, MemOps m) => Int -> SysG r m -> SysG r m
 stepSysN n s
@@ -126,3 +132,49 @@ isBubble _ = False
 
 readMemWord :: Address -> MemBytes -> Word
 readMemWord = readWord
+
+-- | System state paired with a cache model.
+data CacheSys r m c = CacheSys
+  { cacheSysCore :: SysG r m,
+    cacheSysCache :: c,
+    -- | Address and remaining cycles for a pending load miss.
+    cacheSysPending :: Maybe (Address, Int)
+  }
+
+deriving instance (Show (r Identity), Show m, Show c) => Show (CacheSys r m c)
+
+initCacheSys :: SysG r m -> c -> CacheSys r m c
+initCacheSys sys cache = CacheSys sys cache Nothing
+
+-- | Step a system with memory serviced through a cache.
+stepCached :: (RegFileOps r, MemOps m, CacheOps c) => Int -> CacheSys r m c -> CacheSys r m c
+stepCached missPenalty = fst . stepCachedOut missPenalty
+
+stepCachedOut ::
+  (RegFileOps r, MemOps m, CacheOps c) =>
+  Int ->
+  CacheSys r m c ->
+  (CacheSys r m c, Output Identity)
+stepCachedOut missPenalty (CacheSys (Sys s i m) cache pending) =
+  let (s', o) = Core.circuit s i
+      (i', m', cache', pending') = respond (getFirst (outMem o)) m cache pending
+   in (CacheSys (Sys s' i' m') cache' pending', o)
+  where
+    respond mAccess mem c (Just (addr, n))
+      | n > 0 = (Input False (pure 0) False, mem, c, Just (addr, n - 1))
+      | otherwise =
+          let w = memReadWord addr mem
+           in (Input False (pure w) True, mem, cacheInsert addr w c, Nothing)
+    respond Nothing mem c Nothing = (Input False (pure 0) True, mem, c, Nothing)
+    respond (Just (MemAccess isInstr addr size mval)) mem c Nothing = case mval of
+      Just val ->
+        (Input isInstr (pure 0) True, memWriteWord size addr (runIdentity val) mem, cacheInvalidate addr c, Nothing)
+      Nothing | isInstr -> (Input isInstr (pure (memReadWord addr mem)) True, mem, c, Nothing)
+      Nothing -> case cacheLookup addr c of
+        Just w -> (Input isInstr (pure w) True, mem, c, Nothing)
+        Nothing -> (Input isInstr (pure 0) False, mem, c, Just (addr, missPenalty - 1))
+
+stepCachedN :: (RegFileOps r, MemOps m, CacheOps c) => Int -> Int -> CacheSys r m c -> CacheSys r m c
+stepCachedN missPenalty n s
+  | n <= 0 = s
+  | otherwise = stepCachedN missPenalty (n - 1) (stepCached missPenalty s)
diff --git a/src/Core.hs b/src/Core.hs
index 6bdf50d..77df56a 100644
--- a/src/Core.hs
+++ b/src/Core.hs
@@ -61,7 +61,9 @@ data Input f = Input
   { -- | Is this an instruction read?
     inputIsInstr :: Bool,
     -- | Reads from memory.
-    inputMem :: f Word
+    inputMem :: f Word,
+    -- | Is the memory answer ready this cycle?
+    inputMemReady :: Bool
   }
 
 deriving instance (Show (f Word)) => Show (Input f)
@@ -143,7 +145,9 @@ data StateG r f = State
     -- | CPU halt state.
     stateHalt :: Maybe HaltState,
     -- | In case of a halt, the address of the next instruction.
-    stateHaltNextPc :: Address
+    stateHaltNextPc :: Address,
+    -- | True when a load is in flight.
+    stateLoadInFlight :: Bool
   }
 
 -- | The synthesisable state: the register file is a 'Vec'.
@@ -186,7 +190,9 @@ data Control f = Control
     ctrlMeRegFwd :: Maybe (RegIdx, f Word),
     -- | Forwards the `rd` register from the `writeback` stage to the `execute`
     -- stage.
-    ctrlWbRegFwd :: Maybe (RegIdx, f Word)
+    ctrlWbRegFwd :: Maybe (RegIdx, f Word),
+    -- | True when a load was in flight at the start of the cycle.
+    ctrlMeHadInFlight :: Bool
   }
 
 deriving instance (Show (f Word)) => Show (Control f)
@@ -224,7 +230,8 @@ initInput :: (Access f) => Input f
 initInput =
   Input
     { inputIsInstr = False,
-      inputMem = pure 0
+      inputMem = pure 0,
+      inputMemReady = True
     }
 
 init :: forall f r. (Access f, RegFileOps r) => StateG r f
@@ -242,7 +249,8 @@ init =
       stateRegFile = initRFg,
       stateCtrl = initCtrl,
       stateHalt = Nothing,
-      stateHaltNextPc = 0
+      stateHaltNextPc = 0,
+      stateLoadInFlight = False
     }
 
 -- | Initial control lines.
@@ -257,7 +265,8 @@ initCtrl =
       ctrlMeMemInstr = False,
       ctrlMeStoreAddrSize = Nothing,
       ctrlMeRegFwd = Nothing,
-      ctrlWbRegFwd = Nothing
+      ctrlWbRegFwd = Nothing,
+      ctrlMeHadInFlight = False
     }
 
 -- | The control lines need to be reset every tick.
@@ -281,7 +290,7 @@ fetch = do
   -- Always try to read unless the instruction in the `memory` stage is a load or a store.
   unless (ctrlMeMemInstr ctrl) $
     readPC pc
-  
+
   -- We stall if the instruction in the `memory` stage is a load or a store.
   let stall = ctrlMeMemInstr ctrl
 
@@ -304,10 +313,15 @@ fetch = do
 -- | Decode stage.
 decode :: (Access f) => CPUM r f ()
 decode = do
+  hadInFlight <- gets (ctrlMeHadInFlight . stateCtrl)
+  unless hadInFlight decodeFresh
+
+decodeFresh :: (Access f) => CPUM r f ()
+decodeFresh = do
   input <- ask
   pc <- gets stateDePc
   ctrl <- gets stateCtrl
-  
+
   ir <-
     if inputIsInstr input
       then noSecrets' (inputMem input) (Nop Halted) (pure . decode')
@@ -362,6 +376,11 @@ decode = do
 -- | Execute stage.
 execute :: forall f r. (Access f, RegFileOps r) => CPUM r f ()
 execute = do
+  hadInFlight <- gets (ctrlMeHadInFlight . stateCtrl)
+  unless hadInFlight execute'
+
+execute' :: forall f r. (Access f, RegFileOps r) => CPUM r f ()
+execute' = do
   ir <- gets stateExInstr
 
   -- Default values.
@@ -525,8 +544,18 @@ branch op lhs rhs = case op of
   where
     sign = unpack @(Signed 32)
 
+-- | Memory stage.
 memory :: CPUM r f ()
 memory = do
+  wasInFlight <- gets stateLoadInFlight
+  setLines $ \c -> c {ctrlMeHadInFlight = wasInFlight}
+  if wasInFlight
+    then setLines $ \c -> c {ctrlMeMemInstr = True}
+    else memoryFresh
+
+-- | Process a fresh memory instruction.
+memoryFresh :: CPUM r f ()
+memoryFresh = do
   ir <- gets stateMeInstr
   res <- gets stateMeRes
   addr <- gets stateMeAddr
@@ -544,6 +573,7 @@ memory = do
     Instruction.IType (Load size _) _ _ _ -> do
       setLines $ \c -> c {ctrlMeMemInstr = True}
       readRAM addr size
+      modify $ \s -> s {stateLoadInFlight = True}
     Instruction.SType size _ _ _ -> do
       setLines $ \c ->
         c {ctrlMeMemInstr = True, ctrlMeStoreAddrSize = Just (addr, size)}
@@ -559,9 +589,8 @@ memory = do
 -- | Commit computations to the register file.
 writeback :: forall f r. (Access f, RegFileOps r) => CPUM r f ()
 writeback = do
-  input <- asks inputMem
   ir <- gets stateWbInstr
-  res <- gets stateWbRes  
+  res <- gets stateWbRes
 
   case ir of
     Instruction.RType _ rd _ _ -> do
@@ -571,9 +600,13 @@ writeback = do
       setLines $ \c -> c {ctrlWbRegFwd = Just (rd, res)}
       writeRF rd res
     Instruction.IType (Load size sign) rd _ _ -> do
-      let val = loadExtend size sign <$> input
-      setLines $ \c -> c {ctrlWbRegFwd = Just (rd, val)}
-      writeRF rd val
+      ready <- asks inputMemReady
+      when ready $ do
+        input <- asks inputMem
+        let val = loadExtend size sign <$> input
+        setLines $ \c -> c {ctrlWbRegFwd = Just (rd, val)}
+        writeRF rd val
+        modify $ \s -> s {stateLoadInFlight = False}
     Instruction.JType rd _ -> do
       setLines $ \c -> c {ctrlWbRegFwd = Just (rd, res)}
       writeRF rd res
diff --git a/src/HardwareSim.hs b/src/HardwareSim.hs
index 1adb0ef..7113e4c 100644
--- a/src/HardwareSim.hs
+++ b/src/HardwareSim.hs
@@ -40,6 +40,7 @@ system prog = cpuOut
             ( fromMaybe False $ memIsInstr <$> getFirst (outMem o)
             )
             (Identity mread)
+            True
       )
         <$> cpuOut
         <*> ram
diff --git a/src/Memory/Cache.hs b/src/Memory/Cache.hs
new file mode 100644
index 0000000..fbd3e84
--- /dev/null
+++ b/src/Memory/Cache.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | A small, swappable cache model.
+module Memory.Cache
+  ( CacheOps (..),
+    CacheOutcome (..),
+    cacheAccess,
+    CacheLine (..),
+    DirectMapped (..),
+    mkDirectMapped,
+  )
+where
+
+import Clash.Prelude hiding (Word, init)
+import Data.Proxy (Proxy (..))
+import Types (Address, Word)
+import Prelude hiding (Word, repeat, (!!), (&&))
+
+-- | Whether a lookup was a hit or a miss.
+data CacheOutcome = Hit | Miss
+  deriving (Eq, Show, Generic, NFDataX)
+
+-- | Operations supported by a cache model.
+class CacheOps c where
+  -- | Look up a word at an address.
+  cacheLookup :: Address -> c -> Maybe Word
+
+  -- | Install a word at an address.
+  cacheInsert :: Address -> Word -> c -> c
+
+  -- | Invalidate the line for an address.
+  cacheInvalidate :: Address -> c -> c
+
+-- | Access memory through a cache, reading backing memory on a miss.
+cacheAccess ::
+  (CacheOps c) =>
+  (Address -> Word) ->
+  Address ->
+  c ->
+  (c, Word, CacheOutcome)
+cacheAccess readBacking addr c = case cacheLookup addr c of
+  Just w -> (c, w, Hit)
+  Nothing ->
+    let w = readBacking addr
+     in (cacheInsert addr w c, w, Miss)
+
+-- | One line of a direct-mapped cache.
+data CacheLine = CacheLine
+  { clValid :: Bool,
+    clTag :: Address,
+    clWord :: Word
+  }
+  deriving (Eq, Show, Generic, NFDataX)
+
+invalidLine :: CacheLine
+invalidLine = CacheLine {clValid = False, clTag = 0, clWord = 0}
+
+-- | A direct-mapped cache of @n@ lines.
+newtype DirectMapped n = DirectMapped (Vec n CacheLine)
+  deriving (Eq, Show, Generic, NFDataX)
+
+mkDirectMapped :: (KnownNat n) => DirectMapped n
+mkDirectMapped = DirectMapped (repeat invalidLine)
+
+blockOf :: Address -> Address
+blockOf addr = addr `div` 4
+
+indexOf :: forall n. (KnownNat n) => Address -> Index n
+indexOf addr = fromIntegral (blockOf addr `mod` fromIntegral (natVal (Proxy @n)))
+
+tagOf :: forall n. (KnownNat n) => Address -> Address
+tagOf addr = blockOf addr `div` fromIntegral (natVal (Proxy @n))
+
+lineAt :: forall n. (KnownNat n) => Address -> DirectMapped n -> CacheLine
+lineAt addr (DirectMapped ls) = ls !! (indexOf @n addr)
+
+instance (KnownNat n, 1 <= n) => CacheOps (DirectMapped n) where
+  cacheLookup addr dm
+    | clValid line && clTag line == tagOf @n addr = Just (clWord line)
+    | otherwise = Nothing
+    where
+      line = lineAt @n addr dm
+
+  cacheInsert addr w (DirectMapped ls) =
+    DirectMapped (replace (indexOf @n addr) (CacheLine True (tagOf @n addr) w) ls)
+
+  cacheInvalidate addr dm@(DirectMapped ls)
+    | clValid line && clTag line == tagOf @n addr =
+        DirectMapped (replace (indexOf @n addr) invalidLine ls)
+    | otherwise = dm
+    where
+      line = lineAt @n addr dm
diff --git a/src/Simulate.hs b/src/Simulate.hs
index 887e4fa..b8f45dc 100644
--- a/src/Simulate.hs
+++ b/src/Simulate.hs
@@ -49,7 +49,8 @@ simulator =
           Just $
             Input
               { inputIsInstr = mem_instr,
-                inputMem = mem_in
+                inputMem = mem_in,
+                inputMemReady = True
               }
       where
         doMemory :: m (f Word, Bool)
diff --git a/test/CacheSpec.hs b/test/CacheSpec.hs
new file mode 100644
index 0000000..9caef29
--- /dev/null
+++ b/test/CacheSpec.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE BangPatterns #-}
+
+module CacheSpec (cacheTests) where
+
+import Clash.Prelude hiding (Word)
+import Instruction
+import Memory.Cache
+import Memory.Types (MemBytes, mkProg)
+import Proof.Machine
+import RegFile (RegFile)
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (assertEqual, testCase, (@?=))
+import Types (Size (Word), Word)
+import Prelude hiding (Word, not)
+
+cacheTests :: TestTree
+cacheTests =
+  testGroup
+    "Cache"
+    [ directMappedTests,
+      timingLeakTests
+    ]
+
+-- | 4-line direct-mapped cache for collision testing.
+type TestCache = DirectMapped 4
+
+freshCache :: TestCache
+freshCache = mkDirectMapped
+
+directMappedTests :: TestTree
+directMappedTests =
+  testGroup
+    "DirectMapped"
+    [ testCase "a fresh cache misses everywhere" $
+        cacheLookup 0 freshCache @?= (Nothing :: Maybe Word),
+      testCase "a lookup right after an insert hits" $
+        cacheLookup 0 (cacheInsert 0 0xCAFE freshCache) @?= Just 0xCAFE,
+      testCase "a colliding address evicts the resident line" $
+        let c = cacheInsert 16 0xBEEF (cacheInsert 0 0xCAFE freshCache)
+         in (cacheLookup 0 c, cacheLookup 16 c) @?= (Nothing, Just 0xBEEF),
+      testCase "a non-colliding address does not evict" $
+        let c = cacheInsert 4 0xBEEF (cacheInsert 0 0xCAFE freshCache)
+         in (cacheLookup 0 c, cacheLookup 4 c) @?= (Just 0xCAFE, Just 0xBEEF),
+      testCase "invalidating a resident line makes it miss again" $
+        let c = cacheInvalidate 0 (cacheInsert 0 0xCAFE freshCache)
+         in cacheLookup 0 c @?= (Nothing :: Maybe Word)
+    ]
+
+-- | Extra cycles incurred by a cache miss.
+missPenalty :: Int
+missPenalty = 3
+
+-- | Two loads to the same address (second hits).
+progHit :: Vec 50 Word
+progHit =
+  mkProg $
+    IType (Load Word Signed) 1 0 0
+      :> IType (Load Word Signed) 2 0 0
+      :> Instruction.break
+      :> Nil
+
+-- | Two loads to colliding addresses (second misses).
+progMiss :: Vec 50 Word
+progMiss =
+  mkProg $
+    IType (Load Word Signed) 1 0 0
+      :> IType (Load Word Signed) 2 0 16
+      :> Instruction.break
+      :> Nil
+
+-- | Run a cached system to completion, returning cycles taken.
+cyclesToHalt :: CacheSys RegFile MemBytes TestCache -> Int
+cyclesToHalt = go 0
+  where
+    go !n cs
+      | not (running (cacheSysCore cs)) = n
+      | otherwise = go (n + 1) (stepCached missPenalty cs)
+
+timingLeakTests :: TestTree
+timingLeakTests =
+  testGroup
+    "Timing leak"
+    [ testCase "a cache miss costs exactly the configured extra cycles" $ do
+        let hitCycles = cyclesToHalt (initCacheSys (initSys progHit) freshCache)
+            missCycles = cyclesToHalt (initCacheSys (initSys progMiss) freshCache)
+        assertEqual
+          "same instructions, only the second load's address differs, but the \
+          \attacker-visible cycle count does not match"
+          missPenalty
+          (missCycles - hitCycles)
+    ]
diff --git a/test/ProofSpec.hs b/test/ProofSpec.hs
index 2060161..0015015 100644
--- a/test/ProofSpec.hs
+++ b/test/ProofSpec.hs
@@ -568,10 +568,11 @@ wrapCESys =
           stateRegFile = RegFn (const (pure 0)),
           stateCtrl = initCtrl,
           stateHalt = Nothing,
-          stateHaltNextPc = 0
+          stateHaltNextPc = 0,
+          stateLoadInFlight = False
         }
     )
-    (Input True (pure wrapDeWord))
+    (Input True (pure wrapDeWord) True)
     wrapMem
 
 -- Arbitrary-state search ------------------------------------------------------
@@ -766,9 +767,10 @@ genArbSys = do
                stateRegFile = RegFn (P.fmap Identity rfF),
                stateCtrl = initCtrl,
                stateHalt = Nothing,
-               stateHaltNextPc = 0
+               stateHaltNextPc = 0,
+               stateLoadInFlight = False
              })
-          (Input True (pure w1))
+          (Input True (pure w1) True)
           (MemFn memf)
   P.pure (sys, wr, wa)
 
@@ -830,7 +832,7 @@ genRunning2 label genEx = do
   -- premise is exercised rather than making those samples vacuous.
   let ma = base + 64
       wbMem = isMemInstr wbI
-      inp = if wbMem then Input False (pure loaded) else Input True (pure w1)
+      inp = if wbMem then Input False (pure loaded) True else Input True (pure w1) True
       fePc = if wbMem then base + 4 else base + 8
   wr <- genWitnessReg
   wa <- unpack <$> genW
@@ -849,7 +851,8 @@ genRunning2 label genEx = do
                 stateRegFile = RegFn (P.fmap Identity rfF),
                 stateCtrl = initCtrl,
                 stateHalt = Nothing,
-                stateHaltNextPc = 0
+                stateHaltNextPc = 0,
+                stateLoadInFlight = False
               }
           )
           inp
@@ -909,10 +912,11 @@ genSteady2 = do
                 stateRegFile = RegFn (P.fmap Identity rfF),
                 stateCtrl = initCtrl,
                 stateHalt = Nothing,
-                stateHaltNextPc = 0
+                stateHaltNextPc = 0,
+                stateLoadInFlight = False
               }
           )
-          (Input False (pure loaded))
+          (Input False (pure loaded) True)
           (MemFn memf)
   P.pure ("steady", sys, wr, wa)
 
@@ -953,10 +957,11 @@ genSteady1 = do
                 stateRegFile = RegFn (P.fmap Identity rfF),
                 stateCtrl = initCtrl,
                 stateHalt = Nothing,
-                stateHaltNextPc = 0
+                stateHaltNextPc = 0,
+                stateLoadInFlight = False
               }
           )
-          (Input False (pure loaded))
+          (Input False (pure loaded) True)
           (MemFn memf)
   P.pure (sys, wr, wa)
 
@@ -1153,7 +1158,7 @@ genTakenTransfer useJalr = do
       w1 = P.maybe 0 P.id (encode' (roundTrips nextI))
       wT = P.maybe 0 P.id (encode' (roundTrips tgtI))
       wbMem = isLoad wbI || isStore wbI
-      inp = if wbMem then Input False (pure loaded) else Input True (pure w1)
+      inp = if wbMem then Input False (pure loaded) True else Input True (pure w1) True
       fePc = if wbMem then base + 4 else base + 8
       ma = base + 4096 -- parked away from every PC and from the target
 
@@ -1172,7 +1177,8 @@ genTakenTransfer useJalr = do
                 stateRegFile = RegFn (P.fmap Identity rfun),
                 stateCtrl = initCtrl,
                 stateHalt = Nothing,
-                stateHaltNextPc = 0
+                stateHaltNextPc = 0,
+                stateLoadInFlight = False
               }
           )
           inp
@@ -1286,10 +1292,11 @@ mk3 base exI meI wbI nextI wbMem = do
               stateRegFile = RegFn (P.fmap Identity rfF),
               stateCtrl = initCtrl,
               stateHalt = Nothing,
-              stateHaltNextPc = 0
+              stateHaltNextPc = 0,
+              stateLoadInFlight = False
             }
         )
-        (if wbMem then Input False (pure loaded) else Input True (pure w1))
+        (if wbMem then Input False (pure loaded) True else Input True (pure w1) True)
         (MemFn memf),
       wr,
       wa
diff --git a/test/Spec.hs b/test/Spec.hs
index 163a095..e092c67 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -8,6 +8,7 @@ module Main (main) where
 
 import Access
 import BenchmarkSpec (benchmarkTests)
+import CacheSpec (cacheTests)
 import Clash.Prelude hiding (Log, Ordering (..), Word, break, def, init, lift, log, resize)
 import Clash.Sized.Vector (unsafeFromList)
 import Control.Monad
@@ -119,6 +120,7 @@ tests =
       proofTests,
       isaConformanceTests,
       instructionTests,
+      cacheTests,
       testGroup
         "Haskell simulation tests"
         [ testGroup
@@ -350,6 +352,7 @@ instance {-# OVERLAPPING #-} (Access f) => Arbitrary (Control f) where
       <*> arbitrary
       <*> genMaybeRegFwd
       <*> genMaybeRegFwd
+      <*> pure False
     where
       genAccessWord = do
         isSecret <- arbitrary
@@ -395,6 +398,7 @@ instance {-# OVERLAPPING #-} (Access f, Arbitrary (f Word)) => Arbitrary (Core.S
       <*> arbitrary
       <*> arbitrary
       <*> arbitrary
+      <*> pure False
 
 instance {-# OVERLAPPING #-} (Access f) => Arbitrary (Input f) where
   arbitrary = do
@@ -408,3 +412,4 @@ instance {-# OVERLAPPING #-} (Access f) => Arbitrary (Input f) where
       Input
         isInstr
         (conditionalSecret isSecretMem mem)
+        True