BehaviorContract.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedLabels #-}
{-# OPTIONS_GHC -Wno-missing-signatures -Wno-name-shadowing #-}
-- @generated by keiro-dsl; do not edit. Regenerated from the .keiro spec.
module Generated.BehaviorComplete.Journey.BehaviorContract where

import Generated.BehaviorComplete.Journey.Codec (encodeJourneyEvent, parseJourneyEvent, journeyCodec)
import Generated.BehaviorComplete.Journey.Domain
import Generated.BehaviorComplete.Journey.Transducer (journeyTransducer)
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 :: !JourneyVertex
  , requirementCommandName :: !Text
  , requirementExpectedEdge :: !(Maybe (K.EdgeRef JourneyVertex))
  , requirementTarget :: !(Maybe JourneyVertex)
  , requirementEventKinds :: ![Text]
  , requirementLine :: !Int
  }
  deriving stock (Eq, Show)

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

data LiveExpectation
  = Emits (NonEmpty JourneyEvent)
  | Rejects RejectionClass
  | NoOp
  deriving stock (Eq, Show)

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

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

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

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 =
  [ BehaviorRequirement (BehaviorKey "behavior-v1-2e1fd6b9580e1a3d") RequiredRejection GeneratedAuthoritative GuardNotApplicable JourneyClosed "Ping" Nothing Nothing [] 21
  , BehaviorRequirement (BehaviorKey "behavior-v1-2f3ebf37a55781db") LiveTransition GeneratedAuthoritative GuardTotal JourneyActive "Decide" (Just (K.EdgeRef JourneyActive 0)) (Just JourneyActive) ["DecisionRecorded"] 41
  , BehaviorRequirement (BehaviorKey "behavior-v1-37578058289e05a9") LiveTransition GeneratedAuthoritative GuardTotal JourneyEmpty "Start" (Just (K.EdgeRef JourneyEmpty 0)) (Just JourneyActive) ["Started"] 36
  , BehaviorRequirement (BehaviorKey "behavior-v1-43b8fc7fa48595dd") RequiredRejection GeneratedAuthoritative GuardNotApplicable JourneyActive "Start" Nothing Nothing [] 21
  , BehaviorRequirement (BehaviorKey "behavior-v1-68e75665b789892c") LiveTransition GeneratedAuthoritative GuardUnknown JourneyActive "Retire" (Just (K.EdgeRef JourneyActive 3)) (Just JourneyClosed) ["Retired", "RetirementAudited"] 56
  , BehaviorRequirement (BehaviorKey "behavior-v1-7ea811586a738ee5") RequiredRejection GeneratedAuthoritative GuardNotApplicable JourneyClosed "Decide" Nothing Nothing [] 21
  , BehaviorRequirement (BehaviorKey "behavior-v1-83b0a46823e1a788") RequiredRejection GeneratedAuthoritative GuardNotApplicable JourneyEmpty "Ping" Nothing Nothing [] 21
  , BehaviorRequirement (BehaviorKey "behavior-v1-926739ffb27d20e7") RequiredRejection GeneratedAuthoritative GuardNotApplicable JourneyEmpty "Retire" Nothing Nothing [] 21
  , BehaviorRequirement (BehaviorKey "behavior-v1-ba7053f86d15e1b0") RequiredRejection GeneratedAuthoritative GuardNotApplicable JourneyEmpty "Decide" Nothing Nothing [] 21
  , BehaviorRequirement (BehaviorKey "behavior-v1-be8b08a049ab4d8b") RequiredRejection GeneratedAuthoritative GuardNotApplicable JourneyClosed "Start" Nothing Nothing [] 21
  , BehaviorRequirement (BehaviorKey "behavior-v1-db1a553baa3eda84") LiveTransition GeneratedAuthoritative GuardTotal JourneyActive "Decide" (Just (K.EdgeRef JourneyActive 1)) (Just JourneyActive) ["DecisionRecorded"] 47
  , BehaviorRequirement (BehaviorKey "behavior-v1-ea258e9c47d66aac") LiveTransition GeneratedAuthoritative GuardTotal JourneyActive "Ping" (Just (K.EdgeRef JourneyActive 2)) (Just JourneyActive) [] 53
  , BehaviorRequirement (BehaviorKey "behavior-v1-f0fbe3a3ba0b40e8") ReplayTransition GeneratedAuthoritative GuardNotApplicable JourneyActive "Retire" (Just (K.EdgeRef JourneyActive 4)) (Just JourneyClosed) ["Retired", "RetirementAudited"] 63
  , BehaviorRequirement (BehaviorKey "behavior-v1-f9cae2bf4c0d0562") RequiredRejection GeneratedAuthoritative GuardNotApplicable JourneyClosed "Retire" Nothing Nothing [] 21
  ]

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 = [failure | (_, Left failure) <- 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: Journey"
  , "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 failure) <> " [" <> failureCode failure <> "] " <> failureDetail failure | failure <- 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 -> [JourneyEvent] -> JourneyCommand -> 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 requirement seed command expectation = case expectation of
  Emits _ -> failure requirement "expectation-kind" "a rejection requirement cannot expect emitted events"
  NoOp -> failure requirement "expectation-kind" "a rejection requirement cannot expect an accepted no-op"
  Rejects expectedClass -> case K.stepDetailedEither journeyTransducer 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 requirement seed command expectation = case expectation of
  Rejects _ -> failure requirement "expectation-kind" "a live-transition requirement needs Emits or NoOp"
  NoOp -> case K.stepDetailedEither journeyTransducer seed command of
    Left stepFailure -> failure requirement "unexpected-rejection" (tshow stepFailure)
    Right success -> do
      checkAcceptedEnvelope requirement success
      ensure requirement (null (K.stepSuccessOutputs success)) "noop-emitted" "NoOp emitted one or more events"
      ensure requirement (K.stepSuccessState success == fst seed) "noop-vertex-change" "NoOp changed the control vertex"
      ensure requirement (regsEqual (K.stepSuccessRegs success) (snd seed)) "noop-register-change" "NoOp changed one or more registers"
  Emits expectedEvents -> case K.stepDetailedEither journeyTransducer 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"
      ensure requirement (map eventKind actual == requirementEventKinds requirement) "event-envelope-mismatch" "runtime event kinds differ from the declared ordered envelope"
      decoded <- either (failure requirement "emitted-codec-decode") Right (decodeEvents actual)
      replayed <- case K.applyEventsDetailedEither journeyTransducer 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)

checkAcceptedEnvelope requirement success = do
  ensure requirement (K.stepSuccessMode success == K.Live) "forward-mode" "forward execution selected a non-live edge"
  ensure requirement (Just (K.stepSuccessEdge success) == requirementExpectedEdge requirement) "edge-attribution" "runtime selected a different guarded sibling"
  ensure requirement (Just (K.stepSuccessState success) == requirementTarget requirement) "target-mismatch" "runtime reached a different target vertex"

runReplay :: BehaviorRequirement -> [JourneyEvent] -> [JourneyEvent] -> 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 journeyTransducer (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"
    checkSingleAttribution requirement K.ReplayOnly (length decoded) (K.replaySuccessTrace replayed)
  _ -> failure requirement "witness-kind" "ReplayWitness supplied for a non-replay requirement"

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"
    ensure requirement (K.replayAttributionMode attribution == expectedMode) "replay-mode-attribution" "replay selected the wrong live/replay-only phase"
    ensure requirement (K.replayAttributionSource attribution == requirementSource requirement) "replay-source-attribution" "replay attribution starts at the wrong source"
    ensure requirement (Just (K.replayAttributionTarget attribution) == requirementTarget requirement) "replay-target-attribution" "replay attribution ends at the wrong target"
    ensure requirement (K.replayAttributionSpan attribution == K.ReplayEventSpan 0 eventCount) "replay-span-attribution" "replay attribution did not consume the exact chunk"
  _ -> failure requirement "replay-trace-cardinality" "expected exactly one completed-edge attribution"

settleHistory requirement label history = do
  decoded <- either (failure requirement (label <> "-codec-decode")) Right (decodeEvents history)
  case K.applyEventsDetailedEither journeyTransducer (JourneyEmpty, initialJourneyRegs) decoded of
    Left replayFailure -> failure requirement (label <> "-replay-failed") (tshow replayFailure)
    Right replaySuccess -> Right replaySuccess

decodeEvents :: [JourneyEvent] -> Either Text [JourneyEvent]
decodeEvents = traverse (\event -> parseJourneyEvent (Codec.eventType journeyCodec event) (encodeJourneyEvent event))

commandKind command = case command of
  Start _ -> "Start"
  Decide _ -> "Decide"
  Ping _ -> "Ping"
  Retire _ -> "Retire"

eventKind event = case Codec.eventType journeyCodec event of Codec.EventType tag -> tag

regsEqual :: K.RegFile JourneyRegs -> K.RegFile JourneyRegs -> Bool
regsEqual left right = (left K.! #lastAmount) == (right K.! #lastAmount)

proofStrength requirement =
  requirementEvidence requirement == GeneratedAuthoritative
    && requirementGuardCoverage requirement `elem` [GuardTotal, GuardNotApplicable]

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

isPending Pending {} = True
isPending _ = False

ensure requirement condition code detail = if condition then Right () else failure requirement code detail
failure requirement code detail = Left (BehaviorFailure (requirementKey requirement) code detail)
sortedKeys = sortOn unBehaviorKey
keyTexts = map unBehaviorKey
countLine label values = label <> ": " <> tshow (length values)
tshow :: Show value => value -> Text
tshow = T.pack . show