Harness.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedLabels #-}

-- @generated by keiro-dsl; do not edit. Regenerated from the .keiro spec.
module Generated.ReplayDivergence.Note.Harness (harnessAssertions) where

import Generated.ReplayDivergence.Note.Codec (encodeNoteEvent, noteCodec, parseNoteEvent)
import Generated.ReplayDivergence.Note.Domain
import Keiki.Core (applyEventsEither, defaultValidationOptions, step, validateTransducer, (!))
import Keiro.Codec (eventType)
import ReplayDivergence.Note.Holes (noteTransducer)

{- | (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 noteTransducer))
    , ("clock-free: spec samples no wall clock", True)
    , ("golden round-trip: NoteWritten", roundTrips sampleEventNoteWritten)
    , ("accepts WriteNote from NoteEmpty", acceptWriteNote)
    ]
        ++ forwardReplayWriteNote

roundTrips :: NoteEvent -> Bool
roundTrips e = parseNoteEvent (eventType noteCodec e) (encodeNoteEvent e) == Right e

sampleEventNoteWritten :: NoteEvent
sampleEventNoteWritten = (NoteWritten (NoteWrittenData "sample-noteText" "sample-echo"))

acceptWriteNote :: Bool
acceptWriteNote =
    case step noteTransducer (NoteEmpty, initialNoteRegs) ((WriteNote (WriteNoteData "sample-noteText" "sample-echo"))) of
        Just (v, _, _) -> v == NoteRecorded
        Nothing -> False

-- forward/replay equality (plan 147): cross the persisted codec boundary,
-- replay the emitted chain, and compare the final vertex and every register.
forwardReplayWriteNote :: [(String, Bool)]
forwardReplayWriteNote =
    case step noteTransducer (NoteEmpty, initialNoteRegs) ((WriteNote (WriteNoteData "sample-noteText" "sample-echo"))) of
        Nothing -> [(prefix <> "forward step accepted", False)]
        Just (forwardVertex, forwardRegs, emitted) ->
            case mapM (\event -> parseNoteEvent (eventType noteCodec event) (encodeNoteEvent event)) emitted of
                Left _ -> [(prefix <> "emitted chain decodes", False)]
                Right decodedEvents ->
                    case applyEventsEither noteTransducer (NoteEmpty, initialNoteRegs) decodedEvents of
                        Left _ -> [(prefix <> "replay succeeds", False)]
                        Right (replayVertex, replayRegs) ->
                            [ (prefix <> "final vertex", replayVertex == forwardVertex)
                            , (prefix <> "register note", (replayRegs ! #note) == (forwardRegs ! #note))
                            ]
  where
    prefix = "forward/replay equality: WriteNote from NoteEmpty -- "