Epoch Boundary

This module introduces the epoch boundary transition system and the related reward calculation.

{-# 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.Specification.Abstract
open import Ledger.Conway.Specification.Transaction
open import Ledger.Prelude.Numeric.UnitInterval using (fromUnitInterval; UnitInterval-*-0≤)

open Number number renaming (fromNat to fromℕ)

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

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

EPOCH and NEWEPOCH Transition System Types

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
  HasSnapshots-EpochState : HasSnapshots EpochState
  HasSnapshots-EpochState .SnapshotsOf = EpochState.ss

  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

  HasRatifyState-EpochState : HasRatifyState EpochState
  HasRatifyState-EpochState .RatifyStateOf = EpochState.fut

  HasPState-EpochState : HasPState EpochState
  HasPState-EpochState .PStateOf = PStateOf ∘ CertStateOf ∘ LStateOf

PoolDelegatedStake : Type
PoolDelegatedStake = KeyHash ⇀ Coin

record NewEpochState : Type where
  field
    lastEpoch   : Epoch
    bprev       : BlocksMade
    bcur        : BlocksMade
    epochState  : EpochState
    ru          : Maybe RewardUpdate
    pd          : PoolDelegatedStake

Differences with the Shelley Specification

The formal specification utilizes the type PoolDelegatedStake in lieu of the derived type PoolDistr (Figure 5, Shelley specification CVG19). The latter can be computed from the former by divinding the associated Coin to each KeyHash by the total stake in the map.

In addition, the formal specification omits the VRF key hashes in the codomain of PoolDelegatedStake as they are not implemented at the moment.

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

  HasEnactState-NewEpochState : HasEnactState NewEpochState
  HasEnactState-NewEpochState .EnactStateOf = EnactStateOf ∘ EpochStateOf

  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

  HasPParams-NewEpochState : HasPParams NewEpochState
  HasPParams-NewEpochState .PParamsOf = PParamsOf ∘ EpochStateOf

  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)

opaque

RewardUpdate

Computing RewardUpdate

This section defines the function createRUpd which creates a RewardUpdate, i.e. the net flow of Ada due to paying out rewards after an epoch:

  createRUpd : ℕ → BlocksMade → EpochState → Coin → RewardUpdate
  createRUpd slotsPerEpoch b es total =
    record  { Δt = Δt₁
            ; Δr =  - Δr₁ + Δr₂
            ; Δf =  - pos feeSS
            ; rs = rs

            ; flowConservation = flowConservation
            ; Δt-nonnegative = Δt-nonneg
            ; Δf-nonpositive = Δf-nonpos

            }
    where
      prevPp : PParams
      prevPp = PParamsOf es

      reserves : Reserves
      reserves = ReservesOf es

      pstakego : Snapshot
      pstakego = (SnapshotsOf es) .Snapshots.go

      feeSS : Fees
      feeSS = FeesOf (SnapshotsOf es)

      stake : Stake
      stake = StakeOf pstakego

      delegs : StakeDelegs
      delegs = StakeDelegsOf pstakego

      poolParams : Pools
      poolParams = PoolsOf pstakego

      blocksMade : ℕ
      blocksMade = ∑[ m ← b ] m

      ρ η τ : ℚ
      ρ = fromUnitInterval (prevPp .PParams.monetaryExpansion)
      η = fromℕ blocksMade ÷₀ (fromℕ slotsPerEpoch * ActiveSlotCoeff)
      τ = fromUnitInterval (prevPp .PParams.treasuryCut)

      Δr₁ rewardPot Δt₁ R : ℤ
      Δr₁ = floor ( ⊓ η * ρ * fromℕ reserves)
      rewardPot = pos feeSS + Δr₁
      Δt₁ = floor (fromℤ rewardPot * τ)
      R = rewardPot - Δt₁

      circulation : Coin
      circulation = total - reserves

      rs : Rewards
      rs = reward prevPp b (posPart R) poolParams stake delegs circulation

      Δr₂ : ℤ
      Δr₂ = R - pos (∑[ c ← rs ] c)

      -- Proofs
      -- Note: Overloading of + and - seems to interfere with
      -- the ring solver.
      lemmaFlow : ∀ (t₁ r₁ f z : ℤ)
        → (t₁ ℤ.+ ( ℤ.- r₁ ℤ.+ ((f ℤ.+ r₁ ℤ.- t₁) ℤ.- z)) ℤ.+ ( ℤ.- f) ℤ.+ z) ≡ 
      lemmaFlow = solve-∀
      flowConservation :
        let t₁ = Δt₁
            r₁ = Δr₁
            f  = pos feeSS
            z  = pos (∑[ c ← rs ] c)
         in
            (t₁ ℤ.+ ( ℤ.- r₁ ℤ.+ ((f ℤ.+ r₁ ℤ.- t₁) ℤ.- z)) ℤ.+ ( ℤ.- f) ℤ.+ z) ≡ 
      flowConservation = lemmaFlow Δt₁ Δr₁ (pos feeSS) (pos (∑[ c ← rs ] c))

      ÷₀-0≤⇒0≤ : ∀ (x y : ℚ) →  ≤ x →  ≤ y →  ≤ (x ÷₀ y)
      ÷₀-0≤⇒0≤ x y 0≤x 0≤y with y ≟ 
      ... | (yes y≡0) = nonNegative⁻¹ 
      ... | (no y≢0)  = ÷-0≤⇒0≤ x y {{≢-nonZero y≢0}} 0≤x 0≤y

      η-nonneg :  ≤ η
      η-nonneg = ÷₀-0≤⇒0≤ _ _ (fromℕ-0≤ blocksMade)
        (*-0≤⇒0≤ _ _
          (fromℕ-0≤ slotsPerEpoch)
          (nonNegative⁻¹ ActiveSlotCoeff {{pos⇒nonNeg ActiveSlotCoeff}}))

      min1η-nonneg :  ≤  ⊓ η
      min1η-nonneg = ⊓-glb (nonNegative⁻¹ ) η-nonneg

      Δr₁-nonneg :  ≤ Δr₁
      Δr₁-nonneg = 0≤⇒0≤floor _
        (*-0≤⇒0≤ ( ⊓ η * ρ) (fromℕ reserves)
          (UnitInterval-*-0≤ ( ⊓ η) (prevPp .PParams.monetaryExpansion) min1η-nonneg)
          (fromℕ-0≤ reserves))

      rewardPot-nonneg :  ≤ rewardPot
      rewardPot-nonneg = +-mono-≤ (nonNegative⁻¹ℤ (pos feeSS)) Δr₁-nonneg

      Δt-nonneg :  ≤ Δt₁
      Δt-nonneg = 0≤⇒0≤floor _
        (UnitInterval-*-0≤ (fromℤ rewardPot) (prevPp .PParams.treasuryCut)
          (fromℤ-0≤ rewardPot rewardPot-nonneg))

      Δf-nonpos : ( - pos feeSS) ≤ 
      Δf-nonpos = begin
           - pos feeSS ≡⟨ +-identityˡ _ ⟩
          ℤ.- pos feeSS ≤⟨ neg-mono-≤ (ℤ.+≤+ z≤n) ⟩
                       ∎
        where open ≤-Reasoning

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 Team18.

• 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 Team18.

• 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.

Applying RewardUpdate

This section defines the function applyRUpd, which applies a RewardUpdate to the EpochState.

applyRUpd : RewardUpdate → EpochState → EpochState
applyRUpd rewardUpdate $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12115}{\htmlId{12115}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12126}{\htmlId{12126}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix}
                       \\ \,\href{Ledger.Conway.Specification.Epoch.html#12163}{\htmlId{12163}{\htmlClass{Bound}{\text{ss}}}}\,
                       \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12195}{\htmlId{12195}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12202}{\htmlId{12202}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12209}{\htmlId{12209}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12220}{\htmlId{12220}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
                         \\ \,\href{Ledger.Conway.Specification.Epoch.html#12260}{\htmlId{12260}{\htmlClass{Bound}{\text{govSt}}}}\,
                         \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12297}{\htmlId{12297}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12310}{\htmlId{12310}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12324}{\htmlId{12324}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12337}{\htmlId{12337}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12346}{\htmlId{12346}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
                       \\ \,\href{Ledger.Conway.Specification.Epoch.html#12385}{\htmlId{12385}{\htmlClass{Bound}{\text{es}}}}\,
                       \\ \,\href{Ledger.Conway.Specification.Epoch.html#12413}{\htmlId{12413}{\htmlClass{Bound}{\text{fut}}}}\,
                       \end{pmatrix}$ = $\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3348}{\htmlId{12450}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{12458}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#316}{\htmlId{12459}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12115}{\htmlId{12463}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12472}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18185}{\htmlId{12474}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12477}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#316}{\htmlId{12479}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#13034}{\htmlId{12483}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{12491}{\htmlClass{Symbol}{\text{)}}}\,
                               \\ \,\href{Prelude.html#3348}{\htmlId{12526}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{12534}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#316}{\htmlId{12535}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12126}{\htmlId{12539}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12548}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18188}{\htmlId{12550}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{12552}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}
                             \\ \,\href{Ledger.Conway.Specification.Epoch.html#12163}{\htmlId{12587}{\htmlClass{Bound}{\text{ss}}}}\,
                             \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12195}{\htmlId{12625}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3348}{\htmlId{12632}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{12640}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#316}{\htmlId{12641}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12202}{\htmlId{12645}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12650}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18191}{\htmlId{12652}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{12654}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12209}{\htmlId{12658}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12220}{\htmlId{12669}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
                               \\ \,\href{Ledger.Conway.Specification.Epoch.html#12260}{\htmlId{12714}{\htmlClass{Bound}{\text{govSt}}}}\,
                               \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12297}{\htmlId{12757}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12310}{\htmlId{12770}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12324}{\htmlId{12784}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2046}{\htmlId{12792}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12966}{\htmlId{12795}{\htmlClass{Function}{\text{regRU}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12337}{\htmlId{12805}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12346}{\htmlId{12814}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
                             \\ \,\href{Ledger.Conway.Specification.Epoch.html#12385}{\htmlId{12856}{\htmlClass{Bound}{\text{es}}}}\,
                             \\ \,\href{Ledger.Conway.Specification.Epoch.html#12413}{\htmlId{12890}{\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

Stake Distributions

This section defines the functions calculatePoolDelegatedState, calculateVDelegDelegatedStake, and mkStakeDistrs, which calculates stake distributions for voting purposes.

open RwdAddr using (stake)
opaque

  calculatePoolDelegatedStake
    : Snapshot
    → PoolDelegatedStake
  calculatePoolDelegatedStake ss =
      -- Shelley spec: the output map must contain keys appearing in both
      -- sd and the pool parameters.
      sd ∣ dom (PoolsOf ss)
    where
      -- stake credentials delegating to each pool
      stakeCredentialsPerPool : Rel KeyHash Credential
      stakeCredentialsPerPool = (StakeDelegsOf ss ˢ) ⁻¹ʳ

      -- delegated stake per pool
      sd : KeyHash ⇀ Coin
      sd = aggregate₊ ((stakeCredentialsPerPool ∘ʳ (StakeOf ss ˢ)) ᶠˢ)

The function calculatePoolDelegatedState calculates the delegated stake to SPO{.AgdaFunction}s. This function is used both in the EPOCH rule (via calculatePoolDelegatedStateForVoting, see below) and in the NEWEPOCH rule.

  stakeFromGADeposits
    : GovState
    → UTxOState
    → Stake
  stakeFromGADeposits govSt utxoSt = aggregateBy
     (mapˢ (λ (gaid , addr) → (gaid , addr) , stake addr) govSt')
     (mapFromPartialFun (λ (gaid , _) → lookupᵐ? deposits (GovActionDeposit gaid)) govSt')
     where
       open UTxOState utxoSt

       govSt' : ℙ (GovActionID × RwdAddr)
       govSt' = mapˢ (map₂ returnAddr) (fromList govSt)

The function stakeFromGADeposits computes the stake pertaining to governance action deposits. It returns a map which, for each governance action, maps its returnAddr (as a staking credential) to the deposit.

  calculateVDelegDelegatedStake
    : Epoch
    → UTxOState
    → GovState
    → GState
    → DState
    → VDeleg ⇀ Coin
  calculateVDelegDelegatedStake currentEpoch utxoSt govSt gState dState
    = aggregate₊ (((activeVoteDelegs ˢ) ⁻¹ʳ
                  ∘ʳ (stakePerCredential ∪⁺ stakeFromGADeposits govSt utxoSt) ˢ) ᶠˢ)
    where
      open UTxOState utxoSt
      open DState dState
      open GState gState

      -- active DReps
      activeDReps : ℙ Credential
      activeDReps = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) dreps)

      -- active vote delegations
      activeVoteDelegs : VoteDelegs
      activeVoteDelegs = voteDelegs ∣^ ((mapˢ vDelegCredential activeDReps)
                                        ∪ ❴ vDelegNoConfidence ❵ ∪ ❴ vDelegAbstain ❵)

      -- stake per delegated credential
      stakePerCredential : Stake
      stakePerCredential = mapFromFun (λ c → cbalance (utxo ∣^' λ txout → getStakeCred txout ≡ just c))
                                      (dom activeVoteDelegs)

  calculatePoolDelegatedStakeForVoting
    : Snapshot
    → UTxOState
    → GovState
    → GState
    → DState
    → KeyHash ⇀ Coin
  calculatePoolDelegatedStakeForVoting ss utxoSt govSt gState dState
    = calculatePoolDelegatedStake ss ∪⁺ (stakeFromDeposits ∣ dom (PoolsOf ss))
    where
      stakeFromDeposits : KeyHash ⇀ Coin
      stakeFromDeposits = aggregate₊ (((StakeDelegsOf ss ˢ) ⁻¹ʳ
                                      ∘ʳ (stakeFromGADeposits govSt utxoSt ˢ)) ᶠˢ)

The function calculatePoolDelegatedStakeForVoting computes the delegated stake to SPOs that will be used for counting votes. It complements the result of calculatePoolDelegatedStake with the deposits made to governance actions.

Erratum

CIP-1694 specifies that deposits of governance actions should count towards the stake for voting purposes:

The deposit amount will be added to the deposit pot, similar to stake key deposits. It will also be counted towards the stake of the reward address it will be paid back to, to not reduce the submitter's voting power to vote on their own (and competing) actions.

While originally intended for DReps only, the Haskell implementation and the formal specification count deposits on governance actions towards the stake of SPOs as well.

  mkStakeDistrs
    : Snapshot
    → Epoch
    → UTxOState
    → GovState
    → GState
    → DState
    → StakeDistrs
  mkStakeDistrs ss currentEpoch utxoSt govSt gState dState =
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#14910}{\htmlId{17611}{\htmlClass{Function}{\text{calculateVDelegDelegatedStake}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17563}{\htmlId{17641}{\htmlClass{Bound}{\text{currentEpoch}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17576}{\htmlId{17654}{\htmlClass{Bound}{\text{utxoSt}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17583}{\htmlId{17661}{\htmlClass{Bound}{\text{govSt}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17589}{\htmlId{17667}{\htmlClass{Bound}{\text{gState}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17596}{\htmlId{17674}{\htmlClass{Bound}{\text{dState}}}}\,
    \\ \,\href{Ledger.Conway.Specification.Epoch.html#15932}{\htmlId{17687}{\htmlClass{Function}{\text{calculatePoolDelegatedStakeForVoting}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17560}{\htmlId{17724}{\htmlClass{Bound}{\text{ss}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17576}{\htmlId{17727}{\htmlClass{Bound}{\text{utxoSt}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17583}{\htmlId{17734}{\htmlClass{Bound}{\text{govSt}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17589}{\htmlId{17740}{\htmlClass{Bound}{\text{gState}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17596}{\htmlId{17747}{\htmlClass{Bound}{\text{dState}}}}\, \end{pmatrix}$

private variable
  e lastEpoch : Epoch
  fut fut' : RatifyState
  poolReapState : PoolReapState
  eps eps' eps'' : EpochState
  ls : LState
  es₀ : EnactState
  mark set go : Snapshot
  feeSS : Fees
  lstate : LState
  ss ss' : Snapshots
  ru : RewardUpdate
  mru : Maybe RewardUpdate
  pd : PoolDelegatedStake

EPOCH Transition System

The EPOCH transition has a few updates that are encapsulated in the following functions. We need these functions to bring them in scope for some proofs about EPOCH.

Helper Functions

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')

Update Functions

record EPOCH-Updates0 : Type where
  constructor EPOCHUpdates0
  field
    es             : EnactState
    govSt'         : GovState
    payout         : Withdrawals
    gState'        : GState
    utxoSt'        : UTxOState
    totWithdrawals : Coin

EPOCH-updates0 : RatifyState → LState → EPOCH-Updates0
EPOCH-updates0 fut ls =
    EPOCHUpdates0 es govSt' payout gState' utxoSt' totWithdrawals
  where
    open LState ls public
    open CertState certState using (gState) public
    open RatifyState fut renaming (es to esW)

    es : EnactState
    es = record esW { withdrawals = ∅ }

    tmpGovSt : GovState
    tmpGovSt = filter (λ x → proj₁ x ∉ mapˢ proj₁ removed) govSt

    orphans : ℙ (GovActionID × GovActionState)
    orphans  = fromList (getOrphans es tmpGovSt)

    removed' : ℙ (GovActionID × GovActionState)
    removed' = removed ∪ orphans

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

    removedGovActions : ℙ (RwdAddr × DepositPurpose × Coin)
    removedGovActions =
      flip concatMapˢ removed' λ (gaid , gaSt) →
        mapˢ
          (returnAddr gaSt ,_)
          ((DepositsOf utxoSt ∣ ❴ GovActionDeposit gaid ❵) ˢ)

    govActionReturns : RwdAddr ⇀ Coin
    govActionReturns =
      aggregate₊ (mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ)

    payout : RwdAddr ⇀ Coin
    payout = govActionReturns ∪⁺ WithdrawalsOf esW

    gState' : GState
    gState' =
      $\begin{pmatrix} \,\htmlId{20345}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{20346}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{20349}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#19768}{\htmlId{20354}{\htmlClass{Function}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{20361}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#6068}{\htmlId{20366}{\htmlClass{Function}{\text{mapValues}}}}\, \,\htmlId{20376}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{20377}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{20379}{\htmlClass{Field Operator}{\text{+\_}}}}\,\,\htmlId{20381}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{20383}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2179}{\htmlId{20384}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#5215}{\htmlId{20392}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{20398}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{20400}{\htmlClass{Function Operator}{\text{else}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#2179}{\htmlId{20405}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#5215}{\htmlId{20413}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{20419}{\htmlClass{Symbol}{\text{)}}}\,
      \\ \,\href{Ledger.Conway.Specification.Certs.html#2094}{\htmlId{20429}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#5215}{\htmlId{20441}{\htmlClass{Function}{\text{gState}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{20448}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#2578}{\htmlId{20450}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{20458}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#1665}{\htmlId{20459}{\htmlClass{Field}{\text{EnactState.cc}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#19438}{\htmlId{20473}{\htmlClass{Function}{\text{es}}}}\,\,\htmlId{20475}{\htmlClass{Symbol}{\text{)}}}\,
      \end{pmatrix}$

    utxoSt' : UTxOState
    utxoSt' = record utxoSt
      { deposits = DepositsOf utxoSt ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ
      ; donations = 
      }

    totWithdrawals : Coin
    totWithdrawals = ∑[ x ← WithdrawalsOf esW ] x

record EPOCH-Updates : Type where
  constructor EPOCHUpdates
  field
    es             : EnactState
    govSt'         : GovState
    dState''       : DState
    gState'        : GState
    utxoSt'        : UTxOState
    acnt''         : Acnt

EPOCH-updates
  : RatifyState → LState → DState → Acnt → EPOCH-Updates
EPOCH-updates fut ls dState' acnt' =
    EPOCHUpdates (u0 .es) (u0 .govSt') dState'' (u0 .gState') (u0 .utxoSt') acnt''
  where
    open LState
    open EPOCH-Updates0

    u0 = EPOCH-updates0 fut ls

    refunds : Credential ⇀ Coin
    refunds = pullbackMap (u0 .payout) toRwdAddr (dom (RewardsOf dState'))

    dState'' : DState
    dState'' = record dState' { rewards = RewardsOf dState' ∪⁺ refunds }

    unclaimed : Coin
    unclaimed = getCoin (u0 .payout) - getCoin refunds

    acnt'' : Acnt
    acnt'' = record acnt'
      { treasury =
          TreasuryOf acnt' ∸ u0 .totWithdrawals + DonationsOf ls + unclaimed
      }

Transition Rule

This section defines the EPOCH transition rule.

In Conway, the EPOCH rule invokes RATIFIES, and carries out the following tasks:

• Payout all the enacted treasury withdrawals.

• Remove expired and enacted governance actions, and refund deposits.

• If govSt’ 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 fut and store the resulting enact state fut’.

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

  EPOCH :

    ∀ {acnt : Acnt} {utxoSt'' : UTxOState} {acnt' dState' pState'} →

    let
      EPOCHUpdates es govSt' dState'' gState' utxoSt' acnt'' =
        EPOCH-updates fut ls dState' acnt'

      stakeDistrs : StakeDistrs
      stakeDistrs = mkStakeDistrs (Snapshots.mark ss') e utxoSt'
                                  govSt' (GStateOf ls) (DStateOf ls)

      Γ : RatifyEnv
      Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#22703}{\htmlId{22896}{\htmlClass{Bound}{\text{stakeDistrs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17793}{\htmlId{22910}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#2179}{\htmlId{22914}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17902}{\htmlId{22922}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#2094}{\htmlId{22927}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17902}{\htmlId{22939}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Prelude.Base.html#985}{\htmlId{22944}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#22504}{\htmlId{22955}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#2256}{\htmlId{22962}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17902}{\htmlId{22970}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#2222}{\htmlId{22975}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17902}{\htmlId{22988}{\htmlClass{Generalizable}{\text{ls}}}}\, \end{pmatrix}$

    in
        ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
      ∙ Γ  ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#22609}{\htmlId{23049}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{23054}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{23058}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut'
      ∙ _  ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#22636}{\htmlId{23107}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#22504}{\htmlId{23117}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#5433}{\htmlId{23124}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17902}{\htmlId{23133}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#5541}{\htmlId{23138}{\htmlClass{Field}{\text{PStateOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#17902}{\htmlId{23147}{\htmlClass{Generalizable}{\text{ls}}}}\, \end{pmatrix}$ ⇀⦇ e ,POOLREAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#22518}{\htmlId{23170}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#22541}{\htmlId{23181}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#22547}{\htmlId{23189}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#22555}{\htmlId{23199}{\htmlClass{Bound}{\text{pState'}}}}\, \end{pmatrix}$
      ──────────────────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#22504}{\htmlId{23274}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17993}{\htmlId{23281}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17902}{\htmlId{23286}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17916}{\htmlId{23291}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17815}{\htmlId{23297}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#22644}{\htmlId{23318}{\htmlClass{Bound}{\text{acnt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17996}{\htmlId{23327}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#22518}{\htmlId{23335}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#22612}{\htmlId{23346}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#22619}{\htmlId{23357}{\htmlClass{Bound}{\text{dState''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#22555}{\htmlId{23368}{\htmlClass{Bound}{\text{pState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#22628}{\htmlId{23378}{\htmlClass{Bound}{\text{gState'}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#22609}{\htmlId{23394}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17819}{\htmlId{23399}{\htmlClass{Generalizable}{\text{fut'}}}}\, \end{pmatrix}$

NEWEPOCH Transition System

This section defines the NEWEPOCH transition system.

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

  NEWEPOCH-New : ∀ {bprev bcur : BlocksMade} →
    let
      eps' = applyRUpd ru eps
      ss   = EpochState.ss eps''
      pd'  = calculatePoolDelegatedStake (Snapshots.set ss)
    in
      ∙ e ≡ lastEpoch + 
      ∙ _ ⊢ eps' ⇀⦇ e ,EPOCH⦈ eps''
      ──────────────────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#17795}{\htmlId{23978}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#23686}{\htmlId{23990}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#23692}{\htmlId{23998}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17872}{\htmlId{24005}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{24011}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#18014}{\htmlId{24016}{\htmlClass{Generalizable}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18061}{\htmlId{24021}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#17793}{\htmlId{24044}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#23692}{\htmlId{24048}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Axiom.Set.Map.html#2671}{\htmlId{24055}{\htmlClass{Function}{\text{∅ᵐ}}}}\,  \\ \,\href{Ledger.Conway.Specification.Epoch.html#17881}{\htmlId{24061}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{24069}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#23790}{\htmlId{24079}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$

  NEWEPOCH-Not-New : ∀ {bprev bcur : BlocksMade} →
    ∙ e ≢ lastEpoch + 
      ──────────────────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#17795}{\htmlId{24226}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24110}{\htmlId{24238}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24116}{\htmlId{24246}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17872}{\htmlId{24253}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18034}{\htmlId{24259}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18061}{\htmlId{24265}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#17795}{\htmlId{24288}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24110}{\htmlId{24300}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24116}{\htmlId{24308}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17872}{\htmlId{24315}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18034}{\htmlId{24321}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18061}{\htmlId{24327}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$

  NEWEPOCH-No-Reward-Update : ∀ {bprev bcur : BlocksMade} →
    let
      ss  = EpochState.ss eps'
      pd' = calculatePoolDelegatedStake (Snapshots.set ss)
    in
      ∙ e ≡ lastEpoch + 
      ∙ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
      ──────────────────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#17795}{\htmlId{24623}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24366}{\htmlId{24635}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24372}{\htmlId{24643}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17872}{\htmlId{24650}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{24656}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18061}{\htmlId{24666}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#17793}{\htmlId{24689}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24372}{\htmlId{24693}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Axiom.Set.Map.html#2671}{\htmlId{24700}{\htmlClass{Function}{\text{∅ᵐ}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17876}{\htmlId{24705}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{24712}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#24438}{\htmlId{24722}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$

References

[CVG19] Jared Corduan and Polina Vinogradova and Matthias Güdemann. A Formal Specification of the Cardano Ledger. 2019.

[Team18] IOHK Formal Methods Team. Design Specification for Delegation and Incentives in Cardano, IOHK Deliverable SL-D1. 2018.