Harness.hs

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

import Generated.WorkspaceNominalProof.Project.Domain
import Generated.WorkspaceNominalProof.Project.Codec (encodeProjectEvent, parseProjectEvent, projectCodec)
import Generated.WorkspaceNominalProof.Project.Transducer (projectTransducer)
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 projectTransducer))
  , ("clock-free: spec samples no wall clock", True)
  , ("golden round-trip: ProjectRegistered", roundTrips sampleEventProjectRegistered)
  , ("golden round-trip: ArchivalRecorded", roundTrips sampleEventArchivalRecorded)
  , ("accepts RegisterProject from ProjectEmpty", acceptRegisterProject)
  ]
  ++ forwardReplayRegisterProject

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

sampleEventProjectRegistered :: ProjectEvent
sampleEventProjectRegistered = (ProjectRegistered (ProjectRegisteredData (ProjectId "sample") Draft))

sampleEventArchivalRecorded :: ProjectEvent
sampleEventArchivalRecorded = (ArchivalRecorded (ArchivalRecordedData (ProjectId "sample") Draft))

acceptRegisterProject :: Bool
acceptRegisterProject =
  case step projectTransducer (ProjectEmpty, initialProjectRegs) ((RegisterProject (RegisterProjectData (ProjectId "") Draft))) 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 (ProjectId "") Draft))) 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 -- "