packages feed

keiki 0.5.0.0 → 0.6.0.0

raw patch · 8 files changed

+168/−28 lines, 8 files

Files

CHANGELOG.md view
@@ -9,6 +9,26 @@ ## [Unreleased]  +## [0.6.0.0] — 2026-07-31++### Added++- `verifyPredicate`, `predicateTranslationExact`, and+  `PredicateVerification` expose whether a predicate received an exact+  structural translation and a definite solver answer. Opaque fallbacks,+  solver `Unknown`/timeouts, and solver failures remain explicitly unverified.++### Changed++- **Breaking semantic fix:** structural `Natural` addition and multiplication+  are now solver-visible, and structural subtraction is total monus in both+  concrete and symbolic evaluation: `a - b = max 0 (a - b)`. It never invokes+  partial Haskell `Natural` subtraction on an underflowing pair; the symbolic+  form is `ite (a >= b) (a - b) 0`.+- `Natural` now belongs to the curated symbolic numeric registry, so+  `OpaqueGuard` no longer reports structural `Natural` arithmetic.++ ## [0.5.0.0] — 2026-07-31  ### Added
keiki.cabal view
@@ -1,6 +1,6 @@ cabal-version:   3.0 name:            keiki-version:         0.5.0.0+version:         0.6.0.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
@@ -316,8 +316,10 @@  -- * Term language ---------------------------------------------------------- --- | A numeric operation carried by 'TArith'. @OpAdd@\/@OpSub@\/@OpMul@--- are @+@\/@-@\/@*@ respectively. Kept as a single tag (rather than+-- | A numeric operation carried by 'TArith'. @OpAdd@ and @OpMul@ are+-- @+@ and @*@ respectively. @OpSub@ is ordinary subtraction except for+-- 'Natural', where it is total monus: @a - b = max 0 (a - b)@. Kept as a+-- single tag (rather than -- three 'Term' constructors) so each total 'Term' walker switches on -- one value; the three directions are recovered by the smart -- constructors 'tadd'\/'tsub'\/'tmul'.@@ -428,7 +430,9 @@   --     guard over a /computed/ value — a weighted sum, a derived cap — is   --     visible to the solver. The 'Num' constraint prevents constructing   --     arithmetic at non-numeric operand types; 'Typeable' lets the SBV-  --     translator dispatch on @r@. Build with 'tadd'\/'tsub'\/'tmul'.+  --     translator dispatch on @r@. 'Natural' subtraction is total monus in+  --     both evaluators rather than the partial 'Num' method. Build with+  --     'tadd'\/'tsub'\/'tmul'.   TArith ::     (Num r, Typeable r) =>     NumOp ->@@ -894,7 +898,9 @@ -- build a 'TArith' over @+@\/@-@\/@*@. The operand type must be numeric -- ('Num') and 'Typeable'; the SBV translator reads them structurally -- (see 'Keiki.Symbolic.discoverSymNum'), unlike the opaque 'TApp'--- escape hatches.+-- escape hatches. For 'Natural', 'tsub' deliberately means total monus:+-- @tsub a b@ evaluates to zero when @b > a@. It never calls the partial+-- 'Natural' subtraction operation on an underflowing pair. tadd,   tsub,   tmul ::@@ -1008,11 +1014,16 @@               ++ icName ic           ) --- | Interpret a 'NumOp' tag as the corresponding numeric operation.--- The 'Num' evidence is supplied by matching the 'TArith' constructor.-applyNumOp :: (Num r) => NumOp -> r -> r -> r+-- | Interpret a 'NumOp' tag as the corresponding total operation. The 'Num'+-- and 'Typeable' evidence is supplied by matching the 'TArith' constructor.+-- 'Natural' subtraction is special-cased to monus before invoking @(-)@ so+-- concrete evaluation cannot throw @Underflow@.+applyNumOp :: forall r. (Num r, Typeable r) => NumOp -> r -> r -> r applyNumOp OpAdd = (+)-applyNumOp OpSub = (-)+applyNumOp OpSub =+  case eqTypeRep (typeRep @r) (typeRep @Natural) of+    Just HRefl -> \a b -> if a >= b then a - b else 0+    Nothing -> (-) applyNumOp OpMul = (*)  -- | Evaluate an 'OutTerm' against a register file and an input symbol.@@ -2053,7 +2064,7 @@       }   | -- | 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+    --       the symbolic numeric registry. 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
src/Keiki/Internal/SymbolicTypes.hs view
@@ -69,6 +69,7 @@ symbolicTypeSupportsNumeric :: SymbolicType r -> Bool symbolicTypeSupportsNumeric SymbolicInt = True symbolicTypeSupportsNumeric SymbolicInteger = True+symbolicTypeSupportsNumeric SymbolicNatural = True symbolicTypeSupportsNumeric SymbolicWord64 = True symbolicTypeSupportsNumeric SymbolicWord32 = True symbolicTypeSupportsNumeric SymbolicWord16 = True
src/Keiki/Symbolic.hs view
@@ -62,6 +62,9 @@     translateTermSym,     translatePred,     constrainFieldProjection,+    PredicateVerification (..),+    predicateTranslationExact,+    verifyPredicate,      -- * Symbolic predicate wrapper     SymPred (..),@@ -323,10 +326,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. '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'+-- 'Int32' \/ 'Int64'), plus 'Natural'. Natural subtraction has the explicit+-- total monus meaning shared with concrete 'evalTerm'; it is translated as+-- @ite (a >= b) (a - b) 0@ rather than ordinary integer subtraction.+-- 'Bool', 'Text', and 'UTCTime' are 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'@@ -337,6 +340,7 @@ discoverSymNum = case discoverSymbolicType @r of   Just SymbolicInt -> Just SymNumDict   Just SymbolicInteger -> Just SymNumDict+  Just SymbolicNatural -> Just SymNumDict   Just SymbolicWord64 -> Just SymNumDict   Just SymbolicWord32 -> Just SymNumDict   Just SymbolicWord16 -> Just SymNumDict@@ -346,7 +350,6 @@   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'.@@ -507,11 +510,15 @@   Just SymNumDict -> do     sa <- translateTermSym env a     sb <- translateTermSym env b-    let apply = case op of-          OpAdd -> (+)-          OpSub -> (-)-          OpMul -> (*)-    pure (apply sa sb)+    case (discoverSymbolicType @r, op) of+      (Just SymbolicNatural, OpSub) ->+        pure (SBV.ite (sa SBV..>= sb) (sa - sb) 0)+      _ -> do+        let apply = case op of+              OpAdd -> (+)+              OpSub -> (-)+              OpMul -> (*)+        pure (apply sa sb) translateTermSym env (TFieldProj (witness :: FieldWitness projection) base) =   memoFree @r env (projectionVarKey witness base) @@ -658,6 +665,89 @@               CmpGt -> (SBV..>)               CmpGe -> (SBV..>=)         pure (apply sa sb)++-- | A conservative answer from 'verifyPredicate'. The two @Verified@+-- constructors mean every predicate node translated structurally and the+-- solver returned a definite result. Opaque Haskell applications, unsupported+-- carrier dictionaries, solver timeouts or @Unknown@, and solver failures are+-- represented explicitly and must not be treated as successful verification.+data PredicateVerification+  = VerifiedSatisfiable+  | VerifiedUnsatisfiable+  | UnverifiedOpaque+  | UnverifiedSolverUnknown String+  | UnverifiedSolverFailure String+  deriving stock (Eq, Show)++-- | Whether every node in a predicate has an exact structural symbolic+-- translation. This is stricter than merely being accepted by 'translatePred',+-- whose compatibility fallback intentionally replaces unsupported pieces with+-- fresh variables.+predicateTranslationExact :: forall rs ci. HsPred rs ci -> Bool+predicateTranslationExact = goPred+  where+    goPred :: HsPred rs ci -> Bool+    goPred PTop = True+    goPred PBot = True+    goPred (PAnd p q) = goPred p && goPred q+    goPred (POr p q) = goPred p && goPred q+    goPred (PNot p) = goPred p+    goPred (PEq a b) = exactEquality a b+    goPred (PInCtor _) = True+    goPred PLeftArm = True+    goPred PRightArm = True+    goPred (PCmp _ a b) = exactOrdering a b++    exactEquality ::+      forall r ifs1 ifs2.+      (Typeable r) =>+      Term rs ci ifs1 r ->+      Term rs ci ifs2 r ->+      Bool+    exactEquality a b = case discoverSym @r of+      Nothing -> False+      Just SymDict -> exactTerm a && exactTerm b++    exactOrdering ::+      forall r ifs1 ifs2.+      (Typeable r) =>+      Term rs ci ifs1 r ->+      Term rs ci ifs2 r ->+      Bool+    exactOrdering a b = case discoverSymOrd @r of+      Nothing -> False+      Just SymOrdDict -> exactTerm a && exactTerm b++    exactTerm :: forall ifs r. (Sym r) => Term rs ci ifs r -> Bool+    exactTerm (TLit _) = True+    exactTerm (TReg _) = True+    exactTerm (TInpCtorField _ _) = True+    exactTerm (TApp1 _ _) = False+    exactTerm (TApp2 _ _ _) = False+    exactTerm (TArith _ a b) = case discoverSymNum @r of+      Nothing -> False+      Just SymNumDict -> exactTerm a && exactTerm b+    exactTerm TFieldProj {} = True++-- | Translate and solve one predicate without collapsing uncertainty into a+-- Boolean. Exact translations produce a verified satisfiable or unsatisfiable+-- answer. Any opaque fallback is rejected before invoking the solver, and+-- every non-definite solver result remains visibly unverified.+verifyPredicate :: HsPred rs ci -> IO PredicateVerification+verifyPredicate predicate+  | not (predicateTranslationExact predicate) = pure UnverifiedOpaque+  | otherwise = do+      result <- SBV.sat $ do+        env <- mkSymEnv+        translatePred env predicate+      pure $ case result of+        SBV.SatResult status -> case status of+          SBV.Satisfiable {} -> VerifiedSatisfiable+          SBV.Unsatisfiable {} -> VerifiedUnsatisfiable+          SBV.Unknown {} -> UnverifiedSolverUnknown "solver returned Unknown"+          SBV.ProofError {} -> UnverifiedSolverFailure "solver returned ProofError"+          SBV.DeltaSat {} -> UnverifiedSolverUnknown "solver returned DeltaSat"+          SBV.SatExtField {} -> UnverifiedSolverUnknown "solver returned SatExtField"  -- * Symbolic predicate wrapper ----------------------------------------------
test/Keiki/OperatorsSpec.hs view
@@ -1,6 +1,7 @@ module Keiki.OperatorsSpec (spec) where  import Keiki.Core+import Numeric.Natural (Natural) import Test.Hspec  -- A trivial command type; the operators here never read it.@@ -72,6 +73,9 @@       n (lit 2 .+ lit 3 .* lit 4) `shouldBe` 14     it "arithmetic feeds a comparison without parens" $       p (lit (10 :: Int) .<= lit 3 .* lit 4) `shouldBe` True+    it "Natural subtraction is total monus" $ do+      evalTerm (lit (2 :: Natural) .- lit 5) RNil NoCmd `shouldBe` 0+      evalTerm (lit (7 :: Natural) .- lit 5) RNil NoCmd `shouldBe` 2    describe "type synonyms" $     it "Pred is interchangeable with HsPred" $
test/Keiki/SymbolicSpec.hs view
@@ -410,7 +410,7 @@         (PCmp CmpGt (lit (1 :: Natural)) (lit 2) :: HsPred '[] AmtCmd)         `shouldBe` True -    it "extracts a valid Natural witness and withholds generic arithmetic" $ do+    it "extracts a valid Natural witness and exposes total arithmetic" $ do       case symSatExt         ( PAnd             (PInCtor inCtorAmtTick)@@ -421,9 +421,23 @@         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"+      isJust (discoverSymNum @Natural) `shouldBe` True++    it "gives Natural subtraction the same total monus meaning concretely and symbolically" $ do+      let underflowing = tsub (lit (2 :: Natural)) (lit 5)+          ordinary = tsub (lit (9 :: Natural)) (lit 4)+      evalTerm underflowing RNil AmtTick `shouldBe` 0+      evalTerm ordinary RNil AmtTick `shouldBe` 5+      verifyPredicate (underflowing .== lit 0 :: HsPred '[] AmtCmd)+        `shouldReturn` VerifiedSatisfiable+      proveP (underflowing .== lit 0 :: HsPred '[] AmtCmd)+        `shouldReturn` True++    it "never upgrades opaque predicate terms to verified" $ do+      let opaque =+            PEq (TApp1 id (lit (1 :: Integer))) (lit 1) :: HsPred '[] AmtCmd+      predicateTranslationExact opaque `shouldBe` False+      verifyPredicate opaque `shouldReturn` UnverifiedOpaque    describe "ordering predicate PCmp (EP-41 M2)" $ do     it "constant contradiction 5 >= 10 over Word64 is symIsBot" $
test/Keiki/ValidationSpec.hs view
@@ -155,8 +155,8 @@       isFinal = (== Mid)     } --- Natural equality and ordering are symbolic, but generic TArith is opaque--- because its type-wide registry would also expose partial subtraction.+-- Natural equality, ordering, and total arithmetic are symbolic. Subtraction+-- is monus in both concrete and symbolic evaluation. type NaturalRegs = '[ '("n", Natural)]  naturalIdx :: Index NaturalRegs Natural@@ -476,9 +476,9 @@     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" $+    it "total Natural arithmetic remains structural" $       validateTransducer optsOn naturalArithmeticOpaqueT-        `shouldSatisfy` any isOpaqueStart+        `shouldSatisfy` (not . any isOpaqueStart)      it "supported Int arithmetic remains structural" $ do       let isOpaque (OpaqueGuard {}) = True