Epoch Boundary¶
This section is part of the
Ledger.Conway.Specification.Epoch
module of the formal ledger
specification
Definitions for the EPOCH and NEWEPOCH transition systems¶
record EpochState : Type where
field acnt : Acnt ss : Snapshots ls : LState es : EnactState fut : RatifyState
PoolDistr
(Shelley specification ) results from dividing
the coins in PoolDelegatedStake
by the total stake in
PoolDelegatedStake
. We avoid dividing the coins here, in
order to spare us the trouble of proving that the result is between 0
and 1.
We omit the VRF key hashes in the codomain of
PoolDelegatedStake
as they are not needed at the
moment.
PoolDelegatedStake : Type PoolDelegatedStake = KeyHash ⇀ Coin record NewEpochState : Type where field lastEpoch : Epoch epochState : EpochState ru : Maybe RewardUpdate pd : PoolDelegatedStake
Section RewardUpdate Creation defines
the function createRUpd
which creates a
RewardUpdate
, i.e. the net flow of Ada due to paying out
rewards after an epoch. 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 themonetaryExpansion
protocol parameter. -
rewardPot
: Total amount of coin available for rewards this epoch, as described in . -
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 thetreasuryCut
protocol parameter. The remaining pot is called theR
, just as in . -
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.
RewardUpdate Creation¶
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 = PParamsOf es reserves = ReservesOf es pstakego = es .EpochState.ss .Snapshots.go feeSS = es .EpochState.ss .Snapshots.feeSS stake = pstakego .Snapshot.stake delegs = pstakego .Snapshot.delegations poolParams = pstakego .Snapshot.poolParameters blocksMade = ∑[ m ← b ] m ρ = fromUnitInterval (prevPp .PParams.monetaryExpansion) η = fromℕ blocksMade ÷₀ (fromℕ slotsPerEpoch * ActiveSlotCoeff) Δr₁ = floor (1 ⊓ η * ρ * fromℕ reserves) rewardPot = pos feeSS + Δr₁ τ = fromUnitInterval (prevPp .PParams.treasuryCut) Δt₁ = floor (fromℤ rewardPot * τ) R = rewardPot - Δt₁ circulation = total - reserves rs = reward prevPp b (posPart R) poolParams stake delegs circulation Δr₂ = R - pos (∑[ c ← rs ] c)
Untitled Section¶
applyRUpd : RewardUpdate → EpochState → EpochState applyRUpd rewardUpdate $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#11056}{\htmlId{11056}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11067}{\htmlId{11067}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#11083}{\htmlId{11083}{\htmlClass{Bound}{\text{ss}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#11094}{\htmlId{11094}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11101}{\htmlId{11101}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11108}{\htmlId{11108}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11119}{\htmlId{11119}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#11138}{\htmlId{11138}{\htmlClass{Bound}{\text{govSt}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#11154}{\htmlId{11154}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11167}{\htmlId{11167}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11181}{\htmlId{11181}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#11194}{\htmlId{11194}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11203}{\htmlId{11203}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#11221}{\htmlId{11221}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11228}{\htmlId{11228}{\htmlClass{Bound}{\text{fut}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3287}{\htmlId{11246}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{11254}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#421}{\htmlId{11255}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#11056}{\htmlId{11259}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11268}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18195}{\htmlId{11270}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11273}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#421}{\htmlId{11275}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#11641}{\htmlId{11279}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{11287}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Prelude.html#3287}{\htmlId{11295}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{11303}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#421}{\htmlId{11304}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#11067}{\htmlId{11308}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11317}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18198}{\htmlId{11319}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{11321}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#11083}{\htmlId{11329}{\htmlClass{Bound}{\text{ss}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#11094}{\htmlId{11340}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3287}{\htmlId{11347}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{11355}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#421}{\htmlId{11356}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#11101}{\htmlId{11360}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11365}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18201}{\htmlId{11367}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{11369}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11108}{\htmlId{11373}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11119}{\htmlId{11384}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#11138}{\htmlId{11402}{\htmlClass{Bound}{\text{govSt}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#11154}{\htmlId{11418}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11167}{\htmlId{11431}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11181}{\htmlId{11445}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2046}{\htmlId{11453}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#11573}{\htmlId{11456}{\htmlClass{Function}{\text{regRU}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#11194}{\htmlId{11466}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11203}{\htmlId{11475}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#11221}{\htmlId{11490}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#11228}{\htmlId{11497}{\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 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')
Functions for computing stake distributions¶
gaDepositStake : GovState → Deposits → Credential ⇀ Coin gaDepositStake govSt ds = aggregateBy (mapˢ (λ (gaid , addr) → (gaid , addr) , stake addr) govSt') (mapFromPartialFun (λ (gaid , _) → lookupᵐ? ds (GovActionDeposit gaid)) govSt') where govSt' = mapˢ (map₂ returnAddr) (fromList govSt)
mkStakeDistrs : Snapshot → GovState → Deposits → VoteDelegs → StakeDistrs mkStakeDistrs ss govSt ds delegations .StakeDistrs.stakeDistr = aggregateBy ∣ delegations ∣ (Snapshot.stake ss ∪⁺ gaDepositStake govSt ds)
The aggregateBy
function takes a relation
R
: ℙ(A
× B
) and a map
m
: A
⇀
C
and
returns a function that maps each a
in the domain of
m
to the sum of all b
such that
(a
, b
) ∈ R
.
In the definition of mkStakeDistrs
, the relation and
map passed to aggregateBy
are ∣
delegations
∣
: ℙ
Credential
×
VDeleg
and stakeOf
ss
∪⁺
gaDepositStake
govSt
ds
,
respectively.
The EPOCH
transition has a few
updates that are encapsulated in the following functions. We need these
functions to bring them in scope for some proofs about
EPOCH
.
EPOCH update functions¶
record EPOCH-Updates0 : Type where constructor EPOCHUpdates0 field es : EnactState govSt' : GovState payout : Withdrawals gState' : GState utxoSt' : UTxOState totWithdrawals : Coin EPOCH-updates0 : RatifyState → LState → EPOCH-Updates0 EPOCH-updates0 fut ls = EPOCHUpdates0 es govSt' payout gState' utxoSt' totWithdrawals where open LState ls public open CertState certState public open RatifyState fut renaming (es to esW) es : EnactState es = record esW { withdrawals = ∅ } 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 govSt' : GovState govSt' = filter (λ x → proj₁ x ∉ mapˢ proj₁ removed') govSt removedGovActions : ℙ (RwdAddr × DepositPurpose × Coin) removedGovActions = flip concatMapˢ removed' λ (gaid , gaSt) → mapˢ (returnAddr gaSt ,_) ((DepositsOf utxoSt ∣ ❴ GovActionDeposit gaid ❵) ˢ) govActionReturns : RwdAddr ⇀ Coin govActionReturns = aggregate₊ (mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ) payout : RwdAddr ⇀ Coin payout = govActionReturns ∪⁺ WithdrawalsOf esW gState' : GState gState' = $\begin{pmatrix} \,\htmlId{15635}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{15636}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{15639}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#15058}{\htmlId{15644}{\htmlClass{Function}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{15651}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#6068}{\htmlId{15656}{\htmlClass{Function}{\text{mapValues}}}}\, \,\htmlId{15666}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{15667}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{15669}{\htmlClass{Field Operator}{\text{+\_}}}}\,\,\htmlId{15671}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{15673}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2052}{\htmlId{15674}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4983}{\htmlId{15682}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{15688}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{15690}{\htmlClass{Function Operator}{\text{else}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#2052}{\htmlId{15695}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4983}{\htmlId{15703}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{15709}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1967}{\htmlId{15719}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4983}{\htmlId{15731}{\htmlClass{Function}{\text{gState}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{15738}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#2942}{\htmlId{15740}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{15748}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#2024}{\htmlId{15749}{\htmlClass{Field}{\text{EnactState.cc}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#14728}{\htmlId{15763}{\htmlClass{Function}{\text{es}}}}\,\,\htmlId{15765}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ utxoSt' : UTxOState utxoSt' = record utxoSt { deposits = DepositsOf utxoSt ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ ; donations = 0 } totWithdrawals : Coin totWithdrawals = ∑[ x ← WithdrawalsOf esW ] x record EPOCH-Updates : Type where constructor EPOCHUpdates field es : EnactState govSt' : GovState dState'' : DState gState' : GState utxoSt' : UTxOState acnt'' : Acnt EPOCH-updates : RatifyState → LState → DState → Acnt → EPOCH-Updates EPOCH-updates fut ls dState' acnt' = EPOCHUpdates (u0 .es) (u0 .govSt') dState'' (u0 .gState') (u0 .utxoSt') acnt'' where open LState open EPOCH-Updates0 u0 = EPOCH-updates0 fut ls refunds : Credential ⇀ Coin refunds = pullbackMap (u0 .payout) toRwdAddr (dom (RewardsOf dState')) dState'' : DState dState'' = record dState' { rewards = RewardsOf dState' ∪⁺ refunds } unclaimed : Coin unclaimed = getCoin (u0 .payout) - getCoin refunds acnt'' : Acnt acnt'' = record acnt' { treasury = TreasuryOf acnt' ∸ u0 .totWithdrawals + DonationsOf ls + unclaimed }
data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Type where
Section EPOCH transition system defines the EPOCH transition rule. Previously, this incorporated the logic that is now handled by POOLREAP (Shelley specification ).
The EPOCH rule now also needs to invoke RATIFIES and properly deal with its results by carrying out each of the following tasks.
-
Pay out all the enacted treasury withdrawals.
-
Remove expired and enacted governance actions & refund deposits.
-
If
govSt’
is empty, increment the activity counter for DReps. -
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
fut
and store the resulting enact statefut’
.
EPOCH transition system¶
EPOCH : ∀ {acnt : Acnt} {utxoSt'' : UTxOState} {acnt' dState' pState'} → let EPOCHUpdates es govSt' dState'' gState' utxoSt' acnt'' = EPOCH-updates fut ls dState' acnt' in record { currentEpoch = e ; stakeDistrs = mkStakeDistrs (Snapshots.mark ss') govSt' (DepositsOf utxoSt') (VoteDelegsOf ls) ; treasury = TreasuryOf acnt ; GState (GStateOf ls) ; pools = PoolsOf ls ; delegatees = VoteDelegsOf ls } ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18025}{\htmlId{18571}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{18576}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{18580}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut' → ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss' → _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18052}{\htmlId{18665}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17935}{\htmlId{18675}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#5201}{\htmlId{18682}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#13778}{\htmlId{18691}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#5309}{\htmlId{18696}{\htmlClass{Field}{\text{PStateOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#13778}{\htmlId{18705}{\htmlClass{Generalizable}{\text{ls}}}}\, \end{pmatrix}$ ⇀⦇ e ,POOLREAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#17949}{\htmlId{18728}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17972}{\htmlId{18739}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17978}{\htmlId{18747}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17986}{\htmlId{18757}{\htmlClass{Bound}{\text{pState'}}}}\, \end{pmatrix}$ ──────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#17935}{\htmlId{18818}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13869}{\htmlId{18825}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13778}{\htmlId{18830}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13792}{\htmlId{18835}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13691}{\htmlId{18841}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18060}{\htmlId{18862}{\htmlClass{Bound}{\text{acnt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13872}{\htmlId{18871}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#17949}{\htmlId{18879}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18028}{\htmlId{18890}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#18035}{\htmlId{18901}{\htmlClass{Bound}{\text{dState''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17986}{\htmlId{18912}{\htmlClass{Bound}{\text{pState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18044}{\htmlId{18922}{\htmlClass{Bound}{\text{gState'}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#18025}{\htmlId{18938}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13695}{\htmlId{18943}{\htmlClass{Generalizable}{\text{fut'}}}}\, \end{pmatrix}$
The calculatePoolDelegatedState
produces a new pool distribution from the delegation map and stake
allocation of the previous epoch.
calculatePoolDelegatedStake
performs the computation of
calculatePoolDistr
in the Shelley spec, without
normalizing the stakes to be between 0 and 1.
NEWEPOCH transition system¶
opaque calculatePoolDelegatedStake : Snapshot → PoolDelegatedStake calculatePoolDelegatedStake ss = -- Shelley spec: the output map must contain keys appearing in both -- sd and the pool parameters. sd ∣ dom (ss .poolParameters) where open Snapshot -- delegated stake per pool sd : KeyHash ⇀ Coin sd = aggregate₊ ((stakeCredentialsPerPool ∘ʳ (ss .stake ˢ)) ᶠˢ) where mutual -- stake credentials delegating to each pool stakeCredentialsPerPool : Rel KeyHash Credential stakeCredentialsPerPool = (ss .delegations ˢ) ⁻¹ʳ -- TODO: Move to agda-sets -- https://github.com/input-output-hk/agda-sets/pull/13 _⁻¹ʳ : {A B : Type} → Rel A B → Rel B A R ⁻¹ʳ = mapˢ swap R where open import Data.Product using (swap) _∘ʳ_ : {A B C : Type} ⦃ _ : DecEq B ⦄ → Rel A B → Rel B C → Rel A C R ∘ʳ S = concatMapˢ (λ (a , b) → mapˢ ((a ,_) ∘ proj₂) $ filterˢ ((b ≡_) ∘ proj₁) S) R
_⊢_⇀⦇_,NEWEPOCH⦈_ : ⊤ → NewEpochState → Epoch → NewEpochState → Type
NEWEPOCH-New : let eps' = applyRUpd ru eps $\begin{pmatrix} \,\htmlId{20620}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#20624}{\htmlId{20624}{\htmlClass{Bound}{\text{ss}}}}\, \\ \,\htmlId{20629}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{20633}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{20637}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = eps'' pd' = calculatePoolDelegatedStake (Snapshots.set ss) in ∙ e ≡ lastEpoch + 1 ∙ _ ⊢ eps' ⇀⦇ e ,EPOCH⦈ eps'' ──────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#13671}{\htmlId{20826}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13748}{\htmlId{20838}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{20844}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#13890}{\htmlId{20849}{\htmlClass{Generalizable}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13937}{\htmlId{20854}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#13669}{\htmlId{20877}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13757}{\htmlId{20881}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{20889}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#20657}{\htmlId{20899}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$ NEWEPOCH-Not-New : ∙ e ≢ lastEpoch + 1 ──────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#13671}{\htmlId{21002}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13748}{\htmlId{21014}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13910}{\htmlId{21020}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13937}{\htmlId{21026}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#13671}{\htmlId{21049}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13748}{\htmlId{21061}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13910}{\htmlId{21067}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13937}{\htmlId{21073}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ NEWEPOCH-No-Reward-Update : let $\begin{pmatrix} \,\htmlId{21121}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#21125}{\htmlId{21125}{\htmlClass{Bound}{\text{ss}}}}\, \\ \,\htmlId{21130}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{21134}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{21138}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = eps' pd' = calculatePoolDelegatedStake (Snapshots.set ss) in ∙ e ≡ lastEpoch + 1 ∙ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps' ──────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#13671}{\htmlId{21324}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13748}{\htmlId{21336}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{21342}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13937}{\htmlId{21352}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#13669}{\htmlId{21375}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#13752}{\htmlId{21379}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{21386}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#21157}{\htmlId{21396}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$