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.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; mkStakeDistrs; toRwdAddr) public record EpochState : Type where constructor ⟦_,_,_,_,_⟧ᵉ' field acnt : Acnt ss : Snapshots ls : LState es : EnactState fut : RatifyState record NewEpochState : Type where field lastEpoch : Epoch epochState : EpochState ru : Maybe RewardUpdate instance unquoteDecl HasCast-EpochState HasCast-NewEpochState = derive-HasCast ( (quote EpochState , HasCast-EpochState) ∷ [ (quote NewEpochState , HasCast-NewEpochState)]) applyRUpd : RewardUpdate → EpochState → EpochState applyRUpd rewardUpdate $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1578}{\htmlId{1578}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1589}{\htmlId{1589}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1605}{\htmlId{1605}{\htmlClass{Bound}{\text{ss}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1616}{\htmlId{1616}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1623}{\htmlId{1623}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1630}{\htmlId{1630}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1641}{\htmlId{1641}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1660}{\htmlId{1660}{\htmlClass{Bound}{\text{govSt}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1676}{\htmlId{1676}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1689}{\htmlId{1689}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1703}{\htmlId{1703}{\htmlClass{Bound}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1713}{\htmlId{1713}{\htmlClass{Bound}{\text{deposits'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1728}{\htmlId{1728}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1737}{\htmlId{1737}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1755}{\htmlId{1755}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1762}{\htmlId{1762}{\htmlClass{Bound}{\text{fut}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3287}{\htmlId{1780}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1788}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#365}{\htmlId{1789}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1578}{\htmlId{1793}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1802}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18195}{\htmlId{1804}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1807}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#365}{\htmlId{1809}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2187}{\htmlId{1813}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{1821}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Prelude.html#3287}{\htmlId{1829}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1837}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#365}{\htmlId{1838}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1589}{\htmlId{1842}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1851}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18198}{\htmlId{1853}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{1855}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1605}{\htmlId{1863}{\htmlClass{Bound}{\text{ss}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1616}{\htmlId{1874}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3287}{\htmlId{1881}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1889}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#365}{\htmlId{1890}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1623}{\htmlId{1894}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1899}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18201}{\htmlId{1901}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{1903}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1630}{\htmlId{1907}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1641}{\htmlId{1918}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1660}{\htmlId{1936}{\htmlClass{Bound}{\text{govSt}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1676}{\htmlId{1952}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1689}{\htmlId{1965}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1703}{\htmlId{1979}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2046}{\htmlId{1987}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2119}{\htmlId{1990}{\htmlClass{Function}{\text{regRU}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1713}{\htmlId{1998}{\htmlClass{Bound}{\text{deposits'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1728}{\htmlId{2012}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1737}{\htmlId{2021}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1755}{\htmlId{2036}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1762}{\htmlId{2043}{\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 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 open UTxOState open PState; open DState; open GState open Acnt; open EnactState; open GovActionState removedGovActions = flip concatMapˢ removed λ (gaid , gaSt) → mapˢ (returnAddr gaSt ,_) ((utxoSt .deposits ∣ ❴ GovActionDeposit gaid ❵) ˢ) govActionReturns = aggregate₊ (mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ) trWithdrawals = es .withdrawals totWithdrawals = ∑[ x ← trWithdrawals ] x es = record es { withdrawals = ∅ } retired = (pState .retiring) ⁻¹ e payout = govActionReturns ∪⁺ trWithdrawals refunds = pullbackMap payout toRwdAddr (dom (dState .rewards)) unclaimed = getCoin payout - getCoin refunds vDeposits = gState .deposits govSt' = filter (λ x → ¿ proj₁ x ∉ mapˢ proj₁ removed ¿) govSt dState' : DState dState' = record dState { rewards = dState .rewards ∪⁺ refunds } pState' : PState pState' = $\begin{pmatrix} \,\htmlId{3669}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1038}{\htmlId{3670}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{3677}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4621}{\htmlId{3678}{\htmlClass{Field}{\text{pools}}}}\,\,\htmlId{3683}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{3685}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3212}{\htmlId{3687}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{3695}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{3699}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1038}{\htmlId{3700}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{3707}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4643}{\htmlId{3708}{\htmlClass{Field}{\text{retiring}}}}\,\,\htmlId{3716}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{3718}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3212}{\htmlId{3720}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{3728}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$ gState' : GState gState' = $\begin{pmatrix} \,\htmlId{3774}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{3775}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{3778}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3469}{\htmlId{3783}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{3790}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#6068}{\htmlId{3795}{\htmlClass{Function}{\text{mapValues}}}}\, \,\htmlId{3805}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{3806}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{3808}{\htmlClass{Field Operator}{\text{+\_}}}}\,\,\htmlId{3810}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{3812}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1058}{\htmlId{3813}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{3820}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#846}{\htmlId{3821}{\htmlClass{Field}{\text{dreps}}}}\,\,\htmlId{3826}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{3828}{\htmlClass{Function Operator}{\text{else}}}}\, \,\htmlId{3833}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1058}{\htmlId{3834}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{3841}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#846}{\htmlId{3842}{\htmlClass{Field}{\text{dreps}}}}\,\,\htmlId{3847}{\htmlClass{Symbol}{\text{))}}}\, , \,\htmlId{3868}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1058}{\htmlId{3869}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{3876}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#882}{\htmlId{3877}{\htmlClass{Field}{\text{ccHotKeys}}}}\,\,\htmlId{3886}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{3888}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#2942}{\htmlId{3890}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{3898}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#3163}{\htmlId{3899}{\htmlClass{Bound}{\text{es}}}}\, \,\htmlId{3902}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Enact.html#2024}{\htmlId{3903}{\htmlClass{Field}{\text{cc}}}}\,\,\htmlId{3905}{\htmlClass{Symbol}{\text{)}}}\, , \,\href{Ledger.Conway.Conformance.Epoch.html#3432}{\htmlId{3925}{\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#842}{\htmlId{4087}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4094}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{4095}{\htmlClass{Field}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#842}{\htmlId{4102}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4109}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{4110}{\htmlClass{Field}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#842}{\htmlId{4117}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4124}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{4125}{\htmlClass{Field}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4134}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#519}{\htmlId{4136}{\htmlClass{Function}{\text{mapˢ}}}}\, \,\htmlId{4141}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{4142}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Function.Base.html#1134}{\htmlId{4148}{\htmlClass{Function Operator}{\text{∘}}}}\, \,\href{Data.Product.Base.html#650}{\htmlId{4150}{\htmlClass{Field}{\text{proj₂}}}}\,\,\htmlId{4155}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2831}{\htmlId{4157}{\htmlClass{Bound}{\text{removedGovActions}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4175}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{4179}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$ acnt' = record acnt { treasury = acnt .treasury ∸ totWithdrawals + utxoSt .donations + unclaimed } in record { currentEpoch = e ; stakeDistrs = mkStakeDistrs (Snapshots.mark ss') govSt' (utxoSt' .deposits) (voteDelegs dState) ; treasury = acnt .treasury ; GState gState ; pools = pState .pools ; delegatees = dState .voteDelegs } ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#3163}{\htmlId{4625}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{4630}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{4634}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut' → ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss' ──────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2356}{\htmlId{4748}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2447}{\htmlId{4755}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2342}{\htmlId{4760}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2370}{\htmlId{4765}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2287}{\htmlId{4771}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4190}{\htmlId{4800}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2450}{\htmlId{4808}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4075}{\htmlId{4816}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3469}{\htmlId{4826}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3960}{\htmlId{4835}{\htmlClass{Bound}{\text{certState'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3163}{\htmlId{4850}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2291}{\htmlId{4855}{\htmlClass{Generalizable}{\text{fut'}}}}\, \end{pmatrix}$ data _⊢_⇀⦇_,NEWEPOCH⦈_ : ⊤ → NewEpochState → Epoch → NewEpochState → Type where NEWEPOCH-New : let eps' = applyRUpd ru eps in ∙ e ≡ lastEpoch + 1 ∙ _ ⊢ eps' ⇀⦇ e ,EPOCH⦈ eps'' ──────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2267}{\htmlId{5111}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2312}{\htmlId{5123}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{5129}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2468}{\htmlId{5134}{\htmlClass{Generalizable}{\text{ru}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2265}{\htmlId{5157}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2321}{\htmlId{5161}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5169}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$ NEWEPOCH-Not-New : ∙ e ≢ lastEpoch + 1 ──────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2267}{\htmlId{5276}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2312}{\htmlId{5288}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2488}{\htmlId{5294}{\htmlClass{Generalizable}{\text{mru}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2267}{\htmlId{5318}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2312}{\htmlId{5330}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2488}{\htmlId{5336}{\htmlClass{Generalizable}{\text{mru}}}}\, \end{pmatrix}$ NEWEPOCH-No-Reward-Update : ∙ e ≡ lastEpoch + 1 ∙ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps' ──────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2267}{\htmlId{5480}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2312}{\htmlId{5492}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5498}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2265}{\htmlId{5526}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2316}{\htmlId{5530}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5537}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$