DeciderSpec.hs

module Keiki.DeciderSpec (spec) where

import Data.Time (UTCTime (..), fromGregorian, secondsToDiffTime)
import Keiki.Core
import Keiki.Decider
import Keiki.Fixtures.UserRegistration
import Test.Hspec

-- | Same time fixture as 'Keiki.Fixtures.UserRegistrationSpec' so the
-- decider round-trip lands on the snapshot 'reconstitute' produces.
t :: Integer -> UTCTime
t s = UTCTime (fromGregorian 2026 5 1) (secondsToDiffTime s)

type Snapshot = (Email, ConfirmationCode, UTCTime, UTCTime, UTCTime)

snapshot :: RegFile UserRegRegs -> Snapshot
snapshot regs =
  ( regs ! #email,
    regs ! #confirmCode,
    regs ! #registeredAt,
    regs ! #confirmedAt,
    regs ! #deletedAt
  )

-- | The forward command sequence whose 'omega' trace matches
-- 'Keiki.Fixtures.UserRegistrationSpec.canonicalLog'. The reconstitute
-- spec fixes the events; this fixture records the inputs that produce
-- them on the User Registration edge graph.
-- EP-19 M7: the entrance now drives PotentialCustomer →
-- RequiresConfirmation in one transition emitting two events, so
-- there is no separate Continue command in the sequence.
canonicalCmds :: [UserCmd]
canonicalCmds =
  [ StartRegistration (StartRegistrationData "alice@x" "Z9F4" (t 0)),
    ResendConfirmation (ResendConfirmationData "K2P7" (t 100)),
    ConfirmAccount (ConfirmAccountData "K2P7" (t 200)),
    FulfillGDPRRequest (FulfillGDPRRequestData (t 300))
  ]

-- | Hand-computed snapshot at the end of replay. Same values as
-- 'Keiki.Fixtures.UserRegistrationSpec.expectedSnapshot' so the two
-- specs validate the same end-state from opposite directions.
expectedSnapshot :: Snapshot
expectedSnapshot =
  ( "alice@x",
    "K2P7",
    t 100, -- registeredAt rotated by ResendConfirmation
    t 200, -- confirmedAt
    t 300 -- deletedAt
  )

-- | Run one decide/evolve round on the (s, regs) pair: the façade
-- emits zero or one event (on the state-refinement form), and
-- 'evolve' folds the (zero or one) event back into the state.
runRound ::
  Decider
    UserCmd
    UserEvent
    (Vertex, RegFile UserRegRegs)
    (InFlight Vertex UserEvent, RegFile UserRegRegs) ->
  (Vertex, RegFile UserRegRegs) ->
  UserCmd ->
  (Vertex, RegFile UserRegRegs)
runRound d acc cmd = foldl (evolve d) acc (decide d cmd acc)

spec :: Spec
spec = do
  describe "toDecider userReg" $ do
    it "round-trips the canonical command sequence to (Deleted, expectedSnapshot)" $ do
      let d = toDecider userReg
          (sFinal, regsFinal) = foldl (runRound d) (initialState d) canonicalCmds
      (sFinal, snapshot regsFinal) `shouldBe` (Deleted, expectedSnapshot)

    it "isTerminal d reports True after the canonical sequence" $ do
      let d = toDecider userReg
          end = foldl (runRound d) (initialState d) canonicalCmds
      isTerminal d end `shouldBe` True

    it "decide on the very first command emits the multi-event chain [RegistrationStarted, ConfirmationEmailSent]" $ do
      -- EP-19 M7: the entrance is now a length-2 multi-event edge,
      -- so decide returns both events from StartRegistration in
      -- declaration order.
      let d = toDecider userReg
          evs = decide d (head canonicalCmds) (initialState d)
      length evs `shouldBe` 2
      case evs of
        [RegistrationStarted _, ConfirmationEmailSent _] -> pure ()
        _ -> expectationFailure ("unexpected event sequence: " <> show evs)

    it "ε-edge limitation: GDPR from RequiresConfirmation yields [] from decide" $ do
      -- Drive the aggregate to RequiresConfirmation by chunk-replaying
      -- StartRegistration's two-event chain, then attempt the silent
      -- ε-edge (FulfillGDPRRequest before the user has confirmed).
      let d = toDecider userReg
          startCmd = StartRegistration (StartRegistrationData "bob@x" "S0E1" (t 0))
          startEvs = decide d startCmd (initialState d)
          preGdpr = case applyEvents userReg (initialState d) startEvs of
            Just sR -> sR
            Nothing -> error "applyEvents on the 2-event chain failed"
          gdprCmd = FulfillGDPRRequest (FulfillGDPRRequestData (t 999))
          evs = decide d gdprCmd preGdpr
          afterGdpr = foldl (evolve d) preGdpr evs
      length startEvs `shouldBe` 2
      fst preGdpr `shouldBe` RequiresConfirmation
      evs `shouldBe` []
      -- The ε-edge limitation: with no event, evolve is a no-op, so
      -- the façade leaves the state at RequiresConfirmation even
      -- though the keiki delta would transition to Deleted.
      fst afterGdpr `shouldBe` RequiresConfirmation

    it "ε-edge cross-check: delta does transition the same input to Deleted" $ do
      -- Companion to the previous case: confirm that the keiki
      -- transducer itself can drive the ε-edge via 'delta'. The point
      -- is that the limitation lives at the façade boundary, not in
      -- the underlying transducer.
      let d = toDecider userReg
          startCmd = StartRegistration (StartRegistrationData "carol@x" "T1V2" (t 0))
          startEvs = decide d startCmd (initialState d)
          preGdpr = case applyEvents userReg (initialState d) startEvs of
            Just sR -> sR
            Nothing -> error "applyEvents on the 2-event chain failed"
          (vAtRC, regsAtRC) = preGdpr
          gdprCmd = FulfillGDPRRequest (FulfillGDPRRequestData (t 999))
      vAtRC `shouldBe` RequiresConfirmation
      case delta userReg vAtRC regsAtRC gdprCmd of
        Just (vNext, _) -> vNext `shouldBe` Deleted
        Nothing -> expectationFailure "delta returned Nothing"

  describe "evolveStreaming (EP-19 M5)" $ do
    it "Settled PotentialCustomer ⊢ RegistrationStarted → InFlight RequiresConfirmation [ConfirmationEmailSent]" $ do
      -- After EP-19 M7 collapsed the entrance into a length-2
      -- multi-event edge, streaming replay through its head event
      -- transitions to the mid-chain wrapper carrying the expected
      -- tail event. The second event then unwraps to Settled.
      let d = toDecider userReg
          (_, regs0) = initialState d
          ev =
            RegistrationStarted
              (RegistrationStartedData "dave@x" "U2V3" (t 0))
      case evolveStreaming d (Settled PotentialCustomer, regs0) ev of
        Just (InFlight RequiresConfirmation [ConfirmationEmailSent _], _) -> pure ()
        Just (other, _) ->
          expectationFailure ("expected InFlight RequiresConfirmation [...], got " <> show other)
        Nothing -> expectationFailure "evolveStreaming returned Nothing"

    it "Settled Confirmed ⊢ AccountDeleted → Settled Deleted" $ do
      let d = toDecider userReg
          (_, regs0) = initialState d
          ev = AccountDeleted (AccountDeletedData "x@y" (t 200))
      case evolveStreaming d (Settled Confirmed, regs0) ev of
        Just (Settled Deleted, _) -> pure ()
        other -> expectationFailure ("unexpected: " <> show (fmap fst other))