View on GitHub
File Changes
  -- TODO @uroboros Generate _RetirePool_ Certificates
  -- TODO @uroboros Generate _Delegate_ Certificates
  Gen.frequency [ (3, genRegKeyCert keys dState)
-
                , (4, genDeRegKeyCert keys dState)
+
                , (3, genDeRegKeyCert keys dState)
                , (3, genRegPool keys vrfKeys dpState)
                , (1, pure Nothing)
                ]
  , 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 (pattern DPState, _delegations, _rewards, _stkCreds)
-
import           MockTypes (DELEG, DState, KeyHash, LEDGER, RewardAcnt, StakeCredential)
+
import           LedgerState (_delegations, _rewards, _stkCreds)
+
import           MockTypes (DELEG, DState, KeyHash, RewardAcnt, StakeCredential)
import           Test.Utils (assertAll)
-
import           TxData (pattern DeRegKey, pattern Delegate, pattern Delegation, pattern RegKey,
-
                     body, certs)
+
import           TxData (pattern DeRegKey, pattern Delegate, pattern Delegation, pattern RegKey)

                      
-------------------------------
-- 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           Data.Word (Word64)
import           Lens.Micro ((^.))

                      
import           Coin (pattern Coin)
import           LedgerState (pattern DPState, pattern DState, pattern UTxOState, _deposited,
                     _dstate, _fees, _rewards, _utxo)
-
import           MockTypes (LEDGER)
+
import           MockTypes (DELEG, LEDGER, POOL)
import qualified Rules.TestDeleg as TestDeleg
import qualified Rules.TestPool as TestPool
+
import           TxData (body, certs)
import           UTxO (balance)

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

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

                      

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

                      

                      
-- | Check that the value consumed by UTXO is equal to the value produced in
            `ofLengthAtLeast` 1
    TestPool.registeredPoolIsAdded
      (tr ^. traceEnv)
-
      (concatMap TestPool.ledgerToPoolSsts (sourceSignalTargets tr))
+
      (concatMap ledgerToPoolSsts (sourceSignalTargets tr))
+

                      
+

                      
+
-- | 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)]
+

                      
+

                      
+
-- | 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)]

                      
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           BaseTypes ((==>))
import           Delegation.Certificates (cwitness)
-
import           LedgerState (pattern DPState, cCounters, pParams, stPools, _retiring, _stPools)
+
import           LedgerState (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 RegPool, pattern RetirePool,
-
                     pattern StakePools, body, certs, poolPubKey)
+
import           TxData (pattern KeyHashObj, pattern RegPool, pattern RetirePool,
+
                     pattern StakePools, poolPubKey)

                      

                      
import           Ledger.Core (dom, (∈), (∉))
            == 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)]