Harness.hs

{-# LANGUAGE OverloadedLabels #-}
-- @generated by keiro-dsl 0.17.0.0 (language keiro-dsl 6) from aggregate Project; do not edit.
module Generated.WorkspaceNominalProof.Project.Harness (harnessAssertions) where

import Generated.WorkspaceNominalProof.Project.Domain
import Generated.WorkspaceNominalProof.Project.Codec (encodeProjectEvent, parseProjectEvent, projectCodec, encodeProjectClaimMapped, decodeProjectClaimMapped)
import Generated.WorkspaceNominalProof.Project.Transducer (projectTransducer)
import Keiki.Core (applyEventsEither, defaultValidationOptions, step, validateTransducer, (!))
import Keiro.Codec (eventType)
import Generated.WorkspaceNominalProof.Nominals (ProjectId, parseProjectId, ProjectPhase (..))
import Data.Aeson qualified as Aeson
import Data.Aeson.Key qualified as AesonKey
import Data.Aeson.KeyMap qualified as AesonKeyMap
import Data.Either (isLeft)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Text qualified as T
import Keiro.Codec.Structural (FixtureCases (..))
import WorkspaceNominalProof.Bindings qualified as Bindings

-- | (label, passed). A driver runs these and exits non-zero on any False,
-- naming the failing assertion. Filling a hole wrongly turns a specific
-- entry False; the scaffold cannot.
harnessAssertions :: [(String, Bool)]
harnessAssertions =
  [ ("validateTransducer is empty", null (validateTransducer defaultValidationOptions projectTransducer))
  -- clock-free: spec samples no wall clock (verified at scaffold time)
  , ("golden round-trip: ProjectRegistered", roundTrips sampleEventProjectRegistered)
  , ("golden round-trip: ArchivalRecorded", roundTrips sampleEventArchivalRecorded)
  , ("accepts RegisterProject from ProjectEmpty", acceptRegisterProject)
  ]
  ++ mappedConformanceAssertions
  ++ forwardReplayRegisterProject

roundTrips :: ProjectEvent -> Bool
roundTrips e = parseProjectEvent (eventType projectCodec e) (encodeProjectEvent e) == Right e

sampleProjectId :: ProjectId
sampleProjectId =
  case parseProjectId "proj_01h455vb4pex5vsknk084sn02q" of
    Right parsed -> parsed
    Left problem -> error (show problem)

sampleEventProjectRegistered :: ProjectEvent
sampleEventProjectRegistered = ProjectRegistered (ProjectRegisteredData sampleProjectId Draft (snd (NonEmpty.head (fixtureCases Bindings.projectClaimFixtures))))

sampleEventArchivalRecorded :: ProjectEvent
sampleEventArchivalRecorded = ArchivalRecorded (ArchivalRecordedData sampleProjectId Draft)

acceptRegisterProject :: Bool
acceptRegisterProject =
  case step projectTransducer (ProjectEmpty, initialProjectRegs) (RegisterProject (RegisterProjectData sampleProjectId Draft (snd (NonEmpty.head (fixtureCases Bindings.projectClaimFixtures))))) of
    Just (v, _, _) -> v == ProjectLive
    Nothing -> False

-- forward/replay equality (plan 147): cross the persisted codec boundary,
-- replay the emitted chain, and compare the final vertex and every register.
forwardReplayRegisterProject :: [(String, Bool)]
forwardReplayRegisterProject =
  case step projectTransducer (ProjectEmpty, initialProjectRegs) (RegisterProject (RegisterProjectData sampleProjectId Draft (snd (NonEmpty.head (fixtureCases Bindings.projectClaimFixtures))))) of
    Nothing -> [(prefix <> "forward step accepted", False)]
    Just (forwardVertex, forwardRegs, emitted) ->
      case mapM (\event -> parseProjectEvent (eventType projectCodec event) (encodeProjectEvent event)) emitted of
        Left _ -> [(prefix <> "emitted chain decodes", False)]
        Right decodedEvents ->
          case applyEventsEither projectTransducer (ProjectEmpty, initialProjectRegs) decodedEvents of
            Left _ -> [(prefix <> "replay succeeds", False)]
            Right (replayVertex, replayRegs) ->
              [ (prefix <> "final vertex", replayVertex == forwardVertex)
              , (prefix <> "register projectId", (replayRegs ! #projectId) == (forwardRegs ! #projectId))
              , (prefix <> "register phase", (replayRegs ! #phase) == (forwardRegs ! #phase))
              ]
  where
    prefix = "forward/replay equality: RegisterProject from ProjectEmpty -- "

mappedConformanceAssertions :: [(String, Bool)]
mappedConformanceAssertions =
  concat
    [ projectRegisteredClaimAssertions
    , structuralWirePolicyAssertions
    ]

projectRegisteredClaimAssertions :: [(String, Bool)]
projectRegisteredClaimAssertions =
  [ ("mapped codec round-trip: ProjectRegistered/claim/" <> T.unpack label, roundTrips (ProjectRegistered (ProjectRegisteredData sampleProjectId Draft mappedValue)))
  | (label, mappedValue) <- NonEmpty.toList (fixtureCases Bindings.projectClaimFixtures)
  ]

structuralWirePolicyAssertions :: [(String, Bool)]
structuralWirePolicyAssertions =
  [ ("wire policy unknown fields: workspace-nominal-proof.ProjectClaim.v1", all (\(_, value) -> isLeft (decodeProjectClaimMapped (insertObjectField "__keiro_unknown" (Aeson.Bool True) (encodeProjectClaimMapped value)))) (NonEmpty.toList (fixtureCases Bindings.projectClaimFixtures)))
  ]

insertObjectField :: T.Text -> Aeson.Value -> Aeson.Value -> Aeson.Value
insertObjectField key inserted (Aeson.Object objectValue) = Aeson.Object (AesonKeyMap.insert (AesonKey.fromText key) inserted objectValue)
insertObjectField _ _ value = value