{-# 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#1570}{\htmlId{1570}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1581}{\htmlId{1581}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1597}{\htmlId{1597}{\htmlClass{Bound}{\text{ss}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1608}{\htmlId{1608}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1615}{\htmlId{1615}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1622}{\htmlId{1622}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1633}{\htmlId{1633}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1652}{\htmlId{1652}{\htmlClass{Bound}{\text{govSt}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1668}{\htmlId{1668}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1681}{\htmlId{1681}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1695}{\htmlId{1695}{\htmlClass{Bound}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1705}{\htmlId{1705}{\htmlClass{Bound}{\text{deposits'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1720}{\htmlId{1720}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1729}{\htmlId{1729}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1747}{\htmlId{1747}{\htmlClass{Bound}{\text{es}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1754}{\htmlId{1754}{\htmlClass{Bound}{\text{fut}}}}\,
\end{pmatrix}$ =
$\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3279}{\htmlId{1772}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1780}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#357}{\htmlId{1781}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1570}{\htmlId{1785}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1794}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6263}{\htmlId{1796}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1799}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#357}{\htmlId{1801}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2179}{\htmlId{1805}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{1813}{\htmlClass{Symbol}{\text{)}}}\,
\\ \,\href{Prelude.html#3279}{\htmlId{1821}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1829}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#357}{\htmlId{1830}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1581}{\htmlId{1834}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1843}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6266}{\htmlId{1845}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{1847}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1597}{\htmlId{1855}{\htmlClass{Bound}{\text{ss}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1608}{\htmlId{1866}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3279}{\htmlId{1873}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1881}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#357}{\htmlId{1882}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1615}{\htmlId{1886}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1891}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6269}{\htmlId{1893}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{1895}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1622}{\htmlId{1899}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1633}{\htmlId{1910}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1652}{\htmlId{1928}{\htmlClass{Bound}{\text{govSt}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1668}{\htmlId{1944}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1681}{\htmlId{1957}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1695}{\htmlId{1971}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2046}{\htmlId{1979}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2111}{\htmlId{1982}{\htmlClass{Function}{\text{regRU}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1705}{\htmlId{1990}{\htmlClass{Bound}{\text{deposits'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1720}{\htmlId{2004}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1729}{\htmlId{2013}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1747}{\htmlId{2028}{\htmlClass{Bound}{\text{es}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1754}{\htmlId{2035}{\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{3661}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1030}{\htmlId{3662}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{3669}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#3901}{\htmlId{3670}{\htmlClass{Field}{\text{pools}}}}\,\,\htmlId{3675}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{3677}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3204}{\htmlId{3679}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{3687}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{3691}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1030}{\htmlId{3692}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{3699}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#3923}{\htmlId{3700}{\htmlClass{Field}{\text{retiring}}}}\,\,\htmlId{3708}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{3710}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3204}{\htmlId{3712}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{3720}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$
gState' : GState
gState' = $\begin{pmatrix} \,\htmlId{3766}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{3767}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{3770}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3461}{\htmlId{3775}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{3782}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#6068}{\htmlId{3787}{\htmlClass{Function}{\text{mapValues}}}}\, \,\htmlId{3797}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{3798}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{3800}{\htmlClass{Field Operator}{\text{+\_}}}}\,\,\htmlId{3802}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{3804}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1050}{\htmlId{3805}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{3812}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#838}{\htmlId{3813}{\htmlClass{Field}{\text{dreps}}}}\,\,\htmlId{3818}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{3820}{\htmlClass{Function Operator}{\text{else}}}}\, \,\htmlId{3825}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1050}{\htmlId{3826}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{3833}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#838}{\htmlId{3834}{\htmlClass{Field}{\text{dreps}}}}\,\,\htmlId{3839}{\htmlClass{Symbol}{\text{))}}}\,
, \,\htmlId{3860}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1050}{\htmlId{3861}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{3868}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#874}{\htmlId{3869}{\htmlClass{Field}{\text{ccHotKeys}}}}\,\,\htmlId{3878}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{3880}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#1367}{\htmlId{3882}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{3890}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#3155}{\htmlId{3891}{\htmlClass{Bound}{\text{es}}}}\, \,\htmlId{3894}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Enact.html#484}{\htmlId{3895}{\htmlClass{Field}{\text{cc}}}}\,\,\htmlId{3897}{\htmlClass{Symbol}{\text{)}}}\,
, \,\href{Ledger.Conway.Conformance.Epoch.html#3424}{\htmlId{3917}{\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#834}{\htmlId{4079}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4086}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#1294}{\htmlId{4087}{\htmlClass{Field}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#834}{\htmlId{4094}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4101}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#1316}{\htmlId{4102}{\htmlClass{Field}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#834}{\htmlId{4109}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4116}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#1338}{\htmlId{4117}{\htmlClass{Field}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4126}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#519}{\htmlId{4128}{\htmlClass{Function}{\text{mapˢ}}}}\, \,\htmlId{4133}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{4134}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Function.Base.html#1134}{\htmlId{4140}{\htmlClass{Function Operator}{\text{∘}}}}\, \,\href{Data.Product.Base.html#650}{\htmlId{4142}{\htmlClass{Field}{\text{proj₂}}}}\,\,\htmlId{4147}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2823}{\htmlId{4149}{\htmlClass{Bound}{\text{removedGovActions}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4167}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{4171}{\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#3155}{\htmlId{4617}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{4622}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{4626}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut'
→ ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
────────────────────────────────
_ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2348}{\htmlId{4740}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2439}{\htmlId{4747}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2334}{\htmlId{4752}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2362}{\htmlId{4757}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2279}{\htmlId{4763}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4182}{\htmlId{4792}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2442}{\htmlId{4800}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4067}{\htmlId{4808}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3461}{\htmlId{4818}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3952}{\htmlId{4827}{\htmlClass{Bound}{\text{certState'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3155}{\htmlId{4842}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2283}{\htmlId{4847}{\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#2259}{\htmlId{5103}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2304}{\htmlId{5115}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{5121}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2460}{\htmlId{5126}{\htmlClass{Generalizable}{\text{ru}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2257}{\htmlId{5149}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2313}{\htmlId{5153}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5161}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$
NEWEPOCH-Not-New :
∙ e ≢ lastEpoch + 1
────────────────────────────────
_ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2259}{\htmlId{5268}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2304}{\htmlId{5280}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2480}{\htmlId{5286}{\htmlClass{Generalizable}{\text{mru}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2259}{\htmlId{5310}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2304}{\htmlId{5322}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2480}{\htmlId{5328}{\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#2259}{\htmlId{5472}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2304}{\htmlId{5484}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5490}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2257}{\htmlId{5518}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2308}{\htmlId{5522}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5529}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$