{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction

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

open import Agda.Builtin.FromNat

import      Data.Integer as ℤ
open import Data.Integer                    using () renaming (+_ to pos)
open import Data.Integer.Properties         using (module ≤-Reasoning; +-mono-≤; neg-mono-≤; +-identityˡ)
                                            renaming (nonNegative⁻¹ to nonNegative⁻¹ℤ)
open import Data.Integer.Tactic.RingSolver  using (solve-∀)
open import Data.Maybe                      using (fromMaybe)
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 Ledger.Prelude hiding (iterate; _/_; _*_; _⊓_; _≟_; ≢-nonZero)
open import Ledger.Prelude.Numeric.UnitInterval using (fromUnitInterval; UnitInterval-*-0≤)

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

open Filter using (filter)
open Number number renaming (fromNat to fromℕ)


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

  HasDReps-EpochState : HasDReps EpochState
  HasDReps-EpochState .DRepsOf = DRepsOf ∘ CertStateOf ∘ 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


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


  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 : 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 (1 ⊓ η * ρ * 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₁ ℤ.+ (0 ℤ.- r₁ ℤ.+ ((f ℤ.+ r₁ ℤ.- t₁) ℤ.- z)) ℤ.+ (0 ℤ.- f) ℤ.+ z) ≡ 0
      lemmaFlow = solve-∀
      flowConservation :
        let t₁ = Δt₁
            r₁ = Δr₁
            f  = pos feeSS
            z  = pos (∑[ c ← rs ] c)
         in
            (t₁ ℤ.+ (0 ℤ.- r₁ ℤ.+ ((f ℤ.+ r₁ ℤ.- t₁) ℤ.- z)) ℤ.+ (0 ℤ.- f) ℤ.+ z) ≡ 0
      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


applyRUpd : RewardUpdate → EpochState → EpochState
applyRUpd rewardUpdate $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#8788}{\htmlId{8788}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8799}{\htmlId{8799}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix}
                       \\ \,\href{Ledger.Conway.Specification.Epoch.html#8836}{\htmlId{8836}{\htmlClass{Bound}{\text{ss}}}}\,
                       \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#8868}{\htmlId{8868}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8875}{\htmlId{8875}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8882}{\htmlId{8882}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8893}{\htmlId{8893}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
                         \\ \,\href{Ledger.Conway.Specification.Epoch.html#8933}{\htmlId{8933}{\htmlClass{Bound}{\text{govSt}}}}\,
                         \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#8970}{\htmlId{8970}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8983}{\htmlId{8983}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8997}{\htmlId{8997}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#9010}{\htmlId{9010}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9019}{\htmlId{9019}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
                       \\ \,\href{Ledger.Conway.Specification.Epoch.html#9058}{\htmlId{9058}{\htmlClass{Bound}{\text{es}}}}\,
                       \\ \,\href{Ledger.Conway.Specification.Epoch.html#9086}{\htmlId{9086}{\htmlClass{Bound}{\text{fut}}}}\,
                       \end{pmatrix}$ = $\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3280}{\htmlId{9123}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{9131}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#416}{\htmlId{9132}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#8788}{\htmlId{9136}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9145}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6286}{\htmlId{9147}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9150}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#416}{\htmlId{9152}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#9707}{\htmlId{9156}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{9164}{\htmlClass{Symbol}{\text{)}}}\,
                               \\ \,\href{Prelude.html#3280}{\htmlId{9199}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{9207}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#416}{\htmlId{9208}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#8799}{\htmlId{9212}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9221}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6289}{\htmlId{9223}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{9225}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}
                             \\ \,\href{Ledger.Conway.Specification.Epoch.html#8836}{\htmlId{9260}{\htmlClass{Bound}{\text{ss}}}}\,
                             \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#8868}{\htmlId{9298}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3280}{\htmlId{9305}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{9313}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#416}{\htmlId{9314}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#8875}{\htmlId{9318}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9323}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6292}{\htmlId{9325}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{9327}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8882}{\htmlId{9331}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8893}{\htmlId{9342}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
                               \\ \,\href{Ledger.Conway.Specification.Epoch.html#8933}{\htmlId{9387}{\htmlClass{Bound}{\text{govSt}}}}\,
                               \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#8970}{\htmlId{9430}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8983}{\htmlId{9443}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8997}{\htmlId{9457}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{9465}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#9639}{\htmlId{9468}{\htmlClass{Function}{\text{regRU}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#9010}{\htmlId{9478}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9019}{\htmlId{9487}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
                             \\ \,\href{Ledger.Conway.Specification.Epoch.html#9058}{\htmlId{9529}{\htmlClass{Bound}{\text{es}}}}\,
                             \\ \,\href{Ledger.Conway.Specification.Epoch.html#9086}{\htmlId{9563}{\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


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 ˢ)) ᶠˢ)


  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)


module VDelegDelegatedStake
  (currentEpoch : Epoch)
  (utxoSt       : UTxOState)
  (govSt        : GovState)
  (gState       : GState)
  (dState       : DState)
  where

  activeDReps : ℙ Credential
  activeDReps = dom (activeDRepsOf gState currentEpoch)

  activeVDelegs : ℙ VDeleg
  activeVDelegs = mapˢ vDelegCredential activeDReps ∪ ❴ vDelegNoConfidence ❵ ∪ ❴ vDelegAbstain ❵

  -- compute the stake for a credential
  stakePerCredential : Credential → Coin
  stakePerCredential c = cbalance ((UTxOOf utxoSt) ∣^' λ txout → getStakeCred txout ≡ just c)
                         + fromMaybe 0 (lookupᵐ? (stakeFromGADeposits govSt utxoSt) c)
                         + fromMaybe 0 (lookupᵐ? (RewardsOf dState) c)

  calculate : VDeleg ⇀ Coin
  calculate = mapFromFun (λ vd → ∑ˢ[ c ← (VoteDelegsOf dState) ⁻¹ vd ] (stakePerCredential c))
                         activeVDelegs


opaque


  calculateVDelegDelegatedStake
    : Epoch
    → UTxOState
    → GovState
    → GState
    → DState
    → VDeleg ⇀ Coin
  calculateVDelegDelegatedStake = VDelegDelegatedStake.calculate


opaque


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


mkStakeDistrs
  : Snapshot
  → Epoch
  → UTxOState
  → GovState
  → GState
  → DState
  → StakeDistrs
mkStakeDistrs ss currentEpoch utxoSt govSt gState dState =
  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#11630}{\htmlId{12430}{\htmlClass{Function}{\text{calculateVDelegDelegatedStake}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12384}{\htmlId{12460}{\htmlClass{Bound}{\text{currentEpoch}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12397}{\htmlId{12473}{\htmlClass{Bound}{\text{utxoSt}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12404}{\htmlId{12480}{\htmlClass{Bound}{\text{govSt}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12410}{\htmlId{12486}{\htmlClass{Bound}{\text{gState}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12417}{\htmlId{12493}{\htmlClass{Bound}{\text{dState}}}}\,
  \\ \,\href{Ledger.Conway.Specification.Epoch.html#11827}{\htmlId{12504}{\htmlClass{Function}{\text{calculatePoolDelegatedStakeForVoting}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12381}{\htmlId{12541}{\htmlClass{Bound}{\text{ss}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12397}{\htmlId{12544}{\htmlClass{Bound}{\text{utxoSt}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12404}{\htmlId{12551}{\htmlClass{Bound}{\text{govSt}}}}\, \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
  pState'' : PState
  dState' : DState
  acnt acnt' : Acnt
  utxoSt'' : UTxOState
  ss ss' : Snapshots
  ru : RewardUpdate
  mru : Maybe RewardUpdate
  pd : PoolDelegatedStake


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

record Governance-Update : Type where
  constructor GovernanceUpdate
  field
    removedGovActions : ℙ (RwdAddr × DepositPurpose × Coin)
    govSt'            : GovState

module GovernanceUpdate (ls : LState)
                        (fut : RatifyState)
                        where


  open LState ls
  open RatifyState fut


  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

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

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

  updates : Governance-Update
  updates = GovernanceUpdate removedGovActions govSt'

record Pre-POOLREAP-Update : Type where
  inductive
  constructor Pre-POOLREAPUpdate
  field
    pState' : PState
    gState' : GState
    utxoSt' : UTxOState

module Pre-POOLREAPUpdate (ls : LState)
                          (es : EnactState)
                          (govUpdate : Governance-Update)
                          where


  open LState ls
  open CertState certState using (pState; gState)
  open PState pState
  open Governance-Update govUpdate


  utxoSt' : UTxOState
  utxoSt' = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Transaction.html#2939}{\htmlId{14891}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1038}{\htmlId{14898}{\htmlClass{Function}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{14907}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1038}{\htmlId{14914}{\htmlClass{Function}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#916}{\htmlId{14923}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#1038}{\htmlId{14934}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{14941}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#519}{\htmlId{14943}{\htmlClass{Function}{\text{mapˢ}}}}\, \,\htmlId{14948}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{14949}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Function.Base.html#1134}{\htmlId{14955}{\htmlClass{Function Operator}{\text{∘}}}}\, \,\href{Data.Product.Base.html#650}{\htmlId{14957}{\htmlClass{Field}{\text{proj₂}}}}\,\,\htmlId{14962}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#13495}{\htmlId{14964}{\htmlClass{Field}{\text{removedGovActions}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{14982}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{14986}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$

  pState' : PState
  pState' = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#3957}{\htmlId{15024}{\htmlClass{Function}{\text{fPools}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{15031}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#3935}{\htmlId{15034}{\htmlClass{Function}{\text{pools}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{15042}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#3979}{\htmlId{15046}{\htmlClass{Function}{\text{retiring}}}}\, \end{pmatrix}$

  gState' : GState
  gState' =
    $\begin{pmatrix} \,\htmlId{15095}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{15096}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{15099}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#13555}{\htmlId{15104}{\htmlClass{Field}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{15111}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#7106}{\htmlId{15116}{\htmlClass{Function}{\text{mapValues}}}}\, \,\href{Ledger.Core.Specification.Epoch.html#1054}{\htmlId{15126}{\htmlClass{Function}{\text{sucᵉ}}}}\, \,\htmlId{15131}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#7086}{\htmlId{15132}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4249}{\htmlId{15140}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{15146}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{15148}{\htmlClass{Function Operator}{\text{else}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#7086}{\htmlId{15153}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4249}{\htmlId{15161}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{15167}{\htmlClass{Symbol}{\text{)}}}\,
    \\ \,\href{Ledger.Conway.Specification.Certs.html#1477}{\htmlId{15175}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4249}{\htmlId{15187}{\htmlClass{Function}{\text{gState}}}}\, \,\href{Axiom.Set.Map.html#13534}{\htmlId{15194}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#1366}{\htmlId{15196}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{15204}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#484}{\htmlId{15205}{\htmlClass{Field}{\text{EnactState.cc}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#14621}{\htmlId{15219}{\htmlClass{Bound}{\text{es}}}}\,\,\htmlId{15221}{\htmlClass{Symbol}{\text{)}}}\,
    \end{pmatrix}$

  updates : Pre-POOLREAP-Update
  updates = Pre-POOLREAPUpdate pState' gState' utxoSt'

record Post-POOLREAP-Update : Type where
  inductive
  constructor Post-POOLREAPUpdate
  field
    dState''       : DState
    acnt''         : Acnt

module Post-POOLREAPUpdate (es : EnactState)
                           (ls : LState)
                           (dState' : DState)
                           (acnt' : Acnt)
                           (govUpd : Governance-Update)
                           where


  open LState
  open Governance-Update govUpd


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

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

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

  dState'' : DState
  dState'' = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2810}{\htmlId{16146}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#15582}{\htmlId{16159}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1892}{\htmlId{16169}{\htmlClass{Field}{\text{StakeDelegsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#15582}{\htmlId{16183}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1727}{\htmlId{16193}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#15582}{\htmlId{16203}{\htmlClass{Bound}{\text{dState'}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{16211}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#16013}{\htmlId{16214}{\htmlClass{Function}{\text{refunds}}}}\, \end{pmatrix}$

  unclaimed : Coin
  unclaimed = getCoin payout - getCoin refunds

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

  acnt'' : Acnt
  acnt'' = $\begin{pmatrix} \,\href{Ledger.Prelude.Base.html#889}{\htmlId{16393}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#15628}{\htmlId{16404}{\htmlClass{Bound}{\text{acnt'}}}}\, \,\href{Data.Nat.Base.html#4462}{\htmlId{16410}{\htmlClass{Primitive Operator}{\text{∸}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#16294}{\htmlId{16412}{\htmlClass{Function}{\text{totWithdrawals}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{16427}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#554}{\htmlId{16429}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#15541}{\htmlId{16441}{\htmlClass{Bound}{\text{ls}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{16444}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#16227}{\htmlId{16446}{\htmlClass{Function}{\text{unclaimed}}}}\, \\ \,\href{Ledger.Prelude.Base.html#773}{\htmlId{16458}{\htmlClass{Field}{\text{ReservesOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#15628}{\htmlId{16469}{\htmlClass{Bound}{\text{acnt'}}}}\, \end{pmatrix}$

  updates : Post-POOLREAP-Update
  updates = Post-POOLREAPUpdate dState'' acnt''


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


  EPOCH :
    let
      es = EnactStateOf fut

      govUpd : Governance-Update
      govUpd = GovernanceUpdate.updates ls fut

      Pre-POOLREAPUpdate pState' gState' utxoSt' = Pre-POOLREAPUpdate.updates ls es govUpd
      Post-POOLREAPUpdate dState'' acnt'' = Post-POOLREAPUpdate.updates es ls dState' acnt' govUpd

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

      govSt' : GovState
      govSt' = Governance-Update.govSt' govUpd

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

      Γ : RatifyEnv
      Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#17097}{\htmlId{17290}{\htmlClass{Bound}{\text{stakeDistrs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12580}{\htmlId{17304}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#7086}{\htmlId{17308}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12689}{\htmlId{17316}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1477}{\htmlId{17321}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12689}{\htmlId{17333}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Prelude.Base.html#889}{\htmlId{17338}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#16888}{\htmlId{17349}{\htmlClass{Bound}{\text{acnt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1562}{\htmlId{17358}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12689}{\htmlId{17366}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#2810}{\htmlId{17371}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12689}{\htmlId{17384}{\htmlClass{Generalizable}{\text{ls}}}}\, \end{pmatrix}$

    in
        ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
      ∙ _  ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#16803}{\htmlId{17445}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12819}{\htmlId{17455}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4449}{\htmlId{17462}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12689}{\htmlId{17471}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#16787}{\htmlId{17476}{\htmlClass{Bound}{\text{pState'}}}}\, \end{pmatrix}$ ⇀⦇ e ,POOLREAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12839}{\htmlId{17504}{\htmlClass{Generalizable}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12824}{\htmlId{17515}{\htmlClass{Generalizable}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12800}{\htmlId{17523}{\htmlClass{Generalizable}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12780}{\htmlId{17533}{\htmlClass{Generalizable}{\text{pState''}}}}\, \end{pmatrix}$
      ∙ Γ  ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#16959}{\htmlId{17559}{\htmlClass{Bound}{\text{es'}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{17565}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{17569}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut'
      ──────────────────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12819}{\htmlId{17668}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12862}{\htmlId{17675}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12689}{\htmlId{17680}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12703}{\htmlId{17685}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12602}{\htmlId{17691}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#16888}{\htmlId{17712}{\htmlClass{Bound}{\text{acnt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12865}{\htmlId{17721}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12839}{\htmlId{17729}{\htmlClass{Generalizable}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17025}{\htmlId{17740}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#16879}{\htmlId{17751}{\htmlClass{Bound}{\text{dState''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12780}{\htmlId{17762}{\htmlClass{Generalizable}{\text{pState''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#16795}{\htmlId{17773}{\htmlClass{Bound}{\text{gState'}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#16959}{\htmlId{17789}{\htmlClass{Bound}{\text{es'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12606}{\htmlId{17795}{\htmlClass{Generalizable}{\text{fut'}}}}\, \end{pmatrix}$


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 + 1
      ∙ _ ⊢ eps' ⇀⦇ e ,EPOCH⦈ eps''
      ──────────────────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12582}{\htmlId{18197}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17905}{\htmlId{18209}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17911}{\htmlId{18217}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12659}{\htmlId{18224}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{18230}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#12883}{\htmlId{18235}{\htmlClass{Generalizable}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12930}{\htmlId{18240}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12580}{\htmlId{18263}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#17911}{\htmlId{18267}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Axiom.Set.Map.html#2671}{\htmlId{18274}{\htmlClass{Function}{\text{∅ᵐ}}}}\,  \\ \,\href{Ledger.Conway.Specification.Epoch.html#12668}{\htmlId{18280}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{18288}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18009}{\htmlId{18298}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$

  NEWEPOCH-Not-New : ∀ {bprev bcur : BlocksMade} →
    ∙ e ≢ lastEpoch + 1
      ──────────────────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12582}{\htmlId{18445}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18329}{\htmlId{18457}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18335}{\htmlId{18465}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12659}{\htmlId{18472}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12903}{\htmlId{18478}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12930}{\htmlId{18484}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12582}{\htmlId{18507}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18329}{\htmlId{18519}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18335}{\htmlId{18527}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12659}{\htmlId{18534}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12903}{\htmlId{18540}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12930}{\htmlId{18546}{\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 + 1
      ∙ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
      ──────────────────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12582}{\htmlId{18842}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18585}{\htmlId{18854}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18591}{\htmlId{18862}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12659}{\htmlId{18869}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{18875}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12930}{\htmlId{18885}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12580}{\htmlId{18908}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18591}{\htmlId{18912}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Axiom.Set.Map.html#2671}{\htmlId{18919}{\htmlClass{Function}{\text{∅ᵐ}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12663}{\htmlId{18924}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{18931}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#18657}{\htmlId{18941}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$