keiki 0.2.0.0 → 0.3.0.0

raw patch · 32 files changed

+680/−112 lines, 32 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +43/−0
• README.md +4/−0
• keiki.cabal +2/−1
• src/Keiki/Builder.hs +23/−4
• src/Keiki/Composition.hs +18/−9
• src/Keiki/Core.hs +77/−9
• src/Keiki/Profunctor.hs +16/−10
• src/Keiki/Symbolic.hs +8/−2
• test/Keiki/BuilderSpike.hs +5/−2
• test/Keiki/CompositionAlignmentSpec.hs +4/−2
• test/Keiki/CompositionAlternativeSpec.hs +2/−1
• test/Keiki/CompositionFeedback1Spec.hs +6/−3
• test/Keiki/CompositionMultiEventSpec.hs +6/−3
• test/Keiki/CompositionSpec.hs +2/−1
• test/Keiki/CoreInFlightSpec.hs +2/−1
• test/Keiki/CoreSpec.hs +2/−1
• test/Keiki/Fixtures/BrokenTailCoverage.hs +2/−1
• test/Keiki/Fixtures/ComposeStateful.hs +16/−8
• test/Keiki/Fixtures/CounterPipeline.hs +2/−1
• test/Keiki/Fixtures/EmailDelivery.hs +2/−1
• test/Keiki/Fixtures/RegisterEmission.hs +6/−3
• test/Keiki/Fixtures/SplitCoverage.hs +2/−1
• test/Keiki/Fixtures/UserRegistration.hs +10/−5
• test/Keiki/RecomputeVerifySpec.hs +3/−1
• test/Keiki/Render/MermaidSpec.hs +7/−3
• test/Keiki/ReplayOnlySpec.hs +351/−0
• test/Keiki/RoundTripSpec.hs +2/−1
• test/Keiki/StepEitherSpec.hs +4/−4
• test/Keiki/SymbolicSpec.hs +20/−12
• test/Keiki/ValidationReplayAlignmentSpec.hs +10/−7
• test/Keiki/ValidationSpec.hs +21/−15
• test/Spec.hs +2/−0

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

@@ -1,5 +1,9 @@ # keiki — 継起 +<p align="center">+  <img src="docs/assets/keiki-logo.png" alt="keiki — 継起 logo" width="720">+</p>+ A Haskell library for the **pure core** of event sourcing, workflow engines, and durable execution, built on one formalism: the symbolic-register finite-state transducer.

@@ -1,6 +1,6 @@ cabal-version:   3.0 name:            keiki-version:         0.2.0.0+version:         0.3.0.0 synopsis:        Pure core for symbolic-register transducer event sourcing. description:   A Haskell library for the pure core of event sourcing, workflow@@ -139,6 +139,7 @@     Keiki.Render.PrettySpec     Keiki.Render.ValidateSpec     Keiki.ReplayEitherSpec+    Keiki.ReplayOnlySpec     Keiki.RoundTrip     Keiki.RoundTripSpec     Keiki.ShapeSpec

@@ -199,6 +199,9 @@     requireGt,     requireGe, +    -- ** Edge mode+    replayOnly,+     -- ** Termination     goto, @@ -223,6 +226,7 @@ import Keiki.Core   ( Cmp (..),     Edge (..),+    EdgeMode (..),     HsPred (..),     InCtor (..),     Index,@@ -290,7 +294,10 @@     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+    peOutputDecided :: Bool,+    -- | The edge's 'EdgeMode'. Starts 'Live'; a 'replayOnly' call in+    -- the body switches it to 'ReplayOnly'.+    peMode :: EdgeMode   }  -- | Whether an edge body has an enclosing input constructor. The@@ -525,6 +532,15 @@ noEmit :: EdgeBuilder rs ci co v pin w w () noEmit = EdgeBuilder $ \pe -> ((), pe {peOutputDecided = True}) +-- | Mark the edge under construction 'ReplayOnly': it is excluded+-- from forward stepping and participates in inversion only when no+-- 'Live' edge attributes the observed event. Use it to retain the+-- removed region of a tightened guard (@old-guard ∧ ¬new-guard@) as+-- a replay-only twin so events stored under the old rule keep an+-- inverting edge. Idempotent; position in the body is irrelevant.+replayOnly :: EdgeBuilder rs ci co v pin w w ()+replayOnly = EdgeBuilder $ \pe -> ((), pe {peMode = ReplayOnly})+ -- * Field-keyed record sugar ---------------------------------------------  -- | Convert a value of any type bearing the wire-side fields of an@@ -680,7 +696,8 @@             peOutput = [],             peTargets = [],             pePinned = PinCtor ic,-            peOutputDecided = False+            peOutputDecided = False,+            peMode = Live           }       (_, finalPE) = runEdgeBuilder (body (PayloadProj ic)) initial       edge = finalizeEdge finalPE@@ -704,7 +721,8 @@             peOutput = [],             peTargets = [],             pePinned = PinNone,-            peOutputDecided = False+            peOutputDecided = False,+            peMode = Live           }       (_, finalPE) = runEdgeBuilder body initial       edge = finalizeEdge finalPE@@ -753,7 +771,8 @@               { guard = peGuard pe,                 update = peUpdate pe,                 output = peOutput pe,-                target = t+                target = t,+                mode = peMode pe               }   [] -> Left DefectMissingGoto   ts@(_ : _ : _) -> Left (DefectMultipleGoto (length ts))

@@ -1106,6 +1106,7 @@       ![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+      !EdgeMode -- accumulated mode: 'Live' iff every component edge is  -- * compose ---------------------------------------------------------------- @@ -1448,7 +1449,8 @@           { guard = weakenLPred @rs1 @rs2 (guard e1),             update = weakenLUpdate @rs1 @rs2 u1,             output = [],-            target = Composite (target e1) s2+            target = Composite (target e1) s2,+            mode = mode e1           }      productEdge ::@@ -1486,7 +1488,8 @@                 (weakenLUpdate @rs1 @rs2 u1)                 (substUpdate @rs1 @rs2 u2 o1),             output = map (\o2 -> substOut @rs1 @rs2 o2 o1) (output e2),-            target = Composite (target e1) (target e2)+            target = Composite (target e1) (target e2),+            mode = mode e1 <> mode e2           }      -- \| The starting point for EP-19 M6's chain expansion. Carries@@ -1505,6 +1508,7 @@           []           []           s2+          (mode e1)      -- \| Enumerate all t2-edge paths that consume the supplied     -- mid-symbol list in order, starting from the path's current@@ -1522,9 +1526,9 @@     expandPaths [] path = [path]     expandPaths (o : rest) path =       case path of-        PartialPath g u outs env s2 ->+        PartialPath g u outs env s2 m ->           concatMap-            (\e2 -> expandPaths rest (stepPath g u outs env o s2 e2))+            (\e2 -> expandPaths rest (stepPath g u outs env m o s2 e2))             (edgesOut t2 s2)      -- \| Extend a path by one t2-edge consuming one mid-symbol.@@ -1537,11 +1541,12 @@       Update (Append rs1 rs2) w ci1 ->       [OutTerm (Append rs1 rs2) ci1 co] ->       [PendingWrite (Append rs1 rs2) ci1] ->+      EdgeMode ->       OutTerm rs1 ci1 mid ->       s2 ->       Edge (HsPred rs2 mid) rs2 mid co s2 ->       PartialPath rs1 rs2 ci1 co s2-    stepPath g u outs env o _s2 e2 = case e2 of+    stepPath g u outs env m o _s2 e2 = case e2 of       Edge {update = u2} ->         let stepGuard =               applyEnvPred env (substPred @rs1 @rs2 (guard e2) o)@@ -1558,6 +1563,7 @@               (outs ++ stepOutputs)               nextEnv               (target e2)+              (m <> mode e2)      -- \| Convert a fully-expanded path to a composite edge by     -- borrowing t1's @target@ for the composite's target.@@ -1570,12 +1576,13 @@         ci1         co         (Composite s1 s2)-    finalizePath e1 (PartialPath g u outs _env s2End) =+    finalizePath e1 (PartialPath g u outs _env s2End m) =       Edge         { guard = g,           update = u,           output = outs,-          target = Composite (target e1) s2End+          target = Composite (target e1) s2End,+          mode = m         }  -- * alternative -----------------------------------------------------------@@ -1682,7 +1689,8 @@                     . weakenLOut @rs1 @rs2                 )                 (output e1),-            target = Composite (target e1) s2+            target = Composite (target e1) s2,+            mode = mode e1           }      liftEdgeR ::@@ -1712,7 +1720,8 @@                     . weakenROut @rs1 @rs2                 )                 (output e2),-            target = Composite s1 (target e2)+            target = Composite s1 (target e2),+            mode = mode e2           }  -- * feedback1 ------------------------------------------------------------

@@ -96,6 +96,7 @@      -- * Edges and the transducer     Edge (..),+    EdgeMode (..),     SymTransducer (..),     Guarded,     applyEdgeUpdate,@@ -653,12 +654,46 @@ -- 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.+-- | Which execution paths an edge serves.+--+-- A 'Live' edge is an ordinary transition: forward stepping+-- ('delta' \/ 'step' \/ 'stepEither') may take it, and replay+-- ('applyEvent' \/ 'applyEventStreamingEither') may invert against it.+--+-- A 'ReplayOnly' edge is never taken by forward stepping — no new+-- command can fire it. It exists so events emitted under a retired+-- rule keep an inverting edge: when a guard is tightened, the removed+-- region (@old-guard ∧ ¬new-guard@) can be retained as a replay-only+-- twin of the live edge, keeping every stored event replayable while+-- the tightened rule governs all new traffic. Its 'update' defines how+-- those historical events fold /today/.+--+-- Inversion is two-phase: candidates are sought among 'Live' edges+-- first, and only when no live edge matches are 'ReplayOnly' edges+-- tried; ambiguity is judged within the phase that produced+-- candidates. An event attributable under the current rules therefore+-- always attributes there — only unattributable history falls through+-- to the replay-only arms.+data EdgeMode = Live | ReplayOnly+  deriving stock (Eq, Ord, Show, Bounded, Enum)++-- | 'Live' is the identity; 'ReplayOnly' absorbs. This is the+-- combination rule for composed edges: a composite edge may fire+-- forward only when every component may.+instance Semigroup EdgeMode where+  Live <> m = m+  ReplayOnly <> _ = ReplayOnly++instance Monoid EdgeMode where+  mempty = Live+ data Edge phi rs ci co s where   Edge ::     { guard :: phi,       update :: Update rs w ci,       output :: [OutTerm rs ci co],-      target :: s+      target :: s,+      mode :: EdgeMode     } ->     Edge phi rs ci co s @@ -903,7 +938,8 @@      in RCons p x rest'  -- | Single-step transition. Returns 'Just (s', regs')' iff exactly one--- outgoing edge has a satisfied guard.+-- outgoing 'Live' edge has a satisfied guard. 'ReplayOnly' edges are+-- never candidates: they serve inversion only. delta ::   (BoolAlg phi (RegFile rs, ci)) =>   SymTransducer phi rs s ci co ->@@ -914,6 +950,7 @@ delta t s regs ci =   case [ (target e, applyEdgeUpdate e regs ci)        | e <- edgesOut t s,+         mode e == Live,          models (guard e) (regs, ci)        ] of     [single] -> Just single@@ -937,6 +974,7 @@ omega t s regs ci =   case [ [evalOut o regs ci | o <- output e]        | e <- edgesOut t s,+         mode e == Live,          models (guard e) (regs, ci)        ] of     [evaluatedOuts] -> evaluatedOuts@@ -1020,6 +1058,7 @@       let matched =             [ (i, e)             | (i, e) <- indexed,+              mode e == Live,               models (guard e) (regs, ci)             ]        in case matched of@@ -1075,14 +1114,21 @@   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+  case candidates Live of     [single] -> Just single+    [] -> case candidates ReplayOnly of+      [single] -> Just single+      _ -> Nothing     _ -> Nothing+  where+    candidates phase =+      [ (target e, applyEdgeUpdate e regs ci)+      | e <- edgesOut t s,+        mode e == phase,+        o : _ <- [output e],+        Just ci <- [solveOutput o regs co],+        models (guard e) (regs, ci)+      ]  -- | Streaming-replay state wrapper. Used by 'applyEventStreamingEither' -- and its 'applyEventStreaming' compatibility wrapper.@@ -1220,9 +1266,19 @@           ]   where     indexed = zip [0 ..] (edgesOut t s)-    matched =+    -- Two-phase attribution: an event attributable under the current+    -- ('Live') rules attributes there; only unattributable history+    -- falls through to the 'ReplayOnly' arms. Ambiguity is judged+    -- within the phase that produced candidates, so a live edge and+    -- its replay-only twin can never be mutually ambiguous — even+    -- when their guards overlap, the live edge deterministically wins.+    matched = case matchedIn Live of+      [] -> matchedIn ReplayOnly+      liveMatches -> liveMatches+    matchedIn phase =       [ (i, e, ci)       | (i, e) <- indexed,+        mode e == phase,         o : _ <- [output e],         Just ci <- [solveOutput o regs co],         models (guard e) (regs, ci)@@ -2214,6 +2270,10 @@     (i, e1) <- indexedEdges,     (j, e2) <- indexedEdges,     i < j,+    -- Cross-mode pairs are resolved by replay's two-phase attribution+    -- (live candidates win outright; see 'applyEventStreamingEither'),+    -- so only same-mode pairs can be runtime-ambiguous.+    mode e1 == mode e2,     not (isBot (guard e1) || isBot (guard e2)),     Just wireName <- [headWireName e1],     Just otherWireName <- [headWireName e2],@@ -2270,6 +2330,10 @@     (i, e1) <- ies,     (j, e2) <- ies,     i < j,+    -- Only 'Live' edges compete in forward dispatch; a guard overlap+    -- involving a 'ReplayOnly' edge cannot cause forward ambiguity.+    mode e1 == Live,+    mode e2 == Live,     not (isBot (guard e1 `conj` guard e2))   ] @@ -2301,6 +2365,8 @@     (i, e1) <- ies,     (j, e2) <- ies,     i < j,+    mode e1 == Live,+    mode e2 == Live,     provablyOverlap (guard e1) (guard e2)   ] @@ -2677,6 +2743,8 @@     (i, e1) <- ies,     (j, e2) <- ies,     i < j,+    mode e1 == Live,+    mode e2 == Live,     provablyOverlap (guard e1) (guard e2)   ] 

@@ -409,7 +409,8 @@             { guard = PInCtor identityInCtor,               update = UKeep,               output = [identityOutTerm],-              target = IdVertex+              target = IdVertex,+              mode = Live             }         ],       initial = IdVertex,@@ -692,12 +693,13 @@     firstEdge ::       Edge (HsPred rs ci) rs ci co s ->       Edge (HsPred rs (ci, c)) rs (ci, c) (co, c) s-    firstEdge Edge {guard = g, update = u, output = mo, target = tgt} =+    firstEdge Edge {guard = g, update = u, output = mo, target = tgt, mode = m} =       Edge         { guard = contraPred fst g,           update = contraUpdate fst u,           output = fmap firstOutTerm mo,-          target = tgt+          target = tgt,+          mode = m         }      -- EP-53: 'OutFields' is now indexed by a single input field schema,@@ -847,7 +849,8 @@             { guard = PInCtor identityInCtor,               update = UKeep,               output = [arrOut],-              target = IdVertex+              target = IdVertex,+              mode = Live             }         ],       initial = IdVertex,@@ -1062,34 +1065,37 @@ -- ** Edge ---------------------------------------------------------------  rewriteEdge :: (ci' -> ci) -> Edge (HsPred rs ci) rs ci co s -> Edge (HsPred rs ci') rs ci' co s-rewriteEdge f Edge {guard = g, update = u, output = mo, target = tgt} =+rewriteEdge f Edge {guard = g, update = u, output = mo, target = tgt, mode = m} =   Edge     { guard = contraPred f g,       update = contraUpdate f u,       output = fmap (contraOutTerm f) mo,-      target = tgt+      target = tgt,+      mode = m     }  rewriteEdgeMaybe ::   (ci' -> Maybe ci) ->   Edge (HsPred rs ci) rs ci co s ->   Edge (HsPred rs ci') rs ci' co s-rewriteEdgeMaybe f Edge {guard = g, update = u, output = mo, target = tgt} =+rewriteEdgeMaybe f Edge {guard = g, update = u, output = mo, target = tgt, mode = m} =   Edge     { guard = contraMaybePred f g,       update = contraMaybeUpdate f u,       output = fmap (contraMaybeOutTerm f) mo,-      target = tgt+      target = tgt,+      mode = m     }  rewriteEdgeOut ::   (co -> co') ->   Edge (HsPred rs ci) rs ci co s ->   Edge (HsPred rs ci) rs ci co' s-rewriteEdgeOut g Edge {guard = guardP, update = u, output = mo, target = tgt} =+rewriteEdgeOut g Edge {guard = guardP, update = u, output = mo, target = tgt, mode = m} =   Edge     { guard = guardP,       update = u,       output = fmap (mapOutTermCo g) mo,-      target = tgt+      target = tgt,+      mode = m     }

@@ -648,11 +648,16 @@     vertexSV s =       let es = edgesOut t s           ies = zip [(0 :: Int) ..] es+          -- Only 'Live' edges compete in forward dispatch; guard+          -- overlap with or between 'ReplayOnly' edges cannot cause+          -- forward ambiguity.           pairs =             [ (e1, e2)             | (i, e1) <- ies,               (j, e2) <- ies,-              i < j+              i < j,+              mode e1 == Live,+              mode e2 == Live             ]        in all (\(e1, e2) -> isBot (guard e1 `conj` guard e2)) pairs @@ -679,7 +684,8 @@         { guard = SymPred (guard e),           update = u,           output = output e,-          target = target e+          target = target e,+          mode = mode e         }  -- * Solver-backed validation diagnostics (EP-56) ---------------------------

@@ -16,6 +16,7 @@ import Keiki.Builder qualified as B import Keiki.Core   ( Edge (..),+    EdgeMode (..),     HsPred,     Index,     OutFields (..),@@ -130,7 +131,8 @@                 wireBrewed                 (OFCons (inpInsert #amount) OFNil)             ],-          target = Brewing+          target = Brewing,+          mode = Live         }     ]   Brewing ->@@ -138,7 +140,8 @@         { guard = isContinue,           update = UKeep,           output = [],-          target = Idle+          target = Idle,+          mode = Live         }     ] 

@@ -42,7 +42,8 @@             { guard = PInCtor typoInMsgB,               update = UKeep,               output = [],-              target = StageVertex+              target = StageVertex,+              mode = Live             }         ],       initial = StageVertex,@@ -64,7 +65,8 @@                   ),               update = UKeep,               output = [],-              target = StageVertex+              target = StageVertex,+              mode = Live             }         ],       initial = StageVertex,

@@ -127,7 +127,8 @@                 wirePong                 (OFCons (inpPing #nonce) OFNil)             ],-          target = PingDone+          target = PingDone,+          mode = Live         }     ]   PingDone -> []

@@ -127,7 +127,8 @@                 wireFlipped                 (OFCons (inpFlip #tValue) OFNil)             ],-          target = On+          target = On,+          mode = Live         }     ]   On ->@@ -140,7 +141,8 @@                 wireFlipped                 (OFCons (inpFlip #tValue) OFNil)             ],-          target = Off+          target = Off,+          mode = Live         }     ] @@ -202,7 +204,8 @@                 wirePFlip                 (OFCons (inpPFlipped #tValue) OFNil)             ],-          target = Pol+          target = Pol,+          mode = Live         }     ] 

@@ -102,7 +102,8 @@                         OFNil                     )                 ],-              target = Q+              target = Q,+              mode = Live             }         ],       initial = Q,@@ -160,7 +161,8 @@                         OFNil                     )                 ],-              target = Z+              target = Z,+              mode = Live             },           Edge             { guard = matchInCtor inCtorMidB,@@ -177,7 +179,8 @@                         OFNil                     )                 ],-              target = Z+              target = Z,+              mode = Live             }         ],       initial = Z,

@@ -143,7 +143,8 @@                     )                 )             ],-          target = AlertEmitted+          target = AlertEmitted,+          mode = Live         }     ]   AlertEmitted -> []

@@ -61,7 +61,8 @@                       wcEchoed                       (OFCons (TInpCtorField inCtorBegin (#payload :: Index '[ '("payload", Int)] Int)) OFNil)                   ],-                target = True+                target = True,+                mode = Live               }           ]         True -> [],

@@ -73,7 +73,8 @@               { guard = matchInCtor inCtorTrue,                 update = UKeep,                 output = [pack inCtorTrue wcStringTrue OFNil],-                target = True+                target = True,+                mode = Live               }           ]         True -> [],

@@ -123,7 +123,8 @@                       wireQuotaAssigned                       (provisionQuota *: oNil)                   ],-                target = BtcProvisioned+                target = BtcProvisioned,+                mode = Live               }           ]         BtcProvisioned -> []

@@ -217,7 +217,8 @@                     wireMidVal                     (proj (#srcCount :: Index CounterRegs Int) *: oNil)                 ],-              target = CounterVertex+              target = CounterVertex,+              mode = Live             }         ],       initial = CounterVertex,@@ -241,7 +242,8 @@                     wireOutVal                     (inpCtor inCtorMidVal (#v :: Index '[ '("v", Int)] Int) *: oNil)                 ],-              target = SinkVertex+              target = SinkVertex,+              mode = Live             }         ],       initial = SinkVertex,@@ -260,7 +262,8 @@                 [ pack inCtorGo wireMidVal (lit 10 *: oNil),                   pack inCtorGo wireMidVal (lit 20 *: oNil)                 ],-              target = PairVertex+              target = PairVertex,+              mode = Live             }         ],       initial = PairVertex,@@ -283,7 +286,8 @@                     wireStage1                     (inpCtor inCtorMidVal (#v :: Index '[ '("v", Int)] Int) *: oNil)                 ],-              target = PhaseVertex+              target = PhaseVertex,+              mode = Live             },           Edge             { guard =@@ -296,7 +300,8 @@                     wireStage2                     (inpCtor inCtorMidVal (#v :: Index '[ '("v", Int)] Int) *: oNil)                 ],-              target = PhaseVertex+              target = PhaseVertex,+              mode = Live             }         ],       initial = PhaseVertex,@@ -312,7 +317,8 @@             { guard = matchInCtor inCtorProduceA,               update = UKeep,               output = [pack inCtorProduceA wireM2A (lit 5 *: oNil)],-              target = M2SourceVertex+              target = M2SourceVertex,+              mode = Live             }         ],       initial = M2SourceVertex,@@ -335,7 +341,8 @@                     wireSawA                     (inpCtor inCtorM2A (#a :: Index '[ '("a", Int)] Int) *: oNil)                 ],-              target = WrongVertex+              target = WrongVertex,+              mode = Live             },           Edge             { guard =@@ -348,7 +355,8 @@                     wireSawB                     (inpCtor inCtorM2B (#b :: Index '[ '("b", Int)] Int) *: oNil)                 ],-              target = WrongVertex+              target = WrongVertex,+              mode = Live             }         ],       initial = WrongVertex,

@@ -114,7 +114,8 @@               update = USet IZ (tadd (TReg ZIdx) (TInpCtorField ic ZIdx)),               output =                 [pack ic wc (OFCons (mkField (TInpCtorField ic ZIdx)) OFNil)],-              target = StageVertex+              target = StageVertex,+              mode = Live             }         ],       initial = StageVertex,

@@ -233,7 +233,8 @@                     )                 )             ],-          target = EmailSentVertex+          target = EmailSentVertex,+          mode = Live         }     ]   EmailSentVertex -> []

@@ -102,7 +102,8 @@               { guard = matchInCtor inCtorOpen,                 update = USet (#owner :: IndexN "owner" RegisterEmissionRegs Text) (TInpCtorField inCtorOpen (#owner :: Index '[ '("owner", Text)] Text)),                 output = [pack inCtorOpen wireOpened (TInpCtorField inCtorOpen (#owner :: Index '[ '("owner", Text)] Text) *: oNil)],-                target = Active+                target = Active,+                mode = Live               }           ]         Active ->@@ -118,7 +119,8 @@                           *: oNil                       )                   ],-                target = Active+                target = Active,+                mode = Live               },             Edge               { guard = matchInCtor inCtorClose,@@ -127,7 +129,8 @@                   [ pack inCtorClose wireClosed (TReg (#owner :: Index RegisterEmissionRegs Text) *: oNil),                     pack inCtorClose wireArchived (TReg (#owner :: Index RegisterEmissionRegs Text) *: oNil)                   ],-                target = Finished+                target = Finished,+                mode = Live               }           ]         Finished -> [],

@@ -102,7 +102,8 @@               { guard = matchInCtor inCtorBegin,                 update = UKeep,                 output = outputs,-                target = True+                target = True,+                mode = Live               }           ]         True -> [],

@@ -430,7 +430,8 @@                 wireConfirmationEmailSent                 (OFCons (inpStart #email) OFNil)             ],-          target = RequiresConfirmation+          target = RequiresConfirmation,+          mode = Live         }     ]   RequiresConfirmation ->@@ -459,7 +460,8 @@                     )                 )             ],-          target = Confirmed+          target = Confirmed,+          mode = Live         },       -- Resend: rotate the code (code arrives in the command).       Edge@@ -483,7 +485,8 @@                     )                 )             ],-          target = RequiresConfirmation+          target = RequiresConfirmation,+          mode = Live         },       -- GDPR before confirmation emits the deletion event so replay observes       -- the state and register change.@@ -502,7 +505,8 @@                     (OFCons (inpGdpr #at) OFNil)                 )             ],-          target = Deleted+          target = Deleted,+          mode = Live         }     ]   Confirmed ->@@ -521,7 +525,8 @@                     (OFCons (inpGdpr #at) OFNil)                 )             ],-          target = Deleted+          target = Deleted,+          mode = Live         }     ]   Deleted -> []

@@ -31,6 +31,7 @@ import Keiki.Builder qualified as B import Keiki.Core   ( Edge (..),+    EdgeMode (..),     HiddenInputWarning (..),     HsPred (..),     Index,@@ -133,7 +134,8 @@             { guard = PInCtor inCtorAdd,               update = UKeep,               output = [badOut],-              target = CartOpen+              target = CartOpen,+              mode = Live             }         ],       initial = CartOpen,

@@ -38,6 +38,7 @@ import Keiki.CompositionSpec (alertSource) import Keiki.Core   ( Edge (..),+    EdgeMode (..),     HsPred (..),     InCtor (..),     OutFields (..),@@ -681,7 +682,8 @@                 { guard = PInCtor inCtorTick,                   update = UKeep,                   output = [pack inCtorTick wireTick OFNil],-                  target = tgt+                  target = tgt,+                  mode = Live                 }             ]           else [],@@ -811,7 +813,8 @@                     pack inCtorGo wireMB OFNil,                     pack inCtorGo wireMC OFNil                   ],-                target = MS1+                target = MS1,+                mode = Live               }           ]         MS1 ->@@ -822,7 +825,8 @@                   [ pack inCtorGo wireMA OFNil,                     pack inCtorGo wireMB OFNil                   ],-                target = MS2+                target = MS2,+                mode = Live               }           ]         MS2 -> [],

@@ -0,0 +1,351 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE QualifiedDo #-}++-- | EP-6 (keiro MasterPlan 24): 'ReplayOnly' edges. A replay-only edge+-- is excluded from forward stepping and participates in inversion only+-- when no 'Live' edge attributes the observed event. The fixture is the+-- keiki-level shape of the "black-acuity" guard-tightening scenario:+-- machine A confirms any reservation; machine B tightens the guard to+-- non-black acuity; the replay-only twin carries the removed region+-- (@acuityBlack == True@) so history stays replayable.+module Keiki.ReplayOnlySpec (spec) where++import Data.Proxy (Proxy (..))+import Keiki.Builder ((.=))+import Keiki.Builder qualified as B+import Keiki.Core+import Test.Hspec++-- * Fixture: the black-acuity scenario at the keiki level ------------------++data DivertCmd = ConfirmReservation Bool+  deriving stock (Eq, Show)++data DivertEvent = ReservationConfirmed Bool+  deriving stock (Eq, Show)++data DivertVertex = Held | Confirmed+  deriving stock (Eq, Ord, Show, Enum, Bounded)++type DivertRegs = '[ '("wasBlack", Bool)]++inCtorConfirm :: InCtor DivertCmd '[ '("acuityBlack", Bool)]+inCtorConfirm =+  InCtor+    { icName = "ConfirmReservation",+      icMatch = \case+        ConfirmReservation b -> Just (RCons (Proxy @"acuityBlack") b RNil),+      icBuild = \(RCons _ b RNil) -> ConfirmReservation b+    }++wireConfirmed :: WireCtor DivertEvent (Bool, ())+wireConfirmed =+  WireCtor+    { wcName = "ReservationConfirmed",+      wcMatch = \case+        ReservationConfirmed b -> Just (b, ()),+      wcBuild = \(b, ()) -> ReservationConfirmed b+    }++initialDivertRegs :: RegFile DivertRegs+initialDivertRegs = RCons (Proxy @"wasBlack") False RNil++acuityRead :: Term DivertRegs DivertCmd '[ '("acuityBlack", Bool)] Bool+acuityRead = inpCtor inCtorConfirm ZIdx++confirmOut :: OutTerm DivertRegs DivertCmd DivertEvent+confirmOut = pack inCtorConfirm wireConfirmed (OFCons acuityRead OFNil)++recordAcuity :: Update DivertRegs '["wasBlack"] DivertCmd+recordAcuity = USet (#wasBlack :: IndexN "wasBlack" DivertRegs Bool) acuityRead++-- | The old rule: confirm any reservation.+oldGuard :: HsPred DivertRegs DivertCmd+oldGuard = matchInCtor inCtorConfirm++-- | The tightened rule: confirm only non-black acuity.+newGuard :: HsPred DivertRegs DivertCmd+newGuard = PAnd (matchInCtor inCtorConfirm) (PEq acuityRead (TLit False))++-- | The removed region, @old ∧ ¬new@: exactly black acuity.+removedRegionGuard :: HsPred DivertRegs DivertCmd+removedRegionGuard = PAnd (matchInCtor inCtorConfirm) (PEq acuityRead (TLit True))++confirmEdge :: HsPred DivertRegs DivertCmd -> EdgeMode -> Edge (HsPred DivertRegs DivertCmd) DivertRegs DivertCmd DivertEvent DivertVertex+confirmEdge g m =+  Edge+    { guard = g,+      update = recordAcuity,+      output = [confirmOut],+      target = Confirmed,+      mode = m+    }++divertMachine ::+  [Edge (HsPred DivertRegs DivertCmd) DivertRegs DivertCmd DivertEvent DivertVertex] ->+  SymTransducer (HsPred DivertRegs DivertCmd) DivertRegs DivertVertex DivertCmd DivertEvent+divertMachine heldEdges =+  SymTransducer+    { edgesOut = \case+        Held -> heldEdges+        Confirmed -> [],+      initial = Held,+      initialRegs = initialDivertRegs,+      isFinal = (== Confirmed)+    }++-- | Machine A: the original rule, before tightening.+machineA :: SymTransducer (HsPred DivertRegs DivertCmd) DivertRegs DivertVertex DivertCmd DivertEvent+machineA = divertMachine [confirmEdge oldGuard Live]++-- | Machine B without the twin: the tightened rule alone. Events+-- written under the old rule in the removed region lose their+-- inverting edge.+machineBBad :: SymTransducer (HsPred DivertRegs DivertCmd) DivertRegs DivertVertex DivertCmd DivertEvent+machineBBad = divertMachine [confirmEdge newGuard Live]++-- | Machine B with the replay-only twin carrying the removed region.+machineBGood :: SymTransducer (HsPred DivertRegs DivertCmd) DivertRegs DivertVertex DivertCmd DivertEvent+machineBGood =+  divertMachine+    [ confirmEdge newGuard Live,+      confirmEdge removedRegionGuard ReplayOnly+    ]++-- | A sloppy twin whose guard overlaps the live edge (it kept the whole+-- old guard instead of the complement). Its update is deliberately+-- distinguishable (constant 'True') so a test can tell which edge+-- applied during replay.+machineOverlap :: SymTransducer (HsPred DivertRegs DivertCmd) DivertRegs DivertVertex DivertCmd DivertEvent+machineOverlap =+  divertMachine+    [ confirmEdge newGuard Live,+      Edge+        { guard = oldGuard,+          update = USet (#wasBlack :: IndexN "wasBlack" DivertRegs Bool) (TLit True),+          output = [confirmOut],+          target = Confirmed,+          mode = ReplayOnly+        }+    ]++-- | Two replay-only edges competing for the same wire constructor with+-- overlapping guards: same-mode ambiguity must still be caught.+machineTwinClash :: SymTransducer (HsPred DivertRegs DivertCmd) DivertRegs DivertVertex DivertCmd DivertEvent+machineTwinClash =+  divertMachine+    [ confirmEdge oldGuard ReplayOnly,+      confirmEdge oldGuard ReplayOnly+    ]++-- | Both overlap edges live: the pre-existing checks must still flag.+machineLiveClash :: SymTransducer (HsPred DivertRegs DivertCmd) DivertRegs DivertVertex DivertCmd DivertEvent+machineLiveClash =+  divertMachine+    [ confirmEdge newGuard Live,+      confirmEdge oldGuard Live+    ]++-- | 'Confirmed' is reachable ONLY through the replay-only edge, and has+-- an outgoing live edge. Replay continuation makes that vertex live+-- (an old stream replays through the twin, then serves new commands),+-- so the dead-edge check must not flag its outgoing edges.+machineTwinOnlyPath :: SymTransducer (HsPred DivertRegs DivertCmd) DivertRegs DivertVertex DivertCmd DivertEvent+machineTwinOnlyPath =+  SymTransducer+    { edgesOut = \case+        Held -> [confirmEdge removedRegionGuard ReplayOnly]+        -- A live self-loop at the vertex reachable only via the twin.+        Confirmed -> [confirmEdge oldGuard Live],+      initial = Held,+      initialRegs = initialDivertRegs,+      isFinal = (== Confirmed)+    }++blackHistory :: [DivertEvent]+blackHistory = [ReservationConfirmed True]++-- * Builder surface --------------------------------------------------------++-- | The same twin-bearing machine written through "Keiki.Builder",+-- marking the twin with 'B.replayOnly'.+builderMachine :: SymTransducer (HsPred DivertRegs DivertCmd) DivertRegs DivertVertex DivertCmd DivertEvent+builderMachine =+  B.buildTransducer Held initialDivertRegs (== Confirmed) $ Prelude.do+    B.from Held Prelude.do+      B.onCmd inCtorConfirm $ \d -> B.do+        B.requireEq d.acuityBlack (TLit False)+        B.slot @"wasBlack" .= d.acuityBlack+        B.emit wireConfirmed (d.acuityBlack B.*: B.oNil)+        B.goto Confirmed+      B.onCmd inCtorConfirm $ \d -> B.do+        B.replayOnly+        B.requireEq d.acuityBlack (TLit True)+        B.slot @"wasBlack" .= d.acuityBlack+        B.emit wireConfirmed (d.acuityBlack B.*: B.oNil)+        B.goto Confirmed+    B.from Confirmed (Prelude.pure ())++-- * Specs ------------------------------------------------------------------++spec :: Spec+spec = do+  describe "forward stepping" $ do+    it "machine A accepts a black-acuity confirmation and emits its event" $+      case stepEither machineA (Held, initialDivertRegs) (ConfirmReservation True) of+        Right (v, regs, outs) -> do+          v `shouldBe` Confirmed+          regs ! #wasBlack `shouldBe` True+          outs `shouldBe` blackHistory+        Left failure -> expectationFailure ("machine A rejected: " <> show failure)++    it "never selects a ReplayOnly edge even when its guard models the command" $+      case stepEither machineBGood (Held, initialDivertRegs) (ConfirmReservation True) of+        Left (NoMatchingEdge Held rejected) ->+          -- Both edges are reported rejected: the live edge by its+          -- guard, the twin by its mode.+          map (edgeIndex . rejectedEdge) rejected `shouldBe` [0, 1]+        Left other -> expectationFailure ("expected NoMatchingEdge, got " <> show other)+        Right (v, _, outs) ->+          expectationFailure ("expected rejection, stepped to " <> show (v, outs))++    it "delta and omega agree that the removed region is rejected" $ do+      case delta machineBGood Held initialDivertRegs (ConfirmReservation True) of+        Nothing -> pure ()+        Just (v, _) -> expectationFailure ("delta stepped to " <> show v)+      omega machineBGood Held initialDivertRegs (ConfirmReservation True)+        `shouldBe` []++    it "still accepts commands under the tightened live rule" $+      case stepEither machineBGood (Held, initialDivertRegs) (ConfirmReservation False) of+        Right (v, regs, outs) -> do+          v `shouldBe` Confirmed+          regs ! #wasBlack `shouldBe` False+          outs `shouldBe` [ReservationConfirmed False]+        Left failure -> expectationFailure ("live edge rejected: " <> show failure)++    it "reports NoMatchingEdge (not NoOutgoingEdges) at a replay-only-only vertex" $+      case stepEither machineTwinOnlyPath (Held, initialDivertRegs) (ConfirmReservation True) of+        Left (NoMatchingEdge Held [rejected]) ->+          rejectedTarget rejected `shouldBe` Confirmed+        Left other -> expectationFailure ("expected one rejected edge, got " <> show other)+        Right (v, _, outs) ->+          expectationFailure ("expected rejection, stepped to " <> show (v, outs))++  describe "two-phase inversion" $ do+    it "black-acuity history fails to invert without the twin" $+      case reconstituteEither machineBBad blackHistory of+        Left failure -> do+          replayFailedIndex failure `shouldBe` 0+          case replayFailureReason failure of+            ReplayEventFailed (ReplayNoInvertingEdge Held _) -> pure ()+            other ->+              expectationFailure ("expected ReplayNoInvertingEdge, got " <> show other)+        Right result ->+          expectationFailure ("expected replay failure, got " <> show (fst result))++    it "black-acuity history inverts through the twin, applying its writes" $+      case reconstituteEither machineBGood blackHistory of+        Right (v, regs) -> do+          v `shouldBe` Confirmed+          regs ! #wasBlack `shouldBe` True+        Left failure -> expectationFailure ("twin replay failed: " <> show failure)++    it "replays machine A's history identically under the twin-bearing machine" $+      case (reconstituteEither machineA blackHistory, reconstituteEither machineBGood blackHistory) of+        (Right (vA, regsA), Right (vB, regsB)) ->+          (vB, regsB ! #wasBlack) `shouldBe` (vA, regsA ! #wasBlack)+        (Left failure, _) -> expectationFailure ("machine A replay failed: " <> show failure)+        (_, Left failure) -> expectationFailure ("machine B replay failed: " <> show failure)++    it "prefers the live edge when a sloppy twin's guard overlaps it" $+      case reconstituteEither machineOverlap [ReservationConfirmed False] of+        Right (v, regs) -> do+          v `shouldBe` Confirmed+          -- The live edge writes the event's own acuity (False); the+          -- sloppy twin would have written the constant True. Live wins.+          regs ! #wasBlack `shouldBe` False+        Left failure ->+          expectationFailure ("expected live-phase attribution: " <> show failure)++    it "falls through to the sloppy twin only for unattributable history" $+      case reconstituteEither machineOverlap blackHistory of+        Right (v, regs) -> do+          v `shouldBe` Confirmed+          regs ! #wasBlack `shouldBe` True+        Left failure -> expectationFailure ("twin fallthrough failed: " <> show failure)++    it "still reports ambiguity between two replay-only candidates" $+      case reconstituteEither machineTwinClash blackHistory of+        Left failure ->+          case replayFailureReason failure of+            ReplayEventFailed (ReplayAmbiguousInversions Held matchedEdges) ->+              map (edgeIndex . matchedEdge) matchedEdges `shouldBe` [0, 1]+            other ->+              expectationFailure ("expected ReplayAmbiguousInversions, got " <> show other)+        Right result ->+          expectationFailure ("expected ambiguity failure, got " <> show (fst result))++    it "applies the same two-phase preference in letter-only applyEvent" $ do+      case applyEvent machineBBad Held initialDivertRegs (ReservationConfirmed True) of+        Nothing -> pure ()+        Just (v, _) -> expectationFailure ("applyEvent inverted to " <> show v)+      case applyEvent machineBGood Held initialDivertRegs (ReservationConfirmed True) of+        Just (v, regs) -> do+          v `shouldBe` Confirmed+          regs ! #wasBlack `shouldBe` True+        Nothing -> expectationFailure "applyEvent could not use the twin"+      case applyEvent machineOverlap Held initialDivertRegs (ReservationConfirmed False) of+        Just (_, regs) -> regs ! #wasBlack `shouldBe` False+        Nothing -> expectationFailure "applyEvent could not use the live edge"++  describe "static checks" $ do+    it "does not flag a live/replay-only pair as an inversion ambiguity" $+      inversionAmbiguityWarnings machineBGood `shouldBe` []++    it "still flags a same-mode replay-only pair as an inversion ambiguity" $+      case inversionAmbiguityWarnings machineTwinClash of+        [InversionAmbiguity {tvwSource = Held, tvwEdgeA = 0, tvwEdgeB = 1}] -> pure ()+        other -> expectationFailure ("expected one same-mode warning, got " <> show other)++    it "does not flag a live/replay-only guard overlap as nondeterminism" $+      checkTransitionDeterminismPure machineOverlap `shouldBe` []++    it "still flags the same overlap when both edges are live" $+      case checkTransitionDeterminismPure machineLiveClash of+        [DeterminismWarning {dwSource = Held, dwEdgeA = 0, dwEdgeB = 1}] -> pure ()+        other -> expectationFailure ("expected one overlap warning, got " <> show other)++    it "keeps vertices reachable through replay-only edges out of the dead-edge report" $+      checkDeadEdges defaultDeadEdgeOptions machineTwinOnlyPath `shouldBe` []++    it "validates the twin-bearing black-acuity machine clean by default" $+      validateTransducer defaultValidationOptions machineBGood `shouldBe` []++    it "flags machineLiveClash through the default umbrella (control)" $+      validateTransducer defaultValidationOptions machineLiveClash+        `shouldNotBe` []++  describe "Keiki.Builder replayOnly" $ do+    it "marks the edge ReplayOnly and leaves unmarked edges Live" $+      map mode (edgesOut builderMachine Held) `shouldBe` [Live, ReplayOnly]++    it "behaves like the hand-written twin machine" $ do+      case stepEither builderMachine (Held, initialDivertRegs) (ConfirmReservation True) of+        Left (NoMatchingEdge Held _) -> pure ()+        Left other -> expectationFailure ("expected forward rejection, got " <> show other)+        Right (v, _, outs) ->+          expectationFailure ("expected rejection, stepped to " <> show (v, outs))+      case reconstituteEither builderMachine blackHistory of+        Right (v, regs) -> do+          v `shouldBe` Confirmed+          regs ! #wasBlack `shouldBe` True+        Left failure -> expectationFailure ("builder twin replay failed: " <> show failure)++  describe "EdgeMode combination" $ do+    it "is Live only when every component is Live" $ do+      Live <> Live `shouldBe` Live+      Live <> ReplayOnly `shouldBe` ReplayOnly+      ReplayOnly <> Live `shouldBe` ReplayOnly+      ReplayOnly <> ReplayOnly `shouldBe` ReplayOnly+      mempty `shouldBe` Live

@@ -364,7 +364,8 @@               { guard = PTop,                 update = UKeep,                 output = [],-                target = EpsilonDone+                target = EpsilonDone,+                mode = Live               }           ]         EpsilonDone -> []

@@ -18,12 +18,12 @@   SymTransducer     { edgesOut = \case         V0 ->-          [ Edge {guard = PTop, update = UKeep, output = [], target = VEnd},-            Edge {guard = PTop, update = UKeep, output = [], target = V3}+          [ Edge {guard = PTop, update = UKeep, output = [], target = VEnd, mode = Live},+            Edge {guard = PTop, update = UKeep, output = [], target = V3, mode = Live}           ]-        V1 -> [Edge {guard = PBot, update = UKeep, output = [], target = VEnd}]+        V1 -> [Edge {guard = PBot, update = UKeep, output = [], target = VEnd, mode = Live}]         V2 -> []-        V3 -> [Edge {guard = PTop, update = UKeep, output = [], target = VEnd}]+        V3 -> [Edge {guard = PTop, update = UKeep, output = [], target = VEnd, mode = Live}]         VEnd -> [],       initial = V0,       initialRegs = RNil,

@@ -68,8 +68,8 @@   SymTransducer     { edgesOut = \case         False ->-          [ Edge byteWrapGuard UKeep [] True,-            Edge byteHighGuard UKeep [] True+          [ Edge byteWrapGuard UKeep [] True Live,+            Edge byteHighGuard UKeep [] True Live           ]         True -> [],       initial = False,@@ -104,8 +104,8 @@   SymTransducer     { edgesOut = \case         False ->-          [ Edge timeAfterGuard UKeep [] True,-            Edge timeBeforeGuard UKeep [] True+          [ Edge timeAfterGuard UKeep [] True Live,+            Edge timeBeforeGuard UKeep [] True Live           ]         True -> [],       initial = False,@@ -137,13 +137,15 @@               { guard = PEq (proj amountIdx) (lit (0 :: Word64)),                 update = UKeep,                 output = [],-                target = True+                target = True,+                mode = Live               },             Edge               { guard = PEq (lit (5 :: Word64)) (lit (6 :: Word64)),                 update = UKeep,                 output = [],-                target = True+                target = True,+                mode = Live               }           ]         True -> [],@@ -177,13 +179,15 @@               { guard = PEq (proj amountIdx) (lit (0 :: Word64)),                 update = UKeep,                 output = [],-                target = True+                target = True,+                mode = Live               },             Edge               { guard = PEq (proj amountIdx) (lit (1 :: Word64)),                 update = UKeep,                 output = [],-                target = True+                target = True,+                mode = Live               }           ]         True -> [],@@ -739,13 +743,15 @@               { guard = SymPred (PInCtor inCtorTinyFoo),                 update = UKeep,                 output = [],-                target = True+                target = True,+                mode = Live               },             Edge               { guard = SymPred (PInCtor inCtorTinyBar),                 update = UKeep,                 output = [],-                target = True+                target = True,+                mode = Live               }           ]         True -> [],@@ -765,13 +771,15 @@               { guard = SymPred PTop,                 update = UKeep,                 output = [],-                target = True+                target = True,+                mode = Live               },             Edge               { guard = SymPred PTop,                 update = UKeep,                 output = [],-                target = True+                target = True,+                mode = Live               }           ]         True -> [],

@@ -82,7 +82,8 @@                       wireLogged                       (TInpCtorField inCtorX (#value :: Index AmbiguousFields Int) *: oNil)                   ],-                target = True+                target = True,+                mode = Live               },             Edge               { guard = matchInCtor inCtorY,@@ -93,7 +94,8 @@                       secondWire                       (TInpCtorField inCtorY (#value :: Index AmbiguousFields Int) *: oNil)                   ],-                target = True+                target = True,+                mode = Live               }           ]         True -> [],@@ -122,7 +124,8 @@                     (#seen :: IndexN "seen" ReadRegs Int)                     (TInpCtorField inCtorX (#value :: Index AmbiguousFields Int)),                 output = [],-                target = True+                target = True,+                mode = Live               }           ]         True -> [],@@ -169,13 +172,13 @@         EpsilonStart ->           case epsilonCase of             ChangesVertexOnly ->-              [Edge (matchInCtor inCtorX) UKeep [] EpsilonEnd]+              [Edge (matchInCtor inCtorX) UKeep [] EpsilonEnd Live]             WritesRegistersOnly ->-              [Edge (matchInCtor inCtorX) setSeen [] EpsilonStart]+              [Edge (matchInCtor inCtorX) setSeen [] EpsilonStart Live]             ChangesBoth ->-              [Edge (matchInCtor inCtorX) setSeen [] EpsilonEnd]+              [Edge (matchInCtor inCtorX) setSeen [] EpsilonEnd Live]             NoOpSelfLoop ->-              [Edge (matchInCtor inCtorX) UKeep [] EpsilonStart]+              [Edge (matchInCtor inCtorX) UKeep [] EpsilonStart Live]         EpsilonEnd -> [],       initial = EpsilonStart,       initialRegs = RCons (Proxy @"seen") 0 RNil,

@@ -56,8 +56,8 @@   SymTransducer     { edgesOut = \case         Start ->-          [ Edge {guard = PTop, update = UKeep, output = [], target = Mid},-            Edge {guard = PTop, update = UKeep, output = [], target = Mid}+          [ Edge {guard = PTop, update = UKeep, output = [], target = Mid, mode = Live},+            Edge {guard = PTop, update = UKeep, output = [], target = Mid, mode = Live}           ]         _ -> [],       initial = Start,@@ -70,8 +70,8 @@ deadT =   SymTransducer     { edgesOut = \case-        Start -> [Edge {guard = matchInCtor inCtorFoo, update = UKeep, output = [], target = Mid}]-        Orphan -> [Edge {guard = PTop, update = UKeep, output = [], target = Start}]+        Start -> [Edge {guard = matchInCtor inCtorFoo, update = UKeep, output = [], target = Mid, mode = Live}]+        Orphan -> [Edge {guard = PTop, update = UKeep, output = [], target = Start, mode = Live}]         _ -> [],       initial = Start,       initialRegs = RNil,@@ -83,7 +83,7 @@ botT =   SymTransducer     { edgesOut = \case-        Start -> [Edge {guard = PBot, update = UKeep, output = [], target = Mid}]+        Start -> [Edge {guard = PBot, update = UKeep, output = [], target = Mid, mode = Live}]         _ -> [],       initial = Start,       initialRegs = RNil,@@ -98,8 +98,8 @@   SymTransducer     { edgesOut = \case         Start ->-          [ Edge {guard = matchInCtor inCtorFoo, update = UKeep, output = [pack inCtorFoo wireFooed oNil], target = Mid},-            Edge {guard = matchInCtor inCtorBar, update = UKeep, output = [pack inCtorBar wireBared oNil], target = Mid}+          [ Edge {guard = matchInCtor inCtorFoo, update = UKeep, output = [pack inCtorFoo wireFooed oNil], target = Mid, mode = Live},+            Edge {guard = matchInCtor inCtorBar, update = UKeep, output = [pack inCtorBar wireBared oNil], target = Mid, mode = Live}           ]         _ -> [],       initial = Start,@@ -116,8 +116,8 @@   SymTransducer     { edgesOut = \case         Start ->-          [ Edge {guard = matchInCtor inCtorFoo, update = UKeep, output = [], target = Mid},-            Edge {guard = PTop, update = UKeep, output = [], target = Mid}+          [ Edge {guard = matchInCtor inCtorFoo, update = UKeep, output = [], target = Mid, mode = Live},+            Edge {guard = PTop, update = UKeep, output = [], target = Mid, mode = Live}           ]         _ -> [],       initial = Start,@@ -143,7 +143,8 @@                     (TLit True),                 update = UKeep,                 output = [pack inCtorFoo wireFooed oNil],-                target = Mid+                target = Mid,+                mode = Live               }           ]         _ -> [],@@ -201,7 +202,8 @@                           (OFCons (TInpCtorField inCtorBegin (#b :: Index '[ '("a", Int), '("b", Int), '("c", Int)] Int)) OFNil)                       )                   ],-                target = True+                target = True,+                mode = Live               }           ]         True -> [],@@ -226,8 +228,8 @@   SymTransducer     { edgesOut = \case         Start ->-          [ Edge leftGuard UKeep [] Start,-            Edge rightGuard UKeep [] Start+          [ Edge leftGuard UKeep [] Start Live,+            Edge rightGuard UKeep [] Start Live           ]         _ -> [],       initial = Start,@@ -301,7 +303,8 @@               )               UKeep               []-              Start,+              Start+              Live,             Edge               ( PAnd                   (PInCtor inCtorFoo)@@ -310,6 +313,7 @@               UKeep               []               Start+              Live           ]         _ -> [],       initial = Start,@@ -332,12 +336,14 @@               (PAnd (PInCtor inCtorFoo) (PEq (proj boolOverlapIdx) (TLit True)))               UKeep               []-              Start,+              Start+              Live,             Edge               (PAnd (PInCtor inCtorFoo) (PEq (TLit True) (proj boolOverlapIdx)))               UKeep               []               Start+              Live           ]         _ -> [],       initial = Start,

@@ -32,6 +32,7 @@ import Keiki.Render.PrettySpec qualified import Keiki.Render.ValidateSpec qualified import Keiki.ReplayEitherSpec qualified+import Keiki.ReplayOnlySpec qualified import Keiki.RoundTripSpec qualified import Keiki.ShapeSpec qualified import Keiki.StepEitherSpec qualified@@ -72,6 +73,7 @@   describe "Keiki.RecomputeVerify (EP-47)" Keiki.RecomputeVerifySpec.spec   describe "Keiki.RoundTrip (EP-73)" Keiki.RoundTripSpec.spec   describe "Keiki.Core structured replay (EP-72)" Keiki.ReplayEitherSpec.spec+  describe "Keiki.Core replay-only edges (keiro MP-24 EP-6)" Keiki.ReplayOnlySpec.spec   describe "Keiki.Render.Inspector (EP-62)" Keiki.Render.InspectorSpec.spec   describe "Keiki.Render.Markdown (EP-65)" Keiki.Render.MarkdownSpec.spec   describe "Keiki.Render.Mermaid (EP-30, EP-31, EP-32, EP-33)" Keiki.Render.MermaidSpec.spec