Cache leakage proof, link 2 restored, and the cache tests

app/Main.hs

@@ -4,7 +4,7 @@ import Clash.Prelude hiding (Log, Ordering (..), Word, break, def, init, lift, l
 import Control.Exception (catch)
 import Control.Monad (when)
 import Control.Monad.IO.Class (MonadIO, liftIO)
-import qualified Core as Core
+import qualified Core.Pipeline as Core
 import Data.IORef
 import Elf.ElfLoader
 import Elf.Syscall (ProgramExitException (..), handleSyscall)

package.yaml

@@ -108,13 +108,18 @@ library:
   when:
     - condition: flag(smt-proof)
       exposed-modules:
-        - Proof.Cache.Functional.Solver
+        - Proof.Memory.Cache4K.Server.Functional.Solver
+        - Proof.Memory.Cache4K.Server.Leakage.Solver
+        - Proof.Memory.Cache4K.CachedCore.Functional.Solver
+        - Proof.Memory.Cache4K.CachedCore.Leakage.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.Core.SMT.Array
+        - Proof.Core.SMT.Axioms
+        - Proof.Memory.Cache4K.SMT.Array
+        - Proof.Memory.Cache4K.SMT.Axioms
+        - Proof.Memory.Cache4K.SMT.Coherent
         - Proof.SMT.Logged
         - Proof.SMT.Sanity
         - Proof.Core.Functional.System
@@ -123,11 +128,24 @@ library:
   # live in proof/ too, and must only be built with the smt-proof flag.
   other-modules: []
   exposed-modules:
-    - Proof.Cache.Functional.Contract
-    - Proof.Cache.Functional.Driver
-    - Proof.Cache.Functional.Invariant
-    - Proof.Cache.Functional.Obligation
-    - Proof.Cache.SMT.Raw
+    - Proof.Memory.Cache4K.Server.Functional.Contract
+    - Proof.Memory.Cache4K.Server.Functional.Driver
+    - Proof.Memory.Cache4K.Server.Functional.Invariant
+    - Proof.Memory.Cache4K.Server.Functional.Obligation
+    - Proof.Memory.Cache4K.Server.Leakage.Driver
+    - Proof.Memory.Cache4K.Server.Leakage.Invariant
+    - Proof.Memory.Cache4K.Server.Leakage.Model
+    - Proof.Memory.Cache4K.Server.Leakage.Obligation
+    - Proof.Memory.Cache4K.Server.Leakage.Simulator
+    - Proof.Memory.Cache4K.CachedCore.Functional.Driver
+    - Proof.Memory.Cache4K.CachedCore.Functional.Invariant
+    - Proof.Memory.Cache4K.CachedCore.Functional.Machine
+    - Proof.Memory.Cache4K.CachedCore.Functional.Obligation
+    - Proof.Memory.Cache4K.CachedCore.Leakage.Driver
+    - Proof.Memory.Cache4K.CachedCore.Leakage.Invariant
+    - Proof.Memory.Cache4K.CachedCore.Leakage.Obligation
+    - Proof.Memory.Cache4K.CachedCore.Leakage.Simulator
+    - Proof.Memory.Cache4K.SMT.Raw
     - Proof.SMT.Array
     - Proof.Core.Functional.Machine
     - Proof.Core.Functional.Driver
@@ -138,12 +156,13 @@ library:
     - Proof.Core.Leakage.Driver
     - Proof.Core.Leakage.Invariant
     - Proof.Core.Leakage.Obligation
-    - Core
     - Elf.ElfLoader
     - Elf.Syscall
     - HardwareSim
+    - Core.Alu
     - Core.Instruction
     - Core.ISA
+    - Core.Pipeline
     - Memory.Types
     - Memory.Ideal
     - Memory.Vec
@@ -173,10 +192,10 @@ 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
+      - Cache4KSpec
+      - CacheProofSpec
       - InstructionSpec
       - IsaSpec
       - ProofSpec