Harness.hs

-- @generated by keiro-dsl 0.15.0.0 (language keiro-dsl 4) from aggregate Alpha; do not edit.
module Proof.WorkspaceProof.Alpha.Generated.Harness (harnessAssertions) where

import Proof.WorkspaceProof.Alpha.Generated.Domain
import Proof.WorkspaceProof.Alpha.Generated.Codec (encodeAlphaEvent, parseAlphaEvent, alphaCodec)
import Proof.WorkspaceProof.Alpha.Generated.Transducer (alphaTransducer)
import Keiki.Core (applyEventsEither, defaultValidationOptions, step, validateTransducer)
import Keiro.Codec (eventType)
import Proof.WorkspaceProof.Generated.Nominals (ProofId, parseProofId)

-- | (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 alphaTransducer))
  -- clock-free: spec samples no wall clock (verified at scaffold time)
  , ("golden round-trip: AlphaPinged", roundTrips sampleEventAlphaPinged)
  , ("golden round-trip: LegacyAlphaPinged", roundTrips sampleEventLegacyAlphaPinged)
  , ("accepts PingAlpha from AlphaActive", acceptPingAlpha)
  ]
  ++ forwardReplayPingAlpha

roundTrips :: AlphaEvent -> Bool
roundTrips e = parseAlphaEvent (eventType alphaCodec e) (encodeAlphaEvent e) == Right e

sampleProofId :: ProofId
sampleProofId =
  case parseProofId "proof_01h455vb4pex5vsknk084sn02q" of
    Right parsed -> parsed
    Left problem -> error (show problem)

sampleEventAlphaPinged :: AlphaEvent
sampleEventAlphaPinged = AlphaPinged (AlphaPingedData sampleProofId False)

sampleEventLegacyAlphaPinged :: AlphaEvent
sampleEventLegacyAlphaPinged = LegacyAlphaPinged (LegacyAlphaPingedData sampleProofId)

acceptPingAlpha :: Bool
acceptPingAlpha =
  case step alphaTransducer (AlphaActive, initialAlphaRegs) (PingAlpha (PingAlphaData sampleProofId False)) of
    Just (v, _, _) -> v == AlphaActive
    Nothing -> False

-- forward/replay equality (plan 147): cross the persisted codec boundary,
-- replay the emitted chain, and compare the final vertex and every register.
forwardReplayPingAlpha :: [(String, Bool)]
forwardReplayPingAlpha =
  case step alphaTransducer (AlphaActive, initialAlphaRegs) (PingAlpha (PingAlphaData sampleProofId False)) of
    Nothing -> [(prefix <> "forward step accepted", False)]
    Just (forwardVertex, _forwardRegs, emitted) ->
      case mapM (\event -> parseAlphaEvent (eventType alphaCodec event) (encodeAlphaEvent event)) emitted of
        Left _ -> [(prefix <> "emitted chain decodes", False)]
        Right decodedEvents ->
          case applyEventsEither alphaTransducer (AlphaActive, initialAlphaRegs) decodedEvents of
            Left _ -> [(prefix <> "replay succeeds", False)]
            Right (replayVertex, _replayRegs) ->
              [ (prefix <> "final vertex", replayVertex == forwardVertex)
              ]
  where
    prefix = "forward/replay equality: PingAlpha from AlphaActive -- "