diff --git a/shelley/chain-and-ledger/executable-spec/delegation.cabal b/shelley/chain-and-ledger/executable-spec/delegation.cabal index 998b2ad98a3..c5467cb87b4 100644 --- a/shelley/chain-and-ledger/executable-spec/delegation.cabal +++ b/shelley/chain-and-ledger/executable-spec/delegation.cabal @@ -88,6 +88,8 @@ library microlens-th, mtl, non-integer, + stm, + transformers, cs-ledger, cardano-binary, cardano-crypto-class, diff --git a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs index 612d48bb089..cb984258dfd 100644 --- a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs +++ b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs @@ -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 @@ -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 diff --git a/shelley/chain-and-ledger/executable-spec/src/Cardano/Ledger/Shelley/API/Validation.hs b/shelley/chain-and-ledger/executable-spec/src/Cardano/Ledger/Shelley/API/Validation.hs index a46c6d3fcb3..83260bdfe45 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Cardano/Ledger/Shelley/API/Validation.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Cardano/Ledger/Shelley/API/Validation.hs @@ -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 diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index daa9dd7b4d1..c5b791d1ec9 100644 --- a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs +++ b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs @@ -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) @@ -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 @@ -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 @@ -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 @@ -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. @@ -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)] ] @@ -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 diff --git a/shelley/chain-and-ledger/executable-spec/src/OCert.hs b/shelley/chain-and-ledger/executable-spec/src/OCert.hs index 0e5efc9490e..7b09af0540f 100644 --- a/shelley/chain-and-ledger/executable-spec/src/OCert.hs +++ b/shelley/chain-and-ledger/executable-spec/src/OCert.hs @@ -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) @@ -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 diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs index 78719b889b9..cccdc066485 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs @@ -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 @@ -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 diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs index 61fc2a0fe37..de1d92a4a2e 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs @@ -18,7 +18,7 @@ where import Data.Set (Set) import Control.State.Transition - +import BaseTypes import BlockChain import Coin (Coin) import EpochBoundary @@ -58,6 +58,8 @@ instance type Environment (BBODY crypto) = BbodyEnv + type BaseM (BBODY crypto) = ShelleyBase + data PredicateFailure (BBODY crypto) = WrongBlockBodySizeBBODY | InvalidBodyHashBBODY diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Bhead.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Bhead.hs index e8164435220..8cc67b0e45d 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Bhead.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Bhead.hs @@ -13,7 +13,7 @@ module STS.Bhead where import Data.Set (Set) - +import BaseTypes import BlockChain import Keys import LedgerState @@ -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 @@ -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 @@ -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' } diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs index 364c8a307d6..3ea122bba34 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs @@ -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)) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Deleg.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Deleg.hs index 5205e844009..05bb9211fcf 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Deleg.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Deleg.hs @@ -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 @@ -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) @@ -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 @@ -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 @@ -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) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Delegs.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Delegs.hs index c6dff3f94f1..6bb3c720b36 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Delegs.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Delegs.hs @@ -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 @@ -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 @@ -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)) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Delpl.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Delpl.hs index 6fe6ab1b9c0..2ad1e8a3f23 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Delpl.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Delpl.hs @@ -11,6 +11,7 @@ module STS.Delpl ) where +import BaseTypes import Coin (Coin) import Delegation.Certificates import LedgerState @@ -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)) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Epoch.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Epoch.hs index 6199f4a220e..979f0ece3dd 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Epoch.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Epoch.hs @@ -10,6 +10,7 @@ module STS.Epoch ) where +import BaseTypes import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Set (Set) @@ -33,6 +34,7 @@ instance STS (EPOCH crypto) where type State (EPOCH crypto) = EpochState crypto type Signal (EPOCH crypto) = EpochNo type Environment (EPOCH crypto) = () + type BaseM (EPOCH crypto) = ShelleyBase data PredicateFailure (EPOCH crypto) = PoolReapFailure (PredicateFailure (POOLREAP crypto)) | SnapFailure (PredicateFailure (SNAP crypto)) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Ledger.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Ledger.hs index bc2307944fc..8c9b0a4d9fc 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Ledger.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ledger.hs @@ -15,7 +15,7 @@ module STS.Ledger where import Lens.Micro ((^.)) - +import BaseTypes import Cardano.Ledger.Shelley.Crypto import Coin (Coin) import Control.State.Transition @@ -51,6 +51,7 @@ instance = (UTxOState crypto, DPState crypto) type Signal (LEDGER crypto) = Tx crypto type Environment (LEDGER crypto) = LedgerEnv + type BaseM (LEDGER crypto) = ShelleyBase data PredicateFailure (LEDGER crypto) = UtxowFailure (PredicateFailure (UTXOW crypto)) | DelegsFailure (PredicateFailure (DELEGS crypto)) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Ledgers.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Ledgers.hs index 2cb658f85ad..222eb4c9016 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Ledgers.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ledgers.hs @@ -18,7 +18,7 @@ import Data.Foldable (toList) import qualified Data.Map.Strict as Map import Data.Sequence (Seq) import qualified Data.Set as Set - +import BaseTypes import Control.State.Transition import Cardano.Ledger.Shelley.Crypto @@ -50,6 +50,7 @@ instance type State (LEDGERS crypto) = LedgerState crypto type Signal (LEDGERS crypto) = Seq (Tx crypto) type Environment (LEDGERS crypto) = LedgersEnv + type BaseM (LEDGERS crypto) = ShelleyBase data PredicateFailure (LEDGERS crypto) = LedgerFailure (PredicateFailure (LEDGER crypto)) deriving (Show, Eq) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/NewEpoch.hs b/shelley/chain-and-ledger/executable-spec/src/STS/NewEpoch.hs index f2e4e0ecdd4..837e5d8ecad 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/NewEpoch.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/NewEpoch.hs @@ -12,14 +12,14 @@ where import qualified Data.Map.Strict as Map import Data.Maybe (catMaybes) - +import BaseTypes import Coin import EpochBoundary import LedgerState import Slot import TxData -import STS.EpochNo +import STS.Epoch import Delegation.Certificates @@ -36,6 +36,7 @@ instance Crypto crypto type State (NEWEPOCH crypto) = NewEpochState crypto type Signal (NEWEPOCH crypto) = EpochNo type Environment (NEWEPOCH crypto) = NewEpochEnv crypto + type BaseM (NEWEPOCH crypto) = ShelleyBase data PredicateFailure (NEWEPOCH crypto) = EpochFailure (PredicateFailure (EPOCH crypto)) deriving (Show, Eq) @@ -78,7 +79,7 @@ newEpochTransition = do pd' = Map.intersectionWith (,) sd (Map.map _poolVrf (_poolsSS ss)) - osched' = overlaySchedule e gkeys pp + osched' <- liftSTS $ overlaySchedule e gkeys pp pure $ NewEpochState e bcur @@ -94,7 +95,7 @@ instance Crypto crypto => Embed (EPOCH crypto) (NEWEPOCH crypto) where wrapFailed = EpochFailure -instance Crypto crypto - => HasTrace (NEWEPOCH crypto) where - envGen _ = undefined :: Gen (NewEpochEnv crypto) - sigGen _ _ = undefined :: Gen EpochNo +-- instance Crypto crypto +-- => HasTrace (NEWEPOCH crypto) where +-- envGen _ = undefined :: Gen (NewEpochEnv crypto) +-- sigGen _ _ = undefined :: Gen EpochNo diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Newpp.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Newpp.hs index 652db13ed54..588bcbc567a 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Newpp.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Newpp.hs @@ -11,7 +11,7 @@ module STS.Newpp where import qualified Data.Map.Strict as Map - +import BaseTypes import Lens.Micro ((^.)) import Coin @@ -22,6 +22,7 @@ import PParams import Slot import Updates import UTxO +import Control.Monad.Trans.Reader (asks) import Control.State.Transition @@ -37,6 +38,7 @@ instance STS (NEWPP crypto) where type State (NEWPP crypto) = NewppState crypto type Signal (NEWPP crypto) = EpochNo type Environment (NEWPP crypto) = NewppEnv crypto + type BaseM (NEWPP crypto) = ShelleyBase data PredicateFailure (NEWPP crypto) = FailureNEWPP deriving (Show, Eq) @@ -56,8 +58,10 @@ newPpTransition = do case ppNew of Just ppNew' -> do - let slot_ = firstSlotNo e - Coin oblgCurr = obligation pp (ds ^. stkCreds) (ps ^. stPools) slot_ + slot_ <- liftSTS $ do + ei <- asks epochInfo + epochInfoFirst ei e + let Coin oblgCurr = obligation pp (ds ^. stkCreds) (ps ^. stPools) slot_ Coin oblgNew = obligation ppNew' (ds ^. stkCreds) (ps ^. stPools) slot_ diff = oblgCurr - oblgNew Coin reserves = _reserves acnt diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Ocert.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Ocert.hs index 5b556f14f89..543f910f80b 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Ocert.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ocert.hs @@ -11,7 +11,7 @@ where import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Numeric.Natural (Natural) - +import BaseTypes import BlockChain import Keys import Ledger.Core ((⨃)) @@ -34,6 +34,7 @@ instance type Signal (OCERT crypto) = BHeader crypto type Environment (OCERT crypto) = OCertEnv crypto + type BaseM (OCERT crypto) = ShelleyBase data PredicateFailure (OCERT crypto) = KESBeforeStartOCERT | KESAfterEndOCERT @@ -58,8 +59,9 @@ ocertTransition = do let OCert vk_hot vk_cold n c0@(KESPeriod c0_) tau = bheaderOCert bhb hk = hashKey vk_cold s = bheaderSlotNo bhb - kp@(KESPeriod kp_) = kesPeriod s - t = kp_ - c0_ + kp@(KESPeriod kp_) <- liftSTS $ kesPeriod s + + let t = kp_ - c0_ c0 <= kp ?! KESBeforeStartOCERT kp_ < c0_ + 90 ?! KESAfterEndOCERT diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs index a0223cc2d39..dbeef72645f 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs @@ -62,6 +62,7 @@ instance = BHeader crypto type Environment (OVERLAY crypto) = OverlayEnv crypto + type BaseM (OVERLAY crypto) = ShelleyBase data PredicateFailure (OVERLAY crypto) = NotPraosLeaderOVERLAY diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Pool.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Pool.hs index d36d21ed603..87a04b799ce 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Pool.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Pool.hs @@ -18,10 +18,11 @@ import Lens.Micro ((^.)) import PParams import Slot import TxData - +import BaseTypes import Cardano.Ledger.Shelley.Crypto import Control.State.Transition import Control.State.Transition.Generator (HasTrace, envGen, sigGen) +import Control.Monad.Trans.Reader (asks) import Hedgehog (Gen) @@ -36,6 +37,7 @@ instance STS (POOL crypto) type State (POOL crypto) = PState crypto type Signal (POOL crypto) = DCert crypto type Environment (POOL crypto) = PoolEnv + type BaseM (POOL crypto) = ShelleyBase data PredicateFailure (POOL crypto) = StakePoolNotRegisteredOnKeyPOOL | StakePoolRetirementWrongEpochPOOL @@ -64,8 +66,10 @@ poolDelegationTransition = do } RetirePool hk (EpochNo e) -> do - let EpochNo cepoch = epochFromSlotNo slot - EpochNo maxEpoch = pp ^. eMax + EpochNo cepoch <- liftSTS $ do + ei <- asks epochInfo + epochInfoEpoch ei slot + let EpochNo maxEpoch = pp ^. eMax hk ∈ dom stPools_ ?! StakePoolNotRegisteredOnKeyPOOL @@ -91,7 +95,7 @@ m ⨃ (k,v) = Map.union (Map.singleton k v) m -> Map (KeyHash crypto) a m ∪ (k,v) = Map.union m (Map.singleton k v) -instance Crypto crypto - => HasTrace (POOL crypto) where - envGen _ = undefined :: Gen PoolEnv - sigGen _ _ = undefined :: Gen (DCert crypto) +-- instance Crypto crypto +-- => HasTrace (POOL crypto) where +-- envGen _ = undefined :: Gen PoolEnv +-- sigGen _ _ = undefined :: Gen (DCert crypto) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/PoolReap.hs b/shelley/chain-and-ledger/executable-spec/src/STS/PoolReap.hs index d893e793f20..ca16dd58da7 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/PoolReap.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/PoolReap.hs @@ -11,14 +11,14 @@ import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Lens.Micro ((^.)) - +import BaseTypes import Delegation.Certificates import EpochBoundary (poolRefunds) import LedgerState import PParams import Slot import TxData (_poolRAcnt) - +import Control.Monad.Trans.Reader (asks) import Control.State.Transition import Control.State.Transition.Generator (HasTrace, envGen, sigGen) @@ -40,6 +40,7 @@ instance STS (POOLREAP crypto) where type State (POOLREAP crypto) = PoolreapState crypto type Signal (POOLREAP crypto) = EpochNo type Environment (POOLREAP crypto) = PParams + type BaseM (POOLREAP crypto) = ShelleyBase data PredicateFailure (POOLREAP crypto) = FailurePOOLREAP deriving (Show, Eq) @@ -50,9 +51,12 @@ poolReapTransition :: TransitionRule (POOLREAP crypto) poolReapTransition = do TRC (pp, PoolreapState us a ds ps, e) <- judgmentContext + firstSlot <- liftSTS $ do + ei <- asks epochInfo + epochInfoFirst ei e let retired = dom $ (ps ^. retiring) ▷ Set.singleton e StakePools stPools' = ps ^. stPools - pr = poolRefunds pp (retired ◁ stPools') (firstSlotNo e) + pr = poolRefunds pp (retired ◁ stPools') firstSlot rewardAcnts = Map.map _poolRAcnt $ retired ◁ (ps ^. pParams) rewardAcnts' = Map.fromList . Map.elems $ Map.intersectionWith (,) rewardAcnts pr @@ -73,6 +77,6 @@ poolReapTransition = do , _retiring = retired ⋪ _retiring ps } -instance HasTrace (POOLREAP crypto) where - envGen _ = undefined :: Gen PParams - sigGen _ _ = undefined :: Gen EpochNo +-- instance HasTrace (POOLREAP crypto) where +-- envGen _ = undefined :: Gen PParams +-- sigGen _ _ = undefined :: Gen EpochNo diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs index ff2139f28d8..2231a59b8c2 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs @@ -19,6 +19,7 @@ import PParams import Slot import Updates +import Control.Monad.Trans.Reader (asks) import Control.State.Transition import Data.Ix (inRange) import Numeric.Natural (Natural) @@ -32,6 +33,7 @@ instance STS (PPUP crypto) where type State (PPUP crypto) = PPUpdate crypto type Signal (PPUP crypto) = PPUpdate crypto type Environment (PPUP crypto) = PPUPEnv crypto + type BaseM (PPUP crypto) = ShelleyBase data PredicateFailure (PPUP crypto) = NonGenesisUpdatePPUP (Set (GenKeyHash crypto)) (Set (GenKeyHash crypto)) | PPUpdateTooLatePPUP @@ -70,7 +72,10 @@ ppupTransitionNonEmpty = do (dom pup ⊆ dom _genDelegs) ?! NonGenesisUpdatePPUP (dom pup) (dom _genDelegs) - let EpochNo e = epochFromSlotNo s - s < firstSlotNo (EpochNo $ e + 1) *- slotsPrior ?! PPUpdateTooLatePPUP + firstSlotNextEpoch <- liftSTS $ do + ei <- asks epochInfo + EpochNo e <- epochInfoEpoch ei s + epochInfoFirst ei (EpochNo $ e + 1) + s < firstSlotNextEpoch *- slotsPrior ?! PPUpdateTooLatePPUP pure $ PPUpdate (pupS ⨃ Map.toList pup) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Prtcl.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Prtcl.hs index 393f1070c49..ad576ed4b17 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Prtcl.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Prtcl.hs @@ -79,6 +79,8 @@ instance type Environment (PRTCL crypto) = PrtclEnv crypto + type BaseM (PRTCL crypto) = ShelleyBase + data PredicateFailure (PRTCL crypto) = WrongSlotIntervalPRTCL | WrongBlockSequencePRTCL diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Rupd.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Rupd.hs index 2a5d6b41b22..29933e89572 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Rupd.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Rupd.hs @@ -7,12 +7,14 @@ module STS.Rupd ) where +import BaseTypes import BlockChain import EpochBoundary import LedgerState import Slot - +import Data.Functor ((<&>)) import Control.State.Transition +import Control.Monad.Trans.Reader (asks) data RUPD crypto @@ -21,8 +23,9 @@ data RupdEnv crypto instance STS (RUPD crypto) where type State (RUPD crypto) = Maybe (RewardUpdate crypto) - type Signal (RUPD crypto) = SlotNo.SlotNo + type Signal (RUPD crypto) = Slot.SlotNo type Environment (RUPD crypto) = RupdEnv crypto + type BaseM (RUPD crypto) = ShelleyBase data PredicateFailure (RUPD crypto) = FailureRUPD deriving (Show, Eq) @@ -33,9 +36,13 @@ instance STS (RUPD crypto) where rupdTransition :: TransitionRule (RUPD crypto) rupdTransition = do TRC (RupdEnv b es, ru, s) <- judgmentContext - let slot = firstSlotNo (epochFromSlotNo s) +* startRewards + (epoch, slot) <- liftSTS $ do + ei <- asks epochInfo + e <- epochInfoEpoch ei s + slot <- epochInfoFirst ei e <&> (+* startRewards) + return (e, slot) if s <= slot then pure ru else case ru of - Nothing -> pure $ Just (createRUpd b es) + Nothing -> Just <$> (liftSTS $ createRUpd epoch b es) Just _ -> pure ru diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Snap.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Snap.hs index 7a43996024b..cace33ce152 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Snap.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Snap.hs @@ -10,8 +10,9 @@ where import qualified Data.Map.Strict as Map +import Control.Monad.Trans.Reader (asks) import Lens.Micro ((^.)) - +import BaseTypes import Coin import EpochBoundary import LedgerState @@ -39,6 +40,7 @@ instance STS (SNAP crypto) where type State (SNAP crypto) = SnapState crypto type Signal (SNAP crypto) = EpochNo type Environment (SNAP crypto) = SnapEnv crypto + type BaseM (SNAP crypto) = ShelleyBase data PredicateFailure (SNAP crypto) = FailureSNAP deriving (Show, Eq) @@ -51,7 +53,9 @@ snapTransition :: TransitionRule (SNAP crypto) snapTransition = do TRC (SnapEnv pparams d p, SnapState s u, eNew) <- judgmentContext let pooledStake = stakeDistr (u ^. utxo) d p - let _slot = firstSlotNo eNew + _slot <- liftSTS $ do + ei <- asks epochInfo + epochInfoFirst ei eNew let oblg = obligation pparams (d ^. stkCreds) (p ^. stPools) _slot let decayed = (u ^. deposited) - oblg pure $ SnapState diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs index 7fb8c0e9733..0c71eb5abe0 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs @@ -10,6 +10,7 @@ module STS.Up ) where +import BaseTypes import Keys import PParams import Slot @@ -30,6 +31,7 @@ instance Crypto crypto => STS (UP crypto) where type State (UP crypto) = UpdateState crypto type Signal (UP crypto) = Update crypto type Environment (UP crypto) = UpdateEnv crypto + type BaseM (UP crypto) = ShelleyBase data PredicateFailure (UP crypto) = NonGenesisUpdateUP | AvupFailure (PredicateFailure (AVUP crypto)) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Updn.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Updn.hs index 8eca03e764f..9c6efb181a7 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Updn.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Updn.hs @@ -12,7 +12,7 @@ import BaseTypes import BlockChain import PParams import Slot - +import Control.Monad.Trans.Reader (asks) import Control.State.Transition data UPDN @@ -23,8 +23,10 @@ data UpdnState = UpdnState Nonce Nonce Nonce instance STS UPDN where type State UPDN = UpdnState - type Signal UPDN = SlotNo.SlotNo + type Signal UPDN = Slot.SlotNo type Environment UPDN = UpdnEnv + type BaseM UPDN = ShelleyBase + data PredicateFailure UPDN = FailureUPDN deriving (Show, Eq) initialRules = [pure (UpdnState (mkNonce 0) (mkNonce 0) (mkNonce 0))] @@ -33,11 +35,13 @@ instance STS UPDN where updTransition :: TransitionRule UPDN updTransition = do TRC (UpdnEnv eta pp ne, UpdnState eta_0 eta_v eta_c, s) <- judgmentContext - let EpochNo e = epochFromSlotNo s + ei <- liftSTS $ asks epochInfo + EpochNo e <- liftSTS $ epochInfoEpoch ei s + firstSlotNextEpoch <- liftSTS $ epochInfoFirst ei (EpochNo (e + 1)) pure $ UpdnState (if ne then eta_c ⭒ _extraEntropy pp else eta_0) (eta_v ⭒ eta) - (if s +* slotsPrior < firstSlotNo (EpochNo (e + 1)) + (if s +* slotsPrior < firstSlotNextEpoch then eta_v ⭒ eta else eta_c ) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs index ff1e086f9df..f67bfeb5383 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs @@ -18,7 +18,7 @@ import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Lens.Micro ((^.)) - +import BaseTypes import Coin import Delegation.Certificates import Keys @@ -57,6 +57,7 @@ instance type State (UTXO crypto) = UTxOState crypto type Signal (UTXO crypto) = Tx crypto type Environment (UTXO crypto) = UtxoEnv crypto + type BaseM (UTXO crypto) = ShelleyBase data PredicateFailure (UTXO crypto) = BadInputsUTxO | ExpiredUTxO SlotNo SlotNo @@ -108,8 +109,8 @@ utxoInductive = do txSize_ <= maxTxSize_ ?! MaxTxSizeUTxO txSize_ maxTxSize_ let refunded = keyRefunds pp stakeKeys txBody - decayed = decayedTx pp stakeKeys txBody - txCerts = toList $ txBody ^. certs + decayed <- liftSTS $ decayedTx pp stakeKeys txBody + let txCerts = toList $ txBody ^. certs depositChange = deposits pp stakePools txCerts - (refunded + decayed) @@ -125,10 +126,10 @@ instance Crypto crypto where wrapFailed = UpdateFailure -instance - ( Crypto crypto - , Signable (DSIGN crypto) (TxBody crypto) - ) - => HasTrace (UTXO crypto) where - envGen _ = undefined :: Gen (UtxoEnv crypto) - sigGen _ _ = undefined :: Gen (Tx crypto) +-- instance +-- ( Crypto crypto +-- , Signable (DSIGN crypto) (TxBody crypto) +-- ) +-- => HasTrace (UTXO crypto) where +-- envGen _ = undefined :: Gen (UtxoEnv crypto) +-- sigGen _ _ = undefined :: Gen (Tx crypto) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Utxow.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Utxow.hs index 3faf7c0fcc7..04906ad7c9e 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Utxow.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Utxow.hs @@ -16,7 +16,7 @@ import qualified Data.Map.Strict as Map import qualified Data.Sequence as Seq (filter) import qualified Data.Set as Set -import BaseTypes (intervalValue, (==>)) +import BaseTypes (ShelleyBase, intervalValue, (==>)) import Delegation.Certificates (isInstantaneousRewards) import Keys import Ledger.Core (dom, (∩)) @@ -45,6 +45,7 @@ instance type State (UTXOW crypto) = UTxOState crypto type Signal (UTXOW crypto) = Tx crypto type Environment (UTXOW crypto) = UtxoEnv crypto + type BaseM (UTXOW crypto) = ShelleyBase data PredicateFailure (UTXOW crypto) = InvalidWitnessesUTXOW | MissingVKeyWitnessesUTXOW @@ -114,10 +115,10 @@ instance where wrapFailed = UtxoFailure -instance - ( Crypto crypto - , Signable (DSIGN crypto) (TxBody crypto) - ) - => HasTrace (UTXOW crypto) where - envGen _ = undefined :: Gen (UtxoEnv crypto) - sigGen _ _ = undefined :: Gen (Tx crypto) +-- instance +-- ( Crypto crypto +-- , Signable (DSIGN crypto) (TxBody crypto) +-- ) +-- => HasTrace (UTXOW crypto) where +-- envGen _ = undefined :: Gen (UtxoEnv crypto) +-- sigGen _ _ = undefined :: Gen (Tx crypto)