Pool Reaping Transition
{-# OPTIONS --safe #-}
open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction
module Ledger.Conway.Specification.PoolReap
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs)
where
open import Ledger.Prelude
open import Ledger.Conway.Specification.Utxo txs abs
open import Ledger.Conway.Specification.Certs govStructure
record PoolReapState : Type where
constructor ⟦_,_,_,_⟧ᵖ
field
utxoSt : UTxOState
acnt : Acnt
dState : DState
pState : PState
instance
unquoteDecl HasCast-PoolReapState = derive-HasCast
[ (quote PoolReapState , HasCast-PoolReapState) ]
private variable
e lastEpoch : Epoch
poolReapState : PoolReapState
data
_⊢_⇀⦇_,POOLREAP⦈_ : ⊤ → PoolReapState → Epoch → PoolReapState → Type where
POOLREAP : let
open PoolReapState poolReapState
open StakePoolParams
open UTxOState
open PState
open DState
open Acnt
open PParams
retired = pState .retiring ⁻¹ e
rewardAcnts : DepositPurpose ⇀ Credential
rewardAcnts =
mapKeys PoolDeposit $
mapValues rewardAccount $
pState .pools ∣ retired
rewardAcnts' : Credential ⇀ Coin
rewardAcnts' = aggregateBy (rewardAcnts ˢ) (utxoSt .deposits)
refunds : Credential ⇀ Coin
refunds = rewardAcnts' ∣ dom (dState .rewards)
mRefunds = rewardAcnts' ∣ dom (dState .rewards) ᶜ
unclaimed = getCoin mRefunds
retiredDeposits : ℙ DepositPurpose
retiredDeposits = mapˢ PoolDeposit retired
utxoSt' = record utxoSt { deposits = utxoSt .deposits ∣ retiredDeposits ᶜ }
acnt' = record acnt { treasury = acnt .treasury + unclaimed }
dState' =
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.PoolReap.html#671}{\htmlId{1967}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{1974}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4497}{\htmlId{1975}{\htmlClass{Field}{\text{voteDelegs}}}}\,
\\ \,\href{Ledger.Conway.Specification.PoolReap.html#671}{\htmlId{1994}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{2001}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4527}{\htmlId{2002}{\htmlClass{Field}{\text{stakeDelegs}}}}\, \,\href{Axiom.Set.Map.html#14509}{\htmlId{2014}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1242}{\htmlId{2017}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#14509}{\htmlId{2025}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Conway.Specification.PoolReap.html#671}{\htmlId{2035}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{2042}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4558}{\htmlId{2043}{\htmlClass{Field}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2046}{\htmlId{2051}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1540}{\htmlId{2054}{\htmlClass{Bound}{\text{refunds}}}}\,
\end{pmatrix}$
pState' = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.PoolReap.html#720}{\htmlId{2087}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{2094}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4621}{\htmlId{2095}{\htmlClass{Field}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{2101}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1242}{\htmlId{2103}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{2111}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#720}{\htmlId{2115}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{2122}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4643}{\htmlId{2123}{\htmlClass{Field}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{2132}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1242}{\htmlId{2134}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{2142}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$
in
────────────────────────────────
_ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.PoolReap.html#585}{\htmlId{2201}{\htmlClass{Function}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#628}{\htmlId{2210}{\htmlClass{Function}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#671}{\htmlId{2217}{\htmlClass{Function}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#720}{\htmlId{2226}{\htmlClass{Function}{\text{pState}}}}\, \end{pmatrix}$ ⇀⦇ e ,POOLREAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.PoolReap.html#1801}{\htmlId{2253}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#1882}{\htmlId{2263}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#1949}{\htmlId{2271}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#2075}{\htmlId{2281}{\htmlClass{Bound}{\text{pState'}}}}\, \end{pmatrix}$