Skip to content

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

  inductive
  constructor ⟦_,_,_,_⟧ᵖ

  field
    utxoSt     : UTxOState   -- utxo state
    acnt       : Acnt        -- accounting
    dState     : DState      -- delegation state
    pState     : PState      -- pool state

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#778}{\htmlId{2074}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{2081}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4480}{\htmlId{2082}{\htmlClass{Field}{\text{voteDelegs}}}}\,
      \\ \,\href{Ledger.Conway.Specification.PoolReap.html#778}{\htmlId{2101}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{2108}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4510}{\htmlId{2109}{\htmlClass{Field}{\text{stakeDelegs}}}}\, \,\href{Axiom.Set.Map.html#17850}{\htmlId{2121}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1349}{\htmlId{2124}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#17850}{\htmlId{2132}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
      \\ \,\href{Ledger.Conway.Specification.PoolReap.html#778}{\htmlId{2142}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{2149}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4541}{\htmlId{2150}{\htmlClass{Field}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{2158}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1647}{\htmlId{2161}{\htmlClass{Bound}{\text{refunds}}}}\,
      \end{pmatrix}$

    pState' =
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.PoolReap.html#827}{\htmlId{2200}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{2207}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4604}{\htmlId{2208}{\htmlClass{Field}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2214}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1349}{\htmlId{2216}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2224}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
      \\ \,\href{Ledger.Conway.Specification.PoolReap.html#827}{\htmlId{2234}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{2241}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4626}{\htmlId{2242}{\htmlClass{Field}{\text{fPools}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2249}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1349}{\htmlId{2251}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2259}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
      \\ \,\href{Ledger.Conway.Specification.PoolReap.html#827}{\htmlId{2269}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{2276}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4648}{\htmlId{2277}{\htmlClass{Field}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2286}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.PoolReap.html#1349}{\htmlId{2288}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2296}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
      \end{pmatrix}$

    in
    ────────────────────────────────
    _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.PoolReap.html#692}{\htmlId{2361}{\htmlClass{Function}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#735}{\htmlId{2370}{\htmlClass{Function}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#778}{\htmlId{2377}{\htmlClass{Function}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#827}{\htmlId{2386}{\htmlClass{Function}{\text{pState}}}}\, \end{pmatrix}$ ⇀⦇ e ,POOLREAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.PoolReap.html#1908}{\htmlId{2413}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#1989}{\htmlId{2423}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#2056}{\htmlId{2431}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.PoolReap.html#2182}{\htmlId{2441}{\htmlClass{Bound}{\text{pState'}}}}\, \end{pmatrix}$