BehaviorContract.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.BehaviorContract
  ( BehaviorKey (..)
  , ObligationKind (..)
  , EvidenceLevel (..)
  , GuardCoverage (..)
  , BehaviorRequirement (..)
  , RejectionClass (..)
  , LiveExpectation (..)
  , BehaviorWitness (..)
  , BehaviorFailure (..)
  , BehaviorConformanceReport (..)
  , behaviorRequirements
  , behaviorCoverageReport
  , behaviorConformancePassed
  , behaviorConformancePassedWith
  , renderBehaviorConformanceText
  ) where

import Generated.DomainOutcomes.Reservation.Codec (encodeReservationEvent, parseReservationEvent, reservationCodec)
import Generated.DomainOutcomes.Reservation.Domain
import Generated.DomainOutcomes.Reservation.Transducer (reservationTransducer)
import Generated.DomainOutcomes.BehaviorSourceMap qualified as BehaviorSourceMap
import Generated.DomainOutcomes.Reservation.EventStream (reservationDomainCommandHandler)
import Generated.DomainOutcomes.Nominals (ReservationNoOp, ReservationRejection)
import Keiro.Command (DomainCommandHandler (..), SilentCommandContext (..), SilentDomainDecision (..))
import Data.Aeson (ToJSON (..), object, (.=))
import Data.List (sortOn)
import Data.List.NonEmpty (NonEmpty)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
import Data.Text (Text)
import Data.Text qualified as T
import Keiki.Core qualified as K (EdgeMode (..), EdgeRef (..), RegFile, ReplayAttribution (..), ReplayEventSpan (..), ReplaySuccess (..), StepFailure (..), StepSuccess (..), applyEventsDetailedEither, stepDetailedEither, (!))
import Keiro.Codec qualified as Codec (Codec (eventType), EventType (..))

newtype BehaviorKey = BehaviorKey { unBehaviorKey :: Text }
  deriving stock (Eq, Ord, Show)

data ObligationKind = LiveTransition | RequiredRejection | ReplayTransition
  deriving stock (Eq, Ord, Show)

data EvidenceLevel = GeneratedAuthoritative | HoleWitnessed | LegacyRuntimeWitness
  deriving stock (Eq, Ord, Show)

data GuardCoverage = GuardTotal | GuardPartial | GuardUnknown | GuardNotApplicable
  deriving stock (Eq, Ord, Show)

data BehaviorRequirement = BehaviorRequirement
  { requirementKey :: !BehaviorKey
  , requirementKind :: !ObligationKind
  , requirementEvidence :: !EvidenceLevel
  , requirementGuardCoverage :: !GuardCoverage
  , requirementSource :: !ReservationVertex
  , requirementCommandName :: !Text
  , requirementExpectedEdge :: !(Maybe (K.EdgeRef ReservationVertex))
  , requirementTarget :: !(Maybe ReservationVertex)
  , requirementEventKinds :: ![Text]
  }
  deriving stock (Eq, Show)

data RejectionClass = RejectNoOutgoingEdges | RejectNoMatchingEdge
  deriving stock (Eq, Show)

data LiveExpectation
  = Emits (NonEmpty ReservationEvent)
  | Rejects RejectionClass
  | RejectedWith ReservationRejection
  | NoOpWith ReservationNoOp
  | NoOp
  deriving stock (Eq, Show)

data BehaviorWitness
  = Pending BehaviorKey
  | LiveWitness
      { witnessKey :: BehaviorKey
      , witnessHistory :: [ReservationEvent]
      , witnessCommand :: ReservationCommand
      , witnessExpected :: LiveExpectation
      }
  | ReplayWitness
      { witnessKey :: BehaviorKey
      , witnessHistoryPrefix :: [ReservationEvent]
      , witnessObservedChunk :: [ReservationEvent]
      }
  deriving stock (Eq, Show)

data BehaviorFailure = BehaviorFailure
  { failureKey :: !BehaviorKey
  , failureSubject :: !Text
  , failureCode :: !Text
  , failureDetail :: !Text
  }
  deriving stock (Eq, Show)

instance ToJSON BehaviorFailure where
  toJSON behaviorFailure = object
    [ "key" .= unBehaviorKey (failureKey behaviorFailure)
    , "subject" .= failureSubject behaviorFailure
    , "code" .= failureCode behaviorFailure
    , "detail" .= failureDetail behaviorFailure
    ]

data BehaviorConformanceReport = BehaviorConformanceReport
  { reportRequired :: ![BehaviorKey]
  , reportFilled :: ![BehaviorKey]
  , reportPending :: ![BehaviorKey]
  , reportMissing :: ![BehaviorKey]
  , reportDuplicate :: ![BehaviorKey]
  , reportStale :: ![BehaviorKey]
  , reportFailed :: ![BehaviorFailure]
  , reportVerified :: ![BehaviorKey]
  , reportUnverified :: ![BehaviorKey]
  }
  deriving stock (Eq, Show)

instance ToJSON BehaviorConformanceReport where
  toJSON report = object
    [ "schema" .= ("keiro/behavior-conformance/1" :: Text)
    , "required" .= keyTexts (reportRequired report)
    , "filled" .= keyTexts (reportFilled report)
    , "pending" .= keyTexts (reportPending report)
    , "missing" .= keyTexts (reportMissing report)
    , "duplicate" .= keyTexts (reportDuplicate report)
    , "stale" .= keyTexts (reportStale report)
    , "failed" .= reportFailed report
    , "verified" .= keyTexts (reportVerified report)
    , "unverified" .= keyTexts (reportUnverified report)
    ]

behaviorRequirements :: [BehaviorRequirement]
behaviorRequirements =
  [ -- ReservationEligible x Cancel: live transition
    BehaviorRequirement
      { requirementKey = BehaviorKey "behavior-v1-0b1588f69a27bc77"
      , requirementKind = LiveTransition
      , requirementEvidence = GeneratedAuthoritative
      , requirementGuardCoverage = GuardTotal
      , requirementSource = ReservationEligible
      , requirementCommandName = "Cancel"
      , requirementExpectedEdge = (Just (K.EdgeRef ReservationEligible 0))
      , requirementTarget = Just ReservationCancelledState
      , requirementEventKinds = ["Cancelled"]
      }
  , -- ReservationCancelledState x Cancel: live transition
    BehaviorRequirement
      { requirementKey = BehaviorKey "behavior-v1-316c9e96fc1a94b1"
      , requirementKind = LiveTransition
      , requirementEvidence = GeneratedAuthoritative
      , requirementGuardCoverage = GuardTotal
      , requirementSource = ReservationCancelledState
      , requirementCommandName = "Cancel"
      , requirementExpectedEdge = (Just (K.EdgeRef ReservationCancelledState 0))
      , requirementTarget = Just ReservationCancelledState
      , requirementEventKinds = []
      }
  , -- ReservationCancelledState x Cancel: live transition
    BehaviorRequirement
      { requirementKey = BehaviorKey "behavior-v1-fd391b55fbbfa640"
      , requirementKind = LiveTransition
      , requirementEvidence = GeneratedAuthoritative
      , requirementGuardCoverage = GuardTotal
      , requirementSource = ReservationCancelledState
      , requirementCommandName = "Cancel"
      , requirementExpectedEdge = (Just (K.EdgeRef ReservationCancelledState 1))
      , requirementTarget = Just ReservationCancelledState
      , requirementEventKinds = []
      }
  ]

behaviorCoverageReport :: [BehaviorWitness] -> BehaviorConformanceReport
behaviorCoverageReport witnesses =
  BehaviorConformanceReport
    { reportRequired = sortedKeys (Map.keys requiredByKey)
    , reportFilled = sortedKeys [key | (key, [witness]) <- Map.toList witnessGroups, Map.member key requiredByKey, not (isPending witness)]
    , reportPending = sortedKeys [key | (key, rows) <- Map.toList witnessGroups, Map.member key requiredByKey, any isPending rows]
    , reportMissing = sortedKeys [key | key <- Map.keys requiredByKey, Map.notMember key witnessGroups]
    , reportDuplicate = sortedKeys [key | (key, rows) <- Map.toList witnessGroups, length rows > 1]
    , reportStale = sortedKeys [key | key <- Map.keys witnessGroups, Map.notMember key requiredByKey]
    , reportFailed = sortOn (unBehaviorKey . failureKey) failures
    , reportVerified = sortedKeys [requirementKey requirement | (requirement, Right ()) <- executions, proofStrength requirement]
    , reportUnverified = sortedKeys [requirementKey requirement | (requirement, Right ()) <- executions, not (proofStrength requirement)]
    }
 where
  requiredByKey = Map.fromList [(requirementKey requirement, requirement) | requirement <- behaviorRequirements]
  witnessGroups = Map.fromListWith (flip (<>)) [(behaviorWitnessKey witness, [witness]) | witness <- witnesses]
  executions =
    [ (requirement, runWitness requirement witness)
    | (key, [witness]) <- Map.toList witnessGroups
    , not (isPending witness)
    , Just requirement <- [Map.lookup key requiredByKey]
    ]
  failures = [behaviorFailure | (_, Left behaviorFailure) <- executions]

behaviorConformancePassed :: BehaviorConformanceReport -> Bool
behaviorConformancePassed = behaviorConformancePassedWith False

behaviorConformancePassedWith :: Bool -> BehaviorConformanceReport -> Bool
behaviorConformancePassedWith failOnUnverified report =
  null (reportPending report)
    && null (reportMissing report)
    && null (reportDuplicate report)
    && null (reportStale report)
    && null (reportFailed report)
    && (not failOnUnverified || null (reportUnverified report))

renderBehaviorConformanceText :: BehaviorConformanceReport -> Text
renderBehaviorConformanceText report = T.unlines
  [ "behavior conformance: Reservation"
  , "schema: keiro/behavior-conformance/1"
  , countLine "required" (reportRequired report)
  , countLine "filled" (reportFilled report)
  , countLine "pending" (reportPending report)
  , countLine "missing" (reportMissing report)
  , countLine "duplicate" (reportDuplicate report)
  , countLine "stale" (reportStale report)
  , "failed: " <> tshow (length (reportFailed report))
  , countLine "verified" (reportVerified report)
  , countLine "unverified" (reportUnverified report)
  ] <> T.unlines ["FAIL " <> unBehaviorKey (failureKey behaviorFailure) <> " " <> failureSubject behaviorFailure <> " [" <> failureCode behaviorFailure <> "] " <> failureDetail behaviorFailure | behaviorFailure <- reportFailed report]

runWitness :: BehaviorRequirement -> BehaviorWitness -> Either BehaviorFailure ()
runWitness requirement witness = case witness of
  Pending _ -> failure requirement "pending" "witness is still Pending"
  LiveWitness _ history command expectation -> runLive requirement history command expectation
  ReplayWitness _ prefix chunk -> runReplay requirement prefix chunk

runLive :: BehaviorRequirement -> [ReservationEvent] -> ReservationCommand -> LiveExpectation -> Either BehaviorFailure ()
runLive requirement history command expectation = do
  settled <- settleHistory requirement "history" history
  ensure requirement (K.replaySuccessState settled == requirementSource requirement) "history-wrong-source" "history does not settle at the required source vertex"
  ensure requirement (commandKind command == requirementCommandName requirement) "command-mismatch" "witness command constructor does not match the required state/command cell"
  case requirementKind requirement of
    ReplayTransition -> failure requirement "witness-kind" "a replay-only requirement needs ReplayWitness"
    RequiredRejection -> runRejection requirement (K.replaySuccessState settled, K.replaySuccessRegs settled) command expectation
    LiveTransition -> runAcceptance requirement (K.replaySuccessState settled, K.replaySuccessRegs settled) command expectation

runRejection :: BehaviorRequirement -> (ReservationVertex, K.RegFile ReservationRegs) -> ReservationCommand -> LiveExpectation -> Either BehaviorFailure ()
runRejection requirement seed command expectation = case expectation of
  Emits _ -> failure requirement "expectation-kind" "a rejection requirement cannot expect emitted events"
  RejectedWith _ -> failure requirement "expectation-kind" "an unmatched-command rejection cannot expect a selected domain rejection"
  NoOpWith _ -> failure requirement "expectation-kind" "an unmatched-command rejection cannot expect a selected domain no-op"
  NoOp -> failure requirement "expectation-kind" "a rejection requirement cannot expect an accepted no-op"
  Rejects expectedClass -> case K.stepDetailedEither reservationTransducer seed command of
    Left K.NoOutgoingEdges {} -> ensure requirement (expectedClass == RejectNoOutgoingEdges) "rejection-class" "expected NoMatchingEdge but runtime returned NoOutgoingEdges"
    Left K.NoMatchingEdge {} -> ensure requirement (expectedClass == RejectNoMatchingEdge) "rejection-class" "expected NoOutgoingEdges but runtime returned NoMatchingEdge"
    Left K.AmbiguousEdges {} -> failure requirement "ambiguous-edges" "AmbiguousEdges can never satisfy a rejection witness"
    Right _ -> failure requirement "unexpected-acceptance" "runtime accepted a command required to reject"

runAcceptance :: BehaviorRequirement -> (ReservationVertex, K.RegFile ReservationRegs) -> ReservationCommand -> LiveExpectation -> Either BehaviorFailure ()
runAcceptance requirement seed command expectation = case expectation of
  Rejects _ -> failure requirement "expectation-kind" "a live-transition requirement needs Emits or NoOp"
  RejectedWith expectedReason -> do
    decision <- runSilentDecision requirement seed command
    case decision of
      SilentRejected actualReason -> ensure requirement (actualReason == expectedReason) "domain-rejection-reason" ("selected rejection reason differs; actual=" <> tshow actualReason <> " expected=" <> tshow expectedReason)
      SilentNoOp actualReason -> failure requirement "domain-outcome-kind" ("expected a selected rejection but classifier returned no-op " <> tshow actualReason)
  NoOpWith expectedReason -> do
    decision <- runSilentDecision requirement seed command
    case decision of
      SilentRejected actualReason -> failure requirement "domain-outcome-kind" ("expected a selected no-op but classifier returned rejection " <> tshow actualReason)
      SilentNoOp actualReason -> ensure requirement (actualReason == expectedReason) "domain-noop-reason" ("selected no-op reason differs; actual=" <> tshow actualReason <> " expected=" <> tshow expectedReason)
  NoOp -> failure requirement "expectation-kind" "an outcome-enabled transition requires RejectedWith or NoOpWith exact reason evidence"
  Emits expectedEvents -> case K.stepDetailedEither reservationTransducer seed command of
    Left stepFailure -> failure requirement "unexpected-rejection" (tshow stepFailure)
    Right success -> do
      checkAcceptedEnvelope requirement success
      let expected = NonEmpty.toList expectedEvents
          actual = K.stepSuccessOutputs success
      ensure requirement (actual == expected) "event-value-mismatch" ("runtime event values differ from the exact witness expectation; actual=" <> tshow actual <> " expected=" <> tshow expected)
      ensure requirement (map eventKind actual == requirementEventKinds requirement) "event-envelope-mismatch" ("runtime event kinds differ from the declared ordered envelope; actual=" <> tshow (map eventKind actual) <> " expected=" <> tshow (requirementEventKinds requirement))
      decoded <- either (failure requirement "emitted-codec-decode") Right (decodeEvents actual)
      replayed <- case K.applyEventsDetailedEither reservationTransducer seed decoded of
        Left replayFailure -> failure requirement "emitted-replay-failed" (tshow replayFailure)
        Right replaySuccess -> Right replaySuccess
      ensure requirement (K.replaySuccessState replayed == K.stepSuccessState success) "forward-replay-vertex" "decoded emissions replay to a different vertex"
      ensure requirement (regsEqual (K.replaySuccessRegs replayed) (K.stepSuccessRegs success)) "forward-replay-registers" "decoded emissions replay to different registers"
      checkSingleAttribution requirement K.Live (length decoded) (K.replaySuccessTrace replayed)

runSilentDecision
  :: BehaviorRequirement
  -> (ReservationVertex, K.RegFile ReservationRegs)
  -> ReservationCommand
  -> Either BehaviorFailure (SilentDomainDecision ReservationRejection ReservationNoOp)
runSilentDecision requirement seed command = case K.stepDetailedEither reservationTransducer seed command of
  Left stepFailure -> failure requirement "unexpected-rejection" (tshow stepFailure)
  Right success -> do
    checkAcceptedEnvelope requirement success
    ensure requirement (null (K.stepSuccessOutputs success)) "silent-emitted" "typed silent outcome emitted one or more events"
    ensure requirement (K.stepSuccessState success == fst seed) "silent-vertex-change" "typed silent outcome changed the control vertex"
    ensure requirement (regsEqual (K.stepSuccessRegs success) (snd seed)) "silent-register-change" "typed silent outcome changed one or more registers"
    case reservationDomainCommandHandler of
      DomainCommandHandler _ classify ->
        Right (classify (SilentCommandContext (fst seed) (snd seed) command (K.stepSuccessEdge success)))

checkAcceptedEnvelope :: BehaviorRequirement -> K.StepSuccess ReservationRegs ReservationVertex ReservationEvent -> Either BehaviorFailure ()
checkAcceptedEnvelope requirement success = do
  ensure requirement (K.stepSuccessMode success == K.Live) "forward-mode" ("forward execution selected a non-live edge; actual=" <> tshow (K.stepSuccessMode success) <> " expected=" <> tshow K.Live)
  ensure requirement (Just (K.stepSuccessEdge success) == requirementExpectedEdge requirement) "edge-attribution" ("runtime selected a different guarded sibling; actual=" <> tshow (Just (K.stepSuccessEdge success)) <> " expected=" <> tshow (requirementExpectedEdge requirement))
  ensure requirement (Just (K.stepSuccessState success) == requirementTarget requirement) "target-mismatch" ("runtime reached a different target vertex; actual=" <> tshow (Just (K.stepSuccessState success)) <> " expected=" <> tshow (requirementTarget requirement))

runReplay :: BehaviorRequirement -> [ReservationEvent] -> [ReservationEvent] -> Either BehaviorFailure ()
runReplay requirement prefix chunk = case requirementKind requirement of
  ReplayTransition -> do
    settled <- settleHistory requirement "history-prefix" prefix
    ensure requirement (K.replaySuccessState settled == requirementSource requirement) "history-wrong-source" "history prefix does not settle at the replay edge source"
    ensure requirement (not (null chunk)) "empty-replay-chunk" "a replay-only edge has no observable empty chunk"
    decoded <- either (failure requirement "replay-chunk-codec-decode") Right (decodeEvents chunk)
    replayed <- case K.applyEventsDetailedEither reservationTransducer (K.replaySuccessState settled, K.replaySuccessRegs settled) decoded of
      Left replayFailure -> failure requirement "replay-chunk-failed" (tshow replayFailure)
      Right replaySuccess -> Right replaySuccess
    ensure requirement (Just (K.replaySuccessState replayed) == requirementTarget requirement) "target-mismatch" ("replay chunk reached a different target vertex; actual=" <> tshow (Just (K.replaySuccessState replayed)) <> " expected=" <> tshow (requirementTarget requirement))
    checkSingleAttribution requirement K.ReplayOnly (length decoded) (K.replaySuccessTrace replayed)
  _ -> failure requirement "witness-kind" "ReplayWitness supplied for a non-replay requirement"

checkSingleAttribution :: BehaviorRequirement -> K.EdgeMode -> Int -> [K.ReplayAttribution ReservationVertex] -> Either BehaviorFailure ()
checkSingleAttribution requirement expectedMode eventCount trace = case trace of
  [attribution] -> do
    ensure requirement (Just (K.replayAttributionEdge attribution) == requirementExpectedEdge requirement) "replay-edge-attribution" ("replay selected a different edge; actual=" <> tshow (Just (K.replayAttributionEdge attribution)) <> " expected=" <> tshow (requirementExpectedEdge requirement))
    ensure requirement (K.replayAttributionMode attribution == expectedMode) "replay-mode-attribution" ("replay selected the wrong live/replay-only phase; actual=" <> tshow (K.replayAttributionMode attribution) <> " expected=" <> tshow expectedMode)
    ensure requirement (K.replayAttributionSource attribution == requirementSource requirement) "replay-source-attribution" ("replay attribution starts at the wrong source; actual=" <> tshow (K.replayAttributionSource attribution) <> " expected=" <> tshow (requirementSource requirement))
    ensure requirement (Just (K.replayAttributionTarget attribution) == requirementTarget requirement) "replay-target-attribution" ("replay attribution ends at the wrong target; actual=" <> tshow (Just (K.replayAttributionTarget attribution)) <> " expected=" <> tshow (requirementTarget requirement))
    ensure requirement (K.replayAttributionSpan attribution == K.ReplayEventSpan 0 eventCount) "replay-span-attribution" ("replay attribution did not consume the exact chunk; actual=" <> tshow (K.replayAttributionSpan attribution) <> " expected=" <> tshow (K.ReplayEventSpan 0 eventCount))
  _ -> failure requirement "replay-trace-cardinality" "expected exactly one completed-edge attribution"

settleHistory :: BehaviorRequirement -> Text -> [ReservationEvent] -> Either BehaviorFailure (K.ReplaySuccess ReservationRegs ReservationVertex)
settleHistory requirement label history = do
  decoded <- either (failure requirement (label <> "-codec-decode")) Right (decodeEvents history)
  case K.applyEventsDetailedEither reservationTransducer (ReservationEligible, initialReservationRegs) decoded of
    Left replayFailure -> failure requirement (label <> "-replay-failed") (tshow replayFailure)
    Right replaySuccess -> Right replaySuccess

decodeEvents :: [ReservationEvent] -> Either Text [ReservationEvent]
decodeEvents = traverse (\event -> parseReservationEvent (Codec.eventType reservationCodec event) (encodeReservationEvent event))

commandKind :: ReservationCommand -> Text
commandKind command = case command of
  Cancel _ -> "Cancel"

eventKind :: ReservationEvent -> Text
eventKind event = case Codec.eventType reservationCodec event of Codec.EventType tag -> tag

regsEqual :: K.RegFile ReservationRegs -> K.RegFile ReservationRegs -> Bool
regsEqual left right = (left K.! #lastRequestId) == (right K.! #lastRequestId)

proofStrength :: BehaviorRequirement -> Bool
proofStrength requirement =
  requirementEvidence requirement == GeneratedAuthoritative
    && requirementGuardCoverage requirement `elem` [GuardTotal, GuardNotApplicable]

behaviorWitnessKey :: BehaviorWitness -> BehaviorKey
behaviorWitnessKey witness = case witness of
  Pending key -> key
  LiveWitness { witnessKey = key } -> key
  ReplayWitness { witnessKey = key } -> key

isPending :: BehaviorWitness -> Bool
isPending Pending {} = True
isPending _ = False

ensure :: BehaviorRequirement -> Bool -> Text -> Text -> Either BehaviorFailure ()
ensure requirement condition code detail = if condition then Right () else failure requirement code detail
failure :: BehaviorRequirement -> Text -> Text -> Either BehaviorFailure failed
failure requirement code detail =
  Left
    ( BehaviorFailure
        (requirementKey requirement)
        (tshow (requirementSource requirement) <> " x " <> requirementCommandName requirement <> ": " <> kindPhrase <> " (" <> BehaviorSourceMap.renderBehaviorSourceLocation (unBehaviorKey (requirementKey requirement)) <> ")")
        code
        detail
    )
 where
  kindPhrase = case requirementKind requirement of
    LiveTransition -> "live transition"
    RequiredRejection -> "required rejection"
    ReplayTransition -> "replay-only transition"
sortedKeys :: [BehaviorKey] -> [BehaviorKey]
sortedKeys = sortOn unBehaviorKey
keyTexts :: [BehaviorKey] -> [Text]
keyTexts = map unBehaviorKey
countLine :: Text -> [BehaviorKey] -> Text
countLine label values = label <> ": " <> tshow (length values)
tshow :: Show value => value -> Text
tshow = T.pack . show