@hackage / keiki

Pure core for symbolic-register transducer event sourcing.

Changelog

Changelog

All notable changes to this package are documented in this file. The format follows Keep a Changelog, and this project adheres to the Haskell PVP.

[Unreleased]

[0.3.0.0] — 2026-07-23

Added
  • Keiki.Core.EdgeMode (Live / ReplayOnly): a first-class edge mode for guard evolution. A ReplayOnly edge is never taken by forward stepping (delta / step / stepEither filter on Live) and participates in inversion only when no Live edge attributes the observed event — inversion (applyEvent, applyEventStreamingEither) is now two-phase, with ambiguity judged within the phase that produced candidates. Use it to retain the removed region of a tightened guard (old-guard ∧ ¬new-guard) as a replay-only twin so events stored under the old rule keep an inverting edge. The Semigroup/Monoid instances (Live identity, ReplayOnly absorbing) define the mode of composed edges.
  • Keiki.Builder.replayOnly marks the edge under construction ReplayOnly.
Changed
  • Breaking: Edge gained the field mode :: EdgeMode. Existing construction sites should set mode = Live to keep their exact previous semantics. Composition (compose, alternative), the profunctor rewrites, and withSymPred propagate the mode (a composite edge is Live only when every component is).
  • Static checks are mode-aware: the determinism family (checkTransitionDeterminism, checkTransitionDeterminismPure, determinismWarnings, isSingleValuedSym) considers only Live/Live pairs (only live edges compete in forward dispatch), and inversionAmbiguityWarnings flags only same-mode pairs (cross-mode pairs are resolved deterministically by the live-first phase order). All other checks — hidden-input, head-recoverability, guard-implies-input-read, state-changing epsilon, opaque-guard, and both dead-edge analyses (structural reachability still traverses replay-only targets: a vertex reachable only through a replay-only edge stays live for replay continuation) — apply to replay-only edges unchanged.
Migration
  • Deleting a deployed replay-only twin re-creates exactly the break it fixed (stored events in the removed region lose their inverting edge). Delete a twin only once every stream containing the region's events is terminal or truncated.

[0.2.0.0] — 2026-07-13

Added

  • Keiki.Symbolic.satResultIsProvablyUnsat exposes the conservative solver verdict used by symbolic emptiness checks: only a definite Unsatisfiable result proves a predicate empty.

  • Keiki.Composition.checkComposeAlignment and composeChecked report constructor-name drift, unmatched expectations, field-arity mismatches, and mapped/poisoned boundary names with exact source edge locations.

  • PLeftArm and PRightArm give alternative concrete and symbolic Either-arm exclusion even when an underlying edge guard is PTop.

  • Keiki.Builder.buildTransducerEither returns all eagerly located builder defects as structured BuilderError values. BuilderDefect and renderBuilderErrors expose the same validation and historical message format without exception plumbing.

  • DistinctNames provides the canonical compile-time duplicate register-slot check, and slotNamesOf is now exported from Keiki.Core for structural constructor validation.

  • Structured replay diagnostics are available through applyEventStreamingEither, replayEvents, applyEventsEither, and reconstituteEither. ReplayStepFailure, ReplayFailureReason, and ReplayFailure identify the failing event index, wrapper state, and exact reason, including ambiguous inversion, queue mismatch, and truncated multi-event chains. The existing Maybe functions remain compatibility wrappers over this primary surface.

Changed

  • Aggregate-constructor TH now rejects positional payload types immediately with a record-syntax diagnostic. The *All and *With enumeration splices warn when they skip unsupported GADT or explicitly quantified constructors.

  • Breaking: built-in CanonicalTypeName instances now use pinned, module-independent names such as Int, Text, and Maybe(Int). Every non-empty register-file shape hash therefore changes once in this release. Snapshot stores keyed by the old hash treat existing snapshots as cache misses and replay the event log in full; keiro follows this benign fallback path.

  • Maybe, list, Either, and tuple canonical-name instances now recurse through CanonicalTypeName instead of Typeable, so application overrides compose inside containers. A custom type used there may need deriving anyclass (CanonicalTypeName); missing evidence is a compile-time migration rather than silent hash drift.

  • Symbolic emptiness checks no longer mistake solver uncertainty for proof of unsatisfiability. symIsBot, symSatExt, isSingleValuedSym, withSymPred, checkTransitionDeterminismSym, and checkDeadEdgesSym keep their existing names and signatures; Unknown, ProofError, and other non-definitive solver results now fail conservatively instead of blessing a guard pair as disjoint or an edge as dead. These pure-looking APIs still run z3 through unsafePerformIO and throw if the solver is unavailable.

  • checkDeadEdgesSym no longer carries a redundant Show s constraint. Relaxing a constraint is source-compatible, so existing call sites need no change.

  • Symbolic encodings for Word8, Word16, Word32, Word64, Int32, and Int64 now use exact fixed-width SBV values, preserving modular wraparound. UTCTime now round-trips at its native picosecond resolution instead of truncating to whole seconds. Platform-sized Int remains modeled as an unbounded Integer, so analyses whose truth depends on Int overflow should use an explicitly sized type.

  • The pure determinism pass used by validateTransducer now proves overlap through supported conjunction spines, including constructor consistency, exact integral intervals, and concrete literal witnesses. Unsupported disjunctions, negations, arithmetic, opaque terms, and variable-to-variable comparisons remain unknown and produce no pure warning; use the z3-backed checks as the exact gate. Existing consumers, including keiro, remain source-compatible, but may see new NondeterministicPair warnings. Such warnings are true positives and should be repaired or explicitly acknowledged rather than suppressed by pinning the old behavior.

  • SomeSymTransducer now carries input/output poison provenance while retaining its one-argument compatibility pattern. Variance rewrites stamp constructor names with #lmapped/#rmapped; categorical composition across a poisoned boundary raises PoisonedCompositionError instead of silently bypassing a map or producing a dead pipeline.

  • feedback1 is documented as its actual two-copy cascade contract, not shared-state aggregate feedback; no feedback1Checked API is exposed.

  • runUpdate now gives UCombine snapshot (parallel-assignment) semantics: every right-hand side reads the edge-entry register file and writes apply left-to-right. Sequential compose now symbolically threads t2 register writes across multi-event chains, so stateful composition agrees with stepping t1 and then t2 event-by-event. Constructor-mismatched comparison leaves become PBot, while mismatches in other positions use walker-safe opaque poison terms. This is a pre-release behavior change; the surveyed current keiro consumer has no update depending on the former threaded-within-one-edge behavior and does not call composition operators.

  • validateTransducer defaultValidationOptions now enforces four additional replay-safety checks: head-event recoverability, cross-edge inversion ambiguity, constructor guards before input-field reads, and state-changing ε-edges. The corresponding warning constructors are HeadUnrecoverable, InversionAmbiguity, UnguardedInputRead, and StateChangingEpsilon; the new default-on option fields are checkHeadRecoverability, checkInversionAmbiguity, checkGuardImpliesInputRead, and checkStateChangingEpsilon. Code that exhaustively matches TransducerValidationWarning must add these four cases, and code that constructs ValidationOptions should record-update defaultValidationOptions so future checks remain enabled.

  • checkHiddenInputs now requires the first event of a multi-event edge to recover every consumed command field. Coverage spread across the union of the head and tail is no longer accepted because streaming replay inverts only the head; tail-only fields produce HeadUnrecoverable through validateTransducer and an equivalent legacy string warning through checkHiddenInputs.

  • The canonical User Registration pre-confirmation deletion now emits AccountDeleted instead of changing vertex and registers silently, so its forward result is recoverable from its persisted log.

  • Keiki.Builder now requires every onCmd/onEpsilon edge body to declare its output intent explicitly. A body that reaches goto without calling emit/emitWith or noEmit is an eager construction error instead of silently becoming an ε-edge; deliberately silent edges keep working by calling noEmit.

  • Keiki.Builder now validates every declared edge when the returned transducer is evaluated to weak head normal form. Missing/multiple goto calls and mismatched explicit emitWith constructors no longer remain latent until an affected edgesOut branch is demanded; duplicate from blocks merge in declaration order with stable per-vertex edge indices.

  • The builder pins the enclosing onCmd input schema in EdgeBuilder. Passing another command's term-fields record to emit, or calling emit inside onEpsilon, is now a compile-time error. emitWith remains the explicit form for onEpsilon and must agree with the enclosing constructor inside onCmd.

  • buildTransducer and buildTransducerEither require DistinctNames (Names rs), rejecting register files with duplicated slot names instead of silently resolving the first occurrence. Vertex grouping now requires Eq v; the unused Bounded v and Enum v constraints were removed.

  • Current keiro authoring remains source-compatible: the standard B.emit wireCtorX XTermFields {..} shape and both build call forms are unchanged for valid aggregates.

  • Keiki.Profunctor no longer fabricates method-carrying WeakenR and KnownSlotNames dictionaries with unsafeCoerce. Nested stateful Category composition previously misindexed register reads and writes and hid slot names from CategoryOverlapError. SomeSymTransducer now carries the exported KnownSlots/SlotListWitness evidence from Keiki.Composition, and composite evidence is derived by structural induction. The smart constructor's structural constraints are now expressed as KnownSlots rs.

  • Keiki.Acceptor.outputAcceptor now carries (InFlight s co, RegFile rs) and steps with applyEventStreaming, so its acceptance result agrees with reconstitute for multi-event and truncated logs as well as letter-only logs.

Removed
  • Keiki.Builder no longer uses unsafeCoerce to reinterpret the input schema recovered by emit; the schema relationship is represented in its types.
  • The lossy pre-release Decider facade has been removed. Use stepEither for forward decisions and the structured Keiki.Core replay functions for hydration; there is no letter-only replay facade that silently retains the input state after a failure.

[0.1.0.0] — 2026-06-07

Initial Hackage release. Public surface stabilised around the symbolic-register transducer formalism described in docs/research/synthesis-c-foundation-b-presentation-with-worked-examples.md.

Added
  • Keiki.Core — the foundational RegFile rs register file, the SymTransducer GADT, and the slot / predicate / command / event / output algebra. Edges carry a list-shaped output (output :: [OutTerm rs ci co]) so one transition can emit zero, one, or N events in declaration order — a Generalized Sequential Machine, not a letter FST. The InFlight s co wrapper exposes the streaming-replay state for event-by-event replay through length-N edges; applyEvent (letter-only) and applyEventStreaming (InFlight-aware) cover the two regimes, while applyEvents does atomic chunk replay over command boundaries.
  • Keiki.Acceptor — input- and output-side acceptor projections.
  • Keiki.Builder — the monadic edge-authoring DSL.
  • Keiki.Composition — sequential, alternative, and single-step feedback combinators on SymTransducers.
  • Keiki.Generics — RegFieldsOf, GRecord, mkInCtor / mkInCtorVia, mkWireCtor / mkWireCtorVia, plus EmptyRegFile.
  • Keiki.Generics.TH — deriveAggregateCtors, deriveWireCtors, deriveView for record-payload aggregates, plus zero-enumeration *All splices that retire the hand-typed (constructorName, shortName) spec list in the common case where the short name equals the constructor name:
    • deriveAggregateCtorsAll ''Cmd ''Regs — enumerates every command constructor and emits inCtor<Ctor> / inp<Ctor> / is<Ctor> (singletons omit inp<Ctor>), defaulting each short-name suffix to the constructor name.
    • deriveWireCtorsAll ''Event — the event-side dual, emitting wire<Ctor> plus, for record-payload events, the <Ctor>TermFields record and its ToOutFields instance.
    • deriveAggregate ''Cmd ''Regs ''Event — fuses both *All variants into one splice covering an aggregate's command and event constructors. The enumerated deriveAggregateCtors / deriveWireCtors remain for abbreviated short names that differ from the constructor name.
  • Keiki.NoThunks — strict-evaluation discipline assertions for the register file and per-vertex state.
  • Keiki.Profunctor — Profunctor / Category / Strong / Choice instances on the existential SymTransducer wrapper.
  • Keiki.Render.Mermaid — Mermaid renderers for single and composite SymTransducer diagrams.
  • Keiki.Shape — GHC-upgrade-safe shape hash for snapshot discrimination. class CanonicalTypeName a, class KnownRegFileShape (rs :: [Slot]), regFileShapeHash, regFileShapeCanonical, renderStableTypeRep, sha256Hex. Reusable by any codec; the optional JSON codec lives in the sibling package keiki-codec-json.
  • Keiki.Symbolic — SBV-backed sat / isBot / isSingleValuedSym analyses for symbolic CI gating.
Out of scope (intentional)
  • No built-in serialization. JSON / CBOR / Protobuf codecs are runtime concerns and live in sibling packages — currently keiki-codec-json. The pure core talks only typed Haskell values; the shape hash discriminates snapshots regardless of codec choice.
Validated against
  • GHC 9.12.2 locally on macOS aarch64 and in CI on Ubuntu Linux x86_64 (see .github/workflows/ci.yml).
  • 278 hspec assertions in the in-tree test suite, including 11 Keiki.ShapeSpec golden assertions for the shape hash, 10 Keiki.CoreInFlightSpec assertions for the GSM streaming replay path, and 3 Keiki.CompositionMultiEventSpec assertions for multi-event composition. The downstream jitsurei package adds 96 more assertions exercising eight worked-example aggregates against the public surface.