From 5e4000da5dad0c44d12e3c92c7524b41788259d8 Mon Sep 17 00:00:00 2001 From: Kristina Date: Fri, 6 Nov 2026 15:14:37 +0100 Subject: [PATCH] Merge the invariant's two halted cases into one The halted cases for ebreak and ecall differed only in which halt state they expect. One case now checks, through haltMatches, that the halt matches the instruction at the ISA's pc. The invariant is logically unchanged: (A && rest) || (B && rest) is (A || B) && rest. Co-Authored-By: Claude Opus 5.5 --- proof/Proof/Core/Functional/Invariant.hs | 51 ++++++++++------------- proof/Proof/Core/Functional/Obligation.hs | 4 +- test/ProofSpec.hs | 4 +- 3 files changed, 25 insertions(+), 34 deletions(-) diff --git a/proof/Proof/Core/Functional/Invariant.hs b/proof/Proof/Core/Functional/Invariant.hs index bf89dbf..10f023c 100644 --- a/proof/Proof/Core/Functional/Invariant.hs +++ b/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 -------------------- diff --git a/proof/Proof/Core/Functional/Obligation.hs b/proof/Proof/Core/Functional/Obligation.hs index 017ad91..ee0f51a 100644 --- a/proof/Proof/Core/Functional/Obligation.hs +++ b/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 = diff --git a/test/ProofSpec.hs b/test/ProofSpec.hs index 4998585..fe4edf9 100644 --- a/test/ProofSpec.hs +++ b/test/ProofSpec.hs @@ -500,8 +500,8 @@ proofTests = ] 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 (\_ -> "") $ \(label, sys, wr, wa) ->