core: fix ledger month boundary drift

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

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.

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