{-# 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#1582}{\htmlId{1582}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1593}{\htmlId{1593}{\htmlClass{Bound}{\text{reserves}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1609}{\htmlId{1609}{\htmlClass{Bound}{\text{ss}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1620}{\htmlId{1620}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1627}{\htmlId{1627}{\htmlClass{Bound}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1634}{\htmlId{1634}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1645}{\htmlId{1645}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1664}{\htmlId{1664}{\htmlClass{Bound}{\text{govSt}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1680}{\htmlId{1680}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1693}{\htmlId{1693}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1707}{\htmlId{1707}{\htmlClass{Bound}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1717}{\htmlId{1717}{\htmlClass{Bound}{\text{deposits'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1732}{\htmlId{1732}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1741}{\htmlId{1741}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1759}{\htmlId{1759}{\htmlClass{Bound}{\text{es}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1766}{\htmlId{1766}{\htmlClass{Bound}{\text{fut}}}}\,
\end{pmatrix}$ =
$\begin{pmatrix} \begin{pmatrix} \,\href{Prelude.html#3279}{\htmlId{1784}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1792}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#357}{\htmlId{1793}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1582}{\htmlId{1797}{\htmlClass{Bound}{\text{treasury}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1806}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6247}{\htmlId{1808}{\htmlClass{Function}{\text{Δt}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1811}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#357}{\htmlId{1813}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2191}{\htmlId{1817}{\htmlClass{Function}{\text{unregRU'}}}}\,\,\htmlId{1825}{\htmlClass{Symbol}{\text{)}}}\,
\\ \,\href{Prelude.html#3279}{\htmlId{1833}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1841}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#357}{\htmlId{1842}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1593}{\htmlId{1846}{\htmlClass{Bound}{\text{reserves}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1855}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6250}{\htmlId{1857}{\htmlClass{Function}{\text{Δr}}}}\,\,\htmlId{1859}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1609}{\htmlId{1867}{\htmlClass{Bound}{\text{ss}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1620}{\htmlId{1878}{\htmlClass{Bound}{\text{utxo}}}}\, \\ \,\href{Prelude.html#3279}{\htmlId{1885}{\htmlClass{Function}{\text{posPart}}}}\, \,\htmlId{1893}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#357}{\htmlId{1894}{\htmlClass{InductiveConstructor}{\text{pos}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1627}{\htmlId{1898}{\htmlClass{Bound}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1903}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Rewards.html#6253}{\htmlId{1905}{\htmlClass{Function}{\text{Δf}}}}\,\,\htmlId{1907}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1634}{\htmlId{1911}{\htmlClass{Bound}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1645}{\htmlId{1922}{\htmlClass{Bound}{\text{donations}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1664}{\htmlId{1940}{\htmlClass{Bound}{\text{govSt}}}}\,
\\ \begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1680}{\htmlId{1956}{\htmlClass{Bound}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1693}{\htmlId{1969}{\htmlClass{Bound}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1707}{\htmlId{1983}{\htmlClass{Bound}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2046}{\htmlId{1991}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2123}{\htmlId{1994}{\htmlClass{Function}{\text{regRU}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1717}{\htmlId{2002}{\htmlClass{Bound}{\text{deposits'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1732}{\htmlId{2016}{\htmlClass{Bound}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1741}{\htmlId{2025}{\htmlClass{Bound}{\text{gState}}}}\, \end{pmatrix} \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1759}{\htmlId{2040}{\htmlClass{Bound}{\text{es}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Epoch.html#1766}{\htmlId{2047}{\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{4116}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1030}{\htmlId{4117}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{4124}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4045}{\htmlId{4125}{\htmlClass{Field}{\text{pools}}}}\,\,\htmlId{4130}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4132}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3729}{\htmlId{4134}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4142}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{4146}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1030}{\htmlId{4147}{\htmlClass{Function}{\text{pState}}}}\, \,\htmlId{4154}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4067}{\htmlId{4155}{\htmlClass{Field}{\text{retiring}}}}\,\,\htmlId{4163}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4165}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3729}{\htmlId{4167}{\htmlClass{Bound}{\text{retired}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4175}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$
gState' : GState
gState' = $\begin{pmatrix} \,\htmlId{4221}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.ToBool.html#342}{\htmlId{4222}{\htmlClass{Function Operator}{\text{if}}}}\, \,\href{Data.List.Base.html#4681}{\htmlId{4225}{\htmlClass{Function}{\text{null}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3179}{\htmlId{4230}{\htmlClass{Bound}{\text{govSt'}}}}\, \,\href{Class.ToBool.html#342}{\htmlId{4237}{\htmlClass{Function Operator}{\text{then}}}}\, \,\href{Axiom.Set.Map.html#6068}{\htmlId{4242}{\htmlClass{Function}{\text{mapValues}}}}\, \,\htmlId{4252}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{4253}{\htmlClass{Number}{\text{1}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{4255}{\htmlClass{Field Operator}{\text{+\_}}}}\,\,\htmlId{4257}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{4259}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1050}{\htmlId{4260}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{4267}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#838}{\htmlId{4268}{\htmlClass{Field}{\text{dreps}}}}\,\,\htmlId{4273}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Class.ToBool.html#342}{\htmlId{4275}{\htmlClass{Function Operator}{\text{else}}}}\, \,\htmlId{4280}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1050}{\htmlId{4281}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{4288}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#838}{\htmlId{4289}{\htmlClass{Field}{\text{dreps}}}}\,\,\htmlId{4294}{\htmlClass{Symbol}{\text{))}}}\,
, \,\htmlId{4315}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#1050}{\htmlId{4316}{\htmlClass{Function}{\text{gState}}}}\, \,\htmlId{4323}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#874}{\htmlId{4324}{\htmlClass{Field}{\text{ccHotKeys}}}}\,\,\htmlId{4333}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{4335}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Enact.html#1366}{\htmlId{4337}{\htmlClass{Function}{\text{ccCreds}}}}\, \,\htmlId{4345}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Epoch.html#2855}{\htmlId{4346}{\htmlClass{Bound}{\text{es}}}}\, \,\htmlId{4349}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Enact.html#484}{\htmlId{4350}{\htmlClass{Field}{\text{cc}}}}\,\,\htmlId{4352}{\htmlClass{Symbol}{\text{)}}}\,
, \,\href{Ledger.Conway.Conformance.Epoch.html#3949}{\htmlId{4372}{\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{4534}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4541}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#1294}{\htmlId{4542}{\htmlClass{Field}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#834}{\htmlId{4549}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4556}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#1316}{\htmlId{4557}{\htmlClass{Field}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Conformance.Ledger.html#834}{\htmlId{4564}{\htmlClass{Function}{\text{utxoSt}}}}\, \,\htmlId{4571}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#1338}{\htmlId{4572}{\htmlClass{Field}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4581}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{abstract-set-theory.FiniteSetTheory.html#519}{\htmlId{4583}{\htmlClass{Function}{\text{mapˢ}}}}\, \,\htmlId{4588}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{4589}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Function.Base.html#1134}{\htmlId{4595}{\htmlClass{Function Operator}{\text{∘}}}}\, \,\href{Data.Product.Base.html#650}{\htmlId{4597}{\htmlClass{Field}{\text{proj₂}}}}\,\,\htmlId{4602}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#3250}{\htmlId{4604}{\htmlClass{Bound}{\text{removedGovActions}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{4622}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\htmlId{4626}{\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#2855}{\htmlId{5259}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{5264}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\href{Agda.Builtin.Bool.html#192}{\htmlId{5268}{\htmlClass{InductiveConstructor}{\text{false}}}}\, \end{pmatrix}$ ⇀⦇ govSt' ,RATIFIES⦈ fut'
→ ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
────────────────────────────────
_ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2360}{\htmlId{5382}{\htmlClass{Generalizable}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2451}{\htmlId{5389}{\htmlClass{Generalizable}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2346}{\htmlId{5394}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2374}{\htmlId{5399}{\htmlClass{Generalizable}{\text{es₀}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2291}{\htmlId{5405}{\htmlClass{Generalizable}{\text{fut}}}}\, \end{pmatrix}$ ⇀⦇ e ,EPOCH⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4637}{\htmlId{5434}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2454}{\htmlId{5442}{\htmlClass{Generalizable}{\text{ss'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#4522}{\htmlId{5450}{\htmlClass{Bound}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#3179}{\htmlId{5460}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#4407}{\htmlId{5469}{\htmlClass{Bound}{\text{certState'}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2855}{\htmlId{5484}{\htmlClass{Bound}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2295}{\htmlId{5489}{\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#2271}{\htmlId{5745}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2316}{\htmlId{5757}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#173}{\htmlId{5763}{\htmlClass{InductiveConstructor}{\text{just}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#2472}{\htmlId{5768}{\htmlClass{Generalizable}{\text{ru}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2269}{\htmlId{5791}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2325}{\htmlId{5795}{\htmlClass{Generalizable}{\text{eps''}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5803}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$
NEWEPOCH-Not-New :
∙ e ≢ lastEpoch + 1
────────────────────────────────
_ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2271}{\htmlId{5910}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2316}{\htmlId{5922}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2492}{\htmlId{5928}{\htmlClass{Generalizable}{\text{mru}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2271}{\htmlId{5952}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2316}{\htmlId{5964}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2492}{\htmlId{5970}{\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#2271}{\htmlId{6114}{\htmlClass{Generalizable}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2316}{\htmlId{6126}{\htmlClass{Generalizable}{\text{eps}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{6132}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$ ⇀⦇ e ,NEWEPOCH⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#2269}{\htmlId{6160}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#2320}{\htmlId{6164}{\htmlClass{Generalizable}{\text{eps'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{6171}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \end{pmatrix}$