BehaviorContract.hs

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

import Generated.ReplayDivergence.Note.Codec (encodeNoteEvent, parseNoteEvent, noteCodec)
import Generated.ReplayDivergence.Note.Domain
import Generated.ReplayDivergence.Note.Transducer (noteTransducer)
import Generated.ReplayDivergence.BehaviorSourceMap qualified as BehaviorSourceMap
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)

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 :: !NoteVertex
  , commandName :: !Text
  , expectedEdge :: !(Maybe (K.EdgeRef NoteVertex))
  , target :: !(Maybe NoteVertex)
  , eventKinds :: ![Text]
  }
  deriving stock (Eq, Show)

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

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

data BehaviorWitness
  = Pending BehaviorKey
  | LiveWitness
      { key :: BehaviorKey
      , history :: [NoteEvent]
      , command :: NoteCommand
      , expected :: LiveExpectation
      }
  | ReplayWitness
      { key :: BehaviorKey
      , historyPrefix :: [NoteEvent]
      , observedChunk :: [NoteEvent]
      }
  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 =
  [ -- NoteEmpty x WriteNote: live transition
    BehaviorRequirement
      { key = BehaviorKey "behavior-v1-248e9c1b1eb3e5bc"
      , kind = LiveTransition
      , evidence = GeneratedAuthoritative
      , guardCoverage = GuardTotal
      , source = NoteEmpty
      , commandName = "WriteNote"
      , expectedEdge = (Just (K.EdgeRef NoteEmpty 0))
      , target = Just NoteRecorded
      , eventKinds = ["NoteWritten"]
      }
  , -- NoteRecorded x WriteNote: required rejection
    BehaviorRequirement
      { key = BehaviorKey "behavior-v1-7c36eda198514110"
      , kind = RequiredRejection
      , evidence = GeneratedAuthoritative
      , guardCoverage = GuardNotApplicable
      , source = NoteRecorded
      , commandName = "WriteNote"
      , expectedEdge = Nothing
      , target = Nothing
      , eventKinds = []
      }
  ]

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: Note"
  , "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 -> [NoteEvent] -> NoteCommand -> 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 -> (NoteVertex, K.RegFile NoteRegs) -> NoteCommand -> 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 noteTransducer 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 -> (NoteVertex, K.RegFile NoteRegs) -> NoteCommand -> 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 noteTransducer 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 noteTransducer 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 noteTransducer 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 NoteRegs NoteVertex NoteEvent -> 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 -> [NoteEvent] -> [NoteEvent] -> 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 noteTransducer (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 NoteVertex] -> 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 -> [NoteEvent] -> Either BehaviorFailure (K.ReplaySuccess NoteRegs NoteVertex)
settleHistory requirement label history = do
  decoded <- either (failure requirement (label <> "-codec-decode")) Right (decodeEvents history)
  case K.applyEventsDetailedEither noteTransducer (NoteEmpty, initialNoteRegs) decoded of
    Left replayFailure -> failure requirement (label <> "-replay-failed") (tshow replayFailure)
    Right replaySuccess -> Right replaySuccess

decodeEvents :: [NoteEvent] -> Either Text [NoteEvent]
decodeEvents = traverse (\event -> parseNoteEvent (Codec.eventType noteCodec event) (encodeNoteEvent event))

commandKind :: NoteCommand -> Text
commandKind command = case command of
  WriteNote _ -> "WriteNote"

eventKind :: NoteEvent -> Text
eventKind event = case Codec.eventType noteCodec event of Codec.EventType tag -> tag

regsEqual :: K.RegFile NoteRegs -> K.RegFile NoteRegs -> Bool
regsEqual left right = (left K.! #note) == (right K.! #note)

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 <> " (" <> BehaviorSourceMap.renderBehaviorSourceLocation (unBehaviorKey requirement.key) <> ")")
        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