Skip to content

Commit

Permalink
Use base monad
Browse files Browse the repository at this point in the history
  • Loading branch information
nc6 committed Dec 4, 2019
1 parent 3c0ea55 commit 3235ebb
Show file tree
Hide file tree
Showing 29 changed files with 201 additions and 106 deletions.
2 changes: 2 additions & 0 deletions shelley/chain-and-ledger/executable-spec/delegation.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,8 @@ library
microlens-th,
mtl,
non-integer,
stm,
transformers,
cs-ledger,
cardano-binary,
cardano-crypto-class,
Expand Down
17 changes: 17 additions & 0 deletions shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,18 +20,24 @@ module BaseTypes
, mkNonce
, (⭒)
, (==>)
-- * STS Base
, Globals (..)
, ShelleyBase
) where


import Cardano.Binary (ToCBOR (toCBOR), encodeListLen)
import Cardano.Crypto.Hash
import Cardano.Prelude (NoUnexpectedThunks (..))
import Cardano.Slotting.EpochInfo
import Data.Coerce (coerce)
import qualified Data.Fixed as FP (Fixed, HasResolution, resolution)
import Data.Ratio (denominator, numerator, (%))
import Data.Word (Word64, Word8)
import GHC.Generics (Generic)
import Numeric.Natural (Natural)
import Control.Monad.Trans.Reader
import Control.Monad.STM

data E34

Expand Down Expand Up @@ -111,3 +117,14 @@ newtype Seed = Seed (Hash SHA256 Seed)
(==>) :: Bool -> Bool -> Bool
a ==> b = not a || b
infix 1 ==>

--------------------------------------------------------------------------------
-- Base monad for all STS systems
--------------------------------------------------------------------------------

data Globals = Globals
{ epochInfo :: EpochInfo ShelleyBase
, slotsPerKESPeriod :: Word64
}

type ShelleyBase = ReaderT Globals STM
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ import qualified Cardano.Crypto.DSIGN as DSIGN
import Cardano.Ledger.Shelley.Crypto
import Control.Arrow (left, right)
import Control.Monad.Except
import Control.State.Transition (TRC (..), applySTS)
import Control.State.Transition.Extended (TRC (..), applySTS)
import Ledger.Core (Relation (..))
import qualified LedgerState
import qualified STS.Bbody as STS
Expand Down
62 changes: 37 additions & 25 deletions shelley/chain-and-ledger/executable-spec/src/LedgerState.hs
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,8 @@ import Address (mkRwdAcnt)
import Cardano.Ledger.Shelley.Crypto
import Cardano.Prelude (NoUnexpectedThunks (..))
import Coin (Coin (..))
import Data.Foldable (toList)
import Control.Monad.Trans.Reader (asks)
import Data.Foldable (asum, toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe)
Expand Down Expand Up @@ -134,8 +135,8 @@ import Delegation.Certificates (DCert (..), PoolDistr (..), StakeCreds
StakePools (..), cwitness, decayKey, refund)
import Delegation.PoolParams (poolSpec)

import BaseTypes (UnitInterval, intervalValue, mkUnitInterval)

import BaseTypes (ShelleyBase, Globals(..), UnitInterval, intervalValue, mkUnitInterval)
import Cardano.Slotting.EpochInfo
import Ledger.Core (dom, (∪), (∪+), (⋪), (▷), (◁))

-- | Representation of a list of pairs of key pairs, e.g., pay and stake keys
Expand Down Expand Up @@ -451,30 +452,34 @@ decayedKey
-> StakeCreds crypto
-> SlotNo
-> DCert crypto
-> Coin
-> ShelleyBase Coin
decayedKey pp stk@(StakeCreds stkcreds) cslot cert =
case cert of
DeRegKey key ->
if Map.notMember key stkcreds
then 0
else let created' = stkcreds Map.! key in
let start = max (firstSlotNo $ epochFromSlotNo cslot) created' in
let dval = pp ^. keyDeposit in
let dmin = pp ^. keyMinRefund in
let lambda = pp ^. keyDecayRate in
let epochRefund = keyRefund dval dmin lambda stk start cert in
let currentRefund = keyRefund dval dmin lambda stk cslot cert in
epochRefund - currentRefund
_ -> 0
then pure 0
else do
let created' = stkcreds Map.! key
start <- do
ei <- asks epochInfo
fs <- epochInfoFirst ei =<< epochInfoEpoch ei cslot
pure $ max fs created'
let dval = pp ^. keyDeposit
dmin = pp ^. keyMinRefund
lambda = pp ^. keyDecayRate
epochRefund = keyRefund dval dmin lambda stk start cert
currentRefund = keyRefund dval dmin lambda stk cslot cert
pure $ epochRefund - currentRefund
_ -> pure 0

-- | Decayed deposit portions
decayedTx
:: PParams
-> StakeCreds crypto
-> TxBody crypto
-> Coin
-> ShelleyBase Coin
decayedTx pp stk tx =
sum [decayedKey pp stk (tx ^. ttl) c | c@(DeRegKey _) <- toList $ tx ^. certs]
asum [decayedKey pp stk (tx ^. ttl) c | c@(DeRegKey _) <- toList $ tx ^. certs]

-- |Compute the lovelace which are destroyed by the transaction
consumed
Expand Down Expand Up @@ -856,12 +861,14 @@ applyRUpd ru (EpochState as ss ls pp) = EpochState as' ss ls' pp

-- | Create a reward update
createRUpd
:: BlocksMade crypto
:: EpochNo
-> BlocksMade crypto
-> EpochState crypto
-> RewardUpdate crypto
createRUpd b@(BlocksMade b') (EpochState acnt ss ls pp) =
RewardUpdate (Coin $ deltaT1 + deltaT2) (-deltaR') rs' (-(_feeSS ss)) registered
where Coin reserves' = _reserves acnt
-> ShelleyBase (RewardUpdate crypto)
createRUpd e b@(BlocksMade b') (EpochState acnt ss ls pp) = do
ei <- asks epochInfo
slotsPerEpoch <- epochInfoSize ei e
let Coin reserves' = _reserves acnt

ds = _dstate $ _delegationState ls
rewards' = _rewards ds
Expand Down Expand Up @@ -891,6 +898,7 @@ createRUpd b@(BlocksMade b') (EpochState acnt ss ls pp) =

blocksMade = fromIntegral $ Map.foldr (+) 0 b' :: Integer
expectedBlocks = intervalValue (_activeSlotCoeff pp) * fromIntegral slotsPerEpoch
pure $ RewardUpdate (Coin $ deltaT1 + deltaT2) (-deltaR') rs' (-(_feeSS ss)) registered

-- | Overlay schedule
-- This is just a very simple round-robin, evenly spaced schedule.
Expand All @@ -899,16 +907,19 @@ overlaySchedule
:: EpochNo
-> Set (GenKeyHash crypto)
-> PParams
-> Map SlotNo (Maybe (GenKeyHash crypto))
overlaySchedule e gkeys pp = Map.union active inactive
where
-> ShelleyBase (Map SlotNo (Maybe (GenKeyHash crypto)))
overlaySchedule e gkeys pp = do
ei <- asks epochInfo
slotsPerEpoch <- epochInfoSize ei e
firstSlotNo <- epochInfoFirst ei e
let
numActive = dval * fromIntegral slotsPerEpoch
dval = intervalValue $ pp ^. d
dInv = 1 / dval
asc = intervalValue $ pp ^. activeSlotCoeff

toRelativeSlotNo x = (Duration . floor) (dInv * fromInteger x)
toSlotNo x = firstSlotNo e +* toRelativeSlotNo x
toSlotNo x = firstSlotNo +* toRelativeSlotNo x

genesisSlots = [ toSlotNo x | x <-[0..(floor numActive)] ]

Expand All @@ -924,6 +935,7 @@ overlaySchedule e gkeys pp = Map.union active inactive
Map.fromList $ fmap
(\x -> (snd x, Nothing))
(filter (not . fst) unassignedSched)
pure $ Map.union active inactive

-- | Update new epoch state
updateNES
Expand Down
12 changes: 6 additions & 6 deletions shelley/chain-and-ledger/executable-spec/src/OCert.hs
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,10 @@ import GHC.Generics (Generic)
import Cardano.Ledger.Shelley.Crypto
import Keys (KeyHash, Sig, VKey, VKeyES)
import Slot (SlotNo (..))

import BaseTypes
import Numeric.Natural (Natural)
import Control.Monad.Trans.Reader (asks)
import Data.Functor ((<&>))

data OCertEnv crypto = OCertEnv
{ ocertEnvStPools :: Set (KeyHash crypto)
Expand Down Expand Up @@ -83,8 +85,6 @@ instance
<*> fromCBOR
<*> fromCBOR

slotsPerKESPeriod :: Natural
slotsPerKESPeriod = 90

kesPeriod :: SlotNo -> KESPeriod
kesPeriod (SlotNo s) = KESPeriod $ s `div` slotsPerKESPeriod
kesPeriod :: SlotNo -> ShelleyBase KESPeriod
kesPeriod (SlotNo s) = asks slotsPerKESPeriod <&> \spkp ->
KESPeriod . fromIntegral $ s `div` spkp
3 changes: 2 additions & 1 deletion shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ where

import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

import BaseTypes
import BlockChain
import Keys
import Slot
Expand All @@ -37,6 +37,7 @@ instance STS (AVUP crypto) where
= AVUPState crypto
type Signal (AVUP crypto) = AVUpdate crypto
type Environment (AVUP crypto) = AVUPEnv crypto
type BaseM (AVUP crypto) = ShelleyBase
data PredicateFailure (AVUP crypto)
= EmptyAVUP
| NonEmptyAVUP
Expand Down
4 changes: 3 additions & 1 deletion shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ where
import Data.Set (Set)

import Control.State.Transition

import BaseTypes
import BlockChain
import Coin (Coin)
import EpochBoundary
Expand Down Expand Up @@ -58,6 +58,8 @@ instance

type Environment (BBODY crypto) = BbodyEnv

type BaseM (BBODY crypto) = ShelleyBase

data PredicateFailure (BBODY crypto)
= WrongBlockBodySizeBBODY
| InvalidBodyHashBBODY
Expand Down
10 changes: 8 additions & 2 deletions shelley/chain-and-ledger/executable-spec/src/STS/Bhead.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ module STS.Bhead
where

import Data.Set (Set)

import BaseTypes
import BlockChain
import Keys
import LedgerState
Expand All @@ -23,6 +23,7 @@ import STS.NewEpoch
import STS.Rupd
import Cardano.Ledger.Shelley.Crypto
import Control.State.Transition
import Control.Monad.Trans.Reader (asks)

data BHEAD crypto

Expand All @@ -37,6 +38,7 @@ instance Crypto crypto
type Signal (BHEAD crypto)
= BHeader crypto
type Environment (BHEAD crypto) = BheadEnv crypto
type BaseM (BHEAD crypto) = ShelleyBase
data PredicateFailure (BHEAD crypto)
= HeaderSizeTooLargeBHEAD
| BlockSizeTooLargeBHEAD
Expand All @@ -60,8 +62,12 @@ bheadTransition = do
fromIntegral (bHeaderSize bh) < _maxBHSize pp ?! HeaderSizeTooLargeBHEAD
fromIntegral (hBbsize bhb) < _maxBBSize pp ?! BlockSizeTooLargeBHEAD

epoch <- liftSTS $ do
ei <- asks epochInfo
epochInfoEpoch ei slot

nes' <- trans @(NEWEPOCH crypto)
$ TRC (NewEpochEnv slot gkeys, nes, epochFromSlotNo slot)
$ TRC (NewEpochEnv slot gkeys, nes, epoch)

ru' <- trans @(RUPD crypto) $ TRC (RupdEnv bprev es, nesRu nes', slot)
let nes'' = nes' { nesRu = ru' }
Expand Down
1 change: 1 addition & 0 deletions shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ instance
= Block crypto

type Environment (CHAIN crypto) = SlotNo
type BaseM (CHAIN crypto) = ShelleyBase

data PredicateFailure (CHAIN crypto)
= BbodyFailure (PredicateFailure (BBODY crypto))
Expand Down
19 changes: 12 additions & 7 deletions shelley/chain-and-ledger/executable-spec/src/STS/Deleg.hs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ where

import qualified Data.Map.Strict as Map
import qualified Data.Set as Set

import BaseTypes
import BlockChain (slotsPrior)
import Coin (Coin (..))
import Delegation.Certificates
Expand All @@ -20,6 +20,7 @@ import LedgerState
import Slot
import TxData

import Control.Monad.Trans.Reader (asks)
import Cardano.Ledger.Shelley.Crypto
import Control.State.Transition
import Control.State.Transition.Generator (HasTrace, envGen, sigGen)
Expand All @@ -41,6 +42,7 @@ instance STS (DELEG crypto)
type State (DELEG crypto) = DState crypto
type Signal (DELEG crypto) = DCert crypto
type Environment (DELEG crypto) = DelegEnv
type BaseM (DELEG crypto) = ShelleyBase
data PredicateFailure (DELEG crypto)
= StakeKeyAlreadyRegisteredDELEG
| StakeKeyNotRegisteredDELEG
Expand Down Expand Up @@ -102,8 +104,11 @@ delegationTransition = do
InstantaneousRewards credCoinMap -> do
let combinedMap = Map.union credCoinMap (_irwd ds)
requiredForRewards = foldl (+) (Coin 0) (range combinedMap)
EpochNo currEpoch = epochFromSlotNo slot_
slot_ < (firstSlotNo $ EpochNo (currEpoch + 1)) *- slotsPrior
firstSlot <- liftSTS $ do
ei <- asks epochInfo
EpochNo currEpoch <- epochInfoEpoch ei slot_
epochInfoFirst ei $ EpochNo (currEpoch + 1)
slot_ < firstSlot *- slotsPrior
?! MIRCertificateTooLateinEpochDELEG
requiredForRewards <= reserves_ ?! InsufficientForInstantaneousRewardsDELEG

Expand All @@ -114,7 +119,7 @@ delegationTransition = do
pure ds


instance Crypto crypto
=> HasTrace (DELEG crypto) where
envGen _ = undefined :: Gen DelegEnv
sigGen _ _ = undefined :: Gen (DCert crypto)
-- instance Crypto crypto
-- => HasTrace (DELEG crypto) where
-- envGen _ = undefined :: Gen DelegEnv
-- sigGen _ _ = undefined :: Gen (DCert crypto)
11 changes: 6 additions & 5 deletions shelley/chain-and-ledger/executable-spec/src/STS/Delegs.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ where
import qualified Data.Set as Set

import Data.Sequence (Seq (..))

import BaseTypes
import Coin (Coin)
import Delegation.Certificates
import LedgerState
Expand Down Expand Up @@ -52,6 +52,7 @@ instance
type State (DELEGS crypto) = DPState crypto
type Signal (DELEGS crypto) = Seq (DCert crypto)
type Environment (DELEGS crypto) = DelegsEnv crypto
type BaseM (DELEGS crypto) = ShelleyBase
data PredicateFailure (DELEGS crypto)
= DelegateeNotRegisteredDELEG
| WithrawalsNotInRewardsDELEGS
Expand Down Expand Up @@ -104,7 +105,7 @@ instance
wrapFailed = DelplFailure


instance Crypto crypto
=> HasTrace (DELEGS crypto) where
envGen _ = undefined :: Gen (DelegsEnv crypto)
sigGen _ _ = undefined :: Gen (Seq (DCert crypto))
-- instance Crypto crypto
-- => HasTrace (DELEGS crypto) where
-- envGen _ = undefined :: Gen (DelegsEnv crypto)
-- sigGen _ _ = undefined :: Gen (Seq (DCert crypto))
2 changes: 2 additions & 0 deletions shelley/chain-and-ledger/executable-spec/src/STS/Delpl.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ module STS.Delpl
)
where

import BaseTypes
import Coin (Coin)
import Delegation.Certificates
import LedgerState
Expand Down Expand Up @@ -41,6 +42,7 @@ instance
type State (DELPL crypto) = DPState crypto
type Signal (DELPL crypto) = DCert crypto
type Environment (DELPL crypto) = DelplEnv
type BaseM (DELPL crypto) = ShelleyBase
data PredicateFailure (DELPL crypto)
= PoolFailure (PredicateFailure (POOL crypto))
| DelegFailure (PredicateFailure (DELEG crypto))
Expand Down
Loading

0 comments on commit 3235ebb

Please sign in to comment.