Branch for fixing the self-writing bug with overlapping non-identical addresses

.github/workflows/stack-test.yml

@@ -9,6 +9,7 @@ on:
 jobs:
   build:
     runs-on: ubuntu-latest
+    timeout-minutes: 60
 
     steps:
     - name: Checkout code
@@ -26,6 +27,7 @@ jobs:
         curl -sL "https://github.com/bitwuzla/bitwuzla/releases/download/${BITWUZLA_VERSION}/Bitwuzla-Linux-x86_64-static.zip" -o /tmp/bitwuzla.zip
         unzip -q /tmp/bitwuzla.zip -d /tmp
         sudo install -m 755 /tmp/Bitwuzla-Linux-x86_64-static/bin/bitwuzla /usr/local/bin/bitwuzla
+        sudo ln -sf /usr/local/bin/bitwuzla /usr/local/bin/z3
         rm -rf /tmp/Bitwuzla-Linux-x86_64-static /tmp/bitwuzla.zip
         bitwuzla --version
 
@@ -43,4 +45,7 @@ jobs:
       run: stack test --only-dependencies --no-nix
 
     - name: Build and run tests
+      env:
+        SBV_Z3: /usr/local/bin/bitwuzla
+        SBV_Z3_OPTIONS: "--produce-models"
       run: stack test --no-nix

.gitignore

@@ -4,4 +4,5 @@ dist-newstyle/
 *.cabal
 /log.txt
 *.log
-/scratch
+/scratch
+/bitwuzla/

app/Main.hs

@@ -225,7 +225,7 @@ runNormalMemory Options{..} elf entryOffset leakOutputHandle leakDigest finalSta
     runIOMemT mem $ loadProgram elf
 
   let initialSims = P.map (\_ -> simulator @Identity @(IOMemT IO)) [1..optNumInstances]
-  let initialStates = P.map (\(sim, mem) -> sim { circuitState = (Core.init @Identity) { Core.stateFePc = fromIntegral entryOffset, Core.stateRegFile = modifyRF 2 (pure $ ioMemInitSP mem) initRF } }) (P.zip initialSims memInstances)
+  let initialStates = P.map (\(sim, mem) -> sim { circuitState = (Core.init @Identity @RegFile) { Core.stateFePc = fromIntegral entryOffset, Core.stateRegFile = modifyRF 2 (pure $ ioMemInitSP mem) initRF } }) (P.zip initialSims memInstances)
 
   go 0 (P.zip memInstances initialStates)
   where
@@ -254,7 +254,7 @@ runNormalMemory Options{..} elf entryOffset leakOutputHandle leakDigest finalSta
               case mRet of
                 Nothing -> pure (Nothing, True)  -- exit
                 Just ret -> do
-                  let s'' = Core.init {Core.stateFePc = resumePc,
+                  let s'' = (Core.init :: Core.State Identity) {Core.stateFePc = resumePc,
                                        Core.stateRegFile = modifyRF 10 ret (Core.stateRegFile s')}
                   _ <- next s'' o
                   pure (Just Core.initInput, False)
@@ -329,7 +329,7 @@ runExecutable opts@Options{..} = do
               (secureInstrument optVerbose leakOutputHandle leakDigest finalStateRef)
               (simulator @PubSec @(SecureIOMemT IO))
                 { circuitState =
-                    (Core.init @PubSec)
+                    (Core.init @PubSec @RegFile)
                       { Core.stateFePc = fromIntegral entryOffset,
                         Core.stateRegFile = modifyRF 2 (pure $ secureIOMemInitSP secureIOMem) initRF
                       }

package.yaml

@@ -19,6 +19,29 @@ 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
+# 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:
+#
+#   SBV_Z3=/usr/local/bin/bitwuzla SBV_Z3_OPTIONS="--produce-models" stack test
+#
+# CI does exactly this: it installs bitwuzla and sets SBV_Z3 to it (see
+# .github/workflows/stack-test.yml).
+#
+# Do not add --fast: at -O0 GHC creates no unfoldings and the plugin fails with
+# "Unbound variable in symbolise" rather than reporting a failed proof.
+#
+# Turn the flag off for a quicker local build and test without a solver:
+#
+#   stack test --flag aimcore:-smt-proof
+flags:
+  smt-proof:
+    description: Discharge the symbolic proof obligations at compile time.
+    manual: true
+    default: true
+
 default-extensions:
 - BinaryLiterals
 - DataKinds
@@ -62,6 +85,7 @@ dependencies:
 - pantomime
 - pantomime-clash
 - pantomime-base
+- template-haskell
 
 ghc-options:
 - -Wall
@@ -78,8 +102,32 @@ ghc-options:
 - -fplugin Pantomime
 
 library:
-  source-dirs: src
+  source-dirs:
+    - src
+    - proof
+  when:
+    - condition: flag(smt-proof)
+      source-dirs: proof-smt
+      exposed-modules:
+        - Proof.Functional.Induction
+        - Proof.SMT.Sanity
+      cpp-options: -DSMT_PROOF
   exposed-modules:
+    - Proof.Machine
+    - Proof.Driver
+    - Proof.Functional.Invariant
+    - Proof.Functional.Obligation
+    - Proof.Leakage.Model
+    - Proof.Leakage.Simulator
+    - Proof.Leakage.Obligation
+    # Proof.Leakage.Induction: temporarily out of the build. Its four properties
+    # are invalid since the aliasing-store assumption was dropped, and the
+    # counterexample-extraction path trips a Pantomime/effectful unlifting bug
+    # ("version (2356) /= storageVersion (0)") that fails the build outright.
+    # Restore once the leakage model can express the store-hazard stall.
+    - Proof.SMT.Array
+    - Proof.SMT.Axioms
+    - Proof.SMT.Logged
     - Access
     - Core
     - Elf.ElfLoader
@@ -128,6 +176,9 @@ tests:
   aimcore-test:
     main:                Spec.hs
     source-dirs:         test
+    when:
+      - condition: flag(smt-proof)
+        cpp-options: -DSMT_PROOF
     ghc-options:
     - -threaded
     - -rtsopts
@@ -137,4 +188,4 @@ tests:
     - melf
     - bytestring
     - exceptions
-
+    - QuickCheck

proof-smt/Proof/Functional/Induction.hs

@@ -0,0 +1,203 @@
+-- | 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 an ADT of scalars ('KState') plus SMT-array
+-- register file and memory: 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").
+module Proof.Functional.Induction
+  ( -- | 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
+    -- the constructor looks dead to @-Wunused-top-binds@. It is also what a new
+    -- property in this module would take as its pipeline-state argument.
+    KState (..),
+    arrRoundTrip,
+    shiftsSane,
+    baseCase,
+    indStep0,
+    indStep1,
+    indStep2,
+    indStep3,
+    results,
+  )
+where
+
+import Proof.SMT.Array
+import Proof.SMT.Axioms (arrayAxioms)
+import Clash.Prelude hiding (Ordering (..), Word, def, init, lift, log)
+import qualified Core
+import Data.Functor.Identity
+import ISA (IsaStateG (..))
+import Instruction
+import Proof.Functional.Invariant (invAtFree)
+import Proof.SMT.Logged (pantomime)
+import Proof.Machine
+import Memory.Types (initPc)
+import Proof.Driver (driver)
+import Proof.Functional.Obligation
+import Pantomime (Theory (..))
+import qualified Pantomime.BuiltIn as Pantomime
+import Types
+import Prelude hiding (Ordering (..), Word, init, log, not, undefined, (!!), (&&), (++), (||))
+
+-- | The pipeline registers, as plain scalars.
+data KState = KState
+  { kFePc :: Address,
+    kDePc :: Address,
+    kExPc :: Address,
+    kExIr :: Instruction,
+    kMeIr :: Instruction,
+    kMeRes :: Word,
+    kMeAddr :: Address,
+    kWbIr :: Instruction,
+    kWbRes :: Word,
+    kCtrl :: Core.Control Identity,
+    kHalt :: Maybe Core.HaltState,
+    kHaltNextPc :: Address
+  }
+
+-- | Assemble a system state from the symbolic pieces.
+sysOf :: KState -> Core.Input Identity -> RegArr -> MemArr -> SysG RegArrF MemArr
+sysOf ss i ra ma =
+  Sys
+    { sysState =
+        Core.State
+          { Core.stateFePc = kFePc ss,
+            Core.stateDePc = kDePc ss,
+            Core.stateExPc = kExPc ss,
+            Core.stateExInstr = kExIr ss,
+            Core.stateMeInstr = kMeIr ss,
+            Core.stateMeRes = Identity (kMeRes ss),
+            Core.stateMeAddr = kMeAddr ss,
+            Core.stateWbInstr = kWbIr ss,
+            Core.stateWbRes = Identity (kWbRes ss),
+            Core.stateRegFile = RegArrF ra,
+            Core.stateCtrl = kCtrl ss,
+            Core.stateHalt = kHalt ss,
+            Core.stateHaltNextPc = kHaltNextPc ss
+          },
+      sysInput = i,
+      sysMem = ma
+    }
+
+-- 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 ----------------------------------------------------------------
+
+-- | The invariant holds once the reset state has taken its first hop.
+--
+-- Without this the four steps below say only that the invariant is /preserved/,
+-- which is vacuous if it never holds anywhere. Together they give the theorem:
+-- the invariant relates the core to the ISA at every state the driver lands on
+-- after reset.
+--
+-- The reset state itself is not a case of the invariant. 'Core.init' has nothing
+-- in the pipeline, so the driver gives it a two-cycle hop that fetches and
+-- decodes the first instruction without executing anything. This property
+-- states that hop directly: the driver does assign it two cycles, and after
+-- them the running case relates the core to the ISA's /initial/ state -- zero
+-- ISA steps. Handling it here rather than as a case of the invariant is what
+-- lets every inductive step retire exactly one instruction.
+--
+-- It holds for any loaded program, hence the arbitrary memory. Every field
+-- except the register file comes from 'Core.init' itself, so the reset shape
+-- cannot drift from the real one. The register file has to be substituted
+-- because 'RegFileOps.initRFg' builds a Clash 'Vec' with the opaque 'repeat'.
+--
+-- Note what that substitution costs: memory and the register file are the same
+-- symbolic values on both sides, and the reset 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 reset register file and the
+-- ISA's ('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.
+{-# ANN baseCase (Theory arrayAxioms) #-}
+baseCase :: RegArr -> MemArr -> RegIdx -> Address -> Pantomime.Bool
+baseCase ra ma wr wa =
+  Pantomime.boolean $ driver sys == 1 && invAtFree wr wa isa (stepSys (stepSys sys))
+  where
+    st = (Core.init :: Core.StateG RegArrF Identity) {Core.stateRegFile = RegArrF ra}
+    sys = Sys st Core.initInput ma
+    isa = IsaState {isaPc = initPc, isaRegFile = RegArrF ra, isaMem = ma}
+
+-- The inductive steps ----------------------------------------------------------
+
+-- | @k = 0@: the one-cycle hop (steady, writeback non-memory).
+{-# ANN indStep0 (Theory arrayAxioms) #-}
+indStep0 :: KState -> Core.Input Identity -> RegArr -> MemArr -> RegIdx -> Address -> Address -> Pantomime.Bool
+indStep0 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)),
+    ("indStep0", $(pantomime 'indStep0)),
+    ("indStep1", $(pantomime 'indStep1)),
+    ("indStep2", $(pantomime 'indStep2)),
+    ("indStep3", $(pantomime 'indStep3))
+  ]