{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Abstract
open import Ledger.Dijkstra.Specification.Transaction

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

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.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 Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid)
open import Data.List using (filter)

open import Agda.Builtin.FromNat
open import Data.Nat.GeneralisedArithmetic using (iterate)

open import Data.Maybe                      using (fromMaybe)

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

open Number number renaming (fromNat to fromℕ)


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

getStakeCred : TxOut → Maybe Credential
getStakeCred (a , _ , _ , _) = stakeCred a

open GovActionState using (returnAddr)
-- open RewardAddress using (stake)

PoolDelegatedStake : Type
PoolDelegatedStake = KeyHash ⇀ Coin

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


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

instance
  HasAccount-EpochState : HasAccount EpochState
  HasAccount-EpochState .AccountOf = EpochState.acnt

  HasSnapshots-EpochState : HasSnapshots EpochState
  HasSnapshots-EpochState .SnapshotsOf = EpochState.ss

  HasLedgerState-EpochState : HasLedgerState EpochState
  HasLedgerState-EpochState .LedgerStateOf = EpochState.ls

  HasGovState-EpochState : HasGovState EpochState
  HasGovState-EpochState .GovStateOf = GovStateOf ∘ LedgerStateOf

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

  HasDReps-EpochState : HasDReps EpochState
  HasDReps-EpochState .DRepsOf = DRepsOf ∘ CertStateOf ∘ LedgerStateOf

  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 ∘ LedgerStateOf

  HasRetiring-EpochState : HasRetiring EpochState
  HasRetiring-EpochState .RetiringOf = RetiringOf ∘ PStateOf


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

  HasLedgerState-NewEpochState : HasLedgerState NewEpochState
  HasLedgerState-NewEpochState .LedgerStateOf = LedgerStateOf ∘ EpochStateOf

  HasGovState-NewEpochState : HasGovState NewEpochState
  HasGovState-NewEpochState .GovStateOf = GovStateOf ∘ LedgerStateOf

  HasCertState-NewEpochState : HasCertState NewEpochState
  HasCertState-NewEpochState .CertStateOf = CertStateOf ∘ LedgerStateOf

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

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

open RewardAddress using (stake)


applyRUpd : RewardUpdate → EpochState → EpochState
applyRUpd rewardUpdate
  $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#9622}{\htmlId{9622}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9633}{\htmlId{9633}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9647}{\htmlId{9647}{\htmlClass{Bound}{\text{ss}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#9656}{\htmlId{9656}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9663}{\htmlId{9663}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9670}{\htmlId{9670}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9685}{\htmlId{9685}{\htmlClass{Bound}{\text{govSt}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#9697}{\htmlId{9697}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9710}{\htmlId{9710}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9724}{\htmlId{9724}{\htmlClass{Bound}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9734}{\htmlId{9734}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9748}{\htmlId{9748}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9757}{\htmlId{9757}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9773}{\htmlId{9773}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9778}{\htmlId{9778}{\htmlClass{Bound}{\text{fut}}}}\, \end{pmatrix}$ = $\begin{pmatrix}  \begin{pmatrix} \,\href{Prelude.html#3332}{\htmlId{9793}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{9801}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Epoch.html#383}{\htmlId{9802}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#9622}{\htmlId{9806}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9815}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Rewards.html#6275}{\htmlId{9817}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9820}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#383}{\htmlId{9822}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#10167}{\htmlId{9826}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{9834}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Prelude.html#3332}{\htmlId{9838}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{9846}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Epoch.html#383}{\htmlId{9847}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#9633}{\htmlId{9851}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9860}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Rewards.html#6278}{\htmlId{9862}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{9864}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9647}{\htmlId{9870}{\htmlClass{Bound}{\text{ss}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#9656}{\htmlId{9879}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3332}{\htmlId{9886}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{9894}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Epoch.html#383}{\htmlId{9895}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#9663}{\htmlId{9899}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9904}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Rewards.html#6281}{\htmlId{9906}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{9908}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9670}{\htmlId{9912}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9685}{\htmlId{9926}{\htmlClass{Bound}{\text{govSt}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#9697}{\htmlId{9938}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9710}{\htmlId{9951}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9724}{\htmlId{9965}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{9973}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#10103}{\htmlId{9976}{\htmlClass{Function}{\text{regRU}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9734}{\htmlId{9984}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9748}{\htmlId{9998}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9757}{\htmlId{10007}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix}  \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9773}{\htmlId{10024}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#9778}{\htmlId{10029}{\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 = sd ∣ dom (ss .pools)
    -- Shelley spec: the output map must contain keys appearing in both
    -- sd and the pool parameters.
    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 ˢ)) ᶠˢ)

  -- In Dijkstra, look up each gov action's deposit from GState.deposits
  -- using the stake credential of the proposal's returnAddr.
  stakeFromGADeposits : GovState → GState → Stake
  stakeFromGADeposits govSt gState =
    aggregateBy
      (mapˢ (λ (gaid , addr) → (gaid , addr) , stake addr) govSt')
      (mapFromPartialFun (λ (_ , addr) → lookupᵐ? (DepositsOf gState) (stake addr)) govSt')
    where
      govSt' : ℙ (GovActionID × RewardAddress)
      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 ❵
  stakePerCredential : Credential → Coin
  stakePerCredential c =
      cbalance ((UTxOOf utxoSt) ∣^' λ txout → getStakeCred txout ≡ just c)
    + fromMaybe 0 (lookupᵐ? (stakeFromGADeposits govSt gState) c)  -- ← gState, not utxoSt
    + 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

  -- Pool-delegated stake for voting:
  -- also uses gState instead of utxoSt for gov-action deposit component.
  calculatePoolDelegatedStakeForVoting : Snapshot → GovState → GState → KeyHash ⇀ Coin
  calculatePoolDelegatedStakeForVoting ss govSt gState =
    calculatePoolDelegatedStake ss ∪⁺ (stakeFromDeposits ∣ dom (PoolsOf ss))
    where
    stakeFromDeposits : KeyHash ⇀ Coin
    stakeFromDeposits = aggregate₊ (((StakeDelegsOf ss ˢ) ⁻¹ʳ ∘ʳ (stakeFromGADeposits govSt gState ˢ)) ᶠˢ)

-- mkStakeDistrs no longer takes utxoSt for the deposit lookup,
-- but still takes it for the UTxO-balance part of VDeleg stake.
mkStakeDistrs : Snapshot → Epoch → UTxOState → GovState → GState → DState → StakeDistrs
mkStakeDistrs ss currentEpoch utxoSt govSt gState dState =
  $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#12090}{\htmlId{13021}{\htmlClass{Function}{\text{calculateVDelegDelegatedStake}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#12975}{\htmlId{13051}{\htmlClass{Bound}{\text{currentEpoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#12988}{\htmlId{13064}{\htmlClass{Bound}{\text{utxoSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#12995}{\htmlId{13071}{\htmlClass{Bound}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#13001}{\htmlId{13077}{\htmlClass{Bound}{\text{gState}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#13008}{\htmlId{13084}{\htmlClass{Bound}{\text{dState}}}}\,
  \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#12365}{\htmlId{13095}{\htmlClass{Function}{\text{calculatePoolDelegatedStakeForVoting}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#12972}{\htmlId{13132}{\htmlClass{Bound}{\text{ss}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#12995}{\htmlId{13135}{\htmlClass{Bound}{\text{govSt}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#13001}{\htmlId{13141}{\htmlClass{Bound}{\text{gState}}}}\,   \,\htmlId{13150}{\htmlClass{Comment}{\text{-- ← no utxoSt here}}}\,
  \end{pmatrix}$


private variable
  e lastEpoch : Epoch
  fut fut' : RatifyState
  eps eps' eps'' : EpochState
  ls : LedgerState
  acnt : Acnt
  es₀ : EnactState
  ss ss' : Snapshots
  ru : RewardUpdate
  mru : Maybe RewardUpdate


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

  EPOCH : let
      open LedgerState ls
      open RatifyState fut renaming (es to esW)

      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 : ℙ (RewardAddress × Coin)
      removedGovActions =
          mapPartial
            (λ (gaid , gaSt) →
              let ra   = GovActionState.returnAddr gaSt
                  cred = RewardAddress.stake ra
              in  (ra ,_) <$> lookupᵐ? (DepositsOf (GStateOf ls)) cred)
            removed'

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

      trWithdrawals   = WithdrawalsOf esW
      totWithdrawals  = ∑[ x ← trWithdrawals ] x

      retired    = (RetiringOf (PStateOf ls)) ⁻¹ e
      payout     = govActionReturns ∪⁺ trWithdrawals
      refunds    = pullbackMap payout toRewardAddress (dom (RewardsOf (DStateOf ls)))
      unclaimed  = getCoin payout - getCoin refunds

      dState' : DState
      dState' = record (DStateOf ls) { rewards = (RewardsOf (DStateOf ls)) ∪⁺ refunds }

      pState' : PState
      pState' = let ps = PStateOf ls in
        $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#2930}{\htmlId{14934}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#14904}{\htmlId{14942}{\htmlClass{Bound}{\text{ps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{14945}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#14512}{\htmlId{14947}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{14955}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#2140}{\htmlId{14959}{\htmlClass{Field}{\text{PState.fPools}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#14904}{\htmlId{14973}{\htmlClass{Bound}{\text{ps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{14976}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#14512}{\htmlId{14978}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{14986}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3037}{\htmlId{14990}{\htmlClass{Field}{\text{RetiringOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#14904}{\htmlId{15001}{\htmlClass{Bound}{\text{ps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15004}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#14512}{\htmlId{15006}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15014}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#2697}{\htmlId{15018}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#14904}{\htmlId{15029}{\htmlClass{Bound}{\text{ps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15032}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#14512}{\htmlId{15034}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15042}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

      gState' : GState
      gState' = $\begin{pmatrix} \,\htmlId{15088}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{15089}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{15092}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#13883}{\htmlId{15097}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{15104}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#7108}{\htmlId{15109}{\htmlClass{Function}{\text{mapValues}}}}\, \,\htmlId{15119}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{15120}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{15122}{\htmlClass{Field Operator}{\text{+\_}}}}\,\,\htmlId{15124}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{15126}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4981}{\htmlId{15127}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#13272}{\htmlId{15135}{\htmlClass{Generalizable}{\text{ls}}}}\,\,\htmlId{15137}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{15139}{\htmlClass{Function Operator}{\text{else}}}}\, \,\htmlId{15144}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4981}{\htmlId{15145}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#13272}{\htmlId{15153}{\htmlClass{Generalizable}{\text{ls}}}}\,\,\htmlId{15155}{\htmlClass{Symbol}{\text{))}}}\,
                , \,\href{Ledger.Dijkstra.Specification.Certs.html#2814}{\htmlId{15176}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#13272}{\htmlId{15188}{\htmlClass{Generalizable}{\text{ls}}}}\, \,\href{Axiom.Set.Map.html#13536}{\htmlId{15191}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Enact.html#1554}{\htmlId{15193}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{15201}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Enact.html#672}{\htmlId{15202}{\htmlClass{Field}{\text{EnactState.cc}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#13559}{\htmlId{15216}{\htmlClass{Bound}{\text{es}}}}\,\,\htmlId{15218}{\htmlClass{Symbol}{\text{)}}}\,
                , \,\href{Ledger.Dijkstra.Specification.Certs.html#2697}{\htmlId{15238}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{15249}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3713}{\htmlId{15250}{\htmlClass{Field}{\text{GStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#13272}{\htmlId{15259}{\htmlClass{Generalizable}{\text{ls}}}}\,\,\htmlId{15261}{\htmlClass{Symbol}{\text{)}}}\,
                  \,\htmlId{15281}{\htmlClass{Comment}{\text{-- ∣ mapˢ (RewardAddress.stake ∘ GovActionState.returnAddr ∘ proj₂) removed' ᶜ}}}\,
                \end{pmatrix}$

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

      -- utxoSt' = ⟦ utxoSt .utxo , utxoSt .fees , utxoSt .deposits ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ , 0 ⟧
      utxoSt' = UTxOStateOf ls

      acnt' = record acnt
        { treasury  = TreasuryOf acnt ∸ totWithdrawals + DonationsOf utxoSt + unclaimed }

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

      ratifyΓ : RatifyEnv
      ratifyΓ = record { stakeDistrs  = stakeDistrs
                       ; currentEpoch = e
                       ; dreps        = DRepsOf ls
                       ; ccHotKeys    = CCHotKeysOf ls
                       ; treasury     = TreasuryOf acnt
                       ; pools        = PoolsOf ls
                       ; delegatees   = VoteDelegsOf ls }

    in
    ∙ ratifyΓ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#13559}{\htmlId{16310}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{16315}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{16319}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut'
    ∙ ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
      ────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#13291}{\htmlId{16435}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13324}{\htmlId{16442}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13272}{\htmlId{16447}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13305}{\htmlId{16452}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13217}{\htmlId{16458}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#15649}{\htmlId{16479}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13327}{\htmlId{16487}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#15617}{\htmlId{16495}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13883}{\htmlId{16505}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#15385}{\htmlId{16514}{\htmlClass{Bound}{\text{certState'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13559}{\htmlId{16529}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13221}{\htmlId{16534}{\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 + 1
       ∙ _ ⊢ eps' ⇀⦇ e ,EPOCH⦈ eps''
       ────────────────────────────────
       _ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#13197}{\htmlId{16959}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#16647}{\htmlId{16971}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#16653}{\htmlId{16979}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13242}{\htmlId{16986}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{16992}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#13345}{\htmlId{16997}{\htmlClass{Generalizable}{\text{ru}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#16673}{\htmlId{17002}{\htmlClass{Bound}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#13195}{\htmlId{17025}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#16653}{\htmlId{17029}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Axiom.Set.Map.html#2671}{\htmlId{17036}{\htmlClass{Function}{\text{∅ᵐ}}}}\,  \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13251}{\htmlId{17042}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{17050}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#16780}{\htmlId{17060}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$

  NEWEPOCH-Not-New : ∀ {bprev bcur : BlocksMade} {pd : PoolDelegatedStake} →
    ∙ e ≢ lastEpoch + 1
      ────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#13197}{\htmlId{17219}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17091}{\htmlId{17231}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17097}{\htmlId{17239}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13242}{\htmlId{17246}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13365}{\htmlId{17252}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17117}{\htmlId{17258}{\htmlClass{Bound}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#13197}{\htmlId{17281}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17091}{\htmlId{17293}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17097}{\htmlId{17301}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13242}{\htmlId{17308}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13365}{\htmlId{17314}{\htmlClass{Generalizable}{\text{mru}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17117}{\htmlId{17320}{\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 + 1
      ∙ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
      ────────────────────────────────
      _ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#13197}{\htmlId{17632}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17363}{\htmlId{17644}{\htmlClass{Bound}{\text{bprev}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17369}{\htmlId{17652}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13242}{\htmlId{17659}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{17665}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17389}{\htmlId{17675}{\htmlClass{Bound}{\text{pd}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#13195}{\htmlId{17698}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17369}{\htmlId{17702}{\htmlClass{Bound}{\text{bcur}}}}\, \\ \,\href{Axiom.Set.Map.html#2671}{\htmlId{17709}{\htmlClass{Function}{\text{∅ᵐ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#13246}{\htmlId{17714}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{17721}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#17461}{\htmlId{17731}{\htmlClass{Bound}{\text{pd'}}}}\, \end{pmatrix}$