Insecure core with stall support, src/Core layout, and the 4 KiB cache's functional proof

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"
 

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 <https://github.com/githubuser/aimcore#readme>
 
-# 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