Functional leakage invariants, and case on its own line

proof/Proof/Core/Functional/Driver.hs

@@ -112,16 +112,18 @@ storeHazard sys@(Sys core _ _) =
     || maybe False (Core.Instruction.storeHazard dePc) meStore
   where
     dePc = stateDePc core
-    exStore = case stateExInstr core of
-      SType size imm rs1 _ ->
-        Just
-          ( unpack (alu ADD (exArg sys rs1) (signExtend imm)),
-            size
-          )
-      _ -> Nothing
-    meStore = case stateMeInstr core of
-      SType size _ _ _ -> Just (stateMeAddr core, size)
-      _ -> Nothing
+    exStore =
+      case stateExInstr core of
+        SType size imm rs1 _ ->
+          Just
+            ( unpack (alu ADD (exArg sys rs1) (signExtend imm)),
+              size
+            )
+        _ -> Nothing
+    meStore =
+      case stateMeInstr core of
+        SType size _ _ _ -> Just (stateMeAddr core, size)
+        _ -> Nothing
 
 -- | The load-hazard condition of 'Core.decode', between the instruction
 -- arriving on 'inputMem' and the one in the execute stage.
@@ -189,11 +191,12 @@ driverCaseName sys@(Sys core _ _)
 -- that has left the execute stage but not yet halted the core -- @Nop Halted@
 -- is a bubble like the stall reasons, so the hop runs on until the core halts.
 isBubble :: SysG r m -> Bool
-isBubble (Sys core _ _) = case stateExInstr core of
-  Nop DecodeFail -> False
-  Nop Halted -> isNothing (stateHalt core)
-  Nop _ -> True
-  _ -> False
+isBubble (Sys core _ _) =
+  case stateExInstr core of
+    Nop DecodeFail -> False
+    Nop Halted -> isNothing (stateHalt core)
+    Nop _ -> True
+    _ -> False
 
 -- | The operational reading of the driver's stated invariant: step until the
 -- execute stage holds something that is not a no-op. Returns the number of

proof/Proof/Core/Functional/Invariant.hs

@@ -332,12 +332,14 @@ haltedCaseAt kind wr wa (IsaState ipc irf imem) (Sys core inp mem) =
     && memReadByte wa imem == memReadByte wa mem
     && lookupRFg wr irf == lookupRFg wr (stateRegFile core)
   where
-    isKind = case kind of
-      HaltBreak -> isBreak
-      HaltCall -> isCall
-    expected = case kind of
-      HaltBreak -> EBreak (ipc + 4)
-      HaltCall -> Syscall (ipc + 4)
+    isKind =
+      case kind of
+        HaltBreak -> isBreak
+        HaltCall -> isCall
+    expected =
+      case kind of
+        HaltBreak -> EBreak (ipc + 4)
+        HaltCall -> Syscall (ipc + 4)
 
 -- The architectural state, and properties of the invariant --------------------
 
@@ -375,10 +377,11 @@ sysInvAt wr wa sys = invAt wr wa (isaOf sys) sys
 -- the trapping instruction's, which is the resume address the halt carries
 -- minus 4.
 archPc :: SysG r m -> Address
-archPc (Sys core _ _) = case Core.stateHalt core of
-  Nothing -> Core.stateExPc core
-  Just (EBreak resume) -> resume - 4
-  Just (Syscall resume) -> resume - 4
+archPc (Sys core _ _) =
+  case Core.stateHalt core of
+    Nothing -> Core.stateExPc core
+    Just (EBreak resume) -> resume - 4
+    Just (Syscall resume) -> resume - 4
 
 -- | The register file the core stands for: its own, with the writes still in
 -- the pipeline (the memory and writeback stages) applied.

proof/Proof/Core/Functional/Obligation.hs

@@ -87,9 +87,10 @@ indStep0 wr wa sys =
   not premises || conclusion
   where
     isa = isaOf sys
-    isa' = case isaStep isa of
-      Next next -> next
-      IsaHalted -> isa
+    isa' =
+      case isaStep isa of
+        Next next -> next
+        IsaHalted -> isa
 
     sys' = stepSys sys
 
@@ -110,9 +111,10 @@ indStep1 wr wa sys =
   not premises || conclusion
   where
     isa = isaOf sys
-    isa' = case isaStep isa of
-      Next next -> next
-      IsaHalted -> isa
+    isa' =
+      case isaStep isa of
+        Next next -> next
+        IsaHalted -> isa
 
     sys' = stepSysN 1 sys
 
@@ -133,9 +135,10 @@ indStep2 wr wa sys =
   not premises || conclusion
   where
     isa = isaOf sys
-    isa' = case isaStep isa of
-      Next next -> next
-      IsaHalted -> isa
+    isa' =
+      case isaStep isa of
+        Next next -> next
+        IsaHalted -> isa
 
     sys' = stepSysN 2 sys
 
@@ -158,9 +161,10 @@ indStep3 wr wa sys =
   not premises || conclusion
   where
     isa = isaOf sys
-    isa' = case isaStep isa of
-      Next next -> next
-      IsaHalted -> isa
+    isa' =
+      case isaStep isa of
+        Next next -> next
+        IsaHalted -> isa
 
     sys' = stepSysN 3 sys
 

proof/Proof/Core/Leakage/Driver.hs

@@ -34,12 +34,14 @@ simStoreHazard inp st =
     || maybe False (Core.Instruction.storeHazard dePc) meStore
   where
     dePc = simStateDePc st
-    exStore = case inp of
-      Just (LStore size addr) -> Just (addr, size)
-      _ -> Nothing
-    meStore = case simStateMeInstr st of
-      LStore size addr -> Just (addr, size)
-      _ -> Nothing
+    exStore =
+      case inp of
+        Just (LStore size addr) -> Just (addr, size)
+        _ -> Nothing
+    meStore =
+      case simStateMeAccess st of
+        SimStore size addr -> Just (addr, size)
+        _ -> Nothing
 
 -- | The load-hazard condition of 'Core.Pipeline.decode', computed by the ISA as
 -- part of the leakage.
@@ -56,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
-  | not (isMemLeak (simStateMeInstr st)) = 1
+  | simStateMeAccess st == SimNoAccess = 1
   | not (maybe False isMemLeak inp) = 2
   | otherwise = 3
 
@@ -65,10 +67,11 @@ simDriver inp st
 -- decoded instruction is not, and neither is a halted simulator; the stall
 -- reasons are.
 simIsBubble :: SimState -> Bool
-simIsBubble sim = case simStateExInstrType sim of
-  DecodedInstr -> False
-  Halted -> False
-  _ -> True
+simIsBubble sim =
+  case simStateExInstrType sim of
+    DecodedInstr -> False
+    Halted -> False
+    _ -> True
 
 -- | The operational reading of 'simDriver', as
 -- 'Proof.Core.Functional.Driver.driverSpec' is of the core's: step on the

proof/Proof/Core/Leakage/Invariant.hs

@@ -1,15 +1,15 @@
 -- | The invariant relating the leakage simulator to the core: the leakage
 -- counterpart of "Proof.Core.Functional.Invariant".
 module Proof.Core.Leakage.Invariant
-  ( simInv
+  ( simInv,
+    simInvFunctional,
   )
 where
 
 import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log)
 import Core.Pipeline as Core
-import Data.Maybe (isJust, isNothing)
+import Data.Maybe (isJust)
 import Core.Instruction hiding (Halted)
-import Proof.Core.Leakage.Model
 import Proof.Core.Leakage.Simulator
 import Proof.Core.Functional.Machine
 import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||))
@@ -19,7 +19,8 @@ import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&
 --
 -- The two machines fetch and decode at the same PCs, agree on whether decode
 -- expects an instruction, are both running or both halted, and have the same
--- memory access pending in the memory stage. Which instruction the core is
+-- memory access pending in the memory stage. The simulator's control lines
+-- are at rest, as they are after every cycle. Which instruction the core is
 -- executing is not stated here: the functional invariant pins the core's
 -- execute stage to the ISA's next instruction, and the simulator is fed that
 -- instruction's leakage, so the two agree by construction.
@@ -38,15 +39,27 @@ simInv sim (Sys core _ _) =
     && simStateDeExpInstr sim == stateDeExpInstr core
     && exStage
     && meStage
+    && simStateCtrl sim == simInitCtrl
   where
-    exStage = case simStateExInstrType sim of
-      DecodedInstr -> isNothing (stateHalt core)
-      Halted -> isJust (stateHalt core)
-      _ -> False
+    exStage
+      | isJust (stateHalt core) = simStateExInstrType sim == Halted
+      | otherwise = simStateExInstrType sim == DecodedInstr
 
-    meStage = case (simStateMeInstr sim, stateMeInstr core) of
-      (LLoad size addr _, Core.Instruction.IType (Load size' _) _ _ _) ->
-        size == size' && addr == stateMeAddr core
-      (LStore size addr, Core.Instruction.SType size' _ _ _) ->
-        size == size' && addr == stateMeAddr core
-      (leak, ir) -> not (isMemLeak leak) && not (Core.Instruction.isMemInstr ir)
+    meStage =
+      case stateMeInstr core of
+        Core.Instruction.IType (Load size _) _ _ _ ->
+          simStateMeAccess sim == SimLoad size (stateMeAddr core)
+        Core.Instruction.SType size _ _ _ ->
+          simStateMeAccess sim == SimStore size (stateMeAddr core)
+        _ -> simStateMeAccess sim == SimNoAccess
+
+-- | 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
+-- decode flag, its execute stage by whether the core has halted, its memory
+-- stage by the core's, and its control lines, which are at rest.
+simInvFunctional :: SimState -> SimState -> SysG r m -> Bool
+simInvFunctional sim1 sim2 sys =
+  not premises || conclusion
+  where
+    premises = simInv sim1 sys && simInv sim2 sys
+    conclusion = sim1 == sim2

proof/Proof/Core/Leakage/Model.hs

@@ -76,11 +76,12 @@ obsOf o = obsReq (outputMem o)
 
 -- | The observation of a request on the bus: the request without its data.
 obsReq :: Request -> Obs
-obsReq req = case req of
-  Nothing -> NoAccess
-  Just (MemFetch addr) -> Fetch addr
-  Just (MemRead addr size) -> DataRead addr size
-  Just (MemWrite addr size _) -> DataWrite addr size
+obsReq req =
+  case req of
+    Nothing -> NoAccess
+    Just (MemFetch addr) -> Fetch addr
+    Just (MemRead addr size) -> DataRead addr size
+    Just (MemWrite addr size _) -> DataWrite addr size
 
 -- Leakage ---------------------------------------------------------------------
 

proof/Proof/Core/Leakage/Simulator.hs

@@ -12,6 +12,7 @@ module Proof.Core.Leakage.Simulator
   ( SimInput,
     SimOutput,
     SimExInstrType (..),
+    SimMemAccess (..),
     SimState (..),
     SimControl (..),
     SimM,
@@ -68,6 +69,15 @@ data SimExInstrType
     Halted
   deriving (Eq, Show, Generic, NFDataX)
 
+-- | 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
+  | SimLoad Size Address
+  | SimStore Size Address
+  deriving (Eq, Show, Generic, NFDataX)
+
 -- | The internal state of the simulator.
 data SimState = SimState
   { -- | Program counter fetch stage.
@@ -78,8 +88,8 @@ data SimState = SimState
     simStateDeExpInstr :: Bool,
     -- | Instruction execute stage.
     simStateExInstrType :: SimExInstrType,
-    -- | Instruction memory stage.
-    simStateMeInstr :: Leak,
+    -- | What the instruction in the memory stage does with memory.
+    simStateMeAccess :: SimMemAccess,
     -- | Control/forwarding lines.
     simStateCtrl :: SimControl
   }
@@ -150,7 +160,7 @@ simInit =
       simStateDePc = 0,
       simStateDeExpInstr = False,
       simStateExInstrType = FirstCycle,
-      simStateMeInstr = LArith,
+      simStateMeAccess = SimNoAccess,
       simStateCtrl = simInitCtrl
     }
 
@@ -274,37 +284,38 @@ simExecute = do
     DecodedInstr ->
       case input of
         Just ir -> do
-          modify $ \s -> s {simStateMeInstr = ir}
-
           case ir of
-            LArith -> pure ()
-            LJump addr ->
+            LArith ->
+              modify $ \s -> s {simStateMeAccess = SimNoAccess}
+            LJump addr -> do
+              modify $ \s -> s {simStateMeAccess = SimNoAccess}
               simSetLines $ \c -> c {simCtrlExJumpAddr = Just addr}
-            LLoad _ _ haz ->
+            LLoad size addr haz -> do
+              modify $ \s -> s {simStateMeAccess = SimLoad size addr}
               simSetLines $ \c -> c {simCtrlExLoadHazard = Just haz}
-            LStore size addr ->
+            LStore size addr -> do
+              modify $ \s -> s {simStateMeAccess = SimStore size addr}
               simSetLines $ \c -> c {simCtrlExStoreAddrSize = Just (addr, size)}
-            LEnv ->
+            LEnv -> do
+              modify $ \s -> s {simStateMeAccess = SimNoAccess}
               simSetLines $ \c -> c {simCtrlExEnvInstr = True}
-        Nothing -> modify $ \s -> s {simStateMeInstr = LArith}
-    _ -> modify $ \s -> s {simStateMeInstr = LArith}
+        Nothing -> modify $ \s -> s {simStateMeAccess = SimNoAccess}
+    _ -> modify $ \s -> s {simStateMeAccess = SimNoAccess}
 
 -- | Memory stage.
 simMemory :: SimM ()
 simMemory = do
-  ir <- gets simStateMeInstr
+  ir <- gets simStateMeAccess
 
   case ir of
-    LArith -> pure ()
-    LJump _ -> pure ()
-    LLoad size addr _ -> do
+    SimNoAccess -> pure ()
+    SimLoad size addr -> do
       simSetLines $ \c -> c {simCtrlMeMemInstr = True}
       simReadRAM addr size
-    LStore size addr -> do
+    SimStore size addr -> do
       simSetLines $ \c ->
         c {simCtrlMeMemInstr = True, simCtrlMeStoreAddrSize = Just (addr, size)}
       simWriteRAM addr size
-    LEnv -> pure ()
 
 -- | Writeback stage.
 simWriteback :: SimM ()