keiki 0.1.0.0 → 0.2.0.0

raw patch · 56 files changed

+8074/−2894 lines, 56 filesdep +QuickCheckPVP ok

version bump matches the API change (PVP)

Dependencies added: QuickCheck

API changes (from Hackage documentation)

Files

• CHANGELOG.md +147/−7
• README.md +17/−13
• keiki.cabal +26/−8
• src/Keiki/Acceptor.hs +27/−17
• src/Keiki/Builder.hs +283/−154
• src/Keiki/Composition.hs +579/−47
• src/Keiki/Core.hs +2677/−1830
• src/Keiki/Decider.hs +0/−119
• src/Keiki/Generics.hs +9/−2
• src/Keiki/Generics/TH.hs +100/−36
• src/Keiki/Internal/Slots.hs +33/−5
• src/Keiki/Profunctor.hs +236/−115
• src/Keiki/Render/Inspector.hs +2/−0
• src/Keiki/Render/Mermaid.hs +4/−0
• src/Keiki/Render/Pretty.hs +2/−0
• src/Keiki/Render/Validate.hs +5/−1
• src/Keiki/Shape.hs +94/−33
• src/Keiki/Symbolic.hs +97/−66
• test/Keiki/AcceptorSpec.hs +53/−3
• test/Keiki/ArrowSpec.hs +28/−14
• test/Keiki/BuilderSpec.hs +127/−6
• test/Keiki/BuilderSpike.hs +13/−5
• test/Keiki/BuilderTypeErrorsSpec.hs +77/−0
• test/Keiki/CategorySpec.hs +120/−16
• test/Keiki/ChoiceSpec.hs +51/−22
• test/Keiki/CompositionAlignmentSpec.hs +118/−0
• test/Keiki/CompositionAlternativeSpec.hs +38/−1
• test/Keiki/CompositionFeedback1Spec.hs +11/−0
• test/Keiki/CompositionHomomorphismSpec.hs +154/−0
• test/Keiki/CompositionNarySpec.hs +3/−0
• test/Keiki/CompositionSpec.hs +3/−4
• test/Keiki/CompositionStatefulSpec.hs +48/−0
• test/Keiki/CoreHiddenInputsGSMSpec.hs +35/−168
• test/Keiki/CoreSpec.hs +31/−0
• test/Keiki/DeciderSpec.hs +0/−152
• test/Keiki/Fixtures/BrokenTailCoverage.hs +130/−0
• test/Keiki/Fixtures/ComposeStateful.hs +366/−0
• test/Keiki/Fixtures/CounterPipeline.hs +153/−0
• test/Keiki/Fixtures/EmailDelivery.hs +1/−1
• test/Keiki/Fixtures/RegisterEmission.hs +140/−0
• test/Keiki/Fixtures/SplitCoverage.hs +142/−0
• test/Keiki/Fixtures/UserRegistration.hs +20/−5
• test/Keiki/Generics/THSpec.hs +3/−0
• test/Keiki/LawHelpers.hs +27/−0
• test/Keiki/ProfunctorSpec.hs +25/−0
• test/Keiki/Render/InspectorSpec.hs +4/−3
• test/Keiki/Render/MermaidSpec.hs +7/−7
• test/Keiki/ReplayEitherSpec.hs +280/−0
• test/Keiki/RoundTrip.hs +332/−0
• test/Keiki/RoundTripSpec.hs +371/−0
• test/Keiki/ShapeSpec.hs +55/−11
• test/Keiki/StrongSpec.hs +39/−14
• test/Keiki/SymbolicSpec.hs +127/−0
• test/Keiki/ValidationReplayAlignmentSpec.hs +380/−0
• test/Keiki/ValidationSpec.hs +210/−7
• test/Spec.hs +14/−2

@@ -9,6 +9,153 @@ ## [Unreleased]  +## [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@@ -32,13 +179,6 @@ - `Keiki.Builder` — the monadic edge-authoring DSL. - `Keiki.Composition` — sequential, alternative, and single-step   feedback combinators on `SymTransducer`s.-- `Keiki.Decider` — the Chassaing-shape `Decider` facade-  (`decide` / `evolve` / `evolveStreaming` / `initialState` /-  `isTerminal`) derived mechanically from a `SymTransducer`.-  `decide` returns the full event list directly, including-  length-2+ chains from multi-event edges; `evolveStreaming`-  threads the `Keiki.Core.InFlight` wrapper through length-N-  edges for event-by-event streaming replay. - `Keiki.Generics` — `RegFieldsOf`, `GRecord`, `mkInCtor` /   `mkInCtorVia`, `mkWireCtor` / `mkWireCtorVia`, plus `EmptyRegFile`. - `Keiki.Generics.TH` — `deriveAggregateCtors`, `deriveWireCtors`,

@@ -5,10 +5,10 @@ symbolic-register finite-state transducer.  keiki keeps the runtime boundary deliberately small. You describe an-aggregate or workflow once as a typed transducer; the library derives-the event-sourcing facade, replay, acceptors, projections, composition-machinery, diagram renderers, and optional symbolic checks from that-single declaration.+aggregate or workflow once as a typed transducer; the library provides+forward decisions, replay, acceptors, projections, composition machinery,+diagram renderers, and optional symbolic checks from that single+declaration.  ## The name @@ -44,15 +44,17 @@ keiki models all three as **finite-state transducers** with a typed register file and predicate-labelled guards: a practical hybrid of Symbolic Finite Transducers and Streaming String Transducers. From one-`SymTransducer` declaration, the library mechanically derives:+`SymTransducer` declaration, the library provides: -- the Chassaing-shape `Decider` (`decide`/`evolve`/`initialState`/`isTerminal`),+- strict forward-decision and replay operations with structured failure diagnostics+  (`stepEither`, `reconstituteEither`, and `replayEvents`), - input- and output-side `Acceptor`s, - per-vertex projections (the "B-presentation" view),-- composition (`compose`, `alternative`, `feedback1`),-- profunctor / `Category` / `Strong` / `Choice` instances,+- checked sequential composition (`composeChecked`) plus `alternative` and `feedback1`,+- profunctor / `Category` / `Strong` / `Choice` / `Arrow` instances, - Mermaid and Markdown renderers for documentation,-- single-valuedness checks via SBV + z3 as an opt-in symbolic CI gate.+- eager builder validation, default-on replay-safety checks, and optional+  single-valuedness checks via SBV + z3.  `delta` / `omega` / `applyEvent` use concrete predicate evaluation — no solver in the per-event hot path. Solver dispatch is reserved for@@ -67,7 +69,9 @@ The core package is intentionally codec-free. JSON support lives in [`keiki-codec-json`](keiki-codec-json/README.md), and downstream codec testing helpers live in-[`keiki-codec-json-test`](keiki-codec-json-test/README.md).+[`keiki-codec-json-test`](keiki-codec-json-test/README.md). The JSON event+codec supports pinned wire kinds, in-band schema versions, and explicit+upcaster chains for persisted-event evolution.  ## Build @@ -106,9 +110,9 @@       B.goto EmailSentVertex ``` -`Decider`, `Acceptor`, replay, and the per-vertex view are all derived-from this one declaration. See the sibling `jitsurei/` package for the-full worked aggregates the test suite drives.+Forward decisions, structured replay, `Acceptor`s, and the per-vertex+view all operate from this one declaration. See the downstream+`jitsurei` package for the full worked aggregates the test suite drives.  ## Repository documentation 

@@ -1,6 +1,6 @@ cabal-version:   3.0 name:            keiki-version:         0.1.0.0+version:         0.2.0.0 synopsis:        Pure core for symbolic-register transducer event sourcing. description:   A Haskell library for the pure core of event sourcing, workflow@@ -9,11 +9,12 @@   Transducers and Streaming String Transducers).   .   Provides a typed register-file (@RegFile rs@), a deterministic-  transducer DSL with predicate-labelled guards, composition-  combinators (sequential, alternative, single-step feedback), a-  mechanically-derived @Decider@ facade, input- and output-side-  acceptors, generic Mermaid renderers, and a GHC-upgrade-safe-  shape hash (@Keiki.Shape@) for snapshot discrimination.+  transducer DSL with eager builder validation and replay-safety+  analyses, structured forward-decision and replay operations,+  composition combinators (checked sequential, alternative,+  single-step feedback), input- and output-side acceptors, generic+  Mermaid renderers, and a GHC-upgrade-safe shape hash+  (@Keiki.Shape@) for snapshot discrimination.   .   The library is intentionally codec-free: the pure layer talks   only typed Haskell values. JSON serialisation lives in the@@ -31,6 +32,10 @@   CHANGELOG.md   README.md +source-repository head+  type:     git+  location: https://github.com/shinzui/keiki.git+ common warnings   ghc-options:     -Wall -Wcompat -Widentities -Wincomplete-record-updates@@ -61,7 +66,6 @@     Keiki.Builder     Keiki.Composition     Keiki.Core-    Keiki.Decider     Keiki.Generics     Keiki.Generics.TH     Keiki.Internal.Slots@@ -99,22 +103,31 @@     Keiki.ArrowSpec     Keiki.BuilderSpec     Keiki.BuilderSpike+    Keiki.BuilderTypeErrorsSpec     Keiki.CategorySpec     Keiki.ChoiceSpec     Keiki.CollectionSpike+    Keiki.CompositionAlignmentSpec     Keiki.CompositionAlternativeSpec     Keiki.CompositionFeedback1Spec+    Keiki.CompositionHomomorphismSpec     Keiki.CompositionMultiEventSpec     Keiki.CompositionNarySpec     Keiki.CompositionSpec+    Keiki.CompositionStatefulSpec     Keiki.CoreApplyEventsSpec     Keiki.CoreHiddenInputsGSMSpec     Keiki.CoreInFlightSpec     Keiki.CoreSpec-    Keiki.DeciderSpec+    Keiki.Fixtures.BrokenTailCoverage+    Keiki.Fixtures.ComposeStateful+    Keiki.Fixtures.CounterPipeline     Keiki.Fixtures.EmailDelivery+    Keiki.Fixtures.RegisterEmission+    Keiki.Fixtures.SplitCoverage     Keiki.Fixtures.UserRegistration     Keiki.Generics.THSpec+    Keiki.LawHelpers     Keiki.NoThunksSpec     Keiki.OperatorsQualifiedSpec     Keiki.OperatorsSpec@@ -125,10 +138,14 @@     Keiki.Render.MermaidSpec     Keiki.Render.PrettySpec     Keiki.Render.ValidateSpec+    Keiki.ReplayEitherSpec+    Keiki.RoundTrip+    Keiki.RoundTripSpec     Keiki.ShapeSpec     Keiki.StepEitherSpec     Keiki.StrongSpec     Keiki.SymbolicSpec+    Keiki.ValidationReplayAlignmentSpec     Keiki.ValidationSpec    build-depends:@@ -139,6 +156,7 @@     , keiki     , nothunks     >=0.3   && <0.4     , profunctors  >=5.6   && <6+    , QuickCheck   ^>=2.15     , sbv          >=11.7  && <15     , text         ^>=2.1     , time         ^>=1.14

@@ -16,7 +16,7 @@ --   replayable logs. -- -- In 'Keiki.Core' these projections are /implicit/: π₁ is--- 'Keiki.Core.delta'; π₂ is 'Keiki.Core.applyEvent'. This module+-- 'Keiki.Core.delta'; π₂ is 'Keiki.Core.applyEventStreaming'. This module -- /names/ them as a first-class data type so downstream code (UI, -- validation, generated documentation) can pattern-match on a known -- shape instead of plumbing the step functions by hand.@@ -29,8 +29,7 @@ -- @ -- -- See @docs/research/acceptor-projections-design.md@ for the design--- record (deferred scope, why the state carrier is--- @(s, 'Keiki.Core.RegFile' rs)@, relationship to 'Keiki.Decider').+-- record and relationship to Core replay. module Keiki.Acceptor   ( -- * The acceptor projection     Acceptor (..),@@ -47,9 +46,10 @@  import Keiki.Core   ( BoolAlg,+    InFlight (..),     RegFile,     SymTransducer (..),-    applyEvent,+    applyEventStreaming,     delta,   ) @@ -65,7 +65,7 @@ --   terminates in a state for which this predicate holds. -- -- The richer return type of 'Keiki.Core.delta' /--- 'Keiki.Core.applyEvent' (which thread an updated 'RegFile') is+-- 'Keiki.Core.applyEventStreaming' (which thread an updated 'RegFile') is -- preserved by the projections in this module by hiding the register -- file inside @s@; see 'inputAcceptor' / 'outputAcceptor'. --@@ -107,29 +107,39 @@  -- | Project a 'SymTransducer' to its /output/ acceptor (π₂): the -- acceptor over the event alphabet whose step is--- 'Keiki.Core.applyEvent'.+-- 'Keiki.Core.applyEventStreaming'. ----- The state carrier is @(s, 'RegFile' rs)@ because 'applyEvent'--- itself threads the register file through replay.+-- The state carrier is @('Keiki.Core.InFlight' s co, 'RegFile' rs)@+-- because streaming replay must remember the expected tail of a+-- multi-event output chain as well as the register file. -- -- @ -- accepts (outputAcceptor t) events  ==  True -- @ ----- iff successively applying 'Keiki.Core.applyEvent' to each event--- reaches a final control vertex — equivalently, iff--- @'Keiki.Core.reconstitute' t events@ returns 'Just' a final--- @(s, regs)@. The output acceptor /is/ the @evolve@ acceptor the--- foundations chapter derives.+-- is equivalent to:+--+-- @+-- case 'Keiki.Core.reconstitute' t events of+--   Just (s, _) -> 'isFinal' t s+--   Nothing     -> False+-- @+--+-- A log rejects when an event cannot replay or when the log ends in+-- the middle of a multi-event chain, leaving a non-final 'InFlight'+-- carrier. outputAcceptor ::   (BoolAlg phi (RegFile rs, ci), Eq co) =>   SymTransducer phi rs s ci co ->-  Acceptor co (s, RegFile rs)+  Acceptor co (InFlight s co, RegFile rs) outputAcceptor t =   Acceptor-    { aStep = \(s, regs) co -> applyEvent t s regs co,-      aInitial = (initial t, initialRegs t),-      aIsFinal = \(s, _regs) -> isFinal t s+    { aStep = \(wrapper, regs) co ->+        applyEventStreaming t wrapper regs co,+      aInitial = (Settled (initial t), initialRegs t),+      aIsFinal = \(wrapper, _regs) -> case wrapper of+        Settled s -> isFinal t s+        InFlight {} -> False     }  -- | Run an 'Acceptor' over a sequence. Returns 'Just' the terminal

@@ -5,7 +5,7 @@ -- builder is purely additive on top of "Keiki.Core": every edge it -- produces is a value of the existing 'Keiki.Core.Edge' type, and -- the resulting 'Keiki.Core.SymTransducer' is consumed unchanged by--- "Keiki.Acceptor", "Keiki.Composition", "Keiki.Decider",+-- "Keiki.Acceptor", "Keiki.Composition", -- "Keiki.Symbolic", and the example-side specs. -- -- == Why a builder@@ -114,12 +114,28 @@ --   the 'Keiki.Internal.Slots.Disjoint' 'GHC.TypeError.TypeError', --   which names the duplicated slot. ----- * Missing 'goto': caught at finalize time (when 'buildTransducer'---   evaluates the 'VertexBuilder' do-block) with a runtime error---   naming the source vertex and edge index.+-- * Duplicate names in the register file: caught at compile time by+--   the 'Keiki.Internal.Slots.DistinctNames' constraint on the two+--   build entry points. ----- * Multiple 'goto's in the same edge body: caught the same way.+-- * An 'emit' whose term-fields schema differs from its enclosing+--   'onCmd', or an 'emit' inside 'onEpsilon': caught at compile time. --+-- * Missing or multiple 'goto's: every declared edge is checked when+--   the transducer returned by 'buildTransducer' is first evaluated,+--   even if its source vertex is never inspected. All defects are+--   reported together with source vertices and edge indices. Use+--   'buildTransducerEither' to receive them as structured values.+--+-- * An 'emitWith' inside 'onCmd' whose explicit input constructor+--   differs in name or slot names from the enclosing constructor:+--   rejected by the same eager validation pass.+--+-- * An edge with neither 'emit' / 'emitWith' nor 'noEmit': rejected+--   by eager validation with a located structured defect directing+--   the user to declare whether the edge emits or is deliberately+--   silent.+-- -- == When to drop down to the AST -- -- Use the AST directly when:@@ -138,6 +154,10 @@ module Keiki.Builder   ( -- * Top-level entry point     buildTransducer,+    buildTransducerEither,+    BuilderDefect (..),+    BuilderError (..),+    renderBuilderErrors,      -- * Vertex-level builder     VertexBuilder,@@ -194,6 +214,9 @@   ) where +import Data.List (intercalate)+import Data.List.NonEmpty (NonEmpty)+import Data.List.NonEmpty qualified as NonEmpty import Data.Typeable (Typeable) import GHC.Records (HasField (..)) import GHC.TypeLits (KnownSymbol, Symbol)@@ -201,11 +224,12 @@   ( Cmp (..),     Edge (..),     HsPred (..),-    InCtor,+    InCtor (..),     Index,     OutFields (..),-    OutTerm,+    OutTerm (..),     RegFile,+    Slot,     SymTransducer (..),     Term (TReg),     Update (..),@@ -215,16 +239,18 @@     matchInCtor,     oNil,     pack,+    slotNamesOf,     (*:),   ) import Keiki.Core qualified as K import Keiki.Internal.Slots   ( Concat,     Disjoint,+    DistinctNames,     HasIndexN (..),     IndexN (..),+    Names,   )-import Unsafe.Coerce (unsafeCoerce) import Prelude hiding (pure, return, (>>), (>>=)) import Prelude qualified @@ -244,9 +270,10 @@ -- 'PTop' or @'matchInCtor' ic@ as guard, 'UKeep' as update, no -- output, no targets); each step in the body modifies one or more -- fields; 'finalizeEdge' validates that exactly one 'goto' was--- called and packages the result into a closed 'Edge'. The+-- called and that output intent was declared, then packages the+-- result into a closed 'Edge'. The -- existential @w@ on 'Edge''s 'update' field closes here.-data PartialEdge rs ci co v (w :: [Symbol]) = PartialEdge+data PartialEdge rs ci co v (pin :: Maybe [Slot]) (w :: [Symbol]) = PartialEdge   { peGuard :: HsPred rs ci,     peUpdate :: Update rs w ci,     -- | Output terms accumulated by 'emit' / 'emitWith' calls in@@ -258,23 +285,19 @@     -- | Reverse-order list of every 'goto' invocation in the body.     -- Finalization requires exactly one element.     peTargets :: [v],-    -- | The 'InCtor' bound by the enclosing 'onCmd', so that the-    -- 2-argument 'emit' can recover it without the user repeating-    -- it. 'Nothing' inside an 'onEpsilon' body — 'emit' there must-    -- use 'emitWith' to supply the 'InCtor' explicitly.-    peInCtor :: Maybe (PeInCtor ci)+    -- | The 'InCtor' bound by the enclosing 'onCmd', indexed by its+    -- real input-field schema. 'PinNone' marks an 'onEpsilon' body.+    pePinned :: Pinned ci pin,+    -- | Whether the body explicitly chose to emit or remain silent.+    -- Any 'emit', 'emitWith', or 'noEmit' call sets this to 'True'.+    peOutputDecided :: Bool   } --- | Existential wrapper hiding the @ifs@ slot list of an 'InCtor'.--- Stored on 'PartialEdge' by 'onCmd' and read back by 'emit'.------ This is a builder-local existential rather than a reuse of--- 'Keiki.Symbolic.SomeInCtor' because the latter carries an--- 'ExtractRegFile' constraint the builder does not need and lives--- in a module that pulls SBV; reusing it would add an SBV edge to--- every consumer of "Keiki.Builder".-data PeInCtor ci where-  PeInCtor :: InCtor ci ifs -> PeInCtor ci+-- | Whether an edge body has an enclosing input constructor. The+-- schema index preserves the equality that 'emit' needs.+data Pinned ci (pin :: Maybe [Slot]) where+  PinNone :: Pinned ci 'Nothing+  PinCtor :: InCtor ci ifs -> Pinned ci ('Just ifs)  -- | The per-edge indexed-state monad. The two phantom slot-set -- indices @(w :: [Symbol])@ (before this step) and @(w' :: [Symbol])@@@ -289,11 +312,11 @@ -- requires a separate type-class hierarchy. Instead, this module -- exports its own @(>>=)@ / @(>>)@ / 'pure' / 'return' for use -- with @QualifiedDo@.-newtype EdgeBuilder rs ci co v (w :: [Symbol]) (w' :: [Symbol]) a+newtype EdgeBuilder rs ci co v (pin :: Maybe [Slot]) (w :: [Symbol]) (w' :: [Symbol]) a   = EdgeBuilder   { runEdgeBuilder ::-      PartialEdge rs ci co v w ->-      (a, PartialEdge rs ci co v w')+      PartialEdge rs ci co v pin w ->+      (a, PartialEdge rs ci co v pin w')   }  -- * QualifiedDo bind/return exports ----------------------------------------@@ -302,9 +325,9 @@ -- the second argument's @w@ argument, and the second argument's @w'@ -- index becomes the result's @w'@. Re-export for @QualifiedDo@. (>>=) ::-  EdgeBuilder rs ci co v w1 w2 a ->-  (a -> EdgeBuilder rs ci co v w2 w3 b) ->-  EdgeBuilder rs ci co v w1 w3 b+  EdgeBuilder rs ci co v pin w1 w2 a ->+  (a -> EdgeBuilder rs ci co v pin w2 w3 b) ->+  EdgeBuilder rs ci co v pin w1 w3 b EdgeBuilder f >>= k = EdgeBuilder $ \pe ->   let (a, pe1) = f pe       EdgeBuilder g = k a@@ -314,19 +337,19 @@  -- | Sequence. Defined in terms of '(>>=)'. (>>) ::-  EdgeBuilder rs ci co v w1 w2 a ->-  EdgeBuilder rs ci co v w2 w3 b ->-  EdgeBuilder rs ci co v w1 w3 b+  EdgeBuilder rs ci co v pin w1 w2 a ->+  EdgeBuilder rs ci co v pin w2 w3 b ->+  EdgeBuilder rs ci co v pin w1 w3 b m >> n = m Keiki.Builder.>>= \_ -> n  infixl 1 >>  -- | Embed a value. Slot-set unchanged.-pure :: a -> EdgeBuilder rs ci co v w w a+pure :: a -> EdgeBuilder rs ci co v pin w w a pure a = EdgeBuilder $ \pe -> (a, pe)  -- | Synonym for 'pure'. Re-exported for @QualifiedDo@.-return :: a -> EdgeBuilder rs ci co v w w a+return :: a -> EdgeBuilder rs ci co v pin w w a return = Keiki.Builder.pure  -- * Slot writes ----------------------------------------------------------@@ -394,11 +417,11 @@ -- 'Keiki.Core.lit' / 'Keiki.Core.proj' / 'Keiki.Core.inpCtor' or -- @d.fieldName@ via 'PayloadProj' to construct it. (.=) ::-  forall name r rs ci ifs co v w.+  forall name r rs ci ifs co v pin w.   (KnownSymbol name, Disjoint '[name] w) =>   IndexN name rs r ->   Term rs ci ifs r ->-  EdgeBuilder rs ci co v w (Concat '[name] w) ()+  EdgeBuilder rs ci co v pin w (Concat '[name] w) () ix .= t = EdgeBuilder $ \pe ->   ((), pe {peUpdate = USet ix t `combine` peUpdate pe}) @@ -416,11 +439,11 @@ -- reserves operators beginning with a colon for data constructors, so a -- value-level synonym must start with another symbol — hence @=:@.) (=:) ::-  forall name r rs ci ifs co v w.+  forall name r rs ci ifs co v pin w.   (KnownSymbol name, Disjoint '[name] w) =>   IndexN name rs r ->   Term rs ci ifs r ->-  EdgeBuilder rs ci co v w (Concat '[name] w) ()+  EdgeBuilder rs ci co v pin w (Concat '[name] w) () (=:) = (.=)  infixr 6 =:@@ -428,10 +451,9 @@ -- * Termination -----------------------------------------------------------  -- | Set the edge's target vertex. Required exactly once per edge--- body; missing 'goto' produces a finalize-time runtime error--- naming the source vertex and edge index, and so does multiple--- 'goto's in the same body.-goto :: v -> EdgeBuilder rs ci co v w w ()+-- body; missing or multiple 'goto's are reported by the eager+-- validation pass, with the source vertex and edge index.+goto :: v -> EdgeBuilder rs ci co v pin w w () goto v = EdgeBuilder $ \pe ->   ((), pe {peTargets = v : peTargets pe}) @@ -442,9 +464,8 @@ -- either a per-event @\<CtorName\>TermFields rs ci@ record (emitted -- by 'Keiki.Generics.TH.deriveWireCtors') or a bare 'OutFields' -- HList constructed with '(*:)' / 'oNil'. The input-side 'InCtor'--- is recovered from the enclosing 'onCmd'; an 'emit' inside--- 'onEpsilon' (where no 'InCtor' is bound) raises a finalize-time--- error directing the user to 'emitWith'.+-- is recovered at its real schema from the enclosing 'onCmd'. An+-- 'emit' inside 'onEpsilon' is a compile error; use 'emitWith' there. -- -- == Multi-event commands (EP-19) --@@ -461,62 +482,48 @@   (ToOutFields rec rs ci ifs fs) =>   WireCtor co fs ->   rec ->-  EdgeBuilder rs ci co v w w ()-emit wc rec = EdgeBuilder $ \pe -> case peInCtor pe of-  Just (PeInCtor ic) ->-    -- 'onCmd' pins the same 'InCtor' into 'peInCtor' /and/ into the-    -- 'PayloadProj' the body projects through, so the record's input-    -- field schema 'ifs' (from 'ToOutFields') equals the pinned-    -- 'InCtor''s schema. The existential 'PeInCtor' hides that-    -- equality; 'reIndexPinnedInCtor' re-establishes it. This does not-    -- weaken replay soundness: the resulting 'OPack''s 'InCtor' and-    -- 'OutFields' share 'ifs', so 'solveOutput' recovers fields with no-    -- coercion (EP-53). Mirrors 'Keiki.Composition.unsafeCoerceInCtor'.+  EdgeBuilder rs ci co v ('Just ifs) w w ()+emit wc rec = EdgeBuilder $ \pe -> case pePinned pe of+  PinCtor ic ->     ( (),       pe         { peOutput =             peOutput pe-              ++ [pack (reIndexPinnedInCtor @ci @_ @ifs ic) wc (toOutFields rec)]+              ++ [pack ic wc (toOutFields rec)],+          peOutputDecided = True         }     )-  Nothing ->-    error-      "Keiki.Builder.emit: no enclosing onCmd pinned an InCtor. \-      \Use 'emitWith ic wc fs' inside 'onEpsilon', or move the \-      \emit inside an 'onCmd' block." --- | Re-establish the (existentially hidden) equality between a pinned--- 'InCtor''s field schema and the schema the enclosing 'onCmd''s--- 'PayloadProj' exposes. Unsound in general; justified at the single--- 'emit' call site by 'onCmd' storing one and the same 'InCtor' in both--- places (see 'emit'). The runtime representation is identical.-reIndexPinnedInCtor :: forall ci ifs0 ifs. InCtor ci ifs0 -> InCtor ci ifs-reIndexPinnedInCtor = unsafeCoerce---- | Emit an event with an explicit 'InCtor'. The escape hatch for--- 'onEpsilon' bodies (which do not pin an 'InCtor') and for any--- caller that needs to override the one bound by the enclosing--- 'onCmd'. Inside 'onCmd' the InCtor-less 'emit' is preferred.--- Like 'emit', accumulates into the edge's output list — multiple--- calls produce a multi-event edge.+-- | Emit an event with an explicit 'InCtor'. This is the output form+-- for 'onEpsilon' bodies, which have no pinned constructor. Inside+-- 'onCmd', the supplied constructor must have the same name and slot+-- names as the pinned constructor; 'buildTransducer' rejects a+-- mismatch eagerly because it would invert replay to another command.+-- The InCtor-less 'emit' is preferred inside 'onCmd'. Like 'emit',+-- accumulates into the edge's output list — multiple calls produce a+-- multi-event edge. emitWith ::-  forall co fs rs ci v w ifs rec.+  forall co fs rs ci v pin w ifs rec.   (ToOutFields rec rs ci ifs fs) =>   InCtor ci ifs ->   WireCtor co fs ->   rec ->-  EdgeBuilder rs ci co v w w ()+  EdgeBuilder rs ci co v pin w w () emitWith ic wc rec = EdgeBuilder $ \pe ->-  ((), pe {peOutput = peOutput pe ++ [pack ic wc (toOutFields rec)]})+  ( (),+    pe+      { peOutput = peOutput pe ++ [pack ic wc (toOutFields rec)],+        peOutputDecided = True+      }+  ) --- | Mark the edge as ε-output (no event). Idempotent: an edge with--- no 'emit' or 'noEmit' call is also an ε-edge by default; 'noEmit'--- exists only so the user can be explicit about intent. Mixing--- 'noEmit' and 'emit' in the same body is allowed but the 'noEmit'--- is a documentation no-op (the 'emit's still produce a non-empty--- output list).-noEmit :: EdgeBuilder rs ci co v w w ()-noEmit = EdgeBuilder $ \pe -> ((), pe)+-- | Declare the edge deliberately silent (an ε-edge with+-- @output = []@). Every body that does not call 'emit' or 'emitWith'+-- must call 'noEmit'; otherwise eager builder validation rejects the+-- edge. Mixing 'noEmit' and 'emit' in one body is allowed, and the+-- emitted terms still populate the output list.+noEmit :: EdgeBuilder rs ci co v pin w w ()+noEmit = EdgeBuilder $ \pe -> ((), pe {peOutputDecided = True})  -- * Field-keyed record sugar --------------------------------------------- @@ -555,7 +562,7 @@ -- Use this when the structural sugar of 'requireEq' is not enough -- (e.g. for negated predicates, disjunctions, or guards constructed -- by helper functions).-requireGuard :: HsPred rs ci -> EdgeBuilder rs ci co v w w ()+requireGuard :: HsPred rs ci -> EdgeBuilder rs ci co v pin w w () requireGuard p = EdgeBuilder $ \pe ->   ((), pe {peGuard = PAnd (peGuard pe) p}) @@ -565,7 +572,7 @@   (Eq r, Typeable r) =>   Term rs ci ifs1 r ->   Term rs ci ifs2 r ->-  EdgeBuilder rs ci co v w w ()+  EdgeBuilder rs ci co v pin w w () requireEq a b = requireGuard (PEq a b)  -- | Conjoin an ordering predicate (@a `op` b@ for the relation named@@ -579,7 +586,7 @@   Cmp ->   Term rs ci ifs1 r ->   Term rs ci ifs2 r ->-  EdgeBuilder rs ci co v w w ()+  EdgeBuilder rs ci co v pin w w () requireCmp op a b = requireGuard (PCmp op a b)  -- | Require @a < b@. See 'requireCmp'.@@ -590,7 +597,7 @@     (Ord r, Typeable r) =>     Term rs ci ifs1 r ->     Term rs ci ifs2 r ->-    EdgeBuilder rs ci co v w w ()+    EdgeBuilder rs ci co v pin w w () requireLt = requireCmp CmpLt requireLe = requireCmp CmpLe requireGt = requireCmp CmpGt@@ -635,8 +642,8 @@ newtype EdgeListBuilder rs ci co v a = EdgeListBuilder   { runEdgeListBuilder ::       v ->-      [Edge (HsPred rs ci) rs ci co v] ->-      (a, [Edge (HsPred rs ci) rs ci co v])+      [Either BuilderDefect (Edge (HsPred rs ci) rs ci co v)] ->+      (a, [Either BuilderDefect (Edge (HsPred rs ci) rs ci co v)])   }  instance Functor (EdgeListBuilder rs ci co v) where@@ -662,22 +669,21 @@ -- into a closed 'Edge'. onCmd ::   forall ci ifs rs co v w.-  (Show v) =>   InCtor ci ifs ->-  (PayloadProj rs ci ifs -> EdgeBuilder rs ci co v '[] w ()) ->+  (PayloadProj rs ci ifs -> EdgeBuilder rs ci co v ('Just ifs) '[] w ()) ->   EdgeListBuilder rs ci co v ()-onCmd ic body = EdgeListBuilder $ \src acc ->+onCmd ic body = EdgeListBuilder $ \_src acc ->   let initial =         PartialEdge           { peGuard = matchInCtor ic,             peUpdate = UKeep,             peOutput = [],             peTargets = [],-            peInCtor = Just (PeInCtor ic)+            pePinned = PinCtor ic,+            peOutputDecided = False           }       (_, finalPE) = runEdgeBuilder (body (PayloadProj ic)) initial-      edgeIx = length acc-      edge = finalizeEdge edgeIx src finalPE+      edge = finalizeEdge finalPE    in ((), edge : acc)  -- | ε-edge entry: no input projection, no input-ctor match-guard.@@ -688,61 +694,89 @@ -- directly with an explicit 'InCtor' if needed. onEpsilon ::   forall rs ci co v w.-  (Show v) =>-  EdgeBuilder rs ci co v '[] w () ->+  EdgeBuilder rs ci co v 'Nothing '[] w () ->   EdgeListBuilder rs ci co v ()-onEpsilon body = EdgeListBuilder $ \src acc ->+onEpsilon body = EdgeListBuilder $ \_src acc ->   let initial =         PartialEdge           { peGuard = PTop,             peUpdate = UKeep,             peOutput = [],             peTargets = [],-            peInCtor = Nothing+            pePinned = PinNone,+            peOutputDecided = False           }       (_, finalPE) = runEdgeBuilder body initial-      edgeIx = length acc-      edge = finalizeEdge edgeIx src finalPE+      edge = finalizeEdge finalPE    in ((), edge : acc) +-- | One structural problem found while closing a single edge body.+data BuilderDefect+  = -- | The body never called 'goto'.+    DefectMissingGoto+  | -- | The body called 'goto' more than once; carries the count.+    DefectMultipleGoto Int+  | -- | An output constructor contradicts the enclosing 'onCmd'.+    DefectOutputCtorMismatch String [String] String [String]+  | -- | The body neither emitted nor explicitly declared silence.+    DefectMissingOutputIntent+  deriving stock (Eq, Show)++-- | A defect located at a specific edge of a specific source vertex.+-- The edge index is assigned after duplicate-'from' merging.+data BuilderError v = BuilderError+  { beVertex :: v,+    beEdgeIndex :: Int,+    beDefect :: BuilderDefect+  }+  deriving stock (Eq, Show)+ -- | Close a 'PartialEdge' into an 'Edge'. Validation: 'peTargets'--- must have exactly one entry; missing or duplicated 'goto' calls--- raise a runtime 'error' naming the source vertex and edge index.+-- must have exactly one entry; missing or duplicated 'goto' calls are+-- returned structurally. A single-target edge must also declare output+-- intent with 'emit', 'emitWith', or 'noEmit'; otherwise finalization+-- returns 'DefectMissingOutputIntent'. 'buildTransducerEither' attaches location. -- The 'peOutput' list (zero or more 'OutTerm's accumulated by -- 'emit' / 'emitWith' calls) flows directly into the resulting -- 'Edge.output' field. finalizeEdge ::-  (Show v) =>-  Int ->-  v ->-  PartialEdge rs ci co v w ->-  Edge (HsPred rs ci) rs ci co v-finalizeEdge n src pe = case peTargets pe of-  [t] ->-    Edge-      { guard = peGuard pe,-        update = peUpdate pe,-        output = peOutput pe,-        target = t-      }-  [] ->-    error $-      "Keiki.Builder: edge #"-        <> show n-        <> " from "-        <> show src-        <> ": goto missing. Each onCmd/"-        <> "onEpsilon body must end with exactly one goto V."-  (_ : _ : _) ->-    error $-      "Keiki.Builder: edge #"-        <> show n-        <> " from "-        <> show src-        <> ": goto called more than once. "-        <> "Each onCmd/onEpsilon body must end with "-        <> "exactly one goto V."+  PartialEdge rs ci co v pin w ->+  Either BuilderDefect (Edge (HsPred rs ci) rs ci co v)+finalizeEdge pe = case peTargets pe of+  [t] -> case outputCtorMismatch (pePinned pe) (peOutput pe) of+    Just defect -> Left defect+    Nothing+      | not (peOutputDecided pe) -> Left DefectMissingOutputIntent+      | otherwise ->+          Right+            Edge+              { guard = peGuard pe,+                update = peUpdate pe,+                output = peOutput pe,+                target = t+              }+  [] -> Left DefectMissingGoto+  ts@(_ : _ : _) -> Left (DefectMultipleGoto (length ts)) +outputCtorMismatch :: Pinned ci pin -> [OutTerm rs ci co] -> Maybe BuilderDefect+outputCtorMismatch PinNone _ = Nothing+outputCtorMismatch (PinCtor pinned) outputs = go outputs+  where+    expectedName = icName pinned+    expectedSlots = slotNamesOf pinned++    go [] = Nothing+    go (OPack actual _ _ : rest)+      | icName actual /= expectedName || slotNamesOf actual /= expectedSlots =+          Just+            ( DefectOutputCtorMismatch+                expectedName+                expectedSlots+                (icName actual)+                (slotNamesOf actual)+            )+      | otherwise = go rest+ -- * Vertex builder --------------------------------------------------------  -- | Top-level builder. Accumulates @[(v, [Edge ...])]@ entries, one@@ -751,8 +785,8 @@ -- default for unmentioned vertices. newtype VertexBuilder rs ci co v a = VertexBuilder   { runVertexBuilder ::-      [(v, [Edge (HsPred rs ci) rs ci co v])] ->-      (a, [(v, [Edge (HsPred rs ci) rs ci co v])])+      [(v, [Either BuilderDefect (Edge (HsPred rs ci) rs ci co v)])] ->+      (a, [(v, [Either BuilderDefect (Edge (HsPred rs ci) rs ci co v)])])   }  instance Functor (VertexBuilder rs ci co v) where@@ -780,7 +814,6 @@ -- (terminal). To assert "this vertex is terminal" explicitly, -- write @from V (Prelude.pure ())@. from ::-  (Eq v, Show v) =>   v ->   EdgeListBuilder rs ci co v () ->   VertexBuilder rs ci co v ()@@ -799,24 +832,120 @@ -- returns the concatenation of every entry's edges in declaration -- order. ----- The @Bounded v@ / @Enum v@ constraints are not currently used by--- 'buildTransducer' itself but are recorded as reserved for a--- future @withCompletenessCheck@ combinator that would assert every--- vertex appears in some 'from' block.+-- Every declared edge is validated before the result is returned.+-- Forcing the returned transducer to weak head normal form therefore+-- reports malformed edges even when their source vertices are never+-- otherwise inspected. Use 'buildTransducerEither' for structured+-- diagnostics instead of an exception. buildTransducer ::   forall rs ci co v.-  (Bounded v, Enum v, Eq v, Show v) =>+  (DistinctNames (Names rs), Eq v, Show v) =>   v ->   RegFile rs ->   (v -> Bool) ->   VertexBuilder rs ci co v () ->   SymTransducer (HsPred rs ci) rs v ci co buildTransducer initS initR isF vb =-  SymTransducer-    { edgesOut = \v -> Prelude.concatMap snd (Prelude.filter ((== v) . fst) vmap),-      initial = initS,-      initialRegs = initR,-      isFinal = isF-    }+  case buildTransducerEither initS initR isF vb of+    Left errs -> error (renderBuilderErrors errs)+    Right tr -> tr++-- | Validating entry point. Runs the complete 'VertexBuilder', merges+-- duplicate vertices in declaration order, assigns stable per-vertex+-- edge indices, and returns every structural defect found.+buildTransducerEither ::+  forall rs ci co v.+  (DistinctNames (Names rs), Eq v) =>+  v ->+  RegFile rs ->+  (v -> Bool) ->+  VertexBuilder rs ci co v () ->+  Either+    (NonEmpty (BuilderError v))+    (SymTransducer (HsPred rs ci) rs v ci co)+buildTransducerEither initS initR isF vb =+  forceBuilderErrors errors `seq`+    forceEdgeTable cleanTable `seq`+      case NonEmpty.nonEmpty errors of+        Just errs -> Left errs+        Nothing ->+          Right+            SymTransducer+              { edgesOut = \v -> maybe [] id (lookup v cleanTable),+                initial = initS,+                initialRegs = initR,+                isFinal = isF+              }   where-    (_, vmap) = runVertexBuilder vb []+    (_, rawEntries) = runVertexBuilder vb []+    mergedEntries = foldl' mergeEntry [] (Prelude.reverse rawEntries)+    locatedEntries =+      [ (v, zipWith (locate v) [0 ..] results)+      | (v, results) <- mergedEntries+      ]+    errors =+      [ builderError+      | (_, results) <- locatedEntries,+        Left builderError <- results+      ]+    cleanTable =+      [ (v, [edge | Right edge <- results])+      | (v, results) <- locatedEntries+      ]++    mergeEntry acc (v, edges) =+      case break ((== v) . fst) acc of+        (_, []) -> acc ++ [(v, edges)]+        (before, (existingV, existingEdges) : after) ->+          before ++ (existingV, existingEdges ++ edges) : after++    locate v edgeIndex = \case+      Left defect -> Left (BuilderError v edgeIndex defect)+      Right edge -> Right edge++-- | Render structured builder errors in the historical message format.+-- Multiple errors are joined by newlines in declaration order.+renderBuilderErrors :: (Show v) => NonEmpty (BuilderError v) -> String+renderBuilderErrors = intercalate "\n" . fmap renderBuilderError . NonEmpty.toList++renderBuilderError :: (Show v) => BuilderError v -> String+renderBuilderError (BuilderError src n defect) =+  "Keiki.Builder: edge #"+    <> show n+    <> " from "+    <> show src+    <> case defect of+      DefectMissingGoto ->+        ": goto missing. Each onCmd/onEpsilon body must end with exactly one goto V."+      DefectMultipleGoto _ ->+        ": goto called more than once. Each onCmd/onEpsilon body must end with exactly one goto V."+      DefectOutputCtorMismatch expectedName expectedSlots actualName actualSlots ->+        ": emitWith InCtor "+          <> show actualName+          <> " (slots "+          <> renderSlotNames actualSlots+          <> ") contradicts the enclosing onCmd's InCtor "+          <> show expectedName+          <> " (slots "+          <> renderSlotNames expectedSlots+          <> "). An onCmd edge's outputs must pack the command constructor the edge matches on, or replay will invert the event to a different command."+      DefectMissingOutputIntent ->+        ": no emit or noEmit. Each onCmd/onEpsilon body must call 'emit' (or 'emitWith') to produce an event, or 'noEmit' to declare the edge deliberately silent (ε-edge)."++renderSlotNames :: [String] -> String+renderSlotNames names = "[" <> intercalate "," names <> "]"++forceBuilderErrors :: [BuilderError v] -> ()+forceBuilderErrors [] = ()+forceBuilderErrors (builderError : rest) = builderError `seq` forceBuilderErrors rest++forceEdgeTable :: [(v, [Edge p rs ci co v])] -> ()+forceEdgeTable [] = ()+forceEdgeTable ((_, edges) : rest) = forceEdges edges `seq` forceEdgeTable rest+  where+    forceEdges [] = ()+    forceEdges (edge : more) =+      edge `seq` forceOutputSpine (output edge) `seq` forceEdges more++    forceOutputSpine [] = ()+    forceOutputSpine (_ : outputs) = forceOutputSpine outputs

@@ -4,16 +4,27 @@ -- slot-name domains; the body uses raw 'UCombine' (decision logged -- in EP-18) so GHC sees the constraint as unused. Same reasoning as -- "Keiki.Core"'s 'combine'.-{-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# OPTIONS_GHC -Wno-partial-fields -Wno-redundant-constraints #-}  -- | Sequential composition of two 'SymTransducer's. ----- The single user-facing value is 'compose'. Given a transducer @t1@+-- Stability: experimental. The categorical representation may change before+-- its full law contract is resolved. For validated aggregate pipelines prefer+-- 'composeChecked'; 'compose' remains the unchecked construction primitive.+--+-- Given a transducer @t1@ -- whose output alphabet is @mid@ and a transducer @t2@ whose input -- alphabet is also @mid@, @compose t1 t2@ is the composite transducer -- whose input is t1's input, whose output is t2's output, whose -- vertex is the pair (wrapped in 'Composite' so 'Bounded'/'Enum' -- derive cleanly), and whose register file is @'Append' rs1 rs2@.+-- Update right-hand sides use the entry register snapshot. For a+-- multi-event t1 edge, path expansion symbolically threads each t2 write+-- into later t2 guards, updates, and outputs before collapsing the path.+-- A comparison leaf that reads a different mid constructor becomes+-- 'PBot'; mismatched reads in other positions become opaque poison terms+-- that structural validation and rendering can inspect safely and whose+-- values raise only if an unsatisfiable edge nevertheless demands them. -- -- See @docs/research/composition-combinators-design.md@ for the -- formal semantics, the substitution algorithm, the proof sketch@@ -30,6 +41,9 @@      -- * Sequential composition     compose,+    ComposeAlignmentWarning (..),+    checkComposeAlignment,+    composeChecked,      -- * Disjoint-input dispatch     alternative,@@ -48,6 +62,14 @@     weakenRUpdate,     weakenROutFields, +    -- * Slot-list witnesses+    SlotListWitness (..),+    KnownSlots (..),+    appendWitness,+    withKnownSlots,+    withDisjointNil,+    witnessNames,+     -- * Substitution (exposed for advanced uses)     substTerm,     substPred,@@ -84,6 +106,10 @@   ) where +import Data.List (isInfixOf, isSuffixOf, nub)+import Data.Set qualified as Set+import Data.Type.Equality ((:~:) (Refl))+import GHC.TypeLits (KnownSymbol) import Keiki.Core import Keiki.Generics (Append, appendRegFile) import NoThunks.Class (NoThunks (..), allNoThunks)@@ -96,7 +122,7 @@ -- instances on @(s1, s2)@ — those would conflict with downstream -- code. data Composite s1 s2 = Composite !s1 !s2-  deriving (Eq, Show)+  deriving (Eq, Ord, Show)  instance (Bounded s1, Bounded s2) => Bounded (Composite s1 s2) where   minBound = Composite minBound minBound@@ -158,6 +184,59 @@   weakenR i = SIdx (weakenR @rs1 i)   weakenRIndexN i = IS (weakenRIndexN @rs1 i) +-- * Slot-list witnesses ---------------------------------------------------++-- | Value-level singleton of a slot-list spine. 'WNil' mirrors @'[]@;+-- 'WCons' mirrors one cons cell, capturing the slot name's+-- 'KnownSymbol'. Packed by 'Keiki.Profunctor.SomeSymTransducer' at+-- wrap time (where @rs@ is concrete) so that instance dictionaries+-- for hidden slot lists can later be re-derived by structural+-- recursion instead of fabricated with @unsafeCoerce@.+data SlotListWitness (rs :: [Slot]) where+  WNil :: SlotListWitness '[]+  WCons :: (KnownSymbol s) => SlotListWitness rs -> SlotListWitness ('(s, t) ': rs)++-- | Conjure a 'SlotListWitness' for a concrete slot list. The+-- superclasses bundle the two structural classes every wrapper+-- consumer needs, so a packed @KnownSlots rs@ also supplies+-- 'WeakenR' and 'KnownSlotNames'.+class (WeakenR rs, KnownSlotNames rs) => KnownSlots (rs :: [Slot]) where+  slotWitness :: SlotListWitness rs++instance KnownSlots '[] where+  slotWitness = WNil++instance (KnownSymbol s, KnownSlots rs) => KnownSlots ('(s, t) ': rs) where+  slotWitness = WCons (slotWitness @rs)++-- | Append two witnesses. This is the value-level mirror of+-- 'Keiki.Generics.appendRegFile'; each equation matches one+-- 'Append' reduction step.+appendWitness ::+  SlotListWitness rs1 ->+  SlotListWitness rs2 ->+  SlotListWitness (Append rs1 rs2)+appendWitness WNil w2 = w2+appendWitness (WCons w1) w2 = WCons (appendWitness w1 w2)++-- | Discharge @KnownSlots rs@, and therefore 'WeakenR rs' and+-- 'KnownSlotNames rs', from a witness by induction on its spine.+withKnownSlots :: SlotListWitness rs -> ((KnownSlots rs) => r) -> r+withKnownSlots WNil k = k+withKnownSlots (WCons w) k = withKnownSlots w k++-- | Discharge @Disjoint (Names rs) '[]@: no slot name collides with+-- the empty list. This replaces the fabricated evidence formerly+-- used by 'Keiki.Profunctor.left''.+withDisjointNil :: SlotListWitness rs -> ((Disjoint (Names rs) '[]) => r) -> r+withDisjointNil WNil k = k+withDisjointNil (WCons w) k = withDisjointNil w k++-- | Return the names described by a witness, using the same induction+-- that re-derives the structural dictionaries.+witnessNames :: forall rs. SlotListWitness rs -> [String]+witnessNames w = withKnownSlots w (slotNames @rs)+ -- * weakenL: lift an Index over rs1 to (Append rs1 rs2) -------------------  -- | Lift a head-side 'Index' across an rs2 suffix. Walks the@@ -204,6 +283,8 @@     (weakenLTerm @rs1 @rs2 a)     (weakenLTerm @rs1 @rs2 b) weakenLPred (PInCtor ic) = PInCtor ic+weakenLPred PLeftArm = PLeftArm+weakenLPred PRightArm = PRightArm weakenLPred (PCmp op a b) =   PCmp     op@@ -277,6 +358,8 @@     (weakenRTerm @rs1 @rs2 a)     (weakenRTerm @rs1 @rs2 b) weakenRPred (PInCtor ic) = PInCtor ic+weakenRPred PLeftArm = PLeftArm+weakenRPred PRightArm = PRightArm weakenRPred (PCmp op a b) =   PCmp     op@@ -369,6 +452,27 @@   | n > 0 = nthTerm (n - 1) rest   | otherwise = Nothing +-- | A structurally inert term whose value raises only when demanded.+-- Structural walkers see an opaque 'TApp1' over a harmless literal, so a+-- constructor-mismatched composite edge cannot crash validation or rendering.+poisonTerm :: String -> Term rs ci ifs r+poisonTerm message = TApp1 (\() -> error message) (TLit ())++-- | Detect a field read for a constructor other than the mid constructor+-- produced by the t1 output currently being substituted.+termHasCtorMismatch :: String -> Term rs ci ifs r -> Bool+termHasCtorMismatch _ (TLit _) = False+termHasCtorMismatch _ (TReg _) = False+termHasCtorMismatch expected (TInpCtorField ic _) = icName ic /= expected+termHasCtorMismatch expected (TApp1 _ term) = termHasCtorMismatch expected term+termHasCtorMismatch expected (TArith _ a b) =+  termHasCtorMismatch expected a || termHasCtorMismatch expected b+termHasCtorMismatch expected (TApp2 _ a b) =+  termHasCtorMismatch expected a || termHasCtorMismatch expected b++outCtorName :: OutTerm rs ci co -> String+outCtorName (OPack _ wc _) = wcName wc+ -- | Substitute a t2-side 'Term' against t1's edge output. See the -- design note's "Substituting a Term" section for the rules. --@@ -399,7 +503,7 @@                   -- type and the input field schema.                   weakenLTerm @rs1 @rs2 (unsafeCoerceTerm tm)                 Nothing ->-                  error+                  poisonTerm                     ( "Keiki.Composition.compose: nthTerm overflow at\                       \ position "                         <> show n@@ -411,16 +515,14 @@                            \ mid type."                     )       | otherwise ->-          error-            ( "Keiki.Composition.compose: TInpCtorField over "+          poisonTerm+            ( "Keiki.Composition.compose: t2-side guard, update, or output reads "                 <> icName ic2-                <> " but t1's edge produced "+                <> " while t1's edge carries "                 <> wcName wc1-                <> " — caller should ensure structural alignment of mid's\-                   \ constructors. Substitution at this position is\-                   \ unsound; the composite edge guard's PInCtor\-                   \ substitution should make the edge unsatisfiable\-                   \ before evaluation reaches this term."+                <> ". This composite edge cannot supply that constructor field;\+                   \ its mismatched guard leaf should be unsatisfiable before\+                   \ the value is demanded."             ) substTerm (TApp1 f t) o1 = TApp1 f (substTerm @rs1 @rs2 t o1) substTerm (TArith op a b) o1 =@@ -463,20 +565,64 @@     (substPred @rs1 @rs2 q o1) substPred (PNot p) o1 = PNot (substPred @rs1 @rs2 p o1) substPred (PEq a b) o1 =-  PEq-    (substTerm @rs1 @rs2 a o1)-    (substTerm @rs1 @rs2 b o1)+  if termHasCtorMismatch (outCtorName o1) a+    || termHasCtorMismatch (outCtorName o1) b+    then PBot+    else+      PEq+        (substTerm @rs1 @rs2 a o1)+        (substTerm @rs1 @rs2 b o1) substPred (PCmp op a b) o1 =-  PCmp-    op-    (substTerm @rs1 @rs2 a o1)-    (substTerm @rs1 @rs2 b o1)+  if termHasCtorMismatch (outCtorName o1) a+    || termHasCtorMismatch (outCtorName o1) b+    then PBot+    else+      PCmp+        op+        (substTerm @rs1 @rs2 a o1)+        (substTerm @rs1 @rs2 b o1) substPred (PInCtor ic2) o1 =   case o1 of     OPack _ wc1 _       | icName ic2 == wcName wc1 -> PTop       | otherwise -> PBot+substPred PLeftArm o1 = substLeftArmPred @rs1 @rs2 o1+substPred PRightArm o1 = substRightArmPred @rs1 @rs2 o1 +-- | Preserve concrete arm tests when a sum-valued intermediate is+-- substituted away. The wire builder reconstructs the intermediate value+-- from a structural term for its fields; the resulting opaque term is exact+-- for forward evaluation (and conservatively opaque to the solver).+substLeftArmPred ::+  forall rs1 rs2 ci1 mid1 mid2.+  (WeakenR rs1) =>+  OutTerm rs1 ci1 (Either mid1 mid2) ->+  HsPred (Append rs1 rs2) ci1+substLeftArmPred (OPack _ wc fields) =+  PEq+    ( TApp1+        (\fs -> case wcBuild wc fs of Left _ -> True; Right _ -> False)+        (weakenLTerm @rs1 @rs2 (outFieldsAsTerm fields))+    )+    (TLit True)++substRightArmPred ::+  forall rs1 rs2 ci1 mid1 mid2.+  (WeakenR rs1) =>+  OutTerm rs1 ci1 (Either mid1 mid2) ->+  HsPred (Append rs1 rs2) ci1+substRightArmPred (OPack _ wc fields) =+  PEq+    ( TApp1+        (\fs -> case wcBuild wc fs of Left _ -> False; Right _ -> True)+        (weakenLTerm @rs1 @rs2 (outFieldsAsTerm fields))+    )+    (TLit True)++outFieldsAsTerm :: OutFields rs ci ifs fs -> Term rs ci ifs fs+outFieldsAsTerm OFNil = TLit ()+outFieldsAsTerm (OFCons term rest) = TApp2 (,) term (outFieldsAsTerm rest)+ -- | Substitute a t2-side 'Update' against t1's edge output. The -- slot-name index @w@ is preserved by substitution — substituting -- input reads inside the right-hand-side 'Term's does not change@@ -645,6 +791,8 @@     (liftLTermAlt @rs @ci1 @ci2 a)     (liftLTermAlt @rs @ci1 @ci2 b) liftLPredAlt (PInCtor ic) = PInCtor (leftInCtor ic)+liftLPredAlt PLeftArm = PInCtor (liftedArmInCtor "left" (\case Left value -> Just value; Right _ -> Nothing) True)+liftLPredAlt PRightArm = PInCtor (liftedArmInCtor "left" (\case Left value -> Just value; Right _ -> Nothing) False) liftLPredAlt (PCmp op a b) =   PCmp     op@@ -672,12 +820,29 @@     (liftRTermAlt @rs @ci1 @ci2 a)     (liftRTermAlt @rs @ci1 @ci2 b) liftRPredAlt (PInCtor ic) = PInCtor (rightInCtor ic)+liftRPredAlt PLeftArm = PInCtor (liftedArmInCtor "right" (\case Left _ -> Nothing; Right value -> Just value) True)+liftRPredAlt PRightArm = PInCtor (liftedArmInCtor "right" (\case Left _ -> Nothing; Right value -> Just value) False) liftRPredAlt (PCmp op a b) =   PCmp     op     (liftRTermAlt @rs @ci1 @ci2 a)     (liftRTermAlt @rs @ci1 @ci2 b) +liftedArmInCtor ::+  String ->+  (outer -> Maybe (Either inner1 inner2)) ->+  Bool ->+  InCtor outer '[]+liftedArmInCtor outerName project wantLeft =+  InCtor+    { icName = "keiki#" <> outerName <> "#" <> (if wantLeft then "leftArm#lmapped" else "rightArm#lmapped"),+      icMatch = \outer -> case project outer of+        Just (Left _) | wantLeft -> Just RNil+        Just (Right _) | not wantLeft -> Just RNil+        _ -> Nothing,+      icBuild = \_ -> error "Keiki.Composition: nested lifted arm predicates cannot rebuild inputs"+    }+ -- | Lift an 'Update' from the left side's input alphabet to -- @Either ci1 ci2@. The slot-name index @w@ is preserved; only the -- right-hand-side 'Term's are walked.@@ -829,6 +994,100 @@  -- * Multi-event composition (EP-19 M6) ----------------------------------- +-- | A symbolic write performed by an earlier t2 step in a multi-event+-- composition path. The value term has already been substituted into the+-- composite register/input domain. Its input-field schema is existential+-- because updates never expose that schema.+data PendingWrite rs ci where+  PendingWrite ::+    (KnownSymbol s) =>+    IndexN s rs r ->+    Term rs ci ifs r ->+    PendingWrite rs ci++-- | Compare a slot-name-tagged update index with a positional register+-- index. Equal positions refine the stored value types to equality.+matchIndex :: IndexN s rs a -> Index rs b -> Maybe (a :~: b)+matchIndex IZ ZIdx = Just Refl+matchIndex (IS i) (SIdx j) = matchIndex i j+matchIndex _ _ = Nothing++-- | Look up the most recent symbolic write to a register. The environment+-- is newest-first; 'unsafeCoerceTerm' only realigns the existential input+-- field schema, under the same justification used by 'substTerm'.+lookupPending ::+  Index rs r ->+  [PendingWrite rs ci] ->+  Maybe (Term rs ci ifs r)+lookupPending _ [] = Nothing+lookupPending ix (PendingWrite pendingIx pendingTerm : rest) =+  case matchIndex pendingIx ix of+    Just Refl -> Just (unsafeCoerceTerm pendingTerm)+    Nothing -> lookupPending ix rest++-- | Inline earlier t2 writes so a later chain step observes the symbolic+-- register state that sequential execution would have produced.+applyEnvTerm ::+  [PendingWrite rs ci] ->+  Term rs ci ifs r ->+  Term rs ci ifs r+applyEnvTerm _ (TLit r) = TLit r+applyEnvTerm env (TReg ix) = maybe (TReg ix) id (lookupPending ix env)+applyEnvTerm _ (TInpCtorField ic ix) = TInpCtorField ic ix+applyEnvTerm env (TApp1 f term) = TApp1 f (applyEnvTerm env term)+applyEnvTerm env (TArith op a b) =+  TArith op (applyEnvTerm env a) (applyEnvTerm env b)+applyEnvTerm env (TApp2 f a b) =+  TApp2 f (applyEnvTerm env a) (applyEnvTerm env b)++applyEnvPred ::+  [PendingWrite rs ci] ->+  HsPred rs ci ->+  HsPred rs ci+applyEnvPred _ PTop = PTop+applyEnvPred _ PBot = PBot+applyEnvPred env (PAnd a b) = PAnd (applyEnvPred env a) (applyEnvPred env b)+applyEnvPred env (POr a b) = POr (applyEnvPred env a) (applyEnvPred env b)+applyEnvPred env (PNot pred') = PNot (applyEnvPred env pred')+applyEnvPred env (PEq a b) = PEq (applyEnvTerm env a) (applyEnvTerm env b)+applyEnvPred env (PCmp op a b) =+  PCmp op (applyEnvTerm env a) (applyEnvTerm env b)+applyEnvPred _ (PInCtor ic) = PInCtor ic+applyEnvPred _ PLeftArm = PLeftArm+applyEnvPred _ PRightArm = PRightArm++applyEnvUpdate ::+  [PendingWrite rs ci] ->+  Update rs w ci ->+  Update rs w ci+applyEnvUpdate _ UKeep = UKeep+applyEnvUpdate env (USet ix term) = USet ix (applyEnvTerm env term)+applyEnvUpdate env (UCombine a b) =+  UCombine (applyEnvUpdate env a) (applyEnvUpdate env b)++applyEnvOutFields ::+  [PendingWrite rs ci] ->+  OutFields rs ci ifs fs ->+  OutFields rs ci ifs fs+applyEnvOutFields _ OFNil = OFNil+applyEnvOutFields env (OFCons term rest) =+  OFCons (applyEnvTerm env term) (applyEnvOutFields env rest)++applyEnvOut ::+  [PendingWrite rs ci] ->+  OutTerm rs ci co ->+  OutTerm rs ci co+applyEnvOut env (OPack ic wc fields) =+  OPack ic wc (applyEnvOutFields env fields)++-- | Collect one t2 step's writes newest-first. The right half is collected+-- before the left so an internal raw 'UCombine' that repeats a slot matches+-- 'runUpdate''s rightmost-write-wins application order.+pendingWrites :: Update rs w ci -> [PendingWrite rs ci]+pendingWrites UKeep = []+pendingWrites (USet ix term) = [PendingWrite ix term]+pendingWrites (UCombine a b) = pendingWrites b ++ pendingWrites a+ -- | An in-progress t2-edge path through a multi-event 'compose' -- expansion. Carries the accumulated guard (the lifted @e1@-guard -- conjoined with each consumed t2-edge's substituted guard), the@@ -845,10 +1104,243 @@       !(HsPred (Append rs1 rs2) ci1) -- accumulated guard       !(Update (Append rs1 rs2) w ci1) -- chained update (existential w)       ![OutTerm (Append rs1 rs2) ci1 co] -- accumulated outputs in order+      ![PendingWrite (Append rs1 rs2) ci1] -- earlier t2 writes, newest first       !s2 -- t2-state after consuming so far  -- * compose ---------------------------------------------------------------- +-- | A conservative structural fact discovered at a composition boundary.+-- The checker reports concrete name/position mismatches. Its reachability scan+-- is conservative, so exotic Boolean guards can produce warnings on a+-- semantically unreachable path or hide an expectation the structural walker+-- cannot expose. Every warning is a reviewable structural fact, but an empty+-- result is not a proof about arbitrary opaque guard logic.+data ComposeAlignmentWarning s1 s2+  = UnconsumedWireOutput+      { cawT1Edge :: EdgeRef s1,+        cawWireName :: String,+        cawT2Vertex :: s2+      }+  | UnmatchedInCtorExpectation+      { cawT2Edge :: EdgeRef s2,+        cawInCtorName :: String,+        cawT1Vertex :: s1+      }+  | FieldArityMismatch+      { cawT1EdgeA :: EdgeRef s1,+        cawT2EdgeA :: EdgeRef s2,+        cawSharedName :: String,+        cawReadPosition :: Int,+        cawAvailableFields :: Int+      }+  | PoisonedNameInComposition+      { cawName :: String,+        cawSide :: String+      }+  deriving stock (Eq, Show)++data EmittedName s = EmittedName+  { emittedEdge :: EdgeRef s,+    emittedName :: String,+    emittedArity :: Int+  }++data ExpectedName s = ExpectedName+  { expectedEdge :: EdgeRef s,+    expectedName :: String,+    expectedPosition :: Maybe Int+  }++outFieldsLength :: OutFields rs ci ifs fs -> Int+outFieldsLength OFNil = 0+outFieldsLength (OFCons _ rest) = 1 + outFieldsLength rest++edgeEmittedNames :: s -> Int -> Edge p rs ci co s -> [EmittedName s]+edgeEmittedNames source edgeIx edge =+  [ EmittedName+      { emittedEdge = EdgeRef source edgeIx,+        emittedName = wcName wc,+        emittedArity = outFieldsLength fields+      }+  | OPack _ wc fields <- output edge+  ]++termExpectedReads :: Term rs ci ifs r -> [(String, Int)]+termExpectedReads (TLit _) = []+termExpectedReads (TReg _) = []+termExpectedReads (TInpCtorField ic ix) = [(icName ic, indexInt ix)]+termExpectedReads (TApp1 _ term) = termExpectedReads term+termExpectedReads (TApp2 _ a b) = termExpectedReads a ++ termExpectedReads b+termExpectedReads (TArith _ a b) = termExpectedReads a ++ termExpectedReads b++predCtorAtoms :: HsPred rs ci -> [String]+predCtorAtoms PTop = []+predCtorAtoms PBot = []+predCtorAtoms (PAnd a b) = predCtorAtoms a ++ predCtorAtoms b+predCtorAtoms (POr a b) = predCtorAtoms a ++ predCtorAtoms b+predCtorAtoms (PNot pred') = predCtorAtoms pred'+predCtorAtoms (PEq _ _) = []+predCtorAtoms (PInCtor ic) = [icName ic]+predCtorAtoms PLeftArm = []+predCtorAtoms PRightArm = []+predCtorAtoms (PCmp _ _ _) = []++predExpectedReads :: HsPred rs ci -> [(String, Int)]+predExpectedReads PTop = []+predExpectedReads PBot = []+predExpectedReads (PAnd a b) = predExpectedReads a ++ predExpectedReads b+predExpectedReads (POr a b) = predExpectedReads a ++ predExpectedReads b+predExpectedReads (PNot pred') = predExpectedReads pred'+predExpectedReads (PEq a b) = termExpectedReads a ++ termExpectedReads b+predExpectedReads (PInCtor _) = []+predExpectedReads PLeftArm = []+predExpectedReads PRightArm = []+predExpectedReads (PCmp _ a b) = termExpectedReads a ++ termExpectedReads b++updateExpectedReads :: Update rs w ci -> [(String, Int)]+updateExpectedReads UKeep = []+updateExpectedReads (USet _ term) = termExpectedReads term+updateExpectedReads (UCombine a b) = updateExpectedReads a ++ updateExpectedReads b++outFieldsExpectedReads :: OutFields rs ci ifs fs -> [(String, Int)]+outFieldsExpectedReads OFNil = []+outFieldsExpectedReads (OFCons term rest) =+  termExpectedReads term ++ outFieldsExpectedReads rest++edgeExpectedNames :: s -> Int -> Edge (HsPred rs ci) rs ci co s -> [ExpectedName s]+edgeExpectedNames source edgeIx Edge {guard = edgeGuard, update = edgeUpdate, output = edgeOutput} =+  [ ExpectedName (EdgeRef source edgeIx) name Nothing+  | name <- predCtorAtoms edgeGuard+  ]+    ++ [ ExpectedName (EdgeRef source edgeIx) name (Just position)+       | (name, position) <-+           predExpectedReads edgeGuard+             ++ updateExpectedReads edgeUpdate+             ++ concatMap (\(OPack _ _ fields) -> outFieldsExpectedReads fields) edgeOutput+       ]++edgeConsumesName :: String -> Edge (HsPred rs ci) rs ci co s -> Bool+edgeConsumesName name edge =+  null atoms || name `elem` atoms+  where+    atoms = predCtorAtoms (guard edge)++isPoisonedBoundaryName :: String -> Bool+isPoisonedBoundaryName name =+  "#lmapped" `isInfixOf` name+    || "#rmapped" `isInfixOf` name+    || "_first" `isSuffixOf` name++-- | Check constructor-name and field-position alignment before building a+-- composite. Reachable vertex pairs are expanded from the two initial+-- vertices; multi-event outputs advance the downstream machine one symbol+-- at a time, matching 'compose''s path expansion conservatively.+checkComposeAlignment ::+  forall rs1 rs2 s1 s2 ci1 mid co.+  (Bounded s1, Enum s1, Ord s1, Bounded s2, Enum s2, Ord s2) =>+  SymTransducer (HsPred rs1 ci1) rs1 s1 ci1 mid ->+  SymTransducer (HsPred rs2 mid) rs2 s2 mid co ->+  [ComposeAlignmentWarning s1 s2]+checkComposeAlignment t1 t2 = nub (concatMap warningsAt reachablePairs)+  where+    reachablePairs = Set.toList (walk Set.empty [(initial t1, initial t2)])++    walk seen [] = seen+    walk seen (pair : rest)+      | pair `Set.member` seen = walk seen rest+      | otherwise =+          walk (Set.insert pair seen) (successors pair ++ rest)++    successors (v1, v2) =+      [ (target edge1, v2')+      | edge1 <- edgesOut t1 v1,+        v2' <- case output edge1 of+          [] -> [v2]+          mids -> advance v2 mids+      ]++    advance vertex [] = [vertex]+    advance vertex (OPack _ wc _ : rest) =+      [ end+      | edge2 <- edgesOut t2 vertex,+        edgeConsumesName (wcName wc) edge2,+        end <- advance (target edge2) rest+      ]++    warningsAt (v1, v2) =+      unconsumed ++ unmatched ++ arity ++ poison+      where+        t1Edges = zip [0 ..] (edgesOut t1 v1)+        t2Edges = zip [0 ..] (edgesOut t2 v2)+        emissions = concatMap (uncurry (edgeEmittedNames v1)) t1Edges+        expectations = concatMap (uncurry (edgeExpectedNames v2)) t2Edges+        emittedNames = map emittedName emissions+        expectedNames = map expectedName expectations++        unconsumed =+          [ UnconsumedWireOutput (emittedEdge emission) (emittedName emission) v2+          | emission <- emissions,+            not (any (edgeConsumesName (emittedName emission) . snd) t2Edges)+          ]++        unmatched =+          [ UnmatchedInCtorExpectation (expectedEdge expectation) name v1+          | expectation <- expectations,+            let name = expectedName expectation,+            name `notElem` emittedNames+          ]++        arity =+          [ FieldArityMismatch+              (emittedEdge emission)+              (expectedEdge expectation)+              name+              position+              (emittedArity emission)+          | emission <- emissions,+            expectation <- expectations,+            let name = expectedName expectation,+            emittedName emission == name,+            Just position <- [expectedPosition expectation],+            position >= emittedArity emission+          ]++        poison =+          [ PoisonedNameInComposition name side+          | (name, side) <-+              [(name, "upstream output") | name <- emittedNames]+                ++ [(name, "downstream input") | name <- expectedNames],+            isPoisonedBoundaryName name+          ]++-- | Checked entry point for validated aggregate pipelines. The unchecked+-- 'compose' primitive remains available for internal/experimental use.+composeChecked ::+  forall rs1 rs2 s1 s2 ci1 mid co.+  ( WeakenR rs1,+    Disjoint (Names rs1) (Names rs2),+    Bounded s1,+    Enum s1,+    Ord s1,+    Bounded s2,+    Enum s2,+    Ord s2+  ) =>+  SymTransducer (HsPred rs1 ci1) rs1 s1 ci1 mid ->+  SymTransducer (HsPred rs2 mid) rs2 s2 mid co ->+  Either+    [ComposeAlignmentWarning s1 s2]+    ( SymTransducer+        (HsPred (Append rs1 rs2) ci1)+        (Append rs1 rs2)+        (Composite s1 s2)+        ci1+        co+    )+composeChecked t1 t2 = case checkComposeAlignment t1 t2 of+  [] -> Right (compose t1 t2)+  warnings -> Left warnings+ -- | Sequential composition of two 'SymTransducer's. The composite -- consumes t1's input alphabet and produces t2's output alphabet, -- threading t1's events through t2 transparently.@@ -861,6 +1353,16 @@ --     t2 from @s2@: one composite edge whose guard / update / --     output are t2's structurally substituted against t1's edge --     output, conjoined with t1's lifted guard / update.+--   * For a multi-event t1 edge, every t2 path is expanded in event+--     order. Earlier t2 writes are substituted into later guards,+--     updates, and outputs, so the collapsed edge observes the same+--     register snapshots as sequential t2 stepping.+--   * All writes in the final edge evaluate their right-hand sides+--     against the edge-entry snapshot; internal repeated writes are+--     applied left-to-right, making the last chain step win.+--   * A constructor-mismatched comparison leaf is unsatisfiable+--     regardless of Boolean operand order. Other mismatched term+--     positions remain structurally inert and fail only if evaluated. -- -- The composite preserves the keiki guarantees: --   * Mechanical inversion: 'solveOutput' on the composite@@ -1001,6 +1503,7 @@           (weakenLPred @rs1 @rs2 (guard e1))           (weakenLUpdate @rs1 @rs2 u1)           []+          []           s2      -- \| Enumerate all t2-edge paths that consume the supplied@@ -1019,9 +1522,9 @@     expandPaths [] path = [path]     expandPaths (o : rest) path =       case path of-        PartialPath g u outs s2 ->+        PartialPath g u outs env s2 ->           concatMap-            (\e2 -> expandPaths rest (stepPath g u outs o s2 e2))+            (\e2 -> expandPaths rest (stepPath g u outs env o s2 e2))             (edgesOut t2 s2)      -- \| Extend a path by one t2-edge consuming one mid-symbol.@@ -1033,17 +1536,28 @@       HsPred (Append rs1 rs2) ci1 ->       Update (Append rs1 rs2) w ci1 ->       [OutTerm (Append rs1 rs2) ci1 co] ->+      [PendingWrite (Append rs1 rs2) ci1] ->       OutTerm rs1 ci1 mid ->       s2 ->       Edge (HsPred rs2 mid) rs2 mid co s2 ->       PartialPath rs1 rs2 ci1 co s2-    stepPath g u outs o _s2 e2 = case e2 of+    stepPath g u outs env o _s2 e2 = case e2 of       Edge {update = u2} ->-        PartialPath-          (PAnd g (substPred @rs1 @rs2 (guard e2) o))-          (UCombine u (substUpdate @rs1 @rs2 u2 o))-          (outs ++ map (\o2 -> substOut @rs1 @rs2 o2 o) (output e2))-          (target e2)+        let stepGuard =+              applyEnvPred env (substPred @rs1 @rs2 (guard e2) o)+            stepUpdate =+              applyEnvUpdate env (substUpdate @rs1 @rs2 u2 o)+            stepOutputs =+              map+                (applyEnvOut env . (\o2 -> substOut @rs1 @rs2 o2 o))+                (output e2)+            nextEnv = pendingWrites stepUpdate ++ env+         in PartialPath+              (PAnd g stepGuard)+              (UCombine u stepUpdate)+              (outs ++ stepOutputs)+              nextEnv+              (target e2)      -- \| Convert a fully-expanded path to a composite edge by     -- borrowing t1's @target@ for the composite's target.@@ -1056,7 +1570,7 @@         ci1         co         (Composite s1 s2)-    finalizePath e1 (PartialPath g u outs s2End) =+    finalizePath e1 (PartialPath g u outs _env s2End) =       Edge         { guard = g,           update = u,@@ -1096,14 +1610,12 @@ --     wrapping; symmetric for @Right@. --   * Hidden-input check: each side's per-edge check inherits via --     the lifters (which preserve 'TInpCtorField' slot reads).---   * Symbolic single-valuedness: at any @Composite s1 s2@, the t1---     edges' guards (which require @Left _@ via 'leftInCtor') and---     t2 edges' guards (which require @Right _@ via 'rightInCtor')---     are pairwise mutually exclusive. Within each arm,+--   * Symbolic single-valuedness: every lifted t1 guard is conjoined+--     with 'PLeftArm' and every lifted t2 guard with 'PRightArm'. The+--     concrete and symbolic interpretations make these independent arm+--     predicates disjoint even when the original guard was 'PTop'. Within each arm, --     single-valuedness reduces to the underlying sub-aggregate's---     check at the relevant sub-vertex. **No cross-transducer---     mutual-exclusion check is needed** — the @Either@ arms make---     it vacuous.+--     check at the relevant sub-vertex. -- -- See 'docs/research/composition-combinators-design.md' under -- "Combinators beyond `compose`" → "`alternative` — admitted" for@@ -1156,8 +1668,11 @@       Edge {update = u1} ->         Edge           { guard =-              liftLPredAlt @(Append rs1 rs2) @ci1 @ci2-                (weakenLPred @rs1 @rs2 (guard e1)),+              PAnd+                PLeftArm+                ( liftLPredAlt @(Append rs1 rs2) @ci1 @ci2+                    (weakenLPred @rs1 @rs2 (guard e1))+                ),             update =               liftLUpdateAlt @(Append rs1 rs2) @_ @ci1 @ci2                 (weakenLUpdate @rs1 @rs2 u1),@@ -1183,8 +1698,11 @@       Edge {update = u2} ->         Edge           { guard =-              liftRPredAlt @(Append rs1 rs2) @ci1 @ci2-                (weakenRPred @rs1 @rs2 (guard e2)),+              PAnd+                PRightArm+                ( liftRPredAlt @(Append rs1 rs2) @ci1 @ci2+                    (weakenRPred @rs1 @rs2 (guard e2))+                ),             update =               liftRUpdateAlt @(Append rs1 rs2) @_ @ci1 @ci2                 (weakenRUpdate @rs1 @rs2 u2),@@ -1199,8 +1717,8 @@  -- * feedback1 ------------------------------------------------------------ --- | Single-step feedback combinator. Models one round of an--- aggregate ↔ stateless-policy reaction: the aggregate consumes an+-- | Single-step two-copy cascade. It runs one round of an+-- aggregate-shaped transducer ↔ policy reaction: the first copy consumes an -- external command, the policy observes the aggregate's emitted -- event and emits a follow-up command, and the aggregate consumes -- that follow-up. The composite emits the aggregate's *second*@@ -1213,17 +1731,31 @@ --   * The outer @compose t _@ feeds t's first event into that --     inner pipeline. ----- The composite vertex is @Composite s1 (Composite s2 s1)@ —+-- This is /not shared-state aggregate feedback/. The composite vertex is+-- @Composite s1 (Composite s2 s1)@ — -- "outer t state, then (policy state, inner t state)". Even though -- the inner @s1@ is the same Haskell type as the outer, it occupies--- a distinct dimension of the composite vertex tuple, so+-- a distinct state dimension and (when admitted by the constraints) a+-- distinct register segment. The policy-produced command therefore updates+-- the inner copy, not the aggregate state that handled the external command.+-- The regression in @Keiki.CompositionFeedback1Spec@ distinguishes this from+-- shared feedback with a toggle. Consequently there is deliberately no+-- @feedback1Checked@: alignment cannot make two copies share state.+-- -- 'Keiki.Symbolic.isSingleValuedSym''s per-vertex enumeration walks+-- 'Keiki.Symbolic.isSingleValuedSym''s per-vertex enumeration walks -- all @|s1| * |s2| * |s1|@ combinations independently. -- -- Multi-round patterns are expressed by nesting: -- --     twoRounds = feedback1 (feedback1 t f) f --+-- This nested form requires both @rs1 ~ '[]@ and @rs2 ~ '[]@: the+-- outer call's slot-disjointness check ranges over the first result's+-- @Append rs1 (Append rs2 rs1)@ register file, so the policy must be+-- stateless as well as the aggregate. A single unnested call only forces+-- @rs1 ~ '[]@.+-- -- The pure-core boundary holds because there is no loop — the -- cascade runs exactly once per external command. --@@ -1242,10 +1774,10 @@ -- A "shared-state" variant — where the second t reads/writes the -- first t's registers via a custom edge construction — is -- documented as a future extension and is not in scope for MP-8.--- The "stateless policy" recommendation (single vertex, empty--- @rs2@) is convention rather than enforced; if violated, the--- composite still typechecks but the single-step semantics may--- not be preserved.+-- For one call, the "stateless policy" recommendation (single vertex,+-- empty @rs2@) is convention rather than enforced. Nesting the result in+-- another 'feedback1' does enforce empty @rs2@ through the next call's+-- 'Disjoint' constraint, as described above. -- -- == Future extensions --

@@ -2,1836 +2,2683 @@ -- sees it as unused (the body is @UCombine@) and would otherwise warn. -- Same reasoning for any future helpers that re-export the constraint -- as a typed witness.-{-# OPTIONS_GHC -Wno-redundant-constraints #-}---- | The pure core of keiki: the symbolic-register transducer.------ This module is the v1 prototype of the design pinned by--- @docs/research/dsl-shape-for-symbolic-register.md@ (the DSL note),--- @docs/research/effects-boundary.md@ (the boundary note), and--- @docs/research/synthesis-c-foundation-b-presentation-with-worked-examples.md@--- (the working baseline). See those notes for the rationale behind every--- shape declared here.------ All v1 escape hatches were retired by MasterPlan 6 (see the--- Outcomes section of--- @docs/masterplans/6-retire-remaining-v1-escape-hatches-in-pure-core-ofn-pmatchc-unsafecombine-static-check.md@):--- @TInpField@ / @OPack@'s hand-written inverse (MP-2 EP-1), 'OFn' /--- 'mkOut' (MP-6 EP-16), 'PMatchC' / 'matchCmd' (MP-6 EP-17), and--- 'unsafeCombine' (MP-6 EP-18, replaced by the static 'Disjoint'--- check on 'combine').------ == Guard-authoring operators (EP-45)------ Predicates and term arithmetic can be written with infix operators--- that mirror their Prelude counterparts:------   * Relational (build 'HsPred', @infix 4@): '.<' '.<=' '.>' '.>='---     '.==' './=' — each an alias for 'PCmp'/'PEq' at a fixed relation.---   * Logical (combine 'HsPred'): '.&&' (@infixr 3@, 'PAnd'),---     '.||' (@infixr 2@, 'POr'), 'pnot' ('PNot').---   * Arithmetic (build 'Term', mirror @+@\/@-@\/@*@): '.+' '.-' '.*' —---     aliases for 'tadd'\/'tsub'\/'tmul'.------ The verbose carrier signatures have synonyms: 'Pred' @rs ci@ for--- @'HsPred' rs ci@, 'Guarded' @rs s ci co@ for--- @'SymTransducer' ('HsPred' rs ci) rs s ci co@ (and--- 'Keiki.Symbolic.SymGuarded' for the SBV-backed carrier).------ Keep spaces around the operators (@lit a .* lit b@); a dot touching an--- identifier (@x.y@) is OverloadedRecordDot field access. If you import--- "Data.SBV" alongside this module, import it qualified — SBV exports--- the same operator names.-module Keiki.Core-  ( -- * Slots and the register file-    Slot,-    RegFile (..),-    Index (..),-    (!),--    -- * Index resolution from labels-    HasIndex (..),--    -- * Term language-    Term (..),-    NumOp (..),--    -- * Input-side structural constructor (v2)-    InCtor (..),-    AssembleRegFile,-    KnownSlotNames (..),--    -- * Slot-name machinery (re-exported from "Keiki.Internal.Slots")-    IndexN (..),-    HasIndexN (..),-    Disjoint,-    Concat,-    Names,--    -- * Update language-    Update (..),-    combine,--    -- * Output term language-    WireCtor (..),-    OutFields (..),-    (*:),-    oNil,-    OutTerm (..),--    -- * Predicate carrier (v1 first-class AST)-    HsPred (..),-    Pred,-    Cmp (..),--    -- * Effective Boolean algebra-    BoolAlg (..),-    Sat (..),--    -- * Edges and the transducer-    Edge (..),-    SymTransducer (..),-    Guarded,-    applyEdgeUpdate,-    edgeReadsInput,--    -- * Helpers (the user-facing DSL surface)-    matchInCtor,-    proj,-    inpCtor,-    lit,-    tadd,-    tsub,-    tmul,-    (.==),-    (.<),-    (.<=),-    (.>),-    (.>=),-    (./=),-    (.&&),-    (.||),-    pnot,-    (.+),-    (.-),-    (.*),-    pack,--    -- * Evaluators-    evalTerm,-    evalOut,-    evalPred,-    runUpdate,-    delta,-    omega,--    -- * Pure-layer entry points (effects-boundary note)-    step,-    stepEither,-    StepFailure (..),-    EdgeRef (..),-    RejectedEdgeSummary (..),-    MatchedEdgeSummary (..),-    reconstitute,-    applyEvent,-    applyEventStreaming,-    applyEvents,--    -- * Streaming-replay state wrapper (EP-19 M3)-    InFlight (..),--    -- * Build-time analyses-    solveOutput,-    HiddenInputWarning (..),-    checkHiddenInputs,--    -- * Build-time validation umbrella (EP-56)-    TransducerValidationWarning (..),-    ValidationOptions (..),-    defaultValidationOptions,-    validateTransducer,-    hiddenInputWarnings,-    opaqueGuardWarnings,-    DeterminismWarning (..),-    checkTransitionDeterminism,-    checkTransitionDeterminismPure,-    DeadEdgeOptions (..),-    defaultDeadEdgeOptions,-    DeadEdgeWarning (..),-    checkDeadEdges,--    -- * Internals exposed for testing-    termReadsInput,-    updateReadsInput,-    outFieldsHaveInpCtorField,-    detectMissingInCtorFields,-    MissingInCtorFields (..),-  )-where--import Data.Kind (Type)-import Data.List (nub, (\\))-import Data.Proxy (Proxy (..))-import Data.Set qualified as Set-import Data.Typeable (Typeable)-import GHC.OverloadedLabels (IsLabel (..))-import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)-import Keiki.Internal.Slots-  ( Concat,-    Disjoint,-    HasIndexN (..),-    IndexN (..),-    Names,-  )---- | A register slot is a label paired with the type of its value.-type Slot = (Symbol, Type)---- * Register file --------------------------------------------------------------- | A typed heterogeneous register tuple indexed by a list of 'Slot's.------ The slot-value field is intentionally lazy: 'Keiki.Generics.emptyRegFile'--- seeds each slot with a deferred @error "uninit: \<slot\>"@ thunk so--- that reading an unwritten slot fails loudly with a targeted message--- instead of returning a silent bottom. Strictness for *written*--- slots is enforced on the write path ('setSlotN') instead — see--- EP-23's Surprises entry for the long-running-service rationale.-data RegFile (rs :: [Slot]) where-  RNil :: RegFile '[]-  RCons ::-    (KnownSymbol s) =>-    Proxy s -> r -> RegFile rs -> RegFile ('(s, r) ': rs)---- | A type-safe pointer into a 'RegFile'. 'ZIdx' picks the head;--- 'SIdx' skips one slot.-data Index (rs :: [Slot]) (r :: Type) where-  ZIdx :: (KnownSymbol s) => Index ('(s, r) ': rs) r-  SIdx :: Index rs r -> Index ('(s', r') ': rs) r---- | Runtime register lookup. Matching on 'Index' first lets GHC's GADT--- pattern checker see that 'RNil' is unreachable — 'ZIdx' and 'SIdx'--- both refine @rs@ to @'(_,_) ': _@.-(!) :: RegFile rs -> Index rs r -> r-regs ! ZIdx = case regs of RCons _ x _ -> x-regs ! SIdx i = case regs of RCons _ _ rest -> rest ! i--infixl 9 !---- * IsLabel / HasIndex --------------------------------------------------------- | Resolve a label @s@ against a slot list @rs@ to an 'Index' for the--- value at that slot. The functional dependency @s rs -> r@ ensures that--- a label uniquely determines the slot's type.-class-  HasIndex (s :: Symbol) (rs :: [Slot]) (r :: Type)-    | s rs -> r-  where-  indexOf :: Index rs r--instance-  {-# OVERLAPPING #-}-  (KnownSymbol s) =>-  HasIndex s ('(s, r) ': rs) r-  where-  indexOf = ZIdx--instance-  {-# OVERLAPPABLE #-}-  forall s s' r r' rs.-  (HasIndex s rs r) =>-  HasIndex s ('(s', r') ': rs) r-  where-  indexOf = SIdx (indexOf @s @rs @r)--instance-  forall s rs r.-  (HasIndex s rs r) =>-  IsLabel s (Index rs r)-  where-  fromLabel = indexOf @s @rs @r---- | Resolve a label directly to a 'Term' that reads the named register.--- This instance lets call sites write @#name@ in any 'Term'-typed--- context (the arguments of 'requireEq', the elements of 'OutFields',--- etc.) without the @proj (#name :: Index Regs T)@ annotation that--- 'IsLabel s (Index rs r)' alone would require.------ The two 'IsLabel' instances ('Index' and 'Term') coexist because GHC--- dispatches by the expected result type: a context expecting an--- 'Index' (e.g. 'inpFoo'\'s argument) selects the 'Index' instance; a--- context expecting a 'Term' (e.g. 'requireEq'\'s arguments) selects--- this one.-instance-  forall s rs ci ifs r.-  (HasIndex s rs r) =>-  IsLabel s (Term rs ci ifs r)-  where-  fromLabel = TReg (indexOf @s @rs @r)---- The @IsLabel s (IndexN s rs r)@ instance lives next to 'IndexN' in--- "Keiki.Internal.Slots" so the orphan check is satisfied.---- * Term language -------------------------------------------------------------- | A numeric operation carried by 'TArith'. @OpAdd@\/@OpSub@\/@OpMul@--- are @+@\/@-@\/@*@ respectively. Kept as a single tag (rather than--- three 'Term' constructors) so each total 'Term' walker switches on--- one value; the three directions are recovered by the smart--- constructors 'tadd'\/'tsub'\/'tmul'.-data NumOp = OpAdd | OpSub | OpMul-  deriving stock (Eq, Show)---- | A pure expression over the register file and the input symbol,--- yielding a value of type @r@.------ The @ifs :: [Slot]@ parameter is the /input field schema/ this term--- may project from: it is pinned by 'TInpCtorField' (whose 'Index' is--- into @ifs@) and left free by terms that do not read an input field--- ('TLit', 'TReg'). Threading @ifs@ through the AST is what lets an--- 'OutFields' (and hence an 'OPack') guarantee /by construction/ that--- every top-level input projection reads the same constructor schema as--- the 'OPack''s 'InCtor' — so 'solveOutput' recovers a command field--- with no @unsafeCoerce@. Terms that do not appear in an invertible--- output position ('Update' right-hand sides, 'HsPred' operands)--- existentially hide @ifs@, so it never leaks into the 'Edge' /--- 'SymTransducer' surface. See @docs/research/tinpproj-design.md@.-data Term (rs :: [Slot]) (ci :: Type) (ifs :: [Slot]) (r :: Type) where-  TLit :: r -> Term rs ci ifs r-  TReg :: Index rs r -> Term rs ci ifs r-  -- | Structural input projection: read field @ix@ of the input-  --     constructor described by @ic@. The 'InCtor' value names the-  --     expected constructor and supplies the round-trip-  --     ('icMatch'/'icBuild') so that 'solveOutput' can mechanically-  --     recover @ci@ from an observed output. Pins the term's @ifs@ to the-  --     constructor's field schema. See @docs/research/tinpproj-design.md@.-  TInpCtorField :: InCtor ci ifs -> Index ifs r -> Term rs ci ifs r-  TApp1 ::-    (a -> r) ->-    Term rs ci ifs a ->-    Term rs ci ifs r-  TApp2 ::-    (a -> b -> r) ->-    Term rs ci ifs a ->-    Term rs ci ifs b ->-    Term rs ci ifs r-  -- | Structural arithmetic over a numeric operand type. Unlike the-  --     opaque 'TApp1'\/'TApp2' escape hatches, the SBV translator reads-  --     'TArith' for real (on a 'Keiki.Symbolic.discoverSymNum' hit), so a-  --     guard over a /computed/ value — a weighted sum, a derived cap — is-  --     visible to the solver. The 'Num' constraint prevents constructing-  --     arithmetic at non-numeric operand types; 'Typeable' lets the SBV-  --     translator dispatch on @r@. Build with 'tadd'\/'tsub'\/'tmul'.-  TArith ::-    (Num r, Typeable r) =>-    NumOp ->-    Term rs ci ifs r ->-    Term rs ci ifs r ->-    Term rs ci ifs r---- | Per-constructor input projection. An 'InCtor' value names one--- constructor of the input symbol type @ci@ and pins the round-trip--- between that constructor's payload and a typed register file--- @'RegFile' ifs@. The slot list @ifs@ is the field schema for the--- constructor; together with 'Index' it lets call sites read fields--- via 'OverloadedLabels' (for example @inpStart #email@).------ 'icMatch' must return 'Just' iff @ci@ is the named constructor.--- 'icBuild' is its left inverse: @icMatch (icBuild rf) == Just rf@ for--- every well-formed @rf@.------ The constraints 'AssembleRegFile' and 'KnownSlotNames' on the data--- constructor mean that any code holding an 'InCtor' can both--- mechanically rebuild a 'RegFile' from a bag of '(Index, value)' pairs--- and recover the slot names of @ifs@ at run time. The instances are--- automatic for any concrete slot list, so users do not write any--- additional code.------ See @docs/research/tinpproj-design.md@ for the design rationale and--- the inversion algorithm that walks 'OutFields' gathering these--- per-field reads.-data InCtor ci (ifs :: [Slot]) where-  InCtor ::-    (AssembleRegFile ifs, KnownSlotNames ifs) =>-    { icName :: String,-      icMatch :: ci -> Maybe (RegFile ifs),-      icBuild :: RegFile ifs -> ci-    } ->-    InCtor ci ifs---- * Slot-list helper classes (v2 inversion machinery) ------------------------- | Recover the slot names of an @ifs :: [Slot]@ at run time. Used to--- print precise hidden-input warnings.-class KnownSlotNames (rs :: [Slot]) where-  slotNames :: [String]--instance KnownSlotNames '[] where-  slotNames = []--instance-  (KnownSymbol s, KnownSlotNames rs) =>-  KnownSlotNames ('(s, r) ': rs)-  where-  slotNames = symbolVal (Proxy @s) : slotNames @rs---- | An (Index, value) pair indexed by an InCtor's slot list. Using a--- GADT existential lets us bag entries with different element types--- under one slot list and unpack them safely via pattern matching on--- the carried 'Index'.-data ByIndex (ifs :: [Slot]) where-  ByIndex :: Index ifs r -> r -> ByIndex ifs---- | Class to assemble a 'RegFile' from a bag of '(Index, value)' pairs.--- 'assemble' returns 'Just' iff every slot of @ifs@ is covered by--- exactly one entry of the bag (extra entries beyond what slots--- demand are ignored as long as the per-slot lookups succeed in--- order).-class AssembleRegFile (ifs :: [Slot]) where-  assemble :: [ByIndex ifs] -> Maybe (RegFile ifs)--instance AssembleRegFile '[] where-  assemble _ = Just RNil--instance-  (KnownSymbol s, AssembleRegFile rs) =>-  AssembleRegFile ('(s, r) ': rs)-  where-  assemble entries = do-    v <- findHead entries-    rest <- assemble (popHead entries)-    pure (RCons (Proxy @s) v rest)-    where-      findHead :: [ByIndex ('(s, r) ': rs)] -> Maybe r-      findHead [] = Nothing-      findHead (ByIndex ZIdx v : _) = Just v-      findHead (_ : rest) = findHead rest--      popHead :: [ByIndex ('(s, r) ': rs)] -> [ByIndex rs]-      popHead [] = []-      popHead (ByIndex ZIdx _ : rest) = popHead rest-      popHead (ByIndex (SIdx i) v : rest) = ByIndex i v : popHead rest---- * Update language ------------------------------------------------------------ | The copyless update language. The @(w :: [Symbol])@ index--- records the set of slot names this update writes; the smart--- constructor 'combine' demands @'Disjoint' w1 w2@ to combine two--- updates, so "each register is written at most once per edge--- update" becomes a type-level invariant rather than a runtime check.------ The 'UCombine' raw constructor is *not* constrained by 'Disjoint':--- the invariant is enforced at the smart-constructor introduction--- point ('combine'). This keeps internal pattern-matches in--- "Keiki.Composition" (which reconstruct 'UCombine' values during--- weakening / substitution) cheap. EP-18 M8 retired the v1--- 'unsafeCombine' escape hatch; aggregate authors use 'combine'--- exclusively.-data Update (rs :: [Slot]) (w :: [Symbol]) (ci :: Type) where-  UKeep :: Update rs '[] ci-  -- The right-hand-side 'Term''s input field schema @ifs@ is-  -- existentially hidden: updates are never inverted, so @ifs@ need not-  -- escape into the 'Update' kind (keeping 'Edge' / 'SymTransducer'-  -- unchanged).-  USet ::-    (KnownSymbol s) =>-    IndexN s rs r -> Term rs ci ifs r -> Update rs '[s] ci-  UCombine ::-    Update rs w1 ci ->-    Update rs w2 ci ->-    Update rs (Concat w1 w2) ci---- | Smart constructor for 'UCombine'. The @'Disjoint' w1 w2@--- constraint statically enforces that the two halves write to--- disjoint slot-name sets; an aggregate that writes the same slot--- twice (e.g. @'USet' #email t1 \`combine\` 'USet' #email t2@) is--- rejected at compile time with a 'GHC.TypeError.TypeError' naming--- the offending slot.-combine ::-  (Disjoint w1 w2) =>-  Update rs w1 ci ->-  Update rs w2 ci ->-  Update rs (Concat w1 w2) ci-combine = UCombine---- * Output term language ------------------------------------------------------- | A wire-type tag for one constructor of the user's output sum @co@.--- The functions let 'solveOutput' pattern-match an observed @co@ and--- 'evalOut' rebuild a @co@ from its fields.-data WireCtor co fields = WireCtor-  { wcName :: String,-    wcMatch :: co -> Maybe fields,-    wcBuild :: fields -> co-  }---- | An HList of 'Term's, one per field of the wire constructor. The--- field-tuple type @fs@ is built up nested-pair style so that--- 'solveOutput' can walk the HList structurally.------ The @ifs :: [Slot]@ parameter is the shared input field schema of--- every 'Term' in the list (see 'Term'). 'OPack' ties it to the--- 'OPack''s 'InCtor', so a top-level 'TInpCtorField' inside an--- 'OutFields' is statically an 'Index' into the 'OPack''s constructor--- schema — 'gatherInpEntries' recovers it with no coercion.-data OutFields rs ci ifs fs where-  OFNil :: OutFields rs ci ifs ()-  OFCons ::-    Term rs ci ifs f ->-    OutFields rs ci ifs fs ->-    OutFields rs ci ifs (f, fs)---- | Right-associative HList constructor synonym for 'OFCons'. Lets--- 'OutFields' literals read top-to-bottom in the wire ctor's field--- order:------ > d.recipient *: d.subject *: d.at *: oNil------ Identical AST: @t1 *: t2 *: oNil@ produces the same 'OutFields'--- value as @OFCons t1 (OFCons t2 OFNil)@. Available at the AST--- layer (here) so authors who skip the builder can use it; also--- re-exported by "Keiki.Builder" for builder-form call sites.-(*:) :: Term rs ci ifs f -> OutFields rs ci ifs fs -> OutFields rs ci ifs (f, fs)-(*:) = OFCons--infixr 5 *:---- | The empty 'OutFields' HList. Synonym for 'OFNil'.-oNil :: OutFields rs ci ifs ()-oNil = OFNil---- | A pure expression yielding an output value @co@.-data OutTerm (rs :: [Slot]) (ci :: Type) (co :: Type) where-  -- | Structural pack: tagged by an input constructor (which the edge-  --     consumes) and an output wire constructor (which the edge produces),-  --     with one 'Term' per field of the wire constructor. 'solveOutput'-  --     walks the structural 'OutFields', gathering '(Index, value)' pairs-  --     against the named 'InCtor', and reconstructs the input by calling-  --     'icBuild' on the assembled register file. Empty-payload input-  --     constructors (the 'InCtor's slot list is @\'[]@) recover trivially-  --     as @icBuild ic RNil@.-  OPack ::-    InCtor ci ifs ->-    WireCtor co fields ->-    OutFields rs ci ifs fields ->-    OutTerm rs ci co---- * Predicate carrier ---------------------------------------------------------- | The predicate AST. Carries enough structure to evaluate guards and--- to translate to SMT through the SBV-backed 'BoolAlg' instance in--- "Keiki.Symbolic" (added in EP-2 of MasterPlan 2).-data HsPred (rs :: [Slot]) (ci :: Type) where-  PTop :: HsPred rs ci-  PBot :: HsPred rs ci-  PAnd :: HsPred rs ci -> HsPred rs ci -> HsPred rs ci-  POr :: HsPred rs ci -> HsPred rs ci -> HsPred rs ci-  PNot :: HsPred rs ci -> HsPred rs ci-  PEq ::-    (Eq r, Typeable r) =>-    Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci-  -- | Structural input-constructor guard: @True@ iff the input symbol-  --     is the constructor named by the carried 'InCtor'. The SBV-backed-  --     'BoolAlg' instance recognises constructor mutual exclusion-  --     symbolically through this constructor. See-  --     @docs/research/sbv-boolalg-design.md@.-  PInCtor :: InCtor ci ifs -> HsPred rs ci-  -- | Ordering guard: compares two 'Term's of the same orderable type-  --     with the relation named by 'Cmp'. @PCmp CmpGe a b@ means @a >= b@,-  --     and so on. Unlike a threshold written through 'TApp1'\/'TApp2'-  --     (which is opaque to the solver), 'PCmp' is /structural/: the-  --     SBV-backed translator in "Keiki.Symbolic" emits a real symbolic-  --     comparison (@.<@, @.<=@, @.>@, @.>=@) whenever the operand type's-  --     'Keiki.Symbolic.SymRep' is symbolically orderable (see-  --     'Keiki.Symbolic.discoverSymOrd'); otherwise it falls back to a-  --     fresh opaque 'SBool', exactly as 'PEq' does for non-'Sym' operands.-  --     Equality is intentionally left to 'PEq' — 'Cmp' has no "equal"-  --     case. Added by EP-41.-  PCmp ::-    (Ord r, Typeable r) =>-    Cmp -> Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci---- | A four-way ordering relation carried by 'PCmp'. @Lt@\/@Le@\/@Gt@\/--- @Ge@ are @<@\/@<=@\/@>@\/@>=@ respectively. Kept as a single tag--- (rather than four 'HsPred' constructors) so the evaluator and the--- SBV translator each switch on one value; the four directions are--- recovered by the builder conveniences--- 'Keiki.Builder.requireLt'\/'requireLe'\/'requireGt'\/'requireGe'.-data Cmp = CmpLt | CmpLe | CmpGt | CmpGe-  deriving stock (Eq, Show)---- * Effective Boolean algebra -------------------------------------------------- | An effective Boolean algebra over @a@-typed witnesses, used as the--- guard carrier of edges. Witness /extraction/ ('sat') is a separate,--- stronger capability — see 'Sat'.-class BoolAlg phi a | phi -> a where-  top :: phi-  bot :: phi-  conj :: phi -> phi -> phi-  disj :: phi -> phi -> phi-  neg :: phi -> phi-  models :: phi -> a -> Bool-  isBot :: phi -> Bool---- | A 'BoolAlg' whose witnesses can be /extracted/ from a satisfiable--- predicate: @'sat' phi@ returns 'Just' a value satisfying @phi@, or--- 'Nothing' when @phi@ is unsatisfiable.------ Split out of 'BoolAlg' by EP-44 (MasterPlan 12). Witness--- reconstruction needs carrier-specific evidence — for the SBV-backed--- 'Keiki.Symbolic.SymPred' carrier, @ExtractRegFile rs@ (to rebuild the--- register file from the solver model) and @KnownInCtors ci@ (to rebuild--- the command) — that the algebra's build/decide methods do not. Keeping--- 'sat' in its own class means the witness-free analyses--- ('Keiki.Symbolic.isSingleValuedSym', which uses only 'isBot'/'conj')--- carry no extraction constraints, so they keep type-checking on--- register-file-existential carriers (e.g. 'Keiki.Profunctor.SomeSymTransducer')--- and on composition-produced @ci@ types ('Either', tuples) that have no--- 'KnownInCtors'. See @docs/research/sbv-boolalg-design.md@.-class (BoolAlg phi a) => Sat phi a where-  sat :: phi -> Maybe a--instance BoolAlg (HsPred rs ci) (RegFile rs, ci) where-  top = PTop-  bot = PBot-  conj p q = PAnd p q-  disj p q = POr p q-  neg p = PNot p-  models p (regs, ci) = evalPred p regs ci-  isBot PBot = True-  isBot _ = False---- | The v1 syntactic carrier has no solver, hence no extractable--- witness; 'sat' is always 'Nothing'. The precise witnesses come from--- the SBV-backed @Sat (SymPred …)@ instance in "Keiki.Symbolic".-instance Sat (HsPred rs ci) (RegFile rs, ci) where-  sat _ = Nothing---- * Edges and the transducer --------------------------------------------------- | A single transition. The 'output' is a list of 'OutTerm's:--- @[]@ is the ε-edge (no observable emission), @[o]@ is the letter--- edge (one event, identical to today's @'Just' o@), @[o1, o2, ...]@--- is the multi-event edge — one transition emits N events in--- declaration order. See @docs/research/gsm-widening-design.md@.------ The @(w :: [Symbol])@ index on 'update' (the slot-name set the--- update writes) is *existentially* quantified at the 'Edge' record--- — different edges out of the same vertex write different slot--- sets, but the homogeneous list @[Edge phi rs ci co s]@ in--- 'edgesOut' demands a single @Edge@ type. The existential preserves--- the static disjointness check at the *introduction* point of any--- 'Update' value (via 'combine') without polluting the @Edge@'s--- public type with a per-edge @w@ parameter.-data Edge phi rs ci co s where-  Edge ::-    { guard :: phi,-      update :: Update rs w ci,-      output :: [OutTerm rs ci co],-      target :: s-    } ->-    Edge phi rs ci co s---- | The single source of truth: a finite control graph plus a register--- file evolved by edges' 'update' terms.-data SymTransducer phi rs s ci co = SymTransducer-  { edgesOut :: s -> [Edge phi rs ci co s],-    initial :: s,-    initialRegs :: RegFile rs,-    isFinal :: s -> Bool-  }---- | Readable alias for the v1 predicate carrier:--- @'Pred' rs ci@ is exactly @'HsPred' rs ci@.-type Pred rs ci = HsPred rs ci---- | A 'SymTransducer' whose guard carrier is the v1 'HsPred'. Collapses--- the @'SymTransducer' ('HsPred' rs ci) rs s ci co@ signature — which--- otherwise repeats @rs@ and @ci@ — into @'Guarded' rs s ci co@.-type Guarded rs s ci co = SymTransducer (HsPred rs ci) rs s ci co---- | Apply an edge's update to the register file. The 'Edge''s--- existentially-quantified @w@ index makes @'update' e@ unusable as--- a function (GHC rejects with "escaped type variables"); this--- helper hides the existential by pattern-matching internally.-applyEdgeUpdate ::-  Edge phi rs ci co s -> RegFile rs -> ci -> RegFile rs-applyEdgeUpdate Edge {update = u} regs ci = runUpdate u regs ci---- | Does an edge's update read the input symbol via 'TInpCtorField'?--- Existential-hiding companion to 'updateReadsInput'.-edgeReadsInput :: Edge phi rs ci co s -> Bool-edgeReadsInput Edge {update = u} = updateReadsInput u---- * Helpers (DSL surface) ------------------------------------------------------ | Structural input-constructor guard: @True@ iff the input symbol--- is the constructor named by the supplied 'InCtor'. The SBV-backed--- 'BoolAlg' instance can decide constructor-mutual-exclusion--- symbolically through this guard. The semantics is--- @evalPred (matchInCtor ic) regs ci == isJust (icMatch ic ci)@.-matchInCtor :: InCtor ci ifs -> HsPred rs ci-matchInCtor = PInCtor---- | Read a register slot into a 'Term'.-proj :: Index rs r -> Term rs ci ifs r-proj = TReg---- | Structural input projection: read field @ix@ of the input--- constructor described by @ic@. The result 'Term''s @ifs@ is the--- constructor's field schema, so an 'OutFields' built from these is--- statically tied to the 'OPack''s 'InCtor'.-inpCtor :: InCtor ci ifs -> Index ifs r -> Term rs ci ifs r-inpCtor = TInpCtorField---- | A constant 'Term'.-lit :: r -> Term rs ci ifs r-lit = TLit---- | Structural arithmetic smart constructors. @tadd@\/@tsub@\/@tmul@--- build a 'TArith' over @+@\/@-@\/@*@. The operand type must be numeric--- ('Num') and 'Typeable'; the SBV translator reads them structurally--- (see 'Keiki.Symbolic.discoverSymNum'), unlike the opaque 'TApp'--- escape hatches.-tadd,-  tsub,-  tmul ::-    (Num r, Typeable r) =>-    Term rs ci ifs r -> Term rs ci ifs r -> Term rs ci ifs r-tadd = TArith OpAdd-tsub = TArith OpSub-tmul = TArith OpMul---- | Equality predicate sugar.-(.==) :: (Eq r, Typeable r) => Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci-(.==) = PEq--infix 4 .==---- * Predicate & term operators (readable guard DSL) -------------------------- | Ordering-guard operators. Each is an alias for 'PCmp' at a fixed--- 'Cmp': @a .>= b@ is @'PCmp' 'CmpGe' a b@ (i.e. @a >= b@); @a .< b@ is--- @'PCmp' 'CmpLt' a b@; and so on. Same fixity as '(.==)' (@infix 4@):--- relational operators do not chain, sit below the arithmetic operators--- ('.+'/'.-'/'.*'), and above the logical ones ('.&&'/'.||').-(.<),-  (.<=),-  (.>),-  (.>=) ::-    (Ord r, Typeable r) => Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci-(.<) = PCmp CmpLt-(.<=) = PCmp CmpLe-(.>) = PCmp CmpGt-(.>=) = PCmp CmpGe--infix 4 .<, .<=, .>, .>=---- | Inequality guard. @a ./= b@ is @'pnot' (a '.==' b)@, i.e.--- @'PNot' ('PEq' a b)@. Mirrors 'Prelude.(/=)' against the existing--- '(.==)'.-(./=) :: (Eq r, Typeable r) => Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci-a ./= b = PNot (PEq a b)--infix 4 ./=---- | Conjunction / disjunction of predicates. Aliases for 'PAnd' / 'POr',--- mirroring 'Prelude.(&&)' / 'Prelude.(||)' in fixity (@infixr 3@ /--- @infixr 2@), so @p .&& q .|| r@ parses as @(p .&& q) .|| r@.-(.&&), (.||) :: HsPred rs ci -> HsPred rs ci -> HsPred rs ci-(.&&) = PAnd-(.||) = POr--infixr 3 .&&--infixr 2 .||---- | Predicate negation. Alias for 'PNot'. ('Keiki.Core.BoolAlg' also--- exposes 'neg', which is this same operation lifted through the class;--- 'pnot' is the direct AST alias for hand-written guards.)-pnot :: HsPred rs ci -> HsPred rs ci-pnot = PNot---- | Structural arithmetic operators on 'Term's. Aliases for--- 'tadd' / 'tsub' / 'tmul', mirroring 'Prelude.(+)' / '(-)' / '(*)' in--- fixity (@infixl 6@ / @infixl 6@ / @infixl 7@). Because they build the--- structural 'TArith' node (not an opaque 'TApp'), arithmetic written--- with them is visible to the SBV translator in "Keiki.Symbolic".-(.+),-  (.-),-  (.*) ::-    (Num r, Typeable r) => Term rs ci ifs r -> Term rs ci ifs r -> Term rs ci ifs r-(.+) = tadd-(.-) = tsub-(.*) = tmul--infixl 6 .+, .---infixl 7 .*---- | Structural-output construction. 'solveOutput' inverts the result--- mechanically by walking 'OutFields' against the named input--- constructor; users no longer supply an inverse function. The--- 'InCtor' first argument names the @ci@ constructor the edge expects;--- it makes recovery work even for edges whose input has no payload--- (e.g. a singleton 'Continue' command).-pack ::-  InCtor ci ifs ->-  WireCtor co fields ->-  OutFields rs ci ifs fields ->-  OutTerm rs ci co-pack = OPack---- * Evaluators ----------------------------------------------------------------- | Evaluate a 'Term' against a register file and an input symbol.-evalTerm :: Term rs ci ifs r -> RegFile rs -> ci -> r-evalTerm (TLit r) _ _ = r-evalTerm (TReg ix) regs _ = regs ! ix-evalTerm (TInpCtorField ic ix) _ ci = case icMatch ic ci of-  Just rf -> rf ! ix-  Nothing -> error ("evalTerm: TInpCtorField guard violation: " ++ icName ic)-evalTerm (TApp1 f t) regs ci = f (evalTerm t regs ci)-evalTerm (TApp2 f a b) regs ci = f (evalTerm a regs ci) (evalTerm b regs ci)-evalTerm (TArith op a b) regs ci =-  applyNumOp op (evalTerm a regs ci) (evalTerm b regs ci)---- | Interpret a 'NumOp' tag as the corresponding numeric operation.--- The 'Num' evidence is supplied by matching the 'TArith' constructor.-applyNumOp :: (Num r) => NumOp -> r -> r -> r-applyNumOp OpAdd = (+)-applyNumOp OpSub = (-)-applyNumOp OpMul = (*)---- | Evaluate an 'OutTerm' against a register file and an input symbol.--- The 'InCtor' on 'OPack' is consulted only by the inverse direction--- ('solveOutput'); evaluation just runs the wire build over the--- evaluated 'OutFields'.-evalOut :: OutTerm rs ci co -> RegFile rs -> ci -> co-evalOut (OPack _ic ctor fields) regs ci =-  wcBuild ctor (evalOutFields fields regs ci)--evalOutFields :: OutFields rs ci ifs fs -> RegFile rs -> ci -> fs-evalOutFields OFNil _ _ = ()-evalOutFields (OFCons t rest) regs ci =-  (evalTerm t regs ci, evalOutFields rest regs ci)---- | Evaluate a predicate to a 'Bool' on the current state.-evalPred :: HsPred rs ci -> RegFile rs -> ci -> Bool-evalPred PTop _ _ = True-evalPred PBot _ _ = False-evalPred (PAnd p q) r c = evalPred p r c && evalPred q r c-evalPred (POr p q) r c = evalPred p r c || evalPred q r c-evalPred (PNot p) r c = not (evalPred p r c)-evalPred (PEq a b) r c = evalTerm a r c == evalTerm b r c-evalPred (PInCtor ic) _ c = case icMatch ic c of-  Just _ -> True-  Nothing -> False-evalPred (PCmp op a b) r c = applyCmp op (evalTerm a r c) (evalTerm b r c)-  where-    applyCmp :: (Ord x) => Cmp -> x -> x -> Bool-    applyCmp CmpLt x y = x < y-    applyCmp CmpLe x y = x <= y-    applyCmp CmpGt x y = x > y-    applyCmp CmpGe x y = x >= y---- | Apply an 'Update' to the register file. 'UCombine' applies left--- then right; the smart 'combine''s 'Disjoint' constraint guarantees--- the two halves write to disjoint slots, so the application order--- does not affect the result.-runUpdate :: Update rs w ci -> RegFile rs -> ci -> RegFile rs-runUpdate UKeep regs _ = regs-runUpdate (USet ix t) regs ci = setSlotN ix (evalTerm t regs ci) regs-runUpdate (UCombine a b) regs ci = runUpdate b (runUpdate a regs ci) ci---- | Pure register-file slot update at a slot-name-tagged 'IndexN'.------ The bang-pattern on @v@ forces the new slot value to WHNF before--- threading it into the rebuilt 'RCons'. Without this, every--- 'runUpdate' / 'step' cycle in a long-running embedder accumulates--- a tower of thunks at the written slot, which is exactly the failure--- mode the @NoThunks (RegFile rs)@ instance ("Keiki.NoThunks") was--- introduced to detect (EP-23). Untouched slots retain whatever--- WHNF status they already had, which preserves--- 'Keiki.Generics.emptyRegFile'\'s targeted @uninit:@ sentinels for--- slots that have never been written.-setSlotN :: IndexN s rs r -> r -> RegFile rs -> RegFile rs-setSlotN IZ !v regs = case regs of RCons p _ rest -> RCons p v rest-setSlotN (IS i) !v regs = case regs of-  RCons p x rest ->-    let !rest' = setSlotN i v rest-     in RCons p x rest'---- | Single-step transition. Returns 'Just (s', regs')' iff exactly one--- outgoing edge has a satisfied guard.-delta ::-  (BoolAlg phi (RegFile rs, ci)) =>-  SymTransducer phi rs s ci co ->-  s ->-  RegFile rs ->-  ci ->-  Maybe (s, RegFile rs)-delta t s regs ci =-  case [ (target e, applyEdgeUpdate e regs ci)-       | e <- edgesOut t s,-         models (guard e) (regs, ci)-       ] of-    [single] -> Just single-    _ -> Nothing---- | Single-step output. Returns the list of events emitted by the--- unique active edge: @[]@ for an ε-edge, @[o]@ for a letter edge,--- @[o1, o2, ...]@ for a multi-event edge. Returns @[]@ if no edge--- (or more than one edge) is active — the caller cannot distinguish--- "no active edge" from "active ε-edge" from this function alone;--- use 'step' or 'delta' if that distinction matters.-omega ::-  (BoolAlg phi (RegFile rs, ci)) =>-  SymTransducer phi rs s ci co ->-  s ->-  RegFile rs ->-  ci ->-  [co]-omega t s regs ci =-  case [ [evalOut o regs ci | o <- output e]-       | e <- edgesOut t s,-         models (guard e) (regs, ci)-       ] of-    [evaluatedOuts] -> evaluatedOuts-    _ -> []---- * Pure-layer entry points ---------------------------------------------------- | One full step of the transducer combining 'delta' and 'omega'.--- Returns 'Nothing' if no edge from the current vertex has a satisfied--- guard. The inner @[co]@ is @[]@ for an ε-edge, @[o]@ for a letter--- edge, @[o1, o2, ...]@ for a multi-event edge.-step ::-  (BoolAlg phi (RegFile rs, ci)) =>-  SymTransducer phi rs s ci co ->-  (s, RegFile rs) ->-  ci ->-  Maybe (s, RegFile rs, [co])-step t (s, regs) ci = case delta t s regs ci of-  Nothing -> Nothing-  Just (s', regs') -> Just (s', regs', omega t s regs ci)---- | A locator for one outgoing edge: the vertex it leaves from and its--- zero-based position in @'edgesOut' t source@. This is the canonical--- edge-identity vocabulary shared with build-time diagnostics (EP-56).-data EdgeRef s = EdgeRef-  { edgeSource :: s,-    edgeIndex :: Int-  }-  deriving stock (Eq, Show)---- | Why one outgoing edge was rejected during a step: its locator, its--- declared target, and whether its guard matched (always 'False' here;--- the field keeps the shape uniform with 'MatchedEdgeSummary' and leaves--- room for richer rejection reasons later). Deliberately carries NO--- register values — diagnostics summarize, they do not dump state.-data RejectedEdgeSummary s = RejectedEdgeSummary-  { rejectedEdge :: EdgeRef s,-    rejectedTarget :: s,-    rejectedGuard :: Bool-  }-  deriving stock (Eq, Show)---- | One outgoing edge whose guard matched during a step: its locator and--- its declared target. Carries NO register values.-data MatchedEdgeSummary s = MatchedEdgeSummary-  { matchedEdge :: EdgeRef s,-    matchedTarget :: s-  }-  deriving stock (Eq, Show)---- | A precise explanation of why a step could not advance.------   * 'NoOutgoingEdges' — the source vertex has no outgoing edges at all.---   * 'NoMatchingEdge'   — there are outgoing edges, but none matched the---     command; carries one 'RejectedEdgeSummary' per edge, in declaration---     order.---   * 'AmbiguousEdges'   — two or more guards matched the same command, a---     runtime witness of a single-valuedness violation (the property---     EP-56's 'checkTransitionDeterminism' proves statically); carries one---     'MatchedEdgeSummary' per matched edge.-data StepFailure s-  = NoOutgoingEdges s-  | NoMatchingEdge s [RejectedEdgeSummary s]-  | AmbiguousEdges s [MatchedEdgeSummary s]-  deriving stock (Eq, Show)---- | Like 'step', but returns a precise 'StepFailure' explanation on the--- 'Left' instead of collapsing every failure into 'Nothing'. On the--- 'Right' it returns EXACTLY the triple 'step' returns. 'step' is left--- unchanged; this is purely additive.-stepEither ::-  (BoolAlg phi (RegFile rs, ci)) =>-  SymTransducer phi rs s ci co ->-  (s, RegFile rs) ->-  ci ->-  Either (StepFailure s) (s, RegFile rs, [co])-stepEither t (s, regs) ci =-  case zip [0 ..] (edgesOut t s) of-    [] -> Left (NoOutgoingEdges s)-    indexed ->-      let matched =-            [ (i, e)-            | (i, e) <- indexed,-              models (guard e) (regs, ci)-            ]-       in case matched of-            [] ->-              Left $-                NoMatchingEdge-                  s-                  [ RejectedEdgeSummary-                      { rejectedEdge = EdgeRef {edgeSource = s, edgeIndex = i},-                        rejectedTarget = target e,-                        rejectedGuard = False-                      }-                  | (i, e) <- indexed-                  ]-            [(_, e)] ->-              let !regs' = applyEdgeUpdate e regs ci-                  outs = [evalOut o regs ci | o <- output e]-               in Right (target e, regs', outs)-            _ ->-              Left $-                AmbiguousEdges-                  s-                  [ MatchedEdgeSummary-                      { matchedEdge = EdgeRef {edgeSource = s, edgeIndex = i},-                        matchedTarget = target e-                      }-                  | (i, e) <- matched-                  ]---- | Apply one observed output to the state by walking outgoing edges,--- inverting each edge's @output@ via 'solveOutput', verifying the--- guard on the recovered input, and applying the edge's @update@.--- Used by 'reconstitute' for full-log replay and exposed so that--- single-event façades (notably 'Keiki.Decider.toDecider') can--- implement an @evolve :: s -> e -> s@ step on top of it.------ == Letter-only semantics------ This function handles ε-edges (@output = []@; skipped because they--- emit nothing observable) and letter edges (@output = [o]@;--- inverted via 'solveOutput'). For multi-event edges (@output =--- [o1, ..., oN]@ with N >= 2), this letter-flavoured 'applyEvent'--- only inverts against the *head* of the output list, returning the--- target vertex on a successful match. It is suitable when the--- caller knows it is replaying letter-only events; for true--- streaming replay across multi-event edges (where intermediate--- events in the chain must be matched against the expected tail of--- a prior edge's output list) use 'applyEventStreaming'.-applyEvent ::-  (BoolAlg phi (RegFile rs, ci), Eq co) =>-  SymTransducer phi rs s ci co ->-  s ->-  RegFile rs ->-  co ->-  Maybe (s, RegFile rs)-applyEvent t s regs co =-  case [ (target e, applyEdgeUpdate e regs ci)-       | e <- edgesOut t s,-         o : _ <- [output e],-         Just ci <- [solveOutput o regs co],-         models (guard e) (regs, ci)-       ] of-    [single] -> Just single-    _ -> Nothing---- | Streaming-replay state wrapper. Used by 'applyEventStreaming'--- (the InFlight-aware replay) and exposed as the carrier of the--- 'Keiki.Decider.evolveStreaming' field added in EP-19 M5.------ @'Settled' s@ is the state at a stable vertex — the next event--- must be the first emission of /some/ outgoing edge of @s@.------ @'InFlight' s [e2, ..., eN]@ is the mid-chain state at vertex--- @s@ (the *target* of the in-flight chain's edge; register updates--- have already been applied at the transition into 'InFlight'). The--- queue holds the *evaluated* expected events in order; the next--- observed event must equal the head, popping it; when the queue--- empties, the wrapper transitions to @'Settled' s@.------ See @docs/research/gsm-widening-design.md@ §4 for the formal--- treatment and a worked example on the @StartRegistration@ chain.-data InFlight s co-  = Settled !s-  | InFlight !s ![co]-  deriving (Eq, Show)---- | Apply one observed output to a streaming-replay state. Two arms:------   1. @'Settled' s@ — walk outgoing edges of @s@; find the unique---      edge whose @output@'s *head* inverts to a valid @ci@ via---      'solveOutput' satisfying the guard. Commit to that edge, run---      its update, evaluate the *tail* of the output list against---      the recovered @(regs, ci)@ snapshot. If the tail is empty---      (letter edge), return @('Settled' (target e), regs')@. If the---      tail is non-empty (multi-event edge), return @('InFlight'---      (target e) tail, regs')@.------   2. @'InFlight' s (q1 : rest) regs@ — equality-check @q1@---      against the observed event. On match, advance the queue---      (returning @'Settled' s@ when @rest == []@, otherwise---      @'InFlight' s rest@). No register update — registers were---      updated at the @Settled → InFlight@ transition. On mismatch---      (out-of-order replay) return 'Nothing'.------ The 'Eq' constraint on @co@ supports the queue equality check.--- Most aggregate event types derive 'Eq' (a documented expectation--- of the foundations).-applyEventStreaming ::-  (BoolAlg phi (RegFile rs, ci), Eq co) =>-  SymTransducer phi rs s ci co ->-  InFlight s co ->-  RegFile rs ->-  co ->-  Maybe (InFlight s co, RegFile rs)-applyEventStreaming t (Settled s) regs co =-  case [ (e, ci)-       | e <- edgesOut t s,-         o : _ <- [output e],-         Just ci <- [solveOutput o regs co],-         models (guard e) (regs, ci)-       ] of-    [(e, ci)] ->-      let regs' = applyEdgeUpdate e regs ci-          evaluatedTail = [evalOut o regs ci | o <- drop 1 (output e)]-          wrapped = case evaluatedTail of-            [] -> Settled (target e)-            xs -> InFlight (target e) xs-       in Just (wrapped, regs')-    _ -> Nothing-applyEventStreaming _ (InFlight s queue) regs co = case queue of-  [] -> Nothing-  [q1]-    | q1 == co -> Just (Settled s, regs)-    | otherwise -> Nothing-  (q1 : rest)-    | q1 == co -> Just (InFlight s rest, regs)-    | otherwise -> Nothing---- | Reconstitute @(state, registers)@ from a log of outputs by--- replaying each event through the InFlight-aware--- 'applyEventStreaming', which threads mid-chain state through--- multi-event edges invisibly and unwraps to 'Settled' at the log's--- end.------ For letter-only transducers (every edge has @output@ of length 0--- or 1) the streaming wrapper is always 'Settled' and the result is--- identical to the pre-EP-19 letter-fold. A log that ends mid-chain--- through a multi-event edge returns 'Nothing' — there is no valid--- @(s, regs)@ to surface from an 'InFlight' final state.-reconstitute ::-  (BoolAlg phi (RegFile rs, ci), Eq co) =>-  SymTransducer phi rs s ci co ->-  [co] ->-  Maybe (s, RegFile rs)-reconstitute t = applyEvents t (initial t, initialRegs t)---- | Replay a chunk of events from a caller-supplied--- @(state, registers)@ start. Structurally similar to 'reconstitute'--- except that the start state is an argument rather than the--- transducer's initial state, so a runtime adapter can chunk-replay--- the events corresponding to one logical command from any current--- state.------ Useful when the runtime preserves command boundaries (event store--- with command-id tags, transactional batches, deterministic test--- fixtures): replay one command's events as one atomic step and--- consume the unwrapped final state.------ == Multi-event edges (EP-19 M3)------ Internally, the implementation lifts the start state to 'Settled'--- and folds 'applyEventStreaming' over the chunk; the wrapper--- transitions through 'InFlight' for multi-event edges and unwraps--- back to 'Settled' when the chunk completes. A chunk that ends--- mid-flight (the queue is non-empty at the end of the input list)--- returns 'Nothing'; this signals a truncated chunk relative to the--- edge's static output length.------ For length-0/1 edges the behaviour is identical to the legacy--- letter-fold; for length-2+ edges the chunk must contain the full--- expected sequence of evaluated events in order.------ Returns 'Nothing' if any event in the chunk fails to replay (e.g.--- a malformed log, an event that does not match any active edge's--- output at the current vertex, or a chunk that ends mid-flight).-applyEvents ::-  (BoolAlg phi (RegFile rs, ci), Eq co) =>-  SymTransducer phi rs s ci co ->-  (s, RegFile rs) ->-  [co] ->-  Maybe (s, RegFile rs)-applyEvents t (s0, regs0) cos_ = go (Settled s0) regs0 cos_-  where-    go (Settled s) regs [] = Just (s, regs)-    go (InFlight _ _) _ [] = Nothing -- chunk ended mid-flight-    go inFlight regs (co : rest) = do-      (inFlight', regs') <- applyEventStreaming t inFlight regs co-      go inFlight' regs' rest---- * Build-time analyses -------------------------------------------------------- | Recover the input that produced a given output by walking--- 'OutFields' structurally against the input constructor named by the--- 'OPack'. Gather '(Index, value)' pairs from every top-level--- 'TInpCtorField' read whose 'InCtor' matches by 'icName'; assemble a--- 'RegFile' covering every slot of the 'InCtor'; call 'icBuild'.------ == Recompute-and-verify (EP-47)------ The command is recovered from the /invertible/ fields alone--- (@TLit@\/@TReg@\/@TInpCtorField@); /derived/ fields (@TArith@\/@TApp1@\/--- @TApp2@) are skipped during recovery by 'gatherInpEntries'. After the--- command is rebuilt, the observed field tuple is rebuilt with each--- /derived/ field recomputed forward (via 'recomputeDerivedFields') and--- the resulting event is required to equal the observed event, so each--- derived field is /verified/ rather than trusted — a tampered derived--- value is rejected. Invertible fields are kept at their observed values--- and are /not/ re-verified (so a @TReg@ audit field still round-trips--- even when replay starts from a state whose registers are not yet--- populated). This generalizes, at field granularity, the--- forward-recompute-and-@Eq@-match that 'applyEventStreaming' already does--- for multi-event tails (see @docs/research/recompute-and-verify-derived-outputs.md@).------ For an all-invertible edge no field is recomputed, so the rebuilt event--- equals the observed event by construction (the check is a no-op) and the--- result is identical to the pre-EP-47 behavior. The build-time net--- 'checkHiddenInputs' still rejects a schema whose command slot is read--- only inside a derived field (a hidden input), so the command remains--- recoverable from invertible fields alone — "the event determines the--- command" is preserved.-solveOutput :: (Eq co) => OutTerm rs ci co -> RegFile rs -> co -> Maybe ci-solveOutput (OPack ic@InCtor {} ctor fields) regs co = do-  fs_obs <- wcMatch ctor co-  entries <- gatherInpEntries fields fs_obs ic-  rf <- assemble entries-  let ci = icBuild ic rf-      -- Rebuild the observed field tuple, recomputing ONLY the derived-      -- fields (TApp/TArith) forward; invertible fields keep their observed-      -- value. Comparing the rebuilt event to the observed one then verifies-      -- exactly the derived fields — never the invertible ones, so a-      -- register-read audit field is not re-checked against state and the-      -- command thunk is not forced for an all-invertible edge.-      rebuilt = wcBuild ctor (recomputeDerivedFields fields fs_obs regs ci)-  if rebuilt == co-    then Just ci-    else Nothing---- | Rebuild an observed output-field tuple, recomputing each /derived/--- field ('TApp1'\/'TApp2'\/'TArith') forward via 'evalTerm' against the--- recovered command and the pre-update registers, while leaving every--- /invertible/ field ('TLit'\/'TReg'\/'TInpCtorField') at its observed--- value. Used by 'solveOutput' (EP-47 recompute-and-verify): comparing the--- rebuilt event to the observed one (via 'Eq' on @co@) then verifies--- exactly the derived fields. Invertible fields are deliberately /not/--- recomputed, so (a) a register-read audit field is not re-verified against--- the current register file — preserving the "@TReg@ round-trips" contract--- even when replay starts from a state whose registers are not yet--- populated — and (b) the recovered-command thunk is not forced for an--- all-invertible edge.-recomputeDerivedFields ::-  forall rs ci ifs fs. OutFields rs ci ifs fs -> fs -> RegFile rs -> ci -> fs-recomputeDerivedFields OFNil () _ _ = ()-recomputeDerivedFields (OFCons t rest) (v, vs) regs ci =-  (recomputeOne t v, recomputeDerivedFields rest vs regs ci)-  where-    recomputeOne :: forall f. Term rs ci ifs f -> f -> f-    recomputeOne term@(TApp1 _ _) _observed = evalTerm term regs ci-    recomputeOne term@(TApp2 _ _ _) _observed = evalTerm term regs ci-    recomputeOne term@(TArith _ _ _) _observed = evalTerm term regs ci-    recomputeOne _ observed = observed---- | Walk an 'OutFields' HList in lockstep with an observed-fields--- tuple, gathering '(Index, value)' pairs for the named 'InCtor' from--- the /invertible/ fields. 'TLit'\/'TReg' contribute nothing; a--- 'TInpCtorField' for the matching 'InCtor' contributes its--- '(Index, value)' pair. Since EP-47 the /derived/ fields--- ('TArith'\/'TApp1'\/'TApp2') are /skipped/ (they contribute no--- entries) rather than aborting the walk — 'solveOutput' verifies them--- forward afterwards. Returns 'Nothing' only on a genuinely malformed--- edge: a 'TInpCtorField' naming a /different/ 'InCtor' (a runtime--- diagnostic; soundness no longer depends on it — see below). 'assemble--- []' for an empty 'ifs' is 'Just RNil', so empty-payload input--- constructors recover trivially; and if a derived field is the /only/--- place a command slot is read, the skipped slot leaves 'assemble'--- short and 'solveOutput' fails — exactly the hidden-input case that--- 'checkHiddenInputs' flags at build time.------ == Type-safe index recovery (EP-53)------ Because 'OutFields' is indexed by the same input field schema @ifs@ as--- the 'OPack''s 'InCtor', a top-level 'TInpCtorField' inside this--- 'OutFields' carries an @'Index' ifs r@ /into the @OPack@'s schema by--- construction/. So @'ByIndex' ix val@ type-checks directly — no--- @unsafeCoerce@ — and a constructor whose field schema differs from the--- 'OPack''s 'InCtor' is rejected at compile time rather than coerced at--- run time. The @'icName' ic1 == 'icName' ic2@ guard is retained only as--- a defensive runtime diagnostic for an 'OutFields' that names a--- different (but same-schema) constructor.-gatherInpEntries ::-  forall rs ci ifs fs.-  OutFields rs ci ifs fs -> fs -> InCtor ci ifs -> Maybe [ByIndex ifs]-gatherInpEntries OFNil () _ic = Just []-gatherInpEntries (OFCons t rest) (v, fs) ic = do-  here <- stepOne t v ic-  more <- gatherInpEntries rest fs ic-  pure (here ++ more)-  where-    stepOne :: forall f. Term rs ci ifs f -> f -> InCtor ci ifs -> Maybe [ByIndex ifs]-    stepOne (TLit _) _val _ = Just []-    stepOne (TReg _) _val _ = Just []-    stepOne (TInpCtorField ic2 ix) val ic1-      | icName ic1 == icName ic2 = Just [ByIndex ix val]-      | otherwise = Nothing-    -- Derived fields are skipped here and verified forward by-    -- 'solveOutput' (EP-47 recompute-and-verify); they contribute no-    -- command information of their own.-    stepOne (TApp1 _ _) _val _ = Just []-    stepOne (TApp2 _ _ _) _val _ = Just []-    stepOne (TArith _ _ _) _val _ = Just []---- | A diagnostic produced by 'checkHiddenInputs'.-data HiddenInputWarning = HiddenInputWarning-  { -- | Description of the edge's source (typically @show s@).-    hiwEdgeSource :: String,-    -- | Human-readable description of what's hidden.-    hiwReason :: String-  }-  deriving (Eq, Show)---- | For every edge in the transducer, check whether the @output@ can--- mechanically recover the input on replay. Specifically:------   * If @output@ is @[]@ (an ε-edge), and @update@ reads the input---     symbol, that contribution is silent on the wire and---     unrecoverable.---   * If @output@ is non-empty, the per-edge check groups the---     'OPack's by 'InCtor' name (via 'icName') and computes the---     *union* of slots visited across every 'OPack' naming the same---     'InCtor'. If the union still leaves any of the 'InCtor''s---     slots unvisited, the warning names the 'InCtor' and the---     missing slot(s).------ For length-1 edges this matches the legacy per-'OPack' check--- (there is only one 'OPack' so the union is trivial). For length-2+--- edges the union strengthening means an 'InCtor' jointly recovered--- by multiple 'OPack's in the same edge — none of which covers all--- slots alone, but together they do — does *not* fire the warning.------ The check is intentionally conservative: it flags candidates for--- the author to inspect, not theorems.-checkHiddenInputs ::-  forall phi rs s ci co.-  (Bounded s, Enum s, Show s) =>-  SymTransducer phi rs s ci co ->-  [HiddenInputWarning]-checkHiddenInputs t =-  [ HiddenInputWarning-      { hiwEdgeSource = show s,-        hiwReason = formatHiddenInputReason n r-      }-  | s <- [minBound .. maxBound],-    (n, e) <- zip [(0 :: Int) ..] (edgesOut t s),-    r <- hiddenInputReasons e-  ]---- | A structured reason an edge's output cannot mechanically recover its--- input on replay. This is the single source of truth behind both--- 'checkHiddenInputs' (which formats these into the legacy 'HiddenInputWarning'--- strings via 'formatHiddenInputReason') and 'hiddenInputWarnings' (which lifts--- each into a structured 'TransducerValidationWarning' carrying the typed source--- vertex, the input-constructor name, and the missing slot names).-data HiddenInputReason-  = -- | An ε-edge (empty @output@) whose @update@ reads the input symbol,-    --       so the read information is silent on the wire.-    HirEpsilonReadsInput-  | -- | The named input constructor has declared slots the edge's output-    --       never recovers (after unioning every same-constructor 'OPack').-    --       Carries the constructor name and the missing slot names.-    HirUnionMiss String [String]-  deriving (Eq, Show)---- | The per-edge hidden-input analysis, factored out of 'checkHiddenInputs'--- so the legacy string warnings and the structured 'hiddenInputWarnings' share--- one implementation. For an ε-edge it reports 'HirEpsilonReadsInput' iff the--- update reads the input; for a non-empty output it groups 'OPack's by input--- constructor name, unions the recovered slots, and reports a 'HirUnionMiss' for--- any constructor with uncovered slots (first-seen order, deterministic).-hiddenInputReasons ::-  forall phi rs ci co s. Edge phi rs ci co s -> [HiddenInputReason]-hiddenInputReasons e = case output e of-  []-    | edgeReadsInput e -> [HirEpsilonReadsInput]-    | otherwise -> []-  outs ->-    [ HirUnionMiss icN missing-    | (icN, allSlots, visitedUnion) <- groupByInCtorName outs,-      let missing = allSlots \\ nub visitedUnion,-      not (null missing)-    ]-  where-    -- Walk the output list, accumulating per-InCtor (slot list, visited-    -- slots). First seen wins on the slot list; subsequent OPacks with the-    -- same InCtor name extend the visited list.-    groupByInCtorName ::-      [OutTerm rs ci co] -> [(String, [String], [String])]-    groupByInCtorName = foldl add []-      where-        add acc (OPack ic _ fields) =-          let icN = icName ic-              allSl = slotNamesOf ic-              visited = visitedSlotsOf ic fields-           in extend acc icN allSl visited--        extend [] icN allSl visited = [(icN, allSl, visited)]-        extend ((n, sl, v) : rest) icN allSl visited-          | n == icN = (n, sl, v ++ visited) : rest-          | otherwise = (n, sl, v) : extend rest icN allSl visited--    -- Slots of an OPack's named 'InCtor' that the supplied 'OutFields' walk-    -- recovers via a /top-level/ 'TInpCtorField'. Since EP-47 this does NOT-    -- descend into derived ('TApp1'\/'TApp2'\/'TArith') terms: a slot read-    -- only inside a derived field is a /hidden input/, so it is reported-    -- missing rather than counted as covered.-    visitedSlotsOf ::-      forall ifs fs.-      InCtor ci ifs -> OutFields rs ci ifs fs -> [String]-    visitedSlotsOf ic@InCtor {} fields = goFields fields-      where-        allSlots = slotNamesOf ic--        goFields :: forall fs'. OutFields rs ci ifs fs' -> [String]-        goFields OFNil = []-        goFields (OFCons tt rest) = goTerm tt ++ goFields rest--        goTerm :: forall r. Term rs ci ifs r -> [String]-        goTerm (TInpCtorField ic2 ix)-          | icName ic2 == icName ic =-              [allSlots !! indexPos ix]-          | otherwise = []-        goTerm _ = [] -- do not descend into derived terms-        indexPos :: forall rs' r. Index rs' r -> Int-        indexPos ZIdx = 0-        indexPos (SIdx i) = 1 + indexPos i---- | Format a 'HiddenInputReason' into the legacy 'HiddenInputWarning' reason--- string. The output is byte-identical to the pre-refactor 'checkHiddenInputs'--- text so existing consumers and tests are unaffected.-formatHiddenInputReason :: Int -> HiddenInputReason -> String-formatHiddenInputReason n HirEpsilonReadsInput =-  "edge #" <> show n <> ": ε-edge with input read in update"-formatHiddenInputReason n (HirUnionMiss icN missing) =-  "edge #"-    <> show n-    <> ": OPack walk for InCtor \""-    <> icN-    <> "\" leaves field"-    <> (if length missing == 1 then " " else "s ")-    <> "{"-    <> showMissing missing-    <> "} unrecovered"-  where-    showMissing :: [String] -> String-    showMissing [] = ""-    showMissing [x] = "\"" <> x <> "\""-    showMissing (x : xs) = "\"" <> x <> "\", " <> showMissing xs---- | Does the 'Update' read the input symbol via 'TInpCtorField'?-updateReadsInput :: Update rs w ci -> Bool-updateReadsInput UKeep = False-updateReadsInput (USet _ t) = termReadsInput t-updateReadsInput (UCombine a b) = updateReadsInput a || updateReadsInput b---- | Does the 'Term' read the input symbol via 'TInpCtorField'?-termReadsInput :: Term rs ci ifs r -> Bool-termReadsInput (TLit _) = False-termReadsInput (TReg _) = False-termReadsInput (TInpCtorField _ _) = True-termReadsInput (TApp1 _ t) = termReadsInput t-termReadsInput (TApp2 _ a b) = termReadsInput a || termReadsInput b-termReadsInput (TArith _ a b) = termReadsInput a || termReadsInput b---- | Do the 'OutFields' contain a 'TInpCtorField' read anywhere?-outFieldsHaveInpCtorField :: OutFields rs ci ifs fs -> Bool-outFieldsHaveInpCtorField OFNil = False-outFieldsHaveInpCtorField (OFCons t rest) =-  termHasInpCtorField t || outFieldsHaveInpCtorField rest-  where-    termHasInpCtorField :: Term rs ci ifs r -> Bool-    termHasInpCtorField (TLit _) = False-    termHasInpCtorField (TReg _) = False-    termHasInpCtorField (TInpCtorField _ _) = True-    termHasInpCtorField (TApp1 _ t') = termHasInpCtorField t'-    termHasInpCtorField (TApp2 _ a b) = termHasInpCtorField a || termHasInpCtorField b-    termHasInpCtorField (TArith _ a b) = termHasInpCtorField a || termHasInpCtorField b---- | The result of 'detectMissingInCtorFields': the offending 'InCtor'--- name plus the names of slots its 'OutFields' walk does not visit.-data MissingInCtorFields = MissingInCtorFields-  { mifIcName :: String,-    mifMissing :: [String]-  }-  deriving (Eq, Show)---- | Given the 'InCtor' an 'OPack' is tagged with and that 'OPack'\'s--- 'OutFields', return the field names of the 'InCtor' that the--- 'OutFields' walk does not visit. 'Nothing' means every slot of the--- 'InCtor' is visited. The slot list comes from the 'InCtor' itself--- (via 'KnownSlotNames'), not from any 'TInpCtorField' inside the--- 'OutFields' — this lets us flag empty 'OutFields' against a non---- empty 'InCtor' as well.-detectMissingInCtorFields ::-  forall rs ci ifs fs.-  InCtor ci ifs ->-  OutFields rs ci ifs fs ->-  Maybe MissingInCtorFields-detectMissingInCtorFields ic@InCtor {} fields =-  case allSlots \\ nub visited of-    [] -> Nothing-    missing -> Just (MissingInCtorFields (icName ic) missing)-  where-    allSlots = slotNamesOf ic-    visited = goFields fields--    goFields :: forall fs'. OutFields rs ci ifs fs' -> [String]-    goFields OFNil = []-    goFields (OFCons t rest) = goTerm t ++ goFields rest--    goTerm :: forall r. Term rs ci ifs r -> [String]-    goTerm (TInpCtorField ic2 ix)-      | icName ic2 == icName ic =-          [allSlots !! indexPos ix]-      | otherwise = []-    goTerm _ = [] -- EP-47: top-level reads only; derived-    -- (TApp/TArith) terms are not descended-    -- into, so a slot read only inside one is-    -- reported missing (a hidden input).-    indexPos :: forall rs' r. Index rs' r -> Int-    indexPos ZIdx = 0-    indexPos (SIdx i) = 1 + indexPos i---- | Read the slot-name list out of an 'InCtor' (uses the--- 'KnownSlotNames' instance carried by the data constructor).-slotNamesOf :: forall ci ifs. InCtor ci ifs -> [String]-slotNamesOf InCtor {} = slotNames @ifs---- * Build-time validation umbrella (EP-56) ------------------------------------ | A structured build-time validation warning, parameterized over the--- vertex type @s@ so it carries the real source vertex rather than a--- pre-stringified one. It reuses the canonical 'EdgeRef' locator owned by EP-55--- (the runtime explainer 'stepEither'), so the runtime and build-time--- diagnostics speak one vocabulary.------ Produced by 'validateTransducer'. The three kinds correspond to the three--- authoring mistakes the consumer audit flagged: hidden replay inputs,--- nondeterministic (overlapping) guards, and edges that can never fire.-data TransducerValidationWarning s-  = -- | An edge consumes command information that its output does not-    --       emit, so the command cannot be reconstructed on replay.-    HiddenInput-      { tvwEdge :: EdgeRef s,-        -- | input constructor name, when known-        tvwInCtor :: Maybe String,-        -- | slot/field names left off the wire-        tvwMissingSlots :: [String],-        -- | human-readable summary-        tvwDetail :: String-      }-  | -- | Two outgoing edges of the same vertex whose guards can both hold-    --       for one command — a runtime nondeterminism / single-valuedness-    --       violation (its dynamic witness is EP-55's @AmbiguousEdges@).-    NondeterministicPair-      { tvwSource :: s,-        tvwEdgeA :: Int,-        tvwEdgeB :: Int,-        tvwInCtor :: Maybe String,-        tvwDetail :: String-      }-  | -- | An edge that can never fire: its source vertex is unreachable-    --       from 'initial', or its guard is statically unsatisfiable. Labelled-    --       "possibly" because the structural pass is conservative.-    PossiblyDeadEdge-      { tvwEdge :: EdgeRef s,-        tvwDetail :: String-      }-  | -- | An edge whose guard contains an opaque 'TApp' term. The symbolic-    --       single-valuedness and dead-edge analyses translate such a term to an-    --       unconstrained free variable ('Keiki.Symbolic.translateTermSym' emits-    --       @SBV.free "app1"@), so they cannot see through the guard and silently-    --       under-verify it. Most often this is a collection-content condition-    --       (membership, "all resolved", size) lifted through a closure because the-    --       structural predicate language has no node for it; see the user guide and-    --       @docs\/plans\/60-first-class-collection-registers-design-gated.md@ for the-    --       options. Advisory, not a soundness error: opt in via 'warnOpaqueGuards'.-    OpaqueGuard-      { tvwEdge :: EdgeRef s,-        tvwDetail :: String-      }-  deriving stock (Eq, Show)---- | Which checks 'validateTransducer' runs. All default to 'True' (see--- 'defaultValidationOptions').-data ValidationOptions = ValidationOptions-  { -- | run the hidden-input check-    failOnEpsilonReadsInput :: Bool,-    -- | run the (pure, structural) determinism check-    checkDeterminism :: Bool,-    -- | run the (structural) dead-edge check-    checkReachability :: Bool,-    -- | run the opaque-guard audit (opt-in; default off). Flags edges whose-    --     guard branches on an opaque 'TApp' term the symbolic analyses cannot-    --     see through. Off by default so 'defaultValidationOptions' keeps its-    --     meaning for existing consumers.-    warnOpaqueGuards :: Bool-  }-  deriving stock (Eq, Show)---- | The three soundness checks enabled; the opt-in opaque-guard audit off.-defaultValidationOptions :: ValidationOptions-defaultValidationOptions =-  ValidationOptions-    { failOnEpsilonReadsInput = True,-      checkDeterminism = True,-      checkReachability = True,-      warnOpaqueGuards = False-    }---- | The build-time validation umbrella. Runs the enabled checks over the--- 'HsPred' (syntactic, /no solver/) carrier and concatenates their structured--- warnings, so a project can put @validateTransducer defaultValidationOptions t--- == []@ directly in a unit test and have it pass or fail in microseconds with--- no external z3 process.------ The default path is deliberately specialised to the 'HsPred' carrier and is--- /cheap and pure/: the determinism component flags only structurally-provable--- overlaps (never a false positive, but it can miss overlaps it cannot prove--- syntactically), and the dead-edge component is structural reachability plus a--- literal-'PBot' check. For the exact, solver-backed answers use--- 'Keiki.Symbolic.checkTransitionDeterminismSym' and--- 'Keiki.Symbolic.checkDeadEdgesSym' directly.-validateTransducer ::-  (Bounded s, Enum s, Ord s, Show s) =>-  ValidationOptions ->-  SymTransducer (HsPred rs ci) rs s ci co ->-  [TransducerValidationWarning s]-validateTransducer opts t =-  concat-    [ if failOnEpsilonReadsInput opts then hiddenInputWarnings t else [],-      if checkDeterminism opts then determinismWarnings t else [],-      if checkReachability opts-        then-          [ PossiblyDeadEdge (dewEdge w) (dewReason w)-          | w <- checkDeadEdges defaultDeadEdgeOptions t-          ]-        else [],-      if warnOpaqueGuards opts then opaqueGuardWarnings t else []-    ]---- | Structured form of the hidden-input check, additive over--- 'checkHiddenInputs'. Reuses the same per-edge analysis ('hiddenInputReasons')--- and lifts each result into a 'TransducerValidationWarning' carrying the typed--- source vertex (via 'EdgeRef'), the input-constructor name, and the missing--- slot names — data a downstream project can pattern-match on rather than parse--- out of a string.-hiddenInputWarnings ::-  (Bounded s, Enum s) =>-  SymTransducer phi rs s ci co ->-  [TransducerValidationWarning s]-hiddenInputWarnings t =-  [ HiddenInput-      { tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},-        tvwInCtor = inCtorOf r,-        tvwMissingSlots = missingSlotsOf r,-        tvwDetail = formatHiddenInputReason n r-      }-  | s <- [minBound .. maxBound],-    (n, e) <- zip [(0 :: Int) ..] (edgesOut t s),-    r <- hiddenInputReasons e-  ]-  where-    inCtorOf (HirUnionMiss icN _) = Just icN-    inCtorOf HirEpsilonReadsInput = Nothing-    missingSlotsOf (HirUnionMiss _ ms) = ms-    missingSlotsOf HirEpsilonReadsInput = []---- ** Opaque-guard diagnostics---- | Does the term contain an opaque 'TApp1'\/'TApp2' anywhere? Mirrors the--- structural recursion of 'termReadsInput'; 'TArith' is transparent, so it--- recurses into its operands rather than counting as opaque.-termHasOpaqueApp :: Term rs ci ifs r -> Bool-termHasOpaqueApp (TLit _) = False-termHasOpaqueApp (TReg _) = False-termHasOpaqueApp (TInpCtorField _ _) = False-termHasOpaqueApp (TApp1 _ _) = True-termHasOpaqueApp (TApp2 _ _ _) = True-termHasOpaqueApp (TArith _ a b) = termHasOpaqueApp a || termHasOpaqueApp b---- | Does the guard predicate branch on an opaque term anywhere? The symbolic--- analyses cannot see through such a guard (it becomes a free SBV variable),--- so they silently under-verify the edge.-predHasOpaqueTerm :: HsPred rs ci -> Bool-predHasOpaqueTerm PTop = False-predHasOpaqueTerm PBot = False-predHasOpaqueTerm (PAnd p q) = predHasOpaqueTerm p || predHasOpaqueTerm q-predHasOpaqueTerm (POr p q) = predHasOpaqueTerm p || predHasOpaqueTerm q-predHasOpaqueTerm (PNot p) = predHasOpaqueTerm p-predHasOpaqueTerm (PEq a b) = termHasOpaqueApp a || termHasOpaqueApp b-predHasOpaqueTerm (PInCtor _) = False-predHasOpaqueTerm (PCmp _ a b) = termHasOpaqueApp a || termHasOpaqueApp b---- | The opt-in opaque-guard audit (run by 'validateTransducer' only when--- 'warnOpaqueGuards' is set). For every edge whose guard contains an opaque--- 'TApp' term, emit an 'OpaqueGuard' warning locating the edge by its typed--- 'EdgeRef'. Specialised to the 'HsPred' carrier because it walks the predicate--- AST, exactly as 'validateTransducer' is.-opaqueGuardWarnings ::-  (Bounded s, Enum s) =>-  SymTransducer (HsPred rs ci) rs s ci co ->-  [TransducerValidationWarning s]-opaqueGuardWarnings t =-  [ OpaqueGuard-      { tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},-        tvwDetail =-          "guard contains an opaque TApp term the symbolic analyses cannot "-            ++ "see through; its single-valuedness was not verified"-      }-  | s <- [minBound .. maxBound],-    (n, e) <- zip [(0 :: Int) ..] (edgesOut t s),-    predHasOpaqueTerm (guard e)-  ]---- ** Determinism diagnostics---- | A determinism warning: two outgoing edges of the same vertex whose guards--- can both hold. Carries both edge indices and the (typed) source vertex.-data DeterminismWarning s = DeterminismWarning-  { dwSource :: s,-    -- | first overlapping edge index-    dwEdgeA :: Int,-    -- | second overlapping edge index-    dwEdgeB :: Int,-    dwDetail :: String-  }-  deriving stock (Eq, Show)---- | Per-vertex, per-pair determinism diagnostic. Reuses the exact pairing--- structure of 'Keiki.Symbolic.isSingleValuedSym': for every vertex, for every--- pair @(i,e1),(j,e2)@ with @i<j@, the pair is ambiguous when--- @guard e1 \`conj\` guard e2@ is /not/ 'isBot'. So--- @checkTransitionDeterminism t == []@ iff @isSingleValuedSym t@ under the same--- carrier.------ Soundness direction: with the pure 'HsPred' carrier, 'isBot' only recognises--- the literal 'PBot', so @not (isBot (a \`conj\` b))@ holds for /every/ non-'PBot'--- pair — i.e. this polymorphic check over-approximates overlap on the 'HsPred'--- carrier (it would flag almost every multi-edge vertex). It is intended to be--- run over the /symbolic/ 'SymPred' carrier (via--- 'Keiki.Symbolic.checkTransitionDeterminismSym'), whose 'isBot' is exact. For--- the pure path 'validateTransducer' uses the under-approximating--- 'checkTransitionDeterminismPure' instead, which flags only true positives.-checkTransitionDeterminism ::-  forall phi rs s ci co.-  (BoolAlg phi (RegFile rs, ci), Bounded s, Enum s, Show s) =>-  SymTransducer phi rs s ci co ->-  [DeterminismWarning s]-checkTransitionDeterminism t =-  [ DeterminismWarning-      { dwSource = s,-        dwEdgeA = i,-        dwEdgeB = j,-        dwDetail = overlapDetail i j s-      }-  | s <- [minBound .. maxBound],-    let ies = zip [(0 :: Int) ..] (edgesOut t s),-    (i, e1) <- ies,-    (j, e2) <- ies,-    i < j,-    not (isBot (guard e1 `conj` guard e2))-  ]---- | Over-approximation-free determinism check for the pure 'HsPred' carrier:--- emits a warning only when overlap is structurally provable (both guards are--- 'PTop', or both name the same input constructor). Used by 'validateTransducer'--- so the pure path yields no false positives. Every warning it emits is a true--- positive; the absence of a warning does NOT prove determinism — run--- 'Keiki.Symbolic.checkTransitionDeterminismSym' for the exact answer.-checkTransitionDeterminismPure ::-  forall rs s ci co.-  (Bounded s, Enum s, Show s) =>-  SymTransducer (HsPred rs ci) rs s ci co ->-  [DeterminismWarning s]-checkTransitionDeterminismPure t =-  [ DeterminismWarning-      { dwSource = s,-        dwEdgeA = i,-        dwEdgeB = j,-        dwDetail = overlapDetail i j s-      }-  | s <- [minBound .. maxBound],-    let ies = zip [(0 :: Int) ..] (edgesOut t s),-    (i, e1) <- ies,-    (j, e2) <- ies,-    i < j,-    provablyOverlap (guard e1) (guard e2)-  ]--overlapDetail :: (Show s) => Int -> Int -> s -> String-overlapDetail i j s =-  "edges #"-    <> show i-    <> " and #"-    <> show j-    <> " out of "-    <> show s-    <> " have overlapping guards"---- | Structurally-provable guard overlap for the pure 'HsPred' carrier: 'True'--- only when overlap is certain (both 'PTop', or the same input constructor).--- Conservative — never a false positive; misses overlaps it cannot prove--- syntactically (those are left to the symbolic variant).-provablyOverlap :: HsPred rs ci -> HsPred rs ci -> Bool-provablyOverlap PTop PTop = True-provablyOverlap (PInCtor a) (PInCtor b) = icName a == icName b-provablyOverlap _ _ = False---- | Internal: the determinism component of 'validateTransducer'. Like--- 'checkTransitionDeterminismPure' but emits the richer 'NondeterministicPair'--- directly, populating 'tvwInCtor' with the overlapping command constructor when--- both guards name the same one (and 'Nothing' for the 'PTop' case).-determinismWarnings ::-  (Bounded s, Enum s, Show s) =>-  SymTransducer (HsPred rs ci) rs s ci co ->-  [TransducerValidationWarning s]-determinismWarnings t =-  [ NondeterministicPair-      { tvwSource = s,-        tvwEdgeA = i,-        tvwEdgeB = j,-        tvwInCtor = overlapCtor (guard e1) (guard e2),-        tvwDetail = overlapDetail i j s-      }-  | s <- [minBound .. maxBound],-    let ies = zip [(0 :: Int) ..] (edgesOut t s),-    (i, e1) <- ies,-    (j, e2) <- ies,-    i < j,-    provablyOverlap (guard e1) (guard e2)-  ]-  where-    overlapCtor (PInCtor a) (PInCtor b)-      | icName a == icName b = Just (icName a)-    overlapCtor _ _ = Nothing+{-# LANGUAGE TypeAbstractions #-}+-- Validation diagnostics intentionally expose constructor-specific record+-- selectors. Changing them to total fields would break the public diagnostic+-- API, so keep the partiality explicit and silence the definition-site warning.+{-# OPTIONS_GHC -Wno-partial-fields -Wno-redundant-constraints #-}++-- | The pure core of keiki: the symbolic-register transducer.+--+-- This module is the v1 prototype of the design pinned by+-- @docs/research/dsl-shape-for-symbolic-register.md@ (the DSL note),+-- @docs/research/effects-boundary.md@ (the boundary note), and+-- @docs/research/synthesis-c-foundation-b-presentation-with-worked-examples.md@+-- (the working baseline). See those notes for the rationale behind every+-- shape declared here.+--+-- All v1 escape hatches were retired by MasterPlan 6 (see the+-- Outcomes section of+-- @docs/masterplans/6-retire-remaining-v1-escape-hatches-in-pure-core-ofn-pmatchc-unsafecombine-static-check.md@):+-- @TInpField@ / @OPack@'s hand-written inverse (MP-2 EP-1), 'OFn' /+-- 'mkOut' (MP-6 EP-16), 'PMatchC' / 'matchCmd' (MP-6 EP-17), and+-- 'unsafeCombine' (MP-6 EP-18, replaced by the static 'Disjoint'+-- check on 'combine').+--+-- == Guard-authoring operators (EP-45)+--+-- Predicates and term arithmetic can be written with infix operators+-- that mirror their Prelude counterparts:+--+--   * Relational (build 'HsPred', @infix 4@): '.<' '.<=' '.>' '.>='+--     '.==' './=' — each an alias for 'PCmp'/'PEq' at a fixed relation.+--   * Logical (combine 'HsPred'): '.&&' (@infixr 3@, 'PAnd'),+--     '.||' (@infixr 2@, 'POr'), 'pnot' ('PNot').+--   * Arithmetic (build 'Term', mirror @+@\/@-@\/@*@): '.+' '.-' '.*' —+--     aliases for 'tadd'\/'tsub'\/'tmul'.+--+-- The verbose carrier signatures have synonyms: 'Pred' @rs ci@ for+-- @'HsPred' rs ci@, 'Guarded' @rs s ci co@ for+-- @'SymTransducer' ('HsPred' rs ci) rs s ci co@ (and+-- 'Keiki.Symbolic.SymGuarded' for the SBV-backed carrier).+--+-- Keep spaces around the operators (@lit a .* lit b@); a dot touching an+-- identifier (@x.y@) is OverloadedRecordDot field access. If you import+-- "Data.SBV" alongside this module, import it qualified — SBV exports+-- the same operator names.+module Keiki.Core+  ( -- * Slots and the register file+    Slot,+    RegFile (..),+    Index (..),+    (!),++    -- * Index resolution from labels+    HasIndex (..),++    -- * Term language+    Term (..),+    NumOp (..),++    -- * Input-side structural constructor (v2)+    InCtor (..),+    AssembleRegFile,+    KnownSlotNames (..),+    slotNamesOf,++    -- * Slot-name machinery (re-exported from "Keiki.Internal.Slots")+    IndexN (..),+    HasIndexN (..),+    Disjoint,+    DistinctNames,+    Concat,+    Names,++    -- * Update language+    Update (..),+    combine,++    -- * Output term language+    WireCtor (..),+    OutFields (..),+    (*:),+    oNil,+    OutTerm (..),++    -- * Predicate carrier (v1 first-class AST)+    HsPred (..),+    Pred,+    Cmp (..),++    -- * Effective Boolean algebra+    BoolAlg (..),+    Sat (..),++    -- * Edges and the transducer+    Edge (..),+    SymTransducer (..),+    Guarded,+    applyEdgeUpdate,+    edgeReadsInput,++    -- * Helpers (the user-facing DSL surface)+    matchInCtor,+    proj,+    inpCtor,+    lit,+    tadd,+    tsub,+    tmul,+    (.==),+    (.<),+    (.<=),+    (.>),+    (.>=),+    (./=),+    (.&&),+    (.||),+    pnot,+    (.+),+    (.-),+    (.*),+    pack,++    -- * Evaluators+    evalTerm,+    evalOut,+    evalPred,+    runUpdate,+    delta,+    omega,++    -- * Pure-layer entry points (effects-boundary note)+    step,+    stepEither,+    StepFailure (..),+    EdgeRef (..),+    RejectedEdgeSummary (..),+    MatchedEdgeSummary (..),+    ReplayStepFailure (..),+    ReplayFailureReason (..),+    ReplayFailure (..),+    reconstitute,+    reconstituteEither,+    applyEvent,+    applyEventStreaming,+    applyEventStreamingEither,+    applyEvents,+    applyEventsEither,+    replayEvents,++    -- * Streaming-replay state wrapper (EP-19 M3)+    InFlight (..),++    -- * Build-time analyses+    solveOutput,+    HiddenInputWarning (..),+    checkHiddenInputs,++    -- * Build-time validation umbrella (EP-56)+    TransducerValidationWarning (..),+    ValidationOptions (..),+    defaultValidationOptions,+    validateTransducer,+    hiddenInputWarnings,+    headRecoverabilityWarnings,+    inversionAmbiguityWarnings,+    guardImpliesInputReadWarnings,+    stateChangingEpsilonWarnings,+    opaqueGuardWarnings,+    DeterminismWarning (..),+    checkTransitionDeterminism,+    checkTransitionDeterminismPure,+    DeadEdgeOptions (..),+    defaultDeadEdgeOptions,+    DeadEdgeWarning (..),+    checkDeadEdges,++    -- * Internals exposed for testing+    termReadsInput,+    updateReadsInput,+    outFieldsHaveInpCtorField,+    HiddenInputReason (..),+    hiddenInputReasons,+    detectMissingInCtorFields,+    MissingInCtorFields (..),+  )+where++import Data.Int (Int32, Int64)+import Data.Kind (Type)+import Data.List (nub, partition, (\\))+import Data.Proxy (Proxy (..))+import Data.Set qualified as Set+import Data.Typeable (Typeable)+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.OverloadedLabels (IsLabel (..))+import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)+import Keiki.Internal.Slots+  ( Concat,+    Disjoint,+    DistinctNames,+    HasIndexN (..),+    IndexN (..),+    Names,+  )+import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))++-- | A register slot is a label paired with the type of its value.+type Slot = (Symbol, Type)++-- * Register file -----------------------------------------------------------++-- | A typed heterogeneous register tuple indexed by a list of 'Slot's.+--+-- The slot-value field is intentionally lazy: 'Keiki.Generics.emptyRegFile'+-- seeds each slot with a deferred @error "uninit: \<slot\>"@ thunk so+-- that reading an unwritten slot fails loudly with a targeted message+-- instead of returning a silent bottom. Strictness for *written*+-- slots is enforced on the write path ('setSlotN') instead — see+-- EP-23's Surprises entry for the long-running-service rationale.+data RegFile (rs :: [Slot]) where+  RNil :: RegFile '[]+  RCons ::+    (KnownSymbol s) =>+    Proxy s -> r -> RegFile rs -> RegFile ('(s, r) ': rs)++-- | A type-safe pointer into a 'RegFile'. 'ZIdx' picks the head;+-- 'SIdx' skips one slot.+data Index (rs :: [Slot]) (r :: Type) where+  ZIdx :: (KnownSymbol s) => Index ('(s, r) ': rs) r+  SIdx :: Index rs r -> Index ('(s', r') ': rs) r++-- | Runtime register lookup. Matching on 'Index' first lets GHC's GADT+-- pattern checker see that 'RNil' is unreachable — 'ZIdx' and 'SIdx'+-- both refine @rs@ to @'(_,_) ': _@.+(!) :: RegFile rs -> Index rs r -> r+regs ! ZIdx = case regs of RCons _ x _ -> x+regs ! SIdx i = case regs of RCons _ _ rest -> rest ! i++infixl 9 !++-- * IsLabel / HasIndex -----------------------------------------------------++-- | Resolve a label @s@ against a slot list @rs@ to an 'Index' for the+-- value at that slot. The functional dependency @s rs -> r@ ensures that+-- a label uniquely determines the slot's type.+class+  HasIndex (s :: Symbol) (rs :: [Slot]) (r :: Type)+    | s rs -> r+  where+  indexOf :: Index rs r++instance+  {-# OVERLAPPING #-}+  (KnownSymbol s) =>+  HasIndex s ('(s, r) ': rs) r+  where+  indexOf = ZIdx++instance+  {-# OVERLAPPABLE #-}+  forall s s' r r' rs.+  (HasIndex s rs r) =>+  HasIndex s ('(s', r') ': rs) r+  where+  indexOf = SIdx (indexOf @s @rs @r)++instance+  forall s rs r.+  (HasIndex s rs r) =>+  IsLabel s (Index rs r)+  where+  fromLabel = indexOf @s @rs @r++-- | Resolve a label directly to a 'Term' that reads the named register.+-- This instance lets call sites write @#name@ in any 'Term'-typed+-- context (the arguments of 'requireEq', the elements of 'OutFields',+-- etc.) without the @proj (#name :: Index Regs T)@ annotation that+-- 'IsLabel s (Index rs r)' alone would require.+--+-- The two 'IsLabel' instances ('Index' and 'Term') coexist because GHC+-- dispatches by the expected result type: a context expecting an+-- 'Index' (e.g. 'inpFoo'\'s argument) selects the 'Index' instance; a+-- context expecting a 'Term' (e.g. 'requireEq'\'s arguments) selects+-- this one.+instance+  forall s rs ci ifs r.+  (HasIndex s rs r) =>+  IsLabel s (Term rs ci ifs r)+  where+  fromLabel = TReg (indexOf @s @rs @r)++-- The @IsLabel s (IndexN s rs r)@ instance lives next to 'IndexN' in+-- "Keiki.Internal.Slots" so the orphan check is satisfied.++-- * Term language ----------------------------------------------------------++-- | A numeric operation carried by 'TArith'. @OpAdd@\/@OpSub@\/@OpMul@+-- are @+@\/@-@\/@*@ respectively. Kept as a single tag (rather than+-- three 'Term' constructors) so each total 'Term' walker switches on+-- one value; the three directions are recovered by the smart+-- constructors 'tadd'\/'tsub'\/'tmul'.+data NumOp = OpAdd | OpSub | OpMul+  deriving stock (Eq, Show)++-- | A pure expression over the register file and the input symbol,+-- yielding a value of type @r@.+--+-- The @ifs :: [Slot]@ parameter is the /input field schema/ this term+-- may project from: it is pinned by 'TInpCtorField' (whose 'Index' is+-- into @ifs@) and left free by terms that do not read an input field+-- ('TLit', 'TReg'). Threading @ifs@ through the AST is what lets an+-- 'OutFields' (and hence an 'OPack') guarantee /by construction/ that+-- every top-level input projection reads the same constructor schema as+-- the 'OPack''s 'InCtor' — so 'solveOutput' recovers a command field+-- with no @unsafeCoerce@. Terms that do not appear in an invertible+-- output position ('Update' right-hand sides, 'HsPred' operands)+-- existentially hide @ifs@, so it never leaks into the 'Edge' /+-- 'SymTransducer' surface. See @docs/research/tinpproj-design.md@.+data Term (rs :: [Slot]) (ci :: Type) (ifs :: [Slot]) (r :: Type) where+  TLit :: r -> Term rs ci ifs r+  TReg :: Index rs r -> Term rs ci ifs r+  -- | Structural input projection: read field @ix@ of the input+  --     constructor described by @ic@. The 'InCtor' value names the+  --     expected constructor and supplies the round-trip+  --     ('icMatch'/'icBuild') so that 'solveOutput' can mechanically+  --     recover @ci@ from an observed output. Pins the term's @ifs@ to the+  --     constructor's field schema. See @docs/research/tinpproj-design.md@.+  TInpCtorField :: InCtor ci ifs -> Index ifs r -> Term rs ci ifs r+  TApp1 ::+    (a -> r) ->+    Term rs ci ifs a ->+    Term rs ci ifs r+  TApp2 ::+    (a -> b -> r) ->+    Term rs ci ifs a ->+    Term rs ci ifs b ->+    Term rs ci ifs r+  -- | Structural arithmetic over a numeric operand type. Unlike the+  --     opaque 'TApp1'\/'TApp2' escape hatches, the SBV translator reads+  --     'TArith' for real (on a 'Keiki.Symbolic.discoverSymNum' hit), so a+  --     guard over a /computed/ value — a weighted sum, a derived cap — is+  --     visible to the solver. The 'Num' constraint prevents constructing+  --     arithmetic at non-numeric operand types; 'Typeable' lets the SBV+  --     translator dispatch on @r@. Build with 'tadd'\/'tsub'\/'tmul'.+  TArith ::+    (Num r, Typeable r) =>+    NumOp ->+    Term rs ci ifs r ->+    Term rs ci ifs r ->+    Term rs ci ifs r++-- | Per-constructor input projection. An 'InCtor' value names one+-- constructor of the input symbol type @ci@ and pins the round-trip+-- between that constructor's payload and a typed register file+-- @'RegFile' ifs@. The slot list @ifs@ is the field schema for the+-- constructor; together with 'Index' it lets call sites read fields+-- via 'OverloadedLabels' (for example @inpStart #email@).+--+-- 'icMatch' must return 'Just' iff @ci@ is the named constructor.+-- 'icBuild' is its left inverse: @icMatch (icBuild rf) == Just rf@ for+-- every well-formed @rf@.+--+-- The constraints 'AssembleRegFile' and 'KnownSlotNames' on the data+-- constructor mean that any code holding an 'InCtor' can both+-- mechanically rebuild a 'RegFile' from a bag of '(Index, value)' pairs+-- and recover the slot names of @ifs@ at run time. The instances are+-- automatic for any concrete slot list, so users do not write any+-- additional code.+--+-- See @docs/research/tinpproj-design.md@ for the design rationale and+-- the inversion algorithm that walks 'OutFields' gathering these+-- per-field reads.+data InCtor ci (ifs :: [Slot]) where+  InCtor ::+    (AssembleRegFile ifs, KnownSlotNames ifs) =>+    { icName :: String,+      icMatch :: ci -> Maybe (RegFile ifs),+      icBuild :: RegFile ifs -> ci+    } ->+    InCtor ci ifs++-- * Slot-list helper classes (v2 inversion machinery) ---------------------++-- | Recover the slot names of an @ifs :: [Slot]@ at run time. Used to+-- print precise hidden-input warnings.+class KnownSlotNames (rs :: [Slot]) where+  slotNames :: [String]++instance KnownSlotNames '[] where+  slotNames = []++instance+  (KnownSymbol s, KnownSlotNames rs) =>+  KnownSlotNames ('(s, r) ': rs)+  where+  slotNames = symbolVal (Proxy @s) : slotNames @rs++-- | An (Index, value) pair indexed by an InCtor's slot list. Using a+-- GADT existential lets us bag entries with different element types+-- under one slot list and unpack them safely via pattern matching on+-- the carried 'Index'.+data ByIndex (ifs :: [Slot]) where+  ByIndex :: Index ifs r -> r -> ByIndex ifs++-- | Class to assemble a 'RegFile' from a bag of '(Index, value)' pairs.+-- 'assemble' returns 'Just' iff every slot of @ifs@ is covered by+-- exactly one entry of the bag (extra entries beyond what slots+-- demand are ignored as long as the per-slot lookups succeed in+-- order).+class AssembleRegFile (ifs :: [Slot]) where+  assemble :: [ByIndex ifs] -> Maybe (RegFile ifs)++instance AssembleRegFile '[] where+  assemble _ = Just RNil++instance+  (KnownSymbol s, AssembleRegFile rs) =>+  AssembleRegFile ('(s, r) ': rs)+  where+  assemble entries = do+    v <- findHead entries+    rest <- assemble (popHead entries)+    pure (RCons (Proxy @s) v rest)+    where+      findHead :: [ByIndex ('(s, r) ': rs)] -> Maybe r+      findHead [] = Nothing+      findHead (ByIndex ZIdx v : _) = Just v+      findHead (_ : rest) = findHead rest++      popHead :: [ByIndex ('(s, r) ': rs)] -> [ByIndex rs]+      popHead [] = []+      popHead (ByIndex ZIdx _ : rest) = popHead rest+      popHead (ByIndex (SIdx i) v : rest) = ByIndex i v : popHead rest++-- * Update language --------------------------------------------------------++-- | The copyless update language. The @(w :: [Symbol])@ index+-- records the set of slot names this update writes; the smart+-- constructor 'combine' demands @'Disjoint' w1 w2@ to combine two+-- updates, so "each register is written at most once per edge+-- update" becomes a type-level invariant rather than a runtime check.+--+-- The 'UCombine' raw constructor is *not* constrained by 'Disjoint':+-- the invariant is enforced at the smart-constructor introduction+-- point ('combine'). This keeps internal pattern-matches in+-- "Keiki.Composition" (which reconstruct 'UCombine' values during+-- weakening / substitution) cheap. EP-18 M8 retired the v1+-- 'unsafeCombine' escape hatch; aggregate authors use 'combine'+-- exclusively.+data Update (rs :: [Slot]) (w :: [Symbol]) (ci :: Type) where+  UKeep :: Update rs '[] ci+  -- The right-hand-side 'Term''s input field schema @ifs@ is+  -- existentially hidden: updates are never inverted, so @ifs@ need not+  -- escape into the 'Update' kind (keeping 'Edge' / 'SymTransducer'+  -- unchanged).+  USet ::+    (KnownSymbol s) =>+    IndexN s rs r -> Term rs ci ifs r -> Update rs '[s] ci+  UCombine ::+    Update rs w1 ci ->+    Update rs w2 ci ->+    Update rs (Concat w1 w2) ci++-- | Smart constructor for 'UCombine'. The @'Disjoint' w1 w2@+-- constraint statically enforces that the two halves write to+-- disjoint slot-name sets; an aggregate that writes the same slot+-- twice (e.g. @'USet' #email t1 \`combine\` 'USet' #email t2@) is+-- rejected at compile time with a 'GHC.TypeError.TypeError' naming+-- the offending slot.+combine ::+  (Disjoint w1 w2) =>+  Update rs w1 ci ->+  Update rs w2 ci ->+  Update rs (Concat w1 w2) ci+combine = UCombine++-- * Output term language ---------------------------------------------------++-- | A wire-type tag for one constructor of the user's output sum @co@.+-- The functions let 'solveOutput' pattern-match an observed @co@ and+-- 'evalOut' rebuild a @co@ from its fields.+data WireCtor co fields = WireCtor+  { wcName :: String,+    wcMatch :: co -> Maybe fields,+    wcBuild :: fields -> co+  }++-- | An HList of 'Term's, one per field of the wire constructor. The+-- field-tuple type @fs@ is built up nested-pair style so that+-- 'solveOutput' can walk the HList structurally.+--+-- The @ifs :: [Slot]@ parameter is the shared input field schema of+-- every 'Term' in the list (see 'Term'). 'OPack' ties it to the+-- 'OPack''s 'InCtor', so a top-level 'TInpCtorField' inside an+-- 'OutFields' is statically an 'Index' into the 'OPack''s constructor+-- schema — 'gatherInpEntries' recovers it with no coercion.+data OutFields rs ci ifs fs where+  OFNil :: OutFields rs ci ifs ()+  OFCons ::+    Term rs ci ifs f ->+    OutFields rs ci ifs fs ->+    OutFields rs ci ifs (f, fs)++-- | Right-associative HList constructor synonym for 'OFCons'. Lets+-- 'OutFields' literals read top-to-bottom in the wire ctor's field+-- order:+--+-- > d.recipient *: d.subject *: d.at *: oNil+--+-- Identical AST: @t1 *: t2 *: oNil@ produces the same 'OutFields'+-- value as @OFCons t1 (OFCons t2 OFNil)@. Available at the AST+-- layer (here) so authors who skip the builder can use it; also+-- re-exported by "Keiki.Builder" for builder-form call sites.+(*:) :: Term rs ci ifs f -> OutFields rs ci ifs fs -> OutFields rs ci ifs (f, fs)+(*:) = OFCons++infixr 5 *:++-- | The empty 'OutFields' HList. Synonym for 'OFNil'.+oNil :: OutFields rs ci ifs ()+oNil = OFNil++-- | A pure expression yielding an output value @co@.+data OutTerm (rs :: [Slot]) (ci :: Type) (co :: Type) where+  -- | Structural pack: tagged by an input constructor (which the edge+  --     consumes) and an output wire constructor (which the edge produces),+  --     with one 'Term' per field of the wire constructor. 'solveOutput'+  --     walks the structural 'OutFields', gathering '(Index, value)' pairs+  --     against the named 'InCtor', and reconstructs the input by calling+  --     'icBuild' on the assembled register file. Empty-payload input+  --     constructors (the 'InCtor's slot list is @\'[]@) recover trivially+  --     as @icBuild ic RNil@.+  OPack ::+    InCtor ci ifs ->+    WireCtor co fields ->+    OutFields rs ci ifs fields ->+    OutTerm rs ci co++-- * Predicate carrier ------------------------------------------------------++-- | The predicate AST. Carries enough structure to evaluate guards and+-- to translate to SMT through the SBV-backed 'BoolAlg' instance in+-- "Keiki.Symbolic" (added in EP-2 of MasterPlan 2).+data HsPred (rs :: [Slot]) (ci :: Type) where+  PTop :: HsPred rs ci+  PBot :: HsPred rs ci+  PAnd :: HsPred rs ci -> HsPred rs ci -> HsPred rs ci+  POr :: HsPred rs ci -> HsPred rs ci -> HsPred rs ci+  PNot :: HsPred rs ci -> HsPred rs ci+  PEq ::+    (Eq r, Typeable r) =>+    Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci+  -- | Structural input-constructor guard: @True@ iff the input symbol+  --     is the constructor named by the carried 'InCtor'. The SBV-backed+  --     'BoolAlg' instance recognises constructor mutual exclusion+  --     symbolically through this constructor. See+  --     @docs/research/sbv-boolalg-design.md@.+  PInCtor :: InCtor ci ifs -> HsPred rs ci+  -- | Structural guard for the outer @Left@ arm of an 'Either' input.+  --     This discriminator is independent of 'PInCtor', so a guard can+  --     constrain both the sum arm and the constructor inside that arm.+  PLeftArm :: HsPred rs (Either ci1 ci2)+  -- | Structural guard for the outer @Right@ arm of an 'Either' input.+  PRightArm :: HsPred rs (Either ci1 ci2)+  -- | Ordering guard: compares two 'Term's of the same orderable type+  --     with the relation named by 'Cmp'. @PCmp CmpGe a b@ means @a >= b@,+  --     and so on. Unlike a threshold written through 'TApp1'\/'TApp2'+  --     (which is opaque to the solver), 'PCmp' is /structural/: the+  --     SBV-backed translator in "Keiki.Symbolic" emits a real symbolic+  --     comparison (@.<@, @.<=@, @.>@, @.>=@) whenever the operand type's+  --     'Keiki.Symbolic.SymRep' is symbolically orderable (see+  --     'Keiki.Symbolic.discoverSymOrd'); otherwise it falls back to a+  --     fresh opaque 'SBool', exactly as 'PEq' does for non-'Sym' operands.+  --     Equality is intentionally left to 'PEq' — 'Cmp' has no "equal"+  --     case. Added by EP-41.+  PCmp ::+    (Ord r, Typeable r) =>+    Cmp -> Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci++-- | A four-way ordering relation carried by 'PCmp'. @Lt@\/@Le@\/@Gt@\/+-- @Ge@ are @<@\/@<=@\/@>@\/@>=@ respectively. Kept as a single tag+-- (rather than four 'HsPred' constructors) so the evaluator and the+-- SBV translator each switch on one value; the four directions are+-- recovered by the builder conveniences+-- 'Keiki.Builder.requireLt'\/'requireLe'\/'requireGt'\/'requireGe'.+data Cmp = CmpLt | CmpLe | CmpGt | CmpGe+  deriving stock (Eq, Show)++-- * Effective Boolean algebra ----------------------------------------------++-- | An effective Boolean algebra over @a@-typed witnesses, used as the+-- guard carrier of edges. Witness /extraction/ ('sat') is a separate,+-- stronger capability — see 'Sat'.+class BoolAlg phi a | phi -> a where+  top :: phi+  bot :: phi+  conj :: phi -> phi -> phi+  disj :: phi -> phi -> phi+  neg :: phi -> phi+  models :: phi -> a -> Bool+  isBot :: phi -> Bool++-- | A 'BoolAlg' whose witnesses can be /extracted/ from a satisfiable+-- predicate: @'sat' phi@ returns 'Just' a value satisfying @phi@, or+-- 'Nothing' when @phi@ is unsatisfiable.+--+-- Split out of 'BoolAlg' by EP-44 (MasterPlan 12). Witness+-- reconstruction needs carrier-specific evidence — for the SBV-backed+-- 'Keiki.Symbolic.SymPred' carrier, @ExtractRegFile rs@ (to rebuild the+-- register file from the solver model) and @KnownInCtors ci@ (to rebuild+-- the command) — that the algebra's build/decide methods do not. Keeping+-- 'sat' in its own class means the witness-free analyses+-- ('Keiki.Symbolic.isSingleValuedSym', which uses only 'isBot'/'conj')+-- carry no extraction constraints, so they keep type-checking on+-- register-file-existential carriers (e.g. 'Keiki.Profunctor.SomeSymTransducer')+-- and on composition-produced @ci@ types ('Either', tuples) that have no+-- 'KnownInCtors'. See @docs/research/sbv-boolalg-design.md@.+class (BoolAlg phi a) => Sat phi a where+  sat :: phi -> Maybe a++instance BoolAlg (HsPred rs ci) (RegFile rs, ci) where+  top = PTop+  bot = PBot+  conj p q = PAnd p q+  disj p q = POr p q+  neg p = PNot p+  models p (regs, ci) = evalPred p regs ci+  isBot PBot = True+  isBot _ = False++-- | The v1 syntactic carrier has no solver, hence no extractable+-- witness; 'sat' is always 'Nothing'. The precise witnesses come from+-- the SBV-backed @Sat (SymPred …)@ instance in "Keiki.Symbolic".+instance Sat (HsPred rs ci) (RegFile rs, ci) where+  sat _ = Nothing++-- * Edges and the transducer -----------------------------------------------++-- | A single transition. The 'output' is a list of 'OutTerm's:+-- @[]@ is the ε-edge (no observable emission), @[o]@ is the letter+-- edge (one event, identical to today's @'Just' o@), @[o1, o2, ...]@+-- is the multi-event edge — one transition emits N events in+-- declaration order. See @docs/research/gsm-widening-design.md@.+--+-- The @(w :: [Symbol])@ index on 'update' (the slot-name set the+-- update writes) is *existentially* quantified at the 'Edge' record+-- — different edges out of the same vertex write different slot+-- sets, but the homogeneous list @[Edge phi rs ci co s]@ in+-- 'edgesOut' demands a single @Edge@ type. The existential preserves+-- the static disjointness check at the *introduction* point of any+-- 'Update' value (via 'combine') without polluting the @Edge@'s+-- public type with a per-edge @w@ parameter.+data Edge phi rs ci co s where+  Edge ::+    { guard :: phi,+      update :: Update rs w ci,+      output :: [OutTerm rs ci co],+      target :: s+    } ->+    Edge phi rs ci co s++-- | The single source of truth: a finite control graph plus a register+-- file evolved by edges' 'update' terms.+data SymTransducer phi rs s ci co = SymTransducer+  { edgesOut :: s -> [Edge phi rs ci co s],+    initial :: s,+    initialRegs :: RegFile rs,+    isFinal :: s -> Bool+  }++-- | Readable alias for the v1 predicate carrier:+-- @'Pred' rs ci@ is exactly @'HsPred' rs ci@.+type Pred rs ci = HsPred rs ci++-- | A 'SymTransducer' whose guard carrier is the v1 'HsPred'. Collapses+-- the @'SymTransducer' ('HsPred' rs ci) rs s ci co@ signature — which+-- otherwise repeats @rs@ and @ci@ — into @'Guarded' rs s ci co@.+type Guarded rs s ci co = SymTransducer (HsPred rs ci) rs s ci co++-- | Apply an edge's update to the register file. The 'Edge''s+-- existentially-quantified @w@ index makes @'update' e@ unusable as+-- a function (GHC rejects with "escaped type variables"); this+-- helper hides the existential by pattern-matching internally.+applyEdgeUpdate ::+  Edge phi rs ci co s -> RegFile rs -> ci -> RegFile rs+applyEdgeUpdate Edge {update = u} regs ci = runUpdate u regs ci++-- | Does an edge's update read the input symbol via 'TInpCtorField'?+-- Existential-hiding companion to 'updateReadsInput'.+edgeReadsInput :: Edge phi rs ci co s -> Bool+edgeReadsInput Edge {update = u} = updateReadsInput u++-- * Helpers (DSL surface) --------------------------------------------------++-- | Structural input-constructor guard: @True@ iff the input symbol+-- is the constructor named by the supplied 'InCtor'. The SBV-backed+-- 'BoolAlg' instance can decide constructor-mutual-exclusion+-- symbolically through this guard. The semantics is+-- @evalPred (matchInCtor ic) regs ci == isJust (icMatch ic ci)@.+matchInCtor :: InCtor ci ifs -> HsPred rs ci+matchInCtor = PInCtor++-- | Read a register slot into a 'Term'.+proj :: Index rs r -> Term rs ci ifs r+proj = TReg++-- | Structural input projection: read field @ix@ of the input+-- constructor described by @ic@. The result 'Term''s @ifs@ is the+-- constructor's field schema, so an 'OutFields' built from these is+-- statically tied to the 'OPack''s 'InCtor'.+inpCtor :: InCtor ci ifs -> Index ifs r -> Term rs ci ifs r+inpCtor = TInpCtorField++-- | A constant 'Term'.+lit :: r -> Term rs ci ifs r+lit = TLit++-- | Structural arithmetic smart constructors. @tadd@\/@tsub@\/@tmul@+-- build a 'TArith' over @+@\/@-@\/@*@. The operand type must be numeric+-- ('Num') and 'Typeable'; the SBV translator reads them structurally+-- (see 'Keiki.Symbolic.discoverSymNum'), unlike the opaque 'TApp'+-- escape hatches.+tadd,+  tsub,+  tmul ::+    (Num r, Typeable r) =>+    Term rs ci ifs r -> Term rs ci ifs r -> Term rs ci ifs r+tadd = TArith OpAdd+tsub = TArith OpSub+tmul = TArith OpMul++-- | Equality predicate sugar.+(.==) :: (Eq r, Typeable r) => Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci+(.==) = PEq++infix 4 .==++-- * Predicate & term operators (readable guard DSL) ----------------------++-- | Ordering-guard operators. Each is an alias for 'PCmp' at a fixed+-- 'Cmp': @a .>= b@ is @'PCmp' 'CmpGe' a b@ (i.e. @a >= b@); @a .< b@ is+-- @'PCmp' 'CmpLt' a b@; and so on. Same fixity as '(.==)' (@infix 4@):+-- relational operators do not chain, sit below the arithmetic operators+-- ('.+'/'.-'/'.*'), and above the logical ones ('.&&'/'.||').+(.<),+  (.<=),+  (.>),+  (.>=) ::+    (Ord r, Typeable r) => Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci+(.<) = PCmp CmpLt+(.<=) = PCmp CmpLe+(.>) = PCmp CmpGt+(.>=) = PCmp CmpGe++infix 4 .<, .<=, .>, .>=++-- | Inequality guard. @a ./= b@ is @'pnot' (a '.==' b)@, i.e.+-- @'PNot' ('PEq' a b)@. Mirrors 'Prelude.(/=)' against the existing+-- '(.==)'.+(./=) :: (Eq r, Typeable r) => Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci+a ./= b = PNot (PEq a b)++infix 4 ./=++-- | Conjunction / disjunction of predicates. Aliases for 'PAnd' / 'POr',+-- mirroring 'Prelude.(&&)' / 'Prelude.(||)' in fixity (@infixr 3@ /+-- @infixr 2@), so @p .&& q .|| r@ parses as @(p .&& q) .|| r@.+(.&&), (.||) :: HsPred rs ci -> HsPred rs ci -> HsPred rs ci+(.&&) = PAnd+(.||) = POr++infixr 3 .&&++infixr 2 .||++-- | Predicate negation. Alias for 'PNot'. ('Keiki.Core.BoolAlg' also+-- exposes 'neg', which is this same operation lifted through the class;+-- 'pnot' is the direct AST alias for hand-written guards.)+pnot :: HsPred rs ci -> HsPred rs ci+pnot = PNot++-- | Structural arithmetic operators on 'Term's. Aliases for+-- 'tadd' / 'tsub' / 'tmul', mirroring 'Prelude.(+)' / '(-)' / '(*)' in+-- fixity (@infixl 6@ / @infixl 6@ / @infixl 7@). Because they build the+-- structural 'TArith' node (not an opaque 'TApp'), arithmetic written+-- with them is visible to the SBV translator in "Keiki.Symbolic".+(.+),+  (.-),+  (.*) ::+    (Num r, Typeable r) => Term rs ci ifs r -> Term rs ci ifs r -> Term rs ci ifs r+(.+) = tadd+(.-) = tsub+(.*) = tmul++infixl 6 .+, .-++infixl 7 .*++-- | Structural-output construction. 'solveOutput' inverts the result+-- mechanically by walking 'OutFields' against the named input+-- constructor; users no longer supply an inverse function. The+-- 'InCtor' first argument names the @ci@ constructor the edge expects;+-- it makes recovery work even for edges whose input has no payload+-- (e.g. a singleton 'Continue' command).+pack ::+  InCtor ci ifs ->+  WireCtor co fields ->+  OutFields rs ci ifs fields ->+  OutTerm rs ci co+pack = OPack++-- * Evaluators -------------------------------------------------------------++-- | Evaluate a 'Term' against a register file and an input symbol.+evalTerm :: Term rs ci ifs r -> RegFile rs -> ci -> r+evalTerm (TLit r) _ _ = r+evalTerm (TReg ix) regs _ = regs ! ix+evalTerm (TInpCtorField ic ix) _ ci = case icMatch ic ci of+  Just rf -> rf ! ix+  Nothing -> error ("evalTerm: TInpCtorField guard violation: " ++ icName ic)+evalTerm (TApp1 f t) regs ci = f (evalTerm t regs ci)+evalTerm (TApp2 f a b) regs ci = f (evalTerm a regs ci) (evalTerm b regs ci)+evalTerm (TArith op a b) regs ci =+  applyNumOp op (evalTerm a regs ci) (evalTerm b regs ci)++-- | Interpret a 'NumOp' tag as the corresponding numeric operation.+-- The 'Num' evidence is supplied by matching the 'TArith' constructor.+applyNumOp :: (Num r) => NumOp -> r -> r -> r+applyNumOp OpAdd = (+)+applyNumOp OpSub = (-)+applyNumOp OpMul = (*)++-- | Evaluate an 'OutTerm' against a register file and an input symbol.+-- The 'InCtor' on 'OPack' is consulted only by the inverse direction+-- ('solveOutput'); evaluation just runs the wire build over the+-- evaluated 'OutFields'.+evalOut :: OutTerm rs ci co -> RegFile rs -> ci -> co+evalOut (OPack _ic ctor fields) regs ci =+  wcBuild ctor (evalOutFields fields regs ci)++evalOutFields :: OutFields rs ci ifs fs -> RegFile rs -> ci -> fs+evalOutFields OFNil _ _ = ()+evalOutFields (OFCons t rest) regs ci =+  (evalTerm t regs ci, evalOutFields rest regs ci)++-- | Evaluate a predicate to a 'Bool' on the current state.+evalPred :: HsPred rs ci -> RegFile rs -> ci -> Bool+evalPred PTop _ _ = True+evalPred PBot _ _ = False+evalPred (PAnd p q) r c = evalPred p r c && evalPred q r c+evalPred (POr p q) r c = evalPred p r c || evalPred q r c+evalPred (PNot p) r c = not (evalPred p r c)+evalPred (PEq a b) r c = evalTerm a r c == evalTerm b r c+evalPred (PInCtor ic) _ c = case icMatch ic c of+  Just _ -> True+  Nothing -> False+evalPred PLeftArm _ input = case input of+  Left _ -> True+  Right _ -> False+evalPred PRightArm _ input = case input of+  Left _ -> False+  Right _ -> True+evalPred (PCmp op a b) r c = applyCmp op (evalTerm a r c) (evalTerm b r c)+  where+    applyCmp :: (Ord x) => Cmp -> x -> x -> Bool+    applyCmp CmpLt x y = x < y+    applyCmp CmpLe x y = x <= y+    applyCmp CmpGt x y = x > y+    applyCmp CmpGe x y = x >= y++-- | Apply an 'Update' to the register file. Every right-hand-side term+-- reads the register snapshot from before the whole update began. Writes+-- are then applied left-to-right; the public 'combine' constructor requires+-- disjoint slots, while internal raw 'UCombine' values that repeat a slot+-- therefore keep the rightmost write.+runUpdate :: forall rs w ci. Update rs w ci -> RegFile rs -> ci -> RegFile rs+runUpdate update regs ci = go update regs+  where+    go :: Update rs w' ci -> RegFile rs -> RegFile rs+    go UKeep acc = acc+    go (USet ix t) acc = setSlotN ix (evalTerm t regs ci) acc+    go (UCombine a b) acc = go b (go a acc)++-- | Pure register-file slot update at a slot-name-tagged 'IndexN'.+--+-- The bang-pattern on @v@ forces the new slot value to WHNF before+-- threading it into the rebuilt 'RCons'. Without this, every+-- 'runUpdate' / 'step' cycle in a long-running embedder accumulates+-- a tower of thunks at the written slot, which is exactly the failure+-- mode the @NoThunks (RegFile rs)@ instance ("Keiki.NoThunks") was+-- introduced to detect (EP-23). Untouched slots retain whatever+-- WHNF status they already had, which preserves+-- 'Keiki.Generics.emptyRegFile'\'s targeted @uninit:@ sentinels for+-- slots that have never been written.+setSlotN :: IndexN s rs r -> r -> RegFile rs -> RegFile rs+setSlotN IZ !v regs = case regs of RCons p _ rest -> RCons p v rest+setSlotN (IS i) !v regs = case regs of+  RCons p x rest ->+    let !rest' = setSlotN i v rest+     in RCons p x rest'++-- | Single-step transition. Returns 'Just (s', regs')' iff exactly one+-- outgoing edge has a satisfied guard.+delta ::+  (BoolAlg phi (RegFile rs, ci)) =>+  SymTransducer phi rs s ci co ->+  s ->+  RegFile rs ->+  ci ->+  Maybe (s, RegFile rs)+delta t s regs ci =+  case [ (target e, applyEdgeUpdate e regs ci)+       | e <- edgesOut t s,+         models (guard e) (regs, ci)+       ] of+    [single] -> Just single+    _ -> Nothing++-- | Single-step output. Returns the list of events emitted by the+-- unique active edge: @[]@ for an ε-edge, @[o]@ for a letter edge,+-- @[o1, o2, ...]@ for a multi-event edge. Returns @[]@ if no edge+-- is active or if more than one edge is active. Therefore @[]@ conflates+-- three different outcomes: a rejected command, an ambiguous command,+-- and an accepted ε-edge that emits nothing. Never interpret @[]@ as+-- proof that a command was rejected; use 'stepEither' to distinguish all+-- three outcomes with structured failures.+omega ::+  (BoolAlg phi (RegFile rs, ci)) =>+  SymTransducer phi rs s ci co ->+  s ->+  RegFile rs ->+  ci ->+  [co]+omega t s regs ci =+  case [ [evalOut o regs ci | o <- output e]+       | e <- edgesOut t s,+         models (guard e) (regs, ci)+       ] of+    [evaluatedOuts] -> evaluatedOuts+    _ -> []++-- * Pure-layer entry points ------------------------------------------------++-- | One full step of the transducer combining 'delta' and 'omega'.+-- Returns 'Nothing' if no edge from the current vertex has a satisfied+-- guard. The inner @[co]@ is @[]@ for an ε-edge, @[o]@ for a letter+-- edge, @[o1, o2, ...]@ for a multi-event edge.+step ::+  (BoolAlg phi (RegFile rs, ci)) =>+  SymTransducer phi rs s ci co ->+  (s, RegFile rs) ->+  ci ->+  Maybe (s, RegFile rs, [co])+step t (s, regs) ci = case delta t s regs ci of+  Nothing -> Nothing+  Just (s', regs') -> Just (s', regs', omega t s regs ci)++-- | A locator for one outgoing edge: the vertex it leaves from and its+-- zero-based position in @'edgesOut' t source@. This is the canonical+-- edge-identity vocabulary shared with build-time diagnostics (EP-56).+data EdgeRef s = EdgeRef+  { edgeSource :: s,+    edgeIndex :: Int+  }+  deriving stock (Eq, Show)++-- | Why one outgoing edge was rejected during a step: its locator, its+-- declared target, and whether its guard matched (always 'False' here;+-- the field keeps the shape uniform with 'MatchedEdgeSummary' and leaves+-- room for richer rejection reasons later). Deliberately carries NO+-- register values — diagnostics summarize, they do not dump state.+data RejectedEdgeSummary s = RejectedEdgeSummary+  { rejectedEdge :: EdgeRef s,+    rejectedTarget :: s,+    rejectedGuard :: Bool+  }+  deriving stock (Eq, Show)++-- | One outgoing edge whose guard matched during a step: its locator and+-- its declared target. Carries NO register values.+data MatchedEdgeSummary s = MatchedEdgeSummary+  { matchedEdge :: EdgeRef s,+    matchedTarget :: s+  }+  deriving stock (Eq, Show)++-- | A precise explanation of why a step could not advance.+--+--   * 'NoOutgoingEdges' — the source vertex has no outgoing edges at all.+--   * 'NoMatchingEdge'   — there are outgoing edges, but none matched the+--     command; carries one 'RejectedEdgeSummary' per edge, in declaration+--     order.+--   * 'AmbiguousEdges'   — two or more guards matched the same command, a+--     runtime witness of a single-valuedness violation (the property+--     EP-56's 'checkTransitionDeterminism' proves statically); carries one+--     'MatchedEdgeSummary' per matched edge.+data StepFailure s+  = NoOutgoingEdges s+  | NoMatchingEdge s [RejectedEdgeSummary s]+  | AmbiguousEdges s [MatchedEdgeSummary s]+  deriving stock (Eq, Show)++-- | Like 'step', but returns a precise 'StepFailure' explanation on the+-- 'Left' instead of collapsing every failure into 'Nothing'. On the+-- 'Right' it returns EXACTLY the triple 'step' returns. 'step' is left+-- unchanged; this is purely additive.+stepEither ::+  (BoolAlg phi (RegFile rs, ci)) =>+  SymTransducer phi rs s ci co ->+  (s, RegFile rs) ->+  ci ->+  Either (StepFailure s) (s, RegFile rs, [co])+stepEither t (s, regs) ci =+  case zip [0 ..] (edgesOut t s) of+    [] -> Left (NoOutgoingEdges s)+    indexed ->+      let matched =+            [ (i, e)+            | (i, e) <- indexed,+              models (guard e) (regs, ci)+            ]+       in case matched of+            [] ->+              Left $+                NoMatchingEdge+                  s+                  [ RejectedEdgeSummary+                      { rejectedEdge = EdgeRef {edgeSource = s, edgeIndex = i},+                        rejectedTarget = target e,+                        rejectedGuard = False+                      }+                  | (i, e) <- indexed+                  ]+            [(_, e)] ->+              let !regs' = applyEdgeUpdate e regs ci+                  outs = [evalOut o regs ci | o <- output e]+               in Right (target e, regs', outs)+            _ ->+              Left $+                AmbiguousEdges+                  s+                  [ MatchedEdgeSummary+                      { matchedEdge = EdgeRef {edgeSource = s, edgeIndex = i},+                        matchedTarget = target e+                      }+                  | (i, e) <- matched+                  ]++-- | Apply one observed output to the state by walking outgoing edges,+-- inverting each edge's @output@ via 'solveOutput', verifying the+-- guard on the recovered input, and applying the edge's @update@.+-- Exposed for callers that deliberately model letter-only event streams;+-- full-log replay uses the InFlight-aware streaming surface instead.+--+-- == Letter-only semantics+--+-- This function handles ε-edges (@output = []@; skipped because they+-- emit nothing observable) and letter edges (@output = [o]@;+-- inverted via 'solveOutput'). For multi-event edges (@output =+-- [o1, ..., oN]@ with N >= 2), this letter-flavoured 'applyEvent'+-- only inverts against the *head* of the output list, returning the+-- target vertex on a successful match. It is suitable when the+-- caller knows it is replaying letter-only events; for true+-- streaming replay across multi-event edges (where intermediate+-- events in the chain must be matched against the expected tail of+-- a prior edge's output list) use 'applyEventStreaming'.+applyEvent ::+  (BoolAlg phi (RegFile rs, ci), Eq co) =>+  SymTransducer phi rs s ci co ->+  s ->+  RegFile rs ->+  co ->+  Maybe (s, RegFile rs)+applyEvent t s regs co =+  case [ (target e, applyEdgeUpdate e regs ci)+       | e <- edgesOut t s,+         o : _ <- [output e],+         Just ci <- [solveOutput o regs co],+         models (guard e) (regs, ci)+       ] of+    [single] -> Just single+    _ -> Nothing++-- | Streaming-replay state wrapper. Used by 'applyEventStreamingEither'+-- and its 'applyEventStreaming' compatibility wrapper.+--+-- @'Settled' s@ is the state at a stable vertex — the next event+-- must be the first emission of /some/ outgoing edge of @s@.+--+-- @'InFlight' s [e2, ..., eN]@ is the mid-chain state at vertex+-- @s@ (the *target* of the in-flight chain's edge; register updates+-- have already been applied at the transition into 'InFlight'). The+-- queue holds the *evaluated* expected events in order; the next+-- observed event must equal the head, popping it; when the queue+-- empties, the wrapper transitions to @'Settled' s@.+--+-- See @docs/research/gsm-widening-design.md@ §4 for the formal+-- treatment and a worked example on the @StartRegistration@ chain.+data InFlight s co+  = Settled !s+  | InFlight !s ![co]+  deriving (Eq, Show)++-- | Why one observed event could not be replayed. Mirrors 'StepFailure'+-- and deliberately carries NO register values: diagnostics summarize,+-- they do not dump state. Events are carried where they identify the+-- failure because the event log is already observable data.+--+-- 'ReplayNoInvertingEdge' carries one rejected summary per outgoing+-- edge in declaration order, including edges with no output. An empty+-- list means the vertex had no outgoing edges. 'rejectedGuard' is+-- currently always 'False', matching 'NoMatchingEdge'.+data ReplayStepFailure s co+  = ReplayNoInvertingEdge s [RejectedEdgeSummary s]+  | ReplayAmbiguousInversions s [MatchedEdgeSummary s]+  | ReplayQueueMismatch s co [co]+  deriving stock (Eq, Show)++-- | Why replaying a list of observed events failed. A step failure+-- identifies an event that could not be consumed; truncation means the+-- input ended while a multi-event output chain still had pending events.+data ReplayFailureReason s co+  = ReplayEventFailed (ReplayStepFailure s co)+  | ReplayLogTruncated [co]+  deriving stock (Eq, Show)++-- | A list-level replay failure with its zero-based input position and+-- wrapper state immediately before the failure. For 'ReplayLogTruncated',+-- 'replayFailedIndex' is the input length: the position where the next+-- expected event was missing.+data ReplayFailure s co = ReplayFailure+  { replayFailedIndex :: Int,+    replayFailedState :: InFlight s co,+    replayFailureReason :: ReplayFailureReason s co+  }+  deriving stock (Eq, Show)++-- | Compatibility wrapper around 'applyEventStreamingEither'. Prefer the+-- structured 'Either' variant for new code; this function preserves the+-- historical @Maybe@ signature and semantics.+--+-- Apply one observed output to a streaming-replay state. Two arms:+--+--   1. @'Settled' s@ — walk outgoing edges of @s@; find the unique+--      edge whose @output@'s *head* inverts to a valid @ci@ via+--      'solveOutput' satisfying the guard. Commit to that edge, run+--      its update, evaluate the *tail* of the output list against+--      the recovered @(regs, ci)@ snapshot. If the tail is empty+--      (letter edge), return @('Settled' (target e), regs')@. If the+--      tail is non-empty (multi-event edge), return @('InFlight'+--      (target e) tail, regs')@.+--+--   2. @'InFlight' s (q1 : rest) regs@ — equality-check @q1@+--      against the observed event. On match, advance the queue+--      (returning @'Settled' s@ when @rest == []@, otherwise+--      @'InFlight' s rest@). No register update — registers were+--      updated at the @Settled → InFlight@ transition. On mismatch+--      (out-of-order replay) return 'Nothing'.+--+-- The 'Eq' constraint on @co@ supports the queue equality check.+-- Most aggregate event types derive 'Eq' (a documented expectation+-- of the foundations).+--+-- Inversion is deliberately head-only: 'solveOutput' is applied to the first+-- 'OutTerm' before the tail queue exists, and later events are equality-checked+-- only. Tail events therefore cannot supply command fields missing from the+-- head. 'validateTransducer' reports that authoring error as+-- 'HeadUnrecoverable'.+applyEventStreaming ::+  (BoolAlg phi (RegFile rs, ci), Eq co) =>+  SymTransducer phi rs s ci co ->+  InFlight s co ->+  RegFile rs ->+  co ->+  Maybe (InFlight s co, RegFile rs)+applyEventStreaming t wrapper regs co =+  either (const Nothing) Just (applyEventStreamingEither t wrapper regs co)++-- | Apply one observed event to a streaming-replay state, returning a+-- structured explanation when replay cannot advance.+applyEventStreamingEither ::+  (BoolAlg phi (RegFile rs, ci), Eq co) =>+  SymTransducer phi rs s ci co ->+  InFlight s co ->+  RegFile rs ->+  co ->+  Either (ReplayStepFailure s co) (InFlight s co, RegFile rs)+applyEventStreamingEither t (Settled s) regs co =+  case matched of+    [] ->+      Left $+        ReplayNoInvertingEdge+          s+          [ RejectedEdgeSummary+              { rejectedEdge = EdgeRef {edgeSource = s, edgeIndex = i},+                rejectedTarget = target e,+                rejectedGuard = False+              }+          | (i, e) <- indexed+          ]+    [(_, e, ci)] ->+      let regs' = applyEdgeUpdate e regs ci+          evaluatedTail = [evalOut o regs ci | o <- drop 1 (output e)]+          wrapped = case evaluatedTail of+            [] -> Settled (target e)+            xs -> InFlight (target e) xs+       in Right (wrapped, regs')+    _ ->+      Left $+        ReplayAmbiguousInversions+          s+          [ MatchedEdgeSummary+              { matchedEdge = EdgeRef {edgeSource = s, edgeIndex = i},+                matchedTarget = target e+              }+          | (i, e, _) <- matched+          ]+  where+    indexed = zip [0 ..] (edgesOut t s)+    matched =+      [ (i, e, ci)+      | (i, e) <- indexed,+        o : _ <- [output e],+        Just ci <- [solveOutput o regs co],+        models (guard e) (regs, ci)+      ]+applyEventStreamingEither _ (InFlight s queue) regs co = case queue of+  q1 : rest+    | q1 == co ->+        Right+          ( case rest of+              [] -> Settled s+              _ -> InFlight s rest,+            regs+          )+  _ -> Left (ReplayQueueMismatch s co queue)++-- | Strictly replay a list of observed events from an arbitrary wrapper+-- state and register-file seed. A list that ends mid-chain succeeds with+-- a final 'InFlight' wrapper so paginated callers can resume with the next+-- page. Use 'applyEventsEither' when ending mid-chain must be an error.+replayEvents ::+  (BoolAlg phi (RegFile rs, ci), Eq co) =>+  SymTransducer phi rs s ci co ->+  (InFlight s co, RegFile rs) ->+  [co] ->+  Either (ReplayFailure s co) (InFlight s co, RegFile rs)+replayEvents t = go 0+  where+    go !_ seed [] = Right seed+    go !eventIndex (wrapper, regs) (co : rest) =+      case applyEventStreamingEither t wrapper regs co of+        Left stepFailure ->+          Left+            ReplayFailure+              { replayFailedIndex = eventIndex,+                replayFailedState = wrapper,+                replayFailureReason = ReplayEventFailed stepFailure+              }+        Right next -> go (eventIndex + 1) next rest++-- | Compatibility wrapper around 'reconstituteEither'. Prefer the+-- structured 'Either' variant for new code. This function reconstitutes+-- @(state, registers)@ from a log of outputs while preserving the+-- historical @Maybe@ signature and semantics.+--+-- For letter-only transducers (every edge has @output@ of length 0+-- or 1) the streaming wrapper is always 'Settled' and the result is+-- identical to the pre-EP-19 letter-fold. A log that ends mid-chain+-- through a multi-event edge returns 'Nothing' — there is no valid+-- @(s, regs)@ to surface from an 'InFlight' final state.+reconstitute ::+  (BoolAlg phi (RegFile rs, ci), Eq co) =>+  SymTransducer phi rs s ci co ->+  [co] ->+  Maybe (s, RegFile rs)+reconstitute t events =+  either (const Nothing) Just (reconstituteEither t events)++-- | Reconstitute @(state, registers)@ from the transducer's initial+-- state, returning the exact event index, wrapper state, and structured+-- reason when replay fails.+reconstituteEither ::+  (BoolAlg phi (RegFile rs, ci), Eq co) =>+  SymTransducer phi rs s ci co ->+  [co] ->+  Either (ReplayFailure s co) (s, RegFile rs)+reconstituteEither t = applyEventsEither t (initial t, initialRegs t)++-- | Compatibility wrapper around 'applyEventsEither'. Prefer the+-- structured 'Either' variant for new code. This function replays a+-- chunk of events from a caller-supplied @(state, registers)@ start while+-- preserving the historical @Maybe@ signature and semantics.+--+-- Useful when the runtime preserves command boundaries (event store+-- with command-id tags, transactional batches, deterministic test+-- fixtures): replay one command's events as one atomic step and+-- consume the unwrapped final state.+--+-- == Multi-event edges (EP-19 M3)+--+-- Internally, the implementation lifts the start state to 'Settled'+-- and folds 'applyEventStreaming' over the chunk; the wrapper+-- transitions through 'InFlight' for multi-event edges and unwraps+-- back to 'Settled' when the chunk completes. A chunk that ends+-- mid-flight (the queue is non-empty at the end of the input list)+-- returns 'Nothing'; this signals a truncated chunk relative to the+-- edge's static output length.+--+-- For length-0/1 edges the behaviour is identical to the legacy+-- letter-fold; for length-2+ edges the chunk must contain the full+-- expected sequence of evaluated events in order.+--+-- Returns 'Nothing' if any event in the chunk fails to replay (e.g.+-- a malformed log, an event that does not match any active edge's+-- output at the current vertex, or a chunk that ends mid-flight).+applyEvents ::+  (BoolAlg phi (RegFile rs, ci), Eq co) =>+  SymTransducer phi rs s ci co ->+  (s, RegFile rs) ->+  [co] ->+  Maybe (s, RegFile rs)+applyEvents t seed events =+  either (const Nothing) Just (applyEventsEither t seed events)++-- | Replay a complete chunk from a caller-supplied settled state. Unlike+-- 'replayEvents', this strict facade rejects a chunk that ends while a+-- multi-event output chain still has pending events.+applyEventsEither ::+  (BoolAlg phi (RegFile rs, ci), Eq co) =>+  SymTransducer phi rs s ci co ->+  (s, RegFile rs) ->+  [co] ->+  Either (ReplayFailure s co) (s, RegFile rs)+applyEventsEither t (s0, regs0) events =+  case replayEvents t (Settled s0, regs0) events of+    Left failure -> Left failure+    Right (Settled s, regs) -> Right (s, regs)+    Right (wrapper@(InFlight _ pending), _regs) ->+      Left+        ReplayFailure+          { replayFailedIndex = length events,+            replayFailedState = wrapper,+            replayFailureReason = ReplayLogTruncated pending+          }++-- * Build-time analyses ----------------------------------------------------++-- | Recover the input that produced a given output by walking+-- 'OutFields' structurally against the input constructor named by the+-- 'OPack'. Gather '(Index, value)' pairs from every top-level+-- 'TInpCtorField' read whose 'InCtor' matches by 'icName'; assemble a+-- 'RegFile' covering every slot of the 'InCtor'; call 'icBuild'.+--+-- == Recompute-and-verify (EP-47)+--+-- The command is recovered from the /invertible/ fields alone+-- (@TLit@\/@TReg@\/@TInpCtorField@); /derived/ fields (@TArith@\/@TApp1@\/+-- @TApp2@) are skipped during recovery by 'gatherInpEntries'. After the+-- command is rebuilt, the observed field tuple is rebuilt with each+-- /derived/ field recomputed forward (via 'recomputeDerivedFields') and+-- the resulting event is required to equal the observed event, so each+-- derived field is /verified/ rather than trusted — a tampered derived+-- value is rejected. Invertible fields are kept at their observed values+-- and are /not/ re-verified (so a @TReg@ audit field still round-trips+-- even when replay starts from a state whose registers are not yet+-- populated). This generalizes, at field granularity, the+-- forward-recompute-and-@Eq@-match that 'applyEventStreaming' already does+-- for multi-event tails (see @docs/research/recompute-and-verify-derived-outputs.md@).+--+-- For an all-invertible edge no field is recomputed, so the rebuilt event+-- equals the observed event by construction (the check is a no-op) and the+-- result is identical to the pre-EP-47 behavior. The build-time net+-- 'checkHiddenInputs' still rejects a schema whose command slot is read+-- only inside a derived field (a hidden input), so the command remains+-- recoverable from invertible fields alone — "the event determines the+-- command" is preserved.+--+-- Streaming replay calls this function only for an edge's head 'OutTerm'. It+-- never combines evidence from later outputs, so every command field needed by+-- replay must be recoverable here; 'HeadUnrecoverable' diagnoses a field found+-- only in the tail.+solveOutput :: (Eq co) => OutTerm rs ci co -> RegFile rs -> co -> Maybe ci+solveOutput (OPack ic@InCtor {} ctor fields) regs co = do+  fs_obs <- wcMatch ctor co+  entries <- gatherInpEntries fields fs_obs ic+  rf <- assemble entries+  let ci = icBuild ic rf+      -- Rebuild the observed field tuple, recomputing ONLY the derived+      -- fields (TApp/TArith) forward; invertible fields keep their observed+      -- value. Comparing the rebuilt event to the observed one then verifies+      -- exactly the derived fields — never the invertible ones, so a+      -- register-read audit field is not re-checked against state and the+      -- command thunk is not forced for an all-invertible edge.+      rebuilt = wcBuild ctor (recomputeDerivedFields fields fs_obs regs ci)+  if rebuilt == co+    then Just ci+    else Nothing++-- | Rebuild an observed output-field tuple, recomputing each /derived/+-- field ('TApp1'\/'TApp2'\/'TArith') forward via 'evalTerm' against the+-- recovered command and the pre-update registers, while leaving every+-- /invertible/ field ('TLit'\/'TReg'\/'TInpCtorField') at its observed+-- value. Used by 'solveOutput' (EP-47 recompute-and-verify): comparing the+-- rebuilt event to the observed one (via 'Eq' on @co@) then verifies+-- exactly the derived fields. Invertible fields are deliberately /not/+-- recomputed, so (a) a register-read audit field is not re-verified against+-- the current register file — preserving the "@TReg@ round-trips" contract+-- even when replay starts from a state whose registers are not yet+-- populated — and (b) the recovered-command thunk is not forced for an+-- all-invertible edge.+recomputeDerivedFields ::+  forall rs ci ifs fs. OutFields rs ci ifs fs -> fs -> RegFile rs -> ci -> fs+recomputeDerivedFields OFNil () _ _ = ()+recomputeDerivedFields (OFCons t rest) (v, vs) regs ci =+  (recomputeOne t v, recomputeDerivedFields rest vs regs ci)+  where+    recomputeOne :: forall f. Term rs ci ifs f -> f -> f+    recomputeOne term@(TApp1 _ _) _observed = evalTerm term regs ci+    recomputeOne term@(TApp2 _ _ _) _observed = evalTerm term regs ci+    recomputeOne term@(TArith _ _ _) _observed = evalTerm term regs ci+    recomputeOne _ observed = observed++-- | Walk an 'OutFields' HList in lockstep with an observed-fields+-- tuple, gathering '(Index, value)' pairs for the named 'InCtor' from+-- the /invertible/ fields. 'TLit'\/'TReg' contribute nothing; a+-- 'TInpCtorField' for the matching 'InCtor' contributes its+-- '(Index, value)' pair. Since EP-47 the /derived/ fields+-- ('TArith'\/'TApp1'\/'TApp2') are /skipped/ (they contribute no+-- entries) rather than aborting the walk — 'solveOutput' verifies them+-- forward afterwards. Returns 'Nothing' only on a genuinely malformed+-- edge: a 'TInpCtorField' naming a /different/ 'InCtor' (a runtime+-- diagnostic; soundness no longer depends on it — see below). 'assemble+-- []' for an empty 'ifs' is 'Just RNil', so empty-payload input+-- constructors recover trivially; and if a derived field is the /only/+-- place a command slot is read, the skipped slot leaves 'assemble'+-- short and 'solveOutput' fails — exactly the hidden-input case that+-- 'checkHiddenInputs' flags at build time.+--+-- == Type-safe index recovery (EP-53)+--+-- Because 'OutFields' is indexed by the same input field schema @ifs@ as+-- the 'OPack''s 'InCtor', a top-level 'TInpCtorField' inside this+-- 'OutFields' carries an @'Index' ifs r@ /into the @OPack@'s schema by+-- construction/. So @'ByIndex' ix val@ type-checks directly — no+-- @unsafeCoerce@ — and a constructor whose field schema differs from the+-- 'OPack''s 'InCtor' is rejected at compile time rather than coerced at+-- run time. The @'icName' ic1 == 'icName' ic2@ guard is retained only as+-- a defensive runtime diagnostic for an 'OutFields' that names a+-- different (but same-schema) constructor.+gatherInpEntries ::+  forall rs ci ifs fs.+  OutFields rs ci ifs fs -> fs -> InCtor ci ifs -> Maybe [ByIndex ifs]+gatherInpEntries OFNil () _ic = Just []+gatherInpEntries (OFCons t rest) (v, fs) ic = do+  here <- stepOne t v ic+  more <- gatherInpEntries rest fs ic+  pure (here ++ more)+  where+    stepOne :: forall f. Term rs ci ifs f -> f -> InCtor ci ifs -> Maybe [ByIndex ifs]+    stepOne (TLit _) _val _ = Just []+    stepOne (TReg _) _val _ = Just []+    stepOne (TInpCtorField ic2 ix) val ic1+      | icName ic1 == icName ic2 = Just [ByIndex ix val]+      | otherwise = Nothing+    -- Derived fields are skipped here and verified forward by+    -- 'solveOutput' (EP-47 recompute-and-verify); they contribute no+    -- command information of their own.+    stepOne (TApp1 _ _) _val _ = Just []+    stepOne (TApp2 _ _ _) _val _ = Just []+    stepOne (TArith _ _ _) _val _ = Just []++-- | A diagnostic produced by 'checkHiddenInputs'.+data HiddenInputWarning = HiddenInputWarning+  { -- | Description of the edge's source (typically @show s@).+    hiwEdgeSource :: String,+    -- | Human-readable description of what's hidden.+    hiwReason :: String+  }+  deriving (Eq, Show)++-- | For every edge in the transducer, check whether the @output@ can+-- mechanically recover the input on replay. Specifically:+--+--   * If @output@ is @[]@ (an ε-edge), and @update@ reads the input+--     symbol, that contribution is silent on the wire and+--     unrecoverable.+--   * If @output@ is non-empty, the per-edge check distinguishes data+--     absent from the entire output union ('HirUnionMiss') from data+--     present only after the head event ('HirHeadUnrecoverable'). Replay+--     cannot use tail-only data because 'applyEventStreaming' inverts only+--     the head and equality-checks the tail.+--+-- For length-1 edges this matches the legacy per-'OPack' check. For+-- length-2+ edges, union coverage is retained only to classify the fix:+-- add absent data to the output, or move tail-only data into the head.+--+-- The check is intentionally conservative: it flags candidates for+-- the author to inspect, not theorems.+checkHiddenInputs ::+  forall phi rs s ci co.+  (Bounded s, Enum s, Show s) =>+  SymTransducer phi rs s ci co ->+  [HiddenInputWarning]+checkHiddenInputs t =+  [ HiddenInputWarning+      { hiwEdgeSource = show s,+        hiwReason = formatHiddenInputReason n r+      }+  | s <- [minBound .. maxBound],+    (n, e) <- zip [(0 :: Int) ..] (edgesOut t s),+    r <- hiddenInputReasons e+  ]++-- | A structured reason an edge's output cannot mechanically recover its+-- input on replay. This is the single source of truth behind both+-- 'checkHiddenInputs' (which formats these into the legacy 'HiddenInputWarning'+-- strings via 'formatHiddenInputReason') and 'hiddenInputWarnings' (which lifts+-- each into a structured 'TransducerValidationWarning' carrying the typed source+-- vertex, the input-constructor name, and the missing slot names).+data HiddenInputReason+  = -- | An ε-edge (empty @output@) whose @update@ reads the input symbol,+    --       so the read information is silent on the wire.+    HirEpsilonReadsInput+  | -- | The named input constructor has declared slots the edge's output+    --       never recovers (after unioning every same-constructor 'OPack').+    --       Carries the constructor name and the missing slot names.+    HirUnionMiss String [String]+  | -- | The named input constructor's slots appear in the output union but+    --       not in the head event, so replay cannot reach them. Carries the+    --       constructor name and the tail-only slot names.+    HirHeadUnrecoverable String [String]+  deriving (Eq, Show)++-- | The per-edge hidden-input analysis, factored out of 'checkHiddenInputs'+-- so the legacy string warnings and the structured 'hiddenInputWarnings' share+-- one implementation. For an ε-edge it reports 'HirEpsilonReadsInput' iff the+-- update reads the input; for a non-empty output it groups 'OPack's by input+-- constructor name, unions the recovered slots, and classifies misses as absent+-- from the union or present only after the head event (first-seen order,+-- deterministic).+hiddenInputReasons ::+  forall phi rs ci co s. Edge phi rs ci co s -> [HiddenInputReason]+hiddenInputReasons e = case output e of+  []+    | edgeReadsInput e -> [HirEpsilonReadsInput]+    | otherwise -> []+  outs@(headOut : _) -> concatMap (reasonsFor headOut) (groupByInCtorName outs)+  where+    reasonsFor ::+      OutTerm rs ci co ->+      (String, [String], [String]) ->+      [HiddenInputReason]+    reasonsFor headOut (icN, allSlots, visitedUnion) =+      [HirUnionMiss icN missingFromUnion | not (null missingFromUnion)]+        ++ [HirHeadUnrecoverable icN tailOnly | not (null tailOnly)]+      where+        missingFromUnion = allSlots \\ nub visitedUnion+        missingFromHead = case headOut of+          OPack headIc _ headFields+            | icName headIc == icN ->+                maybe [] mifMissing (detectMissingInCtorFields headIc headFields)+            | otherwise -> allSlots+        tailOnly = missingFromHead \\ missingFromUnion++    -- Walk the output list, accumulating per-InCtor (slot list, visited+    -- slots). First seen wins on the slot list; subsequent OPacks with the+    -- same InCtor name extend the visited list.+    groupByInCtorName ::+      [OutTerm rs ci co] -> [(String, [String], [String])]+    groupByInCtorName = foldl add []+      where+        add acc (OPack ic _ fields) =+          let icN = icName ic+              allSl = slotNamesOf ic+              visited = visitedSlotsOf ic fields+           in extend acc icN allSl visited++        extend [] icN allSl visited = [(icN, allSl, visited)]+        extend ((n, sl, v) : rest) icN allSl visited+          | n == icN = (n, sl, v ++ visited) : rest+          | otherwise = (n, sl, v) : extend rest icN allSl visited++    -- Slots of an OPack's named 'InCtor' that the supplied 'OutFields' walk+    -- recovers via a /top-level/ 'TInpCtorField'. Since EP-47 this does NOT+    -- descend into derived ('TApp1'\/'TApp2'\/'TArith') terms: a slot read+    -- only inside a derived field is a /hidden input/, so it is reported+    -- missing rather than counted as covered.+    visitedSlotsOf ::+      forall ifs fs.+      InCtor ci ifs -> OutFields rs ci ifs fs -> [String]+    visitedSlotsOf ic@InCtor {} fields = goFields fields+      where+        allSlots = slotNamesOf ic++        goFields :: forall fs'. OutFields rs ci ifs fs' -> [String]+        goFields OFNil = []+        goFields (OFCons tt rest) = goTerm tt ++ goFields rest++        goTerm :: forall r. Term rs ci ifs r -> [String]+        goTerm (TInpCtorField ic2 ix)+          | icName ic2 == icName ic =+              [allSlots !! indexPos ix]+          | otherwise = []+        goTerm _ = [] -- do not descend into derived terms+        indexPos :: forall rs' r. Index rs' r -> Int+        indexPos ZIdx = 0+        indexPos (SIdx i) = 1 + indexPos i++-- | Format a 'HiddenInputReason' into the legacy 'HiddenInputWarning' reason+-- string. The output is byte-identical to the pre-refactor 'checkHiddenInputs'+-- text so existing consumers and tests are unaffected.+formatHiddenInputReason :: Int -> HiddenInputReason -> String+formatHiddenInputReason n HirEpsilonReadsInput =+  "edge #" <> show n <> ": ε-edge with input read in update"+formatHiddenInputReason n (HirUnionMiss icN missing) =+  "edge #"+    <> show n+    <> ": OPack walk for InCtor \""+    <> icN+    <> "\" leaves field"+    <> (if length missing == 1 then " " else "s ")+    <> "{"+    <> showMissing missing+    <> "} unrecovered"+  where+    showMissing :: [String] -> String+    showMissing [] = ""+    showMissing [x] = "\"" <> x <> "\""+    showMissing (x : xs) = "\"" <> x <> "\", " <> showMissing xs+formatHiddenInputReason n (HirHeadUnrecoverable icN missing) =+  "edge #"+    <> show n+    <> ": head event does not recover InCtor \""+    <> icN+    <> "\" field"+    <> (if length missing == 1 then " " else "s ")+    <> "{"+    <> showMissing missing+    <> "}; the data appears only in later events of this edge, which replay cannot invert - move the field(s) into the FIRST emitted event"+  where+    showMissing :: [String] -> String+    showMissing [] = ""+    showMissing [x] = "\"" <> x <> "\""+    showMissing (x : xs) = "\"" <> x <> "\", " <> showMissing xs++-- | Does the 'Update' read the input symbol via 'TInpCtorField'?+updateReadsInput :: Update rs w ci -> Bool+updateReadsInput UKeep = False+updateReadsInput (USet _ t) = termReadsInput t+updateReadsInput (UCombine a b) = updateReadsInput a || updateReadsInput b++-- | Does the 'Term' read the input symbol via 'TInpCtorField'?+termReadsInput :: Term rs ci ifs r -> Bool+termReadsInput (TLit _) = False+termReadsInput (TReg _) = False+termReadsInput (TInpCtorField _ _) = True+termReadsInput (TApp1 _ t) = termReadsInput t+termReadsInput (TApp2 _ a b) = termReadsInput a || termReadsInput b+termReadsInput (TArith _ a b) = termReadsInput a || termReadsInput b++-- | Do the 'OutFields' contain a 'TInpCtorField' read anywhere?+outFieldsHaveInpCtorField :: OutFields rs ci ifs fs -> Bool+outFieldsHaveInpCtorField OFNil = False+outFieldsHaveInpCtorField (OFCons t rest) =+  termHasInpCtorField t || outFieldsHaveInpCtorField rest+  where+    termHasInpCtorField :: Term rs ci ifs r -> Bool+    termHasInpCtorField (TLit _) = False+    termHasInpCtorField (TReg _) = False+    termHasInpCtorField (TInpCtorField _ _) = True+    termHasInpCtorField (TApp1 _ t') = termHasInpCtorField t'+    termHasInpCtorField (TApp2 _ a b) = termHasInpCtorField a || termHasInpCtorField b+    termHasInpCtorField (TArith _ a b) = termHasInpCtorField a || termHasInpCtorField b++-- | The result of 'detectMissingInCtorFields': the offending 'InCtor'+-- name plus the names of slots its 'OutFields' walk does not visit.+data MissingInCtorFields = MissingInCtorFields+  { mifIcName :: String,+    mifMissing :: [String]+  }+  deriving (Eq, Show)++-- | Given the 'InCtor' an 'OPack' is tagged with and that 'OPack'\'s+-- 'OutFields', return the field names of the 'InCtor' that the+-- 'OutFields' walk does not visit. 'Nothing' means every slot of the+-- 'InCtor' is visited. The slot list comes from the 'InCtor' itself+-- (via 'KnownSlotNames'), not from any 'TInpCtorField' inside the+-- 'OutFields' — this lets us flag empty 'OutFields' against a non-+-- empty 'InCtor' as well.+detectMissingInCtorFields ::+  forall rs ci ifs fs.+  InCtor ci ifs ->+  OutFields rs ci ifs fs ->+  Maybe MissingInCtorFields+detectMissingInCtorFields ic@InCtor {} fields =+  case allSlots \\ nub visited of+    [] -> Nothing+    missing -> Just (MissingInCtorFields (icName ic) missing)+  where+    allSlots = slotNamesOf ic+    visited = goFields fields++    goFields :: forall fs'. OutFields rs ci ifs fs' -> [String]+    goFields OFNil = []+    goFields (OFCons t rest) = goTerm t ++ goFields rest++    goTerm :: forall r. Term rs ci ifs r -> [String]+    goTerm (TInpCtorField ic2 ix)+      | icName ic2 == icName ic =+          [allSlots !! indexPos ix]+      | otherwise = []+    goTerm _ = [] -- EP-47: top-level reads only; derived+    -- (TApp/TArith) terms are not descended+    -- into, so a slot read only inside one is+    -- reported missing (a hidden input).+    indexPos :: forall rs' r. Index rs' r -> Int+    indexPos ZIdx = 0+    indexPos (SIdx i) = 1 + indexPos i++-- | Read the slot-name list out of an 'InCtor' (uses the+-- 'KnownSlotNames' instance carried by the data constructor).+slotNamesOf :: forall ci ifs. InCtor ci ifs -> [String]+slotNamesOf InCtor {} = slotNames @ifs++-- * Build-time validation umbrella (EP-56) --------------------------------++-- | A structured build-time validation warning, parameterized over the+-- vertex type @s@ so it carries the real source vertex rather than a+-- pre-stringified one. It reuses the canonical 'EdgeRef' locator owned by EP-55+-- (the runtime explainer 'stepEither'), so the runtime and build-time+-- diagnostics speak one vocabulary.+--+-- Produced by 'validateTransducer'. The warning constructors cover replay+-- recoverability, safe input reads, deterministic inversion, and structural+-- reachability.+data TransducerValidationWarning s+  = -- | An edge consumes command information that its output does not+    --       emit, so the command cannot be reconstructed on replay.+    HiddenInput+      { tvwEdge :: EdgeRef s,+        -- | input constructor name, when known+        tvwInCtor :: Maybe String,+        -- | slot/field names left off the wire+        tvwMissingSlots :: [String],+        -- | human-readable summary+        tvwDetail :: String+      }+  | -- | A multi-event edge whose first event cannot recover all command+    --       fields even though later events carry the missing data. Streaming+    --       replay inverts only the first event, so the edge produces a log it+    --       cannot replay.+    HeadUnrecoverable+      { tvwEdge :: EdgeRef s,+        tvwInCtor :: Maybe String,+        tvwTailOnlySlots :: [String],+        tvwDetail :: String+      }+  | -- | Two outgoing edges use the same wire constructor for their first+    --       event. Replay requires a unique inverting edge, so the observed+    --       event may reconstruct commands for both edges and become ambiguous.+    InversionAmbiguity+      { tvwSource :: s,+        tvwEdgeA :: Int,+        tvwEdgeB :: Int,+        tvwWireCtor :: String,+        tvwDetail :: String+      }+  | -- | An edge reads a field of an input constructor without first+    --       establishing the matching top-level 'PInCtor' guard. A different+    --       command can reach the read and make 'evalTerm' throw.+    UnguardedInputRead+      { tvwEdge :: EdgeRef s,+        tvwInCtor :: Maybe String,+        tvwDetail :: String+      }+  | -- | An output-free edge changes control state or can write registers.+    --       Persisting only emitted events loses that transition, so replay of+    --       the resulting log cannot reproduce the forward state.+    StateChangingEpsilon+      { tvwEdge :: EdgeRef s,+        tvwChangesVertex :: Bool,+        tvwWritesRegisters :: Bool,+        tvwDetail :: String+      }+  | -- | Two outgoing edges of the same vertex whose guards can both hold+    --       for one command — a runtime nondeterminism / single-valuedness+    --       violation (its dynamic witness is EP-55's @AmbiguousEdges@).+    NondeterministicPair+      { tvwSource :: s,+        tvwEdgeA :: Int,+        tvwEdgeB :: Int,+        tvwInCtor :: Maybe String,+        tvwDetail :: String+      }+  | -- | An edge that can never fire: its source vertex is unreachable+    --       from 'initial', or its guard is statically unsatisfiable. Labelled+    --       "possibly" because the structural pass is conservative.+    PossiblyDeadEdge+      { tvwEdge :: EdgeRef s,+        tvwDetail :: String+      }+  | -- | An edge whose guard contains an opaque 'TApp' term. The symbolic+    --       single-valuedness and dead-edge analyses translate such a term to an+    --       unconstrained free variable ('Keiki.Symbolic.translateTermSym' emits+    --       @SBV.free "app1"@), so they cannot see through the guard and silently+    --       under-verify it. Most often this is a collection-content condition+    --       (membership, "all resolved", size) lifted through a closure because the+    --       structural predicate language has no node for it; see the user guide and+    --       @docs\/plans\/60-first-class-collection-registers-design-gated.md@ for the+    --       options. Advisory, not a soundness error: opt in via 'warnOpaqueGuards'.+    OpaqueGuard+      { tvwEdge :: EdgeRef s,+        tvwDetail :: String+      }+  deriving stock (Eq, Show)++-- | Which checks 'validateTransducer' runs. Construct options by updating+-- 'defaultValidationOptions'; new fields are added as new checks land.+data ValidationOptions = ValidationOptions+  { -- | run the hidden-input check+    failOnEpsilonReadsInput :: Bool,+    -- | run the (pure, structural) determinism check+    checkDeterminism :: Bool,+    -- | run the (structural) dead-edge check+    checkReachability :: Bool,+    -- | run the opaque-guard audit (opt-in; default off). Flags edges whose+    --     guard branches on an opaque 'TApp' term the symbolic analyses cannot+    --     see through. Off by default so 'defaultValidationOptions' keeps its+    --     meaning for existing consumers.+    warnOpaqueGuards :: Bool,+    -- | require the first emitted event to recover every command field used+    --     by replay+    checkHeadRecoverability :: Bool,+    -- | conservatively flag outgoing edge pairs with the same head wire+    --     constructor+    checkInversionAmbiguity :: Bool,+    -- | require every input-field read to be protected by an earlier matching+    --     constructor guard+    checkGuardImpliesInputRead :: Bool,+    -- | reject output-free edges that change vertex or can write registers.+    --     Never disable this for a transducer whose events are persisted:+    --     downstream durable boundaries must force-enable it rather than let+    --     callers opt out.+    checkStateChangingEpsilon :: Bool+  }+  deriving stock (Eq, Show)++-- | Replay-safety checks enabled; the advisory opaque-guard audit off.+defaultValidationOptions :: ValidationOptions+defaultValidationOptions =+  ValidationOptions+    { failOnEpsilonReadsInput = True,+      checkDeterminism = True,+      checkReachability = True,+      warnOpaqueGuards = False,+      checkHeadRecoverability = True,+      checkInversionAmbiguity = True,+      checkGuardImpliesInputRead = True,+      checkStateChangingEpsilon = True+    }++-- | The build-time validation umbrella. Runs the enabled checks over the+-- 'HsPred' (syntactic, /no solver/) carrier and concatenates their structured+-- warnings, so a project can put @validateTransducer defaultValidationOptions t+-- == []@ directly in a unit test and have it pass or fail in microseconds with+-- no external z3 process.+--+-- Subject to honest 'InCtor' and 'WireCtor' implementations, a transducer for+-- which this returns @[]@ under 'defaultValidationOptions' can replay every log+-- it produces via 'reconstitute'. 'HeadUnrecoverable',+-- 'InversionAmbiguity', 'UnguardedInputRead', and+-- 'StateChangingEpsilon' exist to align build-time acceptance with the+-- head-first semantics of 'applyEventStreaming'. Disabling those checks weakens+-- that replay guarantee.+--+-- The default path is deliberately specialised to the 'HsPred' carrier and is+-- /cheap and pure/: the determinism component flags only structurally-provable+-- overlaps in conjunction spines containing constructor tests and+-- variable-versus-literal comparisons. It uses exact interval reasoning for+-- integral variables and concrete literal witnesses for other types. Disjunction,+-- negation, arithmetic, opaque terms, variable-versus-variable comparisons, and+-- non-integral strict-bound density remain unknown and produce no pure warning.+-- The pass therefore has no false positives but can miss overlaps outside that+-- fragment. The dead-edge component is structural reachability plus a literal-+-- 'PBot' check. For the exact, solver-backed answers use+-- 'Keiki.Symbolic.checkTransitionDeterminismSym' and+-- 'Keiki.Symbolic.checkDeadEdgesSym' directly.+validateTransducer ::+  (Bounded s, Enum s, Ord s, Show s) =>+  ValidationOptions ->+  SymTransducer (HsPred rs ci) rs s ci co ->+  [TransducerValidationWarning s]+validateTransducer opts t =+  concat+    [ if failOnEpsilonReadsInput opts then hiddenInputWarnings t else [],+      if checkHeadRecoverability opts then headRecoverabilityWarnings t else [],+      if checkInversionAmbiguity opts then inversionAmbiguityWarnings t else [],+      if checkGuardImpliesInputRead opts then guardImpliesInputReadWarnings t else [],+      if checkStateChangingEpsilon opts then stateChangingEpsilonWarnings t else [],+      if checkDeterminism opts then determinismWarnings t else [],+      if checkReachability opts+        then+          [ PossiblyDeadEdge (dewEdge w) (dewReason w)+          | w <- checkDeadEdges defaultDeadEdgeOptions t+          ]+        else [],+      if warnOpaqueGuards opts then opaqueGuardWarnings t else []+    ]++-- | Structured form of the hidden-input check, additive over+-- 'checkHiddenInputs'. Reuses the same per-edge analysis ('hiddenInputReasons')+-- and lifts each result into a 'TransducerValidationWarning' carrying the typed+-- source vertex (via 'EdgeRef'), the input-constructor name, and the missing+-- slot names — data a downstream project can pattern-match on rather than parse+-- out of a string.+hiddenInputWarnings ::+  (Bounded s, Enum s) =>+  SymTransducer phi rs s ci co ->+  [TransducerValidationWarning s]+hiddenInputWarnings t =+  [ HiddenInput+      { tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},+        tvwInCtor = inCtorOf r,+        tvwMissingSlots = missingSlotsOf r,+        tvwDetail = formatHiddenInputReason n r+      }+  | s <- [minBound .. maxBound],+    (n, e) <- zip [(0 :: Int) ..] (edgesOut t s),+    r <- hiddenInputReasons e,+    isHiddenReason r+  ]+  where+    inCtorOf (HirUnionMiss icN _) = Just icN+    inCtorOf HirEpsilonReadsInput = Nothing+    inCtorOf (HirHeadUnrecoverable _ _) = Nothing+    missingSlotsOf (HirUnionMiss _ ms) = ms+    missingSlotsOf HirEpsilonReadsInput = []+    missingSlotsOf (HirHeadUnrecoverable _ _) = []+    isHiddenReason HirEpsilonReadsInput = True+    isHiddenReason (HirUnionMiss _ _) = True+    isHiddenReason (HirHeadUnrecoverable _ _) = False++-- | Warn when a multi-event edge's head event cannot alone recover command+-- fields that appear later in the same output chain. 'applyEventStreaming'+-- inverts only the head output; tail events are equality-checked after the edge+-- has already been selected.+headRecoverabilityWarnings ::+  (Bounded s, Enum s) =>+  SymTransducer phi rs s ci co ->+  [TransducerValidationWarning s]+headRecoverabilityWarnings t =+  [ HeadUnrecoverable+      { tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},+        tvwInCtor = Just icN,+        tvwTailOnlySlots = missing,+        tvwDetail = formatHiddenInputReason n reason+      }+  | s <- [minBound .. maxBound],+    (n, e) <- zip [(0 :: Int) ..] (edgesOut t s),+    reason@(HirHeadUnrecoverable icN missing) <- hiddenInputReasons e+  ]++-- ** Opaque-guard diagnostics++-- | Does the term contain an opaque 'TApp1'\/'TApp2' anywhere? Mirrors the+-- structural recursion of 'termReadsInput'; 'TArith' is transparent, so it+-- recurses into its operands rather than counting as opaque.+termHasOpaqueApp :: Term rs ci ifs r -> Bool+termHasOpaqueApp (TLit _) = False+termHasOpaqueApp (TReg _) = False+termHasOpaqueApp (TInpCtorField _ _) = False+termHasOpaqueApp (TApp1 _ _) = True+termHasOpaqueApp (TApp2 _ _ _) = True+termHasOpaqueApp (TArith _ a b) = termHasOpaqueApp a || termHasOpaqueApp b++-- | Does the guard predicate branch on an opaque term anywhere? The symbolic+-- analyses cannot see through such a guard (it becomes a free SBV variable),+-- so they silently under-verify the edge.+predHasOpaqueTerm :: HsPred rs ci -> Bool+predHasOpaqueTerm PTop = False+predHasOpaqueTerm PBot = False+predHasOpaqueTerm (PAnd p q) = predHasOpaqueTerm p || predHasOpaqueTerm q+predHasOpaqueTerm (POr p q) = predHasOpaqueTerm p || predHasOpaqueTerm q+predHasOpaqueTerm (PNot p) = predHasOpaqueTerm p+predHasOpaqueTerm (PEq a b) = termHasOpaqueApp a || termHasOpaqueApp b+predHasOpaqueTerm (PInCtor _) = False+predHasOpaqueTerm PLeftArm = False+predHasOpaqueTerm PRightArm = False+predHasOpaqueTerm (PCmp _ a b) = termHasOpaqueApp a || termHasOpaqueApp b++-- | The opt-in opaque-guard audit (run by 'validateTransducer' only when+-- 'warnOpaqueGuards' is set). For every edge whose guard contains an opaque+-- 'TApp' term, emit an 'OpaqueGuard' warning locating the edge by its typed+-- 'EdgeRef'. Specialised to the 'HsPred' carrier because it walks the predicate+-- AST, exactly as 'validateTransducer' is.+opaqueGuardWarnings ::+  (Bounded s, Enum s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  [TransducerValidationWarning s]+opaqueGuardWarnings t =+  [ OpaqueGuard+      { tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},+        tvwDetail =+          "guard contains an opaque TApp term the symbolic analyses cannot "+            ++ "see through; its single-valuedness was not verified"+      }+  | s <- [minBound .. maxBound],+    (n, e) <- zip [(0 :: Int) ..] (edgesOut t s),+    predHasOpaqueTerm (guard e)+  ]++-- ** Guarded input-read diagnostics++termInCtorNames :: Term rs ci ifs r -> [String]+termInCtorNames (TLit _) = []+termInCtorNames (TReg _) = []+termInCtorNames (TInpCtorField ic _) = [icName ic]+termInCtorNames (TApp1 _ t) = termInCtorNames t+termInCtorNames (TApp2 _ a b) = termInCtorNames a ++ termInCtorNames b+termInCtorNames (TArith _ a b) = termInCtorNames a ++ termInCtorNames b++predInCtorReadNames :: HsPred rs ci -> [String]+predInCtorReadNames PTop = []+predInCtorReadNames PBot = []+predInCtorReadNames (PAnd p q) = predInCtorReadNames p ++ predInCtorReadNames q+predInCtorReadNames (POr p q) = predInCtorReadNames p ++ predInCtorReadNames q+predInCtorReadNames (PNot p) = predInCtorReadNames p+predInCtorReadNames (PEq a b) = termInCtorNames a ++ termInCtorNames b+predInCtorReadNames (PInCtor _) = []+predInCtorReadNames PLeftArm = []+predInCtorReadNames PRightArm = []+predInCtorReadNames (PCmp _ a b) = termInCtorNames a ++ termInCtorNames b++updateInCtorNames :: Update rs w ci -> [String]+updateInCtorNames UKeep = []+updateInCtorNames (USet _ term) = termInCtorNames term+updateInCtorNames (UCombine a b) = updateInCtorNames a ++ updateInCtorNames b++outFieldsInCtorNames :: OutFields rs ci ifs fs -> [String]+outFieldsInCtorNames OFNil = []+outFieldsInCtorNames (OFCons term rest) =+  termInCtorNames term ++ outFieldsInCtorNames rest++outTermInCtorNames :: OutTerm rs ci co -> [String]+outTermInCtorNames (OPack _ _ fields) = outFieldsInCtorNames fields++-- | Check that every 'TInpCtorField' read is protected by a matching+-- top-level 'PInCtor' conjunct. Guard reads are order-sensitive: the guard is+-- walked along its top-level 'PAnd' spine from left to right, matching Haskell's+-- lazy @(&&)@ evaluation. A constructor established to the right of a read is+-- too late. Reads in updates and outputs run after the complete guard succeeds,+-- so any constructor established on the spine protects them.+--+-- 'POr', 'PNot', comparisons, and nested boolean forms establish nothing; a+-- constructor atom inside them does not imply that the whole guard matched that+-- constructor. Builder 'onCmd' edges are safe by construction because their+-- guard starts with the appropriate 'PInCtor'. An unsatisfiable conjunction of+-- different constructors may pass this crash-safety check and is left to the+-- dead-edge analyses.+guardImpliesInputReadWarnings ::+  forall rs s ci co.+  (Bounded s, Enum s, Show s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  [TransducerValidationWarning s]+guardImpliesInputReadWarnings t =+  [ UnguardedInputRead+      { tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},+        tvwInCtor = Just icN,+        tvwDetail =+          location+            <> " reads InCtor \""+            <> icN+            <> "\" but edge #"+            <> show n+            <> " out of "+            <> show s+            <> " does not establish PInCtor \""+            <> icN+            <> "\" before it; a non-\""+            <> icN+            <> "\" command reaching this edge crashes instead of being rejected"+      }+  | s <- [minBound .. maxBound],+    (n, edge) <- zip [(0 :: Int) ..] (edgesOut t s),+    (icN, location) <- edgeViolations edge+  ]+  where+    edgeViolations :: Edge (HsPred rs ci) rs ci co s -> [(String, String)]+    edgeViolations Edge {guard = edgeGuard, update = edgeUpdate, output = edgeOutput} =+      nub (guardViolations ++ updateViolations ++ outputViolations)+      where+        (guardViolations, established) = checkGuard [] edgeGuard+        updateViolations =+          [ (icN, "update")+          | icN <- nub (updateInCtorNames edgeUpdate),+            icN `notElem` established+          ]+        outputViolations =+          [ (icN, "output")+          | icN <- nub (concatMap outTermInCtorNames edgeOutput),+            icN `notElem` established+          ]++    checkGuard :: [String] -> HsPred rs ci -> ([(String, String)], [String])+    checkGuard established (PAnd p q) =+      let (leftViolations, afterLeft) = checkGuard established p+          (rightViolations, afterRight) = checkGuard afterLeft q+       in (leftViolations ++ rightViolations, afterRight)+    checkGuard established (PInCtor ic) =+      ([], nub (established ++ [icName ic]))+    checkGuard established predicate =+      ( [ (icN, "guard")+        | icN <- nub (predInCtorReadNames predicate),+          icN `notElem` established+        ],+        established+      )++-- ** State-changing epsilon diagnostics++updateWritesRegisters :: Update rs w ci -> Bool+updateWritesRegisters UKeep = False+updateWritesRegisters USet {} = True+updateWritesRegisters (UCombine a b) =+  updateWritesRegisters a || updateWritesRegisters b++-- | Flag output-free edges that change control state or are structurally+-- capable of writing registers. Such an edge can be meaningful when a+-- transducer is used only as an in-memory state machine, but it is not durable:+-- persisting the empty output loses the transition and replay cannot reproduce+-- its result.+--+-- Control-state detection is exact. Register detection is conservative:+-- 'USet', or any 'UCombine' containing one, warns even when a particular write+-- happens to store the value already present. A self-loop with 'UKeep' remains+-- clean.+stateChangingEpsilonWarnings ::+  forall rs s ci co.+  (Bounded s, Enum s, Eq s, Show s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  [TransducerValidationWarning s]+stateChangingEpsilonWarnings t =+  [ StateChangingEpsilon+      { tvwEdge = EdgeRef {edgeSource = source, edgeIndex = edgeNumber},+        tvwChangesVertex = changesVertex,+        tvwWritesRegisters = writesRegisters,+        tvwDetail =+          "output-free edge #"+            <> show edgeNumber+            <> " out of "+            <> show source+            <> changeSummary changesVertex writesRegisters+            <> "; persisted replay cannot reproduce that transition without an emitted event"+      }+  | source <- [minBound .. maxBound],+    (edgeNumber, Edge {update = edgeUpdate, output = edgeOutput, target = edgeTarget}) <-+      zip [(0 :: Int) ..] (edgesOut t source),+    null edgeOutput,+    let changesVertex = edgeTarget /= source,+    let writesRegisters = updateWritesRegisters edgeUpdate,+    changesVertex || writesRegisters+  ]+  where+    changeSummary True True = " changes vertex and can write registers"+    changeSummary True False = " changes vertex"+    changeSummary False True = " can write registers"+    changeSummary False False = ""++-- ** Replay inversion diagnostics++-- | Conservatively flag pairs of outgoing edges whose first emitted events+-- use the same 'WireCtor' name. Replay selects an edge by inverting one observed+-- head event, so both edges may reconstruct their own commands and satisfy their+-- own guards even when forward command dispatch is deterministic.+--+-- This structural check intentionally over-approximates ambiguity. It cannot+-- prove semantic guard disjointness over recovered values or registers; it+-- cannot compare differing 'TLit' values because 'TLit' carries no 'Eq' or+-- 'Typeable' evidence; and it does not predict derived-field verification in+-- 'solveOutput'. It ignores tail events because replay equality-checks rather+-- than inverts them. Different head constructor names are safe under the+-- documented honesty law of 'wcMatch'. Literal-'PBot' guards are exempt because+-- such an edge cannot participate in a successful inversion.+inversionAmbiguityWarnings ::+  forall rs s ci co.+  (Bounded s, Enum s, Show s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  [TransducerValidationWarning s]+inversionAmbiguityWarnings t =+  [ InversionAmbiguity+      { tvwSource = s,+        tvwEdgeA = i,+        tvwEdgeB = j,+        tvwWireCtor = wireName,+        tvwDetail =+          "edges #"+            <> show i+            <> " and #"+            <> show j+            <> " out of "+            <> show s+            <> " both emit \""+            <> wireName+            <> "\" as their first event; replay may not be able to attribute an observed \""+            <> wireName+            <> "\" to a unique edge"+      }+  | s <- [minBound .. maxBound],+    let indexedEdges = zip [(0 :: Int) ..] (edgesOut t s),+    (i, e1) <- indexedEdges,+    (j, e2) <- indexedEdges,+    i < j,+    not (isBot (guard e1) || isBot (guard e2)),+    Just wireName <- [headWireName e1],+    Just otherWireName <- [headWireName e2],+    wireName == otherWireName+  ]+  where+    headWireName :: Edge (HsPred rs ci) rs ci co s -> Maybe String+    headWireName Edge {output = OPack _ wire _ : _} = Just (wcName wire)+    headWireName _ = Nothing++-- ** Determinism diagnostics++-- | A determinism warning: two outgoing edges of the same vertex whose guards+-- can both hold. Carries both edge indices and the (typed) source vertex.+data DeterminismWarning s = DeterminismWarning+  { dwSource :: s,+    -- | first overlapping edge index+    dwEdgeA :: Int,+    -- | second overlapping edge index+    dwEdgeB :: Int,+    dwDetail :: String+  }+  deriving stock (Eq, Show)++-- | Per-vertex, per-pair determinism diagnostic. Reuses the exact pairing+-- structure of 'Keiki.Symbolic.isSingleValuedSym': for every vertex, for every+-- pair @(i,e1),(j,e2)@ with @i<j@, the pair is ambiguous when+-- @guard e1 \`conj\` guard e2@ is /not/ 'isBot'. So+-- @checkTransitionDeterminism t == []@ iff @isSingleValuedSym t@ under the same+-- carrier.+--+-- Soundness direction: with the pure 'HsPred' carrier, 'isBot' only recognises+-- the literal 'PBot', so @not (isBot (a \`conj\` b))@ holds for /every/ non-'PBot'+-- pair — i.e. this polymorphic check over-approximates overlap on the 'HsPred'+-- carrier (it would flag almost every multi-edge vertex). It is intended to be+-- run over the /symbolic/ 'SymPred' carrier (via+-- 'Keiki.Symbolic.checkTransitionDeterminismSym'), whose 'isBot' is exact. For+-- the pure path 'validateTransducer' uses the under-approximating+-- 'checkTransitionDeterminismPure' instead, which flags only true positives.+checkTransitionDeterminism ::+  forall phi rs s ci co.+  (BoolAlg phi (RegFile rs, ci), Bounded s, Enum s, Show s) =>+  SymTransducer phi rs s ci co ->+  [DeterminismWarning s]+checkTransitionDeterminism t =+  [ DeterminismWarning+      { dwSource = s,+        dwEdgeA = i,+        dwEdgeB = j,+        dwDetail = overlapDetail i j s+      }+  | s <- [minBound .. maxBound],+    let ies = zip [(0 :: Int) ..] (edgesOut t s),+    (i, e1) <- ies,+    (j, e2) <- ies,+    i < j,+    not (isBot (guard e1 `conj` guard e2))+  ]++-- | Over-approximation-free determinism check for the pure 'HsPred' carrier.+-- It proves overlap through conjunction spines containing 'PTop', compatible+-- 'PInCtor' atoms, and variable-versus-literal equality or ordering atoms.+-- Integral variables ('Int', 'Integer', fixed-width words and signed integers)+-- use exact interval intersection; other types require one of the mentioned+-- literals to be a concrete witness. Disjunction, negation, structural+-- arithmetic, opaque terms, variable-versus-variable comparisons, and strict+-- non-integral bounds are outside the fragment and produce no warning. Used by+-- 'validateTransducer' so every warning is a true positive. Absence does not+-- prove determinism; run 'Keiki.Symbolic.checkTransitionDeterminismSym' for the+-- exact solver-backed answer.+checkTransitionDeterminismPure ::+  forall rs s ci co.+  (Bounded s, Enum s, Show s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  [DeterminismWarning s]+checkTransitionDeterminismPure t =+  [ DeterminismWarning+      { dwSource = s,+        dwEdgeA = i,+        dwEdgeB = j,+        dwDetail = overlapDetail i j s+      }+  | s <- [minBound .. maxBound],+    let ies = zip [(0 :: Int) ..] (edgesOut t s),+    (i, e1) <- ies,+    (j, e2) <- ies,+    i < j,+    provablyOverlap (guard e1) (guard e2)+  ]++overlapDetail :: (Show s) => Int -> Int -> s -> String+overlapDetail i j s =+  "edges #"+    <> show i+    <> " and #"+    <> show j+    <> " out of "+    <> show s+    <> " have overlapping guards"++-- | A named variable in the pure overlap fragment. Register and input-field+-- namespaces are distinct. Input fields retain their constructor name so a+-- witness is accepted only when a matching 'PInCtor' atom is present.+data PureVariable = PureVariable+  { pureVariableName :: String,+    pureVariableInputCtor :: Maybe String+  }+  deriving stock (Eq, Show)++data PureRelation = PureEq | PureLt | PureLe | PureGt | PureGe+  deriving stock (Eq, Show)++-- | One normalized @variable relation literal@ atom. The predicate closure+-- captures the source constructor's real 'Eq' or 'Ord' dictionary for concrete+-- literal-witness probing.+data PureComparison where+  PureComparison ::+    (Typeable r) =>+    PureVariable ->+    PureRelation ->+    r ->+    (r -> Bool) ->+    PureComparison++data PureGuard = PureGuard+  { pureGuardConstructors :: [String],+    pureGuardComparisons :: [PureComparison]+  }++data PureFragment+  = PureUnknown+  | PureUnsatisfiable+  | PureKnown PureGuard++emptyPureGuard :: PureGuard+emptyPureGuard = PureGuard [] []++-- | Parse the exact, deliberately small fragment accepted by+-- 'provablyOverlap'.+pureFragment :: HsPred rs ci -> PureFragment+pureFragment PTop = PureKnown emptyPureGuard+pureFragment PBot = PureUnsatisfiable+pureFragment (PAnd a b) = mergePureFragments (pureFragment a) (pureFragment b)+pureFragment (PInCtor ic) =+  PureKnown emptyPureGuard {pureGuardConstructors = [icName ic]}+pureFragment (PEq a b) = pureEquality a b+pureFragment (PCmp relation a b) = pureOrdering relation a b+pureFragment PLeftArm = PureUnknown+pureFragment PRightArm = PureUnknown+pureFragment (POr _ _) = PureUnknown+pureFragment (PNot _) = PureUnknown++mergePureFragments :: PureFragment -> PureFragment -> PureFragment+mergePureFragments PureUnsatisfiable _ = PureUnsatisfiable+mergePureFragments _ PureUnsatisfiable = PureUnsatisfiable+mergePureFragments PureUnknown _ = PureUnknown+mergePureFragments _ PureUnknown = PureUnknown+mergePureFragments (PureKnown a) (PureKnown b) =+  PureKnown+    PureGuard+      { pureGuardConstructors =+          pureGuardConstructors a <> pureGuardConstructors b,+        pureGuardComparisons =+          pureGuardComparisons a <> pureGuardComparisons b+      }++pureEquality ::+  forall rs ci ifs1 ifs2 r.+  (Eq r, Typeable r) =>+  Term rs ci ifs1 r ->+  Term rs ci ifs2 r ->+  PureFragment+pureEquality (TLit a) (TLit b)+  | a == b = PureKnown emptyPureGuard+  | otherwise = PureUnsatisfiable+pureEquality variable (TLit literalValue)+  | Just name <- pureVariable variable =+      knownComparison name PureEq literalValue (== literalValue)+pureEquality (TLit literalValue) variable+  | Just name <- pureVariable variable =+      knownComparison name PureEq literalValue (== literalValue)+pureEquality _ _ = PureUnknown++pureOrdering ::+  forall rs ci ifs1 ifs2 r.+  (Ord r, Typeable r) =>+  Cmp ->+  Term rs ci ifs1 r ->+  Term rs ci ifs2 r ->+  PureFragment+pureOrdering relation (TLit a) (TLit b)+  | applyPureCmp relation a b = PureKnown emptyPureGuard+  | otherwise = PureUnsatisfiable+pureOrdering relation variable (TLit literalValue)+  | Just name <- pureVariable variable =+      let normalized = pureRelation relation+       in knownComparison+            name+            normalized+            literalValue+            (\value -> applyPureRelation normalized value literalValue)+pureOrdering relation (TLit literalValue) variable+  | Just name <- pureVariable variable =+      let normalized = flipPureRelation (pureRelation relation)+       in knownComparison+            name+            normalized+            literalValue+            (\value -> applyPureRelation normalized value literalValue)+pureOrdering _ _ _ = PureUnknown++knownComparison ::+  (Typeable r) =>+  PureVariable ->+  PureRelation ->+  r ->+  (r -> Bool) ->+  PureFragment+knownComparison variable relation literalValue accepts =+  PureKnown+    emptyPureGuard+      { pureGuardComparisons =+          [PureComparison variable relation literalValue accepts]+      }++pureVariable :: Term rs ci ifs r -> Maybe PureVariable+pureVariable (TReg index) =+  Just (PureVariable ("reg/" <> pureIndexName index) Nothing)+pureVariable (TInpCtorField ic index) =+  Just+    ( PureVariable+        ("inp/" <> icName ic <> "/" <> pureIndexName index)+        (Just (icName ic))+    )+pureVariable _ = Nothing++pureIndexName :: forall rs r. Index rs r -> String+pureIndexName (ZIdx @name) = symbolVal (Proxy @name)+pureIndexName (SIdx index) = pureIndexName index++pureRelation :: Cmp -> PureRelation+pureRelation CmpLt = PureLt+pureRelation CmpLe = PureLe+pureRelation CmpGt = PureGt+pureRelation CmpGe = PureGe++flipPureRelation :: PureRelation -> PureRelation+flipPureRelation PureEq = PureEq+flipPureRelation PureLt = PureGt+flipPureRelation PureLe = PureGe+flipPureRelation PureGt = PureLt+flipPureRelation PureGe = PureLe++applyPureCmp :: (Ord r) => Cmp -> r -> r -> Bool+applyPureCmp CmpLt = (<)+applyPureCmp CmpLe = (<=)+applyPureCmp CmpGt = (>)+applyPureCmp CmpGe = (>=)++applyPureRelation :: (Ord r) => PureRelation -> r -> r -> Bool+applyPureRelation PureEq = (==)+applyPureRelation PureLt = (<)+applyPureRelation PureLe = (<=)+applyPureRelation PureGt = (>)+applyPureRelation PureGe = (>=)++-- | Structurally prove that a concrete witness exists for both guards. The+-- accepted fragment is described on 'checkTransitionDeterminismPure'. Returning+-- 'False' means either disjoint or unknown. Like the historical @PTop@ and+-- @PInCtor@ cases, this proof assumes the register and command schemas are+-- inhabited.+provablyOverlap :: HsPred rs ci -> HsPred rs ci -> Bool+provablyOverlap PLeftArm PLeftArm = True+provablyOverlap PRightArm PRightArm = True+provablyOverlap a b = case (pureFragment a, pureFragment b) of+  (PureKnown leftGuard, PureKnown rightGuard) ->+    pureGuardsOverlap leftGuard rightGuard+  _ -> False++pureGuardsOverlap :: PureGuard -> PureGuard -> Bool+pureGuardsOverlap leftGuard rightGuard = case commonPureConstructor of+  Nothing -> False+  Just constructorName ->+    all (comparisonMatchesConstructor constructorName) comparisons+      && all pureComparisonGroupSatisfiable (groupPureComparisons comparisons)+  where+    comparisons =+      pureGuardComparisons leftGuard <> pureGuardComparisons rightGuard+    commonPureConstructor = do+      leftConstructor <- singlePureConstructor (pureGuardConstructors leftGuard)+      rightConstructor <- singlePureConstructor (pureGuardConstructors rightGuard)+      compatiblePureConstructors leftConstructor rightConstructor++singlePureConstructor :: [String] -> Maybe (Maybe String)+singlePureConstructor names = case nub names of+  [] -> Just Nothing+  [name] -> Just (Just name)+  _ -> Nothing++compatiblePureConstructors ::+  Maybe String -> Maybe String -> Maybe (Maybe String)+compatiblePureConstructors Nothing Nothing = Just Nothing+compatiblePureConstructors (Just name) Nothing = Just (Just name)+compatiblePureConstructors Nothing (Just name) = Just (Just name)+compatiblePureConstructors (Just leftName) (Just rightName)+  | leftName == rightName = Just (Just leftName)+  | otherwise = Nothing++comparisonMatchesConstructor :: Maybe String -> PureComparison -> Bool+comparisonMatchesConstructor constructorName (PureComparison variable _ _ _) =+  case pureVariableInputCtor variable of+    Nothing -> True+    Just inputConstructor -> constructorName == Just inputConstructor++groupPureComparisons :: [PureComparison] -> [[PureComparison]]+groupPureComparisons [] = []+groupPureComparisons (comparison : rest) =+  (comparison : sameVariable) : groupPureComparisons otherVariables+  where+    variable = pureComparisonVariable comparison+    (sameVariable, otherVariables) =+      partition ((== variable) . pureComparisonVariable) rest++pureComparisonVariable :: PureComparison -> PureVariable+pureComparisonVariable (PureComparison variable _ _ _) = variable++data TypedPureComparison r = TypedPureComparison+  { typedPureRelation :: PureRelation,+    typedPureLiteral :: r,+    typedPureAccepts :: r -> Bool+  }++alignPureComparison ::+  forall r. (Typeable r) => PureComparison -> Maybe (TypedPureComparison r)+alignPureComparison (PureComparison @other _ relation literalValue accepts) =+  case eqTypeRep (typeRep @r) (typeRep @other) of+    Just HRefl -> Just (TypedPureComparison relation literalValue accepts)+    Nothing -> Nothing++pureComparisonGroupSatisfiable :: [PureComparison] -> Bool+pureComparisonGroupSatisfiable [] = True+pureComparisonGroupSatisfiable+  (PureComparison @r _ relation literalValue accepts : rest) =+    case traverse (alignPureComparison @r) rest of+      Nothing -> False+      Just alignedRest ->+        let comparisons =+              TypedPureComparison relation literalValue accepts : alignedRest+         in case discoverIntegralDomain @r of+              Just domain -> integralComparisonsSatisfiable domain comparisons+              Nothing -> literalWitnessSatisfies comparisons++data IntegralDomain r = IntegralDomain+  { integralValue :: r -> Integer,+    integralMinimum :: Maybe Integer,+    integralMaximum :: Maybe Integer+  }++discoverIntegralDomain :: forall r. (Typeable r) => Maybe (IntegralDomain r)+discoverIntegralDomain+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Integer) =+      Just (IntegralDomain id Nothing Nothing)+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int) =+      Just (boundedIntegralDomain @Int)+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word8) =+      Just (boundedIntegralDomain @Word8)+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word16) =+      Just (boundedIntegralDomain @Word16)+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word32) =+      Just (boundedIntegralDomain @Word32)+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word64) =+      Just (boundedIntegralDomain @Word64)+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int32) =+      Just (boundedIntegralDomain @Int32)+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int64) =+      Just (boundedIntegralDomain @Int64)+  | otherwise = Nothing++boundedIntegralDomain ::+  forall r. (Integral r, Bounded r) => IntegralDomain r+boundedIntegralDomain =+  IntegralDomain+    { integralValue = toInteger,+      integralMinimum = Just (toInteger (minBound @r)),+      integralMaximum = Just (toInteger (maxBound @r))+    }++integralComparisonsSatisfiable ::+  IntegralDomain r -> [TypedPureComparison r] -> Bool+integralComparisonsSatisfiable domain comparisons =+  intervalIsNonempty finalMinimum finalMaximum+  where+    (finalMinimum, finalMaximum) =+      foldl' refine (integralMinimum domain, integralMaximum domain) comparisons++    refine (minimumValue, maximumValue) comparison =+      let literalValue = integralValue domain (typedPureLiteral comparison)+       in case typedPureRelation comparison of+            PureEq ->+              ( maximumMaybe minimumValue (Just literalValue),+                minimumMaybe maximumValue (Just literalValue)+              )+            PureLt ->+              (minimumValue, minimumMaybe maximumValue (Just (literalValue - 1)))+            PureLe ->+              (minimumValue, minimumMaybe maximumValue (Just literalValue))+            PureGt ->+              (maximumMaybe minimumValue (Just (literalValue + 1)), maximumValue)+            PureGe ->+              (maximumMaybe minimumValue (Just literalValue), maximumValue)++maximumMaybe :: Maybe Integer -> Maybe Integer -> Maybe Integer+maximumMaybe Nothing b = b+maximumMaybe a Nothing = a+maximumMaybe (Just a) (Just b) = Just (max a b)++minimumMaybe :: Maybe Integer -> Maybe Integer -> Maybe Integer+minimumMaybe Nothing b = b+minimumMaybe a Nothing = a+minimumMaybe (Just a) (Just b) = Just (min a b)++intervalIsNonempty :: Maybe Integer -> Maybe Integer -> Bool+intervalIsNonempty (Just minimumValue) (Just maximumValue) =+  minimumValue <= maximumValue+intervalIsNonempty _ _ = True++literalWitnessSatisfies :: [TypedPureComparison r] -> Bool+literalWitnessSatisfies comparisons =+  any satisfiesEveryComparison (map typedPureLiteral comparisons)+  where+    satisfiesEveryComparison candidate =+      all (\comparison -> typedPureAccepts comparison candidate) comparisons++overlapConstructor :: HsPred rs ci -> HsPred rs ci -> Maybe String+overlapConstructor leftGuard rightGuard = do+  PureKnown left <- Just (pureFragment leftGuard)+  PureKnown right <- Just (pureFragment rightGuard)+  leftConstructor <- singlePureConstructor (pureGuardConstructors left)+  rightConstructor <- singlePureConstructor (pureGuardConstructors right)+  compatible <- compatiblePureConstructors leftConstructor rightConstructor+  compatible++-- | Internal: the determinism component of 'validateTransducer'. Like+-- 'checkTransitionDeterminismPure' but emits the richer 'NondeterministicPair'+-- directly, populating 'tvwInCtor' with the common command constructor found+-- anywhere in either conjunction spine (and 'Nothing' when neither names one).+determinismWarnings ::+  (Bounded s, Enum s, Show s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  [TransducerValidationWarning s]+determinismWarnings t =+  [ NondeterministicPair+      { tvwSource = s,+        tvwEdgeA = i,+        tvwEdgeB = j,+        tvwInCtor = overlapConstructor (guard e1) (guard e2),+        tvwDetail = overlapDetail i j s+      }+  | s <- [minBound .. maxBound],+    let ies = zip [(0 :: Int) ..] (edgesOut t s),+    (i, e1) <- ies,+    (j, e2) <- ies,+    i < j,+    provablyOverlap (guard e1) (guard e2)+  ]  -- ** Dead-edge diagnostics 

@@ -1,119 +0,0 @@--- | A Chassaing-shape Decider façade over a 'SymTransducer'.------ Users coming from the naive functional event-sourcing world--- (Jérémie Chassaing's /Functional Event Sourcing Decider/) work--- with a small record:------ @--- data Decider c e s = Decider---   { decide       :: c -> s -> [e]---   , evolve       :: s -> e -> s---   , initialState :: s---   , isTerminal   :: s -> Bool---   }--- @------ 'toDecider' projects the keiki 'SymTransducer' onto this shape.--- 'decide' is built on 'omega' (the forward step that emits one or--- more events per command after the EP-19 widening); 'evolve' is--- built on 'applyEvent' (the letter-only inverse step). With the--- widened @'Keiki.Core.Edge.output' :: ['Keiki.Core.OutTerm' rs ci--- co]@ a single command can yield two or more events end-to-end--- without any state-refinement scaffolding — 'decide' returns the--- full list directly. EP-19 retired the previous EP-20 façades--- (@toMultiDecider@ + @DriverConfig@); the multi-event behaviour is--- now first-class in the AST.------ == Streaming replay through multi-event edges------ The 'evolve' field is letter-only (handles edges with output of--- length 0 or 1) and remains the canonical letter-replay verb.--- Event-by-event streaming across a length-2+ edge passes through--- the intermediate "I just observed event 1, expecting event 2 next"--- state; the 'evolveStreaming' field exposes this via--- 'Keiki.Core.InFlight' and 'Keiki.Core.applyEventStreaming'. The--- two evolve fields agree on length-0/1 commands; they diverge--- only on length-2+ where the streaming path stays /InFlight/--- between events.------ == One semantic gap remains------ /ε-edges/ — edges whose @output@ is @[]@. The transducer--- transitions state without emitting an event. 'decide' returns--- @[]@ for such commands, and the result is identical to "no event--- happened" from the Decider record's perspective. Use--- 'Keiki.Core.delta' / 'Keiki.Core.step' directly when ε-driven--- transitions matter.-module Keiki.Decider-  ( Decider (..),-    toDecider,-  )-where--import Keiki.Core-  ( BoolAlg,-    InFlight (..),-    RegFile,-    SymTransducer (..),-    applyEvent,-    applyEventStreaming,-    omega,-  )---- | The Chassaing-shape Decider record. Field selectors are named--- to match published Decider examples; conflicts with other modules--- are avoided by importing this module qualified.------ The @s_streaming@ parameter carries the InFlight-aware streaming--- state ('Keiki.Core.InFlight' s co paired with a register file);--- for letter-only callers it is unused.-data Decider c e s s_streaming = Decider-  { decide :: c -> s -> [e],-    evolve :: s -> e -> s,-    evolveStreaming :: s_streaming -> e -> Maybe s_streaming,-    initialState :: s,-    isTerminal :: s -> Bool-  }---- | Project a keiki 'SymTransducer' to a 'Decider' record. The--- letter-replay state carrier is @(s, RegFile rs)@ and the--- streaming-replay state carrier is @('Keiki.Core.InFlight' s co,--- RegFile rs)@ — keiki edge guards depend on the register file as--- well as the control vertex, and streaming replay through a--- length-2+ edge intrinsically observes a mid-chain wrapper.------ == Field-by-field correspondence------ @--- decide d cmd (s, regs)        -- = omega t s regs cmd            (EP-19 widened)--- evolve d (s, regs) ev         -- = letter-only applyEvent;---                               --   on length-2+ edges, falls back---                               --   to the input state defensively--- evolveStreaming d ws ev       -- = applyEventStreaming, returning---                               --   the wrapped state mid-chain--- initialState d                -- = (initial t, initialRegs t)--- isTerminal   d (s, _regs)     -- = isFinal t s--- @------ == Defensive 'evolve'------ 'applyEvent' returns 'Nothing' when an event cannot be replayed--- letter-by-letter from @(s, regs)@. To keep the Chassaing signature--- non-'Maybe', 'evolve' returns the input state on failure. Callers--- that want strict replay use 'evolveStreaming' (whose 'Maybe' is--- explicit) or 'Keiki.Core.applyEvents' (which returns 'Nothing' on--- the first replay failure across a chunk).-toDecider ::-  (BoolAlg phi (RegFile rs, ci), Eq co) =>-  SymTransducer phi rs s ci co ->-  Decider ci co (s, RegFile rs) (InFlight s co, RegFile rs)-toDecider t =-  Decider-    { decide = \cmd (s, regs) -> omega t s regs cmd,-      evolve = \(s, regs) ev -> case applyEvent t s regs ev of-        Just (s', regs') -> (s', regs')-        Nothing -> (s, regs),-      evolveStreaming = \(w, regs) ev -> applyEventStreaming t w regs ev,-      initialState = (initial t, initialRegs t),-      isTerminal = \(s, _regs) -> isFinal t s-    }

@@ -314,7 +314,9 @@ -- | Derive an initial 'RegFile' for any slot list. Every slot is -- pre-bound to a deferred error tagged with the slot's name so reads -- of an uninitialized slot crash with a targeted message instead of--- a silent bottom.+-- a silent bottom. Every slot must be written before the register file is+-- read or encoded; 'emptyRegFile' is an initialization scaffold, not an+-- encodable snapshot. class EmptyRegFile (rs :: [Slot]) where   emptyRegFile :: RegFile rs @@ -328,7 +330,12 @@   emptyRegFile =     RCons       (Proxy @s)-      (error ("uninit: " ++ symbolVal (Proxy @s)))+      ( error+          ( "uninit: "+              ++ symbolVal (Proxy @s)+              ++ " (slot read before first write; a RegFile must be fully initialized before it is read or encoded)"+          )+      )       emptyRegFile  -- * Sum-walking machinery -------------------------------------------------

@@ -1,18 +1,10 @@ {-# LANGUAGE TemplateHaskell #-} --- \$('deriveAggregateCtors' \'\'UserCmd \'\'UserRegRegs---     [ ("StartRegistration",  "Start")---     , ("ConfirmAccount",     "Confirm")---     , ("ResendConfirmation", "Resend")---     , ("FulfillGDPRRequest", "Gdpr")---     , ("Continue",           "Continue")---     ])--- @+-- |+-- Module      : Keiki.Generics.TH+-- Description : Template Haskell splices for aggregate constructor plumbing. ----- expands to the same 14 declarations a hand-written module ships--- (4 record ctors × 3 decls + 1 singleton × 2 decls).---- | Template Haskell splices that retire the per-constructor authoring+-- These splices retire the per-constructor authoring -- boilerplate at the example layer. -- -- 'deriveAggregateCtors' emits, for each entry in its spec list, the@@ -53,7 +45,39 @@ --   | ResendConfirmation ResendConfirmationData --   | FulfillGDPRRequest FulfillGDPRRequestData --   | Continue---   deriving ('Eq', 'Show', 'GHC.Generics.Generic')+--   deriving (Eq, Show, Generic)+--+-- \$('deriveAggregateCtors' \'\'UserCmd \'\'UserRegRegs+--     [ ("StartRegistration",  "Start")+--     , ("ConfirmAccount",     "Confirm")+--     , ("ResendConfirmation", "Resend")+--     , ("FulfillGDPRRequest", "Gdpr")+--     , ("Continue",           "Continue")+--     ])+-- @+--+-- This expands to the same 14 declarations a hand-written module ships+-- (4 record constructors × 3 declarations + 1 singleton × 2 declarations).+--+-- The @*All@ and @*With@ enumeration variants skip unsupported GADT and+-- explicitly quantified constructors, emitting a compile-time warning that+-- names both the skipped constructor and the splice. Explicit spec-list+-- variants fail when asked to generate helpers for an unsupported shape.+--+-- == Negative-test procedure (manual)+--+-- A positional payload is classified as the command constructor's payload,+-- then rejected immediately because it is not a single record-syntax type:+--+-- @+-- data BadCmd = Placed Int+-- type BadRegs = '[]+-- \$(deriveAggregateCtors \'\'BadCmd \'\'BadRegs [("Placed", "Placed")])+-- @+--+-- Compiling that splice must fail with+-- @deriveAggregateCtors: requires a single record-syntax constructor on+-- payload GHC.Types.Int@. module Keiki.Generics.TH   ( deriveAggregateCtors,     deriveAggregateCtorsAll,@@ -134,6 +158,7 @@   Q [Dec] deriveAggregateCtorsAll cmdName regsName = do   ctors <- reifyCtors cmdName "deriveAggregateCtorsAll"+  warnSkippedConstructors "deriveAggregateCtorsAll" ctors   let ctorMap = [(nameBase n, c) | c <- ctors, n <- conNames c]       specs = [(nameBase n, nameBase n) | c <- ctors, n <- conNames c]   genAggregateCtors cmdName regsName ctorMap specs@@ -185,6 +210,7 @@   Q [Dec] deriveAggregateCtorsWith cmdName regsName opts = do   ctors <- reifyCtors cmdName "deriveAggregateCtorsWith"+  warnSkippedConstructors "deriveAggregateCtorsWith" ctors   let ctorMap = [(nameBase n, c) | c <- ctors, n <- conNames c]       allCtors = map fst ctorMap   specs <-@@ -224,6 +250,7 @@   Q [Dec] deriveWireCtorsAll evtName = do   ctors <- reifyCtors evtName "deriveWireCtorsAll"+  warnSkippedConstructors "deriveWireCtorsAll" ctors   let ctorMap = [(nameBase n, c) | c <- ctors, n <- conNames c]       specs = [(nameBase n, nameBase n) | c <- ctors, n <- conNames c]   genWireCtors evtName ctorMap specs@@ -267,6 +294,7 @@   Q [Dec] deriveWireCtorsWith evtName opts = do   ctors <- reifyCtors evtName "deriveWireCtorsWith"+  warnSkippedConstructors "deriveWireCtorsWith" ctors   let ctorMap = [(nameBase n, c) | c <- ctors, n <- conNames c]       allCtors = map fst ctorMap   specs <-@@ -284,10 +312,8 @@ -- each constructor's own name as its short-name suffix. -- -- @---- $('deriveAggregate' \'\'OrderCmd \'\'OrderCartRegs \'\'OrderEvent)+-- \$('deriveAggregate' \'\'OrderCmd \'\'OrderCartRegs \'\'OrderEvent) -- @- deriveAggregate ::   -- | command sum type, e.g. @\'\'OrderCmd@   Name ->@@ -314,8 +340,7 @@ -- == Worked invocation -- -- @---- $('deriveView' \'\'Vertex \'\'UserRegRegs+-- \$('deriveView' \'\'Vertex \'\'UserRegRegs --     "SUserVertex" "UserView" "userView" --     [ ("PotentialCustomer",    []) --     , ("Registering",          [])@@ -324,7 +349,6 @@ --     , ("Deleted",              ["email", "deletedAt"]) --     ]) -- @- deriveView ::   -- | vertex enum, e.g. @\'\'Vertex@   Name ->@@ -537,6 +561,36 @@ conNames (InfixC _ n _) = [n] conNames _ = [] +-- | Extract names from every Template Haskell constructor shape, including+-- shapes that keiki deliberately does not generate helpers for.+allConNames :: Con -> [Name]+allConNames (NormalC n _) = [n]+allConNames (RecC n _) = [n]+allConNames (InfixC _ n _) = [n]+allConNames (ForallC _ _ con) = allConNames con+allConNames (GadtC names _ _) = names+allConNames (RecGadtC names _ _) = names++-- | Enumeration splices skip unsupported GADT or explicitly quantified+-- constructors, but never silently. Explicit spec-list splices retain their+-- existing fail-fast behavior when a requested constructor is unsupported.+warnSkippedConstructors :: String -> [Con] -> Q ()+warnSkippedConstructors caller ctors =+  mapM_ warn skipped+  where+    skipped =+      [ name+      | con <- ctors,+        null (conNames con),+        name <- allConNames con+      ]+    warn name =+      reportWarning+        ( caller+            <> ": skipped unsupported GADT or explicitly quantified constructor "+            <> nameBase name+        )+ -- | Three-state classification of a constructor's payload. -- --   * @Just Nothing@  — singleton (zero-arg 'NormalC').@@ -682,6 +736,7 @@ recordDecls ::   Name -> Name -> String -> String -> Type -> Q [Dec] recordDecls cmdName regsName ctorStr shortStr payTy = do+  _ <- requireSingleRecordCtor "deriveAggregateCtors" payTy   let inCtorN = mkName ("inCtor" <> shortStr)       inpN = mkName ("inp" <> shortStr)       isN = mkName ("is" <> shortStr)@@ -844,18 +899,7 @@ -- unambiguous. genTermFieldsRecord :: String -> Type -> Q [Dec] genTermFieldsRecord shortStr payTy = do-  payName <- typeConstructorName payTy-  payInfo <- reify payName-  fields <- case payInfo of-    TyConI (DataD _ _ _ _ [RecC _ fs] _) -> pure fs-    TyConI (NewtypeD _ _ _ _ (RecC _ fs) _) -> pure fs-    _ ->-      fail $-        "deriveWireCtors: TermFields generation requires "-          <> "a single record-syntax constructor on payload "-          <> show payName-          <> ", got "-          <> show payInfo+  fields <- requireSingleRecordCtor "deriveWireCtors" payTy   let recName = mkName (shortStr <> "TermFields")   rsN <- newName "rs"   ciN <- newName "ci"@@ -910,15 +954,35 @@       instDec = InstanceD Nothing [] instHead [methodDef]   pure [recDataDec, instDec] +-- | Require a payload type to name a data or newtype with exactly one+-- record-syntax constructor. Shared by command projections and event+-- @TermFields@ generation so both sides reject invalid payloads at the splice+-- boundary with the same diagnostic shape.+requireSingleRecordCtor :: String -> Type -> Q [VarBangType]+requireSingleRecordCtor caller payTy = do+  payName <- typeConstructorName caller payTy+  payInfo <- reify payName+  case payInfo of+    TyConI (DataD _ _ _ _ [RecC _ fields] _) -> pure fields+    TyConI (NewtypeD _ _ _ _ (RecC _ fields) _) -> pure fields+    _ ->+      fail $+        caller+          <> ": requires a single record-syntax constructor on payload "+          <> show payName+          <> ", got "+          <> show payInfo+ -- | Extract a type's head constructor name. Accepts @ConT@ and the -- common forms it might wear after kind-elaboration; rejects -- function/forall/promoted shapes.-typeConstructorName :: Type -> Q Name-typeConstructorName (ConT n) = pure n-typeConstructorName (SigT t _) = typeConstructorName t-typeConstructorName other =+typeConstructorName :: String -> Type -> Q Name+typeConstructorName _ (ConT n) = pure n+typeConstructorName caller (SigT t _) = typeConstructorName caller t+typeConstructorName caller other =   fail $-    "deriveWireCtors: payload type must be a type constructor, "+    caller+      <> ": payload type must be a type constructor, "       <> "got "       <> show other 

@@ -4,9 +4,11 @@ -- on 'Keiki.Core.Update' (EP-18 of MasterPlan 6). -- -- The keiki invariant is that slot names within a register file are--- pairwise distinct. EP-18 promotes that invariant from a runtime--- check (the old @combine@'s integer-position overlap test) to a--- type-level constraint by:+-- pairwise distinct. 'DistinctNames' enforces that invariant at builder+-- entry points. Lower-level 'HasIndexN' resolution still selects the+-- first matching occurrence, so callers that bypass those entry points+-- also bypass the distinctness check. EP-18 separately promotes update+-- target distinctness from a runtime check to a type-level constraint by: -- --   * indexing 'Keiki.Core.Update' over @(w :: [Symbol])@, the set of --     slot names the update writes; and@@ -23,6 +25,7 @@     Concat,     Member,     Disjoint,+    DistinctNames,      -- * Slot-name projection     Names,@@ -79,6 +82,29 @@           ':$$: 'Text "Each register slot may be written at most once per edge update."       ) +-- | Pairwise distinctness of one slot-name list. Reports the first+-- duplicated name. Builder entry points apply this to 'Names' of the+-- register schema; lower-level AST construction does not.+type family DistinctNames (xs :: [Symbol]) :: Constraint where+  DistinctNames '[] = ()+  DistinctNames (x ': xs) = (NotElemSlot x xs, DistinctNames xs)++type family NotElemSlot (x :: Symbol) (ys :: [Symbol]) :: Constraint where+  NotElemSlot _ '[] = ()+  NotElemSlot x (y ': ys) = (NotElemSlotCmp (CmpSymbol x y) x, NotElemSlot x ys)++type family NotElemSlotCmp (cmp :: Ordering) (x :: Symbol) :: Constraint where+  NotElemSlotCmp 'LT _ = ()+  NotElemSlotCmp 'GT _ = ()+  NotElemSlotCmp 'EQ x =+    TypeError+      ( 'Text "Keiki: register file declares slot \""+          ':<>: 'Text x+          ':<>: 'Text "\" more than once. "+          ':$$: 'Text "Slot names in a register file must be pairwise distinct; "+          ':$$: 'Text "a duplicated name silently shadows the later slot."+      )+ -- | Project the slot-name list out of a slot list. The kind -- @[(Symbol, Type)]@ is keiki's @[Slot]@ at the kind level (a synonym -- defined in 'Keiki.Core'); written here in unfolded form to avoid a@@ -96,8 +122,10 @@   IS :: IndexN s rs r -> IndexN s ('(s', r') ': rs) r  -- | Resolve a label @s@ against a slot list @rs@ to an 'IndexN' for--- the value at that slot. The functional dependency @s rs -> r@--- ensures that a label uniquely determines the slot's type.+-- the value at that slot. Resolution selects the first matching slot.+-- Builder-authored transducers enforce pairwise-distinct names with+-- 'DistinctNames', but lower-level callers can still supply a duplicate+-- schema and will observe this first-match behavior. class   HasIndexN (s :: Symbol) (rs :: [(Symbol, Type)]) (r :: Type)     | s rs -> r

@@ -3,6 +3,7 @@ -- @Disjoint '[] '[]@ witness. GHC sees the @forall xs ys.@ as -- ambiguous because neither @xs@ nor @ys@ appear in the result; that -- is intentional — call sites pin them via 'TypeApplications'.+{-# LANGUAGE PatternSynonyms #-} {-# OPTIONS_GHC -Wno-redundant-constraints #-}  -- | Existential wrapper for 'SymTransducer' enabling participation in@@ -15,6 +16,48 @@ -- typeclasses ('Profunctor', 'Category', 'Strong', 'Choice', 'Arrow') -- expect. --+-- Stability: experimental. The wrapper and its categorical instances may+-- change before the law contract is resolved. Concrete checked composition+-- through 'Keiki.Composition.composeChecked' is the supported validation+-- boundary for aggregate pipelines.+--+-- == Law status: forward fragment versus inversion/replay+--+-- /Forward equivalence/ means that 'Keiki.Core.delta', 'Keiki.Core.omega',+-- and 'Keiki.Core.step' agree for every command sequence, comparing control+-- states up to the documented state isomorphism. /Inversion equivalence/ adds+-- agreement of 'Keiki.Core.solveOutput', streaming replay, and+-- reconstitution. Because replay is public and central to keiki, a law that+-- holds only forward is called a /forward fragment/, not an unqualified law.+--+-- * 'Profunctor'/'Functor': identity and composition hold on tested multi-step+--   forward traces. They fail inversion equivalence because input maps poison+--   @icBuild@ and output maps poison @wcMatch@. Mapped names are stamped with+--   @#lmapped@/@#rmapped@; arm predicates lowered by contramap use the same+--   marker and are symbolically conservative.+-- * 'Category': the identity sentinel is definitional, and stateful forward+--   associativity is tested after the real witness and snapshot fixes.+--   Non-identity composition is partial: slot overlap raises+--   'CategoryOverlapError', and a mapped boundary raises+--   'PoisonedCompositionError'. It is therefore not an unqualified lawful+--   'Category' over all public values.+-- * 'Choice': 'left''/'right'' preserve forward routing and replay for a+--   replayable stateful transducer on tested multi-step traces; they do not+--   repair an underlying transducer's inversion defect. Real+--   'PLeftArm'/'PRightArm' guards make the arms disjoint even for+--   epsilon/register-only underlying guards.+-- * 'Strong': 'first''/'second'' preserve the threaded value and forward+--   state evolution, but fail inversion equivalence because their paired+--   descriptors are not invertible. A Strong-produced boundary is poisoned.+-- * 'Arrow': standalone 'Arr.arr' has forward function behavior but is not+--   replay-invertible. Fusion fails: @arr f >>> arr g@ raises+--   'PoisonedCompositionError' rather than equalling @arr (g . f)@.+--+-- Deferred API choices (recorded 2026-07-12) are a forward-only wrapper, a+-- separate replay-safe/isomorphism capability, a total internal category, or+-- selective instance removal. This module selects none of them; all existing+-- instances remain available while the experimental contract is evaluated.+-- -- See @docs/plans/27-existential-wrapper-for-symtransducer-plus-profunctor-instance-and-variance-combinators.md@ -- for the design rationale and the documented variance caveat: -- transducers produced by 'lmapCi' / 'rmapCo' / 'dimapTransducer' /@@ -36,8 +79,10 @@ -- cannot be discharged by GHC at the wrapper boundary. module Keiki.Profunctor   ( -- * Existential wrapper-    SomeSymTransducer (..),+    SomeSymTransducer (SomeSymIdentity),+    pattern SomeSymTransducer,     someSymTransducer,+    PoisonProvenance (..),      -- * Standalone variance combinators on the concrete 'SymTransducer'     lmapCi,@@ -54,6 +99,7 @@      -- * Category-instance overlap exception     CategoryOverlapError (..),+    PoisonedCompositionError (..),   ) where @@ -62,9 +108,16 @@ import Control.Exception (Exception, throw) import Data.Profunctor (Choice (..), Profunctor (..), Strong (..)) import Data.Proxy (Proxy (..))-import Keiki.Composition (WeakenR, alternative, compose)+import Keiki.Composition+  ( KnownSlots (..),+    SlotListWitness (WNil),+    alternative,+    appendWitness,+    compose,+    withDisjointNil,+    withKnownSlots,+  ) import Keiki.Core-import Keiki.Generics (Append) import Unsafe.Coerce (unsafeCoerce)  -- | Existential wrapper hiding @rs@ (register-file slot list) and@@ -72,11 +125,12 @@ -- output alphabet @co@. Predicate carrier is fixed to 'HsPred' since -- "Keiki.Composition"'s combinators are pinned to that carrier. ----- The packed constraints @WeakenR rs@ and @KnownSlotNames rs@ are--- needed by the 'Cat.Category' instance: 'compose' demands--- @WeakenR rs1@, and the runtime slot-overlap check that guards--- 'Cat..' reads each transducer's slot names at the value level--- via @KnownSlotNames@. The packed constraints @Bounded s@ and+-- The packed 'KnownSlots' constraint supplies a value-level witness+-- for the hidden slot-list spine and bundles 'WeakenR' and+-- 'KnownSlotNames' as superclasses. Composite wrappers append the+-- real witnesses and re-derive all three dictionaries by structural+-- induction; no method-carrying dictionary is fabricated. The+-- packed constraints @Bounded s@ and -- @Enum s@ let pattern-matched-out transducers participate in the -- symbolic analyses ('Keiki.Symbolic.isSingleValuedSym', -- 'Keiki.Core.checkHiddenInputs'), which both enumerate the vertex@@ -102,35 +156,64 @@ -- 'compose'. See 'identityTransducer' for the concrete-identity -- transducer that some non-Category code paths still want. ----- Pattern-match on the constructor to recover the underlying+-- Pattern-match on the compatibility pattern to recover the underlying -- 'SymTransducer' (the @rs@ and @s@ variables come into scope as -- skolem types — they may not escape the pattern match). Handle -- 'SomeSymIdentity' explicitly when traversing arbitrary -- 'SomeSymTransducer' values.+--+-- | Tracks whether an existential wrapper's input or output descriptor has+-- been rewritten in a way that is unsafe to cross at a composition boundary.+data PoisonProvenance = PoisonProvenance+  { poisonedInput :: !Bool,+    poisonedOutput :: !Bool+  }+  deriving stock (Eq, Show)++cleanProvenance :: PoisonProvenance+cleanProvenance = PoisonProvenance False False++-- | A concrete symbolic transducer with its register and vertex types hidden,+-- or the definitional identity sentinel used by the 'Cat.Category' instance. data SomeSymTransducer ci co where-  SomeSymTransducer ::-    ( WeakenR rs,-      KnownSlotNames rs,+  SomeSymTransducerWith ::+    ( KnownSlots rs,       Bounded s,       Enum s     ) =>+    PoisonProvenance ->     SymTransducer (HsPred rs ci) rs s ci co ->     SomeSymTransducer ci co   SomeSymIdentity :: SomeSymTransducer a a +-- | Compatibility construction and match pattern for a concrete wrapper.+-- Direct construction starts with honest input/output alphabets; internal+-- instance operations retain provenance through @SomeSymTransducerWith@.+pattern SomeSymTransducer ::+  forall ci co.+  () =>+  forall rs s.+  (KnownSlots rs, Bounded s, Enum s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  SomeSymTransducer ci co+pattern SomeSymTransducer t <- SomeSymTransducerWith _ t+  where+    SomeSymTransducer t = SomeSymTransducerWith cleanProvenance t++{-# COMPLETE SomeSymTransducer, SomeSymIdentity #-}+ -- | Smart constructor: lift a concrete 'SymTransducer' into the -- wrapper. Equivalent to applying the data constructor; provided for -- naming consistency with the rest of @Keiki.Profunctor@'s exports -- and for users who prefer functions over constructors. someSymTransducer ::-  ( WeakenR rs,-    KnownSlotNames rs,+  ( KnownSlots rs,     Bounded s,     Enum s   ) =>   SymTransducer (HsPred rs ci) rs s ci co ->   SomeSymTransducer ci co-someSymTransducer = SomeSymTransducer+someSymTransducer = SomeSymTransducerWith cleanProvenance  -- * Standalone variance combinators --------------------------------------- @@ -138,7 +221,7 @@ -- 'InCtor' inside the transducer's guards / updates / outputs and -- replaces each with one whose 'icMatch' is precomposed with @f@. ----- /Variance caveat:/ the rewritten 'InCtor's 'icBuild' is poisoned+-- /Variance caveat (see "Law status" above):/ the rewritten 'InCtor's 'icBuild' is poisoned -- (raises a runtime error if invoked) — callers must not invoke -- 'Keiki.Core.solveOutput' on edges produced by this combinator. The -- forward evaluation path ('Keiki.Core.evalPred',@@ -163,7 +246,7 @@ -- structural 'PInCtor' check, effectively filtering them out of the -- transducer's command stream. ----- /Variance caveat:/ same as 'lmapCi' — 'Keiki.Core.solveOutput' is+-- /Variance caveat (see "Law status" above):/ same as 'lmapCi' — 'Keiki.Core.solveOutput' is -- not preserved. lmapMaybeCi ::   forall ci ci' rs s co.@@ -182,7 +265,7 @@ -- every 'WireCtor' inside the transducer's outputs and replaces each -- with one whose 'wcBuild' is post-composed with @g@. ----- /Variance caveat:/ the rewritten 'WireCtor's 'wcMatch' is set to+-- /Variance caveat (see "Law status" above):/ the rewritten 'WireCtor's 'wcMatch' is set to -- @const Nothing@ — 'Keiki.Core.solveOutput' on rewritten edges -- returns 'Nothing'. The forward output construction (which only -- uses 'wcBuild') is unaffected.@@ -200,7 +283,7 @@     }  -- | Bidirectional map on input and output alphabets. Equivalent to--- @'rmapCo' g . 'lmapCi' f@. /Variance caveat/ as both 'lmapCi' and+-- @'rmapCo' g . 'lmapCi' f@. /Variance caveat (see "Law status" above)/ as both 'lmapCi' and -- 'rmapCo': 'Keiki.Core.solveOutput' is not preserved on the result. dimapTransducer ::   (ci' -> ci) ->@@ -221,18 +304,30 @@ -- 'identityTransducer' wrap before the variance combinators run, so -- the @ci@/@co@ rewrites apply uniformly. instance Profunctor SomeSymTransducer where-  dimap f g (SomeSymTransducer t) =-    SomeSymTransducer (dimapTransducer f g t)+  dimap f g (SomeSymTransducerWith provenance t) =+    SomeSymTransducerWith+      provenance {poisonedInput = True, poisonedOutput = True}+      (dimapTransducer f g t)   dimap f g SomeSymIdentity =-    SomeSymTransducer (dimapTransducer f g identityTransducer)-  lmap f (SomeSymTransducer t) =-    SomeSymTransducer (lmapCi f t)+    SomeSymTransducerWith+      (PoisonProvenance True True)+      (dimapTransducer f g identityTransducer)+  lmap f (SomeSymTransducerWith provenance t) =+    SomeSymTransducerWith+      provenance {poisonedInput = True}+      (lmapCi f t)   lmap f SomeSymIdentity =-    SomeSymTransducer (lmapCi f identityTransducer)-  rmap g (SomeSymTransducer t) =-    SomeSymTransducer (rmapCo g t)+    SomeSymTransducerWith+      (PoisonProvenance True False)+      (lmapCi f identityTransducer)+  rmap g (SomeSymTransducerWith provenance t) =+    SomeSymTransducerWith+      provenance {poisonedOutput = True}+      (rmapCo g t)   rmap g SomeSymIdentity =-    SomeSymTransducer (rmapCo g identityTransducer)+    SomeSymTransducerWith+      (PoisonProvenance False True)+      (rmapCo g identityTransducer)  -- | 'Functor' on the output alphabet. @'fmap' = 'rmap'@. instance Functor (SomeSymTransducer ci) where@@ -345,18 +440,30 @@  instance Exception CategoryOverlapError +-- | Exception raised when categorical composition would cross a boundary+-- rewritten by a non-invertible input/output map. The boundary is rejected+-- before name substitution can silently bypass the map.+data PoisonedCompositionError = PoisonedCompositionError+  { pceSide :: String,+    pceDetail :: String+  }+  deriving stock (Eq, Show)++instance Exception PoisonedCompositionError+ -- | A constraint dictionary for @'Disjoint' xs ys@. Used together -- with 'unsafeCoerceDisjointness' to smuggle the constraint into -- scope after a value-level overlap check. data DictDisjoint xs ys where   DictDisjoint :: (Disjoint xs ys) => DictDisjoint xs ys --- | Fabricate a 'DictDisjoint' for arbitrary @xs@ and @ys@. The--- only safe call site is the body of 'Cat..' on--- 'SomeSymTransducer', after the value-level check has confirmed--- the slot lists are disjoint. The 'CategoryOverlapError' exception--- raised on overlap is the *only* safety net; calling this without--- a prior check can produce a semantically broken composite.+-- | Fabricate a 'DictDisjoint' for arbitrary @xs@ and @ys@. This is+-- the only fabricated dictionary in this module, and its only call+-- site is the body of 'Cat..' after the value-level check has+-- confirmed the slot lists are disjoint. Composite wrappers carry+-- real 'KnownSlots' witnesses, so the checked names remain accurate+-- under arbitrary nesting. Calling this without that check can+-- produce a semantically broken composite. -- -- Implementation: @'Disjoint' '[] '[]@ reduces to the trivially-true -- constraint @()@, so @DictDisjoint @'[] @'[]@ is always@@ -368,33 +475,6 @@ unsafeCoerceDisjointness =   unsafeCoerce (DictDisjoint :: DictDisjoint '[] '[]) --- | A constraint dictionary witnessing that a slot list satisfies--- the two structural classes the wrapper packs. Used together with--- 'unsafeCoerceWrapperDict' to wrap a freshly-composed--- @SymTransducer ... (Append rs1 rs2) ...@ back into--- 'SomeSymTransducer' when 'GHC' cannot reduce--- @WeakenR (Append rs1 rs2)@ / @KnownSlotNames (Append rs1 rs2)@--- (because the spines @rs1@ and @rs2@ are skolems).-data DictWrapper rs where-  DictWrapper :: (WeakenR rs, KnownSlotNames rs) => DictWrapper rs---- | Fabricate a 'DictWrapper' for an arbitrary slot list. Both--- 'WeakenR' and 'KnownSlotNames' are structural classes with--- automatic instances for every concrete @[Slot]@: whenever both--- @rs1@ and @rs2@ have these instances, so does @'Append' rs1 rs2@--- (provable by induction on @rs1@'s spine, which we cannot perform--- without a value-level witness — hence the 'unsafeCoerce').------ Safe at the 'Cat..' call site because both inner transducers'--- packed @WeakenR@ + @KnownSlotNames@ constraints already hold for--- @rs1@ and @rs2@ individually, and the composite slot list--- @'Append' rs1 rs2@ inherits the structural property.-unsafeCoerceWrapperDict ::-  forall rs.-  DictWrapper rs-unsafeCoerceWrapperDict =-  unsafeCoerce (DictWrapper :: DictWrapper '[])- -- * Category instance --------------------------------------------------  -- | Standard 'Control.Category.Category' instance.@@ -411,13 +491,13 @@ -- 'Keiki.Composition.compose'. The wrapper hides @rs@, so -- @compose@'s static @Disjoint (Names rs1) (Names rs2)@ constraint -- cannot be discharged by GHC; instead, the operator reads each--- transducer's slot names at the value level via 'KnownSlotNames',+-- transducer's slot names at the value level via 'KnownSlots', -- checks for overlap, and either: -- --   * raises 'CategoryOverlapError' (synchronously, on overlap), or---   * uses 'unsafeCoerceDisjointness' to fabricate the constraint---     evidence and calls 'compose' with the existential @rs@'s---     restored as the composite @'Append' rs1 rs2@.+--   * uses 'unsafeCoerceDisjointness' for the methodless constraint,+--     calls 'compose', and re-derives the composite's method-carrying+--     dictionaries from the appended slot-list witnesses. -- -- /Why a sentinel rather than a real identity transducer:/ -- 'Keiki.Composition.compose' substitutes t2's @TInpCtorField ic2@@@ -436,8 +516,8 @@    SomeSymIdentity . t = t   t . SomeSymIdentity = t-  SomeSymTransducer t2 . SomeSymTransducer t1 =-    composeWrappers t1 t2+  SomeSymTransducerWith provenance2 t2 . SomeSymTransducerWith provenance1 t1 =+    composeWrappers provenance1 t1 provenance2 t2  -- | Compose two existentially-packed transducers, performing the -- runtime overlap check that 'Cat..' delegates to. Factored out so@@ -446,27 +526,51 @@ -- their own, name them in a form usable inside 'TypeApplications'). composeWrappers ::   forall rs1 rs2 s1 s2 ci mid co.-  ( WeakenR rs1,-    KnownSlotNames rs1,-    KnownSlotNames rs2,+  ( KnownSlots rs1,+    KnownSlots rs2,     Bounded s1,     Enum s1,     Bounded s2,     Enum s2   ) =>+  PoisonProvenance ->   SymTransducer (HsPred rs1 ci) rs1 s1 ci mid ->+  PoisonProvenance ->   SymTransducer (HsPred rs2 mid) rs2 s2 mid co ->   SomeSymTransducer ci co-composeWrappers t1 t2 =+composeWrappers provenance1 t1 provenance2 t2 =   let names1 = slotNames @rs1       names2 = slotNames @rs2       overlap = filter (`elem` names2) names1-   in if not (null overlap)-        then throw (CategoryOverlapError overlap)-        else case unsafeCoerceDisjointness @(Names rs1) @(Names rs2) of+      boundaryPoison+        | poisonedOutput provenance1 =+            Just+              ( PoisonedCompositionError+                  "upstream output"+                  "the upstream wrapper was produced by rmap/dimap/first/arr; move the output map outside the composition (see Law status)"+              )+        | poisonedInput provenance2 =+            Just+              ( PoisonedCompositionError+                  "downstream input"+                  "the downstream wrapper was produced by lmap/dimap/first; move the input map outside the composition (see Law status)"+              )+        | otherwise = Nothing+   in case boundaryPoison of+        Just err -> throw err+        Nothing | not (null overlap) -> throw (CategoryOverlapError overlap)+        Nothing -> case unsafeCoerceDisjointness @(Names rs1) @(Names rs2) of           DictDisjoint ->-            case unsafeCoerceWrapperDict @(Append rs1 rs2) of-              DictWrapper -> SomeSymTransducer (compose t1 t2)+            withKnownSlots+              (appendWitness (slotWitness @rs1) (slotWitness @rs2))+              ( SomeSymTransducerWith+                  ( PoisonProvenance+                      { poisonedInput = poisonedInput provenance1,+                        poisonedOutput = poisonedOutput provenance2+                      }+                  )+                  (compose t1 t2)+              )  -- * Choice instance ---------------------------------------------------- @@ -483,13 +587,10 @@ -- -- /No slot-name overlap risk:/ 'identityTransducer' has @rs = '[]@, -- so the @'Disjoint' (Names rs) (Names '[])@ side condition on--- 'alternative' reduces to a vacuous constraint — no--- 'CategoryOverlapError' path is needed (unlike 'Cat..'). The--- 'unsafeCoerceDisjointness' call below fabricates the constraint--- evidence purely because GHC cannot reduce the type family with--- @rs@ being a skolem; the underlying claim--- (@Disjoint xs '[]@ is always vacuously true) is sound by the--- definition of 'Disjoint' in "Keiki.Internal.Slots".+-- 'alternative' is proved by induction over the packed 'KnownSlots'+-- witness — no 'CategoryOverlapError' path and no coercion are needed.+-- For 'right'', the left register list is empty, so both append and+-- disjointness reduce definitionally and the original witness applies. -- -- /Sentinel handling:/ when the input is the 'SomeSymIdentity' -- sentinel, both @'left''@ and @'right''@ return 'SomeSymIdentity' —@@ -497,7 +598,7 @@ -- of identity. The Choice law @left' Cat.id = Cat.id@ holds *by -- construction* on the wrapper. ----- /Variance caveat:/ inherits 'Keiki.Composition.alternative''s+-- /Variance caveat (see "Law status" above):/ inherits 'Keiki.Composition.alternative''s -- mechanical-inversion preservation: @solveOutput@ on edges produced -- by @left'@ / @right'@ runs the underlying alternative's -- @leftInCtor@ / @rightInCtor@ wrappers, which preserve round-trip@@ -510,52 +611,47 @@     SomeSymTransducer a b ->     SomeSymTransducer (Either a c) (Either b c)   left' SomeSymIdentity = SomeSymIdentity-  left' (SomeSymTransducer t) = leftWrap t+  left' (SomeSymTransducerWith provenance t) = leftWrap provenance t    right' ::     forall a b c.     SomeSymTransducer a b ->     SomeSymTransducer (Either c a) (Either c b)   right' SomeSymIdentity = SomeSymIdentity-  right' (SomeSymTransducer t) = rightWrap t+  right' (SomeSymTransducerWith provenance t) = rightWrap provenance t  -- | Helper for 'left'' on a wrapped concrete transducer. Factored out -- to bind the existentially-packed @rs@ and @s@ to named type--- variables so 'TypeApplications' on 'unsafeCoerceDisjointness' /--- 'unsafeCoerceWrapperDict' can reach them.+-- variables for the witness induction. leftWrap ::   forall rs s ci co c.-  ( WeakenR rs,-    KnownSlotNames rs,+  ( KnownSlots rs,     Bounded s,     Enum s   ) =>+  PoisonProvenance ->   SymTransducer (HsPred rs ci) rs s ci co ->   SomeSymTransducer (Either ci c) (Either co c)-leftWrap t =-  case unsafeCoerceDisjointness @(Names rs) @(Names '[]) of-    DictDisjoint ->-      case unsafeCoerceWrapperDict @(Append rs '[]) of-        DictWrapper ->-          SomeSymTransducer (alternative t (identityTransducer @c))+leftWrap provenance t =+  let w = slotWitness @rs+   in withDisjointNil w $+        withKnownSlots+          (appendWitness w WNil)+          (SomeSymTransducerWith provenance (alternative t (identityTransducer @c)))  -- | Helper for 'right'' on a wrapped concrete transducer. Symmetric -- to 'leftWrap'. rightWrap ::   forall rs s ci co c.-  ( WeakenR rs,-    KnownSlotNames rs,+  ( KnownSlots rs,     Bounded s,     Enum s   ) =>+  PoisonProvenance ->   SymTransducer (HsPred rs ci) rs s ci co ->   SomeSymTransducer (Either c ci) (Either c co)-rightWrap t =-  case unsafeCoerceDisjointness @(Names '[]) @(Names rs) of-    DictDisjoint ->-      case unsafeCoerceWrapperDict @(Append '[] rs) of-        DictWrapper ->-          SomeSymTransducer (alternative (identityTransducer @c) t)+rightWrap provenance t =+  SomeSymTransducerWith provenance (alternative (identityTransducer @c) t)  -- * Strong instance ---------------------------------------------------- @@ -576,7 +672,7 @@ --     'WireCtor' with one that consumes @(c, fs)@ and produces --     @(co, c)@ — @\\(c, fs) -> (wcBuild wc fs, c)@. ----- /Variance caveat:/ same lossy-@solveOutput@ contract as 'lmapCi' /+-- /Variance caveat (see "Law status" above):/ same lossy-@solveOutput@ contract as 'lmapCi' / -- 'rmapCo'. The contramapped 'InCtor's 'icBuild' is poisoned, the -- new 'WireCtor's 'wcMatch' is @const Nothing@, and 'pairSndInCtor''s -- 'icBuild' is poisoned. Forward processing@@ -683,7 +779,7 @@ -- rewrites for ~10% better build cost, but the current shape keeps -- the symmetry obvious and the implementation small. ----- /Variance caveat:/ inherits 'firstSym''s lossy-@solveOutput@+-- /Variance caveat (see "Law status" above):/ inherits 'firstSym''s lossy-@solveOutput@ -- contract. instance Strong SomeSymTransducer where   first' ::@@ -691,15 +787,19 @@     SomeSymTransducer a b ->     SomeSymTransducer (a, c) (b, c)   first' SomeSymIdentity = SomeSymIdentity-  first' (SomeSymTransducer t) = SomeSymTransducer (firstSym t)+  first' (SomeSymTransducerWith provenance t) =+    SomeSymTransducerWith+      provenance {poisonedInput = True, poisonedOutput = True}+      (firstSym t)    second' ::     forall a b c.     SomeSymTransducer a b ->     SomeSymTransducer (c, a) (c, b)   second' SomeSymIdentity = SomeSymIdentity-  second' (SomeSymTransducer t) =-    SomeSymTransducer+  second' (SomeSymTransducerWith provenance t) =+    SomeSymTransducerWith+      provenance {poisonedInput = True, poisonedOutput = True}       (lmapCi swap (rmapCo swap (firstSym t)))     where       swap :: forall x y. (x, y) -> (y, x)@@ -716,13 +816,13 @@ -- — see 'identityTransducer' for the same lesson); the edge's -- 'WireCtor's 'wcBuild' applies @f@ to the read input. ----- /Variance caveat:/ same lossy-@solveOutput@ contract as+-- /Variance caveat (see "Law status" above):/ same lossy-@solveOutput@ contract as -- 'lmapCi' / 'rmapCo' / 'firstSym'. The 'WireCtor's 'wcMatch' is -- @const Nothing@ — there is no inverse function in general. -- Forward processing ('Keiki.Core.delta', 'Keiki.Core.omega') is -- unaffected. ----- /Composition limitation:/ 'Keiki.Composition.compose' substitutes+-- /Composition limitation (see "Law status" above):/ 'Keiki.Composition.compose' substitutes -- t2's 'TInpCtorField' against t1's 'WireCtor'-emitted output and -- demands 'icName ic2 == wcName wc1'. An 'arrTransducer'-produced -- transducer's 'WireCtor' is named @"arr"@ but the next stage's@@ -786,7 +886,10 @@ -- 'arr f >>> arr g' applies — see 'arrTransducer' for the full -- caveat. instance Arr.Arrow SomeSymTransducer where-  arr f = SomeSymTransducer (arrTransducer f)+  arr f =+    SomeSymTransducerWith+      (PoisonProvenance False True)+      (arrTransducer f)   first = first'   second = second' @@ -803,7 +906,7 @@ contraInCtor :: (ci' -> ci) -> InCtor ci ifs -> InCtor ci' ifs contraInCtor f InCtor {icName = n, icMatch = m} =   InCtor-    { icName = n,+    { icName = n <> "#lmapped",       icMatch = m . f,       icBuild = poisonedIcBuild n     }@@ -814,7 +917,7 @@ contraMaybeInCtor :: (ci' -> Maybe ci) -> InCtor ci ifs -> InCtor ci' ifs contraMaybeInCtor f InCtor {icName = n, icMatch = m} =   InCtor-    { icName = n,+    { icName = n <> "#lmapped",       icMatch = \ci' -> f ci' >>= m,       icBuild = poisonedIcBuild n     }@@ -834,7 +937,7 @@ mapWireCtor :: (co -> co') -> WireCtor co fs -> WireCtor co' fs mapWireCtor g WireCtor {wcName = n, wcBuild = b} =   WireCtor-    { wcName = n,+    { wcName = n <> "#rmapped",       wcMatch = \_co' -> Nothing,       wcBuild = g . b     }@@ -876,6 +979,8 @@     go (PNot p) = PNot (go p)     go (PEq a b) = PEq (contraTerm f a) (contraTerm f b)     go (PInCtor ic) = PInCtor (contraInCtor f ic)+    go PLeftArm = PInCtor (mappedArmInCtor (Just . f) True)+    go PRightArm = PInCtor (mappedArmInCtor (Just . f) False)     go (PCmp op a b) = PCmp op (contraTerm f a) (contraTerm f b)  contraMaybePred :: forall ci ci' rs. (ci' -> Maybe ci) -> HsPred rs ci -> HsPred rs ci'@@ -889,7 +994,23 @@     go (PNot p) = PNot (go p)     go (PEq a b) = PEq (contraMaybeTerm f a) (contraMaybeTerm f b)     go (PInCtor ic) = PInCtor (contraMaybeInCtor f ic)+    go PLeftArm = PInCtor (mappedArmInCtor f True)+    go PRightArm = PInCtor (mappedArmInCtor f False)     go (PCmp op a b) = PCmp op (contraMaybeTerm f a) (contraMaybeTerm f b)++mappedArmInCtor ::+  (ci' -> Maybe (Either ci1 ci2)) ->+  Bool ->+  InCtor ci' '[]+mappedArmInCtor f wantLeft =+  InCtor+    { icName = if wantLeft then "keiki#leftArm#lmapped" else "keiki#rightArm#lmapped",+      icMatch = \ci' -> case f ci' of+        Just (Left _) | wantLeft -> Just RNil+        Just (Right _) | not wantLeft -> Just RNil+        _ -> Nothing,+      icBuild = poisonedIcBuild (if wantLeft then "keiki#leftArm#lmapped" else "keiki#rightArm#lmapped")+    }  -- ** Update -------------------------------------------------------------