{-# 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




record EpochState : Type where


  constructor ⟦_,_,_,_,_⟧ᵉ'


  field
    acnt       : Acnt
    ss         : Snapshots
    ls         : LState
    es         : EnactState
    fut        : RatifyState



record HasEpochState {a} (A : Type a) : Type a where
  field EpochStateOf : A  EpochState
open HasEpochState ⦃...⦄ public

instance
  HasLState-EpochState : HasLState EpochState
  HasLState-EpochState .LStateOf = EpochState.ls

  HasEnactState-EpochState : HasEnactState EpochState
  HasEnactState-EpochState .EnactStateOf = EpochState.es

  HasDeposits-EpochState : HasDeposits EpochState
  HasDeposits-EpochState .DepositsOf = DepositsOf  LStateOf

  HasTreasury-EpochState : HasTreasury EpochState
  HasTreasury-EpochState .TreasuryOf = Acnt.treasury  EpochState.acnt

  HasReserves-EpochState : HasReserves EpochState
  HasReserves-EpochState .ReservesOf = Acnt.reserves  EpochState.acnt

  HasPParams-EpochState : HasPParams EpochState
  HasPParams-EpochState .PParamsOf = PParamsOf  EnactStateOf

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


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


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


          }
  where
    prevPp       = PParamsOf es
    reserves     = ReservesOf es
    pstakego     = es .EpochState.ss .Snapshots.go
    feeSS        = es .EpochState.ss .Snapshots.feeSS
    stake        = pstakego .Snapshot.stake
    delegs       = pstakego .Snapshot.delegations
    poolParams   = pstakego .Snapshot.poolParameters
    blocksMade   = ∑[ m  b ] m
    ρ            = fromUnitInterval (prevPp .PParams.monetaryExpansion)
    η            = fromℕ blocksMade ÷₀ (fromℕ slotsPerEpoch * ActiveSlotCoeff)
    Δr₁          = floor (1  η * ρ * fromℕ reserves)
    rewardPot    = pos feeSS + Δr₁
    τ            = fromUnitInterval (prevPp .PParams.treasuryCut)
    Δt₁          = floor (fromℤ rewardPot * τ)
    R            = rewardPot - Δt₁
    circulation  = total - reserves
    rs           = reward prevPp b (posPart R) poolParams stake delegs circulation
    Δr₂          = R - pos (∑[ c  rs ] c)



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

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

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

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

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

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

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

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


applyRUpd : RewardUpdate  EpochState  EpochState
applyRUpd rewardUpdate
  $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#7892}{\htmlId{7892}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7903}{\htmlId{7903}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix}
  \\ \,\href{Ledger.Conway.Specification.Epoch.html#7919}{\htmlId{7919}{\htmlClass{Bound}{\text{ss}}}}\,
  \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#7930}{\htmlId{7930}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7937}{\htmlId{7937}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7944}{\htmlId{7944}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7955}{\htmlId{7955}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
    \\ \,\href{Ledger.Conway.Specification.Epoch.html#7974}{\htmlId{7974}{\htmlClass{Bound}{\text{govSt}}}}\,
    \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#7990}{\htmlId{7990}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8003}{\htmlId{8003}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8017}{\htmlId{8017}{\htmlClass{Bound}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#8030}{\htmlId{8030}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8039}{\htmlId{8039}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
  \\ \,\href{Ledger.Conway.Specification.Epoch.html#8057}{\htmlId{8057}{\htmlClass{Bound}{\text{es}}}}\,
  \\ \,\href{Ledger.Conway.Specification.Epoch.html#8064}{\htmlId{8064}{\htmlClass{Bound}{\text{fut}}}}\,
  \end{pmatrix}$ =
  $\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3279}{\htmlId{8082}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{8090}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#76}{\htmlId{8091}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#7892}{\htmlId{8095}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8104}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6263}{\htmlId{8106}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8109}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#76}{\htmlId{8111}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#8477}{\htmlId{8115}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{8123}{\htmlClass{Symbol}{\text{)}}}\,
    \\ \,\href{Prelude.html#3279}{\htmlId{8131}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{8139}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#76}{\htmlId{8140}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#7903}{\htmlId{8144}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8153}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6266}{\htmlId{8155}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{8157}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}
  \\ \,\href{Ledger.Conway.Specification.Epoch.html#7919}{\htmlId{8165}{\htmlClass{Bound}{\text{ss}}}}\,
  \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#7930}{\htmlId{8176}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3279}{\htmlId{8183}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{8191}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#76}{\htmlId{8192}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#7937}{\htmlId{8196}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8201}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6269}{\htmlId{8203}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{8205}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7944}{\htmlId{8209}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#7955}{\htmlId{8220}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
    \\ \,\href{Ledger.Conway.Specification.Epoch.html#7974}{\htmlId{8238}{\htmlClass{Bound}{\text{govSt}}}}\,
    \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#7990}{\htmlId{8254}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8003}{\htmlId{8267}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8017}{\htmlId{8281}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2046}{\htmlId{8289}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#8409}{\htmlId{8292}{\htmlClass{Function}{\text{regRU}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#8030}{\htmlId{8302}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#8039}{\htmlId{8311}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
  \\ \,\href{Ledger.Conway.Specification.Epoch.html#8057}{\htmlId{8326}{\htmlClass{Bound}{\text{es}}}}\,
  \\ \,\href{Ledger.Conway.Specification.Epoch.html#8064}{\htmlId{8333}{\htmlClass{Bound}{\text{fut}}}}\, \end{pmatrix}$
  where
    open RewardUpdate rewardUpdate using (Δt; Δr; Δf; rs)
    regRU     = rs  dom rewards
    unregRU   = rs  dom rewards 
    unregRU'  = ∑[ x  unregRU ] x

getOrphans : EnactState  GovState  GovState
getOrphans es govSt = proj₁ $ iterate step ([] , govSt) (length govSt)
  where
    step : GovState × GovState  GovState × GovState
    step (orps , govSt) =
      let
        isOrphan? a prev = ¬? (hasParent? es govSt a prev)
        (orps' , govSt') = partition
           (_ , record {action = a ; prevAction = prev})  isOrphan? (a .gaType) prev) govSt
      in
        (orps ++ orps' , govSt')


open RwdAddr using (stake)


gaDepositStake : GovState  Deposits  Credential  Coin
gaDepositStake govSt ds = aggregateBy
  (mapˢ  (gaid , addr)  (gaid , addr) , stake addr) govSt')
  (mapFromPartialFun  (gaid , _)  lookupᵐ? ds (GovActionDeposit gaid)) govSt')
  where govSt' = mapˢ (map₂ returnAddr) (fromList govSt)



opaque


  mkStakeDistrs : Snapshot  GovState  Deposits  VoteDelegs  StakeDistrs
  mkStakeDistrs ss govSt ds delegations .StakeDistrs.stakeDistr =
    aggregateBy  delegations  (Snapshot.stake ss ∪⁺ gaDepositStake govSt ds)


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


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 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{11257}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{11258}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{11261}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#10680}{\htmlId{11266}{\htmlClass{Function}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{11273}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#6068}{\htmlId{11278}{\htmlClass{Function}{\text{mapValues}}}}\, \,\htmlId{11288}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{11289}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11291}{\htmlClass{Field Operator}{\text{+\_}}}}\,\,\htmlId{11293}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{11295}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#1530}{\htmlId{11296}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4193}{\htmlId{11304}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{11310}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{11312}{\htmlClass{Function Operator}{\text{else}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#1530}{\htmlId{11317}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4193}{\htmlId{11325}{\htmlClass{Function}{\text{gState}}}}\,\,\htmlId{11331}{\htmlClass{Symbol}{\text{)}}}\,
      \\ \,\href{Ledger.Conway.Specification.Certs.html#1445}{\htmlId{11341}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4193}{\htmlId{11353}{\htmlClass{Function}{\text{gState}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{11360}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#1367}{\htmlId{11362}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{11370}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Enact.html#484}{\htmlId{11371}{\htmlClass{Field}{\text{EnactState.cc}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#10350}{\htmlId{11385}{\htmlClass{Function}{\text{es}}}}\,\,\htmlId{11387}{\htmlClass{Symbol}{\text{)}}}\,
      \end{pmatrix}$

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

    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
      }


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'

    in
      record { currentEpoch = e
             ; stakeDistrs = mkStakeDistrs
                               (Snapshots.mark ss')
                               govSt'
                               (DepositsOf utxoSt')
                               (VoteDelegsOf ls)
             ; treasury = TreasuryOf acnt
             ; GState (GStateOf ls)
             ; pools = PoolsOf ls
             ; delegatees = VoteDelegsOf ls
             }
           $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12762}{\htmlId{13308}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{13313}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{13317}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut'
         ls  ss ⇀⦇ tt ,SNAP⦈ ss'
         _  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12789}{\htmlId{13402}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12672}{\htmlId{13412}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4393}{\htmlId{13419}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#9647}{\htmlId{13428}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4501}{\htmlId{13433}{\htmlClass{Field}{\text{PStateOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#9647}{\htmlId{13442}{\htmlClass{Generalizable}{\text{ls}}}}\, \end{pmatrix}$ ⇀⦇ e ,POOLREAP⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12686}{\htmlId{13465}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12709}{\htmlId{13476}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12715}{\htmlId{13484}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12723}{\htmlId{13494}{\htmlClass{Bound}{\text{pState'}}}}\, \end{pmatrix}$
      ────────────────────────────────
      _  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12672}{\htmlId{13555}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9738}{\htmlId{13562}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9647}{\htmlId{13567}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9661}{\htmlId{13572}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9560}{\htmlId{13578}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12797}{\htmlId{13599}{\htmlClass{Bound}{\text{acnt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9741}{\htmlId{13608}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12686}{\htmlId{13616}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12765}{\htmlId{13627}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#12772}{\htmlId{13638}{\htmlClass{Bound}{\text{dState''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12723}{\htmlId{13649}{\htmlClass{Bound}{\text{pState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#12781}{\htmlId{13659}{\htmlClass{Bound}{\text{gState'}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Epoch.html#12762}{\htmlId{13675}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9564}{\htmlId{13680}{\htmlClass{Generalizable}{\text{fut'}}}}\, \end{pmatrix}$


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 .poolParameters)
    where
      open Snapshot

      -- delegated stake per pool
      sd : KeyHash  Coin
      sd = aggregate₊ ((stakeCredentialsPerPool ∘ʳ (ss .stake ˢ)) ᶠˢ)
        where mutual
          -- stake credentials delegating to each pool
          stakeCredentialsPerPool : Rel KeyHash Credential
          stakeCredentialsPerPool = (ss .delegations ˢ) ⁻¹ʳ

          -- TODO: Move to agda-sets
          -- https://github.com/input-output-hk/agda-sets/pull/13
          _⁻¹ʳ : {A B : Type}  Rel A B  Rel B A
          R ⁻¹ʳ = mapˢ swap R
            where open import Data.Product using (swap)

          _∘ʳ_ : {A B C : Type}  _ : DecEq B   Rel A B  Rel B C  Rel A C
          R ∘ʳ S =
            concatMapˢ
               (a , b)  mapˢ ((a ,_)  proj₂) $ filterˢ ((b ≡_)  proj₁) S)
              R


data


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


  where


  NEWEPOCH-New : let
      eps' = applyRUpd ru eps
      $\begin{pmatrix} \,\htmlId{14903}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#14907}{\htmlId{14907}{\htmlClass{Bound}{\text{ss}}}}\, \\ \,\htmlId{14912}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{14916}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{14920}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = eps''
      pd' = calculatePoolDelegatedStake (Snapshots.set ss)
    in
     e  lastEpoch + 1
     _  eps' ⇀⦇ e ,EPOCH⦈ eps''
      ────────────────────────────────
      _  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#9540}{\htmlId{15109}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9617}{\htmlId{15121}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{15127}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#9759}{\htmlId{15132}{\htmlClass{Generalizable}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9806}{\htmlId{15137}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#9538}{\htmlId{15160}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9626}{\htmlId{15164}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{15172}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#14940}{\htmlId{15182}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$

  NEWEPOCH-Not-New :
     e  lastEpoch + 1
      ────────────────────────────────
      _  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#9540}{\htmlId{15285}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9617}{\htmlId{15297}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9779}{\htmlId{15303}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9806}{\htmlId{15309}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#9540}{\htmlId{15332}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9617}{\htmlId{15344}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9779}{\htmlId{15350}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9806}{\htmlId{15356}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$

  NEWEPOCH-No-Reward-Update : let
      $\begin{pmatrix} \,\htmlId{15404}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#15408}{\htmlId{15408}{\htmlClass{Bound}{\text{ss}}}}\, \\ \,\htmlId{15413}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{15417}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{15421}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = eps'
      pd' = calculatePoolDelegatedStake (Snapshots.set ss)
    in
     e  lastEpoch + 1
     _  eps ⇀⦇ e ,EPOCH⦈ eps'
      ────────────────────────────────
      _  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#9540}{\htmlId{15607}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9617}{\htmlId{15619}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{15625}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9806}{\htmlId{15635}{\htmlClass{Generalizable}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#9538}{\htmlId{15658}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#9621}{\htmlId{15662}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{15669}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#15440}{\htmlId{15679}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$