Epoch Boundary¶
This module introduces the epoch boundary transition system and the related reward calculation.
Epoch State¶
The EpochState type encapsulates the components needed to represent an epoch state.
record EpochState : Type where
field acnt : Acnt ss : Snapshots ls : LState es : EnactState fut : RatifyState
Note that the Acnt type has two fields—treasury and
reserves. Thus the acnt field in EpochState
can keep track of the total assets that remain in treasury and reserves.
PoolDelegatedStake : Type PoolDelegatedStake = KeyHash ⇀ Coin record NewEpochState : Type where field lastEpoch : Epoch bprev : BlocksMade bcur : BlocksMade epochState : EpochState ru : Maybe RewardUpdate pd : PoolDelegatedStake
Differences with the Shelley Specification
The formal specification utilizes the type PoolDelegatedStake
in lieu of the derived type PoolDistr (Figure 5, Shelley
specification CVG19). The latter can be computed from the
former by divinding the associated Coin to each KeyHash
by the total stake in the map.
In addition, the formal specification omits the VRF key hashes in the
codomain of PoolDelegatedStake as they are not implemented at
the moment.
Reward Updates¶
Computing Reward Updates¶
This section defines the function createRUpd which creates a
RewardUpdate, i.e. the net flow of Ada due to paying out rewards
after an epoch:
createRUpd : ℕ → BlocksMade → EpochState → Coin → RewardUpdate createRUpd slotsPerEpoch b es total = record { Δt = Δt₁ ; Δr = 0 - Δr₁ + Δr₂ ; Δf = 0 - pos feeSS ; rs = rs
} where prevPp : PParams prevPp = PParamsOf es reserves : Reserves reserves = ReservesOf es pstakego : Snapshot pstakego = (SnapshotsOf es) .Snapshots.go feeSS : Fees feeSS = FeesOf (SnapshotsOf es) stake : Stake stake = StakeOf pstakego delegs : StakeDelegs delegs = StakeDelegsOf pstakego poolParams : Pools poolParams = PoolsOf pstakego blocksMade : ℕ blocksMade = ∑[ m ← b ] m ρ η τ : ℚ ρ = fromUnitInterval (prevPp .PParams.monetaryExpansion) η = fromℕ blocksMade ÷₀ (fromℕ slotsPerEpoch * ActiveSlotCoeff) τ = fromUnitInterval (prevPp .PParams.treasuryCut) Δr₁ rewardPot Δt₁ R : ℤ Δr₁ = floor (1 ⊓ η * ρ * fromℕ reserves) rewardPot = pos feeSS + Δr₁ Δt₁ = floor (fromℤ rewardPot * τ) R = rewardPot - Δt₁ circulation : Coin circulation = total - reserves rs : Rewards rs = reward prevPp b (posPart R) poolParams stake delegs circulation Δr₂ : ℤ Δr₂ = R - pos (∑[ c ← rs ] c)
Relevant quantities are:
-
prevPp: Previous protocol parameters, which correspond to the parameters during the epoch for which we are creating rewards. -
ActiveSlotCoeff: Global constant, equal to the probability that a party holding all the stake will be selected to be a leader for given slot. Equals \(1/20\) during the Shelley era on the Cardano Mainnet. -
Δr₁: Ada taken out of the reserves for paying rewards, as determined by themonetaryExpansionprotocol parameter. -
rewardPot: Total amount of coin available for rewards this epoch, as described in Team18. -
feeSS: The fee pot which, together with the reserves, funds therewardPot. We use the fee pot that accumulated during the epoch for which we now compute block production rewards. Note that fees are not explicitly removed from any account: the fees come from transactions paying them and are accounted for whenever transactions are processed. -
Δt₁: The proportion of the reward pot that will move to the treasury, as determined by thetreasuryCutprotocol parameter. The remaining pot is called theR, just as in Team18. -
pstakego: Stake distribution used for calculating the rewards. This is the oldest stake distribution snapshot, labeledgo. -
rs: The rewards, as calculated by the functionreward. -
Δr₂: The difference between the maximal amount of rewards that could have been paid out if pools had been optimal, and the actual rewards paid out. This difference is returned to the reserves. -
÷₀: Division operator that returns zero when the denominator is zero.
Applying Reward Updates¶
This section defines the function applyRUpd, which applies a
RewardUpdate to the EpochState.
applyRUpd : RewardUpdate → EpochState → EpochState applyRUpd rewardUpdate $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12537}{\htmlId{12537}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12548}{\htmlId{12548}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12585}{\htmlId{12585}{\htmlClass{Bound}{\text{ss}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12617}{\htmlId{12617}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12624}{\htmlId{12624}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12631}{\htmlId{12631}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12642}{\htmlId{12642}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12682}{\htmlId{12682}{\htmlClass{Bound}{\text{govSt}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12719}{\htmlId{12719}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12732}{\htmlId{12732}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12746}{\htmlId{12746}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12759}{\htmlId{12759}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12768}{\htmlId{12768}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12807}{\htmlId{12807}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12835}{\htmlId{12835}{\htmlClass{Bound}{\text{fut}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3352}{\htmlId{12872}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{12880}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#656}{\htmlId{12881}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12537}{\htmlId{12885}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12894}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18002}{\htmlId{12896}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12899}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#656}{\htmlId{12901}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#13456}{\htmlId{12905}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{12913}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Prelude.html#3352}{\htmlId{12948}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{12956}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#656}{\htmlId{12957}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12548}{\htmlId{12961}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12970}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18005}{\htmlId{12972}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{12974}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12585}{\htmlId{13009}{\htmlClass{Bound}{\text{ss}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12617}{\htmlId{13047}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3352}{\htmlId{13054}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{13062}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#656}{\htmlId{13063}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12624}{\htmlId{13067}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{13072}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18008}{\htmlId{13074}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{13076}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12631}{\htmlId{13080}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12642}{\htmlId{13091}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12682}{\htmlId{13136}{\htmlClass{Bound}{\text{govSt}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12719}{\htmlId{13179}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12732}{\htmlId{13192}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12746}{\htmlId{13206}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{13214}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#13388}{\htmlId{13217}{\htmlClass{Function}{\text{regRU}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12759}{\htmlId{13227}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12768}{\htmlId{13236}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12807}{\htmlId{13278}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12835}{\htmlId{13312}{\htmlClass{Bound}{\text{fut}}}}\, \end{pmatrix}$ where open RewardUpdate rewardUpdate using (Δt; Δr; Δf; rs) regRU = rs ∣ dom rewards unregRU = rs ∣ dom rewards ᶜ unregRU' = ∑[ x ← unregRU ] x
Stake Distributions¶
This section defines the functions
calculatePoolDelegatedState,
calculateVDelegDelegatedStake, and
mkStakeDistrs, which calculates stake distributions
for voting purposes.
calculatePoolDelegatedStake : Snapshot → PoolDelegatedStake calculatePoolDelegatedStake ss = -- Shelley spec: the output map must contain keys appearing in both -- sd and the pool parameters. sd ∣ dom (PoolsOf ss) where -- stake credentials delegating to each pool stakeCredentialsPerPool : Rel KeyHash Credential stakeCredentialsPerPool = (StakeDelegsOf ss ˢ) ⁻¹ʳ -- delegated stake per pool sd : KeyHash ⇀ Coin sd = aggregate₊ ((stakeCredentialsPerPool ∘ʳ (StakeOf ss ˢ)) ᶠˢ)
The function calculatePoolDelegatedState calculates the delegated
stake to SPOs. This function is used both in the
EPOCH rule (via
calculatePoolDelegatedStateForVoting, see below) and in the
NEWEPOCH rule.
stakeFromGADeposits : GovState → UTxOState → Stake stakeFromGADeposits govSt utxoSt = aggregateBy (mapˢ (λ (gaid , addr) → (gaid , addr) , stake addr) govSt') (mapFromPartialFun (λ (gaid , _) → lookupᵐ? deposits (GovActionDeposit gaid)) govSt') where open UTxOState utxoSt govSt' : ℙ (GovActionID × RwdAddr) govSt' = mapˢ (map₂ returnAddr) (fromList govSt)
The function stakeFromGADeposits computes the stake
pertaining to governance action deposits. It returns a map which, for
each governance action, maps its returnAddr (as a staking
credential) to the deposit.
module VDelegDelegatedStake (currentEpoch : Epoch) (utxoSt : UTxOState) (govSt : GovState) (gState : GState) (dState : DState) where activeDReps : ℙ Credential activeDReps = dom (activeDRepsOf gState currentEpoch) activeVDelegs : ℙ VDeleg activeVDelegs = mapˢ vDelegCredential activeDReps ∪ ❴ vDelegNoConfidence ❵ ∪ ❴ vDelegAbstain ❵ -- compute the stake for a credential stakePerCredential : Credential → Coin stakePerCredential c = cbalance ((UTxOOf utxoSt) ∣^' λ txout → getStakeCred txout ≡ just c) + fromMaybe 0 (lookupᵐ? (stakeFromGADeposits govSt utxoSt) c) + fromMaybe 0 (lookupᵐ? (RewardsOf dState) c) calculate : VDeleg ⇀ Coin calculate = mapFromFun (λ vd → ∑ˢ[ c ← (VoteDelegsOf dState) ⁻¹ vd ] (stakePerCredential c)) activeVDelegs
calculateVDelegDelegatedStake : Epoch → UTxOState → GovState → GState → DState → VDeleg ⇀ Coin calculateVDelegDelegatedStake = VDelegDelegatedStake.calculate
calculatePoolDelegatedStakeForVoting : Snapshot → UTxOState → GovState → KeyHash ⇀ Coin calculatePoolDelegatedStakeForVoting ss utxoSt govSt = calculatePoolDelegatedStake ss ∪⁺ (stakeFromDeposits ∣ dom (PoolsOf ss)) where stakeFromDeposits : KeyHash ⇀ Coin stakeFromDeposits = aggregate₊ (((StakeDelegsOf ss ˢ) ⁻¹ʳ ∘ʳ (stakeFromGADeposits govSt utxoSt ˢ)) ᶠˢ)
The function calculatePoolDelegatedStakeForVoting computes the
delegated stake to SPOs that will be used for counting
votes. It complements the result of calculatePoolDelegatedStake with
the deposits made to governance actions.
Erratum
CIP-1694 specifies that deposits of governance actions should count towards the stake for voting purposes:
The deposit amount will be added to the deposit pot, similar to stake key deposits. It will also be counted towards the stake of the reward address it will be paid back to, to not reduce the submitter's voting power to vote on their own (and competing) actions.
While originally intended for DReps
only, the Haskell implementation and the formal specification
count deposits on governance actions towards the stake of
SPOs as well.
mkStakeDistrs : Snapshot → Epoch → UTxOState → GovState → GState → DState → StakeDistrs mkStakeDistrs ss currentEpoch utxoSt govSt gState dState = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#16268}{\htmlId{18113}{\htmlClass{Function}{\text{calculateVDelegDelegatedStake}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18067}{\htmlId{18143}{\htmlClass{Bound}{\text{currentEpoch}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18080}{\htmlId{18156}{\htmlClass{Bound}{\text{utxoSt}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18087}{\htmlId{18163}{\htmlClass{Bound}{\text{govSt}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18093}{\htmlId{18169}{\htmlClass{Bound}{\text{gState}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18100}{\htmlId{18176}{\htmlClass{Bound}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#16494}{\htmlId{18187}{\htmlClass{Function}{\text{calculatePoolDelegatedStakeForVoting}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18064}{\htmlId{18224}{\htmlClass{Bound}{\text{ss}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18080}{\htmlId{18227}{\htmlClass{Bound}{\text{utxoSt}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18087}{\htmlId{18234}{\htmlClass{Bound}{\text{govSt}}}}\, \end{pmatrix}$
The EPOCH Transition System¶
The EPOCH transition system updates several parts of the
EpochState. We encapsulate these updates using Agda's module
system. This modularization reduces typechecking times and helps strucuturing
proofs about properties of the EPOCH transition system.
Update Modules and Functions¶
We organize the EPOCH rule around three modules.
-
GovernanceUpdateis used to compute the set of governance actions to be removed and update the governance state accordingly; -
Pre-POOLREAPUpdateis used to update thePState,GStateandutxoStwhich are the inputs to thePOOLREAPtransition system; -
Post-POOLREAPUpdateis used to updateAcntandDStatefrom the output ofPOOLREAPpart of which is in the environment of theRATIFYtransition system and part of which belongs to the returnedEpochState.
Helper Functions¶
getOrphans : EnactState → GovState → GovState getOrphans es govSt = proj₁ $ iterate step ([] , govSt) (length govSt) where step : GovState × GovState → GovState × GovState step (orps , govSt) = let isOrphan? a prev = ¬? (hasParent? es govSt a prev) (orps' , govSt') = partition (λ (_ , record {action = a ; prevAction = prev}) → isOrphan? (a .gaType) prev) govSt in (orps ++ orps' , govSt') record Governance-Update : Type where constructor GovernanceUpdate field removedGovActions : ℙ (RwdAddr × DepositPurpose × Coin) govSt' : GovState module GovernanceUpdate (ls : LState) (fut : RatifyState) where
tmpGovSt : GovState tmpGovSt = filter (λ x → proj₁ x ∉ mapˢ proj₁ removed) govSt orphans : ℙ (GovActionID × GovActionState) orphans = fromList (getOrphans es tmpGovSt) removed' : ℙ (GovActionID × GovActionState) removed' = removed ∪ orphans removedGovActions : ℙ (RwdAddr × DepositPurpose × Coin) removedGovActions = flip concatMapˢ removed' λ (gaid , gaSt) → mapˢ (returnAddr gaSt ,_) ((DepositsOf utxoSt ∣ ❴ GovActionDeposit gaid ❵) ˢ) govSt' : GovState govSt' = filter (λ x → proj₁ x ∉ mapˢ proj₁ removed') govSt updates : Governance-Update updates = GovernanceUpdate removedGovActions govSt' record Pre-POOLREAP-Update : Type where inductive constructor Pre-POOLREAPUpdate field pState' : PState gState' : GState utxoSt' : UTxOState module Pre-POOLREAPUpdate (ls : LState) (es : EnactState) (govUpdate : Governance-Update) where
utxoSt' : UTxOState utxoSt' = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Transaction.html#4490}{\htmlId{21786}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1408}{\htmlId{21793}{\htmlClass{Function}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{21802}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1408}{\htmlId{21809}{\htmlClass{Function}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1154}{\htmlId{21818}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1408}{\htmlId{21829}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{21836}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#519}{\htmlId{21838}{\htmlClass{Function}{\text{mapˢ}}}}\, \,\htmlId{21843}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{21844}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Function.Base.html#1134}{\htmlId{21850}{\htmlClass{Function Operator}{\text{∘}}}}\, \,\href{Data.Product.Base.html#650}{\htmlId{21852}{\htmlClass{Field}{\text{proj₂}}}}\,\,\htmlId{21857}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#20332}{\htmlId{21859}{\htmlClass{Field}{\text{removedGovActions}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{21877}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{21881}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$ pState' : PState pState' = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#4420}{\htmlId{21919}{\htmlClass{Function}{\text{fPools}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{21926}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4398}{\htmlId{21929}{\htmlClass{Function}{\text{pools}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{21937}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4442}{\htmlId{21941}{\htmlClass{Function}{\text{retiring}}}}\, \end{pmatrix}$ gState' : GState gState' = $\begin{pmatrix} \,\htmlId{21990}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{21991}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{21994}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#20392}{\htmlId{21999}{\htmlClass{Field}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{22006}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#7106}{\htmlId{22011}{\htmlClass{Function}{\text{mapValues}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#1150}{\htmlId{22021}{\htmlClass{Function}{\text{sucᵉ}}}}\, \,\htmlId{22026}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#14319}{\htmlId{22027}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4774}{\htmlId{22035}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{22041}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{22043}{\htmlClass{Function Operator}{\text{else}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#14319}{\htmlId{22048}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4774}{\htmlId{22056}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{22062}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1778}{\htmlId{22070}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4774}{\htmlId{22082}{\htmlClass{Function}{\text{gState}}}}\, \,\href{Axiom.Set.Map.html#13534}{\htmlId{22089}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#2583}{\htmlId{22091}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{22099}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#1670}{\htmlId{22100}{\htmlClass{Field}{\text{EnactState.cc}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#21487}{\htmlId{22114}{\htmlClass{Bound}{\text{es}}}}\,\,\htmlId{22116}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ updates : Pre-POOLREAP-Update updates = Pre-POOLREAPUpdate pState' gState' utxoSt' record Post-POOLREAP-Update : Type where inductive constructor Post-POOLREAPUpdate field dState'' : DState acnt'' : Acnt module Post-POOLREAPUpdate (es : EnactState) (ls : LState) (dState' : DState) (acnt' : Acnt) (govUpd : Governance-Update) where
opaque govActionReturns : RwdAddr ⇀ Coin govActionReturns = aggregate₊ (mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ) payout : RwdAddr ⇀ Coin payout = govActionReturns ∪⁺ WithdrawalsOf es opaque refunds : Credential ⇀ Coin refunds = pullbackMap payout toRwdAddr (dom (RewardsOf dState')) dState'' : DState dState'' = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#7079}{\htmlId{23070}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#22477}{\htmlId{23083}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#2193}{\htmlId{23093}{\htmlClass{Field}{\text{StakeDelegsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#22477}{\htmlId{23107}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#2028}{\htmlId{23117}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#22477}{\htmlId{23127}{\htmlClass{Bound}{\text{dState'}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{23135}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#22937}{\htmlId{23138}{\htmlClass{Function}{\text{refunds}}}}\, \end{pmatrix}$ unclaimed : Coin unclaimed = getCoin payout - getCoin refunds totWithdrawals : Coin totWithdrawals = ∑[ x ← WithdrawalsOf es ] x acnt'' : Acnt acnt'' = $\begin{pmatrix} \,\href{Ledger.Prelude.Base.html#985}{\htmlId{23317}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#22523}{\htmlId{23328}{\htmlClass{Bound}{\text{acnt'}}}}\, \,\href{Data.Nat.Base.html#4462}{\htmlId{23334}{\htmlClass{Primitive Operator}{\text{∸}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#23218}{\htmlId{23336}{\htmlClass{Function}{\text{totWithdrawals}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{23351}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#650}{\htmlId{23353}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#22436}{\htmlId{23365}{\htmlClass{Bound}{\text{ls}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{23368}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#23151}{\htmlId{23370}{\htmlClass{Function}{\text{unclaimed}}}}\, \\ \,\href{Ledger.Prelude.Base.html#869}{\htmlId{23382}{\htmlClass{Field}{\text{ReservesOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#22523}{\htmlId{23393}{\htmlClass{Bound}{\text{acnt'}}}}\, \end{pmatrix}$ updates : Post-POOLREAP-Update updates = Post-POOLREAPUpdate dState'' acnt''
Transition Rule¶
This section defines the EPOCH transition rule.
In Conway, the EPOCH rule invokes RATIFIES,
and carries out the following tasks:
-
payout all the enacted treasury withdrawals;
-
remove expired and enacted governance actions, and refund deposits;
-
if
govSt’is empty, increment the activity counter forDReps; -
remove all hot keys from the constitutional committee delegation map that do not belong to currently elected members;
-
Apply the resulting enact state from the previous epoch boundary
futand store the resulting enact statefut’.
data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Type where
EPOCH : let es = EnactStateOf fut govUpd : Governance-Update govUpd = GovernanceUpdate.updates ls fut Pre-POOLREAPUpdate pState' gState' utxoSt' = Pre-POOLREAPUpdate.updates ls es govUpd Post-POOLREAPUpdate dState'' acnt'' = Post-POOLREAPUpdate.updates es ls dState' acnt' govUpd es' : EnactState es' = record es { withdrawals = ∅ } govSt' : GovState govSt' = Governance-Update.govSt' govUpd stakeDistrs : StakeDistrs stakeDistrs = mkStakeDistrs (Snapshots.mark ss') e utxoSt' govSt' (GStateOf ls) (DStateOf ls) Γ : RatifyEnv Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#24752}{\htmlId{24945}{\htmlClass{Bound}{\text{stakeDistrs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18279}{\htmlId{24959}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#14319}{\htmlId{24963}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18388}{\htmlId{24971}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1778}{\htmlId{24976}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18388}{\htmlId{24988}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Prelude.Base.html#985}{\htmlId{24993}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#24543}{\htmlId{25004}{\htmlClass{Bound}{\text{acnt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1863}{\htmlId{25013}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18388}{\htmlId{25021}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#7079}{\htmlId{25026}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18388}{\htmlId{25039}{\htmlClass{Generalizable}{\text{ls}}}}\, \end{pmatrix}$ in ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss' ∙ _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#24458}{\htmlId{25100}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18518}{\htmlId{25110}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4990}{\htmlId{25117}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18388}{\htmlId{25126}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24442}{\htmlId{25131}{\htmlClass{Bound}{\text{pState'}}}}\, \end{pmatrix}$ ⇀⦇ e ,POOLREAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18538}{\htmlId{25159}{\htmlClass{Generalizable}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18523}{\htmlId{25170}{\htmlClass{Generalizable}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18499}{\htmlId{25178}{\htmlClass{Generalizable}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18479}{\htmlId{25188}{\htmlClass{Generalizable}{\text{pState''}}}}\, \end{pmatrix}$ ∙ Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#24614}{\htmlId{25214}{\htmlClass{Bound}{\text{es'}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{25220}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{25224}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut' ────────────────────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18518}{\htmlId{25323}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18561}{\htmlId{25330}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18388}{\htmlId{25335}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18402}{\htmlId{25340}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18301}{\htmlId{25346}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#24543}{\htmlId{25367}{\htmlClass{Bound}{\text{acnt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18564}{\htmlId{25376}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18538}{\htmlId{25384}{\htmlClass{Generalizable}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24680}{\htmlId{25395}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#24534}{\htmlId{25406}{\htmlClass{Bound}{\text{dState''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18479}{\htmlId{25417}{\htmlClass{Generalizable}{\text{pState''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24450}{\htmlId{25428}{\htmlClass{Bound}{\text{gState'}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#24614}{\htmlId{25444}{\htmlClass{Bound}{\text{es'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18305}{\htmlId{25450}{\htmlClass{Generalizable}{\text{fut'}}}}\, \end{pmatrix}$
The NEWEPOCH Transition System¶
Finally, we define the NEWEPOCH transition system, which computes
the new state as of the start of a new epoch.
data _⊢_⇀⦇_,NEWEPOCH⦈_ : ⊤ → NewEpochState → Epoch → NewEpochState → Type where NEWEPOCH-New : ∀ {bprev bcur : BlocksMade} → let eps' = applyRUpd ru eps ss = EpochState.ss eps'' pd' = calculatePoolDelegatedStake (Snapshots.set ss) in ∙ e ≡ lastEpoch + 1 ∙ _ ⊢ eps' ⇀⦇ e ,EPOCH⦈ eps'' ────────────────────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18281}{\htmlId{26100}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#25808}{\htmlId{26112}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#25814}{\htmlId{26120}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18358}{\htmlId{26127}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{26133}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18582}{\htmlId{26138}{\htmlClass{Generalizable}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18629}{\htmlId{26143}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18279}{\htmlId{26166}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#25814}{\htmlId{26170}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Axiom.Set.Map.html#2671}{\htmlId{26177}{\htmlClass{Function}{\text{∅ᵐ}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18367}{\htmlId{26183}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{26191}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#25912}{\htmlId{26201}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$ NEWEPOCH-Not-New : ∀ {bprev bcur : BlocksMade} → ∙ e ≢ lastEpoch + 1 ────────────────────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18281}{\htmlId{26348}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#26232}{\htmlId{26360}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#26238}{\htmlId{26368}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18358}{\htmlId{26375}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18602}{\htmlId{26381}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18629}{\htmlId{26387}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18281}{\htmlId{26410}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#26232}{\htmlId{26422}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#26238}{\htmlId{26430}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18358}{\htmlId{26437}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18602}{\htmlId{26443}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18629}{\htmlId{26449}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ NEWEPOCH-No-Reward-Update : ∀ {bprev bcur : BlocksMade} → let ss = EpochState.ss eps' pd' = calculatePoolDelegatedStake (Snapshots.set ss) in ∙ e ≡ lastEpoch + 1 ∙ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps' ────────────────────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18281}{\htmlId{26745}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#26488}{\htmlId{26757}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#26494}{\htmlId{26765}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18358}{\htmlId{26772}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{26778}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18629}{\htmlId{26788}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18279}{\htmlId{26811}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#26494}{\htmlId{26815}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Axiom.Set.Map.html#2671}{\htmlId{26822}{\htmlClass{Function}{\text{∅ᵐ}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18362}{\htmlId{26827}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{26834}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#26560}{\htmlId{26844}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$
References¶
[CVG19] Jared Corduan and Polina Vinogradova and Matthias Güdemann. A Formal Specification of the Cardano Ledger. 2019.
[Team18] IOHK Formal Methods Team. Design Specification for Delegation and Incentives in Cardano, IOHK Deliverable SL-D1. 2018.