diff --git a/shelley/chain-and-ledger/executable-spec/delegation.cabal b/shelley/chain-and-ledger/executable-spec/delegation.cabal index a88a16b7396..88dfae2168b 100644 --- a/shelley/chain-and-ledger/executable-spec/delegation.cabal +++ b/shelley/chain-and-ledger/executable-spec/delegation.cabal @@ -29,6 +29,8 @@ library Delegation.PoolParams Delegation.Certificates OCert + Updates + STS.Avup STS.Bbody STS.Bhead STS.Chain @@ -41,10 +43,14 @@ library STS.NewEpoch STS.Newpp STS.Ocert + STS.Overlay STS.Pool STS.PoolReap + STS.Ppup + STS.Prtcl STS.Rupd STS.Snap + STS.Up STS.Updn STS.Utxo STS.Utxow diff --git a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs index 409e0674fb0..3ccedae1b66 100644 --- a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs +++ b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs @@ -9,17 +9,14 @@ module BaseTypes , intervalValue , interval0 , interval1 - , Seed + , Seed(..) , mkNonce , seedOp , neutralSeed - , EEnt(..) ) where -import qualified Data.Map.Strict as Map import qualified Data.Fixed as FP -import qualified Keys as Keys data E34 @@ -59,6 +56,8 @@ interval1 = UnitInterval 1 data Seed = Nonce Integer | NeutralSeed + | SeedL + | SeedEta | SeedOp Seed Seed deriving (Show, Eq, Ord) @@ -73,7 +72,3 @@ neutralSeed = NeutralSeed mkNonce :: Integer -> Seed mkNonce = Nonce - --- | Extra entropy -newtype EEnt = EEnt (Map.Map Keys.VKeyGenesis Seed) - deriving (Show, Ord, Eq) diff --git a/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs b/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs index da6d2065838..3c0eb8ba791 100644 --- a/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs @@ -4,9 +4,11 @@ module BlockChain , BHeader(..) , Block(..) , bhHash + , bhbHash , bHeaderSize , bBodySize , slotToSeed + , hBbsize -- accessor functions , bheader , bhbody @@ -18,33 +20,65 @@ module BlockChain , verifyVrf , seedEta , seedL - ) where - -import Crypto.Hash (Digest, SHA256, hash) -import qualified Data.ByteArray as BA -import qualified Data.ByteString.Char8 as BS + , bvkcold + , vrfChecks + , incrBlocks + ) +where + +import Crypto.Hash ( Digest + , SHA256 + , hash + ) +import qualified Data.ByteArray as BA +import qualified Data.ByteString.Char8 as BS +import Numeric.Natural ( Natural ) +import Data.Ratio +import qualified Data.Map.Strict as Map import BaseTypes -import qualified Keys as Keys +import Delegation.Certificates +import EpochBoundary +import qualified Keys as Keys import OCert -import qualified Slot as Slot -import qualified UTxO as U +import qualified Slot as Slot +import qualified UTxO as U + +import NonIntegral ( (***) ) --- |The hash of public Key +-- |The hash of a Block Header newtype HashHeader = HashHeader (Digest SHA256) deriving (Show, Eq, Ord) +-- | Hash of block body +newtype HashBBody = + HashBBody (Digest SHA256) + deriving (Show, Eq, Ord) + -- |Hash a given block header bhHash :: BHeader -> HashHeader bhHash = HashHeader . hash +-- |Hash a given block header +bhbHash :: BHBody -> HashBBody +bhbHash = HashBBody . hash + instance BA.ByteArrayAccess BHeader where length = BA.length . BS.pack . show withByteArray = BA.withByteArray . BS.pack . show +instance BA.ByteArrayAccess BHBody where + length = BA.length . BS.pack . show + withByteArray = BA.withByteArray . BS.pack . show + +-- | TODO: This is just a mock implementation wihtout too much insight into how +-- VRF actually will work. +class VrfProof a where + toSeed :: a -> Seed + data Proof a = - Proof Keys.VKey Seed + Proof Keys.VKey a deriving (Show, Eq) data BHeader = @@ -69,6 +103,10 @@ data BHBody = BHBody , bheaderPrfL :: Proof UnitInterval -- | signature of block body , bheaderBlockSignature :: Keys.Sig [U.Tx] + -- | Size of the block body + , bsize :: Natural + -- | Hash of block body + , bhash :: HashBBody -- | operational certificate , bheaderOCert :: OCert } deriving (Show, Eq) @@ -105,11 +143,53 @@ slotsPrior = 33 -- one third of slots per epoch startRewards :: Slot.Duration startRewards = 33 -- see above -verifyVrf :: Keys.VKey -> Seed -> Proof a -> Bool -verifyVrf vk seed (Proof k s) = vk == k && seed == s +verifyVrf :: VrfProof a => Keys.VKey -> Seed -> Proof a -> Bool +verifyVrf vk seed (Proof k s) = vk == k && seed == toSeed s + +instance VrfProof Seed where + toSeed = id + +instance VrfProof UnitInterval where + toSeed u = mkNonce $ (numerator r * denominator r) + where r = intervalValue u + +vrfChecks :: Seed -> PoolDistr -> UnitInterval -> BHBody -> Bool +vrfChecks eta0 (PoolDistr pd) f bhb = + let sigma' = Map.lookup hk pd + in case sigma' of + Nothing -> False + Just sigma -> + verifyVrf vk ((eta0 `seedOp` ss) `seedOp` SeedEta) (bheaderPrfEta bhb) + && verifyVrf vk + ((eta0 `seedOp` ss) `seedOp` SeedL) + (bheaderPrfL bhb) + && intervalValue (bheaderL bhb) + < 1 + - ((1 - activeSlotsCoeff) *** (fromRational sigma)) + where + vk = bvkcold bhb + hk = Keys.hashKey vk + ss = slotToSeed $ bheaderSlot bhb + f' = intervalValue f + activeSlotsCoeff = + (fromIntegral $ numerator f') / (fromIntegral $ denominator f') seedEta :: Seed seedEta = mkNonce 0 seedL :: Seed seedL = mkNonce 1 + +bvkcold :: BHBody -> Keys.VKey +bvkcold bhb = ocertVkCold $ bheaderOCert bhb + +hBbsize :: BHBody -> Natural +hBbsize = bsize + +incrBlocks :: Bool -> Keys.HashKey -> BlocksMade -> BlocksMade +incrBlocks isOverlay hk b'@(BlocksMade b) + | isOverlay = b' + | otherwise = BlocksMade $ case hkVal of + Nothing -> Map.insert hk 1 b + Just n -> Map.insert hk (n + 1) b + where hkVal = Map.lookup hk b diff --git a/shelley/chain-and-ledger/executable-spec/src/Keys.hs b/shelley/chain-and-ledger/executable-spec/src/Keys.hs index 0055060e152..91017abaca3 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Keys.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Keys.hs @@ -59,7 +59,7 @@ verifyKES :: Eq a => VKey -> a -> KESig a -> Natural -> Bool verifyKES (VKey vk) vd (KESig (Sig sd sk) m) n = vk == sk && vd == sd && m == n newtype Dms = Dms (Map.Map VKeyGenesis VKey) - deriving (Show, Eq) + deriving (Show, Ord, Eq) newtype GKeys = GKeys (Set.Set VKeyGenesis) - deriving (Show, Eq) + deriving (Show, Ord, Eq) diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index 905832c52df..3c38ba99c75 100644 --- a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs +++ b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs @@ -40,7 +40,6 @@ module LedgerState , emptyAccount , emptyPState , emptyDState - , emptyUPIState , poolRAcnt , treasury , reserves @@ -69,18 +68,15 @@ module LedgerState , validStakeDelegation , preserveBalance , verifiedWits - , enoughWits - , noUnneededWits + , witsNeeded -- lenses , utxoState , delegationState - , pcs - , current -- UTxOState , utxo , deposited , fees - , eEntropy + , ups -- DelegationState , rewards , stKeys @@ -108,6 +104,9 @@ module LedgerState , NewEpochState(..) , NewEpochEnv(..) , overlaySchedule + , getGKeys + , setIssueNumbers + , updateNES ) where import Control.Monad (foldM) @@ -131,6 +130,7 @@ import PParams (PParams(..), minfeeA, minfeeB, keyDeposit, keyMinRefund, keyDecayRate, emptyPParams) import EpochBoundary +import qualified Updates import Delegation.Certificates (DCert (..), refund, getRequiredSigningKey, StakeKeys(..), StakePools(..), decayKey, PoolDistr(..)) import Delegation.PoolParams (Delegation (..), PoolParams (..), @@ -139,8 +139,6 @@ import Delegation.PoolParams (Delegation (..), PoolParams (..), import BaseTypes -import qualified Ledger.Update as Byron.Update (UPIState, emptyUPIState) - -- | Representation of a list of pairs of key pairs, e.g., pay and stake keys type KeyPairs = [(KeyPair, KeyPair)] @@ -168,8 +166,6 @@ data ValidationError = | InvalidWitness -- | The transaction does not have the required witnesses. | MissingWitnesses - -- | The transaction includes a redundant witness. - | UnneededWitnesses -- | Missing Replay Attack Protection, at least one input must be spent. | InputSetEmpty -- | A stake key cannot be registered again. @@ -264,13 +260,11 @@ emptyEpochState = EpochState emptyAccount emptySnapShots emptyLedgerState emptyPParams emptyLedgerState :: LedgerState -emptyLedgerState = LedgerState - (UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) (EEnt Map.empty)) - emptyDelegation - emptyUPIState - emptyPParams - 0 - (Slot 0) +emptyLedgerState = + LedgerState + (UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) Updates.emptyUpdateState) + emptyDelegation + 0 emptyAccount :: AccountState emptyAccount = AccountState (Coin 0) (Coin 0) @@ -289,21 +283,15 @@ emptyPState = data UTxOState = UTxOState - { - _utxo :: !UTxO + { _utxo :: !UTxO , _deposited :: Coin , _fees :: Coin - , _eEntropy :: EEnt + , _ups :: ( Updates.PPUpdate + , Updates.AVUpdate + , Map.Map Slot Updates.Applications + , Updates.Applications) } deriving (Show, Eq) --- | For now this contains the Byron `UPIState` and the Shelley PParams --- separately. -data UPIState = UPIState Byron.Update.UPIState PParams - deriving (Show, Eq) - -emptyUPIState :: UPIState -emptyUPIState = UPIState Byron.Update.emptyUPIState emptyPParams - -- | New Epoch state and environment data NewEpochState = NewEpochState { @@ -317,6 +305,12 @@ data NewEpochState = , nesOsched :: Map.Map Slot (Maybe VKeyGenesis) } deriving (Show, Eq) +getGKeys :: NewEpochState -> Set VKeyGenesis +getGKeys nes = Map.keysSet dms + where NewEpochState _ _ _ _ es _ _ _ = nes + EpochState _ _ ls _ = es + LedgerState _ (DPState (DState _ _ _ _ (Dms dms)) _) _ = ls + data NewEpochEnv = NewEpochEnv { neeEta1 :: Seed @@ -331,13 +325,8 @@ data LedgerState = _utxoState :: !UTxOState -- |The current delegation state , _delegationState :: !DPState - -- | UPIState - , upiState :: !UPIState - -- |The current protocol constants. - , _pcs :: !PParams - -- | The current transaction index in the current slot. - , _txSlotIx :: Ix - , _currentSlot :: Slot + -- |The current transaction index in the current slot. +, _txSlotIx :: Ix } deriving (Show, Eq) makeLenses ''DPState @@ -350,23 +339,28 @@ makeLenses ''LedgerState -- |The transaction Id for 'UTxO' included at the beginning of a new ledger. genesisId :: TxId genesisId = - TxId $ hash (TxBody Set.empty [] [] Map.empty (Coin 0) (Slot 0) (EEnt Map.empty)) + TxId $ hash + (TxBody + Set.empty + [] + [] + Map.empty + (Coin 0) + (Slot 0) + Updates.emptyUpdate) -- |Creates the ledger state for an empty ledger which -- contains the specified transaction outputs. genesisState :: PParams -> [TxOut] -> LedgerState -genesisState pc outs = LedgerState +genesisState _ outs = LedgerState (UTxOState (UTxO $ Map.fromList [(TxIn genesisId idx, out) | (idx, out) <- zip [0..] outs]) (Coin 0) (Coin 0) - (EEnt Map.empty)) + Updates.emptyUpdateState) emptyDelegation - emptyUPIState - pc 0 - (Slot 0) -- | Determine if the transaction has expired current :: TxBody -> Slot -> Validity @@ -486,28 +480,26 @@ correctWithdrawals accs withdrawals = -- |Collect the set of hashes of keys that needs to sign a -- given transaction. This set consists of the txin owners, -- certificate authors, and withdrawal reward accounts. -witsNeeded :: UTxO -> TxBody -> Dms -> Set HashKey -witsNeeded utxo' tx (Dms d) = +witsNeeded :: UTxO -> Tx -> Dms -> Set HashKey +witsNeeded utxo' tx@(Tx txbody _) _dms = inputAuthors `Set.union` wdrlAuthors `Set.union` certAuthors `Set.union` - owners `Set.union` - genEEntropy + updateKeys `Set.union` + owners where - inputAuthors = Set.foldr insertHK Set.empty (tx ^. inputs) + inputAuthors = Set.foldr insertHK Set.empty (txbody ^. inputs) insertHK txin hkeys = case txinLookup txin utxo' of Just (TxOut (AddrTxin pay _) _) -> Set.insert pay hkeys _ -> hkeys - wdrlAuthors = Set.map getRwdHK (Map.keysSet (tx ^. wdrls)) - owners = foldl Set.union Set.empty [pool ^. poolOwners | RegPool pool <- tx ^. certs] - certAuthors = Set.fromList (fmap getCertHK (tx ^. certs)) + wdrlAuthors = Set.map getRwdHK (Map.keysSet (txbody ^. wdrls)) + owners = foldl Set.union Set.empty + [pool ^. poolOwners | RegPool pool <- txbody ^. certs] + certAuthors = Set.fromList (fmap getCertHK (txbody ^. certs)) getCertHK cert = hashKey $ getRequiredSigningKey cert - EEnt eent = _txeent tx - genEEntropy = Set.fromList $ - Map.elems $ Map.map hashKey $ Map.restrictKeys d (Map.keysSet eent) - + updateKeys = propWits (txup tx) _dms -- |Given a ledger state, determine if the UTxO witnesses in a given -- transaction are correct. @@ -523,22 +515,13 @@ verifiedWits (Tx tx wits) = -- from the same address are used, it is not strictly necessary to include more -- than one witness. enoughWits :: Tx -> Dms -> UTxOState -> Validity -enoughWits (Tx tx wits) d u = +enoughWits tx@(Tx _ wits) d u = if witsNeeded (u ^. utxo) tx d `Set.isSubsetOf` signers then Valid else Invalid [MissingWitnesses] where signers = Set.map (\(Wit vkey _) -> hashKey vkey) wits --- |Check that there are no redundant witnesses. -noUnneededWits :: Tx -> Dms -> UTxOState -> Validity -noUnneededWits (Tx tx wits) d u = - if signers `Set.isSubsetOf` witsNeeded (u ^. utxo) tx d - then Valid - else Invalid [UnneededWitnesses] - where - signers = Set.map (\(Wit vkey _) -> hashKey vkey) wits - validRuleUTXO :: RewardAccounts -> StakePools @@ -559,14 +542,21 @@ validRuleUTXO accs stakePools stakeKeys pc slot tx u = validRuleUTXOW :: Tx -> Dms -> LedgerState -> Validity validRuleUTXOW tx d l = verifiedWits tx <> enoughWits tx d (l ^. utxoState) - <> noUnneededWits tx d (l ^. utxoState) -validTx :: Tx -> Dms -> Slot -> LedgerState -> Validity -validTx tx d slot l = +-- | Calculate the set of hash keys of the required witnesses for update +-- proposals. +propWits :: Updates.Update -> Dms -> Set.Set HashKey +propWits (Updates.Update (Updates.PPUpdate pup) (Updates.AVUpdate aup)) (Dms _dms) = + Set.fromList $ Map.elems $ Map.map hashKey updateKeys + where updateKeys = + Map.restrictKeys _dms (Map.keysSet pup `Set.union` Map.keysSet aup) + +validTx :: Tx -> Dms -> Slot -> PParams -> LedgerState -> Validity +validTx tx d slot pp l = validRuleUTXO (l ^. delegationState . dstate . rewards) (l ^. delegationState . pstate . stPools) (l ^. delegationState . dstate . stKeys) - (l ^. pcs) + pp slot (tx ^. body) (l ^. utxoState) @@ -627,13 +617,18 @@ validDelegation cert ds = -- apply the transaction as a state transition function on the ledger state. -- Otherwise, return a list of validation errors. asStateTransition - :: Slot -> LedgerState -> Tx -> Dms -> Either [ValidationError] LedgerState -asStateTransition slot ls tx d = - case validTx tx d slot ls of + :: Slot + -> PParams + -> LedgerState + -> Tx + -> Dms + -> Either [ValidationError] LedgerState +asStateTransition slot pp ls tx d = + case validTx tx d slot pp ls of Invalid errors -> Left errors Valid -> foldM (certAsStateTransition slot (ls ^. txSlotIx)) ls' cs where - ls' = applyTxBody slot ls (tx ^. body) + ls' = applyTxBody ls pp (tx ^. body) cs = zip [0..] (tx ^. body . certs) -- index certificates -- |In the case where a certificate is valid for a given ledger state, @@ -649,10 +644,10 @@ certAsStateTransition slot txIx ls (clx, cert) = -- | Apply transition independent of validity, collect validation errors on the -- way. asStateTransition' - :: Slot -> LedgerValidation -> Tx -> Dms -> LedgerValidation -asStateTransition' slot (LedgerValidation valErrors ls) tx d = - let ls' = applyTxBody slot ls (tx ^. body) in - case validTx tx d slot ls of + :: Slot -> PParams -> LedgerValidation -> Tx -> Dms -> LedgerValidation +asStateTransition' slot pp (LedgerValidation valErrors ls) tx d = + let ls' = applyTxBody ls pp (tx ^. body) in + case validTx tx d slot pp ls of Invalid errors -> LedgerValidation (valErrors ++ errors) ls' Valid -> LedgerValidation valErrors ls' @@ -660,7 +655,7 @@ asStateTransition' slot (LedgerValidation valErrors ls) tx d = -- |Retire the appropriate stake pools when the epoch changes. retirePools :: LedgerState -> Epoch -> LedgerState -retirePools ls@(LedgerState _ ds _ _ _ _) epoch = +retirePools ls@(LedgerState _ ds _) epoch = ls & delegationState .~ (ds & pstate . stPools .~ (StakePools $ Map.filterWithKey @@ -671,26 +666,25 @@ retirePools ls@(LedgerState _ ds _ _ _ _) epoch = (StakePools stakePools) = ds ^. pstate . stPools -- |Calculate the change to the deposit pool for a given transaction. -depositPoolChange :: LedgerState -> TxBody -> Coin -depositPoolChange ls tx = (currentPool + txDeposits) - txRefunds +depositPoolChange :: LedgerState -> PParams -> TxBody -> Coin +depositPoolChange ls pp tx = (currentPool + txDeposits) - txRefunds -- Note that while (currentPool + txDeposits) >= txRefunds, -- it could be that txDeposits < txRefunds. We keep the parenthesis above -- to emphasize this point. where currentPool = ls ^. utxoState . deposited txDeposits = - deposits (ls ^. pcs) (ls ^. delegationState . pstate . stPools) (tx ^. certs) - txRefunds = keyRefunds (ls ^. pcs) (ls ^. delegationState . dstate . stKeys) tx + deposits pp (ls ^. delegationState . pstate . stPools) (tx ^. certs) + txRefunds = keyRefunds pp (ls ^. delegationState . dstate . stKeys) tx -- |Apply a transaction body as a state transition function on the ledger state. -applyTxBody :: Slot -> LedgerState -> TxBody -> LedgerState -applyTxBody slot ls tx = +applyTxBody :: LedgerState -> PParams -> TxBody -> LedgerState +applyTxBody ls pp tx = ls & utxoState %~ flip applyUTxOUpdate tx - & utxoState . deposited .~ depositPoolChange ls tx + & utxoState . deposited .~ depositPoolChange ls pp tx & utxoState . fees .~ (tx ^. txfee) + (ls ^. utxoState . fees) & delegationState . dstate . rewards .~ newAccounts - & txSlotIx %~ (if slot == ls ^. currentSlot then (+1) else const (0::Natural)) - & currentSlot .~ slot + & txSlotIx %~ (+) 1 where newAccounts = reapRewards (ls ^. delegationState . dstate. rewards) (tx ^. wdrls) @@ -760,7 +754,7 @@ applyDCertPState _ _ ps = ps -- |Compute how much stake each active stake pool controls. delegatedStake :: LedgerState -> Map.Map HashKey Coin -delegatedStake ls@(LedgerState _ ds _ _ _ _) = Map.fromListWith (+) delegatedOutputs +delegatedStake ls@(LedgerState _ ds _) = Map.fromListWith (+) delegatedOutputs where getOutputs (UTxO utxo') = Map.elems utxo' addStake delegs (TxOut (AddrTxin _ hsk) c) = do @@ -942,3 +936,16 @@ overlaySchedule -> PParams -> Map.Map Slot (Maybe VKeyGenesis) overlaySchedule = undefined + +-- | Set issue numbers +setIssueNumbers :: LedgerState -> Map.Map HashKey Natural -> LedgerState +setIssueNumbers (LedgerState u + (DPState _dstate + (PState stpools poolParams _retiring _ )) i) cs = + LedgerState u (DPState _dstate (PState stpools poolParams _retiring cs)) i + +-- | Update new epoch state +updateNES :: NewEpochState -> BlocksMade -> LedgerState ->NewEpochState +updateNES (NewEpochState eL eta0 bprev _ + (EpochState acnt ss _ pp) ru pd osched) bcur ls = + NewEpochState eL eta0 bprev bcur (EpochState acnt ss ls pp) ru pd osched diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs new file mode 100644 index 00000000000..ea4969083f0 --- /dev/null +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} + +module STS.Avup + ( AVUP + ) +where + +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set + +import BlockChain +import Keys +import Slot +import Updates + +import Control.State.Transition + +data AVUP + +instance STS AVUP where + type State AVUP = (AVUpdate, Map.Map Slot Applications, Applications) + type Signal AVUP = AVUpdate + type Environment AVUP = (Slot, Dms) + data PredicateFailure AVUP = NonGenesisUpdateAVUP + + deriving (Show, Eq) + initialRules = [] + + transitionRules = [avupTransition] + +avupTransition :: TransitionRule AVUP +avupTransition = do + TRC ((_slot, Dms _dms), src@(AVUpdate aupS, favs, avs), AVUpdate _aup) <- + judgmentContext + + if Map.null aupS + then pure src + else do + Map.keysSet _aup `Set.isSubsetOf` Map.keysSet _dms ?! NonGenesisUpdateAVUP + + let aup' = Map.union _aup aupS + let (cur, favs') = Map.partitionWithKey (\s _ -> s >= _slot) favs + let avs' = newAVs avs cur + let fav = votedValue aup' + case fav of + Nothing -> pure (AVUpdate aup', favs', avs') + Just fav' -> + pure + ( AVUpdate Map.empty + , Map.insert (_slot +* slotsPrior) fav' favs' + , avs' + ) 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 45f0045fbe0..8cb1b3ef5cd 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs @@ -5,16 +5,18 @@ module STS.Bbody ( BBODY - ) where + ) +where -import qualified Data.Map.Strict as Map -import Data.Maybe (fromMaybe) +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set import BlockChain import EpochBoundary import Keys import LedgerState import PParams +import Slot import Control.State.Transition @@ -25,9 +27,8 @@ data BBODY instance STS BBODY where type State BBODY = (LedgerState, BlocksMade) type Signal BBODY = Block - type Environment BBODY = PParams - data PredicateFailure BBODY = BodySizeTooLargeBBODY - | InvalidTxsSignatureBBODY + type Environment BBODY = (Set.Set Slot, PParams) + data PredicateFailure BBODY = WrongBlockBodySizeBBODY | LedgersFailure (PredicateFailure LEDGERS) deriving (Show, Eq) initialRules = [pure (emptyLedgerState, BlocksMade Map.empty)] @@ -35,16 +36,15 @@ instance STS BBODY where bbodyTransition :: TransitionRule BBODY bbodyTransition = do - TRC (pp, (ls, BlocksMade b), (Block (BHeader bhb _) txs)) <- - judgmentContext - let vk = bheaderVk bhb - let sigma = bheaderBlockSignature bhb - not (verify vk txs sigma) ?! InvalidTxsSignatureBBODY - bBodySize txs < (fromIntegral $ _maxBBSize pp) ?! BodySizeTooLargeBBODY - let hk = hashKey vk - let n = fromMaybe 0 (Map.lookup hk b) + TRC ((oslots, pp), (ls, b), (Block (BHeader bhb _) txs)) <- judgmentContext + let hk = hashKey $ bvkcold bhb + bBodySize txs == (fromIntegral $ hBbsize bhb) ?! WrongBlockBodySizeBBODY + ls' <- trans @LEDGERS $ TRC ((bheaderSlot bhb, pp), ls, txs) - pure (ls', BlocksMade $ Map.insert hk (n + 1) b) + + let b' = incrBlocks (Set.member (bheaderSlot bhb) oslots) hk b + + pure (ls', b') instance Embed LEDGERS BBODY where wrapFailed = LedgersFailure 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 c92bbb8a544..1dc2c6ae955 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Bhead.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Bhead.hs @@ -1,61 +1,60 @@ -{-# LANGUAGE EmptyDataDecls #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} module STS.Bhead ( BHEAD - ) where + ) +where -import qualified Data.Map.Strict as Map - -import Crypto.Hash (hash) -import qualified Data.ByteString.Char8 as BS +import qualified Data.Set as Set +import BaseTypes import BlockChain import Keys -import OCert +import LedgerState import PParams import Slot -import Delegation.Certificates (StakePools (..)) +import STS.NewEpoch +import STS.Rupd import Control.State.Transition data BHEAD instance STS BHEAD where - type State BHEAD = (HashHeader, Slot) + type State BHEAD = NewEpochState type Signal BHEAD = BHeader - type Environment BHEAD = (Slot, PParams, StakePools) - data PredicateFailure BHEAD = WrongPreviousHashBHEAD - | SlotTooEarlyBHEAD - | SlotTooLateBHEAD - | InvalidHeaderKESBHEAD - | HeaderSizeTooLargeBHEAD - | KeyNotRegisteredBHEAD - | KESPeriodInvalidBHEAD + type Environment BHEAD = (Seed, Set.Set VKeyGenesis) + data PredicateFailure BHEAD = HeaderSizeTooLargeBHEAD + | BlockSizeTooLargeBHEAD + | NewEpochFailure (PredicateFailure NEWEPOCH) + | RupdFailure (PredicateFailure RUPD) deriving (Show, Eq) - initialRules = [pure (HashHeader $ hash (BS.pack "emptyBHeader"), Slot 0)] + initialRules = [] transitionRules = [bheadTransition] bheadTransition :: TransitionRule BHEAD bheadTransition = do - TRC ((sNow, pp, StakePools stPools), (h, sL), bh@(BHeader bhb sigma)) <- + TRC ((etaC, gkeys), nes@(NewEpochState _ _ bprev _ es ru _ _), bh@(BHeader bhb _)) <- judgmentContext - let slot = bheaderSlot bhb - sL >= slot ?! SlotTooEarlyBHEAD - slot > sNow ?! SlotTooLateBHEAD - h /= bheaderPrev bhb ?! WrongPreviousHashBHEAD + let slot = bheaderSlot bhb + let EpochState _ _ _ pp = es + fromIntegral (bHeaderSize bh) > _maxBHSize pp ?! HeaderSizeTooLargeBHEAD - let vkHot = ocertVkHot $ bheaderOCert bhb - let hkEntry = Map.lookup (hashKey vkHot) stPools - case hkEntry of - Nothing -> do - failBecause KeyNotRegisteredBHEAD - pure (h, sL) - Just s0 -> do - let KESPeriod kps0 = kesPeriod s0 - let KESPeriod kpslot = kesPeriod slot - kps0 > kpslot ?! KESPeriodInvalidBHEAD - let t = kpslot - kps0 - not (verifyKES vkHot bhb sigma t) ?! InvalidHeaderKESBHEAD - pure (bhHash bh, slot) + fromIntegral (hBbsize bhb) > _maxBBSize pp ?! BlockSizeTooLargeBHEAD + + nes' <- trans @NEWEPOCH + $ TRC ((NewEpochEnv etaC slot gkeys), nes, epochFromSlot slot) + + ru' <- trans @RUPD $ TRC ((bprev, es), ru, slot) + let nes'' = nes' { nesRu = ru' } + pure nes'' + +instance Embed NEWEPOCH BHEAD where + wrapFailed = NewEpochFailure + +instance Embed RUPD BHEAD where + wrapFailed = RupdFailure 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 92775e2ffa1..52ea28b8387 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs @@ -5,99 +5,66 @@ module STS.Chain ( CHAIN - ) where + ) +where -import qualified Data.Map.Strict as Map +import qualified Data.Map.Strict as Map import BaseTypes import BlockChain -import EpochBoundary import LedgerState -import PParams import Slot -import Delegation.Certificates - import Control.State.Transition import STS.Bbody -import STS.NewEpoch -import STS.Ocert -import STS.Rupd -import STS.Updn +import STS.Bhead +import STS.Prtcl data CHAIN instance STS CHAIN where - type State CHAIN = ( (Seed, Seed, Seed) - , BlocksMade - , Slot - , Epoch - , EpochState - , Maybe RewardUpdate - , PoolDistr) + type State CHAIN = ( NewEpochState + , Seed + , Seed + , HashHeader + , Slot) type Signal CHAIN = Block - type Environment CHAIN = (Slot, PParams) + type Environment CHAIN = Slot data PredicateFailure CHAIN = BbodyFailure (PredicateFailure BBODY) - | RupdFailure (PredicateFailure RUPD) - | OcertFailure (PredicateFailure OCERT) - | NewepochFailure (PredicateFailure NEWEPOCH) - | UpdnFailure (PredicateFailure UPDN) + | BheadFailure (PredicateFailure BHEAD) + | PrtclFailure (PredicateFailure PRTCL) deriving (Show, Eq) - initialRules = - [ pure $ - ( (mkNonce 0, mkNonce 1, mkNonce 2) - , BlocksMade Map.empty - , Slot 0 - , Epoch 0 - , emptyEpochState - , Nothing - , PoolDistr Map.empty) - ] + initialRules = [] transitionRules = [chainTransition] chainTransition :: TransitionRule CHAIN chainTransition = do - TRC ((_, _ppN), ((eta0, etaC, etaV), b, sL, _eL, _es, _ru, _pd), block@(Block bh _)) <- - judgmentContext - let bhb = bhbody bh - let s = bheaderSlot bhb - let _e = epochFromSlot s -- TODO where is Epoch `e` coming from? - (etaV', etaC') <- trans @UPDN $ TRC (eta0, (etaV, etaC), s) - -- (eL', eta0', b', es'@(EpochState acnt' ls' ss' pp'), ru', pd') <- - -- trans @NEWEPOCH $ TRC (undefined, undefined, e) -- TODO: - -- TODO add PRTCL rule - let ls' = undefined - let pp' = undefined - let es' = undefined - let ru' = undefined - let b' = undefined - let acnt' = undefined - let ss' = undefined - let eta0' = undefined - let eL' = undefined - let pd' = undefined - ru'' <- trans @RUPD $ TRC ((b, es'), ru', s) - let _delegationState' = _delegationState ls' - _ <- trans @OCERT $ TRC ((), Map.empty, bh) -- TODO: OVERLAY -> PRTCL - let ls'' = ls' -- {_delegationState = delegationState' {_pstate = ps''}} - let sL' = sL - -- TODO after removal of Vrf, add PRTCL to get sL' - (ls''', b'') <- trans @BBODY $ TRC (pp', (ls'', b'), block) - let es'' = EpochState acnt' ss' ls''' pp' - pure $ ((eta0', etaC', etaV'), b'', sL', eL', es'', ru'', pd') + TRC (sNow, (nes, etaV, etaC, h, sL), block@(Block bh _)) <- judgmentContext -instance Embed BBODY CHAIN where - wrapFailed = BbodyFailure + let gkeys = getGKeys nes + nes' <- trans @BHEAD $ TRC ((etaC, gkeys), nes, bh) + + let NewEpochState _ eta0 _ bcur es _ _pd osched = nes' + let EpochState _ _ ls pp = es + let LedgerState _ (DPState (DState _ _ _ _ _dms) (PState _ _ _ cs)) _ = ls + + (cs', h', sL', etaV', etaC') <- trans @PRTCL + $ TRC (((pp, osched, eta0, _pd, _dms), sNow), (cs, h, sL, etaV, etaC), bh) -instance Embed OCERT CHAIN where - wrapFailed = OcertFailure + let ls' = setIssueNumbers ls cs' + (ls'', bcur') <- trans @BBODY + $ TRC ((Map.keysSet osched, pp), (ls', bcur), block) -instance Embed NEWEPOCH CHAIN where - wrapFailed = NewepochFailure + let nes'' = updateNES nes' bcur' ls'' + + pure (nes'', etaV', etaC', h', sL') + +instance Embed BBODY CHAIN where + wrapFailed = BbodyFailure -instance Embed UPDN CHAIN where - wrapFailed = UpdnFailure +instance Embed BHEAD CHAIN where + wrapFailed = BheadFailure -instance Embed RUPD CHAIN where - wrapFailed = RupdFailure +instance Embed PRTCL CHAIN where + wrapFailed = PrtclFailure 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 a66312c8ffa..889378b0cc1 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Deleg.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Deleg.hs @@ -3,7 +3,8 @@ module STS.Deleg ( DELEG - ) where + ) +where import LedgerState import Delegation.Certificates 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 d179a1fefe4..ffe7260215a 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Delegs.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Delegs.hs @@ -5,9 +5,10 @@ module STS.Delegs ( DELEGS - ) where + ) +where -import Control.Monad (foldM) +import Control.Monad ( foldM ) import LedgerState import Delegation.Certificates @@ -33,10 +34,11 @@ instance STS DELEGS where delegsTransition :: TransitionRule DELEGS delegsTransition = do - TRC((slot, ix, pp), d, certificates) <- judgmentContext - foldM (\d' (clx, c) -> - trans @DELPL $ - TRC((slot, Ptr slot ix clx, pp), d', c)) d $ zip [0..] certificates + TRC ((slot, ix, pp), d, certificates) <- judgmentContext + foldM + (\d' (clx, c) -> trans @DELPL $ TRC ((slot, Ptr slot ix clx, pp), d', c)) + d + $ zip [0 ..] certificates instance Embed DELPL DELEGS where wrapFailed = DelplFailure 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 c9cccc2ded2..7b11cd17b72 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Delpl.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Delpl.hs @@ -5,7 +5,8 @@ module STS.Delpl ( DELPL - ) where + ) +where import LedgerState import Delegation.Certificates @@ -33,21 +34,21 @@ instance STS DELPL where delplTransition :: TransitionRule DELPL delplTransition = do - TRC((slotIx, ptr, pp), d, c) <- judgmentContext + TRC ((slotIx, ptr, pp), d, c) <- judgmentContext case c of - RegPool _ -> do - ps <- trans @POOL $ TRC ((slotIx, ptr, pp), _pstate d, c) + RegPool _ -> do + ps <- trans @POOL $ TRC ((slotIx, ptr, pp), _pstate d, c) pure $ d { _pstate = ps } RetirePool _ _ -> do - ps <- trans @POOL $ TRC ((slotIx, ptr, pp), _pstate d, c) + ps <- trans @POOL $ TRC ((slotIx, ptr, pp), _pstate d, c) pure $ d { _pstate = ps } - RegKey _ -> do + RegKey _ -> do ds <- trans @DELEG $ TRC ((slotIx, ptr), _dstate d, c) pure $ d { _dstate = ds } - DeRegKey _ -> do + DeRegKey _ -> do ds <- trans @DELEG $ TRC ((slotIx, ptr), _dstate d, c) pure $ d { _dstate = ds } - Delegate _ -> do + Delegate _ -> do ds <- trans @DELEG $ TRC ((slotIx, ptr), _dstate d, c) pure $ d { _dstate = ds } 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 a73a103aeb9..aee16de7389 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Epoch.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Epoch.hs @@ -5,7 +5,8 @@ module STS.Epoch ( EPOCH - ) where + ) +where import LedgerState import PParams @@ -33,23 +34,23 @@ instance STS EPOCH where transitionRules = [ epochTransition ] initialEpoch :: InitialRule EPOCH -initialEpoch = pure $ EpochState - emptyAccount - emptySnapShots - emptyLedgerState - emptyPParams +initialEpoch = + pure $ EpochState emptyAccount emptySnapShots emptyLedgerState emptyPParams epochTransition :: TransitionRule EPOCH epochTransition = do - TRC(blocks, EpochState as ss ls pp, e) <- judgmentContext - let us = _utxoState ls - let DPState ds ps = _delegationState ls - (ss', us') <- trans @SNAP $ TRC((pp, ds, ps, blocks), (ss, us), e) - (as', ds', ps') <- trans @POOLREAP $ TRC(pp, (as, ds, ps), e) - let ppNew = undefined -- TODO: result from votedValuePParams - (us'', as'', pp') - <- trans @NEWPP $ TRC((ppNew, ds', ps'), (us', as', pp), e) - pure $ EpochState as'' ss' (ls { _utxoState = us'', _delegationState = DPState ds' ps'}) pp' + TRC (blocks, EpochState as ss ls pp, e) <- judgmentContext + let us = _utxoState ls + let DPState ds ps = _delegationState ls + (ss', us') <- trans @SNAP $ TRC ((pp, ds, ps, blocks), (ss, us), e) + (as', ds', ps') <- trans @POOLREAP $ TRC (pp, (as, ds, ps), e) + let ppNew = undefined -- TODO: result from votedValuePParams + (us'', as'', pp') <- trans @NEWPP $ TRC ((ppNew, ds', ps'), (us', as', pp), e) + pure $ EpochState + as'' + ss' + (ls { _utxoState = us'', _delegationState = DPState ds' ps' }) + pp' instance Embed SNAP EPOCH where wrapFailed = SnapFailure 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 6cb8b7315b9..952836757bd 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Ledger.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ledger.hs @@ -5,11 +5,12 @@ module STS.Ledger ( LEDGER - ) where + ) +where -import qualified Data.Map.Strict as Map +import qualified Data.Map.Strict as Map -import Lens.Micro ((^.)) +import Lens.Micro ( (^.) ) import Keys import LedgerState @@ -28,7 +29,7 @@ data LEDGER instance STS LEDGER where type State LEDGER = (UTxOState, DPState) type Signal LEDGER = Tx - type Environment LEDGER = (PParams, Slot, Ix) + type Environment LEDGER = (Slot, Ix, PParams) data PredicateFailure LEDGER = UtxowFailure (PredicateFailure UTXOW) | DelegsFailure (PredicateFailure DELEGS) deriving (Show, Eq) @@ -38,20 +39,20 @@ instance STS LEDGER where initialLedgerStateLEDGER :: InitialRule LEDGER initialLedgerStateLEDGER = do - IRC (pp, slot, ix) <- judgmentContext - utxo' <- trans @UTXOW + IRC (slot, ix, pp) <- judgmentContext + utxo' <- trans @UTXOW $ IRC (slot, pp, StakeKeys Map.empty, StakePools Map.empty, Dms Map.empty) deleg <- trans @DELEGS $ IRC (slot, ix, pp) pure (utxo', deleg) ledgerTransition :: TransitionRule LEDGER ledgerTransition = do - TRC ((pp, slot, ix), (u, d), txwits) <- judgmentContext - utxo' <- trans @UTXOW - $ TRC (( slot - , pp, d ^. dstate . stKeys - , d ^. pstate . stPools - , d ^. dstate . dms), u, txwits) + TRC ((slot, ix, pp), (u, d), txwits) <- judgmentContext + utxo' <- trans @UTXOW $ TRC + ( (slot, pp, d ^. dstate . stKeys, d ^. pstate . stPools, d ^. dstate . dms) + , u + , txwits + ) deleg' <- trans @DELEGS $ TRC ((slot, ix, pp), d, txwits ^. body . certs) pure (utxo', deleg') 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 388ab882c30..4648957feb4 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Ledgers.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ledgers.hs @@ -5,9 +5,10 @@ module STS.Ledgers ( LEDGERS - ) where + ) +where -import Control.Monad (foldM) +import Control.Monad ( foldM ) import LedgerState import PParams @@ -36,12 +37,12 @@ ledgersTransition = do let (u, dw) = (_utxoState ls, _delegationState ls) (u'', dw'') <- foldM - (\(u', dw') (ix, tx) -> - trans @LEDGER $ TRC ((pp, slot, ix), (u', dw'), tx)) - (u, dw) $ - zip [0 ..] txwits - pure $ - LedgerState u'' dw'' (upiState ls) (_pcs ls) (_txSlotIx ls) (_currentSlot ls) + (\(u', dw') (ix, tx) -> + trans @LEDGER $ TRC ((slot, ix, pp), (u', dw'), tx) + ) + (u, dw) + $ zip [0 ..] txwits + pure $ LedgerState u'' dw'' (_txSlotIx ls) instance Embed LEDGER LEDGERS where wrapFailed = LedgerFailure 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 d80e7a4b5c1..c60214f5d24 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/NewEpoch.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/NewEpoch.hs @@ -5,10 +5,12 @@ module STS.NewEpoch ( NEWEPOCH - ) where + ) +where -import qualified Data.Map.Strict as Map -import qualified Data.Maybe as Maybe (fromMaybe) +import qualified Data.Map.Strict as Map +import qualified Data.Maybe as Maybe + ( fromMaybe ) import BaseTypes import Coin @@ -53,27 +55,32 @@ ocertTransition = do if eL' /= e' + 1 then pure src else do - let es_ = - case ru of - Nothing -> es - Just ru' -> applyRUpd ru' es + let es_ = case ru of + Nothing -> es + Just ru' -> applyRUpd ru' es es' <- trans @EPOCH $ TRC (bprev, es_, e) let EpochState acnt ss ls pp = es' - let (Stake stake, delegs) = _pstakeSet ss - let Coin total = Map.foldl (+) (Coin 0) stake - let etaE = _extraEntropy pp - let osched' = overlaySchedule gkeys eta1 pp + let (Stake stake, delegs) = _pstakeSet ss + let Coin total = Map.foldl (+) (Coin 0) stake + let etaE = _extraEntropy pp + let osched' = overlaySchedule gkeys eta1 pp let es'' = EpochState acnt ss ls (pp { _extraEntropy = neutralSeed }) - let pd' = - foldr - (\(hk, (Coin c)) m -> - Map.insertWith (+) hk ((fromIntegral c) / fromIntegral total) m) - Map.empty - [ (poolKey, Maybe.fromMaybe (Coin 0) (Map.lookup stakeKey stake)) - | (stakeKey, poolKey) <- Map.toList delegs - ] - pure $ - NewEpochState e (seedOp eta1 etaE) bcur (BlocksMade Map.empty) es'' Nothing (PoolDistr pd') osched' + let pd' = foldr + (\(hk, (Coin c)) m -> + Map.insertWith (+) hk ((fromIntegral c) / fromIntegral total) m + ) + Map.empty + [ (poolKey, Maybe.fromMaybe (Coin 0) (Map.lookup stakeKey stake)) + | (stakeKey, poolKey) <- Map.toList delegs + ] + pure $ NewEpochState e + (seedOp eta1 etaE) + bcur + (BlocksMade Map.empty) + es'' + Nothing + (PoolDistr pd') + osched' instance Embed EPOCH NEWEPOCH where wrapFailed = EpochFailure 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 c395197ab7e..5d971d54e4d 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Newpp.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Newpp.hs @@ -3,17 +3,18 @@ module STS.Newpp ( NEWPP - ) where + ) +where -import qualified Data.Map.Strict as Map +import qualified Data.Map.Strict as Map -import Lens.Micro ((^.)) +import Lens.Micro ( (^.) ) -import BaseTypes import EpochBoundary import LedgerState hiding (reserves) import PParams import Slot +import Updates import UTxO import Coin @@ -31,11 +32,11 @@ instance STS NEWPP where transitionRules = [newPpTransition] initialNewPp :: InitialRule NEWPP -initialNewPp = - pure - (UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) (EEnt Map.empty) - , emptyAccount - , emptyPParams) +initialNewPp = pure + ( UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) (emptyUpdateState) + , emptyAccount + , emptyPParams + ) newPpTransition :: TransitionRule NEWPP newPpTransition = do @@ -43,25 +44,33 @@ newPpTransition = do case ppNew of Just ppNew' -> do - let Coin oblgCurr = obligation pp (ds ^. stKeys) (ps ^. stPools) (firstSlot e) + let Coin oblgCurr = + obligation pp (ds ^. stKeys) (ps ^. stPools) (firstSlot e) let Coin oblgNew = obligation ppNew' (ds ^. stKeys) (ps ^. stPools) (slotFromEpoch e) - let diff = oblgCurr - oblgNew + let diff = oblgCurr - oblgNew let Coin reserves = _reserves acnt - if reserves + diff >= 0 - && (_maxTxSize ppNew' + _maxBHSize ppNew') < _maxBBSize ppNew' - then - let utxoSt' = utxoSt { _deposited = Coin oblgNew } in -- TODO: update mechanism - let acnt' = acnt { _reserves = Coin $ reserves + diff } in - pure $ (utxoSt', acnt', ppNew') - else - pure $ - ((if reserves + diff < 0 - || (_maxTxSize ppNew' + _maxBHSize ppNew') >= _maxBBSize ppNew' - then - utxoSt -- TODO update mechanism - else - utxoSt) - , acnt - , pp) + if reserves + + diff + >= 0 + && (_maxTxSize ppNew' + _maxBHSize ppNew') + < _maxBBSize ppNew' + then + let utxoSt' = utxoSt { _deposited = Coin oblgNew } + in -- TODO: update mechanism + let acnt' = acnt { _reserves = Coin $ reserves + diff } + in pure $ (utxoSt', acnt', ppNew') + else + pure + $ ( (if reserves + + diff + < 0 + || (_maxTxSize ppNew' + _maxBHSize ppNew') + >= _maxBBSize ppNew' + then utxoSt -- TODO update mechanism + else utxoSt + ) + , acnt + , pp + ) Nothing -> pure (utxoSt, acnt, pp) 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 ff3008f0aee..d1c43627476 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Ocert.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ocert.hs @@ -3,10 +3,11 @@ module STS.Ocert ( OCERT - ) where + ) +where -import qualified Data.Map.Strict as Map -import Numeric.Natural (Natural) +import qualified Data.Map.Strict as Map +import Numeric.Natural ( Natural ) import BlockChain import Keys @@ -35,7 +36,7 @@ ocertTransition = do TRC (_, cs, BHeader bhb sigma) <- judgmentContext let OCert vk_hot vk_cold n c0@(KESPeriod c0') tau = bheaderOCert bhb let hk = hashKey vk_cold - let s = bheaderSlot bhb + let s = bheaderSlot bhb not (verify vk_cold (vk_hot, n, c0) tau) ?! InvalidSignatureOCERT let kp@(KESPeriod kp') = kesPeriod s c0 > kp ?! KESBeforeStartOCERT diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs new file mode 100644 index 00000000000..f2f646f434f --- /dev/null +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} + +module STS.Overlay + ( OVERLAY + ) +where + +import qualified Data.Map.Strict as Map +import Numeric.Natural ( Natural ) + +import BaseTypes +import BlockChain +import Delegation.Certificates +import Keys +import PParams +import Slot + +import STS.Ocert + +import Control.State.Transition + +data OVERLAY + +instance STS OVERLAY where + type State OVERLAY = Map.Map HashKey Natural + type Signal OVERLAY = BHeader + type Environment OVERLAY = + ( PParams + , Map.Map Slot (Maybe VKeyGenesis) + , Seed + , PoolDistr + , Dms) + data PredicateFailure OVERLAY = NotPraosLeaderOVERLAY + | NotActiveSlotOVERLAY + | WrongGenesisColdKeyOVERLAY + | NoGenesisStakingOVERLAY + | OcertFailure (PredicateFailure OCERT) + deriving (Show, Eq) + initialRules = [] + + transitionRules = [overlayTransition] + +overlayTransition :: TransitionRule OVERLAY +overlayTransition = do + TRC ((pp, osched, eta0, pd, Dms dms), cs, bh@(BHeader bhb _)) <- + judgmentContext + let gkey'' = Map.lookup (bheaderSlot bhb) osched + let vk = bvkcold bhb + case gkey'' of + Nothing -> do + vrfChecks eta0 pd (_activeSlotCoeff pp) bhb ?! NotPraosLeaderOVERLAY + cs' <- trans @OCERT $ TRC ((), cs, bh) + pure cs' + Just gkey' -> do + case gkey' of + Nothing -> failBecause NotActiveSlotOVERLAY + Just gkey -> do + let dmsKey' = Map.lookup gkey dms + case dmsKey' of + Nothing -> failBecause NoGenesisStakingOVERLAY + Just dmsKey -> vk == dmsKey ?! WrongGenesisColdKeyOVERLAY + cs' <- trans @OCERT $ TRC ((), cs, bh) + pure cs' + +instance Embed OCERT OVERLAY where + wrapFailed = OcertFailure 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 c4876c976bc..017120f5926 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Pool.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Pool.hs @@ -3,9 +3,10 @@ module STS.Pool ( POOL - ) where + ) +where -import Lens.Micro ((^.)) +import Lens.Micro ( (^.) ) import Delegation.Certificates import LedgerState @@ -32,10 +33,10 @@ poolDelegationTransition :: TransitionRule POOL poolDelegationTransition = do TRC ((slot, p@(Ptr _ _ _), pp), ps, c) <- judgmentContext case c of - RegPool _ -> pure $ applyDCertPState p c ps + RegPool _ -> pure $ applyDCertPState p c ps RetirePool _ (Epoch e) -> do validStakePoolRetire c ps == Valid ?! StakePoolNotRegisteredOnKeyPOOL - let Epoch cepoch = epochFromSlot slot + let Epoch cepoch = epochFromSlot slot let Epoch maxEpoch = pp ^. eMax cepoch < e && e < cepoch + maxEpoch ?! StakePoolRetirementWrongEpochPOOL pure $ applyDCertPState p c ps 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 44f0061ed39..353a1d5ff84 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/PoolReap.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/PoolReap.hs @@ -3,12 +3,17 @@ module STS.PoolReap ( POOLREAP - ) where + ) +where -import qualified Data.Map.Strict as Map -import qualified Data.Set as Set +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set -import Lens.Micro ((^.), (&), (.~), (%~)) +import Lens.Micro ( (^.) + , (&) + , (.~) + , (%~) + ) import LedgerState import PParams @@ -32,31 +37,37 @@ instance STS POOLREAP where poolReapTransition :: TransitionRule POOLREAP poolReapTransition = do TRC (pp, (a, ds, ps), e) <- judgmentContext - let retired = Map.keysSet $ Map.filter (== e) $ ps ^. retiring - let pr = poolRefunds pp (ps ^. retiring) (firstSlot e) + let retired = Map.keysSet $ Map.filter (== e) $ ps ^. retiring + let pr = poolRefunds pp (ps ^. retiring) (firstSlot e) let relevant = Map.restrictKeys (ps ^. pParams) retired - let rewardAcnts = - Map.mapMaybeWithKey - (\k v -> - case Map.lookup k relevant of - Nothing -> Nothing - Just _ -> Just (v ^. poolRAcnt)) - (ps ^. pParams) + let rewardAcnts = Map.mapMaybeWithKey + (\k v -> case Map.lookup k relevant of + Nothing -> Nothing + Just _ -> Just (v ^. poolRAcnt) + ) + (ps ^. pParams) let rewardAcnts' = Map.restrictKeys rewardAcnts (Map.keysSet pr) - let refunds' = - Map.foldlWithKey - (\m k addr -> Map.insert addr (pr Map.! k) m) - Map.empty - rewardAcnts' -- not yet restricted to a in dom(rewards) + let refunds' = Map.foldlWithKey + (\m k addr -> Map.insert addr (pr Map.! k) m) + Map.empty + rewardAcnts' -- not yet restricted to a in dom(rewards) let domRewards = Map.keysSet (ds ^. rewards) let (refunds, unclaimed') = Map.partitionWithKey (\k _ -> k `Set.member` domRewards) refunds' - let unclaimed = Map.foldl (+) (Coin 0) unclaimed' + let unclaimed = Map.foldl (+) (Coin 0) unclaimed' let StakePools stakePools = ps ^. stPools pure ( a & treasury %~ (+) unclaimed - , ds & rewards %~ flip Map.union refunds - & delegations %~ flip Map.withoutKeys retired - , ps & stPools .~ (StakePools $ Map.withoutKeys stakePools retired) - & pParams %~ flip Map.withoutKeys retired - & retiring %~ flip Map.withoutKeys retired) + , ds + & rewards + %~ flip Map.union refunds + & delegations + %~ flip Map.withoutKeys retired + , ps + & stPools + .~ (StakePools $ Map.withoutKeys stakePools retired) + & pParams + %~ flip Map.withoutKeys retired + & retiring + %~ flip Map.withoutKeys retired + ) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs new file mode 100644 index 00000000000..596e67371da --- /dev/null +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} + +module STS.Ppup + ( PPUP + ) +where + +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set + +import BlockChain +import Keys +import Slot +import Updates + +import Control.State.Transition + +data PPUP + +instance STS PPUP where + type State PPUP = PPUpdate + type Signal PPUP = PPUpdate + type Environment PPUP = (Slot, Dms) + data PredicateFailure PPUP = NonGenesisUpdatePPUP + | PPUpdateTooLatePPUP + deriving (Show, Eq) + initialRules = [] + + transitionRules = [ppupTransition] + +ppupTransition :: TransitionRule PPUP +ppupTransition = do + TRC ((s, Dms _dms), pupS@(PPUpdate pupS'), pup@(PPUpdate pup')) <- + judgmentContext + if Map.null pupS' + then pure pupS + else do + (not $ Map.keysSet pup' `Set.isSubsetOf` Map.keysSet _dms) + ?! NonGenesisUpdatePPUP + let Epoch slotEpoch = epochFromSlot (Slot 1) + s + < (firstSlot (Epoch $ slotEpoch + 1) *- slotsPrior) + ?! PPUpdateTooLatePPUP + pure $ updatePPup pupS 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 new file mode 100644 index 00000000000..fb6ed8caddf --- /dev/null +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Prtcl.hs @@ -0,0 +1,66 @@ +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} + +module STS.Prtcl + ( PRTCL + ) +where + +import qualified Data.Map.Strict as Map +import Numeric.Natural ( Natural ) + +import BaseTypes +import BlockChain +import Delegation.Certificates +import Keys +import PParams +import Slot + +import STS.Overlay +import STS.Updn + +import Control.State.Transition + +data PRTCL + +instance STS PRTCL where + type State PRTCL = (Map.Map HashKey Natural, HashHeader, Slot, Seed, Seed) + type Signal PRTCL = BHeader + type Environment PRTCL = + ( -- OverlayEnvironment + ( PParams + , Map.Map Slot (Maybe VKeyGenesis) + , Seed + , PoolDistr + , Dms) + , Slot) + data PredicateFailure PRTCL = WrongSlotIntervalPRTCL + | WrongBlockSequencePRTCL + | OverlayFailure (PredicateFailure OVERLAY) + | UpdnFailure (PredicateFailure UPDN) + deriving (Show, Eq) + initialRules = [] + + transitionRules = [prtclTransition] + +prtclTransition :: TransitionRule PRTCL +prtclTransition = do + TRC ((oe, sNow), (cs, h, sL, etaV, etaC), bh) <- judgmentContext + let bhb = bhbody bh + let slot = bheaderSlot bhb + let eta = bheaderEta bhb + sL < slot && slot <= sNow ?! WrongSlotIntervalPRTCL + h == bheaderPrev bhb ?! WrongBlockSequencePRTCL + + cs' <- trans @OVERLAY $ TRC (oe, cs, bh) + (etaV', etaC') <- trans @UPDN $ TRC (eta, (etaV, etaC), slot) + + pure (cs', bhHash bh, slot, etaV', etaC') + +instance Embed OVERLAY PRTCL where + wrapFailed = OverlayFailure + +instance Embed UPDN PRTCL where + wrapFailed = UpdnFailure 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 23ef578d5e7..9b4026dd8e9 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Rupd.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Rupd.hs @@ -3,7 +3,8 @@ module STS.Rupd ( RUPD - ) where + ) +where import BlockChain import EpochBoundary @@ -30,5 +31,5 @@ rupdTransition = do if s <= slot then pure ru else case ru of - Nothing -> pure $ Just (createRUpd b es) - Just _ -> pure $ ru + Nothing -> pure $ Just (createRUpd 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 bcc39102d62..0769d193a04 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Snap.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Snap.hs @@ -3,17 +3,22 @@ module STS.Snap ( SNAP - ) where + ) +where -import qualified Data.Map.Strict as Map +import qualified Data.Map.Strict as Map -import Lens.Micro ((^.), (&), (.~), (%~)) +import Lens.Micro ( (^.) + , (&) + , (.~) + , (%~) + ) -import BaseTypes import Coin import EpochBoundary import LedgerState import PParams hiding (d) +import Updates import Slot import UTxO @@ -28,20 +33,30 @@ instance STS SNAP where data PredicateFailure SNAP = FailureSNAP deriving (Show, Eq) initialRules = - [pure (emptySnapShots, UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) (EEnt Map.empty))] + [pure (emptySnapShots, UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) emptyUpdateState)] transitionRules = [snapTransition] snapTransition :: TransitionRule SNAP snapTransition = do TRC ((pparams, d, p, blocks), (s, u), eNew) <- judgmentContext let pooledStake = poolDistr (u ^. utxo) d p - let slot = firstSlot eNew - let oblg = obligation pparams (d ^. stKeys) (p ^. stPools) slot - let decayed = (u ^. deposited) - oblg + let _slot = firstSlot eNew + let oblg = obligation pparams (d ^. stKeys) (p ^. stPools) _slot + let decayed = (u ^. deposited) - oblg pure - ( s & pstakeMark .~ pooledStake & pstakeSet .~ (s ^. pstakeMark) & - pstakeGo .~ (s ^. pstakeSet) & - poolsSS .~ (p ^. pParams) & - blocksSS .~ blocks & - feeSS .~ (u ^. fees) + decayed - , u & deposited .~ oblg & fees %~ (+) decayed) + ( s + & pstakeMark + .~ pooledStake + & pstakeSet + .~ (s ^. pstakeMark) + & pstakeGo + .~ (s ^. pstakeSet) + & poolsSS + .~ (p ^. pParams) + & blocksSS + .~ blocks + & feeSS + .~ (u ^. fees) + + decayed + , u & deposited .~ oblg & fees %~ (+) decayed + ) diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs new file mode 100644 index 00000000000..3f3b3b1ba27 --- /dev/null +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} + +module STS.Up + ( UP + ) +where + +import qualified Data.Map.Strict as Map + +import Keys +import Slot +import Updates + +import Control.State.Transition + +import STS.Avup +import STS.Ppup + +data UP + +instance STS UP where + type State UP = (PPUpdate, AVUpdate, Map.Map Slot Applications, Applications) + type Signal UP = Update + type Environment UP = (Slot, Dms) + data PredicateFailure UP = NonGenesisUpdateUP + | AvupFailure (PredicateFailure AVUP) + | PpupFailure (PredicateFailure PPUP) + deriving (Show, Eq) + initialRules = [] + + transitionRules = [upTransition] + +upTransition :: TransitionRule UP +upTransition = do + TRC (env, (pupS, aupS, favs, avs), Update pup _aup) <- judgmentContext + + pup' <- trans @PPUP $ TRC (env, pupS, pup) + (aup', favs', avs') <- trans @AVUP $ TRC (env, (aupS, favs, avs), _aup) + + pure (pup', aup', favs', avs') + +instance Embed AVUP UP where + wrapFailed = AvupFailure + +instance Embed PPUP UP where + wrapFailed = PpupFailure 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 0ebc59f2f96..71f460bec75 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Updn.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Updn.hs @@ -3,7 +3,8 @@ module STS.Updn ( UPDN - ) where + ) +where import BaseTypes import BlockChain 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 94213ae2ddb..0c1e807e300 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs @@ -1,26 +1,34 @@ {-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} module STS.Utxo ( UTXO - ) where + ) +where -import qualified Data.Map.Strict as Map -import qualified Data.Set as Set +import qualified Data.Map.Strict as Map -import Lens.Micro ((%~), (&), (^.), (.~)) +import Lens.Micro ( (%~) + , (&) + , (^.) + , (.~) + ) -import BaseTypes import Coin import Delegation.Certificates import Keys import LedgerState hiding (dms) import PParams import Slot +import Updates import UTxO import Control.State.Transition +import STS.Up + data UTXO instance STS UTXO where @@ -35,6 +43,7 @@ instance STS UTXO where | UnexpectedFailureUTXO [ValidationError] | UnexpectedSuccessUTXO | BadExtraEntropyUTxO + | UpdateFailure (PredicateFailure UP) deriving (Eq, Show) transitionRules = [utxoInductive] initialRules = [initialLedgerState] @@ -42,31 +51,41 @@ instance STS UTXO where initialLedgerState :: InitialRule UTXO initialLedgerState = do IRC _ <- judgmentContext - pure $ UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) (EEnt Map.empty) + pure $ UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) emptyUpdateState utxoInductive :: TransitionRule UTXO utxoInductive = do - TRC ((slot, pp, stakeKeys, stakePools, Dms dms), u, tx) <- judgmentContext + TRC ((_slot, pp, stakeKeys, stakePools, _dms), u, tx) <- judgmentContext + let txbody = _body tx validInputs txbody u == Valid ?! BadInputsUTxO - current txbody slot == Valid ?! ExpiredUTxO (txbody ^. ttl) slot + _ttl txbody >= _slot ?! ExpiredUTxO (_ttl txbody) _slot validNoReplay txbody == Valid ?! InputSetEmptyUTxO + let validateFee = validFee pp txbody validateFee == Valid ?! unwrapFailureUTXO validateFee + let validateBalance = preserveBalance stakePools stakeKeys pp txbody u validateBalance == Valid ?! unwrapFailureUTXO validateBalance + let refunded = keyRefunds pp stakeKeys txbody - let decayed = decayedTx pp stakeKeys txbody + let decayed = decayedTx pp stakeKeys txbody let depositChange = deposits pp stakePools (txbody ^. certs) - (refunded + decayed) + let u' = applyUTxOUpdate u txbody -- change UTxO - let EEnt h' = txbody ^. txeent - Set.isSubsetOf (Map.keysSet h') (Map.keysSet dms) ?! BadExtraEntropyUTxO - let EEnt h = _eEntropy u - pure $ - u' & deposited %~ (+) depositChange - & fees %~ (+) ((txbody ^. txfee) + decayed) - & eEntropy .~ (EEnt $ Map.union h h') + + -- process Update Proposals + ups' <- trans @UP $ TRC ((_slot, _dms), u ^. ups, txup tx) + + pure + $ u' + & deposited + %~ (+) depositChange + & fees + %~ (+) ((txbody ^. txfee) + decayed) + & ups + .~ ups' unwrapFailureUTXO :: Validity -> PredicateFailure UTXO unwrapFailureUTXO (Invalid [e]) = unwrapFailureUTXO' e @@ -77,6 +96,9 @@ unwrapFailureUTXO' :: ValidationError -> PredicateFailure UTXO unwrapFailureUTXO' BadInputs = BadInputsUTxO unwrapFailureUTXO' (Expired s s') = ExpiredUTxO s s' unwrapFailureUTXO' InputSetEmpty = InputSetEmptyUTxO -unwrapFailureUTXO' (FeeTooSmall c c') = FeeTooSmallUTxO c c' +unwrapFailureUTXO' (FeeTooSmall c c') = FeeTooSmallUTxO c c' unwrapFailureUTXO' (ValueNotConserved c c') = ValueNotConservedUTxO c c' unwrapFailureUTXO' x = UnexpectedFailureUTXO [x] + +instance Embed UP UTXO where + wrapFailed = UpdateFailure 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 4c63fb9263f..0b9c9c6fdc6 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Utxow.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Utxow.hs @@ -5,7 +5,10 @@ module STS.Utxow ( UTXOW - ) where + ) +where + +import qualified Data.Set as Set import Delegation.Certificates import Keys @@ -26,7 +29,6 @@ instance STS UTXOW where type Environment UTXOW = (Slot, PParams, StakeKeys, StakePools, Dms) data PredicateFailure UTXOW = InvalidWitnessesUTXOW | MissingWitnessesUTXOW - | UnneededWitnessesUTXOW | UtxoFailure (PredicateFailure UTXO) deriving (Eq, Show) transitionRules = [utxoWitnessed] @@ -39,11 +41,12 @@ initialLedgerStateUTXOW = do utxoWitnessed :: TransitionRule UTXOW utxoWitnessed = do - TRC ((slot, pp, stakeKeys, stakePools, dms), u, tx) <- judgmentContext + TRC ((slot, pp, stakeKeys, stakePools, _dms), u, tx@(Tx _ wits)) + <- judgmentContext verifiedWits tx == Valid ?! InvalidWitnessesUTXOW - enoughWits tx dms u == Valid ?! MissingWitnessesUTXOW - noUnneededWits tx dms u == Valid ?! UnneededWitnessesUTXOW - trans @UTXO $ TRC ((slot, pp, stakeKeys, stakePools, dms), u, tx) + let witnessKeys = Set.map (\(Wit vk _) -> hashKey vk) wits + witsNeeded (_utxo u) tx _dms == witnessKeys ?! MissingWitnessesUTXOW + trans @UTXO $ TRC ((slot, pp, stakeKeys, stakePools, _dms), u, tx) instance Embed UTXO UTXOW where wrapFailed = UtxoFailure diff --git a/shelley/chain-and-ledger/executable-spec/src/Slot.hs b/shelley/chain-and-ledger/executable-spec/src/Slot.hs index 1b502d168bd..d586254a596 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Slot.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Slot.hs @@ -4,7 +4,7 @@ module Slot ( Slot(..) , Duration(..) - , (-*), (+*) + , (-*), (+*), (*-) , Epoch(..) -- conversion functions , slotFromEpoch @@ -36,6 +36,10 @@ newtype Duration = Duration Natural (+*) :: Slot -> Duration -> Slot (Slot s) +* (Duration d) = Slot (s + d) +-- | Subtract a duration from a slot +(*-) :: Slot -> Duration -> Slot +(Slot s) *- (Duration d) = Slot (if s > d then s - d else 0) + -- |An Epoch newtype Epoch = Epoch Natural deriving (Show, Eq, Ord) diff --git a/shelley/chain-and-ledger/executable-spec/src/UTxO.hs b/shelley/chain-and-ledger/executable-spec/src/UTxO.hs index c193d5f47ae..dde2acd3c94 100644 --- a/shelley/chain-and-ledger/executable-spec/src/UTxO.hs +++ b/shelley/chain-and-ledger/executable-spec/src/UTxO.hs @@ -29,6 +29,7 @@ module UTxO , txins , txinLookup , txouts + , txUpdate , balance , deposits , (<|) @@ -47,11 +48,11 @@ module UTxO , wdrls , txfee , ttl - , txeent -- Tx , body , witnessSet , verifyWit + , txup ) where import Crypto.Hash (Digest, SHA256, hash) @@ -66,11 +67,11 @@ import Numeric.Natural (Natural) import Lens.Micro ((^.)) import Lens.Micro.TH (makeLenses) -import BaseTypes import Coin (Coin (..)) import Keys import PParams (PParams(..)) import Slot (Slot(..)) +import Updates (Update) import Delegation.Certificates (StakePools(..), DCert (..), dvalue) import Delegation.PoolParams (poolPubKey, RewardAcnt(..)) @@ -114,7 +115,7 @@ data TxBody = TxBody { _inputs :: !(Set TxIn) , _wdrls :: Wdrl , _txfee :: Coin , _ttl :: Slot - , _txeent :: EEnt + , _txUpdate:: Update } deriving (Show, Eq, Ord) makeLenses ''TxBody @@ -199,3 +200,6 @@ deposits pc (StakePools stpools) cs = foldl f (Coin 0) cs' instance BA.ByteArrayAccess TxBody where length = BA.length . BS.pack . show withByteArray = BA.withByteArray . BS.pack . show + +txup :: Tx -> Update +txup (Tx txbody _ ) = _txUpdate txbody diff --git a/shelley/chain-and-ledger/executable-spec/src/Updates.hs b/shelley/chain-and-ledger/executable-spec/src/Updates.hs new file mode 100644 index 00000000000..fe7fed972c8 --- /dev/null +++ b/shelley/chain-and-ledger/executable-spec/src/Updates.hs @@ -0,0 +1,110 @@ +{-# LANGUAGE EmptyDataDecls #-} + +module Updates + ( PPUpdateEnv(..) + , PPUpdate(..) + , updatePPup + , ApName(..) + , ApVer(..) + , Metadata + , Applications(..) + , AVUpdate(..) + , Update(..) + , newAVs + , votedValue + , emptyUpdateState + , emptyUpdate + ) +where + +import qualified Data.Map.Strict as Map +import qualified Data.List as List + ( group ) + +import BaseTypes +import Coin +import Keys +import Slot + +import Numeric.Natural + +newtype ApVer = ApVer Natural + deriving (Show, Ord, Eq) + +newtype ApName = ApName String + deriving (Show, Ord, Eq) + +data Metadata = Metadata -- for now, there are no requirements on Metadata + deriving (Show, Ord, Eq) + +data Applications = Applications { + apps :: Map.Map ApName (ApVer, Metadata) + } deriving (Show, Ord, Eq) + +data AVUpdate = AVUpdate { + aup :: Map.Map VKeyGenesis Applications + } deriving (Show, Ord, Eq) + +-- | Update Proposal +data Update = Update PPUpdate AVUpdate + deriving (Show, Ord, Eq) + +data PPUpdateEnv = PPUpdateEnv { + slot :: Slot + , dms :: Dms + } deriving (Show, Ord, Eq) + +data Ppm = MinFeeA Integer + | MinFeeB Natural + | MaxBBSize Natural + | MaxTxSize Natural + | KeyDeposit Coin + | KeyMinRefund UnitInterval + | KeyDecayRate Rational + | PoolDeposit Coin + | PoolMinRefund UnitInterval + | PoolDecayRate Rational + | EMax Epoch + | Nopt Natural + | A0 Rational + | Rho UnitInterval + | Tau UnitInterval + | ActiveSlotCoefficient UnitInterval + | D UnitInterval + | ExtraEntropy Seed + | ProtocolVersion (Natural, Natural, Natural) + deriving (Show, Ord, Eq) + +data PPUpdate = PPUpdate (Map.Map VKeyGenesis (Map.Map Ppm Seed)) + deriving (Show, Ord, Eq) + +-- | Update Protocol Parameter update with new values, prefer value from `pup1` +-- in case of already existing value in `pup0` +updatePPup :: PPUpdate -> PPUpdate -> PPUpdate +updatePPup (PPUpdate pup0') (PPUpdate pup1') = PPUpdate $ Map.union pup1' pup0' + +newAVs :: Applications -> Map.Map Slot Applications -> Applications +newAVs avs favs = if not $ Map.null favs + then let maxSlot = maximum $ Map.keys favs in favs Map.! maxSlot -- value exists because maxSlot is in keys + else avs + +votedValue :: Eq a => Map.Map VKeyGenesis a -> Maybe a +votedValue vs | null elemLists = Nothing + | otherwise = Just $ (head . head) elemLists -- elemLists contains an element + -- and that list contains at + -- least 5 elements + where + elemLists = + filter (\l -> length l >= 5) $ List.group $ map snd $ Map.toList vs + +emptyUpdateState + :: ( Updates.PPUpdate + , Updates.AVUpdate + , Map.Map Slot Updates.Applications + , Updates.Applications + ) +emptyUpdateState = + (PPUpdate Map.empty, AVUpdate Map.empty, Map.empty, Applications Map.empty) + +emptyUpdate :: Update +emptyUpdate = Update (PPUpdate Map.empty) (AVUpdate Map.empty) diff --git a/shelley/chain-and-ledger/executable-spec/test/Generator.hs b/shelley/chain-and-ledger/executable-spec/test/Generator.hs index 11e05eade6e..a65f0ee6fd4 100644 --- a/shelley/chain-and-ledger/executable-spec/test/Generator.hs +++ b/shelley/chain-and-ledger/executable-spec/test/Generator.hs @@ -44,6 +44,7 @@ import LedgerState (LedgerState (..), stKeys ) import Slot +import Updates import UTxO import PParams (PParams(..), emptyPParams) import Delegation.Certificates (DCert(..), StakeKeys(..)) @@ -149,7 +150,7 @@ genTx keyList (UTxO m) cslot = do Map.empty -- TODO generate witdrawals txfee' (cslot + (Slot txttl)) - (EEnt Map.empty) + emptyUpdate let !txwit = makeWitness txbody selectedKeyPair pure (txfee', Tx txbody $ Set.fromList [txwit]) where utxoInputs = Map.keys m @@ -161,12 +162,12 @@ genTx keyList (UTxO m) cslot = do -- information in case of an invalid transaction. genLedgerStateTx :: KeyPairs -> Slot -> LedgerState -> Gen (Coin, Tx, Either [ValidationError] LedgerState) -genLedgerStateTx keyList (Slot slot) sourceState = do +genLedgerStateTx keyList (Slot _slot) sourceState = do let utxo' = sourceState ^. utxoState . utxo - let dms = _dms $ _dstate $ _delegationState sourceState - slot' <- genNatural slot (slot + 100) + let dms' = _dms $ _dstate $ _delegationState sourceState + slot' <- genNatural _slot (_slot + 100) (txfee', tx) <- genTx keyList utxo' (Slot slot') - pure (txfee', tx, asStateTransition (Slot slot') sourceState tx dms) + pure (txfee', tx, asStateTransition (Slot slot') defPCs sourceState tx dms') -- | Generator of a non-emtpy ledger genesis state and a random number of -- transactions applied to it. Returns the amount of accumulated fees, the @@ -204,11 +205,11 @@ repeatCollectTx -> [Tx] -> Gen (Coin, [Tx], Either [ValidationError] LedgerState) repeatCollectTx 0 _ _ fees ls txs = pure (fees, reverse txs, Right ls) -repeatCollectTx n keyPairs (Slot slot) fees ls txs = do - (txfee', tx, next) <- genLedgerStateTx keyPairs (Slot slot) ls +repeatCollectTx n keyPairs (Slot _slot) fees ls txs = do + (txfee', tx, next) <- genLedgerStateTx keyPairs (Slot _slot) ls case next of Left _ -> pure (fees, txs, next) - Right ls' -> repeatCollectTx (n - 1) keyPairs (Slot $ slot + 1) (txfee' + fees) ls' (tx:txs) + Right ls' -> repeatCollectTx (n - 1) keyPairs (Slot $ _slot + 1) (txfee' + fees) ls' (tx:txs) -- | Mutated variant of `repeatCollectTx'`, stops at recursion depth or after -- exhausting the UTxO set to prevent calling 'head' on empty input list. @@ -254,8 +255,8 @@ genValidLedgerState = do genValidSuccessorState :: KeyPairs -> Slot -> LedgerState -> Gen (Coin, Tx, LedgerState) -genValidSuccessorState keyPairs slot sourceState = do - (txfee', entry, next) <- genLedgerStateTx keyPairs slot sourceState +genValidSuccessorState keyPairs _slot sourceState = do + (txfee', entry, next) <- genLedgerStateTx keyPairs _slot sourceState case next of Left _ -> Gen.discard Right ls -> pure (txfee', entry, ls) @@ -281,13 +282,13 @@ genLedgerStateTx' :: KeyPairs -> LedgerState -> Gen (Coin, Tx, LedgerValidation) genLedgerStateTx' keyList sourceState = do let utxo' = sourceState ^. utxoState . utxo - let dms = _dms $ _dstate $ _delegationState sourceState - slot <- genNatural 0 1000 - (txfee', tx) <- genTx keyList utxo' (Slot slot) + let dms' = _dms $ _dstate $ _delegationState sourceState + _slot <- genNatural 0 1000 + (txfee', tx) <- genTx keyList utxo' (Slot _slot) tx' <- mutateTx tx pure (txfee' , tx' - , asStateTransition' (Slot slot) (LedgerValidation [] sourceState) tx' dms) + , asStateTransition' (Slot _slot) defPCs (LedgerValidation [] sourceState) tx' dms') -- Generators for 'DelegationData' diff --git a/shelley/chain-and-ledger/executable-spec/test/Mutator.hs b/shelley/chain-and-ledger/executable-spec/test/Mutator.hs index 771d2505036..b41e0fa490d 100644 --- a/shelley/chain-and-ledger/executable-spec/test/Mutator.hs +++ b/shelley/chain-and-ledger/executable-spec/test/Mutator.hs @@ -30,6 +30,7 @@ import Delegation.Certificates (DCert(..)) import Delegation.PoolParams import Keys import LedgerState (DPState(..), KeyPairs) +import Updates import UTxO (TxBody(..), Tx(..), TxIn(..), TxOut(..)) import Slot @@ -89,7 +90,7 @@ mutateTxBody tx = do (_wdrls tx) (_txfee tx) (_ttl tx) - (_txeent tx) + emptyUpdate -- | Mutator for a list of 'TxIn'. mutateInputs :: [TxIn] -> Gen [TxIn] diff --git a/shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs b/shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs index 0678151ed06..99a431bfec2 100644 --- a/shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs +++ b/shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs @@ -22,6 +22,7 @@ import Generator import Coin import LedgerState hiding (dms) import Slot +import PParams import UTxO @@ -169,8 +170,8 @@ propertyTests = testGroup "Property-Based Testing" "No Double Spend in valid ledger states" propNoDoubleSpend , testProperty - "changing witness set" - propCheckMinimalWitnessSet + "adding redundant witness" + propCheckRedundantWitnessSet , testProperty "using subset of witness set" propCheckMissingWitness @@ -218,27 +219,26 @@ propBalanceTxInTxOut' = )) success --- | Check that we correctly report redundant witnesses. We get the list of the +-- | Check that we correctly test redundant witnesses. We get the list of the -- keys from the generator and use one to generate a new witness. If that key --- was used to sign the transaction, then the transaction must validate. If the --- witness was not already used to sign the transaction, a `UnneededWitnesses` --- validation error must be reported. -propCheckMinimalWitnessSet :: Property -propCheckMinimalWitnessSet = property $ do +-- was used to sign the transaction, then the transaction must validate. If a +-- new, redundant witness signature is added, the transaction must still +-- validate. +propCheckRedundantWitnessSet :: Property +propCheckRedundantWitnessSet = property $ do (l, steps, _, txwits, _, keyPairs) <- forAll genValidStateTxKeys let keyPair = fst $ head keyPairs let tx = txwits ^. body let witness = makeWitness tx keyPair let txwits' = txwits & witnessSet %~ (Set.insert witness) let dms = _dms $ _dstate $ _delegationState l - let l'' = asStateTransition (Slot (steps)) l txwits' dms + let l'' = asStateTransition (Slot (steps)) emptyPParams l txwits' dms classify "unneeded signature added" (not $ witness `Set.member` (txwits ^. witnessSet)) case l'' of - Left [UnneededWitnesses] -> - (witness `Set.member` (txwits ^. witnessSet)) === False Right _ -> - (witness `Set.member` (txwits ^. witnessSet)) === True + True === (Set.null $ + Set.filter (\wit -> not $ verifyWit tx wit) (_witnessSet txwits')) _ -> failure -- | Check that we correctly report missing witnesses. @@ -250,7 +250,7 @@ propCheckMissingWitness = property $ do let witnessSet'' = txwits ^. witnessSet let witnessSet' = Set.fromList witnessList let dms = _dms $ _dstate $ _delegationState l - let l' = asStateTransition (Slot steps) l (txwits & witnessSet .~ witnessSet') dms + let l' = asStateTransition (Slot steps) emptyPParams l (txwits & witnessSet .~ witnessSet') dms let isRealSubset = witnessSet' `Set.isSubsetOf` witnessSet'' && witnessSet' /= witnessSet'' classify "real subset" (isRealSubset) @@ -266,9 +266,9 @@ propPreserveBalance = property $ do (l, _, fee, tx, l') <- forAll genValidStateTx let destroyed = (balance (l ^. utxoState . utxo)) - + (keyRefunds (l ^. pcs) (l ^. delegationState . dstate . stKeys) $ tx ^. body) + + (keyRefunds emptyPParams (l ^. delegationState . dstate . stKeys) $ tx ^. body) let created = (balance (l' ^. utxoState . utxo)) + fee - + (deposits (l' ^. pcs) (l' ^. delegationState . pstate . stPools) $ tx ^.body . certs) + + (deposits emptyPParams (l' ^. delegationState . pstate . stPools) $ tx ^.body . certs) destroyed === created diff --git a/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs b/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs index 5359e97464b..116d50a6300 100644 --- a/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs +++ b/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs @@ -22,6 +22,7 @@ import Keys import LedgerState hiding (dms) import PParams import Slot +import Updates import UTxO alicePay :: KeyPair @@ -69,8 +70,8 @@ stakePoolKey1 :: KeyPair stakePoolKey1 = keyPair (Owner 5) ledgerState :: [Tx] -> Either [ValidationError] LedgerState -ledgerState = foldM (\l t -> asStateTransition (Slot 0) l t dms) genesis - where dms = _dms $ _dstate $ _delegationState genesis +ledgerState = foldM (\l t -> asStateTransition (Slot 0) testPCs l t dms') genesis + where dms' = _dms $ _dstate $ _delegationState genesis testLedgerValidTransactions :: @@ -79,10 +80,7 @@ testLedgerValidTransactions ls utxoState' = ls @?= Right (LedgerState utxoState' LedgerState.emptyDelegation - emptyUPIState - testPCs - 1 - (Slot 0)) + 1) testValidStakeKeyRegistration :: Tx -> UTxOState -> DPState -> Assertion @@ -92,10 +90,7 @@ testValidStakeKeyRegistration tx utxoState' stakeKeyRegistration = in ls2 @?= Right (LedgerState utxoState' stakeKeyRegistration - emptyUPIState - testPCs - 1 - (Slot 0)) + 1) testValidDelegation :: [Tx] -> UTxOState -> DPState -> PoolParams -> Assertion @@ -110,10 +105,7 @@ testValidDelegation txs utxoState' stakeKeyRegistration pool = & dstate . delegations .~ Map.fromList [(hashKey $ vKey aliceStake, poolhk)] & pstate . stPools .~ (StakePools $ Map.fromList [(poolhk, Slot 0)]) & pstate . pParams .~ Map.fromList [(poolhk, pool)]) - emptyUPIState - testPCs - (fromIntegral $ length txs) - (Slot 0)) + (fromIntegral $ length txs)) testValidRetirement :: [Tx] -> UTxOState -> DPState -> Epoch -> PoolParams -> Assertion @@ -129,10 +121,7 @@ testValidRetirement txs utxoState' stakeKeyRegistration e pool = & pstate . stPools .~ (StakePools $ Map.fromList [(poolhk, Slot 0)]) & pstate . pParams .~ Map.fromList [(poolhk, pool)] & pstate . retiring .~ Map.fromList [(poolhk, e)]) - emptyUPIState - testPCs - 3 - (Slot 0)) + 3) bobWithdrawal :: Map RewardAcnt Coin bobWithdrawal = Map.singleton (mkRwdAcnt bobStake) (Coin 10) @@ -151,22 +140,19 @@ testValidWithdrawal = bobWithdrawal (Coin 1000) (Slot 0) - (EEnt Map.empty) + emptyUpdate wits = makeWitnesses tx [alicePay, bobStake] utxo' = Map.fromList [ (TxIn genesisId 1, TxOut bobAddr (Coin 1000)) , (TxIn (txid tx) 0, TxOut aliceAddr (Coin 6000)) , (TxIn (txid tx) 1, TxOut bobAddr (Coin 3010)) ] - ls = asStateTransition (Slot 0) genesisWithReward (Tx tx wits) (Dms Map.empty) + ls = asStateTransition (Slot 0) testPCs genesisWithReward (Tx tx wits) (Dms Map.empty) expectedDS = LedgerState.emptyDelegation & dstate . rewards .~ Map.singleton (mkRwdAcnt bobStake) (Coin 0) in ls @?= Right (LedgerState - (UTxOState (UTxO utxo') (Coin 0) (Coin 1000) (EEnt Map.empty)) + (UTxOState (UTxO utxo') (Coin 0) (Coin 1000) emptyUpdateState) expectedDS - emptyUPIState - testPCs - 1 - (Slot 0)) + 1) testInvalidWintess :: Assertion testInvalidWintess = @@ -179,28 +165,11 @@ testInvalidWintess = Map.empty (Coin 1000) (Slot 1) - (EEnt Map.empty) + emptyUpdate tx' = tx & ttl .~ Slot 2 wits = makeWitnesses tx' [alicePay] in ledgerState [Tx tx wits] @?= Left [InvalidWitness] - -testTooManyWintesses :: Assertion -testTooManyWintesses = - let - tx = TxBody - (Set.fromList [TxIn genesisId 0]) - [ TxOut aliceAddr (Coin 6000) - , TxOut bobAddr (Coin 3000) ] - [] - Map.empty - (Coin 1000) - (Slot 1) - (EEnt Map.empty) - wits = makeWitnesses tx [alicePay, bobStake] - in ledgerState [Tx tx wits] @?= Left [UnneededWitnesses] - - testWithdrawalNoWit :: Assertion testWithdrawalNoWit = let @@ -212,9 +181,9 @@ testWithdrawalNoWit = bobWithdrawal (Coin 1000) (Slot 0) - (EEnt Map.empty) + emptyUpdate wits = Set.singleton $ makeWitness tx alicePay - ls = asStateTransition (Slot 0) genesisWithReward (Tx tx wits) (Dms Map.empty) + ls = asStateTransition (Slot 0) testPCs genesisWithReward (Tx tx wits) (Dms Map.empty) in ls @?= Left [MissingWitnesses] testWithdrawalWrongAmt :: Assertion @@ -228,9 +197,9 @@ testWithdrawalWrongAmt = (Map.singleton (mkRwdAcnt bobStake) (Coin 11)) (Coin 1000) (Slot 0) - (EEnt Map.empty) + emptyUpdate wits = makeWitnesses tx [alicePay, bobStake] - ls = asStateTransition (Slot 0) genesisWithReward (Tx tx wits) (Dms Map.empty) + ls = asStateTransition (Slot 0) testPCs genesisWithReward (Tx tx wits) (Dms Map.empty) in ls @?= Left [IncorrectRewards] aliceGivesBobLovelace :: TxIn -> Coin -> Coin -> Coin -> Coin -> @@ -246,7 +215,7 @@ aliceGivesBobLovelace txin coin fee txdeps txrefs cs s signers = Tx txbody wits Map.empty fee s - (EEnt Map.empty) + emptyUpdate wits = makeWitnesses txbody signers tx1 :: Tx @@ -266,7 +235,7 @@ utxoSt1 = UTxOState , (TxIn (txid $ tx1 ^. body) 1, TxOut bobAddr (Coin 3000)) ]) (Coin 0) (Coin 600) - (EEnt Map.empty) + emptyUpdateState ls1 :: Either [ValidationError] LedgerState ls1 = ledgerState [tx1] @@ -290,7 +259,7 @@ utxoSt2 = UTxOState , (TxIn (txid $ tx2 ^. body) 1, TxOut bobAddr (Coin 3000)) ]) (Coin 300) (Coin 1300) - (EEnt Map.empty) + emptyUpdateState tx3Body :: TxBody tx3Body = TxBody @@ -301,7 +270,7 @@ tx3Body = TxBody Map.empty (Coin 1200) (Slot 100) - (EEnt Map.empty) + emptyUpdate tx3 :: Tx tx3 = Tx tx3Body (makeWitnesses tx3Body keys) @@ -315,7 +284,7 @@ utxoSt3 = UTxOState , (TxIn (txid $ tx2 ^. body) 1, TxOut bobAddr (Coin 3000)) ]) (Coin 550) (Coin 2500) - (EEnt Map.empty) + emptyUpdateState stakeKeyRegistration1 :: DPState stakeKeyRegistration1 = LedgerState.emptyDelegation @@ -371,7 +340,7 @@ tx4Body = TxBody Map.empty (Coin 1000) (Slot 100) - (EEnt Map.empty) + emptyUpdate tx4 :: Tx tx4 = Tx tx4Body (makeWitnesses tx4Body [alicePay, stakePoolKey1]) @@ -384,7 +353,7 @@ utxoSt4 = UTxOState , (TxIn (txid $ tx2 ^. body) 1, TxOut bobAddr (Coin 3000)) ]) (Coin 550) (Coin 3500) - (EEnt Map.empty) + emptyUpdateState utxo5 :: Epoch -> UTxOState utxo5 e = UTxOState @@ -394,7 +363,7 @@ utxo5 e = UTxOState , (TxIn (txid $ tx2 ^. body) 1, TxOut bobAddr (Coin 3000)) ]) (Coin 550) (Coin 3500) - (EEnt Map.empty) + emptyUpdateState tx5Body :: Epoch -> TxBody tx5Body e = TxBody @@ -404,7 +373,7 @@ tx5Body e = TxBody Map.empty (Coin 1000) (Slot 100) - (EEnt Map.empty) + emptyUpdate tx5 :: Epoch -> Tx tx5 e = Tx (tx5Body e) (makeWitnesses (tx5Body e) [alicePay, stakePoolKey1]) @@ -441,9 +410,7 @@ testSpendNonexistentInput = [alicePay] in ledgerState [tx] @?= Left [ BadInputs - , ValueNotConserved (Coin 0) (Coin 10000) - , UnneededWitnesses] - -- Note that BadInputs implies UnneededWitnesses + , ValueNotConserved (Coin 0) (Coin 10000)] testWitnessNotIncluded :: Assertion testWitnessNotIncluded = @@ -456,7 +423,7 @@ testWitnessNotIncluded = Map.empty (Coin 596) (Slot 100) - (EEnt Map.empty) + emptyUpdate tx = Tx txbody Set.empty in ledgerState [tx] @?= Left [MissingWitnesses] @@ -470,10 +437,10 @@ testSpendNotOwnedUTxO = Map.empty (Coin 768) (Slot 100) - (EEnt Map.empty) + emptyUpdate aliceWit = makeWitness txbody alicePay tx = Tx txbody (Set.fromList [aliceWit]) - in ledgerState [tx] @?= Left [MissingWitnesses, UnneededWitnesses] + in ledgerState [tx] @?= Left [MissingWitnesses] testWitnessWrongUTxO :: Assertion testWitnessWrongUTxO = @@ -485,7 +452,7 @@ testWitnessWrongUTxO = Map.empty (Coin 770) (Slot 100) - (EEnt Map.empty) + emptyUpdate tx2body = TxBody (Set.fromList [TxIn genesisId 1]) [ TxOut aliceAddr (Coin 230)] @@ -493,12 +460,11 @@ testWitnessWrongUTxO = Map.empty (Coin 770) (Slot 101) - (EEnt Map.empty) + emptyUpdate aliceWit = makeWitness tx2body alicePay tx = Tx txbody (Set.fromList [aliceWit]) in ledgerState [tx] @?= Left [ InvalidWitness - , MissingWitnesses - , UnneededWitnesses ] + , MissingWitnesses] testEmptyInputSet :: Assertion testEmptyInputSet = @@ -511,10 +477,10 @@ testEmptyInputSet = aliceWithdrawal (Coin 1000) (Slot 0) - (EEnt Map.empty) + emptyUpdate wits = makeWitnesses tx [aliceStake] genesisWithReward' = changeReward genesis (mkRwdAcnt aliceStake) (Coin 2000) - ls = asStateTransition (Slot 0) genesisWithReward' (Tx tx wits) (Dms Map.empty) + ls = asStateTransition (Slot 0) testPCs genesisWithReward' (Tx tx wits) (Dms Map.empty) in ls @?= Left [ InputSetEmpty ] testFeeTooSmall :: Assertion @@ -538,7 +504,7 @@ testExpiredTx = [] (Slot 0) [alicePay] - in asStateTransition (Slot 1) genesis tx (Dms Map.empty) @?= + in asStateTransition (Slot 1) testPCs genesis tx (Dms Map.empty) @?= Left [ Expired (Slot 0) (Slot 1) ] testsInvalidLedger :: TestTree @@ -551,7 +517,6 @@ testsInvalidLedger = testGroup "Tests with invalid transactions in ledger" , testCase "Invalid Ledger - Alice's fee is too small" testFeeTooSmall , testCase "Invalid Ledger - Alice's transaction has expired" testExpiredTx , testCase "Invalid Ledger - Invalid witnesses" testInvalidWintess - , testCase "Invalid Ledger - Too many witnesses" testTooManyWintesses , testCase "Invalid Ledger - No withdrawal witness" testWithdrawalNoWit , testCase "Invalid Ledger - Incorrect withdrawal amount" testWithdrawalWrongAmt ] diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index d773a617461..c32e20215c5 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -708,7 +708,8 @@ \subsection{Block Header Transition} \var{nes}' } \\~\\ - (\wcard,~\wcard,~\var{b_{prev}},~\wcard,~\var{es},~\var{ru},~\wcard,~\wcard)\leteq\var{nes} + (\wcard,~\wcard,~\var{b_{prev}},~\wcard,~\var{es},~\var{ru},~\wcard,~\wcard)\leteq\var{nes} \\ + (\wcard,~\wcard,~\wcard,~\var{es})\leteq \var{es} \\ { \left( @@ -852,6 +853,7 @@ \subsection{Verifiable Random Function} & ~~~~\where \\ & ~~~~~~~~~~\var{hk} \leteq \hashKey{(\bvkcold bhb)} \\ & ~~~~~~~~~~\var{ss} \leteq \slotToSeed{(\bslot{bhb})} \\ + & ~~~~~~~~~~\var{vk} \leteq \fun{bvkcold}~\var{bhb} \\ \end{align*} \label{fig:vrf-checks} \end{figure} @@ -1357,9 +1359,9 @@ \subsection{Chain Transition} \left(\begin{array}{c} \var{pp} \\ \var{osched} \\ - \var{dms} \\ \eta_0 \\ \var{pd} \\ + \var{dms} \\ \end{array}\right)\\ \var{s_{now}} \\ \end{array}} @@ -1381,7 +1383,7 @@ \subsection{Chain Transition} \eta_c' \\ \end{array}\right)} } \\~\\~\\ - \var{ls'}\leteq\fun{setIssueNumbers}~\var{ls}~\var{cs} \\ + \var{ls'}\leteq\fun{setIssueNumbers}~\var{ls}~\var{cs'} \\ { {\left(\begin{array}{c} \dom{osched} \\ diff --git a/shelley/chain-and-ledger/formal-spec/update.tex b/shelley/chain-and-ledger/formal-spec/update.tex index 3cd2441e10b..d3414e795b6 100644 --- a/shelley/chain-and-ledger/formal-spec/update.tex +++ b/shelley/chain-and-ledger/formal-spec/update.tex @@ -15,7 +15,7 @@ \section{Updates} $\mathsf{PPUP}$ transition for the protocol parameters and the the $\mathsf{AVUP}$ transition for the application versions. Recall that $\PPUpdate$, $\AVUpdate$, and $\Update$ were defined in -Figure~\ref{fig:defs:utxo-shelley} +Figure~\ref{fig:defs:utxo-shelley} The signature for the keys in the proposal will be checked in the @@ -327,7 +327,7 @@ \section{Updates} \begin{equation}\label{eq:update} \inference[Update] { - (\var{pup},~\var{aup})\leteq\var{up} + (\var{pup_{u}},~\var{aup_{u}})\leteq\var{up} \\~\\ { \left( @@ -339,7 +339,7 @@ \section{Updates} } \vdash \left(\var{pup}\right) - \trans{\hyperref[fig:rules:pp-update]{ppup}}{\var{pup}} + \trans{\hyperref[fig:rules:pp-update]{ppup}}{\var{pup_{u}}} \left(\var{pup'}\right) & { @@ -360,7 +360,7 @@ \section{Updates} \end{array} \right) } - \trans{\hyperref[fig:rules:av-update]{avup}}{\var{aup}} + \trans{\hyperref[fig:rules:av-update]{avup}}{\var{aup_{u}}} { \left( \begin{array}{r} diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex index dcf584e2c35..ad8c776512b 100644 --- a/shelley/chain-and-ledger/formal-spec/utxo.tex +++ b/shelley/chain-and-ledger/formal-spec/utxo.tex @@ -336,7 +336,7 @@ \subsection{UTxO Transitions} \var{utxo} \\ \var{deposits} \\ \var{fees} \\ - \var{up}\\ + \var{ups}\\ \end{array} \right) \trans{utxo}{tx} @@ -551,9 +551,9 @@ \subsection{Witnesses} \begin{figure}[htb] \begin{align*} - & \fun{propWits} \in \Update \to \powerset{\HashKey} + & \fun{propWits} \in \Update \to (\VKeyGen\mapsto\VKey) \to \powerset{\HashKey} & \text{hashkeys for proposals} \\ - & \fun{propWits}~(\var{pup},~\var{aup}) = \\ + & \fun{propWits}~(\var{pup},~\var{aup}) \var{dms} = \\ & ~~\left\{ \hashKey{vkey} \mid