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 ( POOLREAP-total .proj₂ , SNAP-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'₁} {pState'' = pState'₁} {ss' = ss'₁} (p₁ , p₂ , p₃) ) (EPOCH {dState' = dState'₂} {acnt' = acnt'₂} {pState'' = pState'₂} {ss' = ss'₂} (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 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{2671}{\htmlClass{Bound}{\text{acnt'₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1713}{\htmlId{2680}{\htmlClass{Bound}{\text{dState'₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1768}{\htmlId{2691}{\htmlClass{Bound}{\text{pState'₁}}}}\, \end{pmatrix}$ ≡ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1889}{\htmlId{2729}{\htmlClass{Bound}{\text{acnt'₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1862}{\htmlId{2738}{\htmlClass{Bound}{\text{dState'₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1917}{\htmlId{2749}{\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 ls'₁ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#20913}{\htmlId{3008}{\htmlClass{Function}{\text{pPRUpd.utxoSt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#2252}{\htmlId{3025}{\htmlClass{Function}{\text{govSt'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#21809}{\htmlId{3036}{\htmlClass{Function}{\text{pPRUpd₁.dState''}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1768}{\htmlId{3055}{\htmlClass{Bound}{\text{pState'₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#20892}{\htmlId{3066}{\htmlClass{Function}{\text{pPRUpd.gState'}}}}\, \end{pmatrix} \end{pmatrix}$ ls'₂ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#20913}{\htmlId{3105}{\htmlClass{Function}{\text{pPRUpd.utxoSt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#2252}{\htmlId{3122}{\htmlClass{Function}{\text{govSt'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#21809}{\htmlId{3133}{\htmlClass{Function}{\text{pPRUpd₂.dState''}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1917}{\htmlId{3152}{\htmlClass{Bound}{\text{pState'₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#20892}{\htmlId{3163}{\htmlClass{Function}{\text{pPRUpd.gState'}}}}\, \end{pmatrix} \end{pmatrix}$ ls'₁≡ls'₂ : ls'₁ ≡ ls'₂ ls'₁≡ls'₂ = cong₂ (λ ds ps → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#20913}{\htmlId{3258}{\htmlClass{Function}{\text{pPRUpd.utxoSt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#2252}{\htmlId{3275}{\htmlClass{Function}{\text{govSt'}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#3248}{\htmlId{3286}{\htmlClass{Bound}{\text{ds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#3251}{\htmlId{3291}{\htmlClass{Bound}{\text{ps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#20892}{\htmlId{3296}{\htmlClass{Function}{\text{pPRUpd.gState'}}}}\, \end{pmatrix} \end{pmatrix}$) (cong Post-POOLREAP-Update.dState'' pPRUpd₁≡pPRUpd₂) (cong PoolReapState.pState prs'≡prs'') ss'₁≡ss'₂ : ss'₁ ≡ ss'₂ ss'₁≡ss'₂ = SNAP-deterministic-≡ ls'₁≡ls'₂ p₂ p₂' mkΓ : Snapshots → Post-POOLREAP-Update → LedgerState → RatifyEnv mkΓ ss'' pPR ls'' = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Epoch.html#16098}{\htmlId{3666}{\htmlClass{Function}{\text{calculateVDelegDelegatedStake}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1258}{\htmlId{3696}{\htmlClass{Bound}{\text{e}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#20913}{\htmlId{3698}{\htmlClass{Function}{\text{pPRUpd.utxoSt'}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#2252}{\htmlId{3713}{\htmlClass{Function}{\text{govSt'}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.html#20892}{\htmlId{3720}{\htmlClass{Function}{\text{pPRUpd.gState'}}}}\, \,\htmlId{3735}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Epoch.html#21809}{\htmlId{3736}{\htmlClass{Field}{\text{Post-POOLREAP-Update.dState''}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#3642}{\htmlId{3766}{\htmlClass{Bound}{\text{pPR}}}}\,\,\htmlId{3769}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.html#16324}{\htmlId{3784}{\htmlClass{Function}{\text{calculatePoolDelegatedStakeForVoting}}}}\, \,\htmlId{3821}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Rewards.html#7984}{\htmlId{3822}{\htmlClass{Field}{\text{Snapshots.mark}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#3637}{\htmlId{3837}{\htmlClass{Bound}{\text{ss''}}}}\,\,\htmlId{3841}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#2252}{\htmlId{3843}{\htmlClass{Function}{\text{govSt'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#1258}{\htmlId{3863}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{3878}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#3646}{\htmlId{3886}{\htmlClass{Bound}{\text{ls''}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4141}{\htmlId{3904}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#3646}{\htmlId{3916}{\htmlClass{Bound}{\text{ls''}}}}\, \\ \,\href{Ledger.Prelude.Base.html#985}{\htmlId{3934}{\htmlClass{Field}{\text{TreasuryOf}}}}\, \,\htmlId{3945}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Epoch.html#21837}{\htmlId{3946}{\htmlClass{Field}{\text{Post-POOLREAP-Update.acnt''}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#3642}{\htmlId{3974}{\htmlClass{Bound}{\text{pPR}}}}\,\,\htmlId{3977}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4398}{\htmlId{3992}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#3646}{\htmlId{4000}{\htmlClass{Bound}{\text{ls''}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4773}{\htmlId{4018}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#3646}{\htmlId{4031}{\htmlClass{Bound}{\text{ls''}}}}\, \end{pmatrix}$ Γ≡Γ' : mkΓ ss'₁ pPRUpd₁ ls'₁ ≡ mkΓ ss'₂ pPRUpd₂ ls'₂ Γ≡Γ' = trans (cong (λ x → mkΓ x pPRUpd₁ ls'₁) ss'₁≡ss'₂) (trans (cong (λ x → mkΓ ss'₂ x ls'₁) pPRUpd₁≡pPRUpd₂) (cong (mkΓ ss'₂ pPRUpd₂) ls'₁≡ls'₂)) 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#5356}{\htmlId{5603}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\htmlId{5607}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5611}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#4921}{\htmlId{5615}{\htmlClass{Function}{\text{EPOCH-total'}}}}\, \,\htmlId{5628}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{5629}{\htmlClass{Field}{\text{proj₁}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5637}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\htmlId{5647}{\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#5356}{\htmlId{5772}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\htmlId{5776}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5780}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Data.Product.Base.html#636}{\htmlId{5784}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Epoch.Properties.Computational.html#4921}{\htmlId{5790}{\htmlClass{Function}{\text{EPOCH-total'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5805}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\htmlId{5815}{\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)