Epoch

{-# OPTIONS --safe #-}

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

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

open import Ledger.Prelude
open import Data.Integer using () renaming (+_ to pos)
import Data.Integer as ℤ

open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid)
open import Data.List using (filter)

open import Agda.Builtin.FromNat

open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Conformance.Equivalence txs abs
open import Ledger.Conway.Conformance.Equivalence.Convert
open import Ledger.Conway.Conformance.Equivalence.Deposits txs abs
open import Ledger.Conway.Conformance.Ledger txs abs
open import Ledger.Conway.Specification.Ratify txs
open import Ledger.Conway.Conformance.Utxo txs abs
open import Ledger.Conway.Conformance.Certs govStructure
open import Ledger.Conway.Conformance.Rewards txs abs
open import Ledger.Conway.Specification.Epoch txs abs
  using (getStakeCred; getOrphans; mkStakeDistrs; toRwdAddr) public
import Ledger.Conway.Specification.Epoch txs abs as EpochSpec

record EpochState : Type where
  constructor ⟦_,_,_,_,_⟧ᵉ'
  field
    acnt       : Acnt
    ss         : Snapshots
    ls         : LState
    es         : EnactState
    fut        : RatifyState

PoolDelegatedStake : Type
PoolDelegatedStake = KeyHash ⇀ Coin

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

instance
  unquoteDecl HasCast-EpochState HasCast-NewEpochState = derive-HasCast
    ( (quote EpochState     , HasCast-EpochState)
    ∷ [ (quote NewEpochState  , HasCast-NewEpochState)])

  EpochStateFromConf : EpochState ⭆ EpochSpec.EpochState
  EpochStateFromConf .convⁱ _ epochState =
    let open EpochState epochState in
    $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1391}{\htmlId{2142}{\htmlClass{Field}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1413}{\htmlId{2149}{\htmlClass{Field}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#559}{\htmlId{2154}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1440}{\htmlId{2159}{\htmlClass{Field}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1464}{\htmlId{2164}{\htmlClass{Field}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1492}{\htmlId{2169}{\htmlClass{Field}{\text{fut}}}}\, \end{pmatrix}$

  EpochStateToConf : EpochSpec.EpochState ⭆ EpochState
  EpochStateToConf .convⁱ deposits epochSt =
    let open EpochSpec.EpochState epochSt in
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#2305}{\htmlId{2327}{\htmlClass{Field}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#2327}{\htmlId{2334}{\htmlClass{Field}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Deposits.html#12902}{\htmlId{2339}{\htmlClass{Function}{\text{certDeposits}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#2354}{\htmlId{2352}{\htmlClass{Field}{\text{ls}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#377}{\htmlId{2355}{\htmlClass{Function Operator}{\text{⊢conv}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#2354}{\htmlId{2361}{\htmlClass{Field}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#2378}{\htmlId{2366}{\htmlClass{Field}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#2406}{\htmlId{2371}{\htmlClass{Field}{\text{fut}}}}\, \end{pmatrix}$

  NewEpochStateFromConf : NewEpochState ⭆ EpochSpec.NewEpochState
  NewEpochStateFromConf .convⁱ _ newEpochState =
    let open NewEpochState newEpochState in
    $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1627}{\htmlId{2545}{\htmlClass{Field}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1651}{\htmlId{2557}{\htmlClass{Field}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1680}{\htmlId{2565}{\htmlClass{Field}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#559}{\htmlId{2572}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1709}{\htmlId{2577}{\htmlClass{Field}{\text{epochState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1738}{\htmlId{2590}{\htmlClass{Field}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1775}{\htmlId{2595}{\htmlClass{Field}{\text{pd}}}}\, \end{pmatrix}$

  NewEpochStateToConf : EpochSpec.NewEpochState ⭆ NewEpochState
  NewEpochStateToConf .convⁱ deposits newEpochSt =
    let open EpochSpec.NewEpochState newEpochSt in
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#4077}{\htmlId{2773}{\htmlClass{Field}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#4130}{\htmlId{2785}{\htmlClass{Field}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#4101}{\htmlId{2792}{\htmlClass{Field}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#559}{\htmlId{2800}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#4159}{\htmlId{2805}{\htmlClass{Field}{\text{epochState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#4188}{\htmlId{2818}{\htmlClass{Field}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#4225}{\htmlId{2823}{\htmlClass{Field}{\text{pd}}}}\, \end{pmatrix}$


applyRUpd : RewardUpdate → EpochState → EpochState
applyRUpd rewardUpdate
  $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2910}{\htmlId{2910}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2921}{\htmlId{2921}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix}
  \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2937}{\htmlId{2937}{\htmlClass{Bound}{\text{ss}}}}\,
  \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2948}{\htmlId{2948}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2955}{\htmlId{2955}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2962}{\htmlId{2962}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2973}{\htmlId{2973}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
    \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2992}{\htmlId{2992}{\htmlClass{Bound}{\text{govSt}}}}\,
    \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#3008}{\htmlId{3008}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3021}{\htmlId{3021}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3035}{\htmlId{3035}{\htmlClass{Bound}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3045}{\htmlId{3045}{\htmlClass{Bound}{\text{deposits'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3060}{\htmlId{3060}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3069}{\htmlId{3069}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
  \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3087}{\htmlId{3087}{\htmlClass{Bound}{\text{es}}}}\,
  \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3094}{\htmlId{3094}{\htmlClass{Bound}{\text{fut}}}}\,
  \end{pmatrix}$ =
  $\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3352}{\htmlId{3112}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{3120}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#450}{\htmlId{3121}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2910}{\htmlId{3125}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{3134}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18002}{\htmlId{3136}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{3139}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#450}{\htmlId{3141}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3519}{\htmlId{3145}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{3153}{\htmlClass{Symbol}{\text{)}}}\,
    \\ \,\href{Prelude.html#3352}{\htmlId{3161}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{3169}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#450}{\htmlId{3170}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2921}{\htmlId{3174}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{3183}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18005}{\htmlId{3185}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{3187}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}
  \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2937}{\htmlId{3195}{\htmlClass{Bound}{\text{ss}}}}\,
  \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2948}{\htmlId{3206}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3352}{\htmlId{3213}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{3221}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#450}{\htmlId{3222}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2955}{\htmlId{3226}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{3231}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18008}{\htmlId{3233}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{3235}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2962}{\htmlId{3239}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2973}{\htmlId{3250}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
    \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2992}{\htmlId{3268}{\htmlClass{Bound}{\text{govSt}}}}\,
    \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#3008}{\htmlId{3284}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3021}{\htmlId{3297}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3035}{\htmlId{3311}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{3319}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3451}{\htmlId{3322}{\htmlClass{Function}{\text{regRU}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3045}{\htmlId{3330}{\htmlClass{Bound}{\text{deposits'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3060}{\htmlId{3344}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3069}{\htmlId{3353}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
  \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3087}{\htmlId{3368}{\htmlClass{Bound}{\text{es}}}}\,
  \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3094}{\htmlId{3375}{\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

opaque
  calculatePoolDelegatedStake : Snapshot → PoolDelegatedStake
  calculatePoolDelegatedStake ss =
      -- Shelley spec: the output map must contain keys appearing in both
      -- sd and the pool parameters.
      sd ∣ dom (ss .pools)
    where
      open Snapshot

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


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
  certState' : CertState

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

  EPOCH : let
      open LState ls
      open CertState certState
      open RatifyState fut renaming (es to esW)
      open UTxOState
      open PState; open DState; open GState
      open Acnt; open EnactState; open GovActionState

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

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

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

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

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

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

      govActionReturns : RwdAddr ⇀ Coin
      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
      vDeposits  = gState .deposits

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

      pState' : PState
      pState' = $\begin{pmatrix} \,\htmlId{6014}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1128}{\htmlId{6015}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{6022}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4398}{\htmlId{6023}{\htmlClass{Field}{\text{pools}}}}\,\,\htmlId{6028}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{6030}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#5627}{\htmlId{6032}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{6040}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
                \\ \,\htmlId{6060}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1128}{\htmlId{6061}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{6068}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4420}{\htmlId{6069}{\htmlClass{Field}{\text{fPools}}}}\,\,\htmlId{6075}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{6077}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#5627}{\htmlId{6079}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{6087}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
                \\ \,\htmlId{6107}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1128}{\htmlId{6108}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{6115}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4442}{\htmlId{6116}{\htmlClass{Field}{\text{retiring}}}}\,\,\htmlId{6124}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{6126}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#5627}{\htmlId{6128}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{6136}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
                \end{pmatrix}$

      gState' : GState
      gState' = $\begin{pmatrix} \,\htmlId{6198}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{6199}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{6202}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#5077}{\htmlId{6207}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{6214}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#7106}{\htmlId{6219}{\htmlClass{Function}{\text{mapValues}}}}\, \,\htmlId{6229}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{6230}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{6232}{\htmlClass{Field Operator}{\text{+\_}}}}\,\,\htmlId{6234}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{6236}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1148}{\htmlId{6237}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{6244}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#936}{\htmlId{6245}{\htmlClass{Field}{\text{dreps}}}}\,\,\htmlId{6250}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{6252}{\htmlClass{Function Operator}{\text{else}}}}\, \,\htmlId{6257}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1148}{\htmlId{6258}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{6265}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#936}{\htmlId{6266}{\htmlClass{Field}{\text{dreps}}}}\,\,\htmlId{6271}{\htmlClass{Symbol}{\text{))}}}\,
                , \,\htmlId{6292}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1148}{\htmlId{6293}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{6300}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#972}{\htmlId{6301}{\htmlClass{Field}{\text{ccHotKeys}}}}\,\,\htmlId{6310}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#13534}{\htmlId{6312}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#2583}{\htmlId{6314}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{6322}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#4753}{\htmlId{6323}{\htmlClass{Bound}{\text{es}}}}\, \,\htmlId{6326}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Enact.html#1670}{\htmlId{6327}{\htmlClass{Field}{\text{cc}}}}\,\,\htmlId{6329}{\htmlClass{Symbol}{\text{)}}}\,
                , \,\href{Ledger.Conway.Conformance.Epoch.html#5847}{\htmlId{6349}{\htmlClass{Bound}{\text{vDeposits}}}}\,
                \end{pmatrix}$

      certState' : CertState
      certState' = record { dState = dState' ; pState = pState' ; gState = gState' }

      utxoSt' = $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Ledger.html#928}{\htmlId{6511}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{6518}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#2998}{\htmlId{6519}{\htmlClass{Field}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#928}{\htmlId{6526}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{6533}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#3020}{\htmlId{6534}{\htmlClass{Field}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#928}{\htmlId{6541}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{6548}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#3042}{\htmlId{6549}{\htmlClass{Field}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{6558}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#519}{\htmlId{6560}{\htmlClass{Function}{\text{mapˢ}}}}\, \,\htmlId{6565}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{6566}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Function.Base.html#1134}{\htmlId{6572}{\htmlClass{Function Operator}{\text{∘}}}}\, \,\href{Data.Product.Base.html#650}{\htmlId{6574}{\htmlClass{Field}{\text{proj₂}}}}\,\,\htmlId{6579}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#5148}{\htmlId{6581}{\htmlClass{Bound}{\text{removedGovActions}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{6599}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{6603}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$

      acnt' = record acnt
        { treasury  = acnt .treasury ∸ totWithdrawals + utxoSt .donations + unclaimed }

      stakeDistrs : StakeDistrs
      stakeDistrs = mkStakeDistrs (Snapshots.mark ss') e utxoSt' govSt' (record { GState (CertState.gState (LState.certState ls)) })
                                                                        (record { DState (CertState.dState (LState.certState ls)) })

    in
    record { currentEpoch = e
           ; stakeDistrs = stakeDistrs
           ; treasury = acnt .treasury ; GState gState
           ; pools = pState .pools ; delegatees = dState .voteDelegs }
        ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4753}{\htmlId{7236}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{7241}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{7245}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut'
      → ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
    ────────────────────────────────
    _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4258}{\htmlId{7359}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4349}{\htmlId{7366}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4244}{\htmlId{7371}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4272}{\htmlId{7376}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4189}{\htmlId{7382}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#6614}{\htmlId{7411}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4352}{\htmlId{7419}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#6499}{\htmlId{7427}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#5077}{\htmlId{7437}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#6384}{\htmlId{7446}{\htmlClass{Bound}{\text{certState'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4753}{\htmlId{7461}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4193}{\htmlId{7466}{\htmlClass{Generalizable}{\text{fut'}}}}\, \end{pmatrix}$

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

  NEWEPOCH-New :
    ∀ {bprev bcur : BlocksMade} {pd : PoolDelegatedStake} →
    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.Conformance.Epoch.html#4169}{\htmlId{7891}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#7579}{\htmlId{7903}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#7585}{\htmlId{7911}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4214}{\htmlId{7918}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{7924}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#4370}{\htmlId{7929}{\htmlClass{Generalizable}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#7605}{\htmlId{7934}{\htmlClass{Bound}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4167}{\htmlId{7957}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#7585}{\htmlId{7961}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Axiom.Set.Map.html#2671}{\htmlId{7968}{\htmlClass{Function}{\text{∅ᵐ}}}}\,  \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4223}{\htmlId{7974}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{7982}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#7712}{\htmlId{7992}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$

  NEWEPOCH-Not-New : ∀ {bprev bcur : BlocksMade} {pd : PoolDelegatedStake} →
    ∙ e ≢ lastEpoch + 
      ────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4169}{\htmlId{8151}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8023}{\htmlId{8163}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8029}{\htmlId{8171}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4214}{\htmlId{8178}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4390}{\htmlId{8184}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8049}{\htmlId{8190}{\htmlClass{Bound}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4169}{\htmlId{8213}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8023}{\htmlId{8225}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8029}{\htmlId{8233}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4214}{\htmlId{8240}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4390}{\htmlId{8246}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8049}{\htmlId{8252}{\htmlClass{Bound}{\text{pd}}}}\, \end{pmatrix}$

  NEWEPOCH-No-Reward-Update :
    ∀ {bprev bcur : BlocksMade} {pd : PoolDelegatedStake} →
    let
      ss  = EpochState.ss eps'
      pd' = calculatePoolDelegatedStake (Snapshots.set ss)
    in
      ∙ e ≡ lastEpoch + 
      ∙ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
      ────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4169}{\htmlId{8564}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8295}{\htmlId{8576}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8301}{\htmlId{8584}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4214}{\htmlId{8591}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{8597}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8321}{\htmlId{8607}{\htmlClass{Bound}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4167}{\htmlId{8630}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8301}{\htmlId{8634}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Axiom.Set.Map.html#2671}{\htmlId{8641}{\htmlClass{Function}{\text{∅ᵐ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4218}{\htmlId{8646}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{8653}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#8393}{\htmlId{8663}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$