{-# OPTIONS --safe #-}
open import Ledger.Conway.Specification.Transaction
open import Ledger.Conway.Specification.Abstract
module Ledger.Conway.Specification.Epoch.Properties.Computational
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where
open import Agda.Builtin.FromNat
import Relation.Binary.PropositionalEquality as PE
open import Ledger.Prelude
open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Epoch txs abs
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Ledger txs abs
open import Ledger.Conway.Specification.PoolReap txs abs
open import Ledger.Conway.Specification.PoolReap.Properties.Computational txs abs
open import Ledger.Conway.Specification.Ratify txs
open import Ledger.Conway.Specification.Ratify.Properties.Computational txs
open import Ledger.Conway.Specification.Rewards txs abs
open import Ledger.Conway.Specification.Rewards.Properties.Computational txs abs
open Computational ⦃...⦄
module _ {eps : EpochState} {e : Epoch} where
EPOCH-total : ∃[ eps' ] _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
EPOCH-total =
-, EPOCH
( SNAP-total .proj₂
, POOLREAP-total .proj₂
, RATIFIES-total' .proj₂)
EPOCH-deterministic : ∀ eps' eps''
→ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
→ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps''
→ eps' ≡ eps''
EPOCH-deterministic
eps'
eps''
(EPOCH
{dState' = dState'₁}
{acnt' = acnt'₁}
{ss' = ss'₁}
{utxoSt'' = utxoSt''₁}
{pState'' = pState'₁}
(p₁ , p₂ , p₃)
)
(EPOCH
{dState' = dState'₂}
{acnt' = acnt'₂}
{ss' = ss'₂}
{utxoSt'' = utxoSt''₂}
{pState'' = pState'₂}
(p₁' , p₂' , p₃')
) = eps'≡eps''
where
ls : LState
ls = LStateOf eps
es : EnactState
es = EnactStateOf (RatifyStateOf eps)
govUpd : Governance-Update
govUpd = GovernanceUpdate.updates ls (RatifyStateOf eps)
govSt' = Governance-Update.govSt' govUpd
ss'₁≡ss'₂ : ss'₁ ≡ ss'₂
ss'₁≡ss'₂ = SNAP-deterministic p₁ p₁'
module pPRUpd = Pre-POOLREAP-Update (Pre-POOLREAPUpdate.updates ls es govUpd)
pPRUpd₁ = Post-POOLREAPUpdate.updates es ls dState'₁ acnt'₁ govUpd
module pPRUpd₁ = Post-POOLREAP-Update pPRUpd₁
pPRUpd₂ = Post-POOLREAPUpdate.updates es ls dState'₂ acnt'₂ govUpd
module pPRUpd₂ = Post-POOLREAP-Update pPRUpd₂
prs'≡prs'' : $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1637}{\htmlId{2652}{\htmlClass{Bound}{\text{utxoSt''₁}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1588}{\htmlId{2664}{\htmlClass{Bound}{\text{acnt'₁}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1561}{\htmlId{2673}{\htmlClass{Bound}{\text{dState'₁}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1668}{\htmlId{2684}{\htmlClass{Bound}{\text{pState'₁}}}}\, \end{pmatrix}$ ≡
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1817}{\htmlId{2722}{\htmlClass{Bound}{\text{utxoSt''₂}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1768}{\htmlId{2734}{\htmlClass{Bound}{\text{acnt'₂}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1741}{\htmlId{2743}{\htmlClass{Bound}{\text{dState'₂}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1848}{\htmlId{2754}{\htmlClass{Bound}{\text{pState'₂}}}}\, \end{pmatrix}$
prs'≡prs'' = POOLREAP-deterministic-≡ refl refl p₂ p₂'
pPRUpd₁≡pPRUpd₂ : pPRUpd₁ ≡ pPRUpd₂
pPRUpd₁≡pPRUpd₂ rewrite (cong PoolReapState.dState prs'≡prs'') | (cong PoolReapState.acnt prs'≡prs'') = refl
stakeDistrs₁≡stakeDistrs₂ : mkStakeDistrs (Snapshots.mark ss'₁) e pPRUpd.utxoSt' govSt' (GStateOf ls) (DStateOf ls)
≡ mkStakeDistrs (Snapshots.mark ss'₂) e pPRUpd.utxoSt' govSt' (GStateOf ls) (DStateOf ls)
stakeDistrs₁≡stakeDistrs₂ = cong (λ ss' → mkStakeDistrs (Snapshots.mark ss') e pPRUpd.utxoSt' govSt' (GStateOf ls) (DStateOf ls)) ss'₁≡ss'₂
Γ≡Γ' = cong₂ (λ sd acnt → $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#3421}{\htmlId{3433}{\htmlClass{Bound}{\text{sd}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1106}{\htmlId{3438}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#7086}{\htmlId{3442}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1927}{\htmlId{3450}{\htmlClass{Function}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1477}{\htmlId{3455}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1927}{\htmlId{3467}{\htmlClass{Function}{\text{ls}}}}\, \\ \,\href{Ledger.Prelude.Base.html#889}{\htmlId{3472}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#3424}{\htmlId{3483}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#1562}{\htmlId{3490}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1927}{\htmlId{3498}{\htmlClass{Function}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#2810}{\htmlId{3503}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#1927}{\htmlId{3516}{\htmlClass{Function}{\text{ls}}}}\, \end{pmatrix}$)
stakeDistrs₁≡stakeDistrs₂ (cong Post-POOLREAP-Update.acnt'' pPRUpd₁≡pPRUpd₂)
fut'≡fut'' : RatifyStateOf eps' ≡ RatifyStateOf eps''
fut'≡fut'' = RATIFIES-deterministic-≡ Γ≡Γ' refl refl p₃ p₃'
eps'≡eps'' : eps' ≡ eps''
eps'≡eps''
rewrite ss'₁≡ss'₂
| cong PoolReapState.utxoSt prs'≡prs''
| cong PoolReapState.pState prs'≡prs''
| cong Post-POOLREAP-Update.acnt'' pPRUpd₁≡pPRUpd₂
| cong Post-POOLREAP-Update.dState'' pPRUpd₁≡pPRUpd₂
| fut'≡fut'' = refl
EPOCH-complete : ∀ eps' → _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps' → proj₁ EPOCH-total ≡ eps'
EPOCH-complete eps' p = EPOCH-deterministic (proj₁ EPOCH-total) eps' (proj₂ EPOCH-total) p
abstract
EPOCH-total' : ∃[ eps' ] _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
EPOCH-total' = EPOCH-total
EPOCH-complete' : ∀ eps' → _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps' → proj₁ EPOCH-total' ≡ eps'
EPOCH-complete' = EPOCH-complete
instance
Computational-EPOCH : Computational _⊢_⇀⦇_,EPOCH⦈_ ⊥
Computational-EPOCH .computeProof Γ s sig = success EPOCH-total'
Computational-EPOCH .completeness Γ s sig s' h = cong success (EPOCH-complete' s' h)
module _ {e : Epoch} where
NEWEPOCH-total : ∀ nes'' → ∃[ nes' ] _ ⊢ nes'' ⇀⦇ e ,NEWEPOCH⦈ nes'
NEWEPOCH-total nes with e ≟ NewEpochState.lastEpoch nes + 1 | NewEpochState.ru nes | inspect NewEpochState.ru nes
... | yes p | just ru | PE.[ refl ] = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#4732}{\htmlId{4979}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\htmlId{4983}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4987}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#4297}{\htmlId{4991}{\htmlClass{Function}{\text{EPOCH-total'}}}}\, \,\htmlId{5004}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{5005}{\htmlClass{Field}{\text{proj₁}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5013}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\htmlId{5023}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$
, NEWEPOCH-New (p , EPOCH-total' .proj₂)
... | yes p | nothing | PE.[ refl ] = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#4732}{\htmlId{5148}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\htmlId{5152}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5156}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Data.Product.Base.html#636}{\htmlId{5160}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Ledger.Conway.Specification.Epoch.Properties.Computational.html#4297}{\htmlId{5166}{\htmlClass{Function}{\text{EPOCH-total'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5181}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\htmlId{5191}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$
, NEWEPOCH-No-Reward-Update (p , EPOCH-total' .proj₂)
... | no ¬p | _ | _ = -, NEWEPOCH-Not-New ¬p
NEWEPOCH-complete : ∀ nes nes' → _ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes' → proj₁ (NEWEPOCH-total nes) ≡ nes'
NEWEPOCH-complete nes nes' h with e ≟ NewEpochState.lastEpoch nes + 1 | NewEpochState.ru nes | inspect NewEpochState.ru nes | h
... | yes p | just ru | PE.[ refl ] | NEWEPOCH-New (x , x₁) rewrite EPOCH-complete' _ x₁ = refl
... | yes p | ru | PE.[ refl ] | NEWEPOCH-Not-New x = ⊥-elim $ x p
... | yes p | nothing | PE.[ refl ] | NEWEPOCH-No-Reward-Update (x , x₁) rewrite EPOCH-complete' _ x₁ = refl
... | no ¬p | ru | PE.[ refl ] | NEWEPOCH-New (x , x₁) = ⊥-elim $ ¬p x
... | no ¬p | ru | PE.[ refl ] | NEWEPOCH-Not-New x = refl
... | no ¬p | nothing | PE.[ refl ] | NEWEPOCH-No-Reward-Update (x , x₁) = ⊥-elim $ ¬p x
instance
Computational-NEWEPOCH : Computational _⊢_⇀⦇_,NEWEPOCH⦈_ ⊥
Computational-NEWEPOCH .computeProof Γ s sig = success (NEWEPOCH-total _)
Computational-NEWEPOCH .completeness Γ s sig s' h = cong success (NEWEPOCH-complete _ s' h)