Harness.hs

{-# LANGUAGE OverloadedLabels #-}
-- @generated by keiro-dsl 0.12.0.0 (language keiro-dsl 5) from aggregate Reservation; do not edit.
module Generated.DomainOutcomes.Reservation.Harness (harnessAssertions) where

import Generated.DomainOutcomes.Reservation.Domain
import Generated.DomainOutcomes.Reservation.Codec (encodeReservationEvent, parseReservationEvent, reservationCodec)
import Generated.DomainOutcomes.Reservation.Transducer (reservationTransducer)
import Keiki.Core (applyEventsEither, defaultValidationOptions, step, validateTransducer, (!))
import Keiro.Codec (eventType)

-- | (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 reservationTransducer))
  -- clock-free: spec samples no wall clock (verified at scaffold time)
  , ("golden round-trip: Cancelled", roundTrips sampleEventCancelled)
  , ("accepts Cancel from ReservationEligible", acceptCancel)
  ]
  ++ forwardReplayCancel

roundTrips :: ReservationEvent -> Bool
roundTrips e = parseReservationEvent (eventType reservationCodec e) (encodeReservationEvent e) == Right e

sampleEventCancelled :: ReservationEvent
sampleEventCancelled = Cancelled (CancelledData "sample-requestId")

acceptCancel :: Bool
acceptCancel =
  case step reservationTransducer (ReservationEligible, initialReservationRegs) (Cancel (CancelData "sample-requestId")) of
    Just (v, _, _) -> v == ReservationCancelledState
    Nothing -> False

-- forward/replay equality (plan 147): cross the persisted codec boundary,
-- replay the emitted chain, and compare the final vertex and every register.
forwardReplayCancel :: [(String, Bool)]
forwardReplayCancel =
  case step reservationTransducer (ReservationEligible, initialReservationRegs) (Cancel (CancelData "sample-requestId")) of
    Nothing -> [(prefix <> "forward step accepted", False)]
    Just (forwardVertex, forwardRegs, emitted) ->
      case mapM (\event -> parseReservationEvent (eventType reservationCodec event) (encodeReservationEvent event)) emitted of
        Left _ -> [(prefix <> "emitted chain decodes", False)]
        Right decodedEvents ->
          case applyEventsEither reservationTransducer (ReservationEligible, initialReservationRegs) decodedEvents of
            Left _ -> [(prefix <> "replay succeeds", False)]
            Right (replayVertex, replayRegs) ->
              [ (prefix <> "final vertex", replayVertex == forwardVertex)
              , (prefix <> "register lastRequestId", (replayRegs ! #lastRequestId) == (forwardRegs ! #lastRequestId))
              ]
  where
    prefix = "forward/replay equality: Cancel from ReservationEligible -- "