Harness.hs

{-# LANGUAGE OverloadedLabels #-}
-- @generated by keiro-dsl 0.21.0.0 (language keiro-dsl 6) from aggregate Lifecycle; do not edit.
module Generated.MappedRegisterConstruction.Lifecycle.Harness (harnessAssertions) where

import Generated.MappedRegisterConstruction.Lifecycle.Domain
import Generated.MappedRegisterConstruction.Lifecycle.Codec (encodeLifecycleEvent, parseLifecycleEvent, lifecycleCodec)
import Generated.MappedRegisterConstruction.Lifecycle.Transducer (lifecycleTransducer)
import Keiki.Core (applyEventsEither, defaultValidationOptions, step, validateTransducer, (!))
import Keiro.Codec (eventType)
import Data.Time.Calendar (fromGregorian)
import Data.Time.Clock (UTCTime (..), picosecondsToDiffTime)

-- | (label, passed). A driver runs these and exits non-zero on any False,
-- naming the failing assertion. Filling a hole wrongly turns a specific
-- entry False; the scaffold cannot.
harnessAssertions :: [(String, Bool)]
harnessAssertions =
  [ ("validateTransducer is empty", null (validateTransducer defaultValidationOptions lifecycleTransducer))
  -- clock-free: spec samples no wall clock (verified at scaffold time)
  , ("golden round-trip: Created", roundTrips sampleEventCreated)
  , ("golden round-trip: Marked", roundTrips sampleEventMarked)
  , ("golden round-trip: Pinged", roundTrips sampleEventPinged)
  , ("golden round-trip: Awakened", roundTrips sampleEventAwakened)
  , ("golden round-trip: ClosedEvent", roundTrips sampleEventClosedEvent)
  , ("golden round-trip: Reopened", roundTrips sampleEventReopened)
  , ("accepts Create from LifecycleEmpty", acceptCreate)
  ]
  ++ forwardReplayCreate

roundTrips :: LifecycleEvent -> Bool
roundTrips e = parseLifecycleEvent (eventType lifecycleCodec e) (encodeLifecycleEvent e) == Right e

sampleTime :: UTCTime
sampleTime = UTCTime (fromGregorian 2026 1 2) (picosecondsToDiffTime 11045123456789012)

sampleEventCreated :: LifecycleEvent
sampleEventCreated = Created (CreatedData False)

sampleEventMarked :: LifecycleEvent
sampleEventMarked = Marked (MarkedData sampleTime)

sampleEventPinged :: LifecycleEvent
sampleEventPinged = Pinged (PingedData sampleTime)

sampleEventAwakened :: LifecycleEvent
sampleEventAwakened = Awakened (AwakenedData sampleTime)

sampleEventClosedEvent :: LifecycleEvent
sampleEventClosedEvent = ClosedEvent (ClosedEventData sampleTime)

sampleEventReopened :: LifecycleEvent
sampleEventReopened = Reopened (ReopenedData sampleTime)

acceptCreate :: Bool
acceptCreate =
  case step lifecycleTransducer (LifecycleEmpty, initialLifecycleRegs) (Create (CreateData False)) of
    Just (v, _, _) -> v == LifecycleAwake
    Nothing -> False

-- forward/replay equality (plan 147): cross the persisted codec boundary,
-- replay the emitted chain, and compare the final vertex and every register.
forwardReplayCreate :: [(String, Bool)]
forwardReplayCreate =
  case step lifecycleTransducer (LifecycleEmpty, initialLifecycleRegs) (Create (CreateData False)) of
    Nothing -> [(prefix <> "forward step accepted", False)]
    Just (forwardVertex, forwardRegs, emitted) ->
      case mapM (\event -> parseLifecycleEvent (eventType lifecycleCodec event) (encodeLifecycleEvent event)) emitted of
        Left _ -> [(prefix <> "emitted chain decodes", False)]
        Right decodedEvents ->
          case applyEventsEither lifecycleTransducer (LifecycleEmpty, initialLifecycleRegs) decodedEvents of
            Left _ -> [(prefix <> "replay succeeds", False)]
            Right (replayVertex, replayRegs) ->
              [ (prefix <> "final vertex", replayVertex == forwardVertex)
              , (prefix <> "register dormantSince", (replayRegs ! #dormantSince) == (forwardRegs ! #dormantSince))
              , (prefix <> "register automatic", (replayRegs ! #automatic) == (forwardRegs ! #automatic))
              ]
  where
    prefix = "forward/replay equality: Create from LifecycleEmpty -- "