exchangealgebra 0.5.2.0 → 0.5.3.0

raw patch · 16 files changed

+1586/−31 lines, 16 files

Files

• ChangeLog.md +29/−0
• exchangealgebra.cabal +7/−2
• src/ExchangeAlgebra/Algebra/Base.hs +11/−0
• src/ExchangeAlgebra/Algebra/Base/Account/Types.hs +38/−1
• src/ExchangeAlgebra/Algebra/Base/Element.hs +13/−2
• src/ExchangeAlgebra/Algebra/Transfer.hs +6/−2
• src/ExchangeAlgebra/Algebra/Transfer/Closing.hs +39/−0
• src/ExchangeAlgebra/Algebra/Transfer/Rule.hs +196/−16
• src/ExchangeAlgebra/Journal/Transfer/Rule.hs +113/−8
• src/ExchangeAlgebra/Posting.hs +199/−0
• test/Journal/CarrySpec.hs +277/−0
• test/Posting/NoNumPosted.hs +28/−0
• test/Posting/PostingSpec.hs +338/−0
• test/Posting/SettleSpec.hs +189/−0
• test/Spec.hs +6/−0
• test/Transfer/RuleSpec.hs +97/−0

@@ -1,5 +1,34 @@ # Changelog for ExchangeAlgebra +## 0.5.3.0 - 2026-09-26++### Added++- `NFData` instances for base components, including account titles, units,+  Hat labels, account metadata, and `HatBase` values, support forcing ledger keys.+  The benchmark now uses these library instances in place of its local orphans.+- `ExchangeAlgebra.Posting` provides `Posted`, `PostedError`,+  `postedUpperBound`, `posted`, and `unPosted` for checked posting values;+  `PostSide(HatSide, NotSide)` and `sideHat` for concrete sides; and `Posting`,+  `entry`, and `postingAlg` for constructing and reading posting sequences.+- `ExchangeAlgebra.Algebra.Transfer.Rule` provides `SignedNet`, `SettleRule`,+  `retainedEarningsRule`, `SettlementBatch`, `SettleError`, `settleEntries`,+  and `settlementSteps` for ordered settlement pairs. These names are also+  available from the root `ExchangeAlgebra` umbrella. `settleEntries` returns+  `Either` for non-finite nets, including those at excluded keys. Finite+  settlement magnitudes can exceed the checked posting bound.+- `ExchangeAlgebra.Journal.Transfer.Rule` provides `carryEntries` to generate+  reversals under the selected source notes and one rounded exact net per+  complete base under a supplied carry note. Add the result to the journal to+  retain its audit entries. The same module provides `carryBefore` to replace+  selected entries with those carried nets. Other entries, including existing+  entries under the carry note, retain their notes and values. Both operations+  return `Either` when exact aggregation fails.+- `collapseEntries` and `collapseNetEntries` move selected algebra entries to+  rewritten base coordinates, including wildcard axes. The former preserves+  every posting; the latter nets the rewritten entries after axes coincide.+  Add either result to the original ledger to retain its audit entries.+ ## 0.5.2.0 - 2026-09-23  ### Added

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           exchangealgebra-version:        0.5.2.0+version:        0.5.3.0 synopsis:       Exchange Algebra for bookkeeping and economic simulation description:    Please see the README on GitHub at <https://github.com/yakagika/ExchangeAlgebra#readme> category:       Accounting, Finance, Math@@ -104,6 +104,7 @@       ExchangeAlgebra.Optimize       ExchangeAlgebra.Optimize.Annealing       ExchangeAlgebra.Optimize.GA+      ExchangeAlgebra.Posting       ExchangeAlgebra.Render.Bookkeeping       ExchangeAlgebra.Render.Csv       ExchangeAlgebra.Render.Simulation@@ -123,7 +124,7 @@       ExchangeAlgebra.Value       ExchangeAlgebra.Write   other-modules:-      Paths_exchangealgebra+      ExchangeAlgebra.Algebra.Transfer.Closing   hs-source-dirs:       src   ghc-options: -feager-blackholing@@ -238,6 +239,10 @@       Algebra.ExactSumSpec       Algebra.ProjWildcardSpec       Golden.WriteRows+      Journal.CarrySpec+      Posting.NoNumPosted+      Posting.PostingSpec+      Posting.SettleSpec       Transfer.RuleSpec   hs-source-dirs:       test

@@ -39,6 +39,7 @@ import              Data.Time           (Day, TimeOfDay) import GHC.Stack (HasCallStack, callStack, prettyCallStack) import qualified Data.Binary as Binary+import Control.DeepSeq (NFData(..))  customError :: HasCallStack => String -> a customError msg = error (msg ++ "\nCallStack:\n" ++ prettyCallStack callStack)@@ -121,6 +122,8 @@             | HatNot             deriving (Enum, Eq, Ord, Show, Generic) +instance NFData Hat+ instance Hashable Hat where instance Binary.Binary Hat @@ -139,6 +142,8 @@ data BaseForSingleHat = BaseForSingleHat     deriving (Eq,Ord,Generic) +instance NFData BaseForSingleHat+ instance Show BaseForSingleHat where     show _ = "" @@ -189,6 +194,9 @@ data HatBase a where      (:<)  :: (BaseClass a) => {_hat :: Hat,  _base :: a } -> HatBase a +instance (BaseClass a, NFData a) => NFData (HatBase a) where+    rnf (hatValue :< baseValue) = rnf hatValue `seq` rnf baseValue+ instance (BaseClass a, Binary.Binary a) => Binary.Binary (HatBase a) where     put (h :< b) = Binary.put h >> Binary.put b     get = (:<) <$> Binary.get <*> Binary.get@@ -430,6 +438,9 @@             | MS  -- ^ minus stock (stock decrease; Liability\/Equity and contra assets)             | OUT -- ^ output (flow out; Cost)             deriving (Ord, Show, Eq)++instance NFData PIMO where+    rnf value = value `seq` ()  -- | The division-to-PIMO map of the standard interpretation (the @g@ of -- Proposition 5.3.8 restricted to non-contra accounts): Assets are plus

@@ -14,10 +14,12 @@     , ReportingEligibility(..)     ) where +import Control.DeepSeq (NFData(..))+ -- | Account division (financial-statement classification). The -- 'ExchangeAlgebra.Algebra.Base.AccountBase' -- correspondence instance lives in "ExchangeAlgebra.Algebra.Base" (the class's--- home module), so this declaration stays instance-free.+-- home module). data AccountDivision = Assets       -- ^ Assets                      | Equity       -- ^ Equity                      | Liability    -- ^ Liability@@ -25,12 +27,18 @@                      | Revenue      -- ^ Revenue                      deriving (Ord, Show, Eq) +instance NFData AccountDivision where+    rnf value = value `seq` ()+ -- | Credit/debit distinction. v'Side' is the wildcard used by legacy APIs. data Side = Credit -- ^ Credit side.           | Debit  -- ^ Debit side.           | Side   -- ^ Wildcard.           deriving (Ord, Show, Eq) +instance NFData Side where+    rnf value = value `seq` ()+ -- | Registry-level policy for automatic closing entries. -- -- 'CloseByDivision' derives the transfer side from 'AccountDivision'.@@ -40,12 +48,18 @@                  | NoClose         -- ^ Do not generate an automatic closing entry.                  deriving (Show, Eq) +instance NFData ClosingRule where+    rnf value = value `seq` ()+ -- | Fixed/Current distinction. Used for classifying account titles as fixed or current. data FixedCurrent = Fixed   -- ^ Fixed                   | Current -- ^ Current                   | Other   -- ^ Other (expenses, revenues, etc.)                   deriving (Show, Eq) +instance NFData FixedCurrent where+    rnf value = value `seq` ()+ -- | Accounting role of an account-basis coordinate. Roles are not assumed to -- be mutually exclusive; see -- 'ExchangeAlgebra.Algebra.Base.Account.Registry.AccountSemantics' in the@@ -61,6 +75,9 @@     | ReportingSubtotal     deriving (Show, Eq) +instance NFData AccountRole where+    rnf value = value `seq` ()+ -- | Context in which an account title may be used as a posting coordinate. -- Enforcement is introduced by the checked-conversion API in a later land; -- this type is the canonical metadata used by that gate.@@ -72,6 +89,9 @@     | NotPostable     deriving (Show, Eq) +instance NFData PostingCapability where+    rnf value = value `seq` ()+ -- | Meaning of the legacy five-way 'AccountDivision' value. -- -- This separates a genuine statement classification from a bookkeeping@@ -84,6 +104,13 @@     | NoStatementDivision     deriving (Show, Eq) +instance NFData DivisionSemantics where+    rnf value = case value of+        StatementDivision division        -> rnf division+        BookkeepingControlClass division  -> rnf division+        DirectionEncoding division        -> rnf division+        NoStatementDivision               -> ()+ -- | Semantic status of an account's normal posting side. data HomeSideSemantics     = FixedHomeSide Side@@ -92,6 +119,13 @@     | NoPostingSide     deriving (Show, Eq) +instance NFData HomeSideSemantics where+    rnf value = case value of+        FixedHomeSide side       -> rnf side+        ContextDependentHomeSide -> ()+        NoFixedHomeSide          -> ()+        NoPostingSide            -> ()+ -- | Coarse reporting eligibility. Actual presentation remains a function of -- reporting context and policy and is implemented in a later land. data ReportingEligibility@@ -100,3 +134,6 @@     | DerivedPresentation     | NotPresented     deriving (Show, Eq)++instance NFData ReportingEligibility where+    rnf value = value `seq` ()

@@ -18,11 +18,12 @@      To use your own type as a basis component, declare an 'Element' instance.     A single distinguished value must serve as the wildcard used by the-    transfer engine and by projection operations:+    transfer engine and by projection operations. Derive 'NFData' when keys+    containing this component must be fully evaluated:      @     data Company = CompanyA | CompanyB | CompanyWildcard-      deriving (Eq, Ord, Show, Generic, Hashable, Typeable)+      deriving (Eq, Ord, Show, Generic, Hashable, NFData, Typeable)      instance Element Company where       wildcard = CompanyWildcard@@ -63,6 +64,7 @@ import GHC.Generics (Generic) import Data.Hashable import Data.Typeable (Typeable, cast, typeOf)+import Control.DeepSeq (NFData(..)) import qualified Data.Binary as Binary import qualified Data.Binary.Get as BinaryGet import qualified Data.Binary.Put as BinaryPut@@ -203,6 +205,11 @@ -- Used to decompose multi-dimensional bases (tuples) into per-axis keys for indexing. data AxisKey = forall a. Element a => AxisKey !a +-- | Force the stored axis to weak head normal form without requiring 'NFData'+-- from every user-defined 'Element'.+instance NFData AxisKey where+    rnf (AxisKey axis) = axis `seq` ()+ instance Eq AxisKey where     AxisKey x == AxisKey y = case cast y of         Nothing -> False@@ -502,6 +509,8 @@ -- (2026-06-11 調査)。Enum/Binary 序数の安定のため削除はせず, 新名称への移行を促す。 {-# DEPRECATED Commutation "通信費 (communication expenses) — use 'CommunicationExpenses' instead" #-} +instance NFData AccountTitles+ instance Hashable AccountTitles where     {-# INLINE hashWithSalt #-}     hashWithSalt salt x = hashWithSalt salt (fromEnum x)@@ -541,6 +550,8 @@                 | Amount                 | CountUnit                 deriving (Show, Ord, Eq, Enum,Generic)++instance NFData CountUnit  instance Hashable CountUnit where     {-# INLINE hashWithSalt #-}

@@ -15,8 +15,12 @@     Mixed wildcard positions can make the legacy tree lookup miss matching     entries even for disjoint rules. Overlap priority is unspecified, and     matching is symmetric (ledger wildcards also match concrete patterns).-    These known limitations are preserved for compatibility.-    Use "ExchangeAlgebra.Algebra.Transfer.Rule" for one-way source matching.+    P3 is required only for equivalence with the legacy @transfer@ and+    @finalStockTransfer@ APIs, which match symmetrically. The new+    "ExchangeAlgebra.Algebra.Transfer.Rule" API uses one-way matching in+    @transferEntries@ and groups @closingEntries@ by actual base; both treat+    a wildcard stored in the ledger as a value. These known legacy+    limitations are preserved for compatibility.      Package for Exchange Algebra defined by Hiroshi Deguchi. 

@@ -0,0 +1,39 @@+{-|+Module      : ExchangeAlgebra.Algebra.Transfer.Closing+Description : Shared closing posting construction.++This internal Foundation module constructs a source reversal and destination+posting using the algebra. The transfer rules and Accounting settlement select+the destination side before calling 'closingPairBy'. Read 'closingPairBy' after+the source-side rules in the calling module.++The pair implements the posting construction used in Definition 9.+-}+module ExchangeAlgebra.Algebra.Transfer.Closing+    ( closingPairBy+    ) where++import ExchangeAlgebra.Algebra+    ( Alg+    , HatVal+    , HatBaseClass(..)+    , ExBaseClass(..)+    , AccountTitles+    , Redundant((.+))+    , (.@)+    )++-- | Reverse a closing balance and post it to the given destination account.+-- The first argument transforms the source to the target side: @id@ retains+-- Hat/Not, and 'revHat' reverses it. The caller must classify the source,+-- and the value must satisfy the non-negative,+-- finite posting contract of '.@'.+closingPairBy :: (HatVal v, ExBaseClass b)+              => (b -> b)+              -> AccountTitles+              -> v+              -> b+              -> Alg v b+closingPairBy targetSide targetAccount value source+    =  (value .@ revHat source)+    .+ (value .@ setAccountTitle (targetSide source) targetAccount)

@@ -1,4 +1,9 @@ {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}  {- | Module      : ExchangeAlgebra.Algebra.Transfer.Rule@@ -7,8 +12,10 @@ Definition 9 describes a transfer by adding source cancellations and target postings to the original algebra. For @Right entries = transferEntries rules a@, @a .+ entries@ is precisely that expression. This module returns only the-additional entries, preserving the original audit trail. It never applies-@bar@. 'closingEntries' explicitly nets each closing account first.+additional entries, preserving the original audit trail. Only+'collapseNetEntries' applies @bar@ to rewritten entries. 'closingEntries'+uses sequential side totals from the source entries, while 'settleEntries'+accepts signed nets already computed by its caller.  == Laws @@ -24,7 +31,10 @@   P2, patterns are disjoint; P3, ledger bases contain no wildcards; P4, axes   are not nested tuples; P5, transformed values are nonzero. The legacy table   translates 'Relabel', 'MulBy' and 'DivBy' to @id@, @(* p)@ and @(/ p)@,-  respectively, and applying the new rules returns @Right entries@.+  respectively, and applying the new rules returns @Right entries@. P3 is+  needed only for equivalence with legacy @transfer@, whose matching is+  symmetric. 'transferEntries' matches one way and treats ledger wildcards+  as values. * Relation: @obs (a .+ entries) ~= obs (transfer a table)@. * Observation: @obs@ as defined above, including every target base. * Tolerance: relative @1e-9@; tested values are integers in @1..1000000@,@@ -36,7 +46,10 @@ * Subject: 'closingEntries' and legacy @finalStockTransfer@. * Preconditions: concrete ledger bases, valid Hat\/Not postings and values   in the L1 range; the ledger includes only entries up to the closing date.-  Closing returns @Right entries@.+  Closing returns @Right entries@. Concrete bases are needed only for+  equivalence with legacy @finalStockTransfer@ and its symmetric matching;+  'closingEntries' groups by each actual base, including ledger wildcards+  as values. * Relation: @obs (a .+ entries) ~= obs (finalStockTransfer a)@. * Observation: @obs@, including 'RetainedEarnings' and all retained axes. * Tolerance: relative @1e-9@ within the stated range. Large historical@@ -77,6 +90,18 @@ * Tolerance: none. * Instances: all lawful 'HatVal' and 'HatBaseClass' instances (closing also   requires 'ExBaseClass'). Hat reversal is never numeric negation.++=== L6: coordinate collapse++* Subject: 'collapseEntries' and 'collapseNetEntries'.+* Preconditions: non-negative valid postings and an exact additive value type.+* Relation: @bar (x .+ collapseEntries p f x) ==+  bar (x .+ collapseNetEntries p f x)@. The raw form has twice as many+  postings as @proj p x@ and twice its norm; the net form calls 'bar' after+  rewriting the base parts.+* Observation: net ledger and raw posting count and norm.+* Tolerance: exact.+* Instances: @MoneyDecimal@ with 'HatBaseClass' bases. -} module ExchangeAlgebra.Algebra.Transfer.Rule     ( TransferScale(..)@@ -89,24 +114,41 @@     , relabel     , scaleBy     , divideBy+      -- * Additional entries     , transferEntries+    , collapseEntries+    , collapseNetEntries+      -- * Closing entries     , ClosingSide(..)     , closingSide     , closingEntries+    , SettleRule+    , retainedEarningsRule+    , SettlementBatch+    , SignedNet+    , SettleError(..)+    , settleEntries+    , settlementSteps     ) where  import           Data.Binary (Binary(..)) import           Data.Hashable (Hashable) import           Data.List (find, sortOn, tails)+import           Data.Map.Strict (Map) import qualified Data.Map.Strict as Map+import           Data.Maybe (mapMaybe) import           GHC.Generics (Generic) import           ExchangeAlgebra.Algebra                      ( Alg(..), HatVal(..), HatBaseClass(..), ExBaseClass(..)-                     , Hat(..), AccountTitles(..), Redundant((.+))-                     , ignoreWildcard, foldEntries+                     , Hat(..), HatBase(..), CountUnit(..), Element(..)+                     , AccountTitles(..), Redundant((.+), (.^), bar, norm)+                     , (.@)+                     , ignoreWildcard, foldEntries, mapBasePart, proj+                     , postFromNetBy, vals                      , accountSpec, asClosing, ClosingRule(..)                      , classifyAccountDivision, classifyAccountContra                      , pimoFromDivision, pimoFlip, PIMO(..) )+import ExchangeAlgebra.Algebra.Transfer.Closing (closingPairBy)  -- | How a rule changes the value it moves. data TransferScale v@@ -204,6 +246,8 @@ matches :: HatBaseClass b => b -> b -> Bool matches patternBase entry = ignoreWildcard entry patternBase == entry +-- * Additional entries+ -- | Generate cancellation and destination entries, without the input ledger. -- Input values must satisfy the ordinary non-negative, finite posting contract. -- 'Relabel'-only rules cannot fail. Scaled overflow returns 'NonFiniteResult',@@ -239,6 +283,62 @@             DivBy coefficient -> value / coefficient         cancellation = value :@ revHat source +-- | Move selected entries to new base coordinates while retaining every posting.+-- Query patterns use one-way matching: only a pattern wildcard matches any+-- coordinate. The function rewrites each selected 'BasePart' with the supplied+-- function, so callers can replace an axis with its wildcard. A transfer+-- rule's target wildcard instead keeps the source coordinate; it cannot turn+-- a concrete coordinate into a wildcard.+--+-- The result contains only the added entries: a Hat-reversed copy of each+-- selected posting and its rewritten copy. Add it to the ledger with @(.+)@.+-- Values remain non-negative, and this function does not call 'bar', so it+-- retains redundant audit detail. 'collapseNetEntries' nets the rewritten+-- entries instead. 'postFromNetBy' generates new postings for each netted+-- classification; both collapse functions move the coordinates of the same+-- entries.+-- On an axis-preserving ledger, @norm . bar@ cannot cancel across axes.+--+-- >>> type T = Alg Double (HatBase CountUnit)+-- >>> x = 10 .@ Not :< Yen .+ 4 .@ Hat :< Dollar :: T+-- >>> let moved = collapseEntries [HatNot :< wildcard] (const wildcard) x+-- >>> norm moved+-- 28.0+-- >>> length (vals moved)+-- 4+collapseEntries :: (HatVal v, HatBaseClass b)+                => [b] -> (BasePart b -> BasePart b) -> Alg v b -> Alg v b+collapseEntries pats f x = (.^) selected .+ mapBasePart f selected+  where+    selected = proj pats x++-- | Move selected entries to new base coordinates and net the rewritten side.+-- The result contains only added entries: a Hat-reversed copy of the selected+-- postings plus @bar (mapBasePart f selected)@. This function calls 'bar'+-- internally after rewriting, so opposite sides from distinct original axes+-- can cancel when the new base parts coincide. Add the result to the original+-- ledger with @(.+)@. It leaves the original audit entries in place.+--+-- Query wildcards match one way. A wildcard in a transfer rule's target+-- preserves the source coordinate; use this function to replace a concrete+-- coordinate with a wildcard. 'collapseEntries' retains all rewritten+-- postings. 'postFromNetBy' generates new postings for each netted+-- classification, while this function moves the coordinates of the same+-- entries. On an axis-preserving ledger, @norm . bar@ does not cancel across+-- axes.+--+-- >>> type T = Alg Double (HatBase CountUnit)+-- >>> x = 10 .@ Not :< Yen .+ 4 .@ Hat :< Dollar :: T+-- >>> norm (bar (x .+ collapseNetEntries [HatNot :< wildcard] (const wildcard) x))+-- 6.0+collapseNetEntries :: (HatVal v, HatBaseClass b)+                   => [b] -> (BasePart b -> BasePart b) -> Alg v b -> Alg v b+collapseNetEntries pats f x = (.^) selected .+ bar (mapBasePart f selected)+  where+    selected = proj pats x++-- * Closing entries+ -- | The retained-earnings side selected by a closing account's PIMO direction. data ClosingSide     = ClosingKeep -- ^ IN: retain Hat/Not (revenue or contra cost).@@ -266,7 +366,7 @@         | otherwise = ordinaryDirection     ordinaryDirection = pimoFromDivision (classifyAccountDivision title) --- | Generate closing entries from each eligible base's exact net balance.+-- | Generate closing entries from each eligible base's sequential side totals. -- Supply only postings through the closing date. Hat and Not totals are -- compared without a tolerance; their non-negative difference is closed. -- This deliberately folds the source sequences (audit detail) per base,@@ -302,12 +402,92 @@         | otherwise = checkedPair source (notTotal - hatTotal) source     checkedPair source value balanceBase         | isErrorValue value = Left (NonFiniteBalance source)-        | otherwise = Right (closingPair value balanceBase)-    closingPair value source = case closingSide (getAccountTitle source) of-        Nothing -> Zero-        Just side ->-            let targetSource = case side of-                    ClosingKeep -> source-                    ClosingFlip -> revHat source-            in (value :@ revHat source)-                .+ (value :@ setAccountTitle targetSource RetainedEarnings)+        | otherwise = case closingSide (getAccountTitle balanceBase) of+            Nothing   -> Right Zero+            Just side -> Right+                (closingPairBy (targetSide side) RetainedEarnings value balanceBase)+    targetSide side = case side of+        ClosingKeep -> id+        ClosingFlip -> revHat++-- | A closing rule containing only its destination account title.+-- The private constructor restricts destinations to accounts compatible with+-- the closing directions.+newtype SettleRule = SettleRule AccountTitles++-- | Close eligible accounts into 'RetainedEarnings', preserving all other axes.+retainedEarningsRule :: SettleRule+retainedEarningsRule = SettleRule RetainedEarnings++-- | Settlement pairs in strictly ascending source-base order.+-- A model returns only @Posting@ built with @entry@ and 'Monoid'. Settlement+-- magnitudes can exceed the @Posted@ bound, so this type has no conversion to+-- @Posting@ and no 'Semigroup' or 'Monoid' instance.+--+-- Record each pair separately in source-base order. Combining all pairs first+-- can change the order of additions to a shared destination. For example,+-- sequential increments @T, 1, -T@ with @T = 2^53@ give 0 in 'Double', whereas+-- adding @T, -T, 1@ gives 1.+newtype SettlementBatch b = SettlementBatch [(BasePart b, Alg Double b)]++-- | A signed Not-minus-Hat net. This is not a non-negative posting magnitude.+-- As a type synonym, it does not enforce finiteness or any numeric range.+type SignedNet = Double++-- | The first non-finite input net, identified by its complete base coordinates.+data SettleError b = NonFiniteNet (BasePart b)++deriving instance Eq (BasePart b) => Eq (SettleError b)+deriving instance Show (BasePart b) => Show (SettleError b)++-- | Construct one reversal and destination pair per eligible source base.+-- Input values are signed Not-minus-Hat nets. Zero nets, accounts without a+-- closing side, and destination bases produce no pair. Every pair has two+-- finite, non-negative magnitudes equal to the absolute input net; the source+-- reversal cancels that net exactly. Other base axes are preserved.+--+-- A non-finite input, including at an excluded key, returns 'Left' with the+-- first key in ascending order. Finite magnitudes above+-- 'ExchangeAlgebra.Posting.postedUpperBound' are accepted, without passing+-- through 'ExchangeAlgebra.Posting.posted'. No implicit @bar@ or @compress@ is+-- applied. Complexity: O(b) for b input bases.+-- Law: subject: each generated settlement pair; preconditions: all nets finite.+-- Relation: each reversal cancels its source net. For each destination base,+-- its increment is the sum of @direction * net@ over the source bases, where+-- @direction@ is +1 for 'ClosingKeep' and -1 for 'ClosingFlip'.+-- Observation: sums of @decL@ and @decR@ lifted to Rational for each pair.+-- Tolerance: exact. Instances: 'ExBaseClass' bases with Double posting values.+settleEntries :: forall b. ExBaseClass b+              => SettleRule+              -> Map (BasePart b) SignedNet+              -> Either (SettleError b) (SettlementBatch b)+settleEntries (SettleRule destination) amounts+    = case mapMaybe nonFinite (Map.toAscList amounts) of+        first : _ -> Left (NonFiniteNet first)+        []        -> Right (SettlementBatch (mapMaybe close (Map.toAscList amounts)))+  where+    finite amount = not (isNaN amount || isInfinite amount)+    nonFinite (coordinates, amount)+        | finite amount = Nothing+        | otherwise     = Just coordinates+    close (coordinates, amount)+        | amount == 0 = Nothing+        | coordinates == base (setAccountTitle source destination) = Nothing+        | otherwise = case closingSide (getAccountTitle source) of+            Nothing   -> Nothing+            Just side -> Just+                (coordinates, closingPairBy (targetSide side) destination (abs amount) source)+      where+        source = merge (sourceSide amount) coordinates :: b+    sourceSide amount+        | amount < 0 = Hat+        | otherwise  = Not+    targetSide side = case side of+        ClosingKeep -> id+        ClosingFlip -> revHat++-- | Read the pairs in strictly ascending source-base order, without constraints+-- on the base type. Record each pair before proceeding to the next source.+-- Complexity: O(1) to expose the list; O(b) to consume b pairs.+settlementSteps :: SettlementBatch b -> [(BasePart b, Alg Double b)]+settlementSteps (SettlementBatch steps) = steps

@@ -1,27 +1,39 @@ {- | Module      : ExchangeAlgebra.Journal.Transfer.Rule-Description : Note-preserving transfer entries and closing across notes.+Description : Note-preserving transfer and carry entries across notes.  Use a qualified import to distinguish these functions from the Algebra API:  > import qualified ExchangeAlgebra.Journal.Transfer.Rule as Transfer -Definition 9 and laws L1-L5 are documented in-"ExchangeAlgebra.Algebra.Transfer.Rule". Transfer lifts that operation over-notes; closing reads the combined ledger and returns an unannotated algebra-through 'Either'.+The additional-entry operations return entries to add to the input journal.+'carryBefore' instead returns the complete journal after replacing selected+notes. Transfer lifts Definition 9 over notes; closing reads the combined+ledger and returns an unannotated algebra through 'Either'. Read the+additional-entry section before the complete-result section. -} module ExchangeAlgebra.Journal.Transfer.Rule-    ( transferEntries+    ( -- * Additional entries+      transferEntries     , closingEntries+    , carryEntries+      -- * Complete results+    , carryBefore     ) where  import qualified Data.HashMap.Strict as Map-import           ExchangeAlgebra.Algebra (Alg, HatVal, HatBaseClass, ExBaseClass)+import qualified Data.Map.Strict as OrderedMap+import           ExchangeAlgebra.Algebra (Alg, HatVal, ExBaseClass, (.@), Redundant((.^))) import           ExchangeAlgebra.Algebra.Transfer.Rule (TransferRules, TransferApplyError) import qualified ExchangeAlgebra.Algebra.Transfer.Rule as Rule-import           ExchangeAlgebra.Journal (Journal, Note, toMap, fromMap, toAlg)+import           ExchangeAlgebra.Algebra.Base (Hat(..), HatBaseClass(..))+import           ExchangeAlgebra.Journal (Journal, Note, (.|), toMap, fromMap, toAlg)+import qualified ExchangeAlgebra.Journal as Journal+import           ExchangeAlgebra.Journal.Exact (ExactSumError)+import qualified ExchangeAlgebra.Journal.Exact as Exact +-- * Additional entries+ -- | Generate additional entries under the same notes as their sources. -- Each note is processed in the traversal order of 'toMap'. The first failure -- aborts the whole operation; no partial Journal is returned. This order is@@ -51,3 +63,96 @@ closingEntries :: (Note n, HatVal v, ExBaseClass b)                => Journal n v b -> Either (TransferApplyError v b) (Alg v b) closingEntries = Rule.closingEntries . toAlg++-- | Round selected complete-base nets once and attach the carry note.+carryNetEntries :: (Note n, HatBaseClass b)+                => n+                -> Journal n Double b+                -> Either ExactSumError (Journal n Double b)+carryNetEntries carryNote selected = do+    balances <- Exact.balanceMapByExact Just selected+    pure (OrderedMap.foldlWithKey' append mempty balances)+  where+    append result coordinates (direction, value) = case direction of+        EQ -> result+        GT -> result <> ((value .@ merge Not coordinates) .| carryNote)+        LT -> result <> ((value .@ merge Hat coordinates) .| carryNote)++-- | Generate carry entries while retaining every original posting.+-- Select source notes with the predicate, reverse the Hat or Not side of each+-- selected scalar under its original note, and append one rounded exact net+-- per complete base under the carry note. An exact zero net adds no entry.+-- The net uses 'Exact.balanceMapByExact' on the selected original scalars;+-- no @bar@ or intermediate rounding is applied. An aggregation failure+-- returns 'Left' with 'ExactSumError'.+--+-- Inputs require concrete Hat or Not sides and finite, non-negative values.+-- Selected nonzero HatNot entries lie outside this contract. Applying the+-- returned entries cancels selected notes mathematically, but reading the+-- resulting journal with Exact can fail: reversing Not and Hat entries of+-- @2^1023@ at one base makes each side total @2^1024@.+--+-- Law: subject: 'carryEntries'. Preconditions: selected exact aggregation+-- succeeds and the input meets the side and value contract above.+-- Relation: for each base @b@, the Rational Not-minus-Hat balance obeys+-- @exact_b(j <> e) - exact_b(j) = RN(s_b) - s_b@, where @e@ is the generated+-- journal, @s_b@ is the selected exact net, and @RN@ rounds once to Double.+-- Observation: Rational balances of original scalar entries, including zero+-- bases. Tolerance: exact Rational equality. Instances: 'Note' and+-- 'HatBaseClass' with Double values.+carryEntries :: (Note n, HatBaseClass b)+             => (n -> Bool)+             -> n+             -> Journal n Double b+             -> Either ExactSumError (Journal n Double b)+carryEntries selectedNote carryNote journal = do+    carried <- carryNetEntries carryNote selected+    pure (Journal.map (.^) selected <> carried)+  where+    selected = Journal.filterWithNote (\note _ -> selectedNote note) journal++-- * Complete results++-- | Replace selected notes with one rounded exact net per complete base.+-- Other entries retain their notes, bases, sides, and values. Entries already+-- under the carry note remain when that note is not selected. This returns+-- the entire resulting journal: selected audit entries are discarded, rather+-- than retained with cancellation entries. Positive nets become Not entries,+-- negative nets become Hat entries, and exact zero nets add nothing.+--+-- For selected entries @S@, unselected entries @U@, and rounded carried+-- entries @Q@, this function constructs @U <> Q@ directly. Its result has+-- the same nonzero scalar-entry multiset as adding 'carryEntries' to the+-- original journal and then forgetting notes selected by the predicate.+-- This decomposition requires @not (selectedNote carryNote)@, concrete Hat+-- or Not sides, finite non-negative values, and successful exact aggregation.+-- It does not claim equality for zero entries, empty notes, or sequence order.+-- Existing entries under the carry note remain and are not netted again.+-- When @selectedNote carryNote@ is true, this function still carries as+-- described, but the decomposition does not hold because forgetting the+-- selected notes would also remove @Q@. Selected nonzero HatNot entries lie+-- outside the contract.+--+-- The selected net is computed by 'Exact.balanceMapByExact' and rounded once+-- per complete base. An aggregation failure returns 'Left' with+-- 'ExactSumError'. Structurally, 'carryEntries' resembles+-- 'ExchangeAlgebra.Algebra.Transfer.Rule.collapseNetEntries': both generate+-- reversals and moved nets. The latter uses @bar@ after rewriting and has a+-- different numeric contract. Complexity: O(e log(k + 1)) for e selected+-- scalars and k distinct selected complete bases, plus filtering and merge.+-- Law: subject: 'carryBefore'. Preconditions: the decomposition conditions+-- above. Relation: the nonzero scalar-entry multiset equals that obtained+-- from @forgetNotes p (j <> e)@ for @Right e = carryEntries p n j@.+-- Observation: nonzero scalar-entry multiset. Tolerance: exact.+-- Instances: 'Note' and 'HatBaseClass' with Double values.+carryBefore :: (Note n, HatBaseClass b)+            => (n -> Bool)+            -> n+            -> Journal n Double b+            -> Either ExactSumError (Journal n Double b)+carryBefore selectedNote carryNote journal = do+    carried <- carryNetEntries carryNote selected+    pure (retained <> carried)+  where+    selected = Journal.filterWithNote (\note _ -> selectedNote note) journal+    retained = Journal.filterWithNote (\note _ -> not (selectedNote note)) journal

@@ -0,0 +1,199 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}++-- | Build checked postings in the Accounting layer.+-- The module uses the foundation algebra to construct @Posting@ values without+-- implicit cancellation. Models and simulators consume these postings. Read+-- checked values, sides, and then entries.+--+-- Posting construction follows Definitions 3-5.+module ExchangeAlgebra.Posting+    ( -- * Posting values+      Posted+    , PostedError(..)+    , postedUpperBound+    , posted+    , unPosted+      -- * Posting sides+    , PostSide(..)+    , sideHat+      -- * Postings+    , Posting+    , entry+    , postingAlg+    ) where++import Control.DeepSeq (NFData(..))+import Data.Binary (Binary(..))+import Data.Hashable (Hashable(..))+import GHC.Generics (Generic)++import ExchangeAlgebra.Algebra (Alg(Zero), HatVal(isErrorValue), (.+), (.@))+import ExchangeAlgebra.Algebra.Base+    ( Hat(..)+    , HatBaseClass(BasePart, merge, base)+    )++-- * Posting values++-- | A checked posting value with no 'Num', 'Fractional', or 'Real' instance.+--+-- Invariant: the stored 'Double' is finite and lies in @[0, 2^900]@;+-- zero is stored as positive zero. Construct values through 'posted'.+newtype Posted = Posted Double+    deriving stock (Eq, Ord, Show)++instance NFData Posted where+    rnf (Posted value) = rnf value++instance Hashable Posted where+    hashWithSalt salt (Posted value) = hashWithSalt salt value++-- | Decoding checks the same invariant as 'posted' and fails on invalid input.+instance Binary Posted where+    put = put . unPosted+    get = do+        value <- get+        case posted value of+            Left failure    -> fail (show failure)+            Right validated -> pure validated++-- | The first failed check, in the order used by 'posted'.+data PostedError+    = NonFinite  -- ^ NaN or either infinity.+    | Negative   -- ^ A finite value below zero.+    | AboveBound -- ^ A finite value above 'postedUpperBound'.+    deriving stock (Eq, Show, Generic)++instance NFData PostedError++-- | Inclusive bound @2^900@. A sum of nearly @2^123@ such values remains below+-- the largest finite Double (less than @2^1024@), leaving aggregation headroom.+-- Complexity: O(1).+postedUpperBound :: Double+postedUpperBound = 2 ^ (900 :: Int)++-- | Validate a value, normalizing negative zero to positive zero.+-- Checks non-finiteness, negativity, and the upper bound in that order,+-- returning the corresponding 'PostedError' on failure.+--+-- For every finite @x@ in @[0, postedUpperBound]@, with @normalizeZero x@+-- equal to positive zero when @x == 0@ and to @x@ otherwise:+--+-- > fmap unPosted (posted x) == Right (normalizeZero x)+--+-- The law uses exact 'Double' equality, with the sign of zero also normalized.+-- Finite, nonnegative values use the same 'isErrorValue' check as '.@'.+-- 'postedUpperBound' is checked only at the posting entry point.+-- Complexity: O(1).+posted :: Double -> Either PostedError Posted+posted value+    | isErrorValue value       = Left (invalidValueError value)+    | value > postedUpperBound = Left AboveBound+    | value == 0               = Right (Posted 0)+    | otherwise                = Right (Posted value)+  where+    invalidValueError invalid+        | isNaN invalid || isInfinite invalid = NonFinite+        | otherwise                           = Negative++-- | Read a checked value. For every @p@, @posted (unPosted p) == Right p@.+-- Complexity: O(1).+unPosted :: Posted -> Double+unPosted (Posted value) = value++-- * Posting sides++-- | The two posting sides; query wildcard 'HatNot' is excluded.+data PostSide+    = HatSide -- ^ The @Hat@ side.+    | NotSide -- ^ The 'Not' side.+    deriving stock (Eq, Ord, Show, Enum, Bounded, Generic)++instance Binary PostSide++instance Hashable PostSide++instance NFData PostSide++-- | Embed a posting side into a query-capable hat.+-- @sideHat HatSide == Hat@ and @sideHat NotSide == Not@; 'HatNot' is never returned.+-- Complexity: O(1).+sideHat :: PostSide -> Hat+sideHat HatSide = Hat+sideHat NotSide = Not++-- * Postings++-- | Postings built through 'entry' and 'Monoid', without implicit cancellation+-- or compression. Equality and display delegate to the underlying 'Alg'.+-- Equality is structural and depends on construction order. To compare+-- multisets of postings instead, compare the results of @toASCList . postingAlg@.+newtype Posting b = Posting (Alg Double b)++instance HatBaseClass b => Eq (Posting b) where+    Posting left == Posting right = left == right++instance HatBaseClass b => Show (Posting b) where+    showsPrec precedence (Posting algebra) = showsPrec precedence algebra++instance NFData (Posting b) where+    rnf (Posting algebra) = rnf algebra++-- | Preserve algebra addition:+--+-- > postingAlg (a <> b) == (postingAlg a .+ postingAlg b)+--+-- This law uses 'Alg' equality without a tolerance for every 'HatBaseClass'+-- instance, so it also preserves the multiset of postings. Associativity+-- holds as equality of posting multisets, using+-- @sameMultiset x y = toASCList x == toASCList y@:+--+-- > sameMultiset (postingAlg ((a <> b) <> c)) (postingAlg (a <> (b <> c)))+--+-- Complexity: the same as '(.+)' on the underlying algebras.+instance HatBaseClass b => Semigroup (Posting b) where+    Posting left <> Posting right = Posting (left .+ right)++-- | The empty posting obeys @postingAlg mempty == Zero@ using exact 'Alg' equality.+-- The identity laws hold as equality of posting multisets for every+-- 'HatBaseClass' instance, without a numeric tolerance:+--+-- > sameMultiset (postingAlg (mempty <> a)) (postingAlg a)+-- > sameMultiset (postingAlg (a <> mempty)) (postingAlg a)+--+-- Here @sameMultiset x y = toASCList x == toASCList y@.+-- Complexity: O(1) for 'mempty'; combination uses the 'Semigroup' instance.+instance HatBaseClass b => Monoid (Posting b) where+    mempty = Posting Zero++-- | Read the underlying algebra. For every side, checked value, and base part:+--+-- > postingAlg (entry side value part) == unPosted value .@ merge (sideHat side) part+--+-- This is a one-way conversion with exact 'Alg' equality. For a list @xs@+-- of @(side, value, part)@ triples, let @mk (s, v, p) = entry s v p@ and+-- @sameMultiset x y = toASCList x == toASCList y@. Conversion and projection+-- preserve the multiset of postings for every query list @qs@, including+-- 'HatNot' and coordinate wildcards:+--+-- > sameMultiset (postingAlg (foldMap mk xs))+-- >              (foldr (.+) Zero (map (postingAlg . mk) xs))+-- > sameMultiset (proj qs (postingAlg (foldMap mk xs)))+-- >              (foldr (.+) Zero [proj qs (postingAlg (mk x)) | x <- xs])+--+-- These laws use exact multiset equality without a numeric tolerance for+-- every 'HatBaseClass' instance. Complexity of 'postingAlg': O(1).+postingAlg :: Posting b -> Alg Double b+postingAlg (Posting algebra) = algebra++-- | Build one posting from a side, checked value, and base coordinates.+-- A zero value produces 'Zero' through '(.@)'. The side is embedded by+-- 'sideHat' and the coordinates are combined with 'merge'.+--+-- > postingAlg (entry side value part) == unPosted value .@ merge (sideHat side) part+--+-- The law holds with exact 'Alg' equality for every 'HatBaseClass' instance.+-- Complexity: O(1).+entry :: HatBaseClass b => PostSide -> Posted -> BasePart b -> Posting b+entry side value part = Posting (unPosted value .@ merge (sideHat side) part)

@@ -0,0 +1,277 @@+-- | Acceptance properties for explicit journal carryover.+module Journal.CarrySpec (runTests) where++import Control.Monad (unless)+import qualified Data.HashMap.Strict as HashMap+import qualified Data.Map.Strict as Map+import System.Exit (exitFailure)+import Test.QuickCheck++import ExchangeAlgebra.Algebra ((.@), foldEntries)+import ExchangeAlgebra.Algebra.Base+    ( AccountTitles(..)+    , CountUnit(..)+    , Hat(..)+    , HatBase(..)+    )+import ExchangeAlgebra.Journal (Journal, (.|))+import qualified ExchangeAlgebra.Journal as Journal+import ExchangeAlgebra.Journal.Transfer.Rule (carryBefore, carryEntries)+import ExchangeAlgebra.Journal.Exact (ExactSumError(..))++-- | Test postings use two base axes and integer note labels.+type Part = (CountUnit, AccountTitles)++-- | One scalar posting with its complete base coordinates.+type Row = (Int, Part, Hat, Double)++-- | The generated journal's concrete base has unit and account coordinates.+type TestJournal = Journal Int Double (HatBase Part)++-- | Include decimal values and the binary64 rounding boundary.+valueGen :: Gen Double+valueGen = elements [0.1, 0.2, 0.3, 1, 2, 2 ^ (53 :: Int), 2 ^ (53 :: Int) + 2]++-- | Vary selected notes, retained notes, sides, and complete bases.+rowsGen :: Gen [Row]+rowsGen = do+    count <- chooseInt (0, 18)+    vectorOf count $ do+        note <- elements [0, 1, 2, 3, 4, 9]+        unit <- elements [Yen, Dollar]+        account <- elements [Cash, Deposits, Products]+        side <- elements [Not, Hat]+        value <- valueGen+        pure (note, (unit, account), side, value)++-- | Retain the redundancy of each original scalar posting.+build :: [Row] -> TestJournal+build = foldMap (\(note, coordinates, side, value) ->+    (value .@ (side :< coordinates)) .| note)++-- | Extract individual scalar entries, including their original note.+rows :: TestJournal -> [Row]+rows journal = concatMap entries (HashMap.toList (Journal.toMap journal))+  where+    entries (note, algebra) = foldEntries+        (\previous value (side :< coordinates) ->+            (note, coordinates, side, value) : previous)+        []+        algebra++-- | Count repeated entries without relying on their storage order.+multiset :: Ord a => [a] -> Map.Map a Int+multiset = Map.fromListWith (+) . fmap (\entry -> (entry, 1))++-- | Compute exact signed balances directly from the scalar entries.+balances :: [Row] -> Map.Map Part Rational+balances = Map.fromListWith (+) . fmap contribution+  where+    contribution (_, coordinates, side, value) =+        (coordinates, case side of+            Not    -> toRational value+            Hat    -> negate (toRational value)+            HatNot -> error "CarrySpec: concrete-side invariant violated")++-- | Carry preserves retained scalars and rounds only each selected net.+propCarry :: Property+propCarry = forAll rowsGen $ \original ->+    case carryBefore (< 3) 9 (build original) of+      Left failure -> counterexample (show failure) False+      Right after  -> checkCarry original (rows after)++-- | Forgetting selected notes after adding carry entries matches replacement.+-- The carry note 9 is outside the selected notes 0, 1, and 2.+propCarryEntriesDecomposition :: Property+propCarryEntriesDecomposition = forAll rowsGen $ \original ->+    let journal = build original+        observed = do+            additions <- carryEntries (< 3) 9 journal+            pure (Journal.filterWithNote (\note _ -> note >= 3) (journal <> additions))+    in fmap (multiset . filter nonzero . rows) observed+        === fmap (multiset . filter nonzero . rows) (carryBefore (< 3) 9 journal)+  where+    nonzero (_, _, _, value) = value /= 0++-- | Each base's exact balance changes by the rounding of its selected net.+propCarryEntriesBalance :: Property+propCarryEntriesBalance = forAll rowsGen $ \original ->+    let journal = build original+        selectedBalances = balances+            (filter (\(note, _, _, _) -> note < 3) original)+        originalBalances = balances original+        observed = do+            additions <- carryEntries (< 3) 9 journal+            pure (balances (rows (journal <> additions)))+        check result = all (matches result) allCoordinates+        allCoordinates = Map.keys (Map.union originalBalances selectedBalances)+        matches result coordinates =+            let before = Map.findWithDefault 0 coordinates originalBalances+                after = Map.findWithDefault 0 coordinates result+                selected = Map.findWithDefault 0 coordinates selectedBalances+                rounded = toRational (fromRational selected :: Double)+            in after - before == rounded - selected+    in fmap check observed === Right True++-- | Compare exact balances and entry multisets after a successful carry.+checkCarry :: [Row] -> [Row] -> Property+checkCarry original observed =+    let retained = filter (\(note, _, _, _) -> note >= 3) original+        retainedCounts = multiset retained+        observedCounts = multiset observed+        originalBalances = balances original+        observedBalances = balances observed+        selectedBalances = balances+            (filter (\(note, _, _, _) -> note < 3) original)+        expectedCarried =+            [ (9, coordinates, netSide amount, fromRational (abs amount))+            | (coordinates, amount) <- Map.toAscList selectedBalances+            , amount /= 0+            ]+        allCoordinates = Map.keys (Map.unions+            [originalBalances, observedBalances, selectedBalances])+        retainedPresent = all (\(entry, count) ->+            Map.findWithDefault 0 entry observedCounts >= count)+            (Map.toList retainedCounts)+        otherRetained = filter (\(note, _, _, _) -> note /= 9) retained+        otherObserved = filter (\(note, _, _, _) -> note /= 9) observed+        roundedExactlyOnce coordinates =+            let beforeBalance = Map.findWithDefault 0 coordinates originalBalances+                afterBalance = Map.findWithDefault 0 coordinates observedBalances+                selectedBalance = Map.findWithDefault 0 coordinates selectedBalances+                roundedSelected = toRational (fromRational selectedBalance :: Double)+            in afterBalance - beforeBalance == roundedSelected - selectedBalance+        valid (_, _, side, value) =+            side /= HatNot && value > 0 && not (isNaN value) && not (isInfinite value)+    in conjoin+        [ multiset observed === multiset (retained ++ expectedCarried)+        , counterexample "retained scalar multiset" (property retainedPresent)+        , multiset otherObserved === multiset otherRetained+        , counterexample "carry difference is not the selected net's one rounding"+            (property (all roundedExactlyOnce allCoordinates))+        , counterexample "carry generated an invalid magnitude or side"+            (property (all valid observed))+        ]+  where+    netSide amount+        | amount > 0 = Not+        | otherwise  = Hat++-- | An exact cancellation adds nothing, even with an existing carry note.+propZeroAndExistingNote :: Property+propZeroAndExistingNote =+    let original =+            [ (0, (Yen, Cash), Not, 0.1)+            , (1, (Yen, Cash), Hat, 0.1)+            , (9, (Yen, Deposits), Not, 3)+            ]+        after = fmap rows (carryBefore (< 3) 9 (build original))+    in fmap multiset after === Right (multiset [(9, (Yen, Deposits), Not, 3)])++-- | An existing entry on the carry note and complete base is appended to.+propCarryNoteCollision :: Property+propCarryNoteCollision =+    let original =+            [ (0, (Yen, Cash), Not, 2)+            , (9, (Yen, Cash), Not, 2)+            , (0, (Dollar, Cash), Hat, 3)+            ]+        expected =+            [ (9, (Yen, Cash), Not, 2)+            , (9, (Yen, Cash), Not, 2)+            , (9, (Dollar, Cash), Hat, 3)+            ]+    in fmap (multiset . rows) (carryBefore (< 3) 9 (build original))+        === Right (multiset expected)++-- | Carry entries keep the existing carry-note entry and add a separate net.+propCarryEntriesCollision :: Property+propCarryEntriesCollision =+    let original =+            [ (0, (Yen, Cash), Not, 2)+            , (9, (Yen, Cash), Not, 2)+            ]+        expected =+            [ (0, (Yen, Cash), Hat, 2)+            , (9, (Yen, Cash), Not, 2)+            ]+    in fmap (multiset . rows) (carryEntries (< 3) 9 (build original))+        === Right (multiset expected)++-- | Both carry operations report the same checked aggregation failure.+propCarryEntriesFailureParity :: Property+propCarryEntriesFailureParity =+    let maximumFinite = encodeFloat (2 ^ (53 :: Int) - 1) 971 :: Double+        original = build+            [ (0, (Yen, Cash), Not, maximumFinite)+            , (1, (Yen, Cash), Not, maximumFinite)+            ]+        before = fmap (const ()) (carryBefore (< 3) 9 original)+        entries = fmap (const ()) (carryEntries (< 3) 9 original)+    in conjoin+        [ before === Left SumOutOfRange+        , entries === before+        ]++-- | Selection of every or no note follows the same exact balance contract.+propSelectionExtremes :: Property+propSelectionExtremes =+    let original =+            [ (0, (Yen, Cash), Not, 0.1)+            , (1, (Yen, Cash), Not, 0.2)+            , (9, (Dollar, Cash), Hat, 4)+            ]+        none = fmap (multiset . rows) (carryBefore (const False) 12 (build original))+        allEntries = fmap (multiset . rows) (carryBefore (const True) 12 (build original))+        expectedAll =+            [ (12, (Yen, Cash), Not, fromRational+                (toRational (0.1 :: Double) + toRational (0.2 :: Double)))+            , (12, (Dollar, Cash), Hat, 4)+            ]+    in conjoin+        [ none === Right (multiset original)+        , allEntries === Right (multiset expectedAll)+        ]++-- | A selected complete base whose exact side sum exceeds Double fails.+testOverflow :: IO ()+testOverflow = do+    let maximumFinite = encodeFloat (2 ^ (53 :: Int) - 1) 971 :: Double+        original =+            [ (0, (Yen, Cash), Not, maximumFinite)+            , (1, (Yen, Cash), Not, maximumFinite)+            ]+        carried = carryBefore (< 3) 9 (build original)+        additions = carryEntries (< 3) 9 (build original)+    unless (fmap (const ()) carried == fmap (const ()) additions) $+        failTest "carryEntries and carryBefore disagree on overflow"+    case carried of+        Left SumOutOfRange -> pure ()+        Left failure     -> failTest ("unexpected overflow error: " ++ show failure)+        Right _          -> failTest "overflowing selected side sum succeeded"++-- | Report a deterministic acceptance failure and stop the suite.+failTest :: String -> IO ()+failTest message = do+    putStrLn ("[FAIL] journal carry: " ++ message)+    exitFailure++-- | Run journal carry properties as part of the package test suite.+runTests :: IO ()+runTests = do+    quickProperty 500 "carry" propCarry+    quickProperty 500 "carry decomposition" propCarryEntriesDecomposition+    quickProperty 500 "carry balance" propCarryEntriesBalance+    quickProperty 1 "carry zero" propZeroAndExistingNote+    quickProperty 1 "carry collision" propCarryNoteCollision+    quickProperty 1 "carry entries collision" propCarryEntriesCollision+    quickProperty 1 "carry error parity" propCarryEntriesFailureParity+    quickProperty 1 "carry selection" propSelectionExtremes+    testOverflow+    putStrLn "[PASS] journal carry (retention, rounding, zero, and carry note)"++-- | Run one named QuickCheck property and fail on a counterexample.+quickProperty :: Testable property => Int -> String -> property -> IO ()+quickProperty count label proposition = do+    result <- quickCheckWithResult stdArgs { maxSuccess = count, chatty = False } proposition+    unless (isSuccess result) $ failTest (label ++ ": " ++ output result)

@@ -0,0 +1,28 @@+{-# OPTIONS_GHC -fdefer-type-errors -Wno-deferred-type-errors #-}++-- | Expressions that must fail when 'Posted' has no 'Num' instance.+module Posting.NoNumPosted+    ( literalPosted+    , addPosted+    , addPosting+    , genericPosted+    ) where++import ExchangeAlgebra.Posting (Posted, Posting)+import GHC.Generics (from)++-- | Demand an integer literal at the protected posting type.+literalPosted :: Posted+literalPosted = 1++-- | Demand arithmetic at the protected posting type.+addPosted :: Posted -> Posted+addPosted value = value + 1++-- | Demand arithmetic at the protected posting container type.+addPosting :: Posting b -> Posting b+addPosting value = value + 1++-- | Demand a Generic representation of the protected posting value.+genericPosted :: Posted -> ()+genericPosted value = from value `seq` ()

@@ -0,0 +1,338 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}++-- | Validation, serialization, and algebraic laws for checked ledger postings.+module Posting.PostingSpec (runTests) where++import Control.DeepSeq (force, rnf)+import Control.Exception (TypeError, evaluate, try)+import Control.Monad (unless)+import qualified Data.Binary as Binary+import Data.Hashable (hash)+import System.Exit (exitFailure)+import Test.QuickCheck hiding (label)+import ExchangeAlgebra.Algebra hiding (map, filter)+import qualified ExchangeAlgebra.Posting as Posting+import ExchangeAlgebra.Posting+    ( Posted+    , PostSide(..)+    , Posting+    , entry+    , posted+    , postedUpperBound+    , postingAlg+    , sideHat+    , unPosted+    )+import qualified Posting.NoNumPosted as NoNum++-- | Account and unit coordinates used for every algebraic property.+type TestBase = HatBase (AccountTitles, CountUnit)++-- | Values stay exact after all generated postings are added.+type TestEntry = (PostSide, Posted, BasePart TestBase)++-- | Generate accepted magnitudes across normal and subnormal exponents.+genAccepted :: Gen Double+genAccepted = frequency+    [ (1, pure 0)+    , (2, do+          significand <- chooseInteger (1, 2 ^ (52 :: Int) - 1)+          pure (encodeFloat significand (-1074)))+    , (7, do+          exponent <- chooseInt (-1022, 899)+          significand <- chooseInteger (2 ^ (52 :: Int), 2 ^ (53 :: Int) - 1)+          pure (encodeFloat significand (exponent - 52)))+    , (1, pure postedUpperBound)+    ]++-- | Smart-constructor identity throughout its accepted domain.+propAcceptedIdentity :: Property+propAcceptedIdentity = forAll genAccepted $ \value ->+    case posted value of+        Left failure  -> counterexample (show (value, failure)) False+        Right checked -> counterexample (show value) (unPosted checked == value)++-- | Every validated posting survives reading and revalidation.+propPostedRoundTrip :: Property+propPostedRoundTrip = forAll genAccepted $ \value ->+    case posted value of+        Left failure  -> counterexample (show failure) False+        Right checked -> posted (unPosted checked) === Right checked++-- | Generate checked integer amounts without floating-point rounding in sums.+genExactPosted :: Gen Posted+genExactPosted = do+    value <- chooseInteger (0, 1000)+    case posted (fromInteger value) of+        Right checked -> pure checked+        Left failure  -> error ("integer test amount rejected: " ++ show failure)++-- | Generate every concrete side and occasional wildcard coordinates.+genEntry :: Gen TestEntry+genEntry = do+    side <- elements [HatSide, NotSide]+    value <- genExactPosted+    title <- elements [Cash, Products, Sales, wildcard]+    unit <- elements [Yen, Amount, Dollar, wildcard]+    pure (side, value, (title, unit))++-- | Generate queries with empty, duplicate, overlapping, partial, and full cases.+genQueries :: Gen [TestBase]+genQueries = frequency+    [ (1, pure [])+    , (2, (: []) <$> genQuery)+    , (2, do+          query <- genQuery+          pure [query, query])+    , (2, do+          title <- elements [Cash, Products, Sales]+          pure [Hat :< (title, Yen), HatNot :< (title, wildcard)])+    , (2, do+          title <- elements [Cash, Products, Sales]+          unit <- elements [Yen, Amount, Dollar]+          pure [Not :< (title, unit)])+    , (1, pure [HatNot :< (wildcard, wildcard)])+    , (2, do+          count <- chooseInt (1, 4)+          vectorOf count genQuery)+    ]++-- | Sample every query hat and wildcard positions independently.+genQuery :: Gen TestBase+genQuery = do+    queryHat <- elements [Hat, Not, HatNot]+    title <- elements [Cash, Products, Sales, wildcard]+    unit <- elements [Yen, Amount, Dollar, wildcard]+    pure (queryHat :< (title, unit))++-- | Generate posting lists and queries without forcing every projection to match.+genAlgebraCase :: Gen ([TestEntry], [TestBase])+genAlgebraCase = do+    count <- chooseInt (0, 20)+    entries <- vectorOf count genEntry+    queries <- genQueries+    pure (entries, queries)++-- | Convert one checked entry through the public constructor.+single :: TestEntry -> Posting TestBase+single (side, value, part) = entry side value part++-- | Ignore only the internal sequence order, preserving each posting's value and base.+sameMultiset :: Alg Double TestBase -> Alg Double TestBase -> Bool+sameMultiset left right = toASCList left == toASCList right++-- | IX-8a: projection distributes across the checked posting list.+propProjection :: Property+propProjection = forAll genAlgebraCase $ \(entries, queries) ->+    let checked = postingAlg (foldMap single entries)+        raw = foldr (.+) Zero [postingAlg (single item) | item <- entries]+        projected = foldr (.+) Zero+            [proj queries (postingAlg (single item)) | item <- entries]+    in counterexample (show (entries, queries)) $+        sameMultiset checked raw && sameMultiset (proj queries checked) projected++-- | Checked concatenation has both identities and is associative in the algebra.+propMonoid :: Property+propMonoid = forAll genAlgebraCase $ \(entries, _) ->+    let (first, rest) = splitAt (length entries `div` 3) entries+        (second, third) = splitAt (length rest `div` 2) rest+        x = foldMap single first+        y = foldMap single second+        z = foldMap single third+        zero = mempty :: Posting TestBase+    in counterexample (show entries) $+        sameMultiset (postingAlg (zero <> x)) (postingAlg x)+        && sameMultiset (postingAlg (x <> zero)) (postingAlg x)+        && sameMultiset (postingAlg ((x <> y) <> z)) (postingAlg (x <> (y <> z)))++-- | Conversion preserves a single append with the algebra's structural equality.+propConversion :: Property+propConversion = forAll genAlgebraCase $ \(entries, _) ->+    let (leftEntries, rightEntries) = splitAt (length entries `div` 2) entries+        left = foldMap single leftEntries+        right = foldMap single rightEntries+    in counterexample (show entries) $+        postingAlg (left <> right) == (postingAlg left .+ postingAlg right)++-- | Fail an ordinary Boolean assertion through the same test harness.+assertTest :: String -> Bool -> IO ()+assertTest label success = unless success $ do+    putStrLn ("[FAIL] ledger posting: " ++ label)+    exitFailure++-- | Run a named QuickCheck property and fail the executable on a counterexample.+quickProperty :: Testable property => String -> property -> IO ()+quickProperty label proposition = do+    result <- quickCheckWithResult stdArgs { maxSuccess = 200, chatty = False } proposition+    unless (isSuccess result) $ do+        putStrLn ("[FAIL] " ++ label ++ ": " ++ output result)+        exitFailure+    putStrLn ("[PASS] " ++ label)++-- | Check every validation boundary, including negative zero normalization.+testValidation :: IO ()+testValidation = do+    let positiveInfinity = 1 / 0 :: Double+        negativeInfinity = -1 / 0 :: Double+        nanValue = 0 / 0 :: Double+        nextAboveBound = postedUpperBound * (1 + 2 ** (-52))+        smallestSubnormal = encodeFloat 1 (-1074) :: Double+    assertTest "NaN rejected" (posted nanValue == Left Posting.NonFinite)+    assertTest "positive Infinity rejected" $+        posted positiveInfinity == Left Posting.NonFinite+    assertTest "negative Infinity rejected" $+        posted negativeInfinity == Left Posting.NonFinite+    assertTest "negative finite value rejected" $+        posted (-1e-300) == Left Posting.Negative+    assertTest "next representable value above bound rejected" $+        posted nextAboveBound == Left Posting.AboveBound+    assertTest "2^1000 rejected" (posted (2 ** 1000) == Left Posting.AboveBound)+    assertTest "zero accepted" (fmap unPosted (posted 0) == Right 0)+    assertTest "negative zero normalized" $ case posted (-0.0) of+        Right checked -> isPositiveZero (unPosted checked)+        Left _        -> False+    assertTest "smallest subnormal accepted" $+        fmap unPosted (posted smallestSubnormal) == Right smallestSubnormal+    assertTest "one accepted" (fmap unPosted (posted 1) == Right 1)+    assertTest "upper bound accepted" $+        fmap unPosted (posted postedUpperBound) == Right postedUpperBound+  where+    isPositiveZero value = value == 0 && isInfinite (1 / value) && 1 / value > 0++-- | Binary instances round-trip valid values and reject invalid Posted bytes.+testBinary :: IO ()+testBinary = do+    let smallestSubnormal = encodeFloat 1 (-1074) :: Double+        checkedValues =+            [value | Right value <- map posted [0, smallestSubnormal, 1, postedUpperBound]]+        sides = [HatSide, NotSide]+        rejects value = case Binary.decodeOrFail (Binary.encode (value :: Double)) of+            Left _                      -> True+            Right (_, _, (_ :: Posted)) -> False+        decodedNegativeZero = Binary.decodeOrFail (Binary.encode (-0.0 :: Double))+    assertTest "Posted Binary round trip" $+        all (\value -> Binary.decode (Binary.encode value) == value) checkedValues+    assertTest "PostSide Binary round trip" $+        all (\side -> Binary.decode (Binary.encode side) == side) sides+    assertTest "Posted Binary decoder validates" $+        all rejects+            [ 0 / 0+            , 1 / 0+            , -1 / 0+            , -1e-300+            , postedUpperBound * (1 + 2 ** (-52))+            , 2 ** 1000+            ]+    assertTest "Posted Binary normalizes negative zero" $ case decodedNegativeZero of+        Left _                          -> False+        Right (_, _, (value :: Posted)) ->+            unPosted value == 0 && 1 / unPosted value > 0+    assertTest "NFData and Hashable instances" $+        force checkedValues `seq` force sides `seq`+        sum (map hash checkedValues) `seq` sum (map hash sides) `seq` True+    assertTest "base component NFData instances" $+        rnf (Cash :: AccountTitles) `seq`+        rnf (Yen :: CountUnit) `seq`+        rnf (AxisKey Cash) `seq`+        rnf (Hat :: Hat) `seq`+        rnf (BaseForSingleHat :: BaseForSingleHat) `seq`+        rnf (PS :: PIMO) `seq`+        rnf (Assets :: AccountDivision) `seq`+        rnf (Credit :: Side) `seq`+        rnf (Current :: FixedCurrent) `seq`+        rnf (CloseByDivision :: ClosingRule) `seq`+        rnf (ContraAccount :: AccountRole) `seq`+        rnf (OrdinaryPosting :: PostingCapability) `seq`+        rnf (StatementDivision Assets :: DivisionSemantics) `seq`+        rnf (FixedHomeSide Credit :: HomeSideSemantics) `seq`+        rnf (StatementEligible :: ReportingEligibility) `seq`+        rnf (Not :< (Yen, Cash) :: HatBase (CountUnit, AccountTitles)) `seq`+        True++-- | Both posting sides map to concrete Hat values only.+testSides :: IO ()+testSides = do+    assertTest "HatSide maps to Hat" (sideHat HatSide == Hat)+    assertTest "NotSide maps to Not" (sideHat NotSide == Not)+    assertTest "PostSide excludes HatNot" $+        all ((/= HatNot) . sideHat) [minBound .. maxBound]++-- | Three equal-base entries expose structural ordering without breaking the multiset law.+testAssociativityRegression :: IO ()+testAssociativityRegression = case traverse posted [1, 2, 3] of+    Left failure                 -> do+        putStrLn ("[FAIL] ledger posting fixture: " ++ show failure)+        exitFailure+    Right [first, second, third] -> do+        let part = (Cash, Yen)+            x = entry HatSide first part :: Posting TestBase+            y = entry HatSide second part :: Posting TestBase+            z = entry HatSide third part :: Posting TestBase+            left = postingAlg ((x <> y) <> z)+            right = postingAlg (x <> (y <> z))+        assertTest "equal-base grouping changes structural order" (left /= right)+        assertTest "equal-base grouping preserves the multiset" (sameMultiset left right)+    Right _                      -> assertTest "three checked fixture values" False++-- | Fixed queries cover each Hat value and both coordinate wildcard positions.+testQueryCoverage :: IO ()+testQueryCoverage = case posted 3 of+    Left failure -> do+        putStrLn ("[FAIL] ledger posting fixture: " ++ show failure)+        exitFailure+    Right value  -> do+        let entries =+                [ (HatSide, value, (Cash, Yen))+                , (NotSide, value, (Products, Amount))+                , (HatSide, value, (Sales, Dollar))+                ]+            queries =+                [ Hat :< (Cash, wildcard)+                , Not :< (wildcard, Amount)+                , HatNot :< (Sales, wildcard)+                ]+            checked = postingAlg (foldMap single entries)+            projected = foldr (.+) Zero+                [proj queries (postingAlg (single item)) | item <- entries]+        assertTest "three query hats and coordinate wildcards" $+            sameMultiset (proj queries checked) projected++-- | Deferred errors prove that clients cannot request Num for Posted.+testNoNum :: IO ()+testNoNum = do+    literal <- try (evaluate NoNum.literalPosted) :: IO (Either TypeError Posted)+    assertTest "Posted numeric literal is rejected" (isTypeError literal)+    case posted 1 of+        Left failure  -> do+            putStrLn ("[FAIL] ledger posting fixture: " ++ show failure)+            exitFailure+        Right checked -> do+            arithmetic <- try (evaluate (NoNum.addPosted checked))+                :: IO (Either TypeError Posted)+            assertTest "Posted arithmetic is rejected" (isTypeError arithmetic)+            generic <- try (evaluate (NoNum.genericPosted checked))+                :: IO (Either TypeError ())+            assertTest "Posted Generic is rejected" (isTypeError generic)+            container <- try (evaluate (NoNum.addPosting (mempty :: Posting TestBase)))+                :: IO (Either TypeError (Posting TestBase))+            assertTest "Posting arithmetic is rejected" (isTypeError container)+  where+    isTypeError (Left _) = True+    isTypeError (Right _) = False++-- | Register checked-posting tests with ExchangeAlgebra-test.+runTests :: IO ()+runTests = do+    testValidation+    testBinary+    testSides+    testAssociativityRegression+    testQueryCoverage+    testNoNum+    quickProperty "V-1 accepted-domain identity" propAcceptedIdentity+    quickProperty "validated posting round trip" propPostedRoundTrip+    quickProperty "IX-8a projection and raw conversion" propProjection+    quickProperty "Posting monoid laws" propMonoid+    quickProperty "Posting conversion preserves structural append" propConversion+    putStrLn "[PASS] checked ledger posting"

@@ -0,0 +1,189 @@+{-# LANGUAGE ScopedTypeVariables #-}++-- | Ordered settlement pairs preserve source nets and exact accounting balance.+module Posting.SettleSpec (runTests) where++import Control.Monad (forM_, unless)+import Data.List (foldl', sort)+import qualified Data.Map.Strict as Map+import System.Exit (exitFailure)+import Test.QuickCheck hiding (label)++import ExchangeAlgebra.Algebra hiding (filter, map)+import ExchangeAlgebra.Algebra.Transfer.Rule++-- | Two coordinates exercise complete-base ordering and axis preservation.+type TestBase = HatBase (CountUnit, AccountTitles)++-- | Signed input amounts indexed by complete base coordinates.+type Nets = Map.Map (CountUnit, AccountTitles) Double++-- | Cover zero, both signs, fractions, subnormals, and amounts above Posted.+genNet :: Gen Double+genNet = do+    magnitude <- frequency+        [ (3, elements [0, 0.1, 0.2, 1, 2 ^ (53 :: Int), 2 ^ (950 :: Int)+                       , encodeFloat 1 (-1074), encodeFloat (2 ^ (53 :: Int) - 1) 971])+        , (2, do+              significand <- chooseInteger (1, 2 ^ (53 :: Int) - 1)+              exponent <- chooseInt (-1074, 971)+              pure (encodeFloat significand exponent))+        ]+    sign <- elements [1, -1]+    pure (sign * magnitude)++-- | Include closing, non-closing, and destination accounts on several units.+genNets :: Gen Nets+genNets = do+    count <- chooseInt (0, 30)+    entries <- vectorOf count $ do+        unit <- elements [Yen, Dollar, Amount]+        title <- elements [Sales, Purchases, Depreciation, Cash, RetainedEarnings, NetIncome]+        amount <- genNet+        pure ((unit, title), amount)+    pure (Map.fromList entries)++-- | Read scalar entries without cancellation or approximate comparisons.+scalars :: Alg Double TestBase -> [(Double, TestBase)]+scalars = foldEntries (\previous value postingBase -> (value, postingBase) : previous) []++-- | The exact signed net at one complete base.+netAt :: (CountUnit, AccountTitles) -> Alg Double TestBase -> Rational+netAt coordinates = foldEntries add 0+  where+    add total value postingBase+        | base postingBase /= coordinates = total+        | hat postingBase == Not = total + toRational value+        | otherwise = total - toRational value++-- | Sum magnitudes as rationals rather than through floating-point norm.+exactMagnitude :: Alg Double TestBase -> Rational+exactMagnitude = foldEntries (\total value _ -> total + toRational value) 0++-- | The key set, pair structure, signs, and debit/credit equality hold exactly.+propSettlement :: Property+propSettlement = forAll genNets $ \amounts ->+    case settleEntries retainedEarningsRule amounts of+      Left failure -> counterexample (show failure) False+      Right batch -> checkSettlement amounts (settlementSteps batch)++-- | Check each generated pair with exact Rational accounting readouts.+checkSettlement :: Nets -> [((CountUnit, AccountTitles), Alg Double TestBase)] -> Property+checkSettlement amounts steps =+    let expectedKeys = Map.keys (Map.filterWithKey eligible amounts)+        keys = map fst steps+        checkPair (coordinates@(unit, title), algebra) =+            let amount = Map.findWithDefault 0 coordinates amounts+                sourceSide = sideFor amount+                reverseSide = revHat sourceSide+                targetSide = case closingSide title of+                    Just ClosingKeep -> sourceSide+                    _                -> reverseSide+                expected = sort+                    [ (abs amount, reverseSide :< coordinates)+                    , (abs amount, targetSide :< (unit, RetainedEarnings))+                    ]+                valid (value, postingBase) =+                    value >= 0 && not (isNaN value || isInfinite value)+                    && hat postingBase /= HatNot+            in conjoin+                [ sort (scalars algebra) === expected+                , length (scalars algebra) === 2+                , netAt coordinates algebra + toRational amount === 0+                , exactMagnitude (decL algebra) === exactMagnitude (decR algebra)+                , property (all valid (scalars algebra))+                ]+    in conjoin+        [ keys === expectedKeys+        , property (and (zipWith (<) keys (drop 1 keys)))+        , conjoin (map checkPair steps)+        ]+  where+    eligible (_, title) amount = amount /= 0 && title /= RetainedEarnings+        && closingSide title /= Nothing+    sideFor amount+        | amount > 0 = Not+        | otherwise  = Hat++-- | Report fixed regression failures through the ordinary test executable.+assertTest :: String -> Bool -> IO ()+assertTest label success = unless success $ do+    putStrLn ("[FAIL] settlement: " ++ label)+    exitFailure++-- | Exclusion, both directions, and large finite magnitudes are deterministic.+testFixed :: IO ()+testFixed = do+    let steps amounts = fmap settlementSteps+            (settleEntries retainedEarningsRule amounts ::+                Either (SettleError TestBase) (SettlementBatch TestBase))+        excluded = Map.fromList+            [ ((Yen, Sales), 0)+            , ((Dollar, Purchases), -0.0)+            , ((Yen, Cash), 10)+            , ((Yen, RetainedEarnings), 12)+            , ((Yen, NetIncome), 5)+            ]+    assertTest "empty input" (fmap null (steps Map.empty) == Right True)+    assertTest "only excluded keys" (fmap null (steps excluded) == Right True)+    assertTest "known keep and flip accounts" $+        closingSide Sales == Just ClosingKeep && closingSide Purchases == Just ClosingFlip+    forM_ [Sales, Purchases] $ \title ->+        forM_ [1, -1] $ \sign -> do+            let magnitude = 2 ^ (950 :: Int)+                amount = sign * magnitude+                coordinates = (Yen, title)+                result = steps (Map.singleton coordinates amount)+            assertTest "finite 2^950 accepted without Posted validation" $+                case result of+                    Right [(source, algebra)] -> source == coordinates+                        && length (scalars algebra) == 2+                        && all ((== magnitude) . fst) (scalars algebra)+                        && netAt source algebra == negate (toRational amount)+                        && exactMagnitude (decL algebra) == exactMagnitude (decR algebra)+                    _                         -> False+    -- Select three ClosingKeep accounts by their actual key order so the+    -- destination increments are T, 1, -T, independent of enum ordering.+    let titles = take 3 [title | title <- [minBound .. maxBound]+                             , closingSide title == Just ClosingKeep]+        sourceKeys = sort [(Yen, title) | title <- titles]+        large = 2 ^ (53 :: Int)+        result = steps (Map.fromList (zip sourceKeys [large, 1, -large]))+        increments = fmap+            (map (\(_, algebra) ->+                fromRational (netAt (Yen, RetainedEarnings) algebra) :: Double))+            result+    assertTest "three distinct keep accounts in fixture" (length sourceKeys == 3)+    assertTest "sequential destination increments preserve source order" $+        increments == Right [large, 1, -large]+        && fmap (foldl' (+) 0) increments == Right 0+        && foldl' (+) 0 [large, -large, 1] == 1++-- | All input keys obey the finite-input contract, even excluded accounts.+testNonFinite :: IO ()+testNonFinite = forM_ [0 / 0, 1 / 0, -1 / 0] $ \amount ->+    forM_ [Sales, Cash, RetainedEarnings] $ \title -> do+        let first = (Dollar, title)+            second = (Yen, Sales)+            result = settleEntries retainedEarningsRule+                (Map.fromList [(second, amount), (first, amount)])+                :: Either (SettleError TestBase) (SettlementBatch TestBase)+        assertTest "first non-finite key, including excluded keys" $ case result of+            Left (NonFiniteNet coordinates) -> coordinates == min first second+            Right _                          -> False+        assertTest "excluded non-finite key alone is rejected" $ case+            (settleEntries retainedEarningsRule (Map.singleton (Dollar, Cash) amount)+                :: Either (SettleError TestBase) (SettlementBatch TestBase)) of+            Left (NonFiniteNet coordinates) -> coordinates == (Dollar, Cash)+            Right _                          -> False++-- | Run generated laws and boundary regressions with the main test suite.+runTests :: IO ()+runTests = do+    testFixed+    testNonFinite+    result <- quickCheckWithResult stdArgs { maxSuccess = 500, chatty = False } propSettlement+    unless (isSuccess result) $ do+        putStrLn ("[FAIL] settlement properties: " ++ output result)+        exitFailure+    putStrLn "[PASS] settlement (order, keys, exact pairs, sides, axes, bounds, and errors)"

@@ -76,6 +76,9 @@ import qualified Transfer.RuleSpec as TransferRuleSpec import qualified Algebra.ProjWildcardSpec as ProjWildcardSpec import qualified Algebra.ExactSumSpec as ExactSumSpec+import qualified Posting.PostingSpec as PostingSpec+import qualified Posting.SettleSpec as SettleSpec+import qualified Journal.CarrySpec as CarrySpec import           Numeric             (showHex) import           Control.Monad       (forM_) import           Control.Monad.ST@@ -6969,6 +6972,9 @@     ExactSumSpec.runTests     TransferRuleSpec.runTests     ProjWildcardSpec.runTests+    PostingSpec.runTests+    SettleSpec.runTests+    CarrySpec.runTests     testAccountTitlesBinary     testPracticalAndManufacturingAccountTitles     testAccountTitleClassification

@@ -369,6 +369,99 @@     assertTest "closing target postings are not aggregated" $         length (vals retained) == 4 && all (not . isErrorValue) (vals retained) +-- | Two goods share an owner and differ only in the axis collapsed below.+data ValuationGood = GoodA | GoodB | AnyValuationGood+    deriving (Eq, Ord, Show, Generic)++instance Hashable ValuationGood++instance Element ValuationGood where+    wildcard = AnyValuationGood++type ValuationBase = HatBase (AccountTitles, ValuationGood, Owner, CountUnit)++-- | Retain the raw count in its own axes, then net the value across goods.+testValuationCollapse :: IO ()+testValuationCollapse = do+    let source good = Not :< (Products, good, Alice, Amount)+        target good = Not :< (Products, good, Alice, Yen)+        ledger = 5 .@ source GoodA .+ 3 .@ source GoodB+            :: Alg MoneyDecimal ValuationBase+        patternBase = Not :< (Products, wildcard, Alice, Yen)+        dropGood (title, _, owner, unit) = (title, wildcard, owner, unit)+        expected = Not :< (Products, wildcard, Alice, Yen)+    rules <- requireRight "valuation rules" $+        mkTransferRules [scaleBy (source GoodA) (target GoodA) 2,+                         scaleBy (source GoodB) (target GoodB) 10]+    valuationEntries <- requireRight "valuation transfer" (transferEntries rules ledger)+    let valued = ledger .+ valuationEntries+        collapsed = bar (valued .+ collapseNetEntries [patternBase] dropGood valued)+    assertTest "valuation of two goods becomes one 40 posting" $+        rawObservation collapsed == Map.singleton expected 40+        && length (vals collapsed) == 1++-- | Opposite sides cancel only after their good coordinates coincide.+testRetainedCollapse :: IO ()+testRetainedCollapse = do+    let source good side = side :< (RetainedEarnings, good, Alice, Yen)+        ledger = 10 .@ source GoodA Not .+ 4 .@ source GoodB Hat+            :: Alg MoneyDecimal ValuationBase+        patternBase = HatNot :< (RetainedEarnings, wildcard, Alice, Yen)+        dropGood (title, _, owner, unit) = (title, wildcard, owner, unit)+        expected = source AnyValuationGood Not+        collapsed = bar (ledger .+ collapseNetEntries [patternBase] dropGood ledger)+    assertTest "retained earnings net to one Not 6 posting" $+        rawObservation collapsed == Map.singleton expected 6+        && length (vals collapsed) == 1++-- | Exact values expose count, norm, non-negativity and net equivalence.+propCollapse :: Property+propCollapse = forAll genLedger $ \ledger ->+    let patterns = [HatNot :< (Cash, wildcard)]+        dropUnit (title, _) = (title, wildcard)+        selected = proj patterns ledger+        raw = collapseEntries patterns dropUnit ledger+        net = collapseNetEntries patterns dropUnit ledger+    in counterexample (show (rawObservation raw, rawObservation net)) $+        property (bar (ledger .+ raw) == bar (ledger .+ net)+            && norm raw == 2 * norm selected+            && all (>= 0) (vals raw ++ vals net)+            && length (vals raw) == 2 * length (vals selected))+  where+    genLedger = do+        count <- chooseInt (0, 30)+        postings <- vectorOf count $ do+            value <- chooseInteger (1, 100)+            side <- elements [Hat, Not]+            title <- elements [Cash, Products]+            unit <- elements [Yen, Amount, wildcard]+            pure (fromInteger value .@ side :< (title, unit))+        pure (Algebra.fromList postings :: Alg MoneyDecimal TestBase)++-- | Ledger wildcards remain literal in transfer matching and closing output.+testWildcardLedger :: IO ()+testWildcardLedger = do+    let source = Not :< (Sales, wildcard)+        ledger = 7 .@ source :: Alg MoneyDecimal TestBase+        target = Not :< (Deposits, wildcard)+    concrete <- requireRight "concrete source rule" $+        mkTransferRules [relabel (Not :< (Sales, Yen)) target]+    concreteEntries <- requireRight "concrete source application" $+        transferEntries concrete ledger+    assertTest "concrete source does not match ledger wildcard" $+        Algebra.isZero concreteEntries+    wildcardRule <- requireRight "wildcard source rule" $+        mkTransferRules [relabel source target]+    wildcardEntries <- requireRight "wildcard source application" $+        transferEntries wildcardRule ledger+    assertTest "wildcard source matches ledger wildcard" $+        rawObservation wildcardEntries == rawObservation+            (7 .@ revHat source .+ 7 .@ target)+    closed <- requireRight "wildcard ledger closing" (closingEntries ledger)+    assertTest "closing retains wildcard axis on earnings" $+        rawObservation closed == rawObservation+            (7 .@ revHat source .+ 7 .@ Not :< (RetainedEarnings, wildcard))+ -- | A good axis owned only by this acceptance fixture. data Good     = Widget@@ -466,10 +559,14 @@     quickProperty "L4 canonical rules" propCanonical     quickProperty "L5 Double" (propNonnegative (Proxy :: Proxy Double))     quickProperty "L5 MoneyDecimal" (propNonnegative (Proxy :: Proxy MoneyDecimal))+    quickProperty "L6 collapse" propCollapse     testValidation     testLegacyMiss     testApplication     testClosing     testClosingOverflow+    testValuationCollapse+    testRetainedCollapse+    testWildcardLedger     testAcceptance     putStrLn "[PASS] transfer rule regressions and two-period acceptance"