From f284120410b0cc0800e50a01bf213ef76fce37ef Mon Sep 17 00:00:00 2001 From: shum Date: Mon, 24 Aug 2026 10:48:20 +0000 Subject: [PATCH] core: fix ledger month boundary drift --- .../src/BadgeService/Ledger.hs | 18 ++++- src/Simplex/Chat/Badges/Months.hs | 25 ++++--- tests/Bots/BadgeLedgerTests.hs | 66 +++++++++++++++++-- 3 files changed, 87 insertions(+), 22 deletions(-) diff --git a/apps/simplex-badge-service/src/BadgeService/Ledger.hs b/apps/simplex-badge-service/src/BadgeService/Ledger.hs index 3838a6bccd..699a5358e6 100644 --- a/apps/simplex-badge-service/src/BadgeService/Ledger.hs +++ b/apps/simplex-badge-service/src/BadgeService/Ledger.hs @@ -33,10 +33,16 @@ data LedgerState = LedgerState -- @k = min balanceMonths (fullMonthsBetween balanceStartTs t)@: capped at the balance so a long -- absence on a small or zero balance can never lapse more months than are actually owed. Returns -- 'Nothing' (state unchanged) when @k@ would be 0 — never 'Just (0, _)'. +-- +-- The new 'balanceStartTs' is reached by stepping 'addMonths' 1 forward @k@ times, not by a +-- direct @addMonths k@ jump: 'fullMonthsBetween' counts months the same iterated way (see its +-- Haddock), and 'issue' always advances one month at a time, so all three must agree on the same +-- stepwise sequence or a boundary computed here can land past where 'issue' would place it, +-- letting a re-'issue' at the same instant slip through the guard below. advance :: UTCTime -> LedgerState -> Maybe (Int, LedgerState) advance t st@LedgerState {balanceMonths, balanceStartTs} | k <= 0 = Nothing - | otherwise = Just (k, st {balanceMonths = balanceMonths - k, balanceStartTs = addMonths k balanceStartTs}) + | otherwise = Just (k, st {balanceMonths = balanceMonths - k, balanceStartTs = iterate (addMonths 1) balanceStartTs !! k}) where k = min balanceMonths (fullMonthsBetween balanceStartTs t) @@ -55,8 +61,14 @@ debitAll _reason st = st {balanceMonths = 0} -- | @consume@: issues a credential for @[balanceStartTs, addMonths 1 balanceStartTs)@, debiting -- one month. 'Nothing' when @balanceMonths == 0@ (nothing to issue) or when the current month is --- already issued (@balanceStartTs > t@ — 'balanceStartTs' only reaches the next period's start --- once this one has been consumed); the caller tells the two apart by the balance. +-- already issued (@balanceStartTs > t@); the caller tells the two apart by the balance. +-- +-- This guard only works because 'advance' steps to the same month boundaries 'issue' does (see +-- 'advance''s Haddock): whenever 'advance' is not capped by a low balance, its resulting +-- @balanceStartTs@ is @<= t@ and the /next/ boundary after it is @> t@ by construction, so the +-- 'issue' that follows always leaves @balanceStartTs' > t@ — a second 'issue' at the same @t@ is +-- correctly rejected. A freshly 'credit'ed balance sets @balanceStartTs == t@ exactly, which must +-- stay issuable, so this guard is strictly @>@, never @>=@. issue :: UTCTime -> LedgerState -> Maybe (LedgerState, UTCTime, UTCTime) issue t st@LedgerState {balanceMonths, balanceStartTs} | balanceMonths == 0 = Nothing diff --git a/src/Simplex/Chat/Badges/Months.hs b/src/Simplex/Chat/Badges/Months.hs index bae1ce7a2b..d597a1c05c 100644 --- a/src/Simplex/Chat/Badges/Months.hs +++ b/src/Simplex/Chat/Badges/Months.hs @@ -8,7 +8,7 @@ module Simplex.Chat.Badges.Months ) where -import Data.Time.Calendar (addDays, addGregorianMonthsClip, toGregorian) +import Data.Time.Calendar (addDays, addGregorianMonthsClip) import Data.Time.Calendar.WeekDate (toWeekDate) import Data.Time.Clock (UTCTime (..), secondsToDiffTime) @@ -17,21 +17,18 @@ import Data.Time.Clock (UTCTime (..), secondsToDiffTime) addMonths :: Int -> UTCTime -> UTCTime addMonths n (UTCTime day tod) = UTCTime (addGregorianMonthsClip (fromIntegral n) day) tod --- | The largest @m >= 0@ with @addMonths m start <= t@. Returns 0 when @t < start@. +-- | The largest @m >= 0@ with the @m@-times-iterated one-month step from @start@ landing at or +-- before @t@. Returns 0 when @t < start@. -- --- 'addMonths' is monotonic and moves to a new calendar month on every step, so the plain --- year/month difference between @start@ and @t@ is never more than one month away from the --- answer; at most one correction step is needed either way. +-- This deliberately steps one month at a time via 'addMonths' 1, rather than jumping straight to +-- @addMonths m start@ for a candidate @m@: 'addMonths' is /not/ additive under clamping (a Feb +-- clamp encountered partway through a multi-month span permanently lowers the day-of-month for +-- every later step), so a direct @m@-month jump from @start@ can land on a different date than +-- @m@ single-month steps chained through the same intermediate clamps. That divergence is +-- path-dependent, so there is no O(1) closed form here — the only way to agree with 'issue' +-- (which always advances one month at a time) is to step the same way. fullMonthsBetween :: UTCTime -> UTCTime -> Int -fullMonthsBetween start t - | t < start = 0 - | addMonths (approx + 1) start <= t = approx + 1 - | addMonths approx start > t = approx - 1 - | otherwise = approx - where - (sy, sm, _) = toGregorian (utctDay start) - (ty, tm, _) = toGregorian (utctDay t) - approx = fromInteger (ty - sy) * 12 + (tm - sm) +fullMonthsBetween start t = length (takeWhile (<= t) (drop 1 (iterate (addMonths 1) start))) -- | 23:59:59 UTC of the next Sunday strictly after @t@. A @t@ that already falls on a Sunday -- yields the following Sunday (7 days later), never the same day. diff --git a/tests/Bots/BadgeLedgerTests.hs b/tests/Bots/BadgeLedgerTests.hs index a8c84400bf..e32d7ac26d 100644 --- a/tests/Bots/BadgeLedgerTests.hs +++ b/tests/Bots/BadgeLedgerTests.hs @@ -31,10 +31,18 @@ badgeLedgerTests = modifyMaxSuccess (const 500) $ do prop "re-running issue inside an already-issued period appends nothing (property 4)" prop_issueIdempotentWithinPeriod prop "advance lapses only fully elapsed, unissued months (property 5)" prop_advanceOnlyFullyElapsed it "reproduces the worked example: buy 3 months, app off a month, reissue (property 6)" testWorkedExample + it "does not double-issue when a Feb clamp puts balanceStartTs exactly on t (property 4 regression, seeds 6/7)" testFebClampRegression noon :: DiffTime noon = secondsToDiffTime (12 * 3600) +-- | Independent oracle for "n months forward, stepping one month at a time": the ledger's own +-- month-boundary definition (see 'fullMonthsBetween' and 'advance' in BadgeService.Ledger), used +-- here instead of a direct @addMonths n@ jump because the two disagree once a Feb clamp falls +-- partway through the span (regression for the property-4 counterexample below). +iterAddMonths :: Int -> UTCTime -> UTCTime +iterAddMonths n t0 = iterate (addMonths 1) t0 !! n + endOfDay :: DiffTime endOfDay = secondsToDiffTime (23 * 3600 + 59 * 60 + 59) @@ -50,11 +58,28 @@ genDebitType :: Gen StatementDebitType genDebitType = elements [SDRefund, SDBadge, SDLapse, SDSupport] genTime :: Gen UTCTime -genTime = do +genTime = oneof [genUniformTime, genClampProneTime] + +genUniformTime :: Gen UTCTime +genUniformTime = do dayOffset <- chooseInt (0, 3000) secOfDay <- chooseInt (0, 86399) pure $ UTCTime (addDays (toInteger dayOffset) (fromGregorian 2020 1 1)) (secondsToDiffTime (toInteger secOfDay)) +-- | Dates on the 28th-31st of a month, the only days where 'addMonths' can clamp. Direct-jump vs. +-- iterated-step boundary computations only diverge when a clamp falls partway through a span, so +-- a uniformly-random day-of-month (as in 'genUniformTime') samples that region far too thinly — +-- the property-4 regression below needed 493 QuickCheck cases to surface it. Picking the +-- day-of-month explicitly from the clamp-prone range, with month/year otherwise random, makes +-- every generated history exercise that region directly instead of by chance. +genClampProneTime :: Gen UTCTime +genClampProneTime = do + year <- chooseInt (2020, 2028) + month <- chooseInt (1, 12) + day <- elements [28, 29, 30, 31] + secOfDay <- chooseInt (0, 86399) + pure $ UTCTime (fromGregorian (toInteger year) month day) (secondsToDiffTime (toInteger secOfDay)) + genLedgerState :: Gen LedgerState genLedgerState = do months <- chooseInt (0, 36) @@ -138,7 +163,7 @@ verifyRow :: Row -> Bool verifyRow (Row kind t prev next) = case kind of EKLapse k -> balanceMonths next == balanceMonths prev - k - && balanceStartTs next == addMonths k (balanceStartTs prev) + && balanceStartTs next == iterAddMonths k (balanceStartTs prev) && balanceBadgeType next == balanceBadgeType prev EKCredit n -> balanceMonths next == balanceMonths prev + n @@ -207,9 +232,9 @@ prop_advanceOnlyFullyElapsed = forAll genStateAndTime $ \(st, t) -> case advance property $ k > 0 && k <= balanceMonths st - && addMonths k (balanceStartTs st) <= t - && (k == balanceMonths st || addMonths (k + 1) (balanceStartTs st) > t) - && balanceStartTs st' == addMonths k (balanceStartTs st) + && iterAddMonths k (balanceStartTs st) <= t + && (k == balanceMonths st || iterAddMonths (k + 1) (balanceStartTs st) > t) + && balanceStartTs st' == iterAddMonths k (balanceStartTs st) && balanceMonths st' == balanceMonths st - k genSunday :: Gen UTCTime @@ -263,3 +288,34 @@ testWorkedExample = do periodStart4 `shouldBe` mayTen periodEnd4 `shouldBe` junTen sundayAfter periodEnd4 `shouldBe` UTCTime (fromGregorian 2026 6 14) endOfDay + +-- | Exact counterexample from the property-4 falsification (QuickCheck seeds 6 and 7, 493 tests +-- in): a direct 11-month jump from Apr 29, 2020 overshoots Mar 28, 2021 by a day (it lands on Mar +-- 29), while the true, iterated 11th month boundary (stepping through the Feb 2021 clamp) lands +-- exactly on Mar 28. The old 'fullMonthsBetween' picked 10 months via its overshoot-correction +-- check, leaving 'advance' at Feb 28, and 'issue' then walked one more month to land its new +-- 'balanceStartTs' exactly on @t@ — which the old @balanceStartTs > t@ guard failed to reject on +-- a same-instant re-issue, so a second 'issue' fired and silently debited a month nobody paid +-- for. This pins the fix: 'fullMonthsBetween' must count the same 11 months 'advance' resolves +-- to, and the second 'issue' at the same @t@ must be rejected. +testFebClampRegression :: IO () +testFebClampRegression = do + let start = UTCTime (fromGregorian 2020 4 29) (secondsToDiffTime (15 * 3600 + 16 * 60 + 21)) + t = UTCTime (fromGregorian 2021 3 28) (secondsToDiffTime (15 * 3600 + 16 * 60 + 21)) + st0 = LedgerState {balanceMonths = 18, balanceStartTs = start, balanceBadgeType = BTInvestor} + -- advance resolves 11 fully elapsed months (not 10): the direct jump and the iterated boundary + -- must agree, and here the iterated boundary lands exactly on t. + Just (lapsed, st1) <- pure (advance t st0) + lapsed `shouldBe` 11 + balanceStartTs st1 `shouldBe` t + balanceMonths st1 `shouldBe` 7 + -- issuing at t is legitimate: balanceStartTs == t, the boundary was just reached, not consumed. + Just (st2, periodStart, periodEnd) <- pure (issue t st1) + periodStart `shouldBe` t + balanceStartTs st2 `shouldBe` periodEnd + balanceStartTs st2 `shouldSatisfy` (> t) + -- re-running advance-then-issue at the same t must now append nothing: no further lapse (the + -- new start is already past t)... + advance t st2 `shouldBe` Nothing + -- ...and no second issuance. + issue t st2 `shouldBe` Nothing