Harness.hs

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

import Generated.WorkspaceNominalProof.ProjectArtifact.Domain
import Generated.WorkspaceNominalProof.ProjectArtifact.Codec (encodeProjectArtifactEvent, parseProjectArtifactEvent, projectArtifactCodec, encodeArtifactClaimMapped, decodeArtifactClaimMapped)
import Generated.WorkspaceNominalProof.ProjectArtifact.Transducer (projectArtifactTransducer)
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 projectArtifactTransducer))
  -- clock-free: spec samples no wall clock (verified at scaffold time)
  , ("golden round-trip: ArtifactRecorded", roundTrips sampleEventArtifactRecorded)
  , ("accepts RecordArtifact from ProjectArtifactEmpty", acceptRecordArtifact)
  ]
  ++ mappedConformanceAssertions
  ++ forwardReplayRecordArtifact

roundTrips :: ProjectArtifactEvent -> Bool
roundTrips e = parseProjectArtifactEvent (eventType projectArtifactCodec e) (encodeProjectArtifactEvent e) == Right e

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

sampleEventArtifactRecorded :: ProjectArtifactEvent
sampleEventArtifactRecorded = ArtifactRecorded (ArtifactRecordedData sampleProjectId Draft (snd (NonEmpty.head (fixtureCases Bindings.artifactClaimFixtures))))

acceptRecordArtifact :: Bool
acceptRecordArtifact =
  case step projectArtifactTransducer (ProjectArtifactEmpty, initialProjectArtifactRegs) (RecordArtifact (RecordArtifactData sampleProjectId Draft (snd (NonEmpty.head (fixtureCases Bindings.artifactClaimFixtures))))) of
    Just (v, _, _) -> v == ProjectArtifactRecorded
    Nothing -> False

-- forward/replay equality (plan 147): cross the persisted codec boundary,
-- replay the emitted chain, and compare the final vertex and every register.
forwardReplayRecordArtifact :: [(String, Bool)]
forwardReplayRecordArtifact =
  case step projectArtifactTransducer (ProjectArtifactEmpty, initialProjectArtifactRegs) (RecordArtifact (RecordArtifactData sampleProjectId Draft (snd (NonEmpty.head (fixtureCases Bindings.artifactClaimFixtures))))) of
    Nothing -> [(prefix <> "forward step accepted", False)]
    Just (forwardVertex, forwardRegs, emitted) ->
      case mapM (\event -> parseProjectArtifactEvent (eventType projectArtifactCodec event) (encodeProjectArtifactEvent event)) emitted of
        Left _ -> [(prefix <> "emitted chain decodes", False)]
        Right decodedEvents ->
          case applyEventsEither projectArtifactTransducer (ProjectArtifactEmpty, initialProjectArtifactRegs) 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: RecordArtifact from ProjectArtifactEmpty -- "

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

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

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

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