From 6bae771110c49a1a863725492acb3bc4579f3540 Mon Sep 17 00:00:00 2001 From: Kristina Date: Sat, 7 Nov 2026 14:36:01 +0100 Subject: [PATCH 1/3] Rename SimMemAccess to SimDataAccess The simulator's memory stage holds only data accesses, so SimMemAccess read like a counterpart of Core.Pipeline.MemAccess, which includes fetches. SimNoAccess was also easy to confuse with the observation NoAccess, which means the bus shows nothing. Co-Authored-By: Claude Opus 5.5 --- proof/Proof/Core/Leakage/Driver.hs | 2 +- proof/Proof/Core/Leakage/Invariant.hs | 2 +- proof/Proof/Core/Leakage/Simulator.hs | 22 +++++++++++----------- proof/Proof/SMT/Symbolic.hs | 4 ++-- 4 files changed, 15 insertions(+), 15 deletions(-) diff --git a/proof/Proof/Core/Leakage/Driver.hs b/proof/Proof/Core/Leakage/Driver.hs index f6908ff..3259254 100644 --- a/proof/Proof/Core/Leakage/Driver.hs +++ b/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 diff --git a/proof/Proof/Core/Leakage/Invariant.hs b/proof/Proof/Core/Leakage/Invariant.hs index 17f781d..fa7f7ae 100644 --- a/proof/Proof/Core/Leakage/Invariant.hs +++ b/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 diff --git a/proof/Proof/Core/Leakage/Simulator.hs b/proof/Proof/Core/Leakage/Simulator.hs index 2e7b996..5d8bcd2 100644 --- a/proof/Proof/Core/Leakage/Simulator.hs +++ b/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,10 +297,10 @@ 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 () @@ -308,7 +308,7 @@ simMemory = do ir <- gets simStateMeAccess case ir of - SimNoAccess -> pure () + SimNoDataAccess -> pure () SimLoad size addr -> do simSetLines $ \c -> c {simCtrlMeMemInstr = True} simReadRAM addr size diff --git a/proof/Proof/SMT/Symbolic.hs b/proof/Proof/SMT/Symbolic.hs index ebd5511..c85531d 100644 --- a/proof/Proof/SMT/Symbolic.hs +++ b/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 From 58119ff8060a864989975b19b63e4954e84a00d4 Mon Sep 17 00:00:00 2001 From: Kristina Date: Sat, 7 Nov 2026 15:07:42 +0100 Subject: [PATCH 2/3] Call the cached simulator's flag ready rather than answered The Boolean in SimCachedSys says whether the simulator is ready to receive an input. Describing it as "the cache answered in the previous cycle" needed a made-up justification for its initial value True, since nothing has answered before the start. The field is now simCachedReady, and the comments on the type, its initial state and its step describe it as readiness. Co-Authored-By: Claude Opus 5.5 --- .../Cache4K/CachedCore/Leakage/Driver.hs | 6 ++--- .../Cache4K/CachedCore/Leakage/Invariant.hs | 6 ++--- .../Cache4K/CachedCore/Leakage/Simulator.hs | 25 ++++++++----------- test/CacheProofSpec.hs | 2 +- 4 files changed, 18 insertions(+), 21 deletions(-) diff --git a/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Driver.hs b/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Driver.hs index 0540698..d617c0e 100644 --- a/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Driver.hs +++ b/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Driver.hs @@ -36,7 +36,7 @@ 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)) @@ -55,10 +55,10 @@ simCachedDriverSpec fuel sim0 inp = go 0 (fst (simStepCached sim0 inp)) -- '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) diff --git a/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Invariant.hs b/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Invariant.hs index 8331669..774e573 100644 --- a/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Invariant.hs +++ b/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Invariant.hs @@ -24,8 +24,8 @@ import Proof.Memory.Cache4K.Server.Leakage.Simulator (SimCacheSrv (..)) -- proof ('Proof.Memory.Cache4K.Server.Leakage.Invariant.srvSimInvAt'), and the -- simulator records that an answer has just arrived. 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 @@ -44,7 +44,7 @@ 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 diff --git a/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Simulator.hs b/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Simulator.hs index d532d11..c607f0a 100644 --- a/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Simulator.hs +++ b/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) diff --git a/test/CacheProofSpec.hs b/test/CacheProofSpec.hs index aa4a78d..2a77ea0 100644 --- a/test/CacheProofSpec.hs +++ b/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' From df8bdf87be10bbac9a6dc6438e669de9e673f20a Mon Sep 17 00:00:00 2001 From: Kristina Date: Sat, 7 Nov 2026 15:10:29 +0100 Subject: [PATCH 3/3] Describe the cached simulator's flag as readiness in the remaining comments The invariant and driver of link 2's leakage half still described the flag as "the last cycle brought an answer". They now call it readiness to receive an input, as the simulator itself does. Co-Authored-By: Claude Opus 5.5 --- .../Memory/Cache4K/CachedCore/Leakage/Driver.hs | 12 ++++++------ .../Memory/Cache4K/CachedCore/Leakage/Invariant.hs | 8 ++++---- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Driver.hs b/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Driver.hs index d617c0e..11abd9f 100644 --- a/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Driver.hs +++ b/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) @@ -40,8 +40,8 @@ simCachedDriverSpec fuel sim0 inp = go 0 (fst (simStepCached sim0 inp)) | 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 @@ -49,8 +49,8 @@ simCachedDriverSpec fuel sim0 inp = go 0 (fst (simStepCached sim0 inp)) -- -- 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. diff --git a/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Invariant.hs b/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Invariant.hs index 774e573..d28206e 100644 --- a/proof/Proof/Memory/Cache4K/CachedCore/Leakage/Invariant.hs +++ b/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 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'). @@ -48,7 +48,7 @@ cachedSimInvFunctional wsi sim1 sim2 csys = -- | 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