Rename SimMemAccess to SimDataAccess

proof/Proof/Core/Leakage/Driver.hs

@@ -58,7 +58,7 @@ simDriver inp st
   | simStoreHazard inp st = if maybe False isMemLeak inp then 3 else 2
   | simLoadHazard inp st = 3
   | simStateDeExpInstr st = 0
-  | simStateMeAccess st == SimNoAccess = 1
+  | simStateMeAccess st == SimNoDataAccess = 1
   | not (maybe False isMemLeak inp) = 2
   | otherwise = 3
 

proof/Proof/Core/Leakage/Invariant.hs

@@ -51,7 +51,7 @@ simInv sim (Sys core _ _) =
           simStateMeAccess sim == SimLoad size (stateMeAddr core)
         Core.Instruction.SType size _ _ _ ->
           simStateMeAccess sim == SimStore size (stateMeAddr core)
-        _ -> simStateMeAccess sim == SimNoAccess
+        _ -> simStateMeAccess sim == SimNoDataAccess
 
 -- | The invariant is functional: two simulators it relates to the same system
 -- are equal. Every field of the simulator is pinned by the core: its PCs and

proof/Proof/Core/Leakage/Simulator.hs

@@ -12,7 +12,7 @@ module Proof.Core.Leakage.Simulator
   ( SimInput,
     SimOutput,
     SimExInstrType (..),
-    SimMemAccess (..),
+    SimDataAccess (..),
     SimState (..),
     SimControl (..),
     SimM,
@@ -72,8 +72,8 @@ data SimExInstrType
 -- | What the instruction in the memory stage does with memory: nothing, or a
 -- load or a store of a size at an address. The only part of an instruction's
 -- leakage the memory stage uses, so the simulator keeps no more of it.
-data SimMemAccess
-  = SimNoAccess
+data SimDataAccess
+  = SimNoDataAccess
   | SimLoad Size Address
   | SimStore Size Address
   deriving (Eq, Show, Generic, NFDataX)
@@ -89,7 +89,7 @@ data SimState = SimState
     -- | Instruction execute stage.
     simStateExInstrType :: SimExInstrType,
     -- | What the instruction in the memory stage does with memory.
-    simStateMeAccess :: SimMemAccess,
+    simStateMeAccess :: SimDataAccess,
     -- | Control/forwarding lines.
     simStateCtrl :: SimControl
   }
@@ -160,7 +160,7 @@ simInit =
       simStateDePc = 0,
       simStateDeExpInstr = False,
       simStateExInstrType = FirstCycle,
-      simStateMeAccess = SimNoAccess,
+      simStateMeAccess = SimNoDataAccess,
       simStateCtrl = simInitCtrl
     }
 
@@ -286,9 +286,9 @@ simExecute = do
         Just ir -> do
           case ir of
             LArith ->
-              modify $ \s -> s {simStateMeAccess = SimNoAccess}
+              modify $ \s -> s {simStateMeAccess = SimNoDataAccess}
             LJump addr -> do
-              modify $ \s -> s {simStateMeAccess = SimNoAccess}
+              modify $ \s -> s {simStateMeAccess = SimNoDataAccess}
               simSetLines $ \c -> c {simCtrlExJumpAddr = Just addr}
             LLoad size addr haz -> do
               modify $ \s -> s {simStateMeAccess = SimLoad size addr}
@@ -297,18 +297,18 @@ simExecute = do
               modify $ \s -> s {simStateMeAccess = SimStore size addr}
               simSetLines $ \c -> c {simCtrlExStoreAddrSize = Just (addr, size)}
             LEnv -> do
-              modify $ \s -> s {simStateMeAccess = SimNoAccess}
+              modify $ \s -> s {simStateMeAccess = SimNoDataAccess}
               simSetLines $ \c -> c {simCtrlExEnvInstr = True}
-        Nothing -> modify $ \s -> s {simStateMeAccess = SimNoAccess}
-    _ -> modify $ \s -> s {simStateMeAccess = SimNoAccess}
+        Nothing -> modify $ \s -> s {simStateMeAccess = SimNoDataAccess}
+    _ -> modify $ \s -> s {simStateMeAccess = SimNoDataAccess}
 
 -- | Memory stage.
 simMemory :: SimM ()
 simMemory = do
   ir <- gets simStateMeAccess
 
   case ir of
-    SimNoAccess -> pure ()
+    SimNoDataAccess -> pure ()
     SimLoad size addr -> do
       simSetLines $ \c -> c {simCtrlMeMemInstr = True}
       simReadRAM addr size

proof/Proof/Memory/Cache4K/CachedCore/Leakage/Driver.hs

@@ -21,8 +21,8 @@ import Proof.Core.Leakage.Model (Obs (..))
 -- | The cycles the core waits after a request observed as @inp@: the cache
 -- simulator's driver
 -- ('Proof.Memory.Cache4K.Server.Leakage.Driver.simSrvDriver') on that
--- observation. Only ever run from a ready simulator, so whether the last cycle
--- brought an answer is not consulted.
+-- observation. Only ever run from a ready simulator, so whether it is ready is
+-- not consulted.
 simCachedDriver :: SimCachedSys -> SimCachedInput -> Int
 simCachedDriver (SimCachedSys sim _) inp =
   simSrvDriver sim (fromMaybe NoAccess inp)
@@ -36,29 +36,29 @@ simCachedDriverSpec :: Int -> SimCachedSys -> SimCachedInput -> Maybe Int
 simCachedDriverSpec fuel sim0 inp = go 0 (fst (simStepCached sim0 inp))
   where
     go n sim
-      | simCachedAnswered sim = Just n
+      | simCachedReady sim = Just n
       | n >= fuel = Nothing
       | otherwise = go (n + 1) (fst (simStepCached sim Nothing))
 
--- | From a ready simulator -- its last cycle brought an answer, and the cache's
--- simulator is ready
+-- | From a ready simulator -- ready to receive an input, and with the cache's
+-- simulator ready
 -- ('Proof.Memory.Cache4K.Server.Leakage.Simulator.simSrvReady') -- its driver
 -- agrees with its operational reading, for the observation of any request: a
 -- hop starts with one, never in the middle of a driver hop. Eight cycles of
 -- fuel, 2 * 'penalty', cover the longest hop.
 --
 -- Follows from the cache simulator's
 -- ('Proof.Memory.Cache4K.Server.Leakage.Driver.simSrvDriverMatchesSpec'): since
--- the last cycle brought an answer, 'simStepCached' passes the input on to the
--- cache's simulator, and until it answers again passes it no input, so the
+-- the simulator is ready, 'simStepCached' passes the input on to the cache's
+-- simulator, and until it answers again passes it no input, so the
 -- cache's simulator is stepped exactly as
 -- 'Proof.Memory.Cache4K.Server.Leakage.Driver.simSrvDriverSpec' steps it, and
 -- 'simCachedDriver' is its driver.
 simCachedDriverMatchesSpec :: SimCachedSys -> Obs -> Bool
-simCachedDriverMatchesSpec sim@(SimCachedSys srvSim answered) obs =
+simCachedDriverMatchesSpec sim@(SimCachedSys srvSim ready) obs =
   not premises || conclusion
   where
-    premises = answered && simSrvReady srvSim
+    premises = ready && simSrvReady srvSim
 
     conclusion =
       simCachedDriverSpec 8 sim (Just obs)

proof/Proof/Memory/Cache4K/CachedCore/Leakage/Invariant.hs

@@ -22,14 +22,14 @@ import Proof.Memory.Cache4K.Server.Leakage.Simulator (SimCacheSrv (..))
 -- | The simulator agrees with the cached system at a hop boundary: the cache's
 -- simulator agrees with the server at set @wsi@, as in the cache's leakage
 -- proof ('Proof.Memory.Cache4K.Server.Leakage.Invariant.srvSimInvAt'), and the
--- simulator records that an answer has just arrived.
+-- simulator is ready to receive an input.
 cachedSimInvAt :: SetIdx -> SimCachedSys -> CachedSysG r m -> Bool
-cachedSimInvAt wsi (SimCachedSys sim answered) (CachedSys _ _ srv) =
-  srvSimInvAt wsi sim srv && answered
+cachedSimInvAt wsi (SimCachedSys sim ready) (CachedSys _ _ srv) =
+  srvSimInvAt wsi sim srv && ready
 
 -- | The invariant is functional: two simulators it relates to the same cached
 -- system agree at set @wsi@: the cache's simulators have the same tag there
--- and the same state, and both record an answer. Quantifying over @wsi@ gives
+-- and the same state, and both are ready. Quantifying over @wsi@ gives
 -- equality of the simulators. Follows from the cache's simulator invariant
 -- being functional
 -- ('Proof.Memory.Cache4K.Server.Leakage.Invariant.srvSimInvFunctional').
@@ -44,11 +44,11 @@ cachedSimInvFunctional wsi sim1 sim2 csys =
     conclusion =
       tagRead wsi (simTagArr srvSim1) == tagRead wsi (simTagArr srvSim2)
         && simSrvState srvSim1 == simSrvState srvSim2
-        && simCachedAnswered sim1 == simCachedAnswered sim2
+        && simCachedReady sim1 == simCachedReady sim2
 
 -- | The simulator a cached system determines at the start of a hop: the
 -- cache's simulator built from its server
--- ('Proof.Memory.Cache4K.Server.Leakage.Invariant.simOf'), and an answer in the
--- previous cycle, as at every hop boundary.
+-- ('Proof.Memory.Cache4K.Server.Leakage.Invariant.simOf'), ready to receive an
+-- input, as at every hop boundary.
 simCachedOf :: CachedSysG r m -> SimCachedSys
 simCachedOf (CachedSys _ _ srv) = SimCachedSys (simOf srv) True

proof/Proof/Memory/Cache4K/CachedCore/Leakage/Simulator.hs

@@ -35,33 +35,30 @@ type SimCachedInput = Maybe Obs
 
 -- | The simulator's counterpart of
 -- 'Proof.Memory.Cache4K.CachedCore.Functional.Machine.CachedSysG': the cache's
--- simulator, and what the core can see of its input -- whether the cache
--- answered in the previous cycle, and so whether the core is no longer
--- waiting.
+-- simulator, and whether the simulator is ready to receive an input.
 data SimCachedSys = SimCachedSys
   { -- | The cache's simulator.
     simCachedSrv :: SimCacheSrv,
-    -- | Did the cache answer in the previous cycle?
-    simCachedAnswered :: Bool
+    -- | Is the simulator ready to receive an input?
+    simCachedReady :: Bool
   }
   deriving (Show, Eq)
 
 -- | The simulator at start: the cache's simulator at start
--- ('Proof.Memory.Cache4K.Server.Leakage.Simulator.simInitCacheSrv'), and an
--- answer in the previous cycle, as the core's input at start holds one
--- ('Core.Pipeline.initInput').
+-- ('Proof.Memory.Cache4K.Server.Leakage.Simulator.simInitCacheSrv'), ready to
+-- receive an input.
 simInitCachedSys :: SimCachedSys
 simInitCachedSys = SimCachedSys simInitCacheSrv True
 
 -- | One cycle of the core behind the cache, as
 -- 'Proof.Memory.Cache4K.CachedCore.Functional.Machine.stepCachedOut'. If the
--- cache answered in the previous cycle, the core makes the ideal observation,
--- and the cache's simulator is given it; otherwise the core waits, the bus
--- shows no request and the simulator has no input. Returns the simulator
--- afterwards and the bus's observation.
+-- simulator is ready, it takes the ideal observation, shows it on the bus and
+-- gives it to the cache's simulator; otherwise the bus shows no request and the
+-- input is ignored. It is ready again once the cache's simulator answers.
+-- Returns the simulator afterwards and the bus's observation.
 simStepCached :: SimCachedSys -> SimCachedInput -> (SimCachedSys, Obs)
-simStepCached (SimCachedSys sim answered) inp
-  | answered =
+simStepCached (SimCachedSys sim ready) inp
+  | ready =
       let obs = fromMaybe NoAccess inp
           (sim', ans) = simServe sim obs
       in (SimCachedSys sim' ans, obs)

proof/Proof/SMT/Symbolic.hs

@@ -16,7 +16,7 @@ import qualified Core.Pipeline as Core
 import Core.Instruction
 import Memory.Cache4KServer (CacheSrvState (..))
 import Proof.Core.Leakage.Model (Leak, Obs)
-import Proof.Core.Leakage.Simulator (SimControl, SimExInstrType, SimMemAccess, SimState)
+import Proof.Core.Leakage.Simulator (SimControl, SimExInstrType, SimDataAccess, SimState)
 import Proof.Memory.Cache4K.Server.Leakage.Simulator (SimCacheSrvState (..))
 import qualified SymFC.Base ()
 import qualified SymFC.BuiltIn as SymFC
@@ -57,7 +57,7 @@ instance SymFC.Symbolic Leak
 
 instance SymFC.Symbolic Obs
 
-instance SymFC.Symbolic SimMemAccess
+instance SymFC.Symbolic SimDataAccess
 
 deriving instance Generic SimCacheSrvState
 

test/CacheProofSpec.hs

@@ -421,7 +421,7 @@ compositeTrace n sys0 = go (P.concat (P.take n (simHops sys0))) simInitCachedSys
       let (sim', bus) = simStepCached sim (Just obs)
        in bus : waiting rest sim'
     waiting rest sim
-      | simCachedAnswered sim = go rest sim
+      | simCachedReady sim = go rest sim
       | otherwise =
           let (sim', bus) = simStepCached sim Nothing
            in bus : waiting rest sim'