Properties
{-# OPTIONS --safe #-}
open import Ledger.Prelude
open import Ledger.Conway.Specification.Transaction
open import Ledger.Conway.Specification.Abstract
open import Agda.Builtin.FromNat
module Ledger.Conway.Specification.Epoch.Properties
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where
open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Epoch txs abs
open import Ledger.Conway.Specification.Ledger txs abs
open import Ledger.Conway.Specification.PoolReap txs abs
open import Ledger.Conway.Specification.Ratify txs
open import Ledger.Conway.Specification.Ratify.Properties txs
open import Ledger.Conway.Specification.Rewards txs abs
open import Data.List using (filter)
import Relation.Binary.PropositionalEquality as PE
open Computational ⦃...⦄
module _ {lstate : LState} {ss : Snapshots} where
SNAP-total : ∃[ ss' ] lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
SNAP-total = -, SNAP
SNAP-complete : ∀ ss' → lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss' → proj₁ SNAP-total ≡ ss'
SNAP-complete ss' SNAP = refl
SNAP-deterministic : ∀ {ss' ss''}
→ lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
→ lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'' → ss' ≡ ss''
SNAP-deterministic SNAP SNAP = refl
module _ {e : Epoch} (prs : PoolReapState) where
POOLREAP-total : ∃[ prs' ] _ ⊢ prs ⇀⦇ e ,POOLREAP⦈ prs'
POOLREAP-total = -, POOLREAP
POOLREAP-complete
: ∀ prs' → _ ⊢ prs ⇀⦇ e ,POOLREAP⦈ prs' → proj₁ POOLREAP-total ≡ prs'
POOLREAP-complete prs' POOLREAP = refl
POOLREAP-deterministic
: ∀ {prs' prs''}
→ _ ⊢ prs ⇀⦇ e ,POOLREAP⦈ prs'
→ _ ⊢ prs ⇀⦇ e ,POOLREAP⦈ prs''
→ prs' ≡ prs''
POOLREAP-deterministic POOLREAP POOLREAP = refl
module _ {eps : EpochState} {e : Epoch} where
open EpochState eps hiding (es)
prs = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2012}{\htmlId{1859}{\htmlClass{Function}{\text{u0}}}}\, \,\htmlId{1862}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Epoch.html#14408}{\htmlId{1863}{\htmlClass{Field}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#2235}{\htmlId{1873}{\htmlClass{Function}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#1987}{\htmlId{1880}{\htmlClass{Function}{\text{cs}}}}\, \,\htmlId{1883}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4943}{\htmlId{1884}{\htmlClass{Field}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#1987}{\htmlId{1893}{\htmlClass{Function}{\text{cs}}}}\, \,\htmlId{1896}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4963}{\htmlId{1897}{\htmlClass{Field}{\text{pState}}}}\, \end{pmatrix}$
where
open LState
open CertState
open EPOCH-Updates0
cs = ls .certState
u0 = EPOCH-updates0 fut ls
EPOCH-total : ∃[ eps' ] _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
EPOCH-total =
-, EPOCH
(RATIFIES-total' .proj₂)
(SNAP-total .proj₂)
(POOLREAP-total prs .proj₂)
private
EPOCH-state : Snapshots → RatifyState → PoolReapState → EpochState
EPOCH-state ss fut' ($\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2330}{\htmlId{2330}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2341}{\htmlId{2341}{\htmlClass{Bound}{\text{acnt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2349}{\htmlId{2349}{\htmlClass{Bound}{\text{dState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2359}{\htmlId{2359}{\htmlClass{Bound}{\text{pState'}}}}\, \end{pmatrix}$) =
let
EPOCHUpdates es govSt' dState'' gState' _ acnt'' =
EPOCH-updates fut ls dState' acnt'
certState' = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2414}{\htmlId{2510}{\htmlClass{Bound}{\text{dState''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2359}{\htmlId{2521}{\htmlClass{Bound}{\text{pState'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2423}{\htmlId{2531}{\htmlClass{Bound}{\text{gState'}}}}\, \end{pmatrix}$
in
record
{ acnt = acnt''
; ss = ss
; ls = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2330}{\htmlId{2641}{\htmlClass{Bound}{\text{utxoSt''}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2407}{\htmlId{2652}{\htmlClass{Bound}{\text{govSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2495}{\htmlId{2661}{\htmlClass{Bound}{\text{certState'}}}}\, \end{pmatrix}$
; es = es
; fut = fut'
}
EPOCH-deterministic : ∀ eps' eps''
→ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
→ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps''
→ eps' ≡ eps''
EPOCH-deterministic
eps'
eps''
(EPOCH
{utxoSt'' = utxoSt''₁}
{acnt' = acnt'₁}
{dState' = dState'₁}
{pState' = pState'₁}
p₁ p₂ p₃
)
(EPOCH
{utxoSt'' = utxoSt''₂}
{acnt' = acnt'₂}
{dState' = dState'₂}
{pState' = pState'₂}
p₁' p₂' p₃'
) =
cong₂ _$_ (cong₂ EPOCH-state ss'≡ss'' fut'≡fut'') prs'≡prs''
where
ss'≡ss'' : EpochState.ss eps' ≡ EpochState.ss eps''
ss'≡ss'' = SNAP-deterministic p₂ p₂'
fut'≡fut'' : EpochState.fut eps' ≡ EpochState.fut eps''
fut'≡fut'' = RATIFIES-deterministic-≡
(cong (λ x → record
{ stakeDistrs = mkStakeDistrs (Snapshots.mark x) _ _ _
; currentEpoch = _
; dreps = _
; ccHotKeys = _
; treasury = _
}) ss'≡ss'')
refl refl p₁ p₁'
prs'≡prs'' : $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.html#2990}{\htmlId{4003}{\htmlClass{Bound}{\text{utxoSt''₁}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#3018}{\htmlId{4015}{\htmlClass{Bound}{\text{acnt'₁}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#3045}{\htmlId{4024}{\htmlClass{Bound}{\text{dState'₁}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#3074}{\htmlId{4035}{\htmlClass{Bound}{\text{pState'₁}}}}\, \end{pmatrix}$ ≡
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.html#3142}{\htmlId{4070}{\htmlClass{Bound}{\text{utxoSt''₂}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#3170}{\htmlId{4082}{\htmlClass{Bound}{\text{acnt'₂}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#3197}{\htmlId{4091}{\htmlClass{Bound}{\text{dState'₂}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#3226}{\htmlId{4102}{\htmlClass{Bound}{\text{pState'₂}}}}\, \end{pmatrix}$
prs'≡prs'' = POOLREAP-deterministic prs p₃ p₃'
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.html#4792}{\htmlId{5039}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.Properties.html#4357}{\htmlId{5043}{\htmlClass{Function}{\text{EPOCH-total'}}}}\, \,\htmlId{5056}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{5057}{\htmlClass{Field}{\text{proj₁}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5065}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\htmlId{5075}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$
, NEWEPOCH-New (p , EPOCH-total' .proj₂)
... | yes p | nothing | PE.[ refl ] = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.Properties.html#4792}{\htmlId{5200}{\htmlClass{Bound}{\text{e}}}}\, \\ \,\href{Data.Product.Base.html#636}{\htmlId{5204}{\htmlClass{Field}{\text{proj₁}}}}\, \,\href{Ledger.Conway.Specification.Epoch.Properties.html#4357}{\htmlId{5210}{\htmlClass{Function}{\text{EPOCH-total'}}}}\, \\ \,\href{Agda.Builtin.Maybe.html#194}{\htmlId{5225}{\htmlClass{InductiveConstructor}{\text{nothing}}}}\, \\ \,\htmlId{5235}{\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)