keiki 0.7.0.0 → 0.8.0.0

raw patch · 16 files changed

+987/−215 lines, 16 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +30/−0
• README.md +11/−4
• keiki.cabal +1/−1
• src/Keiki/Composition.hs +16/−4
• src/Keiki/Core.hs +61/−25
• src/Keiki/Profunctor.hs +3/−0
• src/Keiki/Render/Inspector.hs +3/−3
• src/Keiki/Render/Mermaid.hs +268/−108
• src/Keiki/Render/Pretty.hs +10/−9
• src/Keiki/Symbolic.hs +3/−1
• test/Keiki/CompositionAlignmentSpec.hs +36/−9
• test/Keiki/CoreSpec.hs +218/−0
• test/Keiki/Render/MermaidSpec.hs +256/−45
• test/Keiki/Render/PrettySpec.hs +10/−6
• test/Keiki/SymbolicSpec.hs +43/−0
• test/Keiki/ValidationSpec.hs +18/−0

@@ -9,6 +9,36 @@ ## [Unreleased]  +## [0.8.0.0] — 2026-08-02++### Added++- `TOpaqueLit` and `opaqueLit` preserve exact concrete, replay, pure-analysis,+  and symbolic literal semantics while deliberately rendering the stored value+  as `<lit>`.+- `MermaidUpdateMode`, `topologyMermaidOptions`, and `toTopologyMermaid` make+  complete updates, compact written-slot summaries, and Keiki 0.7-compatible+  topology output explicit policies.+- Options-aware Mermaid entry points now cover composite, nested, three-way,+  alternative, feedback, and labeled diagrams. Backend-level regression tests+  pin semantic-label escaping through the documentation site's+  `beautiful-mermaid` renderer.++### Changed++- **Breaking:** `TLit` and `lit` now require `Show` so renderers derive ordinary+  literal text from the executable value. Exhaustive `Term` matches must handle+  `TOpaqueLit`; values without `Show`, secrets, and deliberately redacted values+  use `opaqueLit`.+- **Breaking:** `toMermaid` and every no-options shape renderer now default to+  readable guards, complete register assignments, multiline labels, and no+  semantic truncation. Use `toTopologyMermaid` or an options-aware shape+  renderer with `topologyMermaidOptions` for the previous compact bytes.+- **Breaking:** `MermaidOptions` removes `showWrittenSlots` and+  `showGuardSummary`. Set `updateMode = MermaidUpdateWrittenSlots` and+  `guardMode = MermaidGuardStructuralSummary` respectively.++ ## [0.7.0.0] — 2026-08-01  ### Added

@@ -56,7 +56,8 @@ - per-vertex projections (the "B-presentation" view), - checked sequential composition (`composeChecked`) plus `alternative` and `feedback1`, - profunctor / `Category` / `Strong` / `Choice` / `Arrow` instances,-- Mermaid and Markdown renderers for documentation,+- behavior-readable Mermaid and Markdown renderers, with explicit compact+  topology output, - eager builder validation, default-on replay-safety checks, and optional   single-valuedness checks via SBV + z3. @@ -66,9 +67,9 @@  ## Status -Pre-1.0, prepared for the initial `0.1.0.0` Hackage release. The-planned v0.1 surface is implemented and validated against in-tree tests-plus the downstream `jitsurei` worked-example package.+Pre-1.0 and released under the Haskell PVP. The current surface is validated+against the in-tree suites plus the downstream `jitsurei` worked-example+package; see [`CHANGELOG.md`](CHANGELOG.md) for release history and migrations.  The core package is intentionally codec-free. JSON support lives in [`keiki-codec-json`](keiki-codec-json/README.md), and downstream codec@@ -117,6 +118,12 @@ 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.++The primary `toMermaid emailDelivery` diagram is derived from the same edge AST+and shows its command, event constructor, complete register assignments, and+guard. Use `toTopologyMermaid emailDelivery` when only shape is intended.+Ordinary `lit` values appear in readable diagrams; model a value with+`opaqueLit` when it lacks `Show` or must remain redacted.  ## Repository documentation 

@@ -1,6 +1,6 @@ cabal-version:   3.0 name:            keiki-version:         0.7.0.0+version:         0.8.0.0 synopsis:        Pure core for symbolic-register transducer event sourcing. description:   A Haskell library for the pure core of event sourcing, workflow

@@ -248,12 +248,13 @@ weakenL (SIdx i) = SIdx (weakenL @_ @rs2 i)  -- | Walk a 'Term' and weaken every register read across an rs2--- suffix. 'TInpCtorField' / 'TLit' do not touch the register file,+-- suffix. 'TInpCtorField', 'TLit', and 'TOpaqueLit' do not touch the register file, -- so they pass through unchanged. weakenLTerm ::   forall rs1 rs2 ci ifs r.   Term rs1 ci ifs r -> Term (Append rs1 rs2) ci ifs r weakenLTerm (TLit r) = TLit r+weakenLTerm (TOpaqueLit r) = TOpaqueLit r weakenLTerm (TReg ix) = TReg (weakenL @rs1 @rs2 ix) weakenLTerm (TInpCtorField ic ix) = TInpCtorField ic ix weakenLTerm (TApp1 f t) = TApp1 f (weakenLTerm @rs1 @rs2 t)@@ -331,6 +332,7 @@   (WeakenR rs1) =>   Term rs2 ci ifs r -> Term (Append rs1 rs2) ci ifs r weakenRTerm (TLit r) = TLit r+weakenRTerm (TOpaqueLit r) = TOpaqueLit r weakenRTerm (TReg ix) = TReg (weakenR @rs1 ix) weakenRTerm (TInpCtorField ic ix) = TInpCtorField ic ix weakenRTerm (TApp1 f t) = TApp1 f (weakenRTerm @rs1 @rs2 t)@@ -466,12 +468,13 @@ -- 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 ())+poisonTerm message = TApp1 (\() -> error message) (TOpaqueLit ())  -- | 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 _ (TOpaqueLit _) = False termHasCtorMismatch _ (TReg _) = False termHasCtorMismatch expected (TInpCtorField ic _) = icName ic /= expected termHasCtorMismatch expected (TApp1 _ term) = termHasCtorMismatch expected term@@ -500,6 +503,7 @@   OutTerm rs1 ci1 mid ->   Term (Append rs1 rs2) ci1 ifsR r substTerm (TLit r) _o1 = TLit r+substTerm (TOpaqueLit r) _o1 = TOpaqueLit r substTerm (TReg ix2) _o1 = TReg (weakenR @rs1 ix2) substTerm (TInpCtorField ic2 ix2) o1 =   substInputField @rs1 @rs2 ic2 ix2 o1@@ -593,7 +597,9 @@ projectThroughTermWithStatus witness (TInpCtorField ic ix) =   (TFieldProj witness (PBInp ic ix), ProjectionPreserved) projectThroughTermWithStatus witness (TLit owner) =-  (TLit (fieldWitnessGet witness owner), ProjectionFolded)+  (TOpaqueLit (fieldWitnessGet witness owner), ProjectionFolded)+projectThroughTermWithStatus witness (TOpaqueLit owner) =+  (TOpaqueLit (fieldWitnessGet witness owner), ProjectionFolded) projectThroughTermWithStatus witness ownerTerm =   (TApp1 (fieldWitnessGet witness) ownerTerm, ProjectionLowered) @@ -805,12 +811,13 @@  -- | Lift a 'Term' from the left side's input alphabet to -- @Either ci1 ci2@. Walks the AST and adjusts every 'TInpCtorField'--- to read through 'leftInCtor'. 'TLit' / 'TReg' don't depend on+-- to read through 'leftInCtor'. Literals and 'TReg' don't depend on -- @ci@ and pass through unchanged. liftLTermAlt ::   forall rs ci1 ci2 ifs r.   Term rs ci1 ifs r -> Term rs (Either ci1 ci2) ifs r liftLTermAlt (TLit r) = TLit r+liftLTermAlt (TOpaqueLit r) = TOpaqueLit r liftLTermAlt (TReg ix) = TReg ix liftLTermAlt (TInpCtorField ic ix) = TInpCtorField (leftInCtor ic) ix liftLTermAlt (TApp1 f t) = TApp1 f (liftLTermAlt @rs @ci1 @ci2 t)@@ -829,6 +836,7 @@   forall rs ci1 ci2 ifs r.   Term rs ci2 ifs r -> Term rs (Either ci1 ci2) ifs r liftRTermAlt (TLit r) = TLit r+liftRTermAlt (TOpaqueLit r) = TOpaqueLit r liftRTermAlt (TReg ix) = TReg ix liftRTermAlt (TInpCtorField ic ix) = TInpCtorField (rightInCtor ic) ix liftRTermAlt (TApp1 f t) = TApp1 f (liftRTermAlt @rs @ci1 @ci2 t)@@ -1104,6 +1112,7 @@   Term rs ci ifs r ->   Term rs ci ifs r applyEnvTerm _ (TLit r) = TLit r+applyEnvTerm _ (TOpaqueLit r) = TOpaqueLit 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)@@ -1251,6 +1260,7 @@  termExpectedReads :: Term rs ci ifs r -> [(String, Int)] termExpectedReads (TLit _) = []+termExpectedReads (TOpaqueLit _) = [] termExpectedReads (TReg _) = [] termExpectedReads (TInpCtorField ic ix) = [(icName ic, indexInt ix)] termExpectedReads (TApp1 _ term) = termExpectedReads term@@ -1341,6 +1351,7 @@      goTerm :: forall ifs r. Term rs2 mid ifs r -> [ComposeAlignmentWarning s1 s2]     goTerm (TLit _) = []+    goTerm (TOpaqueLit _) = []     goTerm (TReg _) = []     goTerm (TInpCtorField _ _) = []     goTerm (TApp1 _ term) = goTerm term@@ -1393,6 +1404,7 @@      goTerm :: forall ifs r. Term rs ci ifs r -> [ComposeAlignmentWarning s1 s2]     goTerm (TLit _) = []+    goTerm (TOpaqueLit _) = []     goTerm (TReg _) = []     goTerm (TInpCtorField _ _) = []     goTerm (TApp1 _ term) = goTerm term

@@ -119,6 +119,7 @@     regProj,     inpProj,     lit,+    opaqueLit,     tadd,     tsub,     tmul,@@ -536,7 +537,7 @@ -- 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+-- ('TLit', 'TOpaqueLit', '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@@ -545,7 +546,12 @@ -- 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+  -- | An ordinary literal. The 'Show' dictionary is presentation evidence+  -- retained for renderers; evaluation and proof paths use only the value.+  TLit :: (Show r) => r -> Term rs ci ifs r+  -- | A display-opaque literal. It has the same concrete and symbolic meaning+  -- as 'TLit' but renderers deliberately do not expose its value.+  TOpaqueLit :: 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@@ -1032,10 +1038,16 @@   Term rs ci ifs (FieldResult projection) inpProj witness ic ix = TFieldProj witness (PBInp ic ix) --- | A constant 'Term'.-lit :: r -> Term rs ci ifs r+-- | A readable constant 'Term'. Renderers derive its text from 'show'; use+-- 'opaqueLit' when the value has no 'Show' instance or must remain redacted.+lit :: (Show r) => r -> Term rs ci ifs r lit = TLit +-- | A display-opaque constant 'Term'. This changes presentation only: concrete+-- evaluation and symbolic translation still treat the stored value exactly.+opaqueLit :: r -> Term rs ci ifs r+opaqueLit = TOpaqueLit+ -- | 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@@ -1137,6 +1149,7 @@ -- | 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 (TOpaqueLit r) _ _ = r evalTerm (TReg ix) regs _ = regs ! ix evalTerm (TInpCtorField ic ix) _ ci = case icMatch ic ci of   Just rf -> rf ! ix@@ -2022,7 +2035,8 @@ -- == Recompute-and-verify (EP-47) -- -- The command is recovered from the /invertible/ fields alone--- (@TLit@\/@TReg@\/@TInpCtorField@); /derived/ fields (@TArith@\/@TApp1@\/+-- (@TLit@\/@TOpaqueLit@\/@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@@ -2067,7 +2081,7 @@ -- | 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+-- /invertible/ field ('TLit'\/'TOpaqueLit'\/'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/@@ -2091,7 +2105,7 @@  -- | 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+-- the /invertible/ fields. 'TLit'\/'TOpaqueLit'\/'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@@ -2127,6 +2141,7 @@   where     stepOne :: forall f. Term rs ci ifs f -> f -> InCtor ci ifs -> Maybe [ByIndex ifs]     stepOne (TLit _) _val _ = Just []+    stepOne (TOpaqueLit _) _val _ = Just []     stepOne (TReg _) _val _ = Just []     stepOne (TInpCtorField ic2 ix) val ic1       | icName ic1 == icName ic2 = Just [ByIndex ix val]@@ -2322,6 +2337,7 @@ -- | Does the 'Term' read the input symbol via 'TInpCtorField'? termReadsInput :: Term rs ci ifs r -> Bool termReadsInput (TLit _) = False+termReadsInput (TOpaqueLit _) = False termReadsInput (TReg _) = False termReadsInput (TInpCtorField _ _) = True termReadsInput (TApp1 _ t) = termReadsInput t@@ -2338,6 +2354,7 @@   where     termHasInpCtorField :: Term rs ci ifs r -> Bool     termHasInpCtorField (TLit _) = False+    termHasInpCtorField (TOpaqueLit _) = False     termHasInpCtorField (TReg _) = False     termHasInpCtorField (TInpCtorField _ _) = True     termHasInpCtorField (TApp1 _ t') = termHasInpCtorField t'@@ -2710,6 +2727,7 @@ -- deliberately falls back to a fresh domain-valid value. termHasOpaqueFallback :: forall rs ci ifs r. Term rs ci ifs r -> Bool termHasOpaqueFallback (TLit _) = False+termHasOpaqueFallback (TOpaqueLit _) = False termHasOpaqueFallback (TReg _) = False termHasOpaqueFallback (TInpCtorField _ _) = False termHasOpaqueFallback (TApp1 _ _) = True@@ -2774,6 +2792,7 @@  termProjectionInfos :: Term rs ci ifs r -> [ProjectionInfo] termProjectionInfos (TLit _) = []+termProjectionInfos (TOpaqueLit _) = [] termProjectionInfos (TReg _) = [] termProjectionInfos (TInpCtorField _ _) = [] termProjectionInfos (TApp1 _ term) = termProjectionInfos term@@ -2905,6 +2924,7 @@  termInCtorNames :: Term rs ci ifs r -> [String] termInCtorNames (TLit _) = []+termInCtorNames (TOpaqueLit _) = [] termInCtorNames (TReg _) = [] termInCtorNames (TInpCtorField ic _) = [icName ic] termInCtorNames (TApp1 _ t) = termInCtorNames t@@ -3094,8 +3114,9 @@ -- -- 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+-- cannot compare differing literal values without the 'Eq' or 'Typeable'+-- evidence supplied by a predicate constructor; 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@@ -3311,17 +3332,27 @@   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 =+pureEquality left right+  | Just a <- termLiteralValue left,+    Just b <- termLiteralValue right,+    a == b =+      PureKnown emptyPureGuard+  | Just _ <- termLiteralValue left,+    Just _ <- termLiteralValue right =+      PureUnsatisfiable+  | Just literalValue <- termLiteralValue right,+    Just name <- pureVariable left =       knownComparison name PureEq literalValue (== literalValue)-pureEquality (TLit literalValue) variable-  | Just name <- pureVariable variable =+  | Just literalValue <- termLiteralValue left,+    Just name <- pureVariable right =       knownComparison name PureEq literalValue (== literalValue)-pureEquality _ _ = PureUnknown+  | otherwise = PureUnknown +termLiteralValue :: Term rs ci ifs r -> Maybe r+termLiteralValue (TLit value) = Just value+termLiteralValue (TOpaqueLit value) = Just value+termLiteralValue _ = Nothing+ pureOrdering ::   forall rs ci ifs1 ifs2 r.   (Ord r, Typeable r) =>@@ -3329,26 +3360,31 @@   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 =+pureOrdering relation left right+  | Just a <- termLiteralValue left,+    Just b <- termLiteralValue right,+    applyPureCmp relation a b =+      PureKnown emptyPureGuard+  | Just _ <- termLiteralValue left,+    Just _ <- termLiteralValue right =+      PureUnsatisfiable+  | Just literalValue <- termLiteralValue right,+    Just name <- pureVariable left =       let normalized = pureRelation relation        in knownComparison             name             normalized             literalValue             (\value -> applyPureRelation normalized value literalValue)-pureOrdering relation (TLit literalValue) variable-  | Just name <- pureVariable variable =+  | Just literalValue <- termLiteralValue left,+    Just name <- pureVariable right =       let normalized = flipPureRelation (pureRelation relation)        in knownComparison             name             normalized             literalValue             (\value -> applyPureRelation normalized value literalValue)-pureOrdering _ _ _ = PureUnknown+  | otherwise = PureUnknown  knownComparison ::   (Typeable r) =>

@@ -762,6 +762,7 @@           Term rs ci ifs a ->           Term rs (ci, c) ('("snd", c) ': ifs) a         goTerm (TLit r) = TLit r+        goTerm (TOpaqueLit r) = TOpaqueLit r         goTerm (TReg ix) = TReg ix         goTerm (TInpCtorField _ ix) = TInpCtorField cic (SIdx ix)         goTerm (TApp1 h a) = TApp1 h (goTerm a)@@ -956,6 +957,7 @@   where     go :: forall a. Term rs ci ifs a -> Term rs ci' ifs a     go (TLit r) = TLit r+    go (TOpaqueLit r) = TOpaqueLit r     go (TReg ix) = TReg ix     go (TInpCtorField ic ix) = TInpCtorField (contraInCtor f ic) ix     go (TApp1 h a) = TApp1 h (go a)@@ -971,6 +973,7 @@   where     go :: forall a. Term rs ci ifs a -> Term rs ci' ifs a     go (TLit r) = TLit r+    go (TOpaqueLit r) = TOpaqueLit r     go (TReg ix) = TReg ix     go (TInpCtorField ic ix) = TInpCtorField (contraMaybeInCtor f ic) ix     go (TApp1 h a) = TApp1 h (go a)

@@ -1,7 +1,7 @@ -- | A Markdown edge-detail renderer for 'SymTransducer', a sibling to--- the Mermaid topology renderer in "Keiki.Render.Mermaid". Where--- 'Keiki.Render.Mermaid.toMermaid' shows the /shape/ of a workflow (one--- line per edge), this renderer lays out every edge in /full/: its+-- the behavioral Mermaid renderer in "Keiki.Render.Mermaid". Where+-- 'Keiki.Render.Mermaid.toMermaid' keeps executable behavior compact in+-- one transition label, this renderer expands every edge's metadata: its -- source and target states, its 0-based edge index, the input -- (command) constructor, the output (event) constructor(s), the guard -- predicate (structural and/or domain-readable), the register slots it

@@ -8,8 +8,8 @@ -- -- The rendered output is a @stateDiagram-v2@ block as 'Data.Text.Text'. -- It can be pasted into a Markdown file or Notion page; GitHub renders--- Mermaid blocks inline so PR reviewers see the topology diff alongside--- the source diff.+-- Mermaid blocks inline so PR reviewers see executable guard and update+-- semantics alongside the topology and source diff. -- -- The renderer is specialised to @phi ~ 'HsPred' rs ci@ — extracting -- the input-constructor name from an edge guard requires walking the@@ -24,13 +24,20 @@ --     for the initiative motivation. module Keiki.Render.Mermaid   ( toMermaid,+    toTopologyMermaid,     toMermaidAlternative,     toMermaidAlternativeWith,+    toMermaidAlternativeWithOptions,     toMermaidComposite,+    toMermaidCompositeWith,     toMermaidCompositeNested,+    toMermaidCompositeNestedWith,     toMermaidCompose3,+    toMermaidCompose3With,     toMermaidCompose3Nested,+    toMermaidCompose3NestedWith,     toMermaidFeedback1,+    toMermaidFeedback1With,     toMermaidAtlas,     toMermaidAtlasWith,     MermaidSection (..),@@ -42,11 +49,13 @@     toMermaidWithLabels,     MermaidOptions (..),     MermaidGuardMode (..),+    MermaidUpdateMode (..),     MermaidLabelLayout (..),     MermaidOutputLayout (..),     MermaidStateLabels (..),     duplicateStateIds,     defaultMermaidOptions,+    topologyMermaidOptions,     vertexLabel,     compositeLabel,     compose3Label,@@ -73,7 +82,7 @@   ) import Keiki.Generics (Append) import Keiki.Internal.Slots (indexNName)-import Keiki.Render.Pretty (prettyPred)+import Keiki.Render.Pretty (prettyPred, prettyUpdate)  -- | How an edge's guard predicate is rendered into the @[g: …]@ -- segment.@@ -81,7 +90,7 @@ --   * 'MermaidGuardHidden' — no guard segment at all. --   * 'MermaidGuardStructuralSummary' — the structural constructor-tag --     walk produced by 'guardSummary', e.g. @PAnd PInCtor PEq@. This is---     the legacy rendering that the 'showGuardSummary' flag selects.+--     the compact structural alternative to readable guards. --   * 'MermaidGuardPretty' — the domain-readable rendering produced by --     'Keiki.Render.Pretty.prettyPred', e.g. --     @(ConfirmAccount && ConfirmAccount.confirmCode == confirmCode)@.@@ -91,6 +100,19 @@   | MermaidGuardPretty   deriving stock (Eq, Show) +-- | How an edge's register update is rendered.+--+--   * 'MermaidUpdateHidden' — no update segment at all.+--   * 'MermaidUpdateWrittenSlots' — only the names of written slots,+--     retained as a compact compatibility option.+--   * 'MermaidUpdatePretty' — the complete update produced by+--     'Keiki.Render.Pretty.prettyUpdate', including right-hand terms.+data MermaidUpdateMode+  = MermaidUpdateHidden+  | MermaidUpdateWrittenSlots+  | MermaidUpdatePretty+  deriving stock (Eq, Show)+ -- | How dense edge labels are laid out. -- --   * 'MermaidLabelInline' — the current single-line @[seg; seg]@ form.@@ -116,32 +138,18 @@   | MermaidOutputCounted   deriving stock (Eq, Show) --- | Rendering options for the structural edge-summary suffix. All--- fields default to the no-suffix setting in 'defaultMermaidOptions', so--- the default rendering is byte-identical to 'toMermaid'.+-- | Rendering options for edge semantics and layout. ----- The record is extended /additively/: new fields are appended with a--- default that reproduces the existing behaviour, and existing fields--- are never removed or reordered. The legacy 'showGuardSummary' flag and--- the newer 'guardMode' field are reconciled by 'renderGuardSegment' (an--- explicit 'guardMode' wins; otherwise 'showGuardSummary' is honoured as--- the legacy spelling of 'MermaidGuardStructuralSummary').+-- 'defaultMermaidOptions' is the readable primary policy: complete guards+-- and updates, multiline labels, and no semantic truncation.+-- 'topologyMermaidOptions' is the explicit compact compatibility policy and+-- reproduces Keiki 0.7's topology-only bytes. data MermaidOptions = MermaidOptions-  { -- | When 'True', append the update's written-slot names, e.g.-    --     @[w: email; confirmCode; registeredAt]@.-    showWrittenSlots :: Bool,-    -- | When 'True', append a structural guard summary listing the-    --     guard's constructor / comparison tags, e.g. @[g: PAnd PInCtor PEq]@.-    --     This is the legacy spelling of @'guardMode' = 'MermaidGuardStructuralSummary'@;-    --     it is honoured only when 'guardMode' is left at its default-    --     ('MermaidGuardHidden').-    showGuardSummary :: Bool,-    -- | How the guard segment is rendered. When set to anything other-    --     than 'MermaidGuardHidden', it takes precedence over the legacy-    --     'showGuardSummary' flag. Defaults to 'MermaidGuardHidden'.+  { -- | How the guard segment is rendered.     guardMode :: MermaidGuardMode,-    -- | Inline (default, byte-identical) or multiline @<br/>@ layout-    --     of an edge label's segments. Defaults to 'MermaidLabelInline'.+    -- | How the register-update segment is rendered.+    updateMode :: MermaidUpdateMode,+    -- | Inline bracketed segments or multiline @<br/>@ layout.     labelLayout :: MermaidLabelLayout,     -- | When @'Just' k@ and an edge writes @n > k@ slots, show the     --     first @k@ then a single @+{n-k} more@ token. 'Nothing' (the@@ -157,14 +165,26 @@     outputLayout :: MermaidOutputLayout   } --- | The default: no summary suffix. @'toMermaid' t@ equals--- @'toMermaidWith' 'defaultMermaidOptions' t@.+-- | The readable primary policy used by every no-options renderer. defaultMermaidOptions :: MermaidOptions defaultMermaidOptions =   MermaidOptions-    { showWrittenSlots = False,-      showGuardSummary = False,-      guardMode = MermaidGuardHidden,+    { guardMode = MermaidGuardPretty,+      updateMode = MermaidUpdatePretty,+      labelLayout = MermaidLabelMultiline,+      maxInlineWrittenSlots = Nothing,+      maxInlineGuardWidth = Nothing,+      outputLayout = MermaidOutputSemicolon+    }++-- | Keiki 0.7's compact topology-only policy. This is intentionally a+-- separate named value rather than an implicit default so callers make the+-- loss of business semantics explicit.+topologyMermaidOptions :: MermaidOptions+topologyMermaidOptions =+  MermaidOptions+    { guardMode = MermaidGuardHidden,+      updateMode = MermaidUpdateHidden,       labelLayout = MermaidLabelInline,       maxInlineWrittenSlots = Nothing,       maxInlineGuardWidth = Nothing,@@ -178,22 +198,27 @@ -- 'show'. The output begins with @stateDiagram-v2@, followed by an -- initial-state line (@[*] --> <initial>@), one line per outgoing -- edge of every vertex, and a final-state line (@<vertex> --> [*]@)--- for every vertex where 'isFinal' returns 'True'. Edge labels follow--- the format described by 'edgeLabel'.+-- for every vertex where 'isFinal' returns 'True'. The readable default+-- adds complete update and guard segments on renderer-owned @<br/>@ lines;+-- use 'toTopologyMermaid' for the compact 'edgeLabel' form. toMermaid ::   (Enum s, Bounded s, Show s) =>   SymTransducer (HsPred rs ci) rs s ci co ->   Text toMermaid = toMermaidWith defaultMermaidOptions --- | Like 'toMermaid', but takes 'MermaidOptions' controlling the--- structural edge-summary suffix. @'toMermaidWith' 'defaultMermaidOptions'@--- is byte-identical to 'toMermaid'. With 'showWrittenSlots' and/or--- 'showGuardSummary' enabled, each edge label gains a compact bracketed--- suffix, e.g. @… [w: email; confirmCode; registeredAt; g: PAnd PInCtor PTop]@.------ Only the single-transducer path is annotated; the composite renderers--- ('toMermaidComposite' and relatives) keep the guard-free default.+-- | Render only topology using Keiki 0.7's compact label policy. Use this+-- when guards and register assignments are intentionally out of scope.+toTopologyMermaid ::+  (Enum s, Bounded s, Show s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  Text+toTopologyMermaid = toMermaidWith topologyMermaidOptions++-- | Like 'toMermaid', but takes the complete edge-semantics and layout+-- policy explicitly. @'toMermaidWith' 'defaultMermaidOptions'@ is+-- byte-identical to 'toMermaid'; use 'topologyMermaidOptions' for the+-- Keiki 0.7 topology-only form. toMermaidWith ::   (Enum s, Bounded s, Show s) =>   MermaidOptions ->@@ -267,8 +292,8 @@ -- Uses the **flat cross-product** shape: each composite vertex -- @'Composite' a b@ becomes a single Mermaid identifier -- @<show a>_<show b>@. The structure is otherwise identical to--- 'toMermaid' — same initial / final / edge emission rules, same--- 'edgeLabel' format. See EP-31's Decision Log+-- 'toMermaid' — same initial / final / edge emission rules and readable+-- semantics policy. See EP-31's Decision Log -- (@docs/plans/31-mermaid-rendering-for-composite-symtransducers.md@) -- for why the flat shape was chosen over Mermaid's nested-subgraph -- syntax (Shape B in the plan).@@ -282,8 +307,23 @@   ) =>   SymTransducer (HsPred rs ci) rs (Composite s1 s2) ci co ->   Text-toMermaidComposite = renderTopology compositeLabel+toMermaidComposite = toMermaidCompositeWith defaultMermaidOptions +-- | Options-aware variant of 'toMermaidComposite'.+toMermaidCompositeWith ::+  ( Enum s1,+    Bounded s1,+    Show s1,+    Enum s2,+    Bounded s2,+    Show s2+  ) =>+  MermaidOptions ->+  SymTransducer (HsPred rs ci) rs (Composite s1 s2) ci co ->+  Text+toMermaidCompositeWith opts =+  renderTopologyWith opts compositeLabel compositeLabel+ -- | Render a right-associative 3-deep -- @t1 \`'Keiki.Composition.compose'\` (t2 \`'Keiki.Composition.compose'\` t3)@ -- composite (vertex type @'Composite' s1 ('Composite' s2 s3)@) to a@@ -292,8 +332,8 @@ -- Each composite vertex becomes a single Mermaid identifier -- @\<show s1\>_\<show s2\>_\<show s3\>@ via 'compose3Label'. The -- structure is otherwise identical to 'toMermaid' /--- 'toMermaidComposite' — same initial / final / edge emission rules,--- same 'edgeLabel' format. See EP-35's plan+-- 'toMermaidComposite' — same initial / final / edge emission rules and+-- readable semantics policy. See EP-35's plan -- (@docs/plans/35-mermaid-renderer-for-right-associative-3-deep-compose-composites.md@) -- for the rationale and for the comparison against the -- nested-subgraph variant 'toMermaidCompose3Nested'.@@ -316,8 +356,32 @@     ci     co ->   Text-toMermaidCompose3 = renderTopology compose3Label+toMermaidCompose3 = toMermaidCompose3With defaultMermaidOptions +-- | Options-aware variant of 'toMermaidCompose3'.+toMermaidCompose3With ::+  forall rs s1 s2 s3 ci co.+  ( Enum s1,+    Bounded s1,+    Show s1,+    Enum s2,+    Bounded s2,+    Show s2,+    Enum s3,+    Bounded s3,+    Show s3+  ) =>+  MermaidOptions ->+  SymTransducer+    (HsPred rs ci)+    rs+    (Composite s1 (Composite s2 s3))+    ci+    co ->+  Text+toMermaidCompose3With opts =+  renderTopologyWith opts compose3Label compose3Label+ -- | Render a composite 'SymTransducer' (a 'Keiki.Composition.compose' -- result, vertex type @'Composite' s1 s2@) using the **nested-subgraph** -- shape (Shape B): each outer @s1@ vertex hosts a@@ -359,7 +423,23 @@   ) =>   SymTransducer (HsPred rs ci) rs (Composite s1 s2) ci co ->   Text-toMermaidCompositeNested t =+toMermaidCompositeNested =+  toMermaidCompositeNestedWith defaultMermaidOptions++-- | Options-aware variant of 'toMermaidCompositeNested'.+toMermaidCompositeNestedWith ::+  forall rs s1 s2 ci co.+  ( Enum s1,+    Bounded s1,+    Show s1,+    Enum s2,+    Bounded s2,+    Show s2+  ) =>+  MermaidOptions ->+  SymTransducer (HsPred rs ci) rs (Composite s1 s2) ci co ->+  Text+toMermaidCompositeNestedWith opts t =   let outers = [minBound .. maxBound] :: [s1]       inners = [minBound .. maxBound] :: [s2]       composites = [minBound .. maxBound] :: [Composite s1 s2]@@ -390,7 +470,7 @@             <> arrow             <> compositeLabel (target e)             <> colon-            <> edgeLabel e+            <> edgeLabelWith opts e         | s <- composites,           e <- edgesOut t s         ]@@ -448,7 +528,31 @@     ci     co ->   Text-toMermaidCompose3Nested t =+toMermaidCompose3Nested =+  toMermaidCompose3NestedWith defaultMermaidOptions++-- | Options-aware variant of 'toMermaidCompose3Nested'.+toMermaidCompose3NestedWith ::+  forall rs s1 s2 s3 ci co.+  ( Enum s1,+    Bounded s1,+    Show s1,+    Enum s2,+    Bounded s2,+    Show s2,+    Enum s3,+    Bounded s3,+    Show s3+  ) =>+  MermaidOptions ->+  SymTransducer+    (HsPred rs ci)+    rs+    (Composite s1 (Composite s2 s3))+    ci+    co ->+  Text+toMermaidCompose3NestedWith opts t =   let outers = [minBound .. maxBound] :: [s1]       inners = [minBound .. maxBound] :: [Composite s2 s3]       composites = [minBound .. maxBound] :: [Composite s1 (Composite s2 s3)]@@ -479,7 +583,7 @@             <> arrow             <> compose3Label (target e)             <> colon-            <> edgeLabel e+            <> edgeLabelWith opts e         | s <- composites,           e <- edgesOut t s         ]@@ -516,10 +620,11 @@ -- 'toMermaidAlternativeWith' to override (e.g. for domain-specific -- naming such as @EmailArm@ / @PingerArm@). ----- Edge labels are the standard @\<input ctor\> / \<output ctor\>@ format--- ('edgeLabel'). Because 'Keiki.Composition' lifters preserve--- @icName@ and @wcName@ verbatim, the label reads naturally even--- though the runtime input is @'Left' …@ / @'Right' …@.+-- Edge labels use the same readable guard/update policy as 'toMermaid'.+-- Because 'Keiki.Composition' lifters preserve @icName@ and @wcName@+-- verbatim, the base label reads naturally even though the runtime input is+-- @'Left' …@ / @'Right' …@. Use 'toMermaidAlternativeWithOptions' with+-- 'topologyMermaidOptions' for the historical compact form. -- -- See @docs/plans/33-shape-aware-mermaid-renderers-for-alternative-and-feedback1-composites.md@ -- for the full design record.@@ -535,7 +640,10 @@   SymTransducer (HsPred rs2 ci2) rs2 s2 ci2 co2 ->   Text toMermaidAlternative =-  toMermaidAlternativeWith (T.pack "LeftArm") (T.pack "RightArm")+  toMermaidAlternativeWithOptions+    defaultMermaidOptions+    (T.pack "LeftArm")+    (T.pack "RightArm")  -- | The arm-name-overridable variant of 'toMermaidAlternative'. The -- two 'Text' arguments name the left and right @state … { … }@@@ -560,7 +668,27 @@   SymTransducer (HsPred rs1 ci1) rs1 s1 ci1 co1 ->   SymTransducer (HsPred rs2 ci2) rs2 s2 ci2 co2 ->   Text-toMermaidAlternativeWith leftName rightName t1 t2 =+toMermaidAlternativeWith =+  toMermaidAlternativeWithOptions defaultMermaidOptions++-- | Options-aware, arm-name-overridable variant of+-- 'toMermaidAlternative'.+toMermaidAlternativeWithOptions ::+  forall rs1 rs2 s1 s2 ci1 ci2 co1 co2.+  ( Enum s1,+    Bounded s1,+    Show s1,+    Enum s2,+    Bounded s2,+    Show s2+  ) =>+  MermaidOptions ->+  Text ->+  Text ->+  SymTransducer (HsPred rs1 ci1) rs1 s1 ci1 co1 ->+  SymTransducer (HsPred rs2 ci2) rs2 s2 ci2 co2 ->+  Text+toMermaidAlternativeWithOptions opts leftName rightName t1 t2 =   let ind = T.pack "    "       ind2 = T.pack "        "       arrow = T.pack " --> "@@ -587,7 +715,7 @@                    <> arrow                    <> vertexLabel (target e)                    <> colon-                   <> edgeLabel e+                   <> edgeLabelWith opts e                | s <- [minBound .. maxBound],                  e <- edgesOut t s                ]@@ -645,8 +773,28 @@   SymTransducer (HsPred rs1 ci) rs1 s1 ci co ->   SymTransducer (HsPred rs2 co) rs2 s2 co ci ->   Text-toMermaidFeedback1 t f = renderTopology feedback1Label (feedback1 t f)+toMermaidFeedback1 = toMermaidFeedback1With defaultMermaidOptions +-- | Options-aware variant of 'toMermaidFeedback1'.+toMermaidFeedback1With ::+  ( Enum s1,+    Bounded s1,+    Show s1,+    Enum s2,+    Bounded s2,+    Show s2,+    WeakenR rs1,+    WeakenR rs2,+    Disjoint (Names rs2) (Names rs1),+    Disjoint (Names rs1) (Names (Append rs2 rs1))+  ) =>+  MermaidOptions ->+  SymTransducer (HsPred rs1 ci) rs1 s1 ci co ->+  SymTransducer (HsPred rs2 co) rs2 s2 co ci ->+  Text+toMermaidFeedback1With opts t f =+  renderTopologyWith opts feedback1Label feedback1Label (feedback1 t f)+ -- | The Mermaid identifier for a 'feedback1' composite vertex. -- @\<show outer\>_\<show policy\>_\<show inner\>@. Like -- 'compositeLabel', joined with underscores so the result still@@ -685,25 +833,9 @@     <> T.pack "_"     <> T.pack (show c) --- | The shared rendering core: walk @[minBound .. maxBound]@, emit--- the @stateDiagram-v2@ header, the initial-state line, one line per--- outgoing edge, and one final-state line per vertex where--- 'isFinal' fires. The vertex-label function is the only piece that--- varies between 'toMermaid' (single transducer) and--- 'toMermaidComposite' (composite); factoring it out keeps the--- rendering logic in one place.-renderTopology ::-  (Enum s, Bounded s) =>-  (s -> Text) ->-  SymTransducer (HsPred rs ci) rs s ci co ->-  Text-renderTopology label = renderTopologyWith defaultMermaidOptions label label---- | The options-aware rendering core. Identical to 'renderTopology'--- except the per-edge line calls 'edgeLabelWith' so the structural--- summary suffix appears when 'MermaidOptions' requests it. With--- 'defaultMermaidOptions' the output is byte-identical to the original--- 'renderTopology', which is what keeps 'toMermaid' guard-free.+-- | The shared options-aware rendering core: walk+-- @[minBound .. maxBound]@ and render every transition with+-- 'edgeLabelWith'. renderTopologyWith ::   (Enum s, Bounded s) =>   MermaidOptions ->@@ -827,7 +959,7 @@   many -> Just (render layout (Prelude.map wcN many))   where     wcN :: OutTerm rs ci co -> Text-    wcN (OPack _ wc _) = T.pack (wcName wc)+    wcN (OPack _ wc _) = escapeSemanticText (T.pack (wcName wc))     render :: MermaidOutputLayout -> [Text] -> Text     render MermaidOutputSemicolon ns       | length ns == 2 = T.intercalate (T.pack "; ") ns@@ -852,16 +984,13 @@   Edge (HsPred rs ci) rs ci co s ->   Text edgeLabelWithLayout layout e =-  let inp = maybe (T.pack "?") id (edgeInputName e)+  let inp = escapeSemanticText (maybe (T.pack "?") id (edgeInputName e))       out = maybe (T.pack "\x03B5") id (edgeOutputNameWith layout e)    in inp <> T.pack " / " <> out --- | The options-aware edge label: 'edgeLabel' plus an optional--- structural suffix @[w: …; g: …]@. When neither flag is set this is--- exactly 'edgeLabel' (no trailing space, no brackets), which is what--- keeps the 'toMermaid' default byte-identical. The written-slots part--- is omitted entirely when the edge writes nothing (an empty @w:@ would--- be noise); the guard part renders the full structural tag walk.+-- | The options-aware edge label. Semantic text is escaped before this+-- function inserts its own @<br/>@ layout separators, so user/domain text+-- cannot create extra label lines. edgeLabelWith ::   MermaidOptions ->   Edge (HsPred rs ci) rs ci co s ->@@ -874,15 +1003,13 @@   -- the output rendering; guard /text/ is produced by   -- 'renderGuardSegment' (EP-61's chokepoint).   let base = edgeLabelWithLayout (outputLayout opts) e-      ws = if showWrittenSlots opts then writtenSlots u else []-      wPart =-        case truncateSlots (maxInlineWrittenSlots opts) ws of-          [] -> []-          xs -> [T.pack "w: " <> T.intercalate (T.pack "; ") xs]+      uPart = case renderUpdateSegment opts u of+        Just t -> [t]+        Nothing -> []       gPart = case renderGuardSegment opts g of         Just t -> [T.pack "g: " <> truncateGuard (maxInlineGuardWidth opts) t]         Nothing -> []-      parts = wPart ++ gPart+      parts = uPart ++ gPart    in case labelLayout opts of         MermaidLabelInline ->           if null parts@@ -920,28 +1047,61 @@ writtenSlots (USet ix _) = [T.pack (indexNName ix)] writtenSlots (UCombine a b) = writtenSlots a ++ writtenSlots b +-- | Produce the update segment text for an edge. Pretty mode retains the+-- complete right-hand expressions; written-slot mode is the compact legacy+-- summary and may use its dedicated truncation option.+renderUpdateSegment :: MermaidOptions -> Update rs w ci -> Maybe Text+renderUpdateSegment opts u =+  case updateMode opts of+    MermaidUpdateHidden -> Nothing+    MermaidUpdateWrittenSlots ->+      case truncateSlots+        (maxInlineWrittenSlots opts)+        (Prelude.map escapeSemanticText (writtenSlots u)) of+        [] -> Nothing+        xs -> Just (T.pack "w: " <> T.intercalate (T.pack "; ") xs)+    MermaidUpdatePretty ->+      Just (T.pack "u: " <> escapeSemanticText (prettyUpdate u))+ -- | Produce the guard segment text for an edge, or 'Nothing' when no--- guard segment should appear. The effective mode reconciles the legacy--- 'showGuardSummary' flag with the new 'guardMode': an explicit--- 'guardMode' (anything other than 'MermaidGuardHidden') wins; otherwise--- 'showGuardSummary' is honoured as the legacy spelling of--- 'MermaidGuardStructuralSummary'.------ This is the single chokepoint for guard /text/ production. A sibling--- renderer that changes how edge-label /segments are laid out/ (inline--- vs. multiline) wraps the assembly of segments and leaves this--- function's text untouched.+-- guard segment should appear. Semantic text is escaped here, before label+-- layout is assembled. renderGuardSegment :: MermaidOptions -> HsPred rs ci -> Maybe Text renderGuardSegment opts g =-  case effectiveMode of+  escapeSemanticText <$> case guardMode opts of     MermaidGuardHidden -> Nothing     MermaidGuardStructuralSummary -> Just (guardSummary g)     MermaidGuardPretty -> Just (prettyPred g)++-- | Escape domain-derived label text exactly once into a visible,+-- non-structural alphabet. The documentation backend decodes XML entities+-- before parsing Mermaid and also turns both @<br>@ spellings and literal+-- @\\n@ into line breaks, so entity encoding alone cannot isolate semantic+-- text. Full-width punctuation keeps the value recognizable while preventing+-- parser control. XML entities retain punctuation that the backend can safely+-- decode, full-width angle brackets keep break-tag-like input inert, and+-- control pictures make raw line endings visible rather than structural.+-- Renderer-owned ASCII @<br/>@ is inserted only after this pass. The known+-- opaque marker @<lit>@ is encoded as entities because it cannot be a break+-- tag and should remain visually exact.+escapeSemanticText :: Text -> Text+escapeSemanticText =+  T.intercalate (T.pack "&lt;lit&gt;")+    . Prelude.map (T.concatMap escapeChar)+    . T.splitOn (T.pack "<lit>")   where-    effectiveMode-      | guardMode opts /= MermaidGuardHidden = guardMode opts-      | showGuardSummary opts = MermaidGuardStructuralSummary-      | otherwise = MermaidGuardHidden+    escapeChar '\r' = T.pack "\x240D"+    escapeChar '\n' = T.pack "\x240A"+    escapeChar '\\' = T.pack "\xFF3C"+    escapeChar '\'' = T.pack "&apos;"+    escapeChar '"' = T.pack "&quot;"+    escapeChar '&' = T.pack "&amp;"+    escapeChar '<' = T.pack "\xFF1C"+    escapeChar '>' = T.pack "\xFF1E"+    escapeChar '|' = T.pack "&#124;"+    escapeChar '{' = T.pack "&#123;"+    escapeChar '}' = T.pack "&#125;"+    escapeChar c = T.singleton c  -- | A structural, total summary of a guard predicate: its constructor -- tags in left-to-right (prefix) order, with 'PCmp' carrying its 'Cmp'

@@ -2,14 +2,14 @@  -- | Pure, domain-readable pretty-printer for keiki's predicate, term, -- and update syntax trees ('HsPred', 'Term', 'Update'). Produces--- 'Data.Text.Text'. No solver, no IO. Shared by the Mermaid topology+-- 'Data.Text.Text'. No solver, no IO. Shared by the Mermaid behavioral -- renderer ('Keiki.Render.Mermaid') and the sibling edge-inspector / -- multiline-label renderers. ----- Two things are provably unprintable and are marked, not dropped:--- applied opaque Haskell functions render as @<fn>(...)@; literal--- values render as @<lit>@ (a 'TLit' carries an unconstrained type--- with no 'Show').+-- Two things are deliberately marked rather than invented: applied opaque+-- Haskell functions render as @<fn>(...)@, and explicit display-opaque literal+-- values render as @<lit>@. Ordinary 'TLit' values use their retained 'Show'+-- evidence. module Keiki.Render.Pretty   ( indexName,     prettyTerm,@@ -44,11 +44,12 @@  -- | Render a 'Term' as domain-readable 'Text'. Register reads render by -- slot name, input-field reads as @ctor.field@, arithmetic structurally--- with @+ - *@. Opaque applied functions render @<fn>(...)@; literal--- values render @<lit>@ (a 'TLit' carries an unconstrained type with no--- 'Show').+-- with @+ - *@. Opaque applied functions render @<fn>(...)@. Ordinary+-- literals use their value's 'Show' instance; explicit opaque literals render+-- as @<lit>@. prettyTerm :: Term rs ci ifs r -> Text-prettyTerm (TLit _) = T.pack "<lit>"+prettyTerm (TLit value) = T.pack (show value)+prettyTerm (TOpaqueLit _) = T.pack "<lit>" prettyTerm (TReg ix) = T.pack (indexName ix) prettyTerm (TInpCtorField ic ix) =   T.pack (icName ic) <> T.pack "." <> T.pack (indexName ix)

@@ -576,7 +576,7 @@ -- | Translate a 'Term rs ci r' to an SBV expression of the carrier's -- representation type. Requires 'Sym' evidence for @r@. ----- The translation is /structural/ for 'TLit', 'TReg',+-- The translation is /structural/ for 'TLit', 'TOpaqueLit', 'TReg', -- 'TInpCtorField', and (since EP-43) 'TArith': a 'TArith' over a type -- whose 'SymRep' is SBV-numeric (a 'discoverSymNum' hit) emits a real -- @+@ \/ @-@ \/ @*@ over the translated operands, so a guard over a@@ -624,6 +624,7 @@   Term rs ci ifs r ->   SBV.Symbolic (SBV.SBV (SymRep r)) translateTermSym _env (TLit r) = pure (symLit r)+translateTermSym _env (TOpaqueLit r) = pure (symLit r) translateTermSym env (TReg ix) =   memoFree @r env (RegVar (indexName ix)) translateTermSym env (TInpCtorField ic ix) =@@ -1045,6 +1046,7 @@   Term rs ci ifs r ->   [TranslationReportEvent] termReportEvents _root _context (TLit _) = []+termReportEvents _root _context (TOpaqueLit _) = [] termReportEvents _root _context (TReg ix) =   [DirectOwnerReadEvent (registerBaseDescriptor @r ix)] termReportEvents _root _context (TInpCtorField ic ix) =

@@ -1,12 +1,14 @@ module Keiki.CompositionAlignmentSpec (spec) where  import Data.Proxy (Proxy (..))+import Data.Text qualified as T import Keiki.Composition import Keiki.Core import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Fixtures.ComposeStateful import Keiki.Fixtures.CounterPipeline import Keiki.Profunctor (rmapCo)+import Keiki.Render.Pretty (prettyPred, prettyTerm) import Test.Hspec  type Payload1 = '[ '("payload", Int)]@@ -218,6 +220,7 @@         inputTerm = TInpCtorField projectionSourceCtor #doc         passThrough = projectionSource inputTerm         literalOwner = projectionSource (TLit matchingDoc)+        opaqueOwner = projectionSource (opaqueLit matchingDoc)         computedOwner = projectionSource (TApp1 id inputTerm)      it "preserves a stable input-field owner through checked composition" $ do@@ -226,15 +229,39 @@         Left warnings -> expectationFailure ("stable projection warned: " <> show warnings)         Right pipeline -> opaqueGuardWarnings pipeline `shouldBe` [] -    it "constant-folds a literal owner without introducing opacity" $ do-      let pipeline = compose literalOwner projectionSink-      opaqueGuardWarnings pipeline `shouldBe` []-      case stepEither-        pipeline-        (initial pipeline, initialRegs pipeline)-        (ProjectionSourceCmd (FieldProj.DocInfo "ignored" "" [])) of-        Left failure -> expectationFailure ("literal-folded pipeline failed: " <> show failure)-        Right _ -> pure ()+    it "constant-folds a literal owner with display opacity but exact semantics" $ do+      case composeChecked literalOwner projectionSink of+        Left warnings -> expectationFailure ("literal fold failed checked composition: " <> show warnings)+        Right pipeline -> do+          opaqueGuardWarnings pipeline `shouldBe` []+          case edgesOut pipeline (initial pipeline) of+            [edge] ->+              prettyPred (guard edge)+                `shouldSatisfy` T.isInfixOf (T.pack "<lit>")+            _ -> expectationFailure "literal-folded pipeline no longer has one edge"+          case stepEither+            pipeline+            (initial pipeline, initialRegs pipeline)+            (ProjectionSourceCmd (FieldProj.DocInfo "ignored" "" [])) of+            Left failure -> expectationFailure ("literal-folded pipeline failed: " <> show failure)+            Right _ -> pure ()++    it "preserves literal display evidence through positional substitution" $ do+      let midRead = TInpCtorField projectionMidCtor #doc+      case edgesOut literalOwner (initial literalOwner) of+        [Edge {output = [out]}] -> do+          let substituted =+                substTerm @'[] @'[] midRead out ::+                  Term '[] ProjectionSourceCmd ProjectionSourceFields FieldProj.DocInfo+          prettyTerm substituted `shouldBe` T.pack (show matchingDoc)+        _ -> expectationFailure "readable literal source no longer has one output"+      case edgesOut opaqueOwner (initial opaqueOwner) of+        [Edge {output = [out]}] -> do+          let substituted =+                substTerm @'[] @'[] midRead out ::+                  Term '[] ProjectionSourceCmd ProjectionSourceFields FieldProj.DocInfo+          prettyTerm substituted `shouldBe` T.pack "<lit>"+        _ -> expectationFailure "opaque literal source no longer has one output"      it "keeps raw composition forward-correct but rejects a computed owner at the checked boundary" $ do       let pipeline = compose computedOwner projectionSink

@@ -8,6 +8,142 @@ -- | A two-constructor input symbol used by the 'TInpCtorField' tests. data TinyCmd = TinyFoo Int Int | TinyBar Int deriving (Eq, Show) +-- EP-84 guarantee-ledger fixtures. 'NoShowValue' proves the term language can+-- still carry a value with no display dictionary. 'ThrowingShowValue' carries+-- a dictionary whose method is bottom, so execution and replay tests detect+-- any accidental renderer observation on a semantic path.+data NoShowValue = NoShowValue Int deriving (Eq)++data NoShowEvent = NoShowEvent NoShowValue deriving (Eq)++data ThrowingShowValue = ThrowingShowValue Int deriving (Eq)++instance Show ThrowingShowValue where+  show _ = error "EP-84: semantic execution forced Show"++data LiteralLedgerEvent = LiteralLedgerEvent ThrowingShowValue deriving (Eq)++data LiteralLedgerVertex = LiteralLedgerStart | LiteralLedgerDone+  deriving stock (Eq, Ord, Show, Enum, Bounded)++type LiteralLedgerRegs = '[ '("payload", ThrowingShowValue)]++literalLedgerInCtor :: InCtor () '[]+literalLedgerInCtor =+  InCtor+    { icName = "LiteralLedgerCommand",+      icMatch = \() -> Just RNil,+      icBuild = \RNil -> ()+    }++literalLedgerWireCtor :: WireCtor LiteralLedgerEvent (ThrowingShowValue, ())+literalLedgerWireCtor =+  WireCtor+    { wcName = "LiteralLedgerEvent",+      wcMatch = \(LiteralLedgerEvent value) -> Just (value, ()),+      wcBuild = \(value, ()) -> LiteralLedgerEvent value+    }++literalLedgerValue :: ThrowingShowValue+literalLedgerValue = ThrowingShowValue 41++literalLedgerTransducerWith ::+  Term LiteralLedgerRegs () '[] ThrowingShowValue ->+  SymTransducer+    (HsPred LiteralLedgerRegs ())+    LiteralLedgerRegs+    LiteralLedgerVertex+    ()+    LiteralLedgerEvent+literalLedgerTransducerWith literalTerm =+  SymTransducer+    { edgesOut = \case+        LiteralLedgerStart ->+          [ Edge+              { guard = PEq literalTerm literalTerm,+                update =+                  USet+                    (#payload :: IndexN "payload" LiteralLedgerRegs ThrowingShowValue)+                    literalTerm,+                output =+                  [ pack+                      literalLedgerInCtor+                      literalLedgerWireCtor+                      (OFCons literalTerm OFNil)+                  ],+                target = LiteralLedgerDone,+                mode = Live+              }+          ]+        LiteralLedgerDone -> [],+      initial = LiteralLedgerStart,+      initialRegs =+        RCons (Proxy @"payload") (ThrowingShowValue 0) RNil,+      isFinal = (== LiteralLedgerDone)+    }++literalLedgerTransducer ::+  SymTransducer+    (HsPred LiteralLedgerRegs ())+    LiteralLedgerRegs+    LiteralLedgerVertex+    ()+    LiteralLedgerEvent+literalLedgerTransducer = literalLedgerTransducerWith (lit literalLedgerValue)++opaqueLiteralLedgerTransducer ::+  SymTransducer+    (HsPred LiteralLedgerRegs ())+    LiteralLedgerRegs+    LiteralLedgerVertex+    ()+    LiteralLedgerEvent+opaqueLiteralLedgerTransducer =+  literalLedgerTransducerWith (opaqueLit literalLedgerValue)++type NoShowRegs = '[ '("payload", NoShowValue)]++noShowWireCtor :: WireCtor NoShowEvent (NoShowValue, ())+noShowWireCtor =+  WireCtor+    { wcName = "NoShowEvent",+      wcMatch = \(NoShowEvent value) -> Just (value, ()),+      wcBuild = \(value, ()) -> NoShowEvent value+    }++noShowTransducer ::+  SymTransducer+    (HsPred NoShowRegs ())+    NoShowRegs+    LiteralLedgerVertex+    ()+    NoShowEvent+noShowTransducer =+  SymTransducer+    { edgesOut = \case+        LiteralLedgerStart ->+          [ Edge+              { guard = PTop,+                update =+                  USet+                    (#payload :: IndexN "payload" NoShowRegs NoShowValue)+                    (opaqueLit (NoShowValue 7)),+                output =+                  [ pack+                      literalLedgerInCtor+                      noShowWireCtor+                      (OFCons (opaqueLit (NoShowValue 7)) OFNil)+                  ],+                target = LiteralLedgerDone,+                mode = Live+              }+          ]+        LiteralLedgerDone -> [],+      initial = LiteralLedgerStart,+      initialRegs = RCons (Proxy @"payload") (NoShowValue 0) RNil,+      isFinal = (== LiteralLedgerDone)+    }+ type SnapshotRegs =   '[ '("x", Int),      '("y", Int)@@ -85,6 +221,88 @@  spec :: Spec spec = do+  describe "EP-84 literal semantic guarantee ledger" $ do+    it "evaluates a display-opaque value with no Show instance" $+      case evalTerm (opaqueLit (NoShowValue 7)) RNil () of+        NoShowValue 7 -> pure ()+        _ -> expectationFailure "literal evaluation changed the no-Show value"++    it "updates, emits, and replays a value with no Show instance" $ do+      case step+        noShowTransducer+        (initial noShowTransducer, initialRegs noShowTransducer)+        () of+        Just+          ( LiteralLedgerDone,+            RCons _ (NoShowValue 7) RNil,+            [NoShowEvent (NoShowValue 7)]+            ) -> pure ()+        _ -> expectationFailure "no-Show literal step changed its value"+      case reconstitute noShowTransducer [NoShowEvent (NoShowValue 7)] of+        Just (LiteralLedgerDone, RCons _ (NoShowValue 7) RNil) -> pure ()+        _ -> expectationFailure "no-Show literal replay changed its value"++    it "evaluates, compares, updates, and emits without forcing Show" $ do+      evalPred+        (PEq (lit literalLedgerValue) (lit literalLedgerValue) :: HsPred '[] ())+        RNil+        ()+        `shouldBe` True+      case step+        literalLedgerTransducer+        (initial literalLedgerTransducer, initialRegs literalLedgerTransducer)+        () of+        Just+          ( LiteralLedgerDone,+            RCons _ (ThrowingShowValue 41) RNil,+            [LiteralLedgerEvent (ThrowingShowValue 41)]+            ) -> pure ()+        _ -> expectationFailure "literal step changed state, registers, or output"++    it "solves and replays the emitted literal without forcing Show" $ do+      let observed = LiteralLedgerEvent literalLedgerValue+      case edgesOut literalLedgerTransducer LiteralLedgerStart of+        [Edge {output = [out]}] -> solveOutput out (initialRegs literalLedgerTransducer) observed `shouldBe` Just ()+        _ -> expectationFailure "literal ledger fixture no longer has one output"+      case reconstitute literalLedgerTransducer [observed] of+        Just+          ( LiteralLedgerDone,+            RCons _ (ThrowingShowValue 41) RNil+            ) -> pure ()+        _ -> expectationFailure "literal replay changed state or registers"++    it "retains the clean validation classification" $+      validateTransducer defaultValidationOptions literalLedgerTransducer+        `shouldBe` []++    it "gives readable and display-opaque literals identical step and replay results" $ do+      let readableStep =+            step+              literalLedgerTransducer+              (initial literalLedgerTransducer, initialRegs literalLedgerTransducer)+              ()+          opaqueStep =+            step+              opaqueLiteralLedgerTransducer+              (initial opaqueLiteralLedgerTransducer, initialRegs opaqueLiteralLedgerTransducer)+              ()+      case (readableStep, opaqueStep) of+        ( Just (LiteralLedgerDone, RCons _ (ThrowingShowValue 41) RNil, [LiteralLedgerEvent (ThrowingShowValue 41)]),+          Just (LiteralLedgerDone, RCons _ (ThrowingShowValue 41) RNil, [LiteralLedgerEvent (ThrowingShowValue 41)])+          ) -> pure ()+        _ -> expectationFailure "readable and opaque literal steps diverged"+      let observed = [LiteralLedgerEvent literalLedgerValue]+      case ( reconstitute literalLedgerTransducer observed,+             reconstitute opaqueLiteralLedgerTransducer observed+           ) of+        ( Just (LiteralLedgerDone, RCons _ (ThrowingShowValue 41) RNil),+          Just (LiteralLedgerDone, RCons _ (ThrowingShowValue 41) RNil)+          ) -> pure ()+        _ -> expectationFailure "readable and opaque literal replay diverged"++    it "does not classify display opacity as an opaque semantic guard" $+      opaqueGuardWarnings opaqueLiteralLedgerTransducer `shouldBe` []+   describe "evalTerm" $ do     it "evaluates TLit" $       evalTerm (TLit (42 :: Int)) RNil () `shouldBe` 42

@@ -30,6 +30,7 @@ --     nested) and the synthetic three-toy fixture. module Keiki.Render.MermaidSpec (spec) where +import Data.Proxy (Proxy (..)) import Data.Text (Text) import Data.Text qualified as T import Keiki.Composition (Composite, compose)@@ -41,13 +42,16 @@     EdgeMode (..),     HsPred (..),     InCtor (..),+    IndexN (..),     OutFields (..),     RegFile (..),     SymTransducer (..),     Update (..),     WireCtor (..),+    opaqueLit,     pack,   )+import Keiki.Fixtures.CounterPipeline (stageB) import Keiki.Fixtures.EmailDelivery (emailDelivery) import Keiki.Fixtures.UserRegistration (Vertex (..), userReg) import Keiki.Render.Mermaid@@ -60,57 +64,112 @@     MermaidSection (..),     MermaidSectionKind (..),     MermaidStateLabels (..),+    MermaidUpdateMode (..),     defaultMermaidAtlasOptions,     defaultMermaidOptions,     duplicateStateIds,     toMermaid,     toMermaidAlternative,+    toMermaidAlternativeWithOptions,     toMermaidAtlas,     toMermaidAtlasWith,     toMermaidCompose3,     toMermaidCompose3Nested,+    toMermaidCompose3NestedWith,+    toMermaidCompose3With,     toMermaidComposite,     toMermaidCompositeNested,+    toMermaidCompositeNestedWith,+    toMermaidCompositeWith,     toMermaidFeedback1,+    toMermaidFeedback1With,     toMermaidWith,     toMermaidWithLabels,+    toTopologyMermaid,+    topologyMermaidOptions,     vertexLabel,   )+import Keiki.Render.Validate+  ( MermaidValidationOptions (..),+    defaultMermaidValidationOptions,+    validateMermaidDiagram,+  ) import Test.Hspec  spec :: Spec spec = do-  describe "toMermaid (single SymTransducer)" $+  describe "toMermaid (readable single SymTransducer)" $     it "renders userReg to the canonical stateDiagram-v2 block" $-      toMermaid userReg `shouldBe` userRegCanonical+      toMermaid userReg `shouldBe` userRegReadableCanonical -  describe "toMermaidComposite (composite SymTransducer)" $-    it "renders the AlertSource ⨾ EmailDelivery pipeline" $+  describe "toMermaid (complete business expressions, EP-84)" $+    it "shows update right-hand expressions and ordinary literal values" $ do+      let diagram = toMermaid stageB+      diagram `shouldSatisfy` T.isInfixOf (T.pack "u: regB := (regB + MsgB.payload)")+      diagram `shouldSatisfy` T.isInfixOf (T.pack "g: (MsgB &amp;&amp; regB ＞= 0)")+      diagram `shouldNotSatisfy` T.isInfixOf (T.pack "<lit>")++  describe "toMermaid (explicit display opacity, EP-84)" $+    it "shows opaqueLit as <lit> while topology mode hides the expression" $ do+      toMermaid opaqueValue+        `shouldSatisfy` T.isInfixOf (T.pack "u: secret := &lt;lit&gt;")+      toTopologyMermaid opaqueValue+        `shouldNotSatisfy` T.isInfixOf (T.pack "lit")++  describe "toTopologyMermaid (0.7 compatibility)" $+    it "renders userReg to the prior topology-only block exactly" $+      toTopologyMermaid userReg `shouldBe` userRegCanonical++  describe "toMermaidComposite (composite SymTransducer)" $ do+    it "renders readable semantics for the AlertSource ⨾ EmailDelivery pipeline" $       toMermaidComposite (compose alertSource emailDelivery)+        `shouldSatisfy` hasReadableSemantics+    it "reproduces the 0.7 topology with explicit options" $+      toMermaidCompositeWith topologyMermaidOptions (compose alertSource emailDelivery)         `shouldBe` alertEmailCompositeCanonical -  describe "toMermaidCompositeNested (composite SymTransducer)" $-    it "renders the AlertSource ⨾ EmailDelivery pipeline in nested form" $+  describe "toMermaidCompositeNested (composite SymTransducer)" $ do+    it "renders readable semantics in nested form" $       toMermaidCompositeNested (compose alertSource emailDelivery)+        `shouldSatisfy` hasReadableSemantics+    it "reproduces the 0.7 nested topology with explicit options" $+      toMermaidCompositeNestedWith topologyMermaidOptions (compose alertSource emailDelivery)         `shouldBe` alertEmailCompositeNestedCanonical -  describe "toMermaidAlternative (alternative composite)" $-    it "renders alternative emailDelivery pinger as parallel arms" $+  describe "toMermaidAlternative (alternative composite)" $ do+    it "renders readable semantics for both parallel arms" $       toMermaidAlternative emailDelivery pinger+        `shouldSatisfy` hasReadableSemantics+    it "reproduces the 0.7 parallel-arm topology with explicit options" $+      toMermaidAlternativeWithOptions+        topologyMermaidOptions+        (T.pack "LeftArm")+        (T.pack "RightArm")+        emailDelivery+        pinger         `shouldBe` emailPingerAltCanonical -  describe "toMermaidFeedback1 (feedback1 composite)" $-    it "renders feedback1 toggleAgg togglePolicy as flat 3-deep cross-product" $+  describe "toMermaidFeedback1 (feedback1 composite)" $ do+    it "renders readable feedback semantics" $       toMermaidFeedback1 toggleAgg togglePolicy+        `shouldSatisfy` hasReadableSemantics+    it "reproduces the 0.7 flat feedback topology with explicit options" $+      toMermaidFeedback1With topologyMermaidOptions toggleAgg togglePolicy         `shouldBe` toggleFeedback1Canonical -  describe "toMermaidCompose3 (right-associative 3-deep compose)" $-    it "renders the toy1 ⨾ (toy2 ⨾ toy3) flat block" $-      toMermaidCompose3 toy3deep `shouldBe` toy3deepFlatCanonical+  describe "toMermaidCompose3 (right-associative 3-deep compose)" $ do+    it "renders readable semantics in the flat block" $+      toMermaidCompose3 toy3deep `shouldSatisfy` hasReadableSemantics+    it "reproduces the 0.7 flat topology with explicit options" $+      toMermaidCompose3With topologyMermaidOptions toy3deep+        `shouldBe` toy3deepFlatCanonical -  describe "toMermaidCompose3Nested (right-associative 3-deep compose)" $-    it "renders the toy1 ⨾ (toy2 ⨾ toy3) one-level nested block" $-      toMermaidCompose3Nested toy3deep `shouldBe` toy3deepNestedCanonical+  describe "toMermaidCompose3Nested (right-associative 3-deep compose)" $ do+    it "renders readable semantics in the one-level nested block" $+      toMermaidCompose3Nested toy3deep `shouldSatisfy` hasReadableSemantics+    it "reproduces the 0.7 nested topology with explicit options" $+      toMermaidCompose3NestedWith topologyMermaidOptions toy3deep+        `shouldBe` toy3deepNestedCanonical    -- EP-50 M3: the default must stay byte-identical to today (the   -- guard-free pedagogy in deriving-lifecycle-transitions.md depends on@@ -124,23 +183,27 @@   describe "toMermaidWith (annotated edge summary)" $     it "renders userReg with written-slot and guard-summary suffixes" $       toMermaidWith-        (defaultMermaidOptions {showWrittenSlots = True, showGuardSummary = True})+        ( topologyMermaidOptions+            { updateMode = MermaidUpdateWrittenSlots,+              guardMode = MermaidGuardStructuralSummary+            }+        )         userReg         `shouldBe` userRegAnnotatedCanonical    describe "toMermaidWith (MermaidGuardPretty, EP-61)" $     it "renders userReg guards in domain-readable form" $       toMermaidWith-        (defaultMermaidOptions {guardMode = MermaidGuardPretty})+        (topologyMermaidOptions {guardMode = MermaidGuardPretty})         userReg         `shouldBe` userRegPrettyGuardCanonical    describe "toMermaidWith (multiline label layout, EP-63)" $     it "renders userReg labels with <br/>-separated segments" $       toMermaidWith-        ( defaultMermaidOptions-            { showWrittenSlots = True,-              showGuardSummary = True,+        ( topologyMermaidOptions+            { updateMode = MermaidUpdateWrittenSlots,+              guardMode = MermaidGuardStructuralSummary,               labelLayout = MermaidLabelMultiline             }         )@@ -150,8 +213,8 @@   describe "toMermaidWith (written-slot truncation, EP-63)" $     it "truncates a long written-slot list with +N more" $       toMermaidWith-        ( defaultMermaidOptions-            { showWrittenSlots = True,+        ( topologyMermaidOptions+            { updateMode = MermaidUpdateWrittenSlots,               maxInlineWrittenSlots = Just 2             }         )@@ -161,8 +224,8 @@   describe "toMermaidWith (guard-width truncation, EP-63)" $     it "truncates an over-long guard segment with an ellipsis" $       toMermaidWith-        ( defaultMermaidOptions-            { showGuardSummary = True,+        ( topologyMermaidOptions+            { guardMode = MermaidGuardStructuralSummary,               maxInlineGuardWidth = Just 10             }         )@@ -171,25 +234,36 @@    describe "toMermaidWith (MermaidOutputSemicolon default, EP-63)" $     it "renders multiEvt with the length-based default output layout" $-      toMermaid multiEvt `shouldBe` multiEvtSemicolonCanonical+      toTopologyMermaid multiEvt `shouldBe` multiEvtSemicolonCanonical    describe "toMermaidWith (MermaidOutputMultiline, EP-63)" $     it "renders every multi-event edge one event per line" $       toMermaidWith-        (defaultMermaidOptions {outputLayout = MermaidOutputMultiline})+        (topologyMermaidOptions {outputLayout = MermaidOutputMultiline})         multiEvt         `shouldBe` multiEvtMultilineCanonical    describe "toMermaidWith (MermaidOutputCounted, EP-63)" $     it "renders multi-event edges as an N events count" $       toMermaidWith-        (defaultMermaidOptions {outputLayout = MermaidOutputCounted})+        (topologyMermaidOptions {outputLayout = MermaidOutputCounted})         multiEvt         `shouldBe` multiEvtCountedCanonical +  describe "semantic-label escaping (EP-84)" $ do+    it "escapes every backend control spelling before inserting layout" $+      toMermaid specialChars `shouldBe` specialCharsCanonical+    it "preserves the diagram and transition line counts" $ do+      length (T.lines (toMermaid specialChars)) `shouldBe` 4+      T.count (T.pack " --> ") (toMermaid specialChars) `shouldBe` 3+      T.count (T.pack "<br/>") (toMermaid specialChars) `shouldBe` 2+    it "passes suspicious-character validation without disabling that check" $+      validateMermaidDiagram semanticValidationOptions (toMermaid specialChars)+        `shouldBe` []+   describe "toMermaidWithLabels (stable ASCII ids, spaced display labels, EP-64)" $     it "renders userReg with friendly labels and stable ids" $-      toMermaidWithLabels defaultMermaidOptions userRegLabels userReg+      toMermaidWithLabels topologyMermaidOptions userRegLabels userReg         `shouldBe` userRegLabeledCanonical    describe "toMermaidWithLabels (id == display is byte-identical, EP-64)" $@@ -210,8 +284,8 @@   describe "toMermaidAtlas (multi-diagram document)" $     it "assembles two labelled diagrams into one document" $       toMermaidAtlas-        [ (T.pack "User registration", toMermaid userReg),-          (T.pack "Alert \x2A3E Email", toMermaidComposite (compose alertSource emailDelivery))+        [ (T.pack "User registration", toTopologyMermaid userReg),+          (T.pack "Alert \x2A3E Email", toMermaidCompositeWith topologyMermaidOptions (compose alertSource emailDelivery))         ]         `shouldBe` atlasCanonical @@ -228,19 +302,38 @@             (T.pack "incident-command")             (T.pack "Incident Command")             AggregateDiagram-            (toMermaid userReg),+            (toTopologyMermaid userReg),           MermaidSection             (T.pack "dispatch")             (T.pack "Dispatch")             ProcessManagerDiagram-            (toMermaidComposite (compose alertSource emailDelivery))+            (toMermaidCompositeWith topologyMermaidOptions (compose alertSource emailDelivery))         ]         `shouldBe` typedAtlasCanonical --- | The canonical Mermaid block for @userReg@, mirrored verbatim from--- the aggregate's diagram in @docs/guide/diagrams/user-registration.md@.--- Stored inline (not in an external fixture file) so a formatting change--- requires touching this file alongside the producer change.+hasReadableSemantics :: Text -> Bool+hasReadableSemantics diagram =+  T.pack "<br/>u: " `T.isInfixOf` diagram+    && T.pack "<br/>g: " `T.isInfixOf` diagram++-- | The readable-primary golden. Unlike the Keiki 0.7 topology golden below,+-- every transition includes the complete update and guard expression.+userRegReadableCanonical :: Text+userRegReadableCanonical =+  T.intercalate+    (T.pack "\n")+    [ "stateDiagram-v2",+      "    [*] --> PotentialCustomer",+      "    PotentialCustomer --> RequiresConfirmation : StartRegistration / RegistrationStarted; ConfirmationEmailSent<br/>u: registeredAt := StartRegistration.at, confirmCode := StartRegistration.confirmCode, email := StartRegistration.email, (keep)<br/>g: StartRegistration",+      "    RequiresConfirmation --> Confirmed : ConfirmAccount / AccountConfirmed<br/>u: confirmedAt := ConfirmAccount.at, (keep)<br/>g: (ConfirmAccount &amp;&amp; ConfirmAccount.confirmCode == confirmCode)",+      "    RequiresConfirmation --> RequiresConfirmation : ResendConfirmation / ConfirmationResent<br/>u: registeredAt := ResendConfirmation.at, confirmCode := ResendConfirmation.code, (keep)<br/>g: ResendConfirmation",+      "    RequiresConfirmation --> Deleted : FulfillGDPRRequest / AccountDeleted<br/>u: deletedAt := FulfillGDPRRequest.at, (keep)<br/>g: FulfillGDPRRequest",+      "    Confirmed --> Deleted : FulfillGDPRRequest / AccountDeleted<br/>u: deletedAt := FulfillGDPRRequest.at, (keep)<br/>g: FulfillGDPRRequest",+      "    Deleted --> [*]"+    ]++-- | The Keiki 0.7 topology-only block for @userReg@, retained as the+-- compatibility golden for 'toTopologyMermaid'. userRegCanonical :: Text userRegCanonical =   unlinesNoTrail@@ -259,8 +352,8 @@   where     unlinesNoTrail = T.intercalate (T.pack "\n") --- | EP-50: the canonical block for @userReg@ rendered with both summary--- flags on (@MermaidOptions True True@). Differs from 'userRegCanonical'+-- | EP-50: the canonical block for @userReg@ rendered with written-slot+-- and structural-guard modes. Differs from 'userRegCanonical' -- only by the bracketed @[w: …; g: …]@ suffixes. Captured verbatim from -- the renderer (the slot order is the @UCombine@ nesting order, and each -- guard is the actual 'HsPred' shape @onCmd@ produced — a bare 'PInCtor'@@ -280,8 +373,8 @@     ]  -- | EP-61: the canonical block for @userReg@ rendered with--- @guardMode = MermaidGuardPretty@ and 'showWrittenSlots' left at its--- default 'False', so each label carries only a domain-readable+-- @guardMode = MermaidGuardPretty@ and updates hidden, so each label carries+-- only a domain-readable -- @[g: …]@ segment. Differs from 'userRegAnnotatedCanonical' by -- rendering real names — @ConfirmAccount@, @confirmCode@ — instead of -- the structural constructor-tag walk (@PAnd PInCtor PEq@). Captured@@ -293,14 +386,14 @@     [ "stateDiagram-v2",       "    [*] --> PotentialCustomer",       "    PotentialCustomer --> RequiresConfirmation : StartRegistration / RegistrationStarted; ConfirmationEmailSent [g: StartRegistration]",-      "    RequiresConfirmation --> Confirmed : ConfirmAccount / AccountConfirmed [g: (ConfirmAccount && ConfirmAccount.confirmCode == confirmCode)]",+      "    RequiresConfirmation --> Confirmed : ConfirmAccount / AccountConfirmed [g: (ConfirmAccount &amp;&amp; ConfirmAccount.confirmCode == confirmCode)]",       "    RequiresConfirmation --> RequiresConfirmation : ResendConfirmation / ConfirmationResent [g: ResendConfirmation]",       "    RequiresConfirmation --> Deleted : FulfillGDPRRequest / AccountDeleted [g: FulfillGDPRRequest]",       "    Confirmed --> Deleted : FulfillGDPRRequest / AccountDeleted [g: FulfillGDPRRequest]",       "    Deleted --> [*]"     ] --- | EP-63: @userReg@ rendered with both summary flags on and+-- | EP-63: @userReg@ rendered with written-slot and structural-guard modes and -- @labelLayout = MermaidLabelMultiline@. Same per-edge content as -- 'userRegAnnotatedCanonical', but the bracketed inline suffix is replaced -- by @<br/>@-separated segments: the @command / event@ base on the first@@ -322,7 +415,7 @@       "    Deleted --> [*]"     ] --- | EP-63: @userReg@ rendered with @showWrittenSlots = True@ and+-- | EP-63: @userReg@ rendered with @updateMode = MermaidUpdateWrittenSlots@ and -- @maxInlineWrittenSlots = Just 2@. The only edge writing more than two -- slots is @StartRegistration@ (three slots), which truncates to the first -- two followed by a single @+1 more@ token; every other edge writes two or@@ -341,7 +434,7 @@       "    Deleted --> [*]"     ] --- | EP-63: @userReg@ rendered with @showGuardSummary = True@ and+-- | EP-63: @userReg@ rendered with structural guard summaries and -- @maxInlineGuardWidth = Just 10@. The only guard whose structural text -- exceeds ten characters is @ConfirmAccount@'s @PAnd PInCtor PEq@ (length -- 16), truncated to the first ten characters plus the ellipsis @…@. The@@ -749,6 +842,124 @@       "    T1A_T2A_T3A --> T1B_T2B_T3B : Tick / Tick",       "    T1B_T2B_T3B --> [*]"     ]++-- * Semantic-label escaping fixture (EP-84) -------------------------++type SecretRegs = '[ '("secret", Int)]++data SecretCmd = SetSecret++data SecretEvt = SecretSet++data SecretState = SecretState+  deriving (Eq, Show, Enum, Bounded)++secretInCtor :: InCtor SecretCmd '[]+secretInCtor =+  InCtor+    { icName = "SetSecret",+      icMatch = \SetSecret -> Just RNil,+      icBuild = \RNil -> SetSecret+    }++secretWireCtor :: WireCtor SecretEvt ()+secretWireCtor =+  WireCtor+    { wcName = "SecretSet",+      wcMatch = \SecretSet -> Just (),+      wcBuild = \() -> SecretSet+    }++opaqueValue ::+  SymTransducer+    (HsPred SecretRegs SecretCmd)+    SecretRegs+    SecretState+    SecretCmd+    SecretEvt+opaqueValue =+  SymTransducer+    { edgesOut = \SecretState ->+        [ Edge+            { guard = PInCtor secretInCtor,+              update = USet IZ (opaqueLit (7 :: Int)),+              output = [pack secretInCtor secretWireCtor OFNil],+              target = SecretState,+              mode = Live+            }+        ],+      initial = SecretState,+      initialRegs = RCons (Proxy @"secret") 0 RNil,+      isFinal = const True+    }++data SpecialCmd = SpecialCmd++data SpecialEvt = SpecialEvt++data SpecialState = SpecialStart | SpecialDone+  deriving (Eq, Show, Enum, Bounded)++specialName :: String+specialName =+  "Command \"quote\" 'apostrophe' <br> <br/> <br /> &lt;br&gt; | {value}\r\n\\n"++specialInCtor :: InCtor SpecialCmd '[]+specialInCtor =+  InCtor+    { icName = specialName,+      icMatch = \SpecialCmd -> Just RNil,+      icBuild = \RNil -> SpecialCmd+    }++specialWireCtor :: WireCtor SpecialEvt ()+specialWireCtor =+  WireCtor+    { wcName = "Event",+      wcMatch = \SpecialEvt -> Just (),+      wcBuild = \() -> SpecialEvt+    }++specialChars ::+  SymTransducer+    (HsPred '[] SpecialCmd)+    '[]+    SpecialState+    SpecialCmd+    SpecialEvt+specialChars =+  SymTransducer+    { edgesOut = \case+        SpecialStart ->+          [ Edge+              { guard = PInCtor specialInCtor,+                update = UKeep,+                output = [pack specialInCtor specialWireCtor OFNil],+                target = SpecialDone,+                mode = Live+              }+          ]+        SpecialDone -> [],+      initial = SpecialStart,+      initialRegs = RNil,+      isFinal = (== SpecialDone)+    }++specialCharsCanonical :: Text+specialCharsCanonical =+  T.intercalate+    (T.pack "\n")+    [ "stateDiagram-v2",+      "    [*] --> SpecialStart",+      "    SpecialStart --> SpecialDone : Command &quot;quote&quot; &apos;apostrophe&apos; ＜br＞ ＜br/＞ ＜br /＞ &amp;lt;br&amp;gt; &#124; &#123;value&#125;␍␊＼n / Event<br/>u: (keep)<br/>g: Command &quot;quote&quot; &apos;apostrophe&apos; ＜br＞ ＜br/＞ ＜br /＞ &amp;lt;br&amp;gt; &#124; &#123;value&#125;␍␊＼n",+      "    SpecialDone --> [*]"+    ]++semanticValidationOptions :: MermaidValidationOptions+semanticValidationOptions =+  defaultMermaidValidationOptions+    { maxLabelLength = Nothing+    }  -- * Multi-event output fixture (EP-63 M2) ----------------------------- 

@@ -15,6 +15,7 @@     Term (..),     Update (..),     inpProj,+    opaqueLit,     regProj,   ) import Keiki.FieldProjSpec qualified as FieldProj@@ -66,8 +67,11 @@     it "renders an input-field read as ctor.field" $       prettyTerm (TInpCtorField inCtorDeposit amountIx :: Term Regs Cmd DepFields Int)         `shouldBe` T.pack "Deposit.amount"-    it "renders a literal opaquely as <lit>" $+    it "renders an ordinary literal from its value" $       prettyTerm (TLit (42 :: Int) :: Term Regs Cmd '[] Int)+        `shouldBe` T.pack "42"+    it "renders an explicit display-opaque literal as <lit>" $+      prettyTerm (opaqueLit (42 :: Int) :: Term Regs Cmd '[] Int)         `shouldBe` T.pack "<lit>"     it "renders TApp1 as <fn>(arg)" $       prettyTerm (TApp1 (+ (1 :: Int)) (TReg balanceIx) :: Term Regs Cmd '[] Int)@@ -105,9 +109,9 @@     it "renders PInCtor as the constructor name" $       prettyPred (PInCtor inCtorDeposit :: HsPred Regs Cmd)         `shouldBe` T.pack "Deposit"-    it "renders PEq structurally with <lit> on the literal side" $+    it "renders PEq structurally with the literal value" $       prettyPred (PEq (TReg balanceIx) (TLit (0 :: Int)) :: HsPred Regs Cmd)-        `shouldBe` T.pack "balance == <lit>"+        `shouldBe` T.pack "balance == 0"     it "renders each PCmp direction" $ do       prettyPred (PCmp CmpLt (TReg balanceIx) (TReg limitIx) :: HsPred Regs Cmd)         `shouldBe` T.pack "balance < limit"@@ -127,14 +131,14 @@             ) ::             HsPred Regs Cmd         )-        `shouldBe` T.pack "(Deposit && (balance >= <lit> || !(limit == <lit>)))"+        `shouldBe` T.pack "(Deposit && (balance >= 0 || !(limit == 0)))"    describe "prettyUpdate" $ do     it "renders UKeep" $       prettyUpdate (UKeep :: Update Regs '[] Cmd) `shouldBe` T.pack "(keep)"     it "renders USet as slot := term" $       prettyUpdate (USet balanceN (TLit (0 :: Int)) :: Update Regs '["balance"] Cmd)-        `shouldBe` T.pack "balance := <lit>"+        `shouldBe` T.pack "balance := 0"     it "renders UCombine comma-separated" $       prettyUpdate         ( UCombine@@ -142,4 +146,4 @@             (USet balanceN (TLit (1 :: Int))) ::             Update Regs '["balance", "balance"] Cmd         )-        `shouldBe` T.pack "balance := limit, balance := <lit>"+        `shouldBe` T.pack "balance := limit, balance := 1"

@@ -1,5 +1,6 @@ module Keiki.SymbolicSpec (spec) where +import Control.Monad (forM_) import Data.Int (Int32, Int64) import Data.Kind (Type) import Data.Maybe (isJust, isNothing)@@ -476,6 +477,48 @@       predicateTranslationExact unsatisfiable `shouldBe` True       verifyPredicate satisfiable `shouldReturn` VerifiedSatisfiable       verifyPredicate unsatisfiable `shouldReturn` VerifiedUnsatisfiable++    it "keeps every readable/opaque literal equality pairing exact" $ do+      let readable value = lit value :: Term '[] () '[] Bool+          hidden value = opaqueLit value :: Term '[] () '[] Bool+          equalPairs =+            [ (readable True, readable True),+              (readable True, hidden True),+              (hidden True, readable True),+              (hidden True, hidden True)+            ]+          unequalPairs =+            [ (readable True, readable False),+              (readable True, hidden False),+              (hidden True, readable False),+              (hidden True, hidden False)+            ]+      forM_ equalPairs $ \(left, right) -> do+        let predicate = PEq left right :: HsPred '[] ()+        predicateTranslationReport predicate `shouldBe` ExactTranslation+        verifyPredicate predicate `shouldReturn` VerifiedSatisfiable+        detail <- verifyPredicateDetailed predicate+        detail `shouldSatisfy` \case+          PredicateSatisfiable ExactTranslation [] -> True+          _ -> False+      forM_ unequalPairs $ \(left, right) -> do+        let predicate = PEq left right :: HsPred '[] ()+        predicateTranslationReport predicate `shouldBe` ExactTranslation+        verifyPredicate predicate `shouldReturn` VerifiedUnsatisfiable++    it "keeps every readable/opaque literal ordering pairing exact" $ do+      let readable value = lit value :: Term '[] () '[] Int+          hidden value = opaqueLit value :: Term '[] () '[] Int+          pairings =+            [ (readable 3, readable 5),+              (readable 3, hidden 5),+              (hidden 3, readable 5),+              (hidden 3, hidden 5)+            ]+      forM_ pairings $ \(left, right) -> do+        let predicate = PCmp CmpLt left right :: HsPred '[] ()+        predicateTranslationReport predicate `shouldBe` ExactTranslation+        verifyPredicate predicate `shouldReturn` VerifiedSatisfiable      it "verifies supported structural arithmetic" $ do       let arithmetic =

@@ -1,5 +1,6 @@ module Keiki.ValidationSpec (spec) where +import Control.Monad (forM_) import Data.List (isInfixOf) import Data.Proxy (Proxy (..)) import Data.Word (Word8)@@ -675,6 +676,23 @@     it "uses a mentioned non-integral literal as a concrete witness" $       checkTransitionDeterminismPure boolLiteralWitnessT         `shouldSatisfy` (not . null)++    it "treats every readable/opaque literal pairing identically" $ do+      let readable value = lit value :: Term OverlapRegs Cmd '[] Int+          hidden value = opaqueLit value :: Term OverlapRegs Cmd '[] Int+          pairings =+            [ (readable 3, readable 5),+              (readable 3, hidden 5),+              (hidden 3, readable 5),+              (hidden 3, hidden 5)+            ]+      forM_ pairings $ \(left, right) -> do+        checkTransitionDeterminismPure+          (overlapFixture (PEq left left) (PEq right right))+          `shouldSatisfy` (not . null)+        checkTransitionDeterminismPure+          (overlapFixture (PCmp CmpLt left right) PTop)+          `shouldSatisfy` (not . null)      it "finds an interior overlap in Natural's zero-bounded domain" $ do       let purePairs = map warningPair (checkTransitionDeterminismPure naturalInteriorOverlapT)