Merge the invariant's two halted cases into one

proof/Proof/Core/Functional/Invariant.hs

@@ -2,8 +2,8 @@
 -- | The functional-correctness invariant.
 --
 -- 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
+-- a system state @((core state), (input), mem)@. It is a disjunction of two
+-- cases: one for the running core, and one for the halted core. The reset state is
 -- not among them: 'Proof.Core.Functional.Solver.baseCase' steps it two cycles,
 -- into the running case, instead.
 --
@@ -175,8 +175,7 @@ invCasesGen ::
   [Case]
 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))
+    haltedCase
   ]
   where
     inputWord = fromMaybe 0 (inputMem inp)
@@ -244,11 +243,10 @@ invCasesGen eqRF eqMem (IsaState ipc irf imem) (Sys core inp mem) =
     -- @isaPc + 4@ is 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 =
+    haltedCase =
       Case
-        name
-        [ ("isa instruction is of this kind", isKind isaInstr),
-          ("halt state matches", stateHalt core == Just expected),
+        "halted"
+        [ ("halt state matches the isa instruction", haltMatches ipc isaInstr (stateHalt core)),
           ("wb == Nop Halted", stateWbInstr core == Nop Halted),
           ("memory answered", isJust (inputMem inp)),
           ("me == Nop Halted", stateMeInstr core == Nop Halted),
@@ -271,19 +269,15 @@ invAt ::
   Bool
 invAt wr wa isa sys =
   runningCaseAt wr wa isa sys
-    || haltedCaseAt HaltBreak wr wa isa sys
-    || haltedCaseAt HaltCall wr wa isa sys
-
--- | Which of the two halted cases: @ebreak@ or @ecall@.
-data HaltKind = HaltBreak | HaltCall
+    || haltedCaseAt wr wa isa sys
 
 -- | The running case.
 runningCaseAt ::
   (RegFileOps r, MemOps m) =>
   RegIdx -> Address -> IsaStateG r m -> SysG r m -> Bool
 runningCaseAt wr wa (IsaState ipc irf imem) (Sys core inp mem) =
-  stateHalt core == Nothing
-    && isJust (inputMem inp)
+  isJust (inputMem inp)    
+    && stateHalt core == Nothing
     && not (isEnvInstr (stateWbInstr core))
     && not (isEnvInstr (stateMeInstr core))
     && stateExPc core == ipc
@@ -318,28 +312,25 @@ runningCaseAt wr wa (IsaState ipc irf imem) (Sys core inp mem) =
             (mem, stateRegFile core)
         )
 
--- | One halted case.
+-- | The 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 core inp mem) =
-  isKind (decode' (memReadWord ipc imem))
-    && stateHalt core == Just expected
+  RegIdx -> Address -> IsaStateG r m -> SysG r m -> Bool
+haltedCaseAt wr wa (IsaState ipc irf imem) (Sys core inp mem) =
+  isJust (inputMem inp)
+    && haltMatches ipc (decode' (memReadWord ipc imem)) (stateHalt core)
     && stateWbInstr core == Nop Halted
-    && isJust (inputMem inp)
     && stateMeInstr core == Nop Halted
     && stateExInstr core == Nop Halted
     && memReadByte wa imem == memReadByte wa mem
     && lookupRFg wr irf == lookupRFg wr (stateRegFile core)
-  where
-    isKind =
-      case kind of
-        HaltBreak -> isBreak
-        HaltCall -> isCall
-    expected =
-      case kind of
-        HaltBreak -> EBreak (ipc + 4)
-        HaltCall -> Syscall (ipc + 4)
+
+-- | The core has halted on the instruction @ir@ at @pc@: on an @ebreak@ with
+-- an 'EBreak', on an @ecall@ with a 'Syscall', resuming at @pc + 4@.
+haltMatches :: Address -> Instruction -> Maybe HaltState -> Bool
+haltMatches pc ir halt =
+  (isBreak ir && halt == Just (EBreak (pc + 4)))
+    || (isCall ir && halt == Just (Syscall (pc + 4)))
 
 -- The architectural state, and properties of the invariant --------------------
 

proof/Proof/Core/Functional/Obligation.hs

@@ -78,7 +78,7 @@ baseCase wr wa pc rf mem =
 --
 -- @driver == 0@ covers two shapes: a running state whose hop retires one
 -- instruction, and a halted one. The @IsaHalted@ branch is what says the halted
--- core stands still -- the halted cases of the invariant require the
+-- core stands still -- the halted case of the invariant requires the
 -- architectural register file and memory to equal the core's, so carrying the
 -- same @isa@ across the step asserts that neither changed.
 indStep0 ::
@@ -128,7 +128,7 @@ indStep1 wr wa sys =
 --
 -- 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.
+-- core reaches the halted case of the invariant.
 indStep2 ::
   (RegFileOps r, MemOps m) => RegIdx -> Address -> SysG r m -> Bool
 indStep2 wr wa sys =

test/ProofSpec.hs

@@ -327,7 +327,7 @@
               then pure ()
               else assertFailure (P.unlines [n P.++ ":\n" P.++ baseReport prog | (n, prog) <- progs, P.elem n bad]),
       testProperty "invariant holds after the reset hop for any program" $
         withMaxSuccess 2000 $
           forAll genProg $ \prog ->
             counterexample (baseReport prog) (baseHolds prog),
       testGroup
@@ -368,12 +368,12 @@
           | (name, prog) <- progs
         ],
       testProperty "simulator matches the core on random programs" $
         withMaxSuccess 2000 $
           forAll genProg $ \prog ->
             let r = leakReport 40 prog
              in counterexample (show prog P.++ "\n" P.++ r) (P.null r),
       testProperty "driver and invariant on random programs" $
         withMaxSuccess 2000 $
           forAll genProg $ \prog ->
             let r = checkProg 40 prog
              in counterexample (show prog P.++ "\n" P.++ r) (P.null r),
@@ -391,7 +391,7 @@
       -- On reachable states, the driven step preserves the invariant.
       testCase "inductive on reachable states" $
         let bad = [e | sys <- sampleStates 200, Just e <- [inductiveStep sys]]
          in if P.null bad then pure () else assertFailure (P.head bad),
       -- A jump spliced into the memory stage. No reachable state has one -- a
       -- 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
@@ -400,7 +400,7 @@
       -- stop writing @rd@.
       testCase "inductive with a jump in the memory stage" $
         let bad = [e | sys <- sampleStates 200, Just e <- [inductiveStep (withJumpInMe sys)]]
          in if P.null bad then pure () else assertFailure (P.head bad),
       -- The pointwise form is what symbolic execution uses, since function-backed
       -- register files and memories have no decidable equality. It must agree
       -- with the container form wherever the latter holds, or the witness
@@ -456,7 +456,7 @@
         -- extended to wrapping memory layouts, boundary-straddling PCs,
         -- near-PC store addresses, and branches/memory ops in decode: 25s,
         -- no counterexample.
         withMaxSuccess 20000 $
           forAllShow genArbSys (\_ -> "<state; see counterexample below>") $ \(sys, wr, wa) ->
             let isa = isaFromSys sys
                 sys' = stepSys sys
@@ -475,7 +475,7 @@
       -- this specific is easy to miss entirely and still see a green property.
       testProperty "k=1 inductive step on arbitrary pipeline states" $
         -- 1e6 run by hand: 23s, no counterexample. 20k keeps the suite fast.
         withMaxSuccess 20000 $
           forAllShow genArbSys1 (\_ -> "<state; see counterexample below>") $ \(sys, wr, wa) ->
             let isa = isaFromSys sys
                 s2 = stepSysN 2 sys
@@ -491,7 +491,7 @@
                   )
                   (indStep1 wr wa sys),
       testCase "k=1 generator satisfies the premise" $
         let sample = [s | (s, _, _) <- unGen (vectorOf 4000 genArbSys1) (mkQCGen 7) 30]
             admitted =
               [ ()
                 | s <- sample,
@@ -500,11 +500,11 @@
               ]
          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
-      -- invariant case after three core cycles; ecall/ebreak return to one of
-      -- the two halted cases.
+      -- invariant case after three core cycles; ecall/ebreak reach the halted
+      -- case.
       testProperty "k=2 inductive step on arbitrary pipeline states" $
         withMaxSuccess 20000 $
           forAllShow genArbSys2 (\_ -> "<k=2 state; see counterexample below>") $ \(label, sys, wr, wa) ->
             counterexample
               ( "case=" P.++ label
                   P.++ " driverCase=" P.++ driverCaseName sys