diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/keiki.cabal b/keiki.cabal --- a/keiki.cabal +++ b/keiki.cabal @@ -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 diff --git a/src/Keiki/Composition.hs b/src/Keiki/Composition.hs --- a/src/Keiki/Composition.hs +++ b/src/Keiki/Composition.hs @@ -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. diff --git a/src/Keiki/Core.hs b/src/Keiki/Core.hs --- a/src/Keiki/Core.hs +++ b/src/Keiki/Core.hs @@ -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 = [] diff --git a/src/Keiki/Internal/SymbolicTypes.hs b/src/Keiki/Internal/SymbolicTypes.hs new file mode 100644 --- /dev/null +++ b/src/Keiki/Internal/SymbolicTypes.hs @@ -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 diff --git a/src/Keiki/Profunctor.hs b/src/Keiki/Profunctor.hs --- a/src/Keiki/Profunctor.hs +++ b/src/Keiki/Profunctor.hs @@ -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 ------------------------------------------------------------- diff --git a/src/Keiki/Render/Pretty.hs b/src/Keiki/Render/Pretty.hs --- a/src/Keiki/Render/Pretty.hs +++ b/src/Keiki/Render/Pretty.hs @@ -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 diff --git a/src/Keiki/Symbolic.hs b/src/Keiki/Symbolic.hs --- a/src/Keiki/Symbolic.hs +++ b/src/Keiki/Symbolic.hs @@ -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/\"@, --- 'TInpCtorField' allocates @"inp/\/\"@). 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//"@ — 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/"@, 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 diff --git a/test/Keiki/CompositionAlignmentSpec.hs b/test/Keiki/CompositionAlignmentSpec.hs --- a/test/Keiki/CompositionAlignmentSpec.hs +++ b/test/Keiki/CompositionAlignmentSpec.hs @@ -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 + ) diff --git a/test/Keiki/CompositionMultiEventSpec.hs b/test/Keiki/CompositionMultiEventSpec.hs --- a/test/Keiki/CompositionMultiEventSpec.hs +++ b/test/Keiki/CompositionMultiEventSpec.hs @@ -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 + ) diff --git a/test/Keiki/FieldProjSpec.hs b/test/Keiki/FieldProjSpec.hs new file mode 100644 --- /dev/null +++ b/test/Keiki/FieldProjSpec.hs @@ -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 diff --git a/test/Keiki/ProfunctorSpec.hs b/test/Keiki/ProfunctorSpec.hs --- a/test/Keiki/ProfunctorSpec.hs +++ b/test/Keiki/ProfunctorSpec.hs @@ -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 diff --git a/test/Keiki/Render/PrettySpec.hs b/test/Keiki/Render/PrettySpec.hs --- a/test/Keiki/Render/PrettySpec.hs +++ b/test/Keiki/Render/PrettySpec.hs @@ -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 diff --git a/test/Keiki/StrongSpec.hs b/test/Keiki/StrongSpec.hs --- a/test/Keiki/StrongSpec.hs +++ b/test/Keiki/StrongSpec.hs @@ -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 diff --git a/test/Keiki/SymbolicSpec.hs b/test/Keiki/SymbolicSpec.hs --- a/test/Keiki/SymbolicSpec.hs +++ b/test/Keiki/SymbolicSpec.hs @@ -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, diff --git a/test/Keiki/ValidationSpec.hs b/test/Keiki/ValidationSpec.hs --- a/test/Keiki/ValidationSpec.hs +++ b/test/Keiki/ValidationSpec.hs @@ -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" $ diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -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