keiki 0.3.1.0 → 0.4.0.0

raw patch · 17 files changed

+1806/−73 lines, 17 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +44/−0
• keiki.cabal +3/−1
• src/Keiki/Composition.hs +246/−10
• src/Keiki/Core.hs +363/−1
• src/Keiki/Internal/SymbolicTypes.hs +75/−0
• src/Keiki/Profunctor.hs +12/−0
• src/Keiki/Render/Pretty.hs +3/−0
• src/Keiki/Symbolic.hs +148/−58
• test/Keiki/CompositionAlignmentSpec.hs +138/−0
• test/Keiki/CompositionMultiEventSpec.hs +148/−3
• test/Keiki/FieldProjSpec.hs +419/−0
• test/Keiki/ProfunctorSpec.hs +10/−0
• test/Keiki/Render/PrettySpec.hs +13/−0
• test/Keiki/StrongSpec.hs +18/−0
• test/Keiki/SymbolicSpec.hs +20/−0
• test/Keiki/ValidationSpec.hs +144/−0
• test/Spec.hs +2/−0

@@ -9,6 +9,50 @@ ## [Unreleased]  +## [0.4.0.0] — 2026-07-28++### Added++- `Keiki.Core` now exposes nominal typed field projections over+  consumer-owned values: `FieldProjection(..)`, abstract `FieldWitness`,+  `fieldWitness`, `ProjBase(..)`, `regProj`, `inpProj`,+  `fieldProjectionPath`, `fieldWitnessAgrees`, and the documented-internals+  helpers `fieldWitnessGet` and `indexPosition`. A projection reads one scalar+  field from a direct register or matched input field without requiring the+  owner type to have a symbolic representation.+- `Keiki.Symbolic.constrainFieldProjection` binds a memoized projection to a+  concrete getter result for concrete-to-symbolic agreement tests. Repeated+  reads share through structured base, nominal tag, owner, and result identity;+  caller-controlled diagnostic strings never determine solver identity.+- `ProjectionResultUnsupported`, `ProjectionOrderingUnsupported`, and+  `ProjectionOutsideGuard` make unsupported result types, unsupported ordering,+  and projected writes/outputs unconditional validation findings.+- `NonStructuralProjectionBoundary` identifies mapped composition boundaries+  that cannot retain a stable typed projection path, including pending writes+  in multi-event chains.++### Changed++- **Breaking:** `Term` gains the `TFieldProj` constructor. Code that exhaustively+  matches `Term` must handle it. Concrete evaluation applies the projection's+  total coherent getter; replay treats the result as derived.+- **Breaking:** `TransducerValidationWarning` and `ComposeAlignmentWarning` gain+  the projection constructors above, and `checkComposeAlignment` now requires+  the structural `WeakenR` evidence used to inspect mapped upstream terms.+- Projection use is guards-only in validated transducers. Equality requires a+  result in the curated symbolic registry, ordering requires its ordering+  subset, and input projections retain the existing `PInCtor` and hidden-input+  disciplines.+- Composition preserves a projection over a direct register/input owner, folds+  a literal owner, and lowers any computed owner to an opaque `TApp1`. Raw+  composition remains forward-correct; `composeChecked` rejects the precision-+  losing case.+- `symSatExt` does not reconstruct consumer-owned values from free projection+  scalars. The supported agreement is one-way: every concrete owner can bind a+  matching symbolic projection value, but an arbitrary symbolic projection+  model need not correspond to a constructible owner.++ ## [0.3.1.0] — 2026-07-23  ### Added

@@ -1,6 +1,6 @@ cabal-version:   3.0 name:            keiki-version:         0.3.1.0+version:         0.4.0.0 synopsis:        Pure core for symbolic-register transducer event sourcing. description:   A Haskell library for the pure core of event sourcing, workflow@@ -80,6 +80,7 @@     Keiki.Shape     Keiki.Symbolic +  other-modules:   Keiki.Internal.SymbolicTypes   hs-source-dirs:  src   build-depends:     , base               ^>=4.21@@ -119,6 +120,7 @@     Keiki.CoreHiddenInputsGSMSpec     Keiki.CoreInFlightSpec     Keiki.CoreSpec+    Keiki.FieldProjSpec     Keiki.Fixtures.BrokenTailCoverage     Keiki.Fixtures.ComposeStateful     Keiki.Fixtures.CounterPipeline

@@ -107,8 +107,10 @@ where  import Data.List (isInfixOf, isSuffixOf, nub)+import Data.Proxy (Proxy (..)) import Data.Set qualified as Set import Data.Type.Equality ((:~:) (Refl))+import Data.Typeable (Typeable) import GHC.TypeLits (KnownSymbol) import Keiki.Core import Keiki.Generics (Append, appendRegFile)@@ -262,6 +264,10 @@     f     (weakenLTerm @rs1 @rs2 a)     (weakenLTerm @rs1 @rs2 b)+weakenLTerm (TFieldProj witness base) =+  TFieldProj witness $ case base of+    PBReg ix -> PBReg (weakenL @rs1 @rs2 ix)+    PBInp ic ix -> PBInp ic ix  -- | Walk an 'HsPred' and weaken every term inside it. weakenLPred ::@@ -335,6 +341,10 @@     f     (weakenRTerm @rs1 @rs2 a)     (weakenRTerm @rs1 @rs2 b)+weakenRTerm (TFieldProj witness base) =+  TFieldProj witness $ case base of+    PBReg ix -> PBReg (weakenR @rs1 ix)+    PBInp ic ix -> PBInp ic ix  -- | Walk an 'HsPred' on a tail-side register file and lift every term -- inside via 'weakenRTerm'.@@ -469,6 +479,9 @@   termHasCtorMismatch expected a || termHasCtorMismatch expected b termHasCtorMismatch expected (TApp2 _ a b) =   termHasCtorMismatch expected a || termHasCtorMismatch expected b+termHasCtorMismatch _ (TFieldProj _ (PBReg _)) = False+termHasCtorMismatch expected (TFieldProj _ (PBInp ic _)) =+  icName ic /= expected  outCtorName :: OutTerm rs ci co -> String outCtorName (OPack _ wc _) = wcName wc@@ -489,6 +502,28 @@ substTerm (TLit r) _o1 = TLit r substTerm (TReg ix2) _o1 = TReg (weakenR @rs1 ix2) substTerm (TInpCtorField ic2 ix2) o1 =+  substInputField @rs1 @rs2 ic2 ix2 o1+substTerm (TFieldProj witness (PBReg ix2)) _o1 =+  TFieldProj witness (PBReg (weakenR @rs1 ix2))+substTerm (TFieldProj witness (PBInp ic2 ix2)) o1 =+  projectThroughTerm witness (substInputField @rs1 @rs2 ic2 ix2 o1)+substTerm (TApp1 f t) o1 = TApp1 f (substTerm @rs1 @rs2 t o1)+substTerm (TArith op a b) o1 =+  TArith op (substTerm @rs1 @rs2 a o1) (substTerm @rs1 @rs2 b o1)+substTerm (TApp2 f a b) o1 =+  TApp2+    f+    (substTerm @rs1 @rs2 a o1)+    (substTerm @rs1 @rs2 b o1)++substInputField ::+  forall rs1 rs2 ci1 mid ifs2 ifsR r.+  (WeakenR rs1) =>+  InCtor mid ifs2 ->+  Index ifs2 r ->+  OutTerm rs1 ci1 mid ->+  Term (Append rs1 rs2) ci1 ifsR r+substInputField ic2 ix2 o1 =   case o1 of     OPack _ic1 wc1 of1       | icName ic2 == wcName wc1 ->@@ -524,15 +559,44 @@                    \ its mismatched guard leaf should be unsatisfiable before\                    \ the value is demanded."             )-substTerm (TApp1 f t) o1 = TApp1 f (substTerm @rs1 @rs2 t o1)-substTerm (TArith op a b) o1 =-  TArith op (substTerm @rs1 @rs2 a o1) (substTerm @rs1 @rs2 b o1)-substTerm (TApp2 f a b) o1 =-  TApp2-    f-    (substTerm @rs1 @rs2 a o1)-    (substTerm @rs1 @rs2 b o1) +projectThroughTerm ::+  ( FieldProjection projection,+    KnownSymbol (FieldName projection),+    Typeable projection,+    Typeable (FieldOwner projection),+    Typeable (FieldResult projection)+  ) =>+  FieldWitness projection ->+  Term rs ci ifs (FieldOwner projection) ->+  Term rs ci ifs (FieldResult projection)+projectThroughTerm witness = fst . projectThroughTermWithStatus witness++data ProjectionTransformStatus+  = ProjectionPreserved+  | ProjectionFolded+  | ProjectionLowered+  deriving stock (Eq, Show)++projectThroughTermWithStatus ::+  ( FieldProjection projection,+    KnownSymbol (FieldName projection),+    Typeable projection,+    Typeable (FieldOwner projection),+    Typeable (FieldResult projection)+  ) =>+  FieldWitness projection ->+  Term rs ci ifs (FieldOwner projection) ->+  (Term rs ci ifs (FieldResult projection), ProjectionTransformStatus)+projectThroughTermWithStatus witness (TReg ix) =+  (TFieldProj witness (PBReg ix), ProjectionPreserved)+projectThroughTermWithStatus witness (TInpCtorField ic ix) =+  (TFieldProj witness (PBInp ic ix), ProjectionPreserved)+projectThroughTermWithStatus witness (TLit owner) =+  (TLit (fieldWitnessGet witness owner), ProjectionFolded)+projectThroughTermWithStatus witness ownerTerm =+  (TApp1 (fieldWitnessGet witness) ownerTerm, ProjectionLowered)+ -- | Existentially-coerce a 'Term''s result type /and/ input field -- schema. Unsound in general; justified here by the structural- -- alignment invariant the design note documents: when@@ -754,6 +818,10 @@   TArith op (liftLTermAlt @rs @ci1 @ci2 a) (liftLTermAlt @rs @ci1 @ci2 b) liftLTermAlt (TApp2 f a b) =   TApp2 f (liftLTermAlt @rs @ci1 @ci2 a) (liftLTermAlt @rs @ci1 @ci2 b)+liftLTermAlt (TFieldProj witness base) =+  TFieldProj witness $ case base of+    PBReg ix -> PBReg ix+    PBInp ic ix -> PBInp (leftInCtor ic) ix  -- | Lift a 'Term' from the right side's input alphabet to -- @Either ci1 ci2@. Symmetric to 'liftLTermAlt'.@@ -768,6 +836,10 @@   TArith op (liftRTermAlt @rs @ci1 @ci2 a) (liftRTermAlt @rs @ci1 @ci2 b) liftRTermAlt (TApp2 f a b) =   TApp2 f (liftRTermAlt @rs @ci1 @ci2 a) (liftRTermAlt @rs @ci1 @ci2 b)+liftRTermAlt (TFieldProj witness base) =+  TFieldProj witness $ case base of+    PBReg ix -> PBReg ix+    PBInp ic ix -> PBInp (rightInCtor ic) ix  -- | Lift an 'HsPred' from the left side's input alphabet to -- @Either ci1 ci2@. Walks the AST and recurses through every@@ -1039,6 +1111,10 @@   TArith op (applyEnvTerm env a) (applyEnvTerm env b) applyEnvTerm env (TApp2 f a b) =   TApp2 f (applyEnvTerm env a) (applyEnvTerm env b)+applyEnvTerm env original@(TFieldProj witness (PBReg ix)) =+  maybe original (projectThroughTerm witness) (lookupPending ix env)+applyEnvTerm _ (TFieldProj witness (PBInp ic ix)) =+  TFieldProj witness (PBInp ic ix)  applyEnvPred ::   [PendingWrite rs ci] ->@@ -1138,6 +1214,13 @@       { cawName :: String,         cawSide :: String       }+  | NonStructuralProjectionBoundary+      { cawProjectionT1Edge :: EdgeRef s1,+        cawProjectionT2Edge :: EdgeRef s2,+        cawProjectionPath :: String,+        cawProjectionShape :: String,+        cawProjectionReason :: String+      }   deriving stock (Eq, Show)  data EmittedName s = EmittedName@@ -1173,6 +1256,9 @@ termExpectedReads (TApp1 _ term) = termExpectedReads term termExpectedReads (TApp2 _ a b) = termExpectedReads a ++ termExpectedReads b termExpectedReads (TArith _ a b) = termExpectedReads a ++ termExpectedReads b+termExpectedReads (TFieldProj _ (PBReg _)) = []+termExpectedReads (TFieldProj _ (PBInp ic ix)) =+  [(icName ic, indexPosition ix)]  predCtorAtoms :: HsPred rs ci -> [String] predCtorAtoms PTop = []@@ -1232,13 +1318,119 @@     || "#rmapped" `isInfixOf` name     || "_first" `isSuffixOf` name +upstreamProjectionWarnings ::+  forall rs1 rs2 ci1 mid s1 s2.+  (WeakenR rs1) =>+  EdgeRef s1 ->+  EdgeRef s2 ->+  OutTerm rs1 ci1 mid ->+  HsPred rs2 mid ->+  [ComposeAlignmentWarning s1 s2]+upstreamProjectionWarnings edge1Ref edge2Ref midOutput = goPred+  where+    goPred PTop = []+    goPred PBot = []+    goPred (PAnd a b) = goPred a ++ goPred b+    goPred (POr a b) = goPred a ++ goPred b+    goPred (PNot predicate) = goPred predicate+    goPred (PEq a b) = goTerm a ++ goTerm b+    goPred (PInCtor _) = []+    goPred PLeftArm = []+    goPred PRightArm = []+    goPred (PCmp _ a b) = goTerm a ++ goTerm b++    goTerm :: forall ifs r. Term rs2 mid ifs r -> [ComposeAlignmentWarning s1 s2]+    goTerm (TLit _) = []+    goTerm (TReg _) = []+    goTerm (TInpCtorField _ _) = []+    goTerm (TApp1 _ term) = goTerm term+    goTerm (TApp2 _ a b) = goTerm a ++ goTerm b+    goTerm (TArith _ a b) = goTerm a ++ goTerm b+    goTerm (TFieldProj _ (PBReg _)) = []+    goTerm+      (TFieldProj (witness :: FieldWitness projection) base@(PBInp ic ix))+        | icName ic /= outCtorName midOutput = []+        | otherwise =+            let ownerTerm ::+                  Term+                    (Append rs1 rs2)+                    ci1+                    ifs+                    (FieldOwner projection)+                ownerTerm = substInputField @rs1 @rs2 ic ix midOutput+             in case snd (projectThroughTermWithStatus witness ownerTerm) of+                  ProjectionLowered ->+                    [ NonStructuralProjectionBoundary+                        { cawProjectionT1Edge = edge1Ref,+                          cawProjectionT2Edge = edge2Ref,+                          cawProjectionPath = fieldProjectionPath witness base,+                          cawProjectionShape = fieldShapeId (Proxy @projection),+                          cawProjectionReason = "upstream computed output"+                        }+                    ]+                  ProjectionPreserved -> []+                  ProjectionFolded -> []++pendingProjectionWarnings ::+  forall rs ci s1 s2.+  EdgeRef s1 ->+  EdgeRef s2 ->+  [PendingWrite rs ci] ->+  HsPred rs ci ->+  [ComposeAlignmentWarning s1 s2]+pendingProjectionWarnings edge1Ref edge2Ref env = goPred+  where+    goPred PTop = []+    goPred PBot = []+    goPred (PAnd a b) = goPred a ++ goPred b+    goPred (POr a b) = goPred a ++ goPred b+    goPred (PNot predicate) = goPred predicate+    goPred (PEq a b) = goTerm a ++ goTerm b+    goPred (PInCtor _) = []+    goPred PLeftArm = []+    goPred PRightArm = []+    goPred (PCmp _ a b) = goTerm a ++ goTerm b++    goTerm :: forall ifs r. Term rs ci ifs r -> [ComposeAlignmentWarning s1 s2]+    goTerm (TLit _) = []+    goTerm (TReg _) = []+    goTerm (TInpCtorField _ _) = []+    goTerm (TApp1 _ term) = goTerm term+    goTerm (TApp2 _ a b) = goTerm a ++ goTerm b+    goTerm (TArith _ a b) = goTerm a ++ goTerm b+    goTerm (TFieldProj _ (PBInp _ _)) = []+    goTerm+      (TFieldProj (witness :: FieldWitness projection) base@(PBReg ix)) =+        case lookupPending ix env of+          Nothing -> []+          Just ownerTerm ->+            case snd (projectThroughTermWithStatus witness ownerTerm) of+              ProjectionLowered ->+                [ NonStructuralProjectionBoundary+                    { cawProjectionT1Edge = edge1Ref,+                      cawProjectionT2Edge = edge2Ref,+                      cawProjectionPath = fieldProjectionPath witness base,+                      cawProjectionShape = fieldShapeId (Proxy @projection),+                      cawProjectionReason = "pending write"+                    }+                ]+              ProjectionPreserved -> []+              ProjectionFolded -> []+ -- | Check constructor-name and field-position alignment before building a -- composite. Reachable vertex pairs are expanded from the two initial -- vertices; multi-event outputs advance the downstream machine one symbol -- at a time, matching 'compose''s path expansion conservatively. checkComposeAlignment ::   forall rs1 rs2 s1 s2 ci1 mid co.-  (Bounded s1, Enum s1, Ord s1, Bounded s2, Enum s2, Ord s2) =>+  ( WeakenR rs1,+    Bounded s1,+    Enum s1,+    Ord s1,+    Bounded s2,+    Enum s2,+    Ord s2+  ) =>   SymTransducer (HsPred rs1 ci1) rs1 s1 ci1 mid ->   SymTransducer (HsPred rs2 mid) rs2 s2 mid co ->   [ComposeAlignmentWarning s1 s2]@@ -1269,7 +1461,7 @@       ]      warningsAt (v1, v2) =-      unconsumed ++ unmatched ++ arity ++ poison+      unconsumed ++ unmatched ++ arity ++ poison ++ projection       where         t1Edges = zip [0 ..] (edgesOut t1 v1)         t2Edges = zip [0 ..] (edgesOut t2 v2)@@ -1313,6 +1505,50 @@                 ++ [(name, "downstream input") | name <- expectedNames],             isPoisonedBoundaryName name           ]++        projection = concatMap projectionForEdge t1Edges++        projectionForEdge (edgeIx, edge1) =+          let edge1Ref = EdgeRef v1 edgeIx+           in case output edge1 of+                [] -> []+                [midOutput] ->+                  concat+                    [ upstreamProjectionWarnings+                        edge1Ref+                        (EdgeRef v2 edge2Ix)+                        midOutput+                        (guard edge2)+                    | (edge2Ix, edge2) <- t2Edges+                    ]+                midOutputs ->+                  projectionPathWarnings edge1Ref midOutputs [] v2++        projectionPathWarnings _ [] _ _ = []+        projectionPathWarnings edge1Ref (midOutput : rest) env vertex =+          concat+            [ case edge2 of+                Edge {update = edge2Update} ->+                  let edge2Ref = EdgeRef vertex edge2Ix+                      substitutedGuard = substPred @rs1 @rs2 (guard edge2) midOutput+                      upstreamWarnings =+                        upstreamProjectionWarnings+                          edge1Ref+                          edge2Ref+                          midOutput+                          (guard edge2)+                      pendingWarnings =+                        pendingProjectionWarnings edge1Ref edge2Ref env substitutedGuard+                      stepUpdate =+                        applyEnvUpdate+                          env+                          (substUpdate @rs1 @rs2 edge2Update midOutput)+                      nextEnv = pendingWrites stepUpdate ++ env+                   in upstreamWarnings+                        ++ pendingWarnings+                        ++ projectionPathWarnings edge1Ref rest nextEnv (target edge2)+            | (edge2Ix, edge2) <- zip [0 ..] (edgesOut t2 vertex)+            ]  -- | Checked entry point for validated aggregate pipelines. The unchecked -- 'compose' primitive remains available for internal/experimental use.

@@ -3,6 +3,7 @@ -- Same reasoning for any future helpers that re-export the constraint -- as a typed witness. {-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeFamilies #-} -- Validation diagnostics intentionally expose constructor-specific record -- selectors. Changing them to total fields would break the public diagnostic -- API, so keep the partiality explicit and silence the definition-site warning.@@ -59,6 +60,10 @@     -- * Term language     Term (..),     NumOp (..),+    FieldProjection (..),+    FieldWitness,+    fieldWitness,+    ProjBase (..),      -- * Input-side structural constructor (v2)     InCtor (..),@@ -106,6 +111,8 @@     matchInCtor,     proj,     inpCtor,+    regProj,+    inpProj,     lit,     tadd,     tsub,@@ -186,6 +193,10 @@     hiddenInputReasons,     detectMissingInCtorFields,     MissingInCtorFields (..),+    fieldProjectionPath,+    fieldWitnessAgrees,+    fieldWitnessGet,+    indexPosition,   ) where @@ -206,6 +217,11 @@     IndexN (..),     Names,   )+import Keiki.Internal.SymbolicTypes+  ( discoverSymbolicType,+    symbolicTypeSupportsEquality,+    symbolicTypeSupportsOrdering,+  ) import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))  -- | A register slot is a label paired with the type of its value.@@ -306,6 +322,71 @@ data NumOp = OpAdd | OpSub | OpMul   deriving stock (Eq, Show) +-- | One nominal, solver-visible projection from a consumer-owned value.+-- Define one fresh tag type and one coherent instance per logical field, and+-- reuse that canonical tag at every occurrence of the field. The tag's+-- 'Typeable' identity, rather than 'FieldName' or 'fieldShapeId', is used by+-- the symbolic layer to decide variable sharing. Two different tags for the+-- same logical field are sound but imprecise: the solver treats them as+-- independent values.+--+-- 'projectFieldValue' must be total for every well-formed 'FieldOwner'.+-- 'FieldName' and 'fieldShapeId' must truthfully describe that getter.+-- Normal Haskell instance coherence supplies one getter per tag; defining+-- incoherent instances is outside Keiki's supported contract. Keiki checks+-- concrete term behavior and supplies 'fieldWitnessAgrees'; a binding+-- generator such as Keiro remains responsible for proving that a generated+-- instance agrees with its schema and codec provenance. A dishonest instance+-- can therefore misname a field, but cannot make one coherent tag mean two+-- different getters.+class FieldProjection projection where+  type FieldName projection :: Symbol+  type FieldOwner projection :: Type+  type FieldResult projection :: Type+  fieldShapeId :: Proxy projection -> String+  projectFieldValue ::+    Proxy projection -> FieldOwner projection -> FieldResult projection++-- | Abstract nominal token for a coherent 'FieldProjection' instance.+-- Construct one with 'fieldWitness'. Its nominal role prevents changing the+-- projection tag with 'coerce', and the tag's 'TypeRep' supplies symbolic+-- cache identity independently of caller-controlled diagnostic strings.+type role FieldWitness nominal++data FieldWitness projection = FieldWitness++-- | Construct the abstract witness for a projection tag. Normal Haskell+-- instance coherence supplies one getter per tag; generators should therefore+-- reuse one canonical tag for every occurrence of the same logical field and+-- test it against the schema-derived reference getter with+-- 'fieldWitnessAgrees'. Duplicate tags remain sound, but lose proof precision.+fieldWitness ::+  ( FieldProjection projection,+    KnownSymbol (FieldName projection),+    Typeable projection,+    Typeable (FieldOwner projection),+    Typeable (FieldResult projection)+  ) =>+  FieldWitness projection+fieldWitness = FieldWitness++-- | Eliminate a 'FieldWitness' using its coherent projection instance.+fieldWitnessGet ::+  forall projection.+  (FieldProjection projection) =>+  FieldWitness projection ->+  FieldOwner projection ->+  FieldResult projection+fieldWitnessGet _ = projectFieldValue (Proxy @projection)++-- | Where a structural field projection may read its owner value. Restricting+-- the base to a register slot or one input-constructor field gives the+-- symbolic layer a stable, typed path identity. Arbitrary computed bases are+-- deliberately not representable here.+data ProjBase (rs :: [Slot]) (ci :: Type) (ifs :: [Slot]) owner where+  PBReg :: Index rs owner -> ProjBase rs ci ifs owner+  PBInp :: InCtor ci ifs -> Index ifs owner -> ProjBase rs ci ifs owner+ -- | A pure expression over the register file and the input symbol, -- yielding a value of type @r@. --@@ -352,6 +433,24 @@     Term rs ci ifs r ->     Term rs ci ifs r ->     Term rs ci ifs r+  -- | A single-hop, solver-visible field projection. The coherent nominal tag+  -- identifies the logical getter; only the projected result needs symbolic+  -- support, while the consumer-owned base value does not. Concrete+  -- evaluation applies the total getter. Symbolic translation creates a free+  -- variable for the typed path, so agreement is intentionally one-way: a+  -- concrete owner can constrain that variable to its getter result, but a+  -- solver model cannot reconstruct the owner. Default validation permits+  -- this node in guards and rejects it in updates or outputs.+  TFieldProj ::+    ( FieldProjection projection,+      KnownSymbol (FieldName projection),+      Typeable projection,+      Typeable (FieldOwner projection),+      Typeable (FieldResult projection)+    ) =>+    FieldWitness projection ->+    ProjBase rs ci ifs (FieldOwner projection) ->+    Term rs ci ifs (FieldResult projection)  -- | Per-constructor input projection. An 'InCtor' value names one -- constructor of the input symbol type @ci@ and pins the round-trip@@ -749,6 +848,42 @@ inpCtor :: InCtor ci ifs -> Index ifs r -> Term rs ci ifs r inpCtor = TInpCtorField +-- | Project one field from a consumer-owned value stored in a register slot.+-- The total getter comes from the witness's coherent nominal instance.+-- Repeated reads of this exact typed path share one symbolic variable without+-- requiring the owner type itself to be symbolic. That symbolic value is an+-- over-approximation: concrete owners can be bound to it, but solver models do+-- not reconstruct owners.+regProj ::+  ( FieldProjection projection,+    KnownSymbol (FieldName projection),+    Typeable projection,+    Typeable (FieldOwner projection),+    Typeable (FieldResult projection)+  ) =>+  FieldWitness projection ->+  Index rs (FieldOwner projection) ->+  Term rs ci ifs (FieldResult projection)+regProj witness ix = TFieldProj witness (PBReg ix)++-- | Project one field from a consumer-owned value carried by the matched+-- input constructor. The getter and one-way symbolic agreement laws are the+-- same as for 'regProj'. Pair this term with the corresponding 'matchInCtor'+-- guard, just as for 'inpCtor'; validation treats the projected read as a read+-- of the whole underlying input field.+inpProj ::+  ( FieldProjection projection,+    KnownSymbol (FieldName projection),+    Typeable projection,+    Typeable (FieldOwner projection),+    Typeable (FieldResult projection)+  ) =>+  FieldWitness projection ->+  InCtor ci ifs ->+  Index ifs (FieldOwner projection) ->+  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 lit = TLit@@ -860,6 +995,16 @@ evalTerm (TApp2 f a b) regs ci = f (evalTerm a regs ci) (evalTerm b regs ci) evalTerm (TArith op a b) regs ci =   applyNumOp op (evalTerm a regs ci) (evalTerm b regs ci)+evalTerm (TFieldProj witness base) regs ci =+  fieldWitnessGet witness $ case base of+    PBReg ix -> regs ! ix+    PBInp ic ix -> case icMatch ic ci of+      Just rf -> rf ! ix+      Nothing ->+        error+          ( "evalTerm: TFieldProj input guard violation: "+              ++ icName ic+          )  -- | Interpret a 'NumOp' tag as the corresponding numeric operation. -- The 'Num' evidence is supplied by matching the 'TArith' constructor.@@ -1478,6 +1623,7 @@     recomputeOne term@(TApp1 _ _) _observed = evalTerm term regs ci     recomputeOne term@(TApp2 _ _ _) _observed = evalTerm term regs ci     recomputeOne term@(TArith _ _ _) _observed = evalTerm term regs ci+    recomputeOne term@TFieldProj {} _observed = evalTerm term regs ci     recomputeOne _ observed = observed  -- | Walk an 'OutFields' HList in lockstep with an observed-fields@@ -1528,6 +1674,7 @@     stepOne (TApp1 _ _) _val _ = Just []     stepOne (TApp2 _ _ _) _val _ = Just []     stepOne (TArith _ _ _) _val _ = Just []+    stepOne TFieldProj {} _val _ = Just []  -- | A diagnostic produced by 'checkHiddenInputs'. data HiddenInputWarning = HiddenInputWarning@@ -1717,6 +1864,8 @@ termReadsInput (TApp1 _ t) = termReadsInput t termReadsInput (TApp2 _ a b) = termReadsInput a || termReadsInput b termReadsInput (TArith _ a b) = termReadsInput a || termReadsInput b+termReadsInput (TFieldProj _ (PBReg _)) = False+termReadsInput (TFieldProj _ (PBInp _ _)) = True  -- | Do the 'OutFields' contain a 'TInpCtorField' read anywhere? outFieldsHaveInpCtorField :: OutFields rs ci ifs fs -> Bool@@ -1731,6 +1880,8 @@     termHasInpCtorField (TApp1 _ t') = termHasInpCtorField t'     termHasInpCtorField (TApp2 _ a b) = termHasInpCtorField a || termHasInpCtorField b     termHasInpCtorField (TArith _ a b) = termHasInpCtorField a || termHasInpCtorField b+    termHasInpCtorField (TFieldProj _ (PBReg _)) = False+    termHasInpCtorField (TFieldProj _ (PBInp _ _)) = True  -- | The result of 'detectMissingInCtorFields': the offending 'InCtor' -- name plus the names of slots its 'OutFields' walk does not visit.@@ -1782,6 +1933,45 @@ slotNamesOf :: forall ci ifs. InCtor ci ifs -> [String] slotNamesOf InCtor {} = slotNames @ifs +-- | Zero-based position of an 'Index' in its slot list. Symbolic projection+-- identity includes the position as well as the diagnostic name, so manually+-- constructed duplicate-labelled schemas cannot accidentally share a value.+indexPosition :: Index xs a -> Int+indexPosition ZIdx = 0+indexPosition (SIdx ix) = 1 + indexPosition ix++indexNameOf :: Index xs a -> String+indexNameOf (ZIdx @name) = symbolVal (Proxy @name)+indexNameOf (SIdx ix) = indexNameOf ix++-- | Render the stable base and field name of a projection as a dotted path.+-- This string is diagnostic only; symbolic variable identity is structural.+fieldProjectionPath ::+  forall projection rs ci ifs.+  (FieldProjection projection, KnownSymbol (FieldName projection)) =>+  FieldWitness projection ->+  ProjBase rs ci ifs (FieldOwner projection) ->+  String+fieldProjectionPath _ base =+  basePath <> "." <> symbolVal (Proxy @(FieldName projection))+  where+    basePath = case base of+      PBReg ix -> indexNameOf ix+      PBInp ic ix -> icName ic <> "." <> indexNameOf ix++-- | Check a projection instance's getter against a reference getter on one+-- owner value. Generators can QuickCheck this helper over their own owner+-- generators and mutation-test an intentionally wrong instance.+fieldWitnessAgrees ::+  forall projection.+  (FieldProjection projection, Eq (FieldResult projection)) =>+  FieldWitness projection ->+  (FieldOwner projection -> FieldResult projection) ->+  FieldOwner projection ->+  Bool+fieldWitnessAgrees witness reference owner =+  fieldWitnessGet witness owner == reference owner+ -- * Build-time validation umbrella (EP-56) --------------------------------  -- | A structured build-time validation warning, parameterized over the@@ -1872,6 +2062,35 @@       { tvwEdge :: EdgeRef s,         tvwDetail :: String       }+  | -- | A field projection's result type is outside the curated symbolic+    --       equality registry. Translating such a guard would otherwise fall+    --       back to an opaque Boolean and silently lose the promised proof.+    ProjectionResultUnsupported+      { tvwEdge :: EdgeRef s,+        tvwProjectionPath :: String,+        tvwProjectionShape :: String,+        tvwProjectionResultType :: String,+        tvwDetail :: String+      }+  | -- | A field projection occurs under an ordering comparison, but its+    --       result type has no curated symbolic ordering dictionary.+    ProjectionOrderingUnsupported+      { tvwEdge :: EdgeRef s,+        tvwProjectionPath :: String,+        tvwProjectionShape :: String,+        tvwProjectionResultType :: String,+        tvwDetail :: String+      }+  | -- | A field projection occurs in an update or output. Projections are a+    --       guard-only structural feature; raw evaluation remains total, but+    --       default validation rejects this placement.+    ProjectionOutsideGuard+      { tvwEdge :: EdgeRef s,+        tvwProjectionPath :: String,+        tvwProjectionShape :: String,+        tvwProjectionLocation :: String,+        tvwDetail :: String+      }   deriving stock (Eq, Show)  -- | Which checks 'validateTransducer' runs. Construct options by updating@@ -1964,7 +2183,8 @@           | w <- checkDeadEdges defaultDeadEdgeOptions t           ]         else [],-      if warnOpaqueGuards opts then opaqueGuardWarnings t else []+      if warnOpaqueGuards opts then opaqueGuardWarnings t else [],+      projectionValidationWarnings t     ]  -- | Structured form of the hidden-input check, additive over@@ -2032,6 +2252,7 @@ termHasOpaqueApp (TApp1 _ _) = True termHasOpaqueApp (TApp2 _ _ _) = True termHasOpaqueApp (TArith _ a b) = termHasOpaqueApp a || termHasOpaqueApp b+termHasOpaqueApp TFieldProj {} = False  -- | Does the guard predicate branch on an opaque term anywhere? The symbolic -- analyses cannot see through such a guard (it becomes a free SBV variable),@@ -2069,6 +2290,145 @@     predHasOpaqueTerm (guard e)   ] +-- ** Field-projection diagnostics++data ProjectionInfo = ProjectionInfo+  { projectionInfoPath :: String,+    projectionInfoShape :: String,+    projectionInfoResultType :: String,+    projectionInfoSupportsEquality :: Bool,+    projectionInfoSupportsOrdering :: Bool+  }++termProjectionInfos :: Term rs ci ifs r -> [ProjectionInfo]+termProjectionInfos (TLit _) = []+termProjectionInfos (TReg _) = []+termProjectionInfos (TInpCtorField _ _) = []+termProjectionInfos (TApp1 _ term) = termProjectionInfos term+termProjectionInfos (TApp2 _ a b) =+  termProjectionInfos a ++ termProjectionInfos b+termProjectionInfos (TArith _ a b) =+  termProjectionInfos a ++ termProjectionInfos b+termProjectionInfos+  (TFieldProj (witness :: FieldWitness projection) base) =+    [ ProjectionInfo+        { projectionInfoPath = fieldProjectionPath witness base,+          projectionInfoShape = fieldShapeId (Proxy @projection),+          projectionInfoResultType = show (typeRep @(FieldResult projection)),+          projectionInfoSupportsEquality =+            maybe+              False+              symbolicTypeSupportsEquality+              (discoverSymbolicType @(FieldResult projection)),+          projectionInfoSupportsOrdering =+            maybe+              False+              symbolicTypeSupportsOrdering+              (discoverSymbolicType @(FieldResult projection))+        }+    ]++updateProjectionInfos :: Update rs w ci -> [ProjectionInfo]+updateProjectionInfos UKeep = []+updateProjectionInfos (USet _ term) = termProjectionInfos term+updateProjectionInfos (UCombine a b) =+  updateProjectionInfos a ++ updateProjectionInfos b++outFieldsProjectionInfos :: OutFields rs ci ifs fs -> [ProjectionInfo]+outFieldsProjectionInfos OFNil = []+outFieldsProjectionInfos (OFCons term rest) =+  termProjectionInfos term ++ outFieldsProjectionInfos rest++outTermProjectionInfos :: OutTerm rs ci co -> [ProjectionInfo]+outTermProjectionInfos (OPack _ _ fields) = outFieldsProjectionInfos fields++projectionValidationWarnings ::+  (Bounded s, Enum s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  [TransducerValidationWarning s]+projectionValidationWarnings transducer =+  concat+    [ warningsForEdge (EdgeRef source edgeNumber) edge+    | source <- [minBound .. maxBound],+      (edgeNumber, edge) <- zip [(0 :: Int) ..] (edgesOut transducer source)+    ]+  where+    warningsForEdge edgeRef Edge {guard = edgeGuard, update = edgeUpdate, output = edgeOutput} =+      guardWarnings edgeRef edgeGuard+        ++ outsideWarnings edgeRef "update" (updateProjectionInfos edgeUpdate)+        ++ outsideWarnings+          edgeRef+          "output"+          (concatMap outTermProjectionInfos edgeOutput)++    guardWarnings _ PTop = []+    guardWarnings _ PBot = []+    guardWarnings edgeRef (PAnd a b) =+      guardWarnings edgeRef a ++ guardWarnings edgeRef b+    guardWarnings edgeRef (POr a b) =+      guardWarnings edgeRef a ++ guardWarnings edgeRef b+    guardWarnings edgeRef (PNot predicate) = guardWarnings edgeRef predicate+    guardWarnings edgeRef (PEq a b) =+      concatMap (equalityWarnings edgeRef) (termProjectionInfos a ++ termProjectionInfos b)+    guardWarnings _ (PInCtor _) = []+    guardWarnings _ PLeftArm = []+    guardWarnings _ PRightArm = []+    guardWarnings edgeRef (PCmp _ a b) =+      concatMap+        (\info -> equalityWarnings edgeRef info ++ orderingWarnings edgeRef info)+        (termProjectionInfos a ++ termProjectionInfos b)++    equalityWarnings edgeRef info+      | projectionInfoSupportsEquality info = []+      | otherwise =+          [ ProjectionResultUnsupported+              { tvwEdge = edgeRef,+                tvwProjectionPath = projectionInfoPath info,+                tvwProjectionShape = projectionInfoShape info,+                tvwProjectionResultType = projectionInfoResultType info,+                tvwDetail =+                  "projection "+                    <> projectionInfoPath info+                    <> " has result type "+                    <> projectionInfoResultType info+                    <> " outside Keiki's symbolic equality registry"+              }+          ]++    orderingWarnings edgeRef info+      | projectionInfoSupportsOrdering info = []+      | otherwise =+          [ ProjectionOrderingUnsupported+              { tvwEdge = edgeRef,+                tvwProjectionPath = projectionInfoPath info,+                tvwProjectionShape = projectionInfoShape info,+                tvwProjectionResultType = projectionInfoResultType info,+                tvwDetail =+                  "projection "+                    <> projectionInfoPath info+                    <> " has result type "+                    <> projectionInfoResultType info+                    <> " without symbolic ordering support"+              }+          ]++    outsideWarnings edgeRef location =+      map+        ( \info ->+            ProjectionOutsideGuard+              { tvwEdge = edgeRef,+                tvwProjectionPath = projectionInfoPath info,+                tvwProjectionShape = projectionInfoShape info,+                tvwProjectionLocation = location,+                tvwDetail =+                  "projection "+                    <> projectionInfoPath info+                    <> " appears in an edge "+                    <> location+                    <> "; field projections are supported only in guards"+              }+        )+ -- ** Guarded input-read diagnostics  termInCtorNames :: Term rs ci ifs r -> [String]@@ -2078,6 +2438,8 @@ termInCtorNames (TApp1 _ t) = termInCtorNames t termInCtorNames (TApp2 _ a b) = termInCtorNames a ++ termInCtorNames b termInCtorNames (TArith _ a b) = termInCtorNames a ++ termInCtorNames b+termInCtorNames (TFieldProj _ (PBReg _)) = []+termInCtorNames (TFieldProj _ (PBInp ic _)) = [icName ic]  predInCtorReadNames :: HsPred rs ci -> [String] predInCtorReadNames PTop = []

@@ -0,0 +1,75 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeApplications #-}++-- | The cycle-free, curated set of concrete types understood by Keiki's+-- symbolic layer. This module deliberately contains no SBV dictionaries:+-- 'Keiki.Core' can use it for validation without importing+-- 'Keiki.Symbolic', while 'Keiki.Symbolic' turns the same constructors into+-- the required dictionaries.+module Keiki.Internal.SymbolicTypes+  ( SymbolicType (..),+    discoverSymbolicType,+    symbolicTypeSupportsEquality,+    symbolicTypeSupportsOrdering,+    symbolicTypeSupportsNumeric,+  )+where++import Data.Int (Int32, Int64)+import Data.Text (Text)+import Data.Time (UTCTime)+import Data.Typeable (Typeable)+import Data.Word (Word16, Word32, Word64, Word8)+import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))++-- | Evidence that a type belongs to Keiki's closed symbolic registry.+data SymbolicType r where+  SymbolicBool :: SymbolicType Bool+  SymbolicInt :: SymbolicType Int+  SymbolicInteger :: SymbolicType Integer+  SymbolicText :: SymbolicType Text+  SymbolicUTCTime :: SymbolicType UTCTime+  SymbolicWord64 :: SymbolicType Word64+  SymbolicWord32 :: SymbolicType Word32+  SymbolicWord16 :: SymbolicType Word16+  SymbolicWord8 :: SymbolicType Word8+  SymbolicInt64 :: SymbolicType Int64+  SymbolicInt32 :: SymbolicType Int32++-- | Discover membership in the curated registry without importing SBV.+discoverSymbolicType :: forall r. (Typeable r) => Maybe (SymbolicType r)+discoverSymbolicType+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Bool) = Just SymbolicBool+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int) = Just SymbolicInt+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Integer) = Just SymbolicInteger+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Text) = Just SymbolicText+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @UTCTime) = Just SymbolicUTCTime+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word64) = Just SymbolicWord64+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word32) = Just SymbolicWord32+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word16) = Just SymbolicWord16+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word8) = Just SymbolicWord8+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int64) = Just SymbolicInt64+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int32) = Just SymbolicInt32+  | otherwise = Nothing++-- | Every curated type supports symbolic equality.+symbolicTypeSupportsEquality :: SymbolicType r -> Bool+symbolicTypeSupportsEquality _ = True++-- | Whether the registry supplies symbolic ordering for this type.+symbolicTypeSupportsOrdering :: SymbolicType r -> Bool+symbolicTypeSupportsOrdering SymbolicBool = False+symbolicTypeSupportsOrdering SymbolicText = False+symbolicTypeSupportsOrdering _ = True++-- | Whether the registry supplies symbolic numeric operations for this type.+symbolicTypeSupportsNumeric :: SymbolicType r -> Bool+symbolicTypeSupportsNumeric SymbolicInt = True+symbolicTypeSupportsNumeric SymbolicInteger = True+symbolicTypeSupportsNumeric SymbolicWord64 = True+symbolicTypeSupportsNumeric SymbolicWord32 = True+symbolicTypeSupportsNumeric SymbolicWord16 = True+symbolicTypeSupportsNumeric SymbolicWord8 = True+symbolicTypeSupportsNumeric SymbolicInt64 = True+symbolicTypeSupportsNumeric SymbolicInt32 = True+symbolicTypeSupportsNumeric _ = False

@@ -767,6 +767,10 @@         goTerm (TApp1 h a) = TApp1 h (goTerm a)         goTerm (TApp2 h a b) = TApp2 h (goTerm a) (goTerm b)         goTerm (TArith op a b) = TArith op (goTerm a) (goTerm b)+        goTerm (TFieldProj witness base) =+          TFieldProj witness $ case base of+            PBReg ix -> PBReg ix+            PBInp _ ix -> PBInp cic (SIdx ix)  -- | Standard 'Data.Profunctor.Strong.Strong' instance. Threads an -- unrelated value through a transducer.@@ -957,6 +961,10 @@     go (TApp1 h a) = TApp1 h (go a)     go (TApp2 h a b) = TApp2 h (go a) (go b)     go (TArith op a b) = TArith op (go a) (go b)+    go (TFieldProj witness base) =+      TFieldProj witness $ case base of+        PBReg ix -> PBReg ix+        PBInp ic ix -> PBInp (contraInCtor f ic) ix  contraMaybeTerm :: forall ci ci' rs ifs r. (ci' -> Maybe ci) -> Term rs ci ifs r -> Term rs ci' ifs r contraMaybeTerm f = go@@ -968,6 +976,10 @@     go (TApp1 h a) = TApp1 h (go a)     go (TApp2 h a b) = TApp2 h (go a) (go b)     go (TArith op a b) = TArith op (go a) (go b)+    go (TFieldProj witness base) =+      TFieldProj witness $ case base of+        PBReg ix -> PBReg ix+        PBInp ic ix -> PBInp (contraMaybeInCtor f ic) ix  -- ** HsPred ------------------------------------------------------------- 

@@ -30,6 +30,7 @@     NumOp (..),     Term (..),     Update (..),+    fieldProjectionPath,   ) import Keiki.Internal.Slots (indexNName) @@ -66,6 +67,8 @@     numOpSym OpAdd = T.pack "+"     numOpSym OpSub = T.pack "-"     numOpSym OpMul = T.pack "*"+prettyTerm (TFieldProj witness base) =+  T.pack (fieldProjectionPath witness base)  -- | Render an 'HsPred' guard as domain-readable 'Text'. Boolean -- structure renders with @&& || !@ and parentheses; @PInCtor@ renders

@@ -24,8 +24,9 @@ --     solver-visible). --   * 'SymEnv' carrying the shared symbolic input-constructor tag and --     (since EP-42 of MasterPlan 12) an 'IORef' memo cache that shares---     one SBV variable per register slot / input field across repeated---     reads, so @proj #x .== proj #x@ is valid, not merely satisfiable.+--     one SBV variable per register slot, input field, or nominal typed field+--     projection across repeated reads, so @proj #x .== proj #x@ and repeated+--     projected reads are valid, not merely satisfiable. --   * 'translateTermSym' / 'translatePred' walking 'Term' / 'HsPred' --     into SBV expressions. --   * 'discoverSym' — runtime dispatch from 'Typeable' to 'Sym'@@ -60,6 +61,7 @@     mkSymEnv,     translateTermSym,     translatePred,+    constrainFieldProjection,      -- * Symbolic predicate wrapper     SymPred (..),@@ -106,8 +108,12 @@ import Data.Word (Word16, Word32, Word64, Word8) import GHC.TypeLits (KnownSymbol, symbolVal) import Keiki.Core+import Keiki.Internal.SymbolicTypes+  ( SymbolicType (..),+    discoverSymbolicType,+  ) import System.IO.Unsafe (unsafePerformIO)-import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))+import Type.Reflection (SomeTypeRep (..), eqTypeRep, typeRep, type (:~~:) (HRefl))  -- * Symbolic representation ------------------------------------------------- @@ -235,19 +241,19 @@ -- SBV terms; a miss falls back to a fresh 'SBool' (loses precision but -- stays sound). discoverSym :: forall r. (Typeable r) => Maybe (SymDict r)-discoverSym-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Bool) = Just SymDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int) = Just SymDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Integer) = Just SymDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Text) = Just SymDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @UTCTime) = Just SymDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word64) = Just SymDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word32) = Just SymDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word16) = Just SymDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word8) = Just SymDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int64) = Just SymDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int32) = Just SymDict-  | otherwise = Nothing+discoverSym = case discoverSymbolicType @r of+  Just SymbolicBool -> Just SymDict+  Just SymbolicInt -> Just SymDict+  Just SymbolicInteger -> Just SymDict+  Just SymbolicText -> Just SymDict+  Just SymbolicUTCTime -> Just SymDict+  Just SymbolicWord64 -> Just SymDict+  Just SymbolicWord32 -> Just SymDict+  Just SymbolicWord16 -> Just SymDict+  Just SymbolicWord8 -> Just SymDict+  Just SymbolicInt64 -> Just SymDict+  Just SymbolicInt32 -> Just SymDict+  Nothing -> Nothing  -- | Reify both a 'Sym' instance for @r@ and evidence that its -- 'SymRep' is symbolically orderable (an 'SBV.OrdSymbolic' instance on@@ -268,17 +274,19 @@ -- translator fall back to a fresh opaque 'SBool', exactly as 'goEq' -- does for non-'Sym' operands — sound, just imprecise. discoverSymOrd :: forall r. (Typeable r) => Maybe (SymOrdDict r)-discoverSymOrd-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int) = Just SymOrdDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Integer) = Just SymOrdDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word64) = Just SymOrdDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word32) = Just SymOrdDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word16) = Just SymOrdDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word8) = Just SymOrdDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int64) = Just SymOrdDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int32) = Just SymOrdDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @UTCTime) = Just SymOrdDict-  | otherwise = Nothing+discoverSymOrd = case discoverSymbolicType @r of+  Just SymbolicInt -> Just SymOrdDict+  Just SymbolicInteger -> Just SymOrdDict+  Just SymbolicUTCTime -> Just SymOrdDict+  Just SymbolicWord64 -> Just SymOrdDict+  Just SymbolicWord32 -> Just SymOrdDict+  Just SymbolicWord16 -> Just SymOrdDict+  Just SymbolicWord8 -> Just SymOrdDict+  Just SymbolicInt64 -> Just SymOrdDict+  Just SymbolicInt32 -> Just SymOrdDict+  Just SymbolicBool -> Nothing+  Just SymbolicText -> Nothing+  Nothing -> Nothing  -- | Reify both a 'Sym' instance for @r@ and evidence that its 'SymRep' -- is symbolically /numeric/ (a 'Num' instance on @'SBV.SBV' ('SymRep'@@ -302,16 +310,19 @@ -- fallback is only reachable for a numeric type intentionally left out -- of the registry.) discoverSymNum :: forall r. (Typeable r) => Maybe (SymNumDict r)-discoverSymNum-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int) = Just SymNumDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Integer) = Just SymNumDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word64) = Just SymNumDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word32) = Just SymNumDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word16) = Just SymNumDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word8) = Just SymNumDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int64) = Just SymNumDict-  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int32) = Just SymNumDict-  | otherwise = Nothing+discoverSymNum = case discoverSymbolicType @r of+  Just SymbolicInt -> Just SymNumDict+  Just SymbolicInteger -> Just SymNumDict+  Just SymbolicWord64 -> Just SymNumDict+  Just SymbolicWord32 -> Just SymNumDict+  Just SymbolicWord16 -> Just SymNumDict+  Just SymbolicWord8 -> Just SymNumDict+  Just SymbolicInt64 -> Just SymNumDict+  Just SymbolicInt32 -> Just SymNumDict+  Just SymbolicBool -> Nothing+  Just SymbolicText -> Nothing+  Just SymbolicUTCTime -> Nothing+  Nothing -> Nothing  -- | Lift a concrete value to an SBV literal of its 'SymRep'. symLit :: forall a. (Sym a) => a -> SBV.SBV (SymRep a)@@ -337,17 +348,33 @@ --   * 'seInputArm' — an independent discriminator for 'PLeftArm' and --     'PRightArm'. It is separate from constructor names so both facts can --     be asserted by the same guard.---   * 'seVarCache' — a per-translation memo cache (EP-42) keyed by the---     deterministic variable name ('TReg' allocates @"reg/\<slot\>"@,---     'TInpCtorField' allocates @"inp/\<ctor\>/\<field\>"@). The first---     read of a name allocates one 'SBV.free' variable and stores it;---     every later read of the same name returns the cached variable.+--   * 'seVarCache' — a per-translation memo cache (EP-42) keyed by a+--     structured 'SymVarKey'. Ordinary register and input reads preserve their+--     historical labels; field projections use base position and nominal+--     'TypeRep' identity, never caller-controlled diagnostic strings alone.+--     The first read allocates one 'SBV.free' variable and stores it; every+--     later read of the same key returns the cached variable. --     This makes the solver see two reads of @#x@ as the /same/ value, --     so @proj #x .== proj #x@ is valid (not merely satisfiable). The --     'TApp1' \/ 'TApp2' escape hatches are deliberately /not/ cached: --     they wrap opaque Haskell functions with no 'Eq', so two --     applications cannot be recognized as equal and each stays a fresh --     per-occurrence variable.+data ProjectionBaseKey+  = ProjectionReg String Int+  | ProjectionInp String String Int+  deriving stock (Eq, Ord, Show)++data SymVarKey+  = RegVar String+  | InpVar String String+  | ProjectionVar+      ProjectionBaseKey+      SomeTypeRep+      SomeTypeRep+      SomeTypeRep+  deriving stock (Eq, Ord, Show)+ data SymEnv = SymEnv   { -- | The shared symbolic input constructor tag. 'PInCtor' atoms     --     assert @seInputCtor .== literal (icName ic)@; the solver@@ -363,7 +390,11 @@     --     falls back to 'symDefault' for them). Scoped to one     --     'translatePred' walk (one 'mkSymEnv'), so variables are shared     --     /within/ a query but never leak across independent queries.-    seVarCache :: IORef (Map String SomeSBV)+    seVarCache :: IORef (Map SymVarKey SomeSBV),+    -- | Next internal projection label. Projection labels are intentionally+    --     generated by Keiki so arbitrary schema names never reach SBV's+    --     restricted label namespace.+    seProjectionOrdinal :: IORef Int   }  -- | An SBV variable of some representation type, packed so the memo@@ -384,7 +415,8 @@   ctor <- SBV.free "inputCtor"   arm <- SBV.free "inputArm"   cache <- liftIO (newIORef Map.empty)-  pure (SymEnv ctor arm cache)+  projectionOrdinal <- liftIO (newIORef 0)+  pure (SymEnv ctor arm cache projectionOrdinal)  -- * Translation ------------------------------------------------------------- @@ -409,17 +441,23 @@ --   * 'TInpCtorField' allocates --     @"inp/<icName>/<slotName>"@ — the 'InCtor''s name plus the --     field's slot label.+--   * 'TFieldProj' uses a structured cache key containing the base position,+--     nominal projection tag, owner type, and result type. Its actual SBV+--     label is an internal @"proj/<ordinal>"@, so arbitrary schema strings+--     cannot collide with or violate SBV's label syntax. --   * 'TApp1' / 'TApp2' keep their anonymous names; their values are --     not extracted as part of the witness. ----- Note on repeated reads (EP-42): 'TReg' and 'TInpCtorField' reads are--- memoized through the env's 'seVarCache'. The first read of a given--- slot\/field allocates one 'SBV.free' variable and caches it under its--- deterministic name; every later read of the same name returns the--- cached variable. So two reads of the same slot (e.g.+-- Note on repeated reads (EP-42): 'TReg', 'TInpCtorField', and+-- 'TFieldProj' reads are memoized through the env's 'seVarCache'. The first+-- read of a given structural key allocates one 'SBV.free' variable and caches+-- it; every later read of the same key returns the cached variable. So two+-- reads of the same slot (e.g. -- @proj #x .== proj #x@) share /one/ SBV variable: the solver knows -- they are equal, @x \/= x@ is unsat, and 'symSatExt''s by-name witness--- extraction is correct for repeated reads. The 'TApp1' \/ 'TApp2'+-- extraction is correct for ordinary repeated reads. Projection variables+-- are deliberately not extracted: the solver knows the scalar result but not+-- how to construct its consumer-owned base value. The 'TApp1' \/ 'TApp2' -- escape hatches stay per-occurrence fresh (their opaque functions -- have no 'Eq', so two applications cannot be recognized as equal); -- their values are not part of the extracted witness.@@ -431,9 +469,9 @@   SBV.Symbolic (SBV.SBV (SymRep r)) translateTermSym _env (TLit r) = pure (symLit r) translateTermSym env (TReg ix) =-  memoFree env ("reg/" <> indexName ix)+  memoFree env (RegVar (indexName ix)) translateTermSym env (TInpCtorField ic ix) =-  memoFree env ("inp/" <> icName ic <> "/" <> indexName ix)+  memoFree env (InpVar (icName ic) (indexName ix)) translateTermSym _env (TApp1 _f _t) = SBV.free "app1" translateTermSym _env (TApp2 _f _a _b) = SBV.free "app2" translateTermSym env (TArith op a b) = case discoverSymNum @r of@@ -446,7 +484,51 @@           OpSub -> (-)           OpMul -> (*)     pure (apply sa sb)+translateTermSym env (TFieldProj (witness :: FieldWitness projection) base) =+  memoFree env (projectionVarKey witness base) +projectionVarKey ::+  forall projection rs ci ifs.+  ( Typeable projection,+    Typeable (FieldOwner projection),+    Typeable (FieldResult projection)+  ) =>+  FieldWitness projection ->+  ProjBase rs ci ifs (FieldOwner projection) ->+  SymVarKey+projectionVarKey _ base =+  ProjectionVar+    ( case base of+        PBReg ix -> ProjectionReg (indexName ix) (indexPosition ix)+        PBInp ic ix ->+          ProjectionInp (icName ic) (indexName ix) (indexPosition ix)+    )+    (SomeTypeRep (typeRep @projection))+    (SomeTypeRep (typeRep @(FieldOwner projection)))+    (SomeTypeRep (typeRep @(FieldResult projection)))++-- | Bind one memoized projection variable to the concrete getter result for+-- a known owner. Pass @fieldWitnessGet witness owner@ as the concrete result.+-- This supplies the concrete-to-symbolic simulation used by agreement+-- properties: every concrete evaluation has a matching symbolic valuation.+-- The converse is intentionally not claimed. This function is not an inverse+-- for 'symSatExt', and projection variables are not extracted into or checked+-- for joint realizability as consumer-owned values.+constrainFieldProjection ::+  forall projection rs ci ifs.+  ( Typeable projection,+    Typeable (FieldOwner projection),+    Sym (FieldResult projection)+  ) =>+  SymEnv ->+  FieldWitness projection ->+  ProjBase rs ci ifs (FieldOwner projection) ->+  FieldResult projection ->+  SBV.Symbolic ()+constrainFieldProjection env witness base concrete = do+  symbolic <- memoFree env (projectionVarKey witness base)+  SBV.constrain (symbolic SBV..== symLit concrete)+ -- | Memoized symbolic-variable allocator (EP-42). Looks @name@ up in -- the env's 'seVarCache'. On a hit, recover the cached SBV variable — -- checking its representation type matches the requested one, which it@@ -457,19 +539,27 @@ memoFree ::   forall a.   (SBV.SymVal a) =>-  SymEnv -> String -> SBV.Symbolic (SBV.SBV a)-memoFree env name = do+  SymEnv -> SymVarKey -> SBV.Symbolic (SBV.SBV a)+memoFree env key = do   m <- liftIO (readIORef (seVarCache env))-  case Map.lookup name m of+  case Map.lookup key m of     Just (SomeSBV (v :: SBV.SBV b)) ->       case eqTypeRep (typeRep @a) (typeRep @b) of         Just HRefl -> pure v         Nothing ->           -- Unreachable: a name maps to exactly one representation type.-          error ("memoFree: type mismatch for cached variable " <> name)+          error ("memoFree: type mismatch for cached variable " <> show key)     Nothing -> do-      v <- SBV.free name-      liftIO (modifyIORef' (seVarCache env) (Map.insert name (SomeSBV v)))+      label <- case key of+        RegVar name -> pure ("reg/" <> name)+        InpVar ctorName fieldName ->+          pure ("inp/" <> ctorName <> "/" <> fieldName)+        ProjectionVar {} -> liftIO $ do+          ordinal <- readIORef (seProjectionOrdinal env)+          modifyIORef' (seProjectionOrdinal env) (+ 1)+          pure ("proj/" <> show ordinal)+      v <- SBV.free label+      liftIO (modifyIORef' (seVarCache env) (Map.insert key (SomeSBV v)))       pure v  -- | Recover the slot name an 'Index' points at by walking to the

@@ -3,6 +3,7 @@ import Data.Proxy (Proxy (..)) import Keiki.Composition import Keiki.Core+import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Fixtures.ComposeStateful import Keiki.Fixtures.CounterPipeline import Keiki.Profunctor (rmapCo)@@ -74,6 +75,99 @@       isFinal = const True     } +data ProjectionSourceCmd = ProjectionSourceCmd FieldProj.DocInfo+  deriving stock (Eq, Show)++type ProjectionSourceFields = '[ '("doc", FieldProj.DocInfo)]++projectionSourceCtor :: InCtor ProjectionSourceCmd ProjectionSourceFields+projectionSourceCtor =+  InCtor+    { icName = "ProjectionSourceCmd",+      icMatch = \(ProjectionSourceCmd doc) ->+        Just (RCons (Proxy @"doc") doc RNil),+      icBuild = \(RCons _ doc RNil) -> ProjectionSourceCmd doc+    }++data ProjectionMid = ProjectionMid FieldProj.DocInfo+  deriving stock (Eq, Show)++projectionMidCtor :: InCtor ProjectionMid '[ '("doc", FieldProj.DocInfo)]+projectionMidCtor =+  InCtor+    { icName = "ProjectionMid",+      icMatch = \(ProjectionMid doc) -> Just (RCons (Proxy @"doc") doc RNil),+      icBuild = \(RCons _ doc RNil) -> ProjectionMid doc+    }++projectionMidWire :: WireCtor ProjectionMid (FieldProj.DocInfo, ())+projectionMidWire =+  WireCtor+    { wcName = "ProjectionMid",+      wcMatch = \(ProjectionMid doc) -> Just (doc, ()),+      wcBuild = \(doc, ()) -> ProjectionMid doc+    }++data ProjectionVertex = ProjectionVertex+  deriving stock (Eq, Ord, Show, Enum, Bounded)++projectionSource ::+  Term '[] ProjectionSourceCmd ProjectionSourceFields FieldProj.DocInfo ->+  SymTransducer+    (HsPred '[] ProjectionSourceCmd)+    '[]+    ProjectionVertex+    ProjectionSourceCmd+    ProjectionMid+projectionSource ownerTerm =+  SymTransducer+    { edgesOut = \ProjectionVertex ->+        [ Edge+            { guard = matchInCtor projectionSourceCtor,+              update = UKeep,+              output =+                [ pack+                    projectionSourceCtor+                    projectionMidWire+                    (OFCons ownerTerm OFNil)+                ],+              target = ProjectionVertex,+              mode = Live+            }+        ],+      initial = ProjectionVertex,+      initialRegs = RNil,+      isFinal = const True+    }++projectionSink ::+  SymTransducer+    (HsPred '[] ProjectionMid)+    '[]+    ProjectionVertex+    ProjectionMid+    ()+projectionSink =+  SymTransducer+    { edgesOut = \ProjectionVertex ->+        [ Edge+            { guard =+                PAnd+                  (matchInCtor projectionMidCtor)+                  ( inpProj FieldProj.docHashW projectionMidCtor #doc+                      .== TLit "match"+                  ),+              update = UKeep,+              output = [],+              target = ProjectionVertex,+              mode = Live+            }+        ],+      initial = ProjectionVertex,+      initialRegs = RNil,+      isFinal = const True+    }+ spec :: Spec spec = do   describe "checkComposeAlignment" $ do@@ -118,3 +212,47 @@      it "walks every symbol in a multi-event source chain" $       checkComposeAlignment pairSource twoPhaseSink `shouldBe` []++  describe "typed field projection composition" $ do+    let matchingDoc = FieldProj.DocInfo "match" "title" []+        inputTerm = TInpCtorField projectionSourceCtor #doc+        passThrough = projectionSource inputTerm+        literalOwner = projectionSource (TLit matchingDoc)+        computedOwner = projectionSource (TApp1 id inputTerm)++    it "preserves a stable input-field owner through checked composition" $ do+      checkComposeAlignment passThrough projectionSink `shouldBe` []+      case composeChecked passThrough projectionSink of+        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 "keeps raw composition forward-correct but rejects a computed owner at the checked boundary" $ do+      let pipeline = compose computedOwner projectionSink+      opaqueGuardWarnings pipeline `shouldSatisfy` (not . null)+      case stepEither+        pipeline+        (initial pipeline, initialRegs pipeline)+        (ProjectionSourceCmd matchingDoc) of+        Left failure -> expectationFailure ("raw projected pipeline failed: " <> show failure)+        Right _ -> pure ()+      case composeChecked computedOwner projectionSink of+        Right _ -> expectationFailure "computed owner passed composeChecked"+        Left warnings ->+          warnings+            `shouldSatisfy` any+              ( \case+                  NonStructuralProjectionBoundary+                    { cawProjectionReason = "upstream computed output"+                    } -> True+                  _ -> False+              )

@@ -8,8 +8,14 @@ module Keiki.CompositionMultiEventSpec (spec) where  import Data.Proxy (Proxy (..))-import Keiki.Composition (Composite (..), compose)+import Keiki.Composition+  ( ComposeAlignmentWarning (..),+    Composite (..),+    compose,+    composeChecked,+  ) import Keiki.Core+import Keiki.FieldProjSpec qualified as FieldProj import Test.Hspec  -- * t1 ---------------------------------------------------------------------@@ -71,7 +77,7 @@  -- | t1's transducer: a single vertex Q with a self-loop edge that -- emits two mid-symbols ([MidA n, MidB n]) from one T1Trigger input.-data Q = Q deriving (Eq, Show, Bounded, Enum)+data Q = Q deriving (Eq, Ord, Show, Bounded, Enum)  t1 :: SymTransducer (HsPred '[] T1Cmd) '[] Q T1Cmd Mid t1 =@@ -137,7 +143,7 @@     }  -- | t2's vertex (single).-data Z = Z deriving (Eq, Show, Bounded, Enum)+data Z = Z deriving (Eq, Ord, Show, Bounded, Enum)  -- | t2's transducer: two edges from Z, one per mid-symbol. --   Z on MidA → Z / [EchoA payload]@@ -188,6 +194,119 @@       isFinal = const True     } +data PendingSourceCmd = PendingSourceCmd FieldProj.DocInfo+  deriving stock (Eq, Show)++pendingSourceCtor :: InCtor PendingSourceCmd '[ '("doc", FieldProj.DocInfo)]+pendingSourceCtor =+  InCtor+    { icName = "PendingSourceCmd",+      icMatch = \(PendingSourceCmd doc) -> Just (RCons (Proxy @"doc") doc RNil),+      icBuild = \(RCons _ doc RNil) -> PendingSourceCmd doc+    }++data PendingMid+  = PendingLoad FieldProj.DocInfo+  | PendingCheck+  deriving stock (Eq, Show)++pendingLoadCtor :: InCtor PendingMid '[ '("doc", FieldProj.DocInfo)]+pendingLoadCtor =+  InCtor+    { icName = "PendingLoad",+      icMatch = \case+        PendingLoad doc -> Just (RCons (Proxy @"doc") doc RNil)+        PendingCheck -> Nothing,+      icBuild = \(RCons _ doc RNil) -> PendingLoad doc+    }++pendingCheckCtor :: InCtor PendingMid '[]+pendingCheckCtor =+  InCtor+    { icName = "PendingCheck",+      icMatch = \case PendingCheck -> Just RNil; PendingLoad _ -> Nothing,+      icBuild = \RNil -> PendingCheck+    }++pendingLoadWire :: WireCtor PendingMid (FieldProj.DocInfo, ())+pendingLoadWire =+  WireCtor+    { wcName = "PendingLoad",+      wcMatch = \case PendingLoad doc -> Just (doc, ()); PendingCheck -> Nothing,+      wcBuild = \(doc, ()) -> PendingLoad doc+    }++pendingCheckWire :: WireCtor PendingMid ()+pendingCheckWire =+  WireCtor+    { wcName = "PendingCheck",+      wcMatch = \case PendingCheck -> Just (); PendingLoad _ -> Nothing,+      wcBuild = \() -> PendingCheck+    }++pendingSource ::+  SymTransducer (HsPred '[] PendingSourceCmd) '[] Q PendingSourceCmd PendingMid+pendingSource =+  SymTransducer+    { edgesOut = \Q ->+        [ Edge+            { guard = matchInCtor pendingSourceCtor,+              update = UKeep,+              output =+                [ pack+                    pendingSourceCtor+                    pendingLoadWire+                    (OFCons (TInpCtorField pendingSourceCtor #doc) OFNil),+                  pack pendingSourceCtor pendingCheckWire OFNil+                ],+              target = Q,+              mode = Live+            }+        ],+      initial = Q,+      initialRegs = RNil,+      isFinal = const True+    }++pendingSink ::+  SymTransducer+    (HsPred FieldProj.DocRegs PendingMid)+    FieldProj.DocRegs+    Z+    PendingMid+    ()+pendingSink =+  SymTransducer+    { edgesOut = \Z ->+        [ Edge+            { guard = matchInCtor pendingLoadCtor,+              update =+                USet+                  FieldProj.docN+                  (TApp1 id (TInpCtorField pendingLoadCtor #doc)),+              output = [],+              target = Z,+              mode = Live+            },+          Edge+            { guard =+                PAnd+                  (matchInCtor pendingCheckCtor)+                  ( regProj FieldProj.docHashW FieldProj.docIx+                      .== TLit "pending-match"+                  ),+              update = UKeep,+              output = [],+              target = Z,+              mode = Live+            }+        ],+      initial = Z,+      initialRegs =+        RCons (Proxy @"doc") FieldProj.initialDocInfo RNil,+      isFinal = const True+    }+ -- * Specs ------------------------------------------------------------------  spec :: Spec@@ -221,3 +340,29 @@             ( "expected Just (Composite Q Z, _), got "                 <> show (fmap (\(s, _) -> s) other)             )++  describe "projection through a multi-event pending write" $ do+    let matchingDoc = FieldProj.DocInfo "pending-match" "title" []++    it "raw composition preserves forward behavior and makes the loss auditable" $ do+      let pipeline = compose pendingSource pendingSink+      opaqueGuardWarnings pipeline `shouldSatisfy` (not . null)+      case stepEither+        pipeline+        (initial pipeline, initialRegs pipeline)+        (PendingSourceCmd matchingDoc) of+        Left failure -> expectationFailure ("pending-write pipeline failed: " <> show failure)+        Right _ -> pure ()++    it "composeChecked rejects the computed pending-write projection" $+      case composeChecked pendingSource pendingSink of+        Right _ -> expectationFailure "computed pending write passed composeChecked"+        Left warnings ->+          warnings+            `shouldSatisfy` any+              ( \case+                  NonStructuralProjectionBoundary+                    { cawProjectionReason = "pending write"+                    } -> True+                  _ -> False+              )

@@ -0,0 +1,419 @@+{-# LANGUAGE TypeFamilies #-}++module Keiki.FieldProjSpec where++import Data.Proxy (Proxy (..))+import Data.SBV qualified as SBV+import Data.Text (Text)+import Data.Text qualified as T+import Keiki.Core+import Keiki.Symbolic+  ( SymEnv (..),+    constrainFieldProjection,+    mkSymEnv,+    symIsBot,+    translatePred,+  )+import Test.Hspec+import Test.QuickCheck+  ( expectFailure,+    ioProperty,+    property,+  )+import Test.QuickCheck.Property (withMaxSuccess)++data DocInfo = DocInfo+  { diHash :: Text,+    diTitle :: Text,+    diNumbers :: [Int]+  }+  deriving stock (Eq, Show)++data DocContentHash++instance FieldProjection DocContentHash where+  type FieldName DocContentHash = "contentHash"+  type FieldOwner DocContentHash = DocInfo+  type FieldResult DocContentHash = Text+  fieldShapeId _ = "test.doc-info.v1"+  projectFieldValue _ = diHash++data DocTitle++instance FieldProjection DocTitle where+  type FieldName DocTitle = "title"+  type FieldOwner DocTitle = DocInfo+  type FieldResult DocTitle = Text+  fieldShapeId _ = "test.doc-info.v1"+  projectFieldValue _ = diTitle++data DocContentHashAlias++instance FieldProjection DocContentHashAlias where+  type FieldName DocContentHashAlias = "contentHash"+  type FieldOwner DocContentHashAlias = DocInfo+  type FieldResult DocContentHashAlias = Text+  fieldShapeId _ = "test.doc-info.v1"+  projectFieldValue _ = diHash++data DocNumbers++instance FieldProjection DocNumbers where+  type FieldName DocNumbers = "numbers"+  type FieldOwner DocNumbers = DocInfo+  type FieldResult DocNumbers = [Int]+  fieldShapeId _ = "test.doc-info.v1"+  projectFieldValue _ = diNumbers++data DocIdentity++instance FieldProjection DocIdentity where+  type FieldName DocIdentity = "self"+  type FieldOwner DocIdentity = DocInfo+  type FieldResult DocIdentity = DocInfo+  fieldShapeId _ = "test.doc-info.v1"+  projectFieldValue _ = id++data AdversarialHash++instance FieldProjection AdversarialHash where+  type FieldName AdversarialHash = "content/|\\hash"+  type FieldOwner AdversarialHash = DocInfo+  type FieldResult AdversarialHash = Text+  fieldShapeId _ = "shape/|\\doc"+  projectFieldValue _ = diHash++docHashW :: FieldWitness DocContentHash+docHashW = fieldWitness @DocContentHash++docTitleW :: FieldWitness DocTitle+docTitleW = fieldWitness @DocTitle++docHashAliasW :: FieldWitness DocContentHashAlias+docHashAliasW = fieldWitness @DocContentHashAlias++docNumbersW :: FieldWitness DocNumbers+docNumbersW = fieldWitness @DocNumbers++docIdentityW :: FieldWitness DocIdentity+docIdentityW = fieldWitness @DocIdentity++adversarialHashW :: FieldWitness AdversarialHash+adversarialHashW = fieldWitness @AdversarialHash++type DocRegs = '[ '("doc", DocInfo)]++docIx :: Index DocRegs DocInfo+docIx = #doc++docN :: IndexN "doc" DocRegs DocInfo+docN = IZ++data DocCmd = NewDoc DocInfo+  deriving stock (Eq, Show)++type NewDocFields = '[ '("doc", DocInfo)]++newDocCtor :: InCtor DocCmd NewDocFields+newDocCtor =+  InCtor+    { icName = "NewDoc",+      icMatch = \case+        NewDoc doc -> Just (RCons (Proxy @"doc") doc RNil),+      icBuild = \(RCons _ doc RNil) -> NewDoc doc+    }++data DocEvent = DocAccepted DocInfo+  deriving stock (Eq, Show)++docAcceptedWire :: WireCtor DocEvent (DocInfo, ())+docAcceptedWire =+  WireCtor+    { wcName = "DocAccepted",+      wcMatch = \case DocAccepted doc -> Just (doc, ()),+      wcBuild = \(doc, ()) -> DocAccepted doc+    }++data DocState = DocState+  deriving stock (Eq, Ord, Show, Enum, Bounded)++initialDocInfo :: DocInfo+initialDocInfo = DocInfo "old-hash" "old title" []++docProjectionTransducer ::+  SymTransducer (HsPred DocRegs DocCmd) DocRegs DocState DocCmd DocEvent+docProjectionTransducer =+  SymTransducer+    { edgesOut = \DocState ->+        [ Edge+            { guard =+                PAnd+                  (matchInCtor newDocCtor)+                  (regProj docHashW docIx ./= inpProj docHashW newDocCtor #doc),+              update = USet docN (TInpCtorField newDocCtor #doc),+              output =+                [ pack+                    newDocCtor+                    docAcceptedWire+                    (OFCons (TInpCtorField newDocCtor #doc) OFNil)+                ],+              target = DocState,+              mode = Live+            }+        ],+      initial = DocState,+      initialRegs = RCons (Proxy @"doc") initialDocInfo RNil,+      isFinal = const True+    }++inputProjectionTransducer ::+  SymTransducer (HsPred '[] DocCmd) '[] DocState DocCmd DocEvent+inputProjectionTransducer =+  SymTransducer+    { edgesOut = \DocState ->+        [ Edge+            { guard =+                PAnd+                  (matchInCtor newDocCtor)+                  (inpProj docHashW newDocCtor #doc .== TLit "new-hash"),+              update = UKeep,+              output =+                [ pack+                    newDocCtor+                    docAcceptedWire+                    (OFCons (TInpCtorField newDocCtor #doc) OFNil)+                ],+              target = DocState,+              mode = Live+            }+        ],+      initial = DocState,+      initialRegs = RNil,+      isFinal = const True+    }++data PairInts = PairInts Int Int+  deriving stock (Eq, Show)++data WrongFirst++instance FieldProjection WrongFirst where+  type FieldName WrongFirst = "first"+  type FieldOwner WrongFirst = PairInts+  type FieldResult WrongFirst = Int+  fieldShapeId _ = "test.pair-ints.v1"+  projectFieldValue _ (PairInts _ second) = second++wrongFirstW :: FieldWitness WrongFirst+wrongFirstW = fieldWitness @WrongFirst++data NumberOwner = NumberOwner Int Integer++data NumberAsInt++instance FieldProjection NumberAsInt where+  type FieldName NumberAsInt = "number"+  type FieldOwner NumberAsInt = NumberOwner+  type FieldResult NumberAsInt = Int+  fieldShapeId _ = "test.number-owner.v1"+  projectFieldValue _ (NumberOwner value _) = value++data NumberAsInteger++instance FieldProjection NumberAsInteger where+  type FieldName NumberAsInteger = "number"+  type FieldOwner NumberAsInteger = NumberOwner+  type FieldResult NumberAsInteger = Integer+  fieldShapeId _ = "test.number-owner.v1"+  projectFieldValue _ (NumberOwner _ value) = value++type NumberRegs = '[ '("numberOwner", NumberOwner)]++numberIntW :: FieldWitness NumberAsInt+numberIntW = fieldWitness @NumberAsInt++numberIntegerW :: FieldWitness NumberAsInteger+numberIntegerW = fieldWitness @NumberAsInteger++proveConcreteAgreement ::+  HsPred rs ci ->+  (SymEnv -> SBV.Symbolic ()) ->+  Bool ->+  IO Bool+proveConcreteAgreement predicate bindConcrete concrete = do+  result <- SBV.prove $ do+    env <- mkSymEnv+    translated <- translatePred env predicate+    bindConcrete env+    pure (translated SBV..<=> SBV.literal concrete)+  pure (not (SBV.modelExists result))++spec :: Spec+spec = do+  describe "concrete field projection" $ do+    let doc = DocInfo "hash-1" "title-1" [1, 2]+        regs = RCons (Proxy @"doc") doc RNil++    it "evaluates a register-owned field" $+      evalTerm (regProj docHashW docIx :: Term DocRegs DocCmd '[] Text) regs (NewDoc doc)+        `shouldBe` "hash-1"++    it "evaluates an input-owned field" $+      evalTerm+        (inpProj docHashW newDocCtor #doc :: Term '[] DocCmd NewDocFields Text)+        RNil+        (NewDoc doc)+        `shouldBe` "hash-1"++    it "keeps projection guards out of the opaque audit while TApp1 remains opaque" $ do+      opaqueGuardWarnings docProjectionTransducer `shouldBe` []+      let opaque =+            docProjectionTransducer+              { edgesOut = \DocState ->+                  [ Edge+                      { guard = PEq (TApp1 diHash (TReg docIx)) (TLit "old-hash"),+                        update = UKeep,+                        output = [],+                        target = DocState,+                        mode = Live+                      }+                  ]+              }+      opaqueGuardWarnings opaque `shouldSatisfy` (not . null)++  describe "path-keyed symbolic projection" $ do+    it "shares one variable for the same nominal projection and base" $+      symIsBot+        ( regProj docHashW docIx ./= regProj docHashW docIx ::+            HsPred DocRegs ()+        )+        `shouldBe` True++    it "keeps distinct fields of one owner independent" $+      symIsBot+        ( PAnd+            (regProj docHashW docIx .== TLit "left")+            (regProj docTitleW docIx .== TLit "right") ::+            HsPred DocRegs ()+        )+        `shouldBe` False++    it "keeps nominal tags independent even with identical diagnostics" $+      symIsBot+        ( PAnd+            (regProj docHashW docIx .== TLit "left")+            (regProj docHashAliasW docIx .== TLit "right") ::+            HsPred DocRegs ()+        )+        `shouldBe` False++    it "keeps Int and Integer results independent despite a shared SBV representation" $+      symIsBot+        ( PAnd+            (regProj numberIntW (#numberOwner :: Index NumberRegs NumberOwner) .== TLit 0)+            (regProj numberIntegerW (#numberOwner :: Index NumberRegs NumberOwner) .== TLit 1) ::+            HsPred NumberRegs ()+        )+        `shouldBe` False++    it "uses index position when duplicate diagnostic labels are constructed manually" $ do+      let first = ZIdx :: Index '[ '("doc", DocInfo), '("doc", DocInfo)] DocInfo+          second = SIdx ZIdx :: Index '[ '("doc", DocInfo), '("doc", DocInfo)] DocInfo+      symIsBot+        ( PAnd+            (regProj docHashW first .== TLit "left")+            (regProj docHashW second .== TLit "right") ::+            HsPred '[ '("doc", DocInfo), '("doc", DocInfo)] ()+        )+        `shouldBe` False++    it "keeps register and input bases distinct even when dotted paths coincide" $ do+      let registerBase = ZIdx :: Index '[ '("NewDoc.doc", DocInfo)] DocInfo+      symIsBot+        ( PAnd+            (regProj docHashW registerBase .== TLit "left")+            (inpProj docHashW newDocCtor #doc .== TLit "right") ::+            HsPred '[ '("NewDoc.doc", DocInfo)] DocCmd+        )+        `shouldBe` False++    it "never sends adversarial diagnostic strings to SBV labels" $+      let adversarialIx = ZIdx :: Index '[ '("doc/|\\owner", DocInfo)] DocInfo+       in symIsBot+            ( regProj adversarialHashW adversarialIx+                ./= regProj adversarialHashW adversarialIx ::+                HsPred '[ '("doc/|\\owner", DocInfo)] ()+            )+            `shouldBe` True++  describe "concrete-to-symbolic agreement" $ do+    it "agrees for register projections in both truth directions" $+      withMaxSuccess 25 $+        property $ \rawHash same ->+          let owner = DocInfo (T.pack rawHash) "title" []+              comparison = if same then diHash owner else diHash owner <> "#different"+              regs = RCons (Proxy @"doc") owner RNil+              predicate = regProj docHashW docIx .== TLit comparison+              concrete = evalPred predicate regs (NewDoc owner)+           in ioProperty $+                proveConcreteAgreement+                  predicate+                  (\env -> constrainFieldProjection env docHashW (PBReg docIx) (diHash owner))+                  concrete++    it "agrees for input projections in both truth directions" $+      withMaxSuccess 25 $+        property $ \rawHash same ->+          let owner = DocInfo (T.pack rawHash) "title" []+              comparison = if same then diHash owner else diHash owner <> "#different"+              input = NewDoc owner+              predicate =+                PAnd+                  (matchInCtor newDocCtor)+                  (inpProj docHashW newDocCtor #doc .== TLit comparison)+              concrete = evalPred predicate RNil input+           in ioProperty $+                proveConcreteAgreement+                  predicate+                  ( \env -> do+                      SBV.constrain (seInputCtor env SBV..== SBV.literal "NewDoc")+                      constrainFieldProjection+                        env+                        docHashW+                        (PBInp newDocCtor #doc)+                        (diHash owner)+                  )+                  concrete++  describe "instance law harness" $ do+    it "accepts the truthful generated-style witness" $+      property $ \rawHash rawTitle ->+        let owner = DocInfo (T.pack rawHash) (T.pack rawTitle) []+         in fieldWitnessAgrees docHashW diHash owner++    it "finds a deliberately wrong coherent instance" $+      expectFailure $+        property $ \value ->+          fieldWitnessAgrees+            wrongFirstW+            (\(PairInts first _) -> first)+            (PairInts value (value + 1))++  describe "validation and replay" $ do+    it "validates the projection-guarded transducer under default options" $+      validateTransducer defaultValidationOptions docProjectionTransducer+        `shouldBe` []++    it "replays a projection-selected event to the complete forward state" $ do+      let nextDoc = DocInfo "new-hash" "new title" [3]+      case stepEither+        docProjectionTransducer+        (initial docProjectionTransducer, initialRegs docProjectionTransducer)+        (NewDoc nextDoc) of+        Left failure -> expectationFailure ("forward step failed: " <> show failure)+        Right (forwardState, forwardRegs, events) ->+          case reconstituteEither docProjectionTransducer events of+            Left failure -> expectationFailure ("replay failed: " <> show failure)+            Right (replayState, replayRegs) -> do+              replayState `shouldBe` forwardState+              replayRegs ! docIx `shouldBe` forwardRegs ! docIx

@@ -12,6 +12,7 @@ import Data.Time.Clock (UTCTime (..), secondsToDiffTime) import GHC.Generics (Generic) import Keiki.Core+import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Fixtures.CounterPipeline import Keiki.Fixtures.EmailDelivery import Keiki.LawHelpers (emittedLog, runScript)@@ -38,6 +39,9 @@ router (ToEmail c) = Just c router OtherCmd = Nothing +newtype WrappedDocCmd = WrappedDocCmd {unwrapDocCmd :: FieldProj.DocCmd}+  deriving stock (Eq, Show)+ -- | A representative input we will fire through transducers. sampleEmailCmd :: EmailCmd sampleEmailCmd =@@ -128,6 +132,12 @@     it "preserves isSingleValuedSym" $ do       isSingleValuedSym (withSymPred (lmapCi unwrapCmd emailDelivery))         `shouldBe` True++    it "rehomes an input-based field projection without changing evaluation" $ do+      let mapped = lmapCi unwrapDocCmd FieldProj.inputProjectionTransducer+          doc = FieldProj.DocInfo "new-hash" "title" []+      omega mapped (initial mapped) (initialRegs mapped) (WrappedDocCmd (FieldProj.NewDoc doc))+        `shouldBe` [FieldProj.DocAccepted doc]    describe "rmapCo" $ do     it "post-composes the output through the supplied function" $ do

@@ -14,7 +14,10 @@     RegFile (..),     Term (..),     Update (..),+    inpProj,+    regProj,   )+import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Internal.Slots (IndexN (..)) import Keiki.Render.Pretty (prettyPred, prettyTerm, prettyUpdate) import Test.Hspec@@ -84,6 +87,16 @@     it "renders TArith mul as (a * b)" $       prettyTerm (TArith OpMul (TReg balanceIx) (TReg limitIx) :: Term Regs Cmd '[] Int)         `shouldBe` T.pack "(balance * limit)"+    it "renders a register field projection as a dotted path" $+      prettyTerm+        (regProj FieldProj.docHashW FieldProj.docIx :: Term FieldProj.DocRegs FieldProj.DocCmd '[] T.Text)+        `shouldBe` T.pack "doc.contentHash"+    it "renders an input field projection as ctor.owner.field" $+      prettyTerm+        ( inpProj FieldProj.docHashW FieldProj.newDocCtor #doc ::+            Term '[] FieldProj.DocCmd FieldProj.NewDocFields T.Text+        )+        `shouldBe` T.pack "NewDoc.doc.contentHash"    describe "prettyPred" $ do     it "renders PTop / PBot" $ do

@@ -29,6 +29,7 @@ import Data.Time.Calendar (fromGregorian) import Data.Time.Clock (UTCTime (..), secondsToDiffTime) import Keiki.Core+import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Fixtures.CounterPipeline import Keiki.Fixtures.EmailDelivery import Keiki.LawHelpers (emittedLog, runScript)@@ -86,6 +87,23 @@         SomeSymIdentity -> pure ()         SomeSymTransducer _ ->           expectationFailure "first' Cat.id should preserve the identity sentinel"++    it "rehomes an input-based field projection into the combined constructor" $ do+      let lifted =+            first' (someSymTransducer FieldProj.inputProjectionTransducer) ::+              SomeSymTransducer+                (FieldProj.DocCmd, RequestId)+                (FieldProj.DocEvent, RequestId)+          doc = FieldProj.DocInfo "new-hash" "title" []+          requestId = RequestId 7+      case lifted of+        SomeSymTransducer transducer ->+          omega+            transducer+            (initial transducer)+            (initialRegs transducer)+            (FieldProj.NewDoc doc, requestId)+            `shouldBe` [(FieldProj.DocAccepted doc, requestId)]    describe "second'" $ do     it "threads an unrelated RequestId through emailDelivery on the second slot" $ do

@@ -10,6 +10,7 @@ import Data.Time.Clock.POSIX (posixSecondsToUTCTime) import Data.Typeable (Typeable) import Data.Word (Word16, Word32, Word64, Word8)+import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Symbolic import Test.Hspec @@ -448,6 +449,25 @@      it "x == x stays satisfiable: symIsBot (PEq #amount #amount) is False (sanity)" $       symIsBot pEq `shouldBe` False++    it "a repeated typed field projection is one symbolic variable" $+      symIsBot+        ( FieldProj.docHashW+            `regProj` FieldProj.docIx+            ./= FieldProj.docHashW+            `regProj` FieldProj.docIx ::+            HsPred FieldProj.DocRegs ()+        )+        `shouldBe` True++    it "different typed fields of one mapped owner remain independent" $+      symIsBot+        ( PAnd+            (FieldProj.docHashW `regProj` FieldProj.docIx .== TLit "hash")+            (FieldProj.docTitleW `regProj` FieldProj.docIx .== TLit "title") ::+            HsPred FieldProj.DocRegs ()+        )+        `shouldBe` False      it "two edges PEq #amount 0 / PEq #amount 1 are single-valued" $       -- The single-valuedness conjunction is #amount == 0 ∧ #amount == 1,

@@ -4,6 +4,7 @@ import Data.Proxy (Proxy (..)) import Data.Word (Word8) import Keiki.Core+import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Symbolic (checkDeadEdgesSym, checkTransitionDeterminismSym) import Test.Hspec @@ -406,6 +407,149 @@      it "the audit is silent under defaultValidationOptions (backward compat)" $       validateTransducer defaultValidationOptions opaqueT `shouldBe` []++  describe "typed field projection validation" $ do+    let validOutput =+          [ pack+              FieldProj.newDocCtor+              FieldProj.docAcceptedWire+              (OFCons (TInpCtorField FieldProj.newDocCtor #doc) OFNil)+          ]+        projectionWarnings fixture =+          validateTransducer defaultValidationOptions fixture++    it "accepts supported Text equality and stays out of OpaqueGuard" $ do+      let warnings =+            validateTransducer+              defaultValidationOptions {warnOpaqueGuards = True}+              FieldProj.docProjectionTransducer+      warnings `shouldBe` []++    it "rejects a projection result outside the symbolic registry" $ do+      let fixture =+            FieldProj.docProjectionTransducer+              { edgesOut = \FieldProj.DocState ->+                  [ Edge+                      { guard =+                          PAnd+                            (matchInCtor FieldProj.newDocCtor)+                            ( regProj FieldProj.docNumbersW FieldProj.docIx+                                .== inpProj FieldProj.docNumbersW FieldProj.newDocCtor #doc+                            ),+                        update = UKeep,+                        output = validOutput,+                        target = FieldProj.DocState,+                        mode = Live+                      }+                  ]+              }+          isUnsupported ProjectionResultUnsupported {} = True+          isUnsupported _ = False+      projectionWarnings fixture `shouldSatisfy` any isUnsupported++    it "rejects ordering over a Text projection while equality remains supported" $ do+      let fixture =+            FieldProj.docProjectionTransducer+              { edgesOut = \FieldProj.DocState ->+                  [ Edge+                      { guard =+                          PAnd+                            (matchInCtor FieldProj.newDocCtor)+                            ( PCmp+                                CmpLt+                                (regProj FieldProj.docHashW FieldProj.docIx)+                                (TLit "z")+                            ),+                        update = UKeep,+                        output = validOutput,+                        target = FieldProj.DocState,+                        mode = Live+                      }+                  ]+              }+          isOrdering ProjectionOrderingUnsupported {} = True+          isOrdering _ = False+          isResult ProjectionResultUnsupported {} = True+          isResult _ = False+          warnings = projectionWarnings fixture+      warnings `shouldSatisfy` any isOrdering+      warnings `shouldSatisfy` (not . any isResult)++    it "rejects a projection in an update" $ do+      let fixture =+            FieldProj.docProjectionTransducer+              { edgesOut = \FieldProj.DocState ->+                  [ Edge+                      { guard = matchInCtor FieldProj.newDocCtor,+                        update =+                          USet+                            FieldProj.docN+                            (regProj FieldProj.docIdentityW FieldProj.docIx),+                        output = validOutput,+                        target = FieldProj.DocState,+                        mode = Live+                      }+                  ]+              }+          isUpdate ProjectionOutsideGuard {tvwProjectionLocation = "update"} = True+          isUpdate _ = False+      projectionWarnings fixture `shouldSatisfy` any isUpdate++    it "rejects an output projection and still reports its owner field hidden" $ do+      let projectedWire =+            WireCtor+              { wcName = "ProjectedHash",+                wcMatch = \case+                  FieldProj.DocAccepted doc -> Just (FieldProj.diHash doc, ()),+                wcBuild = \(hash, ()) ->+                  FieldProj.DocAccepted (FieldProj.DocInfo hash "" [])+              }+          fixture =+            FieldProj.docProjectionTransducer+              { edgesOut = \FieldProj.DocState ->+                  [ Edge+                      { guard = matchInCtor FieldProj.newDocCtor,+                        update = UKeep,+                        output =+                          [ pack+                              FieldProj.newDocCtor+                              projectedWire+                              ( OFCons+                                  (inpProj FieldProj.docHashW FieldProj.newDocCtor #doc)+                                  OFNil+                              )+                          ],+                        target = FieldProj.DocState,+                        mode = Live+                      }+                  ]+              }+          isOutput ProjectionOutsideGuard {tvwProjectionLocation = "output"} = True+          isOutput _ = False+          isHiddenDoc HiddenInput {tvwMissingSlots = missing} = "doc" `elem` missing+          isHiddenDoc _ = False+          warnings = projectionWarnings fixture+      warnings `shouldSatisfy` any isOutput+      warnings `shouldSatisfy` any isHiddenDoc++    it "requires PInCtor before an input-based projection read" $ do+      let fixture =+            FieldProj.docProjectionTransducer+              { edgesOut = \FieldProj.DocState ->+                  [ Edge+                      { guard =+                          inpProj FieldProj.docHashW FieldProj.newDocCtor #doc+                            .== TLit "hash",+                        update = UKeep,+                        output = validOutput,+                        target = FieldProj.DocState,+                        mode = Live+                      }+                  ]+              }+          isUnguarded UnguardedInputRead {} = True+          isUnguarded _ = False+      projectionWarnings fixture `shouldSatisfy` any isUnguarded    describe "checkTransitionDeterminismSym (z3-backed)" $ do     it "mutually-exclusive PInCtor guards yield no determinism warning" $

@@ -20,6 +20,7 @@ import Keiki.CoreHiddenInputsGSMSpec qualified import Keiki.CoreInFlightSpec qualified import Keiki.CoreSpec qualified+import Keiki.FieldProjSpec qualified import Keiki.Generics.THSpec qualified import Keiki.NoThunksSpec qualified import Keiki.OperatorsQualifiedSpec qualified@@ -59,6 +60,7 @@   describe "Keiki.Composition (N-ary codec, EP-48)" Keiki.CompositionNarySpec.spec   describe "Keiki.Composition (stateful, EP-74)" Keiki.CompositionStatefulSpec.spec   describe "Keiki.Core" Keiki.CoreSpec.spec+  describe "Keiki.FieldProj" Keiki.FieldProjSpec.spec   describe "Keiki.Core.stepEither (EP-55)" Keiki.StepEitherSpec.spec   describe "Keiki.Core.applyEvents (EP-20 M2)" Keiki.CoreApplyEventsSpec.spec   describe "Keiki.Core.InFlight / streaming (EP-19 M3)" Keiki.CoreInFlightSpec.spec