keiki 0.9.0.0 → 0.9.1.0
raw patch · 4 files changed
+302/−36 lines, 4 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- CHANGELOG.md +13/−0
- keiki.cabal +1/−1
- src/Keiki/Core.hs +67/−18
- test/Keiki/ValidationReplayAlignmentSpec.hs +221/−17
CHANGELOG.md view
@@ -9,6 +9,19 @@ ## [Unreleased] +## [0.9.1.0] — 2026-08-20++### Changed++- Default `inversionAmbiguityWarnings` now proves complementary standard+ `Bool` register guards disjoint by exhaustively evaluating their captured+ equality or ordering closures over Keiki's producer-owned exact domain+ `[False, True]`. Integral interval reasoning is unchanged; arbitrary+ `Bounded`/`Enum` carriers, unregistered equality anchors, `PNot`, and opaque+ guards remain conservative warnings. Public validation and runtime replay+ interfaces are unchanged.++ ## [0.9.0.0] — 2026-08-04 ### Added
keiki.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: keiki-version: 0.9.0.0+version: 0.9.1.0 synopsis: Pure core for symbolic-register transducer event sourcing. description: A Haskell library for the pure core of event sourcing, workflow
src/Keiki/Core.hs view
@@ -246,6 +246,7 @@ import Data.Int (Int32, Int64) import Data.Kind (Type) import Data.List (nub, partition, (\\))+import Data.List.NonEmpty (NonEmpty (..)) import Data.Proxy (Proxy (..)) import Data.Set qualified as Set import Data.Typeable (Typeable)@@ -2858,11 +2859,15 @@ -- The pass therefore has no false positives but can miss overlaps outside that -- fragment. The inversion component classifies head wires through trusted -- structural schemas (with the legacy name fallback for unavailable schemas),--- then suppresses a same-mode warning only when exact integral--- register-versus-literal conjuncts are jointly unsatisfiable. Opaque or--- unsupported conjuncts are dropped as weakening and can never supply proof;--- retained warnings name the first precision blocker in 'tvwDetail'. The--- dead-edge component is structural reachability plus a literal-'PBot' check.+-- then suppresses a same-mode warning only when supported exact+-- register-versus-literal conjuncts are jointly unsatisfiable. Integral+-- carriers use interval intersection; 'Bool' uses exhaustive evaluation over+-- Keiki's producer-owned @[False, True]@ domain. Arbitrary 'Bounded'/'Enum'+-- instances and equality literals on unregistered carriers supply no proof.+-- Opaque or unsupported conjuncts are dropped as weakening and can never+-- supply proof; retained warnings name the first precision blocker in+-- 'tvwDetail'. The dead-edge component is structural reachability plus a+-- literal-'PBot' check. -- For the exact, solver-backed answers use -- 'Keiki.Symbolic.checkTransitionDeterminismSym' and -- 'Keiki.Symbolic.checkDeadEdgesSym' directly, and use@@ -3341,15 +3346,19 @@ -- Head aliasing uses 'wireHeadsMayAliasForDefault': trusted structural schemas -- can prove constructor paths different, while unavailable evidence retains -- the legacy equal-'wcName' fallback. For a pair that may alias, the cheap pure--- proof recursively extracts exact integral @TReg relation literal@ conjuncts--- through 'PAnd'. Register variables are keyed by zero-based position and--- runtime type; labels are diagnostic only. Unsupported sibling conjuncts are--- dropped as weakening, so they cannot manufacture disjointness and a supported--- contradiction may still prove the full candidates disjoint. The warning is--- suppressed only when the combined necessary register conditions are--- definitely unsatisfiable. Satisfiable, unsupported, type-inconsistent, and--- otherwise unknown cases retain the warning, whose 'tvwDetail' names the first--- precision blocker.+-- proof recursively extracts exact @TReg relation literal@ conjuncts through+-- 'PAnd'. Integral carriers use exact interval intersection. Standard 'Bool'+-- uses exhaustive evaluation of the captured concrete 'Eq'/'Ord' closures over+-- Keiki's complete producer-owned @[False, True]@ domain. It does not trust an+-- arbitrary 'Bounded'/'Enum' enumeration or infer universal equality anchors+-- for unregistered consumer types. Register variables are keyed by zero-based+-- position and runtime type; labels are diagnostic only. Unsupported sibling+-- conjuncts are dropped as weakening, so they cannot manufacture disjointness+-- and a supported contradiction may still prove the full candidates disjoint.+-- The warning is suppressed only when the combined necessary register+-- conditions are definitely unsatisfiable. Satisfiable, unsupported,+-- type-inconsistent, and otherwise unknown cases retain the warning, whose+-- 'tvwDetail' names the first precision blocker. -- -- The proof intentionally does not enter 'POr' or 'PNot', model output fields, -- or infer disjointness from different reconstructed command constructors. It@@ -3541,6 +3550,9 @@ } deriving stock (Show) +-- | An extracted register comparison plus the exact concrete acceptance+-- closure from its source 'PEq' or 'PCmp' dictionary. Exact finite-domain+-- proofs evaluate this closure rather than reconstructing relation semantics. data RegisterComparison where RegisterComparison :: (Typeable r) =>@@ -3671,6 +3683,8 @@ } registerVariable _ = Nothing +-- | Retain a comparison only when Keiki owns exact carrier evidence: an+-- integral interval model or a closed producer-owned finite domain. knownRegisterComparison :: forall r. (Typeable r) =>@@ -3680,15 +3694,15 @@ (r -> Bool) -> RegisterConstraintExtraction knownRegisterComparison variable relation literalValue accepts =- case discoverIntegralDomain @r of- Nothing ->+ case (discoverIntegralDomain @r, discoverExactFiniteDomain @r) of+ (Nothing, Nothing) -> blockedRegisterConstraintExtraction ( "unsupported register carrier " <> show (typeRep @r) <> " at position " <> show variable.registerVariablePosition )- Just _ ->+ _ -> emptyRegisterConstraintExtraction { registerExtractionComparisons = [RegisterComparison variable relation literalValue accepts]@@ -3756,6 +3770,9 @@ Just HRefl -> Just (TypedPureComparison relation literalValue accepts) Nothing -> Nothing +-- | Decide one structurally aligned register group. Integral interval reasoning+-- remains first; exact finite carriers are exhausted; absent evidence is+-- unknown and cannot suppress a warning. registerComparisonGroupVerdict :: [RegisterComparison] -> RegisterConstraintVerdict registerComparisonGroupVerdict [] = RegisterConstraintsSatisfiable registerComparisonGroupVerdict@@ -3766,11 +3783,17 @@ let comparisons = TypedPureComparison relation literalValue accepts : alignedRest in case discoverIntegralDomain @r of- Nothing -> RegisterConstraintsUnknown Just domain | integralComparisonsSatisfiable domain comparisons -> RegisterConstraintsSatisfiable | otherwise -> RegisterConstraintsUnsatisfiable+ Nothing ->+ case discoverExactFiniteDomain @r of+ Nothing -> RegisterConstraintsUnknown+ Just domain+ | exactFiniteComparisonsSatisfiable domain comparisons ->+ RegisterConstraintsSatisfiable+ | otherwise -> RegisterConstraintsUnsatisfiable registerPositionTypeMismatch :: [RegisterComparison] -> Maybe String registerPositionTypeMismatch comparisons =@@ -4125,6 +4148,32 @@ integralMinimum :: Maybe Integer, integralMaximum :: Maybe Integer }++-- | A non-empty, producer-owned complete inhabitant list for one recognised+-- carrier. Completeness is established by the closed discovery function, never+-- by a consumer 'Enum' instance.+data ExactFiniteDomain r = ExactFiniteDomain+ { exactFiniteValues :: NonEmpty r+ }++-- | Discover exact finite evidence. The only admitted carrier is standard+-- 'Bool', whose two inhabitants are listed explicitly.+discoverExactFiniteDomain :: forall r. (Typeable r) => Maybe (ExactFiniteDomain r)+discoverExactFiniteDomain+ | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Bool) =+ Just (ExactFiniteDomain (False :| [True]))+ | otherwise = Nothing++-- | Whether at least one listed inhabitant satisfies every captured concrete+-- comparison closure. Returning 'False' proves unsatisfiability only because+-- @ExactFiniteDomain@ is complete.+exactFiniteComparisonsSatisfiable ::+ ExactFiniteDomain r -> [TypedPureComparison r] -> Bool+exactFiniteComparisonsSatisfiable domain comparisons =+ any satisfiesEveryComparison (exactFiniteValues domain)+ where+ satisfiesEveryComparison candidate =+ all (\comparison -> typedPureAccepts comparison candidate) comparisons discoverIntegralDomain :: forall r. (Typeable r) => Maybe (IntegralDomain r) discoverIntegralDomain
test/Keiki/ValidationReplayAlignmentSpec.hs view
@@ -3,7 +3,7 @@ module Keiki.ValidationReplayAlignmentSpec (spec) where import Control.Exception (evaluate)-import Control.Monad (foldM, forM_)+import Control.Monad (foldM, forM_, unless) import Data.Proxy (Proxy (..)) import Data.Text (Text) import Data.Time (UTCTime (..), fromGregorian, secondsToDiffTime)@@ -352,39 +352,144 @@ ) ] -type UnsupportedCarrierRegs = '[ '("enabled", Bool)]+type BoolRegisterRegs = '[ '("enabled", Bool)] -unsupportedCarrierFixture ::+boolRegisterTerm :: Term BoolRegisterRegs RegisterReplayCmd ifs Bool+boolRegisterTerm = TReg (#enabled :: Index BoolRegisterRegs Bool)++boolRegisterRegs :: Bool -> RegFile BoolRegisterRegs+boolRegisterRegs enabled = RCons (Proxy @"enabled") enabled RNil++boolRegisterFixture ::+ Bool ->+ EdgeMode ->+ HsPred BoolRegisterRegs RegisterReplayCmd ->+ HsPred BoolRegisterRegs RegisterReplayCmd -> SymTransducer- (HsPred UnsupportedCarrierRegs RegisterReplayCmd)- UnsupportedCarrierRegs+ (HsPred BoolRegisterRegs RegisterReplayCmd)+ BoolRegisterRegs Bool RegisterReplayCmd RegisterReplayEvent-unsupportedCarrierFixture =+boolRegisterFixture initialEnabled edgeMode leftCondition rightCondition = SymTransducer { edgesOut = \case False ->- [ unsupportedEdge inCompleteNonFinal True,- unsupportedEdge inCompleteFinal False+ [ boolRegisterEdge leftCondition,+ boolRegisterEdge rightCondition ] True -> [], initial = False,- initialRegs = RCons (Proxy @"enabled") True RNil,+ initialRegs = boolRegisterRegs initialEnabled, isFinal = id } where- unsupportedEdge inputCtor expected =+ boolRegisterEdge condition = Edge { guard = PAnd- (PInCtor inputCtor)+ (PInCtor inCompleteNonFinal)+ condition,+ update = UKeep,+ output = [registerReplayOutput inCompleteNonFinal],+ target = True,+ mode = edgeMode+ }++complementaryBoolFixture ::+ Bool ->+ EdgeMode ->+ SymTransducer+ (HsPred BoolRegisterRegs RegisterReplayCmd)+ BoolRegisterRegs+ Bool+ RegisterReplayCmd+ RegisterReplayEvent+complementaryBoolFixture initialEnabled edgeMode =+ boolRegisterFixture+ initialEnabled+ edgeMode+ (PEq boolRegisterTerm (TLit True))+ (PEq boolRegisterTerm (TLit False))++data BoolRegisterAtom = BoolRegisterAtom+ { boolAtomLabel :: String,+ boolAtomPredicate :: HsPred BoolRegisterRegs RegisterReplayCmd+ }++boolRegisterAtoms :: [BoolRegisterAtom]+boolRegisterAtoms =+ [ BoolRegisterAtom "enabled == False" (PEq boolRegisterTerm (TLit False)),+ BoolRegisterAtom "enabled == True" (PEq boolRegisterTerm (TLit True)),+ BoolRegisterAtom "enabled < False" (PCmp CmpLt boolRegisterTerm (TLit False)),+ BoolRegisterAtom "enabled < True" (PCmp CmpLt boolRegisterTerm (TLit True)),+ BoolRegisterAtom "enabled <= False" (PCmp CmpLe boolRegisterTerm (TLit False)),+ BoolRegisterAtom "enabled <= True" (PCmp CmpLe boolRegisterTerm (TLit True)),+ BoolRegisterAtom "enabled > False" (PCmp CmpGt boolRegisterTerm (TLit False)),+ BoolRegisterAtom "enabled > True" (PCmp CmpGt boolRegisterTerm (TLit True)),+ BoolRegisterAtom "enabled >= False" (PCmp CmpGe boolRegisterTerm (TLit False)),+ BoolRegisterAtom "enabled >= True" (PCmp CmpGe boolRegisterTerm (TLit True))+ ]++boolAtomsShareWitness :: BoolRegisterAtom -> BoolRegisterAtom -> Bool+boolAtomsShareWitness leftAtom rightAtom =+ any satisfiesBoth [False, True]+ where+ command = CompleteNonFinal (ReplayCompletionData 7)+ satisfiesBoth enabled =+ models (boolAtomPredicate leftAtom) (boolRegisterRegs enabled, command)+ && models (boolAtomPredicate rightAtom) (boolRegisterRegs enabled, command)++boolTopControlFixture ::+ SymTransducer+ (HsPred BoolRegisterRegs RegisterReplayCmd)+ BoolRegisterRegs+ Bool+ RegisterReplayCmd+ RegisterReplayEvent+boolTopControlFixture =+ boolRegisterFixture+ True+ Live+ (PEq boolRegisterTerm (TLit True))+ PTop++data UnregisteredFlag = UnregisteredOff | UnregisteredOn+ deriving stock (Eq, Ord, Show)++type UnregisteredCarrierRegs = '[ '("flag", UnregisteredFlag)]++unregisteredCarrierFixture ::+ SymTransducer+ (HsPred UnregisteredCarrierRegs RegisterReplayCmd)+ UnregisteredCarrierRegs+ Bool+ RegisterReplayCmd+ RegisterReplayEvent+unregisteredCarrierFixture =+ SymTransducer+ { edgesOut = \case+ False ->+ [ unregisteredEdge UnregisteredOff,+ unregisteredEdge UnregisteredOn+ ]+ True -> [],+ initial = False,+ initialRegs = RCons (Proxy @"flag") UnregisteredOff RNil,+ isFinal = id+ }+ where+ unregisteredEdge expected =+ Edge+ { guard =+ PAnd+ (PInCtor inCompleteNonFinal) ( PEq- (TReg (#enabled :: Index UnsupportedCarrierRegs Bool))+ (TReg (#flag :: Index UnregisteredCarrierRegs UnregisteredFlag)) (TLit expected) ), update = UKeep,- output = [registerReplayOutput inputCtor],+ output = [registerReplayOutput inCompleteNonFinal], target = True, mode = Live }@@ -793,12 +898,111 @@ [InversionAmbiguity {tvwDetail = detail}] -> detail `shouldContain` "TApp1" other -> expectationFailure ("expected one opaque-only warning, got " <> show other) - it "names an unsupported register carrier and fails conservatively" $- case inversionAmbiguityWarnings unsupportedCarrierFixture of+ it "suppresses complementary same-command Bool guards in default validation" $ do+ let transducer = complementaryBoolFixture True Live+ inversionAmbiguityWarnings transducer `shouldBe` []+ validateTransducer defaultValidationOptions transducer `shouldBe` []++ it "preserves forward/replay agreement for both complementary Bool register values" $ do+ forM_ [False, True] $ \initialEnabled -> do+ let transducer = complementaryBoolFixture initialEnabled Live+ command = CompleteNonFinal (ReplayCompletionData 7)+ case runCommands transducer [command] of+ Just (forwardVertex, forwardRegs, emitted) -> do+ emitted `shouldBe` [StepCompleted (ReplayCompletionData 7)]+ case reconstitute transducer emitted of+ Just (replayVertex, replayRegs) -> do+ replayVertex `shouldBe` forwardVertex+ replayRegs ! (#enabled :: Index BoolRegisterRegs Bool)+ `shouldBe` (forwardRegs ! (#enabled :: Index BoolRegisterRegs Bool))+ Nothing -> expectationFailure "complementary-Bool fixture did not replay"+ Nothing -> expectationFailure "complementary-Bool fixture did not step"++ it "suppresses flag < True versus flag == True" $+ inversionAmbiguityWarnings+ ( boolRegisterFixture+ False+ Live+ (PCmp CmpLt boolRegisterTerm (TLit True))+ (PEq boolRegisterTerm (TLit True))+ )+ `shouldBe` []++ it "retains flag <= True versus flag == True" $+ case inversionAmbiguityWarnings+ ( boolRegisterFixture+ True+ Live+ (PCmp CmpLe boolRegisterTerm (TLit True))+ (PEq boolRegisterTerm (TLit True))+ ) of+ [InversionAmbiguity {}] -> pure ()+ other -> expectationFailure ("expected one inclusive-ordering warning, got " <> show other)++ it "agrees with all concrete Bool relation pairs across modes, values, and observed events" $ do+ forM_ boolRegisterAtoms $ \leftAtom ->+ forM_ boolRegisterAtoms $ \rightAtom -> do+ let sharedWitnessExists = boolAtomsShareWitness leftAtom rightAtom+ pairLabel = boolAtomLabel leftAtom <> " / " <> boolAtomLabel rightAtom+ forM_ [Live, ReplayOnly] $ \candidateMode -> do+ let transducer =+ boolRegisterFixture+ False+ candidateMode+ (boolAtomPredicate leftAtom)+ (boolAtomPredicate rightAtom)+ warningSuppressed = null (inversionAmbiguityWarnings transducer)+ unless (warningSuppressed == not sharedWitnessExists) $+ expectationFailure+ ( "warning/concrete disagreement for "+ <> pairLabel+ <> " in "+ <> show candidateMode+ )+ unless sharedWitnessExists $+ forM_ [False, True] $ \registerValue ->+ forM_ [-2 .. 2] $ \observedId ->+ concreteReplayCandidateCount+ candidateMode+ transducer+ False+ (boolRegisterRegs registerValue)+ (StepCompleted (ReplayCompletionData observedId))+ `shouldSatisfy` (<= 1)++ it "keeps Bool inequality negation unsupported unless a sibling contradiction proves disjointness" $ do+ let negatedEquality = boolRegisterTerm ./= TLit True+ blockedFixture = boolRegisterFixture True Live negatedEquality negatedEquality+ case inversionAmbiguityWarnings blockedFixture of+ [InversionAmbiguity {tvwDetail = detail}] -> detail `shouldContain` "PNot"+ other -> expectationFailure ("expected one negation warning, got " <> show other)++ let contradictedFixture =+ boolRegisterFixture+ True+ Live+ (PAnd negatedEquality (PEq boolRegisterTerm (TLit True)))+ (PAnd negatedEquality (PEq boolRegisterTerm (TLit False)))+ inversionAmbiguityWarnings contradictedFixture `shouldBe` []++ it "retains True versus PTop and exhibits two concrete replay candidates" $ do+ case inversionAmbiguityWarnings boolTopControlFixture of+ [InversionAmbiguity {}] -> pure ()+ other -> expectationFailure ("expected one Bool/PTop warning, got " <> show other)+ concreteReplayCandidateCount+ Live+ boolTopControlFixture+ False+ (boolRegisterRegs True)+ (StepCompleted (ReplayCompletionData 7))+ `shouldBe` 2++ it "names an unregistered non-integral carrier and fails conservatively" $+ case inversionAmbiguityWarnings unregisteredCarrierFixture of [InversionAmbiguity {tvwDetail = detail}] -> do detail `shouldContain` "unsupported register carrier"- detail `shouldContain` "Bool"- other -> expectationFailure ("expected one unsupported-carrier warning, got " <> show other)+ detail `shouldContain` "UnregisteredFlag"+ other -> expectationFailure ("expected one unregistered-carrier warning, got " <> show other) it "retains every unsupported guard shape unless a supported sibling proves disjointness" $ do forM_ unsupportedRegisterConditions $ \(label, expectedBlocker, condition) -> do