BehaviorContract.hs

{-# LANGUAGE OverloadedLabels #-}
-- @generated by keiro-dsl 0.11.0.0 (language keiro-dsl 4) from aggregate NominalLedger; do not edit.
module Generated.NominalScalars.NominalLedger.BehaviorContract
  ( BehaviorKey (..)
  , ObligationKind (..)
  , EvidenceLevel (..)
  , GuardCoverage (..)
  , BehaviorRequirement (..)
  , RejectionClass (..)
  , LiveExpectation (..)
  , BehaviorWitness (..)
  , BehaviorFailure (..)
  , BehaviorConformanceReport (..)
  , behaviorRequirements
  , behaviorCoverageReport
  , behaviorConformancePassed
  , behaviorConformancePassedWith
  , renderBehaviorConformanceText
  ) where

import Generated.NominalScalars.NominalLedger.Codec (encodeNominalLedgerEvent, parseNominalLedgerEvent, nominalLedgerCodec)
import Generated.NominalScalars.NominalLedger.Domain
import Generated.NominalScalars.NominalLedger.Transducer (nominalLedgerTransducer)
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 :: !NominalLedgerVertex
  , requirementCommandName :: !Text
  , requirementExpectedEdge :: !(Maybe (K.EdgeRef NominalLedgerVertex))
  , requirementTarget :: !(Maybe NominalLedgerVertex)
  , requirementEventKinds :: ![Text]
  , requirementLine :: !Int
  }
  deriving stock (Eq, Show)

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

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

data BehaviorWitness
  = Pending BehaviorKey
  | LiveWitness
      { witnessKey :: BehaviorKey
      , witnessHistory :: [NominalLedgerEvent]
      , witnessCommand :: NominalLedgerCommand
      , witnessExpected :: LiveExpectation
      }
  | ReplayWitness
      { witnessKey :: BehaviorKey
      , witnessHistoryPrefix :: [NominalLedgerEvent]
      , witnessObservedChunk :: [NominalLedgerEvent]
      }
  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 =
  [ -- NominalLedgerEmpty x RecordNominals: live transition (spec line 84)
    BehaviorRequirement
      { requirementKey = BehaviorKey "behavior-v1-274eaf83d346048a"
      , requirementKind = LiveTransition
      , requirementEvidence = GeneratedAuthoritative
      , requirementGuardCoverage = GuardUnknown
      , requirementSource = NominalLedgerEmpty
      , requirementCommandName = "RecordNominals"
      , requirementExpectedEdge = (Just (K.EdgeRef NominalLedgerEmpty 0))
      , requirementTarget = Just NominalLedgerRecorded
      , requirementEventKinds = ["NominalsRecorded"]
      , requirementLine = 84
      }
  , -- NominalLedgerRecorded x RecordNominals: required rejection (spec line 76)
    BehaviorRequirement
      { requirementKey = BehaviorKey "behavior-v1-971c0c80ffdfe018"
      , requirementKind = RequiredRejection
      , requirementEvidence = GeneratedAuthoritative
      , requirementGuardCoverage = GuardNotApplicable
      , requirementSource = NominalLedgerRecorded
      , requirementCommandName = "RecordNominals"
      , requirementExpectedEdge = Nothing
      , requirementTarget = Nothing
      , requirementEventKinds = []
      , requirementLine = 76
      }
  ]

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: NominalLedger"
  , "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 -> [NominalLedgerEvent] -> NominalLedgerCommand -> 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 -> (NominalLedgerVertex, K.RegFile NominalLedgerRegs) -> NominalLedgerCommand -> 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 nominalLedgerTransducer 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 -> (NominalLedgerVertex, K.RegFile NominalLedgerRegs) -> NominalLedgerCommand -> 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 nominalLedgerTransducer 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 nominalLedgerTransducer 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 nominalLedgerTransducer 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 NominalLedgerRegs NominalLedgerVertex NominalLedgerEvent -> 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 -> [NominalLedgerEvent] -> [NominalLedgerEvent] -> 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 nominalLedgerTransducer (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 NominalLedgerVertex] -> 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 -> [NominalLedgerEvent] -> Either BehaviorFailure (K.ReplaySuccess NominalLedgerRegs NominalLedgerVertex)
settleHistory requirement label history = do
  decoded <- either (failure requirement (label <> "-codec-decode")) Right (decodeEvents history)
  case K.applyEventsDetailedEither nominalLedgerTransducer (NominalLedgerEmpty, initialNominalLedgerRegs) decoded of
    Left replayFailure -> failure requirement (label <> "-replay-failed") (tshow replayFailure)
    Right replaySuccess -> Right replaySuccess

decodeEvents :: [NominalLedgerEvent] -> Either Text [NominalLedgerEvent]
decodeEvents = traverse (\event -> parseNominalLedgerEvent (Codec.eventType nominalLedgerCodec event) (encodeNominalLedgerEvent event))

commandKind :: NominalLedgerCommand -> Text
commandKind command = case command of
  RecordNominals _ -> "RecordNominals"

eventKind :: NominalLedgerEvent -> Text
eventKind event = case Codec.eventType nominalLedgerCodec event of Codec.EventType tag -> tag

regsEqual :: K.RegFile NominalLedgerRegs -> K.RegFile NominalLedgerRegs -> Bool
regsEqual left right = (left K.! #orderId) == (right K.! #orderId) && (left K.! #status) == (right K.! #status) && (left K.! #accountNumber) == (right K.! #accountNumber) && (left K.! #riskScore) == (right K.! #riskScore) && (left K.! #sequenceNumber) == (right K.! #sequenceNumber) && (left K.! #featureFlag) == (right K.! #featureFlag) && (left K.! #observedAt) == (right K.! #observedAt)

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 <> " (spec line " <> tshow (requirementLine 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