keiki 0.4.0.0 → 0.5.0.0

raw patch · 9 files changed

+260/−46 lines, 9 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +29/−0
• keiki.cabal +1/−1
• src/Keiki/Core.hs +39/−26
• src/Keiki/Internal/SymbolicTypes.hs +3/−0
• src/Keiki/Shape.hs +4/−0
• src/Keiki/Symbolic.hs +47/−19
• test/Keiki/ShapeSpec.hs +6/−0
• test/Keiki/SymbolicSpec.hs +39/−0
• test/Keiki/ValidationSpec.hs +92/−0

@@ -9,6 +9,35 @@ ## [Unreleased]  +## [0.5.0.0] — 2026-07-31++### Added++- `Natural` now has a pinned `CanonicalTypeName` and belongs to the curated+  symbolic equality/ordering registry. Its unbounded integer representation is+  constrained non-negative whenever Keiki allocates a symbolic variable.+- `Sym.constrainSymDomain` lets refined scalar instances state the validity+  invariant for their solver representation. `symFree`, structural register+  and input reads, field projections, and opaque term fallbacks all apply it.++### Changed++- `Natural` is deliberately absent from the symbolic arithmetic registry.+  Haskell subtraction on `Natural` throws `Underflow` when its mathematical+  result would be negative, whereas ordinary SMT integer subtraction returns+  that negative value.+- The opt-in opaque-guard audit now reports `TArith` whose carrier is absent+  from the symbolic numeric registry, including `Natural` arithmetic.+- The fast pure overlap validator treats `Natural` as the exact integral+  interval `[0, infinity)`, so it can find non-literal interior witnesses.+- The `OpaqueGuard` warning detail no longer names `TApp` specifically, since+  the audit now covers unsupported `TArith` carriers too. Consumers asserting+  on the exact message text will need to update.+- PVP major bump: the `Sym` class definition gained `constrainSymDomain`. The+  method has a default, so existing hand-written instances continue to compile+  unchanged.++ ## [0.4.0.0] — 2026-07-28  ### Added

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

@@ -220,8 +220,10 @@ import Keiki.Internal.SymbolicTypes   ( discoverSymbolicType,     symbolicTypeSupportsEquality,+    symbolicTypeSupportsNumeric,     symbolicTypeSupportsOrdering,   )+import Numeric.Natural (Natural) import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))  -- | A register slot is a label paired with the type of its value.@@ -2049,13 +2051,12 @@       { tvwEdge :: EdgeRef s,         tvwDetail :: String       }-  | -- | An edge whose guard contains an opaque 'TApp' term. The symbolic-    --       single-valuedness and dead-edge analyses translate such a term to an-    --       unconstrained free variable ('Keiki.Symbolic.translateTermSym' emits-    --       @SBV.free "app1"@), so they cannot see through the guard and silently-    --       under-verify it. Most often this is a collection-content condition-    --       (membership, "all resolved", size) lifted through a closure because the-    --       structural predicate language has no node for it; see the user guide and+  | -- | An edge whose guard contains a term the symbolic translator must make+    --       opaque. This includes 'TApp' closures and 'TArith' at a carrier outside+    --       the symbolic numeric registry (for example 'Natural'). The solver uses+    --       a fresh domain-valid variable for such a term, so the result remains+    --       sound but loses precision. Most opaque guards are collection-content+    --       conditions lifted through a closure; see the user guide and     --       @docs\/plans\/60-first-class-collection-registers-design-gated.md@ for the     --       options. Advisory, not a soundness error: opt in via 'warnOpaqueGuards'.     OpaqueGuard@@ -2103,9 +2104,9 @@     -- | run the (structural) dead-edge check     checkReachability :: Bool,     -- | run the opaque-guard audit (opt-in; default off). Flags edges whose-    --     guard branches on an opaque 'TApp' term the symbolic analyses cannot-    --     see through. Off by default so 'defaultValidationOptions' keeps its-    --     meaning for existing consumers.+    --     guard branches on a 'TApp' term or unsupported symbolic 'TArith'+    --     carrier the analyses cannot see through. Off by default so+    --     'defaultValidationOptions' keeps its meaning for existing consumers.     warnOpaqueGuards :: Bool,     -- | require the first emitted event to recover every command field used     --     by replay@@ -2242,17 +2243,27 @@  -- ** Opaque-guard diagnostics --- | Does the term contain an opaque 'TApp1'\/'TApp2' anywhere? Mirrors the--- structural recursion of 'termReadsInput'; 'TArith' is transparent, so it--- recurses into its operands rather than counting as opaque.-termHasOpaqueApp :: Term rs ci ifs r -> Bool-termHasOpaqueApp (TLit _) = False-termHasOpaqueApp (TReg _) = False-termHasOpaqueApp (TInpCtorField _ _) = False-termHasOpaqueApp (TApp1 _ _) = True-termHasOpaqueApp (TApp2 _ _ _) = True-termHasOpaqueApp (TArith _ a b) = termHasOpaqueApp a || termHasOpaqueApp b-termHasOpaqueApp TFieldProj {} = False+-- | Does the term contain a node that becomes an opaque symbolic variable?+-- 'TApp1'\/'TApp2' are always opaque. 'TArith' is structural only when its+-- carrier belongs to the symbolic numeric registry; otherwise the translator+-- deliberately falls back to a fresh domain-valid value.+termHasOpaqueFallback :: forall rs ci ifs r. Term rs ci ifs r -> Bool+termHasOpaqueFallback (TLit _) = False+termHasOpaqueFallback (TReg _) = False+termHasOpaqueFallback (TInpCtorField _ _) = False+termHasOpaqueFallback (TApp1 _ _) = True+termHasOpaqueFallback (TApp2 _ _ _) = True+termHasOpaqueFallback (TArith _ a b) =+  not carrierSupportsNumeric+    || termHasOpaqueFallback a+    || termHasOpaqueFallback b+  where+    carrierSupportsNumeric =+      maybe+        False+        symbolicTypeSupportsNumeric+        (discoverSymbolicType @r)+termHasOpaqueFallback 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),@@ -2263,15 +2274,15 @@ predHasOpaqueTerm (PAnd p q) = predHasOpaqueTerm p || predHasOpaqueTerm q predHasOpaqueTerm (POr p q) = predHasOpaqueTerm p || predHasOpaqueTerm q predHasOpaqueTerm (PNot p) = predHasOpaqueTerm p-predHasOpaqueTerm (PEq a b) = termHasOpaqueApp a || termHasOpaqueApp b+predHasOpaqueTerm (PEq a b) = termHasOpaqueFallback a || termHasOpaqueFallback b predHasOpaqueTerm (PInCtor _) = False predHasOpaqueTerm PLeftArm = False predHasOpaqueTerm PRightArm = False-predHasOpaqueTerm (PCmp _ a b) = termHasOpaqueApp a || termHasOpaqueApp b+predHasOpaqueTerm (PCmp _ a b) = termHasOpaqueFallback a || termHasOpaqueFallback b  -- | The opt-in opaque-guard audit (run by 'validateTransducer' only when -- 'warnOpaqueGuards' is set). For every edge whose guard contains an opaque--- 'TApp' term, emit an 'OpaqueGuard' warning locating the edge by its typed+-- term fallback, emit an 'OpaqueGuard' warning locating the edge by its typed -- 'EdgeRef'. Specialised to the 'HsPred' carrier because it walks the predicate -- AST, exactly as 'validateTransducer' is. opaqueGuardWarnings ::@@ -2282,8 +2293,8 @@   [ OpaqueGuard       { tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},         tvwDetail =-          "guard contains an opaque TApp term the symbolic analyses cannot "-            ++ "see through; its single-valuedness was not verified"+          "guard contains a term the symbolic analyses translate opaquely; "+            ++ "its single-valuedness was not verified"       }   | s <- [minBound .. maxBound],     (n, e) <- zip [(0 :: Int) ..] (edgesOut t s),@@ -3004,6 +3015,8 @@ discoverIntegralDomain   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Integer) =       Just (IntegralDomain id Nothing Nothing)+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Natural) =+      Just (IntegralDomain toInteger (Just 0) Nothing)   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int) =       Just (boundedIntegralDomain @Int)   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word8) =

@@ -20,6 +20,7 @@ import Data.Time (UTCTime) import Data.Typeable (Typeable) import Data.Word (Word16, Word32, Word64, Word8)+import Numeric.Natural (Natural) import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))  -- | Evidence that a type belongs to Keiki's closed symbolic registry.@@ -27,6 +28,7 @@   SymbolicBool :: SymbolicType Bool   SymbolicInt :: SymbolicType Int   SymbolicInteger :: SymbolicType Integer+  SymbolicNatural :: SymbolicType Natural   SymbolicText :: SymbolicType Text   SymbolicUTCTime :: SymbolicType UTCTime   SymbolicWord64 :: SymbolicType Word64@@ -42,6 +44,7 @@   | 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 @Natural) = Just SymbolicNatural   | 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

@@ -63,6 +63,7 @@ import GHC.Generics qualified as G import GHC.TypeLits (KnownSymbol, symbolVal) import Keiki.Core (Slot)+import Numeric.Natural (Natural) import Type.Reflection   ( SomeTypeRep (..),     TypeRep,@@ -123,6 +124,9 @@  instance CanonicalTypeName Integer where   canonicalTypeName _ = T.pack "Integer"++instance CanonicalTypeName Natural where+  canonicalTypeName _ = T.pack "Natural"  instance CanonicalTypeName Word where   canonicalTypeName _ = T.pack "Word"

@@ -18,7 +18,7 @@ -- Milestones implemented in this revision (through M5 of EP-2): -- --   * The 'Sym' typeclass and instances for 'Bool', 'Int', 'Integer',---     'Text', 'UTCTime', and the fixed-width integers 'Word8' \/+--     'Natural', 'Text', 'UTCTime', and the fixed-width integers 'Word8' \/ --     'Word16' \/ 'Word32' \/ 'Word64' \/ 'Int32' \/ 'Int64' (the --     last group added by EP-41 so money and count registers are --     solver-visible).@@ -112,6 +112,7 @@   ( SymbolicType (..),     discoverSymbolicType,   )+import Numeric.Natural (Natural) import System.IO.Unsafe (unsafePerformIO) import Type.Reflection (SomeTypeRep (..), eqTypeRep, typeRep, type (:~~:) (HRefl)) @@ -137,6 +138,12 @@   fromSym :: SymRep a -> a   symDefault :: a +  -- | Restrict a symbolic representation to values that denote a real @a@.+  -- Most carriers use their whole SBV domain. Refined carriers such as+  -- 'Natural' add constraints whenever Keiki allocates a symbolic variable.+  constrainSymDomain :: SBV.SBV (SymRep a) -> SBV.Symbolic ()+  constrainSymDomain _ = pure ()+ instance Sym Bool where   type SymRep Bool = Bool   toSym = id@@ -149,6 +156,19 @@   fromSym = id   symDefault = 0 +-- | Arbitrary-precision non-negative integers. The representation stays an+-- unbounded SMT integer, while every allocated variable is constrained to the+-- actual 'Natural' domain. Numeric arithmetic is deliberately not registered:+-- Haskell 'Natural' subtraction throws @Underflow@ when its mathematical result+-- would be negative, while ordinary SMT integer subtraction returns that negative+-- integer. Treating the operations as identical would not preserve concrete behavior.+instance Sym Natural where+  type SymRep Natural = Integer+  toSym = fromIntegral+  fromSym = fromInteger+  symDefault = 0+  constrainSymDomain value = SBV.constrain (value SBV..>= 0)+ -- | Encoded as 'Integer'. SBV does not provide an 'SInt'-of-arbitrary- -- size; using 'Integer' means machine-width 'Int' wraparound is not modeled. -- Guards whose truth depends on 'Int' overflow should use an explicit@@ -234,7 +254,7 @@  -- | Try to discover a 'Sym' instance for @r@ at runtime. Returns -- @Just SymDict@ for any of the curated supported types--- ('Bool', 'Int', 'Integer', 'Text', 'UTCTime', and the fixed-width+-- ('Bool', 'Int', 'Integer', 'Natural', 'Text', 'UTCTime', and the fixed-width -- integers 'Word8' \/ 'Word16' \/ 'Word32' \/ 'Word64' \/ 'Int32' \/ -- 'Int64'); 'Nothing' otherwise. The translator uses this to route -- 'PEq' over arbitrary types: a 'Sym' hit translates to '(.==)' on@@ -245,6 +265,7 @@   Just SymbolicBool -> Just SymDict   Just SymbolicInt -> Just SymDict   Just SymbolicInteger -> Just SymDict+  Just SymbolicNatural -> Just SymDict   Just SymbolicText -> Just SymDict   Just SymbolicUTCTime -> Just SymDict   Just SymbolicWord64 -> Just SymDict@@ -266,7 +287,7 @@ -- | Try to discover ordering evidence for @r@ at runtime, companion to -- 'discoverSym'. Returns @Just SymOrdDict@ for the numeric and time -- types whose 'SymRep' is an 'SBV.OrdSymbolic' 'Integer' ('Int',--- 'Integer', the fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32'+-- 'Integer', 'Natural', the fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32' -- \/ 'Word64' \/ 'Int32' \/ 'Int64', and 'UTCTime' encoded as epoch -- seconds); 'Nothing' otherwise. 'Bool' and 'Text' are deliberately -- omitted: ordering a 'Bool' guard is not meaningful, and 'SString'@@ -277,6 +298,7 @@ discoverSymOrd = case discoverSymbolicType @r of   Just SymbolicInt -> Just SymOrdDict   Just SymbolicInteger -> Just SymOrdDict+  Just SymbolicNatural -> Just SymOrdDict   Just SymbolicUTCTime -> Just SymOrdDict   Just SymbolicWord64 -> Just SymOrdDict   Just SymbolicWord32 -> Just SymOrdDict@@ -301,8 +323,10 @@ -- 'discoverSymOrd'. Returns @Just SymNumDict@ for the numeric types -- whose 'SymRep' is the SBV-'Num' 'Integer' ('Int', 'Integer', and the -- fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32' \/ 'Word64' \/--- 'Int32' \/ 'Int64'); 'Nothing' otherwise. 'Bool', 'Text', and--- 'UTCTime' are omitted — not meaningfully arithmetic here. A 'Nothing'+-- 'Int32' \/ 'Int64'); 'Nothing' otherwise. 'Natural' is omitted because+-- its subtraction is partial and throws @Underflow@ for a negative result,+-- unlike ordinary SMT integer subtraction. 'Bool', 'Text', and 'UTCTime' are+-- also omitted. A 'Nothing' -- makes the 'TArith' translator fall back to a fresh opaque variable, -- exactly as 'goEq' \/ 'goCmp' fall back for non-'Sym' operands — -- sound, just imprecise. (The 'Num' constraint on the 'TArith'@@ -322,6 +346,7 @@   Just SymbolicBool -> Nothing   Just SymbolicText -> Nothing   Just SymbolicUTCTime -> Nothing+  Just SymbolicNatural -> Nothing   Nothing -> Nothing  -- | Lift a concrete value to an SBV literal of its 'SymRep'.@@ -330,7 +355,10 @@  -- | Allocate a fresh symbolic variable of the carrier's 'SymRep'. symFree :: forall a. (Sym a) => String -> SBV.Symbolic (SBV.SBV (SymRep a))-symFree = SBV.free+symFree label = do+  value <- SBV.free label+  constrainSymDomain @a value+  pure value  -- * Translation environment ------------------------------------------------- @@ -469,13 +497,13 @@   SBV.Symbolic (SBV.SBV (SymRep r)) translateTermSym _env (TLit r) = pure (symLit r) translateTermSym env (TReg ix) =-  memoFree env (RegVar (indexName ix))+  memoFree @r env (RegVar (indexName ix)) translateTermSym env (TInpCtorField ic 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"+  memoFree @r env (InpVar (icName ic) (indexName ix))+translateTermSym _env (TApp1 _f _t) = symFree @r "app1"+translateTermSym _env (TApp2 _f _a _b) = symFree @r "app2" translateTermSym env (TArith op a b) = case discoverSymNum @r of-  Nothing -> SBV.free "arith" -- sound opaque fallback+  Nothing -> symFree @r "arith" -- sound opaque fallback within the carrier domain   Just SymNumDict -> do     sa <- translateTermSym env a     sb <- translateTermSym env b@@ -485,7 +513,7 @@           OpMul -> (*)     pure (apply sa sb) translateTermSym env (TFieldProj (witness :: FieldWitness projection) base) =-  memoFree env (projectionVarKey witness base)+  memoFree @r env (projectionVarKey witness base)  projectionVarKey ::   forall projection rs ci ifs.@@ -526,7 +554,7 @@   FieldResult projection ->   SBV.Symbolic () constrainFieldProjection env witness base concrete = do-  symbolic <- memoFree env (projectionVarKey witness base)+  symbolic <- memoFree @(FieldResult projection) env (projectionVarKey witness base)   SBV.constrain (symbolic SBV..== symLit concrete)  -- | Memoized symbolic-variable allocator (EP-42). Looks @name@ up in@@ -537,14 +565,14 @@ -- return it. This is what makes repeated reads of the same register or -- input field share a single solver variable. memoFree ::-  forall a.-  (SBV.SymVal a) =>-  SymEnv -> SymVarKey -> SBV.Symbolic (SBV.SBV a)+  forall r.+  (Sym r) =>+  SymEnv -> SymVarKey -> SBV.Symbolic (SBV.SBV (SymRep r)) memoFree env key = do   m <- liftIO (readIORef (seVarCache env))   case Map.lookup key m of     Just (SomeSBV (v :: SBV.SBV b)) ->-      case eqTypeRep (typeRep @a) (typeRep @b) of+      case eqTypeRep (typeRep @(SymRep r)) (typeRep @b) of         Just HRefl -> pure v         Nothing ->           -- Unreachable: a name maps to exactly one representation type.@@ -558,7 +586,7 @@           ordinal <- readIORef (seProjectionOrdinal env)           modifyIORef' (seProjectionOrdinal env) (+ 1)           pure ("proj/" <> show ordinal)-      v <- SBV.free label+      v <- symFree @r label       liftIO (modifyIORef' (seVarCache env) (Map.insert key (SomeSBV v)))       pure v @@ -831,7 +859,7 @@ -- -- The instance constraints @KnownSymbol s@ and @Sym t@ make this -- automatic for any concrete slot list whose value types are in the--- curated 'Sym' registry ('Bool', 'Int', 'Integer', 'Text',+-- curated 'Sym' registry ('Bool', 'Int', 'Integer', 'Natural', 'Text', -- 'UTCTime'). User Registration's 'UserRegRegs' shape qualifies -- without further user code. class ExtractRegFile (rs :: [Slot]) where

@@ -24,6 +24,7 @@     sha256Hex,     stateShapeHash,   )+import Numeric.Natural (Natural) import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy) import Type.Reflection (someTypeRep) @@ -81,6 +82,7 @@      '("int32", Int32),      '("int64", Int64),      '("integer", Integer),+     '("natural", Natural),      '("word", Word),      '("word8", Word8),      '("word16", Word16),@@ -148,6 +150,10 @@     it "concatenates one slot in the documented R3 form" $       regFileShapeCanonical (Proxy @('[ '("retryCount", Int)] :: [(Symbol, Type)]))         `shouldBe` T.pack "retryCount:Int;regfile:0"++    it "pins Natural independently of its base-library representation" $+      regFileShapeCanonical (Proxy @('[ '("revision", Natural)] :: [(Symbol, Type)]))+        `shouldBe` T.pack "revision:Natural;regfile:0"      it "keeps GHC-internal module paths out of every built-in name" $ do       let canonical = regFileShapeCanonical (Proxy @BuiltInSlots)

@@ -12,6 +12,7 @@ import Data.Word (Word16, Word32, Word64, Word8) import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Symbolic+import Numeric.Natural (Natural) import Test.Hspec  -- | A two-constructor input symbol for the 'PInCtor' tests.@@ -114,6 +115,15 @@       isFinal = (== True)     } +-- | Natural uses an unbounded SMT integer with a non-negative domain+-- constraint. It supports equality and ordering, but intentionally not the+-- generic arithmetic registry because Haskell subtraction throws Underflow+-- when its mathematical result would be negative.+type NaturalRegs = '[ '("count", Natural)]++naturalIdx :: Index NaturalRegs Natural+naturalIdx = ZIdx+ -- | A two-edge transducer over a 'Word64' register. Both edges leave -- the @False@ vertex; the second edge carries a constant 'Word64' -- equality that is always false (@5 == 6@), so the pair is mutually@@ -325,6 +335,7 @@     it "discovers Sym Bool" $ symKnown (Proxy @Bool) `shouldBe` True     it "discovers Sym Int" $ symKnown (Proxy @Int) `shouldBe` True     it "discovers Sym Integer" $ symKnown (Proxy @Integer) `shouldBe` True+    it "discovers Sym Natural" $ symKnown (Proxy @Natural) `shouldBe` True     it "discovers Sym Text" $ symKnown (Proxy @Text) `shouldBe` True     it "discovers Sym UTCTime" $ symKnown (Proxy @UTCTime) `shouldBe` True     -- EP-41: fixed-width integers (money + counts).@@ -385,6 +396,34 @@       evalPred timeBeforeGuard runtimeRegs AmtTick `shouldBe` True       checkTransitionDeterminismSym timePrecisionFixture `shouldSatisfy` (not . null)       isSingleValuedSym (withSymPred timePrecisionFixture) `shouldBe` False++    it "constrains Natural register variables to non-negative values" $+      symIsBot+        (PCmp CmpLt (proj naturalIdx) (lit (0 :: Natural)) :: HsPred NaturalRegs AmtCmd)+        `shouldBe` True++    it "keeps Natural equality and ordering solver-visible" $ do+      symIsBot+        (PEq (lit (1 :: Natural)) (lit 2) :: HsPred '[] AmtCmd)+        `shouldBe` True+      symIsBot+        (PCmp CmpGt (lit (1 :: Natural)) (lit 2) :: HsPred '[] AmtCmd)+        `shouldBe` True++    it "extracts a valid Natural witness and withholds generic arithmetic" $ do+      case symSatExt+        ( PAnd+            (PInCtor inCtorAmtTick)+            (PCmp CmpGe (proj naturalIdx) (lit (3 :: Natural))) ::+            HsPred NaturalRegs AmtCmd+        ) of+        Nothing -> expectationFailure "expected a Natural witness"+        Just (registers, command) -> do+          registers ! naturalIdx `shouldSatisfy` (>= 3)+          command `shouldBe` AmtTick+      case discoverSymNum @Natural of+        Nothing -> pure ()+        Just _ -> expectationFailure "Natural must not use ordinary integer arithmetic"    describe "ordering predicate PCmp (EP-41 M2)" $ do     it "constant contradiction 5 >= 10 over Word64 is symIsBot" $

@@ -6,6 +6,7 @@ import Keiki.Core import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Symbolic (checkDeadEdgesSym, checkTransitionDeterminismSym)+import Numeric.Natural (Natural) import Test.Hspec  -- A tiny two-constructor command for guards.@@ -154,6 +155,37 @@       isFinal = (== Mid)     } +-- Natural equality and ordering are symbolic, but generic TArith is opaque+-- because its type-wide registry would also expose partial subtraction.+type NaturalRegs = '[ '("n", Natural)]++naturalIdx :: Index NaturalRegs Natural+naturalIdx = ZIdx++naturalArithmeticOpaqueT ::+  SymTransducer (HsPred NaturalRegs Cmd) NaturalRegs V Cmd ()+naturalArithmeticOpaqueT =+  SymTransducer+    { edgesOut = \case+        Start ->+          [ Edge+              { guard =+                  PCmp+                    CmpGt+                    (tadd (proj naturalIdx) (TLit 1))+                    (TLit 0),+                update = UKeep,+                output = [],+                target = Start,+                mode = Live+              }+          ]+        _ -> [],+      initial = Start,+      initialRegs = RCons (Proxy @"n") 0 RNil,+      isFinal = const False+    }+ -- A 3-slot input constructor, mirroring CoreHiddenInputsGSMSpec, used to build -- a hidden-input edge (its output recovers only slots a, b — never c). data MultiInput = Begin Int Int Int@@ -279,6 +311,50 @@     )     (fooWith (PCmp CmpGt (proj xIdx) (TLit 5))) +intArithmeticStructuralT ::+  SymTransducer (HsPred OverlapRegs Cmd) OverlapRegs V Cmd ()+intArithmeticStructuralT =+  SymTransducer+    { edgesOut = \case+        Start ->+          [ Edge+              (PCmp CmpGt (tadd (proj xIdx) (TLit 1)) (TLit 0))+              UKeep+              []+              Start+              Live+          ]+        _ -> [],+      initial = Start,+      initialRegs = RCons (Proxy @"x") 0 RNil,+      isFinal = const False+    }++naturalInteriorOverlapT ::+  SymTransducer (HsPred NaturalRegs Cmd) NaturalRegs V Cmd ()+naturalInteriorOverlapT =+  SymTransducer+    { edgesOut = \case+        Start ->+          [ Edge+              (PCmp CmpGt (proj naturalIdx) (TLit 1))+              UKeep+              []+              Start+              Live,+            Edge+              (PCmp CmpLt (proj naturalIdx) (TLit 3))+              UKeep+              []+              Start+              Live+          ]+        _ -> [],+      initial = Start,+      initialRegs = RCons (Proxy @"n") 0 RNil,+      isFinal = const False+    }+ differentCtorT ::   SymTransducer (HsPred OverlapRegs Cmd) OverlapRegs V Cmd () differentCtorT =@@ -400,6 +476,16 @@     it "an opaque collection-style guard is flagged when the audit is on" $       validateTransducer optsOn opaqueT `shouldSatisfy` any isOpaqueStart +    it "unsupported Natural arithmetic is flagged when the audit is on" $+      validateTransducer optsOn naturalArithmeticOpaqueT+        `shouldSatisfy` any isOpaqueStart++    it "supported Int arithmetic remains structural" $ do+      let isOpaque (OpaqueGuard {}) = True+          isOpaque _ = False+      validateTransducer optsOn intArithmeticStructuralT+        `shouldSatisfy` (not . any isOpaque)+     it "a fully structural transducer is never flagged, even with the audit on" $ do       let isOpaque (OpaqueGuard {}) = True           isOpaque _ = False@@ -589,6 +675,12 @@     it "uses a mentioned non-integral literal as a concrete witness" $       checkTransitionDeterminismPure boolLiteralWitnessT         `shouldSatisfy` (not . null)++    it "finds an interior overlap in Natural's zero-bounded domain" $ do+      let purePairs = map warningPair (checkTransitionDeterminismPure naturalInteriorOverlapT)+          symbolicPairs = map warningPair (checkTransitionDeterminismSym naturalInteriorOverlapT)+      purePairs `shouldBe` [(Start, 0, 1)]+      purePairs `shouldSatisfy` all (`elem` symbolicPairs)      it "does not guess through POr or an opaque TApp term" $ do       checkTransitionDeterminismPure unknownOrT `shouldBe` []