View on GitHub
File Changes
  , credentialRemovedAfterDereg
  , rewardZeroAfterReg
  , rewardsSumInvariant
+
  , ledgerToDelegSsts
  )
where

                      
+
import           Data.Foldable (toList)
import           Data.Map (Map)
import qualified Data.Map.Strict as Map (difference, filter, lookup)
import qualified Data.Maybe as Maybe (maybe)
import           Data.Set (Set)
import qualified Data.Set as Set (singleton, size)
import           Data.Word (Word64)
import           Hedgehog (MonadTest, Property, TestLimit, forAll, property, withTests)
+
import           Lens.Micro ((^.))

                      
import           Address (mkRwdAcnt)
import           BaseTypes ((==>))
import           Ledger.Core (dom, range, (∈), (∉), (◁))

                      
import           Coin (Coin, pattern Coin)
-
import           LedgerState (_delegations, _rewards, _stkCreds)
-
import           MockTypes (DELEG, DState, KeyHash, RewardAcnt, StakeCredential)
+
import           LedgerState (pattern DPState, _delegations, _rewards, _stkCreds)
+
import           MockTypes (DELEG, DState, KeyHash, LEDGER, RewardAcnt, StakeCredential)
import           Test.Utils (assertAll)
-
import           TxData (pattern DeRegKey, pattern Delegate, pattern Delegation, pattern RegKey)
+
import           TxData (pattern DeRegKey, pattern Delegate, pattern Delegation, pattern RegKey,
+
                     body, certs)

                      
-------------------------------
-- helper accessor functions --
             null (Map.filter (/= Coin 0) $ rew `Map.difference` rew')
          && -- added elements have a zero reward balance
             null (Map.filter (/= Coin 0) $ rew' `Map.difference` rew)
+

                      
+
-- | Transform LEDGER `sourceSignalTargets`s to DELEG ones.
+
ledgerToDelegSsts
+
  :: SourceSignalTarget LEDGER
+
  -> [SourceSignalTarget DELEG]
+
ledgerToDelegSsts (SourceSignalTarget (_, DPState d _) (_, DPState d' _) tx) =
+
  [SourceSignalTarget d d' cert | cert <- toList (tx ^. body . certs)]
  )
where

                      
-
import           Data.Foldable (toList)
-
import qualified Data.Map as M
-
import           Data.Maybe (mapMaybe)
import           Data.Word (Word64)
-
import           Lens.Micro (to, (^.))
+
import           Lens.Micro ((^.))

                      
import           Hedgehog (Property, forAll, property, withTests)

                      
-
import           Control.State.Transition (Environment)
import           Control.State.Transition.Generator (ofLengthAtLeast, trace,
                     traceOfLengthWithInitState)
import           Control.State.Transition.Trace (SourceSignalTarget (..), source,
import           Generator.LedgerTrace ()

                      
import           Coin (pattern Coin)
-
import           Ledger.Core ((∈))
-
import           LedgerState (pattern DPState, pattern DState, pattern UTxOState, cCounters,
-
                     pParams, pstate, stPools, _deposited, _dstate, _fees, _rewards, _utxo)
-
import           MockTypes (DCert, DELEG, LEDGER, PoolParams)
+
import           LedgerState (pattern DPState, pattern DState, pattern UTxOState, _deposited,
+
                     _dstate, _fees, _rewards, _utxo)
+
import           MockTypes (LEDGER)
import qualified Rules.TestDeleg as TestDeleg
-
import           STS.Ledger (LedgerEnv (ledgerSlot))
-
import           TxData (pattern RegPool, StakePools (StakePools), body, certs, poolPubKey, _body,
-
                     _certs)
+
import qualified Rules.TestPool as TestPool
import           UTxO (balance)

                      
import           Test.Utils (assertAll)
        `ofLengthAtLeast` 1)

                      
  TestDeleg.rewardZeroAfterReg
-
    ((concatMap ledgerToDelegSsts . sourceSignalTargets) t)
+
    ((concatMap TestDeleg.ledgerToDelegSsts . sourceSignalTargets) t)

                      

                      
credentialRemovedAfterDereg :: Property
                                     mkGenesisLedgerState
            `ofLengthAtLeast` 1
    TestDeleg.credentialRemovedAfterDereg
-
      (concatMap ledgerToDelegSsts tr)
+
      (concatMap TestDeleg.ledgerToDelegSsts tr)

                      

                      
-- | Check that the value consumed by UTXO is equal to the value produced in
                                     (fromIntegral traceLen)
                                     mkGenesisLedgerState
            `ofLengthAtLeast` 1
-
    assertAll (addedRegPool (tr ^. traceEnv)) (sourceSignalTargets tr)
-

                      
-
 where
-

                      
-
  getTxRegPoolParams :: SourceSignalTarget LEDGER -> [PoolParams]
-
  getTxRegPoolParams sst =
-
    mapMaybe getPoolParams (toList (signal sst ^. body . certs))
-

                      
-
  getPoolParams :: DCert -> Maybe PoolParams
-
  getPoolParams cert = case cert of
-
                         RegPool pps -> Just pps
-
                         _ -> Nothing
-

                      
-
  addedRegPool :: Environment LEDGER
-
               -> SourceSignalTarget LEDGER
-
               -> Bool
-
  addedRegPool env sst = all check (getTxRegPoolParams sst)
-
   where
-
    check :: PoolParams -> Bool
-
    check poolParams =
-
      let hk = poolParams ^. poolPubKey
-
          pSt = snd (target sst) ^. pstate
-
          -- PoolParams are registered in pParams map
-
       in M.lookup hk (pSt ^. pParams) == Just poolParams
-
          -- Hashkey is registered in stPools map
-
       && M.lookup hk (pSt ^. stPools . to (\(StakePools x) -> x))
-
            == Just (ledgerSlot env)
-
          -- Hashkey is registered in cCounters map
-
       && hk ∈ M.keys (pSt ^. cCounters)
-

                      
-

                      
-
-- | Transform LEDGER `sourceSignalTargets`s to DELEG ones.
-
ledgerToDelegSsts
-
  :: SourceSignalTarget LEDGER
-
  -> [SourceSignalTarget DELEG]
-
ledgerToDelegSsts (SourceSignalTarget (_, DPState d _) (_, DPState d' _) tx) =
-
  [SourceSignalTarget d d' cert | cert <- toList . _certs . _body $ tx]
+
    TestPool.registeredPoolIsAdded
+
      (tr ^. traceEnv)
+
      (concatMap TestPool.ledgerToPoolSsts (sourceSignalTargets tr))

                      
module Rules.TestPool where

                      
+
import           Data.Foldable (toList)
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 (Property, forAll, property, withTests)
+
import           Hedgehog (MonadTest, Property, forAll, property, withTests)

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

                      
import           BaseTypes ((==>))
import           Delegation.Certificates (cwitness)
-
import           LedgerState (_retiring, _stPools)
-
import           MockTypes (KeyHash, POOL, PState, StakePools)
+
import           LedgerState (pattern DPState, cCounters, pParams, stPools, _retiring, _stPools)
+
import           MockTypes (KeyHash, LEDGER, POOL, PState, PoolParams, StakePools)
import           PParams (_eMax)
import           Slot (Epoch (..), epochFromSlot)
+
import           STS.Ledger (LedgerEnv (ledgerSlot))
import           STS.Pool (PoolEnv (..))
-
import           TxData (pattern KeyHashObj, pattern RegPool, pattern RetirePool,
-
                     pattern StakePools)
+
import           TxData (pattern KeyHashObj, pattern RegPool, pattern RegPool, pattern RetirePool,
+
                     pattern StakePools, body, certs, poolPubKey)

                      

                      
import           Ledger.Core (dom, (∈), (∉))
                                    && Maybe.maybe False ((== e) . epochFromSlot) (stp' !? certWit))
            _                  -> False
        registeredPoolRetired _ _ _ = True
+

                      
+
-- | Check that a `RegPool` certificate properly adds a stake pool.
+
registeredPoolIsAdded
+
  :: MonadTest m
+
  => Environment LEDGER
+
  -> [SourceSignalTarget POOL]
+
  -> m ()
+
registeredPoolIsAdded env ssts =
+
  assertAll addedRegPool ssts
+

                      
+
 where
+

                      
+
  addedRegPool :: SourceSignalTarget POOL
+
               -> Bool
+
  addedRegPool sst =
+
    case signal sst of
+
      RegPool poolParams -> check poolParams
+
      _ -> True
+
   where
+
    check :: PoolParams -> Bool
+
    check poolParams =
+
      let hk = poolParams ^. poolPubKey
+
          pSt = target sst
+
          -- PoolParams are registered in pParams map
+
       in M.lookup hk (pSt ^. pParams) == Just poolParams
+
          -- Hashkey is registered in stPools map
+
       && M.lookup hk (pSt ^. stPools . to (\(StakePools x) -> x))
+
            == Just (ledgerSlot env)
+
          -- Hashkey is registered in cCounters map
+
       && hk ∈ M.keys (pSt ^. cCounters)
+

                      
+
-- | Transform LEDGER `SourceSignalTargets`s to POOL ones.
+
ledgerToPoolSsts
+
  :: SourceSignalTarget LEDGER
+
  -> [SourceSignalTarget POOL]
+
ledgerToPoolSsts (SourceSignalTarget (_, DPState _ p) (_, DPState _ p') tx) =
+
  [SourceSignalTarget p p' cert | cert <- toList (tx ^. body . certs)]