Computational
{-# OPTIONS --safe #-} open import Ledger.Dijkstra.Specification.Transaction open import Ledger.Dijkstra.Specification.Abstract module Ledger.Dijkstra.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.Dijkstra.Specification.Certs govStructure open import Ledger.Dijkstra.Specification.Epoch txs abs open import Ledger.Dijkstra.Specification.Enact govStructure open import Ledger.Dijkstra.Specification.Ledger txs abs open import Ledger.Dijkstra.Specification.PoolReap txs open import Ledger.Dijkstra.Specification.PoolReap.Properties.Computational txs open import Ledger.Dijkstra.Specification.Ratify govStructure open import Ledger.Dijkstra.Specification.Ratify.Properties.Computational txs open import Ledger.Dijkstra.Specification.Rewards txs abs open import Ledger.Dijkstra.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'₁} {pState'' = pState'₁} (p₁ , p₂ , p₃) ) (EPOCH {dState' = dState'₂} {acnt' = acnt'₂} {ss' = ss'₂} {pState'' = pState'₂} (p₁' , p₂' , p₃') ) = eps'≡eps'' where ls : LedgerState ls = LedgerStateOf 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.Dijkstra.Specification.Epoch.Properties.Computational.html#1740}{\htmlId{2752}{\htmlClass{Bound}{\text{acnt'₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1713}{\htmlId{2761}{\htmlClass{Bound}{\text{dState'₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1789}{\htmlId{2772}{\htmlClass{Bound}{\text{pState'₁}}}}\, \end{pmatrix}$ ≡ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1889}{\htmlId{2810}{\htmlClass{Bound}{\text{acnt'₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1862}{\htmlId{2819}{\htmlClass{Bound}{\text{dState'₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1938}{\htmlId{2830}{\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.Dijkstra.Specification.Epoch.Properties.Computational.html#3498}{\htmlId{3510}{\htmlClass{Bound}{\text{sd}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1258}{\htmlId{3515}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{3519}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#2017}{\htmlId{3527}{\htmlClass{Function}{\text{ls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3459}{\htmlId{3532}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#2017}{\htmlId{3544}{\htmlClass{Function}{\text{ls}}}}\, \\ \,\href{Ledger.Prelude.Base.html#985}{\htmlId{3549}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#3501}{\htmlId{3560}{\htmlClass{Bound}{\text{acnt}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3575}{\htmlId{3567}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#2017}{\htmlId{3575}{\htmlClass{Function}{\text{ls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4773}{\htmlId{3580}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#2017}{\htmlId{3593}{\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.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.Dijkstra.Specification.Epoch.Properties.Computational.html#4757}{\htmlId{5004}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\htmlId{5008}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5012}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#4322}{\htmlId{5016}{\htmlClass{Function}{\text{EPOCH-total'}}}}\, \,\htmlId{5029}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{5030}{\htmlClass{Field}{\text{proj₁}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5038}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\htmlId{5048}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ , NEWEPOCH-New (p , EPOCH-total' .proj₂) ... | yes p | nothing | PE.[ refl ] = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#4757}{\htmlId{5173}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\htmlId{5177}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5181}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Data.Product.Base.html#636}{\htmlId{5185}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#4322}{\htmlId{5191}{\htmlClass{Function}{\text{EPOCH-total'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5206}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\htmlId{5216}{\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)