keiki-0.8.0.0: CHANGELOG.md

# Changelog

All notable changes to this package are documented in this file.
The format follows [Keep a Changelog](https://keepachangelog.com/),
and this project adheres to the
[Haskell PVP](https://pvp.haskell.org).


## [Unreleased]


## [0.8.0.0] — 2026-08-02

### Added

- `TOpaqueLit` and `opaqueLit` preserve exact concrete, replay, pure-analysis,
  and symbolic literal semantics while deliberately rendering the stored value
  as `<lit>`.
- `MermaidUpdateMode`, `topologyMermaidOptions`, and `toTopologyMermaid` make
  complete updates, compact written-slot summaries, and Keiki 0.7-compatible
  topology output explicit policies.
- Options-aware Mermaid entry points now cover composite, nested, three-way,
  alternative, feedback, and labeled diagrams. Backend-level regression tests
  pin semantic-label escaping through the documentation site's
  `beautiful-mermaid` renderer.

### Changed

- **Breaking:** `TLit` and `lit` now require `Show` so renderers derive ordinary
  literal text from the executable value. Exhaustive `Term` matches must handle
  `TOpaqueLit`; values without `Show`, secrets, and deliberately redacted values
  use `opaqueLit`.
- **Breaking:** `toMermaid` and every no-options shape renderer now default to
  readable guards, complete register assignments, multiline labels, and no
  semantic truncation. Use `toTopologyMermaid` or an options-aware shape
  renderer with `topologyMermaidOptions` for the previous compact bytes.
- **Breaking:** `MermaidOptions` removes `showWrittenSlots` and
  `showGuardSummary`. Set `updateMode = MermaidUpdateWrittenSlots` and
  `guardMode = MermaidGuardStructuralSummary` respectively.


## [0.7.0.0] — 2026-08-01

### Added

- `Keiki.ProjectionDomain` provides backend-neutral exact images for nominal
  projections: non-empty finite domains, audited whole-carrier domains, and a
  validated full-string `TextPattern` algebra with literal, character set/range,
  concatenation, alternation, and bounded repetition forms.
- `ExactFieldProjection`, `exactFieldWitness`,
  `checkFieldProjectionOwner`, and `checkFieldProjectionKey` let one coherent
  projection tag declare its complete image and a checked canonical-owner
  inverse without changing existing `fieldWitness` call sites.
- `predicateTranslationReport` explains predicate-wide exactness, including
  conflicting views, direct-plus-projected reads, unsupported operations, and
  unguarded input projections. `verifyPredicateDetailed` returns translation
  strength, full solver status, and typed, checked path-local
  `ProjectionModel` values. Detailed determinism and dead-edge APIs retain the
  one solver result and `EdgeRef` attribution used by compatibility warnings.
- `StepSuccess` and `stepDetailedEither` expose the exact construction-local
  `EdgeRef`, `Live` mode, post-state, registers, and ordered output word selected
  by forward execution. `stepEither` preserves its signature and erases this
  proof-relevant success without changing failures.
- `ReplayEventSpan`, `ReplayAttribution`, `ReplaySuccess`,
  `applyEventsDetailedEither`, and `reconstituteDetailedEither` expose an
  ordered completed-edge factorization of a successful strict replay. Spans
  are zero-based and half-open, multi-event tails complete one attribution,
  live-first mode is reported exactly, and epsilon-output edges remain
  unobservable in replay. Existing replay functions share the evaluator but
  retain a nullary no-trace policy and O(1) auxiliary trace state.

### Changed

- Exact projection domains are constrained once per structured symbolic key.
  Finite domains are accepted only when every literal round-trips through its
  symbolic representation and satisfies backend bounds such as Text's
  U+2FFFF ceiling; unsupported domains emit no partial constraint.
  Satisfying model keys are checked for domain membership, inverse success, and
  getter round-trip before they are exposed. Relation-safe owners may override
  the matching structural path during `symSatExt`, whose final concrete recheck
  remains authoritative.
- `verifyPredicate` is now a compatibility projection of the detailed solver
  result and reports verified SAT/UNSAT only for predicate-global exact
  translations. `symIsBot`, determinism, and dead-edge compatibility paths use
  the same failure-aware solving kernel; only definite UNSAT counts as proof.
- **Semantic correctness fix:** `predicateTranslationExact` no longer treats a
  one-way `fieldWitness` projection as exact merely because its result carrier
  is solver-supported. Existing projection callers now receive
  `UnverifiedOpaque` from `verifyPredicate`; path-stable repeated reads and the
  conservative `symIsBot` emptiness proof remain available. The new
  documented-internals query `fieldWitnessHasExactDomain` reports the private
  evidence used by this classification and returns `False` for every released
  `fieldWitness`.
- `symSatExt` now concretely rechecks every reconstructed candidate, restoring
  the unconditional guarantee that each returned pair satisfies `models`.
  Unrealizable free projection assignments, opaque `TApp1`/`TApp2`
  assignments, and non-`Sym` equality fallbacks now return `Nothing` instead
  of a pair that fails concrete evaluation. `Nothing` remains “no concrete
  witness recovered,” not proof of unsatisfiability.


## [0.6.0.0] — 2026-07-31

### Added

- `verifyPredicate`, `predicateTranslationExact`, and
  `PredicateVerification` expose whether a predicate received an exact
  structural translation and a definite solver answer. Opaque fallbacks,
  solver `Unknown`/timeouts, and solver failures remain explicitly unverified.

### Changed

- **Breaking semantic fix:** structural `Natural` addition and multiplication
  are now solver-visible, and structural subtraction is total monus in both
  concrete and symbolic evaluation: `a - b = max 0 (a - b)`. It never invokes
  partial Haskell `Natural` subtraction on an underflowing pair; the symbolic
  form is `ite (a >= b) (a - b) 0`.
- `Natural` now belongs to the curated symbolic numeric registry, so
  `OpaqueGuard` no longer reports structural `Natural` arithmetic.


## [0.5.0.0] — 2026-07-31

### Added

- `Natural` now has a pinned `CanonicalTypeName` and belongs to the curated
  symbolic equality/ordering registry. Its unbounded integer representation is
  constrained non-negative whenever Keiki allocates a symbolic variable.
- `Sym.constrainSymDomain` lets refined scalar instances state the validity
  invariant for their solver representation. `symFree`, structural register
  and input reads, field projections, and opaque term fallbacks all apply it.

### Changed

- `Natural` is deliberately absent from the symbolic arithmetic registry.
  Haskell subtraction on `Natural` throws `Underflow` when its mathematical
  result would be negative, whereas ordinary SMT integer subtraction returns
  that negative value.
- The opt-in opaque-guard audit now reports `TArith` whose carrier is absent
  from the symbolic numeric registry, including `Natural` arithmetic.
- The fast pure overlap validator treats `Natural` as the exact integral
  interval `[0, infinity)`, so it can find non-literal interior witnesses.
- The `OpaqueGuard` warning detail no longer names `TApp` specifically, since
  the audit now covers unsupported `TArith` carriers too. Consumers asserting
  on the exact message text will need to update.
- PVP major bump: the `Sym` class definition gained `constrainSymDomain`. The
  method has a default, so existing hand-written instances continue to compile
  unchanged.


## [0.4.0.0] — 2026-07-28

### Added

- `Keiki.Core` now exposes nominal typed field projections over
  consumer-owned values: `FieldProjection(..)`, abstract `FieldWitness`,
  `fieldWitness`, `ProjBase(..)`, `regProj`, `inpProj`,
  `fieldProjectionPath`, `fieldWitnessAgrees`, and the documented-internals
  helpers `fieldWitnessGet` and `indexPosition`. A projection reads one scalar
  field from a direct register or matched input field without requiring the
  owner type to have a symbolic representation.
- `Keiki.Symbolic.constrainFieldProjection` binds a memoized projection to a
  concrete getter result for concrete-to-symbolic agreement tests. Repeated
  reads share through structured base, nominal tag, owner, and result identity;
  caller-controlled diagnostic strings never determine solver identity.
- `ProjectionResultUnsupported`, `ProjectionOrderingUnsupported`, and
  `ProjectionOutsideGuard` make unsupported result types, unsupported ordering,
  and projected writes/outputs unconditional validation findings.
- `NonStructuralProjectionBoundary` identifies mapped composition boundaries
  that cannot retain a stable typed projection path, including pending writes
  in multi-event chains.

### Changed

- **Breaking:** `Term` gains the `TFieldProj` constructor. Code that exhaustively
  matches `Term` must handle it. Concrete evaluation applies the projection's
  total coherent getter; replay treats the result as derived.
- **Breaking:** `TransducerValidationWarning` and `ComposeAlignmentWarning` gain
  the projection constructors above, and `checkComposeAlignment` now requires
  the structural `WeakenR` evidence used to inspect mapped upstream terms.
- Projection use is guards-only in validated transducers. Equality requires a
  result in the curated symbolic registry, ordering requires its ordering
  subset, and input projections retain the existing `PInCtor` and hidden-input
  disciplines.
- Composition preserves a projection over a direct register/input owner, folds
  a literal owner, and lowers any computed owner to an opaque `TApp1`. Raw
  composition remains forward-correct; `composeChecked` rejects the precision-
  losing case.
- `symSatExt` does not reconstruct consumer-owned values from free projection
  scalars. The supported agreement is one-way: every concrete owner can bind a
  matching symbolic projection value, but an arbitrary symbolic projection
  model need not correspond to a constructible owner.


## [0.3.1.0] — 2026-07-23

### Added

- `Keiki.Shape.CanonicalStateShape`, `stateShapeCanonical`, and
  `stateShapeHash` provide a generic, deterministic control-state discriminator
  for snapshot compatibility. The canonical form records datatype and
  constructor identity plus field type names; semantic fold changes still need
  an explicit version or fold fingerprint.


## [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 `SymTransducer`s.
- `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.