View on GitHub
File Changes
  , decayPool
  , isRegKey
  , isDeRegKey
+
  , isRegPool
  , isInstantaneousRewards
  ) where

                      
isDeRegKey (DeRegKey _) = True
isDeRegKey _ = False

                      
+
-- | Check for `RegPool` constructor
+
isRegPool :: DCert hashAlgo dsignAlgo vrfAlgo -> Bool
+
isRegPool (RegPool _) = True
+
isRegPool _ = False
+

                      
decayKey :: PParams -> (Coin, UnitInterval, Rational)
decayKey pc = (dval, dmin, lambdad)
    where dval    = fromIntegral $ pc ^. keyDeposit
    (
      utxoSize
    , utxoMap
-
    , genNatural
    , genNonEmptyAndAdvanceTx
    , genNonEmptyAndAdvanceTx'
    , genNonemptyGenesisState
-
    , genStakePool
    , genStateTx
    , genValidStateTx
    , genValidStateTxKeys
    , genDelegationData
    , genDelegation
-
    , genDCertRegPool
    , genDCertDelegate
    , genKeyPairs
    ) where

                      
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
-
import           Data.Ratio
import           Data.Sequence (Seq (..))
import qualified Data.Set as Set

                      
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range

                      
-
import           BaseTypes
import           Coin
-
import           Generator.Core (findPayKeyPair, genInteger, genNatural)
-
import           Keys (pattern KeyPair, hashKey, hashKeyVRF, vKey)
+
import           Generator.Core (findPayKeyPair, genNatural)
+
import           Keys (pattern KeyPair, hashKey, vKey)
import           LedgerState (DState (..), pattern LedgerValidation, ValidationError (..),
                     asStateTransition, asStateTransition', dstate, genesisCoins, genesisState,
                     stkCreds, utxo, utxoState, _delegationState, _dstate)
import           PParams (PParams (..), emptyPParams)
import           Slot
import           Tx (pattern Tx, pattern TxBody, pattern TxOut)
import           TxData (pattern AddrBase, pattern DeRegKey, pattern Delegate, pattern Delegation,
-
                     pattern KeyHashObj, pattern PoolParams, pattern RegKey, pattern RegPool,
-
                     pattern RetirePool, RewardAcnt (..), StakeCreds (..))
+
                     pattern KeyHashObj, pattern RegKey, pattern RetirePool, StakeCreds (..))
import           Updates
import           UTxO (pattern UTxO, balance, makeWitnessVKey)

                      
  key <- getAnyStakeKey keys
  pure $ RetirePool (hashKey key) epoch

                      
-
genStakePool :: KeyPairs -> [(SignKeyVRF, VerKeyVRF)] -> Gen PoolParams
-
genStakePool skeys vrfKeys = do
-
  poolKey       <- getAnyStakeKey skeys
-
  vrfKey        <- snd <$> Gen.element vrfKeys
-
  cost          <- Coin <$> genInteger 1 100
-
  pledge        <- Coin <$> genInteger 1 100
-
  marginPercent <- genNatural 0 100
-
  acntKey       <- getAnyStakeKey skeys
-
  let interval = case mkUnitInterval $ fromIntegral marginPercent % 100 of
-
                   Just i  -> i
-
                   Nothing -> interval0
-
  pure $ PoolParams
-
           (hashKey poolKey)
-
           (hashKeyVRF vrfKey)
-
           pledge
-
           cost
-
           interval
-
           (RewardAcnt $ KeyHashObj $ hashKey acntKey)
-
           Set.empty
-

                      
genDelegation :: KeyPairs -> DPState -> Gen Delegation
genDelegation keys d = do
  poolKey      <- Gen.element $ Map.keys stkCreds'
  delegatorKey <- getAnyStakeKey keys
  pure $ Delegation (KeyHashObj $ hashKey delegatorKey) $ (hashKey $ vKey $ findStakeKeyPair poolKey keys)
       where (StakeCreds stkCreds') = d ^. dstate . stkCreds

                      
-
genDCertRegPool :: KeyPairs -> [(SignKeyVRF, VerKeyVRF)] -> Gen DCert
-
genDCertRegPool skeys vrfKeys = RegPool <$> genStakePool skeys vrfKeys
-

                      
genDCertDelegate :: KeyPairs -> DPState -> Gen DCert
genDCertDelegate keys ds = Delegate <$> genDelegation keys ds
  , increasingProbabilityAt
  , mkGenesisLedgerState
  , traceKeyPairs
+
  , traceVRFKeyPairs
  , someKeyPairs
  , pickStakeKey
  , toAddr
  , toCred)
  where

                      
+
import           Cardano.Crypto.VRF (deriveVerKeyVRF, genKeyVRF)
+
import           Crypto.Random (drgNewTest, withDRG)
import           Data.Tuple (swap)
import           Data.Word (Word64)
import           Hedgehog (Gen)
import           Examples (mkKeyPair)
import           Keys (pattern KeyPair, hashKey, vKey)
import           LedgerState (pattern LedgerState, genesisCoins, genesisState)
-
import           MockTypes (Addr, DPState, KeyPair, KeyPairs, LedgerEnv, TxOut, UTxO, UTxOState,
-
                     VKey)
+
import           MockTypes (Addr, DPState, KeyPair, KeyPairs, LedgerEnv, SignKeyVRF, TxOut, UTxO,
+
                     UTxOState, VKey, VerKeyVRF)
import           Numeric.Natural (Natural)
import           Tx (pattern TxOut)
import           TxData (pattern AddrBase, pattern KeyHashObj)

                      
-- | Constant list of KeyPairs intended to be used in the generators.
traceKeyPairs :: KeyPairs
-
traceKeyPairs = mkKeyPairs <$> [1 .. 50]
+
traceKeyPairs = mkKeyPairs <$> [1 .. 150]

                      
-- | Select between _lower_ and _upper_ keys from 'traceKeyPairs'
someKeyPairs :: Int -> Int -> Gen KeyPairs
                  , (90, gen)
                  , (5, pure upper)
                  ]
+

                      
+
-- | A pre-populated space of VRF keys for use in the generators.
+
traceVRFKeyPairs :: [(SignKeyVRF, VerKeyVRF)]
+
traceVRFKeyPairs = [body (0,0,0,0,i) | i <- [1 .. 50]]
+
 where
+
  body seed = fst . withDRG (drgNewTest seed) $ do
+
    sk <- genKeyVRF
+
    return (sk, deriveVerKeyVRF sk)
  ( genDCerts )
  where

                      
+
import qualified Data.Map as Map
+
import           Data.Ratio ((%))
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
+
import qualified Data.Set as Set
import           Hedgehog (Gen)
-
import           Lens.Micro ((^.))
+
import           Lens.Micro (to, (^.))

                      
import qualified Hedgehog.Gen as Gen

                      
import           Coin (Coin (..))
-
import           Delegation.Certificates (pattern DeRegKey, pattern RegKey, decayKey, isDeRegKey)
-
import           Generator.Core (toCred)
+
import           Delegation.Certificates (pattern DeRegKey, pattern RegKey, pattern RegPool,
+
                     decayKey, isDeRegKey)
+
import           Examples (unsafeMkUnitInterval)
+
import           Generator.Core (genInteger, genNatural, toCred)
+
import           Keys (hashKey, hashKeyVRF, vKey)
import           Ledger.Core (dom, (∈), (∉))
-
import           LedgerState (dstate, keyRefund, stkCreds, _dstate, _pstate, _stkCreds, _stPools)
-
import           MockTypes (DCert, DPState, DState, KeyPair, KeyPairs)
+
import           LedgerState (dstate, keyRefund, pParams, pstate, stkCreds, _pstate, _stPools,
+
                     _stkCreds)
+
import           MockTypes (DCert, DPState, DState, KeyPair, KeyPairs, PoolParams, VrfKeyPairs)
+
import           Mutator (getAnyStakeKey)
import           PParams (PParams (..))
import           Slot (Slot)
+
import           TxData (Credential (KeyHashObj), pattern PoolParams, RewardAcnt (..), _poolPubKey,
+
                     _poolVrf)
import           UTxO (deposits)

                      
-- | Generate certificates and also return the associated witnesses and
-- deposits and refunds required.
genDCerts
  :: KeyPairs
+
  -> VrfKeyPairs
  -> PParams
  -> DPState
  -> Slot
  -> Gen (Seq DCert, [KeyPair], Coin, Coin)
-
genDCerts keys pparams dpState slotWithTTL = do
+
genDCerts keys vrfKeys pparams dpState slotWithTTL = do
  -- TODO @uroboros Generate _multiple_ certs per Tx
  -- TODO ensure that the `Seq` is constructed with the list reversed, or that
  -- later traversals are done backwards, to be consistent with the executable
  -- spec (see `delegsTransition` in `STS.Delegs`) which consumes the list
  -- starting at the tail end.
-
  cert <- genDCert keys (_dstate dpState)
+
  cert <- genDCert keys vrfKeys dpState
  case cert of
    Nothing ->
      return (Seq.empty, [], Coin 0, Coin 0)
-- | Occasionally generate a valid certificate
genDCert
  :: KeyPairs
-
  -> DState
+
  -> VrfKeyPairs
+
  -> DPState
  -> Gen (Maybe (DCert, KeyPair))
-
genDCert keys dState =
-
  -- TODO @uroboros Generate _RegPool_ Certificates
+
genDCert keys vrfKeys dpState =
  -- TODO @uroboros Generate _RetirePool_ Certificates
  -- TODO @uroboros Generate _Delegate_ Certificates
-
  Gen.frequency [ (1, genRegKeyCert keys dState)
-
                , (1, genDeRegKeyCert keys dState)
+
  Gen.frequency [ (3, genRegKeyCert keys dState)
+
                , (3, genDeRegKeyCert keys dState)
+
                , (3, genRegPool keys vrfKeys dpState)
                , (1, pure Nothing)
                ]
+
 where
+
  dState = dpState ^. dstate

                      
-- | Generate a RegKey certificate along and also returns the stake key
-- (needed to witness the certificate)
  where
    registered k = k ∈ dom (_stkCreds delegSt)
    availableKeys = filter (registered . toCred . snd) keys
+

                      
+
-- | Generate and return a RegPool certificate along with its witnessing key.
+
genRegPool
+
  :: KeyPairs
+
  -> VrfKeyPairs
+
  -> DPState
+
  -> Gen (Maybe (DCert, KeyPair))
+
genRegPool keys vrfKeys dpState =
+
  if null availableKeys || null availableVrfKeys
+
     then pure Nothing
+
     else do
+
       Just <$> genDCertRegPool availableKeys availableVrfKeys
+
 where
+
  notRegistered k = k `notElem` (dpState ^. pstate . pParams . to Map.elems . to (_poolPubKey <$>))
+
  availableKeys = filter (notRegistered . hashKey . vKey . snd) keys
+

                      
+
  notRegisteredVrf k = k `notElem` (dpState ^. pstate . pParams . to Map.elems . to (_poolVrf <$>))
+
  availableVrfKeys = filter (notRegisteredVrf . hashKeyVRF . snd) vrfKeys
+

                      
+
-- | Generate PoolParams and the key witness.
+
genStakePool :: KeyPairs -> VrfKeyPairs -> Gen (PoolParams, KeyPair)
+
genStakePool skeys vrfKeys =
+
  mkPoolParams
+
    <$> (Gen.element skeys)
+
    <*> (snd <$> Gen.element vrfKeys)
+
    <*> (Coin <$> genInteger 1 100)
+
    <*> (Coin <$> genInteger 1 100)
+
    <*> (genNatural 0 100)
+
    <*> (getAnyStakeKey skeys)
+
 where
+
  mkPoolParams poolKeyPair vrfKey cost pledge marginPercent acntKey =
+
    let interval = unsafeMkUnitInterval $ fromIntegral marginPercent % 100
+
        pps = PoolParams
+
                (hashKey . vKey . snd $ poolKeyPair)
+
                (hashKeyVRF vrfKey)
+
                pledge
+
                cost
+
                interval
+
                (RewardAcnt $ KeyHashObj $ hashKey acntKey)
+
                Set.empty
+
     in (pps, snd poolKeyPair)
+

                      
+
-- | Generate `RegPool` and the key witness.
+
genDCertRegPool :: KeyPairs -> VrfKeyPairs -> Gen (DCert, KeyPair)
+
genDCertRegPool skeys vrfKeys = do
+
  (pps, poolKey) <- genStakePool skeys vrfKeys
+
  pure (RegPool pps, poolKey)
import           Cardano.Crypto.VRF.Fake (FakeVRF)

                      
import           Control.State.Transition.Generator (HasTrace, envGen, sigGen)
-
import           Generator.Core (genCoin, traceKeyPairs)
+
import           Generator.Core (genCoin, traceKeyPairs, traceVRFKeyPairs)
import           Generator.Update (genPParams)
import           Generator.Utxo (genTx)
import           Slot (Slot (..))
                <*> genCoin 0 1000

                      
    sigGen ledgerEnv ledgerSt =
-
      genTx ledgerEnv ledgerSt traceKeyPairs
+
      genTx ledgerEnv ledgerSt traceKeyPairs traceVRFKeyPairs
                       -- protocolVersion
                       <*> ((,,) <$> genNatural 1 10 <*> genNatural 1 50 <*> genNatural 1 100)
  where
-
    low = 1
+
    low = 10000
    hi = 200000

                      
    -- A wrapper to enable the dependent generators for the max sizes
import           Generator.Delegation (genDCerts)
import           LedgerState (pattern UTxOState)
import           MockTypes (Addr, DCert, DPState, KeyPair, KeyPairs, Tx, TxBody, TxIn, TxOut, UTxO,
-
                     UTxOState)
+
                     UTxOState, VrfKeyPairs)
import           Slot (Slot (..))
import           STS.Ledger (LedgerEnv (..))
import           Tx (pattern Tx, pattern TxBody, pattern TxOut)
genTx :: LedgerEnv
      -> (UTxOState, DPState)
      -> KeyPairs
+
      -> VrfKeyPairs
      -> Gen Tx
-
genTx (LedgerEnv slot _ pparams _) (UTxOState utxo _ _ _, dpState) keys = do
+
genTx (LedgerEnv slot _ pparams _) (UTxOState utxo _ _ _, dpState) keys vrfKeys = do
  keys' <- Gen.shuffle keys

                      
  -- inputs

                      
  -- certificates
  (certs, certWitnesses, deposits_, refunds_)
-
    <- genDCerts keys' pparams dpState slotWithTTL
+
    <- genDCerts keys' vrfKeys pparams dpState slotWithTTL

                      
  -- attempt to make provision for certificate deposits (otherwise discard this generator)
  when (spendingBalance < deposits_) Gen.discard

                      
type VerKeyVRF = Keys.VerKeyVRF FakeVRF

                      
+
type VrfKeyPairs = [(SignKeyVRF, VerKeyVRF)]
+

                      
type CertifiedVRF = Keys.CertifiedVRF FakeVRF

                      
type KESig = Keys.KESig MockKES BHBody
import           LedgerState hiding (genDelegs)
import           PParams
import           Rules.ClassifyTraces (relevantCasesAreCovered)
-
import           Rules.TestLedger (credentialRemovedAfterDereg, rewardZeroAfterReg)
+
import           Rules.TestLedger (credentialRemovedAfterDereg, 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 \
+
                                 \appropriate state mappings"
+
                                 registeredPoolIsAdded
                  ]
                , testGroup "Ledger Genesis State"
                  [testProperty
import           Control.State.Transition.Trace (TraceOrder (OldestFirst), traceLength,
                     traceSignals)

                      
-
import           Delegation.Certificates (isDeRegKey, isRegKey)
+
import           Delegation.Certificates (isDeRegKey, isRegKey, isRegPool)
import           Generator.Core (mkGenesisLedgerState)
import           Generator.LedgerTrace ()
import           MockTypes (DCert, LEDGER, Tx)
        "there is at least 1 DeRegKey certificate for every 5 transactions"
        (traceLength tr <= 5 * length (filter isDeRegKey certs_))

                      
+
  cover 75
+
        "there is at least 1 RegPool certificate for every 20 transactions"
+
        (traceLength tr <= 20 * length (filter isRegPool certs_))
+

                      
  cover 25
        "at most 75% of transactions have no certificates"
        (0.75 >= noCertsRatio (certsByTx txs))
  ( rewardZeroAfterReg
  , credentialRemovedAfterDereg
  , consumedEqualsProduced
+
  , registeredPoolIsAdded
  )
where

                      
import           Data.Foldable (toList)
import           Data.Word (Word64)
+
import           Lens.Micro ((^.))

                      
import           Hedgehog (Property, forAll, property, withTests)

                      
import           Control.State.Transition.Generator (ofLengthAtLeast, trace,
                     traceOfLengthWithInitState)
import           Control.State.Transition.Trace (SourceSignalTarget (..), source,
-
                     sourceSignalTargets, target)
+
                     sourceSignalTargets, target, traceEnv)
import           Generator.Core (mkGenesisLedgerState)
import           Generator.LedgerTrace ()

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

                      
import           Test.Utils (assertAll)
          (balance u' + d' + fees' + foldl (+) (Coin 0) rewards')

                      

                      
+
-- | Check that a `RegPool` certificate properly adds a stake pool.
+
registeredPoolIsAdded :: Property
+
registeredPoolIsAdded = do
+
  withTests (fromIntegral numberOfTests) . property $ do
+
    tr <- forAll
+
          $ traceOfLengthWithInitState @LEDGER
+
                                     (fromIntegral traceLen)
+
                                     mkGenesisLedgerState
+
            `ofLengthAtLeast` 1
+
    TestPool.registeredPoolIsAdded
+
      (tr ^. traceEnv)
+
      (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 . _certs . _body $ 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.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 (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)
+
                     pattern StakePools, 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)