Skip to content

The POOLREAP Transition System

The pool reap transition system is responsible for removing pools slated for retirement in the given epoch.

In Dijkstra, pool registration deposits are tracked as part of pool state (i.e., PState).

{-# OPTIONS --safe #-}
open import Ledger.Dijkstra.Specification.Transaction
module Ledger.Dijkstra.Specification.PoolReap
  (txs : _) (open TransactionStructure txs)
  where
open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Certs govStructure

record PoolReapState : Type where
  constructor ⟦_,_,_⟧ᵖ
  field
    acnt    : Acnt
    dState  : DState
    pState  : PState

instance
  unquoteDecl HasCast-PoolReapState = derive-HasCast
                [ (quote PoolReapState , HasCast-PoolReapState) ]

private variable
  e : Epoch
  treasury reserves : Coin
  pools fPools : Pools
  retiring : KeyHash ⇀ Epoch
  depositsᵖ : KeyHash ⇀ Coin
  voteDelegs : VoteDelegs
  stakeDelegs : StakeDelegs
  rewards : Rewards
  depositsᵈ : Credential ⇀ Coin

open StakePoolParams using (rewardAccount)

data _⊢_⇀⦇_,POOLREAP⦈_ : ⊤ → PoolReapState → Epoch → PoolReapState → Type where
  POOLREAP :
    let
        retired : ℙ KeyHash
        retired = retiring ⁻¹ e

        rewardAccounts : KeyHash ⇀ Credential
        rewardAccounts = mapValues rewardAccount (pools ∣ retired)

        rewardAccounts' : Credential ⇀ Coin
        rewardAccounts' = aggregateBy (rewardAccounts ˢ) depositsᵖ

        refunds : Credential ⇀ Coin
        refunds = rewardAccounts' ∣ dom (rewards)

        unclaimed : Coin
        unclaimed = getCoin (rewardAccounts' ∣ dom (rewards) ᶜ)
    in
      ────────────────────────────────
      _ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1008}{\htmlId{1905}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1017}{\htmlId{1916}{\htmlClass{Generalizable}{\text{reserves}}}}\, \end{pmatrix} \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1116}{\htmlId{1931}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1142}{\htmlId{1944}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1170}{\htmlId{1958}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1190}{\htmlId{1968}{\htmlClass{Generalizable}{\text{depositsᵈ}}}}\, \end{pmatrix} \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1035}{\htmlId{1984}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1041}{\htmlId{1992}{\htmlClass{Generalizable}{\text{fPools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1058}{\htmlId{2001}{\htmlClass{Generalizable}{\text{retiring}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1087}{\htmlId{2012}{\htmlClass{Generalizable}{\text{depositsᵖ}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ e ,POOLREAP⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1008}{\htmlId{2046}{\htmlClass{Generalizable}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{2055}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1764}{\htmlId{2057}{\htmlClass{Bound}{\text{unclaimed}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1017}{\htmlId{2069}{\htmlClass{Generalizable}{\text{reserves}}}}\, \end{pmatrix} \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1116}{\htmlId{2084}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1142}{\htmlId{2097}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \,\href{Axiom.Set.Map.html#17850}{\htmlId{2109}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1390}{\htmlId{2112}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#17850}{\htmlId{2120}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1170}{\htmlId{2124}{\htmlClass{Generalizable}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{2132}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1677}{\htmlId{2135}{\htmlClass{Bound}{\text{refunds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1190}{\htmlId{2145}{\htmlClass{Generalizable}{\text{depositsᵈ}}}}\, \end{pmatrix} \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1035}{\htmlId{2161}{\htmlClass{Generalizable}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2167}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1390}{\htmlId{2169}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2177}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1041}{\htmlId{2181}{\htmlClass{Generalizable}{\text{fPools}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2188}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1390}{\htmlId{2190}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2198}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1058}{\htmlId{2202}{\htmlClass{Generalizable}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2211}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1390}{\htmlId{2213}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2221}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1087}{\htmlId{2225}{\htmlClass{Generalizable}{\text{depositsᵖ}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2235}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.PoolReap.html#1390}{\htmlId{2237}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2245}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix} \end{pmatrix}$