diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 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.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 diff --git a/src/Keiki/Core.hs b/src/Keiki/Core.hs --- a/src/Keiki/Core.hs +++ b/src/Keiki/Core.hs @@ -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 diff --git a/test/Keiki/ValidationReplayAlignmentSpec.hs b/test/Keiki/ValidationReplayAlignmentSpec.hs --- a/test/Keiki/ValidationReplayAlignmentSpec.hs +++ b/test/Keiki/ValidationReplayAlignmentSpec.hs @@ -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