[#870] Add pStateIsInternallyConsistent property

Relates to #870.
IntersectMBO · Oct 18, 2019 · 8caea52 · 8caea52
1 parent f35596b
commit 8caea52
Show file tree

Hide file tree

Showing 3 changed files with 56 additions and 6 deletions.
diff --git a/shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs b/shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs
@@ -24,8 +24,8 @@ import           Ledger.Core ((<|))
 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)
@@ -161,9 +161,13 @@ propertyTests = testGroup "Property-Based Testing"
                   [ 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

diff --git a/shelley/chain-and-ledger/executable-spec/test/Rules/TestLedger.hs b/shelley/chain-and-ledger/executable-spec/test/Rules/TestLedger.hs
@@ -8,6 +8,7 @@ module Rules.TestLedger
   , credentialRemovedAfterDereg
   , consumedEqualsProduced
   , registeredPoolIsAdded
+  , pStateIsInternallyConsistent
   )
 where
 
@@ -121,6 +122,18 @@ registeredPoolIsAdded = do
       (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

diff --git a/shelley/chain-and-ledger/executable-spec/test/Rules/TestPool.hs b/shelley/chain-and-ledger/executable-spec/test/Rules/TestPool.hs
@@ -1,27 +1,29 @@
 {-# 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)
@@ -34,6 +36,8 @@ import           TxData (pattern KeyHashObj, pattern RegPool, pattern RetirePool
 import           Ledger.Core (dom, (∈), (∉))
 import           Test.Utils (assertAll)
 
+import qualified Debug.Trace as T
+
 -------------------------------
 -- helper accessor functions --
 -------------------------------
@@ -136,3 +140,32 @@ registeredPoolIsAdded env ssts =
             == 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