View on GitHub
File Changes
import           LedgerState hiding (genDelegs)
import           PParams
import           Rules.ClassifyTraces (relevantCasesAreCovered)
-
import           Rules.TestLedger (credentialRemovedAfterDereg, registeredPoolIsAdded,
-
                     rewardZeroAfterReg)
+
import           Rules.TestLedger (credentialRemovedAfterDereg, pStateIsInternallyConsistent,
+
                     registeredPoolIsAdded, rewardZeroAfterReg)
import           Slot
import           Tx (pattern TxIn, pattern TxOut, body, certs, inputs, outputs, witnessVKeySet,
                     _body, _witnessVKeySet)
                  [ testProperty "newly registered key has a reward of 0" rewardZeroAfterReg
                  , testProperty "deregistered key's credential is removed"
                                 credentialRemovedAfterDereg
-
                  , testProperty "newly registered stake pool is added to \
+
                  ]
+
                , testGroup "STS Rules - Pool Properties"
+
                  [ testProperty "newly registered stake pool is added to \
                                 \appropriate state mappings"
                                 registeredPoolIsAdded
+
                  , testProperty "pool state is internally consistent"
+
                                 pStateIsInternallyConsistent
                  ]
                , testGroup "Ledger Genesis State"
                  [testProperty
  , credentialRemovedAfterDereg
  , consumedEqualsProduced
  , registeredPoolIsAdded
+
  , pStateIsInternallyConsistent
  )
where

                      
      (concatMap ledgerToPoolSsts (sourceSignalTargets tr))

                      

                      
+
pStateIsInternallyConsistent :: Property
+
pStateIsInternallyConsistent = do
+
  withTests (fromIntegral numberOfTests) . property $ do
+
    tr <- forAll
+
          $ traceOfLengthWithInitState @LEDGER
+
                                     (fromIntegral traceLen)
+
                                     mkGenesisLedgerState
+
            `ofLengthAtLeast` 1
+
    TestPool.pStateIsInternallyConsistent
+
      (concatMap ledgerToPoolSsts (sourceSignalTargets tr))
+

                      
+

                      
-- | Transform LEDGER `sourceSignalTargets`s to DELEG ones.
ledgerToDelegSsts
  :: SourceSignalTarget LEDGER
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
+
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}

                      
module Rules.TestPool where

                      
+
import           Data.Foldable (traverse_)
import           Data.Map (Map, (!?))
import qualified Data.Map as M
import qualified Data.Maybe as Maybe (maybe)
import           Data.Word (Word64)
import           Lens.Micro (to, (^.))

                      
-
import           Hedgehog (MonadTest, Property, forAll, property, withTests)
+
import           Hedgehog (MonadTest, Property, assert, forAll, property, withTests, (===))

                      
-
import           Control.State.Transition (Environment)
+
import           Control.State.Transition (Environment, State)
import           Control.State.Transition.Generator (ofLengthAtLeast, trace)
import           Control.State.Transition.Trace (SourceSignalTarget, pattern SourceSignalTarget,
                     signal, source, sourceSignalTargets, target, _traceEnv)

                      
import           BaseTypes ((==>))
import           Delegation.Certificates (cwitness)
-
import           LedgerState (cCounters, pParams, stPools, _retiring, _stPools)
+
import           LedgerState (pattern PState, cCounters, pParams, stPools, _retiring, _stPools)
import           MockTypes (KeyHash, LEDGER, POOL, PState, PoolParams, StakePools)
import           PParams (_eMax)
import           Slot (Epoch (..), epochFromSlot)
import           Ledger.Core (dom, (∈), (∉))
import           Test.Utils (assertAll)

                      
+
import qualified Debug.Trace as T
+

                      
-------------------------------
-- helper accessor functions --
-------------------------------
            == Just (ledgerSlot env)
          -- Hashkey is registered in cCounters map
       && hk ∈ M.keys (pSt ^. cCounters)
+

                      
+
-- | Assert that PState maps are in sync with each other after each `Signal
+
-- POOL` transition.
+
pStateIsInternallyConsistent
+
  :: forall m
+
   . MonadTest m
+
  => [SourceSignalTarget POOL]
+
  -> m ()
+
pStateIsInternallyConsistent ssts =
+
  traverse_ isConsistent (concatMap (\sst -> [source sst, target sst]) ssts)
+
 where
+
  isConsistent :: State POOL -> m ()
+
  isConsistent (PState stPools_ pParams_ retiring_ cCounters_) = do
+
    let StakePools stPoolsMap = stPools_
+
        poolKeys = M.keys stPoolsMap
+
        pParamKeys = M.keys pParams_
+
        retiringKeys = M.keys retiring_
+
        cCountersKeys = M.keys cCounters_
+
        printout = "length poolKeys: " <> show (length poolKeys)
+
              <> "\nlength pParamKeys: " <> show (length pParamKeys)
+
              <> "\nlength retiringKeys: " <> show (length retiringKeys)
+
              <> "\nlength cCountersKeys: " <> show (length cCountersKeys)
+
    T.trace printout $
+
      sequence_ [ poolKeys === pParamKeys
+
                , pParamKeys === cCountersKeys
+
                , cCountersKeys === poolKeys
+
                , traverse_ (assert . (`elem` poolKeys)) retiringKeys
+
                ]
+
   where