The POOLREAP Transition System
{-# 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
inductive
constructor ⟦_,_,_,_⟧ᵖ
field
utxoSt : UTxOState
acnt : Acnt
dState : DState
pState : PState
instance
unquoteDecl HasCast-PoolReapState = derive-HasCast
[ (quote PoolReapState , HasCast-PoolReapState) ]
HasDState-PoolReapState : HasDState PoolReapState
HasDState-PoolReapState .DStateOf = PoolReapState.dState
HasRewards-PoolReapState : HasRewards PoolReapState
HasRewards-PoolReapState .RewardsOf = RewardsOf ∘ DStateOf
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#819}{\htmlId{2344}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{2351}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4480}{\htmlId{2352}{\htmlClass{Field}{\text{voteDelegs}}}}\,
\\ \,\href{Ledger.Conway.Specification.PoolReap.html#819}{\htmlId{2371}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{2378}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4510}{\htmlId{2379}{\htmlClass{Field}{\text{stakeDelegs}}}}\, \,\href{Axiom.Set.Map.html#17850}{\htmlId{2391}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1619}{\htmlId{2394}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#17850}{\htmlId{2402}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Conway.Specification.PoolReap.html#819}{\htmlId{2412}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{2419}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4541}{\htmlId{2420}{\htmlClass{Field}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{2428}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1917}{\htmlId{2431}{\htmlClass{Bound}{\text{refunds}}}}\,
\end{pmatrix}$
pState' =
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.PoolReap.html#868}{\htmlId{2470}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{2477}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4604}{\htmlId{2478}{\htmlClass{Field}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2484}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1619}{\htmlId{2486}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2494}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Conway.Specification.PoolReap.html#868}{\htmlId{2504}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{2511}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4626}{\htmlId{2512}{\htmlClass{Field}{\text{fPools}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2519}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1619}{\htmlId{2521}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2529}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Conway.Specification.PoolReap.html#868}{\htmlId{2539}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{2546}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4648}{\htmlId{2547}{\htmlClass{Field}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2556}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1619}{\htmlId{2558}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2566}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\end{pmatrix}$
in
────────────────────────────────
_ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.PoolReap.html#733}{\htmlId{2631}{\htmlClass{Function}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#776}{\htmlId{2640}{\htmlClass{Function}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#819}{\htmlId{2647}{\htmlClass{Function}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#868}{\htmlId{2656}{\htmlClass{Function}{\text{pState}}}}\, \end{pmatrix}$ ⇀⦇ e ,POOLREAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.PoolReap.html#2178}{\htmlId{2683}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#2259}{\htmlId{2693}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#2326}{\htmlId{2701}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#2452}{\htmlId{2711}{\htmlClass{Bound}{\text{pState'}}}}\, \end{pmatrix}$