BehaviorContract.hs

-- @generated by keiro-dsl 0.11.0.0 (language keiro-dsl 4) from aggregate Surge; do not edit.
module SkelProcess.Generated.MyService.Surge.BehaviorContract
  ( BehaviorKey (..)
  , ObligationKind (..)
  , EvidenceLevel (..)
  , GuardCoverage (..)
  , BehaviorRequirement (..)
  , RejectionClass (..)
  , LiveExpectation (..)
  , BehaviorWitness (..)
  , BehaviorFailure (..)
  , BehaviorConformanceReport (..)
  , behaviorRequirements
  , behaviorCoverageReport
  , behaviorConformancePassed
  , behaviorConformancePassedWith
  , renderBehaviorConformanceText
  ) where

import SkelProcess.Generated.MyService.Surge.Codec (encodeSurgeEvent, parseSurgeEvent, surgeCodec)
import SkelProcess.Generated.MyService.Surge.Domain
import SkelProcess.Generated.MyService.Surge.Transducer (surgeTransducer)
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 Text
  deriving stock (Eq, Ord, Show)

unBehaviorKey :: BehaviorKey -> Text
unBehaviorKey (BehaviorKey value) = value

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
  { key :: !BehaviorKey
  , kind :: !ObligationKind
  , evidence :: !EvidenceLevel
  , guardCoverage :: !GuardCoverage
  , source :: !SurgeVertex
  , commandName :: !Text
  , expectedEdge :: !(Maybe (K.EdgeRef SurgeVertex))
  , target :: !(Maybe SurgeVertex)
  , eventKinds :: ![Text]
  , line :: !Int
  }
  deriving stock (Eq, Show)

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

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

data BehaviorWitness
  = Pending BehaviorKey
  | LiveWitness
      { key :: BehaviorKey
      , history :: [SurgeEvent]
      , command :: SurgeCommand
      , expected :: LiveExpectation
      }
  | ReplayWitness
      { key :: BehaviorKey
      , historyPrefix :: [SurgeEvent]
      , observedChunk :: [SurgeEvent]
      }
  deriving stock (Eq, Show)

data BehaviorFailure = BehaviorFailure
  { key :: !BehaviorKey
  , subject :: !Text
  , code :: !Text
  , detail :: !Text
  }
  deriving stock (Eq, Show)

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

data BehaviorConformanceReport = BehaviorConformanceReport
  { required :: ![BehaviorKey]
  , filled :: ![BehaviorKey]
  , pending :: ![BehaviorKey]
  , missing :: ![BehaviorKey]
  , duplicate :: ![BehaviorKey]
  , stale :: ![BehaviorKey]
  , failed :: ![BehaviorFailure]
  , verified :: ![BehaviorKey]
  , unverified :: ![BehaviorKey]
  }
  deriving stock (Eq, Show)

instance ToJSON BehaviorConformanceReport where
  toJSON report = object
    [ "schema" .= ("keiro/behavior-conformance/1" :: Text)
    , "required" .= keyTexts (report.required)
    , "filled" .= keyTexts (report.filled)
    , "pending" .= keyTexts (report.pending)
    , "missing" .= keyTexts (report.missing)
    , "duplicate" .= keyTexts (report.duplicate)
    , "stale" .= keyTexts (report.stale)
    , "failed" .= report.failed
    , "verified" .= keyTexts (report.verified)
    , "unverified" .= keyTexts (report.unverified)
    ]

behaviorRequirements :: [BehaviorRequirement]
behaviorRequirements =
  [ -- SurgeIdle x NoteSurgeThreshold: live transition (spec line 43)
    BehaviorRequirement
      { key = BehaviorKey "behavior-v1-86bc21fdc4a8ca5d"
      , kind = LiveTransition
      , evidence = GeneratedAuthoritative
      , guardCoverage = GuardTotal
      , source = SurgeIdle
      , commandName = "NoteSurgeThreshold"
      , expectedEdge = (Just (K.EdgeRef SurgeIdle 0))
      , target = Just SurgeIdle
      , eventKinds = ["SurgeThresholdNoted"]
      , line = 43
      }
  , -- SurgeIdle x MarkSurgeTimerFired: live transition (spec line 44)
    BehaviorRequirement
      { key = BehaviorKey "behavior-v1-86bd3f785d9c7719"
      , kind = LiveTransition
      , evidence = GeneratedAuthoritative
      , guardCoverage = GuardTotal
      , source = SurgeIdle
      , commandName = "MarkSurgeTimerFired"
      , expectedEdge = (Just (K.EdgeRef SurgeIdle 1))
      , target = Just SurgeFired
      , eventKinds = ["SurgeTimerMarked"]
      , line = 44
      }
  , -- SurgeFired x NoteSurgeThreshold: required rejection (spec line 37)
    BehaviorRequirement
      { key = BehaviorKey "behavior-v1-d517bd7075620508"
      , kind = RequiredRejection
      , evidence = GeneratedAuthoritative
      , guardCoverage = GuardNotApplicable
      , source = SurgeFired
      , commandName = "NoteSurgeThreshold"
      , expectedEdge = Nothing
      , target = Nothing
      , eventKinds = []
      , line = 37
      }
  , -- SurgeFired x MarkSurgeTimerFired: required rejection (spec line 37)
    BehaviorRequirement
      { key = BehaviorKey "behavior-v1-fe2793e47f0b6989"
      , kind = RequiredRejection
      , evidence = GeneratedAuthoritative
      , guardCoverage = GuardNotApplicable
      , source = SurgeFired
      , commandName = "MarkSurgeTimerFired"
      , expectedEdge = Nothing
      , target = Nothing
      , eventKinds = []
      , line = 37
      }
  ]

behaviorCoverageReport :: [BehaviorWitness] -> BehaviorConformanceReport
behaviorCoverageReport witnesses =
  BehaviorConformanceReport
    { required = sortedKeys (Map.keys requiredByKey)
    , filled = sortedKeys [key | (key, [witness]) <- Map.toList witnessGroups, Map.member key requiredByKey, not (isPending witness)]
    , pending = sortedKeys [key | (key, rows) <- Map.toList witnessGroups, Map.member key requiredByKey, any isPending rows]
    , missing = sortedKeys [key | key <- Map.keys requiredByKey, Map.notMember key witnessGroups]
    , duplicate = sortedKeys [key | (key, rows) <- Map.toList witnessGroups, length rows > 1]
    , stale = sortedKeys [key | key <- Map.keys witnessGroups, Map.notMember key requiredByKey]
    , failed = sortOn (unBehaviorKey . (.key)) failures
    , verified = sortedKeys [requirement.key | (requirement, Right ()) <- executions, proofStrength requirement]
    , unverified = sortedKeys [requirement.key | (requirement, Right ()) <- executions, not (proofStrength requirement)]
    }
 where
  requiredByKey = Map.fromList [(requirement.key, 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 (report.pending)
    && null (report.missing)
    && null (report.duplicate)
    && null (report.stale)
    && null (report.failed)
    && (not failOnUnverified || null (report.unverified))

renderBehaviorConformanceText :: BehaviorConformanceReport -> Text
renderBehaviorConformanceText report = T.unlines
  [ "behavior conformance: Surge"
  , "schema: keiro/behavior-conformance/1"
  , countLine "required" (report.required)
  , countLine "filled" (report.filled)
  , countLine "pending" (report.pending)
  , countLine "missing" (report.missing)
  , countLine "duplicate" (report.duplicate)
  , countLine "stale" (report.stale)
  , "failed: " <> tshow (length (report.failed))
  , countLine "verified" (report.verified)
  , countLine "unverified" (report.unverified)
  ] <> T.unlines ["FAIL " <> unBehaviorKey (behaviorFailure.key) <> " " <> behaviorFailure.subject <> " [" <> behaviorFailure.code <> "] " <> behaviorFailure.detail | behaviorFailure <- report.failed]

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 -> [SurgeEvent] -> SurgeCommand -> LiveExpectation -> Either BehaviorFailure ()
runLive requirement history command expectation = do
  settled <- settleHistory requirement "history" history
  ensure requirement (K.replaySuccessState settled == requirement.source) "history-wrong-source" "history does not settle at the required source vertex"
  ensure requirement (commandKind command == requirement.commandName) "command-mismatch" "witness command constructor does not match the required state/command cell"
  case requirement.kind 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 -> (SurgeVertex, K.RegFile SurgeRegs) -> SurgeCommand -> LiveExpectation -> Either BehaviorFailure ()
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 surgeTransducer 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 -> (SurgeVertex, K.RegFile SurgeRegs) -> SurgeCommand -> LiveExpectation -> Either BehaviorFailure ()
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 surgeTransducer 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 surgeTransducer 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 == requirement.eventKinds) "event-envelope-mismatch" ("runtime event kinds differ from the declared ordered envelope; actual=" <> tshow (map eventKind actual) <> " expected=" <> tshow (requirement.eventKinds))
      decoded <- either (failure requirement "emitted-codec-decode") Right (decodeEvents actual)
      replayed <- case K.applyEventsDetailedEither surgeTransducer 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 :: BehaviorRequirement -> K.StepSuccess SurgeRegs SurgeVertex SurgeEvent -> 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) == requirement.expectedEdge) "edge-attribution" ("runtime selected a different guarded sibling; actual=" <> tshow (Just (K.stepSuccessEdge success)) <> " expected=" <> tshow (requirement.expectedEdge))
  ensure requirement (Just (K.stepSuccessState success) == requirement.target) "target-mismatch" ("runtime reached a different target vertex; actual=" <> tshow (Just (K.stepSuccessState success)) <> " expected=" <> tshow (requirement.target))

runReplay :: BehaviorRequirement -> [SurgeEvent] -> [SurgeEvent] -> Either BehaviorFailure ()
runReplay requirement prefix chunk = case requirement.kind of
  ReplayTransition -> do
    settled <- settleHistory requirement "history-prefix" prefix
    ensure requirement (K.replaySuccessState settled == requirement.source) "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 surgeTransducer (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) == requirement.target) "target-mismatch" ("replay chunk reached a different target vertex; actual=" <> tshow (Just (K.replaySuccessState replayed)) <> " expected=" <> tshow (requirement.target))
    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 SurgeVertex] -> Either BehaviorFailure ()
checkSingleAttribution requirement expectedMode eventCount trace = case trace of
  [attribution] -> do
    ensure requirement (Just (K.replayAttributionEdge attribution) == requirement.expectedEdge) "replay-edge-attribution" ("replay selected a different edge; actual=" <> tshow (Just (K.replayAttributionEdge attribution)) <> " expected=" <> tshow (requirement.expectedEdge))
    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 == requirement.source) "replay-source-attribution" ("replay attribution starts at the wrong source; actual=" <> tshow (K.replayAttributionSource attribution) <> " expected=" <> tshow (requirement.source))
    ensure requirement (Just (K.replayAttributionTarget attribution) == requirement.target) "replay-target-attribution" ("replay attribution ends at the wrong target; actual=" <> tshow (Just (K.replayAttributionTarget attribution)) <> " expected=" <> tshow (requirement.target))
    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 -> [SurgeEvent] -> Either BehaviorFailure (K.ReplaySuccess SurgeRegs SurgeVertex)
settleHistory requirement label history = do
  decoded <- either (failure requirement (label <> "-codec-decode")) Right (decodeEvents history)
  case K.applyEventsDetailedEither surgeTransducer (SurgeIdle, initialSurgeRegs) decoded of
    Left replayFailure -> failure requirement (label <> "-replay-failed") (tshow replayFailure)
    Right replaySuccess -> Right replaySuccess

decodeEvents :: [SurgeEvent] -> Either Text [SurgeEvent]
decodeEvents = traverse (\event -> parseSurgeEvent (Codec.eventType surgeCodec event) (encodeSurgeEvent event))

commandKind :: SurgeCommand -> Text
commandKind command = case command of
  NoteSurgeThreshold _ -> "NoteSurgeThreshold"
  MarkSurgeTimerFired _ -> "MarkSurgeTimerFired"

eventKind :: SurgeEvent -> Text
eventKind event = case Codec.eventType surgeCodec event of Codec.EventType tag -> tag

regsEqual :: K.RegFile SurgeRegs -> K.RegFile SurgeRegs -> Bool
regsEqual _ _ = True

proofStrength :: BehaviorRequirement -> Bool
proofStrength requirement =
  requirement.evidence == GeneratedAuthoritative
    && requirement.guardCoverage `elem` [GuardTotal, GuardNotApplicable]

behaviorWitnessKey :: BehaviorWitness -> BehaviorKey
behaviorWitnessKey witness = case witness of
  Pending key -> key
  LiveWitness { key = key } -> key
  ReplayWitness { key = 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
        (requirement.key)
        (tshow (requirement.source) <> " x " <> requirement.commandName <> ": " <> kindPhrase <> " (spec line " <> tshow (requirement.line) <> ")")
        code
        detail
    )
 where
  kindPhrase = case requirement.kind 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