Harness.hs

{-# LANGUAGE OverloadedLabels #-}
-- @generated by keiro-dsl 0.21.0.0 (language keiro-dsl 4) from aggregate Assignment; do not edit.
module Proof.WorkspaceProof.Assignment.Generated.Harness (harnessAssertions) where

import Proof.WorkspaceProof.Assignment.Generated.Domain
import Proof.WorkspaceProof.Assignment.Generated.Codec (encodeAssignmentEvent, parseAssignmentEvent, assignmentCodec)
import Proof.WorkspaceProof.Assignment.Generated.Transducer (assignmentTransducer)
import Keiki.Core (applyEventsEither, defaultValidationOptions, step, validateTransducer, (!))
import Keiro.Codec (eventType)
import Proof.WorkspaceProof.Assignment.BehaviorHoles (behaviorWitnesses)
import Proof.WorkspaceProof.Assignment.Generated.BehaviorContract (BehaviorConformanceReport (..), BehaviorKey (..), behaviorObligationReport)

-- | (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; pending Hole witnesses fail until filled and verified.
harnessAssertions :: [(String, Bool)]
harnessAssertions =
  [ ("validateTransducer is empty", null (validateTransducer defaultValidationOptions assignmentTransducer))
  -- clock-free: spec samples no wall clock (verified at scaffold time)
  , ("golden round-trip: PropertySet", roundTrips sampleEventPropertySet)
  , ("golden round-trip: PropertyCleared", roundTrips sampleEventPropertyCleared)
  , ("golden round-trip: Touched", roundTrips sampleEventTouched)
  , ("accepts SetProperty from AssignmentActive", acceptSetProperty)
  , ("accepts ClearProperty from AssignmentActive", acceptClearProperty)
  , ("accepts Touch from AssignmentActive", acceptTouch)
  ]
  ++ forwardReplaySetProperty
  ++ forwardReplayClearProperty
  ++ forwardReplayTouch

roundTrips :: AssignmentEvent -> Bool
roundTrips e = parseAssignmentEvent (eventType assignmentCodec e) (encodeAssignmentEvent e) == Right e

-- | One required obligation carrying exactly one non-pending witness.
holeWitnessFilled :: BehaviorKey -> BehaviorConformanceReport -> Bool
holeWitnessFilled key report = report.required == [key] && report.filled == [key]

sampleEventPropertySet :: AssignmentEvent
sampleEventPropertySet = PropertySet (PropertySetData "sample-key" "sample-value")

sampleEventPropertyCleared :: AssignmentEvent
sampleEventPropertyCleared = PropertyCleared (PropertyClearedData "sample-key")

sampleEventTouched :: AssignmentEvent
sampleEventTouched = Touched (TouchedData "sample-note")

acceptTouch :: Bool
acceptTouch =
  case step assignmentTransducer (AssignmentActive, initialAssignmentRegs) (Touch (TouchData "sample-note")) of
    Just (v, _, _) -> v == AssignmentActive
    Nothing -> False

-- Hole-owned initial edge: the consumer's history-backed live witness
-- proves acceptance through the generated behavior contract.
holeWitnessSetProperty :: BehaviorConformanceReport
holeWitnessSetProperty = behaviorObligationReport (BehaviorKey "behavior-v1-fbe5335a1e485829") behaviorWitnesses

acceptSetProperty :: Bool
acceptSetProperty = holeWitnessFilled (BehaviorKey "behavior-v1-fbe5335a1e485829") holeWitnessSetProperty && null holeWitnessSetProperty.failed

-- Hole-owned initial edge: the consumer's history-backed live witness
-- proves acceptance through the generated behavior contract.
holeWitnessClearProperty :: BehaviorConformanceReport
holeWitnessClearProperty = behaviorObligationReport (BehaviorKey "behavior-v1-075a56dd42e6bc95") behaviorWitnesses

acceptClearProperty :: Bool
acceptClearProperty = holeWitnessFilled (BehaviorKey "behavior-v1-075a56dd42e6bc95") holeWitnessClearProperty && null holeWitnessClearProperty.failed

-- forward/replay equality (plan 147): cross the persisted codec boundary,
-- replay the emitted chain, and compare the final vertex and every register.
forwardReplayTouch :: [(String, Bool)]
forwardReplayTouch =
  case step assignmentTransducer (AssignmentActive, initialAssignmentRegs) (Touch (TouchData "sample-note")) of
    Nothing -> [(prefix <> "forward step accepted", False)]
    Just (forwardVertex, forwardRegs, emitted) ->
      case mapM (\event -> parseAssignmentEvent (eventType assignmentCodec event) (encodeAssignmentEvent event)) emitted of
        Left _ -> [(prefix <> "emitted chain decodes", False)]
        Right decodedEvents ->
          case applyEventsEither assignmentTransducer (AssignmentActive, initialAssignmentRegs) decodedEvents of
            Left _ -> [(prefix <> "replay succeeds", False)]
            Right (replayVertex, replayRegs) ->
              [ (prefix <> "final vertex", replayVertex == forwardVertex)
              , (prefix <> "register values", (replayRegs ! #values) == (forwardRegs ! #values))
              ]
  where
    prefix = "forward/replay equality: Touch from AssignmentActive -- "

-- The behavior contract decodes emissions through the persisted codec,
-- replays them, and compares the final vertex and every register.
forwardReplaySetProperty :: [(String, Bool)]
forwardReplaySetProperty =
  [ (prefix <> "hole witness filled", holeWitnessFilled key holeWitnessSetProperty)
  , (prefix <> "hole witness verified", holeWitnessFilled key holeWitnessSetProperty && null holeWitnessSetProperty.failed)
  ]
  where
    key = BehaviorKey "behavior-v1-fbe5335a1e485829"
    prefix = "forward/replay equality: SetProperty from AssignmentActive -- "

-- The behavior contract decodes emissions through the persisted codec,
-- replays them, and compares the final vertex and every register.
forwardReplayClearProperty :: [(String, Bool)]
forwardReplayClearProperty =
  [ (prefix <> "hole witness filled", holeWitnessFilled key holeWitnessClearProperty)
  , (prefix <> "hole witness verified", holeWitnessFilled key holeWitnessClearProperty && null holeWitnessClearProperty.failed)
  ]
  where
    key = BehaviorKey "behavior-v1-075a56dd42e6bc95"
    prefix = "forward/replay equality: ClearProperty from AssignmentActive -- "