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; getOrphans; 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#1675}{\htmlId{1675}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1686}{\htmlId{1686}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1702}{\htmlId{1702}{\htmlClass{Bound}{\text{ss}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1713}{\htmlId{1713}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1720}{\htmlId{1720}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1727}{\htmlId{1727}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1738}{\htmlId{1738}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1757}{\htmlId{1757}{\htmlClass{Bound}{\text{govSt}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1773}{\htmlId{1773}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1786}{\htmlId{1786}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1800}{\htmlId{1800}{\htmlClass{Bound}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1810}{\htmlId{1810}{\htmlClass{Bound}{\text{deposits'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1825}{\htmlId{1825}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1834}{\htmlId{1834}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1852}{\htmlId{1852}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1859}{\htmlId{1859}{\htmlClass{Bound}{\text{fut}}}}\, \end{pmatrix}$ = $\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3348}{\htmlId{1877}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1885}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#450}{\htmlId{1886}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1675}{\htmlId{1890}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1899}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18185}{\htmlId{1901}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1904}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#450}{\htmlId{1906}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2284}{\htmlId{1910}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{1918}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Prelude.html#3348}{\htmlId{1926}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1934}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#450}{\htmlId{1935}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1686}{\htmlId{1939}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1948}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18188}{\htmlId{1950}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{1952}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1702}{\htmlId{1960}{\htmlClass{Bound}{\text{ss}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1713}{\htmlId{1971}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3348}{\htmlId{1978}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1986}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#450}{\htmlId{1987}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1720}{\htmlId{1991}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1996}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#18191}{\htmlId{1998}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{2000}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1727}{\htmlId{2004}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1738}{\htmlId{2015}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1757}{\htmlId{2033}{\htmlClass{Bound}{\text{govSt}}}}\, \\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1773}{\htmlId{2049}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1786}{\htmlId{2062}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1800}{\htmlId{2076}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2046}{\htmlId{2084}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2216}{\htmlId{2087}{\htmlClass{Function}{\text{regRU}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1810}{\htmlId{2095}{\htmlClass{Bound}{\text{deposits'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1825}{\htmlId{2109}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1834}{\htmlId{2118}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1852}{\htmlId{2133}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1859}{\htmlId{2140}{\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 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{4209}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1123}{\htmlId{4210}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{4217}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4853}{\htmlId{4218}{\htmlClass{Field}{\text{pools}}}}\,\,\htmlId{4223}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4225}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3822}{\htmlId{4227}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4235}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{4239}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1123}{\htmlId{4240}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{4247}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4875}{\htmlId{4248}{\htmlClass{Field}{\text{retiring}}}}\,\,\htmlId{4256}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4258}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3822}{\htmlId{4260}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4268}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$ gState' : GState gState' = $\begin{pmatrix} \,\htmlId{4314}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{4315}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{4318}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3272}{\htmlId{4323}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{4330}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#6068}{\htmlId{4335}{\htmlClass{Function}{\text{mapValues}}}}\, \,\htmlId{4345}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{4346}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{4348}{\htmlClass{Field Operator}{\text{+\_}}}}\,\,\htmlId{4350}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{4352}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1143}{\htmlId{4353}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{4360}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#931}{\htmlId{4361}{\htmlClass{Field}{\text{dreps}}}}\,\,\htmlId{4366}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{4368}{\htmlClass{Function Operator}{\text{else}}}}\, \,\htmlId{4373}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1143}{\htmlId{4374}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{4381}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#931}{\htmlId{4382}{\htmlClass{Field}{\text{dreps}}}}\,\,\htmlId{4387}{\htmlClass{Symbol}{\text{))}}}\, , \,\htmlId{4408}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1143}{\htmlId{4409}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{4416}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#967}{\htmlId{4417}{\htmlClass{Field}{\text{ccHotKeys}}}}\,\,\htmlId{4426}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{4428}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#2578}{\htmlId{4430}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{4438}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#2948}{\htmlId{4439}{\htmlClass{Bound}{\text{es}}}}\, \,\htmlId{4442}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Enact.html#1665}{\htmlId{4443}{\htmlClass{Field}{\text{cc}}}}\,\,\htmlId{4445}{\htmlClass{Symbol}{\text{)}}}\, , \,\href{Ledger.Conway.Conformance.Epoch.html#4042}{\htmlId{4465}{\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{4627}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4634}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#3104}{\htmlId{4635}{\htmlClass{Field}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#928}{\htmlId{4642}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4649}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#3126}{\htmlId{4650}{\htmlClass{Field}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#928}{\htmlId{4657}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4664}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#3148}{\htmlId{4665}{\htmlClass{Field}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4674}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#519}{\htmlId{4676}{\htmlClass{Function}{\text{mapˢ}}}}\, \,\htmlId{4681}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{4682}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Function.Base.html#1134}{\htmlId{4688}{\htmlClass{Function Operator}{\text{∘}}}}\, \,\href{Data.Product.Base.html#650}{\htmlId{4690}{\htmlClass{Field}{\text{proj₂}}}}\,\,\htmlId{4695}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3343}{\htmlId{4697}{\htmlClass{Bound}{\text{removedGovActions}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4715}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{4719}{\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#2948}{\htmlId{5352}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{5357}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{5361}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut' → ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss' ──────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2453}{\htmlId{5475}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2544}{\htmlId{5482}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2439}{\htmlId{5487}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2467}{\htmlId{5492}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2384}{\htmlId{5498}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4730}{\htmlId{5527}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2547}{\htmlId{5535}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4615}{\htmlId{5543}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3272}{\htmlId{5553}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4500}{\htmlId{5562}{\htmlClass{Bound}{\text{certState'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2948}{\htmlId{5577}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2388}{\htmlId{5582}{\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#2364}{\htmlId{5838}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2409}{\htmlId{5850}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{5856}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2565}{\htmlId{5861}{\htmlClass{Generalizable}{\text{ru}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2362}{\htmlId{5884}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2418}{\htmlId{5888}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5896}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$ NEWEPOCH-Not-New : ∙ e ≢ lastEpoch + 1 ──────────────────────────────── _ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2364}{\htmlId{6003}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2409}{\htmlId{6015}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2585}{\htmlId{6021}{\htmlClass{Generalizable}{\text{mru}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2364}{\htmlId{6045}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2409}{\htmlId{6057}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2585}{\htmlId{6063}{\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#2364}{\htmlId{6207}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2409}{\htmlId{6219}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{6225}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2362}{\htmlId{6253}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2413}{\htmlId{6257}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{6264}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$