{-# OPTIONS --safe #-}
open import Data.Integer using () renaming (+_ to pos)
import Data.Integer as ℤ
open import Data.Integer.Properties using (module ≤-Reasoning; +-mono-≤; neg-mono-≤; +-identityˡ)
renaming (nonNegative⁻¹ to nonNegative⁻¹ℤ)
open import Data.Nat.GeneralisedArithmetic using (iterate)
open import Data.Rational using (ℚ; floor; _*_; _÷_; _/_; _⊓_; _≟_; ≢-nonZero)
open import Data.Rational.Literals using (number; fromℤ)
open import Data.Rational.Properties using (nonNegative⁻¹; pos⇒nonNeg; ⊓-glb)
open import stdlib.Data.Rational.Properties using (0≤⇒0≤floor; ÷-0≤⇒0≤; fromℕ-0≤; *-0≤⇒0≤; fromℤ-0≤)
open import Data.Integer.Tactic.RingSolver using (solve-∀)
open import Agda.Builtin.FromNat
open import Ledger.Prelude hiding (iterate; _/_; _*_; _⊓_; _≟_; ≢-nonZero)
open Filter using (filter)
open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction
open import Ledger.Prelude.Numeric.UnitInterval using (fromUnitInterval; UnitInterval-*-0≤)
open Number number renaming (fromNat to fromℕ)
module Ledger.Conway.Specification.Epoch
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where
open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Gov txs
open import Ledger.Conway.Specification.Ledger txs abs
open import Ledger.Conway.Specification.PoolReap txs abs
open import Ledger.Conway.Specification.Ratify txs
open import Ledger.Conway.Specification.Rewards txs abs
open import Ledger.Conway.Specification.Utxo txs abs
record EpochState : Type where
constructor ⟦_,_,_,_,_⟧ᵉ'
field
acnt : Acnt
ss : Snapshots
ls : LState
es : EnactState
fut : RatifyState
record HasEpochState {a} (A : Type a) : Type a where
field EpochStateOf : A → EpochState
open HasEpochState ⦃...⦄ public
instance
HasLState-EpochState : HasLState EpochState
HasLState-EpochState .LStateOf = EpochState.ls
HasEnactState-EpochState : HasEnactState EpochState
HasEnactState-EpochState .EnactStateOf = EpochState.es
HasDeposits-EpochState : HasDeposits EpochState
HasDeposits-EpochState .DepositsOf = DepositsOf ∘ LStateOf
HasTreasury-EpochState : HasTreasury EpochState
HasTreasury-EpochState .TreasuryOf = Acnt.treasury ∘ EpochState.acnt
HasReserves-EpochState : HasReserves EpochState
HasReserves-EpochState .ReservesOf = Acnt.reserves ∘ EpochState.acnt
HasPParams-EpochState : HasPParams EpochState
HasPParams-EpochState .PParamsOf = PParamsOf ∘ EnactStateOf
HasRatifyState-EpochState : HasRatifyState EpochState
HasRatifyState-EpochState .RatifyStateOf = EpochState.fut
HasPState-EpochState : HasPState EpochState
HasPState-EpochState .PStateOf = PStateOf ∘ CertStateOf ∘ LStateOf
PoolDelegatedStake : Type
PoolDelegatedStake = KeyHash ⇀ Coin
record NewEpochState : Type where
field
lastEpoch : Epoch
epochState : EpochState
ru : Maybe RewardUpdate
pd : PoolDelegatedStake
record HasNewEpochState {a} (A : Type a) : Type a where
field NewEpochStateOf : A → NewEpochState
open HasNewEpochState ⦃...⦄ public
record HasLastEpoch {a} (A : Type a) : Type a where field LastEpochOf : A → Epoch
open HasLastEpoch ⦃...⦄ public
instance
HasLastEpoch-NewEpochState : HasLastEpoch NewEpochState
HasLastEpoch-NewEpochState .LastEpochOf = NewEpochState.lastEpoch
HasEpochState-NewEpochState : HasEpochState NewEpochState
HasEpochState-NewEpochState .EpochStateOf = NewEpochState.epochState
HasEnactState-NewEpochState : HasEnactState NewEpochState
HasEnactState-NewEpochState .EnactStateOf = EnactStateOf ∘ EpochStateOf
Hastreasury-NewEpochState : HasTreasury NewEpochState
Hastreasury-NewEpochState .TreasuryOf = TreasuryOf ∘ EpochStateOf
HasLState-NewEpochState : HasLState NewEpochState
HasLState-NewEpochState .LStateOf = LStateOf ∘ EpochStateOf
HasGovState-NewEpochState : HasGovState NewEpochState
HasGovState-NewEpochState .GovStateOf = GovStateOf ∘ LStateOf
HasCertState-NewEpochState : HasCertState NewEpochState
HasCertState-NewEpochState .CertStateOf = CertStateOf ∘ LStateOf
HasDReps-NewEpochState : HasDReps NewEpochState
HasDReps-NewEpochState .DRepsOf = DRepsOf ∘ CertStateOf
HasRewards-NewEpochState : HasRewards NewEpochState
HasRewards-NewEpochState .RewardsOf = RewardsOf ∘ CertStateOf
HasPParams-NewEpochState : HasPParams NewEpochState
HasPParams-NewEpochState .PParamsOf = PParamsOf ∘ EpochStateOf
unquoteDecl HasCast-EpochState HasCast-NewEpochState = derive-HasCast
( (quote EpochState , HasCast-EpochState)
∷ [ (quote NewEpochState , HasCast-NewEpochState)])
toRwdAddr : Credential → RwdAddr
toRwdAddr x = record { net = NetworkId ; stake = x }
getStakeCred : TxOut → Maybe Credential
getStakeCred (a , _ , _ , _) = stakeCred a
open GovActionState using (returnAddr)
createRUpd : ℕ → BlocksMade → EpochState → Coin → RewardUpdate
createRUpd slotsPerEpoch b es total =
record { Δt = Δt₁
; Δr = 0 - Δr₁ + Δr₂
; Δf = 0 - pos feeSS
; rs = rs
; flowConservation = flowConservation
; Δt-nonnegative = Δt-nonneg
; Δf-nonpositive = Δf-nonpos
}
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)
lemmaFlow : ∀ (t₁ r₁ f z : ℤ)
→ (t₁ ℤ.+ (0 ℤ.- r₁ ℤ.+ ((f ℤ.+ r₁ ℤ.- t₁) ℤ.- z)) ℤ.+ (0 ℤ.- f) ℤ.+ z) ≡ 0
lemmaFlow = solve-∀
flowConservation = lemmaFlow Δt₁ Δr₁ (pos feeSS) (pos (∑[ c ← rs ] c))
÷₀-0≤⇒0≤ : ∀ (x y : ℚ) → 0 ≤ x → 0 ≤ y → 0 ≤ (x ÷₀ y)
÷₀-0≤⇒0≤ x y 0≤x 0≤y with y ≟ 0
... | (yes y≡0) = nonNegative⁻¹ 0
... | (no y≢0) = ÷-0≤⇒0≤ x y {{≢-nonZero y≢0}} 0≤x 0≤y
η-nonneg : 0 ≤ η
η-nonneg = ÷₀-0≤⇒0≤ _ _ (fromℕ-0≤ blocksMade)
(*-0≤⇒0≤ _ _
(fromℕ-0≤ slotsPerEpoch)
(nonNegative⁻¹ ActiveSlotCoeff {{pos⇒nonNeg ActiveSlotCoeff}}))
min1η-nonneg : 0 ≤ 1 ⊓ η
min1η-nonneg = ⊓-glb (nonNegative⁻¹ 1) η-nonneg
Δr₁-nonneg : 0 ≤ Δr₁
Δr₁-nonneg = 0≤⇒0≤floor _
(*-0≤⇒0≤ (1 ⊓ η * ρ) (fromℕ reserves)
(UnitInterval-*-0≤ (1 ⊓ η) (prevPp .PParams.monetaryExpansion) min1η-nonneg)
(fromℕ-0≤ reserves))
rewardPot-nonneg : 0 ≤ rewardPot
rewardPot-nonneg = +-mono-≤ (nonNegative⁻¹ℤ (pos feeSS)) Δr₁-nonneg
Δt-nonneg : 0 ≤ Δt₁
Δt-nonneg = 0≤⇒0≤floor _
(UnitInterval-*-0≤ (fromℤ rewardPot) (prevPp .PParams.treasuryCut)
(fromℤ-0≤ rewardPot rewardPot-nonneg))
Δf-nonpos : (0 - pos feeSS) ≤ 0
Δf-nonpos = begin
0 - pos feeSS ≡⟨ +-identityˡ _ ⟩
ℤ.- pos feeSS ≤⟨ neg-mono-≤ (ℤ.+≤+ z≤n) ⟩
0 ∎
where open ≤-Reasoning
applyRUpd : RewardUpdate → EpochState → EpochState
applyRUpd rewardUpdate
$\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#7892}{\htmlId{7892}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7903}{\htmlId{7903}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Specification.Epoch.html#7919}{\htmlId{7919}{\htmlClass{Bound}{\text{ss}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#7930}{\htmlId{7930}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7937}{\htmlId{7937}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7944}{\htmlId{7944}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7955}{\htmlId{7955}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Specification.Epoch.html#7974}{\htmlId{7974}{\htmlClass{Bound}{\text{govSt}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#7990}{\htmlId{7990}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8003}{\htmlId{8003}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8017}{\htmlId{8017}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#8030}{\htmlId{8030}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8039}{\htmlId{8039}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
\\ \,\href{Ledger.Conway.Specification.Epoch.html#8057}{\htmlId{8057}{\htmlClass{Bound}{\text{es}}}}\,
\\ \,\href{Ledger.Conway.Specification.Epoch.html#8064}{\htmlId{8064}{\htmlClass{Bound}{\text{fut}}}}\,
\end{pmatrix}$ =
$\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3279}{\htmlId{8082}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{8090}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#76}{\htmlId{8091}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#7892}{\htmlId{8095}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8104}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6263}{\htmlId{8106}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8109}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#76}{\htmlId{8111}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#8477}{\htmlId{8115}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{8123}{\htmlClass{Symbol}{\text{)}}}\,
\\ \,\href{Prelude.html#3279}{\htmlId{8131}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{8139}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#76}{\htmlId{8140}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#7903}{\htmlId{8144}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8153}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6266}{\htmlId{8155}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{8157}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Specification.Epoch.html#7919}{\htmlId{8165}{\htmlClass{Bound}{\text{ss}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#7930}{\htmlId{8176}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3279}{\htmlId{8183}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{8191}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#76}{\htmlId{8192}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#7937}{\htmlId{8196}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8201}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6269}{\htmlId{8203}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{8205}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7944}{\htmlId{8209}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7955}{\htmlId{8220}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Specification.Epoch.html#7974}{\htmlId{8238}{\htmlClass{Bound}{\text{govSt}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#7990}{\htmlId{8254}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8003}{\htmlId{8267}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8017}{\htmlId{8281}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2046}{\htmlId{8289}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#8409}{\htmlId{8292}{\htmlClass{Function}{\text{regRU}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#8030}{\htmlId{8302}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8039}{\htmlId{8311}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
\\ \,\href{Ledger.Conway.Specification.Epoch.html#8057}{\htmlId{8326}{\htmlClass{Bound}{\text{es}}}}\,
\\ \,\href{Ledger.Conway.Specification.Epoch.html#8064}{\htmlId{8333}{\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')
open RwdAddr using (stake)
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)
opaque
mkStakeDistrs : Snapshot → GovState → Deposits → VoteDelegs → StakeDistrs
mkStakeDistrs ss govSt ds delegations .StakeDistrs.stakeDistr =
aggregateBy ∣ delegations ∣ (Snapshot.stake ss ∪⁺ gaDepositStake govSt ds)
private variable
e lastEpoch : Epoch
fut fut' : RatifyState
poolReapState : PoolReapState
eps eps' eps'' : EpochState
ls : LState
es₀ : EnactState
mark set go : Snapshot
feeSS : Fees
lstate : LState
ss ss' : Snapshots
ru : RewardUpdate
mru : Maybe RewardUpdate
pd : PoolDelegatedStake
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{11257}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{11258}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{11261}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#10680}{\htmlId{11266}{\htmlClass{Function}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{11273}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#6068}{\htmlId{11278}{\htmlClass{Function}{\text{mapValues}}}}\, \,\htmlId{11288}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{11289}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11291}{\htmlClass{Field Operator}{\text{+\_}}}}\,\,\htmlId{11293}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{11295}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#1530}{\htmlId{11296}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4193}{\htmlId{11304}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{11310}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{11312}{\htmlClass{Function Operator}{\text{else}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#1530}{\htmlId{11317}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4193}{\htmlId{11325}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{11331}{\htmlClass{Symbol}{\text{)}}}\,
\\ \,\href{Ledger.Conway.Specification.Certs.html#1445}{\htmlId{11341}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4193}{\htmlId{11353}{\htmlClass{Function}{\text{gState}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{11360}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#1367}{\htmlId{11362}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{11370}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#484}{\htmlId{11371}{\htmlClass{Field}{\text{EnactState.cc}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#10350}{\htmlId{11385}{\htmlClass{Function}{\text{es}}}}\,\,\htmlId{11387}{\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
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#12762}{\htmlId{13308}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{13313}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{13317}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut'
→ ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
→ _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12789}{\htmlId{13402}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12672}{\htmlId{13412}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4393}{\htmlId{13419}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#9647}{\htmlId{13428}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4501}{\htmlId{13433}{\htmlClass{Field}{\text{PStateOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#9647}{\htmlId{13442}{\htmlClass{Generalizable}{\text{ls}}}}\, \end{pmatrix}$ ⇀⦇ e ,POOLREAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12686}{\htmlId{13465}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12709}{\htmlId{13476}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12715}{\htmlId{13484}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12723}{\htmlId{13494}{\htmlClass{Bound}{\text{pState'}}}}\, \end{pmatrix}$
────────────────────────────────
_ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12672}{\htmlId{13555}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9738}{\htmlId{13562}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9647}{\htmlId{13567}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9661}{\htmlId{13572}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9560}{\htmlId{13578}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12797}{\htmlId{13599}{\htmlClass{Bound}{\text{acnt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9741}{\htmlId{13608}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12686}{\htmlId{13616}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12765}{\htmlId{13627}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12772}{\htmlId{13638}{\htmlClass{Bound}{\text{dState''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12723}{\htmlId{13649}{\htmlClass{Bound}{\text{pState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12781}{\htmlId{13659}{\htmlClass{Bound}{\text{gState'}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12762}{\htmlId{13675}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9564}{\htmlId{13680}{\htmlClass{Generalizable}{\text{fut'}}}}\, \end{pmatrix}$
opaque
calculatePoolDelegatedStake : Snapshot → PoolDelegatedStake
calculatePoolDelegatedStake ss =
sd ∣ dom (ss .poolParameters)
where
open Snapshot
sd : KeyHash ⇀ Coin
sd = aggregate₊ ((stakeCredentialsPerPool ∘ʳ (ss .stake ˢ)) ᶠˢ)
where mutual
stakeCredentialsPerPool : Rel KeyHash Credential
stakeCredentialsPerPool = (ss .delegations ˢ) ⁻¹ʳ
_⁻¹ʳ : {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
data
_⊢_⇀⦇_,NEWEPOCH⦈_ : ⊤ → NewEpochState → Epoch → NewEpochState → Type
where
NEWEPOCH-New : let
eps' = applyRUpd ru eps
$\begin{pmatrix} \,\htmlId{14903}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#14907}{\htmlId{14907}{\htmlClass{Bound}{\text{ss}}}}\, \\ \,\htmlId{14912}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{14916}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{14920}{\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#9540}{\htmlId{15109}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9617}{\htmlId{15121}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{15127}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#9759}{\htmlId{15132}{\htmlClass{Generalizable}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9806}{\htmlId{15137}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#9538}{\htmlId{15160}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9626}{\htmlId{15164}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{15172}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#14940}{\htmlId{15182}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$
NEWEPOCH-Not-New :
∙ e ≢ lastEpoch + 1
────────────────────────────────
_ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#9540}{\htmlId{15285}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9617}{\htmlId{15297}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9779}{\htmlId{15303}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9806}{\htmlId{15309}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#9540}{\htmlId{15332}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9617}{\htmlId{15344}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9779}{\htmlId{15350}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9806}{\htmlId{15356}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$
NEWEPOCH-No-Reward-Update : let
$\begin{pmatrix} \,\htmlId{15404}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#15408}{\htmlId{15408}{\htmlClass{Bound}{\text{ss}}}}\, \\ \,\htmlId{15413}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{15417}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{15421}{\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#9540}{\htmlId{15607}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9617}{\htmlId{15619}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{15625}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9806}{\htmlId{15635}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#9538}{\htmlId{15658}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9621}{\htmlId{15662}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{15669}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#15440}{\htmlId{15679}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$