{-# OPTIONS --safe #-}
open import Ledger.Conway.Specification.Transaction
open import Ledger.Conway.Specification.Abstract
module Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where
open import Ledger.Prelude using (mapˢ)
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.Ledger.Properties txs abs
open import Ledger.Conway.Specification.PoolReap txs abs
open import Ledger.Prelude renaming (map to map'; mapˢ to map)
open import Ledger.Conway.Specification.Ratify txs hiding (vote)
open import Ledger.Conway.Specification.Utxo txs abs
open import Axiom.Set.Properties th
open import Data.List.Base using (filter)
open import Data.List.Membership.Propositional.Properties using (∈-filter⁺; map-∈↔)
open import stdlib.Data.List.Subpermutations using (∈ˡ-map-filter)
open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
open import Data.Product.Properties using (×-≡,≡←≡)
open import Data.Product.Properties.Ext using (×-⇔-swap)
open import Relation.Unary using (Decidable)
open Equivalence
import Function.Related.Propositional as R
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
module EPOCH-Body (eps : EpochState) where
open EpochState eps hiding (es) renaming (ls to epsLState; fut to epsRState) public
open RatifyState renaming (es to ensRState) public
open LState epsLState public
open PState public
open GovActionState public
ens = record (epsRState .ensRState) { withdrawals = ∅ }
tmpGovSt = filter (λ x → ¿ proj₁ x ∉ map proj₁ (epsRState .removed) ¿) govSt
orphans = fromList $ getOrphans ens tmpGovSt
removed' : ℙ (GovActionID × GovActionState)
removed' = (epsRState .removed) ∪ orphans
removedGovActions = flip concatMapˢ removed' λ (gaid , gaSt) →
map (returnAddr gaSt ,_) ((DepositsOf utxoSt ∣ ❴ GovActionDeposit gaid ❵) ˢ)
module EPOCH-PROPS {eps : EpochState} where
open EPOCH-Body eps
EPOCH-govDepsMatch : {eps' : EpochState} {e : Epoch}
→ map (GovActionDeposit ∘ proj₁) removed' ⊆ dom (DepositsOf eps)
→ _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
→ govDepsMatch (LStateOf eps) → govDepsMatch (LStateOf eps')
EPOCH-govDepsMatch {eps'} {e} ratify-removed (EPOCH x _ POOLREAP) =
poolReapMatch ∘ ratifiesSnapMatch
where
ΔΠ : ℙ DepositPurpose
ΔΠ = map (proj₁ ∘ proj₂) removedGovActions
ΔΠ' : ℙ DepositPurpose
ΔΠ' = map (GovActionDeposit ∘ proj₁) removed'
P : GovActionID × GovActionState → Type
P = λ u → proj₁ u ∉ map proj₁ removed'
P? : Decidable P
P? = λ u → ¿ P u ¿
utxoDeps : Deposits
utxoDeps = UTxOState.deposits (LState.utxoSt epsLState)
utxoDeps' : Deposits
utxoDeps' = utxoDeps ∣ ΔΠ' ᶜ
ΔΠ'≡ΔΠ : ΔΠ' ≡ᵉ ΔΠ
ΔΠ'≡ΔΠ = ΔΠ'⊆ΔΠ , ΔΠ⊆ΔΠ'
where
ΔΠ'⊆ΔΠ : ΔΠ' ⊆ ΔΠ
ΔΠ'⊆ΔΠ {a} x with from ∈-map x
... | (gaid , gast) , refl , gaidgast∈rem with from ∈-map (ratify-removed x)
... | (dp , c) , refl , dpc∈utxoDeps = let gadc = (GovActionDeposit gaid , c) in
to ∈-map ((returnAddr {txs} gast , gadc)
, refl
, to ∈-concatMapˢ ((gaid , gast)
, gaidgast∈rem
, to ∈-map (gadc , refl , res-singleton⁺ {m = utxoDeps} dpc∈utxoDeps)))
ΔΠ⊆ΔΠ' : ΔΠ ⊆ ΔΠ'
ΔΠ⊆ΔΠ' {a} x with from ∈-map x
... | (rwa , dp , c) , refl , rwa-dp-c∈ with (from ∈-concatMapˢ rwa-dp-c∈)
... | (gaid , gast) , gaid-gast-∈-removed , rwa-dp-c-∈-map with (from ∈-map rwa-dp-c-∈-map)
... | (_ , _) , refl , q∈ =
to ∈-map ((gaid , gast)
, proj₁ (×-≡,≡←≡ (proj₂ (res-singleton'' {m = utxoDeps} q∈)))
, gaid-gast-∈-removed)
map-filter-decomp : ∀ a → (a ∉ ΔΠ' × a ∈ˡ map' (GovActionDeposit ∘ proj₁) govSt)
⇔ (a ∈ˡ map' (GovActionDeposit ∘ proj₁)(filter P? govSt))
map-filter-decomp a = mk⇔ i (λ h → ii h , iii h)
where
i : ((a ∉ ΔΠ') × (a ∈ˡ map' (GovActionDeposit ∘ proj₁) govSt))
→ a ∈ˡ map' (GovActionDeposit ∘ proj₁) (filter P? govSt)
i (a∉ΔΠ' , a∈) with Inverse.from (map-∈↔ (GovActionDeposit ∘ proj₁)) a∈
... | b , b∈ , refl = Inverse.to (map-∈↔ (GovActionDeposit ∘ proj₁))
(b , ∈-filter⁺ P? b∈ (a∉ΔΠ' ∘ ∈-map⁺-∘) , refl)
ii : a ∈ˡ map' (GovActionDeposit ∘ proj₁) (filter P? govSt) → a ∉ ΔΠ'
ii a∈ a∈ΔΠ' with from (∈ˡ-map-filter {l = govSt} {P? = P?}) a∈
... | _ , _ , refl , Pb with ∈-map⁻' a∈ΔΠ'
... | q , refl , q∈rem = Pb (to ∈-map (q , refl , q∈rem))
iii : a ∈ˡ map' (GovActionDeposit ∘ proj₁) (filter P? govSt)
→ a ∈ˡ map' (GovActionDeposit ∘ proj₁) govSt
iii a∈ with from (∈ˡ-map-filter {l = govSt} {P? = P?}) a∈
... | b , b∈ , refl , Pb = Inverse.to (map-∈↔ (GovActionDeposit ∘ proj₁)) (b , (b∈ , refl))
main-invariance-lemma :
filterˢ isGADeposit (dom utxoDeps) ≡ᵉ' fromList (map' (GovActionDeposit ∘ proj₁) govSt)
→ filterˢ isGADeposit (dom utxoDeps') ≡ᵉ' fromList (map' (GovActionDeposit ∘ proj₁) (filter P? govSt))
main-invariance-lemma HYP a = let open R.EquationalReasoning in
a ∈ filterˢ isGADeposit (dom utxoDeps') ∼⟨ R.SK-sym ∈-filter ⟩
(isGADeposit a × a ∈ dom utxoDeps') ∼⟨ R.K-refl ×-cong ∈-resᶜ-dom ⟩
(isGADeposit a × a ∉ ΔΠ' × ∃[ q ] (a , q) ∈ utxoDeps) ∼⟨ ×-⇔-swap ⟩
(a ∉ ΔΠ' × isGADeposit a × ∃[ q ] (a , q) ∈ utxoDeps) ∼⟨ R.K-refl ×-cong (R.K-refl ×-cong dom∈)⟩
(a ∉ ΔΠ' × isGADeposit a × a ∈ dom utxoDeps) ∼⟨ R.K-refl ×-cong ∈-filter ⟩
(a ∉ ΔΠ' × a ∈ filterˢ isGADeposit (dom utxoDeps)) ∼⟨ R.K-refl ×-cong (HYP a) ⟩
(a ∉ ΔΠ' × a ∈ fromList (map' (GovActionDeposit ∘ proj₁) govSt)) ∼⟨ R.K-refl ×-cong (R.SK-sym ∈-fromList)⟩
(a ∉ ΔΠ' × a ∈ˡ map' (GovActionDeposit ∘ proj₁) govSt) ∼⟨ map-filter-decomp a ⟩
a ∈ˡ map' (GovActionDeposit ∘ proj₁) (filter P? govSt) ∼⟨ ∈-fromList ⟩
a ∈ fromList (map' (GovActionDeposit ∘ proj₁) (filter P? govSt)) ∎
u0 = EPOCH-updates0 (RatifyStateOf eps) (LStateOf eps)
ls₁ = record (LStateOf eps') { utxoSt = EPOCH-Updates0.utxoSt' u0 }
mutual
open LState
open CertState
retiredDeposits : ℙ DepositPurpose
retiredDeposits = mapˢ PoolDeposit ((PStateOf eps) .retiring ⁻¹ e)
ratifiesSnapMatch : govDepsMatch (LStateOf eps) → govDepsMatch ls₁
ratifiesSnapMatch =
≡ᵉ.trans (filter-cong $ dom-cong (res-comp-cong $ ≡ᵉ.sym ΔΠ'≡ΔΠ))
∘ from ≡ᵉ⇔≡ᵉ' ∘ main-invariance-lemma ∘ to ≡ᵉ⇔≡ᵉ'
poolReapMatch : govDepsMatch ls₁ → govDepsMatch (LStateOf eps')
poolReapMatch = ≡ᵉ.trans dropRetiredDeposits
dropRetiredDeposits :
filterˢ isGADeposit (dom (DepositsOf ls₁ ∣ retiredDeposits ᶜ)) ≡ᵉ
filterˢ isGADeposit (dom (DepositsOf ls₁))
dropRetiredDeposits = begin
filterˢ isGADeposit (dom (DepositsOf ls₁ ∣ retiredDeposits ᶜ))
≈⟨ ∪-identityˡ _ ⟨
∅ˢ ∪ filterˢ isGADeposit (dom (DepositsOf ls₁ ∣ retiredDeposits ᶜ))
≈⟨ ∪-cong
(filter-∅ noGADepositIsRetired)
(IsEquivalence.refl ≡ᵉ-isEquivalence)
⟨
filterˢ isGADeposit (dom (DepositsOf ls₁ ∣ retiredDeposits))
∪
filterˢ isGADeposit (dom (DepositsOf ls₁ ∣ retiredDeposits ᶜ))
≈⟨ filter-hom-∪ ⟨
filterˢ isGADeposit
(dom (DepositsOf ls₁ ∣ retiredDeposits)
∪
dom (DepositsOf ls₁ ∣ retiredDeposits ᶜ)
)
≈⟨ filter-cong dom∪ ⟨
filterˢ isGADeposit
(dom
((DepositsOf ls₁ ∣ retiredDeposits) ˢ
∪
(DepositsOf ls₁ ∣ retiredDeposits ᶜ) ˢ
)
)
≈⟨ IsEquivalence.refl ≡ᵉ-isEquivalence ⟩
filterˢ isGADeposit
(Rel.dom
(((DepositsOf ls₁ ˢ) ∣ʳ retiredDeposits)
∪
((DepositsOf ls₁ ˢ) ∣ʳ retiredDeposits ᶜ)
)
)
≈⟨ filter-cong $ dom-cong (res-ex-∪ dec¹) ⟩
filterˢ isGADeposit (dom (DepositsOf ls₁))
∎
where
open SetoidReasoning (≡ᵉ-Setoid {A = DepositPurpose})
open import Relation.Binary using (IsEquivalence)
import Axiom.Set.Rel th as Rel
noGADepositIsRetired
: (d : DepositPurpose)
→ d ∈ dom (DepositsOf ls₁ ∣ retiredDeposits)
→ ¬ isGADeposit d
noGADepositIsRetired d d∈res dIsGA
rewrite (proj₂ $ d≡PoolDepositA d d∈res)
with dIsGA
... | ()
d≡PoolDepositA
: (d : DepositPurpose)
→ d ∈ dom (DepositsOf ls₁ ∣ retiredDeposits)
→ ∃[ kh ] d ≡ PoolDeposit kh
d≡PoolDepositA d d∈res =
Product.map₂ proj₁ $
∈-map⁻' $
res-dom d∈res
where import Data.Product.Base as Product using (map₂)