Harness.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedLabels #-}
-- @generated by keiro-dsl; do not edit. Regenerated from the .keiro spec.
module Generated.WorkspaceNominalProof.ProjectArtifact.Harness (harnessAssertions) where

import Generated.WorkspaceNominalProof.ProjectArtifact.Domain
import Generated.WorkspaceNominalProof.ProjectArtifact.Codec (encodeProjectArtifactEvent, parseProjectArtifactEvent, projectArtifactCodec)
import Generated.WorkspaceNominalProof.ProjectArtifact.Transducer (projectArtifactTransducer)
import Keiki.Core (applyEventsEither, defaultValidationOptions, step, validateTransducer, (!))
import Keiro.Codec (eventType)
import Generated.WorkspaceNominalProof.Nominals (ProjectId (..), ProjectPhase (..))

{- | (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", True)
  , ("golden round-trip: ArtifactRecorded", roundTrips sampleEventArtifactRecorded)
  , ("accepts RecordArtifact from ProjectArtifactEmpty", acceptRecordArtifact)
  ]
  ++ forwardReplayRecordArtifact

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

sampleEventArtifactRecorded :: ProjectArtifactEvent
sampleEventArtifactRecorded = (ArtifactRecorded (ArtifactRecordedData (ProjectId "sample") Draft))

acceptRecordArtifact :: Bool
acceptRecordArtifact =
  case step projectArtifactTransducer (ProjectArtifactEmpty, initialProjectArtifactRegs) ((RecordArtifact (RecordArtifactData (ProjectId "") Draft))) 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 (ProjectId "") Draft))) 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 -- "