From c6e8d91075604d203ad56f7e0bc7166a8a312e2c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Mon, 17 Jun 2019 17:12:28 +0200 Subject: [PATCH 01/22] Add `OVERLAY` STS rule in exec spec --- .../executable-spec/delegation.cabal | 1 + .../executable-spec/src/BaseTypes.hs | 4 +- .../executable-spec/src/BlockChain.hs | 66 +++++++++++++++-- .../executable-spec/src/STS/Overlay.hs | 72 +++++++++++++++++++ .../chain-and-ledger/formal-spec/chain.tex | 1 + 5 files changed, 139 insertions(+), 5 deletions(-) create mode 100644 shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs diff --git a/shelley/chain-and-ledger/executable-spec/delegation.cabal b/shelley/chain-and-ledger/executable-spec/delegation.cabal index a88a16b7396..5d32189b4bb 100644 --- a/shelley/chain-and-ledger/executable-spec/delegation.cabal +++ b/shelley/chain-and-ledger/executable-spec/delegation.cabal @@ -41,6 +41,7 @@ library STS.NewEpoch STS.Newpp STS.Ocert + STS.Overlay STS.Pool STS.PoolReap STS.Rupd diff --git a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs index 409e0674fb0..0c3ee35a214 100644 --- a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs +++ b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs @@ -9,7 +9,7 @@ module BaseTypes , intervalValue , interval0 , interval1 - , Seed + , Seed(..) , mkNonce , seedOp , neutralSeed @@ -59,6 +59,8 @@ interval1 = UnitInterval 1 data Seed = Nonce Integer | NeutralSeed + | SeedL + | SeedEta | SeedOp Seed Seed deriving (Show, Eq, Ord) diff --git a/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs b/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs index da6d2065838..24757da44ca 100644 --- a/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs @@ -4,6 +4,7 @@ module BlockChain , BHeader(..) , Block(..) , bhHash + , bhbHash , bHeaderSize , bBodySize , slotToSeed @@ -18,33 +19,59 @@ module BlockChain , verifyVrf , seedEta , seedL + , bvkcold + , vrfChecks ) 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 Delegation.Certificates import qualified Keys as Keys import OCert import qualified Slot as Slot import qualified UTxO as U --- |The hash of public Key +import NonIntegral ((***)) + +-- |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 +96,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 +136,38 @@ 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 pd'@(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 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..04c1e0e411e --- /dev/null +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs @@ -0,0 +1,72 @@ +{-# 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 + -- | Praos schedule + Nothing -> do + vrfChecks eta0 pd (_activeSlotCoeff pp) bhb ?! NotPraosLeaderOVERLAY + cs' <- trans @OCERT $ TRC ((), cs, bh) + pure cs' + -- | Found in OBFT overlay schedule + Just gkey' -> do + case gkey' of + -- | osched is a mapping `Slot |-> Maybe VKeyGenesis`, so `gkey''` can + -- be `Just Nothing` + 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/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index d773a617461..f1a9ece87fd 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -852,6 +852,7 @@ \subsection{Verifiable Random Function} & ~~~~\where \\ & ~~~~~~~~~~\var{hk} \leteq \hashKey{(\bvkcold bhb)} \\ & ~~~~~~~~~~\var{ss} \leteq \slotToSeed{(\bslot{bhb})} \\ + % TODO : is vk = bvkcold bhb ? \end{align*} \label{fig:vrf-checks} \end{figure} From 50e4b34d6b7d52461810d4188dd631818bfd69c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 18 Jun 2019 12:06:03 +0200 Subject: [PATCH 02/22] Add `PRTCL` STS rule --- .../executable-spec/src/STS/Prtcl.hs | 66 +++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 shelley/chain-and-ledger/executable-spec/src/STS/Prtcl.hs 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 From 22e298d05068ef9250cc307b6a8114473fd64482 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 18 Jun 2019 13:19:26 +0200 Subject: [PATCH 03/22] Adapt `CHAIN` STS rule with call to `PRTCL` --- .../executable-spec/src/STS/Chain.hs | 89 ++++++------------- 1 file changed, 25 insertions(+), 64 deletions(-) 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..c61534809ae 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs @@ -21,83 +21,44 @@ 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 nes'@(NewEpochState _ eta0 _ bCur es _ _pd osched) = nes -- TODO: converge BHEAD + 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 + pure undefined -instance Embed NEWEPOCH CHAIN where - wrapFailed = NewepochFailure +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 From 98f20b2256eeae4f3367fc8ff7a5804daf2cc494 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 18 Jun 2019 13:20:23 +0200 Subject: [PATCH 04/22] Fix Environment type in `CHAIN` rule --- shelley/chain-and-ledger/formal-spec/chain.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index f1a9ece87fd..c665653429c 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -1358,9 +1358,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}} From 7766aab5700cae1e2080f7dfeff924386341074e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 18 Jun 2019 13:58:26 +0200 Subject: [PATCH 05/22] Adapt `BHEAD` STS rule --- .../executable-spec/src/BlockChain.hs | 4 ++ .../executable-spec/src/STS/Bhead.hs | 67 ++++++++++--------- .../chain-and-ledger/formal-spec/chain.tex | 1 + 3 files changed, 41 insertions(+), 31 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs b/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs index 24757da44ca..f6e4f5bf3a6 100644 --- a/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs @@ -8,6 +8,7 @@ module BlockChain , bHeaderSize , bBodySize , slotToSeed + , hBbsize -- accessor functions , bheader , bhbody @@ -171,3 +172,6 @@ seedL = mkNonce 1 bvkcold :: BHBody -> Keys.VKey bvkcold bhb = ocertVkCold $ bheaderOCert bhb + +hBbsize :: BHBody -> Natural +hBbsize = bsize 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..55e75be4cac 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,66 @@ -{-# LANGUAGE EmptyDataDecls #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} module STS.Bhead ( BHEAD ) where import qualified Data.Map.Strict as Map - +import qualified Data.Set as Set import Crypto.Hash (hash) import qualified Data.ByteString.Char8 as BS +import BaseTypes import BlockChain import Keys +import LedgerState import OCert 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)) <- - judgmentContext + 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 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/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index c665653429c..67413239466 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -709,6 +709,7 @@ \subsection{Block Header Transition} } \\~\\ (\wcard,~\wcard,~\var{b_{prev}},~\wcard,~\var{es},~\var{ru},~\wcard,~\wcard)\leteq\var{nes} + % TODO: is es = (_ _ _ pp) ? \\ { \left( From 4141a28d4db5476b9bfcf74ca5cbaff51a94312d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 18 Jun 2019 14:06:11 +0200 Subject: [PATCH 06/22] Call `BHEAD` from `CHAIN` --- shelley/chain-and-ledger/executable-spec/delegation.cabal | 1 + .../chain-and-ledger/executable-spec/src/LedgerState.hs | 7 +++++++ shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs | 5 ++++- .../chain-and-ledger/executable-spec/src/STS/Overlay.hs | 4 ---- 4 files changed, 12 insertions(+), 5 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/delegation.cabal b/shelley/chain-and-ledger/executable-spec/delegation.cabal index 5d32189b4bb..3272a17e990 100644 --- a/shelley/chain-and-ledger/executable-spec/delegation.cabal +++ b/shelley/chain-and-ledger/executable-spec/delegation.cabal @@ -44,6 +44,7 @@ library STS.Overlay STS.Pool STS.PoolReap + STS.Prtcl STS.Rupd STS.Snap STS.Updn diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index 905832c52df..6917cfefb4b 100644 --- a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs +++ b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs @@ -108,6 +108,7 @@ module LedgerState , NewEpochState(..) , NewEpochEnv(..) , overlaySchedule + , getGKeys ) where import Control.Monad (foldM) @@ -317,6 +318,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 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 c61534809ae..22d11e7d60e 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs @@ -45,7 +45,10 @@ chainTransition :: TransitionRule CHAIN chainTransition = do TRC (sNow, (nes, etaV, etaC, h, sL), block@(Block bh _)) <- judgmentContext - let nes'@(NewEpochState _ eta0 _ bCur es _ _pd osched) = nes -- TODO: converge BHEAD + 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 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 04c1e0e411e..d3d28709721 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs @@ -49,16 +49,12 @@ overlayTransition = do let gkey'' = Map.lookup (bheaderSlot bhb) osched let vk = bvkcold bhb case gkey'' of - -- | Praos schedule Nothing -> do vrfChecks eta0 pd (_activeSlotCoeff pp) bhb ?! NotPraosLeaderOVERLAY cs' <- trans @OCERT $ TRC ((), cs, bh) pure cs' - -- | Found in OBFT overlay schedule Just gkey' -> do case gkey' of - -- | osched is a mapping `Slot |-> Maybe VKeyGenesis`, so `gkey''` can - -- be `Just Nothing` Nothing -> failBecause NotActiveSlotOVERLAY Just gkey -> do let dmsKey' = Map.lookup gkey dms From 5cce29123a9a1b5a0e1c09e58fc0533ec437d5b5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 19 Jun 2019 12:02:52 +0200 Subject: [PATCH 07/22] Add Updates module --- .../executable-spec/delegation.cabal | 1 + .../executable-spec/src/Updates.hs | 51 +++++++++++++++++++ 2 files changed, 52 insertions(+) create mode 100644 shelley/chain-and-ledger/executable-spec/src/Updates.hs diff --git a/shelley/chain-and-ledger/executable-spec/delegation.cabal b/shelley/chain-and-ledger/executable-spec/delegation.cabal index 3272a17e990..0a769a907bf 100644 --- a/shelley/chain-and-ledger/executable-spec/delegation.cabal +++ b/shelley/chain-and-ledger/executable-spec/delegation.cabal @@ -29,6 +29,7 @@ library Delegation.PoolParams Delegation.Certificates OCert + Updates STS.Bbody STS.Bhead STS.Chain 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..f65b3892af7 --- /dev/null +++ b/shelley/chain-and-ledger/executable-spec/src/Updates.hs @@ -0,0 +1,51 @@ +{-# LANGUAGE EmptyDataDecls #-} + +module Updates + ( PPUpdateEnv(..) + , PPUpdate(..) + , updatePPup + ) +where + +import qualified Data.Map.Strict as Map + +import BaseTypes +import Coin +import Keys +import Slot + +import Numeric.Natural + +data PPUpdateEnv = PPUpdateEnv { + slot :: Slot + , dms :: Dms + } deriving Show + +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 + +data PPUpdate = PPUpdate (Map.Map VKeyGenesis (Map.Map Ppm Seed)) + deriving Show + +-- | 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' From ef9e6287435cbeeb690e9d5d994d9e3eb3a5dbbe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 19 Jun 2019 12:04:31 +0200 Subject: [PATCH 08/22] Add `PPUP` STS rule --- .../executable-spec/delegation.cabal | 1 + .../executable-spec/src/STS/Ppup.hs | 51 +++++++++++++++++++ .../executable-spec/src/Slot.hs | 6 ++- 3 files changed, 57 insertions(+), 1 deletion(-) create mode 100644 shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs diff --git a/shelley/chain-and-ledger/executable-spec/delegation.cabal b/shelley/chain-and-ledger/executable-spec/delegation.cabal index 0a769a907bf..6025b6e733e 100644 --- a/shelley/chain-and-ledger/executable-spec/delegation.cabal +++ b/shelley/chain-and-ledger/executable-spec/delegation.cabal @@ -45,6 +45,7 @@ library STS.Overlay STS.Pool STS.PoolReap + STS.Ppup STS.Prtcl STS.Rupd STS.Snap 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..08981a633c3 --- /dev/null +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs @@ -0,0 +1,51 @@ +{-# 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 Numeric.Natural ( Natural ) + +import BaseTypes +import BlockChain +import Delegation.Certificates +import Keys +import PParams +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/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) From 519b10cbbf43d639bea5887d5c79efb39e367f59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 19 Jun 2019 12:57:36 +0200 Subject: [PATCH 09/22] Add ApplicationUpdate types and helper functions --- .../executable-spec/src/Keys.hs | 4 +- .../executable-spec/src/Updates.hs | 50 +++++++++++++++++-- 2 files changed, 49 insertions(+), 5 deletions(-) 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/Updates.hs b/shelley/chain-and-ledger/executable-spec/src/Updates.hs index f65b3892af7..ed1432971af 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Updates.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Updates.hs @@ -4,10 +4,17 @@ module Updates ( PPUpdateEnv(..) , PPUpdate(..) , updatePPup + , ApName(..) + , ApVer(..) + , Metadata + , Applications(..) + , newAVs + , votedValue ) where import qualified Data.Map.Strict as Map +import qualified Data.List as List (group) import BaseTypes import Coin @@ -16,10 +23,31 @@ 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 + } deriving (Show, Ord, Eq) data Ppm = MinFeeA Integer | MinFeeB Natural @@ -40,12 +68,28 @@ data Ppm = MinFeeA Integer | D UnitInterval | ExtraEntropy Seed | ProtocolVersion (Natural, Natural, Natural) - deriving Show + deriving (Show, Ord, Eq) data PPUpdate = PPUpdate (Map.Map VKeyGenesis (Map.Map Ppm Seed)) - deriving Show + 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 From 54fc3934137edc2813ec7b226c04705d713da212 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 19 Jun 2019 13:58:35 +0200 Subject: [PATCH 10/22] Add `AVUP` STS rule --- .../executable-spec/src/STS/Avup.hs | 55 +++++++++++++++++++ .../executable-spec/src/Updates.hs | 2 + .../chain-and-ledger/formal-spec/update.tex | 4 +- 3 files changed, 59 insertions(+), 2 deletions(-) create mode 100644 shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs 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..73ee3337c72 --- /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/Updates.hs b/shelley/chain-and-ledger/executable-spec/src/Updates.hs index ed1432971af..69c34889b34 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Updates.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Updates.hs @@ -8,6 +8,8 @@ module Updates , ApVer(..) , Metadata , Applications(..) + , AVUpdate(..) + , Update(..) , newAVs , votedValue ) diff --git a/shelley/chain-and-ledger/formal-spec/update.tex b/shelley/chain-and-ledger/formal-spec/update.tex index 3cd2441e10b..1daeb5188e8 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 @@ -244,7 +244,7 @@ \section{Updates} & \dom{\var{aup}}\subseteq\dom{\var{dms}} \\ - \var{aup'}\leteq\var{aup_s}\unionoverrideRight\var{aup} + \var{aup'}\leteq\var{aup_s}\unionoverrideRight\var{aup} % TODO: not needed here? & \var{fav}\leteq\fun{votedValue_{Applications}}~\var{aup'} \\ From a804097a5f9e1516385058a32b34df4ec2afe3db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 19 Jun 2019 14:15:00 +0200 Subject: [PATCH 11/22] Add `UP` STS rule --- .../executable-spec/delegation.cabal | 2 + .../executable-spec/src/STS/Up.hs | 49 +++++++++++++++++++ .../chain-and-ledger/formal-spec/update.tex | 3 +- 3 files changed, 53 insertions(+), 1 deletion(-) create mode 100644 shelley/chain-and-ledger/executable-spec/src/STS/Up.hs diff --git a/shelley/chain-and-ledger/executable-spec/delegation.cabal b/shelley/chain-and-ledger/executable-spec/delegation.cabal index 6025b6e733e..88dfae2168b 100644 --- a/shelley/chain-and-ledger/executable-spec/delegation.cabal +++ b/shelley/chain-and-ledger/executable-spec/delegation.cabal @@ -30,6 +30,7 @@ library Delegation.Certificates OCert Updates + STS.Avup STS.Bbody STS.Bhead STS.Chain @@ -49,6 +50,7 @@ library STS.Prtcl STS.Rupd STS.Snap + STS.Up STS.Updn STS.Utxo STS.Utxow 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..feeb264ae35 --- /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/formal-spec/update.tex b/shelley/chain-and-ledger/formal-spec/update.tex index 1daeb5188e8..6d8bdf73803 100644 --- a/shelley/chain-and-ledger/formal-spec/update.tex +++ b/shelley/chain-and-ledger/formal-spec/update.tex @@ -327,7 +327,8 @@ \section{Updates} \begin{equation}\label{eq:update} \inference[Update] { - (\var{pup},~\var{aup})\leteq\var{up} + (\var{pup},~\var{aup})\leteq\var{up} % TODO: duplicate of state names in + % signal \\~\\ { \left( From b85270b526ed8162373516de16f44cae39e991bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 19 Jun 2019 15:15:08 +0200 Subject: [PATCH 12/22] Adapt `UTXO` STS rule --- .../executable-spec/src/LedgerState.hs | 39 ++++++++++++------- .../executable-spec/src/STS/Newpp.hs | 3 +- .../executable-spec/src/STS/Snap.hs | 3 +- .../executable-spec/src/STS/Utxo.hs | 27 ++++++++++--- .../executable-spec/src/UTxO.hs | 6 +++ .../executable-spec/src/Updates.hs | 14 +++++++ shelley/chain-and-ledger/formal-spec/utxo.tex | 2 +- 7 files changed, 72 insertions(+), 22 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index 6917cfefb4b..b2e7acdc8f5 100644 --- a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs +++ b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs @@ -80,7 +80,7 @@ module LedgerState , utxo , deposited , fees - , eEntropy + , ups -- DelegationState , rewards , stKeys @@ -132,6 +132,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 (..), @@ -265,13 +266,14 @@ 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 + emptyUPIState + emptyPParams + 0 + (Slot 0) emptyAccount :: AccountState emptyAccount = AccountState (Coin 0) (Coin 0) @@ -290,11 +292,13 @@ 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 @@ -357,7 +361,16 @@ 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 + (EEnt Map.empty)) -- |Creates the ledger state for an empty ledger which -- contains the specified transaction outputs. @@ -368,7 +381,7 @@ genesisState pc outs = LedgerState [(TxIn genesisId idx, out) | (idx, out) <- zip [0..] outs]) (Coin 0) (Coin 0) - (EEnt Map.empty)) + Updates.emptyUpdateState) emptyDelegation emptyUPIState pc 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..6c912a5bf82 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Newpp.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Newpp.hs @@ -14,6 +14,7 @@ import EpochBoundary import LedgerState hiding (reserves) import PParams import Slot +import Updates import UTxO import Coin @@ -33,7 +34,7 @@ instance STS NEWPP where initialNewPp :: InitialRule NEWPP initialNewPp = pure - (UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) (EEnt Map.empty) + (UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) (emptyUpdateState) , emptyAccount , emptyPParams) 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..6ad4bb77a50 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Snap.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Snap.hs @@ -14,6 +14,7 @@ import Coin import EpochBoundary import LedgerState import PParams hiding (d) +import Updates import Slot import UTxO @@ -28,7 +29,7 @@ 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 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..23410fec414 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs @@ -1,4 +1,6 @@ {-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} module STS.Utxo @@ -17,10 +19,13 @@ 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 +40,7 @@ instance STS UTXO where | UnexpectedFailureUTXO [ValidationError] | UnexpectedSuccessUTXO | BadExtraEntropyUTxO + | UpdateFailure (PredicateFailure UP) deriving (Eq, Show) transitionRules = [utxoInductive] initialRules = [initialLedgerState] @@ -42,31 +48,37 @@ 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 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 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 + + -- process Update Proposals + ups' <- trans @UP $ TRC ((slot, dms), u ^. ups, txup tx) + pure $ u' & deposited %~ (+) depositChange & fees %~ (+) ((txbody ^. txfee) + decayed) - & eEntropy .~ (EEnt $ Map.union h h') + & ups .~ ups' unwrapFailureUTXO :: Validity -> PredicateFailure UTXO unwrapFailureUTXO (Invalid [e]) = unwrapFailureUTXO' e @@ -80,3 +92,6 @@ unwrapFailureUTXO' InputSetEmpty = InputSetEmptyUTxO 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/UTxO.hs b/shelley/chain-and-ledger/executable-spec/src/UTxO.hs index c193d5f47ae..a2640adfe04 100644 --- a/shelley/chain-and-ledger/executable-spec/src/UTxO.hs +++ b/shelley/chain-and-ledger/executable-spec/src/UTxO.hs @@ -52,6 +52,7 @@ module UTxO , body , witnessSet , verifyWit + , txup ) where import Crypto.Hash (Digest, SHA256, hash) @@ -71,6 +72,7 @@ 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,6 +116,7 @@ data TxBody = TxBody { _inputs :: !(Set TxIn) , _wdrls :: Wdrl , _txfee :: Coin , _ttl :: Slot + , _txUpdate:: Update , _txeent :: EEnt } deriving (Show, Eq, Ord) @@ -199,3 +202,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 index 69c34889b34..dedc2487eae 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Updates.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Updates.hs @@ -12,6 +12,8 @@ module Updates , Update(..) , newAVs , votedValue + , emptyUpdateState + , emptyUpdate ) where @@ -95,3 +97,15 @@ votedValue vs -- 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/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex index dcf584e2c35..2418213e213 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} From eaf763b64347b43543d37b1542e4d05787ecf661 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 19 Jun 2019 16:28:06 +0200 Subject: [PATCH 13/22] Simplify `LedgerState`, adapt tests `LedgerState` still contains a field for the current `Ix` in the slot. This doesn't appear in the formal spec. --- .../executable-spec/src/LedgerState.hs | 67 ++++++++----------- .../executable-spec/src/STS/Chain.hs | 2 +- .../executable-spec/src/STS/Ledger.hs | 6 +- .../executable-spec/src/STS/Ledgers.hs | 4 +- .../executable-spec/src/STS/Utxo.hs | 4 +- .../executable-spec/test/Generator.hs | 6 +- .../executable-spec/test/Mutator.hs | 2 + .../executable-spec/test/PropertyTests.hs | 9 +-- .../executable-spec/test/UnitTests.hs | 64 +++++++++--------- 9 files changed, 79 insertions(+), 85 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index b2e7acdc8f5..500c92dac33 100644 --- a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs +++ b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs @@ -74,8 +74,6 @@ module LedgerState -- lenses , utxoState , delegationState - , pcs - , current -- UTxOState , utxo , deposited @@ -270,10 +268,7 @@ emptyLedgerState = LedgerState (UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) Updates.emptyUpdateState) emptyDelegation - emptyUPIState - emptyPParams 0 - (Slot 0) emptyAccount :: AccountState emptyAccount = AccountState (Coin 0) (Coin 0) @@ -326,7 +321,7 @@ getGKeys :: NewEpochState -> Set VKeyGenesis getGKeys nes = Map.keysSet dms where NewEpochState _ _ _ _ es _ _ _ = nes EpochState _ _ ls _ = es - LedgerState _ (DPState (DState _ _ _ _ (Dms dms)) _) _ _ _ _ = ls + LedgerState _ (DPState (DState _ _ _ _ (Dms dms)) _) _ = ls data NewEpochEnv = NewEpochEnv { @@ -342,13 +337,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 @@ -383,10 +373,7 @@ genesisState pc outs = LedgerState (Coin 0) Updates.emptyUpdateState) emptyDelegation - emptyUPIState - pc 0 - (Slot 0) -- | Determine if the transaction has expired current :: TxBody -> Slot -> Validity @@ -581,12 +568,12 @@ 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 = +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) @@ -647,13 +634,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, @@ -669,10 +661,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' @@ -680,7 +672,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 @@ -691,26 +683,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) @@ -780,7 +771,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 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 22d11e7d60e..f2cbbbe6bb0 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs @@ -50,7 +50,7 @@ chainTransition = do let NewEpochState _ eta0 _ bCur es _ _pd osched = nes' let EpochState _ _ ls pp = es - let LedgerState _ (DPState (DState _ _ _ _ _dms) (PState _ _ _ cs)) _ _ _ _ = ls + 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) 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..462ed404c3b 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Ledger.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ledger.hs @@ -28,7 +28,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,7 +38,7 @@ instance STS LEDGER where initialLedgerStateLEDGER :: InitialRule LEDGER initialLedgerStateLEDGER = do - IRC (pp, slot, ix) <- judgmentContext + 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) @@ -46,7 +46,7 @@ initialLedgerStateLEDGER = do ledgerTransition :: TransitionRule LEDGER ledgerTransition = do - TRC ((pp, slot, ix), (u, d), txwits) <- judgmentContext + TRC ((slot, ix, pp), (u, d), txwits) <- judgmentContext utxo' <- trans @UTXOW $ TRC (( slot , pp, d ^. dstate . stKeys 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..b4b852fee90 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Ledgers.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ledgers.hs @@ -37,11 +37,11 @@ ledgersTransition = do (u'', dw'') <- foldM (\(u', dw') (ix, tx) -> - trans @LEDGER $ TRC ((pp, slot, ix), (u', dw'), tx)) + trans @LEDGER $ TRC ((slot, ix, pp), (u', dw'), tx)) (u, dw) $ zip [0 ..] txwits pure $ - LedgerState u'' dw'' (upiState ls) (_pcs ls) (_txSlotIx ls) (_currentSlot ls) + LedgerState u'' dw'' (_txSlotIx ls) instance Embed LEDGER LEDGERS where wrapFailed = LedgerFailure 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 23410fec414..112595bfdb6 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs @@ -8,11 +8,9 @@ module STS.Utxo ) where 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 @@ -56,7 +54,7 @@ utxoInductive = do 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 diff --git a/shelley/chain-and-ledger/executable-spec/test/Generator.hs b/shelley/chain-and-ledger/executable-spec/test/Generator.hs index 11e05eade6e..d0354793866 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,6 +150,7 @@ genTx keyList (UTxO m) cslot = do Map.empty -- TODO generate witdrawals txfee' (cslot + (Slot txttl)) + emptyUpdate (EEnt Map.empty) let !txwit = makeWitness txbody selectedKeyPair pure (txfee', Tx txbody $ Set.fromList [txwit]) @@ -166,7 +168,7 @@ genLedgerStateTx keyList (Slot slot) sourceState = do 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 @@ -287,7 +289,7 @@ genLedgerStateTx' keyList sourceState = do 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..0babba65b26 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,6 +90,7 @@ mutateTxBody tx = do (_wdrls tx) (_txfee tx) (_ttl tx) + emptyUpdate (_txeent tx) -- | Mutator for a list of '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..536a3642a83 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 @@ -231,7 +232,7 @@ propCheckMinimalWitnessSet = property $ do 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 @@ -250,7 +251,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 +267,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..a1012f29cb3 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,7 +70,7 @@ stakePoolKey1 :: KeyPair stakePoolKey1 = keyPair (Owner 5) ledgerState :: [Tx] -> Either [ValidationError] LedgerState -ledgerState = foldM (\l t -> asStateTransition (Slot 0) l t dms) genesis +ledgerState = foldM (\l t -> asStateTransition (Slot 0) testPCs l t dms) genesis where dms = _dms $ _dstate $ _delegationState genesis @@ -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,20 @@ testValidWithdrawal = bobWithdrawal (Coin 1000) (Slot 0) + emptyUpdate (EEnt Map.empty) 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,6 +166,7 @@ testInvalidWintess = Map.empty (Coin 1000) (Slot 1) + emptyUpdate (EEnt Map.empty) tx' = tx & ttl .~ Slot 2 wits = makeWitnesses tx' [alicePay] @@ -196,6 +184,7 @@ testTooManyWintesses = Map.empty (Coin 1000) (Slot 1) + emptyUpdate (EEnt Map.empty) wits = makeWitnesses tx [alicePay, bobStake] in ledgerState [Tx tx wits] @?= Left [UnneededWitnesses] @@ -212,9 +201,10 @@ testWithdrawalNoWit = bobWithdrawal (Coin 1000) (Slot 0) + emptyUpdate (EEnt Map.empty) 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 +218,10 @@ testWithdrawalWrongAmt = (Map.singleton (mkRwdAcnt bobStake) (Coin 11)) (Coin 1000) (Slot 0) + emptyUpdate (EEnt Map.empty) 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,6 +237,7 @@ aliceGivesBobLovelace txin coin fee txdeps txrefs cs s signers = Tx txbody wits Map.empty fee s + emptyUpdate (EEnt Map.empty) wits = makeWitnesses txbody signers @@ -266,7 +258,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 +282,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,6 +293,7 @@ tx3Body = TxBody Map.empty (Coin 1200) (Slot 100) + emptyUpdate (EEnt Map.empty) tx3 :: Tx @@ -315,7 +308,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,6 +364,7 @@ tx4Body = TxBody Map.empty (Coin 1000) (Slot 100) + emptyUpdate (EEnt Map.empty) tx4 :: Tx @@ -384,7 +378,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 +388,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,6 +398,7 @@ tx5Body e = TxBody Map.empty (Coin 1000) (Slot 100) + emptyUpdate (EEnt Map.empty) tx5 :: Epoch -> Tx @@ -456,6 +451,7 @@ testWitnessNotIncluded = Map.empty (Coin 596) (Slot 100) + emptyUpdate (EEnt Map.empty) tx = Tx txbody Set.empty in ledgerState [tx] @?= Left [MissingWitnesses] @@ -470,6 +466,7 @@ testSpendNotOwnedUTxO = Map.empty (Coin 768) (Slot 100) + emptyUpdate (EEnt Map.empty) aliceWit = makeWitness txbody alicePay tx = Tx txbody (Set.fromList [aliceWit]) @@ -485,6 +482,7 @@ testWitnessWrongUTxO = Map.empty (Coin 770) (Slot 100) + emptyUpdate (EEnt Map.empty) tx2body = TxBody (Set.fromList [TxIn genesisId 1]) @@ -493,6 +491,7 @@ testWitnessWrongUTxO = Map.empty (Coin 770) (Slot 101) + emptyUpdate (EEnt Map.empty) aliceWit = makeWitness tx2body alicePay tx = Tx txbody (Set.fromList [aliceWit]) @@ -511,10 +510,11 @@ testEmptyInputSet = aliceWithdrawal (Coin 1000) (Slot 0) + emptyUpdate (EEnt Map.empty) 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 +538,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 From 751eed4c95711d0b1583439f5fa016ca231c3b2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 19 Jun 2019 16:47:58 +0200 Subject: [PATCH 14/22] Remove `EEnt` extra entropy type --- .../executable-spec/src/BaseTypes.hs | 5 ----- .../executable-spec/src/LedgerState.hs | 10 ++-------- .../chain-and-ledger/executable-spec/src/UTxO.hs | 2 -- .../executable-spec/test/Generator.hs | 1 - .../executable-spec/test/UnitTests.hs | 14 -------------- 5 files changed, 2 insertions(+), 30 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs index 0c3ee35a214..f5818483fd7 100644 --- a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs +++ b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs @@ -13,7 +13,6 @@ module BaseTypes , mkNonce , seedOp , neutralSeed - , EEnt(..) ) where import qualified Data.Map.Strict as Map @@ -75,7 +74,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/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index 500c92dac33..9ad0451020f 100644 --- a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs +++ b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs @@ -359,8 +359,7 @@ genesisId = Map.empty (Coin 0) (Slot 0) - Updates.emptyUpdate - (EEnt Map.empty)) + Updates.emptyUpdate) -- |Creates the ledger state for an empty ledger which -- contains the specified transaction outputs. @@ -498,8 +497,7 @@ witsNeeded utxo' tx (Dms d) = inputAuthors `Set.union` wdrlAuthors `Set.union` certAuthors `Set.union` - owners `Set.union` - genEEntropy + owners where inputAuthors = Set.foldr insertHK Set.empty (tx ^. inputs) insertHK txin hkeys = @@ -511,10 +509,6 @@ witsNeeded utxo' tx (Dms d) = owners = foldl Set.union Set.empty [pool ^. poolOwners | RegPool pool <- tx ^. certs] certAuthors = Set.fromList (fmap getCertHK (tx ^. certs)) getCertHK cert = hashKey $ getRequiredSigningKey cert - EEnt eent = _txeent tx - genEEntropy = Set.fromList $ - Map.elems $ Map.map hashKey $ Map.restrictKeys d (Map.keysSet eent) - -- |Given a ledger state, determine if the UTxO witnesses in a given -- transaction are correct. diff --git a/shelley/chain-and-ledger/executable-spec/src/UTxO.hs b/shelley/chain-and-ledger/executable-spec/src/UTxO.hs index a2640adfe04..06c5a72d83f 100644 --- a/shelley/chain-and-ledger/executable-spec/src/UTxO.hs +++ b/shelley/chain-and-ledger/executable-spec/src/UTxO.hs @@ -47,7 +47,6 @@ module UTxO , wdrls , txfee , ttl - , txeent -- Tx , body , witnessSet @@ -117,7 +116,6 @@ data TxBody = TxBody { _inputs :: !(Set TxIn) , _txfee :: Coin , _ttl :: Slot , _txUpdate:: Update - , _txeent :: EEnt } deriving (Show, Eq, Ord) makeLenses ''TxBody diff --git a/shelley/chain-and-ledger/executable-spec/test/Generator.hs b/shelley/chain-and-ledger/executable-spec/test/Generator.hs index d0354793866..4cd01c2a1fd 100644 --- a/shelley/chain-and-ledger/executable-spec/test/Generator.hs +++ b/shelley/chain-and-ledger/executable-spec/test/Generator.hs @@ -151,7 +151,6 @@ genTx keyList (UTxO m) cslot = do txfee' (cslot + (Slot txttl)) emptyUpdate - (EEnt Map.empty) let !txwit = makeWitness txbody selectedKeyPair pure (txfee', Tx txbody $ Set.fromList [txwit]) where utxoInputs = Map.keys m diff --git a/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs b/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs index a1012f29cb3..1b70e94dfd6 100644 --- a/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs +++ b/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs @@ -141,7 +141,6 @@ testValidWithdrawal = (Coin 1000) (Slot 0) emptyUpdate - (EEnt Map.empty) wits = makeWitnesses tx [alicePay, bobStake] utxo' = Map.fromList [ (TxIn genesisId 1, TxOut bobAddr (Coin 1000)) @@ -167,7 +166,6 @@ testInvalidWintess = (Coin 1000) (Slot 1) emptyUpdate - (EEnt Map.empty) tx' = tx & ttl .~ Slot 2 wits = makeWitnesses tx' [alicePay] in ledgerState [Tx tx wits] @?= Left [InvalidWitness] @@ -185,7 +183,6 @@ testTooManyWintesses = (Coin 1000) (Slot 1) emptyUpdate - (EEnt Map.empty) wits = makeWitnesses tx [alicePay, bobStake] in ledgerState [Tx tx wits] @?= Left [UnneededWitnesses] @@ -202,7 +199,6 @@ testWithdrawalNoWit = (Coin 1000) (Slot 0) emptyUpdate - (EEnt Map.empty) wits = Set.singleton $ makeWitness tx alicePay ls = asStateTransition (Slot 0) testPCs genesisWithReward (Tx tx wits) (Dms Map.empty) in ls @?= Left [MissingWitnesses] @@ -219,7 +215,6 @@ testWithdrawalWrongAmt = (Coin 1000) (Slot 0) emptyUpdate - (EEnt Map.empty) wits = makeWitnesses tx [alicePay, bobStake] ls = asStateTransition (Slot 0) testPCs genesisWithReward (Tx tx wits) (Dms Map.empty) in ls @?= Left [IncorrectRewards] @@ -238,7 +233,6 @@ aliceGivesBobLovelace txin coin fee txdeps txrefs cs s signers = Tx txbody wits fee s emptyUpdate - (EEnt Map.empty) wits = makeWitnesses txbody signers tx1 :: Tx @@ -294,7 +288,6 @@ tx3Body = TxBody (Coin 1200) (Slot 100) emptyUpdate - (EEnt Map.empty) tx3 :: Tx tx3 = Tx tx3Body (makeWitnesses tx3Body keys) @@ -365,7 +358,6 @@ tx4Body = TxBody (Coin 1000) (Slot 100) emptyUpdate - (EEnt Map.empty) tx4 :: Tx tx4 = Tx tx4Body (makeWitnesses tx4Body [alicePay, stakePoolKey1]) @@ -399,7 +391,6 @@ tx5Body e = TxBody (Coin 1000) (Slot 100) emptyUpdate - (EEnt Map.empty) tx5 :: Epoch -> Tx tx5 e = Tx (tx5Body e) (makeWitnesses (tx5Body e) [alicePay, stakePoolKey1]) @@ -452,7 +443,6 @@ testWitnessNotIncluded = (Coin 596) (Slot 100) emptyUpdate - (EEnt Map.empty) tx = Tx txbody Set.empty in ledgerState [tx] @?= Left [MissingWitnesses] @@ -467,7 +457,6 @@ testSpendNotOwnedUTxO = (Coin 768) (Slot 100) emptyUpdate - (EEnt Map.empty) aliceWit = makeWitness txbody alicePay tx = Tx txbody (Set.fromList [aliceWit]) in ledgerState [tx] @?= Left [MissingWitnesses, UnneededWitnesses] @@ -483,7 +472,6 @@ testWitnessWrongUTxO = (Coin 770) (Slot 100) emptyUpdate - (EEnt Map.empty) tx2body = TxBody (Set.fromList [TxIn genesisId 1]) [ TxOut aliceAddr (Coin 230)] @@ -492,7 +480,6 @@ testWitnessWrongUTxO = (Coin 770) (Slot 101) emptyUpdate - (EEnt Map.empty) aliceWit = makeWitness tx2body alicePay tx = Tx txbody (Set.fromList [aliceWit]) in ledgerState [tx] @?= Left [ InvalidWitness @@ -511,7 +498,6 @@ testEmptyInputSet = (Coin 1000) (Slot 0) emptyUpdate - (EEnt Map.empty) wits = makeWitnesses tx [aliceStake] genesisWithReward' = changeReward genesis (mkRwdAcnt aliceStake) (Coin 2000) ls = asStateTransition (Slot 0) testPCs genesisWithReward' (Tx tx wits) (Dms Map.empty) From d6f7ca0218a180b9b390dfaa3ea4bd4534fffc12 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 19 Jun 2019 16:59:38 +0200 Subject: [PATCH 15/22] Fixes for compilation and layout --- .../executable-spec/src/BaseTypes.hs | 2 - .../executable-spec/src/BlockChain.hs | 2 +- .../executable-spec/src/LedgerState.hs | 4 +- .../executable-spec/src/STS/Avup.hs | 10 +-- .../executable-spec/src/STS/Bbody.hs | 14 ++--- .../executable-spec/src/STS/Bhead.hs | 22 +++---- .../executable-spec/src/STS/Chain.hs | 18 ++---- .../executable-spec/src/STS/Deleg.hs | 3 +- .../executable-spec/src/STS/Delegs.hs | 14 +++-- .../executable-spec/src/STS/Delpl.hs | 17 ++--- .../executable-spec/src/STS/Epoch.hs | 31 +++++----- .../executable-spec/src/STS/Ledger.hs | 19 +++--- .../executable-spec/src/STS/Ledgers.hs | 17 ++--- .../executable-spec/src/STS/NewEpoch.hs | 49 ++++++++------- .../executable-spec/src/STS/Newpp.hs | 62 +++++++++++-------- .../executable-spec/src/STS/Ocert.hs | 9 +-- .../executable-spec/src/STS/Overlay.hs | 3 +- .../executable-spec/src/STS/Pool.hs | 9 +-- .../executable-spec/src/STS/PoolReap.hs | 59 +++++++++++------- .../executable-spec/src/STS/Ppup.hs | 8 +-- .../executable-spec/src/STS/Rupd.hs | 7 ++- .../executable-spec/src/STS/Snap.hs | 40 ++++++++---- .../executable-spec/src/STS/Up.hs | 4 +- .../executable-spec/src/STS/Updn.hs | 3 +- .../executable-spec/src/STS/Utxo.hs | 33 ++++++---- .../executable-spec/src/STS/Utxow.hs | 3 +- .../executable-spec/src/UTxO.hs | 2 +- .../executable-spec/src/Updates.hs | 39 ++++++------ .../executable-spec/test/Generator.hs | 26 ++++---- .../executable-spec/test/Mutator.hs | 1 - .../executable-spec/test/UnitTests.hs | 4 +- 31 files changed, 288 insertions(+), 246 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs index f5818483fd7..3ccedae1b66 100644 --- a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs +++ b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs @@ -15,10 +15,8 @@ module BaseTypes , neutralSeed ) where -import qualified Data.Map.Strict as Map import qualified Data.Fixed as FP -import qualified Keys as Keys data E34 diff --git a/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs b/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs index f6e4f5bf3a6..cedb9426cdd 100644 --- a/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs @@ -148,7 +148,7 @@ instance VrfProof UnitInterval where where r = intervalValue u vrfChecks :: Seed -> PoolDistr -> UnitInterval -> BHBody -> Bool -vrfChecks eta0 pd'@(PoolDistr pd) f bhb = +vrfChecks eta0 (PoolDistr pd) f bhb = let sigma' = Map.lookup hk pd in case sigma' of Nothing -> False diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index 9ad0451020f..78b6e859585 100644 --- a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs +++ b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs @@ -364,7 +364,7 @@ genesisId = -- |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]) @@ -493,7 +493,7 @@ correctWithdrawals accs withdrawals = -- 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 _ = inputAuthors `Set.union` wdrlAuthors `Set.union` certAuthors `Set.union` 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 73ee3337c72..ea4969083f0 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Avup.hs @@ -33,16 +33,16 @@ instance STS AVUP where avupTransition :: TransitionRule AVUP avupTransition = do - TRC ((slot, Dms dms), src@(AVUpdate aupS, favs, avs), AVUpdate aup) <- + 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 + 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 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 @@ -50,6 +50,6 @@ avupTransition = do Just fav' -> pure ( AVUpdate Map.empty - , Map.insert (slot +* slotsPrior) fav' favs' + , 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..40644509f68 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs @@ -5,10 +5,11 @@ 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 Data.Maybe ( fromMaybe ) import BlockChain import EpochBoundary @@ -35,14 +36,13 @@ instance STS BBODY where bbodyTransition :: TransitionRule BBODY bbodyTransition = do - TRC (pp, (ls, BlocksMade b), (Block (BHeader bhb _) txs)) <- - judgmentContext - let vk = bheaderVk bhb + 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) + let n = fromMaybe 0 (Map.lookup hk b) ls' <- trans @LEDGERS $ TRC ((bheaderSlot bhb, pp), ls, txs) pure (ls', BlocksMade $ Map.insert hk (n + 1) b) 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 55e75be4cac..1dc2c6ae955 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Bhead.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Bhead.hs @@ -5,23 +5,18 @@ module STS.Bhead ( BHEAD - ) where + ) +where -import qualified Data.Map.Strict as Map -import qualified Data.Set as Set -import Crypto.Hash (hash) -import qualified Data.ByteString.Char8 as BS +import qualified Data.Set as Set import BaseTypes import BlockChain import Keys import LedgerState -import OCert import PParams import Slot -import Delegation.Certificates (StakePools (..)) - import STS.NewEpoch import STS.Rupd @@ -43,19 +38,18 @@ instance STS BHEAD where bheadTransition :: TransitionRule BHEAD bheadTransition = do - TRC ( (etaC, gkeys) - , nes@(NewEpochState _ _ bprev _ es ru _ _) - , bh@(BHeader bhb _)) <- judgmentContext - let slot = bheaderSlot bhb + TRC ((etaC, gkeys), nes@(NewEpochState _ _ bprev _ es ru _ _), bh@(BHeader bhb _)) <- + judgmentContext + let slot = bheaderSlot bhb let EpochState _ _ _ pp = es fromIntegral (bHeaderSize bh) > _maxBHSize pp ?! HeaderSizeTooLargeBHEAD fromIntegral (hBbsize bhb) > _maxBBSize pp ?! BlockSizeTooLargeBHEAD nes' <- trans @NEWEPOCH - $ TRC((NewEpochEnv etaC slot gkeys), nes, epochFromSlot slot) + $ TRC ((NewEpochEnv etaC slot gkeys), nes, epochFromSlot slot) - ru' <- trans @RUPD $ TRC((bprev, es), ru, slot) + ru' <- trans @RUPD $ TRC ((bprev, es), ru, slot) let nes'' = nes' { nesRu = ru' } pure nes'' 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 f2cbbbe6bb0..25c07e5f93a 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs @@ -5,19 +5,14 @@ module STS.Chain ( CHAIN - ) where - -import qualified Data.Map.Strict as Map + ) +where import BaseTypes import BlockChain -import EpochBoundary import LedgerState -import PParams import Slot -import Delegation.Certificates - import Control.State.Transition import STS.Bbody @@ -43,17 +38,16 @@ instance STS CHAIN where chainTransition :: TransitionRule CHAIN chainTransition = do - TRC (sNow, (nes, etaV, etaC, h, sL), block@(Block bh _)) <- judgmentContext + TRC (sNow, (nes, etaV, etaC, h, sL), (Block bh _)) <- judgmentContext let gkeys = getGKeys nes - nes' <- trans @BHEAD $ TRC((etaC, gkeys), nes, bh) + nes' <- trans @BHEAD $ TRC ((etaC, gkeys), nes, bh) - let NewEpochState _ eta0 _ bCur es _ _pd osched = nes' + let NewEpochState _ eta0 _ _ 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) + _ <- trans @PRTCL $ TRC(((pp, osched, eta0, _pd, _dms), sNow), (cs, h, sL, etaV, etaC), bh) pure undefined 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 462ed404c3b..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 @@ -39,7 +40,7 @@ instance STS LEDGER where initialLedgerStateLEDGER :: InitialRule LEDGER initialLedgerStateLEDGER = do IRC (slot, ix, pp) <- judgmentContext - utxo' <- trans @UTXOW + 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) @@ -47,11 +48,11 @@ initialLedgerStateLEDGER = do ledgerTransition :: TransitionRule LEDGER ledgerTransition = do 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) + 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 b4b852fee90..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 ((slot, ix, pp), (u', dw'), tx)) - (u, dw) $ - zip [0 ..] txwits - pure $ - LedgerState u'' dw'' (_txSlotIx 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 6c912a5bf82..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,13 +3,13 @@ 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 @@ -32,11 +32,11 @@ instance STS NEWPP where transitionRules = [newPpTransition] initialNewPp :: InitialRule NEWPP -initialNewPp = - pure - (UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) (emptyUpdateState) - , emptyAccount - , emptyPParams) +initialNewPp = pure + ( UTxOState (UTxO Map.empty) (Coin 0) (Coin 0) (emptyUpdateState) + , emptyAccount + , emptyPParams + ) newPpTransition :: TransitionRule NEWPP newPpTransition = do @@ -44,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 index d3d28709721..f2f646f434f 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs @@ -45,7 +45,8 @@ instance STS OVERLAY where overlayTransition :: TransitionRule OVERLAY overlayTransition = do - TRC ((pp, osched, eta0, pd, Dms dms), cs, bh@(BHeader bhb _)) <- judgmentContext + 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 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 index 08981a633c3..596e67371da 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs @@ -10,13 +10,9 @@ where import qualified Data.Map.Strict as Map import qualified Data.Set as Set -import Numeric.Natural ( Natural ) -import BaseTypes import BlockChain -import Delegation.Certificates import Keys -import PParams import Slot import Updates @@ -37,12 +33,12 @@ instance STS PPUP where ppupTransition :: TransitionRule PPUP ppupTransition = do - TRC ((s, Dms dms), pupS@(PPUpdate pupS'), pup@(PPUpdate pup')) <- + 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) + (not $ Map.keysSet pup' `Set.isSubsetOf` Map.keysSet _dms) ?! NonGenesisUpdatePPUP let Epoch slotEpoch = epochFromSlot (Slot 1) s 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 6ad4bb77a50..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,13 +3,17 @@ 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 @@ -36,13 +40,23 @@ 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 index feeb264ae35..3f3b3b1ba27 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs @@ -35,10 +35,10 @@ instance STS UP where upTransition :: TransitionRule UP upTransition = do - TRC (env, (pupS, aupS, favs, avs), Update pup aup) <- judgmentContext + 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) + (aup', favs', avs') <- trans @AVUP $ TRC (env, (aupS, favs, avs), _aup) pure (pup', aup', favs', avs') 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 112595bfdb6..0c1e807e300 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs @@ -5,11 +5,16 @@ module STS.Utxo ( UTXO - ) where + ) +where -import qualified Data.Map.Strict as Map +import qualified Data.Map.Strict as Map -import Lens.Micro ((%~), (&), (^.), (.~)) +import Lens.Micro ( (%~) + , (&) + , (^.) + , (.~) + ) import Coin import Delegation.Certificates @@ -50,11 +55,11 @@ initialLedgerState = do utxoInductive :: TransitionRule UTXO utxoInductive = do - TRC ((slot, pp, stakeKeys, stakePools, dms), u, tx) <- judgmentContext + TRC ((_slot, pp, stakeKeys, stakePools, _dms), u, tx) <- judgmentContext let txbody = _body tx validInputs txbody u == Valid ?! BadInputsUTxO - _ttl txbody >= slot ?! ExpiredUTxO (_ttl txbody) slot + _ttl txbody >= _slot ?! ExpiredUTxO (_ttl txbody) _slot validNoReplay txbody == Valid ?! InputSetEmptyUTxO let validateFee = validFee pp txbody @@ -64,19 +69,23 @@ utxoInductive = do 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 -- process Update Proposals - ups' <- trans @UP $ TRC ((slot, dms), u ^. ups, txup tx) + ups' <- trans @UP $ TRC ((_slot, _dms), u ^. ups, txup tx) - pure $ - u' & deposited %~ (+) depositChange - & fees %~ (+) ((txbody ^. txfee) + decayed) - & ups .~ ups' + pure + $ u' + & deposited + %~ (+) depositChange + & fees + %~ (+) ((txbody ^. txfee) + decayed) + & ups + .~ ups' unwrapFailureUTXO :: Validity -> PredicateFailure UTXO unwrapFailureUTXO (Invalid [e]) = unwrapFailureUTXO' e @@ -87,7 +96,7 @@ 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] 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..946acfb13f7 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,8 @@ module STS.Utxow ( UTXOW - ) where + ) +where import Delegation.Certificates import Keys diff --git a/shelley/chain-and-ledger/executable-spec/src/UTxO.hs b/shelley/chain-and-ledger/executable-spec/src/UTxO.hs index 06c5a72d83f..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 , (<|) @@ -66,7 +67,6 @@ import Numeric.Natural (Natural) import Lens.Micro ((^.)) import Lens.Micro.TH (makeLenses) -import BaseTypes import Coin (Coin (..)) import Keys import PParams (PParams(..)) diff --git a/shelley/chain-and-ledger/executable-spec/src/Updates.hs b/shelley/chain-and-ledger/executable-spec/src/Updates.hs index dedc2487eae..fe7fed972c8 100644 --- a/shelley/chain-and-ledger/executable-spec/src/Updates.hs +++ b/shelley/chain-and-ledger/executable-spec/src/Updates.hs @@ -18,7 +18,8 @@ module Updates where import qualified Data.Map.Strict as Map -import qualified Data.List as List (group) +import qualified Data.List as List + ( group ) import BaseTypes import Coin @@ -83,29 +84,27 @@ 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 +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 +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) + 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 4cd01c2a1fd..a65f0ee6fd4 100644 --- a/shelley/chain-and-ledger/executable-spec/test/Generator.hs +++ b/shelley/chain-and-ledger/executable-spec/test/Generator.hs @@ -162,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') defPCs 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 @@ -205,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. @@ -255,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) @@ -282,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) defPCs (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 0babba65b26..b41e0fa490d 100644 --- a/shelley/chain-and-ledger/executable-spec/test/Mutator.hs +++ b/shelley/chain-and-ledger/executable-spec/test/Mutator.hs @@ -91,7 +91,6 @@ mutateTxBody tx = do (_txfee tx) (_ttl tx) emptyUpdate - (_txeent tx) -- | Mutator for a list of 'TxIn'. mutateInputs :: [TxIn] -> Gen [TxIn] diff --git a/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs b/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs index 1b70e94dfd6..d8f8cb0ec56 100644 --- a/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs +++ b/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs @@ -70,8 +70,8 @@ stakePoolKey1 :: KeyPair stakePoolKey1 = keyPair (Owner 5) ledgerState :: [Tx] -> Either [ValidationError] LedgerState -ledgerState = foldM (\l t -> asStateTransition (Slot 0) testPCs 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 :: From c7f18b90bf18d7edabe3082567c1a3d050b529ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 21 Jun 2019 13:09:51 +0200 Subject: [PATCH 16/22] Adapt `BBODY` rule --- .../executable-spec/src/BlockChain.hs | 66 ++++++++++++------- .../executable-spec/src/STS/Bbody.hs | 24 +++---- 2 files changed, 54 insertions(+), 36 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs b/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs index cedb9426cdd..3c0eb8ba791 100644 --- a/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/BlockChain.hs @@ -22,23 +22,29 @@ module BlockChain , seedL , bvkcold , vrfChecks - ) where - -import Crypto.Hash (Digest, SHA256, hash) -import qualified Data.ByteArray as BA -import qualified Data.ByteString.Char8 as BS -import Numeric.Natural (Natural) + , 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 qualified Data.Map.Strict as Map import BaseTypes import Delegation.Certificates -import qualified Keys as Keys +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 ((***)) +import NonIntegral ( (***) ) -- |The hash of a Block Header newtype HashHeader = @@ -149,20 +155,24 @@ instance VrfProof UnitInterval where 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 -> + 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') + && 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 @@ -175,3 +185,11 @@ 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/STS/Bbody.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs index 40644509f68..8cb1b3ef5cd 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs @@ -9,13 +9,14 @@ module STS.Bbody where import qualified Data.Map.Strict as Map -import Data.Maybe ( fromMaybe ) +import qualified Data.Set as Set import BlockChain import EpochBoundary import Keys import LedgerState import PParams +import Slot import Control.State.Transition @@ -26,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)] @@ -36,15 +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 From 626fa1177d34a2f9f7483f35bf4eb9678ffc4dca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 21 Jun 2019 14:57:56 +0200 Subject: [PATCH 17/22] Adapt `CHAIN` STS rule --- .../executable-spec/src/LedgerState.hs | 15 +++++++++++++++ .../executable-spec/src/STS/Chain.hs | 19 ++++++++++++++----- .../chain-and-ledger/formal-spec/chain.tex | 3 ++- .../chain-and-ledger/formal-spec/epoch.tex | 2 ++ 4 files changed, 33 insertions(+), 6 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index 78b6e859585..c2fa08b3c9f 100644 --- a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs +++ b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs @@ -107,6 +107,8 @@ module LedgerState , NewEpochEnv(..) , overlaySchedule , getGKeys + , setIssueNumbers + , updateNES ) where import Control.Monad (foldM) @@ -947,3 +949,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/Chain.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs index 25c07e5f93a..52ea28b8387 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs @@ -8,6 +8,8 @@ module STS.Chain ) where +import qualified Data.Map.Strict as Map + import BaseTypes import BlockChain import LedgerState @@ -38,18 +40,25 @@ instance STS CHAIN where chainTransition :: TransitionRule CHAIN chainTransition = do - TRC (sNow, (nes, etaV, etaC, h, sL), (Block bh _)) <- judgmentContext + TRC (sNow, (nes, etaV, etaC, h, sL), block@(Block bh _)) <- judgmentContext let gkeys = getGKeys nes nes' <- trans @BHEAD $ TRC ((etaC, gkeys), nes, bh) - let NewEpochState _ eta0 _ _ es _ _pd osched = nes' - let EpochState _ _ ls pp = es + let NewEpochState _ eta0 _ bcur es _ _pd osched = nes' + let EpochState _ _ ls pp = es let LedgerState _ (DPState (DState _ _ _ _ _dms) (PState _ _ _ cs)) _ = ls - _ <- trans @PRTCL $ TRC(((pp, osched, eta0, _pd, _dms), sNow), (cs, h, sL, etaV, etaC), bh) + (cs', h', sL', etaV', etaC') <- trans @PRTCL + $ TRC (((pp, osched, eta0, _pd, _dms), sNow), (cs, h, sL, etaV, etaC), bh) + + let ls' = setIssueNumbers ls cs' + (ls'', bcur') <- trans @BBODY + $ TRC ((Map.keysSet osched, pp), (ls', bcur), block) + + let nes'' = updateNES nes' bcur' ls'' - pure undefined + pure (nes'', etaV', etaC', h', sL') instance Embed BBODY CHAIN where wrapFailed = BbodyFailure diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index 67413239466..bc9f8c1a7f9 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -1383,7 +1383,8 @@ \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} \\ % TODO should + % this be cs' ? { {\left(\begin{array}{c} \dom{osched} \\ diff --git a/shelley/chain-and-ledger/formal-spec/epoch.tex b/shelley/chain-and-ledger/formal-spec/epoch.tex index d1d0645cadd..266fbdd3d70 100644 --- a/shelley/chain-and-ledger/formal-spec/epoch.tex +++ b/shelley/chain-and-ledger/formal-spec/epoch.tex @@ -901,6 +901,8 @@ \subsection{Complete Epoch Boundary Transition} \\~\\~\\ \var{(\wcard,~\wcard,~\wcard,~(\var{pup},~\wcard,~\wcard,~\wcard))}\leteq\var{utxoSt'}\\ \var{pp_{new}}\leteq\fun{votedValue_{PParams}}~\var{pup}\\ + % TODO: I think this isn't the right type, `pup` is PPUpdate which is not + % a complete set of `PParams`. { \begin{array}{l} \var{pp_{new}}\\ From afe89c43d761c78d8d93d82955b6d1a4f07b9c54 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Sat, 22 Jun 2019 12:01:19 +0200 Subject: [PATCH 18/22] Adapt `witsNeeded` in `UTXOW`, remove `UneededWitness` failure We allow redundant witnesses to support mutli-sig which might require more than one valid signature for transactions. --- .../executable-spec/src/LedgerState.hs | 38 +++++++++---------- .../executable-spec/src/STS/Utxow.hs | 12 +++--- shelley/chain-and-ledger/formal-spec/utxo.tex | 4 +- 3 files changed, 28 insertions(+), 26 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index c2fa08b3c9f..33802d46813 100644 --- a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs +++ b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs @@ -69,8 +69,7 @@ module LedgerState , validStakeDelegation , preserveBalance , verifiedWits - , enoughWits - , noUnneededWits + , witsNeeded -- lenses , utxoState , delegationState @@ -494,23 +493,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 _ = +witsNeeded :: UTxO -> Tx -> Dms -> Set HashKey +witsNeeded utxo' tx@(Tx txbody _) _dms = inputAuthors `Set.union` wdrlAuthors `Set.union` certAuthors `Set.union` + 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 + updateKeys = propWits (txup tx) _dms -- |Given a ledger state, determine if the UTxO witnesses in a given -- transaction are correct. @@ -526,22 +528,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 @@ -562,7 +555,14 @@ 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) + +-- | 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 = 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 946acfb13f7..0b9c9c6fdc6 100644 --- a/shelley/chain-and-ledger/executable-spec/src/STS/Utxow.hs +++ b/shelley/chain-and-ledger/executable-spec/src/STS/Utxow.hs @@ -8,6 +8,8 @@ module STS.Utxow ) where +import qualified Data.Set as Set + import Delegation.Certificates import Keys import LedgerState hiding (dms) @@ -27,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] @@ -40,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/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex index 2418213e213..ad8c776512b 100644 --- a/shelley/chain-and-ledger/formal-spec/utxo.tex +++ b/shelley/chain-and-ledger/formal-spec/utxo.tex @@ -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 From d59124c00c4cc86a231eba020afee799d2b0cfd3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Sat, 22 Jun 2019 12:56:37 +0200 Subject: [PATCH 19/22] Remove `UnneededWitnesses` from expected results in unit test - remove unit tests that tests exactly that situation - remove `UnneededWitnesses` from expected failures --- .../executable-spec/test/UnitTests.hs | 27 +++---------------- 1 file changed, 3 insertions(+), 24 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs b/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs index d8f8cb0ec56..116d50a6300 100644 --- a/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs +++ b/shelley/chain-and-ledger/executable-spec/test/UnitTests.hs @@ -170,23 +170,6 @@ testInvalidWintess = 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) - emptyUpdate - wits = makeWitnesses tx [alicePay, bobStake] - in ledgerState [Tx tx wits] @?= Left [UnneededWitnesses] - - testWithdrawalNoWit :: Assertion testWithdrawalNoWit = let @@ -427,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 = @@ -459,7 +440,7 @@ testSpendNotOwnedUTxO = 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 = @@ -483,8 +464,7 @@ testWitnessWrongUTxO = aliceWit = makeWitness tx2body alicePay tx = Tx txbody (Set.fromList [aliceWit]) in ledgerState [tx] @?= Left [ InvalidWitness - , MissingWitnesses - , UnneededWitnesses ] + , MissingWitnesses] testEmptyInputSet :: Assertion testEmptyInputSet = @@ -537,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 ] From 5b99f544ea29e8e8002e1daed3601f6fecc3d02e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Sat, 22 Jun 2019 13:39:12 +0200 Subject: [PATCH 20/22] Adapt property-based test for redundant witnesses --- .../executable-spec/src/LedgerState.hs | 2 -- .../executable-spec/test/PropertyTests.hs | 21 +++++++++---------- 2 files changed, 10 insertions(+), 13 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index 33802d46813..348e4a7f158 100644 --- a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs +++ b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs @@ -169,8 +169,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. diff --git a/shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs b/shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs index 536a3642a83..99a431bfec2 100644 --- a/shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs +++ b/shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs @@ -170,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 @@ -219,13 +219,13 @@ 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 @@ -236,10 +236,9 @@ propCheckMinimalWitnessSet = property $ do 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. From 5b08f745a76ef2346896dc3deb9c07a22f397e32 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Mon, 24 Jun 2019 11:03:27 +0200 Subject: [PATCH 21/22] Remove `UPIState` from executable specification --- .../executable-spec/src/LedgerState.hs | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs index 348e4a7f158..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 @@ -140,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)] @@ -295,14 +292,6 @@ data UTxOState = , 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 { From 6925664aec59e189a065c1745bdc86273a1ef603 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Mon, 24 Jun 2019 18:18:19 +0200 Subject: [PATCH 22/22] Fix `TODOs` in the formal spec --- shelley/chain-and-ledger/formal-spec/chain.tex | 9 ++++----- shelley/chain-and-ledger/formal-spec/epoch.tex | 2 -- shelley/chain-and-ledger/formal-spec/update.tex | 9 ++++----- 3 files changed, 8 insertions(+), 12 deletions(-) diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex index bc9f8c1a7f9..c32e20215c5 100644 --- a/shelley/chain-and-ledger/formal-spec/chain.tex +++ b/shelley/chain-and-ledger/formal-spec/chain.tex @@ -708,8 +708,8 @@ \subsection{Block Header Transition} \var{nes}' } \\~\\ - (\wcard,~\wcard,~\var{b_{prev}},~\wcard,~\var{es},~\var{ru},~\wcard,~\wcard)\leteq\var{nes} - % TODO: is es = (_ _ _ pp) ? + (\wcard,~\wcard,~\var{b_{prev}},~\wcard,~\var{es},~\var{ru},~\wcard,~\wcard)\leteq\var{nes} \\ + (\wcard,~\wcard,~\wcard,~\var{es})\leteq \var{es} \\ { \left( @@ -853,7 +853,7 @@ \subsection{Verifiable Random Function} & ~~~~\where \\ & ~~~~~~~~~~\var{hk} \leteq \hashKey{(\bvkcold bhb)} \\ & ~~~~~~~~~~\var{ss} \leteq \slotToSeed{(\bslot{bhb})} \\ - % TODO : is vk = bvkcold bhb ? + & ~~~~~~~~~~\var{vk} \leteq \fun{bvkcold}~\var{bhb} \\ \end{align*} \label{fig:vrf-checks} \end{figure} @@ -1383,8 +1383,7 @@ \subsection{Chain Transition} \eta_c' \\ \end{array}\right)} } \\~\\~\\ - \var{ls'}\leteq\fun{setIssueNumbers}~\var{ls}~\var{cs} \\ % TODO should - % this be 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/epoch.tex b/shelley/chain-and-ledger/formal-spec/epoch.tex index 266fbdd3d70..d1d0645cadd 100644 --- a/shelley/chain-and-ledger/formal-spec/epoch.tex +++ b/shelley/chain-and-ledger/formal-spec/epoch.tex @@ -901,8 +901,6 @@ \subsection{Complete Epoch Boundary Transition} \\~\\~\\ \var{(\wcard,~\wcard,~\wcard,~(\var{pup},~\wcard,~\wcard,~\wcard))}\leteq\var{utxoSt'}\\ \var{pp_{new}}\leteq\fun{votedValue_{PParams}}~\var{pup}\\ - % TODO: I think this isn't the right type, `pup` is PPUpdate which is not - % a complete set of `PParams`. { \begin{array}{l} \var{pp_{new}}\\ diff --git a/shelley/chain-and-ledger/formal-spec/update.tex b/shelley/chain-and-ledger/formal-spec/update.tex index 6d8bdf73803..d3414e795b6 100644 --- a/shelley/chain-and-ledger/formal-spec/update.tex +++ b/shelley/chain-and-ledger/formal-spec/update.tex @@ -244,7 +244,7 @@ \section{Updates} & \dom{\var{aup}}\subseteq\dom{\var{dms}} \\ - \var{aup'}\leteq\var{aup_s}\unionoverrideRight\var{aup} % TODO: not needed here? + \var{aup'}\leteq\var{aup_s}\unionoverrideRight\var{aup} & \var{fav}\leteq\fun{votedValue_{Applications}}~\var{aup'} \\ @@ -327,8 +327,7 @@ \section{Updates} \begin{equation}\label{eq:update} \inference[Update] { - (\var{pup},~\var{aup})\leteq\var{up} % TODO: duplicate of state names in - % signal + (\var{pup_{u}},~\var{aup_{u}})\leteq\var{up} \\~\\ { \left( @@ -340,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) & { @@ -361,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}