I began my investigation on a rainy Monday morning...

This commit reworks the "preservation of ADA" test to more accurately
reflect what it's testing (CHAIN level rather than NEWEPOCH). In
addition, it adds an extra ada preservation property, which confirms
that outside of an epoch boundary, the change in rewards is equal to the
sum of withdrawls.

shelley/chain-and-ledger/executable-spec/shelley-spec-ledger.cabal

@@ -155,7 +155,6 @@ test-suite shelley-spec-ledger-test
                          Test.Shelley.Spec.Ledger.Rules.TestDeleg
                          Test.Shelley.Spec.Ledger.Rules.TestDelegs
                          Test.Shelley.Spec.Ledger.Rules.TestLedger
-                         Test.Shelley.Spec.Ledger.Rules.TestNewEpoch
                          Test.Shelley.Spec.Ledger.Rules.TestPool
                          Test.Shelley.Spec.Ledger.Rules.TestPoolreap
                          Test.Shelley.Spec.Ledger.Rules.TestUtxo

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/BlockChain.hs

@@ -24,7 +24,7 @@ module Shelley.Spec.Ledger.BlockChain
     BHeader (BHeader),
     Block (Block),
     LaxBlock (..),
-    TxSeq (TxSeq),
+    TxSeq (TxSeq, txSeqTxns'),
     HashBBody,
     bhHash,
     bbHash,

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/LedgerState.hs

@@ -918,6 +918,8 @@ depositPoolChange ls pp tx = (currentPool + txDeposits) - txRefunds
     txRefunds = keyRefunds pp tx
 
 -- | Apply a transaction body as a state transition function on the ledger state.
+--
+--   TODO this function is only used in testing, and should be moved accordingly.
 applyTxBody ::
   (Crypto crypto) =>
   LedgerState crypto ->

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/PoolReap.hs

@@ -55,7 +55,10 @@ instance STS (POOLREAP crypto) where
   type BaseM (POOLREAP crypto) = ShelleyBase
   data PredicateFailure (POOLREAP crypto) -- No predicate Falures
     deriving (Show, Eq, Generic)
-  initialRules = [pure $ PoolreapState emptyUTxOState emptyAccount emptyDState emptyPState]
+  initialRules =
+    [ pure $
+        PoolreapState emptyUTxOState emptyAccount emptyDState emptyPState
+    ]
   transitionRules = [poolReapTransition]
 
 instance NoUnexpectedThunks (PredicateFailure (POOLREAP crypto))
@@ -68,8 +71,14 @@ poolReapTransition = do
       StakePools stpools = _stPools ps
       pr = Map.fromList $ fmap (\kh -> (kh, _poolDeposit pp)) (Set.toList retired)
       rewardAcnts = Map.map _poolRAcnt $ retired ◁ (_pParams ps)
-      rewardAcnts' = Map.fromList . Map.elems $ Map.intersectionWith (,) rewardAcnts pr
-      (refunds, mRefunds) = Map.partitionWithKey (\k _ -> k ∈ dom (_rewards ds)) rewardAcnts'
+      rewardAcnts' =
+        Map.fromList
+          . Map.elems
+          $ Map.intersectionWith (,) rewardAcnts pr
+      (refunds, mRefunds) =
+        Map.partitionWithKey
+          (\k _ -> k ∈ dom (_rewards ds))
+          rewardAcnts'
       refunded = sum $ Map.elems refunds
       unclaimed = sum $ Map.elems mRefunds
 
@@ -84,5 +93,6 @@ poolReapTransition = do
       ps
         { _stPools = StakePools $ retired ⋪ stpools,
           _pParams = retired ⋪ _pParams ps,
+          _fPParams = retired ⋪ _fPParams ps,
           _retiring = retired ⋪ _retiring ps
         }

shelley/chain-and-ledger/executable-spec/test/Test/Shelley/Spec/Ledger/PropertyTests.hs

@@ -15,7 +15,7 @@ import Test.Shelley.Spec.Ledger.Rules.ClassifyTraces
 import Test.Shelley.Spec.Ledger.Rules.TestChain
   ( constantSumPots,
     nonNegativeDeposits,
-    preservationOfAda,
+    adaPreservationChain,
     removedAfterPoolreap,
   )
 import Test.Shelley.Spec.Ledger.Rules.TestLedger
@@ -49,7 +49,7 @@ minimalPropertyTests =
   testGroup
     "Minimal Property Tests"
     [ TQC.testProperty "Chain and Ledger traces cover the relevant cases" relevantCasesAreCovered,
-      TQC.testProperty "total amount of Ada is preserved" preservationOfAda,
+      TQC.testProperty "total amount of Ada is preserved (Chain)" adaPreservationChain,
       TQC.testProperty "Only valid CHAIN STS signals are generated" onlyValidChainSignalsAreGenerated,
       bootstrapHashTest
     ]
@@ -119,7 +119,7 @@ propertyTests =
         "STS Rules - NewEpoch Properties"
         [ TQC.testProperty
             "total amount of Ada is preserved"
-            preservationOfAda
+            adaPreservationChain
         ],
       testGroup
         "STS Rules - MIR certificates"

shelley/chain-and-ledger/executable-spec/test/Test/Shelley/Spec/Ledger/Rules/TestChain.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -8,39 +10,35 @@ module Test.Shelley.Spec.Ledger.Rules.TestChain
     nonNegativeDeposits,
     removedAfterPoolreap,
     -- TestNewEpoch
-    preservationOfAda,
+    adaPreservationChain,
   )
 where
 
 import Cardano.Crypto.Hash (ShortHash)
+import Control.Monad (join)
 import Control.State.Transition.Extended (TRC (TRC), applySTS)
 import Control.State.Transition.Trace
   ( SourceSignalTarget (..),
     Trace (..),
     sourceSignalTargets,
   )
 import Control.State.Transition.Trace.Generator.QuickCheck (forAllTraceFromInitState)
+import Data.Foldable (foldl')
 import Data.Proxy
 import Data.Word (Word64)
-import Shelley.Spec.Ledger.BlockChain (Block (..), bhbody, bheaderSlotNo)
+import Shelley.Spec.Ledger.BlockChain (Block (..), TxSeq (..), bbody, bhbody, bheaderSlotNo)
+import Shelley.Spec.Ledger.Coin
 import Shelley.Spec.Ledger.LedgerState
-  ( esAccountState,
-    esLState,
-    getGKeys,
-    nesEs,
-    _delegationState,
-    _utxoState,
-    pattern DPState,
-  )
-import Shelley.Spec.Ledger.STS.Chain (ChainState (..))
+import Shelley.Spec.Ledger.STS.Chain (ChainState (..), totalAda)
 import Shelley.Spec.Ledger.STS.PoolReap (PoolreapState (..))
 import Shelley.Spec.Ledger.STS.Tick (TickEnv (TickEnv))
-import Test.QuickCheck (Property, Testable, property, withMaxSuccess)
-import Test.Shelley.Spec.Ledger.ConcreteCryptoTypes (CHAIN, NEWEPOCH, POOLREAP, TICK)
+import Shelley.Spec.Ledger.Tx
+import Shelley.Spec.Ledger.TxData
+import Test.QuickCheck
+import Test.Shelley.Spec.Ledger.ConcreteCryptoTypes (CHAIN, POOLREAP, TICK)
 import Test.Shelley.Spec.Ledger.Generator.Core (GenEnv (geConstants))
 import qualified Test.Shelley.Spec.Ledger.Generator.Presets as Preset (genEnv)
 import Test.Shelley.Spec.Ledger.Generator.Trace.Chain (mkGenesisChainState)
-import qualified Test.Shelley.Spec.Ledger.Rules.TestNewEpoch as TestNewEpoch
 import qualified Test.Shelley.Spec.Ledger.Rules.TestPoolreap as TestPoolreap
 import Test.Shelley.Spec.Ledger.Utils (epochFromSlotNo, runShelleyBase, testGlobals)
 
@@ -54,6 +52,68 @@ numberOfTests = 300
 traceLen :: Word64
 traceLen = 100
 
+----------------------------------------------------------------------
+-- Properties for Chain
+---------------------------------------------------------------------
+
+adaPreservationChain :: Property
+adaPreservationChain =
+  forAllChainTrace $ \tr ->
+    conjoin . join $
+      map (\x -> [checkWithdrawlBound x, checkPreservation x]) $
+        sourceSignalTargets tr
+  where
+    checkPreservation SourceSignalTarget {source, signal, target} =
+      counterexample
+        ( mconcat
+            [ "source\n",
+              show source,
+              "signal\n",
+              show signal,
+              "target\n",
+              show target
+            ]
+        )
+        $ totalAda source === totalAda target
+    -- | Check that the sum of the withdrawls equals the change in the rewards,
+    -- assuming we are not on an epoch boundary.
+    checkWithdrawlBound SourceSignalTarget {source, signal, target} =
+      epoch source == epoch target ==> rewardDelta === withdrawls
+      where
+        epoch s = nesEL . chainNes $ s
+        sum_ :: Foldable f => f Coin -> Coin
+        sum_ = foldl' (+) (Coin 0)
+        withdrawls :: Coin
+        withdrawls =
+          foldl'
+            ( \c tx ->
+              let
+                wdrls = unWdrl . _wdrls . _body $
+                              tx
+              in
+                c + sum_ wdrls
+            )
+            (Coin 0)
+            $ txSeqTxns' . bbody $ signal
+        rewardDelta :: Coin
+        rewardDelta =
+          sum_
+            ( _rewards . _dstate
+                . _delegationState
+                . esLState
+                . nesEs
+                . chainNes
+                $ source
+            )
+            - sum_
+              ( _rewards . _dstate
+                  . _delegationState
+                  . esLState
+                  . nesEs
+                  . chainNes
+                  $ target
+              )
+
 ----------------------------------------------------------------------
 -- Properties for PoolReap (using the CHAIN Trace) --
 ----------------------------------------------------------------------
@@ -76,16 +136,6 @@ removedAfterPoolreap =
     let ssts = map chainToPoolreapSst (chainSstWithTick tr)
      in TestPoolreap.removedAfterPoolreap ssts
 
-----------------------------------------------------------------------
--- Properties for NewEpoch (using the CHAIN Trace) --
-----------------------------------------------------------------------
-
-preservationOfAda :: Property
-preservationOfAda =
-  forAllChainTrace $ \tr ->
-    let sst = map chainToNewEpochSst (sourceSignalTargets tr)
-     in TestNewEpoch.preservationOfAda sst
-
 ---------------------------
 -- Utils --
 ---------------------------
@@ -132,20 +182,6 @@ chainToPoolreapSst
       utxoSt = _utxoState . esLState . nesEs
       accountSt = esAccountState . nesEs
 
--- | Transform CHAIN `sourceSignalTargets`s to NEWEPOCH ones.
-chainToNewEpochSst ::
-  SourceSignalTarget (CHAIN ShortHash) ->
-  SourceSignalTarget (NEWEPOCH ShortHash)
-chainToNewEpochSst
-  ( SourceSignalTarget
-      ChainState {chainNes = nes}
-      ChainState {chainNes = nes'}
-      (Block bh _)
-    ) =
-    SourceSignalTarget nes nes' (epochFromSlotNo s)
-    where
-      s = (bheaderSlotNo . bhbody) bh
-
 -- | Transform the [(source, signal, target)] of a CHAIN Trace
 -- by manually applying the Chain TICK Rule to each source and producing
 -- [(source, signal, target')].