diff --git a/app/Main.hs b/app/Main.hs index 9461fe3..c656b90 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,20 +1,18 @@ module Main (main) where -import Access import Clash.Prelude hiding (Log, Ordering (..), Word, break, def, init, lift, log, resize) import Control.Exception (catch) import Control.Monad (when) import Control.Monad.IO.Class (MonadIO, liftIO) import qualified Core as Core -import Data.Functor.Identity import Data.IORef import Elf.ElfLoader import Elf.Syscall (ProgramExitException (..), handleSyscall) -import Memory.IO (IOMemT, SecureIOMemT, ioMemInitSP, loadProgram, loadSecureProgram, newIOMem, newSecureIOMem, runIOMemT, runSecureIOMemT, secureIOMemInitSP) +import Memory.IO (IOMemT, ioMemInitSP, loadProgram, newIOMem, runIOMemT) import Memory.Types import Numeric (showHex) import Options.Applicative -import RegFile +import Core.RegFile import Simulate import System.Exit (ExitCode (..), exitWith) import Types (Word) @@ -25,7 +23,6 @@ import Prelude hiding (Ordering (..), Word, break, init, log, map, not, repeat, -- | Command line options data Options = Options { optVerbose :: Bool - , optSecureMemory :: Bool , optExecutable :: String } deriving (Show) @@ -36,13 +33,6 @@ verboseParser = switch <> short 'v' <> help "Enable verbose output (shows PC and instruction trace)" ) --- | Parser for secure memory flag -secureMemoryParser :: Parser Bool -secureMemoryParser = switch - ( long "secure-memory" - <> short 's' - <> help "Enable secure memory tracking (PubSec mode)" ) - -- | Parser for executable argument executableParser :: Parser String executableParser = strArgument @@ -53,7 +43,6 @@ executableParser = strArgument optionsParser :: Parser Options optionsParser = Options <$> verboseParser - <*> secureMemoryParser <*> executableParser -- | Program info for help generation @@ -64,14 +53,13 @@ programInfo = info (optionsParser <**> helper) <> header "uc-risc-v - RISC-V Simulator" <> footer "Examples:\n\ \ uc-risc-v benchmark/bench_chacha20\n\ - \ uc-risc-v --verbose benchmark/bench_blake2b\n\ - \ uc-risc-v --secure-memory benchmark/bench_secure_memory" ) + \ uc-risc-v --verbose benchmark/bench_blake2b" ) -- | Called by 'runElf' whenever the core halts on a syscall: optionally log the -- state, remember it as the final state, and service the syscall. instrument :: - (Access f, Show (f Word), MonadIO m, MonadMemory m) => - String -> Bool -> IORef (Maybe (Core.State f)) -> Instrument f m + (MonadIO m, MonadMemory m) => + String -> Bool -> IORef (Maybe Core.State) -> Instrument m instrument modeName shouldLog finalStateRef s = do let pc = Core.stateExPc s @@ -98,42 +86,20 @@ runExecutable Options{..} = do when optVerbose $ do putStrLn $ "Entry point: 0x" P.++ showHex entryOffset "" - if optSecureMemory - then putStrLn "Starting execution in SECURE MEMORY mode..." - else putStrLn "Starting execution in standard mode..." - - if optSecureMemory - then do - secureIOMem <- newSecureIOMem elf - finalStateRef <- newIORef Nothing - runSecureIOMemT secureIOMem $ do - loadSecureProgram elf - runElf - (instrument "SECURE" optVerbose finalStateRef) - (simulator @PubSec @(SecureIOMemT IO)) - { circuitState = - Core.initAt - (fromIntegral entryOffset) - (modifyRF 2 (pure $ secureIOMemInitSP secureIOMem) (initRF @PubSec)) - } - finalState <- readIORef finalStateRef - case finalState of - Just state | Core.stateHalt state == Just Core.SecurityViolation -> - putStrLn "Program aborted due to security violation" - _ -> pure () - else do - mem <- newIOMem elf - finalStateRef <- newIORef Nothing - runIOMemT mem $ do - loadProgram elf - runElf - (instrument "STANDARD" optVerbose finalStateRef) - (simulator @Identity @(IOMemT IO)) - { circuitState = - Core.initAt - (fromIntegral entryOffset) - (modifyRF 2 (pure $ ioMemInitSP mem) (initRF @Identity)) - } + putStrLn "Starting execution..." + + mem <- newIOMem elf + finalStateRef <- newIORef Nothing + runIOMemT mem $ do + loadProgram elf + runElf + (instrument "STANDARD" optVerbose finalStateRef) + (simulator @(IOMemT IO)) + { circuitState = + Core.initAt + (fromIntegral entryOffset) + (modifyRF 2 (ioMemInitSP mem) initRF) + } when optVerbose $ putStrLn "Execution completed successfully" diff --git a/package.yaml b/package.yaml index 987ec75..a49a311 100644 --- a/package.yaml +++ b/package.yaml @@ -19,9 +19,9 @@ extra-source-files: # common to point users to the README.md file. description: Please see the README on GitHub at -# The modules under proof-smt/ discharge their properties through an SMT solver -# while GHC compiles them, so building them needs a solver on PATH and takes as -# long as the solver does. Pantomime goes through SBV, and SBV's Z3 backend is +# The modules listed under the smt-proof flag in the library discharge their +# properties through an SMT solver while GHC compiles them, so building them +# needs a solver on PATH and takes as long as the solver does. Pantomime goes through SBV, and SBV's Z3 backend is # pointed at a different binary with SBV_Z3; Z3 itself does not finish these in # useful time, while bitwuzla discharges each in under a minute: # @@ -107,39 +107,52 @@ library: - proof when: - condition: flag(smt-proof) - source-dirs: proof-smt exposed-modules: - - Proof.Functional.Induction - - Proof.Leakage.Induction - - Proof.SMT.Array + - Proof.Cache.Functional.Solver + - Proof.Core.Functional.Solver + - Proof.Core.Leakage.Solver - Proof.SMT.Axioms + - Proof.Cache.SMT.Array + - Proof.Cache.SMT.Axioms + - Proof.Cache.SMT.Coherent - Proof.SMT.Logged - Proof.SMT.Sanity - - Proof.SMT.System + - Proof.Core.Functional.System cpp-options: -DSMT_PROOF + # Listed explicitly, with no automatic discovery: the solver modules above + # live in proof/ too, and must only be built with the smt-proof flag. + other-modules: [] exposed-modules: - - Proof.Machine - - Proof.Functional.Driver - - Proof.Functional.Invariant - - Proof.Functional.Obligation - - Proof.Leakage.Model - - Proof.Leakage.Simulator - - Proof.Leakage.Driver - - Proof.Leakage.Invariant - - Proof.Leakage.Obligation - - Access + - Proof.Cache.Functional.Contract + - Proof.Cache.Functional.Driver + - Proof.Cache.Functional.Invariant + - Proof.Cache.Functional.Obligation + - Proof.Cache.SMT.Raw + - Proof.SMT.Array + - Proof.Core.Functional.Machine + - Proof.Core.Functional.Driver + - Proof.Core.Functional.Invariant + - Proof.Core.Functional.Obligation + - Proof.Core.Leakage.Model + - Proof.Core.Leakage.Simulator + - Proof.Core.Leakage.Driver + - Proof.Core.Leakage.Invariant + - Proof.Core.Leakage.Obligation - Core - Elf.ElfLoader - Elf.Syscall - HardwareSim - - Instruction - - ISA + - Core.Instruction + - Core.ISA - Memory.Types + - Memory.Ideal - Memory.Vec - Memory.ST - Memory.IO + - Memory.Cache4K + - Memory.Cache4KServer - Pretty - - RegFile + - Core.RegFile - Simulate - Types - Util @@ -160,6 +173,13 @@ tests: aimcore-test: main: Spec.hs source-dirs: test + # Listed explicitly: Cache4KSpec and CompositionSpec are still written + # against the cache's old interface and wait for the cache's leakage proof. + other-modules: + - BenchmarkSpec + - InstructionSpec + - IsaSpec + - ProofSpec when: - condition: flag(smt-proof) cpp-options: -DSMT_PROOF diff --git a/proof-smt/Proof/Functional/Induction.hs b/proof-smt/Proof/Functional/Induction.hs deleted file mode 100644 index 02c41a5..0000000 --- a/proof-smt/Proof/Functional/Induction.hs +++ /dev/null @@ -1,119 +0,0 @@ --- | The inductive steps of the refinement proof, checked symbolically. --- --- 'baseCase' says the invariant holds once the reset state has taken its first --- hop. Then one property per driver --- delay: if the invariant relates @(isa, sys)@ and the driver says the hop takes --- @k + 1@ cycles, then after those cycles (and one ISA step, where the hop --- retires an instruction) the invariant relates them again. Base case plus the --- four steps is the whole refinement theorem. --- --- Checking one @k@ at a time keeps the number of unrolled cycles concrete, --- which sidesteps Pantomime's termination check: @stepSysN (driver sys + 1)@ --- would recurse on a symbolic count. --- --- Each property is checked by the plugin at compile time and spliced into --- 'results': 'Nothing' when valid, @'Just' counterexample@ when not. The --- statements themselves live in "Proof.Functional.Obligation", shared with the QuickCheck --- harness so the two cannot drift. --- --- The pipeline state is passed as a 'KState' plus SMT-array register file and --- memory; see "Proof.SMT.System". -module Proof.Functional.Induction - ( arrRoundTrip, - shiftsSane, - baseCase, - indStep, - indStep1, - indStep2, - indStep3, - results, - ) -where - -import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) -import qualified Core -import Data.Functor.Identity -import Pantomime (Theory (..)) -import qualified Pantomime.BuiltIn as Pantomime -import Proof.Functional.Obligation -import Proof.SMT.Array -import Proof.SMT.Axioms (arrayAxioms) -import Proof.SMT.Logged (pantomime) -import Proof.SMT.System -import Types -import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) - --- Sanity probes for the trusted embeddings ------------------------------------- --- --- The term axioms in "Proof.SMT.Axioms" replace Haskell functions by hand-written SMT --- counterparts, so they are trusted, not proved. These two probes check each --- embedding against facts a broken one would get wrong. - --- | The register-file array embedding: a read after a write at the same index --- gives the written value. -{-# ANN arrRoundTrip (Theory arrayAxioms) #-} -arrRoundTrip :: RegArr -> RegIdx -> Word -> Pantomime.Bool -arrRoundTrip a i v = Pantomime.boolean $ loadRA (storeRA a i v) i == v - --- | The shift embeddings: identities that would fail if the three shifts were --- mixed up, the zero-extension of the amount were wrong, or the arithmetic --- shift lost its sign. -{-# ANN shiftsSane (Theory arrayAxioms) #-} -shiftsSane :: Word -> Pantomime.Bool -shiftsSane x = - Pantomime.boolean $ - Core.sllWord x 0 == x - && Core.srlWord x 0 == x - && Core.sraWord x 0 == x - && Core.sllWord x 1 == x + x - && Core.srlWord x 31 == (if sign == 1 then 1 else 0) - && Core.sraWord x 31 == (if sign == 1 then 0xFFFFFFFF else 0) - where - sign = slice d31 d31 x - --- The base case ---------------------------------------------------------------- - -{-# ANN baseCase (Theory arrayAxioms) #-} -baseCase :: RegArr -> MemArr -> RegIdx -> Address -> Address -> Pantomime.Bool -baseCase ra ma wr wa pc = - Pantomime.boolean $ baseCaseObligation (RegArrF ra) ma wr wa pc - --- The inductive steps ---------------------------------------------------------- - --- | @k = 0@: the one-cycle hop (steady, writeback non-memory). -{-# ANN indStep (Theory arrayAxioms) #-} -indStep :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> Pantomime.Bool -indStep ss i ra ma wr wa ipc = - Pantomime.boolean $ indStepObligation wr wa ipc (sysOf ss i ra ma) - --- | @k = 1@: the two-cycle hop (a memory instruction in writeback). -{-# ANN indStep1 (Theory arrayAxioms) #-} -indStep1 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> Pantomime.Bool -indStep1 ss i ra ma wr wa ipc = - Pantomime.boolean $ indStepObligation1 wr wa ipc (sysOf ss i ra ma) - --- | @k = 2@: the three-cycle hop (environment, taken jump, store hazard with a --- non-memory execute instruction, or memory instructions in both older stages). --- The hop on which the ISA enters a halt; a halted state then sits at k = 0. -{-# ANN indStep2 (Theory arrayAxioms) #-} -indStep2 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> Pantomime.Bool -indStep2 ss i ra ma wr wa ipc = - Pantomime.boolean $ indStepObligation2 wr wa ipc (sysOf ss i ra ma) - --- | @k = 3@: the four-cycle hop (store hazard with a memory execute --- instruction, load hazard, or all three stages holding memory instructions). -{-# ANN indStep3 (Theory arrayAxioms) #-} -indStep3 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> Pantomime.Bool -indStep3 ss i ra ma wr wa ipc = - Pantomime.boolean $ indStepObligation3 wr wa ipc (sysOf ss i ra ma) - -results :: [(String, Maybe String)] -results = - [ ("arrRoundTrip", $(pantomime 'arrRoundTrip)), - ("shiftsSane", $(pantomime 'shiftsSane)), - ("baseCase", $(pantomime 'baseCase)), - ("indStep", $(pantomime 'indStep)), - ("indStep1", $(pantomime 'indStep1)), - ("indStep2", $(pantomime 'indStep2)), - ("indStep3", $(pantomime 'indStep3)) - ] diff --git a/proof/Proof/Cache/Functional/Contract.hs b/proof/Proof/Cache/Functional/Contract.hs new file mode 100644 index 0000000..865378b --- /dev/null +++ b/proof/Proof/Cache/Functional/Contract.hs @@ -0,0 +1,83 @@ +-- | The contract between the core and the 4 KiB cache in front of memory: what +-- each side promises beyond the cache's proof against ideal memory +-- ("Proof.Cache.Functional.Obligation"), so that the core runs behind the +-- cache as it would behind ideal memory, with stutter steps inserted. +-- +-- The two sides are not symmetric: the core makes the requests and the cache +-- answers them. +-- +-- * The core waits for what it asked for ('waitsAfterRequest'): after a +-- request, given no answer, it makes no request and its state stays the +-- same. +-- * The cache answers 'Nothing' only while a request is outstanding: a +-- server related to ideal memory by the invariant is ready +-- ('readyUnderInv'), and a ready server asked nothing answers within the +-- cycle ('readyIdleNoWait'). While a request is outstanding, the driver and the +-- cache's step obligations say how it answers: 'Nothing' for as many cycles +-- as the driver counts, then ideal memory's answer. +-- +-- The properties are checked in "Proof.Cache.Functional.Solver". +module Proof.Cache.Functional.Contract + ( isReady, + readyUnderInv, + readyIdleNoWait, + sameCoreAt, + waitsAfterRequest, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Core (Input (..), Output (..), StateG (..), circuit) +import Data.Maybe (isNothing) +import Memory.Cache4KServer (CacheSrv (..), CacheSrvState (..)) +import Memory.Types (MemOps) +import Proof.Cache.Functional.Driver (driver) +import Proof.Cache.Functional.Invariant (srvInvAt) +import Core.RegFile (RegFileOps (..)) +import Types (Address, RegIdx) +import Memory.Cache4K (SetIdx, WordIdx) +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- The cache's side -------------------------------------------------------------- + +-- | Is the server ready for a request: no read waiting for memory? +isReady :: CacheSrv m -> Bool +isReady (CacheSrv _ _ st) = st == CacheSrvReady + +-- | A server related to ideal memory by the invariant is ready. +readyUnderInv :: (MemOps m) => Address -> SetIdx -> WordIdx -> m -> CacheSrv m -> Bool +readyUnderInv wa wsi wwi ideal srv = not (srvInvAt wa wsi wwi ideal srv) || isReady srv + +-- | A ready server that is asked nothing answers within the cycle. +readyIdleNoWait :: CacheSrv m -> Bool +readyIdleNoWait srv = not (isReady srv) || driver srv Nothing == 0 + +-- The core's side --------------------------------------------------------------- + +-- | Two core states agree at register @wr@: every field is equal, the register +-- file at @wr@. Quantifying over @wr@ gives equality of the states. +sameCoreAt :: (RegFileOps r) => RegIdx -> StateG r -> StateG r -> Bool +sameCoreAt wr s1 s2 = + stateFePc s1 == stateFePc s2 + && stateDePc s1 == stateDePc s2 + && stateDeExpInstr s1 == stateDeExpInstr s2 + && stateExPc s1 == stateExPc s2 + && stateExInstr s1 == stateExInstr s2 + && stateMeInstr s1 == stateMeInstr s2 + && stateMeRes s1 == stateMeRes s2 + && stateMeAddr s1 == stateMeAddr s2 + && stateWbInstr s1 == stateWbInstr s2 + && stateWbRes s1 == stateWbRes s2 + && lookupRFg wr (stateRegFile s1) == lookupRFg wr (stateRegFile s2) + && stateCtrl s1 == stateCtrl s2 + && stateHalt s1 == stateHalt s2 + +-- | The core waits for what it asked for: after a request, given no answer, it +-- makes no request and stays where it was (at register @wr@). +waitsAfterRequest :: (RegFileOps r) => RegIdx -> StateG r -> Input -> Bool +waitsAfterRequest wr s inp = case outMem o of + Nothing -> True + Just _ -> isNothing (outMem o') && sameCoreAt wr s'' s' + where + (s', o) = circuit s inp + (s'', o') = circuit s' (Input Nothing) diff --git a/proof/Proof/Cache/Functional/Driver.hs b/proof/Proof/Cache/Functional/Driver.hs new file mode 100644 index 0000000..a699231 --- /dev/null +++ b/proof/Proof/Cache/Functional/Driver.hs @@ -0,0 +1,54 @@ +-- | The cache's driver: how many cycles after a request the cache's answer is +-- final -- the cache's counterpart of "Proof.Core.Functional.Driver". +-- +-- * 'driver', a case table over the cache and the request, and +-- * 'driverRef', the operational reading, obtained by actually serving. +module Proof.Cache.Functional.Driver + ( driver, + driverRef, + ) +where + +import Core (MemAccess (..), Request) +import Memory.Cache4K (cacheHit, setOf) +import Memory.Cache4KServer +import Memory.Types (MemOps (..)) +import Types + +-- | The cycles after the request until the cache's answer is final: 'penalty' +-- for every line a data read misses, nothing for anything else. A read touches +-- the lines of its first and last byte; within four bytes those are different +-- lines exactly when they are in different sets. The driver is only ever run +-- from servers that satisfy the invariant +-- ('Proof.Cache.Functional.Invariant.srvInvAt'), which are ready, so the +-- server's state is not consulted; elsewhere it need not agree with +-- 'driverRef'. +driver :: CacheSrv m -> Request -> Cycles +driver (CacheSrv c _ _) req = case req of + Just (MemRead addr size) -> + let off = case size of + Byte -> 0 + Half -> 1 + Word -> 3 + + hit1stLine = cacheHit addr c + penalty1stLine = if hit1stLine then 0 else penalty + + hit2ndLine = setOf (addr + off) == setOf addr || cacheHit (addr + off) c + penalty2ndLine = if hit2ndLine then 0 else penalty + + in penalty1stLine + penalty2ndLine + _ -> 0 + +-- | The operational reading of 'driver': serve the request, then serve without +-- one until the server is ready again, and count every cycle of the hop, +-- including the request's. So, from a server that satisfies the invariant, +-- @'driverRef' fuel srv0 req == Just ('driver' srv0 req + 1)@. 'Nothing' if the +-- hop takes more than @fuel@ cycles. +driverRef :: (MemOps m) => Int -> CacheSrv m -> Request -> Maybe Int +driverRef fuel srv0 req = go 1 (fst (serve srv0 req)) + where + go n srv + | srvState srv == CacheSrvReady = Just n + | n >= fuel = Nothing + | otherwise = go (n + 1) (fst (serve srv Nothing)) diff --git a/proof/Proof/Cache/Functional/Invariant.hs b/proof/Proof/Cache/Functional/Invariant.hs new file mode 100644 index 0000000..bfb678d --- /dev/null +++ b/proof/Proof/Cache/Functional/Invariant.hs @@ -0,0 +1,37 @@ +-- | The cache's invariant -- the cache's counterpart of +-- "Proof.Core.Functional.Invariant". The cache holds 1024 words and memory +-- many more bytes, so the invariant is stated at a witness byte and a witness +-- word, and the obligations quantify over them, as the core's invariant does +-- over a register and a byte. +module Proof.Cache.Functional.Invariant + ( coherentAt, + srvInvAt + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Memory.Cache4K +import Memory.Cache4KServer +import Memory.Types (MemOps (..)) +import Types (Address) +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- | Coherence at word @wwi@ of set @wsi@: if the line there is valid, the word +-- is the one memory holds at its address. The cache is coherent if this holds +-- at every set and word. +coherentAt :: (MemOps m) => SetIdx -> WordIdx -> m -> Cache4K -> Bool +coherentAt wsi wwi mem c = + not (entryValid e) || dataRead (wsi ++# wwi) (dataArr c) == w + where + e = tagRead wsi (tagArr c) + w = memReadWord (wordAddr (entryTag e) wsi wwi 0) mem + +-- | The invariant at byte @wa@ and word @wwi@ of set @wsi@, relating the cache +-- server to ideal memory @ideal@: no miss is pending, the server's memory holds +-- ideal memory's byte @wa@, and if the line is valid, its word @wwi@ is the +-- server's memory's. +srvInvAt :: (MemOps m) => Address -> SetIdx -> WordIdx -> m -> CacheSrv m -> Bool +srvInvAt wa wsi wwi ideal (CacheSrv c mem st) = + st == CacheSrvReady && + memReadByte wa ideal == memReadByte wa mem && + coherentAt wsi wwi mem c diff --git a/proof/Proof/Cache/Functional/Obligation.hs b/proof/Proof/Cache/Functional/Obligation.hs new file mode 100644 index 0000000..0943dfe --- /dev/null +++ b/proof/Proof/Cache/Functional/Obligation.hs @@ -0,0 +1,139 @@ +{-# LANGUAGE InstanceSigs #-} +-- | The cache's proof obligations, in one place: the cache's counterpart of +-- "Proof.Core.Functional.Obligation". +-- +-- They relate the cached memory to ideal memory ("Memory.Ideal") one request at +-- a time: ideal memory answers in one cycle, the cached memory in +-- 'Proof.Cache.Functional.Driver.driver' + 1 cycles. As the core's obligations +-- build the ISA state from the system ('Proof.Core.Functional.Obligation.isaAt'), +-- these take ideal memory to be the server's memory before the hop; the +-- conclusion compares the memory ideal memory steps to with the server's after +-- the hop. +-- +-- From a server that satisfies the invariant the driver is 0, 'penalty' or +-- twice 'penalty' (no, one or two lines missed), so there is one step +-- obligation per hop length, named after it for @'penalty' = 4@. Split by +-- length because Pantomime unrolls recursion only when its count is concrete. +module Proof.Cache.Functional.Obligation + ( CoherentOps (..), + mkDataMem, + baseCase, + indStep0, + indStep4, + indStep8, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Core (Input (..), Request) +import Memory.Cache4K +import Memory.Cache4KServer +import Memory.Ideal (idealServe) +import Memory.Types (MemOps (..)) +import Proof.Cache.Functional.Driver (driver) +import Proof.Cache.Functional.Invariant (srvInvAt) +import Proof.Cache.SMT.Raw (RawData (..)) +import Proof.SMT.Array (MemArr) +import Types (Address, Word) +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- | Memories a coherent cache can be built from. A class, as memory's +-- operations are ('MemOps'), so that the obligations stay polymorphic in memory +-- and the solver only meets the monomorphic 'mkDataMem'. +class (MemOps m) => CoherentOps m where + -- | The data array of a coherent cache with tags @t@ in front of @mem@: a + -- valid line holds memory's words at the address its tag gives, an invalid + -- line the words of @raw@. + mkData :: m -> TagArr -> RawData -> DataArr + +instance CoherentOps MemArr where + mkData :: MemArr -> TagArr -> RawData -> DataArr + mkData = mkDataMem + +-- | 'mkData' on the solver's memory. The solver does not run this body: +-- 'Proof.Cache.SMT.Axioms.coherentAxioms' replaces it by +-- 'Proof.Cache.SMT.Coherent.mkDataC'. +{-# OPAQUE mkDataMem #-} +mkDataMem :: MemArr -> TagArr -> RawData -> DataArr +mkDataMem mem t (RawData raw) = DataArr (imap word raw) + where + word :: Index 1024 -> Word -> Word + word i w + | entryValid e = memReadWord (wordAddr (entryTag e) si wi 0) mem + | otherwise = w + where + idx = fromIntegral i :: BitVector 10 + si = slice d9 d2 idx + wi = slice d1 d0 idx + e = tagRead si t + +-- | The base case: the server at start, in front of any memory, satisfies the +-- invariant against that memory. +baseCase :: + (MemOps m) => Address -> SetIdx -> WordIdx -> m -> Bool +baseCase wa wsi wwi mem = + srvInvAt wa wsi wwi mem (initCacheSrv mem) + +-- | The one-cycle hop: a request the cache answers at once. +indStep0 :: + (CoherentOps m) => Address -> SetIdx -> WordIdx -> m -> TagArr -> RawData -> Request -> Bool +indStep0 wa wsi wwi mem t raw req = + not premises || conclusion + where + ideal = mem + srv = CacheSrv (Cache4K t (mkData mem t raw)) mem CacheSrvReady + + (ideal', idealAns) = idealServe ideal req + + premises = + srvInvAt wa wsi wwi ideal srv + && driver srv req == 0 + + conclusion = conclusionN 0 wa wsi wwi ideal' idealAns srv req + +-- | The hop of a read that misses one line: 'penalty' + 1 cycle. +indStep4 :: + (CoherentOps m) => Address -> SetIdx -> WordIdx -> m -> TagArr -> RawData -> Request -> Bool +indStep4 wa wsi wwi mem t raw req = + not premises || conclusion + where + ideal = mem + srv = CacheSrv (Cache4K t (mkData mem t raw)) mem CacheSrvReady + + (ideal', idealAns) = idealServe ideal req + + premises = + srvInvAt wa wsi wwi ideal srv + && driver srv req == penalty + + conclusion = conclusionN penalty wa wsi wwi ideal' idealAns srv req + +-- | The hop of a read that misses both its lines: 2 * 'penalty' + 1 cycle. +indStep8 :: + (CoherentOps m) => Address -> SetIdx -> WordIdx -> m -> TagArr -> RawData -> Request -> Bool +indStep8 wa wsi wwi mem t raw req = + not premises || conclusion + where + ideal = mem + srv = CacheSrv (Cache4K t (mkData mem t raw)) mem CacheSrvReady + + (ideal', idealAns) = idealServe ideal req + + premises = + srvInvAt wa wsi wwi ideal srv + && driver srv req == 2 * penalty + + conclusion = conclusionN (2 * penalty) wa wsi wwi ideal' idealAns srv req + +-- | The conclusion of a hop of @n@ + 1 cycles: serve the request, then @n@ +-- cycles without one. A stalling server ignores its requests, so this covers +-- any requests in those cycles. The first @n@ +-- answers are 'Nothing', the last is ideal memory's answer @idealAns@, and after it +-- the server satisfies the invariant against @ideal'@, the memory ideal memory +-- stepped to. Recursive on @n@, which each obligation fixes to a constant. +conclusionN :: (MemOps m) => Cycles -> Address -> SetIdx -> WordIdx -> m -> Input -> CacheSrv m -> Request -> Bool +conclusionN n wa wsi wwi ideal' idealAns srv req + | n == 0 = ans == idealAns && srvInvAt wa wsi wwi ideal' srv' + | otherwise = + ans == Input Nothing && conclusionN (n - 1) wa wsi wwi ideal' idealAns srv' Nothing + where (srv', ans) = serve srv req diff --git a/proof/Proof/Cache/Functional/Solver.hs b/proof/Proof/Cache/Functional/Solver.hs new file mode 100644 index 0000000..d136a5a --- /dev/null +++ b/proof/Proof/Cache/Functional/Solver.hs @@ -0,0 +1,180 @@ +-- | The cache's functional proof, checked symbolically: the cache's counterpart +-- of "Proof.Core.Functional.Solver". +-- +-- 'baseCase' plus one property per hop length: on a hop of that length, the +-- corresponding obligation in "Proof.Cache.Functional.Obligation" holds. The +-- statements live there; this module only instantiates them, over every tag +-- array, data array, memory, request and witness. +-- +-- Each step starts from a ready server whose cache is coherent by +-- construction ('mkData'). +-- +-- == Running them +-- +-- Under Bitwuzla, not Z3: +-- +-- > SBV_Z3=/usr/local/bin/bitwuzla SBV_Z3_OPTIONS="--produce-models" stack build +module Proof.Cache.Functional.Solver + ( cacheArraysP, + coherentDataP, + coherentWriteP, + coherentLayoutP, + baseCaseP, + indStep0P, + indStep4P, + indStep8P, + readyUnderInvP, + readyIdleNoWaitP, + waitsAfterRequestP, + results, + ) +where + +import Clash.Prelude (BitVector, d0, d1, d2, d9, not, slice, (++#), (||)) +import Core (Request) +import qualified Core +import Memory.Cache4KServer (CacheSrv (..), CacheSrvState) +import Memory.Cache4K +import Memory.Types (MemOps (..)) +import Pantomime (Theory (..)) +import qualified Pantomime.BuiltIn as Pantomime +import Proof.Cache.SMT.Axioms (cacheAxioms, coherentAxioms) +import Proof.Cache.SMT.Raw (RawData, rawRead) +import Proof.Cache.Functional.Contract (readyIdleNoWait, readyUnderInv, waitsAfterRequest) +import Proof.Cache.Functional.Obligation +import Proof.Core.Functional.Machine (SysG (..)) +import Proof.Core.Functional.System (KState, sysOf) +import Proof.SMT.Array (MemArr, RegArr) +import Proof.SMT.Axioms (arrayAxioms) +import Proof.SMT.Logged (pantomime) +import Types +import Prelude hiding (Word, not, (||)) + +-- Sanity probes for the trusted embeddings ------------------------------------- + +-- | The tag and data array embeddings, which are trusted, against facts a +-- broken one would get wrong. +{-# ANN cacheArraysP (Theory cacheAxioms) #-} +cacheArraysP :: + TagArr -> DataArr -> SetIdx -> BitVector 21 -> BitVector 10 -> Word -> Pantomime.Bool +cacheArraysP t d s e i w = + Pantomime.boolean $ + tagRead s (tagWrite s e t) == e + && dataRead i (dataWrite i w d) == w + && tagRead s tagEmpty == 0 + && dataRead i dataZero == 0 + +-- | The embedding of the coherent cache ('mkData' as +-- 'Proof.Cache.SMT.Coherent.DataC'), which is trusted, against what 'mkData' +-- defines: a read of the constructed array is memory's word if the line is +-- valid, else the raw word. Writes are checked by 'coherentWrite'. +{-# ANN coherentDataP (Theory coherentAxioms) #-} +coherentDataP :: MemArr -> TagArr -> RawData -> BitVector 10 -> Pantomime.Bool +coherentDataP ma t raw i = + Pantomime.boolean $ dataRead i (mkData ma t raw) == constructed i + where + constructed k + | entryValid e = memReadWord (wordAddr (entryTag e) si (slice d1 d0 k) 0) ma + | otherwise = rawRead k raw + where + si = slice d9 d2 k + e = tagRead si t + +-- | A write on any data array of the coherent cache's embedding, including one +-- that already holds writes: a read after it gives the written word at its +-- index and leaves the other slots as they were. Since it holds for every +-- array, it covers any sequence of writes. +{-# ANN coherentWriteP (Theory coherentAxioms) #-} +coherentWriteP :: DataArr -> BitVector 10 -> BitVector 10 -> Word -> Pantomime.Bool +coherentWriteP d i j w = + Pantomime.boolean $ + dataRead i (dataWrite i w d) == w + && (i == j || dataRead j (dataWrite i w d) == dataRead j d) + +-- | The coherent cache's index layout agrees with the cache's addressing: at +-- any address whose line is valid and holds its block, the cache's word (index +-- set, then word, as 'Memory.Cache4K' composes it) is memory's word there. +{-# ANN coherentLayoutP (Theory coherentAxioms) #-} +coherentLayoutP :: MemArr -> TagArr -> RawData -> Address -> Pantomime.Bool +coherentLayoutP ma t raw a = + Pantomime.boolean $ + not (entryValid e && entryTag e == tagOf a) + || dataRead (setOf a ++# wordOf a) (mkData ma t raw) + == memReadWord (wordAddr (tagOf a) (setOf a) (wordOf a) 0) ma + where + e = tagRead (setOf a) t + +-- The base case ---------------------------------------------------------------- + +-- | Under 'cacheAxioms': the initial cache is the empty one ('Memory.Cache4K.dataZero'), +-- not a constructed one. +{-# ANN baseCaseP (Theory cacheAxioms) #-} +baseCaseP :: + Address -> SetIdx -> WordIdx -> MemArr -> Pantomime.Bool +baseCaseP wa wsi wwi ma = + Pantomime.boolean $ baseCase wa wsi wwi ma + +-- The inductive steps ---------------------------------------------------------- + +-- | The one-cycle hop: a request the cache answers at once. +{-# ANN indStep0P (Theory coherentAxioms) #-} +indStep0P :: + Address -> SetIdx -> WordIdx -> MemArr -> TagArr -> RawData -> Request -> Pantomime.Bool +indStep0P wa wsi wwi ma t raw req = + Pantomime.boolean $ indStep0 wa wsi wwi ma t raw req + +-- | The hop of a read that misses one line. +{-# ANN indStep4P (Theory coherentAxioms) #-} +indStep4P :: + Address -> SetIdx -> WordIdx -> MemArr -> TagArr -> RawData -> Request -> Pantomime.Bool +indStep4P wa wsi wwi ma t raw req = + Pantomime.boolean $ indStep4 wa wsi wwi ma t raw req + +-- | The hop of a read that misses both its lines. +{-# ANN indStep8P (Theory coherentAxioms) #-} +indStep8P :: + Address -> SetIdx -> WordIdx -> MemArr -> TagArr -> RawData -> Request -> Pantomime.Bool +indStep8P wa wsi wwi ma t raw req = + Pantomime.boolean $ indStep8 wa wsi wwi ma t raw req + +-- The contract ----------------------------------------------------------------- +-- +-- The properties of "Proof.Cache.Functional.Contract": the cache's over a +-- server with arbitrary tags, data, memory and state, the core's over a core +-- state built from symbolic parts as in the core's proof +-- ('Proof.Core.Functional.System.sysOf'). + +-- | A server related to ideal memory by the invariant is ready. +{-# ANN readyUnderInvP (Theory cacheAxioms) #-} +readyUnderInvP :: + Address -> SetIdx -> WordIdx -> MemArr -> TagArr -> DataArr -> MemArr -> CacheSrvState -> Pantomime.Bool +readyUnderInvP wa wsi wwi ideal t d ma st = + Pantomime.boolean $ readyUnderInv wa wsi wwi ideal (CacheSrv (Cache4K t d) ma st) + +-- | A ready server that is asked nothing answers within the cycle. +{-# ANN readyIdleNoWaitP (Theory cacheAxioms) #-} +readyIdleNoWaitP :: TagArr -> DataArr -> MemArr -> CacheSrvState -> Pantomime.Bool +readyIdleNoWaitP t d ma st = Pantomime.boolean $ readyIdleNoWait (CacheSrv (Cache4K t d) ma st) + +-- | The core waits for what it asked for. +{-# ANN waitsAfterRequestP (Theory arrayAxioms) #-} +waitsAfterRequestP :: RegIdx -> KState -> Core.Input -> RegArr -> MemArr -> Pantomime.Bool +waitsAfterRequestP wr ss i ra ma = + Pantomime.boolean $ waitsAfterRequest wr (sysCore (sysOf ss i ra ma)) i + +-- | The verdicts, spliced in by the plugin at compile time: 'Nothing' when the +-- property is valid. +results :: [(String, Maybe String)] +results = + [ ("cacheArraysP", $(pantomime 'cacheArraysP)), + ("coherentDataP", $(pantomime 'coherentDataP)), + ("coherentWriteP", $(pantomime 'coherentWriteP)), + ("coherentLayoutP", $(pantomime 'coherentLayoutP)), + ("baseCaseP", $(pantomime 'baseCaseP)), + ("indStep0P", $(pantomime 'indStep0P)), + ("indStep4P", $(pantomime 'indStep4P)), + ("indStep8P", $(pantomime 'indStep8P)), + ("readyUnderInvP", $(pantomime 'readyUnderInvP)), + ("readyIdleNoWaitP", $(pantomime 'readyIdleNoWaitP)), + ("waitsAfterRequestP", $(pantomime 'waitsAfterRequestP)) + ] diff --git a/proof/Proof/Cache/Induction4K.hs b/proof/Proof/Cache/Induction4K.hs new file mode 100644 index 0000000..00806e6 --- /dev/null +++ b/proof/Proof/Cache/Induction4K.hs @@ -0,0 +1,52 @@ +-- | The server proof for the 4 KiB cache ("Proof.Cache.Server4K"), checked +-- symbolically, over every tag array, data array, memory and request, with the +-- witnesses quantified. The array embeddings are checked in +-- 'Proof.Cache.Server.Functional.Induction.cacheArrays'. +module Proof.Cache.Induction4K + ( srvInitP, + srvRefineP, + srvLeakP, + stallsOnReadsP, + results, + ) +where + +import qualified Core +import Data.Functor.Identity +import Memory.Cache4K +import Pantomime (Theory (..)) +import qualified Pantomime.BuiltIn as Pantomime +import Proof.Cache.Server4K (srvInit, srvLeak, srvRefine, stallsOnReads) +import Memory.Cache4KServer (CacheSrv (..)) +import Proof.SMT.Array (MemArr) +import Proof.Cache.SMT.Axioms (cacheAxioms) +import Proof.SMT.Logged (pantomime) +import Clash.Prelude (BitVector) +import Types +import Prelude hiding (Word) + +{-# ANN srvInitP (Theory cacheAxioms) #-} +srvInitP :: SetIdx -> WordIdx -> MemArr -> Pantomime.Bool +srvInitP s w ma = Pantomime.boolean $ srvInit s w ma + +{-# ANN srvRefineP (Theory cacheAxioms) #-} +srvRefineP :: Address -> SetIdx -> WordIdx -> TagArr -> DataArr -> MemArr -> Maybe (Core.MemAccess Identity) -> Pantomime.Bool +srvRefineP wa ws ww t d ma q = Pantomime.boolean $ srvRefine wa ws ww (CacheSrv (Cache4K t d) Nothing ma) q + +{-# ANN srvLeakP (Theory cacheAxioms) #-} +srvLeakP :: SetIdx -> TagArr -> DataArr -> MemArr -> Maybe (Core.MemAccess Identity) -> Pantomime.Bool +srvLeakP ws t d ma q = Pantomime.boolean $ srvLeak ws (CacheSrv (Cache4K t d) Nothing ma) q + +{-# ANN stallsOnReadsP (Theory cacheAxioms) #-} +stallsOnReadsP :: TagArr -> DataArr -> MemArr -> Maybe (Core.MemAccess Identity) -> Pantomime.Bool +stallsOnReadsP t d ma q = Pantomime.boolean $ stallsOnReads (CacheSrv (Cache4K t d) Nothing ma) q + +-- | The verdicts, spliced in by the plugin at compile time: 'Nothing' when the +-- property is valid. +results :: [(String, Maybe String)] +results = + [ ("srvInitP", $(pantomime 'srvInitP)), + ("srvRefineP", $(pantomime 'srvRefineP)), + ("srvLeakP", $(pantomime 'srvLeakP)), + ("stallsOnReadsP", $(pantomime 'stallsOnReadsP)) + ] diff --git a/proof/Proof/Cache/SMT/Array.hs b/proof/Proof/Cache/SMT/Array.hs new file mode 100644 index 0000000..8391abe --- /dev/null +++ b/proof/Proof/Cache/SMT/Array.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE KindSignatures #-} + +-- | The arrays of "Memory.Cache4K" embedded as SMT arrays, as "Proof.SMT.Array" +-- embeds the register file and memory: a monomorphic SMT newtype per array, and +-- an embedding per wrapper, which the term axioms in "Proof.Cache.SMT.Axioms" +-- put in place of the wrapper. +module Proof.Cache.SMT.Array + ( TagArrSMT (..), + tagReadE, + tagWriteE, + tagEmptyE, + DataArrSMT (..), + dataReadE, + dataWriteE, + dataZeroE, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Data.Coerce (Coercible, coerce) +import qualified Pantomime.BuiltIn as P +import qualified Pantomime.Clash as Clash +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- | 'Memory.Cache4K.TagArr' on the SMT side. +newtype TagArrSMT = TagArrSMT (P.Array (P.BitVec 8) (P.BitVec 21)) + +tagReadE :: + forall arr (bvI :: Nat -> Type) (bvV :: Nat -> Type). + (Coercible TagArrSMT arr) => + (Coercible Clash.BitVec bvI) => + (Coercible Clash.BitVec bvV) => + bvI 8 -> + arr -> + bvV 21 +tagReadE = coerce go + where + go :: Clash.BitVec 8 -> TagArrSMT -> Clash.BitVec 21 + go (Clash.BitVecP k) (TagArrSMT arr) = Clash.BitVecP (P.aselect arr k) + +tagWriteE :: + forall arr (bvI :: Nat -> Type) (bvV :: Nat -> Type). + (Coercible TagArrSMT arr) => + (Coercible Clash.BitVec bvI) => + (Coercible Clash.BitVec bvV) => + bvI 8 -> + bvV 21 -> + arr -> + arr +tagWriteE = coerce go + where + go :: Clash.BitVec 8 -> Clash.BitVec 21 -> TagArrSMT -> TagArrSMT + go (Clash.BitVecP k) (Clash.BitVecP v) (TagArrSMT arr) = TagArrSMT (P.astore arr k v) + +tagEmptyE :: forall arr. (Coercible TagArrSMT arr) => arr +tagEmptyE = coerce (TagArrSMT (P.aconst 0)) + +-- | 'Memory.Cache4K.DataArr' on the SMT side. +newtype DataArrSMT = DataArrSMT (P.Array (P.BitVec 10) (P.BitVec 32)) + +dataReadE :: + forall arr (bvI :: Nat -> Type) (bvV :: Nat -> Type). + (Coercible DataArrSMT arr) => + (Coercible Clash.BitVec bvI) => + (Coercible Clash.BitVec bvV) => + bvI 10 -> + arr -> + bvV 32 +dataReadE = coerce go + where + go :: Clash.BitVec 10 -> DataArrSMT -> Clash.BitVec 32 + go (Clash.BitVecP k) (DataArrSMT arr) = Clash.BitVecP (P.aselect arr k) + +dataWriteE :: + forall arr (bvI :: Nat -> Type) (bvV :: Nat -> Type). + (Coercible DataArrSMT arr) => + (Coercible Clash.BitVec bvI) => + (Coercible Clash.BitVec bvV) => + bvI 10 -> + bvV 32 -> + arr -> + arr +dataWriteE = coerce go + where + go :: Clash.BitVec 10 -> Clash.BitVec 32 -> DataArrSMT -> DataArrSMT + go (Clash.BitVecP k) (Clash.BitVecP v) (DataArrSMT arr) = DataArrSMT (P.astore arr k v) + +dataZeroE :: forall arr. (Coercible DataArrSMT arr) => arr +dataZeroE = coerce (DataArrSMT (P.aconst 0)) diff --git a/proof/Proof/Cache/SMT/Axioms.hs b/proof/Proof/Cache/SMT/Axioms.hs new file mode 100644 index 0000000..351d8d0 --- /dev/null +++ b/proof/Proof/Cache/SMT/Axioms.hs @@ -0,0 +1,62 @@ +-- | The axioms for the properties about "Memory.Cache4K": those of the register +-- file and memory, and the two cache arrays. In its own module for the same +-- reason as "Proof.SMT.Axioms". +module Proof.Cache.SMT.Axioms (cacheAxioms, coherentAxioms) where + +import qualified Data.Map as Map +import Memory.Cache4K (DataArr, TagArr, dataRead, dataWrite, dataZero, tagEmpty, tagRead, tagWrite) +import Pantomime (PluginAxioms (..)) +import Proof.SMT.Axioms (arrayAxioms) +import Proof.Cache.SMT.Array +import Proof.Cache.Functional.Obligation (mkDataMem) +import Proof.Cache.SMT.Coherent +import Proof.Cache.SMT.Raw + +cacheAxioms :: PluginAxioms +cacheAxioms = + arrayAxioms + <> PluginAxioms + { typeAxioms = + Map.fromList + [ (''TagArr, ''TagArrSMT), + (''DataArr, ''DataArrSMT) + ], + termAxioms = + [ ('tagRead, 'tagReadE), + ('tagWrite, 'tagWriteE), + ('tagEmpty, 'tagEmptyE), + ('dataRead, 'dataReadE), + ('dataWrite, 'dataWriteE), + ('dataZero, 'dataZeroE) + ] + } + +-- | The axioms for the cache's proof: as 'cacheAxioms', but the data array is +-- embedded as 'Proof.Cache.SMT.Coherent.DataC', so that +-- 'Proof.Cache.Functional.Obligation.mkData' builds a cache coherent by +-- construction (through its 'MemArr' instance, +-- 'Proof.Cache.Functional.Obligation.mkDataMem'). The raw-array and tag axioms +-- come first: an embedding that calls another wrapper ('dataReadC' calls +-- 'rawRead' and 'tagRead') only sees the axioms listed before its own. +coherentAxioms :: PluginAxioms +coherentAxioms = + arrayAxioms + <> PluginAxioms + { typeAxioms = + Map.fromList + [ (''TagArr, ''TagArrSMT), + (''DataArr, ''DataC), + (''RawData, ''DataArrSMT) + ], + termAxioms = + [ ('rawRead, 'dataReadE), + ('rawWrite, 'dataWriteE), + ('rawZero, 'dataZeroE), + ('tagRead, 'tagReadE), + ('tagWrite, 'tagWriteE), + ('tagEmpty, 'tagEmptyE), + ('dataRead, 'dataReadC), + ('dataWrite, 'dataWriteC), + ('mkDataMem, 'mkDataC) + ] + } diff --git a/proof/Proof/Cache/SMT/Coherent.hs b/proof/Proof/Cache/SMT/Coherent.hs new file mode 100644 index 0000000..562158b --- /dev/null +++ b/proof/Proof/Cache/SMT/Coherent.hs @@ -0,0 +1,57 @@ +-- | The SMT side of a cache that is coherent by construction +-- ('Proof.Cache.Functional.Obligation.cachedOf'): the term axioms in +-- "Proof.Cache.SMT.Axioms" ('Proof.Cache.SMT.Axioms.coherentAxioms') embed +-- 'Memory.Cache4K.DataArr' as 'DataC', which carries only arrays: +-- +-- * the words written since construction, and which slots were written; +-- * the memory and tags the construction reads from, and the raw contents. +-- +-- A read takes a written word if there is one, else memory's word if the line +-- is valid, else the raw word. Everything stays an array, so the solver can +-- share it across the cache's branches; a Haskell function in its place makes +-- the longest hop exhaust memory before the query is even built. +module Proof.Cache.SMT.Coherent + ( DataC (..), + dataReadC, + dataWriteC, + mkDataC, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Data.Coerce (Coercible, coerce) +import Memory.Cache4K +import Memory.Types (MemOps (..)) +import Proof.Cache.SMT.Raw +import Proof.SMT.Array (MemArr) +import Types (Word) +import Prelude hiding (Ordering (..), Word, init, log, not, repeat, undefined, (!!), (&&), (++), (||)) + +-- The data array ------------------------------------------------------------------ + +-- | 'Memory.Cache4K.DataArr' on the proof side: the words written since +-- construction, which slots were written (nonzero = written), and the memory, +-- tags and raw contents the construction reads from. +data DataC = DataC RawData RawData MemArr TagArr RawData + +-- | The embedding of 'Memory.Cache4K.dataRead'. +dataReadC :: forall arr. (Coercible DataC arr) => BitVector 10 -> arr -> Word +dataReadC i a + | rawRead i written /= 0 = rawRead i ws + | entryValid e = memReadWord (wordAddr (entryTag e) si (slice d1 d0 i) 0) mem + | otherwise = rawRead i raw + where + DataC ws written mem tags raw = coerce a + si = slice d9 d2 i + e = tagRead si tags + +-- | The embedding of 'Memory.Cache4K.dataWrite'. +dataWriteC :: forall arr. (Coercible DataC arr) => BitVector 10 -> Word -> arr -> arr +dataWriteC i v a = coerce (DataC (rawWrite i v ws) (rawWrite i 1 written) mem tags raw) + where + DataC ws written mem tags raw = coerce a + +-- | The embedding of 'Proof.Cache.Functional.Obligation.mkDataMem': nothing +-- written yet. +mkDataC :: forall arr. (Coercible DataC arr) => MemArr -> TagArr -> RawData -> arr +mkDataC mem t raw = coerce (DataC rawZero rawZero mem t raw) diff --git a/proof/Proof/Cache/SMT/Raw.hs b/proof/Proof/Cache/SMT/Raw.hs new file mode 100644 index 0000000..24adb26 --- /dev/null +++ b/proof/Proof/Cache/SMT/Raw.hs @@ -0,0 +1,32 @@ +-- | A raw array of 1024 words, indexed like the cache's data array: the +-- arbitrary contents of a coherent cache's invalid lines +-- ('Proof.Cache.Functional.Obligation.cachedOf'). The term axioms in +-- "Proof.Cache.SMT.Axioms" embed it as 'Proof.Cache.SMT.Array.DataArrSMT'. +-- +-- In a module of its own, without the solver's types, so that the obligations +-- can mention it and still build without the solver. +module Proof.Cache.SMT.Raw + ( RawData (..), + rawRead, + rawWrite, + rawZero, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Types (Word) +import Prelude hiding (Ordering (..), Word, init, log, not, repeat, undefined, (!!), (&&), (++), (||)) + +newtype RawData = RawData (Vec 1024 Word) + +{-# OPAQUE rawRead #-} +rawRead :: BitVector 10 -> RawData -> Word +rawRead i (RawData v) = v !! i + +{-# OPAQUE rawWrite #-} +rawWrite :: BitVector 10 -> Word -> RawData -> RawData +rawWrite i w (RawData v) = RawData (replace i w v) + +{-# OPAQUE rawZero #-} +rawZero :: RawData +rawZero = RawData (repeat 0) diff --git a/proof/Proof/Cache/Server4K.hs b/proof/Proof/Cache/Server4K.hs new file mode 100644 index 0000000..84ddbac --- /dev/null +++ b/proof/Proof/Cache/Server4K.hs @@ -0,0 +1,157 @@ +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | The server proof for the 4 KiB cache ("Memory.Cache4K"), served by +-- 'Memory.Cache4KServer.serve'. +-- +-- The artifacts: the hop of a request ('Proof.Cache.Server.Functional.Driver.driver' +-- cycles after it), +-- the invariant (no miss pending, every valid line holds memory's words), the +-- flush 'srvMem', the censor 'srvTag' (the tag array), and the simulator +-- 'simStep', derived from the cache itself. +-- +-- The cache holds 1024 words, so the invariant is stated at one word, +-- 'srvInvAt', and the obligations quantify over that word, as the functional +-- invariant does over a register and a byte. 'srvRefine' also assumes the +-- invariant at the word the request accesses. Both assumptions are instances of +-- the invariant at every word, so 'srvRefine' for every witness gives the +-- obligation for the whole invariant. +module Proof.Cache.Server4K + ( srvTag, + simStep, + simBus, + srvInit, + srvRefine, + srvLeak, + stallsOnReads, + CacheSys (..), + initCacheSys, + stepCachedOut, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Core (Input (..), MemAccess (..), Output (..), Request, circuit) +import Data.Functor.Identity +import Memory.Cache4K +import Memory.Types (MemOps (..)) +import Proof.Core.Leakage.Model (Obs (..), obsReq) +import Memory.Cache4KServer +import Proof.Cache.Server.Functional.Driver (driver) +import Proof.Cache.Server.Functional.Invariant (noMiss, srvInvAt) +import Proof.Core.Functional.Machine (SysG (..)) +import Memory.Ideal (idealServe) +import Core.RegFile (RegFileOps) +import Types +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) +import qualified Prelude as P + +-- | The censor: the tags. +srvTag :: CacheSrv m -> TagArr +srvTag y = tagArr (srvCache y) + +-- | The simulator's memory: zeros, and writes are dropped. The simulator knows +-- no data. +data NoMem = NoMem + deriving (Eq, Show) + +instance MemOps NoMem where + memReadWord _ _ = 0 + memWrite _ _ _ m = m + memReadByte _ _ = 0 + +-- | A request with a given observation: a fetch of a word, and a write of zero. +reqOf :: Obs -> Request +reqOf o = case o of + NoAccess -> Nothing + Fetch addr -> Just (MemAccess True addr Types.Word Nothing) + DataRead addr size -> Just (MemAccess False addr size Nothing) + DataWrite addr size -> Just (MemAccess False addr size (Just (Identity 0))) + +-- | The simulator: the cache's own hop, on the tags with no data, in front of +-- 'NoMem', on a request with the observation. Returns the next tags and how many +-- responses are not ready. +simStep :: TagArr -> Obs -> (TagArr, Cycles) +simStep t o = (srvTag y', k) + where + y0 = CacheSrv (Cache4K t dataZero) Nothing NoMem + q = reqOf o + n = driver y0 q + k = fromIntegral n + (y', _) = serveN n y0 q + +-- | The simulator as it shows on the bus: the observed request, then one cycle +-- without a request per response that is not ready. +simBus :: TagArr -> Obs -> (TagArr, [Obs]) +simBus t o = (t', o : P.replicate (fromIntegral k) NoAccess) + where + (t', k) = simStep t o + +sameInput :: Input Identity -> Input Identity -> Bool +sameInput a b = + runIdentity (inputMem a) == runIdentity (inputMem b) + && inputMemReady a == inputMemReady b + +-- | The empty cache, in front of any memory, satisfies the invariant. Its +-- censor is 'tagEmpty' for every memory by definition. +srvInit :: (MemOps m) => SetIdx -> WordIdx -> m -> Bool +srvInit s w mem = srvInvAt s w (CacheSrv emptyCache4K Nothing mem) + +-- | The refinement proof, at witnesses: memory at byte @wa@ and the invariant at +-- word @ww@ of set @ws@. The hop of a request ends with ideal memory's response, +-- and with memory and the invariant as ideal memory leaves them. +srvRefine :: (MemOps m) => Address -> SetIdx -> WordIdx -> CacheSrv m -> Request -> Bool +srvRefine wa ws ww y q = + not (srvInvAt ws ww y && accessed) + || ( sameInput x xI + && srvInvAt ws ww y' + && memReadByte wa (srvMem y') == memReadByte wa mI + ) + where + (y', x) = serveN (driver y q) y q + (mI, xI) = idealServe (srvMem y) q + accessed = case q of + Just (MemAccess _ addr _ _) -> srvInvAt (setOf addr) (wordOf addr) y + Nothing -> True + +-- | The leakage proof, at a witness set: with no miss pending, how many +-- responses of the hop are not ready, and the next tags, are what 'simStep' computes +-- from the tags and the observation of the request. +srvLeak :: (MemOps m) => SetIdx -> CacheSrv m -> Request -> Bool +srvLeak ws y q = + not (noMiss y) || (k == fromIntegral kS && tagRead ws (srvTag y') == tagRead ws tS) + where + k = driver y q + (y', _) = serveN k y q + (tS, kS) = simStep (srvTag y) (obsReq q) + +-- | The cache answers late only to a data read. With the core's patience +-- ('Proof.CachedCore.Obligation.waitObligation'), the core's leakage proof carries +-- over to the core behind this cache too. +stallsOnReads :: (MemOps m) => CacheSrv m -> Request -> Bool +stallsOnReads y q = not (noMiss y) || inputMemReady x || isDataRead + where + (_, x) = serve y q + isDataRead = case q of + Just (MemAccess False _ _ Nothing) -> True + _ -> False + +-- | System state paired with a cache model. +data CacheSys r m c = CacheSys + { cacheSysCore :: SysG r m, + cacheSysCache :: c, + -- | A read waiting for memory: its address and width, and the cycles left. + cacheSysPending :: Maybe (Address, Size, Cycles) + } + +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 + +-- | The core in a loop with the cache in front of memory. +stepCachedOut :: (RegFileOps r, MemOps m) => CacheSys r m Cache4K -> (CacheSys r m Cache4K, Output Identity) +stepCachedOut (CacheSys (Sys s i m) cache pending) = + let (s', o) = circuit s i + (CacheSrv cache' pending' m', i') = serve (CacheSrv cache pending m) (outMem o) + in (CacheSys (Sys s' i' m') cache' pending', o) diff --git a/proof/Proof/Functional/Driver.hs b/proof/Proof/Core/Functional/Driver.hs similarity index 65% rename from proof/Proof/Functional/Driver.hs rename to proof/Proof/Core/Functional/Driver.hs index 261a2a5..5ddf546 100644 --- a/proof/Proof/Functional/Driver.hs +++ b/proof/Proof/Core/Functional/Driver.hs @@ -1,4 +1,4 @@ --- | The driver: how many cycles 'Proof.Machine.stepSys' should advance the core +-- | The driver: how many cycles 'Proof.Core.Functional.Machine.stepSys' should advance the core -- before its state is compared against the ISA again. Its stated invariant is -- operational -- \"step until the instruction in the execute phase is no longer -- a no-op\" -- so this module provides both: @@ -13,7 +13,7 @@ -- values, which in turn depend on the register file, on the memory-stage and -- writeback-stage forwarding lines, and (for a load in writeback) on -- 'inputMem'. -module Proof.Functional.Driver +module Proof.Core.Functional.Driver ( driver, driverCaseName, driverRef, @@ -27,20 +27,20 @@ where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Core -import Data.Functor.Identity -import Instruction hiding (loadHazard, storeHazard) -import qualified Instruction +import Data.Maybe (fromMaybe) +import Core.Instruction hiding (loadHazard, storeHazard) +import qualified Core.Instruction import Memory.Types (MemOps (..)) -import Proof.Machine -import RegFile +import Proof.Core.Functional.Machine +import Core.RegFile import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) -- | @ctrlMeRegFwd@ as set by 'Core.memory'. Note that a load in the memory -- stage forwards nothing (its value is not available yet). meFwd :: SysG r m -> Maybe (RegIdx, Word) -meFwd (Sys st _ _) = - case stateMeInstr st of +meFwd (Sys core _ _) = + case stateMeInstr core of RType _ rd _ _ -> Just (rd, res) IType (Arith _) rd _ _ -> Just (rd, res) JType rd _ -> Just (rd, res) @@ -48,30 +48,30 @@ meFwd (Sys st _ _) = UType _ rd _ -> Just (rd, res) _ -> Nothing where - res = runIdentity (stateMeRes st) + res = stateMeRes core -- | @ctrlWbRegFwd@ as set by 'Core.writeback'. A load forwards the value read -- from memory on this cycle's 'inputMem', not 'stateWbRes'. wbFwd :: SysG r m -> Maybe (RegIdx, Word) -wbFwd (Sys st inp _) = - case stateWbInstr st of +wbFwd (Sys core inp _) = + case stateWbInstr core of RType _ rd _ _ -> Just (rd, res) IType (Arith _) rd _ _ -> Just (rd, res) - IType (Load size sign) rd _ _ -> Just (rd, loadExtend size sign (runIdentity (inputMem inp))) + IType (Load size sign) rd _ _ -> Just (rd, loadExtend size sign (fromMaybe 0 (inputMem inp))) JType rd _ -> Just (rd, res) IType Jump rd _ _ -> Just (rd, res) UType _ rd _ -> Just (rd, res) _ -> Nothing where - res = runIdentity (stateWbRes st) + res = stateWbRes core -- | The value 'Core.execute' reads for a source register, honouring the -- memory-then-writeback forwarding priority of 'Core.execute'. exArg :: (RegFileOps r) => SysG r m -> RegIdx -> Word -exArg sys@(Sys st _ _) idx = +exArg sys@(Sys core _ _) idx = case pick (meFwd sys) <|> pick (wbFwd sys) of Just v -> v - Nothing -> runIdentity (lookupRFg idx (stateRegFile st)) + Nothing -> lookupRFg idx (stateRegFile core) where pick m = do (fwdIdx, fwdVal) <- m @@ -80,10 +80,10 @@ exArg sys@(Sys st _ _) idx = -- | Does the execute-stage instruction take a jump this cycle? This is -- @ctrlExJumpAddr@ becoming 'Just'. takingJump :: (RegFileOps r) => SysG r m -> Bool -takingJump sys@(Sys st _ _) = - case stateExInstr st of +takingJump sys@(Sys core _ _) = + case stateExInstr core of BType cmp _ rs1 rs2 -> - runIdentity (branch cmp (pure (exArg sys rs1)) (pure (exArg sys rs2))) + (branch cmp (exArg sys rs1) (exArg sys rs2)) JType _ _ -> True IType Jump _ _ _ -> True _ -> False @@ -92,67 +92,70 @@ takingJump sys@(Sys st _ _) = -- decode-stage PC overlaps a store either in the execute stage or in the memory -- stage. -- --- The overlap test is 'Instruction.storeHazard', the core's own, which is why +-- The overlap test is 'Core.Instruction.storeHazard', the core's own, which is why -- the store's size is carried alongside its address: a byte store and a word -- store at the same address clash with different sets of PCs. 'Core.decode' -- reads the pair off @ctrlExStoreAddrSize@ / @ctrlMeStoreAddrSize@; here the -- execute-stage address is recomputed from the forwarded operand, as -- 'Core.execute' would, and the memory-stage one is already in @stateMeAddr@. storeHazard :: (RegFileOps r) => SysG r m -> Bool -storeHazard sys@(Sys st _ _) = - maybe False (Instruction.storeHazard dePc) exStore - || maybe False (Instruction.storeHazard dePc) meStore +storeHazard sys@(Sys core _ _) = + maybe False (Core.Instruction.storeHazard dePc) exStore + || maybe False (Core.Instruction.storeHazard dePc) meStore where - dePc = stateDePc st - exStore = case stateExInstr st of + dePc = stateDePc core + exStore = case stateExInstr core of SType size imm rs1 _ -> Just - ( unpack (runIdentity (alu ADD (pure (exArg sys rs1)) (pure (signExtend imm)))), + ( unpack (alu ADD (exArg sys rs1) (signExtend imm)), size ) _ -> Nothing - meStore = case stateMeInstr st of - SType size _ _ _ -> Just (stateMeAddr st, size) + 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. loadHazard :: SysG r m -> Bool -loadHazard (Sys st inp _) = - Instruction.loadHazard deIr (stateExInstr st) +loadHazard (Sys core inp _) = + Core.Instruction.loadHazard deIr (stateExInstr core) where - expInstr = stateDeExpInstr st + expInstr = stateDeExpInstr core deIr - | expInstr = decode' (runIdentity (inputMem inp)) - | otherwise = Nop MemoryBusBusy + | expInstr = maybe (Nop NoInstruction) decode' (inputMem inp) + | otherwise = Nop NoInstruction --- | The driver's case table. The cases are checked in order. +-- | The driver's case table. The cases are checked in order. The driver is +-- only ever run from states that satisfy the invariant +-- ('Proof.Core.Functional.Invariant.invAt'); elsewhere it need not agree +-- with 'driverRef'. driver :: (RegFileOps r) => SysG r m -> Int -driver sys@(Sys st _ _) - | stateExInstr st == Nop FirstCycle = 1 - | stateExInstr st == Nop Halted = 0 - | isEnvInstr (stateExInstr st) = 2 +driver sys@(Sys core _ _) + | stateExInstr core == Nop FirstCycle = 1 + | stateExInstr core == Nop Halted = 0 + | isEnvInstr (stateExInstr core) = 2 | takingJump sys = 2 - | storeHazard sys = if isMemInstr (stateExInstr st) then 3 else 2 + | storeHazard sys = if isMemInstr (stateExInstr core) then 3 else 2 | loadHazard sys = 3 - | not (isMemInstr (stateWbInstr st)) = 0 - | not (isMemInstr (stateMeInstr st)) = 1 - | not (isMemInstr (stateExInstr st)) = 2 + | not (isMemInstr (stateWbInstr core)) = 0 + | not (isMemInstr (stateMeInstr core)) = 1 + | not (isMemInstr (stateExInstr core)) = 2 | otherwise = 3 -- | Which case of the table 'driver' fired. Used to measure how much of the -- table the tests actually reach. driverCaseName :: (RegFileOps r) => SysG r m -> String -driverCaseName sys@(Sys st _ _) - | stateExInstr st == Nop FirstCycle = "firstCycle" - | stateExInstr st == Nop Halted = "halted" - | isEnvInstr (stateExInstr st) = "env" +driverCaseName sys@(Sys core _ _) + | stateExInstr core == Nop FirstCycle = "firstCycle" + | stateExInstr core == Nop Halted = "halted" + | isEnvInstr (stateExInstr core) = "env" | takingJump sys = "jump" - | storeHazard sys = if isMemInstr (stateExInstr st) then "storeHazard/mem" else "storeHazard/nomem" + | storeHazard sys = if isMemInstr (stateExInstr core) then "storeHazard/mem" else "storeHazard/nomem" | loadHazard sys = "loadHazard" - | not (isMemInstr (stateWbInstr st)) = "steady/wb-nomem" - | not (isMemInstr (stateMeInstr st)) = "steady/me-nomem" - | not (isMemInstr (stateExInstr st)) = "steady/ex-nomem" + | not (isMemInstr (stateWbInstr core)) = "steady/wb-nomem" + | not (isMemInstr (stateMeInstr core)) = "steady/me-nomem" + | not (isMemInstr (stateExInstr core)) = "steady/ex-nomem" | otherwise = "steady/all-mem" -- | Is this a pipeline bubble, as opposed to a real instruction? @@ -169,7 +172,7 @@ isBubble _ = 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.Machine.stepSys' steps taken, or 'Nothing' if @fuel@ ran out (which is what +-- 'Proof.Core.Functional.Machine.stepSys' steps taken, or 'Nothing' if @fuel@ ran out (which is what -- happens once the core has halted, since the execute stage then holds -- @Nop Halted@ forever). -- @@ -179,7 +182,7 @@ isBubble _ = False driverRef :: (RegFileOps r, MemOps m) => Int -> SysG r m -> Maybe Int driverRef fuel sys0 = go 1 (stepSys sys0) where - go n s@(Sys st _ _) - | not (isBubble (stateExInstr st)) = Just n + go n s@(Sys core _ _) + | not (isBubble (stateExInstr core)) = Just n | n >= fuel = Nothing | otherwise = go (n + 1) (stepSys s) diff --git a/proof/Proof/Functional/Invariant.hs b/proof/Proof/Core/Functional/Invariant.hs similarity index 65% rename from proof/Proof/Functional/Invariant.hs rename to proof/Proof/Core/Functional/Invariant.hs index c496d35..123f834 100644 --- a/proof/Proof/Functional/Invariant.hs +++ b/proof/Proof/Core/Functional/Invariant.hs @@ -4,41 +4,45 @@ -- The invariant relates an architectural state @(isaPc, isaRegFile, isaMem)@ to -- a system state @((core state), (input), mem)@. It is a disjunction of cases: -- one for the running core, and two for the halted core. The reset state is --- not among them: 'Proof.Functional.Induction.baseCase' steps it two cycles, +-- not among them: 'Proof.Core.Functional.Solver.baseCase' steps it two cycles, -- into the running case, instead. -- -- Two forms of the same predicate live here: -- -- * 'invCases' represents each case as a named list of conjuncts, so a -- failing QuickCheck run can report which clause broke ('explain'); --- * 'invAtFree' is the identical predicate built from '&&' and '||' with no +-- * 'invAt' is the identical predicate built from '&&' and '||' with no -- lists, because Pantomime's evaluator diverges on recursion it cannot -- prove terminating -- even over a fully concrete list. Symbolic execution -- uses this one. -- -- The test \"fold-free invariant agrees with the list version\" keeps the two -- from drifting. -module Proof.Functional.Invariant +-- +-- The invariant describes the core attached to memory that answers every +-- request in the next cycle ('Proof.Core.Functional.Machine.stepSys'), so the bus always holds +-- an answer ('Core.inputMem' is 'Just'). +module Proof.Core.Functional.Invariant ( flushWbStage, flushMeStage, Case (..), inv, - invAt, + invAtList, invCases, invCasesAt, - invAtFree, + invAt, explain, ) where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Core -import Data.Functor.Identity -import Instruction +import Data.Maybe (fromMaybe, isJust) +import Core.Instruction import Memory.Types -import ISA (IsaStateG (..), IsaState) -import Proof.Machine -import RegFile +import Core.ISA (IsaStateG (..), IsaState) +import Proof.Core.Functional.Machine +import Core.RegFile import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) import qualified Prelude as P @@ -50,8 +54,8 @@ flushWbStage :: Instruction -> Word -> Word -> - (m, r Identity) -> - (m, r Identity) + (m, r) -> + (m, r) flushWbStage ir res inputWord (mem, rf) = case ir of RType _ rd _ _ -> (mem, put rd res) @@ -65,7 +69,7 @@ flushWbStage ir res inputWord (mem, rf) = IType (Env _) _ _ _ -> (mem, rf) Nop _ -> (mem, rf) where - put rd v = modifyRFg rd (pure v) rf + put rd v = modifyRFg rd v rf -- | Apply the pending effect of the memory-stage instruction. -- @@ -77,15 +81,15 @@ flushMeStage :: Instruction -> Word -> Address -> - (m, r Identity) -> - (m, r Identity) + (m, r) -> + (m, r) flushMeStage ir res addr (mem, rf) = case ir of RType _ rd _ _ -> (mem, put rd res) IType (Arith _) rd _ _ -> (mem, put rd res) IType (Load size sign) rd _ _ -> (mem, put rd (loadExtend size sign (memReadWord addr mem))) - SType size _ _ _ -> (memWriteWord size addr res mem, rf) + SType size _ _ _ -> (memWrite addr size res mem, rf) BType {} -> (mem, rf) JType rd _ -> (mem, put rd res) IType Jump rd _ _ -> (mem, put rd res) @@ -93,7 +97,7 @@ flushMeStage ir res addr (mem, rf) = IType (Env _) _ _ _ -> (mem, rf) Nop _ -> (mem, rf) where - put rd v = modifyRFg rd (pure v) rf + put rd v = modifyRFg rd v rf -- | A named case of the invariant, with its conjuncts. data Case = Case @@ -111,11 +115,13 @@ inv isa sys = P.any holds (invCases isa sys) -- | The invariant in pointwise form: instead of comparing whole register files -- and memories, compare them at one witness register @wr@ and one witness byte -- address @wa@. Quantifying over the witnesses recovers the container form. +-- Pointwise, because function-backed containers have no decidable equality but +-- can be read at a symbolic point. -- --- This is the version symbolic execution can use: function-backed containers --- have no decidable equality, but they can be read at a symbolic point. -invAt :: (RegFileOps r, MemOps m) => RegIdx -> Address -> IsaStateG r m -> SysG r m -> Bool -invAt wr wa isa sys = P.any holds (invCasesAt wr wa isa sys) +-- Built from the named cases ('invCasesAt'), for the tests; the proofs use the +-- fold-free 'invAt', which the tests check agrees with it. +invAtList :: (RegFileOps r, MemOps m) => RegIdx -> Address -> IsaStateG r m -> SysG r m -> Bool +invAtList wr wa isa sys = P.any holds (invCasesAt wr wa isa sys) -- | Human-readable account of why the invariant failed: for each case, the -- conjuncts that were false. @@ -136,7 +142,7 @@ invCasesAt :: RegIdx -> Address -> IsaStateG r m -> SysG r m -> [Case] invCasesAt wr wa = invCasesGen - (\a b -> runIdentity (lookupRFg wr a) == runIdentity (lookupRFg wr b)) + (\a b -> lookupRFg wr a == lookupRFg wr b) (\a b -> memReadByte wa a == memReadByte wa b) -- | The cases of the invariant, parameterised over how register files and @@ -147,24 +153,24 @@ invCasesAt wr wa = -- reads them. invCasesGen :: (RegFileOps r, MemOps m) => - (r Identity -> r Identity -> Bool) -> + (r -> r -> Bool) -> (m -> m -> Bool) -> IsaStateG r m -> SysG r m -> [Case] -invCasesGen eqRF eqMem (IsaState ipc irf imem) (Sys st inp mem) = +invCasesGen eqRF eqMem (IsaState ipc irf imem) (Sys core inp mem) = [ runningCase, haltedCase "halted/ebreak" isBreak (EBreak (ipc + 4)), haltedCase "halted/ecall" isCall (Syscall (ipc + 4)) ] where - inputWord = runIdentity (inputMem inp) + inputWord = fromMaybe 0 (inputMem inp) -- Bound once: under symbolic execution a repeated 'decode'' is not shared, -- and it is a large decision tree. isaInstr = decode' (memReadWord ipc imem) - dePcWord = memReadWord (stateDePc st) mem + dePcWord = memReadWord (stateDePc core) mem -- The note's four running cases, collapsed. -- @@ -178,47 +184,49 @@ invCasesGen eqRF eqMem (IsaState ipc irf imem) (Sys st inp mem) = -- therefore stated directly as \"not an environment instruction\". runningCase = Case "running" $ - [ ("running", stateHalt st == Nothing), - ("wb is not an env instruction", P.not (isEnvInstr (stateWbInstr st))), - ("me is not an env instruction", P.not (isEnvInstr (stateMeInstr st))), - ("exPc == isaPc", stateExPc st == ipc), - ("ex == decode (mem[isaPc])", stateExInstr st == isaInstr), - ("dePc == exPc + 4", stateDePc st == stateExPc st + 4), - ("no load-use hazard me->ex", P.not (loadHazard (stateExInstr st) (stateMeInstr st))), + [ ("running", stateHalt core == Nothing), + ("memory answered", isJust (inputMem inp)), + ("wb is not an env instruction", P.not (isEnvInstr (stateWbInstr core))), + ("me is not an env instruction", P.not (isEnvInstr (stateMeInstr core))), + ("exPc == isaPc", stateExPc core == ipc), + ("ex == decode (mem[isaPc])", stateExInstr core == isaInstr), + ("dePc == exPc + 4", stateDePc core == stateExPc core + 4), + ("no load-use hazard me->ex", P.not (loadHazard (stateExInstr core) (stateMeInstr core))), ( "(isaMem, isaRegFile) == flush", let (fm, frf) = flushMeStage - (stateMeInstr st) - (runIdentity (stateMeRes st)) - (stateMeAddr st) - (flushWbStage (stateWbInstr st) (runIdentity (stateWbRes st)) inputWord (mem, stateRegFile st)) + (stateMeInstr core) + (stateMeRes core) + (stateMeAddr core) + (flushWbStage (stateWbInstr core) (stateWbRes core) inputWord (mem, stateRegFile core)) in eqMem imem fm && eqRF irf frf ) ] - P.++ if isMemInstr (stateWbInstr st) + P.++ if isMemInstr (stateWbInstr core) then - [ ("not deExpInstr", P.not (stateDeExpInstr st)), - ("fePc == exPc + 4", stateFePc st == stateExPc st + 4) + [ ("not deExpInstr", P.not (stateDeExpInstr core)), + ("fePc == exPc + 4", stateFePc core == stateExPc core + 4) ] else - [ ("deExpInstr", stateDeExpInstr st), + [ ("deExpInstr", stateDeExpInstr core), ("inputMem == mem[dePc]", inputWord == dePcWord), - ("fePc == exPc + 8", stateFePc st == stateExPc st + 8) + ("fePc == exPc + 8", stateFePc core == stateExPc core + 8) ] -- The halt carries the address the core would resume at, which 'Core.execute' -- set from the trapping instruction's own PC. Pinning it to @isaPc + 4@ is - -- what fixes @isaPc@ as that instruction's address; "ISA" leaves + -- what fixes @isaPc@ as that instruction's address; "Core.ISA" leaves -- the architectural state where it was, so the ISA is still \"at\" the trap. haltedCase name isKind expected = Case name [ ("isa instruction is of this kind", isKind isaInstr), - ("halt state matches", stateHalt st == Just expected), - ("wb == Nop Halted", stateWbInstr st == Nop Halted), - ("me == Nop Halted", stateMeInstr st == Nop Halted), - ("ex == Nop Halted", stateExInstr st == Nop Halted), - ("isaRegFile == stateRegFile", eqRF irf (stateRegFile st)), + ("halt state matches", stateHalt core == Just expected), + ("wb == Nop Halted", stateWbInstr core == Nop Halted), + ("memory answered", isJust (inputMem inp)), + ("me == Nop Halted", stateMeInstr core == Nop Halted), + ("ex == Nop Halted", stateExInstr core == Nop Halted), + ("isaRegFile == stateRegFile", eqRF irf (stateRegFile core)), ("isaMem == stateMem", eqMem imem mem) ] @@ -227,14 +235,14 @@ invCasesGen eqRF eqMem (IsaState ipc irf imem) (Sys st inp mem) = -- | The invariant, pointwise, built from '&&' and '||' with no lists and no -- folds. Semantically identical to @'P.any' holds ('invCasesAt' wr wa)@; see -- the module header for why both exist. -invAtFree :: +invAt :: (RegFileOps r, MemOps m) => RegIdx -> Address -> IsaStateG r m -> SysG r m -> Bool -invAtFree wr wa isa sys = +invAt wr wa isa sys = runningCaseAt wr wa isa sys || haltedCaseAt HaltBreak wr wa isa sys || haltedCaseAt HaltCall wr wa isa sys @@ -246,53 +254,55 @@ data HaltKind = HaltBreak | HaltCall runningCaseAt :: (RegFileOps r, MemOps m) => RegIdx -> Address -> IsaStateG r m -> SysG r m -> Bool -runningCaseAt wr wa (IsaState ipc irf imem) (Sys st inp mem) = - stateHalt st == Nothing - && not (isEnvInstr (stateWbInstr st)) - && not (isEnvInstr (stateMeInstr st)) - && stateExPc st == ipc - && stateExInstr st == decode' (memReadWord ipc imem) - && stateDePc st == stateExPc st + 4 - && not (loadHazard (stateExInstr st) (stateMeInstr st)) - && ( if isMemInstr (stateWbInstr st) - then not (stateDeExpInstr st) && stateFePc st == stateExPc st + 4 +runningCaseAt wr wa (IsaState ipc irf imem) (Sys core inp mem) = + stateHalt core == Nothing + && isJust (inputMem inp) + && not (isEnvInstr (stateWbInstr core)) + && not (isEnvInstr (stateMeInstr core)) + && stateExPc core == ipc + && stateExInstr core == decode' (memReadWord ipc imem) + && stateDePc core == stateExPc core + 4 + && not (loadHazard (stateExInstr core) (stateMeInstr core)) + && ( if isMemInstr (stateWbInstr core) + then not (stateDeExpInstr core) && stateFePc core == stateExPc core + 4 else - stateDeExpInstr st - && runIdentity (inputMem inp) == memReadWord (stateDePc st) mem - && stateFePc st == stateExPc st + 8 + stateDeExpInstr core + && inputMem inp == Just (memReadWord (stateDePc core) mem) + && stateFePc core == stateExPc core + 8 ) && memReadByte wa imem == memReadByte wa fm - && runIdentity (lookupRFg wr irf) == runIdentity (lookupRFg wr frf) + && lookupRFg wr irf == lookupRFg wr frf where -- The same flush the container form applies, read at the witness. Writing - -- it out pointwise by hand would duplicate 'flushMeStage' and 'memWriteWord' - -- for no gain: 'Proof.Functional.Obligation.isaAt' already puts this flush + -- it out pointwise by hand would duplicate 'flushMeStage' and 'memWrite' + -- for no gain: 'Proof.Core.Functional.Obligation.isaAt' already puts this flush -- into every query, and the solver rewrites @select@ over a @store@ chain -- natively. (fm, frf) = flushMeStage - (stateMeInstr st) - (runIdentity (stateMeRes st)) - (stateMeAddr st) + (stateMeInstr core) + (stateMeRes core) + (stateMeAddr core) ( flushWbStage - (stateWbInstr st) - (runIdentity (stateWbRes st)) - (runIdentity (inputMem inp)) - (mem, stateRegFile st) + (stateWbInstr core) + (stateWbRes core) + (fromMaybe 0 (inputMem inp)) + (mem, stateRegFile core) ) -- | One halted case. haltedCaseAt :: (RegFileOps r, MemOps m) => HaltKind -> RegIdx -> Address -> IsaStateG r m -> SysG r m -> Bool -haltedCaseAt kind wr wa (IsaState ipc irf imem) (Sys st _ mem) = +haltedCaseAt kind wr wa (IsaState ipc irf imem) (Sys core inp mem) = isKind (decode' (memReadWord ipc imem)) - && stateHalt st == Just expected - && stateWbInstr st == Nop Halted - && stateMeInstr st == Nop Halted - && stateExInstr st == Nop Halted + && stateHalt core == Just expected + && stateWbInstr core == Nop Halted + && isJust (inputMem inp) + && stateMeInstr core == Nop Halted + && stateExInstr core == Nop Halted && memReadByte wa imem == memReadByte wa mem - && runIdentity (lookupRFg wr irf) == runIdentity (lookupRFg wr (stateRegFile st)) + && lookupRFg wr irf == lookupRFg wr (stateRegFile core) where isKind = case kind of HaltBreak -> isBreak diff --git a/proof/Proof/Core/Functional/Machine.hs b/proof/Proof/Core/Functional/Machine.hs new file mode 100644 index 0000000..50bfa25 --- /dev/null +++ b/proof/Proof/Core/Functional/Machine.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | The system the core's proofs reason about: the core together with ideal +-- memory. +-- +-- 'Core.circuit' is only the pipeline: memory lives outside it. The core emits +-- a 'MemAccess' on its 'Output' and receives the response on the next 'Input'. +-- So a single system step is one 'Core.circuit' step plus ideal memory's answer +-- ('idealServe'), and the state the proofs reason about is the triple +-- +-- > (Core.State, Input, memory) +module Proof.Core.Functional.Machine + ( SysG (..), + Sys, + stepSys, + stepSysOut, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Core +import Memory.Types +import Memory.Ideal (idealServe) +import Core.RegFile +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- | Core state, the input it is about to consume, and memory. +data SysG r m = Sys + { sysCore :: Core.StateG r, + sysInput :: Input, + sysMem :: m + } + +-- | The concrete system the QuickCheck harness runs: @Vec@-backed throughout. +type Sys = SysG RegFile MemBytes + +deriving instance (Show r, Show m) => Show (SysG r m) + +-- | Structural equality. +instance (Eq r, Eq m) => Eq (SysG r m) where + Sys s1 i1 m1 == Sys s2 i2 m2 = + s1 == s2 + && inputMem i1 == inputMem i2 + && m1 == m2 + +-- | One system step: run the pipeline for a cycle, then service whatever +-- memory access it emitted. Mirrors 'Simulate.simulator', except that a halted +-- core simply stops changing instead of ending the stream. +stepSys :: (RegFileOps r, MemOps m) => SysG r m -> SysG r m +stepSys = fst . stepSysOut + +-- | 'stepSys', but also returning the pipeline's 'Output' for that cycle. +-- +-- The leakage proof observes the cycle-by-cycle memory traffic, which 'stepSys' +-- discards. Defining both here means what it observes is exactly the traffic +-- the memory service responds to. +-- +-- The system is the core in a loop with 'idealServe': the core's request goes +-- to memory, and memory's response is the core's input in the next cycle. +stepSysOut :: (RegFileOps r, MemOps m) => SysG r m -> (SysG r m, Output) +stepSysOut (Sys core inp mem) = + let (core', o) = Core.circuit core inp + (mem', inp') = idealServe mem (outMem o) + in (Sys core' inp' mem', o) diff --git a/proof/Proof/Functional/Obligation.hs b/proof/Proof/Core/Functional/Obligation.hs similarity index 68% rename from proof/Proof/Functional/Obligation.hs rename to proof/Proof/Core/Functional/Obligation.hs index 86cc88e..706f17b 100644 --- a/proof/Proof/Functional/Obligation.hs +++ b/proof/Proof/Core/Functional/Obligation.hs @@ -1,29 +1,33 @@ -- | The proof obligations, in one place. -- --- Both the symbolic properties ("Proof.Functional.Induction") and the QuickCheck harness +-- Both the symbolic properties ("Proof.Core.Functional.Solver") and the QuickCheck harness -- ("ProofSpec") go through these definitions, so the two cannot drift apart. -- The only thing they are allowed to differ in is how the system state is -- built: symbolic scalars on one side, a generator on the other. That is the -- input space, not the property. -module Proof.Functional.Obligation +module Proof.Core.Functional.Obligation ( isaAt, - baseCaseObligation, - indStepObligation, - indStepObligation1, - indStepObligation2, - indStepObligation3, + flushedRegFile, + flushedMem, + regFileUnderInv, + memUnderInv, + baseCase, + indStep0, + indStep1, + indStep2, + indStep3, ) where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Data.Maybe (fromMaybe) import qualified Core -import Data.Functor.Identity -import Proof.Functional.Driver (driver) -import ISA (IsaStateG (..), StepG (..), isaStep) -import Proof.Functional.Invariant +import Proof.Core.Functional.Driver (driver) +import Core.ISA (IsaStateG (..), StepG (..), isaStep) +import Proof.Core.Functional.Invariant import Memory.Types (MemOps (..)) -import Proof.Machine -import RegFile +import Proof.Core.Functional.Machine +import Core.RegFile import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) @@ -33,7 +37,7 @@ import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&& -- The containers are /derived/ from @sys@ by the flush rather than taken as -- further inputs. They have to be: the invariant compares them pointwise, at one -- witness register and one witness byte, so a freely quantified register file --- and memory would be tied to @sys@ only at those two points. 'ISA.isaStep' +-- and memory would be tied to @sys@ only at those two points. 'Core.ISA.isaStep' -- reads memory at @isaPc@ and registers at @rs1@/@rs2@, which are elsewhere, so -- the solver could pick an architectural state whose instruction at @isaPc@ -- bears no relation to the one the core is executing. Deriving them makes the @@ -45,20 +49,46 @@ import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&& -- @stateExPc@ when running and @stateHalt@ once halted. Deriving it from either -- one would make the other case unsatisfiable as a premise. isaAt :: (RegFileOps r, MemOps m) => Address -> SysG r m -> IsaStateG r m -isaAt ipc (Sys st inp mem) = - IsaState {isaPc = ipc, isaRegFile = frf, isaMem = fm} - where - (fm, frf) = - flushMeStage - (Core.stateMeInstr st) - (runIdentity (Core.stateMeRes st)) - (Core.stateMeAddr st) - ( flushWbStage - (Core.stateWbInstr st) - (runIdentity (Core.stateWbRes st)) - (runIdentity (Core.inputMem inp)) - (mem, Core.stateRegFile st) - ) +isaAt ipc sys = + IsaState {isaPc = ipc, isaRegFile = flushedRegFile sys, isaMem = flushedMem sys} + +-- | The register file the core stands for: its own, with the writes still in +-- the pipeline (the memory and writeback stages) applied. +flushedRegFile :: (RegFileOps r, MemOps m) => SysG r m -> r +flushedRegFile = snd . flushed + +-- | The memory the core stands for: its own, with the stores still in the +-- pipeline (the memory and writeback stages) applied. +flushedMem :: (RegFileOps r, MemOps m) => SysG r m -> m +flushedMem = fst . flushed + +-- | The pipeline's pending writes applied to memory and the register file. +flushed :: (RegFileOps r, MemOps m) => SysG r m -> (m, r) +flushed (Sys core inp mem) = + flushMeStage + (Core.stateMeInstr core) + (Core.stateMeRes core) + (Core.stateMeAddr core) + ( flushWbStage + (Core.stateWbInstr core) + (Core.stateWbRes core) + (fromMaybe 0 (Core.inputMem inp)) + (mem, Core.stateRegFile core) + ) + +-- | The invariant relating the core to the ISA implies that the ISA's register +-- file is the core's, flushed ('flushedRegFile'), at register @wr@. +regFileUnderInv :: (RegFileOps r, MemOps m) => RegIdx -> Address -> IsaStateG r m -> SysG r m -> Bool +regFileUnderInv wr wa isa sys = + not (invAt wr wa isa sys) + || lookupRFg wr (isaRegFile isa) == lookupRFg wr (flushedRegFile sys) + +-- | The invariant relating the core to the ISA implies that the ISA's memory is +-- the core's, flushed ('flushedMem'), at byte @wa@. +memUnderInv :: (RegFileOps r, MemOps m) => RegIdx -> Address -> IsaStateG r m -> SysG r m -> Bool +memUnderInv wr wa isa sys = + not (invAt wr wa isa sys) + || memReadByte wa (isaMem isa) == memReadByte wa (flushedMem sys) -- | The base case: the invariant holds once the initial state has taken its -- first hop. @@ -87,13 +117,13 @@ isaAt ipc (Sys st inp mem) = -- values on both sides, and the first hop writes neither, so the invariant's -- two container equalities hold by construction here and this property alone -- would not notice if the core's initial register file and the ISA's --- ('RegFile.initRF') disagreed. The concrete test in "ProofSpec" closes that +-- ('Core.RegFile.initRF') disagreed. The concrete test in "ProofSpec" closes that -- gap -- it runs on the real 'Vec'-backed state, where both files are built -- independently. -baseCaseObligation :: - (RegFileOps r, MemOps m) => r Identity -> m -> RegIdx -> Address -> Address -> Bool -baseCaseObligation rf mem wr wa pc = - driver sys == 1 && invAtFree wr wa isa sys2 +baseCase :: + (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> r -> m -> Bool +baseCase wr wa pc rf mem = + driver sys == 1 && invAt wr wa isa sys2 where isa = IsaState {isaPc = pc, isaRegFile = rf, isaMem = mem} sys = Sys (Core.initAt pc rf) Core.initInput mem @@ -115,9 +145,9 @@ baseCaseObligation rf mem wr wa pc = -- core stands still -- the halted cases of the invariant require the -- architectural register file and memory to equal the core's, so carrying the -- same @isa@ across the step asserts that neither changed. -indStepObligation :: +indStep0 :: (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> Bool -indStepObligation wr wa ipc sys = +indStep0 wr wa ipc sys = not premises || conclusion where isa = isaAt ipc sys @@ -128,19 +158,19 @@ indStepObligation wr wa ipc sys = sys' = stepSys sys premises = - invAtFree wr wa isa sys + invAt wr wa isa sys && driver sys == 0 - conclusion = invAtFree wr wa isa' sys' + conclusion = invAt wr wa isa' sys' -- | The @k = 1@ inductive step: the driver's two-cycle hop. -- -- The driver also gives the reset state a two-cycle hop, but no obligation -- covers it: the invariant does not admit the reset state, and --- 'Proof.Functional.Induction.baseCase' states that hop directly. -indStepObligation1 :: +-- 'Proof.Core.Functional.Solver.baseCase' states that hop directly. +indStep1 :: (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> Bool -indStepObligation1 wr wa ipc sys = +indStep1 wr wa ipc sys = not premises || conclusion where isa = isaAt ipc sys @@ -152,19 +182,19 @@ indStepObligation1 wr wa ipc sys = sys2 = stepSys sys1 premises = - invAtFree wr wa isa sys + invAt wr wa isa sys && driver sys == 1 - conclusion = invAtFree wr wa isa' sys2 + conclusion = invAt wr wa isa' sys2 -- | The @k = 2@ inductive step: the driver's three-cycle hop. -- -- Unlike the shorter hops, this one can execute an environment instruction. -- The architectural state then stays at the trapping instruction while the -- core reaches one of the two halted invariant cases. -indStepObligation2 :: +indStep2 :: (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> Bool -indStepObligation2 wr wa ipc sys = +indStep2 wr wa ipc sys = not premises || conclusion where isa = isaAt ipc sys @@ -177,21 +207,21 @@ indStepObligation2 wr wa ipc sys = sys3 = stepSys sys2 premises = - invAtFree wr wa isa sys + invAt wr wa isa sys && driver sys == 2 - conclusion = invAtFree wr wa isa' sys3 + conclusion = invAt wr wa isa' sys3 -- | The @k = 3@ inductive step: the driver's four-cycle hop, the longest. -- --- Stated exactly as 'indStepObligation2', one cycle longer. The @IsaHalted@ +-- Stated exactly as 'indStep2', one cycle longer. The @IsaHalted@ -- alternative is kept even though this hop should not be able to trap -- the -- driver routes environment instructions to a three-cycle hop -- because -- covering it costs nothing and assuming it away would be an unchecked side -- argument. -indStepObligation3 :: +indStep3 :: (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> Bool -indStepObligation3 wr wa ipc sys = +indStep3 wr wa ipc sys = not premises || conclusion where isa = isaAt ipc sys @@ -205,7 +235,7 @@ indStepObligation3 wr wa ipc sys = sys4 = stepSys sys3 premises = - invAtFree wr wa isa sys + invAt wr wa isa sys && driver sys == 3 - conclusion = invAtFree wr wa isa' sys4 + conclusion = invAt wr wa isa' sys4 diff --git a/proof/Proof/Core/Functional/Solver.hs b/proof/Proof/Core/Functional/Solver.hs new file mode 100644 index 0000000..9f2f7ca --- /dev/null +++ b/proof/Proof/Core/Functional/Solver.hs @@ -0,0 +1,141 @@ +-- | The inductive steps of the refinement proof, checked symbolically. +-- +-- 'baseCase' says the invariant holds once the reset state has taken its first +-- hop. Then one property per driver +-- delay: if the invariant relates @(isa, sys)@ and the driver says the hop takes +-- @k + 1@ cycles, then after those cycles (and one ISA step, where the hop +-- retires an instruction) the invariant relates them again. Base case plus the +-- four steps is the whole refinement theorem. +-- +-- Checking one @k@ at a time keeps the number of unrolled cycles concrete, +-- which sidesteps Pantomime's termination check: @stepSysN (driver sys + 1)@ +-- would recurse on a symbolic count. +-- +-- Each property is checked by the plugin at compile time and spliced into +-- 'results': 'Nothing' when valid, @'Just' counterexample@ when not. The +-- statements themselves live in "Proof.Core.Functional.Obligation", shared with the QuickCheck +-- harness so the two cannot drift. +-- +-- The pipeline state is passed as a 'KState' plus SMT-array register file and +-- memory; see "Proof.Core.Functional.System". +module Proof.Core.Functional.Solver + ( arrRoundTripP, + shiftsSaneP, + baseCaseP, + indStep0P, + indStep1P, + indStep2P, + indStep3P, + regFileUnderInvP, + memUnderInvP, + results, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import qualified Core +import Core.ISA (IsaStateG (..)) +import Pantomime (Theory (..)) +import qualified Pantomime.BuiltIn as Pantomime +import Proof.Core.Functional.Obligation +import Proof.SMT.Array +import Proof.SMT.Axioms (arrayAxioms) +import Proof.SMT.Logged (pantomime) +import Proof.Core.Functional.System +import Types +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- Sanity probes for the trusted embeddings ------------------------------------- +-- +-- The term axioms in "Proof.SMT.Axioms" replace Haskell functions by hand-written SMT +-- counterparts, so they are trusted, not proved. These two probes check each +-- embedding against facts a broken one would get wrong. + +-- | The register-file array embedding: a read after a write at the same index +-- gives the written value. +{-# ANN arrRoundTripP (Theory arrayAxioms) #-} +arrRoundTripP :: RegArr -> RegIdx -> Word -> Pantomime.Bool +arrRoundTripP a i v = Pantomime.boolean $ loadRA (storeRA a i v) i == v + +-- | The shift embeddings: identities that would fail if the three shifts were +-- mixed up, the zero-extension of the amount were wrong, or the arithmetic +-- shift lost its sign. +{-# ANN shiftsSaneP (Theory arrayAxioms) #-} +shiftsSaneP :: Word -> Pantomime.Bool +shiftsSaneP x = + Pantomime.boolean $ + Core.sllWord x 0 == x + && Core.srlWord x 0 == x + && Core.sraWord x 0 == x + && Core.sllWord x 1 == x + x + && Core.srlWord x 31 == (if sign == 1 then 1 else 0) + && Core.sraWord x 31 == (if sign == 1 then 0xFFFFFFFF else 0) + where + sign = slice d31 d31 x + +-- The base case ---------------------------------------------------------------- + +{-# ANN baseCaseP (Theory arrayAxioms) #-} +baseCaseP :: RegIdx -> Address -> Address -> RegArr -> MemArr -> Pantomime.Bool +baseCaseP wr wa pc ra ma = + Pantomime.boolean $ baseCase wr wa pc (RegArrF ra) ma + +-- The inductive steps ---------------------------------------------------------- + +-- | @k = 0@: the one-cycle hop (steady, writeback non-memory). +{-# ANN indStep0P (Theory arrayAxioms) #-} +indStep0P :: RegIdx -> Address -> Address -> KState -> Core.Input -> RegArr -> MemArr -> Pantomime.Bool +indStep0P wr wa ipc ss i ra ma = + Pantomime.boolean $ indStep0 wr wa ipc (sysOf ss i ra ma) + +-- | @k = 1@: the two-cycle hop (a memory instruction in writeback). +{-# ANN indStep1P (Theory arrayAxioms) #-} +indStep1P :: RegIdx -> Address -> Address -> KState -> Core.Input -> RegArr -> MemArr -> Pantomime.Bool +indStep1P wr wa ipc ss i ra ma = + Pantomime.boolean $ indStep1 wr wa ipc (sysOf ss i ra ma) + +-- | @k = 2@: the three-cycle hop (environment, taken jump, store hazard with a +-- non-memory execute instruction, or memory instructions in both older stages). +-- The hop on which the ISA enters a halt; a halted state then sits at k = 0. +{-# ANN indStep2P (Theory arrayAxioms) #-} +indStep2P :: RegIdx -> Address -> Address -> KState -> Core.Input -> RegArr -> MemArr -> Pantomime.Bool +indStep2P wr wa ipc ss i ra ma = + Pantomime.boolean $ indStep2 wr wa ipc (sysOf ss i ra ma) + +-- | @k = 3@: the four-cycle hop (store hazard with a memory execute +-- instruction, load hazard, or all three stages holding memory instructions). +{-# ANN indStep3P (Theory arrayAxioms) #-} +indStep3P :: RegIdx -> Address -> Address -> KState -> Core.Input -> RegArr -> MemArr -> Pantomime.Bool +indStep3P wr wa ipc ss i ra ma = + Pantomime.boolean $ indStep3 wr wa ipc (sysOf ss i ra ma) + +-- The invariant and the flush --------------------------------------------------- + +-- | The invariant relating the core to the ISA implies that the ISA's register +-- file is the core's, flushed. The ISA state is free, not derived from the core. +{-# ANN regFileUnderInvP (Theory arrayAxioms) #-} +regFileUnderInvP :: + RegIdx -> Address -> Address -> RegArr -> MemArr -> KState -> Core.Input -> RegArr -> MemArr -> Pantomime.Bool +regFileUnderInvP wr wa ipc ira ima ss i ra ma = + Pantomime.boolean $ regFileUnderInv wr wa (IsaState ipc (RegArrF ira) ima) (sysOf ss i ra ma) + +-- | The invariant relating the core to the ISA implies that the ISA's memory is +-- the core's, flushed. +{-# ANN memUnderInvP (Theory arrayAxioms) #-} +memUnderInvP :: + RegIdx -> Address -> Address -> RegArr -> MemArr -> KState -> Core.Input -> RegArr -> MemArr -> Pantomime.Bool +memUnderInvP wr wa ipc ira ima ss i ra ma = + Pantomime.boolean $ memUnderInv wr wa (IsaState ipc (RegArrF ira) ima) (sysOf ss i ra ma) + +results :: [(String, Maybe String)] +results = + [ ("arrRoundTripP", $(pantomime 'arrRoundTripP)), + ("shiftsSaneP", $(pantomime 'shiftsSaneP)), + ("baseCaseP", $(pantomime 'baseCaseP)), + ("indStep0P", $(pantomime 'indStep0P)), + ("indStep1P", $(pantomime 'indStep1P)), + ("indStep2P", $(pantomime 'indStep2P)), + ("indStep3P", $(pantomime 'indStep3P)), + ("regFileUnderInvP", $(pantomime 'regFileUnderInvP)), + ("memUnderInvP", $(pantomime 'memUnderInvP)) + ] diff --git a/proof-smt/Proof/SMT/System.hs b/proof/Proof/Core/Functional/System.hs similarity index 79% rename from proof-smt/Proof/SMT/System.hs rename to proof/Proof/Core/Functional/System.hs index 69e9f4a..5d35ac7 100644 --- a/proof-smt/Proof/SMT/System.hs +++ b/proof/Proof/Core/Functional/System.hs @@ -4,12 +4,12 @@ -- register file and memory as SMT arrays: an ADT of scalars can be a fresh -- symbolic argument, a record containing a function cannot, and the Clash -- @Vec@ API is opaque to the plugin (see "Proof.SMT.Array"). 'sysOf' assembles --- the pieces into a 'Proof.Machine.SysG'. +-- the pieces into a 'Proof.Core.Functional.Machine.SysG'. -- -- Shared by the functional and the leakage inductions, so that neither imports -- the other: their obligations are discharged while GHC compiles them, and an -- import between them would re-run one proof whenever the other changes. -module Proof.SMT.System +module Proof.Core.Functional.System ( -- | Exported because nothing in Haskell ever applies the constructor: the -- plugin synthesises a 'KState' as a fresh symbolic input to each property, -- and 'sysOf' only reads it back through the field accessors. Without this @@ -21,9 +21,8 @@ where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import qualified Core -import Data.Functor.Identity -import Instruction (Instruction) -import Proof.Machine +import Core.Instruction (Instruction) +import Proof.Core.Functional.Machine import Proof.SMT.Array import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) @@ -40,16 +39,15 @@ data KState = KState kMeAddr :: Address, kWbIr :: Instruction, kWbRes :: Word, - kCtrl :: Core.Control Identity, - kHalt :: Maybe Core.HaltState, - kHaltNextPc :: Address + kCtrl :: Core.Control, + kHalt :: Maybe Core.HaltState } -- | Assemble a system state from the symbolic pieces. -sysOf :: KState -> Core.Input Identity -> RegArr -> MemArr -> SysG RegArrF MemArr +sysOf :: KState -> Core.Input -> RegArr -> MemArr -> SysG RegArrF MemArr sysOf ss i ra ma = Sys - { sysState = + { sysCore = Core.State { Core.stateFePc = kFePc ss, Core.stateDePc = kDePc ss, @@ -57,14 +55,13 @@ sysOf ss i ra ma = Core.stateExPc = kExPc ss, Core.stateExInstr = kExIr ss, Core.stateMeInstr = kMeIr ss, - Core.stateMeRes = Identity (kMeRes ss), + Core.stateMeRes = kMeRes ss, Core.stateMeAddr = kMeAddr ss, Core.stateWbInstr = kWbIr ss, - Core.stateWbRes = Identity (kWbRes ss), + Core.stateWbRes = kWbRes ss, Core.stateRegFile = RegArrF ra, Core.stateCtrl = kCtrl ss, - Core.stateHalt = kHalt ss, - Core.stateHaltNextPc = kHaltNextPc ss + Core.stateHalt = kHalt ss }, sysInput = i, sysMem = ma diff --git a/proof/Proof/Leakage/Driver.hs b/proof/Proof/Core/Leakage/Driver.hs similarity index 82% rename from proof/Proof/Leakage/Driver.hs rename to proof/Proof/Core/Leakage/Driver.hs index b23e0a4..e84a71d 100644 --- a/proof/Proof/Leakage/Driver.hs +++ b/proof/Proof/Core/Leakage/Driver.hs @@ -1,8 +1,8 @@ -- | The simulator's driver: how many cycles the simulator takes for an -- instruction, computed from its own state and the instruction's leakage. The --- counterpart of 'Proof.Functional.Driver.driver', case for case; the leakage +-- counterpart of 'Proof.Core.Functional.Driver.driver', case for case; the leakage -- proof's first step is that the two agree. -module Proof.Leakage.Driver +module Proof.Core.Leakage.Driver ( simDriver, simStoreHazard, simLoadHazard @@ -10,9 +10,9 @@ module Proof.Leakage.Driver where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) -import qualified Instruction -import Proof.Leakage.Model -import Proof.Leakage.Simulator +import qualified Core.Instruction +import Proof.Core.Leakage.Model +import Proof.Core.Leakage.Simulator import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) -- | The store-hazard condition of 'Core.decode': the instruction word at the @@ -20,8 +20,8 @@ import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&& -- stage. simStoreHazard :: SimInput -> SimState -> Bool simStoreHazard inp st = - maybe False (Instruction.storeHazard dePc) exStore - || maybe False (Instruction.storeHazard dePc) meStore + maybe False (Core.Instruction.storeHazard dePc) exStore + || maybe False (Core.Instruction.storeHazard dePc) meStore where dePc = simStateDePc st exStore = case inp of diff --git a/proof/Proof/Leakage/Invariant.hs b/proof/Proof/Core/Leakage/Invariant.hs similarity index 59% rename from proof/Proof/Leakage/Invariant.hs rename to proof/Proof/Core/Leakage/Invariant.hs index 5ba9c61..4740b21 100644 --- a/proof/Proof/Leakage/Invariant.hs +++ b/proof/Proof/Core/Leakage/Invariant.hs @@ -1,6 +1,6 @@ -- | The invariant relating the leakage simulator to the core: the leakage --- counterpart of "Proof.Functional.Invariant". -module Proof.Leakage.Invariant +-- counterpart of "Proof.Core.Functional.Invariant". +module Proof.Core.Leakage.Invariant ( simInv ) where @@ -8,10 +8,10 @@ where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Core import Data.Maybe (isJust, isNothing) -import Instruction hiding (Halted) -import Proof.Leakage.Model -import Proof.Leakage.Simulator -import Proof.Machine +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, (!!), (&&), (++), (||)) -- | The relation between the simulator and the core that the leakage proof @@ -32,21 +32,21 @@ simInv :: SimState -> SysG r m -> Bool -simInv sim (Sys st _ _) = - simStateFePc sim == stateFePc st - && simStateDePc sim == stateDePc st - && simStateDeExpInstr sim == stateDeExpInstr st +simInv sim (Sys core _ _) = + simStateFePc sim == stateFePc core + && simStateDePc sim == stateDePc core + && simStateDeExpInstr sim == stateDeExpInstr core && exStage && meStage where exStage = case simStateExInstrType sim of - DecodedInstr -> isNothing (stateHalt st) - Halted -> isJust (stateHalt st) + DecodedInstr -> isNothing (stateHalt core) + Halted -> isJust (stateHalt core) _ -> False - meStage = case (simStateMeInstr sim, stateMeInstr st) of - (LLoad size addr _, Instruction.IType (Load size' _) _ _ _) -> - size == size' && addr == stateMeAddr st - (LStore size addr, Instruction.SType size' _ _ _) -> - size == size' && addr == stateMeAddr st - (leak, ir) -> not (isMemLeak leak) && not (Instruction.isMemInstr ir) + 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) diff --git a/proof/Proof/Leakage/Model.hs b/proof/Proof/Core/Leakage/Model.hs similarity index 74% rename from proof/Proof/Leakage/Model.hs rename to proof/Proof/Core/Leakage/Model.hs index 4d77cb4..e14c7fb 100644 --- a/proof/Proof/Leakage/Model.hs +++ b/proof/Proof/Core/Leakage/Model.hs @@ -1,6 +1,6 @@ -- | What an attacker sees, and what one architectural instruction leaks. -- --- The leakage proof ("Proof.Leakage.Obligation") establishes that an attacker +-- The leakage proof ("Proof.Core.Leakage.Obligation") establishes that an attacker -- watching the memory bus learns nothing beyond 'Leak'. Two definitions carry -- that statement: -- @@ -18,25 +18,20 @@ -- load-use hazard against it, which is the one thing the fetch trace does not -- already give away, since it decides how long the hop takes. -- --- == What 'Leak' is, and is not +-- == What 'Leak' means -- --- It is not a list of secrets. Every field is public in any run that does not --- halt, because 'Core.execute' computes each one inside @noSecrets'@: the --- branch condition, the @jalr@ target, and the load and store addresses. The --- fetched instruction word goes through @noSecrets'@ in 'Core.decode' too, so --- the program is public even under self-modifying code -- which matters, because --- store /data/ is not forced public, so a store could otherwise plant a --- secret-dependent instruction. A secret reaching any of these halts the core --- with 'Core.SecurityViolation'. The hazard bit is not even data dependent: --- 'Instruction.loadHazard' compares register /fields/, not their contents. --- --- So 'Leak' is what the /simulator/ needs in order to replay the observation --- from the architectural state alone, not what escapes. The security content --- lives in the @Access@ / @noSecrets@ discipline. -module Proof.Leakage.Model +-- The leakage theorem says the bus observation is a function of the ISA-level +-- leakage trace: an attacker watching the bus learns nothing beyond the 'Leak' +-- of each executed instruction. The core does not keep any of it secret -- the +-- branch outcome, the @jalr@ target and the load and store addresses all show. +-- Whether a program is constant-time is a property of its leakage trace, +-- checked at the ISA level. The hazard bit is not data dependent: +-- 'Core.Instruction.loadHazard' compares register /fields/, not their contents. +module Proof.Core.Leakage.Model ( -- * Observation Obs (..), obsOf, + obsReq, -- * Leakage Leak (..), @@ -49,11 +44,10 @@ where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Core -import Data.Functor.Identity -import Instruction -import ISA (IsaStateG (..), isaInstrAt) +import Core.Instruction +import Core.ISA (IsaStateG (..), isaInstrAt) import Memory.Types (MemOps (..)) -import RegFile +import Core.RegFile import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) @@ -75,13 +69,21 @@ instance Semigroup Obs where instance Monoid Obs where mempty = NoAccess --- | The observation a cycle's 'Core.Output' produces. -obsOf :: Output Identity -> Obs -obsOf o = case outMem o of +-- | The observation a cycle's 'Core.Output' produces: that of its request. +obsOf :: Output -> Obs +obsOf o = obsReq (outMem o) + +-- | The observation of a request on the bus: the request without its data. +-- +-- This is also what a cache in front of the core leaks about each request it +-- receives ("Proof.Cache.Server4K"), which is what lets the core's leakage proof +-- and the cache's compose. +obsReq :: Request -> Obs +obsReq req = case req of Nothing -> NoAccess - Just (MemAccess True addr _ _) -> Fetch addr - Just (MemAccess False addr size Nothing) -> DataRead addr size - Just (MemAccess False addr size (Just _)) -> DataWrite addr size + Just (MemFetch addr) -> Fetch addr + Just (MemRead addr size) -> DataRead addr size + Just (MemWrite addr size _) -> DataWrite addr size -- Leakage --------------------------------------------------------------------- @@ -132,7 +134,7 @@ leakOf isa@(IsaState pc rf _) = IType (Arith _) _ _ _ -> LArith UType {} -> LArith BType cmp imm rs1 rs2 -> - let doBranch = runIdentity $ branch cmp (pure (regv rs1)) (pure (regv rs2)) + let doBranch = branch cmp (regv rs1) (regv rs2) in if doBranch then LJump (pc + off imm) else LArith @@ -151,6 +153,6 @@ leakOf isa@(IsaState pc rf _) = Nop _ -> LArith where ir = isaInstrAt isa - regv i = runIdentity (lookupRFg i rf) + regv i = lookupRFg i rf off imm = unpack $ signExtend imm addr rs1 imm = unpack $ regv rs1 + signExtend imm diff --git a/proof/Proof/Leakage/Obligation.hs b/proof/Proof/Core/Leakage/Obligation.hs similarity index 80% rename from proof/Proof/Leakage/Obligation.hs rename to proof/Proof/Core/Leakage/Obligation.hs index b1c73e1..f527e81 100644 --- a/proof/Proof/Leakage/Obligation.hs +++ b/proof/Proof/Core/Leakage/Obligation.hs @@ -5,33 +5,32 @@ -- sees only 'leakOf' of the ISA state, produces the same bus observation as the -- core on every cycle, and takes the same number of cycles per instruction. -- --- Each inductive step assumes the functional invariant ('invAtFree') as a +-- Each inductive step assumes the functional invariant ('invAt') as a -- premise. It pins the core's execute stage to the ISA's next instruction, so -- feeding the simulator that instruction's leakage keeps the two machines in -- step. The functional proof supplies the invariant for the next hop, so it is -- not re-proved here. 'simInv' carries the rest from hop to hop. -module Proof.Leakage.Obligation - ( baseCaseLeakObligation, - indStepLeakObligation, - indStepLeakObligation1, - indStepLeakObligation2, - indStepLeakObligation3 +module Proof.Core.Leakage.Obligation + ( baseCaseLeak, + indStepLeak0, + indStepLeak1, + indStepLeak2, + indStepLeak3 ) where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Core -import Data.Functor.Identity import Memory.Types (MemOps (..)) -import Proof.Functional.Driver -import Proof.Functional.Invariant (invAtFree) -import Proof.Functional.Obligation -import Proof.Leakage.Driver -import Proof.Leakage.Invariant -import Proof.Leakage.Model -import Proof.Leakage.Simulator -import Proof.Machine -import RegFile +import Proof.Core.Functional.Driver +import Proof.Core.Functional.Invariant (invAt) +import Proof.Core.Functional.Obligation +import Proof.Core.Leakage.Driver +import Proof.Core.Leakage.Invariant +import Proof.Core.Leakage.Model +import Proof.Core.Leakage.Simulator +import Proof.Core.Functional.Machine +import Core.RegFile import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) @@ -43,10 +42,10 @@ import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&& -- gets no leakage, the simulator's driver gives the same hop length as the -- core's, the two make the same bus observations, and 'simInv' holds -- afterwards. The register file and memory are arbitrary, as in --- 'Proof.Functional.Obligation.baseCaseObligation'. -baseCaseLeakObligation :: - (RegFileOps r, MemOps m) => r Identity -> m -> Address -> Bool -baseCaseLeakObligation rf mem pc = +-- 'Proof.Core.Functional.Obligation.baseCase'. +baseCaseLeak :: + (RegFileOps r, MemOps m) => Address -> r -> m -> Bool +baseCaseLeak pc rf mem = simDriver Nothing sim == 1 && obs1 == obsOf out1 && obs2 == obsOf out2 @@ -67,9 +66,9 @@ baseCaseLeakObligation rf mem pc = -- > ==> simDriver(leak, sim) = 0 /\ obs(sim) = obs(sys) /\ simInv(sim', sys') -- -- The simulator gets @leakOf isa@ on the hop's first cycle and nothing after. -indStepLeakObligation :: +indStepLeak0 :: (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> SimState -> Bool -indStepLeakObligation wr wa ipc sys sim = +indStepLeak0 wr wa ipc sys sim = not premises || conclusion where isa = isaAt ipc sys @@ -79,7 +78,7 @@ indStepLeakObligation wr wa ipc sys sim = (sim', obs') = simCircuit sim (Just leak) premises = - invAtFree wr wa isa sys + invAt wr wa isa sys && driver sys == 0 && simInv sim sys @@ -89,9 +88,9 @@ indStepLeakObligation wr wa ipc sys sim = && simInv sim' sys' -- | The @k = 1@ leakage step: the two-cycle hop. -indStepLeakObligation1 :: +indStepLeak1 :: (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> SimState -> Bool -indStepLeakObligation1 wr wa ipc sys sim = +indStepLeak1 wr wa ipc sys sim = not premises || conclusion where isa = isaAt ipc sys @@ -104,7 +103,7 @@ indStepLeakObligation1 wr wa ipc sys sim = (sim2, obs2) = simCircuit sim1 Nothing premises = - invAtFree wr wa isa sys + invAt wr wa isa sys && driver sys == 1 && simInv sim sys @@ -115,9 +114,9 @@ indStepLeakObligation1 wr wa ipc sys sim = && simInv sim2 sys2 -- | The @k = 2@ leakage step: the three-cycle hop. -indStepLeakObligation2 :: +indStepLeak2 :: (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> SimState -> Bool -indStepLeakObligation2 wr wa ipc sys sim = +indStepLeak2 wr wa ipc sys sim = not premises || conclusion where isa = isaAt ipc sys @@ -133,7 +132,7 @@ indStepLeakObligation2 wr wa ipc sys sim = (sim3, obs3) = simCircuit sim2 Nothing premises = - invAtFree wr wa isa sys + invAt wr wa isa sys && driver sys == 2 && simInv sim sys @@ -145,9 +144,9 @@ indStepLeakObligation2 wr wa ipc sys sim = && simInv sim3 sys3 -- | The @k = 3@ leakage step: the four-cycle hop, the longest. -indStepLeakObligation3 :: +indStepLeak3 :: (RegFileOps r, MemOps m) => RegIdx -> Address -> Address -> SysG r m -> SimState -> Bool -indStepLeakObligation3 wr wa ipc sys sim = +indStepLeak3 wr wa ipc sys sim = not premises || conclusion where isa = isaAt ipc sys @@ -166,7 +165,7 @@ indStepLeakObligation3 wr wa ipc sys sim = (sim4, obs4) = simCircuit sim3 Nothing premises = - invAtFree wr wa isa sys + invAt wr wa isa sys && driver sys == 3 && simInv sim sys diff --git a/proof/Proof/Leakage/Simulator.hs b/proof/Proof/Core/Leakage/Simulator.hs similarity index 96% rename from proof/Proof/Leakage/Simulator.hs rename to proof/Proof/Core/Leakage/Simulator.hs index 61cf228..d36a964 100644 --- a/proof/Proof/Leakage/Simulator.hs +++ b/proof/Proof/Core/Leakage/Simulator.hs @@ -8,7 +8,7 @@ -- shows that, fed the ISA's leakage, it produces the same observations as the -- core, so everything an attacker on the bus sees is a function of the leakage -- alone. -module Proof.Leakage.Simulator +module Proof.Core.Leakage.Simulator ( SimInput, SimOutput, SimExInstrType (..), @@ -25,9 +25,9 @@ import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Control.Monad import Control.Monad.RWS import Data.Maybe (fromMaybe, isJust) -import Instruction (storeHazard) +import Core.Instruction (storeHazard) import Memory.Types -import Proof.Leakage.Model +import Proof.Core.Leakage.Model import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) @@ -52,8 +52,9 @@ data SimExInstrType StallStoreHazardFirstCycle | -- | Second instruction discarded because of a store hazard. StallStoreHazardSecondCycle - | -- | No instruction read because of memory bus overload. - StallMemoryBusBusy + | -- | No instruction this cycle: the fetch stage did not fetch, because the + -- memory stage used the bus. + StallNoInstruction | -- | First cycle. FirstCycle | -- | The core has halted. @@ -194,7 +195,7 @@ simDecode = do expInstr <- gets simStateDeExpInstr ctrl <- gets simStateCtrl - let irt = if expInstr then DecodedInstr else StallMemoryBusBusy + let irt = if expInstr then DecodedInstr else StallNoInstruction let halted = simCtrlExInstrType ctrl == Just Halted let env_instr_current_cycle = simCtrlExEnvInstr ctrl diff --git a/proof-smt/Proof/Leakage/Induction.hs b/proof/Proof/Core/Leakage/Solver.hs similarity index 50% rename from proof-smt/Proof/Leakage/Induction.hs rename to proof/Proof/Core/Leakage/Solver.hs index dae284c..c431935 100644 --- a/proof-smt/Proof/Leakage/Induction.hs +++ b/proof/Proof/Core/Leakage/Solver.hs @@ -1,23 +1,23 @@ -- | The leakage proof, checked symbolically. -- -- 'baseCaseLeak' plus one property per driver delay: on a hop of that length, --- the corresponding obligation in "Proof.Leakage.Obligation" holds. Split by +-- the corresponding obligation in "Proof.Core.Leakage.Obligation" holds. Split by -- @k@ because the number of unrolled cycles has to be concrete -- Pantomime -- cannot recurse on a symbolic count -- and each property pins @driver == k@ so -- it carries one unrolling rather than four. -- --- Together with "Proof.Functional.Induction" these are the leakage theorem: the +-- Together with "Proof.Core.Functional.Solver" these are the leakage theorem: the -- functional proof establishes that the invariant holds wherever the driver -- lands, which each step here assumes as a premise. -- -- Each query runs both the core and the simulator over the hop and compares -- their per-cycle bus observations, the two drivers' hop lengths and the -- simulator invariant, so they are larger than the corresponding functional --- ones. The statements live in "Proof.Leakage.Obligation"; this module only +-- ones. The statements live in "Proof.Core.Leakage.Obligation"; this module only -- instantiates them. -- -- The system state is passed as a 'KState' plus SMT-array register file and --- memory (see "Proof.SMT.System"); the simulator state is passed directly, +-- memory (see "Proof.Core.Functional.System"); the simulator state is passed directly, -- since it holds no register file or memory. -- -- == Running them @@ -25,27 +25,26 @@ -- Under Bitwuzla, not Z3: -- -- > SBV_Z3=/usr/local/bin/bitwuzla SBV_Z3_OPTIONS="--produce-models" stack build -module Proof.Leakage.Induction - ( baseCaseLeak, - indStepLeak, - indStepLeak1, - indStepLeak2, - indStepLeak3, +module Proof.Core.Leakage.Solver + ( baseCaseLeakP, + indStepLeak0P, + indStepLeak1P, + indStepLeak2P, + indStepLeak3P, results, ) where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import qualified Core -import Data.Functor.Identity import Pantomime (Theory (..)) import qualified Pantomime.BuiltIn as Pantomime -import Proof.Leakage.Obligation -import Proof.Leakage.Simulator +import Proof.Core.Leakage.Obligation +import Proof.Core.Leakage.Simulator import Proof.SMT.Array import Proof.SMT.Axioms (arrayAxioms) import Proof.SMT.Logged (pantomime) -import Proof.SMT.System +import Proof.Core.Functional.System import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) @@ -53,45 +52,45 @@ import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&& -- | The first hop from the initial state, for any start PC, register file and -- memory. -{-# ANN baseCaseLeak (Theory arrayAxioms) #-} -baseCaseLeak :: RegArr -> MemArr -> Address -> Pantomime.Bool -baseCaseLeak ra ma pc = - Pantomime.boolean $ baseCaseLeakObligation (RegArrF ra) ma pc +{-# ANN baseCaseLeakP (Theory arrayAxioms) #-} +baseCaseLeakP :: Address -> RegArr -> MemArr -> Pantomime.Bool +baseCaseLeakP pc ra ma = + Pantomime.boolean $ baseCaseLeak pc (RegArrF ra) ma -- The inductive steps ---------------------------------------------------------- -- | @k = 0@: the one-cycle hop (steady, writeback non-memory). -{-# ANN indStepLeak (Theory arrayAxioms) #-} -indStepLeak :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> SimState -> Pantomime.Bool -indStepLeak ss i ra ma wr wa ipc sim = - Pantomime.boolean $ indStepLeakObligation wr wa ipc (sysOf ss i ra ma) sim +{-# ANN indStepLeak0P (Theory arrayAxioms) #-} +indStepLeak0P :: RegIdx -> Address -> Address -> KState -> Core.Input -> RegArr -> MemArr -> SimState -> Pantomime.Bool +indStepLeak0P wr wa ipc ss i ra ma sim = + Pantomime.boolean $ indStepLeak0 wr wa ipc (sysOf ss i ra ma) sim -- | @k = 1@: the two-cycle hop (a memory instruction in writeback). -{-# ANN indStepLeak1 (Theory arrayAxioms) #-} -indStepLeak1 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> SimState -> Pantomime.Bool -indStepLeak1 ss i ra ma wr wa ipc sim = - Pantomime.boolean $ indStepLeakObligation1 wr wa ipc (sysOf ss i ra ma) sim +{-# ANN indStepLeak1P (Theory arrayAxioms) #-} +indStepLeak1P :: RegIdx -> Address -> Address -> KState -> Core.Input -> RegArr -> MemArr -> SimState -> Pantomime.Bool +indStepLeak1P wr wa ipc ss i ra ma sim = + Pantomime.boolean $ indStepLeak1 wr wa ipc (sysOf ss i ra ma) sim -- | @k = 2@: the three-cycle hop (environment, taken jump, store hazard with a -- non-memory execute instruction, or memory instructions in both older stages). -- The hop on which the ISA enters a halt; a halted state then sits at k = 0. -{-# ANN indStepLeak2 (Theory arrayAxioms) #-} -indStepLeak2 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> SimState -> Pantomime.Bool -indStepLeak2 ss i ra ma wr wa ipc sim = - Pantomime.boolean $ indStepLeakObligation2 wr wa ipc (sysOf ss i ra ma) sim +{-# ANN indStepLeak2P (Theory arrayAxioms) #-} +indStepLeak2P :: RegIdx -> Address -> Address -> KState -> Core.Input -> RegArr -> MemArr -> SimState -> Pantomime.Bool +indStepLeak2P wr wa ipc ss i ra ma sim = + Pantomime.boolean $ indStepLeak2 wr wa ipc (sysOf ss i ra ma) sim -- | @k = 3@: the four-cycle hop (store hazard with a memory execute -- instruction, load hazard, or all three stages holding memory instructions). -{-# ANN indStepLeak3 (Theory arrayAxioms) #-} -indStepLeak3 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> SimState -> Pantomime.Bool -indStepLeak3 ss i ra ma wr wa ipc sim = - Pantomime.boolean $ indStepLeakObligation3 wr wa ipc (sysOf ss i ra ma) sim +{-# ANN indStepLeak3P (Theory arrayAxioms) #-} +indStepLeak3P :: RegIdx -> Address -> Address -> KState -> Core.Input -> RegArr -> MemArr -> SimState -> Pantomime.Bool +indStepLeak3P wr wa ipc ss i ra ma sim = + Pantomime.boolean $ indStepLeak3 wr wa ipc (sysOf ss i ra ma) sim results :: [(String, Maybe String)] results = - [ ("baseCaseLeak", $(pantomime 'baseCaseLeak)), - ("indStepLeak", $(pantomime 'indStepLeak)), - ("indStepLeak1", $(pantomime 'indStepLeak1)), - ("indStepLeak2", $(pantomime 'indStepLeak2)), - ("indStepLeak3", $(pantomime 'indStepLeak3)) + [ ("baseCaseLeakP", $(pantomime 'baseCaseLeakP)), + ("indStepLeak0P", $(pantomime 'indStepLeak0P)), + ("indStepLeak1P", $(pantomime 'indStepLeak1P)), + ("indStepLeak2P", $(pantomime 'indStepLeak2P)), + ("indStepLeak3P", $(pantomime 'indStepLeak3P)) ] diff --git a/proof/Proof/Machine.hs b/proof/Proof/Machine.hs deleted file mode 100644 index 702a990..0000000 --- a/proof/Proof/Machine.hs +++ /dev/null @@ -1,97 +0,0 @@ -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE UndecidableInstances #-} - --- | The \"system\" that the driver and the invariant talk about. --- --- 'Core.circuit' is only the pipeline: memory lives outside it. The core emits --- a 'MemAccess' on its 'Output' and receives the response on the next --- 'Input'. So a single system step is one 'Core.circuit' step plus the memory --- service that 'Simulate.simulator' performs, and the state the proof reasons --- about is the triple --- --- > (Core.State f, Input f, Mem) --- --- which is exactly the shape the driver and invariant notes use. -module Proof.Machine - ( SysG (..), - Sys, - stepSys, - stepSysOut, - stepSysN, - initSys, - readMemWord, - ) -where - -import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) -import Core -import Data.Functor.Identity -import Memory.Types -import RegFile -import Types -import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) - --- | Core state, the input it is about to consume, and memory. -data SysG r m = Sys - { sysState :: Core.StateG r Identity, - sysInput :: Input Identity, - sysMem :: m - } - --- | The concrete system the QuickCheck harness runs: @Vec@-backed throughout. -type Sys = SysG RegFile MemBytes - -deriving instance (Show (r Identity), Show m) => Show (SysG r m) - --- | Structural equality. 'Input' has no 'Eq' instance in "Core" (adding one --- there clashes with the existing @Eq Out@ in the Leak modules), so we compare --- its fields directly. -instance (Eq (r Identity), Eq m) => Eq (SysG r m) where - Sys s1 i1 m1 == Sys s2 i2 m2 = - s1 == s2 - && runIdentity (inputMem i1) == runIdentity (inputMem i2) - && m1 == m2 - --- | One system step: run the pipeline for a cycle, then service whatever --- memory access it emitted. Mirrors 'Simulate.simulator', except that a halted --- core simply stops changing instead of ending the stream. -stepSys :: (RegFileOps r, MemOps m) => SysG r m -> SysG r m -stepSys = fst . stepSysOut - --- | 'stepSys', but also returning the pipeline's 'Output' for that cycle. --- --- The leakage proof observes the cycle-by-cycle memory traffic, which 'stepSys' --- discards. Defining both here means what it observes is exactly the traffic --- the memory service responds to. -stepSysOut :: (RegFileOps r, MemOps m) => SysG r m -> (SysG r m, Output Identity) -stepSysOut (Sys s i m) = - let (s', o) = Core.circuit s i - (i', m') = service (outMem o) m - in (Sys s' i' m', o) - where - service (Just (MemAccess _ addr size mval)) mem = - case mval of - -- 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 (pure (memReadWord addr mem)), mem) - -- A write. - Just val -> (Input (pure 0), memWriteWord size addr (runIdentity val) mem) - service Nothing mem = (Input (pure 0), mem) - -stepSysN :: (RegFileOps r, MemOps m) => Int -> SysG r m -> SysG r m -stepSysN n s - | n <= 0 = s - | otherwise = stepSysN (n - 1) (stepSys s) - --- | The system as it starts up, with @prog@ loaded at 'initPc'. -initSys :: Vec PROG_SIZE Word -> Sys -initSys prog = - Sys - { sysState = Core.init, - sysInput = initInput, - sysMem = mkRAM @PROG_SIZE @RAM_SIZE_BYTES prog - } - -readMemWord :: Address -> MemBytes -> Word -readMemWord = readWord diff --git a/proof-smt/Proof/SMT/Array.hs b/proof/Proof/SMT/Array.hs similarity index 93% rename from proof-smt/Proof/SMT/Array.hs rename to proof/Proof/SMT/Array.hs index 5216d7c..f06519e 100644 --- a/proof-smt/Proof/SMT/Array.hs +++ b/proof/Proof/SMT/Array.hs @@ -40,17 +40,13 @@ module Proof.SMT.Array ) where -import Access -import qualified Clash.Prelude import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Data.Coerce (Coercible, coerce) -import Data.Kind (Type) import qualified Pantomime.BuiltIn as P import qualified Pantomime.Clash as Clash import Memory.Types (MEM_SIZE_BYTES, MemOps (..)) -import RegFile (RegFileOps (..)) +import Core.RegFile (RegFileOps (..)) import Types -import qualified Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) -- | The Haskell-side register file: 32 entries, so the index is exactly a @@ -120,7 +116,7 @@ storeRAE = coerce go -- | The all-zero register file. -- --- 'Proof.Leakage.Simulator.censor' installs this on every state it builds, so +-- 'Proof.Core.Leakage.Simulator.censor' installs this on every state it builds, so -- unlike 'Core.init' it is on the symbolic path and has to be embeddable. -- 'Clash.Prelude.repeat' gives the Haskell semantics; 'zeroRAE' replaces it -- under the term axiom, which is keyed on this name -- hence OPAQUE, for the @@ -133,18 +129,15 @@ zeroRA = RegArr (Clash.Prelude.repeat 0) zeroRAE :: forall arr. (Coercible RegArrSMT arr) => arr zeroRAE = coerce (RegArrSMT (P.aconst 0)) --- | The array-backed register file, wrapped so it fits 'RegFileOps'. --- --- The @f@ parameter is phantom: the embedding must be monomorphic, so the --- element type is fixed to 'Word'. This is a verification-only representation --- and is used at @f ~ Identity@, where 'unAccess' is the identity. -newtype RegArrF (f :: Type -> Type) = RegArrF RegArr +-- | The array-backed register file, wrapped so it fits 'RegFileOps'. A +-- verification-only representation. +newtype RegArrF = RegArrF RegArr instance RegFileOps RegArrF where - lookupRFg idx (RegArrF a) = if idx == 0 then pure 0 else pure (loadRA a idx) + lookupRFg idx (RegArrF a) = if idx == 0 then 0 else loadRA a idx modifyRFg idx v rf@(RegArrF a) | idx == 0 = rf - | otherwise = RegArrF (storeRA a idx (unAccess v)) + | otherwise = RegArrF (storeRA a idx v) -- On the symbolic path; see 'zeroRA'. initRFg = RegArrF zeroRA @@ -262,7 +255,7 @@ instance MemOps MemArr where memReadWord a m = loadM m (a + 3) ++# loadM m (a + 2) ++# loadM m (a + 1) ++# loadM m a - memWriteWord size a w m = + memWrite a size w m = case size of Types.Byte -> put a b0 m Types.Half -> put (a + 1) b1 (put a b0 m) diff --git a/proof-smt/Proof/SMT/Axioms.hs b/proof/Proof/SMT/Axioms.hs similarity index 100% rename from proof-smt/Proof/SMT/Axioms.hs rename to proof/Proof/SMT/Axioms.hs diff --git a/proof-smt/Proof/SMT/Logged.hs b/proof/Proof/SMT/Logged.hs similarity index 100% rename from proof-smt/Proof/SMT/Logged.hs rename to proof/Proof/SMT/Logged.hs diff --git a/proof-smt/Proof/SMT/Sanity.hs b/proof/Proof/SMT/Sanity.hs similarity index 100% rename from proof-smt/Proof/SMT/Sanity.hs rename to proof/Proof/SMT/Sanity.hs diff --git a/src/Access.hs b/src/Access.hs deleted file mode 100644 index fd45459..0000000 --- a/src/Access.hs +++ /dev/null @@ -1,61 +0,0 @@ -{-# LANGUAGE DeriveFunctor #-} - -module Access where - -import Clash.Prelude hiding (Ordering (..), Word, init, lift) -import Data.Functor.Identity -import Data.Maybe -import Prelude hiding (Ordering (..), Word, init, lines, not, undefined, (&&), (||)) - -class (Applicative f) => Access f where - -- | Access the underlying value, regardless of secrecy. - unAccess :: f a -> a - -- | Try to extract a public value. Returns 'Nothing' if the value is secret. - fromPublic :: f a -> Maybe a - -- | Create a secret value if the boolean is True, otherwise create a public value - conditionalSecret :: Bool -> a -> f a - -isPublic :: (Access f) => f a -> Bool -isPublic = isJust . fromPublic - -data PubSec a - = Public a - | Secret a - deriving (Functor, Show, Eq, Generic, NFDataX) - -fromPubSec :: a -> PubSec a -> a -fromPubSec _ (Public a) = a -fromPubSec a Secret {} = a - -instance Access PubSec where - unAccess (Public a) = a - unAccess (Secret a) = a - - fromPublic (Public a) = pure a - fromPublic _ = empty - - conditionalSecret True a = Secret a - conditionalSecret False a = Public a - -instance Applicative PubSec where - pure = Public - (Public f) <*> (Public x) = Public (f x) - f <*> x = Secret (unAccess f (unAccess x)) - -instance Monad PubSec where - (Public x) >>= f = f x - (Secret x) >>= f = Secret $ unAccess $ f x - -instance Access Identity where - unAccess = runIdentity - fromPublic = pure . unAccess - conditionalSecret _ = pure - -censor :: (Access f, Default a) => PubSec a -> f a -censor x = conditionalSecret (not $ isPublic x) (fromPubSec def x) - --- | Run a computation only if the value is public. -noSecrets :: (Access f, Monad m) => f a -> m b -> (a -> m b) -> m b -noSecrets w mb m = case fromPublic w of - Just v -> m v - Nothing -> mb diff --git a/src/Core.hs b/src/Core.hs index d49d4f3..32a9f9e 100644 --- a/src/Core.hs +++ b/src/Core.hs @@ -24,6 +24,7 @@ module Core writeback, CPUM, MemAccess (..), + Request, Control (..), alu, branch, @@ -34,76 +35,60 @@ module Core ) where -import Access import Clash.Prelude hiding (Ordering (..), Word, def, init, lift) import Control.Monad import Control.Monad.RWS -import Data.Maybe (fromMaybe, isJust) -import Instruction hiding (decode) +import Data.Maybe (fromMaybe, isJust, isNothing) +import Core.Instruction hiding (decode) import Memory.Types -import RegFile +import Core.RegFile import Types import Prelude hiding (Ordering (..), Word, init, lines, not, undefined, (&&), (||)) topEntity :: - forall f. - (Access f, Generic (f Word), NFDataX (f Word)) => Clock System -> Reset System -> Enable System -> - Signal System (Input f) -> - Signal System (Output f) -topEntity = exposeClockResetEnable $ mealy (circuit @f @RegFile) (init @f @RegFile) - --- | The input to the CPU. -newtype Input f = Input {inputMem :: f Word} - -deriving instance (Show (f Word)) => Show (Input f) - -deriving instance Generic (Input f) - -deriving instance (Generic (f Word), NFDataX (f Word)) => NFDataX (Input f) - --- | A memory access -data MemAccess f = MemAccess - { -- | Is this an instruction read? - memIsInstr :: Bool, - memAddress :: Address, - memSize :: Size, - -- | The word to be written, if there is one. If set to `Nothing`, then the - -- `MemAccess` is a read. Otherwise, it's a write. - memVal :: Maybe (f Word) - } - -deriving instance (Show (f Word)) => Show (MemAccess f) - -deriving instance Generic (MemAccess f) - -deriving instance (Generic (f Word), NFDataX (f Word)) => NFDataX (MemAccess f) + Signal System Input -> + Signal System Output +topEntity = exposeClockResetEnable $ mealy (circuit @RegFile) (init @RegFile) + +-- | The input to the CPU: memory's answer to the previous request, or 'Nothing' +-- while it is not ready yet. +newtype Input = Input {inputMem :: Maybe Word} + deriving (Show, Eq, Generic, NFDataX) + +-- | A memory access. +data MemAccess + = -- | An instruction fetch: always a whole word. + MemFetch Address + | -- | A data read of the given size. + MemRead Address Size + | -- | A data write of the given size, with the value to write. + MemWrite Address Size Word + deriving (Show, Generic, NFDataX) + +-- | A request on the memory bus, if any, as the memory servers see it. +type Request = Maybe MemAccess -- | The output of the CPU. -newtype Output f = Output +newtype Output = Output { -- | A memory access. - outMem :: Maybe (MemAccess f) + outMem :: Request } + deriving (Show, Generic, NFDataX) -deriving instance (Show (f Word)) => Show (Output f) - -deriving instance Generic (Output f) - -deriving instance (Generic (f Word), NFDataX (f Word)) => NFDataX (Output f) - -instance Semigroup (Output f) where - (<>) :: Output f -> Output f -> Output f +instance Semigroup Output where + (<>) :: Output -> Output -> Output -- When several stages access memory in one cycle, the first one wins. Output mem <> Output mem' = Output (mem <|> mem') -instance Monoid (Output f) where +instance Monoid Output where mempty = Output Nothing -- | CPU halt state -data HaltState = EBreak Address | Syscall Address | SecurityViolation +data HaltState = EBreak Address | Syscall Address deriving (Show, Eq, Generic) instance NFDataX HaltState @@ -113,7 +98,7 @@ instance NFDataX HaltState -- Parameterised over the register-file representation @r@ so that the same -- pipeline can be run on the synthesisable 'RegFile' or, for symbolic -- execution, on the function-backed 'RegFn'. See 'RegFileOps'. -data StateG r f = State +data StateG r = State { -- | Program counter fetch stage. stateFePc :: Address, -- | Program counter decode stage. @@ -127,38 +112,34 @@ data StateG r f = State -- | Instruction memory stage. stateMeInstr :: Instruction, -- | Computation result memory stage. - stateMeRes :: f Word, + stateMeRes :: Word, -- | Address for load and store, memory stage. stateMeAddr :: Address, -- | Instruction writeback stage. stateWbInstr :: Instruction, -- | Computation result writeback stage. - stateWbRes :: f Word, + stateWbRes :: Word, -- | Register file. - stateRegFile :: r f, + stateRegFile :: r, -- | Control/forwarding lines. - stateCtrl :: Control f, + stateCtrl :: Control, -- | CPU halt state. - stateHalt :: Maybe HaltState, - -- | In case of a halt, the address of the next instruction. - stateHaltNextPc :: Address + stateHalt :: Maybe HaltState } -- | The synthesisable state: the register file is a 'Vec'. type State = StateG RegFile -deriving instance (Show (f Word), Show (r f)) => Show (StateG r f) +deriving instance (Show r) => Show (StateG r) -deriving instance (Eq (f Word), Eq (r f)) => Eq (StateG r f) +deriving instance (Eq r) => Eq (StateG r) -deriving instance Generic (StateG r f) +deriving instance Generic (StateG r) -deriving anyclass instance - (Generic (f Word), NFDataX (f Word), Generic (r f), NFDataX (r f)) => - NFDataX (StateG r f) +deriving anyclass instance (Generic r, NFDataX r) => NFDataX (StateG r) -- | Control lines. -data Control f = Control +data Control = Control { -- | Stores `stateDePc` when the instruction in the `decode` stage has -- a load hazard with the instruction in the `execute` stage. ctrlDeLoadHazard :: Maybe Address, @@ -181,36 +162,26 @@ data Control f = Control ctrlMeStoreAddrSize :: Maybe (Address, Size), -- | Forwards the `rd` register from the `memory` stage to the `execute` -- stage. - ctrlMeRegFwd :: Maybe (RegIdx, f Word), + ctrlMeRegFwd :: Maybe (RegIdx, Word), -- | Forwards the `rd` register from the `writeback` stage to the `execute` -- stage. - ctrlWbRegFwd :: Maybe (RegIdx, f Word) + ctrlWbRegFwd :: Maybe (RegIdx, Word), + -- | True when memory has not answered yet: the pipeline holds. + ctrlMemNotReady :: Bool } + deriving (Show, Eq, Generic, NFDataX) -deriving instance (Show (f Word)) => Show (Control f) - -deriving instance (Eq (f Word)) => Eq (Control f) - -deriving instance Generic (Control f) - -deriving anyclass instance (Generic (f Word), NFDataX (f Word)) => NFDataX (Control f) - -type CPUM r f = RWS (Input f) (Output f) (StateG r f) +type CPUM r = RWS Input Output (StateG r) -setLines :: (MonadState (StateG r f) m) => (Control f -> Control f) -> m () +setLines :: (MonadState (StateG r) m) => (Control -> Control) -> m () setLines f = modify $ \s -> s {stateCtrl = f (stateCtrl s)} --- | No secrets here, buddy: unwrap a word. If it's public, we gucci. If it's --- private, die. -noSecrets' :: (Access f) => f a -> b -> (a -> CPUM r f b) -> CPUM r f b -noSecrets' w a = noSecrets w (setSecurityViolation >> pure a) - -- | Run the CPU for one step. -circuit :: forall f r. (Access f, RegFileOps r) => StateG r f -> Input f -> (StateG r f, Output f) +circuit :: forall r. (RegFileOps r) => StateG r -> Input -> (StateG r, Output) circuit = flip $ execRWS pipe -- | The CPU, composed of each stage. -pipe :: (Access f, RegFileOps r) => CPUM r f () +pipe :: (RegFileOps r) => CPUM r () pipe = do -- The control lines need to be reset every tick. modify $ \s -> s {stateCtrl = initCtrl} @@ -219,11 +190,14 @@ pipe = do execute decode fetch + -- The lines only carry values within a tick, so none of them survives it: + -- a cycle in which the pipeline holds leaves the state exactly as it was. + modify $ \s -> s {stateCtrl = initCtrl} -initInput :: (Access f) => Input f -initInput = Input (pure 0) +initInput :: Input +initInput = Input (Just 0) -initAt :: (Access f) => Address -> r f -> StateG r f +initAt :: Address -> r -> StateG r initAt pc rf = State { stateFePc = pc, @@ -232,21 +206,20 @@ initAt pc rf = stateExPc = 0, stateExInstr = Nop FirstCycle, stateMeInstr = Nop FirstCycle, - stateMeRes = pure 0, + stateMeRes = 0, stateMeAddr = 0, stateWbInstr = Nop FirstCycle, - stateWbRes = pure 0, + stateWbRes = 0, stateRegFile = rf, stateCtrl = initCtrl, - stateHalt = Nothing, - stateHaltNextPc = 0 + stateHalt = Nothing } -init :: forall f r. (Access f, RegFileOps r) => StateG r f +init :: forall r. (RegFileOps r) => StateG r init = initAt initPc initRFg -- | Initial control lines. -initCtrl :: Control f +initCtrl :: Control initCtrl = Control { ctrlDeLoadHazard = Nothing, @@ -257,17 +230,21 @@ initCtrl = ctrlMeMemInstr = False, ctrlMeStoreAddrSize = Nothing, ctrlMeRegFwd = Nothing, - ctrlWbRegFwd = Nothing + ctrlWbRegFwd = Nothing, + ctrlMemNotReady = False } --- | Set security violation flag. -setSecurityViolation :: CPUM r f () -setSecurityViolation = - modify $ \s -> s {stateHalt = Just SecurityViolation} - --- | Fetch stage. -fetch :: CPUM r f () +-- | Fetch stage. Holds while memory has not answered (see 'writeback'), like the +-- other stages before writeback: a stall then leaves every pipeline register +-- as it was. +fetch :: CPUM r () fetch = do + notReady <- gets (ctrlMemNotReady . stateCtrl) + unless notReady fetchFresh + +-- | Fetch stage, in a cycle where the pipeline advances. +fetchFresh :: CPUM r () +fetchFresh = do pc <- gets stateFePc ctrl <- gets stateCtrl @@ -296,18 +273,24 @@ fetch = do stateDeExpInstr = not stall } --- | Decode stage. -decode :: (Access f) => CPUM r f () +-- | Decode stage. Holds while memory has not answered (see 'writeback'). +decode :: CPUM r () decode = do + notReady <- gets (ctrlMemNotReady . stateCtrl) + unless notReady decodeFresh + +-- | Decode stage, in a cycle where the pipeline advances. +decodeFresh :: CPUM r () +decodeFresh = do input <- ask pc <- gets stateDePc expInstr <- gets stateDeExpInstr ctrl <- gets stateCtrl - ir <- - if expInstr - then noSecrets' (inputMem input) (Nop Halted) (pure . decode') - else pure $ Nop MemoryBusBusy + let ir = + if expInstr + then maybe (Nop NoInstruction) decode' (inputMem input) + else Nop NoInstruction let halted = ctrlExInstr ctrl == Just (Nop Halted) let call_current_cycle = maybe False isCall (ctrlExInstr ctrl) @@ -355,102 +338,99 @@ decode = do when (ir' == Nop LoadHazardFirstCycle) $ do setLines $ \c -> c {ctrlDeLoadHazard = Just pc} --- | Execute stage. -execute :: forall f r. (Access f, RegFileOps r) => CPUM r f () +-- | Execute stage. Holds while memory has not answered (see 'writeback'). +execute :: forall r. (RegFileOps r) => CPUM r () execute = do + notReady <- gets (ctrlMemNotReady . stateCtrl) + unless notReady executeFresh + +-- | Execute stage, in a cycle where the pipeline advances. +executeFresh :: forall r. (RegFileOps r) => CPUM r () +executeFresh = do ir <- gets stateExInstr -- Default values. modify $ \s -> s { stateMeInstr = ir, - stateMeRes = pure 0, + stateMeRes = 0, stateMeAddr = 0 } setLines $ \c -> c {ctrlExInstr = Just ir} case ir of - Instruction.RType op _ rs1 rs2 -> do + Core.Instruction.RType op _ rs1 rs2 -> do r1 <- getFirstArg rs1 r2 <- getSecondArg rs2 let res = alu op r1 r2 modify $ \s -> s {stateMeRes = res} - Instruction.IType (Arith op) _ rs1 imm -> do + Core.Instruction.IType (Arith op) _ rs1 imm -> do r1 <- getFirstArg rs1 let imm' = signExtend imm - let res = alu op r1 (pure imm') + let res = alu op r1 imm' modify $ \s -> s {stateMeRes = res} - Instruction.IType (Load _ _) _ rs1 imm -> do + Core.Instruction.IType (Load _ _) _ rs1 imm -> do r1 <- getFirstArg rs1 let imm' = signExtend imm - let res = alu ADD r1 (pure imm') - noSecrets' res () $ \res' -> do - modify $ \s -> s {stateMeAddr = unpack res'} - Instruction.SType size imm rs1 rs2 -> do + let res = alu ADD r1 imm' + modify $ \s -> s {stateMeAddr = unpack res} + Core.Instruction.SType size imm rs1 rs2 -> do r1 <- getFirstArg rs1 r2 <- getSecondArg rs2 let imm' = signExtend imm - let res = alu ADD r1 (pure imm') - modify $ \s -> s {stateMeRes = r2} - noSecrets' res () $ \res' -> do - modify $ \s -> s {stateMeAddr = unpack res'} - setLines $ \c -> c {ctrlExStoreAddrSize = Just (unpack res', size)} - Instruction.BType cmp imm rs1 rs2 -> do + let res = alu ADD r1 imm' + modify $ \s -> s {stateMeRes = r2, stateMeAddr = unpack res} + setLines $ \c -> c {ctrlExStoreAddrSize = Just (unpack res, size)} + Core.Instruction.BType cmp imm rs1 rs2 -> do r1 <- getFirstArg rs1 r2 <- getSecondArg rs2 pc <- gets $ pack . stateExPc - let doBranch = branch cmp r1 r2 - noSecrets' doBranch () $ \doBranch' -> - when doBranch' $ do - let imm' = signExtend imm - let branchAddr = alu ADD (pure pc) (pure imm') :: f Word - setLines $ \c -> - c {ctrlExJumpAddr = fromPublic $ unpack <$> branchAddr} - Instruction.JType _ imm -> do + when (branch cmp r1 r2) $ do + let imm' = signExtend imm + let branchAddr = alu ADD pc imm' + setLines $ \c -> c {ctrlExJumpAddr = Just (unpack branchAddr)} + Core.Instruction.JType _ imm -> do pc <- gets $ pack . stateExPc - let res = alu ADD (pure pc) (pure 4) + let res = alu ADD pc 4 modify $ \s -> s {stateMeRes = res} let imm' = signExtend imm - let jumpAddr = alu ADD (pure pc) (pure imm') :: f Word - setLines $ \c -> - c {ctrlExJumpAddr = fromPublic $ unpack <$> jumpAddr} - Instruction.IType Jump _ rs1 imm -> do + let jumpAddr = alu ADD pc imm' + setLines $ \c -> c {ctrlExJumpAddr = Just (unpack jumpAddr)} + Core.Instruction.IType Jump _ rs1 imm -> do r1 <- getFirstArg rs1 pc <- gets $ pack . stateExPc - let res = alu ADD (pure pc) (pure 4) + let res = alu ADD pc 4 modify $ \s -> s {stateMeRes = res} - noSecrets' r1 () $ \r1' -> do - let imm' = signExtend imm - let jumpAddr = alu ADD (pure r1') (pure imm') :: f Word - setLines $ \c -> - c {ctrlExJumpAddr = fromPublic $ unpack <$> jumpAddr} - Instruction.UType base _ imm -> do + let imm' = signExtend imm + let jumpAddr = alu ADD r1 imm' + setLines $ \c -> c {ctrlExJumpAddr = Just (unpack jumpAddr)} + Core.Instruction.UType base _ imm -> do base' <- case base of Zero -> pure 0 PC -> gets $ pack . stateExPc let imm' = imm ++# (0 :: BitVector 12) - let res = alu ADD (pure base') (pure imm') + let res = alu ADD base' imm' modify $ \s -> s {stateMeRes = res} - Instruction.IType (Env Call) _ _ _ -> do + Core.Instruction.IType (Env Call) _ _ _ -> do pc <- gets stateExPc - modify $ \s -> s {stateHaltNextPc = pc + 4} - Instruction.IType (Env Break) _ _ _ -> do + modify $ \s -> s {stateMeRes = pack $ pc + 4} + Core.Instruction.IType (Env Break) _ _ _ -> do pc <- gets stateExPc - modify $ \s -> s {stateHaltNextPc = pc + 4} - Instruction.Nop _ -> pure () + modify $ \s -> s {stateMeRes = pack $ pc + 4} + Core.Instruction.Nop _ -> pure () where - getFirstArg :: RegIdx -> CPUM r f (f Word) + getFirstArg :: RegIdx -> CPUM r Word getFirstArg idx = do rf <- gets stateRegFile regWithFwd idx (lookupRFg idx rf) - getSecondArg :: RegIdx -> CPUM r f (f Word) + getSecondArg :: RegIdx -> CPUM r Word getSecondArg idx = do rf <- gets stateRegFile regWithFwd idx (lookupRFg idx rf) - regWithFwd :: RegIdx -> f Word -> CPUM r f (f Word) + regWithFwd :: RegIdx -> Word -> CPUM r Word regWithFwd idx def = do ctrl <- gets stateCtrl let pick line = do @@ -459,18 +439,18 @@ execute = do pure fwdVal pure $ fromMaybe def (pick ctrlMeRegFwd <|> pick ctrlWbRegFwd) -alu :: (Access f) => Arith -> f Word -> f Word -> f Word +alu :: Arith -> Word -> Word -> Word alu op lhs rhs = case op of - ADD -> (+) <$> lhs <*> rhs - SUB -> (-) <$> lhs <*> rhs - XOR -> (.^.) <$> lhs <*> rhs - OR -> (.|.) <$> lhs <*> rhs - AND -> (.&.) <$> lhs <*> rhs - SLL -> sllWord <$> lhs <*> (shiftBits <$> rhs) - SRL -> srlWord <$> lhs <*> (shiftBits <$> rhs) - SRA -> sraWord <$> lhs <*> (shiftBits <$> rhs) - SLT -> set <$> ((<) <$> (sign <$> lhs) <*> (sign <$> rhs)) - SLTU -> set <$> ((<) <$> lhs <*> rhs) + ADD -> lhs + rhs + SUB -> lhs - rhs + XOR -> lhs .^. rhs + OR -> lhs .|. rhs + AND -> lhs .&. rhs + SLL -> sllWord lhs (shiftBits rhs) + SRL -> srlWord lhs (shiftBits rhs) + SRA -> sraWord lhs (shiftBits rhs) + SLT -> set (sign lhs < sign rhs) + SLTU -> set (lhs < rhs) where shiftBits = slice d4 d0 sign = unpack @(Signed 32) @@ -509,20 +489,26 @@ srlWord x n = shiftR x (fromIntegral n) sraWord :: Word -> BitVector 5 -> Word sraWord x n = pack (shiftR (unpack x :: Signed 32) (fromIntegral n)) -branch :: (Access f) => Comparison -> f Word -> f Word -> f Bool +branch :: Comparison -> Word -> Word -> Bool branch op lhs rhs = case op of - EQ -> (==) <$> lhs <*> rhs - NE -> (/=) <$> lhs <*> rhs - LT -> (<) <$> (sign <$> lhs) <*> (sign <$> rhs) - GE -> (>=) <$> (sign <$> lhs) <*> (sign <$> rhs) - LTU -> (<) <$> lhs <*> rhs - GEU -> (>=) <$> lhs <*> rhs + EQ -> lhs == rhs + NE -> lhs /= rhs + LT -> sign lhs < sign rhs + GE -> sign lhs >= sign rhs + LTU -> lhs < rhs + GEU -> lhs >= rhs where sign = unpack @(Signed 32) --- | Memory stage. -memory :: CPUM r f () +-- | Memory stage. Holds while memory has not answered (see 'writeback'). +memory :: CPUM r () memory = do + notReady <- gets (ctrlMemNotReady . stateCtrl) + unless notReady memoryFresh + +-- | Memory stage, in a cycle where the pipeline advances. +memoryFresh :: CPUM r () +memoryFresh = do ir <- gets stateMeInstr res <- gets stateMeRes addr <- gets stateMeAddr @@ -533,102 +519,93 @@ memory = do setLines $ \c -> c {ctrlMeRegFwd = Nothing} case ir of - Instruction.RType _ rd _ _ -> + Core.Instruction.RType _ rd _ _ -> setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} - Instruction.IType (Arith _) rd _ _ -> + Core.Instruction.IType (Arith _) rd _ _ -> setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} - Instruction.IType (Load size _) _ _ _ -> do + Core.Instruction.IType (Load size _) _ _ _ -> do setLines $ \c -> c {ctrlMeMemInstr = True} readRAM addr size - Instruction.SType size _ _ _ -> do + Core.Instruction.SType size _ _ _ -> do setLines $ \c -> c {ctrlMeMemInstr = True, ctrlMeStoreAddrSize = Just (addr, size)} writeRAM addr size res - Instruction.JType rd _ -> + Core.Instruction.JType rd _ -> setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} - Instruction.IType Jump rd _ _ -> + Core.Instruction.IType Jump rd _ _ -> setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} - Instruction.UType _ rd _ -> + Core.Instruction.UType _ rd _ -> setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} _ -> pure () --- | Writeback stage. -writeback :: forall f r. (Access f, RegFileOps r) => CPUM r f () +-- | Writeback stage. While memory has not answered ('inputMem' is 'Nothing'), +-- the instruction waits, and raises 'ctrlMemNotReady' so that the other stages +-- hold too: the whole pipeline keeps its state and makes no request, whatever +-- the request memory delays. Otherwise the instruction completes +-- ('writebackFresh'). +writeback :: forall r. (RegFileOps r) => CPUM r () writeback = do input <- asks inputMem + + if isNothing input + then setLines $ \c -> c {ctrlMemNotReady = True} + else writebackFresh + +-- | Writeback stage, in a cycle where the instruction in it completes. +writebackFresh :: forall r. (RegFileOps r) => CPUM r () +writebackFresh = do ir <- gets stateWbInstr res <- gets stateWbRes case ir of - Instruction.RType _ rd _ _ -> do + Core.Instruction.RType _ rd _ _ -> do setLines $ \c -> c {ctrlWbRegFwd = Just (rd, res)} writeRF rd res - Instruction.IType (Arith _) rd _ _ -> do + Core.Instruction.IType (Arith _) rd _ _ -> 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 - Instruction.JType rd _ -> do + Core.Instruction.IType (Load size sign) rd _ _ -> do + input <- asks inputMem + case input of + -- this case should not arise + Nothing -> pure () + Just w -> do + let val = loadExtend size sign w + setLines $ \c -> c {ctrlWbRegFwd = Just (rd, val)} + writeRF rd val + Core.Instruction.JType rd _ -> do setLines $ \c -> c {ctrlWbRegFwd = Just (rd, res)} writeRF rd res - Instruction.IType Jump rd _ _ -> do + Core.Instruction.IType Jump rd _ _ -> do setLines $ \c -> c {ctrlWbRegFwd = Just (rd, res)} writeRF rd res - Instruction.UType _ rd _ -> do + Core.Instruction.UType _ rd _ -> do setLines $ \c -> c {ctrlWbRegFwd = Just (rd, res)} writeRF rd res - Instruction.IType (Env Call) _ _ _ -> do - cont <- gets stateHaltNextPc - modify $ \s -> s {stateHalt = Just (Syscall cont), stateHaltNextPc = 0} - Instruction.IType (Env Break) _ _ _ -> do - cont <- gets stateHaltNextPc - modify $ \s -> s {stateHalt = Just (EBreak cont), stateHaltNextPc = 0} + Core.Instruction.IType (Env Call) _ _ _ -> do + modify $ \s -> s {stateHalt = Just (Syscall $ unpack res)} + Core.Instruction.IType (Env Break) _ _ _ -> do + modify $ \s -> s {stateHalt = Just (EBreak $ unpack res)} _ -> setLines $ \c -> c {ctrlWbRegFwd = Nothing} where - writeRF :: RegIdx -> f Word -> CPUM r f () + writeRF :: RegIdx -> Word -> CPUM r () writeRF idx val = modify $ \s -> s {stateRegFile = modifyRFg idx val (stateRegFile s)} -readPC :: (MonadWriter (Output f) m) => Address -> m () +readPC :: (MonadWriter Output m) => Address -> m () readPC addr = tell $ - (mempty :: Output f) - { outMem = - pure $ - MemAccess - { memIsInstr = True, - memAddress = addr, - memSize = Word, - memVal = Nothing - } - } + (mempty :: Output) + { outMem = pure $ MemFetch addr } -readRAM :: (MonadWriter (Output f) m) => Address -> Size -> m () +readRAM :: (MonadWriter Output m) => Address -> Size -> m () readRAM addr size = tell $ - (mempty :: Output f) - { outMem = - pure $ - MemAccess - { memIsInstr = False, - memAddress = addr, - memSize = size, - memVal = Nothing - } - } + (mempty :: Output) + { outMem = pure $ MemRead addr size } -writeRAM :: (MonadWriter (Output f) m) => Address -> Size -> f Word -> m () +writeRAM :: (MonadWriter Output m) => Address -> Size -> Word -> m () writeRAM addr size val = tell $ - (mempty :: Output f) - { outMem = - pure $ - MemAccess - { memIsInstr = False, - memAddress = addr, - memSize = size, - memVal = Just val - } - } + (mempty :: Output) + { outMem = pure $ MemWrite addr size val } diff --git a/src/ISA.hs b/src/Core/ISA.hs similarity index 77% rename from src/ISA.hs rename to src/Core/ISA.hs index ead78c6..8ae7a67 100644 --- a/src/ISA.hs +++ b/src/Core/ISA.hs @@ -5,18 +5,18 @@ -- | The ISA specification: what each instruction means, and how the -- architectural state evolves. -- --- Two halves, both semantics. 'interp' turns an 'Instruction.Instruction' into +-- Two halves, both semantics. 'interp' turns an 'Core.Instruction.Instruction' into -- an @'Instr' 'Func'@ -- the effect it denotes -- and 'apply' evaluates one of -- those 'Func's against the two source-register values and the PC. On top of -- that, 'isaStep' says how the @(isaPc, isaRegFile, isaMem)@ triple moves. -- -- The architectural state is parameterised over the register-file and memory -- representations because the @Vec@-backed ones cannot be symbolically --- executed; see 'RegFile.RegFileOps' and 'Memory.Types.MemOps'. +-- executed; see 'Core.RegFile.RegFileOps' and 'Memory.Types.MemOps'. -- -- This is specification, not proof machinery. The refinement proof is stated -- against it, so it must not depend on anything the proof defines. -module ISA +module Core.ISA ( Func, Done (..), apply, @@ -37,14 +37,12 @@ module ISA ) where -import Access import Clash.Prelude hiding (Const, Log, Ordering (..), Word, def, init, lift, log) import Core hiding (Syscall) -import Data.Functor.Identity -import Instruction (Instruction, Sign, decode', loadExtend) -import qualified Instruction +import Core.Instruction (Instruction, Sign, decode', loadExtend) +import qualified Core.Instruction import Memory.Types (MemBytes, MemOps (..)) -import RegFile +import Core.RegFile import Types import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (||)) @@ -118,46 +116,46 @@ instance DepReg (Instr Func) where deps Nop = (empty, empty) deps Syscall = (pure 17, empty) -interp :: Instruction.Instruction -> Instr Func +interp :: Core.Instruction.Instruction -> Instr Func interp instr - | Instruction.isBreak instr = Break + | Core.Instruction.isBreak instr = Break | otherwise = case instr of - Instruction.RType op rd r1 r2 -> - Reg rd $ binaryF r1 r2 $ \w1 w2 -> unAccess $ alu op (Identity w1) (Identity w2) - Instruction.IType iop rd r1 imm -> + Core.Instruction.RType op rd r1 r2 -> + Reg rd $ binaryF r1 r2 $ \w1 w2 -> alu op w1 w2 + Core.Instruction.IType iop rd r1 imm -> let op = case iop of - Instruction.Arith op' -> op' - _ -> Instruction.ADD - alu_res = unaryF r1 $ \w -> unAccess $ alu op (Identity w) (Identity $ signExtend imm) + Core.Instruction.Arith op' -> op' + _ -> Core.Instruction.ADD + alu_res = unaryF r1 $ \w -> alu op w (signExtend imm) in case iop of - Instruction.Arith {} -> + Core.Instruction.Arith {} -> Reg rd alu_res - Instruction.Load size sign -> + Core.Instruction.Load size sign -> Load size sign rd $ bitCoerce <$> alu_res - Instruction.Jump -> + Core.Instruction.Jump -> Jump rd (pcF (bitCoerce . (+ 4))) $ bitCoerce <$> alu_res - Instruction.Env Instruction.Break -> + Core.Instruction.Env Core.Instruction.Break -> Break - Instruction.Env Instruction.Call -> + Core.Instruction.Env Core.Instruction.Call -> Syscall - Instruction.SType size imm r1 r2 -> do + Core.Instruction.SType size imm r1 r2 -> do let addr_comp = unpack <$> unaryF r1 (+ signExtend imm) in Store size addr_comp r2 - Instruction.BType cmp imm r1 r2 -> - let branched_comp = binaryF r1 r2 $ \w1 w2 -> unAccess $ branch cmp (Identity w1) (Identity w2) + Core.Instruction.BType cmp imm r1 r2 -> + let branched_comp = binaryF r1 r2 $ \w1 w2 -> branch cmp w1 w2 addr_comp = pcF (+ bitCoerce (signExtend imm)) in Branch branched_comp addr_comp - Instruction.UType Instruction.Zero rd imm -> + Core.Instruction.UType Core.Instruction.Zero rd imm -> let imm' = imm ++# (0 :: BitVector 12) in Reg rd $ constF imm' - Instruction.UType Instruction.PC rd imm -> do + Core.Instruction.UType Core.Instruction.PC rd imm -> do let imm' = imm ++# (0 :: BitVector 12) in Reg rd $ pcF $ \pc -> bitCoerce pc + imm' - Instruction.JType rd imm -> + Core.Instruction.JType rd imm -> Jump rd (pcF (bitCoerce . (+ 4))) $ pcF (+ bitCoerce (signExtend imm)) - Instruction.Nop _ -> Nop + Core.Instruction.Nop _ -> Nop where constF :: a -> Func a constF a = @@ -190,16 +188,16 @@ interp instr -- | Architectural state: the ISA-visible triple. data IsaStateG r m = IsaState { isaPc :: PC, - isaRegFile :: r Identity, + isaRegFile :: r, isaMem :: m } -- | The concrete architectural state the QuickCheck harness uses. type IsaState = IsaStateG RegFile MemBytes -deriving instance (Show (r Identity), Show m) => Show (IsaStateG r m) +deriving instance (Show r, Show m) => Show (IsaStateG r m) -deriving instance (Eq (r Identity), Eq m) => Eq (IsaStateG r m) +deriving instance (Eq r, Eq m) => Eq (IsaStateG r m) -- | The result of one architectural step. 'IsaHalted' covers @ebreak@ and -- @ecall@, which is where 'Core' parks in a 'Core.HaltState'. @@ -209,9 +207,9 @@ data StepG r m type Step = StepG RegFile MemBytes -deriving instance (Show (r Identity), Show m) => Show (StepG r m) +deriving instance (Show r, Show m) => Show (StepG r m) -deriving instance (Eq (r Identity), Eq m) => Eq (StepG r m) +deriving instance (Eq r, Eq m) => Eq (StepG r m) -- | The instruction the ISA would execute next. isaInstrAt :: (MemOps m) => IsaStateG r m -> Instruction @@ -235,18 +233,18 @@ isaStepDecoded :: isaStepDecoded ir st@(IsaState pc rf mem) = case instr of Reg rd f -> - Next st {isaPc = pc + 4, isaRegFile = modifyRFg rd (pure (ap f)) rf} + Next st {isaPc = pc + 4, isaRegFile = modifyRFg rd (ap f) rf} Load size sign rd f -> let val = loadExtend size sign (memReadWord (ap f) mem) - in Next st {isaPc = pc + 4, isaRegFile = modifyRFg rd (pure val) rf} + in Next st {isaPc = pc + 4, isaRegFile = modifyRFg rd val rf} Jump rd link target -> Next st { isaPc = ap target, - isaRegFile = modifyRFg rd (pure (bitCoerce (ap link))) rf + isaRegFile = modifyRFg rd (bitCoerce (ap link)) rf } Store size addr rs2 -> - Next st {isaPc = pc + 4, isaMem = memWriteWord size (ap addr) (reg (Just rs2)) mem} + Next st {isaPc = pc + 4, isaMem = memWrite (ap addr) size (reg (Just rs2)) mem} Branch cond target -> Next st {isaPc = if ap cond then ap target else pc + 4} Nop -> Next st {isaPc = pc + 4} @@ -255,7 +253,7 @@ isaStepDecoded ir st@(IsaState pc rf mem) = where instr = interp ir - reg = maybe 0 (\idx -> runIdentity (lookupRFg idx rf)) + reg = maybe 0 (\idx -> lookupRFg idx rf) -- 'Func' is evaluated against the values of its two dependency -- registers and the PC, exactly as 'apply' prescribes. diff --git a/src/Instruction.hs b/src/Core/Instruction.hs similarity index 92% rename from src/Instruction.hs rename to src/Core/Instruction.hs index 69bf94f..c5f39bc 100644 --- a/src/Instruction.hs +++ b/src/Core/Instruction.hs @@ -1,7 +1,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} -module Instruction +module Core.Instruction ( Instruction (..), Reason4Stall (..), nop, @@ -25,6 +25,7 @@ module Instruction storeHazard, loadHazard, isMemInstr, + isLoad, loadExtend, ) where @@ -35,7 +36,6 @@ import Data.Binary (Binary) import Data.Maybe (fromMaybe, isJust) import Types import Prelude hiding (Ordering (..), Word, break, undefined, (&&), (||)) -import Pantomime.Expr (Literal(Bool)) -- | All arithmetic and logic operations. data Arith @@ -117,8 +117,9 @@ data Reason4Stall StoreHazardFirstCycle | -- | Second instruction discarded because of a store hazard. StoreHazardSecondCycle - | -- | No instruction read because of memory bus overload. - MemoryBusBusy + | -- | No instruction this cycle: the fetch stage did not fetch, because the + -- memory stage used the bus. + NoInstruction | -- | Failed to decode an instruction. DecodeFail | -- | First cycle. @@ -402,32 +403,32 @@ encode instr = -- | Get the destination register of an instruction, if any. getRd :: (Alternative f) => Instruction -> f RegIdx getRd = \case - Instruction.RType _ rd _ _ -> pure rd - Instruction.IType (Env Call) _ _ _ -> pure 10 -- a0 - Instruction.IType _ rd _ _ -> pure rd - Instruction.UType _ rd _ -> pure rd - Instruction.JType rd _ -> pure rd - Instruction.Nop _ -> pure 0 + Core.Instruction.RType _ rd _ _ -> pure rd + Core.Instruction.IType (Env Call) _ _ _ -> pure 10 -- a0 + Core.Instruction.IType _ rd _ _ -> pure rd + Core.Instruction.UType _ rd _ -> pure rd + Core.Instruction.JType rd _ -> pure rd + Core.Instruction.Nop _ -> pure 0 _ -> empty -- | Get the first source register of an instruction, if any. getRs1 :: (Alternative f) => Instruction -> f RegIdx getRs1 = \case - Instruction.RType _ _ rs1 _ -> pure rs1 - Instruction.IType (Env Call) _ _ _ -> pure 17 -- a7 - Instruction.IType _ _ rs1 _ -> pure rs1 - Instruction.SType _ _ rs1 _ -> pure rs1 - Instruction.BType _ _ rs1 _ -> pure rs1 - Instruction.Nop _ -> pure 0 + Core.Instruction.RType _ _ rs1 _ -> pure rs1 + Core.Instruction.IType (Env Call) _ _ _ -> pure 17 -- a7 + Core.Instruction.IType _ _ rs1 _ -> pure rs1 + Core.Instruction.SType _ _ rs1 _ -> pure rs1 + Core.Instruction.BType _ _ rs1 _ -> pure rs1 + Core.Instruction.Nop _ -> pure 0 _ -> empty -- | Get the second source register of an instruction, if any. getRs2 :: (Alternative f) => Instruction -> f RegIdx getRs2 = \case - Instruction.RType _ _ _ rs2 -> pure rs2 - Instruction.SType _ _ _ rs2 -> pure rs2 - Instruction.BType _ _ _ rs2 -> pure rs2 - Instruction.Nop _ -> pure 0 + Core.Instruction.RType _ _ _ rs2 -> pure rs2 + Core.Instruction.SType _ _ _ rs2 -> pure rs2 + Core.Instruction.BType _ _ _ rs2 -> pure rs2 + Core.Instruction.Nop _ -> pure 0 _ -> empty isBreak :: Instruction -> Bool @@ -449,6 +450,12 @@ isMemInstr (IType Load {} _ _ _) = True isMemInstr (SType {}) = True isMemInstr _ = False +-- | Loads: the instructions whose result arrives over the memory bus in the +-- writeback stage. +isLoad :: Instruction -> Bool +isLoad (IType Load {} _ _ _) = True +isLoad _ = False + break :: Instruction break = IType (Env Break) 0 0 0 diff --git a/src/RegFile.hs b/src/Core/RegFile.hs similarity index 69% rename from src/RegFile.hs rename to src/Core/RegFile.hs index e2e06ab..13bf6af 100644 --- a/src/RegFile.hs +++ b/src/Core/RegFile.hs @@ -2,7 +2,7 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} -module RegFile +module Core.RegFile ( RegFile (..), initRF, lookupRF, @@ -13,54 +13,49 @@ module RegFile ) where -import Access import Clash.Prelude hiding (Word, zip) import Pretty import Types import Prelude hiding (Ordering (..), Word, repeat, undefined, (!!), (++)) import qualified Prelude as P -import Numeric (showHex) import Data.List (intercalate) -- | Register file used in this core. -newtype RegFile f = RegFile (Vec ((2 ^ 5) - 1) (f Word)) - -deriving instance (Generic (f Word), NFDataX (f Word)) => Generic (RegFile f) -deriving instance (Generic (f Word), NFDataX (f Word)) => NFDataX (RegFile f) -deriving instance (Eq (f Word)) => Eq (RegFile f) +newtype RegFile = RegFile (Vec ((2 ^ 5) - 1) Word) + deriving (Eq, Generic, NFDataX) regIdxName :: RegIdx -> String regIdxName idx = ["zero", "ra", "sp", "gp", "tp", "t0", "t1", "t2", "s0", "s1", "a0", "a1", "a2", "a3", "a4", "a5", "a6", "a7", "s2", "s3", "s4", "s5", "s6", "s7", "s8", "s9", "s10", "s11", "t3", "t4", "t5", "t6"] P.!! (fromIntegral idx) -instance (Show (f Word)) => Show (RegFile f) where +instance Show RegFile where show (RegFile rf) = intercalate ", " $ Prelude.zipWith (\i x -> "%" <> regIdxName i <> "=" <> show x) [1..] (toList rf) -instance (Access f, Pretty (f Word)) => Pretty (RegFile f) where +instance Pretty RegFile where pretty (RegFile rf) = vcat $ uncurry line <$> P.zip [0 :: Int ..] rf' where line idx word = "%r" <> pretty idx <+> "=" <+> pretty word - rf' = toList $ singleton (pure 0) ++ rf + rf' = toList $ singleton 0 ++ rf -initRF :: (Access f) => RegFile f -initRF = RegFile $ repeat (pure 0) +initRF :: RegFile +initRF = RegFile $ repeat 0 -- | Lookup a register from the register file. -lookupRF :: (Access f) => RegIdx -> RegFile f -> f Word -lookupRF 0 _ = pure 0 +lookupRF :: RegIdx -> RegFile -> Word +lookupRF 0 _ = 0 lookupRF idx (RegFile rf) = rf !! (idx - 1) -- | Modify a register in the register file. -modifyRF :: (Access f) => RegIdx -> f Word -> RegFile f -> RegFile f +modifyRF :: RegIdx -> Word -> RegFile -> RegFile modifyRF idx val (RegFile rf) = case idx of 0 -> RegFile rf _ -> RegFile $ replace (idx - 1) val rf -- | Censor all registers in the register file. -censorRF :: (Access f) => RegFile f -> RegFile f +censorRF :: RegFile -> RegFile censorRF _ = initRF -- | The operations the pipeline needs from a register file. @@ -70,9 +65,9 @@ censorRF _ = initRF -- function) which is what symbolic execution can actually handle. See -- "Induction" for why the 'Vec' one cannot be symbolically executed. class RegFileOps r where - lookupRFg :: (Access f) => RegIdx -> r f -> f Word - modifyRFg :: (Access f) => RegIdx -> f Word -> r f -> r f - initRFg :: (Access f) => r f + lookupRFg :: RegIdx -> r -> Word + modifyRFg :: RegIdx -> Word -> r -> r + initRFg :: r instance RegFileOps RegFile where lookupRFg = lookupRF @@ -85,10 +80,10 @@ instance RegFileOps RegFile where -- must never reach 'Core.topEntity'. It exists purely so that reads become -- applications and writes become lambdas, both of which the symbolic executor -- handles natively. -newtype RegFn f = RegFn (RegIdx -> f Word) +newtype RegFn = RegFn (RegIdx -> Word) instance RegFileOps RegFn where - lookupRFg idx (RegFn g) = if idx == 0 then pure 0 else g idx + lookupRFg idx (RegFn g) = if idx == 0 then 0 else g idx modifyRFg idx v rf@(RegFn g) = if idx == 0 then rf else RegFn (\j -> if j == idx then v else g j) - initRFg = RegFn (const (pure 0)) + initRFg = RegFn (const 0) diff --git a/src/Elf/ElfLoader.hs b/src/Elf/ElfLoader.hs index 82369bf..24cf652 100644 --- a/src/Elf/ElfLoader.hs +++ b/src/Elf/ElfLoader.hs @@ -9,7 +9,6 @@ module Elf.ElfLoader , getElfSegments ) where -import Access import Clash.Explicit.Prelude (Unsigned, bitCoerce, zeroExtend) import Clash.Explicit.Prelude.Safe ((.&.)) import Control.Monad (forM_, forM) @@ -23,7 +22,7 @@ import Data.Elf.Constants import Data.Elf.Headers import Data.Word import Types -import RegFile (modifyRF) +import Core.RegFile (modifyRF) import Memory.Types import Util import Prelude hiding (Ordering (..), Word, init, log, map, not, repeat, undefined, (&&), (++), (||)) @@ -94,9 +93,9 @@ readStringFromMemory addr count = do pure $ P.map chr $ takeWhile (/= 0) bytes -- | Called when the core halts with a syscall. Return the value to write to a0, or Nothing to truly exit. -type Instrument f m = Core.State f -> m (Maybe (f Types.Word)) +type Instrument m = Core.State -> m (Maybe Types.Word) -runElf :: forall f m. (Access f, MonadIO m, MonadMemory m) => Instrument f m -> CircuitSim m (Core.Input f) (Core.State f) (Core.Output f) -> m () +runElf :: forall m. (MonadIO m, MonadMemory m) => Instrument m -> CircuitSim m Core.Input Core.State Core.Output -> m () runElf instr c = go c where go sim@(CircuitSim i s step next) = do @@ -114,5 +113,4 @@ runElf instr c = go c Just ret -> do let s'' = Core.initAt resumePc (modifyRF 10 ret (Core.stateRegFile s')) go $ sim {circuitInput = Core.initInput, circuitState = s''} - Just (Core.EBreak _) -> pure () - Just Core.SecurityViolation -> pure () \ No newline at end of file + Just (Core.EBreak _) -> pure () \ No newline at end of file diff --git a/src/Elf/Syscall.hs b/src/Elf/Syscall.hs index f38ea63..ef28693 100644 --- a/src/Elf/Syscall.hs +++ b/src/Elf/Syscall.hs @@ -4,7 +4,6 @@ module Elf.Syscall (handleSyscall, ProgramExitException(..)) where import Clash.Prelude hiding (Log, Ordering (..), Word, break, def, init, lift, log, resize, zip, (++)) import Prelude hiding (Ordering (..), Word, break, init, log, map, not, repeat, undefined, (&&), (||)) -import Access import Memory.Types import Elf.ElfLoader import Data.Int (Int32) @@ -16,7 +15,7 @@ import qualified Data.ByteString as BS import Types import qualified Core -import RegFile +import Core.RegFile -- Custom exception type for non-zero program exit codes newtype ProgramExitException = ProgramExitException Int32 @@ -28,64 +27,57 @@ instance Exception ProgramExitException randomFd :: BitVector 32 randomFd = 67 -handleSyscall :: (Access f, MonadIO m, MonadMemory m) => Core.State f -> m (Maybe (f Word)) +handleSyscall :: (MonadIO m, MonadMemory m) => Core.State -> m (Maybe Word) handleSyscall s = do let rf = Core.stateRegFile s reg n = lookupRF n rf - noSecrets (reg 17) (pure Nothing) $ \case + case reg 17 of 64 -> do -- write - noSecrets (reg 10) (pure Nothing) $ \fd -> - noSecrets (reg 11) (pure Nothing) $ \buf -> - noSecrets (reg 12) (pure Nothing) $ \count -> do - when (fd == 1 || fd == 2) $ do - str <- readStringFromMemory (fromIntegral buf) (fromIntegral count) - liftIO $ putStr str - pure $ Just (pure count) + let fd = reg 10 + buf = reg 11 + count = reg 12 + when (fd == 1 || fd == 2) $ do + str <- readStringFromMemory (fromIntegral buf) (fromIntegral count) + liftIO $ putStr str + pure $ Just count 93 -> do -- exit - noSecrets (reg 10) (pure Nothing) $ \code -> do - when (code /= 0) $ - liftIO $ throwIO $ ProgramExitException (bitCoerce code :: Int32) - pure Nothing - 80 -> do -- fstat - noSecrets (reg 10) (pure Nothing) $ \case + let code = reg 10 + when (code /= 0) $ + liftIO $ throwIO $ ProgramExitException (bitCoerce code :: Int32) + pure Nothing + 80 -> -- fstat + case reg 10 of a0 | a0 /= randomFd -> - pure $ Just (pure $ bitCoerce (-1 :: Int32)) - _ -> - noSecrets (reg 11) (pure Nothing) $ \buf' -> do - let buf = bitCoerce buf' - forM_ [0 .. 0x70 - 1] $ \offset -> ramWrite (buf + offset) Byte 0 - ramWrite (buf + 8) Half 0x67 -- st_dev - ramWrite (buf + 16) Half 0x2000 -- st_mode = S_IFCHR - pure $ Just (pure 0) - 63 -> do -- read - noSecrets (reg 10) (pure Nothing) $ \case + pure $ Just (bitCoerce (-1 :: Int32)) + _ -> do + let buf = bitCoerce (reg 11) + forM_ [0 .. 0x70 - 1] $ \offset -> ramWrite (buf + offset) Byte 0 + ramWrite (buf + 8) Half 0x67 -- st_dev + ramWrite (buf + 16) Half 0x2000 -- st_mode = S_IFCHR + pure $ Just 0 + 63 -> -- read + case reg 10 of a0 | a0 /= randomFd -> - pure $ Just (pure $ bitCoerce (-1 :: Int32)) - _ -> - noSecrets (reg 11) (pure Nothing) $ \buf -> - noSecrets (reg 12) (pure Nothing) $ \count -> do - entropy <- liftIO $ getEntropy (fromIntegral count) - forM_ (zip [0 ..] (BS.unpack entropy)) $ \(i, byte) -> - ramWrite (bitCoerce buf + i) Byte (fromIntegral byte) - pure $ Just (pure $ bitCoerce count) + pure $ Just (bitCoerce (-1 :: Int32)) + _ -> do + let buf = reg 11 + count = reg 12 + entropy <- liftIO $ getEntropy (fromIntegral count) + forM_ (zip [0 ..] (BS.unpack entropy)) $ \(i, byte) -> + ramWrite (bitCoerce buf + i) Byte (fromIntegral byte) + pure $ Just (bitCoerce count) 57 -> -- close - pure $ Just (pure 0) + pure $ Just 0 214 -> -- brk - pure $ Just (pure $ bitCoerce (-1 :: Int32)) + pure $ Just (bitCoerce (-1 :: Int32)) 1024 -> do -- open - noSecrets (reg 10) (pure Nothing) $ \a0 -> do - path <- readStringFromMemory (bitCoerce a0) 256 - pure $ Just $ pure $ case path of - "/dev/random" -> randomFd - "/dev/urandom" -> randomFd - _ -> bitCoerce (-1 :: Int32) - 676767 -> do -- mark_memory_region - noSecrets (reg 10) (pure Nothing) $ \addr -> - noSecrets (reg 11) (pure Nothing) $ \size -> - noSecrets (reg 12) (pure Nothing) $ \level -> do - let endAddr = addr + size - 1 - markMemoryRegion (fromIntegral addr) (fromIntegral endAddr) (level /= 0) - pure $ Just (pure 0) + path <- readStringFromMemory (bitCoerce (reg 10)) 256 + pure $ Just $ case path of + "/dev/random" -> randomFd + "/dev/urandom" -> randomFd + _ -> bitCoerce (-1 :: Int32) + 676767 -> -- mark_memory_region: accepted and ignored; the core tracks no secrets + pure $ Just 0 n -> do liftIO $ putStrLn $ "Syscall: Unknown " ++ show (toInteger n) pure Nothing diff --git a/src/HardwareSim.hs b/src/HardwareSim.hs index fd56011..5ee0611 100644 --- a/src/HardwareSim.hs +++ b/src/HardwareSim.hs @@ -4,14 +4,12 @@ module HardwareSim (topEntity) where -import Access import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) import Core hiding (topEntity) -import Data.Functor.Identity import Data.Maybe (fromMaybe) import qualified GHC.TypeNats -import Instruction hiding (decode) -import RegFile +import Core.Instruction hiding (decode) +import Core.RegFile import Types import Memory.Types import Prelude hiding (Ordering (..), Word, init, log, map, not, repeat, take, undefined, (!!), (&&), (++), (||)) @@ -20,35 +18,39 @@ topEntity :: Clock System -> Reset System -> Enable System -> - Signal System (Output Identity) + Signal System Output topEntity = exposeClockResetEnable $ system prog3 -cpu :: forall f dom. (Access f, Generic (f Word), NFDataX (f Word), HiddenClockResetEnable dom) => Signal dom (Input f) -> Signal dom (Output f) -cpu = mealy (circuit @f @RegFile) (init @f @RegFile) +cpu :: forall dom. (HiddenClockResetEnable dom) => Signal dom Input -> Signal dom Output +cpu = mealy (circuit @RegFile) (init @RegFile) -system :: forall dom. (HiddenClockResetEnable dom) => Vec PROG_SIZE Word -> Signal dom (Output Identity) +system :: forall dom. (HiddenClockResetEnable dom) => Vec PROG_SIZE Word -> Signal dom Output system prog = cpuOut where - cpuInput :: Signal dom (Input Identity) + cpuInput :: Signal dom Input cpuInput = register initInput input - cpuOut = cpu @Identity cpuInput - ram = HardwareSim.mkRAM @Identity @PROG_SIZE @RAM_SIZE prog (fromMaybe (MemAccess False 0 Word Nothing) . outMem <$> cpuOut) - input = Input . Identity <$> ram + cpuOut = cpu cpuInput + ram = HardwareSim.mkRAM @PROG_SIZE @RAM_SIZE prog (fromMaybe (MemRead 0 Word) . outMem <$> cpuOut) + input = Input . Just <$> ram -mkRAM :: forall f progSize ramSize dom. - (Access f, HiddenClockResetEnable dom, KnownNat ((GHC.TypeNats.*) ramSize 4), KnownNat (progSize + ramSize), KnownNat ((GHC.TypeNats.*) (progSize + ramSize) 4)) => +mkRAM :: forall progSize ramSize dom. + (HiddenClockResetEnable dom, KnownNat ((GHC.TypeNats.*) ramSize 4), KnownNat (progSize + ramSize), KnownNat ((GHC.TypeNats.*) (progSize + ramSize) 4)) => Vec progSize Word -> - Signal dom (MemAccess f) -> + Signal dom MemAccess -> Signal dom Word mkRAM prog memAccessM = combine <$> ram0 <*> ram1 <*> ram2 <*> ram3 where - addr = memAddress <$> memAccessM + addr = accessAddr <$> memAccessM + + accessAddr (MemFetch a) = a + accessAddr (MemRead a _) = a + accessAddr (MemWrite a _ _) = a mkWrite n = - fmap $ \memAccess -> do - w <- memVal memAccess - pure (memAddress memAccess, extractByte n (unAccess w)) + fmap $ \memAccess -> case memAccess of + MemWrite a _ w -> Just (a, extractByte n w) + _ -> Nothing extractByte 0 w = slice d7 d0 w extractByte 1 w = slice d15 d8 w @@ -100,6 +102,6 @@ prog3 = :> -- mem[1 + r0] := r2 SType Word 4 0 2 - :> Instruction.break + :> Core.Instruction.break :> Nil ) diff --git a/src/Memory/Cache4K.hs b/src/Memory/Cache4K.hs new file mode 100644 index 0000000..c364a27 --- /dev/null +++ b/src/Memory/Cache4K.hs @@ -0,0 +1,234 @@ +{- HLINT ignore "Eta reduce" -} +-- | A 4 KiB direct-mapped cache: 256 lines of 16 bytes, four words each. +-- +-- An address splits into a tag (bits 31 to 12), a set (bits 11 to 4), a word +-- within the line (bits 3 and 2) and a byte within the word (bits 1 and 0). The +-- tags and the data live in two arrays, 'TagArr' indexed by set and 'DataArr' +-- indexed by set and word. A tag entry is the valid bit followed by the tag. +-- +-- The arrays are 'Vec's, read and written only through the wrappers below. +-- Those are @OPAQUE@ so that the proof can replace them by SMT array operations +-- ("Proof.Cache.Array"), as it does for the register file and memory: the +-- Clash 'Vec' operations themselves cannot be symbolically executed. +module Memory.Cache4K + ( -- * Arrays + TagArr (..), + tagRead, + tagWrite, + tagEmpty, + DataArr (..), + dataRead, + dataWrite, + dataZero, + + -- * Addresses + Tag, + SetIdx, + WordIdx, + ByteIdx, + tagOf, + setOf, + wordOf, + byteOf, + wordAddr, + + -- * The cache + Cache4K (..), + emptyCache4K, + entryValid, + entryTag, + cacheHit, + cacheFill, + cacheRead, + cacheWrite, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Memory.Types (MemOps (..)) +import Types (Address, Size (..), Word, Byte) +import Prelude hiding (Ordering (..), Word, init, log, not, repeat, undefined, (!!), (&&), (++), (||)) + +-- Arrays ------------------------------------------------------------------------ + +-- | The tag entries, one per set: the valid bit, then the tag. +newtype TagArr = TagArr (Vec 256 (BitVector 21)) + deriving (Eq, Show) + +-- | The tag entry of set @si@. +{-# OPAQUE tagRead #-} +tagRead :: BitVector 8 -> TagArr -> BitVector 21 +tagRead si (TagArr v) = v !! si + +-- | Set the tag entry of set @si@ to @e@. +{-# OPAQUE tagWrite #-} +tagWrite :: BitVector 8 -> BitVector 21 -> TagArr -> TagArr +tagWrite si e (TagArr v) = TagArr (replace si e v) + +-- | No line valid. +{-# OPAQUE tagEmpty #-} +tagEmpty :: TagArr +tagEmpty = TagArr (repeat 0) + +-- | The data, one word per set and word within the line. +newtype DataArr = DataArr (Vec 1024 Word) + deriving (Eq, Show) + +-- | The word at index @i@ (set, then word within the line). +{-# OPAQUE dataRead #-} +dataRead :: BitVector 10 -> DataArr -> Word +dataRead i (DataArr v) = v !! i + +-- | Set the word at index @i@ to @w@. +{-# OPAQUE dataWrite #-} +dataWrite :: BitVector 10 -> Word -> DataArr -> DataArr +dataWrite i w (DataArr v) = DataArr (replace i w v) + +-- | All words zero. +{-# OPAQUE dataZero #-} +dataZero :: DataArr +dataZero = DataArr (repeat 0) + +-- Addresses --------------------------------------------------------------------- + +-- | Which block of memory a line holds, among those that map to its set: bits +-- 31 to 12 of an address. +type Tag = BitVector 20 + +-- | The set, and so the line, an address maps to: bits 11 to 4. +type SetIdx = BitVector 8 + +-- | The word within a line: bits 3 and 2. +type WordIdx = BitVector 2 + +-- | The byte within a word: bits 1 and 0. +type ByteIdx = BitVector 2 + +-- | The tag of an address. +tagOf :: Address -> Tag +tagOf addr = slice d31 d12 (pack addr) + +-- | The set of an address. +setOf :: Address -> SetIdx +setOf addr = slice d11 d4 (pack addr) + +-- | The word of an address within its line. +wordOf :: Address -> WordIdx +wordOf addr = slice d3 d2 (pack addr) + +-- | The byte of an address within its word. +byteOf :: Address -> ByteIdx +byteOf addr = slice d1 d0 (pack addr) + +-- | The address of byte @bi@ of word @wi@ of the line with tag @t@ in set @si@. +wordAddr :: Tag -> SetIdx -> WordIdx -> ByteIdx -> Address +wordAddr t si wi bi = unpack (t ++# si ++# wi ++# bi) + +-- The cache --------------------------------------------------------------------- + +-- | The cache: a tag entry per set, and the four words of each line. +data Cache4K = Cache4K + { -- | The tag entries, one per set. + tagArr :: TagArr, + -- | The cached words, four per set. + dataArr :: DataArr + } + deriving (Eq, Show) + +-- | The empty cache: no line valid. +emptyCache4K :: Cache4K +emptyCache4K = Cache4K tagEmpty dataZero + +-- | Does a tag entry hold a block? Its top bit, the valid bit. +entryValid :: BitVector 21 -> Bool +entryValid e = slice d20 d20 e == 1 + +-- | The tag of the block a tag entry holds: its low 20 bits. +entryTag :: BitVector 21 -> Tag +entryTag e = slice d19 d0 e + +-- | Does the line of an address hold its block? +cacheHit :: Address -> Cache4K -> Bool +cacheHit addr c = entryValid e && entryTag e == tagOf addr + where + e = tagRead (setOf addr) (tagArr c) + +-- | Load the line of an address from memory: the four words of its block, and +-- the line's tag entry made valid with the address's tag. +cacheFill :: (MemOps m) => Address -> m -> Cache4K -> Cache4K +cacheFill addr mem c = Cache4K tags' dat4 + where + tags' = tagWrite (setOf addr) ((1 :: BitVector 1) ++# tagOf addr) (tagArr c) + + dat1 = dataWrite (i 0) (rd 0) (dataArr c) + dat2 = dataWrite (i 1) (rd 1) dat1 + dat3 = dataWrite (i 2) (rd 2) dat2 + dat4 = dataWrite (i 3) (rd 3) dat3 + + i :: WordIdx -> BitVector 10 + i wi = setOf addr ++# wi + rd :: WordIdx -> Word + rd wi = memReadWord (wordAddr (tagOf addr) (setOf addr) wi 0) mem + +-- | Byte @bi@ of a word. +cacheReadByteInWord :: ByteIdx -> Word -> Byte +cacheReadByteInWord bi w = case bi of + 0 -> slice d7 d0 w + 1 -> slice d15 d8 w + 2 -> slice d23 d16 w + _ -> slice d31 d24 w + +-- | The cached byte at an address, meaningful on a hit. +cacheReadByte :: Address -> Cache4K -> Byte +cacheReadByte addr c = + let w = dataRead (setOf addr ++# wordOf addr) (dataArr c) + in cacheReadByteInWord (byteOf addr) w + +-- | What a read of @size@ at an address gets from the cache: its bytes, the +-- byte at the address lowest, zero above, as memory answers +-- ('Memory.Types.readResp'). Byte by byte, so a read may cross a word or line +-- boundary. Meaningful when the lines of all its bytes hit. +cacheRead :: Address -> Size -> Cache4K -> Word +cacheRead addr size c = case size of + Byte -> zeroExtend b0 + Half -> zeroExtend (b1 ++# b0) + Word -> b3 ++# b2 ++# b1 ++# b0 + where + b0 = cacheReadByte addr c + b1 = cacheReadByte (addr + 1) c + b2 = cacheReadByte (addr + 2) c + b3 = cacheReadByte (addr + 3) c + +-- | A word with byte @bi@ replaced by @b@. +cacheWriteByteInWord :: ByteIdx -> Byte -> Word -> Word +cacheWriteByteInWord bi b w = case bi of + 0 -> slice d31 d8 w ++# b + 1 -> slice d31 d16 w ++# b ++# slice d7 d0 w + 2 -> slice d31 d24 w ++# b ++# slice d15 d0 w + _ -> b ++# slice d23 d0 w + +-- | Put a byte into the cached word of its address, if its line holds the +-- address's block; otherwise leave the cache alone (no allocation). +cacheWriteByte :: Address -> Byte -> Cache4K -> Cache4K +cacheWriteByte addr b c + | cacheHit addr c = c {dataArr = dataWrite i (cacheWriteByteInWord (byteOf addr) b w) (dataArr c)} + | otherwise = c + where + i = setOf addr ++# wordOf addr + w = dataRead i (dataArr c) + +-- | What a write does to the cache. Memory always takes the write +-- (write-through); the cache only makes sure its copy does not go stale. Byte by +-- byte, as memory stores it ('Memory.Types.memWrite'): each byte goes into +-- its cached word if its line hits, so a write may cross a word or line +-- boundary. +cacheWrite :: Address -> Size -> Word -> Cache4K -> Cache4K +cacheWrite addr size w c = case size of + Byte -> c1 + Half -> c2 + Word -> c4 + where + c1 = cacheWriteByte addr (slice d7 d0 w) c + c2 = cacheWriteByte (addr + 1) (slice d15 d8 w) c1 + c3 = cacheWriteByte (addr + 2) (slice d23 d16 w) c2 + c4 = cacheWriteByte (addr + 3) (slice d31 d24 w) c3 diff --git a/src/Memory/Cache4KServer.hs b/src/Memory/Cache4KServer.hs new file mode 100644 index 0000000..0d447b4 --- /dev/null +++ b/src/Memory/Cache4KServer.hs @@ -0,0 +1,99 @@ +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | The 4 KiB cache ("Memory.Cache4K") as a server between the core and memory: +-- how it answers the core's memory requests, cycle by cycle. +-- +-- A read miss takes 'penalty' extra cycles and then fills the line with the +-- four words of its block; a read that leaves its word bypasses the cache with +-- the same delay. A write goes through to memory at once: inside one word, on a +-- hit, it is merged into the cached word; if it crosses a word boundary, the +-- lines it touches are invalidated instead ('Memory.Cache4K.write'). Fetches +-- bypass the cache. +module Memory.Cache4KServer + ( Cycles, + CacheSrv (..), + CacheSrvState (..), + initCacheSrv, + penalty, + serve, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Core (Input (..), MemAccess (..), Request) +import Memory.Cache4K +import Memory.Types (MemOps (..)) +import Types +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- | Cycles of a miss penalty: a small counter, sized as hardware would size it. +-- (This also keeps the symbolic proof in the bitvector fragment Bitwuzla reads.) +type Cycles = Unsigned 8 + +-- | Extra cycles of a read miss: the four words of a line. +penalty :: Cycles +penalty = 4 + +-- | The address of the last byte of an access. An access touches at most two +-- lines: the lines of its first and last byte. +data CacheSrvState = CacheSrvReady | CacheSrvStall Cycles Word + deriving (Show, Eq) + +-- | A cache in front of memory, as a server: the cache, a read waiting for +-- memory, and memory. +data CacheSrv m = CacheSrv + { srvCache :: Cache4K, + srvMem :: m, + -- | A read waiting for memory: its address and width, and the cycles left. + srvState :: CacheSrvState + } + +deriving instance (Show m) => Show (CacheSrv m) + +-- | The cache server at start: no line valid and no read waiting, in front of +-- memory @mem@. +initCacheSrv :: m -> CacheSrv m +initCacheSrv mem = CacheSrv emptyCache4K mem CacheSrvReady + +-- | One cycle of the cache in front of ideal memory. The answer is 'Nothing' +-- only while a read is not ready yet; a write and no request answer @Just 0@. +serve :: (MemOps m) => CacheSrv m -> Request -> (CacheSrv m, Input) +serve (CacheSrv c mem st) req = case st of + CacheSrvStall n w + | n > 0 -> + (CacheSrv c mem (CacheSrvStall (n - 1) w), Input Nothing) + | otherwise -> + (CacheSrv c mem CacheSrvReady, Input (Just w)) + CacheSrvReady -> case req of + Just (MemFetch addr) -> + (CacheSrv c mem CacheSrvReady, Input (Just (memReadWord addr mem))) + Just (MemRead addr size) -> + let off = case size of + Byte -> 0 + Half -> 1 + Word -> 3 + + hit1stLine = cacheHit addr c + penalty1stLine = if hit1stLine then 0 else penalty + c1 = if hit1stLine then c else cacheFill addr mem c + + hit2ndLine = cacheHit (addr + off) c1 + penalty2ndLine = if hit2ndLine then 0 else penalty + c2 = if hit2ndLine then c1 else cacheFill (addr + off) mem c1 + + n = penalty1stLine + penalty2ndLine + w = cacheRead addr size c2 + + in if n > 0 + then (CacheSrv c2 mem (CacheSrvStall (n - 1) w), Input Nothing) + else (CacheSrv c2 mem CacheSrvReady, Input $ Just w) + Just (MemWrite addr size val) -> + ( CacheSrv + (cacheWrite addr size val c) + (memWrite addr size val mem) + CacheSrvReady, + Input (Just 0) + ) + -- No request. + _ -> (CacheSrv c mem CacheSrvReady, Input (Just 0)) diff --git a/src/Memory/IO.hs b/src/Memory/IO.hs index 4d54ff4..094d699 100644 --- a/src/Memory/IO.hs +++ b/src/Memory/IO.hs @@ -4,12 +4,6 @@ module Memory.IO runIOMemT, newIOMem, loadProgram, - SecureIOMem (..), - SecureIOMemT (..), - runSecureIOMemT, - newSecureIOMem, - loadSecureProgram, - MemoryRegion (..), ) where @@ -19,11 +13,9 @@ import Control.Monad (forM_) import Control.Monad.Reader import Data.Array.IO import Data.Elf (Elf) -import Data.IORef (modifyIORef) import Data.Traversable (forM) import Data.Word (Word8) import Elf.ElfLoader (baseAddr, loadElf) -import GHC.IORef import Memory.Types import Types import Prelude hiding (Ordering (..), Word, break, init, log, map, not, repeat, undefined, (&&), (++), (||)) @@ -80,82 +72,3 @@ instance {-# OVERLAPPING #-} MonadMemory (IOMemT IO) where Byte -> writeBytes [bitCoerce b0] -- Write 1 byte Half -> writeBytes [bitCoerce b0, bitCoerce b1] -- Write 2 bytes (halfword) Word -> writeBytes [bitCoerce b0, bitCoerce b1, bitCoerce b2, bitCoerce b3] -- Write 4 bytes (word) - -- IOMemT implementation: no-op security functions (like Identity) - markMemoryRegion _ _ _ = pure () - isMemorySecret _ = pure False - --- | Secure memory implementation that tracks security regions -data SecureIOMem = SecureIOMem - { secureIOMemInitSP :: Word, - secureIOMemRAM :: IOUArray Int Word8, - -- | List of memory regions and their security levels - secureIOMemRegions :: IORef [MemoryRegion] - } - deriving (Eq) - --- | A memory region with security classification -data MemoryRegion = MemoryRegion - { regionStart :: Address, - regionEnd :: Address, - regionIsSecret :: Bool - } - deriving (Eq, Show) - --- Newtype wrapper for secure memory monad -newtype SecureIOMemT m a = SecureIOMemT (ReaderT SecureIOMem m a) - deriving newtype (Functor, Applicative, Monad, MonadIO, MonadReader SecureIOMem) - -instance MonadTrans SecureIOMemT where - lift = SecureIOMemT . lift - -runSecureIOMemT :: SecureIOMem -> SecureIOMemT m a -> m a -runSecureIOMemT secmem (SecureIOMemT m) = runReaderT m secmem - -newSecureIOMem :: (MonadIO m) => Elf -> m SecureIOMem -newSecureIOMem elf = do - let memSize = 0x4000000 - base <- liftIO $ fromIntegral <$> baseAddr elf - let sp = base + memSize - 0x1000000 - ramArray <- liftIO $ newArray (base, base + memSize) 0 - regionsRef <- liftIO $ newIORef [] - pure $ SecureIOMem (fromIntegral sp) ramArray regionsRef - -loadSecureProgram :: (MonadMemory m) => Elf -> m () -loadSecureProgram elf = loadElf elf - -instance {-# OVERLAPPING #-} MonadMemory (SecureIOMemT IO) where - ramRead addr _size = do - ramArray <- asks secureIOMemRAM - bytes <- forM [0 .. 3] $ \i -> do - w8 <- lift $ readArray ramArray (fromIntegral addr + i) - pure $ bitCoerce w8 - let word = readWord @4 0 $ unsafeFromList bytes - pure word - ramWrite addr size w = do - ramArray <- asks secureIOMemRAM - let b0 = slice d7 d0 w -- Extract bits 7-0 (least significant byte) - b1 = slice d15 d8 w -- Extract bits 15-8 - b2 = slice d23 d16 w -- Extract bits 23-16 - b3 = slice d31 d24 w -- Extract bits 31-24 (most significant byte) - writeBytes bytes = do - forM_ (P.zip [0 ..] bytes) $ \(i, byte) -> - lift $ writeArray ramArray (fromIntegral addr + i) byte - case size of - Byte -> writeBytes [bitCoerce b0] -- Write 1 byte - Half -> writeBytes [bitCoerce b0, bitCoerce b1] -- Write 2 bytes (halfword) - Word -> writeBytes [bitCoerce b0, bitCoerce b1, bitCoerce b2, bitCoerce b3] -- Write 4 bytes (word) - - -- Secure memory implementation: actually track security regions - markMemoryRegion startAddr endAddr isSecret = do - regionsRef <- asks secureIOMemRegions - let region = MemoryRegion startAddr endAddr isSecret - liftIO $ modifyIORef regionsRef (region :) - - isMemorySecret addr = do - regionsRef <- asks secureIOMemRegions - regions <- liftIO $ readIORef regionsRef - pure $ any (isAddrInSecretRegion addr) regions - where - isAddrInSecretRegion :: Address -> MemoryRegion -> Bool - isAddrInSecretRegion a (MemoryRegion start end secret) = - secret && a >= start && a <= end diff --git a/src/Memory/Ideal.hs b/src/Memory/Ideal.hs new file mode 100644 index 0000000..79276db --- /dev/null +++ b/src/Memory/Ideal.hs @@ -0,0 +1,35 @@ +-- | Ideal memory: the memory the core is specified against, as the ISA is the +-- core it is specified against. It answers every request in the next cycle, +-- and applies a write at once. +module Memory.Ideal + ( idealServe, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Core (Input (..), MemAccess (..)) +import Memory.Types (MemOps (..)) +import Types (Address, Size (..), Word) +import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||)) + +-- | One cycle of ideal memory: the memory after the request, and the core's +-- input for the next cycle. +idealServe :: (MemOps m) => m -> Maybe MemAccess -> (m, Input) +idealServe mem req = case req of + Just (MemFetch addr) -> (mem, Input (Just (memReadWord addr mem))) + -- A read answers exactly the bytes it asks for. + Just (MemRead addr size) -> (mem, Input (Just (readSized addr size mem))) + Just (MemWrite addr size val) -> (memWrite addr size val mem, Input (Just 0)) + Nothing -> (mem, Input (Just 0)) + +-- | The @size@ bytes at @addr@, the byte at the address lowest, zero-extended. +readSized :: (MemOps m) => Address -> Size -> m -> Word +readSized addr size mem = case size of + Byte -> zeroExtend b0 + Half -> zeroExtend (b1 ++# b0) + Word -> b3 ++# b2 ++# b1 ++# b0 + where + b0 = memReadByte addr mem + b1 = memReadByte (addr + 1) mem + b2 = memReadByte (addr + 2) mem + b3 = memReadByte (addr + 3) mem diff --git a/src/Memory/ST.hs b/src/Memory/ST.hs index 963c3dd..91a1f72 100644 --- a/src/Memory/ST.hs +++ b/src/Memory/ST.hs @@ -12,7 +12,6 @@ module Memory.ST ) where -import Access (Access) import Clash.Prelude hiding (Ordering (..), Word, init, lift) import Control.Monad (when) import Control.Monad.Reader @@ -59,8 +58,6 @@ instance {-# OVERLAPPING #-} (MonadIO m) => MonadMemory (STMemoryT RealWorld m) liftIO $ stToIO $ writeDataArray offset size w (stData st) - markMemoryRegion _ _ _ = pure () - isMemorySecret _ = pure False -- | Read a sized value from the data array. readDataArray :: Address -> Size -> STUArray s Address Word8 -> ST s Word @@ -106,7 +103,7 @@ runSTSim f sim = f sim -- | Utility to run a full simulation until halt. -- Uses deepseqX to ensure the state is fully evaluated and prevent thunk leaks. -runUntilHalt :: (NFDataX (f Word), Generic (f Word), MonadMemory m) => CircuitSim m (Core.Input f) (Core.State f) (Core.Output f) -> m (Core.State f) +runUntilHalt :: (MonadMemory m) => CircuitSim m Core.Input Core.State Core.Output -> m Core.State runUntilHalt sim = go sim where go sim' = do diff --git a/src/Memory/Types.hs b/src/Memory/Types.hs index abc5268..d10e4b4 100644 --- a/src/Memory/Types.hs +++ b/src/Memory/Types.hs @@ -22,17 +22,13 @@ where import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) import Data.Proxy (Proxy (..)) import qualified GHC.TypeNats -import Instruction +import Core.Instruction import Types import Prelude hiding (Ordering (..), Word, init, iterate, log, map, not, repeat, replicate, take, undefined, (!!), (&&), (++), (||)) class Monad m => MonadMemory m where ramRead :: Address -> Size -> m Word ramWrite :: Address -> Size -> Word -> m () - -- | Mark a region of memory as public or secret - markMemoryRegion :: Address -> Address -> Bool -> m () - -- | Check if a memory address is marked as secret - isMemorySecret :: Address -> m Bool -- | The byte-addressed memory the ISA model and the proof harness use. Same -- size as the one the simulation tests use. @@ -40,19 +36,19 @@ type MemBytes = Vec MEM_SIZE_BYTES Byte -- | The operations a memory representation has to provide. -- --- Parameterised for the same reason as 'RegFile.RegFileOps': the @Vec@-backed +-- Parameterised for the same reason as 'Core.RegFile.RegFileOps': the @Vec@-backed -- 'MemBytes' cannot be symbolically executed, while the function-backed 'MemFn' -- can. class MemOps m where memReadWord :: Address -> m -> Word - memWriteWord :: Size -> Address -> Word -> m -> m + memWrite :: Address -> Size -> Word -> m -> m -- | Single byte, which is what the pointwise form of the invariant compares. memReadByte :: Address -> m -> Byte instance (KnownNat n) => MemOps (Vec n Byte) where memReadWord = readWord - memWriteWord = write + memWrite = write memReadByte a m = m !! a -- | Verification-only memory: a function rather than a container. @@ -60,7 +56,7 @@ newtype MemFn = MemFn {memByte :: Address -> Byte} instance MemOps MemFn where memReadWord a (MemFn m) = m (a + 3) ++# m (a + 2) ++# m (a + 1) ++# m a - memWriteWord size a w m = + memWrite a size w m = case size of Byte -> put a b0 m Half -> put (a + 1) b1 (put a b0 m) @@ -78,8 +74,8 @@ readWord :: (KnownNat n) => Address -> Vec n Byte -> Word readWord addr m = (m !! (addr + 3)) ++# (m !! (addr + 2)) ++# (m !! (addr + 1)) ++# (m !! addr) -write :: (KnownNat n) => Size -> Address -> Word -> Vec n Byte -> Vec n Byte -write size addr w mem = +write :: (KnownNat n) => Address -> Size -> Word -> Vec n Byte -> Vec n Byte +write addr size w mem = let b0 = slice d7 d0 w b1 = slice d15 d8 w b2 = slice d23 d16 w diff --git a/src/Memory/Vec.hs b/src/Memory/Vec.hs index 0d48b62..030c88e 100644 --- a/src/Memory/Vec.hs +++ b/src/Memory/Vec.hs @@ -23,7 +23,4 @@ instance (KnownNat n, Monad m, MonadState (Mem n) m) => MonadMemory m where ramRead addr _size = readWord addr <$> gets memRAM ramWrite addr size w = do ram <- gets memRAM - modify $ \s -> s {memRAM = write size addr w ram} - -- Identity implementation: no-op security functions - markMemoryRegion _ _ _ = pure () - isMemorySecret _ = pure False + modify $ \s -> s {memRAM = write addr size w ram} diff --git a/src/Simulate.hs b/src/Simulate.hs index f2d336a..f5fa58e 100644 --- a/src/Simulate.hs +++ b/src/Simulate.hs @@ -13,13 +13,11 @@ module Simulate ) where -import Access import Clash.Prelude hiding (Log, Ordering (..), Word, def, init, lift, log) import Control.Monad.RWS import Control.Monad.State import Core hiding (State) import qualified Core -import Data.Functor.Identity import Data.Maybe (isJust) import Memory.Types import Memory.Vec @@ -30,7 +28,7 @@ import Prelude hiding (Ordering (..), Word, init, log, map, not, repeat, take, u result :: (MonadState (Mem n) m) => CircuitSim m i s o -> m (Vec n Byte) result c = watch c *> gets memRAM -simulator :: forall f m. (Access f, MonadMemory m) => CircuitSim m (Input f) (Core.State f) (Output f) +simulator :: forall m. (MonadMemory m) => CircuitSim m Input Core.State Output simulator = CircuitSim { circuitInput = initInput, @@ -39,38 +37,34 @@ simulator = circuitNext = next } where - next :: Core.State f -> Output f -> m (Maybe (Input f)) + next :: Core.State -> Output -> m (Maybe Input) next s (Output mem) = do mem_in <- doMemory if isJust (Core.stateHalt s) then pure Nothing - else pure (Just (Input mem_in)) + else pure (Just (Input (Just mem_in))) where - doMemory :: m (f Word) - doMemory - | Just (MemAccess _ addr size mval) <- mem = - case mval of - Nothing -> do - word <- ramRead addr size - isSecret <- isMemorySecret addr - pure (conditionalSecret isSecret word) - Just val -> do - ramWrite addr size (unAccess val) - pure (pure 0) - | otherwise = pure (pure 0) + doMemory :: m Word + doMemory = case mem of + Just (MemFetch addr) -> ramRead addr Word + Just (MemRead addr size) -> ramRead addr size + Just (MemWrite addr size val) -> do + ramWrite addr size val + pure 0 + Nothing -> pure 0 runSimulator :: - forall f ramSize progSize a. - (Access f, KnownNat ramSize, KnownNat (MemSizeFrom progSize ramSize)) => - ( CircuitSim (State (Mem (MemSizeFrom progSize ramSize))) (Input f) (Core.State f) (Output f) -> + forall ramSize progSize a. + (KnownNat ramSize, KnownNat (MemSizeFrom progSize ramSize)) => + ( CircuitSim (State (Mem (MemSizeFrom progSize ramSize))) Input Core.State Output -> State (Mem (MemSizeFrom progSize ramSize)) a ) -> Vec progSize Word -> a runSimulator f = evalState (f simulator) . Mem . mkRAM -watchSim :: forall ramSize progSize. (KnownNat ramSize, KnownNat (MemSizeFrom progSize ramSize)) => Vec progSize Word -> [(Core.State Identity, Output Identity, Maybe (Input Identity))] -watchSim = runSimulator @Identity @ramSize @progSize watch +watchSim :: forall ramSize progSize. (KnownNat ramSize, KnownNat (MemSizeFrom progSize ramSize)) => Vec progSize Word -> [(Core.State, Output, Maybe Input)] +watchSim = runSimulator @ramSize @progSize watch simResult :: forall ramSize progSize. (KnownNat ramSize, KnownNat (MemSizeFrom progSize ramSize)) => Vec progSize Word -> Vec (MemSizeFrom progSize ramSize) Byte -simResult = runSimulator @Identity result +simResult = runSimulator result diff --git a/test/BenchmarkSpec.hs b/test/BenchmarkSpec.hs index aec9f65..b9e30ac 100644 --- a/test/BenchmarkSpec.hs +++ b/test/BenchmarkSpec.hs @@ -12,11 +12,10 @@ import Control.Monad (when) import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad.ST (stToIO, RealWorld) import qualified Core as Core -import Data.Functor.Identity import Elf.ElfLoader import Elf.Syscall (handleSyscall) import Numeric (showHex) -import RegFile +import Core.RegFile import Memory.ST import Memory.Types import Simulate @@ -30,10 +29,10 @@ import qualified Prelude as P -- | Data type for benchmark test configuration data BenchmarkTest = BenchmarkTest { benchmarkPath :: String, - benchmarkInstrument :: forall m. (MonadIO m, MonadMemory m) => Core.State Identity -> m (Maybe (Identity Types.Word)) + benchmarkInstrument :: forall m. (MonadIO m, MonadMemory m) => Core.State -> m (Maybe Types.Word) } -cryptoInstrument :: (MonadIO m, MonadMemory m) => Bool -> Core.State Identity -> m (Maybe (Identity Types.Word)) +cryptoInstrument :: (MonadIO m, MonadMemory m) => Bool -> Core.State -> m (Maybe Types.Word) cryptoInstrument shouldLog s = do when shouldLog $ do let pc = Core.stateExPc s @@ -43,7 +42,7 @@ cryptoInstrument shouldLog s = do liftIO $ print $ "stateExPc=0x" P.++ showHex pc "" P.++ " stateExInstr=0x" P.++ show (Core.stateExInstr s) P.++ " s9=" P.++ show s9 P.++ " s11=" P.++ show s11 handleSyscall s -testSuiteInstrument :: (MonadIO m) => Bool -> Core.State Identity -> m (Maybe (Identity Types.Word)) +testSuiteInstrument :: (MonadIO m) => Bool -> Core.State -> m (Maybe Types.Word) testSuiteInstrument shouldLog s = do when shouldLog $ do let pc = Core.stateExPc s @@ -73,7 +72,7 @@ mkBenchmarkTest testName _benchmark = _ <- runSTMemoryT stMem $ do loadElf elf - let sim :: CircuitSim (STMemoryT RealWorld IO) (Core.Input Identity) (Core.State Identity) (Core.Output Identity) + let sim :: CircuitSim (STMemoryT RealWorld IO) (Core.Input) (Core.State) (Core.Output) sim = simulator runElf (benchmarkInstrument _benchmark) @@ -81,7 +80,7 @@ mkBenchmarkTest testName _benchmark = { circuitState = Core.initAt (fromIntegral entryOffset) - (modifyRF 2 (pure $ fromIntegral (base + 0x1000000 - 0x1000)) (initRF @Identity)) + (modifyRF 2 (fromIntegral (base + 0x1000000 - 0x1000)) initRF) }) pure () diff --git a/test/Cache4KSpec.hs b/test/Cache4KSpec.hs new file mode 100644 index 0000000..a4c09d8 --- /dev/null +++ b/test/Cache4KSpec.hs @@ -0,0 +1,365 @@ +{-# LANGUAGE PackageImports #-} + +-- | The 4 KiB cache ("Memory.Cache4K"): a few concrete runs, its server proof +-- ("Proof.Cache.Server4K") on random states, and the composition end to end. +module Cache4KSpec + ( cache4KTests, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Clash.Sized.Vector (unsafeFromList) +import CompositionSpec (coreDiff, ctTrace, genByteProg, genCTProg, genData, genSecretFreeProg, genWord, sameModuloCtrl, simHops, withData) +import Core +import Data.Functor.Identity (Identity (..)) +import Data.Maybe (isNothing) +import Core.Instruction +import Memory.Cache4K +import Memory.Cache4KServer +import Memory.Types +import Proof.Cache.Server.Functional.Driver (driver) +import Proof.Cache.Server.Functional.Invariant (coherentAt, srvInvAt) +import Proof.Cache.Server4K +import Proof.Core.Functional.Obligation (isaAt) +import Proof.Core.Leakage.Model +import Proof.Core.Functional.Machine +import ProofSpec (initSys) +import Core.RegFile (RegFile) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@?=)) +import Test.Tasty.QuickCheck +import "aimcore" Types +import Prelude hiding (Ordering (..), Word, init, log, map, not, undefined, (!!), (&&), (++), (||)) +import qualified Prelude as P + +cache4KTests :: TestTree +cache4KTests = + testGroup + "Core behind a 4 KiB cache" + [ runTests, + testProperty "read, from the lines of the first and last byte, answers as memory does" $ + withMaxSuccess 2000 $ checkCoverage $ + forAllShow genMem (const "") $ \mem -> forAll genAddr $ \a -> forAll (elements [Byte, Half, Types.Word]) $ \size -> + let c = cacheFill (lastByteOf a size) mem (cacheFill a mem emptyCache4K) + in cover 10 (straddles a size) "straddling" (cacheRead a size c == readResp a size mem), + serverTests, + testProperty "composition: the cached core's bus trace follows from the leakage alone" $ + withMaxSuccess 300 $ checkCoverage $ + forAll genCTProg $ \prog -> + let sys = initSys prog + r = compositeReport sys + in cover 30 (stallCycles sys > 0) "the core waits for the cache" (counterexample r (P.null r)), + testProperty "... also with reads and writes of every width and alignment" $ + withMaxSuccess 300 $ checkCoverage $ + forAll genByteProg $ \prog -> forAll genData $ \ds -> + let sys = withData ds (initSys prog) + r = compositeReport sys + in cover 30 (stallCycles sys > 0) "the core waits for the cache" (counterexample r (P.null r)), + testProperty "the cached run is the ideal run with stall cycles inserted" $ + withMaxSuccess 300 $ + forAll genCTProg $ \prog -> + let r = stutterReport 300 (initSys prog) + in counterexample r (P.null r), + testProperty "... also with reads and writes of every width and alignment" $ + withMaxSuccess 300 $ + forAll genByteProg $ \prog -> + forAll genData $ \ds -> + let r = stutterReport 300 (withData ds (initSys prog)) + in counterexample r (P.null r), + testProperty "a secret-free program leaks nothing about its data, behind the cache" $ + withMaxSuccess 300 $ + forAll genSecretFreeProg $ \prog -> + forAll genData $ \da -> + forAll genData $ \db -> + let s1 = withData da (initSys prog) + s2 = withData db (initSys prog) + in ctTrace 100 (isaAt initPc s1) == ctTrace 100 (isaAt initPc s2) + P.&& cachedObs 300 s1 == cachedObs 300 s2, + testProperty "a load through a loaded pointer leaks it, even to a timing attacker" $ + -- The control: @lw x5, 0(x0); lw x1, 0(x5); lw x2, 0(x0); ebreak@. The + -- second load's address is data. With the pointer at 0 the second load + -- hits the line the first one filled; with the pointer at 16, in the next + -- set, it misses. So even an attacker who sees only in which cycles a + -- request is made tells the two apart. + let prog = + map encode $ + unsafeFromList $ + [ IType (Load Types.Word Signed) 5 0 0, + IType (Load Types.Word Signed) 1 5 0, + IType (Load Types.Word Signed) 2 0 0 + ] + P.++ P.replicate 47 Core.Instruction.break + timing p = P.map (/= NoAccess) (cachedObs 100 (withData [(0, p)] (initSys prog))) + in once (timing 0 /= timing 16) + ] + +-- Concrete runs ------------------------------------------------------------------- + +memU :: MemFn +memU = MemFn (\a -> slice d7 d0 (pack (a * 13 + 7))) + +rdReq :: Address -> Size -> Request +rdReq a sz = Just (MemAccess False a sz Nothing) + +wrReq :: Address -> Size -> Word -> Request +wrReq a sz v = Just (MemAccess False a sz (Just (Identity v))) + +-- | Serve requests one hop each, from the empty cache in front of 'memU': +-- the stall count and the response word of each. +hops :: [Request] -> [(Cycles, Word)] +hops = go (CacheSrv emptyCache4K Nothing memU) + where + go _ [] = [] + go y (q : qs) = + let k = driver y q + (y', x) = serveN k y q + in (fromIntegral k, runIdentity (inputMem x)) : go y' qs + +runTests :: TestTree +runTests = + testGroup + "concrete runs" + [ testCase "a read miss stalls, then the rest of its line hits" $ + hops [rdReq 0x100 Types.Word, rdReq 0x10C Types.Word, rdReq 0x106 Half] + @?= [ (penalty, memReadWord 0x100 memU), + (0, memReadWord 0x10C memU), + (0, loadExtend Half Unsigned (memReadWord 0x106 memU)) + ], + testCase "lines 4 KiB apart evict each other" $ + P.map fst (hops [rdReq 0x100 Types.Word, rdReq 0x1100 Types.Word, rdReq 0x100 Types.Word]) + @?= [penalty, penalty, penalty], + testCase "a write hit is merged into the cached word" $ + hops [rdReq 0x100 Types.Word, wrReq 0x101 Byte 0xAB, rdReq 0x100 Types.Word] + @?= [ (penalty, memReadWord 0x100 memU), + (0, 0), + (0, memReadWord 0x100 (memWrite 0x101 Byte 0xAB memU)) + ], + testCase "a write that leaves its word drops its lines" $ + P.map fst (hops [rdReq 0x100 Types.Word, rdReq 0x110 Types.Word, wrReq 0x10E Types.Word 1, rdReq 0x100 Types.Word, rdReq 0x110 Types.Word]) + @?= [penalty, penalty, 0, penalty, penalty] + ] + +-- The server proof on random states ------------------------------------------------- + +-- | A memory whose bytes are a function of their address, different in every +-- test. +genMem :: Gen MemFn +genMem = do + k1 <- genU32 + k2 <- genU32 + pure (MemFn (\a -> slice d7 d0 (pack ((a * (k1 .|. 1) + k2) `xor` (a `shiftR` 9))))) + where + genU32 = fromIntegral <$> choose (0 :: Integer, 0xFFFFFFFF) :: Gen (Unsigned 32) + +-- | Tags of the first three 4 KiB blocks of memory, sometimes others. +genTag :: Gen Tag +genTag = frequency [(10, elements [0, 1, 2]), (1, fromIntegral <$> choose (0 :: Int, 0xFFFFF))] + +-- | The cache in front of memory, with no miss pending: lines mostly valid, +-- holding memory's words, and rarely a wrong word, which takes the server out of +-- its invariant at that word. +genSrv :: Gen (CacheSrv MemFn) +genSrv = do + mem <- genMem + es <- vectorOf 256 (frequency [(2, pure 0), (8, ((1 :: BitVector 1) ++#) <$> genTag)]) + ws <- P.mapM (genData1 mem es) [0 .. 1023] + pure (CacheSrv (Cache4K (TagArr (unsafeFromList es)) (DataArr (unsafeFromList ws))) Nothing mem) + where + genData1 mem es i = + let s = fromIntegral (i `P.div` 4) :: SetIdx + w = fromIntegral (i `P.mod` 4) :: WordIdx + e = es P.!! (i `P.div` 4) + in if entryValid e + then frequency [(60, pure (memReadWord (wordAddr (entryTag e) s w 0) mem)), (1, genWord)] + else genWord + +-- | Addresses in the first three 4 KiB blocks, sometimes anywhere. +genAddr :: Gen Address +genAddr = + frequency + [ (10, fromIntegral <$> choose (0 :: Int, 3 * 4096 - 1)), + (1, fromIntegral <$> choose (0 :: Integer, 0xFFFFFFFF)) + ] + +-- | Requests: none, fetches, and reads and writes of every width and alignment, +-- and also requests the core never makes. +genReq :: Gen Request +genReq = + frequency + [ (1, pure Nothing), + (2, (\a -> Just (MemAccess True a Types.Word Nothing)) <$> genAddr), + (1, (\a sz -> Just (MemAccess True a sz Nothing)) <$> genAddr <*> genSize), + (1, (\a sz v -> Just (MemAccess True a sz (Just (Identity v)))) <$> genAddr <*> genSize <*> genWord), + (8, (\a sz -> Just (MemAccess False a sz Nothing)) <$> genAddr <*> genSize), + (4, (\a sz v -> Just (MemAccess False a sz (Just (Identity v)))) <$> genAddr <*> genSize <*> genWord) + ] + where + genSize = elements [Byte, Half, Types.Word] + +-- | Witnesses, half of the time at the request's own set, word and bytes. +genWitness :: Request -> Gen (Address, SetIdx, WordIdx) +genWitness q = do + let a = maybe 0 memAddress q + wa <- frequency [(1, (\o -> a + fromIntegral o) <$> choose (0 :: Int, 4)), (1, genAddr)] + ws <- frequency [(1, pure (setOf a)), (1, fromIntegral <$> choose (0 :: Int, 255))] + ww <- frequency [(1, pure (wordOf a)), (1, fromIntegral <$> choose (0 :: Int, 3))] + pure (wa, ws, ww) + +-- | Serve a request, then @n@ cycles without one. A harness helper: the proofs +-- write their cycles out. +serveN :: (MemOps m) => Int -> CacheSrv m -> Request -> (CacheSrv m, Input) +serveN n srv req = go n (serve srv req) + where + go k (y', x) + | k <= 0 = (y', x) + | otherwise = go (k - 1) (serve y' Nothing) + +-- | Has the core not halted yet? +running :: SysG r m -> Bool +running = isNothing . stateHalt . sysCore + +-- | The address of the last byte of an access. +lastByteOf :: Address -> Size -> Address +lastByteOf a sz = + a + case sz of + Byte -> 0 + Half -> 1 + Types.Word -> 3 + +-- | Does an access cross a word boundary? +straddles :: Address -> Size -> Bool +straddles a sz = a `shiftR` 2 /= lastByteOf a sz `shiftR` 2 + +-- | What kind of request, against what cache. +reqKind :: CacheSrv MemFn -> Request -> String +reqKind y q = case q of + Nothing -> "none" + Just (MemAccess _ a sz (Just _)) + | straddles a sz -> "straddling write" + | hit a c -> "write hit" + | otherwise -> "write miss" + Just (MemAccess True _ _ Nothing) -> "fetch" + Just (MemAccess False a sz Nothing) + | straddles a sz -> "straddling read" + | hit a c -> "hit" + | otherwise -> "miss" + where + c = srvCache y + +coverKinds :: CacheSrv MemFn -> Request -> Property -> Property +coverKinds y q = + P.foldr + (\k f -> cover 3 (reqKind y q == k) k . f) + id + ["none", "fetch", "write hit", "write miss", "straddling write", "hit", "miss", "straddling read"] + +serverTests :: TestTree +serverTests = + testGroup + "server proof" + [ testProperty "the empty cache starts in the invariant" $ + forAllShow genMem (const "") $ \mem -> + forAll (fromIntegral <$> choose (0 :: Int, 255)) $ \s -> + forAll (fromIntegral <$> choose (0 :: Int, 3)) $ \w -> srvInit s w mem, + testProperty "refinement: the hop of a request ends with ideal memory's response" $ + withMaxSuccess 4000 $ checkCoverage $ + forAllShow genSrv (const "") $ \y -> forAll genReq $ \q -> forAll (genWitness q) $ \(wa, ws, ww) -> + coverKinds y q $ + cover 80 (srvInvAt ws ww y) "in the invariant at the witness" $ + cover 10 (ws == maybe 0 (setOf . memAddress) q P.&& ww == maybe 0 (wordOf . memAddress) q) "the witness is the accessed word" $ + srvRefine wa ws ww y q, + testProperty "leakage: the stalls and the next tags follow from the tags and the observed request" $ + withMaxSuccess 4000 $ checkCoverage $ + forAllShow genSrv (const "") $ \y -> forAll genReq $ \q -> forAll (genWitness q) $ \(_, ws, _) -> + coverKinds y q (property (srvLeak ws y q)), + testProperty "the cache answers late only to a data read" $ + withMaxSuccess 2000 $ + forAllShow genSrv (const "") $ \y -> forAll genReq $ \q -> stallsOnReads y q + ] + +-- Composition, end to end ----------------------------------------------------------- + +-- | The requests the core makes behind the 4 KiB cache, cycle by cycle, until it +-- halts. +cachedObs :: Int -> Sys -> [Obs] +cachedObs n sys = go n (initCacheSys sys emptyCache4K) + where + go :: Int -> CacheSys RegFile MemBytes Cache4K -> [Obs] + go 0 _ = [] + go j cs + | P.not (running (cacheSysCore cs)) = [] + | otherwise = let (cs', o) = stepCachedOut cs in obsOf o : go (j - 1) cs' + +-- | The same trace from the leakage alone: the core's simulator produces each +-- hop's requests as behind ideal memory, and the cache's simulator adds the +-- cycles in which the core waits. +compositeTrace :: Int -> Sys -> [Obs] +compositeTrace n sys0 = go (P.take n (simHops sys0)) tagEmpty + where + go [] _ = [] + go (os : rest) t = + let (t', bus) = serveAll t os + in bus P.++ go rest t' + serveAll t [] = (t, []) + serveAll t (o : os) = + let (t1, xs) = simBus t o + (t2, ys) = serveAll t1 os + in (t2, xs P.++ ys) + +compositeReport :: Sys -> String +compositeReport sys0 + | cached == P.take (P.length cached) composite = "" + | otherwise = "first difference at cycle " P.++ show i P.++ ": " P.++ show (P.take 6 (P.drop i cached)) P.++ " vs " P.++ show (P.take 6 (P.drop i composite)) + where + cached = cachedObs 600 sys0 + composite = compositeTrace 600 sys0 + i = P.length (P.takeWhile id (P.zipWith (==) cached composite)) + +-- | The cycles in which the core behind the cache waits, until it halts. +stallCycles :: Sys -> Int +stallCycles sys0 = go (600 :: Int) (initCacheSys sys0 emptyCache4K) + where + go 0 _ = 0 + go j cs + | P.not (running (cacheSysCore cs)) = 0 + | otherwise = + (if inputMemReady (sysInput (cacheSysCore cs)) then 0 else 1) + + go (j - 1) (fst (stepCachedOut cs)) + +-- | Is the cache coherent with memory at every set the harness's memory can +-- fill? Memory is 'MEM_SIZE' words, below address 512, so only sets 0 to 31. +coherentLow :: MemBytes -> Cache4K -> Bool +coherentLow mem c = P.and [coherentAt mem s w c | s <- [0 .. 31], w <- [0 .. 3]] + +-- | Walk the cached system and the ideal one together for @n@ cycles of the +-- cached one, skipping the cached run's stall cycles -- those whose bus input is +-- not ready -- in the ideal one. Returns @\"\"@ if every stall cycle makes no +-- request and leaves the core alone, the cache stays coherent with memory, and +-- every other cycle makes the ideal run's request from the ideal run's state, up +-- to 'sameModuloCtrl'. +stutterReport :: Int -> Sys -> String +stutterReport n sys0 = go n (0 :: Int) (initCacheSys sys0 emptyCache4K) sys0 + where + go :: Int -> Int -> CacheSys RegFile MemBytes Cache4K -> Sys -> String + go 0 _ _ _ = "" + go j c cs ideal + | P.not (running core) = "" + | P.not (coherentLow (sysMem core) (cacheSysCache cs)) = failAt "the cache is not coherent with memory" "" + | P.not ready = + if obsOf oC /= NoAccess + then failAt "a stall cycle made a request: " (show (obsOf oC)) + else + -- The bus input is the memory's answer, which may arrive now. + if P.not (sameModuloCtrl (withInput (cacheSysCore cs')) core) + then failAt "a stall cycle changed the core: " (P.unwords (coreDiff core (cacheSysCore cs'))) + else go (j - 1) (c + 1) cs' ideal + | P.not (sameModuloCtrl core ideal) = failAt "the cached core left the ideal run: " (P.unwords (coreDiff ideal core)) + | obsOf oC /= obsOf oI = failAt "different requests: " (show (obsOf oC, obsOf oI)) + | otherwise = go (j - 1) (c + 1) cs' ideal' + where + core = cacheSysCore cs + ready = inputMemReady (sysInput core) + withInput (Sys st _ m) = Sys st (sysInput core) m + (cs', oC) = stepCachedOut cs + (ideal', oI) = stepSysOut ideal + failAt what detail = "\ncycle " P.++ show c P.++ ": " P.++ what P.++ detail P.++ "\n" diff --git a/test/CompositionSpec.hs b/test/CompositionSpec.hs new file mode 100644 index 0000000..3ad5cb1 --- /dev/null +++ b/test/CompositionSpec.hs @@ -0,0 +1,332 @@ +{-# LANGUAGE PackageImports #-} + +-- | The core behind a cache: what holds for any cache, and the programs and +-- traces the cache tests ("Cache4KSpec") are built from. +-- +-- The constant-time leakage proof ("Proof.Core.Leakage.Solver") is about the core +-- attached to memory that answers every request in the next cycle. Behind a +-- cache a load that misses is answered only after the miss penalty, and in the +-- meantime the core stalls. The core's side of what lets the ideal-memory result +-- carry over is checked here: after a data read the core waits +-- ('Proof.CachedCore.Obligation.waitObligation'), and a stall cycle is a stutter step +-- ('Proof.CachedCore.Obligation.stallObligation'). +module CompositionSpec + ( compositionTests, + sameModuloCtrl, + coreDiff, + ctTrace, + genByteProg, + genCTProg, + genData, + genSecretFreeProg, + genWord, + simHops, + withData, + ) +where + +import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) +import Clash.Sized.Vector (unsafeFromList) +import Core +import Data.Functor.Identity (Identity (..)) +import Core.ISA (IsaState, StepG (..), isaStep) +import Core.Instruction +import Memory.Types +import Proof.CachedCore.Obligation (stallObligation, waitObligation) +import Proof.Core.Leakage.Model +import Proof.Core.Functional.Obligation (isaAt) +import Proof.Core.Leakage.Driver (simDriver) +import Proof.Core.Leakage.Simulator (SimInput, SimState, simCircuit, simInit) +import Proof.Core.Functional.Machine +import ProofSpec (genArbSys1) +import Core.RegFile (RegFileOps) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck +import "aimcore" Types +import Prelude hiding (Ordering (..), Word, init, log, map, not, undefined, (!!), (&&), (++), (||)) +import qualified Prelude as P + +-- | Two systems equal in everything but the control lines, which +-- 'Core.withCtrlReset' overwrites before any stage reads them. +sameModuloCtrl :: Sys -> Sys -> Bool +sameModuloCtrl (Sys a ia ma) (Sys b ib mb) = + a {stateCtrl = initCtrl} == b {stateCtrl = initCtrl} + P.&& runIdentity (inputMem ia) == runIdentity (inputMem ib) + P.&& inputMemReady ia == inputMemReady ib + P.&& ma == mb + +-- | The fields, other than the control lines, on which two systems differ, as +-- @field(first | second)@. +coreDiff :: Sys -> Sys -> [String] +coreDiff (Sys a ia ma) (Sys b ib mb) = + P.concat + [ f "fePc" stateFePc, + f "dePc" stateDePc, + f "deExpInstr" stateDeExpInstr, + f "exPc" stateExPc, + f "ex" stateExInstr, + f "me" stateMeInstr, + f "meAddr" stateMeAddr, + f "meRes" (runIdentity . stateMeRes), + f "wb" stateWbInstr, + f "wbRes" (runIdentity . stateWbRes), + f "halt" stateHalt, + f "loadInFlight" stateLoadInFlight, + g "bus" (runIdentity . inputMem), + g "ready" inputMemReady, + ["registers" | stateRegFile a /= stateRegFile b], + ["memory" | ma /= mb] + ] + where + f :: (Eq v, Show v) => String -> (State Identity -> v) -> [String] + f name sel + | sel a == sel b = [] + | otherwise = [name P.++ "(" P.++ show (sel a) P.++ " | " P.++ show (sel b) P.++ ")"] + g :: (Eq v, Show v) => String -> (Input Identity -> v) -> [String] + g name sel + | sel ia == sel ib = [] + | otherwise = [name P.++ "(" P.++ show (sel ia) P.++ " | " P.++ show (sel ib) P.++ ")"] + +-- | The ISA-level constant-time leakage trace of the first @n@ instructions. +ctTrace :: Int -> IsaState -> [Leak] +ctTrace 0 _ = [] +ctTrace n a = leakOf a : case isaStep a of + Next a' -> ctTrace (n - 1) a' + IsaHalted -> [] + +-- | Load a data image (word-aligned addresses below the program) into a system. +withData :: [(Address, Word)] -> Sys -> Sys +withData ws (Sys s i m) = Sys s i (P.foldr (\(a, w) -> memWrite a Types.Word w) m ws) + +genData :: Gen [(Address, Word)] +genData = + P.mapM (\k -> (\w -> (4 * k, w)) <$> elements [0, 1, 4, 0x10, 0x40, 0xDEADBEEF]) [0 .. 49] + +-- | Random programs whose loads, stores and @jalr@s go through base registers. +-- +-- @x5@ and @x6@ are reserved as base registers: they are written only by +-- @addi@ from @x0@, with a word-aligned data address (below 'initPc') or the +-- address of an instruction of the program. Stores through them therefore also +-- hit the code, which raises store hazards; they store @x0@, so an overwritten +-- instruction decodes to @Nop DecodeFail@. Every access stays inside the +-- harness's memory. A @jalr@ off @x0@, whose target fits the immediate, is +-- generated as well. +genCTProg :: Gen (Vec PROG_SIZE Word) +genCTProg = do + n <- choose (2, 12) + body <- P.mapM (genCTInstr n) [0 .. n - 1] + let instrs = P.map roundTrips body P.++ P.replicate (50 - n) Core.Instruction.break + pure (map encode (unsafeFromList instrs)) + where + roundTrips i = case encode' i of + Just w | decode' w == i -> i + _ -> IType (Arith ADD) 0 0 0 + +genCTInstr :: Int -> Int -> Gen Instruction +genCTInstr n i = + frequency + [ (2, RType <$> genArith <*> genDst <*> genSrc <*> genSrc), + (1, IType <$> (Arith <$> genArith) <*> genDst <*> genSrc <*> genSmallImm), + (3, (\b a -> IType (Arith ADD) b 0 (fromIntegral a)) <$> genBase <*> genAddr), + ( 3, + (\size sign rd b off -> IType (Load size sign) rd b off) + <$> genSize + <*> elements [Signed, Unsigned] + <*> genDst + <*> genBase + <*> genOff + ), + (3, (\size off b -> SType size off b 0) <$> genSize <*> genOff <*> genBase), + (1, (\t -> SType Word (fromIntegral (codeAddr t)) 0 0) <$> choose (0, n)), + ( 2, + (\cmp t rs1 rs2 -> BType cmp (fromIntegral ((t - i) * 4)) rs1 rs2) + <$> elements [EQ, NE, LT, GE, LTU, GEU] + <*> choose (0, n) + <*> genSrc + <*> genSrc + ), + (1, (\rd t -> JType rd (fromIntegral ((t - i) * 4))) <$> genDst <*> choose (0, n)), + (1, (\b -> IType Jump 0 b 0) <$> genBase), + (1, (\t -> IType Jump 0 0 (fromIntegral (codeAddr t))) <$> choose (0, n)) + ] + where + genArith = elements [ADD, SUB, XOR, OR, AND, SLT, SLTU] + genSize = elements [Byte, Half, Word] + genSmallImm = fromIntegral <$> choose (0 :: Int, 15) + -- Base registers, and everything else. + genBase = elements [5, 6] + genDst = elements [1, 2, 3, 4, 7] + genSrc = elements [0, 1, 2, 3, 4, 5, 6, 7] + genOff = (\k -> fromIntegral (k * 4)) <$> choose (0 :: Int, 2) + codeAddr t = fromIntegral initPc + 4 * t :: Int + genAddr = + oneof + [ (\k -> 4 * k) <$> choose (0 :: Int, 40), + codeAddr <$> choose (0, n) + ] + +-- | Programs whose control flow and addresses never depend on loaded data. +-- +-- As 'genCTProg', with @x5@ and @x6@ the base registers, set only +-- from constants; loads write @x1@ to @x4@ and @x7@, and branches compare only +-- @x0@, @x5@ and @x6@, so no loaded value reaches a branch or an address. Stores +-- store @x0@, so no loaded value reaches memory either. +genSecretFreeProg :: Gen (Vec PROG_SIZE Word) +genSecretFreeProg = do + n <- choose (2, 12) + body <- P.mapM (genOne n) [0 .. n - 1] + let instrs = P.map roundTrips body P.++ P.replicate (50 - n) Core.Instruction.break + pure (map encode (unsafeFromList instrs)) + where + roundTrips i = case encode' i of + Just w | decode' w == i -> i + _ -> IType (Arith ADD) 0 0 0 + + genOne n i = + frequency + [ (2, RType <$> elements [ADD, SUB, XOR, OR, AND] <*> genDst <*> genAny <*> genAny), + (3, (\b a -> IType (Arith ADD) b 0 (fromIntegral a)) <$> genBase <*> genAddr n), + ( 3, + (\size sign rd b off -> IType (Load size sign) rd b off) + <$> elements [Byte, Half, Types.Word] + <*> elements [Signed, Unsigned] + <*> genDst + <*> genBase + <*> genOff + ), + (2, (\size off b -> SType size off b 0) <$> elements [Byte, Half, Types.Word] <*> genOff <*> genBase), + ( 2, + (\cmp t rs1 rs2 -> BType cmp (fromIntegral ((t - i) * 4)) rs1 rs2) + <$> elements [EQ, NE, LT, GE, LTU, GEU] + <*> choose (0, n) + <*> genCtl + <*> genCtl + ), + (1, (\rd t -> JType rd (fromIntegral ((t - i) * 4))) <$> genDst <*> choose (0, n)) + ] + + genBase = elements [5, 6] + genCtl = elements [0, 5, 6] + genDst = elements [1, 2, 3, 4, 7] + genAny = elements [0, 1, 2, 3, 4, 5, 6, 7] + genOff = (\k -> fromIntegral (k * 4)) <$> choose (0 :: Int, 2) + genAddr n = + oneof + [ (\k -> 4 * k) <$> choose (0 :: Int, 40), + (\t -> fromIntegral initPc + 4 * t) <$> choose (0, n) + ] + +-- | Programs whose loads and stores have every width and alignment, including +-- reads and writes that straddle two blocks. +-- +-- Base registers @x5@ and @x6@ are set only from constants, to data addresses, +-- so no access reaches the program; offsets are any byte offset up to 11. +-- Stores store data registers, loads write them, and branches compare them, so +-- loaded values flow back into memory and into control flow. +genByteProg :: Gen (Vec PROG_SIZE Word) +genByteProg = do + n <- choose (2, 14) + body <- P.mapM (genOne n) [0 .. n - 1] + let instrs = P.map roundTrips body P.++ P.replicate (50 - n) Core.Instruction.break + pure (map encode (unsafeFromList instrs)) + where + roundTrips i = case encode' i of + Just w | decode' w == i -> i + _ -> IType (Arith ADD) 0 0 0 + + genOne n i = + frequency + [ (2, RType <$> elements [ADD, SUB, XOR, OR, AND] <*> genDst <*> genDst <*> genDst), + (3, (\b k -> IType (Arith ADD) b 0 (fromIntegral (4 * k :: Int))) <$> genBase <*> choose (0, 40)), + ( 4, + (\size sign rd b off -> IType (Load size sign) rd b off) + <$> elements [Byte, Half, Types.Word] + <*> elements [Signed, Unsigned] + <*> genDst + <*> genBase + <*> genOff + ), + (3, (\size off b rs2 -> SType size off b rs2) <$> elements [Byte, Half, Types.Word] <*> genOff <*> genBase <*> genDst), + ( 1, + (\cmp t rs1 rs2 -> BType cmp (fromIntegral ((t - i) * 4)) rs1 rs2) + <$> elements [EQ, NE, LT, GE, LTU, GEU] + <*> choose (i + 1, n) + <*> genDst + <*> genDst + ) + ] + + genBase = elements [5, 6] + genDst = elements [1, 2, 3, 4] + genOff = fromIntegral <$> choose (0 :: Int, 11) + +genWord :: Gen Word +genWord = oneof [elements [0, 1, 0xFF, 0x1234, 0x80000000, 0xDEADBEEF], fromIntegral <$> (arbitrary :: Gen Int)] + +-- | The core's bus observations computed from the leakage alone, hop by hop, as +-- behind ideal memory: the leakage simulator ('Proof.Core.Leakage.Simulator.simCircuit') +-- run on the ISA's leakage trace. +-- +-- The hops are those of 'ProofSpec.leakReport': the first gets no leakage, and +-- every later one gets @'leakOf' isa@ on its first cycle, after which the ISA +-- steps. A halted ISA stands still. +simHops :: Sys -> [[Obs]] +simHops sys0 = go Nothing (isaAt (stateFePc (sysCore sys0)) sys0) simInit + where + go :: SimInput -> IsaState -> SimState -> [[Obs]] + go inp a sim = + let (sim', os) = runSim (simDriver inp sim + 1) inp sim + a' = case inp of + Nothing -> a + Just _ -> isaNext a + in os : go (Just (leakOf a')) a' sim' + -- The simulator for @n@ cycles; it gets @inp@ on the first only. + runSim :: Int -> SimInput -> SimState -> (SimState, [Obs]) + runSim 0 _ sim = (sim, []) + runSim n inp sim = + let (sim1, o) = simCircuit sim inp + (sim2, os) = runSim (n - 1) Nothing sim1 + in (sim2, o : os) + isaNext a = case isaStep a of + Next a' -> a' + IsaHalted -> a + +-- | A load to put into the memory stage, or none. +genMeLoad :: Gen (Maybe Instruction) +genMeLoad = + frequency + [ (1, pure Nothing), + ( 4, + (\size sign rd rs1 imm -> Just (IType (Load size sign) rd rs1 imm)) + <$> elements [Byte, Half, Types.Word] + <*> elements [Signed, Unsigned] + <*> (fromIntegral <$> choose (0 :: Int, 31)) + <*> (fromIntegral <$> choose (0 :: Int, 31)) + <*> (fromIntegral <$> choose (0 :: Int, 63)) + ) + ] + +-- | Does a cycle of the core from this state issue a data read? +issuesDataRead :: (RegFileOps r) => StateG r Identity -> Input Identity -> Bool +issuesDataRead s inp = case outMem (snd (circuit s inp)) of + Just (MemAccess False _ _ Nothing) -> True + _ -> False + +compositionTests :: TestTree +compositionTests = + testGroup + "Core behind a cache" + [ testProperty "patience: after a data read the core waits" $ + -- Arbitrary states, mostly with a load in the memory stage and none in + -- flight, so that the cycle issues a data read. + withMaxSuccess 5000 $ checkCoverage $ + forAllShow genArbSys1 (const "") $ \(Sys s0 inp _, _, _) -> + forAll genMeLoad $ \me -> + let s = maybe s0 (\ir -> s0 {stateMeInstr = ir, stateLoadInFlight = False}) me + in cover 50 (issuesDataRead s inp) "the cycle issues a data read" (waitObligation s inp), + testProperty "a stall cycle is a stutter step, on arbitrary stalled states" $ + withMaxSuccess 5000 $ + forAllShow genArbSys1 (const "") $ \(Sys st inp _, wr, _) -> + isLoad (stateWbInstr st) ==> + stallObligation wr st {stateLoadInFlight = True} inp {inputMemReady = False} + ] diff --git a/test/InstructionSpec.hs b/test/InstructionSpec.hs index 3d7f46a..b7b3129 100644 --- a/test/InstructionSpec.hs +++ b/test/InstructionSpec.hs @@ -6,7 +6,7 @@ module InstructionSpec (instructionTests) where import Clash.Prelude hiding (Ordering (..), Word, break, def, init, lift, log, resize) import Control.Monad import Data.Maybe (isJust, fromJust) -import Instruction +import Core.Instruction import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (assertBool, testCase, (@?=)) import Test.Tasty.QuickCheck diff --git a/test/IsaSpec.hs b/test/IsaSpec.hs index 29e7e57..e6e3e4c 100644 --- a/test/IsaSpec.hs +++ b/test/IsaSpec.hs @@ -3,15 +3,15 @@ -- | Direct validation of the ISA specification against the official RISC-V -- conformance suite. -- --- The refinement proof is stated against "ISA", so nothing in the proof can --- tell us whether "ISA" itself is right -- it is the thing being proved +-- The refinement proof is stated against "Core.ISA", so nothing in the proof can +-- tell us whether "Core.ISA" itself is right -- it is the thing being proved -- against. The @rv32ui@ programs in @test/rv32ui@ are an external reference, so -- running the ISA model on them and checking the suite's own pass condition is -- evidence about the specification that does not come from the implementation. -- --- Without this, the only check on "ISA" is transitive: the core passes +-- Without this, the only check on "Core.ISA" is transitive: the core passes -- @rv32ui@ (see "BenchmarkSpec") and the proof says the core refines --- "ISA". That validates the specification /through/ the implementation, +-- "Core.ISA". That validates the specification /through/ the implementation, -- which is the wrong direction. -- -- The pass condition is the one "BenchmarkSpec" applies to the core: at the @@ -20,12 +20,11 @@ module IsaSpec (isaConformanceTests) where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import qualified Data.ByteString as BS -import Data.Functor.Identity (Identity (..)) import qualified Data.Map.Strict as M import Elf.ElfLoader (baseAddr, getElfSegments, readElf, startAddr) -import ISA (IsaStateG (..), StepG (..), isaStep) +import Core.ISA (IsaStateG (..), StepG (..), isaStep) import Memory.Types (MemOps (..)) -import RegFile +import Core.RegFile import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (assertFailure, testCase) import "aimcore" Types @@ -46,7 +45,7 @@ instance MemOps MemMap where memReadWord a m = memReadByte (a + 3) m ++# memReadByte (a + 2) m ++# memReadByte (a + 1) m ++# memReadByte a m - memWriteWord size a w (MemMap m) = + memWrite a size w (MemMap m) = MemMap $ case size of Byte -> put a b0 m Half -> put (a + 1) b1 (put a b0 m) @@ -86,7 +85,7 @@ loadProgram path = do P.pure IsaState { isaPc = fromIntegral entry, - isaRegFile = modifyRF 2 (Identity sp) initRF, + isaRegFile = modifyRF 2 sp initRF, isaMem = MemMap bytes } @@ -97,8 +96,8 @@ checkPassed st | a0 P./= 0 = Left ("a0 = " P.++ show a0 P.++ ", expected 0") | otherwise = Right () where - gp = runIdentity (lookupRFg 3 (isaRegFile st)) - a0 = runIdentity (lookupRFg 10 (isaRegFile st)) + gp = (lookupRFg 3 (isaRegFile st)) + a0 = (lookupRFg 10 (isaRegFile st)) mkIsaTest :: String -> TestTree mkIsaTest name = diff --git a/test/ProofSpec.hs b/test/ProofSpec.hs index c258f60..475d990 100644 --- a/test/ProofSpec.hs +++ b/test/ProofSpec.hs @@ -1,23 +1,22 @@ {-# LANGUAGE PackageImports #-} -module ProofSpec (proofTests, progs, alignedWalk, invTrace, invReport, genProg, genArbSys, genArbSys1, genArbSys2, genArbSys3, genTakenTransfer) where +module ProofSpec (proofTests, progs, initSys, alignedWalk, invTrace, invReport, genProg, genArbSys, genArbSys1, genArbSys2, genArbSys3, genTakenTransfer) where import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log) import Clash.Sized.Vector (unsafeFromList) import Core -import Data.Functor.Identity (Identity (..), runIdentity) -import Proof.Functional.Driver hiding (loadHazard, storeHazard) -import ISA (IsaStateG (..), IsaState, StepG (..), isaStep, isaInstrAt) -import Instruction -import Proof.Functional.Invariant -import Proof.Machine -import Proof.Functional.Obligation (indStepObligation, indStepObligation1, indStepObligation2, isaAt) -import Proof.Leakage.Driver (simDriver) -import Proof.Leakage.Invariant (simInv) -import Proof.Leakage.Model (Obs, leakOf, obsOf) -import Proof.Leakage.Simulator (SimInput, SimState, simCircuit, simInit) +import Proof.Core.Functional.Driver hiding (loadHazard, storeHazard) +import Core.ISA (IsaStateG (..), IsaState, StepG (..), isaStep, isaInstrAt) +import Core.Instruction +import Proof.Core.Functional.Invariant +import Proof.Core.Functional.Machine +import Proof.Core.Functional.Obligation (indStep0, indStep1, indStep2, isaAt) +import Proof.Core.Leakage.Driver (simDriver) +import Proof.Core.Leakage.Invariant (simInv) +import Proof.Core.Leakage.Model (Obs, leakOf, obsOf) +import Proof.Core.Leakage.Simulator (SimInput, SimState, simCircuit, simInit) import Memory.Types -import RegFile +import Core.RegFile import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (assertBool, assertFailure, testCase) import Test.Tasty.QuickCheck @@ -27,12 +26,18 @@ import "aimcore" Types import Prelude hiding (Ordering (..), Word, init, log, map, not, undefined, (!!), (&&), (++), (||)) import qualified Prelude as P +-- | @n@ system steps. A harness helper: the proofs write their steps out. +stepSysN :: (RegFileOps r, MemOps m) => Int -> SysG r m -> SysG r m +stepSysN n s + | n <= 0 = s + | otherwise = stepSysN (n - 1) (stepSys s) + -- | A state the driver is meant to be evaluated in: the execute stage holds a -- real instruction. The startup state (@Nop FirstCycle@) is the one bubble the -- driver has an explicit case for. Note @Nop DecodeFail@ is /not/ a bubble -- -- see 'Proof.Machine.isBubble'. aligned :: Sys -> Bool -aligned s = not (isBubble (stateExInstr (sysState s))) || stateExInstr (sysState s) == Nop FirstCycle +aligned s = not (isBubble (stateExInstr (sysCore s))) || stateExInstr (sysCore s) == Nop FirstCycle -- | Walk the machine from aligned state to aligned state, taking -- @driver s + 1@ cycles each hop. @@ -43,7 +48,7 @@ alignedWalk k prog = go k 0 (initSys prog) go j i s = let n = driver s + 1 s' = stepSysN n s - in (i, n, s') : if stateHalt (sysState s') == Nothing then go (j - 1) (i + n) s' else [] + in (i, n, s') : if stateHalt (sysCore s') == Nothing then go (j - 1) (i + n) s' else [] -- | Hops that do not land on an aligned state. walkReport :: Int -> Vec PROG_SIZE Word -> String @@ -55,18 +60,27 @@ walkReport k prog = " took ", show n, " cycles -> ex=", - show (stateExInstr (sysState s')), + show (stateExInstr (sysCore s')), " exPc=", - show (stateExPc (sysState s')) + show (stateExPc (sysCore s')) ] | (i, n, s') <- alignedWalk k prog, not (aligned s'), - stateHalt (sysState s') == Nothing + stateHalt (sysCore s') == Nothing ] +-- | The system as it starts up, with @prog@ loaded at 'initPc'. +initSys :: Vec PROG_SIZE Word -> Sys +initSys prog = + Sys + { sysCore = Core.init, + sysInput = initInput, + sysMem = mkRAM @PROG_SIZE @RAM_SIZE_BYTES prog + } + -- | The architectural state @prog@ starts in: execution begins at 'initPc', the -- register file is zeroed, and memory holds the program. The counterpart of --- 'Proof.Machine.initSys' on the ISA side. +-- 'initSys' on the ISA side. initIsa :: Vec PROG_SIZE Word -> IsaState initIsa prog = IsaState initPc initRF (mkRAM @PROG_SIZE @RAM_SIZE_BYTES prog) @@ -95,7 +109,7 @@ baseReport prog = -- The reset state is not one of them. Its hop brings the first instruction into -- the execute stage without the ISA having executed anything, so the ISA state -- is unchanged across it and the trace starts after it, at the state --- 'Proof.Functional.Induction.baseCase' is about. Every later hop advances the +-- 'Proof.Core.Functional.Solver.baseCase' is about. Every later hop advances the -- ISA by one step. invTrace :: Int -> Vec PROG_SIZE Word -> [(Int, IsaState, Sys)] invTrace k prog = go k 0 isa0 sys0 True @@ -114,7 +128,7 @@ invTrace k prog = go k 0 isa0 sys0 True IsaHalted -> [(c', isa, sys')] Next isa' -> (c', isa', sys') - : if stateHalt (sysState sys') == Nothing then go (j - 1) c' isa' sys' False else [] + : if stateHalt (sysCore sys') == Nothing then go (j - 1) c' isa' sys' False else [] -- | The first point at which the invariant fails, with an explanation. invReport :: Int -> Vec PROG_SIZE Word -> String @@ -130,15 +144,15 @@ invReport k prog = " isaInstr=", show (isaInstrAt isa), "\n ex=", - show (stateExInstr (sysState sys)), + show (stateExInstr (sysCore sys)), " exPc=", - show (stateExPc (sysState sys)), + show (stateExPc (sysCore sys)), " me=", - show (stateMeInstr (sysState sys)), + show (stateMeInstr (sysCore sys)), " wb=", - show (stateWbInstr (sysState sys)), + show (stateWbInstr (sysCore sys)), "\n halt=", - show (stateHalt (sysState sys)), + show (stateHalt (sysCore sys)), "\n", explain isa sys ] @@ -146,7 +160,7 @@ invReport k prog = -- | The leakage simulator run alongside the core, hop by hop, on a concrete -- program. Returns the first discrepancy, or @""@ if there is none. -- --- The concrete counterpart of "Proof.Leakage.Induction", in the way 'invTrace' +-- The concrete counterpart of "Proof.Core.Leakage.Solver", in the way 'invTrace' -- is of the functional one. Both machines start from their initial states and -- take the first hop with no leakage, as in the leakage base case. After that, -- each hop feeds the simulator @'leakOf' isa@ on its first cycle and nothing @@ -177,7 +191,7 @@ leakReport k prog = Nothing -> case isaStep isa of IsaHalted -> "" Next isa' - | stateHalt (sysState sys') == Nothing -> go (j - 1) (c + n) isa' sys' sim' + | stateHalt (sysCore sys') == Nothing -> go (j - 1) (c + n) isa' sys' sim' | otherwise -> "" -- Both machines for @n@ cycles; the simulator gets @inp@ on the first only. @@ -220,7 +234,7 @@ storeHazardEx = SType Word 204 0 0 :> IType (Arith ADD) 1 0 1 :> IType (Arith ADD) 2 0 2 - :> Instruction.break + :> Core.Instruction.break :> Nil -- | Store hazard raised by the store in the /memory/ stage, one cycle later, @@ -232,7 +246,7 @@ storeHazardMe = :> SType Word 212 0 0 :> IType (Arith ADD) 2 0 2 :> IType (Arith ADD) 3 0 3 - :> Instruction.break + :> Core.Instruction.break :> Nil -- Random program generation ------------------------------------------------- @@ -260,7 +274,7 @@ genProg :: Gen (Vec PROG_SIZE Word) genProg = do n <- choose (1, 12) body <- P.mapM (genInstr n) [0 .. n - 1] - let instrs = P.map roundTrips body P.++ P.replicate (50 - n) Instruction.break + let instrs = P.map roundTrips body P.++ P.replicate (50 - n) Core.Instruction.break pure (map encode (unsafeFromList instrs)) genInstr :: Int -> Int -> Gen Instruction @@ -299,11 +313,11 @@ proofTests :: TestTree proofTests = testGroup "Driver and invariant" - [ -- The base case, on the real 'Vec'-backed reset state. 'Proof.Functional.Induction.baseCase' + [ -- The base case, on the real 'Vec'-backed reset state. 'Proof.Core.Functional.Solver.baseCase' -- proves this for an arbitrary memory, but has to substitute the register -- file (Clash's 'repeat' is opaque to the symbolic executor), so the -- concrete check is what pins that the state it describes is the one - -- 'Proof.Machine.initSys' actually produces -- including 'Core.init''s reset + -- 'Proof.Core.Functional.Machine.initSys' actually produces -- including 'Core.init''s reset -- register file and the loaded program. It also checks the reset hop's -- length against the operational reading, since 'invTrace' does not -- sample the reset state. @@ -343,12 +357,12 @@ proofTests = -- is no next non-bubble for the operational reading to find. testCase "driver agrees with its operational reading" $ let bad = - [ (driver sys, ref, stateExInstr (sysState sys)) + [ (driver sys, ref, stateExInstr (sysCore sys)) | prog <- allProgs 500, (_, _, sys) <- invTrace 40 prog, - stateHalt (sysState sys) == Nothing, + stateHalt (sysCore sys) == Nothing, aligned sys, - P.not (isEnvInstr (stateExInstr (sysState sys))), + P.not (isEnvInstr (stateExInstr (sysCore sys))), let ref = driverRef 12 sys, ref /= Just (driver sys + 1) ] @@ -391,7 +405,7 @@ proofTests = -- jump costs three cycles, so it has retired past writeback by the next -- aligned state -- and nothing else in the invariant rules it out, so this -- is the only thing constraining the @JType@ / @IType Jump@ clauses of - -- 'Proof.Functional.Invariant.flushMeStage'. It fails if those clauses + -- 'Proof.Core.Functional.Invariant.flushMeStage'. It fails if those clauses -- stop writing @rd@. testCase "inductive with a jump in the memory stage" $ let bad = [e | sys <- sampleStates 200, Just e <- [inductiveStep (withJumpInMe sys)]] @@ -408,7 +422,7 @@ proofTests = inv isa sys, wr <- [0 .. 31], wa <- [0, 16 .. 396], - P.not (invAt wr wa isa sys) + P.not (invAtList wr wa isa sys) ] in if P.null bad then pure () else assertFailure (show (P.take 5 bad)), -- The fold-free invariant is what the plugin runs on; it must agree with @@ -421,7 +435,7 @@ proofTests = (c, isa, sys) <- invTrace 40 prog, wr <- [0 .. 31], wa <- [0, 16 .. 396], - invAt wr wa isa sys /= invAtFree wr wa isa sys + invAtList wr wa isa sys /= invAt wr wa isa sys ] in if P.null bad then pure () else assertFailure (show (P.take 5 bad)), -- The fifth counterexample of the earlier proof: a store whose byte range @@ -436,13 +450,13 @@ proofTests = isa = isaFromSys sys sys' = stepSysN (driver sys P.+ 1) sys isa' = case isaStep isa of Next x -> x; IsaHalted -> isa - assertBool "state satisfies the invariant" (invAtFree wr wa isa sys) + assertBool "state satisfies the invariant" (invAt wr wa isa sys) assertBool "decode stalls on the store hazard rather than taking a one-cycle hop" (driver sys P./= 0) assertBool "the driven hop preserves the invariant" - (invAtFree wr wa isa' sys'), + (invAt wr wa isa' sys'), testProperty "inductive step on arbitrary pipeline states" $ -- 1e6 has been run by hand (60s, no counterexample); 20k keeps the -- suite fast. @@ -457,14 +471,14 @@ proofTests = sys' = stepSys sys isa' = case isaStep isa of Next x -> x; IsaHalted -> isa in counterexample - ( "me=" P.++ show (stateMeInstr (sysState sys)) - P.++ "\nwb=" P.++ show (stateWbInstr (sysState sys)) - P.++ "\nex=" P.++ show (stateExInstr (sysState sys)) - P.++ "\nexPc=" P.++ show (stateExPc (sysState sys)) + ( "me=" P.++ show (stateMeInstr (sysCore sys)) + P.++ "\nwb=" P.++ show (stateWbInstr (sysCore sys)) + P.++ "\nex=" P.++ show (stateExInstr (sysCore sys)) + P.++ "\nexPc=" P.++ show (stateExPc (sysCore sys)) P.++ " wr=" P.++ show wr P.++ " wa=" P.++ show wa P.++ "\nfailing=" P.++ show (P.map P.fst (P.filter (P.not . P.snd) (P.concatMap caseConjuncts (invCasesAt wr wa isa' sys')))) ) - (indStepObligation wr wa (stateExPc (sysState sys)) sys), + (indStep0 wr wa (stateExPc (sysCore sys)) sys), -- k = 1: the two-cycle hop, a memory instruction in writeback. The test -- below asserts generated states actually satisfy the premise, since one -- this specific is easy to miss entirely and still see a green property. @@ -476,22 +490,22 @@ proofTests = s2 = stepSysN 2 sys isa' = case isaStep isa of Next x -> x; IsaHalted -> isa in counterexample - ( "me=" P.++ show (stateMeInstr (sysState sys)) - P.++ "\nwb=" P.++ show (stateWbInstr (sysState sys)) - P.++ "\nex=" P.++ show (stateExInstr (sysState sys)) - P.++ "\nexPc=" P.++ show (stateExPc (sysState sys)) - P.++ " fePc=" P.++ show (stateFePc (sysState sys)) + ( "me=" P.++ show (stateMeInstr (sysCore sys)) + P.++ "\nwb=" P.++ show (stateWbInstr (sysCore sys)) + P.++ "\nex=" P.++ show (stateExInstr (sysCore sys)) + P.++ "\nexPc=" P.++ show (stateExPc (sysCore sys)) + P.++ " fePc=" P.++ show (stateFePc (sysCore sys)) P.++ " wr=" P.++ show wr P.++ " wa=" P.++ show wa P.++ "\nfailing=" P.++ show (P.map P.fst (P.filter (P.not . P.snd) (P.concatMap caseConjuncts (invCasesAt wr wa isa' s2)))) ) - (indStepObligation1 wr wa (stateExPc (sysState sys)) sys), + (indStep1 wr wa (stateExPc (sysCore sys)) sys), testCase "k=1 generator satisfies the premise" $ let sample = [s | (s, _, _) <- unGen (vectorOf 4000 genArbSys1) (mkQCGen 7) 30] admitted = [ () | s <- sample, driver s P.== 1, - invAtFree 1 0 (isaAt (stateExPc (sysState s)) s) s + invAt 1 0 (isaAt (stateExPc (sysCore s)) s) s ] in assertBool "no generated state satisfied the k=1 premise" (P.not (P.null admitted)), -- k = 2: jumps and the all-memory steady shape return to a running @@ -503,20 +517,20 @@ proofTests = counterexample ( "case=" P.++ label P.++ " driverCase=" P.++ driverCaseName sys - P.++ "\nme=" P.++ show (stateMeInstr (sysState sys)) - P.++ "\nwb=" P.++ show (stateWbInstr (sysState sys)) - P.++ "\nex=" P.++ show (stateExInstr (sysState sys)) - P.++ "\nexPc=" P.++ show (stateExPc (sysState sys)) + P.++ "\nme=" P.++ show (stateMeInstr (sysCore sys)) + P.++ "\nwb=" P.++ show (stateWbInstr (sysCore sys)) + P.++ "\nex=" P.++ show (stateExInstr (sysCore sys)) + P.++ "\nexPc=" P.++ show (stateExPc (sysCore sys)) P.++ " wr=" P.++ show wr P.++ " wa=" P.++ show wa ) - (indStepObligation2 wr wa (stateExPc (sysState sys)) sys), + (indStep2 wr wa (stateExPc (sysCore sys)) sys), testCase "k=2 generator reaches env, jump, and steady cases" $ let sample = [ (label, driverCaseName s) | (label, s, wr, wa) <- unGen (vectorOf 4000 genArbSys2) (mkQCGen 29) 30, driver s P.== 2, - invAtFree wr wa (isaAt (stateExPc (sysState s)) s) s + invAt wr wa (isaAt (stateExPc (sysCore s)) s) s ] has label = P.any ((P.== label) . P.fst) sample in do @@ -525,10 +539,10 @@ proofTests = assertBool "no steady k=2 state satisfied the premise" (has "steady"), testCase "jumps never occupy me/wb at a checked state" $ let bad = - [ (shape (stateMeInstr (sysState sys)), shape (stateWbInstr (sysState sys))) + [ (shape (stateMeInstr (sysCore sys)), shape (stateWbInstr (sysCore sys))) | prog <- allProgs 2000, (_, _, sys) <- invTrace 40 prog, - isJumpShape (stateMeInstr (sysState sys)) || isJumpShape (stateWbInstr (sysState sys)) + isJumpShape (stateMeInstr (sysCore sys)) || isJumpShape (stateWbInstr (sysCore sys)) ] in if P.null bad then pure () else assertFailure (show (P.take 5 bad)) ] @@ -544,9 +558,9 @@ proofTests = -- | The architectural state that makes the flush conjunct hold at @sys@ by -- construction. If @sys@ is an aligned running state, this is the ISA state the -- invariant claims it corresponds to. --- Shared with 'Proof.Functional.Induction.indStep0' via "Proof.Functional.Obligation", so the two cannot drift. +-- Shared with 'Proof.Core.Functional.Solver.indStep0' via "Proof.Core.Functional.Obligation", so the two cannot drift. isaFromSys :: (RegFileOps r, MemOps m) => SysG r m -> IsaStateG r m -isaFromSys sys = isaAt (stateExPc (sysState sys)) sys +isaFromSys sys = isaAt (stateExPc (sysCore sys)) sys -- | Take one driven step and report whether the invariant survived. Returns -- 'Nothing' when @sys@ does not satisfy the invariant to begin with (such a @@ -571,9 +585,9 @@ sampleStates n = [ sys | prog <- allProgs n, (_, _, sys) <- invTrace 40 prog, - stateHalt (sysState sys) == Nothing, + stateHalt (sysCore sys) == Nothing, aligned sys, - P.not (isEnvInstr (stateExInstr (sysState sys))) + P.not (isEnvInstr (stateExInstr (sysCore sys))) ] -- | Put a jump in the memory stage. The invariant permits this -- a jump is not @@ -581,7 +595,7 @@ sampleStates n = -- never actually occur, so nothing else in the invariant rules it out. withJumpInMe :: Sys -> Sys withJumpInMe s = - s {sysState = (sysState s) {stateMeInstr = JType 5 0, stateMeRes = pure 0x1234}} + s {sysCore = (sysCore s) {stateMeInstr = JType 5 0, stateMeRes = 0x1234}} -- The fifth counterexample, explained: address wraparound --------------------- -- @@ -597,7 +611,7 @@ withJumpInMe s = -- @0xFFFFFFFE..0x00000001@, wrapping into a low PC word without ever -- satisfying @p < a + n@. -- --- There is no assumption now: 'Instruction.storeHazard' is wrap-correct and +-- There is no assumption now: 'Core.Instruction.storeHazard' is wrap-correct and -- 'Core.decode' stalls on the overlap, so this state has to survive its hop. -- -- This state realises the mechanism concretely: the pipeline sits astride the @@ -627,7 +641,7 @@ wrapMem = MemFn bytes wrapCESys :: SysG RegFn MemFn wrapCESys = Sys - ( (sysState (initSys (mkProg prog1))) + ( (sysCore (initSys (mkProg prog1))) { stateFePc = 0x00000000, stateDePc = 0xFFFFFFFC, stateDeExpInstr = True, @@ -637,17 +651,16 @@ wrapCESys = -- its operand fields are already spent by the time it reaches the -- memory stage. stateMeInstr = SType Types.Byte 0 0 0, - stateWbInstr = Nop MemoryBusBusy, - stateMeRes = pure 0, -- the byte written: 0x00, over 0x01 - stateWbRes = pure 0, + stateWbInstr = Nop NoInstruction, + stateMeRes = 0, -- the byte written: 0x00, over 0x01 + stateWbRes = 0, stateMeAddr = 0xFFFFFFFD, -- second byte of the decode-stage word - stateRegFile = RegFn (const (pure 0)), + stateRegFile = RegFn (const 0), stateCtrl = initCtrl, - stateHalt = Nothing, - stateHaltNextPc = 0 + stateHalt = Nothing } ) - (Input (pure wrapDeWord)) + (Input (Just wrapDeWord)) wrapMem -- Arbitrary-state search ------------------------------------------------------ @@ -663,7 +676,7 @@ wrapCESys = -- -- 'stateCtrl' is left at 'initCtrl' soundly: 'Core.pipe' overwrites it at the -- start of the cycle, before any stage reads it, so the incoming value cannot --- affect 'Proof.Machine.stepSys'. +-- affect 'Proof.Core.Functional.Machine.stepSys'. -- | Instruction generators that build in the premise's constraints, rather than -- generating freely and filtering. Filtering discarded ~6 examples per hit, @@ -688,7 +701,7 @@ genNonMem = UType <$> elements [Zero, PC] <*> gr3 <*> (fromIntegral <$> choose (0 :: Int, 15)), JType <$> gr3 <*> (fromIntegral <$> choose (0 :: Int, 15)), (\rd rs i -> IType Jump rd rs i) <$> gr3 <*> gr3 <*> gi15, - P.pure (Nop MemoryBusBusy) + P.pure (Nop NoInstruction) ] -- | The decode-stage instruction. Unlike the writeback stage, nothing under @@ -743,7 +756,7 @@ genExInstr = -- immediate is kept even so 'roundTrips' preserves the shape. (\cmp t r1 r2 -> BType cmp (fromIntegral (2 * t :: Int)) r1 r2) <$> elements [EQ, NE, LT, GE, LTU, GEU] <*> choose (0, 7) <*> gr3 <*> gr3, - P.pure (Nop MemoryBusBusy) + P.pure (Nop NoInstruction) ] -- | The memory stage. A load's destination avoids the execute stage's sources, @@ -829,7 +842,7 @@ genArbSys = do wa <- unpack <$> genW let sys = Sys - ((sysState (initSys (mkProg prog1))) + ((sysCore (initSys (mkProg prog1))) { stateFePc = base + 8, stateDePc = base + 4, stateDeExpInstr = True, @@ -837,15 +850,14 @@ genArbSys = do stateExInstr = decode' w0, stateMeInstr = meI, stateWbInstr = wbI, - stateMeRes = pure mr, - stateWbRes = pure wbr, + stateMeRes = mr, + stateWbRes = wbr, stateMeAddr = ma, - stateRegFile = RegFn (P.fmap Identity rfF), + stateRegFile = RegFn rfF, stateCtrl = initCtrl, - stateHalt = Nothing, - stateHaltNextPc = 0 + stateHalt = Nothing }) - (Input (pure w1)) + (Input (Just w1)) (MemFn memf) P.pure (sys, wr, wa) @@ -853,7 +865,7 @@ genArbSys = do -- invariant admits: a memory instruction in writeback, which occupied the bus -- last cycle, so no instruction was fetched and @fePc == exPc + 4@. The reset -- state also gets a two-cycle hop, but it is not in the invariant; see --- 'Proof.Functional.Induction.baseCase'. +-- 'Proof.Core.Functional.Solver.baseCase'. genArbSys1 :: Gen (SysG RegFn MemFn, RegIdx, Address) genArbSys1 = genSteady1 @@ -907,13 +919,13 @@ genRunning2 label genEx = do -- premise is exercised rather than making those samples vacuous. let ma = base + 64 wbMem = isMemInstr wbI - inp = Input (pure (if wbMem then loaded else w1)) + inp = Input (Just (if wbMem then loaded else w1)) fePc = if wbMem then base + 4 else base + 8 wr <- genWitnessReg wa <- unpack <$> genW let sys = Sys - ( (sysState (initSys (mkProg prog1))) + ( (sysCore (initSys (mkProg prog1))) { stateFePc = fePc, stateDePc = base + 4, stateDeExpInstr = P.not wbMem, @@ -921,13 +933,12 @@ genRunning2 label genEx = do stateExInstr = decode' w0, stateMeInstr = meI, stateWbInstr = wbI, - stateMeRes = pure mr, - stateWbRes = pure wbr, + stateMeRes = mr, + stateWbRes = wbr, stateMeAddr = ma, - stateRegFile = RegFn (P.fmap Identity rfF), + stateRegFile = RegFn rfF, stateCtrl = initCtrl, - stateHalt = Nothing, - stateHaltNextPc = 0 + stateHalt = Nothing } ) inp @@ -944,7 +955,7 @@ genSteady2 = do (\op rd rs i -> IType (Arith op) rd rs i) <$> elements [ADD, XOR] <*> gr3 <*> gr3 <*> gi15, UType <$> elements [Zero, PC] <*> gr3 <*> (fromIntegral <$> choose (0 :: Int, 15)), - P.pure (Nop MemoryBusBusy) + P.pure (Nop NoInstruction) ] meI <- oneof @@ -974,7 +985,7 @@ genSteady2 = do wa <- unpack <$> genW let sys = Sys - ( (sysState (initSys (mkProg prog1))) + ( (sysCore (initSys (mkProg prog1))) { stateFePc = base + 4, stateDePc = base + 4, stateDeExpInstr = False, @@ -982,16 +993,15 @@ genSteady2 = do stateExInstr = decode' w0, stateMeInstr = meI, stateWbInstr = wbI, - stateMeRes = pure mr, - stateWbRes = pure wbr, + stateMeRes = mr, + stateWbRes = wbr, stateMeAddr = base + 64, - stateRegFile = RegFn (P.fmap Identity rfF), + stateRegFile = RegFn rfF, stateCtrl = initCtrl, - stateHalt = Nothing, - stateHaltNextPc = 0 + stateHalt = Nothing } ) - (Input (pure loaded)) + (Input (Just loaded)) (MemFn memf) P.pure ("steady", sys, wr, wa) @@ -1019,7 +1029,7 @@ genSteady1 = do wa <- unpack <$> genW let sys = Sys - ( (sysState (initSys (mkProg prog1))) + ( (sysCore (initSys (mkProg prog1))) { stateFePc = base + 4, stateDePc = base + 4, stateDeExpInstr = False, @@ -1027,16 +1037,15 @@ genSteady1 = do stateExInstr = decode' w0, stateMeInstr = meI, stateWbInstr = wbI, - stateMeRes = pure mr, - stateWbRes = pure wbr, + stateMeRes = mr, + stateWbRes = wbr, stateMeAddr = ma, - stateRegFile = RegFn (P.fmap Identity rfF), + stateRegFile = RegFn rfF, stateCtrl = initCtrl, - stateHalt = Nothing, - stateHaltNextPc = 0 + stateHalt = Nothing } ) - (Input (pure loaded)) + (Input (Just loaded)) (MemFn memf) P.pure (sys, wr, wa) @@ -1117,8 +1126,8 @@ coverage n = tally (P.concatMap observations (allProgs n)) observations prog = P.concat [ [ "driver:" P.++ driverCaseName sys, - "me:" P.++ shape (stateMeInstr (sysState sys)), - "wb:" P.++ shape (stateWbInstr (sysState sys)) + "me:" P.++ shape (stateMeInstr (sysCore sys)), + "wb:" P.++ shape (stateWbInstr (sysCore sys)) ] | (_, _, sys) <- invTrace 40 prog ] @@ -1165,7 +1174,7 @@ prog1 :: Vec 3 Instruction prog1 = IType (Arith ADD) 2 0 5 :> SType Word 0 0 2 - :> Instruction.break + :> Core.Instruction.break :> Nil prog2 :: Vec 6 Instruction @@ -1175,7 +1184,7 @@ prog2 = :> IType (Load Word Signed) 3 0 0 :> RType ADD 4 0 3 :> SType Word 4 0 4 - :> Instruction.break + :> Core.Instruction.break :> Nil prog3 :: Vec 6 Instruction @@ -1185,7 +1194,7 @@ prog3 = :> BType EQ 8 2 3 :> SType Word 0 0 2 :> SType Word 4 0 2 - :> Instruction.break + :> Core.Instruction.break :> Nil sumTo :: Int -> Vec 8 Instruction @@ -1198,7 +1207,7 @@ sumTo n = IType (Arith ADD) 1 1 (-1), JType 0 (-12), SType Word 0 0 2, - Instruction.break + Core.Instruction.break ] -- Targeted generators for the transfer and four-cycle shapes --------------------- @@ -1233,13 +1242,13 @@ genTakenTransfer useJalr = do w1 = P.maybe 0 P.id (encode' (roundTrips nextI)) wT = P.maybe 0 P.id (encode' (roundTrips tgtI)) wbMem = isMemInstr wbI - inp = Input (pure (if wbMem then loaded else w1)) + inp = Input (Just (if wbMem then loaded else w1)) fePc = if wbMem then base + 4 else base + 8 ma = base + 4096 -- parked away from every PC and from the target mkSys w0 rfun = Sys - ( (sysState (initSys (mkProg prog1))) + ( (sysCore (initSys (mkProg prog1))) { stateFePc = fePc, stateDePc = base + 4, stateDeExpInstr = P.not wbMem, @@ -1247,13 +1256,12 @@ genTakenTransfer useJalr = do stateExInstr = decode' w0, stateMeInstr = meI, stateWbInstr = wbI, - stateMeRes = pure mr, - stateWbRes = pure wbr, + stateMeRes = mr, + stateWbRes = wbr, stateMeAddr = ma, - stateRegFile = RegFn (P.fmap Identity rfun), + stateRegFile = RegFn rfun, stateCtrl = initCtrl, - stateHalt = Nothing, - stateHaltNextPc = 0 + stateHalt = Nothing } ) inp @@ -1265,7 +1273,7 @@ genTakenTransfer useJalr = do | a - target P.< 4 = byteAt wT (a - target) | P.otherwise = 0 - -- Probe the forwarded operands; 'Proof.Functional.Driver.exArg' never reads the execute + -- Probe the forwarded operands; 'Proof.Core.Functional.Driver.exArg' never reads the execute -- stage, so a provisional instruction there makes the probe exact. let probe = mkSys 0 rfF v1 = exArg probe rs1 @@ -1312,7 +1320,7 @@ genLoadHazard3 = do (\rd' -> IType Jump rd' rd 0) <$> genSmallReg, P.pure (IType (Env Call) 0 0 0), -- An @ebreak@ whose encoded rs1 is the load's destination. - -- 'Instruction.getRs1' reports that field -- it hardcodes x17 only for + -- 'Core.Instruction.getRs1' reports that field -- it hardcodes x17 only for -- @ecall@ -- so this is a genuine load-use hazard. P.pure (IType (Env Break) 0 rd 1) ] @@ -1354,7 +1362,7 @@ mk3 base exI meI wbI nextI wbMem = do | P.otherwise = 0 P.pure ( Sys - ( (sysState (initSys (mkProg prog1))) + ( (sysCore (initSys (mkProg prog1))) { stateFePc = if wbMem then base + 4 else base + 8, stateDePc = base + 4, stateDeExpInstr = P.not wbMem, @@ -1362,16 +1370,15 @@ mk3 base exI meI wbI nextI wbMem = do stateExInstr = decode' w0, stateMeInstr = meI, stateWbInstr = wbI, - stateMeRes = pure mr, - stateWbRes = pure wbr, + stateMeRes = mr, + stateWbRes = wbr, stateMeAddr = ma, - stateRegFile = RegFn (P.fmap Identity rfF), + stateRegFile = RegFn rfF, stateCtrl = initCtrl, - stateHalt = Nothing, - stateHaltNextPc = 0 + stateHalt = Nothing } ) - (Input (pure (if wbMem then loaded else w1))) + (Input (Just (if wbMem then loaded else w1))) (MemFn memf), wr, wa @@ -1402,7 +1409,7 @@ genStageInstr = P.pure (IType (Env Call) 0 0 0), IType (Env Break) 0 <$> genSmallReg <*> P.pure 1, JType <$> genSmallReg <*> (fromIntegral . (2 *) <$> choose (0 :: Int, 7)), - P.pure (Nop MemoryBusBusy), + P.pure (Nop NoInstruction), P.pure (Nop DecodeFail) ] diff --git a/test/Spec.hs b/test/Spec.hs index 0392bb9..6b9bd58 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -6,16 +6,15 @@ module Main (main) where -import Access import BenchmarkSpec (benchmarkTests) import Clash.Prelude hiding (Log, Ordering (..), Word, break, def, init, lift, log, resize) import Clash.Sized.Vector (unsafeFromList) import Control.Monad import Core import Data.Maybe (fromJust, isJust) -import Instruction +import Core.Instruction import InstructionSpec (instructionTests) -import RegFile +import Core.RegFile import Simulate import Memory.Types import Memory.Vec @@ -24,8 +23,9 @@ import qualified Proof.SMT.Sanity as Sanity #endif import qualified Prelude #ifdef SMT_PROOF -import qualified Proof.Functional.Induction -import qualified Proof.Leakage.Induction +import qualified Proof.Cache.Functional.Solver +import qualified Proof.Core.Functional.Solver +import qualified Proof.Core.Leakage.Solver #endif import IsaSpec (isaConformanceTests) import ProofSpec (proofTests) @@ -59,8 +59,8 @@ mkPureTest s (CPUTest prog expected) = -- The first three establish that the Pantomime plugin is wired in and actually -- discharging properties -- since pantomime 1821a71 an invalid property no -- longer fails the build, so the negative control has to be asserted here. --- The rest are the proofs themselves; see "Proof.Functional.Induction" and --- "Proof.Leakage.Induction". +-- The rest are the proofs themselves; see "Proof.Core.Functional.Solver" and +-- "Proof.Core.Leakage.Solver". sanityTests :: TestTree sanityTests = testGroup @@ -71,29 +71,50 @@ sanityTests = assertBool "expected a counterexample for 'bogus'" $ isJust (verdict "bogus"), testCase "array embedding round-trips" $ - lookup "arrRoundTrip" Proof.Functional.Induction.results @?= Just Nothing, + lookup "arrRoundTripP" Proof.Core.Functional.Solver.results @?= Just Nothing, testCase "shift embeddings are sane" $ - lookup "shiftsSane" Proof.Functional.Induction.results @?= Just Nothing, + lookup "shiftsSaneP" Proof.Core.Functional.Solver.results @?= Just Nothing, testCase "base case: invariant holds after the reset hop" $ - lookup "baseCase" Proof.Functional.Induction.results @?= Just Nothing, + lookup "baseCaseP" Proof.Core.Functional.Solver.results @?= Just Nothing, testCase "k = 0 inductive step is valid" $ - lookup "indStep" Proof.Functional.Induction.results @?= Just Nothing, + lookup "indStep0P" Proof.Core.Functional.Solver.results @?= Just Nothing, testCase "k = 1 inductive step is valid" $ - lookup "indStep1" Proof.Functional.Induction.results @?= Just Nothing, + lookup "indStep1P" Proof.Core.Functional.Solver.results @?= Just Nothing, testCase "k = 2 inductive step is valid" $ - lookup "indStep2" Proof.Functional.Induction.results @?= Just Nothing, + lookup "indStep2P" Proof.Core.Functional.Solver.results @?= Just Nothing, testCase "k = 3 inductive step is valid" $ - lookup "indStep3" Proof.Functional.Induction.results @?= Just Nothing, + lookup "indStep3P" Proof.Core.Functional.Solver.results @?= Just Nothing, + testCase "the invariant implies the ISA's register file is the core's, flushed" $ + lookup "regFileUnderInvP" Proof.Core.Functional.Solver.results @?= Just Nothing, + testCase "the invariant implies the ISA's memory is the core's, flushed" $ + lookup "memUnderInvP" Proof.Core.Functional.Solver.results @?= Just Nothing, testCase "leakage base case: simulator matches the first hop" $ - lookup "baseCaseLeak" Proof.Leakage.Induction.results @?= Just Nothing, + lookup "baseCaseLeakP" Proof.Core.Leakage.Solver.results @?= Just Nothing, testCase "k = 0 leakage step is valid" $ - lookup "indStepLeak" Proof.Leakage.Induction.results @?= Just Nothing, + lookup "indStepLeak0P" Proof.Core.Leakage.Solver.results @?= Just Nothing, testCase "k = 1 leakage step is valid" $ - lookup "indStepLeak1" Proof.Leakage.Induction.results @?= Just Nothing, + lookup "indStepLeak1P" Proof.Core.Leakage.Solver.results @?= Just Nothing, testCase "k = 2 leakage step is valid" $ - lookup "indStepLeak2" Proof.Leakage.Induction.results @?= Just Nothing, + lookup "indStepLeak2P" Proof.Core.Leakage.Solver.results @?= Just Nothing, testCase "k = 3 leakage step is valid" $ - lookup "indStepLeak3" Proof.Leakage.Induction.results @?= Just Nothing + lookup "indStepLeak3P" Proof.Core.Leakage.Solver.results @?= Just Nothing, + testGroup + "the 4 KiB cache answers as ideal memory, with delay" + [ testCase name $ lookup name Proof.Cache.Functional.Solver.results @?= Just Nothing + | name <- + [ "cacheArraysP", + "coherentDataP", + "coherentWriteP", + "coherentLayoutP", + "baseCaseP", + "indStep0P", + "indStep4P", + "indStep8P", + "readyUnderInvP", + "readyIdleNoWaitP", + "waitsAfterRequestP" + ] + ] ] where verdict :: String -> Maybe String @@ -288,7 +309,7 @@ instance Arbitrary Instruction where bImmGen = chooseBoundedIntegral (0, 5) jImmGen = chooseBoundedIntegral (0, 5) -instance {-# OVERLAPPING #-} (Access f) => Arbitrary (Control f) where +instance Arbitrary Control where arbitrary = Control <$> arbitrary @@ -300,36 +321,29 @@ instance {-# OVERLAPPING #-} (Access f) => Arbitrary (Control f) where <*> arbitrary <*> genMaybeRegFwd <*> genMaybeRegFwd + <*> pure False where - genAccessWord = do - isSecret <- arbitrary - word <- arbitrary - pure $ conditionalSecret isSecret word genMaybeRegFwd = do hasFwd <- arbitrary if hasFwd then do regIdx <- arbitrary - accessWord <- genAccessWord - pure $ Just (regIdx, accessWord) + word <- arbitrary + pure $ Just (regIdx, word) else pure Nothing -instance (Arbitrary a) => Arbitrary (PubSec a) where - arbitrary = oneof [Public <$> arbitrary, Secret <$> arbitrary] - instance Arbitrary Core.HaltState where arbitrary = oneof [ Core.EBreak <$> arbitrary , Core.Syscall <$> arbitrary - , pure Core.SecurityViolation ] -instance (Access f, Arbitrary (f Word)) => Arbitrary (RegFile f) where +instance Arbitrary RegFile where arbitrary = do vals <- vectorOf 31 arbitrary pure $ RegFile $ unsafeFromList vals -instance {-# OVERLAPPING #-} (Access f, Arbitrary (f Word)) => Arbitrary (Core.State f) where +instance Arbitrary Core.State where arbitrary = Core.State <$> arbitrary @@ -345,17 +359,15 @@ instance {-# OVERLAPPING #-} (Access f, Arbitrary (f Word)) => Arbitrary (Core.S <*> arbitrary <*> arbitrary <*> arbitrary - <*> arbitrary -- | Half the time a valid instruction encoding, half the time an arbitrary data -- word. Whether the core treats it as an instruction is up to the state's -- 'Core.stateDeExpInstr'. -instance {-# OVERLAPPING #-} (Access f) => Arbitrary (Input f) where +instance Arbitrary Input where arbitrary = do mem <- oneof [ fromJust <$> ((encode' <$> arbitrary) `suchThat` isJust), arbitrary ] - isSecretMem <- arbitrary - pure $ Input (conditionalSecret isSecretMem mem) + pure $ Input (Just mem)