Epoch Boundary¶

This section is part of the Ledger.Conway.Epoch module of the formal ledger specification

{-# 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.Abstract
open import Ledger.Conway.Transaction
open import Ledger.Conway.Types.Numeric.UnitInterval

open Number number renaming (fromNat to fromℕ)

module Ledger.Conway.Epoch
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Conway.Certs govStructure
open import Ledger.Conway.Enact govStructure
open import Ledger.Conway.Gov txs
open import Ledger.Conway.Ledger txs abs
open import Ledger.Conway.Ratify txs
open import Ledger.Conway.Rewards txs abs
open import Ledger.Conway.Utxo txs abs

Definitions for the EPOCH and NEWEPOCH transition systems¶


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


record NewEpochState : Type where
  field
    lastEpoch   : Epoch
    epochState  : EpochState
    ru          : Maybe RewardUpdate

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

  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

  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)

Figure 'RewardUpdate-Creation' defines the function createRUpd which creates a RewardUpdate, i.e.the net flow of Ada due to paying out rewards after an epoch. Relevant quantities are:

prevPp: Previous protocol parameters, which correspond to the parameters during the epoch for which we are creating rewards.
ActiveSlotCoeff: Global constant, equal to the probability that a party holding all the stake will be selected to be a leader for given slot. Equals \(1/20\) during the Shelley era on the Cardano Mainnet.
Δr₁: Ada taken out of the reserves for paying rewards, as determined by the monetaryExpansion protocol parameter.
rewardPot: Total amount of coin available for rewards this epoch, as described in .
feeSS: The fee pot which, together with the reserves, funds the rewardPot. We use the fee pot that accumulated during the epoch for which we now compute block production rewards. Note that fees are not explicitly removed from any account: the fees come from transactions paying them and are accounted for whenever transactions are processed.
Δt₁: The proportion of the reward pot that will move to the treasury, as determined by the treasuryCut protocol parameter. The remaining pot is called the R, just as in .
pstakego: Stake distribution used for calculating the rewards. This is the oldest stake distribution snapshot, labeled go.
rs: The rewards, as calculated by the function reward.
Δr₂: The difference between the maximal amount of rewards that could have been paid out if pools had been optimal, and the actual rewards paid out. This difference is returned to the reserves.
÷₀: Division operator that returns zero when the denominator is zero.

RewardUpdate Creation¶

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)

    -- Proofs
    -- Note: Overloading of + and - seems to interfere with
    -- the ring solver.
    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

Untitled Section¶

applyRUpd : RewardUpdate → EpochState → EpochState
applyRUpd rewardUpdate
  $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#9780}{\htmlId{9780}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9791}{\htmlId{9791}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix}
  \\ \,\href{Ledger.Conway.Epoch.html#9807}{\htmlId{9807}{\htmlClass{Bound}{\text{ss}}}}\,
  \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#9818}{\htmlId{9818}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9825}{\htmlId{9825}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9832}{\htmlId{9832}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9843}{\htmlId{9843}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
    \\ \,\href{Ledger.Conway.Epoch.html#9862}{\htmlId{9862}{\htmlClass{Bound}{\text{govSt}}}}\,
    \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#9878}{\htmlId{9878}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9891}{\htmlId{9891}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9905}{\htmlId{9905}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Epoch.html#9918}{\htmlId{9918}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9927}{\htmlId{9927}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
  \\ \,\href{Ledger.Conway.Epoch.html#9945}{\htmlId{9945}{\htmlClass{Bound}{\text{es}}}}\,
  \\ \,\href{Ledger.Conway.Epoch.html#9952}{\htmlId{9952}{\htmlClass{Bound}{\text{fut}}}}\,
  \end{pmatrix}$ =
  $\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3175}{\htmlId{9970}{\htmlClass{Function}{\text{posPart}}}}\, (\,\href{Ledger.Conway.Epoch.html#393}{\htmlId{9979}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Epoch.html#9780}{\htmlId{9983}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9992}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Rewards.html#17463}{\htmlId{9994}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9997}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Epoch.html#393}{\htmlId{9999}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Epoch.html#10365}{\htmlId{10003}{\htmlClass{Function}{\text{unregRU'}}}}\,)
    \\ \,\href{Prelude.html#3175}{\htmlId{10019}{\htmlClass{Function}{\text{posPart}}}}\, (\,\href{Ledger.Conway.Epoch.html#393}{\htmlId{10028}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Epoch.html#9791}{\htmlId{10032}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{10041}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Rewards.html#17466}{\htmlId{10043}{\htmlClass{Function}{\text{Δr}}}}\,) \end{pmatrix}
  \\ \,\href{Ledger.Conway.Epoch.html#9807}{\htmlId{10053}{\htmlClass{Bound}{\text{ss}}}}\,
  \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#9818}{\htmlId{10064}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3175}{\htmlId{10071}{\htmlClass{Function}{\text{posPart}}}}\, (\,\href{Ledger.Conway.Epoch.html#393}{\htmlId{10080}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Epoch.html#9825}{\htmlId{10084}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{10089}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Rewards.html#17469}{\htmlId{10091}{\htmlClass{Function}{\text{Δf}}}}\,) \\ \,\href{Ledger.Conway.Epoch.html#9832}{\htmlId{10097}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9843}{\htmlId{10108}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
    \\ \,\href{Ledger.Conway.Epoch.html#9862}{\htmlId{10126}{\htmlClass{Bound}{\text{govSt}}}}\,
    \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#9878}{\htmlId{10142}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9891}{\htmlId{10155}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9905}{\htmlId{10169}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#1854}{\htmlId{10177}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Epoch.html#10297}{\htmlId{10180}{\htmlClass{Function}{\text{regRU}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Epoch.html#9918}{\htmlId{10190}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#9927}{\htmlId{10199}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
  \\ \,\href{Ledger.Conway.Epoch.html#9945}{\htmlId{10214}{\htmlClass{Bound}{\text{es}}}}\,
  \\ \,\href{Ledger.Conway.Epoch.html#9952}{\htmlId{10221}{\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')

Functions for computing stake distributions¶

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 → (Credential ⇀ VDeleg) → StakeDistrs
  mkStakeDistrs ss govSt ds delegations .StakeDistrs.stakeDistr =
    aggregateBy ∣ delegations ∣ (Snapshot.stake ss ∪⁺ gaDepositStake govSt ds)

private variable
  nes nes' : NewEpochState
  e lastEpoch : Epoch
  fut fut' : RatifyState
  eps eps' eps'' : EpochState
  ls : LState
  acnt : Acnt
  es₀ : EnactState
  mark set go : Snapshot
  feeSS : Coin
  lstate : LState
  ss ss' : Snapshots
  ru : RewardUpdate
  mru : Maybe RewardUpdate

Untitled Section¶

data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Type where

Figure 'EPOCH-transition-system' defines the EPOCH transition rule. Currently, this incorporates logic that was previously handled by POOLREAP in the Shelley specification ; POOLREAP is not implemented here.

The EPOCH rule now also needs to invoke RATIFIES and properly deal with its results by carrying out each of the following tasks.

Pay out all the enacted treasury withdrawals.
Remove expired and enacted governance actions & refund deposits.
If is empty, increment the activity counter for DReps.
Remove all hot keys from the constitutional committee delegation map that do not belong to currently elected members.
Apply the resulting enact state from the previous epoch boundary and store the resulting enact state .

EPOCH transition system¶

  EPOCH : let

      open LState ls
      open CertState certState
      open RatifyState fut hiding (es)
      open UTxOState
      open PState; open DState; open GState
      open Acnt; open EnactState; open GovActionState

      esW               = RatifyState.es fut
      es                = record esW { withdrawals = ∅ }
      tmpGovSt          = filter (λ x → proj₁ x ∉ mapˢ proj₁ removed) govSt
      orphans           = fromList (getOrphans es tmpGovSt)
      removed'          = removed ∪ orphans
      removedGovActions = flip concatMapˢ removed' λ (gaid , gaSt) →
        mapˢ (returnAddr gaSt ,_) ((utxoSt .deposits ∣ ❴ GovActionDeposit gaid ❵) ˢ)
      govActionReturns = aggregate₊ (mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ)

      trWithdrawals   = esW .withdrawals
      totWithdrawals  = ∑[ x ← trWithdrawals ] x

      retired    = (pState .retiring) ⁻¹ e
      payout     = govActionReturns ∪⁺ trWithdrawals
      refunds    = pullbackMap payout toRwdAddr (dom (dState .rewards))
      unclaimed  = getCoin payout - getCoin refunds

      govSt' = filter (λ x → proj₁ x ∉ mapˢ proj₁ removed') govSt

      dState' = $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5218}{\htmlId{14034}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{14041}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Certs.html#3883}{\htmlId{14042}{\htmlClass{Field}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5218}{\htmlId{14055}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{14062}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Certs.html#3922}{\htmlId{14063}{\htmlClass{Field}{\text{stakeDelegs}}}}\, \\  \,\href{Ledger.Conway.Certs.html#5218}{\htmlId{14078}{\htmlClass{Function}{\text{dState}}}}\, \,\htmlId{14085}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Certs.html#3962}{\htmlId{14086}{\htmlClass{Field}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#1854}{\htmlId{14094}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Epoch.html#13830}{\htmlId{14097}{\htmlClass{Bound}{\text{refunds}}}}\, \end{pmatrix}$

      pState' = $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5238}{\htmlId{14126}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{14133}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Certs.html#4501}{\htmlId{14134}{\htmlClass{Field}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{14140}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Epoch.html#13734}{\htmlId{14142}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{14150}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5238}{\htmlId{14154}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{14161}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Certs.html#4538}{\htmlId{14162}{\htmlClass{Field}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{14171}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Epoch.html#13734}{\htmlId{14173}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{14181}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

      gState' = $\begin{pmatrix} (\,\href{Class.ToBool.html#389}{\htmlId{14205}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4703}{\htmlId{14208}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Epoch.html#13955}{\htmlId{14213}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#389}{\htmlId{14220}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#6068}{\htmlId{14225}{\htmlClass{Function}{\text{mapValues}}}}\, (\,\htmlId{14236}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{14238}{\htmlClass{Field Operator}{\text{+\_}}}}\,) (\,\href{Ledger.Conway.Certs.html#5258}{\htmlId{14243}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{14250}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Certs.html#4812}{\htmlId{14251}{\htmlClass{Field}{\text{dreps}}}}\,) \,\href{Class.ToBool.html#389}{\htmlId{14258}{\htmlClass{Function Operator}{\text{else}}}}\, (\,\href{Ledger.Conway.Certs.html#5258}{\htmlId{14264}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{14271}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Certs.html#4812}{\htmlId{14272}{\htmlClass{Field}{\text{dreps}}}}\,)
                , \,\href{Ledger.Conway.Certs.html#5258}{\htmlId{14298}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{14305}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Certs.html#4835}{\htmlId{14306}{\htmlClass{Field}{\text{ccHotKeys}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{14316}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Enact.html#2707}{\htmlId{14318}{\htmlClass{Function}{\text{ccCreds}}}}\, (\,\href{Ledger.Conway.Epoch.html#13163}{\htmlId{14327}{\htmlClass{Bound}{\text{es}}}}\, \,\htmlId{14330}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Enact.html#1911}{\htmlId{14331}{\htmlClass{Field}{\text{cc}}}}\,) \end{pmatrix}$

      certState' : CertState
      certState' = $\begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#14022}{\htmlId{14388}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#14114}{\htmlId{14398}{\htmlClass{Bound}{\text{pState'}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#14192}{\htmlId{14408}{\htmlClass{Bound}{\text{gState'}}}}\, \end{pmatrix}$

      utxoSt' = $\begin{pmatrix} \,\href{Ledger.Conway.Ledger.html#1719}{\htmlId{14437}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{14444}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Utxo.html#4779}{\htmlId{14445}{\htmlClass{Field}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Ledger.html#1719}{\htmlId{14452}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{14459}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Utxo.html#4801}{\htmlId{14460}{\htmlClass{Field}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Ledger.html#1719}{\htmlId{14467}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{14474}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Utxo.html#4823}{\htmlId{14475}{\htmlClass{Field}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{14484}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#519}{\htmlId{14486}{\htmlClass{Function}{\text{mapˢ}}}}\, (\,\href{Data.Product.Base.html#636}{\htmlId{14492}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Function.Base.html#1115}{\htmlId{14498}{\htmlClass{Function Operator}{\text{∘}}}}\, \,\href{Data.Product.Base.html#650}{\htmlId{14500}{\htmlClass{Field}{\text{proj₂}}}}\,) \,\href{Ledger.Conway.Epoch.html#13400}{\htmlId{14507}{\htmlClass{Bound}{\text{removedGovActions}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{14525}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{14529}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$

      acnt' = record acnt
        { treasury  = acnt .treasury ∸ totWithdrawals + utxoSt .donations + unclaimed }
    in
    record { currentEpoch = e
           ; stakeDistrs = mkStakeDistrs  (Snapshots.mark ss') govSt'
                                          (utxoSt' .deposits) (voteDelegs dState)
           ; treasury = acnt .treasury ; GState gState
           ; pools = pState .pools ; delegatees = dState .voteDelegs }
        ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#13163}{\htmlId{14975}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{14980}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{14984}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut'
      → ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
    ────────────────────────────────
    _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#11736}{\htmlId{15098}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11827}{\htmlId{15105}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11722}{\htmlId{15110}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11750}{\htmlId{15115}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11667}{\htmlId{15121}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#14540}{\htmlId{15150}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11830}{\htmlId{15158}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#14425}{\htmlId{15166}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#13955}{\htmlId{15176}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#14344}{\htmlId{15185}{\htmlClass{Bound}{\text{certState'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Epoch.html#13163}{\htmlId{15200}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11671}{\htmlId{15205}{\htmlClass{Generalizable}{\text{fut'}}}}\, \end{pmatrix}$

NEWEPOCH transition system¶

data

  _⊢_⇀⦇_,NEWEPOCH⦈_ : ⊤ → NewEpochState → Epoch → NewEpochState → Type

  where

  NEWEPOCH-New : let
      eps' = applyRUpd ru eps
    in
    ∙ e ≡ lastEpoch + 1
    ∙ _ ⊢ eps' ⇀⦇ e ,EPOCH⦈ eps''
      ────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#11647}{\htmlId{15576}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11692}{\htmlId{15588}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{15594}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Epoch.html#11848}{\htmlId{15599}{\htmlClass{Generalizable}{\text{ru}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#11645}{\htmlId{15622}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11701}{\htmlId{15626}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{15634}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$

  NEWEPOCH-Not-New :
    ∙ e ≢ lastEpoch + 1
      ────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#11647}{\htmlId{15741}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11692}{\htmlId{15753}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11868}{\htmlId{15759}{\htmlClass{Generalizable}{\text{mru}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#11647}{\htmlId{15783}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11692}{\htmlId{15795}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11868}{\htmlId{15801}{\htmlClass{Generalizable}{\text{mru}}}}\, \end{pmatrix}$

  NEWEPOCH-No-Reward-Update :
    ∙ e ≡ lastEpoch + 1
    ∙ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
      ────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#11647}{\htmlId{15945}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11692}{\htmlId{15957}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{15963}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Epoch.html#11645}{\htmlId{15991}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Epoch.html#11696}{\htmlId{15995}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{16002}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$