The case of the missing ada

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

@@ -123,7 +123,7 @@ import Shelley.Spec.Ledger.BaseTypes
     intervalValue,
   )
 import Shelley.Spec.Ledger.Coin (Coin (..))
-import Shelley.Spec.Ledger.Core (dom, (∪), (∪+), (⋪), (▷), (◁))
+import Shelley.Spec.Ledger.Core (dom, haskey, range, (∪), (∪+), (⋪), (▷), (◁))
 import Shelley.Spec.Ledger.Credential (Credential (..))
 import Shelley.Spec.Ledger.Crypto (Crypto)
 import Shelley.Spec.Ledger.Delegation.Certificates
@@ -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 ->
@@ -990,10 +992,14 @@ applyRUpd ru (EpochState as ss ls pr pp _nm) = EpochState as' ss ls' pr pp nm'
     utxoState_ = _utxoState ls
     delegState = _delegationState ls
     dState = _dstate delegState
+    (regRU, unregRU) =
+      Map.partitionWithKey
+        (\(RewardAcnt _ k) _ -> haskey k $ _stkCreds dState)
+        (rs ru)
     as' =
       as
         { _treasury = _treasury as + deltaT ru,
-          _reserves = _reserves as + deltaR ru
+          _reserves = _reserves as + deltaR ru + sum (range unregRU)
         }
     ls' =
       ls
@@ -1003,7 +1009,7 @@ applyRUpd ru (EpochState as ss ls pr pp _nm) = EpochState as' ss ls' pr pp nm'
             delegState
               { _dstate =
                   dState
-                    { _rewards = _rewards dState ∪+ rs ru
+                    { _rewards = _rewards dState ∪+ regRU
                     }
               }
         }

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

@@ -105,6 +105,10 @@ instance STS (DELEG crypto) where
   data PredicateFailure (DELEG crypto)
     = StakeKeyAlreadyRegisteredDELEG
         !(Credential 'Staking crypto) -- Credential which is already registered
+    | -- | Indicates that the stake key is somehow already in the rewards map.
+      --   This error being seen indicates a potential bug in the rules.
+      StakeKeyInRewardsDELEG
+        !(Credential 'Staking crypto) -- Credential which is already registered
     | StakeKeyNotRegisteredDELEG
         !(Credential 'Staking crypto) -- Credential which is not registered
     | StakeKeyNonZeroAccountBalanceDELEG
@@ -139,6 +143,8 @@ instance
   toCBOR = \case
     StakeKeyAlreadyRegisteredDELEG cred ->
       encodeListLen 2 <> toCBOR (0 :: Word8) <> toCBOR cred
+    StakeKeyInRewardsDELEG cred ->
+      encodeListLen 2 <> toCBOR (10 :: Word8) <> toCBOR cred
     StakeKeyNotRegisteredDELEG cred ->
       encodeListLen 2 <> toCBOR (1 :: Word8) <> toCBOR cred
     StakeKeyNonZeroAccountBalanceDELEG rewardBalance ->
@@ -172,6 +178,10 @@ instance
         matchSize "StakeKeyAlreadyRegisteredDELEG" 2 n
         kh <- fromCBOR
         pure $ StakeKeyAlreadyRegisteredDELEG kh
+      10 -> do
+        matchSize "StakeKeyInRewardsDELEG" 2 n
+        kh <- fromCBOR
+        pure $ StakeKeyInRewardsDELEG kh
       1 -> do
         matchSize "StakeKeyNotRegisteredDELEG" 2 n
         kh <- fromCBOR
@@ -222,6 +232,7 @@ delegationTransition = do
       -- note that pattern match is used instead of regCred, as in the spec
       -- hk ∉ dom (_stkCreds ds) -- Specification code translates below
       not (haskey hk (_stkCreds ds)) ?! StakeKeyAlreadyRegisteredDELEG hk
+      not (haskey (RewardAcnt network hk) (_rewards ds)) ?! StakeKeyInRewardsDELEG hk
 
       pure $
         ds

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

@@ -13,10 +13,11 @@ import Test.Shelley.Spec.Ledger.Rules.ClassifyTraces
     relevantCasesAreCovered,
   )
 import Test.Shelley.Spec.Ledger.Rules.TestChain
-  ( constantSumPots,
+  ( adaPreservationChain,
+    constantSumPots,
     nonNegativeDeposits,
-    preservationOfAda,
     removedAfterPoolreap,
+    rewardStkCredSync,
   )
 import Test.Shelley.Spec.Ledger.Rules.TestLedger
   ( consumedEqualsProduced,
@@ -49,7 +50,8 @@ 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 "reward and stake credential maps stay in sync" rewardStkCredSync,
       TQC.testProperty "Only valid CHAIN STS signals are generated" onlyValidChainSignalsAreGenerated,
       bootstrapHashTest
     ]
@@ -119,7 +121,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,38 @@ module Test.Shelley.Spec.Ledger.Rules.TestChain
     nonNegativeDeposits,
     removedAfterPoolreap,
     -- TestNewEpoch
-    preservationOfAda,
+    adaPreservationChain,
+    rewardStkCredSync,
   )
 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 qualified Data.Set as Set
 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.Core
 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 +55,95 @@ numberOfTests = 300
 traceLen :: Word64
 traceLen = 100
 
+----------------------------------------------------------------------
+-- Properties for Chain
+---------------------------------------------------------------------
+
+-- | Verify that the domains for '_rewards' and '_srkCreds' remain in sync.
+rewardStkCredSync :: Property
+rewardStkCredSync =
+  forAllChainTrace $ \tr ->
+    conjoin $
+      map checkSync $
+        sourceSignalTargets tr
+  where
+    checkSync SourceSignalTarget {source, signal, target} =
+      let ds =
+            _dstate
+              . _delegationState
+              . esLState
+              . nesEs
+              . chainNes
+              $ target
+       in counterexample
+            ( mconcat
+                [ "source\n",
+                  show source,
+                  "signal\n",
+                  show signal,
+                  "target\n",
+                  show target
+                ]
+            )
+            $ dom
+              (_stkCreds ds)
+              === (Set.map getRwdCred $ dom (_rewards ds))
+
+adaPreservationChain :: Property
+adaPreservationChain =
+  forAllChainTrace $ \tr ->
+    conjoin . join $
+      map (\x -> [checkPreservation x, checkWithdrawlBound 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
+    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 +166,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 +212,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')].